d6c53d9 · Idris-dev · git.iko.soy

src/Core/Elaborate.hs+7−5

compare with master

unifiedsplit

@@ -198,11 +198,13 @@ rewrite :: Raw -> Elab ()

198rewrite tm = processTactic' (Rewrite tm)

199

200patvar :: Name -> Elab ()

201+patvar n = do env <- get_env

202+ if (n `elem` map fst env) then do apply (Var n) []; solve

201−patvar n = do n' <- case n of

203+ else do n' <- case n of

202− UN _ -> return n

204+ UN _ -> return n

203− MN _ _ -> unique_hole n

205+ MN _ _ -> unique_hole n

204− NS _ _ -> return n

206+ NS _ _ -> return n

205− processTactic' (PatVar n')

207+ processTactic' (PatVar n')

206

208

207patbind :: Name -> Elab ()

209patbind :: Name -> Elab ()

208patbind n = processTactic' (PatBind n)

210patbind n = processTactic' (PatBind n)

src/Core/Evaluate.hs+9−1

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

7 Context, initContext, ctxtAlist, uconstraints, next_tvar,

8 addToCtxt, setAccess, addCtxtDef, addTyDecl, addDatatype,

9 addCasedef, addOperator,

10− lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,

10+ lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv, isConName,

11 Value(..)) where

12

13import Debug.Trace

@@ -540,6 +540,14 @@ lookupTy root n ctxt

540 (Operator ty _ _) -> return ty

541 (CaseOp _ ty _ _ _) -> return ty

542

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+

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

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

544lookupP root n ctxt

552lookupP root n ctxt

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

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

src/Idris/ElabTerm.hs+4−8

@@ -119,14 +119,10 @@ elab ist info pattern tcgen fn tm

119 showHd x = show x

120 elab' ina (PRef fc n) | pattern && not (inparamBlock n)

121 = do ctxt <- get_context

122− let sc = case lookupTy Nothing n ctxt of

122+ let iscon = isConName Nothing n ctxt

123− [] -> True

124− _ -> False

125− if sc

126− then erun fc $

123+ if (not iscon && ina) then erun fc $ patvar n

127− try (do apply (Var n) []; solve)

124+ else try (do apply (Var n) []; solve)

128− (patvar n)

125+ (patvar n)

129− else do apply (Var n) []; solve

130 where inparamBlock n = case lookupCtxtName Nothing n (inblock info) of

126 where inparamBlock n = case lookupCtxtName Nothing n (inblock info) of

131 [] -> False

127 [] -> False

132 _ -> True

128 _ -> True