Changeset 1102


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

Tidy up branch

Location:
Deliverables/D3.3/id-lookup-branch
Files:
7 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)
  • Deliverables/D3.3/id-lookup-branch/Cminor/initialisation.ma

    r1101 r1102  
    44include "Cminor/syntax.ma".
    55include "common/Globalenvs.ma".
     6include "utilities/pair.ma".
     7include "utilities/deppair.ma".
    68
    79(* XXX having to specify the return type in the match is annoying. *)
     
    3941qed.
    4042
    41 lemma unpair : ∀A,B,C,D,x. ∀P:A → B → C. ∀Q:A → B → D.
    42   let 〈a,b〉 ≝ x in 〈P a b, Q a b〉 = 〈P (\fst x) (\snd x), Q (\fst x) (\snd x)〉.
    43 #A #B #C #D * // qed.
    44 
    45 lemma sndredex : ∀A,B,C,D,x. ∀R:D → Prop. ∀P:A → C. ∀Q:A → B → D.
    46   R (Q (\fst x) (\snd x)) → R (\snd (let 〈a,b〉 ≝ x in 〈P a, Q a b〉)).
    47 #A #B #C #D *; normalize /2/
    48 qed.
    49 
    50 lemma sig_stmt_inv : ∀s:Σs:stmt.stmt_inv s.
    51   stmt_inv s.
    52 * #s #p @p
    53 qed.
    54 
    5543definition init_var : ident → region → list init_data → Σs:stmt. stmt_inv s ≝
    5644λid,r,init.
     
    6351| elim init
    6452  [ % //
    65   | #h #t #IH whd in ⊢ (?(???%)) @sndredex % [ % [ % // | @sig_stmt_inv ] | @IH ]
     53  | #h #t #IH whd in ⊢ (?(???%)) @breakup_pair whd in ⊢ (?%) % [ % [ % // | @(use_sig ? stmt_inv) ] | @IH ]
    6654] qed.
    6755
     
    6957λvars. foldr ? (Σs:stmt. stmt_inv s)
    7058  (λvar,s. dp ? (λx.stmt_inv x ) (St_seq s (init_var (\fst (\fst (\fst var))) (\snd (\fst var)) (\snd (\fst (\fst var))))) ?) (dp ? (λx.stmt_inv x ) St_skip (conj ?? I I)) vars.
    71 % [ % [ % // | @sig_stmt_inv ] | @sig_stmt_inv ]
     59% [ % [ % // | @(use_sig ? stmt_inv) ] | @(use_sig ? stmt_inv) ]
    7260qed.
    7361
  • Deliverables/D3.3/id-lookup-branch/Cminor/semantics.ma

    r961 r1102  
    106106].
    107107
    108 let rec find_label (l:ident) (s:stmt) (k:cont) on s : option (stmt × cont) ≝
     108let rec find_label (l:identifier Label) (s:stmt) (k:cont) on s : option (stmt × cont) ≝
    109109match s with
    110110[ St_seq s1 s2 ⇒
     
    121121| St_block s' ⇒ find_label l s' (Kblock k)
    122122| St_label l' s' ⇒
    123     match ident_eq l l' with
     123    match identifier_eq ? l l' with
    124124    [ inl _ ⇒ Some ? 〈s',k〉
    125125    | inr _ ⇒ find_label l s' k
  • Deliverables/D3.3/id-lookup-branch/Cminor/toRTLabs.ma

    r1101 r1102  
    33include "Cminor/syntax.ma".
    44include "RTLabs/syntax.ma".
     5include "utilities/pair.ma".
     6include "utilities/deppair.ma".
    57
    68definition env ≝ identifier_map SymbolTag register.
     
    7779] qed.
    7880
    79 lemma lookup_sigma : ∀tag,A,m. ∀i:(Σl:identifier tag. lookup tag A m l ≠ None ?).
    80   lookup tag A m i ≠ None ?.
    81 #tag #A #m * #i #H @H
    82 qed.
    83 
    8481definition lookup' : ∀e:env. ∀id. present ?? e id → register ≝
    8582λe,id. match lookup ?? e id return λx. x ≠ None ? → ? with [ Some r ⇒ λ_. r | None ⇒ λH.⊥ ].
     
    9895                       (f_stacksize f) (add ?? (f_graph f) l s)
    9996                       (dp ?? (f_entry f) ?) (dp ?? (f_exit f) ?).
    100 @lookup_add_oblivious @lookup_sigma
     97@lookup_add_oblivious @use_sig
    10198qed.
    10299
     
    109106                       (dp ?? l ?) (dp ?? (f_exit f) ?).
    110107[ >lookup_add_hit % #E destruct
    111 | @lookup_add_oblivious @lookup_sigma
     108| @lookup_add_oblivious @use_sig
    112109] qed.
    113110
     
    123120                       (dp ?? l ?) (dp ?? (f_exit f) ?)).
    124121[ >lookup_add_hit % #E destruct
    125 | @lookup_add_oblivious @lookup_sigma
     122| @lookup_add_oblivious @use_sig
    126123] qed.
    127124
     
    235232axiom ReturnMismatch : String.
    236233
    237 notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
    238  with precedence 10
    239 for @{ match $t return λx.x = $t → ? with [ pair ${ident x} ${ident y} ⇒
    240         λ${ident E}.$s ] (refl ? $t) }.
    241 
    242234definition stmt_inv : env → label_env → stmt → Prop ≝
    243235λenv,lenv. stmt_P (λs. stmt_vars (present ?? env) s ∧ stmt_labels (present ?? lenv) s).
    244 
    245 notation "π1" with precedence 10 for @{ (proj1 ??) }.
    246 notation "π2" with precedence 10 for @{ (proj2 ??) }.
    247236
    248237let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (exits:list label) (f:internal_function) on s : res internal_function ≝
     
    358347] qed.
    359348
    360 notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
    361  with precedence 10
    362 for @{ match $t return λx.x = $t → ? with [ pair ${fresh xy} ${ident z} ⇒
    363        match ${fresh xy} return λx. ? = $t → ? with [ pair ${ident x} ${ident y} ⇒
    364         λ${ident E}.$s ] ] (refl ? $t) }.
    365 
    366349
    367350definition c2ra_function (*: internal_function → internal_function*) ≝
  • Deliverables/D3.3/id-lookup-branch/common/Errors.ma

    r797 r1102  
    1818include "basics/list.ma".
    1919include "common/PreIdentifiers.ma".
     20include "utilities/lists.ma".
     21include "utilities/deppair.ma".
    2022
    2123(* * Error reporting and the error monad. *)
     
    8789notation "'ret' e" non associative with precedence 45 for @{'ret ${e}}.*)
    8890
     91(* Dependent pair version. *)
     92notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40
     93  for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ dp ${ident v} ${ident p} ⇒ ${e'} ]) }.
     94
    8995(*
    9096(** The [do] notation, inspired by Haskell's, keeps the code readable. *)
     
    127133  | cons hd tl ⇒ do hd' ← f hd; do tl' ← mmap ?? f tl; OK ? (hd'::tl')
    128134  ].
     135
     136(* And mmap coupled with proofs. *)
     137
     138let 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') ≝
     139match l with
     140[ nil ⇒ OK ? «nil B, ?»
     141| cons h t ⇒
     142    do h' ← f h;
     143    do t' ← mmap_sigma A B P f t;
     144    OK ? «cons B h' t', ?»
     145].
     146whd // %
     147[ @(use_sig B P)
     148| cases t' #l' #p @p
     149] qed.
    129150
    130151(*
     
    214235#A #m #P #e elim e; /2/;
    215236qed.
     237
     238(* A variation of bind and its notation that provides an equality proof for
     239   later use. *)
     240
     241definition bind_eq ≝ λA,B:Type[0]. λf: res A. λg: ∀a:A. f = OK ? a → res B.
     242  match f return λx. f = x → ? with
     243  [ OK x ⇒ g x
     244  | Error msg ⇒ λ_. Error ? msg
     245  ] (refl ? f).
     246
     247notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
     248
  • Deliverables/D3.3/id-lookup-branch/utilities/extralib.ma

    r891 r1102  
    1616include "basics/list.ma".
    1717include "basics/logic.ma".
     18include "utilities/pair.ma".
    1819include "utilities/binary/Z.ma".
    1920include "utilities/binary/positive.ma".
     
    516517lemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m.
    517518/2/; qed.
    518 
    519 lemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2.
    520 #A #B #a1 #a2 #b1 #b2 #H destruct //
    521 qed.
    522 
    523 lemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2.
    524 #A #B #a1 #a2 #b1 #b2 #H destruct //
    525 qed.
    526519
    527520theorem divide_ok : ∀m,n,dv,md.
  • Deliverables/D3.3/id-lookup-branch/utilities/lists.ma

    r1087 r1102  
    4040] qed.
    4141
     42lemma Exists_append_l : ∀A,P,l1,l2.
     43  Exists A P l1 → Exists A P (l1@l2).
     44#A #P #l1 #l2 elim l1
     45[ *
     46| #h #t #IH *
     47  [ #H %1 @H
     48  | #H %2 @IH @H
     49  ]
     50] qed.
     51
     52lemma Exists_append_r : ∀A,P,l1,l2.
     53  Exists A P l2 → Exists A P (l1@l2).
     54#A #P #l1 #l2 elim l1
     55[ #H @H
     56| #h #t #IH #H %2 @IH @H
     57] qed.
     58
     59lemma Exists_add : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2).
     60#A #P #l1 #x #l2 elim l1
     61[ normalize #H %2 @H
     62| #h #t #IH normalize * [ #H %1 @H | #H %2 @IH @H ]
     63qed.
     64
     65lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2).
     66#A #P #l1 #x #l2 #H elim l1
     67[ %1 @H
     68| #h #t #IH %2 @IH
     69] qed.
     70
     71lemma Exists_map : ∀A,B,P,Q,f,l.
     72Exists A P l →
     73(∀a.P a → Q (f a)) →
     74Exists B Q (map A B f l).
     75#A #B #P #Q #f #l elim l //
     76#h #t #IH * [ #H #F %1 @F @H | #H #F %2 @IH [ @H | @F ] ] qed.
     77
    4278lemma map_append : ∀A,B,f,l1,l2.
    4379  (map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
Note: See TracChangeset for help on using the changeset viewer.