Changeset 1233 for src/LIN


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/LIN/LIN.ma

    r1224 r1233  
    22
    33definition 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.
    75
    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).
     6definition lin_statement ≝ joint_statement lin_params.
    147
    158definition well_formed_P ≝
     
    2114      match \fst hd with
    2215      [ Some lbl ⇒ False
    23       | None ⇒ True
    24       ]
    25     ].
     16      | None ⇒ True]].
    2617
     18(*
    2719definition lin_sem_params_: ∀globals. sem_params_ lin_params globals ≝
    2820 λglobals.
     
    3123cases daemon
    3224qed.
     25*)
    3326
    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 }.
     27definition ltl_program ≝ joint_program lin_params.
Note: See TracChangeset for help on using the changeset viewer.