Add frontend for FFI

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

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

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
 
 

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)

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.

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 }

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 "<primitive>"
+  ppPrec _ DForeign  = text "<foreign>"
   ppPrec p (DExpr e) = ppPrec p e
 
 

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 }
 

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.

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 }

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

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

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

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

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

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 "<primitive>"
+  ppPrec _ (WithNames DForeign _)   = text "<foreign>"
   ppPrec _ (WithNames (DExpr e) nm) = ppWithNames nm e
 
 instance PP Decl where

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 ]

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 $

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