Source file Cut_form.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
(** {1 Universally Quantified Conjunction of Clauses} *)
open Logtk
module Fmt = CCFormat
module T = Term
type var = Term.var
type term = Term.t
type clause = Literals.t
type form = clause list
type t = {
vars: T.VarSet.t;
cs: form;
}
type cut_form = t
let trivial = {cs=[]; vars=T.VarSet.empty}
let make cs =
if cs=[] then trivial
else (
let vars =
Iter.of_list cs
|> Iter.flat_map Literals.Seq.vars
|> T.VarSet.of_seq
and cs = CCList.sort_uniq ~cmp:Literals.compare cs in
{cs; vars;}
)
let vars t = t.vars
let cs t = t.cs
let hash (f:t): int = Hash.list Literals.hash f.cs
let equal f1 f2: bool = CCList.equal Literals.equal f1.cs f2.cs
let compare f1 f2 = CCList.compare Literals.compare f1.cs f2.cs
let pp out (f:t): unit =
let pp_c = Literals.pp in
let pp_body out () = match f.cs with
| [c] -> pp_c out c
| _ -> Fmt.fprintf out "@<1>∧{@[<hv>%a@]}" (Util.pp_list ~sep:"," pp_c) f.cs
in
if T.VarSet.is_empty f.vars then (
pp_body out ()
) else (
Fmt.fprintf out "(@[<2>forall %a.@ %a@])"
(Util.pp_list ~sep:" " Type.pp_typed_var) (T.VarSet.to_list f.vars) pp_body ()
)
let to_string = Fmt.to_string pp
let pp_tstp out (f:t): unit =
let pp_c = Fmt.within "(" ")" Literals.pp_tstp in
let pp_body out () = match f.cs with
| [c] -> pp_c out c
| _ -> Fmt.fprintf out "(@[%a@])" (Util.pp_list ~sep:" & " pp_c) f.cs
in
if T.VarSet.is_empty f.vars then (
pp_body out ()
) else (
Fmt.fprintf out "(@[<2>![%a]:@ (%a)@])"
(Util.pp_list Type.TPTP.pp_typed_var) (T.VarSet.to_list f.vars) pp_body ()
)
let pp_zf out (f:t): unit =
let pp_c = Fmt.within "(" ")" Literals.pp_zf in
let pp_body out () = match f.cs with
| [c] -> pp_c out c
| _ -> Fmt.fprintf out "(@[%a@])" (Util.pp_list ~sep:" && " pp_c) f.cs
in
if T.VarSet.is_empty f.vars then (
pp_body out ()
) else (
Fmt.fprintf out "(@[<2>forall %a.@ (%a)@])"
(Util.pp_list Type.ZF.pp_typed_var) (T.VarSet.to_list f.vars) pp_body ()
)
let ind_vars t =
vars t
|> T.VarSet.to_list
|> List.filter
(fun v ->
let ty = HVar.ty v in
begin match Ind_ty.as_inductive_type ty with
| Some (ity,_) -> Ind_ty.is_recursive ity
| None -> false
end)
let apply_subst renaming subst (f,sc): t =
let cs =
List.map (fun lits -> Literals.apply_subst renaming subst (lits,sc)) f.cs
in
make cs
let subst1 (v:var) (t:term) (f:t): t =
let renaming = Subst.Renaming.create () in
let subst =
Subst.FO.bind Subst.empty ((v:var:>InnerTerm.t HVar.t),0) (t,1)
in
apply_subst renaming subst (f,0)
let variant_ ~subst (f1,sc1)(f2,sc2): _ Iter.t =
Unif.unif_list_com ~size:`Same subst
~op:(fun subst c1 c2 k ->
Literals.variant ~subst c1 c2 (fun (subst,_tags) -> k subst))
(f1.cs,sc1)(f2.cs,sc2)
let are_variant f1 f2: bool =
not @@ Iter.is_empty @@ variant_ ~subst:Subst.empty (f1,1)(f2,0)
let normalize (f:t): t = cs f |> Test_prop.normalize_form |> make
let to_s_form (f:t) =
let module F = TypedSTerm.Form in
let ctx = Term.Conv.create() in
let l = List.map (Literals.Conv.to_s_form ~ctx) (cs f) in
F.and_ l |> F.close_forall
module Pos = struct
module P = Position
let bad_pos f p = Util.invalid_argf "invalid pos `%a`@ in %a" P.pp p pp f
let clause_at f p = match p with
| P.Stop -> bad_pos f p
| P.Arg (n,p') ->
let cs = cs f in
if n<0 || n >= List.length cs then bad_pos f p;
List.nth cs n, p'
| _ -> bad_pos f p
let lit_at f p =
let c, p = clause_at f p in
Literals.Pos.lit_at c p
let at f p: term =
let lit, p = lit_at f p in
Literal.Pos.at lit p
let replace_many f m: t =
let l = cs f in
P.Map.fold
(fun p by l ->
let n, p_c = match p with P.Arg (n,p') -> n,p' | _ -> assert false in
let c = List.nth l n in
let c' = Array.copy c in
Literals.Pos.replace c' ~at:p_c ~by;
CCList.set_at_idx n c' l)
m l
|> make
let replace f ~at ~by = replace_many f (P.Map.singleton at by)
end
module Seq = struct
let terms f =
cs f
|> Iter.of_list
|> Iter.flat_map Literals.Seq.terms
let terms_with_pos ?(subterms=true) f =
cs f
|> Iter.of_list
|> Util.seq_zipi
|> Iter.flat_map
(fun (i,c) ->
Iter.of_array_i c
|> Iter.map (fun (j,lit) -> i, j, lit))
|> Iter.flat_map
(fun (i,j,lit) ->
let position = Position.(arg i @@ arg j @@ stop) in
Literal.fold_terms lit
~position ~ord:Ordering.none ~which:`All ~vars:true ~subterms)
end
module FV_tbl(X : Map.OrderedType) = struct
type value = X.t
let to_lits (f:cut_form) =
cs f
|> Iter.of_list
|> Iter.flat_map_l Literals.to_form
module FV = FV_tree.Make(struct
type t = cut_form * X.t
let compare (l1,v1)(l2,v2) =
let open CCOrd.Infix in
compare l1 l2 <?> (X.compare, v1, v2)
let to_lits (l,_) = to_lits l
let labels _ = Util.Int_set.empty
end)
type t = {
mutable fv: FV.t;
}
let create () = {fv=FV.empty ()}
let add t k v = t.fv <- FV.add t.fv (k,v)
let get t k =
FV.retrieve_alpha_equiv t.fv (to_lits k) Util.Int_set.empty
|> Iter.find_map
(fun (k',v) -> if are_variant k k' then Some v else None)
let mem t k = get t k |> CCOpt.is_some
let to_seq t = FV.iter t.fv
end