# avsm/Ivor

Fixed a unification bug and added eta to equality test on terms

Ignore-this: 4eb72737b1f296457c8d7d9580eff42

darcs-hash:20100211205059-228f4-3264f338ecd584dda495aebc8c395bbd4acefe3d.gz
1 parent 579239a commit 30d87904d3ead9262b855fe1e3fea038d3d0b0f3 eb committed Feb 11, 2010
Showing with 29 additions and 9 deletions.
1. +6 −0 Ivor/TTCore.lhs
2. +19 −6 Ivor/Tactics.lhs
3. +2 −1 Ivor/Typecheck.lhs
4. +2 −2 Ivor/Unify.lhs
 @@ -677,6 +677,12 @@ Apply a function to a list of arguments > (==) (Elim x) (Elim y) = x==y > (==) (App f a) (App f' a') = f==f' && a==a' > (==) (Bind _ b sc) (Bind _ b' sc') = b==b' && sc==sc' + +Eta equality: + +> (==) (Bind x (B Lambda ty) (Sc (App t (V 0)))) t' = t == t' +> (==) t' (Bind x (B Lambda ty) (Sc (App t (V 0)))) = t == t' + > (==) (Proj _ i x) (Proj _ j y) = i==j && x==y > (==) (Const x) (Const y) = case cast x of > Just x' -> x'==y
 @@ -263,19 +263,32 @@ 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 + +Get the names and types of the arguments to be passed to the thing +we're refining by. + > let claimTypes = getClaims (makePsEnv (map fst env) nty) > let rawapp = mkapp rtm (map (\_ -> RInfer) claimTypes) + +Normalise the goal. + > let (Ind tyin') = finalise (normaliseEnv (ptovenv env) gam (Ind ty)) + +Type check the application we've just built, with the placeholders, some of +which may have been solved. + > (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 argguesses = -- trace (show rawapp ++ "\n" ++ show tyin' ++ "\n" ++ show rtch ++ "\n" ++ show rtych ++ "\nNew env: " ++ show ev) \$ +> 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 +> (tm',_) <- doClaims x claimGuesses gam env tm > let guess = (mkGuess claimGuesses [] (forget bvin)) -> (filled, unified) <- runtacticEnv gam env x tm' -> (fill guess) +> (filled, unified) <- runtacticEnv gam env x tm' (fill guess) > -- (filled, solved) <- solveUnified [] unified filled > -- filled <- tryDefaults defaults claims filled > -- (tm', _) <- trace (show claims) \$ tidy gam env filled
 @@ -113,7 +113,7 @@ constraints and applying it to the term and type. > 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") \$ +> -- 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... @@ -179,6 +179,7 @@ Handy to pass through all the variables, for tracing purposes when debugging. > 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)
 @@ -42,8 +42,8 @@ Unify on named terms, but normalise using de Bruijn indices. > {- trace (show (x,y) ++ "\n" ++ > show (p (normalise (gam' gam) x)) ++ "\n" ++ > show (p (normalise (gam' gam) x))) \$-} -> case unifynferr i env (p x) -> (p y) of +> case unifynferr False env (p x) +> (p y) of > (Right x) -> return x > _ -> {- trace (dbgtt x ++ ", " ++ dbgtt y ++"\n") \$ -}