Permalink
Browse files

Fix let overloading bug with do blocks

  • Loading branch information...
1 parent 0338d39 commit 09f2abd0cdcdde6d3ba574f6e1157073673761e2 Edwin Brady committed Feb 6, 2012
Showing with 30 additions and 5 deletions.
  1. +5 −0 CHANGELOG
  2. +1 −1 idris.cabal
  3. +3 −3 src/Core/CaseTree.hs
  4. +8 −0 src/Core/Elaborate.hs
  5. +10 −1 src/Core/Evaluate.hs
  6. +3 −0 src/Idris/DSL.hs
View
@@ -1,3 +1,8 @@
+New in 0.9.2:
+-------------
+
+* case expressions allowed in type signatures
+
New in 0.9.1:
-------------
View
@@ -1,5 +1,5 @@
Name: idris
-Version: 0.9.1
+Version: 0.9.2
License: BSD3
License-file: LICENSE
Author: Edwin Brady
@@ -38,11 +38,11 @@ small _ = False
namesUsed :: SC -> [Name]
namesUsed sc = nub $ nu' [] sc where
- nu' ps (Case n alts) = concatMap (nua ps) alts
- nu' ps (STerm t) = nut ps t
+ nu' ps (Case n alts) = nub (concatMap (nua ps) alts) \\ [n]
+ nu' ps (STerm t) = nub $ nut ps t
nu' ps _ = []
- nua ps (ConCase n i args sc) = nu' (ps ++ args) sc
+ nua ps (ConCase n i args sc) = nub (nu' (ps ++ args) sc) \\ args
nua ps (ConstCase _ sc) = nu' ps sc
nua ps (DefaultCase sc) = nu' ps sc
@@ -108,6 +108,14 @@ goal = do ES p _ _ <- get
b <- lift $ goalAtFocus (fst p)
return (binderTy b)
+-- Get the guess at the current hole, if there is one
+get_guess :: Elab' aux Type
+get_guess = do ES p _ _ <- get
+ b <- lift $ goalAtFocus (fst p)
+ case b of
+ Guess t v -> return v
+ _ -> fail "Not a guess"
+
-- typecheck locally
get_type :: Raw -> Elab' aux Type
get_type tm = do ctxt <- get_context
View
@@ -8,7 +8,7 @@ module Core.Evaluate(normalise, normaliseC, normaliseAll,
addToCtxt, setAccess, setTotal, addCtxtDef, addTyDecl, addDatatype,
addCasedef, addOperator,
lookupTy, lookupP, lookupDef, lookupVal, lookupTotal,
- lookupTyEnv, isConName,
+ lookupTyEnv, isConName, isFnName,
Value(..)) where
import Debug.Trace
@@ -656,6 +656,15 @@ isConName root n ctxt
(TyDecl (TCon _ _) _) -> return True
_ -> return False
+isFnName :: Maybe [String] -> Name -> Context -> Bool
+isFnName root n ctxt
+ = or $ do def <- lookupCtxt root n (definitions ctxt)
+ case tfst def of
+ (Function _ _) -> return True
+ (Operator _ _ _) -> return True
+ (CaseOp _ _ _ _ _ _ _) -> return True
+ _ -> return False
+
lookupP :: Maybe [String] -> Name -> Context -> [Term]
lookupP root n ctxt
= do def <- lookupCtxt root n (definitions ctxt)
View
@@ -9,6 +9,8 @@ import Core.CoreParser
import Core.TT
import Core.Evaluate
+import Debug.Trace
+
desugar :: SyntaxInfo -> IState -> PTerm -> PTerm
desugar syn i t = let t' = expandDo (dsl_info syn) t in
t' -- addImpl i t'
@@ -82,6 +84,7 @@ var dsl n t i = v' i t where
v' i (PAlternative as) = PAlternative $ map (v' i) as
v' i (PHidden t) = PHidden (v' i t)
v' i (PIdiom f t) = PIdiom f (v' i t)
+ v' i (PDoBlock ds) = PDoBlock (map (fmap (v' i)) ds)
v' i t = t
mkVar fc 0 = case index_first dsl of

0 comments on commit 09f2abd

Please sign in to comment.