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

Fixes to composition of HITs

Amélia Liao 3 years ago
committed by Abigail Magalhães
parent
46c867725a
commit
79b5a08bd3
12 changed files with 299 additions and 147 deletions
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. +1
    -0
      Setup.hs
  2. +2
    -0
      cubical.cabal
  3. +79
    -10
      intro.tt
  4. +38
    -0
      src/Debug.hs
  5. +9
    -9
      src/Elab.hs
  6. +28
    -21
      src/Elab/Eval.hs
  7. +2
    -2
      src/Elab/Eval/Formula.hs
  8. +66
    -60
      src/Elab/WiredIn.hs
  9. +14
    -12
      src/Elab/WiredIn.hs-boot
  10. +3
    -3
      src/Main.hs
  11. +6
    -2
      src/Syntax.hs
  12. +51
    -28
      src/Syntax/Pretty.hs

+ 1
- 0
Setup.hs View File

@ -1,3 +1,4 @@
import Distribution.Simple
main = defaultMain

+ 2
- 0
cubical.cabal View File

@ -46,6 +46,8 @@ executable cubical
, Elab.WiredIn
, Elab.Eval.Formula
, Debug
build-tool-depends: alex:alex >= 3.2.4 && < 4.0
, happy:happy >= 1.19.12 && < 2.0


+ 79
- 10
intro.tt View File

@ -292,6 +292,19 @@ hfill {A} {phi} u a0 i = fill (\i -> A) {phi} u a0 i
transRefl : {A : Type} {x : A} {y : A} (p : Path x y) -> Path (trans p refl) p
transRefl p j i = fill (\i -> A) {ior i (inot i)} (\k [ (i = i0) -> x, (i = i1) -> y ]) (inS (p i)) (inot j)
rightCancel : {A : Type} {x : A} {y : A} (p : Path x y) -> Path (trans p (sym p)) refl
rightCancel p j i = cube p i1 j i where
cube : {A : Type} {x : A} {y : A} (p : Path x y) -> I -> I -> I -> A
cube {A} {x} p k j i =
hfill {A} (\ k [ (i = i0) -> x
, (i = i1) -> p (iand (inot k) (inot j))
, (j = i1) -> x
])
(inS (p (iand i (inot j)))) k
leftCancel : {A : Type} {x : A} {y : A} (p : Path x y) -> Path (trans (sym p) p) refl
leftCancel p = rightCancel (sym p)
transpFill : {A : I -> Type} (x : A i0) -> PathP A x (transp (\i -> A i) x)
transpFill {A} x i = fill (\i -> A i) (\k []) (inS x) i
@ -313,7 +326,8 @@ 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)))
(\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,
@ -512,6 +526,13 @@ J : {A : Type} {x : A}
-> P y p
J P d p = transp (\i -> P (p i) (\j -> p (iand i j))) d
Jay : {A : Type} {x : A}
(P : ((y : A) * Path x y) -> Type)
(d : P (x, refl))
(s : (y : A) * Path x y)
-> P s
Jay P d s = transp (\i -> P ((singContr {A} {x}).2 s i)) d
-- Isomorphisms
---------------
@ -598,6 +619,9 @@ IsoToEquiv {A} {B} iso = (f, \y -> (fCenter y, fIsCenter y)) where
fIsCenter : (y : B) (w : fiber f y) -> Path (fCenter y) w
fIsCenter y w = lemIso y (fCenter y).1 w.1 (fCenter y).2 w.2
IsoToId : {A : Type} {B : Type} -> Iso A B -> Path A B
IsoToId i = univalence (IsoToEquiv i)
-- We can prove that any involutive function is an isomorphism, since
-- such a function is its own inverse.
@ -899,14 +923,18 @@ windingBase = refl
goAround : Int -> Path base base
goAround =
\case
pos n -> goAround_nat n
neg n -> sym (goAround_nat (succ n))
pos n -> forwards n
neg n -> backwards n
where
goAround_nat : Nat -> Path base base
goAround_nat = \case
forwards : Nat -> Path base base
forwards = \case
zero -> refl
succ n -> trans (\i -> loop i) (goAround_nat n)
succ n -> trans (forwards n) (\i -> loop i)
backwards : Nat -> Path base base
backwards = \case
zero -> \i -> loop (inot i)
succ n -> trans (backwards n) (\i -> loop (inot i))
-- One particularly general higher inductive type is the homotopy pushout,
-- which can be seen as a kind of sum B + C with the extra condition that
-- whenever x and y are in the image of f (resp. g), inl x ≡ inr y.
@ -1139,7 +1167,7 @@ S2IsSuspS1 = univalence (IsoToEquiv iso) where
fromS2 = \case { base2 -> north; surf2 i j -> suspSurf i j i1 }
toFromS2 : (x : S2) -> Path (toS2 (fromS2 x)) x
toFromS2 = \case { base2 -> refl; surf2 i j -> refl }
toFromS2 = \case { base2 -> refl; surf2 i j -> \k -> toS2 (suspSurf i j (inot k)) }
fromToS2 : (x : Susp S1) -> Path (fromS2 (toS2 x)) x
fromToS2 = \case { north -> refl; south -> \i -> merid base i; merid x i -> meridCase i x } where
@ -1177,7 +1205,7 @@ S3IsSuspS2 = univalence (IsoToEquiv iso) where
fromS3 = \case { base3 -> north; surf3 i j k -> suspSurf i j k i1 }
toFromS3 : (x : S3) -> Path (toS3 (fromS3 x)) x
toFromS3 = \case { base3 -> refl; surf3 i j k -> refl }
toFromS3 = \case { base3 -> refl; surf3 i j k -> \l -> toS3 (suspSurf i j k (inot l)) }
fromToS3 : (x : Susp S2) -> Path (fromS3 (toS3 x)) x
fromToS3 = \case { north -> refl; south -> \i -> merid base2 i; merid x i -> meridCase i x } where
@ -1264,4 +1292,45 @@ rightIsOne : {a : I} {b : I} -> Eq_s b i1 -> Eq_s (ior a b) i1
rightIsOne {a} {b} p = J_s {I} {i1} (\i p -> IsOne (ior a i)) refl_s (sym_s p)
bothAreOne : {a : I} {b : I} -> Eq_s a i1 -> Eq_s b i1 -> Eq_s (iand a b) i1
bothAreOne {a} {b} p q = J_s {I} {i1} (\i p -> IsOne (iand i b)) q (sym_s p)
bothAreOne {a} {b} p q = J_s {I} {i1} (\i p -> IsOne (iand i b)) q (sym_s p)
test : {X : Type} -> (S1 -> X) -> (a : X) * Path a a
test {X} f = (f base, \i -> f (loop i))
test' : {X : Type} -> ((a : X) * Path a a) -> S1 -> X
test' {X} p = \case
base -> p.1
loop i -> p.2 i
test_test' : {X : Type} -> (f : S1 -> X) -> Path (test' (test f)) f
test_test' {X} f = funext {S1} {\s -> X} {\x -> test' (test f) x} {f} h where
h : (x : S1) -> Path (test' (test f) x) (f x)
h = \case
base -> refl
loop i -> refl
test'_test : {X : Type} -> (x : (a : X) * Path a a) -> Path (test (test' x)) x
test'_test x = refl
test'' : {X : Type} -> Path (S1 -> X) ((a : X) * Path a a)
test'' = IsoToId {S1 -> X} {(a : X) * Path a a} (test, test', test'_test, test_test')
-- HoTT book lemma 8.9.1
encodeDecode : {A : Type} {a0 : A}
-> (code : A -> Type)
-> (c0 : code a0)
-> (decode : (x : A) -> code x -> (Path a0 x))
-> ((c : code a0) -> Path (transp (\i -> code (decode a0 c i)) c0) c)
-> Path (decode a0 c0) refl
-> Path (Path a0 a0) (code a0)
encodeDecode code c0 decode encDec based = IsoToId (encode {a0}, decode a0, encDec, decEnc) where
encode : {x : A} -> Path a0 x -> code x
encode alpha = transp (\i -> code (alpha i)) c0
encodeRefl : Path (encode refl) c0
encodeRefl = sym (transpFill {\i -> code a0} c0)
decEnc : {x : A} (p : Path a0 x) -> Path (decode x (encode p)) p
decEnc p = J (\x p -> Path (decode x (encode p)) p) q p where
q : Path (decode a0 (encode refl)) refl
q = transp (\i -> Path (decode a0 (encodeRefl (inot i))) refl) based

+ 38
- 0
src/Debug.hs View File

@ -0,0 +1,38 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}
module Debug where
import qualified Debug.Trace as D
#if defined(RELEASE)
import GHC.Exts
#else
import GHC.Stack
import Prettyprinter
#endif
traceDoc :: Doc a -> b -> b
#if defined(RELEASE)
type DebugCallStack = (() :: Constraint)
traceDoc !_ v = v
#else
type DebugCallStack = HasCallStack
traceDoc x = D.trace (show x)
#endif
trace :: Pretty a => a -> b -> b
trace x = traceDoc (pretty x)
traceWith :: Pretty a => String -> a -> b -> b
traceWith s x = traceDoc (pretty s <> pretty ": " <> pretty x)
traceId :: Pretty a => a -> a
traceId x = traceDoc (pretty x) x
traceDocM :: (Applicative m) => Doc a -> m ()
traceDocM x = traceDoc x (pure ())
traceM :: (Applicative m, Pretty a) => a -> m ()
traceM = traceDocM . pretty

+ 9
- 9
src/Elab.hs View File

@ -15,6 +15,7 @@ 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.Maybe (fromMaybe)
import Data.Traversable
import Data.Text (Text)
import Data.Map (Map)
@ -32,7 +33,6 @@ import Prettyprinter
import Syntax.Pretty
import Syntax
import Data.Maybe (fromMaybe)
infer :: P.Expr -> ElabM (Term, NFType)
infer (P.Span ex a b) = withSpan a b $ infer ex
@ -188,7 +188,7 @@ check (P.LamSystem bs) ty = do
, indent 2 $ pretty '*' <+> prettyTm (quote formula) <+> operator (pretty "=>") <+> prettyTm rhs
, indent 2 $ pretty '*' <+> prettyTm (quote formula') <+> operator (pretty "=>") <+> prettyTm rhs'
]
`withNote` (pretty "Consider this face, where both are true:" <+> showFace (snd truth))
`withNote` (pretty "Consider this face, where both are true:" <+> showFace False (snd truth))
name <- newName
let
@ -232,14 +232,14 @@ check (P.LamCase pats) ty =
let rhs = cases @@ side
for_ (truthAssignments formula mempty) $ \i -> do
let vl = foldl (\v n -> vApp P.Ex v (lookup n)) base (getBoundaryNames boundary)
lookup n = fromMaybe VI0 (snd <$> (Map.lookup n i))
lookup n = fromMaybe (VVar n) (snd <$> (Map.lookup n i))
unify vl rhs
`withNote` (pretty "From the boundary conditions of the constructor" <+> prettyTm (quote pat_nf) <> pretty ":")
`withNote` vcat [ pretty "These must be the same because of the face"
, indent 2 $ prettyTm (quote formula) <+> operator (pretty "=>") <+> prettyTm (quote (zonk side))
, pretty "which evaluates into"
, indent 2 $ prettyTm (quote formula) <+> operator (pretty "=>") <+> prettyVl rhs
, indent 2 $ prettyVl (zonk formula) <+> operator (pretty "=>") <+> prettyVl (zonk side)
, pretty "which is mapped to"
, indent 2 $ prettyVl (zonk formula) <+> operator (pretty "=>") <+> prettyVl (zonk rhs)
]
`withNote` (pretty "Mandated by the constructor" <+> prettyTm (quote pat_nf))
_ -> pure ()
pure (pat, n_lams, wp rhs)
@ -502,7 +502,7 @@ checkStatement (P.ReplNf e) k = do
(e, _) <- infer e
e_nf <- eval e
h <- asks commHook
liftIO (h (prettyVl e_nf))
liftIO $ h . prettyVl =<< zonkIO e_nf
k
checkStatement (P.ReplTy e) k = do
@ -624,4 +624,4 @@ data NotACon = NotACon { theNotConstr :: Name }
deriving anyclass (Exception)
newtype DeclaredUndefined = DeclaredUndefined { declaredUndefName :: Name }
deriving (Eq, Show, Exception)
deriving (Eq, Show, Exception)

+ 28
- 21
src/Elab/Eval.hs View File

@ -82,17 +82,14 @@ 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 (VInc a b c) = incS <$> 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 (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' <- (\x -> x {getEnv = env}) <$> emptyEnv
let xs' = map (\(a, i, n) -> (a, i, quote (eval' env' n))) xs
evalCase 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
@ -130,7 +127,7 @@ 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 (error ("type of abs " ++ show (pretty (Lam p s t))), a) (getEnv env) } t
eval' env (Pi p s d t) =
VPi p (eval' env d) $ Closure s $ \a ->
@ -166,7 +163,7 @@ eval' e (PartialP x y) = VPartialP (eval' e x) (eval' e y)
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)
@ -195,11 +192,14 @@ 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 (fun (const 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
@ -213,10 +213,10 @@ evalCase env rng (val@(VNe (HPCon _ _ x) sp)) ((Con x', _, k):xs)
evalCase env rng sc xs = VCase (getEnv env) (fun rng) sc xs
evalFix' :: ElabEnv -> Name -> NFType -> Term -> Value
evalFix' :: HasCallStack => ElabEnv -> Name -> NFType -> Term -> Value
evalFix' env name nft term = fix $ \val -> eval' env{ getEnv = Map.insert name (nft, val) (getEnv env) } term
evalFix :: Name -> NFType -> Term -> ElabM Value
evalFix :: HasCallStack => Name -> NFType -> Term -> ElabM Value
evalFix name nft term = do
t <- ask
pure (evalFix' t name nft term)
@ -231,8 +231,10 @@ unify' 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 = go (force s) rhs
go lhs (VNe (HPCon s _ _) _) = go lhs (force s)
go (VNe (HPCon _ _ x) sp) (VNe (HPCon _ _ y) sp')
| x == y = traverse_ (uncurry unify'Spine) (Seq.zip sp sp')
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 _ a b) (VCase e' _ a' b') = do
env <- ask
@ -343,6 +345,11 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
| compareDNFs x y = pure ()
| otherwise = fail
trivialSystem :: Value -> Maybe Value
trivialSystem = go . force where
go VSystem{} = Nothing
go x = Just x
unify'Spine :: Projection -> Projection -> ElabM ()
unify'Spine (PApp a v) (PApp a' v')
| a == a' = unify' v v'
@ -568,7 +575,7 @@ substituteIO sub = substituteIO . force where
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
@ -576,8 +583,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 <$> zonkIO a <*> zonkIO x <*> zonkIO y
substituteIO (VReflStrict a x) = VReflStrict <$> zonkIO a <*> zonkIO x
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
@ -594,7 +601,7 @@ substituteSp _ PProj2 = pure PProj2
mkVSystem :: Map.Map Value Value -> Value
mkVSystem vals =
let map' = Map.fromList (Map.toList vals >>= go)
go (x, y) =
go (x, y) =
case (force x, y) of
(VI0, _) -> []
(VIOr _ _, VSystem y) -> Map.toList y >>= go
@ -653,7 +660,7 @@ 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 (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 (prettyTm (quote x))
@ -663,7 +670,7 @@ 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 (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))

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

@ -2,13 +2,13 @@ module Elab.Eval.Formula where
import qualified Data.Map.Strict as Map
import qualified Data.Sequence as Seq
import qualified Data.Set as Set
import Data.Map.Strict (Map)
import Data.Set (Set)
import Syntax
import {-# SOURCE #-} Elab.WiredIn (inot, ior, iand)
import Data.Set (Set)
import qualified Data.Set as Set
toDnf :: Value -> Maybe Value
toDnf = fmap (dnf2Val . normalise) . val2Dnf where


+ 66
- 60
src/Elab/WiredIn.hs View File

@ -4,6 +4,9 @@
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}
module Elab.WiredIn where
import Control.Exception
@ -15,10 +18,13 @@ import Data.Map.Strict (Map)
import Data.Text (Text)
import Data.Typeable
import Debug
import Elab.Eval
import GHC.Stack (HasCallStack)
import Presyntax.Presyntax (Plicity(Im, Ex))
import qualified Presyntax.Presyntax as P
import Syntax.Pretty (prettyTm, prettyVl)
@ -71,17 +77,17 @@ wiValue WiInterval = VI
wiValue WiI0 = VI0
wiValue WiI1 = VI1
wiValue WiIAnd = fun \x -> fun \y -> iand x y
wiValue WiIOr = fun \x -> fun \y -> ior x y
wiValue WiINot = fun inot
wiValue WiPathP = fun \a -> fun \x -> fun \y -> VPath a x y
wiValue WiIAnd = functions [(Ex, "i"), (Ex, "j")] \[i, j] -> iand i j
wiValue WiIOr = functions [(Ex, "i"), (Ex, "j")] \[i, j] -> ior i j
wiValue WiINot = fun' "x" inot
wiValue WiPathP = functions [(Ex, "A"), (Ex, "x"), (Ex, "y")] \[a, x, y] -> VPath a x y
wiValue WiPartial = fun \phi -> fun \r -> VPartial phi r
wiValue WiPartialP = fun \phi -> fun \r -> VPartialP phi r
wiValue WiSub = fun \a -> fun \phi -> fun \u -> VSub a phi u
wiValue WiInS = forallI \a -> forallI \phi -> fun \u -> VInc a phi u
wiValue WiOutS = forallI \a -> forallI \phi -> forallI \u -> fun \x -> outS a phi u x
wiValue WiComp = fun \a -> forallI \phi -> fun \u -> fun \x -> VInc (a @@ VI1) phi (comp a phi u x)
wiValue WiPartial = functions [(Ex, "phi"), (Ex, "A")] \[phi, a] -> VPartial phi a
wiValue WiPartialP = functions [(Ex, "phi"), (Ex, "A")] \[phi, a] -> VPartialP phi a
wiValue WiSub = functions [(Ex, "A"), (Ex, "phi"), (Ex, "u")] \[a, phi, u] -> VSub a phi u
wiValue WiInS = functions [(Im, "A"), (Im, "phi"), (Ex, "u")] \[a, phi, u] -> incS a phi u
wiValue WiOutS = functions [(Im, "A"), (Im, "phi"), (Im, "u"), (Ex, "u0")] \[a, phi, u, x] -> outS a phi u x
wiValue WiComp = fun' "A" \a -> forallI \phi -> fun' "u" \u -> fun' "u0" \x -> incS (a @@ VI1) phi (comp a phi u x)
wiValue WiGlue = fun \a -> forallI \phi -> fun \t -> fun \e -> glueType a phi t e
wiValue WiGlueElem = forallI \a -> forallI \phi -> forallI \ty -> forallI \eqv -> fun \x -> fun \y -> glueElem a phi ty eqv x y
@ -109,6 +115,11 @@ 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)
functions :: [(P.Plicity, String)] -> ([Value] -> Value) -> Value
functions args cont = go args [] where
go [] acc = cont (reverse acc)
go ((p, x):xs) acc = VLam p $ Closure (Bound (T.pack x) 0) \arg -> go xs (arg:acc)
forallI :: (Value -> Value) -> Value
forallI k = VLam P.Im $ Closure (Bound "x" 0) (k . force)
@ -130,7 +141,6 @@ forAll' n a b = VPi P.Im a (Closure (Bound (T.pack n) 0) b)
forAll :: Value -> (Value -> Value) -> Value
forAll = forAll' "x"
wiredInNames :: Map Text WiredIn
wiredInNames = Map.fromList
[ ("Pretype", WiPretype)
@ -153,7 +163,7 @@ wiredInNames = Map.fromList
, ("Glue", WiGlue)
, ("glue", WiGlueElem)
, ("unglue", WiUnglue)
, ("Eq_s", WiSEq)
, ("refl_s", WiSRefl)
, ("K_s", WiSK)
@ -221,21 +231,26 @@ ielim line left right fn i =
_ -> error $ "can't ielim " ++ show (prettyTm (quote fn))
outS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value
incS :: DebugCallStack => NFSort -> NFEndp -> Value -> Value
incS _ _ (force -> VNe h (sp Seq.:|> POuc _ _ _))
= VNe h sp
incS a phi u = VInc a phi u
outS :: DebugCallStack => NFSort -> NFEndp -> Value -> Value -> Value
outS _ (force -> VI1) u _ = u @@ VReflStrict VI VI1
outS _ _phi _ (VInc _ _ x) = x
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 (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) = mkVSystem (fmap (outS a phi u) fs)
outS _ _ _ v = error $ "can't outS " ++ show (prettyTm (quote v))
-- Composition
comp :: HasCallStack => NFLine -> NFEndp -> Value -> Value -> Value
comp :: DebugCallStack => NFLine -> NFEndp -> Value -> Value -> Value
comp _a VI1 u _a0 = u @@ VI1 @@ VReflStrict VI VI1
comp a psi@phi u incA0@(compOutS (a @@ VI0) phi (u @@ VI0) -> a0) =
comp a psi@phi u incA0@(outS (a @@ VI0) phi (u @@ VI0) -> a0) =
case force (a @@ VVar name) of
VPi{} ->
let
@ -243,20 +258,21 @@ comp a psi@phi u incA0@(compOutS (a @@ VI0) phi (u @@ VI0) -> a0) =
dom i = let VPi _ d _ = force (a @@ i) in d
rng i = let VPi _ _ (Closure _ r) = force (a @@ i) in r
y' i y = fill (fun (dom . inot)) VI0 (fun \_ -> fun \_ -> VSystem mempty) (VInc (dom VI0) phi y) i
y' i y = fill (fun (dom . inot)) VI0 (fun \_ -> fun \_ -> VSystem mempty) (incS (dom VI0) phi y) i
ybar i y = y' (inot i) y
in VLam (plic VI1) . Closure (Bound "x" 0) $ \arg ->
comp (line \i -> rng i (ybar i arg))
phi
(system \i isone -> vApp (plic i) (u @@ i @@ isone) (ybar i arg))
(VInc (rng VI0 (ybar VI0 arg)) phi (vApp (plic VI0) a0 (ybar VI0 arg)))
(incS (rng VI0 (ybar VI0 arg)) phi (vApp (plic VI0) a0 (ybar VI0 arg)))
VSigma{} ->
let
dom i = let VSigma d _ = force (a @@ i) in d
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
c2 = comp (fun \x -> rng x (w x)) phi (system \i isone -> vProj2 (u @@ i @@ isone)) (VInc (rng VI0 (w VI0)) phi (vProj2 a0))
w i = fill (fun dom) phi (system \i isone -> vProj1 (u @@ i @@ isone)) (incS (dom VI0) phi (vProj1 a0)) i
c2 = comp (fun \x -> rng x (w x)) phi (system \i isone -> vProj2 (u @@ i @@ isone)) (incS (rng VI0 (w VI0)) phi (vProj2 a0))
in
VPair (w VI1) c2
@ -272,7 +288,7 @@ comp a psi@phi u incA0@(compOutS (a @@ VI0) phi (u @@ VI0) -> a0) =
(system \i isone -> mkVSystem (Map.fromList [ (phi, ielim (a' VI0) (u' VI0) (v' VI0) (u @@ i @@ isone) j)
, (j, v' i)
, (inot j, u' i)]))
(VInc (a' VI0 @@ VI0 @@ j) phi (ielim (a' VI0 @@ VI0) (u' VI0) (v' VI0) a0 j))
(incS (a' VI0 @@ VI0 @@ j) phi (ielim (a' VI0 @@ VI0) (u' VI0) (v' VI0) a0 j))
VGlueTy _ thePhi theTypes theEquivs ->
let
@ -290,8 +306,8 @@ comp a psi@phi u incA0@(compOutS (a @@ VI0) phi (u @@ VI0) -> a0) =
a0 = unglue (base VI0) (phi VI0) (types VI0) (equivs VI0) b0
del = faceForall phi
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)
a1' = comp (line base) psi (system a) (incS (base VI0) psi a0)
t1' = comp (line (const (types VI0))) psi (line (b @@)) (incS (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
@ -309,7 +325,7 @@ comp a psi@phi u incA0@(compOutS (a @@ VI0) phi (u @@ VI0) -> a0) =
(phi VI1 `ior` psi)
(system \j _u -> mkVSystem (Map.fromList [ (phi VI1, ielim (base VI1) a1' (vProj1 (equivs VI1 @@ VReflStrict VI VI1)) alpha j)
, (psi, a VI1 (VReflStrict VI VI1))]))
(VInc (base VI1) (phi VI1 `ior` psi) a1')
(incS (base VI1) (phi VI1 `ior` psi) a1')
b1 = glueElem (base VI1) (phi VI1) (types VI1) (equivs VI1) (fun (const t1)) a1
in b1
@ -321,14 +337,11 @@ comp a psi@phi u incA0@(compOutS (a @@ VI0) phi (u @@ VI0) -> a0) =
case force a0 of
VNe (HCon con_type con_name) con_args ->
VNe (HCon con_type con_name) $ compConArgs makeSetFiller (length args) (a @@) con_type con_args phi u
_ -> VComp a phi u (VInc (a @@ VI0) phi a0)
_ -> VComp a phi u (incS (a @@ VI0) phi a0)
VNe (HData True name) args -> compHIT name (length args) (a @@) phi u incA0
VLam{} -> error $ "comp VLam " ++ show (prettyTm (quote a))
VSystem map -> mkVSystem (fmap (\x -> comp x psi u incA0) map)
_ -> VComp a phi u (VInc (a @@ VI0) phi a0)
_ -> VComp a phi u (incS (a @@ VI0) phi a0)
where
{-# NOINLINE name #-}
name = unsafePerformIO newName
@ -350,12 +363,12 @@ compHIT :: HasCallStack => Name -> Int -> (NFEndp -> NFSort) -> NFEndp -> Value
compHIT name n a phi u a0 =
case force phi of
VI1 -> u @@ VI1 @@ VReflStrict VI VI1
VI0 | n == 0 -> compOutS (a VI0) phi u a0
| otherwise -> transHit name a VI0 (compOutS (a VI0) phi u a0)
VI0 | n == 0 -> outS (a VI0) phi u a0
| otherwise -> transHit name a VI0 (outS (a VI0) phi u a0)
x -> go n a x u a0
where
go 0 a phi u a0 = VHComp (a VI0) phi u a0
go _ a phi u a0 = VHComp (a VI1) phi (system \i n -> transSqueeze name a VI0 (\i -> u @@ i @@ n) i) (transHit name a VI0 (compOutS (a VI1) phi (u @@ VI1 @@ VReflStrict VI VI1) a0))
go _ a phi u a0 = VHComp (a VI1) phi (system \i n -> transSqueeze name a VI0 (\i -> u @@ i @@ n) i) (transHit name a VI0 (outS (a VI0) phi (u @@ VI1 @@ VReflStrict VI VI1) a0))
compConArgs :: (Name -> Int -> Value -> t1 -> t2 -> Value -> Value)
-> Int
@ -396,13 +409,6 @@ nthArg i (force -> VNe hd s) =
nthArg i (force -> VSystem vs) = VSystem (fmap (nthArg i) vs)
nthArg i xs = error $ "can't get " ++ show i ++ "th argument of " ++ show (prettyTm (quote xs))
compOutS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value
compOutS a b c d = compOutS a b c (force d) where
compOutS _ _hi _0 vl@VComp{} = error $ "unwrapped composition given as input to composition operation is fuckign illegal " ++ show (prettyTm (quote (zonk vl)))
compOutS _ _hi _0 vl@VHComp{} = error $ "unwrapped composition (gay) given as input to composition operation is fuckign illegal " ++ show (prettyTm (quote (zonk 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 "[i]" 0) \isone -> k i isone
@ -414,18 +420,18 @@ fill a phi u a0 j =
, (inot j, outS a phi (u @@ VI0) a0)]))
a0
hComp :: NFSort -> NFEndp -> Value -> Value -> Value
hComp :: DebugCallStack => NFSort -> NFEndp -> Value -> Value -> Value
hComp _ (force -> VI1) u _ = u @@ VI1 @@ VReflStrict VI VI1
hComp a phi u a0 = VHComp a phi u a0
glueType :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
glueType :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
glueType a phi tys eqvs = VGlueTy a phi tys eqvs
glueElem :: NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
glueElem :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
glueElem _a (force -> VI1) _tys _eqvs t _vl = t @@ VReflStrict VI VI1
glueElem a phi tys eqvs t vl = VGlue a phi tys eqvs t vl
unglue :: HasCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
unglue :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
unglue _a (force -> VI1) _tys eqvs x = vProj1 (eqvs @@ VReflStrict VI VI1) @@ x
unglue _a _phi _tys _eqvs (force -> VGlue _ _ _ _ t vl) = outS _a _phi (t @@ VReflStrict VI VI1) vl
unglue a phi tys eqvs (force -> VSystem fs) = VSystem (fmap (unglue a phi tys eqvs) fs)
@ -462,18 +468,18 @@ equiv a b = GluedVl (HCon VType (Defined (T.pack "Equiv") (-1))) sp $ exists' "f
sp = Seq.fromList [ PApp P.Ex a, PApp P.Ex b ]
pres :: (NFEndp -> NFSort) -> (NFEndp -> NFSort) -> (NFEndp -> Value) -> NFEndp -> (NFEndp -> Value) -> Value -> (Value, NFSort, Value)
pres tyT tyA f phi t t0 = (VInc pathT phi (VLine (tyA VI1) c1 c2 (line path)), pathT, fun $ \u -> VLine (fun (const (tyA VI1))) c1 c2 (fun (const (f VI1 @@ (t VI1 @@ u))))) where
pres tyT tyA f phi t t0 = (incS pathT phi (VLine (tyA VI1) c1 c2 (line path)), pathT, fun $ \u -> VLine (fun (const (tyA VI1))) c1 c2 (fun (const (f VI1 @@ (t VI1 @@ u))))) where
pathT = VPath (fun (const (tyA VI1))) c1 c2
c1 = comp (line tyA) phi (system \i u -> f i @@ (t i @@ u)) (VInc (tyA VI0) phi (f VI0 @@ t0))
c1 = comp (line tyA) phi (system \i u -> f i @@ (t i @@ u)) (incS (tyA VI0) phi (f VI0 @@ t0))
c2 = f VI1 @@ comp (line tyT) phi (system \i u -> t i @@ u) t0
a0 = f VI0 @@ t0
v = fill (fun tyT) phi (system \i u -> t i @@ u) t0
path j = comp (fun tyA) (phi `ior` j) (system \i _ -> f i @@ (v i)) (VInc (tyA VI0) phi a0)
path j = comp (fun tyA) (phi `ior` j) (system \i _ -> f i @@ (v i)) (incS (tyA VI0) phi a0)
opEquiv :: HasCallStack => Value -> Value -> Value -> NFEndp -> Value -> Value -> Value -> (Value, NFSort, Value)
opEquiv aT tT f phi t p a = (VInc ty phi v, ty, fun \u -> VPair (t @@ u) (p @@ u)) where
opEquiv aT tT f phi t p a = (incS ty phi v, ty, fun \u -> VPair (t @@ u) (p @@ u)) where
fn = vProj1 f
ty = exists' "f" tT \x -> VPath (line (const aT)) a (fn @@ x)
v = contr ty (vProj2 f @@ a) phi (\u -> VPair (t @@ u) (p @@ u))
@ -483,17 +489,17 @@ 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)
(VInc a phi (vProj1 aC))
(incS a phi (vProj1 aC))
transp :: (NFEndp -> Value) -> Value -> Value
transp line a0 = comp (fun line) VI0 (system \_ _ -> VSystem mempty) (VInc (line VI0) VI0 a0)
transp line a0 = comp (fun line) VI0 (system \_ _ -> VSystem mempty) (incS (line VI0) VI0 a0)
gtrans :: (NFEndp -> Value) -> NFEndp -> Value -> Value
gtrans line phi a0 = comp (fun line) phi (system \_ _ -> mkVSystem (Map.singleton phi a0)) (VInc (line VI0) VI0 a0)
gtrans line phi a0 = comp (fun line) phi (system \_ _ -> mkVSystem (Map.singleton phi a0)) (incS (line VI0) VI0 a0)
transHit :: Name -> (NFEndp -> Value) -> NFEndp -> Value -> Value
transHit name line phi x = transHit name line phi (force x) where
transHit name line phi (VHComp _ psi u u0) = VHComp (line VI1) psi (system \i j -> transHit name line phi (u @@ i @@ j)) (transHit name line phi (compOutS (line VI0) phi u u0))
transHit name line phi (VHComp _ psi u u0) = VHComp (line VI1) psi (system \i j -> transHit name line phi (u @@ i @@ j)) (transHit name line phi (outS (line VI0) phi u u0))
transHit name line phi (VNe (HCon con_type con_name) spine) | ourType = x' where
x' = VNe (HCon con_type con_name) $ compConArgs (makeTransFiller name) nargs line con_type spine phi ()
(_, VNe hd (length -> nargs)) = unPi con_type
@ -538,17 +544,17 @@ makeEquiv' line' = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vP
f = fun \x -> transp (line @@) x
g = fun \x -> transp ((line @@) . inot) x
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)
u i = fun \x -> fill line VI0 (system \_ _ -> mkVSystem mempty) (incS a VI0 x) i
v i = fun \x -> fill (fun ((line @@) . inot)) VI0 (system \_ _ -> mkVSystem mempty) (incS 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
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))])) (incS 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))
(incS 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))))
@ -556,7 +562,7 @@ makeEquiv' line' = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vP
, (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)))
(incS 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)
@ -571,7 +577,7 @@ idEquiv a = VPair idfun idisequiv where
id_fiber y = VPair y (VLine a y y (fun (const y)))
strictK :: Value -> Value -> Value -> Value -> Value -> Value
strictK :: DebugCallStack => Value -> Value -> Value -> Value -> Value -> Value
strictK _ _ _ pr (VReflStrict _ _) = pr
strictK a x bigp pr (VNe h sp) = VNe h (sp Seq.:|> PK a x bigp pr)
strictK a x bigp pr (VCase env rng sc cases) = VCase env rng sc (map (projIntoCase func) cases) where
@ -579,7 +585,7 @@ strictK a x bigp pr (VCase env rng sc cases) = VCase env rng sc (map (projIntoCa
strictK a x bigp pr (GluedVl h sp vl) = GluedVl h (sp Seq.:|> PK a x bigp pr) (strictK a x bigp pr vl)
strictK _ _ _ _r eq = error $ "can't K " ++ show (prettyVl eq)
strictJ :: Value -> Value -> Value -> Value -> Value -> Value -> Value
strictJ :: DebugCallStack => Value -> Value -> Value -> Value -> Value -> Value -> Value
strictJ _a _x _bigp pr _ (VReflStrict _ _) = pr
strictJ a x bigp pr y (VNe h sp) = VNe h (sp Seq.:|> PJ a x bigp pr y)
strictJ a x bigp pr y (VCase env rng sc cases) = VCase env rng sc (map (projIntoCase func) cases) where
@ -592,4 +598,4 @@ projIntoCase fun (pat, nLams, term) = (pat, nLams, go nLams term) where
go 0 x = fun x
go n (Lam p x r) = Lam p x (go (n - 1) r)
go n (PathIntro l a b r) = PathIntro l a b (go (n - 1) r)
go _ x = x
go _ x = x

+ 14
- 12
src/Elab/WiredIn.hs-boot View File

@ -1,8 +1,9 @@
module Elab.WiredIn where
import GHC.Stack.Types
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}
module Elab.WiredIn (wiType, wiValue, iand, ior, inot, ielim, incS, outS, comp, fill, hComp, glueType, glueElem, unglue, fun, system, strictK, strictJ, projIntoCase) where
import Syntax
import Debug (DebugCallStack)
wiType :: WiredIn -> NFType
wiValue :: WiredIn -> NFType
@ -11,19 +12,20 @@ iand, ior :: NFEndp -> NFEndp -> NFEndp
inot :: NFEndp -> NFEndp
ielim :: NFSort -> Value -> Value -> Value -> NFEndp -> Value
outS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value
comp :: HasCallStack => NFLine -> NFEndp -> Value -> Value -> Value
fill :: HasCallStack => NFLine -> NFEndp -> Value -> Value -> Value -> Value
hComp :: NFSort -> NFEndp -> Value -> Value -> Value
incS :: DebugCallStack => NFSort -> NFEndp -> Value -> Value
outS :: DebugCallStack => NFSort -> NFEndp -> Value -> Value -> Value
comp :: DebugCallStack => NFLine -> NFEndp -> Value -> Value -> Value
fill :: DebugCallStack => NFLine -> NFEndp -> Value -> Value -> Value -> Value
hComp :: DebugCallStack => NFSort -> NFEndp -> Value -> Value -> Value
glueType :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
glueElem :: NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
unglue :: HasCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
glueType :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
glueElem :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
unglue :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
fun :: (Value -> Value) -> Value
system :: (Value -> Value -> Value) -> Value
strictK :: NFSort -> Value -> NFSort -> Value -> Value -> Value
strictJ :: NFSort -> Value -> NFSort -> Value -> Value -> Value -> Value
strictK :: DebugCallStack => NFSort -> Value -> NFSort -> Value -> Value -> Value
strictJ :: DebugCallStack => NFSort -> Value -> NFSort -> Value -> Value -> Value -> Value
projIntoCase :: (Term -> Term) -> (Term, Int, Term) -> (Term, Int, Term)

+ 3
- 3
src/Main.hs View File

@ -22,7 +22,7 @@ import Data.Foldable
import Data.Maybe
import Data.IORef
import Debug.Trace
import Debug (traceDocM)
import Elab.Monad hiding (switch)
import Elab.WiredIn
@ -64,7 +64,7 @@ evalArgExpr env str =
Right e ->
flip runElab env (do
(e, _) <- infer e
liftIO . putStrLn . show . prettyTm . quote . zonk =<< Elab.Eval.eval e)
liftIO . T.putStrLn . render . prettyTm . quote . zonk =<< Elab.Eval.eval e)
`catch` \e -> do
displayExceptions' inp (e :: SomeException)
Left e -> liftIO $ print e
@ -267,5 +267,5 @@ dumpTokens = do
case tokenClass t of
TokEof -> pure ()
_ -> do
traceM (show t)
traceDocM (viaShow t)
dumpTokens

+ 6
- 2
src/Syntax.hs View File

@ -201,7 +201,8 @@ quoteWith names (VNe h sp) = foldl goSpine (goHead h) sp where
case Map.lookup VI1 f of
Just vl -> constantly (length sp) vl
_ -> PCon (quote sys) v
_ -> PCon (quote sys) v
VLam{} -> PCon (quote sys) v
s -> constantly (length sp) s
goHead (HData x v) = Data x v
goSpine t (PApp p v) = App p t (quoteWith names v)
@ -220,6 +221,9 @@ quoteWith names (GluedVl _ Seq.Empty x) = quoteWith names x
quoteWith names (GluedVl h sp (VLam p (Closure n k))) =
quoteWith names (VLam p (Closure n (\a -> GluedVl h (sp Seq.:|> PApp p a) (k a))))
quoteWith names (GluedVl h sp (VLine ty x y (VLam p (Closure n k)))) =
quoteWith names (VLine ty x y (VLam p (Closure n (\a -> GluedVl h (sp Seq.:|> PIElim ty x y a) (k a)))))
quoteWith names (GluedVl h sp vl)
| GluedVl _ _ inner <- vl = quoteWith names (GluedVl h sp inner)
| alwaysShort vl = quoteWith names vl
@ -328,4 +332,4 @@ unPi :: Value -> ([(Plicity, Value)], Value)
unPi (VPi p d (Closure n k)) =
let (a, x) = unPi (k (VVar n))
in ((p, d):a, x)
unPi x = ([], x)
unPi x = ([], x)

+ 51
- 28
src/Syntax/Pretty.hs View File

@ -2,9 +2,9 @@
{-# OPTIONS_GHC -Wno-orphans #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE CPP #-}
module Syntax.Pretty where
import qualified Data.Map.Strict as Map
import qualified Data.Text.Lazy as L
import qualified Data.Text as T
@ -21,8 +21,8 @@ import Syntax
instance Pretty Name where
pretty = pretty . getNameText
prettyTm :: Term -> Doc AnsiStyle
prettyTm = go True 0 where
prettyTm' :: Bool -> Term -> Doc AnsiStyle
prettyTm' implicits = go True 0 where
go t p =
\case
Ref v -> pretty v
@ -30,12 +30,16 @@ prettyTm = go True 0 where
PCon _ v -> keyword $ pretty v
Data _ v -> keyword $ pretty v
App Im f _ -> go t p f
App Im f x
| implicits -> parenIf (p >= arg_prec) $
go False fun_prec f
<+> braces (go False 0 x)
| otherwise -> go t p f
App Ex f x ->
parenIf (p >= arg_prec) $
go False fun_prec f
<+> group (go False arg_prec x)
Lam Ex v (App Ex f (Ref v')) | v == v' -> instead f
Lam i v t ->
let
@ -50,8 +54,8 @@ prettyTm = go True 0 where
parenIf (p >= fun_prec) . group $
pretty '\\' <> hsep (map (\(i, v) -> braceIf (i == Im) (pretty v)) as)
<+> arrow
<+> nest 2 (go False 0 b)
<+> nest 2 (align (go False 0 b))
Pi _ (T.unpack . getNameText -> "_") d r ->
parenIf (p >= fun_prec) $
group (go False dom_prec d)
@ -67,12 +71,12 @@ prettyTm = go True 0 where
parenIf (p >= fun_prec) $
plic i (pretty x <+> colon <+> go False 0 d)
<> c <> go t 0 r
Let binds body ->
parenIf (p >= fun_prec) $
align $ keyword (pretty "let")
<> line
<> indent 2 (prettyBinds binds)
<> indent 2 (prettyBinds False binds)
<> keyword (pretty "in")
<+> go False 0 body
@ -104,7 +108,7 @@ prettyTm = go True 0 where
PathP _ x y -> parenIf (p >= arg_prec) $
go False 0 x <+> operator (pretty "≡") <+> go False 0 y
IElim _a _x _y f i -> instead (App Ex f i)
PathIntro _a _x _y f -> instead f
@ -116,18 +120,18 @@ prettyTm = go True 0 where
let
face (f, t) = go False 0 f <+> operator (pretty "=>") <+> align (go False 0 t)
in
braces (line <> indent 2 (vsep (map face (Map.toList fs))) <> line)
braces (line <> indent 2 (align (vsep (punctuate comma (map face (Map.toList fs))))) <> line)
Sub a phi u -> apps (con "Sub") [(Ex, a), (Ex, phi), (Ex, u)]
Inc a phi u -> apps (con "inS") [(Ex, a), (Ex, phi), (Ex, u)]
Ouc a phi u a0 -> apps (con "outS") [(Ex, a), (Ex, phi), (Ex, u), (Ex, a0)]
Inc a phi u -> apps (con "inS") [(Im, a), (Im, phi), (Ex, u)]
Ouc a phi u a0 -> apps (con "outS") [(Im, a), (Im, phi), (Im, u), (Ex, a0)]
GlueTy a phi t e -> apps (con "primGlue") [(Ex, a), (Ex, phi), (Ex, t), (Ex, e)]
Glue _a _phi _ty _e t im -> apps (con "glue") [(Ex, t), (Ex, im)]
Unglue _a _phi _ty _e t -> apps (con "unglue") [(Ex, t)]
Comp a phi u a0 -> apps (con "comp") [(Ex, a), (Ex, phi), (Ex, u), (Ex, a0)]
HComp a phi u a0 -> apps (con "hcomp") [(Ex, a), (Ex, phi), (Ex, u), (Ex, a0)]
Comp a phi u a0 -> apps (con "comp") [(Ex, a), (Im, phi), (Ex, u), (Ex, a0)]
HComp a phi u a0 -> apps (con "hcomp") [(Im, a), (Im, phi), (Ex, u), (Ex, a0)]
Case _ t cs ->
let
@ -162,7 +166,7 @@ prettyTm = go True 0 where
| otherwise = x
con x = Con (Bound (T.pack x) 0)
plic = \case
Ex -> parens
Im -> braces
@ -170,24 +174,43 @@ prettyTm = go True 0 where
arrow = operator (pretty "->")
instead = go t p
apps :: Term -> [(Plicity, Term)] -> Doc AnsiStyle
apps :: Term -> [(Plicity, Term)] -> Doc AnsiStyle
apps f xs = instead (foldl (\f (p, x) -> App p f x) f xs)
prettyBinds :: [(Name, Term, Term)] -> Doc AnsiStyle
prettyBinds [] = mempty
prettyBinds ((x, ty, tm):bs) =
pretty x <+> colon <+> align (prettyTm ty)
prettyBinds :: Bool -> [(Name, Term, Term)] -> Doc AnsiStyle
prettyBinds _ [] = mempty
prettyBinds imp ((x, ty, tm):bs) =
pretty x <+> colon <+> align (prettyTm' imp ty)
<> line
<> pretty x <+> equals <+> align (prettyTm tm)
<> pretty x <+> equals <+> align (prettyTm' imp tm)
<> line
<> prettyBinds bs
<> prettyBinds imp bs
showFace :: Map Head Bool -> Doc AnsiStyle
showFace = hsep . map go . Map.toList where
go (h, b) = parens $ prettyTm (quote (VNe h mempty)) <+> operator (pretty "=") <+> pretty (if b then "i1" else "i0")
showFace :: Bool -> Map Head Bool -> Doc AnsiStyle
showFace imp = hsep . map go . Map.toList where
go (h, b) = parens $ prettyTm' imp (quote (VNe h mempty)) <+> operator (pretty "=") <+> pretty (if b then "i1" else "i0")
prettyVl' :: Bool -> Value -> Doc AnsiStyle
prettyVl' b = prettyTm' b . quote
instance Pretty Term where
pretty = unAnnotate . prettyTm
prettyTm :: Term -> Doc AnsiStyle
prettyTm = prettyTm' printImplicits
instance Pretty Value where
pretty = unAnnotate . prettyVl
prettyVl :: Value -> Doc AnsiStyle
prettyVl = prettyTm . quote
prettyVl = prettyVl' printImplicits
printImplicits :: Bool
#if defined(RELEASE)
printImplicits = False
#else
printImplicits = True
#endif
render :: Doc AnsiStyle -> Text
render = L.toStrict . renderLazy . layoutSmart defaultLayoutOptions
@ -203,4 +226,4 @@ keyword :: Doc AnsiStyle -> Doc AnsiStyle
keyword = annotate (color Magenta)
operator :: Doc AnsiStyle -> Doc AnsiStyle
operator = annotate (color Yellow)
operator = annotate (color Yellow)

Write Preview
Loading…
Cancel
Save