c2446fa · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #3196 from Melvar/instate-parentn

Use ParentN for its intended purpose

commitc2446fafc951492781126e4f8a0e096b807dcd31 authorEdwin Brady <edwin.brady@gmail.com> dateFri 3 Jun 2016, 16:54 (10 years ago) parentc70672d c6f1061

8 files changed+6−23

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+2−3 src/Idris/Completion.hs−2 src/Idris/Core/TT.hs+1−2 src/Idris/Elab/Class.hs+1−2 src/Idris/Elab/Clause.hs+1−4 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/Completion.hs−2

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

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

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

4141nameString :: Name -> Maybe String

42−nameString (UN nm)

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

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

4543nameString (NS n _) = nameString n

4644nameString _ = Nothing

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

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

598598

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

600600-- typeclass.

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

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

601+tcname (UN xs) = False

603602tcname (NS n _) = tcname n

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

605604tcname (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

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

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

793793 mkLHSapp t = t

794794

795795 decorate (NS x ns)

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

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

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

798797 decorate x

799798 = SN (WhereN cnum fname x)

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

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

802799

803800 sepBlocks bs = sepBlocks' [] bs where

804801 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

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