summaryrefslogtreecommitdiff
path: root/compiler/Contexts.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/Contexts.ml')
-rw-r--r--compiler/Contexts.ml75
1 files changed, 46 insertions, 29 deletions
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)