Browse Source

some fixes to inductive types

feature/hits
Amélia Liao 3 years ago
parent
commit
15cfd9abf1
6 changed files with 92 additions and 42 deletions
  1. +53
    -8
      intro.tt
  2. +23
    -20
      src/Elab.hs
  3. +4
    -5
      src/Elab/Eval.hs
  4. +1
    -1
      src/Elab/WiredIn.hs
  5. +2
    -4
      src/Syntax.hs
  6. +9
    -4
      src/Syntax/Pretty.hs

+ 53
- 8
intro.tt View File

@ -682,11 +682,56 @@ pathIsHom {A} {B} {f} {g} =
theIso = (happly {A} {B} {f} {g}, happlyIsIso {A} {B} {f} {g})
in univalence (IsoToEquiv theIso)
data List (A : Type) : Type where
nil : List A
cons : A -> List A -> List A
map : {A : Type} {B : Type} -> (A -> B) -> List A -> List B
map f = \case
nil -> nil
cons x xs -> cons (f x) (map f xs)
data Nat : Type where
zero : Nat
succ : Nat -> Nat
data Int : Type where
pos : Nat -> Int
neg : Nat -> Int
sucZ : Int -> Int
sucZ = \case
pos n -> pos (succ n)
neg n ->
let suc_neg : Nat -> Int
suc_neg = \case
zero -> pos zero
succ n -> neg n
in suc_neg n
predZ : Int -> Int
predZ = \case
pos n ->
let pred_pos : Nat -> Int
pred_pos = \case
zero -> neg zero
succ n -> pos n
in pred_pos n
neg n -> neg (succ n)
sucEquiv : isIso sucZ
sucEquiv =
let
sucPredZ : (x : Int) -> Path (sucZ (predZ x)) x
sucPredZ = \case
pos n ->
let k : (n : Nat) -> Path (sucZ (predZ (pos n))) (pos n)
k = \case
zero -> refl
succ n -> refl
in k n
neg n -> refl
predSucZ : (x : Int) -> Path (predZ (sucZ x)) x
predSucZ = \case
pos n -> refl
neg n ->
let k : (n : Nat) -> Path (predZ (sucZ (neg n))) (neg n)
k = \case
zero -> refl
succ n -> refl
in k n
in (predZ, sucPredZ, predSucZ)
intPath : Path Int Int
intPath = univalence (IsoToEquiv (sucZ, sucEquiv))

+ 23
- 20
src/Elab.hs View File

@ -199,13 +199,12 @@ check (P.LamCase pats) ty = do
case porp of
It'sProd dom rng wp -> do
name <- newName
liftIO . print $ show pats
cases <- for pats $ \(pat, rhs) -> do
checkPattern pat dom \pat wp -> do
pat_nf <- eval pat
checkPattern pat dom \pat wp pat_nf -> do
rhs <- check rhs (rng pat_nf)
pure (pat, wp rhs)
pure (wp (Lam P.Ex name (Case (Ref name) cases)))
let x = wp (Lam P.Ex name (Case (Ref name) cases))
pure x
_ -> do
dom <- newMeta VTypeω
n <- newName' (Bound (T.singleton 'x') 0)
@ -218,29 +217,29 @@ check exp ty = do
wp <- isConvertibleTo has ty
pure (wp tm)
checkPattern :: P.Pattern -> NFSort -> (Term -> (Term -> Term) -> ElabM a) -> ElabM a
checkPattern :: P.Pattern -> NFSort -> (Term -> (Term -> Term) -> 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 <- instantiate =<< getNfType name
_ <- isConvertibleTo ty dom
(ty, wp) <- instantiate =<< getNfType name
unify ty dom
wrap <- skipLams skip
cont (Con name) wrap
cont (Con name) wrap =<< eval (wp (Con name))
Just name -> throwElab $ NotACon name
Nothing -> assume (Bound var 0) dom \name -> cont (Ref name) (Lam P.Ex name)
Nothing -> assume (Bound var 0) dom \name -> cont (Ref name) (Lam P.Ex name) (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 <- instantiate =<< getNfType name
(ty, wp) <- instantiate =<< getNfType name
_ <- isConvertibleTo (skipBinders arity ty) dom
skip <- skipLams nskip
bindNames args ty $ \_ wrap ->
cont (Con name) (skip . wrap)
bindNames args ty $ \names wrap ->
cont (Con name) (skip . wrap) =<< eval (foldl (\x y -> App P.Ex x (Ref y)) (wp (Con name)) names)
Just name -> throwElab $ NotACon name
_ -> throwElab $ NotInScope (Bound var 0)
where
@ -255,11 +254,12 @@ checkPattern (P.PCon var args) dom cont =
bindNames [] _ k = k [] id
bindNames xs t _ = error $ show (xs, t)
instantiate :: NFType -> ElabM NFType
instantiate :: NFType -> ElabM (NFType, Term -> Term)
instantiate (VPi P.Im d (Closure _ k)) = do
t <- newMeta d
instantiate (k t)
instantiate x = pure x
(ty, w) <- instantiate (k t)
pure (ty, \inner -> App P.Im (w inner) (quote t))
instantiate x = pure (x, id)
skipLams :: Int -> ElabM (Term -> Term)
skipLams 0 = pure id
@ -445,18 +445,20 @@ checkStatement (P.ReplTy e) k = do
checkStatement (P.Data name tele retk constrs) k =
do
checkTeleRetk True tele retk \kind tele -> do
checkTeleRetk True tele retk \kind tele undef -> do
kind_nf <- eval kind
defineInternal (Bound name 0) kind_nf (\name' -> VNe (HData name') mempty) \name' -> do
checkCons tele (VNe (HData name') (Seq.fromList (map makeProj tele))) constrs k
defineInternal (Defined name 0) kind_nf (\name' -> VNe (HData name') mempty) \name' ->
checkCons tele (VNe (HData 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) }
checkTeleRetk allKan [] retk cont = do
t <- check retk VTypeω
t_nf <- eval t
when allKan $ unify t_nf VType
cont t []
cont t [] id
checkTeleRetk allKan ((x, p, t):xs) retk cont = do
(t, ty) <- infer t
_ <- isConvertibleTo ty VTypeω
@ -465,7 +467,8 @@ checkStatement (P.Data name tele retk constrs) k =
VType -> allKan
_ -> False
t_nf <- eval t
assume (Bound x 0) t_nf $ \nm -> checkTeleRetk allKan' xs retk \k xs -> cont (Pi p nm t k) ((nm, p, t_nf):xs)
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


+ 4
- 5
src/Elab/Eval.hs View File

@ -6,7 +6,6 @@
{-# LANGUAGE TupleSections #-}
module Elab.Eval where
import Control.Arrow (Arrow(second))
import Control.Monad.Reader
import Control.Exception
@ -114,7 +113,7 @@ zonkIO (VComp a b c d) = comp <$> zonkIO a <*> zonkIO b <*> zonkIO c <*> zonkIO
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 x xs) = VCase <$> zonkIO x <*> traverse (\(x, y) -> (x,) <$> zonkIO y) xs
zonkIO (VCase x xs) = VCase <$> zonkIO x <*> pure xs
zonkSp :: Projection -> IO Projection
zonkSp (PApp p x) = PApp p <$> zonkIO x
@ -203,12 +202,12 @@ eval' e (Let ns x) =
eval' e (Case sc xs) = evalCase e (eval' e sc) xs
evalCase :: ElabEnv -> Value -> [(Term, Term)] -> Value
evalCase _ sc [] = error $ "unmatched pattern for value: " ++ show (prettyTm (quote sc))
evalCase _ sc [] = error $ "unmatched pattern for value: " ++ show (prettyTm (quote sc))
evalCase env sc ((Ref _, k):_) = eval' env k @@ sc
evalCase env (force -> val@(VNe (HCon _ x) sp)) ((Con x', k):xs)
| x == x' = foldl applProj (eval' env k) sp
| otherwise = evalCase env val xs
evalCase env sc xs = VCase sc (map (second (eval' env)) xs)
evalCase _ sc xs = VCase sc xs
vApp :: HasCallStack => Plicity -> Value -> Value -> Value
vApp p (VLam p' k) arg
@ -489,7 +488,7 @@ 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 s (VCase v xs) = checkScope s v *> traverse_ (checkScope s . snd) xs
checkScope s (VCase v _) = checkScope s v
checkSpine :: Set Name -> Seq Projection -> ElabM [Name]
checkSpine scope (PApp Ex (VVar n@Bound{}) Seq.:<| xs)


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

@ -195,7 +195,7 @@ ielim line left right fn i =
VNe n sp -> VNe n (sp Seq.:|> PIElim line left right i)
VSystem map -> VSystem (fmap (flip (ielim line left right) i) map)
VInc (VPath _ _ _) _ u -> ielim line left right u i
VCase x xs -> VCase x (fmap (fmap (flip (ielim line left right) i)) xs)
VCase x xs -> VCase x (fmap (fmap (flip (IElim (quote line) (quote left) (quote right)) (quote i))) xs)
_ -> error $ "can't ielim " ++ show (prettyTm (quote fn))
outS :: NFSort -> NFEndp -> Value -> Value -> Value


+ 2
- 4
src/Syntax.hs View File

@ -3,8 +3,6 @@
{-# LANGUAGE DeriveDataTypeable #-}
module Syntax where
import Control.Arrow (Arrow(second))
import qualified Data.Map.Strict as Map
import qualified Data.Sequence as Seq
import qualified Data.Set as Set
@ -175,7 +173,7 @@ data Value
| VGlue NFSort NFEndp NFPartial NFPartial NFPartial Value
| VUnglue NFSort NFEndp NFPartial NFPartial Value
| VCase Value [(Term, Value)]
| VCase Value [(Term, Term)]
deriving (Eq, Show, Ord)
pattern VVar :: Name -> Value
@ -243,7 +241,7 @@ quoteWith names (VGlueTy a phi t e) = GlueTy (quoteWith names a) (quoteWith n
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 names (VCase v xs) = Case (quoteWith names v) (map (second (quoteWith names)) xs)
quoteWith names (VCase v xs) = Case (quoteWith names v) xs
alwaysShort :: Value -> Bool
alwaysShort (VNe HCon{} _) = True


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

@ -39,7 +39,7 @@ prettyTm = prettyTm . everywhere (mkT beautify) where
prettyTm (Proj1 x) = prettyTm x <> operator (pretty ".1")
prettyTm (Proj2 x) = prettyTm x <> operator (pretty ".2")
prettyTm l@(Lam _ _ _) = pretty '\\' <> hsep (map prettyArgList al) <+> pretty "->" <+> prettyTm bod where
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)
@ -73,16 +73,20 @@ prettyTm = prettyTm . everywhere (mkT beautify) where
prettyTm (IOr x y) = parens $ prettyTm x <+> operator (pretty "||") <+> prettyTm y
prettyTm (INot x) = operator (pretty '~') <> prettyTm x
prettyTm (System xs) = braces (mempty <+> hsep (punctuate comma (map go (Map.toList xs))) <+> mempty) where
prettyTm (System xs) = braces (line <> indent 2 (vcat (punctuate comma (map go (Map.toList xs)))) <> line) where
go (f, t) = prettyTm f <+> operator (pretty "=>") <+> prettyTm t
prettyTm (Case x xs) = keyword (pretty "case") <+> prettyTm x <+> keyword (pretty "of") <+> braces (prettyCase xs)
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
prettyTm x = error (show x)
prettyCase = vsep . map go where
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
@ -126,6 +130,7 @@ 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


Loading…
Cancel
Save