Ignore:
Timestamp:
May 15, 2012, 5:51:25 PM (9 years ago)
Author:
tranquil
Message:
  • lemma trace rel to eq flatten trace
  • some more properties of generic monad relations and predicates
  • removed 'iff notation from extralib as already there
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint_paolo.ma

    r1908 r1949  
    7474  | extension: ext_step p → joint_step p globals.
    7575
     76axiom EmptyString : String.
     77definition NOOP ≝ λp,globals.COMMENT p globals EmptyString.
     78
    7679notation "r ← a1 .op. a2" with precedence 60 for
    7780  @{'op2 $op $r $a1 $a2}.
     
    124127  }.
    125128
     129inductive joint_fin_step (p: stmt_params) (globals: list ident): Type[0] ≝
     130  | GOTO: label → joint_fin_step p globals
     131  | RETURN: joint_fin_step p globals
     132  | extension_fin : ext_fin_stmt p → joint_fin_step p globals.
     133
    126134inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
    127135  | sequential: joint_step p globals → succ p → joint_statement p globals
    128   | GOTO: label → joint_statement p globals
    129   | RETURN: joint_statement p globals
    130   | extension_fin : ext_fin_stmt p → joint_statement p globals.
    131 
    132 coercion extension_fin_to_stmt : ∀p : stmt_params.∀globals.∀s : ext_fin_stmt p.joint_statement p globals ≝
    133   extension_fin on _s : ext_fin_stmt ? to joint_statement ??.
    134 
    135 definition no_seq ≝ λp : stmt_params.λglobals.λs : joint_statement p globals.
    136   match s with
    137   [ sequential _ _ ⇒ False
    138   | _ ⇒ True
    139   ].
     136  | final: joint_fin_step p globals → joint_statement p globals.
     137
     138coercion extension_fin_to_fin_step : ∀p : stmt_params.∀globals.
     139  ∀s : ext_fin_stmt p.joint_fin_step p globals ≝
     140  extension_fin on _s : ext_fin_stmt ? to joint_fin_step ??.
     141
     142coercion fin_step_to_stmt : ∀p : stmt_params.∀globals.
     143  ∀s : joint_fin_step p globals.joint_statement p globals ≝
     144  final on _s : joint_fin_step ?? to joint_statement ??.
    140145
    141146record params : Type[1] ≝
     
    187192  ].
    188193
     194definition fin_step_labels ≝
     195  λp,globals.λs : joint_fin_step p globals.
     196  match s with
     197  [ GOTO l ⇒ [ l ]
     198  | RETURN ⇒ [ ]
     199  | extension_fin c ⇒ ext_fin_stmt_labels … c
     200  ].
     201
    189202definition stmt_explicit_labels :
    190203  ∀p,globals.
     
    192205  λp,globals,stmt. match stmt with
    193206  [ sequential c _ ⇒ step_labels … c
    194   | GOTO l ⇒ [ l ]
    195   | RETURN ⇒ [ ]
    196   | extension_fin c ⇒ ext_fin_stmt_labels … c
     207  | final c ⇒ fin_step_labels … c
    197208  ].
    198209
Note: See TracChangeset for help on using the changeset viewer.