Changeset 1631 for src/Cminor


Ignore:
Timestamp:
Dec 19, 2011, 2:48:37 PM (8 years ago)
Author:
campbell
Message:

Use fact that type environments in Cminor have distinct variables to
remove last freshness related axiom in front-end.

Location:
src/Cminor
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/initialisation.ma

    r1626 r1631  
    8888                                           (f_params f)
    8989                                           (f_vars f)
     90                                           (f_distinct f)
    9091                                           (f_stacksize f)
    9192                                           (St_seq s (f_body f))
  • src/Cminor/syntax.ma

    r1626 r1631  
    144144; f_params    : list (ident × typ)
    145145; f_vars      : list (ident × typ)
     146; f_distinct  : distinct_env … (f_params @ f_vars)
    146147; f_stacksize : nat
    147148; f_body      : stmt
  • src/Cminor/toRTLabs.ma

    r1626 r1631  
    1313   let 〈r,gen'〉 ≝ fresh … gen in
    1414     〈〈r,ty〉::rs, add ?? en id 〈r,ty〉, gen'〉) 〈[ ], en, gen〉.
    15 (*
     15
     16definition Env_has : env → ident → typ → Prop ≝
     17λe,i,t. match lookup ?? e i with [ Some x ⇒ \snd x = t | None ⇒ False ].
     18
     19lemma Env_has_present : ∀e,i,t. Env_has e i t → present … e i.
     20#e #i #t whd in ⊢ (% → %); cases (lookup ?? e i)
     21[ * | * #r #t' #E % #E' destruct ]
     22qed.
     23
    1624lemma populates_env : ∀l,e,u,l',e',u'.
     25  distinct_env ?? l →
    1726  populate_env e u l = 〈l',e',u'〉 →
    18   ∀i. Exists ? (λx.\fst x = i) l →
    19       present ?? e' i.
     27  ∀i,t. Exists ? (λx.x = 〈i,t〉) l →
     28      Env_has e' i t.
    2029#l elim l
    21 [ #e #u #l' #e' #u' #E whd in E:(??%?); #i destruct (E) *
    22 | * #id #t #tl #IH #e #u #l' #e' #u' #E #i whd in E:(??%?) ⊢ (% → ?);
    23   * [ whd in ⊢ (??%? → ?); #E1 <E1
     30[ #e #u #l' #e' #u' #D #E whd in E:(??%?); #i #t destruct (E) *
     31| * #id #ty #tl #IH #e #u #l' #e' #u' #D #E #i #t whd in E:(??%?) ⊢ (% → ?);
     32  * [ #E1 destruct (E1)
    2433      generalize in E:(??(match % with [ _ ⇒ ? ])?) ⊢ ?; * * #x #y #z
    25       whd in ⊢ (??%? → ?); elim (fresh RegisterTag z) #r #gen' #E
    26       whd in E:(??%?); destruct;
    27       whd >lookup_add_hit % #A destruct
     34      whd in ⊢ (??%? → ?);
     35      lapply (refl ? (fresh ? z)) elim (fresh ? z) in ⊢ (??%? → %);
     36      #r #gen' #E1 #E2
     37      whd in E2:(??%?); destruct;
     38      whd >lookup_add_hit %
    2839    | #H change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ? ])?);
    2940      lapply (refl ? (populate_env e u tl))
    3041      cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); (* XXX if I do this directly it rewrites both sides of the equality *)
    31       * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?); cases (fresh RegisterTag u1) #r #u''
     42      * #rs #e1 #u1 #E1 >E1 in E; whd in ⊢ (??%? → ?);
     43      lapply (refl ? (fresh ? u1)) cases (fresh ? u1) in ⊢ (??%? → %); #r #u'' #E2
    3244      whd in ⊢ (??%? → ?); #E destruct
    33       @lookup_add_oblivious
    34       @(IH … E1 ? H)
     45      whd >lookup_add_miss
     46      [ @(IH … E1 ?? H) @(proj2 … D)
     47      | cases (Exists_All … H (proj1 … D)) #x * #E3 destruct #NE /2/
     48      ]
    3549    ]
    3650] qed.
    3751
     52lemma populates_env_distinct : ∀r,l,e,u,l',e',u'.
     53  distinct_env ?? (l@r) →
     54  populate_env e u l = 〈l',e',u'〉 →
     55  All ? (λit. fresh_for_map … (\fst it) e) r →
     56  All ? (λit. fresh_for_map … (\fst it) e') r.
     57#r #l elim l
     58[ #e #u #l' #e' #u' #D #E whd in E:(??%?); destruct (E) //
     59| * #id #ty #tl #IH #e #u #l' #e' #u' #D #E whd in E:(??%?) ⊢ (% → ?);
     60  change with (populate_env ???) in E:(??(match % with [ _ ⇒ ?])?);
     61  lapply (refl ? (populate_env e u tl)) cases (populate_env e u tl) in (*E*) ⊢ (???% → ?);
     62  * #x #y #z #E2 >E2 in E;
     63  whd in ⊢ (??%? → ?);
     64  elim (fresh ? z)
     65  #rg #gen' #E
     66  whd in E:(??%?); destruct
     67  #F lapply (IH … E2 F)
     68  [ @(proj2 … D)
     69  | lapply (All_append_r … (proj1 … D))
     70    elim r
     71    [ //
     72    | * #i #t #tl' #IH * #D1 #D2 * #H1 #H2 %
     73      [ @fresh_for_map_add /2/
     74      | @IH //
     75      ]
     76    ]
     77  ]
     78] qed.
     79
    3880lemma populate_extends : ∀l,e,u,l',e',u'.
     81  All ? (λit. fresh_for_map ?? (\fst it) e) l →
    3982  populate_env e u l = 〈l',e',u'〉 →
    40   ∀i. present ?? e i → present ?? e' i.
     83  ∀i,t. Env_has e i t → Env_has e' i t.
    4184#l elim l
    42 [ #e #u #l' #e' #u' #E whd in E:(??%?); destruct //
    43 | * #id #t #tl #IH #e #u #l' #e' #u' #E whd in E:(??%?);
     85[ #e #u #l' #e' #u' #F #E whd in E:(??%?); destruct //
     86| * #id #t #tl #IH #e #u #l' #e' #u' #F #E whd in E:(??%?);
    4487  change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ?])?);
    4588  lapply (refl ? (populate_env e u tl))
    4689  cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0
    47   >E0 in E; whd in ⊢ (??%? → ?); #E
     90  >E0 in E; whd in ⊢ (??%? → ?); cases (fresh ? u0) #fi #fu whd in ⊢ (??%? → ?); #E
    4891  destruct
    49   #i #H @lookup_add_oblivious @(IH … E0) @H
    50 ] qed.
    51 *)
     92  #i #t #H whd >lookup_add_miss
     93  [ @(IH … E0) [ @(proj2 … F) | @H ]
     94  | @(present_not_fresh ?? e) [ whd in H ⊢ %; % #E >E in H; * | @(proj1 … F) ]
     95] qed.
     96
     97definition lookup_reg : ∀e:env. ∀id,ty. Env_has e id ty → register ≝ λe,id,ty,H. \fst (lookup_present ?? e id ?).
     98/2/ qed.
     99
     100lemma populate_env_list : ∀l,e,u,l',e',u'.
     101  populate_env e u l = 〈l',e',u'〉 →
     102  ∀i,r,t. ∀H:Env_has e' i t. lookup_reg e' i t H = r →
     103    (∃H:Env_has e i t. lookup_reg e i t H = r) ∨ env_has l' r t.
     104#l elim l
     105[ #e #u #l' #e' #u' #E whd in E:(??%?); destruct #i #r #t #H #L %1 %{H} @L
     106| * #id #ty #tl #IH #e #u #l' #e' #u' #E
     107  whd in E:(??%?);
     108  change with (populate_env e u tl) in E:(??(match % with [ _ ⇒ ?])?);
     109  lapply (refl ? (populate_env e u tl))
     110  cases (populate_env e u tl) in (*E:%*) ⊢ (???% → ?); * #l0 #e0 #u0 #E0
     111  >E0 in E; whd in ⊢ (??%? → ?); cases (fresh ? u0) #fi #fu whd in ⊢ (??%? → ?); #E
     112  destruct
     113  #i #r #t cases (identifier_eq ? i id)
     114  [ #E1 >E1 #H whd in ⊢ (??%? → %); whd in match (lookup_present ?????);
     115    generalize in ⊢ (??(??? (?%))? → ?);
     116    whd in H ⊢ (% → ?); >lookup_add_hit in H ⊢ %; normalize #E2 #NE #E3 destruct
     117    %2 %1 %
     118  | #NE #H #L cases (IH … E0 i r t ??)
     119    [ /2/
     120    | #X %2 %2 @X
     121    | whd in H ⊢ %; >lookup_add_miss in H; //
     122    | whd in L:(??%?); whd in match (lookup_present ?????) in L;
     123      lapply L -L
     124      generalize in ⊢ (??(???(?%))? → ?); whd in ⊢ (% → ?);
     125      generalize in ⊢ (? → ? → ??(????%)?);
     126      >lookup_add_miss // #H0 #p
     127      change with (lookup_present SymbolTag (register×typ) e0 i ?) in ⊢ (??(???%)? → ?);
     128      whd in ⊢ (? → ??%?); generalize in ⊢ (? → ??(???(?????%))?);
     129      #p' #X @X
     130    ]
     131  ]
     132] qed.
     133
    52134definition  populate_label_env : label_env → universe LabelTag → list (identifier Label) → label_env × (universe LabelTag) ≝
    53135λen,gen. foldr ??
     
    67149  cases (populate_label_env lbls u t) in ⊢ (???% → %);
    68150  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?);
     151  cases (fresh LabelTag u1) #lf #uf whd in ⊢ (??%? → ?);
    69152  #E destruct
    70153  #l *
     
    84167  cases (populate_label_env lbls u t) in ⊢ (???% → %);
    85168  #lbls1 #u1 #E1 whd in ⊢ (??%? → ?);
     169  cases (fresh ? u1) #fi #fu whd in ⊢ (??%? → ?);
    86170  #E destruct
    87171  #l #H cases (identifier_eq ? l h)
     
    92176] qed.
    93177
    94 definition Env_has : env → ident → typ → Prop ≝
    95 λe,i,t. match lookup ?? e i with [ Some x ⇒ \snd x = t | None ⇒ False ].
    96 
    97 lemma Env_has_present : ∀e,i,t. Env_has e i t → present … e i.
    98 #e #i #t whd in ⊢ (% → %); cases (lookup ?? e i)
    99 [ * | * #r #t' #E % #E' destruct ]
    100 qed.
    101 
    102 definition lookup_reg : ∀e:env. ∀id,ty. Env_has e id ty → register ≝ λe,id,ty,H. \fst (lookup_present ?? e id ?).
    103 /2/ qed.
    104178definition lookup_label : ∀e:label_env. ∀id. present ?? e id → label ≝ lookup_present ??.
    105179
     
    754828] qed.
    755829
     830notation > "hvbox('let' ❬ident x,ident y❭ 'as' ident E ≝ t 'in' s)"
     831 with precedence 10
     832for @{ match $t return λx.x = $t → ? with [ mk_DPair ${ident x} ${ident y} ⇒
     833        λ${ident E}.$s ] (refl ? $t) }.
    756834
    757835definition c2ra_function (*: internal_function → internal_function*) ≝
     
    762840let 〈params, env1, reggen1〉 as E1 ≝ populate_env (empty_map …) reggen0 (f_params f) in
    763841let 〈locals0, env, reggen2〉 as E2 ≝ populate_env env1 reggen1 (f_vars f) in
    764 let ❬locals_reggen, result❭
     842let ❬locals_reggen, result❭ as E3
    765843  match f_return f return λ_.𝚺lr. option (Σrt. env_has ((\fst lr)@params) (\fst rt) (\snd rt)) with
    766844  [ None ⇒ ❬〈locals0, reggen2〉, None ?❭
     
    807885  [ @(stmt_vars_mp … V)
    808886    #i #t #H cases (Exists_append … H)
    809     cases daemon (* XXX needs populates_env
    810     [ #H1 @(populate_extends ?????? (sym_eq … E2))
    811           @(populates_env … (sym_eq … E1)) @H1
    812     | #H1 @(populates_env … (sym_eq … E2)) @H1
    813     ]*)
     887    [ #H1 @(populate_extends … (sym_eq … E2))
     888      [ @(populates_env_distinct … (sym_eq … E1)) //
     889        @All_alt //
     890      | @(populates_env … (sym_eq … E1)) [ @distinct_env_append_l // | @H1 ]
     891      ]
     892    | #H1 @(populates_env … (sym_eq … E2)) /2/ @H1
     893    ]
    814894  | @(stmt_labels_mp … L)
    815895    #l #H @(populates_label_env … (sym_eq … El)) @H
     
    826906  ]
    827907  ]
    828 | cases daemon (* XXX need information about env *)
     908| #id #ty #r #H #L cases (populate_env_list … (sym_eq … E2) … H L)
     909  [ * #H1 #L1 cases (populate_env_list … (sym_eq … E1) … H1 L1)
     910    [ * * | normalize @Exists_append_r ]
     911  | cases (f_return f) in E3;
     912    [ whd in ⊢ (??%% → ?); #E3 whd in match locals; destruct
     913      @Exists_append_l
     914    | #rt cases (fresh ? reggen2) #rr #ru whd in ⊢ (??%% → ?); #E3 whd in match locals; destruct
     915      #H' @Exists_append_l %2 @H'
     916    ]
     917  ]
    829918| #l1 #s #LOOKUP cases (lookup_add_cases ??????? LOOKUP)
    830919  [ * #E1 #E2 >E2 @I
Note: See TracChangeset for help on using the changeset viewer.