You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
651 lines
21 KiB
651 lines
21 KiB
{-# LANGUAGE ViewPatterns #-}
|
|
{-# LANGUAGE DeriveAnyClass #-}
|
|
{-# LANGUAGE BlockArguments #-}
|
|
{-# LANGUAGE LambdaCase #-}
|
|
module Eval where
|
|
|
|
import Control.Exception
|
|
|
|
import qualified Data.Map.Strict as Map
|
|
import Data.Foldable
|
|
import Data.Typeable
|
|
import Data.IORef
|
|
import Data.Maybe
|
|
|
|
import GHC.Stack
|
|
|
|
import qualified Presyntax as P
|
|
import Presyntax (Formula)
|
|
|
|
import Syntax
|
|
|
|
import System.IO.Unsafe (unsafePerformIO)
|
|
|
|
import Systems
|
|
import Debug.Trace (traceShowId)
|
|
|
|
iand :: Value -> Value -> Value
|
|
iand = \case
|
|
VI1 -> id
|
|
VI0 -> const VI0
|
|
x -> \case
|
|
VI0 -> VI0
|
|
VI1 -> x
|
|
y -> VIAnd x y
|
|
|
|
ior :: Value -> Value -> Value
|
|
ior = \case
|
|
VI0 -> id
|
|
VI1 -> const VI1
|
|
x -> \case
|
|
VI1 -> VI1
|
|
VI0 -> x
|
|
y -> VIOr x y
|
|
|
|
inot :: Value -> Value
|
|
inot VI1 = VI0
|
|
inot VI0 = VI1
|
|
inot (VIOr x y) = iand (inot x) (inot y)
|
|
inot (VIAnd x y) = ior (inot x) (inot y)
|
|
inot (VINot x) = x
|
|
inot x = VINot x
|
|
|
|
(@@) :: Value -> Value -> Value
|
|
VNe hd xs @@ vl = VNe hd (PApp vl:xs)
|
|
VLam _ _ k @@ vl = k vl
|
|
VEqGlued a b @@ vl = VEqGlued (a @@ vl) (b @@ vl)
|
|
VOfSub (VPi _ _ k) phi u0 x @@ vl = VOfSub (k vl) phi (u0 @@ vl) (x @@ vl)
|
|
VSystem fs @@ vl = mapVSystem (VSystem fs) (@@ vl)
|
|
VIf (VLam s d k) c t b @@ vl = VIf (VLam s d (ap . force . k)) (c @@ vl) (t @@ vl) b where
|
|
ap (VPi _ _ r) = r vl
|
|
ap _ = error "type error when pushing application into if"
|
|
f @@ _ = error $ "\ncan't apply argument to " ++ show f
|
|
|
|
proj1 :: Value -> Value
|
|
proj1 (VPair x _) = x
|
|
proj1 (VEqGlued x y) = VEqGlued (proj1 x) (proj1 y)
|
|
proj1 (VNe s xs) = VNe s (PProj1:xs)
|
|
proj1 (VOfSub (VSigma _ d _) phi u0 x) = VOfSub d phi (proj1 u0) (proj1 x)
|
|
proj1 v@VSystem{} = mapVSystem v proj1
|
|
proj1 (VIf (VLam s d k) c t b) = VIf (VLam s d (proj1t . k)) (proj1 c) (proj1 t) b where
|
|
proj1t (VSigma _ d _) = d
|
|
proj1t _ = error "type error when pushing proj1 into if"
|
|
proj1 x = error $ "can't proj1 " ++ show x
|
|
|
|
proj2 :: Value -> Value
|
|
proj2 (VPair _ y) = y
|
|
proj2 (VEqGlued x y) = VEqGlued (proj2 x) (proj2 y)
|
|
proj2 (VNe s xs) = VNe s (PProj2:xs)
|
|
proj2 (VOfSub (VSigma _ d r) phi u0 x) =
|
|
VOfSub (r (proj1 x)) phi (proj2 u0) (proj2 x)
|
|
proj2 v@VSystem{} = mapVSystem v proj2
|
|
proj2 (VIf (VLam s d k) c t b) = VIf (VLam s d (proj2t . k)) (proj2 c) (proj2 t) b where
|
|
proj2t (VSigma _ d r) = r (VIf (VLam s VBool (const d)) (proj1 c) (proj1 t) b)
|
|
proj2t _ = error "type error when pushing proj1 into if"
|
|
proj2 x = error $ "can't proj2 " ++ show x
|
|
|
|
pathp :: Env -> Value -> Value -> Value -> Value -> Value -> Value
|
|
pathp env p x y f@(VLine _a _x _y e) i =
|
|
case reduceCube env i of
|
|
Just P.Bot -> VEqGlued (e i) x
|
|
Just P.Top -> VEqGlued (e i) y
|
|
_ -> e i
|
|
pathp env p x y (VEqGlued e e') i = VEqGlued (pathp env p x y e i) (pathp env p x y e' i)
|
|
|
|
pathp env p x y (VNe hd sp) i =
|
|
case reduceCube env i of
|
|
Just P.Bot -> VEqGlued (VNe hd (PPathP p x y i:sp)) x
|
|
Just P.Top -> VEqGlued (VNe hd (PPathP p x y i:sp)) y
|
|
_ | quote x == quote y -> VEqGlued (VNe hd (PPathP p x y i:sp)) x
|
|
_ -> VNe hd (PPathP p x y i:sp)
|
|
|
|
pathp env p x y (VOfSub _ _ _ v) i = pathp env p x y v i
|
|
pathp env p x y v@VSystem{} i = mapVSystem v (\f -> pathp env p x y f i)
|
|
pathp env p x y f i = error $ "Invalid pathP " ++ show f ++ " @@ " ++ show i
|
|
|
|
comp :: Env -> Value -> Formula -> Value -> Value -> Value
|
|
comp env a@(VLam ivar VI fam) phi u a0 = glue $ go (fam (VVar "woopsie")) phi u a0 where
|
|
stuck :: Value
|
|
stuck = VComp a (toValue phi) u a0
|
|
|
|
glue :: Value -> Value
|
|
glue = VOfSub (fam VI1) (toValue phi) (u @@ VI1)
|
|
|
|
go :: HasCallStack => Value -> Formula -> Value -> Value -> Value
|
|
go VPi{} phi u a0 =
|
|
let
|
|
dom x = let VPi _ d _ = fam x in d
|
|
rng x = let VPi _ _ r = fam x in r
|
|
|
|
ai1 = dom VI0
|
|
y' i y = fill env i (dom . inot) P.Bot (VSystem emptySystem) y
|
|
ybar i y = y' (inot i) y
|
|
in VLam "x" ai1 \arg ->
|
|
comp env
|
|
(VLam ivar VI (\i -> rng i (ybar i arg)))
|
|
phi
|
|
(VLam "i" VI \i -> mapVSystem (u @@ i) (@@ ybar i arg))
|
|
(a0 @@ ybar VI0 arg)
|
|
|
|
go VSigma{} phi u a0 =
|
|
let
|
|
dom x = let VSigma _ d _ = fam x in d
|
|
rng x = let VSigma _ d _ = fam x in d
|
|
|
|
a i = fill env i (dom . fam) phi (VLam "j" VI \v -> mapVSystem (u @@ v) proj1) (proj1 a0)
|
|
c1 = comp env (VLam ivar VI (getd . fam)) phi (VLam "i" VI \v -> mapVSystem (u @@ v) proj1) (proj1 a0)
|
|
c2 = comp env (VLam ivar VI (apr (a VI1) . fam)) phi (VLam "i" VI \v -> mapVSystem (u @@ v) proj2) (proj2 a0)
|
|
|
|
getd (VSigma _ d _) = d
|
|
apr x (VSigma _ _ r) = r x
|
|
in VPair c1 c2
|
|
|
|
go VPath{} phi p p0 =
|
|
let
|
|
~(VPath ai1 u1 v1) = fam VI1
|
|
~(VPath ai0 u0 v0) = fam VI0
|
|
getA (VPath a _ _) = a
|
|
u' x = let ~(VPath _ u _) = fam x in u
|
|
v' x = let ~(VPath _ _ v) = fam x in v
|
|
in
|
|
VLine (ai1 @@ VI1) u1 v1 \j ->
|
|
let
|
|
jc = reduceCube' env j
|
|
in comp env (VLam ivar VI (getA . fam))
|
|
(orFormula [phi, jc, notFormula jc])
|
|
(VLam "j" VI \v ->
|
|
let
|
|
VSystem (FMap sys) = p @@ v
|
|
sys' = fmap (flip (pathp env ai0 u0 v0) j) sys
|
|
in mkVSystem $ Map.fromList [ (phi, mapVSystem (p @@ v) (flip (pathp env ai0 u0 v0) j))
|
|
, (notFormula jc, u' v)
|
|
, (jc, v' v)
|
|
])
|
|
(pathp env (ai0 @@ VI0) u0 v0 p0 j)
|
|
|
|
go VGlue{} psi b b0 =
|
|
let
|
|
base i = let VGlue base _ _ _ = force $ fam i in base
|
|
phi i =
|
|
case force (fam i) of
|
|
VGlue _ phi _ _ -> fromJust (reduceCube env phi)
|
|
x -> error (show x)
|
|
types i = let VGlue _ _ types _ = force $ fam i in types
|
|
equivs i = let VGlue _ _ _ equivs = force $ fam i in equivs
|
|
|
|
a i = mapVSystem (b @@ i) (unglue (base i) (phi i) (types i) (equivs i))
|
|
a0 = unglue (base VI0) (phi VI0) (types VI0) (equivs VI0) b0
|
|
|
|
del = faceForall phi
|
|
a1' = comp env (VLam "i" VI base) psi (VLam "i" VI a) a0
|
|
t1' = comp env (VLam "i" VI types) psi (VLam "i" VI (b @@)) b0
|
|
omega = pres env types base (flip mapVSystem proj1 . equivs) psi b b0
|
|
t1alpha = opEquiv env (base VI1) (types VI1) (equivs VI1) (orFormula [del, psi]) ts ps a1'
|
|
(t1, alpha) = (proj1 t1alpha, proj2 t1alpha)
|
|
|
|
ts = VSystem (FMap (Map.fromList [(del, t1'), (psi, b @@ VI1)]))
|
|
ps = VSystem (FMap (Map.fromList [(del, omega), (psi, VLine (VLam "j" VI \_ -> base VI1) a1' a1' (\j -> a1'))]))
|
|
|
|
a1 = comp env (VLam "j" VI (const (base VI1))) (orFormula [phi VI1, psi]) (VLam "j" VI \j -> a1_sys j) a1'
|
|
a1_sys j = VSystem (FMap (Map.fromList [(phi VI1, pathp env (base VI1) a1' (mapVSystem (equivs VI1) proj1) alpha j), (psi, a VI1)]))
|
|
b1 = introGlue (base VI1) (phi VI1) (types VI1) (equivs VI1) t1 a1
|
|
in b1
|
|
|
|
go VBool{} _ _ a0 = a0
|
|
go a P.Top u a0 = u @@ VI1
|
|
go a phi u a0 = stuck
|
|
|
|
comp env va phi u a0 =
|
|
if phi == P.Top
|
|
then VEqGlued (VComp va phi' u a0) (u @@ VI1)
|
|
else VComp va phi' u a0
|
|
where
|
|
phi' = toValue phi
|
|
|
|
opEquiv :: Env -> Value -> Value -> Value -> Formula -> Value -> Value -> Value -> Value
|
|
opEquiv env aT tT f phi t p a = VOfSub ty (toValue phi) (VPair t p) v where
|
|
fun = proj1 f
|
|
ty = VSigma "x" tT \x -> VPath (VLam "i" VI (const aT)) a (fun @@ x)
|
|
sys = Map.singleton phi (VPair t p)
|
|
v = contr env ty (proj2 f @@ a) phi (VSystem (FMap sys))
|
|
|
|
force :: Value -> Value
|
|
force (VEqGlued x _) = force x
|
|
force (VOfSub _ _ _ x) = force x
|
|
force x = x
|
|
|
|
faceForall :: (Value -> Formula) -> Formula
|
|
faceForall k = go (k (VVar "$elim")) where
|
|
go (P.Is0 "$elim") = P.Bot
|
|
go (P.Is1 "$elim") = P.Bot
|
|
go (P.Or a b) = orFormula [go a, go b]
|
|
go (P.And a b) = andFormula [go a, go b]
|
|
go x = x
|
|
|
|
pres :: Env -> (Value -> Value) -> (Value -> Value) -> (Value -> Value) -> Formula -> Value -> Value -> Value
|
|
pres env tT tA f phi t t0 = VOfSub (VPath (tA VI1) c1 c2) (toValue phi) base (VLine (tA VI1) c1 c2 cont) where
|
|
c1 = comp env (VLam "i" VI tA) phi (VLam "i" VI \j -> mapVSystem t (f j @@)) (f VI0 @@ t0)
|
|
c2 = f VI1 @@ comp env (VLam "i" VI tA) phi t t0
|
|
base = VLine (tA VI1) (f VI1 @@ (t @@ VI1)) (f VI1 @@ (t @@ VI1)) (\i -> f VI1 @@ (t @@ VI1))
|
|
cont j =
|
|
let v i = fill env i tT phi t t0
|
|
form = orFormula [phi, fromJust (reduceCube env j)]
|
|
a0 = f VI0 @@ t0
|
|
in comp env (VLam "I" VI tA) form
|
|
(VLam "I" VI (\j -> VSystem (FMap (Map.fromList [(form, f j @@ v j)]))))
|
|
a0
|
|
|
|
contr :: Env -> Value -> Value -> Formula -> Value -> Value
|
|
contr env a aC phi u =
|
|
comp env (VLam "i" VI (const a)) phi
|
|
(VLam "i" VI (pathp env a u (proj1 aC) (proj2 aC @@ u)))
|
|
(proj1 aC)
|
|
|
|
-- t : Partial phi T
|
|
-- T : Type
|
|
-- a : A
|
|
-- f : Equiv T A
|
|
|
|
mkVSystem :: Map.Map Formula Value -> Value
|
|
mkVSystem mp
|
|
| Just e <- Map.lookup P.Top mp = e
|
|
| otherwise = VSystem $ FMap $ Map.filterWithKey f mp
|
|
where
|
|
f P.Bot _ = False
|
|
f _ _ = True
|
|
|
|
reduceCube' :: Env -> Value -> Formula
|
|
reduceCube' env = fromJust . reduceCube env
|
|
|
|
mapVSystem :: Value -> (Value -> Value) -> Value
|
|
mapVSystem (VSystem ss) f = VSystem (mapSystem ss f)
|
|
mapVSystem x f = f x
|
|
|
|
evalSystem :: Env -> Map.Map Formula Term -> Value
|
|
evalSystem env face = mk . Map.fromList . mapMaybe (uncurry go) . Map.toList $ face where
|
|
go :: Formula -> Term -> Maybe (Formula, Value)
|
|
go face tm
|
|
| VI0 <- toValue' env face = Nothing
|
|
| otherwise = Just (evalF env face, eval env tm)
|
|
|
|
evalF env tm =
|
|
case toFormula (toValue' env tm) of
|
|
Just f -> f
|
|
Nothing -> error $ "eval turned formula into non formula"
|
|
|
|
mk x = case Map.toList x of
|
|
[(_, x)] -> x
|
|
_ -> mkVSystem x
|
|
|
|
glue :: Value -> Formula -> Value -> Value -> Value
|
|
-- glue baseT P.Top types _equivs = types
|
|
glue baseT phi types equivs = VGlue baseT (toValue phi) types equivs
|
|
|
|
introGlue :: Value -> Formula -> Value -> Value -> Value -> Value -> Value
|
|
introGlue baseT P.Top types equivs t a = t
|
|
introGlue baseT phi types equivs t a = VGlueIntro baseT (toValue phi) types equivs t a
|
|
|
|
unglue :: Value -> Formula -> Value -> Value -> Value -> Value
|
|
unglue baseT P.Top types equivs b = mapVSystem equivs ((@@ b) . proj1)
|
|
unglue baseT phi types equivs val =
|
|
VOfSub baseT (toValue phi) (mapVSystem equivs ((@@ val) . proj1)) (VGlueElim baseT (toValue phi) types equivs val)
|
|
|
|
eval :: Env -> Term -> Value
|
|
eval env = \case
|
|
Var v ->
|
|
case Map.lookup v (names env) of
|
|
Just (_, vl) -> vl
|
|
Nothing -> error $ "variable not in scope: " ++ show v
|
|
|
|
App f x -> eval env f @@ eval env x
|
|
|
|
Lam s d b ->
|
|
let d' = eval env d
|
|
in VLam s d' \a -> eval env{ names = Map.insert s (d', a) (names env) } b
|
|
|
|
Let s t b d ->
|
|
let b' = eval env b
|
|
t' = eval env t
|
|
in eval env{ names = Map.insert s (t', b') (names env) } d
|
|
|
|
Pi s d r ->
|
|
let d' = eval env d
|
|
in VPi s d' \a -> eval env{ names = Map.insert s (d', a) (names env) } r
|
|
|
|
Sigma s d r ->
|
|
let d' = eval env d
|
|
in VSigma s d' \a -> eval env{ names = Map.insert s (d', a) (names env) } r
|
|
|
|
Pair a b -> VPair (eval env a) (eval env b)
|
|
Proj1 x -> proj1 (eval env x)
|
|
Proj2 y -> proj2 (eval env y)
|
|
|
|
Type -> VType
|
|
Typeω -> VTypeω
|
|
|
|
I -> VI
|
|
I0 -> VI0
|
|
I1 -> VI1
|
|
|
|
Path p x y -> VPath (eval env p) (eval env x) (eval env y)
|
|
Partial r a -> VPartial (eval env r) (eval env a)
|
|
PartialP r a -> VPartialP (eval env r) (eval env a)
|
|
|
|
PathI p x y s e -> VLine (eval env p) (eval env x) (eval env y) (\ a -> eval env{ names = Map.insert s (VI, a) (names env) } e)
|
|
PathP p x y f i -> pathp env (eval env p) (eval env x) (eval env y) (eval env f) (eval env i)
|
|
|
|
Sub p x y -> VSub (eval env p) (eval env x) (eval env y)
|
|
InclSub a phi u a0 -> VOfSub (eval env a) (eval env phi) (eval env u) (eval env a0)
|
|
|
|
IAnd x y -> iand (eval env x) (eval env y)
|
|
IOr x y -> ior (eval env x) (eval env y)
|
|
INot x -> inot (eval env x)
|
|
|
|
Comp a phi u a0 ->
|
|
case reduceCube env (eval env phi) of
|
|
Just formula -> comp env (eval env a) formula (eval env u) (eval env a0)
|
|
Nothing -> VComp (eval env a) (eval env phi) (eval env u) (eval env a0)
|
|
|
|
System fs -> evalSystem env (getSystem fs)
|
|
|
|
GlueTy a phi types equivs ->
|
|
let phi' = eval env phi in
|
|
case reduceCube env phi' of
|
|
Just formula -> glue (eval env a) formula (eval env types) (eval env equivs)
|
|
Nothing -> VGlue (eval env a) phi' (eval env types) (eval env equivs)
|
|
|
|
Glue a phi types equivs t a0 ->
|
|
let phi' = eval env phi
|
|
t' = eval env t
|
|
a0' = eval env a0
|
|
types' = eval env types
|
|
equivs' = eval env equivs
|
|
a' = eval env a
|
|
in
|
|
case reduceCube env phi' of
|
|
Just formula -> introGlue a' formula types' equivs' t' a0'
|
|
Nothing -> VGlueIntro a' phi' types' equivs' t' a0'
|
|
|
|
Unglue a phi types equivs val ->
|
|
let phi' = eval env phi
|
|
val' = eval env val
|
|
types' = eval env types
|
|
equivs' = eval env equivs
|
|
a' = eval env a
|
|
in
|
|
case reduceCube env phi' of
|
|
Just formula -> unglue a' formula types' equivs' val'
|
|
Nothing -> VGlueElim a' phi' types' equivs' val'
|
|
|
|
If p x y t -> elimBool (eval env p) (eval env x) (eval env y) (eval env t)
|
|
Tt -> VTrue
|
|
Ff -> VFalse
|
|
Bool -> VBool
|
|
|
|
elimBool :: Value -> Value -> Value -> Value -> Value
|
|
elimBool _ x _ (VEqGlued _ VTrue) = x
|
|
elimBool _ x _ (VOfSub _ _ _ VTrue) = x
|
|
elimBool _ x _ VTrue = x
|
|
|
|
elimBool _ _ y (VEqGlued _ VFalse) = y
|
|
elimBool _ _ y (VOfSub _ _ _ VFalse) = y
|
|
elimBool _ _ y VFalse = y
|
|
|
|
elimBool p x y t = VIf p x y t
|
|
|
|
data UnifyError
|
|
= Mismatch Value Value
|
|
| NotPiType Value
|
|
| NotPartialType Formula Value
|
|
| NotSigmaType Value
|
|
| NotSort Value
|
|
deriving (Show, Typeable, Exception)
|
|
|
|
unify :: HasCallStack => Env -> Value -> Value -> IO ()
|
|
unify env (VEqGlued a b) c =
|
|
unify env a c `catch` \e -> const (unify env b c) (e :: UnifyError)
|
|
unify env c (VEqGlued a b) =
|
|
unify env c a `catch` \e -> const (unify env c b) (e :: UnifyError)
|
|
|
|
unify env (VLine a x y f) e =
|
|
let env' = env { names = Map.insert "i" (VI, VVar "i") (names env) }
|
|
in unify env' (f (VVar "i")) (pathp env' a x y e (VVar "i"))
|
|
unify env e (VLine a x y f) =
|
|
let env' = env { names = Map.insert "i" (VI, VVar "i") (names env) }
|
|
in unify env' (f (VVar "i")) (pathp env' a x y e (VVar "i"))
|
|
|
|
unify env (VPartial r b) (VPartial r' b') = do
|
|
unify env b b'
|
|
case sameCube env r r' of
|
|
Just True -> pure ()
|
|
_ -> unify env r r'
|
|
|
|
unify env (VPartial r b) x = do
|
|
case sameCube env r VI1 of
|
|
Just True -> pure ()
|
|
_ -> unify env r VI1
|
|
unify env b x
|
|
|
|
unify env x (VPartial r b) = do
|
|
case sameCube env r VI1 of
|
|
Just True -> pure ()
|
|
_ -> unify env r VI1
|
|
unify env x b
|
|
|
|
unify env (VSub a phi _u0) vl = unify env a vl
|
|
|
|
unify env u1 (VOfSub _a phi u0 a) = do
|
|
case sameCube env phi VI1 of
|
|
Just True -> unify env u1 u0
|
|
_ -> unify env u1 a
|
|
|
|
unify env (VOfSub _a phi u0 a) u1 = do
|
|
case sameCube env phi VI1 of
|
|
Just True -> unify env u1 u0
|
|
_ -> unify env u1 a
|
|
|
|
unify env vl1@(VNe x sp) vl2@(VNe y sp')
|
|
| x == y = traverse_ (uncurry unifySp) (zip sp sp')
|
|
| otherwise = throwIO $ Mismatch vl1 vl2
|
|
where
|
|
unifySp (PApp x) (PApp y) = unify env x y
|
|
unifySp (PPathP _a _x _y i) (PPathP _a' _x' _y' i') = unify env i i'
|
|
unifySp PProj1 PProj1 = pure ()
|
|
unifySp PProj2 PProj2 = pure ()
|
|
unifySp _ _ = throwIO $ Mismatch vl1 vl2
|
|
|
|
unify env (VLam x _ k) e = unify env (k (VVar x)) (e @@ VVar x)
|
|
unify env e (VLam x _ k) = unify env (e @@ VVar x) (k (VVar x))
|
|
|
|
unify env (VPi x d r) (VPi _ d' r') = do
|
|
unify env d d'
|
|
unify env (r (VVar x)) (r' (VVar x))
|
|
|
|
unify env (VSigma x d r) (VSigma _ d' r') = do
|
|
unify env d d'
|
|
unify env (r (VVar x)) (r' (VVar x))
|
|
|
|
unify env VType VType = pure ()
|
|
unify env VI VI = pure ()
|
|
unify env VBool VBool = pure ()
|
|
|
|
unify env (VPair a b) e = unify env a (proj1 e) *> unify env b (proj2 e)
|
|
unify env e (VPair a b) = unify env a (proj1 e) *> unify env b (proj2 e)
|
|
|
|
unify env (VPath a x y) (VPath a' x' y') = unify env a a' *> unify env x x' *> unify env y y'
|
|
unify env (VComp a phi u a0) (VComp a' phi' u' a0') =
|
|
traverse_ (uncurry (unify env))
|
|
[ (a, a')
|
|
, (phi, phi')
|
|
, (u, u')
|
|
, (a0, a0')
|
|
]
|
|
|
|
unify env (VComp a (reduceCube env -> Just P.Top) u a0) vl =
|
|
unify env (u @@ VI1) vl
|
|
|
|
unify env vl (VComp a (reduceCube env -> Just P.Top) u a0) =
|
|
unify env (u @@ VI1) vl
|
|
|
|
unify env (VSystem fs) vl
|
|
| ((_, vl'):_) <-
|
|
Map.toList (Map.filterWithKey (\f _ -> isTrue (toValue' env f)) (getSystem fs))
|
|
= unify env vl' vl
|
|
| Map.null (getSystem fs) = pure ()
|
|
|
|
unify env vl (VSystem fs)
|
|
| ((_, vl'):_) <-
|
|
Map.toList (Map.filterWithKey (\f _ -> isTrue (toValue' env f)) (getSystem fs))
|
|
= unify env vl' vl
|
|
| Map.null (getSystem fs) = pure ()
|
|
|
|
unify env VType VTypeω = pure ()
|
|
unify env VTypeω VTypeω = pure ()
|
|
|
|
unify env (VGlue _ VI1 b _) x = unify env b x
|
|
|
|
unify env VTrue VTrue = pure ()
|
|
unify env VFalse VFalse = pure ()
|
|
unify env (VIf p a b c) (VIf p' a' b' c') = traverse_ (uncurry (unify env)) [(p, p'), (a, a'), (b, b'), (c, c')]
|
|
|
|
unify env x y =
|
|
case sameCube env x y of
|
|
Just True -> pure ()
|
|
_ -> throwIO $ Mismatch x y
|
|
|
|
reduceCube :: Env -> Value -> Maybe Formula
|
|
reduceCube env x = fmap (toDNF . simplify) (toFormula x) where
|
|
simplify :: Formula -> Formula
|
|
simplify (P.Is0 x) =
|
|
case Map.lookup x (names env) of
|
|
Just (VI, VI0) -> P.Top
|
|
Just (VI, VI1) -> P.Bot
|
|
_ -> P.Is0 x
|
|
simplify (P.Is1 x) =
|
|
case Map.lookup x (names env) of
|
|
Just (VI, VI1) -> P.Top
|
|
Just (VI, VI0) -> P.Bot
|
|
_ -> P.Is1 x
|
|
simplify (P.And x y) = P.And (simplify x) (simplify y)
|
|
simplify (P.Or x y) = P.Or (simplify x) (simplify y)
|
|
simplify x = x
|
|
|
|
sameCube :: Env -> Value -> Value -> Maybe Bool
|
|
sameCube env x y =
|
|
case (reduceCube env x, reduceCube env y) of
|
|
(Just x, Just y) -> Just (x == y)
|
|
_ -> Nothing
|
|
|
|
toFormula :: Value -> Maybe Formula
|
|
toFormula VI0 = Just P.Bot
|
|
toFormula VI1 = Just P.Top
|
|
toFormula (VNe x []) = Just (P.Is1 x)
|
|
toFormula (VINot f) = notFormula <$> toFormula f
|
|
toFormula (VIAnd x y) = do
|
|
s <- toFormula y
|
|
t <- toFormula x
|
|
pure $ andFormula [s, t]
|
|
toFormula (VIOr x y) = do
|
|
s <- toFormula y
|
|
t <- toFormula x
|
|
pure $ orFormula [s, t]
|
|
toFormula _ = Nothing
|
|
|
|
faceInEnv :: Env -> Face -> Bool
|
|
faceInEnv e f = Map.isSubmapOf (getFace f) (faceOfEnv (names e)) where
|
|
faceOfEnv = Map.map (\(_, v) -> case v of { VI1 -> True; VEqGlued _ VI1 -> True; _ -> False }) . Map.filter (\(_, v) -> isI v)
|
|
|
|
isI VI1 = True
|
|
isI VI0 = True
|
|
isI (VEqGlued _ x) = isI x
|
|
isI _ = False
|
|
|
|
isPiType :: Value -> IO (String, Value, Value -> Value)
|
|
isPiType (VPi x d r) = pure (x, d, r)
|
|
isPiType x = throwIO $ NotPiType x
|
|
|
|
isSigmaType :: Value -> IO (String, Value, Value -> Value)
|
|
isSigmaType (VSigma x d r) = pure (x, d, r)
|
|
isSigmaType x = throwIO $ NotSigmaType x
|
|
|
|
isPiOrPathType :: Value -> IO (Either (String, Value, Value -> Value) (Value, Value, Value))
|
|
isPiOrPathType (VPi x d r) = pure (Left (x, d, r))
|
|
isPiOrPathType (VPath x d r) = pure (Right (x, d, r))
|
|
isPiOrPathType x = throwIO $ NotPiType x
|
|
|
|
isPartialType :: Formula -> Value -> IO (Formula, Value)
|
|
isPartialType f p@(VPartial x y) =
|
|
case toFormula x of
|
|
Just x -> pure (x, y)
|
|
Nothing -> throwIO $ NotPartialType f p
|
|
isPartialType f p@(VPartialP x y) =
|
|
case toFormula x of
|
|
Just x -> pure (x, y)
|
|
Nothing -> throwIO $ NotPartialType f p
|
|
isPartialType f x = throwIO $ NotPartialType f x
|
|
|
|
getVar :: IO Value
|
|
getVar =
|
|
do
|
|
n <- atomicModifyIORef ref \x -> (x + 1, x)
|
|
pure (VVar (show n))
|
|
where
|
|
ref :: IORef Int
|
|
ref = unsafePerformIO (newIORef 0)
|
|
{-# NOINLINE ref #-}
|
|
|
|
fill :: Env
|
|
-> Value
|
|
-> (Value -> Value) -- (Γ i : I, A : Type)
|
|
-> Formula -- (phi : I)
|
|
-> Value -- (u : (i : I) -> Partial phi (A i))
|
|
-> Value -- (Sub (A i0) phi (u i0))
|
|
-> Value -- -> A i
|
|
fill env i a phi u a0 =
|
|
comp env
|
|
(VLam "j" VI \j -> a (i `iand` j))
|
|
(phi `P.Or` notFormula ifc)
|
|
(VLam "j" VI \j ->
|
|
mkVSystem (Map.fromList [ (phi, uiand j)
|
|
, (notFormula ifc, a0) ]))
|
|
a0
|
|
where
|
|
uiand j = u @@ (i `iand` j)
|
|
ifc = fromMaybe P.Bot $ (reduceCube env i)
|
|
|
|
toValue :: Formula -> Value
|
|
toValue P.Top = VI1
|
|
toValue P.Bot = VI0
|
|
toValue (P.And x y) = toValue x `iand` toValue y
|
|
toValue (P.Or x y) = toValue x `ior` toValue y
|
|
toValue (P.Is0 x) = inot (VVar x)
|
|
toValue (P.Is1 x) = VVar x
|
|
|
|
toValue' :: HasCallStack => Env -> Formula -> Value
|
|
toValue' env P.Top = VI1
|
|
toValue' env P.Bot = VI0
|
|
toValue' env (P.And x y) = toValue x `iand` toValue y
|
|
toValue' env (P.Or x y) = toValue x `ior` toValue y
|
|
toValue' env (P.Is0 x) =
|
|
case Map.lookup x (names env) of
|
|
Just (VI, VI0) -> VI1
|
|
Just (VI, VI1) -> VI0
|
|
Just (VI, x) -> inot x
|
|
vl -> error $ "type error in toValue' " ++ x ++ ": " ++ show vl
|
|
toValue' env (P.Is1 x) =
|
|
case Map.lookup x (names env) of
|
|
Just (VI, x) -> x
|
|
vl -> error $ "type error in toValue': Is1 " ++ show x ++ ": " ++ show vl
|
|
|
|
isTrue :: Value -> Bool
|
|
isTrue VI1 = True
|
|
isTrue _ = False
|
|
|
|
equiv :: Value -> Value -> Value
|
|
equiv t a = VSigma "f" (VPi "_" t (const a)) \f -> isEquiv t a f
|
|
|
|
isEquiv :: Value -> Value -> Value -> Value
|
|
isEquiv t a f = VPi "y" a \y -> isContr (VSigma "x" t \x -> VPath (VLam "_" VI (const a)) y (f @@ x))
|
|
|
|
isContr :: Value -> Value
|
|
isContr t = VSigma "x" t \x -> VPi "y" t \y -> VPath (VLam "_" VI (const t)) x y
|