amelia
/
cubical
1
0
Fork 0
Code Issues 0 Pull Requests 0 Projects 0 Releases 0 Wiki Activity
Browse Source

fix composition for the universe

master
Amélia Liao 3 years ago
parent
b4cf411a1b
commit
f745f7357d
7 changed files with 179 additions and 40 deletions
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. +0
    -1
      src/Elab.hs
  2. +140
    -7
      src/Elab/Eval.hs
  3. +33
    -24
      src/Elab/WiredIn.hs
  4. +3
    -3
      src/Elab/WiredIn.hs-boot
  5. +1
    -1
      src/Main.hs
  6. +2
    -2
      src/Syntax.hs
  7. +0
    -2
      src/Syntax/Pretty.hs

+ 0
- 1
src/Elab.hs View File

@ -31,7 +31,6 @@ import Prettyprinter
import Syntax.Pretty
import Syntax
import Syntax.Subst
infer :: P.Expr -> ElabM (Term, NFType)
infer (P.Span ex a b) = withSpan a b $ infer ex


+ 140
- 7
src/Elab/Eval.hs View File

@ -37,12 +37,11 @@ import System.IO.Unsafe
import {-# SOURCE #-} Elab.WiredIn
import Data.List (sortOn)
import Syntax.Subst
import Data.Map.Strict (Map)
eval :: Term -> ElabM Value
eval t = asks (flip eval' t)
-- everywhere force
zonkIO :: Value -> IO Value
zonkIO (VNe hd sp) = do
@ -93,7 +92,9 @@ zonkIO (VHComp a b c d) = hComp <$> zonkIO a <*> zonkIO b <*> zonkIO c <*> zonkI
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 t x xs) = VCase <$> zonkIO t <*> zonkIO x <*> pure xs
zonkIO (VCase env t x xs) = do
env' <- emptyEnv
evalCase env'{getEnv = env} . (@@) <$> zonkIO t <*> zonkIO x <*> pure xs
zonkSp :: Projection -> IO Projection
zonkSp (PApp p x) = PApp p <$> zonkIO x
@ -184,7 +185,9 @@ eval' e (Case range sc xs) = evalCase e (eval' e range @@) (force (eval' e sc))
evalCase :: ElabEnv -> (Value -> Value) -> Value -> [(Term, Term)] -> Value
evalCase _ _ sc [] = error $ "unmatched pattern for value: " ++ show (prettyTm (quote sc))
evalCase env rng (VHComp a phi u a0) cases =
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))
where
@ -200,7 +203,7 @@ evalCase env rng (val@(VNe (HPCon _ _ x) sp)) ((Con x', k):xs)
| x == x' = foldl applProj (eval' env k) sp
| otherwise = evalCase env rng val xs
evalCase _ rng sc xs = VCase (fun rng) sc xs
evalCase env rng sc xs = VCase (getEnv env) (fun rng) sc xs
data NotEqual = NotEqual Value Value
@ -287,7 +290,7 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
go (VSystem sys) rhs = goSystem unify' sys rhs
go rhs (VSystem sys) = goSystem (flip unify') sys rhs
go (VCase _ a b) (VCase _ a' b') = do
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')
@ -465,7 +468,7 @@ 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 s (VCase _ v _) = checkScope s v
checkScope s (VCase _ _ v _) = checkScope s v
checkSpine :: Set Name -> Seq Projection -> ElabM [Name]
checkSpine scope (PApp Ex (VVar n@Bound{}) Seq.:<| xs)
@ -479,3 +482,133 @@ newtype NonLinearSpine = NonLinearSpine { getDupeName :: Name }
newtype SpineProjection = SpineProj { getSpineProjection :: Projection }
deriving (Show, Typeable, Exception)
substituteIO :: Map.Map Name Value -> Value -> IO Value
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'
hd -> pure $ VNe hd sp'
substituteIO (GluedVl h sp vl) = GluedVl h <$> traverse (substituteSp sub) sp <*> substituteIO vl
substituteIO (VLam p (Closure s k)) = pure $ VLam p (Closure s (substitute (Map.delete s sub) . k))
substituteIO (VPi p d (Closure s k)) = VPi p <$> substituteIO d <*> pure (Closure s (substitute (Map.delete s sub) . k))
substituteIO (VSigma d (Closure s k)) = VSigma <$> substituteIO d <*> pure (Closure s (substitute (Map.delete s sub) . k))
substituteIO (VPair a b) = VPair <$> substituteIO a <*> substituteIO b
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ω
substituteIO VI = pure VI
substituteIO VI0 = pure VI0
substituteIO VI1 = pure VI1
substituteIO (VIAnd x y) = iand <$> substituteIO x <*> substituteIO y
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 (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
substituteIO (VGlueTy a phi ty e) = glueType <$> substituteIO a <*> substituteIO phi <*> substituteIO ty <*> substituteIO e
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
substitute :: Map Name Value -> Value -> Value
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 (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
Just x -> x
Nothing -> VSystem (Map.filterWithKey (\k _ -> k /= VI0) map')
forceIO :: MonadIO m => Value -> m Value
forceIO mv@(VNe (HMeta (mvCell -> 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 (GluedVl _ _ vl) = forceIO vl
forceIO (VComp line phi u a0) = comp <$> 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
forceIO x = pure x
applProj :: 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 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 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 _ x _ = error $ "can't apply " ++ show (prettyTm (quote x))
(@@) :: HasCallStack => Value -> Value -> Value
(@@) = vApp Ex
infixl 9 @@
vProj1 :: HasCallStack => Value -> Value
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))
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))

+ 33
- 24
src/Elab/WiredIn.hs View File

@ -25,7 +25,6 @@ import Syntax.Pretty (prettyTm)
import Syntax
import System.IO.Unsafe
import Syntax.Subst
wiType :: WiredIn -> NFType
wiType WiType = VType
@ -94,6 +93,9 @@ fun, line :: (Value -> Value) -> Value
fun k = VLam P.Ex $ Closure (Bound "x" 0) (k . force)
line k = VLam P.Ex $ Closure (Bound "i" 0) (k . force)
fun' :: String -> (Value -> Value) -> Value
fun' x k = VLam P.Ex $ Closure (Bound (T.pack x) 0) (k . force)
forallI :: (Value -> Value) -> Value
forallI k = VLam P.Im $ Closure (Bound "x" 0) (k . force)
@ -196,7 +198,7 @@ ielim line left right fn i =
VNe n sp -> VNe n (sp Seq.:|> PIElim line left right i)
VSystem map -> VSystem (fmap (flip (ielim line left right) i) map)
VInc (VPath _ _ _) _ u -> ielim line left right u i
VCase r x xs -> VCase r x (fmap (fmap (flip (IElim (quote line) (quote left) (quote right)) (quote i))) xs)
VCase env r x xs -> VCase env r x (fmap (fmap (flip (IElim (quote line) (quote left) (quote right)) (quote i))) xs)
_ -> error $ "can't ielim " ++ show (prettyTm (quote fn))
outS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value
@ -207,11 +209,12 @@ outS _ VI0 _ x = x
outS a phi u (GluedVl x sp vl) = GluedVl x (sp Seq.:|> POuc a phi u) (outS a phi u vl)
outS a phi u (VNe x sp) = VNe x (sp Seq.:|> POuc a phi u)
outS a phi u (VSystem fs) = VSystem (fmap (outS a phi u) fs)
outS _ _ _ v = error $ "can't outS " ++ show (prettyTm (quote v))
-- Composition
comp :: NFLine -> NFEndp -> Value -> Value -> Value
comp _a VI1 u _a0 = u @@ VI1 @@ VItIsOne
comp :: HasCallStack => NFLine -> NFEndp -> Value -> Value -> Value
comp _a VI1 u _a0 = u @@ VI1 @@ VItIsOne
comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
case force $ a @@ VVar (Bound (T.pack "i") (negate 1)) of
VPi{} ->
@ -252,28 +255,29 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
, (inot j, u' i)]))
(VInc (a' VI0 @@ VI0 @@ j) phi (ielim (a' VI0 @@ VI0) (u' VI0) (v' VI0) a0 j))
VGlueTy theBase thePhi theTypes theEquivs ->
VGlueTy _ thePhi theTypes theEquivs ->
let
b = u
b0 = a0
fam = a
in
let
base i = substitute (Map.singleton (Bound "i" (negate 1)) i) theBase
base i = let VGlueTy b _ _ _ = forceAndGlue (fam @@ i) in b
phi i = substitute (Map.singleton (Bound "i" (negate 1)) i) thePhi
types i = substitute (Map.singleton (Bound "i" (negate 1)) i) theTypes
types i = substitute (Map.singleton (Bound "i" (negate 1)) i) theTypes @@ VItIsOne
equivs i = substitute (Map.singleton (Bound "i" (negate 1)) i) theEquivs
a i = fun \u -> unglue (base i) (phi i) (types i @@ u) (equivs i @@ u) (b @@ i @@ u)
a i u = unglue (base i) (phi i) (types i @@ u) (equivs i) (b @@ i @@ u)
a0 = unglue (base VI0) (phi VI0) (types VI0) (equivs VI0) b0
del = faceForall phi
a1' = comp (line base) psi (line a) (VInc (base VI0) (phi VI0) a0)
t1' = comp (line types) psi (line (b @@)) (VInc (base VI0) (phi VI0) b0)
a1' = comp (line base) psi (system a) (VInc (base VI0) psi a0)
t1' = comp (line (const (types VI0))) psi (line (b @@)) (VInc (base VI0) psi b0)
(omega_st, omega_t, omega_rep) = pres types base equivs psi (b @@) b0
omega = outS omega_t psi omega_rep omega_st
(t1alpha_st, t1a_t, t1a_rep) = opEquiv (base VI1) (types VI1 @@ VItIsOne) (equivs VI1 @@ VItIsOne) (del `ior` psi) (fun ts) (fun ps) a1'
(t1alpha_st, t1a_t, t1a_rep) = opEquiv (base VI1) (types VI1) (equivs VI1 @@ VItIsOne) (del `ior` psi) (fun ts) (fun ps) a1'
t1alpha = outS t1a_t (del `ior` psi) t1a_rep t1alpha_st
(t1, alpha) = (vProj1 t1alpha, vProj2 t1alpha)
@ -282,17 +286,18 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
ps _isone = mkVSystem . Map.fromList $ [(del, omega), (psi, VLine (line (const (base VI1))) a1' a1' (fun (const a1')))]
a1 = comp
(fun (const (base VI1 @@ VItIsOne)))
(fun (const (base VI1)))
(phi VI1 `ior` psi)
(system \j _u -> mkVSystem (Map.fromList [ (phi VI1, ielim (base VI1) a1' (vProj1 (equivs VI1 @@ VItIsOne)) alpha j)
, (psi, a VI1)]))
a1'
, (psi, a VI1 VItIsOne)]))
(VInc (base VI1) (phi VI1 `ior` psi) a1')
b1 = glueElem (base VI1) (phi VI1) (types VI1) (equivs VI1) (fun (const t1)) a1
in b1
VType -> VGlueTy a0 phi (fun \is1 -> u @@ VI1 @@ is1)
(fun \i -> mapVSystem makeEquiv (u @@ inot i @@ VItIsOne))
VType -> VGlueTy a0 phi (fun' "is1" \is1 -> u @@ VI1 @@ is1)
(fun' "is1" \_ -> mapVSystem makeEquiv (u @@ VVar (Bound (T.pack "_equivLine_") (negate 3)) @@ VItIsOne))
VNe (HData False _) Seq.Empty -> a0
VNe (HData False _) args ->
case force a0 of
VNe (HCon con_type con_name) con_args ->
@ -301,6 +306,9 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
VNe (HData True _) args -> compHIT (length args) (a @@) phi u incA0
VLam{} -> error $ "comp VLam " ++ show (prettyTm (quote a))
sys@VSystem{} -> error $ "comp VSystem: " ++ show (prettyTm (quote sys))
_ -> VComp a phi u (VInc (a @@ VI0) phi a0)
mapVSystem :: (Value -> Value) -> Value -> Value
@ -349,16 +357,16 @@ compConArgs total_args fam = go total_args where
smuggle x = VNe (HData False (Bound "__comp_con_tyarg" (negate 10))) (Seq.singleton (PApp P.Ex x))
compOutS :: NFSort -> NFEndp -> Value -> Value -> Value
compOutS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value
compOutS a b c d = compOutS a b c (force d) where
compOutS _ _hi _0 vl@VComp{} = vl
compOutS _ _hi _0 vl@VComp{} = vl
compOutS _ _hi _0 (VInc _ _ x) = x
compOutS a phi a0 v = outS a phi a0 v
system :: (Value -> Value -> Value) -> Value
system k = VLam P.Ex $ Closure (Bound "i" 0) \i -> VLam P.Ex $ Closure (Bound "phi" 0) \isone -> k i isone
fill :: NFLine -> NFEndp -> Value -> Value -> NFEndp -> Value
fill :: HasCallStack => NFLine -> NFEndp -> Value -> Value -> NFEndp -> Value
fill a phi u a0 j =
comp (line \i -> a @@ (i `iand` j))
(phi `ior` inot j)
@ -377,7 +385,7 @@ glueElem :: NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value ->
glueElem _a (force -> VI1) _tys _eqvs t _vl = t @@ VItIsOne
glueElem a phi tys eqvs t vl = VGlue a phi tys eqvs t vl
unglue :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
unglue :: HasCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
unglue _a (force -> VI1) _tys eqvs x = vProj1 (eqvs @@ VItIsOne) @@ x
unglue _a _phi _tys _eqvs (force -> VGlue _ _ _ _ _ vl) = vl
unglue a phi tys eqvs (force -> VSystem fs) = VSystem (fmap (unglue a phi tys eqvs) fs)
@ -434,21 +442,22 @@ contr a aC phi u =
comp (line (const a))
phi
(system \i is1 -> ielim (line (const a)) (vProj1 aC) (u is1) (vProj2 aC @@ u is1) i)
(vProj1 aC)
(VInc a phi (vProj1 aC))
transp :: (NFEndp -> Value) -> Value -> Value
transp line a0 = comp (fun line) VI0 (system \_ _ -> VSystem mempty) (VInc (line VI0) VI0 a0)
makeEquiv :: Value -> Value
makeEquiv line = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vProj2 u) y)
makeEquiv argh = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vProj2 u) y)
where
line = fun \i -> substitute (Map.singleton (Bound (T.pack "_equivLine_") (negate 3)) (inot i)) argh
a = line @@ VI0
b = line @@ VI1
f = fun \x -> transp (line @@) x
g = fun \x -> transp ((line @@) . inot) x
u i = fun \x -> fill line VI0 (system \_ _ -> mkVSystem mempty) x i
v i = fun \x -> fill (fun ((line @@) . inot)) VI0 (system \_ _ -> mkVSystem mempty) x i
u i = fun \x -> fill line VI0 (system \_ _ -> mkVSystem mempty) (VInc a VI0 x) i
v i = fun \x -> fill (fun ((line @@) . inot)) VI0 (system \_ _ -> mkVSystem mempty) (VInc a VI1 x) (inot i)
fib y = VPair (g @@ y) (VLine b y (f @@ (g @@ y)) (fun (theta0 y VI1)))
theta0 y i j = fill line (ior j (inot j)) (system \i _ -> mkVSystem (Map.fromList [(j, v i @@ y), (inot j, u i @@ (g @@ y))])) (VInc a (ior j (inot j)) (g @@ y)) i


+ 3
- 3
src/Elab/WiredIn.hs-boot View File

@ -12,13 +12,13 @@ inot :: NFEndp -> NFEndp
ielim :: NFSort -> Value -> Value -> Value -> NFEndp -> Value
outS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value
comp :: NFLine -> NFEndp -> Value -> Value -> Value
fill :: NFLine -> NFEndp -> Value -> Value -> Value -> Value
comp :: HasCallStack => NFLine -> NFEndp -> Value -> Value -> Value
fill :: HasCallStack => NFLine -> NFEndp -> Value -> Value -> Value -> Value
hComp :: NFSort -> NFEndp -> Value -> Value -> Value
glueType :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
glueElem :: NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
unglue :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
unglue :: HasCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
fun :: (Value -> Value) -> Value
system :: (Value -> Value -> Value) -> Value

+ 1
- 1
src/Main.hs View File

@ -53,7 +53,7 @@ main = do
Check files verbose -> do
env <- checkFiles files
when verbose $ dumpEnv env
Repl -> enterReplIn =<< checkFiles ["./intro.tt"]
Repl -> enterReplIn =<< checkFiles ["./test.tt"]
enterReplIn :: ElabEnv -> IO ()
enterReplIn env = runInputT defaultSettings (loop env') where


+ 2
- 2
src/Syntax.hs View File

@ -176,7 +176,7 @@ data Value
| VGlue NFSort NFEndp NFPartial NFPartial NFPartial Value
| VUnglue NFSort NFEndp NFPartial NFPartial Value
| VCase Value Value [(Term, Term)]
| VCase (Map.Map Name (NFType, Value)) Value Value [(Term, Term)]
deriving (Eq, Show, Ord)
pattern VVar :: Name -> Value
@ -256,7 +256,7 @@ quoteWith names (VGlueTy a phi t e) = GlueTy (quoteWith names a) (quoteWith n
quoteWith names (VGlue a phi ty e t x) = Glue (quoteWith names a) (quoteWith names phi) (quoteWith names ty) (quoteWith names e) (quoteWith names t) (quoteWith names x)
quoteWith names (VUnglue a phi ty e x) = Unglue (quoteWith names a) (quoteWith names phi) (quoteWith names ty) (quoteWith names e) (quoteWith names x)
quoteWith names (VCase rng v xs) = Case (quoteWith names rng) (quoteWith names v) xs
quoteWith names (VCase _ rng v xs) = Case (quoteWith names rng) (quoteWith names v) xs
alwaysShort :: Value -> Bool
alwaysShort (VNe HCon{} _) = True


+ 0
- 2
src/Syntax/Pretty.hs View File

@ -114,8 +114,6 @@ prettyTm = prettyTm . everywhere (mkT beautify) where
beautify (Inc _ _ u) = toFun "inS" [u]
beautify (Ouc a phi u u0) = toFun "outS" [a, phi, u, u0]
beautify (GlueTy a I1 _ _) = a
beautify (GlueTy a b c d) = toFun "Glue" [a,b,c,d]
beautify (Glue a b c d e f) = toFun "glue" [a,b,c,d,e,f]


Write Preview
Loading…
Cancel
Save