From cb58d03b282b6e2c93aa0d2ea5c3cc65a2f4fcf1 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sun, 23 Jun 2024 18:03:32 +0200 Subject: [PATCH] first --- .gitignore | 1 + CHANGELOG.md | 5 + Check.lhs | 195 ++++++++++++++ Context.lhs | 266 +++++++++++++++++++ Kit.lhs | 91 +++++++ LICENSE | 30 +++ README.txt | 11 + Test.lhs | 716 +++++++++++++++++++++++++++++++++++++++++++++++++++ Tm.lhs | 333 ++++++++++++++++++++++++ Unify.lhs | 639 +++++++++++++++++++++++++++++++++++++++++++++ patuni.cabal | 42 +++ 11 files changed, 2329 insertions(+) create mode 100644 .gitignore create mode 100644 CHANGELOG.md create mode 100644 Check.lhs create mode 100644 Context.lhs create mode 100644 Kit.lhs create mode 100644 LICENSE create mode 100644 README.txt create mode 100644 Test.lhs create mode 100644 Tm.lhs create mode 100644 Unify.lhs create mode 100644 patuni.cabal diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..48a004c --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +dist-newstyle diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 index 0000000..f63c9cc --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,5 @@ +# Revision history for patuni + +## 1.0 -- 2024-06-23 + +* Updated for GHC 9.2–9.10 diff --git a/Check.lhs b/Check.lhs new file mode 100644 index 0000000..66b9a4f --- /dev/null +++ b/Check.lhs @@ -0,0 +1,195 @@ +This module defines a typechecker and definitional equality test for a +simple Set-in-Set type theory. + +> module Check where + +> import Prelude hiding (any) + +> import Control.Monad +> import Control.Monad.Except +> import Control.Monad.Reader +> import Data.Foldable (any) + +> import Unbound.Generics.LocallyNameless +> import GHC.Generics + +> import Kit +> import Tm +> import Context + + +> data Tel where +> Stop :: Tel +> Ask :: Type -> Bind Nom Tel -> Tel +> deriving (Show, Generic, Alpha, Subst VAL) + +> askTel :: String -> Type -> Tel -> Tel +> askTel x _S _T = Ask _S (bind (s2n x) _T) + +> supply :: Fresh m => Bind Nom Tel -> VAL -> m Tel +> supply _T v = do (x, tel) <- unbind _T +> return $ subst x v tel + + +> canTy :: (Can, [VAL]) -> Can -> Contextual Tel +> canTy (Set, []) Set = return Stop +> canTy (Set, []) c | c `elem` [Pi, Sig] = return $ askTel "S" SET $ +> askTel "T" (mv "S" --> SET) Stop +> canTy (Sig, [_S, _T]) Pair = return $ askTel "s" _S $ askTel "t" (_T $$ mv "s") Stop +> canTy (c, as) v = fail $ "canTy: canonical type " ++ pp (C c as) ++ +> " does not accept " ++ pp v + + +> typecheck :: Type -> VAL -> Contextual Bool +> typecheck _T t = (check _T t >> return True) `catchError` +> (\ _ -> return False) + +> check :: Type -> VAL -> Contextual () +> check (C c as) (C v bs) = do +> tel <- canTy (c, as) v +> checkTel tel bs + +> check (PI _S _T) (L b) = do +> (x, t) <- unbind b +> inScope x (P _S) $ check (_T $$ var x) t + +> check _T (N u as) = do +> _U <- infer u +> _T' <- checkSpine _U (N u []) as +> eq <- _T <-> _T' +> unless eq $ fail $ "Inferred type " ++ pp _T' ++ +> " of " ++ pp (N u as) ++ +> " is not " ++ pp _T + +> check _T (C c as) = fail $ "check: canonical inhabitant " ++ pp (C c as) ++ +> " of non-canonical type " ++ pp _T + +> check _T (L _) = fail $ "check: lambda cannot inhabit " ++ pp _T + +> infer :: Head -> Contextual Type +> infer (Var x w) = lookupVar x w +> infer (Meta x) = lookupMeta x + + + +> checkTel :: Tel -> [VAL] -> Contextual () +> checkTel Stop [] = return () +> checkTel (Ask _S _T) (s:ss) = do check _S s +> tel' <- supply _T s +> checkTel tel' ss +> checkTel Stop (_:_) = fail "Overapplied canonical constructor" +> checkTel (Ask _ _) [] = fail "Underapplied canonical constructor" + + +> checkSpine :: Type -> VAL -> [Elim] -> Contextual Type +> checkSpine _T _ [] = return _T +> checkSpine (PI _S _T) u (A s:ts) = check _S s >> +> checkSpine (_T $$ s) (u $$ s) ts +> checkSpine (SIG _S _T) u (Hd:ts) = checkSpine _S (u %% Hd) ts +> checkSpine (SIG _S _T) u (Tl:ts) = checkSpine (_T $$ (u %% Hd)) (u %% Tl) ts +> checkSpine ty _ (s:_) = fail $ "checkSpine: type " ++ pp ty +> ++ " does not permit " ++ pp s + + + +> quote :: Type -> VAL -> Contextual VAL +> quote (PI _S _T) f = do +> x <- fresh (s2n "xq") +> lam x <$> inScope x (P _S) +> (quote (_T $$ var x) (f $$ var x)) + +> quote (SIG _S _T) v = PAIR <$> quote _S (v %% Hd) <*> +> quote (_T $$ (v %% Hd)) (v %% Tl) + +> quote (C c as) (C v bs) = do tel <- canTy (c, as) v +> bs' <- quoteTel tel bs +> return $ C v bs' + +> quote _T (N h as) = do _S <- infer h +> quoteSpine _S (N h []) as + +> quote _T t = error $ "quote: type " ++ pp _T ++ +> " does not accept " ++ pp t + + +> quoteTel :: Tel -> [VAL] -> Contextual [VAL] +> quoteTel Stop [] = return [] +> quoteTel (Ask _S _T) (s:ss) = do s' <- quote _S s +> tel <- supply _T s +> ss' <- quoteTel tel ss +> return $ s':ss' +> quoteTel _ _ = error "quoteTel: arity error" + + +> quoteSpine :: Type -> VAL -> [Elim] -> Contextual VAL +> quoteSpine _T u [] = return u +> quoteSpine (PI _S _T) u (A s:as) = do +> s' <- quote _S s +> quoteSpine (_T $$ s') (u $$ s') as +> quoteSpine (SIG _S _T) u (Hd:as) = quoteSpine _S (u %% Hd) as +> quoteSpine (SIG _S _T) u (Tl:as) = quoteSpine (_T $$ (u %% Hd)) (u %% Tl) as +> quoteSpine _T u (s:_) = error $ "quoteSpine: type " ++ pp _T ++ +> " of " ++ pp u ++ +> " does not permit " ++ pp s + + + +> equal :: Type -> VAL -> VAL -> Contextual Bool +> equal _T s t = do +> s' <- quote _T s +> t' <- quote _T t +> return $ s' == t' + +> (<->) :: Type -> Type -> Contextual Bool +> _S <-> _T = equal SET _S _T + +> isReflexive :: Equation -> Contextual Bool +> isReflexive (EQN _S s _T t) =do +> eq <- equal SET _S _T +> if eq then equal _S s t +> else return False + + + +> checkProb :: ProblemState -> Problem -> Contextual () +> checkProb st p@(Unify (EQN _S s _T t)) = do +> check SET _S +> check _S s +> check SET _T +> check _T t +> when (st == Solved) $ do +> eq <- isReflexive (EQN _S s _T t) +> unless eq $ error $ "checkProb: not unified " ++ pp p +> checkProb st (All (P _T) b) = do +> check SET _T +> (x, p) <- unbind b +> inScope x (P _T) $ checkProb st p +> checkProb st (All (Twins _S _T) b) = do +> check SET _S +> check SET _T +> (x, p) <- unbind b +> inScope x (Twins _S _T) $ checkProb st p + + + +> validate :: (ProblemState -> Bool) -> Contextual () +> validate q = local (const []) $ do +> _Del' <- getR +> unless (null _Del') $ error "validate: not at far right" +> _Del <- getL +> help _Del `catchError` (error . (++ ("\nwhen validating\n" ++ pp (_Del, _Del')))) +> putL _Del +> where +> help :: ContextL -> Contextual () +> help B0 = return () +> help (_Del :< E x _ _) | any (x `occursIn`) _Del = throwError "validate: dependency error" +> help (_Del :< E _ _T HOLE) = do putL _Del +> check SET _T +> help _Del +> help (_Del :< E _ _T (DEFN v)) = do putL _Del +> check SET _T +> check _T v +> help _Del +> help (_Del :< Prob _ p st) = do checkProb st p +> unless (q st) $ throwError "validate: bad state" +> help _Del diff --git a/Context.lhs b/Context.lhs new file mode 100644 index 0000000..8e2bcac --- /dev/null +++ b/Context.lhs @@ -0,0 +1,266 @@ +This module defines unification problems, metacontexts and operations +for working on them in the |Contextual| monad. + +> module Context where + +> import Control.Applicative +> import Control.Monad.Identity +> import Control.Monad.Except +> import Control.Monad.Reader +> import Control.Monad.State +> import Data.Bifunctor + +> import Debug.Trace + +> import Unbound.Generics.LocallyNameless +> import Unbound.Generics.LocallyNameless.Bind (Bind(..)) +> import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind) +> import GHC.Generics + +> import qualified Data.Set as Set + +> import Kit +> import Tm + + +> data Dec = HOLE | DEFN VAL +> deriving (Show, Generic, Alpha, Subst VAL) + +> instance Occurs Dec where +> occurrence _ HOLE = Nothing +> occurrence xs (DEFN t) = occurrence xs t +> frees _ HOLE = Set.empty +> frees isMeta (DEFN t) = frees isMeta t + +> data Equation = EQN Type VAL Type VAL +> deriving (Show, Generic, Alpha, Subst VAL) + +> instance Occurs Equation where +> occurrence xs (EQN _S s _T t) = occurrence xs [_S, s, _T, t] +> frees isMeta (EQN _S s _T t) = frees isMeta [_S, s, _T, t] + +> instance Pretty Equation where +> pretty (EQN _S s _T t) = +> f <$> pretty _S <*> pretty s <*> pretty _T <*> pretty t +> where f _S' s' _T' t' = parens (s' <+> colon <+> _S') <+> +> text "==" <+> parens (t' <+> colon <+> _T') + +> data Problem = Unify Equation +> | All Param (Bind Nom Problem) +> deriving (Show, Generic, Alpha) + +> instance Occurs Problem where +> occurrence xs (Unify q) = occurrence xs q +> occurrence xs (All e (B _ p)) = max (occurrence xs e) (occurrence xs p) +> frees isMeta (Unify q) = frees isMeta q +> frees isMeta (All e (B _ p)) = frees isMeta e `Set.union` frees isMeta p + +> instance Subst VAL Problem where +> substs s (Unify q) = Unify (substs s q) +> substs s (All e b) = All (substs s e) (bind x (substs s p)) +> where (x, p) = unsafeUnbind b + +> instance Pretty Problem where +> pretty (Unify q) = pretty q +> pretty (All e b) = lunbind b $ \ (x, p) -> do +> e' <- pretty e +> x' <- pretty x +> p' <- pretty p +> return $ parens (x' <+> colon <+> e') <+> text "->" <+> p' + + +> allProb :: Nom -> Type -> Problem -> Problem +> allProb x _T p = All (P _T) (bind x p) + +> allTwinsProb :: Nom -> Type -> Type -> Problem -> Problem +> allTwinsProb x _S _T p = All (Twins _S _T) (bind x p) + +> wrapProb :: [(Nom, Param)] -> Problem -> Problem +> wrapProb [] p = p +> wrapProb ((x, e) : _Gam) p = All e (bind x (wrapProb _Gam p)) + + + +> newtype ProbId = ProbId Nom +> deriving stock (Eq, Show, Generic) +> deriving newtype (Pretty) +> deriving anyclass (Alpha, Subst VAL) + + + +> data ProblemState = Blocked | Active | Pending [ProbId] | Solved | Failed Err +> deriving (Eq, Show, Generic, Alpha, Subst VAL) + +> instance Pretty ProblemState where +> pretty Blocked = return $ text "BLOCKED" +> pretty Active = return $ text "ACTIVE" +> pretty (Pending xs) = return $ text $ "PENDING " ++ show xs +> pretty Solved = return $ text "SOLVED" +> pretty (Failed e) = return $ text $ "FAILED: " ++ e + + +> data Entry = E Nom Type Dec +> | Prob ProbId Problem ProblemState +> deriving (Show, Generic, Alpha, Subst VAL) + +> instance Occurs Entry where +> occurrence xs (E _ _T d) = occurrence xs _T `max` occurrence xs d +> occurrence xs (Prob _ p _) = occurrence xs p +> frees isMeta (E _ _T d) = frees isMeta _T `Set.union` frees isMeta d +> frees isMeta (Prob _ p _) = frees isMeta p + +> instance Pretty Entry where +> pretty (E x _T HOLE) = between (text "? :") <$> pretty x <*> pretty _T +> pretty (E x _T (DEFN d)) = +> (\d' -> between (text ":=" <+> d' <+> text ":")) <$> +> prettyAt PiSize d <*> pretty x <*> prettyAt PiSize _T +> pretty (Prob x p s) = +> between (text "<=") <$> +> (between (text "?? :") <$> pretty x <*> pretty p) <*> +> pretty s + + + +> type ContextL = Bwd Entry +> type ContextR = [Either Subs Entry] +> type Context = (ContextL, ContextR) + +> type VarEntry = (Nom, Type) +> type HoleEntry = (Nom, Type) + +> data Param = P Type | Twins Type Type +> deriving (Show, Generic, Alpha, Subst VAL) + +> instance Occurs Param where +> occurrence xs (P _T) = occurrence xs _T +> occurrence xs (Twins _S _T) = max (occurrence xs _S) (occurrence xs _T) +> frees isMeta (P _T) = frees isMeta _T +> frees isMeta (Twins _S _T) = frees isMeta _S `Set.union` frees isMeta _T + +> instance Pretty Param where +> pretty (P _T) = pretty _T +> pretty (Twins _S _T) = between (text "&") <$> pretty _S <*> pretty _T + + +> type Params = [(Nom, Param)] + +> instance Pretty Context where +> pretty (cl, cr) = pair <$> prettyEntries (trail cl) +> <*> fmap vcat (mapM f cr) +> where +> pair cl' cr' = cl' $+$ text "*" $+$ cr' +> f (Left ns) = prettySubs ns +> f (Right e) = pretty e + +> prettyEntries :: (Applicative m, LFresh m, MonadReader Size m) => [Entry] -> m Doc +> prettyEntries xs = vcat <$> mapM pretty xs + +> prettySubs :: (Applicative m, LFresh m, MonadReader Size m) => Subs -> m Doc +> prettySubs ns = brackets . commaSep <$> +> forM ns (\ (x, v) -> between (text "|->") <$> pretty x <*> pretty v) + +> prettyDeps :: (Applicative m, LFresh m, MonadReader Size m) => [(Nom, Type)] -> m Doc +> prettyDeps ns = brackets . commaSep <$> +> forM ns (\ (x, _T) -> between (text ":") <$> pretty x <*> pretty _T) + +> prettyDefns :: (Applicative m, LFresh m, MonadReader Size m) => [(Nom, Type, VAL)] -> m Doc +> prettyDefns ns = brackets . commaSep <$> +> forM ns (\ (x, _T, v) -> f <$> pretty x <*> pretty _T <*> pretty v) +> where f x' _T' v' = x' <+> text ":=" <+> v' <+> text ":" <+> _T' + +> prettyParams :: (Applicative m, LFresh m, MonadReader Size m) => Params -> m Doc +> prettyParams xs = vcat <$> +> forM xs (\ (x, p) -> between colon <$> pretty x <*> pretty p) + + + +> type Err = String + +> newtype Contextual a = Contextual { unContextual :: +> ReaderT Params (StateT Context (FreshMT (ExceptT Err Identity))) a } +> deriving newtype (Functor, Applicative, Monad, +> Fresh, MonadError Err, +> MonadState Context, MonadReader Params, +> MonadPlus, Alternative) + +> instance MonadFail Contextual where fail = throwError + +> ctrace :: String -> Contextual () +> ctrace s = do +> cx <- get +> _Gam <- ask +> trace (s ++ "\n" ++ pp cx ++ "\n---\n" ++ ppWith prettyParams _Gam) +> (return ()) >>= \ () -> return () + +> runContextual :: Context -> Contextual a -> Either Err (a, Context) +> runContextual cx = runIdentity . runExceptT . runFreshMT . flip runStateT cx . flip runReaderT [] . unContextual + +> modifyL :: (ContextL -> ContextL) -> Contextual () +> modifyL f = modify $ first f + +> modifyR :: (ContextR -> ContextR) -> Contextual () +> modifyR f = modify $ second f + +> pushL :: Entry -> Contextual () +> pushL e = modifyL (:< e) + +> pushR :: Either Subs Entry -> Contextual () +> pushR (Left s) = pushSubs s +> pushR (Right e) = modifyR (Right e :) + +> pushSubs :: Subs -> Contextual () +> pushSubs [] = return () +> pushSubs n = modifyR (\ cr -> if null cr then [] else Left n : cr) + +> popL :: Contextual Entry +> popL = do +> cx <- getL +> case cx of +> (cx' :< e) -> putL cx' >> return e +> B0 -> error "popL ran out of context" + +> popR :: Contextual (Maybe (Either Subs Entry)) +> popR = do +> cx <- getR +> case cx of +> (x : cx') -> putR cx' >> return (Just x) +> [] -> return Nothing + +> getL :: MonadState Context m => m ContextL +> getL = gets fst + +> getR :: Contextual ContextR +> getR = gets snd + +> putL :: ContextL -> Contextual () +> putL x = modifyL (const x) + +> putR :: ContextR -> Contextual () +> putR x = modifyR (const x) + + +> inScope :: MonadReader Params m => Nom -> Param -> m a -> m a +> inScope x p = local (++ [(x, p)]) + +> localParams :: (Params -> Params) -> Contextual a -> Contextual a +> localParams = local + +> lookupVar :: (MonadReader Params m, MonadFail m) => Nom -> Twin -> m Type +> lookupVar x w = look =<< ask +> where +> look [] = fail $ "lookupVar: missing " ++ show x +> look ((y, e) : _) | x == y = case (e, w) of +> (P _T, Only) -> return _T +> (Twins _S _T, TwinL) -> return _S +> (Twins _S _T, TwinR) -> return _T +> _ -> fail "lookupVar: evil twin" +> look (_ : _Gam) = look _Gam + +> lookupMeta :: (MonadState Context m, MonadFail m) => Nom -> m Type +> lookupMeta x = look =<< getL +> where +> look :: MonadFail m => ContextL -> m Type +> look B0 = fail $ "lookupMeta: missing " ++ show x +> look (cx :< E y t _) | x == y = return t +> | otherwise = look cx +> look (cx :< Prob {}) = look cx diff --git a/Kit.lhs b/Kit.lhs new file mode 100644 index 0000000..30a96ee --- /dev/null +++ b/Kit.lhs @@ -0,0 +1,91 @@ +This module defines some basic general purpose kit, in particular +backwards lists and a typeclass of things that can be pretty-printed. + +> module Kit ( bool +> , Bwd(..) +> , (<><) +> , (<>>) +> , trail +> , Size(..) +> , prettyAt +> , prettyLow +> , prettyHigh +> , wrapDoc +> , runPretty +> , pp +> , ppWith +> , Pretty(..) +> , between +> , commaSep +> , module PP +> ) where + +> import Control.Monad.Reader + +> import Text.PrettyPrint.HughesPJ as PP hiding (($$), first) +> import Unbound.Generics.LocallyNameless + +> bool :: a -> a -> Bool -> a +> bool no yes b = if b then yes else no + + +> data Bwd a = B0 | Bwd a :< a +> deriving (Eq, Show, Functor, Foldable) + +> (<><) :: Bwd a -> [a] -> Bwd a +> xs <>< [] = xs +> xs <>< (y : ys) = (xs :< y) <>< ys + +> (<>>) :: Bwd a -> [a] -> [a] +> B0 <>> ys = ys +> (xs :< x) <>> ys = xs <>> (x : ys) + +> trail :: Bwd a -> [a] +> trail = (<>> []) + + +> data Size = ArgSize | AppSize | PiSize | LamSize +> deriving (Bounded, Enum, Eq, Ord, Show) + +> prettyAt :: +> (Pretty a, Applicative m, LFresh m, MonadReader Size m) => Size -> a -> m Doc +> prettyAt sz = local (const sz) . pretty + +> prettyLow, prettyHigh :: +> (Pretty a, Applicative m, LFresh m, MonadReader Size m) => a -> m Doc +> prettyLow = prettyAt minBound +> prettyHigh = prettyAt maxBound + +> wrapDoc :: MonadReader Size m => Size -> m Doc -> m Doc +> wrapDoc dSize md = do +> d <- md +> curSize <- ask +> return $ if dSize > curSize then parens d else d + +> runPretty :: ReaderT Size LFreshM a -> a +> runPretty = runLFreshM . flip runReaderT maxBound + +> pp :: Pretty a => a -> String +> pp = render . runPretty . pretty + +> ppWith :: (a -> ReaderT Size LFreshM Doc) -> a -> String +> ppWith f = render . runPretty . f + +> class Pretty a where +> pretty :: (Applicative m, LFresh m, MonadReader Size m) => a -> m Doc + +> instance Pretty (Name x) where +> pretty n = return $ text $ show n + +> instance (Pretty a, Pretty b) => Pretty (Either a b) where +> pretty (Left x) = (text "Left" <+>) <$> pretty x +> pretty (Right y) = (text "Right" <+>) <$> pretty y + +> instance Pretty () where +> pretty () = return $ text "()" + +> between :: Doc -> Doc -> Doc -> Doc +> between d x y = x <+> d <+> y + +> commaSep :: [Doc] -> Doc +> commaSep = hsep . punctuate comma diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..f99b474 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2013, Adam Gundry & Conor McBride + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Adam Gundry nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.txt b/README.txt new file mode 100644 index 0000000..3bd63f1 --- /dev/null +++ b/README.txt @@ -0,0 +1,11 @@ +This is the source code accompanying + +A tutorial implementation of dynamic pattern unification +by Adam Gundry and Conor McBride + +10th July 2012 + + +The algorithm presented in the paper is in the file Unify.lhs. Look at +the file Test.lhs to see how to invoke it (via GHCi). Note that a +recent version of GHC is required, with the unbound-generics library. diff --git a/Test.lhs b/Test.lhs new file mode 100644 index 0000000..8016fe0 --- /dev/null +++ b/Test.lhs @@ -0,0 +1,716 @@ +This module defines test cases for the unification algorithm, divided +into those which must succeed, those which should block (possibly +succeeding partially), and those which must fail. + +> module Test where + +> import Unbound.Generics.LocallyNameless + +> import Kit +> import Tm +> import Unify +> import Context +> import Check + + +The |test| function executes the constraint solving algorithm on the +given metacontext. + +> test :: [Entry] -> IO () +> test = runTest (const True) + + +Allocate a fresh name so the counter starts from 1, to avoid clashing +with s2n (which generates names with index 0): + +> initialise :: Contextual () +> initialise = (fresh (s2n "init") :: Contextual (Name VAL)) >> return () + +> runTest :: (ProblemState -> Bool) -> [Entry] -> IO () +> runTest q es = do putStrLn $ "Initial context:\n" ++ +> render (runPretty (prettyEntries es)) +> let r = runContextual (B0, map Right es) +> (initialise >> ambulando [] [] >> validate q) +> case r of +> Left err -> putStrLn $ "Error: " ++ err +> Right ((), cx) -> putStrLn $ "Final context:\n" ++ pp cx ++ "\n" + +> runTestSolved, runTestStuck, runTestFailed :: IO () +> runTestSolved = mapM_ (runTest (== Solved)) tests +> runTestStuck = mapM_ (runTest (not . isFailed)) stucks +> runTestFailed = mapM_ (runTest isFailed) fails + +> isFailed :: ProblemState -> Bool +> isFailed (Failed _) = True +> isFailed _ = False + +> lifted :: Nom -> Type -> [Entry] -> [Entry] +> lifted x _T es = lift [] es +> where +> lift :: Subs -> [Entry] -> [Entry] +> lift g (E a _A d : as) = E a (_Pi x _T (substs g _A)) d : +> lift ((a, meta a $$ var x) : g) as +> lift g (Prob a p s : as) = Prob a (allProb x _T (substs g p)) s : lift g as +> lift _ [] = [] + +> boy :: String -> Type -> [Entry] -> [Entry] +> boy = lifted . s2n + +> gal :: String -> Type -> Entry +> gal x _T = E (s2n x) _T HOLE + +> eq :: String -> Type -> VAL -> Type -> VAL -> Entry +> eq x _S s _T t = Prob (ProbId (s2n x)) (Unify (EQN _S s _T t)) Active + +> tests, stucks, fails :: [[Entry]] +> tests = [ + +> -- test 0: solve B with A +> ( gal "A" SET +> : gal "B" SET +> : eq "p" SET (mv "A") SET (mv "B") +> : []) + +> -- test 1: solve B with \ _ . A +> , ( gal "A" SET +> : gal "B" (mv "A" --> SET) +> : boy "x" (mv "A") +> ( eq "p" SET (mv "A") SET (mv "B" $$ vv "x") +> : []) +> ) + +> -- test 2: restrict B to second argument +> , ( gal "A" SET +> : boy "x" (mv "A") +> ( boy "y" (mv "A") +> ( gal "B" (mv "A" --> mv "A" --> SET) +> : eq "p" SET (mv "B" $$$ [vv "y", vv "x"]) +> SET (mv "B" $$$ [vv "x", vv "x"]) +> : []) +> ) +> ) + +> -- test 3: X unchanged +> , [ gal "X" (_PI "A" SET (vv "A" --> SET)) +> , eq "p" SET (mv "X" $$$ [SET, SET]) +> SET (mv "X" $$$ [SET, SET]) +> ] + +> -- test 4: solve A with SET +> , [ gal "A" SET +> , eq "p" SET (mv "A") SET SET +> ] + +> -- test 5: solve A with B -> B +> , [ gal "A" SET +> , gal "B" SET +> , gal "C" SET +> , eq "p" SET (mv "A") SET (mv "B" --> mv "B") +> ] + +> -- test 6: solve A with \ X . B -> X +> , ( gal "A" (SET --> SET) +> : gal "B" SET +> : boy "X" SET +> ( eq "p" SET (mv "A" $$ vv "X") SET (mv "B" --> vv "X") +> : []) +> ) + +> -- test 7: solve A with \ _ X _ . B X -> X +> , ( gal "A" (SET --> SET --> SET --> SET) +> : gal "B" (SET --> SET) +> : boy "X" SET +> ( boy "Y" SET +> (eq "p" SET (mv "A" $$$ [vv "Y", vv "X", vv "Y"]) +> SET (mv "B" $$ vv "X" --> vv "X") +> : []) +> ) +> ) + +> -- test 8: solve S with A and T with B +> , [ gal "A" SET +> , gal "S" SET +> , gal "B" (mv "A" --> SET) +> , gal "T" (mv "S" --> SET) +> , eq "p" SET (PI (mv "A") (mv "B")) +> SET (PI (mv "S") (mv "T")) +> ] + +> -- test 9: solve M with \ y . y +> , [ gal "M" (SET --> SET) +> , eq "p" (SET --> SET) (ll "y" (vv "y")) +> (SET --> SET) (ll "y" (mv "M" $$ vv "y")) +> ] + +> -- test 10: solve A with \ _ X _ . X -> X and B with \ X _ _ . X +> , ( gal "A" (SET --> SET --> SET --> SET) +> : boy "X" SET +> ( boy "Y" SET +> ( gal "B" (SET --> SET) +> : eq "q" SET (mv "A" $$$ [vv "Y", vv "X", vv "Y"]) +> SET (mv "B" $$ vv "Y" --> vv "X") +> : eq "p" SET (mv "A" $$$ [vv "Y", vv "X", vv "Y"]) +> SET (vv "X" --> vv "X") +> : []) +> ) +> ) + +> -- test 11: solve A with \ _ y . y +> , [ gal "A" (_PI "X" SET (vv "X" --> vv "X")) +> , eq "p" (_PI "X" SET (vv "X" --> vv "X")) (ll "X" (ll "y" (vv "y"))) +> (_PI "X" SET (vv "X" --> vv "X")) (ll "X" (mv "A" $$ vv "X")) +> ] + +> -- test 12: solve f with \ _ y . y after lifting type +> , ( gal "f" (_PI "Y" SET (vv "Y" --> vv "Y")) +> : boy "X" SET +> ( eq "p" (vv "X" --> vv "X") (ll "y" (vv "y")) +> (vv "X" --> vv "X") (mv "f" $$ vv "X") +> : []) +> ) + +> -- test 13: intersection with nonlinearity, restrict F to first two args +> , ( gal "F" (SET --> SET --> SET --> SET) +> : boy "X" SET +> ( boy "Y" SET +> ( eq "p" SET (mv "F" $$$ [vv "X", vv "X", vv "Y"]) +> SET (mv "F" $$$ [vv "X", vv "X", vv "X"]) +> : []) +> ) +> ) + +> -- test 14: heterogeneous equality; solve A and B with SET +> , [ gal "A" SET +> , gal "B" SET +> , eq "p" (mv "A" --> SET) (ll "a" SET) +> (mv "B" --> SET) (ll "b" (mv "B")) +> , eq "q" SET (mv "A") SET (mv "B") +> ] + +> -- test 15: sigma metavariable; solve A with ((?, Set), ?) +> , [ gal "A" (_SIG "X" (SET *: SET) (vv "X" %% Tl)) +> , eq "p" SET SET SET (mv "A" %% Hd %% Tl) +> ] + +> -- test 16: sigma variable; solve A with \ X Y . X * Y +> , ( gal "A" (SET --> SET --> SET) +> : boy "B" (_SIG "X" SET (vv "X" *: SET)) +> ( eq "p" SET (mv "A" $$ (vv "B" %% Hd) $$ (vv "B" %% Tl %% Tl)) +> SET ((vv "B" %% Hd) *: (vv "B" %% Tl %% Tl)) +> : []) +> ) + +> -- test 17: sigma variable; restrict A to \ _ X . ?A' X +> , ( gal "A" (SET --> SET --> SET) +> : boy "B" (_SIG "X" SET (vv "X" *: SET)) +> ( eq "p" SET (mv "A" $$$ [vv "B" %% Hd, vv "B" %% Tl %% Tl]) +> SET (mv "A" $$$ [vv "B" %% Tl %% Tl, vv "B" %% Tl %% Tl]) +> : []) +> ) + +> -- test 18: sigma variable; solve B with \ X z . ?A X (z -) +> , ( gal "A" (SET --> SET --> SET) +> : gal "B" (_PI "X" SET (vv "X" *: SET --> SET)) +> : boy "C" (_SIG "X" SET (vv "X" *: SET)) +> ( eq "p" SET (mv "A" $$$ [vv "C" %% Hd, vv "C" %% Tl %% Tl]) +> SET (mv "B" $$$ [vv "C" %% Hd, vv "C" %% Tl]) +> : []) +> ) + +> -- test 19: sigma metavariable and equation; solve A +> , [ gal "A" (_SIG "X" SET (vv "X")) +> , eq "p" (_SIG "X" SET (vv "X" *: SET)) +> (PAIR (mv "A" %% Hd) (PAIR (mv "A" %% Tl) (SET --> SET))) +> (_SIG "X" SET (vv "X" *: SET)) +> (PAIR (SET --> SET) (PAIR (ll "z" (vv "z")) (mv "A" %% Hd))) +> ] + +> -- test 20: solve A with X ! and a with X - +> , ( boy "X" (_SIG "Y" SET (vv "Y")) +> ( gal "A" SET +> : gal "a" (mv "A") +> : eq "p" (_SIG "Y" SET (vv "Y")) (vv "X") +> (_SIG "Y" SET (vv "Y")) (PAIR (mv "A") (mv "a")) +> : []) +> ) + +> -- test 21: solve A with f +> , ( boy "f" (SET --> SET) +> ( gal "A" (SET --> SET) +> : eq "p" (SET --> SET) (vv "f") +> (SET --> SET) (ll "x" (mv "A" $$ vv "x")) +> : []) +> ) + +> -- test 22: solve A with SET +> , ( boy "X" ((SET --> SET) *: SET) +> ( gal "A" SET +> : eq "p" SET (vv "X" %% Hd $$ SET) SET (vv "X" %% Hd $$ mv "A") +> : []) +> ) + +> -- test 23: solve SS with [S', S'] +> , ( gal "SS" (SET *: SET) +> : boy "f" (SET --> SET --> SET) +> ( eq "p" SET (vv "f" $$$ [mv "SS" %% Tl, mv "SS" %% Hd]) +> SET (vv "f" $$$ [mv "SS" %% Hd, mv "SS" %% Tl]) +> : []) +> ) + +> -- test 24: solve A with SET +> , [ gal "A" SET +> , eq "p" (mv "A" --> SET) (ll "a" (mv "A")) +> (SET --> SET) (ll "a" SET) +> ] + +> -- test 25: solve with extensionality and refl +> , [ gal "A" SET +> , eq "p" (mv "A" --> SET) (ll "x" SET) +> (SET --> SET) (ll "x" SET) +> ] + +> -- test 26: solve A with \ _ Y . Y +> , ( gal "A" (SET --> SET --> SET) +> : boy "X" SET +> ( eq "p" (mv "A" $$ vv "X" $$ vv "X" --> SET) +> (ll "Y" (mv "A" $$ vv "X" $$ vv "Y")) +> (vv "X" --> SET) +> (ll "Y" (vv "X")) +> : []) +> ) + +> -- test 27: solve A with SET +> , [ gal "A" SET +> , eq "p" SET (_PI "X" (SET --> SET) (vv "X" $$ mv "A")) +> SET (_PI "X" (SET --> SET) (vv "X" $$ SET)) +> ] + +> -- test 28: prune and solve A with \ _ . B -> B +> , ( gal "A" (SET --> SET) +> : boy "x" (_SIG "Y" SET (vv "Y")) +> ( gal "B" SET +> : eq "p" SET (mv "A" $$ (vv "x" %% Hd)) +> SET (mv "B" --> mv "B") +> : []) +> ) + +> -- test 29: prune A and solve B with A +> , ( gal "A" (SET --> SET) +> : gal "B" SET +> : eq "p" (SET --> SET) (ll "X" (mv "A" $$ (vv "X" --> vv "X"))) +> (SET --> SET) (ll "X" (mv "B")) +> : []) + +> -- test 30: prune A and solve B with A +> , ( gal "B" SET +> : gal "A" (SET --> SET) +> : eq "p" (SET --> SET) (ll "X" (mv "A" $$ (vv "X" --> vv "X"))) +> (SET --> SET) (ll "X" (mv "B")) +> : []) + +> -- test 31: solve A with SET and f with \ x . x +> , ( gal "A" SET +> : gal "f" (mv "A" --> SET) +> : eq "p" (mv "A" --> SET) (mv "f") +> (mv "A" --> mv "A") (ll "x" (vv "x")) +> : eq "q" SET (mv "A" --> SET) SET (mv "A" --> mv "A") +> : []) + +> -- test 32: prune B and solve A with B -> B +> , ( gal "A" SET +> : gal "B" (SET --> SET) +> : eq "p" (SET --> SET) (ll "Y" (mv "A")) +> (SET --> SET) (ll "X" ((mv "B" $$ mv "A") --> +> (mv "B" $$ vv "X"))) +> : []) + +> -- test 33: eta-contract pi +> , ( gal "A" ((SET --> SET) --> SET) +> : boy "f" (SET --> SET) +> ( eq "p" SET (mv "A" $$ (ll "y" (vv "f" $$ vv "y"))) +> SET (vv "f" $$ SET) +> : []) +> ) + +> -- test 34: eta-contract sigma +> , ( gal "A" (SET *: SET --> SET) +> : boy "b" (SET *: SET) +> ( eq "p" SET (mv "A" $$ (PAIR (vv "b" %% Hd) (vv "b" %% Tl))) +> SET (vv "b" %% Hd) +> : []) +> ) + +> -- test 35: eta-contract pi and sigma +> , ( gal "A" ((SET *: SET --> SET) --> SET) +> : boy "f" (SET *: SET --> SET) +> ( eq "p" SET (mv "A" $$ (ll "b" (vv "f" $$ PAIR (vv "b" %% Hd) (vv "b" %% Tl)))) +> SET (vv "f" $$ PAIR SET SET) +> : []) +> ) + +> -- test 36: A/P Flattening Sigma-types +> , ( gal "u" ((SET --> SET *: SET) --> SET) +> : boy "z1" (SET --> SET) +> ( boy "z2" (SET --> SET) +> ( eq "p" SET (mv "u" $$ (ll "x" (PAIR (vv "z1" $$ vv "x") (vv "z2" $$ vv "x")))) +> SET SET +> : []) +> ) +> ) + +> -- test 37: A/P Eliminating projections +> , ( gal "u" ((SET --> SET) --> SET) +> : boy "y" (SET --> SET *: SET) +> ( eq "p" SET (mv "u" $$ (ll "x" (vv "y" $$ vv "x" %% Hd))) +> SET (vv "y" $$ SET %% Hd) +> : []) +> ) + +> -- test 38: prune A and solve B with A +> , ( gal "B" SET +> : gal "A" (SET --> SET) +> : eq "p" (SET --> SET) (ll "X" (mv "B")) +> (SET --> SET) (ll "X" (mv "A" $$ (vv "X" --> vv "X"))) +> +> : []) + +> -- test 39: solve u with \ _ x . x +> , ( gal "u" (_PI "v" (_SIG "S" SET (vv "S" *: (vv "S" --> SET))) ((vv "v" %% Tl %% Tl $$ (vv "v" %% Tl %% Hd)) --> (vv "v" %% Tl %% Tl $$ (vv "v" %% Tl %% Hd)))) +> : boy "A" SET +> ( boy "a" (vv "A") +> ( boy "f" (vv "A" --> SET) +> ( eq "p" ((vv "f" $$ vv "a") --> (vv "f" $$ vv "a")) (mv "u" $$ PAIR (vv "A") (PAIR (vv "a") (vv "f"))) +> ((vv "f" $$ vv "a") --> (vv "f" $$ vv "a")) (ll "x" (vv "x")) +> : []) +> ) +> ) +> ) + +> -- test 40: restrict A to second argument +> , ( gal "A" (SET --> SET --> SET) +> : boy "X" SET +> ( boy "Y" SET +> ( eq "p" (SET --> SET) (mv "A" $$ vv "X") +> (SET --> SET) (ll "Z" (mv "A" $$ vv "Y" $$ vv "Z")) +> : []) +> ) +> ) + +> -- test 41: solve A with [ SET , SET ] +> , ( gal "A" (SET *: SET) +> : eq "p" (SET *: SET) (mv "A") +> (SET *: SET) (PAIR (mv "A" %% Tl) SET) +> : []) + +> -- test 42 +> , ( gal "T" (SET --> SET) +> : gal "A" (_PI "Y" SET (mv "T" $$ vv "Y" --> SET)) +> : gal "B" SET +> : boy "X" SET +> ( boy "t" (mv "T" $$ vv "X") +> ( eq "p" SET (mv "B") SET (mv "A" $$ vv "X" $$ vv "t" --> SET) +> : []) +> ) +> ) + +> -- test 43 +> , ( gal "A" (SET --> SET) +> : gal "F" (SET --> SET) +> : gal "B" SET +> : boy "X" SET +> ( eq "p" SET (mv "B") +> SET (mv "A" $$ (mv "F" $$ vv "X") --> mv "A" $$ vv "X") +> : []) +> ) + +> -- test 44: false occurrence +> , ( gal "A" SET +> : gal "B" SET +> : gal "C" SET +> : eq "p" (mv "C" --> SET) (lamK (mv "B")) +> (mv "C" --> SET) (lamK (mv "A")) +> : []) + +> -- test 45 +> , ( gal "A" SET +> : gal "B" (mv "A" --> SET) +> : gal "C" (mv "A" --> SET) +> : boy "x" (mv "A") +> ( boy "y" (mv "A") +> ( eq "p" SET (mv "B" $$ vv "x") +> SET (mv "C" $$ vv "x") +> : []) +> ) +> ) + +> -- test 46: prune p to learn B doesn't depend on its argument +> , ( gal "A" (SET --> SET) +> : boy "Z" SET +> ( gal "B" (SET --> SET) +> : gal "C" SET +> : boy "X" SET +> ( boy "Y" SET +> ( eq "p" SET (mv "A" $$ (mv "B" $$ mv "C")) +> SET (mv "B" $$ vv "Y") +> : eq "q" SET (mv "B" $$ mv "C") SET (vv "Z") +> : []) +> ) +> ) +> ) + +> -- test 47 +> , ( gal "A" (_PI "X" SET (vv "X" --> SET)) +> : gal "B" SET +> : boy "Y" SET +> ( boy "y" (vv "Y") +> ( eq "p" SET (mv "B") +> SET (mv "A" $$ vv "Y" $$ vv "y") +> : []) +> ) +> ) + +> -- test 48 +> , ( gal "A" (SET --> SET) +> : gal "B" SET +> : eq "p" SET (mv "B") +> SET (_PI "X" SET (mv "A" $$ vv "X")) +> +> : []) + +> -- test 49: don't prune A too much +> , ( gal "F" (SET --> SET --> SET) +> : gal "A" (_PI "X" SET (mv "F" $$ SET $$ vv "X" --> SET)) +> : gal "B" (SET --> SET) +> : boy "Y" SET +> ( eq "p" (SET --> SET) (mv "B") +> (mv "F" $$ SET $$ vv "Y" --> SET) (mv "A" $$ vv "Y") +> : boy "y" (mv "F" $$ SET $$ vv "Y") +> ( eq "q" SET (mv "F" $$ vv "Y" $$ vv "Y") SET SET +> : eq "r" SET (mv "A" $$ vv "Y" $$ vv "y") +> (mv "F" $$ SET $$ vv "Y") (vv "y") +> : []) +> ) +> ) + +> -- test 50: Miller's nasty non-pruning example +> , ( boy "a" SET +> ( gal "X" ((SET --> SET) --> SET --> SET) +> : boy "y" SET +> ( eq "p" SET (mv "X" $$ (ll "z" (vv "a")) $$ vv "y") +> SET (vv "a") +> : eq "q" ((SET --> SET) --> SET --> SET) (mv "X") +> ((SET --> SET) --> SET --> SET) (ll "z1" (ll "z2" (vv "z1" $$ vv "z2"))) +> : []) +> ) +> ) + +> -- test 51 +> , ( gal "A" (_PI "X" SET (_PI "x" (vv "X") SET)) +> : gal "B" SET +> : eq "p" SET (mv "B") +> SET (_PI "X" SET (_PI "x" (vv "X") (mv "A" $$ vv "X" $$ vv "x"))) +> : []) + +> ] + + +> stucks = [ + +> -- stuck 0: nonlinear +> ( gal "A" (SET --> SET --> SET --> SET) +> : gal "B" (SET --> SET) +> : boy "X" SET +> ( boy "Y" SET +> ( eq "p" SET (mv "A" $$$ [vv "Y", vv "X", vv "Y"]) +> SET (mv "B" $$ vv "Y" --> vv "X") +> : []) +> ) +> ) + +> -- stuck 1: nonlinear +> , ( gal "F" (SET --> SET --> SET) +> : gal "G" (SET --> SET --> SET) +> : boy "X" SET +> ( eq "p" SET (mv "F" $$$ [vv "X", vv "X"]) +> SET (mv "G" $$$ [vv "X", vv "X"]) +> : []) +> ) + +> -- stuck 2: nonlinear +> , ( boy "X" SET +> ( gal "f" (vv "X" --> vv "X" --> vv "X") +> : boy "Y" SET +> ( boy "x" (vv "X") +> ( eq "p" (vv "Y" --> vv "X") (ll "y" (mv "f" $$ vv "x" $$ vv "x")) +> (vv "Y" --> vv "X") (ll "y" (vv "x")) +> : []) +> ) +> ) +> ) + +> -- stuck 3: nonlinear +> , ( gal "B" (SET --> SET --> SET) +> : boy "X" SET +> ( gal "A" SET +> : eq "p" (mv "A" --> SET) (ll "a" (mv "B" $$ vv "X" $$ vv "X")) +> (mv "A" --> SET) (ll "a" (vv "X")) +> : []) +> ) + +> -- stuck 4: double meta +> , [ gal "A" (SET --> SET) +> , gal "B" (SET --> SET) +> , gal "D" SET +> , gal "C" SET +> , eq "p" SET (mv "A" $$ (mv "B" $$ mv "C")) SET (mv "D") +> ] + +> -- stuck 5: solution does not typecheck +> , ( gal "A" SET +> : gal "f" (mv "A" --> SET) +> : eq "p" (mv "A" --> SET) (mv "f") +> (mv "A" --> mv "A") (ll "x" (vv "x")) +> : []) + +> -- stuck 6: weak rigid occurrence should not cause failure +> , ( gal "A" ((SET --> SET) --> SET) +> : boy "f" (SET --> SET) +> ( eq "p" SET (mv "A" $$ vv "f") +> SET (vv "f" $$ (mv "A" $$ (ll "X" (vv "X"))) --> SET) +> : []) +> ) + +> -- stuck 7: prune second argument of B and get stuck +> , ( gal "A" SET +> : gal "B" (SET --> SET --> SET) +> : boy "X" SET +> ( eq "p" SET (mv "A") +> SET (mv "B" $$ mv "A" $$ vv "X") +> : []) +> ) + +> -- stuck 8: prune argument of A +> , ( boy "f" (SET --> SET) +> ( gal "A" (SET --> SET) +> : boy "X" SET +> ( boy "Y" SET +> ( eq "p" SET (mv "A" $$ vv "X") +> SET (vv "f" $$ (mv "A" $$ vv "Y")) +> : []) +> ) +> ) +> ) + +> -- stuck 9 (requires sigma-splitting of twins) +> , ( gal "A" SET +> : gal "B" (SET --> mv "A" --> SET) +> : gal "S" SET +> : gal "T" (SET --> mv "S" --> SET) +> : eq "p" (SIG (mv "A") (mv "B" $$ SET) --> SET) +> (ll "x" (mv "B" $$ SET $$ (vv "x" %% Hd))) +> (SIG (mv "S") (mv "T" $$ SET) --> SET) +> (ll "x" (mv "T" $$ SET $$ (vv "x" %% Hd))) +> : []) + +> -- stuck 10: awkward occurrence (TODO: should this get stuck or fail?) +> , ( gal "A" SET +> : gal "a" (mv "A") +> : gal "f" (mv "A" --> SET) +> : eq "p" SET (mv "A") SET ((mv "f" $$ mv "a") --> SET) +> : []) + +> -- stuck 12: twins with matching spines (stuck on B Set == T Set) +> , ( gal "A" SET +> : gal "B" (SET --> mv "A" --> SET) +> : gal "S" SET +> : gal "T" (SET --> mv "S" --> SET) +> : eq "p" (SIG (mv "A") (mv "B" $$ SET) --> mv "A") +> (ll "x" (vv "x" %% Hd)) +> (SIG (mv "S") (mv "T" $$ SET) --> mv "S") +> (ll "x" (vv "x" %% Hd)) +> : []) + +> -- stuck 13 +> , ( gal "A" (SET --> SET) +> : gal "B" (SET --> SET) +> : gal "a" (mv "A" $$ SET) +> : gal "b" (mv "B" $$ SET) +> : eq "p" (SIG SET (mv "B")) (PAIR SET (mv "b")) +> (mv "A" $$ SET) (mv "a") +> : eq "q" SET (SIG SET (mv "B")) SET (mv "A" $$ SET) +> : []) + +> -- stuck 14 (TODO: should this be solvable by pruning?) +> , ( gal "A" (SET --> SET) +> : gal "B" SET +> : boy "X" SET +> ( eq "p" SET (mv "A" $$ (mv "A" $$ vv "X")) +> SET (mv "B") +> : []) +> ) + +> -- stuck 15 +> , ( gal "F" (SET --> SET) +> : gal "A" (_PI "X" SET (mv "F" $$ vv "X")) +> : boy "X" SET +> ( boy "Y" SET +> ( eq "p" (mv "F" $$ vv "X") (mv "A" $$ vv "X") +> (mv "F" $$ vv "Y") (mv "A" $$ vv "Y") +> : []) +> ) +> ) + +> -- stuck 16 +> , ( gal "B" (SET --> SET) +> : gal "F" (mv "B" $$ SET --> SET) +> : eq "p" (mv "B" $$ SET --> SET) (ll "Y" (mv "F" $$ vv "Y")) +> (SET --> SET) (ll "Y" (vv "Y")) +> : []) + +> -- test 53: solve C with A despite B being in the way +> , ( gal "A" SET +> : gal "C" SET +> : gal "B" (SET --> SET) +> : gal "F" (mv "B" $$ SET --> SET) +> : eq "p" (_PI "X" (mv "B" $$ SET) ((mv "F" $$ vv "X") --> SET)) +> (ll "X" (ll "x" (mv "A"))) +> (_PI "X" SET (vv "X" --> SET)) +> (ll "X" (ll "x" (mv "C"))) +> : []) + +> ] + +> fails = [ + +> -- fail 0: occur check failure (A occurs in A -> A) +> [ gal "A" SET +> , eq "p" SET (mv "A") SET (mv "A" --> mv "A") +> ] + +> -- fail 1: flex-rigid fails because A cannot depend on X +> , ( gal "A" SET +> : gal "B" SET +> : boy "X" SET +> ( eq "p" SET (mv "A") SET (mv "B" --> vv "X") +> : []) +> ) + +> -- fail 2: rigid-rigid clash +> , ( boy "X" SET +> ( boy "Y" SET +> ( eq "p" SET (vv "X") SET (vv "Y") +> : []) +> ) +> ) + +> -- fail 3: spine mismatch +> , ( boy "X" (SET *: SET) +> ( eq "p" SET (vv "X" %% Hd) SET (vv "X" %% Tl) +> : []) +> ) + +> -- fail 4: rigid-rigid constant clash +> , ( eq "p" SET SET SET (SET --> SET) +> : []) + +> ] diff --git a/Tm.lhs b/Tm.lhs new file mode 100644 index 0000000..1346ec6 --- /dev/null +++ b/Tm.lhs @@ -0,0 +1,333 @@ +This module defines terms and machinery for working with them +(including evaluation and occurrence checking). + +> module Tm where + +> import Prelude hiding ((<>)) +> import Data.List (unionBy) +> import Data.Function (on) + +> import Unbound.Generics.LocallyNameless +> import Unbound.Generics.LocallyNameless.Bind (Bind(..)) +> import Unbound.Generics.LocallyNameless.Unsafe (unsafeUnbind) + +> import Data.Set (Set) +> import qualified Data.Set as Set + +> import GHC.Generics + +> import Kit + +> type Nom = Name VAL + +> freshNom :: Fresh m => m Nom +> freshNom = fresh (s2n "x") + + +> data VAL where +> L :: Bind Nom VAL -> VAL +> N :: Head -> [Elim] -> VAL +> C :: Can -> [VAL] -> VAL +> deriving (Show, Generic, Alpha) + +> type Type = VAL + +> data Can = Set | Pi | Sig | Pair +> deriving (Eq, Show, Generic, Alpha, Subst VAL) + +> data Twin = Only | TwinL | TwinR +> deriving (Eq, Show, Generic, Alpha, Subst VAL) + +> data Head = Var Nom Twin | Meta Nom +> deriving (Eq, Show, Generic, Alpha, Subst VAL) + +> data Elim = A VAL | Hd | Tl +> deriving (Eq, Show, Generic, Alpha, Subst VAL) + + +> pattern SET :: VAL +> pattern SET = C Set [] + +> pattern PI :: VAL -> VAL -> VAL +> pattern PI _S _T = C Pi [_S, _T] + +> pattern SIG :: VAL -> VAL -> VAL +> pattern SIG _S _T = C Sig [_S, _T] + +> pattern PAIR :: VAL -> VAL -> VAL +> pattern PAIR s t = C Pair [s, t] + + + +> instance Eq VAL where +> (==) = aeq + +> instance Subst VAL VAL where +> substs = eval +> subst n u = substs [(n, u)] + +> instance Pretty VAL where +> pretty (PI _S (L b)) = +> lunbind b $ \ (x, _T) -> +> wrapDoc PiSize $ +> if x `occursIn` _T +> then (\ x' _S' _T' -> text "Pi" <+> parens (x' <+> colon <+> _S') <+> _T') +> <$> prettyHigh x <*> prettyHigh _S <*> prettyAt ArgSize _T +> else between (text "->") <$> prettyAt AppSize _S <*> prettyAt PiSize _T +> +> pretty (SIG _S (L b)) = +> lunbind b $ \ (x, _T) -> +> wrapDoc PiSize $ +> if x `occursIn` _T +> then (\ x' _S' _T' -> text "Sig" <+> parens (x' <+> colon <+> _S') <+> _T') +> <$> prettyHigh x <*> prettyHigh _S <*> prettyAt ArgSize _T +> else between (text "*") <$> prettyAt AppSize _S <*> prettyAt PiSize _T +> +> pretty (L b) = wrapDoc LamSize $ (text "\\" <+>) <$> prettyLam b +> where +> prettyLam u = lunbind u $ \ (x, t) -> do +> v <- if x `occursIn` t then prettyLow x else return (text "_") +> case t of +> L b' -> (v <+>) <$> prettyLam b' +> _ -> (\ t' -> v <+> text "." <+> t') <$> prettyAt LamSize t +> pretty (N h []) = pretty h +> pretty (N h as) = wrapDoc AppSize $ +> (\ h' as' -> h' <+> hsep as') +> <$> pretty h <*> mapM (prettyAt ArgSize) as +> pretty (C c []) = pretty c +> pretty (C c as) = wrapDoc AppSize $ +> (\ c' as' -> c' <+> hsep as') +> <$> pretty c <*> mapM (prettyAt ArgSize) as + +> instance Pretty Can where +> pretty c = return $ text $ show c + +> instance Pretty Twin where +> pretty Only = pure empty +> pretty TwinL = pure $ text "^<" +> pretty TwinR = pure $ text "^>" + +> instance Pretty Head where +> pretty (Var x w) = (<>) <$> pretty x <*> pretty w +> pretty (Meta x) = (text "?" <>) <$> pretty x + +> instance Pretty Elim where +> pretty (A a) = pretty a +> pretty Hd = return $ text "!" +> pretty Tl = return $ text "-" + + +> var :: Nom -> VAL +> var x = N (Var x Only) [] + +> twin :: Nom -> Twin -> VAL +> twin x w = N (Var x w) [] + +> meta :: Nom -> VAL +> meta x = N (Meta x) [] + + +> lam :: Nom -> VAL -> VAL +> lam x t = L (bind x t) + +> lams :: [Nom] -> VAL -> VAL +> lams xs t = foldr lam t xs + +> lams' :: [(Nom, Type)] -> VAL -> VAL +> lams' xs = lams $ map fst xs + +> lamK :: VAL -> VAL +> lamK t = L (bind (s2n "_x") t) + +> _Pi :: Nom -> Type -> Type -> Type +> _Pi x _S _T = PI _S (lam x _T) + +> _Pis :: [(Nom, Type)] -> Type -> Type +> _Pis xs _T = foldr (uncurry _Pi) _T xs + +> (-->) :: Type -> Type -> Type +> _S --> _T = _Pi (s2n "xp") _S _T +> infixr 5 --> + +> _Sig :: Nom -> Type -> Type -> Type +> _Sig x _S _T = SIG _S (lam x _T) + +> (*:) :: Type -> Type -> Type +> _S *: _T = _Sig (s2n "xx") _S _T + +> vv :: String -> VAL +> vv x = var (s2n x) + +> mv :: String -> VAL +> mv x = meta (s2n x) + +> ll :: String -> VAL -> VAL +> ll x = lam (s2n x) + +> _PI :: String -> VAL -> VAL -> VAL +> _PI x = _Pi (s2n x) + +> _SIG :: String -> VAL -> VAL -> VAL +> _SIG x = _Sig (s2n x) + + + +> mapElim :: (VAL -> VAL) -> Elim -> Elim +> mapElim f (A a) = A (f a) +> mapElim _ Hd = Hd +> mapElim _ Tl = Tl + +> headVar :: Head -> Nom +> headVar (Var x _) = x +> headVar (Meta x) = x + +> isVar :: VAL -> Bool +> isVar v = case etaContract v of +> N (Var _ _) [] -> True +> _ -> False + +> toVars :: [Elim] -> Maybe [Nom] +> toVars = traverse (toVar . mapElim etaContract) +> where +> toVar :: Elim -> Maybe Nom +> toVar (A (N (Var x _) [])) = Just x +> toVar _ = Nothing + +> linearOn :: VAL -> [Nom] -> Bool +> linearOn _ [] = True +> linearOn t (a:as) = not (a `occursIn` t && a `elem` as) && linearOn t as + +> initLast :: [x] -> Maybe ([x], x) +> initLast [] = Nothing +> initLast xs = Just (init xs, last xs) + +> etaContract :: VAL -> VAL +> etaContract (L b) = case etaContract t of +> N x as | Just (bs, A (N (Var y' _) [])) <- initLast as, y == y', +> not (y `occursIn` bs) -> N x bs +> t' -> lam y t' +> where +> (y, t) = unsafeUnbind b +> etaContract (N x as) = N x (map (mapElim etaContract) as) +> etaContract (PAIR s t) = case (etaContract s, etaContract t) of +> (N x as, N y bs) | Just (as', Hd) <- initLast as, +> Just (bs', Tl) <- initLast bs, +> x == y, +> as' == bs' -> N x as' +> (s', t') -> PAIR s' t' +> etaContract (C c as) = C c (map etaContract as) + +> occursIn :: Occurs t => Nom -> t -> Bool +> x `occursIn` t = x `Set.member` fvs t + + +> data Strength = Weak | Strong +> deriving (Eq, Ord, Show) + +> data Occurrence = Flexible | Rigid Strength +> deriving (Eq, Ord, Show) + +> isStrongRigid :: Maybe Occurrence -> Bool +> isStrongRigid (Just (Rigid Strong)) = True +> isStrongRigid _ = False + +> isRigid :: Maybe Occurrence -> Bool +> isRigid (Just (Rigid _)) = True +> isRigid _ = False + +> isFlexible :: Maybe Occurrence -> Bool +> isFlexible (Just Flexible) = True +> isFlexible _ = False + +> fvs :: Occurs t => t -> Set Nom +> fvs = frees False + +> fmvs :: Occurs t => t -> Set Nom +> fmvs = frees True + +> class Occurs t where +> occurrence :: [Nom] -> t -> Maybe Occurrence +> frees :: Bool -> t -> Set Nom + +> instance Occurs Nom where +> occurrence _ _ = Nothing +> frees _ _ = Set.empty + +> instance Occurs VAL where +> occurrence xs (L (B _ b)) = occurrence xs b +> occurrence xs (C _ as) = occurrence xs as +> occurrence xs (N (Var y _) as) +> | y `elem` xs = Just (Rigid Strong) +> | otherwise = weaken <$> occurrence xs as +> where weaken (Rigid _) = Rigid Weak +> weaken Flexible = Flexible +> occurrence xs (N (Meta y) as) +> | y `elem` xs = Just (Rigid Strong) +> | otherwise = Flexible <$ occurrence xs as + +> frees isMeta (L (B _ t)) = frees isMeta t +> frees isMeta (C _ as) = Set.unions (map (frees isMeta) as) +> frees isMeta (N h es) = Set.unions (map (frees isMeta) es) +> `Set.union` x +> where x = case h of +> Var v _ | not isMeta && isFreeName v -> Set.singleton v +> Meta v | isMeta && isFreeName v -> Set.singleton v +> _ -> Set.empty + +> instance Occurs Elim where +> occurrence xs (A a) = occurrence xs a +> occurrence _ _ = Nothing +> frees isMeta (A a) = frees isMeta a +> frees _ _ = Set.empty + +> instance (Occurs a, Occurs b) => Occurs (a, b) where +> occurrence xs (s, t) = max (occurrence xs s) (occurrence xs t) +> frees isMeta (s, t) = frees isMeta s `Set.union` frees isMeta t + +> instance (Occurs a, Occurs b, Occurs c) => Occurs (a, b, c) where +> occurrence xs (s, t, u) = maximum [occurrence xs s, occurrence xs t, occurrence xs u] +> frees isMeta (s, t, u) = Set.unions [frees isMeta s, frees isMeta t, frees isMeta u] + +> instance Occurs a => Occurs [a] where +> occurrence _ [] = Nothing +> occurrence xs ys = maximum $ map (occurrence xs) ys +> frees isMeta = Set.unions . map (frees isMeta) + + +> type Subs = [(Nom, VAL)] + +> compSubs :: Subs -> Subs -> Subs +> compSubs new old = unionBy ((==) `on` fst) new (substs new old) + +> eval :: Subs -> VAL -> VAL +> eval g (L b) = L (bind x (eval g t)) +> where (x, t) = unsafeUnbind b +> eval g (N u as) = evalHead g u %%% map (mapElim (eval g)) as +> eval g (C c as) = C c (map (eval g) as) + +> evalHead :: Subs -> Head -> VAL +> evalHead g hv = case lookup (headVar hv) g of +> Just u -> u +> Nothing -> N hv [] + +> elim :: VAL -> Elim -> VAL +> elim (L b) (A a) = eval [(x, a)] t where (x, t) = unsafeUnbind b +> elim (N u as) e = N u $ as ++ [e] +> elim (PAIR x _) Hd = x +> elim (PAIR _ y) Tl = y +> elim t a = error $ "bad elimination of " ++ pp t ++ " by " ++ pp a + +> ($$) :: VAL -> VAL -> VAL +> f $$ a = elim f (A a) + +> ($$$) :: VAL -> [VAL] -> VAL +> ($$$) = foldl ($$) + +> ($*$) :: VAL -> [(Nom, a)] -> VAL +> f $*$ _Gam = f $$$ map (var . fst) _Gam + +> (%%) :: VAL -> Elim -> VAL +> (%%) = elim + +> (%%%) :: VAL -> [Elim] -> VAL +> (%%%) = foldl (%%) diff --git a/Unify.lhs b/Unify.lhs new file mode 100644 index 0000000..6312132 --- /dev/null +++ b/Unify.lhs @@ -0,0 +1,639 @@ +%if False + +> module Unify where + +> import Control.Monad.Except (catchError, throwError, when) +> import Control.Monad.Reader (ask) + +> import Data.List ((\\)) +> import Data.Maybe (isNothing) +> import Data.Set (Set) +> import qualified Data.Set as Set + +> import Unbound.Generics.LocallyNameless (aeq, unbind, subst, substs, Fresh) + +> import Kit (pp) +> import Tm (VAL(..), Elim(..), Head(..), Twin(..), +> pattern SET, pattern PI, pattern SIG, pattern PAIR, +> Nom, Type, Subs, +> ($$), (%%), ($*$), +> var, lam, lams, lams', _Pi, _Pis, (-->), +> freshNom, compSubs, occurrence, toVars, linearOn, +> isStrongRigid, isRigid, isFlexible, fvs, fmvs, isVar) +> import Check (checkProb, check, typecheck, equal, isReflexive) +> import Context (Entry(..), ProblemState(..), Problem(..), Equation(..), +> Dec(..), Param(..), Contextual, ProbId(..), +> allProb, allTwinsProb, wrapProb, +> pushL, popL, pushR, popR, +> lookupVar, localParams, lookupMeta) + +> notSubsetOf :: Ord a => Set a -> Set a -> Bool +> a `notSubsetOf` b = not (a `Set.isSubsetOf` b) + +> vars :: Ord a => [(a, b)] -> Set a +> vars = Set.fromList . map fst + +> active :: ProbId -> Equation -> Contextual () +> block :: ProbId -> Equation -> Contextual () +> failed :: ProbId -> Equation -> String -> Contextual () +> solved :: ProbId -> Equation -> Contextual () +> simplify :: ProbId -> Problem -> [Problem] -> Contextual () + +> active n q = putProb n (Unify q) Active +> block n q = putProb n (Unify q) Blocked +> failed n q e = putProb n (Unify q) (Failed e) +> solved n q = pendingSolve n (Unify q) [] + +> putProb :: ProbId -> Problem -> ProblemState -> +> Contextual () +> putProb x q s = do +> _Gam <- ask +> pushR . Right $ Prob x (wrapProb _Gam q) s + +> pendingSolve :: ProbId -> Problem -> [ProbId] -> +> Contextual () +> pendingSolve n q [] = do checkProb Solved q `catchError` +> (error . (++ "when checking problem " ++ +> pp n ++ " : " ++ pp q)) +> putProb n q Solved +> pendingSolve n q ds = putProb n q (Pending ds) + +> simplify n q rs = help rs [] +> where +> help :: [Problem] -> [ProbId] -> Contextual () +> help [] xs = pendingSolve n q xs +> help (p:ps) xs = subgoal p (\ x -> help ps (x:xs)) +> +> subgoal :: Problem -> (ProbId -> Contextual a) -> +> Contextual a +> subgoal p f = do +> x <- ProbId <$> freshNom +> _Gam <- ask +> pushL $ Prob x (wrapProb _Gam p) Active +> a <- f x +> goLeft +> return a + +> goLeft :: Contextual () +> goLeft = popL >>= pushR . Right + +> hole :: [(Nom, Type)] -> Type -> +> (VAL -> Contextual a) -> Contextual a +> define :: [(Nom, Type)] -> Nom -> Type -> VAL -> +> Contextual () + +> hole _Gam _T f = do check SET (_Pis _Gam _T) `catchError` +> (error . (++ "\nwhen creating hole of type " ++ +> pp (_Pis _Gam _T))) +> x <- freshNom +> pushL $ E x (_Pis _Gam _T) HOLE +> a <- f (N (Meta x) [] $*$ _Gam) +> goLeft +> return a + +> defineGlobal :: Nom -> Type -> VAL -> Contextual a -> +> Contextual a +> defineGlobal x _T v m = do check _T v `catchError` +> (error . (++ "\nwhen defining " ++ +> pp x ++ " : " ++ pp _T ++ +> " to be " ++ pp v)) +> pushL $ E x _T (DEFN v) +> pushR (Left [(x, v)]) +> a <- m +> goLeft +> return a + +> define _Gam x _T v = +> defineGlobal x (_Pis _Gam _T) (lams' _Gam v) (return ()) + +%endif + + +\subsection{Unification} +\label{subsec:impl:unification} + +As we have seen, unification splits into four main cases: +$\eta$-expanding elements of $\Pi$ or $\Sigma$ types, rigid-rigid +equations between non-metavariable terms (Figure~\ref{fig:decompose}), +flex-rigid equations between a metavariable and a rigid term +(Figure~\ref{fig:flex-rigid}), and flex-flex equations between two +metavariables (Figure~\ref{fig:flex-flex}). When the equation is +between two functions, we use twins (see +subsection~\ref{subsec:twins}) to decompose it heterogeneously. If it +is in fact homogeneous, the twins will be simplified away later. + +We will take slight liberties, here and elsewhere, with the Haskell +syntax. In particular, we will use italicised capital letters (e.g.\ +|_A|) for Haskell variables representing types in the object language, +while sans-serif letters (e.g.\ |A|) will continue to stand for data +constructors. + +> unify :: ProbId -> Equation -> Contextual () +> +> unify n q@(EQN (PI _A _B) f (PI _S _T) g) = do +> x <- freshNom +> let (xL, xR) = (N (Var x TwinL) [], N (Var x TwinR) []) +> simplify n (Unify q) [ Unify (EQN SET _A SET _S), +> allTwinsProb x _A _S (Unify (EQN (_B $$ xL) (f $$ xL) (_T $$ xR) (g $$ xR)))] +> unify n q@(EQN (SIG _A _B) t (SIG _C _D) w) = +> simplify n (Unify q) [ Unify (EQN _A a _C c) +> , Unify (EQN (_B $$ a) b (_D $$ c) d)] +> where (a, b) = (t %% Hd, t %% Tl) +> (c, d) = (w %% Hd, w %% Tl) +> +> unify n q@(EQN _ (N (Meta _) _) _ (N (Meta _) _)) = +> tryPrune n q $ tryPrune n (sym q) $ flexFlex n q +> +> unify n q@(EQN _ (N (Meta _) _) _ _) = +> tryPrune n q $ flexRigid [] n q +> +> unify n q@(EQN _ _ _ (N (Meta _) _)) = +> tryPrune n (sym q) $ flexRigid [] n (sym q) +> +> unify n q = rigidRigid q >>= +> simplify n (Unify q) . map Unify + +Here |sym| swaps the two sides of an equation: + +> sym :: Equation -> Equation +> sym (EQN _S s _T t) = EQN _T t _S s + + +\subsection{Rigid-rigid decomposition} +\label{subsec:impl:rigid-rigid} + +A rigid-rigid equation (between two non-metavariable terms) can either +be decomposed into simpler equations or it is impossible to solve. For +example, $[[Pi A B == Pi S T]]$ splits into $[[A == S]], [[B == T]]$, +but $[[Pi A B == Sigma S T]]$ cannot be solved. + +%% The |rigidRigid| +%% function implements the steps shown in Figure~\ref{fig:decompose}. +%% excluding the $\eta$-expansion steps, which are handled by |unify| +%% above. + +> rigidRigid :: Equation -> Contextual [Equation] +> rigidRigid (EQN SET SET SET SET) = return [] +> +> rigidRigid (EQN SET (PI _A _B) SET (PI _S _T)) = +> return [ EQN SET _A SET _S +> , EQN (_A --> SET) _B (_S --> SET) _T] +> +> rigidRigid (EQN SET (SIG _A _B) SET (SIG _S _T)) = +> return [ EQN SET _A SET _S +> , EQN (_A --> SET) _B (_S --> SET) _T] +> +> rigidRigid (EQN _S (N (Var x w) ds) _T (N (Var y w') es)) +> | x == y = do +> _X <- lookupVar x w +> _Y <- lookupVar y w' +> (EQN SET _X SET _Y :) <$> +> matchSpine _X (N (Var x w) []) ds +> _Y (N (Var y w') []) es +> +> rigidRigid _ = throwError "Rigid-rigid mismatch" + + +When we have the same rigid variable (or twins) at the head on both +sides, we proceed down the spine, demanding that projections are +identical and unifying terms in applications. Note that |matchSpine| +heterogeneously unfolds the types of the terms being applied to +determine the types of the arguments. For example, if +$[[x : Pi a : A . B a -> C]]$ then the constraint $[[x s t == x u v]]$ +will decompose into +$[[(s : A) == (u : A) && (t : B s) == (v : B u)]]$. + +> matchSpine :: Type -> VAL -> [Elim] -> +> Type -> VAL -> [Elim] -> +> Contextual [Equation] +> matchSpine (PI _A _B) u (A a:ds) +> (PI _S _T) v (A s:es) = +> (EQN _A a _S s :) <$> +> matchSpine (_B $$ a) (u $$ a) ds (_T $$ s) (v $$ s) es +> matchSpine (SIG _A _B) u (Hd:ds) (SIG _S _T) v (Hd:es) = +> matchSpine _A (u %% Hd) ds _S (v %% Hd) es +> matchSpine (SIG _A _B) u (Tl:ds) (SIG _S _T) v (Tl:es) = +> matchSpine (_B $$ a) b ds (_T $$ s) t es +> where (a, b) = (u %% Hd, u %% Tl) +> (s, t) = (v %% Hd, v %% Tl) +> matchSpine _ _ [] _ _ [] = return [] +> matchSpine _ _ _ _ _ _ = throwError "spine mismatch" + + +\subsection{Flex-rigid equations} +\label{subsec:impl:flex-rigid} + +A flex-rigid unification problem is one where one side is an applied +metavariable and the other is a non-metavariable term. We move left +in the context, accumulating a list of metavariables that the term +depends on (the bracketed list of entries $[[XI]]$ in the rules). +Once we reach the target metavariable, we attempt to find a solution +by inversion. This implements the steps in +Figure~\ref{fig:flex-rigid}, as described in +subsection~\ref{subsec:spec:flex-rigid}. + +> flexRigid :: [Entry] -> ProbId -> Equation -> Contextual () +> flexRigid _Xi n q@(EQN _ (N (Meta alpha) _) _ _) = do +> _Gam <- ask +> popL >>= \ e -> case e of +> E beta _T HOLE +> | alpha == beta && alpha `elem` fmvs _Xi -> pushL e >> +> mapM_ pushL _Xi >> +> block n q +> | alpha == beta -> mapM_ pushL _Xi >> +> tryInvert n q _T +> ( block n q >> +> pushL e) +> | beta `elem` fmvs (_Gam, _Xi, q) -> flexRigid (e : _Xi) n q +> _ -> pushR (Right e) >> +> flexRigid _Xi n q + +%if False + +> flexRigid _ _ q = error $ "flexRigid: " ++ show q + +%endif + +Given a flex-rigid or flex-flex equation whose head metavariable has +just been found in the context, the |tryInvert| control operator calls +|invert| to seek a solution to the equation. If it finds one, it +defines the metavariable and leaves the equation in the context (so +the definition will be substituted out and the equation found to be +reflexive by the constraint solver). If |invert| cannot find a +solution, it runs the continuation. + +> tryInvert :: ProbId -> Equation -> Type -> Contextual () -> +> Contextual () +> tryInvert n q@(EQN _ (N (Meta alpha) es) _ s) _T k = +> invert alpha _T es s >>= \case +> Nothing -> k +> Just v -> active n q >> +> define [] alpha _T v + +%if False + +> tryInvert _ _ q _ = error $ "tryInvert: " ++ show q + +%endif + + +Given a metavariable $[[alpha]]$ of type $[[T]]$, spine +$[[]]$ and term $[[t]]$, |invert| attempts to find a value +for $[[alpha]]$ that solves the equation +$[[alpha == t]]$. It may also throw an error +if the problem is unsolvable due to an impossible (strong rigid) +occurrence. + +> invert :: Nom -> Type -> [Elim] -> VAL -> +> Contextual (Maybe VAL) +> invert alpha _T es t = do +> let o = occurrence [alpha] t +> when (isStrongRigid o) $ throwError "occurrence" +> case toVars es of +> Just xs | isNothing o && linearOn t xs -> do +> b <- localParams (const []) (typecheck _T (lams xs t)) +> return $ if b then Just (lams xs t) else Nothing +> _ -> return Nothing + +Here |toVars :: [Elim] -> Maybe [Nom]| tries to convert a spine to a +list of variables, and |linearOn :: VAL -> [Nom] -> Bool| determines +if a list of variables is linear on the free variables of a term. Note +that we typecheck the solution |lams xs t| under no parameters, so +typechecking will fail if an out-of-scope variable is used. + + +\subsection{Flex-flex equations} +\label{subsec:impl:flex-flex} + +A flex-flex unification problem is one where both sides are applied +metavariables. As in the flex-rigid case, we proceed leftwards +through the context, looking for one of the metavariables so we can +try to solve it with the other. This implements the steps in +Figure~\ref{fig:flex-flex}, as described in +subsection~\ref{subsec:spec:flex-flex}. + +> flexFlex :: ProbId -> Equation -> Contextual () +> flexFlex n q@(EQN _ (N (Meta alpha) ds) _ (N (Meta beta) es)) = do +> _Gam <- ask +> popL >>= \ e -> case e of +> E gamma _T HOLE +> | gamma == alpha && gamma == beta -> block n q >> +> tryIntersect alpha _T ds es +> | gamma == alpha -> tryInvert n q _T +> (flexRigid [e] n (sym q)) +> | gamma == beta -> tryInvert n (sym q) _T +> (flexRigid [e] n q) +> | gamma `elem` fmvs (_Gam, q) -> pushL e >> +> block n q +> _ -> pushR (Right e) >> +> flexFlex n q + +%if False + +> flexFlex _ q = error $ "flexFlex: " ++ show q + +%endif + +%% Consider the case $[[alpha == beta ]]$ +%% where $[[]]$ is a list of variables but +%% $[[]]$ is not. If we reach $[[alpha]]$ first then we +%% might get stuck even if we could potentially solve for +%% $[[beta]]$. This would be correct if order were important in the +%% metacontext, for example if we wanted to implement let-generalisation +%% \citep{gundry2010}. Here it is not, so we can simply pick up +%% $[[alpha]]$ and carry on moving left. + + +When we have a flex-flex equation with the same metavariable on both +sides, $[[alpha == alpha ]]$, where +$[[]]$ and $[[]]$ are both lists of +variables, we can solve the equation by restricting $[[alpha]]$ to the +arguments on which $[[]]$ and $[[]]$ agree +(i.e. creating a new metavariable $[[beta]]$ and using it to solve +$[[alpha]]$). The |tryIntersect| control operator tests if both spines are +lists of variables, then calls |intersect| to generate a restricted +type for the metavariable. If this succeeds, it creates a new +metavariable and solves the old one. Otherwise, it leaves the old +metavariable in the context. + +> tryIntersect :: Nom -> Type -> [Elim] -> [Elim] -> +> Contextual () +> tryIntersect alpha _T ds es = case (toVars ds, toVars es) of +> (Just xs, Just ys) -> intersect [] [] _T xs ys >>= \case +> Just (_U, f) -> hole [] _U $ \ beta -> +> define [] alpha _T (f beta) +> Nothing -> pushL (E alpha _T HOLE) +> _ -> pushL (E alpha _T HOLE) + +Given the type of $[[alpha]]$ and the two spines, |intersect| produces +a type for $[[beta]]$ and a term with which to solve $[[alpha]]$ given +$[[beta]]$. It accumulates lists of the original and retained +parameters (|_Phi| and |_Psi| respectively). + +> intersect :: Fresh m => [(Nom, Type)] -> [(Nom, Type)] -> +> Type -> [Nom] -> [Nom] -> +> m (Maybe (Type, VAL -> VAL)) +> intersect _Phi _Psi _S [] [] +> | fvs _S `Set.isSubsetOf` vars _Psi = return $ Just +> (_Pis _Psi _S, \ beta -> lams' _Phi (beta $*$ _Psi)) +> | otherwise = return Nothing +> intersect _Phi _Psi (PI _A _B) (x:xs) (y:ys) = do +> z <- freshNom +> let _Psi' = _Psi ++ if x == y then [(z, _A)] else [] +> intersect (_Phi ++ [(z, _A)]) _Psi' (_B $$ var z) xs ys + +%if False + +> intersect _ _ _ _ _ = error "intersect: ill-typed!" + +%endif + +Note that we have to generate fresh names in case the renamings are +not linear. Also note that the resulting type is well-formed: if the +domain of a $\Pi$ depends on a previous variable that was removed, +then the renamings will not agree, so it will be removed as well. + + +\subsection{Pruning} +\label{subsec:impl:pruning} + +When we have a flex-rigid or flex-flex equation, we might be able to +make some progress by pruning the metavariables contained within it, +as described in Figure~\ref{fig:pruning} and +subsection~\ref{subsec:spec:pruning}. The |tryPrune| control operator calls +|prune|, and if it learns anything from pruning, leaves the current +problem where it is and instantiates the pruned metavariable. If not, +it runs the continuation. + +> tryPrune :: ProbId -> Equation -> +> Contextual () -> Contextual () +> tryPrune n q@(EQN _ (N (Meta _) ds) _ t) k = do +> _Gam <- ask +> u <- prune (Set.toList $ vars _Gam Set.\\ fvs ds) t +> case u of +> d:_ -> active n q >> instantiate d +> [] -> k + +%if False + +> tryPrune _ q _ = error $ "tryPrune: " ++ show q + +%endif + +Pruning a term requires traversing it looking for occurrences of +forbidden variables. If any occur rigidly, the corresponding +constraint is impossible. On the other hand, if we encounter a +metavariable, we observe that it cannot depend on any arguments that +contain rigid occurrences of forbidden variables. This can be +implemented by replacing it with a fresh variable of restricted type. +The |prune| function generates a list of triples |(beta, _U, f)| where +|beta| is a metavariable, |_U| is a type for a new metavariable +|gamma| and |f gamma| is a solution for |beta|. We maintain the +invariant that |_U| and |f gamma| depend only on metavariables defined +prior to |beta| in the context. + +> prune :: [Nom] -> VAL -> +> Contextual [(Nom, Type, VAL -> VAL)] +> prune _ SET = return [] +> prune xs (PI _S _T) = (++) <$> prune xs _S <*> prune xs _T +> prune xs (SIG _S _T) = (++) <$> prune xs _S <*> prune xs _T +> prune xs (PAIR s t) = (++) <$> prune xs s <*> prune xs t +> prune xs (L b) = prune xs . snd =<< unbind b +> prune xs (N (Var z _) es) +> | z `elem` xs = throwError "pruning error" +> | otherwise = concat <$> mapM pruneElim es +> where pruneElim (A a) = prune xs a +> pruneElim _ = return [] +> prune xs (N (Meta beta) es) = do +> _T <- lookupMeta beta +> maybe [] (\ (_U, f) -> [(beta, _U, f)]) <$> +> pruneSpine [] [] xs _T es + +%if False + +> prune _ (C {}) = error "concat <$> mapM (prune xs) ts" + +%endif + +Once a metavariable has been found, |pruneSpine| unfolds its type and +inspects its arguments, generating lists of unpruned and pruned +arguments (|_Phi| and |_Psi|). If an argument contains a rigid +occurrence of a forbidden variable, or its type rigidly depends on a +previously removed argument, then it is removed. Ultimately, it +generates a simplified type for the metavariable if the codomain type +does not depend on a pruned argument. + +> pruneSpine :: [(Nom, Type)] -> [(Nom, Type)] -> +> [Nom] -> Type -> [Elim] -> +> Contextual (Maybe (Type, VAL -> VAL)) +> pruneSpine _Phi _Psi xs (PI _A _B) (A a:es) +> | not stuck = do +> z <- freshNom +> let _Psi' = _Psi ++ if pruned then [] else [(z, _A)] +> pruneSpine (_Phi ++ [(z, _A)]) _Psi' xs (_B $$ var z) es +> | otherwise = return Nothing +> where +> o = occurrence xs a +> o' = occurrence (Set.toList $ vars _Phi Set.\\ vars _Psi) _A +> pruned = isRigid o || isRigid o' +> stuck = isFlexible o || (isNothing o && isFlexible o') +> || (not pruned && not (isVar a)) +> pruneSpine _Phi _Psi _ _T [] | fvs _T `Set.isSubsetOf` vars _Psi && _Phi /= _Psi = +> return $ Just (_Pis _Psi _T, \ v -> lams' _Phi (v $*$ _Psi)) +> pruneSpine _ _ _ _ _ = return Nothing + +After pruning, we can |instantiate| a pruned metavariable by moving +left through the context until we find the relevant metavariable, then +creating a new metavariable and solving the old one. + +> instantiate :: (Nom, Type, VAL -> VAL) -> Contextual () +> instantiate d@(alpha, _T, f) = popL >>= \ e -> case e of +> E beta _U HOLE | alpha == beta -> hole [] _T $ \ t -> +> define [] beta _U (f t) +> _ -> pushR (Right e) >> +> instantiate d + + +\subsection{Metavariable and problem simplification} +\label{subsec:impl:simplification} + +Given a problem, the |solver| simplifies it according to the rules in +Figure~\ref{fig:solve}, introduces parameters and calls |unify| from +subsection~\ref{subsec:impl:unification}. In particular, it removes +$\Sigma$-types from parameters, potentially eliminating projections, +and replaces twins whose types are definitionally equal with a normal +parameter. + +> solver :: ProbId -> Problem -> Contextual () +> solver n (Unify q) = isReflexive q >>= \ b -> +> if b then solved n q +> else unify n q `catchError` failed n q +> solver n (All p b) = do +> (x, q) <- unbind b +> case p of +> _ | x `notElem` fvs q -> simplify n (All p b) [q] +> P _S -> splitSig [] x _S >>= \case +> Just (y, _A, z, _B, s, _) -> +> solver n (allProb y _A (allProb z _B (subst x s q))) +> Nothing -> localParams (++ [(x, P _S)]) $ solver n q +> Twins _S _T -> equal SET _S _T >>= \ c -> +> if c then solver n (allProb x _S (subst x (var x) q)) +> else localParams (++ [(x, Twins _S _T)]) $ solver n q +> + +\newpage +Given the name and type of a metavariable, |lower| attempts to +simplify it by removing $\Sigma$-types, according to the metavariable +simplification rules in Figure~\ref{fig:solve}. If it cannot be +simplified, it appends it to the (left) context. + +> lower :: [(Nom, Type)] -> Nom -> Type -> Contextual () +> lower _Phi alpha (SIG _S _T) = hole _Phi _S $ \ s -> +> hole _Phi (_T $$ s) $ \ t -> +> define _Phi alpha (SIG _S _T) (PAIR s t) +> +> lower _Phi alpha (PI _S _T) = do +> x <- freshNom +> splitSig [] x _S >>= maybe +> (lower (_Phi ++ [(x, _S)]) alpha (_T $$ var x)) +> (\ (y, _A, z, _B, s, (u, v)) -> +> hole _Phi (_Pi y _A (_Pi z _B (_T $$ s))) $ \ w -> +> define _Phi alpha (PI _S _T) (lam x (w $$ u $$ v))) +> +> lower _Phi alpha _T = pushL (E alpha (_Pis _Phi _T) HOLE) + + +Both |solver| and |lower| above need to split $\Sigma$-types (possibly +underneath a bunch of parameters) into their components. For example, +$[[y : Pi x : X . Sigma S T]]$ splits into $[[y0 : Pi x : X . S]]$ and +$[[y1 : Pi x : X . T (y0 x)]]$. Given the name of a variable and its +type, |splitSig| attempts to split it, returning fresh variables for +the two components of the $\Sigma$-type, an inhabitant of the original +type in terms of the new variables and inhabitants of the new types by +projecting the original variable. + +> splitSig :: Fresh m => [(Nom, Type)] -> Nom -> Type -> +> m (Maybe (Nom, Type, Nom, Type, +> VAL, (VAL, VAL))) +> splitSig _Phi x (SIG _S _T) = do +> y <- freshNom +> z <- freshNom +> return $ Just (y, _Pis _Phi _S, z, _Pis _Phi (_T $$ var y), +> lams' _Phi (PAIR (var y $*$ _Phi) (var z $*$ _Phi)), +> (lams' _Phi (var x $*$ _Phi %% Hd), +> lams' _Phi (var x $*$ _Phi %% Tl))) +> splitSig _Phi x (PI _A _B) = do +> a <- freshNom +> splitSig (_Phi ++ [(a, _A)]) x (_B $$ var a) +> splitSig _ _ _ = return Nothing + + +\subsection{Solvitur ambulando} +\label{subsec:impl:ambulando} + +We organise constraint solving via an automaton that lazily propagates +a substitution rightwards through the metacontext, making progress on +active problems and maintaining the invariant that the entries to the +left include no active problems. This is not the only possible +strategy: indeed, it is crucial for guaranteeing most general +solutions that solving the constraints in any order would produce the +same result. + +A problem may be in any of five possible states: |Active| and ready to +be worked on; |Blocked| and unable to make progress in its current +state; |Pending| the solution of some other problems in order to +become solved itself; |Solved| as it has become reflexive; or |Failed| +because it is unsolvable. The specification simply removes constraints +that are pending or solved, and represents failed constraints as +failure of the whole process, but in practice it is often useful to have a +more fine-grained representation. + +< data ProblemState = Active | Blocked | Pending [ProbId] +< | Solved | Failed String + +In the interests of simplicity, |Blocked| problems do not store any +information about when they may be resumed, and applying a +substitution that modifies them in any way makes them |Active|. A +useful optimisation would be to track the conditions under which they +should become active, typically when particular metavariables are +solved or types become definitionally equal. + + +The |ambulando| automaton carries a list of problems that have been +solved, for updating the state of subsequent problems, and a +substitution with definitions for metavariables. + +> ambulando :: [ProbId] -> Subs -> Contextual () +> ambulando ns theta = popR >>= \case +> -- if right context is empty, stop +> Nothing -> return () +> -- compose suspended substitutions +> Just (Left theta') -> ambulando ns (compSubs theta theta') +> -- process entries +> Just (Right e) -> case update ns theta e of +> Prob n p Active -> pushR (Left theta) >> +> solver n p >> +> ambulando ns [] +> Prob n p Solved -> pushL (Prob n p Solved) >> +> ambulando (n:ns) theta +> E alpha _T HOLE -> lower [] alpha _T >> +> ambulando ns theta +> e' -> pushL e' >> +> ambulando ns theta + +Given a list of solved problems, a substitution and an entry, |update| +returns a modified entry with the substitution applied and the problem +state changed if appropriate. + +> update :: [ProbId] -> Subs -> Entry -> Entry +> update _ theta (Prob n p Blocked) = Prob n p' k +> where p' = substs theta p +> k = if p `aeq` p' then Blocked else Active +> update ns theta (Prob n p (Pending ys)) +> | null rs = Prob n p' Solved +> | otherwise = Prob n p' (Pending rs) +> where rs = ys \\ ns +> p' = substs theta p +> update _ _ e'@(Prob _ _ Solved) = e' +> update _ _ e'@(Prob _ _ (Failed _)) = e' +> update _ theta e' = substs theta e' diff --git a/patuni.cabal b/patuni.cabal new file mode 100644 index 0000000..353bd5e --- /dev/null +++ b/patuni.cabal @@ -0,0 +1,42 @@ +cabal-version: 3.0 +name: patuni +version: 1.0 + +synopsis: A tutorial implementation of dynamic pattern unification +description: + The code from /A tutorial implementation of dynamic pattern unification/ + by Adam Gundry and Conor McBride, updated to work with GHC 9.2 and up, + @unbound-generics@ instead of @unbound@, and without SHE. + +license: BSD-3-Clause +license-file: LICENSE +author: Adam Gundry, Conor McBride +maintainer: rhiannon morris +build-type: Simple + +extra-doc-files: CHANGELOG.md + +tested-with: + GHC == 9.2.7, + GHC == 9.4.7, + GHC == 9.6.4, + GHC == 9.8.2, + GHC == 9.10.1 + +library + ghc-options: -Wall + + hs-source-dirs: . + exposed-modules: Check, Context, Kit, Tm, Unify, Test + + default-language: GHC2021 + default-extensions: + DeriveAnyClass, DerivingStrategies, GADTs, LambdaCase, + PatternSynonyms, UndecidableInstances + + build-depends: + base >= 4.16.4.0 && < 4.21, + containers ^>= 0.6.7, + mtl ^>= 2.2.2, + pretty ^>= 1.1.3, + unbound-generics ^>= 0.4.4