aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/dp/dp_sorts.ml
blob: 7dbdfa5619d86016be92717201d56f79cf877069 (plain)
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