Compare commits
172 Commits
3c811c6128
...
master
Author | SHA1 | Date | |
---|---|---|---|
0349304632 | |||
|
66de13fff2 | ||
|
17e2f93629 | ||
b0545a2733 | |||
1297835bda | |||
|
a5f8c720f4 | ||
|
ad4f5e7962 | ||
|
2da1fac66f | ||
|
ad74146396 | ||
|
2f0b9a572e | ||
|
42cbc6ddaf | ||
|
23e234732f | ||
|
ad97c6b627 | ||
68d67bb53b | |||
|
b2aa8bc6d5 | ||
|
094f403f5f | ||
|
30f9c71294 | ||
|
fef64987de | ||
b168161b4f | |||
|
f8c673632e | ||
69e84f0a8e | |||
5cabb042fc | |||
|
ff9da14379 | ||
9d7588f103 | |||
|
8c3e3d1eac | ||
|
a673c447e3 | ||
|
03def2ce1a | ||
|
ffa8918330 | ||
|
24108925fd | ||
fd95446636 | |||
19524ea99c | |||
88c145a527 | |||
|
52092b1480 | ||
|
f121f55432 | ||
|
42536df81c | ||
|
c7edb27fb0 | ||
|
3ad133344a | ||
4303dcd0e4 | |||
|
f5daae824c | ||
9fbdb7000f | |||
e1de3e6829 | |||
657fe7e6fa | |||
|
91ff654fc9 | ||
025d25a146 | |||
10838d3f2d | |||
e63123d8f6 | |||
|
01d4a08e8a | ||
|
9483f7df5e | ||
9a0bfd468c | |||
609870755c | |||
|
906a3d948b | ||
|
249ac37934 | ||
|
1d39173e94 | ||
|
4ff193759b | ||
|
c52dce6c02 | ||
|
c344f125e5 | ||
|
aa7f7514d3 | ||
|
77c865e360 | ||
ade62ba678 | |||
02130cf57c | |||
273a868162 | |||
37dfcdda35 | |||
c3a64a2bae | |||
|
1491e279f7 | ||
|
ce686f6c9a | ||
|
1d4e1820e4 | ||
|
007c5b2862 | ||
|
243e8f245a | ||
|
791af71913 | ||
|
233b385608 | ||
|
7a32d474d4 | ||
|
cbc834b32a | ||
|
a877501cca | ||
|
3cbfaeb2a8 | ||
|
916c7f544b | ||
|
6291957be5 | ||
|
bb99a5882b | ||
|
0da0f58b22 | ||
|
fa052f70e2 | ||
0175749296 | |||
|
4054da7d47 | ||
|
fc0a12fa12 | ||
edfec42738 | |||
d06fccf36b | |||
b616bad07a | |||
7a0f54f291 | |||
dbf1583ffd | |||
9e96697991 | |||
|
aa84a07902 | ||
|
ed54fd0114 | ||
|
b69b6998ec | ||
73b753bec2 | |||
a0383dbf13 | |||
530f6ddf51 | |||
|
57dd9c1aa4 | ||
21414e6461 | |||
c37e819f1a | |||
ea94bb84dd | |||
|
3fa0f92233 | ||
|
3417d75620 | ||
f55cd56fde | |||
012131e035 | |||
b58b250532 | |||
78e096d2f4 | |||
621658e177 | |||
85ecea0b9e | |||
7c2c43fe24 | |||
|
c7a97f3305 | ||
|
8d6349dd3f | ||
|
d7f0f148e9 | ||
|
9987922e0f | ||
|
6af9ddf394 | ||
|
1b3af051b3 | ||
b4ae058bf6 | |||
0c8da12afe | |||
|
21d2d0c9bb | ||
|
de294df84a | ||
bfca80bb8b | |||
|
74f8a3c3e1 | ||
|
0d5e045671 | ||
|
97c6020414 | ||
bc8c752649 | |||
|
eceeb3c157 | ||
ca271eaf66 | |||
72ba196142 | |||
1a06fc9a6a | |||
|
8582337774 | ||
|
db5c584435 | ||
|
6459c54159 | ||
|
9151a6e29a | ||
|
19fd3bc1b9 | ||
|
38a7325097 | ||
342aba4426 | |||
|
e84a6e387d | ||
|
ed5f94f821 | ||
|
e75d525a6d | ||
|
73d5ed7726 | ||
|
79f0c7d223 | ||
|
f3416582be | ||
c441f8b1a6 | |||
|
b4cc3ae756 | ||
|
e5ac9a719d | ||
|
69b963c305 | ||
|
bb017afe39 | ||
|
ad1f529863 | ||
|
51ed84504f | ||
|
e9d586dfe7 | ||
|
c4ad75e4cb | ||
|
19be2200f3 | ||
|
8ef4d035a3 | ||
|
ef0effeb1f | ||
298e88f1a5 | |||
014110791d | |||
cbddd63927 | |||
241f3dcbc0 | |||
c0c29e1df7 | |||
da823ac3c8 | |||
38f58f7558 | |||
eac8c6893c | |||
363f5043a0 | |||
5a54f897b1 | |||
ac1eea42e9 | |||
a44c9288f5 | |||
b2e3ec4dd8 | |||
a8e89854a4 | |||
|
54d806f149 | ||
|
5551237414 | ||
45d64f6960 | |||
dcf7320c0d | |||
97930ba85c | |||
|
8775edc6fc | ||
a17b3c6fdd |
8
.gitignore
vendored
8
.gitignore
vendored
@@ -1,2 +1,10 @@
|
||||
_build
|
||||
tags
|
||||
beamer.aux
|
||||
beamer.log
|
||||
beamer.nav
|
||||
beamer.out
|
||||
beamer.pdf
|
||||
beamer.snm
|
||||
beamer.toc
|
||||
texput.log
|
||||
|
8
TODO
8
TODO
@@ -1,8 +0,0 @@
|
||||
# Parseur
|
||||
|
||||
- tests divers et variés
|
||||
- support pour un point-virgule optionel en fin de nœud
|
||||
- ajout des flottants (= réels)
|
||||
- ajout de pre, ->, fby, automates
|
||||
|
||||
# ...
|
247
beamer/beamer.tex
Normal file
247
beamer/beamer.tex
Normal file
@@ -0,0 +1,247 @@
|
||||
\documentclass{beamer}
|
||||
\usepackage{listings}
|
||||
\lstset{
|
||||
basicstyle=\ttfamily,
|
||||
columns=fullflexible,
|
||||
frame=single,
|
||||
breaklines=true,
|
||||
}
|
||||
\usepackage{tikz}
|
||||
|
||||
\usetikzlibrary{positioning}
|
||||
\usetheme{Darmstadt}
|
||||
|
||||
\begin{document}
|
||||
|
||||
\title{Presentation of our Lustre-to-C compiler}
|
||||
\subtitle{github.com/Benjamin-Loison/Synchronous-reactive-systems}
|
||||
\date{16 December 2022}
|
||||
\author{Benjamin Loison, Arnaud Daby-Seesaram, Antoine Grimod}
|
||||
|
||||
\frame{\titlepage}
|
||||
|
||||
\section{Structure of the compiler}
|
||||
\begin{frame}{Main ideas}
|
||||
\begin{figure}
|
||||
\begin{tikzpicture}
|
||||
\node (sf) {Source file};
|
||||
\node[right =2cm of sf] (ast) {Typed AST};
|
||||
\node[right =2cm of ast] (C) {C program};
|
||||
\draw
|
||||
(sf) edge[->] node[above] {parser} (ast)
|
||||
(ast) edge[->] node[above] {compiler} (C);
|
||||
\end{tikzpicture}
|
||||
\caption{Structure of the compiler}
|
||||
\end{figure}
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}{Testing}
|
||||
\begin{block}{Passes}
|
||||
The passes can be split into:
|
||||
\begin{itemize}
|
||||
\item those checking the program validity
|
||||
\item those modifying the AST of the program
|
||||
\end{itemize}
|
||||
\end{block}
|
||||
\end{frame}
|
||||
|
||||
\section{Typed AST}
|
||||
\subsection{First attempt using GADTs}
|
||||
\begin{frame}
|
||||
\begin{block}{Main idea}
|
||||
Using GADTs to represent nodes and expressions allows to ensure the
|
||||
well-typedness of a program.
|
||||
\end{block}
|
||||
\begin{figure}
|
||||
\centering
|
||||
\includegraphics[width=.75\textwidth]{imgs/gadt.png}
|
||||
\end{figure}
|
||||
\end{frame}
|
||||
\begin{frame}
|
||||
\begin{block}{Pros of using GADTs}
|
||||
\begin{itemize}
|
||||
\item Any term of the GADT represents a well-typed program
|
||||
\item Extending the language to support more types consists of adding
|
||||
constructors to variables and constants
|
||||
\item The types are easy to read and understand
|
||||
\end{itemize}
|
||||
\end {block}
|
||||
|
||||
\begin{block}{Cons of using GADTs}
|
||||
\begin{itemize}
|
||||
\item
|
||||
They cannot be dynamically generated (hence it is impossible to
|
||||
implement a parser that gives back a GADT)
|
||||
\item
|
||||
One should think about the isomorphism between
|
||||
\texttt{a $\ast$ (b $\ast$ c)} and \texttt{(a $\ast$ b) $\ast$ c}.
|
||||
\end{itemize}
|
||||
\end{block}
|
||||
\end{frame}
|
||||
|
||||
\subsection{Second attempt: using explicit types in the variables, expressions,
|
||||
\dots{} constructors}
|
||||
\begin{frame}
|
||||
\begin{block}{Idea}
|
||||
Explicitly collect typing information while parsing.
|
||||
\end{block}
|
||||
\begin{figure}
|
||||
\centering
|
||||
\includegraphics[width=.6\textwidth]{imgs/explicit_types.png}
|
||||
\end{figure}
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}
|
||||
\begin{block}{Pros of using explicit types}
|
||||
\begin{itemize}
|
||||
\item Programs can be built dynamically, hence a parser can be
|
||||
written
|
||||
\item While parsing, the parser has all the required information on
|
||||
the sub-variables/nodes/expressions to check the well-typedness
|
||||
\end{itemize}
|
||||
\end{block}
|
||||
\begin{block}{Cons of these definitions}
|
||||
\begin{itemize}
|
||||
\item The typing information on terms is very redundant.
|
||||
\item The rejection of ill-typed programs depends on the correctness
|
||||
of the parser
|
||||
\end{itemize}
|
||||
\end{block}
|
||||
\end{frame}
|
||||
|
||||
\section{Passes}
|
||||
\begin{frame}{}
|
||||
\begin{block}{Classification}
|
||||
\begin{itemize}
|
||||
\item node-passes: for all nodes, do \texttt{P: t\_node -> t\_node
|
||||
option}
|
||||
\pause
|
||||
\item equation-passes: for all equations of all nodes, do
|
||||
\texttt{P: t\_equation -> t\_equation option}
|
||||
(the definition uses the node-passes constructor)
|
||||
\pause
|
||||
\item expression-passes: for all expression of all equations, do
|
||||
\texttt{P: t\_expression -> t\_expression option}
|
||||
(the definition uses the equation-passes constructor)
|
||||
\end{itemize}
|
||||
\end{block}
|
||||
\end{frame}
|
||||
\begin{frame}{Implemented Passes}
|
||||
\begin{block}{Sanity checks}
|
||||
\begin{itemize}
|
||||
\item Check the well-typedness of a program
|
||||
\pause
|
||||
\item Check that there are no assignment conflicts in a programs
|
||||
(node-pass)
|
||||
\pause
|
||||
\end{itemize}
|
||||
\end{block}
|
||||
\begin{block}{AST modification}
|
||||
\begin{itemize}
|
||||
\item Rewrite automata into \texttt{if-then-else} constructs
|
||||
(node-pass)
|
||||
\pause
|
||||
\item Linearization of the equations:
|
||||
\begin{itemize}
|
||||
\item for all, \texttt{pre e} add a, intermediate variable
|
||||
\item \texttt{v1, v2, v3 = f(i), e3;} is rewritten into
|
||||
\texttt{v1, v2 = f(i); v3 = e3;}
|
||||
\end{itemize}
|
||||
(node-pass)
|
||||
\pause
|
||||
\item (no longer required) Push the \texttt{pre} to variables
|
||||
(expression-pass)
|
||||
\end{itemize}
|
||||
\end{block}
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}[fragile]{Translation of automaton}
|
||||
\only<1>{\lstinputlisting[language=ml, firstline=1, lastline=7]{code/example_automaton.lus}}
|
||||
\only<2>{\lstinputlisting[language=ml, firstline=9, lastline=14]{code/example_automaton.lus}}
|
||||
\end{frame}
|
||||
\begin{frame}{Restriction on automaton}
|
||||
The patterns that appears on the left of equations must be the
|
||||
same in all branches
|
||||
|
||||
\only<2>{\lstinputlisting[language=ml, firstline=16, lastline=22]{code/example_automaton.lus}}
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}{Clock unification}
|
||||
|
||||
Derived from the rules provided in \emph{Clock-directed Modular Code Generation for Synchronous
|
||||
Data-flow Languages}
|
||||
\end{frame}
|
||||
|
||||
\section{Translation to C}
|
||||
\begin{frame}
|
||||
|
||||
\texttt{ast\_to\_c.ml} architecture similar to Arnaud's AST pretty-printer.
|
||||
|
||||
\pause
|
||||
|
||||
For instance, go from \texttt{counting.lus} to \texttt{counting.c}.
|
||||
|
||||
\pause
|
||||
|
||||
Use of three tricks, as our compiler only manages \texttt{bool}s, \texttt{int}s and \texttt{float}s:
|
||||
\begin{enumerate}
|
||||
\item \texttt{0} can be interpreted as a \texttt{bool}, an \texttt{int} and a \texttt{float}
|
||||
\pause
|
||||
\item A \texttt{float} correctly encode \texttt{bool}s (\texttt{true} and \texttt{false}) and \texttt{int}s (between $[-2^{24} + 1; 2^{24} + 1]$)
|
||||
\pause
|
||||
\item To run an assignment of \texttt{value} to \texttt{variable} within the condition of a \texttt{if} and also make the cases of the \texttt{if} depends on a condition \texttt{condition}, we can do \texttt{if(((variable = value) \&\& false) || condition)}\\
|
||||
\pause
|
||||
We can also use this trick to execute an assignment and \textit{return} a value \texttt{value\_to\_return} without using any \texttt{;}, by using \texttt{((variable = value) || true) ? value\_to\_return : 0} (thanks to the first trick)
|
||||
\end{enumerate}
|
||||
\end{frame}
|
||||
|
||||
\begin{frame}
|
||||
\begin{itemize}
|
||||
\item
|
||||
\begin{itemize}
|
||||
\item \texttt{pp\_varlist (Base | Arg | Dec)}
|
||||
\item \texttt{pp\_retvarlist}
|
||||
\item \texttt{pp\_prevarlist}
|
||||
\item \texttt{pp\_asnprevarlist}
|
||||
\end{itemize}
|
||||
\pause
|
||||
\item \texttt{when} implementation error: division by zero for instance, so used the first trick (\texttt{when\_merge.node})
|
||||
\pause
|
||||
\item \texttt{->}: use global variable \texttt{init\_\{NODE\_NAME\}}\\
|
||||
\texttt{1 -> 2 -> 3} returns \texttt{0} on first run and only \texttt{3} on the following ones, correct? (\texttt{arrow.node})
|
||||
\pause
|
||||
\item \texttt{pre}
|
||||
\pause
|
||||
\item \texttt{reset}% (\texttt{reset})
|
||||
\pause
|
||||
\item Functions returning tuples thanks to Arnaud's linearization only have to deal with \texttt{(a0, a1, ..., an) = return\_tuple\_a0\_a1\_dots\_an(0)} (\texttt{function\_returning\_tuple.node})
|
||||
\end{itemize}
|
||||
\end{frame}
|
||||
|
||||
\section{Tests}
|
||||
\begin{frame}{Tests}
|
||||
\begin{block}{testing methods}
|
||||
We thought of three testing methods:
|
||||
\begin{itemize}
|
||||
\item manual testing of our functionalities
|
||||
\item run the sanity-checks-passes after any AST-altering pass
|
||||
\item simulation of the nodes (aborted)
|
||||
\end{itemize}
|
||||
\end{block}
|
||||
\end{frame}
|
||||
|
||||
\section{Possible improvements}
|
||||
\begin{frame}{Improvements}
|
||||
\begin{itemize}
|
||||
\item Increase the expressivity of the accepted programs
|
||||
\item Improve the complexity of the different passes
|
||||
\begin{itemize}
|
||||
\item Group neighbour passes of the same type (node-, expression or
|
||||
equation-pass).
|
||||
\end{itemize}
|
||||
\item \dots{}
|
||||
\end{itemize}
|
||||
\end{frame}
|
||||
|
||||
\end{document}
|
||||
|
22
beamer/code/example_automaton.lus
Normal file
22
beamer/code/example_automaton.lus
Normal file
@@ -0,0 +1,22 @@
|
||||
node auto (i: int) returns (o : int);
|
||||
var x, y: int;
|
||||
let
|
||||
automaton
|
||||
| Incr -> do (o,x) = (0 fby o + 1, 2); until o < 5 then Decr
|
||||
| Decr -> do (o,x) = diagonal_int(0 fby o); until o > 3 then Incr
|
||||
tel
|
||||
|
||||
node auto (i: int) returns (o : int);
|
||||
var x, y: int;
|
||||
let
|
||||
_s1 = 1 -> (if _s = 1 and o < 5 then 2 else if _s = 2 and o > then 1 else 1);
|
||||
o, x = if _s = 1 then (0 fby o + 1, 2) else if _s = 2 then diagonal_int(0 fby 0) else (0, 0);
|
||||
tel
|
||||
|
||||
node auto (i: int) returns (o : int);
|
||||
var x, y: int;
|
||||
let
|
||||
automaton
|
||||
| Incr -> do (o,x) = (0 fby o + 1, 2); until o < 5 then Decr
|
||||
| Decr -> do (x,o) = diagonal_int(0 fby o); until o > 3 then Incr
|
||||
tel
|
BIN
beamer/imgs/explicit_types.png
Normal file
BIN
beamer/imgs/explicit_types.png
Normal file
Binary file not shown.
After Width: | Height: | Size: 155 KiB |
BIN
beamer/imgs/gadt.png
Normal file
BIN
beamer/imgs/gadt.png
Normal file
Binary file not shown.
After Width: | Height: | Size: 139 KiB |
21
src/ast.ml
21
src/ast.ml
@@ -35,10 +35,7 @@ type t_var =
|
||||
| IVar of ident
|
||||
| RVar of ident
|
||||
|
||||
type full_ty =
|
||||
| FTArr of full_ty * full_ty
|
||||
| FTList of full_ty list
|
||||
| FTBase of base_ty
|
||||
type full_ty = base_ty list
|
||||
|
||||
type t_expression =
|
||||
| EVar of full_ty * t_var
|
||||
@@ -47,16 +44,23 @@ type t_expression =
|
||||
| ETriOp of full_ty * triop * t_expression * t_expression * t_expression
|
||||
| EComp of full_ty * compop * t_expression * t_expression
|
||||
| EWhen of full_ty * t_expression * t_expression
|
||||
| EReset of full_ty * t_expression * t_expression
|
||||
| EConst of full_ty * const
|
||||
| ETuple of full_ty * (t_expression list)
|
||||
| EApp of full_ty * t_node * t_expression
|
||||
|
||||
and t_varlist = full_ty * (t_var list)
|
||||
|
||||
and t_equation = t_varlist * t_expression
|
||||
and t_equation = t_varlist * t_expression
|
||||
|
||||
and t_eqlist = t_equation list
|
||||
|
||||
and t_state = | State of ident * t_eqlist * (t_expression list) * (ident list)
|
||||
|
||||
and t_automaton = t_state * t_state list
|
||||
|
||||
and t_autolist = t_automaton list
|
||||
|
||||
and t_node =
|
||||
{
|
||||
n_name : ident;
|
||||
@@ -64,8 +68,13 @@ and t_node =
|
||||
n_outputs: t_varlist;
|
||||
n_local_vars: t_varlist;
|
||||
n_equations: t_eqlist;
|
||||
n_type : full_ty;
|
||||
n_automata: t_autolist;
|
||||
}
|
||||
|
||||
type t_nodelist = t_node list
|
||||
|
||||
type t_ck = base_ck list
|
||||
and base_ck =
|
||||
| Base
|
||||
| On of base_ck * t_expression
|
||||
| Unknown
|
||||
|
324
src/ast_to_c.ml
Normal file
324
src/ast_to_c.ml
Normal file
@@ -0,0 +1,324 @@
|
||||
open Ast
|
||||
open Intermediate_ast
|
||||
open Intermediate_utils
|
||||
open Cprint
|
||||
open Cast
|
||||
open Utils
|
||||
open Ctranslation
|
||||
|
||||
|
||||
|
||||
(** [ast_to_intermediate_ast] translates a [t_nodelist] into a [i_nodelist] *)
|
||||
let ast_to_intermediate_ast (nodes: t_nodelist) (h: node_states): i_nodelist =
|
||||
let c = ref 1 in
|
||||
let ast_to_intermediate_ast_varlist vl = snd vl in
|
||||
let rec ast_to_intermediate_ast_expr hloc = function
|
||||
| EVar (_, v) ->
|
||||
begin
|
||||
match Hashtbl.find_opt hloc (Utils.name_of_var v, false) with
|
||||
| None -> IEVar (CVInput (name_of_var v))
|
||||
| Some (s, i) -> IEVar (CVStored (s, i))
|
||||
end
|
||||
| EMonOp (_, MOp_pre, EVar (_, v)) ->
|
||||
let s, i = Hashtbl.find hloc (Utils.name_of_var v, true) in
|
||||
IEVar (CVStored (s, i))
|
||||
| EMonOp (_, op, e) -> IEMonOp (op, ast_to_intermediate_ast_expr hloc e)
|
||||
| EBinOp (_, op, e, e') ->
|
||||
IEBinOp (op, ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e')
|
||||
| ETriOp (_, op, e, e', e'') ->
|
||||
IETriOp
|
||||
(op, ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e', ast_to_intermediate_ast_expr hloc e'')
|
||||
| EComp (_, op, e, e') ->
|
||||
IEComp (op, ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e')
|
||||
| EWhen (_, e, e') ->
|
||||
IEWhen (ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e')
|
||||
| EReset (_, e, e') ->
|
||||
IEReset (ast_to_intermediate_ast_expr hloc e, ast_to_intermediate_ast_expr hloc e')
|
||||
| EConst (_, c) -> IEConst c
|
||||
| ETuple (_, l) -> IETuple (List.map (ast_to_intermediate_ast_expr hloc) l)
|
||||
| EApp (_, n, e) ->
|
||||
begin
|
||||
let e = ast_to_intermediate_ast_expr hloc e in
|
||||
let res = IEApp (!c, n, e) in
|
||||
let () = incr c in
|
||||
res
|
||||
end
|
||||
in
|
||||
let ast_to_intermediate_ast_eq hloc (patt, expr) : i_equation =
|
||||
(ast_to_intermediate_ast_varlist patt, ast_to_intermediate_ast_expr hloc expr) in
|
||||
List.map
|
||||
begin
|
||||
fun node ->
|
||||
let () = c := 1 in
|
||||
let hloc = (Hashtbl.find h node.n_name).nt_map in
|
||||
{
|
||||
in_name = node.n_name;
|
||||
in_inputs = ast_to_intermediate_ast_varlist node.n_inputs;
|
||||
in_outputs = ast_to_intermediate_ast_varlist node.n_outputs;
|
||||
in_local_vars = ast_to_intermediate_ast_varlist node.n_local_vars;
|
||||
in_equations = List.map (ast_to_intermediate_ast_eq hloc) node.n_equations;
|
||||
}
|
||||
end
|
||||
nodes
|
||||
|
||||
(** The following function defines the [node_states] for the nodes of a program,
|
||||
* and puts them in a hash table. *)
|
||||
let make_state_types nodes: node_states =
|
||||
(* Hash table to fill *)
|
||||
let h: (ident, node_state) Hashtbl.t = Hashtbl.create (List.length nodes) in
|
||||
|
||||
(** [one_node node pv ty] computes the number of variables of type [ty] in
|
||||
* [node] and a mapping from the variables of type ([ty] * bool) to int,
|
||||
* where [pv] is a list of variables used in the pre construct in the
|
||||
* program. *)
|
||||
let one_node node pv ty =
|
||||
(* variables of type [ty] among output and local variables *)
|
||||
let vars =
|
||||
List.filter (fun v -> type_var v = [ty])
|
||||
(snd (varlist_concat node.n_outputs node.n_local_vars)) in
|
||||
let all_vars =
|
||||
List.filter (fun v -> type_var v = [ty])
|
||||
(snd (varlist_concat (varlist_concat node.n_inputs node.n_outputs) node.n_local_vars)) in
|
||||
let pre_vars =
|
||||
List.filter (fun v -> List.mem v pv) all_vars in
|
||||
let vars = List.map Utils.name_of_var vars in
|
||||
let pre_vars = List.map Utils.name_of_var pre_vars in
|
||||
let nb = (List.length vars) + (List.length pre_vars) in
|
||||
let tyh: (ident * bool, int) Hashtbl.t = Hashtbl.create nb in
|
||||
let i =
|
||||
List.fold_left
|
||||
(fun i v -> let () = Hashtbl.add tyh (v, false) i in i + 1) 0 vars in
|
||||
let _ =
|
||||
List.fold_left
|
||||
(fun i v -> let () = Hashtbl.add tyh (v, true) i in i + 1) i pre_vars in
|
||||
(nb, tyh)
|
||||
in
|
||||
|
||||
(** [find_prevars n] returns the list of variables appearing after a pre in
|
||||
* the node [n].
|
||||
* Note that the only occurrence of pre are of the form pre (var), due to
|
||||
* the linearization pass.
|
||||
*)
|
||||
let find_prevars node =
|
||||
let rec find_prevars_expr = function
|
||||
| EConst _ | EVar _ -> []
|
||||
| EMonOp (_, MOp_pre, EVar (_, v)) -> [v]
|
||||
| EMonOp (_, _, e) -> find_prevars_expr e
|
||||
| ETriOp (_, _, e, e', e'') ->
|
||||
(find_prevars_expr e) @ (find_prevars_expr e') @ (find_prevars_expr e'')
|
||||
| EComp (_, _, e, e')
|
||||
| EBinOp (_, _, e, e')
|
||||
| EWhen (_, e, e')
|
||||
| EReset (_, e, e') -> (find_prevars_expr e) @ (find_prevars_expr e')
|
||||
| ETuple (_, l) -> List.flatten (List.map (find_prevars_expr) l)
|
||||
| EApp (_, _, e) -> find_prevars_expr e
|
||||
in
|
||||
list_remove_duplicates
|
||||
(List.fold_left
|
||||
(fun acc (_, expr) -> (find_prevars_expr expr) @ acc)
|
||||
[] node.n_equations)
|
||||
in
|
||||
|
||||
(** [count_app n] count the number of auxiliary nodes calls in [n] *)
|
||||
let count_app n =
|
||||
let rec count_app_expr = function
|
||||
| EConst _ | EVar _ -> 0
|
||||
| EMonOp (_, _, e) -> count_app_expr e
|
||||
| ETriOp (_, _, e, e', e'') ->
|
||||
(count_app_expr e) + (count_app_expr e') + (count_app_expr e'')
|
||||
| EComp (_, _, e, e')
|
||||
| EBinOp (_, _, e, e')
|
||||
| EWhen (_, e, e')
|
||||
| EReset (_, e, e') -> (count_app_expr e) + (count_app_expr e')
|
||||
| ETuple (_, l) ->
|
||||
List.fold_left (fun acc e -> acc + count_app_expr e) 0 l
|
||||
| EApp (_, _, e) -> 1 + count_app_expr e
|
||||
in
|
||||
List.fold_left
|
||||
(fun i (_, expr) -> i + count_app_expr expr)
|
||||
0 n.n_equations
|
||||
in
|
||||
|
||||
(** [aux] iterates over all nodes of the program to build the required hash
|
||||
* table *)
|
||||
let rec aux nodes =
|
||||
match nodes with
|
||||
| [] -> h
|
||||
| node :: nodes ->
|
||||
begin
|
||||
let h = aux nodes in
|
||||
let node_name = node.n_name in
|
||||
let pv = find_prevars node in
|
||||
let nb_int_vars, h_int = one_node node pv TInt in
|
||||
let nb_bool_vars, h_bool = one_node node pv TBool in
|
||||
let nb_real_vars, h_real = one_node node pv TReal in
|
||||
|
||||
(** h_map gathers information from h_* maps above *)
|
||||
let h_map =
|
||||
Hashtbl.create (nb_int_vars + nb_bool_vars + nb_real_vars) in
|
||||
let () =
|
||||
Hashtbl.iter (fun k v -> Hashtbl.add h_map k ("ivars", v)) h_int in
|
||||
let () =
|
||||
Hashtbl.iter (fun k v -> Hashtbl.add h_map k ("bvars", v)) h_bool in
|
||||
let () =
|
||||
Hashtbl.iter (fun k v -> Hashtbl.add h_map k ("rvars", v)) h_real in
|
||||
|
||||
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: t_var) ->
|
||||
match v with
|
||||
| IVar s ->
|
||||
let i = Hashtbl.find h_int (s, false) in
|
||||
Hashtbl.add h_out n ("ivars", i)
|
||||
| BVar s ->
|
||||
let i = Hashtbl.find h_bool (s, false) in
|
||||
Hashtbl.add h_out n ("bvars", i)
|
||||
| RVar s ->
|
||||
let i = Hashtbl.find h_real (s, false) in
|
||||
Hashtbl.add h_out n ("rvars", i))
|
||||
(snd node.n_outputs) in
|
||||
let () = Hashtbl.add h node_name
|
||||
{
|
||||
nt_name = Format.asprintf "t_state_%s" node.n_name;
|
||||
nt_nb_int = nb_int_vars;
|
||||
nt_nb_bool = nb_bool_vars;
|
||||
nt_nb_real = nb_real_vars;
|
||||
nt_map = h_map;
|
||||
nt_output_map = h_out;
|
||||
nt_prevars = pv;
|
||||
nt_count_app = count_app node;
|
||||
} in
|
||||
h
|
||||
end
|
||||
in
|
||||
aux nodes
|
||||
|
||||
|
||||
|
||||
(** The following C-printer functions are in this file, as they need to work on
|
||||
* the AST and are not simple printers. *)
|
||||
|
||||
|
||||
|
||||
(** 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.in_name in
|
||||
match (Hashtbl.find h node.in_name).nt_prevars with
|
||||
| [] -> ()
|
||||
| l ->
|
||||
Format.fprintf fmt
|
||||
"\n\t/* Remember the values used in the [pre] construct */\n";
|
||||
List.iter
|
||||
(fun v -> (** Note that «dst_array = src_array» should hold. *)
|
||||
match Hashtbl.find_opt node_st.nt_map (v, false) with
|
||||
| Some (src_array, src_idx) ->
|
||||
let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in
|
||||
Format.fprintf fmt "\t_state->%s[%d] = _state->%s[%d];\n"
|
||||
dst_array dst_idx src_array src_idx
|
||||
| None ->
|
||||
let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in
|
||||
Format.fprintf fmt "\t_state->%s[%d] = %s;\n"
|
||||
dst_array dst_idx v
|
||||
)
|
||||
(List.map Utils.name_of_var l)
|
||||
|
||||
|
||||
|
||||
(** The following function defines the behaviour to have at the first
|
||||
* execution of a node, namely:
|
||||
* - initialize the states of auxiliary nodes
|
||||
*)
|
||||
let cp_init_aux_nodes fmt (node, h) =
|
||||
let rec aux fmt (node, nst, i) =
|
||||
match find_app_opt node.in_equations i with
|
||||
| None -> () (** All auxiliary nodes have been initialized *)
|
||||
| Some n ->
|
||||
begin
|
||||
Format.fprintf fmt "%a\t\tif(!_state->is_reset) {\n\
|
||||
\t\t\t_state->aux_states[%d] = calloc (1, sizeof (%s));\n\
|
||||
\t\t}\n\
|
||||
\t\t((%s*)(_state->aux_states[%d]))->is_init = true;\n\
|
||||
\t\t((%s*)(_state->aux_states[%d]))->is_reset = _state->is_reset;\n"
|
||||
aux (node, nst, i-1)
|
||||
(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)
|
||||
end
|
||||
in
|
||||
let nst = Hashtbl.find h node.in_name in
|
||||
if nst.nt_count_app = 0
|
||||
then ()
|
||||
else begin
|
||||
Format.fprintf fmt "\t/* Initialize the auxiliary nodes */\n\
|
||||
\tif (_state->is_init) {\n%a\t}\n\n\n"
|
||||
aux (node, nst, nst.nt_count_app)
|
||||
end
|
||||
|
||||
|
||||
|
||||
(** [cp_equations] prints the node equations. *)
|
||||
let cp_equations fmt (eqs, hloc, h) =
|
||||
(** [main_block] is modified through some optimization passes, eg:
|
||||
* - merge two CIf blocks using the same condition
|
||||
* - replace [if (! c) { b1 } else { b2 }] by [if(c) { b2 } else { b1 }]
|
||||
*
|
||||
* These passes are defined in [ctranslation.ml]
|
||||
*)
|
||||
let main_block: c_block =
|
||||
List.map (fun eq -> equation_to_expression (hloc, h, eq)) eqs in
|
||||
let main_block = remove_ifnot main_block in
|
||||
let main_block = merge_neighbour_ifs main_block in
|
||||
Format.fprintf fmt "\t/*Main code:*/\n%a"
|
||||
cp_block (main_block, hloc.nt_map)
|
||||
|
||||
(** [cp_node] prints a single node *)
|
||||
let cp_node fmt (node, h) =
|
||||
Format.fprintf fmt "%a\n{\n%a%a\n\n\t_state->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, h)
|
||||
cp_prevars (node, h)
|
||||
|
||||
(** [cp_nodes] recursively prints all the nodes of a program. *)
|
||||
let rec cp_nodes fmt (nodes, h) =
|
||||
match nodes with
|
||||
| [] -> ()
|
||||
| node :: nodes ->
|
||||
Format.fprintf fmt "%a\n%a"
|
||||
cp_node (node, h)
|
||||
cp_nodes (nodes, h)
|
||||
|
||||
|
||||
|
||||
(** [dump_var_locations] dumps the internal tables to map the program variable
|
||||
* (after all the passes) to their location in the final C program. *)
|
||||
let dump_var_locations fmt (st: node_states) =
|
||||
Format.fprintf fmt "Tables mapping the AST variables to the C variables:\n";
|
||||
Hashtbl.iter
|
||||
(fun n st ->
|
||||
Format.fprintf fmt " ∗ NODE: %s\n" n;
|
||||
Hashtbl.iter
|
||||
(fun (s, (ispre: bool)) ((arr: string), (idx: int)) ->
|
||||
match ispre with
|
||||
| true -> Format.fprintf fmt " PRE Variable %s stored as %s[%d]\n" s arr idx
|
||||
| false -> Format.fprintf fmt " Variable %s stored as %s[%d]\n" s arr idx)
|
||||
st.nt_map)
|
||||
st
|
||||
|
||||
|
||||
|
||||
(** main function that prints a C-code from a term of type [t_nodelist]. *)
|
||||
let ast_to_c fmt verbose debug prog =
|
||||
verbose "Computation of the node_states";
|
||||
let prog_st_types = make_state_types prog in
|
||||
debug (Format.asprintf "%a" dump_var_locations prog_st_types);
|
||||
let iprog: i_nodelist = ast_to_intermediate_ast prog prog_st_types in
|
||||
Format.fprintf fmt "%a\n\n#define BUFFER_SIZE 1024\n\n%a\n\n%a\n\n/* Nodes: */\n%a%a\n"
|
||||
cp_includes (Config.c_includes)
|
||||
cp_state_types prog_st_types
|
||||
cp_state_frees (iprog, prog_st_types)
|
||||
cp_nodes (iprog, prog_st_types)
|
||||
cp_main_fn (prog, prog_st_types)
|
||||
|
27
src/cast.ml
Normal file
27
src/cast.ml
Normal file
@@ -0,0 +1,27 @@
|
||||
open Intermediate_ast
|
||||
open Ast
|
||||
|
||||
(** This file contains a small subset of the syntax of C required for the
|
||||
* translation. *)
|
||||
|
||||
(** A [c_block] represents a block in C. *)
|
||||
type c_block = c_expression list
|
||||
|
||||
(** A [c_expresion] represents a C expression, which can need sequences and
|
||||
* function calls. *)
|
||||
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 * int * c_var list * c_var list * node_states
|
||||
| CReset of ident * int * c_value * c_block
|
||||
|
||||
(** A value here is anything that can be inlined into a single C expression
|
||||
* containing no function call, condition, ... *)
|
||||
and c_value =
|
||||
| CVariable of c_var
|
||||
| CMonOp of monop * c_value
|
||||
| CBinOp of binop * c_value * c_value
|
||||
| CComp of compop * c_value * c_value
|
||||
| CConst of const
|
||||
|
6
src/config.ml
Normal file
6
src/config.ml
Normal file
@@ -0,0 +1,6 @@
|
||||
(** Maximum Number of variables declared in a single node.
|
||||
* This corresponds to the sum of the number of local, input and output
|
||||
* variables. *)
|
||||
let maxvar = 100
|
||||
|
||||
let c_includes = ["stdbool"; "stdlib"; "stdio"; "string"]
|
454
src/cprint.ml
Normal file
454
src/cprint.ml
Normal file
@@ -0,0 +1,454 @@
|
||||
open Intermediate_utils
|
||||
open Intermediate_ast
|
||||
open Ast
|
||||
open Cast
|
||||
|
||||
(** This file contains extremely simple functions printing C code. *)
|
||||
|
||||
let rec cp_includes fmt = function
|
||||
| [] -> ()
|
||||
| h :: t ->
|
||||
Format.fprintf fmt "#include <%s.h>\n%a" h cp_includes t
|
||||
|
||||
let cp_node_state fmt (st: node_state) =
|
||||
let print_if_any fmt (ty, nb, name): unit =
|
||||
if nb = 0
|
||||
then ()
|
||||
else Format.fprintf fmt "\n\t%s %s[%d];" ty name nb
|
||||
in
|
||||
if st.nt_count_app = 0
|
||||
then
|
||||
Format.fprintf fmt "typedef struct {%a%a%a\n\
|
||||
\tbool is_init, is_reset;\n\
|
||||
} %s;\n\n"
|
||||
print_if_any ("int", st.nt_nb_int, "ivars")
|
||||
print_if_any ("bool", st.nt_nb_bool, "bvars")
|
||||
print_if_any ("double", st.nt_nb_real, "rvars")
|
||||
st.nt_name
|
||||
else
|
||||
Format.fprintf fmt "typedef struct {%a%a%a\n\
|
||||
\tbool is_init, is_reset;\n\
|
||||
\tvoid* aux_states[%d]; /* stores the states of auxiliary nodes */\n\
|
||||
} %s;\n\n"
|
||||
print_if_any ("int", st.nt_nb_int, "ivars")
|
||||
print_if_any ("bool", st.nt_nb_bool, "bvars")
|
||||
print_if_any ("double", st.nt_nb_real, "rvars")
|
||||
st.nt_count_app st.nt_name
|
||||
|
||||
let cp_state_types fmt (h: (ident, node_state) Hashtbl.t): unit =
|
||||
Hashtbl.iter (fun n nst ->
|
||||
Format.fprintf fmt "/* Struct holding states of the node %s: */\n%a" n
|
||||
cp_node_state nst) h
|
||||
|
||||
|
||||
|
||||
(** [cp_state_frees] prints the required code to recursively free the node
|
||||
* states. *)
|
||||
let cp_state_frees fmt (iprog, sts) =
|
||||
let rec find_callee (i: int) (f: i_node) =
|
||||
let rec aux_expr = function
|
||||
| IETuple [] | IEVar _ | IEConst _ -> None
|
||||
| IEMonOp (_, e) -> aux_expr e
|
||||
| IEWhen (e, e')
|
||||
| IEReset (e, e')
|
||||
| IEComp (_, e, e')
|
||||
| IEBinOp (_, e, e') ->
|
||||
begin
|
||||
match aux_expr e with
|
||||
| None -> aux_expr e'
|
||||
| Some res -> Some res
|
||||
end
|
||||
| IETriOp (_, e, e', e'') ->
|
||||
begin
|
||||
match aux_expr e with
|
||||
| None ->
|
||||
(match aux_expr e' with
|
||||
| None -> aux_expr e''
|
||||
| Some res -> Some res)
|
||||
| Some res -> Some res
|
||||
end
|
||||
| IETuple (h :: t) ->
|
||||
begin
|
||||
match aux_expr h with
|
||||
| None -> aux_expr (IETuple t)
|
||||
| Some res -> Some res
|
||||
end
|
||||
| IEApp (j, n, e) ->
|
||||
if i = j
|
||||
then Some n.n_name
|
||||
else aux_expr e
|
||||
in
|
||||
List.fold_right
|
||||
(fun (_, expr) acc ->
|
||||
match acc with
|
||||
| Some _ -> acc
|
||||
| None -> aux_expr expr)
|
||||
f.in_equations None
|
||||
in
|
||||
let rec cp_free_aux fmt (i, caller_name) =
|
||||
let idx = i - 1 in
|
||||
match find_callee i (List.find (fun n -> n.in_name = caller_name) iprog)with
|
||||
| None -> ()
|
||||
| Some callee_name ->
|
||||
let callee_st = Hashtbl.find sts callee_name in
|
||||
if callee_st.nt_count_app > 0
|
||||
then
|
||||
Format.fprintf fmt "\tif (st->aux_states[%d]) {\n\
|
||||
\t\tfree_state_%s((t_state_%s*)(st->aux_states[%d]));\n\
|
||||
\t\tfree (st->aux_states[%d]);\n\t}\n%a"
|
||||
idx callee_name callee_name idx
|
||||
idx cp_free_aux (i+1, caller_name)
|
||||
else Format.fprintf fmt "\tif (st->aux_states[%d])\n\
|
||||
\t\tfree(st->aux_states[%d]);\n%a"
|
||||
idx idx cp_free_aux (i+1, caller_name)
|
||||
in
|
||||
Hashtbl.iter
|
||||
(fun node_name node_st ->
|
||||
if node_st.nt_count_app = 0
|
||||
then () (** Nothing to free for the node [node_name]. *)
|
||||
else
|
||||
Format.fprintf fmt "void free_state_%s(t_state_%s *);\n"
|
||||
node_name node_name) sts;
|
||||
Hashtbl.iter
|
||||
(fun node_name node_st ->
|
||||
if node_st.nt_count_app = 0
|
||||
then () (** Nothing to free for the node [node_name]. *)
|
||||
else
|
||||
Format.fprintf fmt "void free_state_%s(t_state_%s *st)\n\
|
||||
{\n\
|
||||
%a\
|
||||
}\n"
|
||||
node_name node_name
|
||||
cp_free_aux (1, node_name)) sts
|
||||
|
||||
|
||||
|
||||
let cp_var' fmt = function
|
||||
| CVStored (arr, idx) -> Format.fprintf fmt "_state->%s[%d]" arr idx
|
||||
| CVInput s -> Format.fprintf fmt "%s" s
|
||||
|
||||
let cp_var fmt = function
|
||||
| IVar s -> Format.fprintf fmt "int %s" s
|
||||
| BVar s -> Format.fprintf fmt "bool %s" s
|
||||
| RVar s -> Format.fprintf fmt "double %s" s
|
||||
|
||||
let rec cp_varlist' fmt vl =
|
||||
let print_if_any fmt = function
|
||||
| [] -> ()
|
||||
| _ :: _ -> Format.fprintf fmt ", "
|
||||
in
|
||||
match vl with
|
||||
| [] -> ()
|
||||
| v :: vl ->
|
||||
Format.fprintf fmt "%a%a%a"
|
||||
cp_var' v
|
||||
print_if_any vl
|
||||
cp_varlist' vl
|
||||
|
||||
let rec cp_varlist fmt vl =
|
||||
let print_if_any fmt = function
|
||||
| [] -> ()
|
||||
| _ :: _ -> Format.fprintf fmt ", "
|
||||
in
|
||||
match vl with
|
||||
| [] -> ()
|
||||
| v :: vl ->
|
||||
Format.fprintf fmt "%a%a%a"
|
||||
cp_var v
|
||||
print_if_any vl
|
||||
cp_varlist vl
|
||||
|
||||
|
||||
|
||||
(** [cp_prototype] prints functions prototypes (without the «;»). It is only
|
||||
* used to write the beginning of functions right now. If we later allow to
|
||||
* use auxiliary nodes before their definition, it might be useful to declare
|
||||
* all the prototypes at the beginning of the file (Cf. [cp_prototypes] below.
|
||||
*)
|
||||
let cp_prototype fmt (node, h): unit =
|
||||
match Hashtbl.find_opt h node.in_name with
|
||||
| None -> failwith "This should not happened!"
|
||||
| Some nst ->
|
||||
begin
|
||||
Format.fprintf fmt "void fn_%s (%s *_state, %a)"
|
||||
node.in_name
|
||||
nst.nt_name
|
||||
cp_varlist node.in_inputs
|
||||
end
|
||||
|
||||
let rec cp_prototypes fmt ((nodes, h): i_nodelist * node_states) =
|
||||
match nodes with
|
||||
| [] -> ()
|
||||
| node :: nodes ->
|
||||
Format.fprintf fmt "%a;\n%a"
|
||||
cp_prototype (node, h)
|
||||
cp_prototypes (nodes, h)
|
||||
|
||||
|
||||
|
||||
(** [cp_value] prints values, that is unary or binary operations which can be
|
||||
* inlined in the final code without requiring many manipulations.
|
||||
* It uses a lot of parenthesis at the moment. An improvement would be to
|
||||
* remove useless ones at some point. *)
|
||||
let rec cp_value fmt (value, (hloc: (ident * bool, string * int) Hashtbl.t)) =
|
||||
let string_of_binop = function
|
||||
| BOp_add -> "+"
|
||||
| BOp_sub -> "-"
|
||||
| BOp_mul -> "*"
|
||||
| BOp_div -> "/"
|
||||
| BOp_mod -> "%"
|
||||
| BOp_and -> "&&"
|
||||
| BOp_or -> "||"
|
||||
| BOp_arrow -> failwith "string_of_binop undefined on (->)"
|
||||
in
|
||||
let string_of_compop = function
|
||||
| COp_eq -> "=="
|
||||
| COp_neq -> "!="
|
||||
| COp_le -> "<="
|
||||
| COp_lt -> "<"
|
||||
| COp_ge -> ">="
|
||||
| COp_gt -> ">"
|
||||
in
|
||||
match value with
|
||||
| CVariable (CVInput s) -> Format.fprintf fmt "%s" s
|
||||
| CVariable (CVStored (arr, idx)) -> Format.fprintf fmt "_state->%s[%d]" arr idx
|
||||
| CConst (CInt i) -> Format.fprintf fmt "%d" i
|
||||
| CConst (CBool b) -> Format.fprintf fmt "%s" (Bool.to_string b)
|
||||
| CConst (CReal r) -> Format.fprintf fmt "%f" r
|
||||
| CMonOp (MOp_not, v) -> Format.fprintf fmt "! (%a)" cp_value (v, hloc)
|
||||
| CMonOp (MOp_minus, v) -> Format.fprintf fmt "- (%a)" cp_value (v, hloc)
|
||||
| CMonOp (MOp_pre, (CVariable v)) ->
|
||||
let varname = (match v with
|
||||
| CVStored (arr, idx) ->
|
||||
begin
|
||||
match find_varname hloc (arr, idx) with
|
||||
| None -> failwith "This varname should be defined."
|
||||
| Some (n, _) -> n
|
||||
end
|
||||
| CVInput n -> n) in
|
||||
let (arr, idx) = Hashtbl.find hloc (varname, true) in
|
||||
Format.fprintf fmt "_state->%s[%d]" arr idx
|
||||
| CBinOp (BOp_arrow, v, v') ->
|
||||
Format.fprintf fmt "(_state->is_init ? (%a) : (%a))"
|
||||
cp_value (v, hloc) cp_value (v', hloc)
|
||||
| CBinOp (op, v, v') ->
|
||||
Format.fprintf fmt "(%a) %s (%a)"
|
||||
cp_value (v, hloc) (string_of_binop op) cp_value (v', hloc)
|
||||
| CComp (op, v, v') ->
|
||||
Format.fprintf fmt "(%a) %s (%a)"
|
||||
cp_value (v, hloc) (string_of_compop op) cp_value (v', hloc)
|
||||
| CMonOp (MOp_pre, _) ->
|
||||
failwith "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_block fmt (b, hloc) =
|
||||
match b with
|
||||
| [] -> ()
|
||||
| e :: b ->
|
||||
Format.fprintf fmt "%a%a" cp_expression (e, hloc) cp_block (b, hloc)
|
||||
and cp_expression fmt (expr, hloc) =
|
||||
let prefix = !prefix_ in
|
||||
match expr with
|
||||
| CAssign (CVStored (arr, idx), value) ->
|
||||
begin
|
||||
Format.fprintf fmt "%s_state->%s[%d] = %a;\n"
|
||||
prefix arr idx cp_value (value, hloc)
|
||||
end
|
||||
| CAssign (CVInput _, _) -> failwith "never assign an input."
|
||||
| CSeq (e, e') ->
|
||||
Format.fprintf fmt "%a%a"
|
||||
cp_expression (e, hloc)
|
||||
cp_expression (e', hloc)
|
||||
| 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(%s, %a);\n"
|
||||
prefix fn
|
||||
(Format.asprintf "_state->aux_states[%d]" (nb-1))
|
||||
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 "%s_state->%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 "Impossible!")
|
||||
0 destl in ()
|
||||
end
|
||||
| CReset (node_name, i, v, b) ->
|
||||
begin
|
||||
Format.fprintf fmt "\tif (%a) {\n\
|
||||
\t\t((t_state_%s*)(_state->aux_states[%d]))->is_init = true;\n\
|
||||
\t\t((t_state_%s*)(_state->aux_states[%d]))->is_reset = true;\n\
|
||||
\t}\n\
|
||||
%a\n"
|
||||
cp_value (v, hloc)
|
||||
node_name
|
||||
(i - 1)
|
||||
node_name
|
||||
(i - 1)
|
||||
cp_block (b, hloc)
|
||||
end
|
||||
| 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, hloc)
|
||||
p;
|
||||
prefix_ := p
|
||||
| CIf (v, b1, b2) ->
|
||||
let p = prefix in
|
||||
prefix_ := prefix^"\t";
|
||||
Format.fprintf fmt "%sif (%a) {\n%a%s} else {\n%a%s}\n"
|
||||
p
|
||||
cp_value (v, hloc)
|
||||
cp_block (b1, hloc)
|
||||
p
|
||||
cp_block (b2, hloc)
|
||||
p;
|
||||
prefix_ := p
|
||||
|
||||
|
||||
|
||||
(** [cp_main] prints a main function to the C code if necessary:
|
||||
* if there is a function [main] in the lustre program, it will generate a main
|
||||
* function in the C code, otherwise it does not do anything.
|
||||
*)
|
||||
let cp_main_fn fmt (prog, sts) =
|
||||
let rec cp_array fmt (vl: t_var list): unit =
|
||||
match vl with
|
||||
| [] -> ()
|
||||
| v :: vl ->
|
||||
let typ, name =
|
||||
match v with
|
||||
| IVar s -> ("int", s)
|
||||
| RVar s -> ("double", s)
|
||||
| BVar s ->
|
||||
Format.fprintf fmt "\tchar _char_of_%s;\n" s;
|
||||
("bool", s)
|
||||
in
|
||||
Format.fprintf fmt "\t%s %s;\n%a" typ name
|
||||
cp_array vl
|
||||
in
|
||||
let rec cp_inputs fmt (f, l) =
|
||||
match l with
|
||||
| [] -> ()
|
||||
| h :: t ->
|
||||
(if f
|
||||
then Format.fprintf fmt ", %s%a"
|
||||
else Format.fprintf fmt "%s%a")
|
||||
(Utils.name_of_var h)
|
||||
cp_inputs (true, t)
|
||||
in
|
||||
let cp_scanf fmt vl =
|
||||
let rec cp_scanf_str fmt (b, vl) =
|
||||
match vl with
|
||||
| [] -> ()
|
||||
| h :: t ->
|
||||
(if b
|
||||
then Format.fprintf fmt " %s%a"
|
||||
else Format.fprintf fmt "%s%a")
|
||||
(match h with
|
||||
| IVar _ -> "%d"
|
||||
| BVar _ -> "%c"
|
||||
| RVar _ -> "%lf")
|
||||
cp_scanf_str (true, t)
|
||||
in
|
||||
let rec cp_scanf_args fmt vl =
|
||||
match vl with
|
||||
| [] -> ()
|
||||
| RVar s :: vl | IVar s :: vl ->
|
||||
Format.fprintf fmt ", &%s%a" s cp_scanf_args vl
|
||||
| BVar s :: vl ->
|
||||
Format.fprintf fmt ", &%s%a" (Format.sprintf "_char_of_%s" s)
|
||||
cp_scanf_args vl
|
||||
in
|
||||
Format.fprintf fmt "\"%a\"%a"
|
||||
cp_scanf_str (false, vl)
|
||||
cp_scanf_args vl
|
||||
in
|
||||
let cp_printf fmt vl =
|
||||
let rec cp_printf_str fmt (b, vl) =
|
||||
match vl with
|
||||
| [] -> ()
|
||||
| h :: t ->
|
||||
(if b
|
||||
then Format.fprintf fmt " %s%a"
|
||||
else Format.fprintf fmt "%s%a")
|
||||
(match h with
|
||||
| IVar _ -> "%d"
|
||||
| BVar _ -> "%hd"
|
||||
| RVar _ -> "%f")
|
||||
cp_printf_str (true, t)
|
||||
in
|
||||
let rec cp_printf_arg fmt (h, i) =
|
||||
match Hashtbl.find_opt h i with
|
||||
| None -> ()
|
||||
| Some (s, i) ->
|
||||
Format.fprintf fmt ", _state.%s[%d]%a"
|
||||
s i cp_printf_arg (h, i+1)
|
||||
in
|
||||
Format.fprintf fmt "\"%a\\n\"%a"
|
||||
cp_printf_str (false, vl)
|
||||
cp_printf_arg ((Hashtbl.find sts "main").nt_output_map, 0)
|
||||
in
|
||||
let rec cp_char_to_bool fmt vl =
|
||||
match vl with
|
||||
| [] -> ()
|
||||
| RVar _ :: vl | IVar _ :: vl -> Format.fprintf fmt "%a" cp_char_to_bool vl
|
||||
| BVar s :: vl ->
|
||||
Format.fprintf fmt "\t\t%s = (%s == 't') ? true : false;\n%a"
|
||||
s (Format.sprintf "_char_of_%s" s)
|
||||
cp_char_to_bool vl
|
||||
in
|
||||
let cp_free fmt () =
|
||||
let main_st = Hashtbl.find sts "main" in
|
||||
if main_st.nt_count_app = 0
|
||||
then ()
|
||||
else Format.fprintf fmt "\tfree_state_main(&_state);\n"
|
||||
in
|
||||
match List.find_opt (fun n -> n.n_name = "main") prog with
|
||||
| None -> ()
|
||||
| Some node ->
|
||||
Format.fprintf fmt "int main (int argc, char **argv)\n\
|
||||
{\n%a\n\
|
||||
\tchar buffer[BUFFER_SIZE];\n\
|
||||
\tt_state_main _state;\n\
|
||||
\t_state.is_init = true;\n\
|
||||
\t_state.is_reset = false;\n\
|
||||
\twhile(true) {\n\
|
||||
\t\tprintf(\"input: \");\n\
|
||||
\t\tfor(unsigned short idx = 0; idx < BUFFER_SIZE; idx++) {\n\
|
||||
\t\t\tif(idx == (BUFFER_SIZE - 1) || (buffer[idx] = getchar()) == '\\n') {\n\
|
||||
\t\t\t\tbuffer[idx] = '\\0';\n\
|
||||
\t\t\t\tbreak;\n\
|
||||
\t\t\t}\n\
|
||||
\t\t}\n\
|
||||
\t\tif(!strcmp(buffer, \"exit\")) { break; }\n\
|
||||
\t\tsscanf(buffer, %a);\n%a\
|
||||
\t\tfn_main(&_state, %a);\n\
|
||||
\t\tprintf(\"output: \");\n\
|
||||
\t\tprintf(%a);\n\
|
||||
\t\tprintf(\"\\n\");\n\
|
||||
\t}\n\
|
||||
%a\treturn EXIT_SUCCESS;\n\
|
||||
}\n"
|
||||
cp_array (snd node.n_inputs)
|
||||
cp_scanf (snd node.n_inputs)
|
||||
cp_char_to_bool (snd node.n_inputs)
|
||||
cp_inputs (false, snd node.n_inputs)
|
||||
cp_printf (snd node.n_outputs)
|
||||
cp_free ()
|
||||
|
120
src/ctranslation.ml
Normal file
120
src/ctranslation.ml
Normal file
@@ -0,0 +1,120 @@
|
||||
open Ast
|
||||
open Intermediate_ast
|
||||
open Cast
|
||||
|
||||
let rec iexpression_to_cvalue e =
|
||||
match e with
|
||||
| IEVar v -> CVariable v
|
||||
| IEMonOp (op, e) -> CMonOp (op, iexpression_to_cvalue e)
|
||||
| IEBinOp (op, e, e') ->
|
||||
CBinOp (op, iexpression_to_cvalue e, iexpression_to_cvalue e')
|
||||
| IEComp (op, e, e') ->
|
||||
CComp (op, iexpression_to_cvalue e, iexpression_to_cvalue e')
|
||||
| IEConst c -> CConst c
|
||||
| IEWhen _
|
||||
| IEReset _
|
||||
| IETuple _
|
||||
| IEApp _
|
||||
| IETriOp _ -> failwith "Should not happened."
|
||||
|
||||
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
|
||||
| [v] ->
|
||||
begin
|
||||
match Hashtbl.find_opt hloc (Utils.name_of_var v, false) with
|
||||
| None -> CVInput (Utils.name_of_var v)
|
||||
| Some (arr, idx) -> CVStored (arr, idx)
|
||||
end
|
||||
| _ -> failwith "This should not happened."
|
||||
in
|
||||
match expr with
|
||||
| IEVar vsrc ->
|
||||
CAssign (fetch_unique_var (), CVariable vsrc)
|
||||
| IEMonOp (MOp_pre, IEVar v) ->
|
||||
CAssign (fetch_unique_var (), CVariable v)
|
||||
| IEConst c ->
|
||||
CAssign (fetch_unique_var (), CConst c)
|
||||
| IEMonOp (op, e) ->
|
||||
CAssign (fetch_unique_var (),
|
||||
CMonOp (op, iexpression_to_cvalue e))
|
||||
| IEBinOp (op, e, e') ->
|
||||
CAssign (fetch_unique_var (),
|
||||
CBinOp (op, iexpression_to_cvalue e, iexpression_to_cvalue e'))
|
||||
| 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 "should not happened due to the linearization pass."
|
||||
) l
|
||||
| _ -> failwith "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)
|
||||
| IETuple _ -> failwith "linearization should have \
|
||||
transformed the tuples of the right members."
|
||||
| IEWhen (expr, cond) ->
|
||||
begin
|
||||
CIf (iexpression_to_cvalue cond,
|
||||
[equation_to_expression (node_st, node_sts, (vl, expr))],
|
||||
[])
|
||||
end
|
||||
| IETriOp (TOp_if, _, _, _) ->
|
||||
failwith "A pass should have turned conditionnals into merges."
|
||||
| IETriOp (TOp_merge, c, e, e') ->
|
||||
CIf (iexpression_to_cvalue c,
|
||||
[equation_to_expression (node_st, node_sts, (vl, e))],
|
||||
[equation_to_expression (node_st, node_sts, (vl, e'))])
|
||||
| IEReset (IEApp (i, node, b), c) -> CReset (node.n_name, i, iexpression_to_cvalue c, [equation_to_expression (node_st, node_sts, (vl, IEApp (i, node, b)))])
|
||||
| IEReset _ -> failwith "A pass should have turned not function resets into function resets"
|
||||
|
||||
|
||||
|
||||
let rec remove_ifnot = function
|
||||
| [] -> []
|
||||
| CIf (CMonOp (MOp_not, c), bh :: bt, b'h :: b't) :: block ->
|
||||
(CIf (c, b'h :: b't, bh :: bt)) :: (remove_ifnot block )
|
||||
| stmt :: block ->
|
||||
stmt :: (remove_ifnot block)
|
||||
|
||||
let rec merge_neighbour_ifs = function
|
||||
| [] -> []
|
||||
| [stmt] -> [stmt]
|
||||
| CIf (c, e1, e2) :: CIf (c', e'1, e'2) :: b ->
|
||||
begin
|
||||
if c = c' then
|
||||
merge_neighbour_ifs
|
||||
(CIf (c,
|
||||
merge_neighbour_ifs (e1 @ e'1),
|
||||
merge_neighbour_ifs (e2 @ e'2)) :: b)
|
||||
else if c = CMonOp (MOp_not, c') then
|
||||
merge_neighbour_ifs
|
||||
(CIf (c',
|
||||
merge_neighbour_ifs (e2 @ e'1),
|
||||
merge_neighbour_ifs (e1 @ e'2)) :: b)
|
||||
else if c' = CMonOp (MOp_not, c) then
|
||||
merge_neighbour_ifs
|
||||
(CIf (c,
|
||||
merge_neighbour_ifs (e1 @ e'2),
|
||||
merge_neighbour_ifs (e2 @ e'1)) :: b)
|
||||
else CIf (c, e1, e2) :: merge_neighbour_ifs (CIf (c', e'1, e'2) :: b)
|
||||
end
|
||||
| stmt :: stmt' :: b ->
|
||||
stmt :: merge_neighbour_ifs (stmt' :: b)
|
||||
|
75
src/intermediate_ast.ml
Normal file
75
src/intermediate_ast.ml
Normal file
@@ -0,0 +1,75 @@
|
||||
open Ast
|
||||
|
||||
(** A node state is translated into a struct. This struct has:
|
||||
* 1. A name (t_state_<name of the node>)
|
||||
* 2. A number of local and output variables of each type (int, real, bool)
|
||||
* 3-5. mappings that maps
|
||||
* [(variable, is_pre)] to an index of the corresponding array (see below)
|
||||
* where [variable] is of type [t_var], and [is_pre] indicated whether we
|
||||
* deal with pre (x) or x.
|
||||
* 6. A mapping mapping any variable to the name of the C table containing it
|
||||
* and the index at which it is stored (= union of the tables [nt_map_*])
|
||||
* 7. A mapping mapping the output number i to its location (name of the
|
||||
* table that contains it and index.
|
||||
*
|
||||
* Important Note: if a variable x appears behind a pre, it will count as two
|
||||
* variables in the point 2. above..
|
||||
*
|
||||
* It should be translated as follow in C:
|
||||
typedef struct {
|
||||
int ivars[nt_nb_int]; (or nothing if nt_nb_int = 0)
|
||||
int bvars[nt_nb_bool]; (or nothing if nt_nb_bool = 0)
|
||||
int rvars[nt_nb_real]; (or nothing if nt_nb_real = 0)
|
||||
bool is_init;
|
||||
} t_state_<node name>;
|
||||
*)
|
||||
type node_state =
|
||||
{
|
||||
nt_name: string;
|
||||
nt_nb_int : int;
|
||||
nt_nb_real: int;
|
||||
nt_nb_bool: int;
|
||||
nt_map: (ident * bool, string * int) Hashtbl.t;
|
||||
nt_output_map: (int, string * int) Hashtbl.t;
|
||||
nt_prevars: t_var list;
|
||||
nt_count_app: int;
|
||||
}
|
||||
|
||||
|
||||
|
||||
type c_var =
|
||||
| CVStored of string * int
|
||||
| CVInput of ident
|
||||
|
||||
type i_expression =
|
||||
| IEVar of c_var
|
||||
| IEMonOp of monop * i_expression
|
||||
| IEBinOp of binop * i_expression * i_expression
|
||||
| IETriOp of triop * i_expression * i_expression * i_expression
|
||||
| IEComp of compop * i_expression * i_expression
|
||||
| IEWhen of i_expression * i_expression
|
||||
| IEReset of i_expression * i_expression
|
||||
| IEConst of const
|
||||
| IETuple of (i_expression list)
|
||||
(** [CApp] below represents the n-th call to an aux node *)
|
||||
| IEApp of int * t_node * i_expression
|
||||
|
||||
and i_varlist = t_var list
|
||||
|
||||
and i_equation = i_varlist * i_expression
|
||||
|
||||
and i_eqlist = i_equation list
|
||||
|
||||
and i_node =
|
||||
{
|
||||
in_name : ident;
|
||||
in_inputs: i_varlist;
|
||||
in_outputs: i_varlist;
|
||||
in_local_vars: i_varlist;
|
||||
in_equations: i_eqlist;
|
||||
}
|
||||
|
||||
type i_nodelist = i_node list
|
||||
|
||||
type node_states = (ident, node_state) Hashtbl.t
|
||||
|
50
src/intermediate_utils.ml
Normal file
50
src/intermediate_utils.ml
Normal file
@@ -0,0 +1,50 @@
|
||||
open Intermediate_ast
|
||||
|
||||
let rec find_app_opt eqs i =
|
||||
let rec find_app_expr_opt i = function
|
||||
| IEVar _ | IEConst _ -> None
|
||||
| IEMonOp (_, e) -> find_app_expr_opt i e
|
||||
| IEReset (e, e') | IEWhen (e, e') | IEComp (_, e, e') | IEBinOp (_, e, e') ->
|
||||
begin
|
||||
match find_app_expr_opt i e with
|
||||
| None -> find_app_expr_opt i e'
|
||||
| Some n -> Some n
|
||||
end
|
||||
| IETriOp (_, e, e', e'') ->
|
||||
begin
|
||||
match find_app_expr_opt i e with
|
||||
| None ->
|
||||
begin
|
||||
match find_app_expr_opt i e' with
|
||||
| None -> find_app_expr_opt i e''
|
||||
| Some n -> Some n
|
||||
end
|
||||
| Some n -> Some n
|
||||
end
|
||||
| IETuple 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
|
||||
(** [IEApp] below represents the n-th call to an aux node *)
|
||||
| IEApp (j, n, e) ->
|
||||
if i = j
|
||||
then Some n
|
||||
else find_app_expr_opt i e
|
||||
in
|
||||
match eqs with
|
||||
| [] -> None
|
||||
| (_, expr) :: eqs ->
|
||||
match find_app_expr_opt i expr with
|
||||
| None -> find_app_opt eqs i
|
||||
| Some n -> Some n
|
||||
|
||||
let find_varname h v =
|
||||
Hashtbl.fold
|
||||
(fun s e acc ->
|
||||
match acc with
|
||||
| None -> if e = v then Some s else None
|
||||
| Some _ -> acc)
|
||||
h None
|
@@ -14,25 +14,29 @@
|
||||
("returns", RETURNS);
|
||||
("var", VAR);
|
||||
("int", TYP(Ast.TInt));
|
||||
("real", TYP(Ast.TReal));
|
||||
("bool", TYP(Ast.TBool));
|
||||
("<=", CMP_le);
|
||||
(">=", CMP_ge);
|
||||
("not", MO_not);
|
||||
("mod", BO_mod);
|
||||
("&&", BO_and);
|
||||
("and", BO_and);
|
||||
("||", BO_or);
|
||||
("or", BO_or);
|
||||
("<>", CMP_neq);
|
||||
("if", IF);
|
||||
("then", THEN);
|
||||
("else", ELSE);
|
||||
("merge", TO_merge);
|
||||
("when", WHEN);
|
||||
("reset", RESET);
|
||||
("every", EVERY);
|
||||
("pre", MO_pre);
|
||||
("true", CONST_BOOL(true));
|
||||
("false", CONST_BOOL(false));
|
||||
("fby", BO_fby);
|
||||
("automaton", AUTOMAT);
|
||||
("match", MATCH);
|
||||
("with", WITH);
|
||||
("until", UNTIL);
|
||||
("do", DO);
|
||||
("done", DONE);
|
||||
];
|
||||
fun s ->
|
||||
try Hashtbl.find h s with Not_found -> IDENT s
|
||||
@@ -54,13 +58,22 @@ rule token = parse
|
||||
| ';' { SEMICOL }
|
||||
| ':' { COLON }
|
||||
| '<' { CMP_lt }
|
||||
| "<=" { CMP_le }
|
||||
| '>' { CMP_gt }
|
||||
| ">=" { CMP_ge }
|
||||
| "<>" { CMP_neq }
|
||||
| '+' { PLUS }
|
||||
| '-' { MINUS }
|
||||
| '*' { BO_mul }
|
||||
| '/' { BO_div }
|
||||
| '%' { BO_mod }
|
||||
| "->" { BO_arrow }
|
||||
| '|' { CASE }
|
||||
| "--" { read_single_line_comment lexbuf }
|
||||
| eof { EOF }
|
||||
| _ { raise (Lexing_error (Format.sprintf "Erruer à la vue de %s" (lexeme lexbuf)))}
|
||||
| _ { raise (Lexing_error (Format.sprintf "Error when seeing %s" (lexeme lexbuf)))}
|
||||
|
||||
and read_single_line_comment = parse
|
||||
| '\n' { token lexbuf }
|
||||
| eof { EOF }
|
||||
| _ { read_single_line_comment lexbuf }
|
||||
|
@@ -1,36 +1,58 @@
|
||||
open Ast
|
||||
|
||||
let pp_loc fmt (start, stop) =
|
||||
Lexing.(
|
||||
Format.fprintf fmt "%s: <l: %d, c: %d> -- <l: %d, c: %d>"
|
||||
start.pos_fname
|
||||
start.pos_lnum start.pos_cnum
|
||||
stop.pos_lnum stop.pos_cnum)
|
||||
let rec debug_type_pp fmt = function
|
||||
| [] -> ()
|
||||
| TInt :: t -> Format.fprintf fmt "int %a" debug_type_pp t
|
||||
| TBool :: t -> Format.fprintf fmt "bool %a" debug_type_pp t
|
||||
| TReal :: t -> Format.fprintf fmt "real %a" debug_type_pp t
|
||||
|
||||
let pp_loc fmt ((start, stop), file) =
|
||||
let spos, epos =
|
||||
Lexing.(start.pos_cnum, stop.pos_cnum) in
|
||||
let f = open_in file in
|
||||
try
|
||||
begin
|
||||
let rec aux linenum curpos =
|
||||
let line = input_line f in
|
||||
let nextpos = curpos + (String.length line) + 1 in
|
||||
if nextpos >= epos then
|
||||
Format.fprintf fmt "<line %d: %s >" linenum line
|
||||
else
|
||||
aux (linenum + 1) nextpos
|
||||
in
|
||||
aux 1 0;
|
||||
close_in f
|
||||
end
|
||||
with e ->
|
||||
(close_in_noerr f; Format.fprintf fmt "???")
|
||||
|
||||
let rec pp_varlist fmt : t_varlist -> unit = function
|
||||
| (FTList [], []) -> ()
|
||||
| (FTList (FTBase TInt :: _), IVar h :: []) -> Format.fprintf fmt "%s: int" h
|
||||
| (FTList (FTBase TReal :: _), RVar h :: []) -> Format.fprintf fmt "%s: real" h
|
||||
| (FTList (FTBase TBool :: _), BVar h :: []) -> Format.fprintf fmt "%s: bool" h
|
||||
| (FTList (FTBase TInt :: tl), (IVar h) :: h' :: l) ->
|
||||
Format.fprintf fmt "%s: int, %a" h pp_varlist (FTList tl, (h' :: l))
|
||||
| (FTList (FTBase TBool :: tl), (BVar h) :: h' :: l) ->
|
||||
Format.fprintf fmt "%s: bool, %a" h pp_varlist (FTList tl, (h' :: l))
|
||||
| (FTList (FTBase TReal :: tl), (RVar h) :: h' :: l) ->
|
||||
Format.fprintf fmt "%s: real, %a" h pp_varlist (FTList tl, (h' :: l))
|
||||
| _ -> raise (MyTypeError "This exception should not have beed be raised.")
|
||||
| ([], []) -> ()
|
||||
| ([TInt] , IVar h :: []) -> Format.fprintf fmt "%s: int" h
|
||||
| ([TReal], RVar h :: []) -> Format.fprintf fmt "%s: real" h
|
||||
| ([TBool], BVar h :: []) -> Format.fprintf fmt "%s: bool" h
|
||||
| (TInt :: tl, IVar h :: h' :: l) ->
|
||||
Format.fprintf fmt "%s: int, %a" h pp_varlist (tl, h' :: l)
|
||||
| (TBool :: tl, BVar h :: h' :: l) ->
|
||||
Format.fprintf fmt "%s: bool, %a" h pp_varlist (tl, h' :: l)
|
||||
| (TReal :: tl, RVar h :: h' :: l) ->
|
||||
Format.fprintf fmt "%s: real, %a" h pp_varlist (tl, h' :: l)
|
||||
| _ -> raise (MyTypeError "(1) This exception should not have beed be raised.")
|
||||
|
||||
let pp_expression =
|
||||
let upd_prefix s = s ^ " | " in
|
||||
let rec pp_expression_aux prefix fmt expression =
|
||||
let rec pp_expression_list prefix fmt exprs =
|
||||
match exprs with
|
||||
| ETuple(FTList [], []) -> ()
|
||||
| ETuple (FTList (_ :: tt), expr :: exprs) ->
|
||||
| ETuple([], []) -> ()
|
||||
| ETuple (typs, expr :: exprs) ->
|
||||
let typ_h, typ_t =
|
||||
Utils.list_select (List.length (Utils.type_exp expr)) typs in
|
||||
Format.fprintf fmt "%a%a"
|
||||
(pp_expression_aux (prefix^" |> ")) expr
|
||||
(pp_expression_list prefix) (ETuple (FTList tt, exprs))
|
||||
| _ -> raise (MyTypeError "This exception should not have been raised.")
|
||||
(pp_expression_list prefix) (ETuple (typ_t, exprs))
|
||||
| ETuple (_, []) -> failwith "An empty tuple has a type!"
|
||||
| _ -> failwith "This exception should never occur."
|
||||
in
|
||||
match expression with
|
||||
| EWhen (_, e1, e2) ->
|
||||
@@ -40,12 +62,18 @@ let pp_expression =
|
||||
(pp_expression_aux (upd_prefix prefix)) e1
|
||||
(pp_expression_aux (upd_prefix prefix)) e2
|
||||
end
|
||||
| EReset (_, e1, e2) ->
|
||||
begin
|
||||
Format.fprintf fmt "\t\t\t%sRESET\n%a\t\t\tRESET\n%a"
|
||||
prefix
|
||||
(pp_expression_aux (upd_prefix prefix)) e1
|
||||
(pp_expression_aux (upd_prefix prefix)) e2
|
||||
end
|
||||
| EConst (_, c) ->
|
||||
begin match c with
|
||||
| CBool true -> Format.fprintf fmt "\t\t\t%s<true : bool>\n" prefix
|
||||
| CBool false -> Format.fprintf fmt "\t\t\t%s<false : bool>\n" prefix
|
||||
| CInt i -> Format.fprintf fmt "\t\t\t%s<%5d: int>\n" prefix i
|
||||
| CReal r -> Format.fprintf fmt "\t\t\t%s<%5f: float>\n" prefix r
|
||||
| CBool b -> Format.fprintf fmt "\t\t\t%s<%s : bool>\n" prefix (Bool.to_string b)
|
||||
| CInt i -> Format.fprintf fmt "\t\t\t%s<%5d: int>\n" prefix i
|
||||
| CReal r -> Format.fprintf fmt "\t\t\t%s<%5f: real>\n" prefix r
|
||||
end
|
||||
| EVar (_, IVar v) -> Format.fprintf fmt "\t\t\t%s<int var %s>\n" prefix v
|
||||
| EVar (_, BVar v) -> Format.fprintf fmt "\t\t\t%s<bool var %s>\n" prefix v
|
||||
@@ -104,26 +132,54 @@ let pp_expression =
|
||||
(pp_expression_list prefix) args
|
||||
| ETuple _ ->
|
||||
Format.fprintf fmt "\t\t\t%sTuple\n%a" prefix
|
||||
(pp_expression_list prefix) expression;
|
||||
(pp_expression_list prefix) expression
|
||||
in
|
||||
pp_expression_aux ""
|
||||
|
||||
let rec pp_equations fmt: t_eqlist -> unit = function
|
||||
| [] -> ()
|
||||
| (patt, expr) :: eqs ->
|
||||
Format.fprintf fmt "\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)
|
||||
pp_varlist patt
|
||||
pp_expression expr
|
||||
pp_equations eqs
|
||||
|
||||
let rec pp_automata fmt: t_automaton list -> unit = function
|
||||
| [] -> ()
|
||||
| (_, trans)::tail ->
|
||||
Format.fprintf fmt "\t\t* Automaton : \n%a%a"
|
||||
pp_translist trans
|
||||
pp_automata tail
|
||||
|
||||
and pp_nexts fmt: t_expression list * string list -> unit = function
|
||||
| [], [] -> ()
|
||||
| e::exprs, n::nexts ->
|
||||
Format.fprintf fmt "if %a then %s else %a"
|
||||
pp_expression e
|
||||
n
|
||||
pp_nexts (exprs, nexts)
|
||||
| _, _ -> () (*This should never happen*)
|
||||
|
||||
and pp_translist fmt: t_state list -> unit = function
|
||||
| [] -> ()
|
||||
| State(name, eqs, cond, next)::q ->
|
||||
Format.fprintf fmt "\t\t\t|%s -> do\n%a\n\t\t\tdone until %a \n%a"
|
||||
name
|
||||
pp_equations eqs
|
||||
pp_nexts (cond, next)
|
||||
pp_translist q
|
||||
|
||||
let pp_node fmt node =
|
||||
Format.fprintf fmt "\t∗ Nom du nœud : %s\n\t Inputs:\n%a\n\t Outputs:\n%a\n\t\
|
||||
\ \ Local variables:\n%a\n\t Equations:\n%a\n"
|
||||
Format.fprintf fmt "\t∗ Node name : %s\n\t Inputs:\n%a\n\t Outputs:\n%a\n\t\
|
||||
\ \ Local variables:\n%a\n\t Equations:\n%a\n\t Automata:\n%a\n"
|
||||
node.n_name
|
||||
pp_varlist node.n_inputs
|
||||
pp_varlist node.n_outputs
|
||||
pp_varlist node.n_local_vars
|
||||
pp_equations node.n_equations
|
||||
pp_automata node.n_automata
|
||||
|
||||
let rec pp_nodes fmt nodes =
|
||||
match nodes with
|
||||
@@ -133,7 +189,7 @@ let rec pp_nodes fmt nodes =
|
||||
|
||||
let pp_ast fmt prog =
|
||||
Format.fprintf fmt
|
||||
"Le programme est composé de %d nœud(s), listés ci-dessous :\n%a"
|
||||
"The program is made of %d node(s), listed below :\n%a"
|
||||
(List.length prog)
|
||||
pp_nodes prog
|
||||
|
150
src/main.ml
150
src/main.ml
@@ -9,37 +9,63 @@ let print_debug d s =
|
||||
let print_verbose v s =
|
||||
if v then Format.printf "\x1b[33;01;04mStatus:\x1b[0m %s\n" s else ()
|
||||
|
||||
(** The following function should check whether the program is well-formed, by
|
||||
* induction:
|
||||
* - for any applications of the form (n, arg1, ..., argn)
|
||||
* + n exists
|
||||
* + n waits n arguments
|
||||
* + arg1, ..., argn sont bien formés
|
||||
* - The expressions are well-typed
|
||||
* - The equations are well typed
|
||||
* - The output is set
|
||||
*)
|
||||
let check_well_formedness (a: t_nodelist) = Some a
|
||||
let check_dependencies (a: t_nodelist) = Some a
|
||||
let simplify_prog (a: t_nodelist) = Some a
|
||||
|
||||
let run verbose debug (passes: (t_nodelist -> t_nodelist option) list)
|
||||
= verbose "kjlksjf"
|
||||
|
||||
(** [exec_passes] executes the passes on the parsed typed-AST.
|
||||
* A pass should return [Some program] in case of a success, and [None]
|
||||
* otherwise.
|
||||
*
|
||||
* The function [exec_passes] returns the optionnal program returned by the
|
||||
* last pass.
|
||||
*
|
||||
* A pass should never be interrupted by an exception. Nevertheless, we make
|
||||
* sure that no pass raise one. *)
|
||||
let exec_passes ast verbose debug passes f =
|
||||
let rec aux ast = function
|
||||
| [] -> f ast
|
||||
| (n, p) :: passes ->
|
||||
verbose (Format.asprintf "Executing pass %s:\n" n);
|
||||
match p verbose debug ast with
|
||||
| None -> (exit_error ("Error while in the pass "^n^".\n"); exit 0)
|
||||
| Some ast -> (
|
||||
debug
|
||||
(Format.asprintf
|
||||
"Current AST (after %s):\n%a\n" n Lustre_pp.pp_ast ast);
|
||||
aux ast passes)
|
||||
in
|
||||
aux ast passes
|
||||
|
||||
|
||||
|
||||
let _ =
|
||||
(** Usage and argument parsing. *)
|
||||
let default_passes = ["check_form"; "check_dependencies"; "simplify_prog"] in
|
||||
let usage_msg = "Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] [-o output_file] source_file" in
|
||||
let default_passes =
|
||||
["linearization_reset"; "automata_translation"; "remove_if";
|
||||
"linearization_merge"; "linearization_when";
|
||||
"linearization_pre"; "linearization_tuples"; "linearization_app";
|
||||
"ensure_assign_val";
|
||||
"equations_ordering";
|
||||
"clock_unification"] in
|
||||
let sanity_passes = ["sanity_pass_assignment_unicity"; "check_typing"] in
|
||||
let usage_msg =
|
||||
"Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \
|
||||
[-o output_file] [-m main_function] source_file\n" in
|
||||
let verbose = ref false in
|
||||
let debug = ref false in
|
||||
let ppast = ref false in
|
||||
let nopopt = ref false in
|
||||
let passes = ref [] in
|
||||
let source_file = ref "" in
|
||||
let testopt = ref false in
|
||||
let output_file = ref "out.c" in
|
||||
let anon_fun filename = source_file := filename in
|
||||
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");
|
||||
("-nop", Arg.Set nopopt, "Only computes the AST and execute the passes");
|
||||
("-verbose", Arg.Set verbose, "Output some debug information");
|
||||
("-debug", Arg.Set debug, "Output a lot of debug information");
|
||||
("-p", Arg.String (fun s -> passes := s :: !passes),
|
||||
@@ -50,44 +76,94 @@ let _ =
|
||||
if !source_file = "" then exit_error "No source file specified" else
|
||||
if !passes = [] then passes := default_passes;
|
||||
let print_verbose = print_verbose !verbose in
|
||||
let print_debug = print_debug !verbose in
|
||||
let print_debug = print_debug !debug in
|
||||
|
||||
(** Definition of the passes table *)
|
||||
let passes_table : (string, t_nodelist -> t_nodelist option) Hashtbl.t = Hashtbl.create 100 in
|
||||
let passes_table = Hashtbl.create 100 in
|
||||
List.iter (fun (s, k) -> Hashtbl.add passes_table s k)
|
||||
[
|
||||
("check_form", check_well_formedness);
|
||||
("check_dependencies", check_dependencies);
|
||||
("simplify_prog", simplify_prog);
|
||||
("remove_if", Passes.pass_if_removal);
|
||||
("linearization_merge", Passes.pass_merge_lin);
|
||||
("linearization_when", Passes.pass_when_lin);
|
||||
("linearization_tuples", Passes.pass_linearization_tuples);
|
||||
("linearization_app", Passes.pass_linearization_app);
|
||||
("linearization_pre", Passes.pass_linearization_pre);
|
||||
("ensure_assign_val", Passes.pass_ensure_assignment_value);
|
||||
("linearization_reset", Passes.pass_linearization_reset);
|
||||
("sanity_pass_assignment_unicity", Passes.sanity_pass_assignment_unicity);
|
||||
("automata_translation", Passes.automata_translation_pass);
|
||||
("automata_validity", Passes.check_automata_validity);
|
||||
("equations_ordering", Passes.pass_eq_reordering);
|
||||
("check_typing", Passes.pass_typing);
|
||||
("clock_unification", Passes.clock_unification_pass);
|
||||
];
|
||||
|
||||
(** Main functionnalyty below *)
|
||||
(** Main functionality below *)
|
||||
print_verbose "Parsing the source file...";
|
||||
let ast =
|
||||
let inchan = open_in !source_file in
|
||||
try
|
||||
begin
|
||||
let inchan = open_in !source_file in
|
||||
(**let _ = Parsing.set_trace true in*)
|
||||
let res = Parser.main Lexer.token (Lexing.from_channel inchan) in
|
||||
close_in inchan; res
|
||||
end
|
||||
with
|
||||
| Lexer.Lexing_error s ->
|
||||
(exit_error (Format.sprintf "Code d'erreur:\n\t%s\n\n" s); exit 0)
|
||||
(close_in_noerr inchan;
|
||||
exit_error (Format.sprintf "Error code:\n\t%s\n\n" s); exit 0)
|
||||
| Utils.MyParsingError (s, l) ->
|
||||
begin
|
||||
close_in_noerr inchan;
|
||||
Format.printf "Syntax error at %a: %s\n\n"
|
||||
Pp.pp_loc l s;
|
||||
Lustre_pp.pp_loc (l, !source_file) s;
|
||||
exit 0
|
||||
end in
|
||||
end
|
||||
| Parsing.Parse_error ->
|
||||
begin
|
||||
close_in_noerr inchan;
|
||||
Parsing.(
|
||||
Format.printf "Syntax error at %a\n\n"
|
||||
Lustre_pp.pp_loc ((symbol_start_pos (), symbol_end_pos()), !source_file));
|
||||
exit 0
|
||||
end
|
||||
in
|
||||
|
||||
if !ppast then Format.printf "%a" Pp.pp_ast ast
|
||||
else
|
||||
let passes = List.map (fun (pass: string) ->
|
||||
match Hashtbl.find_opt passes_table pass with
|
||||
| None ->
|
||||
(exit_error (Format.sprintf "The pass %s does not exist." pass); exit 0)
|
||||
| Some f ->
|
||||
(print_debug ("The pass "^pass^" has been selected."); f)) !passes in
|
||||
run print_verbose print_debug passes;
|
||||
print_verbose "End of the program, exiting gracefully."
|
||||
(** Computes the list of passes to execute. If the [-test] flag is set, all
|
||||
* sanity passes (ie. passes which do not modify the AST, but ensure its
|
||||
* validity) are re-run after any other pass.
|
||||
*
|
||||
* Note: the sanity passes are always executed before any other. *)
|
||||
let passes =
|
||||
List.map
|
||||
(fun (pass: string) -> (pass,
|
||||
match Hashtbl.find_opt passes_table pass with
|
||||
| None ->
|
||||
(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"
|
||||
Lustre_pp.pp_ast ast) ;
|
||||
exec_passes ast print_verbose print_debug passes
|
||||
begin
|
||||
if !ppast
|
||||
then (Format.printf "%a" Lustre_pp.pp_ast)
|
||||
else (
|
||||
if !nopopt
|
||||
then (fun _ -> ())
|
||||
else
|
||||
(
|
||||
let oc = open_out !output_file in
|
||||
let fmt = Format.make_formatter
|
||||
(Stdlib.output_substring oc)
|
||||
(fun () -> Stdlib.flush oc) in
|
||||
Ast_to_c.ast_to_c fmt print_verbose print_debug);
|
||||
)
|
||||
end
|
||||
|
||||
|
268
src/parser.mly
268
src/parser.mly
@@ -2,11 +2,12 @@
|
||||
open Ast
|
||||
open Utils
|
||||
|
||||
let bloop () = Format.printf "bloop\n"
|
||||
let current_location () = symbol_start_pos (), symbol_end_pos ()
|
||||
|
||||
let defined_nodes : (ident, t_node) Hashtbl.t = Hashtbl.create 100
|
||||
let defined_nodes : (ident, t_node) Hashtbl.t = Hashtbl.create Config.maxvar
|
||||
|
||||
let defined_vars : (ident, t_var) Hashtbl.t = Hashtbl.create 100
|
||||
let defined_vars : (ident, t_var) Hashtbl.t = Hashtbl.create Config.maxvar
|
||||
|
||||
let fetch_node (n: ident) =
|
||||
match Hashtbl.find_opt defined_nodes n with
|
||||
@@ -22,44 +23,33 @@
|
||||
("The var "^n^" does not exist.", current_location()))
|
||||
| Some var -> var
|
||||
|
||||
let type_var (v: t_var) =
|
||||
match v with
|
||||
| IVar _ -> FTBase TInt
|
||||
| BVar _ -> FTBase TBool
|
||||
| RVar _ -> FTBase TReal
|
||||
(*
|
||||
let fetch_var_def (n: ident) : t_var =
|
||||
match Hashtbl.find_opt defined_vars n with
|
||||
| None ->
|
||||
raise (MyParsingError
|
||||
("The var "^n^" does not exist.", current_location()))
|
||||
| Some (var, true) ->
|
||||
raise (MyParsingError
|
||||
("The variable "^n^" is defined for the second time.",
|
||||
current_location()))
|
||||
| Some (var, false) ->
|
||||
(Hashtbl.replace defined_vars n (var, true) ; var)
|
||||
*)
|
||||
|
||||
let type_exp : t_expression -> full_ty = function
|
||||
| EVar (full_ty , _) -> full_ty
|
||||
| EMonOp (full_ty , _ , _) -> full_ty
|
||||
| EBinOp (full_ty , _ , _ , _) -> full_ty
|
||||
| ETriOp (full_ty , _ , _ , _ , _) -> full_ty
|
||||
| EComp (full_ty , _ , _ , _) -> full_ty
|
||||
| EWhen (full_ty , _ , _) -> full_ty
|
||||
| EConst (full_ty , _) -> full_ty
|
||||
| ETuple (full_ty , _) -> full_ty
|
||||
| EApp (full_ty , _ , _) -> full_ty
|
||||
|
||||
let concat_varlist (t1, e1) (t2, e2) =
|
||||
(
|
||||
match t1, t2 with
|
||||
| FTList lt1, FTList lt2 -> (FTList (lt1 @ lt2), e1@e2)
|
||||
| _ ->
|
||||
raise (MyParsingError ("This exception should not have been raised.",
|
||||
current_location())))
|
||||
let concat_varlist (t1, e1) (t2, e2) = (t1 @ t2, e1 @ e2)
|
||||
|
||||
let make_ident (v : t_var) : t_varlist =
|
||||
match v with
|
||||
| IVar _ -> (FTList [FTBase TInt ], [v])
|
||||
| BVar _ -> (FTList [FTBase TBool], [v])
|
||||
| RVar _ -> (FTList [FTBase TReal], [v])
|
||||
| IVar _ -> [TInt ], [v]
|
||||
| BVar _ -> [TBool], [v]
|
||||
| RVar _ -> [TReal], [v]
|
||||
|
||||
let add_ident (v : t_var) (l: t_varlist) : t_varlist =
|
||||
match v, l with
|
||||
| IVar _, (FTList tl, l) -> (FTList (FTBase TInt :: tl), v :: l)
|
||||
| BVar _, (FTList tl, l) -> (FTList (FTBase TBool :: tl), v :: l)
|
||||
| RVar _, (FTList tl, l) -> (FTList (FTBase TReal :: tl), v :: l)
|
||||
| _ -> raise (MyParsingError ("This exception should not have been raised.",
|
||||
current_location()))
|
||||
| IVar _, (tl, l) -> ((TInt :: tl), v :: l)
|
||||
| BVar _, (tl, l) -> ((TBool :: tl), v :: l)
|
||||
| RVar _, (tl, l) -> ((TReal :: tl), v :: l)
|
||||
|
||||
let monop_condition expr typ_constraint error_msg res =
|
||||
if type_exp expr = typ_constraint
|
||||
@@ -73,37 +63,44 @@
|
||||
|
||||
let make_binop_nonbool e1 e2 op error_msg =
|
||||
let t1 = type_exp e1 in let t2 = type_exp e2 in
|
||||
match t1 with
|
||||
| FTBase _ -> (** e1 and e2 should be nunmbers here.*)
|
||||
if t1 = t2 && t1 <> FTBase TBool
|
||||
then EBinOp (t1, op, e1, e2)
|
||||
else raise (MyParsingError (error_msg, current_location()))
|
||||
| _ -> raise (MyParsingError (error_msg, current_location()))
|
||||
(** e1 and e2 should be numbers here.*)
|
||||
if list_chk t1 [[TInt]; [TReal]] && list_chk t2 [[TInt]; [TReal]]
|
||||
then
|
||||
begin
|
||||
if t1 = t2
|
||||
then EBinOp (t1, op, e1, e2)
|
||||
else raise (MyParsingError (error_msg, current_location()))
|
||||
end
|
||||
else raise (MyParsingError (error_msg, current_location()))
|
||||
|
||||
let make_binop_bool e1 e2 op error_msg =
|
||||
let t1 = type_exp e1 in let t2 = type_exp e2 in
|
||||
if t1 = t2 && t1 = FTBase TBool
|
||||
if t1 = t2 && t1 = [TBool]
|
||||
then EBinOp (t1, op, e1, e2)
|
||||
else raise (MyParsingError (error_msg, current_location()))
|
||||
|
||||
let make_comp e1 e2 op error_msg =
|
||||
let t1 = type_exp e1 in let t2 = type_exp e2 in
|
||||
if t1 = t2
|
||||
then EComp (FTBase TBool, op, e1, e2)
|
||||
(** e1 and e2 should not be tuples *)
|
||||
if t1 = t2 && List.length t1 = 1
|
||||
then EComp ([TBool], op, e1, e2)
|
||||
else raise (MyParsingError (error_msg, current_location()))
|
||||
|
||||
let make_comp_nonbool e1 e2 op error_msg =
|
||||
let t1 = type_exp e1 in let t2 = type_exp e2 in
|
||||
match t1 with
|
||||
| FTBase _ -> (** e1 and e2 should be numbers here. *)
|
||||
if t1 = t2 && t1 <> FTBase TBool
|
||||
then EComp (FTBase TBool, op, e1, e2)
|
||||
else raise (MyParsingError (error_msg, current_location()))
|
||||
| _ -> raise (MyParsingError (error_msg, current_location()))
|
||||
(** e1 and e2 should be numbers here.*)
|
||||
if list_chk t1 [[TInt]; [TReal]] && list_chk t2 [[TInt]; [TReal]]
|
||||
then
|
||||
begin
|
||||
if t1 = t2
|
||||
then EComp ([TBool], op, e1, e2)
|
||||
else raise (MyParsingError (error_msg, current_location()))
|
||||
end
|
||||
else raise (MyParsingError (error_msg, current_location()))
|
||||
|
||||
let make_tertiary e1 e2 e3 op error_msg =
|
||||
let t1 = type_exp e1 in let t2 = type_exp e2 in let t3 = type_exp e3 in
|
||||
if t2 = t3 && t1 = FTBase TBool
|
||||
if t2 = t3 && t1 = [TBool]
|
||||
then ETriOp (t2, op, e1, e2, e3)
|
||||
else raise (MyParsingError (error_msg, current_location()))
|
||||
|
||||
@@ -118,6 +115,7 @@
|
||||
%token COLON
|
||||
%token BOOL
|
||||
%token INT
|
||||
%token REAL
|
||||
%token LET
|
||||
%token TEL
|
||||
%token NODE
|
||||
@@ -145,15 +143,31 @@
|
||||
%token TO_merge
|
||||
|
||||
%token WHEN
|
||||
%token RESET
|
||||
%token EVERY
|
||||
|
||||
%token IF
|
||||
%token THEN
|
||||
%token ELSE
|
||||
|
||||
%token AUTOMAT
|
||||
%token CASE
|
||||
%token MATCH
|
||||
%token WITH
|
||||
%token DO
|
||||
%token DONE
|
||||
%token UNTIL
|
||||
|
||||
%token<int> CONST_INT
|
||||
%token<bool> CONST_BOOL
|
||||
%token<Ast.real> CONST_REAL
|
||||
|
||||
%left MO_not
|
||||
%left MO_pre
|
||||
%left PLUS
|
||||
%left MINUS
|
||||
%left BO_and BO_or BO_mul BO_div BO_mod BO_arrow BO_fby TO_merge
|
||||
|
||||
/* The Entry Point */
|
||||
%start main
|
||||
%type <Ast.t_nodelist> main
|
||||
@@ -172,10 +186,11 @@ node:
|
||||
|
||||
node_content:
|
||||
IDENT LPAREN in_params RPAREN
|
||||
RETURNS LPAREN out_params RPAREN SEMICOL
|
||||
RETURNS LPAREN out_params RPAREN OPTIONAL_SEMICOL
|
||||
local_params
|
||||
LET equations TEL
|
||||
LET node_body TEL OPTIONAL_SEMICOL
|
||||
{ let node_name = $1 in
|
||||
let (eqs, aut) = $12 in
|
||||
let (t_in, e_in) = $3 in
|
||||
let (t_out, e_out) = $7 in
|
||||
let n: t_node =
|
||||
@@ -183,19 +198,48 @@ node_content:
|
||||
n_inputs = (t_in, e_in);
|
||||
n_outputs = (t_out, e_out);
|
||||
n_local_vars = $10;
|
||||
n_equations = $12;
|
||||
n_type = FTArr (t_in, t_out); } in
|
||||
Hashtbl.add defined_nodes node_name n; n };
|
||||
n_equations = eqs;
|
||||
n_automata = aut; } in
|
||||
if List.length t_in = 0
|
||||
then raise (MyParsingError
|
||||
(Format.asprintf "The node %s should have arguments."
|
||||
node_name,
|
||||
current_location()))
|
||||
else
|
||||
begin
|
||||
if Hashtbl.find_opt defined_nodes node_name <> None
|
||||
then raise (MyParsingError
|
||||
(Format.asprintf "The node %s is already defined."
|
||||
node_name,
|
||||
current_location()))
|
||||
else
|
||||
if vars_distinct e_in e_out (snd $10)
|
||||
then (Hashtbl.add defined_nodes node_name n; n)
|
||||
else raise (MyParsingError
|
||||
("There is a conflict between the names of local,\
|
||||
input or output variables.",
|
||||
current_location()))
|
||||
end};
|
||||
|
||||
node_body:
|
||||
| /* empty */ { ([], []) }
|
||||
| equations node_body { let (eq, aut) = $2 in ($1@eq, aut) }
|
||||
| automaton node_body { let (eq, aut) = $2 in (eq, $1::aut) }
|
||||
|
||||
OPTIONAL_SEMICOL:
|
||||
| /* empty */ {}
|
||||
| SEMICOL {}
|
||||
;
|
||||
|
||||
in_params:
|
||||
| /* empty */ { (FTList [], []) }
|
||||
| /* empty */ { ([], []) }
|
||||
| param_list { $1 }
|
||||
;
|
||||
|
||||
out_params: param_list { $1 } ;
|
||||
|
||||
local_params:
|
||||
| /* empty */ { (FTList [], []) }
|
||||
| /* empty */ { ([], []) }
|
||||
| VAR param_list_semicol { $2 }
|
||||
;
|
||||
|
||||
@@ -212,17 +256,17 @@ param:
|
||||
ident_comma_list COLON TYP
|
||||
{ let typ = $3 in
|
||||
let idents = $1 in
|
||||
(
|
||||
(FTList
|
||||
(List.map
|
||||
(fun t -> FTBase t) (list_repeat (List.length idents) typ)),
|
||||
(list_repeat (List.length idents) typ,
|
||||
match typ with
|
||||
| TBool ->
|
||||
List.map (fun s -> Hashtbl.add defined_vars s (BVar s); BVar s) idents
|
||||
List.map (fun s ->
|
||||
Hashtbl.add defined_vars s (BVar s); BVar s) idents
|
||||
| TReal ->
|
||||
List.map (fun s -> Hashtbl.add defined_vars s (RVar s); RVar s) idents
|
||||
List.map (fun s ->
|
||||
Hashtbl.add defined_vars s (RVar s); RVar s) idents
|
||||
| TInt ->
|
||||
List.map (fun s -> Hashtbl.add defined_vars s (IVar s); IVar s) idents)) }
|
||||
List.map (fun s ->
|
||||
Hashtbl.add defined_vars s (IVar s); IVar s) idents) }
|
||||
;
|
||||
|
||||
ident_comma_list:
|
||||
@@ -233,22 +277,24 @@ equations:
|
||||
| /* empty */ { [] }
|
||||
| equation SEMICOL equations
|
||||
{ $1 :: $3 }
|
||||
| equation OPTIONAL_SEMICOL { [$1] }
|
||||
;
|
||||
|
||||
equation:
|
||||
pattern EQUAL expr
|
||||
| pattern EQUAL expr
|
||||
{ let (t_patt, patt) = $1 in
|
||||
let expr = $3 in
|
||||
if type_exp expr = t_patt
|
||||
let expr = $3 in let texpr = type_exp expr in
|
||||
if t_patt = texpr
|
||||
then ((t_patt, patt), expr)
|
||||
else raise (MyParsingError ("The equation does not type check!",
|
||||
current_location())) };
|
||||
else (raise (MyParsingError ("The equation does not type check!",
|
||||
current_location()))) };
|
||||
automaton:
|
||||
| AUTOMAT transition_list { (List.hd $2, $2)}
|
||||
;
|
||||
|
||||
pattern:
|
||||
| IDENT
|
||||
{ let v = fetch_var $1 in
|
||||
(FTList [type_var v], [v])
|
||||
}
|
||||
{ let v = fetch_var $1 in (type_var v, [v]) }
|
||||
| LPAREN ident_comma_list_patt RPAREN { $2 };
|
||||
|
||||
ident_comma_list_patt:
|
||||
@@ -261,39 +307,39 @@ expr:
|
||||
| IDENT { let v = fetch_var $1 in EVar (type_var v, v) }
|
||||
/* Unary operators */
|
||||
| MO_not expr
|
||||
{ monop_condition $2 (FTBase TBool)
|
||||
{ monop_condition $2 [TBool]
|
||||
"You cannot negate a non-boolean expression."
|
||||
(EMonOp (type_exp $2, MOp_not, $2)) }
|
||||
| MO_pre expr { EMonOp (type_exp $2, MOp_pre, $2) }
|
||||
| MINUS expr
|
||||
{ monop_neg_condition $2 (FTBase TBool)
|
||||
"You cannot take the opposite of a boolean expression."
|
||||
{ monop_neg_condition $2 [TBool]
|
||||
"You cannot take the opposite of an expression that is not a number."
|
||||
(EMonOp (type_exp $2, MOp_minus, $2)) }
|
||||
| PLUS expr
|
||||
{ monop_neg_condition $2 (FTBase TBool)
|
||||
"You cannot take the plus of a boolean expression." $2 }
|
||||
{ monop_neg_condition $2 [TBool]
|
||||
"(+) expects its argument to be a number." $2 }
|
||||
/* Binary operators */
|
||||
| expr PLUS expr
|
||||
{ make_binop_nonbool $1 $3 BOp_add
|
||||
"You should know better; addition hates booleans" }
|
||||
"Addition expects both arguments to be (the same kind of) numbers." }
|
||||
| expr MINUS expr
|
||||
{ make_binop_nonbool $1 $3 BOp_sub
|
||||
"You should know better; subtraction hates booleans" }
|
||||
"Substraction expects both arguments to be (the same kind of) numbers." }
|
||||
| expr BO_mul expr
|
||||
{ make_binop_nonbool $1 $3 BOp_mul
|
||||
"You should know better; multiplication hates booleans" }
|
||||
"Multiplication expects both arguments to be (the same kind of) numbers." }
|
||||
| expr BO_div expr
|
||||
{ make_binop_nonbool $1 $3 BOp_div
|
||||
"You should know better; division hates booleans" }
|
||||
"Division expects both arguments to be (the same kind of) numbers." }
|
||||
| expr BO_mod expr
|
||||
{ make_binop_nonbool $1 $3 BOp_mod
|
||||
"You should know better; modulo hates booleans" }
|
||||
"Modulo expects both arguments to be numbers." }
|
||||
| expr BO_and expr
|
||||
{ make_binop_bool $1 $3 BOp_and
|
||||
"You should know better; conjunction hates numbers" }
|
||||
"Conjunction expects both arguments to be booleans." }
|
||||
| expr BO_or expr
|
||||
{ make_binop_bool $1 $3 BOp_or
|
||||
"You should know better; disjunction hates numbers" }
|
||||
"Disjunction expects both arguments to be booleans." }
|
||||
| expr BO_arrow expr
|
||||
{ let e1 = $1 in let t1 = type_exp e1 in
|
||||
let e2 = $3 in let t2 = type_exp e2 in
|
||||
@@ -332,31 +378,38 @@ expr:
|
||||
| expr WHEN expr
|
||||
{ let e1 = $1 in let t1 = type_exp e1 in
|
||||
let e2 = $3 in let t2 = type_exp e2 in
|
||||
if t2 = FTBase TBool
|
||||
then EWhen (type_exp $1, $1, $3)
|
||||
if t2 = [TBool]
|
||||
then EWhen (t1, e1, e2)
|
||||
else raise (MyParsingError ("The when does not type-check!",
|
||||
current_location())) }
|
||||
| RESET expr EVERY expr
|
||||
{ let e1 = $2 in let t1 = type_exp e1 in
|
||||
let e2 = $4 in let t2 = type_exp e2 in
|
||||
if t2 = [TBool]
|
||||
then EReset (t1, e1, e2)
|
||||
else raise (MyParsingError ("The reset does not type-check!",
|
||||
current_location())) }
|
||||
/* Constants */
|
||||
| CONST_INT { EConst (FTBase TInt, CInt $1) }
|
||||
| CONST_BOOL { EConst (FTBase TBool, CBool $1) }
|
||||
| CONST_REAL { EConst (FTBase TReal, CReal $1) }
|
||||
| CONST_INT { EConst ([TInt], CInt $1) }
|
||||
| CONST_BOOL { EConst ([TBool], CBool $1) }
|
||||
| CONST_REAL { EConst ([TReal], CReal $1) }
|
||||
/* Tuples */
|
||||
| LPAREN expr_comma_list RPAREN { $2 }
|
||||
/* Applications */
|
||||
| IDENT LPAREN RPAREN
|
||||
{ raise (MyParsingError ("An application should come with arguments!",
|
||||
current_location())) }
|
||||
| IDENT LPAREN expr_comma_list RPAREN
|
||||
{ let name = $1 in
|
||||
let node = fetch_node name in
|
||||
let args = $3 in
|
||||
match node.n_type with
|
||||
| FTArr (tin, t) ->
|
||||
if tin = type_exp args
|
||||
then EApp (t, fetch_node name, args)
|
||||
else raise (MyParsingError ("The application does not type check!",
|
||||
current_location()))
|
||||
| _ -> raise (MyParsingError ("This exception should not have been \
|
||||
raised from the dead.",
|
||||
if type_exp args = fst node.n_inputs
|
||||
then EApp (fst node.n_outputs, fetch_node name, args)
|
||||
else raise (MyParsingError ("The application does not type check!",
|
||||
current_location()))
|
||||
}
|
||||
|
||||
/* Automaton */
|
||||
;
|
||||
|
||||
expr_comma_list:
|
||||
@@ -364,13 +417,13 @@ expr_comma_list:
|
||||
{ let e = $1 in
|
||||
match e with
|
||||
| ETuple _ -> e
|
||||
| _ -> ETuple (FTList [type_exp e], [e]) }
|
||||
| _ -> ETuple (type_exp e, [e]) }
|
||||
| expr COMMA expr_comma_list
|
||||
{ let e = $1 in
|
||||
let le = $3 in
|
||||
match e, le with
|
||||
| ETuple (FTList l1, t), ETuple (FTList l2, t') -> ETuple (FTList (l1@l2), t @ t')
|
||||
| _, ETuple (FTList lt, t') -> ETuple (FTList ((type_exp e)::lt), e :: t')
|
||||
| ETuple (l1, t), ETuple (l2, t') -> ETuple (l1 @ l2, t @ t')
|
||||
| _, ETuple (lt, t') -> ETuple (((type_exp e) @ lt), e :: t')
|
||||
| _, _ -> raise (MyParsingError ("This exception should not have been \
|
||||
raised.",
|
||||
current_location())) }
|
||||
@@ -381,4 +434,21 @@ ident_comma_list:
|
||||
| IDENT COMMA ident_comma_list { $1 :: $3 }
|
||||
;
|
||||
|
||||
transition:
|
||||
| CASE IDENT BO_arrow DO equations DONE {
|
||||
State($2, $5, [EConst([TBool], CBool(true))], [$2]) }
|
||||
| CASE IDENT BO_arrow DO equations UNTIL next_list {
|
||||
let (exprs, outs) = $7 in
|
||||
State($2, $5, exprs, outs)}
|
||||
;
|
||||
|
||||
transition_list:
|
||||
| transition { [$1] }
|
||||
| transition transition_list { $1 :: $2 }
|
||||
| /* empty */ {raise(MyParsingError("Empty automaton", current_location()))}
|
||||
;
|
||||
|
||||
next_list:
|
||||
| expr THEN IDENT { [$1], [$3] }
|
||||
| next_list ELSE IF expr THEN IDENT { let (exprs, outs) = $1 in $4::exprs, $6::outs }
|
||||
;
|
||||
|
1251
src/passes.ml
Normal file
1251
src/passes.ml
Normal file
File diff suppressed because it is too large
Load Diff
41
src/passes_utils.ml
Normal file
41
src/passes_utils.ml
Normal file
@@ -0,0 +1,41 @@
|
||||
open Ast
|
||||
|
||||
(** [node_pass] is an auxiliary function used to write passes: it will iterate
|
||||
* the function passed as argument on all the nodes of the program *)
|
||||
let node_pass f ast: t_nodelist option =
|
||||
Utils.list_map_option f ast
|
||||
|
||||
(** [equation_pass] is an auxiliary function used to write passes: it will
|
||||
* iterate the function passed as argument on all the equations of the
|
||||
* program *)
|
||||
let equation_pass (f: t_equation -> t_equation option) ast: t_nodelist option =
|
||||
let aux (node: t_node): t_node option =
|
||||
match Utils.list_map_option f node.n_equations with
|
||||
| None -> None
|
||||
| Some eqs -> Some {n_name = node.n_name;
|
||||
n_inputs = node.n_inputs;
|
||||
n_outputs = node.n_outputs;
|
||||
n_local_vars = node.n_local_vars;
|
||||
n_equations = eqs;
|
||||
n_automata = node.n_automata;
|
||||
}
|
||||
in
|
||||
node_pass aux ast
|
||||
|
||||
let expression_pass f: t_nodelist -> t_nodelist option =
|
||||
let aux (patt, expr) =
|
||||
match f expr with
|
||||
| None -> None
|
||||
| Some expr -> Some (patt, expr)
|
||||
in
|
||||
equation_pass aux
|
||||
|
||||
exception PassExn of string
|
||||
|
||||
let counter = ref 0
|
||||
let create_automaton_id : unit -> int = fun () ->
|
||||
counter := !counter + 1;
|
||||
!counter
|
||||
|
||||
let create_automaton_name id =
|
||||
Format.asprintf "_s%d" (id)
|
@@ -1,12 +1,25 @@
|
||||
node diagonal_int (i: int) returns (o1, o2 : int);
|
||||
node id_int (i: int) returns (o: int);
|
||||
let
|
||||
(o1, o2) = (i, i);
|
||||
o = i -> i;
|
||||
tel
|
||||
|
||||
node undiag_test (i: int) returns (o : bool);
|
||||
var l1, l2: int; l3: int;
|
||||
node aux (i, j: int) returns (o: int);
|
||||
let
|
||||
l3 = 1 -> 0;
|
||||
(l1, l2) = diagonal_int(i);
|
||||
o = (not (not (l1 = l2))) and (l1 = l2) and true;
|
||||
o = id_int(i) + id_int(j);
|
||||
tel
|
||||
|
||||
node main (i: int) returns (a, b: int);
|
||||
var tmp: int;
|
||||
let
|
||||
a = 1;
|
||||
b = aux (i, a);
|
||||
tmp = aux (a+b, i);
|
||||
tel
|
||||
|
||||
node test (u, v: int; c: bool) returns (o: int);
|
||||
var x, y: int; b: bool;
|
||||
let
|
||||
x = merge c u v;
|
||||
o = 2 * x;
|
||||
tel
|
||||
|
||||
|
15
src/test2.node
Normal file
15
src/test2.node
Normal file
@@ -0,0 +1,15 @@
|
||||
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);
|
||||
var u1, u2, t1, t2: int; c: bool;
|
||||
let
|
||||
c = true -> not pre c;
|
||||
(t1, t2) = aux (i) when c;
|
||||
(u1, u2) = aux (i) when (not c);
|
||||
o1 = merge c t1 u1;
|
||||
o2 = merge c t2 u2;
|
||||
tel
|
110
src/utils.ml
110
src/utils.ml
@@ -1,4 +1,112 @@
|
||||
open Ast
|
||||
|
||||
let rec list_select n = function
|
||||
| [] -> [], []
|
||||
| h :: t ->
|
||||
if n = 0
|
||||
then ([], h :: t)
|
||||
else
|
||||
let p1, p2 = list_select (n-1) t in
|
||||
h :: p1, p2
|
||||
|
||||
let rec list_remove_duplicates l =
|
||||
match l with
|
||||
| [] -> []
|
||||
| h :: t ->
|
||||
let t = list_remove_duplicates t in
|
||||
if List.mem h t then t else h :: t
|
||||
|
||||
let rec list_map_option (f: 'a -> 'b option) (l: 'a list) : 'b list option =
|
||||
List.fold_right (fun elt acc ->
|
||||
match acc, f elt with
|
||||
| None, _ | _, None -> None
|
||||
| Some acc, Some elt -> Some (elt :: acc)) l (Some [])
|
||||
|
||||
let rec list_repeat n elt =
|
||||
if n = 0 then [] else elt :: (list_repeat (n-1) elt)
|
||||
|
||||
exception MyParsingError of (string * Ast.location)
|
||||
let rec list_chk v = function
|
||||
| [] -> false
|
||||
| h :: t -> if h = v then true else list_chk v t
|
||||
|
||||
let rec vars_distinct lv lv' lv'' =
|
||||
match lv, lv', lv'' with
|
||||
| [], [], _ -> true
|
||||
| [], h :: t , l'' ->
|
||||
if List.mem h l''
|
||||
then false
|
||||
else vars_distinct [] t l''
|
||||
| h :: t, l', l'' ->
|
||||
if List.mem h l' || List.mem h l''
|
||||
then false
|
||||
else vars_distinct t l' l''
|
||||
|
||||
exception MyParsingError of (string * location)
|
||||
|
||||
let type_const = function
|
||||
| CReal _ -> [TReal]
|
||||
| CInt _ -> [TInt ]
|
||||
| CBool _ -> [TBool]
|
||||
|
||||
let type_var (v: t_var) =
|
||||
match v with
|
||||
| IVar _ -> [TInt]
|
||||
| BVar _ -> [TBool]
|
||||
| RVar _ -> [TReal]
|
||||
|
||||
let type_exp : t_expression -> full_ty = function
|
||||
| EVar (full_ty , _) -> full_ty
|
||||
| EMonOp (full_ty , _ , _) -> full_ty
|
||||
| EBinOp (full_ty , _ , _ , _) -> full_ty
|
||||
| ETriOp (full_ty , _ , _ , _ , _) -> full_ty
|
||||
| EComp (full_ty , _ , _ , _) -> full_ty
|
||||
| EWhen (full_ty , _ , _) -> full_ty
|
||||
| EReset (full_ty , _ , _) -> full_ty
|
||||
| EConst (full_ty , _) -> full_ty
|
||||
| ETuple (full_ty , _) -> full_ty
|
||||
| EApp (full_ty , _ , _) -> full_ty
|
||||
|
||||
let somify f = fun e -> Some (f e)
|
||||
|
||||
let name_of_var: t_var -> ident = function
|
||||
| IVar s -> s
|
||||
| BVar s -> s
|
||||
| RVar s -> s
|
||||
|
||||
let rec fresh_var_name (l: t_varlist) n : ident =
|
||||
let rec aux acc n =
|
||||
let r = Random.int 26 in
|
||||
Format.asprintf "%c%s"
|
||||
(char_of_int (r + (if Random.bool () then 65 else 97)))
|
||||
(if n = 0 then acc else aux acc (n-1))
|
||||
in
|
||||
let name = aux "" n in
|
||||
if List.filter (fun v -> name_of_var v = name) (snd l) = []
|
||||
then name
|
||||
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)
|
||||
|
||||
let split_patt (patt: t_varlist) (e: t_expression): t_varlist * t_varlist =
|
||||
let pl, pr = list_select (List.length (type_exp e)) (snd patt) in
|
||||
let tl = List.flatten (List.map type_var pl) in
|
||||
let tr = List.flatten (List.map type_var pr) in
|
||||
(tl, pl), (tr, pr)
|
||||
|
||||
|
4
tests/arrow.node
Normal file
4
tests/arrow.node
Normal file
@@ -0,0 +1,4 @@
|
||||
node main (i: int) returns (o: int);
|
||||
let
|
||||
o = 1 -> 2 -> 3;
|
||||
tel
|
22
tests/automaton.node
Normal file
22
tests/automaton.node
Normal file
@@ -0,0 +1,22 @@
|
||||
node diagonal_int (i: int) returns (o1, o2 : int);
|
||||
let
|
||||
(o1, o2) = (i, i);
|
||||
tel
|
||||
|
||||
node undiag_test (i: int) returns (o : bool);
|
||||
var l1, l2: int; l3: int;
|
||||
let
|
||||
l3 = (pre (1)) -> 0;
|
||||
(l1, l2) = diagonal_int(i);
|
||||
o = (not (not (l1 = l2))) and (l1 = l2) and true;
|
||||
tel
|
||||
|
||||
node main (i: int) returns (o : int);
|
||||
var x, y:int;
|
||||
let
|
||||
automaton
|
||||
| Incr -> do (o,x) = (0 fby o + 1, 2); until x > 0 then Decr else if x = o then Done
|
||||
| Decr -> do (o,x) = diagonal_int(0 fby o); until x < o then Incr
|
||||
| Done -> do o = pre o; done
|
||||
tel
|
||||
|
16
tests/counting.node
Normal file
16
tests/counting.node
Normal file
@@ -0,0 +1,16 @@
|
||||
-- count the number of top between two tick
|
||||
node counting (tick:bool; top:bool)
|
||||
returns (o: int);
|
||||
var v, o1: int;
|
||||
let o = if tick then v else 0 -> (pre o) + v;
|
||||
v = if top then 1 else 0
|
||||
tel;
|
||||
|
||||
node main (i: int)
|
||||
returns (o: int);
|
||||
let
|
||||
-- 0 means no `tick` and no `top`
|
||||
-- 1 means `tick`
|
||||
-- 2 means `top`
|
||||
o = counting(i = 1, i = 2)
|
||||
tel;
|
4
tests/pre.node
Normal file
4
tests/pre.node
Normal file
@@ -0,0 +1,4 @@
|
||||
node main (i: int) returns (o: bool);
|
||||
let
|
||||
o = pre (true and pre( i = pre(pre(i))));
|
||||
tel
|
15
tests/reset.node
Normal file
15
tests/reset.node
Normal file
@@ -0,0 +1,15 @@
|
||||
-- counter of `top`s until `reset` condition holds
|
||||
node counting (tick: bool) returns (o: int);
|
||||
var v: int;
|
||||
let
|
||||
o = v -> (pre o) + v;
|
||||
v = if tick then 1 else 0
|
||||
tel
|
||||
|
||||
node main (i: int) returns (o: int);
|
||||
let
|
||||
-- 0 means no `top` and no `reset`
|
||||
-- 1 means `top`
|
||||
-- 2 means `reset`
|
||||
o = reset counting(i = 1) every (i = 2);
|
||||
tel
|
11
tests/tuple.node
Normal file
11
tests/tuple.node
Normal file
@@ -0,0 +1,11 @@
|
||||
node diagonal_int (i: int) returns (o1, o2 : int);
|
||||
let
|
||||
(o1, o2) = (i, i);
|
||||
tel
|
||||
|
||||
node main (i: int) returns (o1, o2, o3, o4: int);
|
||||
let
|
||||
(o1, o2) = diagonal_int(i);
|
||||
(o3, o4) = diagonal_int(o1);
|
||||
tel
|
||||
|
13
tests/when_merge.node
Normal file
13
tests/when_merge.node
Normal file
@@ -0,0 +1,13 @@
|
||||
node test (i: real) returns (o: real);
|
||||
var x, y: real;
|
||||
let
|
||||
x = (1.0 / i) when (i <> 0.0);
|
||||
y = 0.0 when (not (i <> 0.0));
|
||||
o = merge (i <> 0.0) x y;
|
||||
tel
|
||||
|
||||
node main (i: real) returns (o: real);
|
||||
let
|
||||
-- The idea is to pass `0.0` as the input to acknowledge that the division by zero isn't computed.
|
||||
o = test(i);
|
||||
tel
|
Reference in New Issue
Block a user