Changeset 2674 for src


Ignore:
Timestamp:
Feb 18, 2013, 5:48:19 PM (7 years ago)
Author:
tranquil
Message:
  • another change in block definition
  • RTLabs -> RTL and ERTL -> ERTLptr passes fixed, others stil broken
Location:
src
Files:
8 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL_semantics.ma

    r2666 r2674  
    142142  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.λ_.eval_ertl_seq F gl ge stm id)
    143143  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.pop_ra …).
    144          
     144
    145145definition ERTL_semantics ≝
    146   make_sem_graph_params ERTL ERTL_sem_uns.
     146  mk_sem_graph_params ERTL ERTL_sem_uns.
  • src/ERTLptr/ERTLptr.ma

    r2645 r2674  
    2020    (* call_dest ≝ *) unit
    2121    (* ext_seq ≝ *) ertlptr_seq
    22     (* ext_seq_labels ≝ *) (λ_.[])
     22    (* ext_seq_labels ≝ *)
     23      (λs.match s with [ LOW_ADDRESS _ l ⇒ [l] | HIGH_ADDRESS _ l ⇒ [l] | _ ⇒ [ ]])
    2324    (* has_tailcall ≝ *) false
    2425    (* paramsT ≝ *) ℕ.
  • src/ERTLptr/ERTLtoERTLptr.ma

    r2604 r2674  
    3535|STORE arg1 arg2 reg ⇒ STORE ERTLptr … arg1 arg2 reg
    3636|extension_seq s ⇒ extension_seq ERTLptr … (ertlptr_ertl s)
    37 ]. 
     37].
    3838
    39 
    40 (* PAOLO: implement the b_graph_translate2 that expects functions that
    41    return not (list instr * instr) but (list (label → instr) * instr) *)
    4239definition translate_step:
    4340 ∀globals.
     
    4845match s return λ_.bind_step_block ERTLptr globals with
    4946[ CALL called args dest ⇒
    50     match called with
    51     [inl id ⇒ bret … [CALL ERTLptr ? (inl … id) args dest]
    52     |inr dest1 ⇒ νreg in bret … «[λl.(extension_seq ERTLptr ? (LOW_ADDRESS reg l) : joint_step ??);
    53                                   λ_.PUSH ERTLptr … (Reg … reg);
    54                                   λl.extension_seq ERTLptr ? (HIGH_ADDRESS reg l);
    55                                   λ_.PUSH ERTLptr … (Reg … reg) ;
    56                                   λ_.CALL ERTLptr ? (inr … dest1) args dest], ?»
     47    match called return λ_.bind_step_block ERTLptr globals with
     48    [inl id ⇒ bret … 〈[ ], λ_.CALL ERTLptr ? (inl … id) args dest, [ ]〉
     49    |inr dest1 ⇒ νreg in bret ? (step_block ERTLptr globals)
     50      〈[λl.(LOW_ADDRESS reg l : joint_seq ??);
     51        λ_.PUSH ERTLptr … (Reg … reg);
     52        λl.HIGH_ADDRESS reg l;
     53        λ_.PUSH ERTLptr … (Reg … reg)],
     54        λ_.CALL ERTLptr ? (inr … dest1) args dest, [ ]〉
    5755    ]
    58 | COND reg l ⇒ bret … [COND ERTLptr ? reg l]
     56| COND reg l ⇒ bret … 〈[ ], λ_.COND ERTLptr ? reg l, [ ]〉
    5957| step_seq x ⇒ bret … [seq_embed … x]
    60 ]. @I qed.
     58].
    6159
    6260definition fin_step_embed: joint_fin_step ERTL → joint_fin_step ERTLptr ≝
     
    8078  λglobals,int_fun.
    8179  (* initialize internal function *)
    82   let init ≝ init_graph_if ERTLptr globals
    83     (joint_if_luniverse … int_fun)
    84     (joint_if_runiverse … int_fun)
     80  b_graph_translate ERTL ERTLptr globals
    8581    (joint_if_result … int_fun)
    8682    (joint_if_params … int_fun)
    8783    (joint_if_stacksize … int_fun)
    88     (joint_if_entry … int_fun) in
    89   b_graph_translate …
    90     init
    9184    (translate_step …)
    9285    (translate_fin_step …)
  • src/RTLabs/RTLabsToRTL.ma

    r2640 r2674  
    362362@IH qed.
    363363
    364 lemma last_last_ne : ∀A,l.last A (pi1 … l) = Some ? (last_ne … l).
    365 #A * @list_elim_left [*] #hd #tl #_ #prf
    366 whd in match last_ne; normalize nodelta
    367 >split_on_last_ne_def @last_def qed.
    368 
    369364lemma last_not_empty : ∀A,l.not_empty A l →
    370365  match last A l with
    371366  [ None ⇒ False
    372367  | _ ⇒ True ].
    373 #A #l #prf >(last_last_ne … «l, prf») % qed.
     368#A @list_elim_left [*] #pref #last #_ #_ >last_def % qed.
    374369
    375370definition translate_op_asym_signed :
     
    858853  | cons srcr srcrs' ⇒
    859854    ν tmpr in
    860     let f : register → joint_seq RTL globals ≝
    861       λr. tmpr ← tmpr .Or. r in
    862     bret … ((MOVE RTL globals 〈tmpr,srcr〉 ::
    863     map ?? f srcrs' : list (joint_step ??)) @ [COND … tmpr lbl_true])
     855    let f : register → label → joint_seq RTL globals ≝
     856      λr.λ_. tmpr ← tmpr .Or. r in
     857    bret …
     858    〈(λ_.MOVE RTL globals 〈tmpr,srcr〉) ::
     859     map ?? f srcrs',
     860     λ_.COND … tmpr lbl_true, [ ]〉
    864861  ].
    865862
     
    940937qed.
    941938
     939(* TODO: move it *)
    942940definition ensure_bind_step_block : ∀p : params.∀g.
    943   bind_new register (list (joint_step p g)) → bind_step_block p g ≝
    944   λp,g,b.! l ← b; bret ? (step_block p g) l.
    945 
    946 definition ensure_bind_step_block_from_seq : ∀p : params.∀g.
    947941  bind_new register (list (joint_seq p g)) → bind_step_block p g ≝
    948942  λp,g,b.! l ← b; bret ? (step_block p g) l.
     
    950944coercion bind_step_block_from_bind_list nocomposites :
    951945  ∀p : params.∀g.
    952   ∀b : bind_new register (list (joint_step p g)).bind_step_block p g ≝
    953   ensure_bind_step_block on _b : bind_new register (list (joint_step ??)) to
    954   bind_step_block ??.
    955 
    956 coercion bind_step_block_from_bind_seq_list nocomposites :
    957   ∀p : params.∀g.
    958946  ∀b : bind_new register (list (joint_seq p g)).bind_step_block p g ≝
    959   ensure_bind_step_block_from_seq on _b : bind_new register (list (joint_seq ??)) to
     947  ensure_bind_step_block on _b : bind_new register (list (joint_seq ??)) to
    960948  bind_step_block ??.
    961949
     
    993981      (find_local_env_arg srcr lenv ?)), lbl'❭
    994982  | St_call_id f args retr lbl' ⇒ λstmt_typed.
    995     ❬inl ?? (bret ?? [CALL RTL ? (inl … f) (rtl_args args lenv ?)
    996       (match retr with
    997       [ Some retr ⇒ find_local_env retr lenv ?
    998       | None ⇒ [ ]
    999       ])]), lbl'❭
     983    ❬inl … (bret …
     984      〈[ ],λ_.CALL RTL ? (inl ?? f) (rtl_args args lenv ?)
     985        (match retr with
     986         [ Some retr ⇒
     987           find_local_env retr lenv ?
     988         | None ⇒ [ ]
     989         ]), [ ]〉), lbl'❭
    1000990  | St_call_ptr f args retr lbl' ⇒ λstmt_typed.
    1001991    let fs ≝ find_and_addr_arg f lenv ?? in
    1002     ❬inl … (bret … [CALL RTL ? (inr ?? fs) (rtl_args args lenv ?)
    1003       (match retr with
    1004        [ Some retr ⇒
    1005          find_local_env retr lenv ?
    1006        | None ⇒ [ ]
    1007        ])]), lbl'❭
     992    ❬inl … (bret …
     993      〈[ ],λ_.CALL RTL ? (inr ?? fs) (rtl_args args lenv ?)
     994        (match retr with
     995         [ Some retr ⇒
     996           find_local_env retr lenv ?
     997         | None ⇒ [ ]
     998         ]), [ ]〉), lbl'❭
    1008999  | St_cond r lbl_true lbl_false ⇒ λstmt_typed.
    10091000    ❬inl … (translate_cond globals (find_local_env r lenv ?) lbl_true), lbl_false❭
     
    10411032  let stack_size' ≝ f_stacksize def in
    10421033  let entry' ≝ f_entry def in
    1043   let init ≝ init_graph_if RTL globals luniverse' runiverse' [ ]
    1044      [ ] stack_size' (pi1 … entry') in
     1034  let init ≝ mk_joint_internal_function RTL globals
     1035    luniverse' runiverse' [ ] [ ] stack_size'
     1036    (add … (empty_map ? (joint_statement ??)) entry' (RETURN …)) (pi1 … entry') in
    10451037  let 〈init',lenv〉 as pr_eq ≝ initialize_locals_params_ret globals
    10461038    (f_locals def) (f_params def) (f_result def) init in
     
    10531045    | inr instrs ⇒ λ_.b_fin_adds_graph … instrs lbl def
    10541046    ] (dpi2 … pr) in
    1055   foldi … f_trans (f_graph def) init'. (* TODO *) cases daemon
     1047  foldi … f_trans (f_graph def) init'.
     1048[4: >graph_code_has_point @mem_set_add_id ] 
     1049(* TODO *) cases daemon
    10561050qed.
    10571051
  • src/joint/TranslateUtils.ma

    r2595 r2674  
    2828     〈set_runiverse … def runiverse, r〉.
    2929
    30 (* insert into a graph a block of instructions *)
    31 let rec adds_graph_list
     30definition state_update : ∀S.(S → S) → state_monad S unit ≝
     31λS,f,s.〈f s, it〉.
     32
     33(* insert into a graph a list of instructions *)
     34let rec adds_graph_pre
     35  X
    3236  (g_pars: graph_params)
    3337  (globals: list ident)
    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
    38   | cons instr others ⇒
    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     ]
     38  (* for ERTLptr: the label parameter is filled by the last label *)
     39  (pre_process : label → X → joint_seq g_pars globals)
     40  (insts: list X)
     41  (src : label) on insts :
     42  state_monad (joint_internal_function g_pars globals) label ≝
     43  match insts with
     44  [ nil ⇒ return src
     45  | cons i rest ⇒
     46    ! mid ← fresh_label … ;
     47    ! dst ← adds_graph_pre … pre_process rest mid ;
     48    !_ state_update … (add_graph … src (sequential … (pre_process dst i) mid)) ;
     49    return dst
     50  ].
     51
     52let rec adds_graph_post
     53  (g_pars: graph_params)
     54  (globals: list ident)
     55  (insts: list (joint_seq g_pars globals))
     56  (dst : label) on insts :
     57  state_monad (joint_internal_function g_pars globals) label ≝
     58  match insts with
     59  [ nil ⇒ return dst
     60  | cons i rest ⇒
     61    ! src ← fresh_label … ;
     62    ! mid ← adds_graph_post … rest dst ;
     63    !_ state_update … (add_graph … src (sequential … i mid)) ;
     64    return src
    4665  ].
    4766
     
    5372  joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
    5473  λ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   ].
     74  let pref ≝ \fst (\fst insts) in
     75  let op ≝ \snd (\fst insts) in
     76  let post ≝ \snd insts in
     77  let 〈def, mid〉 ≝ adds_graph_pre … (λlbl,inst.inst lbl) pref src def in
     78  let 〈def, mid'〉 ≝ adds_graph_post … post dst def in
     79  add_graph … mid (sequential … (op mid) mid') def.
    6380
    6481definition fin_adds_graph :
     
    6986  joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
    7087  λ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''
    78   ].
     88  let pref ≝ \fst insts in
     89  let last ≝ \snd insts in
     90  let 〈def, mid〉 ≝ adds_graph_pre … (λ_.λi.i) pref src def in
     91  add_graph … mid (final … last) def.
    7992
    8093(* ignoring register allocation for now *)
     
    120133qed.
    121134
     135(*
    122136lemma adds_graph_list_fresh_preserve :
    123137  ∀g_pars,globals,b,src,dst,def.
     
    227241]
    228242qed.
     243*)
    229244
    230245axiom adds_graph_ok :
     
    368383  ∀src_g_pars,dst_g_pars : graph_params.
    369384  ∀globals: list ident.
    370   (* initialized function definition with empty graph *)
    371   joint_internal_function dst_g_pars globals →
     385  (* initialization info *)
     386  call_dest dst_g_pars → (* joint_if_result *)
     387  paramsT dst_g_pars → (* joint_if_params *)
     388  ℕ → (* joint_if_stacksize *)
    372389  (* functions dictating the translation *)
    373390  (label → joint_step src_g_pars globals → bind_step_block dst_g_pars globals) →
     
    377394  (* destination function *)
    378395  joint_internal_function dst_g_pars globals ≝
    379   λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def.
     396  λsrc_g_pars,dst_g_pars,globals,
     397   init_ret,init_params,init_stack_size,trans_step,trans_fin_step,def.
     398  let init ≝
     399    mk_joint_internal_function dst_g_pars globals
     400    (joint_if_luniverse … def)
     401    (joint_if_runiverse … def)
     402    init_ret init_params init_stack_size
     403    (add ?? (empty_map ? (joint_statement ??)) (joint_if_entry … def) (RETURN …))
     404    (pi1 … (joint_if_entry … def)) in
    380405  let f : label → joint_statement (src_g_pars : params) globals →
    381406    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
     
    388413    | FCOND abs _ _ _ ⇒ Ⓧabs
    389414    ] in
    390   foldi … f (joint_if_code … def) empty.
     415  foldi … f (joint_if_code … def) init.
     416@hide_prf >graph_code_has_point @mem_set_add_id qed.
    391417
    392418definition partial_partition : ∀X.∀Y : DeqSet.(X → option (list Y)) → Prop ≝
     
    421447*)
    422448
     449
    423450axiom b_graph_translate_ok :
    424451  ∀src_g_pars,dst_g_pars : graph_params.
    425   ∀globals: list ident.∀empty.∀f_step,f_fin,def_in.
     452  ∀globals: list ident.
     453  ∀init_ret,init_params,init_stack_size.
     454  ∀f_step,f_fin,def_in.
    426455  luniverse_ok ?? def_in →
     456  code_closed … (joint_if_code … def_in) →
    427457  let def_out ≝
    428     b_graph_translate src_g_pars dst_g_pars globals empty f_step f_fin def_in in
     458    b_graph_translate src_g_pars dst_g_pars globals
     459      init_ret init_params init_stack_size f_step f_fin def_in in
    429460  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 ∧
     461  code_closed … (joint_if_code … def_out) ∧
     462  joint_if_result … def_out = init_ret ∧
     463  joint_if_params … def_out = init_params ∧
     464  joint_if_stacksize … def_out = init_stack_size ∧
    433465  pi1 … (joint_if_entry … def_out) = pi1 … (joint_if_entry … def_in) ∧
    434466  ∃f_lbls : label → option (list label).
     
    469501  ∀src_g_pars,dst_g_pars : graph_params.
    470502  ∀globals: list ident.
    471   (* initialized function definition with empty graph *)
    472   joint_internal_function dst_g_pars globals →
     503  (* initialization info *)
     504  call_dest dst_g_pars → (* joint_if_result *)
     505  paramsT dst_g_pars → (* joint_if_params *)
     506  ℕ → (* joint_if_stacksize *)
    473507  (* functions dictating the translation *)
    474508  (label → joint_step src_g_pars globals → step_block dst_g_pars globals) →
     
    478512  (* destination function *)
    479513  joint_internal_function dst_g_pars globals ≝
    480   λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step.
    481   b_graph_translate … empty
     514  λsrc_g_pars,dst_g_pars,globals,init1,init2,init3,trans_step,trans_fin_step.
     515  b_graph_translate … init1 init2 init3
    482516    (λl,s.return trans_step l s)
    483517    (λl,s.return trans_fin_step l s).
    484 
    485 (* helper for initializing a valid init graph (with a valid entry) *)
    486 definition init_graph_if ≝
    487   λg_pars : graph_params.λglobals.
    488   λluniverse,runiverse,ret,params,stack_size,entry.
    489   let graph ≝ add ?? (empty_map ? (joint_statement ??)) entry (RETURN …) in
    490   mk_joint_internal_function g_pars globals
    491     luniverse runiverse ret params stack_size
    492     graph entry.
    493 @hide_prf >graph_code_has_point @map_mem_prop @graph_add
    494 qed.
    495 
    496518
    497519(*
  • src/joint/blocks.ma

    r2666 r2674  
    6565definition not_empty : ∀X.list X → Prop ≝ λX,l.match l with [ nil ⇒ False | _ ⇒ True ].
    6666
    67 definition head_ne : ∀X.(Σl.not_empty X l) → X ≝
    68 λX,l.
    69 match l return λl.not_empty ? l → ? with
    70 [ nil ⇒ Ⓧ
    71 | cons hd _ ⇒ λ_.hd
    72 ] (pi2 … l).
    73 
    74 
    75 let rec split_on_last_ne_aux X l on l : not_empty X l → (list X) × X ≝
    76 match 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)
     67definition split_on_last : ∀X.list X → option ((list X) × X) ≝
     68λX.foldr …
     69  (λel,acc.match acc with
     70    [ None ⇒ Some ? 〈[ ], el〉
     71    | Some pr ⇒ Some ? 〈el :: \fst pr, \snd pr〉
     72    ]) (None ?).
     73
     74lemma split_on_last_inv : ∀X,l.
     75match split_on_last X l with
     76[ None ⇒ l = [ ]
     77| Some pr ⇒ l = \fst pr @ [ \snd pr]
    8378].
    84 
    85 definition split_on_last_ne : ∀X.(Σl.not_empty X l) → (list X)×X ≝
    86 λX,l.split_on_last_ne_aux … (pi2 … l).
    87 
    88 definition last_ne : ∀X.(Σl.not_empty X l) → X ≝ λX,l.\snd (split_on_last_ne … l).
    89 definition chop_last_ne : ∀X.(Σl.not_empty X l) → list X ≝ λX,l.\fst (split_on_last_ne … l).
    90 
    91 lemma split_on_last_ne_def : ∀X,pre,last,prf.split_on_last_ne X «pre@[last], prf» = 〈pre, last〉.
    92 whd 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 % | % ]
    96 qed.
    97 
    98 lemma split_on_last_ne_inv : ∀X,l.
    99 pi1 ?? l = (let 〈pre, last〉 ≝ split_on_last_ne X l in pre @ [last]).
    100 whd in match split_on_last_ne; normalize nodelta
    101 #X * #l elim l -l [ * ]
    102 #hd * [2: #hd' #tl'] #IH * [2: % ]
    103 whd in match (split_on_last_ne_aux ???);
    104 lapply (IH I) @pair_elim #pre #last #_ #EQ >EQ %
    105 qed.
    106 
    107 (* the label input is to accomodate ERTptr pass *)
    108 definition step_block ≝ λp,globals.Σl : list (code_point p → joint_step p globals).not_empty ? l.
    109 unification hint 0 ≔ p : params, g;
    110 S ≟ code_point p → joint_step p g,
    111 L ≟ list S,
    112 P ≟ not_empty S
    113 (*---------------------------------------*)⊢
    114 step_block p g ≡ Sig L P.
    115 
    116 definition fin_block ≝ λp,globals.(list (joint_step p globals))×(joint_fin_step p).
     79#X #l elim l -l normalize nodelta [ // ]
     80#hd #tl
     81change with (match split_on_last ? tl in option  with [ _ ⇒ ?]) in
     82  match (split_on_last ? (hd :: tl)); cases (split_on_last ??)
     83normalize nodelta [2: * #pref #last ] #EQ >EQ normalize % qed.
     84
     85lemma split_on_last_hit : ∀X,pref,last.
     86split_on_last X (pref @ [last]) = Some ? 〈pref, last〉.
     87#X #pref elim pref -pref normalize [//]
     88#hd #tl #IH #last >IH % qed.
     89
     90(* the label input is to accomodate ERTLptr pass
     91   the postfix is for the case CALL ↦ instrs* ; CALL; instrs* *)
     92definition step_block ≝
     93  λp,globals.list (code_point p → joint_seq p globals) ×
     94             (code_point p → joint_step p globals) ×
     95             (list (joint_seq p globals)).
     96
     97definition fin_block ≝ λp,globals.(list (joint_seq p globals))×(joint_fin_step p).
    11798
    11899(*definition seq_to_skip_block :
     
    140121bind_fin_block p g ≡ bind_new register P.
    141122
    142 definition bind_step_list ≝ λp : stmt_params.λglobals.
    143   bind_new register (list (joint_step p globals)).
     123definition bind_seq_list ≝ λp : stmt_params.λglobals.
     124  bind_new register (list (joint_seq p globals)).
    144125unification hint 0 ≔ p : stmt_params, g;
    145 S ≟ joint_step p g,
     126S ≟ joint_seq p g,
    146127L ≟ list S
    147128(*---------------------------------------*)⊢
    148 bind_step_list p g ≡ bind_new register L.
     129bind_seq_list p g ≡ bind_new register L.
    149130
    150131definition add_dummy_variance : ∀X,Y : Type[0].list Y → list (X → Y) ≝ λX,Y.map … (λx.λ_.x).
    151132
    152133definition ensure_step_block : ∀p : params.∀globals.
    153 list (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»
     134list (joint_seq p globals) → step_block p globals ≝
     135λp,g,l.
     136match split_on_last … l return λ_.step_block ?? with
     137[ None ⇒ 〈[ ], λ_.NOOP ??, [ ]〉
     138| Some pr ⇒ 〈add_dummy_variance … (\fst pr), λ_.\snd pr, [ ]〉
    157139].
    158140
    159 definition ensure_step_list : ∀p,globals.
    160 list (joint_seq p globals) → list (joint_step p globals) ≝
    161 λp,g.map … (step_seq …).
    162 
    163 definition ensure_step_block_from_seq : ∀p : params.∀globals.
    164 list (joint_seq p globals) → step_block p globals ≝
    165 λp,g.ensure_step_block ?? ∘ ensure_step_list ??.
    166 
    167 coercion step_block_from_list nocomposites : ∀p : params.∀g.∀l : list (joint_step p g).step_block p g ≝
    168 ensure_step_block on _l : list (joint_step ??) to step_block ??.
    169 
    170 coercion step_list_from_seq nocomposites : ∀p,g.∀l : list (joint_seq p g).list (joint_step p g) ≝
    171 ensure_step_list on _l : list (joint_seq ??) to list (joint_step ??).
    172 
    173 coercion step_block_from_seq nocomposites : ∀p : params.∀g.∀l : list (joint_seq p g).step_block p g ≝
    174 ensure_step_block_from_seq on _l : list (joint_seq ??) to step_block ??.
    175 
     141coercion step_block_from_seq_list nocomposites :
     142∀p : params.∀g.∀l : list (joint_seq p g).step_block p g ≝
     143ensure_step_block on _l : list (joint_seq ??) to step_block ??.
    176144
    177145(*definition bind_skip_block ≝ λp : stmt_params.λglobals,A.
     
    259227  @{'block_in_code $c $x $B $l $y}.
    260228 
    261 notation < "hvbox(x ~❨ B , l ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
     229notation < "hvbox(x ~❨ B , break l ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
    262230  @{'block_in_code $c $x $B $l $y}.
    263231
    264 notation > "x ~❨ B , l, r ❩~> y 'in' c" with precedence 56 for
     232notation > "x ~❨ B , l , r ❩~> y 'in' c" with precedence 56 for
    265233  @{'bind_block_in_code $c $x $B $l $r $y}.
    266234 
    267 notation < "hvbox(x ~❨ B , l, r ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
     235notation < "hvbox(x ~❨ B , break l , break r ❩~> y \nbsp 'in' \nbsp break c)" with precedence 56 for
    268236  @{'bind_block_in_code $c $x $B $l $r $y}.
    269237
     
    278246  stmt_at … c src = Some ? (final … s).
    279247
    280 let rec step_list_in_code p globals (c : codeT p globals)
    281   (src : code_point p) (B : list (joint_step p globals))
     248let rec seq_list_in_code p globals (c : codeT p globals)
     249  (src : code_point p) (B : list (joint_seq p globals))
    282250  (l : list (code_point p)) (dst : code_point p) on B : Prop ≝
    283251  match B with
    284   [ nil ⇒
    285     match l with
    286     [ nil ⇒ src = dst
    287     | _ ⇒ False
    288     ]
     252  [ nil ⇒ l = [ ] ∧ src = dst
    289253  | cons hd tl ⇒
    290     match l with
    291     [ nil ⇒ False
    292     | cons mid rest ⇒
    293       step_in_code …  c src hd mid ∧ step_list_in_code … c mid tl rest dst
    294     ]
    295   ].
    296 
     254    ∃mid,rest.l = src :: rest ∧
     255    step_in_code …  c src hd mid ∧
     256    seq_list_in_code … c mid tl rest dst
     257  ].
     258
     259(* leaving it out because it can be misleading
    297260interpretation "step list in code" 'block_in_code c x B l y = (step_list_in_code ?? c x B l y).
    298 
    299 lemma step_list_in_code_ne : ∀p,globals.∀c : codeT p globals.∀src,B,l,dst.
     261*)
     262
     263lemma seq_list_in_code_ne : ∀p,globals.∀c : codeT p globals.∀src,B,l,dst.
    300264  not_empty ? B →
    301   src ~❨B,l❩~> dst in c
    302   ∃prf : not_empty … l.
    303   \snd (split_on_last_ne … «l, prf») = dst.
    304 #p #globals #c #src #b lapply src -src elim b -b [ #src #l #dst * ]
     265  seq_list_in_code … c src B l dst
     266  ∃post.l = src :: post.
     267#p #globals #c #src * [ #l #dst * ] #hd #tl #l #dst #_ * #mid * #post ** #EQl #_ #_ %{EQl} qed.
     268(* #b lapply src -src elim b -b [ #src #l #dst * ]
    305269#hd * [2: #hd' #tl ] #IH #src * [1,3: #dst #_ * ]
    306 #mid * [ #dst #_ * #_ * |4: #mid' #tl #dst #_ * #_ * ]
    307 [2: #dst * * #_ whd in ⊢ (%→?); #EQ destruct %{I} % ]
    308 #mid' #rest #dst * * #H1 #H2 %{I}
    309 cases (IH … I H2) * #EQ <EQ
    310 whd in match (split_on_last_ne ??);
    311 whd in match split_on_last_ne; normalize nodelta
    312 @pair_elim #a #b #_ %
    313 qed.
    314 
    315 lemma step_list_in_code_append :
     270#mid * [ #dst #_ ** #EQ destruct #_ * |4: #mid' #tl #dst #_ ** #_ #_ * ]
     271[2: #dst #_ ** #EQ destruct normalize nodelta #_ #_ %{[ ]} % ]
     272#mid' #rest #dst #_ ** #EQ destruct #H1 #H2
     273cases (IH … I H2) #post normalize nodelta #EQ destruct %{(mid' :: post)} %
     274qed.
     275*)
     276
     277lemma seq_list_in_code_append :
    316278  ∀p,globals.∀c : codeT p globals.∀src,B1,l1,mid,B2,l2,dst.
    317   src ~❨B1,l1❩~> mid in c → mid ~❨B2,l2❩~> dst in c
    318   src ~❨B1@B2,l1@l2❩~> dst in c.
    319 #p #globals #c #src #B1 lapply src -src elim B1
    320 [ #src * [2: #mid' #rest] #mid #B2 #l2 #dst [*] #EQ normalize in EQ; destruct(EQ)
    321   #H @H
    322 | #hd #tl #IH #src * [2: #mid' #rest] #mid #B2 #l2 #dst * #H1 #H2
    323   #H3 %{H1 (IH … H2 H3)}
     279  seq_list_in_code … c src B1 l1 mid
     280  seq_list_in_code … c mid B2 l2 dst →
     281  seq_list_in_code … c src (B1@B2) (l1@l2) dst.
     282#p #globals #c #src #B1 lapply src -src elim B1 -B1
     283[ #src #l1 #mid #B2 #l2 #dst * #EQ1 #EQ2 destruct #H @H
     284| #hd #tl #IH #src #l1 #mid #B2 #l2 #dst * #mid' * #rest **
     285  #EQ destruct #H1 #H2 #H3 %{mid'} %{(rest@l2)} %{(IH … H2 H3)} %{H1} %
    324286]
    325287qed.
    326288
    327 lemma step_list_in_code_append_inv :
     289lemma seq_list_in_code_append_inv :
    328290  ∀p,globals.∀c : codeT p globals.∀src,B1,B2,l,dst.
    329   src ~❨B1@B2,l❩~> dst in c →
    330   ∃l1,mid,l2.l = l1 @ l2 ∧ src ~❨B1,l1❩~> mid in c ∧ mid ~❨B2,l2❩~> dst in c.
     291  seq_list_in_code … c src (B1@B2) l dst →
     292  ∃l1,mid,l2.l = l1 @ l2 ∧ seq_list_in_code … c src B1 l1 mid ∧
     293  seq_list_in_code … c mid B2 l2 dst.
    331294#p #globals #c #src #B1 lapply src -src elim B1 -B1
    332 [ #src #B2 #l #dst #H %{[ ]} %{src} %{l} %{H} % %
    333 | #hd #tl #IH #src #B2 * [2: #mid #rest] #dst * #H1 #H2
    334   elim (IH … H2) #l1 * #mid' * #l2 ** #G1 #G2 #G3
    335   %{(mid::l1)} %{mid'} %{l2} %{G3} >G1 %{(refl …)}
    336   %{H1 G2}
     295[ #src #B2 #l #dst #H %{[ ]} %{src} %{l} %{H} % % %
     296| #hd #tl #IH #src #B2 #l2 #dst * #mid * #rest ** #EQ destruct
     297  #H1 #H2 elim (IH … H2) #l1 * #mid' * #l2 ** #EQ destruct #G1 #G2
     298  %{(src::l1)} %{mid'} %{l2} %{G2} %{(refl …)} % [| %[| %{G1} %{H1} % ]]
    337299]
    338300qed.
    339 
    340 lemma append_not_empty_r : ∀X,l1,l2.not_empty X l2 → not_empty ? (l1 @ l2).
    341 #X #l1 cases l1 -l1 [ #l2 #K @K | #hd #tl #l2 #_ % ] qed.
    342301
    343302definition map_eval : ∀X,Y : Type[0].list (X → Y) → X → list Y ≝ λX,Y,l,x.map … (λf.f x) l.
     
    345304definition step_block_in_code ≝
    346305  λp,g.λc : codeT p g.λsrc.λb : step_block p g.λl,dst.
    347   let 〈pref, last〉 ≝ split_on_last_ne … b in
    348   ∃mid.src ~❨map_eval … pref mid, l❩~> mid in c ∧ step_in_code ?? c mid (last mid) dst.
     306  let pref ≝ \fst (\fst b) in
     307  let stp ≝ \snd (\fst b) in
     308  let post ≝ \snd b in
     309  ∃l1,mid1,mid2,l2.
     310  l = l1 @ mid1 :: l2 ∧
     311  seq_list_in_code ?? c src (map_eval … pref mid1) l1 mid1 ∧
     312  step_in_code ?? c mid1 (stp mid1) mid2 ∧
     313  seq_list_in_code ?? c mid2 post l2 dst.
    349314
    350315lemma map_compose : ∀X,Y,Z,f,g.∀l : list X.map Y Z f (map X Y g l) = map … (f∘g) l.
     
    357322#X #l elim l -l normalize // qed.
    358323
     324definition fin_block_in_code ≝
     325  λp,g.λc:codeT p g.λsrc.λB : fin_block p g.λl.λdst : unit.
     326  ∃pref,mid.l = pref @ [mid] ∧
     327  seq_list_in_code … c src (\fst B) pref mid ∧ fin_step_in_code … c mid (\snd B).
     328
     329interpretation "step block in code" 'block_in_code c x B l y = (step_block_in_code ?? c x B l y).
     330interpretation "fin block in code" 'block_in_code c x B l y = (fin_block_in_code ?? c x B l y).
     331
    359332lemma coerced_step_list_in_code :
    360 ∀p : params.∀g,c,src.∀b : list (joint_step p g).∀l,dst.
    361 step_block_in_code p g c src b l dst
     333∀p : params.∀g,c,src.∀b : list (joint_seq p g).∀l,dst.
     334src ~❨b, l❩~> dst in c
    362335match b with
    363336[ nil ⇒ step_in_code … c src (NOOP …) dst
    364 | _ ⇒ step_list_in_code … c src b (l@[dst]) dst
     337| _ ⇒ seq_list_in_code … c src b l dst
    365338].
    366339#p #g #c #src @list_elim_left [2: #last #pref #_ ] #l #dst
    367 [2: * #src' * cases l [2: #hd' #tl' *] whd in ⊢ (%→?); #EQ destruct #K @K ]
    368 cases pref -pref [2: #hd #tl ]
    369 whd in ⊢ (%→?);
    370 [2: * #src' * cases l [2: #hd' #tl' *] whd in ⊢ (%→?); #EQ destruct #K %{K} % ]
    371 whd in match (ensure_step_block ???);
    372 <map_append
    373 change with ((? :: ?) @ ?) in match (? :: ? @ ?);
    374 >split_on_last_ne_def normalize nodelta * #mid *
    375 whd in match (map_eval ????);
    376 >map_compose >map_id #H1 #H2
    377 @(step_list_in_code_append … H1) %{H2} %
    378 qed.
    379 
    380 definition fin_block_in_code ≝
    381   λp,g.λc:codeT p g.λsrc.λB : fin_block p g.λl.λdst : unit.
    382   ∃hd,tl.l = hd @ [tl] ∧
    383   src ~❨\fst B, hd❩~> tl in c ∧ fin_step_in_code … c tl (\snd B).
    384 
    385 interpretation "step block in code" 'block_in_code c x B l y = (step_block_in_code ?? c x B l y).
    386 interpretation "fin block in code" 'block_in_code c x B l y = (fin_block_in_code ?? c x B l y).
     340[2: * #pref * #mid1 * #mid2 * #post *** #EQ * #EQ' #EQ''
     341  #H * #EQ''' #EQ'''' destruct @H ]
     342whd in ⊢ (?????%??→?); >split_on_last_hit normalize nodelta
     343*#l1*#mid1*#mid2*#l2*** #EQ1
     344whd in match map_eval; whd in match add_dummy_variance; normalize nodelta
     345>map_compose >map_id #pref_in_code #last_in_code * #EQ2 #EQ3 destruct
     346cut (∃hd,tl.pref@[last] = hd::tl)
     347[ cases pref [ %{last} %{[ ]} % | #hd #tl %{hd} %{(tl@[last])} % ]] * #hd * #tl
     348#EQ >EQ in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?]); normalize nodelta -hd -tl
     349@(seq_list_in_code_append … pref_in_code)
     350%[| %[| % [2: %%] %{last_in_code} % ]]
     351qed.
    387352
    388353let rec bind_new_instantiates B X
  • src/joint/semanticsUtils.ma

    r2645 r2674  
    33include "utilities/hide.ma".
    44include "ASM/BitVectorTrie.ma".
     5include "joint/TranslateUtils.ma".
    56
    67record hw_register_env : Type[0] ≝
     
    6566(******************************** GRAPHS **************************************)
    6667
    67 definition make_sem_graph_params :
    68   ∀pars : unserialized_params.
    69   ∀g_pars : ∀F.sem_unserialized_params pars F.
     68record sem_graph_params : Type[1] ≝
     69{ sgp_pars : unserialized_params
     70; sgp_sup : ∀F.sem_unserialized_params sgp_pars F
     71}.
     72
     73definition sem_graph_params_to_graph_params :
     74  ∀pars : sem_graph_params.graph_params ≝
     75  λpars.mk_graph_params (sgp_pars pars).
     76
     77coercion graph_params_from_sem_graph_params nocomposites :
     78  ∀pars : sem_graph_params.
     79  graph_params ≝ sem_graph_params_to_graph_params
     80  on _pars : sem_graph_params to graph_params.
     81
     82definition sem_graph_params_to_sem_params :
     83  ∀pars : sem_graph_params.
    7084  sem_params ≝
    71   λpars,spars.
    72   let g_pars ≝ mk_graph_params pars in
     85  λpars.
    7386  mk_sem_params
    74     g_pars
    75     (spars ?)
     87    (pars : graph_params)
     88    (sgp_sup pars ?)
    7689    (word_of_identifier ?)
    7790    (an_identifier ?)
    7891    ? (refl …).
    7992* #p % qed.
     93
     94coercion sem_params_from_sem_graph_params :
     95  ∀pars : sem_graph_params.
     96  sem_params ≝ sem_graph_params_to_sem_params
     97  on _pars : sem_graph_params to sem_params.
     98
    8099
    81100(******************************** LINEAR **************************************)
     
    85104#p #IH >nat_possucc whd in ⊢ (??%?); >IH % qed.
    86105
    87 definition make_sem_lin_params :
    88   ∀pars : unserialized_params.
    89   (∀F.sem_unserialized_params pars F) →
     106record sem_lin_params : Type[1] ≝
     107{ slp_pars : unserialized_params
     108; slp_sup : ∀F.sem_unserialized_params slp_pars F
     109}.
     110
     111definition sem_lin_params_to_lin_params :
     112  ∀pars : sem_lin_params.lin_params ≝
     113  λpars.mk_lin_params (slp_pars pars).
     114
     115coercion lin_params_from_sem_lin_params nocomposites :
     116  ∀pars : sem_lin_params.
     117  lin_params ≝ sem_lin_params_to_lin_params
     118  on _pars : sem_lin_params to lin_params.
     119
     120definition sem_lin_params_to_sem_params :
     121  ∀pars : sem_lin_params.
    90122  sem_params ≝
    91   λpars,spars.
    92   let lin_pars ≝ mk_lin_params pars in
     123  λpars.
    93124  mk_sem_params
    94     lin_pars
    95     (spars ?)
     125    (pars : lin_params)
     126    (slp_sup pars ?)
    96127    succ_pos_of_nat
    97128    (λp.pred (nat_of_pos p))
     
    101132] qed.
    102133
    103 
     134coercion sem_params_from_sem_lin_params :
     135  ∀pars : sem_lin_params.
     136  sem_params ≝ sem_lin_params_to_sem_params
     137  on _pars : sem_lin_params to sem_params.
    104138
    105139
     
    130164qed.
    131165
     166(*lemma b_graph_translate_eval :
     167  ∀src : sem_graph_params.
     168  ∀dst : sem_graph_params.
     169  ∀globals: list ident.
     170  ∀init_ret,init_params,init_stack_size.
     171  ∀f_step,f_fin,def_in.
     172  let def_out ≝
     173    b_graph_translate src_g_pars dst_g_pars globals
     174      init_ret init_params init_stack_size f_step f_fin def_in in
     175  ∀st : state_pc src
     176*)
  • src/joint/semantics_blocks.ma

    r2655 r2674  
    5353  eval_seq_no_pc p (globals p) (ev_genv p) curr_id curr_fn s st = return st' →
    5454  as_execute (joint_abstract_status p) st
    55     (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)).
     55    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)) ∧
     56  as_classifier (joint_abstract_status p) st cl_other.
    5657#p #st#curr_id #curr_fn #s #dst #st' #EQfetch * #nxt * #EQstmt_at #EQdst
    57 #EQeval whd whd in match eval_state; whd in match eval_statement_no_pc;
     58#EQeval whd in ⊢ (?%%); whd in ⊢ (?(??%?)(??%?));
     59whd in match eval_statement_no_pc;
    5860whd in match fetch_statement; normalize nodelta >EQfetch >m_return_bind
    59 >EQstmt_at >m_return_bind normalize nodelta >EQeval >m_return_bind
    60 whd in ⊢ (??%%); @eq_f whd in match next; normalize nodelta
    61 whd in match (pc ??);  whd in match succ_pc; normalize nodelta >EQdst %
     61>m_return_bind >EQstmt_at >m_return_bind normalize nodelta
     62% [2: % ]
     63whd in ⊢ (??%?); normalize nodelta >EQeval whd in ⊢ (??%%);
     64@eq_f whd in ⊢ (??%?); @eq_f2 [2: %]
     65whd in match succ_pc; normalize nodelta @eq_f @EQdst
    6266qed.
    6367
     
    7377    return 〈curr_id, curr_fn〉 →
    7478  let src ≝ point_of_pc p (pc … st) in
    75   step_list_in_code … (joint_if_code … curr_fn) src b l dst →
     79  seq_list_in_code … (joint_if_code … curr_fn) src b l dst →
    7680  All ? (no_cost_label …) b →
    7781  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
     
    9094    match l return λx.∀dst,st'.?→?→?→?→Σtaaf.(True ↔ bool_to_Prop (taaf_non_empty … taaf)) with
    9195    [ nil ⇒ λdst,st',fd_prf,in_code.⊥
    92     | cons mid rest ⇒
    93       λdst,st',fd_prf,in_code,all_other,EQ1.
     96    | cons _ rest ⇒ λdst.
     97      let mid ≝ match rest with [ nil ⇒ dst | cons mid _ ⇒ mid ] in
     98      λst',fd_prf,in_code,all_other,EQ1.
    9499      let mid_pc ≝ pc_of_point p (pc_block (pc … st)) mid in
    95100      match eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st
     
    106111      ] (refl …)
    107112    ]
    108   ]. @hide_prf
     113  ].
     114@hide_prf
    109115[1,2: [2: % [*] generalize in ⊢ (?(???? (match % with [ _ ⇒ ?])) → ?); ]
    110116  whd in EQ1 : (??%%);
    111   cases l in in_code; whd in ⊢ (%→?); [2,4: #hd #tl * ] #EQ destruct
     117  cases l in in_code; whd in ⊢ (%→?); [2,4: #hd #tl * #ABS destruct ] * #_ #EQ destruct
    112118  >pc_of_point_of_pc cases st // #a #b #c #e >(K ?? e) normalize nodelta *
    113 | @in_code
     119| cases in_code #a * #b ** #ABS destruct
    114120|12: whd in EQ1 : (??%%); >EQ2 in EQ1; whd in ⊢ (??%?→?); #EQ1 destruct(EQ1)
    115 |4: cases tr_tl -tr_tl #tr_tl cases tl in in_code all_other;
    116   [ #_ #_ * #_ cases (taaf_non_empty ????)
    117     [ #ABS cases (ABS I) | #_ % ]
    118   | #hd' #tl' ** #nxt * #EQstmt_at #EQ_nxt cases rest [*] #mid' #rest' *
    119     * #nxt' * #EQstmt_at' #EQ_nxt' #_ * #hd_other * #hd_other'
    120     #_ * #H #_ >(H I) % whd in ⊢ (%→?);
    121     whd in ⊢ (?(??%?)→?); whd in match (as_pc_of ??);
    122     >fetch_statement_eq [2: whd in match point_of_pc;
    123     normalize nodelta >point_of_offset_of_point @EQstmt_at' |3: @fd_prf |*:]
    124     normalize nodelta
    125     >(no_label_uncosted … hd_other') * #ABS @ABS %
    126   ]
    127 |7: % [2: #_ %] * @taaf_cons_non_empty
     121|4: cases tr_tl -tr_tl #tr_tl * #_ #H
     122  @if_elim [2: #_ % ] #G lapply (H G) -H -G
     123 cases tl in in_code all_other; [ #_ #_ * ]
     124 #hd' #tl' * #mid' * #rest' ** #EQ * #nxt * #EQstmt_at #EQ_nxt
     125 * #mid'' * #rest'' ** #EQ' * #nxt' * #EQstmt_at' #EQnxt' #_
     126 normalize nodelta -mid_pc destruct
     127 * #_ * #H #_ #_ % whd in ⊢ (%→?);
     128 whd in ⊢ (?(??%?)→?); whd in match (as_pc_of ??);
     129  >fetch_statement_eq [2: whd in match point_of_pc;
     130  normalize nodelta >point_of_offset_of_point @EQstmt_at' |3: @fd_prf |*:]
     131  normalize nodelta
     132  >(no_label_uncosted … H) * #ABS @ABS %
     133|7: % [2: #_ %] #_ @taaf_cons_non_empty
    128134]
    129135change with (! y ← ? ; repeat_eval_seq_no_pc ????? = ?) in EQ1;
    130136>EQ2 in EQ1; >m_return_bind
    131 cases in_code -in_code * #nxt * #EQ_stmt_at #EQ_mid #rest_in_code
     137cases in_code -in_code #mid' * #rest' ** #EQ1 #step_in cases (step_in)
     138#nxt * #EQ_stmt_at #EQ_mid' #rest_in_code
     139normalize nodelta
    132140cases all_other -all_other #hd_no_cost #tl_other
    133 #EQ1
     141#EQ3 destruct skip (mid_pc)
    134142try assumption
    135 [2: whd whd in match eval_state; normalize nodelta
    136   >(fetch_statement_eq … fd_prf EQ_stmt_at)
    137   >m_return_bind
    138   whd in match eval_statement_no_pc; normalize nodelta
    139   >EQ2 >m_return_bind
    140   whd in match eval_statement_advance; normalize nodelta
    141   whd in match next; normalize nodelta
    142   whd in match succ_pc; normalize nodelta
    143   >EQ_mid %
    144 |1: whd whd in ⊢ (??%?);
     143[ whd whd in ⊢ (??%?);
    145144  >(fetch_statement_eq … fd_prf EQ_stmt_at) normalize nodelta %
    146 |3: normalize nodelta >point_of_pc_of_point assumption
     145|*:
     146  cases tl in rest_in_code;
     147  [1,3: * #EQ4 #EQ5 destruct normalize nodelta
     148  |*: #hd' #tl' * #mid'' * #rest'' ** #EQ4 #step_in' #rest_in_code'
     149    destruct normalize nodelta
     150  ]
     151  [1,3: @(proj1 … (produce_step_trace … fd_prf … EQ2)) assumption
     152  |2: %[%] @point_of_pc_of_point
     153  |4: >point_of_pc_of_point %[| %[| %{rest_in_code'} %{step_in'} %]]
     154  ]
    147155]
    148156qed.
     
    159167    return 〈curr_id, curr_fn〉 →
    160168  let src ≝ point_of_pc p (pc … st) in
    161   step_list_in_code … (joint_if_code … curr_fn) src b l dst →
     169  seq_list_in_code … (joint_if_code … curr_fn) src b l dst →
    162170  All ? (no_cost_label …) b →
    163171  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
     
    166174  λp,st,curr_id,curr_fn,b,l,dst,st',prf1,prf2,prf3,prf4.
    167175  produce_trace_any_any_free_aux p st curr_id curr_fn b l dst st' prf1 prf2 prf3 prf4.
     176
     177(* when a seq_list is coerced to a step_block *)
     178definition produce_trace_any_any_free_coerced :
     179  ∀p : evaluation_params.
     180  ∀st : state_pc p.
     181  ∀curr_id,curr_fn.
     182  ∀b : list (joint_seq p (globals p)).
     183  ∀l : list (code_point p).
     184  ∀dst : code_point p.
     185  ∀st' : state p.
     186  fetch_internal_function … (ev_genv p) (pc_block (pc … st)) =
     187    return 〈curr_id, curr_fn〉 →
     188  let src ≝ point_of_pc p (pc … st) in
     189  src ~❨b, l❩~> dst in joint_if_code … curr_fn →
     190  All ? (no_cost_label …) b →
     191  repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' →
     192  trace_any_any_free (joint_abstract_status p) st
     193    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)) ≝
     194  λp,st,curr_id,curr_fn,b.?.
     195#l #dst #st' #fd_prf #prf
     196lapply (coerced_step_list_in_code … prf)
     197inversion b normalize nodelta
     198[ #_ #in_code #_ whd in ⊢ (??%%→?); #EQ destruct
     199  cases (produce_step_trace … fd_prf … in_code (refl …))
     200  #H #G
     201  %2{(taa_base …)} assumption
     202| #hd #tl #_ #EQ <EQ -hd -tl @produce_trace_any_any_free assumption
     203]
     204qed.
Note: See TracChangeset for help on using the changeset viewer.