beamer/beamer.tex

@@ -1,169 +0,0 @@
-\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}
-

src/simulation.ml

@@ -1,92 +0,0 @@
-open Ast
-
-type sim_var =
-  | SIVar of ident * (int option)
-  | SBVar of ident * (bool option)
-  | SRVar of ident * (real option)
-
-type sim_node_st =
-  {
-    node_outputs: sim_var list;
-    node_loc_vars: sim_var list;
-    node_inner_nodes: sim_node list;
-  }
-and sim_node_step_fn =
-  sim_node_st -> sim_var list -> (sim_var list * sim_node_st)
-and sim_node = sim_node_st * sim_node_step_fn
-
-let pp_sim fmt ((sn, _): sim_node) =
-  let rec aux fmt vars =
-    match vars with
-    | [] -> ()
-    | SIVar (s, None) :: t ->
-        Format.fprintf fmt "\t<%s : int> uninitialized yet.\n%a" s aux t
-    | SBVar (s, None) :: t ->
-        Format.fprintf fmt "\t<%s : bool> uninitialized yet.\n%a" s aux t
-    | SRVar (s, None) :: t ->
-        Format.fprintf fmt "\t<%s : real> uninitialized yet.\n%a" s aux t
-    | SIVar (s, Some i) :: t ->
-        Format.fprintf fmt "\t<%s : 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
-