From 8f89bd8df9f382284eabb5a2020a2fa634f92fac Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Tue, 12 Mar 2024 17:19:14 +0100
Subject: WIP: does not compile yet because we need to propagate the meta
 variable.

---
 compiler/Contexts.ml | 73 ++++++++++++++++++++++++++--------------------------
 1 file changed, 37 insertions(+), 36 deletions(-)

(limited to 'compiler/Contexts.ml')

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 2563bd9d..6cdae078 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -5,6 +5,7 @@ open LlbcAst
 open LlbcAstUtils
 open ValuesUtils
 open Identifiers
+open Errors
 module L = Logging
 
 (** The [Id] module for dummy variables.
@@ -285,7 +286,7 @@ let lookup_const_generic_var (ctx : eval_ctx) (vid : ConstGenericVarId.id) :
   ConstGenericVarId.nth ctx.const_generic_vars vid
 
 (** Lookup a variable in the current frame *)
-let env_lookup_var (env : env) (vid : VarId.id) : var_binder * typed_value =
+let env_lookup_var (meta : Meta.meta) (env : env) (vid : VarId.id) : var_binder * typed_value =
   (* We take care to stop at the end of current frame: different variables
      in different frames can have the same id!
   *)
@@ -296,12 +297,12 @@ let env_lookup_var (env : env) (vid : VarId.id) : var_binder * typed_value =
     | EBinding (BVar var, v) :: env' ->
         if var.index = vid then (var, v) else lookup env'
     | (EBinding (BDummy _, _) | EAbs _) :: env' -> lookup env'
-    | EFrame :: _ -> raise (Failure "End of frame")
+    | EFrame :: _ -> craise meta "End of frame"
   in
   lookup env
 
-let ctx_lookup_var_binder (ctx : eval_ctx) (vid : VarId.id) : var_binder =
-  fst (env_lookup_var ctx.env vid)
+let ctx_lookup_var_binder (meta : Meta.meta) (ctx : eval_ctx) (vid : VarId.id) : var_binder =
+  fst (env_lookup_var meta ctx.env vid)
 
 let ctx_lookup_type_decl (ctx : eval_ctx) (tid : TypeDeclId.id) : type_decl =
   TypeDeclId.Map.find tid ctx.type_ctx.type_decls
@@ -320,12 +321,12 @@ let ctx_lookup_trait_impl (ctx : eval_ctx) (id : TraitImplId.id) : trait_impl =
   TraitImplId.Map.find id ctx.trait_impls_ctx.trait_impls
 
 (** Retrieve a variable's value in the current frame *)
-let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value =
-  snd (env_lookup_var env vid)
+let env_lookup_var_value (meta : Meta.meta) (env : env) (vid : VarId.id) : typed_value =
+  snd (env_lookup_var meta env vid)
 
 (** Retrieve a variable's value in an evaluation context *)
-let ctx_lookup_var_value (ctx : eval_ctx) (vid : VarId.id) : typed_value =
-  env_lookup_var_value ctx.env vid
+let ctx_lookup_var_value (meta : Meta.meta) (ctx : eval_ctx) (vid : VarId.id) : typed_value =
+  env_lookup_var_value meta ctx.env vid
 
 (** Retrieve a const generic value in an evaluation context *)
 let ctx_lookup_const_generic_value (ctx : eval_ctx) (vid : ConstGenericVarId.id)
@@ -337,18 +338,18 @@ let ctx_lookup_const_generic_value (ctx : eval_ctx) (vid : ConstGenericVarId.id)
     This is a helper function: it can break invariants and doesn't perform
     any check.
 *)
-let env_update_var_value (env : env) (vid : VarId.id) (nv : typed_value) : env =
+let env_update_var_value (meta : Meta.meta) (env : env) (vid : VarId.id) (nv : typed_value) : env =
   (* We take care to stop at the end of current frame: different variables
      in different frames can have the same id!
   *)
   let rec update env =
     match env with
-    | [] -> raise (Failure "Unexpected")
+    | [] -> craise meta "Unexpected"
     | EBinding ((BVar b as var), v) :: env' ->
         if b.index = vid then EBinding (var, nv) :: env'
         else EBinding (var, v) :: update env'
     | ((EBinding (BDummy _, _) | EAbs _) as ee) :: env' -> ee :: update env'
-    | EFrame :: _ -> raise (Failure "End of frame")
+    | EFrame :: _ -> craise meta "End of frame"
   in
   update env
 
@@ -360,17 +361,17 @@ let var_to_binder (var : var) : var_binder =
     This is a helper function: it can break invariants and doesn't perform
     any check.
 *)
-let ctx_update_var_value (ctx : eval_ctx) (vid : VarId.id) (nv : typed_value) :
+let ctx_update_var_value (meta : Meta.meta) (ctx : eval_ctx) (vid : VarId.id) (nv : typed_value) :
     eval_ctx =
-  { ctx with env = env_update_var_value ctx.env vid nv }
+  { ctx with env = env_update_var_value meta ctx.env vid nv }
 
 (** Push a variable in the context's environment.
 
     Checks that the pushed variable and its value have the same type (this
     is important).
 *)
-let ctx_push_var (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
-  assert (TypesUtils.ty_is_ety var.var_ty && var.var_ty = v.ty);
+let ctx_push_var (meta : Meta.meta) (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
+  cassert (TypesUtils.ty_is_ety var.var_ty && var.var_ty = v.ty) meta "Pushed variables and their values do not have the same type TODO: Error message";
   let bv = var_to_binder var in
   { ctx with env = EBinding (BVar bv, v) :: ctx.env }
 
@@ -379,7 +380,7 @@ let ctx_push_var (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
     Checks that the pushed variables and their values have the same type (this
     is important).
 *)
-let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
+let ctx_push_vars (meta : Meta.meta) (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
     =
   log#ldebug
     (lazy
@@ -390,11 +391,11 @@ let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
                (* We can unfortunately not use Print because it depends on Contexts... *)
                show_var var ^ " -> " ^ show_typed_value value)
              vars)));
-  assert (
+  cassert (
     List.for_all
       (fun (var, (value : typed_value)) ->
         TypesUtils.ty_is_ety var.var_ty && var.var_ty = value.ty)
-      vars);
+      vars) meta "Pushed variables and their values do not have the same type TODO: Error message";
   let vars =
     List.map
       (fun (var, value) -> EBinding (BVar (var_to_binder var), value))
@@ -416,11 +417,11 @@ let ctx_push_fresh_dummy_vars (ctx : eval_ctx) (vl : typed_value list) :
   List.fold_left (fun ctx v -> ctx_push_fresh_dummy_var ctx v) ctx vl
 
 (** Remove a dummy variable from a context's environment. *)
-let ctx_remove_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) :
+let ctx_remove_dummy_var meta (ctx : eval_ctx) (vid : DummyVarId.id) :
     eval_ctx * typed_value =
   let rec remove_var (env : env) : env * typed_value =
     match env with
-    | [] -> raise (Failure "Could not lookup a dummy variable")
+    | [] -> craise meta "Could not lookup a dummy variable"
     | EBinding (BDummy vid', v) :: env when vid' = vid -> (env, v)
     | ee :: env ->
         let env, v = remove_var env in
@@ -430,10 +431,10 @@ let ctx_remove_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) :
   ({ ctx with env }, v)
 
 (** Lookup a dummy variable in a context's environment. *)
-let ctx_lookup_dummy_var (ctx : eval_ctx) (vid : DummyVarId.id) : typed_value =
+let ctx_lookup_dummy_var (meta : Meta.meta) (ctx : eval_ctx) (vid : DummyVarId.id) : typed_value =
   let rec lookup_var (env : env) : typed_value =
     match env with
-    | [] -> raise (Failure "Could not lookup a dummy variable")
+    | [] -> craise meta "Could not lookup a dummy variable"
     | EBinding (BDummy vid', v) :: _env when vid' = vid -> v
     | _ :: env -> lookup_var env
   in
@@ -449,13 +450,13 @@ let erase_regions (ty : ty) : ty =
   v#visit_ty () ty
 
 (** Push an uninitialized variable (which thus maps to {!constructor:Values.value.VBottom}) *)
-let ctx_push_uninitialized_var (ctx : eval_ctx) (var : var) : eval_ctx =
-  ctx_push_var ctx var (mk_bottom (erase_regions var.var_ty))
+let ctx_push_uninitialized_var (meta : Meta.meta) (ctx : eval_ctx) (var : var) : eval_ctx =
+  ctx_push_var meta ctx var (mk_bottom (erase_regions var.var_ty))
 
 (** Push a list of uninitialized variables (which thus map to {!constructor:Values.value.VBottom}) *)
-let ctx_push_uninitialized_vars (ctx : eval_ctx) (vars : var list) : eval_ctx =
+let ctx_push_uninitialized_vars (meta : Meta.meta) (ctx : eval_ctx) (vars : var list) : eval_ctx =
   let vars = List.map (fun v -> (v, mk_bottom (erase_regions v.var_ty))) vars in
-  ctx_push_vars ctx vars
+  ctx_push_vars meta ctx vars
 
 let env_find_abs (env : env) (pred : abs -> bool) : abs option =
   let rec lookup env =
@@ -474,10 +475,10 @@ let env_lookup_abs_opt (env : env) (abs_id : AbstractionId.id) : abs option =
     this abstraction (for instance, remove the abs id from all the parent sets
     of all the other abstractions).
  *)
-let env_remove_abs (env : env) (abs_id : AbstractionId.id) : env * abs option =
+let env_remove_abs (meta : Meta.meta) (env : env) (abs_id : AbstractionId.id) : env * abs option =
   let rec remove (env : env) : env * abs option =
     match env with
-    | [] -> raise (Failure "Unreachable")
+    | [] -> craise meta "Unreachable"
     | EFrame :: _ -> (env, None)
     | EBinding (bv, v) :: env ->
         let env, abs_opt = remove env in
@@ -499,11 +500,11 @@ let env_remove_abs (env : env) (abs_id : AbstractionId.id) : env * abs option =
     we also substitute the abstraction id wherever it is used (i.e., in the
     parent sets of the other abstractions).
  *)
-let env_subst_abs (env : env) (abs_id : AbstractionId.id) (nabs : abs) :
+let env_subst_abs (meta : Meta.meta) (env : env) (abs_id : AbstractionId.id) (nabs : abs) :
     env * abs option =
   let rec update (env : env) : env * abs option =
     match env with
-    | [] -> raise (Failure "Unreachable")
+    | [] -> craise meta "Unreachable"
     | EFrame :: _ -> (* We're done *) (env, None)
     | EBinding (bv, v) :: env ->
         let env, opt_abs = update env in
@@ -535,22 +536,22 @@ let ctx_find_abs (ctx : eval_ctx) (p : abs -> bool) : abs option =
   env_find_abs ctx.env p
 
 (** See the comments for {!env_remove_abs} *)
-let ctx_remove_abs (ctx : eval_ctx) (abs_id : AbstractionId.id) :
+let ctx_remove_abs (meta : Meta.meta) (ctx : eval_ctx) (abs_id : AbstractionId.id) :
     eval_ctx * abs option =
-  let env, abs = env_remove_abs ctx.env abs_id in
+  let env, abs = env_remove_abs meta ctx.env abs_id in
   ({ ctx with env }, abs)
 
 (** See the comments for {!env_subst_abs} *)
-let ctx_subst_abs (ctx : eval_ctx) (abs_id : AbstractionId.id) (nabs : abs) :
+let ctx_subst_abs (meta : Meta.meta) (ctx : eval_ctx) (abs_id : AbstractionId.id) (nabs : abs) :
     eval_ctx * abs option =
-  let env, abs_opt = env_subst_abs ctx.env abs_id nabs in
+  let env, abs_opt = env_subst_abs meta ctx.env abs_id nabs in
   ({ ctx with env }, abs_opt)
 
-let ctx_set_abs_can_end (ctx : eval_ctx) (abs_id : AbstractionId.id)
+let ctx_set_abs_can_end (meta : Meta.meta) (ctx : eval_ctx) (abs_id : AbstractionId.id)
     (can_end : bool) : eval_ctx =
   let abs = ctx_lookup_abs ctx abs_id in
   let abs = { abs with can_end } in
-  fst (ctx_subst_abs ctx abs_id abs)
+  fst (ctx_subst_abs meta ctx abs_id abs)
 
 let ctx_type_decl_is_rec (ctx : eval_ctx) (id : TypeDeclId.id) : bool =
   let decl_group = TypeDeclId.Map.find id ctx.type_ctx.type_decls_groups in
-- 
cgit v1.2.3


From 5209cea7012cfa3b39a5a289e65e2ea5e166d730 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 21 Mar 2024 12:34:40 +0100
Subject: WIP: translate.ml and extract.ml do not compile. Some assert left to
 do and we need to see how translate_crate can give meta to the functions it
 calls

---
 compiler/Contexts.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'compiler/Contexts.ml')

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 6cdae078..558aaa4e 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -451,11 +451,11 @@ let erase_regions (ty : ty) : ty =
 
 (** Push an uninitialized variable (which thus maps to {!constructor:Values.value.VBottom}) *)
 let ctx_push_uninitialized_var (meta : Meta.meta) (ctx : eval_ctx) (var : var) : eval_ctx =
-  ctx_push_var meta ctx var (mk_bottom (erase_regions var.var_ty))
+  ctx_push_var meta ctx var (mk_bottom meta (erase_regions var.var_ty))
 
 (** Push a list of uninitialized variables (which thus map to {!constructor:Values.value.VBottom}) *)
 let ctx_push_uninitialized_vars (meta : Meta.meta) (ctx : eval_ctx) (vars : var list) : eval_ctx =
-  let vars = List.map (fun v -> (v, mk_bottom (erase_regions v.var_ty))) vars in
+  let vars = List.map (fun v -> (v, mk_bottom meta (erase_regions v.var_ty))) vars in
   ctx_push_vars meta ctx vars
 
 let env_find_abs (env : env) (pred : abs -> bool) : abs option =
-- 
cgit v1.2.3


From 5ad671a0960692af1c00609fa6864c6f44ca299c Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 28 Mar 2024 13:56:31 +0100
Subject: Should answer all comments, there are still some TODO: error message
 left

---
 compiler/Contexts.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'compiler/Contexts.ml')

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 558aaa4e..51392edf 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -371,7 +371,7 @@ let ctx_update_var_value (meta : Meta.meta) (ctx : eval_ctx) (vid : VarId.id) (n
     is important).
 *)
 let ctx_push_var (meta : Meta.meta) (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
-  cassert (TypesUtils.ty_is_ety var.var_ty && var.var_ty = v.ty) meta "Pushed variables and their values do not have the same type TODO: Error message";
+  cassert (TypesUtils.ty_is_ety var.var_ty && var.var_ty = v.ty) meta "The pushed variables and their values do not have the same type";
   let bv = var_to_binder var in
   { ctx with env = EBinding (BVar bv, v) :: ctx.env }
 
@@ -395,7 +395,7 @@ let ctx_push_vars (meta : Meta.meta) (ctx : eval_ctx) (vars : (var * typed_value
     List.for_all
       (fun (var, (value : typed_value)) ->
         TypesUtils.ty_is_ety var.var_ty && var.var_ty = value.ty)
-      vars) meta "Pushed variables and their values do not have the same type TODO: Error message";
+      vars) meta "The pushed variables and their values do not have the same type TODO: Error message";
   let vars =
     List.map
       (fun (var, value) -> EBinding (BVar (var_to_binder var), value))
-- 
cgit v1.2.3


From 64666edb3c10cd42e15937ac4038b83def630e35 Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Thu, 28 Mar 2024 17:14:27 +0100
Subject: formatting

---
 compiler/Contexts.ml | 75 ++++++++++++++++++++++++++++++++--------------------
 1 file changed, 46 insertions(+), 29 deletions(-)

(limited to 'compiler/Contexts.ml')

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index 51392edf..c2d6999a 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -286,7 +286,8 @@ let lookup_const_generic_var (ctx : eval_ctx) (vid : ConstGenericVarId.id) :
   ConstGenericVarId.nth ctx.const_generic_vars vid
 
 (** Lookup a variable in the current frame *)
-let env_lookup_var (meta : Meta.meta) (env : env) (vid : VarId.id) : var_binder * typed_value =
+let env_lookup_var (meta : Meta.meta) (env : env) (vid : VarId.id) :
+    var_binder * typed_value =
   (* We take care to stop at the end of current frame: different variables
      in different frames can have the same id!
   *)
@@ -301,7 +302,8 @@ let env_lookup_var (meta : Meta.meta) (env : env) (vid : VarId.id) : var_binder
   in
   lookup env
 
-let ctx_lookup_var_binder (meta : Meta.meta) (ctx : eval_ctx) (vid : VarId.id) : var_binder =
+let ctx_lookup_var_binder (meta : Meta.meta) (ctx : eval_ctx) (vid : VarId.id) :
+    var_binder =
   fst (env_lookup_var meta ctx.env vid)
 
 let ctx_lookup_type_decl (ctx : eval_ctx) (tid : TypeDeclId.id) : type_decl =
@@ -321,11 +323,13 @@ let ctx_lookup_trait_impl (ctx : eval_ctx) (id : TraitImplId.id) : trait_impl =
   TraitImplId.Map.find id ctx.trait_impls_ctx.trait_impls
 
 (** Retrieve a variable's value in the current frame *)
-let env_lookup_var_value (meta : Meta.meta) (env : env) (vid : VarId.id) : typed_value =
+let env_lookup_var_value (meta : Meta.meta) (env : env) (vid : VarId.id) :
+    typed_value =
   snd (env_lookup_var meta env vid)
 
 (** Retrieve a variable's value in an evaluation context *)
-let ctx_lookup_var_value (meta : Meta.meta) (ctx : eval_ctx) (vid : VarId.id) : typed_value =
+let ctx_lookup_var_value (meta : Meta.meta) (ctx : eval_ctx) (vid : VarId.id) :
+    typed_value =
   env_lookup_var_value meta ctx.env vid
 
 (** Retrieve a const generic value in an evaluation context *)
@@ -338,7 +342,8 @@ let ctx_lookup_const_generic_value (ctx : eval_ctx) (vid : ConstGenericVarId.id)
     This is a helper function: it can break invariants and doesn't perform
     any check.
 *)
-let env_update_var_value (meta : Meta.meta) (env : env) (vid : VarId.id) (nv : typed_value) : env =
+let env_update_var_value (meta : Meta.meta) (env : env) (vid : VarId.id)
+    (nv : typed_value) : env =
   (* We take care to stop at the end of current frame: different variables
      in different frames can have the same id!
   *)
@@ -361,8 +366,8 @@ let var_to_binder (var : var) : var_binder =
     This is a helper function: it can break invariants and doesn't perform
     any check.
 *)
-let ctx_update_var_value (meta : Meta.meta) (ctx : eval_ctx) (vid : VarId.id) (nv : typed_value) :
-    eval_ctx =
+let ctx_update_var_value (meta : Meta.meta) (ctx : eval_ctx) (vid : VarId.id)
+    (nv : typed_value) : eval_ctx =
   { ctx with env = env_update_var_value meta ctx.env vid nv }
 
 (** Push a variable in the context's environment.
@@ -370,8 +375,11 @@ let ctx_update_var_value (meta : Meta.meta) (ctx : eval_ctx) (vid : VarId.id) (n
     Checks that the pushed variable and its value have the same type (this
     is important).
 *)
-let ctx_push_var (meta : Meta.meta) (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx =
-  cassert (TypesUtils.ty_is_ety var.var_ty && var.var_ty = v.ty) meta "The pushed variables and their values do not have the same type";
+let ctx_push_var (meta : Meta.meta) (ctx : eval_ctx) (var : var)
+    (v : typed_value) : eval_ctx =
+  cassert
+    (TypesUtils.ty_is_ety var.var_ty && var.var_ty = v.ty)
+    meta "The pushed variables and their values do not have the same type";
   let bv = var_to_binder var in
   { ctx with env = EBinding (BVar bv, v) :: ctx.env }
 
@@ -380,8 +388,8 @@ let ctx_push_var (meta : Meta.meta) (ctx : eval_ctx) (var : var) (v : typed_valu
     Checks that the pushed variables and their values have the same type (this
     is important).
 *)
-let ctx_push_vars (meta : Meta.meta) (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx
-    =
+let ctx_push_vars (meta : Meta.meta) (ctx : eval_ctx)
+    (vars : (var * typed_value) list) : eval_ctx =
   log#ldebug
     (lazy
       ("push_vars:\n"
@@ -391,11 +399,14 @@ let ctx_push_vars (meta : Meta.meta) (ctx : eval_ctx) (vars : (var * typed_value
                (* We can unfortunately not use Print because it depends on Contexts... *)
                show_var var ^ " -> " ^ show_typed_value value)
              vars)));
-  cassert (
-    List.for_all
-      (fun (var, (value : typed_value)) ->
-        TypesUtils.ty_is_ety var.var_ty && var.var_ty = value.ty)
-      vars) meta "The pushed variables and their values do not have the same type TODO: Error message";
+  cassert
+    (List.for_all
+       (fun (var, (value : typed_value)) ->
+         TypesUtils.ty_is_ety var.var_ty && var.var_ty = value.ty)
+       vars)
+    meta
+    "The pushed variables and their values do not have the same type TODO: \
+     Error message";
   let vars =
     List.map
       (fun (var, value) -> EBinding (BVar (var_to_binder var), value))
@@ -431,7 +442,8 @@ let ctx_remove_dummy_var meta (ctx : eval_ctx) (vid : DummyVarId.id) :
   ({ ctx with env }, v)
 
 (** Lookup a dummy variable in a context's environment. *)
-let ctx_lookup_dummy_var (meta : Meta.meta) (ctx : eval_ctx) (vid : DummyVarId.id) : typed_value =
+let ctx_lookup_dummy_var (meta : Meta.meta) (ctx : eval_ctx)
+    (vid : DummyVarId.id) : typed_value =
   let rec lookup_var (env : env) : typed_value =
     match env with
     | [] -> craise meta "Could not lookup a dummy variable"
@@ -450,12 +462,16 @@ let erase_regions (ty : ty) : ty =
   v#visit_ty () ty
 
 (** Push an uninitialized variable (which thus maps to {!constructor:Values.value.VBottom}) *)
-let ctx_push_uninitialized_var (meta : Meta.meta) (ctx : eval_ctx) (var : var) : eval_ctx =
+let ctx_push_uninitialized_var (meta : Meta.meta) (ctx : eval_ctx) (var : var) :
+    eval_ctx =
   ctx_push_var meta ctx var (mk_bottom meta (erase_regions var.var_ty))
 
 (** Push a list of uninitialized variables (which thus map to {!constructor:Values.value.VBottom}) *)
-let ctx_push_uninitialized_vars (meta : Meta.meta) (ctx : eval_ctx) (vars : var list) : eval_ctx =
-  let vars = List.map (fun v -> (v, mk_bottom meta (erase_regions v.var_ty))) vars in
+let ctx_push_uninitialized_vars (meta : Meta.meta) (ctx : eval_ctx)
+    (vars : var list) : eval_ctx =
+  let vars =
+    List.map (fun v -> (v, mk_bottom meta (erase_regions v.var_ty))) vars
+  in
   ctx_push_vars meta ctx vars
 
 let env_find_abs (env : env) (pred : abs -> bool) : abs option =
@@ -475,7 +491,8 @@ let env_lookup_abs_opt (env : env) (abs_id : AbstractionId.id) : abs option =
     this abstraction (for instance, remove the abs id from all the parent sets
     of all the other abstractions).
  *)
-let env_remove_abs (meta : Meta.meta) (env : env) (abs_id : AbstractionId.id) : env * abs option =
+let env_remove_abs (meta : Meta.meta) (env : env) (abs_id : AbstractionId.id) :
+    env * abs option =
   let rec remove (env : env) : env * abs option =
     match env with
     | [] -> craise meta "Unreachable"
@@ -500,8 +517,8 @@ let env_remove_abs (meta : Meta.meta) (env : env) (abs_id : AbstractionId.id) :
     we also substitute the abstraction id wherever it is used (i.e., in the
     parent sets of the other abstractions).
  *)
-let env_subst_abs (meta : Meta.meta) (env : env) (abs_id : AbstractionId.id) (nabs : abs) :
-    env * abs option =
+let env_subst_abs (meta : Meta.meta) (env : env) (abs_id : AbstractionId.id)
+    (nabs : abs) : env * abs option =
   let rec update (env : env) : env * abs option =
     match env with
     | [] -> craise meta "Unreachable"
@@ -536,19 +553,19 @@ let ctx_find_abs (ctx : eval_ctx) (p : abs -> bool) : abs option =
   env_find_abs ctx.env p
 
 (** See the comments for {!env_remove_abs} *)
-let ctx_remove_abs (meta : Meta.meta) (ctx : eval_ctx) (abs_id : AbstractionId.id) :
-    eval_ctx * abs option =
+let ctx_remove_abs (meta : Meta.meta) (ctx : eval_ctx)
+    (abs_id : AbstractionId.id) : eval_ctx * abs option =
   let env, abs = env_remove_abs meta ctx.env abs_id in
   ({ ctx with env }, abs)
 
 (** See the comments for {!env_subst_abs} *)
-let ctx_subst_abs (meta : Meta.meta) (ctx : eval_ctx) (abs_id : AbstractionId.id) (nabs : abs) :
-    eval_ctx * abs option =
+let ctx_subst_abs (meta : Meta.meta) (ctx : eval_ctx)
+    (abs_id : AbstractionId.id) (nabs : abs) : eval_ctx * abs option =
   let env, abs_opt = env_subst_abs meta ctx.env abs_id nabs in
   ({ ctx with env }, abs_opt)
 
-let ctx_set_abs_can_end (meta : Meta.meta) (ctx : eval_ctx) (abs_id : AbstractionId.id)
-    (can_end : bool) : eval_ctx =
+let ctx_set_abs_can_end (meta : Meta.meta) (ctx : eval_ctx)
+    (abs_id : AbstractionId.id) (can_end : bool) : eval_ctx =
   let abs = ctx_lookup_abs ctx abs_id in
   let abs = { abs with can_end } in
   fst (ctx_subst_abs meta ctx abs_id abs)
-- 
cgit v1.2.3


From 786c54c01ea98580374638c0ed92d19dfae19b1f Mon Sep 17 00:00:00 2001
From: Escherichia
Date: Fri, 29 Mar 2024 13:21:08 +0100
Subject: added file and line arg to craise and cassert

---
 compiler/Contexts.ml | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'compiler/Contexts.ml')

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index c2d6999a..edda4260 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -298,7 +298,7 @@ let env_lookup_var (meta : Meta.meta) (env : env) (vid : VarId.id) :
     | EBinding (BVar var, v) :: env' ->
         if var.index = vid then (var, v) else lookup env'
     | (EBinding (BDummy _, _) | EAbs _) :: env' -> lookup env'
-    | EFrame :: _ -> craise meta "End of frame"
+    | EFrame :: _ -> craise __FILE__ __LINE__ meta "End of frame"
   in
   lookup env
 
@@ -349,12 +349,12 @@ let env_update_var_value (meta : Meta.meta) (env : env) (vid : VarId.id)
   *)
   let rec update env =
     match env with
-    | [] -> craise meta "Unexpected"
+    | [] -> craise __FILE__ __LINE__ meta "Unexpected"
     | EBinding ((BVar b as var), v) :: env' ->
         if b.index = vid then EBinding (var, nv) :: env'
         else EBinding (var, v) :: update env'
     | ((EBinding (BDummy _, _) | EAbs _) as ee) :: env' -> ee :: update env'
-    | EFrame :: _ -> craise meta "End of frame"
+    | EFrame :: _ -> craise __FILE__ __LINE__ meta "End of frame"
   in
   update env
 
@@ -377,7 +377,7 @@ let ctx_update_var_value (meta : Meta.meta) (ctx : eval_ctx) (vid : VarId.id)
 *)
 let ctx_push_var (meta : Meta.meta) (ctx : eval_ctx) (var : var)
     (v : typed_value) : eval_ctx =
-  cassert
+  cassert __FILE__ __LINE__
     (TypesUtils.ty_is_ety var.var_ty && var.var_ty = v.ty)
     meta "The pushed variables and their values do not have the same type";
   let bv = var_to_binder var in
@@ -399,7 +399,7 @@ let ctx_push_vars (meta : Meta.meta) (ctx : eval_ctx)
                (* We can unfortunately not use Print because it depends on Contexts... *)
                show_var var ^ " -> " ^ show_typed_value value)
              vars)));
-  cassert
+  cassert __FILE__ __LINE__
     (List.for_all
        (fun (var, (value : typed_value)) ->
          TypesUtils.ty_is_ety var.var_ty && var.var_ty = value.ty)
@@ -432,7 +432,7 @@ let ctx_remove_dummy_var meta (ctx : eval_ctx) (vid : DummyVarId.id) :
     eval_ctx * typed_value =
   let rec remove_var (env : env) : env * typed_value =
     match env with
-    | [] -> craise meta "Could not lookup a dummy variable"
+    | [] -> craise __FILE__ __LINE__ meta "Could not lookup a dummy variable"
     | EBinding (BDummy vid', v) :: env when vid' = vid -> (env, v)
     | ee :: env ->
         let env, v = remove_var env in
@@ -446,7 +446,7 @@ let ctx_lookup_dummy_var (meta : Meta.meta) (ctx : eval_ctx)
     (vid : DummyVarId.id) : typed_value =
   let rec lookup_var (env : env) : typed_value =
     match env with
-    | [] -> craise meta "Could not lookup a dummy variable"
+    | [] -> craise __FILE__ __LINE__ meta "Could not lookup a dummy variable"
     | EBinding (BDummy vid', v) :: _env when vid' = vid -> v
     | _ :: env -> lookup_var env
   in
@@ -495,7 +495,7 @@ let env_remove_abs (meta : Meta.meta) (env : env) (abs_id : AbstractionId.id) :
     env * abs option =
   let rec remove (env : env) : env * abs option =
     match env with
-    | [] -> craise meta "Unreachable"
+    | [] -> craise __FILE__ __LINE__ meta "Unreachable"
     | EFrame :: _ -> (env, None)
     | EBinding (bv, v) :: env ->
         let env, abs_opt = remove env in
@@ -521,7 +521,7 @@ let env_subst_abs (meta : Meta.meta) (env : env) (abs_id : AbstractionId.id)
     (nabs : abs) : env * abs option =
   let rec update (env : env) : env * abs option =
     match env with
-    | [] -> craise meta "Unreachable"
+    | [] -> craise __FILE__ __LINE__ meta "Unreachable"
     | EFrame :: _ -> (* We're done *) (env, None)
     | EBinding (bv, v) :: env ->
         let env, opt_abs = update env in
-- 
cgit v1.2.3


From 16bebef339ee390b77e5b5505126aba74019a8f8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 29 Mar 2024 16:23:03 +0100
Subject: Add an error message

---
 compiler/Contexts.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'compiler/Contexts.ml')

diff --git a/compiler/Contexts.ml b/compiler/Contexts.ml
index edda4260..0a62f5ef 100644
--- a/compiler/Contexts.ml
+++ b/compiler/Contexts.ml
@@ -404,9 +404,7 @@ let ctx_push_vars (meta : Meta.meta) (ctx : eval_ctx)
        (fun (var, (value : typed_value)) ->
          TypesUtils.ty_is_ety var.var_ty && var.var_ty = value.ty)
        vars)
-    meta
-    "The pushed variables and their values do not have the same type TODO: \
-     Error message";
+    meta "The pushed variables and their values do not have the same type";
   let vars =
     List.map
       (fun (var, value) -> EBinding (BVar (var_to_binder var), value))
-- 
cgit v1.2.3