Changeset 1317


Ignore:
Timestamp:
Oct 7, 2011, 12:28:46 PM (8 years ago)
Author:
campbell
Message:

Fix listings in D3.2/D3.3.

Location:
Deliverables
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.2/Report/report.tex

    r1277 r1317  
    365365record internal_function : Type[0] ≝
    366366{ f_return    : option typ
    367 ; f_params    : list (ident × typ)
    368 ; f_vars      : list (ident × typ)
     367; f_params    : list (ident $\times$ typ)
     368; f_vars      : list (ident $\times$ typ)
    369369; f_stacksize : nat
    370370; f_body      : stmt
    371 ; f_inv       : stmt_P (λs.stmt_vars (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars)) s ∧
    372                            stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of f_body)) s) f_body
     371; f_inv       : stmt_P ($\lambda$s.stmt_vars ($\lambda$i.Exists ? ($\lambda$x.\fst x = i) (f_params @ f_vars)) s $\wedge$
     372                           stmt_labels ($\lambda$l.Exists ? ($\lambda$l'.l' = l) (labels_of f_body)) s) f_body
    373373}.
    374374\end{lstlisting}
     
    383383                   (Env:expr_vars ty e (present ?? env))
    384384                   (dst:register) (f:partial_fn le) on e
    385      : Σf':partial_fn le. fn_graph_included le f f' ≝
    386 match e return λty,e.expr_vars ty e (present ?? env) →
    387                  Σf':partial_fn le. fn_graph_included le f f' with
    388 [ Id _ i ⇒ λEnv.
     385     : $\Sigma$f':partial_fn le. fn_graph_included le f f' ≝
     386match e return $\lambda$ty,e.expr_vars ty e (present ?? env) $\rightarrow$
     387                 $\Sigma$f':partial_fn le. fn_graph_included le f f' with
     388[ Id _ i $\Rightarrow$ $\lambda$Env.
    389389    let r ≝ lookup_reg env i Env in
    390390    ...
     
    400400on variables needed by \lstinline'add_expr' and its equivalent on statements:
    401401\begin{lstlisting}[language=matita]
    402 lemma populates_env : l,e,u,l',e',u'.
    403   populate_env e u l = 〈l',e',u'〉 →
    404   ∀i. Exists ? (λx.\fst x = i) l →
     402lemma populates_env : $\forall$l,e,u,l',e',u'.
     403  populate_env e u l = $\langle$l',e',u'$\rangle$ $\rightarrow$
     404  $\forall$i. Exists ? ($\lambda$x.\fst x = i) l $\rightarrow$
    405405      present ?? e' i.
    406406\end{lstlisting}
  • Deliverables/D3.3/Report/report.tex

    r1267 r1317  
    226226\begin{lstlisting}
    227227    inductive identifier (tag:String) : Type[0] ≝
    228       an_identifier : Word identifier tag.
     228      an_identifier : Word $\rightarrow$ identifier tag.
    229229\end{lstlisting}
    230230The tries are also tagged in the same manner.  These tags have also proved
     
    276276\textsf{RTLabs} stage (see the accompanying deliverable 3.2 for details):
    277277\begin{lstlisting}
    278     inductive expr : typ Type[0] ≝
    279     | Id : ∀t. ident → expr t
    280     | Cst : ∀t. constant → expr t
    281     | Op1 : ∀t,t'. unary_operation → expr t → expr t'
    282     | Op2 : ∀t1,t2,t'. binary_operation → expr t1 → expr t2 → expr t'
    283     | Mem : ∀t,r. memory_chunk → expr (ASTptr r) → expr t
    284     | Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
    285     | Ecost : ∀t. costlabel → expr t → expr t.
     278    inductive expr : typ $\rightarrow$ Type[0] ≝
     279    | Id : $\forall$t. ident $\rightarrow$ expr t
     280    | Cst : $\forall$t. constant $\rightarrow$ expr t
     281    | Op1 : $\forall$t,t'. unary_operation $\rightarrow$ expr t $\rightarrow$ expr t'
     282    | Op2 : $\forall$t1,t2,t'. binary_operation $\rightarrow$ expr t1 $\rightarrow$ expr t2 $\rightarrow$ expr t'
     283    | Mem : $\forall$t,r. memory_chunk $\rightarrow$ expr (ASTptr r) $\rightarrow$ expr t
     284    | Cond : $\forall$sz,sg,t. expr (ASTint sz sg) $\rightarrow$ expr t $\rightarrow$ expr t $\rightarrow$ expr t
     285    | Ecost : $\forall$t. costlabel $\rightarrow$ expr t $\rightarrow$ expr t.
    286286\end{lstlisting}
    287287For example, note that conditional expressions only switch on integer
     
    315315\begin{lstlisting}[language=matita]
    316316inductive statement : Type[0] ≝
    317 | St_skip : label statement
    318 | St_cost : costlabel → label → statement
    319 | St_const : register → constant → label → statement
    320 | St_op1 : unary_operation → register → register → label → statement
     317| St_skip : label $\rightarrow$ statement
     318| St_cost : costlabel $\rightarrow$ label $\rightarrow$ statement
     319| St_const : register $\rightarrow$ constant $\rightarrow$ label $\rightarrow$ statement
     320| St_op1 : unary_operation $\rightarrow$ register $\rightarrow$ register $\rightarrow$ label $\rightarrow$ statement
    321321...
    322322| St_return : statement
    323323.
    324324
    325 definition graph : Type[0] Type[0] ≝ identifier_map LabelTag.
     325definition graph : Type[0] $\rightarrow$ Type[0] ≝ identifier_map LabelTag.
    326326
    327327record internal_function : Type[0] ≝
    328328{ f_labgen    : universe LabelTag
    329329; f_reggen    : universe RegisterTag
    330 ; f_result    : option (register × typ)
    331 ; f_params    : list (register × typ)
    332 ; f_locals    : list (register × typ)
     330; f_result    : option (register $\times$ typ)
     331; f_params    : list (register $\times$ typ)
     332; f_locals    : list (register $\times$ typ)
    333333; f_stacksize : nat
    334334; f_graph     : graph statement
     
    403403integers in the exit and switch statements:
    404404\begin{lstlisting}[language=matita]
    405     inductive stmt : blockdepth:nat. Type[0] ≝
    406     | St_skip : n. stmt n
     405    inductive stmt : $\forall$blockdepth:nat. Type[0] ≝
     406    | St_skip : $\forall$n. stmt n
    407407    ...
    408     | St_loop : ∀n. stmt n → stmt n
    409     | St_block : ∀n. stmt (S n) → stmt n
    410     | St_exit : ∀n. Fin n → stmt n
     408    | St_loop : $\forall$n. stmt n $\rightarrow$ stmt n
     409    | St_block : $\forall$n. stmt (S n) $\rightarrow$ stmt n
     410    | St_exit : $\forall$n. Fin n $\rightarrow$ stmt n
    411411    (* expr to switch on, table of <switch value, #blocks to exit>, default *)
    412     | St_switch : expr → ∀n. list (int × (Fin n)) → Fin n → stmt n
     412    | St_switch : expr $\rightarrow$ $\forall$n. list (int $\times$ (Fin n)) $\rightarrow$ Fin n $\rightarrow$ stmt n
    413413    ...
    414414\end{lstlisting}
     
    433433a predicate to all substatements:
    434434\begin{lstlisting}[language=matita]
    435 let rec stmt_P (P:stmt Prop) (s:stmt) on s : Prop ≝
     435let rec stmt_P (P:stmt $\rightarrow$ Prop) (s:stmt) on s : Prop ≝
    436436match s with
    437 [ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
    438 | St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
    439 | St_loop s' ⇒ P s ∧ stmt_P P s'
    440 | St_block s' ⇒ P s ∧ stmt_P P s'
    441 | St_label _ s' ⇒ P s ∧ stmt_P P s'
    442 | St_cost _ s' ⇒ P s ∧ stmt_P P s'
    443 | _ P s
     437[ St_seq s1 s2 $\Rightarrow$ P s $\wedge$ stmt_P P s1 $\wedge$ stmt_P P s2
     438| St_ifthenelse _ _ _ s1 s2 $\Rightarrow$ P s $\wedge$ stmt_P P s1 $\wedge$ stmt_P P s2
     439| St_loop s' $\Rightarrow$ P s $\wedge$ stmt_P P s'
     440| St_block s' $\Rightarrow$ P s $\wedge$ stmt_P P s'
     441| St_label _ s' $\Rightarrow$ P s $\wedge$ stmt_P P s'
     442| St_cost _ s' $\Rightarrow$ P s $\wedge$ stmt_P P s'
     443| _ $\Rightarrow$ P s
    444444].
    445445\end{lstlisting}
     
    459459record internal_function : Type[0] ≝
    460460{ f_return    : option typ
    461 ; f_params    : list (ident × typ)
    462 ; f_vars      : list (ident × typ)
     461; f_params    : list (ident $\times$ typ)
     462; f_vars      : list (ident $\times$ typ)
    463463; f_stacksize : nat
    464464; f_body      : stmt
    465 ; f_inv       : stmt_P (λs.stmt_vars (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars)) s ∧
    466                            stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of f_body)) s) f_body
     465; f_inv       : stmt_P ($\lambda$s.stmt_vars ($\lambda$i.Exists ? ($\lambda$x.\fst x = i) (f_params @ f_vars)) s $\wedge$
     466                           stmt_labels ($\lambda$l.Exists ? ($\lambda$l'.l' = l) (labels_of f_body)) s) f_body
    467467}.
    468468\end{lstlisting}
Note: See TracChangeset for help on using the changeset viewer.