mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-17 13:01:31 +03:00
Renamer handles built-in types like Integer
and Bit
using TApp
.
This commit is contained in:
parent
d5c9a030da
commit
9188878c4e
@ -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
|
||||
|
@ -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 @
|
||||
|
@ -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)
|
||||
|
@ -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.
|
||||
|
@ -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))
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user