Changeset 1976 for src/joint


Ignore:
Timestamp:
May 21, 2012, 7:04:21 PM (8 years ago)
Author:
tranquil
Message:
  • monads: just changed some defs, which had to be propagated in some files
  • ASM/CostProof.ma: linked cost as defined there to the one in StructuredTraces? that uses fold
  • added a library for permutations of lists (useful with fold AC ops on lists)
  • first draft of abstract_status implementation for joint languages (file joint/as_semantics.ma)
Location:
src/joint
Files:
1 added
2 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint_paolo.ma

    r1949 r1976  
    77include "common/LabelledObjects.ma".
    88include "ASM/Util.ma".
     9include "basics/deqsets.ma".
     10include "basics/finset.ma". (* for DeqNat *)
    911
    1012(* Here is the structure of parameter records (downward edges are coercions,
     
    147149 { stmt_pars :> stmt_params
    148150 ; codeT: list ident → Type[0]
    149  ; code_point : Type[0]
     151 ; code_point : DeqSet
    150152 ; stmt_at : ∀globals.codeT globals → code_point → option (joint_statement stmt_pars globals)
    151153 ; point_of_label : ∀globals.codeT globals → label → option code_point
     
    290292      (mk_stmt_params lp unit (λ_.None ?))
    291293    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
    292     (* code_point ≝ *)
     294    (* code_point ≝ *)DeqNat
    293295    (* stmt_at ≝ *)(λglobals,code,point.! ls ← nth_opt ? point code ; return \snd ls)
    294296    (* point_of_label ≝ *)(λglobals,c,lbl.
     
    325327  { g_u_pars :> unserialized_params }.
    326328
    327 (* move *)
    328 definition lookup_safe : ∀tag,A.∀m : identifier_map tag A.∀i.i ∈ m → A ≝
    329   λtag,A,m.match m return λx : identifier_map tag A.∀i.i ∈ x → ? with
    330   [ an_id_map m' ⇒ λi.match i return λx.x ∈ an_id_map ?? m' → ? with
    331     [ an_identifier i' ⇒
    332       match lookup_opt … i' m' return λx.match x with [Some y ⇒ true | None ⇒ false] → ? with
    333       [ Some y ⇒ λ_.y
    334       | None ⇒ Ⓧ
    335       ]
    336     ]
    337   ].
    338  
    339 lemma lookup_safe_elim : ∀tag,A.∀P : A → Prop.∀m,i,prf.
    340   (∀x.lookup tag A m i = Some ? x → P x) → P (lookup_safe tag A m i prf).
    341 #tag #A #P *#m *#i normalize elim (lookup_opt A i m) normalize
    342 [ * ]
    343 #s * #H @H %
    344 qed.
    345 
    346329(* One common instantiation of params via Graphs of joint_statements
    347330   (all languages but LIN) *)
     
    351334      (mk_stmt_params gp label (Some ?))
    352335    (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
    353     (* code_point ≝ *)label
     336    (* code_point ≝ *)(Deq_identifier LabelTag)
    354337    (* stmt_at ≝ *)(λglobals,code.lookup LabelTag ? code)
    355338    (* point_of_label ≝ *)(λ_.λ_.λlbl.return lbl)
  • src/joint/semantics_paolo.ma

    r1949 r1976  
    9090  | Proceed  : step_flow p globals labels. (* go to implicit successor *)
    9191
     92definition step_flow_cons : ∀p,globals,l,lbls.
     93  step_flow p globals lbls → step_flow p globals (l :: lbls) ≝
     94  λp,globals,l1,l2,flow.match flow with
     95  [ Redirect l ⇒ Redirect … «l, ?»
     96  | Init id f args dest ⇒ Init … id f args dest
     97  | Proceed ⇒ Proceed ???
     98  ]. cases l /2 by or_intror/ qed.
     99coercion step_flow_c : ∀p,globals,l1,l2.∀flow : step_flow p globals l2.step_flow p globals (l1::l2) ≝
     100  step_flow_cons on _flow : step_flow ??? to step_flow ?? (cons ???).
     101
     102definition step_flow_append_l : ∀p,globals,l1,l2.
     103  step_flow p globals l1 → step_flow p globals (l1 @ l2) ≝
     104  λp,globals,l1,l2,flow.match flow with
     105  [ Redirect l ⇒ Redirect … «l, ?»
     106  | Init id f args dest ⇒ Init … id f args dest
     107  | Proceed ⇒ Proceed ???
     108  ]. cases l /2 by Exists_append_l/ qed.
     109coercion step_flow_l : ∀p,globals,l1,l2.∀flow : step_flow p globals l1.step_flow p globals (l1@l2) ≝
     110  step_flow_append_l on _flow : step_flow ??? to step_flow ?? (append ???).
     111
     112definition step_flow_append_r : ∀p,globals,l1,l2.
     113  step_flow p globals l2 → step_flow p globals (l1 @ l2) ≝
     114  λp,globals,l1,l2,flow.match flow with
     115  [ Redirect l ⇒ Redirect … «l, ?»
     116  | Init id f args dest ⇒ Init … id f args dest
     117  | Proceed ⇒ Proceed ???
     118  ]. cases l /2 by Exists_append_r/ qed.
     119coercion step_flow_r : ∀p,globals,l1,l2.∀flow : step_flow p globals l2.step_flow p globals (l1@l2) ≝
     120  step_flow_append_r on _flow : step_flow ??? to step_flow ?? (append ???).
     121
    92122inductive fin_step_flow (p : params) (globals : list ident) (labels : list label): Type[0] ≝
    93123  | FRedirect : (Σl.In ? labels l) → fin_step_flow p globals labels
    94124  | FTailInit : Z → joint_internal_function globals p → call_args p → fin_step_flow p globals labels
    95125  | FEnd  : fin_step_flow p globals labels. (* end flow *)
     126
     127definition fin_step_flow_cons : ∀p,globals,l,lbls.
     128  fin_step_flow p globals lbls → fin_step_flow p globals (l :: lbls) ≝
     129  λp,globals,l1,l2,flow.match flow with
     130  [ FRedirect l ⇒ FRedirect … «l, ?»
     131  | FTailInit id f args ⇒ FTailInit … id f args
     132  | FEnd ⇒ FEnd ???
     133  ]. cases l /2 by or_intror/ qed.
     134coercion fin_step_flow_c : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l2.fin_step_flow p globals (l1::l2) ≝
     135  fin_step_flow_cons on _flow : fin_step_flow ??? to fin_step_flow ?? (cons ???).
     136
     137definition fin_step_flow_append_l : ∀p,globals,l1,l2.
     138  fin_step_flow p globals l1 → fin_step_flow p globals (l1@l2) ≝
     139  λp,globals,l1,l2,flow.match flow with
     140  [ FRedirect l ⇒ FRedirect … «l, ?»
     141  | FTailInit id f args ⇒ FTailInit … id f args
     142  | FEnd ⇒ FEnd ???
     143  ]. cases l /2 by Exists_append_l/ qed.
     144coercion fin_step_flow_l : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l1.fin_step_flow p globals (l1@l2) ≝
     145  fin_step_flow_append_l on _flow : fin_step_flow ??? to fin_step_flow ?? (append ???).
     146
     147definition fin_step_flow_append_r : ∀p,globals,l1,l2.
     148  fin_step_flow p globals l2 → fin_step_flow p globals (l1@l2) ≝
     149  λp,globals,l1,l2,flow.match flow with
     150  [ FRedirect l ⇒ FRedirect … «l, ?»
     151  | FTailInit id f args ⇒ FTailInit … id f args
     152  | FEnd ⇒ FEnd ???
     153  ]. cases l /2 by Exists_append_r/ qed.
     154coercion fin_step_flow_r : ∀p,globals,l1,l2.∀flow : fin_step_flow p globals l2.fin_step_flow p globals (l1@l2) ≝
     155  fin_step_flow_append_r on _flow : fin_step_flow ??? to fin_step_flow ?? (append ???).
    96156
    97157record more_sem_unserialized_params (uns_pars : unserialized_params) : Type[1] ≝
Note: See TracChangeset for help on using the changeset viewer.