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

git.iko.soy/Idris-dev

on master help sign in

Check definitions structurally as well as by name in conversion

392c225Edwin Brady15 years ago

src/Core/Evaluate.hs+51−1

compare with master

unifiedsplit

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

2 PatternGuards #-}

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

5− simplify, specialise, hnf,

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

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

7 Context, initContext, ctxtAlist, uconstraints, next_tvar,

8 addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl, addDatatype,

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

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

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

426

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+

427-- SPECIALISATION -----------------------------------------------------------

477-- SPECIALISATION -----------------------------------------------------------

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

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

429-- evaluator

479-- evaluator

src/Core/TT.hs−17

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

327 (==) _ Erased = True

328 (==) _ _ = False

329

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−

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

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

348

331

349isInjective :: TT n -> Bool

332isInjective :: TT n -> Bool

src/Core/Typecheck.hs+2−2

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

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

18convertsC ctxt env x y

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

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

20− (finalise (normalise ctxt env y))

20+ (finalise (normalise ctxt env y))

21 if c then return ()

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

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

src/Core/Unify.hs+3−1

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

1+{-# LANGUAGE PatternGuards #-}

1module Core.Unify(unify, Fails) where

3module Core.Unify(unify, Fails) where

3import Core.TT

5import Core.TT

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

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

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

96 combine bnames h1 h2

98 combine bnames h1 h2

97 un' fn bnames x y

99 un' fn bnames x y

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

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

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

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

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

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

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

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

src/Idris/Error.hs+1

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

56getErrLine str

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

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

59+ ([], _) -> 0

59 (num, _) -> read num

60 (num, _) -> read num

60 _ -> 0

61 _ -> 0