1{-# Language OverloadedStrings, DeriveGeneric, DeriveAnyClass, Safe #-} 2module Cryptol.TypeCheck.TCon where 3 4import qualified Data.Map as Map 5import GHC.Generics (Generic) 6import Control.DeepSeq 7 8import Cryptol.Parser.Selector 9import qualified Cryptol.ModuleSystem.Name as M 10import Cryptol.Utils.Fixity 11import Cryptol.Utils.Ident 12import Cryptol.Utils.PP 13 14-- | This is used for pretty prinitng. 15-- XXX: it would be nice to just rely in the info from the Prelude. 16infixPrimTy :: TCon -> Maybe (Ident,Fixity) 17infixPrimTy = \tc -> Map.lookup tc mp 18 where 19 mp = Map.fromList 20 [ tInfix "==" PC PEqual (n 20) 21 , tInfix "!=" PC PNeq (n 20) 22 , tInfix ">=" PC PGeq (n 30) 23 , tInfix "+" TF TCAdd (l 80) 24 , tInfix "-" TF TCSub (l 80) 25 , tInfix "*" TF TCMul (l 90) 26 , tInfix "/" TF TCDiv (l 90) 27 , tInfix "%" TF TCMod (l 90) 28 , tInfix "^^" TF TCExp (r 95) 29 , tInfix "/^" TF TCCeilDiv (l 90) 30 , tInfix "%^" TF TCCeilMod (l 90) 31 ] 32 33 r x = Fixity { fAssoc = RightAssoc, fLevel = x } 34 l x = Fixity { fAssoc = LeftAssoc, fLevel = x } 35 n x = Fixity { fAssoc = NonAssoc, fLevel = x } 36 37 tInfix x mk tc f = (mk tc, (packIdent x, f)) 38 39 40builtInType :: M.Name -> Maybe TCon 41builtInType nm = 42 case M.nameInfo nm of 43 M.Declared m _ 44 | m == preludeName -> Map.lookup (M.nameIdent nm) builtInTypes 45 | m == floatName -> Map.lookup (M.nameIdent nm) builtInFloat 46 | m == arrayName -> Map.lookup (M.nameIdent nm) builtInArray 47 _ -> Nothing 48 49 where 50 x ~> y = (packIdent x, y) 51 52 -- Built-in types from Float.cry 53 builtInFloat = Map.fromList 54 [ "Float" ~> TC TCFloat 55 , "ValidFloat" ~> PC PValidFloat 56 ] 57 58 -- Built-in types from Cryptol.cry 59 builtInTypes = Map.fromList 60 [ -- Types 61 "inf" ~> TC TCInf 62 , "Bit" ~> TC TCBit 63 , "Integer" ~> TC TCInteger 64 , "Rational" ~> TC TCRational 65 , "Z" ~> TC TCIntMod 66 67 -- Predicate contstructors 68 , "==" ~> PC PEqual 69 , "!=" ~> PC PNeq 70 , ">=" ~> PC PGeq 71 , "fin" ~> PC PFin 72 , "prime" ~> PC PPrime 73 , "Zero" ~> PC PZero 74 , "Logic" ~> PC PLogic 75 , "Ring" ~> PC PRing 76 , "Integral" ~> PC PIntegral 77 , "Field" ~> PC PField 78 , "Round" ~> PC PRound 79 , "Eq" ~> PC PEq 80 , "Cmp" ~> PC PCmp 81 , "SignedCmp" ~> PC PSignedCmp 82 , "Literal" ~> PC PLiteral 83 , "LiteralLessThan" ~> PC PLiteralLessThan 84 , "FLiteral" ~> PC PFLiteral 85 86 -- Type functions 87 , "+" ~> TF TCAdd 88 , "-" ~> TF TCSub 89 , "*" ~> TF TCMul 90 , "/" ~> TF TCDiv 91 , "%" ~> TF TCMod 92 , "^^" ~> TF TCExp 93 , "width" ~> TF TCWidth 94 , "min" ~> TF TCMin 95 , "max" ~> TF TCMax 96 , "/^" ~> TF TCCeilDiv 97 , "%^" ~> TF TCCeilMod 98 , "lengthFromThenTo" ~> TF TCLenFromThenTo 99 ] 100 101 -- Built-in types from Array.cry 102 builtInArray = Map.fromList 103 [ "Array" ~> TC TCArray 104 ] 105 106 107 108 109-------------------------------------------------------------------------------- 110 111infixr 5 :-> 112 113-- | Kinds, classify types. 114data Kind = KType 115 | KNum 116 | KProp 117 | Kind :-> Kind 118 deriving (Eq, Ord, Show, Generic, NFData) 119 120class HasKind t where 121 kindOf :: t -> Kind 122 123instance HasKind TCon where 124 kindOf (TC tc) = kindOf tc 125 kindOf (PC pc) = kindOf pc 126 kindOf (TF tf) = kindOf tf 127 kindOf (TError k) = k 128 129instance HasKind UserTC where 130 kindOf (UserTC _ k) = k 131 132instance HasKind TC where 133 kindOf tcon = 134 case tcon of 135 TCNum _ -> KNum 136 TCInf -> KNum 137 TCBit -> KType 138 TCInteger -> KType 139 TCRational -> KType 140 TCFloat -> KNum :-> KNum :-> KType 141 TCIntMod -> KNum :-> KType 142 TCArray -> KType :-> KType :-> KType 143 TCSeq -> KNum :-> KType :-> KType 144 TCFun -> KType :-> KType :-> KType 145 TCTuple n -> foldr (:->) KType (replicate n KType) 146 TCAbstract x -> kindOf x 147 148instance HasKind PC where 149 kindOf pc = 150 case pc of 151 PEqual -> KNum :-> KNum :-> KProp 152 PNeq -> KNum :-> KNum :-> KProp 153 PGeq -> KNum :-> KNum :-> KProp 154 PFin -> KNum :-> KProp 155 PPrime -> KNum :-> KProp 156 PHas _ -> KType :-> KType :-> KProp 157 PZero -> KType :-> KProp 158 PLogic -> KType :-> KProp 159 PRing -> KType :-> KProp 160 PIntegral -> KType :-> KProp 161 PField -> KType :-> KProp 162 PRound -> KType :-> KProp 163 PEq -> KType :-> KProp 164 PCmp -> KType :-> KProp 165 PSignedCmp -> KType :-> KProp 166 PLiteral -> KNum :-> KType :-> KProp 167 PLiteralLessThan -> KNum :-> KType :-> KProp 168 PFLiteral -> KNum :-> KNum :-> KNum :-> KType :-> KProp 169 PValidFloat -> KNum :-> KNum :-> KProp 170 PAnd -> KProp :-> KProp :-> KProp 171 PTrue -> KProp 172 173instance HasKind TFun where 174 kindOf tfun = 175 case tfun of 176 TCWidth -> KNum :-> KNum 177 178 TCAdd -> KNum :-> KNum :-> KNum 179 TCSub -> KNum :-> KNum :-> KNum 180 TCMul -> KNum :-> KNum :-> KNum 181 TCDiv -> KNum :-> KNum :-> KNum 182 TCMod -> KNum :-> KNum :-> KNum 183 TCExp -> KNum :-> KNum :-> KNum 184 TCMin -> KNum :-> KNum :-> KNum 185 TCMax -> KNum :-> KNum :-> KNum 186 TCCeilDiv -> KNum :-> KNum :-> KNum 187 TCCeilMod -> KNum :-> KNum :-> KNum 188 189 TCLenFromThenTo -> KNum :-> KNum :-> KNum :-> KNum 190 191 192 193-- | Type constants. 194data TCon = TC TC | PC PC | TF TFun | TError Kind 195 deriving (Show, Eq, Ord, Generic, NFData) 196 197 198-- | Predicate symbols. 199-- If you add additional user-visible constructors, please update 'primTys'. 200data PC = PEqual -- ^ @_ == _@ 201 | PNeq -- ^ @_ /= _@ 202 | PGeq -- ^ @_ >= _@ 203 | PFin -- ^ @fin _@ 204 | PPrime -- ^ @prime _@ 205 206 -- classes 207 | PHas Selector -- ^ @Has sel type field@ does not appear in schemas 208 | PZero -- ^ @Zero _@ 209 | PLogic -- ^ @Logic _@ 210 | PRing -- ^ @Ring _@ 211 | PIntegral -- ^ @Integral _@ 212 | PField -- ^ @Field _@ 213 | PRound -- ^ @Round _@ 214 | PEq -- ^ @Eq _@ 215 | PCmp -- ^ @Cmp _@ 216 | PSignedCmp -- ^ @SignedCmp _@ 217 | PLiteral -- ^ @Literal _ _@ 218 | PLiteralLessThan -- ^ @LiteralLessThan _ _@ 219 | PFLiteral -- ^ @FLiteral _ _ _@ 220 221 | PValidFloat -- ^ @ValidFloat _ _@ constraints on supported 222 -- floating point representaitons 223 224 | PAnd -- ^ This is useful when simplifying things in place 225 | PTrue -- ^ Ditto 226 deriving (Show, Eq, Ord, Generic, NFData) 227 228-- | 1-1 constants. 229-- If you add additional user-visible constructors, please update 'primTys'. 230data TC = TCNum Integer -- ^ Numbers 231 | TCInf -- ^ Inf 232 | TCBit -- ^ Bit 233 | TCInteger -- ^ Integer 234 | TCFloat -- ^ Float 235 | TCIntMod -- ^ @Z _@ 236 | TCRational -- ^ @Rational@ 237 | TCArray -- ^ @Array _ _@ 238 | TCSeq -- ^ @[_] _@ 239 | TCFun -- ^ @_ -> _@ 240 | TCTuple Int -- ^ @(_, _, _)@ 241 | TCAbstract UserTC -- ^ An abstract type 242 deriving (Show, Eq, Ord, Generic, NFData) 243 244 245data UserTC = UserTC M.Name Kind 246 deriving (Show, Generic, NFData) 247 248instance Eq UserTC where 249 UserTC x _ == UserTC y _ = x == y 250 251instance Ord UserTC where 252 compare (UserTC x _) (UserTC y _) = compare x y 253 254 255 256 257 258 259-- | Built-in type functions. 260-- If you add additional user-visible constructors, 261-- please update 'primTys' in "Cryptol.Prims.Types". 262data TFun 263 264 = TCAdd -- ^ @ : Num -> Num -> Num @ 265 | TCSub -- ^ @ : Num -> Num -> Num @ 266 | TCMul -- ^ @ : Num -> Num -> Num @ 267 | TCDiv -- ^ @ : Num -> Num -> Num @ 268 | TCMod -- ^ @ : Num -> Num -> Num @ 269 | TCExp -- ^ @ : Num -> Num -> Num @ 270 | TCWidth -- ^ @ : Num -> Num @ 271 | TCMin -- ^ @ : Num -> Num -> Num @ 272 | TCMax -- ^ @ : Num -> Num -> Num @ 273 | TCCeilDiv -- ^ @ : Num -> Num -> Num @ 274 | TCCeilMod -- ^ @ : Num -> Num -> Num @ 275 276 -- Computing the lengths of explicit enumerations 277 | TCLenFromThenTo -- ^ @ : Num -> Num -> Num -> Num@ 278 -- Example: @[ 1, 5 .. 9 ] :: [lengthFromThenTo 1 5 9][b]@ 279 280 deriving (Show, Eq, Ord, Bounded, Enum, Generic, NFData) 281 282 283 284-------------------------------------------------------------------------------- 285-- Pretty printing 286 287instance PP Kind where 288 ppPrec p k = case k of 289 KType -> char '*' 290 KNum -> char '#' 291 KProp -> text "Prop" 292 l :-> r -> optParens (p >= 1) (sep [ppPrec 1 l, text "->", ppPrec 0 r]) 293 294instance PP TCon where 295 ppPrec _ (TC tc) = pp tc 296 ppPrec _ (PC tc) = pp tc 297 ppPrec _ (TF tc) = pp tc 298 ppPrec _ (TError _) = "Error" 299 300 301instance PP PC where 302 ppPrec _ x = 303 case x of 304 PEqual -> text "(==)" 305 PNeq -> text "(/=)" 306 PGeq -> text "(>=)" 307 PFin -> text "fin" 308 PPrime -> text "prime" 309 PHas sel -> parens (ppSelector sel) 310 PZero -> text "Zero" 311 PLogic -> text "Logic" 312 PRing -> text "Ring" 313 PIntegral -> text "Integral" 314 PField -> text "Field" 315 PRound -> text "Round" 316 PEq -> text "Eq" 317 PCmp -> text "Cmp" 318 PSignedCmp -> text "SignedCmp" 319 PLiteral -> text "Literal" 320 PLiteralLessThan -> text "LiteralLessThan" 321 PFLiteral -> text "FLiteral" 322 PValidFloat -> text "ValidFloat" 323 PTrue -> text "True" 324 PAnd -> text "(&&)" 325 326instance PP TC where 327 ppPrec _ x = 328 case x of 329 TCNum n -> integer n 330 TCInf -> text "inf" 331 TCBit -> text "Bit" 332 TCInteger -> text "Integer" 333 TCIntMod -> text "Z" 334 TCRational -> text "Rational" 335 TCArray -> text "Array" 336 TCFloat -> text "Float" 337 TCSeq -> text "[]" 338 TCFun -> text "(->)" 339 TCTuple 0 -> text "()" 340 TCTuple 1 -> text "(one tuple?)" 341 TCTuple n -> parens $ hcat $ replicate (n-1) comma 342 TCAbstract u -> pp u 343 344instance PP UserTC where 345 ppPrec p (UserTC x _) = ppPrec p x 346 347instance PP TFun where 348 ppPrec _ tcon = 349 case tcon of 350 TCAdd -> text "+" 351 TCSub -> text "-" 352 TCMul -> text "*" 353 TCDiv -> text "/" 354 TCMod -> text "%" 355 TCExp -> text "^^" 356 TCWidth -> text "width" 357 TCMin -> text "min" 358 TCMax -> text "max" 359 TCCeilDiv -> text "/^" 360 TCCeilMod -> text "%^" 361 TCLenFromThenTo -> text "lengthFromThenTo" 362