|
{-# LANGUAGE LambdaCase #-}
|
|
{-# LANGUAGE BlockArguments #-}
|
|
{-# LANGUAGE TupleSections #-}
|
|
{-# LANGUAGE DeriveAnyClass #-}
|
|
{-# LANGUAGE ScopedTypeVariables #-}
|
|
{-# LANGUAGE DerivingStrategies #-}
|
|
module Elab where
|
|
|
|
import Control.Arrow (Arrow(first))
|
|
import Control.Monad.Reader
|
|
import Control.Exception
|
|
|
|
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.Traversable
|
|
import Data.Text (Text)
|
|
import Data.Map (Map)
|
|
import Data.Typeable
|
|
import Data.Foldable
|
|
|
|
import Elab.Eval.Formula (possible, truthAssignments)
|
|
import Elab.WiredIn
|
|
import Elab.Monad
|
|
import Elab.Eval
|
|
|
|
import qualified Presyntax.Presyntax as P
|
|
|
|
import Prettyprinter
|
|
|
|
import Syntax.Pretty
|
|
import Syntax
|
|
import Data.Maybe (fromMaybe)
|
|
|
|
infer :: P.Expr -> ElabM (Term, NFType)
|
|
infer (P.Span ex a b) = withSpan a b $ infer ex
|
|
|
|
infer (P.Var t) = do
|
|
name <- getNameFor t
|
|
nft <- getNfType name
|
|
pure (Ref name, nft)
|
|
|
|
infer (P.App p f x) = do
|
|
(f, f_ty) <- infer f
|
|
porp <- isPiType p f_ty
|
|
case porp of
|
|
It'sProd d r w -> do
|
|
x <- check x d
|
|
x_nf <- eval x
|
|
pure (App p (w f) x, r x_nf)
|
|
It'sPath li le ri wp -> do
|
|
x <- check x VI
|
|
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)
|
|
pure (App P.Ex (w f) x, a)
|
|
It'sPartialP phi a w -> do
|
|
x <- check x (VIsOne phi)
|
|
x_nf <- eval x
|
|
pure (App P.Ex (w f) x, a @@ x_nf)
|
|
|
|
infer (P.Proj1 x) = do
|
|
(tm, ty) <- infer x
|
|
(d, _, wp) <- isSigmaType ty
|
|
pure (Proj1 (wp tm), d)
|
|
|
|
infer (P.Proj2 x) = do
|
|
(tm, ty) <- infer x
|
|
tm_nf <- eval tm
|
|
(_, r, wp) <- isSigmaType ty
|
|
pure (Proj2 (wp tm), r (vProj1 tm_nf))
|
|
|
|
infer exp = do
|
|
t <- newMeta VType
|
|
tm <- switch $ check exp t
|
|
pure (tm, t)
|
|
|
|
check :: P.Expr -> NFType -> ElabM Term
|
|
check (P.Span ex a b) ty = withSpan a b $ check ex ty
|
|
|
|
check (P.Lam p var body) (VPi p' dom (Closure _ rng)) | p == p' =
|
|
assume (Bound var 0) dom $ \name ->
|
|
Lam p name <$> check body (rng (VVar name))
|
|
|
|
check tm (VPi P.Im dom (Closure var rng)) =
|
|
assume var dom $ \name ->
|
|
Lam P.Im name <$> check tm (rng (VVar name))
|
|
|
|
check (P.Lam p v b) ty = do
|
|
porp <- isPiType p =<< forceIO ty
|
|
case porp of
|
|
It'sProd d r wp ->
|
|
assume (Bound v 0) d $ \name ->
|
|
wp . Lam p name <$> check b (r (VVar name))
|
|
|
|
It'sPath li le ri wp -> do
|
|
tm <- assume (Bound v 0) VI $ \var ->
|
|
Lam P.Ex var <$> check b (force (li (VVar var)))
|
|
|
|
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)
|
|
|
|
pure (wp (PathIntro (quote (fun li)) (quote le) (quote ri) tm))
|
|
|
|
It'sPartial phi a wp ->
|
|
assume (Bound v 0) (VIsOne phi) $ \var ->
|
|
wp . Lam p var <$> check b a
|
|
|
|
It'sPartialP phi a wp ->
|
|
assume (Bound v 0) (VIsOne phi) $ \var ->
|
|
wp . Lam p var <$> check b (a @@ VVar var)
|
|
|
|
check (P.Pair a b) ty = do
|
|
(d, r, wp) <- isSigmaType =<< forceIO ty
|
|
a <- check a d
|
|
a_nf <- eval a
|
|
b <- check b (r a_nf)
|
|
pure (wp (Pair a b))
|
|
|
|
check (P.Pi p s d r) ty = do
|
|
isSort ty
|
|
d <- check d ty
|
|
d_nf <- eval d
|
|
assume (Bound s 0) d_nf \var -> do
|
|
r <- check r ty
|
|
pure (Pi p var d r)
|
|
|
|
check (P.Sigma s d r) ty = do
|
|
isSort ty
|
|
d <- check d ty
|
|
d_nf <- eval d
|
|
assume (Bound s 0) d_nf \var -> do
|
|
r <- check r ty
|
|
pure (Sigma var d r)
|
|
|
|
check (P.Let items body) ty = do
|
|
checkLetItems mempty items \decs -> do
|
|
body <- check body ty
|
|
pure (Let decs body)
|
|
|
|
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)
|
|
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
|
|
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'
|
|
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'
|
|
]
|
|
`withNote` (pretty "Consider this face, where both are true:" <+> showFace (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))))
|
|
|
|
check (P.LamCase pats) ty =
|
|
do
|
|
porp <- isPiType P.Ex ty
|
|
case porp of
|
|
It'sProd dom rng wp -> do
|
|
name <- newName
|
|
let range = Lam P.Ex name (quote (rng (VVar name)))
|
|
|
|
cases <- checkPatterns range [] pats \partialPats (pat, rhs) -> 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
|
|
-- compute what the case expression computed so far does
|
|
-- with all the faces
|
|
|
|
-- and make sure that the current case agrees with that
|
|
-- boundary
|
|
Just boundary -> do
|
|
rhs_nf <- eval (wp rhs)
|
|
cases <- partialPats
|
|
|
|
let
|
|
(ty, a, b) = case pat_nf of
|
|
VNe (HCon ty (ConName _ _ a b)) _ -> (ty, a, b)
|
|
VNe (HPCon _ ty (ConName _ _ a b)) _ -> (ty, a, b)
|
|
_ -> undefined
|
|
dummies <- replicateM ((a + b) - length (getBoundaryNames boundary)) newName
|
|
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 (lookup n)) base (getBoundaryNames boundary)
|
|
lookup n = fromMaybe VI0 (snd <$> (Map.lookup n i))
|
|
unify vl rhs
|
|
`withNote` vcat [ pretty "These must be the same because of the face"
|
|
, indent 2 $ prettyTm (quote formula) <+> operator (pretty "=>") <+> prettyTm (quote (zonk side))
|
|
]
|
|
`withNote` (pretty "Mandated by the constructor" <+> prettyTm (quote pat_nf))
|
|
_ -> pure ()
|
|
|
|
pure (pat, n_lams, wp rhs)
|
|
let x = wp (Lam P.Ex name (Case range (Ref name) cases))
|
|
pure x
|
|
_ -> do
|
|
dom <- newMeta VTypeω
|
|
n <- newName' (Bound (T.singleton 'x') 0)
|
|
assume n dom \_ -> do
|
|
rng <- newMeta VTypeω
|
|
throwElab $ NotEqual (VPi P.Ex dom (Closure n (const rng))) ty
|
|
where
|
|
checkPatterns _ acc [] _ = pure (reverse acc)
|
|
checkPatterns rng acc (x:xs) k = do
|
|
n <- newName
|
|
(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))
|
|
|
|
boundaryFormulas [] (VSystem fs) = fs
|
|
boundaryFormulas (x:xs) k = boundaryFormulas xs $ k @@ VVar x
|
|
boundaryFormulas a b = error (show (a, b))
|
|
|
|
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 -> Int -> Value -> ElabM a) -> ElabM a
|
|
checkPattern (P.PCap var) dom cont = do
|
|
name <- asks (Map.lookup var . nameMap)
|
|
case name of
|
|
Just name@(ConName _ _ skip arity) -> do
|
|
unless (arity == 0) $ throwElab $ UnsaturatedCon name
|
|
(ty, wp, _) <- instantiate =<< getNfType name
|
|
unify ty dom
|
|
wrap <- skipLams skip
|
|
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 0 (VVar name)
|
|
|
|
checkPattern (P.PCon var args) dom cont =
|
|
do
|
|
name <- asks (Map.lookup var . nameMap)
|
|
case name of
|
|
Just name@(ConName _ _ nskip arity) -> do
|
|
unless (arity == length args) $ throwElab $ UnsaturatedCon name
|
|
(ty, wp, xs) <- instantiate =<< getNfType name
|
|
_ <- isConvertibleTo (skipBinders arity ty) dom
|
|
|
|
skip <- skipLams nskip
|
|
t <- asks (Map.lookup name . boundaries)
|
|
|
|
con <- quote <$> getValue name
|
|
|
|
bindNames args ty $ \names wrap ->
|
|
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)
|
|
where
|
|
skipBinders :: Int -> NFType -> NFType
|
|
skipBinders 0 t = t
|
|
skipBinders n (VPi _ _ (Closure v r)) = skipBinders (n - 1) (r (VVar v))
|
|
skipBinders _ _ = error $ "constructor type is wrong?"
|
|
|
|
bindNames (n:ns) (VPi p d (Closure _ r)) k =
|
|
assume (Bound n 0) d \n -> bindNames ns (r (VVar n)) \ns w ->
|
|
k (n:ns) (Lam p n . w)
|
|
bindNames [] _ k = k [] id
|
|
bindNames xs t _ = error $ show (xs, t)
|
|
|
|
instBoundary :: [Value] -> Boundary -> Boundary
|
|
instBoundary metas (Boundary x y) = Boundary x (foldl (vApp P.Ex) y metas)
|
|
|
|
instantiate :: NFType -> ElabM (NFType, Term -> Term, [Value])
|
|
instantiate (VPi P.Im d (Closure _ k)) = do
|
|
t <- newMeta d
|
|
(ty, w, xs) <- instantiate (k t)
|
|
pure (ty, \inner -> w (App P.Im inner (quote t)), t:xs)
|
|
instantiate x = pure (x, id, [])
|
|
|
|
skipLams :: Int -> ElabM (Term -> Term)
|
|
skipLams 0 = pure id
|
|
skipLams k = do
|
|
n <- newName
|
|
(Lam P.Im n . ) <$> skipLams (k - 1)
|
|
|
|
checkLetItems :: Map Text (Maybe (Name, NFType)) -> [P.LetItem] -> ([(Name, Term, Term)] -> ElabM a) -> ElabM a
|
|
checkLetItems _ [] cont = cont []
|
|
checkLetItems map (P.LetDecl v t:xs) cont = do
|
|
t <- check t VTypeω
|
|
t_nf <- eval t
|
|
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
|
|
Nothing -> do
|
|
(tm, ty) <- infer rhs
|
|
tm_nf <- eval tm
|
|
makeLetDef (Defined name 0) ty tm_nf \name' ->
|
|
checkLetItems map xs \xs ->
|
|
cont ((name', quote ty, tm):xs)
|
|
Just Nothing -> throwElab $ Redefinition (Defined name 0)
|
|
Just (Just (name, ty_nf)) -> do
|
|
rhs <- check rhs ty_nf
|
|
rhs_nf <- eval rhs
|
|
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
|
|
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
|
|
nm <- getNameFor x
|
|
ty <- getNfType nm
|
|
unify ty VI
|
|
pure (inot (VVar nm))
|
|
checkFormula (P.FIs1 x) = do
|
|
nm <- getNameFor x
|
|
ty <- getNfType nm
|
|
unify ty VI
|
|
pure (VVar nm)
|
|
|
|
isSort :: NFType -> ElabM ()
|
|
isSort t = isSort (force t) where
|
|
isSort VType = pure ()
|
|
isSort VTypeω = pure ()
|
|
isSort vt@(VNe HMeta{} _) = unify vt VType
|
|
isSort vt = throwElab $ NotEqual vt VType
|
|
|
|
data ProdOrPath
|
|
= It'sProd { prodDmn :: NFType
|
|
, prodRng :: NFType -> NFType
|
|
, prodWrap :: Term -> Term
|
|
}
|
|
| It'sPath { pathLine :: NFType -> NFType
|
|
, pathLeft :: Value
|
|
, pathRight :: Value
|
|
, pathWrap :: Term -> Term
|
|
}
|
|
| It'sPartial { partialExtent :: NFEndp
|
|
, partialDomain :: Value
|
|
, partialWrap :: Term -> Term
|
|
}
|
|
| It'sPartialP { partialExtent :: NFEndp
|
|
, partialDomain :: Value
|
|
, partialWrap :: Term -> Term
|
|
}
|
|
|
|
isPiType :: P.Plicity -> NFType -> ElabM ProdOrPath
|
|
isPiType p x = isPiType p (force x) where
|
|
isPiType p (VPi p' d (Closure _ k)) | p == p' = pure (It'sProd d k id)
|
|
isPiType P.Ex (VPath li le ri) = pure (It'sPath (li @@) le ri id)
|
|
isPiType P.Ex (VPartial phi a) = pure (It'sPartial phi a id)
|
|
isPiType P.Ex (VPartialP phi a) = pure (It'sPartialP phi a id)
|
|
|
|
isPiType P.Ex (VPi P.Im d (Closure _ k)) = do
|
|
meta <- newMeta d
|
|
porp <- isPiType P.Ex (k meta)
|
|
pure $ case porp of
|
|
It'sProd d r w -> It'sProd d r (\f -> w (App P.Im f (quote meta)))
|
|
It'sPath l x y w -> It'sPath l x y (\f -> w (App P.Im f (quote meta)))
|
|
It'sPartial phi a w -> It'sPartial phi a (\f -> w (App P.Im f (quote meta)))
|
|
It'sPartialP phi a w -> It'sPartialP phi a (\f -> w (App P.Im f (quote meta)))
|
|
isPiType p t = do
|
|
dom <- newMeta VType
|
|
name <- newName
|
|
assume name dom $ \name -> do
|
|
rng <- newMeta VType
|
|
wp <- isConvertibleTo t (VPi p dom (Closure name (const rng)))
|
|
pure (It'sProd dom (const rng) wp)
|
|
|
|
isSigmaType :: NFType -> ElabM (Value, NFType -> NFType, Term -> Term)
|
|
isSigmaType t = isSigmaType (force t) where
|
|
isSigmaType (VSigma d (Closure _ k)) = pure (d, k, id)
|
|
isSigmaType t = do
|
|
dom <- newMeta VType
|
|
name <- newName
|
|
assume name dom $ \name -> do
|
|
rng <- newMeta VType
|
|
wp <- isConvertibleTo t (VSigma dom (Closure name (const rng)))
|
|
pure (dom, const rng, wp)
|
|
|
|
isPartialType :: NFType -> ElabM (NFEndp, Value)
|
|
isPartialType t = isPartialType (force t) where
|
|
isPartialType (VPartial phi a) = pure (phi, 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)
|
|
|
|
checkStatement :: P.Statement -> ElabM a -> ElabM a
|
|
checkStatement (P.SpanSt s a b) k = withSpan a b $ checkStatement s k
|
|
|
|
checkStatement (P.Decl name ty) k = do
|
|
ty <- check ty VTypeω
|
|
ty_nf <- eval ty
|
|
assumes (flip Defined 0 <$> name) ty_nf (const k)
|
|
|
|
checkStatement (P.Postulate []) k = k
|
|
checkStatement (P.Postulate ((name, ty):xs)) k = do
|
|
ty <- check ty VTypeω
|
|
ty_nf <- eval ty
|
|
assume (Defined name 0) ty_nf \name ->
|
|
local (\e -> e { definedNames = Set.insert name (definedNames e) }) (checkStatement (P.Postulate xs) k)
|
|
|
|
checkStatement (P.Defn name rhs) k = do
|
|
ty <- asks (Map.lookup name . nameMap)
|
|
case ty of
|
|
Nothing -> do
|
|
(tm, ty) <- infer rhs
|
|
tm_nf <- eval tm
|
|
makeLetDef (Defined name 0) ty tm_nf (const k)
|
|
Just nm -> do
|
|
ty_nf <- getNfType nm
|
|
t <- asks (Set.member nm . definedNames)
|
|
when t $ throwElab (Redefinition (Defined name 0))
|
|
|
|
rhs <- check rhs ty_nf
|
|
rhs_nf <- evalFix (Defined name 0) ty_nf rhs
|
|
makeLetDef (Defined name 0) ty_nf rhs_nf $ \name ->
|
|
local (\e -> e { definedNames = Set.insert name (definedNames e) }) k
|
|
|
|
checkStatement (P.Builtin winame var) k = do
|
|
wi <-
|
|
case Map.lookup winame wiredInNames of
|
|
Just wi -> pure wi
|
|
_ -> throwElab $ NoSuchPrimitive winame
|
|
|
|
let
|
|
check = do
|
|
nm <- getNameFor var
|
|
ty <- getNfType nm
|
|
unify ty (wiType wi)
|
|
`withNote` hsep [ pretty "Previous definition of", pretty nm, pretty "here" ]
|
|
`seeAlso` nm
|
|
|
|
env <- ask
|
|
liftIO $
|
|
runElab check env `catch` \(_ :: NotInScope) -> pure ()
|
|
|
|
define (Defined var 0) (wiType wi) (wiValue wi) $ \name ->
|
|
local (\e -> e { definedNames = Set.insert name (definedNames e) }) k
|
|
|
|
checkStatement (P.ReplNf e) k = do
|
|
(e, _) <- infer e
|
|
e_nf <- eval e
|
|
h <- asks commHook
|
|
liftIO (h e_nf)
|
|
k
|
|
|
|
checkStatement (P.ReplTy e) k = do
|
|
(_, ty) <- infer e
|
|
h <- asks commHook
|
|
liftIO (h ty)
|
|
k
|
|
|
|
checkStatement (P.Data name tele retk constrs) k =
|
|
do
|
|
checkTeleRetk True tele 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)
|
|
where
|
|
makeProj (x, p, _) = PApp p (VVar x)
|
|
|
|
markAsDef x e = e { definedNames = Set.insert x (definedNames e) }
|
|
|
|
mkHead name
|
|
| any (\case { (_, _, P.Path{}) -> True; _ -> False}) constrs = HData True name
|
|
| otherwise = HData False name
|
|
|
|
checkTeleRetk allKan [] 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
|
|
(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)
|
|
|
|
checkCons _ _et [] k = k
|
|
|
|
checkCons n ret ((s, e, P.Point x ty):xs) k = withSpan s e $ do
|
|
t <- check ty VTypeω
|
|
ty_nf <- eval t
|
|
let
|
|
(args, ret') = splitPi ty_nf
|
|
closed = close n t
|
|
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
|
|
(con, closed_nf, value, boundary) <- assumes (flip Bound 0 <$> indices) VI \indices -> do
|
|
t <- check return VTypeω
|
|
ty_nf <- eval t
|
|
let
|
|
(args, ret') = splitPi ty_nf
|
|
closed = close n (addArgs args (addInterval indices (quote ret')))
|
|
n' = map (\(x, _, y) -> (x, P.Im, y)) n
|
|
|
|
addArgs = flip $ foldr (\(x, p, t) -> Pi p x (quote t))
|
|
addInterval = flip $ foldr (\n -> Pi P.Ex n I)
|
|
|
|
envArgs ((x, _, y):xs) = assume x y . const . envArgs xs
|
|
envArgs [] = id
|
|
|
|
closed_nf <- eval closed
|
|
unify ret' ret
|
|
|
|
faces <- envArgs args $ for faces \(f, t) -> do
|
|
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)
|
|
`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
|
|
|
|
close [] t = t
|
|
close ((x, _, y):xs) t = Pi P.Im x (quote y) (close xs t)
|
|
|
|
splitPi (VPi p y (Closure x k)) = first ((x, p, y):) $ splitPi (k (VVar x))
|
|
splitPi t = ([], t)
|
|
|
|
makeCon cty sp [] [] con = VNe (HCon cty con) sp
|
|
makeCon cty sp ((nm, p, _):xs) ys con = VLam p $ Closure nm \a -> makeCon cty (sp Seq.:|> PApp p a) xs ys con
|
|
makeCon cty sp [] ((nm, p, _):ys) con = VLam p $ Closure nm \a -> makeCon cty (sp Seq.:|> PApp p a) [] ys con
|
|
|
|
makePCon cty sp [] [] [] sys con = VNe (HPCon sys cty con) sp
|
|
makePCon cty sp ((nm, p, _):xs) ys zs sys con = VLam p $ Closure nm \a -> makePCon cty (sp Seq.:|> PApp p a) xs 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
|
|
|
|
totalProp (x:xs) = ior (inot (VVar x)) (VVar x) `ior` totalProp xs
|
|
totalProp [] = VI0
|
|
|
|
|
|
checkProgram :: [P.Statement] -> ElabM a -> ElabM a
|
|
checkProgram [] k = k
|
|
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 }
|
|
deriving (Show, Typeable, Exception)
|
|
|
|
data UnsaturatedCon = UnsaturatedCon { theConstr :: Name }
|
|
deriving (Show, Typeable)
|
|
deriving anyclass (Exception)
|
|
|
|
data NotACon = NotACon { theNotConstr :: Name }
|
|
deriving (Show, Typeable)
|
|
deriving anyclass (Exception)
|