Changeset 1397 for Deliverables/D4.2-4.3

Timestamp:

Oct 17, 2011, 6:37:58 PM (9 years ago)

Author:

mulligan

Message:

more changes, talking about parameters

File:

• Deliverables/D4.2-4.3/reports/D4-3.tex (modified) (2 diffs)

Deliverables/D4.2-4.3/reports/D4-3.tex

@@ -162 +162 @@
 % SECTION.                                                                    %
 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
+\subsection{Type parameters, and their purpose}
+\label{subsect.type.parameters.their.purpose}
+
+We mentioned in the Deliverable D4.2 report that all joint languages are parameterised by a number of types, which are later specialised to each distinct intermediate language.
+As this parameterisation process is also dependent on designs decisions in the language semantics, we have so far held off summarising the role of each parameter.
+We now summarise what each parameter is.
+
+\begin{lstlisting}
+record params__: Type[1] ≝
+{
+  acc_a_reg: Type[0];
+  acc_b_reg: Type[0];
+  dpl_reg: Type[0];
+  dph_reg: Type[0];
+  pair_reg: Type[0];
+  generic_reg: Type[0];
+  call_args: Type[0];
+  call_dest: Type[0];
+  extend_statements: Type[0]
+}.
+\end{lstlisting}
+
+As mentioned in the report for Deliverable D4.2, the record \texttt{params\_\_} is enough to be able to specify the instructions of the joint languages:
+\begin{lstlisting}
+inductive joint_instruction (p: params__) (globals: list ident): Type[0] :=
+  | COMMENT: String → joint_instruction p globals
+  | COST_LABEL: costlabel → joint_instruction p globals
+  ...
+\end{lstlisting}
+
+We extend \texttt{params\_\_} with a type corresponding 
+\begin{lstlisting}
+record params_: Type[1] ≝
+{
+  pars__ :> params__;
+  succ: Type[0]
+}.
+\end{lstlisting}
+
+\begin{lstlisting}
+inductive joint_statement (p:params_) (globals: list ident): Type[0] :=
+  | sequential: joint_instruction p globals → succ p → joint_statement p globals
+  | GOTO: label → joint_statement p globals
+  | RETURN: joint_statement p globals.
+\end{lstlisting}
+
+\begin{lstlisting}
+record params0: Type[1] ≝
+ { pars__' :> params__
+ ; resultT: Type[0]
+ ; paramsT: Type[0]
+ }.
+\end{lstlisting}
+
+\begin{lstlisting}
+record params1 : Type[1] ≝
+ { pars0 :> params0
+ ; localsT: Type[0]
+ }.
+\end{lstlisting}
+
+\begin{lstlisting}
+record params (globals: list ident): Type[1] ≝
+ { succ_ : Type[0]
+ ; pars1 :> params1
+ ; codeT: Type[0]
+ ; lookup: codeT → label → option (joint_statement (mk_params_ pars1 succ_) globals)
+ }.
+\end{lstlisting}
+
+\begin{lstlisting}
+definition graph_params_: params__ $\rightarrow$ params_ :=
+  $\lambda$pars__. mk_params_ pars__ label.
+\end{lstlisting}
+
+\begin{lstlisting}
+record joint_internal_function (globals: list ident) (p:params globals) : Type[0] :=
+{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
+  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
+(*  joint_if_sig: signature;  -- dropped in front end *)
+  joint_if_result   : resultT p;
+  joint_if_params   : paramsT p;
+  joint_if_locals   : localsT p;
+(*CSC: XXXXX stacksize unused for LTL-...*)
+  joint_if_stacksize: nat;
+  joint_if_code     : codeT … p;
+(*CSC: XXXXX entry unused for LIN, but invariant in that case... *)
+  joint_if_entry    : $\Sigma$l: label. lookup … joint_if_code l ≠ None ?;
+(*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *)
+  joint_if_exit     : $\Sigma$l: label. lookup … joint_if_code l ≠ None ?
+}.
+\end{lstlisting}
+
+%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
+% SECTION.                                                                    %
+%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
 \subsection{Use of monads}
 \label{subsect.use.of.monads}
@@ -178 +274 @@
 For instance, in the semantics of RTLabs, we make use of the error monad to signal bad final states:
 \begin{lstlisting}
-...
-| Returnstate v dst fs m $\Rightarrow$
-  match fs with
-  [ nil ⇒ Error $\ldots$ (msg FinalState) (* Already in final state *)
-  | cons f fs' $\Rightarrow$
-    ! locals $\leftarrow$ match dst with
-    [ None $\Rightarrow$
-      match v with
-      [ None $\Rightarrow$ OK $\ldots$ (locals f)
-      | _ $\Rightarrow$ Error $\ldots$ (msg ReturnMismatch)
-      ]
-    | Some d $\Rightarrow$
-      match v with
-      [ None $\Rightarrow$ Error $\ldots$ (msg ReturnMismatch)
-      | Some v' $\Rightarrow$ reg_store d v' (locals f)
-      ]
-    ];
-    ret $\ldots$ $\langle$E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m$\rangle$
-  ]
-...
+XXX better example
 \end{lstlisting}
 \item