Changeset 1233 for src/LTL/LTL.ma

Timestamp:

Sep 21, 2011, 11:57:20 AM (9 years ago)

Author:

sacerdot

Message:

1) Ported to Brian's new dependent type for fullexec
2) Universe level raised for fullexec and related stuff to accomodate the

joint semantics

3) Improved joint syntax and semantics
4) Code for LTLToLin simplified

File:

• src/LTL/LTL.ma (modified) (1 diff)

src/LTL/LTL.ma

@@ -3 +3 @@
 
 definition ltl_params: params ≝
- mk_params
-   unit unit unit unit registers_move Register
-     unit unit unit unit.
+ mk_params (mk_params_ unit unit unit unit registers_move Register False unit unit unit) label.
 
-definition ltl_statement ≝ λglobals: list ident. joint_statement ltl_params globals.
+definition ltl_statement ≝ joint_statement ltl_params.
 
-definition ltl_sem_params_: ∀globals. sem_params_ ltl_params globals ≝
+(*definition ltl_sem_params_: ∀globals. sem_params_ ltl_params globals ≝
  λglobals.
-  mk_sem_params_ ltl_params globals (graph (ltl_statement globals)) (lookup …).
+  mk_sem_params_ ltl_params globals (graph (ltl_statement globals)) (lookup …).*)
 
-definition ltl_program ≝ λglobals. joint_program globals … (ltl_sem_params_ globals).
-(*
-  
-record ltl_internal_function (globals: list ident): Type[0] ≝
-{
-  ltl_if_luniverse: universe LabelTag;
-  ltl_if_runiverse: universe RegisterTag;
-  ltl_if_stacksize: nat;
-  ltl_if_graph: ltl_statement_graph globals;
-  ltl_if_entry: Σl: label. lookup ? ? ltl_if_graph l ≠ None ?;
-  ltl_if_exit: Σl: label. lookup ? ? ltl_if_graph l ≠ None ?
-}.
-
-inductive ltl_function_definition (globals: list ident): Type[0] ≝
-  | ltl_fu_internal_function: ltl_internal_function globals → ltl_function_definition globals
-  | ltl_fu_external_function: external_function → ltl_function_definition globals.
-  
-record ltl_program (globals: list (ident × nat)): Type[0] ≝
-{
-  ltl_pr_funcs: list (ident × (ltl_function_definition (map ? ? \fst globals)));
-  ltl_pr_main: option ident
-}.
-*)
+definition ltl_program ≝ joint_program ltl_params.