From b1bbd41f8382baf9e4ba9f88c2fcd8cd7cdad698 Mon Sep 17 00:00:00 2001 From: Trevor Elliott Date: Wed, 3 Jun 2015 18:56:43 -0700 Subject: [PATCH] Plumb through primitive declarations --- src/Cryptol/Eval.hs | 6 ++- src/Cryptol/ModuleSystem/Renamer.hs | 4 ++ src/Cryptol/Parser.y | 42 +++++++++++++++--- src/Cryptol/Parser/AST.hs | 16 ++++++- src/Cryptol/Parser/Lexer.x | 2 + src/Cryptol/Parser/LexerUtils.hs | 1 + src/Cryptol/Parser/Names.hs | 13 +++++- src/Cryptol/Parser/NoPat.hs | 20 ++++++--- src/Cryptol/Parser/ParserUtils.hs | 2 +- src/Cryptol/REPL/Command.hs | 2 +- src/Cryptol/Symbolic.hs | 7 ++- src/Cryptol/Transform/MonoValues.hs | 21 ++++++--- src/Cryptol/Transform/Specialize.hs | 5 ++- src/Cryptol/TypeCheck.hs | 10 ++++- src/Cryptol/TypeCheck/AST.hs | 10 ++++- src/Cryptol/TypeCheck/Infer.hs | 67 ++++++++++++++++++++++------- src/Cryptol/TypeCheck/Sanity.hs | 19 +++++--- src/Cryptol/TypeCheck/Subst.hs | 4 ++ 18 files changed, 198 insertions(+), 53 deletions(-) diff --git a/src/Cryptol/Eval.hs b/src/Cryptol/Eval.hs index 4e36decf..d00060e7 100644 --- a/src/Cryptol/Eval.hs +++ b/src/Cryptol/Eval.hs @@ -123,7 +123,11 @@ evalDeclGroup dg env = env' NonRecursive d -> evalDecl env d env evalDecl :: ReadEnv -> Decl -> EvalEnv -> EvalEnv -evalDecl renv d = bindVar (dName d) (evalExpr renv (dDefinition d)) +evalDecl renv d = bindVar (dName d) (evalDef renv (dDefinition d)) + +evalDef :: ReadEnv -> DeclDef -> Value +evalDef renv (DExpr e) = evalExpr renv e +evalDef _ DPrim = panic "Eval" [ "unimplemented primitive" ] -- Selectors ------------------------------------------------------------------- diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index ec93d279..13794abd 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -419,6 +419,10 @@ instance Rename Bind where , bPragmas = p' } +instance Rename BindDef where + rename DPrim = return DPrim + rename (DExpr e) = DExpr <$> rename e + -- NOTE: this only renames types within the pattern. instance Rename Pattern where rename p = case p of diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y index ff5a16a1..0c5272d3 100644 --- a/src/Cryptol/Parser.y +++ b/src/Cryptol/Parser.y @@ -70,6 +70,8 @@ import Paths_cryptol 'max' { Located $$ (Token (KW KW_max ) _)} 'x' { Located $$ (Token (KW KW_x) _)} + 'primitive' { Located $$ (Token (KW KW_primitive) _)} + '[' { Located $$ (Token (Sym BracketL) _)} ']' { Located $$ (Token (Sym BracketR) _)} '<-' { Located $$ (Token (Sym ArrL ) _)} @@ -236,10 +238,35 @@ vtop_decl :: { [TopDecl] } | 'property' name apats '=' expr { [exportDecl Public (mkProperty $2 $3 $5)]} | 'property' name '=' expr { [exportDecl Public (mkProperty $2 [] $4)]} | newtype { [exportNewtype Public $1] } + | 'primitive' prim_bind { [exportDecl Public $ at ($1,$2) $ DBind $2]} top_decl :: { TopDecl } : decl { Decl (TopLevel {tlExport = Public, tlValue = $1}) } | 'include' STRLIT {% Include `fmap` fromStrLit $2 } + | 'primitive' prim_bind { exportDecl Public $ at ($1,$2) $ DBind $2 } + +prim_bind :: { Bind } + : name ':' schema { Bind { bName = fmap mkUnqual $1 + , bParams = [] + , bDef = at $3 (Located emptyRange DPrim) + , bSignature = Just $3 + , bPragmas = [] + , bMono = False + , bInfix = False + , bFixity = Nothing + } } + + | '(' op ')' ':' schema { Bind { bName = $2 + , bParams = [] + , bDef = at $5 (Located emptyRange DPrim) + , bSignature = Just $5 + , bPragmas = [] + , bMono = False + , bInfix = True + , bFixity = Nothing + } } + + decl :: { Decl } : vars_comma ':' schema { at (head $1,$3) $ DSignature (map (fmap mkUnqual) (reverse $1)) $3 } @@ -247,7 +274,7 @@ decl :: { Decl } | name apats '=' expr { at ($1,$4) $ DBind $ Bind { bName = fmap mkUnqual $1 , bParams = reverse $2 - , bDef = $4 + , bDef = at $4 (Located emptyRange (DExpr $4)) , bSignature = Nothing , bPragmas = [] , bMono = False @@ -258,7 +285,7 @@ decl :: { Decl } | apat op apat '=' expr { at ($1,$5) $ DBind $ Bind { bName = $2 , bParams = [$1,$3] - , bDef = $5 + , bDef = at $5 (Located emptyRange (DExpr $5)) , bSignature = Nothing , bPragmas = [] , bMono = False @@ -279,7 +306,7 @@ let_decl :: { Decl } | 'let' name apats '=' expr { at ($2,$5) $ DBind $ Bind { bName = fmap mkUnqual $2 , bParams = reverse $3 - , bDef = $5 + , bDef = at $5 (Located emptyRange (DExpr $5)) , bSignature = Nothing , bPragmas = [] , bMono = False @@ -298,11 +325,12 @@ newtype_body :: { [Named Type] } | '{' field_types '}' { $2 } vars_comma :: { [ LName ] } - : name { [ $1] } - | vars_comma ',' name { $3 : $1 } + : var { [ $1] } + | vars_comma ',' var { $3 : $1 } - | '(' op ')' { [fmap unqual $2] } - | vars_comma ',' '(' op ')' { fmap unqual $4 : $1 } +var :: { LName } + : name { $1 } + | '(' op ')' { fmap unqual $2 } apats :: { [Pattern] } : apat { [$1] } diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index 7cec0d47..9b3fe04a 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -33,6 +33,7 @@ module Cryptol.Parser.AST , Fixity(..), defaultFixity , TySyn(..) , Bind(..) + , BindDef(..), LBindDef , Pragma(..) , ExportType(..) , ExportSpec(..), exportBind, exportType @@ -152,7 +153,7 @@ data TySyn = TySyn LQName [TParam] Type -} data Bind = Bind { bName :: LQName -- ^ Defined thing , bParams :: [Pattern] -- ^ Parameters - , bDef :: Expr -- ^ Definition + , bDef :: LBindDef -- ^ Definition , bSignature :: Maybe Schema -- ^ Optional type sig , bInfix :: Bool -- ^ Infix operator? , bFixity :: Maybe Fixity -- ^ Optional fixity info @@ -160,6 +161,12 @@ data Bind = Bind { bName :: LQName -- ^ Defined thing , bMono :: Bool -- ^ Is this a monomorphic binding } deriving (Eq,Show) +type LBindDef = Located BindDef + +data BindDef = DPrim + | DExpr Expr + deriving (Eq,Show) + data Fixity = Fixity { fAssoc :: !Assoc , fLevel :: !Int } deriving (Eq,Show) @@ -533,7 +540,7 @@ ppPragma xs p = instance PP Bind where ppPrec _ b = sig $$ vcat [ ppPragma [f] p | p <- bPragmas b ] $$ - hang (def <+> eq) 4 (pp (bDef b)) + hang (def <+> eq) 4 (pp (thing (bDef b))) where def | bInfix b = lhsOp | otherwise = lhs f = bName b @@ -548,6 +555,11 @@ instance PP Bind where _ -> panic "AST" [ "Malformed infix operator", show b ] +instance PP BindDef where + ppPrec _ DPrim = text "" + ppPrec p (DExpr e) = ppPrec p e + + instance PP TySyn where ppPrec _ (TySyn x xs t) = text "type" <+> ppL x <+> fsep (map (ppPrec 1) xs) <+> text "=" <+> pp t diff --git a/src/Cryptol/Parser/Lexer.x b/src/Cryptol/Parser/Lexer.x index 7d722525..2ab07336 100644 --- a/src/Cryptol/Parser/Lexer.x +++ b/src/Cryptol/Parser/Lexer.x @@ -108,6 +108,8 @@ $white+ { emit $ White Space } "infixr" { emit $ KW KW_infixr } "infix" { emit $ KW KW_infix } +"primitive" { emit $ KW KW_primitive } + @num2 { emitS (numToken 2 . drop 2) } @num8 { emitS (numToken 8 . drop 2) } @num10 { emitS (numToken 10 . drop 0) } diff --git a/src/Cryptol/Parser/LexerUtils.hs b/src/Cryptol/Parser/LexerUtils.hs index ccf05d7b..f8ab5b84 100644 --- a/src/Cryptol/Parser/LexerUtils.hs +++ b/src/Cryptol/Parser/LexerUtils.hs @@ -342,6 +342,7 @@ data TokenKW = KW_Arith | KW_infixl | KW_infixr | KW_infix + | KW_primitive deriving (Eq,Show) -- | The named operators are a special case for parsing types, and 'Other' is diff --git a/src/Cryptol/Parser/Names.hs b/src/Cryptol/Parser/Names.hs index e0b38516..048d4d6d 100644 --- a/src/Cryptol/Parser/Names.hs +++ b/src/Cryptol/Parser/Names.hs @@ -71,7 +71,12 @@ tsName (TySyn lqn _ _) = lqn -- | The names defined and used by a single binding. namesB :: Bind -> ([Located QName], Set QName) -namesB b = ([bName b], boundNames (namesPs (bParams b)) (namesE (bDef b))) +namesB b = ([bName b], boundNames (namesPs (bParams b)) (namesDef (thing (bDef b)))) + + +namesDef :: BindDef -> Set QName +namesDef DPrim = Set.empty +namesDef (DExpr e) = namesE e -- | The names used by an expression. @@ -186,7 +191,11 @@ tnamesB b = Set.unions [setS, setP, setE] where setS = maybe Set.empty tnamesS (bSignature b) setP = Set.unions (map tnamesP (bParams b)) - setE = tnamesE (bDef b) + setE = tnamesDef (thing (bDef b)) + +tnamesDef :: BindDef -> Set QName +tnamesDef DPrim = Set.empty +tnamesDef (DExpr e) = tnamesE e -- | The type names used by an expression. tnamesE :: Expr -> Set QName diff --git a/src/Cryptol/Parser/NoPat.hs b/src/Cryptol/Parser/NoPat.hs index 4905c28b..2f4d66c1 100644 --- a/src/Cryptol/Parser/NoPat.hs +++ b/src/Cryptol/Parser/NoPat.hs @@ -16,7 +16,7 @@ module Cryptol.Parser.NoPat (RemovePatterns(..),Error(..)) where import Cryptol.Prims.Syntax import Cryptol.Parser.AST -import Cryptol.Parser.Position(Range(..),start) +import Cryptol.Parser.Position(Range(..),emptyRange,start,at) import Cryptol.Utils.PP import Cryptol.Utils.Panic(panic) @@ -26,7 +26,7 @@ import Data.Either(partitionEithers) import qualified Data.Map as Map #if __GLASGOW_HASKELL__ < 710 -import Control.Applicative(Applicative(..),(<$>)) +import Control.Applicative(Applicative(..),(<$>)(<$)) import Data.Traversable(traverse) #endif @@ -47,7 +47,8 @@ instance RemovePatterns [Decl] where removePatterns ds = runNoPatM (noPatDs ds) simpleBind :: Located QName -> Expr -> Bind -simpleBind x e = Bind { bName = x, bParams = [], bDef = e +simpleBind x e = Bind { bName = x, bParams = [] + , bDef = at e (Located emptyRange (DExpr e)) , bSignature = Nothing, bPragmas = [] , bMono = True, bInfix = False, bFixity = Nothing } @@ -190,8 +191,15 @@ noPatM (MatchLet b) = (return . MatchLet) <$> noMatchB b noMatchB :: Bind -> NoPatM Bind noMatchB b = - do (ps,e) <- noPatFun (bParams b) (bDef b) - return b { bParams = ps, bDef = e } + case thing (bDef b) of + + DPrim | null (bParams b) -> return b + | otherwise -> panic "NoPat" [ "noMatchB: primitive with params" + , show b ] + + DExpr e -> + do (ps,e') <- noPatFun (bParams b) e + return b { bParams = ps, bDef = DExpr e' <$ bDef b } noMatchD :: Decl -> NoPatM [Decl] noMatchD decl = @@ -209,7 +217,7 @@ noMatchD decl = let e2 = foldl ETyped e1 ts return $ DBind Bind { bName = x , bParams = [] - , bDef = e2 + , bDef = at e (Located emptyRange (DExpr e2)) , bSignature = Nothing , bPragmas = [] , bMono = False diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs index c8dd80e7..5602f0d2 100644 --- a/src/Cryptol/Parser/ParserUtils.hs +++ b/src/Cryptol/Parser/ParserUtils.hs @@ -319,7 +319,7 @@ mkPoly rng terms = mk 0 (map fromInteger bits) mkProperty :: LName -> [Pattern] -> Expr -> Decl mkProperty f ps e = DBind Bind { bName = fmap mkUnqual f , bParams = reverse ps - , bDef = ETyped e TBit + , bDef = at e (Located emptyRange (DExpr (ETyped e TBit))) , bSignature = Nothing , bPragmas = [PragmaProperty] , bMono = False diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index e9173c8a..b1caca01 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -781,7 +781,7 @@ bindItVariable ty expr = do } decl = T.Decl { T.dName = freshIt , T.dSignature = schema - , T.dDefinition = expr + , T.dDefinition = T.DExpr expr , T.dPragmas = [] , T.dInfix = False , T.dFixity = Nothing diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs index 1f22e0b5..e134da76 100644 --- a/src/Cryptol/Symbolic.hs +++ b/src/Cryptol/Symbolic.hs @@ -398,7 +398,12 @@ evalDeclGroup env dg = in env' evalDecl :: Env -> Decl -> (QName, Value) -evalDecl env d = (dName d, evalExpr env (dDefinition d)) +evalDecl env d = (dName d, evalDeclDef env (dDefinition d)) + +evalDeclDef :: Env -> DeclDef -> Value +evalDeclDef env (DExpr e) = evalExpr env e +evalDeclDef _ DPrim = panic "Cryptol.Symbolic.evalDeclDef" + [ "Unimplemented primitive" ] -- | Make a copy of the given value, building the spine based only on -- the type without forcing the value argument. This lets us avoid diff --git a/src/Cryptol/Transform/MonoValues.hs b/src/Cryptol/Transform/MonoValues.hs index fcbc8926..3e711b9c 100644 --- a/src/Cryptol/Transform/MonoValues.hs +++ b/src/Cryptol/Transform/MonoValues.hs @@ -212,9 +212,13 @@ rewM rews ma = rewD :: RewMap -> Decl -> M Decl -rewD rews d = do e <- rewE rews (dDefinition d) +rewD rews d = do e <- rewDef rews (dDefinition d) return d { dDefinition = e } +rewDef :: RewMap -> DeclDef -> M DeclDef +rewDef rews (DExpr e) = DExpr <$> rewE rews e +rewDef _ DPrim = return DPrim + rewDeclGroup :: RewMap -> DeclGroup -> M DeclGroup rewDeclGroup rews dg = case dg of @@ -231,9 +235,12 @@ rewDeclGroup rews dg = sameTParams (_,tps1,x,_) (_,tps2,y,_) = tps1 == tps2 && x == y compareTParams (_,tps1,x,_) (_,tps2,y,_) = compare (x,tps1) (y,tps2) - consider d = let (tps,props,e) = splitTParams (dDefinition d) - in if not (null tps) && notFun e - then Right (d, tps, props, e) + consider d = + case dDefinition d of + DPrim -> Left d + DExpr e -> let (tps,props,e') = splitTParams e + in if not (null tps) && notFun e' + then Right (d, tps, props, e') else Left d rewSame ds = @@ -252,7 +259,7 @@ rewDeclGroup rews dg = , d { dName = newN , dSignature = (dSignature d) { sVars = [], sProps = [] } - , dDefinition = e1 + , dDefinition = DExpr e1 } ) @@ -262,7 +269,7 @@ rewDeclGroup rews dg = let newBody = EVar (dName f') newE = EWhere newBody [ Recursive [f'] ] - in foldr ETAbs + in DExpr $ foldr ETAbs (foldr EProofAbs newE props) tps } ] @@ -285,6 +292,7 @@ rewDeclGroup rews dg = (map (sType . dSignature) monoDs) , dDefinition = + DExpr $ addTPs $ EWhere (ETuple [ EVar (dName d) | d <- monoDs ]) [ Recursive monoDs ] @@ -301,6 +309,7 @@ rewDeclGroup rews dg = mkFunDef n f = f { dDefinition = + DExpr $ addTPs $ ESel ( flip (foldl mkProof) props $ flip (foldl ETApp) tys $ EVar tupName diff --git a/src/Cryptol/Transform/Specialize.hs b/src/Cryptol/Transform/Specialize.hs index 04399138..d15df73e 100644 --- a/src/Cryptol/Transform/Specialize.hs +++ b/src/Cryptol/Transform/Specialize.hs @@ -187,7 +187,10 @@ specializeConst e0 = do qname' <- freshName qname ts -- New type instance, record new name sig' <- instantiateSchema ts n (dSignature decl) modifySpecCache (Map.adjust (fmap (insertTM ts (qname', Nothing))) qname) - rhs' <- specializeExpr =<< instantiateExpr ts n (dDefinition decl) + rhs' <- case dDefinition decl of + DExpr e -> do e' <- specializeExpr =<< instantiateExpr ts n e + return (DExpr e') + DPrim -> return DPrim let decl' = decl { dName = qname', dSignature = sig', dDefinition = rhs' } modifySpecCache (Map.adjust (fmap (insertTM ts (qname', Just decl'))) qname) return (EVar qname') diff --git a/src/Cryptol/TypeCheck.hs b/src/Cryptol/TypeCheck.hs index eccf2254..385f9556 100644 --- a/src/Cryptol/TypeCheck.hs +++ b/src/Cryptol/TypeCheck.hs @@ -5,6 +5,7 @@ -- Maintainer : cryptol@galois.com -- Stability : provisional -- Portability : portable +{-# LANGUAGE PatternGuards #-} module Cryptol.TypeCheck ( tcModule @@ -71,7 +72,7 @@ tcExpr e0 inp = runInferM inp { P.bName = P.Located (inpRange inp) $ mkUnqual (P.Name "(expression)") , P.bParams = [] - , P.bDef = expr + , P.bDef = P.Located (inpRange inp) (P.DExpr expr) , P.bPragmas = [] , P.bSignature = Nothing , P.bMono = False @@ -80,7 +81,12 @@ tcExpr e0 inp = runInferM inp } ] case res of - [d] -> return (dDefinition d, dSignature d) + [d] | DExpr e <- dDefinition d -> return (e, dSignature d) + | otherwise -> + panic "Cryptol.TypeCheck.tcExpr" + [ "Expected an expression in definition" + , show d ] + _ -> panic "Cryptol.TypeCheck.tcExpr" ( "Multiple declarations when check expression:" : map show res diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index 11dd9edf..4a9bca82 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -258,12 +258,16 @@ groupDecls dg = case dg of data Decl = Decl { dName :: QName , dSignature :: Schema - , dDefinition :: Expr + , dDefinition :: DeclDef , dPragmas :: [Pragma] , dInfix :: !Bool , dFixity :: Maybe Fixity } deriving (Show) +data DeclDef = DPrim + | DExpr Expr + deriving (Show) + -------------------------------------------------------------------------------- @@ -875,6 +879,10 @@ instance PP (WithNames Decl) where ) $$ pp dName <+> text "=" <+> ppWithNames nm dDefinition +instance PP (WithNames DeclDef) where + ppPrec _ (WithNames DPrim _) = text "" + ppPrec _ (WithNames (DExpr e) nm) = ppWithNames nm e + instance PP Decl where ppPrec = ppWithNamesPrec IntMap.empty diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index 83e78bed..58c236ef 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -567,7 +567,10 @@ inferCArm armNum (m : ms) = -- be unaffected. inferBinds :: Bool -> Bool -> [P.Bind] -> InferM [Decl] inferBinds isTopLevel isRec binds = - mdo let exprMap = Map.fromList [ (x,inst (EVar x) (dDefinition b)) + mdo let dExpr (DExpr e) = e + dExpr DPrim = panic "[TypeCheck]" [ "primitive in a recursive group" ] + + exprMap = Map.fromList [ (x,inst (EVar x) (dExpr (dDefinition b))) | b <- genBs, let x = dName b ] -- REC. inst e (ETAbs x e1) = inst (ETApp e (TVar (tpVar x))) e1 @@ -647,7 +650,9 @@ simpBind d = case simpTypeMaybe t of Nothing -> d Just t1 -> d { dSignature = Forall as qs t1 - , dDefinition = castUnder t1 (dDefinition d) + , dDefinition = case dDefinition d of + DPrim -> DPrim + DExpr e -> DExpr (castUnder t1 e) } where -- Assumes the quantifiers match @@ -715,7 +720,9 @@ generalize bs0 gs0 = qs = map (apSubst su) here genE e = foldr ETAbs (foldr EProofAbs (apSubst su e) qs) asPs - genB d = d { dDefinition = genE (dDefinition d) + genB d = d { dDefinition = case dDefinition d of + DExpr e -> DExpr (genE e) + DPrim -> DPrim , dSignature = Forall asPs qs $ apSubst su $ sType $ dSignature d } @@ -725,27 +732,55 @@ generalize bs0 gs0 = - checkMonoB :: P.Bind -> Type -> InferM Decl checkMonoB b t = inRangeMb (getLoc b) $ - do e1 <- checkFun (pp (thing (P.bName b))) (P.bParams b) (P.bDef b) t - let f = thing (P.bName b) - return Decl { dName = f - , dSignature = Forall [] [] t - , dDefinition = e1 - , dPragmas = P.bPragmas b - , dInfix = P.bInfix b - , dFixity = P.bFixity b - } + case thing (P.bDef b) of + + P.DPrim -> + return Decl { dName = thing (P.bName b) + , dSignature = Forall [] [] t + , dDefinition = DPrim + , dPragmas = P.bPragmas b + , dInfix = P.bInfix b + , dFixity = P.bFixity b + } + + P.DExpr e -> + do e1 <- checkFun (pp (thing (P.bName b))) (P.bParams b) e t + let f = thing (P.bName b) + return Decl { dName = f + , dSignature = Forall [] [] t + , dDefinition = DExpr e1 + , dPragmas = P.bPragmas b + , dInfix = P.bInfix b + , dFixity = P.bFixity b + } -- XXX: Do we really need to do the defaulting business in two different places? checkSigB :: P.Bind -> (Schema,[Goal]) -> InferM Decl -checkSigB b (Forall as asmps0 t0, validSchema) = +checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of + + -- XXX what should we do with validSchema in this case? + P.DPrim + | not (null validSchema) -> + return Decl + { dName = thing (P.bName b) + , dSignature = Forall as asmps0 t0 + , dDefinition = DPrim + , dPragmas = P.bPragmas b + , dInfix = P.bInfix b + , dFixity = P.bFixity b + } + + | otherwise -> + panic "[TypeCheck]" [ "invalid primitive schema", show b, show validSchema ] + + P.DExpr e0 -> inRangeMb (getLoc b) $ withTParams as $ do (e1,cs0) <- collectGoals $ - do e1 <- checkFun (pp (thing (P.bName b))) (P.bParams b) (P.bDef b) t0 + do e1 <- checkFun (pp (thing (P.bName b))) (P.bParams b) e0 t0 () <- simplifyAllConstraints -- XXX: using `asmps` also... return e1 cs <- applySubst cs0 @@ -792,7 +827,7 @@ checkSigB b (Forall as asmps0 t0, validSchema) = return Decl { dName = thing (P.bName b) , dSignature = Forall as asmps t - , dDefinition = foldr ETAbs (foldr EProofAbs e2 asmps) as + , dDefinition = DExpr (foldr ETAbs (foldr EProofAbs e2 asmps) as) , dPragmas = P.bPragmas b , dInfix = P.bInfix b , dFixity = P.bFixity b diff --git a/src/Cryptol/TypeCheck/Sanity.hs b/src/Cryptol/TypeCheck/Sanity.hs index 5b8ee71d..77dc3133 100644 --- a/src/Cryptol/TypeCheck/Sanity.hs +++ b/src/Cryptol/TypeCheck/Sanity.hs @@ -356,12 +356,19 @@ convertible t1 t2 = go t1 t2 -- | Check a declaration. The boolean indicates if we should check the siganture checkDecl :: Bool -> Decl -> TcM (QName, Schema) checkDecl checkSig d = - do let s = dSignature d - when checkSig $ checkSchema s - s1 <- exprSchema (dDefinition d) - unless (same s s1) $ - reportError $ TypeMismatch s s1 - return (dName d, s) + case dDefinition d of + + DPrim -> + do when checkSig $ checkSchema $ dSignature d + return (dName d, dSignature d) + + DExpr e -> + do let s = dSignature d + when checkSig $ checkSchema s + s1 <- exprSchema e + unless (same s s1) $ + reportError $ TypeMismatch s s1 + return (dName d, s) checkDeclGroup :: DeclGroup -> TcM [(QName, Schema)] checkDeclGroup dg = diff --git a/src/Cryptol/TypeCheck/Subst.hs b/src/Cryptol/TypeCheck/Subst.hs index f5c8d676..a983f7ec 100644 --- a/src/Cryptol/TypeCheck/Subst.hs +++ b/src/Cryptol/TypeCheck/Subst.hs @@ -236,6 +236,10 @@ instance TVars Decl where , dDefinition = apSubst su (dDefinition d) } +instance TVars DeclDef where + apSubst su (DExpr e) = DExpr (apSubst su e) + apSubst _ DPrim = DPrim + instance TVars Module where apSubst su m = m { mDecls = apSubst su (mDecls m) }