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