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

effects/Effects.idr+3

compare with master

unifiedsplit

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

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

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

166

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+

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

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

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

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

169eff env (prog `ebind` c) k

172eff env (prog `ebind` c) k

lib/Data/SortedMap.idr+1−1

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

232

233instance Functor (SortedMap k) where

234 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

40 transitive = NatLTEIsTransitive

41 reflexive = NatLTEIsReflexive

42

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

44NatLTEIsAntisymmetric n n nEqn nEqn = refl

45NatLTEIsAntisymmetric n n nEqn nEqn = refl

45NatLTEIsAntisymmetric n m nEqn (nLTESm _) impossible

46NatLTEIsAntisymmetric n m nEqn (nLTESm _) impossible

46NatLTEIsAntisymmetric n m (nLTESm _) nEqn impossible

47NatLTEIsAntisymmetric n m (nLTESm _) nEqn impossible

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

47

49

48instance Poset Nat NatLTE where

50instance Poset Nat NatLTE where

49 antisymmetric = NatLTEIsAntisymmetric

51 antisymmetric = NatLTEIsAntisymmetric

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

74 decide = decideNatLTE

76 decide = decideNatLTE

75

77

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

78lte : (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 =

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

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

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

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

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

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

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

167−-- ++ show (pterm ps)

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

168-- ++ "\n----------") $

169 case fails of

170-- [] -> return u

src/Core/Unify.hs+21−10

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

54

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

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

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

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

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

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

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

60 injective _ = False

61

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

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

134

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

136+ | (injective fx && injective fy)

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

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

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

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

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

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

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

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

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

140 let (heady, _) = unApply fy

142 let (heady, _) = unApply fy

141 -- fail quickly if the heads are disjoint

143 -- fail quickly if the heads are disjoint

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

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

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

158 sc 1

160 sc 1

159 combine bnames hf ha)

161 combine bnames hf ha)

160− | otherwise =

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

161 do let (headx, argsx) = unApply appx

163 do let (headx, argsx) = unApply appx

162 let (heady, argsy) = unApply appy

164 let (heady, argsy) = unApply appy

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

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

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

191 unArgs vs xs ys

193 unArgs vs xs ys

192

194

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

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

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

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

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

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

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

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

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

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

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

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

199

201

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

202+ sameArgStruct appx appy

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

201− (_, ay) = unApply appy in

204+ (_, ay) = unApply appy in

205+ length ax == length ay &&

202− and (zipWith sameStruct ax ay)

206+ and (zipWith sameStruct ax ay)

203

207

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

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

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

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

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

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

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

218 sameStruct _ _ = False

222 sameStruct _ _ = False

219

223

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+

220 metavar t = case t of

231 metavar t = case t of

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

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

222 not (x `elem` dont)

233 not (x `elem` dont)

src/Idris/ElabTerm.hs+2

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

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

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

448 -- elaborate case

449+ env <- get_env

450+ g <- goal

449 updateAux (newdef : )

451 updateAux (newdef : )

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

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

451 movelast tyn

453 movelast tyn

src/Pkg/Package.hs+1

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

69

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

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

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

72 idris (map Filename f ++ opts)

73 idris (map Filename f ++ opts)

73 return ()

74 return ()

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

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

test/reg011/reg011.idr+1−2

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

4-- vfoldl P cons nil []

5-- = nil

6vfoldl P cons nil (x :: xs)

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

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

8−%logging 0

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

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

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

9-- = 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