diff options
| author | Son HO | 2024-03-20 06:48:08 +0100 |
|---|---|---|
| committer | GitHub | 2024-03-20 06:48:08 +0100 |
| commit | 0d52c3fe35d0b24de729bdfb917ad6c7104d0c6e (patch) | |
| tree | 7748d3c19a0993edc710690491a2dc6ea3a2b58f /compiler/PrintPure.ml | |
| parent | 8111c970fcae9d609961eba2ad6716e8c9fc1046 (diff) | |
| parent | 34850eed3c66f7f2c432294e4c589be53ad5d37b (diff) | |
Merge pull request #93 from AeneasVerif/son/examples
Add some examples and improve the shape of the generated code
Diffstat (limited to 'compiler/PrintPure.ml')
| -rw-r--r-- | compiler/PrintPure.ml | 25 |
1 files changed, 20 insertions, 5 deletions
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml index a401594d..00a431a0 100644 --- a/compiler/PrintPure.ml +++ b/compiler/PrintPure.ml @@ -585,7 +585,7 @@ let rec texpression_to_string (env : fmt_env) (inside : bool) (indent : string) let meta_s = emeta_to_string env meta in let e = texpression_to_string env inside indent indent_incr e in match meta with - | Assignment _ | SymbolicAssignment _ | Tag _ -> + | Assignment _ | SymbolicAssignments _ | SymbolicPlaces _ | Tag _ -> let e = meta_s ^ "\n" ^ indent ^ e in if inside then "(" ^ e ^ ")" else e | MPlace _ -> "(" ^ meta_s ^ " " ^ e ^ ")") @@ -717,10 +717,25 @@ and emeta_to_string (env : fmt_env) (meta : emeta) : string = "@assign(" ^ mplace_to_string env lp ^ " := " ^ texpression_to_string env false "" "" rv ^ rp ^ ")" - | SymbolicAssignment (var_id, rv) -> - "@symb_assign(" ^ VarId.to_string var_id ^ " := " - ^ texpression_to_string env false "" "" rv - ^ ")" + | SymbolicAssignments info -> + let infos = + List.map + (fun (var_id, rv) -> + VarId.to_string var_id ^ " == " + ^ texpression_to_string env false "" "" rv) + info + in + let infos = String.concat ", " infos in + "@symb_assign(" ^ infos ^ ")" + | SymbolicPlaces info -> + let infos = + List.map + (fun (var_id, name) -> + VarId.to_string var_id ^ " == \"" ^ name ^ "\"") + info + in + let infos = String.concat ", " infos in + "@symb_places(" ^ infos ^ ")" | MPlace mp -> "@mplace=" ^ mplace_to_string env mp | Tag msg -> "@tag \"" ^ msg ^ "\"" in |