Compare commits

...

2 Commits

Author SHA1 Message Date
dsac
e84a6e387d [beamer] proto 0 2022-12-15 11:40:29 +01:00
dsac
ed5f94f821 [simu] wip 2022-12-15 09:13:59 +01:00
4 changed files with 261 additions and 0 deletions

169
beamer/beamer.tex Normal file
View File

@ -0,0 +1,169 @@
\documentclass{beamer}
\usepackage{tikz}
%\usepackage{minted}
\usetikzlibrary{positioning}
\usetheme{Darmstadt}
\begin{document}
\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}
%type _ t_var =
% | BVar: ident -> bool t_var
% | IVar: ident -> int t_var
% | RVar: ident -> real t_var
%
%type _ t_expression =
% | EVar: 'a t_var -> 'a t_expression
% | EMonOp: monop * 'a t_expression -> 'a t_expression
% | EBinOp: binop * 'a t_expression * 'a t_expression -> 'a t_expression
% | ETriOp: triop * bool t_expression * 'a t_expression * 'a t_expression -> 'a t_expression
% | EComp: compop * 'a t_expression * 'a t_expression -> bool t_expression
% | EConst: 'a const -> 'a t_expression
% | ETuple: 'a t_expression * 'b t_expression -> ('a * 'b) t_expression
% | EApp: (('a -> 'b) t_node) * 'a t_expression -> 'b t_expression
%
%and _ t_varlist =
% | NVar: 'a t_varlist
% | CVar: 'a t_var * 'b t_varlist -> ('a * 'b) t_varlist
%
%and 'a t_equation = 'a t_varlist * 'a t_expression
%
%and _ t_eqlist =
% | NEql: unit t_eqlist
% | CEql: 'a t_equation * 'b t_eqlist -> ('a * 'b) t_eqlist
%
%and _ t_node =
% | MakeNode:
% ident
% * 'i t_varlist * 'o t_varlist
% * 'l t_varlist * 'e t_eqlist
% -> ('i -> 'o) t_node
%
%type _ t_nodelist =
% | NNode: unit t_nodelist
% | CNode: ('a -> 'b) t_node * 'c t_nodelist -> (('a -> 'b) * 'c) t_nodelist
% \end{minted}
\end{frame}
\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}{Passes}
\begin{block}
The passes of our compiler are functions of taking a program and either:
\begin{itemize}
\item returning a program if the pass succeeded
\item returns nothing otherwise
\end{itemize}
We only have one language in our compiler: no intermediary language.
\end{block}
\end{frame}
\subsection{Check}
\begin{frame}
\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}
\begin{frame}{Implemented passes}
\begin{block}{\texttt{pre}-propagation to leaves}
\end{block}
\begin{block}{Check: unique initialization for variables}
\end{block}
\begin{block}{Linearization of the equations}
\end{block}
\end{frame}
\end{document}

Binary file not shown.

After

Width:  |  Height:  |  Size: 155 KiB

BIN
beamer/imgs/gadt.png Normal file

Binary file not shown.

After

Width:  |  Height:  |  Size: 139 KiB

92
src/simulation.ml Normal file
View File

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