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