0 | module Core.TT.Primitive

  2 | import Core.Name

  4 | import Data.String

  5 | import Data.Vect

  7 | import Idris.Pretty.Annotations

  9 | import Libraries.Data.Ordering.Extra

 10 | import Libraries.Decidable.Equality as L

 11 | import Libraries.Text.PrettyPrint.Prettyprinter

 13 | %default total

 15 | public export

 16 | data PrimType

 17 |     = IntType

 18 |     | Int8Type

 19 |     | Int16Type

 20 |     | Int32Type

 21 |     | Int64Type

 22 |     | IntegerType

 23 |     | Bits8Type

 24 |     | Bits16Type

 25 |     | Bits32Type

 26 |     | Bits64Type

 27 |     | StringType

 28 |     | CharType

 29 |     | DoubleType

 30 |     | WorldType

 32 | %name PrimType pty

 34 | public export

 35 | data Constant

 36 |     = I   Int

 37 |     | I8  Int8

 38 |     | I16 Int16

 39 |     | I32 Int32

 40 |     | I64 Int64

 41 |     | BI  Integer

 42 |     | B8  Bits8

 43 |     | B16 Bits16

 44 |     | B32 Bits32

 45 |     | B64 Bits64

 46 |     | Str String

 47 |     | Ch  Char

 48 |     | Db  Double

 49 |     | PrT PrimType

 50 |     | WorldVal

 52 | %name Constant cst

 57 | primType : Constant -> Maybe PrimType

 58 | primType (I {})   = Just IntType

 59 | primType (I8 {})  = Just Int8Type

 60 | primType (I16 {}) = Just Int16Type

 61 | primType (I32 {}) = Just Int32Type

 62 | primType (I64 {}) = Just Int64Type

 63 | primType (BI {})  = Just IntegerType

 64 | primType (B8 {})  = Just Bits8Type

 65 | primType (B16 {}) = Just Bits16Type

 66 | primType (B32 {}) = Just Bits32Type

 67 | primType (B64 {}) = Just Bits64Type

 68 | primType (Str {}) = Just StringType

 69 | primType (Ch {})  = Just CharType

 70 | primType (Db {})  = Just DoubleType

 71 | primType (PrT {}) = Nothing

 72 | primType WorldVal = Just WorldType

 75 | isConstantType : Name -> Maybe PrimType

 76 | isConstantType (UN (Basic n)) = case n of

 77 |   "Int"     => Just IntType

 78 |   "Int8"    => Just Int8Type

 79 |   "Int16"   => Just Int16Type

 80 |   "Int32"   => Just Int32Type

 81 |   "Int64"   => Just Int64Type

 82 |   "Integer" => Just IntegerType

 83 |   "Bits8"   => Just Bits8Type

 84 |   "Bits16"  => Just Bits16Type

 85 |   "Bits32"  => Just Bits32Type

 86 |   "Bits64"  => Just Bits64Type

 87 |   "String"  => Just StringType

 88 |   "Char"    => Just CharType

 89 |   "Double"  => Just DoubleType

 90 |   "%World"  => Just WorldType

 91 |   _ => Nothing

 92 | isConstantType _ = Nothing

 95 | isPrimType : Constant -> Bool

 96 | isPrimType (PrT _) = True

 97 | isPrimType _       = False

100 | primTypeEq : (x, y : PrimType) -> Maybe (x = y)

101 | primTypeEq IntType IntType = Just Refl

102 | primTypeEq Int8Type Int8Type = Just Refl

103 | primTypeEq Int16Type Int16Type = Just Refl

104 | primTypeEq Int32Type Int32Type = Just Refl

105 | primTypeEq Int64Type Int64Type = Just Refl

106 | primTypeEq IntegerType IntegerType = Just Refl

107 | primTypeEq StringType StringType = Just Refl

108 | primTypeEq CharType CharType = Just Refl

109 | primTypeEq DoubleType DoubleType = Just Refl

110 | primTypeEq WorldType WorldType = Just Refl

111 | primTypeEq _ _ = Nothing

114 | constantEq : (x, y : Constant) -> Maybe (x = y)

115 | constantEq (I x) (I y) = L.maybeCong I (L.maybeEq x y)

116 | constantEq (I8 x) (I8 y) = L.maybeCong I8 (L.maybeEq x y)

117 | constantEq (I16 x) (I16 y) = L.maybeCong I16 (L.maybeEq x y)

118 | constantEq (I32 x) (I32 y) = L.maybeCong I32 (L.maybeEq x y)

119 | constantEq (I64 x) (I64 y) = L.maybeCong I64 (L.maybeEq x y)

120 | constantEq (B8 x) (B8 y) = L.maybeCong B8 (L.maybeEq x y)

121 | constantEq (B16 x) (B16 y) = L.maybeCong B16 (L.maybeEq x y)

122 | constantEq (B32 x) (B32 y) = L.maybeCong B32 (L.maybeEq x y)

123 | constantEq (B64 x) (B64 y) = L.maybeCong B64 (L.maybeEq x y)

124 | constantEq (BI x) (BI y) = L.maybeCong BI (L.maybeEq x y)

125 | constantEq (Str x) (Str y) = L.maybeCong Str (L.maybeEq x y)

126 | constantEq (Ch x) (Ch y) = L.maybeCong Ch (L.maybeEq x y)

127 | constantEq (Db x) (Db y) = Nothing -- no DecEq for Doubles!

128 | constantEq (PrT x) (PrT y) = L.maybeCong PrT (primTypeEq x y)

129 | constantEq WorldVal WorldVal = Just Refl

131 | constantEq _ _ = Nothing

134 | Show PrimType where

135 |   show IntType = "Int"

136 |   show Int8Type = "Int8"

137 |   show Int16Type = "Int16"

138 |   show Int32Type = "Int32"

139 |   show Int64Type = "Int64"

140 |   show IntegerType = "Integer"

141 |   show Bits8Type = "Bits8"

142 |   show Bits16Type = "Bits16"

143 |   show Bits32Type = "Bits32"

144 |   show Bits64Type = "Bits64"

145 |   show StringType = "String"

146 |   show CharType = "Char"

147 |   show DoubleType = "Double"

148 |   show WorldType = "%World"

151 | Show Constant where

152 |   show (I x) = show x

153 |   show (I8 x) = show x

154 |   show (I16 x) = show x

155 |   show (I32 x) = show x

156 |   show (I64 x) = show x

157 |   show (BI x) = show x

158 |   show (B8 x) = show x

159 |   show (B16 x) = show x

160 |   show (B32 x) = show x

161 |   show (B64 x) = show x

162 |   show (Str x) = show x

163 |   show (Ch x) = show x

164 |   show (Db x) = show x

165 |   show (PrT x) = show x

166 |   show WorldVal = "%MkWorld"

168 | Pretty IdrisSyntax PrimType where

169 |   pretty c = annotate (TCon Nothing) $ case c of

170 |     IntType => "Int"

171 |     Int8Type => "Int8"

172 |     Int16Type => "Int16"

173 |     Int32Type => "Int32"

174 |     Int64Type => "Int64"

175 |     IntegerType => "Integer"

176 |     Bits8Type => "Bits8"

177 |     Bits16Type => "Bits16"

178 |     Bits32Type => "Bits32"

179 |     Bits64Type => "Bits64"

180 |     StringType => "String"

181 |     CharType => "Char"

182 |     DoubleType => "Double"

183 |     WorldType => "%World"

186 | Pretty IdrisSyntax Constant where

187 |   pretty (PrT x) = pretty x

188 |   pretty v = annotate (DCon Nothing) $ pretty0 $ show v

192 | Eq PrimType where

193 |   IntType == IntType = True

194 |   Int8Type == Int8Type = True

195 |   Int16Type == Int16Type = True

196 |   Int32Type == Int32Type = True

197 |   Int64Type == Int64Type = True

198 |   IntegerType == IntegerType = True

199 |   Bits8Type == Bits8Type = True

200 |   Bits16Type == Bits16Type = True

201 |   Bits32Type == Bits32Type = True

202 |   Bits64Type == Bits64Type = True

203 |   StringType == StringType = True

204 |   CharType == CharType = True

205 |   DoubleType == DoubleType = True

206 |   WorldType == WorldType = True

207 |   _ == _ = False

210 | Eq Constant where

211 |   (I x) == (I y) = x == y

212 |   (I8 x) == (I8 y) = x == y

213 |   (I16 x) == (I16 y) = x == y

214 |   (I32 x) == (I32 y) = x == y

215 |   (I64 x) == (I64 y) = x == y

216 |   (BI x) == (BI y) = x == y

217 |   (B8 x) == (B8 y) = x == y

218 |   (B16 x) == (B16 y) = x == y

219 |   (B32 x) == (B32 y) = x == y

220 |   (B64 x) == (B64 y) = x == y

221 |   (Str x) == (Str y) = x == y

222 |   (Ch x) == (Ch y) = x == y

223 |   (Db x) == (Db y) = x == y

224 |   (PrT x) == (PrT y) = x == y

225 |   WorldVal == WorldVal = True

226 |   _ == _ = False

229 | Ord PrimType where

230 |   compare = compare `on` tag

231 |     where

232 |       tag : PrimType -> Int

233 |       tag IntType     = 1

234 |       tag Int8Type    = 2

235 |       tag Int16Type   = 3

236 |       tag Int32Type   = 4

237 |       tag Int64Type   = 5

238 |       tag IntegerType = 6

239 |       tag Bits8Type   = 7

240 |       tag Bits16Type  = 8

241 |       tag Bits32Type  = 9

242 |       tag Bits64Type  = 10

243 |       tag StringType  = 11

244 |       tag CharType    = 12

245 |       tag DoubleType  = 13

246 |       tag WorldType   = 14

249 | Ord Constant where

250 |     I x `compare` I y = compare x y

251 |     I8 x `compare` I8 y = compare x y

252 |     I16 x `compare` I16 y = compare x y

253 |     I32 x `compare` I32 y = compare x y

254 |     I64 x `compare` I64 y = compare x y

255 |     BI x `compare` BI y = compare x y

256 |     B8 x `compare` B8 y = compare x y

257 |     B16 x `compare` B16 y = compare x y

258 |     B32 x `compare` B32 y = compare x y

259 |     B64 x `compare` B64 y = compare x y

260 |     Str x `compare` Str y = compare x y

261 |     Ch x `compare` Ch y = compare x y

262 |     Db x `compare` Db y = compare x y

263 |     PrT x `compare` PrT y = compare x y

264 |     compare x y = compare (tag x) (tag y)

265 |       where

266 |         tag : Constant -> Int

267 |         tag (I _) = 0

268 |         tag (I8 _) = 1

269 |         tag (I16 _) = 2

270 |         tag (I32 _) = 3

271 |         tag (I64 _) = 4

272 |         tag (BI _) = 5

273 |         tag (B8 _) = 6

274 |         tag (B16 _) = 7

275 |         tag (B32 _) = 8

276 |         tag (B64 _) = 9

277 |         tag (Str _) = 10

278 |         tag (Ch _) = 11

279 |         tag (Db _) = 12

280 |         tag (PrT _) = 13

281 |         tag WorldVal = 14

285 | primTypeTag : PrimType -> Int

287 | primTypeTag IntType = 3

288 | primTypeTag IntegerType = 4

289 | primTypeTag Bits8Type = 5

290 | primTypeTag Bits16Type = 6

291 | primTypeTag Bits32Type = 7

292 | primTypeTag Bits64Type = 8

293 | primTypeTag StringType = 9

294 | primTypeTag CharType = 10

295 | primTypeTag DoubleType = 11

296 | primTypeTag WorldType = 12

297 | primTypeTag Int8Type = 13

298 | primTypeTag Int16Type = 14

299 | primTypeTag Int32Type = 15

300 | primTypeTag Int64Type = 16

303 | public export

304 | data Precision = P Int | Unlimited

306 | %name Precision prec

309 | Eq Precision where

310 |   (P m) == (P n)         = m == n

311 |   Unlimited == Unlimited = True

312 |   _         == _         = False

315 | Ord Precision where

316 |   compare (P m) (P n)         = compare m n

317 |   compare Unlimited Unlimited = EQ

318 |   compare Unlimited _         = GT

319 |   compare _         Unlimited = LT

323 | public export

324 | data IntKind = Signed Precision | Unsigned Int

326 | public export

327 | intKind : PrimType -> Maybe IntKind

328 | intKind IntegerType = Just $ Signed Unlimited

329 | intKind Int8Type    = Just . Signed   $ P 8

330 | intKind Int16Type   = Just . Signed   $ P 16

331 | intKind Int32Type   = Just . Signed   $ P 32

332 | intKind Int64Type   = Just . Signed   $ P 64

333 | intKind IntType     = Just . Signed   $ P 64

334 | intKind Bits8Type   = Just $ Unsigned 8

335 | intKind Bits16Type  = Just $ Unsigned 16

336 | intKind Bits32Type  = Just $ Unsigned 32

337 | intKind Bits64Type  = Just $ Unsigned 64

338 | intKind _           = Nothing

340 | public export

341 | precision : IntKind -> Precision

342 | precision (Signed p)   = p

343 | precision (Unsigned p) = P p

346 | public export

347 | data PrimFn : Nat -> Type where

348 |      Add : (ty : PrimType) -> PrimFn 2

349 |      Sub : (ty : PrimType) -> PrimFn 2

350 |      Mul : (ty : PrimType) -> PrimFn 2

351 |      Div : (ty : PrimType) -> PrimFn 2

352 |      Mod : (ty : PrimType) -> PrimFn 2

353 |      Neg : (ty : PrimType) -> PrimFn 1

354 |      ShiftL : (ty : PrimType) -> PrimFn 2

355 |      ShiftR : (ty : PrimType) -> PrimFn 2

357 |      BAnd : (ty : PrimType) -> PrimFn 2

358 |      BOr : (ty : PrimType) -> PrimFn 2

359 |      BXOr : (ty : PrimType) -> PrimFn 2

361 |      LT  : (ty : PrimType) -> PrimFn 2

362 |      LTE : (ty : PrimType) -> PrimFn 2

363 |      EQ  : (ty : PrimType) -> PrimFn 2

364 |      GTE : (ty : PrimType) -> PrimFn 2

365 |      GT  : (ty : PrimType) -> PrimFn 2

367 |      StrLength : PrimFn 1

368 |      StrHead : PrimFn 1

369 |      StrTail : PrimFn 1

370 |      StrIndex : PrimFn 2

371 |      StrCons : PrimFn 2

372 |      StrAppend : PrimFn 2

373 |      StrReverse : PrimFn 1

374 |      StrSubstr : PrimFn 3

376 |      DoubleExp : PrimFn 1

377 |      DoubleLog : PrimFn 1

378 |      DoublePow : PrimFn 2

379 |      DoubleSin : PrimFn 1

380 |      DoubleCos : PrimFn 1

381 |      DoubleTan : PrimFn 1

382 |      DoubleASin : PrimFn 1

383 |      DoubleACos : PrimFn 1

384 |      DoubleATan : PrimFn 1

385 |      DoubleSqrt : PrimFn 1

386 |      DoubleFloor : PrimFn 1

387 |      DoubleCeiling : PrimFn 1

389 |      Cast : PrimType -> PrimType -> PrimFn 1

390 |      BelieveMe : PrimFn 3

391 |      Crash : PrimFn 2

393 | %name PrimFn f

396 | Show (PrimFn arity) where

397 |   show (Add ty) = "+" ++ show ty

398 |   show (Sub ty) = "-" ++ show ty

399 |   show (Mul ty) = "*" ++ show ty

400 |   show (Div ty) = "/" ++ show ty

401 |   show (Mod ty) = "%" ++ show ty

402 |   show (Neg ty) = "neg " ++ show ty

403 |   show (ShiftL ty) = "shl " ++ show ty

404 |   show (ShiftR ty) = "shr " ++ show ty

405 |   show (BAnd ty) = "and " ++ show ty

406 |   show (BOr ty) = "or " ++ show ty

407 |   show (BXOr ty) = "xor " ++ show ty

408 |   show (LT ty) = "<" ++ show ty

409 |   show (LTE ty) = "<=" ++ show ty

410 |   show (EQ ty) = "==" ++ show ty

411 |   show (GTE ty) = ">=" ++ show ty

412 |   show (GT ty) = ">" ++ show ty

413 |   show StrLength = "op_strlen"

414 |   show StrHead = "op_strhead"

415 |   show StrTail = "op_strtail"

416 |   show StrIndex = "op_strindex"

417 |   show StrCons = "op_strcons"

418 |   show StrAppend = "++"

419 |   show StrReverse = "op_strrev"

420 |   show StrSubstr = "op_strsubstr"

421 |   show DoubleExp = "op_doubleExp"

422 |   show DoubleLog = "op_doubleLog"

423 |   show DoublePow = "op_doublePow"

424 |   show DoubleSin = "op_doubleSin"

425 |   show DoubleCos = "op_doubleCos"

426 |   show DoubleTan = "op_doubleTan"

427 |   show DoubleASin = "op_doubleASin"

428 |   show DoubleACos = "op_doubleACos"

429 |   show DoubleATan = "op_doubleATan"

430 |   show DoubleSqrt = "op_doubleSqrt"

431 |   show DoubleFloor = "op_doubleFloor"

432 |   show DoubleCeiling = "op_doubleCeiling"

433 |   show (Cast x y) = "cast-" ++ show x ++ "-" ++ show y

434 |   show BelieveMe = "believe_me"

435 |   show Crash = "crash"

438 | [Sugared] Show (PrimFn arity) where

439 |   show (Add ty) = "+"

440 |   show (Sub ty) = "-"

441 |   show (Mul ty) = "*"

442 |   show (Div ty) = "div"

443 |   show (Mod ty) = "mod"

444 |   show (Neg ty) = "-"

445 |   show (ShiftL ty) = "shiftl"

446 |   show (ShiftR ty) = "shiftr"

447 |   show (BAnd ty) = "&&"

448 |   show (BOr ty) = "||"

449 |   show (BXOr ty) = "xor"

450 |   show (LT ty) = "<"

451 |   show (LTE ty) = "<="

452 |   show (EQ ty) = "=="

453 |   show (GTE ty) = ">="

454 |   show (GT ty) = ">"

455 |   show StrLength = "length"

456 |   show StrHead = "head"

457 |   show StrTail = "tail"

458 |   show StrIndex = "op_strindex"

459 |   show StrCons = "::"

460 |   show StrAppend = "++"

461 |   show StrReverse = "reverse"

462 |   show StrSubstr = "op_strsubstr"

463 |   show DoubleExp = "exp"

464 |   show DoubleLog = "log"

465 |   show DoublePow = "pow"

466 |   show DoubleSin = "sin"

467 |   show DoubleCos = "cos"

468 |   show DoubleTan = "tan"

469 |   show DoubleASin = "asin"

470 |   show DoubleACos = "acos"

471 |   show DoubleATan = "atan"

472 |   show DoubleSqrt = "sqrt"

473 |   show DoubleFloor = "floor"

474 |   show DoubleCeiling = "ceiling"

475 |   show (Cast x y) = "cast-" ++ show x ++ "-" ++ show y

476 |   show BelieveMe = "believe_me"

477 |   show Crash = "crash"

479 | pretty : PrimFn arity -> Doc ann

480 | pretty = pretty0 . show @{Sugared}

482 | annotatedOp : {default False ticked : Bool} -> PrimFn arity -> Doc IdrisSyntax

483 | annotatedOp {ticked} f =

484 |   annotate (Fun . UN . Basic $ show f) (ticks (pretty f))

485 |     where

486 |       ticks : Doc IdrisSyntax -> Doc IdrisSyntax

487 |       ticks = if ticked then enclose "`" "`" else id

490 | prettyOp : PrimFn arity -> Vect arity (Doc IdrisSyntax) -> Doc IdrisSyntax

491 | prettyOp op@(Add ty) [v1,v2] = v1 <++> annotatedOp op <++> v2

492 | prettyOp op@(Sub ty) [v1,v2] = v1 <++> annotatedOp op <++> v2

493 | prettyOp op@(Mul ty) [v1,v2] = v1 <++> annotatedOp op <++> v2

494 | prettyOp op@(Div ty) [v1,v2] = v1 <++> annotatedOp {ticked=True} op <++> v2

495 | prettyOp op@(Mod ty) [v1,v2] = v1 <++> annotatedOp {ticked=True} op <++> v2

496 | prettyOp op@(Neg ty) [v] = annotatedOp op <++> v

497 | prettyOp op@(ShiftL ty) [v1,v2] = annotatedOp op <++> v1 <++> v2

498 | prettyOp op@(ShiftR ty) [v1,v2] = annotatedOp op <++> v1 <++> v2

499 | prettyOp op@(BAnd ty) [v1,v2] = v1 <++> annotatedOp op <++> v2

500 | prettyOp op@(BOr ty) [v1,v2] = v1 <++> annotatedOp op <++> v2

501 | prettyOp op@(BXOr ty) [v1,v2] = v1 <++> annotatedOp {ticked=True} op <++> v2

502 | prettyOp op@(LT ty) [v1,v2] = v1 <++> annotatedOp op <++> v2

503 | prettyOp op@(LTE ty) [v1,v2] = v1 <++> annotatedOp op <++> v2

504 | prettyOp op@(EQ ty) [v1,v2] = v1 <++> annotatedOp op <++> v2

505 | prettyOp op@(GTE ty) [v1,v2] = v1 <++> annotatedOp op <++> v2

506 | prettyOp op@(GT ty) [v1,v2] = v1 <++> annotatedOp op <++> v2

507 | prettyOp op@StrLength [v] = annotatedOp op <++> v

508 | prettyOp op@StrHead [v] = annotatedOp op <++> v

509 | prettyOp op@StrTail [v] = annotatedOp op <++> v

510 | prettyOp op@StrIndex [v1,v2] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "[" <+> v2 <+> annotate (Fun $ UN $ Basic $ show op) "]"

511 | prettyOp op@StrCons [v1,v2] = v1 <++> annotatedOp op <++> v2

512 | prettyOp op@StrAppend [v1,v2] = v1 <++> annotatedOp op <++> v2

513 | prettyOp op@StrReverse [v] = annotatedOp op <++> v

514 | prettyOp op@StrSubstr [v1,v2,v3] = v1 <++> annotate (Fun $ UN $ Basic $ show op) "[" <+> v2 <+> annotate (Fun $ UN $ Basic $ show op) "," <++> v3 <+> annotate (Fun $ UN $ Basic $ show op) "]"

515 | prettyOp op@DoubleExp [v] = annotatedOp op <++> v

516 | prettyOp op@DoubleLog [v] = annotatedOp op <++> v

517 | prettyOp op@DoublePow [v1,v2] = v1 <++> annotatedOp {ticked=True} op <++> v2

518 | prettyOp op@DoubleSin [v] = annotatedOp op <++> v

519 | prettyOp op@DoubleCos [v] = annotatedOp op <++> v

520 | prettyOp op@DoubleTan [v] = annotatedOp op <++> v

521 | prettyOp op@DoubleASin [v] = annotatedOp op <++> v

522 | prettyOp op@DoubleACos [v] = annotatedOp op <++> v

523 | prettyOp op@DoubleATan [v] = annotatedOp op <++> v

524 | prettyOp op@DoubleSqrt [v] = annotatedOp op <++> v

525 | prettyOp op@DoubleFloor [v] = annotatedOp op <++> v

526 | prettyOp op@DoubleCeiling [v] = annotatedOp op <++> v

527 | prettyOp op@(Cast x y) [v] = annotate (Fun $ UN $ Basic $ show op) "[" <+> pretty x <++> annotate (Fun $ UN $ Basic $ show op) "->" <++> pretty y <+> annotate (Fun $ UN $ Basic $ show op) "]" <++> v

528 | prettyOp op@BelieveMe [v1,v2,v3] = annotatedOp op <++> v1 <++> v2 <++> v3

529 | prettyOp op@Crash [v1,v2] = annotatedOp op <++> v1 <++> v2

532 | primFnEq : PrimFn a1 -> PrimFn a2 -> Maybe (a1 = a2)

533 | primFnEq (Add t1) (Add t2) = if t1 == t2 then Just Refl else Nothing

534 | primFnEq (Sub t1) (Sub t2) = if t1 == t2 then Just Refl else Nothing

535 | primFnEq (Mul t1) (Mul t2) = if t1 == t2 then Just Refl else Nothing

536 | primFnEq (Div t1) (Div t2) = if t1 == t2 then Just Refl else Nothing

537 | primFnEq (Mod t1) (Mod t2) = if t1 == t2 then Just Refl else Nothing

538 | primFnEq (Neg t1) (Neg t2) = if t1 == t2 then Just Refl else Nothing

539 | primFnEq (ShiftL t1) (ShiftL t2) = if t1 == t2 then Just Refl else Nothing

540 | primFnEq (ShiftR t1) (ShiftR t2) = if t1 == t2 then Just Refl else Nothing

541 | primFnEq (BAnd t1) (BAnd t2) = if t1 == t2 then Just Refl else Nothing

542 | primFnEq (BOr t1) (BOr t2) = if t1 == t2 then Just Refl else Nothing

543 | primFnEq (BXOr t1) (BXOr t2) = if t1 == t2 then Just Refl else Nothing

544 | primFnEq (LT t1) (LT t2) = if t1 == t2 then Just Refl else Nothing

545 | primFnEq (LTE t1) (LTE t2) = if t1 == t2 then Just Refl else Nothing

546 | primFnEq (EQ t1) (EQ t2) = if t1 == t2 then Just Refl else Nothing

547 | primFnEq (GTE t1) (GTE t2) = if t1 == t2 then Just Refl else Nothing

548 | primFnEq (GT t1) (GT t2) = if t1 == t2 then Just Refl else Nothing

549 | primFnEq StrLength StrLength = Just Refl

550 | primFnEq StrHead StrHead = Just Refl

551 | primFnEq StrTail StrTail = Just Refl

552 | primFnEq StrIndex StrIndex = Just Refl

553 | primFnEq StrCons StrCons = Just Refl

554 | primFnEq StrAppend StrAppend = Just Refl

555 | primFnEq StrReverse StrReverse = Just Refl

556 | primFnEq StrSubstr StrSubstr = Just Refl

557 | primFnEq DoubleExp DoubleExp = Just Refl

558 | primFnEq DoubleLog DoubleLog = Just Refl

559 | primFnEq DoublePow DoublePow = Just Refl

560 | primFnEq DoubleSin DoubleSin = Just Refl

561 | primFnEq DoubleCos DoubleCos = Just Refl

562 | primFnEq DoubleTan DoubleTan = Just Refl

563 | primFnEq DoubleASin DoubleASin = Just Refl

564 | primFnEq DoubleACos DoubleACos = Just Refl

565 | primFnEq DoubleATan DoubleATan = Just Refl

566 | primFnEq DoubleSqrt DoubleSqrt = Just Refl

567 | primFnEq DoubleFloor DoubleFloor = Just Refl

568 | primFnEq DoubleCeiling DoubleCeiling = Just Refl

569 | primFnEq (Cast f1 t1) (Cast f2 t2) = if f1 == f2 && t1 == t2 then Just Refl else Nothing

570 | primFnEq BelieveMe BelieveMe = Just Refl

571 | primFnEq Crash Crash = Just Refl

572 | primFnEq _ _ = Nothing

575 | primFnCmp : PrimFn a1 -> PrimFn a2 -> Ordering

576 | primFnCmp (Add t1) (Add t2) = compare t1 t2

577 | primFnCmp (Sub t1) (Sub t2) = compare t1 t2

578 | primFnCmp (Mul t1) (Mul t2) = compare t1 t2

579 | primFnCmp (Div t1) (Div t2) = compare t1 t2

580 | primFnCmp (Mod t1) (Mod t2) = compare t1 t2

581 | primFnCmp (Neg t1) (Neg t2) = compare t1 t2

582 | primFnCmp (ShiftL t1) (ShiftL t2) = compare t1 t2

583 | primFnCmp (ShiftR t1) (ShiftR t2) = compare t1 t2

584 | primFnCmp (BAnd t1) (BAnd t2) = compare t1 t2

585 | primFnCmp (BOr t1) (BOr t2) = compare t1 t2

586 | primFnCmp (BXOr t1) (BXOr t2) = compare t1 t2

587 | primFnCmp (LT t1) (LT t2) = compare t1 t2

588 | primFnCmp (LTE t1) (LTE t2) = compare t1 t2

589 | primFnCmp (EQ t1) (EQ t2) = compare t1 t2

590 | primFnCmp (GTE t1) (GTE t2) = compare t1 t2

591 | primFnCmp (GT t1) (GT t2) = compare t1 t2

592 | primFnCmp (Cast f1 t1) (Cast f2 t2) = compare f1 f2 `thenCmp` compare t1 t2

593 | primFnCmp f1 f2 = compare (tag f1) (tag f2)

594 |   where

595 |     tag : forall ar. PrimFn ar -> Int

596 |     tag (Add _) = 0

597 |     tag (Sub _) = 1

598 |     tag (Mul _) = 2

599 |     tag (Div _) = 3

600 |     tag (Mod _) = 4

601 |     tag (Neg _) = 5

602 |     tag (ShiftL _) = 6

603 |     tag (ShiftR _) = 7

604 |     tag (BAnd _) = 8

605 |     tag (BOr _) = 9

606 |     tag (BXOr _) = 10

607 |     tag (LT _) = 11

608 |     tag (LTE _) = 12

609 |     tag (EQ _) = 13

610 |     tag (GTE _) = 14

611 |     tag (GT _) = 15

612 |     tag StrLength = 16

613 |     tag StrHead = 17

614 |     tag StrTail = 18

615 |     tag StrIndex = 19

616 |     tag StrCons = 20

617 |     tag StrAppend = 21

618 |     tag StrReverse = 22

619 |     tag StrSubstr = 23

620 |     tag DoubleExp = 24

621 |     tag DoubleLog = 25

622 |     tag DoublePow = 26

623 |     tag DoubleSin = 27

624 |     tag DoubleCos = 28

625 |     tag DoubleTan = 29

626 |     tag DoubleASin = 30

627 |     tag DoubleACos = 31

628 |     tag DoubleATan = 32

629 |     tag DoubleSqrt = 33

630 |     tag DoubleFloor = 34

631 |     tag DoubleCeiling = 35

632 |     tag (Cast _ _) = 36

633 |     tag BelieveMe = 37

634 |     tag Crash = 38