GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-17 21:11:35 +03:00
Code Issues Projects Releases Wiki Activity

Plumb through primitive declarations

Browse Source
This commit is contained in:
Trevor Elliott 2015-06-03 18:56:43 -07:00
parent e4258b4d2c
commit b1bbd41f83
18 changed files with 198 additions and 53 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/Cryptol/Eval.hs
View File

@ -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 -------------------------------------------------------------------

4
src/Cryptol/ModuleSystem/Renamer.hs
View File

@ -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

42
src/Cryptol/Parser.y
View File

@ -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] }

16
src/Cryptol/Parser/AST.hs
View File

@ -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 "<primitive>"
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

2
src/Cryptol/Parser/Lexer.x
View File

@ -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) }

1
src/Cryptol/Parser/LexerUtils.hs
View File

@ -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

13
src/Cryptol/Parser/Names.hs
View File

@ -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

20
src/Cryptol/Parser/NoPat.hs
View File

@ -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

2
src/Cryptol/Parser/ParserUtils.hs
View File

@ -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

2
src/Cryptol/REPL/Command.hs
View File

@ -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

7
src/Cryptol/Symbolic.hs
View File

@ -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

21
src/Cryptol/Transform/MonoValues.hs
View File

@ -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

5
src/Cryptol/Transform/Specialize.hs
View File

@ -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')

10
src/Cryptol/TypeCheck.hs
View File

@ -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

10
src/Cryptol/TypeCheck/AST.hs
View File

@ -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 "<primitive>"
ppPrec _ (WithNames (DExpr e) nm) = ppWithNames nm e
instance PP Decl where
ppPrec = ppWithNamesPrec IntMap.empty

67
src/Cryptol/TypeCheck/Infer.hs
View File

@ -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

19
src/Cryptol/TypeCheck/Sanity.hs
View File

@ -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 =

4
src/Cryptol/TypeCheck/Subst.hs
View File

@ -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) }