Ignore:
Timestamp:
Aug 4, 2011, 1:55:53 PM (9 years ago)
Author:
campbell
Message:

Tidy up branch

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma

    r1100 r1102  
    33include "Clight/TypeComparison.ma".
    44include "utilities/lists.ma".
     5include "utilities/deppair.ma".
    56(*
    67let rec mem_vars_expr (mem_vars:identifier_set SymbolTag) (e:expr) on e : Prop ≝
     
    205206qed.
    206207
    207 lemma contract_pair : ∀A,B.∀e:A×B. (let 〈a,b〉 ≝ e in 〈a,b〉) = e.
    208 #A #B * // qed.
    209 
    210 lemma extract_pair : ∀A,B,C,D.  ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
    211 ((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
    212 ∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
    213 #A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.
    214 
    215208include "utilities/extralib.ma". (* for pair_eq1 to work around destruct's excessive normalisation *)
    216209
     
    434427λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e.
    435428
    436 notation "hvbox(« term 19 a, break term 19 b»)"
    437 with precedence 90 for @{ (dp ?? $a $b) }.
    438 
    439 lemma sig_ok : ∀A:Type[0]. ∀P:A → Prop. ∀x:Σx:A.P x.
    440   P x.
    441 #A #P * #a #p @p
    442 qed.
    443 
    444429definition translate_cast : ∀P.type → ∀ty2:type. (Σe:CMexpr ?. expr_vars ? e P) → res (Σe':CMexpr (typ_of_type ty2). expr_vars ? e' P) ≝
    445430λP,ty1,ty2.
     
    474459    ]
    475460| _ ⇒ λ_. Error ? (msg TypeMismatch)
    476 ]. whd @sig_ok qed.
     461]. whd @use_sig qed.
    477462
    478463definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝
     
    504489  ]
    505490] qed.
    506 
    507 definition bind_eq ≝ λA,B:Type[0]. λf: res A. λg: ∀a:A. f = OK ? a → res B.
    508   match f return λx. f = x → ? with
    509   [ OK x ⇒ g x
    510   | Error msg ⇒ λ_. Error ? msg
    511   ] (refl ? f).
    512 
    513 notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
    514491
    515492let rec translate_expr (vars:var_types) (e:expr) on e : res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) ≝
     
    675652[ >E @I
    676653| >(E ? (refl ??)) @refl
    677 | 3,4: @sig_ok
    678 | @(translate_binop_vars … E) @sig_ok
    679 | % [ % ] @sig_ok
    680 | % [ % @sig_ok ] whd @I
    681 | % [ % [ @sig_ok | @I ] | @sig_ok ]
    682 | % [ @sig_ok | @I ]
    683 | % [ @sig_ok | @I ]
     654| 3,4: @use_sig
     655| @(translate_binop_vars … E) @use_sig
     656| % [ % ] @use_sig
     657| % [ % @use_sig ] whd @I
     658| % [ % [ @use_sig | @I ] | @use_sig ]
     659| % [ @use_sig | @I ]
     660| % [ @use_sig | @I ]
    684661| >(access_mode_typ … E) @refl
    685 | @sig_ok
    686 | @sig_ok
    687 | % [ @sig_ok | @I ]
     662| @use_sig
     663| @use_sig
     664| % [ @use_sig | @I ]
    688665] qed.
    689666
     
    789766].
    790767#ls whd %
    791 [ % // @sig_ok
     768[ % // @use_sig
    792769| @I
    793 | % @sig_ok
     770| % @use_sig
    794771| @I
    795772] qed.
     
    806783  do e' ← translate_expr v e;
    807784  OK (Σe:(Σt:typ.CMexpr t).?) ««?, e'», ?».
    808 whd @sig_ok
     785whd @use_sig
    809786qed.
    810787
    811788axiom FIXME : String.
    812 
    813 let rec mmap_sigma (A,B:Type[0]) (P:B → Prop) (f:A → res (Σx:B.P x)) (l:list A) on l : res (Σl':list B.All B P l') ≝
    814 match l with
    815 [ nil ⇒ OK ? «nil B, ?»
    816 | cons h t ⇒
    817     do h' ← f h;
    818     do t' ← mmap_sigma A B P f t;
    819     OK ? «cons B h' t', ?»
    820 ].
    821 whd // %
    822 [ @(sig_ok B P)
    823 | cases t' #l' #p @p
    824 ] qed.
    825789
    826790lemma lookup_label_hit : ∀lbls,l,l'.
     
    842806#vars #lbls #s #s' @proj2
    843807qed.
    844 
    845 lemma Exists_append : ∀A,P,l1,l2.
    846   Exists A P (l1@l2) →
    847   Exists A P l1 ∨ Exists A P l2.
    848 #A #P #l1 elim l1
    849 [ #l2 #H %2 @H
    850 | #h #t #IH #l2 whd in ⊢ (% → ?) *
    851   [ #H %1 %1 @H
    852   | #H cases (IH l2 H) /4/
    853   ]
    854 ] qed.
    855 
    856 lemma Exists_append_l : ∀A,P,l1,l2.
    857   Exists A P l1 → Exists A P (l1@l2).
    858 #A #P #l1 #l2 elim l1
    859 [ *
    860 | #h #t #IH *
    861   [ #H %1 @H
    862   | #H %2 @IH @H
    863   ]
    864 ] qed.
    865 
    866 lemma Exists_append_r : ∀A,P,l1,l2.
    867   Exists A P l2 → Exists A P (l1@l2).
    868 #A #P #l1 #l2 elim l1
    869 [ #H @H
    870 | #h #t #IH #H %2 @IH @H
    871 ] qed.
    872808
    873809
     
    965901try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj
    966902try @I
    967 try @(trans_inv_stmt_inv ???? (sig_ok ? (λs.trans_inv ??? s) …))
    968 try @(sig_ok ? (λs.stmt_inv ?? s))
    969 try @(sig_ok ? (λe.expr_vars ? e ?))
    970 try @(sig_ok ? (λs.stmt_vars ?? s))
    971 try @(sig_ok ? (λs.stmt_labels ?? s))
    972 try @(sig_ok ? (All ??))
    973 try @(sig_ok ? (local_id vars))
     903try @(trans_inv_stmt_inv ???? (use_sig ? (λs.trans_inv ??? s) …))
     904try @(use_sig ? (λs.stmt_inv ?? s))
     905try @(use_sig ? (λe.expr_vars ? e ?))
     906try @(use_sig ? (λs.stmt_vars ?? s))
     907try @(use_sig ? (λs.stmt_labels ?? s))
     908try @(use_sig ? (All ??))
     909try @(use_sig ? (local_id vars))
    974910try @(lookup_label_hit … E)
    975911[ 1,3,5,6,7,13,14,15,16,18: whd #l *
    976 | @(sig_ok ?? s')
     912| @(use_sig ?? s')
    977913| @p
    978914| #l #H cases (Exists_append … H)
     
    1033969try @I
    1034970[ whd >E @I
    1035 | @(trans_inv_stmt_inv … s0) @(sig_ok … s)
     971| @(trans_inv_stmt_inv … s0) @(use_sig … s)
    1036972| cases s #s * #S #L @L
    1037973] qed.
     
    1047983false;false;false;false;
    1048984false;false;false;true]].
    1049 
    1050 lemma Exists_rm : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2).
    1051 #A #P #l1 #x #l2 elim l1
    1052 [ normalize #H %2 @H
    1053 | #h #t #IH normalize * [ #H %1 @H | #H %2 @IH @H ]
    1054 qed.
    1055 
    1056 lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2).
    1057 #A #P #l1 #x #l2 #H elim l1
    1058 [ %1 @H
    1059 | #h #t #IH %2 @IH
    1060 ] qed.
    1061 
    1062 lemma Exists_map : ∀A,B,P,Q,f,l.
    1063 Exists A P l →
    1064 (∀a.P a → Q (f a)) →
    1065 Exists B Q (map A B f l).
    1066 #A #B #P #Q #f #l elim l //
    1067 #h #t #IH * [ #H #F %1 @F @H | #H #F %2 @IH [ @H | @F ] ] qed.
    1068 
    1069 notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
    1070  with precedence 10
    1071 for @{ match $t return λx.x = $t → ? with [ pair ${ident x} ${ident y} ⇒
    1072         λ${ident E}.$s ] (refl ? $t) }.
    1073985
    1074986lemma local_id_add_local : ∀vars,id,id'.
     
    11281040  ]
    11291041] qed.
    1130 
    1131 notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40
    1132   for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ dp ${ident v} ${ident p} ⇒ ${e'} ]) }.
    11331042
    11341043definition build_label_env : ∀body:statement. res (Σlbls:lenv. ∀l,l'.lookup_label lbls l = OK ? l' → Exists ? (λl'.l' = l) (labels_defined body)) ≝
     
    11621071    #i #H cases (identifier_eq ? tmp i)
    11631072    [ #E <E @Exists_mid @refl
    1164     | #NE1 @Exists_rm cases (identifier_eq ? tmpp i)
     1073    | #NE1 @Exists_add cases (identifier_eq ? tmpp i)
    11651074      [ #E <E @Exists_mid @refl
    1166       | #NE2 @Exists_rm
     1075      | #NE2 @Exists_add
    11671076        >map_append
    11681077        @Exists_map [ 2: @(characterise_vars_all … (sym_eq ??? E) i)
Note: See TracChangeset for help on using the changeset viewer.