diff --git a/src/Continuations/Core/Term.hs b/src/Continuations/Core/Term.hs index 5edb16a..a2823af 100644 --- a/src/Continuations/Core/Term.hs +++ b/src/Continuations/Core/Term.hs @@ -142,14 +142,15 @@ instance Bizippable PatternFF where instance Bitraversable PatternFF where - bisequenceA (ConPat c ps) = - ConPat c <$> sequenceA [ (,) plic <$> p - | (plic,p) <- ps - ] - bisequenceA (AssertionPat m) = - AssertionPat <$> m - bisequenceA MakeMeta = - pure MakeMeta + bitraverse f g = biseq . bimap f g where + biseq (ConPat c ps) = + ConPat c <$> sequenceA [ (,) plic <$> p + | (plic,p) <- ps + ] + biseq (AssertionPat m) = + AssertionPat <$> m + biseq MakeMeta = + pure MakeMeta -- | 'PatternF' is the type of pattern shaped containers for terms. The diff --git a/src/Continuations/Unification/TypeChecking.hs b/src/Continuations/Unification/TypeChecking.hs index acf260d..ec0a333 100644 --- a/src/Continuations/Unification/TypeChecking.hs +++ b/src/Continuations/Unification/TypeChecking.hs @@ -344,7 +344,7 @@ inferify (Var (Free x)) = return (ElaboratedTerm (Var (Free x)), t) inferify (Var (Bound _ _)) = error "Bound type variables should not be the subject of type checking." -inferify (Var (Meta x)) = +inferify (Var (Meta _ x)) = throwError $ "The metavariable " ++ show x ++ " appears in checkable code, when it should not." inferify (In (Defined x)) = @@ -550,8 +550,8 @@ inferifyApplication f (In (Fun Expl _ _)) Impl m = ++ pretty (appH Impl f m) inferifyApplication f (In (Fun Impl _ sc)) Expl m = do meta <- nextElab nextMeta - let f' = appH Impl f (Var (Meta meta)) - t' = instantiate sc [Var (Meta meta)] + let f' = appH Impl f (Var (Meta Exist meta)) + t' = instantiate sc [Var (Meta Exist meta)] inferifyApplication f' t' Expl m inferifyApplication f _ _ _ = throwError $ "Cannot apply non-function: " ++ pretty f @@ -608,7 +608,7 @@ inferifyConArgs ascs0 bsc0 ms0 = go [] ascs0 bsc0 ms0 go (acc ++ [(Impl,m')]) ascs bsc ms go acc ((Impl,_):ascs) bsc ms = do meta <- nextElab nextMeta - go (acc ++ [(Impl,Var (Meta meta))]) ascs bsc ms + go (acc ++ [(Impl,Var (Meta Exist meta))]) ascs bsc ms go _ _ _ _ = throwError "Cannot match signature." @@ -886,7 +886,7 @@ checkifyConArgs ascs0 bsc ms0 t = return acc accArgsToCheck acc ((Expl,asc):ascs) ((Expl,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Expl, Just m, x, instantiate asc xs) accArgsToCheck @@ -895,7 +895,7 @@ checkifyConArgs ascs0 bsc ms0 t = ms accArgsToCheck acc ((Impl,asc):ascs) ((Impl,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Just m, x, instantiate asc xs) accArgsToCheck @@ -904,7 +904,7 @@ checkifyConArgs ascs0 bsc ms0 t = ms accArgsToCheck acc ((Impl,asc):ascs) ms = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Nothing, x, instantiate asc xs) accArgsToCheck @@ -917,12 +917,12 @@ checkifyConArgs ascs0 bsc ms0 t = swapMetas :: [(Plicity,Term)] -> TypeChecker ([(Term,Term)], [(Plicity,Term)]) swapMetas [] = return ([],[]) - swapMetas ((plic, Var (Meta meta)):ms) = + swapMetas ((plic, Var (Meta Exist meta)):ms) = do (eqs,ms') <- swapMetas ms - return (eqs, (plic,Var (Meta meta)):ms') + return (eqs, (plic,Var (Meta Exist meta)):ms') swapMetas ((plic,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) (eqs,ms') <- swapMetas ms return ((x,m):eqs, (plic,x):ms') @@ -978,7 +978,7 @@ checkifyCaseMotive (CaseMotive tele) = checkifyPattern :: Pattern -> NormalTerm - -> TypeChecker (Pattern,ElaboratedTerm) + -> TypeChecker (Pattern,ElaboratedTerm,[(Term,Term)]) checkifyPattern (Var (Bound _ _)) _ = error "A bound variable should not be the subject of pattern type checking." checkifyPattern (Var (Free x)) t = @@ -986,12 +986,13 @@ checkifyPattern (Var (Free x)) t = unifyHelper t (NormalTerm t') -- @t'@ is guaranteed to be normal return ( Var (Free x) , ElaboratedTerm (Var (Free x)) + , [] ) -checkifyPattern (Var (Meta _)) _ = +checkifyPattern (Var (Meta _ _)) _ = error "Metavariables should not be the subject of pattern type checking." checkifyPattern (In (ConPat c ps)) (NormalTerm t) = do (ec,ConSig plics (BindingTelescope ascs bsc)) <- typeInSignature c - (ps',elms') <- + (ps',elms',cs) <- checkifyPatterns (zip plics ascs) bsc @@ -1000,17 +1001,21 @@ checkifyPattern (In (ConPat c ps)) (NormalTerm t) = let ms' = [ (plic,m') | (plic, ElaboratedTerm m') <- elms' ] return ( conPatH ec ps' , ElaboratedTerm (conH ec ms') + , cs ) checkifyPattern (In (AssertionPat m)) t = do ElaboratedTerm m' <- checkify m t + mv <- nextElab nextMeta return ( In (AssertionPat m') - , ElaboratedTerm m' + , ElaboratedTerm (Var $ Meta Constraint mv) + , [(Var $ Meta Constraint mv, m')] ) checkifyPattern (In MakeMeta) _ = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) return ( In (AssertionPat x) , ElaboratedTerm x + , [] ) @@ -1049,6 +1054,7 @@ checkifyPatterns :: [(Plicity,Scope TermF)] -> Term -> TypeChecker ( [(Plicity,Pattern)] , [(Plicity,ElaboratedTerm)] + , [(Term,Term)] ) checkifyPatterns ascs0 bsc ps0 t = do argsToCheck <- accArgsToCheck [] ascs0 ps0 @@ -1062,33 +1068,36 @@ checkifyPatterns ascs0 bsc ps0 t = return (eqs,ret') ret' -> return ([],ret') unifyHelper (NormalTerm ret') (NormalTerm t) - psms' <- forM argsToCheck $ \(plic,p0,mToElabInto,a) -> + (ps',ms',cs) <- unzip3 <$> forM argsToCheck (\(plic,p0,mToElabInto,a) -> case p0 of Nothing -> do subMToElabInto <- substitute mToElabInto em' <- evaluate subMToElabInto return ( (plic, In (AssertionPat (normTerm em'))) , (plic, ElaboratedTerm (normTerm em')) + , [] ) Just p -> do subMToElabInto <- substitute mToElabInto eMToElabInto <- evaluate subMToElabInto suba <- substitute a ea <- evaluate suba - (p',ElaboratedTerm m') <- checkifyPattern p ea + (p',ElaboratedTerm m',cs) <- checkifyPattern p ea subm' <- substitute m' em' <- evaluate subm' unifyHelper eMToElabInto em' return ( (plic, p') , (plic, ElaboratedTerm (normTerm em')) + , cs ) + ) forM_ eqs $ \(l,r) -> do subl <- substitute l el <- evaluate subl subr <- substitute r er <- evaluate subr unifyHelper el er - return $ unzip psms' + return (ps',ms',concat cs) where accArgsToCheck :: [(Plicity,Maybe Pattern,Term,Term)] -> [(Plicity,Scope TermF)] @@ -1098,7 +1107,7 @@ checkifyPatterns ascs0 bsc ps0 t = return acc accArgsToCheck acc ((Expl,asc):ascs) ((Expl,p):ps) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Expl, Just p, x, instantiate asc xs) accArgsToCheck @@ -1107,7 +1116,7 @@ checkifyPatterns ascs0 bsc ps0 t = ps accArgsToCheck acc ((Impl,asc):ascs) ((Impl,p):ps) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Just p, x, instantiate asc xs) accArgsToCheck @@ -1116,7 +1125,7 @@ checkifyPatterns ascs0 bsc ps0 t = ps accArgsToCheck acc ((Impl,asc):ascs) ps = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Nothing, x, instantiate asc xs) accArgsToCheck @@ -1129,12 +1138,12 @@ checkifyPatterns ascs0 bsc ps0 t = swapMetas :: [(Plicity,Term)] -> TypeChecker ([(Term,Term)], [(Plicity,Term)]) swapMetas [] = return ([],[]) - swapMetas ((plic, Var (Meta meta)):ms) = + swapMetas ((plic, Var (Meta Exist meta)):ms) = do (eqs,ms') <- swapMetas ms - return (eqs, (plic,Var (Meta meta)):ms') + return (eqs, (plic,Var (Meta Exist meta)):ms') swapMetas ((plic,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) (eqs,ms') <- swapMetas ms return ((x,m):eqs, (plic,x):ms') @@ -1160,21 +1169,34 @@ checkifyPatternsCaseMotive :: [Pattern] -> CaseMotive -> TypeChecker ([Pattern], ElaboratedTerm) checkifyPatternsCaseMotive ps0 (CaseMotive (BindingTelescope ascs bsc)) = - do (ps',ms') <- go [] ps0 ascs + do (ps',ms',cs) <- go [] ps0 ascs + forM_ cs (\(l,r) -> do + subl <- substitute l + el <- evaluate subl + subr <- substitute r + er <- evaluate subr + s <- getElab substitution + unifyHelper el er + s' <- getElab substitution + when (length s /= length s') $ + throwError $ "Solving the constraint " + ++ pretty (normTerm el) ++ " == " + ++ pretty (normTerm er) ++ " produced new metavar resolution" + ) return (ps', ElaboratedTerm (instantiate bsc ms')) where go :: [Term] -> [Pattern] -> [Scope TermF] - -> TypeChecker ([Pattern],[Term]) + -> TypeChecker ([Pattern],[Term],[(Term,Term)]) go _ [] [] = - return ([],[]) + return ([],[],[]) go acc (p:ps) (sc:scs) = do subt <- substitute (instantiate sc acc) et <- evaluate subt - (p',ElaboratedTerm m') <- checkifyPattern p et - (ps',ms') <- go (acc ++ [m']) ps scs - return (p':ps', m':ms') + (p',ElaboratedTerm m',cs) <- checkifyPattern p et + (ps',ms',cs') <- go (acc ++ [m']) ps scs + return (p':ps', m':ms', cs ++ cs') go _ _ _ = error $ "The auxiliary function 'go' in 'checkPatternsCaseMotive'" ++ " should always have equal number of args for its patterns and" @@ -1208,7 +1230,7 @@ checkifyClause (Clause pscs sc) mot@(CaseMotive (BindingTelescope ascs _)) = l <- getElab quoteLevel ctx' <- forM ns $ \n -> do m <- nextElab nextMeta - return (n, QLJ (Var (Meta m)) l) + return (n, QLJ (Var (Meta Exist m)) l) extendElab context ctx' $ do (ps',ElaboratedTerm ret) <- checkifyPatternsCaseMotive diff --git a/src/Continuations/Unification/Unification.hs b/src/Continuations/Unification/Unification.hs index a08ffbc..42e77b3 100644 --- a/src/Continuations/Unification/Unification.hs +++ b/src/Continuations/Unification/Unification.hs @@ -35,44 +35,44 @@ import Control.Monad.Except -- | Equating terms by trivial structural equations. instance MonadUnify TermF Elaborator where - equate (Defined n1) (Defined n2) = + equate _ (Defined n1) (Defined n2) = if n1 == n2 then return [] else throwError $ "Mismatching names " ++ showName n1 ++ " and " ++ showName n2 - equate (Ann m1 t1) (Ann m2 t2) = - return [ Equation (instantiate0 m1) (instantiate0 m2) - , Equation (instantiate0 t1) (instantiate0 t2) + equate f (Ann m1 t1) (Ann m2 t2) = + return [ Equation f (instantiate0 m1) (instantiate0 m2) + , Equation f (instantiate0 t1) (instantiate0 t2) ] - equate Type Type = + equate _ Type Type = return [] - equate (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) = + equate f (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) = do unless (plic1 == plic2) $ throwError $ "Mismatching plicities when unifying " ++ pretty (In (Fun plic1 a1 sc1)) ++ " with " ++ pretty (In (Fun plic2 a2 sc2)) ns <- freshRelTo (names sc1) context let xs = map (Var . Free) ns - return [ Equation (instantiate0 a1) (instantiate0 a2) - , Equation (instantiate sc1 xs) (instantiate sc2 xs) + return [ Equation f (instantiate0 a1) (instantiate0 a2) + , Equation f (instantiate sc1 xs) (instantiate sc2 xs) ] - equate (Lam plic1 sc1) (Lam plic2 sc2) = + equate f (Lam plic1 sc1) (Lam plic2 sc2) = do unless (plic1 == plic2) $ throwError $ "Mismatching plicities when unifying " ++ pretty (In (Lam plic1 sc1)) ++ " with " ++ pretty (In (Lam plic2 sc2)) ns <- freshRelTo (names sc1) context let xs = map (Var . Free) ns - return [ Equation (instantiate sc1 xs) (instantiate sc2 xs) ] - equate (App plic1 f1 a1) (App plic2 f2 a2) = + return [ Equation f (instantiate sc1 xs) (instantiate sc2 xs) ] + equate _ (App plic1 f1 a1) (App plic2 f2 a2) = do unless (plic1 == plic2) $ throwError $ "Mismatching plicities when unifying " ++ pretty (In (App plic1 f1 a1)) ++ " with " ++ pretty (In (App plic2 f2 a2)) - return [ Equation (instantiate0 f1) (instantiate0 f2) - , Equation (instantiate0 a1) (instantiate0 a2) + return [ Equation False (instantiate0 f1) (instantiate0 f2) + , Equation False (instantiate0 a1) (instantiate0 a2) ] - equate (Con c1 as1) (Con c2 as2) = + equate f (Con c1 as1) (Con c2 as2) = do unless (c1 == c2) $ throwError $ "Mismatching constructors " ++ showName c1 ++ " and " ++ showName c2 @@ -87,10 +87,10 @@ instance MonadUnify TermF Elaborator where ++ pretty (In (Con c1 as1)) ++ " with " ++ pretty (In (Con c2 as2)) return $ zipWith - Equation + (Equation f) (map instantiate0 as1') (map instantiate0 as2') - equate (Case as1 mot1 cs1) (Case as2 mot2 cs2) = + equate _ (Case as1 mot1 cs1) (Case as2 mot2 cs2) = do unless (length as1 == length as2) $ throwError $ "Mismatching number of case arguments in " ++ pretty (In (Case as1 mot1 cs1)) ++ " and " @@ -100,13 +100,13 @@ instance MonadUnify TermF Elaborator where ++ pretty (In (Case as1 mot1 cs1)) ++ " and " ++ pretty (In (Case as2 mot2 cs2)) let argEqs = zipWith - Equation + (Equation False) (map instantiate0 as1) (map instantiate0 as2) motEqs <- equateCaseMotive mot1 mot2 clauseEqs <- fmap concat $ zipWithM equateClause cs1 cs2 return $ argEqs ++ motEqs ++ clauseEqs - equate (RecordType fields1 tele1) (RecordType fields2 tele2) = + equate f (RecordType fields1 tele1) (RecordType fields2 tele2) = do unless (fields1 == fields2) $ throwError $ "Record types have different field names: " ++ pretty (In (RecordType fields1 tele1)) @@ -121,8 +121,8 @@ instance MonadUnify TermF Elaborator where ++ pretty (In (RecordType fields1 tele1)) ++ " and " ++ pretty (In (RecordType fields2 tele2)) - return $ zipWith Equation as1 as2 - equate (RecordCon fields1) (RecordCon fields2) = + return $ zipWith (Equation f) as1 as2 + equate f (RecordCon fields1) (RecordCon fields2) = do unless (length fields1 == length fields2) $ throwError $ "Records have different number of fields: " ++ pretty (In (RecordCon fields1)) @@ -136,38 +136,38 @@ instance MonadUnify TermF Elaborator where ++ " and " ++ pretty (In (RecordCon fields2)) return $ zipWith - Equation + (Equation f) (map instantiate0 ms1) (map instantiate0 ms2) - equate (RecordProj r1 x1) (RecordProj r2 x2) = + equate _ (RecordProj r1 x1) (RecordProj r2 x2) = do unless (x1 == x2) $ throwError $ "Record projections have different names: " ++ pretty (In (RecordProj r1 x1)) ++ " and " ++ pretty (In (RecordProj r2 x2)) - return [Equation (instantiate0 r1) (instantiate0 r2)] - equate (QuotedType res1 a1) (QuotedType res2 a2) = + return [Equation False (instantiate0 r1) (instantiate0 r2)] + equate _ (QuotedType res1 a1) (QuotedType res2 a2) = do unless (res1 == res2) $ throwError $ "Quoted types have different reset locations: " ++ pretty (In (QuotedType res1 a1)) ++ " and " ++ pretty (In (QuotedType res2 a2)) - return [Equation (instantiate0 a1) (instantiate0 a2)] - equate (Quote m1) (Quote m2) = - return [Equation (instantiate0 m1) (instantiate0 m2)] - equate (Unquote m1) (Unquote m2) = - return [Equation (instantiate0 m1) (instantiate0 m2)] - equate (Continue m1) (Continue m2) = - return [Equation (instantiate0 m1) (instantiate0 m2)] - equate (Shift res1 m1) (Shift res2 m2) = + return [Equation False (instantiate0 a1) (instantiate0 a2)] + equate _ (Quote m1) (Quote m2) = + return [Equation False (instantiate0 m1) (instantiate0 m2)] + equate _ (Unquote m1) (Unquote m2) = + return [Equation False (instantiate0 m1) (instantiate0 m2)] + equate _ (Continue m1) (Continue m2) = + return [Equation False (instantiate0 m1) (instantiate0 m2)] + equate _ (Shift res1 m1) (Shift res2 m2) = do unless (res1 == res2) $ throwError "Shifts have different reset locations." - return [Equation (instantiate0 m1) (instantiate0 m2)] - equate (Reset res1 m1) (Reset res2 m2) = + return [Equation False (instantiate0 m1) (instantiate0 m2)] + equate _ (Reset res1 m1) (Reset res2 m2) = do unless (res1 == res2) $ throwError "Resets have different reset locations." - return [Equation (instantiate0 m1) (instantiate0 m2)] - equate l r = + return [Equation False (instantiate0 m1) (instantiate0 m2)] + equate _ l r = throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r) @@ -185,7 +185,7 @@ equateCaseMotive mot1@(CaseMotive tele1) mot2@(CaseMotive tele2) = unless (length as1 == length as2) $ throwError $ "Motives not equal: " ++ pretty mot1 ++ " and " ++ pretty mot2 - return $ zipWith Equation as1 as2 ++ [ Equation b1 b2 ] + return $ zipWith (Equation False) as1 as2 ++ [ Equation False b1 b2 ] @@ -210,5 +210,5 @@ equateClause (Clause pscs1 sc1) (Clause pscs2 sc2) = Nothing -> throwError "Patterns are not equal." Just pEqss -> - return $ [ Equation a1 a2 | (a1,a2) <- concat pEqss ] - ++ [ Equation b1 b2 ] \ No newline at end of file + return $ [ Equation False a1 a2 | (a1,a2) <- concat pEqss ] + ++ [ Equation False b1 b2 ] diff --git a/src/Dependent/Eq.sfp b/src/Dependent/Eq.sfp new file mode 100644 index 0000000..4ac7dcc --- /dev/null +++ b/src/Dependent/Eq.sfp @@ -0,0 +1,20 @@ + +data Eq (a : Type) (x : a) (y : a) where +| Refl (a : Type) (x : a) : Eq a x x +end + +let inj : + (a : Type) -> + (b : Type) -> + (f : a -> b) -> + (x : a) -> + (y : a) -> + (eq : Eq b (f x) (f y)) -> + Eq a x y = + \a -> \b -> \f -> \x -> \y -> \eq -> + case y || eq + motive (y' : a) || (eq' : Eq b (f x) (f y')) || Eq a x y' + of + | .x || Refl .b .(f x) -> Refl a x + end +end diff --git a/src/Dependent/EqAny.sfp b/src/Dependent/EqAny.sfp new file mode 100644 index 0000000..0b008f6 --- /dev/null +++ b/src/Dependent/EqAny.sfp @@ -0,0 +1,17 @@ + +data Eq (a : Type) (x : a) (y : a) where +| Refl (a : Type) (x : a) : Eq a x x +end + +let anyEq : + (a : Type) -> + (x : a) -> + (y : a) -> + Eq a x y = + \a -> \x -> \y -> + case y + motive (y' : a) || Eq a x y' + of + | .x -> Refl a x + end +end diff --git a/src/Dependent/Monadic/Equality.hs b/src/Dependent/Monadic/Equality.hs index 71ec4a6..bd7ce84 100644 --- a/src/Dependent/Monadic/Equality.hs +++ b/src/Dependent/Monadic/Equality.hs @@ -15,6 +15,7 @@ import Dependent.Core.Term import Data.Functor.Classes +import Utils.ABT @@ -22,42 +23,53 @@ import Data.Functor.Classes instance Eq1 TermF where - eq1 (Defined n) (Defined n') = + liftEq eq (Defined n) (Defined n') = n == n' - eq1 (Ann m t) (Ann m' t') = - m == m' && t == t' - eq1 Type Type = True - eq1 (Fun arg sc) (Fun arg' sc') = - arg == arg' && sc == sc' - eq1 (Lam sc) (Lam sc') = - sc == sc' - eq1 (App f x) (App f' x') = - f == f' && x == x' - eq1 (Con c as) (Con c' as') = - c == c' && as == as' - eq1 (Case as mot cls) (Case as' mot' cls') = - as == as' && eq1 mot mot' && - length cls == length cls' && and (zipWith eq1 cls cls') - eq1 _ _ = False + liftEq eq (Ann m t) (Ann m' t') = + eq m m' && eq t t' + liftEq eq Type Type = True + liftEq eq (Fun arg sc) (Fun arg' sc') = + eq arg arg' && eq sc sc' + liftEq eq (Lam sc) (Lam sc') = + eq sc sc' + liftEq eq (App f x) (App f' x') = + eq f f' && eq x x' + liftEq eq (Con c as) (Con c' as') = + c == c' && liftEq eq as as' + liftEq eq (Case as mot cls) (Case as' mot' cls') = + liftEq eq as as' && liftEq eq mot mot' && + length cls == length cls' && and (zipWith (liftEq eq) cls cls') + liftEq _ _ _ = False instance Eq1 CaseMotiveF where - eq1 (CaseMotive t) (CaseMotive t') = eq1 t t' + liftEq eq (CaseMotive t) (CaseMotive t') = liftEq eq t t' instance Eq1 ClauseF where - eq1 (Clause pscs bsc) (Clause pscs' bsc') = - length pscs == length pscs' && and (zipWith eq1 pscs pscs') && - bsc == bsc' + liftEq eq (Clause pscs bsc) (Clause pscs' bsc') = + length pscs == length pscs' && and (zipWith (liftEq eq) pscs pscs') && + eq bsc bsc' instance Eq1 PatternF where - eq1 (PatternF x) (PatternF y) = x == y + liftEq eq (PatternF x) (PatternF x') = eqScopes eq x x' + where + eqScopes :: (a -> b -> Bool) -> Scope (PatternFF a) -> Scope (PatternFF b) -> Bool + eqScopes eq' = liftScopeEq (liftABTEq $ liftEq2 eq' (eqScopes eq')) instance Eq a => Eq1 (PatternFF a) where - eq1 (ConPat c ps) (ConPat c' ps') = - c == c' && ps == ps' - eq1 (AssertionPat m) (AssertionPat m') = + liftEq eq (ConPat c ps) (ConPat c' ps') = + c == c' && liftEq eq ps ps' + liftEq eq (AssertionPat m) (AssertionPat m') = m == m' - eq1 _ _ = False \ No newline at end of file + liftEq _ _ _ = False + +instance Eq2 PatternFF where + liftEq2 eq eq' (ConPat c ps) (ConPat c' ps') = + c == c' && liftEq eq' ps ps' + liftEq2 eq eq' (AssertionPat m) (AssertionPat m') = + eq m m' + liftEq2 _ _ _ _ = + False diff --git a/src/Dependent/Monadic/TypeChecking.hs b/src/Dependent/Monadic/TypeChecking.hs index f9ec010..ab6781e 100644 --- a/src/Dependent/Monadic/TypeChecking.hs +++ b/src/Dependent/Monadic/TypeChecking.hs @@ -140,7 +140,7 @@ infer (Var (Bound _ _)) = error "A bound variable should never be the subject of type inference." infer (Var (Free x)) = typeInContext x -infer (Var (Meta _)) = +infer (Var (Meta _ _)) = error "Meta variables should not exist in this type checker." infer (In (Defined x)) = typeInDefinitions x @@ -309,7 +309,7 @@ checkPattern (Var (Free x)) (NormalTerm t) = , Var (Free x) , [] ) -checkPattern (Var (Meta _)) _ = +checkPattern (Var (Meta _ _)) _ = error "Metavariables should not occur in this type checker." checkPattern (In (ConPat _ _)) (NormalTerm (In Type)) = throwError "Cannot pattern match on a type." diff --git a/src/Dependent/Unification/TypeChecking.hs b/src/Dependent/Unification/TypeChecking.hs index 73ab0dc..20da8cf 100644 --- a/src/Dependent/Unification/TypeChecking.hs +++ b/src/Dependent/Unification/TypeChecking.hs @@ -163,7 +163,7 @@ inferify (Var (Free x)) = return t inferify (Var (Bound _ _)) = error "Bound type variables should not be the subject of type checking." -inferify (Var (Meta x)) = +inferify (Var (Meta _ x)) = throwError $ "The metavariable " ++ show x ++ " appears in checkable code, when it should not." inferify (In (Defined x)) = @@ -318,15 +318,15 @@ checkifyCaseMotive (CaseMotive tele) = checkifyTelescope tele checkifyPattern :: Pattern -> NormalTerm - -> TypeChecker Term + -> TypeChecker (Term, [(Term,Term)]) checkifyPattern (Var (Bound _ _)) _ = error "A bound variable should not be the subject of pattern type checking." checkifyPattern (Var (Free x)) t = do t' <- typeInContext x unifyHelper t (NormalTerm t') -- @t'@ is guaranteed to be normal - return $ Var (Free x) -checkifyPattern (Var (Meta _)) _ = + return (Var (Free x), []) +checkifyPattern (Var (Meta _ _)) _ = error "Metavariables should not be the subject of pattern type checking." checkifyPattern (In (ConPat c ps)) t = do consig@(ConSig (BindingTelescope ascs _)) <- typeInSignature c @@ -336,14 +336,15 @@ checkifyPattern (In (ConPat c ps)) t = $ throwError $ "The constructor " ++ c ++ " expects " ++ show lascs ++ " " ++ (if lascs == 1 then "arg" else "args") ++ " but was given " ++ show lps - (ms,ret) <- checkifyPatterns (map instantiate0 ps) consig + (ms,ret,cs) <- checkifyPatterns (map instantiate0 ps) consig subret <- substitute ret eret <- evaluate subret unifyHelper eret t - return $ conH c ms + return (conH c ms, cs) checkifyPattern (In (AssertionPat m)) t = do checkify m t - return m + mv <- nextElab nextMeta + return (Var $ Meta Constraint mv, [(Var $ Meta Constraint mv, m)]) @@ -365,19 +366,19 @@ checkifyPattern (In (AssertionPat m)) t = checkifyPatterns :: [Pattern] -> ConSig - -> TypeChecker ([Term], Term) + -> TypeChecker ([Term], Term, [(Term, Term)]) checkifyPatterns ps0 (ConSig (BindingTelescope ascs bsc)) = - do ms <- go [] ps0 ascs - return (ms, instantiate bsc ms) + do (ms, cs) <- go [] ps0 ascs + return (ms, instantiate bsc ms, cs) where - go :: [Term] -> [Pattern] -> [Scope TermF] -> TypeChecker [Term] - go _ [] [] = return [] + go :: [Term] -> [Pattern] -> [Scope TermF] -> TypeChecker ([Term],[(Term, Term)]) + go _ [] [] = return ([], []) go acc (p:ps) (sc:scs) = do subt <- substitute (instantiate sc acc) et <- evaluate subt - m <- checkifyPattern p et - ms <- go (acc ++ [m]) ps scs - return $ m:ms + (m, cs) <- checkifyPattern p et + (ms, cs') <- go (acc ++ [m]) ps scs + return (m:ms, cs ++ cs') go _ _ _ = error $ "The auxiliary function 'go' in 'checkPatterns' should always" ++ " have equal number of args for its patterns and scopes. This" @@ -404,21 +405,34 @@ checkifyPatternsCaseMotive :: [Pattern] -> CaseMotive -> TypeChecker Term checkifyPatternsCaseMotive ps0 (CaseMotive (BindingTelescope ascs bsc)) = - do ms <- go [] ps0 ascs + do (ms, cs) <- go [] ps0 ascs + forM_ cs (\(l,r) -> do + subl <- substitute l + el <- evaluate subl + subr <- substitute r + er <- evaluate subr + s <- getElab substitution + unifyHelper el er + s' <- getElab substitution + when (length s /= length s') $ + throwError $ "Solving the constraint " + ++ pretty (normTerm el) ++ " == " + ++ pretty (normTerm er) ++ " produced new metavar resolution" + ) return $ instantiate bsc ms where go :: [Term] -> [Pattern] -> [Scope TermF] - -> TypeChecker [Term] + -> TypeChecker ([Term], [(Term, Term)]) go _ [] [] = - return [] + return ([], []) go acc (p:ps) (sc:scs) = do subt <- substitute (instantiate sc acc) et <- evaluate subt - m <- checkifyPattern p et - ms <- go (acc ++ [m]) ps scs - return $ m:ms + (m,cs) <- checkifyPattern p et + (ms,cs') <- go (acc ++ [m]) ps scs + return (m:ms, cs ++ cs') go _ _ _ = error $ "The auxiliary function 'go' in 'checkPatternsCaseMotive'" ++ " should always have equal number of args for its patterns and" @@ -451,7 +465,7 @@ checkifyClause (Clause pscs sc) mot@(CaseMotive (BindingTelescope ascs _)) = xs2 = map (Var . Free) ns ctx' <- forM ns $ \n -> do m <- nextElab nextMeta - return (n, Var (Meta m)) + return (n, Var (Meta Exist m)) extendElab context ctx' $ do ret <- checkifyPatternsCaseMotive (map (\psc -> patternInstantiate psc xs1 xs2) diff --git a/src/Dependent/Unification/Unification.hs b/src/Dependent/Unification/Unification.hs index e647a4a..147607d 100644 --- a/src/Dependent/Unification/Unification.hs +++ b/src/Dependent/Unification/Unification.hs @@ -34,31 +34,31 @@ import Control.Monad.Except -- | Equating terms by trivial structural equations. instance MonadUnify TermF Elaborator where - equate (Defined n1) (Defined n2) = + equate _ (Defined n1) (Defined n2) = if n1 == n2 then return [] else throwError $ "Mismatching names " ++ n1 ++ " and " ++ n2 - equate (Ann m1 t1) (Ann m2 t2) = - return [ Equation (instantiate0 m1) (instantiate0 m2) - , Equation (instantiate0 t1) (instantiate0 t2) + equate f (Ann m1 t1) (Ann m2 t2) = + return [ Equation f (instantiate0 m1) (instantiate0 m2) + , Equation f (instantiate0 t1) (instantiate0 t2) ] - equate Type Type = + equate _ Type Type = return [] - equate (Fun a1 sc1) (Fun a2 sc2) = + equate f (Fun a1 sc1) (Fun a2 sc2) = do ns <- freshRelTo (names sc1) context let xs = map (Var . Free) ns - return [ Equation (instantiate0 a1) (instantiate0 a2) - , Equation (instantiate sc1 xs) (instantiate sc2 xs) + return [ Equation f (instantiate0 a1) (instantiate0 a2) + , Equation f (instantiate sc1 xs) (instantiate sc2 xs) ] - equate (Lam sc1) (Lam sc2) = + equate f (Lam sc1) (Lam sc2) = do ns <- freshRelTo (names sc1) context let xs = map (Var . Free) ns - return [ Equation (instantiate sc1 xs) (instantiate sc2 xs) ] - equate (App f1 a1) (App f2 a2) = - return [ Equation (instantiate0 f1) (instantiate0 f2) - , Equation (instantiate0 a1) (instantiate0 a2) + return [ Equation f (instantiate sc1 xs) (instantiate sc2 xs) ] + equate _ (App f1 a1) (App f2 a2) = + return [ Equation False (instantiate0 f1) (instantiate0 f2) + , Equation False (instantiate0 a1) (instantiate0 a2) ] - equate (Con c1 as1) (Con c2 as2) = + equate f (Con c1 as1) (Con c2 as2) = do unless (c1 == c2) $ throwError $ "Mismatching constructors " ++ c1 ++ " and " ++ c2 @@ -67,10 +67,10 @@ instance MonadUnify TermF Elaborator where ++ pretty (In (Con c1 as1)) ++ " and " ++ pretty (In (Con c2 as1)) return $ zipWith - Equation + (Equation f) (map instantiate0 as1) (map instantiate0 as2) - equate (Case as1 mot1 cs1) (Case as2 mot2 cs2) = + equate _ (Case as1 mot1 cs1) (Case as2 mot2 cs2) = do unless (length as1 == length as2) $ throwError $ "Mismatching number of case arguments in " ++ pretty (In (Case as1 mot1 cs1)) ++ " and " @@ -80,13 +80,13 @@ instance MonadUnify TermF Elaborator where ++ pretty (In (Case as1 mot1 cs1)) ++ " and " ++ pretty (In (Case as2 mot2 cs2)) let argEqs = zipWith - Equation + (Equation False) (map instantiate0 as1) (map instantiate0 as2) motEqs <- equateCaseMotive mot1 mot2 clauseEqs <- fmap concat $ zipWithM equateClause cs1 cs2 return $ argEqs ++ motEqs ++ clauseEqs - equate l r = + equate _ l r = throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r) @@ -104,7 +104,7 @@ equateCaseMotive mot1@(CaseMotive tele1) mot2@(CaseMotive tele2) = unless (length as1 == length as2) $ throwError $ "Motives not equal: " ++ pretty mot1 ++ " and " ++ pretty mot2 - return $ zipWith Equation as1 as2 ++ [ Equation b1 b2 ] + return $ zipWith (Equation False) as1 as2 ++ [ Equation False b1 b2 ] @@ -129,5 +129,5 @@ equateClause (Clause pscs1 sc1) (Clause pscs2 sc2) = Nothing -> throwError "Patterns are not equal." Just pEqss -> - return $ [ Equation a1 a2 | (a1,a2) <- concat pEqss ] - ++ [ Equation b1 b2 ] \ No newline at end of file + return $ [ Equation False a1 a2 | (a1,a2) <- concat pEqss ] + ++ [ Equation False b1 b2 ] diff --git a/src/DependentImplicit/Unification/TypeChecking.hs b/src/DependentImplicit/Unification/TypeChecking.hs index 155664f..65e5300 100644 --- a/src/DependentImplicit/Unification/TypeChecking.hs +++ b/src/DependentImplicit/Unification/TypeChecking.hs @@ -194,7 +194,7 @@ inferify (Var (Free x)) = return (ElaboratedTerm (Var (Free x)), t) inferify (Var (Bound _ _)) = error "Bound type variables should not be the subject of type checking." -inferify (Var (Meta x)) = +inferify (Var (Meta _ x)) = throwError $ "The metavariable " ++ show x ++ " appears in checkable code, when it should not." inferify (In (Defined x)) = @@ -305,8 +305,8 @@ inferifyApplication f (In (Fun Expl _ _)) Impl m = ++ pretty (appH Impl f m) inferifyApplication f (In (Fun Impl _ sc)) Expl m = do meta <- nextElab nextMeta - let f' = appH Impl f (Var (Meta meta)) - t' = instantiate sc [Var (Meta meta)] + let f' = appH Impl f (Var (Meta Exist meta)) + t' = instantiate sc [Var (Meta Exist meta)] inferifyApplication f' t' Expl m inferifyApplication f _ _ _ = throwError $ "Cannot apply non-function: " ++ pretty f @@ -363,7 +363,7 @@ inferifyConArgs ascs0 bsc0 ms0 = go [] ascs0 bsc0 ms0 go (acc ++ [(Impl,m')]) ascs bsc ms go acc ((Impl,_):ascs) bsc ms = do meta <- nextElab nextMeta - go (acc ++ [(Impl,Var (Meta meta))]) ascs bsc ms + go (acc ++ [(Impl,Var (Meta Exist meta))]) ascs bsc ms go _ _ _ _ = throwError "Cannot match signature." @@ -576,7 +576,7 @@ checkifyConArgs ascs0 bsc ms0 t = return acc accArgsToCheck acc ((Expl,asc):ascs) ((Expl,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Expl, Just m, x, instantiate asc xs) accArgsToCheck @@ -585,7 +585,7 @@ checkifyConArgs ascs0 bsc ms0 t = ms accArgsToCheck acc ((Impl,asc):ascs) ((Impl,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Just m, x, instantiate asc xs) accArgsToCheck @@ -594,7 +594,7 @@ checkifyConArgs ascs0 bsc ms0 t = ms accArgsToCheck acc ((Impl,asc):ascs) ms = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Nothing, x, instantiate asc xs) accArgsToCheck @@ -607,12 +607,12 @@ checkifyConArgs ascs0 bsc ms0 t = swapMetas :: [(Plicity,Term)] -> TypeChecker ([(Term,Term)], [(Plicity,Term)]) swapMetas [] = return ([],[]) - swapMetas ((plic, Var (Meta meta)):ms) = + swapMetas ((plic, Var (Meta Exist meta)):ms) = do (eqs,ms') <- swapMetas ms - return (eqs, (plic,Var (Meta meta)):ms') + return (eqs, (plic,Var (Meta Exist meta)):ms') swapMetas ((plic,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) (eqs,ms') <- swapMetas ms return ((x,m):eqs, (plic,x):ms') @@ -668,7 +668,7 @@ checkifyCaseMotive (CaseMotive tele) = checkifyPattern :: Pattern -> NormalTerm - -> TypeChecker (Pattern,ElaboratedTerm) + -> TypeChecker (Pattern,ElaboratedTerm,[(Term,Term)]) checkifyPattern (Var (Bound _ _)) _ = error "A bound variable should not be the subject of pattern type checking." checkifyPattern (Var (Free x)) t = @@ -676,14 +676,15 @@ checkifyPattern (Var (Free x)) t = unifyHelper t (NormalTerm t') -- @t'@ is guaranteed to be normal return ( Var (Free x) , ElaboratedTerm (Var (Free x)) + , [] ) -checkifyPattern (Var (Meta _)) _ = +checkifyPattern (Var (Meta _ _)) _ = error "Metavariables should not be the subject of pattern type checking." checkifyPattern (In (ConPat _ _)) (NormalTerm (In Type)) = throwError "Cannot pattern match on a type." checkifyPattern (In (ConPat c ps)) (NormalTerm t) = do ConSig plics (BindingTelescope ascs bsc) <- typeInSignature c - (ps',elms') <- + (ps',elms',cs) <- checkifyPatterns (zip plics ascs) bsc @@ -692,17 +693,21 @@ checkifyPattern (In (ConPat c ps)) (NormalTerm t) = let ms' = [ (plic,m') | (plic, ElaboratedTerm m') <- elms' ] return ( conPatH c ps' , ElaboratedTerm (conH c ms') + , cs ) checkifyPattern (In (AssertionPat m)) t = do ElaboratedTerm m' <- checkify m t + mv <- nextElab nextMeta return ( In (AssertionPat m') - , ElaboratedTerm m' + , ElaboratedTerm (Var $ Meta Constraint mv) + , [(Var $ Meta Constraint mv, m')] ) checkifyPattern (In MakeMeta) _ = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) return ( In (AssertionPat x) , ElaboratedTerm x + , [] ) @@ -741,6 +746,7 @@ checkifyPatterns :: [(Plicity,Scope TermF)] -> Term -> TypeChecker ( [(Plicity,Pattern)] , [(Plicity,ElaboratedTerm)] + , [(Term,Term)] ) checkifyPatterns ascs0 bsc ps0 t = do argsToCheck <- accArgsToCheck [] ascs0 ps0 @@ -754,33 +760,36 @@ checkifyPatterns ascs0 bsc ps0 t = return (eqs,ret') ret' -> return ([],ret') unifyHelper (NormalTerm ret') (NormalTerm t) - psms' <- forM argsToCheck $ \(plic,p0,mToElabInto,a) -> + (ps',ms',cs) <- unzip3 <$> forM argsToCheck (\(plic,p0,mToElabInto,a) -> case p0 of Nothing -> do subMToElabInto <- substitute mToElabInto em' <- evaluate subMToElabInto return ( (plic, In (AssertionPat (normTerm em'))) , (plic, ElaboratedTerm (normTerm em')) + , [] ) Just p -> do subMToElabInto <- substitute mToElabInto eMToElabInto <- evaluate subMToElabInto suba <- substitute a ea <- evaluate suba - (p',ElaboratedTerm m') <- checkifyPattern p ea + (p',ElaboratedTerm m',cs) <- checkifyPattern p ea subm' <- substitute m' em' <- evaluate subm' unifyHelper eMToElabInto em' return ( (plic, p') , (plic, ElaboratedTerm (normTerm em')) + , cs ) + ) forM_ eqs $ \(l,r) -> do subl <- substitute l el <- evaluate subl subr <- substitute r er <- evaluate subr unifyHelper el er - return $ unzip psms' + return (ps',ms',concat cs) where accArgsToCheck :: [(Plicity,Maybe Pattern,Term,Term)] -> [(Plicity,Scope TermF)] @@ -790,7 +799,7 @@ checkifyPatterns ascs0 bsc ps0 t = return acc accArgsToCheck acc ((Expl,asc):ascs) ((Expl,p):ps) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Expl, Just p, x, instantiate asc xs) accArgsToCheck @@ -799,7 +808,7 @@ checkifyPatterns ascs0 bsc ps0 t = ps accArgsToCheck acc ((Impl,asc):ascs) ((Impl,p):ps) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Just p, x, instantiate asc xs) accArgsToCheck @@ -808,7 +817,7 @@ checkifyPatterns ascs0 bsc ps0 t = ps accArgsToCheck acc ((Impl,asc):ascs) ps = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Nothing, x, instantiate asc xs) accArgsToCheck @@ -821,12 +830,12 @@ checkifyPatterns ascs0 bsc ps0 t = swapMetas :: [(Plicity,Term)] -> TypeChecker ([(Term,Term)], [(Plicity,Term)]) swapMetas [] = return ([],[]) - swapMetas ((plic, Var (Meta meta)):ms) = + swapMetas ((plic, Var (Meta Exist meta)):ms) = do (eqs,ms') <- swapMetas ms - return (eqs, (plic,Var (Meta meta)):ms') + return (eqs, (plic,Var (Meta Exist meta)):ms') swapMetas ((plic,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) (eqs,ms') <- swapMetas ms return ((x,m):eqs, (plic,x):ms') @@ -852,21 +861,34 @@ checkifyPatternsCaseMotive :: [Pattern] -> CaseMotive -> TypeChecker ([Pattern], ElaboratedTerm) checkifyPatternsCaseMotive ps0 (CaseMotive (BindingTelescope ascs bsc)) = - do (ps',ms') <- go [] ps0 ascs + do (ps',ms',cs) <- go [] ps0 ascs + forM_ cs (\(l,r) -> do + subl <- substitute l + el <- evaluate subl + subr <- substitute r + er <- evaluate subr + s <- getElab substitution + unifyHelper el er + s' <- getElab substitution + when (length s /= length s') $ + throwError $ "Solving the constraint " + ++ pretty (normTerm el) ++ " == " + ++ pretty (normTerm er) ++ " produced new metavar resolution" + ) return (ps', ElaboratedTerm (instantiate bsc ms')) where go :: [Term] -> [Pattern] -> [Scope TermF] - -> TypeChecker ([Pattern],[Term]) + -> TypeChecker ([Pattern],[Term],[(Term,Term)]) go _ [] [] = - return ([],[]) + return ([],[],[]) go acc (p:ps) (sc:scs) = do subt <- substitute (instantiate sc acc) et <- evaluate subt - (p',ElaboratedTerm m') <- checkifyPattern p et - (ps',ms') <- go (acc ++ [m']) ps scs - return (p':ps', m':ms') + (p',ElaboratedTerm m',cs) <- checkifyPattern p et + (ps',ms',cs') <- go (acc ++ [m']) ps scs + return (p':ps', m':ms', cs ++ cs') go _ _ _ = error $ "The auxiliary function 'go' in 'checkPatternsCaseMotive'" ++ " should always have equal number of args for its patterns and" @@ -899,7 +921,7 @@ checkifyClause (Clause pscs sc) mot@(CaseMotive (BindingTelescope ascs _)) = xs2 = map (Var . Free) ns ctx' <- forM ns $ \n -> do m <- nextElab nextMeta - return (n, Var (Meta m)) + return (n, Var (Meta Exist m)) extendElab context ctx' $ do (ps',ElaboratedTerm ret) <- checkifyPatternsCaseMotive diff --git a/src/DependentImplicit/Unification/Unification.hs b/src/DependentImplicit/Unification/Unification.hs index 0d1255f..6e15dc2 100644 --- a/src/DependentImplicit/Unification/Unification.hs +++ b/src/DependentImplicit/Unification/Unification.hs @@ -34,43 +34,43 @@ import Control.Monad.Except -- | Equating terms by trivial structural equations. instance MonadUnify TermF Elaborator where - equate (Defined n1) (Defined n2) = + equate _ (Defined n1) (Defined n2) = if n1 == n2 then return [] else throwError $ "Mismatching names " ++ n1 ++ " and " ++ n2 - equate (Ann m1 t1) (Ann m2 t2) = - return [ Equation (instantiate0 m1) (instantiate0 m2) - , Equation (instantiate0 t1) (instantiate0 t2) + equate f (Ann m1 t1) (Ann m2 t2) = + return [ Equation f (instantiate0 m1) (instantiate0 m2) + , Equation f (instantiate0 t1) (instantiate0 t2) ] - equate Type Type = + equate _ Type Type = return [] - equate (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) = + equate f (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) = do unless (plic1 == plic2) $ throwError $ "Mismatching plicities when unifying " ++ pretty (In (Fun plic1 a1 sc1)) ++ " with " ++ pretty (In (Fun plic2 a2 sc2)) ns <- freshRelTo (names sc1) context let xs = map (Var . Free) ns - return [ Equation (instantiate0 a1) (instantiate0 a2) - , Equation (instantiate sc1 xs) (instantiate sc2 xs) + return [ Equation f (instantiate0 a1) (instantiate0 a2) + , Equation f (instantiate sc1 xs) (instantiate sc2 xs) ] - equate (Lam plic1 sc1) (Lam plic2 sc2) = + equate f (Lam plic1 sc1) (Lam plic2 sc2) = do unless (plic1 == plic2) $ throwError $ "Mismatching plicities when unifying " ++ pretty (In (Lam plic1 sc1)) ++ " with " ++ pretty (In (Lam plic2 sc2)) ns <- freshRelTo (names sc1) context let xs = map (Var . Free) ns - return [ Equation (instantiate sc1 xs) (instantiate sc2 xs) ] - equate (App plic1 f1 a1) (App plic2 f2 a2) = + return [ Equation f (instantiate sc1 xs) (instantiate sc2 xs) ] + equate _ (App plic1 f1 a1) (App plic2 f2 a2) = do unless (plic1 == plic2) $ throwError $ "Mismatching plicities when unifying " ++ pretty (In (App plic1 f1 a1)) ++ " with " ++ pretty (In (App plic2 f2 a2)) - return [ Equation (instantiate0 f1) (instantiate0 f2) - , Equation (instantiate0 a1) (instantiate0 a2) + return [ Equation False (instantiate0 f1) (instantiate0 f2) + , Equation False (instantiate0 a1) (instantiate0 a2) ] - equate (Con c1 as1) (Con c2 as2) = + equate f (Con c1 as1) (Con c2 as2) = do unless (c1 == c2) $ throwError $ "Mismatching constructors " ++ c1 ++ " and " ++ c2 @@ -85,10 +85,10 @@ instance MonadUnify TermF Elaborator where ++ pretty (In (Con c1 as1)) ++ " with " ++ pretty (In (Con c2 as2)) return $ zipWith - Equation + (Equation f) (map instantiate0 as1') (map instantiate0 as2') - equate (Case as1 mot1 cs1) (Case as2 mot2 cs2) = + equate _ (Case as1 mot1 cs1) (Case as2 mot2 cs2) = do unless (length as1 == length as2) $ throwError $ "Mismatching number of case arguments in " ++ pretty (In (Case as1 mot1 cs1)) ++ " and " @@ -98,13 +98,13 @@ instance MonadUnify TermF Elaborator where ++ pretty (In (Case as1 mot1 cs1)) ++ " and " ++ pretty (In (Case as2 mot2 cs2)) let argEqs = zipWith - Equation + (Equation False) (map instantiate0 as1) (map instantiate0 as2) motEqs <- equateCaseMotive mot1 mot2 clauseEqs <- fmap concat $ zipWithM equateClause cs1 cs2 return $ argEqs ++ motEqs ++ clauseEqs - equate l r = + equate _ l r = throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r) @@ -122,7 +122,7 @@ equateCaseMotive mot1@(CaseMotive tele1) mot2@(CaseMotive tele2) = unless (length as1 == length as2) $ throwError $ "Motives not equal: " ++ pretty mot1 ++ " and " ++ pretty mot2 - return $ zipWith Equation as1 as2 ++ [ Equation b1 b2 ] + return $ zipWith (Equation False) as1 as2 ++ [ Equation False b1 b2 ] @@ -147,5 +147,5 @@ equateClause (Clause pscs1 sc1) (Clause pscs2 sc2) = Nothing -> throwError "Patterns are not equal." Just pEqss -> - return $ [ Equation a1 a2 | (a1,a2) <- concat pEqss ] - ++ [ Equation b1 b2 ] \ No newline at end of file + return $ [ Equation False a1 a2 | (a1,a2) <- concat pEqss ] + ++ [ Equation False b1 b2 ] diff --git a/src/Modular/Unification/TypeChecking.hs b/src/Modular/Unification/TypeChecking.hs index f36d86e..6b4854d 100644 --- a/src/Modular/Unification/TypeChecking.hs +++ b/src/Modular/Unification/TypeChecking.hs @@ -232,7 +232,7 @@ inferify (Var (Free x)) = return (ElaboratedTerm (Var (Free x)), t) inferify (Var (Bound _ _)) = error "Bound type variables should not be the subject of type checking." -inferify (Var (Meta x)) = +inferify (Var (Meta _ x)) = throwError $ "The metavariable " ++ show x ++ " appears in checkable code, when it should not." inferify (In (Defined x)) = @@ -343,8 +343,8 @@ inferifyApplication f (In (Fun Expl _ _)) Impl m = ++ pretty (appH Impl f m) inferifyApplication f (In (Fun Impl _ sc)) Expl m = do meta <- nextElab nextMeta - let f' = appH Impl f (Var (Meta meta)) - t' = instantiate sc [Var (Meta meta)] + let f' = appH Impl f (Var (Meta Exist meta)) + t' = instantiate sc [Var (Meta Exist meta)] inferifyApplication f' t' Expl m inferifyApplication f _ _ _ = throwError $ "Cannot apply non-function: " ++ pretty f @@ -401,7 +401,7 @@ inferifyConArgs ascs0 bsc0 ms0 = go [] ascs0 bsc0 ms0 go (acc ++ [(Impl,m')]) ascs bsc ms go acc ((Impl,_):ascs) bsc ms = do meta <- nextElab nextMeta - go (acc ++ [(Impl,Var (Meta meta))]) ascs bsc ms + go (acc ++ [(Impl,Var (Meta Exist meta))]) ascs bsc ms go _ _ _ _ = throwError "Cannot match signature." @@ -614,7 +614,7 @@ checkifyConArgs ascs0 bsc ms0 t = return acc accArgsToCheck acc ((Expl,asc):ascs) ((Expl,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Expl, Just m, x, instantiate asc xs) accArgsToCheck @@ -623,7 +623,7 @@ checkifyConArgs ascs0 bsc ms0 t = ms accArgsToCheck acc ((Impl,asc):ascs) ((Impl,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Just m, x, instantiate asc xs) accArgsToCheck @@ -632,7 +632,7 @@ checkifyConArgs ascs0 bsc ms0 t = ms accArgsToCheck acc ((Impl,asc):ascs) ms = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Nothing, x, instantiate asc xs) accArgsToCheck @@ -645,12 +645,12 @@ checkifyConArgs ascs0 bsc ms0 t = swapMetas :: [(Plicity,Term)] -> TypeChecker ([(Term,Term)], [(Plicity,Term)]) swapMetas [] = return ([],[]) - swapMetas ((plic, Var (Meta meta)):ms) = + swapMetas ((plic, Var (Meta Exist meta)):ms) = do (eqs,ms') <- swapMetas ms - return (eqs, (plic,Var (Meta meta)):ms') + return (eqs, (plic,Var (Meta Exist meta)):ms') swapMetas ((plic,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) (eqs,ms') <- swapMetas ms return ((x,m):eqs, (plic,x):ms') @@ -706,7 +706,7 @@ checkifyCaseMotive (CaseMotive tele) = checkifyPattern :: Pattern -> NormalTerm - -> TypeChecker (Pattern,ElaboratedTerm) + -> TypeChecker (Pattern,ElaboratedTerm,[(Term,Term)]) checkifyPattern (Var (Bound _ _)) _ = error "A bound variable should not be the subject of pattern type checking." checkifyPattern (Var (Free x)) t = @@ -714,12 +714,13 @@ checkifyPattern (Var (Free x)) t = unifyHelper t (NormalTerm t') -- @t'@ is guaranteed to be normal return ( Var (Free x) , ElaboratedTerm (Var (Free x)) + , [] ) -checkifyPattern (Var (Meta _)) _ = +checkifyPattern (Var (Meta _ _)) _ = error "Metavariables should not be the subject of pattern type checking." checkifyPattern (In (ConPat c ps)) (NormalTerm t) = do (ec,ConSig plics (BindingTelescope ascs bsc)) <- typeInSignature c - (ps',elms') <- + (ps',elms',cs) <- checkifyPatterns (zip plics ascs) bsc @@ -728,17 +729,21 @@ checkifyPattern (In (ConPat c ps)) (NormalTerm t) = let ms' = [ (plic,m') | (plic, ElaboratedTerm m') <- elms' ] return ( conPatH ec ps' , ElaboratedTerm (conH ec ms') + , cs ) checkifyPattern (In (AssertionPat m)) t = do ElaboratedTerm m' <- checkify m t + mv <- nextElab nextMeta return ( In (AssertionPat m') - , ElaboratedTerm m' + , ElaboratedTerm (Var $ Meta Constraint mv) + , [(Var $ Meta Constraint mv, m')] ) checkifyPattern (In MakeMeta) _ = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) return ( In (AssertionPat x) , ElaboratedTerm x + , [] ) @@ -777,6 +782,7 @@ checkifyPatterns :: [(Plicity,Scope TermF)] -> Term -> TypeChecker ( [(Plicity,Pattern)] , [(Plicity,ElaboratedTerm)] + , [(Term,Term)] ) checkifyPatterns ascs0 bsc ps0 t = do argsToCheck <- accArgsToCheck [] ascs0 ps0 @@ -790,33 +796,36 @@ checkifyPatterns ascs0 bsc ps0 t = return (eqs,ret') ret' -> return ([],ret') unifyHelper (NormalTerm ret') (NormalTerm t) - psms' <- forM argsToCheck $ \(plic,p0,mToElabInto,a) -> + (ps',ms',cs) <- unzip3 <$> forM argsToCheck (\(plic,p0,mToElabInto,a) -> case p0 of Nothing -> do subMToElabInto <- substitute mToElabInto em' <- evaluate subMToElabInto return ( (plic, In (AssertionPat (normTerm em'))) , (plic, ElaboratedTerm (normTerm em')) + , [] ) Just p -> do subMToElabInto <- substitute mToElabInto eMToElabInto <- evaluate subMToElabInto suba <- substitute a ea <- evaluate suba - (p',ElaboratedTerm m') <- checkifyPattern p ea + (p',ElaboratedTerm m',cs) <- checkifyPattern p ea subm' <- substitute m' em' <- evaluate subm' unifyHelper eMToElabInto em' return ( (plic, p') , (plic, ElaboratedTerm (normTerm em')) + , cs ) + ) forM_ eqs $ \(l,r) -> do subl <- substitute l el <- evaluate subl subr <- substitute r er <- evaluate subr unifyHelper el er - return $ unzip psms' + return (ps',ms',concat cs) where accArgsToCheck :: [(Plicity,Maybe Pattern,Term,Term)] -> [(Plicity,Scope TermF)] @@ -826,7 +835,7 @@ checkifyPatterns ascs0 bsc ps0 t = return acc accArgsToCheck acc ((Expl,asc):ascs) ((Expl,p):ps) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Expl, Just p, x, instantiate asc xs) accArgsToCheck @@ -835,7 +844,7 @@ checkifyPatterns ascs0 bsc ps0 t = ps accArgsToCheck acc ((Impl,asc):ascs) ((Impl,p):ps) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Just p, x, instantiate asc xs) accArgsToCheck @@ -844,7 +853,7 @@ checkifyPatterns ascs0 bsc ps0 t = ps accArgsToCheck acc ((Impl,asc):ascs) ps = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Nothing, x, instantiate asc xs) accArgsToCheck @@ -857,12 +866,12 @@ checkifyPatterns ascs0 bsc ps0 t = swapMetas :: [(Plicity,Term)] -> TypeChecker ([(Term,Term)], [(Plicity,Term)]) swapMetas [] = return ([],[]) - swapMetas ((plic, Var (Meta meta)):ms) = + swapMetas ((plic, Var (Meta Exist meta)):ms) = do (eqs,ms') <- swapMetas ms - return (eqs, (plic,Var (Meta meta)):ms') + return (eqs, (plic,Var (Meta Exist meta)):ms') swapMetas ((plic,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) (eqs,ms') <- swapMetas ms return ((x,m):eqs, (plic,x):ms') @@ -888,21 +897,34 @@ checkifyPatternsCaseMotive :: [Pattern] -> CaseMotive -> TypeChecker ([Pattern], ElaboratedTerm) checkifyPatternsCaseMotive ps0 (CaseMotive (BindingTelescope ascs bsc)) = - do (ps',ms') <- go [] ps0 ascs + do (ps',ms',cs) <- go [] ps0 ascs + forM_ cs (\(l,r) -> do + subl <- substitute l + el <- evaluate subl + subr <- substitute r + er <- evaluate subr + s <- getElab substitution + unifyHelper el er + s' <- getElab substitution + when (length s /= length s') $ + throwError $ "Solving the constraint " + ++ pretty (normTerm el) ++ " == " + ++ pretty (normTerm er) ++ " produced new metavar resolution" + ) return (ps', ElaboratedTerm (instantiate bsc ms')) where go :: [Term] -> [Pattern] -> [Scope TermF] - -> TypeChecker ([Pattern],[Term]) + -> TypeChecker ([Pattern],[Term],[(Term,Term)]) go _ [] [] = - return ([],[]) + return ([],[],[]) go acc (p:ps) (sc:scs) = do subt <- substitute (instantiate sc acc) et <- evaluate subt - (p',ElaboratedTerm m') <- checkifyPattern p et - (ps',ms') <- go (acc ++ [m']) ps scs - return (p':ps', m':ms') + (p',ElaboratedTerm m',cs) <- checkifyPattern p et + (ps',ms',cs') <- go (acc ++ [m']) ps scs + return (p':ps', m':ms', cs ++ cs') go _ _ _ = error $ "The auxiliary function 'go' in 'checkPatternsCaseMotive'" ++ " should always have equal number of args for its patterns and" @@ -935,7 +957,7 @@ checkifyClause (Clause pscs sc) mot@(CaseMotive (BindingTelescope ascs _)) = xs2 = map (Var . Free) ns ctx' <- forM ns $ \n -> do m <- nextElab nextMeta - return (n, Var (Meta m)) + return (n, Var (Meta Exist m)) extendElab context ctx' $ do (ps',ElaboratedTerm ret) <- checkifyPatternsCaseMotive diff --git a/src/Modular/Unification/Unification.hs b/src/Modular/Unification/Unification.hs index 2847aa8..e675235 100644 --- a/src/Modular/Unification/Unification.hs +++ b/src/Modular/Unification/Unification.hs @@ -35,44 +35,44 @@ import Control.Monad.Except -- | Equating terms by trivial structural equations. instance MonadUnify TermF Elaborator where - equate (Defined n1) (Defined n2) = + equate _ (Defined n1) (Defined n2) = if n1 == n2 then return [] else throwError $ "Mismatching names " ++ showName n1 ++ " and " ++ showName n2 - equate (Ann m1 t1) (Ann m2 t2) = - return [ Equation (instantiate0 m1) (instantiate0 m2) - , Equation (instantiate0 t1) (instantiate0 t2) + equate f (Ann m1 t1) (Ann m2 t2) = + return [ Equation f (instantiate0 m1) (instantiate0 m2) + , Equation f (instantiate0 t1) (instantiate0 t2) ] - equate Type Type = + equate _ Type Type = return [] - equate (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) = + equate f (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) = do unless (plic1 == plic2) $ throwError $ "Mismatching plicities when unifying " ++ pretty (In (Fun plic1 a1 sc1)) ++ " with " ++ pretty (In (Fun plic2 a2 sc2)) ns <- freshRelTo (names sc1) context let xs = map (Var . Free) ns - return [ Equation (instantiate0 a1) (instantiate0 a2) - , Equation (instantiate sc1 xs) (instantiate sc2 xs) + return [ Equation f (instantiate0 a1) (instantiate0 a2) + , Equation f (instantiate sc1 xs) (instantiate sc2 xs) ] - equate (Lam plic1 sc1) (Lam plic2 sc2) = + equate f (Lam plic1 sc1) (Lam plic2 sc2) = do unless (plic1 == plic2) $ throwError $ "Mismatching plicities when unifying " ++ pretty (In (Lam plic1 sc1)) ++ " with " ++ pretty (In (Lam plic2 sc2)) ns <- freshRelTo (names sc1) context let xs = map (Var . Free) ns - return [ Equation (instantiate sc1 xs) (instantiate sc2 xs) ] - equate (App plic1 f1 a1) (App plic2 f2 a2) = + return [ Equation f (instantiate sc1 xs) (instantiate sc2 xs) ] + equate _ (App plic1 f1 a1) (App plic2 f2 a2) = do unless (plic1 == plic2) $ throwError $ "Mismatching plicities when unifying " ++ pretty (In (App plic1 f1 a1)) ++ " with " ++ pretty (In (App plic2 f2 a2)) - return [ Equation (instantiate0 f1) (instantiate0 f2) - , Equation (instantiate0 a1) (instantiate0 a2) + return [ Equation False (instantiate0 f1) (instantiate0 f2) + , Equation False (instantiate0 a1) (instantiate0 a2) ] - equate (Con c1 as1) (Con c2 as2) = + equate f (Con c1 as1) (Con c2 as2) = do unless (c1 == c2) $ throwError $ "Mismatching constructors " ++ showName c1 ++ " and " ++ showName c2 @@ -87,10 +87,10 @@ instance MonadUnify TermF Elaborator where ++ pretty (In (Con c1 as1)) ++ " with " ++ pretty (In (Con c2 as2)) return $ zipWith - Equation + (Equation f) (map instantiate0 as1') (map instantiate0 as2') - equate (Case as1 mot1 cs1) (Case as2 mot2 cs2) = + equate _ (Case as1 mot1 cs1) (Case as2 mot2 cs2) = do unless (length as1 == length as2) $ throwError $ "Mismatching number of case arguments in " ++ pretty (In (Case as1 mot1 cs1)) ++ " and " @@ -100,13 +100,13 @@ instance MonadUnify TermF Elaborator where ++ pretty (In (Case as1 mot1 cs1)) ++ " and " ++ pretty (In (Case as2 mot2 cs2)) let argEqs = zipWith - Equation + (Equation False) (map instantiate0 as1) (map instantiate0 as2) motEqs <- equateCaseMotive mot1 mot2 clauseEqs <- fmap concat $ zipWithM equateClause cs1 cs2 return $ argEqs ++ motEqs ++ clauseEqs - equate l r = + equate _ l r = throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r) @@ -124,7 +124,7 @@ equateCaseMotive mot1@(CaseMotive tele1) mot2@(CaseMotive tele2) = unless (length as1 == length as2) $ throwError $ "Motives not equal: " ++ pretty mot1 ++ " and " ++ pretty mot2 - return $ zipWith Equation as1 as2 ++ [ Equation b1 b2 ] + return $ zipWith (Equation False) as1 as2 ++ [ Equation False b1 b2 ] @@ -149,5 +149,5 @@ equateClause (Clause pscs1 sc1) (Clause pscs2 sc2) = Nothing -> throwError "Patterns are not equal." Just pEqss -> - return $ [ Equation a1 a2 | (a1,a2) <- concat pEqss ] - ++ [ Equation b1 b2 ] \ No newline at end of file + return $ [ Equation False a1 a2 | (a1,a2) <- concat pEqss ] + ++ [ Equation False b1 b2 ] diff --git a/src/OpenDefs/Unification/TypeChecking.hs b/src/OpenDefs/Unification/TypeChecking.hs index 00b476b..41ca240 100644 --- a/src/OpenDefs/Unification/TypeChecking.hs +++ b/src/OpenDefs/Unification/TypeChecking.hs @@ -245,7 +245,7 @@ inferify (Var (Free x)) = return (ElaboratedTerm (Var (Free x)), t) inferify (Var (Bound _ _)) = error "Bound type variables should not be the subject of type checking." -inferify (Var (Meta x)) = +inferify (Var (Meta _ x)) = throwError $ "The metavariable " ++ show x ++ " appears in checkable code, when it should not." inferify (In (Defined x)) = @@ -392,8 +392,8 @@ inferifyApplication f (In (Fun Expl _ _)) Impl m = ++ pretty (appH Impl f m) inferifyApplication f (In (Fun Impl _ sc)) Expl m = do meta <- nextElab nextMeta - let f' = appH Impl f (Var (Meta meta)) - t' = instantiate sc [Var (Meta meta)] + let f' = appH Impl f (Var (Meta Exist meta)) + t' = instantiate sc [Var (Meta Exist meta)] inferifyApplication f' t' Expl m inferifyApplication f _ _ _ = throwError $ "Cannot apply non-function: " ++ pretty f @@ -450,7 +450,7 @@ inferifyConArgs ascs0 bsc0 ms0 = go [] ascs0 bsc0 ms0 go (acc ++ [(Impl,m')]) ascs bsc ms go acc ((Impl,_):ascs) bsc ms = do meta <- nextElab nextMeta - go (acc ++ [(Impl,Var (Meta meta))]) ascs bsc ms + go (acc ++ [(Impl,Var (Meta Exist meta))]) ascs bsc ms go _ _ _ _ = throwError "Cannot match signature." @@ -710,7 +710,7 @@ checkifyConArgs ascs0 bsc ms0 t = return acc accArgsToCheck acc ((Expl,asc):ascs) ((Expl,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Expl, Just m, x, instantiate asc xs) accArgsToCheck @@ -719,7 +719,7 @@ checkifyConArgs ascs0 bsc ms0 t = ms accArgsToCheck acc ((Impl,asc):ascs) ((Impl,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Just m, x, instantiate asc xs) accArgsToCheck @@ -728,7 +728,7 @@ checkifyConArgs ascs0 bsc ms0 t = ms accArgsToCheck acc ((Impl,asc):ascs) ms = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Nothing, x, instantiate asc xs) accArgsToCheck @@ -741,12 +741,12 @@ checkifyConArgs ascs0 bsc ms0 t = swapMetas :: [(Plicity,Term)] -> TypeChecker ([(Term,Term)], [(Plicity,Term)]) swapMetas [] = return ([],[]) - swapMetas ((plic, Var (Meta meta)):ms) = + swapMetas ((plic, Var (Meta Exist meta)):ms) = do (eqs,ms') <- swapMetas ms - return (eqs, (plic,Var (Meta meta)):ms') + return (eqs, (plic,Var (Meta Exist meta)):ms') swapMetas ((plic,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) (eqs,ms') <- swapMetas ms return ((x,m):eqs, (plic,x):ms') @@ -802,7 +802,7 @@ checkifyCaseMotive (CaseMotive tele) = checkifyPattern :: Pattern -> NormalTerm - -> TypeChecker (Pattern,ElaboratedTerm) + -> TypeChecker (Pattern,ElaboratedTerm,[(Term,Term)]) checkifyPattern (Var (Bound _ _)) _ = error "A bound variable should not be the subject of pattern type checking." checkifyPattern (Var (Free x)) t = @@ -810,12 +810,13 @@ checkifyPattern (Var (Free x)) t = unifyHelper t (NormalTerm t') -- @t'@ is guaranteed to be normal return ( Var (Free x) , ElaboratedTerm (Var (Free x)) + , [] ) -checkifyPattern (Var (Meta _)) _ = +checkifyPattern (Var (Meta _ _)) _ = error "Metavariables should not be the subject of pattern type checking." checkifyPattern (In (ConPat c ps)) (NormalTerm t) = do (ec,ConSig plics (BindingTelescope ascs bsc)) <- typeInSignature c - (ps',elms') <- + (ps',elms',cs) <- checkifyPatterns (zip plics ascs) bsc @@ -824,17 +825,21 @@ checkifyPattern (In (ConPat c ps)) (NormalTerm t) = let ms' = [ (plic,m') | (plic, ElaboratedTerm m') <- elms' ] return ( conPatH ec ps' , ElaboratedTerm (conH ec ms') + , cs ) checkifyPattern (In (AssertionPat m)) t = do ElaboratedTerm m' <- checkify m t + mv <- nextElab nextMeta return ( In (AssertionPat m') - , ElaboratedTerm m' + , ElaboratedTerm (Var $ Meta Constraint mv) + , [(Var $ Meta Constraint mv, m')] ) checkifyPattern (In MakeMeta) _ = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) return ( In (AssertionPat x) , ElaboratedTerm x + , [] ) @@ -873,6 +878,7 @@ checkifyPatterns :: [(Plicity,Scope TermF)] -> Term -> TypeChecker ( [(Plicity,Pattern)] , [(Plicity,ElaboratedTerm)] + , [(Term,Term)] ) checkifyPatterns ascs0 bsc ps0 t = do argsToCheck <- accArgsToCheck [] ascs0 ps0 @@ -886,33 +892,36 @@ checkifyPatterns ascs0 bsc ps0 t = return (eqs,ret') ret' -> return ([],ret') unifyHelper (NormalTerm ret') (NormalTerm t) - psms' <- forM argsToCheck $ \(plic,p0,mToElabInto,a) -> + (ps',ms',cs) <- unzip3 <$> forM argsToCheck (\(plic,p0,mToElabInto,a) -> case p0 of Nothing -> do subMToElabInto <- substitute mToElabInto em' <- evaluate subMToElabInto return ( (plic, In (AssertionPat (normTerm em'))) , (plic, ElaboratedTerm (normTerm em')) + , [] ) Just p -> do subMToElabInto <- substitute mToElabInto eMToElabInto <- evaluate subMToElabInto suba <- substitute a ea <- evaluate suba - (p',ElaboratedTerm m') <- checkifyPattern p ea + (p',ElaboratedTerm m',cs) <- checkifyPattern p ea subm' <- substitute m' em' <- evaluate subm' unifyHelper eMToElabInto em' return ( (plic, p') , (plic, ElaboratedTerm (normTerm em')) + , cs ) + ) forM_ eqs $ \(l,r) -> do subl <- substitute l el <- evaluate subl subr <- substitute r er <- evaluate subr unifyHelper el er - return $ unzip psms' + return (ps',ms',concat cs) where accArgsToCheck :: [(Plicity,Maybe Pattern,Term,Term)] -> [(Plicity,Scope TermF)] @@ -922,7 +931,7 @@ checkifyPatterns ascs0 bsc ps0 t = return acc accArgsToCheck acc ((Expl,asc):ascs) ((Expl,p):ps) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Expl, Just p, x, instantiate asc xs) accArgsToCheck @@ -931,7 +940,7 @@ checkifyPatterns ascs0 bsc ps0 t = ps accArgsToCheck acc ((Impl,asc):ascs) ((Impl,p):ps) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Just p, x, instantiate asc xs) accArgsToCheck @@ -940,7 +949,7 @@ checkifyPatterns ascs0 bsc ps0 t = ps accArgsToCheck acc ((Impl,asc):ascs) ps = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Nothing, x, instantiate asc xs) accArgsToCheck @@ -953,12 +962,12 @@ checkifyPatterns ascs0 bsc ps0 t = swapMetas :: [(Plicity,Term)] -> TypeChecker ([(Term,Term)], [(Plicity,Term)]) swapMetas [] = return ([],[]) - swapMetas ((plic, Var (Meta meta)):ms) = + swapMetas ((plic, Var (Meta Exist meta)):ms) = do (eqs,ms') <- swapMetas ms - return (eqs, (plic,Var (Meta meta)):ms') + return (eqs, (plic,Var (Meta Exist meta)):ms') swapMetas ((plic,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) (eqs,ms') <- swapMetas ms return ((x,m):eqs, (plic,x):ms') @@ -984,21 +993,34 @@ checkifyPatternsCaseMotive :: [Pattern] -> CaseMotive -> TypeChecker ([Pattern], ElaboratedTerm) checkifyPatternsCaseMotive ps0 (CaseMotive (BindingTelescope ascs bsc)) = - do (ps',ms') <- go [] ps0 ascs + do (ps',ms',cs) <- go [] ps0 ascs + forM_ cs (\(l,r) -> do + subl <- substitute l + el <- evaluate subl + subr <- substitute r + er <- evaluate subr + s <- getElab substitution + unifyHelper el er + s' <- getElab substitution + when (length s /= length s') $ + throwError $ "Solving the constraint " + ++ pretty (normTerm el) ++ " == " + ++ pretty (normTerm er) ++ " produced new metavar resolution" + ) return (ps', ElaboratedTerm (instantiate bsc ms')) where go :: [Term] -> [Pattern] -> [Scope TermF] - -> TypeChecker ([Pattern],[Term]) + -> TypeChecker ([Pattern],[Term],[(Term,Term)]) go _ [] [] = - return ([],[]) + return ([],[],[]) go acc (p:ps) (sc:scs) = do subt <- substitute (instantiate sc acc) et <- evaluate subt - (p',ElaboratedTerm m') <- checkifyPattern p et - (ps',ms') <- go (acc ++ [m']) ps scs - return (p':ps', m':ms') + (p',ElaboratedTerm m',cs) <- checkifyPattern p et + (ps',ms',cs') <- go (acc ++ [m']) ps scs + return (p':ps', m':ms', cs ++ cs') go _ _ _ = error $ "The auxiliary function 'go' in 'checkPatternsCaseMotive'" ++ " should always have equal number of args for its patterns and" @@ -1031,7 +1053,7 @@ checkifyClause (Clause pscs sc) mot@(CaseMotive (BindingTelescope ascs _)) = xs2 = map (Var . Free) ns ctx' <- forM ns $ \n -> do m <- nextElab nextMeta - return (n, Var (Meta m)) + return (n, Var (Meta Exist m)) extendElab context ctx' $ do (ps',ElaboratedTerm ret) <- checkifyPatternsCaseMotive diff --git a/src/OpenDefs/Unification/Unification.hs b/src/OpenDefs/Unification/Unification.hs index b7869ee..c6b905f 100644 --- a/src/OpenDefs/Unification/Unification.hs +++ b/src/OpenDefs/Unification/Unification.hs @@ -35,44 +35,44 @@ import Control.Monad.Except -- | Equating terms by trivial structural equations. instance MonadUnify TermF Elaborator where - equate (Defined n1) (Defined n2) = + equate _ (Defined n1) (Defined n2) = if n1 == n2 then return [] else throwError $ "Mismatching names " ++ showName n1 ++ " and " ++ showName n2 - equate (Ann m1 t1) (Ann m2 t2) = - return [ Equation (instantiate0 m1) (instantiate0 m2) - , Equation (instantiate0 t1) (instantiate0 t2) + equate f (Ann m1 t1) (Ann m2 t2) = + return [ Equation f (instantiate0 m1) (instantiate0 m2) + , Equation f (instantiate0 t1) (instantiate0 t2) ] - equate Type Type = + equate _ Type Type = return [] - equate (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) = + equate f (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) = do unless (plic1 == plic2) $ throwError $ "Mismatching plicities when unifying " ++ pretty (In (Fun plic1 a1 sc1)) ++ " with " ++ pretty (In (Fun plic2 a2 sc2)) ns <- freshRelTo (names sc1) context let xs = map (Var . Free) ns - return [ Equation (instantiate0 a1) (instantiate0 a2) - , Equation (instantiate sc1 xs) (instantiate sc2 xs) + return [ Equation f (instantiate0 a1) (instantiate0 a2) + , Equation f (instantiate sc1 xs) (instantiate sc2 xs) ] - equate (Lam plic1 sc1) (Lam plic2 sc2) = + equate f (Lam plic1 sc1) (Lam plic2 sc2) = do unless (plic1 == plic2) $ throwError $ "Mismatching plicities when unifying " ++ pretty (In (Lam plic1 sc1)) ++ " with " ++ pretty (In (Lam plic2 sc2)) ns <- freshRelTo (names sc1) context let xs = map (Var . Free) ns - return [ Equation (instantiate sc1 xs) (instantiate sc2 xs) ] - equate (App plic1 f1 a1) (App plic2 f2 a2) = + return [ Equation f (instantiate sc1 xs) (instantiate sc2 xs) ] + equate _ (App plic1 f1 a1) (App plic2 f2 a2) = do unless (plic1 == plic2) $ throwError $ "Mismatching plicities when unifying " ++ pretty (In (App plic1 f1 a1)) ++ " with " ++ pretty (In (App plic2 f2 a2)) - return [ Equation (instantiate0 f1) (instantiate0 f2) - , Equation (instantiate0 a1) (instantiate0 a2) + return [ Equation False (instantiate0 f1) (instantiate0 f2) + , Equation False (instantiate0 a1) (instantiate0 a2) ] - equate (Con c1 as1) (Con c2 as2) = + equate f (Con c1 as1) (Con c2 as2) = do unless (c1 == c2) $ throwError $ "Mismatching constructors " ++ showName c1 ++ " and " ++ showName c2 @@ -87,10 +87,10 @@ instance MonadUnify TermF Elaborator where ++ pretty (In (Con c1 as1)) ++ " with " ++ pretty (In (Con c2 as2)) return $ zipWith - Equation + (Equation f) (map instantiate0 as1') (map instantiate0 as2') - equate (Case as1 mot1 cs1) (Case as2 mot2 cs2) = + equate _ (Case as1 mot1 cs1) (Case as2 mot2 cs2) = do unless (length as1 == length as2) $ throwError $ "Mismatching number of case arguments in " ++ pretty (In (Case as1 mot1 cs1)) ++ " and " @@ -100,13 +100,13 @@ instance MonadUnify TermF Elaborator where ++ pretty (In (Case as1 mot1 cs1)) ++ " and " ++ pretty (In (Case as2 mot2 cs2)) let argEqs = zipWith - Equation + (Equation False) (map instantiate0 as1) (map instantiate0 as2) motEqs <- equateCaseMotive mot1 mot2 clauseEqs <- fmap concat $ zipWithM equateClause cs1 cs2 return $ argEqs ++ motEqs ++ clauseEqs - equate (RecordType fields1 tele1) (RecordType fields2 tele2) = + equate f (RecordType fields1 tele1) (RecordType fields2 tele2) = do unless (fields1 == fields2) $ throwError $ "Record types have different field names: " ++ pretty (In (RecordType fields1 tele1)) @@ -121,8 +121,8 @@ instance MonadUnify TermF Elaborator where ++ pretty (In (RecordType fields1 tele1)) ++ " and " ++ pretty (In (RecordType fields2 tele2)) - return $ zipWith Equation as1 as2 - equate (RecordCon fields1) (RecordCon fields2) = + return $ zipWith (Equation f) as1 as2 + equate f (RecordCon fields1) (RecordCon fields2) = do unless (length fields1 == length fields2) $ throwError $ "Records have different number of fields: " ++ pretty (In (RecordCon fields1)) @@ -136,17 +136,17 @@ instance MonadUnify TermF Elaborator where ++ " and " ++ pretty (In (RecordCon fields2)) return $ zipWith - Equation + (Equation f) (map instantiate0 ms1) (map instantiate0 ms2) - equate (RecordProj r1 x1) (RecordProj r2 x2) = + equate _ (RecordProj r1 x1) (RecordProj r2 x2) = do unless (x1 == x2) $ throwError $ "Record projections have different names: " ++ pretty (In (RecordProj r1 x1)) ++ " and " ++ pretty (In (RecordProj r2 x2)) - return [Equation (instantiate0 r1) (instantiate0 r2)] - equate l r = + return [Equation False (instantiate0 r1) (instantiate0 r2)] + equate _ l r = throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r) @@ -164,7 +164,7 @@ equateCaseMotive mot1@(CaseMotive tele1) mot2@(CaseMotive tele2) = unless (length as1 == length as2) $ throwError $ "Motives not equal: " ++ pretty mot1 ++ " and " ++ pretty mot2 - return $ zipWith Equation as1 as2 ++ [ Equation b1 b2 ] + return $ zipWith (Equation False) as1 as2 ++ [ Equation False b1 b2 ] @@ -189,5 +189,5 @@ equateClause (Clause pscs1 sc1) (Clause pscs2 sc2) = Nothing -> throwError "Patterns are not equal." Just pEqss -> - return $ [ Equation a1 a2 | (a1,a2) <- concat pEqss ] - ++ [ Equation b1 b2 ] \ No newline at end of file + return $ [ Equation False a1 a2 | (a1,a2) <- concat pEqss ] + ++ [ Equation False b1 b2 ] diff --git a/src/Poly/Unification/TypeChecking.hs b/src/Poly/Unification/TypeChecking.hs index b5af9f0..e28c02b 100644 --- a/src/Poly/Unification/TypeChecking.hs +++ b/src/Poly/Unification/TypeChecking.hs @@ -119,7 +119,7 @@ isType (Var (Free x)) = tyVarExists x isType (Var (Bound _ _)) = error "Bound type variables should not be the subject of type checking." -isType (Var (Meta _)) = +isType (Var (Meta _ _)) = error "Metavariables should not be the subject of type checking." isType (In (TyCon c as)) = do TyConSig ar <- tyconExists c @@ -150,7 +150,7 @@ instantiateParams argscs retsc = do metas <- replicateM (length (names retsc)) (nextElab nextMeta) - let ms = map (Var . Meta) metas + let ms = map (Var . Meta Exist) metas return ( map (\sc -> instantiate sc ms) argscs , instantiate retsc ms ) @@ -169,7 +169,7 @@ instantiateParams argscs retsc = instantiateQuantifiers :: Type -> TypeChecker Type instantiateQuantifiers (In (Forall sc)) = do meta <- nextElab nextMeta - let m = Var (Meta meta) + let m = Var (Meta Exist meta) instantiateQuantifiers (instantiate sc [m]) instantiateQuantifiers t = return t @@ -215,7 +215,7 @@ inferify (Var (Bound _ _)) = error "A bound variable should never be the subject of type inference." inferify (Var (Free n)) = typeInContext n -inferify (Var (Meta _)) = +inferify (Var (Meta _ _)) = error "Metavariables should not be the subject of type inference." inferify (In (Defined x)) = typeInDefinitions x @@ -227,7 +227,7 @@ inferify (In (Ann m t)) = inferify (In (Lam sc)) = do [n] <- freshRelTo (names sc) context meta <- nextElab nextMeta - let arg = Var (Meta meta) + let arg = Var (Meta Exist meta) ret <- extendElab context [(n, arg)] $ inferify (instantiate sc [Var (Free n)]) subs <- getElab substitution @@ -287,7 +287,7 @@ inferifyClause patTys (Clause pscs sc) = xs2 = map (Var . Free) ns ctx' <- forM ns $ \n -> do m <- nextElab nextMeta - return (n,Var (Meta m)) + return (n,Var (Meta Exist m)) extendElab context ctx' $ do zipWithM_ checkifyPattern (map (\psc -> instantiate psc xs1) pscs) @@ -403,7 +403,7 @@ subtype t (In (Forall sc')) = subtype t (instantiate sc' [Var (Free n)]) subtype (In (Forall sc)) t' = do meta <- nextElab nextMeta - let x2 = Var (Meta meta) + let x2 = Var (Meta Exist meta) subtype (instantiate sc [x2]) t' subtype (In (Fun arg ret)) (In (Fun arg' ret')) = do subtype (instantiate0 arg') (instantiate0 arg) @@ -432,7 +432,7 @@ subtype t t' = checkifyPattern :: Pattern -> Type -> TypeChecker () checkifyPattern (Var (Bound _ _)) _ = error "A bound variable should not be the subject of pattern type checking." -checkifyPattern (Var (Meta _)) _ = +checkifyPattern (Var (Meta _ _)) _ = error "Metavariables should not be the subject of type checking." checkifyPattern (Var (Free n)) t = do t' <- typeInContext n diff --git a/src/Poly/Unification/Unification.hs b/src/Poly/Unification/Unification.hs index 5c784a8..53a4b65 100644 --- a/src/Poly/Unification/Unification.hs +++ b/src/Poly/Unification/Unification.hs @@ -33,7 +33,7 @@ import Control.Monad.Except -- | Equating terms by trivial structural equations. instance MonadUnify TypeF Elaborator where - equate (TyCon tycon1 as1) (TyCon tycon2 as2) = + equate f (TyCon tycon1 as1) (TyCon tycon2 as2) = do unless (tycon1 == tycon2) $ throwError $ "Mismatching type constructors " ++ tycon1 ++ " and " ++ tycon2 @@ -42,16 +42,16 @@ instance MonadUnify TypeF Elaborator where ++ pretty (In (TyCon tycon1 as1)) ++ " and " ++ pretty (In (TyCon tycon2 as1)) return $ zipWith - Equation + (Equation f) (map instantiate0 as1) (map instantiate0 as2) - equate (Fun a1 b1) (Fun a2 b2) = - return [ Equation (instantiate0 a1) (instantiate0 a2) - , Equation (instantiate0 b1) (instantiate0 b2) + equate f (Fun a1 b1) (Fun a2 b2) = + return [ Equation f (instantiate0 a1) (instantiate0 a2) + , Equation f (instantiate0 b1) (instantiate0 b2) ] - equate (Forall sc1) (Forall sc2) = + equate f (Forall sc1) (Forall sc2) = do ns <- freshRelTo (names sc1) context let xs = map (Var . Free) ns - return [ Equation (instantiate sc1 xs) (instantiate sc2 xs) ] - equate l r = - throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r) \ No newline at end of file + return [ Equation f (instantiate sc1 xs) (instantiate sc2 xs) ] + equate _ l r = + throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r) diff --git a/src/Quasiquote/Unification/TypeChecking.hs b/src/Quasiquote/Unification/TypeChecking.hs index 9aecff6..41970f5 100644 --- a/src/Quasiquote/Unification/TypeChecking.hs +++ b/src/Quasiquote/Unification/TypeChecking.hs @@ -284,7 +284,7 @@ inferify (Var (Free x)) = return (ElaboratedTerm (Var (Free x)), t) inferify (Var (Bound _ _)) = error "Bound type variables should not be the subject of type checking." -inferify (Var (Meta x)) = +inferify (Var (Meta _ x)) = throwError $ "The metavariable " ++ show x ++ " appears in checkable code, when it should not." inferify (In (Defined x)) = @@ -446,8 +446,8 @@ inferifyApplication f (In (Fun Expl _ _)) Impl m = ++ pretty (appH Impl f m) inferifyApplication f (In (Fun Impl _ sc)) Expl m = do meta <- nextElab nextMeta - let f' = appH Impl f (Var (Meta meta)) - t' = instantiate sc [Var (Meta meta)] + let f' = appH Impl f (Var (Meta Exist meta)) + t' = instantiate sc [Var (Meta Exist meta)] inferifyApplication f' t' Expl m inferifyApplication f _ _ _ = throwError $ "Cannot apply non-function: " ++ pretty f @@ -504,7 +504,7 @@ inferifyConArgs ascs0 bsc0 ms0 = go [] ascs0 bsc0 ms0 go (acc ++ [(Impl,m')]) ascs bsc ms go acc ((Impl,_):ascs) bsc ms = do meta <- nextElab nextMeta - go (acc ++ [(Impl,Var (Meta meta))]) ascs bsc ms + go (acc ++ [(Impl,Var (Meta Exist meta))]) ascs bsc ms go _ _ _ _ = throwError "Cannot match signature." @@ -780,7 +780,7 @@ checkifyConArgs ascs0 bsc ms0 t = return acc accArgsToCheck acc ((Expl,asc):ascs) ((Expl,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Expl, Just m, x, instantiate asc xs) accArgsToCheck @@ -789,7 +789,7 @@ checkifyConArgs ascs0 bsc ms0 t = ms accArgsToCheck acc ((Impl,asc):ascs) ((Impl,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Just m, x, instantiate asc xs) accArgsToCheck @@ -798,7 +798,7 @@ checkifyConArgs ascs0 bsc ms0 t = ms accArgsToCheck acc ((Impl,asc):ascs) ms = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Nothing, x, instantiate asc xs) accArgsToCheck @@ -811,12 +811,12 @@ checkifyConArgs ascs0 bsc ms0 t = swapMetas :: [(Plicity,Term)] -> TypeChecker ([(Term,Term)], [(Plicity,Term)]) swapMetas [] = return ([],[]) - swapMetas ((plic, Var (Meta meta)):ms) = + swapMetas ((plic, Var (Meta Exist meta)):ms) = do (eqs,ms') <- swapMetas ms - return (eqs, (plic,Var (Meta meta)):ms') + return (eqs, (plic,Var (Meta Exist meta)):ms') swapMetas ((plic,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) (eqs,ms') <- swapMetas ms return ((x,m):eqs, (plic,x):ms') @@ -872,7 +872,7 @@ checkifyCaseMotive (CaseMotive tele) = checkifyPattern :: Pattern -> NormalTerm - -> TypeChecker (Pattern,ElaboratedTerm) + -> TypeChecker (Pattern,ElaboratedTerm,[(Term,Term)]) checkifyPattern (Var (Bound _ _)) _ = error "A bound variable should not be the subject of pattern type checking." checkifyPattern (Var (Free x)) t = @@ -880,12 +880,13 @@ checkifyPattern (Var (Free x)) t = unifyHelper t (NormalTerm t') -- @t'@ is guaranteed to be normal return ( Var (Free x) , ElaboratedTerm (Var (Free x)) + , [] ) -checkifyPattern (Var (Meta _)) _ = +checkifyPattern (Var (Meta _ _)) _ = error "Metavariables should not be the subject of pattern type checking." checkifyPattern (In (ConPat c ps)) (NormalTerm t) = do (ec,ConSig plics (BindingTelescope ascs bsc)) <- typeInSignature c - (ps',elms') <- + (ps',elms',cs) <- checkifyPatterns (zip plics ascs) bsc @@ -894,17 +895,21 @@ checkifyPattern (In (ConPat c ps)) (NormalTerm t) = let ms' = [ (plic,m') | (plic, ElaboratedTerm m') <- elms' ] return ( conPatH ec ps' , ElaboratedTerm (conH ec ms') + , cs ) checkifyPattern (In (AssertionPat m)) t = do ElaboratedTerm m' <- checkify m t + mv <- nextElab nextMeta return ( In (AssertionPat m') - , ElaboratedTerm m' + , ElaboratedTerm (Var $ Meta Constraint mv) + , [(Var $ Meta Constraint mv, m')] ) checkifyPattern (In MakeMeta) _ = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) return ( In (AssertionPat x) , ElaboratedTerm x + , [] ) @@ -943,6 +948,7 @@ checkifyPatterns :: [(Plicity,Scope TermF)] -> Term -> TypeChecker ( [(Plicity,Pattern)] , [(Plicity,ElaboratedTerm)] + , [(Term,Term)] ) checkifyPatterns ascs0 bsc ps0 t = do argsToCheck <- accArgsToCheck [] ascs0 ps0 @@ -956,33 +962,36 @@ checkifyPatterns ascs0 bsc ps0 t = return (eqs,ret') ret' -> return ([],ret') unifyHelper (NormalTerm ret') (NormalTerm t) - psms' <- forM argsToCheck $ \(plic,p0,mToElabInto,a) -> + (ps',ms',cs) <- unzip3 <$> forM argsToCheck (\(plic,p0,mToElabInto,a) -> case p0 of Nothing -> do subMToElabInto <- substitute mToElabInto em' <- evaluate subMToElabInto return ( (plic, In (AssertionPat (normTerm em'))) , (plic, ElaboratedTerm (normTerm em')) + , [] ) Just p -> do subMToElabInto <- substitute mToElabInto eMToElabInto <- evaluate subMToElabInto suba <- substitute a ea <- evaluate suba - (p',ElaboratedTerm m') <- checkifyPattern p ea + (p',ElaboratedTerm m',cs) <- checkifyPattern p ea subm' <- substitute m' em' <- evaluate subm' unifyHelper eMToElabInto em' return ( (plic, p') , (plic, ElaboratedTerm (normTerm em')) + , cs ) + ) forM_ eqs $ \(l,r) -> do subl <- substitute l el <- evaluate subl subr <- substitute r er <- evaluate subr unifyHelper el er - return $ unzip psms' + return (ps',ms',concat cs) where accArgsToCheck :: [(Plicity,Maybe Pattern,Term,Term)] -> [(Plicity,Scope TermF)] @@ -992,7 +1001,7 @@ checkifyPatterns ascs0 bsc ps0 t = return acc accArgsToCheck acc ((Expl,asc):ascs) ((Expl,p):ps) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Expl, Just p, x, instantiate asc xs) accArgsToCheck @@ -1001,7 +1010,7 @@ checkifyPatterns ascs0 bsc ps0 t = ps accArgsToCheck acc ((Impl,asc):ascs) ((Impl,p):ps) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Just p, x, instantiate asc xs) accArgsToCheck @@ -1010,7 +1019,7 @@ checkifyPatterns ascs0 bsc ps0 t = ps accArgsToCheck acc ((Impl,asc):ascs) ps = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Nothing, x, instantiate asc xs) accArgsToCheck @@ -1023,12 +1032,12 @@ checkifyPatterns ascs0 bsc ps0 t = swapMetas :: [(Plicity,Term)] -> TypeChecker ([(Term,Term)], [(Plicity,Term)]) swapMetas [] = return ([],[]) - swapMetas ((plic, Var (Meta meta)):ms) = + swapMetas ((plic, Var (Meta Exist meta)):ms) = do (eqs,ms') <- swapMetas ms - return (eqs, (plic,Var (Meta meta)):ms') + return (eqs, (plic,Var (Meta Exist meta)):ms') swapMetas ((plic,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) (eqs,ms') <- swapMetas ms return ((x,m):eqs, (plic,x):ms') @@ -1054,21 +1063,34 @@ checkifyPatternsCaseMotive :: [Pattern] -> CaseMotive -> TypeChecker ([Pattern], ElaboratedTerm) checkifyPatternsCaseMotive ps0 (CaseMotive (BindingTelescope ascs bsc)) = - do (ps',ms') <- go [] ps0 ascs + do (ps',ms',cs) <- go [] ps0 ascs + forM_ cs (\(l,r) -> do + subl <- substitute l + el <- evaluate subl + subr <- substitute r + er <- evaluate subr + s <- getElab substitution + unifyHelper el er + s' <- getElab substitution + when (length s /= length s') $ + throwError $ "Solving the constraint " + ++ pretty (normTerm el) ++ " == " + ++ pretty (normTerm er) ++ " produced new metavar resolution" + ) return (ps', ElaboratedTerm (instantiate bsc ms')) where go :: [Term] -> [Pattern] -> [Scope TermF] - -> TypeChecker ([Pattern],[Term]) + -> TypeChecker ([Pattern],[Term],[(Term,Term)]) go _ [] [] = - return ([],[]) + return ([],[],[]) go acc (p:ps) (sc:scs) = do subt <- substitute (instantiate sc acc) et <- evaluate subt - (p',ElaboratedTerm m') <- checkifyPattern p et - (ps',ms') <- go (acc ++ [m']) ps scs - return (p':ps', m':ms') + (p',ElaboratedTerm m',cs) <- checkifyPattern p et + (ps',ms',cs') <- go (acc ++ [m']) ps scs + return (p':ps', m':ms', cs ++ cs') go _ _ _ = error $ "The auxiliary function 'go' in 'checkPatternsCaseMotive'" ++ " should always have equal number of args for its patterns and" @@ -1102,7 +1124,7 @@ checkifyClause (Clause pscs sc) mot@(CaseMotive (BindingTelescope ascs _)) = l <- getElab quoteLevel ctx' <- forM ns $ \n -> do m <- nextElab nextMeta - return (n, QLJ (Var (Meta m)) l) + return (n, QLJ (Var (Meta Exist m)) l) extendElab context ctx' $ do (ps',ElaboratedTerm ret) <- checkifyPatternsCaseMotive diff --git a/src/Quasiquote/Unification/Unification.hs b/src/Quasiquote/Unification/Unification.hs index 7216215..2bb222f 100644 --- a/src/Quasiquote/Unification/Unification.hs +++ b/src/Quasiquote/Unification/Unification.hs @@ -35,44 +35,44 @@ import Control.Monad.Except -- | Equating terms by trivial structural equations. instance MonadUnify TermF Elaborator where - equate (Defined n1) (Defined n2) = + equate _ (Defined n1) (Defined n2) = if n1 == n2 then return [] else throwError $ "Mismatching names " ++ showName n1 ++ " and " ++ showName n2 - equate (Ann m1 t1) (Ann m2 t2) = - return [ Equation (instantiate0 m1) (instantiate0 m2) - , Equation (instantiate0 t1) (instantiate0 t2) + equate f (Ann m1 t1) (Ann m2 t2) = + return [ Equation f (instantiate0 m1) (instantiate0 m2) + , Equation f (instantiate0 t1) (instantiate0 t2) ] - equate Type Type = + equate _ Type Type = return [] - equate (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) = + equate f (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) = do unless (plic1 == plic2) $ throwError $ "Mismatching plicities when unifying " ++ pretty (In (Fun plic1 a1 sc1)) ++ " with " ++ pretty (In (Fun plic2 a2 sc2)) ns <- freshRelTo (names sc1) context let xs = map (Var . Free) ns - return [ Equation (instantiate0 a1) (instantiate0 a2) - , Equation (instantiate sc1 xs) (instantiate sc2 xs) + return [ Equation f (instantiate0 a1) (instantiate0 a2) + , Equation f (instantiate sc1 xs) (instantiate sc2 xs) ] - equate (Lam plic1 sc1) (Lam plic2 sc2) = + equate f (Lam plic1 sc1) (Lam plic2 sc2) = do unless (plic1 == plic2) $ throwError $ "Mismatching plicities when unifying " ++ pretty (In (Lam plic1 sc1)) ++ " with " ++ pretty (In (Lam plic2 sc2)) ns <- freshRelTo (names sc1) context let xs = map (Var . Free) ns - return [ Equation (instantiate sc1 xs) (instantiate sc2 xs) ] - equate (App plic1 f1 a1) (App plic2 f2 a2) = + return [ Equation f (instantiate sc1 xs) (instantiate sc2 xs) ] + equate _ (App plic1 f1 a1) (App plic2 f2 a2) = do unless (plic1 == plic2) $ throwError $ "Mismatching plicities when unifying " ++ pretty (In (App plic1 f1 a1)) ++ " with " ++ pretty (In (App plic2 f2 a2)) - return [ Equation (instantiate0 f1) (instantiate0 f2) - , Equation (instantiate0 a1) (instantiate0 a2) + return [ Equation False (instantiate0 f1) (instantiate0 f2) + , Equation False (instantiate0 a1) (instantiate0 a2) ] - equate (Con c1 as1) (Con c2 as2) = + equate f (Con c1 as1) (Con c2 as2) = do unless (c1 == c2) $ throwError $ "Mismatching constructors " ++ showName c1 ++ " and " ++ showName c2 @@ -87,10 +87,10 @@ instance MonadUnify TermF Elaborator where ++ pretty (In (Con c1 as1)) ++ " with " ++ pretty (In (Con c2 as2)) return $ zipWith - Equation + (Equation f) (map instantiate0 as1') (map instantiate0 as2') - equate (Case as1 mot1 cs1) (Case as2 mot2 cs2) = + equate _ (Case as1 mot1 cs1) (Case as2 mot2 cs2) = do unless (length as1 == length as2) $ throwError $ "Mismatching number of case arguments in " ++ pretty (In (Case as1 mot1 cs1)) ++ " and " @@ -100,13 +100,13 @@ instance MonadUnify TermF Elaborator where ++ pretty (In (Case as1 mot1 cs1)) ++ " and " ++ pretty (In (Case as2 mot2 cs2)) let argEqs = zipWith - Equation + (Equation False) (map instantiate0 as1) (map instantiate0 as2) motEqs <- equateCaseMotive mot1 mot2 clauseEqs <- fmap concat $ zipWithM equateClause cs1 cs2 return $ argEqs ++ motEqs ++ clauseEqs - equate (RecordType fields1 tele1) (RecordType fields2 tele2) = + equate f (RecordType fields1 tele1) (RecordType fields2 tele2) = do unless (fields1 == fields2) $ throwError $ "Record types have different field names: " ++ pretty (In (RecordType fields1 tele1)) @@ -121,8 +121,8 @@ instance MonadUnify TermF Elaborator where ++ pretty (In (RecordType fields1 tele1)) ++ " and " ++ pretty (In (RecordType fields2 tele2)) - return $ zipWith Equation as1 as2 - equate (RecordCon fields1) (RecordCon fields2) = + return $ zipWith (Equation f) as1 as2 + equate f (RecordCon fields1) (RecordCon fields2) = do unless (length fields1 == length fields2) $ throwError $ "Records have different number of fields: " ++ pretty (In (RecordCon fields1)) @@ -136,23 +136,23 @@ instance MonadUnify TermF Elaborator where ++ " and " ++ pretty (In (RecordCon fields2)) return $ zipWith - Equation + (Equation f) (map instantiate0 ms1) (map instantiate0 ms2) - equate (RecordProj r1 x1) (RecordProj r2 x2) = + equate _ (RecordProj r1 x1) (RecordProj r2 x2) = do unless (x1 == x2) $ throwError $ "Record projections have different names: " ++ pretty (In (RecordProj r1 x1)) ++ " and " ++ pretty (In (RecordProj r2 x2)) - return [Equation (instantiate0 r1) (instantiate0 r2)] - equate (QuotedType a1) (QuotedType a2) = - return [Equation (instantiate0 a1) (instantiate0 a2)] - equate (Quote m1) (Quote m2) = - return [Equation (instantiate0 m1) (instantiate0 m2)] - equate (Unquote m1) (Unquote m2) = - return [Equation (instantiate0 m1) (instantiate0 m2)] - equate l r = + return [Equation False (instantiate0 r1) (instantiate0 r2)] + equate _ (QuotedType a1) (QuotedType a2) = + return [Equation False (instantiate0 a1) (instantiate0 a2)] + equate _ (Quote m1) (Quote m2) = + return [Equation False (instantiate0 m1) (instantiate0 m2)] + equate _ (Unquote m1) (Unquote m2) = + return [Equation False (instantiate0 m1) (instantiate0 m2)] + equate _ l r = throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r) @@ -170,7 +170,7 @@ equateCaseMotive mot1@(CaseMotive tele1) mot2@(CaseMotive tele2) = unless (length as1 == length as2) $ throwError $ "Motives not equal: " ++ pretty mot1 ++ " and " ++ pretty mot2 - return $ zipWith Equation as1 as2 ++ [ Equation b1 b2 ] + return $ zipWith (Equation False) as1 as2 ++ [ Equation False b1 b2 ] @@ -195,5 +195,5 @@ equateClause (Clause pscs1 sc1) (Clause pscs2 sc2) = Nothing -> throwError "Patterns are not equal." Just pEqss -> - return $ [ Equation a1 a2 | (a1,a2) <- concat pEqss ] - ++ [ Equation b1 b2 ] \ No newline at end of file + return $ [ Equation False a1 a2 | (a1,a2) <- concat pEqss ] + ++ [ Equation False b1 b2 ] diff --git a/src/Record/Unification/TypeChecking.hs b/src/Record/Unification/TypeChecking.hs index 89095ff..ce649b2 100644 --- a/src/Record/Unification/TypeChecking.hs +++ b/src/Record/Unification/TypeChecking.hs @@ -245,7 +245,7 @@ inferify (Var (Free x)) = return (ElaboratedTerm (Var (Free x)), t) inferify (Var (Bound _ _)) = error "Bound type variables should not be the subject of type checking." -inferify (Var (Meta x)) = +inferify (Var (Meta _ x)) = throwError $ "The metavariable " ++ show x ++ " appears in checkable code, when it should not." inferify (In (Defined x)) = @@ -392,8 +392,8 @@ inferifyApplication f (In (Fun Expl _ _)) Impl m = ++ pretty (appH Impl f m) inferifyApplication f (In (Fun Impl _ sc)) Expl m = do meta <- nextElab nextMeta - let f' = appH Impl f (Var (Meta meta)) - t' = instantiate sc [Var (Meta meta)] + let f' = appH Impl f (Var (Meta Exist meta)) + t' = instantiate sc [Var (Meta Exist meta)] inferifyApplication f' t' Expl m inferifyApplication f _ _ _ = throwError $ "Cannot apply non-function: " ++ pretty f @@ -450,7 +450,7 @@ inferifyConArgs ascs0 bsc0 ms0 = go [] ascs0 bsc0 ms0 go (acc ++ [(Impl,m')]) ascs bsc ms go acc ((Impl,_):ascs) bsc ms = do meta <- nextElab nextMeta - go (acc ++ [(Impl,Var (Meta meta))]) ascs bsc ms + go (acc ++ [(Impl,Var (Meta Exist meta))]) ascs bsc ms go _ _ _ _ = throwError "Cannot match signature." @@ -710,7 +710,7 @@ checkifyConArgs ascs0 bsc ms0 t = return acc accArgsToCheck acc ((Expl,asc):ascs) ((Expl,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Expl, Just m, x, instantiate asc xs) accArgsToCheck @@ -719,7 +719,7 @@ checkifyConArgs ascs0 bsc ms0 t = ms accArgsToCheck acc ((Impl,asc):ascs) ((Impl,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Just m, x, instantiate asc xs) accArgsToCheck @@ -728,7 +728,7 @@ checkifyConArgs ascs0 bsc ms0 t = ms accArgsToCheck acc ((Impl,asc):ascs) ms = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Nothing, x, instantiate asc xs) accArgsToCheck @@ -741,12 +741,12 @@ checkifyConArgs ascs0 bsc ms0 t = swapMetas :: [(Plicity,Term)] -> TypeChecker ([(Term,Term)], [(Plicity,Term)]) swapMetas [] = return ([],[]) - swapMetas ((plic, Var (Meta meta)):ms) = + swapMetas ((plic, Var (Meta Exist meta)):ms) = do (eqs,ms') <- swapMetas ms - return (eqs, (plic,Var (Meta meta)):ms') + return (eqs, (plic,Var (Meta Exist meta)):ms') swapMetas ((plic,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) (eqs,ms') <- swapMetas ms return ((x,m):eqs, (plic,x):ms') @@ -802,7 +802,7 @@ checkifyCaseMotive (CaseMotive tele) = checkifyPattern :: Pattern -> NormalTerm - -> TypeChecker (Pattern,ElaboratedTerm) + -> TypeChecker (Pattern,ElaboratedTerm,[(Term,Term)]) checkifyPattern (Var (Bound _ _)) _ = error "A bound variable should not be the subject of pattern type checking." checkifyPattern (Var (Free x)) t = @@ -810,12 +810,13 @@ checkifyPattern (Var (Free x)) t = unifyHelper t (NormalTerm t') -- @t'@ is guaranteed to be normal return ( Var (Free x) , ElaboratedTerm (Var (Free x)) + , [] ) -checkifyPattern (Var (Meta _)) _ = +checkifyPattern (Var (Meta _ _)) _ = error "Metavariables should not be the subject of pattern type checking." checkifyPattern (In (ConPat c ps)) (NormalTerm t) = do (ec,ConSig plics (BindingTelescope ascs bsc)) <- typeInSignature c - (ps',elms') <- + (ps',elms',cs) <- checkifyPatterns (zip plics ascs) bsc @@ -824,17 +825,21 @@ checkifyPattern (In (ConPat c ps)) (NormalTerm t) = let ms' = [ (plic,m') | (plic, ElaboratedTerm m') <- elms' ] return ( conPatH ec ps' , ElaboratedTerm (conH ec ms') + , cs ) checkifyPattern (In (AssertionPat m)) t = do ElaboratedTerm m' <- checkify m t + mv <- nextElab nextMeta return ( In (AssertionPat m') - , ElaboratedTerm m' + , ElaboratedTerm (Var $ Meta Constraint mv) + , [(Var $ Meta Constraint mv, m')] ) checkifyPattern (In MakeMeta) _ = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) return ( In (AssertionPat x) , ElaboratedTerm x + , [] ) @@ -873,6 +878,7 @@ checkifyPatterns :: [(Plicity,Scope TermF)] -> Term -> TypeChecker ( [(Plicity,Pattern)] , [(Plicity,ElaboratedTerm)] + , [(Term,Term)] ) checkifyPatterns ascs0 bsc ps0 t = do argsToCheck <- accArgsToCheck [] ascs0 ps0 @@ -886,33 +892,36 @@ checkifyPatterns ascs0 bsc ps0 t = return (eqs,ret') ret' -> return ([],ret') unifyHelper (NormalTerm ret') (NormalTerm t) - psms' <- forM argsToCheck $ \(plic,p0,mToElabInto,a) -> + (ps',ms',cs) <- unzip3 <$> forM argsToCheck (\(plic,p0,mToElabInto,a) -> case p0 of Nothing -> do subMToElabInto <- substitute mToElabInto em' <- evaluate subMToElabInto return ( (plic, In (AssertionPat (normTerm em'))) , (plic, ElaboratedTerm (normTerm em')) + , [] ) Just p -> do subMToElabInto <- substitute mToElabInto eMToElabInto <- evaluate subMToElabInto suba <- substitute a ea <- evaluate suba - (p',ElaboratedTerm m') <- checkifyPattern p ea + (p',ElaboratedTerm m',cs) <- checkifyPattern p ea subm' <- substitute m' em' <- evaluate subm' unifyHelper eMToElabInto em' return ( (plic, p') , (plic, ElaboratedTerm (normTerm em')) + , cs ) + ) forM_ eqs $ \(l,r) -> do subl <- substitute l el <- evaluate subl subr <- substitute r er <- evaluate subr unifyHelper el er - return $ unzip psms' + return (ps',ms',concat cs) where accArgsToCheck :: [(Plicity,Maybe Pattern,Term,Term)] -> [(Plicity,Scope TermF)] @@ -922,7 +931,7 @@ checkifyPatterns ascs0 bsc ps0 t = return acc accArgsToCheck acc ((Expl,asc):ascs) ((Expl,p):ps) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Expl, Just p, x, instantiate asc xs) accArgsToCheck @@ -931,7 +940,7 @@ checkifyPatterns ascs0 bsc ps0 t = ps accArgsToCheck acc ((Impl,asc):ascs) ((Impl,p):ps) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Just p, x, instantiate asc xs) accArgsToCheck @@ -940,7 +949,7 @@ checkifyPatterns ascs0 bsc ps0 t = ps accArgsToCheck acc ((Impl,asc):ascs) ps = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Nothing, x, instantiate asc xs) accArgsToCheck @@ -953,12 +962,12 @@ checkifyPatterns ascs0 bsc ps0 t = swapMetas :: [(Plicity,Term)] -> TypeChecker ([(Term,Term)], [(Plicity,Term)]) swapMetas [] = return ([],[]) - swapMetas ((plic, Var (Meta meta)):ms) = + swapMetas ((plic, Var (Meta Exist meta)):ms) = do (eqs,ms') <- swapMetas ms - return (eqs, (plic,Var (Meta meta)):ms') + return (eqs, (plic,Var (Meta Exist meta)):ms') swapMetas ((plic,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) (eqs,ms') <- swapMetas ms return ((x,m):eqs, (plic,x):ms') @@ -984,21 +993,34 @@ checkifyPatternsCaseMotive :: [Pattern] -> CaseMotive -> TypeChecker ([Pattern], ElaboratedTerm) checkifyPatternsCaseMotive ps0 (CaseMotive (BindingTelescope ascs bsc)) = - do (ps',ms') <- go [] ps0 ascs + do (ps',ms',cs) <- go [] ps0 ascs + forM_ cs (\(l,r) -> do + subl <- substitute l + el <- evaluate subl + subr <- substitute r + er <- evaluate subr + s <- getElab substitution + unifyHelper el er + s' <- getElab substitution + when (length s /= length s') $ + throwError $ "Solving the constraint " + ++ pretty (normTerm el) ++ " == " + ++ pretty (normTerm er) ++ " produced new metavar resolution" + ) return (ps', ElaboratedTerm (instantiate bsc ms')) where go :: [Term] -> [Pattern] -> [Scope TermF] - -> TypeChecker ([Pattern],[Term]) + -> TypeChecker ([Pattern],[Term],[(Term,Term)]) go _ [] [] = - return ([],[]) + return ([],[],[]) go acc (p:ps) (sc:scs) = do subt <- substitute (instantiate sc acc) et <- evaluate subt - (p',ElaboratedTerm m') <- checkifyPattern p et - (ps',ms') <- go (acc ++ [m']) ps scs - return (p':ps', m':ms') + (p',ElaboratedTerm m',cs) <- checkifyPattern p et + (ps',ms',cs') <- go (acc ++ [m']) ps scs + return (p':ps', m':ms', cs ++ cs') go _ _ _ = error $ "The auxiliary function 'go' in 'checkPatternsCaseMotive'" ++ " should always have equal number of args for its patterns and" @@ -1031,7 +1053,7 @@ checkifyClause (Clause pscs sc) mot@(CaseMotive (BindingTelescope ascs _)) = xs2 = map (Var . Free) ns ctx' <- forM ns $ \n -> do m <- nextElab nextMeta - return (n, Var (Meta m)) + return (n, Var (Meta Exist m)) extendElab context ctx' $ do (ps',ElaboratedTerm ret) <- checkifyPatternsCaseMotive diff --git a/src/Record/Unification/Unification.hs b/src/Record/Unification/Unification.hs index 1ce54eb..5b84fd0 100644 --- a/src/Record/Unification/Unification.hs +++ b/src/Record/Unification/Unification.hs @@ -35,44 +35,44 @@ import Control.Monad.Except -- | Equating terms by trivial structural equations. instance MonadUnify TermF Elaborator where - equate (Defined n1) (Defined n2) = + equate _ (Defined n1) (Defined n2) = if n1 == n2 then return [] else throwError $ "Mismatching names " ++ showName n1 ++ " and " ++ showName n2 - equate (Ann m1 t1) (Ann m2 t2) = - return [ Equation (instantiate0 m1) (instantiate0 m2) - , Equation (instantiate0 t1) (instantiate0 t2) + equate f (Ann m1 t1) (Ann m2 t2) = + return [ Equation f (instantiate0 m1) (instantiate0 m2) + , Equation f (instantiate0 t1) (instantiate0 t2) ] - equate Type Type = + equate _ Type Type = return [] - equate (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) = + equate f (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) = do unless (plic1 == plic2) $ throwError $ "Mismatching plicities when unifying " ++ pretty (In (Fun plic1 a1 sc1)) ++ " with " ++ pretty (In (Fun plic2 a2 sc2)) ns <- freshRelTo (names sc1) context let xs = map (Var . Free) ns - return [ Equation (instantiate0 a1) (instantiate0 a2) - , Equation (instantiate sc1 xs) (instantiate sc2 xs) + return [ Equation f (instantiate0 a1) (instantiate0 a2) + , Equation f (instantiate sc1 xs) (instantiate sc2 xs) ] - equate (Lam plic1 sc1) (Lam plic2 sc2) = + equate f (Lam plic1 sc1) (Lam plic2 sc2) = do unless (plic1 == plic2) $ throwError $ "Mismatching plicities when unifying " ++ pretty (In (Lam plic1 sc1)) ++ " with " ++ pretty (In (Lam plic2 sc2)) ns <- freshRelTo (names sc1) context let xs = map (Var . Free) ns - return [ Equation (instantiate sc1 xs) (instantiate sc2 xs) ] - equate (App plic1 f1 a1) (App plic2 f2 a2) = + return [ Equation f (instantiate sc1 xs) (instantiate sc2 xs) ] + equate _ (App plic1 f1 a1) (App plic2 f2 a2) = do unless (plic1 == plic2) $ throwError $ "Mismatching plicities when unifying " ++ pretty (In (App plic1 f1 a1)) ++ " with " ++ pretty (In (App plic2 f2 a2)) - return [ Equation (instantiate0 f1) (instantiate0 f2) - , Equation (instantiate0 a1) (instantiate0 a2) + return [ Equation False (instantiate0 f1) (instantiate0 f2) + , Equation False (instantiate0 a1) (instantiate0 a2) ] - equate (Con c1 as1) (Con c2 as2) = + equate f (Con c1 as1) (Con c2 as2) = do unless (c1 == c2) $ throwError $ "Mismatching constructors " ++ showName c1 ++ " and " ++ showName c2 @@ -87,10 +87,10 @@ instance MonadUnify TermF Elaborator where ++ pretty (In (Con c1 as1)) ++ " with " ++ pretty (In (Con c2 as2)) return $ zipWith - Equation + (Equation f) (map instantiate0 as1') (map instantiate0 as2') - equate (Case as1 mot1 cs1) (Case as2 mot2 cs2) = + equate _ (Case as1 mot1 cs1) (Case as2 mot2 cs2) = do unless (length as1 == length as2) $ throwError $ "Mismatching number of case arguments in " ++ pretty (In (Case as1 mot1 cs1)) ++ " and " @@ -100,13 +100,13 @@ instance MonadUnify TermF Elaborator where ++ pretty (In (Case as1 mot1 cs1)) ++ " and " ++ pretty (In (Case as2 mot2 cs2)) let argEqs = zipWith - Equation + (Equation False) (map instantiate0 as1) (map instantiate0 as2) motEqs <- equateCaseMotive mot1 mot2 clauseEqs <- fmap concat $ zipWithM equateClause cs1 cs2 return $ argEqs ++ motEqs ++ clauseEqs - equate (RecordType fields1 tele1) (RecordType fields2 tele2) = + equate f (RecordType fields1 tele1) (RecordType fields2 tele2) = do unless (fields1 == fields2) $ throwError $ "Record types have different field names: " ++ pretty (In (RecordType fields1 tele1)) @@ -121,8 +121,8 @@ instance MonadUnify TermF Elaborator where ++ pretty (In (RecordType fields1 tele1)) ++ " and " ++ pretty (In (RecordType fields2 tele2)) - return $ zipWith Equation as1 as2 - equate (RecordCon fields1) (RecordCon fields2) = + return $ zipWith (Equation f) as1 as2 + equate f (RecordCon fields1) (RecordCon fields2) = do unless (length fields1 == length fields2) $ throwError $ "Records have different number of fields: " ++ pretty (In (RecordCon fields1)) @@ -136,17 +136,17 @@ instance MonadUnify TermF Elaborator where ++ " and " ++ pretty (In (RecordCon fields2)) return $ zipWith - Equation + (Equation f) (map instantiate0 ms1) (map instantiate0 ms2) - equate (RecordProj r1 x1) (RecordProj r2 x2) = + equate _ (RecordProj r1 x1) (RecordProj r2 x2) = do unless (x1 == x2) $ throwError $ "Record projections have different names: " ++ pretty (In (RecordProj r1 x1)) ++ " and " ++ pretty (In (RecordProj r2 x2)) - return [Equation (instantiate0 r1) (instantiate0 r2)] - equate l r = + return [Equation False (instantiate0 r1) (instantiate0 r2)] + equate _ l r = throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r) @@ -164,7 +164,7 @@ equateCaseMotive mot1@(CaseMotive tele1) mot2@(CaseMotive tele2) = unless (length as1 == length as2) $ throwError $ "Motives not equal: " ++ pretty mot1 ++ " and " ++ pretty mot2 - return $ zipWith Equation as1 as2 ++ [ Equation b1 b2 ] + return $ zipWith (Equation False) as1 as2 ++ [ Equation False b1 b2 ] @@ -189,5 +189,5 @@ equateClause (Clause pscs1 sc1) (Clause pscs2 sc2) = Nothing -> throwError "Patterns are not equal." Just pEqss -> - return $ [ Equation a1 a2 | (a1,a2) <- concat pEqss ] - ++ [ Equation b1 b2 ] \ No newline at end of file + return $ [ Equation False a1 a2 | (a1,a2) <- concat pEqss ] + ++ [ Equation False b1 b2 ] diff --git a/src/Require/Core/Parser.hs b/src/Require/Core/Parser.hs index 43e9cb0..9eaed5d 100644 --- a/src/Require/Core/Parser.hs +++ b/src/Require/Core/Parser.hs @@ -19,8 +19,8 @@ import Require.Core.DeclArg import Require.Core.Term import Require.Core.Program -import Debug - +--import Debug +debug_ = const $ return () diff --git a/src/Require/Core/Term.hs b/src/Require/Core/Term.hs index 2b41660..defaf1c 100644 --- a/src/Require/Core/Term.hs +++ b/src/Require/Core/Term.hs @@ -64,45 +64,45 @@ data TermF r instance Eq1 TermF where - eq1 (Defined n) (Defined n') = + liftEq _ (Defined n) (Defined n') = n == n' - eq1 (Ann m t) (Ann m' t') = - m == m' && t == t' - eq1 Type Type = + liftEq eq (Ann m t) (Ann m' t') = + eq m m' && eq t t' + liftEq _ Type Type = True - eq1 (Fun plic a sc) (Fun plic' a' sc') = - plic == plic' && a == a' && sc == sc' - eq1 (Lam plic sc) (Lam plic' sc') = - plic == plic' && sc == sc' - eq1 (App plic f x) (App plic' f' x') = - plic == plic' && f == f' && x == x' - eq1 (Con c ms) (Con c' ms') = - c == c' && ms == ms' - eq1 (Case ms motive clauses) (Case ms' motive' clauses') = - ms == ms' && eq1 motive motive' + liftEq eq (Fun plic a sc) (Fun plic' a' sc') = + plic == plic' && eq a a' && eq sc sc' + liftEq eq (Lam plic sc) (Lam plic' sc') = + plic == plic' && eq sc sc' + liftEq eq (App plic f x) (App plic' f' x') = + plic == plic' && eq f f' && eq x x' + liftEq eq (Con c ms) (Con c' ms') = + c == c' && liftEq (\(p,a) (p',a') -> p == p' && eq a a') ms ms' + liftEq eq (Case ms motive clauses) (Case ms' motive' clauses') = + liftEq eq ms ms' && liftEq eq motive motive' && length clauses == length clauses' - && all (uncurry eq1) (zip clauses clauses') - eq1 (RecordType fields tele) (RecordType fields' tele') = - fields == fields' && eq1 tele tele' - eq1 (RecordCon fs) (RecordCon fs') = - fs == fs' - eq1 (RecordProj m x) (RecordProj m' x') = - x == x' && m == m' - eq1 (QuotedType resets a) (QuotedType resets' a') = - resets == resets' && a == a' - eq1 (Quote m) (Quote m') = - m == m' - eq1 (Unquote m) (Unquote m') = - m == m' - eq1 (Continue m) (Continue m') = - m == m' - eq1 (Shift res m) (Shift res' m') = - res == res' && m == m' - eq1 (Reset res m) (Reset res' m') = - res == res' && m == m' - eq1 (Require a sc) (Require a' sc') = - a == a' && sc == sc' - eq1 _ _ = + && all (uncurry $ liftEq eq) (zip clauses clauses') + liftEq eq (RecordType fields tele) (RecordType fields' tele') = + fields == fields' && liftEq eq tele tele' + liftEq eq (RecordCon fs) (RecordCon fs') = + liftEq (\(n,a) (n',a') -> n == n' && eq a a') fs fs' + liftEq eq (RecordProj m x) (RecordProj m' x') = + x == x' && eq m m' + liftEq eq (QuotedType resets a) (QuotedType resets' a') = + resets == resets' && eq a a' + liftEq eq (Quote m) (Quote m') = + eq m m' + liftEq eq (Unquote m) (Unquote m') = + eq m m' + liftEq eq (Continue m) (Continue m') = + eq m m' + liftEq eq (Shift res m) (Shift res' m') = + res == res' && eq m m' + liftEq eq (Reset res m) (Reset res' m') = + res == res' && eq m m' + liftEq eq (Require a sc) (Require a' sc') = + eq a a' && eq sc sc' + liftEq _ _ _ = False @@ -124,8 +124,8 @@ newtype CaseMotiveF r = CaseMotive (BindingTelescope r) instance Eq1 CaseMotiveF where - eq1 (CaseMotive tele) (CaseMotive tele') = - eq1 tele tele' + liftEq eq (CaseMotive tele) (CaseMotive tele') = + liftEq eq tele tele' type CaseMotive = CaseMotiveF (Scope TermF) @@ -137,10 +137,10 @@ data ClauseF r instance Eq1 ClauseF where - eq1 (Clause ps sc) (Clause ps' sc') = + liftEq eq (Clause ps sc) (Clause ps' sc') = length ps == length ps' - && all (uncurry eq1) (zip ps ps') - && sc == sc' + && all (uncurry $ liftEq eq) (zip ps ps') + && eq sc sc' type Clause = ClauseF (Scope TermF) @@ -172,15 +172,24 @@ data PatternFF a r instance Eq a => Eq1 (PatternFF a) where - eq1 (ConPat c ps) (ConPat c' ps') = - c == c' && ps == ps' - eq1 (AssertionPat m) (AssertionPat m') = + liftEq eq (ConPat c ps) (ConPat c' ps') = + c == c' && liftEq (\(p,a) (p',a') -> p == p' && eq a a') ps ps' + liftEq eq (AssertionPat m) (AssertionPat m') = m == m' - eq1 MakeMeta MakeMeta = + liftEq eq MakeMeta MakeMeta = True - eq1 _ _ = + liftEq eq _ _ = False +instance Eq2 PatternFF where + liftEq2 eq eq' (ConPat c ps) (ConPat c' ps') = + c == c' && liftEq (\(p,a) (p',a') -> p == p' && eq' a a') ps ps' + liftEq2 eq eq' (AssertionPat m) (AssertionPat m') = + eq m m' + liftEq2 eq eq' MakeMeta MakeMeta = + True + liftEq2 _ _ _ _ = + False instance Bifunctor PatternFF where bimap _ g (ConPat s xs) = ConPat s [ (plic,g x) | (plic,x) <- xs ] @@ -210,14 +219,15 @@ instance Bizippable PatternFF where instance Bitraversable PatternFF where - bisequenceA (ConPat c ps) = - ConPat c <$> sequenceA [ (,) plic <$> p - | (plic,p) <- ps - ] - bisequenceA (AssertionPat m) = - AssertionPat <$> m - bisequenceA MakeMeta = - pure MakeMeta + bitraverse f g = biseq . bimap f g where + biseq (ConPat c ps) = + ConPat c <$> sequenceA [ (,) plic <$> p + | (plic,p) <- ps + ] + biseq (AssertionPat m) = + AssertionPat <$> m + biseq MakeMeta = + pure MakeMeta -- | 'PatternF' is the type of pattern shaped containers for terms. The @@ -229,7 +239,10 @@ newtype PatternF a = PatternF { unwrapPatternF :: Scope (PatternFF a) } instance Eq1 PatternF where - eq1 (PatternF x) (PatternF x') = x == x' + liftEq eq (PatternF x) (PatternF x') = eqScopes eq x x' + where + eqScopes :: (a -> b -> Bool) -> Scope (PatternFF a) -> Scope (PatternFF b) -> Bool + eqScopes eq' = liftScopeEq (liftABTEq $ liftEq2 eq' (eqScopes eq')) type Pattern = ABT (PatternFF Term) diff --git a/src/Require/Unification/TypeChecking.hs b/src/Require/Unification/TypeChecking.hs index 9f9ab1a..384270b 100644 --- a/src/Require/Unification/TypeChecking.hs +++ b/src/Require/Unification/TypeChecking.hs @@ -344,7 +344,7 @@ inferify (Var (Free x)) = return (ElaboratedTerm (Var (Free x)), t) inferify (Var (Bound _ _)) = error "Bound type variables should not be the subject of type checking." -inferify (Var (Meta x)) = +inferify (Var (Meta _ x)) = throwError $ "The metavariable " ++ show x ++ " appears in checkable code, when it should not." inferify (In (Defined x)) = @@ -552,8 +552,8 @@ inferifyApplication f (In (Fun Expl _ _)) Impl m = ++ pretty (appH Impl f m) inferifyApplication f (In (Fun Impl _ sc)) Expl m = do meta <- nextElab nextMeta - let f' = appH Impl f (Var (Meta meta)) - t' = instantiate sc [Var (Meta meta)] + let f' = appH Impl f (Var (Meta Exist meta)) + t' = instantiate sc [Var (Meta Exist meta)] inferifyApplication f' t' Expl m inferifyApplication f _ _ _ = throwError $ "Cannot apply non-function: " ++ pretty f @@ -610,7 +610,7 @@ inferifyConArgs ascs0 bsc0 ms0 = go [] ascs0 bsc0 ms0 go (acc ++ [(Impl,m')]) ascs bsc ms go acc ((Impl,_):ascs) bsc ms = do meta <- nextElab nextMeta - go (acc ++ [(Impl,Var (Meta meta))]) ascs bsc ms + go (acc ++ [(Impl,Var (Meta Exist meta))]) ascs bsc ms go _ _ _ _ = throwError "Cannot match signature." @@ -903,7 +903,7 @@ checkifyConArgs ascs0 bsc ms0 t = return acc accArgsToCheck acc ((Expl,asc):ascs) ((Expl,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Expl, Just m, x, instantiate asc xs) accArgsToCheck @@ -912,7 +912,7 @@ checkifyConArgs ascs0 bsc ms0 t = ms accArgsToCheck acc ((Impl,asc):ascs) ((Impl,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Just m, x, instantiate asc xs) accArgsToCheck @@ -921,7 +921,7 @@ checkifyConArgs ascs0 bsc ms0 t = ms accArgsToCheck acc ((Impl,asc):ascs) ms = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Nothing, x, instantiate asc xs) accArgsToCheck @@ -934,12 +934,12 @@ checkifyConArgs ascs0 bsc ms0 t = swapMetas :: [(Plicity,Term)] -> TypeChecker ([(Term,Term)], [(Plicity,Term)]) swapMetas [] = return ([],[]) - swapMetas ((plic, Var (Meta meta)):ms) = + swapMetas ((plic, Var (Meta Exist meta)):ms) = do (eqs,ms') <- swapMetas ms - return (eqs, (plic,Var (Meta meta)):ms') + return (eqs, (plic,Var (Meta Exist meta)):ms') swapMetas ((plic,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) (eqs,ms') <- swapMetas ms return ((x,m):eqs, (plic,x):ms') @@ -995,7 +995,7 @@ checkifyCaseMotive (CaseMotive tele) = checkifyPattern :: Pattern -> NormalTerm - -> TypeChecker (Pattern,ElaboratedTerm) + -> TypeChecker (Pattern,ElaboratedTerm,[(Term,Term)]) checkifyPattern (Var (Bound _ _)) _ = error "A bound variable should not be the subject of pattern type checking." checkifyPattern (Var (Free x)) t = @@ -1003,12 +1003,13 @@ checkifyPattern (Var (Free x)) t = unifyHelper t (NormalTerm t') -- @t'@ is guaranteed to be normal return ( Var (Free x) , ElaboratedTerm (Var (Free x)) + , [] ) -checkifyPattern (Var (Meta _)) _ = +checkifyPattern (Var (Meta _ _)) _ = error "Metavariables should not be the subject of pattern type checking." checkifyPattern (In (ConPat c ps)) (NormalTerm t) = do (ec,ConSig plics (BindingTelescope ascs bsc)) <- typeInSignature c - (ps',elms') <- + (ps',elms',cs) <- checkifyPatterns (zip plics ascs) bsc @@ -1017,17 +1018,21 @@ checkifyPattern (In (ConPat c ps)) (NormalTerm t) = let ms' = [ (plic,m') | (plic, ElaboratedTerm m') <- elms' ] return ( conPatH ec ps' , ElaboratedTerm (conH ec ms') + , cs ) checkifyPattern (In (AssertionPat m)) t = do ElaboratedTerm m' <- checkify m t + mv <- nextElab nextMeta return ( In (AssertionPat m') - , ElaboratedTerm m' + , ElaboratedTerm (Var $ Meta Constraint mv) + , [(Var $ Meta Constraint mv, m')] ) checkifyPattern (In MakeMeta) _ = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) return ( In (AssertionPat x) , ElaboratedTerm x + , [] ) @@ -1066,6 +1071,7 @@ checkifyPatterns :: [(Plicity,Scope TermF)] -> Term -> TypeChecker ( [(Plicity,Pattern)] , [(Plicity,ElaboratedTerm)] + , [(Term,Term)] ) checkifyPatterns ascs0 bsc ps0 t = do argsToCheck <- accArgsToCheck [] ascs0 ps0 @@ -1079,33 +1085,36 @@ checkifyPatterns ascs0 bsc ps0 t = return (eqs,ret') ret' -> return ([],ret') unifyHelper (NormalTerm ret') (NormalTerm t) - psms' <- forM argsToCheck $ \(plic,p0,mToElabInto,a) -> + (ps',ms',cs) <- unzip3 <$> forM argsToCheck (\(plic,p0,mToElabInto,a) -> case p0 of Nothing -> do subMToElabInto <- substitute mToElabInto em' <- evaluate subMToElabInto return ( (plic, In (AssertionPat (normTerm em'))) , (plic, ElaboratedTerm (normTerm em')) + , [] ) Just p -> do subMToElabInto <- substitute mToElabInto eMToElabInto <- evaluate subMToElabInto suba <- substitute a ea <- evaluate suba - (p',ElaboratedTerm m') <- checkifyPattern p ea + (p',ElaboratedTerm m',cs) <- checkifyPattern p ea subm' <- substitute m' em' <- evaluate subm' unifyHelper eMToElabInto em' return ( (plic, p') , (plic, ElaboratedTerm (normTerm em')) + , cs ) + ) forM_ eqs $ \(l,r) -> do subl <- substitute l el <- evaluate subl subr <- substitute r er <- evaluate subr unifyHelper el er - return $ unzip psms' + return (ps',ms',concat cs) where accArgsToCheck :: [(Plicity,Maybe Pattern,Term,Term)] -> [(Plicity,Scope TermF)] @@ -1115,7 +1124,7 @@ checkifyPatterns ascs0 bsc ps0 t = return acc accArgsToCheck acc ((Expl,asc):ascs) ((Expl,p):ps) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Expl, Just p, x, instantiate asc xs) accArgsToCheck @@ -1124,7 +1133,7 @@ checkifyPatterns ascs0 bsc ps0 t = ps accArgsToCheck acc ((Impl,asc):ascs) ((Impl,p):ps) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Just p, x, instantiate asc xs) accArgsToCheck @@ -1133,7 +1142,7 @@ checkifyPatterns ascs0 bsc ps0 t = ps accArgsToCheck acc ((Impl,asc):ascs) ps = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) xs = [ x' | (_,_,x',_) <- acc ] newSuspension = (Impl, Nothing, x, instantiate asc xs) accArgsToCheck @@ -1146,12 +1155,12 @@ checkifyPatterns ascs0 bsc ps0 t = swapMetas :: [(Plicity,Term)] -> TypeChecker ([(Term,Term)], [(Plicity,Term)]) swapMetas [] = return ([],[]) - swapMetas ((plic, Var (Meta meta)):ms) = + swapMetas ((plic, Var (Meta Exist meta)):ms) = do (eqs,ms') <- swapMetas ms - return (eqs, (plic,Var (Meta meta)):ms') + return (eqs, (plic,Var (Meta Exist meta)):ms') swapMetas ((plic,m):ms) = do meta <- nextElab nextMeta - let x = Var (Meta meta) + let x = Var (Meta Exist meta) (eqs,ms') <- swapMetas ms return ((x,m):eqs, (plic,x):ms') @@ -1177,21 +1186,34 @@ checkifyPatternsCaseMotive :: [Pattern] -> CaseMotive -> TypeChecker ([Pattern], ElaboratedTerm) checkifyPatternsCaseMotive ps0 (CaseMotive (BindingTelescope ascs bsc)) = - do (ps',ms') <- go [] ps0 ascs + do (ps',ms',cs) <- go [] ps0 ascs + forM_ cs (\(l,r) -> do + subl <- substitute l + el <- evaluate subl + subr <- substitute r + er <- evaluate subr + s <- getElab substitution + unifyHelper el er + s' <- getElab substitution + when (length s /= length s') $ + throwError $ "Solving the constraint " + ++ pretty (normTerm el) ++ " == " + ++ pretty (normTerm er) ++ " produced new metavar resolution" + ) return (ps', ElaboratedTerm (instantiate bsc ms')) where go :: [Term] -> [Pattern] -> [Scope TermF] - -> TypeChecker ([Pattern],[Term]) + -> TypeChecker ([Pattern],[Term],[(Term,Term)]) go _ [] [] = - return ([],[]) + return ([],[],[]) go acc (p:ps) (sc:scs) = do subt <- substitute (instantiate sc acc) et <- evaluate subt - (p',ElaboratedTerm m') <- checkifyPattern p et - (ps',ms') <- go (acc ++ [m']) ps scs - return (p':ps', m':ms') + (p',ElaboratedTerm m',cs) <- checkifyPattern p et + (ps',ms',cs') <- go (acc ++ [m']) ps scs + return (p':ps', m':ms', cs ++ cs') go _ _ _ = error $ "The auxiliary function 'go' in 'checkPatternsCaseMotive'" ++ " should always have equal number of args for its patterns and" @@ -1225,7 +1247,7 @@ checkifyClause (Clause pscs sc) mot@(CaseMotive (BindingTelescope ascs _)) = l <- getElab quoteLevel ctx' <- forM ns $ \n -> do m <- nextElab nextMeta - return (n, QLJ (Var (Meta m)) l) + return (n, QLJ (Var (Meta Exist m)) l) extendElab context ctx' $ do (ps',ElaboratedTerm ret) <- checkifyPatternsCaseMotive diff --git a/src/Require/Unification/Unification.hs b/src/Require/Unification/Unification.hs index 9654fbb..c58c835 100644 --- a/src/Require/Unification/Unification.hs +++ b/src/Require/Unification/Unification.hs @@ -35,44 +35,44 @@ import Control.Monad.Except -- | Equating terms by trivial structural equations. instance MonadUnify TermF Elaborator where - equate (Defined n1) (Defined n2) = + equate _ (Defined n1) (Defined n2) = if n1 == n2 then return [] else throwError $ "Mismatching names " ++ showName n1 ++ " and " ++ showName n2 - equate (Ann m1 t1) (Ann m2 t2) = - return [ Equation (instantiate0 m1) (instantiate0 m2) - , Equation (instantiate0 t1) (instantiate0 t2) + equate f (Ann m1 t1) (Ann m2 t2) = + return [ Equation f (instantiate0 m1) (instantiate0 m2) + , Equation f (instantiate0 t1) (instantiate0 t2) ] - equate Type Type = + equate _ Type Type = return [] - equate (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) = + equate f (Fun plic1 a1 sc1) (Fun plic2 a2 sc2) = do unless (plic1 == plic2) $ throwError $ "Mismatching plicities when unifying " ++ pretty (In (Fun plic1 a1 sc1)) ++ " with " ++ pretty (In (Fun plic2 a2 sc2)) ns <- freshRelTo (names sc1) context let xs = map (Var . Free) ns - return [ Equation (instantiate0 a1) (instantiate0 a2) - , Equation (instantiate sc1 xs) (instantiate sc2 xs) + return [ Equation f (instantiate0 a1) (instantiate0 a2) + , Equation f (instantiate sc1 xs) (instantiate sc2 xs) ] - equate (Lam plic1 sc1) (Lam plic2 sc2) = + equate f (Lam plic1 sc1) (Lam plic2 sc2) = do unless (plic1 == plic2) $ throwError $ "Mismatching plicities when unifying " ++ pretty (In (Lam plic1 sc1)) ++ " with " ++ pretty (In (Lam plic2 sc2)) ns <- freshRelTo (names sc1) context let xs = map (Var . Free) ns - return [ Equation (instantiate sc1 xs) (instantiate sc2 xs) ] - equate (App plic1 f1 a1) (App plic2 f2 a2) = + return [ Equation f (instantiate sc1 xs) (instantiate sc2 xs) ] + equate _ (App plic1 f1 a1) (App plic2 f2 a2) = do unless (plic1 == plic2) $ throwError $ "Mismatching plicities when unifying " ++ pretty (In (App plic1 f1 a1)) ++ " with " ++ pretty (In (App plic2 f2 a2)) - return [ Equation (instantiate0 f1) (instantiate0 f2) - , Equation (instantiate0 a1) (instantiate0 a2) + return [ Equation False (instantiate0 f1) (instantiate0 f2) + , Equation False (instantiate0 a1) (instantiate0 a2) ] - equate (Con c1 as1) (Con c2 as2) = + equate f (Con c1 as1) (Con c2 as2) = do unless (c1 == c2) $ throwError $ "Mismatching constructors " ++ showName c1 ++ " and " ++ showName c2 @@ -87,10 +87,10 @@ instance MonadUnify TermF Elaborator where ++ pretty (In (Con c1 as1)) ++ " with " ++ pretty (In (Con c2 as2)) return $ zipWith - Equation + (Equation f) (map instantiate0 as1') (map instantiate0 as2') - equate (Case as1 mot1 cs1) (Case as2 mot2 cs2) = + equate _ (Case as1 mot1 cs1) (Case as2 mot2 cs2) = do unless (length as1 == length as2) $ throwError $ "Mismatching number of case arguments in " ++ pretty (In (Case as1 mot1 cs1)) ++ " and " @@ -100,13 +100,13 @@ instance MonadUnify TermF Elaborator where ++ pretty (In (Case as1 mot1 cs1)) ++ " and " ++ pretty (In (Case as2 mot2 cs2)) let argEqs = zipWith - Equation + (Equation False) (map instantiate0 as1) (map instantiate0 as2) motEqs <- equateCaseMotive mot1 mot2 clauseEqs <- fmap concat $ zipWithM equateClause cs1 cs2 return $ argEqs ++ motEqs ++ clauseEqs - equate (RecordType fields1 tele1) (RecordType fields2 tele2) = + equate f (RecordType fields1 tele1) (RecordType fields2 tele2) = do unless (fields1 == fields2) $ throwError $ "Record types have different field names: " ++ pretty (In (RecordType fields1 tele1)) @@ -121,8 +121,8 @@ instance MonadUnify TermF Elaborator where ++ pretty (In (RecordType fields1 tele1)) ++ " and " ++ pretty (In (RecordType fields2 tele2)) - return $ zipWith Equation as1 as2 - equate (RecordCon fields1) (RecordCon fields2) = + return $ zipWith (Equation f) as1 as2 + equate f (RecordCon fields1) (RecordCon fields2) = do unless (length fields1 == length fields2) $ throwError $ "Records have different number of fields: " ++ pretty (In (RecordCon fields1)) @@ -136,44 +136,44 @@ instance MonadUnify TermF Elaborator where ++ " and " ++ pretty (In (RecordCon fields2)) return $ zipWith - Equation + (Equation f) (map instantiate0 ms1) (map instantiate0 ms2) - equate (RecordProj r1 x1) (RecordProj r2 x2) = + equate _ (RecordProj r1 x1) (RecordProj r2 x2) = do unless (x1 == x2) $ throwError $ "Record projections have different names: " ++ pretty (In (RecordProj r1 x1)) ++ " and " ++ pretty (In (RecordProj r2 x2)) - return [Equation (instantiate0 r1) (instantiate0 r2)] - equate (QuotedType res1 a1) (QuotedType res2 a2) = + return [Equation False (instantiate0 r1) (instantiate0 r2)] + equate _ (QuotedType res1 a1) (QuotedType res2 a2) = do unless (res1 == res2) $ throwError $ "Quoted types have different reset locations: " ++ pretty (In (QuotedType res1 a1)) ++ " and " ++ pretty (In (QuotedType res2 a2)) - return [Equation (instantiate0 a1) (instantiate0 a2)] - equate (Quote m1) (Quote m2) = - return [Equation (instantiate0 m1) (instantiate0 m2)] - equate (Unquote m1) (Unquote m2) = - return [Equation (instantiate0 m1) (instantiate0 m2)] - equate (Continue m1) (Continue m2) = - return [Equation (instantiate0 m1) (instantiate0 m2)] - equate (Shift res1 m1) (Shift res2 m2) = + return [Equation False (instantiate0 a1) (instantiate0 a2)] + equate _ (Quote m1) (Quote m2) = + return [Equation False (instantiate0 m1) (instantiate0 m2)] + equate _ (Unquote m1) (Unquote m2) = + return [Equation False (instantiate0 m1) (instantiate0 m2)] + equate _ (Continue m1) (Continue m2) = + return [Equation False (instantiate0 m1) (instantiate0 m2)] + equate _ (Shift res1 m1) (Shift res2 m2) = do unless (res1 == res2) $ throwError "Shifts have different reset locations." - return [Equation (instantiate0 m1) (instantiate0 m2)] - equate (Reset res1 m1) (Reset res2 m2) = + return [Equation False (instantiate0 m1) (instantiate0 m2)] + equate _ (Reset res1 m1) (Reset res2 m2) = do unless (res1 == res2) $ throwError "Resets have different reset locations." - return [Equation (instantiate0 m1) (instantiate0 m2)] - equate (Require a1 sc1) (Require a2 sc2) = + return [Equation False (instantiate0 m1) (instantiate0 m2)] + equate _ (Require a1 sc1) (Require a2 sc2) = do ns <- freshRelTo (names sc1) context let xs = map (Var . Free) ns - return [ Equation (instantiate0 a1) (instantiate0 a2) - , Equation (instantiate sc1 xs) (instantiate sc2 xs) + return [ Equation False (instantiate0 a1) (instantiate0 a2) + , Equation False (instantiate sc1 xs) (instantiate sc2 xs) ] - equate l r = + equate _ l r = throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r) @@ -191,7 +191,7 @@ equateCaseMotive mot1@(CaseMotive tele1) mot2@(CaseMotive tele2) = unless (length as1 == length as2) $ throwError $ "Motives not equal: " ++ pretty mot1 ++ " and " ++ pretty mot2 - return $ zipWith Equation as1 as2 ++ [ Equation b1 b2 ] + return $ zipWith (Equation False) as1 as2 ++ [ Equation False b1 b2 ] @@ -216,5 +216,5 @@ equateClause (Clause pscs1 sc1) (Clause pscs2 sc2) = Nothing -> throwError "Patterns are not equal." Just pEqss -> - return $ [ Equation a1 a2 | (a1,a2) <- concat pEqss ] - ++ [ Equation b1 b2 ] \ No newline at end of file + return $ [ Equation False a1 a2 | (a1,a2) <- concat pEqss ] + ++ [ Equation False b1 b2 ] diff --git a/src/Simple/Monadic/Equality.hs b/src/Simple/Monadic/Equality.hs index c4a65f7..b561223 100644 --- a/src/Simple/Monadic/Equality.hs +++ b/src/Simple/Monadic/Equality.hs @@ -22,8 +22,8 @@ import Data.Functor.Classes instance Eq1 TypeF where - eq1 (TyCon c) (TyCon c') = + liftEq _ (TyCon c) (TyCon c') = c == c' - eq1 (Fun a b) (Fun a' b') = - a == a' && b == b' - eq1 _ _ = False \ No newline at end of file + liftEq eq (Fun a b) (Fun a' b') = + eq a a' && eq b b' + liftEq _ _ _ = False diff --git a/src/Simple/Monadic/TypeChecking.hs b/src/Simple/Monadic/TypeChecking.hs index b5faa34..a0d7f18 100644 --- a/src/Simple/Monadic/TypeChecking.hs +++ b/src/Simple/Monadic/TypeChecking.hs @@ -140,7 +140,7 @@ infer (Var (Bound _ _)) = error "A bound variable should never be the subject of type inference." infer (Var (Free x)) = typeInContext x -infer (Var (Meta _)) = +infer (Var (Meta _ _)) = error "Metavariables should not occur in this type checker." infer (In (Defined n)) = typeInDefinitions n @@ -275,7 +275,7 @@ checkPattern (Var (Bound _ _)) _ = error "A bound variable should never be the subject of type checking." checkPattern (Var (Free x)) t = return [(x,t)] -checkPattern (Var (Meta _)) _ = +checkPattern (Var (Meta _ _)) _ = error "Metavariables should not occur in this type checker." checkPattern (In (ConPat c ps)) t = do ConSig args ret <- typeInSignature c diff --git a/src/Simple/Unification/TypeChecking.hs b/src/Simple/Unification/TypeChecking.hs index 96b552f..03ea8d1 100644 --- a/src/Simple/Unification/TypeChecking.hs +++ b/src/Simple/Unification/TypeChecking.hs @@ -142,7 +142,7 @@ inferify (Var (Bound _ _)) = error "A bound variable should never be the subject of type inference." inferify (Var (Free x)) = typeInContext x -inferify (Var (Meta _)) = +inferify (Var (Meta _ _)) = error "Metavariables should not occur in this type checker." inferify (In (Defined x)) = typeInDefinitions x @@ -152,7 +152,7 @@ inferify (In (Ann m t)) = inferify (In (Lam sc)) = do [n] <- freshRelTo (names sc) context meta <- nextElab nextMeta - let arg = Var (Meta meta) + let arg = Var (Meta Exist meta) ret <- extendElab context [(n, arg)] $ inferify (instantiate sc [Var (Free n)]) subs <- getElab substitution @@ -203,7 +203,7 @@ inferifyClause patTys (Clause pscs sc) = xs2 = map (Var . Free) ns ctx' <- forM ns $ \n -> do m <- nextElab nextMeta - return (n,Var (Meta m)) + return (n,Var (Meta Exist m)) extendElab context ctx' $ do zipWithM_ checkifyPattern (map (\psc -> instantiate psc xs1) pscs) @@ -306,7 +306,7 @@ checkifyPattern (Var (Free n)) t = unify substitution context t t' checkifyPattern (Var (Bound _ _)) _ = error "A bound variable should not be the subject of pattern type checking." -checkifyPattern (Var (Meta _)) _ = +checkifyPattern (Var (Meta _ _)) _ = error "A metavariable should not be the subject of pattern type checking." checkifyPattern (In (ConPat c ps)) t = do ConSig args ret <- typeInSignature c diff --git a/src/Simple/Unification/Unification.hs b/src/Simple/Unification/Unification.hs index 5509d75..46a2bb8 100644 --- a/src/Simple/Unification/Unification.hs +++ b/src/Simple/Unification/Unification.hs @@ -31,14 +31,14 @@ import Control.Monad.Except -- | Equating terms by trivial structural equations. instance MonadUnify TypeF Elaborator where - equate (TyCon tycon1) (TyCon tycon2) = + equate _ (TyCon tycon1) (TyCon tycon2) = do unless (tycon1 == tycon2) $ throwError $ "Mismatching type constructors " ++ tycon1 ++ " and " ++ tycon2 return [] - equate (Fun a1 b1) (Fun a2 b2) = - return [ Equation (instantiate0 a1) (instantiate0 a2) - , Equation (instantiate0 b1) (instantiate0 b2) + equate f (Fun a1 b1) (Fun a2 b2) = + return [ Equation f (instantiate0 a1) (instantiate0 a2) + , Equation f (instantiate0 b1) (instantiate0 b2) ] - equate l r = - throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r) \ No newline at end of file + equate _ l r = + throwError $ "Cannot unify " ++ pretty (In l) ++ " with " ++ pretty (In r) diff --git a/src/Utils/ABT.hs b/src/Utils/ABT.hs index ad075a4..633c634 100644 --- a/src/Utils/ABT.hs +++ b/src/Utils/ABT.hs @@ -87,10 +87,12 @@ deriving instance Show (f (Scope f)) => Show (ABT f) -- binder that binds the index. All both have string values that represent the -- stored display name of the variable, for pretty printing. +data MetaType = Exist | Constraint deriving (Show,Eq,Ord) + data Variable = Free FreeVar | Bound String BoundVar - | Meta MetaVar + | Meta MetaType MetaVar deriving (Show) @@ -99,7 +101,7 @@ data Variable name :: Variable -> String name (Free (FreeVar n)) = n name (Bound n _) = n -name (Meta i) = "?" ++ show i +name (Meta _ i) = "?" ++ show i -- | Equality of variables is by the parts which identify them, so names for @@ -108,7 +110,7 @@ name (Meta i) = "?" ++ show i instance Eq Variable where Free x == Free y = x == y Bound _ i == Bound _ j = i == j - Meta m == Meta n = m == n + Meta _ m == Meta _ n = m == n _ == _ = False @@ -659,9 +661,9 @@ freeToDefinedScope d (Scope ns _ b) = substMetas :: (Functor f, Foldable f) => [(MetaVar, ABT f)] -> ABT f -> ABT f substMetas [] x = x -substMetas subs (Var (Meta m)) = +substMetas subs (Var (Meta mt m)) = case lookup m subs of - Nothing -> Var (Meta m) + Nothing -> Var (Meta mt m) Just x -> x substMetas _ (Var v) = Var v @@ -682,7 +684,7 @@ occurs :: (Functor f, Foldable f) => MetaVar -> ABT f -> Bool occurs m x = fold ocAlgV ocAlgRec ocAlgSc x where ocAlgV :: Variable -> Bool - ocAlgV (Meta m') = m == m' + ocAlgV (Meta _ m') = m == m' ocAlgV _ = False ocAlgRec :: Foldable f => f Bool -> Bool @@ -697,7 +699,7 @@ occurs m x = fold ocAlgV ocAlgRec ocAlgSc x metaVars :: (Functor f, Foldable f) => ABT f -> [MetaVar] metaVars = fold mvAlgV mvAlgRec mvAlgSc where - mvAlgV (Meta n) = [n] + mvAlgV (Meta _ n) = [n] mvAlgV _ = [] mvAlgRec :: Foldable f => f [MetaVar] -> [MetaVar] @@ -726,8 +728,15 @@ instance Eq1 f => Eq (Scope f) where +-- needed for Eq1 PatternF instance +liftABTEq :: (f (Scope f) -> g (Scope g) -> Bool) -> ABT f -> ABT g -> Bool +liftABTEq _ (Var x) (Var y) = x == y +liftABTEq eq (In x) (In y) = eq x y +liftABTEq _ _ _ = False - +liftScopeEq :: (ABT f -> ABT g -> Bool) -> Scope f -> Scope g -> Bool +liftScopeEq eq (Scope ns _ x) (Scope ns' _ y) = + length ns == length ns' && eq x y -- * Zipping diff --git a/src/Utils/Telescope.hs b/src/Utils/Telescope.hs index c9d5029..2b73567 100644 --- a/src/Utils/Telescope.hs +++ b/src/Utils/Telescope.hs @@ -35,7 +35,7 @@ data Telescope a instance Eq1 Telescope where - eq1 (Telescope as) (Telescope as') = as == as' + liftEq eq (Telescope as) (Telescope as') = liftEq eq as as' namesTelescope :: Telescope (Scope f) -> [String] @@ -153,8 +153,8 @@ data BindingTelescope a instance Eq1 BindingTelescope where - eq1 (BindingTelescope as b) (BindingTelescope as' b') = - as == as' && b == b' + liftEq eq (BindingTelescope as b) (BindingTelescope as' b') = + liftEq eq as as' && eq b b' namesBindingTelescope :: BindingTelescope (Scope f) -> [String] diff --git a/src/Utils/Unifier.hs b/src/Utils/Unifier.hs index 9e70ab2..4f0f6d1 100644 --- a/src/Utils/Unifier.hs +++ b/src/Utils/Unifier.hs @@ -144,15 +144,15 @@ updateSubstitutionJ subsl ctxl subs = -- | Equations are just pairs of values. -data Equation a = Equation a a +data Equation a = Equation Bool a a -- | Equations can be substituted into, as will be necessary during solving. substMetasEquation :: (Functor f, Foldable f) => Substitution f -> Equation (ABT f) -> Equation (ABT f) -substMetasEquation subs (Equation l r) = - Equation (substMetas subs l) (substMetas subs r) +substMetasEquation subs (Equation f l r) = + Equation f (substMetas subs l) (substMetas subs r) @@ -162,7 +162,8 @@ substMetasEquation subs (Equation l r) = -- ABTs. This involves producing a new set of equations from the input. class Monad m => MonadUnify f m where - equate :: f (Scope f) + equate :: Bool + -> f (Scope f) -> f (Scope f) -> m [Equation (ABT f)] @@ -186,15 +187,20 @@ solve eqs0 = go eqs0 [] go [] subs = return subs - go (Equation (Var (Meta x)) (Var (Meta y)):eqs) subs + go (Equation f (Var (Meta mxt x)) (Var (Meta myt y)):eqs) subs | x == y = go eqs subs - | otherwise = go eqs' subs' + | otherwise = case (f,mxt,myt) of + (False,Constraint,Constraint) -> throwError $ "Cannot unify " ++ show x ++ " with " ++ show y + _ -> go eqs' subs' where - newSubs = [(x, Var (Meta y))] + (x',y') = if mxt <= myt then (x,y) else (y,x) + newSubs = [(x', Var (Meta (max mxt myt) y'))] eqs' = map (substMetasEquation newSubs) eqs subs' = substMetasSubs newSubs (newSubs ++ subs) - - go (Equation v1@(Var (Meta x)) r:eqs) subs = + + go (Equation False v1@(Var (Meta Constraint _)) r:_) _ = + throwError $ "Cannot unify " ++ pretty v1 ++ " with " ++ pretty r + go (Equation _ v1@(Var (Meta _ x)) r:eqs) subs = do unless (not (occurs x r)) $ throwError $ "Cannot unify because " ++ pretty v1 ++ " occurs in " ++ pretty r @@ -203,8 +209,10 @@ solve eqs0 = go eqs0 [] newSubs = [(x,r)] eqs' = map (substMetasEquation newSubs) eqs subs' = substMetasSubs newSubs (newSubs ++ subs) - - go (Equation l v2@(Var (Meta y)):eqs) subs = + + go (Equation False l v2@(Var (Meta Constraint _)):_) _ = + throwError $ "Cannot unify " ++ pretty l ++ " with " ++ pretty v2 + go (Equation _ l v2@(Var (Meta _ y)):eqs) subs = do unless (not (occurs y l)) $ throwError $ "Cannot unify because " ++ pretty v2 ++ " occurs in " ++ pretty l @@ -214,16 +222,16 @@ solve eqs0 = go eqs0 [] eqs' = map (substMetasEquation newSubs) eqs subs' = substMetasSubs newSubs (newSubs ++ subs) - go (Equation v1@(Var x) v2@(Var y):eqs) subs + go (Equation _ v1@(Var x) v2@(Var y):eqs) subs | x == y = go eqs subs | otherwise = throwError $ "Cannot unify variables " ++ pretty v1 ++ " and " ++ pretty v2 - go (Equation (In l) (In r):eqs) subs = - do newEqs <- equate l r + go (Equation f (In l) (In r):eqs) subs = + do newEqs <- equate f l r go (newEqs ++ eqs) subs - go (Equation l r:_) _ = + go (Equation _ l r:_) _ = throwError $ "Cannot unify " ++ pretty l ++ " and " ++ pretty r @@ -243,7 +251,7 @@ unify :: ( Eq a, Functor f, Foldable f, Pretty (ABT f) unify subsl ctxl l r = do newSubs <- catchError - (solve [Equation l r]) + (solve [Equation True l r]) (\e -> throwError $ "Could not unify "++ pretty l ++ " with " ++ pretty r ++ ". " ++ e) @@ -267,7 +275,7 @@ unifyJ :: ( Eq a, Functor f, Foldable f, Pretty (ABT f) unifyJ subsl ctxl l r = do newSubs <- catchError - (solve [Equation l r]) + (solve [Equation True l r]) (\e -> throwError $ "Could not unify "++ pretty l ++ " with " ++ pretty r ++ ". " ++ e) diff --git a/stack.yaml b/stack.yaml new file mode 100644 index 0000000..f87eddc --- /dev/null +++ b/stack.yaml @@ -0,0 +1,35 @@ +# For more information, see: http://docs.haskellstack.org/en/stable/yaml_configuration.html + +# Specifies the GHC version and set of packages available (e.g., lts-3.5, nightly-2015-09-21, ghc-7.10.2) +resolver: lts-8.13 + +# Local packages, usually specified by relative directory name +packages: +- '.' + +# Packages to be pulled from upstream that are not in the resolver (e.g., acme-missiles-0.3) +extra-deps: [] + +# Override default flag values for local packages and extra-deps +flags: {} + +# Extra package databases containing global packages +extra-package-dbs: [] + +# Control whether we use the GHC we find on the path +# system-ghc: true + +# Require a specific version of stack, using version ranges +# require-stack-version: -any # Default +# require-stack-version: >= 1.0.0 + +# Override the architecture used by stack, especially useful on Windows +# arch: i386 +# arch: x86_64 + +# Extra directories used by stack for building +# extra-include-dirs: [/path/to/dir] +# extra-lib-dirs: [/path/to/dir] + +# Allow a newer minor version of GHC than the snapshot specifies +# compiler-check: newer-minor