Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Tree: 30d87904d3
Fetching contributors…

Cannot retrieve contributors at this time

752 lines (648 sloc) 33.032 kB
> {-# OPTIONS_GHC -fglasgow-exts #-}
> module Ivor.Typecheck(typecheck, tcClaim,
> check, checkAndBind, checkAndBindWith, checkAndBindPair,
> convert,
> checkConv, checkConvEnv, pToV, pToV2,
> verify, Gamma) where
> import Ivor.TTCore
> import Ivor.Gadgets
> import Ivor.Nobby
> import Ivor.Unify
> import Ivor.Constant
> import Ivor.Errors
> import Ivor.Evaluator
> import Ivor.Values
> import Ivor.Overloading
> import Control.Monad.State
> import Data.List
> import Debug.Trace
Conversion in the presence of staging is a bit more than simply syntactic
equality on values, since it is possible values contain quoted code which
code be run later. So we say {'x} =~ {'y] iff x =~ y. Otherwise it's
syntactic.
> convert :: Gamma Name -> Indexed Name -> Indexed Name -> Bool
> convert g x y = convertEnv [] g x y
> convertEnv env g x y
> = (convNormaliseEnv env g x) == (convNormaliseEnv env g y)
> -- conv (Stage (Quote x)) (Stage (Quote y)) = convertEnv env g x y
> -- need to actually reduce inside quotes to do conversion check
convert g x y = trace ((show (normalise g x)) ++ " & " ++ (show (normalise g y))) $ (normalise g x)==(normalise g y)
> checkConv :: Gamma Name -> Indexed Name -> Indexed Name -> IError -> IvorM ()
> checkConv g x y err = if convert g x y then return ()
> else ifail err
> checkConvEnv :: Env Name -> Gamma Name -> Indexed Name -> Indexed Name ->
> IError -> IvorM ()
> checkConvEnv env g x y err = if convertEnv env g x y then return ()
> else ifail err
*****
SORT OUT TOP LEVEL TYPECHECKING FUNCTIONS
DEFINE THE INTERFACE CLEARLY
These are: check, checkAndBind, checkAndBindPair.
All should work by generating constraints and solving them, differing only
in when the constraints get solved.
so....
1. Generate constraints
2. Unify, checking for conversion and creating a substitution
3. Substitute into term and type
*****
Top level typechecking function - takes a context and a raw term,
returning a pair of a term and its type
> typecheck :: Gamma Name -> Raw -> IvorM (Indexed Name,Indexed Name)
> typecheck gamma term = do t <- check gamma [] term Nothing
> return t
> typecheckAndBind :: Gamma Name -> Raw ->
> IvorM (Indexed Name,Indexed Name, Env Name)
> typecheckAndBind gamma term = checkAndBind gamma [] term Nothing
Check a term, and return well typed terms with explicit names (i.e. no
de Bruijn indices)
> tcClaim :: Gamma Name -> Raw -> IvorM (Indexed Name,Indexed Name)
> tcClaim gamma term = do (Ind t, Ind v) <- check gamma [] term Nothing
> {-trace (show t) $-}
> return (Ind (makePs t), Ind (makePs v))
Check takes a global context, a local context, the term to check and
its expected type, if known, and returns a pair of a term and its
type.
> type CheckState =
> (Level, -- Level number
> Bool, -- Inferring types of names (if true)
> Env Name, -- Extra bindings, if above is true
> -- conversion constraints; remember the environment at the time we tried
> -- also the context of where the constraint came from
> [(Env Name, Indexed Name, Indexed Name, Maybe FileContext)],
> -- Metavariables we've introduce to define later
> [Name],
> Maybe FileContext)
> type Level = Int
> data FileContext = FC FilePath Int
> deriving (Show, Eq)
> errCtxt :: Maybe FileContext -> IError -> IError
> errCtxt (Just (FC f l)) err = IContext (f ++ ":" ++ show l ++ ":") err
> errCtxt _ err = err
> errCtxtCS :: CheckState -> IError -> IError
> errCtxtCS (_,_,_,_,_,fc) err = errCtxt fc err
Finishes up type checking by making a substitution from all the conversion
constraints and applying it to the term and type.
> doConversion :: Raw -> Gamma Name ->
> [(Env Name, Indexed Name, Indexed Name,Maybe FileContext)] ->
> Indexed Name -> Indexed Name ->
> IvorM (Indexed Name, Indexed Name)
> doConversion raw gam constraints (Ind tm) (Ind ty) =
> -- trace ("Finishing checking " ++ show tm ++ " with " ++ show (length constraints) ++ " equations\n" ++ showeqn (map (\x -> (True,x)) constraints)) $
> -- Unify twice; first time collect the substitutions, second
> -- time do them. Because we don't know what order we can solve
> -- constraints in and they might depend on each other...
> do let cs = nub constraints
> (subst, nms) <- mkSubst $ (map (\x -> (True,x)) cs) ++
> (map (\x -> (False,x)) (reverse cs))
> let tm' = papp subst tm
> let ty' = papp subst ty
> return (Ind tm',Ind ty')
Handy to pass through all the variables, for tracing purposes when debugging.
> where mkSubst xs = mkSubst' (P,[]) xs xs
> mkSubst' acc [] all = return acc
> mkSubst' acc (q:xs) all
> = do acc' <- mkSubstQ acc q all
> mkSubst' acc' xs all
>
> eqn (ok, (env, x, y, fc)) = if ok then (x,y,fc) else (x,y,Nothing)
> showeqn all = concat $ map ((++"\n").show.eqn) all
> mkSubstQ (s',nms) (ok, (env,Ind x,Ind y,fc)) all
> = do -- (s',nms) <- mkSubst xs
> let x' = papp s' x
> let (Ind y') = eval_nf gam (Ind (papp s' y))
> uns <- case unifyenvErr ok gam env (Ind y') (Ind x') of
> Right uns -> {- trace (show (y', x', uns)) $ -} return uns
> Left err -> {- trace (showeqn all) $ -}
> ifail (errCtxt fc (ICantUnify (Ind y') (Ind x')))
Failure err -> fail $ err ++"\n" ++ show nms ++"\n" ++ show constraints -- $ -} ++ " Can't convert "++show x'++" and "++show y' ++ "\n" ++ show constraints ++ "\n" ++ show nms
> extend s' nms uns
> extend phi nms [] = return (phi, nms)
> extend phi nms ((n,tm):uns)
> = extend ((scomp $! (delta n tm)) $! phi) ((n,tm):nms) uns
> scomp :: Subst -> Subst -> Subst
> scomp s2 s1 tn = papp s2 (s1 tn)
> delta n ty n' | n == n' = ty
> | otherwise = P n'
> convertAllEnv :: Gamma Name ->
> [(Env Name, Indexed Name, Indexed Name,Maybe FileContext)] ->
> Env Name -> IvorM (Env Name)
> convertAllEnv gam constraints [] = return []
> convertAllEnv gam constraints ((n,B b t):xs)
> = do (Ind t', _) <- doConversion RStar gam constraints (Ind t) (Ind Star)
> xs' <- convertAllEnv gam constraints xs
> return ((n,B b t'):xs')
> check :: Gamma Name -> Env Name -> Raw -> Maybe (Indexed Name) ->
> IvorM (Indexed Name, Indexed Name)
> check gam env tm mty = do
> ((tm', ty'), (_,_,_,convs,_,_)) <- lvlcheck 0 False 0 gam env tm mty
> tm'' <- doConversion tm gam convs tm' ty'
> return tm''
> checkAndBind :: Gamma Name -> Env Name -> Raw ->
> Maybe (Indexed Name) ->
> IvorM (Indexed Name, Indexed Name, Env Name)
> checkAndBind gam env tm mty = do
> ((v,t), (next,inf,e,convs,_,_)) <- lvlcheck 0 True 0 gam env tm mty
> e <- convertAllEnv gam convs e
> (v'@(Ind vtm),t') <- doConversion tm gam convs v t -- (normalise gam t1')
> return (v',t',e)
Check a pattern and an intermediate computation together
> checkAndBindWith :: Gamma Name -> Raw -> Raw -> Name ->
> IvorM (Indexed Name, Indexed Name, Indexed Name, Indexed Name, Env Name)
> checkAndBindWith gam tm1 tm2 root = do
> ((v1,t1), (next, inf, e, bs,_,_)) <- lvlcheck 0 True 0 gam [] tm1 Nothing
> -- rename all the 'inferred' things to another generated name,
> -- so that they actually get properly checked on the rhs
> let realNames = mkNames next
> -- The environment will need the conversions applying, to fill in any implicit
> -- variables in the pattern
> e <- convertAllEnv gam bs e
> e' <- renameB gam realNames (renameBinders e)
> (v1, t1) <- doConversion tm1 gam bs v1 t1
> (v1', t1') <- fixupGam gam realNames (v1, t1)
> (v1''@(Ind vtm),t1'') <- doConversion tm1 gam bs v1' t1' -- (normalise gam t1')
> -- Drop names out of e' that don't appear in v1'' as a result of the
> -- unification.
> let namesbound = getNames (Sc vtm)
> let ein = orderEnv (filter (\ (n, ty) -> n `elem` namesbound) e')
> ((v2,t2), (_, _, e'', bs',metas,_)) <- lvlcheck 0 inf next gam ein tm2 Nothing
> (v2',t2') <- doConversion tm2 gam bs' v2 t2 -- (normalise gam t2)
> let retEnv = reverse (ein ++ e'')
> if (null metas)
> then return (v1',t1',v2',t2',retEnv)
> else fail "Can't have metavariables here"
> where mkNames 0 = []
> mkNames n
> = ([],Ind (P (MN ("INFER",n-1))),
> Ind (P (MN ("T",n-1))), "renaming"):(mkNames (n-1))
> renameBinders [] = []
> renameBinders (((MN ("INFER",n)),b):bs)
> = ((MN ("T",n),b):(renameBinders bs))
> renameBinders (b:bs) = b:renameBinders bs
Check two things together, with the same environment and variable inference,
and with the same expected type.
We need this for checking pattern clauses...
Return a list of the functions we need to define to complete the definition.
> checkAndBindPair :: Gamma Name -> Raw -> Raw ->
> IvorM (Indexed Name, Indexed Name,
> Indexed Name, Indexed Name, Env Name,
> [(Name, Indexed Name)])
> checkAndBindPair gam tm1 tm2 = do
> ((v1,t1), (next, inf, e, bs,_,_)) <- lvlcheck 0 True 0 gam [] tm1 Nothing
> -- rename all the 'inferred' things to another generated name,
> -- so that they actually get properly checked on the rhs
> let realNames = mkNames next
> -- The environment will need the conversions applying, to fill in any implicit
> -- variables in the pattern
> e <- convertAllEnv gam bs e
> e' <- renameB gam realNames (renameBinders e)
> (v1, t1) <- doConversion tm1 gam bs v1 t1
> (v1', t1') <- fixupGam gam realNames (v1, t1)
> (v1''@(Ind vtm),t1'') <- doConversion tm1 gam bs v1' t1' -- (normalise gam t1')
> -- Drop names out of e' that don't appear in v1'' as a result of the
> -- unification.
> let namesbound = getNames (Sc vtm)
> let ein = orderEnv (filter (\ (n, ty) -> n `elem` namesbound) e')
> ((v2,t2), (_, _, e'', bs',metas,_)) <- {- trace ("Checking " ++ show tm2 ++ " has type " ++ show t1') $ -} lvlcheck 0 inf next gam ein tm2 (Just t1')
> (v2',t2') <- doConversion tm2 gam bs' v2 t2 -- (normalise gam t2)
> let retEnv = reverse (ein ++ e'')
> if (null metas)
> then return (v1',t1',v2',t2',retEnv, [])
> else do let (Ind v2tt) = v2'
> let (v2'', newdefs) = updateMetas v2tt
> return (v1',t1',Ind v2'',t2',retEnv, map (\ (x,y) -> (x, (normalise gam (Ind y)))) newdefs)
if (null newdefs) then
else trace (traceConstraints bs') $ return (v1',t1',Ind v2'',t2',e'', map (\ (x,y) -> (x, Ind y)) newdefs)
> where mkNames 0 = []
> mkNames n
> = ([],Ind (P (MN ("INFER",n-1))),
> Ind (P (MN ("T",n-1))), IMessage "renaming"):(mkNames (n-1))
> renameBinders [] = []
> renameBinders (((MN ("INFER",n)),b):bs)
> = ((MN ("T",n),b):(renameBinders bs))
> renameBinders (b:bs) = b:renameBinders bs
We need to order environments so that names used later are bound first.
*sigh*. This is turning into an almighty hack... I'm not convinced an
ordinary sort will do all the comparisons we need. Still, it's O(n^3) but
n is unlikely ever to be very big. Let's rethink this if it proves a
bottleneck.
> orderEnv [] = []
> orderEnv (x:xs) = insertEnv x (orderEnv xs)
> insertEnv x [] = [x]
Insert here if the name at x does not appear later in any type.
> insertEnv x (y:ys) = if (appearsIn x (y:ys))
> then y:(insertEnv x ys)
> else x:y:ys
if (all (\e -> envLT x e) (y:ys))
then y:(insertEnv x ys)
else x:y:ys
> where
> appearsIn (n,_) env = any (n_in n) env
> n_in n (n2, B _ t) = n `elem` (getNames (Sc t))
envLT (n1,B _ t1) (n2,B _ t2)
| n2 `elem` (getNames (Sc t1)) = False
| otherwise = True -- not (n1 `elem` (getNames (Sc t2)))
> traceConstraints [] = ""
> traceConstraints ((_,x,y,_):xs) = show (x,y) ++ "\n" ++ traceConstraints xs
> inferName n = (MN ("INFER", n))
> lvlcheck :: Level -> Bool -> Int ->
> Gamma Name -> Env Name -> Raw ->
> Maybe (Indexed Name) ->
> IvorM ((Indexed Name, Indexed Name), CheckState)
> lvlcheck lvl infer next gamma env tm exp
> = -- let tms = getTerms tm in
> runStateT (tcfixupTop env lvl tm exp) (next, infer, [], [], [], Nothing)
> where
Do the typechecking, then unify all the inferred terms.
> tcfixupTop env lvl t exp = do
> tm@(_,tmty) <- tc env lvl t exp
> (next, infer, bindings, errs ,mvs, fc) <- get
> -- First, insert inferred values into the term
> tm'@(_,tmty) <- fixup errs tm
> -- Then check the resulting type matches the expected type.
> if infer then (case exp of
> Nothing -> return ()
> Just expty -> checkConvSt env gamma tmty expty )
> else return ()
> -- Then fill in any remained inferred values we got by knowing the
> -- expected type
> (next, infer, bindings, errs, mvs, fc) <- get
> tm <- fixup errs tm
> -- bindings <- fixupB gamma errs bindings
> put (next, infer, bindings, errs, mvs, fc)
> return tm'
> tcfixup env lvl t exp = do
> tm@(_,tmty) <- tc env lvl t exp
> -- case exp of
> -- Nothing -> return ()
> -- Just expt -> checkConvSt env gamma expt tmty "Type error"
> (next, infer, bindings, errs, mvs, fc) <- get
> tm' <- fixup errs tm
> bindings <- (fixupB gamma errs) $! bindings
> put (next, infer, bindings, errs, mvs, fc)
> return tm'
tc has state threaded through -- state is a tuple of the next name to
generate, the stage we're at, and a list of conversion errors (which
will later be unified). Needs an explicit type to help out ghc's
typechecker...
> tc :: Env Name -> Level -> Raw -> Maybe (Indexed Name) ->
> StateT CheckState IvorM (Indexed Name, Indexed Name)
> tc env lvl (Var n) exp = do
> (rv, rt) <- mkTT (lookupi n env 0) (glookup n gamma)
> case exp of
> Nothing -> return (rv,rt)
> Just expt -> do checkConvSt env gamma rt expt
> return (rv,rt)
> where mkTT (Just (i, B _ t)) _ = return (Ind (P n), Ind t)
> mkTT Nothing (Just ((Fun _ _),t)) = return (Ind (P n), t)
> mkTT Nothing (Just ((Partial _ _),t)) = return (Ind (P n), t)
> mkTT Nothing (Just ((PatternDef _ _ _),t)) = return (Ind (P n), t)
> mkTT Nothing (Just (Unreducible,t)) = return (Ind (P n), t)
> mkTT Nothing (Just (Undefined,t)) = return (Ind (P n), t)
> mkTT Nothing (Just ((ElimRule _),t)) = return (Ind (Elim n), t)
> mkTT Nothing (Just ((PrimOp _ _),t)) = return (Ind (P n), t)
> mkTT Nothing (Just ((DCon tag i),t)) = return (Ind (Con tag n i), t)
> mkTT Nothing (Just ((TCon i _),t)) = return (Ind (TyCon n i), t)
> mkTT Nothing Nothing = defaultResult
> lookupi x [] _ = Nothing
> lookupi x ((n,t):xs) i | x == n = Just (i,t)
> lookupi x (_:xs) i = lookupi x xs (i+1)
> defaultResult = do
> (next, infer, bindings, errs, mvs, fc) <- get
> case lookup n bindings of
> Nothing ->
> if infer then case exp of
> Nothing -> lift $ ifail (errCtxt fc (INoSuchVar n))
> Just (Ind t) -> do put (next, infer, (n, B Pi t):bindings, errs, mvs, fc)
> return (Ind (P n), Ind t)
> else lift $ ifail (errCtxt fc (INoSuchVar n))
> Just (B Pi t) -> return (Ind (P n), Ind t)
> tc env lvl (ROpts ns) Nothing = fail $ "Need a type for overloaded names"
> tc env lvl (ROpts ns) (Just exp) = fail $ "Overloading not implemented (" ++ show ns ++ " : " ++ show exp ++ ")"
> tc env lvl (RApp f a) exp = do
> (Ind fv, Ind ft) <- tcfixup env lvl f Nothing
> let fnfng = normaliseEnv env emptyGam (Ind ft)
> let fnf = normaliseEnv env gamma (Ind ft)
> (rv, rt) <-
> case (fnfng,fnf) of
> ((Ind (Bind _ (B Pi s) (Sc t))),_) -> do
> (Ind av,Ind at) <- tcfixup env lvl a (Just (Ind s))
> let sty = (normaliseEnv env gamma (Ind s))
> let tt = (Bind (MN ("x",0)) (B (Let av) at) (Sc t))
> let tmty = (normaliseEnv env emptyGam (Ind tt))
> checkConvSt env gamma (Ind at) sty
> return (Ind (App fv av), tmty)
> (_, (Ind (Bind _ (B Pi s) (Sc t)))) -> do
> (Ind av,Ind at) <- tcfixup env lvl a (Just (Ind s))
> checkConvSt env gamma (Ind at) (Ind s)
> let tt = (Bind (MN ("x",0)) (B (Let av) at) (Sc t))
> let tt' = (normaliseEnv env gamma (Ind tt))
> return (Ind (App fv av), (normaliseEnv env gamma (Ind tt)))
> _ -> fail $ "Cannot apply a non function type " ++ show ft ++ " to " ++ show a
> return (rv,rt)
> case exp of
> Nothing -> return (rv,rt)
> Just expt -> do checkConvSt env gamma rt expt
> return (rv,rt)
> tc env lvl (RConst x) _ = lift $ tcConst x
> tc env lvl RStar _ = return (Ind Star, Ind Star)
> tc env lvl (RFileLoc f l t) exp =
> do (next, infer, bindings, errs, mvs, fc) <- get
> put (next, infer, bindings, errs, mvs, Just (FC f l))
> tc env lvl t exp
Pattern bindings are a special case since they may bind several names,
and we don't convert names to de Bruijn indices
> tc env lvl (RBind n (B (Pattern p) ty) sc) exp = do
> (gb, env) <- checkpatt gamma env lvl n p ty
> let scexp = case exp of
> Nothing -> Nothing
> (Just (Ind (Bind sn sb (Sc st)))) -> Just $
> normaliseEnv ((sn,sb):env) gamma (Ind st)
> (Ind scv, Ind sct) <- tcfixup ((n,gb):env) lvl sc scexp
> discharge gamma n gb (Sc scv) (Sc sct)
> tc env lvl (RBind n b sc) exp = do
> gb <- checkbinder gamma env lvl n b
> let scexp = case exp of
> Nothing -> Nothing
> (Just (Ind (Bind sn sb (Sc st)))) -> Just $
> normaliseEnv ((sn,sb):env) gamma (Ind st)
> _ -> fail (show exp)
> (Ind scv, Ind sct) <- tcfixup ((n,gb):env) lvl sc Nothing -- scexp
> --discharge gamma n gb (Sc scv) (Sc sct)
> discharge gamma n gb (pToV n scv) (pToV n sct)
> tc env lvl l@(RLabel t comp) _ = do
> (Ind tv, Ind tt) <- tcfixup env lvl t Nothing
> let ttnf = normaliseEnv env gamma (Ind tt)
> case ttnf of
> (Ind Star) -> do compv <- checkComp env lvl comp
> return (Ind (Label tv compv), Ind Star)
> _ -> fail $ "Type of label " ++ show l ++ " must be *"
> tc env lvl (RCall comp t) _ = do
> compv <- checkComp env lvl comp
> (Ind tv, Ind tt) <- tcfixup env lvl t Nothing
> let ttnf = normaliseEnv env gamma (Ind tt)
> case ttnf of
> (Ind (Label t comp)) -> return (Ind (Call compv tv), Ind t)
> _ -> fail $ "Type of call must be a label"
> tc env lvl (RReturn t) (Just exp) = do
> let expnf = normaliseEnv env gamma exp
> case expnf of
> (Ind (Label lt comp)) -> do
> (Ind tv, Ind tt) <- tcfixup env lvl t (Just (Ind lt))
> checkConvSt env gamma (Ind lt) (Ind tt)
> return (Ind (Return tv), Ind (Label tt comp))
> _ -> fail $ "return " ++ show t++ " should give a label, got " ++ show expnf
> tc env lvl (RReturn t) Nothing = fail $ "Need to know the type to return for "++show t
> tc env lvl (RStage s) exp = do
> (Ind sv, Ind st) <- tcStage env lvl s exp
> return (Ind sv, Ind st)
> tc env lvl RInfer (Just (Ind exp)) = do
> (next, infer, bindings, errs, mvs, fc) <- get
> let bindings' = if infer
> then (inferName next, B Pi exp):bindings
> else bindings
> put (next+1, infer, bindings', errs, mvs, fc)
> return (Ind (P (inferName next)), Ind exp)
> tc env lvl RInfer Nothing = fail "Can't infer a term for placeholder"
If we have a metavariable, we need to record the type of the expression which
will solve it. It needs to take the environment as arguments, and return
the expected type.
> tc env lvl (RMeta n) (Just (Ind exp))
> = do (next, infer, bindings, errs, mvs, fc) <- get
> put (next, infer, bindings, errs, n:mvs, fc)
> -- Abstract it over the environment so that we have everything
> -- in scope we need.
> tm <- abstractOver (orderEnv env) n exp []
> {-trace (show tm ++ " : " ++ show exp) $ -}
> return (tm,Ind exp)
> -- fail $ show (n, exp, bindings, env) ++ " -- Not implemented"
> where abstractOver [] mv exp args =
> return (Ind (appArgs (Meta mv exp) args))
> abstractOver ((n,B _ t):ns) mv exp args =
> abstractOver ns mv (Bind n (B Pi t) (pToV n exp)) ((P n):args)
mkn (UN n) = MN (n,0)
mkn (MN (n,x)) = MN (n,x+1)
> tc env lvl (RMeta n) Nothing
> -- just invent a name for it and see what inference gives us
> = do (next, infer, bindings, errs, mvs, fc) <- get
> put (next+1, infer, bindings, errs, mvs, fc)
> -- let guessty = Bind (MN ("X", 0)) (B Pi (P (inferName next)))
> -- (Sc (P (inferName (next+1))))
> let guessty = (P (inferName next))
> tc env lvl (RMeta n) (Just (Ind guessty))
fail $ "Don't know the expected type of " ++ show n
> tcStage env lvl (RQuote t) _ = do
> (Ind tv, Ind tt) <- tc env (lvl+1) t Nothing
> return (Ind (Stage (Quote tv)), Ind (Stage (Code tt)))
> tcStage env lvl (RCode t) _ = do
> (Ind tv, Ind tt) <- tc env lvl t Nothing
> let ttnf = normaliseEnv env gamma (Ind tt)
> case ttnf of
> (Ind Star) -> return (Ind (Stage (Code tv)), Ind Star)
> _ -> fail $ "Type of code " ++ show t ++ " must be *"
> tcStage env lvl (REval t) _ = do
> -- when (lvl/=0) $ fail $ "Can't eval at level " ++ show lvl
> (Ind tv, Ind tt) <- tc env lvl t Nothing
> let ttnf = normaliseEnv env gamma (Ind tt)
> case ttnf of
> (Ind (Stage (Code tcode))) ->
> return (Ind (Stage (Eval tv tt)), Ind tcode)
> _ -> fail $ "Can't eval a non-quoted term (type " ++ show ttnf ++ ")"
> tcStage env lvl (REscape t) _ = do
> -- when (lvl==0) $ fail $ "Can't escape at level " ++ show lvl
> (Ind tv, Ind tt) <- tc env lvl t Nothing
> let ttnf = normaliseEnv env gamma (Ind tt)
> case ttnf of
> (Ind (Stage (Code tcode))) ->
> return (Ind (Stage (Escape tv tt)), Ind tcode)
> _ -> fail "Can't escape a non-quoted term"
> checkComp env lvl (RComp n ts) = do
> tsc <- mapM (\ t -> tcfixup env lvl t Nothing) ts
> return (Comp n (map ( \ (Ind v, Ind t) -> v) tsc))
Insert inferred values into the term
> fixup e tm = fixupGam gamma e tm
> tcConst :: (Constant c) => c -> IvorM (Indexed Name, Indexed Name)
> tcConst c = return (Ind (Const c), Ind (constType c))
tcConst Star = return (Ind (Const Star), Ind (Const Star)) --- *:* is a bit dodgy...
checkbinder :: Monad m => Gamma Name -> Env Name -> Level ->
Name -> Binder Raw -> m (Binder (TT Name))
-- FIXME: Should convert here rather than assert it must be *
> checkbinder gamma env lvl n (B Lambda t) = do
> (Ind tv,Ind tt) <- tcfixup env lvl t (Just (Ind Star))
> let ttnf = normaliseEnv env gamma (Ind tt)
> let (Ind tvnf) = normaliseEnv env gamma (Ind tv)
> case ttnf of
> (Ind Star) -> return (B Lambda tvnf)
> (Ind (P (MN ("INFER",_)))) -> return (B Lambda tvnf)
> _ -> fail $ "The type of the binder " ++ show n ++ " must be *"
> checkbinder gamma env lvl n (B Pi t) = do
> (Ind tv,Ind tt) <- tcfixup env lvl t (Just (Ind Star))
> let (Ind tvnf) = normaliseEnv env gamma (Ind tv)
> -- let ttnf = normaliseEnv env gamma (Ind tt)
> checkConvSt env gamma (Ind tt) (Ind Star)
> return (B Pi tvnf)
case ttnf of
(Ind Star) -> return (B Pi tv)
(Ind (P (MN ("INFER",_)))) -> return (B Pi tv)
_ -> fail $ "The type of the binder " ++ show n ++ " must be *"
> checkbinder gamma env lvl n (B (Let v) RInfer) = do
> (Ind vv,Ind vt) <- tcfixup env lvl v Nothing
> return (B (Let vv) vt)
> checkbinder gamma env lvl n (B (Let v) t) = do
> (Ind tv,Ind tt) <- tcfixup env lvl t (Just (Ind Star))
> (Ind vv,Ind vt) <- tcfixup env lvl v (Just (Ind tv))
> let ttnf = normaliseEnv env gamma (Ind tt)
> lift $ checkConvEnv env gamma (Ind vt) (Ind tv) (INotConvertible (Ind vt) (Ind tv))
> case ttnf of
> (Ind Star) -> return (B (Let vv) tv)
> _ -> fail $ "The type of the binder " ++ show n ++ " must be *"
> where dbg (Ind t) = debugTT t
> checkbinder gamma env lvl n (B Hole t) = do
> (Ind tv,Ind tt) <- tcfixup env lvl t Nothing
> let ttnf = normaliseEnv env gamma (Ind tt)
> case ttnf of
> (Ind Star) -> return (B Hole tv)
> _ -> fail $ "The type of the binder " ++ show n ++ " must be *"
> checkbinder gamma env lvl n (B (Guess v) t) = do
> (Ind tv,Ind tt) <- tcfixup env lvl t Nothing
> (Ind vv,Ind vt) <- tcfixup env lvl v Nothing
> let ttnf = normaliseEnv env gamma (Ind tt)
> lift $ checkConvEnv env gamma (Ind vt) (Ind tv) (INotConvertible (Ind vt) (Ind tv))
> case ttnf of
> (Ind Star) -> return (B (Guess vv) tv)
> _ -> fail $ "The type of the binder " ++ show n ++ " must be *"
> checkpatt gamma env lvl n RInfer t = do
> (Ind tv,Ind tt) <- tcfixup env lvl t Nothing
> return ((B MatchAny tv), env)
> checkpatt gamma env lvl n pat t = do
> (Ind tv,Ind tt) <- tcfixup env lvl t Nothing
> (next, infer, bindings, err, mvs, fc) <- get
> put (next, True, bindings, err, mvs, fc)
> (Ind patv,Ind patt) <- tcfixup (bindings++env) lvl pat Nothing
> (next, _ ,bindings, err, mvs, fc) <- get
> put (next, infer, bindings, err, mvs, fc)
> let ttnf = normaliseEnv env gamma (Ind tt)
> --checkConvEnv env gamma (Ind patt) (Ind tv) $
> -- show patt ++ " and " ++ show tv ++ " are not convertible"
> case ttnf of
> (Ind Star) -> return ((B (Pattern patv) tv), bindings++env)
> _ -> fail $ "The type of the binder " ++ show n ++ " must be *"
Check a raw term representing a pattern. Return the pattern, and the
extended environment.
-- > checkPatt :: Monad m => Gamma Name -> Env Name -> Maybe (Pattern Name) ->
-- > Raw -> Raw ->
-- > m (Pattern Name, Env Name)
-- > checkPatt gam env acc (Var n) ty = trace (show n ++ ": "++ show env) $ do
-- > (Ind tyc, _) <- check gam env ty (Just (Ind Star))
-- > (pat, t) <- mkVarPatt (lookupi n env 0) (glookup n gam) (Ind tyc)
-- > --checkConvEnv env gam (Ind tyc) (Ind t) $
-- > -- show ty ++ " and " ++ show t ++ " are not convertible"
-- > return (combinepats acc pat, (n, (B Pi tyc)):env)
-- > where
-- > mkVarPatt (Just (i, B _ t)) _ _ = return (PVar n, t)
-- > mkVarPatt Nothing (Just ((DCon tag i), (Ind t))) _
-- > = do tyname <- getTyName gam n
-- > return (PCon tag n tyname [], t)
-- > mkVarPatt Nothing Nothing (Ind defty) = return (PVar n, defty)
-- > lookupi x [] _ = Nothing
-- > lookupi x ((n,t):xs) i | x == n = Just (i,t)
-- > lookupi x (_:xs) i = lookupi x xs (i+1)
-- > checkPatt gam env acc (RApp f a) ty = do
-- > (Ind tyc, _) <- trace (show ty) $ check gam env ty (Just (Ind Star))
-- > let (RBind _ _ fscope) = ty
-- > let (Bind nm (B _ nmt) _) = tyc
-- > (fpat, fbindingsin) <- checkPatt gam env Nothing f ty
-- > let fbindings = ((nm,(B Pi nmt)):fbindingsin)
-- > (apat, abindings) <- checkPatt gam (fbindings++env)
-- > (Just fpat) a fscope
-- > return (combinepats (Just fpat) apat, fbindings++abindings)
-- where
-- mkEnv = map (\ (n,Ind t) -> (n, B Pi t))
-- > checkPatt gam env acc RInfer ty = return (combinepats acc PTerm, env)
-- > checkPatt gam env _ _ _ = fail "Invalid pattern"
> checkConvSt env g x y
> = do (next, infer, bindings, err, mvs, fc) <- get
> put (next, infer, bindings, (env,x,y,fc):err, mvs, fc)
> return ()
> fixupGam gamma [] tm = return tm
> fixupGam gamma ((env,x,y,_):xs) (Ind tm, Ind ty) = do
> uns <- case unifyenv gamma env y x of
> Right x' -> return x'
> Left err -> return [] -- fail err -- $ "Can't convert "++show x++" and "++show y ++ " ("++show err++")"
> let tm' = fixupNames gamma uns tm
> let ty' = fixupNames gamma uns ty
> fixupGam gamma xs (Ind tm', Ind ty')
> fixupNames gam [] tm = tm
> fixupNames gam ((x,ty):xs) tm = fixupNames gam xs $ substName x ty (Sc tm)
> fixupB gam xs bs = fixupB' gam xs bs []
> fixupB' gam xs [] acc = return acc
> fixupB' gam xs ((n, (B b t)):bs) acc =
> -- if t is already fully explicit, don't bother
> if (allExplicit (getNames (Sc t))) then fixupB' gam xs bs ((n,(B b t)):acc)
> else do (Ind t', _) <- fixupGam gam xs (Ind t, Ind Star)
> fixupB' gam xs bs ((n,(B b t')):acc)
> where allExplicit [] = True
> allExplicit ((MN ("INFER",_)):_) = False
> allExplicit (_:xs) = allExplicit xs
> renameB gam xs [] = return []
> renameB gam xs ((n, (B b t)):bs) = do
> bs' <- renameB gam xs bs
> let t' = renameGam xs t
> return ((n,(B b t')):bs')
> where renameGam [] tm = tm
> renameGam ((env,Ind (P x),Ind (P y),_):xs) tm =
> let tm' = fixupNames gam [(x, P y)] tm in
> renameGam xs tm'
> combinepats Nothing x = x
> combinepats (Just (PVar n)) x = error "can't apply things to a variable"
> combinepats (Just (PCon tag n ty args)) x = PCon tag n ty (args++[x])
> discharge :: Gamma Name -> Name -> Binder (TT Name) ->
> (Scope (TT Name)) -> (Scope (TT Name)) ->
> StateT CheckState IvorM (Indexed Name, Indexed Name)
> discharge gamma n (B Lambda t) scv sct = do
> let lt = Bind n (B Pi t) sct
> let lv = Bind n (B Lambda t) scv
> return (Ind lv,Ind lt)
> discharge gamma n (B Pi t) scv (Sc sct) = do
> checkConvSt [] gamma (Ind Star) (Ind sct)
> let lt = Star
> let lv = Bind n (B Pi t) scv
> return (Ind lv,Ind lt)
> discharge gamma n (B (Let v) t) scv sct = do
> let lt = Bind n (B (Let v) t) sct
> let lv = Bind n (B (Let v) t) scv
> return (Ind lv,Ind lt)
> discharge gamma n (B Hole t) scv (Sc sct) = do
> let lt = sct -- already checked sct and t are convertible
> let lv = Bind n (B Hole t) scv
> -- A hole can't appear in the type of its scope, however.
> lift $ checkNotHoley 0 sct
> return (Ind lv,Ind lt)
> discharge gamma n (B (Guess v) t) scv (Sc sct) = do
> let lt = sct -- already checked sct and t are convertible
> let lv = Bind n (B (Guess v) t) scv
> -- A hole can't appear in the type of its scope, however.
> lift $ checkNotHoley 0 sct
> return (Ind lv,Ind lt)
> discharge gamma n (B (Pattern v) t) scv (Sc sct) = do
> let lt = sct -- already checked sct and t are convertible
> let lv = Bind n (B (Pattern v) t) scv
> -- A hole can't appear in the type of its scope, however.
> lift $ checkNotHoley 0 sct
> return (Ind lv,Ind lt)
> discharge gamma n (B MatchAny t) scv (Sc sct) = do
> let lt = sct
> let lv = Bind n (B MatchAny t) scv
> return (Ind lv,Ind lt)
> checkNotHoley :: Int -> TT n -> IvorM ()
> checkNotHoley i (V v) | v == i = fail "You can't put a hole where a hole don't belong."
> checkNotHoley i (App f a) = do checkNotHoley i f
> checkNotHoley i a
> checkNotHoley i (Bind _ _ (Sc s)) = checkNotHoley (i+1) s
> checkNotHoley i (Proj _ _ t) = checkNotHoley i t
> checkNotHoley _ _ = return ()
checkR g t = (typecheck g t):: (Result (Indexed Name, Indexed Name))
If we're paranoid - recheck a supposedly well-typed term. Might want to
do this after finishing a proof.
> verify :: Gamma Name -> Indexed Name -> IvorM ()
> verify gam tm = do (_,_) <- typecheck gam (forget tm)
> return ()
Jump to Line
Something went wrong with that request. Please try again.