source: src/common/AST.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.0 KB
Line 
1include "arithmetics/nat.ma".
2
3include "ASM/String.ma".
4include "ASM/BitVector.ma".
5include "utilities/Compare.ma".
6
7definition Identifier ≝ Byte.
8definition Immediate ≝ nat.
9
10inductive Compare: Type[0] ≝
11  Compare_Equal: Compare
12| Compare_Less: Compare
13| Compare_Greater: Compare
14| Compare_LessEqual: Compare
15| Compare_GreaterEqual: Compare.
16
17inductive Cast: Type[0] ≝
18  Cast_Int: Byte → Cast
19| Cast_AddrSymbol: Identifier → Cast
20| Cast_StackOffset: Immediate → Cast.
21
22inductive Op1: Type[0] ≝
23  Op1_Cast8U: Op1
24| Op1_Cast8S: Op1
25| Op1_Cast16U: Op1
26| Op1_Cast16S: Op1
27| Op1_NegInt: Op1
28| Op1_NotBool: Op1
29| Op1_NotInt: Op1
30(*
31| Op1_NegFloat: Op1
32| Op1_AbsFloat: Op1
33| Op1_SingleOfFloat: Op1
34| Op1_IntOfFloat: Op1
35| Op1_IntUOfFloat: Op1
36| Op1_FloatOfInt: Op1
37| Op1_FloatOfIntU: Op1
38*)
39| Op1_Id: Op1
40| Op1_PtrOfInt: Op1
41| Op1_IntOfPtr: Op1.
42
43inductive Op2: Type[0] ≝
44  Op2_Add: Op2
45| Op2_Sub: Op2
46| Op2_Mul: Op2
47| Op2_Div: Op2
48| Op2_DivU: Op2
49| Op2_Mod: Op2
50| Op2_ModU: Op2
51| Op2_And: Op2
52| Op2_Or: Op2
53| Op2_XOr: Op2
54| Op2_ShL: Op2
55| Op2_ShR: Op2
56| Op2_ShRU: Op2
57(*
58| Op2_AddF: Op2
59| Op2_SubF: Op2
60| Op2_MulF: Op2
61| Op2_DivF: Op2
62*)
63| Op2_Cmp: Compare → Op2
64| Op2_CmpU: Compare → Op2
65(*
66| Op2_CmpF: Compare → Op2
67*)
68| Op2_AddP: Op2
69| Op2_SubP: Op2
70| Op2_CmpP: Compare → Op2.
71
72inductive Data: Type[0] ≝
73  Data_Reserve: nat → Data
74| Data_Int8: Byte → Data
75| Data_Int16: Word → Data.
76
77inductive DataSize: Type[0] ≝
78  DataSize_Byte: DataSize
79| DataSize_HalfWord: DataSize
80| DataSize_Word: DataSize.
81
82inductive SigType: Type[0] ≝
83  SigType_Int: SigType
84(*
85| SigType_Float: SigType
86*)
87| SigType_Ptr: SigType.
88
89inductive TypeReturn: Type[0] ≝
90  TypeReturn_Ret: SigType → TypeReturn
91| TypeReturn_Void: TypeReturn.
92
93record Signature: Type[0] ≝
94{
95  signature_args: list SigType;
96  signature_return: TypeReturn
97}.
98
99record ExternalFunction: Type[0] ≝
100{
101  external_function_tag: Identifier;
102  external_function_sig: Signature
103}.
104
105definition Trace ≝ list Identifier.
Note: See TracBrowser for help on using the repository browser.