Changeset 1949 for src/joint/blocks.ma


Ignore:
Timestamp:
May 15, 2012, 5:51:25 PM (8 years ago)
Author:
tranquil
Message:
  • lemma trace rel to eq flatten trace
  • some more properties of generic monad relations and predicates
  • removed 'iff notation from extralib as already there
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/blocks.ma

    r1908 r1949  
    22include "utilities/bind_new.ma".
    33
    4 inductive block_cont (p : params) (globals : list ident) : Type[0] ≝
    5   | Skip : block_cont p globals
    6   | Final : (Σs.no_seq p globals s) → block_cont p globals
    7   | Cons : joint_step p globals → block_cont p globals → block_cont p globals.
    8  
    9 definition instr_block ≝ λp : params.λglobals.bind_new (localsT p) (block_cont p globals).
    10 unification hint 0 ≔ p, globals;
    11 B ≟ block_cont p globals, R ≟ localsT p
     4definition uncurry_helper : ∀A,B,C : Type[0].(A → B → C) → (A×B) → C ≝
     5  λA,B,C,f,p.f (\fst p) (\snd p).
     6
     7inductive stmt_type : Type[0] ≝
     8  | SEQ : stmt_type
     9  | FIN : stmt_type.
     10
     11definition stmt_type_if : ∀A : Type[1].stmt_type → A → A → A ≝
     12  λA,t,x,y.match t with [ SEQ ⇒ x | FIN ⇒ y ].
     13
     14definition block_cont ≝ λp : params.λglobals,ty.
     15  (list (joint_step p globals)) ×
     16    (stmt_type_if ? ty (joint_step p) (joint_fin_step p) globals).
     17
     18definition Skip : ∀p,globals.block_cont p globals SEQ ≝
     19  λp,globals.〈[ ], NOOP …〉.
     20
     21definition instr_block ≝ λp : params.λglobals,ty.
     22  bind_new (localsT p) (block_cont p globals ty).
     23unification hint 0 ≔ p, globals, ty;
     24B ≟ block_cont p globals ty, R ≟ localsT p
    1225(*---------------------------------------*)⊢
    13 instr_block p globals ≡ bind_new R B.
    14 
    15 (* it returns b1 if it is ended by final rather than skip *)
    16 let rec block_cont_append p g (b1 : block_cont p g) (b2 : block_cont p g) on b1 : block_cont p g ≝
    17 match b1 with
    18 [ Skip ⇒ b2
    19 | Cons x b1' ⇒ Cons … x (block_cont_append … b1' b2)
    20 | Final _ ⇒ b1
    21 ].
    22 
    23 interpretation "block contents nil" 'vnil = (Skip ??).
    24 interpretation "block contents cons" 'vcons x b = (Cons ?? x b).
    25 interpretation "block contents append" 'vappend b1 b2 = (block_cont_append ?? b1 b2).
     26instr_block p globals ty ≡ bind_new R B.
     27
     28definition block_cont_append :
     29  ∀p,g,ty.
     30  ∀b1 : block_cont p g SEQ.
     31  ∀b2 : block_cont p g ty.
     32  block_cont p g ty ≝
     33  λp,globals,ty,b1,b2.〈\fst b1 @ \snd b1 :: \fst b2, \snd b2〉.
     34
     35definition block_cont_cons ≝ λp,g,ty,x.λb : block_cont p g ty.〈x :: \fst b,\snd b〉.
     36
     37interpretation "block contents cons" 'cons x b = (block_cont_cons ??? x b).
     38interpretation "block contents append" 'append b1 b2 = (block_cont_append ??? b1 b2).
     39
     40definition step_to_block : ∀p : params.∀g.
     41  joint_step p g → block_cont p g SEQ ≝ λp,g,s.〈[ ], s〉.
     42
     43definition fin_step_to_block : ∀p : params.∀g.
     44  joint_fin_step p g → block_cont p g FIN ≝ λp,g,s.〈[ ], s〉.
     45
     46coercion block_from_step : ∀p : params.∀g.∀s : joint_step p g.
     47  block_cont p g SEQ ≝ step_to_block on _s : joint_step ?? to block_cont ?? SEQ.
     48
     49coercion block_from_fin_step : ∀p : params.∀g.∀s : joint_fin_step p g.
     50  block_cont p g FIN ≝ fin_step_to_block
     51  on _s : joint_fin_step ?? to block_cont ?? FIN.
    2652
    2753definition block_cons :
    28   ∀p : params.∀globals.joint_step p globals → instr_block p globals → instr_block p globals
    29   ≝ λp,globals,x.m_map … (Cons … x).
     54  ∀p : params.∀globals,ty.
     55  joint_step p globals → instr_block p globals ty → instr_block p globals ty
     56  ≝ λp,globals,ty,x.m_map … (block_cont_cons … x).
    3057
    3158definition block_append :
    32   ∀p : params.∀globals.instr_block p globals → instr_block p globals → instr_block p globals ≝
    33   λp,globals.m_bin_op … (block_cont_append …).
    34 
    35 interpretation "instruction block nil" 'vnil = (bret ?? (Skip ??)).
    36 interpretation "instruction block cons" 'vcons x b = (block_cons ?? x b).
    37 interpretation "instruction block append" 'vappend b1 b2 = (block_append ?? b1 b2).
    38 
    39 let rec block_conts_of_list (p : params) globals (l : list (joint_step p globals)) on l : block_cont p globals ≝
    40   match l with
    41   [ nil ⇒ Skip ??
    42   | cons x l' ⇒ Cons … x (block_conts_of_list ?? l')
    43   ].
    44 definition inst_block_of_list :
    45   ∀p : params.∀globals.list (joint_step p globals) → instr_block p globals ≝
    46   λp,globals,l.return block_conts_of_list … l.
    47 
    48 coercion list_to_inst_block :
    49   ∀p : params.∀globals.∀l : list (joint_step p globals).instr_block p globals ≝
    50   inst_block_of_list on _l : list (joint_step ??) to instr_block ??.
    51 
    52 let rec is_block_instance (p : params) g (b : instr_block p g) (l : list (localsT p)) (b' : block_cont p g) on b : Prop ≝
     59  ∀p : params.∀globals,ty.
     60  instr_block p globals SEQ → instr_block p globals ty → instr_block p globals ty ≝
     61  λp,globals,ty.m_bin_op … (block_cont_append …).
     62
     63interpretation "instruction block cons" 'cons x b = (block_cons ??? x b).
     64interpretation "instruction block append" 'append b1 b2 = (block_append ??? b1 b2).
     65
     66let rec is_block_instance (p : params) g ty (b : instr_block p g ty) (l : list (localsT p)) (b' : block_cont p g ty) on b : Prop ≝
    5367  match b with
    5468  [ bret B ⇒
     
    6175    [ nil ⇒ False
    6276    | cons r l' ⇒
    63       is_block_instance p g (f r) l' b'
     77      is_block_instance p g ty (f r) l' b'
    6478    ]
    6579  ].
    6680
    67 lemma is_block_instance_append : ∀p,globals,b1,b2,l1,l2,b1',b2'.
    68   is_block_instance p globals b1 l1 b1' →
    69   is_block_instance p globals b2 l2 b2' →
    70   is_block_instance p globals (b1 @@ b2) (l1 @ l2) (b1' @@ b2').
    71 #p#globals#b1 elim b1
     81lemma is_block_instance_append : ∀p,globals,ty,b1,b2,l1,l2,b1',b2'.
     82  is_block_instance p globals SEQ b1 l1 b1' →
     83  is_block_instance p globals ty b2 l2 b2' →
     84  is_block_instance p globals ty (b1 @ b2) (l1 @ l2) (b1' @ b2').
     85#p#globals#ty #b1 elim b1
    7286[ #B1 | #f1 #IH1 ] #b2 * [2,4: #r1 #l1' ] #l2 #b1' #b2' [1,4: *]
    7387normalize in ⊢ (%→?);
     
    7690  [ #B2 | #f2 #IH2] * [2,4: #r2 #l2'] #b2' [1,4: *]
    7791  normalize in ⊢ (%→?); [2: //] #H2
    78   change with (is_block_instance ?? ('new ?) (r2 :: ?) ?) whd
     92  change with (is_block_instance ??? ('new ?) (r2 :: ?) ?) whd
    7993  @(IH2 … H2)
    8094]
     
    145159qed.
    146160
    147 let rec block_cont_in_code (p : params) g (c : codeT p g)
    148   (once : bool) src b (dst : option (code_point p))
    149   on b : Prop ≝
    150   match b with
    151   [ Skip ⇒
    152     match dst with
    153     [ Some x ⇒
    154       if once then src ~~>^+ x in c else src ~~>^* x in c
    155     | None ⇒ False
    156     ]
    157   | Final s ⇒
    158     match dst with
    159     [ Some _ ⇒ False
    160     | None ⇒ ∃mid.src ~~>^* mid in c ∧ stmt_at … c mid = Some ? s
    161     ]
    162   | Cons s B' ⇒
    163     ∃mid.src ~~>^* mid in c ∧
     161let rec seq_list_in_code (p : params) g (c : codeT p g)
     162  src l dst on l : Prop ≝
     163  match l with
     164  [ nil ⇒ src = dst
     165  | cons hd tl ⇒
     166    ∃n.stmt_at … c src = Some ? (sequential … hd n) ∧
     167       seq_list_in_code p g c (point_of_succ … src n) tl dst
     168  ].
     169
     170(*
     171definition seq_block_cont_to_list : ∀p,g.block_cont p g SEQ → list (joint_step p g) ≝
     172  λp,g,b.\fst b @ [\snd b].
     173
     174coercion list_from_seq_block_cont : ∀p,g.∀b:block_cont p g SEQ.list (joint_step p g) ≝
     175  seq_block_cont_to_list on _b : block_cont ?? SEQ to list (joint_step ??).
     176*)
     177
     178definition block_cont_in_code : ∀p,g.codeT p g → ∀ty.
     179  code_point p → block_cont p g ty → stmt_type_if ? ty (code_point p) unit → Prop ≝
     180  λp,g.λc : codeT p g.λty,src,b,dst.
     181  ∃mid.seq_list_in_code p g c src (\fst b) mid ∧
     182  match ty
     183  return λx.stmt_type_if ? x ??? →
     184    stmt_type_if ? x ?? → Prop
     185  with
     186  [ SEQ ⇒ λs,dst.
    164187      ∃n.stmt_at … c mid = Some ? (sequential … s n) ∧
    165         block_cont_in_code p g c false (point_of_succ … mid n) B' dst
    166    ].
    167    
    168 
    169 notation > "x ~❨ B opt( , b) ❩~> y 'in' c" with precedence 56 for
    170   ${default @{'block_in_code $c $b $x $B $y}
    171             @{'block_in_code $c false $x $B $y}
    172   }.
     188         point_of_succ … mid n = dst
     189  | FIN ⇒ λs.λ_.stmt_at … c mid = Some ? (final … s)
     190  ] (\snd b) dst.
    173191 
    174 notation < "hvbox(x ~❨ B , b ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
    175   @{'block_in_code $c $b $x $B $y}.
     192
     193notation > "x ~❨ B ❩~> y 'in' c" with precedence 56 for
     194  @{'block_in_code $c $x $B $y}.
     195 
    176196notation < "hvbox(x ~❨ B ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
    177   @{'block_in_code $c false $x $B $y}.
    178 
    179 interpretation "block cont in code" 'block_in_code c b x B y =
    180   (block_cont_in_code ?? c b x B y).
    181 
    182 lemma tunnel_append_l : ∀p,g.∀c : codeT p g.∀p,x,y,B,z.
    183   x ~~>^* y in c → y ~❨B,p❩~> z in c → x ~❨B,p❩~> z in c.
    184 #p #g #c #b #x #y *
    185 [ * [ #_ *] #z cases b
    186   [ @tunnel_tunnel_plus | @tunnel_trans]
    187 | #s * [2: #z #_ *]
    188 | #s #B' #z]
    189 #H1 * #mid * #H2 #H3 %{mid} %{? H3} @(tunnel_trans … H1 H2)
     197  @{'block_in_code $c $x $B $y}.
     198
     199interpretation "block cont in code" 'block_in_code c x B y =
     200  (block_cont_in_code ?? c ? x B y).
     201
     202lemma seq_list_in_code_append : ∀p,g.∀c : codeT p g.∀x,l1,y,l2,z.
     203  seq_list_in_code p g c x l1 y →
     204  seq_list_in_code p g c y l2 z →
     205  seq_list_in_code p g c x (l1@l2) z.
     206#p#g#c#x#l1 lapply x -x
     207elim l1 [2: #hd #tl #IH] #x #y #l2 #z normalize in ⊢ (%→?);
     208[ * #n * #EQ1 #H #G %{n} %{EQ1} @(IH … H G)
     209| #EQ destruct(EQ) //
     210]
     211qed.
     212
     213lemma block_cont_in_code_append : ∀p,g.∀c : codeT p g.∀ty,x.
     214  ∀B1 : block_cont p g SEQ.∀y.∀B2 : block_cont p g ty.∀z.
     215  x ~❨B1❩~> y in c → y ~❨B2❩~> z in c → x ~❨B1@B2❩~> z in c.
     216#p#g#c #ty #x * whd in match stmt_type_if in ⊢ (?→%→%→?); normalize nodelta
     217#l1 #s1 #y * #l2 #s2 #z * normalize nodelta
     218#mid1 * #H1 * #n * #EQ1 #EQ2 * #mid2 * #H2 #H3
     219%{mid2} %
     220[ whd in match (〈?,?〉@?);
     221  @(seq_list_in_code_append … H1)
     222  %{n} %{EQ1} >EQ2 assumption
     223| assumption
     224]
    190225qed.
    191226
    192 lemma tunnel_plus_append_l : ∀p,g.∀c : codeT p g.∀b,x,y,B,z.
    193   x ~~>^+ y in c → y ~❨B,b❩~> z in c → x ~❨B,true❩~> z in c.
    194 #p #g #c #b #x #y *
    195 [ * [ #_ *] #z cases b
    196   [ @tunnel_plus_trans | @tunnel_plus_tunnel]
    197 | #s * [2: #z #_ *]
    198 | #s #B' #z]
    199 #H1 * #mid * #H2 #H3 %{mid} %{? H3}
    200 @(tunnel_trans … H2) /2 by tunnel_plus_to_star/
    201 qed.
    202 
    203 lemma block_cont_in_code_plus_to_star : ∀p,g.∀c : codeT p g.∀b,x,B1,y.
    204   x ~❨B1,b❩~> y in c → x ~❨B1❩~> y in c.
    205 #p#g#c#b#x *
    206 [ * [*] #y cases b [ @tunnel_plus_to_star | //]
    207 |*: //
    208 ] qed.
    209 
    210 lemma block_cont_in_code_append : ∀p,g.∀c : codeT p g.∀b1,b2,x,B1,y,B2,z.
    211   x ~❨B1,b1❩~> Some ? y in c → y ~❨B2,b2❩~> z in c → x ~❨B1@@B2,b1∨b2❩~> z in c.
    212 #p#g#c #b1 #b2 #x #B1 lapply x -x lapply b2 -b2 lapply b1 -b1 elim B1
    213 [ * #b2 #x #y #B2 #z
    214   [ @tunnel_plus_append_l | @tunnel_append_l ]
    215 | #s #b1 #b2 #x #y #B2 #z *
    216 | #s #B1' #IH #b1 #b2 #x #y #B2 #dst * #m *
    217   #H1 * #n * #H2 #H3 #H4
    218   %{m} %{H1} %{n} %{H2} @(IH false false … H3)
    219   @(block_cont_in_code_plus_to_star … H4)
    220 ]
    221 qed.
    222 
    223227definition instr_block_in_function :
    224   ∀p,g.∀fn : joint_internal_function g p.bool →
    225     instr_block p g
     228  ∀p,g.∀fn : joint_internal_function g p.∀ty.
     229    instr_block p g ty
    226230    code_point p →
    227     option (code_point p) → Prop ≝
    228  λp,g,fn,b,B,src,dst.
     231    ? → Prop ≝
     232 λp,g,fn,ty,B,src,dst.
    229233 ∃vars,B'.
    230234  All ? (In ? (joint_if_locals … fn)) vars ∧
    231235  is_block_instance … B vars B' ∧
    232   src ~❨B',b❩~> dst in joint_if_code … fn.
    233 
    234 interpretation "instr block in function" 'block_in_code fn b x B y =
    235   (instr_block_in_function ?? fn b B x y).
     236  src ~❨B'❩~> dst in joint_if_code … fn.
     237
     238interpretation "instr block in function" 'block_in_code fn x B y =
     239  (instr_block_in_function ?? fn ? B x y).
    236240
    237241lemma instr_block_in_function_trans :
    238   ∀p,g.∀fn : joint_internal_function p g.∀b1,b2,src,B1,mid,B2,dst.
    239   src ~❨B1,b1❩~> Some ? mid in fn →
    240   mid ~❨B2,b2❩~> dst in fn →
    241   src ~❨B1@@B2,b1∨b2❩~> dst in fn.
    242 #p#g#fn#b1#b2#x#B1#y#B2#z
     242  ∀p,g.∀fn : joint_internal_function g p.∀ty,src.
     243  ∀B1 : instr_block p g SEQ.
     244  ∀mid.∀B2 : instr_block p g ty.∀dst.
     245  src ~❨B1❩~> mid in fn →
     246  mid ~❨B2❩~> dst in fn →
     247  src ~❨B1@B2❩~> dst in fn.
     248#p#g#fn#ty#src#B1#mid#B2#dst
    243249* #vars1 * #b1 ** #vars1_ok #b1B1 #b1_in
    244250* #vars2 * #b2 ** #vars2_ok #b2B2 #b2_in
    245 %{(vars1@vars2)} %{(b1 @@ b2)}
    246 /4 by is_block_instance_append, block_cont_in_code_append, All_append, conj/
    247 qed.
     251%{(vars1@vars2)} %{(b1 @ b2)}
     252/4 by All_append, conj, is_block_instance_append, block_cont_in_code_append/
     253qed.
Note: See TracChangeset for help on using the changeset viewer.