uAgda-1.1.0.0: TypeCheckerNF.hs
{-# LANGUAGE PackageImports, TypeSynonymInstances, FlexibleInstances, GADTs #-}
-- Type checker loosely based on
--
-- "On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory", Abel, Coquand, Dybjer
--
-- some ideas from
--
-- "A Tutorial Implementation of a Dependently Typed Lambda Calculus", Löh, McBride, Swierstra
--
-- are also implemented.
--
-- The ideas related to parametricity and erasure are developed in
--
-- "Realizability and Parametricity in Pure Type Systems", Bernardy, Lasson
--
module TypeCheckerNF where
import Prelude hiding (length)
import Basics
import qualified Terms
import Terms (Term (Ann))
import Display
import Control.Monad.Error
import Data.Char
import Data.Maybe (isJust)
import Control.Monad.Trans.Error (ErrorT, runErrorT)
import Control.Monad.Trans.Writer
import Data.Functor.Identity
import Data.Sequence hiding (replicate)
import Data.Foldable (toList)
import Normal hiding (Term)
import Options
instance Error (Term,Doc) where
strMsg s = (Terms.Hole dummyPosition "strMsg: panic!",text s)
type Result a = (ErrorT (Term,Doc)) -- term is used for position information
(WriterT [Doc] Identity) a
report :: Doc -> Result ()
report x = lift $ tell [x]
runChecker :: Result a -> (Either (Term,Doc) a,[Doc])
runChecker x = runIdentity $ runWriterT $ runErrorT x
data Definition = Abstract -- ^ lambda, pi, sigma bound
| Direct Value -- ^ pair bound
type Value = NF
type Type = Value
data Bind = Bind {entryIdent :: Ident,
entryValue :: Definition, -- ^ Value for identifier.
entryType :: Type, -- ^ Attention: context of the type does not contain the variable bound here.
entryRelevance :: Relevance
}
type Context = Seq Bind
display :: Context -> NF -> Doc
display c = prettyTerm (fmap entryIdent c)
displayT :: Context -> Term -> Doc
displayT = Terms.prettyTerm . fmap entryIdent
dispContext :: Context -> Doc
dispContext ctx = case viewl ctx of
EmptyL -> mempty
Bind x val typ o :< ctx' -> let di = display ctx' in (case val of
Abstract -> pretty x <+> colon o <+> di typ
-- Direct (OfParam _ v) -> "⟦"<>pretty x<>"⟧" <+> sep ["=" <+> parens (di v), "::" <+> di typ]
Direct v -> pretty x <+> sep ["=" <+> parens (di v), colon o <+> di typ]
) $$ dispContext ctx'
-- FIXME: flag an error if impredicativity disabled and we use it anyway.
hole = Neu . Var . Hole
todo = Re
resurrect :: Relevance -> Context -> Context
resurrect Re = id
resurrect Ir = fmap (\e -> e {entryRelevance = Re})
iType :: Context -> Term -> Result (Value,Type)
iType g (Ann e tyt)
= do (ty,o) <- iSort g tyt
v <- cType g e ty
return (v,ty) -- annotations are removed
iType g t@(Terms.Star p s)
= return (Star s,Star $ above s)
iType g (Terms.Pi r1 ident tyt tyt')
= do (ty ,s1) <- iSort (resurrect r1 g) tyt
(ty',s2) <- iSort (Bind ident Abstract ty r1 <| g) tyt'
let o = s1 ⊔ s2
return (Pi r1 ident ty ty', Star o)
iType g (Terms.Sigma ident tyt tyt')
= do let r1 = todo
(ty,s1) <- iSort (resurrect r1 g) tyt
(ty',s2) <- iSort (Bind ident Abstract ty r1 <| g) tyt'
let o = s1 ⊔ s2
return (Sigma r1 ident ty ty', Star o)
iType g e@(Terms.Bound _ x) = case o of
Ir -> throwError (e,"Cannot use irrelevant variable in relevant context")
Re -> return $ (val $ value, wkn (x+1) $ typ)
where val (Direct v) = wkn (x+1) v
val _ = var x -- etaExpand o (var' x) typ
Bind _ value typ o = g `index` x
iType g (Terms.Hole p x) = do
report $ hang (text ("context of " ++ x ++ " is")) 2 (dispContext g)
return (hole x, hole ("type of " ++ x))
iType g (e1 Terms.:$: e2)
= do (v1,si) <- iType g e1
case si of
Pi o _ ty ty' -> do
v2 <- cType (resurrect o g) e2 ty
return (app o v1 v2, subst0 v2 ty')
_ -> throwError (e1,"invalid application")
iType g (Terms.Proj e f) = do
(v,t) <- iType g e
search v t
where search :: NF -> NF -> Result (Value,Type)
search v (Sigma o (Irr (Identifier (_,f'))) ty ty')
| f == f' = return (π1,ty)
| otherwise = search π2 (subst0 π1 ty')
where
(π1,π2) = (case v of
Pair _ _ x y -> (x,y) -- substitution is useless if the pair is in normal form.
_ -> (proj o v True (Irr f'),proj o v False (Irr f')) -- This could not happen if eta-expansion were done.
) :: (NF,NF)
search _ _ = throwError (e,"field not found")
iType g (Terms.Pair ident e1 e2) = do
(v1,t1) <- iType g e1
let r1 = todo
(v2,t2) <- iType (Bind ident (Direct v1) t1 r1 <| g) e2
return $ (Pair r1 ident v1 (str v2),Sigma r1 ident t1 t2)
-- Note: the above does not infer a most general type: any potential dependency is discarded.
iType g t@(Terms.Lam x (Terms.Hole _ _) e) = throwError (t,"cannot infer type for" <+> displayT g t)
iType g (Terms.Lam x ty e) = do
(vty,Sort _) <- iSort g ty
let o = todo
(ve,t) <- iType (Bind x Abstract vty o <| g) e
return $ (Lam o x vty ve, Pi o x vty t)
iType g (Terms.Param e) = do
(v,t) <- iType g e
return (param v, app Ir (param t) v)
iType g (Terms.Shift f e) = do
(v,t) <- iType g e
return (shift f v, shift f t)
iType g x@(Terms.Destroy d e) = do
(v,t) <- iType g e
return (destroy d v,destroy d t)
iSort :: Context -> Term -> Result (Type,Sort)
iSort g e = do
(val,v) <- iType g e
case v of
Star i -> return (val,i)
(Neu (Var (Hole h))) -> do
report $ text h <+> "must be a type"
return $ (hole h, Sort 1)
_ -> throwError (e,displayT g e <+> "is not a type")
unify :: Context -> Term -> Type -> Type -> Result ()
unify g e q q' =
do let ii = length g
constraint = report $ vcat ["constraint: " <> display g q',
"equal to : " <> display g q]
case (q,q') of
((Neu (Var (Hole _))), t) -> constraint
(t, Neu (Var (Hole _))) -> constraint
_ -> unless (q == q')
(throwError (e,hang "type mismatch: " 2 $ vcat
["inferred:" <+> display g q',
"expected:" <+> display g q ,
"for:" <+> displayT g e ,
"context:" <+> dispContext g]))
-- Check the type and normalize
cType :: Context -> Term -> Type -> Result Value
cType g (Terms.Lam name (Terms.Hole _ _) e) (Pi o name' ty ty') = do
e' <- cType (Bind name Abstract ty o <| g) e ty'
return (Lam o name ty e') -- the type is filled in.
cType g (Terms.Lam name ty0 e) (Pi o name' ty ty')
= do (t,_o) <- iSort g ty0
unify g (Terms.Hole (identPosition name) (show name)) t ty
e' <- cType (Bind name Abstract ty o <| g) e ty'
return (Lam o name ty e')
cType g (Terms.Pair name e1 e2) (Sigma o name' ty ty') = do
-- note that names do not have to match.
v1 <- cType g e1 ty
v2 <- cType (Bind name (Direct v1) ty o <| g) e2 (wk $ subst0 v1 ty')
-- The above weakening is there because:
-- * the type contains no occurence of the bound variable after substitution, but
-- * the context is extended anyway, to bind the name to its value.
return $ Pair o name' v1 (str v2)
-- note that the pair must use the name of the sigma for the
-- field. (The context will use the field name provided by the type)
-- Γ ⊢ ⌊A⌋ : B
cType g (Terms.OfParam i e) t = do
-- Γ ⊢ A ⌊A⌋ : ⟦B⟧ ⌊A⌋
-- Γ ⊢ A x : ⟦B⟧ x
-- Γ ⊢ A : (x : ⌊B⌋) → ⟦B⟧ x
e' <- cType g e $ Pi Ir i t (zerInRel 0 t)
return (Neu $ OfParam i e')
cType g (Terms.Shift f e) t = do
shift f <$> cType g e (shift (negate f) t)
-- there might be negative sorts in there, but that should be fine;
-- if they occur the type checker will simply reject the term
-- because it's impossible to create an inhabitant of a negative
-- sort.
cType g e v
= do (e',v') <- iType g e
unify g e v v'
return e'