source: src/LIN/LIN.ma @ 698

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

Commit with changes to files to get our files to typecheck.

File size: 2.1 KB
Line 
1include "arithmetics/nat.ma".
2include "ASM/String.ma".
3
4include "ASM/I8051.ma".
5include "common/AST.ma".
6include "utilities/StringTools.ma".
7
8alias id "ASMOp1" = "cic:/matita/cerco/ASM/I8051/Op1.ind(1,0,0)".
9alias id "ASMOp2" = "cic:/matita/cerco/ASM/I8051/Op2.ind(1,0,0)".
10
11let rec member (i: Identifier) (eq_i: Identifier → Identifier → bool)
12               (g: list (Identifier × nat)) on g: Prop ≝
13  match g with
14  [ nil ⇒ False
15  | cons hd tl ⇒
16      bool_to_Prop (eq_i (fst ? ? hd) i) ∨ member i eq_i tl
17  ].
18
19inductive LINStatement (globals: list (Identifier × nat)): 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: CostLabel → 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 × nat)): Type[0] ≝
43  LIN_Fu_Internal: LINInternalFunction globals → LINFunctionDefinition globals
44| LIN_Fu_External: ExternalFunction → LINFunctionDefinition globals.
45
46record LINProgram (globals: list (Identifier × nat)): Type[0] ≝
47{
48  LIN_Pr_vars: list (Identifier × nat);
49  LIN_Pr_funs: list (Identifier × (LINFunctionDefinition globals));
50  LIN_Pr_main: option Identifier
51}.
Note: See TracBrowser for help on using the repository browser.