Tidy up Definition module

backend/cn/lib/cLogicalFuns.ml

@@ -714,8 +714,8 @@ let c_fun_to_it id_loc glob_context (id : Sym.t) fsym def (fn : 'bty Mu.fun_map_
 let upd_def (loc, sym, def_tm) =
   let open Definition.Function in
   let@ def = get_logical_function_def loc sym in
-  match def.definition with
-  | Uninterp -> add_logical_function sym { def with definition = Def def_tm }
+  match def.body with
+  | Uninterp -> add_logical_function sym { def with body = Def def_tm }
   | _ ->
     fail_n
       { loc;

backend/cn/lib/check.ml

@@ -2230,7 +2230,7 @@ let record_and_check_logical_functions funs =
   let@ () =
     ListM.iterM
       (fun (name, def) ->
-        let@ simple_def = WellTyped.WLFD.welltyped { def with definition = Uninterp } in
+        let@ simple_def = WellTyped.WLFD.welltyped { def with body = Uninterp } in
         add_logical_function name simple_def)
       recursive
   in

backend/cn/lib/cn_internal_to_ail.ml

@@ -2932,7 +2932,7 @@ let rec generate_record_opt pred_sym = function
 
 (* TODO: Finish with rest of function - maybe header file with A.Decl_function (cn.h?) *)
 let cn_to_ail_function_internal
-  (fn_sym, (lf_def : Definition.Function.definition))
+  (fn_sym, (lf_def : Definition.Function.t))
   (cn_datatypes : A.sigma_cn_datatype list)
   (cn_functions : A.sigma_cn_function list)
   : ((Locations.t * A.sigma_declaration)
@@ -2942,7 +2942,7 @@ let cn_to_ail_function_internal
   let ret_type = bt_to_ail_ctype ~pred_sym:(Some fn_sym) lf_def.return_bt in
   (* let ret_type = mk_ctype C.(Pointer (empty_qualifiers, ret_type)) in *)
   let bs, ail_func_body_opt =
-    match lf_def.definition with
+    match lf_def.body with
     | Def it | Rec_Def it ->
       let bs, ss =
         cn_to_ail_expr_internal_with_pred_name (Some fn_sym) cn_datatypes [] it Return

backend/cn/lib/cn_internal_to_ail.mli

@@ -148,7 +148,7 @@ val cn_to_ail_records
   A.sigma_tag_definition list
 
 val cn_to_ail_function_internal
-  :  Sym.t * Definition.Function.definition ->
+  :  Sym.t * Definition.Function.t ->
   A.sigma_cn_datatype list ->
   A.sigma_cn_function list ->
   ((Locations.t * A.sigma_declaration)

backend/cn/lib/compile.ml

@@ -1218,7 +1218,7 @@ let translate_cn_function env (def : cn_function) =
             })
       def.cn_func_attrs
   in
-  let@ definition =
+  let@ body =
     match def.cn_func_body with
     | Some body ->
       let@ body = translate_cn_func_body env' body in
@@ -1232,7 +1232,7 @@ let translate_cn_function env (def : cn_function) =
         args = List.map_snd SBT.proj args;
         return_bt = SBT.proj return_bt;
         emit_coq = not coq_unfold;
-        definition
+        body
       }
   in
   return (def.cn_func_name, def2)
@@ -1380,7 +1380,7 @@ let translate_cn_clauses env clauses =
         Pure.handle "Predicate guards" (ET.translate_cn_expr Sym.Set.empty env e_)
       in
       let@ cl = translate_cn_clause env cl_ in
-      self (Def.{ loc; guard = IT.Surface.proj e; packing_ft = cl } :: acc) clauses'
+      self ({ loc; guard = IT.Surface.proj e; packing_ft = cl } :: acc) clauses'
   in
   let@ xs = self [] clauses in
   return (List.rev xs)

backend/cn/lib/context.ml

@@ -280,7 +280,7 @@ let not_given_to_solver ctxt =
   let preds =
     Sym.Map.bindings
       (Sym.Map.filter
-         (fun _ v -> not (Definition.given_to_solver v))
+         (fun _ v -> not (Definition.Predicate.given_to_solver v))
          global.resource_predicates)
   in
   (constraints, funs, preds)

backend/cn/lib/definition.ml

@@ -3,33 +3,33 @@ module AT = ArgumentTypes
 module LAT = LogicalArgumentTypes
 
 module Function = struct
-  type def_or_uninterp =
+  type body =
     | Def of IT.t
     | Rec_Def of IT.t
     | Uninterp
 
-  let subst_def_or_uninterp subst = function
+  let subst_body subst = function
     | Def it -> Def (IT.subst subst it)
     | Rec_Def it -> Rec_Def (IT.subst subst it)
     | Uninterp -> Uninterp
 
 
-  type definition =
+  type t =
     { loc : Locations.t;
       args : (Sym.t * BaseTypes.t) list;
       (* If the predicate is supposed to get used in a quantified form, one of the arguments
          has to be the index/quantified variable. For now at least. *)
       return_bt : BaseTypes.t;
       emit_coq : bool;
-      definition : def_or_uninterp
+      body : body
     }
 
   let is_recursive def =
-    match def.definition with Rec_Def _ -> true | Def _ -> false | Uninterp -> false
+    match def.body with Rec_Def _ -> true | Def _ -> false | Uninterp -> false
 
 
   let given_to_solver def =
-    match def.definition with Rec_Def _ -> false | Def _ -> true | Uninterp -> false
+    match def.body with Rec_Def _ -> false | Def _ -> true | Uninterp -> false
 
 
   let pp_args xs =
@@ -39,71 +39,39 @@ module Function = struct
       xs
 
 
-  let pp_def nm def =
+  let pp nm def =
     let open Pp in
     nm
     ^^ colon
     ^^^ pp_args def.args
     ^^ colon
     ^/^
-    match def.definition with
+    match def.body with
     | Uninterp -> !^"uninterpreted"
     | Def t -> IT.pp t
     | Rec_Def t -> !^"rec:" ^^^ IT.pp t
 
 
-  let open_fun def_args def_body args =
+  let open_ def_args def_body args =
     let su = IT.make_subst (List.map2 (fun (s, _) arg -> (s, arg)) def_args args) in
     IT.subst su def_body
 
 
   let unroll_once def args =
-    match def.definition with
-    | Def body | Rec_Def body -> Some (open_fun def.args body args)
+    match def.body with
+    | Def body | Rec_Def body -> Some (open_ def.args body args)
     | Uninterp -> None
 
 
-  let try_open_fun def args =
-    match def.definition with
-    | Def body -> Some (open_fun def.args body args)
+  let try_open def args =
+    match def.body with
+    | Def body -> Some (open_ def.args body args)
     | Rec_Def _ -> None
     | Uninterp -> None
 
 
-  (* let try_open_fun_to_term def name args = Option.map (fun body -> Body.to_term
-     def.return_bt body ) (try_open_fun def name args) *)
-
-  (* let add_unfolds_to_terms preds terms = let rec f acc t = match IT.term t with |
-     IT.Apply (name, ts) -> let def = Sym.Map.find name preds in begin match
-     try_open_fun_to_term def name ts with | None -> acc | Some t2 -> f (t2 :: acc) t2 end |
-     _ -> acc in IT.fold_list (fun _ acc t -> f acc t) [] terms terms *)
-
-  (* (\* Check for cycles in the logical predicate graph, which would cause *)
-  (*    the system to loop trying to unfold them. Predicates whose definition *)
-  (*    are marked with Rec_Def aren't checked, as cycles there are expected. *\) *)
-  (* let cycle_check (defs : definition Sym.Map.t) = *)
-  (*   let def_preds nm =  *)
-  (*     let def =  Sym.Map.find nm defs in *)
-  (*     begin match def.definition with *)
-  (*     | Def t -> Sym.Set.elements (IT.preds_of (Body.to_term def.return_bt t)) *)
-  (*     | _ -> [] *)
-  (*     end *)
-  (*   in *)
-  (*   let rec search known_ok = function *)
-  (*     | [] -> None *)
-  (*     | (nm, Some path) :: q -> if Sym.Set.mem nm known_ok *)
-  (*       then search known_ok q *)
-  (*       else if List.exists (Sym.equal nm) path *)
-  (*       then Some (List.rev path @ [nm]) *)
-  (*       else *)
-  (*         let deps = List.map (fun p -> (p, Some (nm :: path))) (def_preds nm) in *)
-  (*         search known_ok (deps @ [(nm, None)] @ q) *)
-  (*     | (nm, None) :: q -> search (Sym.Set.add nm known_ok) q *)
-  (* in search Sym.Set.empty (List.map (fun (p, _) -> (p, Some [])) (Sym.Map.bindings
-     defs)) *)
-
   (*Extensibility hook. For now, all functions are displayed as "interesting" in error reporting*)
-  let is_interesting : definition -> bool = fun _ -> true
+  let is_interesting : t -> bool = fun _ -> true
 end
 
 module Clause = struct
@@ -160,6 +128,53 @@ module Predicate = struct
           (match def.clauses with
            | Some clauses -> Pp.list Clause.pp clauses
            | None -> !^"(uninterpreted)")
+
+
+  let instantiate (def : t) ptr_arg iargs =
+    match def.clauses with
+    | Some clauses ->
+      let subst =
+        IT.make_subst
+          ((def.pointer, ptr_arg)
+           :: List.map2 (fun (def_ia, _) ia -> (def_ia, ia)) def.iargs iargs)
+      in
+      Some (List.map (Clause.subst subst) clauses)
+    | None -> None
+
+
+  let identify_right_clause provable (def : t) pointer iargs =
+    match instantiate def pointer iargs with
+    | None ->
+      (* "uninterpreted" predicates cannot be un/packed *)
+      None
+    | Some clauses ->
+      let rec try_clauses : Clause.t list -> _ = function
+        | [] -> None
+        | clause :: clauses ->
+          (match provable (LogicalConstraints.T clause.guard) with
+           | `True -> Some clause
+           | `False ->
+             let loc = Locations.other __FUNCTION__ in
+             (match provable (LogicalConstraints.T (IT.not_ clause.guard loc)) with
+              | `True -> try_clauses clauses
+              | `False ->
+                Pp.debug
+                  5
+                  (lazy
+                    (Pp.item "cannot prove or disprove clause guard" (IT.pp clause.guard)));
+                None))
+      in
+      try_clauses clauses
+
+
+  (* determines if a resource predicate will be given to the solver
+   *    TODO: right now this is an overapproximation *)
+  let given_to_solver (def : t) =
+    match def.clauses with
+    | None -> false
+    | Some [] -> true
+    | Some [ _ ] -> true
+    | _ -> false
 end
 
 let alloc =
@@ -172,52 +187,5 @@ let alloc =
     }
 
 
-let instantiate_clauses (def : Predicate.t) ptr_arg iargs =
-  match def.clauses with
-  | Some clauses ->
-    let subst =
-      IT.make_subst
-        ((def.pointer, ptr_arg)
-         :: List.map2 (fun (def_ia, _) ia -> (def_ia, ia)) def.iargs iargs)
-    in
-    Some (List.map (Clause.subst subst) clauses)
-  | None -> None
-
-
-let identify_right_clause provable (def : Predicate.t) pointer iargs =
-  match instantiate_clauses def pointer iargs with
-  | None ->
-    (* "uninterpreted" predicates cannot be un/packed *)
-    None
-  | Some clauses ->
-    let rec try_clauses : Clause.t list -> _ = function
-      | [] -> None
-      | clause :: clauses ->
-        (match provable (LogicalConstraints.T clause.guard) with
-         | `True -> Some clause
-         | `False ->
-           let loc = Locations.other __FUNCTION__ in
-           (match provable (LogicalConstraints.T (IT.not_ clause.guard loc)) with
-            | `True -> try_clauses clauses
-            | `False ->
-              Pp.debug
-                5
-                (lazy
-                  (Pp.item "cannot prove or disprove clause guard" (IT.pp clause.guard)));
-              None))
-    in
-    try_clauses clauses
-
-
-(* determines if a resource predicate will be given to the solver
-   TODO: right now this is an overapproximation *)
-let given_to_solver (def : Predicate.t) =
-  match def.clauses with
-  | None -> false
-  | Some [] -> true
-  | Some [ _ ] -> true
-  | _ -> false
-
-
 (*Extensibility hook. For now, all predicates are displayed as "interesting" in error reporting*)
 let is_interesting : Predicate.t -> bool = fun _ -> true

backend/cn/lib/definition.mli

@@ -0,0 +1,73 @@
+module Function : sig
+  type body =
+    | Def of IndexTerms.t
+    | Rec_Def of IndexTerms.t
+    | Uninterp
+
+  val subst_body : [ `Rename of Sym.t | `Term of IndexTerms.t ] Subst.t -> body -> body
+
+  type t =
+    { loc : Locations.t;
+      args : (Sym.t * BaseTypes.t) list;
+      return_bt : BaseTypes.t;
+      emit_coq : bool;
+      body : body
+    }
+
+  val is_recursive : t -> bool
+
+  val given_to_solver : t -> bool
+
+  val pp_args : (Cerb_frontend.Symbol.sym * unit BaseTypes.t_gen) list -> Pp.document
+
+  val pp : Pp.document -> t -> Pp.document
+
+  val open_ : (Sym.t * 'a) list -> IndexTerms.t -> IndexTerms.t list -> IndexTerms.t
+
+  val unroll_once : t -> IndexTerms.t list -> IndexTerms.t option
+
+  val try_open : t -> IndexTerms.t list -> IndexTerms.t option
+
+  val is_interesting : t -> bool
+end
+
+module Clause : sig
+  type t =
+    { loc : Locations.t;
+      guard : IndexTerms.t;
+      packing_ft : LogicalArgumentTypes.packing_ft
+    }
+
+  val pp : t -> Pp.document
+
+  val subst : [ `Rename of Sym.t | `Term of IndexTerms.t ] Subst.t -> t -> t
+
+  val lrt : IndexTerms.t -> IndexTerms.t LogicalArgumentTypes.t -> LogicalReturnTypes.t
+end
+
+module Predicate : sig
+  type t =
+    { loc : Locations.t;
+      pointer : Sym.t;
+      iargs : (Sym.t * BaseTypes.t) list;
+      oarg_bt : BaseTypes.t;
+      clauses : Clause.t list option
+    }
+
+  val pp : t -> Pp.document
+
+  val instantiate : t -> IndexTerms.t -> IndexTerms.t list -> Clause.t list option
+
+  val identify_right_clause
+    :  (LogicalConstraints.logical_constraint -> [< `False | `True ]) ->
+    t ->
+    IndexTerms.t ->
+    IndexTerms.t list ->
+    Clause.t option
+
+  val given_to_solver : t -> bool
+end
+
+val alloc : Predicate.t
+
+val is_interesting : Predicate.t -> bool