Changeset 2155 for src/joint


Ignore:
Timestamp:
Jul 6, 2012, 11:25:43 AM (8 years ago)
Author:
tranquil
Message:

updates to blocks and RTLabs to RTL translation (which sidesteps pointer arithmetics issues for now)

Joint semantics and traces momentarily broken, concentrating on syntax now

Location:
src/joint
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint_paolo.ma

    r1976 r2155  
    77include "common/LabelledObjects.ma".
    88include "ASM/Util.ma".
    9 include "basics/deqsets.ma".
    10 include "basics/finset.ma". (* for DeqNat *)
     9include "common/StructuredTraces.ma".
    1110
    1211(* Here is the structure of parameter records (downward edges are coercions,
     
    3736params : adds type of code and related properties *)
    3837
     38inductive possible_flows : Type[0] ≝
     39| Labels : list label → possible_flows
     40| Call : possible_flows.
     41
    3942record step_params : Type[1] ≝
    4043 { acc_a_reg: Type[0] (* registers that will eventually need to be A *)
     
    5053 ; call_args: Type[0] (* arguments of function calls *)
    5154 ; call_dest: Type[0] (* possible destination of function computation *)
    52  ; ext_step: Type[0] (* other instructions not fitting in the general framework *)
    53  ; ext_step_labels : ext_step → list label
    54  ; ext_fin_stmt: Type[0] (* final instructions (e.g. tailcalls) not fitting in the general framework *)
    55  ; ext_fin_stmt_labels : ext_fin_stmt → list label
     55 (* other instructions not fitting in the general framework *)
     56 ; ext_seq : Type[0]
     57(* ; ext_branch : Type[0]
     58 ; ext_branch_labels : ext_branch → list label*)
     59 ; ext_call : Type[0]
     60 ; ext_tailcall : Type[0]
     61 (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *)
    5662 }.
    57  
    58 inductive joint_step (p:step_params) (globals: list ident): Type[0] ≝
    59   | COMMENT: String → joint_step p globals
    60   | COST_LABEL: costlabel → joint_step p globals
    61   | MOVE: pair_move p → joint_step p globals
    62   | POP: acc_a_reg p → joint_step p globals
    63   | PUSH: acc_a_arg p → joint_step p globals
    64   | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_step p globals
    65   | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_step p globals
    66   | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_step p globals
    67   | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_step p globals
     63
     64inductive joint_seq (p:step_params) (globals: list ident): Type[0] ≝
     65  | COMMENT: String → joint_seq p globals
     66  | COST_LABEL: costlabel → joint_seq p globals
     67  | MOVE: pair_move p → joint_seq p globals
     68  | POP: acc_a_reg p → joint_seq p globals
     69  | PUSH: acc_a_arg p → joint_seq p globals
     70  | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_seq p globals
     71  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_seq p globals
     72  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_seq p globals
     73  | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_seq p globals
    6874  (* int done with generic move *)
    69 (*| INT: generic_reg p → Byte → joint_step p globals *)
    70   | CLEAR_CARRY: joint_step p globals
    71   | SET_CARRY: joint_step p globals
    72   | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_step p globals
    73   | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_step p globals
    74   | CALL_ID: ident → call_args p → call_dest p → joint_step p globals
    75   | COND: acc_a_reg p → label → joint_step p globals
    76   | extension: ext_step p → joint_step p globals.
     75(*| INT: generic_reg p → Byte → joint_seq p globals *)
     76  | CLEAR_CARRY: joint_seq p globals
     77  | SET_CARRY: joint_seq p globals
     78  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_seq p globals
     79  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals
     80  | extension_seq : ext_seq p → joint_seq p globals.
    7781
    7882axiom EmptyString : String.
     
    9296interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
    9397
    94 coercion extension_to_step : ∀p,globals.∀s : ext_step p.joint_step p globals ≝
    95   extension on _s : ext_step ? to joint_step ??.
     98coercion extension_to_seq : ∀p,globals.∀s : ext_seq p.joint_seq p globals ≝
     99  extension_seq on _s : ext_seq ? to joint_seq ??.
     100
     101inductive joint_call (p : step_params) : Type[0] ≝
     102  | CALL_ID: ident → call_args p → call_dest p → joint_call p
     103  | extension_call : ext_call p → joint_call p.
     104
     105coercion extension_to_call : ∀p.∀s : ext_call p.joint_call p ≝
     106  extension_call on _s : ext_call ? to joint_call ?.
     107 
     108inductive joint_branch (p : step_params) : Type[0] ≝
     109  | COND: acc_a_reg p → label → joint_branch p
     110  (*| extension_branch : ext_branch p → joint_branch p*).
     111
     112(*coercion extension_to_branch : ∀p.∀s : ext_branch p.joint_branch p ≝
     113  extension_branch on _s : ext_branch ? to joint_branch ?.*)
     114
     115inductive joint_step (p : step_params) (globals : list ident) : Type[0] ≝
     116  | step_seq : joint_seq p globals → joint_step p globals
     117  | step_call : joint_call p → joint_step p globals
     118  | step_branch : joint_branch p → joint_step p globals.
     119
     120coercion seq_to_step : ∀p,globals.∀s : joint_seq p globals.joint_step p globals ≝
     121  step_seq on _s : joint_seq ?? to joint_step ??.
     122coercion call_to_step : ∀p,globals.∀s : joint_call p.joint_step p globals ≝
     123  step_call on _s : joint_call ? to joint_step ??.
     124coercion branch_to_step : ∀p,globals.∀s : joint_branch p.joint_step p globals ≝
     125  step_branch on _s : joint_branch ? to joint_step ??.
     126
     127definition step_flows ≝ λp,globals.λs : joint_step p globals.
     128  match s with
     129  [ step_seq _ ⇒ Labels … [ ]
     130  | step_call _ ⇒ Call
     131  | step_branch s ⇒
     132    match s with
     133    [ COND _ l ⇒ Labels … [l]
     134    (*| extension_branch s' ⇒ Labels … (ext_branch_labels … s')*)
     135    ]
     136  ].
    96137
    97138definition step_labels ≝
    98139  λp, globals.λs : joint_step p globals.
    99     match s with
    100     [ COND _ l ⇒ [l]
    101     | extension ext_s ⇒ ext_step_labels ? ext_s
    102     | _ ⇒ [ ]
     140    match step_flows … s with
     141    [ Labels lbls ⇒ lbls
     142    | Call ⇒ [ ]
    103143    ].
    104144
     
    106146    (label → Prop) → joint_step p globals → Prop ≝
    107147λp,g,P,inst. All … P (step_labels … inst).
    108  
     148
     149definition step_classifier :
     150  ∀p : step_params.∀globals.
     151    joint_step p globals → status_class ≝ λp,g,s.
     152  match s with
     153  [ step_seq _ ⇒ cl_other
     154  | step_call _ ⇒ cl_call
     155  | step_branch _ ⇒ cl_jump
     156  ].
     157
    109158record funct_params : Type[1] ≝
    110159  { resultT : Type[0]
     
    117166 }.
    118167
    119 
    120168record unserialized_params : Type[1] ≝
    121169 { u_inst_pars :> step_params
     
    129177  }.
    130178
    131 inductive joint_fin_step (p: stmt_params) (globals: list ident): Type[0] ≝
    132   | GOTO: label → joint_fin_step p globals
    133   | RETURN: joint_fin_step p globals
    134   | extension_fin : ext_fin_stmt p → joint_fin_step p globals.
     179inductive joint_fin_step (p: step_params): Type[0] ≝
     180  | GOTO: label → joint_fin_step p
     181  | RETURN: joint_fin_step p
     182  | tailcall : ext_tailcall p → joint_fin_step p.
     183
     184definition fin_step_flows ≝ λp.λs : joint_fin_step p.
     185  match s with
     186  [ GOTO l ⇒ Labels … [l]
     187  | _ ⇒ Labels … [ ] (* tailcalls will need to be integrated in structured traces *)
     188  ].
     189
     190definition fin_step_labels ≝
     191  λp.λs : joint_fin_step p.
     192    match fin_step_flows … s with
     193    [ Labels lbls ⇒ lbls
     194    | Call ⇒ [ ]
     195    ].
     196
     197definition fin_step_classifier :
     198  ∀p : stmt_params.
     199    joint_fin_step p → status_class
     200  ≝ λp,s.
     201  match s with
     202  [ GOTO _ ⇒ cl_other
     203  | _ ⇒ cl_return
     204  ].
    135205
    136206inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
    137207  | sequential: joint_step p globals → succ p → joint_statement p globals
    138   | final: joint_fin_step p globals → joint_statement p globals.
    139 
    140 coercion extension_fin_to_fin_step : ∀p : stmt_params.∀globals.
    141   ∀s : ext_fin_stmt p.joint_fin_step p globals ≝
    142   extension_fin on _s : ext_fin_stmt ? to joint_fin_step ??.
     208  | final: joint_fin_step p → joint_statement p globals.
     209
     210definition stmt_classifier :
     211  ∀p : stmt_params.∀globals.
     212    joint_statement p globals → status_class
     213  ≝ λp,g,s.
     214  match s with
     215  [ sequential stp _ ⇒ step_classifier p g stp
     216  | final stp ⇒ fin_step_classifier p stp
     217  ].
     218
     219coercion extension_fin_to_fin_step : ∀p : stmt_params.
     220  ∀s : ext_tailcall p.joint_fin_step p ≝
     221  tailcall on _s : ext_tailcall ? to joint_fin_step ?.
    143222
    144223coercion fin_step_to_stmt : ∀p : stmt_params.∀globals.
    145   ∀s : joint_fin_step p globals.joint_statement p globals ≝
    146   final on _s : joint_fin_step ?? to joint_statement ??.
     224  ∀s : joint_fin_step p.joint_statement p globals ≝
     225  final on _s : joint_fin_step ? to joint_statement ??.
    147226
    148227record params : Type[1] ≝
    149228 { stmt_pars :> stmt_params
    150229 ; codeT: list ident → Type[0]
    151  ; code_point : DeqSet
     230 ; code_point : Type[0]
    152231 ; stmt_at : ∀globals.codeT globals → code_point → option (joint_statement stmt_pars globals)
    153232 ; point_of_label : ∀globals.codeT globals → label → option code_point
     
    192271  [ Some pt ⇒ code_has_point … c pt
    193272  | None ⇒ false
    194   ].
    195 
    196 definition fin_step_labels ≝
    197   λp,globals.λs : joint_fin_step p globals.
    198   match s with
    199   [ GOTO l ⇒ [ l ]
    200   | RETURN ⇒ [ ]
    201   | extension_fin c ⇒ ext_fin_stmt_labels … c
    202273  ].
    203274
     
    254325
    255326record lin_params : Type[1] ≝
    256   { l_u_pars :> unserialized_params }.
     327  { l_u_pars : unserialized_params }.
    257328 
    258329lemma index_of_label_length : ∀tag,A,lbl,l.occurs_exactly_once ?? lbl l → lt (index_of_label tag A lbl l) (|l|).
     
    290361  λlp : lin_params.
    291362     mk_params
    292       (mk_stmt_params lp unit (λ_.None ?))
     363      (mk_stmt_params (l_u_pars lp) unit (λ_.None ?))
    293364    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
    294     (* code_point ≝ *)DeqNat
     365    (* code_point ≝ *)
    295366    (* stmt_at ≝ *)(λglobals,code,point.! ls ← nth_opt ? point code ; return \snd ls)
    296367    (* point_of_label ≝ *)(λglobals,c,lbl.
     
    325396
    326397record graph_params : Type[1] ≝
    327   { g_u_pars :> unserialized_params }.
     398  { g_u_pars : unserialized_params }.
    328399
    329400(* One common instantiation of params via Graphs of joint_statements
     
    332403  λgp : graph_params.
    333404     mk_params
    334       (mk_stmt_params gp label (Some ?))
     405      (mk_stmt_params (g_u_pars gp) label (Some ?))
    335406    (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
    336     (* code_point ≝ *)(Deq_identifier LabelTag)
     407    (* code_point ≝ *)label
    337408    (* stmt_at ≝ *)(λglobals,code.lookup LabelTag ? code)
    338409    (* point_of_label ≝ *)(λ_.λ_.λlbl.return lbl)
  • src/joint/TranslateUtils_paolo.ma

    r1882 r2155  
    11include "joint/Joint_paolo.ma".
    2 include "utilities/bindLists.ma".
     2include "joint/blocks.ma".
    33
    44(* general type of functions generating fresh things *)
     
    3535
    3636(* insert into a graph a block of instructions *)
    37 let rec adds_graph
     37let rec adds_graph_list
    3838  (g_pars: graph_params)
    3939  (globals: list ident)
    40   (insts: list (joint_step g_pars globals))
     40  (insts: list (joint_seq g_pars globals))
    4141  (src : label)
    42   (dest : label)
    43   (def: joint_internal_function … g_pars) on insts
     42  (def: joint_internal_function … g_pars) on insts
     43  : (joint_internal_function … g_pars) × label
    4444  match insts with
    45   [ nil ⇒ add_graph … src (GOTO … dest) def
     45  [ nil ⇒ 〈def, src〉
    4646  | cons instr others ⇒
    47     match others with
    48     [ nil ⇒ (* only one instruction *)
    49       add_graph … src (sequential … instr dest) def
    50     | _ ⇒ (* need to generate label *)
    51       let 〈def, tmp_lbl〉 ≝ fresh_label … def in
    52       adds_graph g_pars globals others tmp_lbl dest
    53         (add_graph … src (sequential … instr tmp_lbl) def)
    54     ]
     47    let 〈def, mid〉 ≝ fresh_label … def in
     48    let def ≝ add_graph … src (sequential … instr mid) def in
     49    adds_graph_list g_pars globals others mid def
     50  ].
     51
     52definition adds_graph :
     53  ∀g_pars : graph_params.
     54  ∀globals: list ident.
     55  ∀b : seq_block g_pars globals (joint_step g_pars globals) +
     56       seq_block g_pars globals (joint_fin_step g_pars).
     57  label → if is_inl … b then label else unit →
     58  joint_internal_function … g_pars → joint_internal_function … g_pars ≝
     59  λg_pars,globals,insts,src.
     60  match insts return λx.if is_inl … x then ? else ? → ? → ? with
     61  [ inl b ⇒ λdst,def.
     62    let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
     63    add_graph … mid (sequential … (\snd b) dst) def
     64  | inr b ⇒ λdst,def.
     65    let 〈def, mid〉 ≝ adds_graph_list … (\fst b) src def in
     66    add_graph … mid (final … (\snd b)) def
    5567  ].
    5668
     
    6072  (* fresh register creation *)
    6173  freshT globals g_pars (localsT … g_pars) →
    62   ∀insts: bind_list (localsT … g_pars) (joint_step g_pars globals).
    63   ∀src : label.
    64   ∀dest : label.
     74  ∀b : bind_seq_block g_pars globals (joint_step g_pars globals) +
     75       bind_seq_block g_pars globals (joint_fin_step g_pars).
     76  label → if is_inl … b then label else unit →
    6577  joint_internal_function globals g_pars →
    6678  joint_internal_function globals g_pars ≝
    67   λg_pars,globals,fresh_r,insts,src,dest,def.
    68   let 〈def', stmts〉 ≝ bcompile … fresh_r insts def in
    69   adds_graph … stmts src dest def'.
     79  λg_pars,globals,fresh_r,insts,src.
     80  match insts return λx.if is_inl … x then ? else ? → ? → ? with
     81  [ inl b ⇒ λdst,def.
     82    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
     83    adds_graph … (inl … stmts) src dst def
     84  | inr b ⇒ λdst,def.
     85    let 〈def, stmts〉 ≝ bcompile ??? fresh_r b def in
     86    adds_graph … (inr … stmts) src dst def
     87  ].
    7088
    7189(* translation with inline fresh register allocation *)
     
    7593  (* fresh register creation *)
    7694  freshT globals dst_g_pars (localsT dst_g_pars) →
    77   (* function dictating the translation *)
    78   (label → joint_step src_g_pars globals →
    79     bind_list (localsT dst_g_pars) (joint_step dst_g_pars globals)
    80     (* this can be added to allow redirections: × label *)) →
    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))) →
    8695  (* initialized function definition with empty graph *)
    8796  joint_internal_function globals dst_g_pars →
     97  (* functions dictating the translation *)
     98  (label → joint_step src_g_pars globals →
     99    bind_seq_block dst_g_pars globals (joint_step dst_g_pars globals)) →
     100  (label → joint_fin_step src_g_pars →
     101    bind_seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
    88102  (* source function *)
    89103  joint_internal_function globals src_g_pars →
    90104  (* destination function *)
    91   joint_internal_function globals dst_g_pars ≝ 
    92   λsrc_g_pars,dst_g_pars,globals,fresh_reg,trans,trans',empty,def.
     105  joint_internal_function globals dst_g_pars ≝
     106  λsrc_g_pars,dst_g_pars,globals,fresh_reg,empty,trans_step,trans_fin_step,def.
    93107  let f : label → joint_statement (src_g_pars : params) globals →
    94108    joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝
    95109    λlbl,stmt,def.
    96110    match stmt with
    97     [ sequential inst next ⇒ b_adds_graph … fresh_reg (trans lbl inst) lbl next def
    98     | GOTO next ⇒ add_graph … lbl (GOTO … next) def
    99     | RETURN ⇒ add_graph … lbl (RETURN …) 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)
     111    [ sequential inst next ⇒
     112      b_adds_graph … fresh_reg (inl … (trans_step lbl inst)) lbl next def
     113    | final inst ⇒
     114      b_adds_graph … fresh_reg (inr … (trans_fin_step lbl inst)) lbl it def
    105115    ] in
    106116  foldi … f (joint_if_code … def) empty.
    107  
     117(* 
    108118(* translation without register allocation *)
    109119definition graph_translate :
     
    137147    ] in
    138148  foldi ??? f (joint_if_code ?? def) empty.
    139 
     149*)
     150(*
    140151definition graph_to_lin_statement :
    141152  ∀p : unserialized_params.∀globals.
    142153  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
     154  λp,globals,stmt.match stmt with
    144155  [ sequential c _ ⇒ sequential … c it
    145   | GOTO l ⇒ GOTO … l
    146   | RETURN ⇒ RETURN …
    147   | extension_fin c ⇒ extension_fin … c
     156  | final c ⇒
     157    final ?? match c return λx.joint_fin_step (mk_lin_params p) globals with
     158    [ GOTO l ⇒ GOTO … l
     159    | RETURN ⇒ RETURN …
     160    | extension_fin c ⇒ extension_fin ?? c
     161    ]
    148162  ].
    149163
     
    152166  stmt_labels … (graph_to_lin_statement p globals s) =
    153167  stmt_explicit_labels … s.
    154 #p#globals * //
     168#p#globals * [//] * //
    155169qed.
    156170
     
    216230(*----------------------------*)⊢
    217231list lo ≡ codeT lp globals.
     232
    218233
    219234definition graph_visit_ret_type ≝ λp,globals.λg : codeT (mk_graph_params p) globals.
     
    791806#f_out * #f_out_closed #H assumption
    792807qed.
    793 
    794  
     808*) 
    795809
    796810     
  • src/joint/blocks.ma

    r2042 r2155  
    11include "joint/Joint_paolo.ma".
    2 include "utilities/bind_new.ma".
    3 
    4 definition uncurry_helper : ∀A,B,C : Type[0].(A → B → C) → (A×B) → C ≝
    5   λA,B,C,f,p.f (\fst p) (\snd p).
    6 
    7 inductive stmt_type : Type[0] ≝
    8   | SEQ : stmt_type
    9   | FIN : stmt_type.
    10 
    11 definition stmt_type_if : ∀A : Type[1].stmt_type → A → A → A ≝
    12   λA,t,x,y.match t with [ SEQ ⇒ x | FIN ⇒ y ].
    13 
    14 definition block_cont ≝ λp : params.λglobals,ty.
    15   (list (joint_step p globals)) ×
    16     (stmt_type_if ? ty (joint_step p) (joint_fin_step p) globals).
    17 
    18 definition Skip : ∀p,globals.block_cont p globals SEQ ≝
    19   λp,globals.〈[ ], NOOP …〉.
    20 
    21 definition instr_block ≝ λp : params.λglobals,ty.
    22   bind_new (localsT p) (block_cont p globals ty).
    23 unification hint 0 ≔ p, globals, ty;
    24 B ≟ block_cont p globals ty, R ≟ localsT p
     2include "utilities/bindLists.ma".
     3
     4inductive block_step (p : stmt_params) (globals : list ident) : Type[0] ≝
     5  | block_seq : joint_seq p globals → block_step p globals
     6  | block_skip : label → block_step p globals.
     7
     8definition if_seq : ∀p,globals.∀A:Type[2].block_step p globals → A → A → A ≝
     9λp,g,A,s.match s with
     10[ block_seq _ ⇒ λx,y.x
     11| _ ⇒ λx,y.y
     12].
     13
     14definition stmt_of_block_step : ∀p : stmt_params.∀globals.
     15  ∀s : block_step p globals.if_seq … s (succ p) unit → joint_statement p globals ≝
     16  λp,g,s.match s return λx.if_seq ??? x ?? → joint_statement ?? with
     17  [ block_seq s' ⇒ λnxt.sequential … s' nxt
     18  | block_skip l ⇒ λ_.GOTO … l
     19  ].
     20
     21definition seq_to_block_step_list : ∀p : stmt_params.∀globals.
     22  list (joint_seq p globals) →
     23  list (block_step p globals) ≝ λp,globals.map ?? (block_seq ??).
     24
     25coercion block_step_from_seq_list : ∀p : stmt_params.∀globals.
     26  ∀l:list (joint_seq p globals).
     27  list (block_step p globals) ≝
     28  seq_to_block_step_list
     29  on _l:list (joint_seq ??)
     30  to list (block_step ??).
     31
     32definition is_inr : ∀A,B.A + B → bool ≝ λA,B,x.match x with
     33  [ inl _ ⇒ true
     34  | inr _ ⇒ false
     35  ].
     36definition is_inl : ∀A,B.A + B → bool ≝ λA,B,x.match x with
     37  [ inl _ ⇒ true
     38  | inr _ ⇒ false
     39  ].
     40
     41definition skip_block ≝ λp,globals,A.
     42  (list (block_step p globals)) × A.
     43
     44definition seq_block ≝ λp : stmt_params.λglobals,A.
     45  (list (joint_seq p globals)) × A.
     46
     47definition seq_to_skip_block :
     48  ∀p,g,A.seq_block p g A → skip_block p g A
     49 ≝ λp,g,A,b.〈\fst b, \snd b〉.
     50
     51coercion skip_from_seq_block :
     52  ∀p,g,A.∀b : seq_block p g A.skip_block p g A ≝
     53  seq_to_skip_block on _b : seq_block ??? to skip_block ???.
     54
     55definition bind_seq_block ≝ λp : stmt_params.λglobals,A.
     56  bind_new (localsT p) (seq_block p globals A).
     57unification hint 0 ≔ p : stmt_params, g, X;
     58R ≟ localsT p,
     59P ≟ seq_block p g X
    2560(*---------------------------------------*)⊢
    26 instr_block p globals ty ≡ bind_new R B.
    27 
    28 definition block_cont_append :
    29   ∀p,g,ty.
    30   ∀b1 : block_cont p g SEQ.
    31   ∀b2 : block_cont p g ty.
    32   block_cont p g ty ≝
    33   λp,globals,ty,b1,b2.〈\fst b1 @ \snd b1 :: \fst b2, \snd b2〉.
    34 
    35 definition block_cont_cons ≝ λp,g,ty,x.λb : block_cont p g ty.〈x :: \fst b,\snd b〉.
    36 
    37 interpretation "block contents cons" 'cons x b = (block_cont_cons ??? x b).
    38 interpretation "block contents append" 'append b1 b2 = (block_cont_append ??? b1 b2).
    39 
    40 definition step_to_block : ∀p : params.∀g.
    41   joint_step p g → block_cont p g SEQ ≝ λp,g,s.〈[ ], s〉.
    42 
    43 definition fin_step_to_block : ∀p : params.∀g.
    44   joint_fin_step p g → block_cont p g FIN ≝ λp,g,s.〈[ ], s〉.
    45 
    46 coercion block_from_step : ∀p : params.∀g.∀s : joint_step p g.
    47   block_cont p g SEQ ≝ step_to_block on _s : joint_step ?? to block_cont ?? SEQ.
    48 
    49 coercion block_from_fin_step : ∀p : params.∀g.∀s : joint_fin_step p g.
    50   block_cont p g FIN ≝ fin_step_to_block
    51   on _s : joint_fin_step ?? to block_cont ?? FIN.
    52 
    53 definition block_cons :
    54   ∀p : params.∀globals,ty.
    55   joint_step p globals → instr_block p globals ty → instr_block p globals ty
    56   ≝ λp,globals,ty,x.m_map … (block_cont_cons … x).
    57 
    58 definition block_append :
    59   ∀p : params.∀globals,ty.
    60   instr_block p globals SEQ → instr_block p globals ty → instr_block p globals ty ≝
    61   λp,globals,ty.m_bin_op … (block_cont_append …).
    62 
    63 interpretation "instruction block cons" 'cons x b = (block_cons ??? x b).
    64 interpretation "instruction block append" 'append b1 b2 = (block_append ??? b1 b2).
    65 
    66 let rec is_block_instance (p : params) g ty (b : instr_block p g ty) (l : list (localsT p)) (b' : block_cont p g ty) on b : Prop ≝
     61bind_seq_block p g X ≡ bind_new R P.
     62
     63definition bind_seq_list ≝ λp : stmt_params.λglobals.
     64  bind_new (localsT p) (list (joint_seq p globals)).
     65unification hint 0 ≔ p : stmt_params, g;
     66R ≟ localsT p,
     67S ≟ joint_seq p g,
     68L ≟ list S
     69(*---------------------------------------*)⊢
     70bind_seq_list p g ≡ bind_new R L.
     71
     72definition bind_skip_block ≝ λp : stmt_params.λglobals,A.
     73  bind_new (localsT p) (skip_block p globals A).
     74unification hint 0 ≔ p : stmt_params, g, A;
     75B ≟ skip_block p g A, R ≟ localsT p
     76(*---------------------------------------*)⊢
     77bind_skip_block p g A ≡ bind_new R B.
     78
     79definition bind_seq_to_skip_block :
     80  ∀p,g,A.bind_seq_block p g A → bind_skip_block p g A ≝
     81  λp,g,A.m_map ? (seq_block p g A) (skip_block p g A)
     82    (λx.x).
     83
     84coercion bind_skip_from_seq_block :
     85  ∀p,g,A.∀b:bind_seq_block p g A.bind_skip_block p g A ≝
     86  bind_seq_to_skip_block on _b : bind_seq_block ??? to bind_skip_block ???.
     87(*
     88definition block_classifier ≝
     89  λp,g.λb : other_block p g.
     90  seq_or_fin_step_classifier ?? (\snd b).
     91*)
     92
     93let rec split_on_last A (dflt : A) (l : list A) on l : (list A) × A ≝
     94match 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
     105lemma 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]
     117qed.
     118
     119definition seq_block_from_seq_list :
     120∀p : stmt_params.∀g.list (joint_seq p g) → seq_block p g (joint_step p g) ≝
     121λp,g,l.let 〈pre,post〉 ≝ split_on_last … (NOOP ??) l in 〈pre, (post : joint_step ??)〉.
     122
     123definition bind_seq_block_from_bind_seq_list :
     124  ∀p : stmt_params.∀g.bind_new (localsT p) (list (joint_seq p g)) →
     125    bind_seq_block p g (joint_step p g) ≝ λp.λg.m_map … (seq_block_from_seq_list …).
     126
     127definition bind_seq_block_step :
     128  ∀p,g.bind_seq_block p g (joint_step p g) →
     129    bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝
     130  λp,g.inl ….
     131coercion bind_seq_block_from_step :
     132  ∀p,g.∀b:bind_seq_block p g (joint_step p g).
     133    bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝
     134  bind_seq_block_step on _b : bind_seq_block ?? (joint_step ??) to
     135    bind_seq_block ?? (joint_step ??) + bind_seq_block ?? (joint_fin_step ?).
     136
     137definition bind_seq_block_fin_step :
     138  ∀p,g.bind_seq_block p g (joint_fin_step p) →
     139    bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝
     140  λp,g.inr ….
     141coercion bind_seq_block_from_fin_step :
     142  ∀p,g.∀b:bind_seq_block p g (joint_fin_step p).
     143    bind_seq_block p g (joint_step p g) + bind_seq_block p g (joint_fin_step p) ≝
     144  bind_seq_block_fin_step on _b : bind_seq_block ?? (joint_fin_step ?) to
     145    bind_seq_block ?? (joint_step ??) + bind_seq_block ?? (joint_fin_step ?).
     146
     147definition seq_block_bind_seq_block :
     148  ∀p : stmt_params.∀g,A.seq_block p g A → bind_seq_block p g A ≝ λp,g,A.bret ….
     149coercion seq_block_to_bind_seq_block :
     150  ∀p : stmt_params.∀g,A.∀b:seq_block p g A.bind_seq_block p g A ≝
     151  seq_block_bind_seq_block
     152  on _b : seq_block ??? to bind_seq_block ???.
     153
     154definition joint_step_seq_block : ∀p : stmt_params.∀g.joint_step p g → seq_block p g (joint_step p g) ≝
     155  λp,g,x.〈[ ], x〉.
     156coercion joint_step_to_seq_block : ∀p : stmt_params.∀g.∀b : joint_step p g.seq_block p g (joint_step p g) ≝
     157  joint_step_seq_block on _b : joint_step ?? to seq_block ?? (joint_step ??).
     158
     159definition joint_fin_step_seq_block : ∀p : stmt_params.∀g.joint_fin_step p → seq_block p g (joint_fin_step p) ≝
     160  λp,g,x.〈[ ], x〉.
     161coercion joint_fin_step_to_seq_block : ∀p : stmt_params.∀g.∀b : joint_fin_step p.seq_block p g (joint_fin_step p) ≝
     162  joint_fin_step_seq_block on _b : joint_fin_step ? to seq_block ?? (joint_fin_step ?).
     163
     164definition seq_list_seq_block :
     165  ∀p:stmt_params.∀g.list (joint_seq p g) → seq_block p g (joint_step p g) ≝
     166  λp,g,l.let pr ≝ split_on_last … (NOOP ??) l in 〈\fst pr, \snd pr〉.
     167coercion seq_list_to_seq_block :
     168  ∀p:stmt_params.∀g.∀l:list (joint_seq p g).seq_block p g (joint_step p g) ≝
     169  seq_list_seq_block on _l : list (joint_seq ??) to seq_block ?? (joint_step ??).
     170
     171definition bind_seq_list_bind_seq_block :
     172  ∀p:stmt_params.∀g.bind_new (localsT p) (list (joint_seq p g)) → bind_seq_block p g (joint_step p g) ≝
     173  λp,g.m_map ??? (λx : list (joint_seq ??).(x : seq_block ???)).
     174
     175coercion bind_seq_list_to_bind_seq_block :
     176  ∀p:stmt_params.∀g.∀l:bind_new (localsT p) (list (joint_seq p g)).bind_seq_block p g (joint_step p g) ≝
     177  bind_seq_list_bind_seq_block on _l : bind_new ? (list (joint_seq ??)) to bind_seq_block ?? (joint_step ??).
     178
     179(*
     180
     181definition seq_block_append :
     182  ∀p,g.
     183  ∀b1 : Σb.is_safe_block p g b.
     184  ∀b2 : seq_block p g.
     185  seq_block p g ≝ λp,g,b1,b2.
     186  〈match b1 with
     187  [ mk_Sig instr prf ⇒
     188    match \snd instr return λx.bool_to_Prop (is_inl … x) ∧ seq_or_fin_step_classifier … x = ? → ? with
     189    [ inl i ⇒ λprf.\fst b1 @ i :: \fst b2
     190    | inr _ ⇒ λprf.⊥
     191    ] prf
     192  ],\snd b2〉.
     193  cases prf #H1 #H2 assumption
     194  qed.
     195
     196definition other_block_append :
     197  ∀p,g.
     198  (Σb.block_classifier ?? b = cl_other) →
     199  other_block p g →
     200  other_block p g ≝ λp,g,b1,b2.
     201  〈\fst b1 @ «\snd b1, pi2 … b1» :: \fst b2, \snd b2〉.
     202
     203definition seq_block_cons : ∀p : stmt_params.∀g.(Σs.step_classifier p g s = cl_other) →
     204  seq_block p g → seq_block p g ≝
     205  λp,g,x,b.〈x :: \fst b,\snd b〉.
     206definition other_block_cons : ∀p,g.
     207  (Σs.seq_or_fin_step_classifier p g s = cl_other) → other_block p g →
     208  other_block p g ≝
     209  λp,g,x,b.〈x :: \fst b,\snd b〉.
     210
     211interpretation "seq block cons" 'cons x b = (seq_block_cons ?? x b).
     212interpretation "other block cons" 'vcons x b = (other_block_cons ?? x b).
     213interpretation "seq block append" 'append b1 b2 = (seq_block_append ?? b1 b2).
     214interpretation "other block append" 'vappend b1 b2 = (other_block_append ?? b1 b2).
     215
     216definition step_to_block : ∀p,g.
     217  seq_or_fin_step p g → seq_block p g ≝ λp,g,s.〈[ ], s〉.
     218
     219coercion block_from_step : ∀p,g.∀s : seq_or_fin_step p g.
     220  seq_block p g ≝ step_to_block on _s : seq_or_fin_step ?? to seq_block ??.
     221
     222definition bind_seq_block_cons :
     223  ∀p : stmt_params.∀g,is_seq.
     224  (Σs.step_classifier p g s = cl_other) → bind_seq_block p g is_seq →
     225  bind_seq_block p g is_seq ≝
     226  λp,g,is_seq,x.m_map ??? (λb.〈x::\fst b,\snd b〉).
     227
     228definition bind_other_block_cons :
     229  ∀p,g.(Σs.seq_or_fin_step_classifier p g s = cl_other) → bind_other_block p g → bind_other_block p g ≝
     230  λp,g,x.m_map … (other_block_cons … x).
     231
     232let rec bind_pred_aux B X (P : X → Prop) (c : bind_new B X) on c : Prop ≝
     233  match c with
     234  [ bret x ⇒ P x
     235  | bnew f ⇒ ∀b.bind_pred_aux B X P (f b)
     236  ].
     237
     238let rec bind_pred_inj_aux B X (P : X → Prop) (c : bind_new B X) on c :
     239  bind_pred_aux B X P c → bind_new B (Σx.P x) ≝
     240  match c return λx.bind_pred_aux B X P x → bind_new B (Σx.P x) with
     241  [ bret x ⇒ λprf.return «x, prf»
     242  | bnew f ⇒ λprf.bnew … (λx.bind_pred_inj_aux B X P (f x) (prf x))
     243  ].
     244
     245definition bind_pred ≝ λB.
     246  mk_InjMonadPred (BindNew B)
     247    (mk_MonadPred ?
     248      (bind_pred_aux B)
     249      ???)
     250    (λX,P,c_sig.bind_pred_inj_aux B X P c_sig (pi2 … c_sig))
     251    ?.
     252[ #X #P #Q #H #y elim y [ #x @H | #f #IH #G #b @IH @G]
     253| #X #Y #Pin #Pout #m elim m [#x | #f #IH] #H #g #G [ @G @H | #b @(IH … G) @H]
     254| #X #P #x #Px @Px
     255| #X #P * #m elim m [#x | #f #IH] #H [ % | @bnew_proper #b @IH]
     256]
     257qed.
     258
     259definition bind_seq_block_append :
     260  ∀p,g,is_seq.(Σb : bind_seq_block p g true.bind_pred ? (λb.step_classifier p g (\snd b) = cl_other) b) →
     261  bind_seq_block p g is_seq → bind_seq_block p g is_seq ≝
     262  λp,g,is_seq,b1,b2.
     263    !«p, prf» ← mp_inject … b1;
     264    !〈post, last〉 ← b2;
     265    return 〈\fst p @ «\snd p, prf» :: post, last〉.
     266
     267definition bind_other_block_append :
     268  ∀p,g.(Σb : bind_other_block p g.bind_pred ?
     269    (λx.block_classifier ?? x = cl_other) b) →
     270  bind_other_block p g → bind_other_block p g ≝
     271  λp,g,b1.m_bin_op … (other_block_append ??) (mp_inject … b1).
     272
     273interpretation "bind seq block cons" 'cons x b = (bind_seq_block_cons ??? x b).
     274interpretation "bind other block cons" 'vcons x b = (bind_other_block_cons ?? x b).
     275interpretation "bind seq block append" 'append b1 b2 = (bind_seq_block_append ??? b1 b2).
     276interpretation "bind other block append" 'vappend b1 b2 = (bind_other_block_append ?? b1 b2).
     277
     278let rec instantiates_to B X
     279  (b : bind_new B X) (l : list B) (x : X) on b : Prop ≝
    67280  match b with
    68281  [ bret B ⇒
    69282    match l with
    70     [ nil ⇒ B = b'
    71     | cons _ _ ⇒ False
     283    [ nil ⇒ x = B
     284    | _ ⇒ False
    72285    ]
    73286  | bnew f ⇒
     
    75288    [ nil ⇒ False
    76289    | cons r l' ⇒
    77       is_block_instance p g ty (f r) l' b'
     290      instantiates_to B X (f r) l' x
    78291    ]
    79292  ].
    80293
    81 lemma is_block_instance_append : ∀p,globals,ty,b1,b2,l1,l2,b1',b2'.
    82   is_block_instance p globals SEQ b1 l1 b1' →
    83   is_block_instance p globals ty b2 l2 b2' →
    84   is_block_instance p globals ty (b1 @ b2) (l1 @ l2) (b1' @ b2').
    85 #p#globals#ty #b1 elim b1
    86 [ #B1 | #f1 #IH1 ] #b2 * [2,4: #r1 #l1' ] #l2 #b1' #b2' [1,4: *]
    87 normalize in ⊢ (%→?);
     294lemma instantiates_to_bind_pred :
     295  ∀B,X,P,b,l,x.instantiates_to B X b l x → bind_pred B P b → P x.
     296#B #X #P #b elim b
     297[ #x * [ #y #EQ >EQ normalize // | #hd #tl #y *]
     298| #f #IH * [ #y * | #hd #tl normalize #b #H #G @(IH … H) @G ]
     299]
     300qed.
     301
     302lemma seq_block_append_proof_irr :
     303  ∀p,g,b1,b1',b2.pi1 ?? b1 = pi1 ?? b1' →
     304    seq_block_append p g b1 b2 = seq_block_append p g b1' b2.
     305#p #g * #b1 #b1prf * #b1' #b1prf' #b2 #EQ destruct(EQ) %
     306qed.
     307
     308lemma other_block_append_proof_irr :
     309  ∀p,g,b1,b1',b2.pi1 ?? b1 = pi1 ?? b1' →
     310  other_block_append p g b1 b2 = other_block_append p g b1' b2.
     311#p #g * #b1 #b1prf * #b1' #b1prf' #b2 #EQ destruct(EQ) %
     312qed.
     313
     314(*
     315lemma is_seq_block_instance_append : ∀p,g,is_seq.
     316  ∀B1.
     317  ∀B2 : bind_seq_block p g is_seq.
     318  ∀l1,l2.
     319  ∀b1 : Σb.is_safe_block p g b.
     320  ∀b2 : seq_block p g.
     321  instantiates_to ? (seq_block p g) B1 l1 (pi1 … b1) →
     322  instantiates_to ? (seq_block p g) B2 l2 b2 →
     323  instantiates_to ? (seq_block p g) (B1 @ B2) (l1 @ l2) (b1 @ b2).
     324#p #g * #B1 elim B1 -B1
     325[ #B1 | #f1 #IH1 ]
     326#B1prf whd in B1prf;
     327#B2 * [2,4: #r1 #l1' ] #l2 #b1 #b2 [1,4: *]
     328whd in ⊢ (%→?);
    88329[ @IH1
    89 | #EQ destruct(EQ) lapply b2' -b2' lapply l2 -l2 elim b2
    90   [ #B2 | #f2 #IH2] * [2,4: #r2 #l2'] #b2' [1,4: *]
    91   normalize in ⊢ (%→?); [2: //] #H2
    92   change with (is_block_instance ??? ('new ?) (r2 :: ?) ?) whd
    93   @(IH2 … H2)
     330| #EQ destruct(EQ) lapply b2 -b2 lapply l2 -l2 elim B2 -B2
     331  [ #B2 | #f2 #IH2] * [2,4: #r2 #l2'] #b2 [1,4: *]
     332  whd in ⊢ (%→?);
     333  [ @IH2
     334  | #EQ' whd destruct @seq_block_append_proof_irr %
     335  ]
    94336]
    95337qed.
    96338
    97 definition tunnel_step : ∀p,g.codeT p g → relation (code_point p) ≝
    98   λp,g,c,x,y.∃l.stmt_at … c x = Some ? (GOTO … l) ∧ point_of_label … c l = Some ? y.
    99 
    100 notation > "x ~~> y 'in' c" with precedence 56 for @{'tunnel_step $c $x $y}.
    101 notation < "hvbox(x ~~> y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel_step $c $x $y}.
    102 interpretation "tunnel step in code" 'tunnel_step c x y = (tunnel_step ?? c x y).
    103 
    104 let rec tunnel_through p g (c : codeT p g) x through y on through : Prop ≝
    105   match through with
    106   [ nil ⇒ x = y
    107   | cons hd tl ⇒ x ~~> hd in c ∧ tunnel_through … hd tl y
    108   ].
    109 
    110 definition tunnel ≝ λp,g,c,x,y.∃through.tunnel_through p g c x through y.
    111 
    112 notation > "x ~~>^* y 'in' c" with precedence 56 for @{'tunnel $c $x $y}.
    113 notation < "hvbox(x \nbsp ~~>^* \nbsp y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel $c $x $y}.
    114 interpretation "tunnel in code" 'tunnel c x y = (tunnel ?? c x y).
    115 
    116 lemma tunnel_refl : ∀p,g.∀c : codeT p g.reflexive ? (tunnel p g c).
    117 #p #g #c #x %{[]} % qed.
    118 
    119 lemma tunnel_trans : ∀p,g.∀c : codeT p g.
    120   transitive ? (tunnel p g c).
    121 #p#g#c #x#y#z * #l1 #H1 * #l2 #H2 %{(l1@l2)}
    122 lapply H1 -H1 lapply x -x elim l1 -l1
    123 [ #x #H1 >H1 @H2
    124 | #hd #tl #IH #x * #H11 #H12
    125   %{H11} @IH @H12
    126 ] qed.
    127  
    128 definition tunnel_plus ≝ λp,g.λc : codeT p g.λx,y.
    129   ∃mid.x ~~> mid in c ∧ mid ~~>^* y in c.
    130 
    131 notation > "x ~~>^+ y 'in' c" with precedence 56 for @{'tunnel_plus $c $x $y}.
    132 notation < "hvbox(x \nbsp ~~>^+ \nbsp y \nbsp 'in' \nbsp break c)" with precedence 56 for @{'tunnel_plus $c $x $y}.
    133 interpretation "tunnel in code" 'tunnel_plus c x y = (tunnel_plus ?? c x y).
    134 
    135 lemma tunnel_plus_to_star : ∀p,g.∀c : codeT p g.∀x,y.x ~~>^+ y in c → x ~~>^* y in c.
    136 #p #g #c #x #y * #mid * #H1 * #through #H2 %{(mid :: through)}
    137 %{H1 H2} qed.
    138 
    139 lemma tunnel_plus_trans : ∀p,g.∀c : codeT p g.transitive ? (tunnel_plus p g c).
    140 #p #g #c #x #y #z * #mid * #H1 #H2
    141 #H3 %{mid} %{H1} @(tunnel_trans … H2) /2 by tunnel_plus_to_star/
    142 qed.
    143 
    144 lemma tunnel_tunnel_plus : ∀p,g.∀c : codeT p g.∀x,y,z.
    145   x ~~>^* y in c → y ~~>^+ z in c → x ~~>^+ z in c.
    146 #p #g #c #x #y #z * #through
    147 lapply x -x elim through
    148 [ #x #H1 >H1 //
    149 | #hd #tl #IH #x * #H1 #H2 #H3
    150   %{hd} %{H1} @(tunnel_trans ???? y)
    151   [ %{tl} assumption | /2 by tunnel_plus_to_star/]
     339lemma is_other_block_instance_append : ∀p,g.
     340  ∀B1 : Σb.bind_pred ? (λx.block_classifier p g x = cl_other) b.
     341  ∀B2 : bind_other_block p g.
     342  ∀l1,l2.
     343  ∀b1 : Σb.block_classifier p g b = cl_other.
     344  ∀b2 : other_block p g.
     345  instantiates_to ? (other_block p g) B1 l1 (pi1 … b1) →
     346  instantiates_to ? (other_block p g) B2 l2 b2 →
     347  instantiates_to ? (other_block p g) (B1 @@ B2) (l1 @ l2) (b1 @@ b2).
     348#p #g * #B1 elim B1 -B1
     349[ #B1 | #f1 #IH1 ]
     350#B1prf whd in B1prf;
     351#B2 * [2,4: #r1 #l1' ] #l2 #b1 #b2 [1,4: *]
     352whd in ⊢ (%→?);
     353[ @IH1
     354| #EQ destruct(EQ) lapply b2 -b2 lapply l2 -l2 elim B2 -B2
     355  [ #B2 | #f2 #IH2] * [2,4: #r2 #l2'] #b2 [1,4: *]
     356  whd in ⊢ (%→?);
     357  [ @IH2
     358  | #EQ' whd destruct @other_block_append_proof_irr %
     359  ]
    152360]
    153361qed.
    154362
    155 lemma tunnel_plus_tunnel : ∀p,g.∀c : codeT p g.∀x,y,z.
    156   x ~~>^+ y in c → y ~~>^* z in c → x ~~>^+ z in c.
    157 #p #g #c #x #y #z * #mid * #H1 #H2 #H3 %{mid} %{H1}
    158 @(tunnel_trans … H2 H3)
    159 qed.
    160 
    161 let rec seq_list_in_code (p : params) g (c : codeT p g)
    162   src l dst on l : Prop ≝
    163   match l with
     363lemma other_fin_step_has_one_label :
     364  ∀p,g.∀s:(Σs.fin_step_classifier p g s = cl_other).
     365  match fin_step_labels ?? s with
     366  [ nil ⇒ False
     367  | cons _ tl ⇒
     368    match tl with
     369    [ nil ⇒ True
     370    | _ ⇒ False
     371    ]
     372  ].
     373#p #g ** [#lbl || #ext]
     374normalize
     375[3: cases (ext_fin_step_flows p ext)
     376  [* [2: #lbl' * [2: #lbl'' #tl']]] normalize nodelta ]
     377#EQ destruct %
     378qed.
     379
     380definition label_of_other_fin_step : ∀p,g.
     381  (Σs.fin_step_classifier p g s = cl_other) → label ≝
     382λp,g,s.
     383match fin_step_labels p ? s return λx.match x with [ nil ⇒ ? | cons _ tl ⇒ ?] → ? with
     384[ nil ⇒ Ⓧ
     385| cons lbl tl ⇒ λ_.lbl
     386] (other_fin_step_has_one_label p g s).
     387
     388(*
     389definition point_seq_transition : ∀p,g.codeT p g →
     390  code_point p → code_point p → Prop ≝
     391  λp,g,c,src,dst.
     392  match stmt_at … c src with
     393  [ Some stmt ⇒ match stmt with
     394    [ sequential sq nxt ⇒
     395      point_of_succ … src nxt = dst
     396    | final fn ⇒
     397      match fin_step_labels … fn with
     398      [ nil ⇒ False
     399      | cons lbl tl ⇒
     400        match tl with
     401        [ nil ⇒ point_of_label … c lbl = Some ? dst
     402        | _ ⇒ False
     403        ]
     404      ]
     405    ]
     406  | None ⇒ False
     407  ].
     408
     409lemma point_seq_transition_label_of_other_fin_step :
     410  ∀p,c,src.∀s : (Σs.fin_step_classifier p s = cl_other).∀dst.
     411  stmt_at ?? c src = Some ? s →
     412  point_seq_transition p c src dst →
     413  point_of_label … c (label_of_other_fin_step p s) = Some ? dst.
     414#p #c #src ** [#lbl || #ext] #EQ1
     415#dst #EQ2
     416whd in match point_seq_transition; normalize nodelta
     417>EQ2 normalize nodelta whd in ⊢ (?→??(????%)?);
     418[#H @H | * ]
     419lapply (other_fin_step_has_one_label ? «ext,?»)
     420cases (fin_step_labels p ? ext) normalize nodelta [*]
     421#hd * normalize nodelta [2: #_ #_ *] *
     422#H @H
     423qed.
     424
     425lemma point_seq_transition_succ :
     426  ∀p,c,src.∀s,nxt.∀dst.
     427  stmt_at ?? c src = Some ? (sequential ?? s nxt) →
     428  point_seq_transition p c src dst →
     429  point_of_succ … src nxt = dst.
     430#p #c #src #s #nxt #dst #EQ
     431whd in match point_seq_transition; normalize nodelta
     432>EQ normalize nodelta #H @H
     433qed.
     434*)
     435
     436definition if_other : ∀p,g.∀A : Type[2].seq_or_fin_step p g → A → A → A ≝
     437  λp,g,A,c.match seq_or_fin_step_classifier p g c with
     438  [ cl_other ⇒ λx,y.x
     439  | _ ⇒ λx,y.y
     440  ].
     441
     442definition other_step_in_code ≝
     443  λp,g.
     444  λc : codeT p g.
     445  λsrc : code_point p.
     446  λs : seq_or_fin_step p g.
     447  match s return λx.if_other p g ? x (code_point p) unit → Prop with
     448  [ inl s'' ⇒ λdst.∃n.stmt_at … c src = Some ? (sequential … s'' n) ∧ ?
     449  | inr s'' ⇒ λdst.stmt_at … c src = Some ? (final … s'') ∧ ?
     450  ].
     451  [ whd in dst; cases (seq_or_fin_step_classifier ???) in dst;
     452    normalize nodelta [1,2,3: #_ @True |*: #dst
     453      @(point_of_succ … src n = dst)]
     454  | whd in dst;
     455    lapply dst -dst
     456    lapply (refl … (seq_or_fin_step_classifier ?? (inr … s'')))
     457    cases (seq_or_fin_step_classifier ?? (inr … s'')) in ⊢ (???%→%);
     458    normalize nodelta
     459    [1,2,3: #_ #_ @True
     460    |*: #EQ #dst
     461      @(point_of_label … c (label_of_other_fin_step p g «s'', EQ») = Some ? dst)
     462    ]
     463  ]
     464qed.
     465
     466definition if_other_sig :
     467  ∀p,g.∀B,C : Type[0].∀s : Σs.seq_or_fin_step_classifier p g s = cl_other.
     468  if_other p g ? s B C → B ≝
     469  λp,g,B,C.?.
     470  ** #s whd in match (if_other ??????);
     471  cases (seq_or_fin_step_classifier ???) normalize nodelta #EQ destruct(EQ)
     472  #x @x
     473qed.
     474
     475definition if_other_block_sig :
     476  ∀p,g.∀B,C : Type[0].∀b : Σb.block_classifier p g b = cl_other.
     477  if_other p g ? (\snd b) B C → B ≝
     478  λp,g,B,C.?.
     479  ** #l #s
     480  #prf #x @(if_other_sig ???? «s, prf» x)
     481qed.
     482
     483coercion other_sig_to_if nocomposites:
     484  ∀p,g.∀B,C : Type[0].∀s : Σs.seq_or_fin_step_classifier p g s = cl_other.
     485  ∀x : if_other p g ? s B C.B ≝ if_other_sig
     486  on _x : if_other ?? Type[0] ??? to ?.
     487
     488coercion other_block_sig_to_if nocomposites:
     489  ∀p,g.∀B,C : Type[0].∀s : Σs.block_classifier p g s = cl_other.
     490  ∀x : if_other p g ? (\snd s) B C.B ≝ if_other_block_sig
     491  on _x : if_other ?? Type[0] (\snd ?) ?? to ?.
     492
     493let rec other_list_in_code p g (c : codeT p g)
     494  src
     495  (b : list (Σs.seq_or_fin_step_classifier p g s = cl_other))
     496  dst on b : Prop ≝
     497  match b with
    164498  [ nil ⇒ src = dst
    165   | cons hd tl ⇒
    166     ∃n.stmt_at … c src = Some ? (sequential … hd n) ∧
    167        seq_list_in_code p g c (point_of_succ … src n) tl dst
    168   ].
    169 
    170 (*
    171 definition seq_block_cont_to_list : ∀p,g.block_cont p g SEQ → list (joint_step p g) ≝
    172   λp,g,b.\fst b @ [\snd b].
    173 
    174 coercion list_from_seq_block_cont : ∀p,g.∀b:block_cont p g SEQ.list (joint_step p g) ≝
    175   seq_block_cont_to_list on _b : block_cont ?? SEQ to list (joint_step ??).
    176 *)
    177 
    178 definition unit_deqset: DeqSet ≝ mk_DeqSet unit (λ_.λ_.true) ?.
    179  * * /2/
    180 qed.
    181 
    182 definition block_cont_in_code : ∀p,g.codeT p g → ∀ty.
    183   code_point p → block_cont p g ty → stmt_type_if ? ty (code_point p) unit_deqset → Prop ≝
    184   λp,g.λc : codeT p g.λty,src,b,dst.
    185   ∃mid.seq_list_in_code p g c src (\fst b) mid ∧
    186   match ty
    187   return λx.stmt_type_if ? x ??? →
    188     stmt_type_if ? x ? unit_deqset → Prop
    189   with
    190   [ SEQ ⇒ λs,dst.
    191       ∃n.stmt_at … c mid = Some ? (sequential … s n) ∧
    192          point_of_succ … mid n = dst
    193   | FIN ⇒ λs.λ_.stmt_at … c mid = Some ? (final … s)
    194   ] (\snd b) dst.
    195  
     499  | cons hd tl ⇒ ∃mid.
     500    other_step_in_code p g c src hd mid ∧ other_list_in_code p g c mid tl dst
     501  ].
    196502
    197503notation > "x ~❨ B ❩~> y 'in' c" with precedence 56 for
     
    201507  @{'block_in_code $c $x $B $y}.
    202508
    203 interpretation "block cont in code" 'block_in_code c x B y =
    204   (block_cont_in_code ?? c ? x B y).
    205 
    206 lemma seq_list_in_code_append : ∀p,g.∀c : codeT p g.∀x,l1,y,l2,z.
    207   seq_list_in_code p g c x l1 y →
    208   seq_list_in_code p g c y l2 z →
    209   seq_list_in_code p g c x (l1@l2) z.
    210 #p#g#c#x#l1 lapply x -x
    211 elim l1 [2: #hd #tl #IH] #x #y #l2 #z normalize in ⊢ (%→?);
    212 [ * #n * #EQ1 #H #G %{n} %{EQ1} @(IH … H G)
    213 | #EQ destruct(EQ) //
    214 ]
    215 qed.
    216 
    217 lemma block_cont_in_code_append : ∀p,g.∀c : codeT p g.∀ty,x.
    218   ∀B1 : block_cont p g SEQ.∀y.∀B2 : block_cont p g ty.∀z.
    219   x ~❨B1❩~> y in c → y ~❨B2❩~> z in c → x ~❨B1@B2❩~> z in c.
    220 #p#g#c #ty #x * whd in match stmt_type_if in ⊢ (?→%→%→?); normalize nodelta
    221 #l1 #s1 #y * #l2 #s2 #z * normalize nodelta
    222 #mid1 * #H1 * #n * #EQ1 #EQ2 * #mid2 * #H2 #H3
    223 %{mid2} %
    224 [ whd in match (〈?,?〉@?);
    225   @(seq_list_in_code_append … H1)
    226   %{n} %{EQ1} >EQ2 assumption
    227 | assumption
    228 ]
    229 qed.
    230 
     509interpretation "list in code" 'block_in_code c x B y =
     510  (other_list_in_code ?? c x B y).
     511
     512definition other_block_in_code : ∀p,g.codeT p g →
     513  code_point p → ∀b : other_block p g.
     514    if_other … (\snd b) (code_point p) unit → Prop ≝
     515  λp,g,c,src,b,dst.
     516  ∃mid.src ~❨\fst b❩~> mid in c ∧
     517  other_step_in_code p g c mid (\snd b) dst.
     518
     519interpretation "block in code" 'block_in_code c x B y =
     520  (other_block_in_code ?? c x B y).
     521
     522lemma other_list_in_code_append : ∀p,g.∀c : codeT p g.
     523  ∀x.∀b1 : list ?.
     524  ∀y.∀b2 : list ?.∀z.
     525  x ~❨b1❩~> y in c→ y ~❨b2❩~> z in c → x ~❨b1@b2❩~> z in c.
     526#p#g#c#x#b1 lapply x -x
     527elim b1 [2: ** #hd #hd_prf #tl #IH] #x #y #b2 #z
     528[3: #EQ normalize in EQ; destruct #H @H]
     529* #mid * normalize nodelta [ *#n ] #H1 #H2 #H3
     530whd normalize nodelta %{mid}
     531%{(IH … H2 H3)}
     532[ %{n} ] @H1
     533qed.
     534
     535lemma other_block_in_code_append : ∀p,g.∀c : codeT p g.∀x.
     536  ∀B1 : Σb.block_classifier p g b = cl_other.
     537  ∀y.
     538  ∀B2 : other_block p g.
     539  ∀z.
     540  x ~❨B1❩~> y in c → y ~❨B2❩~> z in c →
     541  x ~❨B1@@B2❩~> z in c.
     542#p#g#c #x ** #hd1 *#tl1 #tl1prf
     543#y * #hd2 #tl2 #z
     544* #mid1 * #H1 #H2
     545* #mid2 * #G1 #G2
     546%{mid2} %{G2}
     547whd in match (\fst ?);
     548@(other_list_in_code_append … H1)
     549%{y} %{H2 G1}
     550qed.
     551
     552(*
    231553definition instr_block_in_function :
    232   ∀p,g.∀fn : joint_internal_function g p.∀ty.
    233     instr_block p g ty →
     554  ∀p : evaluation_params.∀fn : joint_internal_function (globals p) p.
    234555    code_point p →
     556    ∀b : bind_other_block p.
    235557    ? → Prop ≝
    236  λp,g,fn,ty,B,src,dst.
     558 λp,fn,src,B,dst.
    237559 ∃vars,B'.
    238560  All ? (In ? (joint_if_locals … fn)) vars ∧
    239   is_block_instance … B vars B' ∧
     561  instantiates_to … B vars B' ∧
    240562  src ~❨B'❩~> dst in joint_if_code … fn.
    241563
    242 interpretation "instr block in function" 'block_in_code fn x B y =
    243   (instr_block_in_function ?? fn ? B x y).
     564interpretation "bind block in function" 'block_in_code fn x B y =
     565  (instr_block_in_function ? fn x B y).
    244566
    245567lemma instr_block_in_function_trans :
    246   ∀p,g.∀fn : joint_internal_function g p.∀ty,src.
    247   ∀B1 : instr_block p g SEQ.
    248   ∀mid.∀B2 : instr_block p g ty.∀dst.
    249   src ~❨B1❩~> mid in fn →
     568  ∀p,fn,src.
     569  ∀B1 : ΣB.bind_pred ? (λb.block_classifier p b = cl_other) B.
     570  ∀mid.
     571  ∀B2 : bind_other_block p.
     572  ∀dst.
     573  src ~❨B1❩~> Some ? mid in fn →
    250574  mid ~❨B2❩~> dst in fn →
    251   src ~❨B1@B2❩~> dst in fn.
    252 #p#g#fn#ty#src#B1#mid#B2#dst
     575  src ~❨B1@@B2❩~> dst in fn.
     576#p#fn#src*#B1#B1prf#mid#B2#dst
    253577* #vars1 * #b1 ** #vars1_ok #b1B1 #b1_in
    254578* #vars2 * #b2 ** #vars2_ok #b2B2 #b2_in
    255 %{(vars1@vars2)} %{(b1 @ b2)}
    256 /4 by All_append, conj, is_block_instance_append, block_cont_in_code_append/
    257 qed.
     579%{(vars1@vars2)} %{(«b1,instantiates_to_bind_pred … b1B1 B1prf» @@ b2)}
     580/4 by All_append, conj, is_other_block_instance_append, other_block_in_code_append/
     581qed.
     582*)
     583*)
     584*)
Note: See TracChangeset for help on using the changeset viewer.