diff --git a/src/Cryptol/Eval.hs b/src/Cryptol/Eval.hs index 48ed0ca0e..37176159c 100644 --- a/src/Cryptol/Eval.hs +++ b/src/Cryptol/Eval.hs @@ -368,7 +368,16 @@ evalDeclGroup :: SEval sym (GenEvalEnv sym) evalDeclGroup sym env dg = do case dg of - Recursive ds -> do + Recursive ds0 -> do + let ds = filter shouldEval ds0 + -- If there are foreign declarations, we should only evaluate them if + -- they are not already bound in the environment by the previous + -- Cryptol.Eval.FFI.evalForeignDecls pass. + shouldEval d = + case (dDefinition d, lookupVar (dName d) env) of + (DForeign _ _, Just _) -> False + _ -> True + -- declare a "hole" for each declaration -- and extend the evaluation environment holes <- mapM (declHole sym) ds @@ -432,14 +441,19 @@ 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)] - DForeign _ _ -> evalPanic "Unexpected foreign declaration in recursive group" - [show (ppLocName nm)] - DExpr _ -> do - (hole, fill) <- sDeclareHole sym msg - return (nm, sch, hole, fill) + DPrim -> evalPanic "Unexpected primitive declaration in recursive group" + [show (ppLocName nm)] + DForeign _ me -> + case me of + Nothing -> evalPanic + "Unexpected foreign declaration with no cryptol implementation in recursive group" + [show (ppLocName nm)] + Just _ -> doHole + DExpr _ -> doHole where + doHole = do + (hole, fill) <- sDeclareHole sym msg + return (nm, sch, hole, fill) nm = dName d sch = dSignature d msg = unwords ["while evaluating", show (pp nm)] diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index c4758fd63..1833f36ae 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -145,18 +145,23 @@ 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 _ }) - = Just (dName, ffiType) - -- Recursive DeclGroups can't have foreign decls - getForeign _ = Nothing - --- | Find all the foreign declarations that are in functors. +findForeignDecls = mapMaybe getForeign . concatMap groupDecls . mDecls + where getForeign d = + case dDefinition d of + DForeign ffiType _ -> Just (dName d, ffiType) + _ -> Nothing + +-- | Find all the foreign declarations that are in functors, including in the +-- top-level module itself if it is a functor. -- This is used to report an error findForeignDeclsInFunctors :: ModuleG mname -> [Name] -findForeignDeclsInFunctors = concatMap fromM . Map.elems . mFunctors +findForeignDeclsInFunctors mo + | isParametrizedModule mo = fromM mo + | otherwise = findInSubs mo where - fromM m = map fst (findForeignDecls m) ++ findForeignDeclsInFunctors m + findInSubs :: ModuleG mname -> [Name] + findInSubs = concatMap fromM . Map.elems . mFunctors + fromM m = map fst (findForeignDecls m) ++ findInSubs m diff --git a/tests/ffi/ffi-fallback-rec.c b/tests/ffi/ffi-fallback-rec.c new file mode 100644 index 000000000..981c8fd6f --- /dev/null +++ b/tests/ffi/ffi-fallback-rec.c @@ -0,0 +1,5 @@ +#include + +uint8_t f(uint8_t x) { + return x; +} diff --git a/tests/ffi/ffi-fallback-rec.cry b/tests/ffi/ffi-fallback-rec.cry new file mode 100644 index 000000000..4247679bf --- /dev/null +++ b/tests/ffi/ffi-fallback-rec.cry @@ -0,0 +1,5 @@ +foreign f : Bit -> Bit +f x = ~ g x + +foreign g : Bit -> Bit +g x = ~ f x diff --git a/tests/ffi/ffi-fallback-rec.icry b/tests/ffi/ffi-fallback-rec.icry new file mode 100644 index 000000000..e454a20fd --- /dev/null +++ b/tests/ffi/ffi-fallback-rec.icry @@ -0,0 +1,3 @@ +:! make -s ffi-fallback-rec +:l ffi-fallback-rec.cry +g True diff --git a/tests/ffi/ffi-fallback-rec.icry.stdout b/tests/ffi/ffi-fallback-rec.icry.stdout new file mode 100644 index 000000000..c3ba8475f --- /dev/null +++ b/tests/ffi/ffi-fallback-rec.icry.stdout @@ -0,0 +1,8 @@ +Loading module Cryptol +Loading module Cryptol +Loading module Main +Loading dynamic library ffi-fallback-rec.so +[warning] Could not load all foreign implementations for module Main: + Could not load foreign implementation for binding g + Fallback cryptol implementations will be used if available +False diff --git a/tests/ffi/ffi-fallback-rec.icry.stdout.darwin b/tests/ffi/ffi-fallback-rec.icry.stdout.darwin new file mode 100644 index 000000000..192811583 --- /dev/null +++ b/tests/ffi/ffi-fallback-rec.icry.stdout.darwin @@ -0,0 +1,8 @@ +Loading module Cryptol +Loading module Cryptol +Loading module Main +Loading dynamic library ffi-fallback-rec.dylib +[warning] Could not load all foreign implementations for module Main: + Could not load foreign implementation for binding g + Fallback cryptol implementations will be used if available +False diff --git a/tests/ffi/ffi-fallback-rec.icry.stdout.mingw32 b/tests/ffi/ffi-fallback-rec.icry.stdout.mingw32 new file mode 100644 index 000000000..1d8aeaefb --- /dev/null +++ b/tests/ffi/ffi-fallback-rec.icry.stdout.mingw32 @@ -0,0 +1,8 @@ +Loading module Cryptol +Loading module Cryptol +Loading module Main +Loading dynamic library ffi-fallback-rec.dll +[warning] Could not load all foreign implementations for module Main: + Could not load foreign implementation for binding g + Fallback cryptol implementations will be used if available +False