7bfa10c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Some unification fixes

commit7bfa10cca77cd3cb62f2bcc3305b8ec07ba405a1 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 14 Jun 2013, 20:27 (13 years ago) parentb62a2e4

11 files changed+45−17

compare with master

unifiedsplit

effects/Effects.idr+3 lib/Data/SortedMap.idr+1−1 lib/Decidable/Order.idr+4−2 src/Core/ProofState.hs+2−2 src/Core/Unify.hs+21−10 src/Idris/ElabTerm.hs+2 src/Pkg/Package.hs+1 test/reg011/reg011.idr+1−2 test/reg019/expected test/reg019/reg019.idr+7 test/reg019/run+3

effects/Effects.idr+3

@@ -164,6 +164,9 @@ execEff (val :: env) Here eff' k

164164execEff (val :: env) (There p) eff k

165165 = execEff env p eff (\env', v => k (val :: env') v)

166166

167+-- Q: Instead of m b, implement as StateT (Env m xs') m b, so that state

168+-- updates can be propagated even through failing computations?

169+

167170eff : Env m xs -> EffM m xs xs' a -> (Env m xs' -> a -> m b) -> m b

168171eff env (value x) k = k env x

169172eff env (prog `ebind` c) k

lib/Data/SortedMap.idr+1−1

@@ -232,4 +232,4 @@ instance Functor (Tree n k) where

232232

233233instance Functor (SortedMap k) where

234234 fmap _ Empty = Empty

235− fmap f (M _ t) = M _ (fmap f t)

235+ fmap f (M n t) = M _ (fmap f t)

lib/Decidable/Order.idr+4−2

@@ -40,10 +40,12 @@ instance Preorder Nat NatLTE where

4040 transitive = NatLTEIsTransitive

4141 reflexive = NatLTEIsReflexive

4242

43−total NatLTEIsAntisymmetric : (m : Nat) -> (n : Nat) -> po m n -> po n m -> m = n

43+total NatLTEIsAntisymmetric : (m : Nat) -> (n : Nat) ->

44+ NatLTE m n -> NatLTE n m -> m = n

4445NatLTEIsAntisymmetric n n nEqn nEqn = refl

4546NatLTEIsAntisymmetric n m nEqn (nLTESm _) impossible

4647NatLTEIsAntisymmetric n m (nLTESm _) nEqn impossible

48+NatLTEIsAntisymmetric n m (nLTESm _) (nLTESm _) impossible

4749

4850instance Poset Nat NatLTE where

4951 antisymmetric = NatLTEIsAntisymmetric

@@ -74,4 +76,4 @@ instance Decidable NatLTE where

7476 decide = decideNatLTE

7577

7678lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)

77−lte m n = decide {p = NatLTE} m n

79+lte m n = decide {p = NatLTE} m n

src/Core/ProofState.hs+2−2

@@ -161,10 +161,10 @@ unify' ctxt env topx topy =

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

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

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

164−-- -- " in " ++ show env ++

164+-- " in " ++ show env ++

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

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

167−-- ++ show (pterm ps)

167+-- -- ++ show (pterm ps)

168168-- ++ "\n----------") $

169169 case fails of

170170-- [] -> return u

src/Core/Unify.hs+21−10

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

5454

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

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

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

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

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

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

5959 injective (App f a) = injective f -- && injective a

6060 injective _ = False

6161

@@ -133,9 +133,11 @@ unify ctxt env topx topy dont holes =

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

134134

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

136− | (injective fx && sameArgStruct appx appy && metavarApp appy)

137− || (injective fy && sameArgStruct appx appy && metavarApp appx)

138− || (injective fx && injective fy)

136+ | (injective fx && injective fy)

137+ || (injective fx && rigid appx && metavarApp appy)

138+ || (injective fy && rigid appy && metavarApp appx)

139+ || (injective fx && metavarApp fy && ax == ay)

140+ || (injective fy && metavarApp fx && ax == ay)

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

140142 let (heady, _) = unApply fy

141143 -- fail quickly if the heads are disjoint

@@ -157,7 +159,7 @@ unify ctxt env topx topy dont holes =

157159 hf <- un' False bnames fx' fy'

158160 sc 1

159161 combine bnames hf ha)

160− | otherwise =

162+ | otherwise = -- trace (show (appx, appy, injective fx, metavarApp appy, sameArgStruct appx appy)) $

161163 do let (headx, argsx) = unApply appx

162164 let (heady, argsy) = unApply appy

163165 -- traceWhen (headx == heady) (show (appx, appy)) $

@@ -191,15 +193,17 @@ unify ctxt env topx topy dont holes =

191193 unArgs vs xs ys

192194

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

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

196+ all (\x -> metavar x) (f : args)

195197 metavarArgs tm = let (f, args) = unApply tm in

196198 all (\x -> metavar x || inenv x) args

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

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

199201

200− sameArgStruct appx appy = let (_, ax) = unApply appx

201− (_, ay) = unApply appy in

202− and (zipWith sameStruct ax ay)

202+ sameArgStruct appx appy

203+ = let (_, ax) = unApply appx

204+ (_, ay) = unApply appy in

205+ length ax == length ay &&

206+ and (zipWith sameStruct ax ay)

203207

204208 sameStruct fapp@(App f x) gapp@(App g y)

205209 = let (f',a') = unApply fapp

@@ -217,6 +221,13 @@ unify ctxt env topx topy dont holes =

217221 sameStruct (Bind n t sc) (Bind n' t' sc') = sameStruct sc sc'

218222 sameStruct _ _ = False

219223

224+ rigid (P (DCon _ _) _ _) = True

225+ rigid (P (TCon _ _) _ _) = True

226+ rigid t@(P Ref _ _) = inenv t

227+ rigid (Constant _) = True

228+ rigid (App f a) = rigid f && rigid a

229+ rigid t = not (metavar t)

230+

220231 metavar t = case t of

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

222233 not (x `elem` dont)

src/Idris/ElabTerm.hs+2

@@ -446,6 +446,8 @@ elab ist info pattern tcgen fn tm

446446 (caseBlock fc cname' (reverse args) opts)

447447 -- fail $ "Not implemented " ++ show c ++ "\n" ++ show args

448448 -- elaborate case

449+ env <- get_env

450+ g <- goal

449451 updateAux (newdef : )

450452 -- if we haven't got the type yet, hopefully we'll get it later!

451453 movelast tyn

src/Pkg/Package.hs+1

@@ -69,6 +69,7 @@ installPkg pkgdesc

6969

7070buildMods :: [Opt] -> [Name] -> IO ()

7171buildMods opts ns = do let f = map (toPath . show) ns

72+-- putStrLn $ "MODULE: " ++ show f

7273 idris (map Filename f ++ opts)

7374 return ()

7475 where toPath n = foldl1' (</>) $ splitOn "." n

test/reg011/reg011.idr+1−2

@@ -4,7 +4,6 @@ vfoldl : (P : Nat -> Type) ->

44-- vfoldl P cons nil []

55-- = nil

66vfoldl P cons nil (x :: xs)

7− = vfoldl (\n => P (S n)) (\ n => cons (S n)) (cons O nil x) xs

8−%logging 0

7+ = vfoldl (\k => P (S k)) (\ n => cons (S n)) (cons O nil x) xs

98-- vfoldl P cons nil (x :: xs)

109-- = vfoldl (\n => P (S n)) (\ n => cons _) (cons _ nil x) xs

test/reg019/expectednew file

No changes to the content.

test/reg019/reg019.idrnew file+7

@@ -0,0 +1,7 @@

1+m_add : Maybe (Either Bool Int) -> Maybe (Either Bool Int) ->

2+ Maybe (Either Bool Int)

3+m_add x y = do x' <- x -- Extract value from x

4+ y' <- y -- Extract value from y

5+ case x' of

6+ Left _ => Nothing

7+ Right _ => Nothing

test/reg019/runnew file+3

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

1+#!/bin/bash

2+idris $@ reg019.idr --check

3+rm -f *.ibc