14 Commits

19 changed files with 2976 additions and 1056 deletions
Split View
  1. +3
    -2
      cubical.cabal
  2. +1624
    -193
      intro.tt
  3. +45
    -0
      src/Debug.hs
  4. +115
    -113
      src/Elab.hs
  5. +319
    -193
      src/Elab/Eval.hs
  6. +31
    -11
      src/Elab/Eval/Formula.hs
  7. +18
    -0
      src/Elab/Eval/Formula.hs-boot
  8. +30
    -5
      src/Elab/Monad.hs
  9. +272
    -129
      src/Elab/WiredIn.hs
  10. +18
    -11
      src/Elab/WiredIn.hs-boot
  11. +148
    -63
      src/Main.hs
  12. +22
    -5
      src/Presyntax/Lexer.x
  13. +20
    -22
      src/Presyntax/Parser.y
  14. +2
    -5
      src/Presyntax/Presyntax.hs
  15. +2
    -0
      src/Presyntax/Tokens.hs
  16. +99
    -57
      src/Syntax.hs
  17. +202
    -179
      src/Syntax/Pretty.hs
  18. +2
    -64
      stack.yaml
  19. +4
    -4
      stack.yaml.lock

+ 3
- 2
cubical.cabal View File

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

+ 1624
- 193
intro.tt
File diff suppressed because it is too large
View File


+ 45
- 0
src/Debug.hs View File

@ -0,0 +1,45 @@
{-# 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

+ 115
- 113
src/Elab.hs View File

@ -4,6 +4,7 @@
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE EmptyCase #-}
module Elab where
import Control.Arrow (Arrow(first))
@ -14,6 +15,7 @@ import qualified Data.Map.Strict as Map
import qualified Data.Sequence as Seq
import qualified Data.Set as Set
import qualified Data.Text as T
import Data.Maybe (fromMaybe)
import Data.Traversable
import Data.Text (Text)
import Data.Map (Map)
@ -53,10 +55,10 @@ infer (P.App p f x) = do
x_nf <- eval x
pure (IElim (quote (fun li)) (quote le) (quote ri) (wp f) x, li x_nf)
It'sPartial phi a w -> do
x <- check x (VIsOne phi)
x <- check x (VEqStrict VI phi VI1)
pure (App P.Ex (w f) x, a)
It'sPartialP phi a w -> do
x <- check x (VIsOne phi)
x <- check x (VEqStrict VI phi VI1)
x_nf <- eval x
pure (App P.Ex (w f) x, a @@ x_nf)
@ -100,20 +102,17 @@ check (P.Lam p v b) ty = do
tm_nf <- eval tm
unify (tm_nf @@ VI0) le
`catchElab` (throwElab . WhenCheckingEndpoint le ri VI0)
unify (tm_nf @@ VI1) ri
`catchElab` (throwElab . WhenCheckingEndpoint le ri VI1)
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)
pure (wp (PathIntro (quote (fun li)) (quote le) (quote ri) tm))
It'sPartial phi a wp ->
assume (Bound v 0) (VIsOne phi) $ \var ->
assume (Bound v 0) (VEqStrict VI phi VI1) $ \var ->
wp . Lam p var <$> check b a
It'sPartialP phi a wp ->
assume (Bound v 0) (VIsOne phi) $ \var ->
assume (Bound v 0) (VEqStrict VI phi VI1) $ \var ->
wp . Lam p var <$> check b (a @@ VVar var)
check (P.Pair a b) ty = do
@ -146,54 +145,36 @@ check (P.Let items body) ty = do
check (P.LamSystem bs) ty = do
(extent, dom) <- isPartialType ty
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)
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)))
pure (n, (phi, head rhses))
unify extent (foldl ior VI0 (map (fst . snd) eqns))
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
for_ eqns \(n, (formula, rhs)) -> do
for_ eqns $ \(n', (formula', rhs')) -> do
let
k = case binding of
Just v -> assume v (VIsOne formula) . const
Nothing -> id
truth = possible mempty (iand formula formula')
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'
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'
unify vl vl'
`withNote` vsep [ pretty "These two cases must agree because they are both possible:"
, indent 2 $ pretty '*' <+> prettyTm (quote formula) <+> operator (pretty "=>") <+> prettyTm rhs
, indent 2 $ pretty '*' <+> prettyTm (quote formula') <+> operator (pretty "=>") <+> prettyTm rhs'
, indent 2 $ pretty '*' <+> prettyTm (quote formula) <+> operator (pretty "=>") <+> pretty vl
, indent 2 $ pretty '*' <+> prettyTm (quote formula') <+> operator (pretty "=>") <+> pretty (zonk vl')
]
`withNote` (pretty "Consider this face, where both are true:" <+> showFace (snd truth))
`withNote` (pretty "Consider this face, where both are true:" <+> showFace False (snd truth))
name <- newName
let
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))))
pure (Lam P.Ex name (System (Map.fromList (map (\(_, (x, y)) -> (quote x, y)) eqns))))
check (P.LamCase pats) ty =
do
@ -204,7 +185,7 @@ check (P.LamCase pats) ty =
let range = Lam P.Ex name (quote (rng (VVar name)))
cases <- checkPatterns range [] pats \partialPats (pat, rhs) -> do
checkPattern pat dom \pat wp boundary pat_nf -> do
checkPattern pat dom \pat wp boundary n_lams pat_nf -> do
rhs <- check rhs (rng pat_nf)
case boundary of
-- If we're checking a higher constructor then we need to
@ -226,19 +207,22 @@ check (P.LamCase pats) ty =
let
base = appDummies (VVar <$> dummies) ty rhs_nf
sys = boundaryFormulas (drop a dummies ++ getBoundaryNames boundary) (getBoundaryMap boundary)
for_ (Map.toList sys) \(formula, side) -> do
let rhs = cases @@ side
for_ (truthAssignments formula mempty) $ \i -> do
let vl = foldl (\v n -> vApp P.Ex v (snd (i Map.! 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))
unify vl rhs
`withNote` (pretty "From the boundary conditions of the constructor" <+> prettyTm (quote pat_nf) <> pretty ":")
`withNote` vcat [ pretty "These must be the same because of the face"
, indent 2 $ prettyTm (quote formula) <+> operator (pretty "=>") <+> prettyTm (quote (zonk side))
, indent 2 $ prettyVl (zonk formula) <+> operator (pretty "=>") <+> prettyVl (zonk side)
, pretty "which is mapped to"
, indent 2 $ prettyVl (zonk formula) <+> operator (pretty "=>") <+> prettyVl (zonk rhs)
]
`withNote` (pretty "Mandated by the constructor" <+> prettyTm (quote pat_nf))
_ -> pure ()
pure (pat, wp rhs)
pure (pat, n_lams, wp rhs)
let x = wp (Lam P.Ex name (Case range (Ref name) cases))
pure x
_ -> do
@ -251,9 +235,9 @@ check (P.LamCase pats) ty =
checkPatterns _ acc [] _ = pure (reverse acc)
checkPatterns rng acc (x:xs) k = do
n <- newName
(p, t) <- k (eval (Lam P.Ex n (Case rng (Ref n) acc))) x
checkPatterns rng ((p, t):acc) xs k
(p, n, t) <- k (eval (Lam P.Ex n (Case rng (Ref n) acc))) x
checkPatterns rng ((p, n, t):acc) xs k
appDummies (v:vl) (VPi p _ (Closure _ r)) x = appDummies vl (r v) (vApp p x v)
appDummies [] _ x = x
appDummies vs t _ = error (show (vs, t))
@ -262,12 +246,16 @@ check (P.LamCase pats) ty =
boundaryFormulas (x:xs) k = boundaryFormulas xs $ k @@ VVar x
boundaryFormulas a b = error (show (a, b))
check P.Hole ty = do
t <- newMeta' True ty
pure (quote t)
check exp ty = do
(tm, has) <- switch $ infer exp
wp <- isConvertibleTo has ty
pure (wp tm)
checkPattern :: P.Pattern -> NFSort -> (Term -> (Term -> Term) -> Maybe Boundary -> Value -> ElabM a) -> ElabM a
checkPattern :: P.Pattern -> NFSort -> (Term -> (Term -> Term) -> Maybe Boundary -> Int -> Value -> ElabM a) -> ElabM a
checkPattern (P.PCap var) dom cont = do
name <- asks (Map.lookup var . nameMap)
case name of
@ -276,9 +264,9 @@ checkPattern (P.PCap var) dom cont = do
(ty, wp, _) <- instantiate =<< getNfType name
unify ty dom
wrap <- skipLams skip
cont (Con name) wrap Nothing =<< eval (wp (Con name))
cont (Con name) wrap Nothing 0 =<< eval (wp (Con name))
Just name -> throwElab $ NotACon name
Nothing -> assume (Bound var 0) dom \name -> cont (Ref name) (Lam P.Ex name) Nothing (VVar name)
Nothing -> assume (Bound var 0) dom \name -> cont (Ref name) (Lam P.Ex name) Nothing 0 (VVar name)
checkPattern (P.PCon var args) dom cont =
do
@ -295,7 +283,7 @@ checkPattern (P.PCon var args) dom cont =
con <- quote <$> getValue name
bindNames args ty $ \names wrap ->
cont (Con name) (skip . wrap) (instBoundary xs <$> t) =<< eval (foldl (\x y -> App P.Ex x (Ref y)) (wp con) names)
cont (Con name) (skip . wrap) (instBoundary xs <$> t) (length names) =<< eval (foldl (\x y -> App P.Ex x (Ref y)) (wp con) names)
Just name -> throwElab $ NotACon name
_ -> throwElab $ NotInScope (Bound var 0)
@ -327,13 +315,17 @@ skipLams k = do
n <- newName
(Lam P.Im n . ) <$> skipLams (k - 1)
checkLetItems :: Map Text (Maybe NFType) -> [P.LetItem] -> ([(Name, Term, Term)] -> ElabM a) -> ElabM a
checkLetItems _ [] cont = cont []
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 map (P.LetDecl v t:xs) cont = do
t <- check t VTypeω
t_nf <- eval t
assume (Defined v 0) t_nf \_ ->
checkLetItems (Map.insert v (Just t_nf) map) xs cont
assume (Defined v 0) t_nf \name ->
checkLetItems (Map.insert v (Just (name, t_nf)) map) xs cont
checkLetItems map (P.LetBind name rhs:xs) cont = do
case Map.lookup name map of
@ -344,28 +336,34 @@ checkLetItems map (P.LetBind name rhs:xs) cont = do
checkLetItems map xs \xs ->
cont ((name', quote ty, tm):xs)
Just Nothing -> throwElab $ Redefinition (Defined name 0)
Just (Just ty_nf) -> do
Just (Just (name, ty_nf)) -> do
rhs <- check rhs ty_nf
rhs_nf <- eval rhs
makeLetDef (Defined name 0) ty_nf rhs_nf \name' ->
checkLetItems (Map.insert name Nothing map) xs \xs ->
cont ((name', quote ty_nf, rhs):xs)
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
replaceLetDef name ty_nf rhs_nf $
checkLetItems (Map.insert (getNameText name) Nothing map) xs \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.FIs0 x) = do
nm <- getNameFor x
ty <- getNfType nm
unify ty VI
pure (inot (VVar nm))
pure (inot (VVar nm), Set.singleton nm)
checkFormula (P.FIs1 x) = do
nm <- getNameFor x
ty <- getNfType nm
unify ty VI
pure (VVar nm)
pure (VVar nm, Set.singleton nm)
isSort :: NFType -> ElabM ()
isSort t = isSort (force t) where
@ -427,15 +425,15 @@ isSigmaType t = isSigmaType (force t) where
wp <- isConvertibleTo t (VSigma dom (Closure name (const rng)))
pure (dom, const rng, wp)
isPartialType :: NFType -> ElabM (NFEndp, Value)
isPartialType :: NFType -> ElabM (NFEndp, Value -> Value)
isPartialType t = isPartialType (force t) where
isPartialType (VPartial phi a) = pure (phi, a)
isPartialType (VPartialP phi a) = pure (phi, a)
isPartialType (VPartial phi a) = pure (phi, const a)
isPartialType (VPartialP phi a) = pure (phi, (a @@))
isPartialType t = do
phi <- newMeta VI
dom <- newMeta (VPartial phi VType)
unify t (VPartial phi dom)
pure (phi, dom)
unify t (VPartialP phi dom)
pure (phi, (dom @@))
checkStatement :: P.Statement -> ElabM a -> ElabM a
checkStatement (P.SpanSt s a b) k = withSpan a b $ checkStatement s k
@ -494,21 +492,21 @@ checkStatement (P.ReplNf e) k = do
(e, _) <- infer e
e_nf <- eval e
h <- asks commHook
liftIO (h e_nf)
liftIO $ h . prettyVl =<< zonkIO e_nf
k
checkStatement (P.ReplTy e) k = do
(_, ty) <- infer e
(t, ty) <- infer e
h <- asks commHook
liftIO (h ty)
liftIO (h (prettyTm t <+> colon <+> align (prettyVl (zonk ty))))
k
checkStatement (P.Data name tele retk constrs) k =
do
checkTeleRetk True tele retk \kind tele undef -> do
checkTeleRetk tele retk \retk kind tele undef -> do
kind_nf <- eval kind
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)
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)
where
makeProj (x, p, _) = PApp p (VVar x)
@ -518,26 +516,22 @@ checkStatement (P.Data name tele retk constrs) k =
| any (\case { (_, _, P.Path{}) -> True; _ -> False}) constrs = HData True name
| otherwise = HData False name
checkTeleRetk allKan [] retk cont = do
checkTeleRetk [] retk cont = do
t <- check retk VTypeω
t_nf <- eval t
when allKan $ unify t_nf VType
cont t [] id
checkTeleRetk allKan ((x, p, t):xs) retk cont = do
r <- eval t
cont r t [] id
checkTeleRetk ((x, p, t):xs) retk cont = do
(t, ty) <- infer t
_ <- isConvertibleTo ty VTypeω
let
allKan' = case ty of
VType -> allKan
_ -> False
t_nf <- eval t
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 allKan' xs retk \k xs w -> cont (Pi p nm t k) ((nm, p, t_nf):xs) (rm nm . w)
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)
checkCons _ _et [] k = k
checkCons _ _ _et [] k = k
checkCons n ret ((s, e, P.Point x ty):xs) k = withSpan s e $ do
t <- check ty VTypeω
checkCons retk n ret ((s, e, P.Point x ty):xs) k = withSpan s e $ do
t <- check ty retk
ty_nf <- eval t
let
(args, ret') = splitPi ty_nf
@ -545,11 +539,12 @@ checkStatement (P.Data name tele retk constrs) k =
n' = map (\(x, _, y) -> (x, P.Im, y)) n
unify ret' ret
closed_nf <- eval closed
defineInternal (ConName x 0 (length n') (length args)) closed_nf (makeCon closed_nf mempty n' args) \_ -> checkCons n ret xs k
checkCons n ret ((s, e, P.Path name indices return faces):xs) k = withSpan s e $ do
defineInternal (ConName x 0 (length n') (length args)) closed_nf (makeCon closed_nf mempty n' args) \_ -> checkCons retk n ret xs k
checkCons retk n ret ((s, e, P.Path name indices return faces):xs) k = withSpan s e $ do
fibrant retk
(con, closed_nf, value, boundary) <- assumes (flip Bound 0 <$> indices) VI \indices -> do
t <- check return VTypeω
t <- check return retk
ty_nf <- eval t
let
(args, ret') = splitPi ty_nf
@ -566,17 +561,17 @@ checkStatement (P.Data name tele retk constrs) k =
unify ret' ret
faces <- envArgs args $ for faces \(f, t) -> do
phi <- checkFormula f
(phi, _) <- checkFormula f
t <- check t ret
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)
unify (foldr ior VI0 (map fst faces)) (totalProp indices)
unify (foldl ior VI0 (map fst faces)) (totalProp indices)
`withNote` pretty "The formula determining the endpoints of a higher constructor must be a classical tautology"
pure (ConName name 0 (length n') (length args + length indices), closed_nf, makePCon closed_nf mempty n' args indices system, Boundary indices system)
defineInternal con closed_nf value \name -> addBoundary name boundary $ checkCons n ret xs k
defineInternal con closed_nf value \name -> addBoundary name boundary $ checkCons retk n ret xs k
close [] t = t
close ((x, _, y):xs) t = Pi P.Im x (quote y) (close xs t)
@ -593,13 +588,13 @@ 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:zs) sys con = VLam P.Ex $ Closure nm \a -> makePCon cty (sp Seq.:|> PApp P.Ex a) [] [] zs (sys @@ a) con
totalProp (x:xs) = ior (inot (VVar x)) (VVar x) `ior` totalProp xs
totalProp (x:xs) = ior (VVar x) (inot (VVar x) `ior` totalProp xs)
totalProp [] = VI0
evalFix :: Name -> NFType -> Term -> ElabM Value
evalFix name nft term = do
env <- ask
pure . fix $ \val -> eval' env{ getEnv = Map.insert name (nft, val) (getEnv env) } term
fibrant VTypeω = throwElab PathConPretype
fibrant VType = pure ()
fibrant x = error $ "not a constructor kind: " ++ show x
checkProgram :: [P.Statement] -> ElabM a -> ElabM a
checkProgram [] k = k
@ -608,7 +603,7 @@ checkProgram (st:sts) k = checkStatement st $ checkProgram sts k
newtype Redefinition = Redefinition { getRedefName :: Name }
deriving (Show, Typeable, Exception)
data WhenCheckingEndpoint = WhenCheckingEndpoint { leftEndp :: Value, rightEndp :: Value, whichIsWrong :: NFEndp, exc :: SomeException }
data WhenCheckingEndpoint = WhenCheckingEndpoint { direction :: Name, leftEndp :: Value, rightEndp :: Value, whichIsWrong :: NFEndp, exc :: SomeException }
deriving (Show, Typeable, Exception)
data UnsaturatedCon = UnsaturatedCon { theConstr :: Name }
@ -618,3 +613,10 @@ data UnsaturatedCon = UnsaturatedCon { theConstr :: Name }
data NotACon = NotACon { theNotConstr :: Name }
deriving (Show, Typeable)
deriving anyclass (Exception)
data PathConPretype = PathConPretype
deriving (Show, Typeable)
deriving anyclass (Exception)
newtype DeclaredUndefined = DeclaredUndefined { declaredUndefName :: Name }
deriving (Eq, Show, Exception)

+ 319
- 193
src/Elab/Eval.hs View File

@ -13,7 +13,9 @@ import qualified Data.Map.Strict as Map
import qualified Data.Sequence as Seq
import qualified Data.Set as Set
import qualified Data.Text as T
import Data.Map.Strict (Map)
import Data.Sequence (Seq)
import Data.List (sortOn)
import Data.Traversable
import Data.Set (Set)
import Data.Typeable
@ -21,28 +23,25 @@ import Data.Foldable
import Data.IORef
import Data.Maybe
import Elab.Eval.Formula
import {>n class="err">-# SOURCE #-} Elab.Eval.Formula
import Elab.Monad
import GHC.Stack
import Presyntax.Presyntax (Plicity(..))
import Prettyprinter
import Syntax.Pretty
import Syntax
import System.IO.Unsafe
import System.IO.Unsafe ( unsafePerformIO )
import {-# SOURCE #-} Elab.WiredIn
import Data.List (sortOn)
import Data.Map.Strict (Map)
import Debug (traceM, traceDocM)
import Prettyprinter (pretty, (<+>))
eval :: Term -> ElabM Value
eval :: HasCallStack => Term -> ElabM Value
eval t = asks (flip eval' t)
-- everywhere force
zonkIO :: Value -> IO Value
zonkIO (VNe hd sp) = do
sp' <- traverse zonkSp sp
@ -64,7 +63,6 @@ zonkIO (VPair a b) = VPair <$> zonkIO a <*> zonkIO b
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
-- Sorts
zonkIO VType = pure VType
zonkIO VTypeω = pure VTypeω
@ -76,37 +74,37 @@ zonkIO (VIAnd x y) = iand <$> zonkIO x <*> zonkIO y
zonkIO (VIOr x y) = ior <$> zonkIO x <*> zonkIO y
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 (VPartialP x y) = VPartialP <$> zonkIO x <*> zonkIO y
zonkIO (VSystem fs) = do
t <- for (Map.toList fs) $ \(a, b) -> (,) <$> zonkIO a <*> zonkIO b
pure (mkVSystem (Map.fromList t))
zonkIO (VSub a b c) = VSub <$> zonkIO a <*> zonkIO b <*> zonkIO c
zonkIO (VInc a b c) = VInc <$> zonkIO a <*> zonkIO b <*> zonkIO c
zonkIO (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 (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 (VGlueTy a phi ty e) = glueType <$> zonkIO a <*> zonkIO phi <*> zonkIO ty <*> zonkIO e
zonkIO (VGlue a phi ty e t x) = glueElem <$> zonkIO a <*> zonkIO phi <*> zonkIO ty <*> zonkIO e <*> zonkIO t <*> zonkIO x
zonkIO (VUnglue a phi ty e x) = unglue <$> zonkIO a <*> zonkIO phi <*> zonkIO ty <*> zonkIO e <*> zonkIO x
zonkIO (VCase env t x xs) = do
env' <- emptyEnv
evalCase env'{getEnv = env} . (@@) <$> zonkIO t <*> zonkIO x <*> pure xs
zonkIO (VCase env t x xs) = pure $ VCase env t x xs
zonkIO (VEqStrict a x y) = VEqStrict <$> zonkIO a <*> zonkIO x <*> zonkIO y
zonkIO (VReflStrict a x) = VReflStrict <$> zonkIO a <*> zonkIO x
zonkSp :: Projection -> IO Projection
zonkSp (PApp p x) = PApp p <$> zonkIO x
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 (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 PProj2 = pure PProj2
zonk :: Value -> Value
zonk = unsafePerformIO . zonkIO
eval' :: ElabEnv -> Term -> Value
eval' :: HasCallStack => ElabEnv -> Term -> Value
eval' env (Ref x) =
case Map.lookup x (getEnv env) of
Just (_, vl) -> vl
@ -122,23 +120,22 @@ eval' env (PCon sys x) =
Just (ty, _) -> VNe (HPCon (eval' env sys) ty x) mempty
Nothing -> error $ "constructor " ++ show x ++ " has no type in scope"
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 (Lam p s t) =
VLam p $ Closure s $ \a ->
eval' env { getEnv = Map.insert s (error "type of abs", a) (getEnv env) } t
eval' env { getEnv = Map.insert s (idkT, a) (getEnv env) } t
eval' env (Pi p s d t) =
VPi p (eval' env d) $ Closure s $ \a ->
eval' env { getEnv = (Map.insert s (error "type of abs", a) (getEnv env))} t
eval' env { getEnv = (Map.insert s (idkT, a) (getEnv env))} t
eval' _ (Meta m) = VNe (HMeta m) mempty
eval' env (Sigma s d t) =
VSigma (eval' env d) $ Closure s $ \a ->
eval' env { getEnv = Map.insert s (error "type of abs", a) (getEnv env) } t
eval' env { getEnv = Map.insert s (idkT, a) (getEnv env) } t
eval' e (Pair a b) = VPair (eval' e a) (eval' e b)
@ -159,15 +156,12 @@ 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 (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 (PartialP x y) = VPartialP (eval' e x) (eval' e y)
eval' e (System fs) = VSystem (Map.fromList $ map (\(x, y) -> (eval' e x, eval' e y)) $ Map.toList $ fs)
eval' e (System fs) = mkVSystem (Map.fromList $ map (\(x, y) -> (eval' e x, eval' e y)) $ Map.toList $ fs)
eval' e (Sub a phi u) = VSub (eval' e a) (eval' e phi) (eval' e u)
eval' e (Inc a phi u) = VInc (eval' e a) (eval' e phi) (eval' e u)
eval' e (Inc a phi u) = incS (eval' e a) (eval' e phi) (eval' e u)
eval' e (Ouc a phi u x) = outS (eval' e a) (eval' e phi) (eval' e u) (eval' e x)
eval' e (Comp a phi u a0) = comp (eval' e a) (eval' e phi) (eval' e u) (eval' e a0)
@ -177,73 +171,131 @@ eval' e (GlueTy a phi tys f) = glueType (eval' e a) (eval' e phi) (eval' e tys)
eval' e (Glue a phi tys eqvs t x) = glueElem (eval' e a) (eval' e phi) (eval' e tys) (eval' e eqvs) (eval' e t) (eval' e x)
eval' e (Unglue a phi tys f x) = unglue (eval' e a) (eval' e phi) (eval' e tys) (eval' e f) (eval' e x)
eval' e (Let ns x) =
let env' = foldl (\newe (n, ty, x) -> newe { getEnv = Map.insert n (eval' newe ty, eval' newe x) (getEnv newe) }) e ns
let env' = foldl (\newe (n, ty, x) ->
let nft = eval' newe ty
in newe { getEnv = Map.insert n (nft, evalFix' newe n nft x) (getEnv newe) })
e
ns
in eval' env' x
eval' e (Case range sc xs) = evalCase e (eval' e range @@) (force (eval' e sc)) xs
evalCase :: ElabEnv -> (Value -> Value) -> Value -> [(Term, Term)] -> Value
evalCase _ _ sc [] = error $ "unmatched pattern for value: " ++ show (prettyTm (quote sc))
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 env rng sc [] = VCase (getEnv env) (fun rng) sc []
evalCase env rng (VSystem fs) cases = VSystem (fmap (flip (evalCase env rng) cases) fs)
evalCase env rng (VHComp a phi u a0) cases =
comp (fun \i -> rng (v i)) phi (system \i is1 -> evalCase env rng (u @@ i @@ is1) cases)
(VInc (rng a) phi (evalCase env rng (outS a0 phi (u @@ VI0) a0) cases))
evalCase env rng (VHComp a φ u u0) cases =
comp (fun \i -> rng (v i))
φ
(system \i is1 -> α (u @@ i @@ is1))
(VInc (rng a) φ (α (outS a φ (u @@ VI0) u0)))
where
v = Elab.WiredIn.fill a phi u a0
v = Elab.WiredIn.fill (fun (const a)) φ u u0
α x = evalCase env rng x cases
evalCase env _ sc ((Ref _, k):_) = eval' env k @@ sc
evalCase env _ sc ((Ref _, _, k):_) = eval' env k @@ sc
evalCase env rng (val@(VNe (HCon _ x) sp)) ((Con x', k):xs)
evalCase env rng (force -> val@(VNe (HCon _ x) sp)) ((Con x', _, k):xs)
| x == x' = foldl applProj (eval' env k) sp
| otherwise = evalCase env rng val xs
evalCase env rng (val@(VNe (HPCon _ _ x) sp)) ((Con x', k):xs)
evalCase env rng (force -> val@(VNe (HPCon _ _ x) sp)) ((Con x', _, k):xs)
| x == x' = foldl applProj (eval' env k) sp
| otherwise = evalCase env rng val xs
evalCase _ _ (VVar ((== trueCaseSentinel) -> True)) _ = VI1
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 :: HasCallStack => Name -> NFType -> Term -> ElabM Value
evalFix name nft term = do
t <- ask
pure (evalFix' t name (GluedVl (HVar name) mempty nft) term)
data NotEqual = NotEqual Value Value
deriving (Show, Typeable, Exception)
unify' :: HasCallStack => Value -> Value -> ElabM ()
unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
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
go (VNe (HMeta mv) sp) rhs = solveMeta mv sp rhs
go rhs (VNe (HMeta mv) sp) = solveMeta mv sp rhs
go (VNe (HPCon s _ _) _) rhs
| VSystem _ <- s = go (force s) 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 lhs (VNe (HPCon s _ _) _)
| VSystem _ <- s = go lhs (force s)
go (VNe (HPCon s _ _) _) rhs | Just v <- trivialSystem s = go v rhs
go lhs (VNe (HPCon s _ _) _) | Just v <- trivialSystem s = go lhs v
go (VCase e _ _ 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 (VNe x a) (VNe x' a')
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')
| x == x', length a == length a' =
traverse_ (uncurry unify'Spine) (Seq.zip a a')
traverse_ (uncurry (unify'Spine canSwitch topa topb)) (Seq.zip a a')
go (VLam p (Closure n k)) vl = do
t <- VVar <$> newName' n
unify' (k t) (vApp p vl t)
unify' canSwitch (k t) (vApp p vl t)
go vl (VLam p (Closure n k)) = do
t <- VVar <$> newName' n
unify' (vApp p vl t) (k t)
unify' canSwitch (vApp p vl t) (k t)
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 (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 (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 (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 (VSigma d (Closure _ k)) (VSigma d' (Closure _ k')) = 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 VType VType = pure ()
go VTypeω VTypeω = pure ()
@ -251,56 +303,63 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
go VI VI = pure ()
go (VPath l x y) (VPath l' x' y') = do
unify' l l'
unify' x x'
unify' y y'
unify' canSwitch l l'
unify' canSwitch x x'
unify' canSwitch y y'
go (VLine l x y p) p' = do
n <- VVar <$> newName
unify' (p @@ n) (ielim l x y p' n)
n <- VVar <$> newName' (Bound (T.singleton 'i') (- 1))
unify' canSwitch (p @@ n) (ielim l x y p' n)
go p' (VLine l x y p) = do
n <- VVar <$> newName
unify' (ielim l x y p' n) (p @@ n)
go (VIsOne x) (VIsOne y) = unify' x y
unify' canSwitch (ielim l x y p' n) (p @@ n)
-- IsOne is proof-irrelevant:
go VItIsOne _ = pure ()
go _ VItIsOne = pure ()
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 (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 (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')]
go (VComp a phi u a0) (VComp a' phi' u' a0') =
traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
traverse_ (uncurry (unify' canSwitch)) [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
go (VHComp a phi u a0) (VHComp a' phi' u' a0') =
traverse_ (uncurry (unify' canSwitch)) [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
go (VGlueTy _ (force -> VI1) u _0) rhs = unify' (u @@ VItIsOne) rhs
go lhs (VGlueTy _ (force -> VI1) u _0) = unify' lhs (u @@ VItIsOne)
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 a phi u a0) (VGlueTy a' phi' u' a0') =
traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
traverse_ (uncurry (unify' canSwitch)) [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
go (VGlue a phi u a0 t x) (VGlue a' phi' u' a0' t' x') =
traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0'), (t, t'), (x, 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 ()
go (VSystem sys) rhs = goSystem unify' sys rhs
go rhs (VSystem sys) = goSystem (flip unify') sys rhs
go (VINot x) (VINot y) = unify' canSwitch x y
go (VCase _ _ a b) (VCase _ _ a' b') = do
unify' a a'
let go a b = join $ unify' <$> eval (snd a) <*> eval (snd b)
zipWithM_ go (sortOn fst b) (sortOn fst b')
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 x y
| x == y = pure ()
| otherwise =
case (toDnf x, toDnf y) of
(Just xs, Just ys) -> unify'Formula xs ys
_ -> fail
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
goSystem :: (Value -> Value -> ElabM ()) -> Map.Map Value Value -> Value -> ElabM ()
goSystem k sys rhs = do
@ -308,29 +367,58 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
env <- ask
for_ (Map.toList sys) $ \(f, i) -> do
let i_q = quote i
for (truthAssignments f (getEnv env)) $ \e ->
for (truthAssignments f (getEnv env)) $ \e -> do
k (eval' env{getEnv = e} i_q) (eval' env{getEnv = e} rhs_q)
fail = throwElab $ NotEqual topa topb
unify'Formula x y
| compareDNFs x y = pure ()
| otherwise = fail
unify'Spine (PApp a v) (PApp a' v')
| a == a' = unify' v v'
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
unify'Spine PProj1 PProj1 = pure ()
unify'Spine PProj2 PProj2 = pure ()
trivialSystem :: Value -> Maybe Value
trivialSystem = go . force where
go VSystem{} = Nothing
go x = Just x
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 :: Bool -> Value -> Value -> Projection -> Projection -> ElabM ()
unify'Spine cs _ _ (PApp a v) (PApp a' v')
| a == a' = unify' cs v v'
unify'Spine _ _ = fail
unify'Spine _ _ _ PProj1 PProj1 = pure ()
unify'Spine _ _ _ PProj2 PProj2 = pure ()
unify'Formula x y
| compareDNFs x y = pure ()
| otherwise = fail
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 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 :: HasCallStack => Value -> Value -> ElabM ()
unify a b = unify' a b `catchElab` \(_ :: SomeException) -> liftIO $ throwIO (NotEqual a b)
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)
isConvertibleTo :: Value -> Value -> ElabM (Term -> Term)
isConvertibleTo a b = isConvertibleTo (force a) (force b) where
@ -348,26 +436,42 @@ isConvertibleTo a b = isConvertibleTo (force a) (force b) where
wp' <- k (VVar n) `isConvertibleTo` k' (wp_n @@ VVar 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
unify' a b
unify' True a b
pure id
newMeta :: Value -> ElabM Value
newMeta dom = do
newMeta' :: Bool -> Value -> ElabM Value
newMeta' int dom = do
loc <- liftM2 (,) <$> asks currentFile <*> asks currentSpan
n <- newName
c <- liftIO $ newIORef Nothing
let m = MV (getNameText n) c dom (flatten <$> loc)
let m = MV (getNameText n) c dom (flatten <$> loc) int
flatten (x, (y, z)) = (x, y, z)
env <- asks getEnv
t <- for (Map.toList env) $ \(n, _) -> pure $
t <- fmap catMaybes . for (Map.toList env) $ \(n, t) -> pure $
case n of
Bound{} -> Just (PApp Ex (VVar n))
Bound{} -> Just (PApp Ex (VVar n), n, t)
_ -> Nothing
pure (VNe (HMeta m) (Seq.fromList (catMaybes t)))
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
newName :: MonadIO m => m Name
newName = liftIO $ do
@ -384,91 +488,103 @@ _nameCounter = unsafePerformIO $ newIORef 0
{-# NOINLINE _nameCounter #-}
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
when (mvName m == T.pack "2801") do
traceM (VNe (HMeta m) sp)
traceM rhs
env <- ask
names <- tryElab $ checkSpine Set.empty sp
case names of
Right names -> do
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
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 =
liftIO . atomicModifyIORef' (unsolvedMetas env) $ \x -> (, ()) $
case Map.lookup m x of
Just qs -> Map.insert m ((sp, rhs):qs) x
Nothing -> Map.insert m [(sp, rhs)] x
checkScope :: Set Name -> Value -> ElabM ()
checkScope scope (VNe h sp) =
checkScope :: MV -> Set Name -> Value -> ElabM ()
checkScope mv scope (VNe h sp) =
do
case h of
HVar v@Bound{} ->
unless (v `Set.member` scope) . throwElab $
NotInScope v
ScopeCheckingFail v
HVar{} -> pure ()
HCon{} -> pure ()
HPCon{} -> pure ()
HMeta{} -> pure ()
HMeta m' -> when (mv == m') $ throwElab $ CircularSolution mv
HData{} -> pure ()
traverse_ checkProj sp
where
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 (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 PProj1 = pure ()
checkProj PProj2 = pure ()
checkScope scope (GluedVl _ _p vl) = checkScope scope vl
checkScope mv scope (GluedVl _ _p vl) = checkScope mv scope vl
checkScope scope (VLam _ (Closure n k)) =
checkScope (Set.insert n scope) (k (VVar n))
checkScope mv scope (VLam _ (Closure n k)) =
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 (VPi _ 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 scope (VSigma d (Closure n k)) = do
checkScope mv scope d
checkScope mv (Set.insert n scope) (k (VVar n))
checkScope s (VPair a b) = traverse_ (checkScope s) [a, b]
checkScope mv s (VPair a b) = traverse_ (checkScope mv 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 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 (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 (VPath line a b) = traverse_ (checkScope s) [line, a, b]
checkScope s (VLine _ _ _ line) = checkScope s line
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 (VIsOne x) = checkScope s x
checkScope _ VItIsOne = pure ()
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 (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 (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 (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 (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 (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 (VCase _ _ v _) = checkScope mv s v
checkScope s (VCase _ _ v _) = checkScope s v
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]
checkSpine :: Set Name -> Seq Projection -> ElabM [Name]
checkSpine scope (PApp Ex (VVar n@Bound{}) Seq.:<| xs)
@ -477,10 +593,10 @@ checkSpine scope (PApp Ex (VVar [email protected]{}) Seq.:<| xs)
checkSpine _ (p Seq.:<| _) = throwElab $ SpineProj p
checkSpine _ Seq.Empty = pure []
newtype NonLinearSpine = NonLinearSpine { getDupeName :: Name }
deriving (Show, Typeable, Exception)
newtype SpineProjection = SpineProj { getSpineProjection :: Projection }
data MetaException = NonLinearSpine { getDupeName :: Name }
| SpineProj { getSpineProjection :: Projection }
| CircularSolution { getCycle :: MV }
| ScopeCheckingFail { outOfScope :: Name }
deriving (Show, Typeable, Exception)
substituteIO :: Map.Map Name Value -> Value -> IO Value
@ -488,15 +604,10 @@ substituteIO sub = substituteIO . force where
substituteIO (VNe hd sp) = do
sp' <- traverse (substituteSp sub) sp
case hd of
HMeta (mvCell -> cell) -> do
solved <- liftIO $ readIORef cell
case solved of
Just vl -> substituteIO $ foldl applProj vl sp'
Nothing -> pure $ VNe hd sp'
HVar v ->
case Map.lookup v sub of
Just vl -> substituteIO $ foldl applProj vl sp'
Nothing -> pure $ VNe hd sp'
Nothing -> pure $ foldl applProj (VNe hd mempty) sp'
hd -> pure $ VNe hd sp'
substituteIO (GluedVl h sp vl) = GluedVl h <$> traverse (substituteSp sub) sp <*> substituteIO vl
@ -509,7 +620,6 @@ substituteIO sub = substituteIO . force where
substituteIO (VPath line x y) = VPath <$> substituteIO line <*> substituteIO x <*> substituteIO y
substituteIO (VLine line x y f) = VLine <$> substituteIO line <*> substituteIO x <*> substituteIO y <*> substituteIO f
-- Sorts
substituteIO VType = pure VType
substituteIO VTypeω = pure VTypeω
@ -521,16 +631,13 @@ substituteIO sub = substituteIO . force where
substituteIO (VIOr x y) = ior <$> substituteIO x <*> substituteIO y
substituteIO (VINot x) = inot <$> substituteIO x
substituteIO (VIsOne x) = VIsOne <$> substituteIO x
substituteIO VItIsOne = pure VItIsOne
substituteIO (VPartial x y) = VPartial <$> substituteIO x <*> substituteIO y
substituteIO (VPartialP x y) = VPartialP <$> substituteIO x <*> substituteIO y
substituteIO (VSystem fs) = do
t <- for (Map.toList fs) $ \(a, b) -> (,) <$> substituteIO a <*> substituteIO b
pure (mkVSystem (Map.fromList t))
substituteIO (VSub a b c) = VSub <$> substituteIO a <*> substituteIO b <*> substituteIO c
substituteIO (VInc a b c) = VInc <$> substituteIO a <*> substituteIO b <*> substituteIO c
substituteIO (VInc a b c) = incS <$> substituteIO a <*> substituteIO b <*> substituteIO c
substituteIO (VComp a b c d) = comp <$> substituteIO a <*> substituteIO b <*> substituteIO c <*> substituteIO d
substituteIO (VHComp a b c d) = hComp <$> substituteIO a <*> substituteIO b <*> substituteIO c <*> substituteIO d
@ -538,6 +645,8 @@ substituteIO sub = substituteIO . force where
substituteIO (VGlue a phi ty e t x) = glueElem <$> substituteIO a <*> substituteIO phi <*> substituteIO ty <*> substituteIO e <*> substituteIO t <*> substituteIO x
substituteIO (VUnglue a phi ty e x) = unglue <$> substituteIO a <*> substituteIO phi <*> substituteIO ty <*> substituteIO e <*> substituteIO x
substituteIO (VCase env t x xs) = VCase env <$> substituteIO t <*> substituteIO x <*> pure xs
substituteIO (VEqStrict a x y) = VEqStrict <$> substituteIO a <*> substituteIO x <*> substituteIO y
substituteIO (VReflStrict a x) = VReflStrict <$> substituteIO a <*> substituteIO x
substitute :: Map Name Value -> Value -> Value
substitute sub = unsafePerformIO . substituteIO sub
@ -545,16 +654,23 @@ substitute sub = unsafePerformIO . substituteIO sub
substituteSp :: Map Name Value -> Projection -> IO Projection
substituteSp sub (PApp p x) = PApp p <$> substituteIO sub x
substituteSp sub (PIElim l x y i) = PIElim <$> substituteIO sub l <*> substituteIO sub x <*> substituteIO sub y <*> substituteIO sub i
substituteSp sub (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 _ PProj1 = pure PProj1
substituteSp _ PProj2 = pure PProj2
mkVSystem :: Map.Map Value Value -> Value
mkVSystem vals =
let map' = Map.fromList (map (\(a, b) -> (force a, b)) (Map.toList vals)) in
case Map.lookup VI1 map' of
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
Just x -> x
Nothing -> VSystem (Map.filterWithKey (\k _ -> k /= VI0) map')
Nothing -> VSystem map'
forceIO :: MonadIO m => Value -> m Value
forceIO mv@(VNe (HMeta (mvCell -> cell)) args) = do
@ -568,29 +684,35 @@ forceIO [email protected](VSystem fs) =
Nothing -> pure vl
forceIO (GluedVl _ _ vl) = forceIO vl
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
env' <- liftIO emptyEnv
evalCase env'{getEnv=env} . (@@) <$> forceIO rng <*> forceIO v <*> pure vs
r <- forceIO rng
evalCase env'{getEnv=env} (r @@) <$> forceIO v <*> pure vs
forceIO x = pure x
applProj :: Value -> Projection -> Value
force :: Value -> Value
force = unsafePerformIO . forceIO
applProj :: HasCallStack => Value -> Projection -> Value
applProj fun (PApp p arg) = vApp p fun arg
applProj fun (PIElim l x y i) = ielim l x y fun i
applProj fun (POuc a phi u) = outS a phi u fun
applProj fun (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 PProj2 = vProj2 fun
force :: Value -> Value
force = unsafePerformIO . forceIO
vApp :: HasCallStack => Plicity -> Value -> Value -> Value
vApp p (VLam p' k) arg
| p == p' = clCont k arg
| otherwise = error $ "wrong plicity " ++ show p ++ " vs " ++ show p' ++ " in app " ++ show (App p (quote (VLam p' k)) (quote arg))
vApp p (VNe h sp) arg = VNe h (sp Seq.:|> PApp p arg)
vApp _ (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 (GluedVl h sp vl) arg = GluedVl h (sp Seq.:|> PApp p arg) (vApp p vl arg)
vApp p (VSystem fs) arg = VSystem (fmap (flip (vApp p) arg) fs)
vApp p (VInc (VPi _ _ (Closure _ r)) phi f) arg = VInc (r (vApp p f arg)) phi (vApp p f arg)
vApp p (VSystem fs) arg = mkVSystem (fmap (flip (vApp p) arg) fs)
vApp p (VCase env rng sc branches) arg =
VCase env (fun \x -> let VPi _ _ (Closure _ r) = rng @@ x in r arg) sc
(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))
(@@) :: HasCallStack => Value -> Value -> Value
@ -602,13 +724,17 @@ vProj1 (VPair a _) = a
vProj1 (VNe h sp) = VNe h (sp Seq.:|> PProj1)
vProj1 (GluedVl h sp vl) = GluedVl h (sp Seq.:|> PProj1) (vProj1 vl)
vProj1 (VSystem fs) = VSystem (fmap vProj1 fs)
vProj1 (VInc (VSigma a _) b c) = VInc a b (vProj1 c)
vProj1 x = error $ "can't proj1 " ++ show (prettyTm (quote x))
vProj1 (VInc (VSigma a _) b c) = incS a b (vProj1 c)
vProj1 (VCase env rng sc branches) =
VCase env rng sc (map (projIntoCase Proj1) branches)
vProj1 x = error $ "can't proj1 " ++ show x
vProj2 :: HasCallStack => Value -> Value
vProj2 (VPair _ b) = b
vProj2 (VNe h sp) = VNe h (sp Seq.:|> PProj2)
vProj2 (GluedVl h sp vl) = GluedVl h (sp Seq.:|> PProj2) (vProj2 vl)
vProj2 (VSystem fs) = VSystem (fmap vProj2 fs)
vProj2 (VInc (VSigma _ (Closure _ r)) b c) = VInc (r (vProj1 c)) b (vProj2 c)
vProj2 x = error $ "can't proj2 " ++ show (prettyTm (quote x))
vProj2 (VInc (VSigma _ (Closure _ r)) b c) = incS (r (vProj1 c)) b (vProj2 c)
vProj2 (VCase env rng sc branches) =
VCase env rng sc (map (projIntoCase Proj2) branches)
vProj2 x = error $ "can't proj2 " ++ show (prettyTm (quote x))

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

@ -2,22 +2,38 @@ module Elab.Eval.Formula where
import qualified Data.Map.Strict as Map
import qualified Data.Sequence as Seq
import qualified Data.Set as Set
import Data.Map.Strict (Map)
import Data.Set (Set)
import Syntax
import {-# SOURCE #-} Elab.WiredIn (inot, ior, iand)
import Elab.Eval (substitute, trueCaseSentinel)
toDnf :: Value -> Maybe Value
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
<