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

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

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

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