|
|
|
@ -22,6 +22,8 @@ import Data.Maybe |
|
|
|
import Elab.Eval.Formula |
|
|
|
import Elab.Monad |
|
|
|
|
|
|
|
import GHC.Stack |
|
|
|
|
|
|
|
import Presyntax.Presyntax (Plicity(..)) |
|
|
|
|
|
|
|
import Prettyprinter |
|
|
|
@ -32,17 +34,20 @@ import Syntax |
|
|
|
import System.IO.Unsafe |
|
|
|
|
|
|
|
import {-# SOURCE #-} Elab.WiredIn |
|
|
|
import GHC.Stack |
|
|
|
|
|
|
|
eval :: Term -> ElabM Value |
|
|
|
eval t = asks (flip eval' t) |
|
|
|
|
|
|
|
forceIO :: MonadIO m => Value -> m Value |
|
|
|
forceIO mv@(VNe (HMeta (MV id cell)) args) = do |
|
|
|
forceIO mv@(VNe (HMeta (MV _ cell)) args) = do |
|
|
|
solved <- liftIO $ readIORef cell |
|
|
|
case solved of |
|
|
|
Just vl -> forceIO $ foldl applProj vl args |
|
|
|
Nothing -> pure mv |
|
|
|
forceIO vl@(VSystem fs) = |
|
|
|
case Map.lookup VI1 fs of |
|
|
|
Just x -> forceIO x |
|
|
|
Nothing -> pure vl |
|
|
|
forceIO (VComp line phi u a0) = comp line <$> forceIO phi <*> pure u <*> pure a0 |
|
|
|
forceIO x = pure x |
|
|
|
|
|
|
|
@ -73,6 +78,7 @@ zonkIO (VNe hd sp) = do |
|
|
|
zonkSp (POuc a phi u) = POuc <$> zonkIO a <*> zonkIO phi <*> zonkIO u |
|
|
|
zonkSp PProj1 = pure PProj1 |
|
|
|
zonkSp PProj2 = pure PProj2 |
|
|
|
|
|
|
|
zonkIO (VLam p (Closure s k)) = pure $ VLam p (Closure s (zonk . k)) |
|
|
|
zonkIO (VPi p d (Closure s k)) = VPi p <$> zonkIO d <*> pure (Closure s (zonk . k)) |
|
|
|
zonkIO (VSigma d (Closure s k)) = VSigma <$> zonkIO d <*> pure (Closure s (zonk . k)) |
|
|
|
@ -107,6 +113,10 @@ zonkIO (VSub a b c) = VSub <$> zonkIO a <*> zonkIO b <*> zonkIO c |
|
|
|
zonkIO (VInc a b c) = VInc <$> zonkIO a <*> zonkIO b <*> zonkIO c |
|
|
|
zonkIO (VComp a b c d) = comp <$> zonkIO a <*> zonkIO b <*> zonkIO c <*> zonkIO d |
|
|
|
|
|
|
|
zonkIO (VGlueTy a phi ty e) = glueType <$> zonkIO a <*> zonkIO phi <*> zonkIO ty <*> zonkIO e |
|
|
|
zonkIO (VGlue a phi ty e t x) = glueElem <$> zonkIO a <*> zonkIO phi <*> zonkIO ty <*> zonkIO e <*> zonkIO t <*> zonkIO x |
|
|
|
zonkIO (VUnglue a phi ty e x) = unglue <$> zonkIO a <*> zonkIO phi <*> zonkIO ty <*> zonkIO e <*> zonkIO x |
|
|
|
|
|
|
|
mkVSystem :: Map.Map Value Value -> Value |
|
|
|
mkVSystem map = |
|
|
|
case Map.lookup VI1 map of |
|
|
|
@ -120,22 +130,22 @@ eval' :: ElabEnv -> Term -> Value |
|
|
|
eval' env (Ref x) = |
|
|
|
case Map.lookup x (getEnv env) of |
|
|
|
Just (_, vl) -> vl |
|
|
|
_ -> VVar x |
|
|
|
_ -> VNe (HVar x) mempty |
|
|
|
eval' env (App p f x) = vApp p (eval' env f) (eval' env x) |
|
|
|
|
|
|
|
eval' env (Lam p s t) = |
|
|
|
VLam p $ Closure s $ \a -> |
|
|
|
eval' env { getEnv = Map.insert (Bound s) (error "type of abs", a) (getEnv env) } t |
|
|
|
eval' env { getEnv = Map.insert s (error "type of abs", a) (getEnv env) } t |
|
|
|
|
|
|
|
eval' env (Pi p s d t) = |
|
|
|
VPi p (eval' env d) $ Closure s $ \a -> |
|
|
|
eval' env { getEnv = (Map.insert (Bound s) (error "type of abs", a) (getEnv env))} t |
|
|
|
eval' env { getEnv = (Map.insert s (error "type of abs", a) (getEnv env))} t |
|
|
|
|
|
|
|
eval' _ (Meta m) = VNe (HMeta m) mempty |
|
|
|
|
|
|
|
eval' env (Sigma s d t) = |
|
|
|
VSigma (eval' env d) $ Closure s $ \a -> |
|
|
|
eval' env { getEnv = Map.insert (Bound s) (error "type of abs", a) (getEnv env) } t |
|
|
|
eval' env { getEnv = Map.insert s (error "type of abs", a) (getEnv env) } t |
|
|
|
|
|
|
|
eval' e (Pair a b) = VPair (eval' e a) (eval' e b) |
|
|
|
|
|
|
|
@ -171,29 +181,33 @@ eval' e (Ouc a phi u x) = outS (eval' e a) (eval' e phi) (eval' e u) (eval' e x) |
|
|
|
|
|
|
|
eval' e (Comp a phi u a0) = comp (eval' e a) (eval' e phi) (eval' e u) (eval' e a0) |
|
|
|
|
|
|
|
eval' e (GlueTy a phi tys f) = glueType (eval' e a) (eval' e phi) (eval' e tys) (eval' e f) |
|
|
|
eval' e (Glue a phi tys eqvs t x) = glueElem (eval' e a) (eval' e phi) (eval' e tys) (eval' e eqvs) (eval' e t) (eval' e x) |
|
|
|
eval' e (Unglue a phi tys f x) = unglue (eval' e a) (eval' e phi) (eval' e tys) (eval' e f) (eval' e x) |
|
|
|
|
|
|
|
vApp :: HasCallStack => Plicity -> Value -> Value -> Value |
|
|
|
vApp p (VLam p' k) arg |
|
|
|
| p == p' = clCont k arg |
|
|
|
| otherwise = error $ "wrong plicity " ++ show p ++ " vs " ++ show p' ++ " in app " ++ show (App p (quote (VLam p' k)) (quote arg)) |
|
|
|
vApp p (VNe h sp) arg = VNe h (sp Seq.:|> PApp p arg) |
|
|
|
vApp p (VNe h sp) arg = VNe h (sp Seq.:|> PApp p arg) |
|
|
|
vApp p (VSystem fs) arg = VSystem (fmap (flip (vApp p) arg) fs) |
|
|
|
vApp _ x _ = error $ "can't apply " ++ show x |
|
|
|
vApp _ x _ = error $ "can't apply " ++ show (prettyTm (quote x)) |
|
|
|
|
|
|
|
(@@) :: HasCallStack => Value -> Value -> Value |
|
|
|
(@@) = vApp Ex |
|
|
|
infixl 9 @@ |
|
|
|
|
|
|
|
vProj1 :: Value -> Value |
|
|
|
vProj1 :: HasCallStack => Value -> Value |
|
|
|
vProj1 (VPair a _) = a |
|
|
|
vProj1 (VNe h sp) = VNe h (sp Seq.:|> PProj1) |
|
|
|
vProj1 (VSystem fs) = VSystem (fmap vProj1 fs) |
|
|
|
vProj1 x = error $ "can't proj1 " ++ show x |
|
|
|
vProj1 x = error $ "can't proj1 " ++ show (prettyTm (quote x)) |
|
|
|
|
|
|
|
vProj2 :: Value -> Value |
|
|
|
vProj2 :: HasCallStack => Value -> Value |
|
|
|
vProj2 (VPair _ b) = b |
|
|
|
vProj2 (VNe h sp) = VNe h (sp Seq.:|> PProj2) |
|
|
|
vProj2 (VSystem fs) = VSystem (fmap vProj2 fs) |
|
|
|
vProj2 x = error $ "can't proj2 " ++ show x |
|
|
|
vProj2 x = error $ "can't proj2 " ++ show (prettyTm (quote x)) |
|
|
|
|
|
|
|
data NotEqual = NotEqual Value Value |
|
|
|
deriving (Show, Typeable, Exception) |
|
|
|
@ -206,7 +220,6 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where |
|
|
|
go (VNe x a) (VNe x' a') |
|
|
|
| x == x', length a == length a' = |
|
|
|
traverse_ (uncurry unify'Spine) (Seq.zip a a') |
|
|
|
| x == HVar (Bound (T.pack "y")), x' == HVar (Bound (T.pack "A")) = error "what" |
|
|
|
|
|
|
|
go lhs@(VNe _hd (_ Seq.:|> PIElim _l x y i)) rhs = |
|
|
|
case force i of |
|
|
|
@ -225,23 +238,23 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where |
|
|
|
_ -> fail |
|
|
|
|
|
|
|
go (VLam p (Closure _ k)) vl = do |
|
|
|
t <- VVar . Bound <$> newName |
|
|
|
t <- VVar <$> newName |
|
|
|
unify' (k t) (vApp p vl t) |
|
|
|
|
|
|
|
go vl (VLam p (Closure _ k)) = do |
|
|
|
t <- VVar . Bound <$> newName |
|
|
|
t <- VVar <$> newName |
|
|
|
unify' (vApp p vl t) (k t) |
|
|
|
|
|
|
|
go (VPair a b) vl = unify' a (vProj1 vl) *> unify' b (vProj2 vl) |
|
|
|
go vl (VPair a b) = unify' (vProj1 vl) a *> unify' (vProj2 vl) b |
|
|
|
|
|
|
|
go (VPi p d (Closure _ k)) (VPi p' d' (Closure _ k')) | p == p' = do |
|
|
|
t <- VVar . Bound <$> newName |
|
|
|
t <- VVar <$> newName |
|
|
|
unify' d d' |
|
|
|
unify' (k t) (k' t) |
|
|
|
|
|
|
|
go (VSigma d (Closure _ k)) (VSigma d' (Closure _ k')) = do |
|
|
|
t <- VVar . Bound <$> newName |
|
|
|
t <- VVar <$> newName |
|
|
|
unify' d d' |
|
|
|
unify' (k t) (k' t) |
|
|
|
|
|
|
|
@ -256,11 +269,11 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where |
|
|
|
unify' y y' |
|
|
|
|
|
|
|
go (VLine l x y p) p' = do |
|
|
|
n <- VVar . Bound <$> newName |
|
|
|
n <- VVar <$> newName |
|
|
|
unify (p @@ n) (ielim l x y p' n) |
|
|
|
|
|
|
|
go p' (VLine l x y p) = do |
|
|
|
n <- VVar . Bound <$> newName |
|
|
|
n <- VVar <$> newName |
|
|
|
unify (ielim l x y p' n) (p @@ n) |
|
|
|
|
|
|
|
go (VIsOne x) (VIsOne y) = unify' x y |
|
|
|
@ -282,6 +295,15 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where |
|
|
|
go (VComp a phi u a0) (VComp a' phi' u' a0') = |
|
|
|
traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0')] |
|
|
|
|
|
|
|
go (VGlueTy _ VI1 u _0) rhs = unify' (u @@ VItIsOne) rhs |
|
|
|
go lhs (VGlueTy _ VI1 u _0) = unify' lhs (u @@ VItIsOne) |
|
|
|
|
|
|
|
go (VGlueTy a phi u a0) (VGlueTy a' phi' u' a0') = |
|
|
|
traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0')] |
|
|
|
|
|
|
|
go (VGlue a phi u a0 t x) (VGlue a' phi' u' a0' t' x') = |
|
|
|
traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0'), (t, t'), (x, x')] |
|
|
|
|
|
|
|
go (VSystem sys) rhs = goSystem unify' sys rhs |
|
|
|
go rhs (VSystem sys) = goSystem (flip unify') sys rhs |
|
|
|
|
|
|
|
@ -321,29 +343,30 @@ unify :: HasCallStack => Value -> Value -> ElabM () |
|
|
|
unify a b = unify' a b `catchElab` \(_ :: NotEqual) -> liftIO $ throwIO (NotEqual a b) |
|
|
|
|
|
|
|
isConvertibleTo :: Value -> Value -> ElabM (Term -> Term) |
|
|
|
VPi Im d (Closure _v k) `isConvertibleTo` ty = do |
|
|
|
meta <- newMeta d |
|
|
|
cont <- k meta `isConvertibleTo` ty |
|
|
|
pure (\f -> cont (App Im f (quote meta))) |
|
|
|
VType `isConvertibleTo` VTypeω = pure id |
|
|
|
|
|
|
|
VPi p d (Closure _ k) `isConvertibleTo` VPi p' d' (Closure _ k') | p == p' = do |
|
|
|
wp <- d' `isConvertibleTo` d |
|
|
|
n <- newName |
|
|
|
wp_n <- eval (Lam Ex n (wp (Ref (Bound n)))) |
|
|
|
isConvertibleTo a b = isConvertibleTo (force a) (force b) where |
|
|
|
VPi Im d (Closure _v k) `isConvertibleTo` ty = do |
|
|
|
meta <- newMeta d |
|
|
|
cont <- k meta `isConvertibleTo` ty |
|
|
|
pure (\f -> cont (App Im f (quote meta))) |
|
|
|
VType `isConvertibleTo` VTypeω = pure id |
|
|
|
|
|
|
|
wp' <- k (VVar (Bound n)) `isConvertibleTo` k' (wp_n @@ VVar (Bound n)) |
|
|
|
pure (\f -> Lam p n (wp' (App p f (wp (Ref (Bound n)))))) |
|
|
|
VPi p d (Closure _ k) `isConvertibleTo` VPi p' d' (Closure _ k') | p == p' = do |
|
|
|
wp <- d' `isConvertibleTo` d |
|
|
|
n <- newName |
|
|
|
wp_n <- eval (Lam Ex n (wp (Ref n))) |
|
|
|
|
|
|
|
isConvertibleTo a b = do |
|
|
|
unify' a b |
|
|
|
pure id |
|
|
|
wp' <- k (VVar n) `isConvertibleTo` k' (wp_n @@ VVar n) |
|
|
|
pure (\f -> Lam p n (wp' (App p f (wp (Ref n))))) |
|
|
|
|
|
|
|
isConvertibleTo a b = do |
|
|
|
unify' a b |
|
|
|
pure id |
|
|
|
|
|
|
|
newMeta :: Value -> ElabM Value |
|
|
|
newMeta _dom = do |
|
|
|
n <- newName |
|
|
|
c <- liftIO $ newIORef Nothing |
|
|
|
let m = MV n c |
|
|
|
let m = MV (getNameText n) c |
|
|
|
|
|
|
|
env <- asks getEnv |
|
|
|
|
|
|
|
@ -354,10 +377,10 @@ newMeta _dom = do |
|
|
|
|
|
|
|
pure (VNe (HMeta m) (Seq.fromList (catMaybes t))) |
|
|
|
|
|
|
|
newName :: MonadIO m => m T.Text |
|
|
|
newName :: MonadIO m => m Name |
|
|
|
newName = liftIO $ do |
|
|
|
x <- atomicModifyIORef _nameCounter $ \x -> (x + 1, x + 1) |
|
|
|
pure (T.pack (show x)) |
|
|
|
pure (Bound (T.pack (show x)) x) |
|
|
|
|
|
|
|
_nameCounter :: IORef Int |
|
|
|
_nameCounter = unsafePerformIO $ newIORef 0 |
|
|
|
@ -367,7 +390,7 @@ solveMeta :: MV -> Seq Projection -> Value -> ElabM () |
|
|
|
solveMeta m@(MV _ cell) sp rhs = do |
|
|
|
env <- ask |
|
|
|
names <- checkSpine Set.empty sp |
|
|
|
checkScope (Set.fromList (Bound <$> names)) rhs |
|
|
|
checkScope (Set.fromList names) rhs |
|
|
|
`withNote` hsep [prettyTm (quote (VNe (HMeta m) sp)), pretty '≡', prettyTm (quote rhs)] |
|
|
|
let tm = quote rhs |
|
|
|
lam = eval' env $ foldr (Lam Ex) tm names |
|
|
|
@ -393,15 +416,15 @@ checkScope scope (VNe h sp) = |
|
|
|
checkProj PProj2 = pure () |
|
|
|
|
|
|
|
checkScope scope (VLam _ (Closure n k)) = |
|
|
|
checkScope (Set.insert (Bound n) scope) (k (VVar (Bound n))) |
|
|
|
checkScope (Set.insert n scope) (k (VVar n)) |
|
|
|
|
|
|
|
checkScope scope (VPi _ d (Closure n k)) = do |
|
|
|
checkScope scope d |
|
|
|
checkScope (Set.insert (Bound n) scope) (k (VVar (Bound n))) |
|
|
|
checkScope (Set.insert n scope) (k (VVar n)) |
|
|
|
|
|
|
|
checkScope scope (VSigma d (Closure n k)) = do |
|
|
|
checkScope scope d |
|
|
|
checkScope (Set.insert (Bound n) scope) (k (VVar (Bound n))) |
|
|
|
checkScope (Set.insert n scope) (k (VVar n)) |
|
|
|
|
|
|
|
checkScope s (VPair a b) = traverse_ (checkScope s) [a, b] |
|
|
|
|
|
|
|
@ -433,10 +456,14 @@ checkScope s (VSub a b c) = traverse_ (checkScope s) [a, b, c] |
|
|
|
checkScope s (VInc a b c) = traverse_ (checkScope s) [a, b, c] |
|
|
|
checkScope s (VComp a phi u a0) = traverse_ (checkScope s) [a, phi, u, a0] |
|
|
|
|
|
|
|
checkSpine :: Set Name -> Seq Projection -> ElabM [T.Text] |
|
|
|
checkSpine scope (PApp Ex (VVar n@(Bound t)) Seq.:<| xs) |
|
|
|
checkScope s (VGlueTy a phi ty eq) = traverse_ (checkScope s) [a, phi, ty, eq] |
|
|
|
checkScope s (VGlue a phi ty eq inv x) = traverse_ (checkScope s) [a, phi, ty, eq, inv, x] |
|
|
|
checkScope s (VUnglue a phi ty eq vl) = traverse_ (checkScope s) [a, phi, ty, eq, vl] |
|
|
|
|
|
|
|
checkSpine :: Set Name -> Seq Projection -> ElabM [Name] |
|
|
|
checkSpine scope (PApp Ex (VVar n@Bound{}) Seq.:<| xs) |
|
|
|
| n `Set.member` scope = throwElab $ NonLinearSpine n |
|
|
|
| otherwise = (t:) <$> checkSpine scope xs |
|
|
|
| otherwise = (n:) <$> checkSpine scope xs |
|
|
|
checkSpine _ (p Seq.:<| _) = throwElab $ SpineProj p |
|
|
|
checkSpine _ Seq.Empty = pure [] |
|
|
|
|
|
|
|
@ -444,4 +471,4 @@ newtype NonLinearSpine = NonLinearSpine { getDupeName :: Name } |
|
|
|
deriving (Show, Typeable, Exception) |
|
|
|
|
|
|
|
newtype SpineProjection = SpineProj { getSpineProjection :: Projection } |
|
|
|
deriving (Show, Typeable, Exception) |
|
|
|
deriving (Show, Typeable, Exception) |
