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

Makefile+1−1

compare with master

unifiedsplit

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

43 $(CABAL) install $(CABALFLAGS)

44

45linecount:

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

47

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

49doc: dist/setup-config

src/Idris/AbsSyntax.hs+7−3

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

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

1394 collectImps _ = []

1395

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

1397+ scopedimpl _ = False

1398+

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

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

1400+ | scopedimpl i = getImps sc imps

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

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

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

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

1399 where

1403 where

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

1556 pibind using [] sc = sc

1560 pibind using [] sc = sc

1557 pibind using (n:ns) sc

1561 pibind using (n:ns) sc

1558 = case lookup n using of

1562 = case lookup n using of

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

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

1560 n NoFC ty (pibind using ns sc)

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

1562 n NoFC Placeholder (pibind using ns sc)

1566 n NoFC Placeholder (pibind using ns sc)

1563

1567

1564-- Add implicit arguments in function calls

1568-- Add implicit arguments in function calls

src/Idris/AbsSyntaxTree.hs+3−3

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

587is_scoped (Imp _ _ _ s) = s

588is_scoped _ = Nothing

589

590−impl = Imp [] Dynamic False Nothing

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

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

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

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

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

593expl = Exp [] Dynamic False

594expl_param = Exp [] Dynamic True

595constraint = Constraint [] Static

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

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

484instance Binary ImplicitInfo where

485 put x

486 = case x of

487− Impl x1 -> put x1

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

488 get

489 = do x1 <- get

490+ x2 <- get

490− return (Impl x1)

491+ return (Impl x1 x2)

491

492

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

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

493 put x

494 put x

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

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

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

168

169instance NFData ImplicitInfo where

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

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

171

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

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

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

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

811deriving instance NFData Raw

812!-}

813

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

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

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

816

817{-!

src/Idris/Delaborate.hs+3

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

110 _ -> PRef un [] n

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

112 = 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)

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

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

114 | tcinstance impl

117 | tcinstance impl

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

118 = 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

1415 notImplicitable _ = False

1416

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

1418− | tcinstance i

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

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

1420− | otherwise

1420+ | not (toplevel_imp i)

1421 = pimp n Placeholder True : insertScopedImps fc sc xs

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

1423 = x : insertScopedImps fc sc xs

src/Idris/IBC.hs+1−1

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

40import Codec.Archive.Zip

41

42ibcVersion :: Word16

43−ibcVersion = 126

43+ibcVersion = 127

44

45data IBCFile = IBCFile { ver :: Word16,

46 sourcefile :: FilePath,

src/Idris/ParseExpr.hs+3−3

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

1051 sc <- expr syn

1052 let (im,cl)

1053 = if implicitAllowed syn

1054− then (Imp opts st False Nothing,

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

1055 constraint)

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

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

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

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

1058 return (bindList (PPi im) xt

1059 (bindList (PPi cl) cs sc))

1060

src/Idris/REPL.hs+2

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

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

1060 let di = lookupCtxt n (idris_datatypes i)

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

1062+ let imps = lookupCtxt n (idris_implicits i)

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

1062 let d = lookupDef n (tt_ctxt i)

1064 let d = lookupDef n (tt_ctxt i)

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

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

1064 let cg = lookupCtxtName n (idris_callgraph i)

1066 let cg = lookupCtxtName n (idris_callgraph i)