640 lines
26 KiB
Plaintext
640 lines
26 KiB
Plaintext
%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'
|