06edf43 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add implicit lambdas for top level implicits

They shouldn't really be treated differently from scoped implicits during elaboration... Fixes #1536

commit06edf43977da02a5642e147dddb1ee4a4b6d7b14 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 18 Oct 2015, 23:08 (11 years ago) parentc7bed76

11 files changed+27−17

compare with master

unifiedsplit

Makefile+1−1 src/Idris/AbsSyntax.hs+7−3 src/Idris/AbsSyntaxTree.hs+3−3 src/Idris/Core/Binary.hs+3−2 src/Idris/Core/DeepSeq.hs+1−1 src/Idris/Core/TT.hs+1−1 src/Idris/Delaborate.hs+3 src/Idris/Elab/Term.hs+2−2 src/Idris/IBC.hs+1−1 src/Idris/ParseExpr.hs+3−3 src/Idris/REPL.hs+2

Makefile+1−1

@@ -43,7 +43,7 @@ relib: lib_clean

4343 $(CABAL) install $(CABALFLAGS)

4444

4545linecount:

46− wc -l src/Idris/*.hs src/Idris/Core/*.hs src/IRTS/*.hs src/Pkg/*.hs

46+ wc -l src/Idris/*.hs src/Idris/Elab/*.hs src/Idris/Core/*.hs src/IRTS/*.hs src/Pkg/*.hs src/Util/*.hs

4747

4848#Note: this doesn't yet link to Hackage properly

4949doc: dist/setup-config

src/Idris/AbsSyntax.hs+7−3

@@ -1393,7 +1393,11 @@ getUnboundImplicits i t tm = getImps t (collectImps tm)

13931393 = (n, (p, t)) : collectImps sc

13941394 collectImps _ = []

13951395

1396− getImps (Bind n (Pi (Just _) _ _) sc) imps = getImps sc imps

1396+ scopedimpl (Just i) = not (toplevel_imp i)

1397+ scopedimpl _ = False

1398+

1399+ getImps (Bind n (Pi i _ _) sc) imps

1400+ | scopedimpl i = getImps sc imps

13971401 getImps (Bind n (Pi _ t _) sc) imps

13981402 | Just (p, t') <- lookup n imps = argInfo n p t' : getImps sc imps

13991403 where

@@ -1556,9 +1560,9 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

15561560 pibind using [] sc = sc

15571561 pibind using (n:ns) sc

15581562 = case lookup n using of

1559− Just ty -> PPi (Imp [] Dynamic False Nothing)

1563+ Just ty -> PPi (Imp [] Dynamic False (Just (Impl False True)))

15601564 n NoFC ty (pibind using ns sc)

1561− Nothing -> PPi (Imp [InaccessibleArg] Dynamic False Nothing)

1565+ Nothing -> PPi (Imp [InaccessibleArg] Dynamic False (Just (Impl False True)))

15621566 n NoFC Placeholder (pibind using ns sc)

15631567

15641568-- Add implicit arguments in function calls

src/Idris/AbsSyntaxTree.hs+3−3

@@ -587,9 +587,9 @@ is_scoped :: Plicity -> Maybe ImplicitInfo

587587is_scoped (Imp _ _ _ s) = s

588588is_scoped _ = Nothing

589589

590−impl = Imp [] Dynamic False Nothing

591−forall_imp = Imp [] Dynamic False (Just (Impl False))

592−forall_constraint = Imp [] Dynamic False (Just (Impl True))

590+impl = Imp [] Dynamic False (Just (Impl False True))

591+forall_imp = Imp [] Dynamic False (Just (Impl False False))

592+forall_constraint = Imp [] Dynamic False (Just (Impl True False))

593593expl = Exp [] Dynamic False

594594expl_param = Exp [] Dynamic True

595595constraint = Constraint [] Static

src/Idris/Core/Binary.hs+3−2

@@ -484,10 +484,11 @@ instance Binary Raw where

484484instance Binary ImplicitInfo where

485485 put x

486486 = case x of

487− Impl x1 -> put x1

487+ Impl x1 x2 -> do put x1; put x2

488488 get

489489 = do x1 <- get

490− return (Impl x1)

490+ x2 <- get

491+ return (Impl x1 x2)

491492

492493instance (Binary b) => Binary (Binder b) where

493494 put x

src/Idris/Core/DeepSeq.hs+1−1

@@ -167,7 +167,7 @@ instance NFData ErrorReportPart where

167167 rnf (SubReport x1) = rnf x1 `seq` ()

168168

169169instance NFData ImplicitInfo where

170− rnf (Impl x1) = rnf x1 `seq` ()

170+ rnf (Impl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

171171

172172instance (NFData b) => NFData (Binder b) where

173173 rnf (Lam x1) = rnf x1 `seq` ()

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

@@ -811,7 +811,7 @@ deriving instance Binary Raw

811811deriving instance NFData Raw

812812!-}

813813

814−data ImplicitInfo = Impl { tcinstance :: Bool }

814+data ImplicitInfo = Impl { tcinstance :: Bool, toplevel_imp :: Bool }

815815 deriving (Show, Eq, Ord, Data, Typeable)

816816

817817{-!

src/Idris/Delaborate.hs+3

@@ -110,6 +110,9 @@ delabTy' ist imps tm fullname mvs = de [] imps tm

110110 _ -> PRef un [] n

111111 de env _ (Bind n (Lam ty) sc)

112112 = PLam un n NoFC (de env [] ty) (de ((n,n):env) [] sc)

113+ de env (_ : is) (Bind n (Pi (Just impl) ty _) sc)

114+ | toplevel_imp impl -- information in 'imps' repeated

115+ = PPi (Imp [] Dynamic False (Just impl)) n NoFC (de env [] ty) (de ((n,n):env) is sc)

113116 de env is (Bind n (Pi (Just impl) ty _) sc)

114117 | tcinstance impl

115118 = PPi constraint n NoFC (de env [] ty) (de ((n,n):env) is sc)

src/Idris/Elab/Term.hs+2−2

@@ -1415,9 +1415,9 @@ elab ist info emode opts fn tm

14151415 notImplicitable _ = False

14161416

14171417 insertScopedImps fc (Bind n (Pi im@(Just i) _ _) sc) xs

1418− | tcinstance i

1418+ | tcinstance i && not (toplevel_imp i)

14191419 = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs

1420− | otherwise

1420+ | not (toplevel_imp i)

14211421 = pimp n Placeholder True : insertScopedImps fc sc xs

14221422 insertScopedImps fc (Bind n (Pi _ _ _) sc) (x : xs)

14231423 = x : insertScopedImps fc sc xs

src/Idris/IBC.hs+1−1

@@ -40,7 +40,7 @@ import System.Directory

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 126

43+ibcVersion = 127

4444

4545data IBCFile = IBCFile { ver :: Word16,

4646 sourcefile :: FilePath,

src/Idris/ParseExpr.hs+3−3

@@ -1051,10 +1051,10 @@ normalImplicit opts st syn = do

10511051 sc <- expr syn

10521052 let (im,cl)

10531053 = if implicitAllowed syn

1054− then (Imp opts st False Nothing,

1054+ then (Imp opts st False (Just (Impl False True)),

10551055 constraint)

1056− else (Imp opts st False (Just (Impl False)),

1057− Imp opts st False (Just (Impl True)))

1056+ else (Imp opts st False (Just (Impl False False)),

1057+ Imp opts st False (Just (Impl True False)))

10581058 return (bindList (PPi im) xt

10591059 (bindList (PPi cl) cs sc))

10601060

src/Idris/REPL.hs+2

@@ -1059,6 +1059,8 @@ process fn (DebugInfo n)

10591059 when (not (null si)) $ iputStrLn (show si)

10601060 let di = lookupCtxt n (idris_datatypes i)

10611061 when (not (null di)) $ iputStrLn (show di)

1062+ let imps = lookupCtxt n (idris_implicits i)

1063+ when (not (null imps)) $ iputStrLn (show imps)

10621064 let d = lookupDef n (tt_ctxt i)

10631065 when (not (null d)) $ iputStrLn $ "Definition: " ++ (show (head d))

10641066 let cg = lookupCtxtName n (idris_callgraph i)