Ignore:
Timestamp:
Nov 8, 2012, 2:27:54 PM (7 years ago)
Author:
tranquil
Message:

changed joint's stack pointer and internal stack

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils.ma

    r2286 r2443  
    22include "joint/blocks.ma".
    33include "utilities/hide.ma".
     4include "utilities/deqsets.ma".
    45
    56(* general type of functions generating fresh things *)
     
    6465    add_graph … mid (final … (\snd b)) def
    6566  ].
     67
     68(* ignoring register allocation for now *)
     69
     70definition luniverse_ok : ∀p : graph_params.∀g.joint_internal_function p g → Prop ≝
     71λp,g,def.fresh_map_for_univ … (joint_if_code … def) (joint_if_luniverse … def).
     72
     73lemma present_to_memb : ∀tag,A,l,m.present tag A m l → bool_to_Prop (l∈m).
     74#tag #A * #l * #m whd in ⊢ (%→?%);
     75elim (lookup tag ???)
     76[ * #ABS elim (ABS ?) %
     77| #a #_ %
     78] qed.
     79
     80lemma memb_to_present : ∀tag,A,l,m.l∈m → present tag A m l.
     81#tag #A * #l * #m whd in ⊢ (?%→%);
     82elim (lookup tag ???)
     83[ * | #a * % #ABS destruct(ABS) ] qed.
     84
     85(*
     86lemma All_fresh_not_memb : ∀tag,u,l,id,u'.
     87  All (identifier tag) (λid'.¬fresh_for_univ tag id' u) l →
     88  〈id, u'〉 = fresh tag u →
     89  ¬id ∈ l.
     90#tag #u #l elim l [2: #hd #tl #IH] #id #u' *
     91[ #hd_fresh #tl_fresh #EQfresh
     92  whd in ⊢ (?(?%));
     93  change with (eq_identifier ???) in match (?==?);
     94  >eq_identifier_sym
     95  >(eq_identifier_false … (fresh_distinct … hd_fresh EQfresh))
     96  normalize nodelta @(IH … tl_fresh EQfresh)
     97| #_ %
     98]
     99qed.
     100*)
     101
     102lemma fresh_was_fresh : ∀tag,id,id',u,u'.
     103〈id,u'〉 = fresh tag u →
     104fresh_for_univ tag id' u' →
     105id' ≠ id →
     106fresh_for_univ tag id' u.
     107#tag * #id * #id' * #u * #u'
     108normalize #EQfresh destruct
     109#H #NEQ
     110elim (le_to_or_lt_eq … H)
     111[ (* not recompiling... /2 by monotonic_pred/ *) /2/ ]
     112#H >(succ_injective … H) in NEQ;
     113* #G elim (G (refl …))
     114qed.
     115
     116
     117(* use Russell? *)
     118axiom adds_graph_list_ok :
     119  ∀g_pars,globals,b,src,def.
     120  fresh_for_univ … src (joint_if_luniverse … def) →
     121  luniverse_ok ?? def →
     122  let 〈def', dst〉 ≝ adds_graph_list g_pars globals b src def in
     123  luniverse_ok ?? def' ∧
     124  ∃l.bool_to_Prop (uniqueb … l) ∧
     125     All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
     126                  fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
     127     src ~❨b,l❩~> dst in joint_if_code … def'.
     128(* #p #g #l elim l
     129[ #src #def #_ #Hdef whd
     130  %{Hdef} %{[ ]} %%%
     131| #hd #tl #IH #src #def #src_fresh #Hdef
     132  whd in match (adds_graph_list ?????);
     133  whd in match (fresh_label ???);
     134  @(pair_elim … (fresh ??)) normalize nodelta
     135  #mid #luniverse' #EQfresh
     136  whd in ⊢ (match % with [ _ ⇒ ?]);
     137  letin def' ≝ (add_graph p g src (sequential … hd mid) (set_luniverse … def luniverse'))
     138  cut (joint_if_code p g (set_luniverse p g def luniverse') = joint_if_code … def)
     139  [ cases def // ] #EQ_aux
     140  lapply (IH mid def' ??)
     141  [ #l whd in match def'; #Hpres
     142    lapply (present_to_memb … Hpres) -Hpres
     143    >mem_set_add @eq_identifier_elim
     144    [ #EQ destruct(EQ) *
     145    | #NEQ change with (? ∈ joint_if_code p ??) in ⊢ (?%→?); >EQ_aux
     146      #l_in
     147    ]
     148    @(fresh_remains_fresh … (sym_eq … EQfresh))
     149    [2: @Hdef @memb_to_present ] assumption
     150  | whd in match def';
     151    cases def #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
     152    whd in match (set_luniverse ????);
     153    @(fresh_is_fresh … (sym_eq … EQfresh))
     154  ]
     155  elim (adds_graph_list ?????) #def'' #mid' normalize nodelta
     156  * #Hdef'' * #l ** #Hl1 #Hl2 #Hl3 %{Hdef''} %{(mid::l)}
     157  % [ % ]
     158  [ whd in ⊢ (?%);
     159    elim (true_or_false_Prop (mid∈l)) #H >H normalize nodelta
     160    [ elim (All_memb … Hl2 H)
     161      cases def #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 normalize in ⊢ (%→?);
     162      #H #_ @(absurd ?? H)
     163      @(fresh_remains_fresh … (eqEQfresh)
     164      normalize #H10 #H11
     165     
     166    >(All_fresh_not_memb … (sym_eq … EQfresh))
     167    [ assumption ]
     168    @(All_mp … Hl2) #lbl *
     169    cases def in EQfresh; #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19
     170    normalize #EQfresh #H #lbl_not_mid
     171    lapply(fresh_remains_fresh … H (sym_eq … EQfresh))
     172   
     173    elim (true_or_false_Prop (mid∈l)) #mid_l >mid_l
     174    [ normalize
     175*)
    66176
    67177(* preserves first statement if a cost label (should be an invariant) *)
     
    132242  ].
    133243
     244 
     245
    134246(* translation with inline fresh register allocation *)
    135247definition b_graph_translate :
Note: See TracChangeset for help on using the changeset viewer.