Changeset 1247 for src/joint

Timestamp:

Sep 22, 2011, 3:03:41 AM (8 years ago)

Author:

sacerdot

Message:

Code (almost) ported to latest joint/Joint.ma datatype.
I still need to figure out the new unification hint...

File:

• src/joint/semantics.ma (modified) (11 diffs)

src/joint/semantics.ma

@@ -17 +17 @@
   eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).
 
-record more_sem_params (p:params): Type[1] ≝
+record more_sem_params (p:params_): Type[1] ≝
  { framesT: Type[0]
  ; regsT: Type[0] (* regs = pseudo-registers + hw registers *)
@@ -41 +41 @@
 
 record sem_params: Type[1] ≝
- { spp :> params
+ { spp :> params_
  ; more_sem_pars :> more_sem_params spp
  }.
@@ -54 +54 @@
  }.
 
-definition genv ≝ λp:params.λglobals. (genv_t Genv) (joint_function p globals).
+definition genv ≝ λglobals.λp:params globals. (genv_t Genv) (joint_function globals p).
 
 (*
@@ -63 +63 @@
 *)
 
-record more_sem_params2 (p: params) (globals: list ident): Type[1] ≝
+record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] ≝
  { more_sparams:> more_sem_params p
  
@@ -71 +71 @@
  ; fetch_result: state (mk_sem_params … more_sparams) → nat → res val
 
- ; exec_extended: genv p globals → extend_statements (mk_sem_params … more_sparams) → state (mk_sem_params … more_sparams) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams)))
+ ; exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams) → state (mk_sem_params … more_sparams) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams)))
  }.
 
 record sem_params2 (globals: list ident): Type[1] ≝
- { p2:> params
- ; more_sparams2:> more_sem_params2 p2 globals
+ { p2:> params globals
+ ; more_sparams2:> more_sem_params2 globals p2
  }.
 
@@ -82 +82 @@
 coercion sem_params_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params
  ≝ sem_params_of_sem_params2 on _x: sem_params2 ? to sem_params.
-
+(*
 unification hint  0 ≔ globals: (list ident), p: sem_params2 globals;
    S ≟ sem_params_of_sem_params2 globals p
@@ -89 +89 @@
     (more_sparams (p2 globals p) globals
     (more_sparams2 globals p)))) ≡ spp__o__pars_ S.
-
+*)
 definition address_of_label: sem_params → label → address.
  #p #l generalize in match (refl … (beval_pair_of_pointer (pointer_of_label … p l)))
@@ -211 +211 @@
 coercion pi1: ∀A.∀P:A → Prop.∀p:(Σx:A. P x).A ≝ pi1 on _p:Σx:?.? to ?.
 
-definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv p globals → state p → IO io_out io_in (trace × (state p)) ≝
+definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv globals p → state p → IO io_out io_in (trace × (state p)) ≝
  λglobals,p,ge,st.
   ! s ← fetch_statement … st;
@@ -336 +336 @@
  ; exit: address
  ; registersno: nat
- ; genv2: genv sparams2 globals
+ ; genv2: genv globals sparams2
  }.
 
@@ -345 +345 @@
 
 definition make_global :
- ∀pars:params. ∀sparams:∀p: joint_program pars. more_sem_params2 pars (prog_var_names … p).
+ ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
   joint_program pars → evaluation_parameters
 ≝
  λpars,sparams.
   (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) ?? (globalenv Genv … (λx.[Init_space x]) p)).
-[1,2: cases daemon ]
+[1,2: cases daemon (*CSC: XXXXXXXXXXXXX*) ]
 qed.
 
 definition make_initial_state :
- ∀pars:params. ∀sparams:∀p: joint_program pars. more_sem_params2 pars (prog_var_names … p).
- ∀p: joint_program … pars. res (state (mk_sem_params pars (sparams p))) ≝
+ ∀pars:∀globals.params globals. ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
+ ∀p: joint_program … pars. res (state (mk_sem_params (pars (prog_var_names … p)) (sparams p))) ≝
 λpars,sparams,p.
   let ge ≝ genv2 (make_global pars sparams p) in
@@ -376 +376 @@
 
 definition joint_fullexec :
- ∀pars:params.
- ∀sparams:∀p: joint_program pars. more_sem_params2 pars (prog_var_names … p).
+ ∀pars:∀globals.params globals.
+ ∀sparams:∀p: joint_program pars. more_sem_params2 … (pars (prog_var_names … p)).
  fullexec io_out io_in ≝
  λpars,sparams.