Changeset 1233 for src/LTL/LTL.ma
- Timestamp:
- Sep 21, 2011, 11:57:20 AM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LTL/LTL.ma
r1222 r1233 3 3 4 4 definition ltl_params: params ≝ 5 mk_params 6 unit unit unit unit registers_move Register 7 unit unit unit unit. 5 mk_params (mk_params_ unit unit unit unit registers_move Register False unit unit unit) label. 8 6 9 definition ltl_statement ≝ λglobals: list ident. joint_statement ltl_params globals.7 definition ltl_statement ≝ joint_statement ltl_params. 10 8 11 definition ltl_sem_params_: ∀globals. sem_params_ ltl_params globals ≝9 (*definition ltl_sem_params_: ∀globals. sem_params_ ltl_params globals ≝ 12 10 λglobals. 13 mk_sem_params_ ltl_params globals (graph (ltl_statement globals)) (lookup …). 11 mk_sem_params_ ltl_params globals (graph (ltl_statement globals)) (lookup …).*) 14 12 15 definition ltl_program ≝ λglobals. joint_program globals … (ltl_sem_params_ globals). 16 (* 17 18 record ltl_internal_function (globals: list ident): Type[0] ≝ 19 { 20 ltl_if_luniverse: universe LabelTag; 21 ltl_if_runiverse: universe RegisterTag; 22 ltl_if_stacksize: nat; 23 ltl_if_graph: ltl_statement_graph globals; 24 ltl_if_entry: Σl: label. lookup ? ? ltl_if_graph l ≠ None ?; 25 ltl_if_exit: Σl: label. lookup ? ? ltl_if_graph l ≠ None ? 26 }. 27 28 inductive ltl_function_definition (globals: list ident): Type[0] ≝ 29 | ltl_fu_internal_function: ltl_internal_function globals → ltl_function_definition globals 30 | ltl_fu_external_function: external_function → ltl_function_definition globals. 31 32 record ltl_program (globals: list (ident × nat)): Type[0] ≝ 33 { 34 ltl_pr_funcs: list (ident × (ltl_function_definition (map ? ? \fst globals))); 35 ltl_pr_main: option ident 36 }. 37 *) 13 definition ltl_program ≝ joint_program ltl_params.
Note: See TracChangeset
for help on using the changeset viewer.