diff --git a/src/Covenant/ASG.hs b/src/Covenant/ASG.hs index b26b4f8..78e4e36 100644 --- a/src/Covenant/ASG.hs +++ b/src/Covenant/ASG.hs @@ -236,6 +236,7 @@ import Covenant.Internal.Unification ), UnifyM, checkApp, + concretifyFT, fixUp, reconcile, runUnifyM, @@ -757,6 +758,13 @@ err = refTo AnError -- * \'Use this type variable in our scope\', specified as 'Data.Wedge.Here'. -- * \'Use this concrete type\', specified as 'Data.Wedge.There'. -- +-- = IMPORTANT +-- The *only* purpose of explicit type application arguments is to instantiate a tyvar in the result which is +-- not determined by any argument. These variables are instantiated after every other argument has been concretified. +-- +-- For example, if you have a function +-- @f :: forall a b c. (a -> b) -> (b -> a) -> b -> Either a c@ +-- Then you will need to supply *ONE* explicit type application to concretify @c@. -- @since wip app :: forall (m :: Type -> Type). @@ -780,7 +788,7 @@ app fId argRefs instTys = do then throwError $ WrongNumInstantiationsInApp renamedFT numVars numInstantiations else do renamedArgs <- traverse renameArg argRefs - concretifiedFT <- concretifyFT renamedFT renamedArgs + let concretifiedFT = concretifyFT renamedFT renamedArgs instantiatedFT <- instantiate subs concretifiedFT tyDict <- asks (view #datatypeInfo) result <- either (throwError . UnificationError) pure $ checkApp tyDict instantiatedFT (Vector.toList renamedArgs) @@ -797,22 +805,6 @@ app fId argRefs instTys = do Left err' -> throwError $ FailedToRenameInstantiation err' Right res -> pure res - concretifyFT :: CompT Renamed -> Vector (Maybe (ValT Renamed)) -> m (CompT Renamed) - concretifyFT fn@(CompT _ body) argValTypes = do - argSubs <- getArgSubs body argValTypes - instantiate (Map.toList argSubs) fn - - getArgSubs :: CompTBody Renamed -> Vector (Maybe (ValT Renamed)) -> m (Map (Index "tyvar") (ValT Renamed)) - getArgSubs (ArgsAndResult args _) argValTypes = - liftUnifyM - . fmap (Vector.foldMap id) - $ Vector.zipWithM argSubHelper args argValTypes - where - argSubHelper :: ValT Renamed -> Maybe (ValT Renamed) -> UnifyM (Map (Index "tyvar") (ValT Renamed)) - argSubHelper fromFn = \case - Nothing -> pure Map.empty - Just fromArg -> unify fromFn fromArg - -- NOTE: The helper function below only concerns instantiations that result from -- explicit type applications (via the third argument to `app`). -- @@ -830,7 +822,6 @@ app fId argRefs instTys = do [] instantiate :: [(Index "tyvar", ValT Renamed)] -> CompT Renamed -> m (CompT Renamed) - instantiate [] fn = pure fn instantiate subs fn = do instantiated <- liftUnifyM . fixUp $ foldr (\(i, t) f -> substitute i t f) (ThunkT fn) subs case instantiated of diff --git a/src/Covenant/Internal/Unification.hs b/src/Covenant/Internal/Unification.hs index 5ef1258..60f969c 100644 --- a/src/Covenant/Internal/Unification.hs +++ b/src/Covenant/Internal/Unification.hs @@ -11,14 +11,16 @@ module Covenant.Internal.Unification fixUp, reconcile, lookupDatatypeInfo, + concretifyFT, ) where -import Control.Monad (foldM, unless, when) -import Data.Ord (comparing) #if __GLASGOW_HASKELL__==908 import Data.Foldable (foldl') #endif + +import Control.Applicative (Alternative ((<|>))) +import Control.Monad (foldM, unless, when) import Control.Monad.Except (MonadError, catchError, throwError) import Control.Monad.Reader (MonadReader, ReaderT (runReaderT), ask) import Covenant.Data (DatatypeInfo) @@ -34,11 +36,14 @@ import Covenant.Internal.Type TyName, ValT (Abstraction, BuiltinFlat, Datatype, ThunkT), ) +import Covenant.Type (CompT (CompN), CompTBody (ArgsAndResult)) import Data.Kind (Type) import Data.Map (Map) +import Data.Map qualified as M import Data.Map.Merge.Strict qualified as Merge import Data.Map.Strict qualified as Map import Data.Maybe (fromJust, mapMaybe) +import Data.Ord (comparing) import Data.Set (Set) import Data.Set qualified as Set import Data.Text (Text) @@ -404,3 +409,59 @@ reconcile = _ -> case new of Abstraction (Unifiable _) -> pure old _ -> throwError $ CouldNotReconcile i old new + +----- Extra stuff + +concretifyFT :: + CompT Renamed -> + Vector (Maybe (ValT Renamed)) -> + CompT Renamed +concretifyFT (CompN cnt (ArgsAndResult fromFn res)) fromArgs = unfixedResult + where + unfixedResult :: CompT Renamed + unfixedResult = CompN cnt (ArgsAndResult subbedArgs subbedRes) + + subbedArgs = substMany allSubstitutions <$> fromFn + subbedRes = substMany allSubstitutions res + + substMany :: [(Index "tyvar", ValT Renamed)] -> ValT Renamed -> ValT Renamed + substMany subs val = foldl' (\acc (tv, ty) -> substitute tv ty acc) val subs + + allUnifiables = Set.toList $ Vector.foldMap collectUnifiables fromFn + + allSubstitutions = M.toList $ getInstantiations allUnifiables (Vector.toList fromFn) (Vector.toList fromArgs) + +getInstantiations :: [Index "tyvar"] -> [ValT Renamed] -> [Maybe (ValT Renamed)] -> Map (Index "tyvar") (ValT Renamed) +getInstantiations [] _ _ = M.empty +getInstantiations _ [] _ = M.empty +getInstantiations _ _ [] = M.empty +getInstantiations vs (_ : fEs) (Nothing : aEs) = getInstantiations vs fEs aEs +getInstantiations (var : vars) fs@(fE : fEs) as@(aE' : aEs) = + -- somewhat subjective but I think doing it w/ fromJust makes the logic easier to follow here + let aE = fromJust aE' + in case instantiates (Unifiable var) aE fE of + Nothing -> getInstantiations [var] fEs aEs <> getInstantiations vars fs as + Just t -> M.insert var t $ getInstantiations vars fs as + +instantiates :: + Renamed -> + ValT Renamed -> -- the "more concrete type", usually the actual argument from 'app' + ValT Renamed -> -- the "more polymorphic type', usually from the fn definition + Maybe (ValT Renamed) +instantiates var concrete abstract = case (concrete, abstract) of + (x, Abstraction a) -> if var == a then Just x else Nothing -- N.b. we need to be sure we only run this w/ unifiables as the first arg + (ThunkT (CompN _ concreteFn), ThunkT (CompN _ abstractFn)) -> + let concreteFn' = Vector.toList $ compTBodyToVec concreteFn + abstractFn' = Vector.toList $ compTBodyToVec abstractFn + in go concreteFn' abstractFn' + (Datatype tnC argsC, Datatype tnA argsA) + | tnC == tnA -> go (Vector.toList argsC) (Vector.toList argsA) + _ -> Nothing + where + go :: [ValT Renamed] -> [ValT Renamed] -> Maybe (ValT Renamed) + go [] _ = Nothing + go _ [] = Nothing + go (c : cs) (a : as) = instantiates var c a <|> go cs as + +compTBodyToVec :: forall a. CompTBody a -> Vector (ValT a) +compTBodyToVec (ArgsAndResult args res) = Vector.snoc args res diff --git a/src/Covenant/Test.hs b/src/Covenant/Test.hs index 57d27a0..09ab1f4 100644 --- a/src/Covenant/Test.hs +++ b/src/Covenant/Test.hs @@ -1,4 +1,5 @@ {-# LANGUAGE CPP #-} +{-# LANGUAGE OverloadedLists #-} {-# LANGUAGE PolyKinds #-} {- HLINT ignore "Use camelCase" -} @@ -70,6 +71,10 @@ module Covenant.Test typeIdTest, Arg (UnsafeMkArg), Id (UnsafeMkId), + + -- ** Exports for codegen tests + concretifyMinimalBuilder, + concretifyMegaTest, ) where @@ -90,24 +95,16 @@ import Control.Monad.State.Strict ) import Control.Monad.Trans (MonadTrans (lift)) import Control.Monad.Trans.Except (ExceptT, runExceptT) -import Covenant.ASG (ASGEnv (ASGEnv), ASGNode, CovenantError (TypeError), CovenantTypeError, Id, ScopeInfo (ScopeInfo)) +import Covenant.ASG (ASGBuilder, ASGEnv (ASGEnv), ASGNode, CovenantError (TypeError), CovenantTypeError, Id, Ref (AnArg, AnId), ScopeInfo (ScopeInfo), app', arg, boundTyVar, builtin2, builtin3, ctor, ctor', dtype, force, lam, lazyLam, lit, match, thunk) +import Covenant.Constant (AConstant (ABoolean, AnInteger)) import Covenant.Data ( DatatypeInfo, mkDatatypeInfo, noPhantomTyVars, primBaseFunctorInfos, ) -import Covenant.DeBruijn (DeBruijn (Z), asInt) -import Covenant.Index - ( Count, - count0, - count1, - count2, - intCount, - intIndex, - ix0, - ix1, - ) +import Covenant.DeBruijn (DeBruijn (S, Z), asInt) +import Covenant.Index (Count, Index, count0, count1, count2, intCount, intIndex, ix0, ix1, ix2, ix3) import Covenant.Internal.KindCheck ( checkDataDecls, checkEncodingArgs, @@ -164,9 +161,11 @@ import Covenant.Internal.Type runConstructorName, ) import Covenant.Internal.Unification (checkApp) +import Covenant.Prim (ThreeArgFunc (IfThenElse), TwoArgFunc (EqualsInteger)) import Covenant.Type - ( CompT (Comp0, CompN), - CompTBody (ArgsAndResult), + ( CompT (Comp0, Comp1, Comp2, CompN), + CompTBody (ArgsAndResult, ReturnT, (:--:>)), + boolT, tyvar, ) import Covenant.Util (prettyStr) @@ -182,6 +181,7 @@ import Data.Text (Text) import Data.Text qualified as T import Data.Vector (Vector) import Data.Vector qualified as Vector +import Data.Wedge (Wedge (Here)) import GHC.Exts (fromListN) import GHC.Word (Word32) import Optics.Core @@ -994,3 +994,175 @@ conformance_Result = Ctor "OK" [tyvar Z ix1] ] (PlutusData ConstrData) + +-- These are canned tests for concretification. They do double duty as tests for +-- part of the code generator, so we put them here to avoid having to duplicate them across +-- repositories. + +intT :: ValT AbstractTy +intT = BuiltinFlat IntegerT + +mkMaybeT :: ValT AbstractTy -> ValT AbstractTy +mkMaybeT t = dtype "Maybe" [t] + +ix4 :: forall s. Index s +ix4 = fromJust $ preview intIndex 4 + +thunk0 :: forall (a :: Type). CompTBody a -> ValT a +thunk0 = ThunkT . Comp0 + +(#==) :: Ref -> Ref -> ASGBuilder Ref +x #== y = do + equals <- builtin2 EqualsInteger + AnId <$> app' equals [x, y] + +-- This is the minimal example, largely for testing that our fix to the concretification/unification glitch +-- in this repo works. +concretifyMinimalBuilder :: ASGBuilder Id +concretifyMinimalBuilder = lam topLevelTy body + where + topLevelTy :: CompT AbstractTy + topLevelTy = Comp0 $ intT :--:> boolT :--:> ReturnT intT + + body :: ASGBuilder Ref + body = do + intArg <- AnArg <$> arg Z ix0 + boolArg <- AnArg <$> arg Z ix1 + fElim <- fPolyOneElimMinimal + maybeInt <- ctor' "Maybe" "Just" [intArg] + AnId <$> app' fElim [AnId maybeInt, boolArg] + + fPolyOneElimMinimal :: ASGBuilder Id + fPolyOneElimMinimal = lam fPolyOneElimTy $ do + maybeA <- AnArg <$> arg Z ix0 + nothingHandler <- lazyLam (Comp0 $ ReturnT intT) $ do + AnId <$> lit (AnInteger 0) + justHandler <- lazyLam (Comp0 $ tyvar (S Z) ix0 :--:> ReturnT intT) $ do + AnId <$> lit (AnInteger 0) + AnId <$> match maybeA [AnId justHandler, AnId nothingHandler] + where + fPolyOneElimTy :: CompT AbstractTy + fPolyOneElimTy = + Comp2 $ -- forall a b. + mkMaybeT (tyvar Z ix0) -- Maybe a + :--:> tyvar Z ix1 -- b + :--:> ReturnT intT -- Int + +-- This is a torture test example. We'll use it here since we have it and it's relevant, but it's largely +-- designed for a test in the code generator. +concretifyMegaTest :: ASGBuilder Id +concretifyMegaTest = lam topLevelTy body + where + body :: ASGBuilder Ref + body = do + intArg <- AnArg <$> arg Z ix0 + boolArg <- AnArg <$> arg Z ix1 + idF <- AnId <$> (thunk =<< identitee) + fmono <- AnId <$> (thunk =<< fMono) + gmono <- AnId <$> (thunk =<< gMono) + mConst <- AnId <$> (thunk =<< monoConst) + fIntro <- fPolyOneIntro + fElim <- fPolyOneElim + introApplied <- app' fIntro [fmono, mConst, gmono, intArg, boolArg] + -- REVIEW @Koz: You said that a fully polymorphic identity function *should not work* as the second arg here, but it does work? + AnId <$> app' fElim [AnId introApplied, idF, boolArg, fmono] + + ifte :: ASGBuilder Id + ifte = lam (Comp1 $ boolT :--:> tyvar Z ix0 :--:> tyvar Z ix0 :--:> ReturnT (tyvar Z ix0)) $ do + cond <- AnArg <$> arg Z ix0 + t <- AnArg <$> arg Z ix1 + f <- AnArg <$> arg Z ix2 + ifThen <- builtin3 IfThenElse + AnId <$> app' ifThen [cond, t, f] + + -- NOTE: I wonder what happens if we tried to define id and monoConst in terms of each other? + -- Like if we do it so that we get infinite mutual recursion. I should probably *try* + -- to compile something like that just to see whether it explodes. + identitee :: ASGBuilder Id + identitee = lam (Comp1 $ tyvar Z ix0 :--:> ReturnT (tyvar Z ix0)) $ do + -- Not how you would typically implement `id` lol + mConst <- monoConst + x <- AnArg <$> arg Z ix0 + -- Might not need the ty app? + AnId <$> app' mConst [x, x] -- [Here tyX] + + -- forall a. a -> a -> a + monoConst :: ASGBuilder Id + monoConst = lam (Comp1 $ tyvar Z ix0 :--:> tyvar Z ix0 :--:> ReturnT (tyvar Z ix0)) $ do + AnArg <$> arg Z ix1 + + topLevelTy :: CompT AbstractTy + topLevelTy = Comp0 $ intT :--:> boolT :--:> ReturnT intT + + fPolyOneElim :: ASGBuilder Id + fPolyOneElim = lam fPolyOneElimTy $ do + zero <- AnId <$> lit (AnInteger 0) + maybeA <- AnArg <$> arg Z ix0 + nothingHandler <- lazyLam (Comp0 $ ReturnT intT) $ do + mConst <- monoConst + b <- AnArg <$> arg (S Z) ix2 + bToInt <- force . AnArg =<< arg (S Z) ix3 + x <- AnId <$> app' bToInt [b] + AnId <$> app' mConst [zero, x] + justHandler <- lazyLam (Comp0 $ tyvar (S Z) ix0 :--:> ReturnT intT) $ do + aToInt <- force . AnArg =<< arg (S Z) ix1 + a <- AnArg <$> arg Z ix0 + AnId <$> app' aToInt [a] + AnId <$> match maybeA [AnId justHandler, AnId nothingHandler] -- ,AnId justHandler] + where + fPolyOneElimTy :: CompT AbstractTy + fPolyOneElimTy = + Comp2 $ -- forall a b. + mkMaybeT (tyvar Z ix0) -- Maybe a + :--:> thunk0 (tyvar (S Z) ix0 :--:> ReturnT intT) -- (a -> Int) + :--:> tyvar Z ix1 -- b + :--:> thunk0 (tyvar (S Z) ix1 :--:> ReturnT intT) -- (b -> Int) + :--:> ReturnT intT -- Int + fPolyOneIntro :: ASGBuilder Id + fPolyOneIntro = lam fPolyOneIntroTy $ do + fba <- force . AnArg =<< arg Z ix0 + faa <- force . AnArg =<< arg Z ix1 + predA <- force . AnArg =<< arg Z ix2 + a <- AnArg <$> arg Z ix3 + b <- AnArg <$> arg Z ix4 + -- let ba = fba (monoConst b b) + mConst <- monoConst + fbaArg <- AnId <$> app' mConst [b, b] + ba <- AnId <$> app' fba [fbaArg] + -- let aaa = monoConst a (faa a ba) + aaaArg <- AnId <$> app' faa [a, ba] + aaa <- AnId <$> app' mConst [a, aaaArg] + -- if (predA aaa) then Nothing else Just aaa + tvA <- boundTyVar Z ix0 + nothing <- ctor "Maybe" "Nothing" [] [Here tvA] + justAAA <- ctor' "Maybe" "Just" [aaa] + ifThen <- ifte + cond <- app' predA [aaa] + AnId <$> app' ifThen [AnId cond, AnId nothing, AnId justAAA] + where + fPolyOneIntroTy :: CompT AbstractTy + fPolyOneIntroTy = + Comp2 $ -- forall a b. + ThunkT (Comp0 $ tyvar (S Z) ix1 :--:> ReturnT (tyvar (S Z) ix0)) -- (b -> a) + :--:> ThunkT (Comp0 $ tyvar (S Z) ix0 :--:> tyvar (S Z) ix0 :--:> ReturnT (tyvar (S Z) ix0)) -- (a -> a -> a) + :--:> ThunkT (Comp0 $ tyvar (S Z) ix0 :--:> ReturnT boolT) -- (a -> Bool) + :--:> tyvar Z ix0 -- a + :--:> tyvar Z ix1 -- b + :--:> ReturnT (mkMaybeT (tyvar Z ix0)) -- Maybe a + fMono :: ASGBuilder Id + fMono = lam (Comp0 $ boolT :--:> ReturnT intT) $ do + aBool <- AnArg <$> arg Z ix0 + one <- AnId <$> lit (AnInteger 1) + zero <- AnId <$> lit (AnInteger 0) + ifThen <- ifte + AnId <$> app' ifThen [aBool, one, zero] + + gMono :: ASGBuilder Id + gMono = lam (Comp0 $ intT :--:> ReturnT boolT) $ do + anInt <- AnArg <$> arg Z ix0 + zero <- AnId <$> lit (AnInteger 0) + cond <- anInt #== zero + ifThen <- ifte + false <- AnId <$> lit (ABoolean False) + troo <- AnId <$> lit (ABoolean True) + AnId <$> app' ifThen [cond, false, troo] diff --git a/src/Covenant/Type.hs b/src/Covenant/Type.hs index 3ed8174..d84b441 100644 --- a/src/Covenant/Type.hs +++ b/src/Covenant/Type.hs @@ -235,9 +235,10 @@ pattern Comp3 xs <- (countHelper 3 -> Just xs) -- -- @since 1.0.0 pattern CompN :: + forall (a :: Type). Count "tyvar" -> - CompTBody AbstractTy -> - CompT AbstractTy + CompTBody a -> + CompT a pattern CompN count xs <- CompT count xs where CompN count xs = CompT count xs diff --git a/test/asg/Main.hs b/test/asg/Main.hs index efe0398..8b6eac4 100644 --- a/test/asg/Main.hs +++ b/test/asg/Main.hs @@ -74,6 +74,8 @@ import Covenant.Prim import Covenant.Test ( Concrete (Concrete), DebugASGBuilder, + concretifyMegaTest, + concretifyMinimalBuilder, debugASGBuilder, tyAppTestDatatypes, typeIdTest, @@ -166,7 +168,8 @@ main = "Opaque" [unifyOpaque], testGroup "matchOpaque" [matchOpaque], - testGroup "argBugTest" [argBugUnitTest] + testGroup "argBugTest" [argBugUnitTest], + testGroup "concretify" [simpleConcretifyUnitTest, excessiveConcretifyUnitTest] ] where moreTests :: QuickCheckTests -> QuickCheckTests @@ -830,7 +833,7 @@ matchOpaque = runIntroFormTest "matchOpaque" matchOpaqueTy $ do matchOpaqueTy = ThunkT matchOpaqueCompTy argBugUnitTest :: TestTree -argBugUnitTest = testCase "argBugTest" $ withCompilationSuccessUnit asg print +argBugUnitTest = testCase "argBugTest" $ withCompilationSuccessUnit asg (\_ -> pure ()) where intT :: ValT AbstractTy intT = BuiltinFlat IntegerT @@ -841,6 +844,15 @@ argBugUnitTest = testCase "argBugTest" $ withCompilationSuccessUnit asg print one <- AnId <$> lit (AnInteger 1) AnId <$> app' gimmeZ0 [one] +-- tests for our concretification fix in `app`. +-- We only care that compilation succeeds. + +simpleConcretifyUnitTest :: TestTree +simpleConcretifyUnitTest = testCase "simpleConcretify" $ withCompilationSuccessUnit concretifyMinimalBuilder (\_ -> pure ()) + +excessiveConcretifyUnitTest :: TestTree +excessiveConcretifyUnitTest = testCase "excessiveConcretify" $ withCompilationSuccessUnit concretifyMegaTest (\_ -> pure ()) + -- Helpers runIntroFormTest :: String -> ValT AbstractTy -> DebugASGBuilder (ValT AbstractTy) -> TestTree diff --git a/test/json-conformance/Main.hs b/test/json-conformance/Main.hs index 2927ba2..bfb6ac6 100644 --- a/test/json-conformance/Main.hs +++ b/test/json-conformance/Main.hs @@ -23,9 +23,7 @@ import Covenant.ASG match, runASGBuilder, ) -import Covenant.Constant - ( AConstant (AString, AnInteger), - ) +import Covenant.Constant (AConstant (AString, AnInteger)) import Covenant.DeBruijn (DeBruijn (S, Z)) import Covenant.Index (ix0, ix1) import Covenant.JSON (deserializeAndValidate_) @@ -35,14 +33,7 @@ import Covenant.Test conformanceDatatypes2, unsafeMkDatatypeInfos, ) -import Covenant.Type - ( AbstractTy, - BuiltinFlatT (BoolT, IntegerT, StringT), - CompT (Comp0, Comp1), - CompTBody (ReturnT, (:--:>)), - ValT (BuiltinFlat), - tyvar, - ) +import Covenant.Type (AbstractTy, BuiltinFlatT (BoolT, IntegerT, StringT), CompT (Comp0, Comp1), CompTBody (ReturnT, (:--:>)), ValT (BuiltinFlat), tyvar) import Data.Either (isRight) import Data.Vector qualified as Vector import Data.Wedge (Wedge (There)) @@ -292,3 +283,6 @@ conformance_body2_builder = lam topLevelTy body maybeBoolT :: ValT AbstractTy maybeBoolT = dtype "Maybe" [boolT] + +_debugHelp :: ASGBuilder Id -> Either CovenantError ASG +_debugHelp = runASGBuilder (unsafeMkDatatypeInfos conformanceDatatypes1)