From 9bccc79d9b9a3a49f931a4110a6f0b8f3ed0778d Mon Sep 17 00:00:00 2001 From: Bretton Date: Fri, 24 Jun 2022 19:31:35 -0700 Subject: [PATCH] Add frontend for FFI --- src/Cryptol/Eval.hs | 15 ++++++---- src/Cryptol/Eval/Reference.lhs | 5 ++-- src/Cryptol/IR/FreeVars.hs | 1 + src/Cryptol/ModuleSystem/InstantiateModule.hs | 5 ++-- src/Cryptol/ModuleSystem/Renamer.hs | 1 + src/Cryptol/Parser.y | 4 +++ src/Cryptol/Parser/AST.hs | 2 ++ src/Cryptol/Parser/Lexer.x | 1 + src/Cryptol/Parser/Names.hs | 2 ++ src/Cryptol/Parser/NoPat.hs | 5 ++++ src/Cryptol/Parser/ParserUtils.hs | 23 ++++++++++----- src/Cryptol/Parser/Token.hs | 1 + src/Cryptol/Transform/AddModParams.hs | 12 ++++---- src/Cryptol/Transform/MonoValues.hs | 12 ++++---- src/Cryptol/Transform/Specialize.hs | 7 +++-- src/Cryptol/TypeCheck/AST.hs | 2 ++ src/Cryptol/TypeCheck/Error.hs | 25 +++++++++++++++- src/Cryptol/TypeCheck/Infer.hs | 29 +++++++++++++++++-- src/Cryptol/TypeCheck/Parseable.hs | 1 + src/Cryptol/TypeCheck/Sanity.hs | 4 +++ src/Cryptol/TypeCheck/Subst.hs | 1 + 21 files changed, 125 insertions(+), 33 deletions(-) diff --git a/src/Cryptol/Eval.hs b/src/Cryptol/Eval.hs index 874ecf5e1..963cff04c 100644 --- a/src/Cryptol/Eval.hs +++ b/src/Cryptol/Eval.hs @@ -382,9 +382,11 @@ declHole :: sym -> Decl -> SEval sym (Name, Schema, SEval sym (GenValue sym), SEval sym (GenValue sym) -> SEval sym ()) declHole sym d = case dDefinition d of - DPrim -> evalPanic "Unexpected primitive declaration in recursive group" - [show (ppLocName nm)] - DExpr _ -> do + DPrim -> evalPanic "Unexpected primitive declaration in recursive group" + [show (ppLocName nm)] + DForeign -> evalPanic "Unexpected foreign declaration in recursive group" + [show (ppLocName nm)] + DExpr _ -> do (hole, fill) <- sDeclareHole sym msg return (nm, sch, hole, fill) where @@ -416,6 +418,8 @@ evalDecl sym renv env d = Just (Left ex) -> bindVar sym (dName d) (evalExpr sym renv ex) env Nothing -> bindVar sym (dName d) (cryNoPrimError sym (dName d)) env + DForeign -> evalPanic "FFI unimplemented" [] + DExpr e -> bindVar sym (dName d) (evalExpr sym renv e) env @@ -689,5 +693,6 @@ evalMatch sym (lsz, lenv) m = seq lsz $ case m of where f env = case dDefinition d of - DPrim -> evalPanic "evalMatch" ["Unexpected local primitive"] - DExpr e -> evalExpr sym env e + DPrim -> evalPanic "evalMatch" ["Unexpected local primitive"] + DForeign -> evalPanic "evalMatch" ["Unexpected local foreign"] + DExpr e -> evalExpr sym env e diff --git a/src/Cryptol/Eval/Reference.lhs b/src/Cryptol/Eval/Reference.lhs index 19a53b068..196fa7944 100644 --- a/src/Cryptol/Eval/Reference.lhs +++ b/src/Cryptol/Eval/Reference.lhs @@ -510,8 +510,9 @@ the new bindings. > evalDecl :: Env -> Decl -> (Name, E Value) > evalDecl env d = > case dDefinition d of -> DPrim -> (dName d, pure (evalPrim (dName d))) -> DExpr e -> (dName d, evalExpr env e) +> DPrim -> (dName d, pure (evalPrim (dName d))) +> DForeign -> evalPanic "FFI unimplemented" [] +> DExpr e -> (dName d, evalExpr env e) > Newtypes diff --git a/src/Cryptol/IR/FreeVars.hs b/src/Cryptol/IR/FreeVars.hs index 9810af692..bb7a9deee 100644 --- a/src/Cryptol/IR/FreeVars.hs +++ b/src/Cryptol/IR/FreeVars.hs @@ -93,6 +93,7 @@ instance FreeVars Decl where instance FreeVars DeclDef where freeVars d = case d of DPrim -> mempty + DForeign -> mempty DExpr e -> freeVars e diff --git a/src/Cryptol/ModuleSystem/InstantiateModule.hs b/src/Cryptol/ModuleSystem/InstantiateModule.hs index 9d6b46729..2e70d9a8b 100644 --- a/src/Cryptol/ModuleSystem/InstantiateModule.hs +++ b/src/Cryptol/ModuleSystem/InstantiateModule.hs @@ -227,8 +227,9 @@ instance Inst DeclGroup where instance Inst DeclDef where inst env d = case d of - DPrim -> DPrim - DExpr e -> DExpr (inst env e) + DPrim -> DPrim + DForeign -> DForeign + DExpr e -> DExpr (inst env e) instance Inst Decl where inst env d = d { dSignature = inst env (dSignature d) diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index d43402557..baca1b962 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -683,6 +683,7 @@ instance Rename Bind where instance Rename BindDef where rename DPrim = return DPrim + rename DForeign = return DForeign rename (DExpr e) = DExpr <$> rename e -- NOTE: this only renames types within the pattern. diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y index 7ee646f48..cf58621dd 100644 --- a/src/Cryptol/Parser.y +++ b/src/Cryptol/Parser.y @@ -90,6 +90,7 @@ import Paths_cryptol 'primitive' { Located $$ (Token (KW KW_primitive) _)} 'constraint'{ Located $$ (Token (KW KW_constraint) _)} + 'foreign' { Located $$ (Token (KW KW_foreign) _)} 'Prop' { Located $$ (Token (KW KW_Prop) _)} '[' { Located $$ (Token (Sym BracketL) _)} @@ -251,6 +252,7 @@ vtop_decl :: { [TopDecl PName] } { [exportDecl $1 Public (mkProperty $3 [] $5)] } | mbDoc newtype { [exportNewtype Public $1 $2] } | prim_bind { $1 } + | foreign_bind { $1 } | private_decls { $1 } | parameter_decls { $1 } | mbDoc 'submodule' @@ -273,6 +275,8 @@ prim_bind :: { [TopDecl PName] } | mbDoc 'primitive' '(' op ')' ':' schema { mkPrimDecl $1 $4 $7 } | mbDoc 'primitive' 'type' schema ':' kind {% mkPrimTypeDecl $1 $4 $6 } +foreign_bind :: { [TopDecl PName] } + : mbDoc 'foreign' name ':' schema { mkForeignDecl $1 $3 $5 } parameter_decls :: { [TopDecl PName] } : 'parameter' 'v{' par_decls 'v}' { reverse $3 } diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index d10747e74..90ccd0afa 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -278,6 +278,7 @@ data Bind name = Bind type LBindDef = Located (BindDef PName) data BindDef name = DPrim + | DForeign | DExpr (Expr name) deriving (Eq, Show, Generic, NFData, Functor) @@ -725,6 +726,7 @@ instance (Show name, PPName name) => PP (Bind name) where instance (Show name, PPName name) => PP (BindDef name) where ppPrec _ DPrim = text "" + ppPrec _ DForeign = text "" ppPrec p (DExpr e) = ppPrec p e diff --git a/src/Cryptol/Parser/Lexer.x b/src/Cryptol/Parser/Lexer.x index 0f76c62ae..7b82be8b8 100644 --- a/src/Cryptol/Parser/Lexer.x +++ b/src/Cryptol/Parser/Lexer.x @@ -126,6 +126,7 @@ $white+ { emit $ White Space } "primitive" { emit $ KW KW_primitive } "parameter" { emit $ KW KW_parameter } "constraint" { emit $ KW KW_constraint } +"foreign" { emit $ KW KW_foreign } "Prop" { emit $ KW KW_Prop } diff --git a/src/Cryptol/Parser/Names.hs b/src/Cryptol/Parser/Names.hs index 7f9ba8163..14b7e2bdc 100644 --- a/src/Cryptol/Parser/Names.hs +++ b/src/Cryptol/Parser/Names.hs @@ -63,6 +63,7 @@ namesB b = namesDef :: Ord name => BindDef name -> Set name namesDef DPrim = Set.empty +namesDef DForeign = Set.empty namesDef (DExpr e) = namesE e @@ -183,6 +184,7 @@ 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 -- | The type names used by an expression. diff --git a/src/Cryptol/Parser/NoPat.hs b/src/Cryptol/Parser/NoPat.hs index 9b0c781f0..0bf930250 100644 --- a/src/Cryptol/Parser/NoPat.hs +++ b/src/Cryptol/Parser/NoPat.hs @@ -219,6 +219,11 @@ noMatchB b = | otherwise -> panic "NoPat" [ "noMatchB: primitive with params" , show b ] + DForeign + | 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 } diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs index 5c910f8b8..8ecf5cf37 100644 --- a/src/Cryptol/Parser/ParserUtils.hs +++ b/src/Cryptol/Parser/ParserUtils.hs @@ -624,19 +624,26 @@ mkIf ifThens theElse = foldr addIfThen theElse ifThens where addIfThen (cond, doexpr) elseExpr = EIf cond doexpr elseExpr --- | Generate a signature and a primitive binding. The reason for generating --- both instead of just adding the signature at this point is that it means the --- primitive declarations don't need to be treated differently in the noPat +mkPrimDecl :: Maybe (Located Text) -> LPName -> Schema PName -> [TopDecl PName] +mkPrimDecl = mkNoImplDecl DPrim + +mkForeignDecl :: Maybe (Located Text) -> LPName -> Schema PName -> [TopDecl PName] +mkForeignDecl = mkNoImplDecl DForeign + +-- | Generate a signature and a binding for value declarations with no +-- implementation (i.e. primitive or foreign declarations). The reason for +-- generating both instead of just adding the signature at this point is that it +-- means the declarations don't need to be treated differently in the noPat -- pass. This is also the reason we add the doc to the TopLevel constructor, -- instead of just place it on the binding directly. A better solution might be --- to just have a different constructor for primitives. -mkPrimDecl :: - Maybe (Located Text) -> LPName -> Schema PName -> [TopDecl PName] -mkPrimDecl mbDoc ln sig = +-- to just have a different constructor for primitives and foreigns. +mkNoImplDecl :: BindDef PName + -> Maybe (Located Text) -> LPName -> Schema PName -> [TopDecl PName] +mkNoImplDecl def mbDoc ln sig = [ exportDecl mbDoc Public $ DBind Bind { bName = ln , bParams = [] - , bDef = at sig (Located emptyRange DPrim) + , bDef = at sig (Located emptyRange def) , bSignature = Nothing , bPragmas = [] , bMono = False diff --git a/src/Cryptol/Parser/Token.hs b/src/Cryptol/Parser/Token.hs index c1ec16903..e48d433ba 100644 --- a/src/Cryptol/Parser/Token.hs +++ b/src/Cryptol/Parser/Token.hs @@ -50,6 +50,7 @@ data TokenKW = KW_else | KW_primitive | KW_parameter | KW_constraint + | KW_foreign | KW_Prop | KW_by | KW_down diff --git a/src/Cryptol/Transform/AddModParams.hs b/src/Cryptol/Transform/AddModParams.hs index 22575c6d3..c1908de1d 100644 --- a/src/Cryptol/Transform/AddModParams.hs +++ b/src/Cryptol/Transform/AddModParams.hs @@ -146,11 +146,12 @@ instance AddParams DeclGroup where instance AddParams Decl where addParams ps d = case dDefinition d of - DPrim -> d - DExpr e -> d { dSignature = addParams ps (dSignature d) - , dDefinition = DExpr (addParams ps e) - , dName = toParamInstName (dName d) - } + DPrim -> d + DForeign -> d + DExpr e -> d { dSignature = addParams ps (dSignature d) + , dDefinition = DExpr (addParams ps e) + , dName = toParamInstName (dName d) + } instance AddParams TySyn where addParams ps ts = ts { tsParams = pTypes ps ++ tsParams ts @@ -278,6 +279,7 @@ instance Inst DeclDef where inst ps d = case d of DPrim -> DPrim + DForeign -> DForeign DExpr e -> DExpr (inst ps e) instance Inst Type where diff --git a/src/Cryptol/Transform/MonoValues.hs b/src/Cryptol/Transform/MonoValues.hs index baf4e80e1..3611f17c3 100644 --- a/src/Cryptol/Transform/MonoValues.hs +++ b/src/Cryptol/Transform/MonoValues.hs @@ -218,6 +218,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 = return DForeign rewDeclGroup :: RewMap -> DeclGroup -> M DeclGroup rewDeclGroup rews dg = @@ -237,11 +238,12 @@ rewDeclGroup rews dg = 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 + DPrim -> Left d + DForeign -> 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 = do new <- forM (NE.toList ds) $ \(d,_,_,e) -> diff --git a/src/Cryptol/Transform/Specialize.hs b/src/Cryptol/Transform/Specialize.hs index f71fb2f60..62469d14b 100644 --- a/src/Cryptol/Transform/Specialize.hs +++ b/src/Cryptol/Transform/Specialize.hs @@ -187,9 +187,10 @@ specializeConst e0 = do sig' <- instantiateSchema ts n (dSignature decl) modifySpecCache (Map.adjust (fmap (insertTM ts (qname', Nothing))) qname) rhs' <- case dDefinition decl of - DExpr e -> do e' <- specializeExpr =<< instantiateExpr ts n e - return (DExpr e') - DPrim -> return DPrim + DExpr e -> do e' <- specializeExpr =<< instantiateExpr ts n e + return (DExpr e') + DPrim -> return DPrim + DForeign -> return DForeign 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/AST.hs b/src/Cryptol/TypeCheck/AST.hs index a061630e2..80cfe7415 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -178,6 +178,7 @@ data Decl = Decl { dName :: !Name } deriving (Generic, NFData, Show) data DeclDef = DPrim + | DForeign | DExpr Expr deriving (Show, Generic, NFData) @@ -369,6 +370,7 @@ instance PP (WithNames Decl) where instance PP (WithNames DeclDef) where ppPrec _ (WithNames DPrim _) = text "" + ppPrec _ (WithNames DForeign _) = text "" ppPrec _ (WithNames (DExpr e) nm) = ppWithNames nm e instance PP Decl where diff --git a/src/Cryptol/TypeCheck/Error.hs b/src/Cryptol/TypeCheck/Error.hs index cdb542596..e653e18c5 100644 --- a/src/Cryptol/TypeCheck/Error.hs +++ b/src/Cryptol/TypeCheck/Error.hs @@ -143,6 +143,13 @@ data Error = KindMismatch (Maybe TypeSource) Kind Kind | MissingModTParam (Located Ident) | MissingModVParam (Located Ident) + | UnsupportedFFIType TypeSource Type + -- ^ Type is not supported for passing to/returning from a + -- foreign function + + | UnsupportedFFIPoly TypeSource + -- ^ Foreign functions cannot be polymorphic + | TemporaryError Doc -- ^ This is for errors that don't fit other cateogories. -- We should not use it much, and is generally to be used @@ -199,7 +206,8 @@ errorImportance err = AmbiguousSize {} -> 2 - + UnsupportedFFIPoly {} -> 10 + UnsupportedFFIType {} -> 9 instance TVars Warning where @@ -249,6 +257,9 @@ instance TVars Error where MissingModTParam {} -> err MissingModVParam {} -> err + UnsupportedFFIType src t -> UnsupportedFFIType src !$ apSubst su t + UnsupportedFFIPoly {} -> err + TemporaryError {} -> err @@ -284,6 +295,9 @@ instance FVS Error where MissingModTParam {} -> Set.empty MissingModVParam {} -> Set.empty + UnsupportedFFIType _ t -> fvs t + UnsupportedFFIPoly {} -> Set.empty + TemporaryError {} -> Set.empty instance PP Warning where @@ -457,6 +471,15 @@ instance PP (WithNames Error) where MissingModVParam x -> "Missing definition for value parameter" <+> quotes (pp (thing x)) + UnsupportedFFIType src t -> + nested "Type unsupported for FFI:" $ + vcat + [ ppWithNames names t + , "When checking" <+> pp src] + UnsupportedFFIPoly src -> + nested "Polymorphism is not supported for FFI" $ + "When checking" <+> pp src + TemporaryError doc -> doc where bullets xs = vcat [ "•" <+> d | d <- xs ] diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index 62b51cc1e..e0b22c51d 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -927,8 +927,9 @@ generalize bs0 gs0 = genE e = foldr ETAbs (foldr EProofAbs (apSubst su e) qs) asPs genB d = d { dDefinition = case dDefinition d of - DExpr e -> DExpr (genE e) - DPrim -> DPrim + DExpr e -> DExpr (genE e) + DPrim -> DPrim + DForeign -> DForeign , dSignature = Forall asPs qs $ apSubst su $ sType $ dSignature d } @@ -950,6 +951,8 @@ checkMonoB b t = P.DPrim -> panic "checkMonoB" ["Primitive with no signature?"] + P.DForeign -> panic "checkMonoB" ["Foreign with no signature?"] + P.DExpr e -> do let nm = thing (P.bName b) let tGoal = WithSource t (DefinitionOf nm) (getLoc b) @@ -979,6 +982,28 @@ checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of , dDoc = P.bDoc b } + -- We only support very specific types for FFI for now + P.DForeign -> + let loc = getLoc b + src = DefinitionOf $ thing $ P.bName b + in inRangeMb loc do + unless (null as && null asmps0) $ + recordErrorLoc loc $ UnsupportedFFIPoly src + case t0 of + TCon (TC TCFun) + [ TCon (TC TCSeq) [TCon (TC (TCNum 64)) [], TCon (TC TCBit) []] + , TCon (TC TCSeq) [TCon (TC (TCNum 64)) [], TCon (TC TCBit) []] + ] -> pure () + _ -> recordErrorLoc loc $ UnsupportedFFIType src t0 + return Decl { dName = thing (P.bName b) + , dSignature = Forall as asmps0 t0 + , dDefinition = DForeign + , dPragmas = P.bPragmas b + , dInfix = P.bInfix b + , dFixity = P.bFixity b + , dDoc = P.bDoc b + } + P.DExpr e0 -> inRangeMb (getLoc b) $ withTParams as $ diff --git a/src/Cryptol/TypeCheck/Parseable.hs b/src/Cryptol/TypeCheck/Parseable.hs index 86f72f06b..cfb4e3f79 100644 --- a/src/Cryptol/TypeCheck/Parseable.hs +++ b/src/Cryptol/TypeCheck/Parseable.hs @@ -93,6 +93,7 @@ instance ShowParseable Decl where instance ShowParseable DeclDef where showParseable DPrim = text (show DPrim) + showParseable DForeign = text (show DForeign) showParseable (DExpr e) = parens (text "DExpr" $$ showParseable e) instance ShowParseable DeclGroup where diff --git a/src/Cryptol/TypeCheck/Sanity.hs b/src/Cryptol/TypeCheck/Sanity.hs index fc995288d..b4b4c615f 100644 --- a/src/Cryptol/TypeCheck/Sanity.hs +++ b/src/Cryptol/TypeCheck/Sanity.hs @@ -398,6 +398,10 @@ checkDecl checkSig d = do when checkSig $ checkSchema $ dSignature d return (dName d, dSignature d) + DForeign -> + do when checkSig $ checkSchema $ dSignature d + return (dName d, dSignature d) + DExpr e -> do let s = dSignature d when checkSig $ checkSchema s diff --git a/src/Cryptol/TypeCheck/Subst.hs b/src/Cryptol/TypeCheck/Subst.hs index 474c537a8..b14be4540 100644 --- a/src/Cryptol/TypeCheck/Subst.hs +++ b/src/Cryptol/TypeCheck/Subst.hs @@ -408,6 +408,7 @@ instance TVars Decl where instance TVars DeclDef where apSubst su (DExpr e) = DExpr !$ (apSubst su e) apSubst _ DPrim = DPrim + apSubst _ DForeign = DForeign instance TVars Module where apSubst su m =