summaryrefslogtreecommitdiff
path: root/src/PrintPure.ml
diff options
context:
space:
mode:
authorSon Ho2022-04-29 16:10:54 +0200
committerSon Ho2022-04-29 16:10:54 +0200
commit3f189e83f72b9ea570a29f85e77e94c1f662fa21 (patch)
tree2e3f567cb5ea2dafff8ab847c4f1a02667a89ef3 /src/PrintPure.ml
parentf64397c472e82d6b001cf6507d7786d7ee90999d (diff)
Make good progress updating the code
Diffstat (limited to 'src/PrintPure.ml')
-rw-r--r--src/PrintPure.ml21
1 files changed, 10 insertions, 11 deletions
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index cf8c3f57..9ba1bba7 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -455,13 +455,8 @@ 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, mp) ->
- let mp =
- match mp with
- | None -> ""
- | Some mp -> " [@mplace=" ^ mplace_to_string fmt mp ^ "]"
- in
- let s = fmt.var_id_to_string var_id ^ mp in
+ | Local 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
| App _ ->
@@ -482,11 +477,14 @@ let rec texpression_to_string (fmt : ast_formatter) (inside : bool)
| Switch (scrutinee, body) ->
let e = switch_to_string fmt indent indent_incr scrutinee body in
if inside then "(" ^ e ^ ")" else e
- | Meta (meta, e) ->
- let meta = meta_to_string fmt meta in
+ | Meta (meta, e) -> (
+ let meta_s = meta_to_string fmt meta in
let e = texpression_to_string fmt inside indent indent_incr e in
- let e = meta ^ "\n" ^ indent ^ e in
- if inside then "(" ^ e ^ ")" else e
+ match meta with
+ | Assignment _ ->
+ let e = meta_s ^ "\n" ^ indent ^ e in
+ if inside then "(" ^ e ^ ")" else e
+ | MPlace _ -> "(" ^ meta_s ^ " " ^ e ^ ")")
and app_to_string (fmt : ast_formatter) (inside : bool) (indent : string)
(indent_incr : string) (app : texpression) (args : texpression list) :
@@ -596,6 +594,7 @@ and meta_to_string (fmt : ast_formatter) (meta : meta) : string =
"@assign(" ^ mplace_to_string fmt lp ^ " := "
^ texpression_to_string fmt false "" "" rv
^ rp ^ ")"
+ | MPlace mp -> "@mplace=" ^ mplace_to_string fmt mp
in
"@meta[" ^ meta ^ "]"