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

git.iko.soy/Idris-dev

Fix let overloading bug with do blocks

commit09f2abd0cdcdde6d3ba574f6e1157073673761e2 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateMon 6 Feb 2012, 12:27 (15 years ago) parent0338d39

6 files changed+30−5

compare with master

unifiedsplit

CHANGELOG+5 idris.cabal+1−1 src/Core/CaseTree.hs+3−3 src/Core/Elaborate.hs+8 src/Core/Evaluate.hs+10−1 src/Idris/DSL.hs+3

CHANGELOG+5

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

1+New in 0.9.2:

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

4+* case expressions allowed in type signatures

16New in 0.9.1:

27-------------

idris.cabal+1−1

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

11Name: idris

2−Version: 0.9.1

2+Version: 0.9.2

33License: BSD3

44License-file: LICENSE

55Author: Edwin Brady

src/Core/CaseTree.hs+3−3

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

3838

3939namesUsed :: SC -> [Name]

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

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

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

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

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

4343 nu' ps _ = []

4444

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

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

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

4848

src/Core/Elaborate.hs+8

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

108108 b <- lift $ goalAtFocus (fst p)

109109 return (binderTy b)

110110

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+

111119-- typecheck locally

112120get_type :: Raw -> Elab' aux Type

113121get_type tm = do ctxt <- get_context

src/Core/Evaluate.hs+10−1

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

88 addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl, addDatatype,

99 addCasedef, addOperator,

1010 lookupTy, lookupP, lookupDef, lookupVal, lookupTotal,

11− lookupTyEnv, isConName,

11+ lookupTyEnv, isConName, isFnName,

1212 Value(..)) where

1313

1414import Debug.Trace

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

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

657657 _ -> return False

658658

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+

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

660669lookupP root n ctxt

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

src/Idris/DSL.hs+3

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

99import Core.TT

1010import Core.Evaluate

1111

12+import Debug.Trace

13+

1214desugar :: SyntaxInfo -> IState -> PTerm -> PTerm

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

1416 t' -- addImpl i t'

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

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

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

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

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

8588 v' i t = t

8689

8790 mkVar fc 0 = case index_first dsl of