Changeset 2186 for src/joint/blocks.ma


Ignore:
Timestamp:
Jul 16, 2012, 4:59:09 PM (8 years ago)
Author:
tranquil
Message:

updated joint semantics

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/blocks.ma

    r2155 r2186  
    176176  ∀p:stmt_params.∀g.∀l:bind_new (localsT p) (list (joint_seq p g)).bind_seq_block p g (joint_step p g) ≝
    177177  bind_seq_list_bind_seq_block on _l : bind_new ? (list (joint_seq ??)) to bind_seq_block ?? (joint_step ??).
     178
     179notation > "x ~❨ B , l ❩~> y 'in' c" with precedence 56 for
     180  @{'block_in_code $c $x $B $l $y}.
     181 
     182notation < "hvbox(x ~❨ B , l ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
     183  @{'block_in_code $c $x $B $l $y}.
     184
     185definition step_in_code ≝
     186  λp,globals.λc : codeT p globals.λsrc : code_point p.λs : joint_step p globals.
     187  λdst : code_point p.
     188  ∃nxt.stmt_at … c src = Some ? (sequential … s nxt) ∧
     189       point_of_succ … src nxt = dst.
     190
     191definition fin_step_in_code ≝
     192  λp,globals.λc : codeT p globals.λsrc : code_point p.λs : joint_fin_step p.
     193  stmt_at … c src = Some ? (final … s).
     194
     195let rec seq_list_in_code p globals (c : codeT p globals)
     196  (src : code_point p) (B : list (joint_seq p globals))
     197  (l : list (code_point p)) (dst : code_point p) on B : Prop ≝
     198  match B with
     199  [ nil ⇒
     200    match l with
     201    [ nil ⇒ src = dst
     202    | _ ⇒ False
     203    ]
     204  | cons hd tl ⇒
     205    match l with
     206    [ nil ⇒ False
     207    | cons mid rest ⇒
     208      step_in_code …  c src hd mid ∧ seq_list_in_code … c mid tl rest dst
     209    ]
     210  ].
     211
     212interpretation "seq list in code" 'block_in_code c x B l y = (seq_list_in_code ?? c x B l y).
     213
     214lemma seq_list_in_code_append :
     215  ∀p,globals.∀c : codeT p globals.∀src,B1,l1,mid,B2,l2,dst.
     216  src ~❨B1,l1❩~> mid in c → mid ~❨B2,l2❩~> dst in c →
     217  src ~❨B1@B2,l1@l2❩~> dst in c.
     218#p #globals #c #src #B1 lapply src -src elim B1
     219[ #src * [2: #mid' #rest] #mid #B2 #l2 #dst [*] #EQ normalize in EQ; destruct(EQ)
     220  #H @H
     221| #hd #tl #IH #src * [2: #mid' #rest] #mid #B2 #l2 #dst * #H1 #H2
     222  #H3 %{H1 (IH … H2 H3)}
     223]
     224qed.
     225
     226lemma seq_list_in_code_append_inv :
     227  ∀p,globals.∀c : codeT p globals.∀src,B1,B2,l,dst.
     228  src ~❨B1@B2,l❩~> dst in c →
     229  ∃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
     231[ #src #B2 #l #dst #H %{[ ]} %{src} %{l} %{H} % %
     232| #hd #tl #IH #src #B2 * [2: #mid #rest] #dst * #H1 #H2
     233  elim (IH … H2) #l1 * #mid' * #l2 ** #G1 #G2 #G3
     234  %{(mid::l1)} %{mid'} %{l2} %{G3} >G1 %{(refl …)}
     235  %{H1 G2}
     236]
     237qed.
     238
     239definition 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  src ~❨\fst B, \fst l❩~> \snd l in c ∧ step_in_code … c (\snd l) (\snd B) dst.
     242
     243definition seq_block_fin_step_in_code ≝
     244  λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_fin_step p).λl.λdst : unit.
     245  src ~❨\fst B, \fst l❩~> \snd l in c ∧ fin_step_in_code … c (\snd l) (\snd B).
     246
     247(* generates ambiguity even if it shouldn't
     248interpretation "seq block step in code" 'block_in_code c x B l y = (seq_block_step_in_code ?? c x B l y).
     249interpretation "seq block fin step in code" 'block_in_code c x B l y = (seq_block_fin_step_in_code ?? c x B l y).
     250*)
    178251
    179252(*
Note: See TracChangeset for help on using the changeset viewer.