Changeset 2214 for src/joint


Ignore:
Timestamp:
Jul 19, 2012, 2:42:02 PM (7 years ago)
Author:
tranquil
Message:
  • changed order of parameters of joint_internal_function and genv in semantics
  • in semantics, unified more_sem_unserialized_params and more_sem_genv_params
  • renamed all <language>_params to <LANGUAGE>
Location:
src/joint
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint_paolo.ma

    r2208 r2214  
    472472  (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars register))).
    473473
    474 record joint_internal_function (globals: list ident) (p:params) : Type[0] ≝
     474record joint_internal_function (p:params) (globals: list ident) : Type[0] ≝
    475475{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
    476476  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
     
    489489
    490490definition joint_closed_internal_function ≝
    491   λglobals,p.
     491  λp,globals.
    492492    Σdef : joint_internal_function globals p. code_closed … (joint_if_code … def).
    493493
     
    495495  λglobals: list ident.
    496496  λpars: params.
    497   λint_fun: joint_internal_function globals pars.
     497  λint_fun: joint_internal_function pars globals.
    498498  λgraph: codeT pars globals.
    499499  λentry.
    500500  λexit.
    501     mk_joint_internal_function globals pars
     501    mk_joint_internal_function pars globals
    502502      (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun)
    503503      (joint_if_params … int_fun) (joint_if_locals … int_fun) (joint_if_stacksize … int_fun)
     
    507507  λglobals.λpars : graph_params.
    508508  λgraph.
    509   λp:joint_internal_function globals pars.
     509  λp:joint_internal_function pars globals.
    510510  λentry_prf.
    511511  λexit_prf.
     
    536536definition add_graph ≝
    537537  λg_pars : graph_params.λglobals.λl:label.λstmt.
    538     λp:joint_internal_function globals g_pars.
     538    λp:joint_internal_function g_pars globals.
    539539   let code ≝ add … (joint_if_code … p) l stmt in
    540     mk_joint_internal_function ? g_pars
     540    mk_joint_internal_function
    541541     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    542542     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
     
    550550
    551551definition set_locals ≝
    552   λglobals,pars.
    553   λp : joint_internal_function globals pars.
     552  λpars,globals.
     553  λp : joint_internal_function pars globals.
    554554  λlocals.
    555    mk_joint_internal_function globals pars
     555   mk_joint_internal_function pars globals
    556556    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    557557    (joint_if_params … p) locals (joint_if_stacksize … p)
     
    561561
    562562definition joint_program ≝
    563  λp:params. program (λglobals. joint_function globals p) nat.
     563 λp:params. program (joint_function p) nat.
  • src/joint/TranslateUtils_paolo.ma

    r2182 r2214  
    55(* type T is the syntactic type of the generated things *)
    66(* (sig for RTLabs registers, unit in others ) *)
    7 definition freshT ≝ λg.λpars : params.state_monad (joint_internal_function … g pars).
     7definition freshT ≝ λg.λpars : params.state_monad (joint_internal_function pars g).
    88
    99definition rtl_ertl_fresh_reg:
     
    3939  (globals: list ident)
    4040  (insts: list (joint_seq g_pars globals))
    41   (src : label) on insts : state_monad (joint_internal_function … g_pars) label ≝
     41  (src : label) on insts : state_monad (joint_internal_function g_pars globals) label ≝
    4242  match insts with
    4343  [ nil ⇒ return src
     
    4949  ].
    5050
     51definition is_inr : ∀A,B.A + B → bool ≝ λA,B,x.match x with
     52  [ inl _ ⇒ true
     53  | inr _ ⇒ false
     54  ].
     55definition is_inl : ∀A,B.A + B → bool ≝ λA,B,x.match x with
     56  [ inl _ ⇒ true
     57  | inr _ ⇒ false
     58  ].
     59
    5160definition adds_graph :
    5261  ∀g_pars : graph_params.
     
    5564       seq_block g_pars globals (joint_fin_step g_pars).
    5665  label → if is_inl … b then label else unit →
    57   joint_internal_function … g_pars → joint_internal_function … g_pars ≝
     66  joint_internal_function g_pars globals → joint_internal_function g_pars globals ≝
    5867  λg_pars,globals,insts,src.
    5968  match insts return λx.if is_inl … x then ? else ? → ? → ? with
     
    6978definition insert_prologue ≝
    7079  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
    71   λdef : joint_internal_function globals g_pars.
     80  λdef : joint_internal_function g_pars globals.
    7281  let entry ≝ joint_if_entry … def in
    7382  match stmt_at … entry
     
    99108definition insert_epilogue ≝
    100109  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
    101   λdef : joint_internal_function globals g_pars.
     110  λdef : joint_internal_function g_pars globals.
    102111  let exit ≝ joint_if_exit … def in
    103112  match stmt_at … exit
     
    121130       bind_seq_block g_pars globals (joint_fin_step g_pars).
    122131  label → if is_inl … b then label else unit →
    123   joint_internal_function globals g_pars
    124   joint_internal_function globals g_pars ≝
     132  joint_internal_function g_pars globals
     133  joint_internal_function g_pars globals ≝
    125134  λg_pars,globals,fresh_r,insts,src.
    126135  match insts return λx.if is_inl … x then ? else ? → ? → ? with
     
    140149  freshT globals dst_g_pars (localsT dst_g_pars) →
    141150  (* initialized function definition with empty graph *)
    142   joint_internal_function globals dst_g_pars →
     151  joint_internal_function dst_g_pars globals →
    143152  (* functions dictating the translation *)
    144153  (label → joint_step src_g_pars globals →
     
    147156    bind_seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
    148157  (* source function *)
    149   joint_internal_function globals src_g_pars →
     158  joint_internal_function src_g_pars globals →
    150159  (* destination function *)
    151   joint_internal_function globals dst_g_pars ≝
     160  joint_internal_function dst_g_pars globals ≝
    152161  λsrc_g_pars,dst_g_pars,globals,fresh_reg,empty,trans_step,trans_fin_step,def.
    153162  let f : label → joint_statement (src_g_pars : params) globals →
    154     joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝
     163    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
    155164    λlbl,stmt,def.
    156165    match stmt with
     
    167176  ∀globals: list ident.
    168177  (* initialized function definition with empty graph *)
    169   joint_internal_function … dst_g_pars →
     178  joint_internal_function dst_g_pars globals →
    170179  (* functions dictating the translation *)
    171180  (label → joint_step src_g_pars globals →
     
    174183    seq_block dst_g_pars globals (joint_fin_step dst_g_pars)) →
    175184  (* source function *)
    176   joint_internal_function … src_g_pars →
     185  joint_internal_function src_g_pars globals →
    177186  (* destination function *)
    178   joint_internal_function … dst_g_pars ≝
     187  joint_internal_function dst_g_pars globals ≝
    179188  λsrc_g_pars,dst_g_pars,globals,empty,trans_step,trans_fin_step,def.
    180189  let f : label → joint_statement (src_g_pars : params) globals →
    181     joint_internal_function globals dst_g_pars → joint_internal_function globals dst_g_pars ≝
     190    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
    182191    λlbl,stmt,def.
    183192    match stmt with
  • src/joint/blocks.ma

    r2186 r2214  
    22include "utilities/bindLists.ma".
    33
    4 inductive block_step (p : stmt_params) (globals : list ident) : Type[0] ≝
     4(* inductive block_step (p : stmt_params) (globals : list ident) : Type[0] ≝
    55  | block_seq : joint_seq p globals → block_step p globals
    66  | block_skip : label → block_step p globals.
     
    4040
    4141definition skip_block ≝ λp,globals,A.
    42   (list (block_step p globals)) × A.
     42  (list (block_step p globals)) × A.*)
    4343
    4444definition seq_block ≝ λp : stmt_params.λglobals,A.
    4545  (list (joint_seq p globals)) × A.
    4646
    47 definition seq_to_skip_block :
     47(*definition seq_to_skip_block :
    4848  ∀p,g,A.seq_block p g A → skip_block p g A
    4949 ≝ λp,g,A,b.〈\fst b, \snd b〉.
     
    5151coercion skip_from_seq_block :
    5252  ∀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 ???.
     53  seq_to_skip_block on _b : seq_block ??? to skip_block ???.*)
    5454
    5555definition bind_seq_block ≝ λp : stmt_params.λglobals,A.
     
    7070bind_seq_list p g ≡ bind_new R L.
    7171
    72 definition bind_skip_block ≝ λp : stmt_params.λglobals,A.
     72(*definition bind_skip_block ≝ λp : stmt_params.λglobals,A.
    7373  bind_new (localsT p) (skip_block p globals A).
    7474unification hint 0 ≔ p : stmt_params, g, A;
     
    8484coercion bind_skip_from_seq_block :
    8585  ∀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 ???.
     86  bind_seq_to_skip_block on _b : bind_seq_block ??? to bind_skip_block ???.*)
    8787(*
    8888definition block_classifier ≝
  • src/joint/linearise.ma

    r2200 r2214  
    652652  ∀p : unserialized_params.
    653653  ∀globals.
    654     joint_internal_function globals (mk_graph_params p)
    655     joint_internal_function globals (mk_lin_params p)
     654    joint_internal_function (mk_graph_params p) globals
     655    joint_internal_function (mk_lin_params p) globals
    656656     (* ∃sigma : identifier_map LabelTag ℕ.
    657657        let g ≝ joint_if_code ?? (pi1 … fin) in
     
    670670                    (stmt_implicit_label … s)) (nth_opt … n c)*) ≝
    671671  λp,globals,f_in.
    672   mk_joint_internal_function globals (mk_lin_params p)
     672  mk_joint_internal_function (mk_lin_params p) globals
    673673   (joint_if_luniverse ?? f_in) (joint_if_runiverse ?? f_in)
    674674   (joint_if_result ?? f_in) (joint_if_params ?? f_in) (joint_if_locals ?? f_in)
  • src/joint/semanticsUtils_paolo.ma

    r2208 r2214  
    124124definition make_sem_graph_params :
    125125  ∀pars : graph_params.
    126   ∀g_pars : more_sem_genv_params pars.
     126  ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars).
    127127  sem_params ≝
    128128  λpars,g_pars.
     
    163163definition make_sem_lin_params :
    164164  ∀pars : lin_params.
    165   ∀g_pars : more_sem_genv_params pars.
     165  ∀g_pars : more_sem_unserialized_params pars (joint_internal_function pars).
    166166  sem_params ≝
    167167  λpars,g_pars.
  • src/joint/semantics_paolo.ma

    r2200 r2214  
    1212   only the head is kept (or Undef if the list is empty) ??? *)
    1313
    14 definition genv ≝ λglobals.λp:params. genv_t (joint_function globals p).
     14definition genv ≝ λp:params.λglobals.genv_t (joint_function p globals).
    1515definition cpointer ≝ Σp.ptype p = Code.
    1616definition xpointer ≝ Σp.ptype p = XData.
     
    6868 ∀pars : params.
    6969 ∀globals.
    70   genv globals pars →
     70  genv pars globals →
    7171  block →
    72   res (joint_internal_function … pars) ≝
    73   λpars,blobals,ge,b.
     72  res (joint_internal_function pars globals) ≝
     73  λpars,globals,ge,b.
    7474  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
    7575  match def with
     
    8181 ∀pars : params.
    8282 ∀globals.
    83   genv globals pars →
     83  genv pars globals →
    8484  cpointer →
    85   res (joint_internal_function … pars) ≝
     85  res (joint_internal_function pars globals) ≝
    8686 λpars,globals,ge,p.function_of_block pars globals ge (pblock p).
    8787
    88 inductive step_flow (p : params) (globals : list ident) : possible_flows → Type[0] ≝
    89   | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p globals (Labels lbls) (* used for goto-like flow alteration *)
    90   | Init     : Z → joint_internal_function globals p → call_args p → call_dest p → step_flow p globals Call (* call a function with given id, then proceed *)
    91   | Proceed  : ∀flows.step_flow p globals flows. (* go to implicit successor *)
    92 
    93 (*
    94 definition step_flow_cons : ∀p,globals,l,lbls.
    95   step_flow p globals lbls → step_flow p globals (l :: lbls) ≝
    96   λp,globals,l1,l2,flow.match flow with
    97   [ Redirect l ⇒ Redirect … «l, ?»
    98   | Init id f args dest ⇒ Init … id f args dest
    99   | Proceed ⇒ Proceed ???
    100   ]. cases l /2 by or_intror/ qed.
    101 coercion step_flow_c : ∀p,globals,l1,l2.∀flow : step_flow p globals l2.step_flow p globals (l1::l2) ≝
    102   step_flow_cons on _flow : step_flow ??? to step_flow ?? (cons ???).
    103 
    104 definition step_flow_append_l : ∀p,globals,l1,l2.
    105   step_flow p globals l1 → step_flow p globals (l1 @ l2) ≝
    106   λp,globals,l1,l2,flow.match flow with
    107   [ Redirect l ⇒ Redirect … «l, ?»
    108   | Init id f args dest ⇒ Init … id f args dest
    109   | Proceed ⇒ Proceed ???
    110   ]. cases l /2 by Exists_append_l/ qed.
    111 coercion step_flow_l : ∀p,globals,l1,l2.∀flow : step_flow p globals l1.step_flow p globals (l1@l2) ≝
    112   step_flow_append_l on _flow : step_flow ??? to step_flow ?? (append ???).
    113 
    114 definition step_flow_append_r : ∀p,globals,l1,l2.
    115   step_flow p globals l2 → step_flow p globals (l1 @ l2) ≝
    116   λp,globals,l1,l2,flow.match flow with
    117   [ Redirect l ⇒ Redirect … «l, ?»
    118   | Init id f args dest ⇒ Init … id f args dest
    119   | Proceed ⇒ Proceed ???
    120   ]. cases l /2 by Exists_append_r/ qed.
    121 coercion step_flow_r : ∀p,globals,l1,l2.∀flow : step_flow p globals l2.step_flow p globals (l1@l2) ≝
    122   step_flow_append_r on _flow : step_flow ??? to step_flow ?? (append ???).
    123 *)
    124 
    125 inductive fin_step_flow (p : params) (globals : list ident) : possible_flows → Type[0] ≝
    126   | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p globals (Labels lbls)
    127   | FTailInit : Z → joint_internal_function globals p → call_args p → fin_step_flow p globals Call
    128   | FEnd1  : fin_step_flow p globals (Labels [ ]) (* end flow *)
    129   | FEnd2  : fin_step_flow p globals Call. (* end flow *)
    130 
    131 (*
    132 definition fin_step_flow_cons : ∀p,globals,l,lbls.
    133   fin_step_flow p globals lbls → fin_step_flow p globals (l :: lbls) ≝
    134   λp,globals,l1,l2,flow.match flow with
    135   [ FRedirect l ⇒ FRedirect … «l, ?»
    136   | FTailInit id f args ⇒ FTailInit … id f args
    137   | FEnd ⇒ FEnd ???
    138   ]. cases l /2 by or_intror/ qed.
    139 coercion fin_step_flow_c : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l2.fin_step_flow p globals (l1::l2) ≝
    140   fin_step_flow_cons on _flow : fin_step_flow ??? to fin_step_flow ?? (cons ???).
    141 
    142 definition fin_step_flow_append_l : ∀p,globals,l1,l2.
    143   fin_step_flow p globals l1 → fin_step_flow p globals (l1@l2) ≝
    144   λp,globals,l1,l2,flow.match flow with
    145   [ FRedirect l ⇒ FRedirect … «l, ?»
    146   | FTailInit id f args ⇒ FTailInit … id f args
    147   | FEnd ⇒ FEnd ???
    148   ]. cases l /2 by Exists_append_l/ qed.
    149 coercion fin_step_flow_l : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l1.fin_step_flow p globals (l1@l2) ≝
    150   fin_step_flow_append_l on _flow : fin_step_flow ??? to fin_step_flow ?? (append ???).
    151 
    152 definition fin_step_flow_append_r : ∀p,globals,l1,l2.
    153   fin_step_flow p globals l2 → fin_step_flow p globals (l1@l2) ≝
    154   λp,globals,l1,l2,flow.match flow with
    155   [ FRedirect l ⇒ FRedirect … «l, ?»
    156   | FTailInit id f args ⇒ FTailInit … id f args
    157   | FEnd ⇒ FEnd ???
    158   ]. cases l /2 by Exists_append_r/ qed.
    159 coercion fin_step_flow_r : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l2.fin_step_flow p globals (l1@l2) ≝
    160   fin_step_flow_append_r on _flow : fin_step_flow ??? to fin_step_flow ?? (append ???).
    161 *)
    162 
    163 record more_sem_unserialized_params (uns_pars : unserialized_params) : Type[1] ≝
    164   { st_pars :> sem_state_params
     88inductive step_flow (p : step_params) (F : Type[0]) : possible_flows → Type[0] ≝
     89  | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p F (Labels lbls) (* used for goto-like flow alteration *)
     90  | Init     : Z → F → call_args p → call_dest p → step_flow p F Call (* call a function with given id, then proceed *)
     91  | Proceed  : ∀flows.step_flow p F flows. (* go to implicit successor *)
     92
     93inductive fin_step_flow (p : step_params) (F : Type[0]) : possible_flows → Type[0] ≝
     94  | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p F (Labels lbls)
     95  | FTailInit : Z → F → call_args p → fin_step_flow p F Call
     96  | FEnd1  : fin_step_flow p F (Labels [ ]) (* end flow *)
     97  | FEnd2  : fin_step_flow p F Call. (* end flow *)
     98
     99record more_sem_unserialized_params
     100  (uns_pars : unserialized_params)
     101  (F : list ident → Type[0]) : Type[1] ≝
     102  { st_pars :> sem_state_params (* automatic coercion has issues *)
    165103  ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
    166104  ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval
     
    181119  ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars
    182120  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
    183   ; save_frame: cpointer → call_dest uns_pars → state st_pars → framesT st_pars
     121  ; save_frame: cpointer → call_dest uns_pars → state st_pars → res (state st_pars)
    184122   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
    185123     type of arguments. To be fixed using a dependent type *)
     
    191129  ; call_args_for_main: call_args uns_pars
    192130  ; call_dest_for_main: call_dest uns_pars
    193  }.
     131
     132  (* from now on, parameters that use the type of functions *)
     133  ; read_result: ∀globals.genv_t (fundef (F globals)) → state st_pars → res (list beval)
     134  (* change of pc must be left to *_flow execution *)
     135  ; eval_ext_seq: ∀globals.genv_t (fundef (F globals)) → ext_seq uns_pars →
     136      state st_pars → IO io_out io_in (state st_pars)
     137  ; eval_ext_tailcall : ∀globals.genv_t (fundef (F globals)) → ext_tailcall uns_pars →
     138      state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars))
     139  ; eval_ext_call: ∀globals.genv_t (fundef (F globals)) → ∀s : ext_call uns_pars.
     140      state st_pars →
     141      IO io_out io_in ((step_flow uns_pars (F globals) Call)×(state st_pars))
     142  ; pop_frame: ∀globals.genv_t (fundef (F globals)) → state st_pars → res (state st_pars)
     143  }.
     144
     145(*coercion msu_pars_to_ss_pars nocomposites :
     146∀p,F.∀msup : more_sem_unserialized_params p F.sem_state_params
     147 ≝ st_pars
     148on _msup : more_sem_unserialized_params ?? to sem_state_params.*)
    194149
    195150
    196151definition helper_def_retrieve :
    197   ∀X : ? → ? → Type[0].
    198   (∀up.∀p:more_sem_unserialized_params up. regsT p → X up p → res beval) →
    199   ∀up.∀p : more_sem_unserialized_params up.state p → X up p → res beval ≝
    200     λX,f,up,p,st.f ? p (regs … st).
     152  ∀X : ? → ? → ? → Type[0].
     153  (∀up,F.∀p:more_sem_unserialized_params up F. regsT (st_pars up F p) → X up F p → res beval) →
     154  ∀up,F.∀p : more_sem_unserialized_params up F.state (st_pars up F p) → X up F p → res beval ≝
     155    λX,f,up,F,p,st.f ?? p (regs … st).
    201156
    202157definition helper_def_store :
    203   ∀X : ? → ? → Type[0].
    204   (∀up.∀p : more_sem_unserialized_params up.X up p → beval → regsT p → res (regsT p)) →
    205   ∀up.∀p : more_sem_unserialized_params up.X up p → beval → state p → res (state p) ≝
    206   λX,f,up,p,x,v,st.! r ← f ? p x v (regs … st) ; return set_regs … r st.
     158  ∀X : ? → ? → ? → Type[0].
     159  (∀up,F.∀p : more_sem_unserialized_params up F.X up F p → beval → regsT (st_pars … p) → res (regsT (st_pars … p))) →
     160  ∀up,F.∀p : more_sem_unserialized_params up F.X up F p → beval → state (st_pars … p) → res (state (st_pars … p)) ≝
     161  λX,f,up,F,p,x,v,st.! r ← f ?? p x v (regs … st) ; return set_regs … r st.
    207162
    208163definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_.
     
    219174definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_.
    220175definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_.
    221 definition pair_reg_move : ?→?→?→?→? 
    222   λup.λp : more_sem_unserialized_params up.λst : state p.λpm : pair_move up.
    223     ! r ← pair_reg_move_ ? p (regs ? st) pm;
     176definition pair_reg_move
     177  λup,F.λp : more_sem_unserialized_params up F.λst : state (st_pars … p).λpm : pair_move up.
     178    ! r ← pair_reg_move_ ?? p (regs ? st) pm;
    224179    return set_regs ? r st.
    225180
    226181 
    227182axiom BadPointer : String.
    228  
     183
    229184(* this is preamble to all calls (including tail ones). The optional argument in
    230185   input tells the function whether it has to save the frame for internal
     
    235190   serialization and on whether the call is a tail one. *)
    236191definition eval_call_block:
    237  ∀globals.∀p : params.∀p':more_sem_unserialized_params p.
    238   genv globals p → state p' → block → call_args p → call_dest p →
    239     IO io_out io_in ((step_flow p globals Call)×(state p')) ≝
    240  λglobals,p,p',ge,st,b,args,dest.
    241   ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ge b) : IO ? io_in ?);
     192 ∀p,F.∀p':more_sem_unserialized_params p F.∀globals.
     193  genv_t (fundef (F globals)) → state (st_pars ?? p') → block → call_args p → call_dest p →
     194    IO io_out io_in ((step_flow p (F globals) Call)×(state (st_pars ?? p'))) ≝
     195 λp,F,p',globals,ge,st,b,args,dest.
     196  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
    242197    match fd with
    243     [ Internal fn
    244       return 〈Init … (block_id b) fn args dest, st〉
     198    [ Internal fd
     199      return 〈Init ?? (block_id b) fd args dest, st〉
    245200    | External fn ⇒
    246201      ! params ← fetch_external_args … p' fn st : IO ???;
     
    289244  return 〈st'', pr〉.
    290245
    291 (* parameters that need full params to have type of functions,
    292    but are still independent of serialization *)
    293 record more_sem_genv_params (pp : params) : Type[1] ≝
    294   { msu_pars :> more_sem_unserialized_params pp
    295   ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval)
    296   (* change of pc must be left to *_flow execution *)
    297   ; eval_ext_seq: ∀globals.genv globals pp → ext_seq pp →
    298       state msu_pars → IO io_out io_in (state msu_pars)
    299   ; eval_ext_tailcall : ∀globals.genv globals pp → ext_tailcall pp →
    300       state msu_pars → IO io_out io_in ((fin_step_flow pp globals Call)×(state msu_pars))
    301   ; eval_ext_call: ∀globals.genv globals pp →∀s : ext_call pp.
    302       state msu_pars →
    303       IO io_out io_in ((step_flow pp globals Call)×(state msu_pars))
    304   ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars)
    305   }.
    306 
    307246(* parameters that are defined by serialization *)
    308247record more_sem_params (pp : params) : Type[1] ≝
    309   { msg_pars :> more_sem_genv_params pp
     248  { msu_pars :> more_sem_unserialized_params pp (joint_internal_function pp)
    310249  ; offset_of_point : code_point pp → option offset (* can overflow *)
    311250  ; point_of_offset : offset → code_point pp
     
    315254    ∀o.offset_of_point (point_of_offset o) = Some ? o
    316255  }.
     256
     257(*
     258coercion ms_pars_to_msu_pars nocomposites :
     259∀p : params.∀msp : more_sem_params p.more_sem_unserialized_params p (λglobals.joint_internal_function globals p)
     260 ≝ msu_pars
     261on _msp : more_sem_params ? to more_sem_unserialized_params ??.
     262
     263definition ss_pars_of_ms_pars ≝
     264  λp.λpp : more_sem_params p.
     265  st_pars … (msu_pars … pp).
     266coercion ms_pars_to_ss_pars nocomposites :
     267∀p : params.∀msp : more_sem_params p.sem_state_params ≝
     268ss_pars_of_ms_pars on _msp : more_sem_params ? to sem_state_params.*)
    317269
    318270axiom CodePointerOverflow : String.
     
    374326
    375327definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
    376   genv globals p → cpointer → res (joint_statement p globals) ≝
     328  genv p globals → cpointer → res (joint_statement p globals) ≝
    377329  λp,msp,globals,ge,ptr.
    378330  let pt ≝ point_of_pointer ? msp ptr in
     
    381333 
    382334definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
    383   genv globals p → cpointer → label → res cpointer ≝
     335  genv p globals → cpointer → label → res cpointer ≝
    384336  λp,msp,globals,ge,ptr,lbl.
    385337  ! fn ← fetch_function … ge ptr ;
     
    399351  }.
    400352
     353(* definition msu_pars_of_s_pars :
     354∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p))
     355≝ λp : sem_params.
     356  msu_pars … (more_sem_pars p).
     357coercion s_pars_to_msu_pars nocomposites :
     358∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p)) ≝
     359msu_pars_of_s_pars
     360on p : sem_params to more_sem_unserialized_params ??.
     361
     362definition ss_pars_of_s_pars :
     363∀p : sem_params.sem_state_params
     364≝ λp : sem_params.
     365  st_pars … (msu_pars … (more_sem_pars p)).
     366coercion s_pars_to_ss_pars nocomposites :
     367∀p : sem_params.sem_state_params ≝
     368ss_pars_of_s_pars
     369on _p : sem_params to sem_state_params.
     370
     371definition ms_pars_of_s_pars :
     372∀p : sem_params.more_sem_params (spp p)
     373≝ more_sem_pars.
     374coercion s_pars_to_ms_pars nocomposites :
     375∀p : sem_params.more_sem_params (spp p) ≝
     376ms_pars_of_s_pars
     377on p : sem_params to more_sem_params ?.*)
     378
    401379(* definition address_of_label: ∀globals. ∀p:sem_params.
    402380  genv globals p → pointer → label → res address ≝
     
    405383  OK … (address_of_code_pointer newptr). *)
    406384
    407 definition goto: ∀globals. ∀p:sem_params.
    408   genv globals p → label → state p → cpointer → res (state_pc p) ≝
     385definition goto: ∀globals.∀p : sem_params.
     386  genv p globals → label → state p → cpointer → res (state_pc p) ≝
    409387 λglobals,p,ge,l,st,b.
    410388  ! newpc ← pointer_of_label ? p … ge b l ;
     
    427405
    428406definition eval_seq_no_pc :
    429  ∀globals.∀p:sem_params. genv globals p → state p →
     407 ∀globals.∀p:sem_params. genv p globals → state p →
    430408  ∀s:joint_seq p globals.
    431409  IO io_out io_in (state p) ≝
     
    433411  match seq return λx.IO ??? with
    434412  [ extension_seq c ⇒
    435     eval_ext_seq ??? ge c st
     413    eval_ext_seq ge c st
    436414  | LOAD dst addrl addrh ⇒
    437415    ! vaddrh ← dph_arg_retrieve … st addrh ;
     
    484462  | POP dst ⇒
    485463    ! 〈st',v〉 ← pop p st;
    486     acca_store p p dst v st'
     464    acca_store p dst v st'
    487465  | PUSH src ⇒
    488466    ! v ← acca_arg_retrieve … st src;
     
    495473    return st'
    496474  | extension_call s ⇒
    497     !〈flow, st'〉 ← eval_ext_call ??? ge s st ;
     475    !〈flow, st'〉 ← eval_ext_call ge s st ;
    498476    return st'
    499477  | _ ⇒ return st
     
    504482
    505483definition eval_seq_pc :
    506  ∀globals.∀p:sem_params. genv globals p → state p →
     484 ∀globals.∀p:sem_params. genv p globals → state p →
    507485  ∀s:joint_seq p globals.
    508   IO io_out io_in (step_flow p globals (step_flows … s)) ≝
     486  IO io_out io_in (step_flow p ? (step_flows … s)) ≝
    509487  λg,p,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with
    510488  [ CALL_ID id args dest ⇒
     
    513491    return flow
    514492  | extension_call s ⇒
    515     !〈flow, st'〉 ← eval_ext_call ??? ge s st ;
     493    !〈flow, st'〉 ← eval_ext_call ge s st ;
    516494    return flow
    517495  | _ ⇒ return Proceed ???
     
    519497
    520498definition eval_step :
    521  ∀globals.∀p:sem_params. genv globals p → state p →
     499 ∀globals.∀p:sem_params. genv p globals → state p →
    522500  ∀s:joint_step p globals.
    523   IO io_out io_in ((step_flow p globals (step_flows … s))×(state p)) ≝
     501  IO io_out io_in ((step_flow p ? (step_flows … s))×(state p)) ≝
    524502  λglobals,p,ge,st,s.
    525503  match s return λx.IO ?? ((step_flow ?? (step_flows … x))×?) with
     
    538516  %1 % qed.
    539517
    540 definition eval_fin_step_no_pc : ∀globals: list ident.∀p:sem_params. genv globals p
     518definition eval_fin_step_no_pc : ∀globals: list ident.∀p:sem_params. genv p globals
    541519  state p → ∀s : joint_fin_step p.
    542520  IO io_out io_in (state p) ≝
     
    544522  match s return λx.IO ??? with
    545523    [ tailcall c ⇒
    546       !〈flow,st'〉 ← eval_ext_tailcall ??? ge c st ;
     524      !〈flow,st'〉 ← eval_ext_tailcall ge c st ;
    547525      return st'
    548526    | _ ⇒ return st
     
    550528
    551529definition eval_fin_step_pc :
    552  ∀globals.∀p:sem_params. genv globals p → state p →
     530 ∀globals.∀p:sem_params. genv p globals → state p →
    553531  ∀s:joint_fin_step p.
    554   IO io_out io_in (fin_step_flow p globals (fin_step_flows … s)) ≝
     532  IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝
    555533  λg,p,ge,st,s.
    556534  match s return λx.IO ?? (fin_step_flow ?? (fin_step_flows … x)) with
    557535  [ tailcall c ⇒
    558     !〈flow,st'〉 ← eval_ext_tailcall ??? ge c st ;
     536    !〈flow,st'〉 ← eval_ext_tailcall ge c st ;
    559537    return flow 
    560538  | GOTO l ⇒ return FRedirect … l
     
    562540  ]. %1 % qed.
    563541
    564 definition do_call : ∀globals: list ident.∀p:sem_params. genv globals p
    565   state p → Z → joint_internal_function globals p → call_args p →
     542definition do_call : ∀globals: list ident.∀p:sem_params. genv p globals
     543  state p → Z → joint_internal_function p globals → call_args p →
    566544  res (state_pc p) ≝
    567545  λglobals,p,ge,st,id,fn,args.
    568546    ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
    569547              args st ;
    570     let regs ≝ foldr ?? (allocate_local p p) (regs … st) (joint_if_locals … fn) in
     548    let regs ≝ foldr ?? (allocate_local p) (regs … st) (joint_if_locals … fn) in
    571549    let l' ≝ joint_if_entry … fn in
    572550    let st' ≝ set_regs p regs st in
     
    577555(* The pointer provided is the one to the *next* instruction. *)
    578556definition eval_step_flow :
    579  ∀globals.∀p:sem_params.∀flows.genv globals p
    580  state p → cpointer → step_flow p globals flows → res (state_pc p) ≝
     557 ∀globals.∀p:sem_params.∀flows.genv p globals
     558 state p → cpointer → step_flow p ? flows → res (state_pc p) ≝
    581559 λglobals,p,flows,ge,st,nxt,cmd.
    582560 match cmd with
     
    584562    goto … ge l st nxt
    585563  | Init id fn args dest ⇒
    586     let st' ≝ set_frms … (save_frame … nxt dest st) st in
     564    ! st' ← save_frame … nxt dest st ;
    587565    do_call ?? ge st' id fn args
    588566  | Proceed _ ⇒
     
    590568  ].
    591569
    592 definition eval_fin_step_flow : ∀globals: list ident.∀p:sem_params.∀flows. genv globals p
    593   state p → cpointer → fin_step_flow p globals flows → res (state_pc p) ≝
     570definition eval_fin_step_flow : ∀globals: list ident.∀p:sem_params.∀flows. genv p globals
     571  state p → cpointer → fin_step_flow p ? flows → res (state_pc p) ≝
    594572  λglobals,p,lbls,ge,st,curr,cmd.
    595573  match cmd with
     
    604582
    605583definition eval_statement :
    606  ∀globals.∀p:sem_params.genv globals p
     584 ∀globals.∀p:sem_params.genv p globals
    607585  state_pc p → joint_statement p globals →
    608586    IO io_out io_in (state_pc p) ≝
     
    619597 ].
    620598
    621 definition eval_state : ∀globals: list ident.∀p:sem_params. genv globals p
     599definition eval_state : ∀globals: list ident.∀p:sem_params. genv p globals
    622600  state_pc p → IO io_out io_in (state_pc p) ≝
    623601  λglobals,p,ge,st.
     
    629607  not static... *)
    630608definition is_final: ∀globals:list ident. ∀p: sem_params.
    631   genv globals p → cpointer → state_pc p → option int ≝
     609  genv p globals → cpointer → state_pc p → option int ≝
    632610 λglobals,p,ge,exit,st.res_to_opt ? (
    633611  do s ← fetch_statement ? p … ge (pc … st);
Note: See TracChangeset for help on using the changeset viewer.