[general] renaming (pp -> lustre_pp ; c_* -> intermediate_*)

This commit is contained in:
dsac 2022-12-17 21:26:32 +01:00
parent 916c7f544b
commit 3cbfaeb2a8
10 changed files with 57 additions and 130 deletions

View File

@ -1,6 +1,6 @@
open Ast open Ast
open Cast open Intermediate_ast
open C_utils open Intermediate_utils
open Cprint open Cprint
open Utils open Utils
@ -56,7 +56,6 @@ let ast_to_cast (nodes: t_nodelist) (h: node_states): c_nodelist =
end end
nodes nodes
(** The following function defines the [node_states] for the nodes of a program, (** The following function defines the [node_states] for the nodes of a program,
* and puts them in a hash table. *) * and puts them in a hash table. *)
let make_state_types nodes: node_states = let make_state_types nodes: node_states =
@ -198,21 +197,26 @@ let make_state_types nodes: node_states =
(** The following function prints the code to remember previous values of (** The following function prints the code to remember previous values of
* variables used with the pre construct. *) * variables used with the pre construct. *)
let cp_prevars fmt (node, h) = let cp_prevars fmt (node, h) =
Format.fprintf fmt
"\n\t/* Remember the values of variables used in the [pre] construct */\n";
let node_st = Hashtbl.find h node.cn_name in let node_st = Hashtbl.find h node.cn_name in
List.iter match (Hashtbl.find h node.cn_name).nt_prevars with
(fun v -> (** Note that «dst_array = src_array» should hold. *) | [] -> ()
let (src_array, src_idx) = Hashtbl.find node_st.nt_map (v, false) in | l ->
let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in Format.fprintf fmt
Format.fprintf fmt "\t%s[%d] = %s[%d];\n" "\n\t/* Remember the values used in the [pre] construct */\n";
dst_array dst_idx src_array src_idx) List.iter
node_st.nt_prevars (fun v -> (** Note that «dst_array = src_array» should hold. *)
let (src_array, src_idx) = Hashtbl.find node_st.nt_map (v, false) in
let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in
Format.fprintf fmt "\t%s[%d] = %s[%d];\n"
dst_array dst_idx src_array src_idx)
l
(** The following function defines the behaviour to have at the first (** The following function defines the behaviour to have at the first
* execution of a node, namely: * execution of a node, namely:
* - initialize the states of auxiliary nodes * - initialize the states of auxiliary nodes
* *) *)
let cp_init_aux_nodes fmt (node, h) = let cp_init_aux_nodes fmt (node, h) =
let rec aux fmt (node, nst, i) = let rec aux fmt (node, nst, i) =
match find_app_opt node.cn_equations i with match find_app_opt node.cn_equations i with
@ -220,7 +224,7 @@ let cp_init_aux_nodes fmt (node, h) =
| Some n -> | Some n ->
begin begin
Format.fprintf fmt "%a\t\tstate->aux_states[%d] = malloc (sizeof (%s));\n\ Format.fprintf fmt "%a\t\tstate->aux_states[%d] = malloc (sizeof (%s));\n\
\t\t(%s*)(state->aux_states[%d])->is_init = true;\n" \t\t((%s*)(state->aux_states[%d]))->is_init = true;\n"
aux (node, nst, i-1) aux (node, nst, i-1)
(i-1) (Format.asprintf "t_state_%s" n.n_name) (i-1) (Format.asprintf "t_state_%s" n.n_name)
(Format.asprintf "t_state_%s" n.n_name) (i-1) (Format.asprintf "t_state_%s" n.n_name) (i-1)
@ -235,12 +239,33 @@ let cp_init_aux_nodes fmt (node, h) =
aux (node, nst, nst.nt_count_app) aux (node, nst, nst.nt_count_app)
end end
let rec cp_node fmt (node, h) =
Format.fprintf fmt "%a\n{\n%a\t\tTODO...\n\n\tstate->is_init = false;\n%a}\n"
(** The following function prints one equation of the program into a set of
* instruction ending in assignments. *)
let cp_equation fmt (eq, hloc) =
Format.fprintf fmt "\t\t/* TODO! */\n"
(** [cp_equations] prints the node equations. *)
let rec cp_equations fmt (eqs, hloc) =
match eqs with
| [] -> ()
| eq :: eqs ->
Format.fprintf fmt "%a%a"
cp_equation (eq, hloc)
cp_equations (eqs, hloc)
(** [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_prototype (node, h)
cp_init_aux_nodes (node, h) cp_init_aux_nodes (node, h)
cp_equations (node.cn_equations, Hashtbl.find h node.cn_name)
cp_prevars (node, h) cp_prevars (node, h)
(** [cp_nodes] recursively prints all the nodes of a program. *)
let rec cp_nodes fmt (nodes, h) = let rec cp_nodes fmt (nodes, h) =
match nodes with match nodes with
| [] -> () | [] -> ()
@ -251,6 +276,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 ast_to_c prog =
let prog_st_types = make_state_types prog in let prog_st_types = make_state_types prog in
let prog: c_nodelist = ast_to_cast prog prog_st_types in let prog: c_nodelist = ast_to_cast prog prog_st_types in

View File

@ -1,5 +1,5 @@
open C_utils open Intermediate_utils
open Cast open Intermediate_ast
open Ast open Ast
(** This file contains extrimely simple functions printing C code. *) (** This file contains extrimely simple functions printing C code. *)

View File

@ -1,4 +1,4 @@
open Cast open Intermediate_ast
let rec find_app_opt eqs i = let rec find_app_opt eqs i =
let rec find_app_expr_opt i = function let rec find_app_expr_opt i = function

View File

@ -17,7 +17,7 @@ let exec_passes ast main_fn verbose debug passes f =
match p verbose debug main_fn ast with match p verbose debug main_fn ast with
| None -> (exit_error ("Error while in the pass "^n^".\n"); exit 0) | None -> (exit_error ("Error while in the pass "^n^".\n"); exit 0)
| Some ast -> ( | Some ast -> (
debug (Format.asprintf "Current AST (after %s):\n%a\n" n Pp.pp_ast ast); debug (Format.asprintf "Current AST (after %s):\n%a\n" n Lustre_pp.pp_ast ast);
aux ast passes) aux ast passes)
in in
aux ast passes aux ast passes
@ -34,7 +34,6 @@ let _ =
let debug = ref false in let debug = ref false in
let ppast = ref false in let ppast = ref false in
let nopopt = ref false in let nopopt = ref false in
let simopt = ref false in
let passes = ref [] in let passes = ref [] in
let source_file = ref "" in let source_file = ref "" in
let testopt = ref false in let testopt = ref false in
@ -51,7 +50,6 @@ let _ =
("-debug", Arg.Set debug, "Output a lot of debug information"); ("-debug", Arg.Set debug, "Output a lot of debug information");
("-p", Arg.String (fun s -> passes := s :: !passes), ("-p", Arg.String (fun s -> passes := s :: !passes),
"Add a pass to the compilation process"); "Add a pass to the compilation process");
("-sim", Arg.Set simopt, "Simulate the main node");
("-o", Arg.Set_string output_file, "Output file (defaults to [out.c])"); ("-o", Arg.Set_string output_file, "Output file (defaults to [out.c])");
] in ] in
Arg.parse speclist anon_fun usage_msg ; Arg.parse speclist anon_fun usage_msg ;
@ -93,7 +91,7 @@ let _ =
begin begin
close_in_noerr inchan; close_in_noerr inchan;
Format.printf "Syntax error at %a: %s\n\n" Format.printf "Syntax error at %a: %s\n\n"
Pp.pp_loc (l, !source_file) s; Lustre_pp.pp_loc (l, !source_file) s;
exit 0 exit 0
end end
| Parsing.Parse_error -> | Parsing.Parse_error ->
@ -101,7 +99,7 @@ let _ =
close_in_noerr inchan; close_in_noerr inchan;
Parsing.( Parsing.(
Format.printf "Syntax error at %a\n\n" Format.printf "Syntax error at %a\n\n"
Pp.pp_loc ((symbol_start_pos (), symbol_end_pos()), !source_file)); Lustre_pp.pp_loc ((symbol_start_pos (), symbol_end_pos()), !source_file));
exit 0 exit 0
end end
in in
@ -121,19 +119,14 @@ let _ =
in in
print_debug (Format.asprintf "Initial AST (before executing any passes):\n%a" print_debug (Format.asprintf "Initial AST (before executing any passes):\n%a"
Pp.pp_ast ast) ; Lustre_pp.pp_ast ast) ;
exec_passes ast main_fn print_verbose print_debug passes exec_passes ast main_fn print_verbose print_debug passes
begin begin
if !simopt if !ppast
then Simulation.simulate main_fn then (Format.printf "%a" Lustre_pp.pp_ast)
else else (
begin if !nopopt
if !ppast then (fun _ -> ())
then (Format.printf "%a" Pp.pp_ast) else Ast_to_c.ast_to_c)
else ( end
if !nopopt
then (fun _ -> ())
else Ast_to_c.ast_to_c)
end
end

View File

@ -1,92 +0,0 @@
open Ast
type sim_var =
| SIVar of ident * (int option)
| SBVar of ident * (bool option)
| SRVar of ident * (real option)
type sim_node_st =
{
node_outputs: sim_var list;
node_loc_vars: sim_var list;
node_inner_nodes: sim_node list;
}
and sim_node_step_fn =
sim_node_st -> sim_var list -> (sim_var list * sim_node_st)
and sim_node = sim_node_st * sim_node_step_fn
let pp_sim fmt ((sn, _): sim_node) =
let rec aux fmt vars =
match vars with
| [] -> ()
| SIVar (s, None) :: t ->
Format.fprintf fmt "\t<%s : int> uninitialized yet.\n%a" s aux t
| SBVar (s, None) :: t ->
Format.fprintf fmt "\t<%s : bool> uninitialized yet.\n%a" s aux t
| SRVar (s, None) :: t ->
Format.fprintf fmt "\t<%s : real> uninitialized yet.\n%a" s aux t
| SIVar (s, Some i) :: t ->
Format.fprintf fmt "\t<%s : int> = %d\n%a" s i aux t
| SBVar (s, Some b) :: t ->
Format.fprintf fmt "\t<%s : bool> = %s\n%a" s (Bool.to_string b) aux t
| SRVar (s, Some r) :: t ->
Format.fprintf fmt "\t<%s : real> = %f\n%a" s r aux t
in
if sn.node_loc_vars <> []
then
Format.fprintf fmt "State of the simulated node:\n\
\tOutput variables:\n%a
\tLocal variables:\n%a"
aux sn.node_outputs
aux sn.node_loc_vars
else
Format.fprintf fmt "State of the simulated node:\n\
\tOutput variables:\n%a
\tThere are no local variables:\n"
aux sn.node_outputs
exception MySimulationException of string
let fetch_node (p: t_nodelist) (s: ident) : t_node =
match List.filter (fun n -> n.n_name = s) p with
| [e] -> e
| _ -> raise (MySimulationException (Format.asprintf "Node %s undefined." s))
let fetch_var (l: sim_var list) (s: ident) =
match List.filter
(function
| SBVar (v, _) | SRVar (v, _) | SIVar (v, _) -> v = s) l with
| [v] -> v
| _ -> raise (MySimulationException
(Format.asprintf "Variable %s undefined." s))
(** TODO! *)
let make_sim (main_fn: ident) (p: t_nodelist): sim_node =
let main_n = fetch_node p main_fn in
let node_outputs =
List.map
(function
| IVar s -> SIVar (s, None)
| BVar s -> SBVar (s, None)
| RVar s -> SRVar (s, None))
(snd main_n.n_outputs) in
let node_loc_vars: sim_var list =
List.map
(function
| IVar s -> SIVar (s, None)
| BVar s -> SBVar (s, None)
| RVar s -> SRVar (s, None))
(snd main_n.n_local_vars) in
let node_inner_nodes = (* TODO! *) [] in
({node_outputs = node_outputs;
node_loc_vars = node_loc_vars;
node_inner_nodes = node_inner_nodes; },
(fun s l -> (s.node_outputs, s)))
let simulate main_fn ast =
let sim_ast = make_sim main_fn ast in
Format.printf "Initial state:\n%a" pp_sim sim_ast