diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index 76cde3b6..0d519853 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -33,6 +33,7 @@ import Cryptol.ModuleSystem.Exports import Cryptol.Prims.Syntax import Cryptol.Parser.AST import Cryptol.Parser.Position +import Cryptol.TypeCheck.Type (TCon(..)) import Cryptol.Utils.Ident (packIdent,packInfix) import Cryptol.Utils.Panic (panic) import Cryptol.Utils.PP @@ -622,14 +623,12 @@ instance Rename Type where | Just (arity,fun) <- Map.lookup pn tfunNames = do when (arity /= length ps) (record (MalformedBuiltin ty0 pn)) ps' <- traverse go ps - return (TApp fun ps') + return (TApp (TF fun) ps') -- built-in types like Bit and inf - | Just ty <- Map.lookup pn tconNames = - do unless (null ps) (record (MalformedBuiltin ty0 pn)) - -- this should really be a kind error, but our syntax - -- currently has no way to represent the broken type. - rename ty + | Just tc <- Map.lookup pn tconNames = + do ps' <- traverse go ps + return (TApp (TC tc) ps') go (TUser qn ps) = TUser <$> renameType qn <*> traverse go ps go (TApp f xs) = TApp f <$> traverse go xs @@ -698,12 +697,12 @@ mkTInfix t@(TUser o1 [x,y]) op@(o2,f2) z FCError -> return (o2 t z) -- In this case, we know the fixities of both sides. -mkTInfix t@(TApp o1 [x,y]) op@(o2,f2) z +mkTInfix t@(TApp (TF o1) [x,y]) op@(o2,f2) z | Just (a1,p1) <- Map.lookup o1 tBinOpPrec = case compareFixity (Fixity a1 p1) f2 of FCLeft -> return (o2 t z) FCRight -> do r <- mkTInfix y op z - return (TApp o1 [x,r]) + return (TApp (TF o1) [x,r]) -- As the fixity table is known, and this is a case where the fixity came -- from that table, it's a real error if the fixities didn't work out. @@ -722,7 +721,7 @@ mkTInfix t (op,_) z = lookupFixity :: Located PName -> (TOp,Fixity) lookupFixity op = case lkp of - Just (p,f) -> (\x y -> TApp p [x,y], f) + Just (p,f) -> (\x y -> TApp (TF p) [x,y], f) -- unknown type operator, just use default fixity -- NOTE: this works for the props defined above, as all other operators diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index 0e950b18..20684d58 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -75,7 +75,7 @@ import Cryptol.Parser.Fixity import Cryptol.Parser.Name import Cryptol.Parser.Position import Cryptol.Parser.Selector -import Cryptol.Prims.Syntax (TFun(..)) +import Cryptol.TypeCheck.Type (TCon(..), TC(..)) import Cryptol.Utils.Ident import Cryptol.Utils.PP @@ -321,11 +321,11 @@ data Type n = TFun (Type n) (Type n) -- ^ @[8] -> [8]@ | TInf -- ^ @inf@ | TUser n [Type n] -- ^ A type variable or synonym - | TApp TFun [Type n] + | TApp TCon [Type n] -- ^ @2 + x@ -- Note that the parser never produces these; instead it - -- prduces a "TUser" valued. The "TApp" is introduced by - -- the renamed when it spots built-in functions. + -- produces a "TUser" value. The "TApp" is introduced by + -- the renamer when it spots built-in functions. -- XXX: We should just add primitive declarations for the -- built-in type functions, and simplify all this. @@ -342,11 +342,11 @@ data Type n = TFun (Type n) (Type n) -- ^ @[8] -> [8]@ -- If this changes, we should update it. -- XXX: As in the case of TApp, this would all go away if these were -- just declared. -tconNames :: Map.Map PName (Type PName) +tconNames :: Map.Map PName TC tconNames = Map.fromList - [ (mkUnqual (packIdent "Bit"), TBit) - , (mkUnqual (packIdent "Integer"), TInteger) - , (mkUnqual (packIdent "inf"), TInf) + [ (mkUnqual (packIdent "Bit"), TCBit) + , (mkUnqual (packIdent "Integer"), TCInteger) + , (mkUnqual (packIdent "inf"), TCInf) ] data Prop n = CFin (Type n) -- ^ @ fin x @ diff --git a/src/Cryptol/Parser/Utils.hs b/src/Cryptol/Parser/Utils.hs index 30f3c7ae..010da8f8 100644 --- a/src/Cryptol/Parser/Utils.hs +++ b/src/Cryptol/Parser/Utils.hs @@ -18,6 +18,7 @@ module Cryptol.Parser.Utils import Cryptol.Parser.AST import Cryptol.Prims.Syntax +import Cryptol.TypeCheck.Type (TCon(TF)) widthIdent :: Ident @@ -51,7 +52,7 @@ translateExprToNumT expr = TUser f ts -> return (TUser f (ts ++ [t])) _ -> Nothing - mkFun f = return (TApp f []) + mkFun f = return (TApp (TF f) []) cvtLit (ECNum n CharLit) = return (TChar $ toEnum $ fromInteger n) cvtLit (ECNum n _) = return (TNum n) diff --git a/src/Cryptol/TypeCheck/Kind.hs b/src/Cryptol/TypeCheck/Kind.hs index 1f6b6581..2acafc79 100644 --- a/src/Cryptol/TypeCheck/Kind.hs +++ b/src/Cryptol/TypeCheck/Kind.hs @@ -342,8 +342,8 @@ doCheckType ty k = P.TNum n -> tcon (TC (TCNum n)) [] k P.TChar n -> tcon (TC (TCNum $ fromIntegral $ fromEnum n)) [] k P.TInf -> tcon (TC TCInf) [] k - P.TApp tf ts -> - do it <- tcon (TF tf) ts k + P.TApp tc ts -> + do it <- tcon tc ts k -- Now check for additional well-formedness -- constraints. diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs index 0140c0eb..b554ad73 100644 --- a/src/Cryptol/TypeCheck/Type.hs +++ b/src/Cryptol/TypeCheck/Type.hs @@ -890,6 +890,19 @@ instance PP TCon where ppPrec _ (TF tc) = pp tc ppPrec _ (TError _ msg) = pp msg +instance PPName TCon where + ppNameFixity (TC _) = Nothing + ppNameFixity (PC _) = Nothing + ppNameFixity (TF tf) = ppNameFixity tf + + ppPrefixName (TC tc) = pp tc + ppPrefixName (PC pc) = pp pc + ppPrefixName (TF tf) = ppPrefixName tf + + ppInfixName (TC tc) = pp tc + ppInfixName (PC pc) = pp pc + ppInfixName (TF tf) = ppInfixName tf + instance PP TCErrorMessage where ppPrec _ tc = parens (text "error:" <+> text (tcErrorMessage tc))