diff options
author | Son Ho | 2021-11-24 10:52:45 +0100 |
---|---|---|
committer | Son Ho | 2021-11-24 10:52:45 +0100 |
commit | bd93cad791d8191b47f4152461668ffcfbe38e27 (patch) | |
tree | 12d15770c75d6f7629bf6a7acae71c8afb2cddec /src/Contexts.ml | |
parent | ed8bbfc8a0cdc8474c41e16438fd80e6c491e6e2 (diff) |
Start refactoring the code
Diffstat (limited to '')
-rw-r--r-- | src/Contexts.ml | 33 |
1 files changed, 30 insertions, 3 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index 77dd9c49..1f7d28a4 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -45,15 +45,42 @@ let fresh_borrow_id (ctx : eval_ctx) : eval_ctx * BorrowId.id = let lookup_type_var (ctx : eval_ctx) (vid : TypeVarId.id) : type_var = TypeVarId.nth ctx.type_vars vid -let lookup_var (ctx : eval_ctx) (vid : VarId.id) : var = +let ctx_lookup_var (ctx : eval_ctx) (vid : VarId.id) : var = VarId.Map.find vid ctx.vars -let lookup_var_value (ctx : eval_ctx) (vid : VarId.id) : typed_value = +(** Retrieve a variable's value in an environment *) +let env_lookup_var_value (env : env) (vid : VarId.id) : typed_value = let check_ev (ev : env_value) : typed_value option = match ev with | Var (vid', v) -> if vid' = vid then Some v else None | Abs _ -> None in - match List.find_map check_ev ctx.env with + match List.find_map check_ev env with | None -> failwith "Unreachable" | Some v -> v + +(** 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 + +(** Update a variable's value in an environment + + 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 update_ev (ev : env_value) : env_value = + match ev with + | Var (vid', v) -> if vid' = vid then Var (vid, nv) else Var (vid', v) + | Abs abs -> Abs abs + in + List.map update_ev env + +(** Update a variable's value in an evaluation context. + + 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) : + eval_ctx = + { ctx with env = env_update_var_value ctx.env vid nv } |