Changeset 2595 for src/joint/blocks.ma


Ignore:
Timestamp:
Jan 30, 2013, 7:25:39 PM (9 years ago)
Author:
tranquil
Message:
  • dropped locals and exit from definition of joint_if_function
  • new definition of blocks to accomodate ERTLptr pass
  • stated properties of translation as axioms
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/blocks.ma

    r2422 r2595  
    4242  (list (block_step p globals)) × A.*)
    4343
    44 definition seq_block ≝ λp : stmt_params.λglobals,A.
    45   (list (joint_seq p globals)) × A.
     44(* move *)
     45let rec bind_new_P R X (P : X → Prop) (b : bind_new R X) on b : Prop ≝
     46match b with
     47[ bret x ⇒ P x
     48| bnew f ⇒ ∀x.bind_new_P … P (f x)
     49].
     50
     51definition BindNewP : ∀R.MonadPred (BindNew R) ≝
     52λR.mk_MonadPred (BindNew R) (bind_new_P R) ???.
     53[ #X #P #x #K @K
     54| #X #Y #Pin #Pout #m elim m -m
     55  [ #x #H #f #G @G @H
     56  | #g #IH #H #f #G #x @IH [ @H | @G ]
     57  ]
     58| #X #P #Q #H #m elim m -m
     59  [ #x #Px @H @Px
     60  | #g #IH #Pg #x @IH @Pg
     61  ]
     62]
     63qed.
     64
     65definition not_empty : ∀X.list X → Prop ≝ λX,l.match l with [ nil ⇒ False | _ ⇒ True ].
     66
     67definition head_ne : ∀X.(Σl.not_empty X l) → X ≝
     68λX,l.
     69match l return λl.not_empty ? l → ? with
     70[ nil ⇒ Ⓧ
     71| cons hd _ ⇒ λ_.hd
     72] (pi2 … l).
     73
     74
     75let rec split_on_last_ne_aux X l on l : not_empty X l → (list X) × X ≝
     76match l return λx.not_empty ? x → ? with
     77[ nil ⇒ Ⓧ
     78| cons hd tl ⇒ λ_.
     79  match tl return λtl.(not_empty X tl → ?) → ? with
     80  [ nil ⇒ λ_.〈[ ], hd〉
     81  | cons hd' tl' ⇒ λrec_call.let 〈pre, last〉 ≝ rec_call I in 〈hd :: pre, last〉
     82  ] (split_on_last_ne_aux ? tl)
     83].
     84
     85definition split_on_last_ne : ∀X.(Σl.not_empty X l) → (list X)×X ≝
     86λX,l.split_on_last_ne_aux … (pi2 … l).
     87
     88definition last_ne : ∀X.(Σl.not_empty X l) → X ≝ λX,l.\snd (split_on_last_ne … l).
     89definition chop_last_ne : ∀X.(Σl.not_empty X l) → list X ≝ λX,l.\fst (split_on_last_ne … l).
     90
     91lemma split_on_last_ne_def : ∀X,pre,last,prf.split_on_last_ne X «pre@[last], prf» = 〈pre, last〉.
     92whd in match split_on_last_ne; normalize nodelta
     93#X #pre elim pre -pre [ #last #prf % ]
     94#hd * [2: #hd' #tl'] #IH #last *
     95[ whd in ⊢ (??%?); >IH % | % ]
     96qed.
     97
     98lemma split_on_last_ne_inv : ∀X,l.
     99pi1 ?? l = (let 〈pre, last〉 ≝ split_on_last_ne X l in pre @ [last]).
     100whd in match split_on_last_ne; normalize nodelta
     101#X * #l elim l -l [ * ]
     102#hd * [2: #hd' #tl'] #IH * [2: % ]
     103whd in match (split_on_last_ne_aux ???);
     104lapply (IH I) @pair_elim #pre #last #_ #EQ >EQ %
     105qed.
     106
     107(* the label input is to accomodate ERTptr pass *)
     108definition step_block ≝ λp,globals.Σl : list (code_point p → joint_step p globals).not_empty ? l.
     109unification hint 0 ≔ p : params, g;
     110S ≟ code_point p → joint_step p g,
     111L ≟ list S,
     112P ≟ not_empty S
     113(*---------------------------------------*)⊢
     114step_block p g ≡ Sig L P.
     115
     116definition fin_block ≝ λp,globals.(list (joint_step p globals))×(joint_fin_step p).
    46117
    47118(*definition seq_to_skip_block :
     
    53124  seq_to_skip_block on _b : seq_block ??? to skip_block ???.*)
    54125
    55 definition bind_seq_block ≝ λp : stmt_params.λglobals,A.
    56   bind_new (localsT p) (seq_block p globals A).
    57 unification hint 0 ≔ p : stmt_params, g, X;
    58 R ≟ localsT p,
    59 P ≟ seq_block p g X
     126definition bind_step_block ≝ λp.λglobals.
     127  bind_new register (step_block p globals).
     128
     129unification hint 0 ≔ p, g;
     130P ≟ step_block p g
    60131(*---------------------------------------*)⊢
    61 bind_seq_block p g X ≡ bind_new R P.
    62 
    63 definition bind_seq_list ≝ λp : stmt_params.λglobals.
    64   bind_new (localsT p) (list (joint_seq p globals)).
     132bind_step_block p g ≡ bind_new register P.
     133
     134definition bind_fin_block ≝ λp : stmt_params.λglobals.
     135  bind_new register (fin_block p globals).
     136
    65137unification hint 0 ≔ p : stmt_params, g;
    66 R ≟ localsT p,
    67 S ≟ joint_seq p g,
     138P ≟ fin_block p g
     139(*---------------------------------------*)⊢
     140bind_fin_block p g ≡ bind_new register P.
     141
     142definition bind_step_list ≝ λp : stmt_params.λglobals.
     143  bind_new register (list (joint_step p globals)).
     144unification hint 0 ≔ p : stmt_params, g;
     145S ≟ joint_step p g,
    68146L ≟ list S
    69147(*---------------------------------------*)⊢
    70 bind_seq_list p g ≡ bind_new R L.
     148bind_step_list p g ≡ bind_new register L.
     149
     150definition add_dummy_variance : ∀X,Y : Type[0].list Y → list (X → Y) ≝ λX,Y.map … (λx.λ_.x).
     151
     152definition ensure_step_block : ∀p : params.∀globals.
     153list (joint_step p globals) → step_block p globals ≝
     154λp,g,l.match add_dummy_variance … l return λ_.Σl.not_empty ? l with
     155[ nil ⇒ «[λ_.NOOP ??], I»
     156| cons hd tl ⇒ «hd :: tl, I»
     157].
     158
     159definition ensure_step_list : ∀p,globals.
     160list (joint_seq p globals) → list (joint_step p globals) ≝
     161λp,g.map … (step_seq …).
     162
     163definition ensure_step_block_from_seq : ∀p : params.∀globals.
     164list (joint_seq p globals) → step_block p globals ≝
     165λp,g.ensure_step_block ?? ∘ ensure_step_list ??.
     166
     167coercion step_block_from_list nocomposites : ∀p : params.∀g.∀l : list (joint_step p g).step_block p g ≝
     168ensure_step_block on _l : list (joint_step ??) to step_block ??.
     169
     170coercion step_list_from_seq nocomposites : ∀p,g.∀l : list (joint_seq p g).list (joint_step p g) ≝
     171ensure_step_list on _l : list (joint_seq ??) to list (joint_step ??).
     172
     173coercion step_block_from_seq nocomposites : ∀p : params.∀g.∀l : list (joint_seq p g).step_block p g ≝
     174ensure_step_block_from_seq on _l : list (joint_seq ??) to step_block ??.
     175
    71176
    72177(*definition bind_skip_block ≝ λp : stmt_params.λglobals,A.
     
    90195  seq_or_fin_step_classifier ?? (\snd b).
    91196*)
    92 
    93 let rec split_on_last A (dflt : A) (l : list A) on l : (list A) × A ≝
    94 match l with
    95 [ nil ⇒ 〈[ ], dflt〉
    96 | cons hd tl ⇒
    97   match tl with
    98   [ nil ⇒ 〈[ ], hd〉
    99   | _ ⇒
    100     let 〈pref, post〉 ≝ split_on_last A dflt tl in
    101     〈hd :: pref, post〉
    102   ]
    103 ].
    104 
    105 lemma split_on_last_ok :
    106   ∀A,dflt,l.
    107   match l with
    108   [ nil ⇒ True
    109   | _ ⇒ l = (let 〈pre, post〉 ≝ split_on_last A dflt l in pre @ [post])
    110   ].
    111 #A #dflt #l elim l normalize nodelta
    112 [ %
    113 | #hd * [ #_ %]
    114   #hd' #tl #IH whd in match (split_on_last ???); >IH in ⊢ (??%?);
    115   elim (split_on_last ???) #a #b %
    116 ]
    117 qed.
    118 
    119 definition seq_block_from_seq_list :
     197(*definition seq_block_from_seq_list :
    120198∀p : stmt_params.∀g.list (joint_seq p g) → seq_block p g (joint_step p g) ≝
    121199λp,g,l.let 〈pre,post〉 ≝ split_on_last … (NOOP ??) l in 〈pre, (post : joint_step ??)〉.
     
    176254  ∀p:stmt_params.∀g.∀l:bind_new (localsT p) (list (joint_seq p g)).bind_seq_block p g (joint_step p g) ≝
    177255  bind_seq_list_bind_seq_block on _l : bind_new ? (list (joint_seq ??)) to bind_seq_block ?? (joint_step ??).
     256*)
    178257
    179258notation > "x ~❨ B , l ❩~> y 'in' c" with precedence 56 for
     
    183262  @{'block_in_code $c $x $B $l $y}.
    184263
     264notation > "x ~❨ B , l, r ❩~> y 'in' c" with precedence 56 for
     265  @{'bind_block_in_code $c $x $B $l $r $y}.
     266 
     267notation < "hvbox(x ~❨ B , l, r ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
     268  @{'bind_block_in_code $c $x $B $l $r $y}.
     269
    185270definition step_in_code ≝
    186271  λp,globals.λc : codeT p globals.λsrc : code_point p.λs : joint_step p globals.
     
    193278  stmt_at … c src = Some ? (final … s).
    194279
    195 let rec seq_list_in_code p globals (c : codeT p globals)
    196   (src : code_point p) (B : list (joint_seq p globals))
     280let rec step_list_in_code p globals (c : codeT p globals)
     281  (src : code_point p) (B : list (joint_step p globals))
    197282  (l : list (code_point p)) (dst : code_point p) on B : Prop ≝
    198283  match B with
     
    206291    [ nil ⇒ False
    207292    | cons mid rest ⇒
    208       step_in_code …  c src hd mid ∧ seq_list_in_code … c mid tl rest dst
     293      step_in_code …  c src hd mid ∧ step_list_in_code … c mid tl rest dst
    209294    ]
    210295  ].
    211296
    212 interpretation "seq list in code" 'block_in_code c x B l y = (seq_list_in_code ?? c x B l y).
    213 
    214 lemma seq_list_in_code_append :
     297interpretation "step list in code" 'block_in_code c x B l y = (step_list_in_code ?? c x B l y).
     298
     299lemma step_list_in_code_append :
    215300  ∀p,globals.∀c : codeT p globals.∀src,B1,l1,mid,B2,l2,dst.
    216301  src ~❨B1,l1❩~> mid in c → mid ~❨B2,l2❩~> dst in c →
     
    224309qed.
    225310
    226 lemma seq_list_in_code_append_inv :
     311lemma step_list_in_code_append_inv :
    227312  ∀p,globals.∀c : codeT p globals.∀src,B1,B2,l,dst.
    228313  src ~❨B1@B2,l❩~> dst in c →
    229314  ∃l1,mid,l2.l = l1 @ l2 ∧ src ~❨B1,l1❩~> mid in c ∧ mid ~❨B2,l2❩~> dst in c.
    230 #p #globals #c #src #B1 lapply src -src elim B1
     315#p #globals #c #src #B1 lapply src -src elim B1 -B1
    231316[ #src #B2 #l #dst #H %{[ ]} %{src} %{l} %{H} % %
    232317| #hd #tl #IH #src #B2 * [2: #mid #rest] #dst * #H1 #H2
     
    237322qed.
    238323
    239 definition seq_block_step_in_code ≝
    240   λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_step p g).λl,dst.
    241   ∃hd,tl.l = hd @ [tl] ∧
    242   src ~❨\fst B, l❩~> tl in c ∧ step_in_code … c tl (\snd B) dst.
    243 
    244 definition seq_block_fin_step_in_code ≝
    245   λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_fin_step p).λl.λdst : unit.
     324lemma append_not_empty_r : ∀X,l1,l2.not_empty X l2 → not_empty ? (l1 @ l2).
     325#X #l1 cases l1 -l1 [ #l2 #K @K | #hd #tl #l2 #_ % ] qed.
     326
     327definition map_eval : ∀X,Y : Type[0].list (X → Y) → X → list Y ≝ λX,Y,l,x.map … (λf.f x) l.
     328
     329definition step_block_in_code ≝
     330  λp,g.λc : codeT p g.λsrc.λb : step_block p g.λl,dst.
     331  let 〈pref, last〉 ≝ split_on_last_ne … b in
     332  ∃mid.src ~❨map_eval … pref mid, l❩~> mid in c ∧ step_in_code ?? c mid (last mid) dst.
     333
     334lemma map_compose : ∀X,Y,Z,f,g.∀l : list X.map Y Z f (map X Y g l) = map … (f∘g) l.
     335#X #Y #Z #f #g #l elim l -l normalize // qed.
     336
     337lemma map_ext_eq : ∀X,Y,f,g.∀l : list X.(∀x.f x = g x) → map X Y f l = map X Y g l.
     338#X #Y #f #g #l #H elim l -l normalize // qed.
     339
     340lemma map_id : ∀X.∀l : list X.map X X (λx.x) l = l.
     341#X #l elim l -l normalize // qed.
     342
     343lemma coerced_step_list_in_code :
     344∀p : params.∀g,c,src.∀b : list (joint_step p g).∀l,dst.
     345step_block_in_code p g c src b l dst →
     346match b with
     347[ nil ⇒ step_in_code … c src (NOOP …) dst
     348| _ ⇒ step_list_in_code … c src b (l@[dst]) dst
     349].
     350#p #g #c #src @list_elim_left [2: #last #pref #_ ] #l #dst
     351[2: * #src' * cases l [2: #hd' #tl' *] whd in ⊢ (%→?); #EQ destruct #K @K ]
     352cases pref -pref [2: #hd #tl ]
     353whd in ⊢ (%→?);
     354[2: * #src' * cases l [2: #hd' #tl' *] whd in ⊢ (%→?); #EQ destruct #K %{K} % ]
     355whd in match (ensure_step_block ???);
     356<map_append
     357change with ((? :: ?) @ ?) in match (? :: ? @ ?);
     358>split_on_last_ne_def normalize nodelta * #mid *
     359whd in match (map_eval ????);
     360>map_compose >map_id #H1 #H2
     361@(step_list_in_code_append … H1) %{H2} %
     362qed.
     363
     364definition fin_block_in_code ≝
     365  λp,g.λc:codeT p g.λsrc.λB : fin_block p g.λl.λdst : unit.
    246366  ∃hd,tl.l = hd @ [tl] ∧
    247367  src ~❨\fst B, l❩~> tl in c ∧ fin_step_in_code … c tl (\snd B).
     368
     369interpretation "step block in code" 'block_in_code c x B l y = (step_block_in_code ?? c x B l y).
     370interpretation "fin block in code" 'block_in_code c x B l y = (fin_block_in_code ?? c x B l y).
     371
     372let rec bind_new_instantiates B X
     373  (x : X) (b : bind_new B X) (l : list B) on b : Prop ≝
     374  match b with
     375  [ bret B ⇒
     376    match l with
     377    [ nil ⇒ x = B
     378    | _ ⇒ False
     379    ]
     380  | bnew f ⇒
     381    match l with
     382    [ nil ⇒ False
     383    | cons r l' ⇒
     384      bind_new_instantiates B X x (f r) l'
     385    ]
     386  ].
     387
     388definition bind_step_block_in_code ≝
     389  λp,g.λc:codeT p g.λsrc.λB : bind_step_block p g.λlbls,regs.λdst.
     390  ∃b.bind_new_instantiates … b B regs ∧ src ~❨b, lbls❩~> dst in c.
     391
     392definition bind_fin_block_in_code ≝
     393  λp,g.λc:codeT p g.λsrc.λB : bind_fin_block p g.λlbls,regs.λdst.
     394  ∃b.bind_new_instantiates … b B regs ∧ src ~❨b, lbls❩~> dst in c.
     395
     396interpretation "bound step block in code" 'bind_block_in_code c x B l r y = (bind_step_block_in_code ?? c x B l r y).
     397interpretation "bound fin block in code" 'bind_block_in_code c x B l r y = (bind_fin_block_in_code ?? c x B l r y).
    248398
    249399(* generates ambiguity even if it shouldn't
Note: See TracChangeset for help on using the changeset viewer.