8b96fc7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix another unification problem (solving things which shouldn't be)

commit8b96fc781f4152d65f85f94aed20181d03e1290b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 17 Mar 2013, 01:10 (14 years ago) parent2686158

8 files changed+61−21

compare with master

unifiedsplit

src/Core/Elaborate.hs+2−2 src/Core/ProofState.hs+6−3 src/Core/Unify.hs+13−9 src/Idris/AbsSyntax.hs+1−1 src/Idris/ElabTerm.hs+4−6 test/reg012/expected test/reg012/reg012.lidr+32 test/reg012/run+3

src/Core/Elaborate.hs+2−2

@@ -471,8 +471,8 @@ apply_elab n args =

471471

472472simple_app :: Elab' aux () -> Elab' aux () -> Elab' aux ()

473473simple_app fun arg =

474− do a <- unique_hole (MN 0 "a")

475− b <- unique_hole (MN 0 "b")

474+ do a <- unique_hole (MN 0 "argTy")

475+ b <- unique_hole (MN 0 "retTy")

476476 f <- unique_hole (MN 0 "f")

477477 s <- unique_hole (MN 0 "s")

478478 claim a RType

src/Core/ProofState.hs+6−3

@@ -155,9 +155,12 @@ qshow fs = show (map (\ (x, y, _, _) -> (x, y)) fs)

155155unify' :: Context -> Env -> TT Name -> TT Name -> StateT TState TC [(Name, TT Name)]

156156unify' ctxt env topx topy =

157157 do ps <- get

158− (u, fails) <- lift $ unify ctxt env topx topy (injective ps) (holes ps)

159−-- trace ("Unified " ++ show (topx, topy) ++ " in " ++ show env ++

160−-- " " ++ show u ++ "\n" ++ qshow fails ++ "\nCurrent problems:\n"

158+ let dont = dontunify ps

159+ (u, fails) <- -- trace ("Trying " ++ show (topx, topy)) $

160+ lift $ unify ctxt env topx topy dont (holes ps)

161+-- trace ("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++

162+-- -- " in " ++ show env ++

163+-- "\n" ++ show u ++ "\n" ++ qshow fails ++ "\nCurrent problems:\n"

161164-- ++ qshow (problems ps) ++ "\n" ++ show (holes ps) ++ "\n"

162165-- -- ++ show (pterm ps)

163166-- ++ "\n----------") $

src/Core/Unify.hs+13−9

@@ -29,7 +29,7 @@ data UResult a = UOK a

2929

3030unify :: Context -> Env -> TT Name -> TT Name -> [Name] -> [Name] ->

3131 TC ([(Name, TT Name)], Fails)

32−unify ctxt env topx topy injtc holes =

32+unify ctxt env topx topy dont holes =

3333-- trace ("Unifying " ++ show (topx, topy)) $

3434 -- don't bother if topx and topy are different at the head

3535 case runStateT (un False [] topx topy) (UI 0 []) of

@@ -54,8 +54,9 @@ unify ctxt env topx topy injtc holes =

5454

5555 injective (P (DCon _ _) _ _) = True

5656 injective (P (TCon _ _) _ _) = True

57− injective (P _ n _) = n `elem` injtc

58− injective (App f a) = injective f

57+ injective (App f (P _ _ _)) = injective f

58+ injective (App f (Constant _)) = injective f

59+ injective (App f a) = injective f && injective a

5960 injective _ = False

6061

6162 notP (P _ _ _) = False

@@ -97,9 +98,9 @@ unify ctxt env topx topy injtc holes =

9798 un' fn bnames tx@(P _ x _) ty@(P _ y _)

9899 | (x,y) `elem` bnames || x == y = do sc 1; return []

99100 | injective tx && not (holeIn env y || y `elem` holes)

100− = unifyFail tx ty

101+ = unifyTmpFail tx ty

101102 | injective ty && not (holeIn env x || x `elem` holes)

102− = unifyFail tx ty

103+ = unifyTmpFail tx ty

103104 un' fn bnames xtm@(P _ x _) tm

104105 | holeIn env x || x `elem` holes

105106 = do UI s f <- get

@@ -128,8 +129,8 @@ unify ctxt env topx topy injtc holes =

128129 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

129130

130131 un' fn bnames appx@(App fx ax) appy@(App fy ay)

131− | injective fx && metavarApp appy

132− || injective fy && metavarApp appx

132+ | injective fx && metavarApp appy

133+ || injective fy && metavarApp appx

133134 || injective fx && injective fy

134135 || fx == fy

135136 = do let (headx, _) = unApply fx

@@ -165,7 +166,7 @@ unify ctxt env topx topy injtc holes =

165166 unArgs uf argsx argsy

166167 else unifyTmpFail appx appy

167168 where hnormalise [] _ _ t = t

168− hnormalise ns ctxt env t = hnf ctxt env t

169+ hnormalise ns ctxt env t = normalise ctxt env t

169170 checkHeads (P (DCon _ _) x _) (P (DCon _ _) y _)

170171 | x /= y = unifyFail appx appy

171172 checkHeads (P (TCon _ _) x _) (P (TCon _ _) y _)

@@ -186,6 +187,8 @@ unify ctxt env topx topy injtc holes =

186187

187188 metavarApp tm = let (f, args) = unApply tm in

188189 all (\x -> metavar x || inenv x) (f : args)

190+ metavarArgs tm = let (f, args) = unApply tm in

191+ all (\x -> metavar x || inenv x) args

189192 metavarApp' tm = let (f, args) = unApply tm in

190193 all (\x -> pat x || metavar x) (f : args)

191194

@@ -199,7 +202,8 @@ unify ctxt env topx topy injtc holes =

199202 sameStruct _ _ = False

200203

201204 metavar t = case t of

202− P _ x _ -> x `elem` holes || holeIn env x

205+ P _ x _ -> (x `elem` holes || holeIn env x) &&

206+ not (x `elem` dont)

203207 _ -> False

204208 pat t = case t of

205209 P _ x _ -> x `elem` holes || patIn env x

src/Idris/AbsSyntax.hs+1−1

@@ -352,7 +352,7 @@ setImportDirs fps = do i <- getIState

352352

353353allImportDirs :: IState -> Idris [FilePath]

354354allImportDirs i = do let optdirs = opt_importdirs (idris_options i)

355− return ("." : optdirs)

355+ return ("." : reverse optdirs)

356356

357357impShow :: Idris Bool

358358impShow = do i <- getIState

src/Idris/ElabTerm.hs+4−6

@@ -57,6 +57,7 @@ build ist info pattern fn tm

5757 resolveTC 7 fn ist) ivs

5858 probs <- get_probs

5959 tm <- get_term

60+ ctxt <- get_context

6061 case probs of

6162 [] -> return ()

6263 ((_,_,_,e):es) -> lift (Error e)

@@ -125,8 +126,10 @@ elab ist info pattern tcgen fn tm

125126 g <- goal

126127 tm <- get_term

127128 ps <- get_probs

129+ hs <- get_holes

128130-- trace ("Elaborating " ++ show t' ++ " in " ++ show g

129−-- ++ "\n" ++ show tm

131+-- -- ++ "\n" ++ show tm

132+-- ++ "\nholes " ++ show hs

130133-- ++ "\nproblems " ++ show ps

131134-- ++ "\n-----------\n") $

132135 elab' ina t'

@@ -205,13 +208,8 @@ elab ist info pattern tcgen fn tm

205208 trySeq' deferr (x : xs)

206209 = try' (elab' ina x) (trySeq' deferr xs) True

207210 elab' ina (PPatvar fc n) | pattern = patvar n

208−-- = do env <- get_env

209−-- case lookup n env of

210−-- Just (PVar _) -> elab' ina Placeholder

211−-- _ -> patvar n

212211 elab' (ina, guarded) (PRef fc n) | pattern && not (inparamBlock n)

213212 = do ctxt <- get_context

214− env <- get_env

215213 let defined = case lookupTy Nothing n ctxt of

216214 [] -> False

217215 _ -> True

test/reg012/expectednew file

No changes to the content.

test/reg012/reg012.lidrnew file+32

@@ -0,0 +1,32 @@

1+> total soElim : (C : (b : Bool) -> so b -> Type) ->

2+> C True oh ->

3+> (b : Bool) -> (s : so b) -> (C b s)

4+> soElim C coh .True .oh = coh

6+> soFalseElim : so False -> a

7+> soFalseElim x = FalseElim (soElim C () False x)

8+> where

9+> C : (b : Bool) -> so b -> Type

10+> C True s = ()

11+> C False s = _|_

12+

13+> soTrue : so b -> b = True

14+> soTrue {b = False} x = soFalseElim x

15+> soTrue {b = True} x = refl

16+

17+> class Eq alpha => ReflEqEq alpha where

18+> reflexive_eqeq : (a : alpha) -> so (a == a)

19+

20+> modifyFun : (Eq alpha) =>

21+> (alpha -> beta) ->

22+> (alpha, beta) ->

23+> (alpha -> beta)

24+> modifyFun f (a, b) a' = if a' == a then b else f a'

25+

26+> modifyFunLemma : (ReflEqEq alpha) =>

27+> (f : alpha -> beta) ->

28+> (ab : (alpha, beta)) ->

29+> modifyFun f ab (fst ab) = snd ab

30+> modifyFunLemma f (a,b) =

31+> replace {P = \ z => boolElim (a == a) b (f a) = boolElim z b (f a)}

32+> (soTrue (reflexive_eqeq a)) refl

test/reg012/runnew file+3

@@ -0,0 +1,3 @@

1+#!/bin/bash

2+idris $@ reg012.lidr --check

3+rm -f reg012 *.ibc