From 30d87904d3ead9262b855fe1e3fea038d3d0b0f3 Mon Sep 17 00:00:00 2001
From: eb <eb@cs.st-andrews.ac.uk>
Date: Thu, 11 Feb 2010 20:50:59 +0000
Subject: [PATCH] Fixed a unification bug and added eta to equality test on
 terms

Ignore-this: 4eb72737b1f296457c8d7d9580eff42

darcs-hash:20100211205059-228f4-3264f338ecd584dda495aebc8c395bbd4acefe3d.gz
---
 Ivor/TTCore.lhs    |  6 ++++++
 Ivor/Tactics.lhs   | 25 +++++++++++++++++++------
 Ivor/Typecheck.lhs |  3 ++-
 Ivor/Unify.lhs     |  4 ++--
 4 files changed, 29 insertions(+), 9 deletions(-)

diff --git a/Ivor/TTCore.lhs b/Ivor/TTCore.lhs
index fc7f84b..b5325b1 100644
--- a/Ivor/TTCore.lhs
+++ b/Ivor/TTCore.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
diff --git a/Ivor/Tactics.lhs b/Ivor/Tactics.lhs
index d780f44..d2df452 100644
--- a/Ivor/Tactics.lhs
+++ b/Ivor/Tactics.lhs
@@ -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
diff --git a/Ivor/Typecheck.lhs b/Ivor/Typecheck.lhs
index 8c76ae9..1785f8e 100644
--- a/Ivor/Typecheck.lhs
+++ b/Ivor/Typecheck.lhs
@@ -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)
 
diff --git a/Ivor/Unify.lhs b/Ivor/Unify.lhs
index bbebb6c..25be825 100644
--- a/Ivor/Unify.lhs
+++ b/Ivor/Unify.lhs
@@ -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") $ -}