From 9b9cf10f5c53f788fe86af8473e24e60edcc9ac2 Mon Sep 17 00:00:00 2001 From: Nikolaos Bezirgiannis Date: Fri, 19 Jun 2020 13:13:09 +0200 Subject: [PATCH] Added the type pos&neg tests --- plutus-ir/plutus-ir.cabal | 5 +- .../src/Language/PlutusIR/Compiler/Error.hs | 8 ++ .../Language/PlutusIR/TypeCheck/Internal.hs | 94 ++++++++++--------- plutus-ir/test/Spec.hs | 9 +- plutus-ir/test/TestLib.hs | 24 ++++- plutus-ir/test/TypeSpec.hs | 55 +++++++++++ .../rectypebind => errors/recursiveTypeBind} | 0 .../test/errors/recursiveTypeBind.golden | 1 + plutus-ir/test/lets/rectypebind.golden | 13 --- .../type-errors/conflictingRecursiveBinds | 9 ++ .../conflictingRecursiveBinds.golden | 1 + .../test/type-errors/duplicateDataConstrs | 14 +++ .../type-errors/duplicateDataConstrs.golden | 1 + .../test/type-errors/duplicateTypeConstrs | 14 +++ .../type-errors/duplicateTypeConstrs.golden | 1 + .../type-errors/wrongDataConstrReturnType | 13 +++ .../wrongDataConstrReturnType.golden | 1 + plutus-ir/test/types/even3Eval | 27 ++++++ plutus-ir/test/types/even3Eval.golden | 1 + plutus-ir/test/types/ifError | 13 +++ plutus-ir/test/types/ifError.golden | 0 plutus-ir/test/types/letInLet | 14 +++ plutus-ir/test/types/letInLet.golden | 1 + plutus-ir/test/types/listMatch | 25 +++++ plutus-ir/test/types/listMatch.golden | 1 + plutus-ir/test/types/maybe | 16 ++++ plutus-ir/test/types/maybe.golden | 1 + plutus-ir/test/types/mutuallyRecursiveTypes | 21 +++++ .../test/types/mutuallyRecursiveTypes.golden | 1 + plutus-ir/test/types/mutuallyRecursiveValues | 6 ++ .../test/types/mutuallyRecursiveValues.golden | 1 + plutus-ir/test/types/nonrec1 | 14 +++ plutus-ir/test/types/nonrec1.golden | 1 + plutus-ir/test/types/nonrec2 | 20 ++++ plutus-ir/test/types/nonrec2.golden | 1 + plutus-ir/test/types/nonrec3 | 6 ++ plutus-ir/test/types/nonrec3.golden | 1 + plutus-ir/test/types/nonrec4 | 9 ++ plutus-ir/test/types/nonrec4.golden | 1 + plutus-ir/test/types/nonrec6 | 11 +++ plutus-ir/test/types/nonrec6.golden | 1 + plutus-ir/test/types/nonrec7 | 13 +++ plutus-ir/test/types/nonrec7.golden | 1 + plutus-ir/test/types/nonrec8 | 16 ++++ plutus-ir/test/types/nonrec8.golden | 1 + plutus-ir/test/types/nonrecToNonrec | 11 +++ plutus-ir/test/types/nonrecToNonrec.golden | 1 + plutus-ir/test/types/nonrecToRec | 11 +++ plutus-ir/test/types/nonrecToRec.golden | 1 + plutus-ir/test/types/oldLength | 12 +++ plutus-ir/test/types/oldLength.golden | 1 + plutus-ir/test/types/rec1 | 17 ++++ plutus-ir/test/types/rec1.golden | 1 + plutus-ir/test/types/rec2 | 24 +++++ plutus-ir/test/types/rec2.golden | 1 + plutus-ir/test/types/rec3 | 6 ++ plutus-ir/test/types/rec3.golden | 1 + plutus-ir/test/types/rec4 | 5 + plutus-ir/test/types/rec4.golden | 1 + plutus-ir/test/types/sameNameDifferentEnv | 14 +++ .../test/types/sameNameDifferentEnv.golden | 1 + plutus-ir/test/types/strictNonValue | 17 ++++ plutus-ir/test/types/strictNonValue.golden | 1 + plutus-ir/test/types/strictNonValue2 | 17 ++++ plutus-ir/test/types/strictNonValue2.golden | 1 + plutus-ir/test/types/strictNonValue3 | 14 +++ plutus-ir/test/types/strictNonValue3.golden | 1 + plutus-ir/test/types/strictValue | 12 +++ plutus-ir/test/types/strictValue.golden | 1 + plutus-ir/test/types/strictValueNonValue | 15 +++ .../test/types/strictValueNonValue.golden | 1 + plutus-ir/test/types/strictValueValue | 14 +++ plutus-ir/test/types/strictValueValue.golden | 1 + 73 files changed, 627 insertions(+), 63 deletions(-) create mode 100644 plutus-ir/test/TypeSpec.hs rename plutus-ir/test/{lets/rectypebind => errors/recursiveTypeBind} (100%) create mode 100644 plutus-ir/test/errors/recursiveTypeBind.golden delete mode 100644 plutus-ir/test/lets/rectypebind.golden create mode 100644 plutus-ir/test/type-errors/conflictingRecursiveBinds create mode 100644 plutus-ir/test/type-errors/conflictingRecursiveBinds.golden create mode 100644 plutus-ir/test/type-errors/duplicateDataConstrs create mode 100644 plutus-ir/test/type-errors/duplicateDataConstrs.golden create mode 100644 plutus-ir/test/type-errors/duplicateTypeConstrs create mode 100644 plutus-ir/test/type-errors/duplicateTypeConstrs.golden create mode 100644 plutus-ir/test/type-errors/wrongDataConstrReturnType create mode 100644 plutus-ir/test/type-errors/wrongDataConstrReturnType.golden create mode 100644 plutus-ir/test/types/even3Eval create mode 100644 plutus-ir/test/types/even3Eval.golden create mode 100644 plutus-ir/test/types/ifError create mode 100644 plutus-ir/test/types/ifError.golden create mode 100644 plutus-ir/test/types/letInLet create mode 100644 plutus-ir/test/types/letInLet.golden create mode 100644 plutus-ir/test/types/listMatch create mode 100644 plutus-ir/test/types/listMatch.golden create mode 100644 plutus-ir/test/types/maybe create mode 100644 plutus-ir/test/types/maybe.golden create mode 100644 plutus-ir/test/types/mutuallyRecursiveTypes create mode 100644 plutus-ir/test/types/mutuallyRecursiveTypes.golden create mode 100644 plutus-ir/test/types/mutuallyRecursiveValues create mode 100644 plutus-ir/test/types/mutuallyRecursiveValues.golden create mode 100644 plutus-ir/test/types/nonrec1 create mode 100644 plutus-ir/test/types/nonrec1.golden create mode 100644 plutus-ir/test/types/nonrec2 create mode 100644 plutus-ir/test/types/nonrec2.golden create mode 100644 plutus-ir/test/types/nonrec3 create mode 100644 plutus-ir/test/types/nonrec3.golden create mode 100644 plutus-ir/test/types/nonrec4 create mode 100644 plutus-ir/test/types/nonrec4.golden create mode 100644 plutus-ir/test/types/nonrec6 create mode 100644 plutus-ir/test/types/nonrec6.golden create mode 100644 plutus-ir/test/types/nonrec7 create mode 100644 plutus-ir/test/types/nonrec7.golden create mode 100644 plutus-ir/test/types/nonrec8 create mode 100644 plutus-ir/test/types/nonrec8.golden create mode 100644 plutus-ir/test/types/nonrecToNonrec create mode 100644 plutus-ir/test/types/nonrecToNonrec.golden create mode 100644 plutus-ir/test/types/nonrecToRec create mode 100644 plutus-ir/test/types/nonrecToRec.golden create mode 100644 plutus-ir/test/types/oldLength create mode 100644 plutus-ir/test/types/oldLength.golden create mode 100644 plutus-ir/test/types/rec1 create mode 100644 plutus-ir/test/types/rec1.golden create mode 100644 plutus-ir/test/types/rec2 create mode 100644 plutus-ir/test/types/rec2.golden create mode 100644 plutus-ir/test/types/rec3 create mode 100644 plutus-ir/test/types/rec3.golden create mode 100644 plutus-ir/test/types/rec4 create mode 100644 plutus-ir/test/types/rec4.golden create mode 100644 plutus-ir/test/types/sameNameDifferentEnv create mode 100644 plutus-ir/test/types/sameNameDifferentEnv.golden create mode 100644 plutus-ir/test/types/strictNonValue create mode 100644 plutus-ir/test/types/strictNonValue.golden create mode 100644 plutus-ir/test/types/strictNonValue2 create mode 100644 plutus-ir/test/types/strictNonValue2.golden create mode 100644 plutus-ir/test/types/strictNonValue3 create mode 100644 plutus-ir/test/types/strictNonValue3.golden create mode 100644 plutus-ir/test/types/strictValue create mode 100644 plutus-ir/test/types/strictValue.golden create mode 100644 plutus-ir/test/types/strictValueNonValue create mode 100644 plutus-ir/test/types/strictValueNonValue.golden create mode 100644 plutus-ir/test/types/strictValueValue create mode 100644 plutus-ir/test/types/strictValueValue.golden diff --git a/plutus-ir/plutus-ir.cabal b/plutus-ir/plutus-ir.cabal index a486d0d357c..13927763243 100644 --- a/plutus-ir/plutus-ir.cabal +++ b/plutus-ir/plutus-ir.cabal @@ -24,6 +24,7 @@ library Language.PlutusIR.Compiler Language.PlutusIR.Compiler.Names Language.PlutusIR.Compiler.Definitions + Language.PlutusIR.Compiler.Error Language.PlutusIR.Generators.AST Language.PlutusIR.Parser Language.PlutusIR.MkPir @@ -34,11 +35,11 @@ library Language.PlutusIR.Transform.Rename Language.PlutusIR.Transform.NonStrict Language.PlutusIR.Transform.LetFloat + Language.PlutusIR.TypeCheck hs-source-dirs: src other-modules: Language.PlutusIR.Analysis.Dependencies Language.PlutusIR.Analysis.Usages - Language.PlutusIR.Compiler.Error Language.PlutusIR.Compiler.Let Language.PlutusIR.Compiler.Datatype Language.PlutusIR.Compiler.Provenance @@ -46,7 +47,6 @@ library Language.PlutusIR.Compiler.Types Language.PlutusIR.Compiler.Lower Language.PlutusIR.Normalize - Language.PlutusIR.TypeCheck Language.PlutusIR.TypeCheck.Internal default-language: Haskell2010 default-extensions: ExplicitForAll ScopedTypeVariables @@ -89,6 +89,7 @@ test-suite plutus-ir-test OptimizerSpec TransformSpec ParserSpec + TypeSpec TestLib default-language: Haskell2010 build-depends: diff --git a/plutus-ir/src/Language/PlutusIR/Compiler/Error.hs b/plutus-ir/src/Language/PlutusIR/Compiler/Error.hs index f1c9766c999..b9f7be483cc 100644 --- a/plutus-ir/src/Language/PlutusIR/Compiler/Error.hs +++ b/plutus-ir/src/Language/PlutusIR/Compiler/Error.hs @@ -50,6 +50,14 @@ data TypeError uni ann | InternalTypeErrorE ann (PLC.InternalTypeError uni ann) | FreeTypeVariableE ann PLC.TyName | FreeVariableE ann PLC.Name + -- FIXME: attach info + | ConflictingRecBinds + | DuplicateDeclaredIdent ann T.Text + | MalformedDataConstrResType ann + -- expected + (PLC.Type PLC.TyName uni ()) + -- actual + (PLC.Normalized (PLC.Type PLC.TyName uni ())) -- TODO: enable back deriving NFData because PIR.Term does not have it -- TODO: enable back deriving Eq because PIR.Term does not have it, see similar src/Language/PlutusCore/Core/Instance/Eq.hs deriving (Show, Generic) diff --git a/plutus-ir/src/Language/PlutusIR/TypeCheck/Internal.hs b/plutus-ir/src/Language/PlutusIR/TypeCheck/Internal.hs index edaac683462..36f37d1e85c 100644 --- a/plutus-ir/src/Language/PlutusIR/TypeCheck/Internal.hs +++ b/plutus-ir/src/Language/PlutusIR/TypeCheck/Internal.hs @@ -40,13 +40,15 @@ import Data.Foldable import Control.Monad.Except import Control.Monad.Reader import Control.Lens.TH +import Control.Lens import qualified Language.PlutusCore.Normalize.Internal as Norm import qualified Language.PlutusCore.Core as PLC import Data.Map (Map) import qualified Data.Map as Map import qualified Language.PlutusIR.MkPir as PIR - +import Data.List +import qualified Data.Text as T {- Note [Global uniqueness] WARNING: type inference/checking works under the assumption that the global uniqueness condition is satisfied. The invariant is not checked, enforced or automatically fulfilled. So you must ensure @@ -435,9 +437,18 @@ inferTypeM (Let ann recurs bs inTerm) = do inferTypeM inTerm -- G !- inTerm :: * -- TODO: here is the problem of existential-type escaping - checkKindM ann (ann <$ unNormalized tyInTerm) $ Type () + -- FIXME: reenable the check + -- checkKindM ann (ann <$ unNormalized tyInTerm) $ Type () pure tyInTerm + where + withBinds :: forall uni ann a. NonEmpty (Binding TyName Name uni ann) -> TypeCheckM uni ann a -> TypeCheckM uni ann a + withBinds = flip . foldr $ withBind + + checkWellformBinds :: forall uni ann. (GShow uni, GEq uni, DefaultUni <: uni) + => NonEmpty (Binding TyName Name uni ann) -> TypeCheckM uni ann () + checkWellformBinds = traverse_ checkWellformBind + -- See the [Global uniqueness] and [Type rules] notes. -- | Check a 'Term' against a 'NormalizedType'. @@ -452,8 +463,9 @@ checkTypeM ann term vTy = do vTermTy <- inferTypeM term when (vTermTy /= vTy) $ throwError (TypeMismatch ann (void term) (unNormalized vTermTy) vTy) --- | extends the environment with a bind. --- NOTE: does not do any check of binds-name collision checks (which is needed for letrec) +-- | Extends the environment(s) with a bind. +-- NOTE: there are no well-formed or duplication checks here, it just adds to the environment(s) like withVar/withTyVar do. +-- For checks see `checkWellformBind`. withBind :: forall uni ann a. Binding TyName Name uni ann -> TypeCheckM uni ann a @@ -461,7 +473,7 @@ withBind :: forall uni ann a. withBind b m = case b of TermBind _ _ (VarDecl _ n ty) _rhs -> do -- OPTIMIZE: redundant, usually this function is called together with `checkWellformBind`, - -- which performs normalization here as well + -- which performs normalization there as well vTy <- normalizeTypeM $ void ty withVar n vTy m TypeBind _ (TyVarDecl _ tn k) _rhs -> @@ -506,11 +518,6 @@ withBind b m = case b of vdecls ) -withBinds :: forall uni ann a. - NonEmpty (Binding TyName Name uni ann) - -> TypeCheckM uni ann a - -> TypeCheckM uni ann a -withBinds = flip . foldr $ withBind -- | check that a binding is well-formed (correctly typed, kinded) checkWellformBind :: forall uni ann. @@ -526,39 +533,39 @@ checkWellformBind = \case checkTypeM ann rhs vTy TypeBind _ (TyVarDecl ann _ k) rhs -> checkKindM ann rhs (void k) - DatatypeBind _ (Datatype _ (TyVarDecl _ dt _) tvdecls _des vdecls) -> - -- add the type-arguments to environment + DatatypeBind _ (Datatype ann tvdecl@(TyVarDecl _ dataName _) tvdecls des vdecls) -> do + assertNoDuplicate allNewTyNames + assertNoDuplicate allNewNames foldr (\(TyVarDecl _ tn k) -> withTyVar tn (void k)) - -- check the data-constructors' argument-types to be kinded by * - (traverse_ - (\(VarDecl ann _ ty) -> do - checkKindM ann ty $ Type () - -- check that the normalized result-type of the data-constructor is - -- of the form `[DT tyarg1 tyarg2 ... tyargn]` - -- Q: is this normalization absolutely necessary? - actualConstrResultType <- normalizeTypeM $ void ty - -- TODO: after GADTs are added to the language the expected constructor result type - -- has to be "relaxed" from `[DT tyarg1 ... tyargn]` to `[DT Same Arity As ... Tvdecls]` - -- i.e. we should only check that `DT` is applied to the correct *number* of tyargs as the number of tvdecls, - let expectedConstrResultType = foldl - (\acc (TyVarDecl _ tyarg _) -> TyApp () acc $ TyVar () tyarg) - (TyVar () dt) - tvdecls - when (expectedConstrResultType /= unNormalized actualConstrResultType) $ - -- TODO: probably introduce a more specialized constructor type error, - -- because we don't have a valid "occuring-in-term" to put in the typemismatch-error - throwError $ TypeMismatch ann dummyTerm expectedConstrResultType actualConstrResultType - ) - vdecls) - tvdecls - -checkWellformBinds :: forall uni ann. - (GShow uni, GEq uni, DefaultUni <: uni) - => NonEmpty (Binding TyName Name uni ann) - -> TypeCheckM uni ann () -checkWellformBinds = traverse_ checkWellformBind - - + -- check the data-constructors' argument-types to be kinded by * + (traverse_ + (\(VarDecl ann1 _ ty) -> do + checkKindM ann ty $ Type () + -- check that the normalized result-type of the data-constructor is + -- of the form `[DT tyarg1 tyarg2 ... tyargn]` + -- Q: is this normalization absolutely necessary? + actualConstrResultType <- constrResultTy <$> normalizeTypeM (void ty) + -- TODO: after GADTs are added to the language the expected constructor result type + -- has to be "relaxed" from `[DT tyarg1 ... tyargn]` to `[DT Same Arity As ... Tvdecls]` + -- i.e. we should only check that `DT` is applied to the correct *number* of tyargs as the number of tvdecls. + let expectedConstrResultType = foldl + (\acc (TyVarDecl _ tyarg _) -> TyApp () acc $ TyVar () tyarg) + (TyVar () dataName) + tvdecls + when (expectedConstrResultType /= unNormalized actualConstrResultType) $ + throwError $ MalformedDataConstrResType ann1 expectedConstrResultType actualConstrResultType + ) + vdecls) + allNewTyDecls + where + allNewTyDecls = tvdecl:tvdecls + allNewTyNames = fmap (nameString . unTyName . tyVarDeclName) allNewTyDecls + allNewNames = nameString des : fmap (nameString . varDeclName) vdecls + + assertNoDuplicate :: [T.Text] -> TypeCheckM uni ann () + assertNoDuplicate = maybe (pure ()) + (throwError . DuplicateDeclaredIdent ann) + . hasDuplicate -- HELPERS -- | Get the result type of a constructor's type that has been prior normalized. @@ -574,3 +581,6 @@ constrResultTy (Normalized t) = Normalized $ constrResultTy' t -- TyForall _ _ _ t -> constrResultTy' t t' -> t' +hasDuplicate :: Ord a => [a] -> Maybe a +hasDuplicate l = head <$> (find (\ g -> length g > 1) . group $ sort l) + diff --git a/plutus-ir/test/Spec.hs b/plutus-ir/test/Spec.hs index def53d2943a..75457503b62 100644 --- a/plutus-ir/test/Spec.hs +++ b/plutus-ir/test/Spec.hs @@ -15,6 +15,7 @@ import TestLib import OptimizerSpec import ParserSpec import TransformSpec +import TypeSpec import Language.PlutusCore.Pretty (PrettyConst) import Language.PlutusCore.Quote @@ -35,7 +36,6 @@ import Control.Monad.Morph import Control.Monad.Reader import Data.Functor.Identity -import Text.Megaparsec.Pos main :: IO () main = defaultMain $ runTestNestedIn ["test"] tests @@ -45,9 +45,6 @@ instance ( PLC.GShow uni, PLC.GEq uni, PLC.DefaultUni PLC.<: uni ) => GetProgram (Term TyName Name uni a) uni where getProgram = asIfThrown . fmap (trivialProgram . void) . compileAndMaybeTypecheck True -instance Pretty SourcePos where - pretty = pretty . sourcePosPretty - -- | Adapt an computation that keeps its errors in an 'Except' into one that looks as if it caught them in 'IO'. asIfThrown :: Exception e @@ -76,6 +73,8 @@ tests = testGroup "plutus-ir" <$> sequence , errors , optimizer , transform + , types + , typeErrors ] prettyprinting :: TestNested @@ -89,7 +88,6 @@ lets :: TestNested lets = testNested "lets" [ goldenPlcFromPir term "letInLet" , goldenPlcFromPir term "letDep" - , goldenPlcFromPir term "rectypebind" ] datatypes :: TestNested @@ -122,4 +120,5 @@ roundTripPirTerm = deserialise . serialise . void errors :: TestNested errors = testNested "errors" [ goldenPlcFromPirCatch term "mutuallyRecursiveTypes" + , goldenPlcFromPirCatch term "recursiveTypeBind" ] diff --git a/plutus-ir/test/TestLib.hs b/plutus-ir/test/TestLib.hs index af06991a0f1..891ebc33d2e 100644 --- a/plutus-ir/test/TestLib.hs +++ b/plutus-ir/test/TestLib.hs @@ -1,5 +1,6 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} module TestLib where import Common @@ -13,11 +14,15 @@ import Control.Monad.Reader as Reader import qualified Language.PlutusCore.DeBruijn as PLC import Language.PlutusCore.Pretty import Language.PlutusCore.Quote +import Language.PlutusCore.Rename import qualified Language.PlutusCore.Universe as PLC import Language.PlutusIR import Language.PlutusIR.Parser as Parser - +import Language.PlutusIR.Compiler.Error as PIR +import Language.PlutusIR.TypeCheck import System.FilePath (joinPath, ()) +import Data.Text.Prettyprint.Doc +import Text.Megaparsec.Pos import Text.Megaparsec.Error as Megaparsec @@ -58,3 +63,20 @@ goldenPlcFromPirCatch = goldenPirM (\ast -> ppCatch $ do goldenEvalPir :: (GetProgram a PLC.DefaultUni) => Parser a -> String -> TestNested goldenEvalPir = goldenPirM (\ast -> ppThrow $ runPlc [ast]) + + +goldenTypeFromPir :: forall a. (Pretty a, Typeable a) + => Parser (Term TyName Name PLC.DefaultUni a) -> String -> TestNested +goldenTypeFromPir = goldenPirM (\ast -> ppThrow $ + withExceptT (toException :: PIR.Error PLC.DefaultUni a -> SomeException) $ runQuoteT $ inferType defConfig ast) + +goldenTypeFromPirCatch :: forall a. (Pretty a, Typeable a) + => Parser (Term TyName Name PLC.DefaultUni a) -> String -> TestNested +goldenTypeFromPirCatch = goldenPirM (\ast -> ppCatch $ + withExceptT (toException :: PIR.Error PLC.DefaultUni a -> SomeException) $ runQuoteT $ inferType defConfig ast) + + +-- TODO: perhaps move to Common.hs +instance Pretty SourcePos where + pretty = pretty . sourcePosPretty + diff --git a/plutus-ir/test/TypeSpec.hs b/plutus-ir/test/TypeSpec.hs new file mode 100644 index 00000000000..9880f4936da --- /dev/null +++ b/plutus-ir/test/TypeSpec.hs @@ -0,0 +1,55 @@ +module TypeSpec where + +import Common +import TestLib + +import Language.PlutusCore.Quote + +import qualified Language.PlutusCore as PLC +import Language.PlutusIR.Parser +import qualified Language.PlutusIR.Transform.LetFloat as LetFloat +import qualified Language.PlutusIR.Transform.NonStrict as NonStrict +import Language.PlutusIR.Transform.Rename () +import qualified Language.PlutusIR.Transform.ThunkRecursions as ThunkRec + +types :: TestNested +types = testNested "types" + $ map (goldenTypeFromPir term) + [ "letInLet" + ,"listMatch" + ,"maybe" + ,"ifError" + ,"mutuallyRecursiveTypes" + ,"mutuallyRecursiveValues" + ,"nonrec1" + ,"nonrec2" + ,"nonrec3" + ,"nonrec4" + ,"nonrec6" + ,"nonrec7" + ,"nonrec8" + ,"rec1" + ,"rec2" + ,"rec3" + ,"rec4" + ,"nonrecToRec" + ,"nonrecToNonrec" + ,"oldLength" + ,"strictValue" + ,"strictNonValue" + ,"strictNonValue2" + ,"strictNonValue3" + ,"strictValueNonValue" + ,"strictValueValue" + ,"even3Eval" + ,"sameNameDifferentEnv" + ] + +typeErrors :: TestNested +typeErrors = testNested "type-errors" + $ map (goldenTypeFromPirCatch term) + [ "conflictingRecursiveBinds" + , "duplicateDataConstrs" + , "duplicateTypeConstrs" + , "wrongDataConstrReturnType" + ] diff --git a/plutus-ir/test/lets/rectypebind b/plutus-ir/test/errors/recursiveTypeBind similarity index 100% rename from plutus-ir/test/lets/rectypebind rename to plutus-ir/test/errors/recursiveTypeBind diff --git a/plutus-ir/test/errors/recursiveTypeBind.golden b/plutus-ir/test/errors/recursiveTypeBind.golden new file mode 100644 index 00000000000..f63b924ccc7 --- /dev/null +++ b/plutus-ir/test/errors/recursiveTypeBind.golden @@ -0,0 +1 @@ +Error during compilation: Type bindings cannot appear in recursive let, use datatypebind instead((recursive) let binding; from recursiveTypeBind:1:2) \ No newline at end of file diff --git a/plutus-ir/test/lets/rectypebind.golden b/plutus-ir/test/lets/rectypebind.golden deleted file mode 100644 index bc7b366caaa..00000000000 --- a/plutus-ir/test/lets/rectypebind.golden +++ /dev/null @@ -1,13 +0,0 @@ -(program 1.0.0 - { - (abs - unit_i0 - (type) - [ - (lam lazyVal_i0 (fun unit_i2 (con integer)) lazyVal_i1) - (lam x_i0 unit_i2 (con 3)) - ] - ) - (all a_i0 (type) (fun a_i1 a_i1)) - } -) \ No newline at end of file diff --git a/plutus-ir/test/type-errors/conflictingRecursiveBinds b/plutus-ir/test/type-errors/conflictingRecursiveBinds new file mode 100644 index 00000000000..4b4fe6c0598 --- /dev/null +++ b/plutus-ir/test/type-errors/conflictingRecursiveBinds @@ -0,0 +1,9 @@ +(lam x (con integer) +(let + (rec) + (termbind (strict) (vardecl j (con integer)) (con 3)) + (termbind (strict) (vardecl j (con integer)) (con 3)) + (con 5) + ) + ) + diff --git a/plutus-ir/test/type-errors/conflictingRecursiveBinds.golden b/plutus-ir/test/type-errors/conflictingRecursiveBinds.golden new file mode 100644 index 00000000000..63842ebe8d4 --- /dev/null +++ b/plutus-ir/test/type-errors/conflictingRecursiveBinds.golden @@ -0,0 +1 @@ +(fun (con integer) (con integer)) \ No newline at end of file diff --git a/plutus-ir/test/type-errors/duplicateDataConstrs b/plutus-ir/test/type-errors/duplicateDataConstrs new file mode 100644 index 00000000000..afbc88488d2 --- /dev/null +++ b/plutus-ir/test/type-errors/duplicateDataConstrs @@ -0,0 +1,14 @@ +(let + (nonrec) + (datatypebind + (datatype + (tyvardecl Maybe (fun (type) (type))) + (tyvardecl a (type)) + match_Maybe + (vardecl Nothing [Maybe a]) + (vardecl Just (fun a [Maybe a])) + (vardecl Just [Maybe a]) + ) + ) + (con 5) +) diff --git a/plutus-ir/test/type-errors/duplicateDataConstrs.golden b/plutus-ir/test/type-errors/duplicateDataConstrs.golden new file mode 100644 index 00000000000..6185010d65b --- /dev/null +++ b/plutus-ir/test/type-errors/duplicateDataConstrs.golden @@ -0,0 +1 @@ +Error from the PIR typechecker: \ No newline at end of file diff --git a/plutus-ir/test/type-errors/duplicateTypeConstrs b/plutus-ir/test/type-errors/duplicateTypeConstrs new file mode 100644 index 00000000000..bad066d9c11 --- /dev/null +++ b/plutus-ir/test/type-errors/duplicateTypeConstrs @@ -0,0 +1,14 @@ +(let + (nonrec) + (datatypebind + (datatype + (tyvardecl Either (fun (type) (fun (type) (type)))) + (tyvardecl a (type)) + (tyvardecl a (type)) + match_Either + (vardecl Right (fun a [Either a a])) + (vardecl Left (fun a [Either a a])) + ) + ) + (con 5) +) diff --git a/plutus-ir/test/type-errors/duplicateTypeConstrs.golden b/plutus-ir/test/type-errors/duplicateTypeConstrs.golden new file mode 100644 index 00000000000..6185010d65b --- /dev/null +++ b/plutus-ir/test/type-errors/duplicateTypeConstrs.golden @@ -0,0 +1 @@ +Error from the PIR typechecker: \ No newline at end of file diff --git a/plutus-ir/test/type-errors/wrongDataConstrReturnType b/plutus-ir/test/type-errors/wrongDataConstrReturnType new file mode 100644 index 00000000000..36b8f7cdcc7 --- /dev/null +++ b/plutus-ir/test/type-errors/wrongDataConstrReturnType @@ -0,0 +1,13 @@ +(let + (nonrec) + (datatypebind + (datatype + (tyvardecl Maybe (fun (type) (type))) + (tyvardecl a (type)) + match_Maybe + (vardecl Nothing [Maybe a]) + (vardecl Just (fun a [Maybe (con integer)])) + ) + ) + (con 5) +) diff --git a/plutus-ir/test/type-errors/wrongDataConstrReturnType.golden b/plutus-ir/test/type-errors/wrongDataConstrReturnType.golden new file mode 100644 index 00000000000..6185010d65b --- /dev/null +++ b/plutus-ir/test/type-errors/wrongDataConstrReturnType.golden @@ -0,0 +1 @@ +Error from the PIR typechecker: \ No newline at end of file diff --git a/plutus-ir/test/types/even3Eval b/plutus-ir/test/types/even3Eval new file mode 100644 index 00000000000..45000cf7090 --- /dev/null +++ b/plutus-ir/test/types/even3Eval @@ -0,0 +1,27 @@ +(let (rec) + (datatypebind (datatype + (tyvardecl Nat (type)) + -- no arguments + match_Nat + (vardecl Zero Nat) + (vardecl Suc (fun Nat Nat)))) +(let (nonrec) + (datatypebind (datatype + (tyvardecl Bool (type)) + -- no arguments + match_Bool + (vardecl True Bool) + (vardecl False Bool))) + (termbind (strict) (vardecl three Nat) + [Suc [Suc [Suc Zero]]]) +(let (rec) + (termbind (strict) (vardecl even (fun Nat Bool)) + (lam n Nat + [{[match_Nat n] Bool} True (lam pred Nat [odd pred])])) + (termbind (strict) (vardecl odd (fun Nat Bool)) + (lam n Nat + [{[match_Nat n] Bool} False (lam pred Nat [even pred])])) + [even three] +) +) +) diff --git a/plutus-ir/test/types/even3Eval.golden b/plutus-ir/test/types/even3Eval.golden new file mode 100644 index 00000000000..b6c1aac0542 --- /dev/null +++ b/plutus-ir/test/types/even3Eval.golden @@ -0,0 +1 @@ +Bool_4 \ No newline at end of file diff --git a/plutus-ir/test/types/ifError b/plutus-ir/test/types/ifError new file mode 100644 index 00000000000..2f0740ba86b --- /dev/null +++ b/plutus-ir/test/types/ifError @@ -0,0 +1,13 @@ +[ (lam b (all a (type) (fun (fun (con integer) a) (fun (fun (con integer) a) a))) + [ b + (lam z (con integer) + (let + (nonrec) + (termbind (strict) (vardecl err (con integer)) (error (con integer))) + err + ) + ) + (lam z (con integer) (con 1)) + ]) + (abs a (type) (lam x (fun (con integer) a) (lam y (fun (con integer) a) [y (con 0)]))) +] diff --git a/plutus-ir/test/types/ifError.golden b/plutus-ir/test/types/ifError.golden new file mode 100644 index 00000000000..e69de29bb2d diff --git a/plutus-ir/test/types/letInLet b/plutus-ir/test/types/letInLet new file mode 100644 index 00000000000..cdb344a6b14 --- /dev/null +++ b/plutus-ir/test/types/letInLet @@ -0,0 +1,14 @@ +(let + (nonrec) + (termbind (strict) + (vardecl unitval2 (all a (type) (fun a a))) + (let + (nonrec) + (termbind (strict) + (vardecl unitval (all a (type) (fun a a))) (abs a (type) (lam x a x)) + ) + unitval + ) + ) + unitval2 +) diff --git a/plutus-ir/test/types/letInLet.golden b/plutus-ir/test/types/letInLet.golden new file mode 100644 index 00000000000..18b6aec44b2 --- /dev/null +++ b/plutus-ir/test/types/letInLet.golden @@ -0,0 +1 @@ +(all a_7 (type) (fun a_7 a_7)) \ No newline at end of file diff --git a/plutus-ir/test/types/listMatch b/plutus-ir/test/types/listMatch new file mode 100644 index 00000000000..2ccf785b0c3 --- /dev/null +++ b/plutus-ir/test/types/listMatch @@ -0,0 +1,25 @@ +(lam x (con integer) +(let (rec) + (termbind (strict) (vardecl j (con integer)) [(builtin addInteger) (con 3) x]) + (datatypebind + (datatype + (tyvardecl List (fun (type) (type))) + (tyvardecl a (type)) + match_List + (vardecl Nil [List a]) (vardecl Cons (fun a (fun [List a] [List a]))) + ) + ) + [ + [ + { + [{match_List (all a (type) (fun a a))} {Nil (all a (type) (fun a a))}] + (all a (type) (fun a a)) + } + (abs a (type) (lam x a x)) + ] + (lam head (all a (type) (fun a a)) + (lam tail [List (all a (type) (fun a a))] head) + ) + ] +) +) \ No newline at end of file diff --git a/plutus-ir/test/types/listMatch.golden b/plutus-ir/test/types/listMatch.golden new file mode 100644 index 00000000000..5d624d2072e --- /dev/null +++ b/plutus-ir/test/types/listMatch.golden @@ -0,0 +1 @@ +(fun (con integer) (all a_26 (type) (fun a_26 a_26))) \ No newline at end of file diff --git a/plutus-ir/test/types/maybe b/plutus-ir/test/types/maybe new file mode 100644 index 00000000000..44ac3dfe40e --- /dev/null +++ b/plutus-ir/test/types/maybe @@ -0,0 +1,16 @@ +(lam x (con integer) +(let + (nonrec) + (termbind (strict) (vardecl j (con integer)) [(builtin addInteger) (con 3) x]) + (datatypebind + (datatype + (tyvardecl Maybe (fun (type) (type))) + (tyvardecl a (type)) + match_Maybe + (vardecl Nothing [Maybe a]) (vardecl Just (fun a [Maybe a])) + ) + ) + [ { Just (all a (type) (fun a a)) } (abs a (type) (lam x a x)) ] +) + ) + diff --git a/plutus-ir/test/types/maybe.golden b/plutus-ir/test/types/maybe.golden new file mode 100644 index 00000000000..964fb00b25c --- /dev/null +++ b/plutus-ir/test/types/maybe.golden @@ -0,0 +1 @@ +(fun (con integer) [Maybe_2 (all a_13 (type) (fun a_13 a_13))]) \ No newline at end of file diff --git a/plutus-ir/test/types/mutuallyRecursiveTypes b/plutus-ir/test/types/mutuallyRecursiveTypes new file mode 100644 index 00000000000..8ea6b217bb3 --- /dev/null +++ b/plutus-ir/test/types/mutuallyRecursiveTypes @@ -0,0 +1,21 @@ +(let + (rec) + (datatypebind + (datatype + (tyvardecl Tree (fun (type) (type))) + (tyvardecl a (type)) + match_Tree + (vardecl Node (fun a (fun [Forest a] [Tree a]))) + ) + ) + (datatypebind + (datatype + (tyvardecl Forest (fun (type) (type))) + (tyvardecl a (type)) + match_Forest + (vardecl Nil [Forest a]) + (vardecl Cons (fun [Tree a] (fun [Forest a] [Forest a]))) + ) + ) + { Nil (all a (type) (fun a a)) } +) diff --git a/plutus-ir/test/types/mutuallyRecursiveTypes.golden b/plutus-ir/test/types/mutuallyRecursiveTypes.golden new file mode 100644 index 00000000000..fdf8228eaa4 --- /dev/null +++ b/plutus-ir/test/types/mutuallyRecursiveTypes.golden @@ -0,0 +1 @@ +[Forest_3 (all a_13 (type) (fun a_13 a_13))] \ No newline at end of file diff --git a/plutus-ir/test/types/mutuallyRecursiveValues b/plutus-ir/test/types/mutuallyRecursiveValues new file mode 100644 index 00000000000..03066e223f3 --- /dev/null +++ b/plutus-ir/test/types/mutuallyRecursiveValues @@ -0,0 +1,6 @@ +(let + (rec) + (termbind (strict) (vardecl x (all a (type) (fun a a))) y) + (termbind (strict) (vardecl y (all a (type) (fun a a))) (abs a (type) (lam z a [{x a} z]))) + x +) \ No newline at end of file diff --git a/plutus-ir/test/types/mutuallyRecursiveValues.golden b/plutus-ir/test/types/mutuallyRecursiveValues.golden new file mode 100644 index 00000000000..5a74f4989ec --- /dev/null +++ b/plutus-ir/test/types/mutuallyRecursiveValues.golden @@ -0,0 +1 @@ +(all a_8 (type) (fun a_8 a_8)) \ No newline at end of file diff --git a/plutus-ir/test/types/nonrec1 b/plutus-ir/test/types/nonrec1 new file mode 100644 index 00000000000..0e85b3d205b --- /dev/null +++ b/plutus-ir/test/types/nonrec1 @@ -0,0 +1,14 @@ +(let + (nonrec) + (termbind (strict) (vardecl i2 (con integer)) (con 3)) + (termbind (strict) (vardecl j (con integer)) (con 3)) + (let + (nonrec) + (termbind + (strict) + (vardecl i1 (con integer)) + [ [ (builtin addInteger) i2 ] (con 3) ] + ) + [ [ (builtin addInteger) (con 5) ] [ [ (builtin addInteger) j ] i2 ] ] + ) +) diff --git a/plutus-ir/test/types/nonrec1.golden b/plutus-ir/test/types/nonrec1.golden new file mode 100644 index 00000000000..a1674e0be4b --- /dev/null +++ b/plutus-ir/test/types/nonrec1.golden @@ -0,0 +1 @@ +(con integer) \ No newline at end of file diff --git a/plutus-ir/test/types/nonrec2 b/plutus-ir/test/types/nonrec2 new file mode 100644 index 00000000000..0f326989875 --- /dev/null +++ b/plutus-ir/test/types/nonrec2 @@ -0,0 +1,20 @@ +(lam x (con integer) +(let (nonrec) + (termbind (strict) (vardecl i2 (con integer)) (con 2)) + (let (nonrec) + (termbind (strict) (vardecl i1 (con integer)) [(builtin addInteger) i2 (con 1)]) + (let (nonrec) + (termbind (strict) (vardecl i (con integer)) + [(builtin addInteger) i1 + [(builtin addInteger) x + [(builtin addInteger) i2 + (let (nonrec) + (termbind (strict) (vardecl j (con integer)) (con 0)) j)] + ]]) + [(builtin addInteger) i + (let (nonrec) + (termbind (strict) (vardecl j1 (con integer)) (con 0)) j1) + ] + ) + ) + )) diff --git a/plutus-ir/test/types/nonrec2.golden b/plutus-ir/test/types/nonrec2.golden new file mode 100644 index 00000000000..63842ebe8d4 --- /dev/null +++ b/plutus-ir/test/types/nonrec2.golden @@ -0,0 +1 @@ +(fun (con integer) (con integer)) \ No newline at end of file diff --git a/plutus-ir/test/types/nonrec3 b/plutus-ir/test/types/nonrec3 new file mode 100644 index 00000000000..38fe1fbb02f --- /dev/null +++ b/plutus-ir/test/types/nonrec3 @@ -0,0 +1,6 @@ +(lam x (con integer) +(let (nonrec) + (termbind (strict) (vardecl i (con integer)) + [(lam y (con integer) [(builtin addInteger) y x]) (con 1)]) + i + )) diff --git a/plutus-ir/test/types/nonrec3.golden b/plutus-ir/test/types/nonrec3.golden new file mode 100644 index 00000000000..63842ebe8d4 --- /dev/null +++ b/plutus-ir/test/types/nonrec3.golden @@ -0,0 +1 @@ +(fun (con integer) (con integer)) \ No newline at end of file diff --git a/plutus-ir/test/types/nonrec4 b/plutus-ir/test/types/nonrec4 new file mode 100644 index 00000000000..4d9c50dc941 --- /dev/null +++ b/plutus-ir/test/types/nonrec4 @@ -0,0 +1,9 @@ +(let (nonrec) + (termbind (strict) (vardecl i (con integer)) (con 3)) + [(lam x (con integer) + (let (nonrec) + (termbind (strict) (vardecl j (con integer)) [(builtin addInteger) i (con 1)]) + j + )) (con 4)] +) + diff --git a/plutus-ir/test/types/nonrec4.golden b/plutus-ir/test/types/nonrec4.golden new file mode 100644 index 00000000000..a1674e0be4b --- /dev/null +++ b/plutus-ir/test/types/nonrec4.golden @@ -0,0 +1 @@ +(con integer) \ No newline at end of file diff --git a/plutus-ir/test/types/nonrec6 b/plutus-ir/test/types/nonrec6 new file mode 100644 index 00000000000..c79ece08f65 --- /dev/null +++ b/plutus-ir/test/types/nonrec6 @@ -0,0 +1,11 @@ +(lam x (con integer) +(let (nonrec) + (termbind (strict) (vardecl i (con integer)) + (let (nonrec) + (termbind (strict) (vardecl j (con integer)) + [(builtin addInteger) (con 1) x]) + j) + ) + i + )) + diff --git a/plutus-ir/test/types/nonrec6.golden b/plutus-ir/test/types/nonrec6.golden new file mode 100644 index 00000000000..63842ebe8d4 --- /dev/null +++ b/plutus-ir/test/types/nonrec6.golden @@ -0,0 +1 @@ +(fun (con integer) (con integer)) \ No newline at end of file diff --git a/plutus-ir/test/types/nonrec7 b/plutus-ir/test/types/nonrec7 new file mode 100644 index 00000000000..75baaf81c3b --- /dev/null +++ b/plutus-ir/test/types/nonrec7 @@ -0,0 +1,13 @@ +(let (nonrec) + (termbind (strict) (vardecl i (con integer)) + [(lam x (con integer) + (let (nonrec) + (termbind (strict) (vardecl j (con integer)) + [(builtin addInteger) (con 1) x]) + j) + ) + (con 1)] + ) + i + ) + diff --git a/plutus-ir/test/types/nonrec7.golden b/plutus-ir/test/types/nonrec7.golden new file mode 100644 index 00000000000..a1674e0be4b --- /dev/null +++ b/plutus-ir/test/types/nonrec7.golden @@ -0,0 +1 @@ +(con integer) \ No newline at end of file diff --git a/plutus-ir/test/types/nonrec8 b/plutus-ir/test/types/nonrec8 new file mode 100644 index 00000000000..0f9dd4dab55 --- /dev/null +++ b/plutus-ir/test/types/nonrec8 @@ -0,0 +1,16 @@ +(let (nonrec) + (termbind (strict) (vardecl i (con integer)) + [(lam x (con integer) + (let (nonrec) + (termbind (strict) (vardecl k (con integer)) + (con 1)) + (let (nonrec) + (termbind (strict) (vardecl j (con integer)) + [(builtin addInteger) k [(builtin addInteger) (con 1) x]]) + j) + )) + (con 1)] + ) + i + ) + diff --git a/plutus-ir/test/types/nonrec8.golden b/plutus-ir/test/types/nonrec8.golden new file mode 100644 index 00000000000..a1674e0be4b --- /dev/null +++ b/plutus-ir/test/types/nonrec8.golden @@ -0,0 +1 @@ +(con integer) \ No newline at end of file diff --git a/plutus-ir/test/types/nonrecToNonrec b/plutus-ir/test/types/nonrecToNonrec new file mode 100644 index 00000000000..13ce83a28a5 --- /dev/null +++ b/plutus-ir/test/types/nonrecToNonrec @@ -0,0 +1,11 @@ +(let (rec) + (termbind (strict) (vardecl r (con integer)) + (let (nonrec) + -- since `i` is strictNonValue, it will not be moved/floated, + -- thus `i` will remain nonrec + (termbind (strict) (vardecl i (con integer)) + (let (nonrec) + (termbind (strict) (vardecl j (con integer)) r) + j)) + i)) + (con 3)) diff --git a/plutus-ir/test/types/nonrecToNonrec.golden b/plutus-ir/test/types/nonrecToNonrec.golden new file mode 100644 index 00000000000..a1674e0be4b --- /dev/null +++ b/plutus-ir/test/types/nonrecToNonrec.golden @@ -0,0 +1 @@ +(con integer) \ No newline at end of file diff --git a/plutus-ir/test/types/nonrecToRec b/plutus-ir/test/types/nonrecToRec new file mode 100644 index 00000000000..9413b41c136 --- /dev/null +++ b/plutus-ir/test/types/nonrecToRec @@ -0,0 +1,11 @@ +(let (rec) + (termbind (nonstrict) (vardecl r (con integer)) + (let (nonrec) + -- since `i` is not strictNonValue, it will be lifted to the same letgroup level, + -- thus turning `i` from nonrec to rec as r + (termbind (nonstrict) (vardecl i (con integer)) + (let (nonrec) + (termbind (strict) (vardecl j (con integer)) r) + j)) + i)) + (con 3)) diff --git a/plutus-ir/test/types/nonrecToRec.golden b/plutus-ir/test/types/nonrecToRec.golden new file mode 100644 index 00000000000..a1674e0be4b --- /dev/null +++ b/plutus-ir/test/types/nonrecToRec.golden @@ -0,0 +1 @@ +(con integer) \ No newline at end of file diff --git a/plutus-ir/test/types/oldLength b/plutus-ir/test/types/oldLength new file mode 100644 index 00000000000..21c87c3b918 --- /dev/null +++ b/plutus-ir/test/types/oldLength @@ -0,0 +1,12 @@ +(lam x (all a (type) (fun a (fun a a))) + (let + (nonrec) + (termbind (strict) (vardecl i (con integer)) + [(lam y (con integer) + (let (nonrec) (termbind (strict) (vardecl j (con integer)) y) + y + ) + ) (con 5)]) + i + ) +) diff --git a/plutus-ir/test/types/oldLength.golden b/plutus-ir/test/types/oldLength.golden new file mode 100644 index 00000000000..907770999a0 --- /dev/null +++ b/plutus-ir/test/types/oldLength.golden @@ -0,0 +1 @@ +(fun (all a_1 (type) (fun a_1 (fun a_1 a_1))) (con integer)) \ No newline at end of file diff --git a/plutus-ir/test/types/rec1 b/plutus-ir/test/types/rec1 new file mode 100644 index 00000000000..b34bb8ba938 --- /dev/null +++ b/plutus-ir/test/types/rec1 @@ -0,0 +1,17 @@ +(let + (nonrec) + (termbind (strict) (vardecl i2 (con integer)) (con 3)) + (let + (rec) + (termbind (strict) (vardecl j (con integer)) [(builtin addInteger) (con 3) k]) + (termbind (strict) (vardecl k (con integer)) [(builtin addInteger) (con 3) j]) + (let + (nonrec) + (termbind (strict) + (vardecl i1 (con integer)) + [ [ (builtin addInteger) k ] (con 3) ] + ) + [ [ (builtin addInteger) (con 5) ] [ [ (builtin addInteger) j ] i2 ] ] + ) + ) +) \ No newline at end of file diff --git a/plutus-ir/test/types/rec1.golden b/plutus-ir/test/types/rec1.golden new file mode 100644 index 00000000000..a1674e0be4b --- /dev/null +++ b/plutus-ir/test/types/rec1.golden @@ -0,0 +1 @@ +(con integer) \ No newline at end of file diff --git a/plutus-ir/test/types/rec2 b/plutus-ir/test/types/rec2 new file mode 100644 index 00000000000..c2399823f6a --- /dev/null +++ b/plutus-ir/test/types/rec2 @@ -0,0 +1,24 @@ +(lam x (con integer) + [(lam y (con integer) +(let + (nonrec) + (termbind (strict) (vardecl i2 (con integer)) (con 3)) + (let + (rec) + (termbind (strict) (vardecl j (con integer)) [(builtin addInteger) x k]) + (termbind (strict) (vardecl k (con integer)) [(builtin addInteger) y j]) + (termbind (strict) (vardecl c (con integer)) [(builtin addInteger) (con 1) i2]) + (let + (nonrec) + (termbind (strict) + (vardecl i1 (con integer)) + [ [ (builtin addInteger) k ] (con 3) ] + ) + [ [ (builtin addInteger) (con 5) ] [ [ (builtin addInteger) j ] i2 ] ] + ) + ) +) + ) + (con 1)] +) + diff --git a/plutus-ir/test/types/rec2.golden b/plutus-ir/test/types/rec2.golden new file mode 100644 index 00000000000..63842ebe8d4 --- /dev/null +++ b/plutus-ir/test/types/rec2.golden @@ -0,0 +1 @@ +(fun (con integer) (con integer)) \ No newline at end of file diff --git a/plutus-ir/test/types/rec3 b/plutus-ir/test/types/rec3 new file mode 100644 index 00000000000..15055b7d0ac --- /dev/null +++ b/plutus-ir/test/types/rec3 @@ -0,0 +1,6 @@ +(let + (rec) + (termbind (strict) (vardecl j (con integer)) [(builtin addInteger) (con 3) j]) + (termbind (strict) (vardecl k (con integer)) [(builtin addInteger) (con 3) j]) + [ (builtin addInteger) (con 5) j ] + ) \ No newline at end of file diff --git a/plutus-ir/test/types/rec3.golden b/plutus-ir/test/types/rec3.golden new file mode 100644 index 00000000000..a1674e0be4b --- /dev/null +++ b/plutus-ir/test/types/rec3.golden @@ -0,0 +1 @@ +(con integer) \ No newline at end of file diff --git a/plutus-ir/test/types/rec4 b/plutus-ir/test/types/rec4 new file mode 100644 index 00000000000..626260fea75 --- /dev/null +++ b/plutus-ir/test/types/rec4 @@ -0,0 +1,5 @@ +(let + (rec) + (termbind (strict) (vardecl j (con integer)) [(builtin addInteger) (con 3) j]) + (con 1) + ) \ No newline at end of file diff --git a/plutus-ir/test/types/rec4.golden b/plutus-ir/test/types/rec4.golden new file mode 100644 index 00000000000..a1674e0be4b --- /dev/null +++ b/plutus-ir/test/types/rec4.golden @@ -0,0 +1 @@ +(con integer) \ No newline at end of file diff --git a/plutus-ir/test/types/sameNameDifferentEnv b/plutus-ir/test/types/sameNameDifferentEnv new file mode 100644 index 00000000000..911510aa0dd --- /dev/null +++ b/plutus-ir/test/types/sameNameDifferentEnv @@ -0,0 +1,14 @@ +(let + (nonrec) + (datatypebind + (datatype + (tyvardecl Either (fun (type) (fun (type) (type)))) + (tyvardecl a (type)) + (tyvardecl b (type)) + match_Either + (vardecl Either (fun a [Either a b])) + (vardecl Left (fun b [Either a b])) + ) + ) + (con 5) +) \ No newline at end of file diff --git a/plutus-ir/test/types/sameNameDifferentEnv.golden b/plutus-ir/test/types/sameNameDifferentEnv.golden new file mode 100644 index 00000000000..a1674e0be4b --- /dev/null +++ b/plutus-ir/test/types/sameNameDifferentEnv.golden @@ -0,0 +1 @@ +(con integer) \ No newline at end of file diff --git a/plutus-ir/test/types/strictNonValue b/plutus-ir/test/types/strictNonValue new file mode 100644 index 00000000000..48f78e24af6 --- /dev/null +++ b/plutus-ir/test/types/strictNonValue @@ -0,0 +1,17 @@ +(let + (nonrec) + (termbind (nonstrict) (vardecl x (con integer)) + (let + (nonrec) + (termbind + (strict) + (vardecl y (con integer)) + (error (con integer)) + ) + y) + ) + (con 1) +) +-- this test is to make sure that `y` will not be floated outside `x`. +-- `y` may not depend on `x`, but the effects of `y-rhs` cannot be moved +-- outside: it would alter the program semantics. diff --git a/plutus-ir/test/types/strictNonValue.golden b/plutus-ir/test/types/strictNonValue.golden new file mode 100644 index 00000000000..a1674e0be4b --- /dev/null +++ b/plutus-ir/test/types/strictNonValue.golden @@ -0,0 +1 @@ +(con integer) \ No newline at end of file diff --git a/plutus-ir/test/types/strictNonValue2 b/plutus-ir/test/types/strictNonValue2 new file mode 100644 index 00000000000..99bf2c0777f --- /dev/null +++ b/plutus-ir/test/types/strictNonValue2 @@ -0,0 +1,17 @@ +(let + (nonrec) + (termbind (strict) (vardecl x (con integer)) + [ (lam z (con integer) z) + (let + (nonrec) + (termbind + (nonstrict) + (vardecl y (con integer)) + (con 1) + ) + y) + ] + ) + (con 1) +) +-- this test is to make sure that `y` can still float around but only inside/under `x`. see the similar strictNonValue diff --git a/plutus-ir/test/types/strictNonValue2.golden b/plutus-ir/test/types/strictNonValue2.golden new file mode 100644 index 00000000000..a1674e0be4b --- /dev/null +++ b/plutus-ir/test/types/strictNonValue2.golden @@ -0,0 +1 @@ +(con integer) \ No newline at end of file diff --git a/plutus-ir/test/types/strictNonValue3 b/plutus-ir/test/types/strictNonValue3 new file mode 100644 index 00000000000..9cedcc85d23 --- /dev/null +++ b/plutus-ir/test/types/strictNonValue3 @@ -0,0 +1,14 @@ +(lam x (con integer) +(let (nonrec) + (termbind (nonstrict) (vardecl i (con integer)) + (let (nonrec) + (termbind (strict) (vardecl j (con integer)) + [(lam x (con integer) x) (con 1)] + ) + [(builtin addInteger) j x]) + ) + i + )) +-- `j` is immovable, but i is movable. +-- this is to test that j will be included in the rhstable[i] + diff --git a/plutus-ir/test/types/strictNonValue3.golden b/plutus-ir/test/types/strictNonValue3.golden new file mode 100644 index 00000000000..63842ebe8d4 --- /dev/null +++ b/plutus-ir/test/types/strictNonValue3.golden @@ -0,0 +1 @@ +(fun (con integer) (con integer)) \ No newline at end of file diff --git a/plutus-ir/test/types/strictValue b/plutus-ir/test/types/strictValue new file mode 100644 index 00000000000..3ec406c477c --- /dev/null +++ b/plutus-ir/test/types/strictValue @@ -0,0 +1,12 @@ +(lam x (con integer) +(let (nonrec) + (termbind (nonstrict) (vardecl i (con integer)) + (let (nonrec) + (termbind (strict) (vardecl j (con integer)) + (con 1)) + [(builtin addInteger) j x]) + ) + i + )) +-- j should float before i, because i depends on j and j is floatable (e.g. strictValue) + diff --git a/plutus-ir/test/types/strictValue.golden b/plutus-ir/test/types/strictValue.golden new file mode 100644 index 00000000000..63842ebe8d4 --- /dev/null +++ b/plutus-ir/test/types/strictValue.golden @@ -0,0 +1 @@ +(fun (con integer) (con integer)) \ No newline at end of file diff --git a/plutus-ir/test/types/strictValueNonValue b/plutus-ir/test/types/strictValueNonValue new file mode 100644 index 00000000000..bfd924e8204 --- /dev/null +++ b/plutus-ir/test/types/strictValueNonValue @@ -0,0 +1,15 @@ +(let (rec) + (termbind (strict) (vardecl value (fun (con integer) (con integer))) + (lam x (con integer) + (let (rec) + (termbind (strict) (vardecl nonvalue (con integer)) + [value (con 3)] + ) + x + ) + ) + ) + (con 3) + ) +-- similar to strictNonValue3 `nonvalue` is immovable, but value is movable. +-- this is to test that nonvalue will be included in the rhstable[value] diff --git a/plutus-ir/test/types/strictValueNonValue.golden b/plutus-ir/test/types/strictValueNonValue.golden new file mode 100644 index 00000000000..a1674e0be4b --- /dev/null +++ b/plutus-ir/test/types/strictValueNonValue.golden @@ -0,0 +1 @@ +(con integer) \ No newline at end of file diff --git a/plutus-ir/test/types/strictValueValue b/plutus-ir/test/types/strictValueValue new file mode 100644 index 00000000000..213dbbd27f8 --- /dev/null +++ b/plutus-ir/test/types/strictValueValue @@ -0,0 +1,14 @@ +(let (rec) + (termbind (strict) (vardecl value1 (fun (con integer) (con integer))) + (lam x (con integer) + (let (rec) + (termbind (strict) (vardecl value2 (fun (con integer) (con integer))) + (lam y (con integer) [value1 y]) + ) + x + ) + ) + ) + (con 3) + ) +-- nothing is movable, floating transformation should be id diff --git a/plutus-ir/test/types/strictValueValue.golden b/plutus-ir/test/types/strictValueValue.golden new file mode 100644 index 00000000000..a1674e0be4b --- /dev/null +++ b/plutus-ir/test/types/strictValueValue.golden @@ -0,0 +1 @@ +(con integer) \ No newline at end of file