Changeset 1233 for src/LTL/LTL.ma


Ignore:
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:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTL.ma

    r1222 r1233  
    33
    44definition 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.
    86
    9 definition ltl_statement ≝ λglobals: list ident. joint_statement ltl_params globals.
     7definition ltl_statement ≝ joint_statement ltl_params.
    108
    11 definition ltl_sem_params_: ∀globals. sem_params_ ltl_params globals ≝
     9(*definition ltl_sem_params_: ∀globals. sem_params_ ltl_params globals ≝
    1210 λ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 …).*)
    1412
    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 *)
     13definition ltl_program ≝ joint_program ltl_params.
Note: See TracChangeset for help on using the changeset viewer.