source: src/LIN/LIN.ma @ 1166

Last change on this file since 1166 was 1166, checked in by mulligan, 9 years ago

moved joint ltl lin files into their own directory. more changes to ltl and lin passes to help type checker in ertl pass

File size: 1020 bytes
RevLine 
[723]1include "LIN/JointLTLLIN.ma".
2 
[1166]3inductive pre_lin_statement (globals: list ident): Type[0] ≝
4  | lin_st_lift_joint: joint_statement unit Register Register Register Register Register registers_move globals → pre_lin_statement globals.
[491]5
[757]6definition lin_statement ≝
[722]7  λglobals.
[757]8    option ident × (pre_lin_statement globals).
[491]9
[757]10definition well_formed_P ≝
[723]11  λA, B: Type[0].
12  λcode: list (option A × B).
13    match code with
14    [ nil ⇒ False
15    | cons hd tl ⇒
16      match \fst hd with
17      [ Some lbl ⇒ False
18      | None ⇒ True
19      ]
20    ].
21   
[757]22inductive lin_function_definition (globals: list ident): Type[0] ≝
23  lin_fu_internal: ∀code: list (lin_statement globals). well_formed_P ? ? code → lin_function_definition globals
24| lin_fu_external: external_function → lin_function_definition globals.
[491]25
[757]26record lin_program: Type[0] ≝
[491]27{
[757]28  lin_pr_vars: list (ident × nat);
29  lin_pr_funcs: list (ident × (lin_function_definition (map ? ? (fst ? ?) lin_pr_vars)));
30  lin_pr_main: option ident
[699]31}.
Note: See TracBrowser for help on using the repository browser.