source: Deliverables/D4.2-4.3/LIN/LIN.ma @ 491

Last change on this file since 491 was 491, checked in by mulligan, 8 years ago

Initial commit of (part)-formalisation of LIN intermediate language.

File size: 1.6 KB
Line 
1include "arithmetics/nat.ma".
2include "cerco/String.ma".
3
4include "cerco-intermediate-languages/ASM/I8051.ma".
5include "cerco-intermediate-languages/common/AST.ma".
6include "cerco-intermediate-languages/utilities/StringTools.ma".
7
8alias id "ASMOp1" = "cic:/matita/cerco-intermediate-languages/ASM/I8051/Op1.ind(1,0,0)".
9alias id "ASMOp2" = "cic:/matita/cerco-intermediate-languages/ASM/I8051/Op2.ind(1,0,0)".
10
11inductive LINStatement: Type[0] ≝
12  | LIN_St_Goto: Label → LINStatement
13  | LIN_St_Label: Label → LINStatement
14  | LIN_St_Comment: String → LINStatement
15  | LIN_St_CostLabel: CostLabel → LINStatement
16  | LIN_St_Int: Register → Byte → LINStatement
17  | LIN_St_Pop: LINStatement
18  | LIN_St_Push: LINStatement
19  | LIN_St_Address: Identifier → LINStatement
20  | LIN_St_FromAcc: Register → LINStatement
21  | LIN_St_ToAcc: Register → LINStatement
22  | LIN_St_OpAccs: OpAccs → LINStatement
23  | LIN_St_Op1: ASMOp1 → LINStatement
24  | LIN_St_Op2: ASMOp2 → Register → LINStatement
25  | LIN_St_ClearCarry: LINStatement
26  | LIN_St_Load: LINStatement
27  | LIN_St_Store: LINStatement
28  | LIN_St_CallId: Identifier → LINStatement
29  | LIN_St_CondAcc: Label → LINStatement
30  | LIN_St_Return: LINStatement.
31 
32definition LINInternalFunction ≝ list LINStatement.
33
34inductive LINFunctionDefinition: Type[0] ≝
35  LIN_Fu_Internal: LINInternalFunction → LINFunctionDefinition
36| LIN_Fu_External: ExternalFunction → LINFunctionDefinition.
37
38record LINProgram: Type[0] ≝
39{
40  LIN_Pr_vars: list (Identifier × nat);
41  LIN_Pr_funs: list (Identifier × LINFunctionDefinition);
42  LIN_Pr_main: option Identifier
43}.
Note: See TracBrowser for help on using the repository browser.