1{-# Language Safe, DeriveGeneric, DeriveAnyClass, RecordWildCards #-}
2{-# Language FlexibleInstances, FlexibleContexts #-}
3{-# Language PatternGuards #-}
4{-# Language OverloadedStrings #-}
5module Cryptol.TypeCheck.Type
6  ( module Cryptol.TypeCheck.Type
7  , module Cryptol.TypeCheck.TCon
8  ) where
9
10
11import GHC.Generics (Generic)
12import Control.DeepSeq
13
14import qualified Data.IntMap as IntMap
15import           Data.Maybe (fromMaybe)
16import           Data.Set (Set)
17import qualified Data.Set as Set
18import           Data.Text (Text)
19
20import Cryptol.Parser.Selector
21import Cryptol.Parser.Position(Range,emptyRange)
22import Cryptol.ModuleSystem.Name
23import Cryptol.Utils.Ident (Ident, isInfixIdent, exprModName)
24import Cryptol.TypeCheck.TCon
25import Cryptol.TypeCheck.PP
26import Cryptol.TypeCheck.Solver.InfNat
27import Cryptol.Utils.Fixity
28import Cryptol.Utils.Panic(panic)
29import Cryptol.Utils.RecordMap
30import Prelude
31
32infix  4 =#=, >==
33infixr 5 `tFun`
34
35
36
37-- | The types of polymorphic values.
38data Schema = Forall { sVars :: [TParam], sProps :: [Prop], sType :: Type }
39              deriving (Eq, Show, Generic, NFData)
40
41-- | Type parameters.
42data TParam = TParam { tpUnique :: !Int       -- ^ Parameter identifier
43                     , tpKind   :: Kind       -- ^ Kind of parameter
44                     , tpFlav   :: TPFlavor
45                        -- ^ What sort of type parameter is this
46                     , tpInfo   :: !TVarInfo
47                       -- ^ A description for better messages.
48                     }
49              deriving (Generic, NFData, Show)
50
51data TPFlavor = TPModParam Name
52              | TPUnifyVar
53              | TPSchemaParam Name
54              | TPTySynParam Name
55              | TPPropSynParam Name
56              | TPNewtypeParam Name
57              | TPPrimParam Name
58              deriving (Generic, NFData, Show)
59
60tMono :: Type -> Schema
61tMono = Forall [] []
62
63isMono :: Schema -> Maybe Type
64isMono s =
65  case s of
66    Forall [] [] t -> Just t
67    _              -> Nothing
68
69
70schemaParam :: Name -> TPFlavor
71schemaParam = TPSchemaParam
72
73tySynParam :: Name -> TPFlavor
74tySynParam = TPTySynParam
75
76propSynParam :: Name -> TPFlavor
77propSynParam = TPPropSynParam
78
79newtypeParam :: Name -> TPFlavor
80newtypeParam = TPNewtypeParam
81
82modTyParam :: Name -> TPFlavor
83modTyParam = TPModParam
84
85
86tpfName :: TPFlavor -> Maybe Name
87tpfName f =
88  case f of
89    TPUnifyVar       -> Nothing
90    TPModParam x     -> Just x
91    TPSchemaParam x  -> Just x
92    TPTySynParam x   -> Just x
93    TPPropSynParam x -> Just x
94    TPNewtypeParam x -> Just x
95    TPPrimParam x    -> Just x
96
97tpName :: TParam -> Maybe Name
98tpName = tpfName . tpFlav
99
100-- | The internal representation of types.
101-- These are assumed to be kind correct.
102data Type   = TCon !TCon ![Type]
103              -- ^ Type constant with args
104
105            | TVar TVar
106              -- ^ Type variable (free or bound)
107
108            | TUser !Name ![Type] !Type
109              {- ^ This is just a type annotation, for a type that
110              was written as a type synonym.  It is useful so that we
111              can use it to report nicer errors.
112              Example: @TUser T ts t@ is really just the type @t@ that
113              was written as @T ts@ by the user. -}
114
115            | TRec !(RecordMap Ident Type)
116              -- ^ Record type
117
118            | TNewtype !Newtype ![Type]
119              -- ^ A newtype
120
121              deriving (Show, Generic, NFData)
122
123
124
125-- | Type variables.
126data TVar   = TVFree !Int Kind (Set TParam) TVarInfo
127              -- ^ Unique, kind, ids of bound type variables that are in scope.
128              -- The last field gives us some info for nicer warnings/errors.
129
130
131            | TVBound {-# UNPACK #-} !TParam
132              deriving (Show, Generic, NFData)
133
134tvInfo :: TVar -> TVarInfo
135tvInfo tv =
136  case tv of
137    TVFree _ _ _ d -> d
138    TVBound tp     -> tpInfo tp
139
140tvUnique :: TVar -> Int
141tvUnique (TVFree u _ _ _) = u
142tvUnique (TVBound TParam { tpUnique = u }) = u
143
144data TVarInfo = TVarInfo { tvarSource :: !Range -- ^ Source code that gave rise
145                         , tvarDesc   :: !TypeSource -- ^ Description
146                         }
147              deriving (Show, Generic, NFData)
148
149
150-- | Explains how this type came to be, for better error messages.
151data TypeSource = TVFromModParam Name     -- ^ Name of module parameter
152                | TVFromSignature Name    -- ^ A variable in a signature
153                | TypeWildCard
154                | TypeOfRecordField Ident
155                | TypeOfTupleField Int
156                | TypeOfSeqElement
157                | LenOfSeq
158                | TypeParamInstNamed {-Fun-}Name {-Param-}Ident
159                | TypeParamInstPos   {-Fun-}Name {-Pos (from 1)-}Int
160                | DefinitionOf Name
161                | LenOfCompGen
162                | TypeOfArg ArgDescr
163                | TypeOfRes
164                | FunApp
165                | TypeOfIfCondExpr
166                | TypeFromUserAnnotation
167                | GeneratorOfListComp
168                | TypeErrorPlaceHolder
169                  deriving (Show, Generic, NFData)
170
171data ArgDescr = ArgDescr
172  { argDescrFun    :: Maybe Name
173  , argDescrNumber :: Maybe Int
174  }
175  deriving (Show,Generic,NFData)
176
177noArgDescr :: ArgDescr
178noArgDescr = ArgDescr { argDescrFun = Nothing, argDescrNumber = Nothing }
179
180-- | Get the names of something that is related to the tvar.
181tvSourceName :: TypeSource -> Maybe Name
182tvSourceName tvs =
183  case tvs of
184    TVFromModParam x -> Just x
185    TVFromSignature x -> Just x
186    TypeParamInstNamed x _ -> Just x
187    TypeParamInstPos x _ -> Just x
188    DefinitionOf x -> Just x
189    TypeOfArg x -> argDescrFun x
190    _ -> Nothing
191
192
193-- | A type annotated with information on how it came about.
194data TypeWithSource = WithSource
195  { twsType   :: Type
196  , twsSource :: TypeSource
197  }
198
199
200-- | The type is supposed to be of kind 'KProp'.
201type Prop   = Type
202
203
204
205
206
207-- | Type synonym.
208data TySyn  = TySyn { tsName        :: Name       -- ^ Name
209                    , tsParams      :: [TParam]   -- ^ Parameters
210                    , tsConstraints :: [Prop]     -- ^ Ensure body is OK
211                    , tsDef         :: Type       -- ^ Definition
212                    , tsDoc         :: !(Maybe Text) -- ^ Documentation
213                    }
214              deriving (Show, Generic, NFData)
215
216
217
218
219
220-- | Named records
221data Newtype  = Newtype { ntName   :: Name
222                        , ntParams :: [TParam]
223                        , ntConstraints :: [Prop]
224                        , ntFields :: RecordMap Ident Type
225                        , ntDoc :: Maybe Text
226                        } deriving (Show, Generic, NFData)
227
228
229instance Eq Newtype where
230  x == y = ntName x == ntName y
231
232instance Ord Newtype where
233  compare x y = compare (ntName x) (ntName y)
234
235
236-- | Information about an abstract type.
237data AbstractType = AbstractType
238  { atName    :: Name
239  , atKind    :: Kind
240  , atCtrs    :: ([TParam], [Prop])
241  , atFixitiy :: Maybe Fixity
242  , atDoc     :: Maybe Text
243  } deriving (Show, Generic, NFData)
244
245
246
247
248--------------------------------------------------------------------------------
249
250
251instance HasKind TVar where
252  kindOf (TVFree  _ k _ _) = k
253  kindOf (TVBound tp) = kindOf tp
254
255instance HasKind Type where
256  kindOf ty =
257    case ty of
258      TVar a      -> kindOf a
259      TCon c ts   -> quickApply (kindOf c) ts
260      TUser _ _ t -> kindOf t
261      TRec {}     -> KType
262      TNewtype{}  -> KType
263
264instance HasKind TySyn where
265  kindOf ts = foldr (:->) (kindOf (tsDef ts)) (map kindOf (tsParams ts))
266
267instance HasKind Newtype where
268  kindOf nt = foldr (:->) KType (map kindOf (ntParams nt))
269
270instance HasKind TParam where
271  kindOf p = tpKind p
272
273quickApply :: Kind -> [a] -> Kind
274quickApply k []               = k
275quickApply (_ :-> k) (_ : ts) = quickApply k ts
276quickApply k _                = panic "Cryptol.TypeCheck.AST.quickApply"
277                                  [ "Applying a non-function kind:", show k ]
278
279kindResult :: Kind -> Kind
280kindResult (_ :-> k) = kindResult k
281kindResult k         = k
282
283--------------------------------------------------------------------------------
284
285-- | Syntactic equality, ignoring type synonyms and record order.
286instance Eq Type where
287  TUser _ _ x == y        = x == y
288  x == TUser _ _ y        = y == x
289
290  TCon x xs == TCon y ys  = x == y && xs == ys
291  TVar x    == TVar y     = x == y
292  TRec xs   == TRec ys    = xs == ys
293  TNewtype ntx xs == TNewtype nty ys = ntx == nty && xs == ys
294
295  _         == _          = False
296
297instance Ord Type where
298  compare x0 y0 =
299    case (x0,y0) of
300      (TUser _ _ t, _)        -> compare t y0
301      (_, TUser _ _ t)        -> compare x0 t
302
303      (TVar x, TVar y)        -> compare x y
304      (TVar {}, _)            -> LT
305      (_, TVar {})            -> GT
306
307      (TCon x xs, TCon y ys)  -> compare (x,xs) (y,ys)
308      (TCon {}, _)            -> LT
309      (_,TCon {})             -> GT
310
311      (TRec xs, TRec ys)      -> compare xs ys
312      (TRec{}, _)             -> LT
313      (_, TRec{})             -> GT
314
315      (TNewtype x xs, TNewtype y ys) -> compare (x,xs) (y,ys)
316
317instance Eq TParam where
318  x == y = tpUnique x == tpUnique y
319
320instance Ord TParam where
321  compare x y = compare (tpUnique x) (tpUnique y)
322
323tpVar :: TParam -> TVar
324tpVar p = TVBound p
325
326-- | The type is "simple" (i.e., it contains no type functions).
327type SType  = Type
328
329
330--------------------------------------------------------------------
331-- Superclass
332
333-- | Compute the set of all @Prop@s that are implied by the
334--   given prop via superclass constraints.
335superclassSet :: Prop -> Set Prop
336
337superclassSet (TCon (PC PPrime) [n]) =
338  Set.fromList [ pFin n, n >== tTwo ]
339
340superclassSet (TCon (PC p0) [t]) = go p0
341  where
342  super p = Set.insert (TCon (PC p) [t]) (go p)
343
344  go PRing      = super PZero
345  go PLogic     = super PZero
346  go PField     = super PRing
347  go PIntegral  = super PRing
348  go PRound     = super PField <> super PCmp
349  go PCmp       = super PEq
350  go PSignedCmp = super PEq
351  go _ = mempty
352
353superclassSet _ = mempty
354
355
356newtypeConType :: Newtype -> Schema
357newtypeConType nt =
358  Forall as (ntConstraints nt)
359    $ TRec (ntFields nt) `tFun` TNewtype nt (map (TVar . tpVar) as)
360  where
361  as = ntParams nt
362
363
364abstractTypeTC :: AbstractType -> TCon
365abstractTypeTC at =
366  case builtInType (atName at) of
367    Just tcon
368      | kindOf tcon == atKind at -> tcon
369      | otherwise ->
370        panic "abstractTypeTC"
371          [ "Mismatch between built-in and declared type."
372          , "Name: " ++ pretty (atName at)
373          , "Declared: " ++ pretty (atKind at)
374          , "Built-in: " ++ pretty (kindOf tcon)
375          ]
376    _         -> TC $ TCAbstract $ UserTC (atName at) (atKind at)
377
378instance Eq TVar where
379  TVBound x       == TVBound y       = x == y
380  TVFree  x _ _ _ == TVFree  y _ _ _ = x == y
381  _             == _              = False
382
383instance Ord TVar where
384  compare (TVFree x _ _ _) (TVFree y _ _ _) = compare x y
385  compare (TVFree _ _ _ _) _                = LT
386  compare _            (TVFree _ _ _ _)     = GT
387
388  compare (TVBound x) (TVBound y) = compare x y
389
390--------------------------------------------------------------------------------
391-- Queries
392
393isFreeTV :: TVar -> Bool
394isFreeTV (TVFree {}) = True
395isFreeTV _           = False
396
397isBoundTV :: TVar -> Bool
398isBoundTV (TVBound {})  = True
399isBoundTV _             = False
400
401
402tIsError :: Type -> Maybe Type
403tIsError ty = case tNoUser ty of
404                TCon (TError _) [t] -> Just t
405                TCon (TError _) _   -> panic "tIsError" ["Malformed error"]
406                _                   -> Nothing
407
408tHasErrors :: Type -> Bool
409tHasErrors ty =
410  case tNoUser ty of
411    TCon (TError _) _   -> True
412    TCon _ ts           -> any tHasErrors ts
413    TRec mp             -> any tHasErrors mp
414    _                   -> False
415
416tIsNat' :: Type -> Maybe Nat'
417tIsNat' ty =
418  case tNoUser ty of
419    TCon (TC (TCNum x)) [] -> Just (Nat x)
420    TCon (TC TCInf)     [] -> Just Inf
421    _                      -> Nothing
422
423tIsNum :: Type -> Maybe Integer
424tIsNum ty = do Nat x <- tIsNat' ty
425               return x
426
427tIsInf :: Type -> Bool
428tIsInf ty = tIsNat' ty == Just Inf
429
430tIsVar :: Type -> Maybe TVar
431tIsVar ty = case tNoUser ty of
432              TVar x -> Just x
433              _      -> Nothing
434
435tIsFun :: Type -> Maybe (Type, Type)
436tIsFun ty = case tNoUser ty of
437              TCon (TC TCFun) [a, b] -> Just (a, b)
438              _                      -> Nothing
439
440tIsSeq :: Type -> Maybe (Type, Type)
441tIsSeq ty = case tNoUser ty of
442              TCon (TC TCSeq) [n, a] -> Just (n, a)
443              _                      -> Nothing
444
445tIsBit :: Type -> Bool
446tIsBit ty = case tNoUser ty of
447              TCon (TC TCBit) [] -> True
448              _                  -> False
449
450tIsInteger :: Type -> Bool
451tIsInteger ty = case tNoUser ty of
452                  TCon (TC TCInteger) [] -> True
453                  _                      -> False
454
455tIsIntMod :: Type -> Maybe Type
456tIsIntMod ty = case tNoUser ty of
457                 TCon (TC TCIntMod) [n] -> Just n
458                 _                      -> Nothing
459
460tIsRational :: Type -> Bool
461tIsRational ty =
462  case tNoUser ty of
463    TCon (TC TCRational) [] -> True
464    _                       -> False
465
466tIsFloat :: Type -> Maybe (Type, Type)
467tIsFloat ty =
468  case tNoUser ty of
469    TCon (TC TCFloat) [e, p] -> Just (e, p)
470    _                        -> Nothing
471
472tIsTuple :: Type -> Maybe [Type]
473tIsTuple ty = case tNoUser ty of
474                TCon (TC (TCTuple _)) ts -> Just ts
475                _                        -> Nothing
476
477tIsRec :: Type -> Maybe (RecordMap Ident Type)
478tIsRec ty = case tNoUser ty of
479              TRec fs -> Just fs
480              _       -> Nothing
481
482tIsBinFun :: TFun -> Type -> Maybe (Type,Type)
483tIsBinFun f ty = case tNoUser ty of
484                   TCon (TF g) [a,b] | f == g -> Just (a,b)
485                   _                          -> Nothing
486
487-- | Split up repeated occurances of the given binary type-level function.
488tSplitFun :: TFun -> Type -> [Type]
489tSplitFun f t0 = go t0 []
490  where go ty xs = case tIsBinFun f ty of
491                     Just (a,b) -> go a (go b xs)
492                     Nothing    -> ty : xs
493
494
495pIsFin :: Prop -> Maybe Type
496pIsFin ty = case tNoUser ty of
497              TCon (PC PFin) [t1] -> Just t1
498              _                   -> Nothing
499
500pIsPrime :: Prop -> Maybe Type
501pIsPrime ty = case tNoUser ty of
502                TCon (PC PPrime) [t1] -> Just t1
503                _                     -> Nothing
504
505pIsGeq :: Prop -> Maybe (Type,Type)
506pIsGeq ty = case tNoUser ty of
507              TCon (PC PGeq) [t1,t2] -> Just (t1,t2)
508              _                      -> Nothing
509
510pIsEqual :: Prop -> Maybe (Type,Type)
511pIsEqual ty = case tNoUser ty of
512                TCon (PC PEqual) [t1,t2] -> Just (t1,t2)
513                _                        -> Nothing
514
515pIsZero :: Prop -> Maybe Type
516pIsZero ty = case tNoUser ty of
517               TCon (PC PZero) [t1] -> Just t1
518               _                    -> Nothing
519
520pIsLogic :: Prop -> Maybe Type
521pIsLogic ty = case tNoUser ty of
522                TCon (PC PLogic) [t1] -> Just t1
523                _                     -> Nothing
524
525pIsRing :: Prop -> Maybe Type
526pIsRing ty = case tNoUser ty of
527                TCon (PC PRing) [t1] -> Just t1
528                _                    -> Nothing
529
530pIsField :: Prop -> Maybe Type
531pIsField ty = case tNoUser ty of
532                TCon (PC PField) [t1] -> Just t1
533                _                     -> Nothing
534
535pIsIntegral :: Prop -> Maybe Type
536pIsIntegral ty = case tNoUser ty of
537                   TCon (PC PIntegral) [t1] -> Just t1
538                   _                        -> Nothing
539
540pIsRound :: Prop -> Maybe Type
541pIsRound ty = case tNoUser ty of
542                     TCon (PC PRound) [t1] -> Just t1
543                     _                     -> Nothing
544
545pIsEq :: Prop -> Maybe Type
546pIsEq ty = case tNoUser ty of
547             TCon (PC PEq) [t1] -> Just t1
548             _                  -> Nothing
549
550pIsCmp :: Prop -> Maybe Type
551pIsCmp ty = case tNoUser ty of
552              TCon (PC PCmp) [t1] -> Just t1
553              _                   -> Nothing
554
555pIsSignedCmp :: Prop -> Maybe Type
556pIsSignedCmp ty = case tNoUser ty of
557                    TCon (PC PSignedCmp) [t1] -> Just t1
558                    _                         -> Nothing
559
560pIsLiteral :: Prop -> Maybe (Type, Type)
561pIsLiteral ty = case tNoUser ty of
562                  TCon (PC PLiteral) [t1, t2] -> Just (t1, t2)
563                  _                           -> Nothing
564
565pIsLiteralLessThan :: Prop -> Maybe (Type, Type)
566pIsLiteralLessThan ty =
567  case tNoUser ty of
568    TCon (PC PLiteralLessThan) [t1, t2] -> Just (t1, t2)
569    _                                   -> Nothing
570
571pIsFLiteral :: Prop -> Maybe (Type,Type,Type,Type)
572pIsFLiteral ty = case tNoUser ty of
573                   TCon (PC PFLiteral) [t1,t2,t3,t4] -> Just (t1,t2,t3,t4)
574                   _                                 -> Nothing
575
576pIsTrue :: Prop -> Bool
577pIsTrue ty  = case tNoUser ty of
578                TCon (PC PTrue) _ -> True
579                _                 -> False
580
581pIsWidth :: Prop -> Maybe Type
582pIsWidth ty = case tNoUser ty of
583                TCon (TF TCWidth) [t1] -> Just t1
584                _                      -> Nothing
585
586pIsValidFloat :: Prop -> Maybe (Type,Type)
587pIsValidFloat ty = case tNoUser ty of
588                     TCon (PC PValidFloat) [a,b] -> Just (a,b)
589                     _                           -> Nothing
590
591--------------------------------------------------------------------------------
592
593
594tNum     :: Integral a => a -> Type
595tNum n    = TCon (TC (TCNum (toInteger n))) []
596
597tZero     :: Type
598tZero     = tNum (0 :: Int)
599
600tOne     :: Type
601tOne      = tNum (1 :: Int)
602
603tTwo     :: Type
604tTwo      = tNum (2 :: Int)
605
606tInf     :: Type
607tInf      = TCon (TC TCInf) []
608
609tNat'    :: Nat' -> Type
610tNat' n'  = case n' of
611              Inf   -> tInf
612              Nat n -> tNum n
613
614tAbstract :: UserTC -> [Type] -> Type
615tAbstract u ts = TCon (TC (TCAbstract u)) ts
616
617tNewtype :: Newtype -> [Type] -> Type
618tNewtype nt ts = TNewtype nt ts
619
620tBit     :: Type
621tBit      = TCon (TC TCBit) []
622
623tInteger :: Type
624tInteger  = TCon (TC TCInteger) []
625
626tRational :: Type
627tRational  = TCon (TC TCRational) []
628
629tFloat   :: Type -> Type -> Type
630tFloat e p = TCon (TC TCFloat) [ e, p ]
631
632tIntMod :: Type -> Type
633tIntMod n = TCon (TC TCIntMod) [n]
634
635tArray :: Type -> Type -> Type
636tArray a b = TCon (TC TCArray) [a, b]
637
638tWord    :: Type -> Type
639tWord a   = tSeq a tBit
640
641tSeq     :: Type -> Type -> Type
642tSeq a b  = TCon (TC TCSeq) [a,b]
643
644tChar :: Type
645tChar = tWord (tNum (8 :: Int))
646
647tString :: Int -> Type
648tString len = tSeq (tNum len) tChar
649
650tRec     :: RecordMap Ident Type -> Type
651tRec      = TRec
652
653tTuple   :: [Type] -> Type
654tTuple ts = TCon (TC (TCTuple (length ts))) ts
655
656-- | Make a function type.
657tFun     :: Type -> Type -> Type
658tFun a b  = TCon (TC TCFun) [a,b]
659
660-- | Eliminate outermost type synonyms.
661tNoUser  :: Type -> Type
662tNoUser t = case t of
663              TUser _ _ a -> tNoUser a
664              _           -> t
665
666
667--------------------------------------------------------------------------------
668-- Construction of type functions
669
670-- | Make an error value of the given type to replace
671-- the given malformed type (the argument to the error function)
672tError :: Type -> Type
673tError t = TCon (TError (k :-> k)) [t]
674  where k = kindOf t
675
676tf1 :: TFun -> Type -> Type
677tf1 f x = TCon (TF f) [x]
678
679tf2 :: TFun -> Type -> Type -> Type
680tf2 f x y = TCon (TF f) [x,y]
681
682tf3 :: TFun -> Type -> Type -> Type -> Type
683tf3 f x y z = TCon (TF f) [x,y,z]
684
685tSub :: Type -> Type -> Type
686tSub = tf2 TCSub
687
688tMul :: Type -> Type -> Type
689tMul = tf2 TCMul
690
691tDiv :: Type -> Type -> Type
692tDiv = tf2 TCDiv
693
694tMod :: Type -> Type -> Type
695tMod = tf2 TCMod
696
697tExp :: Type -> Type -> Type
698tExp = tf2 TCExp
699
700tMin :: Type -> Type -> Type
701tMin = tf2 TCMin
702
703tCeilDiv :: Type -> Type -> Type
704tCeilDiv = tf2 TCCeilDiv
705
706tCeilMod :: Type -> Type -> Type
707tCeilMod = tf2 TCCeilMod
708
709tLenFromThenTo :: Type -> Type -> Type -> Type
710tLenFromThenTo = tf3 TCLenFromThenTo
711
712
713
714
715
716
717--------------------------------------------------------------------------------
718-- Construction of constraints.
719
720-- | Equality for numeric types.
721(=#=) :: Type -> Type -> Prop
722x =#= y = TCon (PC PEqual) [x,y]
723
724(=/=) :: Type -> Type -> Prop
725x =/= y = TCon (PC PNeq) [x,y]
726
727pZero :: Type -> Prop
728pZero t = TCon (PC PZero) [t]
729
730pLogic :: Type -> Prop
731pLogic t = TCon (PC PLogic) [t]
732
733pRing :: Type -> Prop
734pRing t = TCon (PC PRing) [t]
735
736pIntegral :: Type -> Prop
737pIntegral t = TCon (PC PIntegral) [t]
738
739pField :: Type -> Prop
740pField t = TCon (PC PField) [t]
741
742pRound :: Type -> Prop
743pRound t = TCon (PC PRound) [t]
744
745pEq :: Type -> Prop
746pEq t = TCon (PC PEq) [t]
747
748pCmp :: Type -> Prop
749pCmp t = TCon (PC PCmp) [t]
750
751pSignedCmp :: Type -> Prop
752pSignedCmp t = TCon (PC PSignedCmp) [t]
753
754pLiteral :: Type -> Type -> Prop
755pLiteral x y = TCon (PC PLiteral) [x, y]
756
757pLiteralLessThan :: Type -> Type -> Prop
758pLiteralLessThan x y = TCon (PC PLiteralLessThan) [x, y]
759
760-- | Make a greater-than-or-equal-to constraint.
761(>==) :: Type -> Type -> Prop
762x >== y = TCon (PC PGeq) [x,y]
763
764-- | A @Has@ constraint, used for tuple and record selection.
765pHas :: Selector -> Type -> Type -> Prop
766pHas l ty fi = TCon (PC (PHas l)) [ty,fi]
767
768pTrue :: Prop
769pTrue = TCon (PC PTrue) []
770
771pAnd :: [Prop] -> Prop
772pAnd []       = pTrue
773pAnd [x]      = x
774pAnd (x : xs)
775  | Just _ <- tIsError x    = x
776  | pIsTrue x               = rest
777  | Just _ <- tIsError rest = rest
778  | pIsTrue rest            = x
779  | otherwise               = TCon (PC PAnd) [x, rest]
780  where rest = pAnd xs
781
782pSplitAnd :: Prop -> [Prop]
783pSplitAnd p0 = go [p0]
784  where
785  go [] = []
786  go (q : qs) =
787    case tNoUser q of
788      TCon (PC PAnd) [l,r] -> go (l : r : qs)
789      TCon (PC PTrue) _    -> go qs
790      _                    -> q : go qs
791
792pFin :: Type -> Prop
793pFin ty =
794  case tNoUser ty of
795    TCon (TC (TCNum _)) _ -> pTrue
796    TCon (TC TCInf)     _ -> tError prop -- XXX: should we be doing this here??
797    _                     -> prop
798  where
799  prop = TCon (PC PFin) [ty]
800
801pValidFloat :: Type -> Type -> Type
802pValidFloat e p = TCon (PC PValidFloat) [e,p]
803
804pPrime :: Type -> Prop
805pPrime ty =
806  case tNoUser ty of
807    TCon (TC TCInf) _ -> tError prop
808    _ -> prop
809  where
810  prop = TCon (PC PPrime) [ty]
811
812
813--------------------------------------------------------------------------------
814
815noFreeVariables :: FVS t => t -> Bool
816noFreeVariables = all (not . isFreeTV) . Set.toList . fvs
817
818freeParams :: FVS t => t -> Set TParam
819freeParams x = Set.unions (map params (Set.toList (fvs x)))
820  where
821    params (TVFree _ _ tps _) = tps
822    params (TVBound tp) = Set.singleton tp
823
824class FVS t where
825  fvs :: t -> Set TVar
826
827instance FVS Type where
828  fvs = go
829    where
830    go ty =
831      case ty of
832        TCon _ ts   -> fvs ts
833        TVar x      -> Set.singleton x
834        TUser _ _ t -> go t
835        TRec fs     -> fvs (recordElements fs)
836        TNewtype _nt ts -> fvs ts
837
838instance FVS a => FVS (Maybe a) where
839  fvs Nothing  = Set.empty
840  fvs (Just x) = fvs x
841
842instance FVS a => FVS [a] where
843  fvs xs        = Set.unions (map fvs xs)
844
845instance (FVS a, FVS b) => FVS (a,b) where
846  fvs (x,y) = Set.union (fvs x) (fvs y)
847
848instance FVS Schema where
849  fvs (Forall as ps t) =
850      Set.difference (Set.union (fvs ps) (fvs t)) bound
851    where bound = Set.fromList (map tpVar as)
852
853
854
855
856
857-- Pretty Printing -------------------------------------------------------------
858
859instance PP TParam where
860  ppPrec = ppWithNamesPrec IntMap.empty
861
862instance PP (WithNames TParam) where
863  ppPrec _ (WithNames p mp) = ppWithNames mp (tpVar p)
864
865addTNames :: [TParam] -> NameMap -> NameMap
866addTNames as ns = foldr (uncurry IntMap.insert) ns
867                $ named ++ zip unnamed_nums numNames
868                        ++ zip unnamed_vals valNames
869
870  where avail xs = filter (`notElem` used) (nameList xs)
871        numNames = avail ["n","m","i","j","k"]
872        valNames = avail ["a","b","c","d","e"]
873
874        nm x = (tpUnique x, tpName x, tpKind x)
875
876        named        = [ (u,show (pp n)) | (u,Just n,_)  <- map nm as ]
877        unnamed_nums = [ u               | (u,Nothing,KNum)  <- map nm as ]
878        unnamed_vals = [ u               | (u,Nothing,KType) <- map nm as ]
879
880        used    = map snd named ++ IntMap.elems ns
881
882ppNewtypeShort :: Newtype -> Doc
883ppNewtypeShort nt =
884  text "newtype" <+> pp (ntName nt) <+> hsep (map (ppWithNamesPrec nm 9) ps)
885  where
886  ps  = ntParams nt
887  nm = addTNames ps emptyNameMap
888
889
890instance PP Schema where
891  ppPrec = ppWithNamesPrec IntMap.empty
892
893instance PP (WithNames Schema) where
894  ppPrec _ (WithNames s ns)
895    | null (sVars s) && null (sProps s) = body
896    | otherwise = hang (vars <+> props) 2 body
897    where
898    body = ppWithNames ns1 (sType s)
899
900    vars = case sVars s of
901      [] -> empty
902      vs -> braces $ commaSep $ map (ppWithNames ns1) vs
903
904    props = case sProps s of
905      [] -> empty
906      ps -> parens (commaSep (map (ppWithNames ns1) ps)) <+> text "=>"
907
908    ns1 = addTNames (sVars s) ns
909
910instance PP TySyn where
911  ppPrec = ppWithNamesPrec IntMap.empty
912
913instance PP (WithNames TySyn) where
914  ppPrec _ (WithNames ts ns) =
915    text "type" <+> ctr <+> lhs <+> char '=' <+> ppWithNames ns1 (tsDef ts)
916    where ns1 = addTNames (tsParams ts) ns
917          ctr = case kindResult (kindOf ts) of
918                  KProp -> text "constraint"
919                  _     -> empty
920          n = tsName ts
921          lhs = case (nameFixity n, tsParams ts) of
922                  (Just _, [x, y]) ->
923                    ppWithNames ns1 x <+> pp (nameIdent n) <+> ppWithNames ns1 y
924                  (_, ps) ->
925                    pp n <+> sep (map (ppWithNames ns1) ps)
926
927instance PP Newtype where
928  ppPrec = ppWithNamesPrec IntMap.empty
929
930instance PP (WithNames Newtype) where
931  ppPrec _  (WithNames nt _) = ppNewtypeShort nt -- XXX: do the full thing?
932
933
934
935-- | The precedence levels used by this pretty-printing instance
936-- correspond with parser non-terminals as follows:
937--
938--   * 0-1: @type@
939--
940--   * 2: @infix_type@
941--
942--   * 3: @app_type@
943--
944--   * 4: @dimensions atype@
945--
946--   * 5: @atype@
947instance PP (WithNames Type) where
948  ppPrec prec ty0@(WithNames ty nmMap) =
949    case ty of
950      TVar a  -> ppWithNames nmMap a
951      TNewtype nt ts -> optParens (prec > 3) $ pp (ntName nt) <+> fsep (map (go 5) ts)
952      TRec fs -> braces $ fsep $ punctuate comma
953                    [ pp l <+> text ":" <+> go 0 t | (l,t) <- displayFields fs ]
954
955      _ | Just tinf <- isTInfix ty0 -> optParens (prec > 2)
956                                     $ ppInfix 2 isTInfix tinf
957
958      TUser c ts t ->
959        withNameDisp $ \disp ->
960        case nameInfo c of
961          Declared m _
962            | NotInScope <- getNameFormat m (nameIdent c) disp ->
963              go prec t -- unfold type synonym if not in scope
964          _ ->
965            case ts of
966              [] -> pp c
967              _ -> optParens (prec > 3) $ pp c <+> fsep (map (go 5) ts)
968
969      TCon (TC tc) ts ->
970        case (tc,ts) of
971          (TCNum n, [])       -> integer n
972          (TCInf,   [])       -> text "inf"
973          (TCBit,   [])       -> text "Bit"
974          (TCInteger, [])     -> text "Integer"
975          (TCRational, [])    -> text "Rational"
976
977          (TCIntMod, [n])     -> optParens (prec > 3) $ text "Z" <+> go 5 n
978
979          (TCSeq,   [t1,TCon (TC TCBit) []]) -> brackets (go 0 t1)
980          (TCSeq,   [t1,t2])  -> optParens (prec > 4)
981                              $ brackets (go 0 t1) <.> go 4 t2
982
983          (TCFun,   [t1,t2])  -> optParens (prec > 1)
984                              $ go 2 t1 <+> text "->" <+> go 1 t2
985
986          (TCTuple _, fs)     -> parens $ fsep $ punctuate comma $ map (go 0) fs
987
988          (_, _)              -> optParens (prec > 3) $ pp tc <+> fsep (map (go 5) ts)
989
990      TCon (PC pc) ts ->
991        case (pc,ts) of
992          (PEqual, [t1,t2])   -> go 0 t1 <+> text "==" <+> go 0 t2
993          (PNeq ,  [t1,t2])   -> go 0 t1 <+> text "!=" <+> go 0 t2
994          (PGeq,  [t1,t2])    -> go 0 t1 <+> text ">=" <+> go 0 t2
995          (PFin,  [t1])       -> optParens (prec > 3) $ text "fin" <+> (go 5 t1)
996          (PPrime,  [t1])     -> optParens (prec > 3) $ text "prime" <+> (go 5 t1)
997          (PHas x, [t1,t2])   -> ppSelector x <+> text "of"
998                               <+> go 0 t1 <+> text "is" <+> go 0 t2
999          (PAnd, [t1,t2])     -> parens (commaSep (map (go 0) (t1 : pSplitAnd t2)))
1000
1001          (PRing, [t1])       -> pp pc <+> go 5 t1
1002          (PField, [t1])      -> pp pc <+> go 5 t1
1003          (PIntegral, [t1])   -> pp pc <+> go 5 t1
1004          (PRound, [t1])      -> pp pc <+> go 5 t1
1005
1006          (PCmp, [t1])        -> pp pc <+> go 5 t1
1007          (PSignedCmp, [t1])  -> pp pc <+> go 5 t1
1008          (PLiteral, [t1,t2]) -> pp pc <+> go 5 t1 <+> go 5 t2
1009          (PLiteralLessThan, [t1,t2]) -> pp pc <+> go 5 t1 <+> go 5 t2
1010
1011          (_, _)              -> optParens (prec > 3) $ pp pc <+> fsep (map (go 5) ts)
1012
1013      TCon f ts -> optParens (prec > 3)
1014                $ pp f <+> fsep (map (go 5) ts)
1015
1016    where
1017    go p t = ppWithNamesPrec nmMap p t
1018
1019    isTInfix (WithNames (TCon tc [ieLeft',ieRight']) _) =
1020      do let ieLeft  = WithNames ieLeft' nmMap
1021             ieRight = WithNames ieRight' nmMap
1022         (ieOp, ieFixity) <- infixPrimTy tc
1023         return Infix { .. }
1024
1025    isTInfix (WithNames (TUser n [ieLeft',ieRight'] _) _)
1026      | isInfixIdent (nameIdent n) =
1027      do let ieLeft   = WithNames ieLeft' nmMap
1028             ieRight  = WithNames ieRight' nmMap
1029             ieFixity = fromMaybe defaultFixity (nameFixity n)
1030             ieOp     = nameIdent n
1031         return Infix { .. }
1032
1033    isTInfix _ = Nothing
1034
1035
1036
1037instance PP (WithNames TVar) where
1038
1039  ppPrec _ (WithNames tv mp) =
1040    case tv of
1041      TVBound {} -> nmTxt
1042      TVFree {} -> "?" <.> nmTxt
1043    where
1044    nmTxt
1045      | Just a <- IntMap.lookup (tvUnique tv) mp = text a
1046      | otherwise =
1047          case tv of
1048            TVBound x ->
1049              let declNm n = pp n <.> "`" <.> int (tpUnique x) in
1050              case tpFlav x of
1051                TPModParam n     -> ppPrefixName n
1052                TPUnifyVar       -> pickTVarName (tpKind x) (tvarDesc (tpInfo x)) (tpUnique x)
1053                TPSchemaParam n  -> declNm n
1054                TPTySynParam n   -> declNm n
1055                TPPropSynParam n -> declNm n
1056                TPNewtypeParam n -> declNm n
1057                TPPrimParam n    -> declNm n
1058
1059            TVFree x k _ d -> pickTVarName k (tvarDesc d) x
1060
1061
1062pickTVarName :: Kind -> TypeSource -> Int -> Doc
1063pickTVarName k src uni =
1064  text $
1065  case src of
1066    TVFromModParam n       -> using n
1067    TVFromSignature n      -> using n
1068    TypeWildCard           -> mk $ case k of
1069                                     KNum -> "n"
1070                                     _    -> "a"
1071    TypeOfRecordField i    -> using i
1072    TypeOfTupleField n     -> mk ("tup_" ++ show n)
1073    TypeOfSeqElement       -> mk "a"
1074    LenOfSeq               -> mk "n"
1075    TypeParamInstNamed _ i -> using i
1076    TypeParamInstPos f n   -> mk (sh f ++ "_" ++ show n)
1077    DefinitionOf x ->
1078      case nameInfo x of
1079        Declared m SystemName | m == exprModName -> mk "it"
1080        _ -> using x
1081    LenOfCompGen           -> mk "n"
1082    GeneratorOfListComp    -> "seq"
1083    TypeOfIfCondExpr       -> "b"
1084    TypeOfArg ad           -> mk (case argDescrNumber ad of
1085                                    Nothing -> "arg"
1086                                    Just n  -> "arg_" ++ show n)
1087    TypeOfRes              -> "res"
1088    FunApp                 -> "fun"
1089    TypeFromUserAnnotation -> "user"
1090    TypeErrorPlaceHolder   -> "err"
1091  where
1092  sh a      = show (pp a)
1093  using a   = mk (sh a)
1094  mk a      = a ++ "`" ++ show uni
1095
1096instance PP TVar where
1097  ppPrec = ppWithNamesPrec IntMap.empty
1098
1099instance PP Type where
1100  ppPrec n t = ppWithNamesPrec IntMap.empty n t
1101
1102instance PP TVarInfo where
1103  ppPrec _ tvinfo = pp (tvarDesc tvinfo) <+> loc
1104    where
1105    loc = if rng == emptyRange then empty else "at" <+> pp rng
1106    rng = tvarSource tvinfo
1107
1108instance PP ArgDescr where
1109  ppPrec _ ad = which <+> "argument" <+> ofFun
1110        where
1111        which = maybe "function" ordinal (argDescrNumber ad)
1112        ofFun = case argDescrFun ad of
1113                  Nothing -> empty
1114                  Just f  -> "of" <+> pp f
1115
1116
1117
1118instance PP TypeSource where
1119  ppPrec _ tvsrc =
1120    case tvsrc of
1121      TVFromModParam m    -> "module parameter" <+> pp m
1122      TVFromSignature x   -> "signature variable" <+> quotes (pp x)
1123      TypeWildCard        -> "type wildcard (_)"
1124      TypeOfRecordField l -> "type of field" <+> quotes (pp l)
1125      TypeOfTupleField n  -> "type of" <+> ordinal n <+> "tuple field"
1126      TypeOfSeqElement    -> "type of sequence member"
1127      LenOfSeq            -> "length of sequence"
1128      TypeParamInstNamed f i -> "type argument" <+> quotes (pp i) <+>
1129                                          "of" <+> quotes (pp f)
1130      TypeParamInstPos   f i -> ordinal i <+> "type argument of" <+>
1131                                                      quotes (pp f)
1132      DefinitionOf x      -> "the type of" <+> quotes (pp x)
1133      LenOfCompGen        -> "length of comprehension generator"
1134      TypeOfArg ad        -> "type of" <+> pp ad
1135      TypeOfRes             -> "type of function result"
1136      TypeOfIfCondExpr      -> "type of `if` condition"
1137      TypeFromUserAnnotation -> "user annotation"
1138      GeneratorOfListComp    -> "generator in a list comprehension"
1139      FunApp                -> "function call"
1140      TypeErrorPlaceHolder  -> "type error place-holder"
1141