CN: Reduce code dup. for Global related errs

Because of the split between WellTyped and Typing, the code for handling
lookups in Global was duplicated across the two. This commit adjusts the
API exposed by Global to avoid duplicating the error handling logic. It
also needs to move Global-specific errors out of TypeErrors and into
Global to avoid a circular dependency. (TypeErrors depends on Context
which depends on Global, so Global cannot reference TypeErrors types).

backend/cn/lib/cLogicalFuns.ml

@@ -738,7 +738,7 @@ let add_logical_funs_from_c call_funinfo funs_to_convert funs =
         let@ fbody =
           match Pmap.lookup c_fun_sym funs with
           | Some fbody -> return fbody
-          | None -> fail_n { loc; msg = Unknown_function c_fun_sym }
+          | None -> fail_n { loc; msg = Global (Unknown_function c_fun_sym) }
         in
         let@ it = c_fun_to_it loc global_context l_fun_sym c_fun_sym def fbody in
         Pp.debug

backend/cn/lib/check.ml

@@ -2611,7 +2611,7 @@ let record_and_check_datatypes datatypes =
     datatypes
 
 
-(** Note: this does not check loop invariants and CN statements! *)
+(** NOTE: not clear if this checks loop invariants and CN statements! *)
 let check_decls_lemmata_fun_specs (file : unit Mu.file) =
   Cerb_debug.begin_csv_timing ();
   (* decl, lemmata, function specification checking *)

backend/cn/lib/compile.ml

@@ -424,7 +424,7 @@ module EffectfulTranslation = struct
   let lookup_struct loc tag env =
     match lookup_struct_opt tag env with
     | Some def -> return def
-    | None -> fail { loc; msg = Unknown_struct tag }
+    | None -> fail { loc; msg = Global (Unknown_struct tag) }
 
 
   let lookup_member loc (_tag, def) member =
@@ -437,13 +437,13 @@ module EffectfulTranslation = struct
   let lookup_datatype loc sym env =
     match Sym.Map.find_opt sym env.datatypes with
     | Some info -> return info
-    | None -> fail TypeErrors.{ loc; msg = TypeErrors.Unknown_datatype sym }
+    | None -> fail { loc; msg = Global (Unknown_datatype sym) }
 
 
   let lookup_constr loc sym env =
     match Sym.Map.find_opt sym env.datatype_constrs with
     | Some info -> return info
-    | None -> fail TypeErrors.{ loc; msg = TypeErrors.Unknown_datatype_constr sym }
+    | None -> fail { loc; msg = Global (Unknown_datatype_constr sym) }
 
 
   let cannot_tell_pointee_ctype loc e =
@@ -852,7 +852,9 @@ module EffectfulTranslation = struct
              | Some fsig -> return fsig.return_bty
              | None ->
                fail
-                 { loc; msg = Unknown_logical_function { id = fsym; resource = false } }
+                 { loc;
+                   msg = Global (Unknown_logical_function { id = fsym; resource = false })
+                 }
            in
            return (apply_ fsym args (BaseTypes.Surface.inj bt) loc))
       | CNExpr_cons (c_nm, exprs) ->
@@ -1070,7 +1072,10 @@ module EffectfulTranslation = struct
         let@ pred_sig =
           match lookup_predicate pred env with
           | None ->
-            fail { loc; msg = Unknown_resource_predicate { id = pred; logical = false } }
+            fail
+              { loc;
+                msg = Global (Unknown_resource_predicate { id = pred; logical = false })
+              }
           | Some pred_sig -> return pred_sig
         in
         let output_bt = pred_sig.pred_output in

backend/cn/lib/global.ml

@@ -44,63 +44,89 @@ let sym_map_from_bindings xs =
   List.fold_left (fun m (nm, x) -> Sym.Map.add nm x m) Sym.Map.empty xs
 
 
-module type Reader = sig
-  type global = t
-
+type error =
+  | Unknown_function of Sym.t
+  | Unknown_struct of Sym.t
+  | Unknown_datatype of Sym.t
+  | Unknown_datatype_constr of Sym.t
+  | Unknown_resource_predicate of
+      { id : Sym.t;
+        logical : bool
+      }
+  | Unknown_logical_function of
+      { id : Sym.t;
+        resource : bool
+      }
+  | Unknown_lemma of Sym.t
+
+type global_t_alias_do_not_use = t
+
+module type ErrorReader = sig
   type 'a t
 
   val return : 'a -> 'a t
 
   val bind : 'a t -> ('a -> 'b t) -> 'b t
 
-  type state
-
-  val get : unit -> state t
+  val get_global : unit -> global_t_alias_do_not_use t
 
-  val to_global : state -> global
+  val fail : Locations.t -> error -> 'a t
 end
 
 module type Lifted = sig
   type 'a t
 
-  val get_resource_predicate_def : Sym.t -> Definition.Predicate.t option t
+  val get_resource_predicate_def : Locations.t -> Sym.t -> Definition.Predicate.t t
 
-  val get_logical_function_def : Sym.t -> Definition.Function.t option t
+  val get_logical_function_def : Locations.t -> Sym.t -> Definition.Function.t t
 
   val get_fun_decl
-    :  Sym.t ->
-    (Cerb_location.t * AT.ft option * Sctypes.c_concrete_sig) option t
+    :  Locations.t ->
+    Sym.t ->
+    (Cerb_location.t * AT.ft option * Sctypes.c_concrete_sig) t
 
-  val get_lemma : Sym.t -> (Cerb_location.t * AT.lemmat) option t
+  val get_lemma : Locations.t -> Sym.t -> (Cerb_location.t * AT.lemmat) t
 
-  val get_struct_decl : Sym.t -> Memory.struct_layout option t
+  val get_struct_decl : Locations.t -> Sym.t -> Memory.struct_layout t
 
-  val get_datatype : Sym.t -> BaseTypes.dt_info option t
+  val get_datatype : Locations.t -> Sym.t -> BaseTypes.dt_info t
 
-  val get_datatype_constr : Sym.t -> BaseTypes.constr_info option t
+  val get_datatype_constr : Locations.t -> Sym.t -> BaseTypes.constr_info t
 end
 
-module Lift (M : Reader) : Lifted with type 'a t := 'a M.t = struct
-  let lift f sym =
+module Lift (M : ErrorReader) : Lifted with type 'a t := 'a M.t = struct
+  let lift f loc sym msg =
     let ( let@ ) = M.bind in
-    let@ state = M.get () in
-    let global = M.to_global state in
-    M.return (f global sym)
+    let@ global = M.get_global () in
+    match f global sym with Some x -> M.return x | None -> M.fail loc (msg global)
+
+
+  let get_logical_function_def_opt id = get_logical_function_def id
+
+  let get_logical_function_def loc id =
+    lift get_logical_function_def loc id (fun global ->
+      let res = get_resource_predicate_def global id in
+      Unknown_logical_function { id; resource = Option.is_some res })
+
 
+  let get_resource_predicate_def loc id =
+    lift get_resource_predicate_def loc id (fun global ->
+      let log = get_logical_function_def_opt global id in
+      Unknown_resource_predicate { id; logical = Option.is_some log })
 
-  let get_resource_predicate_def = lift get_resource_predicate_def
 
-  let get_logical_function_def = lift get_logical_function_def
+  let get_fun_decl loc fsym = lift get_fun_decl loc fsym (fun _ -> Unknown_function fsym)
 
-  let get_fun_decl = lift get_fun_decl
+  let get_lemma loc lsym = lift get_lemma loc lsym (fun _ -> Unknown_lemma lsym)
 
-  let get_lemma = lift get_lemma
+  let get_struct_decl loc tag = lift get_struct_decl loc tag (fun _ -> Unknown_struct tag)
 
-  let get_struct_decl = lift get_struct_decl
+  let get_datatype loc tag =
+    lift get_datatype loc tag (fun _ -> Unknown_datatype_constr tag)
 
-  let get_datatype = lift get_datatype
 
-  let get_datatype_constr = lift get_datatype_constr
+  let get_datatype_constr loc tag =
+    lift get_datatype_constr loc tag (fun _ -> Unknown_datatype_constr tag)
 end
 
 let pp_struct_layout (tag, layout) =

backend/cn/lib/typeErrors.ml

@@ -112,21 +112,9 @@ module RequestChain = struct
 end
 
 type message =
-  | Unknown_variable of Sym.t
-  | Unknown_function of Sym.t
-  | Unknown_struct of Sym.t
-  | Unknown_datatype of Sym.t
-  | Unknown_datatype_constr of Sym.t
-  | Unknown_resource_predicate of
-      { id : Sym.t;
-        logical : bool
-      }
-  | Unknown_logical_function of
-      { id : Sym.t;
-        resource : bool
-      }
+  | Global of Global.error
   | Unexpected_member of Id.t list * Id.t
-  | Unknown_lemma of Sym.t
+  | Unknown_variable of Sym.t
   (* some from Kayvan's compilePredicates module *)
   | First_iarg_missing
   | First_iarg_not_pointer of
@@ -272,19 +260,19 @@ let pp_message te =
   | Unknown_variable s ->
     let short = !^"Unknown variable" ^^^ squotes (Sym.pp s) in
     { short; descr = None; state = None }
-  | Unknown_function sym ->
+  | Global (Unknown_function sym) ->
     let short = !^"Unknown function" ^^^ squotes (Sym.pp sym) in
     { short; descr = None; state = None }
-  | Unknown_struct tag ->
+  | Global (Unknown_struct tag) ->
     let short = !^"Struct" ^^^ squotes (Sym.pp tag) ^^^ !^"not defined" in
     { short; descr = None; state = None }
-  | Unknown_datatype tag ->
+  | Global (Unknown_datatype tag) ->
     let short = !^"Datatype" ^^^ squotes (Sym.pp tag) ^^^ !^"not defined" in
     { short; descr = None; state = None }
-  | Unknown_datatype_constr tag ->
+  | Global (Unknown_datatype_constr tag) ->
     let short = !^"Datatype constructor" ^^^ squotes (Sym.pp tag) ^^^ !^"not defined" in
     { short; descr = None; state = None }
-  | Unknown_resource_predicate { id; logical } ->
+  | Global (Unknown_resource_predicate { id; logical }) ->
     let short = !^"Unknown resource predicate" ^^^ squotes (Sym.pp id) in
     let descr =
       if logical then
@@ -293,7 +281,7 @@ let pp_message te =
         None
     in
     { short; descr; state = None }
-  | Unknown_logical_function { id; resource } ->
+  | Global (Unknown_logical_function { id; resource }) ->
     let short = !^"Unknown logical function" ^^^ squotes (Sym.pp id) in
     let descr =
       if resource then
@@ -302,13 +290,13 @@ let pp_message te =
         None
     in
     { short; descr; state = None }
+  | Global (Unknown_lemma sym) ->
+    let short = !^"Unknown lemma" ^^^ squotes (Sym.pp sym) in
+    { short; descr = None; state = None }
   | Unexpected_member (expected, member) ->
     let short = !^"Unexpected member" ^^^ Id.pp member in
     let descr = !^"the struct only has members" ^^^ list Id.pp expected in
     { short; descr = Some descr; state = None }
-  | Unknown_lemma sym ->
-    let short = !^"Unknown lemma" ^^^ squotes (Sym.pp sym) in
-    { short; descr = None; state = None }
   | First_iarg_missing ->
     let short = !^"Missing pointer input argument" in
     let descr = !^"a predicate definition must have at least one input argument" in

backend/cn/lib/typeErrors.mli

@@ -50,21 +50,9 @@ module RequestChain : sig
 end
 
 type message =
-  | Unknown_variable of Sym.t
-  | Unknown_function of Sym.t
-  | Unknown_struct of Sym.t
-  | Unknown_datatype of Sym.t
-  | Unknown_datatype_constr of Sym.t
-  | Unknown_resource_predicate of
-      { id : Sym.t;
-        logical : bool
-      }
-  | Unknown_logical_function of
-      { id : Sym.t;
-        resource : bool
-      }
+  | Global of Global.error
   | Unexpected_member of Id.t list * Id.t
-  | Unknown_lemma of Sym.t
+  | Unknown_variable of Sym.t
   | First_iarg_missing
   | First_iarg_not_pointer of
       { pname : Request.name;

backend/cn/lib/typing.ml

@@ -210,15 +210,17 @@ module ErrorReader = struct
 
   let bind = bind
 
-  type state = s
+  let get_global () =
+    let@ s = get () in
+    return s.typing_context.global
 
-  type global = Global.t
 
-  let get = get
+  let fail loc msg = fail (fun _ -> { loc; msg = Global msg })
 
-  let to_global (s : s) = s.typing_context.global
+  let get_context () =
+    let@ s = get () in
+    return s.typing_context
 
-  let to_context (s : s) = s.typing_context
 
   let lift = lift
 end
@@ -230,63 +232,12 @@ module Global = struct
 
   let is_fun_decl global id = Option.is_some @@ Global.get_fun_decl global id
 
-  let get_logical_function_def_opt id = get_logical_function_def id
-
-  let error_if_none opt loc msg =
-    let@ opt in
-    Option.fold
-      opt
-      ~some:return
-      ~none:
-        (let@ msg in
-         fail (fun _ -> { loc; msg }))
-
-
-  let get_logical_function_def loc id =
-    error_if_none
-      (get_logical_function_def id)
-      loc
-      (let@ res = get_resource_predicate_def id in
-       return (TypeErrors.Unknown_logical_function { id; resource = Option.is_some res }))
-
-
-  let get_struct_decl loc tag =
-    error_if_none (get_struct_decl tag) loc (return (TypeErrors.Unknown_struct tag))
-
-
-  let get_datatype loc tag =
-    error_if_none (get_datatype tag) loc (return (TypeErrors.Unknown_datatype tag))
-
-
-  let get_datatype_constr loc tag =
-    error_if_none
-      (get_datatype_constr tag)
-      loc
-      (return (TypeErrors.Unknown_datatype_constr tag))
-
-
   let get_struct_member_type loc tag member =
     let@ decl = get_struct_decl loc tag in
     let@ ty = get_member_type loc member decl in
     return ty
 
 
-  let get_fun_decl loc fsym =
-    error_if_none (get_fun_decl fsym) loc (return (TypeErrors.Unknown_function fsym))
-
-
-  let get_lemma loc lsym =
-    error_if_none (get_lemma lsym) loc (return (TypeErrors.Unknown_lemma lsym))
-
-
-  let get_resource_predicate_def loc id =
-    error_if_none
-      (get_resource_predicate_def id)
-      loc
-      (let@ log = get_logical_function_def_opt id in
-       return (TypeErrors.Unknown_resource_predicate { id; logical = Option.is_some log }))
-
-
   let get_fun_decls () =
     let@ global = get_global () in
     return (Sym.Map.bindings global.fun_decls)