1signature Import =
2sig
3
4   datatype monop =
5       Abs
6     | BNot
7     | Bin
8     | Cardinality
9     | Cast of ParseDatatype.pretype
10     | Dec
11     | Difference
12     | Drop
13     | Element
14     | FP32To64
15     | FP64To32
16     | FP64To32_
17     | FPAbs of int
18     | FPAdd of int
19     | FPAdd_ of int
20     | FPCmp of int
21     | FPDiv of int
22     | FPDiv_ of int
23     | FPEq of int
24     | FPFromInt of int
25     | FPGe of int
26     | FPGt of int
27     | FPIsIntegral of int
28     | FPIsFinite of int
29     | FPIsNan of int
30     | FPIsNormal of int
31     | FPIsSignallingNan of int
32     | FPIsSubnormal of int
33     | FPIsZero of int
34     | FPLe of int
35     | FPLt of int
36     | FPMul of int
37     | FPMul_ of int
38     | FPMulAdd of int
39     | FPMulAdd_ of int
40     | FPMulSub of int
41     | FPMulSub_ of int
42     | FPNeg of int
43     | FPRoundToIntegral of int
44     | FPSqrt of int
45     | FPSqrt_ of int
46     | FPSub of int
47     | FPSub_ of int
48     | FPToInt of int
49     | Flat
50     | Fst
51     | Head
52     | Hex
53     | IndexOf
54     | Intersect
55     | IsAlpha
56     | IsAlphaNum
57     | IsDigit
58     | IsHexDigit
59     | IsLower
60     | IsMember
61     | IsSome
62     | IsSpace
63     | IsSubset
64     | IsUpper
65     | K1 of ParseDatatype.pretype
66     | Length
67     | Log
68     | Max
69     | Min
70     | Msb
71     | Neg
72     | Not
73     | PadLeft
74     | PadRight
75     | QuotRem
76     | Remove
77     | RemoveExcept
78     | RemoveDuplicates
79     | Rev
80     | SE of ParseDatatype.pretype
81     | Size
82     | Smax
83     | Smin
84     | Snd
85     | SofL
86     | Some
87     | Tail
88     | Take
89     | ToLower
90     | ToUpper
91     | Union
92     | Update
93     | ValOf
94
95   datatype binop =
96       Add
97     | And
98     | Asr
99     | BAnd
100     | BOr
101     | BXor
102     | Bit
103     | Div
104     | Exp
105     | Fld
106     | Ge
107     | Gt
108     | In
109     | Insert
110     | Le
111     | Lsl
112     | Lsr
113     | Lt
114     | Mod
115     | Mul
116     | Or
117     | Quot
118     | Rem
119     | Rep
120     | Rol
121     | Ror
122     | SDiv
123     | SMod
124     | Splitl
125     | Splitr
126     | Sub
127     | Tok
128     | Uge
129     | Ugt
130     | Ule
131     | Ult
132
133   val start : string -> unit
134   val finish : int -> unit
135   val ieee_underflow_before : bool ref
136
137   val Construct : (string * ParseDatatype.constructor list) list -> unit
138   val NoBigRecord : string * ParseDatatype.field list -> unit
139   val Record : string * ParseDatatype.field list -> unit
140
141   val Def : string * Term.term * Term.term -> Theory.thm
142   val Def0 : string * Term.term -> Theory.thm
143   val tDef :
144      string * Term.term * Term.term * Term.term * Tactic.tactic -> Theory.thm
145
146   val bTy : ParseDatatype.pretype (* bool *)
147   val cTy : ParseDatatype.pretype (* char *)
148   val fTy : ParseDatatype.pretype (* IEEE flags *)
149   val iTy : ParseDatatype.pretype (* int *)
150   val nTy : ParseDatatype.pretype (* num *)
151   val oTy : ParseDatatype.pretype (* IEEE ordering *)
152   val rTy : ParseDatatype.pretype (* IEEE rounding *)
153   val sTy : ParseDatatype.pretype (* string *)
154   val uTy : ParseDatatype.pretype (* unit/one *)
155   val vTy : ParseDatatype.pretype (* bit-string *)
156
157   val CTy : string -> ParseDatatype.pretype
158   val VTy : string -> ParseDatatype.pretype
159   val FTy : int -> ParseDatatype.pretype
160   val F1 : ParseDatatype.pretype
161   val F4 : ParseDatatype.pretype
162   val F8 : ParseDatatype.pretype
163   val F16 : ParseDatatype.pretype
164   val F32 : ParseDatatype.pretype
165   val F64 : ParseDatatype.pretype
166   val BTy : string -> ParseDatatype.pretype
167   val ATy : ParseDatatype.pretype * ParseDatatype.pretype ->
168             ParseDatatype.pretype
169   val PTy : ParseDatatype.pretype * ParseDatatype.pretype ->
170             ParseDatatype.pretype
171   val LTy : ParseDatatype.pretype -> ParseDatatype.pretype
172   val OTy : ParseDatatype.pretype -> ParseDatatype.pretype
173   val STy : ParseDatatype.pretype -> ParseDatatype.pretype
174
175   val LU : Term.term
176   val LT : Term.term
177   val LF : Term.term
178   val LI : IntInf.int -> Term.term
179   val LN : IntInf.int -> Term.term
180   val LSC : char -> Term.term
181   val LS : string -> Term.term
182   val LV : string -> Term.term
183   val LW : IntInf.int * int -> Term.term
184   val LY : IntInf.int * string -> Term.term
185   val LC : string * ParseDatatype.pretype -> Term.term
186   val LE : ParseDatatype.pretype -> Term.term
187   val LNL: ParseDatatype.pretype -> Term.term
188   val LO : ParseDatatype.pretype -> Term.term
189   val LX : ParseDatatype.pretype -> Term.term
190
191   val NEGINF32 : Term.term
192   val NEGINF64 : Term.term
193   val POSINF32 : Term.term
194   val POSINF64 : Term.term
195   val NEGZERO32 : Term.term
196   val NEGZERO64 : Term.term
197   val POSZERO32 : Term.term
198   val POSZERO64 : Term.term
199   val NEGMIN32 : Term.term
200   val NEGMIN64 : Term.term
201   val POSMIN32 : Term.term
202   val POSMIN64 : Term.term
203   val NEGMAX32 : Term.term
204   val NEGMAX64 : Term.term
205   val POSMAX32 : Term.term
206   val POSMAX64 : Term.term
207   val QUIETNAN32 : Term.term
208   val QUIETNAN64 : Term.term
209   val SIGNALNAN32 : Term.term
210   val SIGNALNAN64 : Term.term
211
212   val Call : string * ParseDatatype.pretype * Term.term -> Term.term
213   val Const : string * ParseDatatype.pretype -> Term.term
214   val AVar : ParseDatatype.pretype -> Term.term
215   val Var : string * ParseDatatype.pretype -> Term.term
216   val bVar : string -> Term.term
217   val iVar : string -> Term.term
218   val nVar : string -> Term.term
219   val sVar : string -> Term.term
220   val uVar : string -> Term.term
221   val vVar : string -> Term.term
222   val Close : Term.term * Term.term -> Term.term
223   val Apply : Term.term * Term.term -> Term.term
224   val TP : Term.term list -> Term.term
225   val Fupd : Term.term * Term.term * Term.term -> Term.term
226   val CS : Term.term * (Term.term * Term.term) list -> Term.term
227   val Let : Term.term * Term.term * Term.term -> Term.term
228   val LL : Term.term list -> Term.term
229   val LLC : Term.term list * Term.term -> Term.term
230   val SL : Term.term list -> Term.term
231   val Rec : ParseDatatype.pretype * Term.term list -> Term.term
232   val Dest : string * ParseDatatype.pretype * Term.term -> Term.term
233   val Rupd : string * Term.term -> Term.term
234   val BL : int * Term.term -> Term.term
235   val ITE : Term.term * Term.term * Term.term -> Term.term
236   val ITB : (Term.term * Term.term) list * Term.term -> Term.term
237   val EX : Term.term * Term.term * Term.term * ParseDatatype.pretype ->
238            Term.term
239   val BFI : Term.term * Term.term * Term.term * Term.term -> Term.term
240   val REP : Term.term * Term.term * ParseDatatype.pretype -> Term.term
241   val CC : Term.term list -> Term.term
242   val EQ : Term.term * Term.term -> Term.term
243   val MU : Term.term * ParseDatatype.pretype -> Term.term
244   val MB : Term.term * Term.term -> Term.term
245   val MR : Term.term -> Term.term
246   val MW : Term.term -> Term.term
247   val MN : Term.term * Term.term -> Term.term
248   val MD : Term.term * ParseDatatype.pretype -> Term.term
249   val For : Term.term -> Term.term
250   val Foreach : Term.term -> Term.term
251   val Mop : monop * Term.term -> Term.term
252   val Bop : binop * Term.term * Term.term -> Term.term
253
254end
255