b543b29 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow names to be attached to provisional definitions

lhs ?= {name} rhs -- generates a lemma called 'name' which makes the types of the lhs and rhs match. {name} is optional - a unique name is generated if it is absent.

commitb543b29fa8a03981c70e8a0a32512c44cfe01b4b authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 19 Jul 2013, 11:46 (13 years ago) parentf7c7a81

4 files changed+18−8

compare with master

unifiedsplit

CHANGELOG+4 src/Idris/DSL.hs+2 src/Idris/ElabTerm.hs+3−2 src/Idris/Parser.hs+9−6

CHANGELOG+4

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

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

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

66 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.

711* Added Data.HVect module

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

913* 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)

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

3838expandDo dsl (PHidden t) = PHidden (expandDo dsl t)

3939expandDo dsl (PReturn fc) = dsl_return dsl

40+expandDo dsl (PRewrite fc r t ty)

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

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

4143 where

4244 block b [DoExp fc tm] = tm

src/Idris/ElabTerm.hs+3−2

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

334334 _ -> n

335335

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

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

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

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

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

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

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

340341 solve

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

13801380

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

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

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

1384− return (addLet rhs)

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

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

1385+ return n)

1386+ rhs <- pExpr syn

1387+ return (addLet name rhs)

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

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

13871390 mkN (NS x n) = NS (mkN x) n

13881391 n' = mkN n

13891392

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

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

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

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

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

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

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

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

13941397

13951398pClause :: SyntaxInfo -> IParser PClause

13961399pClause syn