Ignore:
Timestamp:
Oct 11, 2011, 12:24:33 PM (8 years ago)
Author:
campbell
Message:

Tidy up some loose ends from the invariants branch merge.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r1316 r1351  
    137137qed.
    138138
    139 include "utilities/extralib.ma". (* for pair_eq1 to work around destruct's excessive normalisation *)
    140 
    141139lemma characterise_vars_all : ∀l,f,vars,n.
    142140  characterise_vars l f = 〈vars,n〉 →
     
    146144whd in ⊢ (∀_.∀_.??%? → ?)
    147145elim (fn_params f @ fn_vars f)
    148 [ #vars #n whd in ⊢ (??%? → ?) #E <(pair_eq1 ?????? E) -E; #i #H @False_ind
     146[ #vars #n whd in ⊢ (??%? → ?) #E destruct #i #H @False_ind
    149147  elim globals in H
    150148  [ normalize //
     
    160158    @(IH m0 n0)
    161159    [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])) >contract_pair @EQ
    162     | 2,4: <(pair_eq1 ?????? EQ2) in H #H' @(local_id_add_miss … H') @NE
     160    | 2,4: destruct (EQ2) @(local_id_add_miss … H) @NE
    163161    ]
    164162  ]
     
    724722generalize in ⊢ (???(match % with [ _ ⇒ ? ]) → ?)
    725723* #tmp' #u whd in ⊢ (???% → ?) #E
    726 >(pair_eq2 ?????? E)
     724destruct
    727725#id #H
    728726whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]
     
    780778generalize in ⊢ (???(match % with [ _ ⇒ ? ]) → ?)
    781779* #tmp' #u' whd in ⊢ (???% → ?) #E
    782 >(pair_eq1 ?????? E) >(pair_eq2 ?????? E)
     780destruct
    783781whd in ⊢ (?%?) whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ] >lookup_add_hit
    784782@I
    785783qed.
    786 
    787 lemma use_sig' : ∀A.∀P,P':A → Prop. (∀x.P x → P' x) → ∀x:Σx:A.P x. P' x.
    788 #A #P #P' #H1 * #x #H2 @H1 @H2
    789 qed.
    790 
    791 definition sigbind2 : ∀A,B,C:Type[0]. ∀P:A×B → Prop. res (Σx:A×B.P x) → (∀a,b. P 〈a,b〉 → res C) → res C ≝
    792 λA,B,C,P,e,f.
    793   match e with
    794   [ OK v ⇒ match v with [ dp v' p ⇒ match v' return λv'. P v' → res C with [ pair a b ⇒ f a b ] p ]
    795   | Error msg ⇒ Error ? msg
    796   ].
    797 
    798 notation > "vbox('do' 〈ident v1, ident v2〉 'with' ident H ← e; break e')" with precedence 40 for @{'sigbind2 ${e} (λ${ident v1}.λ${ident v2}.λ${ident H}.${e'})}.
    799 (*
    800 notation > "vbox('do' 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
    801 notation < "vbox('do' \nbsp 〈ident v1, ident v2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
    802 notation < "vbox('do' \nbsp 〈ident v1 : ty1, ident v2 : ty2〉 ← e; break e')" with precedence 40 for @{'bind2 ${e} (λ${ident v1} : ${ty1}.λ${ident v2} : ${ty2}.${e'})}.
    803 *)
    804 interpretation "error monad sig Prod bind" 'sigbind2 e f = (sigbind2 ???? e f).
    805784
    806785let rec translate_statement (vars:var_types) (lbls:lenv) (u:tmpgen) (s:statement) on s : res (Σsu:stmt×tmpgen.trans_inv vars lbls s u su) ≝
     
    826805    ]
    827806| Ssequence s1 s2 ⇒
    828     do 〈s1', u1〉 with H1 ← translate_statement vars lbls u s1;
    829     do 〈s2', u2〉 with H2 ← translate_statement vars lbls u1 s2;
     807     do «s1', u1, H1» ← translate_statement vars lbls u s1;
     808     do «s2', u2, H2» ← translate_statement vars lbls u1 s2;
    830809    OK ? «〈St_seq s1' s2', u2〉, ?»
    831810| Sifthenelse e1 s1 s2 ⇒
     
    833812    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
    834813    [ ASTint _ _ ⇒ λe1'.
    835         do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1;
    836         do 〈s2', u〉 with H2 ← translate_statement vars lbls u s2;
     814         do «s1', u, H1» ← translate_statement vars lbls u s1;
     815         do «s2', u, H2» ← translate_statement vars lbls u s2;
    837816        OK ? «〈St_ifthenelse ?? e1' s1' s2', u〉, ?»
    838817    | _ ⇒ λ_.Error ? (msg TypeMismatch)
     
    842821    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
    843822    [ ASTint _ _ ⇒ λe1'.
    844         do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1;
     823         do «s1', u, H1» ← translate_statement vars lbls u s1;
    845824        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    846825        OK ? «〈St_block
     
    853832    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
    854833    [ ASTint _ _ ⇒ λe1'.
    855         do 〈s1',u〉 with H1 ← translate_statement vars lbls u s1;
     834         do «s1',u, H1» ← translate_statement vars lbls u s1;
    856835        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    857836        OK ? «〈St_block
     
    864843    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
    865844    [ ASTint _ _ ⇒ λe1'.
    866         do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1;
    867         do 〈s2', u〉 with H2 ← translate_statement vars lbls u s2;
    868         do 〈s3', u〉 with H3 ← translate_statement vars lbls u s3;
     845         do «s1', u, H1» ← translate_statement vars lbls u s1;
     846         do «s2', u, H2» ← translate_statement vars lbls u s2;
     847         do «s3', u, H3» ← translate_statement vars lbls u s3;
    869848        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
    870849        OK ? «〈St_seq s1'
     
    886865| Slabel l s1 ⇒
    887866    do l' as E ← lookup_label lbls l;
    888     do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1;
     867     do «s1', u, H1» ← translate_statement vars lbls u s1;
    889868    OK ? «〈St_label l' s1', u〉, ?»
    890869| Sgoto l ⇒
     
    892871    OK ? «〈St_goto l', u〉, ?»
    893872| Scost l s1 ⇒
    894     do 〈s1', u〉 with H1 ← translate_statement vars lbls u s1;
     873     do «s1', u, H1» ← translate_statement vars lbls u s1;
    895874    OK ? «〈St_cost l s1', u〉, ?»
    896875].
     
    954933λvars,ls,s0,u,params,s. foldl ?? (λsu,it.
    955934  let 〈id,ty〉 ≝ it in
    956   do 〈s,u〉 with Is ← su;
     935   do «s,u, Is» ← su;
    957936  do t as E ← lookup' vars id;
    958937  match t return λx.? → ? with
     
    10741053  let tmp ≝ mk_tmpgen tmpuniverse [ ] in
    10751054  do s ← translate_statement vartypes lbls tmp (fn_body f);
    1076   do 〈s,tmp〉 with Is ← alloc_params vartypes lbls ?? (fn_params f) s;
     1055   do «s,tmp, Is» ← alloc_params vartypes lbls ?? (fn_params f) s;
    10771056  OK ? (mk_internal_function
    10781057    (opttyp_of_type (fn_return f))
Note: See TracChangeset for help on using the changeset viewer.