git.iko.soy/Idris-dev
on master help sign in
Fix pattern name bug where name is already a CAF
commitd6c53d957c9aed2c244e163ad8924e73ddf9b314 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 3 Jan 2012, 11:03 (15 years ago) parent310ca03
3 files changed+20−14
compare with master
unifiedsplit
src/Core/Elaborate.hs+7−5 src/Core/Evaluate.hs+9−1 src/Idris/ElabTerm.hs+4−8
src/Core/Elaborate.hs+7−5
@@ -198,11 +198,13 @@ rewrite :: Raw -> Elab ()
198198rewrite tm = processTactic' (Rewrite tm)
199199
200200patvar :: Name -> Elab ()
201−patvar n = do n' <- case n of
202− UN _ -> return n
203− MN _ _ -> unique_hole n
204− NS _ _ -> return n
205− processTactic' (PatVar n')
201+patvar n = do env <- get_env
202+ if (n `elem` map fst env) then do apply (Var n) []; solve
203+ else do n' <- case n of
204+ UN _ -> return n
205+ MN _ _ -> unique_hole n
206+ NS _ _ -> return n
207+ processTactic' (PatVar n')
206208
207209patbind :: Name -> Elab ()
208210patbind n = processTactic' (PatBind n)
src/Core/Evaluate.hs+9−1
@@ -7,7 +7,7 @@ module Core.Evaluate(normalise, normaliseC, normaliseAll,
77 Context, initContext, ctxtAlist, uconstraints, next_tvar,
88 addToCtxt, setAccess, addCtxtDef, addTyDecl, addDatatype,
99 addCasedef, addOperator,
10− lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,
10+ lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv, isConName,
1111 Value(..)) where
1212
1313import Debug.Trace
@@ -540,6 +540,14 @@ lookupTy root n ctxt
540540 (Operator ty _ _) -> return ty
541541 (CaseOp _ ty _ _ _) -> return ty
542542
543+isConName :: Maybe [String] -> Name -> Context -> Bool
544+isConName root n ctxt
545+ = or $ do def <- lookupCtxt root n (definitions ctxt)
546+ case fst def of
547+ (TyDecl (DCon _ _) _) -> return True
548+ (TyDecl (TCon _ _) _) -> return True
549+ _ -> return False
550+
543551lookupP :: Maybe [String] -> Name -> Context -> [Term]
544552lookupP root n ctxt
545553 = do def <- lookupCtxt root n (definitions ctxt)
src/Idris/ElabTerm.hs+4−8
@@ -119,14 +119,10 @@ elab ist info pattern tcgen fn tm
119119 showHd x = show x
120120 elab' ina (PRef fc n) | pattern && not (inparamBlock n)
121121 = do ctxt <- get_context
122− let sc = case lookupTy Nothing n ctxt of
123− [] -> True
124− _ -> False
125− if sc
126− then erun fc $
127− try (do apply (Var n) []; solve)
128− (patvar n)
129− else do apply (Var n) []; solve
122+ let iscon = isConName Nothing n ctxt
123+ if (not iscon && ina) then erun fc $ patvar n
124+ else try (do apply (Var n) []; solve)
125+ (patvar n)
130126 where inparamBlock n = case lookupCtxtName Nothing n (inblock info) of
131127 [] -> False
132128 _ -> True