source: src/LIN/LIN.ma @ 699

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

More or less finished formalisation of LIN.

File size: 2.3 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
10(* dpm: should go to standard library *)
11let rec member (i: Identifier) (eq_i: Identifier → Identifier → bool)
12               (g: list Identifier) on g: Prop ≝
13  match g with
14  [ nil ⇒ False
15  | cons hd tl ⇒
16      bool_to_Prop (eq_i hd i) ∨ member i eq_i tl
17  ].
18
19inductive LINStatement (globals: list Identifier): Type[0] ≝
20  | LIN_St_Goto: Identifier → LINStatement globals
21  | LIN_St_Label: Identifier → LINStatement globals
22  | LIN_St_Comment: String → LINStatement globals
23  | LIN_St_CostLabel: Identifier → LINStatement globals
24  | LIN_St_Int: Register → Byte → LINStatement globals
25  | LIN_St_Pop: LINStatement globals
26  | LIN_St_Push: LINStatement globals
27  | LIN_St_Address: ∀i: Identifier. (member i (eq_bv ?) globals) → LINStatement globals
28  | LIN_St_FromAcc: Register → LINStatement globals
29  | LIN_St_ToAcc: Register → LINStatement globals
30  | LIN_St_OpAccs: OpAccs → LINStatement globals
31  | LIN_St_Op1: ASMOp1 → LINStatement globals
32  | LIN_St_Op2: ASMOp2 → Register → LINStatement globals
33  | LIN_St_ClearCarry: LINStatement globals
34  | LIN_St_Load: LINStatement globals
35  | LIN_St_Store: LINStatement globals
36  | LIN_St_CallId: Identifier → LINStatement globals
37  | LIN_St_CondAcc: Identifier → LINStatement globals
38  | LIN_St_Return: LINStatement globals.
39 
40definition LINInternalFunction ≝ λglobals. list (LINStatement globals).
41
42inductive LINFunctionDefinition (globals: list Identifier): Type[0] ≝
43  LIN_Fu_Internal: LINInternalFunction globals → LINFunctionDefinition globals
44| LIN_Fu_External: ExternalFunction → LINFunctionDefinition globals.
45
46record LINProgram: Type[0] ≝
47{
48  LIN_Pr_vars: list (Identifier × nat);
49  LIN_Pr_funs: list (Identifier × (LINFunctionDefinition (map ? ? (fst ? ?) LIN_Pr_vars)));
50  LIN_Pr_main: option Identifier
51}.
52
53definition LIN_Pr_vars:
54    LINProgram → list (Identifier × nat).
55  # r
56  cases r
57  # H1 # H2 #H3
58  @ H1
59qed.
60
61definition LIN_Pr_funs:
62  ∀p: LINProgram.
63    list (Identifier × (LINFunctionDefinition (map ? ? (fst ? ?) (LIN_Pr_vars p)))).
64  # r
65  cases r
66  # H1 # H2 #H3
67  @ H2
68qed.
Note: See TracBrowser for help on using the repository browser.