1-- | 2-- Module : Cryptol.TypeCheck.Solver.Class 3-- Copyright : (c) 2013-2016 Galois, Inc. 4-- License : BSD3 5-- Maintainer : cryptol@galois.com 6-- Stability : provisional 7-- Portability : portable 8-- 9-- Solving class constraints. 10 11{-# LANGUAGE PatternGuards #-} 12module Cryptol.TypeCheck.Solver.Class 13 ( solveZeroInst 14 , solveLogicInst 15 , solveRingInst 16 , solveFieldInst 17 , solveIntegralInst 18 , solveRoundInst 19 , solveEqInst 20 , solveCmpInst 21 , solveSignedCmpInst 22 , solveLiteralInst 23 , solveLiteralLessThanInst 24 , solveFLiteralInst 25 , solveValidFloat 26 ) where 27 28import qualified LibBF as FP 29 30import Cryptol.TypeCheck.Type hiding (tSub) 31import Cryptol.TypeCheck.SimpType (tAdd,tSub,tWidth,tMax) 32import Cryptol.TypeCheck.Solver.Types 33import Cryptol.Utils.RecordMap 34 35{- | This places constraints on the floating point numbers that 36we can work with. This is a bit of an odd check, as it is really 37a limitiation of the backend, and not the language itself. 38 39On the other hand, it helps us give sane results if one accidentally 40types a polymorphic float at the REPL. Hopefully, most users will 41stick to particular FP sizes, so this should be quite transparent. 42-} 43solveValidFloat :: Type -> Type -> Solved 44solveValidFloat e p 45 | Just _ <- knownSupportedFloat e p = SolvedIf [] 46 | otherwise = Unsolved 47 48-- | Check that the type parameters correspond to a float that 49-- we support, and if so make the precision settings for the BigFloat library. 50knownSupportedFloat :: Type -> Type -> Maybe FP.BFOpts 51knownSupportedFloat et pt 52 | Just e <- tIsNum et, Just p <- tIsNum pt 53 , minExp <= e && e <= maxExp && minPrec <= p && p <= maxPrec = 54 Just (FP.expBits (fromInteger e) <> FP.precBits (fromInteger p) 55 <> FP.allowSubnormal) 56 | otherwise = Nothing 57 where 58 minExp = max 2 (toInteger FP.expBitsMin) 59 maxExp = toInteger FP.expBitsMax 60 61 minPrec = max 2 (toInteger FP.precBitsMin) 62 maxPrec = toInteger FP.precBitsMax 63 64 65 66 67-- | Solve a Zero constraint by instance, if possible. 68solveZeroInst :: Type -> Solved 69solveZeroInst ty = case tNoUser ty of 70 71 -- Zero Error -> fails 72 TCon (TError {}) _ -> Unsolvable 73 74 -- Zero Bit 75 TCon (TC TCBit) [] -> SolvedIf [] 76 77 -- Zero Integer 78 TCon (TC TCInteger) [] -> SolvedIf [] 79 80 -- Zero (Z n) 81 TCon (TC TCIntMod) [n] -> SolvedIf [ pFin n, n >== tOne ] 82 83 -- Zero Real 84 85 -- Zero Rational 86 TCon (TC TCRational) [] -> SolvedIf [] 87 88 -- ValidVloat e p => Zero (Float e p) 89 TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ] 90 91 -- Zero a => Zero [n]a 92 TCon (TC TCSeq) [_, a] -> SolvedIf [ pZero a ] 93 94 -- Zero b => Zero (a -> b) 95 TCon (TC TCFun) [_, b] -> SolvedIf [ pZero b ] 96 97 -- (Zero a, Zero b) => Zero (a,b) 98 TCon (TC (TCTuple _)) es -> SolvedIf [ pZero e | e <- es ] 99 100 -- (Zero a, Zero b) => Zero { x1 : a, x2 : b } 101 TRec fs -> SolvedIf [ pZero ety | ety <- recordElements fs ] 102 103 -- Zero <newtype> -> fails 104 TNewtype{} -> Unsolvable 105 106 _ -> Unsolved 107 108-- | Solve a Logic constraint by instance, if possible. 109solveLogicInst :: Type -> Solved 110solveLogicInst ty = case tNoUser ty of 111 112 -- Logic Error -> fails 113 TCon (TError {}) _ -> Unsolvable 114 115 -- Logic Bit 116 TCon (TC TCBit) [] -> SolvedIf [] 117 118 -- Logic Integer fails 119 TCon (TC TCInteger) [] -> Unsolvable 120 121 -- Logic (Z n) fails 122 TCon (TC TCIntMod) [_] -> Unsolvable 123 124 -- Logic Rational fails 125 TCon (TC TCRational) [] -> Unsolvable 126 127 -- Logic (Float e p) fails 128 TCon (TC TCFloat) [_, _] -> Unsolvable 129 130 -- Logic a => Logic [n]a 131 TCon (TC TCSeq) [_, a] -> SolvedIf [ pLogic a ] 132 133 -- Logic b => Logic (a -> b) 134 TCon (TC TCFun) [_, b] -> SolvedIf [ pLogic b ] 135 136 -- (Logic a, Logic b) => Logic (a,b) 137 TCon (TC (TCTuple _)) es -> SolvedIf [ pLogic e | e <- es ] 138 139 -- (Logic a, Logic b) => Logic { x1 : a, x2 : b } 140 TRec fs -> SolvedIf [ pLogic ety | ety <- recordElements fs ] 141 142 -- Logic <newtype> -> fails 143 TNewtype{} -> Unsolvable 144 145 _ -> Unsolved 146 147 148-- | Solve a Ring constraint by instance, if possible. 149solveRingInst :: Type -> Solved 150solveRingInst ty = case tNoUser ty of 151 152 -- Ring Error -> fails 153 TCon (TError {}) _ -> Unsolvable 154 155 -- Ring [n]e 156 TCon (TC TCSeq) [n, e] -> solveRingSeq n e 157 158 -- Ring b => Ring (a -> b) 159 TCon (TC TCFun) [_,b] -> SolvedIf [ pRing b ] 160 161 -- (Ring a, Ring b) => Arith (a,b) 162 TCon (TC (TCTuple _)) es -> SolvedIf [ pRing e | e <- es ] 163 164 -- Ring Bit fails 165 TCon (TC TCBit) [] -> Unsolvable 166 167 -- Ring Integer 168 TCon (TC TCInteger) [] -> SolvedIf [] 169 170 -- Ring (Z n) 171 TCon (TC TCIntMod) [n] -> SolvedIf [ pFin n, n >== tOne ] 172 173 -- Ring Rational 174 TCon (TC TCRational) [] -> SolvedIf [] 175 176 -- ValidFloat e p => Ring (Float e p) 177 TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ] 178 179 -- (Ring a, Ring b) => Ring { x1 : a, x2 : b } 180 TRec fs -> SolvedIf [ pRing ety | ety <- recordElements fs ] 181 182 -- Ring <newtype> -> fails 183 TNewtype{} -> Unsolvable 184 185 _ -> Unsolved 186 187 188-- | Solve a Ring constraint for a sequence. The type passed here is the 189-- element type of the sequence. 190solveRingSeq :: Type -> Type -> Solved 191solveRingSeq n ty = case tNoUser ty of 192 193 -- fin n => Ring [n]Bit 194 TCon (TC TCBit) [] -> SolvedIf [ pFin n ] 195 196 -- variables are not solvable. 197 TVar {} -> case tNoUser n of 198 {- We are sure that the lenght is not `fin`, so the 199 special case for `Bit` does not apply. 200 Arith ty => Arith [n]ty -} 201 TCon (TC TCInf) [] -> SolvedIf [ pRing ty ] 202 _ -> Unsolved 203 204 -- Ring ty => Ring [n]ty 205 _ -> SolvedIf [ pRing ty ] 206 207 208-- | Solve an Integral constraint by instance, if possible. 209solveIntegralInst :: Type -> Solved 210solveIntegralInst ty = case tNoUser ty of 211 212 -- Integral Error -> fails 213 TCon (TError {}) _ -> Unsolvable 214 215 -- Integral Bit fails 216 TCon (TC TCBit) [] -> Unsolvable 217 218 -- Integral Integer 219 TCon (TC TCInteger) [] -> SolvedIf [] 220 221 -- fin n => Integral [n] 222 TCon (TC TCSeq) [n, elTy] -> 223 case tNoUser elTy of 224 TCon (TC TCBit) [] -> SolvedIf [ pFin n ] 225 TVar _ -> Unsolved 226 _ -> Unsolvable 227 228 TVar _ -> Unsolved 229 230 _ -> Unsolvable 231 232 233-- | Solve a Field constraint by instance, if possible. 234solveFieldInst :: Type -> Solved 235solveFieldInst ty = case tNoUser ty of 236 237 -- Field Error -> fails 238 TCon (TError {}) _ -> Unsolvable 239 240 -- Field Bit fails 241 TCon (TC TCBit) [] -> Unsolvable 242 243 -- Field Integer fails 244 TCon (TC TCInteger) [] -> Unsolvable 245 246 -- Field Rational 247 TCon (TC TCRational) [] -> SolvedIf [] 248 249 -- ValidFloat e p => Field (Float e p) 250 TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ] 251 252 -- Field Real 253 254 -- Field (Z n) 255 TCon (TC TCIntMod) [n] -> SolvedIf [ pPrime n ] 256 257 -- Field ([n]a) fails 258 TCon (TC TCSeq) [_, _] -> Unsolvable 259 260 -- Field (a -> b) fails 261 TCon (TC TCFun) [_, _] -> Unsolvable 262 263 -- Field (a, b, ...) fails 264 TCon (TC (TCTuple _)) _ -> Unsolvable 265 266 -- Field {x : a, y : b, ...} fails 267 TRec _ -> Unsolvable 268 269 -- Field <newtype> -> fails 270 TNewtype{} -> Unsolvable 271 272 _ -> Unsolved 273 274 275-- | Solve a Round constraint by instance, if possible. 276solveRoundInst :: Type -> Solved 277solveRoundInst ty = case tNoUser ty of 278 279 -- Round Error -> fails 280 TCon (TError {}) _ -> Unsolvable 281 282 -- Round Bit fails 283 TCon (TC TCBit) [] -> Unsolvable 284 285 -- Round Integer fails 286 TCon (TC TCInteger) [] -> Unsolvable 287 288 -- Round (Z n) fails 289 TCon (TC TCIntMod) [_] -> Unsolvable 290 291 -- Round Rational 292 TCon (TC TCRational) [] -> SolvedIf [] 293 294 -- ValidFloat e p => Round (Float e p) 295 TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ] 296 297 -- Round Real 298 299 -- Round ([n]a) fails 300 TCon (TC TCSeq) [_, _] -> Unsolvable 301 302 -- Round (a -> b) fails 303 TCon (TC TCFun) [_, _] -> Unsolvable 304 305 -- Round (a, b, ...) fails 306 TCon (TC (TCTuple _)) _ -> Unsolvable 307 308 -- Round {x : a, y : b, ...} fails 309 TRec _ -> Unsolvable 310 311 -- Round <newtype> -> fails 312 TNewtype{} -> Unsolvable 313 314 _ -> Unsolved 315 316 317 318-- | Solve Eq constraints. 319solveEqInst :: Type -> Solved 320solveEqInst ty = case tNoUser ty of 321 322 -- Eq Error -> fails 323 TCon (TError {}) _ -> Unsolvable 324 325 -- eq Bit 326 TCon (TC TCBit) [] -> SolvedIf [] 327 328 -- Eq Integer 329 TCon (TC TCInteger) [] -> SolvedIf [] 330 331 -- Eq Rational 332 TCon (TC TCRational) [] -> SolvedIf [] 333 334 -- ValidFloat e p => Eq (Float e p) 335 TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ] 336 337 -- Eq (Z n) 338 TCon (TC TCIntMod) [n] -> SolvedIf [ pFin n, n >== tOne ] 339 340 -- (fin n, Eq a) => Eq [n]a 341 TCon (TC TCSeq) [n,a] -> SolvedIf [ pFin n, pEq a ] 342 343 -- (Eq a, Eq b) => Eq (a,b) 344 TCon (TC (TCTuple _)) es -> SolvedIf (map pEq es) 345 346 -- Eq (a -> b) fails 347 TCon (TC TCFun) [_,_] -> Unsolvable 348 349 -- (Eq a, Eq b) => Eq { x:a, y:b } 350 TRec fs -> SolvedIf [ pEq e | e <- recordElements fs ] 351 352 -- Eq <newtype> -> fails 353 TNewtype{} -> Unsolvable 354 355 _ -> Unsolved 356 357 358-- | Solve Cmp constraints. 359solveCmpInst :: Type -> Solved 360solveCmpInst ty = case tNoUser ty of 361 362 -- Cmp Error -> fails 363 TCon (TError {}) _ -> Unsolvable 364 365 -- Cmp Bit 366 TCon (TC TCBit) [] -> SolvedIf [] 367 368 -- Cmp Integer 369 TCon (TC TCInteger) [] -> SolvedIf [] 370 371 -- Cmp Rational 372 TCon (TC TCRational) [] -> SolvedIf [] 373 374 -- Cmp (Z n) fails 375 TCon (TC TCIntMod) [_] -> Unsolvable 376 377 -- ValidFloat e p => Cmp (Float e p) 378 TCon (TC TCFloat) [e,p] -> SolvedIf [ pValidFloat e p ] 379 380 -- (fin n, Cmp a) => Cmp [n]a 381 TCon (TC TCSeq) [n,a] -> SolvedIf [ pFin n, pCmp a ] 382 383 -- (Cmp a, Cmp b) => Cmp (a,b) 384 TCon (TC (TCTuple _)) es -> SolvedIf (map pCmp es) 385 386 -- Cmp (a -> b) fails 387 TCon (TC TCFun) [_,_] -> Unsolvable 388 389 -- (Cmp a, Cmp b) => Cmp { x:a, y:b } 390 TRec fs -> SolvedIf [ pCmp e | e <- recordElements fs ] 391 392 -- Cmp <newtype> -> fails 393 TNewtype{} -> Unsolvable 394 395 _ -> Unsolved 396 397 398-- | Solve a SignedCmp constraint for a sequence. The type passed here is the 399-- element type of the sequence. 400solveSignedCmpSeq :: Type -> Type -> Solved 401solveSignedCmpSeq n ty = case tNoUser ty of 402 403 -- (fin n, n >=1 ) => SignedCmp [n]Bit 404 TCon (TC TCBit) [] -> SolvedIf [ pFin n, n >== tNum (1 :: Integer) ] 405 406 -- variables are not solvable. 407 TVar {} -> Unsolved 408 409 -- (fin n, SignedCmp ty) => SignedCmp [n]ty, when ty != Bit 410 _ -> SolvedIf [ pFin n, pSignedCmp ty ] 411 412 413-- | Solve SignedCmp constraints. 414solveSignedCmpInst :: Type -> Solved 415solveSignedCmpInst ty = case tNoUser ty of 416 417 -- SignedCmp Error -> fails 418 TCon (TError {}) _ -> Unsolvable 419 420 -- SignedCmp Bit fails 421 TCon (TC TCBit) [] -> Unsolvable 422 423 -- SignedCmp Integer fails 424 TCon (TC TCInteger) [] -> Unsolvable 425 426 -- SignedCmp (Z n) fails 427 TCon (TC TCIntMod) [_] -> Unsolvable 428 429 -- SignedCmp Rational fails 430 TCon (TC TCRational) [] -> Unsolvable 431 432 -- SignedCmp (Float e p) fails 433 TCon (TC TCFloat) [_, _] -> Unsolvable 434 435 -- SignedCmp for sequences 436 TCon (TC TCSeq) [n,a] -> solveSignedCmpSeq n a 437 438 -- (SignedCmp a, SignedCmp b) => SignedCmp (a,b) 439 TCon (TC (TCTuple _)) es -> SolvedIf (map pSignedCmp es) 440 441 -- SignedCmp (a -> b) fails 442 TCon (TC TCFun) [_,_] -> Unsolvable 443 444 -- (SignedCmp a, SignedCmp b) => SignedCmp { x:a, y:b } 445 TRec fs -> SolvedIf [ pSignedCmp e | e <- recordElements fs ] 446 447 -- SignedCmp <newtype> -> fails 448 TNewtype{} -> Unsolvable 449 450 _ -> Unsolved 451 452 453-- | Solving fractional literal constraints. 454solveFLiteralInst :: Type -> Type -> Type -> Type -> Solved 455solveFLiteralInst numT denT rndT ty 456 | TCon (TError {}) _ <- tNoUser numT = Unsolvable 457 | TCon (TError {}) _ <- tNoUser denT = Unsolvable 458 | tIsInf numT || tIsInf denT || tIsInf rndT = Unsolvable 459 | Just 0 <- tIsNum denT = Unsolvable 460 461 | otherwise = 462 case tNoUser ty of 463 TVar {} -> Unsolved 464 465 TCon (TError {}) _ -> Unsolvable 466 467 TCon (TC TCRational) [] -> 468 SolvedIf [ pFin numT, pFin denT, denT >== tOne ] 469 470 TCon (TC TCFloat) [e,p] 471 | Just 0 <- tIsNum rndT -> 472 SolvedIf [ pValidFloat e p 473 , pFin numT, pFin denT, denT >== tOne ] 474 475 | Just _ <- tIsNum rndT 476 , Just opts <- knownSupportedFloat e p 477 , Just n <- tIsNum numT 478 , Just d <- tIsNum denT 479 -> case FP.bfDiv opts (FP.bfFromInteger n) (FP.bfFromInteger d) of 480 (_, FP.Ok) -> SolvedIf [] 481 _ -> Unsolvable 482 483 | otherwise -> Unsolved 484 485 _ -> Unsolvable 486 487 488-- | Solve Literal constraints. 489solveLiteralInst :: Type -> Type -> Solved 490solveLiteralInst val ty 491 | TCon (TError {}) _ <- tNoUser val = Unsolvable 492 | otherwise = 493 case tNoUser ty of 494 495 -- Literal n Error -> fails 496 TCon (TError {}) _ -> Unsolvable 497 498 -- (1 >= val) => Literal val Bit 499 TCon (TC TCBit) [] -> SolvedIf [ tOne >== val ] 500 501 -- (fin val) => Literal val Integer 502 TCon (TC TCInteger) [] -> SolvedIf [ pFin val ] 503 504 -- (fin val) => Literal val Rational 505 TCon (TC TCRational) [] -> SolvedIf [ pFin val ] 506 507 -- ValidFloat e p => Literal val (Float e p) if `val` is representable 508 TCon (TC TCFloat) [e,p] 509 | Just n <- tIsNum val 510 , Just opts <- knownSupportedFloat e p -> 511 let bf = FP.bfFromInteger n 512 in case FP.bfRoundFloat opts bf of 513 (bf1,FP.Ok) | bf == bf1 -> SolvedIf [] 514 _ -> Unsolvable 515 516 | otherwise -> Unsolved 517 518 519 -- (fin val, fin m, m >= val + 1) => Literal val (Z m) 520 TCon (TC TCIntMod) [modulus] -> 521 SolvedIf [ pFin val, pFin modulus, modulus >== tAdd val tOne ] 522 523 -- (fin bits, bits >= width n) => Literal n [bits] 524 TCon (TC TCSeq) [bits, elTy] 525 | TCon (TC TCBit) [] <- ety -> 526 SolvedIf [ pFin val, pFin bits, bits >== tWidth val ] 527 | TVar _ <- ety -> Unsolved 528 where ety = tNoUser elTy 529 530 TVar _ -> Unsolved 531 532 _ -> Unsolvable 533 534 535-- | Solve Literal constraints. 536solveLiteralLessThanInst :: Type -> Type -> Solved 537solveLiteralLessThanInst val ty 538 | TCon (TError {}) _ <- tNoUser val = Unsolvable 539 | otherwise = 540 case tNoUser ty of 541 542 -- Literal n Error -> fails 543 TCon (TError {}) _ -> Unsolvable 544 545 -- (2 >= val) => LiteralLessThan val Bit 546 TCon (TC TCBit) [] -> SolvedIf [ tTwo >== val ] 547 548 -- LiteralLessThan val Integer 549 TCon (TC TCInteger) [] -> SolvedIf [ ] 550 551 -- LiteralLessThan val Rational 552 TCon (TC TCRational) [] -> SolvedIf [ ] 553 554 -- ValidFloat e p => LiteralLessThan val (Float e p) if `val-1` is representable 555 -- RWD Should we remove this instance for floats? 556 TCon (TC TCFloat) [e, p] 557 | Just n <- tIsNum val 558 , n > 0 559 , Just opts <- knownSupportedFloat e p -> 560 let bf = FP.bfFromInteger (n-1) 561 in case FP.bfRoundFloat opts bf of 562 (bf1,FP.Ok) | bf == bf1 -> SolvedIf [] 563 _ -> Unsolvable 564 565 | otherwise -> Unsolved 566 567 -- (fin val, fin m, m >= val) => LiteralLessThan val (Z m) 568 TCon (TC TCIntMod) [modulus] -> 569 SolvedIf [ pFin val, pFin modulus, modulus >== val ] 570 571 -- (fin bits, bits >= lg2 n) => LiteralLessThan n [bits] 572 TCon (TC TCSeq) [bits, elTy] 573 | TCon (TC TCBit) [] <- ety -> 574 SolvedIf [ pFin val, pFin bits, bits >== tWidth val' ] 575 | TVar _ <- ety -> Unsolved 576 where ety = tNoUser elTy 577 val' = tSub (tMax val tOne) tOne 578 579 TVar _ -> Unsolved 580 581 _ -> Unsolvable 582