Changeset 1233 for src/LIN

Timestamp:

Sep 21, 2011, 11:57:20 AM (8 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/LIN/LIN.ma (modified) (3 diffs)

src/LIN/LIN.ma

@@ -2 +2 @@
 
 definition lin_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) unit.
 
-definition pre_lin_statement ≝
- λglobals: list ident. joint_statement lin_params globals.
-
-definition lin_statement ≝
-  λglobals.
-    option ident × (pre_lin_statement globals).
+definition lin_statement ≝ joint_statement lin_params.
 
 definition well_formed_P ≝
@@ -21 +14 @@
       match \fst hd with
       [ Some lbl ⇒ False
-      | None ⇒ True
-      ]
-    ].
+      | None ⇒ True]].
 
+(*
 definition lin_sem_params_: ∀globals. sem_params_ lin_params globals ≝
  λglobals.
@@ -31 +23 @@
 cases daemon
 qed.
+*)
 
-definition ltl_program ≝ λglobals. joint_program globals … (lin_sem_params_ globals).
-
-inductive lin_function_definition (globals: list ident): Type[0] ≝
-  lin_fu_internal: ∀code: list (lin_statement globals). well_formed_P ? ? code → lin_function_definition globals
-| lin_fu_external: external_function → lin_function_definition globals.
-
-record lin_program: Type[0] ≝
-{
-  lin_pr_vars: list (ident × nat);
-  lin_pr_funcs: list (ident × (lin_function_definition (map ? ? (fst ? ?) lin_pr_vars)));
-  lin_pr_main: option ident
-}.
+definition ltl_program ≝ joint_program lin_params.