Ignore:
Timestamp:
Apr 6, 2012, 8:02:10 PM (8 years ago)
Author:
tranquil
Message:

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils_paolo.ma

    r1643 r1882  
    55(* type T is the syntactic type of the generated things *)
    66(* (sig for RTLabs registers, unit in others ) *)
    7 definition freshT ≝ λg.λpars : params.λX,T : Type[0].
    8    T → state_monad (joint_internal_function … g pars) X.
     7definition freshT ≝ λg.λpars : params.state_monad (joint_internal_function … g pars).
    98
    109definition rtl_ertl_fresh_reg:
    1110 ∀inst_pars,funct_pars,globals.
    12   freshT globals (rtl_ertl_params inst_pars funct_pars) register unit
    13   λinst_pars,var_pars,globals,it,def.
     11  freshT globals (rtl_ertl_params inst_pars funct_pars) register
     12  λinst_pars,var_pars,globals,def.
    1413    let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
    1514    〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.
    1615
     16include alias "basics/lists/list.ma".
    1717let rec rtl_ertl_fresh_regs inst_pars funct_pars globals (n : ℕ) on n :
    18   freshT globals (rtl_ertl_params inst_pars funct_pars) (list register) unit ≝
    19   match n with
    20   [ O ⇒ λ_. return [ ]
    21   | S n' ⇒ λ_.
    22     ! regs' ← rtl_ertl_fresh_regs inst_pars funct_pars globals n' it;
    23     ! reg ← rtl_ertl_fresh_reg inst_pars funct_pars globals it;
    24     return (reg :: regs')
    25   ].
    26 
    27 lemma rtl_ertl_fresh_regs_length:
    28  ∀i_pars,f_pars,globals.∀def: joint_internal_function … globals
    29   (rtl_ertl_params i_pars f_pars). ∀n: nat.
    30   |(\snd (rtl_ertl_fresh_regs … n it def))| = n.
    31  #ipars#fpars #globals #def #n elim n
    32   [ %
    33   | #m whd in ⊢ (? → ??(??(???%))?); @pair_elim
    34     #def' #regs #EQ>EQ
    35     whd in ⊢ (? → ??(??(???%))?); @pair_elim #def'' #reg #_ normalize // ]
    36 qed.
    37 
    38 definition rtl_ertl_fresh_regs_strong:
    39  ∀i_pars,f_pars,globals. joint_internal_function … globals (rtl_ertl_params i_pars f_pars) →
    40   ∀n: nat. Σregs: (joint_internal_function … globals (rtl_ertl_params i_pars f_pars)) × (list register). |\snd regs| = n ≝
    41  λi_pars,f_pars,globals,def,n.rtl_ertl_fresh_regs i_pars f_pars globals n it def. //
    42 qed.
     18  freshT globals (rtl_ertl_params inst_pars funct_pars)
     19    (Σl : list register. |l| = n) ≝
     20  let ret_type ≝ (Σl : list register. |l| = n) in
     21  match n  return λx.x = n → freshT … ret_type with
     22  [ O ⇒ λeq'.return (mk_Sig … [ ] ?)
     23  | S n' ⇒ λeq'.
     24    ! regs' ← rtl_ertl_fresh_regs inst_pars funct_pars globals n';
     25    ! reg ← rtl_ertl_fresh_reg inst_pars funct_pars globals;
     26    return (mk_Sig … (reg :: regs') ?)
     27  ](refl …). <eq' normalize [//] elim regs' #l #eql >eql //
     28  qed.
    4329
    4430definition fresh_label:
    45  ∀g_pars,globals.freshT globals g_pars label unit
    46   λg_pars,globals,it,def.
     31 ∀g_pars,globals.freshT globals g_pars label
     32  λg_pars,globals,def.
    4733    let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in
    4834     〈set_luniverse … def luniverse, r〉.
     
    5238  (g_pars: graph_params)
    5339  (globals: list ident)
    54   (insts: list (joint_instruction g_pars globals))
     40  (insts: list (joint_step g_pars globals))
    5541  (src : label)
    5642  (dest : label)
     
    6349      add_graph … src (sequential … instr dest) def
    6450    | _ ⇒ (* need to generate label *)
    65       let 〈def, tmp_lbl〉 ≝ fresh_label … it def in
     51      let 〈def, tmp_lbl〉 ≝ fresh_label … def in
    6652      adds_graph g_pars globals others tmp_lbl dest
    6753        (add_graph … src (sequential … instr tmp_lbl) def)
     
    7258  ∀g_pars: graph_params.
    7359  ∀globals: list ident.
    74   (* type of allocatable registers and of their types (unit if not in RTLabs) *)
    75   ∀R,T : Type[0].
    7660  (* fresh register creation *)
    77   freshT globals g_pars R T
    78   ∀insts: bind_list R T (joint_instruction g_pars globals).
     61  freshT globals g_pars (localsT … g_pars)
     62  ∀insts: bind_list (localsT … g_pars) (joint_step g_pars globals).
    7963  ∀src : label.
    8064  ∀dest : label.
    8165  joint_internal_function globals g_pars →
    8266  joint_internal_function globals g_pars ≝
    83   λg_pars,globals,T,R,fresh_r,insts,src,dest,def.
     67  λg_pars,globals,fresh_r,insts,src,dest,def.
    8468  let 〈def', stmts〉 ≝ bcompile … fresh_r insts def in
    8569  adds_graph … stmts src dest def'.
     
    8973  ∀src_g_pars,dst_g_pars : graph_params.
    9074  ∀globals: list ident.
    91   (* type of allocatable registers (unit if not in RTLabs) *)
    92   ∀T : Type[0].
    9375  (* fresh register creation *)
    94   freshT globals dst_g_pars (localsT dst_g_pars) T
     76  freshT globals dst_g_pars (localsT dst_g_pars)
    9577  (* function dictating the translation *)
    96   (label → joint_instruction src_g_pars globals →
    97     bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals)
     78  (label → joint_step src_g_pars globals →
     79    bind_list (localsT dst_g_pars) (joint_step dst_g_pars globals)
    9880    (* this can be added to allow redirections: × label *)) →
    99   (label → ext_fin_instruction src_g_pars →
    100     (bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals))
    101     ×
    102     (joint_statement dst_g_pars globals)) →
     81  (label → ext_fin_stmt src_g_pars →
     82     bind_new (localsT dst_g_pars)
     83      ((list (joint_step dst_g_pars globals))
     84      ×
     85      (joint_statement dst_g_pars globals))) →
    10386  (* initialized function definition with empty graph *)
    10487  joint_internal_function globals dst_g_pars →
     
    10790  (* destination function *)
    10891  joint_internal_function globals dst_g_pars ≝
    109   λsrc_g_pars,dst_g_pars,globals,registerT,fresh_reg,trans,trans',empty,def.
     92  λsrc_g_pars,dst_g_pars,globals,fresh_reg,trans,trans',empty,def.
    11093  let f : label → joint_statement (src_g_pars : params) globals →
    11194    joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝
     
    11598    | GOTO next ⇒ add_graph … lbl (GOTO … next) def
    11699    | RETURN ⇒ add_graph … lbl (RETURN …) def
    117     | extension_fin c ⇒ let 〈l, fin〉 ≝ trans' lbl c in
    118       let 〈def, tmp_lbl〉 ≝ fresh_label … it def in
    119       b_adds_graph … fresh_reg l lbl tmp_lbl (add_graph … tmp_lbl fin def)
     100    | extension_fin c ⇒
     101      let 〈def', p〉 ≝ bcompile … fresh_reg (trans' lbl c) def in
     102      let 〈insts, fin〉 ≝ p in
     103      let 〈def'', tmp_lbl〉 ≝ fresh_label … def' in
     104      adds_graph … insts lbl tmp_lbl (add_graph … tmp_lbl fin def)
    120105    ] in
    121106  foldi … f (joint_if_code … def) empty.
    122 
    123 definition b_graph_translate_no_fin :
    124   ∀src_g_pars : graph_params.
    125   ext_fin_instruction src_g_pars = void →
    126   ∀dst_g_pars : graph_params.
    127   ∀globals: list ident.
    128   (* type of allocatable registers (unit if not in RTLabs) *)
    129   ∀T : Type[0].
    130   (* fresh register creation *)
    131   freshT globals dst_g_pars (localsT dst_g_pars) T →
    132   (* function dictating the translation *)
    133   (label → joint_instruction src_g_pars globals →
    134     bind_list (localsT dst_g_pars) T (joint_instruction dst_g_pars globals)
    135     (* this can be added to allow redirections: × label *)) →
    136   (* initialized function definition with empty graph *)
    137   joint_internal_function globals dst_g_pars →
    138   (* source function *)
    139   joint_internal_function globals src_g_pars →
    140   (* destination function *)
    141   joint_internal_function globals dst_g_pars ≝
    142   λsrc_g_pars,src_g_pars_prf,dst_g_pars,globals,registerT,fresh_reg,trans.
    143     b_graph_translate src_g_pars dst_g_pars globals registerT fresh_reg
    144       trans (λ_.λc.⊥). >src_g_pars_prf in c; #H elim H qed.
    145107 
    146108(* translation without register allocation *)
     
    149111  ∀globals: list ident.
    150112  (* function dictating the translation *)
    151   (label → joint_instruction src_g_pars globals →
    152     list (joint_instruction dst_g_pars globals)) →
    153   (label → ext_fin_instruction src_g_pars →
    154     (list (joint_instruction dst_g_pars globals))
     113  (label → joint_step src_g_pars globals →
     114    list (joint_step dst_g_pars globals)) →
     115  (label → ext_fin_stmt src_g_pars →
     116    (list (joint_step dst_g_pars globals))
    155117    ×
    156118    (joint_statement dst_g_pars globals)) →
     
    171133    | RETURN ⇒ add_graph … lbl (RETURN …) def
    172134    | extension_fin c ⇒ let 〈l, fin〉 ≝ trans' lbl c in
    173       let 〈def, tmp_lbl〉 ≝ fresh_label … it def in
     135      let 〈def, tmp_lbl〉 ≝ fresh_label … def in
    174136      adds_graph … l lbl tmp_lbl (add_graph … tmp_lbl fin def)
    175137    ] in
    176138  foldi ??? f (joint_if_code ?? def) empty.
     139
     140definition graph_to_lin_statement :
     141  ∀p : unserialized_params.∀globals.
     142  joint_statement (mk_graph_params p) globals → joint_statement (mk_lin_params p) globals ≝
     143  λp,globals,stmt.match stmt return λ_.joint_statement (mk_lin_params p) globals with
     144  [ sequential c _ ⇒ sequential … c it
     145  | GOTO l ⇒ GOTO … l
     146  | RETURN ⇒ RETURN …
     147  | extension_fin c ⇒ extension_fin … c
     148  ].
     149
     150lemma graph_to_lin_labels :
     151  ∀p : unserialized_params.∀globals,s.
     152  stmt_labels … (graph_to_lin_statement p globals s) =
     153  stmt_explicit_labels … s.
     154#p#globals * //
     155qed.
     156
     157(* in order to make the coercion from lists to sets to work, one needs these hints *)
     158unification hint 0 ≔ ;
     159X ≟ identifier LabelTag
     160
     161list label ≡ list X.
     162
     163unification hint 0 ≔ ;
     164X ≟ identifier RegisterTag
     165
     166list register ≡ list X.
     167
     168   
     169definition hide_prf : ∀P : Prop.P → P ≝ λP,prf.prf.
     170definition hide_Prop : Prop → Prop ≝ λP.P.
     171
     172interpretation "hide proof" 'hide p = (hide_prf ? p).
     173interpretation "hide Prop" 'hide p = (hide_Prop p).
     174
     175(* discard all elements failing test, return first element succeeding it *)
     176(* and the rest of the list, if any. *)
     177let rec chop A (test : A → bool) (l : list A) on l : option (A × (list A)) ≝
     178  match l with
     179  [ nil ⇒ None ?
     180  | cons x l' ⇒ if test x then return 〈x, l'〉 else chop A test l'
     181  ].
     182
     183lemma chop_hit : ∀A,f,l,pr. chop A f l = Some ? pr →
     184  let x ≝ \fst pr in
     185  let post ≝ \snd pr in
     186  ∃pre.All ? (λx.Not (bool_to_Prop (f x))) pre ∧ l = pre @ x :: post ∧ bool_to_Prop (f x).
     187#A#f#l elim l
     188[ normalize * #x #post #EQ destruct
     189| #y #l' #Hi * #x #post
     190  normalize elim (true_or_false_Prop (f y)) #fy >fy normalize
     191  #EQ
     192  [ destruct >fy %{[ ]} /3 by refl, conj, I/
     193  | elim (Hi … EQ) #pre ** #prefalse #chopd #fx
     194    %{(y :: pre)} %[%[%{fy prefalse}| >chopd %]|@fx]
     195  ]
     196]
     197qed.
     198
     199lemma chop_miss : ∀A,f,l. chop A f l = None ? → All A (λx.Not (bool_to_Prop (f x))) l.
     200#A#f#l elim l
     201[ normalize #_ %
     202| #y #l' #Hi normalize
     203  elim (true_or_false_Prop (f y)) #fy >fy normalize
     204  #EQ
     205  [ destruct
     206  | /3 by conj, nmk/
     207  ]
     208]
     209qed.
     210
     211unification hint 0 ≔ p, globals;
     212lp ≟ lin_params_to_params p,
     213sp ≟ stmt_pars lp,
     214js ≟ joint_statement sp globals,
     215lo ≟ labelled_obj LabelTag js
     216(*----------------------------*)⊢
     217list lo ≡ codeT lp globals.
     218
     219definition graph_visit_ret_type ≝ λp,globals.λg : codeT (mk_graph_params p) globals.
     220  λentry : label.
     221  (Σ〈visited'   : identifier_map LabelTag ℕ,
     222   required'  : identifier_set LabelTag,
     223   generated' : codeT (mk_lin_params p) globals〉.'hide (
     224      And (And (And (lookup ?? visited' entry = Some ? 0) (required' ⊆ visited'))
     225        (code_forall_labels … (λl.bool_to_Prop (l∈required')) generated'))
     226        (∀l,n.lookup ?? visited' l = Some ? n →
     227          And (code_has_label … (rev ? generated') l)
     228            (∃s.And (And
     229              (lookup … g l = Some ? s)
     230              (nth_opt … n (rev … generated') = Some ? 〈Some ? l, graph_to_lin_statement … s〉))
     231              (opt_All ?
     232                (λnext.Or (lookup … visited' next = Some ? (S n))
     233                  (nth_opt … (S n) (rev … generated') = Some ? 〈None ?, GOTO … next〉))
     234                (stmt_implicit_label … s)))))).
     235               
     236unification hint 0 ≔ tag ⊢ identifier_set tag ≡ identifier_map tag unit.
     237
     238let rec graph_visit
     239  (p : unserialized_params)
     240  (globals: list ident)
     241  (g : codeT (mk_graph_params p) globals)
     242  (* = graph (joint_statement (mk_graph_params p) globals *)
     243  (required: identifier_set LabelTag)
     244  (visited: identifier_map LabelTag ℕ) (* the reversed index of labels in the new code *)
     245  (generated: codeT (mk_lin_params p) globals)
     246  (* ≝ list ((option label)×(joint_statement (mk_lin_params p) globals)) *)
     247  (visiting: list label)
     248  (gen_length : ℕ)
     249  (n: nat)
     250  (entry : label)
     251  (g_prf : code_closed … g)
     252  (required_prf1 : ∀i.i∈required → Or (In ? visiting i) (bool_to_Prop (i ∈ visited)))
     253  (required_prf2 : code_forall_labels … (λl.bool_to_Prop (l ∈ required)) generated)
     254  (generated_prf1 : ∀l,n.lookup … visited l = Some ? n → hide_Prop (
     255    And (code_has_label … (rev ? generated) l)
     256    (∃s.And (And
     257      (lookup … g l = Some ? s)
     258      (nth_opt ? n (rev … generated) = Some ? 〈Some ? l, graph_to_lin_statement … s〉))
     259      (opt_All ? (λnext.match lookup … visited next with
     260                     [ Some n' ⇒ Or (n' = S n) (nth_opt ? (S n) (rev ? generated) = Some ? 〈None ?, GOTO … next〉)
     261                     | None ⇒ And (nth_opt ? 0 visiting = Some ? next) (S n = gen_length) ]) (stmt_implicit_label … s)))))
     262  (generated_prf2 : ∀l.lookup … visited l = None ? → does_not_occur … l (rev ? generated))
     263  (visiting_prf : All … (λl.lookup … g l ≠ None ?) visiting)
     264  (gen_length_prf : gen_length = length ? generated)
     265  (entry_prf : Or (And (And (visiting = [entry]) (gen_length = 0)) (Not (bool_to_Prop (entry∈visited))))
     266                  (lookup … visited entry = Some ? 0))
     267  (n_prf : le (id_map_size … g) (plus n (id_map_size … visited)))
     268  on n
     269  : graph_visit_ret_type … g entry ≝
     270  match chop ? (λx.¬x∈visited) visiting
     271  return λx.chop ? (λx.¬x∈visited) visiting = x → graph_visit_ret_type … g entry with
     272  [ None ⇒ λeq_chop.
     273    let H ≝ chop_miss … eq_chop in
     274    mk_Sig … 〈visited, required, generated〉 ?
     275  | Some pr ⇒ λeq_chop.
     276    let vis_hd ≝ \fst pr in
     277    let vis_tl ≝ \snd pr in
     278    let H ≝ chop_hit ???? eq_chop in
     279    match n return λx.x = n → graph_visit_ret_type … g entry with
     280    [ O ⇒ λeq_n.⊥
     281    | S n' ⇒ λeq_n.
     282      (* add the label to the visited ones *)
     283      let visited' ≝ add … visited vis_hd gen_length in
     284      (* take l's statement *)
     285      let statement ≝ opt_safe … (lookup ?? g vis_hd) (hide_prf ? ?) in 
     286      (* translate it to its linear version *)
     287      let translated_statement ≝ graph_to_lin_statement p globals statement in
     288      (* add the translated statement to the code (which will be reversed later) *)
     289      let generated' ≝ 〈Some … vis_hd, translated_statement〉 :: generated in
     290      let required' ≝ stmt_explicit_labels … statement ∪ required in
     291      (* put successors in the visiting worklist *)
     292      let visiting' ≝ stmt_labels … statement @ vis_tl in
     293      (* finally, check the implicit successor *)
     294      (* if it has been already visited, we need to add a GOTO *)
     295      let add_req_gen ≝ match stmt_implicit_label … statement with
     296        [ Some next ⇒
     297          if next ∈ visited' then 〈1, {(next)}, [〈None label, GOTO … next〉]〉 else 〈0, ∅, [ ]〉
     298        | None ⇒ 〈0, ∅, [ ]〉
     299        ] in
     300      graph_visit ???
     301        (\snd (\fst add_req_gen) ∪ required')
     302        visited'
     303        (\snd add_req_gen @ generated')
     304        visiting'
     305        (\fst (\fst add_req_gen) + S(gen_length))
     306        n' entry g_prf ????????
     307    ] (refl …)
     308  ] (refl …).
     309whd
     310[ (* base case, visiting is all visited *)
     311  %[
     312    %[
     313      %[
     314        elim entry_prf
     315        [ ** #eq_visiting #gen_length_O #entry_vis >eq_visiting in H; * >entry_vis
     316          * #ABS elim (ABS I)
     317        | //
     318        ]
     319      | #l #l_req
     320        elim (required_prf1 … l_req) #G
     321        [ lapply (All_In … H G) #H >(notb_false ? H) %
     322        | assumption
     323        ]
     324      ]
     325    | assumption
     326    ]
     327   | #l #n #H elim (generated_prf1 … H)
     328      #H1 * #s ** #H2 #H3 #H4
     329      % [assumption] %{s} %
     330      [% assumption
     331      | @(opt_All_mp … H4) -l #l
     332        lapply (in_map_domain … visited l)
     333        elim (true_or_false (l∈visited)) #l_vis >l_vis
     334        normalize nodelta [ * #n' ] #EQlookup >EQlookup
     335        normalize nodelta *
     336        [ #EQn' % >EQn' %
     337        | #H %2{H}
     338        | #H' lapply (All_nth … H … H') >l_vis * #ABS elim (ABS I)
     339        ]
     340      ]
     341    ]
     342|*: (* unpack H in all other cases *) elim H #pre ** #H1 #H2 #H3 ]
     343(* first, close goals where add_gen_req plays no role *)
     344[10: (* vis_hd is in g *) @(All_split … visiting_prf … H2)
     345|1: (* n = 0 absrud *)
     346  @(absurd … n_prf)
     347  @lt_to_not_le
     348  <eq_n
     349  lapply (add_size … visited vis_hd 0 (* dummy value *))
     350  >(notb_true … H3)
     351  whd in match (if ? then ? else ?);
     352  whd in match (? + ?);
     353  whd in match (lt ? ?);
     354  #EQ <EQ @subset_card @add_subset
     355  [ @(All_split ? (λx.bool_to_Prop (x∈g)) ????? H2) @(All_mp … visiting_prf)
     356    #a elim g #gm whd in ⊢ (?→?%); #H >(opt_to_opt_safe … H) %
     357  | #l #H lapply (mem_map_domain … H) -H #H lapply(opt_to_opt_safe … H)
     358    generalize in match (opt_safe ???); #n #l_is_n
     359    elim (generated_prf1 … l_is_n) #_ * #s ** #s_in_g #_ #_ lapply s_in_g -s_in_g
     360    elim g #mg  whd in ⊢ (?→?%); #H >H whd %
     361  ]
     362|6:
     363  @All_append
     364  [ @(g_prf … vis_hd) <opt_to_opt_safe %
     365  | >H2 in visiting_prf;
     366    #H' lapply (All_append_r … H') -H' * #_ //
     367  ]
     368|8:
     369  %2 elim entry_prf
     370  [ ** >H2 cases pre
     371    [2: #x' #pre' #ABS normalize in ABS; destruct(ABS)
     372      cases pre' in e0; [2: #x'' #pre''] #ABS' normalize in ABS'; destruct(ABS')
     373    |1: #EQ normalize in EQ; destruct(EQ) #eq_gen_length #_
     374      >lookup_add_hit >eq_gen_length %
     375    ]
     376  | #lookup_entry cut (entry ≠ vis_hd)
     377    [ % whd in match vis_hd; #entry_vis_hd <entry_vis_hd in H3; #entry_vis
     378      lapply (in_map_domain … visited entry) >(notb_true … entry_vis)
     379      normalize nodelta >lookup_entry #ABS destruct(ABS)]
     380    #entry_not_vis_hd >(lookup_add_miss ?????? entry_not_vis_hd) assumption
     381  ]
     382|9:
     383  >commutative_plus
     384  >add_size >(notb_true … H3) normalize nodelta
     385  whd in match (? + ?);
     386  >commutative_plus
     387  change with (? ≤ S(?) + ?)
     388  >eq_n assumption
     389|*: (* where add_gen_req does matter, expand the three possible cases *)
     390  lapply (refl … add_req_gen)
     391  whd in ⊢ (???%→?);
     392  lapply (refl … (stmt_implicit_label … statement))
     393  (* BUG *)
     394  [ generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
     395  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
     396  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
     397  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
     398  | generalize in match (stmt_implicit_label … statement) in ⊢ (???%→%);
     399  ]
     400  *[2,4,6,8,10: #next]
     401  #EQimpl
     402  whd in ⊢ (???%→?);
     403  [1,2,3,4,5: elim (true_or_false_Prop … (next∈visited')) #next_vis >next_vis
     404    whd in ⊢ (???%→?);]
     405  #EQ_req_gen >EQ_req_gen
     406  (* these are the cases, reordering them *)
     407  [1,2,11: | 3,4,12: | 5,6,13: | 7,8,14: |9,10,15: ]
     408  [1,2,3: #i >mem_set_union
     409    [ #H elim (orb_Prop_true … H) -H
     410      [ #H >(mem_set_singl_to_eq … H) %2{next_vis}]
     411    |*: >mem_set_empty whd in match (false ∨ ?);
     412    ]
     413    >mem_set_union
     414    #H elim(orb_Prop_true … H) -H
     415    [1,3,5: (* i is an explicit successor *)
     416      #i_succ
     417      (* if it's visited it's ok *)
     418      elim(true_or_false_Prop (i ∈visited')) #i_vis >i_vis
     419      [1,3,5: %2 %
     420      |*: %
     421        @Exists_append_l
     422        whd in match (stmt_labels ???);
     423        @Exists_append_r
     424        @mem_list_as_set
     425        @i_succ
     426      ]
     427    |2,4,6: (* i was already required *)
     428      #i_req
     429      elim (required_prf1 … i_req)
     430      [1,3,5: >H2 #H elim (Exists_append … H) -H
     431        [1,3,5: (* i in preamble → i∈visited *)
     432          #i_pre %2 >mem_set_add @orb_Prop_r
     433          lapply (All_In … H1 i_pre)
     434          #H >(notb_false … H) %
     435        |*: *
     436          [1,3,5: (* i is vis_hd *)
     437            #eq_i >eq_i %2 @mem_set_add_id
     438          |*: (* i in vis_tl → i∈visiting' *)
     439            #i_post % @Exists_append_r assumption
     440          ]
     441        ]
     442      |*: #i_vis %2 >mem_set_add @orb_Prop_r assumption
     443      ]
     444    ]
     445  |4,5,6:
     446    [% [ whd % [ >mem_set_union >mem_set_add_id % | %]]]
     447    whd in match (? @ ?); %
     448    [1,3,5:
     449      whd
     450      >graph_to_lin_labels
     451      change with (All ?? (stmt_explicit_labels ?? statement))
     452      whd in match required';
     453      generalize in match (stmt_explicit_labels … statement);
     454      #l @list_as_set_All
     455      #i >mem_set_union >mem_set_union
     456      #i_l @orb_Prop_r @orb_Prop_l @i_l
     457    |*: @(All_mp … required_prf2)
     458      * #l_opt #s @All_mp
     459      #l #l_req >mem_set_union @orb_Prop_r
     460      >mem_set_union @orb_Prop_r @l_req
     461    ]
     462  |7,8,9:
     463    #i whd in match visited';
     464    @(eq_identifier_elim … i vis_hd)
     465    [1,3,5: #EQi >EQi #pos
     466      >lookup_add_hit #EQpos cut (gen_length = pos)
     467        [1,3,5: (* BUG: -graph_visit *) -visited destruct(EQpos) %]
     468        -EQpos #EQpos <EQpos -pos
     469      %
     470      [1,3,5: whd in match (rev ? ?);
     471        >rev_append_def
     472        whd
     473        [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
     474          <associative_append >occurs_exactly_once_None]
     475        >occurs_exactly_once_Some_eq >eq_identifier_refl
     476        normalize nodelta
     477        @generated_prf2
     478        lapply (in_map_domain … visited vis_hd)
     479        >(notb_true … H3) normalize nodelta //
     480      |*: %{statement}
     481        %
     482        [1,3,5: %
     483          [1,3,5:
     484           change with (? = Some ? (opt_safe ???))
     485           @opt_safe_elim #s //
     486          |*: whd in match (rev ? ?);
     487            >rev_append_def
     488            [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
     489              <associative_append @nth_opt_append_hit_l ]
     490            >nth_opt_append_r
     491            >rev_length
     492            <gen_length_prf
     493            [1,3,5: <minus_n_n] %
     494          ]
     495        |*: >EQimpl whd [3: %]
     496          >mem_set_add in next_vis;
     497          @eq_identifier_elim
     498          [1,3: #EQnext >EQnext * [2: #ABS elim(ABS I)]
     499            >lookup_add_hit
     500          |*: #NEQ >(lookup_add_miss … visited … NEQ)
     501            whd in match (false ∨ ?);
     502            #next_vis lapply(in_map_domain … visited next) >next_vis
     503            whd in ⊢ (% → ?); [ * #s ]
     504            #EQlookup >EQlookup
     505          ] whd
     506          [1,2: %2
     507            >rev_append >nth_opt_append_r
     508            >rev_length whd in match generated';
     509            whd in match (|? :: ?|); <gen_length_prf
     510            [1,3: <minus_n_n ] %
     511          |*: % [2: %] @nth_opt_append_hit_l whd in match (stmt_labels … statement);
     512            >EQimpl %
     513          ]
     514        ]
     515      ]
     516    |*:
     517      #NEQ #n_i >(lookup_add_miss … visited … NEQ)
     518      #Hlookup elim (generated_prf1 … Hlookup)
     519      #G1 * #s ** #G2 #G3 #G4
     520      %
     521      [1,3,5: whd in match (rev ??);
     522        >rev_append_def whd
     523        [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
     524          <associative_append >occurs_exactly_once_None]
     525        >occurs_exactly_once_Some_eq
     526        >eq_identifier_false
     527        [2,4,6: % #ABS >ABS in NEQ; * #ABS' @ABS' %]
     528        normalize nodelta
     529        assumption
     530      |*: %{s}
     531        %
     532        [1,3,5: %
     533          [1,3,5: assumption
     534          |*: whd in match (rev ??); >rev_append_def
     535            [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
     536              <associative_append @nth_opt_append_hit_l ]
     537            @nth_opt_append_hit_l assumption
     538          ]
     539        |*: @(opt_All_mp … G4)
     540          #x
     541          @(eq_identifier_elim … x vis_hd) #Heq
     542          [1,3,5: >Heq
     543            lapply (in_map_domain … visited vis_hd)
     544            >(notb_true … H3)
     545           normalize nodelta #EQlookup >EQlookup normalize nodelta
     546           * #nth_opt_visiting #gen_length_eq
     547           >lookup_add_hit normalize nodelta %
     548           >gen_length_eq %
     549          |*: >(lookup_add_miss ?????? Heq)
     550            lapply (in_map_domain … visited x)
     551            elim (true_or_false_Prop (x∈visited)) #x_vis >x_vis normalize nodelta
     552            [1,3,5: * #n'] #EQlookupx >EQlookupx normalize nodelta *
     553            [1,3,5: #G %{G}
     554            |2,4,6: #G %2 whd in match (rev ??); >rev_append_def
     555              [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
     556              <associative_append @nth_opt_append_hit_l ]
     557              @nth_opt_append_hit_l assumption
     558            |*: #G elim(absurd ?? Heq)
     559              (* BUG (but useless): -required -g -generated *)
     560               >H2 in G; #G
     561              lapply (refl … (nth_opt ? 0 pre))
     562              (* BUG *)
     563              [generalize in ⊢ (???%→?);
     564              |generalize in ⊢ (???%→?);
     565              |generalize in ⊢ (???%→?);
     566              ] *
     567              [1,3,5: #G' >(nth_opt_append_miss_l … G') in G;
     568                change with (Some ? vis_hd = ? → ?)
     569                #EQvis_hd' destruct(EQvis_hd') %
     570              |*: #lbl'' #G' >(nth_opt_append_hit_l ? pre ??? G') in G;
     571                #EQlbl'' destruct(EQlbl'') lapply (All_nth … H1 … G')
     572                >x_vis * #ABS elim (ABS I)
     573              ]
     574            ]
     575          ]
     576        ]
     577      ]
     578    ]
     579  |10,11,12:
     580    #i whd in match visited';
     581    lapply (in_map_domain … visited' i)
     582    >mem_set_add
     583    elim (true_or_false_Prop (eq_identifier … vis_hd i)) #i_vis_hd
     584    >eq_identifier_sym >i_vis_hd
     585    [2,4,6: elim(true_or_false (i∈visited)) #i_vis >i_vis]
     586    [1,3,5,7,8,9: change with ((∃_.?) → ?); * #n #EQlook >EQlook #ABS destruct(ABS)]
     587    #_ #EQlookup >lookup_add_miss in EQlookup;
     588    [2,4,6: % #ABS >ABS in i_vis_hd; >eq_identifier_refl *]
     589    #EQlookup
     590    [1,2,3: @EQlookup %]
     591    whd in match (rev ??); >rev_append_def
     592    [ change with (? @ ([?] @ [?])) in match (? @ [? ; ?]);
     593              <associative_append >does_not_occur_None]
     594    >(does_not_occur_Some ?????? (i_vis_hd))
     595    @generated_prf2 assumption
     596  |13,14,15:
     597    whd in match generated'; normalize <gen_length_prf %
     598  ]
     599]
     600qed.
     601
     602(* CSC: The branch compression (aka tunneling) optimization is not implemented
     603   in Matita *)
     604definition branch_compress
     605  ≝ λp: graph_params.λglobals.λg:codeT p globals.
     606    λentry : Σl.code_has_label … g l.g.
    177607 
    178 definition graph_translate_no_fin :
    179   ∀src_g_pars : graph_params.
    180   ext_fin_instruction src_g_pars = void →
    181   ∀dst_g_pars : graph_params.
    182   ∀globals: list ident.
    183   (* type of allocatable registers (unit if not in RTLabs) *)
    184   (* function dictating the translation *)
    185   (label → joint_instruction src_g_pars globals →
    186     list (joint_instruction dst_g_pars globals)
    187     (* this can be added to allow redirections: × label *)) →
    188   (* initialized function definition with empty graph *)
    189   joint_internal_function globals dst_g_pars →
    190   (* source function *)
    191   joint_internal_function globals src_g_pars →
    192   (* destination function *)
    193   joint_internal_function globals dst_g_pars ≝
    194   λsrc_g_pars,src_g_pars_prf,dst_g_pars,globals,trans.
    195     graph_translate src_g_pars dst_g_pars globals
    196       trans (λ_.λc.⊥). >src_g_pars_prf in c; #H elim H qed.
     608lemma branch_compress_closed : ∀p,globals,g,l.code_closed ?? g →
     609  code_closed … (branch_compress p globals g l).
     610#p#globals#g#l#H @H qed.
     611
     612lemma branch_compress_has_entry : ∀p,globals,g,l.
     613  code_has_label … (branch_compress p globals g l) l.
     614#p#globals#g*#l#l_prf @l_prf qed.
     615
     616definition filter_labels ≝ λtag,A.λtest : identifier tag → bool.λc : list (labelled_obj tag A).
     617  map ??
     618    (λs. let 〈l_opt,x〉 ≝ s in
     619      〈! l ← l_opt ; if test l then return l else None ?, x〉) c.
     620     
     621lemma does_not_occur_filter_labels :
     622  ∀tag,A,test,id,c.
     623    does_not_occur ?? id (filter_labels tag A test c) =
     624      (does_not_occur ?? id c ∨ ¬ test id).
     625#tag #A #test #id #c elim c
     626[ //
     627| ** [2: #lbl] #s #tl #IH
     628  whd in match (filter_labels ????); normalize nodelta
     629  whd in match (does_not_occur ????) in ⊢ (??%%);
     630  [2: @IH]
     631  normalize in match (! l ← ? ; ?); >IH
     632  @(eq_identifier_elim ?? lbl id) #Heq [<Heq]
     633  elim (test lbl) normalize nodelta
     634  change with (eq_identifier ???) in match (instruction_matches_identifier ????);
     635  [1,2: >eq_identifier_refl [2: >commutative_orb] normalize %
     636  |*: >(eq_identifier_false ??? Heq) normalize nodelta %
     637  ]
     638]
     639qed.
     640
     641lemma occurs_exactly_once_filter_labels :
     642  ∀tag,A,test,id,c.
     643    occurs_exactly_once ?? id (filter_labels tag A test c) =
     644      (occurs_exactly_once ?? id c ∧ test id).
     645#tag #A #test #id #c elim c
     646[ //
     647| ** [2: #lbl] #s #tl #IH
     648  whd in match (filter_labels ????); normalize nodelta
     649  whd in match (occurs_exactly_once ????) in ⊢ (??%%);
     650  [2: @IH]
     651  normalize in match (! l ← ? ; ?); >IH
     652  >does_not_occur_filter_labels
     653  @(eq_identifier_elim ?? lbl id) #Heq [<Heq]
     654  elim (test lbl) normalize nodelta
     655  change with (eq_identifier ???) in match (instruction_matches_identifier ????);
     656  [1,2: >eq_identifier_refl >commutative_andb [ >(commutative_andb ? true) >commutative_orb | >(commutative_andb ? false)] normalize %
     657  |*: >(eq_identifier_false ??? Heq) normalize nodelta %
     658  ]
     659]
     660qed.
     661
     662lemma nth_opt_filter_labels : ∀tag,A,test,instrs,n.
     663  nth_opt ? n (filter_labels tag A test instrs) =
     664  ! 〈lopt, s〉 ← nth_opt ? n instrs ;
     665  return 〈 ! lbl ← lopt; if test lbl then return lbl else None ?, s〉.
     666#tag #A #test #instrs elim instrs
     667[ * [2: #n'] %
     668| * #lopt #s #tl #IH * [2: #n']
     669  whd in match (filter_labels ????); normalize nodelta
     670  whd in match (nth_opt ???) in ⊢ (??%%); [>IH] %
     671]
     672qed.
     673
     674definition linearize_code:
     675 ∀p : unserialized_params.∀globals.
     676  ∀g : codeT (mk_graph_params p) globals.code_closed … g →
     677  ∀entry : (Σl. code_has_label … g l).
     678    (Σc : codeT (mk_lin_params p) globals.
     679      code_closed … c ∧
     680      ∃ sigma : identifier_map LabelTag ℕ.
     681      lookup … sigma entry = Some ? 0 ∧
     682      ∀l,n.lookup … sigma l = Some ? n →
     683        ∃s. lookup … g l = Some ? s ∧
     684          opt_Exists ?
     685            (λls.let 〈lopt, ts〉 ≝ ls in
     686              opt_All ? (eq ? l) lopt ∧
     687              ts = graph_to_lin_statement … s ∧
     688              opt_All ?
     689                (λnext.Or (lookup … sigma next = Some ? (S n))
     690                (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
     691                (stmt_implicit_label … s)) (nth_opt … n c))
     692
     693 λp,globals,g,g_prf,entry_sig.
     694    let g ≝ branch_compress (mk_graph_params p) ? g entry_sig in
     695    let g_prf ≝ branch_compress_closed … g entry_sig g_prf in
     696    let entry_sig' ≝ mk_Sig ?? entry_sig (branch_compress_has_entry … g entry_sig) in
     697    match graph_visit p globals g ∅ (empty_map …) [ ] [entry_sig] 0 (|g|)
     698      (entry_sig) g_prf ????????
     699    with
     700    [ mk_Sig triple H ⇒
     701      let sigma ≝ \fst (\fst triple) in
     702      let required ≝ \snd (\fst triple) in
     703      let crev ≝ \snd triple in
     704      let lbld_code ≝ rev ? crev in
     705      mk_Sig ?? (filter_labels … (λl.l∈required) lbld_code) ? ].
     706[ (* done later *)
     707| #i >mem_set_empty *
     708| %
     709|#l #n normalize in ⊢ (%→?); #ABS destruct(ABS)
     710| #l #_ %
     711| % [2: %] @(pi2 … entry_sig')
     712| %
     713| % % [% %] cases (pi1 … entry_sig) normalize #_ % //
     714| >commutative_plus change with (? ≤ |g|) %
     715]
     716lapply (refl … triple)
     717generalize in match triple in ⊢ (???%→%); **
     718#visited #required #generated #EQtriple
     719>EQtriple in H ⊢ %; normalize nodelta ***
     720#entry_O #req_vis #labels_in_req #sigma_prop
     721% >EQtriple
     722[ (* code closed *)
     723  @All_map
     724  [2: @All_rev
     725    @(All_mp … labels_in_req) #ls #H @H
     726  |1: (* side-effect close *)
     727  |3: * #lopt #s @All_mp
     728    #lbl #lbl_req whd in match (code_has_label ????);
     729    >occurs_exactly_once_filter_labels
     730    @andb_Prop [2: assumption]
     731    lapply (in_map_domain … visited lbl)
     732    >(req_vis … lbl_req) * #n #eq_lookup
     733    elim (sigma_prop ?? eq_lookup) #H #_ @H
     734  ]
     735]
     736%{visited} % [assumption]
     737#lbl #n #eq_lookup elim (sigma_prop ?? eq_lookup)
     738#lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in
     739% [2: % [ assumption ] |]
     740>nth_opt_filter_labels in ⊢ (???%);
     741>nth_opt_is_stmt
     742whd in match (! 〈lopt, s〉 ← Some ??; ?);
     743whd
     744whd in match (! lbl0 ← Some ??; ?);
     745% [ % [ elim (lbl ∈ required) ] % ]
     746whd
     747lapply (refl … (stmt_implicit_label … stmt))
     748generalize in match (stmt_implicit_label … stmt) in ⊢ (???%→%); * [2: #next]
     749#eq_impl_lbl normalize nodelta [2: %]
     750>eq_impl_lbl in succ_is_in; whd in match (opt_All ???); * #H
     751[ %{H}
     752| %2 >nth_opt_filter_labels >H
     753  whd in match (! 〈lopt, s〉 ← ?; ?);
     754  whd in match (! lbl0 ← ?; ?);
     755  %
     756]
     757qed.
     758
     759definition graph_linearize :
     760  ∀p : unserialized_params.
     761  ∀globals. ∀fin : joint_closed_internal_function globals (mk_graph_params p).
     762    Σfout : joint_closed_internal_function globals (mk_lin_params p).
     763      ∃sigma : identifier_map LabelTag ℕ.
     764        let g ≝ joint_if_code ?? (pi1 … fin) in
     765        let c ≝ joint_if_code ?? (pi1 … fout) in
     766        let entry ≝ joint_if_entry ?? (pi1 … fin) in
     767         lookup … sigma entry = Some ? 0 ∧
     768          ∀l,n.lookup … sigma l = Some ? n →
     769            ∃s. lookup … g l = Some ? s ∧
     770              opt_Exists ?
     771                (λls.let 〈lopt, ts〉 ≝ ls in
     772                  opt_All ? (eq ? l) lopt ∧
     773                  ts = graph_to_lin_statement … s ∧
     774                  opt_All ?
     775                    (λnext.Or (lookup … sigma next = Some ? (S n))
     776                    (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
     777                    (stmt_implicit_label … s)) (nth_opt … n c) ≝
     778  λp,globals,f_sig.
     779  mk_Sig ?? (match f_sig with
     780  [ mk_Sig f f_prf ⇒ 
     781  mk_joint_internal_function globals (mk_lin_params p)
     782   (joint_if_luniverse ?? f) (joint_if_runiverse ?? f)
     783   (joint_if_result ?? f) (joint_if_params ?? f) (joint_if_locals ?? f)
     784   (joint_if_stacksize ?? f)
     785   (linearize_code p globals (joint_if_code … f) f_prf (joint_if_entry … f))
     786   (mk_Sig ?? it I) (mk_Sig ?? it I)
     787  ]) ?.
     788elim f_sig
     789normalize nodelta #f_in #f_in_prf
     790elim (linearize_code ?????)
     791#f_out * #f_out_closed #H assumption
     792qed.
     793
    197794 
    198795
Note: See TracChangeset for help on using the changeset viewer.