- Timestamp:
- Sep 21, 2011, 11:57:20 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LIN/LIN.ma
r1224 r1233 2 2 3 3 definition lin_params: params ≝ 4 mk_params 5 unit unit unit unit registers_move Register 6 unit unit unit unit. 4 mk_params (mk_params_ unit unit unit unit registers_move Register False unit unit unit) unit. 7 5 8 definition pre_lin_statement ≝ 9 λglobals: list ident. joint_statement lin_params globals. 10 11 definition lin_statement ≝ 12 λglobals. 13 option ident × (pre_lin_statement globals). 6 definition lin_statement ≝ joint_statement lin_params. 14 7 15 8 definition well_formed_P ≝ … … 21 14 match \fst hd with 22 15 [ Some lbl ⇒ False 23 | None ⇒ True 24 ] 25 ]. 16 | None ⇒ True]]. 26 17 18 (* 27 19 definition lin_sem_params_: ∀globals. sem_params_ lin_params globals ≝ 28 20 λglobals. … … 31 23 cases daemon 32 24 qed. 25 *) 33 26 34 definition ltl_program ≝ λglobals. joint_program globals … (lin_sem_params_ globals). 35 36 inductive lin_function_definition (globals: list ident): Type[0] ≝ 37 lin_fu_internal: ∀code: list (lin_statement globals). well_formed_P ? ? code → lin_function_definition globals 38 | lin_fu_external: external_function → lin_function_definition globals. 39 40 record lin_program: Type[0] ≝ 41 { 42 lin_pr_vars: list (ident × nat); 43 lin_pr_funcs: list (ident × (lin_function_definition (map ? ? (fst ? ?) lin_pr_vars))); 44 lin_pr_main: option ident 45 }. 27 definition ltl_program ≝ joint_program lin_params.
Note: See TracChangeset
for help on using the changeset viewer.