source: src/LIN/LIN.ma @ 714

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

Work on translation from LTL to LIN.

File size: 2.0 KB
Line 
1include "arithmetics/nat.ma".
2include "ASM/String.ma".
3
4include "ASM/I8051.ma".
5include "common/AST.ma".
6
7alias id "ASMOp1" = "cic:/matita/cerco/ASM/I8051/Op1.ind(1,0,0)".
8alias id "ASMOp2" = "cic:/matita/cerco/ASM/I8051/Op2.ind(1,0,0)".
9
10inductive LINStatement (globals: list Identifier): Type[0] ≝
11  | LIN_St_Goto: Identifier → LINStatement globals
12  | LIN_St_Label: Identifier → LINStatement globals
13  | LIN_St_Comment: String → LINStatement globals
14  | LIN_St_CostLabel: Identifier → LINStatement globals
15  | LIN_St_Int: Register → Byte → LINStatement globals
16  | LIN_St_Pop: LINStatement globals
17  | LIN_St_Push: LINStatement globals
18  | LIN_St_Address: ∀i: Identifier. (member i (eq_bv ?) globals) → LINStatement globals
19  | LIN_St_FromAcc: Register → LINStatement globals
20  | LIN_St_ToAcc: Register → LINStatement globals
21  | LIN_St_OpAccs: OpAccs → LINStatement globals
22  | LIN_St_Op1: ASMOp1 → LINStatement globals
23  | LIN_St_Op2: ASMOp2 → Register → LINStatement globals
24  | LIN_St_ClearCarry: LINStatement globals
25  | LIN_St_Load: LINStatement globals
26  | LIN_St_Store: LINStatement globals
27  | LIN_St_CallId: Identifier → LINStatement globals
28  | LIN_St_CondAcc: Identifier → LINStatement globals
29  | LIN_St_Return: LINStatement globals.
30 
31definition LINInternalFunction ≝ λglobals. list (LINStatement globals).
32
33inductive LINFunctionDefinition (globals: list Identifier): Type[0] ≝
34  LIN_Fu_Internal: LINInternalFunction globals → LINFunctionDefinition globals
35| LIN_Fu_External: ExternalFunction → LINFunctionDefinition globals.
36
37record LINProgram: Type[0] ≝
38{
39  LIN_Pr_vars: list (Identifier × nat);
40  LIN_Pr_funs: list (Identifier × (LINFunctionDefinition (map ? ? (fst ? ?) LIN_Pr_vars)));
41  LIN_Pr_main: option Identifier
42}.
43
44definition LIN_Pr_vars:
45    LINProgram → list (Identifier × nat).
46  # r
47  cases r
48  # H1 # H2 #H3
49  @ H1
50qed.
51
52definition LIN_Pr_funs:
53  ∀p: LINProgram.
54    list (Identifier × (LINFunctionDefinition (map ? ? (fst ? ?) (LIN_Pr_vars p)))).
55  # r
56  cases r
57  # H1 # H2 #H3
58  @ H2
59qed.
Note: See TracBrowser for help on using the repository browser.