root/src/joint/blocks.ma @ 1908

include "joint/Joint_paolo.ma".
include "utilities/bind_new.ma".

inductive block_cont (p : params) (globals : list ident) : Type[0] ≝
  | Skip : block_cont p globals
  | Final : (Σs.no_seq p globals s) → block_cont p globals
  | Cons : joint_step p globals → block_cont p globals → block_cont p globals.
  
definition instr_block ≝ λp : params.λglobals.bind_new (localsT p) (block_cont p globals).
unification hint 0 ≔ p, globals;
B ≟ block_cont p globals, R ≟ localsT p
(*---------------------------------------*)⊢
instr_block p globals ≡ bind_new R B.

(* it returns b1 if it is ended by final rather than skip *)
let rec block_cont_append p g (b1 : block_cont p g) (b2 : block_cont p g) on b1 : block_cont p g ≝
match b1 with
[ Skip ⇒ b2
| Cons x b1' ⇒ Cons … x (block_cont_append … b1' b2)
| Final _ ⇒ b1
].

interpretation "block contents nil" 'vnil = (Skip ??).
interpretation "block contents cons" 'vcons x b = (Cons ?? x b).
interpretation "block contents append" 'vappend b1 b2 = (block_cont_append ?? b1 b2).

definition block_cons :
  ∀p : params.∀globals.joint_step p globals → instr_block p globals → instr_block p globals
  ≝ λp,globals,x.m_map … (Cons … x).

definition block_append :
  ∀p : params.∀globals.instr_block p globals → instr_block p globals → instr_block p globals ≝
  λp,globals.m_bin_op … (block_cont_append …).

interpretation "instruction block nil" 'vnil = (bret ?? (Skip ??)).
interpretation "instruction block cons" 'vcons x b = (block_cons ?? x b).
interpretation "instruction block append" 'vappend b1 b2 = (block_append ?? b1 b2).

let rec block_conts_of_list (p : params) globals (l : list (joint_step p globals)) on l : block_cont p globals ≝
  match l with
  [ nil ⇒ Skip ??
  | cons x l' ⇒ Cons … x (block_conts_of_list ?? l')
  ].
definition inst_block_of_list :
  ∀p : params.∀globals.list (joint_step p globals) → instr_block p globals ≝
  λp,globals,l.return block_conts_of_list … l.

coercion list_to_inst_block :
  ∀p : params.∀globals.∀l : list (joint_step p globals).instr_block p globals ≝
  inst_block_of_list on _l : list (joint_step ??) to instr_block ??.

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 ≝
  match b with
  [ bret B ⇒
    match l with
    [ nil ⇒ B = b'
    | cons _ _ ⇒ False
    ]
  | bnew f ⇒
    match l with
    [ nil ⇒ False
    | cons r l' ⇒
      is_block_instance p g (f r) l' b'
    ]
  ].

lemma is_block_instance_append : ∀p,globals,b1,b2,l1,l2,b1',b2'.
  is_block_instance p globals b1 l1 b1' →
  is_block_instance p globals b2 l2 b2' →
  is_block_instance p globals (b1 @@ b2) (l1 @ l2) (b1' @@ b2').
#p#globals#b1 elim b1
[ #B1 | #f1 #IH1 ] #b2 * [2,4: #r1 #l1' ] #l2 #b1' #b2' [1,4: *]
normalize in ⊢ (%→?);
[ @IH1
| #EQ destruct(EQ) lapply b2' -b2' lapply l2 -l2 elim b2
  [ #B2 | #f2 #IH2] * [2,4: #r2 #l2'] #b2' [1,4: *]
  normalize in ⊢ (%→?); [2: //] #H2
  change with (is_block_instance ?? ('new ?) (r2 :: ?) ?) whd
  @(IH2 … H2)
]
qed.

definition tunnel_step : ∀p,g.codeT p g → relation (code_point p) ≝
  λp,g,c,x,y.∃l.stmt_at … c x = Some ? (GOTO … l) ∧ point_of_label … c l = Some ? y.

notation > "x ~~> y 'in' c" with precedence 56 for @{'tunnel_step $c $x $y}.
notation < "hvbox(x ~~> y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel_step $c $x $y}.
interpretation "tunnel step in code" 'tunnel_step c x y = (tunnel_step ?? c x y).

let rec tunnel_through p g (c : codeT p g) x through y on through : Prop ≝
  match through with
  [ nil ⇒ x = y
  | cons hd tl ⇒ x ~~> hd in c ∧ tunnel_through … hd tl y
  ].

definition tunnel ≝ λp,g,c,x,y.∃through.tunnel_through p g c x through y.

notation > "x ~~>^* y 'in' c" with precedence 56 for @{'tunnel $c $x $y}.
notation < "hvbox(x \nbsp ~~>^* \nbsp y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel $c $x $y}.
interpretation "tunnel in code" 'tunnel c x y = (tunnel ?? c x y).

lemma tunnel_refl : ∀p,g.∀c : codeT p g.reflexive ? (tunnel p g c).
#p #g #c #x %{[]} % qed.

lemma tunnel_trans : ∀p,g.∀c : codeT p g.
  transitive ? (tunnel p g c).
#p#g#c #x#y#z * #l1 #H1 * #l2 #H2 %{(l1@l2)}
lapply H1 -H1 lapply x -x elim l1 -l1
[ #x #H1 >H1 @H2
| #hd #tl #IH #x * #H11 #H12
  %{H11} @IH @H12
] qed.
 
definition tunnel_plus ≝ λp,g.λc : codeT p g.λx,y.
  ∃mid.x ~~> mid in c ∧ mid ~~>^* y in c.

notation > "x ~~>^+ y 'in' c" with precedence 56 for @{'tunnel_plus $c $x $y}.
notation < "hvbox(x \nbsp ~~>^+ \nbsp y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel_plus $c $x $y}.
interpretation "tunnel in code" 'tunnel_plus c x y = (tunnel_plus ?? c x y).

lemma tunnel_plus_to_star : ∀p,g.∀c : codeT p g.∀x,y.x ~~>^+ y in c → x ~~>^* y in c.
#p #g #c #x #y * #mid * #H1 * #through #H2 %{(mid :: through)}
%{H1 H2} qed.

lemma tunnel_plus_trans : ∀p,g.∀c : codeT p g.transitive ? (tunnel_plus p g c).
#p #g #c #x #y #z * #mid * #H1 #H2
#H3 %{mid} %{H1} @(tunnel_trans … H2) /2 by tunnel_plus_to_star/
qed.

lemma tunnel_tunnel_plus : ∀p,g.∀c : codeT p g.∀x,y,z.
  x ~~>^* y in c → y ~~>^+ z in c → x ~~>^+ z in c.
#p #g #c #x #y #z * #through
lapply x -x elim through
[ #x #H1 >H1 //
| #hd #tl #IH #x * #H1 #H2 #H3
  %{hd} %{H1} @(tunnel_trans ???? y)
  [ %{tl} assumption | /2 by tunnel_plus_to_star/]
]
qed.

lemma tunnel_plus_tunnel : ∀p,g.∀c : codeT p g.∀x,y,z.
  x ~~>^+ y in c → y ~~>^* z in c → x ~~>^+ z in c.
#p #g #c #x #y #z * #mid * #H1 #H2 #H3 %{mid} %{H1}
@(tunnel_trans … H2 H3)
qed.

let rec block_cont_in_code (p : params) g (c : codeT p g)
  (once : bool) src b (dst : option (code_point p))
  on b : Prop ≝
  match b with
  [ Skip ⇒
    match dst with
    [ Some x ⇒
      if once then src ~~>^+ x in c else src ~~>^* x in c
    | None ⇒ False
    ]
  | Final s ⇒
    match dst with
    [ Some _ ⇒ False
    | None ⇒ ∃mid.src ~~>^* mid in c ∧ stmt_at … c mid = Some ? s
    ]
  | Cons s B' ⇒
    ∃mid.src ~~>^* mid in c ∧
      ∃n.stmt_at … c mid = Some ? (sequential … s n) ∧
        block_cont_in_code p g c false (point_of_succ … mid n) B' dst
   ].
   

notation > "x ~❨ B opt( , b) ❩~> y 'in' c" with precedence 56 for
  ${default @{'block_in_code $c $b $x $B $y}
            @{'block_in_code $c false $x $B $y}
  }.
  
notation < "hvbox(x ~❨ B , b ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
  @{'block_in_code $c $b $x $B $y}.
notation < "hvbox(x ~❨ B ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
  @{'block_in_code $c false $x $B $y}.

interpretation "block cont in code" 'block_in_code c b x B y =
  (block_cont_in_code ?? c b x B y).

lemma tunnel_append_l : ∀p,g.∀c : codeT p g.∀p,x,y,B,z.
  x ~~>^* y in c → y ~❨B,p❩~> z in c → x ~❨B,p❩~> z in c.
#p #g #c #b #x #y * 
[ * [ #_ *] #z cases b
  [ @tunnel_tunnel_plus | @tunnel_trans]
| #s * [2: #z #_ *]
| #s #B' #z]
#H1 * #mid * #H2 #H3 %{mid} %{? H3} @(tunnel_trans … H1 H2)
qed. 

lemma tunnel_plus_append_l : ∀p,g.∀c : codeT p g.∀b,x,y,B,z.
  x ~~>^+ y in c → y ~❨B,b❩~> z in c → x ~❨B,true❩~> z in c.
#p #g #c #b #x #y *
[ * [ #_ *] #z cases b
  [ @tunnel_plus_trans | @tunnel_plus_tunnel]
| #s * [2: #z #_ *]
| #s #B' #z]
#H1 * #mid * #H2 #H3 %{mid} %{? H3}
@(tunnel_trans … H2) /2 by tunnel_plus_to_star/
qed.

lemma block_cont_in_code_plus_to_star : ∀p,g.∀c : codeT p g.∀b,x,B1,y.
  x ~❨B1,b❩~> y in c → x ~❨B1❩~> y in c.
#p#g#c#b#x *
[ * [*] #y cases b [ @tunnel_plus_to_star | //]
|*: //
] qed.

lemma block_cont_in_code_append : ∀p,g.∀c : codeT p g.∀b1,b2,x,B1,y,B2,z.
  x ~❨B1,b1❩~> Some ? y in c → y ~❨B2,b2❩~> z in c → x ~❨B1@@B2,b1∨b2❩~> z in c.
#p#g#c #b1 #b2 #x #B1 lapply x -x lapply b2 -b2 lapply b1 -b1 elim B1
[ * #b2 #x #y #B2 #z
  [ @tunnel_plus_append_l | @tunnel_append_l ]
| #s #b1 #b2 #x #y #B2 #z *
| #s #B1' #IH #b1 #b2 #x #y #B2 #dst * #m *
  #H1 * #n * #H2 #H3 #H4
  %{m} %{H1} %{n} %{H2} @(IH false false … H3)
  @(block_cont_in_code_plus_to_star … H4)
]
qed.

definition instr_block_in_function :
  ∀p,g.∀fn : joint_internal_function g p.bool →
    instr_block p g →
    code_point p →
    option (code_point p) → Prop ≝
 λp,g,fn,b,B,src,dst.
 ∃vars,B'.
  All ? (In ? (joint_if_locals … fn)) vars ∧
  is_block_instance … B vars B' ∧
  src ~❨B',b❩~> dst in joint_if_code … fn.

interpretation "instr block in function" 'block_in_code fn b x B y =
  (instr_block_in_function ?? fn b B x y).

lemma instr_block_in_function_trans :
  ∀p,g.∀fn : joint_internal_function p g.∀b1,b2,src,B1,mid,B2,dst.
  src ~❨B1,b1❩~> Some ? mid in fn →
  mid ~❨B2,b2❩~> dst in fn →
  src ~❨B1@@B2,b1∨b2❩~> dst in fn.
#p#g#fn#b1#b2#x#B1#y#B2#z
* #vars1 * #b1 ** #vars1_ok #b1B1 #b1_in
* #vars2 * #b2 ** #vars2_ok #b2B2 #b2_in
%{(vars1@vars2)} %{(b1 @@ b2)}
/4 by is_block_instance_append, block_cont_in_code_append, All_append, conj/
qed.