From 768554137ad8eb2bf5c35b84d4fa937040bb2eb2 Mon Sep 17 00:00:00 2001 From: Jakub Zalewski Date: Thu, 14 May 2020 13:48:17 +0200 Subject: [PATCH] [AST] fix statement vs expression Fixes #51, #52 We make the following changes to the AST by adding - a newly introduced a top-level `Program` node, which is parent to - a newly introduced `Statements` node, which is parent to - a `Statement` node, which is chaned to be a parent of - an `Expr` node. We make the following changes to Statement by - introduce a `EFor` node to the typed AST. We update update the evaluator by - providing an explicit transformer stack (`EvalT`), - fixing the semantics for for loops, and - switching to CPS both in evaluator and normaliser. We also add minor improvements to the codebase by - fixing `Sign` vs `Sig` naming issue, - cleaning up some naming conventions, and - providing `stack bench` benchmark for testing generators for the new AST. --- bench/Main.hs | 81 +++++ field/TinyLang/Field/Core.hs | 19 ++ field/TinyLang/Field/Evaluator.hs | 306 +++++++++++------- field/TinyLang/Field/Generator.hs | 296 ++++++++++------- field/TinyLang/Field/Printer.hs | 34 +- field/TinyLang/Field/Raw/Core.hs | 49 ++- field/TinyLang/Field/Raw/Parser.hs | 31 +- field/TinyLang/Field/Rename.hs | 36 ++- field/TinyLang/Field/Typed/Core.hs | 170 ++++++---- field/TinyLang/Field/Typed/Parser.hs | 49 +-- field/TinyLang/Field/Typed/TypeChecker.hs | 51 ++- test/Field/Raw/golden/00-bool-literals.field | 2 + test/Field/Raw/golden/00-bool-literals.golden | 1 + test/Field/Raw/golden/01-field-literals.field | 5 + .../Field/Raw/golden/01-field-literals.golden | 1 + .../Field/Raw/golden/02-vector-literals.field | 4 + .../Raw/golden/02-vector-literals.golden | 1 + .../Raw/golden/03-lexer-whitespace.field | 13 + .../Raw/golden/03-lexer-whitespace.golden | 1 + .../Raw/golden/04-lexer-whitespace.field | 2 + .../Raw/golden/04-lexer-whitespace.golden | 1 + ...ace-02.field => 05-lexer-whitespace.field} | 6 +- .../Raw/golden/05-lexer-whitespace.golden | 1 + ...-00.field => 06-operator-precedence.field} | 3 +- .../Raw/golden/06-operator-precedence.golden | 1 + .../Raw/golden/07-operator-precedence.field | 3 + .../Raw/golden/07-operator-precedence.golden | 1 + ...-02.field => 08-operator-precedence.field} | 2 + .../Raw/golden/08-operator-precedence.golden | 1 + test/Field/Raw/golden/09-for-loop.field | 1 + test/Field/Raw/golden/09-for-loop.golden | 1 + .../{for-loop-01.field => 10-for-loop.field} | 1 - test/Field/Raw/golden/10-for-loop.golden | 1 + .../{everything.field => 11-everything.field} | 9 +- test/Field/Raw/golden/11-everything.golden | 1 + test/Field/Raw/golden/bool-literal-F.field | 1 - test/Field/Raw/golden/bool-literal-F.golden | 1 - test/Field/Raw/golden/bool-literal-T.field | 1 - test/Field/Raw/golden/bool-literal-T.golden | 1 - test/Field/Raw/golden/everything.golden | 1 - test/Field/Raw/golden/for-loop-00.field | 1 - test/Field/Raw/golden/for-loop-00.golden | 1 - test/Field/Raw/golden/for-loop-01.golden | 1 - .../Raw/golden/lexer-whitespace-01.field | 2 - .../Raw/golden/lexer-whitespace-01.golden | 1 - .../Raw/golden/lexer-whitespace-02.golden | 1 - .../Raw/golden/operator-precedence-00.golden | 1 - .../Raw/golden/operator-precedence-01.field | 1 - .../Raw/golden/operator-precedence-01.golden | 1 - .../Raw/golden/operator-precedence-02.golden | 1 - test/Field/Raw/golden/vec-literal.field | 1 - test/Field/Raw/golden/vec-literal.golden | 1 - test/Field/Renaming.hs | 53 +++ test/Field/TestUtils.hs | 16 +- test/Field/Textual.hs | 195 +++++++---- test/Field/Typed/Textual.hs | 8 - test/Field/Typed/golden/00-constant.field | 1 - test/Field/Typed/golden/00-constant.golden | 1 - test/Field/Typed/golden/00-constants.field | 4 + test/Field/Typed/golden/00-constants.golden | 1 + test/Field/Typed/golden/01-constant.field | 1 - test/Field/Typed/golden/01-constant.golden | 1 - test/Field/Typed/golden/01-variables.field | 3 + test/Field/Typed/golden/01-variables.golden | 1 + test/Field/Typed/golden/02-binops.field | 17 + test/Field/Typed/golden/02-binops.golden | 1 + test/Field/Typed/golden/02-constant.field | 1 - test/Field/Typed/golden/02-constant.golden | 1 - test/Field/Typed/golden/03-unops.field | 7 + test/Field/Typed/golden/03-unops.golden | 1 + test/Field/Typed/golden/03-variable.field | 1 - test/Field/Typed/golden/03-variable.golden | 1 - test/Field/Typed/golden/04-statements.field | 3 + test/Field/Typed/golden/04-statements.golden | 1 + test/Field/Typed/golden/04-variable.field | 1 - test/Field/Typed/golden/04-variable.golden | 1 - test/Field/Typed/golden/05-ifs.field | 3 + test/Field/Typed/golden/05-ifs.golden | 1 + test/Field/Typed/golden/05-variable.field | 1 - test/Field/Typed/golden/05-variable.golden | 1 - test/Field/Typed/golden/06-anns.field | 3 + test/Field/Typed/golden/06-anns.golden | 1 + test/Field/Typed/golden/06-binop.field | 1 - test/Field/Typed/golden/06-binop.golden | 1 - test/Field/Typed/golden/07-binop.field | 1 - test/Field/Typed/golden/07-binop.golden | 1 - ...2-everything.field => 07-everything.field} | 12 +- test/Field/Typed/golden/07-everything.golden | 1 + test/Field/Typed/golden/08-binop.field | 1 - test/Field/Typed/golden/08-binop.golden | 1 - test/Field/Typed/golden/09-binop.field | 1 - test/Field/Typed/golden/09-binop.golden | 1 - test/Field/Typed/golden/10-binop.field | 1 - test/Field/Typed/golden/10-binop.golden | 1 - test/Field/Typed/golden/11-binop.field | 1 - test/Field/Typed/golden/11-binop.golden | 1 - test/Field/Typed/golden/12-binop.field | 1 - test/Field/Typed/golden/12-binop.golden | 1 - test/Field/Typed/golden/13-binop.field | 1 - test/Field/Typed/golden/13-binop.golden | 1 - test/Field/Typed/golden/14-binop.field | 1 - test/Field/Typed/golden/14-binop.golden | 1 - test/Field/Typed/golden/15-binop.field | 1 - test/Field/Typed/golden/15-binop.golden | 1 - test/Field/Typed/golden/16-binop.field | 1 - test/Field/Typed/golden/16-binop.golden | 1 - test/Field/Typed/golden/17-binop.field | 1 - test/Field/Typed/golden/17-binop.golden | 1 - test/Field/Typed/golden/18-binop.field | 1 - test/Field/Typed/golden/18-binop.golden | 1 - test/Field/Typed/golden/19-unop.field | 1 - test/Field/Typed/golden/19-unop.golden | 1 - test/Field/Typed/golden/20-unop.field | 1 - test/Field/Typed/golden/20-unop.golden | 1 - test/Field/Typed/golden/21-unop.field | 1 - test/Field/Typed/golden/21-unop.golden | 1 - test/Field/Typed/golden/22-unop.field | 1 - test/Field/Typed/golden/22-unop.golden | 1 - test/Field/Typed/golden/23-unop.field | 1 - test/Field/Typed/golden/23-unop.golden | 1 - test/Field/Typed/golden/24-statement.field | 1 - test/Field/Typed/golden/24-statement.golden | 1 - test/Field/Typed/golden/25-statement.field | 1 - test/Field/Typed/golden/25-statement.golden | 1 - test/Field/Typed/golden/26-statement.field | 1 - test/Field/Typed/golden/26-statement.golden | 1 - test/Field/Typed/golden/27-if.field | 1 - test/Field/Typed/golden/27-if.golden | 1 - test/Field/Typed/golden/28-if.field | 1 - test/Field/Typed/golden/28-if.golden | 1 - test/Field/Typed/golden/29-ann.field | 1 - test/Field/Typed/golden/29-ann.golden | 1 - test/Field/Typed/golden/30-ann.field | 1 - test/Field/Typed/golden/30-ann.golden | 1 - test/Field/Typed/golden/31-ann.field | 1 - test/Field/Typed/golden/31-ann.golden | 1 - test/Field/Typed/golden/32-everything.golden | 1 - test/Field/golden/00-for-loops.field | 11 + test/Field/golden/00-for-loops.golden | 11 + test/Field/golden/01-uniques.field | 8 + test/Field/golden/01-uniques.golden | 8 + test/Field/golden/forLoops.golden | 1 - test/Main.hs | 10 +- tiny-lang.cabal | 21 +- 144 files changed, 1126 insertions(+), 544 deletions(-) create mode 100644 bench/Main.hs create mode 100644 field/TinyLang/Field/Core.hs create mode 100644 test/Field/Raw/golden/00-bool-literals.field create mode 100644 test/Field/Raw/golden/00-bool-literals.golden create mode 100644 test/Field/Raw/golden/01-field-literals.field create mode 100644 test/Field/Raw/golden/01-field-literals.golden create mode 100644 test/Field/Raw/golden/02-vector-literals.field create mode 100644 test/Field/Raw/golden/02-vector-literals.golden create mode 100644 test/Field/Raw/golden/03-lexer-whitespace.field create mode 100644 test/Field/Raw/golden/03-lexer-whitespace.golden create mode 100644 test/Field/Raw/golden/04-lexer-whitespace.field create mode 100644 test/Field/Raw/golden/04-lexer-whitespace.golden rename test/Field/Raw/golden/{lexer-whitespace-02.field => 05-lexer-whitespace.field} (75%) create mode 100644 test/Field/Raw/golden/05-lexer-whitespace.golden rename test/Field/Raw/golden/{operator-precedence-00.field => 06-operator-precedence.field} (91%) create mode 100644 test/Field/Raw/golden/06-operator-precedence.golden create mode 100644 test/Field/Raw/golden/07-operator-precedence.field create mode 100644 test/Field/Raw/golden/07-operator-precedence.golden rename test/Field/Raw/golden/{operator-precedence-02.field => 08-operator-precedence.field} (87%) create mode 100644 test/Field/Raw/golden/08-operator-precedence.golden create mode 100644 test/Field/Raw/golden/09-for-loop.field create mode 100644 test/Field/Raw/golden/09-for-loop.golden rename test/Field/Raw/golden/{for-loop-01.field => 10-for-loop.field} (90%) create mode 100644 test/Field/Raw/golden/10-for-loop.golden rename test/Field/Raw/golden/{everything.field => 11-everything.field} (80%) create mode 100644 test/Field/Raw/golden/11-everything.golden delete mode 100644 test/Field/Raw/golden/bool-literal-F.field delete mode 100644 test/Field/Raw/golden/bool-literal-F.golden delete mode 100644 test/Field/Raw/golden/bool-literal-T.field delete mode 100644 test/Field/Raw/golden/bool-literal-T.golden delete mode 100644 test/Field/Raw/golden/everything.golden delete mode 100644 test/Field/Raw/golden/for-loop-00.field delete mode 100644 test/Field/Raw/golden/for-loop-00.golden delete mode 100644 test/Field/Raw/golden/for-loop-01.golden delete mode 100644 test/Field/Raw/golden/lexer-whitespace-01.field delete mode 100644 test/Field/Raw/golden/lexer-whitespace-01.golden delete mode 100644 test/Field/Raw/golden/lexer-whitespace-02.golden delete mode 100644 test/Field/Raw/golden/operator-precedence-00.golden delete mode 100644 test/Field/Raw/golden/operator-precedence-01.field delete mode 100644 test/Field/Raw/golden/operator-precedence-01.golden delete mode 100644 test/Field/Raw/golden/operator-precedence-02.golden delete mode 100644 test/Field/Raw/golden/vec-literal.field delete mode 100644 test/Field/Raw/golden/vec-literal.golden create mode 100644 test/Field/Renaming.hs delete mode 100644 test/Field/Typed/golden/00-constant.field delete mode 100644 test/Field/Typed/golden/00-constant.golden create mode 100644 test/Field/Typed/golden/00-constants.field create mode 100644 test/Field/Typed/golden/00-constants.golden delete mode 100644 test/Field/Typed/golden/01-constant.field delete mode 100644 test/Field/Typed/golden/01-constant.golden create mode 100644 test/Field/Typed/golden/01-variables.field create mode 100644 test/Field/Typed/golden/01-variables.golden create mode 100644 test/Field/Typed/golden/02-binops.field create mode 100644 test/Field/Typed/golden/02-binops.golden delete mode 100644 test/Field/Typed/golden/02-constant.field delete mode 100644 test/Field/Typed/golden/02-constant.golden create mode 100644 test/Field/Typed/golden/03-unops.field create mode 100644 test/Field/Typed/golden/03-unops.golden delete mode 100644 test/Field/Typed/golden/03-variable.field delete mode 100644 test/Field/Typed/golden/03-variable.golden create mode 100644 test/Field/Typed/golden/04-statements.field create mode 100644 test/Field/Typed/golden/04-statements.golden delete mode 100644 test/Field/Typed/golden/04-variable.field delete mode 100644 test/Field/Typed/golden/04-variable.golden create mode 100644 test/Field/Typed/golden/05-ifs.field create mode 100644 test/Field/Typed/golden/05-ifs.golden delete mode 100644 test/Field/Typed/golden/05-variable.field delete mode 100644 test/Field/Typed/golden/05-variable.golden create mode 100644 test/Field/Typed/golden/06-anns.field create mode 100644 test/Field/Typed/golden/06-anns.golden delete mode 100644 test/Field/Typed/golden/06-binop.field delete mode 100644 test/Field/Typed/golden/06-binop.golden delete mode 100644 test/Field/Typed/golden/07-binop.field delete mode 100644 test/Field/Typed/golden/07-binop.golden rename test/Field/Typed/golden/{32-everything.field => 07-everything.field} (80%) create mode 100644 test/Field/Typed/golden/07-everything.golden delete mode 100644 test/Field/Typed/golden/08-binop.field delete mode 100644 test/Field/Typed/golden/08-binop.golden delete mode 100644 test/Field/Typed/golden/09-binop.field delete mode 100644 test/Field/Typed/golden/09-binop.golden delete mode 100644 test/Field/Typed/golden/10-binop.field delete mode 100644 test/Field/Typed/golden/10-binop.golden delete mode 100644 test/Field/Typed/golden/11-binop.field delete mode 100644 test/Field/Typed/golden/11-binop.golden delete mode 100644 test/Field/Typed/golden/12-binop.field delete mode 100644 test/Field/Typed/golden/12-binop.golden delete mode 100644 test/Field/Typed/golden/13-binop.field delete mode 100644 test/Field/Typed/golden/13-binop.golden delete mode 100644 test/Field/Typed/golden/14-binop.field delete mode 100644 test/Field/Typed/golden/14-binop.golden delete mode 100644 test/Field/Typed/golden/15-binop.field delete mode 100644 test/Field/Typed/golden/15-binop.golden delete mode 100644 test/Field/Typed/golden/16-binop.field delete mode 100644 test/Field/Typed/golden/16-binop.golden delete mode 100644 test/Field/Typed/golden/17-binop.field delete mode 100644 test/Field/Typed/golden/17-binop.golden delete mode 100644 test/Field/Typed/golden/18-binop.field delete mode 100644 test/Field/Typed/golden/18-binop.golden delete mode 100644 test/Field/Typed/golden/19-unop.field delete mode 100644 test/Field/Typed/golden/19-unop.golden delete mode 100644 test/Field/Typed/golden/20-unop.field delete mode 100644 test/Field/Typed/golden/20-unop.golden delete mode 100644 test/Field/Typed/golden/21-unop.field delete mode 100644 test/Field/Typed/golden/21-unop.golden delete mode 100644 test/Field/Typed/golden/22-unop.field delete mode 100644 test/Field/Typed/golden/22-unop.golden delete mode 100644 test/Field/Typed/golden/23-unop.field delete mode 100644 test/Field/Typed/golden/23-unop.golden delete mode 100644 test/Field/Typed/golden/24-statement.field delete mode 100644 test/Field/Typed/golden/24-statement.golden delete mode 100644 test/Field/Typed/golden/25-statement.field delete mode 100644 test/Field/Typed/golden/25-statement.golden delete mode 100644 test/Field/Typed/golden/26-statement.field delete mode 100644 test/Field/Typed/golden/26-statement.golden delete mode 100644 test/Field/Typed/golden/27-if.field delete mode 100644 test/Field/Typed/golden/27-if.golden delete mode 100644 test/Field/Typed/golden/28-if.field delete mode 100644 test/Field/Typed/golden/28-if.golden delete mode 100644 test/Field/Typed/golden/29-ann.field delete mode 100644 test/Field/Typed/golden/29-ann.golden delete mode 100644 test/Field/Typed/golden/30-ann.field delete mode 100644 test/Field/Typed/golden/30-ann.golden delete mode 100644 test/Field/Typed/golden/31-ann.field delete mode 100644 test/Field/Typed/golden/31-ann.golden delete mode 100644 test/Field/Typed/golden/32-everything.golden create mode 100644 test/Field/golden/00-for-loops.field create mode 100644 test/Field/golden/00-for-loops.golden create mode 100644 test/Field/golden/01-uniques.field create mode 100644 test/Field/golden/01-uniques.golden delete mode 100644 test/Field/golden/forLoops.golden diff --git a/bench/Main.hs b/bench/Main.hs new file mode 100644 index 0000000..d91038e --- /dev/null +++ b/bench/Main.hs @@ -0,0 +1,81 @@ +import TinyLang.Field.Generator () +import TinyLang.Field.Typed.Core + +import Control.Monad +import Data.List +import Test.QuickCheck + +-- A couple of functions for checking the output of generators +progNodes :: Program f -> Int +progNodes = stmtsNodes . unProgram + +stmtsNodes :: Statements f -> Int +stmtsNodes = sum . map stmtNodes . unStatements + +stmtNodes :: Statement f -> Int +stmtNodes (ELet _ e) = 1 + exprNodes e +stmtNodes (EAssert e) = 1 + exprNodes e +stmtNodes (EFor _ _ _ stmts) = 1 + stmtsNodes stmts + +exprNodes :: Expr f a -> Int +exprNodes (EConst _) = 1 +exprNodes (EVar _) = 1 +exprNodes (EAppUnOp _ e) = 1 + exprNodes e +exprNodes (EAppBinOp _ e1 e2) = 1 + exprNodes e1 + exprNodes e2 +exprNodes (EIf e e1 e2) = 1 + exprNodes e + exprNodes e1 + exprNodes e2 + +progDepth :: Program f -> Int +progDepth = stmtsDepth . unProgram + +stmtsDepth :: Statements f -> Int +stmtsDepth = maximum . (0:) . map stmtDepth . unStatements + +stmtDepth :: Statement f -> Int +stmtDepth (ELet _ e) = 1 + exprDepth e +stmtDepth (EAssert e) = 1 + exprDepth e +stmtDepth (EFor _ _ _ stmts) = 1 + stmtsDepth stmts + +exprDepth :: Expr f a -> Int +exprDepth (EConst _) = 1 +exprDepth (EVar _) = 1 +exprDepth (EAppUnOp _ e) = 1 + exprDepth e +exprDepth (EAppBinOp _ e1 e2) = 1 + max (exprDepth e1) (exprDepth e2) +exprDepth (EIf e e1 e2) = 1 + max (exprDepth e) (max (exprDepth e1) (exprDepth e2)) + +data TestResult = TestResult { nodes :: Int + , depth :: Int + } + deriving (Show) + +runGen :: Int -> IO TestResult +runGen size = do + prog <- generate (resize size arbitrary) :: IO (Program (AField Rational)) + pure $ TestResult (progNodes prog) (progDepth prog) + +average :: (Real a, Fractional b) => [a] -> b +average xs = realToFrac (sum xs) / genericLength xs + +main :: IO () +main = do + let size = 1000 + let runs = 1000 :: Int + putStrLn $ "Requested runs: " ++ show runs + putStrLn $ "Requested size: " ++ show size + results <- forM [1 .. runs] $ \_ -> runGen size + let nodess = map nodes results + let depths = map depth results + let minn = minimum nodess + let maxn = maximum nodess + let avgn = average nodess :: Double + let maxd = maximum depths + let mind = minimum depths + let avgd = average depths :: Double + putStrLn "" + putStrLn $ "Minimum depth = " ++ show mind + putStrLn $ "Maximum depth = " ++ show maxd + putStrLn $ "Mean depth = " ++ show avgd + putStrLn "" + putStrLn $ "Minimum number of nodes = " ++ show minn + putStrLn $ "Maximum number of nodes = " ++ show maxn + putStrLn $ "Mean number of nodes = " ++ show avgn + putStrLn "" diff --git a/field/TinyLang/Field/Core.hs b/field/TinyLang/Field/Core.hs new file mode 100644 index 0000000..d44cd03 --- /dev/null +++ b/field/TinyLang/Field/Core.hs @@ -0,0 +1,19 @@ +-- | Basic structure of our programs + +module TinyLang.Field.Core + ( Program (..) + , Statements (..) + ) where + +import GHC.Generics +import Quiet + +-- | Basic wrapper of statements +newtype Statements stmt = Statements { unStatements :: [stmt] } + deriving (Generic, Eq, Functor, Foldable, Traversable) + deriving (Show) via (Quiet (Statements stmt)) + +-- | Basic wrapper of program +newtype Program stmt = Program { unProgram :: (Statements stmt) } + deriving (Generic, Eq, Functor, Foldable, Traversable) + deriving (Show) via (Quiet (Program stmt)) diff --git a/field/TinyLang/Field/Evaluator.hs b/field/TinyLang/Field/Evaluator.hs index ed66aa5..63614e5 100644 --- a/field/TinyLang/Field/Evaluator.hs +++ b/field/TinyLang/Field/Evaluator.hs @@ -1,9 +1,15 @@ -{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE QuasiQuotes #-} module TinyLang.Field.Evaluator ( EvalError (..) , MonadEvalError - , lookupVarEval + , EvalT + , Eval + , execEvalT + , execEval + , evalEvalT + , evalEval + , lookupVarM , invEval , divEval , atEval @@ -14,31 +20,41 @@ module TinyLang.Field.Evaluator , unpackPositiveDesc , packPositiveAsc , packPositiveDesc - , ExprWithEnv (..) + , ProgramWithEnv (..) , evalUnOp , evalBinOp , evalExprUni + , evalStatements + , evalStatement + , evalProgram + , evalProgWithEnv , evalExpr - , evalExprWithEnv , denoteUniConst , denoteSomeUniConst , denoteExpr , normExpr + , normStatement + , normStatements + , normProgram , instStatement , instExpr ) where import Prelude hiding (div) -import TinyLang.Environment import TinyLang.Field.Typed.Core import TinyLang.Prelude import qualified Data.String.Interpolate.IsString as QQ import qualified Data.Vector as Vector +import Data.Kind (Type) data TypeMismatch f = forall a b. TypeMismatch (UniVar f a) (UniConst f b) +instance TextField f => Show (TypeMismatch f) where + show (TypeMismatch (UniVar uniExp var) uniConstAct) = + [QQ.i|Variable #{var} has type #{uniExp}, but was instantiated with #{uniConstAct}|] + data EvalError f = VariableNotInScopeEvalError Var | IndexTooLargeEvalError Int @@ -53,12 +69,46 @@ data EvalError f type MonadEvalError f m = MonadError (EvalError f) m -instance TextField f => Show (TypeMismatch f) where - show (TypeMismatch (UniVar uniExp var) uniConstAct) = - [QQ.i|Variable #{var} has type #{uniExp}, but was instantiated with #{uniConstAct}|] - -lookupVarEval :: MonadEvalError g m => Var -> Env f -> m f -lookupVarEval var = fromOption (throwError $ VariableNotInScopeEvalError var) . lookupVar var +-- | Our evaluator transformer stack +newtype EvalT f (m :: Type -> Type) a = + EvalT { unEvalT :: ReaderT (Env (SomeUniConst f)) (StateT [SomeUniConst f] (ExceptT (EvalError f) m)) a } + deriving newtype ( Monad + , Functor + , Applicative + , MonadError (EvalError f) + , MonadState [SomeUniConst f] + , MonadReader (Env (SomeUniConst f)) + ) + +type Eval f a = EvalT f Identity a + +-- NOTE: that the result of evaluation will be reversed to preserve the order +-- | Run @EvalT@ and return its execution trace +execEvalT :: (Monad m) => EvalT f m a -> Env (SomeUniConst f) -> m (Either (EvalError f) [SomeUniConst f]) +execEvalT ev r = do + result <- runExceptT $ flip execStateT mempty $ flip runReaderT r $ unEvalT ev + pure $ second reverse result +-- | @execEvalT@ specialised for @Identity@ +execEval :: Eval f a -> Env (SomeUniConst f) -> Either (EvalError f) [SomeUniConst f] +execEval ev r = runIdentity $ execEvalT ev r + +-- | Run @EvalT@ and discard the trace +evalEvalT :: (Monad m) => EvalT f m a -> Env (SomeUniConst f) -> m (Either (EvalError f) a) +evalEvalT ev r = runExceptT $ flip evalStateT mempty $ flip runReaderT r $ unEvalT ev + +-- | @evalEvalT@ specialised to @Identity@ +evalEval :: Eval f a -> Env (SomeUniConst f) -> Either (EvalError f) a +evalEval ev = runIdentity . evalEvalT ev + +-- | lookup variable +lookupVarM :: (Monad m) => Var -> EvalT f m (SomeUniConst f) +lookupVarM var = do + env <- ask + fromOption (throwError $ VariableNotInScopeEvalError var) $ lookupVar var env + +-- | Bind a variable to @SomeUniConst@ in continuation +withVar :: (Monad m) => Var -> SomeUniConst f -> EvalT f m a -> EvalT f m a +withVar var uniConst = local (insertVar var uniConst) invEval :: (MonadEvalError g m, Field f) => f -> m f invEval = fromOption (throwError DivideByZeroEvalError) . inv @@ -66,7 +116,7 @@ invEval = fromOption (throwError DivideByZeroEvalError) . inv divEval :: (MonadEvalError g m, Field f) => f -> f -> m f divEval = fromOption (throwError DivideByZeroEvalError) .* div -atEval :: MonadEvalError g m => Int -> Vector a -> m a +atEval :: MonadEvalError f m => Int -> Vector a -> m a atEval i xs = fromOption (throwError $ IndexTooLargeEvalError i) $ xs Vector.!? i asIntegerEval :: (MonadEvalError f m, AsInteger f) => AField f -> m Integer @@ -97,29 +147,26 @@ packPositiveAsc = fst . foldl' (\(a, p) b -> (a + if b then p else 0, p * 2)) (0 packPositiveDesc :: [Bool] -> Integer packPositiveDesc = packPositiveAsc . reverse -normUniConst - :: forall f m a. (MonadEvalError f m, Field f, AsInteger f) - => UniConst f a -> m (UniConst f a) +normUniConst :: forall f m a. (Monad m, Field f, AsInteger f) + => UniConst f a -> EvalT f m (UniConst f a) normUniConst (UniConst Bool b) = return $ UniConst Bool b normUniConst (UniConst Field f) = return $ UniConst Field f normUniConst (UniConst Vector v) = UniConst Vector <$> normUnpacking v where normUnpacking = asIntegerEval . toField @(AField f) . packPositiveAsc >=> - fmap (Vector.fromList) . unpackPositiveAsc + fmap Vector.fromList . unpackPositiveAsc -- | We want to allow order comparisons on elements of the field, but only -- if they're integers (whatever that means), and only if they're positive. -- If we get a non-integer or a negative integer we throw an error. -compareIntegerValues - :: (MonadEvalError f m, AsInteger f) +compareIntegerValues :: (MonadEvalError f m, AsInteger f) => (Integer -> Integer -> Bool) -> AField f -> AField f -> m Bool compareIntegerValues op a b = do m <- asPositiveIntegerEval a n <- asPositiveIntegerEval b return $ m `op` n -evalUnOp - :: (MonadEvalError f m, Eq f, Field f, AsInteger f) +evalUnOp :: (MonadEvalError f m, Eq f, Field f, AsInteger f) => UnOp f a b -> a -> m (UniConst f b) evalUnOp Not = return . UniConst Bool . not evalUnOp Neq0 = return . UniConst Bool . (/= zer) @@ -127,8 +174,7 @@ evalUnOp Neg = return . UniConst Field . neg evalUnOp Inv = fmap (UniConst Field) . invEval evalUnOp Unp = asIntegerEval >=> fmap (UniConst Vector . Vector.fromList) . unpackPositiveAsc -evalBinOp - :: (MonadEvalError f m, Eq f, Field f, AsInteger f) +evalBinOp :: (MonadEvalError f m, Eq f, Field f, AsInteger f) => BinOp f a b c -> a -> b -> m (UniConst f c) evalBinOp Or x y = return . UniConst Bool $ x || y evalBinOp And x y = return . UniConst Bool $ x && y @@ -144,57 +190,72 @@ evalBinOp Mul x y = return . UniConst Field $ x `mul` y evalBinOp Div x y = UniConst Field <$> divEval x y evalBinOp BAt x y = asIntegerEval x >>= fmap (UniConst Bool) . flip atEval y . fromIntegral -evalStatementUni - :: (MonadEvalError f m, Eq f, Field f, AsInteger f) - => Env (SomeUniConst f) -> Statement f -> Expr f a -> m (UniConst f a) -evalStatementUni env (ELet (UniVar _ var) def) rest = do - defR <- evalExprUni env def - evalExprUni (insertVar var (Some defR) env) rest -evalStatementUni env (EAssert expr) rest = do - exprR <- evalExpr env expr - if exprR - then evalExprUni env rest - else throwError $ AssertionFailedEvalError expr +-- | Evaluate a program +evalProgram :: (Monad m, Eq f, Field f, AsInteger f) + => Program f -> EvalT f m () +evalProgram = flip evalStatements (pure ()) . unProgram + +-- TODO: Verify whether it is acutally right fold +evalStatements :: (Monad m, Eq f, Field f, AsInteger f) + => Statements f -> EvalT f m () -> EvalT f m () +evalStatements (Statements stmts) kont = foldr evalStatement kont stmts + +-- | Evaluate a single statement that continue as @kont@ +evalStatement :: (Monad m, Eq f, Field f, AsInteger f) + => Statement f -> EvalT f m () -> EvalT f m () +evalStatement (ELet (UniVar _ var) def) kont = do + defR <- evalExprUni def + let someDefR = Some defR + modify (someDefR:) + withVar var someDefR kont +evalStatement (EAssert expr) kont = do + exprR <- evalExpr expr + unless exprR $ throwError $ AssertionFailedEvalError expr + kont +evalStatement (EFor uniVar@(UniVar _ var) start end body) kont + -- TODO: Figure out if this is the right semantics + | start < end = + withVar var (Some $ fromIntegral start) $ + evalStatements body $ + evalStatement (EFor uniVar (start + 1) end body) kont + | otherwise = + let actualEnd = max start end in + withVar var (Some $ fromIntegral actualEnd) kont -- Note that we could use dependent maps, but we don't. -- | A recursive evaluator for expressions. Perhaps simplistic, but it works. -evalExprUni - :: (MonadEvalError f m, Eq f, Field f, AsInteger f) - => Env (SomeUniConst f) -> Expr f a -> m (UniConst f a) -evalExprUni _ (EConst uniConst) = normUniConst uniConst -evalExprUni env (EVar uniVar@(UniVar uni var)) = do - Some uniConst@(UniConst uni' _) <- lookupVarEval var env +evalExprUni :: (Monad m, Eq f, Field f, AsInteger f) + => Expr f a -> EvalT f m (UniConst f a) +evalExprUni (EConst uniConst) = normUniConst uniConst +evalExprUni (EVar uniVar@(UniVar uni var)) = do + Some uniConst@(UniConst uni' _) <- lookupVarM var let err = throwError . TypeMismatchEvalError $ TypeMismatch uniVar uniConst - withGeqUni uni uni' err $ evalExprUni env $ EConst uniConst -evalExprUni env (EIf e e1 e2) = do - eR <- evalExpr env e + withGeqUni uni uni' err $ evalExprUni $ EConst uniConst +evalExprUni (EIf e e1 e2) = do + eR <- evalExpr e if eR - then evalExprUni env e1 - else evalExprUni env e2 -evalExprUni env (EAppUnOp op e) = evalExpr env e >>= evalUnOp op -evalExprUni env (EAppBinOp op e1 e2) = do - e1R <- evalExpr env e1 - e2R <- evalExpr env e2 + then evalExprUni e1 + else evalExprUni e2 +evalExprUni (EAppUnOp op e) = evalExpr e >>= evalUnOp op +evalExprUni (EAppBinOp op e1 e2) = do + e1R <- evalExpr e1 + e2R <- evalExpr e2 evalBinOp op e1R e2R -evalExprUni env (EStatement stat expr) = evalStatementUni env stat expr -- | A recursive evaluator for expressions. -evalExpr - :: (MonadEvalError f m, Eq f, Field f, AsInteger f) - => Env (SomeUniConst f) -> Expr f a -> m a -evalExpr env = fmap _uniConstVal . evalExprUni env - --- | A type of expressions together with environments -data ExprWithEnv f - = ExprWithEnv (SomeUniExpr f) (Env (SomeUniConst f)) +evalExpr :: (Monad m, Eq f, Field f, AsInteger f) + => Expr f a -> EvalT f m a +evalExpr = fmap _uniConstVal . evalExprUni + +data ProgramWithEnv f + = ProgramWithEnv (Program f) (Env (SomeUniConst f)) deriving (Show) --- | Evaluate an expression in a given environment -evalExprWithEnv - :: (MonadEvalError f m, Eq f, Field f, AsInteger f) - => ExprWithEnv f -> m (SomeUniConst f) -evalExprWithEnv (ExprWithEnv (SomeOf uni expr) env) = - Some . UniConst uni <$> evalExpr env expr +-- | Evaluate a program in a given environment +evalProgWithEnv :: (Eq f, Field f, AsInteger f) + => ProgramWithEnv f -> Either (EvalError f) [SomeUniConst f] +evalProgWithEnv (ProgramWithEnv prog env) = + execEval (evalProgram prog) env denoteUniConst :: Field f => UniConst f a -> f denoteUniConst (UniConst Bool b) = toField b @@ -204,72 +265,97 @@ denoteUniConst (UniConst Vector v) = unAField . fromInteger . packPositiveAsc $ denoteSomeUniConst :: Field f => SomeUniConst f -> f denoteSomeUniConst = forget denoteUniConst -denoteExpr - :: (MonadEvalError f m, Eq f, Field f, AsInteger f) - => Env (SomeUniConst f) -> Expr f a -> m f -denoteExpr env = fmap denoteUniConst . evalExprUni env - -normStatement - :: (MonadEvalError f m, Eq f, Field f, AsInteger f) - => Env (SomeUniConst f) -> Statement f -> Expr f a -> m (Expr f a) -normStatement env (ELet (UniVar uni var) def) rest = do - defN <- normExpr env def +denoteExpr :: (Monad m, Eq f, Field f, AsInteger f) + => Expr f a -> EvalT f m f +denoteExpr = fmap denoteUniConst . evalExprUni + +-- | A recursive normalizer for programs. +normProgram :: (Monad m, Eq f, Field f, AsInteger f) + => Program f -> EvalT f m (Program f) +normProgram (Program stmts) = normStatements stmts (pure . Program) + +-- | A recursive normalizer for statements +normStatements :: (Monad m, Eq f, Field f, AsInteger f) + => Statements f -> (Statements f -> EvalT f m r) -> EvalT f m r +normStatements (Statements []) kont = kont $ Statements [] +normStatements (Statements (s:rest)) kont = normStatement s $ \case + Nothing -> normStatements (Statements rest) kont + Just sN -> normStatements (Statements rest) $ \ (Statements restN) -> + kont $ Statements $ sN : restN + +-- | Normalise single statement +normStatement :: (Monad m, Eq f, Field f, AsInteger f) + => Statement f -> (Maybe (Statement f) -> EvalT f m r) -> EvalT f m r +normStatement (ELet uniVar@(UniVar _ var) def) kont = do + defN <- normExpr def case defN of - EConst uniConst -> normExpr (insertVar var (Some uniConst) env) rest - _ -> EStatement (ELet (UniVar uni var) defN) <$> normExpr env rest -normStatement env (EAssert expr) rest = do - exprN <- normExpr env expr - EStatement (EAssert exprN) <$> normExpr env rest - --- | A recursive normalizer for expressions. -normExpr - :: (MonadEvalError f m, Eq f, Field f, AsInteger f) - => Env (SomeUniConst f) -> Expr f a -> m (Expr f a) -normExpr _ (EConst uniConst) = EConst <$> normUniConst uniConst -normExpr env expr@(EVar uniVar@(UniVar uni var)) = + EConst uniConst -> + withVar var (Some uniConst) $ kont Nothing + _ -> + kont . Just $ ELet uniVar defN +normStatement (EAssert expr) kont = do + exprN <- normExpr expr + case exprN of + EConst (UniConst _ False) -> throwError $ AssertionFailedEvalError expr + EConst (UniConst _ True) -> kont Nothing + _ -> kont . Just $ EAssert exprN +normStatement (EFor uniVar@(UniVar _ var) start end body) kont = + normStatements body $ \bodyN -> + let actualEnd = max start end in + withVar var (Some $ fromIntegral actualEnd) $ case bodyN of + Statements [] -> kont Nothing + _ -> kont . Just $ EFor uniVar start end bodyN + +normExpr :: (Monad m, Eq f, Field f, AsInteger f) + => Expr f a -> EvalT f m (Expr f a) +normExpr (EConst uniConst) = EConst <$> normUniConst uniConst +normExpr expr@(EVar uniVar@(UniVar uni var)) = do + env <- ask case lookupVar var env of Nothing -> return expr Just (Some uniConst@(UniConst uni' _)) -> do let err = throwError . TypeMismatchEvalError $ TypeMismatch uniVar uniConst - withGeqUni uni uni' err $ normExpr env $ EConst uniConst -normExpr env (EIf e e1 e2) = do - eN <- normExpr env e - let nE1 = normExpr env e1 - nE2 = normExpr env e2 + withGeqUni uni uni' err $ normExpr $ EConst uniConst +normExpr (EIf e e1 e2) = do + eN <- normExpr e + let nE1 = normExpr e1 + nE2 = normExpr e2 case eN of EConst (UniConst Bool b) -> if b then nE1 else nE2 - _ -> EIf eN <$> nE1 <*> nE2 -normExpr env (EAppUnOp op e) = do - eN <- normExpr env e + _ -> EIf eN <$> nE1 <*> nE2 +normExpr (EAppUnOp op e) = do + eN <- normExpr e case eN of EConst (UniConst _ x) -> EConst <$> evalUnOp op x - _ -> return $ EAppUnOp op eN -normExpr env (EAppBinOp op e1 e2) = do - e1N <- normExpr env e1 - e2N <- normExpr env e2 + _ -> return $ EAppUnOp op eN +normExpr(EAppBinOp op e1 e2) = do + e1N <- normExpr e1 + e2N <- normExpr e2 case (e1N, e2N) of (EConst (UniConst _ x1), EConst (UniConst _ x2)) -> EConst <$> evalBinOp op x1 x2 - _ -> + _ -> return $ EAppBinOp op e1N e2N -normExpr env (EStatement stat expr) = normStatement env stat expr -- | Instantiate some of the variables of a statement with values. -instStatement - :: MonadEvalError f m => Env (SomeUniConst f) -> Statement f -> m (Statement f) -instStatement env (ELet uniVar def) = ELet uniVar <$> instExpr env def -instStatement env (EAssert expr) = EAssert <$> instExpr env expr +instStatement :: Monad m => Statement f -> EvalT f m (Statement f) +instStatement (ELet uniVar def) = ELet uniVar <$> instExpr def +instStatement (EAssert expr) = EAssert <$> instExpr expr +instStatement (EFor uniVar start end stmts) = EFor uniVar start end <$> instStatements stmts + +instStatements :: Monad m => Statements f -> EvalT f m (Statements f) +instStatements = traverse instStatement -- | Instantiate some of the variables of an expression with values. -instExpr :: MonadEvalError f m => Env (SomeUniConst f) -> Expr f a -> m (Expr f a) -instExpr _ expr@(EConst _) = return expr -instExpr env expr@(EVar uniVar@(UniVar uni var)) = +instExpr :: Monad m => Expr f a -> EvalT f m (Expr f a) +instExpr expr@(EConst _) = return expr +instExpr expr@(EVar uniVar@(UniVar uni var)) = do + env <- ask case lookupVar var env of Nothing -> return expr Just (Some uniConst@(UniConst uni' _)) -> do let err = throwError . TypeMismatchEvalError $ TypeMismatch uniVar uniConst withGeqUni uni uni' err $ return $ EConst uniConst -instExpr env (EIf e e1 e2) = EIf <$> instExpr env e <*> instExpr env e1 <*> instExpr env e2 -instExpr env (EAppUnOp op e) = EAppUnOp op <$> instExpr env e -instExpr env (EAppBinOp op e1 e2) = EAppBinOp op <$> instExpr env e1 <*> instExpr env e2 -instExpr env (EStatement stat expr) = EStatement <$> instStatement env stat <*> instExpr env expr +instExpr (EIf e e1 e2) = EIf <$> instExpr e <*> instExpr e1 <*> instExpr e2 +instExpr (EAppUnOp op e) = EAppUnOp op <$> instExpr e +instExpr (EAppBinOp op e1 e2) = EAppBinOp op <$> instExpr e1 <*> instExpr e2 diff --git a/field/TinyLang/Field/Generator.hs b/field/TinyLang/Field/Generator.hs index 9be8bbf..e00ac56 100644 --- a/field/TinyLang/Field/Generator.hs +++ b/field/TinyLang/Field/Generator.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} {- | NOTE: comparisons. @@ -28,12 +29,15 @@ import TinyLang.Field.Evaluator import TinyLang.Field.Typed.Core import qualified Data.IntMap.Strict as IntMap +import Data.Kind import qualified Data.Vector as Vector import QuickCheck.GenT -import Test.QuickCheck hiding (elements, frequency, - oneof, sized) +import Test.QuickCheck (Arbitrary, Gen, arbitrary, + arbitrarySizedBoundedIntegral, + shrink, shrinkList) import Test.QuickCheck.Instances.Vector () + -- Our generators all run in such an @m@ that @MonadGen m@ and -- @MonadSupply m@ are satisfied for it, so that we can generate fresh -- variables. The final @Arbitrary@ instances call @runSupplyGenT@ to get @@ -121,8 +125,8 @@ instance KnownUni f a => Arbitrary (DefaultUniVar f a) where arbitrary = DefaultUniVar <$> chooseUniVar defaultVars -- | Generate a universe and feed it to the continuation. -withOneofUnis :: MonadGen m => (forall a. KnownUni f a => Uni f a -> m b) -> m b -withOneofUnis k = oneof [k Bool, k Field] +withOneOfUnis :: MonadGen m => (forall a. KnownUni f a => Uni f a -> m b) -> m b +withOneOfUnis k = oneof [k Bool, k Field] -- We define this as a separate function, because the @Arbitrary@ instance of @UniConst@ requires -- @KnownUni f a@ and we do not need this constraint in the shrinker, which we reuse in the @@ -150,7 +154,7 @@ instance (KnownUni f a, Field f, Arbitrary f) => Arbitrary (UniConst f a) where shrink = shrinkUniConst instance (Field f, Arbitrary f) => Arbitrary (SomeUniConst f) where - arbitrary = withOneofUnis $ \(_ :: Uni f a) -> Some <$> arbitrary @(UniConst f a) + arbitrary = withOneOfUnis $ \(_ :: Uni f a) -> Some <$> arbitrary @(UniConst f a) shrink (Some uniConst) = Some <$> shrinkUniConst uniConst @@ -172,10 +176,9 @@ instance (Field f, Arbitrary f) => Arbitrary (SomeUniConst f) where -- Note that @b@ is bound outside of the continuation and @a@ is bound inside. -- This means that the caller decides values of what type the generated operator must return, -- but the caller does not care about the type of argument and so we can pick any. -withOneofUnOps - :: forall f b m r. (KnownUni f b, MonadGen m) +withOneOfUnOps :: forall f b m r. (KnownUni f b, MonadGen m) => (forall a. KnownUni f a => UnOp f a b -> m r) -> m r -withOneofUnOps k = oneof $ case knownUni @f @b of +withOneOfUnOps k = oneof $ case knownUni @f @b of Bool -> [k Not, k Neq0] Field -> [k Neg, k Inv] Vector -> [k Unp] @@ -184,10 +187,9 @@ withOneofUnOps k = oneof $ case knownUni @f @b of -- Note that @c@ is bound outside of the continuation and @a@ and @b@ are bound inside. -- This means that the caller decides values of what type the generated operator must return, -- but the caller does not care about the type of arguments and so we can pick any. -withOneofBinOps - :: forall f c m d. (Field f, Arbitrary f, KnownUni f c, KnownUni f d, MonadGen m) +withOneOfBinOps :: forall f c m d. (Field f, Arbitrary f, KnownUni f c, KnownUni f d, MonadGen m) => (forall a b. (KnownUni f a, KnownUni f b) => BinOp f a b c -> m (Expr f d)) -> m (Expr f d) -withOneofBinOps k = case knownUni @f @c of +withOneOfBinOps k = case knownUni @f @c of Bool -> frequency $ map ((,) 16) [k Or, k And, k Xor, k FEq] ++ map ((,) 1) [k FLt, k FLe, k FGe, k FGt, k BAt] @@ -197,16 +199,16 @@ withOneofBinOps k = case knownUni @f @c of Vector -> EConst <$> arbitraryM -- | Generate a comparison operator and feed it to the continuation. -withOneofComparisons +withOneOfComparisons :: forall f m r. MonadGen m => (BinOp f (AField f) (AField f) Bool -> m r) -> m r -withOneofComparisons k = oneof [k FLt, k FLe, k FGe, k FGt] +withOneOfComparisons k = oneof [k FLt, k FLe, k FGe, k FGt] -- | Generate a binary operator that can be turned into an assertion and feed it to the continuation. -withOneofBinAsserts +withOneOfBinAsserts :: forall f m r. MonadGen m => (forall a. KnownUni f a => BinOp f a a Bool -> m r) -> m r -withOneofBinAsserts k = oneof [k Or, k And, k Xor, k FEq, k FLt, k FLe, k FGe, k FGt] +withOneOfBinAsserts k = oneof [k Or, k And, k Xor, k FEq, k FLt, k FLe, k FGe, k FGt] -- | An arbitrary integer value (for use in comparisons) arbitraryValI :: (Field f, MonadGen m) => m (UniConst f (AField f)) @@ -228,69 +230,116 @@ arbitraryUnOpRing = elements [Neg] arbitraryBinOpRing :: MonadGen m => m (BinOp f (AField f) (AField f) (AField f)) arbitraryBinOpRing = elements [Add, Sub, Mul] -groundArbitraryFreqs - :: (Field f, Arbitrary f, KnownUni f a, MonadGen m) +groundArbitraryFreqs :: (Field f, Arbitrary f, KnownUni f a, MonadGen m) => Vars f -> [(Int, m (Expr f a))] groundArbitraryFreqs vars = [ (1, EConst <$> arbitraryM) , (2, EVar <$> chooseUniVar vars) ] --- | Generate an expression of a particular type from a collection of variables +newtype SGenT f (m :: Type -> Type) a = + SGen { unSGenT :: GenT (SupplyT (StateT (Vars f) m)) a } + deriving newtype ( Monad + , Functor + , Applicative + , MonadSupply + , MonadState (Vars f) + , MonadGen + ) + +-- TODO: Is there a way to automate this? +instance MonadState s m => MonadState s (GenT m) where + get = lift get + put = lift . put + state = lift . state + + +type SGen f a = SGenT f Identity a + +-- Not sure if this is the right type +runSGenT :: (Monad m) => Vars f -> SGenT f m a -> Gen (m a) +runSGenT vars = fmap ((`evalStateT` vars) . runSupplyT) . runGenT . unSGenT + +runSGen :: Vars f -> SGen f a -> Gen a +runSGen vars = fmap runIdentity . runSGenT vars + +boundedArbitraryStmts :: forall m f. (Field f, Arbitrary f, MonadGen m, MonadSupply m, MonadState (Vars f) m) + => Int -> m (Statements f) +boundedArbitraryStmts size = + Statements <$> frequency [ (1, pure []) + , (10, arbStmts) + ] + where + arbStmts = do + numStmts :: Int <- choose (1, size) + let perStmtSize = size `Prelude.div` numStmts + resize numStmts $ listOf $ boundedArbitraryStmt perStmtSize + +boundedArbitraryStmt :: forall m f. (Field f, Arbitrary f, MonadGen m, MonadSupply m, MonadState (Vars f) m) + => Int -> m (Statement f) +boundedArbitraryStmt size + | size <= 1 = do + vars <- get + EAssert <$> boundedArbitraryExpr vars size + | otherwise = frequency stmtGens where + stmtGens = [ (3, withOneOfUnis $ \(_ :: Uni f a') -> do + vars <- get + uniVar <- genFreshUniVar @f @a' + let vars' = Some uniVar : vars + size' = size - 1 + put vars' + ELet uniVar <$> boundedArbitraryExpr vars' size') + -- Generate a completely random assertion (unlikely to hold) + , (1, do + vars <- get + EAssert <$> boundedArbitraryExpr vars size) + -- generate a valid (but necessarily holding) contraint + , (1, do + let size' = size - 1 + vars <- get + EAssert <$> boundedArbitraryComparisons vars size') + -- generate an assertion of form @x binOp x@ + , (1, withOneOfBinAsserts $ \binOp -> do + let size' = size `Prelude.div` 2 + vars <- get + x <- boundedArbitraryExpr vars size' + pure $ EAssert $ EAppBinOp binOp x x) + -- generate a for loop + , (1, do + uniVar <- genFreshUniVar @f @(AField f) + modify' (Some uniVar :) + start <- arbitraryM + let size' = size - 1 + -- NOTE: we also include end < start cases + end = choose (start - 5, start + 10) + EFor uniVar start <$> end <*> boundedArbitraryStmts size') + ] + +-- | Generate an expression of a particular type from a collection of variablesf -- with the number of nodes (approximately) bounded by 'size'. -boundedArbitraryExpr - :: (Field f, Arbitrary f, KnownUni f a, MonadGen m, MonadSupply m) +boundedArbitraryExpr :: forall m f a. (Field f, Arbitrary f, KnownUni f a, MonadGen m, MonadSupply m) => Vars f -> Int -> m (Expr f a) -boundedArbitraryExpr vars0 size0 = go vars0 size0 where - go :: forall f a m. (Field f, Arbitrary f, KnownUni f a, MonadGen m, MonadSupply m) - => Vars f -> Int -> m (Expr f a) - go vars size | size <= 1 = frequency $ groundArbitraryFreqs vars - go vars size = frequency everything where - everything = groundArbitraryFreqs vars ++ recursive ++ comparisons (size `Prelude.div` 2) +boundedArbitraryExpr vars size + | size <= 1 = frequency $ groundArbitraryFreqs vars + | otherwise = frequency everything where + everything = groundArbitraryFreqs vars ++ expressions ++ comparisons (size `Prelude.div` 2) -- The most general generator. - recursive = + expressions = [ (2, do let size' = size `Prelude.div` 3 EIf - <$> go vars size' - <*> go vars size' - <*> go vars size') - , (4, withOneofUnis $ \(_ :: Uni f a') -> do - uniVar <- genFreshUniVar @f @a' - let vars' = Some uniVar : vars - size' = size `Prelude.div` 2 - EStatement . ELet uniVar - <$> go vars size' - <*> go vars' size') - , (2, withOneofUnOps $ \unOp -> do + <$> boundedArbitraryExpr vars size' + <*> boundedArbitraryExpr vars size' + <*> boundedArbitraryExpr vars size') + , (2, withOneOfUnOps $ \unOp -> do let size' = size - 1 - EAppUnOp unOp <$> go vars size') - , (4, withOneofBinOps $ \binOp -> do + EAppUnOp unOp <$> boundedArbitraryExpr vars size') + , (4, withOneOfBinOps $ \binOp -> do let size' = size `Prelude.div` 2 EAppBinOp binOp - <$> go vars size' - <*> go vars size') - , (round $ fromIntegral size / fromIntegral size0 * (4 :: Double), frequency - [ (4, do - -- Generates valid (but not necessarily holding) range constraints. - let size' = size `Prelude.div` 3 - EStatement . EAssert - <$> boundedArbitraryComparisons vars size' - <*> go vars size') - , (4, withOneofBinAsserts $ \binOp -> do - -- Generates assertions of the @x op x@ form. - let size' = size `Prelude.div` 2 - x <- go vars size' - EStatement (EAssert $ EAppBinOp binOp x x) - <$> go vars size') - , (4, do - let size' = size `Prelude.div` 2 - -- Generates assertions that are unlikely to hold. - EStatement . EAssert - <$> go vars size' - <*> go vars size') - ]) + <$> boundedArbitraryExpr vars size' + <*> boundedArbitraryExpr vars size') ] -- A generator of comparisons. @@ -298,11 +347,10 @@ boundedArbitraryExpr vars0 size0 = go vars0 size0 where Bool -> [(2, boundedArbitraryComparisons vars size')] _ -> [] -boundedArbitraryComparisons - :: (Field f, Arbitrary f, MonadGen m, MonadSupply m) +boundedArbitraryComparisons :: (Field f, Arbitrary f, MonadGen m, MonadSupply m) => Vars f -> Int -> m (Expr f Bool) boundedArbitraryComparisons vars size' = - withOneofComparisons $ \comp -> + withOneOfComparisons $ \comp -> EAppBinOp comp <$> boundedArbitraryExprI vars size' <*> boundedArbitraryExprI vars size' @@ -337,13 +385,6 @@ boundedArbitraryExprI vars size = frequency <$> boundedArbitraryExpr vars size' <*> boundedArbitraryExprI vars size' <*> boundedArbitraryExprI vars size') - , (2, do - uniVar <- genFreshUniVar - let vars' = Some uniVar : vars - size' = size `Prelude.div` 2 - EStatement . ELet uniVar - <$> boundedArbitraryExprI vars size' - <*> boundedArbitraryExprI vars' size') , (2, do let size' = size - 1 EAppUnOp @@ -379,15 +420,63 @@ defaultUniConst :: forall f a. (KnownUni f a, Field f) => UniConst f a defaultUniConst = UniConst uni $ case uni of Bool -> True - Field -> fromInteger 101 + Field -> 101 Vector -> Vector.fromList [False, True, True, True, False, False, True] where uni = knownUni @f @a +instance (Field f, Arbitrary f) => Arbitrary (Program f) where + arbitrary = Program <$> arbitrary + shrink = fmap Program . shrink . unProgram + +instance (Field f, Arbitrary f) => Arbitrary (Statements f) where + arbitrary = runSGen vars stmtsGen where + vars = defaultVars + stmtsGen = sized $ \size -> do + adjustUniquesForVars vars + boundedArbitraryStmts size + + shrink (Statements stmts) = + Statements <$> concat + [shrunkEmpty, shrunkNorm, shrunkPreserving, shrunkNonPreserving] where + + shrunkEmpty :: [[Statement f]] + shrunkEmpty = case stmts of + [] -> [] + _ -> [[]] + + -- normalisation steps when shrinking + shrunkNorm :: [[Statement f]] + shrunkNorm = maybe [] pure $ norm stmts + + -- small step "normaliser" + norm :: [Statement f] -> Maybe [Statement f] + norm ((EFor forVar start end (Statements [])) : restStmts) = + pure $ ELet forVar (EConst (fromInteger (max start end))) : restStmts + norm ((EAssert (EConst (UniConst _ True))) : restStmts) = + pure restStmts + norm (stmt : restStmts) = (stmt :) <$> norm restStmts + -- no normalisations performed, abort + norm [] = Nothing + + -- preserves the structure of statements + shrunkPreserving :: [[Statement f]] + shrunkPreserving = shrinkElements shrink stmts + -- does not preserve the structure of statements + shrunkNonPreserving :: [[Statement f]] + shrunkNonPreserving = shrinkList shrink stmts + +-- A modified shrinkList, that preserves the structure of the underlying list +shrinkElements :: (a -> [a]) -> [a] -> [[a]] +shrinkElements shr = shrinkOne where + shrinkOne [] = [] + shrinkOne (x:xs) = [ x':xs | x' <- shr x ] + ++ [ x:xs' | xs' <- shrinkOne xs ] + -- We do not provide an implementation for 'arbitrary' (because we don't need it and it'd be -- annoying to write it), but we still want to make provide an 'Arbitrary' instance, so that --- 'shrink' can be used in the 'Arbitrary' instance of 'Expr' (a separately provided --- 'shrinkStatement' wouldn't work, because we want to shrink a pair of values, see the instance). +-- 'shrink' can be used in the 'Arbitrary' instance of 'Statments' (a separately provided +-- 'shrinkStatement' could also work). instance (Field f, Arbitrary f) => Arbitrary (Statement f) where arbitrary = error "Panic: no implementation of 'arbitrary' for 'Statement'" @@ -396,7 +485,10 @@ instance (Field f, Arbitrary f) => Arbitrary (Statement f) where -- (which most of the time will break the assertion) we should shrink @lhs == rhs@ to -- @lhs' == lhs'@ or @rhs' == rhs'@ where @lhs'@ and @rhs'@ are shrunk version of -- @lhs@ and @rhs@ respectively (just to have some shrinking that does not break the assertion). - shrink (EAssert expr) = EAssert <$> shrink expr + shrink (EAssert expr) = EAssert <$> shrink expr + -- NOTE: Revisit different strategy for shrink end if test performance degrades + shrink (EFor uniVar start end stmts) = efor <$> shrink (start, end, stmts) where + efor (a, b, c) = EFor uniVar a b c instance (KnownUni f a, Field f, Arbitrary f) => Arbitrary (Expr f a) where arbitrary = runSupplyGenT . sized $ \size -> do @@ -420,42 +512,22 @@ instance (KnownUni f a, Field f, Arbitrary f) => Arbitrary (Expr f a) where EIf e e1 e2 -> e1 : e2 : (uncurry (uncurry EIf) <$> shrink ((e, e1), e2)) EConst _ -> [] EVar _ -> [] - -- TODO: we can safely drop an assertion and we can drop a let-expression when - -- the let-bound variable is not used in @expr@. - EStatement stat expr -> uncurry EStatement <$> shrink (stat, expr) - --- An instance that QuickCheck can use for tests. -instance (Field f, Arbitrary f) => Arbitrary (SomeUniExpr f) where - arbitrary = withOneofUnis $ \uni -> SomeOf uni <$> arbitrary - - shrink (SomeOf uni0 expr) = - map (SomeOf uni0) (withKnownUni uni0 $ shrink expr) ++ case expr of - EAppUnOp op e -> withUnOpUnis op $ \argUni _ -> [SomeOf argUni e] - EAppBinOp op e1 e2 -> - withBinOpUnis op $ \uni1 uni2 _ -> - [SomeOf uni1 e1, SomeOf uni2 e2] - EIf e _ _ -> [SomeOf Bool e] - EConst _ -> [] - EVar _ -> [] - EStatement stat _ -> case stat of - ELet (UniVar uni _) def -> [SomeOf uni def] - EAssert e -> [SomeOf Bool e] - -genEnvFromVarSigns :: (Field f, Arbitrary f) => Env (VarSign f) -> Gen (Env (SomeUniConst f)) -genEnvFromVarSigns = - traverse $ \(VarSign _ (uni :: Uni f a)) -> + + +genEnvFromVarSigs :: (Field f, Arbitrary f) => Env (VarSig f) -> Gen (Env (SomeUniConst f)) +genEnvFromVarSigs = + traverse $ \(VarSig _ (uni :: Uni f a)) -> Some <$> withKnownUni uni (arbitrary :: Gen (UniConst f a)) --- | Generate a random ExprWithEnv. Note that you can say things like --- "generate (resize 1000 arbitrary :: Gen (ExprWithEnv F17))" to get --- bigger expressions. There's no means provided to generate things --- over non-default sets of variables, but this would be easy to do. -instance (Field f, Arbitrary f) => Arbitrary (ExprWithEnv f) where +-- | Generate a random ProgramWithEnv. Note that you can say things like +-- "generate (resize 1000 arbitrary :: Gen (ProgramWithEnv F17))" to get bigger +-- expressions. There's no means provided to generate things over non-default +-- sets of variables, but this would be easy to do. +instance (Field f, Arbitrary f) => Arbitrary (ProgramWithEnv f) where arbitrary = do - someUniExpr <- arbitrary - vals <- forget (genEnvFromVarSigns . exprFreeVarSigns) someUniExpr - return $ ExprWithEnv someUniExpr vals - shrink (ExprWithEnv someUniExpr (Env vals)) = - -- TODO: test me. - flip map (shrink someUniExpr) $ \shrunk@(SomeOf _ expr) -> - ExprWithEnv shrunk . Env . IntMap.intersection vals . unEnv $ exprFreeVarSigns expr + prog <- arbitrary + vals <- genEnvFromVarSigs . progFreeVarSigs $ prog + return $ ProgramWithEnv prog vals + shrink (ProgramWithEnv prog (Env vals)) = + flip map (shrink prog) $ \shrunk -> + ProgramWithEnv shrunk . Env . IntMap.intersection vals . unEnv $ progFreeVarSigs shrunk diff --git a/field/TinyLang/Field/Printer.hs b/field/TinyLang/Field/Printer.hs index 9f2ea6c..6541f90 100644 --- a/field/TinyLang/Field/Printer.hs +++ b/field/TinyLang/Field/Printer.hs @@ -2,6 +2,9 @@ module TinyLang.Field.Printer ( PrintStyle (..) , exprToString , someExprToString + , stmtToString + , stmtsToString + , progToString ) where import TinyLang.Prelude @@ -61,14 +64,34 @@ toStringUniConst (UniConst Field i) = showField i toStringUniConst (UniConst Vector v) = "{" ++ intercalate "," (map toStringBool $ Vector.toList v) ++ "}" -statementToString :: TextField f => PrintStyle -> Statement f -> String -statementToString s (ELet (UniVar _ var) def) = concat +stmtToString :: TextField f => PrintStyle -> Statement f -> String +stmtToString s (ELet (UniVar _ var) def) = concat [ "let " , toStringVar s var , " = " , exprToString s def + , ";" ] -statementToString s (EAssert expr) = "assert " ++ exprToString s expr + +stmtToString s (EAssert expr) = "assert " ++ exprToString s expr ++ ";" +stmtToString s (EFor (UniVar _ var) start end stmts) = concat + [ "for " + , toStringVar s var + , " = " + , show start + , " to " + , show end + , " do\n" + , unlines $ map (stmtToString s) $ unStatements stmts + , "end" + , ";" + ] + +stmtsToString :: TextField f => PrintStyle -> (Statements f) -> String +stmtsToString ps = unlines . (map (stmtToString ps)) . unStatements + +progToString :: TextField f => PrintStyle -> Program f -> String +progToString ps = stmtsToString ps . unProgram -- Main function exprToString :: TextField f => PrintStyle -> Expr f a -> String @@ -84,11 +107,6 @@ exprToString s (EIf e e1 e2) = concat , " else " , exprToString1 s e2 ] -exprToString s (EStatement stat e) = concat - [ statementToString s stat - , "; " - , exprToString s e - ] someExprToString :: TextField f => PrintStyle -> SomeUniExpr f -> String someExprToString s = forget $ exprToString s diff --git a/field/TinyLang/Field/Raw/Core.hs b/field/TinyLang/Field/Raw/Core.hs index 8d69c3d..2404fd0 100644 --- a/field/TinyLang/Field/Raw/Core.hs +++ b/field/TinyLang/Field/Raw/Core.hs @@ -7,11 +7,20 @@ module TinyLang.Field.Raw.Core , BinOp(..) , UnOp(..) , Statement(..) - , RawExpr + , Program + , pattern C.Program + , C.unProgram + , Statements + , pattern C.Statements + , C.unStatements + , RawProgram + , RawStatements , RawStatement + , RawExpr ) where import TinyLang.Field.UniConst +import qualified TinyLang.Field.Core as C import GHC.Generics import Quiet @@ -24,16 +33,37 @@ newtype Var = Var { unVar :: Identifier } deriving (Eq, Generic) deriving (Show) via (Quiet Var) +{-| In our AST we have the following + +* @Program v f@, + +* @Statements v f@, + +* @Statement v f@ and +At the moment @Program v f@ is a newtype wrapper around @Statements v f@, and +@Statements v f@ is a newtype wrapper around @[Statement v f]@. -{-| @Expr v f@ is parameterised by the type of variable @v@. +We specify those wrappers as some operations work on the program level, some +operations work on the statements level, and some operations work on the +statement level; the operations acting on statement level are not necessarily +mappable over a list of statements. -} + +type Program v f = C.Program (Statement v f) +type Statements v f = C.Statements (Statement v f) + +data Statement v f + = ELet v (Expr v f) + | EAssert (Expr v f) + | EFor v Integer Integer (Statements v f) + deriving (Show) + data Expr v f = EConst (SomeUniConst f) | EVar v | EAppBinOp BinOp (Expr v f) (Expr v f) | EAppUnOp UnOp (Expr v f) - | EStatement (Statement v f) (Expr v f) | EIf (Expr v f) (Expr v f) (Expr v f) | ETypeAnn (SomeUni f) (Expr v f) deriving (Show) @@ -62,14 +92,9 @@ data UnOp | Unp deriving (Show) -data Statement v f - = ELet v (Expr v f) - | EAssert (Expr v f) - | EFor v Integer Integer [Statement v f] - deriving (Show) - {-| = Utility Type Aliases -} -type RawExpr = Expr Var -type RawStatement = Statement Var - +type RawProgram f = Program Var f +type RawStatements f = Statements Var f +type RawStatement f = Statement Var f +type RawExpr f = Expr Var f diff --git a/field/TinyLang/Field/Raw/Parser.hs b/field/TinyLang/Field/Raw/Parser.hs index c3ad874..ce256be 100644 --- a/field/TinyLang/Field/Raw/Parser.hs +++ b/field/TinyLang/Field/Raw/Parser.hs @@ -1,3 +1,4 @@ +{-# OPTIONS_GHC -fno-warn-orphans #-} {-| = Raw Parser @@ -132,7 +133,7 @@ prefix-op ::= == Statement -Statements are a bit odd at the moment, as they are neither +Program are a bit odd at the moment, as they are neither expressions nor the usual statements. @ @@ -183,6 +184,12 @@ import Text.Megaparsec.Char type ParserT = ParsecT Void String +{-| == IsString instances +-} + +instance TextField f => IsString (RawProgram f) where + fromString = either error id . parseString (pTop @f) "" + {-| == Lexer -} @@ -336,16 +343,14 @@ pTerm = [ try (EConst <$> pConst) -- This can backtrack for keywords , try (EVar <$> pVar) - , EStatement <$> (pStatement <* symbol ";") - <*> pExpr , EIf <$> (keyword "if" *> pExpr) <*> (keyword "then" *> pExpr) <*> (keyword "else" *> pExpr) , parens pExpr ] -pStatements :: Field f => ParserT m [RawStatement f] -pStatements = many (pStatement <* symbol ";") +pExpr :: Field f => ParserT m (RawExpr f) +pExpr = Comb.makeExprParser pTerm operatorTable pStatement :: Field f => ParserT m (RawStatement f) pStatement = @@ -362,8 +367,16 @@ pStatement = <* keyword "end" ] -pExpr :: Field f => ParserT m (RawExpr f) -pExpr = Comb.makeExprParser pTerm operatorTable +pStatements :: Field f => ParserT m (RawStatements f) +pStatements = + choice + -- This can backtrack for statement starting with a "(" + [ try (parens pStatements) + , Statements <$> many (pStatement <* symbol ";") + ] + +pProgram :: Field f => ParserT m (RawProgram f) +pProgram = Program <$> pStatements -pTop :: Field f => ParserT m (RawExpr f) -pTop = top pExpr +pTop :: Field f => ParserT m (RawProgram f) +pTop = top pProgram diff --git a/field/TinyLang/Field/Rename.hs b/field/TinyLang/Field/Rename.hs index e806952..5bf49b9 100644 --- a/field/TinyLang/Field/Rename.hs +++ b/field/TinyLang/Field/Rename.hs @@ -1,15 +1,17 @@ module TinyLang.Field.Rename - ( renameExpr + ( renameProgram ) where import TinyLang.Prelude import TinyLang.Field.Typed.Core -renameExpr :: MonadSupply m => Expr f a -> m (Expr f a) -renameExpr expr = do - supplyFromAtLeastFree expr - runRenameM $ renameExprM expr +import Control.Monad.Cont + +renameProgram :: MonadSupply m => Program f -> m (Program f) +renameProgram (Program stmts) = do + stmtsSupplyFromAtLeastFree stmts + Program <$> runRenameM (withRenamedStatementsM stmts pure) type RenameM = ReaderT (Env Unique) Supply @@ -17,9 +19,9 @@ runRenameM :: MonadSupply m => RenameM a -> m a runRenameM a = liftSupply $ runReaderT a mempty withFreshenedVar :: Var -> (Var -> RenameM c) -> RenameM c -withFreshenedVar var cont = do +withFreshenedVar var kont = do uniqNew <- freshUnique - local (insertVar var uniqNew) . cont $ setUnique uniqNew var + local (insertVar var uniqNew) . kont $ setUnique uniqNew var renameVarM :: Var -> RenameM Var renameVarM var = do @@ -28,11 +30,23 @@ renameVarM var = do Nothing -> var Just uniq -> setUnique uniq var +-- TODO: Add unit tests for renaming withRenamedStatementM :: Statement f -> (Statement f -> RenameM c) -> RenameM c -withRenamedStatementM (ELet (UniVar uni var) def) cont = do +withRenamedStatementM (ELet (UniVar uni var) def) kont = do defRen <- renameExprM def - withFreshenedVar var $ \varFr -> cont $ ELet (UniVar uni varFr) defRen -withRenamedStatementM (EAssert expr) cont = renameExprM expr >>= cont . EAssert + -- Note that @var@ is not in scope in @def@. + withFreshenedVar var $ \varFr -> kont $ ELet (UniVar uni varFr) defRen +withRenamedStatementM (EAssert expr) kont = renameExprM expr >>= kont . EAssert +withRenamedStatementM (EFor (UniVar uni var) start end stmts) kont = + withFreshenedVar var $ \varFr -> + withRenamedStatementsM stmts $ \stmtsRen -> + -- NOTE: The language is imperative and we do not have lexical scoping, + -- therefore kont is called inside @withRenamedStatementsM@. + kont $ EFor (UniVar uni varFr) start end stmtsRen + +withRenamedStatementsM :: Statements f -> (Statements f -> RenameM c) -> RenameM c +withRenamedStatementsM (Statements stmts) kont = + runContT (traverse (ContT . withRenamedStatementM) stmts) $ kont . Statements renameExprM :: Expr f a -> RenameM (Expr f a) renameExprM (EConst uniConst) = pure $ EConst uniConst @@ -41,5 +55,3 @@ renameExprM (EIf cond expr1 expr2) = EIf <$> renameExprM cond <*> renameExprM expr1 <*> renameExprM expr2 renameExprM (EAppUnOp op expr) = EAppUnOp op <$> renameExprM expr renameExprM (EAppBinOp op expr1 expr2) = EAppBinOp op <$> renameExprM expr1 <*> renameExprM expr2 -renameExprM (EStatement stat expr) = - withRenamedStatementM stat $ \statRen -> EStatement statRen <$> renameExprM expr diff --git a/field/TinyLang/Field/Typed/Core.hs b/field/TinyLang/Field/Typed/Core.hs index 9286cb5..44ed1f5 100644 --- a/field/TinyLang/Field/Typed/Core.hs +++ b/field/TinyLang/Field/Typed/Core.hs @@ -16,29 +16,41 @@ module TinyLang.Field.Typed.Core , UnOp (..) , BinOp (..) , Statement (..) + , Statements + , pattern C.Statements + , C.unStatements + , Program + , pattern C.Program + , C.unProgram , Expr (..) , withUnOpUnis , withBinOpUnis , withGeqUni , withKnownUni - , VarSign (..) - , ScopedVarSigns (..) - , exprVarSigns - , exprFreeVarSigns - , supplyFromAtLeastFree + , VarSig (..) + , ScopedVarSigs (..) + -- , stmtVarSigs + -- , stmtFreeVarSigs + -- , stmtsFreeVarSigs + , progFreeVarSigs + -- , exprVarSigs + -- , exprFreeVarSigs + -- , exprSupplyFromAtLeastFree + -- , stmtSupplyFromAtLeastFree + , stmtsSupplyFromAtLeastFree , uniOfExpr ) where import Prelude hiding (div) import TinyLang.Prelude +import qualified TinyLang.Field.Core as C import Data.Field as Field import TinyLang.Environment as Env import TinyLang.Field.Existential import TinyLang.Field.UniConst import TinyLang.Var as Var - -- Needed for the sake of symmetry with 'UniConst'. data UniVar f a = UniVar { _uniVarUni :: Uni f a @@ -76,12 +88,17 @@ data BinOp f a b c where Div :: BinOp f (AField f) (AField f) (AField f) BAt :: BinOp f (AField f) (Vector Bool) Bool + +type Program f = C.Program (Statement f) +type Statements f = C.Statements (Statement f) + data Statement f where ELet :: UniVar f a -> Expr f a -> Statement f -- | Things that get compiled to constraints down the pipeline. -- The evaluation semantics is the following: each assertion becomes a check at runtime -- and the if the check fails, we have evaluation failure. EAssert :: Expr f Bool -> Statement f + EFor :: UniVar f (AField f) -> Integer -> Integer -> Statements f -> Statement f data Expr f a where EConst :: UniConst f a -> Expr f a @@ -89,7 +106,6 @@ data Expr f a where EIf :: Expr f Bool -> Expr f a -> Expr f a -> Expr f a EAppUnOp :: UnOp f a b -> Expr f a -> Expr f b EAppBinOp :: BinOp f a b c -> Expr f a -> Expr f b -> Expr f c - EStatement :: Statement f -> Expr f a -> Expr f a instance (Field f, af ~ AField f) => Field (Expr f af) where zer = EConst zer @@ -144,7 +160,6 @@ uniOfExpr (EVar (UniVar uni _)) = uni uniOfExpr (EAppUnOp op _) = withUnOpUnis op $ \_ resUni -> resUni uniOfExpr (EAppBinOp op _ _) = withBinOpUnis op $ \_ _ resUni -> resUni uniOfExpr (EIf _ x _) = uniOfExpr x -uniOfExpr (EStatement _ expr) = uniOfExpr expr withGeqUnOp :: UnOp f a1 b1 -> UnOp f a2 b2 -> d -> ((a1 ~ a2, b1 ~ b2) => d) -> d withGeqUnOp unOp1 unOp2 z y = @@ -176,10 +191,14 @@ instance Eq f => Eq (UniVar f a) where instance Eq f => Eq (Statement f) where ELet (UniVar u1 v1) d1 == ELet (UniVar u2 v2) d2 = withGeqUni u1 u2 False $ v1 == v2 && d1 == d2 - EAssert as1 == EAssert as2 = as1 == as2 + EAssert as1 == EAssert as2 = + as1 == as2 + EFor (UniVar u1 v1) i1 j1 stmts1 == EFor (UniVar u2 v2) i2 j2 stmts2 = + u1 == u2 && v1 == v2 && i1 == i2 && j1 == j2 && stmts1 == stmts2 ELet {} == _ = False EAssert {} == _ = False + EFor {} == _ = False instance Eq f => Eq (Expr f a) where EConst uval1 == EConst uval2 = uval1 == uval2 @@ -187,7 +206,6 @@ instance Eq f => Eq (Expr f a) where EIf b1 x1 y1 == EIf b2 x2 y2 = b1 == b2 && x1 == x2 && y1 == y2 EAppUnOp o1 x1 == EAppUnOp o2 x2 = withGeqUnOp o1 o2 False $ x1 == x2 EAppBinOp o1 x1 y1 == EAppBinOp o2 x2 y2 = withGeqBinOp o1 o2 False $ x1 == x2 && y1 == y2 - EStatement st1 e1 == EStatement st2 e2 = st1 == st2 && e1 == e2 -- Here we explicitly pattern match on the first argument again and always return 'False'. -- This way we'll get a warning when an additional constructor is added to 'Expr', @@ -197,63 +215,99 @@ instance Eq f => Eq (Expr f a) where EIf {} == _ = False EAppUnOp {} == _ = False EAppBinOp {} == _ = False - EStatement {} == _ = False withKnownUni :: Uni f a -> (KnownUni f a => c) -> c withKnownUni Bool = id withKnownUni Field = id withKnownUni Vector = id -data VarSign f = forall a. VarSign - { _varSignName :: String - , _varSignUni :: Uni f a +data VarSig f = forall a. VarSig + { _varSigName :: String + , _varSigUni :: Uni f a } -deriving instance Show (VarSign f) +deriving instance Show (VarSig f) -instance Eq (VarSign f) where - VarSign name1 uni1 == VarSign name2 uni2 = withGeqUni uni1 uni2 False $ name1 == name2 +instance Eq (VarSig f) where + VarSig name1 uni1 == VarSig name2 uni2 = withGeqUni uni1 uni2 False $ name1 == name2 -data ScopedVarSigns f = ScopedVarSigns - { _scopedVarSignsFree :: Env (VarSign f) - , _scopedVarSignsBound :: Env (VarSign f) +data ScopedVarSigs f = ScopedVarSigs + { _scopedVarSigsFree :: Env (VarSig f) + , _scopedVarSigsBound :: Env (VarSig f) } deriving (Show) -isTracked :: (Eq a, Show a) => Unique -> a -> Env a -> Bool -isTracked uniq x env = - case lookupUnique uniq env of - Just x' - | x == x' -> True - | otherwise -> error $ concat ["panic: mismatch: '", show x, "' vs '", show x', "'"] - Nothing -> False - --- TODO: test me somehow. -exprVarSigns :: Expr f a -> ScopedVarSigns f -exprVarSigns = goExpr $ ScopedVarSigns mempty mempty where - goStat :: ScopedVarSigns f -> Statement f -> ScopedVarSigns f - goStat signs (ELet uniVar def) = ScopedVarSigns free $ insertUnique uniq sign bound where - UniVar uni (Var uniq name) = uniVar - sign = VarSign name uni - ScopedVarSigns free bound = goExpr signs def - goStat signs (EAssert expr) = goExpr signs expr - - goExpr :: ScopedVarSigns f -> Expr f a -> ScopedVarSigns f - goExpr signs (EConst _) = signs - goExpr signs (EVar (UniVar uni (Var uniq name))) - | tracked = signs - | otherwise = ScopedVarSigns (insertUnique uniq sign free) bound - where - ScopedVarSigns free bound = signs - sign = VarSign name uni - tracked = isTracked uniq sign bound || isTracked uniq sign free - goExpr signs (EAppUnOp _ x) = goExpr signs x - goExpr signs (EAppBinOp _ x y) = goExpr (goExpr signs x) y - goExpr signs (EIf b x y) = goExpr (goExpr (goExpr signs b) x) y - goExpr signs (EStatement st e) = goExpr (goStat signs st) e - -exprFreeVarSigns :: Expr f a -> Env (VarSign f) -exprFreeVarSigns = _scopedVarSignsFree . exprVarSigns - -supplyFromAtLeastFree :: MonadSupply m => Expr f a -> m () -supplyFromAtLeastFree = - supplyFromAtLeast . freeUniqueIntMap . unEnv . _scopedVarSignsFree . exprVarSigns +-- | Add variable to the set of bound variables +bindVar :: UniVar f a -> State (ScopedVarSigs f) () +bindVar (UniVar uni (Var uniq name)) = + modify $ \(ScopedVarSigs free bound) -> + let sig = VarSig name uni + bound' = insertUnique uniq sig bound + in ScopedVarSigs free bound' + +-- | Add variable to the set of free variables +freeVar :: UniVar f a -> State (ScopedVarSigs f) () +freeVar (UniVar uni (Var uniq name)) = + modify $ \(ScopedVarSigs free bound) -> + let sig = VarSig name uni + free' = insertUnique uniq sig free + in ScopedVarSigs free' bound + +-- | Check if variable is tracked in bound or free variables +isTracked :: UniVar f a -> State (ScopedVarSigs f) Bool +isTracked (UniVar uni (Var uniq name)) = do + ScopedVarSigs free bound <- get + pure $ isTrackedIn free || isTrackedIn bound + where + sig = VarSig name uni + isTrackedIn env = + case lookupUnique uniq env of + Just x' + | x' == sig -> True + | otherwise -> error $ concat [ "panic: mismatch: '" + , show sig + , "' vs '" + , show x' + , "'"] + Nothing -> False + +-- | Gather VarSigs for a statement +stmtVS :: Statement f -> State (ScopedVarSigs f) () +stmtVS (EAssert expr) = exprVS expr +stmtVS (ELet uniVar def) = do + exprVS def + bindVar uniVar +stmtVS (EFor uniVar _ _ stmts) = do + bindVar uniVar + traverse_ stmtVS stmts + +-- | Gather VarSigs for an expression +exprVS :: Expr f a -> State (ScopedVarSigs f) () +exprVS (EConst _) = pure () +exprVS (EVar uniVar) = do + tracked <- isTracked uniVar + unless tracked $ freeVar uniVar +exprVS (EAppUnOp _ x) = exprVS x +exprVS (EAppBinOp _ x y) = do + exprVS x + exprVS y +exprVS (EIf b x y) = do + exprVS b + exprVS x + exprVS y + +-- | Collect all bindings +execSVS :: State (ScopedVarSigs f) () -> ScopedVarSigs f +execSVS s = execState s $ ScopedVarSigs mempty mempty + +-- | Return free variable signatures for a given program +progFreeVarSigs :: Program f -> Env (VarSig f) +progFreeVarSigs = _scopedVarSigsFree . execSVS . traverse_ stmtVS + +stmtsSupplyFromAtLeastFree :: MonadSupply m => Statements f -> m () +stmtsSupplyFromAtLeastFree = + supplyFromAtLeast + . freeUniqueIntMap + . unEnv + . _scopedVarSigsFree + . execSVS + . traverse_ stmtVS diff --git a/field/TinyLang/Field/Typed/Parser.hs b/field/TinyLang/Field/Typed/Parser.hs index 20beb5c..8215731 100644 --- a/field/TinyLang/Field/Typed/Parser.hs +++ b/field/TinyLang/Field/Typed/Parser.hs @@ -8,8 +8,10 @@ For the new API please refer to "TinyLang.Field.Raw.Parser". -} module TinyLang.Field.Typed.Parser - ( parseScopedExpr - , parseExpr + ( parseScopedProgram + , parseProgram + , parseScopedProgramFrom + , parseProgramFrom ) where import TinyLang.Prelude hiding (many, option, some, @@ -26,30 +28,39 @@ import qualified Data.IntMap.Strict as IntMap import qualified Data.IntSet as IntSet import qualified Data.Map.Strict as Map --- TODO: use a proper @newtype@. -instance TextField f => IsString (Scoped (Some (Expr f))) where - fromString = either error (fmap $ forget Some) . runSupplyT . parseScopedExpr +instance TextField f => IsString (Scoped (Program f)) where + fromString = either error id . runSupplyT . parseScopedProgram -instance TextField f => IsString (Some (Expr f)) where +instance TextField f => IsString (Program f) where fromString = _scopedValue <$> fromString --- | Parse a @String@ and return @Either@ an error message or an @Expr@ of some type. +-- | Parse a @String@ and return @Either@ an error message or an @Program@ of some type. -- If the result is an error, then return the latest 'Scope', otherwise return the 'Scope' -- consisting of all free variables of the expression. -parseScopedExpr +parseScopedProgramFrom :: forall f m. (MonadError String m, MonadSupply m, TextField f) - => String -> m (Scoped (SomeUniExpr f)) -parseScopedExpr str = do - exprRaw <- parseString (pTop @f) "" str - Scoped scopeTotal (SomeOf uni exprTyped) <- typeCheck exprRaw - exprTypedRen <- renameExpr exprTyped - let indicesFree = IntMap.keysSet . unEnv $ exprFreeVarSigns exprTypedRen + => String -> String -> m (Scoped (Program f)) +parseScopedProgramFrom fileName str = do + progRaw <- parseString (pTop @f) fileName str + Scoped scopeTotal progTyped <- typeProgram progRaw + progTypedRen <- renameProgram progTyped + let indicesFree = IntMap.keysSet . unEnv $ progFreeVarSigs progTypedRen isFree var = unUnique (_varUniq var) `IntSet.member` indicesFree scopeFree = Map.filter isFree scopeTotal - return . Scoped scopeFree $ SomeOf uni exprTypedRen + return $ Scoped scopeFree progTypedRen --- | Parse a @String@ and return @Either@ an error message or an @Expr@ of some type. -parseExpr +parseProgramFrom :: forall f m. (MonadError String m, MonadSupply m, TextField f) - => String -> m (SomeUniExpr f) -parseExpr = fmap _scopedValue . parseScopedExpr + => String -> String -> m (Program f) +parseProgramFrom fileName = fmap _scopedValue . parseScopedProgramFrom fileName + +parseScopedProgram + :: forall f m. (MonadError String m, MonadSupply m, TextField f) + => String -> m (Scoped (Program f)) +parseScopedProgram = parseScopedProgramFrom "" + +-- | Convenience version of @parseScopedProgram'@ with an empty file name. +parseProgram + :: forall f m. (MonadError String m, MonadSupply m, TextField f) + => String -> m (Program f) +parseProgram = parseProgramFrom "" diff --git a/field/TinyLang/Field/Typed/TypeChecker.hs b/field/TinyLang/Field/Typed/TypeChecker.hs index 72811c8..33963a0 100644 --- a/field/TinyLang/Field/Typed/TypeChecker.hs +++ b/field/TinyLang/Field/Typed/TypeChecker.hs @@ -25,18 +25,19 @@ module TinyLang.Field.Typed.TypeChecker , runTypeChecker , typeCheck , checkType + , typeProgram , inferExpr , checkExpr , inferUniVar , checkUniVar + , checkStatement + , checkProgram ) where import TinyLang.Prelude hiding (TypeError) import Data.Field -import TinyLang.Environment -import TinyLang.Field.Evaluator import TinyLang.Field.Existential import qualified TinyLang.Field.Raw.Core as R import qualified TinyLang.Field.Typed.Core as T @@ -97,6 +98,13 @@ typeCheck => R.Expr R.Var f -> m (Scoped (T.SomeUniExpr f)) typeCheck = runTypeChecker . inferExpr +{-| +-} +typeProgram + :: (MonadError TypeCheckError m, MonadSupply m, TextField f) + => R.Program R.Var f -> m (Scoped (T.Program f)) +typeProgram = runTypeChecker . checkProgram + {-| -} checkType @@ -127,7 +135,7 @@ mkSomeUniVar var -} inferUniVar :: forall m f. (MonadSupply m, MonadScope m) => R.Var -> m (T.SomeUniVar f) -inferUniVar = liftM mkSomeUniVar . makeVar . R.unVar +inferUniVar = fmap mkSomeUniVar . makeVar . R.unVar {-| Type inference for expressions -} @@ -145,16 +153,12 @@ inferExpr (R.EAppBinOp rBinOp l m) = inferExpr (R.EAppUnOp rUnOp l) = withTypedUnOp rUnOp $ \tUnOp -> SomeOf knownUni <$> (T.EAppUnOp tUnOp <$> checkExpr l) -inferExpr (R.EStatement s l) = do - tS <- checkStatement s - SomeOf uni tL <- inferExpr l - pure $ SomeOf uni $ (foldr T.EStatement) tL tS inferExpr (R.EIf l m n) = do tL <- checkExpr l SomeOf uni tM <- inferExpr m tN <- T.withKnownUni uni $ checkExpr n pure $ SomeOf uni $ T.EIf tL tM tN -inferExpr (R.ETypeAnn u m) = do +inferExpr (R.ETypeAnn u m) = case u of Some uni -> T.withKnownUni uni $ SomeOf uni <$> checkExpr m @@ -214,32 +218,27 @@ checkExpr m = do SomeOf mUni tM <- inferExpr m let uni = knownUni @f @a let uniMismatch = typeMismatch tM uni mUni - withGeqUniM uni mUni uniMismatch $ tM + withGeqUniM uni mUni uniMismatch tM + +checkProgram + :: forall m f. (MonadTypeChecker m, TextField f) + => R.Program R.Var f -> m (T.Program f) +checkProgram = traverse checkStatement + {-| Type checking judgement for statements of form -} checkStatement :: forall m f. (MonadTypeChecker m, TextField f) - => R.Statement R.Var f -> m [T.Statement f] + => R.Statement R.Var f -> m (T.Statement f) checkStatement (R.ELet var m) = do - Some (uniVar@(T.UniVar uni _)) <- inferUniVar var - T.withKnownUni uni $ pure . (T.ELet uniVar) <$> checkExpr m -checkStatement (R.EAssert m) = do - pure . T.EAssert <$> checkExpr m + Some uniVar@(T.UniVar uni _) <- inferUniVar var + T.withKnownUni uni $ T.ELet uniVar <$> checkExpr m +checkStatement (R.EAssert m) = + T.EAssert <$> checkExpr m checkStatement (R.EFor var start end stmts) = do tVar <- makeVar $ R.unVar var - (unrollLoop tVar start end) . concat <$> mapM checkStatement stmts - -{-| Statically unroll for statement loop --} -unrollLoop - :: forall f. (TextField f) - => T.Var -> Integer -> Integer -> [T.Statement f] -> [T.Statement f] -unrollLoop var lower bound stats = do - i <- [lower .. bound] - let env = insertVar var (Some $ fromInteger i) mempty - report err = error $ "Panic: " ++ show err - map (either report id . instStatement env) stats + T.EFor (T.UniVar Field tVar) start end <$> traverse checkStatement stmts {-| Error message for a failed type equality -} diff --git a/test/Field/Raw/golden/00-bool-literals.field b/test/Field/Raw/golden/00-bool-literals.field new file mode 100644 index 0000000..2966a27 --- /dev/null +++ b/test/Field/Raw/golden/00-bool-literals.field @@ -0,0 +1,2 @@ +let ?false = F; +let ?true = T; \ No newline at end of file diff --git a/test/Field/Raw/golden/00-bool-literals.golden b/test/Field/Raw/golden/00-bool-literals.golden new file mode 100644 index 0000000..29d1b5b --- /dev/null +++ b/test/Field/Raw/golden/00-bool-literals.golden @@ -0,0 +1 @@ +Program (Statements [ELet (Var "?false") (EConst (Some (UniConst Bool False))),ELet (Var "?true") (EConst (Some (UniConst Bool True)))]) \ No newline at end of file diff --git a/test/Field/Raw/golden/01-field-literals.field b/test/Field/Raw/golden/01-field-literals.field new file mode 100644 index 0000000..0fad65c --- /dev/null +++ b/test/Field/Raw/golden/01-field-literals.field @@ -0,0 +1,5 @@ +let zero = 0; +let one = 1; +let two = 2; +let half = 1/2; +let third = 1/3; \ No newline at end of file diff --git a/test/Field/Raw/golden/01-field-literals.golden b/test/Field/Raw/golden/01-field-literals.golden new file mode 100644 index 0000000..6840a71 --- /dev/null +++ b/test/Field/Raw/golden/01-field-literals.golden @@ -0,0 +1 @@ +Program (Statements [ELet (Var "zero") (EConst (Some 0)),ELet (Var "one") (EConst (Some 1)),ELet (Var "two") (EConst (Some 2)),ELet (Var "half") (EAppBinOp Div (EConst (Some 1)) (EConst (Some 2))),ELet (Var "third") (EAppBinOp Div (EConst (Some 1)) (EConst (Some 3)))]) \ No newline at end of file diff --git a/test/Field/Raw/golden/02-vector-literals.field b/test/Field/Raw/golden/02-vector-literals.field new file mode 100644 index 0000000..987c452 --- /dev/null +++ b/test/Field/Raw/golden/02-vector-literals.field @@ -0,0 +1,4 @@ +let #one = { T }; +let #two = { T , F }; +let #three = { T , F , T }; +let #four = { T , F , T , F }; \ No newline at end of file diff --git a/test/Field/Raw/golden/02-vector-literals.golden b/test/Field/Raw/golden/02-vector-literals.golden new file mode 100644 index 0000000..a18193a --- /dev/null +++ b/test/Field/Raw/golden/02-vector-literals.golden @@ -0,0 +1 @@ +Program (Statements [ELet (Var "#one") (EConst (Some (UniConst Vector [True]))),ELet (Var "#two") (EConst (Some (UniConst Vector [True,False]))),ELet (Var "#three") (EConst (Some (UniConst Vector [True,False,True]))),ELet (Var "#four") (EConst (Some (UniConst Vector [True,False,True,False])))]) \ No newline at end of file diff --git a/test/Field/Raw/golden/03-lexer-whitespace.field b/test/Field/Raw/golden/03-lexer-whitespace.field new file mode 100644 index 0000000..29d0d2e --- /dev/null +++ b/test/Field/Raw/golden/03-lexer-whitespace.field @@ -0,0 +1,13 @@ + let + +x + += + + +1 / 2 + + + +; + diff --git a/test/Field/Raw/golden/03-lexer-whitespace.golden b/test/Field/Raw/golden/03-lexer-whitespace.golden new file mode 100644 index 0000000..7be2c07 --- /dev/null +++ b/test/Field/Raw/golden/03-lexer-whitespace.golden @@ -0,0 +1 @@ +Program (Statements [ELet (Var "x") (EAppBinOp Div (EConst (Some 1)) (EConst (Some 2)))]) \ No newline at end of file diff --git a/test/Field/Raw/golden/04-lexer-whitespace.field b/test/Field/Raw/golden/04-lexer-whitespace.field new file mode 100644 index 0000000..cb46bae --- /dev/null +++ b/test/Field/Raw/golden/04-lexer-whitespace.field @@ -0,0 +1,2 @@ + + assert T; diff --git a/test/Field/Raw/golden/04-lexer-whitespace.golden b/test/Field/Raw/golden/04-lexer-whitespace.golden new file mode 100644 index 0000000..fb1b82b --- /dev/null +++ b/test/Field/Raw/golden/04-lexer-whitespace.golden @@ -0,0 +1 @@ +Program (Statements [EAssert (EConst (Some (UniConst Bool True)))]) \ No newline at end of file diff --git a/test/Field/Raw/golden/lexer-whitespace-02.field b/test/Field/Raw/golden/05-lexer-whitespace.field similarity index 75% rename from test/Field/Raw/golden/lexer-whitespace-02.field rename to test/Field/Raw/golden/05-lexer-whitespace.field index 18c8e44..b7b797d 100644 --- a/test/Field/Raw/golden/lexer-whitespace-02.field +++ b/test/Field/Raw/golden/05-lexer-whitespace.field @@ -12,4 +12,8 @@ do assert T; end -T \ No newline at end of file +assert T; + + + + diff --git a/test/Field/Raw/golden/05-lexer-whitespace.golden b/test/Field/Raw/golden/05-lexer-whitespace.golden new file mode 100644 index 0000000..68f049a --- /dev/null +++ b/test/Field/Raw/golden/05-lexer-whitespace.golden @@ -0,0 +1 @@ +Program (Statements [EFor (Var "i") 0 100 (Statements [EAssert (EConst (Some (UniConst Bool True)))]),EAssert (EConst (Some (UniConst Bool True)))]) \ No newline at end of file diff --git a/test/Field/Raw/golden/operator-precedence-00.field b/test/Field/Raw/golden/06-operator-precedence.field similarity index 91% rename from test/Field/Raw/golden/operator-precedence-00.field rename to test/Field/Raw/golden/06-operator-precedence.field index 1d6a844..7d6d65c 100644 --- a/test/Field/Raw/golden/operator-precedence-00.field +++ b/test/Field/Raw/golden/06-operator-precedence.field @@ -1,3 +1,4 @@ +assert a * b - c * d == @@ -9,4 +10,4 @@ xor >= e / f + g / h - \ No newline at end of file +; \ No newline at end of file diff --git a/test/Field/Raw/golden/06-operator-precedence.golden b/test/Field/Raw/golden/06-operator-precedence.golden new file mode 100644 index 0000000..d2ecb39 --- /dev/null +++ b/test/Field/Raw/golden/06-operator-precedence.golden @@ -0,0 +1 @@ +Program (Statements [EAssert (EAppBinOp Xor (EAppBinOp FEq (EAppBinOp Sub (EAppBinOp Mul (EVar (Var "a")) (EVar (Var "b"))) (EAppBinOp Mul (EVar (Var "c")) (EVar (Var "d")))) (EAppBinOp Add (EAppBinOp Div (EVar (Var "e")) (EVar (Var "f"))) (EAppBinOp Div (EVar (Var "g")) (EVar (Var "h"))))) (EAppBinOp FGe (EAppBinOp Sub (EAppBinOp Mul (EVar (Var "a")) (EVar (Var "b"))) (EAppBinOp Mul (EVar (Var "c")) (EVar (Var "d")))) (EAppBinOp Add (EAppBinOp Div (EVar (Var "e")) (EVar (Var "f"))) (EAppBinOp Div (EVar (Var "g")) (EVar (Var "h"))))))]) \ No newline at end of file diff --git a/test/Field/Raw/golden/07-operator-precedence.field b/test/Field/Raw/golden/07-operator-precedence.field new file mode 100644 index 0000000..642d66f --- /dev/null +++ b/test/Field/Raw/golden/07-operator-precedence.field @@ -0,0 +1,3 @@ +assert +(neg a and b) <= (neg (a and b)) +; \ No newline at end of file diff --git a/test/Field/Raw/golden/07-operator-precedence.golden b/test/Field/Raw/golden/07-operator-precedence.golden new file mode 100644 index 0000000..7ad8dde --- /dev/null +++ b/test/Field/Raw/golden/07-operator-precedence.golden @@ -0,0 +1 @@ +Program (Statements [EAssert (EAppBinOp FLe (EAppBinOp And (EAppUnOp Neg (EVar (Var "a"))) (EVar (Var "b"))) (EAppUnOp Neg (EAppBinOp And (EVar (Var "a")) (EVar (Var "b")))))]) \ No newline at end of file diff --git a/test/Field/Raw/golden/operator-precedence-02.field b/test/Field/Raw/golden/08-operator-precedence.field similarity index 87% rename from test/Field/Raw/golden/operator-precedence-02.field rename to test/Field/Raw/golden/08-operator-precedence.field index e6c46e9..3a579ed 100644 --- a/test/Field/Raw/golden/operator-precedence-02.field +++ b/test/Field/Raw/golden/08-operator-precedence.field @@ -1,2 +1,4 @@ +assert a + b [c] == a + (b [c]) and a + b [c] <= (a + b) [c] +; \ No newline at end of file diff --git a/test/Field/Raw/golden/08-operator-precedence.golden b/test/Field/Raw/golden/08-operator-precedence.golden new file mode 100644 index 0000000..775a093 --- /dev/null +++ b/test/Field/Raw/golden/08-operator-precedence.golden @@ -0,0 +1 @@ +Program (Statements [EAssert (EAppBinOp And (EAppBinOp FEq (EAppBinOp Add (EVar (Var "a")) (EAppBinOp BAt (EVar (Var "c")) (EVar (Var "b")))) (EAppBinOp Add (EVar (Var "a")) (EAppBinOp BAt (EVar (Var "c")) (EVar (Var "b"))))) (EAppBinOp FLe (EAppBinOp Add (EVar (Var "a")) (EAppBinOp BAt (EVar (Var "c")) (EVar (Var "b")))) (EAppBinOp BAt (EVar (Var "c")) (EAppBinOp Add (EVar (Var "a")) (EVar (Var "b"))))))]) \ No newline at end of file diff --git a/test/Field/Raw/golden/09-for-loop.field b/test/Field/Raw/golden/09-for-loop.field new file mode 100644 index 0000000..257765c --- /dev/null +++ b/test/Field/Raw/golden/09-for-loop.field @@ -0,0 +1 @@ +for i = 0 to 0 do end; diff --git a/test/Field/Raw/golden/09-for-loop.golden b/test/Field/Raw/golden/09-for-loop.golden new file mode 100644 index 0000000..3e3eb4c --- /dev/null +++ b/test/Field/Raw/golden/09-for-loop.golden @@ -0,0 +1 @@ +Program (Statements [EFor (Var "i") 0 0 (Statements [])]) \ No newline at end of file diff --git a/test/Field/Raw/golden/for-loop-01.field b/test/Field/Raw/golden/10-for-loop.field similarity index 90% rename from test/Field/Raw/golden/for-loop-01.field rename to test/Field/Raw/golden/10-for-loop.field index 0fa913a..e27e89c 100644 --- a/test/Field/Raw/golden/for-loop-01.field +++ b/test/Field/Raw/golden/10-for-loop.field @@ -9,4 +9,3 @@ for i = 1 to 2 do let p = p * l; end; end; -p \ No newline at end of file diff --git a/test/Field/Raw/golden/10-for-loop.golden b/test/Field/Raw/golden/10-for-loop.golden new file mode 100644 index 0000000..360f494 --- /dev/null +++ b/test/Field/Raw/golden/10-for-loop.golden @@ -0,0 +1 @@ +Program (Statements [EFor (Var "i") 1 2 (Statements [ELet (Var "i'") (EVar (Var "i")),EFor (Var "j") 2 3 (Statements [ELet (Var "k") (EAppBinOp Mul (EVar (Var "i")) (EVar (Var "j"))),EAssert (EAppBinOp FEq (EVar (Var "k")) (EAppBinOp Mul (EVar (Var "i'")) (EVar (Var "j"))))]),ELet (Var "p") (EVar (Var "i")),EFor (Var "l") 1 2 (Statements [ELet (Var "p") (EAppBinOp Mul (EVar (Var "p")) (EVar (Var "l")))])])]) \ No newline at end of file diff --git a/test/Field/Raw/golden/everything.field b/test/Field/Raw/golden/11-everything.field similarity index 80% rename from test/Field/Raw/golden/everything.field rename to test/Field/Raw/golden/11-everything.field index eed06e1..851ad35 100644 --- a/test/Field/Raw/golden/everything.field +++ b/test/Field/Raw/golden/11-everything.field @@ -22,11 +22,10 @@ let ?neq0 = neq0 f; let neg' = neg g; let inv' = inv h; let #unpack = unpack h; -let ?let = let i = 3; T; -let ?assert = assert T; T; -let ?for = for j = 0 to 2 do end; T; +let ?let = T; +assert T; +for j = 0 to 2 do end; let ?if = if T then T else T; let asf = 1 : field; let ?as = T : bool; -let #as = { T } : vector; -T \ No newline at end of file +let #as = { T } : vector; \ No newline at end of file diff --git a/test/Field/Raw/golden/11-everything.golden b/test/Field/Raw/golden/11-everything.golden new file mode 100644 index 0000000..9602863 --- /dev/null +++ b/test/Field/Raw/golden/11-everything.golden @@ -0,0 +1 @@ +Program (Statements [ELet (Var "?a") (EConst (Some (UniConst Bool True))),ELet (Var "?b") (EConst (Some (UniConst Bool False))),ELet (Var "#v") (EConst (Some (UniConst Vector [True,False,True]))),ELet (Var "?or") (EAppBinOp Or (EVar (Var "?a")) (EVar (Var "?b"))),ELet (Var "?and") (EAppBinOp Or (EVar (Var "?or")) (EVar (Var "?b"))),ELet (Var "?xor") (EAppBinOp Or (EVar (Var "?and")) (EVar (Var "?or"))),ELet (Var "f") (EConst (Some 0)),ELet (Var "g") (EConst (Some 1)),ELet (Var "h") (EConst (Some 2)),ELet (Var "?feq") (EAppBinOp FEq (EVar (Var "g")) (EVar (Var "f"))),ELet (Var "?fle") (EAppBinOp FLe (EVar (Var "h")) (EVar (Var "f"))),ELet (Var "?flt") (EAppBinOp FLt (EVar (Var "f")) (EVar (Var "g"))),ELet (Var "?fge") (EAppBinOp FGe (EVar (Var "g")) (EVar (Var "h"))),ELet (Var "?fgt") (EAppBinOp FGt (EVar (Var "h")) (EVar (Var "f"))),ELet (Var "add") (EAppBinOp Add (EVar (Var "f")) (EVar (Var "g"))),ELet (Var "sub") (EAppBinOp Sub (EVar (Var "g")) (EVar (Var "h"))),ELet (Var "mul") (EAppBinOp Mul (EVar (Var "h")) (EVar (Var "f"))),ELet (Var "div") (EAppBinOp Div (EVar (Var "f")) (EVar (Var "g"))),ELet (Var "?bat") (EAppBinOp BAt (EVar (Var "f")) (EVar (Var "#v"))),ELet (Var "?not") (EAppUnOp Not (EVar (Var "?a"))),ELet (Var "?neq0") (EAppUnOp Neq0 (EVar (Var "f"))),ELet (Var "neg'") (EAppUnOp Neg (EVar (Var "g"))),ELet (Var "inv'") (EAppUnOp Inv (EVar (Var "h"))),ELet (Var "#unpack") (EAppUnOp Unp (EVar (Var "h"))),ELet (Var "?let") (EConst (Some (UniConst Bool True))),EAssert (EConst (Some (UniConst Bool True))),EFor (Var "j") 0 2 (Statements []),ELet (Var "?if") (EIf (EConst (Some (UniConst Bool True))) (EConst (Some (UniConst Bool True))) (EConst (Some (UniConst Bool True)))),ELet (Var "asf") (ETypeAnn (Some Field) (EConst (Some 1))),ELet (Var "?as") (ETypeAnn (Some Bool) (EConst (Some (UniConst Bool True)))),ELet (Var "#as") (ETypeAnn (Some Vector) (EConst (Some (UniConst Vector [True]))))]) \ No newline at end of file diff --git a/test/Field/Raw/golden/bool-literal-F.field b/test/Field/Raw/golden/bool-literal-F.field deleted file mode 100644 index c137216..0000000 --- a/test/Field/Raw/golden/bool-literal-F.field +++ /dev/null @@ -1 +0,0 @@ -F \ No newline at end of file diff --git a/test/Field/Raw/golden/bool-literal-F.golden b/test/Field/Raw/golden/bool-literal-F.golden deleted file mode 100644 index f2e2fe3..0000000 --- a/test/Field/Raw/golden/bool-literal-F.golden +++ /dev/null @@ -1 +0,0 @@ -EConst (Some (UniConst Bool False)) \ No newline at end of file diff --git a/test/Field/Raw/golden/bool-literal-T.field b/test/Field/Raw/golden/bool-literal-T.field deleted file mode 100644 index 96583aa..0000000 --- a/test/Field/Raw/golden/bool-literal-T.field +++ /dev/null @@ -1 +0,0 @@ -T \ No newline at end of file diff --git a/test/Field/Raw/golden/bool-literal-T.golden b/test/Field/Raw/golden/bool-literal-T.golden deleted file mode 100644 index 01a4223..0000000 --- a/test/Field/Raw/golden/bool-literal-T.golden +++ /dev/null @@ -1 +0,0 @@ -EConst (Some (UniConst Bool True)) \ No newline at end of file diff --git a/test/Field/Raw/golden/everything.golden b/test/Field/Raw/golden/everything.golden deleted file mode 100644 index 667f247..0000000 --- a/test/Field/Raw/golden/everything.golden +++ /dev/null @@ -1 +0,0 @@ -EStatement (ELet (Var "?a") (EConst (Some (UniConst Bool True)))) (EStatement (ELet (Var "?b") (EConst (Some (UniConst Bool False)))) (EStatement (ELet (Var "#v") (EConst (Some (UniConst Vector [True,False,True])))) (EStatement (ELet (Var "?or") (EAppBinOp Or (EVar (Var "?a")) (EVar (Var "?b")))) (EStatement (ELet (Var "?and") (EAppBinOp Or (EVar (Var "?or")) (EVar (Var "?b")))) (EStatement (ELet (Var "?xor") (EAppBinOp Or (EVar (Var "?and")) (EVar (Var "?or")))) (EStatement (ELet (Var "f") (EConst (Some 0))) (EStatement (ELet (Var "g") (EConst (Some 1))) (EStatement (ELet (Var "h") (EConst (Some 2))) (EStatement (ELet (Var "?feq") (EAppBinOp FEq (EVar (Var "g")) (EVar (Var "f")))) (EStatement (ELet (Var "?fle") (EAppBinOp FLe (EVar (Var "h")) (EVar (Var "f")))) (EStatement (ELet (Var "?flt") (EAppBinOp FLt (EVar (Var "f")) (EVar (Var "g")))) (EStatement (ELet (Var "?fge") (EAppBinOp FGe (EVar (Var "g")) (EVar (Var "h")))) (EStatement (ELet (Var "?fgt") (EAppBinOp FGt (EVar (Var "h")) (EVar (Var "f")))) (EStatement (ELet (Var "add") (EAppBinOp Add (EVar (Var "f")) (EVar (Var "g")))) (EStatement (ELet (Var "sub") (EAppBinOp Sub (EVar (Var "g")) (EVar (Var "h")))) (EStatement (ELet (Var "mul") (EAppBinOp Mul (EVar (Var "h")) (EVar (Var "f")))) (EStatement (ELet (Var "div") (EAppBinOp Div (EVar (Var "f")) (EVar (Var "g")))) (EStatement (ELet (Var "?bat") (EAppBinOp BAt (EVar (Var "f")) (EVar (Var "#v")))) (EStatement (ELet (Var "?not") (EAppUnOp Not (EVar (Var "?a")))) (EStatement (ELet (Var "?neq0") (EAppUnOp Neq0 (EVar (Var "f")))) (EStatement (ELet (Var "neg'") (EAppUnOp Neg (EVar (Var "g")))) (EStatement (ELet (Var "inv'") (EAppUnOp Inv (EVar (Var "h")))) (EStatement (ELet (Var "#unpack") (EAppUnOp Unp (EVar (Var "h")))) (EStatement (ELet (Var "?let") (EStatement (ELet (Var "i") (EConst (Some 3))) (EConst (Some (UniConst Bool True))))) (EStatement (ELet (Var "?assert") (EStatement (EAssert (EConst (Some (UniConst Bool True)))) (EConst (Some (UniConst Bool True))))) (EStatement (ELet (Var "?for") (EStatement (EFor (Var "j") 0 2 []) (EConst (Some (UniConst Bool True))))) (EStatement (ELet (Var "?if") (EIf (EConst (Some (UniConst Bool True))) (EConst (Some (UniConst Bool True))) (EConst (Some (UniConst Bool True))))) (EStatement (ELet (Var "asf") (ETypeAnn (Some Field) (EConst (Some 1)))) (EStatement (ELet (Var "?as") (ETypeAnn (Some Bool) (EConst (Some (UniConst Bool True))))) (EStatement (ELet (Var "#as") (ETypeAnn (Some Vector) (EConst (Some (UniConst Vector [True]))))) (EConst (Some (UniConst Bool True))))))))))))))))))))))))))))))))) \ No newline at end of file diff --git a/test/Field/Raw/golden/for-loop-00.field b/test/Field/Raw/golden/for-loop-00.field deleted file mode 100644 index 98dc3b2..0000000 --- a/test/Field/Raw/golden/for-loop-00.field +++ /dev/null @@ -1 +0,0 @@ -for i = 0 to 0 do end; T diff --git a/test/Field/Raw/golden/for-loop-00.golden b/test/Field/Raw/golden/for-loop-00.golden deleted file mode 100644 index 726e19e..0000000 --- a/test/Field/Raw/golden/for-loop-00.golden +++ /dev/null @@ -1 +0,0 @@ -EStatement (EFor (Var "i") 0 0 []) (EConst (Some (UniConst Bool True))) \ No newline at end of file diff --git a/test/Field/Raw/golden/for-loop-01.golden b/test/Field/Raw/golden/for-loop-01.golden deleted file mode 100644 index ad3fbb4..0000000 --- a/test/Field/Raw/golden/for-loop-01.golden +++ /dev/null @@ -1 +0,0 @@ -EStatement (EFor (Var "i") 1 2 [ELet (Var "i'") (EVar (Var "i")),EFor (Var "j") 2 3 [ELet (Var "k") (EAppBinOp Mul (EVar (Var "i")) (EVar (Var "j"))),EAssert (EAppBinOp FEq (EVar (Var "k")) (EAppBinOp Mul (EVar (Var "i'")) (EVar (Var "j"))))],ELet (Var "p") (EVar (Var "i")),EFor (Var "l") 1 2 [ELet (Var "p") (EAppBinOp Mul (EVar (Var "p")) (EVar (Var "l")))]]) (EVar (Var "p")) \ No newline at end of file diff --git a/test/Field/Raw/golden/lexer-whitespace-01.field b/test/Field/Raw/golden/lexer-whitespace-01.field deleted file mode 100644 index c93e902..0000000 --- a/test/Field/Raw/golden/lexer-whitespace-01.field +++ /dev/null @@ -1,2 +0,0 @@ - - T diff --git a/test/Field/Raw/golden/lexer-whitespace-01.golden b/test/Field/Raw/golden/lexer-whitespace-01.golden deleted file mode 100644 index 01a4223..0000000 --- a/test/Field/Raw/golden/lexer-whitespace-01.golden +++ /dev/null @@ -1 +0,0 @@ -EConst (Some (UniConst Bool True)) \ No newline at end of file diff --git a/test/Field/Raw/golden/lexer-whitespace-02.golden b/test/Field/Raw/golden/lexer-whitespace-02.golden deleted file mode 100644 index 0c996ea..0000000 --- a/test/Field/Raw/golden/lexer-whitespace-02.golden +++ /dev/null @@ -1 +0,0 @@ -EStatement (EFor (Var "i") 0 100 [EAssert (EConst (Some (UniConst Bool True)))]) (EConst (Some (UniConst Bool True))) \ No newline at end of file diff --git a/test/Field/Raw/golden/operator-precedence-00.golden b/test/Field/Raw/golden/operator-precedence-00.golden deleted file mode 100644 index 98a3640..0000000 --- a/test/Field/Raw/golden/operator-precedence-00.golden +++ /dev/null @@ -1 +0,0 @@ -EAppBinOp Xor (EAppBinOp FEq (EAppBinOp Sub (EAppBinOp Mul (EVar (Var "a")) (EVar (Var "b"))) (EAppBinOp Mul (EVar (Var "c")) (EVar (Var "d")))) (EAppBinOp Add (EAppBinOp Div (EVar (Var "e")) (EVar (Var "f"))) (EAppBinOp Div (EVar (Var "g")) (EVar (Var "h"))))) (EAppBinOp FGe (EAppBinOp Sub (EAppBinOp Mul (EVar (Var "a")) (EVar (Var "b"))) (EAppBinOp Mul (EVar (Var "c")) (EVar (Var "d")))) (EAppBinOp Add (EAppBinOp Div (EVar (Var "e")) (EVar (Var "f"))) (EAppBinOp Div (EVar (Var "g")) (EVar (Var "h"))))) \ No newline at end of file diff --git a/test/Field/Raw/golden/operator-precedence-01.field b/test/Field/Raw/golden/operator-precedence-01.field deleted file mode 100644 index 72e2a00..0000000 --- a/test/Field/Raw/golden/operator-precedence-01.field +++ /dev/null @@ -1 +0,0 @@ -(neg a and b) <= (neg (a and b)) \ No newline at end of file diff --git a/test/Field/Raw/golden/operator-precedence-01.golden b/test/Field/Raw/golden/operator-precedence-01.golden deleted file mode 100644 index 3a65126..0000000 --- a/test/Field/Raw/golden/operator-precedence-01.golden +++ /dev/null @@ -1 +0,0 @@ -EAppBinOp FLe (EAppBinOp And (EAppUnOp Neg (EVar (Var "a"))) (EVar (Var "b"))) (EAppUnOp Neg (EAppBinOp And (EVar (Var "a")) (EVar (Var "b")))) \ No newline at end of file diff --git a/test/Field/Raw/golden/operator-precedence-02.golden b/test/Field/Raw/golden/operator-precedence-02.golden deleted file mode 100644 index 90b4865..0000000 --- a/test/Field/Raw/golden/operator-precedence-02.golden +++ /dev/null @@ -1 +0,0 @@ -EAppBinOp And (EAppBinOp FEq (EAppBinOp Add (EVar (Var "a")) (EAppBinOp BAt (EVar (Var "c")) (EVar (Var "b")))) (EAppBinOp Add (EVar (Var "a")) (EAppBinOp BAt (EVar (Var "c")) (EVar (Var "b"))))) (EAppBinOp FLe (EAppBinOp Add (EVar (Var "a")) (EAppBinOp BAt (EVar (Var "c")) (EVar (Var "b")))) (EAppBinOp BAt (EVar (Var "c")) (EAppBinOp Add (EVar (Var "a")) (EVar (Var "b"))))) \ No newline at end of file diff --git a/test/Field/Raw/golden/vec-literal.field b/test/Field/Raw/golden/vec-literal.field deleted file mode 100644 index 2bd76d1..0000000 --- a/test/Field/Raw/golden/vec-literal.field +++ /dev/null @@ -1 +0,0 @@ -{T, F, T, F, T, F} \ No newline at end of file diff --git a/test/Field/Raw/golden/vec-literal.golden b/test/Field/Raw/golden/vec-literal.golden deleted file mode 100644 index 70adf72..0000000 --- a/test/Field/Raw/golden/vec-literal.golden +++ /dev/null @@ -1 +0,0 @@ -EConst (Some (UniConst Vector [True,False,True,False,True,False])) \ No newline at end of file diff --git a/test/Field/Renaming.hs b/test/Field/Renaming.hs new file mode 100644 index 0000000..966e6d7 --- /dev/null +++ b/test/Field/Renaming.hs @@ -0,0 +1,53 @@ +{-# LANGUAGE QuasiQuotes #-} + +-- | Unit tests for +-- | +-- | * renaming +-- | * free variables + +module Field.Renaming + ( test_free_variables + , test_renaming + ) where + +-- import TinyLang.Prelude + +import TinyLang.Field.Typed.Core +import TinyLang.Field.Typed.Parser +import TinyLang.Field.Rename +import TinyLang.Field.Printer + +import qualified Data.String.Interpolate.IsString as QQ +import Test.Tasty +import Test.Tasty.HUnit + +test_free_variables :: TestTree +test_free_variables = testGroup "free variables" + [ testGroup "let binding" + [ testCase "should not bind variable before" $ + assertNonEmptyEnv $ freeVars "assert x == 1; let x = 1;" + , testCase "should not bind variable in the definition" $ + assertNonEmptyEnv $ freeVars "let x = x;" + , testCase "shoud bind its variable after" $ + emptyEnv @=? freeVars "let x = 1; assert x == 1;" + ] + , testGroup "assert statement" + [ testCase "should make variable free" $ + assertNonEmptyEnv $ freeVars "assert ?x;" + ] + , testGroup "for loop" + [ testCase "should not bind variable before" $ + assertNonEmptyEnv $ freeVars "assert x == 1; for x = 0 to 0 do end;" + , testCase "shoud bind its variable in body" $ + emptyEnv @=? freeVars "for x = 0 to 0 do assert x == 0; end;" + , testCase "should bind its variable after body" $ + emptyEnv @=? freeVars "for x = 0 to 0 do end; assert x == 1;" + ] + ] where + freeVars = progFreeVarSigs @(AField Rational) + emptyEnv = Env mempty + assertNonEmptyEnv = assertBool "set of free vars should not be empty" . (emptyEnv /=) + +-- TODO: Add more tests +test_renaming :: TestTree +test_renaming = testGroup "renamings" [] diff --git a/test/Field/TestUtils.hs b/test/Field/TestUtils.hs index fa6f7f7..42c2481 100644 --- a/test/Field/TestUtils.hs +++ b/test/Field/TestUtils.hs @@ -4,13 +4,18 @@ module Field.TestUtils , parseRational , parseFilePath , discoverTests + , typeCheckFilePath ) where import TinyLang.Prelude -import TinyLang.Field.Raw.Core (RawExpr) +import TinyLang.Field.Raw.Core (RawProgram) import TinyLang.Field.Raw.Parser +import TinyLang.Field.Typed.Core (Program) +import TinyLang.Field.Typed.Parser import TinyLang.ParseUtils +import TinyLang.Var + import System.FilePath import System.FilePath.Glob @@ -27,15 +32,20 @@ testFiles testDir = sort <$> globDir1 pat testDir goldenFile :: FilePath -> FilePath goldenFile filePath = dropExtension filePath ++ ".golden" -parseRational :: String -> String -> Either String (RawExpr Rational) +parseRational :: String -> String -> Either String (RawProgram Rational) parseRational fileName str = parseString pTop fileName str -parseFilePath :: FilePath -> IO (Either String (RawExpr Rational)) +parseFilePath :: FilePath -> IO (Either String (RawProgram Rational)) parseFilePath filePath = parseRational fileName <$> readFile filePath where fileName = takeFileName filePath +typeCheckFilePath :: FilePath -> IO (Either String (Program Rational)) +typeCheckFilePath filePath = + runSupplyT . parseProgramFrom fileName <$> readFile filePath where + fileName = takeFileName filePath + discoverTests :: String -> FilePath -> (FilePath -> TestTree) -> IO TestTree discoverTests groupName testDir genTest = do files <- testFiles testDir diff --git a/test/Field/Textual.hs b/test/Field/Textual.hs index 37ee996..5418d2e 100644 --- a/test/Field/Textual.hs +++ b/test/Field/Textual.hs @@ -5,8 +5,10 @@ module Field.Textual ( test_textual + , gen_test_roundtrip ) where +import Field.TestUtils import Data.Field.F17 import TinyLang.Field.Generator import qualified TinyLang.Field.Jubjub as JJ @@ -14,8 +16,9 @@ import TinyLang.Field.Printer import TinyLang.Field.Typed.Core import TinyLang.Field.Typed.Parser import TinyLang.Prelude +import TinyLang.Field.Rename +import TinyLang.Field.Evaluator -import System.Directory import System.FilePath import Test.QuickCheck import Test.Tasty @@ -26,20 +29,30 @@ import Test.Tasty.QuickCheck -- generators. I.e. we should implement alpha-equality (but it is kind of weird to change -- uniques of free variables and so we probably want a newtype wrapper around @Expr@ with -- that very specific @Eq@ instance). + + +-- TODO: I can probably remove a lot of code now that @Statements@ and @Program@ +-- are functors. +forgetProgramIDs :: Program f -> Program f +forgetProgramIDs = fmap forgetStatementIDs + + -- forgetStatementsIDs :: Statements f -> Statements f +-- forgetStatementsIDs = fmap forgetStatementIDs + forgetID :: UniVar f a -> UniVar f a forgetID (UniVar u v) = UniVar u $ Var (Unique 0) (_varName v) forgetStatementIDs :: Statement f -> Statement f forgetStatementIDs (ELet uvar d) = ELet (forgetID uvar) (forgetIDs d) forgetStatementIDs (EAssert expr) = EAssert $ forgetIDs expr - +forgetStatementIDs (EFor uvar start end stmts) = + EFor (forgetID uvar) start end (forgetStatementIDs <$> stmts) forgetIDs :: Expr f a -> Expr f a forgetIDs (EConst uval) = EConst uval forgetIDs (EVar uvar) = EVar $ forgetID uvar forgetIDs (EAppUnOp op e) = EAppUnOp op (forgetIDs e) forgetIDs (EAppBinOp op e1 e2) = EAppBinOp op (forgetIDs e1) (forgetIDs e2) forgetIDs (EIf e e1 e2) = EIf (forgetIDs e) (forgetIDs e1) (forgetIDs e2) -forgetIDs (EStatement stat e) = EStatement (forgetStatementIDs stat) (forgetIDs e) {- Call this with eg quickCheck (withMaxSuccess 1000 (prop_Ftest :: SomeUniExpr Rational -> Bool)) @@ -47,22 +60,14 @@ forgetIDs (EStatement stat e) = EStatement (forgetStatementIDs stat) (forgetIDs quickCheck (stdArgs {maxSuccess=500, maxSize=1000}) (prop_Ftest :: SomeUniExpr F17 -> Bool) -} -prop_Ftest :: (Eq f, TextField f) => SomeUniExpr f -> Either String () -prop_Ftest (SomeOf uni expr) = do - SomeOf uni' expr' <- runSupplyT $ parseExpr (exprToString NoIDs expr) - let checkResult expr'' = - when (forgetIDs expr /= forgetIDs expr'') . Left $ concat - [ exprToString NoIDs expr - , " is not equal to " - , exprToString NoIDs expr' - ] - uniMismatch = - Left $ concat - [ show uni - , " is not equal to " - , show uni' - ] - withGeqUni uni uni' uniMismatch $ checkResult expr' +prop_prog_roundtrip :: forall f. (Eq f, TextField f) => Program f -> Either String () +prop_prog_roundtrip prog = do + prog' <- runSupplyT $ parseProgram @f $ progToString NoIDs prog + when (forgetProgramIDs prog /= forgetProgramIDs prog) . Left $ concat + [ progToString NoIDs prog + , " is not equal to " + , progToString NoIDs prog' + ] data Binding f = forall a. Binding (UniVar f a) (Expr f a) @@ -70,26 +75,25 @@ deriving instance TextField f => Show (Binding f) instance (Field f, Arbitrary f) => Arbitrary (Binding f) where arbitrary = - withOneofUnis $ \(_ :: Uni f a) -> + withOneOfUnis $ \(_ :: Uni f a) -> Binding @f @a . unDefaultUniVar <$> arbitrary <*> arbitrary -prop_nestedELet +prop_nested_let :: forall f. (Eq f, TextField f) - => [Binding f] -> SomeUniExpr f -> Either String () -prop_nestedELet bindings body0 = prop_Ftest $ foldr bind body0 bindings where - bind :: Binding f -> SomeUniExpr f -> SomeUniExpr f - bind (Binding uniVar body) (SomeOf uni expr) = - SomeOf uni $ EStatement (ELet uniVar body) expr + => [Binding f] -> Either String () +prop_nested_let bindings = prop_prog_roundtrip $ Program $ Statements $ map bind bindings where + bind :: Binding f -> Statement f + bind (Binding uniVar body) = ELet uniVar body test_checkParseGeneric :: TestTree test_checkParseGeneric = testProperty "checkParseGeneric2" $ - withMaxSuccess 1000 . property $ prop_Ftest @JJ.F + withMaxSuccess 1000 . property $ prop_prog_roundtrip @JJ.F test_checkParseNestedLets :: TestTree test_checkParseNestedLets = testProperty "checkParseNestedLets" $ - withMaxSuccess 100 . property $ prop_nestedELet @F17 + withMaxSuccess 100 . property $ prop_nested_let @F17 test_printerParserRoundtrip :: TestTree test_printerParserRoundtrip = @@ -98,47 +102,104 @@ test_printerParserRoundtrip = , test_checkParseNestedLets ] -parsePrint :: String -> String -parsePrint - = either id (forget $ exprToString WithIDs) - . runSupplyT - . parseExpr @Rational - -parsePrintGolden :: String -> String -> TestTree -parsePrintGolden name expr = - withResource (createDirectoryIfMissing True folder) mempty $ \_ -> - goldenVsString - name - (folder name <> ".golden") - (return . fromString $ parsePrint expr) - where - folder = "test" "Field" "golden" - -test_forLoops :: TestTree -test_forLoops = parsePrintGolden "forLoops" $ unlines - [ "for i = 1 to 2 do" - , " let i' = i;" - , " for j = 2 to 3 do" - , " let k = i * j;" - , " assert k == i' * j;" - , " end;" - , " let p = i;" - , " for l = 1 to 2 do" - , " let p = p * l;" - , " end;" - , "end;" - , "p" - ] - -test_parsePrintGolden :: TestTree -test_parsePrintGolden = - testGroup "parsePrintGolden" - [ test_forLoops - ] - test_textual :: TestTree test_textual = testGroup "textual" [ test_printerParserRoundtrip - , test_parsePrintGolden + , test_renaming ] + +parsePrintFilePath :: FilePath -> IO String +parsePrintFilePath filePath = either id (progToString WithIDs) <$> typeCheckFilePath filePath + +testDir :: FilePath +testDir = "test" "Field" "golden" + +genTest :: FilePath -> TestTree +genTest filePath = goldenVsString name golden action + where name = takeBaseName filePath + golden = goldenFile filePath + action = fromString <$> parsePrintFilePath filePath + +gen_test_roundtrip :: IO TestTree +gen_test_roundtrip = + discoverTests "roundtrip golden" testDir genTest + + +prop_rename_same :: forall f. (TextField f) + => Program f -> Either String () +prop_rename_same prog = + when (norm' /= norm) . Left $ unlines [ "renamed program" + , norm' + , "is different from the original program" + , norm + ] where + prog' = runSupply $ renameProgram prog + norm = progToString NoIDs $ prog + norm' = progToString NoIDs $ prog' + + +prop_rename_same_norm :: forall f. (Eq f, TextField f, AsInteger f) + => ProgramWithEnv f -> Either String () +prop_rename_same_norm (ProgramWithEnv prog env) = + when (result' /= result) . Left $ unlines message where + message = [ "ERROR" + , ind $ "normalisation of the renamed program did not match the normalisation of the original program" + , "INITIAL STATE" + , ind $ show env + , "ORIGINAL PROGRAM" + , ind $ progToString WithIDs prog + , "ORIGINAL PROGRAM NORMALISED" + , ind $ either show (progToString WithIDs) norm + , "RENAMED PROGRAM" + , ind $ progToString WithIDs prog' + , "RENAMED PROGRAM NORMALISED" + , ind $ either show (progToString WithIDs) norm' + ] + ind = indent " " + prog' = runSupply $ renameProgram prog + nrmProg = flip evalEval env . normProgram + norm = nrmProg prog + norm' = nrmProg prog' + result = either firstWord (progToString NoIDs) norm + result' = either firstWord (progToString NoIDs) norm' + +indent :: String -> String -> String +indent prefix = unlines . map (prefix++) . lines + +firstWord :: (Show a) => a -> String +firstWord = takeWhile (not . isSpace) . show + +prop_rename_same_eval :: forall f. (Eq f, TextField f, AsInteger f) + => ProgramWithEnv f -> Either String () +prop_rename_same_eval (ProgramWithEnv prog env) = + when (result' /= result) . Left $ unlines message where + message = [ "ERROR" + , ind $ "evaluation of the renamed program did not match the evaluation of the original program" + , "INITIAL STATE" + , ind $ show env + , "ORIGINAL PROGRAM" + , ind $ progToString WithIDs prog + , "ORIGINAL PROGRAM FINAL STATE" + , ind $ show result + , "RENAMED PROGRAM" + , ind $ progToString WithIDs prog' + , "RENAMED PROGRAM FINAL STATE" + , ind $ show result' + ] + ind = indent " " + prog' = runSupply $ renameProgram prog + eval = flip execEval env . evalProgram + -- TODO: Fix equaity for errors + result = either firstWord show $ eval prog + result' = either firstWord show $ eval prog' + +test_renaming :: TestTree +test_renaming = + testGroup "renaming" [ testProperty "is stable with respect to equality" $ + withMaxSuccess 10000 . property $ prop_rename_same @F17 + , testProperty "is stable with respect to normalisation" $ + withMaxSuccess 1000 . property $ prop_rename_same_norm @F17 + , testProperty "is stable with respect to evaluation" $ + withMaxSuccess 1000 . property $ prop_rename_same_eval @F17 + ] diff --git a/test/Field/Typed/Textual.hs b/test/Field/Typed/Textual.hs index a3528a7..a377a59 100644 --- a/test/Field/Typed/Textual.hs +++ b/test/Field/Typed/Textual.hs @@ -3,9 +3,6 @@ module Field.Typed.Textual ) where import Field.TestUtils -import TinyLang.Field.Typed.Core (SomeUniExpr) -import TinyLang.Field.Typed.TypeChecker -import TinyLang.Var import Data.String import System.FilePath @@ -15,11 +12,6 @@ import Test.Tasty.Golden testDir :: FilePath testDir = "test" "Field" "Typed" "golden" -typeCheckFilePath :: FilePath -> IO (Either String (SomeUniExpr Rational)) -typeCheckFilePath filePath = do - parsed <- parseFilePath filePath - pure $ runSupplyT . fmap _scopedValue . typeCheck =<< parsed - genTest :: FilePath -> TestTree genTest filePath = goldenVsString name golden action where name = takeBaseName filePath diff --git a/test/Field/Typed/golden/00-constant.field b/test/Field/Typed/golden/00-constant.field deleted file mode 100644 index 96583aa..0000000 --- a/test/Field/Typed/golden/00-constant.field +++ /dev/null @@ -1 +0,0 @@ -T \ No newline at end of file diff --git a/test/Field/Typed/golden/00-constant.golden b/test/Field/Typed/golden/00-constant.golden deleted file mode 100644 index 92dea11..0000000 --- a/test/Field/Typed/golden/00-constant.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Bool (EConst (UniConst Bool True)) \ No newline at end of file diff --git a/test/Field/Typed/golden/00-constants.field b/test/Field/Typed/golden/00-constants.field new file mode 100644 index 0000000..c3edf4a --- /dev/null +++ b/test/Field/Typed/golden/00-constants.field @@ -0,0 +1,4 @@ +let ?true = T; +let ?false = F; +let field' = 0; +let #vector = { T }; \ No newline at end of file diff --git a/test/Field/Typed/golden/00-constants.golden b/test/Field/Typed/golden/00-constants.golden new file mode 100644 index 0000000..ce0b187 --- /dev/null +++ b/test/Field/Typed/golden/00-constants.golden @@ -0,0 +1 @@ +Program (Statements [ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?true_4}) (EConst (UniConst Bool True)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?false_5}) (EConst (UniConst Bool False)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = field'_6}) (EConst 0),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #vector_7}) (EConst (UniConst Vector [True]))]) \ No newline at end of file diff --git a/test/Field/Typed/golden/01-constant.field b/test/Field/Typed/golden/01-constant.field deleted file mode 100644 index c227083..0000000 --- a/test/Field/Typed/golden/01-constant.field +++ /dev/null @@ -1 +0,0 @@ -0 \ No newline at end of file diff --git a/test/Field/Typed/golden/01-constant.golden b/test/Field/Typed/golden/01-constant.golden deleted file mode 100644 index ea4667c..0000000 --- a/test/Field/Typed/golden/01-constant.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Field (EConst 0) \ No newline at end of file diff --git a/test/Field/Typed/golden/01-variables.field b/test/Field/Typed/golden/01-variables.field new file mode 100644 index 0000000..56820ab --- /dev/null +++ b/test/Field/Typed/golden/01-variables.field @@ -0,0 +1,3 @@ +let ?bool = ?i; +let field' = i; +let #vector = #i; \ No newline at end of file diff --git a/test/Field/Typed/golden/01-variables.golden b/test/Field/Typed/golden/01-variables.golden new file mode 100644 index 0000000..76a6524 --- /dev/null +++ b/test/Field/Typed/golden/01-variables.golden @@ -0,0 +1 @@ +Program (Statements [ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?bool_6}) (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?i_1})),ELet (UniVar {_uniVarUni = Field, _uniVarVar = field'_7}) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = i_3})),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #vector_8}) (EVar (UniVar {_uniVarUni = Vector, _uniVarVar = #i_5}))]) \ No newline at end of file diff --git a/test/Field/Typed/golden/02-binops.field b/test/Field/Typed/golden/02-binops.field new file mode 100644 index 0000000..77a4d19 --- /dev/null +++ b/test/Field/Typed/golden/02-binops.field @@ -0,0 +1,17 @@ +let ?or = T or T; +let ?and = T and T; +let ?xor = T xor T; + +let ?feq = 0 == 0; +let ?fle = 0 <= 1; +let ?flt = 0 < 1; +let ?fge = 1 >= 0; +let ?fgt = 1 > 0; + +let add = 1 + 1; +let sub = 1 - 1; +let mul = 1 * 1; +let div = 1 / 1; + +let ?bat = { T } [ 0 ]; + diff --git a/test/Field/Typed/golden/02-binops.golden b/test/Field/Typed/golden/02-binops.golden new file mode 100644 index 0000000..36a2b1e --- /dev/null +++ b/test/Field/Typed/golden/02-binops.golden @@ -0,0 +1 @@ +Program (Statements [ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?or_13}) (EAppBinOp Or (EConst (UniConst Bool True)) (EConst (UniConst Bool True))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?and_14}) (EAppBinOp And (EConst (UniConst Bool True)) (EConst (UniConst Bool True))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?xor_15}) (EAppBinOp Xor (EConst (UniConst Bool True)) (EConst (UniConst Bool True))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?feq_16}) (EAppBinOp FEq (EConst 0) (EConst 0)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?fle_17}) (EAppBinOp FLe (EConst 0) (EConst 1)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?flt_18}) (EAppBinOp FLt (EConst 0) (EConst 1)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?fge_19}) (EAppBinOp FGe (EConst 1) (EConst 0)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?fgt_20}) (EAppBinOp FGt (EConst 1) (EConst 0)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = add_21}) (EAppBinOp Add (EConst 1) (EConst 1)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = sub_22}) (EAppBinOp Sub (EConst 1) (EConst 1)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = mul_23}) (EAppBinOp Mul (EConst 1) (EConst 1)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = div_24}) (EAppBinOp Div (EConst 1) (EConst 1)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?bat_25}) (EAppBinOp BAt (EConst 0) (EConst (UniConst Vector [True])))]) \ No newline at end of file diff --git a/test/Field/Typed/golden/02-constant.field b/test/Field/Typed/golden/02-constant.field deleted file mode 100644 index a846568..0000000 --- a/test/Field/Typed/golden/02-constant.field +++ /dev/null @@ -1 +0,0 @@ -{ T } \ No newline at end of file diff --git a/test/Field/Typed/golden/02-constant.golden b/test/Field/Typed/golden/02-constant.golden deleted file mode 100644 index 68a6f3a..0000000 --- a/test/Field/Typed/golden/02-constant.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Vector (EConst (UniConst Vector [True])) \ No newline at end of file diff --git a/test/Field/Typed/golden/03-unops.field b/test/Field/Typed/golden/03-unops.field new file mode 100644 index 0000000..3e0ff2d --- /dev/null +++ b/test/Field/Typed/golden/03-unops.field @@ -0,0 +1,7 @@ +let ?not = not T; +let ?neq0 = neq0 0; + +let neg' = neg 0; +let inv' = inv 0; + +let #unpack = unpack 1; \ No newline at end of file diff --git a/test/Field/Typed/golden/03-unops.golden b/test/Field/Typed/golden/03-unops.golden new file mode 100644 index 0000000..fd2798f --- /dev/null +++ b/test/Field/Typed/golden/03-unops.golden @@ -0,0 +1 @@ +Program (Statements [ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?not_5}) (EAppUnOp Not (EConst (UniConst Bool True))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?neq0_6}) (EAppUnOp Neq0 (EConst 0)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = neg'_7}) (EAppUnOp Neg (EConst 0)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = inv'_8}) (EAppUnOp Inv (EConst 0)),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #unpack_9}) (EAppUnOp Unp (EConst 1))]) \ No newline at end of file diff --git a/test/Field/Typed/golden/03-variable.field b/test/Field/Typed/golden/03-variable.field deleted file mode 100644 index 597a6db..0000000 --- a/test/Field/Typed/golden/03-variable.field +++ /dev/null @@ -1 +0,0 @@ -i \ No newline at end of file diff --git a/test/Field/Typed/golden/03-variable.golden b/test/Field/Typed/golden/03-variable.golden deleted file mode 100644 index d89f63f..0000000 --- a/test/Field/Typed/golden/03-variable.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Field (EVar (UniVar {_uniVarUni = Field, _uniVarVar = i_0})) \ No newline at end of file diff --git a/test/Field/Typed/golden/04-statements.field b/test/Field/Typed/golden/04-statements.field new file mode 100644 index 0000000..a88533b --- /dev/null +++ b/test/Field/Typed/golden/04-statements.field @@ -0,0 +1,3 @@ +let x = 1; +assert T; +for x = 1 to 1 do end; \ No newline at end of file diff --git a/test/Field/Typed/golden/04-statements.golden b/test/Field/Typed/golden/04-statements.golden new file mode 100644 index 0000000..039d44d --- /dev/null +++ b/test/Field/Typed/golden/04-statements.golden @@ -0,0 +1 @@ +Program (Statements [ELet (UniVar {_uniVarUni = Field, _uniVarVar = x_1}) (EConst 1),EAssert (EConst (UniConst Bool True)),EFor (UniVar {_uniVarUni = Field, _uniVarVar = x_2}) 1 1 (Statements [])]) \ No newline at end of file diff --git a/test/Field/Typed/golden/04-variable.field b/test/Field/Typed/golden/04-variable.field deleted file mode 100644 index 888b9e5..0000000 --- a/test/Field/Typed/golden/04-variable.field +++ /dev/null @@ -1 +0,0 @@ -?i \ No newline at end of file diff --git a/test/Field/Typed/golden/04-variable.golden b/test/Field/Typed/golden/04-variable.golden deleted file mode 100644 index e4a0a33..0000000 --- a/test/Field/Typed/golden/04-variable.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Bool (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?i_0})) \ No newline at end of file diff --git a/test/Field/Typed/golden/05-ifs.field b/test/Field/Typed/golden/05-ifs.field new file mode 100644 index 0000000..54f4680 --- /dev/null +++ b/test/Field/Typed/golden/05-ifs.field @@ -0,0 +1,3 @@ +let field' = if T then 0 else 0; +let ?bool = if T then T else T; +let #vector = if T then { T } else { T }; \ No newline at end of file diff --git a/test/Field/Typed/golden/05-ifs.golden b/test/Field/Typed/golden/05-ifs.golden new file mode 100644 index 0000000..b389105 --- /dev/null +++ b/test/Field/Typed/golden/05-ifs.golden @@ -0,0 +1 @@ +Program (Statements [ELet (UniVar {_uniVarUni = Field, _uniVarVar = field'_3}) (EIf (EConst (UniConst Bool True)) (EConst 0) (EConst 0)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?bool_4}) (EIf (EConst (UniConst Bool True)) (EConst (UniConst Bool True)) (EConst (UniConst Bool True))),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #vector_5}) (EIf (EConst (UniConst Bool True)) (EConst (UniConst Vector [True])) (EConst (UniConst Vector [True])))]) \ No newline at end of file diff --git a/test/Field/Typed/golden/05-variable.field b/test/Field/Typed/golden/05-variable.field deleted file mode 100644 index 2f980ec..0000000 --- a/test/Field/Typed/golden/05-variable.field +++ /dev/null @@ -1 +0,0 @@ -#i \ No newline at end of file diff --git a/test/Field/Typed/golden/05-variable.golden b/test/Field/Typed/golden/05-variable.golden deleted file mode 100644 index 0978306..0000000 --- a/test/Field/Typed/golden/05-variable.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Vector (EVar (UniVar {_uniVarUni = Vector, _uniVarVar = #i_0})) \ No newline at end of file diff --git a/test/Field/Typed/golden/06-anns.field b/test/Field/Typed/golden/06-anns.field new file mode 100644 index 0000000..86272e1 --- /dev/null +++ b/test/Field/Typed/golden/06-anns.field @@ -0,0 +1,3 @@ +let ?bool = T : bool; +let field' = 1 : field; +let #vector = { T } : vector; \ No newline at end of file diff --git a/test/Field/Typed/golden/06-anns.golden b/test/Field/Typed/golden/06-anns.golden new file mode 100644 index 0000000..edde8c8 --- /dev/null +++ b/test/Field/Typed/golden/06-anns.golden @@ -0,0 +1 @@ +Program (Statements [ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?bool_3}) (EConst (UniConst Bool True)),ELet (UniVar {_uniVarUni = Field, _uniVarVar = field'_4}) (EConst 1),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #vector_5}) (EConst (UniConst Vector [True]))]) \ No newline at end of file diff --git a/test/Field/Typed/golden/06-binop.field b/test/Field/Typed/golden/06-binop.field deleted file mode 100644 index 8fd198c..0000000 --- a/test/Field/Typed/golden/06-binop.field +++ /dev/null @@ -1 +0,0 @@ -T or T \ No newline at end of file diff --git a/test/Field/Typed/golden/06-binop.golden b/test/Field/Typed/golden/06-binop.golden deleted file mode 100644 index 6a56924..0000000 --- a/test/Field/Typed/golden/06-binop.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Bool (EAppBinOp Or (EConst (UniConst Bool True)) (EConst (UniConst Bool True))) \ No newline at end of file diff --git a/test/Field/Typed/golden/07-binop.field b/test/Field/Typed/golden/07-binop.field deleted file mode 100644 index edb6a2a..0000000 --- a/test/Field/Typed/golden/07-binop.field +++ /dev/null @@ -1 +0,0 @@ -T and T \ No newline at end of file diff --git a/test/Field/Typed/golden/07-binop.golden b/test/Field/Typed/golden/07-binop.golden deleted file mode 100644 index 07dd659..0000000 --- a/test/Field/Typed/golden/07-binop.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Bool (EAppBinOp And (EConst (UniConst Bool True)) (EConst (UniConst Bool True))) \ No newline at end of file diff --git a/test/Field/Typed/golden/32-everything.field b/test/Field/Typed/golden/07-everything.field similarity index 80% rename from test/Field/Typed/golden/32-everything.field rename to test/Field/Typed/golden/07-everything.field index eed06e1..09e6c96 100644 --- a/test/Field/Typed/golden/32-everything.field +++ b/test/Field/Typed/golden/07-everything.field @@ -1,6 +1,9 @@ let ?a = T; let ?b = F; let #v = {T, F, T}; +let ?e = ?i; +let e = i; +let #e = #i; let ?or = ?a or ?b; let ?and = ?or or ?b; let ?xor = ?and or ?or; @@ -22,11 +25,10 @@ let ?neq0 = neq0 f; let neg' = neg g; let inv' = inv h; let #unpack = unpack h; -let ?let = let i = 3; T; -let ?assert = assert T; T; -let ?for = for j = 0 to 2 do end; T; +let ?let = T; +assert T; +for j = 0 to 2 do end; let ?if = if T then T else T; let asf = 1 : field; let ?as = T : bool; -let #as = { T } : vector; -T \ No newline at end of file +let #as = { T } : vector; \ No newline at end of file diff --git a/test/Field/Typed/golden/07-everything.golden b/test/Field/Typed/golden/07-everything.golden new file mode 100644 index 0000000..d908f1c --- /dev/null +++ b/test/Field/Typed/golden/07-everything.golden @@ -0,0 +1 @@ +Program (Statements [ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?a_36}) (EConst (UniConst Bool True)),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?b_37}) (EConst (UniConst Bool False)),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #v_38}) (EConst (UniConst Vector [True,False,True])),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?e_39}) (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?i_4})),ELet (UniVar {_uniVarUni = Field, _uniVarVar = e_40}) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = i_6})),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #e_41}) (EVar (UniVar {_uniVarUni = Vector, _uniVarVar = #i_8})),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?or_42}) (EAppBinOp Or (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?a_36})) (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?b_37}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?and_43}) (EAppBinOp Or (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?or_42})) (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?b_37}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?xor_44}) (EAppBinOp Or (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?and_43})) (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?or_42}))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = f_45}) (EConst 0),ELet (UniVar {_uniVarUni = Field, _uniVarVar = g_46}) (EConst 1),ELet (UniVar {_uniVarUni = Field, _uniVarVar = h_47}) (EConst 2),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?feq_48}) (EAppBinOp FEq (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_46})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_45}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?fle_49}) (EAppBinOp FLe (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_47})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_45}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?flt_50}) (EAppBinOp FLt (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_45})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_46}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?fge_51}) (EAppBinOp FGe (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_46})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_47}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?fgt_52}) (EAppBinOp FGt (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_47})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_45}))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = add_53}) (EAppBinOp Add (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_45})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_46}))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = sub_54}) (EAppBinOp Sub (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_46})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_47}))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = mul_55}) (EAppBinOp Mul (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_47})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_45}))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = div_56}) (EAppBinOp Div (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_45})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_46}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?bat_57}) (EAppBinOp BAt (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_45})) (EVar (UniVar {_uniVarUni = Vector, _uniVarVar = #v_38}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?not_58}) (EAppUnOp Not (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?a_36}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?neq0_59}) (EAppUnOp Neq0 (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_45}))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = neg'_60}) (EAppUnOp Neg (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_46}))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = inv'_61}) (EAppUnOp Inv (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_47}))),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #unpack_62}) (EAppUnOp Unp (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_47}))),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?let_63}) (EConst (UniConst Bool True)),EAssert (EConst (UniConst Bool True)),EFor (UniVar {_uniVarUni = Field, _uniVarVar = j_64}) 0 2 (Statements []),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?if_65}) (EIf (EConst (UniConst Bool True)) (EConst (UniConst Bool True)) (EConst (UniConst Bool True))),ELet (UniVar {_uniVarUni = Field, _uniVarVar = asf_66}) (EConst 1),ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?as_67}) (EConst (UniConst Bool True)),ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #as_68}) (EConst (UniConst Vector [True]))]) \ No newline at end of file diff --git a/test/Field/Typed/golden/08-binop.field b/test/Field/Typed/golden/08-binop.field deleted file mode 100644 index 92a8dd0..0000000 --- a/test/Field/Typed/golden/08-binop.field +++ /dev/null @@ -1 +0,0 @@ -T xor T \ No newline at end of file diff --git a/test/Field/Typed/golden/08-binop.golden b/test/Field/Typed/golden/08-binop.golden deleted file mode 100644 index fcdf6ea..0000000 --- a/test/Field/Typed/golden/08-binop.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Bool (EAppBinOp Xor (EConst (UniConst Bool True)) (EConst (UniConst Bool True))) \ No newline at end of file diff --git a/test/Field/Typed/golden/09-binop.field b/test/Field/Typed/golden/09-binop.field deleted file mode 100644 index 65341b1..0000000 --- a/test/Field/Typed/golden/09-binop.field +++ /dev/null @@ -1 +0,0 @@ -0 == 0 \ No newline at end of file diff --git a/test/Field/Typed/golden/09-binop.golden b/test/Field/Typed/golden/09-binop.golden deleted file mode 100644 index cde3ebe..0000000 --- a/test/Field/Typed/golden/09-binop.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Bool (EAppBinOp FEq (EConst 0) (EConst 0)) \ No newline at end of file diff --git a/test/Field/Typed/golden/10-binop.field b/test/Field/Typed/golden/10-binop.field deleted file mode 100644 index b6e6e03..0000000 --- a/test/Field/Typed/golden/10-binop.field +++ /dev/null @@ -1 +0,0 @@ -0 <= 1 \ No newline at end of file diff --git a/test/Field/Typed/golden/10-binop.golden b/test/Field/Typed/golden/10-binop.golden deleted file mode 100644 index 2d359d8..0000000 --- a/test/Field/Typed/golden/10-binop.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Bool (EAppBinOp FLe (EConst 0) (EConst 1)) \ No newline at end of file diff --git a/test/Field/Typed/golden/11-binop.field b/test/Field/Typed/golden/11-binop.field deleted file mode 100644 index 5341e7f..0000000 --- a/test/Field/Typed/golden/11-binop.field +++ /dev/null @@ -1 +0,0 @@ -0 < 1 \ No newline at end of file diff --git a/test/Field/Typed/golden/11-binop.golden b/test/Field/Typed/golden/11-binop.golden deleted file mode 100644 index 757c862..0000000 --- a/test/Field/Typed/golden/11-binop.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Bool (EAppBinOp FLt (EConst 0) (EConst 1)) \ No newline at end of file diff --git a/test/Field/Typed/golden/12-binop.field b/test/Field/Typed/golden/12-binop.field deleted file mode 100644 index 4de0f61..0000000 --- a/test/Field/Typed/golden/12-binop.field +++ /dev/null @@ -1 +0,0 @@ -1 >= 0 \ No newline at end of file diff --git a/test/Field/Typed/golden/12-binop.golden b/test/Field/Typed/golden/12-binop.golden deleted file mode 100644 index 5f0c6f3..0000000 --- a/test/Field/Typed/golden/12-binop.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Bool (EAppBinOp FGe (EConst 1) (EConst 0)) \ No newline at end of file diff --git a/test/Field/Typed/golden/13-binop.field b/test/Field/Typed/golden/13-binop.field deleted file mode 100644 index cf703ff..0000000 --- a/test/Field/Typed/golden/13-binop.field +++ /dev/null @@ -1 +0,0 @@ -1 > 0 \ No newline at end of file diff --git a/test/Field/Typed/golden/13-binop.golden b/test/Field/Typed/golden/13-binop.golden deleted file mode 100644 index fd9f6f9..0000000 --- a/test/Field/Typed/golden/13-binop.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Bool (EAppBinOp FGt (EConst 1) (EConst 0)) \ No newline at end of file diff --git a/test/Field/Typed/golden/14-binop.field b/test/Field/Typed/golden/14-binop.field deleted file mode 100644 index 1a5a117..0000000 --- a/test/Field/Typed/golden/14-binop.field +++ /dev/null @@ -1 +0,0 @@ -1 + 1 \ No newline at end of file diff --git a/test/Field/Typed/golden/14-binop.golden b/test/Field/Typed/golden/14-binop.golden deleted file mode 100644 index b056f4c..0000000 --- a/test/Field/Typed/golden/14-binop.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Field (EAppBinOp Add (EConst 1) (EConst 1)) \ No newline at end of file diff --git a/test/Field/Typed/golden/15-binop.field b/test/Field/Typed/golden/15-binop.field deleted file mode 100644 index 0576959..0000000 --- a/test/Field/Typed/golden/15-binop.field +++ /dev/null @@ -1 +0,0 @@ -1 - 1 \ No newline at end of file diff --git a/test/Field/Typed/golden/15-binop.golden b/test/Field/Typed/golden/15-binop.golden deleted file mode 100644 index 6c3b2c8..0000000 --- a/test/Field/Typed/golden/15-binop.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Field (EAppBinOp Sub (EConst 1) (EConst 1)) \ No newline at end of file diff --git a/test/Field/Typed/golden/16-binop.field b/test/Field/Typed/golden/16-binop.field deleted file mode 100644 index 1bdc0ef..0000000 --- a/test/Field/Typed/golden/16-binop.field +++ /dev/null @@ -1 +0,0 @@ -1 * 1 \ No newline at end of file diff --git a/test/Field/Typed/golden/16-binop.golden b/test/Field/Typed/golden/16-binop.golden deleted file mode 100644 index d8047fd..0000000 --- a/test/Field/Typed/golden/16-binop.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Field (EAppBinOp Mul (EConst 1) (EConst 1)) \ No newline at end of file diff --git a/test/Field/Typed/golden/17-binop.field b/test/Field/Typed/golden/17-binop.field deleted file mode 100644 index f31597d..0000000 --- a/test/Field/Typed/golden/17-binop.field +++ /dev/null @@ -1 +0,0 @@ -1 / 1 \ No newline at end of file diff --git a/test/Field/Typed/golden/17-binop.golden b/test/Field/Typed/golden/17-binop.golden deleted file mode 100644 index 80989ea..0000000 --- a/test/Field/Typed/golden/17-binop.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Field (EAppBinOp Div (EConst 1) (EConst 1)) \ No newline at end of file diff --git a/test/Field/Typed/golden/18-binop.field b/test/Field/Typed/golden/18-binop.field deleted file mode 100644 index 1b8c808..0000000 --- a/test/Field/Typed/golden/18-binop.field +++ /dev/null @@ -1 +0,0 @@ -{ T } [ 0 ] \ No newline at end of file diff --git a/test/Field/Typed/golden/18-binop.golden b/test/Field/Typed/golden/18-binop.golden deleted file mode 100644 index 8239bde..0000000 --- a/test/Field/Typed/golden/18-binop.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Bool (EAppBinOp BAt (EConst 0) (EConst (UniConst Vector [True]))) \ No newline at end of file diff --git a/test/Field/Typed/golden/19-unop.field b/test/Field/Typed/golden/19-unop.field deleted file mode 100644 index 7cbce18..0000000 --- a/test/Field/Typed/golden/19-unop.field +++ /dev/null @@ -1 +0,0 @@ -not T \ No newline at end of file diff --git a/test/Field/Typed/golden/19-unop.golden b/test/Field/Typed/golden/19-unop.golden deleted file mode 100644 index fb23d4a..0000000 --- a/test/Field/Typed/golden/19-unop.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Bool (EAppUnOp Not (EConst (UniConst Bool True))) \ No newline at end of file diff --git a/test/Field/Typed/golden/20-unop.field b/test/Field/Typed/golden/20-unop.field deleted file mode 100644 index c573985..0000000 --- a/test/Field/Typed/golden/20-unop.field +++ /dev/null @@ -1 +0,0 @@ -neq0 1 \ No newline at end of file diff --git a/test/Field/Typed/golden/20-unop.golden b/test/Field/Typed/golden/20-unop.golden deleted file mode 100644 index d5b4a86..0000000 --- a/test/Field/Typed/golden/20-unop.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Bool (EAppUnOp Neq0 (EConst 1)) \ No newline at end of file diff --git a/test/Field/Typed/golden/21-unop.field b/test/Field/Typed/golden/21-unop.field deleted file mode 100644 index d274f6d..0000000 --- a/test/Field/Typed/golden/21-unop.field +++ /dev/null @@ -1 +0,0 @@ -neg 1 \ No newline at end of file diff --git a/test/Field/Typed/golden/21-unop.golden b/test/Field/Typed/golden/21-unop.golden deleted file mode 100644 index b6eff40..0000000 --- a/test/Field/Typed/golden/21-unop.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Field (EAppUnOp Neg (EConst 1)) \ No newline at end of file diff --git a/test/Field/Typed/golden/22-unop.field b/test/Field/Typed/golden/22-unop.field deleted file mode 100644 index c0ecd8b..0000000 --- a/test/Field/Typed/golden/22-unop.field +++ /dev/null @@ -1 +0,0 @@ -inv 1 \ No newline at end of file diff --git a/test/Field/Typed/golden/22-unop.golden b/test/Field/Typed/golden/22-unop.golden deleted file mode 100644 index 59d4e7c..0000000 --- a/test/Field/Typed/golden/22-unop.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Field (EAppUnOp Inv (EConst 1)) \ No newline at end of file diff --git a/test/Field/Typed/golden/23-unop.field b/test/Field/Typed/golden/23-unop.field deleted file mode 100644 index d336756..0000000 --- a/test/Field/Typed/golden/23-unop.field +++ /dev/null @@ -1 +0,0 @@ -unpack 1 \ No newline at end of file diff --git a/test/Field/Typed/golden/23-unop.golden b/test/Field/Typed/golden/23-unop.golden deleted file mode 100644 index f3d81be..0000000 --- a/test/Field/Typed/golden/23-unop.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Vector (EAppUnOp Unp (EConst 1)) \ No newline at end of file diff --git a/test/Field/Typed/golden/24-statement.field b/test/Field/Typed/golden/24-statement.field deleted file mode 100644 index e47409e..0000000 --- a/test/Field/Typed/golden/24-statement.field +++ /dev/null @@ -1 +0,0 @@ -let x = 1; x \ No newline at end of file diff --git a/test/Field/Typed/golden/24-statement.golden b/test/Field/Typed/golden/24-statement.golden deleted file mode 100644 index 1ad7660..0000000 --- a/test/Field/Typed/golden/24-statement.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Field (EStatement (ELet (UniVar {_uniVarUni = Field, _uniVarVar = x_0}) (EConst 1)) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = x_0}))) \ No newline at end of file diff --git a/test/Field/Typed/golden/25-statement.field b/test/Field/Typed/golden/25-statement.field deleted file mode 100644 index 7465219..0000000 --- a/test/Field/Typed/golden/25-statement.field +++ /dev/null @@ -1 +0,0 @@ -assert T; T \ No newline at end of file diff --git a/test/Field/Typed/golden/25-statement.golden b/test/Field/Typed/golden/25-statement.golden deleted file mode 100644 index 6058708..0000000 --- a/test/Field/Typed/golden/25-statement.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Bool (EStatement (EAssert (EConst (UniConst Bool True))) (EConst (UniConst Bool True))) \ No newline at end of file diff --git a/test/Field/Typed/golden/26-statement.field b/test/Field/Typed/golden/26-statement.field deleted file mode 100644 index 348cadc..0000000 --- a/test/Field/Typed/golden/26-statement.field +++ /dev/null @@ -1 +0,0 @@ -for x = 1 to 1 do assert T; end; T \ No newline at end of file diff --git a/test/Field/Typed/golden/26-statement.golden b/test/Field/Typed/golden/26-statement.golden deleted file mode 100644 index 6058708..0000000 --- a/test/Field/Typed/golden/26-statement.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Bool (EStatement (EAssert (EConst (UniConst Bool True))) (EConst (UniConst Bool True))) \ No newline at end of file diff --git a/test/Field/Typed/golden/27-if.field b/test/Field/Typed/golden/27-if.field deleted file mode 100644 index 81a7c49..0000000 --- a/test/Field/Typed/golden/27-if.field +++ /dev/null @@ -1 +0,0 @@ -if T then 0 else 0 \ No newline at end of file diff --git a/test/Field/Typed/golden/27-if.golden b/test/Field/Typed/golden/27-if.golden deleted file mode 100644 index b5ad8f1..0000000 --- a/test/Field/Typed/golden/27-if.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Field (EIf (EConst (UniConst Bool True)) (EConst 0) (EConst 0)) \ No newline at end of file diff --git a/test/Field/Typed/golden/28-if.field b/test/Field/Typed/golden/28-if.field deleted file mode 100644 index 1563ddc..0000000 --- a/test/Field/Typed/golden/28-if.field +++ /dev/null @@ -1 +0,0 @@ -0 + if T then 0 else 0 \ No newline at end of file diff --git a/test/Field/Typed/golden/28-if.golden b/test/Field/Typed/golden/28-if.golden deleted file mode 100644 index bbf9bf8..0000000 --- a/test/Field/Typed/golden/28-if.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Field (EAppBinOp Add (EConst 0) (EIf (EConst (UniConst Bool True)) (EConst 0) (EConst 0))) \ No newline at end of file diff --git a/test/Field/Typed/golden/29-ann.field b/test/Field/Typed/golden/29-ann.field deleted file mode 100644 index aa31b53..0000000 --- a/test/Field/Typed/golden/29-ann.field +++ /dev/null @@ -1 +0,0 @@ -T : bool \ No newline at end of file diff --git a/test/Field/Typed/golden/29-ann.golden b/test/Field/Typed/golden/29-ann.golden deleted file mode 100644 index 92dea11..0000000 --- a/test/Field/Typed/golden/29-ann.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Bool (EConst (UniConst Bool True)) \ No newline at end of file diff --git a/test/Field/Typed/golden/30-ann.field b/test/Field/Typed/golden/30-ann.field deleted file mode 100644 index c03f345..0000000 --- a/test/Field/Typed/golden/30-ann.field +++ /dev/null @@ -1 +0,0 @@ -1 : field \ No newline at end of file diff --git a/test/Field/Typed/golden/30-ann.golden b/test/Field/Typed/golden/30-ann.golden deleted file mode 100644 index d4af0b5..0000000 --- a/test/Field/Typed/golden/30-ann.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Field (EConst 1) \ No newline at end of file diff --git a/test/Field/Typed/golden/31-ann.field b/test/Field/Typed/golden/31-ann.field deleted file mode 100644 index 69c1e4a..0000000 --- a/test/Field/Typed/golden/31-ann.field +++ /dev/null @@ -1 +0,0 @@ -{ T } : vector \ No newline at end of file diff --git a/test/Field/Typed/golden/31-ann.golden b/test/Field/Typed/golden/31-ann.golden deleted file mode 100644 index 68a6f3a..0000000 --- a/test/Field/Typed/golden/31-ann.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Vector (EConst (UniConst Vector [True])) \ No newline at end of file diff --git a/test/Field/Typed/golden/32-everything.golden b/test/Field/Typed/golden/32-everything.golden deleted file mode 100644 index 7959706..0000000 --- a/test/Field/Typed/golden/32-everything.golden +++ /dev/null @@ -1 +0,0 @@ -SomeOf Bool (EStatement (ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?a_0}) (EConst (UniConst Bool True))) (EStatement (ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?b_1}) (EConst (UniConst Bool False))) (EStatement (ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #v_2}) (EConst (UniConst Vector [True,False,True]))) (EStatement (ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?or_3}) (EAppBinOp Or (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?a_0})) (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?b_1})))) (EStatement (ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?and_4}) (EAppBinOp Or (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?or_3})) (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?b_1})))) (EStatement (ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?xor_5}) (EAppBinOp Or (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?and_4})) (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?or_3})))) (EStatement (ELet (UniVar {_uniVarUni = Field, _uniVarVar = f_6}) (EConst 0)) (EStatement (ELet (UniVar {_uniVarUni = Field, _uniVarVar = g_7}) (EConst 1)) (EStatement (ELet (UniVar {_uniVarUni = Field, _uniVarVar = h_8}) (EConst 2)) (EStatement (ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?feq_9}) (EAppBinOp FEq (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_7})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_6})))) (EStatement (ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?fle_10}) (EAppBinOp FLe (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_8})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_6})))) (EStatement (ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?flt_11}) (EAppBinOp FLt (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_6})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_7})))) (EStatement (ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?fge_12}) (EAppBinOp FGe (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_7})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_8})))) (EStatement (ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?fgt_13}) (EAppBinOp FGt (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_8})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_6})))) (EStatement (ELet (UniVar {_uniVarUni = Field, _uniVarVar = add_14}) (EAppBinOp Add (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_6})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_7})))) (EStatement (ELet (UniVar {_uniVarUni = Field, _uniVarVar = sub_15}) (EAppBinOp Sub (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_7})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_8})))) (EStatement (ELet (UniVar {_uniVarUni = Field, _uniVarVar = mul_16}) (EAppBinOp Mul (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_8})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_6})))) (EStatement (ELet (UniVar {_uniVarUni = Field, _uniVarVar = div_17}) (EAppBinOp Div (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_6})) (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_7})))) (EStatement (ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?bat_18}) (EAppBinOp BAt (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_6})) (EVar (UniVar {_uniVarUni = Vector, _uniVarVar = #v_2})))) (EStatement (ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?not_19}) (EAppUnOp Not (EVar (UniVar {_uniVarUni = Bool, _uniVarVar = ?a_0})))) (EStatement (ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?neq0_20}) (EAppUnOp Neq0 (EVar (UniVar {_uniVarUni = Field, _uniVarVar = f_6})))) (EStatement (ELet (UniVar {_uniVarUni = Field, _uniVarVar = neg'_21}) (EAppUnOp Neg (EVar (UniVar {_uniVarUni = Field, _uniVarVar = g_7})))) (EStatement (ELet (UniVar {_uniVarUni = Field, _uniVarVar = inv'_22}) (EAppUnOp Inv (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_8})))) (EStatement (ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #unpack_23}) (EAppUnOp Unp (EVar (UniVar {_uniVarUni = Field, _uniVarVar = h_8})))) (EStatement (ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?let_24}) (EStatement (ELet (UniVar {_uniVarUni = Field, _uniVarVar = i_25}) (EConst 3)) (EConst (UniConst Bool True)))) (EStatement (ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?assert_26}) (EStatement (EAssert (EConst (UniConst Bool True))) (EConst (UniConst Bool True)))) (EStatement (ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?for_27}) (EConst (UniConst Bool True))) (EStatement (ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?if_29}) (EIf (EConst (UniConst Bool True)) (EConst (UniConst Bool True)) (EConst (UniConst Bool True)))) (EStatement (ELet (UniVar {_uniVarUni = Field, _uniVarVar = asf_30}) (EConst 1)) (EStatement (ELet (UniVar {_uniVarUni = Bool, _uniVarVar = ?as_31}) (EConst (UniConst Bool True))) (EStatement (ELet (UniVar {_uniVarUni = Vector, _uniVarVar = #as_32}) (EConst (UniConst Vector [True]))) (EConst (UniConst Bool True))))))))))))))))))))))))))))))))) \ No newline at end of file diff --git a/test/Field/golden/00-for-loops.field b/test/Field/golden/00-for-loops.field new file mode 100644 index 0000000..05453eb --- /dev/null +++ b/test/Field/golden/00-for-loops.field @@ -0,0 +1,11 @@ +for i = 1 to 2 do + let i' = i; + for j = 2 to 3 do + let k = i * j; + assert k == i' * j; + end; + let p = i; + for l = 1 to 2 do + let p = p * l; + end; +end; diff --git a/test/Field/golden/00-for-loops.golden b/test/Field/golden/00-for-loops.golden new file mode 100644 index 0000000..02113f3 --- /dev/null +++ b/test/Field/golden/00-for-loops.golden @@ -0,0 +1,11 @@ +for i_6 = 1 to 2 do +let i'_7 = i_6; +for j_8 = 2 to 3 do +let k_9 = i_6 * j_8; +assert k_9 == (i'_7 * j_8); +end; +let p_10 = i_6; +for l_11 = 1 to 2 do +let p_12 = p_10 * l_11; +end; +end; diff --git a/test/Field/golden/01-uniques.field b/test/Field/golden/01-uniques.field new file mode 100644 index 0000000..1840396 --- /dev/null +++ b/test/Field/golden/01-uniques.field @@ -0,0 +1,8 @@ +let a = a; +let a = a; +for a = 1 to 2 do + let a = a; + let a = a; +end; +let a = a; +let a = a; diff --git a/test/Field/golden/01-uniques.golden b/test/Field/golden/01-uniques.golden new file mode 100644 index 0000000..41b422e --- /dev/null +++ b/test/Field/golden/01-uniques.golden @@ -0,0 +1,8 @@ +let a_1 = a_0; +let a_2 = a_1; +for a_3 = 1 to 2 do +let a_4 = a_3; +let a_5 = a_4; +end; +let a_6 = a_5; +let a_7 = a_6; diff --git a/test/Field/golden/forLoops.golden b/test/Field/golden/forLoops.golden deleted file mode 100644 index 72ac548..0000000 --- a/test/Field/golden/forLoops.golden +++ /dev/null @@ -1 +0,0 @@ -let i'_6 = 1; let k_7 = 1 * 2; assert k_7 == (i'_6 * 2); let k_8 = 1 * 3; assert k_8 == (i'_6 * 3); let p_9 = 1; let p_10 = p_9 * 1; let p_11 = p_10 * 2; let i'_12 = 2; let k_13 = 2 * 2; assert k_13 == (i'_12 * 2); let k_14 = 2 * 3; assert k_14 == (i'_12 * 3); let p_15 = 2; let p_16 = p_15 * 1; let p_17 = p_16 * 2; p_17 \ No newline at end of file diff --git a/test/Main.hs b/test/Main.hs index d8f1e8d..e588c8e 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -2,7 +2,8 @@ module Main where import qualified Field.Axioms as Field (test_fields) import qualified Field.Raw.Textual as Raw (gen_test_parsing) -import qualified Field.Textual as Field (test_textual) +import qualified Field.Renaming as Field (test_renaming, test_free_variables) +import qualified Field.Textual as Field (gen_test_roundtrip, test_textual) import qualified Field.Typed.Textual as Field (gen_test_typechecking) import Test.Tasty @@ -10,11 +11,16 @@ import Test.Tasty test_all :: IO TestTree test_all = testGroup "all" <$> sequence - [ pure Field.test_fields + [ pure Field.test_free_variables + , pure Field.test_renaming + -- Old tests + , pure Field.test_fields , pure Field.test_textual + , Field.gen_test_roundtrip , Raw.gen_test_parsing , Field.gen_test_typechecking ] + main :: IO () main = defaultMain =<< test_all diff --git a/tiny-lang.cabal b/tiny-lang.cabal index 7c933dd..85b7b0f 100644 --- a/tiny-lang.cabal +++ b/tiny-lang.cabal @@ -23,6 +23,7 @@ library TinyLang.ParseUtils TinyLang.Prelude TinyLang.Var + TinyLang.Field.Core TinyLang.Field.Evaluator TinyLang.Field.Existential TinyLang.Field.Generator @@ -71,6 +72,22 @@ library -Wincomplete-uni-patterns -Wincomplete-record-updates -Wredundant-constraints -Widentities +benchmark bench-generators + type: exitcode-stdio-1.0 + main-is: Main.hs + hs-source-dirs: bench + default-language: Haskell2010 + build-depends: + tiny-lang, + base >= 4.7 && < 5, + QuickCheck + default-extensions: + BangPatterns + ghc-options: + -Wall + -Wincomplete-uni-patterns -Wincomplete-record-updates + -Wredundant-constraints -Widentities + test-suite tiny-lang-test type: exitcode-stdio-1.0 main-is: Main.hs @@ -79,6 +96,7 @@ test-suite tiny-lang-test Field.Textual Field.Axioms Field.Raw.Textual + Field.Renaming Field.TestUtils Field.Typed.Textual default-language: Haskell2010 @@ -95,7 +113,8 @@ test-suite tiny-lang-test tasty, tasty-golden, tasty-hunit, - tasty-quickcheck + tasty-quickcheck, + interpolate default-extensions: MultiParamTypeClasses, FlexibleContexts, FlexibleInstances ScopedTypeVariables, ConstraintKinds, DefaultSignatures