source: src/LIN/LIN.ma @ 1164

Last change on this file since 1164 was 1164, checked in by mulligan, 8 years ago

ltl to lin working again, more changes to joint syntax

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