392c225 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Check definitions structurally as well as by name in conversion

commit392c225ce46fc43d433b4418de459ba01c985dda authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 28 Jan 2012, 09:25 (15 years ago) parent21c3a30

5 files changed+57−21

compare with master

unifiedsplit

src/Core/Evaluate.hs+51−1 src/Core/TT.hs−17 src/Core/Typecheck.hs+2−2 src/Core/Unify.hs+3−1 src/Idris/Error.hs+1

src/Core/Evaluate.hs+51−1

@@ -2,7 +2,7 @@

22 PatternGuards #-}

44module Core.Evaluate(normalise, normaliseC, normaliseAll,

5− simplify, specialise, hnf,

5+ simplify, specialise, hnf, convEq, convEq',

66 Def(..), Accessibility(..), Totality(..), PReason(..),

77 Context, initContext, ctxtAlist, uconstraints, next_tvar,

88 addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl, addDatatype,

@@ -424,6 +424,56 @@ eval_hnf ctxt statics genv tm = ev [] tm where

424424 getValArgs (HApp t env args) = (t, env, args)

425425 getValArgs t = (t, [], [])

426426

427+convEq' ctxt x y = evalStateT (convEq ctxt x y) (0, [])

428+

429+convEq :: Context -> TT Name -> TT Name -> StateT UCs TC Bool

430+convEq ctxt = ceq [] where

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

432+ ceq ps (P xt x _) (P yt y _)

433+ | (xt == yt && x ==y ) || (x, y) `elem` ps || (y,x) `elem` ps = return True

434+ | otherwise = sameDefs ps x y

435+ ceq ps (V x) (V y) = return (x == y)

436+ ceq ps (Bind _ xb xs) (Bind _ yb ys)

437+ = liftM2 (&&) (ceqB ps xb yb) (ceq ps xs ys)

438+ where

439+ ceqB ps (Let v t) (Let v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

440+ ceqB ps (Guess v t) (Guess v' t') = liftM2 (&&) (ceq ps v v') (ceq ps t t')

441+ ceqB ps b b' = ceq ps (binderTy b) (binderTy b')

442+ ceq ps (App fx ax) (App fy ay) = liftM2 (&&) (ceq ps fx fy) (ceq ps ax ay)

443+ ceq ps (Constant x) (Constant y) = return (x == y)

444+ ceq ps (Set x) (Set y) = do (v, cs) <- get

445+ put (v, ULE x y : cs)

446+ return True

447+ ceq ps Erased _ = return True

448+ ceq ps _ Erased = return True

449+ ceq ps _ _ = return False

450+

451+ caseeq ps (Case n cs) (Case n' cs') = caseeqA ((n,n'):ps) cs cs'

452+ where

453+ caseeqA ps (ConCase x i as sc : rest) (ConCase x' i' as' sc' : rest')

454+ = do q1 <- caseeq (zip as as' ++ ps) sc sc'

455+ q2 <- caseeqA ps rest rest'

456+ return $ x == x' && i == i' && q1 && q2

457+ caseeqA ps (ConstCase x sc : rest) (ConstCase x' sc' : rest')

458+ = do q1 <- caseeq ps sc sc'

459+ q2 <- caseeqA ps rest rest'

460+ return $ x == x' && q1 && q2

461+ caseeqA ps (DefaultCase sc : rest) (DefaultCase sc' : rest')

462+ = liftM2 (&&) (caseeq ps sc sc') (caseeqA ps rest rest')

463+ caseeqA ps [] [] = return True

464+ caseeqA ps _ _ = return False

465+ caseeq ps (STerm x) (STerm y) = ceq ps x y

466+ caseeq ps (UnmatchedCase _) (UnmatchedCase _) = return True

467+ caseeq ps _ _ = return False

468+

469+ sameDefs ps x y = case (lookupDef Nothing x ctxt, lookupDef Nothing y ctxt) of

470+ ([Function _ xdef], [Function _ ydef])

471+ -> ceq ((x,y):ps) xdef ydef

472+ ([CaseOp _ _ _ _ xdef _ _],

473+ [CaseOp _ _ _ _ ydef _ _])

474+ -> caseeq ((x,y):ps) xdef ydef

475+ _ -> return False

476+

427477-- SPECIALISATION -----------------------------------------------------------

428478-- We need too much control to be able to do this by tweaking the main

429479-- evaluator

src/Core/TT.hs−17

@@ -327,23 +327,6 @@ instance Eq n => Eq (TT n) where

327327 (==) _ Erased = True

328328 (==) _ _ = False

329329

330−convEq :: Eq n => TT n -> TT n -> StateT UCs TC Bool

331−convEq (P xt x _) (P yt y _) = return (xt == yt && x == y)

332−convEq (V x) (V y) = return (x == y)

333−convEq (Bind _ xb xs) (Bind _ yb ys)

334− = liftM2 (&&) (convEqB xb yb) (convEq xs ys)

335− where convEqB (Let v t) (Let v' t') = liftM2 (&&) (convEq v v') (convEq t t')

336− convEqB (Guess v t) (Guess v' t') = liftM2 (&&) (convEq v v') (convEq t t')

337− convEqB b b' = convEq (binderTy b) (binderTy b')

338−convEq (App fx ax) (App fy ay) = liftM2 (&&) (convEq fx fy) (convEq ax ay)

339−convEq (Constant x) (Constant y) = return (x == y)

340−convEq (Set x) (Set y) = do (v, cs) <- get

341− put (v, ULE x y : cs)

342− return True

343−convEq Erased _ = return True

344−convEq _ Erased = return True

345−convEq _ _ = return False

346−

347330-- A few handy operations on well typed terms:

348331

349332isInjective :: TT n -> Bool

src/Core/Typecheck.hs+2−2

@@ -16,8 +16,8 @@ import Core.Evaluate

1616

1717convertsC :: Context -> Env -> Term -> Term -> StateT UCs TC ()

1818convertsC ctxt env x y

19− = do c <- convEq (finalise (normalise ctxt env x))

20− (finalise (normalise ctxt env y))

19+ = do c <- convEq ctxt (finalise (normalise ctxt env x))

20+ (finalise (normalise ctxt env y))

2121 if c then return ()

2222 else fail ("Can't convert between " ++

2323 showEnv env (finalise (normalise ctxt env x)) ++ " and " ++

src/Core/Unify.hs+3−1

@@ -1,3 +1,5 @@

1+{-# LANGUAGE PatternGuards #-}

13module Core.Unify(unify, Fails) where

35import Core.TT

@@ -95,7 +97,7 @@ unify ctxt env topx topy

9597 h2 <- un' False ((x,y):bnames) sx sy

9698 combine bnames h1 h2

9799 un' fn bnames x y

98− | x == y = do sc 1; return []

100+ | OK True <- convEq' ctxt x y = do sc 1; return []

99101 | otherwise = do UI s i f <- get

100102 let err = CantUnify topx topy (CantUnify x y (Msg "") s) s

101103 put (UI s i ((x, y, env, err) : f))

src/Idris/Error.hs+1

@@ -56,6 +56,7 @@ tclift tc = case tc of

5656getErrLine str

5757 = case span (/=':') str of

5858 (_, ':':rest) -> case span isDigit rest of

59+ ([], _) -> 0

5960 (num, _) -> read num

6061 _ -> 0

6162