a7217f1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Tweak scoping rules in instance generation

Variable names in the instance head should be propagated as parameters to the methods, just like other parameters. Fixes #956

commita7217f1e4c3bbd8094fe5f9224ba57165e26ff60 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 6 Mar 2014, 11:47 (13 years ago) parent66ac8da

6 files changed+53−12

compare with master

unifiedsplit

idris.cabal+6 src/Idris/AbsSyntaxTree.hs+1−1 src/Idris/ElabDecls.hs+26−11 test/reg038/expected test/reg038/reg038.idr+17 test/reg038/run+3

idris.cabal+6

@@ -221,6 +221,12 @@ Extra-source-files:

221221 test/reg036/run

222222 test/reg036/*.idr

223223 test/reg036/expected

224+ test/reg037/run

225+ test/reg037/*.idr

226+ test/reg037/expected

227+ test/reg038/run

228+ test/reg038/*.idr

229+ test/reg038/expected

224230

225231 test/basic001/run

226232 test/basic001/*.idr

src/Idris/AbsSyntaxTree.hs+1−1

@@ -1323,7 +1323,7 @@ prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n im

13231323 where strName (UN n) = T.unpack n

13241324 strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n

13251325 | otherwise = strName n

1326− strName (MN i s) = T.unpack s

1326+ strName (MN i s) = T.unpack s

13271327 strName other = show other

13281328

13291329

src/Idris/ElabDecls.hs+26−11

@@ -76,12 +76,12 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

7676 ctxt <- getContext

7777 i <- getIState

7878

79− logLvl 1 $ show n ++ " pre-type " ++ showTmImpls ty'

79+ logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'

8080 ty' <- addUsingConstraints syn fc ty'

8181 ty' <- implicit syn n ty'

8282

8383 let ty = addImpl i ty'

84− logLvl 1 $ show n ++ " type " ++ showTmImpls ty

84+ logLvl 3 $ show n ++ " type " ++ showTmImpls ty

8585 ((tyT, defer, is), log) <-

8686 tclift $ elaborate ctxt n (TType (UVal 0)) []

8787 (errAt "type of " n (erun fc (build i info False [] n ty)))

@@ -656,7 +656,7 @@ elabProvider info syn fc what n ty tm

656656 rhs <- execute (mkApp (P Ref (sUN "run__provider") Erased)

657657 [Erased, e])

658658 let rhs' = normalise ctxt [] rhs

659− logLvl 1 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs

659+ logLvl 3 $ "Normalised " ++ show n ++ "'s RHS to " ++ show rhs

660660

661661 -- Extract the provided term or postulate from the type provider

662662 provided <- getProvided fc rhs'

@@ -667,14 +667,14 @@ elabProvider info syn fc what n ty tm

667667 do -- Finally add a top-level definition of the provided term

668668 elabType info syn "" [] fc [] n ty

669669 elabClauses info fc [] n [PClause fc n (PApp fc (PRef fc n) []) [] (delab i tm) []]

670− logLvl 1 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

670+ logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm

671671 | otherwise ->

672672 ierror . Msg $ "Attempted to provide a term where a postulate was expected."

673673 Postulate

674674 | what `elem` [ProvPostulate, ProvAny] ->

675675 do -- Add the postulate

676676 elabPostulate info syn "Provided postulate" fc [] n ty

677− logLvl 1 $ "Elaborated provided postulate " ++ show n

677+ logLvl 3 $ "Elaborated provided postulate " ++ show n

678678 | otherwise ->

679679 ierror . Msg $ "Attempted to provide a postulate where a term was expected."

680680

@@ -1165,7 +1165,7 @@ elabPE info fc caller r =

11651165 elabType info defaultSyntax "" [] fc opts newnm specTy

11661166 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats

11671167 elabClauses info fc opts newnm def

1168− logLvl 1 $ "Specialised " ++ show newnm)

1168+ logLvl 2 $ "Specialised " ++ show newnm)

11691169 -- if it doesn't work, just don't specialise. Could happen for lots

11701170 -- of valid reasons (e.g. local variables in scope which can't be

11711171 -- lifted out).

@@ -1419,7 +1419,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

14191419 -- Elaborate those with a type *before* RHS, those without *after*

14201420 let (wbefore, wafter) = sepBlocks wb

14211421

1422− logLvl 1 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter

1422+ logLvl 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter

14231423 mapM_ (elabDecl' EAll info) wbefore

14241424 -- Now build the RHS, using the type of the LHS as the goal.

14251425 i <- getIState -- new implicits from where block

@@ -1563,7 +1563,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

15631563 _ -> []

15641564 let params = getParamsInType i [] fn_is fn_ty

15651565 let lhs = propagateParams params fn_ty (addImplPat i (stripLinear i lhs_in))

1566− logLvl 1 ("LHS: " ++ show lhs)

1566+ logLvl 2 ("LHS: " ++ show lhs)

15671567 ((lhs', dlhs, []), _) <-

15681568 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

15691569 (errAt "left hand side of with in " fname

@@ -1921,7 +1921,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

19211921 -- get the implicit parameters that need passing through to the

19221922 -- where block

19231923 wparams <- mapM (\p -> case p of

1924− PApp _ _ args -> getWParams args

1924+ PApp _ _ args -> getWParams (map getTm args)

19251925 _ -> return []) ps

19261926 let pnames = map pname (concat (nub wparams))

19271927 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)

@@ -1947,9 +1947,24 @@ elabInstance info syn what fc cs n ps t expn ds = do

19471947 logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp True . mkTyDecl) mtys)

19481948 logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++

19491949 show (concat (nub wparams))

1950− let lhs = PRef fc iname

1950+

1951+ -- Bring variables in instance head into scope

1952+ ist <- getIState

1953+ let headVars = mapMaybe (\p -> case p of

1954+ PRef _ n ->

1955+ case lookupTy n (tt_ctxt ist) of

1956+ [] -> Just n

1957+ _ -> Nothing

1958+ _ -> Nothing) ps

1959+-- let lhs = PRef fc iname

1960+ let lhs = PApp fc (PRef fc iname)

1961+ (map (\n -> pimp n (PRef fc n) True) headVars)

19511962 let rhs = PApp fc (PRef fc (instanceName ci))

19521963 (map (pexp . mkMethApp) mtys)

1964+

1965+ logLvl 5 $ "Instance LHS " ++ show lhs

1966+ logLvl 5 $ "Instance RHS " ++ show rhs

1967+

19531968 let idecls = [PClauses fc [Dictionary] iname

19541969 [PClause fc iname lhs [] rhs wb]]

19551970 iLOG (show idecls)

@@ -2031,7 +2046,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

20312046

20322047 getWParams [] = return []

20332048 getWParams (p : ps)

2034− | PRef _ n <- getTm p

2049+ | PRef _ n <- p

20352050 = do ps' <- getWParams ps

20362051 ctxt <- getContext

20372052 case lookupP n ctxt of

test/reg038/expectednew file

No changes to the content.

test/reg038/reg038.idrnew file+17

@@ -0,0 +1,17 @@

1+class C t (f : t -> t) (r : t -> t -> Type) where

2+ g : (a : t) -> r (f a) (f a) -> r (f a) (f a)

4+data Foo : {t : Type} -> t -> t -> Type where

5+ MkFoo : {t : Type} -> {x : t} -> {y : t} -> Foo x y

7+instance C t f (Foo {t = t}) where

8+ g x = id

10+data Bar : {t1 : Type} -> {t2 : Type} -> t1 -> t2 -> Type where

11+ MkBar : {x : t1} -> Bar x x

12+

13+instance C s f (Bar {t1 = s} {t2 = s}) where

14+ g x = id

15+

16+instance C s f ((=) {A = s} {B = s}) where

17+ g x = id

test/reg038/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris --check reg038.idr

3+rm -f *.ibc