Changeset 1317 for Deliverables/D3.2/Report
- Timestamp:
- Oct 7, 2011, 12:28:46 PM (9 years ago)
- File:
-
- 1 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}
Note: See TracChangeset
for help on using the changeset viewer.