Ignore:
Timestamp:
Nov 20, 2012, 6:40:08 PM (7 years ago)
Author:
piccolo
Message:

corrected some inconsistencies
fixed some of lineariseProof

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r2473 r2481  
    143143(* this can replace graph_fetch function and lin_fetch_function *)
    144144definition fetch_function:
    145  ∀pars : params.
    146  ∀globals.
    147  ∀ge : genv pars globals.
     145 ∀F.
     146 ∀ge : genv_t (fundef F).
    148147  program_counter →
    149148  res (Σi.is_internal_function … ge i) ≝
    150  λpars,globals,ge,p.
     149 λpars,ge,p.
    151150 opt_to_res … [MSG BadFunction; MSG BadPointer]
    152151    (int_funct_of_block … ge (pc_block p)).
     
    311310
    312311definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
    313   ∀ge:genv p globals. program_counter →
     312  ∀ge : genv_t (joint_function p globals). program_counter →
    314313  res ((Σi.is_internal_function … ge i) × (joint_statement p globals)) ≝
    315314  λp,msp,globals,ge,ptr.
     
    321320
    322321definition pc_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
    323   genv p globals → program_counter → label → res program_counter ≝
     322  genv_t (joint_function p globals) → program_counter → label → res program_counter ≝
    324323  λp,msp,globals,ge,ptr,lbl.
    325324  ! f ← fetch_function … ge ptr ;
     
    372371  OK … (address_of_code_pointer newptr). *)
    373372
    374 definition goto: ∀globals.∀p : sem_params.
    375   genv p globals → label → state p → program_counter → res (state_pc p) ≝
    376  λglobals,p,ge,l,st,b.
     373definition goto: ∀p : sem_params.∀globals.
     374  genv_t (joint_function p globals) → label → state p → program_counter → res (state_pc p) ≝
     375 λp,globals,ge,l,st,b.
    377376  ! newpc ← pc_of_label ? p … ge b l ;
    378377  return mk_state_pc ? st newpc.
     
    390389
    391390definition function_of_call ≝ λp:sem_params.λglobals.
    392   λge: genv p globals.λst : state p.λf.
     391  λge: genv_t (joint_function p globals).λst : state p.λf.
    393392  match f with
    394393  [ inl id ⇒
     
    413412
    414413definition eval_internal_call_pc ≝
    415 λp : sem_params.λglobals : list ident.λge : genv p globals.λi.
     414λp : sem_params.λglobals : list ident.λge : genv_t (joint_function p globals).λi.
    416415let fn ≝ if_of_function … ge i in
    417416let l' ≝ joint_if_entry ?? fn in
     
    572571qed.
    573572
    574 definition eval_state : ∀globals: list ident.∀p:sem_params. genv p globals →
     573definition eval_state : ∀p:sem_params. ∀globals: list ident.
     574  genv p globals →
    575575  state_pc p → IO io_out io_in (state_pc p) ≝
    576   λglobals,p,ge,st.
     576  λp,globals,ge,st.
    577577  ! 〈fn,s〉 ← fetch_statement ? p … ge (pc … st) : IO ???;
    578578  eval_statement … ge fn st s.
     
    581581  tailcall? Maybe it should rely on an FEnd flow command issued, but that's
    582582  not static... *)
    583 definition is_final: ∀globals:list ident. ∀p: sem_params.
     583definition is_final: ∀p: sem_params.∀globals.
    584584  genv p globals → program_counter → state_pc p → option int ≝
    585  λglobals,p,ge,exit,st.res_to_opt ? (
     585 λp,globals,ge,exit,st.res_to_opt ? (
    586586  do 〈f,s〉 ← fetch_statement ? p … ge (pc … st);
    587587  let fn ≝ if_of_function … f in
Note: See TracChangeset for help on using the changeset viewer.