GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-21 10:58:01 +03:00
Code Issues Projects Releases Wiki Activity

Allow cryptol implementation of foreign functions

Browse Source
This commit is contained in:
Bretton 2023-08-21 10:46:49 -07:00
parent cd5d006277
commit 58a3b06796
20 changed files with 302 additions and 199 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
cryptol-remote-api/src/CryptolServer/Data/Expression.hs
View File

@ -518,7 +518,7 @@ getCryptolExpr (Let binds body) =
, CP.bExport = CP.Public
}) .
fakeLoc .
CP.DExpr <$>
CP.exprDef <$>
getCryptolExpr rhs
fakeLoc = Located emptyRange

6
src/Cryptol/Eval.hs
View File

@ -434,7 +434,7 @@ declHole sym d =
case dDefinition d of
DPrim -> evalPanic "Unexpected primitive declaration in recursive group"
[show (ppLocName nm)]
DForeign _ -> evalPanic "Unexpected foreign declaration in recursive group"
DForeign _ _ -> evalPanic "Unexpected foreign declaration in recursive group"
[show (ppLocName nm)]
DExpr _ -> do
(hole, fill) <- sDeclareHole sym msg
@ -470,7 +470,7 @@ evalDecl sym renv env d = do
Just (Left ex) -> bindVar sym (dName d) (evalExpr sym renv ex) env
Nothing -> bindVar sym (dName d) (cryNoPrimError sym (dName d)) env
DForeign _ -> do
DForeign _ _ -> do
-- Foreign declarations should have been handled by the previous
-- Cryptol.Eval.FFI.evalForeignDecls pass already, so they should already
-- be in the environment. If not, then either Cryptol was not compiled
@ -756,5 +756,5 @@ evalMatch sym (lsz, lenv) m = seq lsz $ case m of
f env =
case dDefinition d of
DPrim -> evalPanic "evalMatch" ["Unexpected local primitive"]
DForeign _ -> evalPanic "evalMatch" ["Unexpected local foreign"]
DForeign _ _ -> evalPanic "evalMatch" ["Unexpected local foreign"]
DExpr e -> evalExpr sym env e

2
src/Cryptol/Eval/Reference.lhs
View File

@ -532,7 +532,7 @@ the new bindings.
> evalDecl env d =
> case dDefinition d of
> DPrim -> (dName d, pure (evalPrim (dName d)))
> DForeign _ -> (dName d, cryError $ FFINotSupported $ dName d)
> DForeign _ _ -> (dName d, cryError $ FFINotSupported $ dName d)
> DExpr e -> (dName d, evalExpr env e)
>

2
src/Cryptol/IR/FreeVars.hs
View File

@ -93,7 +93,7 @@ instance FreeVars Decl where
instance FreeVars DeclDef where
freeVars d = case d of
DPrim -> mempty
DForeign _ -> mempty
DForeign _ me -> foldMap freeVars me
DExpr e -> freeVars e

2
src/Cryptol/IR/TraverseNames.hs
View File

@ -110,7 +110,7 @@ instance TraverseNames DeclDef where
traverseNamesIP d =
case d of
DPrim -> pure d
DForeign t -> DForeign <$> traverseNamesIP t
DForeign t me -> DForeign <$> traverseNamesIP t <*> traverseNamesIP me
DExpr e -> DExpr <$> traverseNamesIP e
instance TraverseNames Schema where

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

@ -1047,7 +1047,10 @@ instance Rename Bind where
instance Rename BindDef where
rename DPrim = return DPrim
rename DForeign = return DForeign
rename (DForeign i) = DForeign <$> traverse rename i
rename (DImpl i) = DImpl <$> rename i
instance Rename BindImpl where
rename (DExpr e) = DExpr <$> rename e
rename (DPropGuards cases) = DPropGuards <$> traverse rename cases

4
src/Cryptol/Parser.y
View File

@ -378,7 +378,7 @@ decl :: { Decl PName }
{ at ($1,$5) $
DBind $ Bind { bName = $2
, bParams = [$1,$3]
, bDef = at $5 (Located emptyRange (DExpr $5))
, bDef = at $5 (Located emptyRange (exprDef $5))
, bSignature = Nothing
, bPragmas = []
, bMono = False
@ -408,7 +408,7 @@ let_decl :: { Decl PName }
{ at ($2,$6) $
DBind $ Bind { bName = $3
, bParams = [$2,$4]
, bDef = at $6 (Located emptyRange (DExpr $6))
, bDef = at $6 (Located emptyRange (exprDef $6))
, bSignature = Nothing
, bPragmas = []
, bMono = False

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

@ -64,6 +64,7 @@ module Cryptol.Parser.AST
, PropSyn(..)
, Bind(..)
, BindDef(..), LBindDef
, BindImpl(..), bindImpl, exprDef
, Pragma(..)
, ExportType(..)
, TopLevel(..)
@ -486,11 +487,26 @@ data Bind name = Bind
type LBindDef = Located (BindDef PName)
data BindDef name = DPrim
| DForeign
| DExpr (Expr name)
-- | Foreign functions can have an optional cryptol
-- implementation
| DForeign (Maybe (BindImpl name))
| DImpl (BindImpl name)
deriving (Eq, Show, Generic, NFData, Functor)
bindImpl :: Bind name -> Maybe (BindImpl name)
bindImpl bind =
case thing (bDef bind) of
DPrim -> Nothing
DForeign mi -> mi
DImpl i -> Just i
data BindImpl name = DExpr (Expr name)
| DPropGuards [PropGuardCase name]
deriving (Eq, Show, Generic, NFData, Functor)
exprDef :: Expr name -> BindDef name
exprDef = DImpl . DExpr
data PropGuardCase name = PropGuardCase
{ pgcProps :: [Located (Prop name)]
, pgcExpr :: Expr name
@ -1064,7 +1080,12 @@ instance (Show name, PPName name) => PP (Bind name) where
instance (Show name, PPName name) => PP (BindDef name) where
ppPrec _ DPrim = text "<primitive>"
ppPrec _ DForeign = text "<foreign>"
ppPrec p (DForeign mi) = case mi of
Just i -> "(foreign)" <+> ppPrec p i
Nothing -> "<foreign>"
ppPrec p (DImpl i) = ppPrec p i
instance (Show name, PPName name) => PP (BindImpl name) where
ppPrec p (DExpr e) = ppPrec p e
ppPrec _p (DPropGuards _guards) = text "propguards"

12
src/Cryptol/Parser/ExpandPropGuards.hs
View File

@ -76,7 +76,12 @@ expandDecl decl =
expandBind :: Bind PName -> ExpandPropGuardsM [Bind PName]
expandBind bind =
case thing (bDef bind) of
DPropGuards guards -> do
DImpl (DPropGuards guards) -> expand (DImpl . DPropGuards) guards
DForeign (Just (DPropGuards guards)) -> expand (DForeign . Just . DPropGuards) guards
_ -> pure [bind]
where
expand def guards = do
Forall params props t rng <-
case bSignature bind of
Just schema -> pure schema
@ -104,14 +109,13 @@ expandBind bind =
t rng),
-- keeps same location at original bind
-- i.e. "on top of" original bind
bDef = (bDef bind) {thing = DExpr e}
bDef = (bDef bind) {thing = exprDef e}
}
)
(guards', binds') <- unzip <$> mapM goGuard guards
pure $
bind {bDef = DPropGuards guards' <$ bDef bind} :
bind {bDef = def guards' <$ bDef bind} :
binds'
_ -> pure [bind]
patternToExpr :: Pattern PName -> Expr PName
patternToExpr (PVar locName) = EVar (thing locName)

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

@ -69,9 +69,12 @@ namesB b =
namesDef :: Ord name => BindDef name -> Set name
namesDef DPrim = Set.empty
namesDef DForeign = Set.empty
namesDef (DExpr e) = namesE e
namesDef (DPropGuards guards) = Set.unions (map (namesE . pgcExpr) guards)
namesDef (DForeign mi) = foldMap namesImpl mi
namesDef (DImpl i) = namesImpl i
namesImpl :: Ord name => BindImpl name -> Set name
namesImpl (DExpr e) = namesE e
namesImpl (DPropGuards guards) = Set.unions (map (namesE . pgcExpr) guards)
-- | The names used by an expression.
@ -191,9 +194,12 @@ tnamesB b = Set.unions [setS, setP, setE]
tnamesDef :: Ord name => BindDef name -> Set name
tnamesDef DPrim = Set.empty
tnamesDef DForeign = Set.empty
tnamesDef (DExpr e) = tnamesE e
tnamesDef (DPropGuards guards) = Set.unions (map tnamesPropGuardCase guards)
tnamesDef (DForeign mi) = foldMap tnamesImpl mi
tnamesDef (DImpl i) = tnamesImpl i
tnamesImpl :: Ord name => BindImpl name -> Set name
tnamesImpl (DExpr e) = tnamesE e
tnamesImpl (DPropGuards guards) = Set.unions (map tnamesPropGuardCase guards)
tnamesPropGuardCase :: Ord name => PropGuardCase name -> Set name
tnamesPropGuardCase c =

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

@ -9,7 +9,9 @@
-- The purpose of this module is to convert all patterns to variable
-- patterns. It also eliminates pattern bindings by de-sugaring them
-- into `Bind`. Furthermore, here we associate signatures, fixities,
-- and pragmas with the names to which they belong.
-- and pragmas with the names to which they belong. We also merge
-- empty 'DForeign' binds with their cryptol implementations, if they
-- exist.
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
@ -57,7 +59,7 @@ instance RemovePatterns (NestedModule PName) where
simpleBind :: Located PName -> Expr PName -> Bind PName
simpleBind x e = Bind { bName = x, bParams = []
, bDef = at e (Located emptyRange (DExpr e))
, bDef = at e (Located emptyRange (exprDef e))
, bSignature = Nothing, bPragmas = []
, bMono = True, bInfix = False, bFixity = Nothing
, bDoc = Nothing
@ -220,20 +222,25 @@ noMatchB b =
| otherwise -> panic "NoPat" [ "noMatchB: primitive with params"
, show b ]
DForeign
DForeign Nothing
| null (bParams b) -> return b
| otherwise -> panic "NoPat" [ "noMatchB: foreign with params"
, show b ]
DExpr e ->
do e' <- noPatFun (Just (thing (bName b))) 0 (bParams b) e
return b { bParams = [], bDef = DExpr e' <$ bDef b }
DForeign (Just i) -> noMatchI (DForeign . Just) i
DImpl i -> noMatchI DImpl i
where
noMatchI def i =
do i' <- case i of
DExpr e ->
DExpr <$> noPatFun (Just (thing (bName b))) 0 (bParams b) e
DPropGuards guards ->
do let nm = thing (bName b)
let nm = thing (bName b)
ps = bParams b
gs <- mapM (noPatPropGuardCase nm ps) guards
pure b { bParams = [], bDef = DPropGuards gs <$ bDef b }
in DPropGuards <$> mapM (noPatPropGuardCase nm ps) guards
pure b { bParams = [], bDef = def i' <$ bDef b }
noPatPropGuardCase ::
PName ->
@ -260,7 +267,7 @@ noMatchD decl =
let e2 = foldl ETyped e1 ts
return $ DBind Bind { bName = x
, bParams = []
, bDef = at e (Located emptyRange (DExpr e2))
, bDef = at e (Located emptyRange (exprDef e2))
, bSignature = Nothing
, bPragmas = []
, bMono = False
@ -285,6 +292,8 @@ noPatDs ds =
, annValueFs = fixes
, annTypeFs = fixes
, annDocs = Map.empty
-- There shouldn't be any foreigns at non-top-level
, annForeigns = Map.empty
}
(ds2, AnnotMap { .. }) <- runStateT amap (annotDs ds1)
@ -319,6 +328,7 @@ noPatTopDs tds =
, annValueFs = fixes
, annTypeFs = fixes
, annDocs = Map.fromListWith (++) $ concatMap toDocs $ decls tds
, annForeigns = Map.fromListWith (<>) $ concatMap toForeigns allDecls
}
(tds', AnnotMap { .. }) <- runStateT ann (annotTopDs desugared)
@ -362,12 +372,25 @@ noPatModule m =
--------------------------------------------------------------------------------
-- | For each binding name, does there exist an empty foreign bind, a normal
-- cryptol bind, or both.
data AnnForeign = OnlyForeign | OnlyImpl | BothForeignImpl
instance Semigroup AnnForeign where
OnlyForeign <> OnlyImpl = BothForeignImpl
OnlyImpl <> OnlyForeign = BothForeignImpl
_ <> BothForeignImpl = BothForeignImpl
BothForeignImpl <> _ = BothForeignImpl
OnlyForeign <> OnlyForeign = OnlyForeign
OnlyImpl <> OnlyImpl = OnlyImpl
data AnnotMap = AnnotMap
{ annPragmas :: Map.Map PName [Located Pragma ]
, annSigs :: Map.Map PName [Located (Schema PName)]
, annValueFs :: Map.Map PName [Located Fixity ]
, annTypeFs :: Map.Map PName [Located Fixity ]
, annDocs :: Map.Map PName [Located Text ]
, annForeigns :: Map.Map PName AnnForeign
}
type Annotates a = a -> StateT AnnotMap NoPatM a
@ -428,7 +451,7 @@ annotDs [] = return []
annotD :: Decl PName -> ExceptionT () (StateT AnnotMap NoPatM) (Decl PName)
annotD decl =
case decl of
DBind b -> DBind <$> lift (annotB b)
DBind b -> DBind <$> annotB b
DRec {} -> panic "annotD" [ "DRec" ]
DSignature {} -> raise ()
DFixity{} -> raise ()
@ -439,7 +462,10 @@ annotD decl =
DLocated d r -> (`DLocated` r) <$> annotD d
-- | Add pragma/signature annotations to a binding.
annotB :: Annotates (Bind PName)
-- Also perform de-duplication of empty 'DForeign' binds generated by the parser
-- if there exists a cryptol implementation.
-- The exception indicates which declarations are no longer needed.
annotB :: Bind PName -> ExceptionT () (StateT AnnotMap NoPatM) (Bind PName)
annotB Bind { .. } =
do AnnotMap { .. } <- get
let name = thing bName
@ -448,9 +474,17 @@ annotB Bind { .. } =
(thisSigs , ss') = Map.updateLookupWithKey remove name annSigs
(thisFixes , fs') = Map.updateLookupWithKey remove name annValueFs
(thisDocs , ds') = Map.updateLookupWithKey remove name annDocs
s <- lift $ checkSigs name $ jn thisSigs
f <- lift $ checkFixs name $ jn thisFixes
d <- lift $ checkDocs name $ jn thisDocs
thisForeign = Map.lookup name annForeigns
-- Compute the new def before updating the state, since we don't want to
-- consume the annotations if we are throwing away an empty foreign def.
def' <- case thisForeign of
Just BothForeignImpl
| DForeign _ <- thing bDef -> raise ()
| DImpl i <- thing bDef -> pure (DForeign (Just i) <$ bDef)
_ -> pure bDef
s <- lift $ lift $ checkSigs name $ jn thisSigs
f <- lift $ lift $ checkFixs name $ jn thisFixes
d <- lift $ lift $ checkDocs name $ jn thisDocs
set AnnotMap { annPragmas = ps'
, annSigs = ss'
, annValueFs = fs'
@ -458,6 +492,7 @@ annotB Bind { .. } =
, ..
}
return Bind { bSignature = s
, bDef = def'
, bPragmas = map thing (jn thisPs) ++ bPragmas
, bFixity = f
, bDoc = d
@ -551,6 +586,13 @@ toDocs TopLevel { .. }
DType _ -> []
DProp _ -> []
-- | Is this declaration a foreign or regular bind?
toForeigns :: Decl PName -> [(PName, AnnForeign)]
toForeigns (DLocated d _) = toForeigns d
toForeigns (DBind Bind {..})
| DForeign Nothing <- thing bDef = [ (thing bName, OnlyForeign) ]
| DImpl _ <- thing bDef = [ (thing bName, OnlyImpl) ]
toForeigns _ = []
--------------------------------------------------------------------------------
newtype NoPatM a = M { unM :: ReaderT Range (StateT RW Id) a }

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

@ -692,7 +692,7 @@ mkProperty :: LPName -> [Pattern PName] -> Expr PName -> Decl PName
mkProperty f ps e = at (f,e) $
DBind Bind { bName = f
, bParams = reverse ps
, bDef = at e (Located emptyRange (DExpr e))
, bDef = at e (Located emptyRange (exprDef e))
, bSignature = Nothing
, bPragmas = [PragmaProperty]
, bMono = False
@ -708,7 +708,7 @@ mkIndexedDecl ::
mkIndexedDecl f (ps, ixs) e =
DBind Bind { bName = f
, bParams = reverse ps
, bDef = at e (Located emptyRange (DExpr rhs))
, bDef = at e (Located emptyRange (exprDef rhs))
, bSignature = Nothing
, bPragmas = []
, bMono = False
@ -735,7 +735,7 @@ mkPropGuardsDecl f (ps, ixs) guards =
pure $
DBind Bind { bName = f
, bParams = reverse ps
, bDef = Located (srcRange f) (DPropGuards gs)
, bDef = Located (srcRange f) (DImpl (DPropGuards gs))
, bSignature = Nothing
, bPragmas = []
, bMono = False
@ -777,7 +777,11 @@ mkForeignDecl mbDoc nm ty =
[ "`" ++ txt ++ "` is not a valid foreign name."
, "The name should contain only alpha-numeric characters or '_'."
])
pure (mkNoImplDecl DForeign mbDoc nm ty)
-- We do allow optional cryptol implementations of foreign functions, these
-- will be merged with this binding in the NoPat pass. In the parser they
-- are just treated as a completely separate (non-foreign) binding with the
-- same name.
pure (mkNoImplDecl (DForeign Nothing) mbDoc nm ty)
where
isOk c = c == '_' || isAlphaNum c
@ -791,7 +795,7 @@ mkForeignDecl mbDoc nm ty =
mkNoImplDecl :: BindDef PName
-> Maybe (Located Text) -> LPName -> Schema PName -> [TopDecl PName]
mkNoImplDecl def mbDoc ln sig =
[ exportDecl mbDoc Public
[ exportDecl Nothing Public
$ DBind Bind { bName = ln
, bParams = []
, bDef = at sig (Located emptyRange def)
@ -803,7 +807,7 @@ mkNoImplDecl def mbDoc ln sig =
, bDoc = Nothing
, bExport = Public
}
, exportDecl Nothing Public
, exportDecl mbDoc Public
$ DSignature [ln] sig
]

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

@ -220,7 +220,7 @@ rewD rews d = do e <- rewDef rews (dDefinition d)
rewDef :: RewMap -> DeclDef -> M DeclDef
rewDef rews (DExpr e) = DExpr <$> rewE rews e
rewDef _ DPrim = return DPrim
rewDef _ (DForeign t) = return $ DForeign t
rewDef rews (DForeign t me) = DForeign t <$> traverse (rewE rews) me
rewDeclGroup :: RewMap -> DeclGroup -> M DeclGroup
rewDeclGroup rews dg =
@ -241,8 +241,13 @@ rewDeclGroup rews dg =
consider d =
case dDefinition d of
DPrim -> Left d
DForeign _ -> Left d
DExpr e -> let (tps,props,e') = splitTParams e
DForeign _ me -> case me of
Nothing -> Left d
Just e -> conExpr e
DExpr e -> conExpr e
where
conExpr e =
let (tps,props,e') = splitTParams e
in if not (null tps) && notFun e'
then Right (d, tps, props, e')
else Left d

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

@ -201,11 +201,11 @@ 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)
let spec e = specializeExpr =<< instantiateExpr ts n e
rhs' <- case dDefinition decl of
DExpr e -> do e' <- specializeExpr =<< instantiateExpr ts n e
return (DExpr e')
DExpr e -> DExpr <$> spec e
DPrim -> return DPrim
DForeign t -> return $ DForeign t
DForeign t me -> DForeign t <$> traverse spec me
let decl' = decl { dName = qname', dSignature = sig', dDefinition = rhs' }
modifySpecCache (Map.adjust (fmap (insertTM ts (qname', Just decl'))) qname)
return (EVar qname')

2
src/Cryptol/TypeCheck.hs
View File

@ -86,7 +86,7 @@ tcExpr e0 inp = runInferM inp
[ P.Bind
{ P.bName = P.Located { P.srcRange = loc, P.thing = fresh }
, P.bParams = []
, P.bDef = P.Located (inpRange inp) (P.DExpr expr)
, P.bDef = P.Located (inpRange inp) (P.exprDef expr)
, P.bPragmas = []
, P.bSignature = Nothing
, P.bMono = False

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

@ -146,7 +146,7 @@ emptyModule nm =
-- | Find all the foreign declarations in the module and return their names and FFIFunTypes.
findForeignDecls :: ModuleG mname -> [(Name, FFIFunType)]
findForeignDecls = mapMaybe getForeign . mDecls
where getForeign (NonRecursive Decl { dName, dDefinition = DForeign ffiType })
where getForeign (NonRecursive Decl { dName, dDefinition = DForeign ffiType _ })
= Just (dName, ffiType)
-- Recursive DeclGroups can't have foreign decls
getForeign _ = Nothing
@ -245,7 +245,9 @@ data Decl = Decl { dName :: !Name
} deriving (Generic, NFData, Show)
data DeclDef = DPrim
| DForeign FFIFunType
-- | Foreign functions can have an optional cryptol
-- implementation
| DForeign FFIFunType (Maybe Expr)
| DExpr Expr
deriving (Show, Generic, NFData)
@ -464,7 +466,10 @@ instance PP (WithNames Decl) where
instance PP (WithNames DeclDef) where
ppPrec _ (WithNames DPrim _) = text "<primitive>"
ppPrec _ (WithNames (DForeign _) _) = text "<foreign>"
ppPrec _ (WithNames (DForeign _ me) nm) =
case me of
Just e -> text "(foreign)" <+> ppWithNames nm e
Nothing -> text "<foreign>"
ppPrec _ (WithNames (DExpr e) nm) = ppWithNames nm e
instance PP Decl where

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

@ -873,8 +873,8 @@ checkNumericConstraintGuardsOK isTopLevel haveSig noSig =
-- so no need to look at noSig
hasConstraintGuards b =
case thing (P.bDef b) of
P.DPropGuards {} -> True
case P.bindImpl b of
Just (P.DPropGuards {}) -> True
_ -> False
@ -898,6 +898,7 @@ guessType exprMap b@(P.Bind { .. }) =
do let wildOk = case thing bDef of
P.DForeign {} -> NoWildCards
P.DPrim -> NoWildCards
P.DImpl i -> case i of
P.DExpr {} -> AllowWildCards
P.DPropGuards {} -> NoWildCards
s1 <- checkSchema wildOk s
@ -996,7 +997,7 @@ generalize bs0 gs0 =
genB d = d { dDefinition = case dDefinition d of
DExpr e -> DExpr (genE e)
DPrim -> DPrim
DForeign t -> DForeign t
DForeign t me -> DForeign t (genE <$> me)
, dSignature = Forall asPs qs
$ apSubst su $ sType $ dSignature d
}
@ -1018,7 +1019,10 @@ checkMonoB b t =
P.DPrim -> panic "checkMonoB" ["Primitive with no signature?"]
P.DForeign -> panic "checkMonoB" ["Foreign with no signature?"]
P.DForeign _ -> panic "checkMonoB" ["Foreign with no signature?"]
P.DImpl i ->
case i of
P.DExpr e ->
do let nm = thing (P.bName b)
@ -1042,7 +1046,6 @@ checkMonoB b t =
-- XXX: Do we really need to do the defaulting business in two different places?
checkSigB :: P.Bind Name -> (Schema,[Goal]) -> InferM Decl
checkSigB b (Forall as asmps0 t0, validSchema) =
let name = thing (P.bName b) in
case thing (P.bDef b) of
-- XXX what should we do with validSchema in this case?
@ -1057,10 +1060,13 @@ checkSigB b (Forall as asmps0 t0, validSchema) =
, dDoc = P.bDoc b
}
P.DForeign -> do
P.DForeign mi -> do
(asmps, t, me) <-
case mi of
Just i -> fmap Just <$> checkImpl i
Nothing -> pure (asmps0, t0, Nothing)
let loc = getLoc b
name' = thing $ P.bName b
src = DefinitionOf name'
src = DefinitionOf name
inRangeMb loc do
-- Ensure all type params are of kind #
forM_ as \a ->
@ -1068,10 +1074,10 @@ checkSigB b (Forall as asmps0 t0, validSchema) =
recordErrorLoc loc $ UnsupportedFFIKind src a $ tpKind a
withTParams as do
ffiFunType <-
case toFFIFunType (Forall as asmps0 t0) of
case toFFIFunType (Forall as asmps t) of
Right (props, ffiFunType) -> ffiFunType <$ do
ffiGoals <- traverse (newGoal (CtFFI name')) props
proveImplication True (Just name') as asmps0 $
ffiGoals <- traverse (newGoal (CtFFI name)) props
proveImplication True (Just name) as asmps $
validSchema ++ ffiGoals
Left err -> do
recordErrorLoc loc $ UnsupportedFFIType src err
@ -1080,32 +1086,44 @@ checkSigB b (Forall as asmps0 t0, validSchema) =
{ ffiTParams = as, ffiArgTypes = []
, ffiRetType = FFITuple [] }
pure Decl { dName = thing (P.bName b)
, dSignature = Forall as asmps0 t0
, dDefinition = DForeign ffiFunType
, dSignature = Forall as asmps t
, dDefinition = DForeign ffiFunType me
, dPragmas = P.bPragmas b
, dInfix = P.bInfix b
, dFixity = P.bFixity b
, dDoc = P.bDoc b
}
P.DExpr e0 ->
inRangeMb (getLoc b) $
withTParams as $ do
(t, asmps, e2) <- checkBindDefExpr [] asmps0 e0
P.DImpl i -> do
(asmps, t, expr) <- checkImpl i
return Decl
{ dName = name
, dSignature = Forall as asmps t
, dDefinition = DExpr (foldr ETAbs (foldr EProofAbs e2 asmps) as)
, dDefinition = DExpr expr
, dPragmas = P.bPragmas b
, dInfix = P.bInfix b
, dFixity = P.bFixity b
, dDoc = P.bDoc b
}
P.DPropGuards cases0 ->
where
name = thing (P.bName b)
checkImpl :: P.BindImpl Name -> InferM ([Prop], Type, Expr)
checkImpl i =
inRangeMb (getLoc b) $
withTParams as $ do
withTParams as $
case i of
P.DExpr e0 -> do
(t, asmps, e2) <- checkBindDefExpr [] asmps0 e0
pure ( asmps
, t
, foldr ETAbs (foldr EProofAbs e2 asmps) as
)
P.DPropGuards cases0 -> do
asmps1 <- applySubstPreds asmps0
t1 <- applySubst t0
cases1 <- mapM checkPropGuardCase cases0
@ -1116,25 +1134,14 @@ checkSigB b (Forall as asmps0 t0, validSchema) =
-- necessarily hold
recordWarning (NonExhaustivePropGuards name)
let schema = Forall as asmps1 t1
return Decl
{ dName = name
, dSignature = schema
, dDefinition = DExpr
(foldr ETAbs
pure ( asmps1
, t1
, foldr ETAbs
(foldr EProofAbs
(EPropGuards cases1 t1)
asmps1)
as)
, dPragmas = P.bPragmas b
, dInfix = P.bInfix b
, dFixity = P.bFixity b
, dDoc = P.bDoc b
}
where
as
)
checkBindDefExpr ::
[Prop] -> [Prop] -> P.Expr Name -> InferM (Type, [Prop], Expr)

3
src/Cryptol/TypeCheck/Parseable.hs
View File

@ -95,7 +95,8 @@ instance ShowParseable Decl where
instance ShowParseable DeclDef where
showParseable DPrim = text (show DPrim)
showParseable (DForeign t) = text (show $ DForeign t)
showParseable (DForeign t me) =
parens (text "DForeign" $$ parens (text (show t)) $$ showParseable me)
showParseable (DExpr e) = parens (text "DExpr" $$ showParseable e)
instance ShowParseable DeclGroup where

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

@ -462,21 +462,26 @@ checkDecl checkSig d =
do when checkSig $ checkSchema $ dSignature d
return (dName d, dSignature d)
DForeign _ ->
DForeign _ me ->
do when checkSig $ checkSchema $ dSignature d
mapM_ checkExpr me
return (dName d, dSignature d)
DExpr e ->
do let s = dSignature d
when checkSig $ checkSchema s
checkExpr e
return (dName d, s)
where
checkExpr e =
do let s = dSignature d
s1 <- exprSchema e
let nm = dName d
loc = "definition of " ++ show (pp nm) ++
", at " ++ show (pp (nameLoc nm))
sameSchemas loc s s1
return (dName d, s)
checkDeclGroup :: DeclGroup -> TcM [(Name, Schema)]
checkDeclGroup dg =
case dg of

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

@ -454,7 +454,7 @@ instance TVars Decl where
instance TVars DeclDef where
apSubst su (DExpr e) = DExpr !$ (apSubst su e)
apSubst _ DPrim = DPrim
apSubst _ (DForeign t) = DForeign t
apSubst su (DForeign t me) = DForeign t !$ apSubst su me
-- WARNING: This applies the substitution only to the declarations.
instance TVars (ModuleG names) where