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