Merge branch 'master' of https://gitea.lemnoslife.com/Benjamin_Loison/Synchronous_reactive_systems
This commit is contained in:
commit
72ba196142
8
.gitignore
vendored
8
.gitignore
vendored
@ -1,2 +1,10 @@
|
|||||||
_build
|
_build
|
||||||
tags
|
tags
|
||||||
|
beamer.aux
|
||||||
|
beamer.log
|
||||||
|
beamer.nav
|
||||||
|
beamer.out
|
||||||
|
beamer.pdf
|
||||||
|
beamer.snm
|
||||||
|
beamer.toc
|
||||||
|
texput.log
|
||||||
|
@ -1,6 +1,5 @@
|
|||||||
\documentclass{beamer}
|
\documentclass{beamer}
|
||||||
\usepackage{tikz}
|
\usepackage{tikz}
|
||||||
%\usepackage{minted}
|
|
||||||
|
|
||||||
\usetikzlibrary{positioning}
|
\usetikzlibrary{positioning}
|
||||||
\usetheme{Darmstadt}
|
\usetheme{Darmstadt}
|
||||||
@ -43,42 +42,6 @@
|
|||||||
\centering
|
\centering
|
||||||
\includegraphics[width=.75\textwidth]{imgs/gadt.png}
|
\includegraphics[width=.75\textwidth]{imgs/gadt.png}
|
||||||
\end{figure}
|
\end{figure}
|
||||||
%type _ t_var =
|
|
||||||
% | BVar: ident -> bool t_var
|
|
||||||
% | IVar: ident -> int t_var
|
|
||||||
% | RVar: ident -> real t_var
|
|
||||||
%
|
|
||||||
%type _ t_expression =
|
|
||||||
% | EVar: 'a t_var -> 'a t_expression
|
|
||||||
% | EMonOp: monop * 'a t_expression -> 'a t_expression
|
|
||||||
% | EBinOp: binop * 'a t_expression * 'a t_expression -> 'a t_expression
|
|
||||||
% | ETriOp: triop * bool t_expression * 'a t_expression * 'a t_expression -> 'a t_expression
|
|
||||||
% | EComp: compop * 'a t_expression * 'a t_expression -> bool t_expression
|
|
||||||
% | EConst: 'a const -> 'a t_expression
|
|
||||||
% | ETuple: 'a t_expression * 'b t_expression -> ('a * 'b) t_expression
|
|
||||||
% | EApp: (('a -> 'b) t_node) * 'a t_expression -> 'b t_expression
|
|
||||||
%
|
|
||||||
%and _ t_varlist =
|
|
||||||
% | NVar: 'a t_varlist
|
|
||||||
% | CVar: 'a t_var * 'b t_varlist -> ('a * 'b) t_varlist
|
|
||||||
%
|
|
||||||
%and 'a t_equation = 'a t_varlist * 'a t_expression
|
|
||||||
%
|
|
||||||
%and _ t_eqlist =
|
|
||||||
% | NEql: unit t_eqlist
|
|
||||||
% | CEql: 'a t_equation * 'b t_eqlist -> ('a * 'b) t_eqlist
|
|
||||||
%
|
|
||||||
%and _ t_node =
|
|
||||||
% | MakeNode:
|
|
||||||
% ident
|
|
||||||
% * 'i t_varlist * 'o t_varlist
|
|
||||||
% * 'l t_varlist * 'e t_eqlist
|
|
||||||
% -> ('i -> 'o) t_node
|
|
||||||
%
|
|
||||||
%type _ t_nodelist =
|
|
||||||
% | NNode: unit t_nodelist
|
|
||||||
% | CNode: ('a -> 'b) t_node * 'c t_nodelist -> (('a -> 'b) * 'c) t_nodelist
|
|
||||||
% \end{minted}
|
|
||||||
\end{frame}
|
\end{frame}
|
||||||
\begin{frame}
|
\begin{frame}
|
||||||
\begin{block}{Pros of using GADTs}
|
\begin{block}{Pros of using GADTs}
|
||||||
@ -134,7 +97,7 @@
|
|||||||
|
|
||||||
\section{Passes}
|
\section{Passes}
|
||||||
\begin{frame}{Passes}
|
\begin{frame}{Passes}
|
||||||
\begin{block}
|
\begin{block}{Classification}
|
||||||
The passes of our compiler are functions of taking a program and either:
|
The passes of our compiler are functions of taking a program and either:
|
||||||
\begin{itemize}
|
\begin{itemize}
|
||||||
\item returning a program if the pass succeeded
|
\item returning a program if the pass succeeded
|
||||||
|
@ -69,8 +69,6 @@ and t_node =
|
|||||||
n_local_vars: t_varlist;
|
n_local_vars: t_varlist;
|
||||||
n_equations: t_eqlist;
|
n_equations: t_eqlist;
|
||||||
n_automata: t_autolist;
|
n_automata: t_autolist;
|
||||||
n_inputs_type : full_ty;
|
|
||||||
n_outputs_type : full_ty;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
type t_nodelist = t_node list
|
type t_nodelist = t_node list
|
||||||
|
28
src/main.ml
28
src/main.ml
@ -25,7 +25,8 @@ let exec_passes ast main_fn verbose debug passes f =
|
|||||||
|
|
||||||
let _ =
|
let _ =
|
||||||
(** Usage and argument parsing. *)
|
(** Usage and argument parsing. *)
|
||||||
let default_passes = ["chkvar_init_unicity"; "pre2vars"; "linearization"] in
|
let default_passes = ["pre2vars"; "linearization"; "equations_ordering"] in
|
||||||
|
let sanity_passes = ["chkvar_init_unicity"; "check_typing"] in
|
||||||
let usage_msg =
|
let usage_msg =
|
||||||
"Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \
|
"Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \
|
||||||
[-o output_file] [-m main_function] source_file\n" in
|
[-o output_file] [-m main_function] source_file\n" in
|
||||||
@ -37,10 +38,14 @@ let _ =
|
|||||||
let passes = ref [] in
|
let passes = ref [] in
|
||||||
let main_fn = ref "main" in
|
let main_fn = ref "main" in
|
||||||
let source_file = ref "" in
|
let source_file = ref "" in
|
||||||
|
let testopt = ref false in
|
||||||
let output_file = ref "out.c" in
|
let output_file = ref "out.c" in
|
||||||
let anon_fun filename = source_file := filename in
|
let anon_fun filename = source_file := filename in
|
||||||
let speclist =
|
let speclist =
|
||||||
[
|
[
|
||||||
|
("-test", Arg.Set testopt, "Runs the sanity passes not only at the \
|
||||||
|
begining of the compilation, but also after \
|
||||||
|
each pass altering the AST.");
|
||||||
("-ast", Arg.Set ppast, "Only print the AST of the input file");
|
("-ast", Arg.Set ppast, "Only print the AST of the input file");
|
||||||
("-nop", Arg.Set nopopt, "Only computes the AST and execute the passes");
|
("-nop", Arg.Set nopopt, "Only computes the AST and execute the passes");
|
||||||
("-verbose", Arg.Set verbose, "Output some debug information");
|
("-verbose", Arg.Set verbose, "Output some debug information");
|
||||||
@ -66,6 +71,8 @@ let _ =
|
|||||||
("pre2vars", Passes.pre2vars);
|
("pre2vars", Passes.pre2vars);
|
||||||
("chkvar_init_unicity", Passes.chkvar_init_unicity);
|
("chkvar_init_unicity", Passes.chkvar_init_unicity);
|
||||||
("linearization", Passes.pass_linearization);
|
("linearization", Passes.pass_linearization);
|
||||||
|
("equations_ordering", Passes.pass_eq_reordering);
|
||||||
|
("check_typing", Passes.pass_typing);
|
||||||
];
|
];
|
||||||
|
|
||||||
(** Main functionality below *)
|
(** Main functionality below *)
|
||||||
@ -99,12 +106,19 @@ let _ =
|
|||||||
end
|
end
|
||||||
in
|
in
|
||||||
|
|
||||||
let passes = List.map (fun (pass: string) -> (pass,
|
let passes =
|
||||||
match Hashtbl.find_opt passes_table pass with
|
List.map
|
||||||
| None ->
|
(fun (pass: string) -> (pass,
|
||||||
(exit_error (Format.sprintf "The pass %s does not exist.\n" pass); exit 0)
|
match Hashtbl.find_opt passes_table pass with
|
||||||
| Some f ->
|
| None ->
|
||||||
(print_debug ("The pass "^pass^" has been selected.\n"); f))) !passes in
|
(exit_error (Format.sprintf "The pass %s does not exist.\n" pass); exit 0)
|
||||||
|
| Some f ->
|
||||||
|
(print_debug ("The pass "^pass^" has been selected.\n"); f)))
|
||||||
|
(sanity_passes @
|
||||||
|
if !testopt
|
||||||
|
then List.flatten (List.map (fun p -> p :: sanity_passes) !passes)
|
||||||
|
else !passes)
|
||||||
|
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) ;
|
Pp.pp_ast ast) ;
|
||||||
|
@ -198,9 +198,7 @@ node_content:
|
|||||||
n_outputs = (t_out, e_out);
|
n_outputs = (t_out, e_out);
|
||||||
n_local_vars = $10;
|
n_local_vars = $10;
|
||||||
n_equations = eqs;
|
n_equations = eqs;
|
||||||
n_automata = aut;
|
n_automata = aut; } in
|
||||||
n_inputs_type = t_in;
|
|
||||||
n_outputs_type = t_out; } in
|
|
||||||
if Hashtbl.find_opt defined_nodes node_name <> None
|
if Hashtbl.find_opt defined_nodes node_name <> None
|
||||||
then raise (MyParsingError
|
then raise (MyParsingError
|
||||||
(Format.asprintf "The node %s is already defined."
|
(Format.asprintf "The node %s is already defined."
|
||||||
@ -386,8 +384,8 @@ expr:
|
|||||||
{ let name = $1 in
|
{ let name = $1 in
|
||||||
let node = fetch_node name in
|
let node = fetch_node name in
|
||||||
let args = $3 in
|
let args = $3 in
|
||||||
if type_exp args = node.n_inputs_type
|
if type_exp args = fst node.n_inputs
|
||||||
then EApp (node.n_outputs_type, fetch_node name, args)
|
then EApp (fst node.n_outputs, fetch_node name, args)
|
||||||
else raise (MyParsingError ("The application does not type check!",
|
else raise (MyParsingError ("The application does not type check!",
|
||||||
current_location()))
|
current_location()))
|
||||||
}
|
}
|
||||||
|
439
src/passes.ml
439
src/passes.ml
@ -2,6 +2,7 @@
|
|||||||
|
|
||||||
open Ast
|
open Ast
|
||||||
open Passes_utils
|
open Passes_utils
|
||||||
|
open Utils
|
||||||
|
|
||||||
let pre2vars verbose debug main_fn =
|
let pre2vars verbose debug main_fn =
|
||||||
let rec all_pre expr =
|
let rec all_pre expr =
|
||||||
@ -13,181 +14,285 @@ let pre2vars verbose debug main_fn =
|
|||||||
in
|
in
|
||||||
let rec pre_push expr : t_expression =
|
let rec pre_push expr : t_expression =
|
||||||
match expr with
|
match expr with
|
||||||
| EVar _ -> EMonOp (Utils.type_exp expr, MOp_pre, expr)
|
| EVar _ -> EMonOp (type_exp expr, MOp_pre, expr)
|
||||||
| EConst _ -> expr (** pre(c) = c for any constant c *)
|
| EConst _ -> expr (** pre(c) = c for any constant c *)
|
||||||
| EMonOp (ty, mop, expr) ->
|
| EMonOp (ty, mop, expr) ->
|
||||||
begin
|
begin
|
||||||
match mop with
|
match mop with
|
||||||
| MOp_pre ->
|
| MOp_pre ->
|
||||||
if all_pre expr
|
if all_pre expr
|
||||||
then EMonOp (ty, mop, EMonOp (ty, mop, expr))
|
then EMonOp (ty, mop, EMonOp (ty, mop, expr))
|
||||||
else pre_push (pre_push expr)
|
else pre_push (pre_push expr)
|
||||||
| _ -> EMonOp (ty, mop, pre_push expr)
|
| _ -> EMonOp (ty, mop, pre_push expr)
|
||||||
end
|
end
|
||||||
| EBinOp (ty, bop, expr, expr') ->
|
| EBinOp (ty, bop, expr, expr') ->
|
||||||
let expr = pre_push expr in let expr' = pre_push expr' in
|
let expr = pre_push expr in let expr' = pre_push expr' in
|
||||||
EBinOp (ty, bop, expr, expr')
|
EBinOp (ty, bop, expr, expr')
|
||||||
| ETriOp (ty, top, expr, expr', expr'') ->
|
| ETriOp (ty, top, expr, expr', expr'') ->
|
||||||
let expr = pre_push expr in let expr' = pre_push expr' in
|
let expr = pre_push expr in let expr' = pre_push expr' in
|
||||||
let expr'' = pre_push expr'' in
|
let expr'' = pre_push expr'' in
|
||||||
ETriOp (ty, top, expr, expr', expr'')
|
ETriOp (ty, top, expr, expr', expr'')
|
||||||
| EComp (ty, cop, expr, expr') ->
|
| EComp (ty, cop, expr, expr') ->
|
||||||
let expr = pre_push expr in let expr' = pre_push expr' in
|
let expr = pre_push expr in let expr' = pre_push expr' in
|
||||||
EComp (ty, cop, expr, expr')
|
EComp (ty, cop, expr, expr')
|
||||||
| EWhen (ty, expr, expr') ->
|
| EWhen (ty, expr, expr') ->
|
||||||
let expr = pre_push expr in let expr' = pre_push expr' in
|
let expr = pre_push expr in let expr' = pre_push expr' in
|
||||||
EWhen (ty, expr, expr')
|
EWhen (ty, expr, expr')
|
||||||
| EReset (ty, expr, expr') ->
|
| EReset (ty, expr, expr') ->
|
||||||
let expr = pre_push expr in let expr' = pre_push expr' in
|
let expr = pre_push expr in let expr' = pre_push expr' in
|
||||||
EReset (ty, expr, expr')
|
EReset (ty, expr, expr')
|
||||||
| ETuple (ty, elist) ->
|
| ETuple (ty, elist) ->
|
||||||
let elist =
|
let elist =
|
||||||
List.fold_right (fun expr acc -> (pre_push expr) :: acc) elist [] in
|
List.fold_right (fun expr acc -> (pre_push expr) :: acc) elist [] in
|
||||||
ETuple (ty, elist)
|
ETuple (ty, elist)
|
||||||
| EApp (ty, node, arg) ->
|
| EApp (ty, node, arg) ->
|
||||||
let arg = pre_push arg in
|
let arg = pre_push arg in
|
||||||
EApp (ty, node, arg)
|
EApp (ty, node, arg)
|
||||||
in
|
in
|
||||||
let rec aux (expr: t_expression) =
|
let rec aux (expr: t_expression) =
|
||||||
match expr with
|
match expr with
|
||||||
| EVar _ -> expr
|
| EVar _ -> expr
|
||||||
| EMonOp (ty, mop, expr) ->
|
| EMonOp (ty, mop, expr) ->
|
||||||
begin
|
begin
|
||||||
match mop with
|
match mop with
|
||||||
| MOp_pre -> pre_push expr
|
| MOp_pre -> pre_push expr
|
||||||
| _ -> let expr = aux expr in EMonOp (ty, mop, expr)
|
| _ -> let expr = aux expr in EMonOp (ty, mop, expr)
|
||||||
end
|
end
|
||||||
| EBinOp (ty, bop, expr, expr') ->
|
| EBinOp (ty, bop, expr, expr') ->
|
||||||
let expr = aux expr in let expr' = aux expr' in
|
let expr = aux expr in let expr' = aux expr' in
|
||||||
EBinOp (ty, bop, expr, expr')
|
EBinOp (ty, bop, expr, expr')
|
||||||
| ETriOp (ty, top, expr, expr', expr'') ->
|
| ETriOp (ty, top, expr, expr', expr'') ->
|
||||||
let expr = aux expr in let expr' = aux expr' in
|
let expr = aux expr in let expr' = aux expr' in
|
||||||
let expr'' = aux expr'' in
|
let expr'' = aux expr'' in
|
||||||
ETriOp (ty, top, expr, expr', expr'')
|
ETriOp (ty, top, expr, expr', expr'')
|
||||||
| EComp (ty, cop, expr, expr') ->
|
| EComp (ty, cop, expr, expr') ->
|
||||||
let expr = aux expr in let expr' = aux expr' in
|
let expr = aux expr in let expr' = aux expr' in
|
||||||
EComp (ty, cop, expr, expr')
|
EComp (ty, cop, expr, expr')
|
||||||
| EWhen (ty, expr, expr') ->
|
| EWhen (ty, expr, expr') ->
|
||||||
let expr = aux expr in let expr' = aux expr' in
|
let expr = aux expr in let expr' = aux expr' in
|
||||||
EWhen (ty, expr, expr')
|
EWhen (ty, expr, expr')
|
||||||
| EReset (ty, expr, expr') ->
|
| EReset (ty, expr, expr') ->
|
||||||
let expr = aux expr in let expr' = aux expr' in
|
let expr = aux expr in let expr' = aux expr' in
|
||||||
EReset (ty, expr, expr')
|
EReset (ty, expr, expr')
|
||||||
| EConst (ty, c) -> EConst (ty, c)
|
| EConst (ty, c) -> EConst (ty, c)
|
||||||
| ETuple (ty, elist) ->
|
| ETuple (ty, elist) ->
|
||||||
let elist =
|
let elist =
|
||||||
List.fold_right (fun expr acc -> (aux expr) :: acc) elist [] in
|
List.fold_right (fun expr acc -> (aux expr) :: acc) elist [] in
|
||||||
ETuple (ty, elist)
|
ETuple (ty, elist)
|
||||||
| EApp (ty, node, arg) ->
|
| EApp (ty, node, arg) ->
|
||||||
let arg = aux arg in
|
let arg = aux arg in
|
||||||
EApp (ty, node, arg)
|
EApp (ty, node, arg)
|
||||||
in
|
in
|
||||||
expression_pass (Utils.somify aux)
|
expression_pass (somify aux)
|
||||||
|
|
||||||
let chkvar_init_unicity verbose debug main_fn : t_nodelist -> t_nodelist option =
|
let chkvar_init_unicity verbose debug main_fn : t_nodelist -> t_nodelist option =
|
||||||
let aux (node: t_node) : t_node option =
|
let aux (node: t_node) : t_node option =
|
||||||
let incr_aux h n =
|
let incr_aux h n =
|
||||||
match Hashtbl.find_opt h n with
|
match Hashtbl.find_opt h n with
|
||||||
| None -> failwith "todo, should not happend."
|
| None -> failwith "todo, should not happend."
|
||||||
| Some num -> Hashtbl.replace h n (num + 1)
|
| Some num -> Hashtbl.replace h n (num + 1)
|
||||||
in
|
|
||||||
let incr_eq h (((_, patt), _): t_equation) =
|
|
||||||
List.iter (fun v -> incr_aux h (Utils.name_of_var v)) patt
|
|
||||||
in
|
|
||||||
let rec incr_eqlist h = function
|
|
||||||
| [] -> ()
|
|
||||||
| eq :: eqs -> (incr_eq h eq; incr_eqlist h eqs)
|
|
||||||
in
|
|
||||||
let incr_branch h (State (_, eqs, _, _): t_state) = incr_eqlist h eqs in
|
|
||||||
let incr_automata h ((_, states): t_automaton) =
|
|
||||||
let acc = Hashtbl.copy h in
|
|
||||||
List.iter
|
|
||||||
(fun st ->
|
|
||||||
let h_st = Hashtbl.copy h in
|
|
||||||
incr_branch h_st st;
|
|
||||||
Hashtbl.iter
|
|
||||||
(fun varname num' ->
|
|
||||||
match Hashtbl.find_opt acc varname with
|
|
||||||
| None -> failwith "non!"
|
|
||||||
| Some num -> Hashtbl.replace acc varname (Int.max num num')
|
|
||||||
) h_st) states;
|
|
||||||
Hashtbl.iter (fun v n -> Hashtbl.replace h v n) acc
|
|
||||||
in
|
|
||||||
let check_now h : bool=
|
|
||||||
Hashtbl.fold
|
|
||||||
(fun varname num old_res ->
|
|
||||||
if num > 1
|
|
||||||
then (verbose (Format.asprintf "%s initialized twice!" varname); false)
|
|
||||||
else old_res) h true
|
|
||||||
in
|
|
||||||
(*let purge_initialized h =
|
|
||||||
Hashtbl.iter
|
|
||||||
(fun varname num ->
|
|
||||||
if num > 0
|
|
||||||
then (verbose (Format.asprintf "Purging %s" varname); Hashtbl.remove h varname)
|
|
||||||
else ()) h
|
|
||||||
in*)
|
|
||||||
let h = Hashtbl.create Config.maxvar in
|
|
||||||
let add_var n v =
|
|
||||||
match v with
|
|
||||||
| IVar s -> Hashtbl.add h s n
|
|
||||||
| BVar s -> Hashtbl.add h s n
|
|
||||||
| RVar s -> Hashtbl.add h s n
|
|
||||||
in
|
in
|
||||||
let add_var_in = add_var 1 in
|
let incr_eq h (((_, patt), _): t_equation) =
|
||||||
let add_var_loc = add_var 0 in
|
List.iter (fun v -> incr_aux h (name_of_var v)) patt
|
||||||
List.iter add_var_in (snd node.n_inputs);
|
in
|
||||||
List.iter add_var_loc (snd node.n_outputs);
|
let rec incr_eqlist h = function
|
||||||
List.iter add_var_loc (snd node.n_local_vars);
|
| [] -> ()
|
||||||
(** Usual Equations *)
|
| eq :: eqs -> (incr_eq h eq; incr_eqlist h eqs)
|
||||||
incr_eqlist h node.n_equations;
|
in
|
||||||
if check_now h = false
|
let incr_branch h (State (_, eqs, _, _): t_state) = incr_eqlist h eqs in
|
||||||
then None
|
let incr_automata h ((_, states): t_automaton) =
|
||||||
else
|
let acc = Hashtbl.copy h in
|
||||||
begin
|
List.iter
|
||||||
List.iter (* 0. *) (incr_automata h) node.n_automata;
|
(fun st ->
|
||||||
if check_now h
|
let h_st = Hashtbl.copy h in
|
||||||
then Some node
|
incr_branch h_st st;
|
||||||
else None
|
Hashtbl.iter
|
||||||
end
|
(fun varname num' ->
|
||||||
(** never purge -> failwith never executed! purge_initialized h; *)
|
match Hashtbl.find_opt acc varname with
|
||||||
|
| None -> failwith "non!"
|
||||||
|
| Some num -> Hashtbl.replace acc varname (Int.max num num')
|
||||||
|
) h_st) states;
|
||||||
|
Hashtbl.iter (fun v n -> Hashtbl.replace h v n) acc
|
||||||
|
in
|
||||||
|
let check_now h : bool=
|
||||||
|
Hashtbl.fold
|
||||||
|
(fun varname num old_res ->
|
||||||
|
if num > 1
|
||||||
|
then (verbose (Format.asprintf "%s initialized twice!" varname); false)
|
||||||
|
else old_res) h true
|
||||||
|
in
|
||||||
|
(*let purge_initialized h =
|
||||||
|
Hashtbl.iter
|
||||||
|
(fun varname num ->
|
||||||
|
if num > 0
|
||||||
|
then (verbose (Format.asprintf "Purging %s" varname); Hashtbl.remove h varname)
|
||||||
|
else ()) h
|
||||||
|
in*)
|
||||||
|
let h = Hashtbl.create Config.maxvar in
|
||||||
|
let add_var n v =
|
||||||
|
match v with
|
||||||
|
| IVar s -> Hashtbl.add h s n
|
||||||
|
| BVar s -> Hashtbl.add h s n
|
||||||
|
| RVar s -> Hashtbl.add h s n
|
||||||
in
|
in
|
||||||
node_pass aux
|
let add_var_in = add_var 1 in
|
||||||
|
let add_var_loc = add_var 0 in
|
||||||
|
List.iter add_var_in (snd node.n_inputs);
|
||||||
|
List.iter add_var_loc (snd node.n_outputs);
|
||||||
|
List.iter add_var_loc (snd node.n_local_vars);
|
||||||
|
(** Usual Equations *)
|
||||||
|
incr_eqlist h node.n_equations;
|
||||||
|
if check_now h = false
|
||||||
|
then None
|
||||||
|
else
|
||||||
|
begin
|
||||||
|
List.iter (* 0. *) (incr_automata h) node.n_automata;
|
||||||
|
if check_now h
|
||||||
|
then Some node
|
||||||
|
else None
|
||||||
|
end
|
||||||
|
(** never purge -> failwith never executed! purge_initialized h; *)
|
||||||
|
in
|
||||||
|
node_pass aux
|
||||||
|
|
||||||
let pass_linearization verbose debug main_fn =
|
let pass_linearization verbose debug main_fn =
|
||||||
let node_lin (node: t_node): t_node option =
|
let node_lin (node: t_node): t_node option =
|
||||||
let rec tpl ((pat, exp): t_equation) =
|
let rec tpl ((pat, exp): t_equation) =
|
||||||
match exp with
|
match exp with
|
||||||
| ETuple (_, hexps :: texps) ->
|
| ETuple (_, hexps :: texps) ->
|
||||||
let p1, p2 =
|
debug "An ETuple has been recognized, inlining...";
|
||||||
Utils.list_select
|
let p1, p2 =
|
||||||
(List.length (Utils.type_exp hexps))
|
list_select
|
||||||
(snd pat) in
|
(List.length (type_exp hexps))
|
||||||
let t1 = List.flatten (List.map Utils.type_var p1) in
|
(snd pat) in
|
||||||
let t2 = List.flatten (List.map Utils.type_var p2) in
|
let t1 = List.flatten (List.map type_var p1) in
|
||||||
((t1, p1), hexps)
|
let t2 = List.flatten (List.map type_var p2) in
|
||||||
:: (tpl ((t2, p2),
|
((t1, p1), hexps)
|
||||||
ETuple (List.flatten (List.map Utils.type_exp texps), texps)))
|
:: (tpl ((t2, p2),
|
||||||
| ETuple (_, []) -> []
|
ETuple (List.flatten (List.map type_exp texps), texps)))
|
||||||
| _ -> [(pat, exp)]
|
| ETuple (_, []) -> []
|
||||||
in
|
| _ -> [(pat, exp)]
|
||||||
let new_locvars = node.n_local_vars in
|
|
||||||
let new_equations = List.flatten
|
|
||||||
begin
|
|
||||||
List.map
|
|
||||||
tpl
|
|
||||||
node.n_equations
|
|
||||||
end in
|
|
||||||
Some
|
|
||||||
{
|
|
||||||
n_name = node.n_name;
|
|
||||||
n_inputs = node.n_inputs;
|
|
||||||
n_outputs = node.n_outputs;
|
|
||||||
n_local_vars = new_locvars;
|
|
||||||
n_equations = new_equations;
|
|
||||||
n_automata = node.n_automata;
|
|
||||||
n_inputs_type = node.n_inputs_type;
|
|
||||||
n_outputs_type = node.n_outputs_type;
|
|
||||||
}
|
|
||||||
in
|
in
|
||||||
node_pass node_lin
|
let new_locvars = node.n_local_vars in
|
||||||
|
let new_equations = List.flatten
|
||||||
|
begin
|
||||||
|
List.map
|
||||||
|
tpl
|
||||||
|
node.n_equations
|
||||||
|
end in
|
||||||
|
Some
|
||||||
|
{
|
||||||
|
n_name = node.n_name;
|
||||||
|
n_inputs = node.n_inputs;
|
||||||
|
n_outputs = node.n_outputs;
|
||||||
|
n_local_vars = new_locvars;
|
||||||
|
n_equations = new_equations;
|
||||||
|
n_automata = node.n_automata;
|
||||||
|
}
|
||||||
|
in
|
||||||
|
node_pass node_lin
|
||||||
|
|
||||||
|
let pass_eq_reordering verbose debug main_fn ast =
|
||||||
|
let rec pick_equations init_vars eqs remaining_equations =
|
||||||
|
match remaining_equations with
|
||||||
|
| [] -> Some eqs
|
||||||
|
| _ ->
|
||||||
|
begin
|
||||||
|
match List.filter
|
||||||
|
(fun (patt, expr) ->
|
||||||
|
List.for_all
|
||||||
|
(fun v -> List.mem v init_vars)
|
||||||
|
(vars_of_expr expr))
|
||||||
|
remaining_equations with
|
||||||
|
| [] -> raise (PassExn "[equation ordering] The equations cannot be ordered.")
|
||||||
|
| h :: t ->
|
||||||
|
let init_vars =
|
||||||
|
List.fold_left
|
||||||
|
(fun acc vs ->
|
||||||
|
acc @ (vars_of_patt (fst vs))) init_vars (h :: t) in
|
||||||
|
pick_equations init_vars (eqs@(h :: t))
|
||||||
|
(List.filter (fun eq -> List.for_all (fun e -> eq <> e) (h :: t)) remaining_equations)
|
||||||
|
end
|
||||||
|
in
|
||||||
|
let node_eq_reorganising (node: t_node): t_node option =
|
||||||
|
let init_vars = List.map name_of_var (snd node.n_inputs) in
|
||||||
|
try
|
||||||
|
begin
|
||||||
|
match pick_equations init_vars [] node.n_equations with
|
||||||
|
| None -> None
|
||||||
|
| Some eqs -> Some { node with n_equations = eqs }
|
||||||
|
end
|
||||||
|
with PassExn err -> (verbose err; None)
|
||||||
|
in
|
||||||
|
node_pass node_eq_reorganising ast
|
||||||
|
|
||||||
|
let pass_typing verbose debug main_fn ast =
|
||||||
|
let htbl = Hashtbl.create (List.length ast) in
|
||||||
|
let () = debug "[typing verification]" in
|
||||||
|
let () = List.iter
|
||||||
|
(fun n -> Hashtbl.add htbl n.n_name (fst n.n_inputs, fst n.n_outputs))
|
||||||
|
ast in
|
||||||
|
let rec check_varlist vl =
|
||||||
|
let t = fst vl in
|
||||||
|
let l = snd vl in
|
||||||
|
match t, l with
|
||||||
|
| [], [] -> true
|
||||||
|
| TInt :: t, IVar _ :: l -> check_varlist (t, l)
|
||||||
|
| TBool :: t, BVar _ :: l -> check_varlist (t, l)
|
||||||
|
| TReal :: t, RVar _ :: l -> check_varlist (t, l)
|
||||||
|
| _, _ -> false
|
||||||
|
in
|
||||||
|
let rec check_expr vl = function
|
||||||
|
| EVar (t, v) -> t = type_var v
|
||||||
|
| EMonOp (t, _, e) -> check_expr vl e && type_exp e = t
|
||||||
|
| EBinOp (t, _, e, e') -> check_expr vl e && check_expr vl e'
|
||||||
|
&& t = type_exp e && t = type_exp e'
|
||||||
|
| ETriOp (t, _, c, e, e') ->
|
||||||
|
check_expr vl e && check_expr vl e' && check_expr vl c
|
||||||
|
&& type_exp c = [TBool] && type_exp e = t && type_exp e' = t
|
||||||
|
| EComp (t, _, e, e') ->
|
||||||
|
check_expr vl e && check_expr vl e' && t = [TBool]
|
||||||
|
| EWhen (t, e, e') ->
|
||||||
|
check_expr vl e && check_expr vl e'
|
||||||
|
&& t = type_exp e && [TBool] = type_exp e'
|
||||||
|
| EReset (t, e, e') ->
|
||||||
|
check_expr vl e && check_expr vl e' && t = type_exp e && type_exp e' = [TBool]
|
||||||
|
| EConst (t, c) -> type_const c = t
|
||||||
|
| ETuple (t, l) ->
|
||||||
|
List.for_all (check_expr vl) l
|
||||||
|
&& t = List.flatten (List.map type_exp l)
|
||||||
|
| EApp (t, n, e) ->
|
||||||
|
check_expr vl e && t = (fst n.n_outputs) && type_exp e = (fst n.n_inputs)
|
||||||
|
in
|
||||||
|
let check_equation vl ((peq, eeq): t_equation) =
|
||||||
|
if check_varlist peq
|
||||||
|
then
|
||||||
|
if check_expr vl eeq
|
||||||
|
then fst peq = type_exp eeq
|
||||||
|
else false
|
||||||
|
else false
|
||||||
|
in
|
||||||
|
let rec check_equations vl = function
|
||||||
|
| [] -> true
|
||||||
|
| eq :: eqs ->
|
||||||
|
if check_equation vl eq
|
||||||
|
then check_equations vl eqs
|
||||||
|
else false
|
||||||
|
in
|
||||||
|
let check_one_node node =
|
||||||
|
check_varlist (node.n_inputs)
|
||||||
|
&& check_varlist (node.n_outputs)
|
||||||
|
&& check_varlist (node.n_local_vars)
|
||||||
|
&& check_equations
|
||||||
|
(varlist_concat node.n_inputs
|
||||||
|
(varlist_concat node.n_outputs node.n_local_vars))
|
||||||
|
node.n_equations
|
||||||
|
in
|
||||||
|
let rec aux = function
|
||||||
|
| [] -> Some ast
|
||||||
|
| n :: nodes ->
|
||||||
|
if check_one_node n
|
||||||
|
then aux nodes
|
||||||
|
else None
|
||||||
|
in aux ast
|
||||||
|
|
||||||
|
@ -18,8 +18,6 @@ let equation_pass (f: t_equation -> t_equation option) ast: t_nodelist option =
|
|||||||
n_local_vars = node.n_local_vars;
|
n_local_vars = node.n_local_vars;
|
||||||
n_equations = eqs;
|
n_equations = eqs;
|
||||||
n_automata = node.n_automata;
|
n_automata = node.n_automata;
|
||||||
n_inputs_type = node.n_inputs_type;
|
|
||||||
n_outputs_type = node.n_outputs_type;
|
|
||||||
}
|
}
|
||||||
in
|
in
|
||||||
node_pass aux ast
|
node_pass aux ast
|
||||||
@ -31,3 +29,5 @@ let expression_pass f: t_nodelist -> t_nodelist option =
|
|||||||
| Some expr -> Some (patt, expr)
|
| Some expr -> Some (patt, expr)
|
||||||
in
|
in
|
||||||
equation_pass aux
|
equation_pass aux
|
||||||
|
|
||||||
|
exception PassExn of string
|
||||||
|
@ -136,7 +136,8 @@ let pp_expression =
|
|||||||
let rec pp_equations fmt: t_eqlist -> unit = function
|
let rec pp_equations fmt: t_eqlist -> unit = function
|
||||||
| [] -> ()
|
| [] -> ()
|
||||||
| (patt, expr) :: eqs ->
|
| (patt, expr) :: eqs ->
|
||||||
Format.fprintf fmt "\t\t∗ Equation of type : %a\n\t\t left side: %a\n\t\t right side:\n%a\n%a"
|
Format.fprintf fmt "\t\t∗ Equation of type : %a\n\t\t left side: %a\n\
|
||||||
|
\t\t right side:\n%a\n\n%a"
|
||||||
debug_type_pp (Utils.type_exp expr)
|
debug_type_pp (Utils.type_exp expr)
|
||||||
pp_varlist patt
|
pp_varlist patt
|
||||||
pp_expression expr
|
pp_expression expr
|
||||||
|
@ -1,4 +1,5 @@
|
|||||||
node diagonal_int (i: int) returns (o1, o2 : int);
|
node diagonal_int (i: int) returns (o1, o2 : int);
|
||||||
|
let i: int;
|
||||||
let
|
let
|
||||||
(o1, o2) = (i, i);
|
(o1, o2) = (i, i);
|
||||||
tel
|
tel
|
||||||
|
@ -1,4 +1,7 @@
|
|||||||
node diagonal_int (i: int) returns (o1, o2 : int);
|
node diagonal_int (i: int) returns (o1, o2 : int);
|
||||||
|
var y: int;
|
||||||
let
|
let
|
||||||
(o1, o2) = (i, i);
|
o2 = y;
|
||||||
|
y = i;
|
||||||
|
o1 = i;
|
||||||
tel
|
tel
|
||||||
|
27
src/utils.ml
27
src/utils.ml
@ -22,7 +22,12 @@ let rec list_chk v = function
|
|||||||
| [] -> false
|
| [] -> false
|
||||||
| h :: t -> if h = v then true else list_chk v t
|
| h :: t -> if h = v then true else list_chk v t
|
||||||
|
|
||||||
exception MyParsingError of (string * Ast.location)
|
exception MyParsingError of (string * location)
|
||||||
|
|
||||||
|
let type_const = function
|
||||||
|
| CReal _ -> [TReal]
|
||||||
|
| CInt _ -> [TInt ]
|
||||||
|
| CBool _ -> [TBool]
|
||||||
|
|
||||||
let type_var (v: t_var) =
|
let type_var (v: t_var) =
|
||||||
match v with
|
match v with
|
||||||
@ -60,3 +65,23 @@ let rec fresh_var_name (l: t_varlist) n : ident =
|
|||||||
if List.filter (fun v -> name_of_var v = name) (snd l) = []
|
if List.filter (fun v -> name_of_var v = name) (snd l) = []
|
||||||
then name
|
then name
|
||||||
else fresh_var_name l n
|
else fresh_var_name l n
|
||||||
|
|
||||||
|
let vars_of_patt patt = List.map name_of_var (snd patt)
|
||||||
|
|
||||||
|
let rec vars_of_expr (expr: t_expression) : ident list =
|
||||||
|
match expr with
|
||||||
|
| EConst _ -> []
|
||||||
|
| EVar (_, v) -> [name_of_var v]
|
||||||
|
(** pre (e) does not rely on anything in this round *)
|
||||||
|
| EMonOp (_, MOp_pre, _) -> []
|
||||||
|
| EApp (_, _, e) | EMonOp (_, _, e) -> vars_of_expr e
|
||||||
|
| EComp (_, _, e, e') | EReset (_, e, e') | EBinOp (_, _, e, e')
|
||||||
|
| EWhen (_, e, e') ->
|
||||||
|
(vars_of_expr e) @ (vars_of_expr e')
|
||||||
|
| ETriOp (_, _, e, e', e'') ->
|
||||||
|
(vars_of_expr e) @ (vars_of_expr e') @ (vars_of_expr e'')
|
||||||
|
| ETuple (_, l) -> List.flatten (List.map vars_of_expr l)
|
||||||
|
|
||||||
|
let rec varlist_concat (l1: t_varlist) (l2: t_varlist): t_varlist =
|
||||||
|
(fst l1 @ fst l2, snd l1 @ snd l2)
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user