b543b29 · Idris-dev · git.iko.soy

CHANGELOG+4

compare with master

unifiedsplit

@@ -4,6 +4,10 @@ New in 0.9.9:

4* Apply functions by return type, rather than with arguments:

5 "t <== f" means "apply f with arguments such that it returns a value

6 of type t"

7+* Allow names to be attached to provisional definitions

8+ lhs ?= {name} rhs -- generates a lemma called 'name' which makes the

9+ types of the lhs and rhs match. {name} is optional - a unique name is

10+ generated if it is absent.

7* Added Data.HVect module

11* Added Data.HVect module

8* Fix fromInteger to take an Integer, rather than an Int

12* Fix fromInteger to take an Integer, rather than an Int

9* Integer literals for Fin

13* Integer literals for Fin

src/Idris/DSL.hs+2

@@ -37,6 +37,8 @@ expandDo dsl (PDPair fc l t r) = PDPair fc (expandDo dsl l) (expandDo dsl t)

37expandDo dsl (PAlternative a as) = PAlternative a (map (expandDo dsl) as)

38expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

39expandDo dsl (PReturn fc) = dsl_return dsl

40+expandDo dsl (PRewrite fc r t ty)

41+ = PRewrite fc r (expandDo dsl t) ty

40expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds

42expandDo dsl (PDoBlock ds) = expandDo dsl $ block (dsl_bind dsl) ds

41 where

43 where

42 block b [DoExp fc tm] = tm

44 block b [DoExp fc tm] = tm

src/Idris/ElabTerm.hs+3−2

@@ -334,8 +334,9 @@ elab ist info pattern tcgen fn tm

334 _ -> n

335

336 elab' (ina, g) (PMatchApp fc fn)

337− = do let (fn', imps) = case lookupCtxtName fn (idris_implicits ist) of

337+ = do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of

338− [(n, args)] -> (n, map (const True) args)

338+ [(n, args)] -> return (n, map (const True) args)

339+ _ -> lift $ tfail (NoSuchVariable fn)

339 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)

340 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)

340 solve

341 solve

341 -- if f is local, just do a simple_app

342 -- if f is local, just do a simple_app

src/Idris/Parser.hs+9−6

@@ -1380,17 +1380,20 @@ pArgExpr syn = let syn' = syn { inPattern = True } in

1380

1381pRHS :: SyntaxInfo -> Name -> IParser PTerm

1382pRHS syn n = do lchar '='; pExpr syn

1383+ <|> do symbol "?=";

1384+ name <- option n' (do symbol "{"; n <- pfName; symbol "}";

1385+ return n)

1383− <|> do symbol "?="; rhs <- pExpr syn;

1386+ rhs <- pExpr syn

1384− return (addLet rhs)

1387+ return (addLet name rhs)

1385 <|> do reserved "impossible"; return PImpossible

1388 <|> do reserved "impossible"; return PImpossible

1386 where mkN (UN x) = UN (x++"_lemma_1")

1389 where mkN (UN x) = UN (x++"_lemma_1")

1387 mkN (NS x n) = NS (mkN x) n

1390 mkN (NS x n) = NS (mkN x) n

1388 n' = mkN n

1391 n' = mkN n

1389

1392

1390− addLet (PLet n ty val rhs) = PLet n ty val (addLet rhs)

1393+ addLet nm (PLet n ty val rhs) = PLet n ty val (addLet nm rhs)

1391− addLet (PCase fc t cs) = PCase fc t (map addLetC cs)

1394+ addLet nm (PCase fc t cs) = PCase fc t (map addLetC cs)

1392− where addLetC (l, r) = (l, addLet r)

1395+ where addLetC (l, r) = (l, addLet nm r)

1393− addLet rhs = (PLet (UN "value") Placeholder rhs (PMetavar n'))

1396+ addLet nm rhs = (PLet (UN "value") Placeholder rhs (PMetavar nm))

1394

1397

1395pClause :: SyntaxInfo -> IParser PClause

1398pClause :: SyntaxInfo -> IParser PClause

1396pClause syn

1399pClause syn