rhi/patuni
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

first

Browse source
This commit is contained in:
rhiannon morris 2024-06-23 18:03:32 +02:00
commit cb58d03b28
11 changed files with 2329 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
.gitignore vendored Normal file
View file

@ -0,0 +1 @@
dist-newstyle

5
CHANGELOG.md Normal file
View file

@ -0,0 +1,5 @@
# Revision history for patuni
## 1.0 -- 2024-06-23
* Updated for GHC 9.2–9.10

195
Check.lhs Normal file
View file

@ -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

266
Context.lhs Normal file
View file

@ -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

91
Kit.lhs Normal file
View file

@ -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

30
LICENSE Normal file
View file

@ -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.

11
README.txt Normal file
View file

@ -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.

716
Test.lhs Normal file
View file

@ -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)
> : [])
> ]

333
Tm.lhs Normal file
View file

@ -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 (%%)

639
Unify.lhs Normal file
View file

@ -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
$[[</ ei // i/>]]$ and term $[[t]]$, |invert| attempts to find a value
for $[[alpha]]$ that solves the equation
$[[alpha </ ei // i /> == 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 </ ei // i /> == beta </ xj // j />]]$
%% where $[[</ xj // j />]]$ is a list of variables but
%% $[[</ ei // i />]]$ 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 </ xi // i /> == alpha </ yi // i />]]$, where
$[[</ xi // i />]]$ and $[[</ yi // i />]]$ are both lists of
variables, we can solve the equation by restricting $[[alpha]]$ to the
arguments on which $[[</ xi // i />]]$ and $[[</ yi // i />]]$ 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'

42
patuni.cabal Normal file
View file

@ -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 <rhi@rhiannon.website>
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