source: src/joint/linearise.ma @ 2939

(* include "joint/TranslateUtils.ma". *)
include "joint/Joint.ma".
include "utilities/hide.ma".

definition graph_to_lin_statement :
  ∀p : uns_params.∀globals.
  ∀A.identifier_map LabelTag A →
  joint_statement (mk_graph_params p) globals → joint_statement (mk_lin_params p) globals ≝
  λp,globals,A,visited,stmt.
  match stmt return λ_.joint_statement (mk_lin_params ?) ? with
  [ sequential c nxt ⇒
    match c with
    [ COND a ltrue ⇒
      if nxt ∈ visited then FCOND … I a ltrue nxt else
      sequential (mk_lin_params p) … c it
    | _ ⇒ sequential (mk_lin_params p) … c it
    ]
  | final c ⇒ final … c
  | FCOND abs _ _ _ ⇒ Ⓧabs
  ].

(*
lemma graph_to_lin_labels :
  ∀p : uns_params.∀globals,s.
  stmt_labels … (graph_to_lin_statement p globals s) =
  stmt_explicit_labels … s.
#p#globals * [//] * //
qed.
*)

(* discard all elements passing test, return first element failing it *)
(* and the rest of the list, if any. *)
let rec chop A (test : A → bool) (l : list A) on l : option (A × (list A)) ≝
  match l with
  [ nil ⇒ None ?
  | cons x l' ⇒ if test x then chop A test l' else return 〈x, l'〉
  ].

lemma chop_ok : ∀A,f,l.
  match chop A f l with
  [ Some pr ⇒ 
    let x ≝ \fst pr in
    let post ≝ \snd pr in
    ∃pre.All ? (λx.bool_to_Prop (f x)) pre ∧
    l = pre @ x :: post ∧ ¬bool_to_Prop (f x)
  | None ⇒ All A (λx.bool_to_Prop (f x)) l
  ].
#A #f #l elim l
[ %
| #hd #tl #IH whd in match (chop ???);
  elim (true_or_false_Prop (f hd)) #H >H normalize nodelta
  [ lapply IH elim (chop ???) normalize nodelta
    [ #G %{H G}
    | #pr * #pre ** #H1 #H2 #H3 %{(hd :: pre)} %{H3} %
      [ %{H H1}
      | >H2 %
      ]
    ]
  | %{[ ]} %{H} %%
  ]
]
qed.
 
unification hint 0 ≔ p, globals;
lp ≟ lin_params_to_params p,
sp ≟ stmt_pars lp,
js ≟ joint_statement sp globals,
lo ≟ labelled_obj LabelTag js
(*----------------------------*)⊢
list lo ≡ codeT lp globals.

definition graph_visit_ret_type ≝ λp,globals.λg : codeT (mk_graph_params p) globals.
  λentry : label.
  (Σ〈visited'   : identifier_map LabelTag ℕ,
   required'  : identifier_set LabelTag,
   generated' : codeT (mk_lin_params p) globals〉.'hide (
      And (And (And (And
        (lookup ?? visited' entry = Some ? 0)
        (required' ⊆ visited'))
        ((∃last.stmt_at … generated' 0 = Some ? (final … last)) ∨
         (∃a,ltrue,lfalse.stmt_at … generated' 0 = Some ? (FCOND … I a ltrue lfalse))))
        (code_forall_labels … (λl.bool_to_Prop (l∈required')) (rev … generated')))
        (∀l,n.lookup ?? visited' l = Some ? n →
          And (bool_to_Prop (code_has_label … (rev ? generated') l))
            (∃s.And
              (lookup … g l = Some ? s)
              (match s with
               [ sequential s' nxt ⇒
                 match s' with
                 [ COND a ltrue ⇒
                   Or
                    (And (nth_opt … n (rev … generated') =
                            Some ? 〈Some ? l, sequential … (COND … a ltrue) it〉)
                         (lookup … visited' nxt = Some ? (S n)))
                    (nth_opt … n (rev … generated') =
                            Some ? 〈Some ? l, FCOND … I a ltrue nxt〉)
                 |  _ ⇒
                   And
                     (nth_opt … n (rev … generated') =
                        Some ? 〈Some ? l, sequential … s' it〉)
                     (Or (lookup … visited' nxt = Some ? (S n))
                      (nth_opt … (S n) (rev … generated') =
                       Some ? 〈None ?, GOTO … nxt〉))
                
                 ]
               | final s' ⇒
                  nth_opt … n (rev … generated') =
                            Some ? 〈Some ? l, final … s'〉
               | FCOND abs _ _ _ ⇒ Ⓧabs
               ]))))).
                
unification hint 0 ≔ tag ⊢ identifier_set tag ≡ identifier_map tag unit.

include alias "common/Identifiers.ma".

lemma lookup_safe_elim : ∀tag,A.∀P : A → Prop.∀m,i,prf.
  (∀x.lookup tag A m i = Some ? x → P x) → P (lookup_safe tag A m i prf) ≝
λtag,A,P,m,i,prf,H.(H … (lookup_eq_safe …)).

let rec graph_visit
  (p : uns_params)
  (globals: list ident)
  (g : codeT (mk_graph_params p) globals)
  (* = graph (joint_statement (mk_graph_params p) globals *)
  (required: identifier_set LabelTag)
  (visited: identifier_map LabelTag ℕ) (* the reversed index of labels in the new code *)
  (generated: codeT (mk_lin_params p) globals)
  (* ≝ list ((option label)×(joint_statement (mk_lin_params p) globals)) *)
  (visiting: list label)
  (gen_length : ℕ)
  (n: nat)
  (entry : label)
  (g_prf : code_closed … g)
  (required_prf1 : ∀i.i∈required → Or (In ? visiting i) (bool_to_Prop (i∈visited)))
  (required_prf2 : code_forall_labels … (λl.bool_to_Prop (l ∈ required)) (rev … generated))
  (generated_prf1 : ∀l,n.lookup … visited l = Some ? n → hide_Prop (
    And (bool_to_Prop (code_has_label … (rev ? generated) l))
    (∃s.And
      (lookup … g l = Some ? s)
      (match s with
       [ sequential s' nxt ⇒
         match s' with
         [ COND a ltrue ⇒
           Or
            (And (nth_opt … n (rev … generated) =
                    Some ? 〈Some ? l, sequential … (COND … a ltrue) it〉)
                 (match lookup … visited nxt with
                  [ Some n' ⇒ n' = S n
                  | None ⇒ And (nth_opt ? 0 visiting = Some ? nxt) (S n = gen_length)
                  ]))
            (nth_opt … n (rev … generated) =
                    Some ? 〈Some ? l, FCOND … I a ltrue nxt〉)
         | _ ⇒
           And
             (nth_opt … n (rev … generated) =
                Some ? 〈Some ? l, sequential … s' it〉)
             (match lookup … visited nxt with
              [ Some n' ⇒ Or (n' = S n) (nth_opt … (S n) (rev … generated) = Some ? 〈None ?, GOTO … nxt〉)
              | None ⇒ And (nth_opt ? 0 visiting = Some ? nxt) (S n = gen_length)
              ])
         ]
       | final s' ⇒
          nth_opt … n (rev … generated) =
                    Some ? 〈Some ? l, final … s'〉
       | FCOND abs _ _ _ ⇒ Ⓧabs
       ]))))
  (generated_prf2 : ∀l.lookup … visited l = None ? → does_not_occur … l (rev ? generated))
  (generated_prf3 : (∃last.stmt_at … generated 0 = Some ? (final … last)) ∨
     (∃a,ltrue,lfalse.stmt_at … generated 0 = Some ? (FCOND … a ltrue lfalse)) ∨
     (¬All ? (λx.bool_to_Prop (x∈visited)) visiting))
  (visiting_prf : All … (λl.bool_to_Prop (l∈g)) visiting)
  (gen_length_prf : gen_length = length ? generated)
  (entry_prf : Or (And (And (visiting = [entry]) (gen_length = 0)) (Not (bool_to_Prop (entry∈visited))))
                  (lookup … visited entry = Some ? 0))
  (n_prf : le (id_map_size … g) (plus n (id_map_size … visited)))
  on n
  : graph_visit_ret_type … g entry ≝
  match chop ? (λx.x∈visited) visiting
  return λx.? → graph_visit_ret_type … g entry with
  [ None ⇒ λH.
    «〈visited, required, generated〉, ?»
  | Some pr ⇒ λH.
    let vis_hd ≝ \fst pr in
    let vis_tl ≝ \snd pr in
    match n return λx.? → graph_visit_ret_type … g entry with
    [ O ⇒ λn_prf'.⊥
    | S n' ⇒ λn_prf'.
      (* add the label to the visited ones *)
      let visited' ≝ add … visited vis_hd gen_length in
      (* take l's statement *)
      let hd_vis_in_g ≝ (hide_prf ? ?) in
      let statement ≝ lookup_safe ?? g vis_hd hd_vis_in_g in  
      (* translate it to its linear version *)
      let translated_statement ≝ graph_to_lin_statement … visited' statement in
      (* add the translated statement to the code (which will be reversed later) *)
      let generated' ≝ 〈Some … vis_hd, translated_statement〉 :: generated in
      let required' ≝ union_set ???
        (set_from_list … (stmt_explicit_labels … translated_statement))
        required in
      (* put successors in the visiting worklist *)
      let visiting' ≝ stmt_labels … statement @ vis_tl in
      (* finally, check the implicit successor *)
      (* if it has been already visited, we need to add a GOTO *)
      let add_req_gen ≝
        match statement with
        [ sequential s nxt ⇒
          match s with
          [ COND _ _ ⇒ 〈0, ∅, [ ]〉
          | _ ⇒
            if nxt ∈ visited' then
              〈1, {(nxt)}, [〈None label, (GOTO … nxt : joint_statement ??)〉]〉
            else 〈0, ∅, [ ]〉
          ]
        | _ ⇒ 〈0, ∅, [ ]〉
        ] in
      (* prepare a common utility to deal with add_req_gen *)
      let add_req_gen_prf :
        ∀P : (ℕ × (identifier_set LabelTag) × (codeT (mk_lin_params p) globals)) → Prop.
        (match statement with
         [ sequential s nxt ⇒
           match s with [ COND _ _ ⇒ True | _ ⇒ ¬bool_to_Prop (nxt ∈ visited') ]
         | _ ⇒ True] → P 〈0,∅,[ ]〉) →
        (∀nxt.match statement with
         [ sequential s nxt' ⇒
          match s with [ COND _ _ ⇒ False | _ ⇒
            nxt = nxt']
         | _ ⇒ False]
         → nxt ∈ visited' → P 〈1, {(nxt)}, [〈None ?, GOTO (mk_lin_params p) nxt〉]〉) →
        P add_req_gen ≝ hide_prf ?? in
      graph_visit ???
        (union_set ??? (\snd (\fst add_req_gen)) required')
        visited'
        (\snd add_req_gen @ generated')
        visiting'
        (plus (\fst (\fst add_req_gen)) (S gen_length))
        n' entry g_prf ?????????
    ] n_prf
  ] (chop_ok ? (λx.x∈visited) visiting).
cases daemon (*)
whd
[ (* base case, visiting is all visited *)
  %[%[%[%]]]
  [ elim entry_prf
    [ ** #eq_visiting #gen_length_O #entry_vis >eq_visiting in H; * >entry_vis *
    | //
    ]
  | #l #l_req
    elim (required_prf1 … l_req) #G
    [ @(All_In … H G)
    | assumption
    ]
  | cases generated_prf3 [/2 by /]
    * #ABS @⊥ @ABS assumption
  | assumption
  | #l #n #H elim (generated_prf1 … H) -H
    #H1 * #s * #H2 #H3 %{H1} %{s} %{H2}
    cases s in H3; [3: *]
    [ * ] normalize nodelta
    [1,2,4: [ #c | #f #args #dest |#s'] #nxt * #EQnth_opt #H %{EQnth_opt}
      inversion (lookup … visited nxt) in H; [2,4,6: #n'] normalize nodelta
      #EQlookup
      normalize nodelta *
      [1,3,5: #EQn' %1 >EQn' %
      |2,4,6: #H %2{H}
      |*: #H' lapply (All_nth … H … H')
        whd in ⊢ (?%→?); >EQlookup *
      ]
    | #a #ltrue #lfalse * [2: #H %2{H} ] * #H1 #H2 %1 %{H1}
      inversion (lookup … visited lfalse) in H2;
      [ #ABS * #H' lapply (All_nth … H … H')
        whd in ⊢ (?%→?); >ABS *
      | #n' #_ normalize nodelta #EQ >EQ %
      ]
    | #s #H @H
    ]
  ]
(* first, close goals where add_gen_req plays no role *)
|13: (* vis_hd is in g *)
  elim H #pre ** #_ #H2 #_
  @(All_split … visiting_prf … H2)
|2: (* n = 0 absrud *)
  elim H #pre ** #_ #H2 #H3
  @(absurd … n_prf')
  @lt_to_not_le
  lapply (add_size … visited vis_hd 0 (* dummy value *))
  >H3 normalize nodelta
  whd in match (lt ? ?);
  whd in match (1 + ?);
  #EQ <EQ @subset_card @add_subset
  [ @(All_split ? (λx.bool_to_Prop (x∈g)) ????? H2) @(All_mp … visiting_prf)
    #a elim g #gm whd in ⊢ (?→?%); #H >(lookup_eq_safe … H) %
  | #l #H
    elim (generated_prf1 … (lookup_eq_safe … H)) #_ * #s * #s_in_g #_
    whd in ⊢ (?%); >s_in_g %
  ]
|8:
  elim H #pre ** #_ #H2 #_
  @All_append
  [ elim(g_prf … vis_hd statement ?) [2:@lookup_eq_safe] #G1 #G2
    @(All_append … G1)
    cases statement in G2; [2: // |3: * ]
    #s #nxt #G' %{G'} %
  | >H2 in visiting_prf;
    #H' lapply (All_append_r … H') -H' * #_ //
  ]
|10:
  elim H #pre ** #_ #H2 #H3 -add_req_gen_prf
  %2 elim entry_prf
  [ ** >H2 cases pre
    [2: #x' #pre' #ABS normalize in ABS; destruct(ABS)
      cases pre' in e0; [2: #x'' #pre''] #ABS' normalize in ABS'; destruct(ABS')
    |1: #EQ normalize in EQ; destruct(EQ)
      #eq_gen_length #_
      >lookup_add_hit >eq_gen_length %
    ]
  | #lookup_entry cut (entry ≠ vis_hd)
    [ % whd in match vis_hd; #entry_vis_hd <entry_vis_hd in H3;
      whd in ⊢ (?(?%)→?); >lookup_entry * #ABS @ABS % ]
    #entry_not_vis_hd >(lookup_add_miss ?????? entry_not_vis_hd) assumption
  ]
|11:
  elim H #pre ** #_ #_ #H3
  >commutative_plus
  >add_size >H3 normalize nodelta
  whd in match (1 + ?);
  >commutative_plus
  assumption
|12: (* add_req_gen utility *)
  #P whd in match add_req_gen;
  cases statement [ * [ #cost | #f #args #dest|  #a #ltrue | #s ] #nxt | #s | * ]
  normalize nodelta
  [3,5: #H #_ @(H I) ]
  inversion (nxt ∈ visited') #EQ normalize nodelta
  #H1 #H2 [1,3,5: @(H2 … (refl …)) >EQ % |*: @H1 % * ]
|3: elim H #pre ** #H1 #H2 #_
  #i >mem_set_union
  #H elim (orb_Prop_true … H) -H
  [ @add_req_gen_prf [ #_ >mem_set_empty * ]
    #next #_ #next_vis #H >(mem_set_singl_to_eq … H) %2 assumption
  | >mem_set_union
    #H elim (orb_Prop_true … H) -H
    [ #i_expl %1 @Exists_append_l
      lapply i_expl whd in match translated_statement;
      cases statement [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | *]
      normalize nodelta #H
      lapply (mem_list_as_set … H) -H #H
      [1,2,4,5: @Exists_append_r assumption ]
      cases (nxt ∈ visited') in H; normalize nodelta * [2,4: * [2: * ]]
      #EQ destruct(EQ) [ %1 % |*: %2 %1 % ]
    | (* i was already required *)
      #i_req
      elim (required_prf1 … i_req)
      [ >H2 #H elim (Exists_append … H) -H
        [ (* i in preamble → i∈visited *)
          #i_pre %2 >mem_set_add @orb_Prop_r
          @(All_In … H1 i_pre)
        | *
          [ (* i is vis_hd *)
            #eq_i >eq_i %2 @mem_set_add_id
          | (* i in vis_tl → i∈visiting' *)
            #i_post % @Exists_append_r assumption
          ]
        ]
      | (* i in visited *)
        #i_vis %2 >mem_set_add @orb_Prop_r assumption
      ]
    ]
  ]
|4,5,6: change with reverse in match rev;
  >reverse_append whd in match (reverse ??); >rev_append_def
  >associative_append
  [ #pt #s
    @(leb_elim (S pt) (|generated|)) #cmp
    whd in match (stmt_at ????);
    [ >nth_opt_append_l [2: >length_reverse assumption ]
      change with (stmt_at ???? = ? → ?)
      #EQ lapply(required_prf2 … EQ) @All_mp
      #l #l_req >mem_set_union @orb_Prop_r
      >mem_set_union @orb_Prop_r @l_req
    | >nth_opt_append_r [2: >length_reverse @not_lt_to_le assumption ]
      cases (pt - ?)
      [ whd in match (nth_opt ???); whd in ⊢ (??%?→?);
        #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ) whd
        whd in match required';
        cut (∀p : lin_params.∀globals.∀s.
          stmt_implicit_label p globals s = None ?)
        [ #p #globals * normalize // ]
        #lin_implicit_label change with (? @ ?) in match (stmt_labels ???);
        >lin_implicit_label
        change with (All ?? (stmt_explicit_labels ???))
        generalize in match (stmt_explicit_labels … translated_statement);
        #l @list_as_set_All
        #i >mem_set_union >mem_set_union
        #i_l @orb_Prop_r @orb_Prop_l assumption
      | @add_req_gen_prf
        [ #_ | #next #_ #next_vis *
          [ whd in ⊢ (??%?→?);
            #EQ' destruct(EQ') whd %{I} >mem_set_union
            @orb_Prop_l @mem_set_add_id ]]
        #n whd in ⊢ (??%?→?); #ABS destruct(ABS)
      ]
    ]
  | elim H #pre ** #H1 #H2 #H3
    #i whd in match visited';
    @(eq_identifier_elim … i vis_hd)
    [ #EQi >EQi -i #pos
      >lookup_add_hit in ⊢ (%→?); #EQpos (* too slow: destruct(EQpos) *)
      cut (gen_length = pos)
      [ -visited destruct(EQpos) %]
      -EQpos #EQpos <EQpos -pos
      %
      [ >lin_code_has_label
        @add_req_gen_prf
        [ #_
        | #next #_ #next_vis 
          change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
          <associative_append >occurs_exactly_once_None
        ]
        >occurs_exactly_once_Some_eq >eq_identifier_refl
        normalize nodelta
        @generated_prf2
        lapply (in_map_domain … visited vis_hd)
        >H3 normalize nodelta //
      | %{statement}
        %
        [ @lookup_eq_safe
        | normalize nodelta
          change with statement in match (lookup_safe ?????);
          cases statement;
          [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ] normalize nodelta
          [1,2,3,4: inversion (nxt ∈ visited') normalize nodelta #nxt_vis ]
          [1,2,3,4,7,8: % | %2 | %1 % ]
          [1,3,5,7,9,11,13,14,16:
            >nth_opt_append_r >rev_length <gen_length_prf try %
            <minus_n_n try % try( whd in match graph_to_lin_statement; normalize nodelta
            >nxt_vis %)
          |*:
            lapply (in_map_domain … visited' nxt) >nxt_vis normalize nodelta
            [1,3,5: * #n' ] #EQlookup >EQlookup normalize nodelta
            try (%% @False)
            %2 >nth_opt_append_r >rev_length <gen_length_prf [2,4,6: %2 %1 ]
            <minus_Sn_n %
          ]
        ]
      ]
    | #NEQ #n_i >(lookup_add_miss … visited … NEQ)
      #Hlookup elim (generated_prf1 … Hlookup)
      #G1 * #s * #G2 #G3
      %
      [ >lin_code_has_label <associative_append
        >occurs_exactly_once_append
        @orb_Prop_l @andb_Prop
        [ >occurs_exactly_once_Some_eq
          >eq_identifier_false [2: % #ABS >ABS in NEQ; * #ABS' @ABS' % ]
          normalize nodelta >lin_code_has_label in G1; #K @K
        | @add_req_gen_prf
          [ #_ % |  #next #_ #_  % ]
        ]
      | %{s}
        %{G2}
        cases s in G3;
        [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ]
        [1,2,4: normalize nodelta #H cases H in ⊢ ?; -H
          #EQnth_opt #next_spec % |3: normalize nodelta * [*] #EQnth_opt [#next_spec %1 % | %2] | #EQnth_opt ]
        [1,3,5,7,9: @nth_opt_append_hit_l assumption
        |2,4,6,8: @(eq_identifier_elim … nxt vis_hd)
          [1,3,5,7: #EQ destruct(EQ) >lookup_add_hit whd
            [1,2,3: %1]
            lapply (in_map_domain … visited vis_hd)
            >H3 #EQ >EQ in next_spec; * #_ #OK >OK %
          |*: #NEQ' >(lookup_add_miss … visited … NEQ') in
            ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
            generalize in match next_spec in ⊢ ?;
            inversion (lookup … visited nxt) normalize nodelta
            [2,4,6,8: #n'' ] #EQlookup'
            [1,2,3: * [1,3,5: #H %1{H} ] #H %2 @nth_opt_append_hit_l assumption
            |4: #H @H
            |*: * #nxt_visiting @⊥
              >H2 in nxt_visiting;
              cases pre in H1;
              [1,3,5,7: #_
              |*: #frst #pre_tl * #ABS #_
              ] whd in ⊢ (??%?→?); #EQ destruct(EQ)
              [1,2,3,4: cases NEQ' #ABS cases (ABS ?) %
              |*: lapply ABS; whd in ⊢ (?%→?); >EQlookup' *
              ]
            ]
          ]
        |10: @nth_opt_append_hit_l assumption
        ]
      ]
    ]
  | #i whd in match visited';
    @(eq_identifier_elim … i vis_hd) #Heq
    [ >Heq >lookup_add_hit #ABS destruct(ABS) ]
    >(lookup_add_miss ?????? Heq)
    #i_n_vis
    >does_not_occur_append @andb_Prop
    [ @generated_prf2 assumption
    | change with (bool_to_Prop (¬eq_identifier ??? ∧ ?))
      >eq_identifier_false [2: % #ABS <ABS in Heq; * #ABS' @ABS' % ]
      @add_req_gen_prf [ #_ | #s #next #_ ] %
    ]
  ]
| @add_req_gen_prf
  [ #K | #next #K #next_vis %1 %1 %{(GOTO … next)} % ]
  whd in match generated'; whd in match translated_statement;
  normalize nodelta
  change with statement in match (lookup_safe ?????);
  cases statement in K;
  [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s #_ %1 %1 %{s} % | * ] normalize nodelta
  [3: #_ cases (true_or_false_Prop (nxt ∈ visited')) #nxt_vis
    [ >nxt_vis normalize nodelta %1 %2 %{a} %{ltrue} %{nxt} % ]
  |*: #nxt_vis ]
  %2 % * >nxt_vis *
| whd in match generated';
  @add_req_gen_prf [ #_ | #next #_ #_ ] normalize >gen_length_prf %
|
]
*)
qed. 

(* CSC: The branch compression (aka tunneling) optimization is not implemented
   in Matita *)
definition branch_compress 
  ≝ λp: graph_params.λglobals.λg:codeT p globals.
    λentry : Σl.bool_to_Prop (code_has_label … g l).g.
  
lemma branch_compress_closed : ∀p,globals,g,l.code_closed ?? g →
  code_closed … (branch_compress p globals g l).
#p#globals#g#l#H @H qed.

lemma branch_compress_has_entry : ∀p,globals,g,l.
  code_has_label … (branch_compress p globals g l) l.
#p#globals#g*#l#l_prf @l_prf qed.

definition filter_labels ≝ λtag,A.λtest : identifier tag → bool.λc : list (labelled_obj tag A).
  map ??
    (λs. let 〈l_opt,x〉 ≝ s in
      〈! l ← l_opt ; if test l then return l else None ?, x〉) c.
      
lemma does_not_occur_filter_labels :
  ∀tag,A,test,id,c.
    does_not_occur ?? id (filter_labels tag A test c) =
      (does_not_occur ?? id c ∨ ¬ test id).
#tag #A #test #id #c elim c
[ //
| ** [2: #lbl] #s #tl #IH
  whd in match (filter_labels ????); normalize nodelta
  whd in match (does_not_occur ????) in ⊢ (??%%);
  [2: @IH]
  normalize in match (! l ← ? ; ?); >IH
  @(eq_identifier_elim ?? lbl id) #Heq [<Heq]
  elim (test lbl) normalize nodelta
  change with (eq_identifier ???) in match (instruction_matches_identifier ????);
  [1,2: >eq_identifier_refl [2: >commutative_orb] normalize %
  |*: >(eq_identifier_false ??? Heq) normalize nodelta %
  ]
]
qed.

lemma occurs_exactly_once_filter_labels :
  ∀tag,A,test,id,c.
    occurs_exactly_once ?? id (filter_labels tag A test c) =
      (occurs_exactly_once ?? id c ∧ test id).
#tag #A #test #id #c elim c
[ //
| ** [2: #lbl] #s #tl #IH
  whd in match (filter_labels ????); normalize nodelta
  whd in match (occurs_exactly_once ????) in ⊢ (??%%);
  [2: @IH]
  normalize in match (! l ← ? ; ?); >IH
  >does_not_occur_filter_labels
  @(eq_identifier_elim ?? lbl id) #Heq [<Heq]
  elim (test lbl) normalize nodelta
  change with (eq_identifier ???) in match (instruction_matches_identifier ????);
  [1,2: >eq_identifier_refl >commutative_andb [ >(commutative_andb ? true) >commutative_orb | >(commutative_andb ? false)] normalize %
  |*: >(eq_identifier_false ??? Heq) normalize nodelta %
  ]
]
qed.

lemma nth_opt_filter_labels : ∀tag,A,test,instrs,n.
  nth_opt ? n (filter_labels tag A test instrs) =
  ! 〈lopt, s〉 ← nth_opt ? n instrs ;
  return 〈 ! lbl ← lopt; if test lbl then return lbl else None ?, s〉.
#tag #A #test #instrs elim instrs
[ * [2: #n'] %
| * #lopt #s #tl #IH * [2: #n']
  whd in match (filter_labels ????); normalize nodelta
  whd in match (nth_opt ???) in ⊢ (??%%); [>IH] %
]
qed.

lemma stmt_at_filter_labels : ∀p : lin_params.∀globals,test.∀c : codeT p globals.
∀i.stmt_at p globals (filter_labels ?? test c) i = stmt_at p globals c i.
#p#globals#test #c#i
whd in ⊢ (??%%); >nth_opt_filter_labels
elim (nth_opt ???); //
qed.

(* spostato in ExtraMonads.ma 
lemma option_bind_inverse : ∀A,B.∀m : option A.∀f : A → option B.∀r.
  ! x ← m ; f x = return r →
  ∃x.m = return x ∧ f x = return r.
#A #B * normalize [2:#x] #f #r #EQ destruct
%{x} %{EQ} %
qed.
*)

lemma nth_opt_reverse_hit :
  ∀A,l,n.n < |l| → nth_opt A n (reverse ? l) = nth_opt A (|l| - (S n)) l.
#A #l elim l
[ #n #ABS normalize in ABS; @⊥ -A /2 by absurd/
| #hd #tl #IH #n #lim whd in match (reverse ??); >rev_append_def 
  @(leb_elim (S n) (|tl|)) #H
  [ >nth_opt_append_l [2: >length_reverse @H ]
    >(IH … H) >(minus_Sn_m … H) %
  | >(le_to_le_to_eq … (le_S_S_to_le … lim) (not_lt_to_le … H))
    >nth_opt_append_r >length_reverse [2: % ]
    <minus_n_n <minus_n_n %
  ]
]
qed.

lemma nth_opt_reverse_hit_inv :
  ∀A,l,n.n < |l| → nth_opt A (|l| - (S n)) (reverse ? l) = nth_opt A n l.
#A #l #n #H <(reverse_reverse ? l) in ⊢ (???%); @sym_eq
<length_reverse @nth_opt_reverse_hit >length_reverse @H
qed.

definition good_local_sigma :
  ∀p:uns_params.
  ∀globals.
  ∀g:codeT (mk_graph_params p) globals.
  (Σl.bool_to_Prop (code_has_label … g l)) →
  codeT (mk_lin_params p) globals →
  (label → option ℕ) → Prop ≝
  λp,globals,g,entry,c,sigma.
    sigma entry = Some ? 0 ∧
    (∀l,n.point_of_label … c l = Some ? n → sigma l = Some ? n) ∧
    ∀l,n.sigma l = Some ? n →
      ∃s. stmt_at … g l = Some ? s ∧
          All ? (λl.sigma l ≠ None ?) (stmt_labels … s) ∧
          (match s with
           [ sequential s' nxt ⇒
             match s' with
             [ COND a ltrue ⇒
               (stmt_at … c n = Some ? (sequential … s' it) ∧ sigma nxt = Some ? (S n)) ∨
               (stmt_at … c n = Some ? (FCOND … I a ltrue nxt))
             | _ ⇒
                (stmt_at … c n = Some ? (sequential … s' it)) ∧
                  ((sigma nxt = Some ? (S n)) ∨
                   (stmt_at … c (S n) = Some ? (GOTO … nxt)))
             ]
           | final s' ⇒
             stmt_at … c n = Some ? (final … s')
           | FCOND abs _ _ _ ⇒ Ⓧabs
           ]).

definition linearise_code:
 ∀p : uns_params.∀globals.
  ∀g : codeT (mk_graph_params p) globals.code_closed … g →
  ∀entry : (Σl.bool_to_Prop (code_has_label … g l))
  .Σc_sigma.
    let c ≝ \fst c_sigma in
    let sigma ≝ \snd c_sigma in
    good_local_sigma … g entry c sigma ∧
    code_closed … c
       (* ∧
      ∃ sigma : identifier_map LabelTag ℕ.
      lookup … sigma entry = Some ? 0 ∧
      ∀l,n.lookup … sigma l = Some ? n →
        ∃s. lookup … g l = Some ? s ∧
          opt_Exists ?
            (λls.let 〈lopt, ts〉 ≝ ls in
              opt_All ? (eq ? l) lopt ∧
              ts = graph_to_lin_statement … s ∧
              opt_All ?
                (λnext.Or (lookup … sigma next = Some ? (S n))
                (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
                (stmt_implicit_label … s)) (nth_opt … n c)*)
≝
 λp,globals,g,g_prf,entry_sig.
    let g ≝ branch_compress (mk_graph_params p) ? g entry_sig in
    let g_prf ≝ branch_compress_closed … g entry_sig g_prf in
    match graph_visit p globals g ∅ (empty_map …) [ ] [entry_sig] 0 (|g|)
      (entry_sig) g_prf ?????????
    with
    [ mk_Sig triple H ⇒ 
      let sigma ≝ \fst (\fst triple) in
      let required ≝ \snd (\fst triple) in
      let crev ≝ \snd triple in
      let lbld_code ≝ rev ? crev in
      〈filter_labels … (λl.l∈required) lbld_code, lookup … sigma〉 ].
[ cases (graph_visit ????????????????????)
 (* done later *)
| #i >mem_set_empty *
|3,4: #a #b whd in ⊢ (??%?→?); #ABS destruct(ABS)
| #l #_ %
| %2 % * >mem_set_empty *
| % [2: %] @(branch_compress_has_entry … g entry_sig)
| %
| % % [% %] cases (pi1 … entry_sig) normalize #_ % //
| >commutative_plus change with (? ≤ |g|) %
]
cases daemon (*)
**
#visited #required #generated normalize nodelta ****
#entry_O #req_vis #last_fin #labels_in_req #sigma_prop
%
[ % [ % [assumption]]
  #lbl #n
  [ change with (If ? then with prf do ? else ? = ? → ?)
    @If_elim [2: #_ #ABS destruct(ABS) ]
    #H lapply H
    >occurs_exactly_once_filter_labels
    elim (true_or_false_Prop … (occurs_exactly_once ?? lbl ?))
    [1,2: #H1 >H1 |*:] [2: * ]
    elim (true_or_false_Prop … (lbl ∈ required)) #H2 >H2 *
    lapply (in_map_domain … visited lbl) >(req_vis … H2)
    * #n_lbl #EQsigma
    elim (sigma_prop … EQsigma) #_ * #stmt * #_
    cases stmt [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ] normalize nodelta
    [1,2,4: * #EQnth_opt #_ |3: * [ * ] #EQnth_opt [ #_ ] |5: #EQnth_opt ]
    >(nth_opt_index_of_label ???? n_lbl ? H)
    try (normalize in ⊢ (% → ?); #EQ destruct(EQ) assumption)
    [1,3,5,7,9,11:
      >nth_opt_filter_labels in ⊢ (??%?);
      (* without the try it does not work *)
      try >EQnth_opt in ⊢ (??%?);
      >m_return_bind in ⊢ (??%?);
      >m_return_bind in ⊢ (??%?);
      >H2 in ⊢ (??%?); %
    |*:
    ]
  | #eq_lookup elim (sigma_prop ?? eq_lookup)
    #lbl_in_gen * #stmt * #stmt_in_g #stmt_spec
    % [2: % [ % [ assumption ]] |]
    [ @All_append
      [ cases stmt in stmt_spec;
        [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s #_ % | * ]
        normalize nodelta
        [1,2,4: * #stmt_at_EQ * #nxt_spec |3: * [ * ] #stmt_at_EQ [ #nxt_spec ]]
        %{I}
        try (>nxt_spec % #ABS destruct(ABS) @False)
        lapply (in_map_domain … visited nxt)
        >req_vis
        [1,3,5,7: * #x #EQ >EQ % #ABS destruct(ABS)
        |2,4,6: @(proj1 … (labels_in_req (S n) (GOTO … nxt) …))
          whd in ⊢ (??%?); >nxt_spec %
        |8: @(proj1 … (proj2 … (labels_in_req n (FCOND … I a ltrue nxt) …)))
          whd in ⊢ (??%?); >stmt_at_EQ %
        ]
      | cases stmt in stmt_spec;
        [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ] normalize nodelta
        [1,2,4: * #EQ #_ |3: * [ * ] #EQ [ #_ ] |5: #EQ ]
        whd in match stmt_explicit_labels; normalize nodelta
        [ @(All_mp … (labels_in_req n (sequential … (COST_LABEL … cost) it) ?))
        | @(All_mp … (labels_in_req n (sequential … (CALL … f args dest) it) ?))
        | @(All_mp … (labels_in_req n (sequential … s it) ?))
        | @(All_mp … (labels_in_req n (sequential … (COND … a ltrue) it) ?))
        |6: @(All_mp … (labels_in_req n (final … s) ?))
        | cases (labels_in_req n (FCOND … I a ltrue nxt) ?)
          [ #l_req #_ %{I} lapply (in_map_domain … visited ltrue)
            >(req_vis … l_req) * #n #EQ' >EQ' % #ABS destruct(ABS) ]
        ]
        [1,3,5,7,9: #l #l_req >(lookup_eq_safe … (req_vis … l_req))
          % #ABS destruct(ABS)
        |*: whd in ⊢ (??%?); >EQ %
        ]
      ]
    | cases stmt in stmt_spec;
      [ * [ #cost | #f #args #dest | #a #ltrue | #s ] #nxt | #s | * ] normalize nodelta
      [1,2,4: * #EQ #H |3: * [ * ] #EQ [ #H ] |5: #EQ ]
      >stmt_at_filter_labels
      whd in match (stmt_at (mk_lin_params p) ?? n); >EQ normalize nodelta
      [1,2,3: % [1,3,5: %] cases H -H
        #H try (%1{H}) %2 >stmt_at_filter_labels whd in ⊢ (??%?); >H %
      | %1 %{H} %
      | %2 %
      | %
      ]
    ]
  ]
| #i #s
  >stmt_at_filter_labels #EQ
  %
  [ @stmt_forall_labels_explicit
    @(All_mp … (labels_in_req … EQ))
    #l #l_req >lin_code_has_label
    >occurs_exactly_once_filter_labels >l_req
    >commutative_andb whd in ⊢ (?%);
    elim (sigma_prop ?? (lookup_eq_safe … (req_vis … l_req)))
    >lin_code_has_label #H #_ @H
  | lapply EQ cases s [ #s' * | #s' #_ % | * #a #ltrue #lfalse #_ % ]
    -EQ #EQ change with (bool_to_Prop (code_has_point ????))
    whd in match (point_of_succ ???);
    >lin_code_has_point @leb_elim [ #_ % ] >length_map >length_reverse
    #INEQ
    cut (|generated| = S i)
    [ @(le_to_le_to_eq … (not_lt_to_le … INEQ) )
      whd in EQ : (??%?); inversion (nth_opt ???) in EQ;
      [2: #x ] #EQ1 whd in ⊢ (??%%→?); #EQ2 destruct
      <length_reverse
      @(nth_opt_hit_length … EQ1)
    ] #EQ_length
    elim last_fin * [ #fin | #a * #ltrue * #lfalse ] #EQ'
    lapply EQ whd in match (stmt_at ????);
    >nth_opt_reverse_hit >EQ_length [2,4: % ] <minus_n_n
    change with (stmt_at ???? = ? → ?)
    >EQ' #ABS destruct(ABS)
  ]
]
*)
qed.

definition linearise_int_fun :
  ∀p : uns_params.
  ∀globals.
    ∀fn_in : joint_closed_internal_function (mk_graph_params p) globals
     .Σfn_out_sigma :
      (joint_closed_internal_function (mk_lin_params p) globals × ?).
        good_local_sigma … (joint_if_code … fn_in) (joint_if_entry … fn_in)
          (joint_if_code … (\fst fn_out_sigma)) (\snd fn_out_sigma)
     (* ∃sigma : identifier_map LabelTag ℕ. 
        let g ≝ joint_if_code ?? (pi1 … fin) in
        let c ≝ joint_if_code ?? (pi1 … fout) in
        let entry ≝ joint_if_entry ?? (pi1 … fin) in
         lookup … sigma entry = Some ? 0 ∧
          ∀l,n.lookup … sigma l = Some ? n →
            ∃s. lookup … g l = Some ? s ∧
              opt_Exists ?
                (λls.let 〈lopt, ts〉 ≝ ls in
                  opt_All ? (eq ? l) lopt ∧
                  ts = graph_to_lin_statement … s ∧
                  opt_All ?
                    (λnext.Or (lookup … sigma next = Some ? (S n))
                    (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
                    (stmt_implicit_label … s)) (nth_opt … n c)*) ≝
  λp,globals,f_sig.
  let code_sigma ≝ linearise_code …
    (joint_if_code … f_sig)
    (code_is_closed … (pi2 … f_sig))
    (joint_if_entry … f_sig) in
  let code ≝ \fst code_sigma in
  let sigma ≝ \snd code_sigma in
  «〈«mk_joint_internal_function (mk_lin_params p) globals
   (joint_if_luniverse ?? f_sig) (joint_if_runiverse ?? f_sig)
   (joint_if_result ?? f_sig) (joint_if_params ?? f_sig)
   (joint_if_stacksize ?? f_sig) (joint_if_local_stacksize ?? f_sig)
   code 0 (* exit is dummy! *), hide_prf ??»,
   sigma〉, proj1 ?? (pi2 ?? code_sigma)».
cases daemon (*)
[2: whd in match code; cases code_sigma -code_sigma * #code #sigma
  normalize nodelta *** #H3 #H4 #H5
   elim (H5 … H3)
  #s ** #_ #_ >lin_code_has_point cases code
  [ cases s [ * [ #cost | #f #args #dest | #a #ltrue | #s' ] #nxt | #s' | * ]
    [1,2,4: * #EQnth_opt #_ |3: * [ * ] #EQnth_opt [ #_ ] |5: #EQnth_opt ]
    normalize in EQnth_opt; destruct(EQnth_opt)
  | #hd #tl #_ #_ %
  ]
| @hide_prf %
  (* TODO *)
  [ cases daemon
  | cases daemon
  | @(proj2 ?? (pi2 ?? code_sigma))
  | cases daemon
  | (* We need to add this to graph_visit_ret_type as an invariant.
       To prove the invariant at each step in graph_visit we will exploit
       (regs_are_in_univers … (pi2 … f_sig))
       More generally, to close all the daemons here we need to strengthen
       the invariant of graph_visit_ret_type so that the partial code
       emitted is also good_if at each step *)
    cases daemon
  ]
]
*)
qed.

definition linearise : ∀p : uns_params.
  program (joint_function (mk_graph_params p)) ℕ →
  program (joint_function (mk_lin_params p)) ℕ
   ≝
  λp,pr.transform_program ??? pr
    (λglobals.transf_fundef ?? (λf_in.\fst (linearise_int_fun p globals f_in))).

(*
definition good_sigma :
  ∀p:uns_params.
  ∀prog_in : joint_program (mk_graph_params p).
  ((Σi.is_internal_function_of_program … prog_in i) → label → option ℕ) → Prop ≝
  λp,prog_in,sigma.
  let prog_out ≝ linearise … prog_in in
  ∀i : Σi.is_internal_function_of_program … prog_in i.∀prf.
  let fn_in ≝ if_of_function … i in
  let i' : Σi.is_internal_function_of_program … prog_out i ≝ «pi1 ?? i, prf» in
  let fn_out ≝ if_of_function … i' in
  let sigma_local ≝ sigma i in
  good_local_sigma ?? (joint_if_code ?? fn_in) (joint_if_entry … fn_in)
          (joint_if_code ?? fn_out) sigma_local.

lemma linearise_spec : ∀p,prog.∃sigma.good_sigma p prog sigma.
#p #prog
letin sigma ≝ 
  (λi : Σi.is_internal_function_of_program … prog i.    let fn_in ≝ if_of_function … i in
    \snd (linearise_int_fun … fn_in))
%{sigma}
#i #prf >(prog_if_of_function_transform … i) [2: % ]
normalize nodelta
cases (linearise_int_fun ???) * #fn_out #sigma_loc
normalize nodelta #prf @prf
qed.
*)