source: src/LIN/LIN.ma @ 722

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

Committing changes from today. Several files do not typecheck.

File size: 2.4 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 JointInstruction (globals: list Identifier): Type[0] ≝
11  | Joint_Instr_Goto: Identifier → JointInstruction globals
12  | Joint_Instr_Comment: String → JointInstruction globals
13  | Joint_Instr_CostLabel: Identifier → JointInstruction globals
14  | Joint_Instr_Int: Register → Byte → JointInstruction globals
15  | Joint_Instr_Pop: JointInstruction globals
16  | Joint_Instr_Push: JointInstruction globals
17  | Joint_Instr_Address: ∀i: Identifier. (member i (eq_bv ?) globals) → JointInstruction globals
18  | Joint_Instr_FromAcc: Register → JointInstruction globals
19  | Joint_Instr_ToAcc: Register → JointInstruction globals
20  | Joint_Instr_OpAccs: OpAccs → JointInstruction globals
21  | Joint_Instr_Op1: Op1 → JointInstruction globals
22  | Joint_Instr_Op2: Op2 → Register → JointInstruction globals
23  | Joint_Instr_ClearCarry: JointInstruction globals
24  | Joint_Instr_Load: JointInstruction globals
25  | Joint_Instr_Store: JointInstruction globals
26  | Joint_Instr_CallId: Identifier → JointInstruction globals
27  | Joint_Instr_CondAcc: Identifier → JointInstruction globals.
28
29inductive JointStatement (A: Type[0]) (globals: list Identifier): Type[0] ≝
30  | LIN_St_Sequential: JointInstruction globals → A → JointStatement A globals
31  | LIN_St_Return: JointStatement A globals.
32 
33definition LINStatement ≝
34  λglobals.
35    option Identifier × (JointStatement unit globals).
36 
37definition LINInternalFunction ≝ λglobals. list (LINStatement globals).
38
39inductive LINFunctionDefinition (globals: list Identifier): Type[0] ≝
40  LIN_Fu_Internal: LINInternalFunction globals → LINFunctionDefinition globals
41| LIN_Fu_External: ExternalFunction → LINFunctionDefinition globals.
42
43record LINProgram: Type[0] ≝
44{
45  LIN_Pr_vars: list (Identifier × nat);
46  LIN_Pr_funs: list (Identifier × (LINFunctionDefinition (map ? ? (fst ? ?) LIN_Pr_vars)));
47  LIN_Pr_main: option Identifier
48}.
49
50definition LIN_Pr_vars:
51    LINProgram → list (Identifier × nat).
52  # r
53  cases r
54  # H1 # H2 #H3
55  @ H1
56qed.
57
58definition LIN_Pr_funs:
59  ∀p: LINProgram.
60    list (Identifier × (LINFunctionDefinition (map ? ? (fst ? ?) (LIN_Pr_vars p)))).
61  # r
62  cases r
63  # H1 # H2 #H3
64  @ H2
65qed.
Note: See TracBrowser for help on using the repository browser.