Changeset 2595


Ignore:
Timestamp:
Jan 30, 2013, 7:25:39 PM (6 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
Location:
src/joint
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2562 r2595  
    8888 (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *)
    8989 ; paramsT : Type[0]
    90  ; localsT: Type[0]
    9190 }.
    9291
     
    409408  joint_if_result   : call_dest p;
    410409  joint_if_params   : paramsT p;
    411   joint_if_locals   : list (localsT p); (* use void where no locals are present *)
    412410(*CSC: XXXXX stacksize unused for LTL-...*)
    413411  joint_if_stacksize: nat;
    414412  joint_if_code     : codeT p globals ;
    415   joint_if_entry : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) ;
    416   joint_if_exit : Σpt.bool_to_Prop (code_has_point … joint_if_code pt)
     413  joint_if_entry : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) (*;
     414  joint_if_exit : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) *)
    417415}.
    418416
     
    431429  λgraph: codeT pars globals.
    432430  λentry.
    433   λexit.
     431  (*λexit.*)
    434432    mk_joint_internal_function pars globals
    435433      (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun)
    436       (joint_if_params … int_fun) (joint_if_locals … int_fun) (joint_if_stacksize … int_fun)
    437       graph entry exit.
     434      (joint_if_params … int_fun) (joint_if_stacksize … int_fun)
     435      graph entry (*exit*).
    438436
    439437definition set_joint_if_graph ≝
     
    442440  λp:joint_internal_function pars globals.
    443441  λentry_prf.
    444   λexit_prf.
     442  (*λexit_prf.*)
    445443    set_joint_code globals pars p
    446444      graph
    447445      (mk_Sig ?? (joint_if_entry ?? p) entry_prf)
    448       (mk_Sig … (joint_if_exit ?? p) exit_prf).
     446      (*(mk_Sig … (joint_if_exit ?? p) exit_prf)*).
    449447
    450448definition set_luniverse ≝
     
    454452   mk_joint_internal_function globals pars
    455453    luniverse (joint_if_runiverse … p) (joint_if_result … p)
    456     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    457     (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
     454    (joint_if_params … p) (joint_if_stacksize … p)
     455    (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*).
    458456
    459457definition set_runiverse ≝
     
    463461   mk_joint_internal_function globals pars
    464462    (joint_if_luniverse … p) runiverse (joint_if_result … p)
    465     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
    466     (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
     463    (joint_if_params … p) (joint_if_stacksize … p)
     464    (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*).
    467465   
    468466(* Specialized for graph_params *)
     
    473471    mk_joint_internal_function …
    474472     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    475      (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
     473     (joint_if_params … p) (joint_if_stacksize … p)
    476474     code
    477475     (pi1 … (joint_if_entry … p))
    478      (pi1 … (joint_if_exit … p)).
     476     (*(pi1 … (joint_if_exit … p))*).
    479477>graph_code_has_point whd in match code; >mem_set_add
    480 @orb_Prop_r [elim (joint_if_entry ???) | elim (joint_if_exit ???) ]
     478@orb_Prop_r elim (joint_if_entry ???)
    481479#x #H <graph_code_has_point @H
    482480qed.
    483481
    484 definition set_locals ≝
    485   λpars,globals.
    486   λp : joint_internal_function pars globals.
    487   λlocals.
    488    mk_joint_internal_function pars globals
    489     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    490     (joint_if_params … p) locals (joint_if_stacksize … p)
    491     (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
    492 
    493482definition joint_function ≝ λp,globals. fundef (joint_closed_internal_function p globals).
    494483
  • 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
  • src/joint/blocks.ma

    r2422 r2595  
    4242  (list (block_step p globals)) × A.*)
    4343
    44 definition seq_block ≝ λp : stmt_params.λglobals,A.
    45   (list (joint_seq p globals)) × A.
     44(* move *)
     45let rec bind_new_P R X (P : X → Prop) (b : bind_new R X) on b : Prop ≝
     46match b with
     47[ bret x ⇒ P x
     48| bnew f ⇒ ∀x.bind_new_P … P (f x)
     49].
     50
     51definition BindNewP : ∀R.MonadPred (BindNew R) ≝
     52λR.mk_MonadPred (BindNew R) (bind_new_P R) ???.
     53[ #X #P #x #K @K
     54| #X #Y #Pin #Pout #m elim m -m
     55  [ #x #H #f #G @G @H
     56  | #g #IH #H #f #G #x @IH [ @H | @G ]
     57  ]
     58| #X #P #Q #H #m elim m -m
     59  [ #x #Px @H @Px
     60  | #g #IH #Pg #x @IH @Pg
     61  ]
     62]
     63qed.
     64
     65definition not_empty : ∀X.list X → Prop ≝ λX,l.match l with [ nil ⇒ False | _ ⇒ True ].
     66
     67definition head_ne : ∀X.(Σl.not_empty X l) → X ≝
     68λX,l.
     69match l return λl.not_empty ? l → ? with
     70[ nil ⇒ Ⓧ
     71| cons hd _ ⇒ λ_.hd
     72] (pi2 … l).
     73
     74
     75let rec split_on_last_ne_aux X l on l : not_empty X l → (list X) × X ≝
     76match l return λx.not_empty ? x → ? with
     77[ nil ⇒ Ⓧ
     78| cons hd tl ⇒ λ_.
     79  match tl return λtl.(not_empty X tl → ?) → ? with
     80  [ nil ⇒ λ_.〈[ ], hd〉
     81  | cons hd' tl' ⇒ λrec_call.let 〈pre, last〉 ≝ rec_call I in 〈hd :: pre, last〉
     82  ] (split_on_last_ne_aux ? tl)
     83].
     84
     85definition split_on_last_ne : ∀X.(Σl.not_empty X l) → (list X)×X ≝
     86λX,l.split_on_last_ne_aux … (pi2 … l).
     87
     88definition last_ne : ∀X.(Σl.not_empty X l) → X ≝ λX,l.\snd (split_on_last_ne … l).
     89definition chop_last_ne : ∀X.(Σl.not_empty X l) → list X ≝ λX,l.\fst (split_on_last_ne … l).
     90
     91lemma split_on_last_ne_def : ∀X,pre,last,prf.split_on_last_ne X «pre@[last], prf» = 〈pre, last〉.
     92whd in match split_on_last_ne; normalize nodelta
     93#X #pre elim pre -pre [ #last #prf % ]
     94#hd * [2: #hd' #tl'] #IH #last *
     95[ whd in ⊢ (??%?); >IH % | % ]
     96qed.
     97
     98lemma split_on_last_ne_inv : ∀X,l.
     99pi1 ?? l = (let 〈pre, last〉 ≝ split_on_last_ne X l in pre @ [last]).
     100whd in match split_on_last_ne; normalize nodelta
     101#X * #l elim l -l [ * ]
     102#hd * [2: #hd' #tl'] #IH * [2: % ]
     103whd in match (split_on_last_ne_aux ???);
     104lapply (IH I) @pair_elim #pre #last #_ #EQ >EQ %
     105qed.
     106
     107(* the label input is to accomodate ERTptr pass *)
     108definition step_block ≝ λp,globals.Σl : list (code_point p → joint_step p globals).not_empty ? l.
     109unification hint 0 ≔ p : params, g;
     110S ≟ code_point p → joint_step p g,
     111L ≟ list S,
     112P ≟ not_empty S
     113(*---------------------------------------*)⊢
     114step_block p g ≡ Sig L P.
     115
     116definition fin_block ≝ λp,globals.(list (joint_step p globals))×(joint_fin_step p).
    46117
    47118(*definition seq_to_skip_block :
     
    53124  seq_to_skip_block on _b : seq_block ??? to skip_block ???.*)
    54125
    55 definition bind_seq_block ≝ λp : stmt_params.λglobals,A.
    56   bind_new (localsT p) (seq_block p globals A).
    57 unification hint 0 ≔ p : stmt_params, g, X;
    58 R ≟ localsT p,
    59 P ≟ seq_block p g X
     126definition bind_step_block ≝ λp.λglobals.
     127  bind_new register (step_block p globals).
     128
     129unification hint 0 ≔ p, g;
     130P ≟ step_block p g
    60131(*---------------------------------------*)⊢
    61 bind_seq_block p g X ≡ bind_new R P.
    62 
    63 definition bind_seq_list ≝ λp : stmt_params.λglobals.
    64   bind_new (localsT p) (list (joint_seq p globals)).
     132bind_step_block p g ≡ bind_new register P.
     133
     134definition bind_fin_block ≝ λp : stmt_params.λglobals.
     135  bind_new register (fin_block p globals).
     136
    65137unification hint 0 ≔ p : stmt_params, g;
    66 R ≟ localsT p,
    67 S ≟ joint_seq p g,
     138P ≟ fin_block p g
     139(*---------------------------------------*)⊢
     140bind_fin_block p g ≡ bind_new register P.
     141
     142definition bind_step_list ≝ λp : stmt_params.λglobals.
     143  bind_new register (list (joint_step p globals)).
     144unification hint 0 ≔ p : stmt_params, g;
     145S ≟ joint_step p g,
    68146L ≟ list S
    69147(*---------------------------------------*)⊢
    70 bind_seq_list p g ≡ bind_new R L.
     148bind_step_list p g ≡ bind_new register L.
     149
     150definition add_dummy_variance : ∀X,Y : Type[0].list Y → list (X → Y) ≝ λX,Y.map … (λx.λ_.x).
     151
     152definition ensure_step_block : ∀p : params.∀globals.
     153list (joint_step p globals) → step_block p globals ≝
     154λp,g,l.match add_dummy_variance … l return λ_.Σl.not_empty ? l with
     155[ nil ⇒ «[λ_.NOOP ??], I»
     156| cons hd tl ⇒ «hd :: tl, I»
     157].
     158
     159definition ensure_step_list : ∀p,globals.
     160list (joint_seq p globals) → list (joint_step p globals) ≝
     161λp,g.map … (step_seq …).
     162
     163definition ensure_step_block_from_seq : ∀p : params.∀globals.
     164list (joint_seq p globals) → step_block p globals ≝
     165λp,g.ensure_step_block ?? ∘ ensure_step_list ??.
     166
     167coercion step_block_from_list nocomposites : ∀p : params.∀g.∀l : list (joint_step p g).step_block p g ≝
     168ensure_step_block on _l : list (joint_step ??) to step_block ??.
     169
     170coercion step_list_from_seq nocomposites : ∀p,g.∀l : list (joint_seq p g).list (joint_step p g) ≝
     171ensure_step_list on _l : list (joint_seq ??) to list (joint_step ??).
     172
     173coercion step_block_from_seq nocomposites : ∀p : params.∀g.∀l : list (joint_seq p g).step_block p g ≝
     174ensure_step_block_from_seq on _l : list (joint_seq ??) to step_block ??.
     175
    71176
    72177(*definition bind_skip_block ≝ λp : stmt_params.λglobals,A.
     
    90195  seq_or_fin_step_classifier ?? (\snd b).
    91196*)
    92 
    93 let rec split_on_last A (dflt : A) (l : list A) on l : (list A) × A ≝
    94 match l with
    95 [ nil ⇒ 〈[ ], dflt〉
    96 | cons hd tl ⇒
    97   match tl with
    98   [ nil ⇒ 〈[ ], hd〉
    99   | _ ⇒
    100     let 〈pref, post〉 ≝ split_on_last A dflt tl in
    101     〈hd :: pref, post〉
    102   ]
    103 ].
    104 
    105 lemma split_on_last_ok :
    106   ∀A,dflt,l.
    107   match l with
    108   [ nil ⇒ True
    109   | _ ⇒ l = (let 〈pre, post〉 ≝ split_on_last A dflt l in pre @ [post])
    110   ].
    111 #A #dflt #l elim l normalize nodelta
    112 [ %
    113 | #hd * [ #_ %]
    114   #hd' #tl #IH whd in match (split_on_last ???); >IH in ⊢ (??%?);
    115   elim (split_on_last ???) #a #b %
    116 ]
    117 qed.
    118 
    119 definition seq_block_from_seq_list :
     197(*definition seq_block_from_seq_list :
    120198∀p : stmt_params.∀g.list (joint_seq p g) → seq_block p g (joint_step p g) ≝
    121199λp,g,l.let 〈pre,post〉 ≝ split_on_last … (NOOP ??) l in 〈pre, (post : joint_step ??)〉.
     
    176254  ∀p:stmt_params.∀g.∀l:bind_new (localsT p) (list (joint_seq p g)).bind_seq_block p g (joint_step p g) ≝
    177255  bind_seq_list_bind_seq_block on _l : bind_new ? (list (joint_seq ??)) to bind_seq_block ?? (joint_step ??).
     256*)
    178257
    179258notation > "x ~❨ B , l ❩~> y 'in' c" with precedence 56 for
     
    183262  @{'block_in_code $c $x $B $l $y}.
    184263
     264notation > "x ~❨ B , l, r ❩~> y 'in' c" with precedence 56 for
     265  @{'bind_block_in_code $c $x $B $l $r $y}.
     266 
     267notation < "hvbox(x ~❨ B , l, r ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
     268  @{'bind_block_in_code $c $x $B $l $r $y}.
     269
    185270definition step_in_code ≝
    186271  λp,globals.λc : codeT p globals.λsrc : code_point p.λs : joint_step p globals.
     
    193278  stmt_at … c src = Some ? (final … s).
    194279
    195 let rec seq_list_in_code p globals (c : codeT p globals)
    196   (src : code_point p) (B : list (joint_seq p globals))
     280let rec step_list_in_code p globals (c : codeT p globals)
     281  (src : code_point p) (B : list (joint_step p globals))
    197282  (l : list (code_point p)) (dst : code_point p) on B : Prop ≝
    198283  match B with
     
    206291    [ nil ⇒ False
    207292    | cons mid rest ⇒
    208       step_in_code …  c src hd mid ∧ seq_list_in_code … c mid tl rest dst
     293      step_in_code …  c src hd mid ∧ step_list_in_code … c mid tl rest dst
    209294    ]
    210295  ].
    211296
    212 interpretation "seq list in code" 'block_in_code c x B l y = (seq_list_in_code ?? c x B l y).
    213 
    214 lemma seq_list_in_code_append :
     297interpretation "step list in code" 'block_in_code c x B l y = (step_list_in_code ?? c x B l y).
     298
     299lemma step_list_in_code_append :
    215300  ∀p,globals.∀c : codeT p globals.∀src,B1,l1,mid,B2,l2,dst.
    216301  src ~❨B1,l1❩~> mid in c → mid ~❨B2,l2❩~> dst in c →
     
    224309qed.
    225310
    226 lemma seq_list_in_code_append_inv :
     311lemma step_list_in_code_append_inv :
    227312  ∀p,globals.∀c : codeT p globals.∀src,B1,B2,l,dst.
    228313  src ~❨B1@B2,l❩~> dst in c →
    229314  ∃l1,mid,l2.l = l1 @ l2 ∧ src ~❨B1,l1❩~> mid in c ∧ mid ~❨B2,l2❩~> dst in c.
    230 #p #globals #c #src #B1 lapply src -src elim B1
     315#p #globals #c #src #B1 lapply src -src elim B1 -B1
    231316[ #src #B2 #l #dst #H %{[ ]} %{src} %{l} %{H} % %
    232317| #hd #tl #IH #src #B2 * [2: #mid #rest] #dst * #H1 #H2
     
    237322qed.
    238323
    239 definition seq_block_step_in_code ≝
    240   λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_step p g).λl,dst.
    241   ∃hd,tl.l = hd @ [tl] ∧
    242   src ~❨\fst B, l❩~> tl in c ∧ step_in_code … c tl (\snd B) dst.
    243 
    244 definition seq_block_fin_step_in_code ≝
    245   λp,g.λc:codeT p g.λsrc.λB : seq_block p g (joint_fin_step p).λl.λdst : unit.
     324lemma append_not_empty_r : ∀X,l1,l2.not_empty X l2 → not_empty ? (l1 @ l2).
     325#X #l1 cases l1 -l1 [ #l2 #K @K | #hd #tl #l2 #_ % ] qed.
     326
     327definition map_eval : ∀X,Y : Type[0].list (X → Y) → X → list Y ≝ λX,Y,l,x.map … (λf.f x) l.
     328
     329definition step_block_in_code ≝
     330  λp,g.λc : codeT p g.λsrc.λb : step_block p g.λl,dst.
     331  let 〈pref, last〉 ≝ split_on_last_ne … b in
     332  ∃mid.src ~❨map_eval … pref mid, l❩~> mid in c ∧ step_in_code ?? c mid (last mid) dst.
     333
     334lemma map_compose : ∀X,Y,Z,f,g.∀l : list X.map Y Z f (map X Y g l) = map … (f∘g) l.
     335#X #Y #Z #f #g #l elim l -l normalize // qed.
     336
     337lemma map_ext_eq : ∀X,Y,f,g.∀l : list X.(∀x.f x = g x) → map X Y f l = map X Y g l.
     338#X #Y #f #g #l #H elim l -l normalize // qed.
     339
     340lemma map_id : ∀X.∀l : list X.map X X (λx.x) l = l.
     341#X #l elim l -l normalize // qed.
     342
     343lemma coerced_step_list_in_code :
     344∀p : params.∀g,c,src.∀b : list (joint_step p g).∀l,dst.
     345step_block_in_code p g c src b l dst →
     346match b with
     347[ nil ⇒ step_in_code … c src (NOOP …) dst
     348| _ ⇒ step_list_in_code … c src b (l@[dst]) dst
     349].
     350#p #g #c #src @list_elim_left [2: #last #pref #_ ] #l #dst
     351[2: * #src' * cases l [2: #hd' #tl' *] whd in ⊢ (%→?); #EQ destruct #K @K ]
     352cases pref -pref [2: #hd #tl ]
     353whd in ⊢ (%→?);
     354[2: * #src' * cases l [2: #hd' #tl' *] whd in ⊢ (%→?); #EQ destruct #K %{K} % ]
     355whd in match (ensure_step_block ???);
     356<map_append
     357change with ((? :: ?) @ ?) in match (? :: ? @ ?);
     358>split_on_last_ne_def normalize nodelta * #mid *
     359whd in match (map_eval ????);
     360>map_compose >map_id #H1 #H2
     361@(step_list_in_code_append … H1) %{H2} %
     362qed.
     363
     364definition fin_block_in_code ≝
     365  λp,g.λc:codeT p g.λsrc.λB : fin_block p g.λl.λdst : unit.
    246366  ∃hd,tl.l = hd @ [tl] ∧
    247367  src ~❨\fst B, l❩~> tl in c ∧ fin_step_in_code … c tl (\snd B).
     368
     369interpretation "step block in code" 'block_in_code c x B l y = (step_block_in_code ?? c x B l y).
     370interpretation "fin block in code" 'block_in_code c x B l y = (fin_block_in_code ?? c x B l y).
     371
     372let rec bind_new_instantiates B X
     373  (x : X) (b : bind_new B X) (l : list B) on b : Prop ≝
     374  match b with
     375  [ bret B ⇒
     376    match l with
     377    [ nil ⇒ x = B
     378    | _ ⇒ False
     379    ]
     380  | bnew f ⇒
     381    match l with
     382    [ nil ⇒ False
     383    | cons r l' ⇒
     384      bind_new_instantiates B X x (f r) l'
     385    ]
     386  ].
     387
     388definition bind_step_block_in_code ≝
     389  λp,g.λc:codeT p g.λsrc.λB : bind_step_block p g.λlbls,regs.λdst.
     390  ∃b.bind_new_instantiates … b B regs ∧ src ~❨b, lbls❩~> dst in c.
     391
     392definition bind_fin_block_in_code ≝
     393  λp,g.λc:codeT p g.λsrc.λB : bind_fin_block p g.λlbls,regs.λdst.
     394  ∃b.bind_new_instantiates … b B regs ∧ src ~❨b, lbls❩~> dst in c.
     395
     396interpretation "bound step block in code" 'bind_block_in_code c x B l r y = (bind_step_block_in_code ?? c x B l r y).
     397interpretation "bound fin block in code" 'bind_block_in_code c x B l r y = (bind_fin_block_in_code ?? c x B l r y).
    248398
    249399(* generates ambiguity even if it shouldn't
  • src/joint/semantics.ma

    r2592 r2595  
    197197 
    198198  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
    199   ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars
     199  (* ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars *)
    200200  ; save_frame: call_kind → call_dest uns_pars → ident → state_pc st_pars → res (state st_pars)
    201201   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
     
    218218  }.
    219219
     220(*
    220221definition allocate_locals :
    221222  ∀p,F.∀sup : sem_unserialized_params p F.
     
    223224  λp,F,sup,l,st.
    224225  let r ≝ foldr … (allocate_locals_ … sup) (regs … st) l in
    225   set_regs … r st.
     226  set_regs … r st. *)
    226227
    227228definition helper_def_retrieve :
     
    526527
    527528definition eval_internal_call ≝
    528 λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args,st.
     529λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args.
     530λst : state p.
    529531! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
    530 ! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
    531 return allocate_locals … p (joint_if_locals … fn) st'.
     532setup_call … stack_size (joint_if_params … globals fn) args st.
    532533
    533534definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ].
  • src/joint/semantics_blocks.ma

    r2529 r2595  
    22include "joint/Traces.ma".
    33include "joint/semanticsUtils.ma".
     4
     5include "common/StatusSimulation.ma". (* for trace_any_any_free *)
    46
    57(* let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝
     
    1315  m_fold … (eval_seq_no_pc … (ev_genv … p) curr_id curr_fn).
    1416
    15 definition list_not_empty ≝ λA.λl : list A.match l with [ nil ⇒ false | _ ⇒ true ].
     17definition taaf_cons : ∀S : abstract_status.∀s1,s2,s3.
     18  as_execute S s1 s2 →
     19  as_classifier … s1 cl_other →
     20  ∀taaf : trace_any_any_free S s2 s3.
     21  (if taaf_non_empty … taaf then ¬as_costed … s2 else True) →
     22  trace_any_any_free S s1 s3 ≝
     23λS,s1,s2,s3,H,I,tl.
     24match tl return λs2,s3,tl.
     25  as_execute … s1 s2 →
     26  if taaf_non_empty … tl then ¬as_costed … s2 else True →
     27  trace_any_any_free S s1 s3
     28with
     29[ taaf_base s2 ⇒ λH.λ_.taaf_step … (taa_base …) H I
     30| taaf_step s2 s3 s4 taa H' I' ⇒
     31  λH,J.taaf_step … (taa_step … H I J taa) H' I'
     32| taaf_step_jump s2 s3 s4 taa H' I' K' ⇒
     33  λH,J.taaf_step_jump … (taa_step ???? H I J taa) H' I' K'
     34] H.
    1635
    17 let rec produce_trace_any_any
     36lemma taaf_cons_non_empty : ∀S,s1,s2,s3,H,I,tl,J.
     37bool_to_Prop (taaf_non_empty … (taaf_cons S s1 s2 s3 H I tl J)).
     38#S #s1 #s2 #s3 #H #I #tl lapply H -H cases tl
     39[ #s #H * % |*: #s2 #s3 #s4 #taa #H' #I' [2: #K'] #H #J % ]
     40qed.
     41
     42let rec produce_trace_any_any_free_aux
    1843  (p : evaluation_params)
    1944  (st : state_pc p)
     
    2651    return 〈curr_id, curr_fn〉 →
    2752  let src ≝ point_of_pc p (pc … st) in
    28   if list_not_empty ? b then
    29     ! x ← stmt_at ?? (joint_if_code … curr_fn) dst ; cost_label_of_stmt … x = None ?
    30   else
    31     True →
     53  (* disambiguation: select 3rd (step list in code) *)
    3254  src ~❨b, l❩~> dst in joint_if_code … curr_fn →
    33   All ? (λx.And (no_call … x) (no_cost_label … x)) b →
     55  All ? (no_cost_label …) b →
    3456  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
    35   trace_any_any (joint_abstract_status p) st
    36     (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst)) ≝  match b
    37   return λb.∀l,dst.?→?→?→?→?→?→?
     57  Σtaaf : trace_any_any_free (joint_abstract_status p) st
     58    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)).
     59  (not_empty … b ↔ bool_to_Prop (taaf_non_empty … taaf)) ≝
     60  match b
     61  return λb.∀l,dst.?→?→?→?→?→ Σtaaf.(not_empty ? b ↔ bool_to_Prop (taaf_non_empty … taaf))
    3862  with
    3963  [ nil ⇒
    40     λl,dst,st',fd_prf,dst_prf,in_code,all_other,EQ1.
    41     (taa_base (joint_abstract_status p) st)
    42     ⌈trace_any_any ??? ↦ ?⌉
     64    λl,dst,st',fd_prf,in_code,all_other,EQ1.
     65    «taaf_base (joint_abstract_status p) st
     66    ⌈trace_any_any_free ??? ↦ ?⌉,?»
    4367  | cons hd tl ⇒
    4468    λl.
    45     match l return λx.∀dst,st'.?→?→?→?→?→? with
    46     [ nil ⇒ λdst,st',fd_prf,dst_prf,in_code.⊥
     69    match l return λx.∀dst,st'.?→?→?→?→Σtaaf.(True ↔ bool_to_Prop (taaf_non_empty … taaf)) with
     70    [ nil ⇒ λdst,st',fd_prf,in_code.⊥
    4771    | cons mid rest ⇒
    48       λdst,st',fd_prf,dst_prf,in_code,all_other,EQ1.
     72      λdst,st',fd_prf,in_code,all_other,EQ1.
    4973      let mid_pc ≝ pc_of_point p (pc_block (pc … st)) mid in
    5074      match eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st
    5175      return λx.eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st = x →
    52       trace_any_any (joint_abstract_status p) st
    53         (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst)) with
    54       [ Value st_mid ⇒ λEQ2.
    55         let tr_tl ≝ produce_trace_any_any ?
    56             (mk_state_pc ? st_mid mid_pc)
    57             curr_id curr_fn tl rest dst ?????? in
    58         taa_step … tr_tl
     76      Σtaaf : trace_any_any_free (joint_abstract_status p) st
     77        (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)).
     78        (True ↔ bool_to_Prop (taaf_non_empty … taaf)) with
     79      [ OK st_mid ⇒ λEQ2.
     80        let tr_tl ≝ produce_trace_any_any_free_aux ?
     81            (mk_state_pc ? st_mid mid_pc (last_pop … st))
     82            curr_id curr_fn tl rest dst ????? in
     83        «taaf_cons … tr_tl ?,?»
    5984      | _ ⇒ λEQ2.⊥
    6085      ] (refl …)
    6186    ]
    62   ].
    63 [ whd in EQ1 : (??%%);
    64   cases l in in_code; whd in ⊢ (%→?); [2: #hd #tl * ] #EQ destruct
    65   >pc_of_point_of_pc cases st //
     87  ]. @hide_prf
     88[1,2: [2: % [*] generalize in ⊢ (?(???? (match % with [ _ ⇒ ?])) → ?); ]
     89  whd in EQ1 : (??%%);
     90  cases l in in_code; whd in ⊢ (%→?); [2,4: #hd #tl * ] #EQ destruct
     91  >pc_of_point_of_pc cases st // #a #b #c #e >(K ?? e) normalize nodelta *
    6692| @in_code
    67 |3,12: whd in EQ1 : (??%%); >EQ2 in EQ1; whd in ⊢ (??%?→?); #EQ1 destruct(EQ1)
     93|12: whd in EQ1 : (??%%); >EQ2 in EQ1; whd in ⊢ (??%?→?); #EQ1 destruct(EQ1)
     94|4: cases tr_tl -tr_tl #tr_tl cases tl in in_code all_other;
     95  [ #_ #_ * #_ cases (taaf_non_empty ????)
     96    [ #ABS cases (ABS I) | #_ % ]
     97  | #hd' #tl' ** #nxt * #EQstmt_at #EQ_nxt cases rest [*] #mid' #rest' *
     98    * #nxt' * #EQstmt_at' #EQ_nxt' #_ * #hd_other * #hd_other'
     99    #_ * #H #_ >(H I) % whd in ⊢ (%→?);
     100    whd in ⊢ (?(??%?)→?); whd in match (as_pc_of ??);
     101    >fetch_statement_eq [2: whd in match point_of_pc;
     102    normalize nodelta >point_of_offset_of_point @EQstmt_at' |3: @fd_prf |*:]
     103    normalize nodelta
     104    >(no_label_uncosted … hd_other') * #ABS @ABS %
     105  ]
     106|7: % [2: #_ %] * @taaf_cons_non_empty
    68107]
    69108change with (! y ← ? ; repeat_eval_seq_no_pc ????? = ?) in EQ1;
    70109>EQ2 in EQ1; >m_return_bind
    71110cases in_code -in_code * #nxt * #EQ_stmt_at #EQ_mid #rest_in_code
    72 cases all_other -all_other * #hd_no_call #hd_no_cost #tl_other
     111cases all_other -all_other #hd_no_cost #tl_other
    73112#EQ1
    74113try assumption
    75 [ whd whd in match eval_state; normalize nodelta
     114[2: whd whd in match eval_state; normalize nodelta
    76115  >(fetch_statement_eq … fd_prf EQ_stmt_at)
    77116  >m_return_bind
     
    79118  >EQ2 >m_return_bind
    80119  whd in match eval_statement_advance; normalize nodelta
    81   >(no_call_advance … hd_no_call)
    82120  whd in match next; normalize nodelta
    83121  whd in match succ_pc; normalize nodelta
    84122  >EQ_mid %
    85 | whd whd in ⊢ (??%?);
    86   >(fetch_statement_eq … fd_prf EQ_stmt_at) normalize nodelta
    87   @(no_call_other … hd_no_call)
    88 | whd in ⊢ (?%);
    89   whd in match as_label; normalize nodelta
    90   %* #H @H -H whd in ⊢ (??%?);
    91   whd in match (as_pc_of ??);
    92   inversion (fetch_statement ????) normalize nodelta
    93   [2: // ]
    94   ** #i' #f' #stmt' #EQ
    95   elim (fetch_statement_inv … EQ)
    96   >fd_prf
    97   whd in ⊢ (??%?→?); #EQ destruct(EQ)
    98   whd in ⊢ (%→?);
    99   whd in match (point_of_pc ??); >point_of_offset_of_point
    100   #EQ'
    101   cases tl in tl_other rest_in_code;
    102   [ * cases rest [2: #hd' #tl' * ] whd in ⊢ (%→?); #EQ destruct(EQ)
    103     >EQ' in dst_prf; >m_return_bind #H @H
    104   | #hd' #tl' ** #_ #hd_no_cost' #_
    105     cases rest [ * ] #mid' #rest' * * #nxt' * #EQ_stmt_at' #EQ_mid' #_
    106     >EQ_stmt_at' in EQ'; #EQ' destruct(EQ')
    107     @(no_label_uncosted … hd_no_cost')
    108   ]
    109 | >dst_prf cases (list_not_empty ??) %
    110 | normalize nodelta >point_of_pc_of_point assumption
     123|1: whd whd in ⊢ (??%?);
     124  >(fetch_statement_eq … fd_prf EQ_stmt_at) normalize nodelta %
     125|3: normalize nodelta >point_of_pc_of_point assumption
    111126]
    112127qed.
     128
     129definition produce_trace_any_any_free :
     130  ∀p : evaluation_params.
     131  ∀st : state_pc p.
     132  ∀curr_id,curr_fn.
     133  ∀b : list (joint_seq p (globals p)).
     134  ∀l : list (code_point p).
     135  ∀dst : code_point p.
     136  ∀st' : state p.
     137  fetch_internal_function … (ev_genv p) (pc_block (pc … st)) =
     138    return 〈curr_id, curr_fn〉 →
     139  let src ≝ point_of_pc p (pc … st) in
     140  (* disambiguation: select 3rd (step list in code) *)
     141  src ~❨b, l❩~> dst in joint_if_code … curr_fn →
     142  All ? (no_cost_label …) b →
     143  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
     144  trace_any_any_free (joint_abstract_status p) st
     145    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)) ≝
     146  λp,st,curr_id,curr_fn,b,l,dst,st',prf1,prf2,prf3,prf4.
     147  produce_trace_any_any_free_aux p st curr_id curr_fn b l dst st' prf1 prf2 prf3 prf4.
Note: See TracChangeset for help on using the changeset viewer.