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

definition uncurry_helper : ∀A,B,C : Type[0].(A → B → C) → (A×B) → C ≝
  λA,B,C,f,p.f (\fst p) (\snd p).

inductive stmt_type : Type[0] ≝
  | SEQ : stmt_type
  | FIN : stmt_type.

definition stmt_type_if : ∀A : Type[1].stmt_type → A → A → A ≝
  λA,t,x,y.match t with [ SEQ ⇒ x | FIN ⇒ y ].

definition block_cont ≝ λp : params.λglobals,ty.
  (list (joint_step p globals)) ×
    (stmt_type_if ? ty (joint_step p) (joint_fin_step p) globals).

definition Skip : ∀p,globals.block_cont p globals SEQ ≝
  λp,globals.〈[ ], NOOP …〉.

definition instr_block ≝ λp : params.λglobals,ty.
  bind_new (localsT p) (block_cont p globals ty).
unification hint 0 ≔ p, globals, ty;
B ≟ block_cont p globals ty, R ≟ localsT p
(*---------------------------------------*)⊢
instr_block p globals ty ≡ bind_new R B.

definition block_cont_append : 
  ∀p,g,ty.
  ∀b1 : block_cont p g SEQ.
  ∀b2 : block_cont p g ty.
  block_cont p g ty ≝
  λp,globals,ty,b1,b2.〈\fst b1 @ \snd b1 :: \fst b2, \snd b2〉.

definition block_cont_cons ≝ λp,g,ty,x.λb : block_cont p g ty.〈x :: \fst b,\snd b〉.

interpretation "block contents cons" 'cons x b = (block_cont_cons ??? x b).
interpretation "block contents append" 'append b1 b2 = (block_cont_append ??? b1 b2).

definition step_to_block : ∀p : params.∀g.
  joint_step p g → block_cont p g SEQ ≝ λp,g,s.〈[ ], s〉.

definition fin_step_to_block : ∀p : params.∀g.
  joint_fin_step p g → block_cont p g FIN ≝ λp,g,s.〈[ ], s〉.

coercion block_from_step : ∀p : params.∀g.∀s : joint_step p g.
  block_cont p g SEQ ≝ step_to_block on _s : joint_step ?? to block_cont ?? SEQ.

coercion block_from_fin_step : ∀p : params.∀g.∀s : joint_fin_step p g.
  block_cont p g FIN ≝ fin_step_to_block
  on _s : joint_fin_step ?? to block_cont ?? FIN.

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

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

interpretation "instruction block cons" 'cons x b = (block_cons ??? x b).
interpretation "instruction block append" 'append b1 b2 = (block_append ??? b1 b2).

let 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 ≝
  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 ty (f r) l' b'
    ]
  ].

lemma is_block_instance_append : ∀p,globals,ty,b1,b2,l1,l2,b1',b2'.
  is_block_instance p globals SEQ b1 l1 b1' →
  is_block_instance p globals ty b2 l2 b2' →
  is_block_instance p globals ty (b1 @ b2) (l1 @ l2) (b1' @ b2').
#p#globals#ty #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 seq_list_in_code (p : params) g (c : codeT p g)
  src l dst on l : Prop ≝
  match l with
  [ nil ⇒ src = dst
  | cons hd tl ⇒
    ∃n.stmt_at … c src = Some ? (sequential … hd n) ∧
       seq_list_in_code p g c (point_of_succ … src n) tl dst
  ].

(*
definition seq_block_cont_to_list : ∀p,g.block_cont p g SEQ → list (joint_step p g) ≝
  λp,g,b.\fst b @ [\snd b].

coercion list_from_seq_block_cont : ∀p,g.∀b:block_cont p g SEQ.list (joint_step p g) ≝
  seq_block_cont_to_list on _b : block_cont ?? SEQ to list (joint_step ??).
*)

definition unit_deqset: DeqSet ≝ mk_DeqSet unit (λ_.λ_.true) ?.
 * * /2/
qed.

definition block_cont_in_code : ∀p,g.codeT p g → ∀ty.
  code_point p → block_cont p g ty → stmt_type_if ? ty (code_point p) unit_deqset → Prop ≝
  λp,g.λc : codeT p g.λty,src,b,dst.
  ∃mid.seq_list_in_code p g c src (\fst b) mid ∧
  match ty
  return λx.stmt_type_if ? x ??? →
    stmt_type_if ? x ? unit_deqset → Prop
  with
  [ SEQ ⇒ λs,dst.
      ∃n.stmt_at … c mid = Some ? (sequential … s n) ∧
         point_of_succ … mid n = dst
  | FIN ⇒ λs.λ_.stmt_at … c mid = Some ? (final … s)
  ] (\snd b) dst.
  

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

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

lemma seq_list_in_code_append : ∀p,g.∀c : codeT p g.∀x,l1,y,l2,z.
  seq_list_in_code p g c x l1 y →
  seq_list_in_code p g c y l2 z →
  seq_list_in_code p g c x (l1@l2) z.
#p#g#c#x#l1 lapply x -x
elim l1 [2: #hd #tl #IH] #x #y #l2 #z normalize in ⊢ (%→?);
[ * #n * #EQ1 #H #G %{n} %{EQ1} @(IH … H G)
| #EQ destruct(EQ) //
]
qed.

lemma block_cont_in_code_append : ∀p,g.∀c : codeT p g.∀ty,x.
  ∀B1 : block_cont p g SEQ.∀y.∀B2 : block_cont p g ty.∀z.
  x ~❨B1❩~> y in c → y ~❨B2❩~> z in c → x ~❨B1@B2❩~> z in c.
#p#g#c #ty #x * whd in match stmt_type_if in ⊢ (?→%→%→?); normalize nodelta
#l1 #s1 #y * #l2 #s2 #z * normalize nodelta
#mid1 * #H1 * #n * #EQ1 #EQ2 * #mid2 * #H2 #H3
%{mid2} %
[ whd in match (〈?,?〉@?);
  @(seq_list_in_code_append … H1)
  %{n} %{EQ1} >EQ2 assumption
| assumption
]
qed. 

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

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

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