Add verification pass. (#23)

Author: gmorpheme

lib/prelude.eu

@@ -392,7 +392,7 @@ with-meta: __WITHMETA
     export: :suppress 
     associates: :left
     precedence: :meta }
-(e // m): v with-meta(m)
+(e // m): e with-meta(m)
 
 ` { doc: "`meta e` - retrieve expression metadata for e"
     export: :suppress }
@@ -514,7 +514,7 @@ zip-with: map2
 
 ` { doc: "`zip-apply(fs, vs)` - apply functions in list `fs` to corresponding values in list `vs`, stopping when shorter list is exhausted."
     export: :suppress }
-zip-apply(fs, vs): zip-with(apply1, fs, vs)
+zip-apply(fs, vs): zip-with(cat, vs, fs)
 
 ` { doc: "`reverse(l) - reverse list `l`"
     example: reverse([1,2,3]) //=> [3,2,1]
@@ -614,7 +614,7 @@ by-value(p?): p? ∘ value
 select-items(f, b): b elements filter(f) 
 
 ` "`match-select-values` - return list of values from block `b` with keys matching regex `re`."
-match-select-values(re, b): b select(by-key-match(re)) map(value)
+match-select-values(re, b): b select-items(by-key-match(re)) map(value)
 
 ` "`select-values(p?, b)` - return items from block `b` where values match predicate `p?`"
 select-values(p?, b): b map(value) filter(p?)

src/Eucalypt/Core/Error.hs

@@ -52,6 +52,8 @@ data EvaluationError
   | Panic String CoreExpShow
   | Bug String CoreExpShow
   | EmptyList CoreExpShow
+  | VerifyOperatorsFailed CoreExpShow
+  | VerifyUnresolvedVar CoreBindingName
   | NoSource
   | AssertionFailed CoreExpShow
 
@@ -86,6 +88,8 @@ instance Show EvaluationError where
   show (InvalidArgConvention (CoreExpShow exprs)) = "Args passed incorrectly. " ++ pprint exprs
   show (UnexpectedEndOfExpression (CoreExpShow expr)) = "UnexpectedEndOfExpression after " ++ pprint expr
   show (EmptyList (CoreExpShow expr)) = "List was empty in " ++ pprint expr
+  show (VerifyOperatorsFailed (CoreExpShow expr)) = "Unresolved operator in " ++ pprint expr
+  show (VerifyUnresolvedVar name) = "Unresolved variable in " ++ name
   show (Panic message (CoreExpShow expr)) = "Panic - " ++ message ++ " in " ++ pprint expr
   show (Bug message (CoreExpShow expr)) = "BUG! " ++ message ++ " - " ++ pprint expr
   show (AssertionFailed (CoreExpShow expr)) = "Assertion Failed. " ++ pprint expr

src/Eucalypt/Core/Verify.hs

@@ -0,0 +1,55 @@
+{-# LANGUAGE RankNTypes #-}
+{-|
+Module      : Eucalypt.Core.Verify
+Description : Checks to run prior to evaluation
+Copyright   : (c) Greg Hawkins, 2018
+License     :
+Maintainer  : [email protected]
+Stability   : experimental
+-}
+
+module Eucalypt.Core.Verify where
+
+import Bound
+import Data.Foldable
+import Eucalypt.Core.Error
+import Eucalypt.Core.Syn
+
+-- | Run all the check functions throughout the tree
+runChecks :: Show b => CoreExp b -> [EvaluationError]
+runChecks expr = verify noSoup expr ++ map (VerifyUnresolvedVar . show) (toList expr)
+
+-- | Apply a check function to every level in the syntax tree
+verify ::
+     Show b
+  => (forall a. Show a =>
+                  (CoreExp a -> [EvaluationError]))
+  -> CoreExp b
+  -> [EvaluationError]
+verify f e@(CoreLet bs b) =
+  let shallow = f e
+      deep = foldMap id (verify f (unscope b) : map (verify f . unscope . snd) bs)
+  in shallow ++ deep
+verify f e@(CoreLambda _ b) =
+  let shallow = f e
+      deep = verify f (unscope b)
+   in shallow ++ deep
+verify f e@(CoreMeta m expr) =
+  f e ++ verify f m ++ verify f expr
+verify f e@(CoreTraced expr) =
+  f e ++ verify f expr
+verify f e@(CoreChecked ck expr) =
+  f e ++ verify f ck ++ verify f expr
+verify f e@(CoreBlock expr) =
+  f e ++ verify f expr
+verify f e@(CoreList exprs) =
+  f e ++ concatMap (verify f) exprs
+verify f e@(CoreArgTuple exprs) =
+  f e ++ concatMap (verify f) exprs
+verify f e@(CoreOperator _ _ expr) =
+  f e ++ verify f expr
+verify f e = f e
+
+noSoup :: Show a => CoreExp a -> [EvaluationError]
+noSoup o@(CoreOpSoup _) = [(VerifyOperatorsFailed . CoreExpShow) o]
+noSoup _ = []

src/Eucalypt/Driver/Evaluator.hs

@@ -4,7 +4,7 @@ where
 
 import Control.Applicative ((<|>))
 import Control.Exception.Safe (try)
-import Control.Monad (forM_, when)
+import Control.Monad (forM_, when, unless)
 import Data.Bifunctor
 import qualified Data.ByteString as BS
 import Data.Either (partitionEithers)
@@ -23,6 +23,7 @@ import Eucalypt.Core.Pretty
 import Eucalypt.Core.Syn
 import Eucalypt.Core.Target
 import Eucalypt.Core.Unit
+import Eucalypt.Core.Verify
 import Eucalypt.Driver.Error (CommandError(..))
 import Eucalypt.Driver.IOSource (prepareIOUnit)
 import Eucalypt.Driver.Input (Input(..), InputMode(..), Locator(..))
@@ -237,20 +238,24 @@ evaluate opts whnfM = do
   when (cmd == ListTargets)
     (listTargets opts targets >> exitSuccess)
 
-  -- Stage 5: form an expression to evaluate from the source or
+  -- Stage 4: form an expression to evaluate from the source or
   -- command line and embed it in the core tree
   evaluand <- formEvaluand opts targets core
   when (cmd == DumpEvalSubstituted)
     (putStrLn (pprint evaluand) >> exitSuccess)
 
-  -- Stage 6: cook operator soups to resolve all fixities and prepare
+  -- Stage 5: cook operator soups to resolve all fixities and prepare
   -- a final tree for evaluation
   cookedEvaluand <- runFixityPass evaluand
   when (cmd == DumpCooked)
     (putStrLn (pprint cookedEvaluand) >> exitSuccess)
   when (cmd == DumpFinalCore)
     (putStrLn (pprint cookedEvaluand) >> exitSuccess)
 
+  -- Stage 6: run final checks
+  let failures = runChecks cookedEvaluand
+  unless (null failures) $ reportErrors failures >> exitFailure
+
   -- Stage 7: drive the evaluation by rendering it
   render cookedEvaluand >>= \case
     Left s -> reportErrors [s] >> return (ExitFailure 1)

test/Eucalypt/Core/VerifySpec.hs

@@ -0,0 +1,32 @@
+module Eucalypt.Core.VerifySpec
+  ( main
+  , spec
+  ) where
+
+import Eucalypt.Core.Syn
+import Eucalypt.Core.Verify
+import Test.Hspec
+
+main :: IO ()
+main = hspec spec
+
+spec :: Spec
+spec = do
+  describe "Soup checks" $ do
+    it "discovers soup" $
+      runChecks (lam ["x", "y"] $ soup [var "x", var "+", var "y"])
+      `shouldSatisfy`
+      (not . null)
+    it "passes fully cooked expressions" $
+      runChecks (lam ["x", "y"] $ app (bif "ADD") [var "x", var "y"])
+      `shouldSatisfy`
+      null
+  describe "Closed checks" $ do
+    it "discovers free vars" $
+      runChecks (lam ["x", "y", "+"] $ soup [var "x", var "+", var "s"])
+      `shouldSatisfy`
+       (not . null)
+    it "passes closed expressions" $
+      runChecks (lam ["x", "y", "+"] $ app (bif "ADD") [var "x", var "y"])
+      `shouldSatisfy`
+       null