09f2abd · Idris-dev · git.iko.soy

CHANGELOG+5

compare with master

unifiedsplit

@@ -1,3 +1,8 @@

1+New in 0.9.2:

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

3+

4+* case expressions allowed in type signatures

5+

1New in 0.9.1:

6New in 0.9.1:

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

7-------------

3

8

idris.cabal+1−1

@@ -1,5 +1,5 @@

1Name: idris

2−Version: 0.9.1

2+Version: 0.9.2

3License: BSD3

4License-file: LICENSE

5Author: Edwin Brady

src/Core/CaseTree.hs+3−3

@@ -38,11 +38,11 @@ small _ = False

38

39namesUsed :: SC -> [Name]

40namesUsed sc = nub $ nu' [] sc where

41− nu' ps (Case n alts) = concatMap (nua ps) alts

41+ nu' ps (Case n alts) = nub (concatMap (nua ps) alts) \\ [n]

42− nu' ps (STerm t) = nut ps t

42+ nu' ps (STerm t) = nub $ nut ps t

43 nu' ps _ = []

44

45− nua ps (ConCase n i args sc) = nu' (ps ++ args) sc

45+ nua ps (ConCase n i args sc) = nub (nu' (ps ++ args) sc) \\ args

46 nua ps (ConstCase _ sc) = nu' ps sc

47 nua ps (DefaultCase sc) = nu' ps sc

48

src/Core/Elaborate.hs+8

@@ -108,6 +108,14 @@ goal = do ES p _ _ <- get

108 b <- lift $ goalAtFocus (fst p)

109 return (binderTy b)

110

111+-- Get the guess at the current hole, if there is one

112+get_guess :: Elab' aux Type

113+get_guess = do ES p _ _ <- get

114+ b <- lift $ goalAtFocus (fst p)

115+ case b of

116+ Guess t v -> return v

117+ _ -> fail "Not a guess"

118+

111-- typecheck locally

119-- typecheck locally

112get_type :: Raw -> Elab' aux Type

120get_type :: Raw -> Elab' aux Type

113get_type tm = do ctxt <- get_context

121get_type tm = do ctxt <- get_context

src/Core/Evaluate.hs+10−1

@@ -8,7 +8,7 @@ module Core.Evaluate(normalise, normaliseC, normaliseAll,

8 addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl, addDatatype,

9 addCasedef, addOperator,

10 lookupTy, lookupP, lookupDef, lookupVal, lookupTotal,

11− lookupTyEnv, isConName,

11+ lookupTyEnv, isConName, isFnName,

12 Value(..)) where

13

14import Debug.Trace

@@ -656,6 +656,15 @@ isConName root n ctxt

656 (TyDecl (TCon _ _) _) -> return True

657 _ -> return False

658

659+isFnName :: Maybe [String] -> Name -> Context -> Bool

660+isFnName root n ctxt

661+ = or $ do def <- lookupCtxt root n (definitions ctxt)

662+ case tfst def of

663+ (Function _ _) -> return True

664+ (Operator _ _ _) -> return True

665+ (CaseOp _ _ _ _ _ _ _) -> return True

666+ _ -> return False

667+

659lookupP :: Maybe [String] -> Name -> Context -> [Term]

668lookupP :: Maybe [String] -> Name -> Context -> [Term]

660lookupP root n ctxt

669lookupP root n ctxt

661 = do def <- lookupCtxt root n (definitions ctxt)

670 = do def <- lookupCtxt root n (definitions ctxt)

src/Idris/DSL.hs+3

@@ -9,6 +9,8 @@ import Core.CoreParser

9import Core.TT

10import Core.Evaluate

11

12+import Debug.Trace

13+

12desugar :: SyntaxInfo -> IState -> PTerm -> PTerm

14desugar :: SyntaxInfo -> IState -> PTerm -> PTerm

13desugar syn i t = let t' = expandDo (dsl_info syn) t in

15desugar syn i t = let t' = expandDo (dsl_info syn) t in

14 t' -- addImpl i t'

16 t' -- addImpl i t'

@@ -82,6 +84,7 @@ var dsl n t i = v' i t where

82 v' i (PAlternative as) = PAlternative $ map (v' i) as

84 v' i (PAlternative as) = PAlternative $ map (v' i) as

83 v' i (PHidden t) = PHidden (v' i t)

85 v' i (PHidden t) = PHidden (v' i t)

84 v' i (PIdiom f t) = PIdiom f (v' i t)

86 v' i (PIdiom f t) = PIdiom f (v' i t)

87+ v' i (PDoBlock ds) = PDoBlock (map (fmap (v' i)) ds)

85 v' i t = t

88 v' i t = t

86

89

87 mkVar fc 0 = case index_first dsl of

90 mkVar fc 0 = case index_first dsl of