Browse Source

more pain and suffering

feature/hits
Amélia Liao 3 years ago
parent
commit
f695f9bcc2
9 changed files with 94 additions and 105 deletions
  1. +9
    -0
      intro.tt
  2. +12
    -6
      src/Elab.hs
  3. +2
    -61
      src/Elab/Eval.hs
  4. +52
    -27
      src/Elab/WiredIn.hs
  5. +2
    -1
      src/Elab/WiredIn.hs-boot
  6. +5
    -5
      src/Presyntax/Parser.y
  7. +1
    -1
      src/Presyntax/Presyntax.hs
  8. +2
    -2
      src/Syntax.hs
  9. +9
    -2
      src/Syntax/Pretty.hs

+ 9
- 0
intro.tt View File

@ -293,6 +293,12 @@ transpFun : {A : Type} {B : Type} {C : Type} {D : Type} (p : Path A B) (q : Path
(\x -> transp (\i -> q i) (f (transp (\i -> p (inot i)) x))) (\x -> transp (\i -> q i) (f (transp (\i -> p (inot i)) x)))
transpFun p q f = refl transpFun p q f = refl
-- transpDFun : {A : I -> Type} {B : (i : I) -> A i -> Type}
-- -> (f : (x : A i0) -> B i0 x)
-- -> Path (transp (\i -> (x : A i) -> B i x) f)
-- (\x -> transp (\i -> B i (fill (\j -> A (inot j)) (\k []) (inS x) (inot i))) (f (fill (\j -> A (inot j)) (\k []) (inS x) i1)))
-- transpDFun f = refl
-- When considering the more general case of a composition respecing sides, -- When considering the more general case of a composition respecing sides,
-- the outer transport becomes a composition. -- the outer transport becomes a composition.
@ -326,6 +332,9 @@ inverse eqv y = (eqv y) .1 .1
section : {A : Type} {B : Type} (f : A -> B) (eqv : isEquiv f) -> Path (\x -> f (inverse eqv x)) id section : {A : Type} {B : Type} (f : A -> B) (eqv : isEquiv f) -> Path (\x -> f (inverse eqv x)) id
section f eqv i y = (eqv y) .1 .2 i section f eqv i y = (eqv y) .1 .2 i
contr : {A : Type} {phi : I} -> isContr A -> (u : Partial phi A) -> A
contr {A} {phi} p u = comp (\i -> A) {phi} (\i is1 -> p.2 (u is1) i) (inS (p.1))
-- Proving that it's also a retraction is left as an exercise to the -- Proving that it's also a retraction is left as an exercise to the
-- reader. We can package together a function and a proof that it's an -- reader. We can package together a function and a proof that it's an
-- equivalence to get a capital-E Equivalence. -- equivalence to get a capital-E Equivalence.


+ 12
- 6
src/Elab.hs View File

@ -31,7 +31,7 @@ import Prettyprinter
import Syntax.Pretty import Syntax.Pretty
import Syntax import Syntax
import Debug.Trace
import Syntax.Subst
infer :: P.Expr -> ElabM (Term, NFType) infer :: P.Expr -> ElabM (Term, NFType)
infer (P.Span ex a b) = withSpan a b $ infer ex infer (P.Span ex a b) = withSpan a b $ infer ex
@ -516,7 +516,7 @@ checkStatement (P.Data name tele retk constrs) k =
markAsDef x e = e { definedNames = Set.insert x (definedNames e) } markAsDef x e = e { definedNames = Set.insert x (definedNames e) }
mkHead name mkHead name
| any (\case { P.Path{} -> True; _ -> False}) constrs = HData True name
| any (\case { (_, _, P.Path{}) -> True; _ -> False}) constrs = HData True name
| otherwise = HData False name | otherwise = HData False name
checkTeleRetk allKan [] retk cont = do checkTeleRetk allKan [] retk cont = do
@ -537,7 +537,7 @@ checkStatement (P.Data name tele retk constrs) k =
checkCons _ _et [] k = k checkCons _ _et [] k = k
checkCons n ret (P.Point x ty:xs) k = do
checkCons n ret ((s, e, P.Point x ty):xs) k = withSpan s e $ do
t <- check ty VTypeω t <- check ty VTypeω
ty_nf <- eval t ty_nf <- eval t
let let
@ -548,7 +548,7 @@ checkStatement (P.Data name tele retk constrs) k =
closed_nf <- eval closed closed_nf <- eval closed
defineInternal (ConName x 0 (length n') (length args)) closed_nf (makeCon closed_nf mempty n' args) \_ -> checkCons n ret xs k defineInternal (ConName x 0 (length n') (length args)) closed_nf (makeCon closed_nf mempty n' args) \_ -> checkCons n ret xs k
checkCons n ret (P.Path name indices return faces:xs) k = do
checkCons n ret ((s, e, P.Path name indices return faces):xs) k = withSpan s e $ do
(con, closed_nf, value, boundary) <- assumes (flip Bound 0 <$> indices) VI \indices -> do (con, closed_nf, value, boundary) <- assumes (flip Bound 0 <$> indices) VI \indices -> do
t <- check return VTypeω t <- check return VTypeω
ty_nf <- eval t ty_nf <- eval t
@ -569,9 +569,12 @@ checkStatement (P.Data name tele retk constrs) k =
faces <- envArgs args $ for faces \(f, t) -> do faces <- envArgs args $ for faces \(f, t) -> do
phi <- checkFormula f phi <- checkFormula f
t <- check t ret t <- check t ret
pure (quote phi, t)
pure (phi, (quote phi, t))
system <- eval $ foldr (\x -> Lam P.Ex x) (System (Map.fromList faces)) (map (\(x, _, _) -> x) n' ++ map (\(x, _, _) -> x) args ++ indices)
system <- eval $ foldr (\x -> Lam P.Ex x) (System (Map.fromList (map snd faces))) (map (\(x, _, _) -> x) n' ++ map (\(x, _, _) -> x) args ++ indices)
unify (foldr ior VI0 (map fst faces)) (totalProp indices)
`withNote` pretty "The formula determining the endpoints of a higher constructor must be a classical tautology"
pure (ConName name 0 (length n') (length args + length indices), closed_nf, makePCon closed_nf mempty n' args indices system, Boundary indices system) pure (ConName name 0 (length n') (length args + length indices), closed_nf, makePCon closed_nf mempty n' args indices system, Boundary indices system)
defineInternal con closed_nf value \name -> addBoundary name boundary $ checkCons n ret xs k defineInternal con closed_nf value \name -> addBoundary name boundary $ checkCons n ret xs k
@ -591,6 +594,9 @@ checkStatement (P.Data name tele retk constrs) k =
makePCon cty sp [] ((nm, p, _):ys) zs sys con = VLam p $ Closure nm \a -> makePCon cty (sp Seq.:|> PApp p a) [] ys zs (sys @@ a) con makePCon cty sp [] ((nm, p, _):ys) zs sys con = VLam p $ Closure nm \a -> makePCon cty (sp Seq.:|> PApp p a) [] ys zs (sys @@ a) con
makePCon cty sp [] [] (nm:zs) sys con = VLam P.Ex $ Closure nm \a -> makePCon cty (sp Seq.:|> PApp P.Ex a) [] [] zs (sys @@ a) con makePCon cty sp [] [] (nm:zs) sys con = VLam P.Ex $ Closure nm \a -> makePCon cty (sp Seq.:|> PApp P.Ex a) [] [] zs (sys @@ a) con
totalProp (x:xs) = ior (inot (VVar x)) (VVar x) `ior` totalProp xs
totalProp [] = VI0
evalFix :: Name -> NFType -> Term -> ElabM Value evalFix :: Name -> NFType -> Term -> ElabM Value
evalFix name nft term = do evalFix name nft term = do
env <- ask env <- ask


+ 2
- 61
src/Elab/Eval.hs View File

@ -36,35 +36,12 @@ import Syntax
import System.IO.Unsafe import System.IO.Unsafe
import {-# SOURCE #-} Elab.WiredIn import {-# SOURCE #-} Elab.WiredIn
import Debug.Trace
import Data.List (sortOn) import Data.List (sortOn)
import Syntax.Subst
eval :: Term -> ElabM Value eval :: Term -> ElabM Value
eval t = asks (flip eval' t) eval t = asks (flip eval' t)
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 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
-- everywhere force -- everywhere force
zonkIO :: Value -> IO Value zonkIO :: Value -> IO Value
@ -125,13 +102,6 @@ zonkSp (POuc a phi u) = POuc <$> zonkIO a <*> zonkIO phi <*> zonkIO u
zonkSp PProj1 = pure PProj1 zonkSp PProj1 = pure PProj1
zonkSp PProj2 = pure PProj2 zonkSp 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')
zonk :: Value -> Value zonk :: Value -> Value
zonk = unsafePerformIO . zonkIO zonk = unsafePerformIO . zonkIO
@ -232,35 +202,6 @@ evalCase env rng (val@(VNe (HPCon _ _ x) sp)) ((Con x', k):xs)
evalCase _ rng sc xs = VCase (fun rng) sc xs evalCase _ rng sc xs = VCase (fun rng) sc xs
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))
data NotEqual = NotEqual Value Value data NotEqual = NotEqual Value Value
deriving (Show, Typeable, Exception) deriving (Show, Typeable, Exception)
@ -386,7 +327,7 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
| otherwise = fail | otherwise = fail
unify :: HasCallStack => Value -> Value -> ElabM () unify :: HasCallStack => Value -> Value -> ElabM ()
unify a b = unify' a b -- `catchElab` \(_ :: SomeException) -> liftIO $ throwIO (NotEqual a b)
unify a b = unify' a b `catchElab` \(_ :: SomeException) -> liftIO $ throwIO (NotEqual a b)
isConvertibleTo :: Value -> Value -> ElabM (Term -> Term) isConvertibleTo :: Value -> Value -> ElabM (Term -> Term)
isConvertibleTo a b = isConvertibleTo (force a) (force b) where isConvertibleTo a b = isConvertibleTo (force a) (force b) where


+ 52
- 27
src/Elab/WiredIn.hs View File

@ -25,7 +25,7 @@ import Syntax.Pretty (prettyTm)
import Syntax import Syntax
import System.IO.Unsafe import System.IO.Unsafe
import Debug.Trace (traceShowId, traceShow)
import Syntax.Subst
wiType :: WiredIn -> NFType wiType :: WiredIn -> NFType
wiType WiType = VType wiType WiType = VType
@ -211,16 +211,9 @@ outS _ _ _ v = error $ "can't outS " ++ show (prettyTm (quote v))
-- Composition -- Composition
comp :: NFLine -> NFEndp -> Value -> Value -> Value comp :: NFLine -> NFEndp -> Value -> Value -> Value
comp a VI1 u _
| not (isTyFam a) = u @@ VI1 @@ VItIsOne
where
isTyFam a =
case force (a @@ VI0) of
VType -> True
_ -> False
comp _a VI1 u _a0 = u @@ VI1 @@ VItIsOne
comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
case force $ a @@ VVar (Bound (T.pack "i") 0) of
case force $ a @@ VVar (Bound (T.pack "i") (negate 1)) of
VPi{} -> VPi{} ->
let let
plic i = let VPi p _ _ = force (a @@ i) in p plic i = let VPi p _ _ = force (a @@ i) in p
@ -240,10 +233,10 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
rng i = let VSigma _ (Closure _ r) = force (a @@ i) in r rng i = let VSigma _ (Closure _ r) = force (a @@ i) in r
w i = fill (fun dom) phi (system \i isone -> vProj1 (u @@ i @@ isone)) (VInc (dom VI0) phi (vProj1 a0)) i w i = fill (fun dom) phi (system \i isone -> vProj1 (u @@ i @@ isone)) (VInc (dom VI0) phi (vProj1 a0)) i
c1 = comp (fun dom) phi (system \i isone -> vProj1 (u @@ i @@ isone)) (VInc (dom VI0) phi (vProj1 a0))
-- c1 = comp (fun dom) phi (system \i isone -> vProj1 (u @@ i @@ isone)) (VInc (dom VI0) phi (vProj1 a0))
c2 = comp (fun \x -> rng x (w x)) phi (system \i isone -> vProj2 (u @@ i @@ isone)) (VInc (rng VI0 (w VI0)) phi (vProj2 a0)) c2 = comp (fun \x -> rng x (w x)) phi (system \i isone -> vProj2 (u @@ i @@ isone)) (VInc (rng VI0 (w VI0)) phi (vProj2 a0))
in in
VPair c1 c2
VPair (w VI1) c2
VPath{} -> VPath{} ->
let let
@ -259,17 +252,16 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
, (inot j, u' i)])) , (inot j, u' i)]))
(VInc (a' VI0 @@ VI0 @@ j) phi (ielim (a' VI0 @@ VI0) (u' VI0) (v' VI0) a0 j)) (VInc (a' VI0 @@ VI0 @@ j) phi (ielim (a' VI0 @@ VI0) (u' VI0) (v' VI0) a0 j))
VGlueTy{} ->
VGlueTy theBase thePhi theTypes theEquivs ->
let let
b = u b = u
b0 = a0 b0 = a0
fam = a
in in
let let
base i = let VGlueTy base _ _ _ = forceAndGlue (fam @@ i) in base
phi i = let VGlueTy _ phi _ _ = forceAndGlue (fam @@ i) in phi
types i = let VGlueTy _ _ types _ = forceAndGlue (fam @@ i) in types
equivs i = let VGlueTy _ _ _ equivs = forceAndGlue (fam @@ i) in equivs
base i = substitute (Map.singleton (Bound "i" (negate 1)) i) theBase
phi i = substitute (Map.singleton (Bound "i" (negate 1)) i) thePhi
types i = substitute (Map.singleton (Bound "i" (negate 1)) i) theTypes
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 = fun \u -> unglue (base i) (phi i) (types i @@ u) (equivs i @@ u) (b @@ i @@ u)
a0 = unglue (base VI0) (phi VI0) (types VI0) (equivs VI0) b0 a0 = unglue (base VI0) (phi VI0) (types VI0) (equivs VI0) b0
@ -299,7 +291,7 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
in b1 in b1
VType -> VGlueTy a0 phi (fun \is1 -> u @@ VI1 @@ is1) VType -> VGlueTy a0 phi (fun \is1 -> u @@ VI1 @@ is1)
(fun \i -> mkVSystem (Map.fromList [(phi, makeEquiv (\i -> u @@ inot i @@ VItIsOne))]))
(fun \i -> mapVSystem makeEquiv (u @@ inot i @@ VItIsOne))
VNe (HData False _) args -> VNe (HData False _) args ->
case force a0 of case force a0 of
@ -311,6 +303,10 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
_ -> VComp a phi u (VInc (a @@ VI0) phi a0) _ -> VComp a phi u (VInc (a @@ VI0) phi a0)
mapVSystem :: (Value -> Value) -> Value -> Value
mapVSystem f (VSystem fs) = VSystem (fmap f fs)
mapVSystem f x = f x
forceAndGlue :: Value -> Value forceAndGlue :: Value -> Value
forceAndGlue v = forceAndGlue v =
case force v of case force v of
@ -357,17 +353,17 @@ compOutS :: NFSort -> NFEndp -> Value -> Value -> Value
compOutS a b c d = compOutS a b c (force d) where 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 _ _hi _0 (VInc _ _ x) = x
compOutS _ _ _ v = v
compOutS a phi a0 v = outS a phi a0 v
system :: (Value -> Value -> Value) -> Value system :: (Value -> Value -> Value) -> Value
system k = fun \i -> fun \isone -> k i isone
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 :: NFLine -> NFEndp -> Value -> Value -> NFEndp -> Value
fill a phi u a0 j = fill a phi u a0 j =
comp (line \i -> a @@ (i `iand` j)) comp (line \i -> a @@ (i `iand` j))
(phi `ior` inot j) (phi `ior` inot j)
(fun \i -> fun \isone -> mkVSystem (Map.fromList [ (phi, u @@ (i `iand` j) @@ isone)
, (inot j, a0)]))
(system \i isone -> mkVSystem (Map.fromList [ (phi, u @@ (i `iand` j) @@ isone)
, (inot j, outS a phi (u @@ VI0) a0)]))
a0 a0
hComp :: NFSort -> NFEndp -> Value -> Value -> Value hComp :: NFSort -> NFEndp -> Value -> Value -> Value
@ -440,9 +436,38 @@ contr a aC phi u =
(system \i is1 -> ielim (line (const a)) (vProj1 aC) (u is1) (vProj2 aC @@ u is1) i) (system \i is1 -> ielim (line (const a)) (vProj1 aC) (u is1) (vProj2 aC @@ u is1) i)
(vProj1 aC) (vProj1 aC)
makeEquiv :: (NFEndp -> Value) -> Value
makeEquiv line = comp (fun \i -> equiv a (line i)) VI0 (system \_ _ -> VSystem mempty) (idEquiv a) where
a = line VI0
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)
where
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
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
theta1 x beta y i j =
fill (fun ((line @@) . inot))
(ior j (inot j))
(system \i _ -> mkVSystem (Map.fromList [ (inot j, v (inot i) @@ y)
, (j, u (inot i) @@ x)]))
(VInc b (ior j (inot j)) (ielim b y (f @@ x) beta y))
(inot i)
omega x beta y = theta1 x beta y VI0
delta x beta y j k = comp line (ior k (ior (inot k) (ior j (inot j))))
(system \i _ -> mkVSystem (Map.fromList [ (inot k, theta0 y i j)
, (k, theta1 x beta y i j)
, (inot j, v i @@ y)
, (j, u i @@ omega x beta y k)]))
(VInc a (ior k (ior (inot k) (ior j (inot j)))) (omega x beta y (iand j k)))
p x beta y = VLine (exists a \x -> VPath b y (f @@ x)) (fib y) (VPair x beta) $ fun \k ->
VPair (omega x beta y k) (VLine (VPath b y (f @@ x)) (vProj2 (fib y)) beta $ fun \j -> delta x beta y j k)
idEquiv :: NFSort -> Value idEquiv :: NFSort -> Value
idEquiv a = VPair idfun idisequiv where idEquiv a = VPair idfun idisequiv where
@ -453,4 +478,4 @@ idEquiv a = VPair idfun idisequiv where
VLine (fun (const a)) y (vProj1 u) $ fun \j -> VLine (fun (const a)) y (vProj1 u) $ fun \j ->
ielim (fun (const a)) y y (vProj2 u) (iand i j) ielim (fun (const a)) y y (vProj2 u) (iand i j)
id_fiber y = VPair y (VLine a y y (fun (const y)))
id_fiber y = VPair y (VLine a y y (fun (const y)))

+ 2
- 1
src/Elab/WiredIn.hs-boot View File

@ -1,8 +1,9 @@
module Elab.WiredIn where module Elab.WiredIn where
import Syntax
import GHC.Stack.Types import GHC.Stack.Types
import Syntax
wiType :: WiredIn -> NFType wiType :: WiredIn -> NFType
wiValue :: WiredIn -> NFType wiValue :: WiredIn -> NFType


+ 5
- 5
src/Presyntax/Parser.y View File

@ -167,12 +167,12 @@ Statement :: { Statement }
| 'data' var Parameters ':' Exp 'where' START Constructors END | 'data' var Parameters ':' Exp 'where' START Constructors END
{ spanSt $1 $9 $ Data (getVar $2) $3 $5 $8 } { spanSt $1 $9 $ Data (getVar $2) $3 $5 $8 }
Constructors :: { [Constructor] }
: var ':' Exp { [Point (getVar $1) $3] }
| var PatVarList ':' Exp '[' Faces ']' { [Path (getVar $1) (thd $2) $4 $6] }
| var ':' Exp Semis Constructors { Point (getVar $1) $3:$5 }
Constructors :: { [(Posn, Posn, Constructor)] }
: var ':' Exp { [(startPosn $1, endPosn $3, Point (getVar $1) $3)] }
| var PatVarList ':' Exp '[' Faces ']' { [(startPosn $1, endPosn $7, Path (getVar $1) (thd $2) $4 $6)] }
| var ':' Exp Semis Constructors { (startPosn $1, endPosn $3, Point (getVar $1) $3):$5 }
| var PatVarList ':' Exp '[' Faces ']' Semis Constructors | var PatVarList ':' Exp '[' Faces ']' Semis Constructors
{ Path (getVar $1) (thd $2) $4 $6:$9 }
{ (startPosn $1, endPosn $7, Path (getVar $1) (thd $2) $4 $6):$9 }
Parameters :: { [(Text, Plicity, Expr)] } Parameters :: { [(Text, Plicity, Expr)] }
: {- empty -} { [] } : {- empty -} { [] }


+ 1
- 1
src/Presyntax/Presyntax.hs View File

@ -60,7 +60,7 @@ data Statement
| ReplNf Expr -- REPL eval | ReplNf Expr -- REPL eval
| ReplTy Expr -- REPL :t | ReplTy Expr -- REPL :t
| Data Text [(Text, Plicity, Expr)] Expr [Constructor]
| Data Text [(Text, Plicity, Expr)] Expr [(Posn, Posn, Constructor)]
| SpanSt Statement Posn Posn | SpanSt Statement Posn Posn
deriving (Eq, Show, Ord) deriving (Eq, Show, Ord)


+ 2
- 2
src/Syntax.hs View File

@ -212,7 +212,7 @@ quoteWith names (GluedVl h sp (VLam p (Closure n k))) =
quoteWith names (GluedVl h sp vl) quoteWith names (GluedVl h sp vl)
| GluedVl _ _ inner <- vl = quoteWith names (GluedVl h sp inner) | GluedVl _ _ inner <- vl = quoteWith names (GluedVl h sp inner)
| alwaysShort vl = quoteWith names vl
| True || alwaysShort vl = quoteWith names vl
| otherwise = quoteWith names (VNe h sp) | otherwise = quoteWith names (VNe h sp)
quoteWith names (VLam p (Closure n k)) = quoteWith names (VLam p (Closure n k)) =
@ -307,4 +307,4 @@ data Projection
deriving (Eq, Show, Ord) deriving (Eq, Show, Ord)
data Boundary = Boundary { getBoundaryNames :: [Name], getBoundaryMap :: Value } data Boundary = Boundary { getBoundaryNames :: [Name], getBoundaryMap :: Value }
deriving (Eq, Show, Ord)
deriving (Eq, Show, Ord)

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

@ -74,6 +74,8 @@ prettyTm = prettyTm . everywhere (mkT beautify) where
prettyTm (IOr x y) = parens $ prettyTm x <+> operator (pretty "||") <+> prettyTm y prettyTm (IOr x y) = parens $ prettyTm x <+> operator (pretty "||") <+> prettyTm y
prettyTm (INot x) = operator (pretty '~') <> prettyTm x prettyTm (INot x) = operator (pretty '~') <> prettyTm x
prettyTm (System (Map.null -> True)) = braces mempty
prettyTm (System xs) = braces (line <> indent 2 (vcat (punctuate comma (map go (Map.toList xs)))) <> line) where prettyTm (System xs) = braces (line <> indent 2 (vcat (punctuate comma (map go (Map.toList xs)))) <> line) where
go (f, t) = prettyTm f <+> operator (pretty "=>") <+> prettyTm t go (f, t) = prettyTm f <+> operator (pretty "=>") <+> prettyTm t
@ -92,7 +94,7 @@ prettyTm = prettyTm . everywhere (mkT beautify) where
beautify (IElim _ _ _ f i) = App Ex f i beautify (IElim _ _ _ f i) = App Ex f i
beautify (PathIntro _ _ _ f) = f beautify (PathIntro _ _ _ f) = f
beautify (App p (Lam p' v b) _)
beautify (App _ (Lam _ v b) _)
| v `Set.notMember` freeVars b = beautify b | v `Set.notMember` freeVars b = beautify b
beautify (IsOne phi) = toFun "IsOne" [phi] beautify (IsOne phi) = toFun "IsOne" [phi]
@ -101,6 +103,9 @@ prettyTm = prettyTm . everywhere (mkT beautify) where
beautify (Lam Ex v (App Ex f (Ref v'))) beautify (Lam Ex v (App Ex f (Ref v')))
| v == v', v `Set.notMember` freeVars f = f | v == v', v `Set.notMember` freeVars f = f
beautify (Comp a I0 (System (Map.null -> True)) a0) = toFun "transp" [a, a0]
beautify (Lam _ _ (Lam _ _ (System (Map.null -> True)))) = System mempty
beautify (Partial phi a) = toFun "Partial" [phi, a] beautify (Partial phi a) = toFun "Partial" [phi, a]
beautify (PartialP phi a) = toFun "PartialP" [phi, a] beautify (PartialP phi a) = toFun "PartialP" [phi, a]
beautify (Comp a phi u a0) = toFun "comp" [a, phi, u, a0] beautify (Comp a phi u a0) = toFun "comp" [a, phi, u, a0]
@ -109,7 +114,9 @@ prettyTm = prettyTm . everywhere (mkT beautify) where
beautify (Inc _ _ u) = toFun "inS" [u] beautify (Inc _ _ u) = toFun "inS" [u]
beautify (Ouc a phi u u0) = toFun "outS" [a, phi, u, u0] beautify (Ouc a phi u u0) = toFun "outS" [a, phi, u, u0]
-- beautify (GlueTy a I1 _ _) = a
beautify (GlueTy a I1 _ _) = a
beautify (GlueTy a b c d) = toFun "Glue" [a,b,c,d] 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] beautify (Glue a b c d e f) = toFun "glue" [a,b,c,d,e,f]
beautify (Unglue a b c d e) = toFun "unglue" [a,b,c,d,e] beautify (Unglue a b c d e) = toFun "unglue" [a,b,c,d,e]


Loading…
Cancel
Save