Compare commits

...

No commits in common. 'master' and 'feature/hits' have entirely different histories.

19 changed files with 1070 additions and 2801 deletions
Unified View
  1. +2
    -3
      cubical.cabal
  2. +240
    -1541
      intro.tt
  3. +0
    -45
      src/Debug.hs
  4. +90
    -94
      src/Elab.hs
  5. +192
    -292
      src/Elab/Eval.hs
  6. +11
    -31
      src/Elab/Eval/Formula.hs
  7. +0
    -18
      src/Elab/Eval/Formula.hs-boot
  8. +5
    -27
      src/Elab/Monad.hs
  9. +131
    -259
      src/Elab/WiredIn.hs
  10. +11
    -18
      src/Elab/WiredIn.hs-boot
  11. +57
    -124
      src/Main.hs
  12. +2
    -20
      src/Presyntax/Lexer.x
  13. +22
    -20
      src/Presyntax/Parser.y
  14. +5
    -2
      src/Presyntax/Presyntax.hs
  15. +0
    -2
      src/Presyntax/Tokens.hs
  16. +55
    -97
      src/Syntax.hs
  17. +179
    -202
      src/Syntax/Pretty.hs
  18. +64
    -2
      stack.yaml
  19. +4
    -4
      stack.yaml.lock

+ 2
- 3
cubical.cabal View File

@ -46,9 +46,8 @@ executable cubical
, Elab.WiredIn , Elab.WiredIn
, Elab.Eval.Formula , Elab.Eval.Formula
, Debug
build-tool-depends: alex:alex >= 3.2.4 && < 4.0 build-tool-depends: alex:alex >= 3.2.4 && < 4.0
, happy:happy >= 1.19.12 && < 2.0 , happy:happy >= 1.19.12 && < 2.0
ghc-options: -Wall -Wextra -Wno-name-shadowing -rtsopts
ghc-options: -Wall -Wextra -Wno-name-shadowing

+ 240
- 1541
intro.tt
File diff suppressed because it is too large
View File


+ 0
- 45
src/Debug.hs View File

@ -1,45 +0,0 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE BangPatterns #-}
#undef RELEASE
module Debug where
import qualified Debug.Trace as D
#if defined(RELEASE)
import GHC.Exts
#endif
import GHC.Stack
import Prettyprinter
import qualified Data.Text.Lazy as T
import Data.Text.Prettyprint.Doc.Render.Text (renderLazy)
traceDoc :: Doc a -> b -> b
#if defined(RELEASE)
type DebugCallStack = (() :: Constraint)
traceDoc !_ v = v
#else
type DebugCallStack = HasCallStack
traceDoc x = D.trace (T.unpack (renderLazy (layoutPretty defaultLayoutOptions 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 x)
traceId :: Pretty a => a -> a
traceId x = traceDoc (pretty x) x
traceWithId :: Pretty a => String -> a -> a
traceWithId s x = traceWith s x x
traceDocM :: (Applicative m) => Doc a -> m ()
traceDocM x = traceDoc x (pure ())
traceM :: (Applicative m, Pretty a) => a -> m ()
traceM = traceDocM . pretty

+ 90
- 94
src/Elab.hs View File

@ -4,7 +4,6 @@
{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyCase #-}
module Elab where module Elab where
import Control.Arrow (Arrow(first)) import Control.Arrow (Arrow(first))
@ -15,7 +14,6 @@ import qualified Data.Map.Strict as Map
import qualified Data.Sequence as Seq import qualified Data.Sequence as Seq
import qualified Data.Set as Set import qualified Data.Set as Set
import qualified Data.Text as T import qualified Data.Text as T
import Data.Maybe (fromMaybe)
import Data.Traversable import Data.Traversable
import Data.Text (Text) import Data.Text (Text)
import Data.Map (Map) import Data.Map (Map)
@ -33,6 +31,7 @@ import Prettyprinter
import Syntax.Pretty import Syntax.Pretty
import Syntax import Syntax
import Data.Maybe (fromMaybe)
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
@ -55,10 +54,10 @@ infer (P.App p f x) = do
x_nf <- eval x x_nf <- eval x
pure (IElim (quote (fun li)) (quote le) (quote ri) (wp f) x, li x_nf) pure (IElim (quote (fun li)) (quote le) (quote ri) (wp f) x, li x_nf)
It'sPartial phi a w -> do It'sPartial phi a w -> do
x <- check x (VEqStrict VI phi VI1)
x <- check x (VIsOne phi)
pure (App P.Ex (w f) x, a) pure (App P.Ex (w f) x, a)
It'sPartialP phi a w -> do It'sPartialP phi a w -> do
x <- check x (VEqStrict VI phi VI1)
x <- check x (VIsOne phi)
x_nf <- eval x x_nf <- eval x
pure (App P.Ex (w f) x, a @@ x_nf) pure (App P.Ex (w f) x, a @@ x_nf)
@ -102,17 +101,20 @@ check (P.Lam p v b) ty = do
tm_nf <- eval tm tm_nf <- eval tm
unify (tm_nf @@ VI0) le `catchElab` (throwElab . WhenCheckingEndpoint (Bound v 0) le ri VI0)
unify (tm_nf @@ VI1) ri `catchElab` (throwElab . WhenCheckingEndpoint (Bound v 0) le ri VI1)
unify (tm_nf @@ VI0) le
`catchElab` (throwElab . WhenCheckingEndpoint le ri VI0)
unify (tm_nf @@ VI1) ri
`catchElab` (throwElab . WhenCheckingEndpoint le ri VI1)
pure (wp (PathIntro (quote (fun li)) (quote le) (quote ri) tm)) pure (wp (PathIntro (quote (fun li)) (quote le) (quote ri) tm))
It'sPartial phi a wp -> It'sPartial phi a wp ->
assume (Bound v 0) (VEqStrict VI phi VI1) $ \var ->
assume (Bound v 0) (VIsOne phi) $ \var ->
wp . Lam p var <$> check b a wp . Lam p var <$> check b a
It'sPartialP phi a wp -> It'sPartialP phi a wp ->
assume (Bound v 0) (VEqStrict VI phi VI1) $ \var ->
assume (Bound v 0) (VIsOne phi) $ \var ->
wp . Lam p var <$> check b (a @@ VVar var) wp . Lam p var <$> check b (a @@ VVar var)
check (P.Pair a b) ty = do check (P.Pair a b) ty = do
@ -145,36 +147,54 @@ check (P.Let items body) ty = do
check (P.LamSystem bs) ty = do check (P.LamSystem bs) ty = do
(extent, dom) <- isPartialType ty (extent, dom) <- isPartialType ty
env <- ask
eqns <- for bs \(formula, rhs) -> do
(phi, fv) <- checkFormula formula
n <- newName
rhses <- for (truthAssignments phi (getEnv env)) $ \e -> do
let env' = env{ getEnv = e }
local (const env') $
check rhs (substitute (snd <$> Map.restrictKeys e fv) (dom (VVar n)))
let dom_q = quote dom
eqns <- for (zip [(0 :: Int)..] bs) $ \(n, (formula, rhs)) -> do
phi <- checkFormula (P.condF formula)
rhses <-
case P.condV formula of
Just t -> assume (Bound t 0) (VIsOne phi) $ \var -> do
env <- ask
for (truthAssignments phi (getEnv env)) $ \e -> do
let env' = env{ getEnv = e }
(Just var,) <$> check rhs (eval' env' dom_q)
Nothing -> do
env <- ask
for (truthAssignments phi (getEnv env)) $ \e -> do
let env' = env{ getEnv = e }
(Nothing,) <$> check rhs (eval' env' dom_q)
pure (n, (phi, head rhses)) pure (n, (phi, head rhses))
unify extent (foldl ior VI0 (map (fst . snd) eqns)) unify extent (foldl ior VI0 (map (fst . snd) eqns))
for_ eqns \(n, (formula, rhs)) -> do
for_ eqns $ \(n', (formula', rhs')) -> do
for_ eqns $ \(n, (formula, (binding, rhs))) -> do
let
k = case binding of
Just v -> assume v (VIsOne formula) . const
Nothing -> id
k $ for_ eqns $ \(n', (formula', (binding, rhs'))) -> do
let let
k = case binding of
Just v -> assume v (VIsOne formula) . const
Nothing -> id
truth = possible mempty (iand formula formula') truth = possible mempty (iand formula formula')
when ((n /= n') && fst truth) . for_ (truthAssignments (iand formula formula') (getEnv env)) $ \e -> do
let env' = env { getEnv = e }
vl = eval' env' rhs
vl' = eval' env' rhs'
add [] = id
add ((~(HVar x), True):xs) = redefine x VI VI1 . add xs
add ((~(HVar x), False):xs) = redefine x VI VI0 . add xs
k $ when ((n /= n') && fst truth) . add (Map.toList (snd truth)) $ do
vl <- eval rhs
vl' <- eval rhs'
unify vl vl' unify vl vl'
`withNote` vsep [ pretty "These two cases must agree because they are both possible:" `withNote` vsep [ pretty "These two cases must agree because they are both possible:"
, indent 2 $ pretty '*' <+> prettyTm (quote formula) <+> operator (pretty "=>") <+> pretty vl
, indent 2 $ pretty '*' <+> prettyTm (quote formula') <+> operator (pretty "=>") <+> pretty (zonk vl')
, 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 False (snd truth))
`withNote` (pretty "Consider this face, where both are true:" <+> showFace (snd truth))
name <- newName name <- newName
pure (Lam P.Ex name (System (Map.fromList (map (\(_, (x, y)) -> (quote x, y)) eqns))))
let
mkB name (Just v, b) = App P.Ex (Lam P.Ex v b) (Ref name)
mkB _ (Nothing, b) = b
pure (Lam P.Ex name (System (Map.fromList (map (\(_, (x, y)) -> (quote x, mkB name y)) eqns))))
check (P.LamCase pats) ty = check (P.LamCase pats) ty =
do do
@ -212,14 +232,12 @@ check (P.LamCase pats) ty =
let rhs = cases @@ side let rhs = cases @@ side
for_ (truthAssignments formula mempty) $ \i -> do for_ (truthAssignments formula mempty) $ \i -> do
let vl = foldl (\v n -> vApp P.Ex v (lookup n)) base (getBoundaryNames boundary) let vl = foldl (\v n -> vApp P.Ex v (lookup n)) base (getBoundaryNames boundary)
lookup n = fromMaybe (VVar n) (snd <$> (Map.lookup n i))
lookup n = fromMaybe VI0 (snd <$> (Map.lookup n i))
unify vl rhs 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" `withNote` vcat [ pretty "These must be the same because of the face"
, 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)
, indent 2 $ prettyTm (quote formula) <+> operator (pretty "=>") <+> prettyTm (quote (zonk side))
] ]
`withNote` (pretty "Mandated by the constructor" <+> prettyTm (quote pat_nf))
_ -> pure () _ -> pure ()
pure (pat, n_lams, wp rhs) pure (pat, n_lams, wp rhs)
@ -246,10 +264,6 @@ check (P.LamCase pats) ty =
boundaryFormulas (x:xs) k = boundaryFormulas xs $ k @@ VVar x boundaryFormulas (x:xs) k = boundaryFormulas xs $ k @@ VVar x
boundaryFormulas a b = error (show (a, b)) boundaryFormulas a b = error (show (a, b))
check P.Hole ty = do
t <- newMeta' True ty
pure (quote t)
check exp ty = do check exp ty = do
(tm, has) <- switch $ infer exp (tm, has) <- switch $ infer exp
wp <- isConvertibleTo has ty wp <- isConvertibleTo has ty
@ -316,11 +330,7 @@ skipLams k = do
(Lam P.Im n . ) <$> skipLams (k - 1) (Lam P.Im n . ) <$> skipLams (k - 1)
checkLetItems :: Map Text (Maybe (Name, NFType)) -> [P.LetItem] -> ([(Name, Term, Term)] -> ElabM a) -> ElabM a checkLetItems :: Map Text (Maybe (Name, NFType)) -> [P.LetItem] -> ([(Name, Term, Term)] -> ElabM a) -> ElabM a
checkLetItems map [] cont = do
for_ (Map.toList map) $ \case
(_, Nothing) -> pure ()
(n, Just _) -> throwElab $ DeclaredUndefined (Bound n 0)
cont []
checkLetItems _ [] cont = cont []
checkLetItems map (P.LetDecl v t:xs) cont = do checkLetItems map (P.LetDecl v t:xs) cont = do
t <- check t VTypeω t <- check t VTypeω
t_nf <- eval t t_nf <- eval t
@ -343,27 +353,21 @@ checkLetItems map (P.LetBind name rhs:xs) cont = do
checkLetItems (Map.insert (getNameText name) Nothing map) xs \xs -> checkLetItems (Map.insert (getNameText name) Nothing map) xs \xs ->
cont ((name, quote ty_nf, rhs):xs) cont ((name, quote ty_nf, rhs):xs)
checkFormula :: P.Formula -> ElabM (Value, Set.Set Name)
checkFormula P.FTop = pure (VI1, mempty)
checkFormula P.FBot = pure (VI0, mempty)
checkFormula (P.FAnd x y) = do
(x, f) <- checkFormula x
(y, f') <- checkFormula y
pure (iand x y, f <> f')
checkFormula (P.FOr x y) = do
(x, f) <- checkFormula x
(y, f') <- checkFormula y
pure (ior x y, f <> f')
checkFormula :: P.Formula -> ElabM Value
checkFormula P.FTop = pure VI1
checkFormula P.FBot = pure VI0
checkFormula (P.FAnd x y) = iand <$> checkFormula x <*> checkFormula y
checkFormula (P.FOr x y) = ior <$> checkFormula x <*> checkFormula y
checkFormula (P.FIs0 x) = do checkFormula (P.FIs0 x) = do
nm <- getNameFor x nm <- getNameFor x
ty <- getNfType nm ty <- getNfType nm
unify ty VI unify ty VI
pure (inot (VVar nm), Set.singleton nm)
pure (inot (VVar nm))
checkFormula (P.FIs1 x) = do checkFormula (P.FIs1 x) = do
nm <- getNameFor x nm <- getNameFor x
ty <- getNfType nm ty <- getNfType nm
unify ty VI unify ty VI
pure (VVar nm, Set.singleton nm)
pure (VVar nm)
isSort :: NFType -> ElabM () isSort :: NFType -> ElabM ()
isSort t = isSort (force t) where isSort t = isSort (force t) where
@ -425,15 +429,15 @@ isSigmaType t = isSigmaType (force t) where
wp <- isConvertibleTo t (VSigma dom (Closure name (const rng))) wp <- isConvertibleTo t (VSigma dom (Closure name (const rng)))
pure (dom, const rng, wp) pure (dom, const rng, wp)
isPartialType :: NFType -> ElabM (NFEndp, Value -> Value)
isPartialType :: NFType -> ElabM (NFEndp, Value)
isPartialType t = isPartialType (force t) where isPartialType t = isPartialType (force t) where
isPartialType (VPartial phi a) = pure (phi, const a)
isPartialType (VPartialP phi a) = pure (phi, (a @@))
isPartialType (VPartial phi a) = pure (phi, a)
isPartialType (VPartialP phi a) = pure (phi, a)
isPartialType t = do isPartialType t = do
phi <- newMeta VI phi <- newMeta VI
dom <- newMeta (VPartial phi VType) dom <- newMeta (VPartial phi VType)
unify t (VPartialP phi dom)
pure (phi, (dom @@))
unify t (VPartial phi dom)
pure (phi, dom)
checkStatement :: P.Statement -> ElabM a -> ElabM a checkStatement :: P.Statement -> ElabM a -> ElabM a
checkStatement (P.SpanSt s a b) k = withSpan a b $ checkStatement s k checkStatement (P.SpanSt s a b) k = withSpan a b $ checkStatement s k
@ -492,21 +496,21 @@ checkStatement (P.ReplNf e) k = do
(e, _) <- infer e (e, _) <- infer e
e_nf <- eval e e_nf <- eval e
h <- asks commHook h <- asks commHook
liftIO $ h . prettyVl =<< zonkIO e_nf
liftIO (h e_nf)
k k
checkStatement (P.ReplTy e) k = do checkStatement (P.ReplTy e) k = do
(t, ty) <- infer e
(_, ty) <- infer e
h <- asks commHook h <- asks commHook
liftIO (h (prettyTm t <+> colon <+> align (prettyVl (zonk ty))))
liftIO (h ty)
k k
checkStatement (P.Data name tele retk constrs) k = checkStatement (P.Data name tele retk constrs) k =
do do
checkTeleRetk tele retk \retk kind tele undef -> do
checkTeleRetk True tele retk \kind tele undef -> do
kind_nf <- eval kind kind_nf <- eval kind
defineInternal (Defined name 0) kind_nf (\name' -> GluedVl (mkHead name') mempty (VNe (mkHead name') mempty)) \name' ->
checkCons retk tele (VNe (mkHead name') (Seq.fromList (map makeProj tele))) constrs (local (markAsDef name' . undef) k)
defineInternal (Defined name 0) kind_nf (\name' -> VNe (mkHead name') mempty) \name' ->
checkCons tele (VNe (mkHead name') (Seq.fromList (map makeProj tele))) constrs (local (markAsDef name' . undef) k)
where where
makeProj (x, p, _) = PApp p (VVar x) makeProj (x, p, _) = PApp p (VVar x)
@ -516,22 +520,26 @@ checkStatement (P.Data name tele retk constrs) k =
| 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 [] retk cont = do
checkTeleRetk allKan [] retk cont = do
t <- check retk VTypeω t <- check retk VTypeω
r <- eval t
cont r t [] id
checkTeleRetk ((x, p, t):xs) retk cont = do
t_nf <- eval t
when allKan $ unify t_nf VType
cont t [] id
checkTeleRetk allKan ((x, p, t):xs) retk cont = do
(t, ty) <- infer t (t, ty) <- infer t
_ <- isConvertibleTo ty VTypeω _ <- isConvertibleTo ty VTypeω
let
allKan' = case ty of
VType -> allKan
_ -> False
t_nf <- eval t t_nf <- eval t
let rm nm e = e{ nameMap = Map.delete (getNameText nm) (nameMap e), getEnv = Map.delete nm (getEnv e) } let rm nm e = e{ nameMap = Map.delete (getNameText nm) (nameMap e), getEnv = Map.delete nm (getEnv e) }
assume (Bound x 0) t_nf $ \nm -> checkTeleRetk xs retk \ret k xs w -> cont ret (Pi p nm t k) ((nm, p, t_nf):xs) (rm nm . w)
assume (Bound x 0) t_nf $ \nm -> checkTeleRetk allKan' xs retk \k xs w -> cont (Pi p nm t k) ((nm, p, t_nf):xs) (rm nm . w)
checkCons _ _ _et [] k = k
checkCons _ _et [] k = k
checkCons retk n ret ((s, e, P.Point x ty):xs) k = withSpan s e $ do
t <- check ty retk
checkCons n ret ((s, e, P.Point x ty):xs) k = withSpan s e $ do
t <- check ty VTypeω
ty_nf <- eval t ty_nf <- eval t
let let
(args, ret') = splitPi ty_nf (args, ret') = splitPi ty_nf
@ -539,12 +547,11 @@ checkStatement (P.Data name tele retk constrs) k =
n' = map (\(x, _, y) -> (x, P.Im, y)) n n' = map (\(x, _, y) -> (x, P.Im, y)) n
unify ret' ret unify ret' ret
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 retk 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 retk n ret ((s, e, P.Path name indices return faces):xs) k = withSpan s e $ do
fibrant retk
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 retk
t <- check return VTypeω
ty_nf <- eval t ty_nf <- eval t
let let
(args, ret') = splitPi ty_nf (args, ret') = splitPi ty_nf
@ -561,17 +568,17 @@ checkStatement (P.Data name tele retk constrs) k =
unify ret' ret unify ret' ret
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 (phi, (quote phi, t)) pure (phi, (quote phi, t))
system <- eval $ foldr (\x -> Lam P.Ex x) (System (Map.fromList (map snd 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 (foldl ior VI0 (map fst faces)) (totalProp 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" `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 retk n ret xs k
defineInternal con closed_nf value \name -> addBoundary name boundary $ checkCons n ret xs k
close [] t = t close [] t = t
close ((x, _, y):xs) t = Pi P.Im x (quote y) (close xs t) close ((x, _, y):xs) t = Pi P.Im x (quote y) (close xs t)
@ -588,13 +595,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 (VVar x) (inot (VVar x) `ior` totalProp xs)
totalProp (x:xs) = ior (inot (VVar x)) (VVar x) `ior` totalProp xs
totalProp [] = VI0 totalProp [] = VI0
fibrant VTypeω = throwElab PathConPretype
fibrant VType = pure ()
fibrant x = error $ "not a constructor kind: " ++ show x
checkProgram :: [P.Statement] -> ElabM a -> ElabM a checkProgram :: [P.Statement] -> ElabM a -> ElabM a
checkProgram [] k = k checkProgram [] k = k
@ -603,7 +606,7 @@ checkProgram (st:sts) k = checkStatement st $ checkProgram sts k
newtype Redefinition = Redefinition { getRedefName :: Name } newtype Redefinition = Redefinition { getRedefName :: Name }
deriving (Show, Typeable, Exception) deriving (Show, Typeable, Exception)
data WhenCheckingEndpoint = WhenCheckingEndpoint { direction :: Name, leftEndp :: Value, rightEndp :: Value, whichIsWrong :: NFEndp, exc :: SomeException }
data WhenCheckingEndpoint = WhenCheckingEndpoint { leftEndp :: Value, rightEndp :: Value, whichIsWrong :: NFEndp, exc :: SomeException }
deriving (Show, Typeable, Exception) deriving (Show, Typeable, Exception)
data UnsaturatedCon = UnsaturatedCon { theConstr :: Name } data UnsaturatedCon = UnsaturatedCon { theConstr :: Name }
@ -613,10 +616,3 @@ data UnsaturatedCon = UnsaturatedCon { theConstr :: Name }
data NotACon = NotACon { theNotConstr :: Name } data NotACon = NotACon { theNotConstr :: Name }
deriving (Show, Typeable) deriving (Show, Typeable)
deriving anyclass (Exception) deriving anyclass (Exception)
data PathConPretype = PathConPretype
deriving (Show, Typeable)
deriving anyclass (Exception)
newtype DeclaredUndefined = DeclaredUndefined { declaredUndefName :: Name }
deriving (Eq, Show, Exception)

+ 192
- 292
src/Elab/Eval.hs View File

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

+ 11
- 31
src/Elab/Eval/Formula.hs View File

@ -2,38 +2,22 @@ module Elab.Eval.Formula where
import qualified Data.Map.Strict as Map import qualified Data.Map.Strict as Map
import qualified Data.Sequence as Seq import qualified Data.Sequence as Seq
import qualified Data.Set as Set
import Data.Map.Strict (Map) import Data.Map.Strict (Map)
import Data.Set (Set)
import Syntax import Syntax
import {-# SOURCE #-} Elab.WiredIn (inot, ior, iand) import {-# SOURCE #-} Elab.WiredIn (inot, ior, iand)
import Elab.Eval (substitute, trueCaseSentinel)
toDnf :: Value -> Maybe Value toDnf :: Value -> Maybe Value
toDnf = fmap (dnf2Val . normalise) . val2Dnf where
val2Dnf (VNe _ _) = Nothing
val2Dnf x = toDnf x where
toDnf (VIAnd x y) = idist <$> toDnf (inot x) <*> toDnf (inot y)
toDnf (VIOr x y) = ior <$> toDnf x <*> toDnf y
toDnf (VINot x) = inot <$> toDnf x
toDnf VI0 = pure VI0
toDnf VI1 = pure VI1
toDnf v@(VNe _ Seq.Empty) = pure v
toDnf _ = Nothing
dnf2Val xs = Set.foldl ior VI0 (Set.map (Set.foldl iand VI1) xs)
type Nf = Set (Set Value)
normalise :: Value -> Nf
normalise = normaliseOr where
normaliseOr (VIOr x y) = Set.singleton (normaliseAnd x) <> normaliseOr y
normaliseOr x = Set.singleton (normaliseAnd x)
normaliseAnd (VIAnd x y) = Set.insert x (normaliseAnd y)
normaliseAnd x = Set.singleton x
toDnf (VNe _ _) = Nothing
toDnf x = toDnf x where
toDnf (VIAnd x y) = idist <$> toDnf (inot x) <*> toDnf (inot y)
toDnf (VIOr x y) = ior <$> toDnf x <*> toDnf y
toDnf (VINot x) = inot <$> toDnf x
toDnf VI0 = pure VI0
toDnf VI1 = pure VI1
toDnf v@(VNe _ Seq.Empty) = pure v
toDnf _ = Nothing
compareDNFs :: Value -> Value -> Bool compareDNFs :: Value -> Value -> Bool
compareDNFs (VIOr x y) (VIOr x' y') = compareDNFs (VIOr x y) (VIOr x' y') =
@ -76,14 +60,10 @@ truthAssignments VI0 _ = []
truthAssignments VI1 m = pure m truthAssignments VI1 m = pure m
truthAssignments (VIOr x y) m = truthAssignments x m ++ truthAssignments y m truthAssignments (VIOr x y) m = truthAssignments x m ++ truthAssignments y m
truthAssignments (VIAnd x y) m = truthAssignments x =<< truthAssignments y m truthAssignments (VIAnd x y) m = truthAssignments x =<< truthAssignments y m
truthAssignments (VNe (HVar x) Seq.Empty) m = pure (Map.insert x (VI, VI1) (sub x VI1 <$> m))
truthAssignments (VINot (VNe (HVar x) Seq.Empty)) m = pure (Map.insert x (VI, VI0) (sub x VI0 <$> m))
truthAssignments (VCase _ _ (VNe (HVar x) _) _) m = pure (Map.insert x (VI, VVar trueCaseSentinel) m)
truthAssignments (VNe (HVar x) Seq.Empty) m = pure (Map.insert x (VI, VI1) m)
truthAssignments (VINot (VNe (HVar x) Seq.Empty)) m = pure (Map.insert x (VI, VI0) m)
truthAssignments _ m = pure m truthAssignments _ m = pure m
sub :: Name -> Value -> (NFType, NFEndp) -> (Value, Value)
sub x v (a, b) = (substitute (Map.singleton x v) a, substitute (Map.singleton x v) b)
idist :: Value -> Value -> Value idist :: Value -> Value -> Value
idist (VIOr x y) z = (x `idist` z) `ior` (y `idist` z) idist (VIOr x y) z = (x `idist` z) `ior` (y `idist` z)
idist z (VIOr x y) = (z `idist` x) `ior` (z `idist` y) idist z (VIOr x y) = (z `idist` x) `ior` (z `idist` y)


+ 0
- 18
src/Elab/Eval/Formula.hs-boot View File

@ -1,18 +0,0 @@
module Elab.Eval.Formula where
import Syntax
import Data.Map.Strict (Map)
import Data.Set (Set)
toDnf :: Value -> Maybe Value
type Nf = Set (Set Value)
normalise :: Value -> Nf
compareDNFs :: Value -> Value -> Bool
swap :: Ord b => b -> b -> (b, b)
possible :: Map Head Bool -> Value -> (Bool, Map Head Bool)
truthAssignments :: NFEndp -> Map Name (NFType, NFEndp) -> [Map Name (NFType, NFEndp)]

+ 5
- 27
src/Elab/Monad.hs View File

@ -26,19 +26,17 @@ data ElabEnv =
, nameMap :: Map Text Name , nameMap :: Map Text Name
, pingPong :: {-# UNPACK #-} !Int , pingPong :: {-# UNPACK #-} !Int
, commHook :: Doc AnsiStyle -> IO ()
, commHook :: Value -> IO ()
, currentSpan :: Maybe (P.Posn, P.Posn) , currentSpan :: Maybe (P.Posn, P.Posn)
, currentFile :: Maybe Text , currentFile :: Maybe Text
, whereBound :: Map Name (P.Posn, P.Posn)
, whereBound :: Map Name (P.Posn, P.Posn)
, definedNames :: Set Name , definedNames :: Set Name
, boundaries :: Map Name Boundary
, boundaries :: Map Name Boundary
, unsolvedMetas :: {-# UNPACK #-} !(IORef (Map MV [(Seq Projection, Value)])) , unsolvedMetas :: {-# UNPACK #-} !(IORef (Map MV [(Seq Projection, Value)]))
, loadedFiles :: [String]
} }
newtype ElabM a = ElabM { runElab :: ElabEnv -> IO a } newtype ElabM a = ElabM { runElab :: ElabEnv -> IO a }
@ -46,24 +44,7 @@ newtype ElabM a = ElabM { runElab :: ElabEnv -> IO a }
via ReaderT ElabEnv IO via ReaderT ElabEnv IO
emptyEnv :: IO ElabEnv emptyEnv :: IO ElabEnv
emptyEnv = do
u <- newIORef mempty
pure $ ElabEnv { getEnv = mempty
, nameMap = mempty
, pingPong = 0
, commHook = const (pure ())
, currentSpan = Nothing
, currentFile = Nothing
, whereBound = mempty
, definedNames = mempty
, boundaries = mempty
, unsolvedMetas = u
, loadedFiles = []
}
emptyEnv = ElabEnv mempty mempty 0 (const (pure ())) Nothing Nothing mempty mempty mempty <$> newIORef mempty
addBoundary :: Name -> Boundary -> ElabM a -> ElabM a addBoundary :: Name -> Boundary -> ElabM a -> ElabM a
addBoundary nm boundary = local (\e -> e { boundaries = Map.insert nm boundary (boundaries e)} ) addBoundary nm boundary = local (\e -> e { boundaries = Map.insert nm boundary (boundaries e)} )
@ -137,13 +118,10 @@ switch :: ElabM a -> ElabM a
switch k = switch k =
do do
depth <- asks pingPong depth <- asks pingPong
when (depth >= 128) $ error "stack overflow"
when (depth >= 128) $ throwElab StackOverflow
local go k local go k
where go e = e { pingPong = pingPong e + 1 } where go e = e { pingPong = pingPong e + 1 }
shallowly :: ElabM a -> ElabM a
shallowly = local (\e -> e { pingPong = 0 })
newtype NotInScope = NotInScope { nameNotInScope :: Name } newtype NotInScope = NotInScope { nameNotInScope :: Name }
deriving (Show, Typeable) deriving (Show, Typeable)
deriving anyclass (Exception) deriving anyclass (Exception)


+ 131
- 259
src/Elab/WiredIn.hs View File

@ -4,37 +4,9 @@
{-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE ViewPatterns #-} {-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# OPTIONS_GHC -fno-full-laziness #-}
module Elab.WiredIn
( wiType
, wiValue
, wiredInNames
, NoSuchPrimitive(..)
, iand
, ior
, inot
, ielim
, incS
, outS
, comp
, fill
, hComp
, glueType
, glueElem
, unglue
, fun
, system
, strictK
, strictJ
, projIntoCase
)
where
module Elab.WiredIn where
import Control.Exception ( assert, Exception )
import Control.Exception
import qualified Data.Map.Strict as Map import qualified Data.Map.Strict as Map
import qualified Data.Sequence as Seq import qualified Data.Sequence as Seq
@ -43,19 +15,16 @@ import Data.Map.Strict (Map)
import Data.Text (Text) import Data.Text (Text)
import Data.Typeable import Data.Typeable
import Debug
import Elab.Eval import Elab.Eval
import GHC.Stack (HasCallStack) import GHC.Stack (HasCallStack)
import Presyntax.Presyntax (Plicity(Im, Ex))
import qualified Presyntax.Presyntax as P import qualified Presyntax.Presyntax as P
import Syntax.Pretty (prettyTm, prettyVl)
import Syntax.Pretty (prettyTm)
import Syntax import Syntax
import System.IO.Unsafe ( unsafePerformIO )
import System.IO.Unsafe
wiType :: WiredIn -> NFType wiType :: WiredIn -> NFType
wiType WiType = VType wiType WiType = VType
@ -70,28 +39,25 @@ wiType WiIOr = VI ~> VI ~> VI
wiType WiINot = VI ~> VI wiType WiINot = VI ~> VI
wiType WiPathP = dprod (VI ~> VType) \a -> a @@ VI0 ~> a @@ VI1 ~> VType wiType WiPathP = dprod (VI ~> VType) \a -> a @@ VI0 ~> a @@ VI1 ~> VType
wiType WiIsOne = VI ~> VTypeω
wiType WiItIsOne = VIsOne VI1
wiType WiPartial = VI ~> VType ~> VTypeω wiType WiPartial = VI ~> VType ~> VTypeω
wiType WiPartialP = dprod VI \x -> VPartial x VType ~> VTypeω wiType WiPartialP = dprod VI \x -> VPartial x VType ~> VTypeω
wiType WiPOr = forAll VType \a -> dprod VI \phi -> dprod VI \psi -> VPartial phi a ~> VPartial psi a ~> VPartial (ior phi psi) a
wiType WiSub = dprod VType \a -> dprod VI \phi -> VPartial phi a ~> VTypeω wiType WiSub = dprod VType \a -> dprod VI \phi -> VPartial phi a ~> VTypeω
wiType WiInS = forAll VType \a -> forAll VI \phi -> dprod a \u -> VSub a phi (fun (const u)) wiType WiInS = forAll VType \a -> forAll VI \phi -> dprod a \u -> VSub a phi (fun (const u))
wiType WiOutS = forAll VType \a -> forAll VI \phi -> forAll (VPartial phi a) \u -> VSub a phi u ~> a wiType WiOutS = forAll VType \a -> forAll VI \phi -> forAll (VPartial phi a) \u -> VSub a phi u ~> a
wiType WiComp = dprod' "A" (VI ~> VType) \a -> forAll VI \phi -> dprod (dprod VI \i -> VPartial phi (a @@ i)) \u -> VSub (a @@ VI0) phi (u @@ VI0) ~> VSub (a @@ VI1) phi (u @@ VI1)
wiType WiComp = dprod' "A" (VI ~> VType) \a -> forAll VI \phi -> dprod (dprod VI \i -> VPartial phi (a @@ i)) \u -> VSub (a @@ VI0) phi (u @@ VI0) ~> a @@ VI1
-- (A : Type) {phi : I} (T : Partial phi Type) (e : PartialP phi (\o -> Equiv (T o) A)) -> Type
wiType WiGlue = dprod' "A" VType \a -> forAll' "phi" VI \phi -> dprod' "T" (VPartial phi VType) \t -> VPartialP phi (fun \o -> equiv (t @@ o) a) ~> VType wiType WiGlue = dprod' "A" VType \a -> forAll' "phi" VI \phi -> dprod' "T" (VPartial phi VType) \t -> VPartialP phi (fun \o -> equiv (t @@ o) a) ~> VType
-- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> (t : PartialP phi T) -> Sub A phi (\o -> e o (t o)) -> Glue A phi T e
wiType WiGlueElem = forAll' "A" VType \a -> forAll' "phi" VI \phi -> forAll' "T" (VPartial phi VType) \ty -> forAll' "e" (VPartialP phi (fun \o -> equiv (ty @@ o) a)) \eqv -> wiType WiGlueElem = forAll' "A" VType \a -> forAll' "phi" VI \phi -> forAll' "T" (VPartial phi VType) \ty -> forAll' "e" (VPartialP phi (fun \o -> equiv (ty @@ o) a)) \eqv ->
dprod' "t" (VPartialP phi ty) \t -> VSub a phi (fun \o -> vProj1 (eqv @@ o) @@ (t @@ o)) ~> VGlueTy a phi ty eqv dprod' "t" (VPartialP phi ty) \t -> VSub a phi (fun \o -> vProj1 (eqv @@ o) @@ (t @@ o)) ~> VGlueTy a phi ty eqv
-- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> Glue A phi T e -> A
wiType WiUnglue = forAll' "A" VType \a -> forAll' "phi" VI \phi -> forAll' "T" (VPartial phi VType) \ty -> forAll' "e" (VPartialP phi (fun \o -> equiv (ty @@ o) a)) \e -> VGlueTy a phi ty e ~> a wiType WiUnglue = forAll' "A" VType \a -> forAll' "phi" VI \phi -> forAll' "T" (VPartial phi VType) \ty -> forAll' "e" (VPartialP phi (fun \o -> equiv (ty @@ o) a)) \e -> VGlueTy a phi ty e ~> a
wiType WiSEq = forAll' "A" VTypeω \a -> a ~> a ~> VTypeω
wiType WiSRefl = forAll' "A" VTypeω \a -> forAll' "x" a \x -> VEqStrict a x x
wiType WiSK = forAll' "A" VTypeω \a -> forAll' "x" a \x -> dprod' "P" (VEqStrict a x x ~> VTypeω) \bigp -> (bigp @@ VReflStrict a x) ~> dprod' "p" (VEqStrict a x x) \p -> bigp @@ p
wiType WiSJ = forAll' "A" VTypeω \a -> forAll' "x" a \x -> dprod' "P" (dprod' "y" a \y -> VEqStrict a x y ~> VTypeω) \bigp -> bigp @@ x @@ VReflStrict a x ~> forAll' "y" a \y -> dprod' "p" (VEqStrict a x y) \p -> bigp @@ y @@ p
wiType WiLineToEquiv = dprod' "P" (VI ~> VType) \a -> equiv (a @@ VI0) (a @@ VI1)
wiValue :: WiredIn -> Value wiValue :: WiredIn -> Value
wiValue WiType = VType wiValue WiType = VType
wiValue WiPretype = VTypeω wiValue WiPretype = VTypeω
@ -100,35 +66,25 @@ wiValue WiInterval = VI
wiValue WiI0 = VI0 wiValue WiI0 = VI0
wiValue WiI1 = VI1 wiValue WiI1 = VI1
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 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 WiPartial = functions [(Ex, "phi"), (Ex, "A")] \[phi, a] -> VPartial phi a
wiValue WiPartialP = functions [(Ex, "phi"), (Ex, "A")] \[phi, a] -> VPartialP phi a
wiValue WiPOr = functions [(Im, "A"), (Ex, "phi"), (Ex, "psi"), (Ex, "a"), (Ex, "b")] \[_, phi, psi, a, b] -> mkVSystem (Map.fromList [(phi, a), (psi, b)])
wiValue WiIsOne = fun VIsOne
wiValue WiItIsOne = VItIsOne
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 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 -> comp a phi u x
wiValue WiGlue = fun \a -> forallI \phi -> fun \t -> fun \e -> glueType a phi t e 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 wiValue WiGlueElem = forallI \a -> forallI \phi -> forallI \ty -> forallI \eqv -> fun \x -> fun \y -> glueElem a phi ty eqv x y
wiValue WiUnglue = forallI \a -> forallI \phi -> forallI \ty -> forallI \eqv -> fun \x -> unglue a phi ty eqv x wiValue WiUnglue = forallI \a -> forallI \phi -> forallI \ty -> forallI \eqv -> fun \x -> unglue a phi ty eqv x
wiValue WiSEq = forallI \a -> fun \x -> fun \y -> VEqStrict a x y
wiValue WiSRefl = forallI \a -> forallI \x -> VReflStrict a x
wiValue WiSK = forallI \a -> forallI \x -> fun \bigp -> fun \pr -> fun \p -> strictK a x bigp pr p
wiValue WiSJ = forallI \a -> forallI \x -> fun \bigp -> fun \pr -> forallI \y -> fun \p -> strictJ a x bigp pr y p
wiValue WiLineToEquiv = fun \l ->
GluedVl
(HVar (Defined "lineToEquiv" (-1)))
(Seq.fromList [(PApp P.Ex l)])
(makeEquiv' ((l @@) . inot))
(~>) :: Value -> Value -> Value (~>) :: Value -> Value -> Value
a ~> b = VPi P.Ex a (Closure (Bound "_" 0) (const b)) a ~> b = VPi P.Ex a (Closure (Bound "_" 0) (const b))
infixr 7 ~> infixr 7 ~>
@ -140,11 +96,6 @@ line k = VLam P.Ex $ Closure (Bound "i" 0) (k . force)
fun' :: String -> (Value -> Value) -> Value fun' :: String -> (Value -> Value) -> Value
fun' x k = VLam P.Ex $ Closure (Bound (T.pack x) 0) (k . force) 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 :: (Value -> Value) -> Value
forallI k = VLam P.Im $ Closure (Bound "x" 0) (k . force) forallI k = VLam P.Im $ Closure (Bound "x" 0) (k . force)
@ -166,6 +117,7 @@ forAll' n a b = VPi P.Im a (Closure (Bound (T.pack n) 0) b)
forAll :: Value -> (Value -> Value) -> Value forAll :: Value -> (Value -> Value) -> Value
forAll = forAll' "x" forAll = forAll' "x"
wiredInNames :: Map Text WiredIn wiredInNames :: Map Text WiredIn
wiredInNames = Map.fromList wiredInNames = Map.fromList
[ ("Pretype", WiPretype) [ ("Pretype", WiPretype)
@ -178,9 +130,11 @@ wiredInNames = Map.fromList
, ("inot", WiINot) , ("inot", WiINot)
, ("PathP", WiPathP) , ("PathP", WiPathP)
, ("IsOne", WiIsOne)
, ("itIs1", WiItIsOne)
, ("Partial", WiPartial) , ("Partial", WiPartial)
, ("PartialP", WiPartialP) , ("PartialP", WiPartialP)
, ("partialExt", WiPOr)
, ("Sub", WiSub) , ("Sub", WiSub)
, ("inS", WiInS) , ("inS", WiInS)
, ("outS", WiOutS) , ("outS", WiOutS)
@ -189,19 +143,14 @@ wiredInNames = Map.fromList
, ("Glue", WiGlue) , ("Glue", WiGlue)
, ("glue", WiGlueElem) , ("glue", WiGlueElem)
, ("unglue", WiUnglue) , ("unglue", WiUnglue)
, ("Eq_s", WiSEq)
, ("refl_s", WiSRefl)
, ("K_s", WiSK)
, ("J_s", WiSJ)
, ("lineToEquiv", WiLineToEquiv)
] ]
newtype NoSuchPrimitive = NoSuchPrimitive { getUnknownPrim :: Text } newtype NoSuchPrimitive = NoSuchPrimitive { getUnknownPrim :: Text }
deriving (Show, Typeable) deriving (Show, Typeable)
deriving anyclass (Exception) deriving anyclass (Exception)
-- Interval operations
iand, ior :: Value -> Value -> Value iand, ior :: Value -> Value -> Value
iand x = case force x of iand x = case force x of
VI1 -> id VI1 -> id
@ -250,30 +199,24 @@ ielim line left right fn i =
VNe n sp -> VNe n (sp Seq.:|> PIElim line left right i) VNe n sp -> VNe n (sp Seq.:|> PIElim line left right i)
VSystem map -> VSystem (fmap (flip (ielim line left right) i) map) VSystem map -> VSystem (fmap (flip (ielim line left right) i) map)
VInc (VPath _ _ _) _ u -> ielim line left right u i VInc (VPath _ _ _) _ u -> ielim line left right u i
VCase env r x xs -> VCase env r x (fmap (projIntoCase (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)) _ -> error $ "can't ielim " ++ show (prettyTm (quote fn))
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 :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value
outS _ (force -> VI1) u _ = u @@ VItIsOne
outS _ _phi _ (VInc _ _ x) = x outS _ _phi _ (VInc _ _ x) = x
outS _ VI0 _ 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 (VSystem fs) = mkVSystem (fmap (outS a phi u) fs)
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)) outS _ _ _ v = error $ "can't outS " ++ show (prettyTm (quote v))
comp :: DebugCallStack => NFLine -> NFEndp -> Value -> Value -> Value
comp _a (force -> VI1) u _a0 = u @@ VI1 @@ VReflStrict VI VI1
comp a psi@phi u incA0@(outS (a @@ VI0) phi (u @@ VI0) -> a0) =
-- Composition
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 name) of case force (a @@ VVar name) of
VPi{} -> VPi{} ->
let let
@ -281,21 +224,21 @@ comp a psi@phi u incA0@(outS (a @@ VI0) phi (u @@ VI0) -> a0) =
dom i = let VPi _ d _ = force (a @@ i) in d dom i = let VPi _ d _ = force (a @@ i) in d
rng i = let VPi _ _ (Closure _ r) = force (a @@ i) in r rng i = let VPi _ _ (Closure _ r) = force (a @@ i) in r
y' i y = fill (fun (dom . inot)) VI0 (fun \_ -> fun \_ -> VSystem mempty) (incS (dom VI0) phi y) i
y' i y = fill (fun (dom . inot)) VI0 (fun \_ -> fun \_ -> VSystem mempty) (VInc (dom VI0) phi y) i
ybar i y = y' (inot i) y ybar i y = y' (inot i) y
in VLam (plic VI1) . Closure (Bound "x" 0) $ \arg -> in VLam (plic VI1) . Closure (Bound "x" 0) $ \arg ->
comp (line \i -> rng i (ybar i arg)) comp (line \i -> rng i (ybar i arg))
phi phi
(system \i isone -> vApp (plic i) (u @@ i @@ isone) (ybar i arg)) (system \i isone -> vApp (plic i) (u @@ i @@ isone) (ybar i arg))
(incS (rng VI0 (ybar VI0 arg)) phi (vApp (plic VI0) a0 (ybar VI0 arg)))
(VInc (rng VI0 (ybar VI0 arg)) phi (vApp (plic VI0) a0 (ybar VI0 arg)))
VSigma{} -> VSigma{} ->
let let
dom i = let VSigma d _ = force (a @@ i) in d dom i = let VSigma d _ = force (a @@ i) in d
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)) (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))
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))
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 (w VI1) c2 VPair (w VI1) c2
@ -311,7 +254,7 @@ comp a psi@phi u incA0@(outS (a @@ VI0) phi (u @@ VI0) -> a0) =
(system \i isone -> mkVSystem (Map.fromList [ (phi, ielim (a' VI0) (u' VI0) (v' VI0) (u @@ i @@ isone) j) (system \i isone -> mkVSystem (Map.fromList [ (phi, ielim (a' VI0) (u' VI0) (v' VI0) (u @@ i @@ isone) j)
, (j, v' i) , (j, v' i)
, (inot j, u' i)])) , (inot j, u' i)]))
(incS (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 _ thePhi theTypes theEquivs -> VGlueTy _ thePhi theTypes theEquivs ->
let let
@ -322,20 +265,20 @@ comp a psi@phi u incA0@(outS (a @@ VI0) phi (u @@ VI0) -> a0) =
let let
base i = let VGlueTy b _ _ _ = forceAndGlue (fam @@ i) in b base i = let VGlueTy b _ _ _ = forceAndGlue (fam @@ i) in b
phi i = substitute (Map.singleton name i) thePhi phi i = substitute (Map.singleton name i) thePhi
types i = substitute (Map.singleton name i) theTypes @@ VReflStrict VI VI1
types i = substitute (Map.singleton name i) theTypes @@ VItIsOne
equivs i = substitute (Map.singleton name i) theEquivs equivs i = substitute (Map.singleton name i) theEquivs
a i u = unglue (base i) (phi i) (types i) (equivs i) (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 a0 = unglue (base VI0) (phi VI0) (types VI0) (equivs VI0) b0
del = faceForall phi del = faceForall phi
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)
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_st, omega_t, omega_rep) = pres types base equivs psi (b @@) b0
omega = outS omega_t psi omega_rep omega_st omega = outS omega_t psi omega_rep omega_st
(t1alpha_st, t1a_t, t1a_rep) = opEquiv (base VI1) (types VI1) (equivs VI1 @@ VReflStrict VI VI1) (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 t1alpha = outS t1a_t (del `ior` psi) t1a_rep t1alpha_st
(t1, alpha) = (vProj1 t1alpha, vProj2 t1alpha) (t1, alpha) = (vProj1 t1alpha, vProj2 t1alpha)
@ -344,38 +287,37 @@ comp a psi@phi u incA0@(outS (a @@ VI0) phi (u @@ VI0) -> a0) =
ps _isone = mkVSystem . Map.fromList $ [(del, omega), (psi, VLine (line (const (base VI1))) a1' a1' (fun (const a1')))] ps _isone = mkVSystem . Map.fromList $ [(del, omega), (psi, VLine (line (const (base VI1))) a1' a1' (fun (const a1')))]
a1 = comp a1 = comp
(fun (const (base VI1)))
(del `ior` psi)
(system \j _u -> mkVSystem (Map.fromList [ (del, ielim (base VI1) a1' (vProj1 (equivs VI1 @@ VReflStrict VI VI1)) alpha j)
, (psi, a psi _u)
]))
(incS (base VI1) (phi VI1 `ior` psi) a1')
b1 = glueElem (base VI1) (phi VI1) (types VI1) (equivs VI1) (fun (const t1)) (incS (base VI1) (ior (del `ior` psi) (inot del `iand` inot psi)) a1)
(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 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 in b1
VType -> VGlueTy a0 phi (fun' "is1" \is1 -> u @@ VI1 @@ is1) VType -> VGlueTy a0 phi (fun' "is1" \is1 -> u @@ VI1 @@ is1)
(fun' "is1" \_ -> mapVSystem (makeEquiv equivVar) (u @@ VVar equivVar @@ VReflStrict VI VI1))
(fun' "is1" \_ -> mapVSystem (makeEquiv equivVar) (u @@ VVar equivVar @@ VItIsOne))
VNe (HData False _) Seq.Empty -> a0 VNe (HData False _) Seq.Empty -> a0
VNe (HData False _) args -> VNe (HData False _) args ->
case force a0 of case force a0 of
VNe (HCon con_type con_name) con_args -> 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 (incS (a @@ VI0) phi a0)
VNe (HCon con_type con_name) $ compConArgs (length args) (a @@) con_type con_args phi u
_ -> VComp a phi u (VInc (a @@ VI0) phi a0)
VNe (HData True _) args -> compHIT (length args) (a @@) phi u incA0
VNe (HData True name) args -> compHIT name (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 (incS (a @@ VI0) phi a0)
_ -> VComp a phi u (VInc (a @@ VI0) phi a0)
where where
{-# NOINLINE name #-} {-# NOINLINE name #-}
name :: Name
name = unsafePerformIO newName name = unsafePerformIO newName
{-# NOINLINE equivVar #-} {-# NOINLINE equivVar #-}
equivVar :: Name
equivVar = unsafePerformIO newName equivVar = unsafePerformIO newName
mapVSystem :: (Value -> Value) -> Value -> Value mapVSystem :: (Value -> Value) -> Value -> Value
mapVSystem f (VSystem fs) = VSystem (fmap f fs) mapVSystem f (VSystem fs) = VSystem (fmap f fs)
mapVSystem f x = f x mapVSystem f x = f x
@ -386,63 +328,60 @@ forceAndGlue v =
v@VGlueTy{} -> v v@VGlueTy{} -> v
y -> VGlueTy y VI1 (fun (const y)) (fun (const (idEquiv y))) y -> VGlueTy y VI1 (fun (const y)) (fun (const (idEquiv y)))
compHIT :: HasCallStack => Name -> Int -> (NFEndp -> NFSort) -> NFEndp -> Value -> Value -> Value
compHIT name n a phi u a0 =
case force phi of
VI1 -> u @@ VI1 @@ VReflStrict VI VI1
VI0 | n == 0 -> outS (a VI0) phi u a0
| regular -> 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 (outS (a VI0) phi (u @@ VI1 @@ VReflStrict VI VI1) a0))
regular = a VI0 == a VI1
compConArgs :: (Name -> Int -> Value -> t1 -> t2 -> Value -> Value)
-> Int
-> (Value -> Value)
-> Value
-> Seq.Seq Projection
-> t1 -> t2
-> Seq.Seq Projection
compConArgs makeFiller total_args fam = go total_args where
compHIT :: HasCallStack => Int -> (NFEndp -> NFSort) -> NFEndp -> Value -> Value -> Value
compHIT 0 a phi u a0 =
case phi of
VI1 -> u @@ VI1 @@ VItIsOne
VI0 -> compOutS (a VI0) phi u a0
_ -> VHComp (a VI0) phi u a0
compHIT _ a phi u a0 = error $ unlines
[ "*** TODO: composition for HIT: "
, "domain = " ++ show (prettyTm (quote (zonk (fun a))))
, "phi = " ++ show (prettyTm (quote (zonk phi)))
, "u = " ++ show (prettyTm (quote (zonk u)))
, "a0 = " ++ show (prettyTm (quote (zonk a0)))
]
compConArgs :: Int -> (NFEndp -> Value) -> Value -> Seq.Seq Projection -> NFEndp -> Value -> Seq.Seq Projection
compConArgs total_args fam = go total_args where
go _ _ Seq.Empty _ _ = Seq.Empty go _ _ Seq.Empty _ _ = Seq.Empty
go nargs (VPi p dom (Closure _ rng)) (PApp p' y Seq.:<| xs) phi u go nargs (VPi p dom (Closure _ rng)) (PApp p' y Seq.:<| xs) phi u
| nargs > 0 = assert (p == p') $
PApp p' (nthArg (total_args - nargs) (fam VI1)) Seq.:<| go (nargs - 1) (rng (smuggle (fun (\i -> nthArg (total_args - nargs) (fam i))))) xs phi u
| nargs > 0 = assert (p == p') $ go (nargs - 1) (rng (smuggle (fun (\i -> nthArg (total_args - nargs) (fam i))))) xs phi u
| otherwise = assert (p == p') $ | otherwise = assert (p == p') $
let fill = makeFiller typeArgument nargs dom phi u y
let fill = makeFiller nargs dom phi u y
in PApp p' (fill @@ VI1) Seq.:<| go (nargs - 1) (rng fill) xs phi u in PApp p' (fill @@ VI1) Seq.:<| go (nargs - 1) (rng fill) xs phi u
go _ _ _ _ _ = error $ "invalid constructor" go _ _ _ _ _ = error $ "invalid constructor"
nthArg i (VNe hd s) =
case s Seq.!? i of
Just (PApp _ t) -> t
_ -> error $ "invalid " ++ show i ++ "th argument to data type " ++ show hd
nthArg i (VSystem vs) = VSystem (fmap (nthArg i) vs)
nthArg i xs = error $ "can't get " ++ show i ++ "th argument of " ++ show (prettyTm (quote xs))
makeFiller nth (VNe (HData _ n') args) phi u a0
| n' == typeArgument =
fun $ fill (makeDomain args) phi (system \i is1 -> nthArg nth (u @@ i @@ is1) ) a0
makeFiller _ _ _ _ a0 = fun (const a0)
makeDomain (PApp _ x Seq.:<| xs) = fun \i -> foldl (\t (~(PApp _ x)) -> t @@ (x @@ i)) (x @@ i) xs
makeDomain _ = error "somebody smuggled something that smells"
smuggle x = VNe (HData False typeArgument) (Seq.singleton (PApp P.Ex x)) smuggle x = VNe (HData False typeArgument) (Seq.singleton (PApp P.Ex x))
typeArgument = unsafePerformIO newName typeArgument = unsafePerformIO newName
{-# NOINLINE typeArgument #-} {-# NOINLINE typeArgument #-}
makeSetFiller :: Name -> Int -> Value -> NFEndp -> Value -> Value -> Value
makeSetFiller typeArgument nth (VNe (HData _ n') args) phi u a0
| n' == typeArgument =
fun $ fill (makeDomain args) phi (system \i is1 -> nthArg nth (u @@ i @@ is1) ) a0
where
makeDomain (PApp _ x Seq.:<| xs) = fun \i -> foldl (\t (~(PApp _ x)) -> t @@ (x @@ i)) (x @@ i) xs
makeDomain _ = error "somebody smuggled something that smells"
makeSetFiller _ _ _ _ _ a0 = fun (const a0)
nthArg :: Int -> Value -> Value
nthArg i (force -> VNe hd s) =
case s Seq.!? i of
Just (PApp _ t) -> t
_ -> error $ "invalid " ++ show i ++ "th argument to data type " ++ show hd
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{} = vl
compOutS _ _hi _0 (VInc _ _ x) = x
compOutS a phi a0 v = outS a phi a0 v
system :: (Value -> Value -> Value) -> Value 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
system k = VLam P.Ex $ Closure (Bound "i" 0) \i -> VLam P.Ex $ Closure (Bound "phi" 0) \isone -> k i isone
fill :: DebugCallStack => NFLine -> NFEndp -> Value -> Value -> NFEndp -> Value
fill :: HasCallStack => 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)
@ -450,23 +389,23 @@ fill a phi u a0 j =
, (inot j, outS a phi (u @@ VI0) a0)])) , (inot j, outS a phi (u @@ VI0) a0)]))
a0 a0
hComp :: DebugCallStack => NFSort -> NFEndp -> Value -> Value -> Value
hComp _ (force -> VI1) u _ = u @@ VI1 @@ VReflStrict VI VI1
hComp :: NFSort -> NFEndp -> Value -> Value -> Value
hComp _ (force -> VI1) u _ = u @@ VI1 @@ VItIsOne
hComp a phi u a0 = VHComp a phi u a0 hComp a phi u a0 = VHComp a phi u a0
glueType :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
glueType :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
glueType a phi tys eqvs = VGlueTy a phi tys eqvs glueType a phi tys eqvs = VGlueTy a phi tys eqvs
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 (force -> VInc _ _ (force -> VUnglue _ _ _ _ vl)) = vl
glueElem :: NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> 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 glueElem a phi tys eqvs t vl = VGlue a phi tys eqvs t vl
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 :: 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) unglue a phi tys eqvs (force -> VSystem fs) = VSystem (fmap (unglue a phi tys eqvs) fs)
unglue a phi tys eqvs vl = VUnglue a phi tys eqvs vl unglue a phi tys eqvs vl = VUnglue a phi tys eqvs vl
-- Definition of equivalences
faceForall :: (NFEndp -> NFEndp) -> Value faceForall :: (NFEndp -> NFEndp) -> Value
faceForall phi = T.length (getNameText name) `seq` go (phi (VVar name)) where faceForall phi = T.length (getNameText name) `seq` go (phi (VVar name)) where
@ -488,28 +427,27 @@ isContr :: Value -> Value
isContr a = exists' "x" a \x -> dprod' "y" a \y -> VPath (line (const a)) x y isContr a = exists' "x" a \x -> dprod' "y" a \y -> VPath (line (const a)) x y
fiber :: NFSort -> NFSort -> Value -> Value -> Value fiber :: NFSort -> NFSort -> Value -> Value -> Value
fiber a b f y = exists' "x" a \x -> VPath (line (const b)) y (f @@ x)
fiber a b f y = exists' "x" a \x -> VPath (line (const b)) (f @@ x) y
isEquiv :: NFSort -> NFSort -> Value -> Value isEquiv :: NFSort -> NFSort -> Value -> Value
isEquiv a b f = dprod' "y" b \y -> isContr (fiber a b f y) isEquiv a b f = dprod' "y" b \y -> isContr (fiber a b f y)
equiv :: NFSort -> NFSort -> Value equiv :: NFSort -> NFSort -> Value
equiv a b = GluedVl (HCon VType (Defined (T.pack "Equiv") (-1))) sp $ exists' "f" (a ~> b) \f -> isEquiv a b f where
sp = Seq.fromList [ PApp P.Ex a, PApp P.Ex b ]
equiv a b = exists' "f" (a ~> b) \f -> isEquiv a b f
pres :: (NFEndp -> NFSort) -> (NFEndp -> NFSort) -> (NFEndp -> Value) -> NFEndp -> (NFEndp -> Value) -> Value -> (Value, NFSort, Value) pres :: (NFEndp -> NFSort) -> (NFEndp -> NFSort) -> (NFEndp -> Value) -> NFEndp -> (NFEndp -> Value) -> Value -> (Value, NFSort, Value)
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
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
pathT = VPath (fun (const (tyA VI1))) c1 c2 pathT = VPath (fun (const (tyA VI1))) c1 c2
c1 = comp (line tyA) phi (system \i u -> f i @@ (t i @@ u)) (incS (tyA VI0) phi (f VI0 @@ t0))
c1 = comp (line tyA) phi (system \i u -> f i @@ (t i @@ u)) (VInc (tyA VI0) phi (f VI0 @@ t0))
c2 = f VI1 @@ comp (line tyT) phi (system \i u -> t i @@ u) t0 c2 = f VI1 @@ comp (line tyT) phi (system \i u -> t i @@ u) t0
a0 = f VI0 @@ t0 a0 = f VI0 @@ t0
v = fill (fun tyT) phi (system \i u -> t i @@ u) 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)) (incS (tyA VI0) phi a0)
path j = comp (fun tyA) (phi `ior` j) (system \i _ -> f i @@ (v i)) a0
opEquiv :: HasCallStack => Value -> Value -> Value -> NFEndp -> Value -> Value -> Value -> (Value, NFSort, Value) opEquiv :: HasCallStack => Value -> Value -> Value -> NFEndp -> Value -> Value -> Value -> (Value, NFSort, Value)
opEquiv aT tT f phi t p a = (incS ty phi v, ty, fun \u -> VPair (t @@ u) (p @@ u)) where
opEquiv aT tT f phi t p a = (VInc ty phi v, ty, fun \u -> VPair (t @@ u) (p @@ u)) where
fn = vProj1 f fn = vProj1 f
ty = exists' "f" tT \x -> VPath (line (const aT)) a (fn @@ x) 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)) v = contr ty (vProj2 f @@ a) phi (\u -> VPair (t @@ u) (p @@ u))
@ -517,76 +455,33 @@ opEquiv aT tT f phi t p a = (incS ty phi v, ty, fun \u -> VPair (t @@ u) (p @@ u
contr :: HasCallStack => Value -> Value -> NFEndp -> (Value -> Value) -> Value contr :: HasCallStack => Value -> Value -> NFEndp -> (Value -> Value) -> Value
contr a aC phi u = contr a aC phi u =
comp (line (const a)) comp (line (const a))
(ior phi (inot phi))
(system \i is1 -> mkVSystem $ Map.fromList [ (phi, ielim (line (const a)) (vProj1 aC) (u is1) (vProj2 aC @@ u is1) i)
, (inot phi, vProj1 aC)
])
(incS a phi (vProj1 aC))
phi
(system \i is1 -> ielim (line (const a)) (vProj1 aC) (u is1) (vProj2 aC @@ u is1) i)
(VInc a phi (vProj1 aC))
transp :: (NFEndp -> Value) -> Value -> Value transp :: (NFEndp -> Value) -> Value -> Value
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)) (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 (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 ()
(_, force -> VNe hd (length -> nargs)) = unPi con_type
ourType = case hd of
HData True n' -> n' == name
_ -> False
transHit name line phi (VNe (HPCon sys con_type con_name) spine) | ourType = x' where
x' = VNe (HPCon (mapVSystem rec sys) con_type con_name) $ compConArgs (makeTransFiller name) nargs line con_type spine phi ()
rec = transHit name line phi
(_, force -> VNe hd (length -> nargs)) = unPi con_type
ourType = case hd of
HData True n' -> n' == name
_ -> False
transHit name line phi (VSystem xs) = mkVSystem (fmap (transHit name line phi) xs)
transHit _ line phi a0 = gtrans line phi a0
transFill :: Name -> (NFEndp -> Value) -> NFEndp -> Value -> NFEndp -> Value
transFill name a phi a0 i = transHit name (\j -> a (iand i j)) (phi `ior` inot i) a0 where
transSqueeze :: Name -> (NFEndp -> Value) -> NFEndp -> (NFEndp -> Value) -> NFEndp -> Value
transSqueeze name a phi x i = transHit name (\j -> a (ior i j)) (phi `ior` i) (x i)
makeTransFiller :: Name -> Name -> p -> Value -> NFEndp -> () -> Value -> Value
makeTransFiller thedata typeArgument _ (VNe (HData _ n') args) phi () a0
| n' == typeArgument = fun (transFill thedata (makeDomain args) phi a0)
where
makeDomain (PApp _ x Seq.:<| xs) = \i -> foldl (\t (~(PApp _ x)) -> t @@ (x @@ i)) (x @@ i) xs
makeDomain _ = error "somebody smuggled something that smells"
makeTransFiller _ _ _ _ _ _ a0 = fun (const a0)
transp line a0 = comp (fun line) VI0 (system \_ _ -> VSystem mempty) (VInc (line VI0) VI0 a0)
makeEquiv :: Name -> Value -> Value makeEquiv :: Name -> Value -> Value
makeEquiv var vne = makeEquiv' \x -> substitute (Map.singleton var x) vne
makeEquiv' :: (NFEndp -> Value) -> Value
makeEquiv' line' = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vProj2 u) y)
makeEquiv var vne = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vProj2 u) y)
where where
line = fun \i -> line' (inot i)
line = fun \i -> substitute (Map.singleton var (inot i)) vne
a = line @@ VI0 a = line @@ VI0
b = line @@ VI1 b = line @@ VI1
f = fun \x -> transp (line @@) x f = fun \x -> transp (line @@) x
g = fun \x -> transp ((line @@) . inot) x g = fun \x -> transp ((line @@) . inot) x
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)
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))) 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))])) (incS 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))])) (VInc a (ior j (inot j)) (g @@ y)) i
theta1 x beta y i j = theta1 x beta y i j =
fill (fun ((line @@) . inot)) fill (fun ((line @@) . inot))
(ior j (inot j)) (ior j (inot j))
(system \i _ -> mkVSystem (Map.fromList [ (inot j, v (inot i) @@ y) (system \i _ -> mkVSystem (Map.fromList [ (inot j, v (inot i) @@ y)
, (j, u (inot i) @@ x)])) , (j, u (inot i) @@ x)]))
(incS b (ior j (inot j)) (ielim b y (f @@ x) beta y))
(VInc b (ior j (inot j)) (ielim b y (f @@ x) beta y))
(inot i) (inot i)
omega x beta y = theta1 x beta y VI0 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)))) delta x beta y j k = comp line (ior k (ior (inot k) (ior j (inot j))))
@ -594,7 +489,7 @@ makeEquiv' line' = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vP
, (k, theta1 x beta y i j) , (k, theta1 x beta y i j)
, (inot j, v i @@ y) , (inot j, v i @@ y)
, (j, u i @@ omega x beta y k)])) , (j, u i @@ omega x beta y k)]))
(incS a (ior k (ior (inot k) (ior j (inot j)))) (omega x beta y (iand j 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 -> 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) VPair (omega x beta y k) (VLine (VPath b y (f @@ x)) (vProj2 (fib y)) beta $ fun \j -> delta x beta y j k)
@ -607,27 +502,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)))
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
func = AxK (quote a) (quote x) (quote bigp) (quote pr)
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 :: 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
func = AxJ (quote a) (quote x) (quote bigp) (quote pr) (quote y)
strictJ a x bigp pr y (GluedVl h sp vl) = GluedVl h (sp Seq.:|> PJ a x bigp pr y) (strictJ a x bigp pr y vl)
strictJ _ _ _ _r _ eq = error $ "can't J " ++ show eq
projIntoCase :: (Term -> Term) -> (Term, Int, Term) -> (Term, Int, Term)
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 = error $ show $ prettyTm x
id_fiber y = VPair y (VLine a y y (fun (const y)))

+ 11
- 18
src/Elab/WiredIn.hs-boot View File

@ -1,9 +1,8 @@
{-# 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
module Elab.WiredIn where
import GHC.Stack.Types
import Syntax import Syntax
import Debug (DebugCallStack)
wiType :: WiredIn -> NFType wiType :: WiredIn -> NFType
wiValue :: WiredIn -> NFType wiValue :: WiredIn -> NFType
@ -12,20 +11,14 @@ iand, ior :: NFEndp -> NFEndp -> NFEndp
inot :: NFEndp -> NFEndp inot :: NFEndp -> NFEndp
ielim :: NFSort -> Value -> Value -> Value -> NFEndp -> Value ielim :: NFSort -> Value -> Value -> Value -> NFEndp -> 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
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
glueType :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
glueElem :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
unglue :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
glueType :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
glueElem :: NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
unglue :: HasCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
fun :: (Value -> Value) -> Value fun :: (Value -> Value) -> Value
system :: (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)
system :: (Value -> Value -> Value) -> Value

+ 57
- 124
src/Main.hs View File

@ -3,7 +3,6 @@
{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DeriveAnyClass #-} {-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE NamedFieldPuns #-}
module Main where module Main where
import Control.Monad.IO.Class import Control.Monad.IO.Class
@ -12,9 +11,7 @@ import Control.Exception
import qualified Data.ByteString.Lazy as Bsl import qualified Data.ByteString.Lazy as Bsl
import qualified Data.Text.Encoding as T import qualified Data.Text.Encoding as T
import qualified Data.Text.Lazy.IO as Lt
import qualified Data.Map.Strict as Map import qualified Data.Map.Strict as Map
import qualified Data.Text.Lazy as Lt
import qualified Data.Text.IO as T import qualified Data.Text.IO as T
import qualified Data.Set as Set import qualified Data.Set as Set
import qualified Data.Text as T import qualified Data.Text as T
@ -24,7 +21,7 @@ import Data.Foldable
import Data.Maybe import Data.Maybe
import Data.IORef import Data.IORef
import Debug (traceDocM)
import Debug.Trace
import Elab.Monad hiding (switch) import Elab.Monad hiding (switch)
import Elab.WiredIn import Elab.WiredIn
@ -58,7 +55,7 @@ main = do
Check files verbose -> do Check files verbose -> do
env <- checkFiles files env <- checkFiles files
when verbose $ dumpEnv env when verbose $ dumpEnv env
Repl -> enterReplIn =<< emptyEnv
Repl -> enterReplIn =<< checkFiles ["./test.tt"]
evalArgExpr :: ElabEnv -> String -> IO () evalArgExpr :: ElabEnv -> String -> IO ()
evalArgExpr env str = evalArgExpr env str =
@ -66,7 +63,7 @@ evalArgExpr env str =
Right e -> Right e ->
flip runElab env (do flip runElab env (do
(e, _) <- infer e (e, _) <- infer e
liftIO . print . prettyTm . quote =<< Elab.Eval.eval e)
liftIO . putStrLn . show . prettyTm . quote . zonk =<< Elab.Eval.eval e)
`catch` \e -> do `catch` \e -> do
displayExceptions' inp (e :: SomeException) displayExceptions' inp (e :: SomeException)
Left e -> liftIO $ print e Left e -> liftIO $ print e
@ -74,69 +71,30 @@ evalArgExpr env str =
inp = T.pack str inp = T.pack str
enterReplIn :: ElabEnv -> IO () enterReplIn :: ElabEnv -> IO ()
enterReplIn env =
do
let env' = mkrepl env
envref <- newIORef env'
runInputT (setComplete (complete envref) defaultSettings) (loop env' envref)
where
mkrepl env = env { commHook = Lt.putStrLn . render }
complete :: IORef ElabEnv -> (String, String) -> IO (String, [Completion])
complete c = completeWord Nothing " \n\t\r" go where
go w = do
env <- readIORef c
let
w' = T.pack w
words = Set.toList $ Set.filter ((w' `T.isPrefixOf`) . getNameText) (definedNames env)
pure (map (simpleCompletion . T.unpack . getNameText) words)
loop :: ElabEnv -> IORef ElabEnv -> InputT IO ()
loop env envvar = do
inp <- fmap T.pack <$> getInputLine "% "
case inp of
Nothing -> pure ()
Just inp | ":r" `T.isPrefixOf` inp -> reload env envvar
Just inp ->
case runAlex (Bsl.fromStrict (T.encodeUtf8 inp)) parseRepl of
Left e -> do
liftIO $ print e
loop env envvar
Right st -> do
env <- liftIO $
runElab (checkStatement st ask) env
`catch` \e -> do
displayExceptions' inp (e :: SomeException)
pure env
metas <- liftIO $ atomicModifyIORef' (unsolvedMetas env) (\x -> (mempty, x))
unless (Map.null metas) $ do
liftIO $ reportUnsolved (Just inp) metas
enterReplIn env = runInputT defaultSettings (loop env') where
env' = env { commHook = putStrLn . show . prettyTm . quote }
liftIO $ writeIORef envvar env
loop env envvar
reload :: ElabEnv -> IORef ElabEnv -> InputT IO ()
reload env@ElabEnv{loadedFiles} envref = do
newe <- liftIO $ try $ mkrepl <$> checkFiles (reverse loadedFiles)
case newe of
Left e -> do
liftIO $ do displayExceptions' ":r" (e :: SomeException)
loop env envref
Right newe -> do
liftIO $ writeIORef envref newe
loop newe envref
loop :: ElabEnv -> InputT IO ()
loop env = do
inp <- fmap T.pack <$> getInputLine "% "
case inp of
Nothing -> pure ()
Just inp ->
case runAlex (Bsl.fromStrict (T.encodeUtf8 inp)) parseRepl of
Left e -> do
liftIO $ print e
loop env
Right st -> do
env <- liftIO $
runElab (checkStatement st ask) env
`catch` \e -> do
displayExceptions' inp (e :: SomeException)
pure env
loop env
checkFiles :: [String] -> IO ElabEnv checkFiles :: [String] -> IO ElabEnv
checkFiles files = runElab (go 1 files ask) =<< emptyEnv where
size = length files
sl = length (show size)
pad s
| length s < sl = replicate (sl - length s) ' ' ++ s
| otherwise = s
go _ [] k = do
checkFiles files = runElab (go files ask) =<< emptyEnv where
go [] k = do
env <- ask env <- ask
for_ (Map.toList (nameMap env)) \case for_ (Map.toList (nameMap env)) \case
(_, v@Defined{}) (_, v@Defined{})
@ -144,41 +102,34 @@ checkFiles files = runElab (go 1 files ask) =<< emptyEnv where
| otherwise -> | otherwise ->
let let
pos = fromJust (Map.lookup v (whereBound env)) pos = fromJust (Map.lookup v (whereBound env))
in withSpan (fst pos) (snd pos) $ throwElab $ Elab.DeclaredUndefined v
in withSpan (fst pos) (snd pos) $ throwElab $ DeclaredUndefined v
_ -> pure () _ -> pure ()
metas <- liftIO $ atomicModifyIORef' (unsolvedMetas env) (\x -> (mempty, x))
metas <- liftIO $ readIORef (unsolvedMetas env)
unless (Map.null metas) $ do unless (Map.null metas) $ do
liftIO $ reportUnsolved Nothing metas
k
liftIO $ reportUnsolved metas
go n (x:xs) k = do
liftIO . putStrLn $ "[" ++ pad (show n) ++ "/" ++ show size ++ "] Loading " ++ x
k
go (x:xs) k = do
code <- liftIO $ Bsl.readFile x code <- liftIO $ Bsl.readFile x
case runAlex (code <> Bsl.singleton 10) parseProg of case runAlex (code <> Bsl.singleton 10) parseProg of
Left e -> liftIO (print e) *> k
Left e -> liftIO $ print e *> error (show e)
Right prog -> Right prog ->
local (\e -> e { currentFile = Just (T.pack x), loadedFiles = x:loadedFiles e }) (checkProgram prog (go (n + 1 :: Int) xs k))
local (\e -> e { currentFile = Just (T.pack x) }) (checkProgram prog (go xs k))
`catchElab` \e -> liftIO $ displayAndDie (T.decodeUtf8 (Bsl.toStrict code)) (e :: SomeException) `catchElab` \e -> liftIO $ displayAndDie (T.decodeUtf8 (Bsl.toStrict code)) (e :: SomeException)
dumpEnv :: ElabEnv -> IO () dumpEnv :: ElabEnv -> IO ()
dumpEnv env = for_ (Map.toList (nameMap env)) $ \(_, name) -> dumpEnv env = for_ (Map.toList (nameMap env)) $ \(_, name) ->
let nft = fst $ getEnv env Map.! name in let nft = fst $ getEnv env Map.! name in
Lt.putStrLn $ render (pretty name <+> nest (negate 1) (colon <+> align (prettyTm (quote (zonk nft)))))
T.putStrLn $ render (pretty name <+> align (nest (negate 1) (colon <+> prettyTm (quote (zonk nft)))))
parser :: ParserInfo Opts parser :: ParserInfo Opts
parser = info (subparser (load <> check <> repl) <|> pure Repl <**> helper) (header "cubical - a cubical programming language")
parser = info (subparser (load <> check) <|> pure Repl <**> helper) (header "cubical - a cubical programming language")
where where
load = command "load" $ load = command "load" $
info ((Load <$> (some (argument str (metavar "file..."))) info ((Load <$> (some (argument str (metavar "file...")))
<*> (many (strOption (long "eval" <> short 'e' <> help "Also evaluate this expression")))) <*> (many (strOption (long "eval" <> short 'e' <> help "Also evaluate this expression"))))
<**> helper) (progDesc "Check and load a list of files in the REPL") <**> helper) (progDesc "Check and load a list of files in the REPL")
repl = command "load" $
info ((Load <$> (many (argument str (metavar "file...")))
<*> (many (strOption (long "eval" <> short 'e' <> help "Also evaluate this expression"))))
<**> helper) (progDesc "Enter the REPL, optionally with loaded files")
check = command "check" $ check = command "check" $
info ((Check <$> some (argument str (metavar "file...")) info ((Check <$> some (argument str (metavar "file..."))
<*> switch ( long "verbose" <*> switch ( long "verbose"
@ -208,65 +159,44 @@ displayExceptions lines =
T.putStrLn $ squiggleUnder a b lines T.putStrLn $ squiggleUnder a b lines
, Handler \(AttachedNote n e) -> do , Handler \(AttachedNote n e) -> do
displayExceptions' lines e displayExceptions' lines e
Lt.putStrLn $ "\x1b[1;32mnote\x1b[0m: " <> render n
, Handler \(WhenCheckingEndpoint dir le ri ep e) -> do
T.putStrLn $ "\x1b[1;32mnote\x1b[0m: " <> render n
, Handler \(WhenCheckingEndpoint le ri ep e) -> do
displayExceptions' lines e displayExceptions' lines e
let let
endp = case ep of endp = case ep of
VI0 -> Lt.pack "left"
VI1 -> Lt.pack "right"
_ -> render . prettyTm $ quoteWith False mempty ep
left = render (prettyTm (quoteWith False mempty le))
right = render (prettyTm (quoteWith False mempty ri))
Lt.putStrLn . Lt.unlines $
[ "\n\x1b[1;32mnote\x1b[0m: This path was expected to fill the diagram <<"
, "\t " <> redact left <> " " <> Lt.replicate 7 (Lt.singleton '\x2500') <> " " <> redact right
, " >> in the direction " <> render (pretty dir) <> ", but the " <> endp <> " endpoint is incorrect"
VI0 -> T.pack "left"
VI1 -> T.pack "right"
_ -> T.pack $ show (prettyTm (quote ep))
T.putStrLn . T.unlines $
[ "\x1b[1;32mnote\x1b[0m: This path was expected to fill the diagram"
, "\t " <> render (prettyTm (quote le)) <> " " <> T.replicate 7 (T.singleton '\x2500') <> " " <> render (prettyTm (quote ri))
, "\x1b[1;32mnote\x1b[0m: the " <> endp <> " endpoint is incorrect"
] ]
, Handler \(NotEqual ta tb) -> do , Handler \(NotEqual ta tb) -> do
Lt.putStrLn . render . vsep $
putStrLn . unlines $
[ "\x1b[1;31merror\x1b[0m: Mismatch between actual and expected types:" [ "\x1b[1;31merror\x1b[0m: Mismatch between actual and expected types:"
, indent 2 $ "* \x1b[1mActual\x1b[0m:" <> softline <> align (prettyVl (zonk ta))
, indent 2 $ "* \x1b[1mExpected\x1b[0m:" <> softline <> align (prettyVl (zonk tb))
, " * \x1b[1mActual\x1b[0m: " ++ showValue (zonk ta)
, " * \x1b[1mExpected\x1b[0m: " ++ showValue (zonk tb)
] ]
, Handler \(NoSuchPrimitive x) -> do , Handler \(NoSuchPrimitive x) -> do
putStrLn $ "Unknown primitive: " ++ T.unpack x putStrLn $ "Unknown primitive: " ++ T.unpack x
, Handler \(NotInScope x) -> do , Handler \(NotInScope x) -> do
putStrLn $ "Variable not in scope: " ++ show (pretty x) putStrLn $ "Variable not in scope: " ++ show (pretty x)
, Handler \(Elab.DeclaredUndefined n) -> do
, Handler \(DeclaredUndefined n) -> do
putStrLn $ "Name declared but not defined: " ++ show (pretty n) putStrLn $ "Name declared but not defined: " ++ show (pretty n)
, Handler \Elab.PathConPretype -> do
putStrLn $ "Pretypes can not have path constructors, either change this definition so it lands in Type or remove it."
] ]
redact :: Lt.Text -> Lt.Text
redact x
| length (Lt.lines x) >= 2 = head (Lt.lines x) <> Lt.pack "\x1b[1;32m[...]\x1b[0m"
| otherwise = x
reportUnsolved :: Foldable t => Maybe Text -> Map.Map MV (t (Seq Projection, Value)) -> IO ()
reportUnsolved code metas = do
reportUnsolved :: Foldable t => Map.Map MV (t (Seq Projection, Value)) -> IO ()
reportUnsolved metas = do
for_ (Map.toList metas) \(m, p) -> do for_ (Map.toList metas) \(m, p) -> do
case mvSpan m of case mvSpan m of
Just (f, s, e) ->
case code of
Just code -> T.putStrLn $ squiggleUnder s e code
Nothing -> T.putStrLn . squiggleUnder s e =<< T.readFile (T.unpack f)
Just (f, s, e) -> T.putStrLn . squiggleUnder s e =<< T.readFile (T.unpack f)
Nothing -> pure () Nothing -> pure ()
T.putStrLn . render $
"Unsolved metavariable" <+> prettyTm (Meta m) <+> pretty ':' <+> prettyTm (quote (mvType m)) <+> "should satisfy:"
for_ p \p ->
T.putStrLn . render $ indent 2 $ prettyTm (quote (VNe (HMeta m) (fst p))) <+> pretty '≡' <+> prettyTm (quote (snd p))
case null p of
True -> do
Lt.putStrLn . render $ "Unsolved metavariable" <+> prettyTm (Meta m) <+> pretty ':' <+> align (prettyVl (zonk (mvType m)) <> pretty '.')
_ -> do
Lt.putStrLn . render $
"Unsolved metavariable" <+> prettyTm (Meta m) <+> pretty ':' <+> align (prettyVl (zonk (mvType m)) <+> "should satisfy:")
for_ p \p ->
Lt.putStrLn . render $ indent 2 $ prettyTm (quote (zonk (VNe (HMeta m) (fst p)))) <+> pretty '≡' <+> prettyTm (quote (snd p))
when (mvInteraction m && not (Map.null (mvContext m))) do
putStrLn "Context (first 10 entries):"
for_ (take 10 (Map.toList (mvContext m))) \(x, t) -> unless (isIdkT t) do
Lt.putStrLn . render $ indent 2 $ pretty x <+> pretty ':' <+> prettyVl (zonk t)
displayExceptions' :: Exception e => Text -> e -> IO () displayExceptions' :: Exception e => Text -> e -> IO ()
displayExceptions' lines e = displayAndDie lines e `catch` \(_ :: ExitCode) -> pure () displayExceptions' lines e = displayAndDie lines e `catch` \(_ :: ExitCode) -> pure ()
@ -282,11 +212,14 @@ squiggleUnder (Posn l c) (Posn l' c') file
in T.unlines [ padding, line, padding <> squiggle ] in T.unlines [ padding, line, padding <> squiggle ]
| otherwise = T.unlines (take (l' - l) (drop l (T.lines file))) | otherwise = T.unlines (take (l' - l) (drop l (T.lines file)))
newtype DeclaredUndefined = DeclaredUndefined { declaredUndefName :: Name }
deriving (Eq, Show, Exception)
dumpTokens :: Alex () dumpTokens :: Alex ()
dumpTokens = do dumpTokens = do
t <- alexMonadScan t <- alexMonadScan
case tokenClass t of case tokenClass t of
TokEof -> pure () TokEof -> pure ()
_ -> do _ -> do
traceDocM (viaShow t)
traceM (show t)
dumpTokens dumpTokens

+ 2
- 20
src/Presyntax/Lexer.x View File

@ -7,8 +7,6 @@ import qualified Data.Text as T
import Presyntax.Tokens import Presyntax.Tokens
import Debug.Trace
} }
%wrapper "monadUserState-bytestring" %wrapper "monadUserState-bytestring"
@ -34,14 +32,13 @@ tokens :-
<0> \\ { always TokLambda } <0> \\ { always TokLambda }
<0> "->" { always TokArrow } <0> "->" { always TokArrow }
<0> "_" { always TokUnder }
<0> \( { always TokOParen } <0> \( { always TokOParen }
<0> \{ { always TokOBrace } <0> \{ { always TokOBrace }
<0> \[ { always TokOSquare } <0> \[ { always TokOSquare }
<0> \) { always TokCParen } <0> \) { always TokCParen }
<0> \} { closeBrace }
<0> \} { always TokCBrace }
<0> \] { always TokCSquare } <0> \] { always TokCSquare }
<0> \; { always TokSemi } <0> \; { always TokSemi }
@ -74,7 +71,6 @@ tokens :-
-- layout: indentation of the next token is context for offside rule -- layout: indentation of the next token is context for offside rule
<layout> { <layout> {
\n ; \n ;
\{ { openBrace }
() { startLayout } () { startLayout }
} }
@ -149,20 +145,6 @@ startLayout (AlexPn _ line col, _, _, _) _ = do
else mapUserState $ \s -> s { layoutColumns = col:layoutColumns s } else mapUserState $ \s -> s { layoutColumns = col:layoutColumns s }
pure (Token TokLStart line col) pure (Token TokLStart line col)
openBrace :: AlexInput -> Int64 -> Alex Token
openBrace (AlexPn _ line col, _, _, _) _ = do
popStartCode
mapUserState $ \s -> s { layoutColumns = minBound:layoutColumns s }
pure (Token TokOBrace line col)
closeBrace :: AlexInput -> Int64 -> Alex Token
closeBrace (AlexPn _ line col, _, _, _) _ = do
~(col':tail) <- layoutColumns <$> getUserState
if col' < 0
then mapUserState $ \s -> s { layoutColumns = tail }
else pure ()
pure (Token TokCBrace line col)
variableOrKeyword :: AlexAction Token variableOrKeyword :: AlexAction Token
variableOrKeyword (AlexPn _ l c, _, s, _) size = variableOrKeyword (AlexPn _ l c, _, s, _) size =
let text = T.decodeUtf8 (Lbs.toStrict (Lbs.take size s)) in let text = T.decodeUtf8 (Lbs.toStrict (Lbs.take size s)) in
@ -183,4 +165,4 @@ laidOut x l c = do
mapUserState $ \s -> s { leastColumn = c } mapUserState $ \s -> s { leastColumn = c }
pure (Token x l c) pure (Token x l c)
}
}

+ 22
- 20
src/Presyntax/Parser.y View File

@ -1,5 +1,5 @@
{ {
{-# LANGUAGE FlexibleContexts, FlexibleInstances, ViewPatterns #-}
{-# LANGUAGE FlexibleInstances, ViewPatterns #-}
module Presyntax.Parser where module Presyntax.Parser where
import qualified Data.Text as T import qualified Data.Text as T
@ -50,7 +50,6 @@ import Debug.Trace
'\\' { Token TokLambda _ _ } '\\' { Token TokLambda _ _ }
'->' { Token TokArrow _ _ } '->' { Token TokArrow _ _ }
'_' { Token TokUnder _ _ }
':' { Token TokColon _ _ } ':' { Token TokColon _ _ }
';' { Token TokSemi _ _ } ';' { Token TokSemi _ _ }
'=' { Token TokEqual _ _ } '=' { Token TokEqual _ _ }
@ -81,8 +80,8 @@ import Debug.Trace
Exp :: { Expr } Exp :: { Expr }
Exp Exp
: '\\' LambdaList '->' Exp { span $1 $4 $ makeLams $2 $4 } : '\\' LambdaList '->' Exp { span $1 $4 $ makeLams $2 $4 }
| '\\' MaybeLambdaList '[' Faces ']' { span $1 $5 $ makeLams $2 $ LamSystem $4 }
| '\\' 'case' Block(CaseList) { span $1 $3 $ LamCase (thd $3) }
| '\\' MaybeLambdaList '[' System ']' { span $1 $5 $ makeLams $2 $ LamSystem $4 }
| '\\' 'case' START CaseList END { span $1 $5 $ LamCase $4 }
| '(' var ':' Exp ')' ProdTail { span $1 $6 $ Pi Ex (getVar $2) $4 $6 } | '(' var ':' Exp ')' ProdTail { span $1 $6 $ Pi Ex (getVar $2) $4 $6 }
| '{' var ':' Exp '}' ProdTail { span $1 $6 $ Pi Im (getVar $2) $4 $6 } | '{' var ':' Exp '}' ProdTail { span $1 $6 $ Pi Im (getVar $2) $4 $6 }
| ExpApp '->' Exp { span $1 $3 $ Pi Ex (T.singleton '_') $1 $3 } | ExpApp '->' Exp { span $1 $3 $ Pi Ex (T.singleton '_') $1 $3 }
@ -90,7 +89,8 @@ Exp
| '(' var ':' Exp ')' '*' Exp { span $1 $7 $ Sigma (getVar $2) $4 $7 } | '(' var ':' Exp ')' '*' Exp { span $1 $7 $ Sigma (getVar $2) $4 $7 }
| ExpApp '*' Exp { span $1 $3 $ Sigma (T.singleton '_') $1 $3 } | ExpApp '*' Exp { span $1 $3 $ Sigma (T.singleton '_') $1 $3 }
| 'let' Block(LetList) 'in' Exp { span $1 $4 $ Let (thd $2) $4 }
| 'let' START LetList END 'in' Exp { span $1 $6 $ Let $3 $6 }
| 'let' START LetList END Exp { span $1 $5 $ Let $3 $5 }
| ExpApp { $1 } | ExpApp { $1 }
@ -110,7 +110,6 @@ Tuple :: { Expr }
Atom :: { Expr } Atom :: { Expr }
: var { span $1 $1 $ Var (getVar $1) } : var { span $1 $1 $ Var (getVar $1) }
| '_' { span $1 $1 $ Hole }
| '(' Tuple ')' { span $1 $3 $ $2 } | '(' Tuple ')' { span $1 $3 $ $2 }
ProdTail :: { Expr } ProdTail :: { Expr }
@ -124,9 +123,7 @@ MaybeLambdaList :: { [(Plicity, Text)] }
LambdaList :: { [(Plicity, Text)] } LambdaList :: { [(Plicity, Text)] }
: var { [(Ex, getVar $1)] } : var { [(Ex, getVar $1)] }
| '_' { [(Ex, T.singleton '_')] }
| var LambdaList { (Ex, getVar $1):$2 } | var LambdaList { (Ex, getVar $1):$2 }
| '_' LambdaList { (Ex, T.singleton '_'):$2 }
| '{'var'}' { [(Im, getVar $2)] } | '{'var'}' { [(Im, getVar $2)] }
| '{'var'}' LambdaList { (Im, getVar $2):$4 } | '{'var'}' LambdaList { (Im, getVar $2):$4 }
@ -152,8 +149,7 @@ CaseItem :: { (Pattern, Expr) }
: Pattern '->' Exp { ($1, $3) } : Pattern '->' Exp { ($1, $3) }
CaseList :: { [(Pattern, Expr)] } CaseList :: { [(Pattern, Expr)] }
: { [] }
| CaseItem { [$1] }
: CaseItem { [$1] }
| CaseItem Semis CaseList { $1:$3 } | CaseItem Semis CaseList { $1:$3 }
Pattern :: { Pattern } Pattern :: { Pattern }
@ -167,14 +163,12 @@ Statement :: { Statement }
: VarList ':' Exp { spanSt $1 $3 $ Decl (thd $1) $3 } : VarList ':' Exp { spanSt $1 $3 $ Decl (thd $1) $3 }
| var LhsList '=' Rhs { spanSt $1 $4 $ Defn (getVar $1) (makeLams $2 $4) } | var LhsList '=' Rhs { spanSt $1 $4 $ Defn (getVar $1) (makeLams $2 $4) }
| '{-#' Pragma '#-}' { spanSt $1 $3 $ $2 } | '{-#' Pragma '#-}' { spanSt $1 $3 $ $2 }
| 'postulate' Block(Postulates) { spanSt $1 $2 $ Postulate (thd $2) }
| 'data' var Parameters ':' Exp 'where' Block(Constructors)
{ spanSt $1 $7 $ Data (getVar $2) $3 $5 (thd $7) }
| 'postulate' START Postulates END { spanSt $1 $4 $ Postulate $3 }
| 'data' var Parameters ':' Exp 'where' START Constructors END
{ spanSt $1 $9 $ Data (getVar $2) $3 $5 $8 }
Constructors :: { [(Posn, Posn, Constructor)] } Constructors :: { [(Posn, Posn, Constructor)] }
: { [] }
| var ':' Exp { [(startPosn $1, endPosn $3, Point (getVar $1) $3)] }
: 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 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 ':' Exp Semis Constructors { (startPosn $1, endPosn $3, Point (getVar $1) $3):$5 }
| var PatVarList ':' Exp '[' Faces ']' Semis Constructors | var PatVarList ':' Exp '[' Faces ']' Semis Constructors
@ -219,6 +213,18 @@ Pragma :: { Statement }
: 'PRIMITIVE' var var { Builtin (getVar $2) (getVar $3) } : 'PRIMITIVE' var var { Builtin (getVar $2) (getVar $3) }
| 'PRIMITIVE' var { Builtin (getVar $2) (getVar $2) } | 'PRIMITIVE' var { Builtin (getVar $2) (getVar $2) }
System :: { [(Condition, Expr)] }
: {- empty system -} { [] }
| NeSystem { $1 }
NeSystem :: { [(Condition, Expr) ]}
: SystemLhs '->' Exp { [($1, $3)] }
| SystemLhs '->' Exp ',' NeSystem { ($1, $3):$5 }
SystemLhs :: { Condition }
: Formula 'as' var { Condition $1 (Just (getVar $3)) }
| Formula { Condition $1 Nothing }
Faces :: { [(Formula, Expr)] } Faces :: { [(Formula, Expr)] }
: {- empty system -} { [] } : {- empty system -} { [] }
| NeFaces { $1 } | NeFaces { $1 }
@ -244,10 +250,6 @@ FAtom :: { Formula }
x -> parseError (x, ["i0", "i1"]) x -> parseError (x, ["i0", "i1"])
} }
Block(p)
: START p END { (startPosn $1, endPosn $3, $2) }
| '{' p '}' { (startPosn $1, endPosn $3, $2) }
{ {
lexer cont = alexMonadScan >>= cont lexer cont = alexMonadScan >>= cont


+ 5
- 2
src/Presyntax/Presyntax.hs View File

@ -10,7 +10,6 @@ data Plicity
data Expr data Expr
= Var Text = Var Text
| Hole
| App Plicity Expr Expr | App Plicity Expr Expr
| Pi Plicity Text Expr Expr | Pi Plicity Text Expr Expr
@ -21,7 +20,7 @@ data Expr
| Proj1 Expr | Proj1 Expr
| Proj2 Expr | Proj2 Expr
| LamSystem [(Formula, Expr)]
| LamSystem [(Condition, Expr)]
| LamCase [(Pattern, Expr)] | LamCase [(Pattern, Expr)]
| Let [LetItem] Expr | Let [LetItem] Expr
@ -33,6 +32,10 @@ data LetItem
| LetBind { leIName :: Text, leIVal :: Expr } | LetBind { leIName :: Text, leIVal :: Expr }
deriving (Eq, Show, Ord) deriving (Eq, Show, Ord)
data Condition
= Condition { condF :: Formula, condV :: Maybe Text }
deriving (Eq, Show, Ord)
data Formula data Formula
= FIs1 Text = FIs1 Text
| FIs0 Text | FIs0 Text


+ 0
- 2
src/Presyntax/Tokens.hs View File

@ -9,7 +9,6 @@ data TokenClass
| TokLambda | TokLambda
| TokArrow | TokArrow
| TokUnder
| TokOParen | TokOParen
| TokOBrace | TokOBrace
@ -71,7 +70,6 @@ tokSize TokColon = 1
tokSize TokEqual = 1 tokSize TokEqual = 1
tokSize TokComma = 1 tokSize TokComma = 1
tokSize TokSemi = 1 tokSize TokSemi = 1
tokSize TokUnder = 1
tokSize TokArrow = 2 tokSize TokArrow = 2
tokSize TokPi1 = 2 tokSize TokPi1 = 2
tokSize TokPi2 = 2 tokSize TokPi2 = 2


+ 55
- 97
src/Syntax.hs View File

@ -1,4 +1,3 @@
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE BlockArguments #-} {-# LANGUAGE BlockArguments #-}
{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveDataTypeable #-}
@ -29,9 +28,11 @@ data WiredIn
| WiINot | WiINot
| WiPathP | WiPathP
| WiIsOne -- Proposition associated with an element of the interval
| WiItIsOne -- 1 = 1
| WiPartial -- (φ : I) -> Type -> Typeω | WiPartial -- (φ : I) -> Type -> Typeω
| WiPartialP -- (φ : I) -> Partial r Type -> Typeω | WiPartialP -- (φ : I) -> Partial r Type -> Typeω
| WiPOr -- (A : Type) (φ ψ : I) -> Partial φ A -> Partial ψ A -> Partial (ior φ ψ) A
| WiSub -- (A : Type) (φ : I) -> Partial φ A -> Typeω | WiSub -- (A : Type) (φ : I) -> Partial φ A -> Typeω
| WiInS -- {A : Type} {φ : I} (u : A) -> Sub A φ (λ x -> u) | WiInS -- {A : Type} {φ : I} (u : A) -> Sub A φ (λ x -> u)
@ -39,19 +40,11 @@ data WiredIn
| WiComp -- {A : I -> Type} {phi : I} | WiComp -- {A : I -> Type} {phi : I}
-- -> ((i : I) -> Partial phi (A i) -- -> ((i : I) -> Partial phi (A i)
-- -> (A i0)[phi -> u i0] -> A i1
-- -> (A i0)[phi -> u i0] -> (A i1)[phi -> u i1]
| WiGlue -- (A : Type) {phi : I} (T : Partial phi Type) (e : PartialP phi (\o -> Equiv (T o) A)) -> Type | WiGlue -- (A : Type) {phi : I} (T : Partial phi Type) (e : PartialP phi (\o -> Equiv (T o) A)) -> Type
| WiGlueElem -- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> (t : PartialP phi T) -> Sub A phi (\o -> e o (t o)) -> Glue A phi T e | WiGlueElem -- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> (t : PartialP phi T) -> Sub A phi (\o -> e o (t o)) -> Glue A phi T e
| WiUnglue -- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> Glue A phi T e -> A | WiUnglue -- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> Glue A phi T e -> A
| WiLineToEquiv -- {A : I -> Type} -> Equiv (P i0) (P i1)
-- Two-level
| WiSEq -- Eq_s : {A : Pretype} (x y : A) -> Pretype
| WiSRefl -- refl_s : {A : Pretype} {x : A} -> EqS {A} x x
| WiSK -- K_s : {A : Pretype} {x : A} (P : x = x -> Pretype) -> P refl -> (p : x = x) -> P p
| WiSJ -- J_s : {A : Pretype} {x : A} (P : (y : A) -> x = y -> Pretype) -> P x refl -> {y : A} -> (p : x = y) -> P y p
deriving (Eq, Show, Ord) deriving (Eq, Show, Ord)
data Term data Term
@ -86,6 +79,9 @@ data Term
-- ^ PathIntro : (A : I -> Type) (f : (i : I) -> A i) -> PathP A (f i0) (f i1) -- ^ PathIntro : (A : I -> Type) (f : (i : I) -> A i) -> PathP A (f i0) (f i1)
-- ~~~~~~~~~ not printed at all -- ~~~~~~~~~ not printed at all
| IsOne Term
| ItIsOne
| Partial Term Term | Partial Term Term
| PartialP Term Term | PartialP Term Term
@ -103,11 +99,6 @@ data Term
| Unglue Term Term Term Term Term | Unglue Term Term Term Term Term
| Case Term Term [(Term, Int, Term)] | Case Term Term [(Term, Int, Term)]
| EqS Term Term Term
| Refl Term Term
| AxK Term Term Term Term Term
| AxJ Term Term Term Term Term Term
deriving (Eq, Show, Ord, Data) deriving (Eq, Show, Ord, Data)
data MV = data MV =
@ -115,8 +106,6 @@ data MV =
, mvCell :: {-# UNPACK #-} !(IORef (Maybe Value)) , mvCell :: {-# UNPACK #-} !(IORef (Maybe Value))
, mvType :: NFType , mvType :: NFType
, mvSpan :: Maybe (Text, Posn, Posn) , mvSpan :: Maybe (Text, Posn, Posn)
, mvInteraction :: Bool
, mvContext :: Map Name NFType
} }
instance Eq MV where instance Eq MV where
@ -170,6 +159,9 @@ data Value
| VPath NFLine Value Value | VPath NFLine Value Value
| VLine NFLine Value Value Value | VLine NFLine Value Value Value
| VIsOne NFEndp
| VItIsOne
| VPartial NFEndp Value | VPartial NFEndp Value
| VPartialP NFEndp Value | VPartialP NFEndp Value
| VSystem (Map Value Value) | VSystem (Map Value Value)
@ -185,16 +177,13 @@ data Value
| VUnglue NFSort NFEndp NFPartial NFPartial Value | VUnglue NFSort NFEndp NFPartial NFPartial Value
| VCase (Map.Map Name (NFType, Value)) Value Value [(Term, Int, Term)] | VCase (Map.Map Name (NFType, Value)) Value Value [(Term, Int, Term)]
| VEqStrict NFSort Value Value
| VReflStrict NFSort Value
deriving (Eq, Show, Ord) deriving (Eq, Show, Ord)
pattern VVar :: Name -> Value pattern VVar :: Name -> Value
pattern VVar x = VNe (HVar x) Seq.Empty pattern VVar x = VNe (HVar x) Seq.Empty
quoteWith :: Bool -> Set Name -> Value -> Term
quoteWith short names (VNe h sp) = foldl goSpine (goHead h) sp where
quoteWith :: Set Name -> Value -> Term
quoteWith names (VNe h sp) = foldl goSpine (goHead h) sp where
goHead (HVar v) = Ref v goHead (HVar v) = Ref v
goHead (HMeta m) = Meta m goHead (HMeta m) = Meta m
goHead (HCon _ v) = Con v goHead (HCon _ v) = Con v
@ -204,89 +193,74 @@ quoteWith short names (VNe h sp) = foldl goSpine (goHead h) sp where
case Map.lookup VI1 f of case Map.lookup VI1 f of
Just vl -> constantly (length sp) vl Just vl -> constantly (length sp) vl
_ -> PCon (quote sys) v _ -> PCon (quote sys) v
VLam{} -> PCon (quote sys) v
s -> constantly (length sp) s
_ -> PCon (quote sys) v
goHead (HData x v) = Data x v goHead (HData x v) = Data x v
goSpine t (PApp p v) = App p t (quoteWith short names v)
goSpine t (PApp p v) = App p t (quoteWith names v)
goSpine t (PIElim l x y i) = IElim (quote l) (quote x) (quote y) t (quote i) goSpine t (PIElim l x y i) = IElim (quote l) (quote x) (quote y) t (quote i)
goSpine t (PK l x y i) = AxK (quote l) (quote x) (quote y) (quote i) t
goSpine t (PJ l x y i f) = AxJ (quote l) (quote x) (quote y) (quote i) (quote f) t
goSpine t PProj1 = Proj1 t goSpine t PProj1 = Proj1 t
goSpine t PProj2 = Proj2 t goSpine t PProj2 = Proj2 t
goSpine t (POuc a phi u) = Ouc (quote a) (quote phi) (quote u) t goSpine t (POuc a phi u) = Ouc (quote a) (quote phi) (quote u) t
constantly 0 n = quoteWith short names n
constantly 0 n = quoteWith names n
constantly k x = Lam Ex (Bound (T.pack "x") (negate 1)) $ constantly (k - 1) x constantly k x = Lam Ex (Bound (T.pack "x") (negate 1)) $ constantly (k - 1) x
quoteWith short names (GluedVl _ Seq.Empty x) = quoteWith short names x
quoteWith short names (GluedVl h sp (VLam p (Closure n k))) =
quoteWith short names (VLam p (Closure n (\a -> GluedVl h (sp Seq.:|> PApp p a) (k a))))
quoteWith names (GluedVl _ Seq.Empty x) = quoteWith names x
quoteWith short names (GluedVl h sp (VLine ty x y (VLam p (Closure n k)))) =
quoteWith short 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 (VLam p (Closure n k))) =
quoteWith names (VLam p (Closure n (\a -> GluedVl h (sp Seq.:|> PApp p a) (k a))))
quoteWith short names (GluedVl h sp vl)
| GluedVl _ _ inner <- vl = quoteWith short names (GluedVl h sp inner)
| short || alwaysShort vl = quoteWith short names vl
| _ Seq.:|> PIElim _ x y i <- sp =
case i of
VI0 -> quoteWith short names x
VI1 -> quoteWith short names y
_ -> quoteWith short names (VNe h sp)
| otherwise = quoteWith short names (VNe h sp)
quoteWith names (GluedVl h sp vl)
| GluedVl _ _ inner <- vl = quoteWith names (GluedVl h sp inner)
| True || alwaysShort vl = quoteWith names vl
| otherwise = quoteWith names (VNe h sp)
quoteWith short names (VLam p (Closure n k)) =
quoteWith names (VLam p (Closure n k)) =
let n' = refresh Nothing names n let n' = refresh Nothing names n
in Lam p n' (quoteWith short (Set.insert n' names) (k (VVar n')))
in Lam p n' (quoteWith (Set.insert n' names) (k (VVar n')))
quoteWith short names (VPi p d (Closure n k)) =
quoteWith names (VPi p d (Closure n k)) =
let n' = refresh (Just d) names n let n' = refresh (Just d) names n
in Pi p n' (quoteWith short names d) (quoteWith short (Set.insert n' names) (k (VVar n')))
in Pi p n' (quoteWith names d) (quoteWith (Set.insert n' names) (k (VVar n')))
quoteWith short names (VSigma d (Closure n k)) =
quoteWith names (VSigma d (Closure n k)) =
let n' = refresh (Just d) names n let n' = refresh (Just d) names n
in Sigma n' (quoteWith short names d) (quoteWith short (Set.insert n' names) (k (VVar n')))
in Sigma n' (quoteWith names d) (quoteWith (Set.insert n' names) (k (VVar n')))
quoteWith short names (VPair a b) = Pair (quoteWith short names a) (quoteWith short names b)
quoteWith _ _ VType = Type
quoteWith _ _ VTypeω = Typeω
quoteWith names (VPair a b) = Pair (quoteWith names a) (quoteWith names b)
quoteWith _ VType = Type
quoteWith _ VTypeω = Typeω
quoteWith _ _ VI = I
quoteWith _ _ VI0 = I0
quoteWith _ _ VI1 = I1
quoteWith short names (VIAnd x y) = IAnd (quoteWith short names x) (quoteWith short names y)
quoteWith short names (VIOr x y) = IOr (quoteWith short names x) (quoteWith short names y)
quoteWith short names (VINot x) = INot (quoteWith short names x)
quoteWith _ VI = I
quoteWith _ VI0 = I0
quoteWith _ VI1 = I1
quoteWith names (VIAnd x y) = IAnd (quoteWith names x) (quoteWith names y)
quoteWith names (VIOr x y) = IOr (quoteWith names x) (quoteWith names y)
quoteWith names (VINot x) = INot (quoteWith names x)
quoteWith short names (VPath line x y) = PathP (quoteWith short names line) (quoteWith short names x) (quoteWith short names y)
quoteWith short names (VLine p x y f) = PathIntro (quoteWith short names p) (quoteWith short names x) (quoteWith short names y) (quoteWith short names f)
quoteWith names (VPath line x y) = PathP (quoteWith names line) (quoteWith names x) (quoteWith names y)
quoteWith names (VLine p x y f) = PathIntro (quoteWith names p) (quoteWith names x) (quoteWith names y) (quoteWith names f)
quoteWith short names (VPartial x y) = Partial (quoteWith short names x) (quoteWith short names y)
quoteWith short names (VPartialP x y) = PartialP (quoteWith short names x) (quoteWith short names y)
quoteWith short names (VSystem fs) = System (Map.fromList (map (\(x, y) -> (quoteWith short names x, quoteWith short names y)) (Map.toList fs)))
quoteWith short names (VSub a b c) = Sub (quoteWith short names a) (quoteWith short names b) (quoteWith short names c)
quoteWith short names (VInc a b c) = Inc (quoteWith short names a) (quoteWith short names b) (quoteWith short names c)
quoteWith short names (VComp a phi u a0) = Comp (quoteWith short names a) (quoteWith short names phi) (quoteWith short names u) (quoteWith short names a0)
quoteWith short names (VHComp a phi u a0) = HComp (quoteWith short names a) (quoteWith short names phi) (quoteWith short names u) (quoteWith short names a0)
quoteWith names (VIsOne v) = IsOne (quoteWith names v)
quoteWith _ VItIsOne = ItIsOne
quoteWith short names (VGlueTy a phi t e) = GlueTy (quoteWith short names a) (quoteWith short names phi) (quoteWith short names t) (quoteWith short names e)
quoteWith short names (VGlue a phi ty e t x) = Glue (quoteWith short names a) (quoteWith short names phi) (quoteWith short names ty) (quoteWith short names e) (quoteWith short names t) (quoteWith short names x)
quoteWith short names (VUnglue a phi ty e x) = Unglue (quoteWith short names a) (quoteWith short names phi) (quoteWith short names ty) (quoteWith short names e) (quoteWith short names x)
quoteWith names (VPartial x y) = Partial (quoteWith names x) (quoteWith names y)
quoteWith names (VPartialP x y) = PartialP (quoteWith names x) (quoteWith names y)
quoteWith names (VSystem fs) = System (Map.fromList (map (\(x, y) -> (quoteWith names x, quoteWith names y)) (Map.toList fs)))
quoteWith names (VSub a b c) = Sub (quoteWith names a) (quoteWith names b) (quoteWith names c)
quoteWith names (VInc a b c) = Inc (quoteWith names a) (quoteWith names b) (quoteWith names c)
quoteWith names (VComp a phi u a0) = Comp (quoteWith names a) (quoteWith names phi) (quoteWith names u) (quoteWith names a0)
quoteWith names (VHComp a phi u a0) = HComp (quoteWith names a) (quoteWith names phi) (quoteWith names u) (quoteWith names a0)
quoteWith short names (VCase _ rng v xs) = Case (quoteWith short names rng) (quoteWith short names v) xs
quoteWith names (VGlueTy a phi t e) = GlueTy (quoteWith names a) (quoteWith names phi) (quoteWith names t) (quoteWith names e)
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 short names (VEqStrict a x y) = EqS (quoteWith short names a) (quoteWith short names x) (quoteWith short names y)
quoteWith short names (VReflStrict a x) = Syntax.Refl (quoteWith short names a) (quoteWith short names x)
quoteWith names (VCase _ rng v xs) = Case (quoteWith names rng) (quoteWith names v) xs
alwaysShort :: Value -> Bool alwaysShort :: Value -> Bool
alwaysShort (VNe HCon{} _) = True alwaysShort (VNe HCon{} _) = True
alwaysShort (VNe HPCon{} _) = True
alwaysShort VVar{} = True alwaysShort VVar{} = True
alwaysShort (VLine _ _ _ v) = alwaysShort v
alwaysShort (VLam _ (Closure n k)) = alwaysShort (k (VVar n))
alwaysShort VHComp{} = True
alwaysShort _ = False alwaysShort _ = False
refresh :: Maybe Value -> Set Name -> Name -> Name refresh :: Maybe Value -> Set Name -> Name -> Name
@ -297,7 +271,7 @@ refresh x s n
| otherwise = refresh x s (Bound (getNameText n <> T.singleton '\'') 0) | otherwise = refresh x s (Bound (getNameText n <> T.singleton '\'') 0)
quote :: Value -> Term quote :: Value -> Term
quote = quoteWith True mempty
quote = quoteWith mempty
data Closure data Closure
= Closure = Closure
@ -322,31 +296,15 @@ data Head
| HPCon Value Value Name | HPCon Value Value Name
| HMeta MV | HMeta MV
| HData Bool Name | HData Bool Name
deriving (Ord, Show)
instance Eq Head where
HVar x == HVar y = x == y
HCon _ x == HCon _ y = x == y
HPCon _ _ x == HPCon _ _ y = x == y
HMeta x == HMeta y = x == y
HData x y == HData x' y' = x == x' && y == y'
_ == _ = False
deriving (Eq, Ord, Show)
data Projection data Projection
= PApp Plicity Value = PApp Plicity Value
| PIElim Value Value Value NFEndp | PIElim Value Value Value NFEndp
| PProj1 | PProj1
| PProj2 | PProj2
| POuc NFSort NFEndp Value
| PK NFSort Value NFSort Value
| PJ NFSort Value NFSort Value Value
| POuc NFSort NFEndp Value
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)
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)

+ 179
- 202
src/Syntax/Pretty.hs View File

@ -1,14 +1,17 @@
{-# LANGUAGE LambdaCase #-}
{-# OPTIONS_GHC -Wno-orphans #-} {-# OPTIONS_GHC -Wno-orphans #-}
{-# LANGUAGE ViewPatterns #-} {-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE CPP #-}
module Syntax.Pretty where module Syntax.Pretty where
import Control.Arrow (Arrow(first))
import qualified Data.Map.Strict as Map import qualified Data.Map.Strict as Map
import qualified Data.Text.Lazy as Lazy
import qualified Data.Text.Lazy as L
import qualified Data.Set as Set
import qualified Data.Text as T import qualified Data.Text as T
import Data.Map.Strict (Map) import Data.Map.Strict (Map)
import Data.Text (Text)
import Data.Set (Set)
import Data.Generics
import Presyntax.Presyntax (Plicity(..)) import Presyntax.Presyntax (Plicity(..))
@ -18,216 +21,190 @@ import Prettyprinter
import Syntax import Syntax
instance Pretty Name where instance Pretty Name where
pretty x = pretty (getNameText x) -- <> pretty '\'' <> pretty (getNameNum x)
prettyTm' :: Bool -> Term -> Doc AnsiStyle
prettyTm' implicits = go True 0 where
go t p =
\case
Ref v -> pretty v
Con v -> keyword $ pretty v
PCon _ v -> keyword $ pretty v
Data _ v -> keyword $ pretty v
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
getArgs (Lam i v t) =
let (as, b) = getArgs t in ((i, v):as, b)
getArgs (PathIntro _ _ _ (Lam _ v t)) =
let (as, b) = getArgs t in ((Ex, v):as, b)
getArgs t = ([], t)
(as, b) = getArgs (Lam i v t)
in
parenIf (p >= fun_prec) . group $
pretty '\\' <> hsep (map (\(i, v) -> braceIf (i == Im) (pretty v)) as)
<+> arrow
<+> nest 2 (go False 0 b)
Pi _ (T.unpack . getNameText -> "_") d r ->
parenIf (p >= fun_prec) $
group (go False dom_prec d)
<> space <> arrow <> sp
<> go t 0 r
Pi i x d r ->
let
c = case r of
Pi _ (getNameText -> x) _ _ | x /= T.pack "_" -> sp
_ -> space <> arrow <> sp
in
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 False binds)
<> keyword (pretty "in")
<+> go False 0 body
Meta MV{mvName} -> keyword (pretty '?' <> pretty mvName)
Type -> keyword (pretty "Type")
Typeω -> keyword (pretty "Pretype")
Sigma (T.unpack . getNameText -> "_") d r ->
parenIf (p >= fun_prec) $
go False dom_prec d
<+> operator (pretty "*")
<+> go False dom_prec r
Sigma v d r ->
parenIf (p >= fun_prec) . align $
group (parens (pretty v <+> colon <+> go False 0 d))
<+> operator (pretty "*") <+> go False dom_prec r
Pair a b -> parens $ go False 0 a <> comma <+> go False 0 b
Proj1 a -> parenIf (p >= arg_prec) $ go False 0 a <> keyword (pretty ".1")
Proj2 a -> parenIf (p >= arg_prec) $ go False 0 a <> keyword (pretty ".2")
I -> keyword (pretty "I")
I0 -> keyword (pretty "i0")
I1 -> keyword (pretty "i1")
IAnd x y -> parenIf (True || p > and_prec) $
go False and_prec x <+> operator (pretty "/\\") <+> go False and_prec y
IOr x y -> parenIf (True || p > or_prec) $
go False or_prec x <+> operator (pretty "\\/") <+> go False or_prec y
INot x -> operator (pretty "~") <> go False p x
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
Partial a p -> apps (con "Partial") [(Ex, a), (Ex, p)]
PartialP a p -> apps (con "PartialP") [(Ex, a), (Ex, p)]
System fs | Map.null fs -> brackets mempty
System fs ->
let
face (f, t) = go False 0 f <+> operator (pretty "=>") <+> go False 0 t
in
brackets (line <> nest 2 (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") [(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") [(Im, _a), (Im, _phi), (Im, _ty), (Im, _e), (Ex, t)]
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
oneCase (c, 0, l) = go False 0 c <+> operator (pretty "=>") <+> go False 0 l
oneCase (c, i, l) =
let (args, bd) = getLams i l
in go False 0 c <+> hsep (map pretty args) <+> operator (pretty "=>") <+> go False 0 bd
getLams 0 x = ([], x)
getLams n (Lam _ v t) = let (as, b) = getLams (n - 1) t in (v:as, b)
getLams _ x = ([], x)
in
parenIf (p >= fun_prec) $
keyword (pretty "case") <+> go False 0 t <+> keyword (pretty "of")
<> line
<> indent 2 (vsep (map oneCase cs))
EqS _ x y -> parenIf (p >= arg_prec) $
go False 0 x <+> operator (pretty "≡S") <+> go False 0 y
Syntax.Refl _ _ -> keyword (pretty "refl")
Syntax.AxK _ _ bigp pr eq -> apps (con "K_s") [(Ex, bigp), (Ex, pr), (Ex, eq)]
Syntax.AxJ _ _ bigp pr _ eq -> apps (con "J_s") [(Ex, bigp), (Ex, pr), (Ex, eq)]
where
sp | t = softline
| otherwise = space
parenIf p x | p = parens x
| otherwise = x
braceIf p x | p = braces x
| otherwise = x
con x = Con (Bound (T.pack x) 0)
plic = \case
Ex -> parens
Im -> braces
arrow = operator (pretty "->")
instead = go t p
apps :: Term -> [(Plicity, Term)] -> Doc AnsiStyle
apps f xs = instead (foldl (\f (p, x) -> App p f x) f xs)
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' imp tm)
<> line
<> prettyBinds imp bs
pretty = pretty . getNameText
showFace :: Bool -> Map Head Bool -> Doc AnsiStyle
showFace imp = hsep . map go . Map.toList where
go (h, b) = parens $ prettyTm' imp (quoteWith False mempty (VNe h mempty)) <+> operator (pretty "=") <+> pretty (if b then "i1" else "i0")
prettyTm :: Term -> Doc AnsiStyle
prettyTm = prettyTm . everywhere (mkT beautify) where
prettyTm (Ref v) =
case T.uncons (getNameText v) of
Just ('.', w) -> keyword (pretty w)
_ -> pretty v
prettyTm (Con v) = keyword (pretty v)
prettyTm (PCon _ v) = keyword (pretty v)
prettyTm (Data _ v) = operator (pretty v)
prettyVl' :: Bool -> Value -> Doc AnsiStyle
prettyVl' b = prettyTm' b . quoteWith True mempty
prettyTm (App Im f x) = parenFun f <+> braces (prettyTm x)
prettyTm (App Ex f x) = parenFun f <+> parenArg x
instance Pretty Term where
pretty = unAnnotate . prettyTm
prettyTm (Pair x y) = parens $ prettyTm x <> operator comma <+> prettyTm y
prettyTm (Proj1 x) = prettyTm x <> operator (pretty ".1")
prettyTm (Proj2 x) = prettyTm x <> operator (pretty ".2")
prettyTm :: Term -> Doc AnsiStyle
prettyTm = prettyTm' printImplicits
prettyTm l@(Lam _ _ _) = pretty '\\' <> hsep (map prettyArgList al) <+> pretty "->" <+> nest 2 (prettyTm bod) where
unwindLam (Lam p x y) = first ((p, x):) (unwindLam y)
unwindLam (PathIntro _ _ _ (Lam p x y)) = first ((p, x):) (unwindLam y)
unwindLam t = ([], t)
(al, bod) = unwindLam l
used = freeVars bod
prettyArgList (Ex, v)
| v `Set.member` used = pretty v
| otherwise = pretty "_"
prettyArgList (Im, v)
| v `Set.member` used = braces $ pretty v
| otherwise = pretty "_"
prettyTm (Meta x) = keyword $ pretty '?' <> pretty (mvName x)
prettyTm Type{} = keyword $ pretty "Type"
prettyTm Typeω{} = keyword $ pretty "Typeω"
prettyTm I{} = keyword $ pretty "I"
prettyTm I0{} = keyword $ pretty "i0"
prettyTm I1{} = keyword $ pretty "i1"
prettyTm (Pi Ex (T.unpack . getNameText -> "_") d r) = prettyDom d <+> pretty "->" <+> prettyTm r
prettyTm (Pi Im v d r) = group (braces (pretty v <+> colon <+> prettyTm d)) <> softline <> pretty "->" <+> prettyTm r
prettyTm (Pi Ex v d r) = group (parens (pretty v <+> colon <+> prettyTm d)) <> softline <> pretty "->" <+> prettyTm r
prettyTm (Sigma (T.unpack . getNameText -> "_") d r) = prettyDom d <+> pretty "*" <+> prettyTm r
prettyTm (Sigma v d r) = parens (pretty v <+> colon <+> prettyTm d) <+> pretty "*" <+> prettyTm r
prettyTm (IAnd 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
instance Pretty Value where
pretty = unAnnotate . prettyVl
prettyTm (System (Map.null -> True)) = braces mempty
prettyVl :: Value -> Doc AnsiStyle
prettyVl = prettyVl' printImplicits
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
printImplicits :: Bool
#if defined(RELEASE)
printImplicits = False
#else
printImplicits = True
#endif
prettyTm (Case _ x xs) = keyword (pretty "case") <+> prettyTm x <+> keyword (pretty "of") <+> braces (line <> indent 2 (prettyCase xs) <> line)
prettyTm (Let xs e) = align $ keyword (pretty "let") <+> braces (line <> indent 2 (prettyLet xs) <> line) <+> keyword (pretty "in") <+> prettyTm e
render :: Doc AnsiStyle -> Lazy.Text
render = renderLazy . layoutSmart defaultLayoutOptions
prettyTm x = error (show x)
arg_prec, fun_prec, dom_prec, and_prec, or_prec :: Int
dom_prec = succ fun_prec
arg_prec = succ and_prec
and_prec = succ or_prec
or_prec = succ fun_prec
fun_prec = 1
prettyCase = vcat . map go where
go (x, _, xs) = prettyTm x <+> operator (pretty "=>") <+> prettyTm xs
prettyLet = vcat . map go where
go (x, t, y) = pretty x <+> align (colon <+> nest (- 1) (prettyTm t)) <> line <> pretty x <+> pretty "=" <+> prettyTm y
beautify (PathP l x y) = toFun "PathP" [l, x, y]
beautify (IElim _ _ _ f i) = App Ex f i
beautify (PathIntro _ _ _ f) = f
beautify (App _ (Lam _ v b) _)
| v `Set.notMember` freeVars b = beautify b
beautify (IsOne phi) = toFun "IsOne" [phi]
beautify ItIsOne = Ref (Bound (T.pack ".1=1") 0)
beautify (Lam Ex v (App Ex f (Ref v')))
| 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 (PartialP phi a) = toFun "PartialP" [phi, a]
beautify (Comp a phi u a0) = toFun "comp" [a, phi, u, a0]
beautify (HComp a phi u a0) = toFun "hcomp" [a, phi, u, a0]
beautify (Sub a phi u) = toFun "Sub" [a, phi, u]
beautify (Inc _ _ u) = toFun "inS" [u]
beautify (Ouc a phi u u0) = toFun "outS" [a, phi, u, u0]
beautify (GlueTy _ I1 (Lam _ _ a) _) = 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]
beautify (Unglue a b c d e) = toFun "unglue" [a,b,c,d,e]
beautify x = x
toFun s a = foldl (App Ex) (Ref (Bound (T.pack ('.':s)) 0)) a
keyword :: Doc AnsiStyle -> Doc AnsiStyle keyword :: Doc AnsiStyle -> Doc AnsiStyle
keyword = annotate (color Magenta) keyword = annotate (color Magenta)
operator :: Doc AnsiStyle -> Doc AnsiStyle operator :: Doc AnsiStyle -> Doc AnsiStyle
operator = annotate (color Yellow) operator = annotate (color Yellow)
parenArg :: Term -> Doc AnsiStyle
parenArg x@App{} = parens (prettyTm x)
parenArg x@IElim{} = parens (prettyTm x)
parenArg x@IsOne{} = parens $ prettyTm x
parenArg x@Partial{} = parens $ prettyTm x
parenArg x@PartialP{} = parens $ prettyTm x
parenArg x@Sub{} = parens $ prettyTm x
parenArg x@Inc{} = parens $ prettyTm x
parenArg x@Ouc{} = parens $ prettyTm x
parenArg x@Comp{} = parens $ prettyTm x
parenArg x@Case{} = parens $ prettyTm x
parenArg x = prettyDom x
prettyDom :: Term -> Doc AnsiStyle
prettyDom x@Pi{} = parens (prettyTm x)
prettyDom x@Sigma{} = parens (prettyTm x)
prettyDom x = parenFun x
parenFun :: Term -> Doc AnsiStyle
parenFun x@Lam{} = parens $ prettyTm x
parenFun x@PathIntro{} = parens $ prettyTm x
parenFun x = prettyTm x
render :: Doc AnsiStyle -> Text
render = L.toStrict . renderLazy . layoutSmart defaultLayoutOptions
showValue :: Value -> String
showValue = L.unpack . renderLazy . layoutSmart defaultLayoutOptions . prettyTm . quote
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")
freeVars :: Term -> Set Name
freeVars (Ref v) = Set.singleton v
freeVars (App _ f x) = Set.union (freeVars f) (freeVars x)
freeVars (Pi _ n x y) = Set.union (freeVars x) (n `Set.delete` freeVars y)
freeVars (Lam _ n x) = n `Set.delete` freeVars x
freeVars (Let ns x) = Set.union (freeVars x `Set.difference` bound) freed where
bound = Set.fromList (map (\(x, _, _) -> x) ns)
freed = foldr (\(_, x, y) -> Set.union (Set.union (freeVars x) (freeVars y))) mempty ns
freeVars Meta{} = mempty
freeVars Con{} = mempty
freeVars PCon{} = mempty
freeVars Data{} = mempty
freeVars Type{} = mempty
freeVars Typeω{} = mempty
freeVars I{} = mempty
freeVars I0{} = mempty
freeVars I1{} = mempty
freeVars (Sigma n x y) = Set.union (freeVars x) (n `Set.delete` freeVars y)
freeVars (Pair x y) = Set.unions $ map freeVars [x, y]
freeVars (Proj1 x) = Set.unions $ map freeVars [x]
freeVars (Proj2 x) = Set.unions $ map freeVars [x]
freeVars (IAnd x y) = Set.unions $ map freeVars [x, y]
freeVars (IOr x y) = Set.unions $ map freeVars [x, y]
freeVars (INot x) = Set.unions $ map freeVars [x]
freeVars (PathP x y z) = Set.unions $ map freeVars [x, y, z]
freeVars (IElim x y z a b) = Set.unions $ map freeVars [x, y, z, a, b]
freeVars (PathIntro x y z a) = Set.unions $ map freeVars [x, y, z, a]
freeVars (IsOne a) = Set.unions $ map freeVars [a]
freeVars ItIsOne{} = mempty
freeVars (Partial x y) = Set.unions $ map freeVars [x, y]
freeVars (PartialP x y) = Set.unions $ map freeVars [x, y]
freeVars (System fs) = foldr (\(x, y) -> Set.union (Set.union (freeVars x) (freeVars y))) mempty (Map.toList fs)
freeVars (Sub x y z) = Set.unions $ map freeVars [x, y, z]
freeVars (Inc x y z) = Set.unions $ map freeVars [x, y, z]
freeVars (Ouc x y z a) = Set.unions $ map freeVars [x, y, z, a]
freeVars (Comp x y z a) = Set.unions $ map freeVars [x, y, z, a]
freeVars (HComp x y z a) = Set.unions $ map freeVars [x, y, z, a]
freeVars (GlueTy x y z a) = Set.unions $ map freeVars [x, y, z, a]
freeVars (Glue x y z a b c) = Set.unions $ map freeVars [x, y, z, a, b, c]
freeVars (Unglue x y z a c) = Set.unions $ map freeVars [x, y, z, a, c]
freeVars (Case rng x y) = freeVars rng <> freeVars x <> foldMap (\(_, _, y) -> freeVars y) y

+ 64
- 2
stack.yaml View File

@ -1,5 +1,67 @@
# This file was automatically generated by 'stack init'
#
# Some commonly used options have been documented as comments in this file.
# For advanced use and comprehensive documentation of the format, please see:
# https://docs.haskellstack.org/en/stable/yaml_configuration/
# Resolver to choose a 'specific' stackage snapshot or a compiler version.
# A snapshot resolver dictates the compiler version and the set of packages
# to be used for project dependencies. For example:
#
# resolver: lts-3.5
# resolver: nightly-2015-09-21
# resolver: ghc-7.10.2
#
# The location of a snapshot can be provided as a file or url. Stack assumes
# a snapshot provided as a file might change, whereas a url resource does not.
#
# resolver: ./custom-snapshot.yaml
# resolver: https://example.com/snapshots/2018-01-01.yaml
resolver: resolver:
url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/8.yaml
url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/1.yaml
# User packages to be built.
# Various formats can be used as shown in the example below.
#
# packages:
# - some-directory
# - https://example.com/foo/bar/baz-0.0.2.tar.gz
# subdirs:
# - auto-update
# - wai
packages: packages:
- .
- .
# Dependency packages to be pulled from upstream that are not in the resolver.
# These entries can reference officially published versions as well as
# forks / in-progress versions pinned to a git hash. For example:
#
# extra-deps:
# - acme-missiles-0.3
# - git: https://github.com/commercialhaskell/stack.git
# commit: e7b331f14bcffb8367cd58fbfc8b40ec7642100a
#
# extra-deps: []
# Override default flag values for local packages and extra-deps
# flags: {}
# Extra package databases containing global packages
# extra-package-dbs: []
# Control whether we use the GHC we find on the path
# system-ghc: true
#
# Require a specific version of stack, using version ranges
# require-stack-version: -any # Default
# require-stack-version: ">=2.5"
#
# Override the architecture used by stack, especially useful on Windows
# arch: i386
# arch: x86_64
#
# Extra directories used by stack for building
# extra-include-dirs: [/path/to/dir]
# extra-lib-dirs: [/path/to/dir]
#
# Allow a newer minor version of GHC than the snapshot specifies
# compiler-check: newer-minor

+ 4
- 4
stack.yaml.lock View File

@ -6,8 +6,8 @@
packages: [] packages: []
snapshots: snapshots:
- completed: - completed:
size: 565720
url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/8.yaml
sha256: 76bf8992ff8dfe6eda9c02f81866138c2369344d5011ab39ae403457c4448b03
size: 563098
url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/1.yaml
sha256: 395775c03e66a4286f134d50346b0b6f1432131cf542886252984b4cfa5fef69
original: original:
url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/8.yaml
url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/1.yaml

Loading…
Cancel
Save