diff options
Diffstat (limited to 'src/Contexts.ml')
| -rw-r--r-- | src/Contexts.ml | 45 |
1 files changed, 37 insertions, 8 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index 0fe3a09a..d8ea9a3f 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -55,7 +55,13 @@ type binder = { TODO: rename Var (-> Binding?) *) -type env_elem = Var of (binder[@opaque]) * typed_value | Abs of abs | Frame +type env_elem = + | Var of (binder option[@opaque]) * typed_value + (** Variable binding - the binder is None if the variable is a dummy variable + (we use dummy variables to store temporaries while doing bookkeeping such + as ending borrows for instance). *) + | Abs of abs + | Frame [@@deriving show, visitors @@ -115,13 +121,17 @@ type eval_ctx = { let lookup_type_var (ctx : eval_ctx) (vid : TypeVarId.id) : type_var = TypeVarId.nth ctx.type_vars vid +let opt_binder_has_vid (bv : binder option) (vid : VarId.id) : bool = + match bv with Some bv -> bv.index = vid | None -> false + let ctx_lookup_binder (ctx : eval_ctx) (vid : VarId.id) : binder = (* TOOD: we might want to stop at the end of the frame *) let rec lookup env = match env with | [] -> raise (Invalid_argument ("Variable not found: " ^ VarId.to_string vid)) - | Var (var, _) :: env' -> if var.index = vid then var else lookup env' + | Var (var, _) :: env' -> + if opt_binder_has_vid var vid then Option.get var else lookup env' | (Abs _ | Frame) :: env' -> lookup env' in lookup ctx.env @@ -140,7 +150,8 @@ let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value = let rec lookup env = match env with | [] -> failwith "Unexpected" - | Var (var, v) :: env' -> if var.index = vid then v else lookup env' + | Var (var, v) :: env' -> + if opt_binder_has_vid var vid then v else lookup env' | Abs _ :: env' -> lookup env' | Frame :: _ -> failwith "End of frame" in @@ -163,7 +174,7 @@ let env_update_var_value (env : env) (vid : VarId.id) (nv : typed_value) : env = match env with | [] -> failwith "Unexpected" | Var (var, v) :: env' -> - if var.index = vid then Var (var, nv) :: env' + if opt_binder_has_vid var vid then Var (var, nv) :: env' else Var (var, v) :: update env' | Abs abs :: env' -> Abs abs :: update env' | Frame :: _ -> failwith "End of frame" @@ -189,7 +200,7 @@ let ctx_update_var_value (ctx : eval_ctx) (vid : VarId.id) (nv : typed_value) : let ctx_push_var (ctx : eval_ctx) (var : var) (v : typed_value) : eval_ctx = assert (var.var_ty = v.ty); let bv = var_to_binder var in - { ctx with env = Var (bv, v) :: ctx.env } + { ctx with env = Var (Some bv, v) :: ctx.env } (** Push a list of variables. @@ -203,11 +214,29 @@ let ctx_push_vars (ctx : eval_ctx) (vars : (var * typed_value) list) : eval_ctx (fun (var, (value : typed_value)) -> var.var_ty = value.ty) vars); let vars = - List.map (fun (var, value) -> Var (var_to_binder var, value)) vars + List.map (fun (var, value) -> Var (Some (var_to_binder var), value)) vars in let vars = List.rev vars in { ctx with env = List.append vars ctx.env } +(** Push a dummy variable in the context's environment. *) +let ctx_push_dummy_var (ctx : eval_ctx) (v : typed_value) : eval_ctx = + { ctx with env = Var (None, v) :: ctx.env } + +(** Pop the first dummy variable from the context's environment. *) +let ctx_pop_dummy_var (ctx : eval_ctx) : eval_ctx * typed_value = + let rec pop_var (env : env) : env * typed_value = + match env with + | [] -> failwith "Could not find a dummy variable" + | Var (None, v) :: env -> (env, v) + | ee :: env -> + let env, v = pop_var env in + (ee :: env, v) + in + let env, v = pop_var ctx.env in + ({ ctx with env }, v) + +(* TODO: move *) let mk_bottom (ty : ety) : typed_value = { value = Bottom; ty } (** Push an uninitialized variable (which thus maps to [Bottom]) *) @@ -237,7 +266,7 @@ class ['self] iter_frame = object (self : 'self) inherit [_] V.iter_abs - method visit_Var : 'acc -> binder -> typed_value -> unit = + method visit_Var : 'acc -> binder option -> typed_value -> unit = fun acc _vid v -> self#visit_typed_value acc v method visit_Abs : 'acc -> abs -> unit = @@ -265,7 +294,7 @@ class ['self] map_frame_concrete = object (self : 'self) inherit [_] V.map_abs - method visit_Var : 'acc -> binder -> typed_value -> env_elem = + method visit_Var : 'acc -> binder option -> typed_value -> env_elem = fun acc vid v -> let v = self#visit_typed_value acc v in Var (vid, v) |