CN: Add TypeError interface file

rems-project · Dec 26, 2024 · c90405f · c90405f
1 parent 74d48c6
commit c90405f
Show file tree

Hide file tree

Showing 12 changed files with 365 additions and 116 deletions.
diff --git a/backend/cn/bin/main.ml b/backend/cn/bin/main.ml
@@ -479,7 +479,7 @@ let run_tests
   Pp.print_level := print_level;
   Check.skip_and_only := (opt_comma_split skip, opt_comma_split only);
   Sym.executable_spec_enabled := true;
-  let handle_error (e : TypeErrors.type_error) =
+  let handle_error (e : TypeErrors.t) =
     let report = TypeErrors.pp_message e.msg in
     Pp.error e.loc report.short (Option.to_list report.descr);
     match e.msg with TypeErrors.Unsupported _ -> exit 2 | _ -> exit 1

diff --git a/backend/cn/lib/builtins.ml b/backend/cn/lib/builtins.ml
@@ -1,9 +1,5 @@
 module SBT = BaseTypes.Surface
 open Resultat
-
-open Effectful.Make (Resultat)
-
-open TypeErrors
 open IndexTerms
 
 (* builtin function symbols *)
@@ -51,7 +47,7 @@ let min_bits_def (sign, n) =
   let name = "MIN" ^ letter ^ Int.to_string n in
   ( name,
     Sym.fresh_named name,
-    mk_arg0 (fun loc -> IT.Surface.inj @@ num_lit_ num (BT.Bits (sign, n)) loc) )
+    mk_arg0 (fun loc -> Surface.inj @@ num_lit_ num (BT.Bits (sign, n)) loc) )
 
 
 let max_bits_def (sign, n) =
@@ -63,7 +59,7 @@ let max_bits_def (sign, n) =
   let name = "MAX" ^ letter ^ Int.to_string n in
   ( name,
     Sym.fresh_named name,
-    mk_arg0 (fun loc -> IT.Surface.inj @@ num_lit_ num (BT.Bits (sign, n)) loc) )
+    mk_arg0 (fun loc -> Surface.inj @@ num_lit_ num (BT.Bits (sign, n)) loc) )
 
 
 let mul_uf_def = ("mul_uf", Sym.fresh_named "mul_uf", mk_arg2 mul_no_smt_)
@@ -122,53 +118,49 @@ let array_to_list_def =
   ( "array_to_list",
     Sym.fresh_named "array_to_list",
     mk_arg3_err (fun (arr, i, len) loc ->
-      match SBT.is_map_bt (IT.get_bt arr) with
+      match SBT.is_map_bt (get_bt arr) with
       | None ->
         let reason = "map/array operation" in
         let expected = "map/array" in
         fail
           { loc;
-            msg =
-              Illtyped_it
-                { it = IT.pp arr; has = SBT.pp (IT.get_bt arr); expected; reason }
+            msg = Illtyped_it { it = pp arr; has = SBT.pp (get_bt arr); expected; reason }
           }
       | Some (_, bt) -> return (array_to_list_ (arr, i, len) bt loc)) )
 
 
 let is_null_def =
   ( "is_null",
     Sym.fresh_named "is_null",
-    mk_arg1 IT.(fun p loc -> Surface.inj (eq_ (Surface.proj p, null_ loc) loc)) )
+    mk_arg1 (fun p loc -> Surface.inj (eq_ (Surface.proj p, null_ loc) loc)) )
 
 
 let has_alloc_id_def =
   ( "has_alloc_id",
     Sym.fresh_named "has_alloc_id",
-    mk_arg1 IT.(fun p loc -> Surface.inj @@ hasAllocId_ (Surface.proj p) loc) )
+    mk_arg1 (fun p loc -> Surface.inj @@ hasAllocId_ (Surface.proj p) loc) )
 
 
 let ptr_eq_def =
   ( "ptr_eq",
     Sym.fresh_named "ptr_eq",
     mk_arg2 (fun (p1, p2) loc ->
-      IT.(Surface.inj @@ eq_ (Surface.proj p1, Surface.proj p2) loc)) )
+      Surface.inj @@ eq_ (Surface.proj p1, Surface.proj p2) loc) )
 
 
 let prov_eq_def =
   ( "prov_eq",
     Sym.fresh_named "prov_eq",
     mk_arg2 (fun (p1, p2) loc ->
-      IT.(
-        Surface.inj
-        @@ eq_ (allocId_ (Surface.proj p1) loc, allocId_ (Surface.proj p2) loc) loc)) )
+      Surface.inj
+      @@ eq_ (allocId_ (Surface.proj p1) loc, allocId_ (Surface.proj p2) loc) loc) )
 
 
 let addr_eq_def =
   ( "addr_eq",
     Sym.fresh_named "addr_eq",
     mk_arg2 (fun (p1, p2) loc ->
-      IT.(
-        Surface.inj @@ eq_ (addr_ (Surface.proj p1) loc, addr_ (Surface.proj p2) loc) loc))
+      Surface.inj @@ eq_ (addr_ (Surface.proj p1) loc, addr_ (Surface.proj p2) loc) loc)
   )
 
 

diff --git a/backend/cn/lib/check.ml b/backend/cn/lib/check.ml
@@ -2,6 +2,7 @@ module CF = Cerb_frontend
 module IT = IndexTerms
 module BT = BaseTypes
 module LRT = LogicalReturnTypes
+module Req = Request
 module RT = ReturnTypes
 module AT = ArgumentTypes
 module LAT = LogicalArgumentTypes
@@ -1008,7 +1009,7 @@ module Spine : sig
   val calltype_lt
     :  Loc.t ->
     BT.t Mu.pexpr list ->
-    AT.lt * label_kind ->
+    AT.lt * Where.label ->
     (False.t -> unit m) ->
     unit m
 

diff --git a/backend/cn/lib/compile.ml b/backend/cn/lib/compile.ml
@@ -375,11 +375,14 @@ module E = struct
   type 'a m =
     | Done of 'a
     | Error of TypeErrors.t
-    | ScopeExists of Loc.t * evaluation_scope * (bool -> 'a m)
+    | ScopeExists of Locations.t * evaluation_scope * (bool -> 'a m)
     | Value_of_c_variable of
-        Loc.t * Sym.t * evaluation_scope option * (IT.Surface.t option -> 'a m)
+        Locations.t * Sym.t * evaluation_scope option * (IT.Surface.t option -> 'a m)
     | Deref of
-        Loc.t * IT.Surface.t * evaluation_scope option * (IT.Surface.t option -> 'a m)
+        Locations.t
+        * IT.Surface.t
+        * evaluation_scope option
+        * (IT.Surface.t option -> 'a m)
 
   let return x = Done x
 

diff --git a/backend/cn/lib/lemmata.ml b/backend/cn/lib/lemmata.ml
@@ -32,7 +32,7 @@ module PrevDefs = struct
     { present : Sym.t list StringListMap.t;
       defs : Pp.document list IntMap.t;
       dt_params : (IT.t * Id.t * Sym.t) list;
-      failures : TypeErrors.type_error list
+      failures : TypeErrors.t list
     }
 
   let init_t =

diff --git a/backend/cn/lib/resourceInference.ml b/backend/cn/lib/resourceInference.ml
@@ -47,7 +47,7 @@ module General = struct
       value : IT.t
     }
 
-  type uiinfo = TypeErrors.situation * TypeErrors.request_chain
+  type uiinfo = TypeErrors.situation * TypeErrors.RequestChain.t
 
   type case =
     | One of one
@@ -105,7 +105,7 @@ module General = struct
       let resource = Simplify.Request.simp simp_ctxt resource in
       let situation, request_chain = uiinfo in
       let step =
-        TypeErrors.
+        TypeErrors.RequestChain.
           { resource; loc = Some (fst info); reason = Some ("arg " ^ Sym.pp_string s) }
       in
       let request_chain = step :: request_chain in
@@ -469,7 +469,7 @@ module Special = struct
 
   let predicate_request loc situation (request, oinfo) =
     let requests =
-      [ TypeErrors.
+      [ TypeErrors.RequestChain.
           { resource = P request;
             loc = Option.map fst oinfo;
             reason = Option.map snd oinfo
@@ -546,7 +546,7 @@ module Special = struct
 
   let qpredicate_request loc situation (request, oinfo) =
     let requests =
-      [ TypeErrors.
+      [ TypeErrors.RequestChain.
           { resource = Q request;
             loc = Option.map fst oinfo;
             reason = Option.map snd oinfo

diff --git a/backend/cn/lib/resourceInference.mli b/backend/cn/lib/resourceInference.mli
@@ -6,7 +6,7 @@ val debug_constraint_failure_diagnostics
   unit
 
 module General : sig
-  type uiinfo = TypeErrors.situation * TypeErrors.request_chain
+  type uiinfo = TypeErrors.situation * TypeErrors.RequestChain.t
 
   val ftyp_args_request_step
     :  ([ `Rename of Sym.t | `Term of IndexTerms.t ] Subst.t -> 'a -> 'a) ->