22792d2 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+2−3

compare with master

unifiedsplit

@@ -439,7 +439,7 @@ pop_estack = do i <- getIState

439-- Dodgy hack 1: Put integer instances first in the list so they are

440-- resolved by default.

441--

442−-- Dodgy hack 2: put constraint chasers (@@) last

442+-- Dodgy hack 2: put constraint chasers (ParentN) last

443addInstance :: Bool -- ^ whether the name is an Integer instance

444 -> Bool -- ^ whether to include the instance in instance search

445 -> Name -- ^ the name of the class

@@ -461,8 +461,7 @@ addInstance int res n i

461 insI i (n : ns) | chaser (fst n) = (i, res) : n : ns

462 | otherwise = n : insI i ns

463

464− chaser (UN nm)

464+ chaser (SN (ParentN _ _)) = True

465− | ('@':'@':_) <- str nm = True

466 chaser (NS n _) = chaser n

465 chaser (NS n _) = chaser n

467 chaser _ = False

466 chaser _ = False

468

467

src/Idris/Elab/Class.hs+1−2

@@ -237,8 +237,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

237 -- Generate a function for chasing a dictionary constraint

238 cfun :: Name -> PTerm -> SyntaxInfo -> [a] -> (Name, PTerm) -> Idris [PDecl' PTerm]

239 cfun cn c syn all (cnm, con)

240− = do let cfn = sUN ('@':'@':show cn ++ "#" ++ show con)

241− -- SN (ParentN cn (show con))

240+ = do let cfn = SN (ParentN cn (txt (show con)))

242 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

241 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

243 let capp = PApp fc (PRef fc [] cn) (map (pexp . PRef fc []) mnames)

242 let capp = PApp fc (PRef fc [] cn) (map (pexp . PRef fc []) mnames)

244 let lhs = PApp fc (PRef fc [] cfn) [pconst capp]

243 let lhs = PApp fc (PRef fc [] cfn) [pconst capp]

src/Idris/Elab/Instance.hs+1−1

@@ -258,7 +258,7 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

258 return $ any (isJust . findOverlapping i (class_determiners ci) (delab i nty)) (map fst $ class_instances ci)

259

260 findOverlapping i dets t n

261− | take 2 (show n) == "@@" = Nothing

261+ | SN (ParentN _ _) <- n = Nothing

262 | otherwise

263 = case lookupTy n (tt_ctxt i) of

264 [t'] -> let tret = getRetType t

src/Idris/IdrisDoc.hs−1

@@ -180,7 +180,6 @@ removeOrphans list =

180-- | Whether a Name names something which should be documented

181filterName :: Name -- ^ Name to check

182 -> Bool -- ^ Predicate result

183−filterName (UN n) | '@':'@':_ <- str n = False

184filterName (UN _) = True

183filterName (UN _) = True

185filterName (NS n _) = filterName n

184filterName (NS n _) = filterName n

186filterName _ = False

185filterName _ = False

src/Idris/ProofSearch.hs−8

@@ -451,14 +451,6 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist

451 | Constant _ <- c = not (n `elem` hs)

452 notHole _ _ = True

453

454− -- HACK! Rather than giving a special name, better to have some kind

455− -- of flag in ClassInfo structure

456− chaser (UN nm)

457− | ('@':'@':_) <- str nm = True -- old way

458− chaser (SN (ParentN _ _)) = True

459− chaser (NS n _) = chaser n

460− chaser _ = False

461−

462 numclass = sNS (sUN "Num") ["Interfaces","Prelude"]

454 numclass = sNS (sUN "Num") ["Interfaces","Prelude"]

463

455

464 addDefault t num@(P _ nc _) [P Bound a _] | nc == numclass && defaultOn

456 addDefault t num@(P _ nc _) [P Bound a _] | nc == numclass && defaultOn