diff options
| -rw-r--r-- | compiler/PrintPure.ml | 3 | ||||
| -rw-r--r-- | compiler/Pure.ml | 1 | ||||
| -rw-r--r-- | compiler/PureMicroPasses.ml | 5 | ||||
| -rw-r--r-- | compiler/PureUtils.ml | 5 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 7 |
5 files changed, 17 insertions, 4 deletions
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index de68adc3..c13ce238 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -521,7 +521,7 @@ let rec texpression_to_string (fmt : ast_formatter) (inside : bool) let meta_s = meta_to_string fmt meta in let e = texpression_to_string fmt inside indent indent_incr e in match meta with - | Assignment _ -> + | Assignment _ | Tag _ -> let e = meta_s ^ "\n" ^ indent ^ e in if inside then "(" ^ e ^ ")" else e | MPlace _ -> "(" ^ meta_s ^ " " ^ e ^ ")") @@ -655,6 +655,7 @@ and meta_to_string (fmt : ast_formatter) (meta : meta) : string = ^ texpression_to_string fmt false "" "" rv ^ rp ^ ")" | MPlace mp -> "@mplace=" ^ mplace_to_string fmt mp + | Tag msg -> "@tag \"" ^ msg ^ "\"" in "@meta[" ^ meta ^ "]" diff --git a/compiler/Pure.ml b/compiler/Pure.ml index 97eced1d..521d60e6 100644 --- a/compiler/Pure.ml +++ b/compiler/Pure.ml @@ -519,6 +519,7 @@ and meta = The second (optional) mplace stores the origin. *) | MPlace of mplace (** Meta-information about the origin of a value *) + | Tag of string (** A tag - typically used for debugging *) [@@deriving show, visitors diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml index ae791135..aed5b02d 100644 --- a/compiler/PureMicroPasses.ml +++ b/compiler/PureMicroPasses.ml @@ -483,6 +483,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl = in ctx | MPlace mp -> add_right_constraint mp e ctx + | Tag _ -> ctx in let ctx, e = update_texpression e ctx in let e = mk_meta meta e in @@ -1433,7 +1434,7 @@ let decompose_let_bindings (decompose_monadic : bool) * - if not, make the decomposition in two steps *) match lv.value with - | PatVar _ -> + | PatVar _ | PatDummy -> (* Variable: nothing to do *) (monadic, lv, re, next_e) | _ -> @@ -1444,7 +1445,7 @@ let decompose_let_bindings (decompose_monadic : bool) (* Visit the next expression *) let next_e = self#visit_texpression env next_e in (* Create the let-bindings *) - (true, ltmp, re, mk_let false lv rtmp next_e) + (monadic, ltmp, re, mk_let false lv rtmp next_e) in (* Decompose the nested let-patterns *) let lv, next_e = diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index 4816f31f..a60bcd78 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -68,6 +68,11 @@ let mk_let (monadic : bool) (lv : typed_pattern) (re : texpression) let ty = next_e.ty in { e; ty } +let mk_tag (msg : string) (next_e : texpression) : texpression = + let e = Meta (Tag msg, next_e) in + let ty = next_e.ty in + { e; ty } + (** Type substitution *) let ty_substitute (tsubst : TypeVarId.id -> ty) (ty : ty) : ty = let obj = diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index b2b5e010..2c82cf93 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -284,6 +284,10 @@ let fun_decl_to_string (ctx : bs_ctx) (def : Pure.fun_decl) : string = in PrintPure.fun_decl_to_string fmt def +let typed_pattern_to_string (ctx : bs_ctx) (p : Pure.typed_pattern) : string = + let fmt = bs_ctx_to_pp_ast_formatter ctx in + PrintPure.typed_pattern_to_string fmt p + (* TODO: move *) let abs_to_string (ctx : bs_ctx) (abs : V.abs) : string = let fmt = bs_ctx_to_ast_formatter ctx in @@ -2228,8 +2232,9 @@ and translate_forward_end (ectx : C.eval_ctx) (* Translate the end of the function *) let next_e = translate_end ctx in - (* Introduce the call to the loop in the generated AST *) + (* Introduce the call to the loop forward function in the generated AST *) let out_pat = mk_simpl_tuple_pattern out_pats in + let loop_call = let fun_id = Fun (FromLlbc (fid, Some loop_id, None)) in let func = { id = FunOrOp fun_id; type_args = loop_info.type_args } in |