diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index 71be88e..e812ff5 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -254,20 +254,20 @@ let cp_init_aux_nodes fmt (node, h) = (** [cp_equations] prints the node equations. *) -let rec cp_equations fmt (eqs, hloc) = +let rec cp_equations fmt (eqs, hloc, h) = match eqs with | [] -> () | eq :: eqs -> Format.fprintf fmt "%a%a" - cp_expression (equation_to_expression (hloc.nt_map, eq), hloc.nt_map) - cp_equations (eqs, hloc) + cp_expression (equation_to_expression (hloc, h, eq), hloc.nt_map) + cp_equations (eqs, hloc, h) (** [cp_node] prints a single node *) let cp_node fmt (node, h) = Format.fprintf fmt "%a\n{\n%a%a\n\n\tstate->is_init = false;\n%a}\n" cp_prototype (node, h) cp_init_aux_nodes (node, h) - cp_equations (node.in_equations, Hashtbl.find h node.in_name) + cp_equations (node.in_equations, Hashtbl.find h node.in_name, h) cp_prevars (node, h) (** [cp_nodes] recursively prints all the nodes of a program. *) diff --git a/src/cast.ml b/src/cast.ml index f000b2a..81b0672 100644 --- a/src/cast.ml +++ b/src/cast.ml @@ -13,7 +13,7 @@ and c_expression = | CAssign of c_var * c_value | CSeq of c_expression * c_expression | CIf of c_value * c_block * c_block - | CApplication of ident * c_var list + | CApplication of ident * int * c_var list * c_var list * node_states (** A value here is anything that can be inlined into a single C expression * containing no function call, condition, ... *) diff --git a/src/cprint.ml b/src/cprint.ml index 572ab06..714ae48 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -166,11 +166,26 @@ let rec cp_expression fmt (expr, hloc) = Format.fprintf fmt "%a%a" cp_expression (e, hloc) cp_expression (e', hloc) - | CApplication (fn, l) -> - (Format.fprintf fmt "%s(%a);" - fn - cp_varlist' l; - failwith "TODO: use nt_output_map to fetch the output!") + | CApplication (fn, nb, argl, destl, h) -> + 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" + prefix fn + cp_varlist' argl; + let _ = List.fold_left + (fun i var -> + match var with + | CVStored (arr, idx) -> + let (arr', idx') = Hashtbl.find h_out i in + Format.fprintf fmt "%sstate->%s[%d] = ((%s*)(state->aux_states[%d]))->%s[%d];\n" + prefix arr idx + aux_node_st.nt_name (nb-1) + arr' idx'; + i+1 + | 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" cp_value (v, hloc) diff --git a/src/ctranslation.ml b/src/ctranslation.ml index 78979a4..0e593f3 100644 --- a/src/ctranslation.ml +++ b/src/ctranslation.ml @@ -17,7 +17,8 @@ let rec iexpression_to_cvalue e = | IEApp _ | IETriOp _ -> failwith "[ctranslation.ml] Should not happened." -let equation_to_expression ((hloc: (ident * bool, string * int)Hashtbl.t), ((vl, expr): i_equation)) : c_expression = +let equation_to_expression (node_st, node_sts, (vl, expr)) = + let hloc = node_st.nt_map in let fetch_unique_var () = match vl with | [v] -> @@ -44,12 +45,32 @@ let equation_to_expression ((hloc: (ident * bool, string * int)Hashtbl.t), ((vl, | IEComp (op, e, e') -> CAssign (fetch_unique_var (), CComp (op, iexpression_to_cvalue e, iexpression_to_cvalue e')) + (** [CApp] below represents the i-th call to an aux node *) + | IEApp (i, node, e) -> + (** e is a tuple of variables due to the linearization pass *) + let al: c_var list = + match e with + | IETuple l -> + List.map + (function + | IEVar v -> v + | _ -> failwith "[ctranslation.ml] should not happened due to the linearization pass." + ) l + | _ -> failwith "[ctranslation.ml] should not happened due to the linearization pass." + in + let vl = + List.map + (fun v -> + match Hashtbl.find_opt hloc (Utils.name_of_var v, false) with + | Some (arr, idx) -> CVStored (arr, idx) + | None -> CVInput (Utils.name_of_var v)) + vl + in + CApplication (node.n_name,i , al, vl, node_sts) (*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) - (** [CApp] below represents the n-th call to an aux node *) - | IEApp of int * t_node * i_expression*) + | IETuple of (i_expression list)*) | _ -> failwith "[ctranslation.ml] TODO!" diff --git a/src/test2.node b/src/test2.node new file mode 100644 index 0000000..5dcbf29 --- /dev/null +++ b/src/test2.node @@ -0,0 +1,10 @@ +node aux (i: int) returns (a, b: int); +let + a = 1 -> pre i; + b = 2 * i -> (3 * pre i); +tel + +node n (i: int) returns (o1, o2: int); +let + (o1, o2) = aux (i); +tel