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)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.