Changeset 1317 for Deliverables
 Timestamp:
 Oct 7, 2011, 12:28:46 PM (10 years ago)
 Location:
 Deliverables
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.2/Report/report.tex
r1277 r1317 365 365 record internal_function : Type[0] ≝ 366 366 { 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) 369 369 ; f_stacksize : nat 370 370 ; 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_body371 ; 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 373 373 }. 374 374 \end{lstlisting} … … 383 383 (Env:expr_vars ty e (present ?? env)) 384 384 (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' with388 [ Id _ i ⇒ λEnv.385 : $\Sigma$f':partial_fn le. fn_graph_included le f f' ≝ 386 match 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. 389 389 let r ≝ lookup_reg env i Env in 390 390 ... … … 400 400 on variables needed by \lstinline'add_expr' and its equivalent on statements: 401 401 \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 →402 lemma 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$ 405 405 present ?? e' i. 406 406 \end{lstlisting} 
Deliverables/D3.3/Report/report.tex
r1267 r1317 226 226 \begin{lstlisting} 227 227 inductive identifier (tag:String) : Type[0] ≝ 228 an_identifier : Word →identifier tag.228 an_identifier : Word $\rightarrow$ identifier tag. 229 229 \end{lstlisting} 230 230 The tries are also tagged in the same manner. These tags have also proved … … 276 276 \textsf{RTLabs} stage (see the accompanying deliverable 3.2 for details): 277 277 \begin{lstlisting} 278 inductive expr : typ →Type[0] ≝279  Id : ∀t. ident →expr t280  Cst : ∀t. constant →expr t281  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 t284  Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t →expr t285  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. 286 286 \end{lstlisting} 287 287 For example, note that conditional expressions only switch on integer … … 315 315 \begin{lstlisting}[language=matita] 316 316 inductive statement : Type[0] ≝ 317  St_skip : label →statement318  St_cost : costlabel → label →statement319  St_const : register → constant → label →statement320  St_op1 : unary_operation → register → register → label →statement317  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 321 321 ... 322 322  St_return : statement 323 323 . 324 324 325 definition graph : Type[0] →Type[0] ≝ identifier_map LabelTag.325 definition graph : Type[0] $\rightarrow$ Type[0] ≝ identifier_map LabelTag. 326 326 327 327 record internal_function : Type[0] ≝ 328 328 { f_labgen : universe LabelTag 329 329 ; 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) 333 333 ; f_stacksize : nat 334 334 ; f_graph : graph statement … … 403 403 integers in the exit and switch statements: 404 404 \begin{lstlisting}[language=matita] 405 inductive stmt : ∀blockdepth:nat. Type[0] ≝406  St_skip : ∀n. stmt n405 inductive stmt : $\forall$blockdepth:nat. Type[0] ≝ 406  St_skip : $\forall$n. stmt n 407 407 ... 408  St_loop : ∀n. stmt n →stmt n409  St_block : ∀n. stmt (S n) →stmt n410  St_exit : ∀n. Fin n →stmt n408  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 411 411 (* expr to switch on, table of <switch value, #blocks to exit>, default *) 412  St_switch : expr → ∀n. list (int × (Fin n)) → Fin n →stmt n412  St_switch : expr $\rightarrow$ $\forall$n. list (int $\times$ (Fin n)) $\rightarrow$ Fin n $\rightarrow$ stmt n 413 413 ... 414 414 \end{lstlisting} … … 433 433 a predicate to all substatements: 434 434 \begin{lstlisting}[language=matita] 435 let rec stmt_P (P:stmt →Prop) (s:stmt) on s : Prop ≝435 let rec stmt_P (P:stmt $\rightarrow$ Prop) (s:stmt) on s : Prop ≝ 436 436 match s with 437 [ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧stmt_P P s2438  St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧stmt_P P s2439  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 s437 [ 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 444 444 ]. 445 445 \end{lstlisting} … … 459 459 record internal_function : Type[0] ≝ 460 460 { 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) 463 463 ; f_stacksize : nat 464 464 ; 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_body465 ; 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 467 467 }. 468 468 \end{lstlisting}
Note: See TracChangeset
for help on using the changeset viewer.