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
|
open Fol
let term_has_sort x s = Fatom (Pred ("%sort_" ^ s, [x]))
let has_sort x s = term_has_sort (App (x, [])) s
let rec form = function
| True | False | Fatom _ as f -> f
| Imp (f1, f2) -> Imp (form f1, form f2)
| And (f1, f2) -> And (form f1, form f2)
| Or (f1, f2) -> Or (form f1, form f2)
| Not f -> Not (form f)
| Forall (x, ("INT" as t), f) -> Forall (x, t, form f)
| Forall (x, t, f) -> Forall (x, t, Imp (has_sort x t, form f))
| Exists (x, ("INT" as t), f) -> Exists (x, t, form f)
| Exists (x, t, f) -> Exists (x, t, Imp (has_sort x t, form f))
let sort_ax = let r = ref 0 in fun () -> incr r; "sort_ax_" ^ string_of_int !r
let hyp acc = function
| Assert (id, f) ->
(Assert (id, form f)) :: acc
| DeclVar (id, _, "INT") as d ->
d :: acc
| DeclVar (id, [], t) as d ->
(Assert (sort_ax (), has_sort id t)) :: d :: acc
| DeclVar (id, l, t) as d ->
let n = ref 0 in
let xi =
List.fold_left
(fun l t -> incr n; ("x" ^ string_of_int !n, t) :: l) [] l
in
let f =
List.fold_left
(fun f (x,t) -> if t = "INT" then f else Imp (has_sort x t, f))
(term_has_sort
(App (id, List.rev_map (fun (x,_) -> App (x,[])) xi)) t)
xi
in
let f = List.fold_left (fun f (x,t) -> Forall (x, t, f)) f xi in
(Assert (sort_ax (), f)) :: d :: acc
| DeclPred _ as d ->
d :: acc
| DeclType t as d ->
(DeclPred ("%sort_" ^ t, [t])) :: d :: acc
let query (hyps, f) =
let hyps' = List.fold_left hyp [] hyps in
List.rev hyps', form f
|
