2acbdf6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Small conversion change

commit2acbdf67d28d70ef47499cad19092978374d3676 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 13 Jan 2013, 22:44 (14 years ago) parent6be4eb2

3 files changed+9−8

compare with master

unifiedsplit

src/Core/Evaluate.hs+1−1 src/Core/Typecheck.hs+6−5 src/Idris/ElabDecls.hs+2−2

src/Core/Evaluate.hs+1−1

@@ -552,7 +552,7 @@ convEq :: Context -> TT Name -> TT Name -> StateT UCs TC Bool

552552convEq ctxt = ceq [] where

553553 ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs TC Bool

554554 ceq ps (P xt x _) (P yt y _)

555− | (xt == yt && x ==y ) || (x, y) `elem` ps || (y,x) `elem` ps = return True

555+ | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True

556556 | otherwise = sameDefs ps x y

557557 ceq ps (V x) (V y) = return (x == y)

558558 ceq ps (Bind _ xb xs) (Bind _ yb ys)

src/Core/Typecheck.hs+6−5

@@ -28,11 +28,12 @@ convertsC ctxt env x y

2828

2929converts :: Context -> Env -> Term -> Term -> TC ()

3030converts ctxt env x y

31− = if x == y then return () else

32− if (finalise (normalise ctxt env x) ==

33− finalise (normalise ctxt env y))

34− then return ()

35− else tfail (CantConvert

31+ = case convEq' ctxt x y of

32+ OK _ -> return ()

33+ _ -> case convEq' ctxt (finalise (normalise ctxt env x))

34+ (finalise (normalise ctxt env y)) of

35+ OK _ -> return ()

36+ _ -> tfail (CantConvert

3637 (finalise (normalise ctxt env x))

3738 (finalise (normalise ctxt env y)) (errEnv env))

3839

src/Idris/ElabDecls.hs+2−2

@@ -566,7 +566,7 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

566566 logLvl 6 $ " ==> " ++ show crhsty ++ " against " ++ show clhsty

567567 case converts ctxt [] clhsty crhsty of

568568 OK _ -> return ()

569− Error _ -> ierror (At fc (CantUnify False clhsty crhsty (Msg "") [] 0))

569+ Error e -> ierror (At fc (CantUnify False clhsty crhsty e [] 0))

570570 i <- get

571571 checkInferred fc (delab' i crhs True) rhs

572572 return $ Right (clhs, crhs)

@@ -794,7 +794,7 @@ elabClass info syn doc fc constraints tn ps ds

794794 pibind [] x = x

795795 pibind ((n, ty): ns) x = PPi expl n ty (pibind ns x)

796796

797− mdec (UN n) = (UN ('!':n))

797+ mdec (UN n) = UN ('!':n)

798798 mdec (NS x n) = NS (mdec x) n

799799 mdec x = x

800800