Changeset 1949 for src/joint/Joint_paolo.ma

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:

• src/joint/Joint_paolo.ma (modified) (4 diffs)

src/joint/Joint_paolo.ma

@@ -74 +74 @@
   | extension: ext_step p → joint_step p globals.
 
+axiom EmptyString : String.
+definition NOOP ≝ λp,globals.COMMENT p globals EmptyString.
+
 notation "r ← a1 .op. a2" with precedence 60 for
   @{'op2 $op $r $a1 $a2}.
@@ -124 +127 @@
   }. 
 
+inductive joint_fin_step (p: stmt_params) (globals: list ident): Type[0] ≝
+  | GOTO: label → joint_fin_step p globals
+  | RETURN: joint_fin_step p globals
+  | extension_fin : ext_fin_stmt p → joint_fin_step p globals.
+
 inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
   | sequential: joint_step p globals → succ p → joint_statement p globals
-  | GOTO: label → joint_statement p globals
-  | RETURN: joint_statement p globals
-  | extension_fin : ext_fin_stmt p → joint_statement p globals.
-
-coercion extension_fin_to_stmt : ∀p : stmt_params.∀globals.∀s : ext_fin_stmt p.joint_statement p globals ≝
-  extension_fin on _s : ext_fin_stmt ? to joint_statement ??.
-
-definition no_seq ≝ λp : stmt_params.λglobals.λs : joint_statement p globals.
-  match s with
-  [ sequential _ _ ⇒ False
-  | _ ⇒ True
-  ].
+  | final: joint_fin_step p globals → joint_statement p globals.
+
+coercion extension_fin_to_fin_step : ∀p : stmt_params.∀globals.
+  ∀s : ext_fin_stmt p.joint_fin_step p globals ≝
+  extension_fin on _s : ext_fin_stmt ? to joint_fin_step ??.
+
+coercion fin_step_to_stmt : ∀p : stmt_params.∀globals.
+  ∀s : joint_fin_step p globals.joint_statement p globals ≝
+  final on _s : joint_fin_step ?? to joint_statement ??.
 
 record params : Type[1] ≝
@@ -187 +192 @@
   ].
 
+definition fin_step_labels ≝
+  λp,globals.λs : joint_fin_step p globals.
+  match s with
+  [ GOTO l ⇒ [ l ]
+  | RETURN ⇒ [ ]
+  | extension_fin c ⇒ ext_fin_stmt_labels … c
+  ].
+
 definition stmt_explicit_labels :
   ∀p,globals.
@@ -192 +205 @@
   λp,globals,stmt. match stmt with
   [ sequential c _ ⇒ step_labels … c
-  | GOTO l ⇒ [ l ]
-  | RETURN ⇒ [ ]
-  | extension_fin c ⇒ ext_fin_stmt_labels … c
+  | final c ⇒ fin_step_labels … c
   ].