commit cb58d03b282b6e2c93aa0d2ea5c3cc65a2f4fcf1 Author: rhiannon morris Date: Sun Jun 23 18:03:32 2024 +0200 first 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