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/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