|
|
|
@ -13,7 +13,9 @@ import qualified Data.Map.Strict as Map |
|
|
|
import qualified Data.Sequence as Seq |
|
|
|
import qualified Data.Set as Set |
|
|
|
import qualified Data.Text as T |
|
|
|
import Data.Map.Strict (Map) |
|
|
|
import Data.Sequence (Seq) |
|
|
|
import Data.List (sortOn) |
|
|
|
import Data.Traversable |
|
|
|
import Data.Set (Set) |
|
|
|
import Data.Typeable |
|
|
|
@ -21,28 +23,25 @@ import Data.Foldable |
|
|
|
import Data.IORef |
|
|
|
import Data.Maybe |
|
|
|
|
|
|
|
import Elab.Eval.Formula |
|
|
|
import {>n class="err">-# SOURCE #-} Elab.Eval.Formula |
|
|
|
import Elab.Monad |
|
|
|
|
|
|
|
import GHC.Stack |
|
|
|
|
|
|
|
import Presyntax.Presyntax (Plicity(..)) |
|
|
|
|
|
|
|
import Prettyprinter |
|
|
|
|
|
|
|
import Syntax.Pretty |
|
|
|
import Syntax |
|
|
|
|
|
|
|
import System.IO.Unsafe |
|
|
|
import System.IO.Unsafe ( unsafePerformIO ) |
|
|
|
|
|
|
|
import {-# SOURCE #-} Elab.WiredIn |
|
|
|
import Data.List (sortOn) |
|
|
|
import Data.Map.Strict (Map) |
|
|
|
import Debug (traceM, traceDocM) |
|
|
|
import Prettyprinter (pretty, (<+>)) |
|
|
|
|
|
|
|
eval :: Term -> ElabM Value |
|
|
|
eval :: HasCallStack => Term -> ElabM Value |
|
|
|
eval t = asks (flip eval' t) |
|
|
|
|
|
|
|
-- everywhere force |
|
|
|
zonkIO :: Value -> IO Value |
|
|
|
zonkIO (VNe hd sp) = do |
|
|
|
sp' <- traverse zonkSp sp |
|
|
|
@ -64,7 +63,6 @@ zonkIO (VPair a b) = VPair <$> zonkIO a <*> zonkIO b |
|
|
|
zonkIO (VPath line x y) = VPath <$> zonkIO line <*> zonkIO x <*> zonkIO y |
|
|
|
zonkIO (VLine line x y f) = VLine <$> zonkIO line <*> zonkIO x <*> zonkIO y <*> zonkIO f |
|
|
|
|
|
|
|
-- Sorts |
|
|
|
zonkIO VType = pure VType |
|
|
|
zonkIO VTypeω = pure VTypeω |
|
|
|
|
|
|
|
@ -76,37 +74,37 @@ zonkIO (VIAnd x y) = iand <$> zonkIO x <*> zonkIO y |
|
|
|
zonkIO (VIOr x y) = ior <$> zonkIO x <*> zonkIO y |
|
|
|
zonkIO (VINot x) = inot <$> zonkIO x |
|
|
|
|
|
|
|
zonkIO (VIsOne x) = VIsOne <$> zonkIO x |
|
|
|
zonkIO VItIsOne = pure VItIsOne |
|
|
|
|
|
|
|
zonkIO (VPartial x y) = VPartial <$> zonkIO x <*> zonkIO y |
|
|
|
zonkIO (VPartialP x y) = VPartialP <$> zonkIO x <*> zonkIO y |
|
|
|
zonkIO (VSystem fs) = do |
|
|
|
t <- for (Map.toList fs) $ \(a, b) -> (,) <$> zonkIO a <*> zonkIO b |
|
|
|
pure (mkVSystem (Map.fromList t)) |
|
|
|
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 (VHComp a b c d) = hComp <$> zonkIO a <*> zonkIO b <*> zonkIO c <*> zonkIO d |
|
|
|
zonkIO (VInc a b c) = incS <$> zonkIO a <*> zonkIO b <*> zonkIO c |
|
|
|
zonkIO (VComp a b c d) = pure $ VComp a b c d |
|
|
|
zonkIO (VHComp a b c d) = pure $ VHComp a b c 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 |
|
|
|
zonkIO (VCase env t x xs) = do |
|
|
|
env' <- emptyEnv |
|
|
|
evalCase env'{getEnv = env} . (@@) <$> zonkIO t <*> zonkIO x <*> pure xs |
|
|
|
zonkIO (VCase env t x xs) = pure $ VCase env t x xs |
|
|
|
|
|
|
|
zonkIO (VEqStrict a x y) = VEqStrict <$> zonkIO a <*> zonkIO x <*> zonkIO y |
|
|
|
zonkIO (VReflStrict a x) = VReflStrict <$> zonkIO a <*> zonkIO x |
|
|
|
|
|
|
|
zonkSp :: Projection -> IO Projection |
|
|
|
zonkSp (PApp p x) = PApp p <$> zonkIO x |
|
|
|
zonkSp (PIElim l x y i) = PIElim <$> zonkIO l <*> zonkIO x <*> zonkIO y <*> zonkIO i |
|
|
|
zonkSp (POuc a phi u) = POuc <$> zonkIO a <*> zonkIO phi <*> zonkIO u |
|
|
|
zonkSp (PK a x p pr) = PK <$> zonkIO a <*> zonkIO x <*> zonkIO p <*> zonkIO pr |
|
|
|
zonkSp (PJ a x p pr y) = PJ <$> zonkIO a <*> zonkIO x <*> zonkIO p <*> zonkIO pr <*> zonkIO y |
|
|
|
zonkSp PProj1 = pure PProj1 |
|
|
|
zonkSp PProj2 = pure PProj2 |
|
|
|
|
|
|
|
zonk :: Value -> Value |
|
|
|
zonk = unsafePerformIO . zonkIO |
|
|
|
|
|
|
|
eval' :: ElabEnv -> Term -> Value |
|
|
|
eval' :: HasCallStack => ElabEnv -> Term -> Value |
|
|
|
eval' env (Ref x) = |
|
|
|
case Map.lookup x (getEnv env) of |
|
|
|
Just (_, vl) -> vl |
|
|
|
@ -122,23 +120,22 @@ eval' env (PCon sys x) = |
|
|
|
Just (ty, _) -> VNe (HPCon (eval' env sys) ty x) mempty |
|
|
|
Nothing -> error $ "constructor " ++ show x ++ " has no type in scope" |
|
|
|
|
|
|
|
|
|
|
|
eval' _ (Data n x) = VNe (HData n 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 s (error "type of abs", a) (getEnv env) } t |
|
|
|
eval' env { getEnv = Map.insert s (idkT, a) (getEnv env) } t |
|
|
|
|
|
|
|
eval' env (Pi p s d t) = |
|
|
|
VPi p (eval' env d) $ Closure s $ \a -> |
|
|
|
eval' env { getEnv = (Map.insert s (error "type of abs", a) (getEnv env))} t |
|
|
|
eval' env { getEnv = (Map.insert s (idkT, 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 s (error "type of abs", a) (getEnv env) } t |
|
|
|
eval' env { getEnv = Map.insert s (idkT, a) (getEnv env) } t |
|
|
|
|
|
|
|
eval' e (Pair a b) = VPair (eval' e a) (eval' e b) |
|
|
|
|
|
|
|
@ -159,15 +156,12 @@ eval' e (PathP l a b) = VPath (eval' e l) (eval' e a) (eval' e b) |
|
|
|
eval' e (IElim l x y f i) = ielim (eval' e l) (eval' e x) (eval' e y) (eval' e f) (eval' e i) |
|
|
|
eval' e (PathIntro p x y f) = VLine (eval' e p) (eval' e x) (eval' e y) (eval' e f) |
|
|
|
|
|
|
|
eval' e (IsOne i) = VIsOne (eval' e i) |
|
|
|
eval' _ ItIsOne = VItIsOne |
|
|
|
|
|
|
|
eval' e (Partial x y) = VPartial (eval' e x) (eval' e y) |
|
|
|
eval' e (PartialP x y) = VPartialP (eval' e x) (eval' e y) |
|
|
|
eval' e (System fs) = VSystem (Map.fromList $ map (\(x, y) -> (eval' e x, eval' e y)) $ Map.toList $ fs) |
|
|
|
eval' e (System fs) = mkVSystem (Map.fromList $ map (\(x, y) -> (eval' e x, eval' e y)) $ Map.toList $ fs) |
|
|
|
|
|
|
|
eval' e (Sub a phi u) = VSub (eval' e a) (eval' e phi) (eval' e u) |
|
|
|
eval' e (Inc a phi u) = VInc (eval' e a) (eval' e phi) (eval' e u) |
|
|
|
eval' e (Inc a phi u) = incS (eval' e a) (eval' e phi) (eval' e u) |
|
|
|
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) |
|
|
|
@ -177,73 +171,131 @@ eval' e (GlueTy a phi tys f) = glueType (eval' e a) (eval' e phi) (eval' e tys) |
|
|
|
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) |
|
|
|
eval' e (Let ns x) = |
|
|
|
let env' = foldl (\newe (n, ty, x) -> newe { getEnv = Map.insert n (eval' newe ty, eval' newe x) (getEnv newe) }) e ns |
|
|
|
let env' = foldl (\newe (n, ty, x) -> |
|
|
|
let nft = eval' newe ty |
|
|
|
in newe { getEnv = Map.insert n (nft, evalFix' newe n nft x) (getEnv newe) }) |
|
|
|
e |
|
|
|
ns |
|
|
|
in eval' env' x |
|
|
|
|
|
|
|
eval' e (Case range sc xs) = evalCase e (eval' e range @@) (force (eval' e sc)) xs |
|
|
|
|
|
|
|
evalCase :: ElabEnv -> (Value -> Value) -> Value -> [(Term, Term)] -> Value |
|
|
|
evalCase _ _ sc [] = error $ "unmatched pattern for value: " ++ show (prettyTm (quote sc)) |
|
|
|
eval' e (EqS a x y) = VEqStrict (eval' e a) (eval' e x) (eval' e y) |
|
|
|
eval' e (Syntax.Refl a x) = VReflStrict (eval' e a) (eval' e x) |
|
|
|
eval' e (Syntax.AxK a x p pr eq) = strictK (eval' e a) (eval' e x) (eval' e p) (eval' e pr) (eval' e eq) |
|
|
|
eval' e (Syntax.AxJ a x p pr y eq) = strictJ (eval' e a) (eval' e x) (eval' e p) (eval' e pr) (eval' e y) (eval' e eq) |
|
|
|
|
|
|
|
idkT :: NFType |
|
|
|
idkT = VVar (Defined (T.pack "dunno") (negate 1)) |
|
|
|
|
|
|
|
isIdkT :: NFType -> Bool |
|
|
|
isIdkT (VVar (Defined (T.unpack -> "dunno") (negate -> 1))) = True |
|
|
|
isIdkT _ = False |
|
|
|
|
|
|
|
evalCase :: ElabEnv -> (Value -> Value) -> Value -> [(Term, Int, Term)] -> Value |
|
|
|
evalCase env rng sc [] = VCase (getEnv env) (fun rng) sc [] |
|
|
|
|
|
|
|
evalCase env rng (VSystem fs) cases = VSystem (fmap (flip (evalCase env rng) cases) fs) |
|
|
|
|
|
|
|
evalCase env rng (VHComp a phi u a0) cases = |
|
|
|
comp (fun \i -> rng (v i)) phi (system \i is1 -> evalCase env rng (u @@ i @@ is1) cases) |
|
|
|
(VInc (rng a) phi (evalCase env rng (outS a0 phi (u @@ VI0) a0) cases)) |
|
|
|
evalCase env rng (VHComp a φ u u0) cases = |
|
|
|
comp (fun \i -> rng (v i)) |
|
|
|
φ |
|
|
|
(system \i is1 -> α (u @@ i @@ is1)) |
|
|
|
(VInc (rng a) φ (α (outS a φ (u @@ VI0) u0))) |
|
|
|
where |
|
|
|
v = Elab.WiredIn.fill a phi u a0 |
|
|
|
v = Elab.WiredIn.fill (fun (const a)) φ u u0 |
|
|
|
α x = evalCase env rng x cases |
|
|
|
|
|
|
|
evalCase env _ sc ((Ref _, k):_) = eval' env k @@ sc |
|
|
|
evalCase env _ sc ((Ref _, _, k):_) = eval' env k @@ sc |
|
|
|
|
|
|
|
evalCase env rng (val@(VNe (HCon _ x) sp)) ((Con x', k):xs) |
|
|
|
evalCase env rng (force -> val@(VNe (HCon _ x) sp)) ((Con x', _, k):xs) |
|
|
|
| x == x' = foldl applProj (eval' env k) sp |
|
|
|
| otherwise = evalCase env rng val xs |
|
|
|
|
|
|
|
evalCase env rng (val@(VNe (HPCon _ _ x) sp)) ((Con x', k):xs) |
|
|
|
evalCase env rng (force -> val@(VNe (HPCon _ _ x) sp)) ((Con x', _, k):xs) |
|
|
|
| x == x' = foldl applProj (eval' env k) sp |
|
|
|
| otherwise = evalCase env rng val xs |
|
|
|
|
|
|
|
evalCase _ _ (VVar ((== trueCaseSentinel) -> True)) _ = VI1 |
|
|
|
|
|
|
|
evalCase env rng sc xs = VCase (getEnv env) (fun rng) sc xs |
|
|
|
|
|
|
|
-- This is a great big HACK; When we see a system [ case x of ... => p |
|
|
|
-- ], we somehow need to make the 'case x of ...' become VI1. The way we |
|
|
|
-- do this is by substituting x/trueCaseSentinel in truthAssignments, |
|
|
|
-- and then making case trueCaseSentinel of ... => VI1 always. |
|
|
|
trueCaseSentinel :: Name |
|
|
|
trueCaseSentinel = Bound (T.pack "sentinel for true cases") (-1000) |
|
|
|
|
|
|
|
evalFix' :: HasCallStack => ElabEnv -> Name -> NFType -> Term -> Value |
|
|
|
evalFix' env name nft term = fix $ \val -> eval' env{ getEnv = Map.insert name (nft, GluedVl (HVar name) mempty val) (getEnv env) } term |
|
|
|
|
|
|
|
evalFix :: HasCallStack => Name -> NFType -> Term -> ElabM Value |
|
|
|
evalFix name nft term = do |
|
|
|
t <- ask |
|
|
|
pure (evalFix' t name (GluedVl (HVar name) mempty nft) term) |
|
|
|
|
|
|
|
data NotEqual = NotEqual Value Value |
|
|
|
deriving (Show, Typeable, Exception) |
|
|
|
|
|
|
|
unify' :: HasCallStack => Value -> Value -> ElabM () |
|
|
|
unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where |
|
|
|
unify' :: HasCallStack => Bool -> Value -> Value -> ElabM () |
|
|
|
|
|
|
|
unify' cs topa@(GluedVl h sp a) topb@(GluedVl h' sp' b) |
|
|
|
| h == h', length sp == length sp' = |
|
|
|
traverse_ (uncurry (unify'Spine cs topa topb)) (Seq.zip sp sp') |
|
|
|
`catchElab` \(_ :: SomeException) -> unify' cs a b |
|
|
|
|
|
|
|
unify' canSwitch topa topb = join $ go <$> forceIO topa <*> forceIO topb where |
|
|
|
go (VNe (HMeta mv) sp) rhs = solveMeta mv sp rhs |
|
|
|
go rhs (VNe (HMeta mv) sp) = solveMeta mv sp rhs |
|
|
|
|
|
|
|
go (VNe (HPCon s _ _) _) rhs |
|
|
|
| VSystem _ <- s = go (force s) rhs |
|
|
|
go topa@(VNe (HPCon _ _ x) sp) topb@(VNe (HPCon _ _ y) sp') |
|
|
|
| x == y = traverse_ (uncurry (unify'Spine canSwitch topa topb)) (Seq.zip sp sp') |
|
|
|
|
|
|
|
go lhs (VNe (HPCon s _ _) _) |
|
|
|
| VSystem _ <- s = go lhs (force s) |
|
|
|
go (VNe (HPCon s _ _) _) rhs | Just v <- trivialSystem s = go v rhs |
|
|
|
go lhs (VNe (HPCon s _ _) _) | Just v <- trivialSystem s = go lhs v |
|
|
|
|
|
|
|
go (VCase e _ _ b) (VCase e' _ _ b') = do |
|
|
|
env <- ask |
|
|
|
let |
|
|
|
go (_, _, a) (_, _, b) |
|
|
|
| a == b = pure () |
|
|
|
| otherwise = unify' canSwitch (eval' env{getEnv=moreDefinedFrom e e' <$> e} a) (eval' env{getEnv=moreDefinedFrom e e' <$> e'} b) |
|
|
|
zipWithM_ go (sortOn (\(x, _, _) -> x) b) (sortOn (\(x, _, _) -> x) b') |
|
|
|
|
|
|
|
go (VNe x a) (VNe x' a') |
|
|
|
go (VCase e _ _ b) y = do |
|
|
|
env <- ask |
|
|
|
let |
|
|
|
go (_, n, a') = do |
|
|
|
ns <- replicateM n (VVar <$> newName) |
|
|
|
let a = foldl (vApp Ex) (eval' env{getEnv=e} a') ns |
|
|
|
unify' canSwitch a y |
|
|
|
traverse_ go b |
|
|
|
|
|
|
|
go topa@(VNe x a) topb@(VNe x' a') |
|
|
|
| x == x', length a == length a' = |
|
|
|
traverse_ (uncurry unify'Spine) (Seq.zip a a') |
|
|
|
traverse_ (uncurry (unify'Spine canSwitch topa topb)) (Seq.zip a a') |
|
|
|
|
|
|
|
go (VLam p (Closure n k)) vl = do |
|
|
|
t <- VVar <$> newName' n |
|
|
|
unify' (k t) (vApp p vl t) |
|
|
|
unify' canSwitch (k t) (vApp p vl t) |
|
|
|
|
|
|
|
go vl (VLam p (Closure n k)) = do |
|
|
|
t <- VVar <$> newName' n |
|
|
|
unify' (vApp p vl t) (k t) |
|
|
|
unify' canSwitch (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 (VPair a b) vl = unify' canSwitch a (vProj1 vl) *> unify' canSwitch b (vProj2 vl) |
|
|
|
go vl (VPair a b) = unify' canSwitch (vProj1 vl) a *> unify' canSwitch (vProj2 vl) b |
|
|
|
|
|
|
|
go (VPi p d (Closure _ k)) (VPi p' d' (Closure _ k')) | p == p' = do |
|
|
|
t <- VVar <$> newName |
|
|
|
unify' d d' |
|
|
|
unify' (k t) (k' t) |
|
|
|
go (VPi p d (Closure n k)) (VPi p' d' (Closure _ k')) | p == p' = do |
|
|
|
t <- VVar <$> newName' n |
|
|
|
unify' canSwitch d d' |
|
|
|
unify' canSwitch (k t) (k' t) |
|
|
|
|
|
|
|
go (VSigma d (Closure _ k)) (VSigma d' (Closure _ k')) = do |
|
|
|
t <- VVar <$> newName |
|
|
|
unify' d d' |
|
|
|
unify' (k t) (k' t) |
|
|
|
go (VSigma d (Closure n k)) (VSigma d' (Closure _ k')) = do |
|
|
|
t <- VVar <$> newName' n |
|
|
|
unify' canSwitch d d' |
|
|
|
unify' canSwitch (k t) (k' t) |
|
|
|
|
|
|
|
go VType VType = pure () |
|
|
|
go VTypeω VTypeω = pure () |
|
|
|
@ -251,56 +303,63 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where |
|
|
|
go VI VI = pure () |
|
|
|
|
|
|
|
go (VPath l x y) (VPath l' x' y') = do |
|
|
|
unify' l l' |
|
|
|
unify' x x' |
|
|
|
unify' y y' |
|
|
|
unify' canSwitch l l' |
|
|
|
unify' canSwitch x x' |
|
|
|
unify' canSwitch y y' |
|
|
|
|
|
|
|
go (VLine l x y p) p' = do |
|
|
|
n <- VVar <$> newName |
|
|
|
unify' (p @@ n) (ielim l x y p' n) |
|
|
|
n <- VVar <$> newName' (Bound (T.singleton 'i') (- 1)) |
|
|
|
unify' canSwitch (p @@ n) (ielim l x y p' n) |
|
|
|
|
|
|
|
go p' (VLine l x y p) = do |
|
|
|
n <- VVar <$> newName |
|
|
|
unify' (ielim l x y p' n) (p @@ n) |
|
|
|
|
|
|
|
go (VIsOne x) (VIsOne y) = unify' x y |
|
|
|
unify' canSwitch (ielim l x y p' n) (p @@ n) |
|
|
|
|
|
|
|
-- IsOne is proof-irrelevant: |
|
|
|
go VItIsOne _ = pure () |
|
|
|
go _ VItIsOne = pure () |
|
|
|
go (VPartial phi r) (VPartial phi' r') = unify' canSwitch phi phi' *> unify' canSwitch r r' |
|
|
|
go (VPartialP phi r) (VPartialP phi' r') = unify' canSwitch phi phi' *> unify' canSwitch r r' |
|
|
|
|
|
|
|
go (VPartial phi r) (VPartial phi' r') = unify' phi phi' *> unify' r r' |
|
|
|
go (VPartialP phi r) (VPartialP phi' r') = unify' phi phi' *> unify' r r' |
|
|
|
|
|
|
|
go (VSub a phi u) (VSub a' phi' u') = traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u')] |
|
|
|
go (VInc a phi u) (VInc a' phi' u') = traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u')] |
|
|
|
go (VSub a phi u) (VSub a' phi' u') = traverse_ (uncurry (unify' canSwitch)) [(a, a'), (phi, phi'), (u, u')] |
|
|
|
go (VInc a phi u) (VInc a' phi' u') = traverse_ (uncurry (unify' canSwitch)) [(a, a'), (phi, phi'), (u, u')] |
|
|
|
|
|
|
|
go (VComp a phi u a0) (VComp a' phi' u' a0') = |
|
|
|
traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0')] |
|
|
|
traverse_ (uncurry (unify' canSwitch)) [(a, a'), (phi, phi'), (u, u'), (a0, a0')] |
|
|
|
|
|
|
|
go (VHComp a phi u a0) (VHComp a' phi' u' a0') = |
|
|
|
traverse_ (uncurry (unify' canSwitch)) [(a, a'), (phi, phi'), (u, u'), (a0, a0')] |
|
|
|
|
|
|
|
go (VGlueTy _ (force -> VI1) u _0) rhs = unify' (u @@ VItIsOne) rhs |
|
|
|
go lhs (VGlueTy _ (force -> VI1) u _0) = unify' lhs (u @@ VItIsOne) |
|
|
|
go (VGlueTy _ (force -> VI1) u _0) rhs = unify' canSwitch (u @@ VReflStrict VI VI1) rhs |
|
|
|
go lhs (VGlueTy _ (force -> VI1) u _0) = unify' canSwitch lhs (u @@ VReflStrict VI VI1) |
|
|
|
|
|
|
|
go (VGlueTy a phi u a0) (VGlueTy a' phi' u' a0') = |
|
|
|
traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0')] |
|
|
|
traverse_ (uncurry (unify' canSwitch)) [(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')] |
|
|
|
traverse_ (uncurry (unify' canSwitch)) [(a, a'), (phi, phi'), (u, u'), (a0, a0'), (t, t'), (x, x')] |
|
|
|
|
|
|
|
go (VUnglue a phi u a0 x) (VUnglue a' phi' u' a0' x') = |
|
|
|
traverse_ (uncurry (unify' canSwitch)) [(a, a'), (phi, phi'), (u, u'), (a0, a0'), (x, x')] |
|
|
|
|
|
|
|
go (VSystem sys) rhs = goSystem (unify' canSwitch) sys rhs |
|
|
|
go rhs (VSystem sys) = goSystem (flip (unify' canSwitch)) sys rhs |
|
|
|
|
|
|
|
go (VEqStrict a x y) (VEqStrict a' x' y') = traverse_ (uncurry (unify' canSwitch)) [(a, a'), (x, x'), (y, y')] |
|
|
|
go (VReflStrict a x) (VReflStrict a' x') = traverse_ (uncurry (unify' canSwitch)) [(a, a'), (x, x')] |
|
|
|
go _ VReflStrict{} = pure () |
|
|
|
go VReflStrict{} _ = pure () |
|
|
|
|
|
|
|
go (VSystem sys) rhs = goSystem unify' sys rhs |
|
|
|
go rhs (VSystem sys) = goSystem (flip unify') sys rhs |
|
|
|
go (VINot x) (VINot y) = unify' canSwitch x y |
|
|
|
|
|
|
|
go (VCase _ _ a b) (VCase _ _ a' b') = do |
|
|
|
unify' a a' |
|
|
|
let go a b = join $ unify' <$> eval (snd a) <*> eval (snd b) |
|
|
|
zipWithM_ go (sortOn fst b) (sortOn fst b') |
|
|
|
go x y = |
|
|
|
case (toDnf x, toDnf y) of |
|
|
|
(Just xs, Just ys) -> unify'Formula xs ys |
|
|
|
_ -> |
|
|
|
if canSwitch |
|
|
|
then goDumb x y |
|
|
|
else fail |
|
|
|
|
|
|
|
go x y |
|
|
|
| x == y = pure () |
|
|
|
| otherwise = |
|
|
|
case (toDnf x, toDnf y) of |
|
|
|
(Just xs, Just ys) -> unify'Formula xs ys |
|
|
|
_ -> fail |
|
|
|
goDumb (VIOr a b) (VIOr a' b') = unify' canSwitch a a' *> goDumb b b' |
|
|
|
goDumb (VIAnd a b) (VIAnd a' b') = unify' canSwitch a a' *> goDumb b b' |
|
|
|
goDumb x y = switch $ unify' False x y |
|
|
|
|
|
|
|
goSystem :: (Value -> Value -> ElabM ()) -> Map.Map Value Value -> Value -> ElabM () |
|
|
|
goSystem k sys rhs = do |
|
|
|
@ -308,29 +367,58 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where |
|
|
|
env <- ask |
|
|
|
for_ (Map.toList sys) $ \(f, i) -> do |
|
|
|
let i_q = quote i |
|
|
|
for (truthAssignments f (getEnv env)) $ \e -> |
|
|
|
for (truthAssignments f (getEnv env)) $ \e -> do |
|
|
|
k (eval' env{getEnv = e} i_q) (eval' env{getEnv = e} rhs_q) |
|
|
|
|
|
|
|
fail = throwElab $ NotEqual topa topb |
|
|
|
unify'Formula x y |
|
|
|
| compareDNFs x y = pure () |
|
|
|
| otherwise = fail |
|
|
|
|
|
|
|
unify'Spine (PApp a v) (PApp a' v') |
|
|
|
| a == a' = unify' v v' |
|
|
|
moreDefinedFrom :: Map Name (NFType, Value) -> Map Name (NFType, Value) -> (NFType, Value) -> (NFType, Value) |
|
|
|
moreDefinedFrom map1 map2 ours@(_, VNe (HVar name) _) = |
|
|
|
case Map.lookup name map1 of |
|
|
|
Just (_, VNe HVar{} _) -> map2's |
|
|
|
Just (ty, x) -> (ty, x) |
|
|
|
Nothing -> map2's |
|
|
|
where |
|
|
|
map2's = case Map.lookup name map2 of |
|
|
|
Just (_, VNe HVar{} _) -> ours |
|
|
|
Just (ty, x) -> (ty, x) |
|
|
|
Nothing -> ours |
|
|
|
moreDefinedFrom _ _ ours = ours |
|
|
|
|
|
|
|
unify'Spine PProj1 PProj1 = pure () |
|
|
|
unify'Spine PProj2 PProj2 = pure () |
|
|
|
trivialSystem :: Value -> Maybe Value |
|
|
|
trivialSystem = go . force where |
|
|
|
go VSystem{} = Nothing |
|
|
|
go x = Just x |
|
|
|
|
|
|
|
unify'Spine (PIElim _ _ _ i) (PIElim _ _ _ j) = unify' i j |
|
|
|
unify'Spine (POuc a phi u) (POuc a' phi' u') = |
|
|
|
traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u')] |
|
|
|
unify'Spine :: Bool -> Value -> Value -> Projection -> Projection -> ElabM () |
|
|
|
unify'Spine cs _ _ (PApp a v) (PApp a' v') |
|
|
|
| a == a' = unify' cs v v' |
|
|
|
|
|
|
|
unify'Spine _ _ = fail |
|
|
|
unify'Spine _ _ _ PProj1 PProj1 = pure () |
|
|
|
unify'Spine _ _ _ PProj2 PProj2 = pure () |
|
|
|
|
|
|
|
unify'Formula x y |
|
|
|
| compareDNFs x y = pure () |
|
|
|
| otherwise = fail |
|
|
|
unify'Spine cs _ _ (PIElim _ _ _ i) (PIElim _ _ _ j) = unify' cs i j |
|
|
|
unify'Spine cs _ _ (POuc a phi u) (POuc a' phi' u') = |
|
|
|
traverse_ (uncurry (unify' cs)) [(a, a'), (phi, phi'), (u, u')] |
|
|
|
|
|
|
|
unify'Spine cs _ _ (PK a x p pr) (PK a' x' p' pr') = |
|
|
|
traverse_ (uncurry (unify' cs)) [(a, a'), (x, x'), (p, p'), (pr, pr')] |
|
|
|
|
|
|
|
unify'Spine cs _ _ (PJ a x p pr y) (PJ a' x' p' pr' y') = |
|
|
|
traverse_ (uncurry (unify' cs)) [(a, a'), (x, x'), (p, p'), (pr, pr'), (y, y')] |
|
|
|
|
|
|
|
unify'Spine _ x y _ _ = throwElab (NotEqual x y) |
|
|
|
|
|
|
|
unify :: HasCallStack => Value -> Value -> ElabM () |
|
|
|
unify a b = unify' a b `catchElab` \(_ :: SomeException) -> liftIO $ throwIO (NotEqual a b) |
|
|
|
unify x y = shallowly $ go x y where |
|
|
|
go topa@(GluedVl h sp a) topb@(GluedVl h' sp' b) |
|
|
|
| h == h', length sp == length sp' = |
|
|
|
traverse_ (uncurry (unify'Spine True topa topb)) (Seq.zip sp sp') |
|
|
|
`catchElab` \(_ :: SomeException) -> unify' True a b |
|
|
|
go a b = unify' True a b `catchElab` \(_ :: SomeException) -> liftIO $ throwIO (NotEqual a b) |
|
|
|
|
|
|
|
isConvertibleTo :: Value -> Value -> ElabM (Term -> Term) |
|
|
|
isConvertibleTo a b = isConvertibleTo (force a) (force b) where |
|
|
|
@ -348,26 +436,42 @@ isConvertibleTo a b = isConvertibleTo (force a) (force b) where |
|
|
|
wp' <- k (VVar n) `isConvertibleTo` k' (wp_n @@ VVar n) |
|
|
|
pure (\f -> Lam p n (wp' (App p f (wp (Ref n))))) |
|
|
|
|
|
|
|
VPath a x y `isConvertibleTo` VPi Ex d (Closure _ k') = do |
|
|
|
unify d VI |
|
|
|
nm <- newName |
|
|
|
wp <- isConvertibleTo (a @@ VVar nm) (k' (VVar nm)) |
|
|
|
pure (\f -> Lam Ex nm (wp (IElim (quote a) (quote x) (quote y) f (Ref nm)))) |
|
|
|
|
|
|
|
isConvertibleTo a b = do |
|
|
|
unify' a b |
|
|
|
unify' True a b |
|
|
|
pure id |
|
|
|
|
|
|
|
newMeta :: Value -> ElabM Value |
|
|
|
newMeta dom = do |
|
|
|
newMeta' :: Bool -> Value -> ElabM Value |
|
|
|
newMeta' int dom = do |
|
|
|
loc <- liftM2 (,) <$> asks currentFile <*> asks currentSpan |
|
|
|
n <- newName |
|
|
|
c <- liftIO $ newIORef Nothing |
|
|
|
let m = MV (getNameText n) c dom (flatten <$> loc) |
|
|
|
let m = MV (getNameText n) c dom (flatten <$> loc) int |
|
|
|
flatten (x, (y, z)) = (x, y, z) |
|
|
|
|
|
|
|
env <- asks getEnv |
|
|
|
|
|
|
|
t <- for (Map.toList env) $ \(n, _) -> pure $ |
|
|
|
t <- fmap catMaybes . for (Map.toList env) $ \(n, t) -> pure $ |
|
|
|
case n of |
|
|
|
Bound{} -> Just (PApp Ex (VVar n)) |
|
|
|
Bound{} -> Just (PApp Ex (VVar n), n, t) |
|
|
|
_ -> Nothing |
|
|
|
|
|
|
|
pure (VNe (HMeta m) (Seq.fromList (catMaybes t))) |
|
|
|
let |
|
|
|
ts = Map.fromList $ fmap (\(_, n, (t, _)) -> (n, t)) t |
|
|
|
t' = fmap (\(x, _, _) -> x) t |
|
|
|
|
|
|
|
um <- asks unsolvedMetas |
|
|
|
liftIO . atomicModifyIORef um $ \um -> (Map.insert (m ts) [] um, ()) |
|
|
|
|
|
|
|
pure (VNe (HMeta (m ts)) (Seq.fromList t')) |
|
|
|
|
|
|
|
newMeta :: Value -> ElabM Value |
|
|
|
newMeta = newMeta' False |
|
|
|
|
|
|
|
newName :: MonadIO m => m Name |
|
|
|
newName = liftIO $ do |
|
|
|
@ -384,91 +488,103 @@ _nameCounter = unsafePerformIO $ newIORef 0 |
|
|
|
{-# NOINLINE _nameCounter #-} |
|
|
|
|
|
|
|
solveMeta :: MV -> Seq Projection -> Value -> ElabM () |
|
|
|
solveMeta m Seq.Empty (VNe (HMeta m') Seq.Empty) | m == m' = pure () |
|
|
|
solveMeta m@(mvCell -> cell) sp rhs = do |
|
|
|
when (mvName m == T.pack "2801") do |
|
|
|
traceM (VNe (HMeta m) sp) |
|
|
|
traceM rhs |
|
|
|
|
|
|
|
env <- ask |
|
|
|
names <- tryElab $ checkSpine Set.empty sp |
|
|
|
case names of |
|
|
|
Right names -> do |
|
|
|
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 |
|
|
|
liftIO . atomicModifyIORef' cell $ \case |
|
|
|
Just _ -> error "filled cell in solvedMeta" |
|
|
|
Nothing -> (Just lam, ()) |
|
|
|
Left (_ :: SpineProjection) -> do |
|
|
|
scope <- tryElab $ checkScope m (Set.fromList names) rhs |
|
|
|
case scope of |
|
|
|
Right () -> do |
|
|
|
let tm = quote rhs |
|
|
|
lam = eval' env $ foldr (Lam Ex) tm names |
|
|
|
liftIO . atomicModifyIORef (unsolvedMetas env) $ \mp -> (Map.delete m mp, ()) |
|
|
|
liftIO . atomicModifyIORef' cell $ \case |
|
|
|
Just _ -> error "filled cell in solvedMeta" |
|
|
|
Nothing -> (Just lam, ()) |
|
|
|
Left (_ :: MetaException) -> abort env |
|
|
|
Left (_ :: MetaException) -> abort env |
|
|
|
where |
|
|
|
abort env = |
|
|
|
liftIO . atomicModifyIORef' (unsolvedMetas env) $ \x -> (, ()) $ |
|
|
|
case Map.lookup m x of |
|
|
|
Just qs -> Map.insert m ((sp, rhs):qs) x |
|
|
|
Nothing -> Map.insert m [(sp, rhs)] x |
|
|
|
|
|
|
|
checkScope :: Set Name -> Value -> ElabM () |
|
|
|
checkScope scope (VNe h sp) = |
|
|
|
checkScope :: MV -> Set Name -> Value -> ElabM () |
|
|
|
checkScope mv scope (VNe h sp) = |
|
|
|
do |
|
|
|
case h of |
|
|
|
HVar v@Bound{} -> |
|
|
|
unless (v `Set.member` scope) . throwElab $ |
|
|
|
NotInScope v |
|
|
|
ScopeCheckingFail v |
|
|
|
HVar{} -> pure () |
|
|
|
HCon{} -> pure () |
|
|
|
HPCon{} -> pure () |
|
|
|
HMeta{} -> pure () |
|
|
|
HMeta m' -> when (mv == m') $ throwElab $ CircularSolution mv |
|
|
|
HData{} -> pure () |
|
|
|
traverse_ checkProj sp |
|
|
|
where |
|
|
|
checkProj (PApp _ t) = checkScope scope t |
|
|
|
checkProj (PIElim l x y i) = traverse_ (checkScope scope) [l, x, y, i] |
|
|
|
checkProj (POuc a phi u) = traverse_ (checkScope scope) [a, phi, u] |
|
|
|
checkProj (PApp _ t) = checkScope mv scope t |
|
|
|
checkProj (PIElim l x y i) = traverse_ (checkScope mv scope) [l, x, y, i] |
|
|
|
checkProj (PK l x y i) = traverse_ (checkScope mv scope) [l, x, y, i] |
|
|
|
checkProj (PJ l x y i j) = traverse_ (checkScope mv scope) [l, x, y, i, j] |
|
|
|
checkProj (POuc a phi u) = traverse_ (checkScope mv scope) [a, phi, u] |
|
|
|
checkProj PProj1 = pure () |
|
|
|
checkProj PProj2 = pure () |
|
|
|
|
|
|
|
checkScope scope (GluedVl _ _p vl) = checkScope scope vl |
|
|
|
checkScope mv scope (GluedVl _ _p vl) = checkScope mv scope vl |
|
|
|
|
|
|
|
checkScope scope (VLam _ (Closure n k)) = |
|
|
|
checkScope (Set.insert n scope) (k (VVar n)) |
|
|
|
checkScope mv scope (VLam _ (Closure n k)) = |
|
|
|
checkScope mv (Set.insert n scope) (k (VVar n)) |
|
|
|
|
|
|
|
checkScope scope (VPi _ d (Closure n k)) = do |
|
|
|
checkScope scope d |
|
|
|
checkScope (Set.insert n scope) (k (VVar n)) |
|
|
|
checkScope mv scope (VPi _ d (Closure n k)) = do |
|
|
|
checkScope mv scope d |
|
|
|
checkScope mv (Set.insert n scope) (k (VVar n)) |
|
|
|
|
|
|
|
checkScope scope (VSigma d (Closure n k)) = do |
|
|
|
checkScope scope d |
|
|
|
checkScope (Set.insert n scope) (k (VVar n)) |
|
|
|
checkScope mv scope (VSigma d (Closure n k)) = do |
|
|
|
checkScope mv scope d |
|
|
|
checkScope mv (Set.insert n scope) (k (VVar n)) |
|
|
|
|
|
|
|
checkScope s (VPair a b) = traverse_ (checkScope s) [a, b] |
|
|
|
checkScope mv s (VPair a b) = traverse_ (checkScope mv s) [a, b] |
|
|
|
|
|
|
|
checkScope _ VType = pure () |
|
|
|
checkScope _ VTypeω = pure () |
|
|
|
checkScope _ _ VType = pure () |
|
|
|
checkScope _ _ VTypeω = pure () |
|
|
|
|
|
|
|
checkScope _ VI = pure () |
|
|
|
checkScope _ VI0 = pure () |
|
|
|
checkScope _ VI1 = pure () |
|
|
|
checkScope _ _ VI = pure () |
|
|
|
checkScope _ _ VI0 = pure () |
|
|
|
checkScope _ _ VI1 = pure () |
|
|
|
|
|
|
|
checkScope s (VIAnd x y) = traverse_ (checkScope s) [x, y] |
|
|
|
checkScope s (VIOr x y) = traverse_ (checkScope s) [x, y] |
|
|
|
checkScope s (VINot x) = checkScope s x |
|
|
|
checkScope mv s (VIAnd x y) = traverse_ (checkScope mv s) [x, y] |
|
|
|
checkScope mv s (VIOr x y) = traverse_ (checkScope mv s) [x, y] |
|
|
|
checkScope mv s (VINot x) = checkScope mv s x |
|
|
|
|
|
|
|
checkScope s (VPath line a b) = traverse_ (checkScope s) [line, a, b] |
|
|
|
checkScope s (VLine _ _ _ line) = checkScope s line |
|
|
|
checkScope mv s (VPath line a b) = traverse_ (checkScope mv s) [line, a, b] |
|
|
|
checkScope mv s (VLine _ _ _ line) = checkScope mv s line |
|
|
|
|
|
|
|
checkScope s (VIsOne x) = checkScope s x |
|
|
|
checkScope _ VItIsOne = pure () |
|
|
|
checkScope mv s (VPartial x y) = traverse_ (checkScope mv s) [x, y] |
|
|
|
checkScope mv s (VPartialP x y) = traverse_ (checkScope mv s) [x, y] |
|
|
|
checkScope mv s (VSystem fs) = |
|
|
|
for_ (Map.toList fs) $ \(x, y) -> traverse_ (checkScope mv s) [x, y] |
|
|
|
|
|
|
|
checkScope s (VPartial x y) = traverse_ (checkScope s) [x, y] |
|
|
|
checkScope s (VPartialP x y) = traverse_ (checkScope s) [x, y] |
|
|
|
checkScope s (VSystem fs) = |
|
|
|
for_ (Map.toList fs) $ \(x, y) -> traverse_ (checkScope s) [x, y] |
|
|
|
checkScope mv s (VSub a b c) = traverse_ (checkScope mv s) [a, b, c] |
|
|
|
checkScope mv s (VInc a b c) = traverse_ (checkScope mv s) [a, b, c] |
|
|
|
checkScope mv s (VComp a phi u a0) = traverse_ (checkScope mv s) [a, phi, u, a0] |
|
|
|
checkScope mv s (VHComp a phi u a0) = traverse_ (checkScope mv s) [a, phi, u, a0] |
|
|
|
|
|
|
|
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] |
|
|
|
checkScope s (VHComp a phi u a0) = traverse_ (checkScope s) [a, phi, u, a0] |
|
|
|
checkScope mv s (VGlueTy a phi ty eq) = traverse_ (checkScope mv s) [a, phi, ty, eq] |
|
|
|
checkScope mv s (VGlue a phi ty eq inv x) = traverse_ (checkScope mv s) [a, phi, ty, eq, inv, x] |
|
|
|
checkScope mv s (VUnglue a phi ty eq vl) = traverse_ (checkScope mv s) [a, phi, ty, eq, vl] |
|
|
|
|
|
|
|
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] |
|
|
|
checkScope mv s (VCase _ _ v _) = checkScope mv s v |
|
|
|
|
|
|
|
checkScope s (VCase _ _ v _) = checkScope s v |
|
|
|
checkScope mv s (VEqStrict a x y) = traverse_ (checkScope mv s) [a, x, y] |
|
|
|
checkScope mv s (VReflStrict a x) = traverse_ (checkScope mv s) [a, x] |
|
|
|
|
|
|
|
checkSpine :: Set Name -> Seq Projection -> ElabM [Name] |
|
|
|
checkSpine scope (PApp Ex (VVar n@Bound{}) Seq.:<| xs) |
|
|
|
@ -477,10 +593,10 @@ checkSpine scope (PApp Ex (VVar n@Bound{}) Seq.:<| xs) |
|
|
|
checkSpine _ (p Seq.:<| _) = throwElab $ SpineProj p |
|
|
|
checkSpine _ Seq.Empty = pure [] |
|
|
|
|
|
|
|
newtype NonLinearSpine = NonLinearSpine { getDupeName :: Name } |
|
|
|
deriving (Show, Typeable, Exception) |
|
|
|
|
|
|
|
newtype SpineProjection = SpineProj { getSpineProjection :: Projection } |
|
|
|
data MetaException = NonLinearSpine { getDupeName :: Name } |
|
|
|
| SpineProj { getSpineProjection :: Projection } |
|
|
|
| CircularSolution { getCycle :: MV } |
|
|
|
| ScopeCheckingFail { outOfScope :: Name } |
|
|
|
deriving (Show, Typeable, Exception) |
|
|
|
|
|
|
|
substituteIO :: Map.Map Name Value -> Value -> IO Value |
|
|
|
@ -488,15 +604,10 @@ substituteIO sub = substituteIO . force where |
|
|
|
substituteIO (VNe hd sp) = do |
|
|
|
sp' <- traverse (substituteSp sub) sp |
|
|
|
case hd of |
|
|
|
HMeta (mvCell -> cell) -> do |
|
|
|
solved <- liftIO $ readIORef cell |
|
|
|
case solved of |
|
|
|
Just vl -> substituteIO $ foldl applProj vl sp' |
|
|
|
Nothing -> pure $ VNe hd sp' |
|
|
|
HVar v -> |
|
|
|
case Map.lookup v sub of |
|
|
|
Just vl -> substituteIO $ foldl applProj vl sp' |
|
|
|
Nothing -> pure $ VNe hd sp' |
|
|
|
Nothing -> pure $ foldl applProj (VNe hd mempty) sp' |
|
|
|
hd -> pure $ VNe hd sp' |
|
|
|
|
|
|
|
substituteIO (GluedVl h sp vl) = GluedVl h <$> traverse (substituteSp sub) sp <*> substituteIO vl |
|
|
|
@ -509,7 +620,6 @@ substituteIO sub = substituteIO . force where |
|
|
|
substituteIO (VPath line x y) = VPath <$> substituteIO line <*> substituteIO x <*> substituteIO y |
|
|
|
substituteIO (VLine line x y f) = VLine <$> substituteIO line <*> substituteIO x <*> substituteIO y <*> substituteIO f |
|
|
|
|
|
|
|
-- Sorts |
|
|
|
substituteIO VType = pure VType |
|
|
|
substituteIO VTypeω = pure VTypeω |
|
|
|
|
|
|
|
@ -521,16 +631,13 @@ substituteIO sub = substituteIO . force where |
|
|
|
substituteIO (VIOr x y) = ior <$> substituteIO x <*> substituteIO y |
|
|
|
substituteIO (VINot x) = inot <$> substituteIO x |
|
|
|
|
|
|
|
substituteIO (VIsOne x) = VIsOne <$> substituteIO x |
|
|
|
substituteIO VItIsOne = pure VItIsOne |
|
|
|
|
|
|
|
substituteIO (VPartial x y) = VPartial <$> substituteIO x <*> substituteIO y |
|
|
|
substituteIO (VPartialP x y) = VPartialP <$> substituteIO x <*> substituteIO y |
|
|
|
substituteIO (VSystem fs) = do |
|
|
|
t <- for (Map.toList fs) $ \(a, b) -> (,) <$> substituteIO a <*> substituteIO b |
|
|
|
pure (mkVSystem (Map.fromList t)) |
|
|
|
substituteIO (VSub a b c) = VSub <$> substituteIO a <*> substituteIO b <*> substituteIO c |
|
|
|
substituteIO (VInc a b c) = VInc <$> substituteIO a <*> substituteIO b <*> substituteIO c |
|
|
|
substituteIO (VInc a b c) = incS <$> substituteIO a <*> substituteIO b <*> substituteIO c |
|
|
|
substituteIO (VComp a b c d) = comp <$> substituteIO a <*> substituteIO b <*> substituteIO c <*> substituteIO d |
|
|
|
substituteIO (VHComp a b c d) = hComp <$> substituteIO a <*> substituteIO b <*> substituteIO c <*> substituteIO d |
|
|
|
|
|
|
|
@ -538,6 +645,8 @@ substituteIO sub = substituteIO . force where |
|
|
|
substituteIO (VGlue a phi ty e t x) = glueElem <$> substituteIO a <*> substituteIO phi <*> substituteIO ty <*> substituteIO e <*> substituteIO t <*> substituteIO x |
|
|
|
substituteIO (VUnglue a phi ty e x) = unglue <$> substituteIO a <*> substituteIO phi <*> substituteIO ty <*> substituteIO e <*> substituteIO x |
|
|
|
substituteIO (VCase env t x xs) = VCase env <$> substituteIO t <*> substituteIO x <*> pure xs |
|
|
|
substituteIO (VEqStrict a x y) = VEqStrict <$> substituteIO a <*> substituteIO x <*> substituteIO y |
|
|
|
substituteIO (VReflStrict a x) = VReflStrict <$> substituteIO a <*> substituteIO x |
|
|
|
|
|
|
|
substitute :: Map Name Value -> Value -> Value |
|
|
|
substitute sub = unsafePerformIO . substituteIO sub |
|
|
|
@ -545,16 +654,23 @@ substitute sub = unsafePerformIO . substituteIO sub |
|
|
|
substituteSp :: Map Name Value -> Projection -> IO Projection |
|
|
|
substituteSp sub (PApp p x) = PApp p <$> substituteIO sub x |
|
|
|
substituteSp sub (PIElim l x y i) = PIElim <$> substituteIO sub l <*> substituteIO sub x <*> substituteIO sub y <*> substituteIO sub i |
|
|
|
substituteSp sub (PK l x y i) = PK <$> substituteIO sub l <*> substituteIO sub x <*> substituteIO sub y <*> substituteIO sub i |
|
|
|
substituteSp sub (PJ l x y i j) = PJ <$> substituteIO sub l <*> substituteIO sub x <*> substituteIO sub y <*> substituteIO sub i <*> substituteIO sub j |
|
|
|
substituteSp sub (POuc a phi u) = POuc <$> substituteIO sub a <*> substituteIO sub phi <*> substituteIO sub u |
|
|
|
substituteSp _ PProj1 = pure PProj1 |
|
|
|
substituteSp _ PProj2 = pure PProj2 |
|
|
|
|
|
|
|
mkVSystem :: Map.Map Value Value -> Value |
|
|
|
mkVSystem vals = |
|
|
|
let map' = Map.fromList (map (\(a, b) -> (force a, b)) (Map.toList vals)) in |
|
|
|
case Map.lookup VI1 map' of |
|
|
|
let map' = Map.fromList (Map.toList vals >>= go) |
|
|
|
go (x, y) = |
|
|
|
case (force x, y) of |
|
|
|
(VI0, _) -> [] |
|
|
|
(VIOr _ _, VSystem y) -> Map.toList y >>= go |
|
|
|
(a, b) -> [(a, b)] |
|
|
|
in case Map.lookup VI1 map' of |
|
|
|
Just x -> x |
|
|
|
Nothing -> VSystem (Map.filterWithKey (\k _ -> k /= VI0) map') |
|
|
|
Nothing -> VSystem map' |
|
|
|
|
|
|
|
forceIO :: MonadIO m => Value -> m Value |
|
|
|
forceIO mv@(VNe (HMeta (mvCell -> cell)) args) = do |
|
|
|
@ -568,29 +684,35 @@ forceIO vl@(VSystem fs) = |
|
|
|
Nothing -> pure vl |
|
|
|
forceIO (GluedVl _ _ vl) = forceIO vl |
|
|
|
forceIO (VComp line phi u a0) = comp <$> forceIO line <*> forceIO phi <*> pure u <*> pure a0 |
|
|
|
forceIO (VHComp line phi u a0) = hComp <$> forceIO line <*> forceIO phi <*> pure u <*> pure a0 |
|
|
|
forceIO (VCase env rng v vs) = do |
|
|
|
env' <- liftIO emptyEnv |
|
|
|
evalCase env'{getEnv=env} . (@@) <$> forceIO rng <*> forceIO v <*> pure vs |
|
|
|
r <- forceIO rng |
|
|
|
evalCase env'{getEnv=env} (r @@) <$> forceIO v <*> pure vs |
|
|
|
forceIO x = pure x |
|
|
|
|
|
|
|
applProj :: Value -> Projection -> Value |
|
|
|
force :: Value -> Value |
|
|
|
force = unsafePerformIO . forceIO |
|
|
|
|
|
|
|
applProj :: HasCallStack => Value -> Projection -> Value |
|
|
|
applProj fun (PApp p arg) = vApp p fun arg |
|
|
|
applProj fun (PIElim l x y i) = ielim l x y fun i |
|
|
|
applProj fun (POuc a phi u) = outS a phi u fun |
|
|
|
applProj fun (PK a x p pr) = strictK a x p pr fun |
|
|
|
applProj fun (PJ a x p pr y) = strictJ a x p pr y fun |
|
|
|
applProj fun PProj1 = vProj1 fun |
|
|
|
applProj fun PProj2 = vProj2 fun |
|
|
|
|
|
|
|
force :: Value -> Value |
|
|
|
force = unsafePerformIO . forceIO |
|
|
|
|
|
|
|
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 _ (VLam _ k) arg = clCont k arg |
|
|
|
vApp p (VNe (HData True n) _) _ | T.unpack (getNameText n) == "S1" = undefined |
|
|
|
vApp p (VNe h sp) arg = VNe h (sp Seq.:|> PApp p arg) |
|
|
|
vApp p (GluedVl h sp vl) arg = GluedVl h (sp Seq.:|> PApp p arg) (vApp p vl arg) |
|
|
|
vApp p (VSystem fs) arg = VSystem (fmap (flip (vApp p) arg) fs) |
|
|
|
vApp p (VInc (VPi _ _ (Closure _ r)) phi f) arg = VInc (r (vApp p f arg)) phi (vApp p f arg) |
|
|
|
vApp p (VSystem fs) arg = mkVSystem (fmap (flip (vApp p) arg) fs) |
|
|
|
vApp p (VCase env rng sc branches) arg = |
|
|
|
VCase env (fun \x -> let VPi _ _ (Closure _ r) = rng @@ x in r arg) sc |
|
|
|
(map (projIntoCase (flip (App p) (quote arg))) branches) |
|
|
|
-- vApp _ (VLine _ _ _ (VLam _ k)) arg = clCont k arg |
|
|
|
vApp _ x _ = error $ "can't apply " ++ show (prettyTm (quote x)) |
|
|
|
|
|
|
|
(@@) :: HasCallStack => Value -> Value -> Value |
|
|
|
@ -602,13 +724,17 @@ vProj1 (VPair a _) = a |
|
|
|
vProj1 (VNe h sp) = VNe h (sp Seq.:|> PProj1) |
|
|
|
vProj1 (GluedVl h sp vl) = GluedVl h (sp Seq.:|> PProj1) (vProj1 vl) |
|
|
|
vProj1 (VSystem fs) = VSystem (fmap vProj1 fs) |
|
|
|
vProj1 (VInc (VSigma a _) b c) = VInc a b (vProj1 c) |
|
|
|
vProj1 x = error $ "can't proj1 " ++ show (prettyTm (quote x)) |
|
|
|
vProj1 (VInc (VSigma a _) b c) = incS a b (vProj1 c) |
|
|
|
vProj1 (VCase env rng sc branches) = |
|
|
|
VCase env rng sc (map (projIntoCase Proj1) branches) |
|
|
|
vProj1 x = error $ "can't proj1 " ++ show x |
|
|
|
|
|
|
|
vProj2 :: HasCallStack => Value -> Value |
|
|
|
vProj2 (VPair _ b) = b |
|
|
|
vProj2 (VNe h sp) = VNe h (sp Seq.:|> PProj2) |
|
|
|
vProj2 (GluedVl h sp vl) = GluedVl h (sp Seq.:|> PProj2) (vProj2 vl) |
|
|
|
vProj2 (VSystem fs) = VSystem (fmap vProj2 fs) |
|
|
|
vProj2 (VInc (VSigma _ (Closure _ r)) b c) = VInc (r (vProj1 c)) b (vProj2 c) |
|
|
|
vProj2 x = error $ "can't proj2 " ++ show (prettyTm (quote x)) |
|
|
|
vProj2 (VInc (VSigma _ (Closure _ r)) b c) = incS (r (vProj1 c)) b (vProj2 c) |
|
|
|
vProj2 (VCase env rng sc branches) = |
|
|
|
VCase env rng sc (map (projIntoCase Proj2) branches) |
|
|
|
vProj2 x = error $ "can't proj2 " ++ show (prettyTm (quote x)) |
