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

git.iko.soy/Idris-dev

on master help sign in

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

8b96fc7Edwin Brady14 years ago

src/Core/Elaborate.hs+2−2

compare with master

unifiedsplit

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

471

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

473simple_app fun arg =

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

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

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

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

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

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

478 claim a RType

src/Core/ProofState.hs+6−3

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

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

156unify' ctxt env topx topy =

157 do ps <- get

158+ let dont = dontunify ps

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

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

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

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

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

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

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

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

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

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

162-- -- ++ show (pterm ps)

165-- -- ++ show (pterm ps)

163-- ++ "\n----------") $

166-- ++ "\n----------") $

src/Core/Unify.hs+13−9

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

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

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

32−unify ctxt env topx topy injtc holes =

32+unify ctxt env topx topy dont holes =

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

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

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

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

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

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

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

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

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

58− injective (App f a) = injective f

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

59 injective _ = False

60 injective _ = False

61 notP (P _ _ _) = False

62 notP (P _ _ _) = False

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

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

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

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

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

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

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

100− = unifyFail tx ty

101+ = unifyTmpFail tx ty

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

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

102− = unifyFail tx ty

103+ = unifyTmpFail tx ty

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

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

104 | holeIn env x || x `elem` holes

105 | holeIn env x || x `elem` holes

105 = do UI s f <- get

106 = do UI s f <- get

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

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

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

129

130

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

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

131− | injective fx && metavarApp appy

132+ | injective fx && metavarApp appy

132− || injective fy && metavarApp appx

133+ || injective fy && metavarApp appx

133 || injective fx && injective fy

134 || injective fx && injective fy

134 || fx == fy

135 || fx == fy

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

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

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

165 unArgs uf argsx argsy

166 unArgs uf argsx argsy

166 else unifyTmpFail appx appy

167 else unifyTmpFail appx appy

167 where hnormalise [] _ _ t = t

168 where hnormalise [] _ _ t = t

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

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

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

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

170 | x /= y = unifyFail appx appy

171 | x /= y = unifyFail appx appy

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

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

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

186

187

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

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

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

189 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

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

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

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

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

191

194

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

199 sameStruct _ _ = False

202 sameStruct _ _ = False

200

203

201 metavar t = case t of

204 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)

203 _ -> False

207 _ -> False

204 pat t = case t of

208 pat t = case t of

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

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

src/Idris/AbsSyntax.hs+1−1

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

352

353allImportDirs :: IState -> Idris [FilePath]

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

355− return ("." : optdirs)

355+ return ("." : reverse optdirs)

356

357impShow :: Idris Bool

358impShow = do i <- getIState

src/Idris/ElabTerm.hs+4−6

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

57 resolveTC 7 fn ist) ivs

58 probs <- get_probs

59 tm <- get_term

60+ ctxt <- get_context

60 case probs of

61 case probs of

61 [] -> return ()

62 [] -> return ()

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

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

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

125 g <- goal

126 g <- goal

126 tm <- get_term

127 tm <- get_term

127 ps <- get_probs

128 ps <- get_probs

129+ hs <- get_holes

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

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

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

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

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

130-- ++ "\nproblems " ++ show ps

133-- ++ "\nproblems " ++ show ps

131-- ++ "\n-----------\n") $

134-- ++ "\n-----------\n") $

132 elab' ina t'

135 elab' ina t'

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

205 trySeq' deferr (x : xs)

208 trySeq' deferr (x : xs)

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

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

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

210 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

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

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

213 = do ctxt <- get_context

212 = do ctxt <- get_context

214− env <- get_env

215 let defined = case lookupTy Nothing n ctxt of

213 let defined = case lookupTy Nothing n ctxt of

216 [] -> False

214 [] -> False

217 _ -> True

215 _ -> 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