Changeset 2214 for src/joint/blocks.ma


Ignore:
Timestamp:
Jul 19, 2012, 2:42:02 PM (8 years ago)
Author:
tranquil
Message:
  • changed order of parameters of joint_internal_function and genv in semantics
  • in semantics, unified more_sem_unserialized_params and more_sem_genv_params
  • renamed all <language>_params to <LANGUAGE>
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/blocks.ma

    r2186 r2214  
    22include "utilities/bindLists.ma".
    33
    4 inductive block_step (p : stmt_params) (globals : list ident) : Type[0] ≝
     4(* inductive block_step (p : stmt_params) (globals : list ident) : Type[0] ≝
    55  | block_seq : joint_seq p globals → block_step p globals
    66  | block_skip : label → block_step p globals.
     
    4040
    4141definition skip_block ≝ λp,globals,A.
    42   (list (block_step p globals)) × A.
     42  (list (block_step p globals)) × A.*)
    4343
    4444definition seq_block ≝ λp : stmt_params.λglobals,A.
    4545  (list (joint_seq p globals)) × A.
    4646
    47 definition seq_to_skip_block :
     47(*definition seq_to_skip_block :
    4848  ∀p,g,A.seq_block p g A → skip_block p g A
    4949 ≝ λp,g,A,b.〈\fst b, \snd b〉.
     
    5151coercion skip_from_seq_block :
    5252  ∀p,g,A.∀b : seq_block p g A.skip_block p g A ≝
    53   seq_to_skip_block on _b : seq_block ??? to skip_block ???.
     53  seq_to_skip_block on _b : seq_block ??? to skip_block ???.*)
    5454
    5555definition bind_seq_block ≝ λp : stmt_params.λglobals,A.
     
    7070bind_seq_list p g ≡ bind_new R L.
    7171
    72 definition bind_skip_block ≝ λp : stmt_params.λglobals,A.
     72(*definition bind_skip_block ≝ λp : stmt_params.λglobals,A.
    7373  bind_new (localsT p) (skip_block p globals A).
    7474unification hint 0 ≔ p : stmt_params, g, A;
     
    8484coercion bind_skip_from_seq_block :
    8585  ∀p,g,A.∀b:bind_seq_block p g A.bind_skip_block p g A ≝
    86   bind_seq_to_skip_block on _b : bind_seq_block ??? to bind_skip_block ???.
     86  bind_seq_to_skip_block on _b : bind_seq_block ??? to bind_skip_block ???.*)
    8787(*
    8888definition block_classifier ≝
Note: See TracChangeset for help on using the changeset viewer.