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

Lots more fixing to get both front and backends using same conventions and types.

File size:
1.1 KB

Line  

1  include "LIN/JointLTLLIN.ma". 

2  

3  definition pre_lin_statement ≝ joint_statement unit. 

4  

5  definition lin_statement ≝ 

6  λglobals. 

7  option ident × (pre_lin_statement globals). 

8  

9  definition well_formed_P ≝ 

10  λA, B: Type[0]. 

11  λcode: list (option A × B). 

12  match code with 

13  [ nil ⇒ False 

14   cons hd tl ⇒ 

15  match \fst hd with 

16  [ Some lbl ⇒ False 

17   None ⇒ True 

18  ] 

19  ]. 

20  

21  inductive lin_function_definition (globals: list ident): Type[0] ≝ 

22  lin_fu_internal: ∀code: list (lin_statement globals). well_formed_P ? ? code → lin_function_definition globals 

23   lin_fu_external: external_function → lin_function_definition globals. 

24  

25  record lin_program: Type[0] ≝ 

26  { 

27  lin_pr_vars: list (ident × nat); 

28  lin_pr_funcs: list (ident × (lin_function_definition (map ? ? (fst ? ?) lin_pr_vars))); 

29  lin_pr_main: option ident 

30  }. 

31  

32  definition lin_pr_vars: 

33  lin_program → list (ident × nat). 

34  # r 

35  cases r 

36  # H1 # H2 #H3 

37  @ H1 

38  qed. 

39  

40  definition lin_pr_funcs: 

41  ∀p: lin_program. 

42  list (ident × (lin_function_definition (map ? ? (fst ? ?) (lin_pr_vars p)))). 

43  # r 

44  cases r 

45  # H1 # H2 #H3 

46  @ H2 

47  qed. 

Note: See
TracBrowser
for help on using the repository browser.