From ce686f6c9a1051e89ae592e14d7a6e00b63e459f Mon Sep 17 00:00:00 2001 From: dsac Date: Sun, 18 Dec 2022 10:41:36 +0100 Subject: [PATCH] [ast2C] merge ok (needs linearization) --- src/ast_to_c.ml | 2 +- src/cprint.ml | 25 ++++++++++++++++++++----- src/ctranslation.ml | 13 +++++++++---- src/test2.node | 3 +++ 4 files changed, 33 insertions(+), 10 deletions(-) diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index e812ff5..37f8f4e 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -247,7 +247,7 @@ let cp_init_aux_nodes fmt (node, h) = then () else begin Format.fprintf fmt "\t/* Initialize the auxiliary nodes */\n\ - \tif (state->is_init) {\n%a\t}\n" + \tif (state->is_init) {\n%a\t}\n\n\n" aux (node, nst, nst.nt_count_app) end diff --git a/src/cprint.ml b/src/cprint.ml index 714ae48..43767da 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -42,7 +42,7 @@ let cp_state_types fmt (h: (ident, node_state) Hashtbl.t): unit = let cp_var' fmt = function | CVStored (arr, idx) -> Format.fprintf fmt "state->%s[%d]" arr idx - | CVInput s -> Format.fprintf fmt "s" + | CVInput s -> Format.fprintf fmt "%s" s let cp_var fmt = function | IVar s -> Format.fprintf fmt "int %s" s @@ -147,10 +147,12 @@ let rec cp_value fmt (value, (hloc: (ident * bool, string * int) Hashtbl.t)) = | CMonOp (MOp_pre, _) -> failwith "[cprint.ml] The linearization should have removed this case." +let prefix_ = ref "\t" + (** The following function prints one transformed equation of the program into a * set of instruction ending in assignments. *) let rec cp_expression fmt (expr, hloc) = - let prefix = "\t" in + let prefix = !prefix_ in let rec cp_block fmt = function | [] -> () | e :: b -> Format.fprintf fmt "%a%a" cp_expression (e, hloc) cp_block b @@ -170,8 +172,9 @@ let rec cp_expression fmt (expr, hloc) = begin let aux_node_st = Hashtbl.find h fn in let h_out = aux_node_st.nt_output_map in - Format.fprintf fmt "%sfn_%s(%a);\n" + Format.fprintf fmt "%sfn_%s(%s, %a);\n" prefix fn + (Format.asprintf "state->aux_states[%d]" (nb-1)) cp_varlist' argl; let _ = List.fold_left (fun i var -> @@ -186,9 +189,21 @@ let rec cp_expression fmt (expr, hloc) = | CVInput _ -> failwith "[cprint.ml] Impossible!") 0 destl in () end - | CIf (v, b1, b2) -> - Format.fprintf fmt "if (%a) {\n%a\t\t} else {\n%a\t\t}\n" + | CIf (v, b1, []) -> + let p = prefix in + prefix_ := prefix^"\t"; + Format.fprintf fmt "%sif (%a) {\n%a%s}\n" + p cp_value (v, hloc) cp_block b1 + p; + prefix_ := p + | CIf (v, b1, b2) -> + Format.fprintf fmt "%sif (%a) {\n%a%s} else {\n%a%s}\n" + prefix + cp_value (v, hloc) + cp_block b1 + prefix cp_block b2 + prefix diff --git a/src/ctranslation.ml b/src/ctranslation.ml index 0e593f3..5433596 100644 --- a/src/ctranslation.ml +++ b/src/ctranslation.ml @@ -17,7 +17,7 @@ let rec iexpression_to_cvalue e = | IEApp _ | IETriOp _ -> failwith "[ctranslation.ml] Should not happened." -let equation_to_expression (node_st, node_sts, (vl, expr)) = +let rec equation_to_expression (node_st, node_sts, (vl, expr)) = let hloc = node_st.nt_map in let fetch_unique_var () = match vl with @@ -67,10 +67,15 @@ let equation_to_expression (node_st, node_sts, (vl, expr)) = vl in CApplication (node.n_name,i , al, vl, node_sts) + | IETuple _ -> failwith "[ctranslation.ml] linearisatiosn should have transformed you." + | IEWhen (expr, cond) -> + begin + CIf (iexpression_to_cvalue cond, + [equation_to_expression (node_st, node_sts, (vl, expr))], + []) + end (*TODO! | IETriOp of triop * i_expression * i_expression * i_expression - | IEWhen of i_expression * i_expression - | IEReset of i_expression * i_expression - | IETuple of (i_expression list)*) + | IEReset of i_expression * i_expression*) | _ -> failwith "[ctranslation.ml] TODO!" diff --git a/src/test2.node b/src/test2.node index 5dcbf29..a88c1e6 100644 --- a/src/test2.node +++ b/src/test2.node @@ -5,6 +5,9 @@ let tel node n (i: int) returns (o1, o2: int); +var t1, t2: int; c: bool; let + c = true -> not pre c; + (t1, t2) = aux (i) when c; (o1, o2) = aux (i); tel