Use the new definition type for predicates in Translate

Author: Halbaroth

src/lib/frontend/frontend.ml

@@ -145,7 +145,7 @@ module type S = sig
 
   val assume : (string * E.t * bool) process
 
-  val pred_def : (string * E.t) process
+  val pred_def : E.def process
 
   val query : (string * E.t * Ty.goal_sort) process
 
@@ -350,10 +350,10 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
       | `Unsat ->
         env.expl <- expl
 
-  let internal_pred_def ?(loc = DStd.Loc.dummy) (name, f) env =
+  let internal_pred_def ?(loc = DStd.Loc.dummy) (E.{ name; axiom; _ } as def) env =
     if not (unused_context name env.used_context) then
-      let expl = mk_root_dep name f loc in
-      SAT.pred_def env.sat_env f name expl loc;
+      let expl = mk_root_dep name def.E.axiom loc in
+      SAT.pred_def env.sat_env axiom name expl loc;
       env.expl <- expl
 
   let internal_query ?(loc = DStd.Loc.dummy) (n, f, sort) env =
@@ -447,8 +447,8 @@ module Make(SAT : Sat_solver_sig.S) : S with type sat_env = SAT.t = struct
       | Pop n -> check_if_over (internal_pop ~loc:d.st_loc n) env
       | Assume (n, f, mf) ->
         check_if_over (internal_assume ~loc:d.st_loc (n, f, mf)) env
-      | PredDef (f, name) ->
-        check_if_over (internal_pred_def ~loc:d.st_loc (name, f)) env
+      | PredDef def ->
+        check_if_over (internal_pred_def ~loc:d.st_loc def) env
       | Query (n, f, sort) ->
         begin
           (* If we have reached an unknown state, we can return it right

src/lib/frontend/frontend.mli

@@ -72,7 +72,7 @@ module type S = sig
 
   val assume : (string * Expr.t * bool) process
 
-  val pred_def : (string * Expr.t) process
+  val pred_def : Expr.def process
 
   val query : (string * Expr.t * Ty.goal_sort) process
 

src/lib/frontend/translate.ml

@@ -1830,25 +1830,41 @@ let make file acc stmt =
 
             begin match DStd.Tag.get tags DE.Tags.predicate with
               | Some () ->
-                let decl_kind = E.Dpredicate defn in
-                let ff =
-                  mk_expr ~loc:st_loc ~name_base
+                (* let decl_kind = E.Dpredicate defn in
+                   let ff =
+                   mk_expr ~loc:st_loc ~name_base
                     ~toplevel:false ~decl_kind body
-                in
-                let qb = E.mk_eq ~iff:true defn ff in
-                let ff =
-                  E.mk_forall name_base DStd.Loc.dummy binders [] qb
+                   in
+                   let qb = E.mk_eq ~iff:true defn ff in
+                   let ff =
+                   E.mk_forall name_base DStd.Loc.dummy binders [] qb
                     ~toplevel:true ~decl_kind
-                in
-                assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty));
-                let ff = E.purify_form ff in
-                let e =
-                  if Ty.TvSet.is_empty (E.free_type_vars ff) then ff
-                  else
+                   in
+                   assert (Var.Map.is_empty (E.free_vars ff Var.Map.empty));
+                   let ff = E.purify_form ff in
+                   let e =
+                   if Ty.TvSet.is_empty (E.free_type_vars ff) then ff
+                   else
                     E.mk_forall name_base st_loc
                       Var.Map.empty [] ff ~toplevel:true ~decl_kind
+                   in *)
+                let args =
+                  List.map (
+                    fun (DE.{ path; id_ty; _ } as tv) ->
+                      let ty = dty_to_ty id_ty in
+                      let v = Var.of_string (get_basename path) in
+                      Cache.store_sy tv (Sy.var v);
+                      (v, ty)
+                  ) terml
+                in
+                let body =
+                  mk_expr
+                    ~loc:st_loc ~name_base ~toplevel:false ~decl_kind:Daxiom body
+                in
+                let def =
+                  E.mk_definition ~loc:st_loc ~name:name_base args body
                 in
-                Some C.{ st_decl = C.PredDef (e, name_base); st_loc }
+                Some C.{ st_decl = C.PredDef def; st_loc }
               | None ->
                 let decl_kind = E.Dfunction defn in
                 let ff =

src/lib/structures/commands.ml

@@ -33,7 +33,7 @@ module Log = (val Logs.src_log src : Logs.LOG)
 type sat_decl_aux =
   | Decl of Id.typed
   | Assume of string * Expr.t * bool
-  | PredDef of Expr.t * string (*name of the predicate*)
+  | PredDef of Expr.def
   | Optimize of Objective.Function.t
   | Query of string *  Expr.t * Ty.goal_sort
   | ThAssume of Expr.th_elt
@@ -54,8 +54,8 @@ let print_aux fmt = function
 
   | Assume (name, e, b) ->
     Format.fprintf fmt "assume %s(%b): @[<hov>%a@]" name b Expr.print e
-  | PredDef (e, name) ->
-    Format.fprintf fmt "pred-def %s: @[<hov>%a@]" name Expr.print e
+  | PredDef def ->
+    Format.fprintf fmt "pred-def: %a" Expr.pp_definition def
   | Query (name, e, sort) ->
     Format.fprintf fmt "query %s(%a): @[<hov>%a@]"
       name Ty.print_goal_sort sort Expr.print e

src/lib/structures/commands.mli

@@ -30,7 +30,7 @@
 type sat_decl_aux =
   | Decl of Id.typed
   | Assume of string * Expr.t * bool
-  | PredDef of Expr.t * string (*name of the predicate*)
+  | PredDef of Expr.def
   | Optimize of Objective.Function.t
   | Query of string *  Expr.t * Ty.goal_sort
   | ThAssume of Expr.th_elt

src/lib/structures/expr.ml

@@ -2820,6 +2820,9 @@ let mk_definition ~loc ~name args body =
   in
   { name; args; body; axiom; triggers }
 
+(* TODO: create a better pretty printer. *)
+let pp_definition ppf { name; _ } = Fmt.string ppf name
+
 module Set = TSet
 module Map = TMap
 

src/lib/structures/expr.mli

@@ -423,6 +423,8 @@ val mk_definition :
   t ->
   def
 
+val pp_definition : def Fmt.t
+
 val skolemize : quantified -> t
 
 val elim_let : recursive:bool -> letin -> t