1 files changed, 51 insertions, 0 deletions
diff --git a/contrib/dp/dp_sorts.ml b/contrib/dp/dp_sorts.ml
new file mode 100644
index 00000000..7dbdfa56
--- /dev/null
+++ b/contrib/dp/dp_sorts.ml
@@ -0,0 +1,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
+