c2446fa · 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/Completion.hs−2

@@ -39,8 +39,6 @@ tactics = map fst tacticArgs

39-- | Convert a name into a string usable for completion. Filters out names

40-- that users probably don't want to see.

41nameString :: Name -> Maybe String

42−nameString (UN nm)

43− | not (tnull nm) && (thead nm == '@' || thead nm == '#') = Nothing

44nameString (UN n) = Just (str n)

42nameString (UN n) = Just (str n)

45nameString (NS n _) = nameString n

43nameString (NS n _) = nameString n

46nameString _ = Nothing

44nameString _ = Nothing

src/Idris/Core/TT.hs+1−2

@@ -598,8 +598,7 @@ mapCtxt = fmap . fmap

598

599-- |Return True if the argument 'Name' should be interpreted as the name of a

600-- typeclass.

601−tcname (UN xs) | T.null xs = False

601+tcname (UN xs) = False

602− | otherwise = T.head xs == '@'

603tcname (NS n _) = tcname n

602tcname (NS n _) = tcname n

604tcname (SN (InstanceN _ _)) = True

603tcname (SN (InstanceN _ _)) = True

605tcname (SN (MethodN _)) = True

604tcname (SN (MethodN _)) = True

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/Clause.hs+1−4

@@ -793,12 +793,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

793 mkLHSapp t = t

794

795 decorate (NS x ns)

796− = NS (SN (WhereN cnum fname x)) ns -- ++ [show cnum])

796+ = NS (SN (WhereN cnum fname x)) ns

797−-- = NS (UN ('#':show x)) (ns ++ [show cnum, show fname])

798 decorate x

797 decorate x

799 = SN (WhereN cnum fname x)

798 = SN (WhereN cnum fname x)

800−-- = NS (SN (WhereN cnum fname x)) [show cnum]

801−-- = NS (UN ('#':show x)) [show cnum, show fname]

802

799

803 sepBlocks bs = sepBlocks' [] bs where

800 sepBlocks bs = sepBlocks' [] bs where

804 sepBlocks' ns (d@(PTy _ _ _ _ _ n _ t) : bs)

801 sepBlocks' ns (d@(PTy _ _ _ _ _ n _ t) : bs)

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