fad1c1c · Idris-dev · git.iko.soy

CHANGELOG+7

compare with master

unifiedsplit

@@ -1,3 +1,10 @@

1+New in 0.9.5:

2+-------------

3+

4+Internal changes:

5+

6+* Several improvements and fixes to unification

7+

1New in 0.9.4:

8New in 0.9.4:

2-------------

9-------------

3

10

src/Core/Unify.hs+4

@@ -121,6 +121,10 @@ unify ctxt env topx topy

121 | n == n' = un' False bnames x y

122 un' fn bnames (Bind n (Lam t) (App x (P Bound n' _))) y

123 | n == n' = un' False bnames x y

124+-- un' fn bnames (Bind x (PVar _) sx) (Bind y (PVar _) sy)

125+-- = un' False ((x,y):bnames) sx sy

126+-- un' fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)

127+-- = un' False ((x,y):bnames) sx sy

124 un' fn bnames (Bind x bx sx) (Bind y by sy)

128 un' fn bnames (Bind x bx sx) (Bind y by sy)

125 = do h1 <- uB bnames bx by

129 = do h1 <- uB bnames bx by

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

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

src/Idris/ElabDecls.hs+13−3

@@ -112,13 +112,23 @@ elabRecord info syn fc tyn ty cn cty

112 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)

113 let implBinds = getImplB id cty'

114 update_decls <- mapM (mkUpdate recty implBinds (length nonImp)) (zip nonImp [0..])

115− mapM_ (elabDecl info) (concat (proj_decls ++ update_decls))

115+ mapM_ (elabDecl info) (concat proj_decls)

116+ mapM_ (tryElabDecl info) (update_decls)

116 where

117 where

117-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }

118-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }

118

119

119 isNonImp (PExp _ _ _, a) = Just a

120 isNonImp (PExp _ _ _, a) = Just a

120 isNonImp _ = Nothing

121 isNonImp _ = Nothing

121

122

123+ tryElabDecl info (fn, ty, val)

124+ = do i <- get

125+ idrisCatch (do elabDecl' info ty

126+ elabDecl' info val)

127+ (\v -> do iputStrLn $ show fc ++

128+ ":Warning - can't generate setter for " ++

129+ show fn ++ " (" ++ show ty ++ ")"

130+ put i)

131+

122 getImplB k (PPi (Imp l s) n Placeholder sc)

132 getImplB k (PPi (Imp l s) n Placeholder sc)

123 = getImplB k sc

133 = getImplB k sc

124 getImplB k (PPi (Imp l s) n ty sc)

134 getImplB k (PPi (Imp l s) n ty sc)

@@ -188,7 +198,7 @@ elabRecord info syn fc tyn ty cn cty

188 []

198 []

189 (PApp fc (PRef fc cn)

199 (PApp fc (PRef fc cn)

190 (map pexp rhsArgs)) []

200 (map pexp rhsArgs)) []

191− return [pfnTy, PClauses fc [] setname [pclause]]

201+ return (pn, pfnTy, PClauses fc [] setname [pclause])

192

202

193elabCon :: ElabInfo -> SyntaxInfo -> Name -> (Name, PTerm, FC) -> Idris (Name, Type)

203elabCon :: ElabInfo -> SyntaxInfo -> Name -> (Name, PTerm, FC) -> Idris (Name, Type)

194elabCon info syn tn (n, t_in, fc)

204elabCon info syn tn (n, t_in, fc)

@@ -390,7 +400,7 @@ elabClause info tcgen (PClause fc fname lhs_in withs rhs_in whereblock)

390 logLvl 5 (showImp True (expandParams decorate newargs decls rhs_in))

400 logLvl 5 (showImp True (expandParams decorate newargs decls rhs_in))

391 let rhs = addImplBound i (map fst newargs)

401 let rhs = addImplBound i (map fst newargs)

392 (expandParams decorate newargs decls rhs_in)

402 (expandParams decorate newargs decls rhs_in)

393− logLvl 2 (showImp True rhs)

403+ logLvl 2 $ "RHS: " ++ showImp True rhs

394 ctxt <- getContext -- new context with where block added

404 ctxt <- getContext -- new context with where block added

395 logLvl 5 "STARTING CHECK"

405 logLvl 5 "STARTING CHECK"

396 ((rhs', defer, is), _) <-

406 ((rhs', defer, is), _) <-

test/README+4

@@ -13,3 +13,7 @@ Tests:

13011: record projection and update

14012: various error regressions

15013: binding syntax

16+014: resource DSL

17+015: verified binary adder

18+

19+regxxx: various regression tests

test/mktest.pl+1−1

@@ -14,7 +14,7 @@ open(FOO,">run");

14

15print FOO "#!/bin/bash\n";

16print FOO "idris $test.idr -o $test\n";

17−print FOO "./$test\n";print FOO "rm -f $test $test.ibc\n";

17+print FOO "./$test\n";print FOO "rm -f $test *.ibc\n";

18

19close(FOO);

20

test/reg001/expectednew file

No changes to the content.

test/reg001/reg001.idrnew file+11

@@ -0,0 +1,11 @@

1+apply : (a -> b) -> a -> b

2+apply f x = f x

3+

4+class Functor f => VerifiedFunctor (f : Set -> Set) where

5+ identity : (fa : f a) -> fmap id fa = fa

6+

7+data Imp : Set where

8+ MkImp : {any : Set} -> any -> Imp

9+

10+testVal : Imp

11+testVal = MkImp (apply id O)

test/reg001/runnew file+4

@@ -0,0 +1,4 @@

1+#!/bin/bash

2+idris reg001.idr --check

3+rm -rf reg001.ibc

4+

test/runtest.pl+1−1

@@ -40,7 +40,7 @@ if ($#ARGV>=0) {

40 opendir(DIR, ".");

41 @list = readdir(DIR);

42 foreach $file (@list) {

43− if ($file =~ /^test/) {

43+ if ($file =~ /[0-9][0-9][0-9]/) {

44 push(@tests,$file);

45 }

46 }