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

git.iko.soy/Idris-dev

Use ParentN for its intended purpose

commit22792d2f27519cc95f22b6af071d4866fb10b883 authorMelvar Chen <Melvar.Chen@googlemail.com> dateThu 26 May 2016, 22:27 (10 years ago) parent83ef000

5 files changed+4−15

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+2−3 src/Idris/Elab/Class.hs+1−2 src/Idris/Elab/Instance.hs+1−1 src/Idris/IdrisDoc.hs−1 src/Idris/ProofSearch.hs−8

src/Idris/AbsSyntax.hs+2−3

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

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

440440-- resolved by default.

441441--

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

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

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

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

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

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

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

462462 | otherwise = n : insI i ns

463463

464− chaser (UN nm)

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

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

466465 chaser (NS n _) = chaser n

467466 chaser _ = False

468467

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

237237 -- Generate a function for chasing a dictionary constraint

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

239239 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)))

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

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

244243 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

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

259259

260260 findOverlapping i dets t n

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

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

262262 | otherwise

263263 = case lookupTy n (tt_ctxt i) of

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

src/Idris/IdrisDoc.hs−1

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

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

181181filterName :: Name -- ^ Name to check

182182 -> Bool -- ^ Predicate result

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

184183filterName (UN _) = True

185184filterName (NS n _) = filterName n

186185filterName _ = False

src/Idris/ProofSearch.hs−8

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

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

452452 notHole _ _ = True

453453

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−

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

463455

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