CN: Separate well-typed and consistency checks

WellTyped/well-formedness checks were intertwined with the typing monad
because they also performed consistency checks. This made running just
the well-formedness checks slower, and did not allow users to opt-out
of running the consistency check.

This commit adds variants `consistent` functions, which are variants
on the `welltyped` functions. The latter add variables to scope and
check basetypes; the former add variables to scope, constraints
and resources.

It also tidies up the wellTyped.ml module to clarify and restrict which
of the typing monad functions it was using. This will be the first step
of many to factor out the logging and the error reporting for different
phases.

This commit also required an update to the `pure` function in the typing
monad, so that it can work without a solver (functionality with a
solver initialised should be unaffected).

Slightly awkwardly, the reshuffle also required gathering and delaying
adding the range constraints for global variables, since adding
constraints and resources both require the solver to be initialised.

This can and should be tidied up, which will come in subsequent
commits, but for now this should pass all tests.

backend/cn/bin/main.ml

@@ -322,9 +322,9 @@ let verify
     ~magic_comment_char_dollar (* Callbacks *)
     ~handle_error:(handle_type_error ~json ?output_dir ~serialize_json:json_trace)
     ~f:(fun ~prog5:_ ~ail_prog:_ ~statement_locs:_ ~paused ->
-      let check (functions, lemmas) =
+      let check (functions, global_var_constraints, lemmas) =
         let open Typing in
-        let@ errors = Check.time_check_c_functions functions in
+        let@ errors = Check.time_check_c_functions (global_var_constraints, functions) in
         if not quiet then
           List.iter
             (fun (fn, err) ->

backend/cn/lib/check.ml

@@ -2280,24 +2280,21 @@ let record_and_check_resource_predicates preds =
     preds
 
 
-let record_globals : 'bty. (Sym.t * 'bty Mu.globs) list -> unit m =
+let record_globals : 'bty. (Sym.t * 'bty Mu.globs) list -> LC.t list m =
   fun globs ->
-  (* TODO: check the expressions *)
-  ListM.iterM
-    (fun (sym, def) ->
+  ListM.fold_leftM
+    (fun acc (sym, def) ->
       match def with
       | Mu.GlobalDef (ct, _) | GlobalDecl ct ->
         let@ () = WellTyped.WCT.is_ct (Loc.other __LOC__) ct in
         let bt = BT.(Loc ()) in
         let info = (Loc.other __LOC__, lazy (Pp.item "global" (Sym.pp sym))) in
         let@ () = add_a sym bt info in
         let here = Locations.other __LOC__ in
-        let@ () =
-          add_c here (LC.T (IT.good_pointer ~pointee_ct:ct (sym_ (sym, bt, here)) here))
-        in
+        let good = LC.T (IT.good_pointer ~pointee_ct:ct (sym_ (sym, bt, here)) here) in
         let ptr = sym_ (sym, bt, here) in
-        let@ () = add_c here (LC.T (IT.hasAllocId_ ptr here)) in
-        let@ () =
+        let hasAllocId = LC.T (IT.hasAllocId_ ptr here) in
+        let range =
           if !IT.use_vip then
             let module H = Alloc.History in
             let H.{ base; size } = H.(split (lookup_ptr ptr here) here) in
@@ -2311,11 +2308,13 @@ let record_globals : 'bty. (Sym.t * 'bty Mu.globs) list -> unit m =
                 ]
                 here
             in
-            add_c here (LC.T bounds)
+            [ LC.T bounds ]
           else
-            return ()
+            []
         in
-        return ())
+        (* TODO: check the expressions *)
+        return (good :: hasAllocId :: (range @ acc)))
+    []
     globs
 
 
@@ -2645,8 +2644,7 @@ let check_decls_lemmata_fun_specs (file : unit Mu.file) =
   let@ () = record_tagdefs file.tagDefs in
   let@ () = check_tagdefs file.tagDefs in
   let@ () = record_and_check_datatypes file.datatypes in
-  let@ () = init_solver () in
-  let@ () = record_globals file.globs in
+  let@ global_var_constraints = record_globals file.globs in
   let@ () = register_fun_syms file in
   let@ () =
     ListM.iterM (add_stdlib_spec file.call_funinfo) (Sym.Set.elements file.stdlib_syms)
@@ -2662,14 +2660,41 @@ let check_decls_lemmata_fun_specs (file : unit Mu.file) =
   let@ _trusted, checked = wf_check_and_record_functions file.funs file.call_funinfo in
   Pp.debug 3 (lazy (Pp.headline "type-checked C functions and specifications."));
   Cerb_debug.end_csv_timing "decl, lemmata, function specification checking";
-  return (List.rev checked, lemmata)
+  return (List.rev checked, global_var_constraints, lemmata)
 
 
 (** With CSV timing enabled, check the provided functions with
     [check_c_functions]. See that function for more information on the
     semantics of checking. *)
-let time_check_c_functions (checked : c_function list) : (string * TypeErrors.t) list m =
+let time_check_c_functions (global_var_constraints, (checked : c_function list))
+  : (string * TypeErrors.t) list m
+  =
   Cerb_debug.begin_csv_timing () (*type checking functions*);
+  let@ () = init_solver () in
+  let here = Locations.other __LOC__ in
+  let@ () = add_cs here global_var_constraints in
+  let@ global = get_global () in
+  let@ () =
+    Sym.Map.fold
+      (fun _ def acc ->
+        (* I think this avoids a left-recursion in the monad bind *)
+        let@ () = WellTyped.WRPD.consistent def in
+        acc)
+      global.resource_predicates
+      (return ())
+  in
+  let@ () =
+    Sym.Map.fold
+      (fun _ (loc, def, _) acc ->
+        match def with
+        | None -> acc
+        | Some def ->
+          (* I think this avoids a left-recursion in the monad bind *)
+          let@ () = WellTyped.WFT.consistent "proc/fun" loc def in
+          acc)
+      global.fun_decls
+      (return ())
+  in
   let@ errors = check_c_functions checked in
   Cerb_debug.end_csv_timing "type checking functions";
   return errors
@@ -2678,7 +2703,17 @@ let time_check_c_functions (checked : c_function list) : (string * TypeErrors.t)
 let generate_lemmas lemmata o_lemma_mode =
   let@ global = get_global () in
   match o_lemma_mode with
-  | Some mode -> lift (Lemmata.generate global mode lemmata)
+  | Some mode ->
+    let@ () =
+      Sym.Map.fold
+        (fun sym (loc, lemma_typ) acc ->
+          (* I think this avoids a left-recursion in the monad bind *)
+          let@ () = WellTyped.WLemma.consistent loc sym lemma_typ in
+          acc)
+        global.lemmata
+        (return ())
+    in
+    lift (Lemmata.generate global mode lemmata)
   | None -> return ()
 
 (* TODO:

backend/cn/lib/resourceInference.ml

@@ -160,7 +160,7 @@ module General = struct
     =
     Pp.(debug 7 (lazy (item __LOC__ (Req.pp (P requested)))));
     let start_timing = Pp.time_log_start __LOC__ "" in
-    let@ oarg_bt = WellTyped.oarg_bt_of_pred loc requested.name in
+    let@ oarg_bt = WellTyped.WRS.oarg_bt_of_pred loc requested.name in
     let@ provable = provable loc in
     let@ global = get_global () in
     let@ simp_ctxt = simp_ctxt () in
@@ -384,7 +384,7 @@ module General = struct
 
   and qpredicate_request loc uiinfo (requested : Req.QPredicate.t) =
     let@ o_oarg = qpredicate_request_aux loc uiinfo requested in
-    let@ oarg_item_bt = WellTyped.oarg_bt_of_pred loc requested.name in
+    let@ oarg_item_bt = WellTyped.WRS.oarg_bt_of_pred loc requested.name in
     match o_oarg with
     | None -> return None
     | Some (oarg, rw_time) ->

backend/cn/lib/typing.ml

@@ -72,9 +72,9 @@ let pause_to_result (pause : 'a pause) : 'a Or_TypeError.t = Result.map fst paus
 
 let pure (m : 'a t) : 'a t =
   fun s ->
-  Solver.push (Option.get s.solver);
+  Option.iter Solver.push s.solver;
   let outcome = match m s with Ok (a, _) -> Ok (a, s) | Error e -> Error e in
-  Solver.pop (Option.get s.solver) 1;
+  Option.iter (fun s -> Solver.pop s 1) s.solver;
   outcome
 
 

backend/cn/lib/typing.mli

@@ -1,5 +1,3 @@
-type solver
-
 type 'a t
 
 type 'a m = 'a t