Permalink
Browse files

New typechecking and refinement, improved unification

darcs-hash:20080309213344-228f4-dfdbd16be8eb9af594d294b98f5e8423373bf992.gz
  • Loading branch information...
eb
eb committed Mar 9, 2008
1 parent f631a9f commit 14f22b060d2a113e6b5194905df6be93f2d7a6f8
Showing with 255 additions and 94 deletions.
  1. +19 −0 Ivor/TTCore.lhs
  2. +53 −19 Ivor/Tactics.lhs
  3. +91 −16 Ivor/Typecheck.lhs
  4. +83 −54 Ivor/Unify.lhs
  5. +3 −3 lib/lt.tt
  6. +2 −1 lib/nat.tt
  7. +4 −1 tests/partial.tt
View
@@ -267,6 +267,25 @@ Each V is processed with a function taking the context and the index.
> levelise :: Indexed n -> Levelled n
> levelise (Ind t) = Lev $ vapp (\ (ctx,i) -> V ((length ctx)-i-1)) t
+Same, but for Ps
+
+> papp :: (n -> (TT n)) -> TT n -> TT n
+> papp f t = v' t
+> where
+> v' (P n) = f n
+> v' (V i) = V i
+> v' (App f' a) = (App (v' f') (v' a))
+> v' (Bind n b (Sc sc)) = (Bind n (fmap (v') b)
+> (Sc (v' sc)))
+> v' (Proj n i x) = Proj n i (v' x)
+> v' (Label t (Comp n cs))
+> = Label (v' t) (Comp n (fmap (v') cs))
+> v' (Call (Comp n cs) t)
+> = Call (Comp n (fmap (v') cs)) (v' t)
+> v' (Return t) = Return (v' t)
+> v' (Stage t) = Stage (sLift (v') t)
+> v' x = x
+
FIXME: This needs to rename all duplicated binder names first, otherwise
we get a duff term when we go back to the indexed version.
View
@@ -198,7 +198,7 @@ Add a new claim to the current state
> claim :: Name -> Raw -> Tactic -- ?Name:Type.
> claim x s gam env (Ind t) =
> do (Ind sv, st) <- check gam (ptovenv env) s Nothing
-> checkConv gam st (Ind Star) "Type of claim must be *"
+> -- checkConv gam st (Ind Star) "Type of claim must be *"
> return $ (Ind (Bind x (B Hole (makePsEnv (map fst env) sv)) (Sc t)),
> [NextGoal x])
@@ -209,6 +209,10 @@ Add a new claim with guess to the current state
> claimholey x (Ind holey) (Ind ty) gam env (Ind term) =
> tacret $ Ind (Bind x (B (Guess holey) ty) (Sc term))
+> claimsolved :: Name -> Indexed Name -> Indexed Name -> Tactic
+> claimsolved x (Ind holey) (Ind ty) gam env (Ind term) =
+> tacret $ Ind (Bind x (B (Let holey) ty) (Sc term))
+
Begin solving a goal
> attack :: Name -> Tactic
@@ -223,16 +227,16 @@ Try filling the current goal with a term
> fill :: Raw -> Tactic
> fill guess gam env (Ind (Bind x (B Hole tyin') sc)) =
> do let (Ind tyin) = finalise (Ind tyin')
-> (Ind gvin,Ind gtin) <- {-trace ("checking "++show guess++" in context " ++ show (ptovenv env)) $ -}
-> check gam (ptovenv env) guess (Just (Ind tyin))
+> (Ind gvin,Ind gtin, env) <- {-trace ("checking "++show guess++" in context " ++ show (ptovenv env)) $ -}
+> checkAndBind gam (ptovenv env) guess (Just (Ind tyin))
> let gv = makePsEnv (map fst env) gvin
> let gt = makePsEnv (map fst env) gtin
> let (Ind ty') = normaliseEnv (ptovenv env) (Gam []) (Ind tyin)
> let (Ind ty) = normaliseEnv (ptovenv env) gam (Ind tyin)
> let fgt = finalise (Ind gt)
> let fty' = finalise (Ind ty')
> let fty = finalise (Ind ty)
-> others <- {- trace ("unifying "++show gt++" and "++show ty') $ -}
+> others <- -- trace ("unifying "++show gt++" and "++show ty') $
> case unifyenv (Gam []) (ptovenv env) fgt fty' of
> Nothing -> unifyenv gam (ptovenv env) fgt fty
> (Just x) -> return x
@@ -261,24 +265,42 @@ solvable by unification). (FIXME: Not yet implemented.)
> let (Ind nty) = normaliseEnv (ptovenv env) gam (Ind ntyin)
> let bvin = makePsEnv (map fst env) bv
> -- let (Just (Ind nty)) = lookuptype n gam
-> let claims = uniqifyClaims x env (getClaims (makePsEnv (map fst env) nty))
-> (tm',_) <- doClaims x claims gam env tm
-> let guess = (mkGuess claims [] (forget bvin))
+> let claimTypes = getClaims (makePsEnv (map fst env) nty)
+> let rawapp = mkapp rtm (map (\_ -> RInfer) claimTypes)
+> let (Ind tyin') = finalise (normaliseEnv (ptovenv env) gam (Ind ty))
+> (Ind rtch, rtych, ev) <- checkAndBind gam (ptovenv env) rawapp (Just (Ind tyin'))
+> let argguesses = getArgs rtch
+> -- So we'll have an application, some of the arguments with inferred
+> -- names. Let's record which ones...
+> let claims = uniqifyClaims x env claimTypes
+> let claimGuesses = zip claims (map appVar argguesses)
+> (tm',_) <- {- trace (show claimGuesses) $ -} doClaims x claimGuesses gam env tm
+> let guess = (mkGuess claimGuesses [] (forget bvin))
> (filled, unified) <- runtacticEnv gam env x tm'
> (fill guess)
-> (filled, solved) <- solveUnified [] unified filled
-> filled <- tryDefaults defaults claims filled
+> -- (filled, solved) <- solveUnified [] unified filled
+> -- filled <- tryDefaults defaults claims filled
> -- (tm', _) <- trace (show claims) $ tidy gam env filled
+> let newgoals = mapMaybe isGoal claimGuesses
> return $ (filled, map HideGoal (map fst claims) ++
-> map AddGoal (map fst (reverse claims)))
+> map AddGoal (reverse newgoals))
+> -- map AddGoal (map fst (reverse claims)))
> -- tacret filled --(Ind (Bind x (B Hole ty) (Sc sc')))
> where mkGuess [] defs n = n
-> mkGuess ((x,_):xs) (RInfer:ds) n
+> mkGuess (((x,_),guess):xs) (RInfer:ds) n
> = (mkGuess xs ds (RApp n (Var x)))
-> mkGuess ((x,_):xs) [] n
+> mkGuess (((x,_),guess):xs) [] n
> = (mkGuess xs [] (RApp n (Var x)))
-> mkGuess ((x,_):xs) (d:ds) n
+> -- FIXME: Fix this so default arguments use the 'guess'
+> mkGuess (((x,_),_):xs) (d:ds) n
> = (mkGuess xs ds (RApp n d))
+
+> -- if we inferred a guess, use that, otherwise use the claim name
+> appVar (P (MN ("INFER",_))) = Nothing
+> appVar guess = Just guess
+> isGoal ((n,ty),Nothing) = Just n
+> isGoal ((n,ty),Just _) = Nothing
+
> todo uns (x,_) = not (isSolved x uns)
> solveUnified tohide [] tm = return (tm, tohide)
> solveUnified tohide ((Solved x guess):xs) tm
@@ -296,6 +318,14 @@ solvable by unification). (FIXME: Not yet implemented.)
> (filled, _) <- runtacticEnv gam env c filled solve
> (filled, _) <- runtacticEnv gam env c filled cut
> tryDefaults xs cs filled
+> removeClaims claims tm@(Ind (Bind x b@(B _ ty) (Sc sc)))
+> | x `elem` (map fst claims)
+> = {- trace (show (x,sc, forget sc)) $ -}
+> let (cl',Ind sc') = removeClaims claims (Ind sc) in
+> if (nameOccurs x (forget sc'))
+> then (cl', Ind (Bind x b (Sc sc')))
+> else ((x,ty):cl', Ind sc')
+> | otherwise = ([], tm)
> refine _ _ _ _ _ = fail "Not focused on a hole"
@@ -312,17 +342,21 @@ solvable by unification). (FIXME: Not yet implemented.)
> xs' = substClaim x (P newx) xs in
> (newx, ty):(uniqifyClaims nspace ((newx, B Hole ty):env) xs')
> where substClaim x newx [] = []
-> substClaim x newx ((n,ty):xs) = (n,substName x newx (Sc ty)):
-> (substClaim x newx xs)
+> substClaim x newx ((n,ty):xs)
+> = (n,substName x newx (Sc ty)):
+> (substClaim x newx xs)
> mkns (UN a) (UN b) = UN (a++"_"++b)
> mkns (MN (a,i)) (UN b) = MN (a++"_"++b, i)
> mkns (MN (a,i)) (MN (b,j)) = MN (a++"_"++b, i)
-> doClaims :: Name -> [(Name, TT Name)] -> Tactic
+> doClaims :: Name -> [((Name, TT Name), Maybe (TT Name))] -> Tactic
> doClaims h [] gam env tm = tacret $ tm
-> doClaims h ((n,ty):xs) gam env tm =
+> doClaims h (((n,ty),Nothing):xs) gam env tm =
> do (tm',_) <- runtacticEnv gam env h tm (claim n (forget ty))
> doClaims h xs gam env tm'
+> doClaims h (((n,ty),Just v):xs) gam env tm =
+> do (tm',_) <- runtacticEnv gam env h tm (claimsolved n (Ind v) (Ind ty))
+> doClaims h xs gam env tm'
Give up the current try
@@ -401,7 +435,7 @@ Do case analysis by the given elimination operator
> let mbinding = (B (Let mtype) (snd motive))
> let claims = uniqifyClaims x env methods
> (Ind mbody, [])
-> <- doClaims x claims gam (((fst motive),mbinding):env) tm
+> <- doClaims x (zip claims (repeat Nothing)) gam (((fst motive),mbinding):env) tm
> let mbind = Bind (fst motive) mbinding (Sc mbody)
> let ruleapp = (forget (mkGuess claims (App bvin (P (fst motive)))))
> (filled, _) <- runtacticEnv gam env x (Ind mbind)
@@ -573,7 +607,7 @@ Boolean flag (flip) is True if symmetry should be applied first.
> (qty,a,b) <- getTypes rulet
> let tP = (Bind nm (B Lambda qty) (Sc (substTerm b (P nm) (Sc ty))))
> let p = substTerm b a (Sc ty)
-> (tm',_) <- doClaims x ([(claimname,p)]) gam env tm
+> (tm',_) <- doClaims x ([((claimname,p),Nothing)]) gam env tm
> let repltm = mkapp repl (RInfer:RInfer:RInfer:userule:(forget tP):(Var claimname):[])
> (filled, _) <- runtacticEnv gam env x tm' (fill repltm)
> return (filled, [AddGoal claimname])
View
@@ -1,6 +1,10 @@
> {-# OPTIONS_GHC -fglasgow-exts #-}
-> module Ivor.Typecheck(module Ivor.Typecheck, Gamma) where
+> module Ivor.Typecheck(typecheck, tcClaim,
+> check, checkAndBind, checkAndBindPair,
+> convert,
+> checkConv, checkConvEnv, pToV, pToV2,
+> verify, Gamma) where
> import Ivor.TTCore
> import Ivor.Gadgets
@@ -38,6 +42,20 @@ syntactic.
> else fail 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
@@ -49,6 +67,9 @@ returning a pair of a term and its type
> m (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 :: Monad m => Gamma Name -> Raw -> m (Indexed Name,Indexed Name)
> tcClaim gamma term = do (Ind t, Ind v) <- check gamma [] term Nothing
> {-trace (show t) $-}
@@ -62,23 +83,64 @@ type.
> (Level, -- Level number
> Bool, -- Inferring types of names (if true)
> Env Name, -- Extra bindings, if above is true
-> -- conversion errors; remember the environment at the time we tried
+> -- conversion constraints; remember the environment at the time we tried
> [(Env Name, Indexed Name, Indexed Name)])
> type Level = Int
+Finishes up type checking by making a substitution from all the conversion
+constraints and applying it to the term and type.
+
+> doConversion :: Monad m =>
+> Raw -> Gamma Name ->
+> [(Env Name, Indexed Name, Indexed Name)] ->
+> Indexed Name -> Indexed Name ->
+> m (Indexed Name, Indexed Name)
+> doConversion raw gam constraints (Ind tm) (Ind ty) =
+> -- trace ("Finishing checking " ++ show tm) $ -- ++ " with " ++ show 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 (subst, nms) <- mkSubst $ (map (\x -> (False,x)) constraints) ++
+> (map (\x -> (True,x)) constraints)
+> let tm' = papp subst tm
+> let ty' = papp subst ty
+> return {- $ trace (show nms ++ "\n" ++ show (tm',ty')) -} (Ind tm',Ind ty')
+
+> where mkSubst [] = return (P, [])
+> mkSubst ((ok, (env,Ind x,Ind y)):xs)
+> = do (s',nms) <- mkSubst xs
+> let x' = papp s' x
+> let y' = papp s' y
+> uns <- case unifyenvErr ok gam env (Ind x') (Ind y') of
+> Success x' -> return x'
+> Failure err -> {- trace ("XXX: " ++ err ++ show (x',y')) $ return [] -} fail err -- $ "Can't convert "++show x++" and "++show y ++ " ("++show err++")"
+> 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'
+
> check :: Monad m => Gamma Name -> Env Name -> Raw -> Maybe (Indexed Name) ->
> m (Indexed Name, Indexed Name)
> check gam env tm mty = do
-> (tm', _) <- lvlcheck 0 False 0 gam env tm mty
-> return tm'
+> ((tm', ty'), (_,_,_,convs)) <- lvlcheck 0 False 0 gam env tm mty
+> tm'' <- doConversion tm gam convs tm' ty'
+> return tm''
> checkAndBind :: Monad m => Gamma Name -> Env Name -> Raw ->
> Maybe (Indexed Name) ->
> m (Indexed Name, Indexed Name, Env Name)
> checkAndBind gam env tm mty = do
-> ((v,t), (_,_,e,_)) <- lvlcheck 0 True 0 gam env tm mty
-> return (v,t,e)
+> ((v,t), (_,_,e,convs)) <- lvlcheck 0 True 0 gam env tm mty
+> (v',ty') <- doConversion tm gam convs v t
+> return (v',ty',e)
Check two things together, with the same environment and variable inference,
@@ -95,8 +157,9 @@ We need this for checking pattern clauses...
> let realNames = mkNames next
> e' <- fixupB gam realNames e
> (v1', t1') <- fixupGam gam realNames (v1, t1)
-> ((v2,t2), (_, _, e'', _)) <- {- trace ("Checking " ++ show tm2 ++ " has type " ++ show t1') $ -} lvlcheck 0 inf next gam e' tm2 (Just t1')
-> return (v1',t1',v2,t2,e'')
+> ((v2,t2), (_, _, e'', bs')) <- {- trace ("Checking " ++ show tm2 ++ " has type " ++ show t1') $ -} lvlcheck 0 inf next gam e' tm2 (Just t1')
+> (v2',t2') <- doConversion tm2 gam bs' v2 (normalise gam t2)
+> return (v1',t1',v2',t2',e'')
> where mkNames 0 = []
> mkNames n
> = ([],Ind (P (MN ("INFER",n-1))),
@@ -127,7 +190,7 @@ Do the typechecking, then unify all the inferred terms.
> -- Then fill in any remained inferred values we got by knowing the
> -- expected type
> (next, infer, bindings, errs) <- get
-> tm' <- fixup errs tm
+> tm <- fixup errs tm
> bindings <- fixupB gamma errs bindings
> put (next, infer, bindings, errs)
> return tm'
@@ -147,8 +210,13 @@ typechecker...
> tc :: Monad m => Env Name -> Level -> Raw -> Maybe (Indexed Name) ->
> StateT CheckState m (Indexed Name, Indexed Name)
-> tc env lvl (Var n) exp =
-> mkTT (lookupi n env 0) (glookup n gamma)
+> 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 $ "Type error"
+> 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)
@@ -178,19 +246,26 @@ typechecker...
> (Ind fv, Ind ft) <- tcfixup env lvl f Nothing
> let fnfng = normaliseEnv env (Gam []) (Ind ft)
> let fnf = normaliseEnv env gamma (Ind ft)
-> case (fnfng,fnf) of
-> ((Ind (Bind _ (B Pi s) (Sc t))),_) -> do
+> (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))
> checkConvSt env gamma (Ind at) (Ind s) $ "Type error: " ++ show a ++ " : " ++ show at ++ ", expected type "++show s -- ++" "++show env
> let tt = (Bind (MN ("x",0)) (B (Let av) at) (Sc t))
> let tmty = (normaliseEnv env (Gam []) (Ind tt))
> return (Ind (App fv av), tmty)
-> (_, (Ind (Bind _ (B Pi s) (Sc t)))) -> do
+> (_, (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) $ "Type error: " ++ show a ++ " : " ++ show at ++ ", expected type "++show s -- ++" "++show env
> 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
+> _ -> 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 $ "Type error"
+> return (rv,rt)
> tc env lvl (RConst x) _ = tcConst x
> tc env lvl RStar _ = return (Ind Star, Ind Star)
@@ -412,7 +487,7 @@ extended environment.
> fixupGam gamma ((env,x,y):xs) (Ind tm, Ind ty) = do
> uns <- case unifyenv gamma env y x of
> Success x' -> return x'
-> Failure err -> fail $ "Can't convert "++show x++" and "++show y ++ " ("++show err++")"
+> Failure 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')
Oops, something went wrong.

0 comments on commit 14f22b0

Please sign in to comment.