From b664a5b1e4814a1f0105b76d5b5265e095200c3d Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 1 May 2022 16:15:54 +0200 Subject: Cleanup --- src/ExtractToFStar.ml | 6 ++--- src/PrintPure.ml | 20 +++++++--------- src/Pure.ml | 64 +++++++------------------------------------------- src/PureMicroPasses.ml | 43 +++++++++++++++------------------ src/PureUtils.ml | 16 ++++++------- src/SymbolicToPure.ml | 4 +--- 6 files changed, 47 insertions(+), 106 deletions(-) (limited to 'src') diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 0bcf66bd..0a06ef73 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -817,14 +817,14 @@ let rec extract_typed_pattern (ctx : extraction_ctx) (fmt : F.formatter) | PatConcrete cv -> ctx.fmt.extract_constant_value fmt inside cv; ctx - | PatVar (Var (v, _)) -> + | PatVar (v, _) -> let vname = ctx.fmt.var_basename ctx.names_map.names_set v.basename v.ty in let ctx, vname = ctx_add_var vname v.id ctx in F.pp_print_string fmt vname; ctx - | PatVar Dummy -> + | PatDummy -> F.pp_print_string fmt "_"; ctx | PatAdt av -> @@ -845,7 +845,7 @@ let rec extract_typed_pattern (ctx : extraction_ctx) (fmt : F.formatter) let rec extract_texpression (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (e : texpression) : unit = match e.e with - | Local var_id -> + | Var var_id -> let var_name = ctx_get_var var_id ctx in F.pp_print_string fmt var_name | Const cv -> ctx.fmt.extract_constant_value fmt inside cv diff --git a/src/PrintPure.ml b/src/PrintPure.ml index 2da653bb..f21329ed 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -362,21 +362,17 @@ let adt_g_value_to_string (fmt : value_formatter) ^ "\n- ty: " ^ ty_to_string fmt ty ^ "\n- variant_id: " ^ Print.option_to_string VariantId.to_string variant_id)) -let var_or_dummy_to_string (fmt : ast_formatter) (v : var_or_dummy) : string = - match v with - | Var (v, None) -> var_to_string (ast_to_type_formatter fmt) v - | Var (v, Some mp) -> - let mp = "[@mplace=" ^ mplace_to_string fmt mp ^ "]" in - "(" ^ var_to_varname v ^ " " ^ mp ^ " : " - ^ ty_to_string (ast_to_type_formatter fmt) v.ty - ^ ")" - | Dummy -> "_" - let rec typed_pattern_to_string (fmt : ast_formatter) (v : typed_pattern) : string = match v.value with | PatConcrete cv -> Print.Values.constant_value_to_string cv - | PatVar var -> var_or_dummy_to_string fmt var + | PatVar (v, None) -> var_to_string (ast_to_type_formatter fmt) v + | PatVar (v, Some mp) -> + let mp = "[@mplace=" ^ mplace_to_string fmt mp ^ "]" in + "(" ^ var_to_varname v ^ " " ^ mp ^ " : " + ^ ty_to_string (ast_to_type_formatter fmt) v.ty + ^ ")" + | PatDummy -> "_" | PatAdt av -> adt_g_value_to_string (ast_to_value_formatter fmt) @@ -455,7 +451,7 @@ let fun_id_to_string (fmt : ast_formatter) (fun_id : fun_id) : string = let rec texpression_to_string (fmt : ast_formatter) (inside : bool) (indent : string) (indent_incr : string) (e : texpression) : string = match e.e with - | Local var_id -> + | Var var_id -> let s = fmt.var_id_to_string var_id in if inside then "(" ^ s ^ ")" else s | Const cv -> Print.Values.constant_value_to_string cv diff --git a/src/Pure.ml b/src/Pure.ml index 9cf7a077..e2362338 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -172,7 +172,7 @@ type mplace = { type variant_id = VariantId.id [@@deriving show] -(** Ancestor for [iter_var_or_dummy] visitor *) +(** Ancestor for [iter_pat_var_or_dummy] visitor *) class ['self] iter_value_base = object (_self : 'self) inherit [_] VisitorsRuntime.iter @@ -242,57 +242,13 @@ class virtual ['self] mapreduce_value_base = fun _ x -> (x, self#zero) end -type var_or_dummy = - | Var of var * mplace option - (** Rk.: the mdplace is actually always a variable (i.e.: there are no projections). - - We use [mplace] because it leads to a more uniform treatment of the meta - information. - *) - | Dummy (** Ignored value: `_`. *) -[@@deriving - show, - visitors - { - name = "iter_var_or_dummy"; - variety = "iter"; - ancestors = [ "iter_value_base" ]; - nude = true (* Don't inherit [VisitorsRuntime.iter] *); - concrete = true; - polymorphic = false; - }, - visitors - { - name = "map_var_or_dummy"; - variety = "map"; - ancestors = [ "map_value_base" ]; - nude = true (* Don't inherit [VisitorsRuntime.map] *); - concrete = true; - polymorphic = false; - }, - visitors - { - name = "reduce_var_or_dummy"; - variety = "reduce"; - ancestors = [ "reduce_value_base" ]; - nude = true (* Don't inherit [VisitorsRuntime.reduce] *); - polymorphic = false; - }, - visitors - { - name = "mapreduce_var_or_dummy"; - variety = "mapreduce"; - ancestors = [ "mapreduce_value_base" ]; - nude = true (* Don't inherit [VisitorsRuntime.reduce] *); - polymorphic = false; - }] - (** A pattern (which appears on the left of assignments, in matches, etc.). *) type pattern = | PatConcrete of constant_value (** [PatConcrete] is necessary because we merge the switches over integer values and the matches over enumerations *) - | PatVar of var_or_dummy + | PatVar of var * mplace option + | PatDummy (** Ignored value: `_`. *) | PatAdt of adt_pattern and adt_pattern = { @@ -307,7 +263,7 @@ and typed_pattern = { value : pattern; ty : ty } { name = "iter_typed_pattern"; variety = "iter"; - ancestors = [ "iter_var_or_dummy" ]; + ancestors = [ "iter_value_base" ]; nude = true (* Don't inherit [VisitorsRuntime.iter] *); concrete = true; polymorphic = false; @@ -316,7 +272,7 @@ and typed_pattern = { value : pattern; ty : ty } { name = "map_typed_pattern"; variety = "map"; - ancestors = [ "map_var_or_dummy" ]; + ancestors = [ "map_value_base" ]; nude = true (* Don't inherit [VisitorsRuntime.iter] *); concrete = true; polymorphic = false; @@ -325,7 +281,7 @@ and typed_pattern = { value : pattern; ty : ty } { name = "reduce_typed_pattern"; variety = "reduce"; - ancestors = [ "reduce_var_or_dummy" ]; + ancestors = [ "reduce_value_base" ]; nude = true (* Don't inherit [VisitorsRuntime.iter] *); polymorphic = false; }, @@ -333,7 +289,7 @@ and typed_pattern = { value : pattern; ty : ty } { name = "mapreduce_typed_pattern"; variety = "mapreduce"; - ancestors = [ "mapreduce_var_or_dummy" ]; + ancestors = [ "mapreduce_value_base" ]; nude = true (* Don't inherit [VisitorsRuntime.iter] *); polymorphic = false; }] @@ -439,11 +395,7 @@ class virtual ['self] mapreduce_expression_base = more general than the LLBC statements, in a sense. *) type expression = - | Local of var_id - (** Local variable - TODO: we name it "Local" because "Var" is used - in [var_or_dummy]: change the name. Maybe rename `Var` and `Dummy` - in `var_or_dummy` to `PatVar` and `PatDummy`. - *) + | Var of var_id (** a variable *) | Const of constant_value | App of texpression * texpression (** Application of a function to an argument. diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml index c84bf7cd..bd7d7766 100644 --- a/src/PureMicroPasses.ml +++ b/src/PureMicroPasses.ml @@ -95,7 +95,7 @@ let get_body_min_var_counter (body : fun_body) : VarId.generator = method! visit_var _ v _ = v.id (** For the patterns *) - method! visit_Local _ vid _ = vid + method! visit_Var _ vid _ = vid (** For the rvalues *) end in @@ -296,7 +296,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = object inherit [_] map_typed_pattern - method! visit_Var _ v mp = Var (update_var ctx v mp, mp) + method! visit_PatVar _ v mp = PatVar (update_var ctx v mp, mp) end in obj#visit_typed_pattern () lv @@ -350,7 +350,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = (* Register the place *) let ctx = register_mplace mp ctx in (* Add the constraint *) - match (unmeta rv).e with Local vid -> add_constraint mp vid ctx | _ -> ctx + match (unmeta rv).e with Var vid -> add_constraint mp vid ctx | _ -> ctx in (* Specific case of constraint on left values *) let add_left_constraint (lv : typed_pattern) (ctx : pn_ctx) : pn_ctx = @@ -362,7 +362,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = method plus ctx0 ctx1 _ = merge_ctxs (ctx0 ()) (ctx1 ()) - method! visit_Var _ v mp () = + method! visit_PatVar _ v mp () = (* Register the variable *) let ctx = register_var (self#zero ()) v in (* Register the mplace information if there is such information *) @@ -381,7 +381,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = (* We propagate constraints across variable reassignments: `^0 = x`, * if the destination doesn't have naming information *) match lv.value with - | PatVar (Var (({ id = _; basename = None; ty = _ } as lvar), lmp)) -> + | PatVar (({ id = _; basename = None; ty = _ } as lvar), lmp) -> if (* Check that there is not already a name for the variable *) VarId.Map.mem lvar.id ctx.pure_vars @@ -413,7 +413,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = (* We try to use the rvalue information, if it is a variable *) let ctx = match (unmeta re).e with - | Local rvar_id -> ( + | Var rvar_id -> ( match VarId.Map.find_opt rvar_id ctx.pure_vars with | None -> ctx | Some name -> add name ctx) @@ -429,7 +429,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = let ty = e.ty in let ctx, e = match e.e with - | Local _ -> (* Nothing to do *) (ctx, e.e) + | Var _ -> (* Nothing to do *) (ctx, e.e) | Const _ -> (* Nothing to do *) (ctx, e.e) | App (app, arg) -> let ctx, app = update_texpression app ctx in @@ -590,7 +590,7 @@ let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool) * - the left-value is a variable *) match (monadic, lv.value) with - | false, PatVar (Var (lv_var, _)) -> + | false, PatVar (lv_var, _) -> (* We can filter if: *) let filter = false in (* 1. Either: @@ -610,7 +610,7 @@ let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool) if inline_pure then let app, _ = destruct_apps re in match app.e with - | Const _ | Local _ -> true (* constant or variable *) + | Const _ | Var _ -> true (* constant or variable *) | Qualif qualif -> ( match qualif.id with | AdtCons _ | Proj _ -> true (* ADT constructor *) @@ -635,9 +635,9 @@ let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool) (** Visit the let-bindings to filter the useless ones (and update the substitution map while doing so *) - method! visit_Local (env : texpression VarId.Map.t) (vid : VarId.id) = + method! visit_Var (env : texpression VarId.Map.t) (vid : VarId.id) = match VarId.Map.find_opt vid env with - | None -> (* No substitution *) super#visit_Local env vid + | None -> (* No substitution *) super#visit_Var env vid | Some ne -> (* Substitute - note that we need to reexplore, because * there may be stacked substitutions, if we have: @@ -750,7 +750,7 @@ let expression_contains_child_call_in_all_paths (ctx : trans_ctx) method! visit_texpression env e = match e.e with - | Local _ | Const _ -> fun _ -> false + | Var _ | Const _ -> fun _ -> false | Let (_, _, re, e) -> ( match opt_destruct_function_call re with | None -> fun () -> self#visit_texpression env e () @@ -812,12 +812,9 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx) method plus b0 b1 _ = b0 () && b1 () - method! visit_var_or_dummy env v = - match v with - | Dummy -> (Dummy, fun _ -> true) - | Var (v, mp) -> - if VarId.Set.mem v.id env then (Var (v, mp), fun _ -> false) - else (Dummy, fun _ -> true) + method! visit_PatVar env v mp = + if VarId.Set.mem v.id env then (PatVar (v, mp), fun _ -> false) + else (PatDummy, fun _ -> true) end in let filter_typed_pattern (used_vars : VarId.Set.t) (lv : typed_pattern) : @@ -839,12 +836,12 @@ let filter_useless (filter_monadic_calls : bool) (ctx : trans_ctx) method plus s0 s1 _ = VarId.Set.union (s0 ()) (s1 ()) - method! visit_Local _ vid = (Local vid, fun _ -> VarId.Set.singleton vid) + method! visit_Var _ vid = (Var vid, fun _ -> VarId.Set.singleton vid) (** Whenever we visit a variable, we need to register the used variable *) method! visit_expression env e = match e with - | Local _ | Const _ | App _ | Qualif _ + | Var _ | Const _ | App _ | Qualif _ | Switch (_, _) | Meta (_, _) | Abs _ -> @@ -970,10 +967,8 @@ let unit_vars_to_unit (def : fun_decl) : fun_decl = object inherit [_] map_expression as super - method! visit_var_or_dummy _ v = - match v with - | Dummy -> Dummy - | Var (v, mp) -> if v.ty = unit_ty then Dummy else Var (v, mp) + method! visit_PatVar _ v mp = + if v.ty = unit_ty then PatDummy else PatVar (v, mp) (** Replace in patterns *) method! visit_texpression env e = diff --git a/src/PureUtils.ml b/src/PureUtils.ml index 96d84fb1..fe71b3b2 100644 --- a/src/PureUtils.ml +++ b/src/PureUtils.ml @@ -180,17 +180,17 @@ let functions_not_mutually_recursive (funs : fun_decl list) : bool = *) let rec let_group_requires_parentheses (e : texpression) : bool = match e.e with - | Local _ | Const _ | App _ | Abs _ | Qualif _ -> false + | Var _ | Const _ | App _ | Abs _ | Qualif _ -> false | Let (monadic, _, _, next_e) -> if monadic then true else let_group_requires_parentheses next_e | Switch (_, _) -> false | Meta (_, next_e) -> let_group_requires_parentheses next_e let is_var (e : texpression) : bool = - match e.e with Local _ -> true | _ -> false + match e.e with Var _ -> true | _ -> false let as_var (e : texpression) : VarId.id = - match e.e with Local v -> v | _ -> raise (Failure "Unreachable") + match e.e with Var v -> v | _ -> raise (Failure "Unreachable") (** Remove the external occurrences of [Meta] *) let rec unmeta (e : texpression) : texpression = @@ -350,12 +350,12 @@ let unit_rvalue : texpression = { e; ty } let mk_texpression_from_var (v : var) : texpression = - let e = Local v.id in + let e = Var v.id in let ty = v.ty in { e; ty } let mk_typed_pattern_from_var (v : var) (mp : mplace option) : typed_pattern = - let value = PatVar (Var (v, mp)) in + let value = PatVar (v, mp) in let ty = v.ty in { value; ty } @@ -535,8 +535,8 @@ module TypeCheck = struct | PatConcrete cv -> check_constant_value cv v.ty; ctx - | PatVar Dummy -> ctx - | PatVar (Var (var, _)) -> + | PatDummy -> ctx + | PatVar (var, _) -> assert (var.ty = v.ty); let env = VarId.Map.add var.id var.ty ctx.env in { ctx with env } @@ -567,7 +567,7 @@ module TypeCheck = struct let rec check_texpression (ctx : tc_ctx) (e : texpression) : unit = match e.e with - | Local var_id -> ( + | Var 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 diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml index 14a844a1..c0e47ca7 100644 --- a/src/SymbolicToPure.ml +++ b/src/SymbolicToPure.ml @@ -1512,9 +1512,7 @@ and translate_expansion (config : config) (p : S.mplace option) let branches = List.map translate_branch branches in let otherwise = translate_expression config otherwise ctx in let pat_ty = Integer int_ty in - let otherwise_pat : typed_pattern = - { value = PatVar Dummy; ty = pat_ty } - in + let otherwise_pat : typed_pattern = { value = PatDummy; ty = pat_ty } in let otherwise : match_branch = { pat = otherwise_pat; branch = otherwise } in -- cgit v1.2.3