source: src/common/AST.ma @ 714

Last change on this file since 714 was 714, checked in by mulligan, 10 years ago

Work on translation from LTL to LIN.

File size: 2.3 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
10definition bool_to_Prop ≝
11 λb. match b with [ true ⇒ True | false ⇒ False ].
12
13(* dpm: should go to standard library *)
14let 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
22inductive Compare: Type[0] ≝
23  Compare_Equal: Compare
24| Compare_Less: Compare
25| Compare_Greater: Compare
26| Compare_LessEqual: Compare
27| Compare_GreaterEqual: Compare.
28
29inductive Cast: Type[0] ≝
30  Cast_Int: Byte → Cast
31| Cast_AddrSymbol: Identifier → Cast
32| Cast_StackOffset: Immediate → Cast.
33
34inductive 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
55inductive 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
84inductive Data: Type[0] ≝
85  Data_Reserve: nat → Data
86| Data_Int8: Byte → Data
87| Data_Int16: Word → Data.
88
89inductive DataSize: Type[0] ≝
90  DataSize_Byte: DataSize
91| DataSize_HalfWord: DataSize
92| DataSize_Word: DataSize.
93
94inductive SigType: Type[0] ≝
95  SigType_Int: SigType
96(*
97| SigType_Float: SigType
98*)
99| SigType_Ptr: SigType.
100
101inductive TypeReturn: Type[0] ≝
102  TypeReturn_Ret: SigType → TypeReturn
103| TypeReturn_Void: TypeReturn.
104
105record Signature: Type[0] ≝
106{
107  signature_args: list SigType;
108  signature_return: TypeReturn
109}.
110
111record ExternalFunction: Type[0] ≝
112{
113  external_function_tag: Identifier;
114  external_function_sig: Signature
115}.
116
117definition Trace ≝ list Identifier.
Note: See TracBrowser for help on using the repository browser.