diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index f98ffa3..618cb11 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -6,40 +6,40 @@ open Utils -(** [ast_to_cast] translates a [t_nodelist] into a [c_nodelist] *) -let ast_to_cast (nodes: t_nodelist) (h: node_states): c_nodelist = +(** [ast_to_cast] translates a [t_nodelist] into a [i_nodelist] *) +let ast_to_cast (nodes: t_nodelist) (h: node_states): i_nodelist = let c = ref 1 in let ast_to_cast_varlist vl = snd vl in let rec ast_to_cast_expr hloc = function | EVar (_, v) -> begin match Hashtbl.find_opt hloc (v, false) with - | None -> CVar (CVInput (name_of_var v)) - | Some (s, i) -> CVar (CVStored (s, i)) + | None -> IVar (CVInput (name_of_var v)) + | Some (s, i) -> IVar (CVStored (s, i)) end - | EMonOp (_, op, e) -> CMonOp (op, ast_to_cast_expr hloc e) + | EMonOp (_, op, e) -> IMonOp (op, ast_to_cast_expr hloc e) | EBinOp (_, op, e, e') -> - CBinOp (op, ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') + IBinOp (op, ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') | ETriOp (_, op, e, e', e'') -> - CTriOp + ITriOp (op, ast_to_cast_expr hloc e, ast_to_cast_expr hloc e', ast_to_cast_expr hloc e'') | EComp (_, op, e, e') -> - CComp (op, ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') + IComp (op, ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') | EWhen (_, e, e') -> - CWhen (ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') + IWhen (ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') | EReset (_, e, e') -> - CReset (ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') - | EConst (_, c) -> CConst c - | ETuple (_, l) -> CTuple (List.map (ast_to_cast_expr hloc) l) + IReset (ast_to_cast_expr hloc e, ast_to_cast_expr hloc e') + | EConst (_, c) -> IConst c + | ETuple (_, l) -> ITuple (List.map (ast_to_cast_expr hloc) l) | EApp (_, n, e) -> begin let e = ast_to_cast_expr hloc e in - let res = CApp (!c, n, e) in + let res = IApp (!c, n, e) in let () = incr c in res end in - let ast_to_cast_eq hloc (patt, expr) : c_equation = + let ast_to_cast_eq hloc (patt, expr) : i_equation = (ast_to_cast_varlist patt, ast_to_cast_expr hloc expr) in List.map begin @@ -47,11 +47,11 @@ let ast_to_cast (nodes: t_nodelist) (h: node_states): c_nodelist = let () = c := 1 in let hloc = (Hashtbl.find h node.n_name).nt_map in { - cn_name = node.n_name; - cn_inputs = ast_to_cast_varlist node.n_inputs; - cn_outputs = ast_to_cast_varlist node.n_outputs; - cn_local_vars = ast_to_cast_varlist node.n_local_vars; - cn_equations = List.map (ast_to_cast_eq hloc) node.n_equations; + in_name = node.n_name; + in_inputs = ast_to_cast_varlist node.n_inputs; + in_outputs = ast_to_cast_varlist node.n_outputs; + in_local_vars = ast_to_cast_varlist node.n_local_vars; + in_equations = List.map (ast_to_cast_eq hloc) node.n_equations; } end nodes @@ -156,7 +156,7 @@ let make_state_types nodes: node_states = let node_out_vars = snd node.n_outputs in let h_out = Hashtbl.create (List.length node_out_vars) in let () = List.iteri - (fun n v -> + (fun n (v: t_var) -> match v with | IVar _ -> let i = Hashtbl.find h_int (v, false) in @@ -197,8 +197,8 @@ let make_state_types nodes: node_states = (** The following function prints the code to remember previous values of * variables used with the pre construct. *) let cp_prevars fmt (node, h) = - let node_st = Hashtbl.find h node.cn_name in - match (Hashtbl.find h node.cn_name).nt_prevars with + let node_st = Hashtbl.find h node.in_name in + match (Hashtbl.find h node.in_name).nt_prevars with | [] -> () | l -> Format.fprintf fmt @@ -219,7 +219,7 @@ let cp_prevars fmt (node, h) = *) let cp_init_aux_nodes fmt (node, h) = let rec aux fmt (node, nst, i) = - match find_app_opt node.cn_equations i with + match find_app_opt node.in_equations i with | None -> () (** All auxiliary nodes have been initialized *) | Some n -> begin @@ -230,7 +230,7 @@ let cp_init_aux_nodes fmt (node, h) = (Format.asprintf "t_state_%s" n.n_name) (i-1) end in - let nst = Hashtbl.find h node.cn_name in + let nst = Hashtbl.find h node.in_name in if nst.nt_count_app = 0 then () else begin @@ -262,7 +262,7 @@ 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.cn_equations, Hashtbl.find h node.cn_name) + cp_equations (node.in_equations, Hashtbl.find h node.in_name) cp_prevars (node, h) (** [cp_nodes] recursively prints all the nodes of a program. *) @@ -279,7 +279,7 @@ let rec cp_nodes fmt (nodes, h) = (** main function that prints a C-code from a term of type [t_nodelist]. *) let ast_to_c prog = let prog_st_types = make_state_types prog in - let prog: c_nodelist = ast_to_cast prog prog_st_types in + let prog: i_nodelist = ast_to_cast prog prog_st_types in Format.printf "%a\n\n%a\n\n/* Node Prototypes: */\n%a\n\n/* Nodes: */\n%a" cp_includes (Config.c_includes) cp_state_types prog_st_types diff --git a/src/cprint.ml b/src/cprint.ml index 5f191ae..39da179 100644 --- a/src/cprint.ml +++ b/src/cprint.ml @@ -7,7 +7,7 @@ open Ast let rec cp_includes fmt = function | [] -> () | h :: t -> - Format.fprintf fmt "#include <%s>\n%a" h cp_includes t + Format.fprintf fmt "#include <%s.h>\n%a" h cp_includes t let cp_node_state fmt (st: node_state) = let maybeprint fmt (ty, nb, name): unit = @@ -58,17 +58,17 @@ let rec cp_varlist fmt vl = cp_varlist vl let cp_prototype fmt (node, h): unit = - match Hashtbl.find_opt h node.cn_name with + match Hashtbl.find_opt h node.in_name with | None -> failwith "This should not happend!" | Some nst -> begin Format.fprintf fmt "void fn_%s (%s *state, %a)" - node.cn_name + node.in_name nst.nt_name - cp_varlist node.cn_inputs + cp_varlist node.in_inputs end -let rec cp_prototypes fmt ((nodes, h): c_nodelist * node_states) = +let rec cp_prototypes fmt ((nodes, h): i_nodelist * node_states) = match nodes with | [] -> () | node :: nodes -> diff --git a/src/intermediate_ast.ml b/src/intermediate_ast.ml index 31a4dc7..3cc296b 100644 --- a/src/intermediate_ast.ml +++ b/src/intermediate_ast.ml @@ -44,35 +44,35 @@ type c_var = | CVStored of string * int | CVInput of ident -type c_expression = - | CVar of c_var - | CMonOp of monop * c_expression - | CBinOp of binop * c_expression * c_expression - | CTriOp of triop * c_expression * c_expression * c_expression - | CComp of compop * c_expression * c_expression - | CWhen of c_expression * c_expression - | CReset of c_expression * c_expression - | CConst of const - | CTuple of (c_expression list) +type i_expression = + | IVar of c_var + | IMonOp of monop * i_expression + | IBinOp of binop * i_expression * i_expression + | ITriOp of triop * i_expression * i_expression * i_expression + | IComp of compop * i_expression * i_expression + | IWhen of i_expression * i_expression + | IReset of i_expression * i_expression + | IConst of const + | ITuple of (i_expression list) (** [CApp] below represents the n-th call to an aux node *) - | CApp of int * t_node * c_expression + | IApp of int * t_node * i_expression -and c_varlist = t_var list +and i_varlist = t_var list -and c_equation = c_varlist * c_expression +and i_equation = i_varlist * i_expression -and c_eqlist = c_equation list +and i_eqlist = i_equation list -and c_node = +and i_node = { - cn_name : ident; - cn_inputs: c_varlist; - cn_outputs: c_varlist; - cn_local_vars: c_varlist; - cn_equations: c_eqlist; + in_name : ident; + in_inputs: i_varlist; + in_outputs: i_varlist; + in_local_vars: i_varlist; + in_equations: i_eqlist; } -type c_nodelist = c_node list +type i_nodelist = i_node list type node_states = (ident, node_state) Hashtbl.t diff --git a/src/intermediate_utils.ml b/src/intermediate_utils.ml index c964e50..34414d1 100644 --- a/src/intermediate_utils.ml +++ b/src/intermediate_utils.ml @@ -2,15 +2,15 @@ open Intermediate_ast let rec find_app_opt eqs i = let rec find_app_expr_opt i = function - | CVar _ | CConst _ -> None - | CMonOp (_, e) -> find_app_expr_opt i e - | CReset (e, e') | CWhen (e, e') | CComp (_, e, e') | CBinOp (_, e, e') -> + | IVar _ | IConst _ -> None + | IMonOp (_, e) -> find_app_expr_opt i e + | IReset (e, e') | IWhen (e, e') | IComp (_, e, e') | IBinOp (_, e, e') -> begin match find_app_expr_opt i e with | None -> find_app_expr_opt i e' | Some n -> Some n end - | CTriOp (_, e, e', e'') -> + | ITriOp (_, e, e', e'') -> begin match find_app_expr_opt i e with | None -> @@ -21,15 +21,15 @@ let rec find_app_opt eqs i = end | Some n -> Some n end - | CTuple l -> + | ITuple l -> List.fold_left (fun acc e -> match acc, find_app_expr_opt i e with | Some n, _ -> Some n | None, v -> v) None l - (** [CApp] below represents the n-th call to an aux node *) - | CApp (j, n, e) -> + (** [IApp] below represents the n-th call to an aux node *) + | IApp (j, n, e) -> if i = j then Some n else find_app_expr_opt i e