Ignore:
Timestamp:
Oct 30, 2012, 4:23:09 PM (8 years ago)
Author:
tranquil
Message:

adapted joint to cl_call f

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r2286 r2422  
    1717}.
    1818
    19 definition genv ≝ λp.genv_gen (joint_internal_function p).
     19definition genv ≝ λp.genv_gen (joint_closed_internal_function p).
    2020coercion genv_to_genv_t :
    2121  ∀p,globals.∀g : genv p globals.genv_t (joint_function p globals) ≝
    2222  λp,globals,g.ge ?? g on _g : genv ?? to genv_t ?.
    23 
    2423definition cpointer ≝ Σp.ptype p = Code.
    2524definition xpointer ≝ Σp.ptype p = XData.
    2625unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).
    2726unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer   (λp.ptype p = XData).
     27unification hint 0 ≔ p,g ⊢
     28  joint_closed_internal_function p g ≡
     29  Sig (joint_internal_function p g) (λfd.code_closed p g (joint_if_code p g fd)).
    2830
    2931record sem_state_params : Type[1] ≝
     
    8284  genv pars globals →
    8385  block →
    84   res (joint_internal_function pars globals) ≝
     86  res (joint_closed_internal_function pars globals) ≝
    8587  λpars,globals,ge,b.
    8688  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
     
    9597  genv pars globals →
    9698  cpointer →
    97   res (joint_internal_function pars globals) ≝
     99  res (joint_closed_internal_function pars globals) ≝
    98100 λpars,globals,ge,p.function_of_block pars globals ge (pblock p).
    99101
     
    149151  ; eval_ext_tailcall : ∀globals.genv_gen F globals → ext_tailcall uns_pars →
    150152      F globals → state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars))
     153  ; ext_tailcall_id : ∀globals.genv_gen F globals → ext_tailcall uns_pars →
     154      state st_pars → IO io_out io_in ident
    151155  ; eval_ext_call: ∀globals.genv_gen F globals →
    152156      ext_call uns_pars → state st_pars →
    153157      IO io_out io_in ((step_flow uns_pars (F globals) Call)×(state st_pars))
     158  ; ext_call_id : ∀globals.genv_gen F globals → ext_call uns_pars →
     159      state st_pars → IO io_out io_in ident
    154160  ; pop_frame: ∀globals.genv_gen F globals → F globals → state st_pars → res (state st_pars)
    155161  (* do something more in some op2 calculations (e.g. mark a register for correction
     
    266272(* parameters that are defined by serialization *)
    267273record more_sem_params (pp : params) : Type[1] ≝
    268   { msu_pars :> more_sem_unserialized_params pp (joint_internal_function pp)
     274  { msu_pars :> more_sem_unserialized_params pp (joint_closed_internal_function pp)
    269275  ; offset_of_point : code_point pp → option offset (* can overflow *)
    270276  ; point_of_offset : offset → code_point pp
     
    347353definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
    348354  genv p globals → cpointer →
    349   res ((joint_internal_function p globals) × (joint_statement p globals)) ≝
     355  res ((joint_closed_internal_function p globals) × (joint_statement p globals)) ≝
    350356  λp,msp,globals,ge,ptr.
    351357  let pt ≝ point_of_pointer ? msp ptr in
     
    427433
    428434definition eval_seq_no_pc :
    429  ∀p:sem_params.∀globals. genv p globals → joint_internal_function p globals →
     435 ∀p:sem_params.∀globals. genv p globals → joint_closed_internal_function p globals →
    430436  state p → ∀s:joint_seq p globals.
    431437  IO io_out io_in (state p) ≝
     
    513519definition eval_step :
    514520 ∀p:sem_params.∀globals. genv p globals →
    515   joint_internal_function p globals → state p →
     521  joint_closed_internal_function p globals → state p →
    516522  ∀s:joint_step p globals.
    517523  IO io_out io_in ((step_flow p ? (step_flows … s))×(state p)) ≝
     
    533539
    534540definition eval_fin_step_no_pc : ∀p:sem_params.∀globals. genv p globals →
    535   (* current function *) joint_internal_function p globals → state p → ∀s : joint_fin_step p.
     541  (* current function *) joint_closed_internal_function p globals → state p → ∀s : joint_fin_step p.
    536542  IO io_out io_in (state p) ≝
    537543 λp,globals,ge,curr_fn,st,s.
     
    544550
    545551definition eval_fin_step_pc :
    546  ∀p:sem_params.∀globals. genv p globals → joint_internal_function p globals → state p →
     552 ∀p:sem_params.∀globals. genv p globals → joint_closed_internal_function p globals → state p →
    547553  ∀s:joint_fin_step p.
    548554  IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝
     
    557563
    558564definition do_call : ∀p:sem_params.∀globals: list ident. genv p globals →
    559   state p → Z → joint_internal_function p globals → call_args p →
     565  state p → Z → joint_closed_internal_function p globals → call_args p →
    560566  res (state_pc p) ≝
    561567  λp,globals,ge,st,id,fn,args.
     
    600606definition eval_statement :
    601607 ∀globals.∀p:sem_params.genv p globals →
    602   state_pc p → joint_internal_function p globals → joint_statement p globals →
     608  state_pc p → joint_closed_internal_function p globals → joint_statement p globals →
    603609    IO io_out io_in (state_pc p) ≝
    604610 λglobals,p,ge,st,curr_fn,stmt.
Note: See TracChangeset for help on using the changeset viewer.