diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Print.ml | 5 | ||||
| -rw-r--r-- | src/PrintPure.ml | 40 | ||||
| -rw-r--r-- | src/Pure.ml | 2 | ||||
| -rw-r--r-- | src/PureMicroPasses.ml | 6 |
4 files changed, 30 insertions, 23 deletions
diff --git a/src/Print.ml b/src/Print.ml index 24945298..5ccba517 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -1072,9 +1072,8 @@ module LlbcAst = struct * (we have access to a body) *) match def.body with | None -> - (* Arguments - we need to ignore the first input type which is actually - * the return type... TODO: fix that *) - let input_tys = List.tl sg.inputs in + (* Arguments *) + let input_tys = sg.inputs in let args = List.map sty_to_string input_tys in let args = String.concat ", " args in diff --git a/src/PrintPure.ml b/src/PrintPure.ml index 1ad37a5b..09194d85 100644 --- a/src/PrintPure.ml +++ b/src/PrintPure.ml @@ -191,19 +191,15 @@ let type_decl_to_string (fmt : type_formatter) (def : type_decl) : string = "enum " ^ name ^ params ^ " =\n" ^ variants | Opaque -> "opaque type " ^ name ^ params +let var_to_varname (v : var) : string = + match v.basename with + | Some name -> name ^ "^" ^ VarId.to_string v.id + | None -> "^" ^ VarId.to_string v.id + let var_to_string (fmt : type_formatter) (v : var) : string = - let varname = - match v.basename with - | Some name -> name ^ "^" ^ VarId.to_string v.id - | None -> "^" ^ VarId.to_string v.id - in + let varname = var_to_varname v in "(" ^ varname ^ " : " ^ ty_to_string fmt v.ty ^ ")" -let var_or_dummy_to_string (fmt : value_formatter) (v : var_or_dummy) : string = - match v with - | Var (v, _) -> var_to_string (value_to_type_formatter fmt) v - | Dummy -> "_" - let rec projection_to_string (fmt : ast_formatter) (inside : string) (p : projection) : string = match p with @@ -228,6 +224,20 @@ let rec projection_to_string (fmt : ast_formatter) (inside : string) let variant_name = fmt.adt_variant_to_string adt_id variant_id in "(" ^ s ^ " as " ^ variant_name ^ ")." ^ field_name)) +let mplace_to_string (fmt : ast_formatter) (p : mplace) : string = + let name = match p.name with None -> "_" | Some name -> name in + projection_to_string fmt name p.projection + +let var_or_dummy_to_string (fmt : value_formatter) (v : var_or_dummy) : string = + match v with + | Var (v, Some { name = Some name; projection }) -> + assert (projection = []); + let fmt = value_to_type_formatter fmt in + "(" ^ var_to_varname v ^ " @meta[@dest=" ^ name ^ "] : " + ^ ty_to_string fmt v.ty ^ ")" + | Var (v, _) -> var_to_string (value_to_type_formatter fmt) v + | Dummy -> "_" + let place_to_string (fmt : ast_formatter) (p : place) : string = (* TODO: improve that *) let var = fmt.var_id_to_string p.var in @@ -394,10 +404,6 @@ let fun_id_to_string (fmt : ast_formatter) (fun_id : fun_id) : string = | Binop (binop, int_ty) -> binop_to_string binop ^ "<" ^ integer_type_to_string int_ty ^ ">" -let mplace_to_string (fmt : ast_formatter) (p : mplace) : string = - let name = match p.name with None -> "_" | Some name -> name in - projection_to_string fmt name p.projection - let meta_to_string (fmt : ast_formatter) (meta : meta) : string = let meta = match meta with @@ -444,10 +450,9 @@ and let_to_string (fmt : ast_formatter) (indent : string) (indent_incr : string) (monadic : bool) (lv : typed_lvalue) (re : texpression) (e : texpression) : string = let indent1 = indent ^ indent_incr in - let val_fmt = ast_to_value_formatter fmt in let re = texpression_to_string fmt indent1 indent_incr re in let e = texpression_to_string fmt indent indent_incr e in - let lv = typed_lvalue_to_string val_fmt lv in + let lv = typed_lvalue_to_string (ast_to_value_formatter fmt) lv in if monadic then lv ^ " <-- " ^ re ^ ";\n" ^ indent ^ e else "let " ^ lv ^ " = " ^ re ^ " in\n" ^ indent ^ e @@ -466,9 +471,8 @@ and switch_to_string (fmt : ast_formatter) (indent : string) "if " ^ scrut ^ "\n" ^ indent ^ "then\n" ^ indent ^ e_true ^ "\n" ^ indent ^ "else\n" ^ indent ^ e_false | Match branches -> - let val_fmt = ast_to_value_formatter fmt in let branch_to_string (b : match_branch) : string = - let pat = typed_lvalue_to_string val_fmt b.pat in + let pat = typed_lvalue_to_string (ast_to_value_formatter fmt) b.pat in indent ^ "| " ^ pat ^ " ->\n" ^ indent1 ^ texpression_to_string fmt indent1 indent_incr b.branch in diff --git a/src/Pure.ml b/src/Pure.ml index 9efab912..58ee0b98 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -236,7 +236,7 @@ class virtual ['self] mapreduce_value_base = end type var_or_dummy = - | Var of var * mplace option + | Var of var * mplace option (* TODO: the mplace is actually always a variable *) | Dummy (** Ignored value: `_`. *) [@@deriving show, diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml index 7b34ad76..06fd3d69 100644 --- a/src/PureMicroPasses.ml +++ b/src/PureMicroPasses.ml @@ -242,7 +242,11 @@ let compute_pretty_names (def : fun_decl) : fun_decl = method plus ctx0 ctx1 _ = merge_ctxs (ctx0 ()) (ctx1 ()) - method! visit_var _ v () = add_var (self#zero ()) v + method! visit_Var _ v mp () = + (* Register the variable *) + let ctx = add_var (self#zero ()) v in + (* Register the mplace information if there is such information *) + match mp with None -> ctx | Some mp -> add_constraint mp v.id ctx end in let ctx1 = obj#visit_typed_lvalue () lv () in |