Merge pull request #95 from AeneasVerif/escherichia/errors

Escherichia/errors

1 files changed, 22 insertions, 17 deletions

diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index dbd310b7..177d8c24 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -7,6 +7,7 @@ open Types
 open Values
 open LlbcAst
 open Contexts
+open Errors
 
 (** Generate fresh regions for region variables.
 
@@ -67,25 +68,27 @@ let ctx_adt_get_instantiated_field_types (ctx : eval_ctx)
     **IMPORTANT**: this function doesn't normalize the types, you may want to
     use the [AssociatedTypes] equivalent instead.
  *)
-let ctx_adt_value_get_instantiated_field_types (ctx : eval_ctx)
-    (adt : adt_value) (id : type_id) (generics : generic_args) : ty list =
+let ctx_adt_value_get_instantiated_field_types (meta : Meta.meta)
+    (ctx : eval_ctx) (adt : adt_value) (id : type_id) (generics : generic_args)
+    : ty list =
   match id with
   | TAdtId id ->
       (* Retrieve the types of the fields *)
       ctx_adt_get_instantiated_field_types ctx id adt.variant_id generics
   | TTuple ->
-      assert (generics.regions = []);
+      cassert __FILE__ __LINE__ (generics.regions = []) meta
+        "Tuples don't have region parameters";
       generics.types
   | TAssumed aty -> (
       match aty with
       | TBox ->
-          assert (generics.regions = []);
-          assert (List.length generics.types = 1);
-          assert (generics.const_generics = []);
+          sanity_check __FILE__ __LINE__ (generics.regions = []) meta;
+          sanity_check __FILE__ __LINE__ (List.length generics.types = 1) meta;
+          sanity_check __FILE__ __LINE__ (generics.const_generics = []) meta;
           generics.types
       | TArray | TSlice | TStr ->
           (* Those types don't have fields *)
-          raise (Failure "Unreachable"))
+          craise __FILE__ __LINE__ meta "Unreachable")
 
 (** Substitute a function signature, together with the regions hierarchy
     associated to that signature.
@@ -144,30 +147,32 @@ let subst_ids_visitor (r_subst : RegionId.id -> RegionId.id)
     method! visit_abstraction_id _ id = asubst id
   end
 
-let typed_value_subst_ids (r_subst : RegionId.id -> RegionId.id)
+let typed_value_subst_ids (meta : Meta.meta)
+    (r_subst : RegionId.id -> RegionId.id)
     (ty_subst : TypeVarId.id -> TypeVarId.id)
     (cg_subst : ConstGenericVarId.id -> ConstGenericVarId.id)
     (ssubst : SymbolicValueId.id -> SymbolicValueId.id)
     (bsubst : BorrowId.id -> BorrowId.id) (v : typed_value) : typed_value =
-  let asubst _ = raise (Failure "Unreachable") in
+  let asubst _ = craise __FILE__ __LINE__ meta "Unreachable" in
   let vis = subst_ids_visitor r_subst ty_subst cg_subst ssubst bsubst asubst in
   vis#visit_typed_value () v
 
-let typed_value_subst_rids (r_subst : RegionId.id -> RegionId.id)
-    (v : typed_value) : typed_value =
-  typed_value_subst_ids r_subst
+let typed_value_subst_rids (meta : Meta.meta)
+    (r_subst : RegionId.id -> RegionId.id) (v : typed_value) : typed_value =
+  typed_value_subst_ids meta r_subst
     (fun x -> x)
     (fun x -> x)
     (fun x -> x)
     (fun x -> x)
     v
 
-let typed_avalue_subst_ids (r_subst : RegionId.id -> RegionId.id)
+let typed_avalue_subst_ids (meta : Meta.meta)
+    (r_subst : RegionId.id -> RegionId.id)
     (ty_subst : TypeVarId.id -> TypeVarId.id)
     (cg_subst : ConstGenericVarId.id -> ConstGenericVarId.id)
     (ssubst : SymbolicValueId.id -> SymbolicValueId.id)
     (bsubst : BorrowId.id -> BorrowId.id) (v : typed_avalue) : typed_avalue =
-  let asubst _ = raise (Failure "Unreachable") in
+  let asubst _ = craise __FILE__ __LINE__ meta "Unreachable" in
   let vis = subst_ids_visitor r_subst ty_subst cg_subst ssubst bsubst asubst in
   vis#visit_typed_avalue () v
 
@@ -189,9 +194,9 @@ let env_subst_ids (r_subst : RegionId.id -> RegionId.id)
   let vis = subst_ids_visitor r_subst ty_subst cg_subst ssubst bsubst asubst in
   vis#visit_env () x
 
-let typed_avalue_subst_rids (r_subst : RegionId.id -> RegionId.id)
-    (x : typed_avalue) : typed_avalue =
-  let asubst _ = raise (Failure "Unreachable") in
+let typed_avalue_subst_rids (meta : Meta.meta)
+    (r_subst : RegionId.id -> RegionId.id) (x : typed_avalue) : typed_avalue =
+  let asubst _ = craise __FILE__ __LINE__ meta "Unreachable" in
   let vis =
     subst_ids_visitor r_subst
       (fun x -> x)