From 3f189e83f72b9ea570a29f85e77e94c1f662fa21 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 29 Apr 2022 16:10:54 +0200 Subject: Make good progress updating the code --- src/PureUtils.ml | 22 ++++++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) (limited to 'src/PureUtils.ml') diff --git a/src/PureUtils.ml b/src/PureUtils.ml index c01dd5c9..21f39c0e 100644 --- a/src/PureUtils.ml +++ b/src/PureUtils.ml @@ -190,7 +190,7 @@ let is_var (e : texpression) : bool = match e.e with Local _ -> true | _ -> false let as_var (e : texpression) : VarId.id = - match e.e with Local (v, _) -> v | _ -> raise (Failure "Unreachable") + match e.e with Local v -> v | _ -> raise (Failure "Unreachable") (** Remove the external occurrences of [Meta] *) let rec unmeta (e : texpression) : texpression = @@ -328,8 +328,8 @@ let unit_rvalue : texpression = let ty = unit_ty in { e; ty } -let mk_texpression_from_var (v : var) (mp : mplace option) : texpression = - let e = Local (v.id, mp) in +let mk_texpression_from_var (v : var) : texpression = + let e = Local v.id in let ty = v.ty in { e; ty } @@ -338,6 +338,18 @@ let mk_typed_lvalue_from_var (v : var) (mp : mplace option) : typed_lvalue = let ty = v.ty in { value; ty } +let mk_meta (m : meta) (e : texpression) : texpression = + let ty = e.ty in + let e = Meta (m, e) in + { e; ty } + +let mk_mplace_texpression (mp : mplace) (e : texpression) : texpression = + mk_meta (MPlace mp) e + +let mk_opt_mplace_texpression (mp : mplace option) (e : texpression) : + texpression = + match mp with None -> e | Some mp -> mk_mplace_texpression mp e + (** Make a "simplified" tuple value from a list of values: - if there is exactly one value, just return it - if there is > one value: wrap them in a tuple @@ -383,6 +395,7 @@ let mk_state_ty : ty = Adt (Assumed State, []) let mk_result_ty (ty : ty) : ty = Adt (Assumed Result, [ ty ]) +(* TODO: rename *) let mk_result_fail_rvalue (ty : ty) : texpression = let type_args = [ ty ] in let ty = Adt (Assumed Result, type_args) in @@ -395,6 +408,7 @@ let mk_result_fail_rvalue (ty : ty) : texpression = let cons = { e = cons_e; ty = cons_ty } in cons +(* TODO: rename *) let mk_result_return_rvalue (v : texpression) : texpression = let type_args = [ v.ty ] in let ty = Adt (Assumed Result, type_args) in @@ -529,7 +543,7 @@ module TypeCheck = struct let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit = match e.e with - | Local (var_id, _) -> ( + | Local var_id -> ( (* Lookup the variable - note that the variable may not be there, * if we type-check a subexpression (i.e.: if the variable is introduced * "outside" of the expression) - TODO: this won't happen once -- cgit v1.2.3