1 | include "arithmetics/nat.ma". |
---|
2 | |
---|
3 | include "ASM/String.ma". |
---|
4 | include "ASM/BitVector.ma". |
---|
5 | include "utilities/Compare.ma". |
---|
6 | |
---|
7 | definition Identifier ≝ Byte. |
---|
8 | definition Immediate ≝ nat. |
---|
9 | |
---|
10 | definition bool_to_Prop ≝ |
---|
11 | λb. match b with [ true ⇒ True | false ⇒ False ]. |
---|
12 | |
---|
13 | (* dpm: should go to standard library *) |
---|
14 | let rec member (i: Identifier) (eq_i: Identifier → Identifier → bool) |
---|
15 | (g: list Identifier) on g: Prop ≝ |
---|
16 | match g with |
---|
17 | [ nil ⇒ False |
---|
18 | | cons hd tl ⇒ |
---|
19 | bool_to_Prop (eq_i hd i) ∨ member i eq_i tl |
---|
20 | ]. |
---|
21 | |
---|
22 | inductive Compare: Type[0] ≝ |
---|
23 | Compare_Equal: Compare |
---|
24 | | Compare_Less: Compare |
---|
25 | | Compare_Greater: Compare |
---|
26 | | Compare_LessEqual: Compare |
---|
27 | | Compare_GreaterEqual: Compare. |
---|
28 | |
---|
29 | inductive Cast: Type[0] ≝ |
---|
30 | Cast_Int: Byte → Cast |
---|
31 | | Cast_AddrSymbol: Identifier → Cast |
---|
32 | | Cast_StackOffset: Immediate → Cast. |
---|
33 | |
---|
34 | inductive Op1: Type[0] ≝ |
---|
35 | Op1_Cast8U: Op1 |
---|
36 | | Op1_Cast8S: Op1 |
---|
37 | | Op1_Cast16U: Op1 |
---|
38 | | Op1_Cast16S: Op1 |
---|
39 | | Op1_NegInt: Op1 |
---|
40 | | Op1_NotBool: Op1 |
---|
41 | | Op1_NotInt: Op1 |
---|
42 | (* |
---|
43 | | Op1_NegFloat: Op1 |
---|
44 | | Op1_AbsFloat: Op1 |
---|
45 | | Op1_SingleOfFloat: Op1 |
---|
46 | | Op1_IntOfFloat: Op1 |
---|
47 | | Op1_IntUOfFloat: Op1 |
---|
48 | | Op1_FloatOfInt: Op1 |
---|
49 | | Op1_FloatOfIntU: Op1 |
---|
50 | *) |
---|
51 | | Op1_Id: Op1 |
---|
52 | | Op1_PtrOfInt: Op1 |
---|
53 | | Op1_IntOfPtr: Op1. |
---|
54 | |
---|
55 | inductive Op2: Type[0] ≝ |
---|
56 | Op2_Add: Op2 |
---|
57 | | Op2_Sub: Op2 |
---|
58 | | Op2_Mul: Op2 |
---|
59 | | Op2_Div: Op2 |
---|
60 | | Op2_DivU: Op2 |
---|
61 | | Op2_Mod: Op2 |
---|
62 | | Op2_ModU: Op2 |
---|
63 | | Op2_And: Op2 |
---|
64 | | Op2_Or: Op2 |
---|
65 | | Op2_XOr: Op2 |
---|
66 | | Op2_ShL: Op2 |
---|
67 | | Op2_ShR: Op2 |
---|
68 | | Op2_ShRU: Op2 |
---|
69 | (* |
---|
70 | | Op2_AddF: Op2 |
---|
71 | | Op2_SubF: Op2 |
---|
72 | | Op2_MulF: Op2 |
---|
73 | | Op2_DivF: Op2 |
---|
74 | *) |
---|
75 | | Op2_Cmp: Compare → Op2 |
---|
76 | | Op2_CmpU: Compare → Op2 |
---|
77 | (* |
---|
78 | | Op2_CmpF: Compare → Op2 |
---|
79 | *) |
---|
80 | | Op2_AddP: Op2 |
---|
81 | | Op2_SubP: Op2 |
---|
82 | | Op2_CmpP: Compare → Op2. |
---|
83 | |
---|
84 | inductive Data: Type[0] ≝ |
---|
85 | Data_Reserve: nat → Data |
---|
86 | | Data_Int8: Byte → Data |
---|
87 | | Data_Int16: Word → Data. |
---|
88 | |
---|
89 | inductive DataSize: Type[0] ≝ |
---|
90 | DataSize_Byte: DataSize |
---|
91 | | DataSize_HalfWord: DataSize |
---|
92 | | DataSize_Word: DataSize. |
---|
93 | |
---|
94 | inductive SigType: Type[0] ≝ |
---|
95 | SigType_Int: SigType |
---|
96 | (* |
---|
97 | | SigType_Float: SigType |
---|
98 | *) |
---|
99 | | SigType_Ptr: SigType. |
---|
100 | |
---|
101 | inductive TypeReturn: Type[0] ≝ |
---|
102 | TypeReturn_Ret: SigType → TypeReturn |
---|
103 | | TypeReturn_Void: TypeReturn. |
---|
104 | |
---|
105 | record Signature: Type[0] ≝ |
---|
106 | { |
---|
107 | signature_args: list SigType; |
---|
108 | signature_return: TypeReturn |
---|
109 | }. |
---|
110 | |
---|
111 | record ExternalFunction: Type[0] ≝ |
---|
112 | { |
---|
113 | external_function_tag: Identifier; |
---|
114 | external_function_sig: Signature |
---|
115 | }. |
---|
116 | |
---|
117 | definition Trace ≝ list Identifier. |
---|