fad1c1c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Warn when generating a setter for a record fails

...rather than failing (since it may just not work for dependent records)

commitfad1c1c03ee3a37f2c31d3dd8729ffa295b384eb authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 18 Oct 2012, 20:52 (14 years ago) parent6f54612

9 files changed+45−5

compare with master

unifiedsplit

CHANGELOG+7 src/Core/Unify.hs+4 src/Idris/ElabDecls.hs+13−3 test/README+4 test/mktest.pl+1−1 test/reg001/expected test/reg001/reg001.idr+11 test/reg001/run+4 test/runtest.pl+1−1

CHANGELOG+7

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

1+New in 0.9.5:

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

4+Internal changes:

6+* Several improvements and fixes to unification

18New in 0.9.4:

29-------------

310

src/Core/Unify.hs+4

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

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

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

123123 | 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

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

125129 = do h1 <- uB bnames bx by

126130 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

112112 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)

113113 let implBinds = getImplB id cty'

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

116117 where

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

118119

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

120121 isNonImp _ = Nothing

121122

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+

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

123133 = getImplB k sc

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

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

188198 []

189199 (PApp fc (PRef fc cn)

190200 (map pexp rhsArgs)) []

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

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

192202

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

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

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

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

391401 let rhs = addImplBound i (map fst newargs)

392402 (expandParams decorate newargs decls rhs_in)

393− logLvl 2 (showImp True rhs)

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

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

395405 logLvl 5 "STARTING CHECK"

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

test/README+4

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

1313011: record projection and update

1414012: various error regressions

1515013: 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");

1414

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

1616print 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";

1818

1919close(FOO);

2020

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

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

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

7+data Imp : Set where

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

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

test/runtest.pl+1−1

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

4040 opendir(DIR, ".");

4141 @list = readdir(DIR);

4242 foreach $file (@list) {

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

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

4444 push(@tests,$file);

4545 }

4646 }