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

Sort out most of the fresh names stuff in Clight to Cminor.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/toCminor.ma

    r1627 r1629  
    33include "Clight/TypeComparison.ma".
    44include "basics/lists/list.ma".
     5include "Clight/fresh.ma".
    56
    67(* Identify local variables that must be allocated memory. *)
     
    137138qed.
    138139
     140lemma characterise_vars_src : ∀gl,f,vars,n.
     141  characterise_vars gl f = 〈vars,n〉 →
     142  ∀id. present ?? vars id →
     143   (∃r,ty. lookup' vars id = OK ? 〈Global r,ty〉 ∧ Exists ? (λx.x = 〈〈id,r〉,ty〉) gl) ∨
     144   ∃t.local_id vars id t.
     145#globals #f
     146whd in ⊢ (∀_.∀_.??%? → ?);
     147elim (fn_params f @ fn_vars f)
     148[ #vars #n whd in ⊢ (??%? → ?); #E destruct #i #H %1
     149  elim globals in H ⊢ %;
     150  [ normalize * #H cases (H (refl ??))
     151  | * * #id #rg #ty #tl #IH #H
     152    cases (identifier_eq ? i id)
     153    [ #E <E %{rg} %{ty} % [ whd in ⊢ (??%?); >lookup_add_hit // | %1 // ]
     154    | #NE cases (IH ?)
     155      [ #rg' * #ty' * #H1 #H2 %{rg'} %{ty'} %
     156        [ whd in ⊢ (??%?); >lookup_add_miss  [ @H1 | @NE ]
     157        | %2 @H2
     158        ]
     159      | whd in H ⊢ %; >lookup_add_miss in H; //
     160      ]
     161    ]
     162  ]
     163| * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?); #E #i
     164  #H >(contract_pair var_types nat ?) in E;
     165  whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
     166  cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?);
     167  #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
     168  cases (identifier_eq ? i id)
     169  [ 1,3: #E' <E' in EQ2:%; #EQ2 %2 %{(typ_of_type ty)}
     170         destruct (EQ2) whd whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]);
     171         >lookup_add_hit @refl
     172  | *: #NE cases (IH m0 n0 ? i ?)
     173    [ 1,5: * #rg' * #ty' * #H1 #H2 %1 %{rg'} %{ty'} % //
     174           destruct (EQ2) whd in ⊢ (??%?); >lookup_add_miss try @NE @H1
     175    | 2,6: * #t #H1 %2 %{t} destruct (EQ2) whd whd in ⊢ (match % with [_ ⇒ ?|_ ⇒ ?]);
     176           >lookup_add_miss //
     177    | 3,7: <EQ @refl
     178    | *: destruct (EQ2) whd in H; >lookup_add_miss in H; //
     179    ]
     180  ]
     181] qed.
     182
     183
    139184lemma characterise_vars_all : ∀l,f,vars,n.
    140185  characterise_vars l f = 〈vars,n〉 →
     
    168213    ]
    169214  ]
     215] qed.
     216
     217lemma characterise_vars_fresh : ∀gl,f,vars,n,u.
     218  characterise_vars gl f = 〈vars,n〉 →
     219  globals_fresh_for_univ ? gl u →
     220  fn_fresh_for_univ f u →
     221  fresh_map_for_univ … vars u.
     222#gl #f #vars #n #u #CH #GL #FN
     223#id #H
     224cases (characterise_vars_src … CH … H)
     225[ * #rg * #ty * #H1 #H2
     226  cases (Exists_All … H2 GL) * * #id' #rg' #ty' * #E #H destruct //
     227| * #t #H lapply (characterise_vars_all … CH id t H) #EX
     228  cases (Exists_All … EX FN) * #id' #ty' * * #E1 #E2 #H' -H destruct //
    170229] qed.
    171230
     
    10991158] qed.
    11001159
    1101 definition translate_function : universe SymbolTag → list (ident×region×type) → function → res internal_function ≝
    1102 λtmpuniverse, globals, f.
     1160definition translate_function :
     1161  ∀tmpuniverse:universe SymbolTag.
     1162  ∀globals:list (ident×region×type).
     1163  ∀f:function.
     1164    globals_fresh_for_univ ? globals tmpuniverse →
     1165    fn_fresh_for_univ f tmpuniverse →
     1166  res internal_function ≝
     1167λtmpuniverse, globals, f, Fglobals, Ffn.
    11031168  do «lbls, Ilbls» ← build_label_env (fn_body f);
    11041169  let 〈vartypes, stacksize〉 as E ≝ characterise_vars globals f in
     
    11131178    s ?).
    11141179[ //
    1115 | (* FIXME *) cases daemon
     1180| @(characterise_vars_fresh … (sym_eq … E)) //
    11161181| cases Is * #S #L #TP
    11171182  @(stmt_P_mp ???? S)
     
    11351200] qed.
    11361201
    1137 definition translate_fundef : universe SymbolTag → list (ident×region×type) → clight_fundef → res (fundef internal_function) ≝
    1138 λtmpuniverse,globals,f.
    1139 match f with
    1140 [ CL_Internal fn ⇒ do fn' ← translate_function tmpuniverse globals fn; OK ? (Internal ? fn')
    1141 | CL_External fn argtys retty ⇒ OK ? (External ? (mk_external_function fn (signature_of_type argtys retty)))
     1202definition translate_fundef :
     1203  ∀tmpuniverse:universe SymbolTag.
     1204  ∀globals:list (ident×region×type).
     1205  ∀f:clight_fundef.
     1206    globals_fresh_for_univ ? globals tmpuniverse →
     1207    fd_fresh_for_univ f tmpuniverse →
     1208  res (fundef internal_function) ≝
     1209λtmpuniverse,globals,f,Fglobals.
     1210match f return λf. fd_fresh_for_univ f ? → ? with
     1211[ CL_Internal fn ⇒ λFf. do fn' ← translate_function tmpuniverse globals fn Fglobals Ff; OK ? (Internal ? fn')
     1212| CL_External fn argtys retty ⇒ λ_. OK ? (External ? (mk_external_function fn (signature_of_type argtys retty)))
    11421213].
    11431214
     
    11451216   generation.  Cheating a bit - we only need the new identifiers to be fresh
    11461217   for individual functions. *)
    1147 include "Clight/fresh.ma".
    11481218
    11491219definition clight_to_cminor : clight_program → res Cminor_program ≝
Note: See TracChangeset for help on using the changeset viewer.