Changeset 1631


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
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r1630 r1631  
    11701170  let tmp ≝ mk_tmpgen vartypes tmpuniverse [ ] ?? in
    11711171  do s ← translate_statement vartypes lbls tmp (fn_body f);
    1172    do «s,tmp, Is» ← alloc_params vartypes lbls ?? (fn_params f) s;
     1172  do «s,tmp, Is» ← alloc_params vartypes lbls ?? (fn_params f) s;
     1173  let params ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f) in
     1174  let vars ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (tmp_env ? tmp @ fn_vars f) in
     1175  do D ← check_distinct_env ?? (params @ vars);
    11731176  OK ? (mk_internal_function
    11741177    (opttyp_of_type (fn_return f))
    1175     (map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f))
    1176     ((map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (tmp_env ? tmp @ fn_vars f)))
     1178    params
     1179    vars
     1180    D
    11771181    stacksize
    11781182    s ?).
     
    11901194                  | * #id #ty * #E1 #E2 <E1 <E2 @refl
    11911195                  ]
    1192     | #EX @Exists_append_r <map_append @Exists_append_l @Exists_map [2: @EX | skip | * #id #ty * #E1 #E2 <E1 <E2 % @refl ]
     1196    | #EX @Exists_append_r whd in ⊢ (???%); <map_append @Exists_append_l @Exists_map [2: @EX | skip | * #id #ty * #E1 #E2 <E1 <E2 % @refl ]
    11931197    ]
    11941198  | @(stmt_labels_mp … H2)
  • 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
  • src/common/Identifiers.ma

    r1627 r1631  
    22include "ASM/String.ma".
    33include "utilities/binary/positive.ma".
     4include "utilities/lists.ma".
    45include "common/Errors.ma".
    56
     
    6061#H #E whd % [ @(fresh_is_fresh … E) | @(All_mp … H) * #id #a #H' /2/ ]
    6162qed.
    62 
    6363
    6464definition eq_identifier : ∀t. identifier t → identifier t → bool ≝
     
    110110definition identifier_of_nat : ∀tag:String. nat → identifier tag ≝
    111111  λtag,n. an_identifier tag (succ_pos_of_nat  n).
     112
     113
     114(* States that all identifiers in an environment are distinct from one another. *)
     115let rec distinct_env tag (A:Type[0]) (l:list (identifier tag × A)) on l : Prop ≝
     116match l with
     117[ nil ⇒ True
     118| cons hd tl ⇒ All ? (λia. \fst hd ≠ \fst ia) tl ∧
     119               distinct_env tag A tl
     120].
     121
     122lemma distinct_env_append_l : ∀tag,A,l,r. distinct_env tag A (l@r) → distinct_env tag A l.
     123#tag #A #l elim l
     124[ //
     125| * #id #a #tl #IH #r * #H1 #H2 % /2/
     126] qed.
     127
     128lemma distinct_env_append_r : ∀tag,A,l,r. distinct_env tag A (l@r) → distinct_env tag A r.
     129#tag #A #l elim l
     130[ //
     131| * #id #a #tl #IH #r * #H1 #H2 /2/
     132] qed.
     133
     134(* check_distinct_env is quadratic - we could pay more attention when building maps to make sure that
     135   the original environment was distinct. *)
     136
     137axiom DuplicateVariable : String.
     138
     139let rec check_member_env tag (A:Type[0]) (id:identifier tag) (l:list (identifier tag × A)) on l : res (All ? (λia. id ≠ \fst ia) l) ≝
     140match l return λl.res (All ?? l) with
     141[ nil ⇒ OK ? I
     142| cons hd tl ⇒
     143    match identifier_eq tag id (\fst hd) with
     144    [ inl _ ⇒ Error ? [MSG DuplicateVariable; CTX ? id]
     145    | inr NE ⇒
     146        do Htl ← check_member_env tag A id tl;
     147        OK ? (conj ?? NE Htl)
     148    ]
     149].
     150
     151let rec check_distinct_env tag (A:Type[0]) (l:list (identifier tag × A)) on l : res (distinct_env tag A l) ≝
     152match l return λl.res (distinct_env tag A l) with
     153[ nil ⇒ OK ? I
     154| cons hd tl ⇒
     155    do Hhd ← check_member_env tag A (\fst hd) tl;
     156    do Htl ← check_distinct_env tag A tl;
     157    OK ? (conj ?? Hhd Htl)
     158].
     159
     160
    112161
    113162
     
    263312  lookup … m id = None A.
    264313
     314lemma fresh_for_empty_map : ∀tag,A,id.
     315  fresh_for_map tag A id (empty_map tag A).
     316#tag #A * #id //
     317qed.
     318
    265319definition fresh_map_for_univ ≝
    266320λtag,A. λm:identifier_map tag A. λu:universe tag.
     
    305359qed.
    306360
     361lemma fresh_for_map_add : ∀tag,A,id,m,id',a.
     362  id ≠ id' →
     363  fresh_for_map tag A id m →
     364  fresh_for_map tag A id (add tag A m id' a).
     365#tag #A * #id #m #id' #a #NE #F
     366whd >lookup_add_miss //
     367qed.
     368
     369
    307370(* Sets *)
    308371
     
    343406lemma union_empty_r : ∀tag.∀s:identifier_set tag. s ∪ ∅ = s.
    344407#tag * * // qed.
     408
  • src/utilities/lists.ma

    r1630 r1631  
    55[ //
    66| #hd #tl #IH #r * #H1 #H2 #H3 % // @IH //
    7 ] qed.
     7] qed.
     8
     9lemma All_append_l : ∀A,P,l,r. All A P (l@r) → All A P l.
     10#A #P #l elim l
     11[ //
     12| #hd #tl #IH #r * #H1 #H2 % /2/
     13] qed.
     14
     15lemma All_append_r : ∀A,P,l,r. All A P (l@r) → All A P r.
     16#A #P #l elim l
     17[ //
     18| #h #t #IH #r * /2/
     19] qed.
    820
    921(* An alternative form of All that can be easier to use sometimes. *)
Note: See TracChangeset for help on using the changeset viewer.