Ignore:
Timestamp:
Jan 30, 2013, 7:25:39 PM (8 years ago)
Author:
tranquil
Message:
  • dropped locals and exit from definition of joint_if_function
  • new definition of blocks to accomodate ERTLptr pass
  • stated properties of translation as axioms
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/TranslateUtils.ma

    r2557 r2595  
    44include "utilities/deqsets.ma".
    55
    6 (* general type of functions generating fresh things *)
    7 definition freshT ≝ λpars : params.λg.state_monad (joint_internal_function pars g).
    8 
    9 include alias "basics/lists/list.ma".
     6(*include alias "basics/lists/list.ma".
    107let rec repeat_fresh pars globals A (fresh : freshT pars globals A) (n : ℕ)
    118  on n :
     
    1714    ! reg ← fresh ;
    1815    return «reg::regs',?»
    19   ]. [% | @hide_prf cases regs' #l #EQ normalize >EQ % ] qed.
     16  ]. [% | @hide_prf cases regs' #l #EQ normalize >EQ % ] qed.*)
    2017
    2118definition fresh_label:
    22  ∀g_pars,globals.freshT globals g_pars label ≝
     19 ∀g_pars,globals.state_monad (joint_internal_function g_pars globals) label ≝
    2320  λg_pars,globals,def.
    2421    let 〈r,luniverse〉 ≝ fresh … (joint_if_luniverse … def) in
    2522     〈set_luniverse … def luniverse, r〉.
     23
     24definition fresh_register:
     25 ∀g_pars,globals.state_monad (joint_internal_function g_pars globals) register ≝
     26  λg_pars,globals,def.
     27    let 〈r,runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
     28     〈set_runiverse … def runiverse, r〉.
    2629
    2730(* insert into a graph a block of instructions *)
     
    2932  (g_pars: graph_params)
    3033  (globals: list ident)
    31   (insts: list (joint_seq g_pars globals))
    32   (src : label) on insts : state_monad (joint_internal_function g_pars globals) label
    33   match insts with
    34   [ nil ⇒ return src
     34  (insts: list (joint_step g_pars globals))
     35  (src : label) (dst : label) on insts : joint_internal_function g_pars globals → joint_internal_function g_pars globals
     36  λdef.match insts with
     37  [ nil ⇒ add_graph … src (sequential … (NOOP …) dst) def
    3538  | cons instr others ⇒
    36     ! mid ← fresh_label … ;
    37     ! def ← state_get … ;
    38     !_ state_set … (add_graph … src (sequential … instr mid) def) ;
    39     adds_graph_list g_pars globals others mid
    40   ].
    41 
    42 definition is_inr : ∀A,B.A + B → bool ≝ λA,B,x.match x with
    43   [ inl _ ⇒ true
    44   | inr _ ⇒ false
    45   ].
    46 definition is_inl : ∀A,B.A + B → bool ≝ λA,B,x.match x with
    47   [ inl _ ⇒ true
    48   | inr _ ⇒ false
     39    match others with
     40    [ nil ⇒ add_graph … src (sequential … instr dst) def
     41    | _ ⇒
     42      let 〈def', mid〉 ≝ fresh_label … def in
     43      let def'' ≝ add_graph … src (sequential … instr mid) def' in
     44      adds_graph_list … others mid dst def''
     45    ]
    4946  ].
    5047
     
    5249  ∀g_pars : graph_params.
    5350  ∀globals: list ident.
    54   ∀b : seq_block g_pars globals (joint_step g_pars globals) +
    55        seq_block g_pars globals (joint_fin_step g_pars).
    56   label → if is_inl … b then label else unit →
     51  ∀b : step_block g_pars globals.
     52  label → label →
    5753  joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
    58   λg_pars,globals,insts,src.
    59   match insts return λx.if is_inl … x then ? else ? → ? → ? with
    60   [ inl b ⇒ λdst,def.
    61     let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
    62     add_graph … mid (sequential … (\snd b) dst) def
    63   | inr b ⇒ λdst,def.
    64     let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
    65     add_graph … mid (final … (\snd b)) def
     54  λg_pars,globals,insts,src,dst,def.
     55  let 〈pref, last〉 ≝ split_on_last_ne … insts in
     56  match pref with
     57  [ nil ⇒ add_graph … src (sequential … (last src) dst) def
     58  | _ ⇒
     59    let 〈def', lbl〉 ≝ fresh_label … def in
     60    let def'' ≝ adds_graph_list … (map_eval … pref lbl) src lbl def' in
     61    add_graph … lbl (sequential … (last lbl) dst) def''
     62  ].
     63
     64definition fin_adds_graph :
     65  ∀g_pars : graph_params.
     66  ∀globals: list ident.
     67  ∀b : fin_block g_pars globals.
     68  label →
     69  joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
     70  λg_pars,globals,insts,src,def.
     71  let 〈pref, last〉 ≝ insts in
     72  match pref with
     73  [ nil ⇒ add_graph … src (final … last) def
     74  | _ ⇒
     75    let 〈def', lbl〉 ≝ fresh_label … def in
     76    let def'' ≝ adds_graph_list … pref src lbl def' in
     77    add_graph … lbl (final … last) def''
    6678  ].
    6779
     
    7082definition luniverse_ok : ∀p : graph_params.∀g.joint_internal_function p g → Prop ≝
    7183λp,g,def.fresh_map_for_univ … (joint_if_code … def) (joint_if_luniverse … def).
    72 
    73 lemma present_to_memb : ∀tag,A,l,m.present tag A m l → bool_to_Prop (l∈m).
    74 #tag #A * #l * #m whd in ⊢ (%→?%);
    75 elim (lookup tag ???)
    76 [ * #ABS elim (ABS ?) %
    77 | #a #_ %
    78 ] qed.
    79 
    80 lemma memb_to_present : ∀tag,A,l,m.l∈m → present tag A m l.
    81 #tag #A * #l * #m whd in ⊢ (?%→%);
    82 elim (lookup tag ???)
    83 [ * | #a * % #ABS destruct(ABS) ] qed.
    8484
    8585(*
     
    114114qed.
    115115
     116lemma fresh_not_in_univ : ∀tag,id,u,u'.
     117〈id, u'〉 = fresh tag u →
     118¬fresh_for_univ tag id u.
     119#tag * #id * #u * #u' normalize #EQ destruct //
     120qed.
     121
     122lemma adds_graph_list_fresh_preserve :
     123  ∀g_pars,globals,b,src,dst,def.
     124  let def' ≝ adds_graph_list g_pars globals b src dst def in
     125  ∀lbl.fresh_for_univ … lbl (joint_if_luniverse … def) →
     126       fresh_for_univ … lbl (joint_if_luniverse … def').
     127#g_pars #globals #l elim l -l
     128[ #src #dst #def whd #lbl #H @H ]
     129#hd1 * [ #_ #src #dst #def whd #lbl #H @H ] #hd2 #tl #IH #src #dst #def whd #lbl #H
     130whd in match (adds_graph_list ??????);
     131whd in match fresh_label; normalize nodelta
     132inversion (fresh ??) #mid #luniv' #EQfresh lapply (sym_eq ??? EQfresh) -EQfresh #EQfresh
     133normalize nodelta
     134@IH whd in match (joint_if_luniverse ???);
     135@(fresh_remains_fresh … EQfresh) @H
     136qed.
     137
     138lemma with_last_not_empty : ∀X,pref,last.not_empty X (pref @ [last]).
     139#X * [2: #hd #tl ] #last % qed.
     140
     141lemma split_on_last_ne_elim : ∀X,l.∀P : ((list X) × X) → Prop.
     142(∀pref,last.pi1 ?? l = pref @ [last] → P 〈pref, last〉) →
     143P (split_on_last_ne X l).
     144#X * @list_elim_left [ * ] #last #pref #_ #prf #P #H
     145>split_on_last_ne_def @H % qed.
     146
    116147(* use Russell? *)
    117 axiom adds_graph_list_ok :
    118   ∀g_pars,globals,b,src,def.
     148lemma adds_graph_list_ok :
     149  ∀g_pars,globals,b,src,dst,def.
    119150  fresh_for_univ … src (joint_if_luniverse … def) →
    120151  luniverse_ok ?? def →
    121   let 〈def', dst〉 ≝ adds_graph_list g_pars globals b src def in
     152  let def' ≝ adds_graph_list g_pars globals b src dst def in
    122153  luniverse_ok ?? def' ∧
     154  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
     155                      stmt_at … (joint_if_code … def') lbl =
     156                      stmt_at … (joint_if_code … def) lbl) ∧
     157  let B ≝ ensure_step_block … b in
    123158  ∃l.bool_to_Prop (uniqueb … l) ∧
    124      All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
    125                   fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
    126      src ~❨b,l❩~> dst in joint_if_code … def'.
    127 (*
    128 #p #g #l elim l -l
    129 [ #src #def #_ #Hdef whd
    130   %{Hdef} %{[ ]} %%% ]
    131 #hd #tl #IH #src #def #src_fresh #Hdef
    132 whd in match (adds_graph_list ?????);
     159    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
     160                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
     161    src ~❨B,l❩~> dst in joint_if_code … def'.
     162#p #g #l elim l -l [2: #hd1 * [ #_ | #hd2 #tl #IH ]]
     163#src #dst #def #Hsrc #Hdef
     164[1,3: %
     165  [1,3: %
     166    [1,3: #lbl @(eq_identifier_elim … lbl src) #H destruct [1,3: #_ @Hsrc ]
     167      whd in ⊢ (%→?); whd in match (adds_graph_list ??????);
     168      >(lookup_add_miss ?????? H) @Hdef
     169    |*: #lbl #H #G @lookup_add_miss @H
     170    ]
     171  |*: %{[]} % [1,3: %% ] %{src} % [1,3:%] %{dst} % [1,3: @lookup_add_hit ] %
     172  ]
     173]
     174whd in match (adds_graph_list ??????);
    133175whd in match (fresh_label ???);
    134 @(pair_elim … (fresh ??)) normalize nodelta
    135 #mid #luniverse' #EQfresh
    136 whd in ⊢ (match % with [ _ ⇒ ?]);
    137 letin def' ≝ (add_graph p g src (sequential … hd mid) (set_luniverse … def luniverse'))
    138 cut (joint_if_code p g (set_luniverse p g def luniverse') = joint_if_code … def)
    139   [ % ] #EQ_aux
    140   lapply (IH mid def' ??)
    141   [ #l whd in match def'; #Hpres
    142     lapply (present_to_memb … Hpres) -Hpres
    143     >mem_set_add @eq_identifier_elim
    144     [ #EQ destruct(EQ) *
    145     | #NEQ change with (? ∈ joint_if_code p ??) in ⊢ (?%→?); >EQ_aux
    146       #l_in
     176inversion (fresh ??) normalize nodelta
     177#mid #luniverse' #EQfresh lapply (sym_eq ??? EQfresh) -EQfresh #EQfresh
     178letin def' ≝ (add_graph p g src (sequential … hd1 mid) (set_luniverse … def luniverse'))
     179lapply (IH mid dst def' ??)
     180[ #lbl @(eq_identifier_elim … lbl src) #H destruct
     181  [2: whd in ⊢ (%→?); whd in match (adds_graph_list ??????);
     182    >(lookup_add_miss ?????? H) ]
     183  #Hpres @(fresh_remains_fresh … EQfresh) [ @Hdef ] assumption
     184| whd in match def';
     185  @(fresh_is_fresh … EQfresh)
     186]
     187whd in match (joint_if_luniverse ???);
     188whd in match (joint_if_code ???);
     189** #Hdef'' #stmt_preserved * #l ** #Hl1 #Hl2
     190whd in ⊢ (%→?); @split_on_last_ne_elim #pref #last #EQ * #mid' * #Hl3 #Hl4
     191%
     192[ %{Hdef''} #lbl #NEQ
     193  @(eq_identifier_elim ?? lbl mid)
     194  [ #EQ destruct #ABS cases (absurd ? ABS ?) @(fresh_not_in_univ … EQfresh)
     195  | #NEQ' #H >(stmt_preserved … NEQ')
     196    [ whd in match (joint_if_code ???);
     197      whd in match (stmt_at ????); >lookup_add_miss [2: @NEQ ] %
     198    | @(fresh_remains_fresh … EQfresh) @H
    147199    ]
    148     @(fresh_remains_fresh … (sym_eq … EQfresh))
    149     [2: @Hdef @memb_to_present ] assumption
    150   | whd in match def';
    151     cases def #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
    152     whd in match (set_luniverse ????);
    153     @(fresh_is_fresh … (sym_eq … EQfresh))
    154200  ]
    155   elim (adds_graph_list ?????) #def'' #mid' normalize nodelta
    156   * #Hdef'' * #l ** #Hl1 #Hl2 #Hl3 %{Hdef''} %{(mid::l)}
    157   % [ % ]
    158   [ whd in ⊢ (?%);
    159     cut (Not (bool_to_Prop (mid∈l)))
    160     [ % #H elim (All_memb … Hl2 H)
    161       whd in match (joint_if_luniverse ???);
    162       #G #_ @(absurd ?? G)
    163       @ (fresh_is_fresh … (sym_eq … EQfresh))
    164     | #H >H assumption
    165     ]
    166   | %
    167     [ %
    168       [
    169       normalize #H10 #H11
    170      
    171     >(All_fresh_not_memb … (sym_eq … EQfresh))
    172     [ assumption ]
    173     @(All_mp … Hl2) #lbl *
    174     cases def in EQfresh; #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19
    175     normalize #EQfresh #H #lbl_not_mid
    176     lapply(fresh_remains_fresh … H (sym_eq … EQfresh))
    177    
    178     elim (true_or_false_Prop (mid∈l)) #mid_l >mid_l
    179     [ normalize
    180 *)
     201]
     202%{(mid::l)}
     203% [ % ]
     204[ whd in ⊢ (?%);
     205  cut (Not (bool_to_Prop (mid∈l)))
     206  [ % #H elim (All_memb … Hl2 H)
     207    whd in match (joint_if_luniverse ???);
     208    #G #_ @(absurd ?? G)
     209    @ (fresh_is_fresh … EQfresh)
     210  | #H >H assumption
     211  ]
     212| %
     213  [ %{(fresh_not_in_univ … EQfresh)}
     214    @adds_graph_list_fresh_preserve @(fresh_is_fresh … EQfresh)
     215  | @(All_mp … Hl2) #lbl * * #H1 #H2 %{H2} % #H3 @H1
     216    @(fresh_remains_fresh … EQfresh) assumption
     217  ]
     218| whd in match (ensure_step_block ???) in EQ ⊢ %;
     219  whd in match (map ??? (hd2 :: ?)); >EQ whd
     220  change with ((?::?)@?) in match (?::?@?); >split_on_last_ne_def
     221  %{mid'} % [2: @Hl4 ]
     222  %{Hl3} %{mid} >stmt_preserved
     223  [ % [2: % ] @lookup_add_hit
     224  | @(fresh_remains_fresh … EQfresh) assumption
     225  | % #ABS destruct @(absurd ? Hsrc) @(fresh_not_in_univ … EQfresh)
     226  ]
     227]
     228qed.
     229
     230axiom adds_graph_ok :
     231  ∀g_pars,globals,B,src,dst,def.
     232  fresh_for_univ … src (joint_if_luniverse … def) →
     233  luniverse_ok ?? def →
     234  let def' ≝ adds_graph g_pars globals B src dst def in
     235  luniverse_ok ?? def' ∧
     236  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
     237                      stmt_at … (joint_if_code … def') lbl =
     238                      stmt_at … (joint_if_code … def) lbl) ∧
     239  ∃l.bool_to_Prop (uniqueb … l) ∧
     240    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
     241                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
     242    src ~❨B,l❩~> dst in joint_if_code … def'.
     243 
     244axiom fin_adds_graph_ok :
     245  ∀g_pars,globals,B,src,def.
     246  fresh_for_univ … src (joint_if_luniverse … def) →
     247  luniverse_ok ?? def →
     248  let def' ≝ fin_adds_graph g_pars globals B src def in
     249  luniverse_ok ?? def' ∧
     250  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
     251                      stmt_at … (joint_if_code … def') lbl =
     252                      stmt_at … (joint_if_code … def) lbl) ∧
     253  ∃l.bool_to_Prop (uniqueb … l) ∧
     254    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
     255                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
     256    src ~❨B,l❩~> it in joint_if_code … def'.
    181257
    182258(* preserves first statement if a cost label (should be an invariant) *)
     
    189265  with
    190266  [ Some s ⇒ λ_.
     267    let default_add ≝ λ_ : unit.
     268      let 〈def', lbl〉 ≝ fresh_label … def in
     269      let def'' ≝ add_graph … lbl s def' in
     270      adds_graph … insts entry lbl def'' in
    191271    match s with
    192272    [ sequential s' next ⇒
     
    195275        match s'' with
    196276        [ COST_LABEL _ ⇒
    197           adds_graph ?? (inl … (s'' :: insts)) entry next def
     277          adds_graph ?? (s'' :: insts) entry next def
    198278        | _ ⇒
    199           let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
    200           add_graph … tmp s def'
     279          default_add it
    201280        ]
    202281      | _ ⇒
    203         let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
    204         add_graph … tmp s def'
     282        default_add it
    205283      ]
    206284    | _ ⇒
    207       let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
    208       add_graph … tmp s def'
     285      default_add it
    209286    ]
    210287  | None ⇒ Ⓧ
    211288  ] (pi2 … entry).
    212289
     290(*
    213291definition insert_epilogue ≝
    214292  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
     
    226304whd in match def''; >graph_code_has_point //
    227305qed.
     306*)
    228307
    229308definition b_adds_graph :
    230309  ∀g_pars: graph_params.
    231310  ∀globals: list ident.
    232   (* fresh register creation *)
    233   freshT g_pars globals (localsT … g_pars) →
    234   ∀b : bind_seq_block g_pars globals (joint_step g_pars globals) +
    235        bind_seq_block g_pars globals (joint_fin_step g_pars).
    236   label → if is_inl … b then label else unit →
     311  ∀b : bind_step_block g_pars globals.
     312  label → label →
    237313  joint_internal_function g_pars globals→
    238314  joint_internal_function g_pars globals ≝
    239   λg_pars,globals,fresh_r,insts,src.
    240   match insts return λx.if is_inl … x then ? else ? → ? → ? with
    241   [ inl b ⇒ λdst,def.
    242     let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
    243     adds_graph … (inl … stmts) src dst def
    244   | inr b ⇒ λdst,def.
    245     let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
    246     adds_graph … (inr … stmts) src dst def
    247   ].
    248 
    249  
     315  λg_pars,globals,insts,src,dst,def.
     316  let 〈def, stmts〉 ≝ bcompile ??? (fresh_register …) insts def in
     317  adds_graph … stmts src dst def.
     318
     319axiom b_adds_graph_ok :
     320  ∀g_pars,globals,B,src,dst,def.
     321  fresh_for_univ … src (joint_if_luniverse … def) →
     322  luniverse_ok ?? def →
     323  let def' ≝ b_adds_graph g_pars globals B src dst def in
     324  luniverse_ok ?? def' ∧
     325  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
     326                      stmt_at … (joint_if_code … def') lbl =
     327                      stmt_at … (joint_if_code … def) lbl) ∧
     328  ∃l,r.
     329    bool_to_Prop (uniqueb … l) ∧
     330    bool_to_Prop (uniqueb … r) ∧
     331    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
     332                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
     333    All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def) ∧
     334                 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧
     335    src ~❨B,l,r❩~> dst in joint_if_code … def'.
     336 
     337definition b_fin_adds_graph :
     338  ∀g_pars: graph_params.
     339  ∀globals: list ident.
     340  ∀b : bind_fin_block g_pars globals.
     341  label →
     342  joint_internal_function g_pars globals→
     343  joint_internal_function g_pars globals ≝
     344  λg_pars,globals,insts,src,def.
     345  let 〈def, stmts〉 ≝ bcompile ??? (fresh_register …) insts def in
     346  fin_adds_graph … stmts src def.
     347
     348axiom b_fin_adds_graph_ok :
     349  ∀g_pars,globals,B,src,def.
     350  fresh_for_univ … src (joint_if_luniverse … def) →
     351  luniverse_ok ?? def →
     352  let def' ≝ b_fin_adds_graph g_pars globals B src def in
     353  luniverse_ok ?? def' ∧
     354  (∀lbl.lbl ≠ src → fresh_for_univ … lbl (joint_if_luniverse … def) →
     355                      stmt_at … (joint_if_code … def') lbl =
     356                      stmt_at … (joint_if_code … def) lbl) ∧
     357  ∃l,r.
     358    bool_to_Prop (uniqueb … l) ∧
     359    bool_to_Prop (uniqueb … r) ∧
     360    All … (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def) ∧
     361                 fresh_for_univ … lbl (joint_if_luniverse … def')) l ∧
     362    All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def) ∧
     363                 fresh_for_univ … reg (joint_if_runiverse … def')) r ∧
     364    src ~❨B,l,r❩~> it in joint_if_code … def'.
    250365
    251366(* translation with inline fresh register allocation *)
     
    253368  ∀src_g_pars,dst_g_pars : graph_params.
    254369  ∀globals: list ident.
    255   (* fresh register creation *)
    256   freshT dst_g_pars globals (localsT dst_g_pars) →
    257370  (* initialized function definition with empty graph *)
    258371  joint_internal_function dst_g_pars globals →
    259372  (* functions dictating the translation *)
    260   (label → joint_step src_g_pars globals →
    261     bind_seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
    262   (label → joint_fin_step src_g_pars →
    263     bind_seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
     373  (label → joint_step src_g_pars globals → bind_step_block dst_g_pars globals) →
     374  (label → joint_fin_step src_g_pars → bind_fin_block dst_g_pars globals) →
    264375  (* source function *)
    265376  joint_internal_function src_g_pars globals →
    266377  (* destination function *)
    267378  joint_internal_function dst_g_pars globals ≝
    268   λsrc_g_pars,dst_g_pars,globals,fresh_reg,empty,trans_step,trans_fin_step,def.
     379  λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def.
    269380  let f : label → joint_statement (src_g_pars : params) globals →
    270381    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
     
    272383    match stmt with
    273384    [ sequential inst next ⇒
    274       b_adds_graph … fresh_reg (inl … (trans_step lbl inst)) lbl next def
     385      b_adds_graph … (trans_step lbl inst) lbl next def
    275386    | final inst ⇒
    276       b_adds_graph … fresh_reg (inr … (trans_fin_step lbl inst)) lbl it def
     387      b_fin_adds_graph … (trans_fin_step lbl inst) lbl def
    277388    | FCOND abs _ _ _ ⇒ Ⓧabs
    278389    ] in
    279390  foldi … f (joint_if_code … def) empty.
    280391
    281 (* translation without register allocation *)
     392definition partial_partition : ∀X.∀Y : DeqSet.(X → option (list Y)) → Prop ≝
     393λX,Y,f.
     394(∀x.opt_All … (λys.bool_to_Prop (uniqueb … ys)) (f x)) ∧
     395(∀x1,x2.
     396  opt_All …
     397    (λys1.
     398      opt_All …
     399      (λys2.
     400        ∀y.y ∈ ys1 → y ∈ ys2 → x1 = x2)
     401      (f x2))
     402    (f x1)).
     403
     404lemma opt_All_intro : ∀X,P,o.
     405(∀x.o = Some ? x → P x) → opt_All X P o. #X #P * [//] #x #H @H % qed.
     406 
     407(*
     408definition points_of : ∀p,g.joint_internal_function p g → Type[0] ≝
     409λp,g,def.Σl.bool_to_Prop (code_has_point … (joint_if_code … def) l).
     410
     411unification hint 0 ≔ p, g, def;
     412points ≟ code_point p,
     413code ≟ joint_if_code p g def,
     414P ≟ λl : points.bool_to_Prop (code_has_point p g code l)
     415
     416points_of p g def ≡ Sig points P.
     417
     418definition stmt_at_safe : ∀p,g,def.points_of p g def → joint_statement p g ≝
     419  λp,g,def,pt.opt_safe ? (stmt_at ?? (joint_if_code ?? def) (pi1 … pt)) ?.
     420@hide_prf cases pt -pt #pt whd in ⊢ (?%→?); #H % #G >G in H; * qed.
     421*)
     422
     423axiom b_graph_translate_ok :
     424  ∀src_g_pars,dst_g_pars : graph_params.
     425  ∀globals: list ident.∀empty.∀f_step,f_fin,def_in.
     426  luniverse_ok ?? def_in →
     427  let def_out ≝
     428    b_graph_translate src_g_pars dst_g_pars globals empty f_step f_fin def_in in
     429  luniverse_ok … def_out ∧
     430  joint_if_result … def_out = joint_if_result … empty ∧
     431  joint_if_params … def_out = joint_if_params … empty ∧
     432  joint_if_stacksize … def_out = joint_if_stacksize … empty ∧
     433  pi1 … (joint_if_entry … def_out) = pi1 … (joint_if_entry … def_in) ∧
     434  ∃f_lbls : label → option (list label).
     435  ∃f_regs : label → option (list register).
     436  partial_partition … f_lbls ∧
     437  partial_partition … f_regs ∧
     438  (∀l.opt_All … (All …
     439    (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
     440           fresh_for_univ … lbl (joint_if_luniverse … def_out))) (f_lbls l)) ∧
     441  (∀l.opt_All … (All …
     442    (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
     443           fresh_for_univ … reg (joint_if_runiverse … def_out))) (f_regs l)) ∧
     444  ∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s →
     445  ∃lbls,regs.f_lbls l = Some ? lbls ∧ f_regs l = Some ? regs ∧
     446  match s with
     447  [ sequential s' nxt ⇒
     448    l ~❨f_step l s', lbls, regs❩~> nxt in joint_if_code … def_out
     449  | final s' ⇒
     450    l ~❨f_fin l s', lbls, regs❩~> it in joint_if_code … def_out
     451  | FCOND abs _ _ _ ⇒ Ⓧabs
     452  ].
     453
     454definition added_registers :
     455  ∀p : graph_params.∀g.
     456  joint_internal_function p g → (label → option (list register)) → list register ≝
     457  λp,g,def,f_regs.
     458  let f ≝ λlbl : label.λ_.λacc.
     459    match f_regs lbl with [ None ⇒ acc | Some regs ⇒ regs@acc ] in
     460  foldi … f (joint_if_code p g def) [ ].
     461
     462axiom added_registers_ok :
     463  ∀p,g,def,f_regs.
     464  ∀l,s.stmt_at … (joint_if_code … def) l = Some ? s →
     465  opt_All … (All … (λlbl.bool_to_Prop (lbl ∈ added_registers p g def f_regs))) (f_regs l).
     466
     467(* translation without register allocation (more or less an alias) *)
    282468definition graph_translate :
    283469  ∀src_g_pars,dst_g_pars : graph_params.
     
    286472  joint_internal_function dst_g_pars globals →
    287473  (* functions dictating the translation *)
    288   (label → joint_step src_g_pars globals →
    289     seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
    290   (label → joint_fin_step src_g_pars →
    291     seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
     474  (label → joint_step src_g_pars globals → step_block dst_g_pars globals) →
     475  (label → joint_fin_step src_g_pars → fin_block dst_g_pars globals) →
    292476  (* source function *)
    293477  joint_internal_function src_g_pars globals →
    294478  (* destination function *)
    295479  joint_internal_function dst_g_pars globals ≝
    296   λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def.
    297   let f : label → joint_statement (src_g_pars : params) globals →
    298     joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
    299     λlbl,stmt,def.
    300     match stmt with
    301     [ sequential inst next ⇒
    302       adds_graph … (inl … (trans_step lbl inst)) lbl next def
    303     | final inst ⇒
    304       adds_graph … (inr … (trans_fin_step lbl inst)) lbl it def
    305     | FCOND abs _ _ _ ⇒ Ⓧabs
    306     ] in
    307   foldi … f (joint_if_code … def) empty.
    308 
     480  λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step.
     481  b_graph_translate … empty
     482    (λl,s.return trans_step l s)
     483    (λl,s.return trans_fin_step l s).
     484
     485(* helper for initializing a valid init graph (with a valid entry) *)
    309486definition init_graph_if ≝
    310487  λg_pars : graph_params.λglobals.
    311   λluniverse,runiverse,ret,params,locals,stack_size,entry,exit.
    312   let graph ≝ add ? ? (empty_map ? (joint_statement ??)) entry (GOTO … exit) in
    313   let graph ≝ add ? ? graph exit (RETURN …) in
     488  λluniverse,runiverse,ret,params,stack_size,entry.
     489  let graph ≝ add ?? (empty_map ? (joint_statement ??)) entry (RETURN …) in
    314490  mk_joint_internal_function g_pars globals
    315     luniverse runiverse ret params locals stack_size
    316     graph entry exit.
    317 >graph_code_has_point @map_mem_prop
    318 [@graph_add_lookup] @graph_add
     491    luniverse runiverse ret params stack_size
     492    graph entry.
     493@hide_prf >graph_code_has_point @map_mem_prop @graph_add
    319494qed.
    320495
Note: See TracChangeset for help on using the changeset viewer.