Changeset 1949 for src/joint/Joint_paolo.ma
- Timestamp:
- May 15, 2012, 5:51:25 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/Joint_paolo.ma
r1908 r1949 74 74 | extension: ext_step p → joint_step p globals. 75 75 76 axiom EmptyString : String. 77 definition NOOP ≝ λp,globals.COMMENT p globals EmptyString. 78 76 79 notation "r ← a1 .op. a2" with precedence 60 for 77 80 @{'op2 $op $r $a1 $a2}. … … 124 127 }. 125 128 129 inductive 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 126 134 inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝ 127 135 | 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 138 coercion 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 142 coercion 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 ??. 140 145 141 146 record params : Type[1] ≝ … … 187 192 ]. 188 193 194 definition 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 189 202 definition stmt_explicit_labels : 190 203 ∀p,globals. … … 192 205 λp,globals,stmt. match stmt with 193 206 [ 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 197 208 ]. 198 209
Note: See TracChangeset
for help on using the changeset viewer.