0e76ac9 · Idris-dev · git.iko.soy

CHANGELOG+2

@@ -14,7 +14,9 @@ New in 0.9.10:

1414Internal changes

1515

1616* New module/dependency tree checking

17+* Improved type class resolution

1718* Compiling Nat via GMP integers

19+* Performance improvements in elaboration

1820

1921New in 0.9.9:

2022-------------

src/Idris/AbsSyntax.hs+10−10

@@ -578,7 +578,7 @@ inferDecl = PDatadecl inferTy

578578 PPi expl (MN 0 "a") (PRef bi (MN 0 "A"))

579579 (PRef bi inferTy)), bi)]

580580

581−infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder, pexp t]

581+infTerm t = PApp bi (PRef bi inferCon) [pimp (MN 0 "A") Placeholder True, pexp t]

582582infP = P (TCon 6 0) inferTy (TType (UVal 0))

583583

584584getInferTerm, getInferType :: Term -> Term

@@ -621,8 +621,8 @@ eqDecl = PDatadecl eqTy (piBind [(n "a", PType), (n "b", PType),

621621 PType)

622622 [("", eqCon, PPi impl (n "a") PType (

623623 PPi impl (n "x") (PRef bi (n "a"))

624− (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder,

625− pimp (n "b") Placeholder,

624+ (PApp bi (PRef bi eqTy) [pimp (n "a") Placeholder False,

625+ pimp (n "b") Placeholder False,

626626 pexp (PRef bi (n "x")),

627627 pexp (PRef bi (n "x"))])), bi)]

628628 where n a = MN 0 a

@@ -953,7 +953,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

953953 imps top env (PPi (Imp l _ doc) n ty sc)

954954 = do let isn = nub (namesIn uvars ist ty) `dropAll` [n]

955955 (decls , ns) <- get

956− put (PImp (getPriority ist ty) l n ty doc : decls,

956+ put (PImp (getPriority ist ty) True l n ty doc : decls,

957957 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

958958 imps True (n:env) sc

959959 imps top env (PPi (Exp l _ doc) n ty sc)

@@ -1152,10 +1152,10 @@ aiFn inpat expat ist fc f as

11521152 PConstraint p l tm d : insertImpl ps given

11531153 insertImpl (PConstraint p l ty d : ps) given =

11541154 PConstraint p l (PResolveTC fc) d : insertImpl ps given

1155− insertImpl (PImp p l n ty d : ps) given =

1155+ insertImpl (PImp p _ l n ty d : ps) given =

11561156 case find n given [] of

1157− Just (tm, given') -> PImp p l n tm "" : insertImpl ps given'

1158− Nothing -> PImp p l n Placeholder "" : insertImpl ps given

1157+ Just (tm, given') -> PImp p False l n tm "" : insertImpl ps given'

1158+ Nothing -> PImp p True l n Placeholder "" : insertImpl ps given

11591159 insertImpl (PTacImplicit p l n sc ty d : ps) given =

11601160 case find n given [] of

11611161 Just (tm, given') -> PTacImplicit p l n sc tm "" : insertImpl ps given'

@@ -1166,7 +1166,7 @@ aiFn inpat expat ist fc f as

11661166 insertImpl _ given = given

11671167

11681168 find n [] acc = Nothing

1169− find n (PImp _ _ n' t _ : gs) acc

1169+ find n (PImp _ _ _ n' t _ : gs) acc

11701170 | n == n' = Just (t, reverse acc ++ gs)

11711171 find n (PTacImplicit _ _ n' _ t _ : gs) acc

11721172 | n == n' = Just (t, reverse acc ++ gs)

@@ -1196,8 +1196,8 @@ stripLinear i tm = evalState (sl tm) [] where

11961196 sl (PApp fc fn args) = do fn' <- sl fn

11971197 args' <- mapM slA args

11981198 return $ PApp fc fn' args'

1199− where slA (PImp p l n t d) = do t' <- sl t

1200− return $ PImp p l n t' d

1199+ where slA (PImp p m l n t d) = do t' <- sl t

1200+ return $ PImp p m l n t' d

12011201 slA (PExp p l t d) = do t' <- sl t

12021202 return $ PExp p l t' d

12031203 slA (PConstraint p l t d)

src/Idris/AbsSyntaxTree.hs+6−5

@@ -659,6 +659,7 @@ type PDo = PDo' PTerm

659659-- TODO: priority no longer serves any purpose, drop it!

660660

661661data PArg' t = PImp { priority :: Int,

662+ machine_inf :: Bool, -- true if the machine inferred it

662663 lazyarg :: Bool, pname :: Name, getTm :: t,

663664 pargdoc :: String }

664665 | PExp { priority :: Int,

@@ -675,7 +676,7 @@ data PArg' t = PImp { priority :: Int,

675676 deriving (Show, Eq, Functor)

676677

677678instance Sized a => Sized (PArg' a) where

678− size (PImp p l nm trm _) = 1 + size nm + size trm

679+ size (PImp p _ l nm trm _) = 1 + size nm + size trm

679680 size (PExp p l trm _) = 1 + size trm

680681 size (PConstraint p l trm _) = 1 + size trm

681682 size (PTacImplicit p l nm scr trm _) = 1 + size nm + size scr + size trm

@@ -684,7 +685,7 @@ instance Sized a => Sized (PArg' a) where

684685deriving instance Binary PArg'

685686!-}

686687

687−pimp n t = PImp 1 True n t ""

688+pimp n t mach = PImp 1 mach True n t ""

688689pexp t = PExp 1 False t ""

689690pconst t = PConstraint 1 False t ""

690691ptacimp n s t = PTacImplicit 0 True n s t ""

@@ -851,7 +852,7 @@ showDImp impl (PDatadecl n ty cons)

851852

852853getImps :: [PArg] -> [(Name, PTerm)]

853854getImps [] = []

854−getImps (PImp _ _ n tm _ : xs) = (n, tm) : getImps xs

855+getImps (PImp _ _ _ n tm _ : xs) = (n, tm) : getImps xs

855856getImps (_ : xs) = getImps xs

856857

857858getExps :: [PArg] -> [PTerm]

@@ -1043,7 +1044,7 @@ prettyImp impl = prettySe 10

10431044

10441045 prettySe p _ = text "test"

10451046

1046− prettyArgS (PImp _ _ n tm _) = prettyArgSi (n, tm)

1047+ prettyArgS (PImp _ _ _ n tm _) = prettyArgSi (n, tm)

10471048 prettyArgS (PExp _ _ tm _) = prettyArgSe tm

10481049 prettyArgS (PConstraint _ _ tm _) = prettyArgSc tm

10491050 prettyArgS (PTacImplicit _ _ n _ tm _) = prettyArgSti (n, tm)

@@ -1214,7 +1215,7 @@ showImp ist impl colour tm = se 10 [] tm where

12141215

12151216 natns = "Prelude.Nat."

12161217

1217− sArg bnd (PImp _ _ n tm _) = siArg bnd (n, tm)

1218+ sArg bnd (PImp _ _ _ n tm _) = siArg bnd (n, tm)

12181219 sArg bnd (PExp _ _ tm _) = seArg bnd tm

12191220 sArg bnd (PConstraint _ _ tm _) = scArg bnd tm

12201221 sArg bnd (PTacImplicit _ _ n _ tm _) = stiArg bnd (n, tm)

src/Idris/Coverage.hs+9−4

@@ -117,7 +117,7 @@ quickEq (PApp _ t as) (PApp _ t' as')

117117 | length as == length as'

118118 = quickEq t t' && and (zipWith quickEq (map getTm as) (map getTm as'))

119119quickEq Placeholder Placeholder = True

120−quickEq _ _ = False

120+quickEq x y = False

121121

122122qelem x [] = False

123123qelem x (y : ys) | x `quickEq` y = True

@@ -177,11 +177,13 @@ genAll i args

177177 otherPats o@(PApp _ (PRef fc n) xs) = ops fc n xs o

178178 otherPats o@(PPair fc l r)

179179 = ops fc pairCon

180− ([pimp (UN "A") Placeholder, pimp (UN "B") Placeholder] ++

180+ ([pimp (UN "A") Placeholder True,

181+ pimp (UN "B") Placeholder True] ++

181182 [pexp l, pexp r]) o

182183 otherPats o@(PDPair fc t _ v)

183184 = ops fc (UN "Ex_intro")

184− ([pimp (UN "a") Placeholder, pimp (UN "P") Placeholder] ++

185+ ([pimp (UN "a") Placeholder True,

186+ pimp (UN "P") Placeholder True] ++

185187 [pexp t,pexp v]) o

186188 otherPats o@(PConstant c) = return o

187189 otherPats arg = return Placeholder

@@ -190,7 +192,7 @@ genAll i args

190192 | (TyDecl c@(DCon _ arity) ty : _) <- lookupDef n (tt_ctxt i)

191193 = do let force = getForceable i n -- no need to generate forceable positions

192194 let xs = dropForce force xs_in 0

193− xs' <- mapM otherPats (map getTm xs)

195+ xs' <- mapM otherPats (map getExpTm xs)

194196 let p = resugar (PApp fc (PRef fc n) (zipWith upd xs' xs))

195197 let tyn = getTy n (tt_ctxt i)

196198 case lookupCtxt tyn (idris_datatypes i) of

@@ -198,6 +200,9 @@ genAll i args

198200 _ -> [p]

199201 ops fc n arg o = return Placeholder

200202

203+ getExpTm (PImp _ True _ _ _ _) = Placeholder -- machine inferred, no point!

204+ getExpTm t = getTm t

205+

201206 -- put it back to its original form

202207 resugar (PApp _ (PRef fc (UN "Ex_intro")) [_,_,t,v])

203208 = PDPair fc (getTm t) Placeholder (getTm v)

src/Idris/Delaborate.hs+2−2

@@ -42,7 +42,7 @@ delabTy' ist imps tm fullname = de [] imps tm

4242 | otherwise = PRef un (dens n)

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

4444 = PLam n (de env [] ty) (de ((n,n):env) [] sc)

45− de env (PImp _ _ _ _ _:is) (Bind n (Pi ty) sc)

45+ de env (PImp _ _ _ _ _ _:is) (Bind n (Pi ty) sc)

4646 = PPi impl n (de env [] ty) (de ((n,n):env) is sc)

4747 de env (PConstraint _ _ _ _:is) (Bind n (Pi ty) sc)

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

@@ -88,7 +88,7 @@ delabTy' ist imps tm fullname = de [] imps tm

8888 = PApp un (PRef un n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

8989 | otherwise = PApp un (PRef un n) (map pexp args)

9090

91− imp (PImp p l n _ d) arg = PImp p l n arg d

91+ imp (PImp p m l n _ d) arg = PImp p m l n arg d

9292 imp (PExp p l _ d) arg = PExp p l arg d

9393 imp (PConstraint p l _ d) arg = PConstraint p l arg d

9494 imp (PTacImplicit p l n sc _ d) arg = PTacImplicit p l n sc arg d

src/Idris/Docs.hs+1−1

@@ -41,7 +41,7 @@ instance Show FunDoc where

4141 = Just $ "Class constraint " ++

4242 show (getTm arg) ++ showDoc (pargdoc arg)

4343 ++ "\n"

44− showArg (n, arg@(PImp _ _ _ _ doc))

44+ showArg (n, arg@(PImp _ _ _ _ _ doc))

4545 | not (null doc)

4646 = Just $ "(implicit) " ++

4747 show n ++ " : " ++ show (getTm arg)

src/Idris/ElabDecls.hs+5−5

@@ -414,7 +414,7 @@ elabRecord info syn doc fc tyn ty cdoc cn cty

414414 = getImplB k sc

415415 getImplB k _ = k

416416

417− renameBs (PImp _ _ _ _ _ : ps) (PPi p n ty s)

417+ renameBs (PImp _ _ _ _ _ _ : ps) (PPi p n ty s)

418418 = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))

419419 renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)

420420 renameBs _ t = t

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

932932 propagateParams :: [Name] -> PTerm -> PTerm

933933 propagateParams ps (PApp _ (PRef fc n) args)

934934 = PApp fc (PRef fc n) (map addP args)

935− where addP imp@(PImp _ _ _ Placeholder _)

935+ where addP imp@(PImp _ _ _ _ Placeholder _)

936936 | pname imp `elem` ps = imp { getTm = PRef fc (pname imp) }

937937 addP t = t

938938 propagateParams ps (PRef fc n)

939− = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x)) ps)

939+ = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)

940940 propagateParams ps x = x

941941

942942elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

@@ -1344,7 +1344,7 @@ elabInstance info syn fc cs n ps t expn ds

13441344 = PLam (MN i "meth") Placeholder (lamBind (i+1) sc sc')

13451345 lamBind i _ sc = sc

13461346 methArgs i (PPi (Imp _ _ _) n ty sc)

1347− = PImp 0 False n (PRef fc (MN i "meth")) "" : methArgs (i+1) sc

1347+ = PImp 0 True False n (PRef fc (MN i "meth")) "" : methArgs (i+1) sc

13481348 methArgs i (PPi (Exp _ _ _) n ty sc)

13491349 = PExp 0 False (PRef fc (MN i "meth")) "" : methArgs (i+1) sc

13501350 methArgs i (PPi (Constraint _ _ _) n ty sc)

@@ -1360,7 +1360,7 @@ elabInstance info syn fc cs n ps t expn ds

13601360 = do ps' <- getWParams ps

13611361 ctxt <- getContext

13621362 case lookupP n ctxt of

1363− [] -> return (pimp n (PRef fc n) : ps')

1363+ [] -> return (pimp n (PRef fc n) True : ps')

13641364 _ -> return ps'

13651365 getWParams (_ : ps) = getWParams ps

13661366

src/Idris/ElabTerm.hs+16−14

@@ -158,11 +158,13 @@ elab ist info pattern tcgen fn tm

158158 try (resolveTC 2 fn ist)

159159 (do c <- unique_hole (MN 0 "class")

160160 instanceArg c)

161− elab' ina (PRefl fc t) = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder,

162− pimp (MN 0 "x") t])

163− elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy) [pimp (MN 0 "a") Placeholder,

164− pimp (MN 0 "b") Placeholder,

165− pexp l, pexp r])

161+ elab' ina (PRefl fc t)

162+ = elab' ina (PApp fc (PRef fc eqCon) [pimp (MN 0 "a") Placeholder True,

163+ pimp (MN 0 "x") t False])

164+ elab' ina (PEq fc l r) = elab' ina (PApp fc (PRef fc eqTy)

165+ [pimp (MN 0 "a") Placeholder True,

166+ pimp (MN 0 "b") Placeholder False,

167+ pexp l, pexp r])

166168 elab' ina@(_, a) (PPair fc l r)

167169 = do hnf_compute

168170 g <- goal

@@ -170,8 +172,8 @@ elab ist info pattern tcgen fn tm

170172 TType _ -> elabE (True, a) (PApp fc (PRef fc pairTy)

171173 [pexp l,pexp r])

172174 _ -> elabE (True, a) (PApp fc (PRef fc pairCon)

173− [pimp (MN 0 "A") Placeholder,

174− pimp (MN 0 "B") Placeholder,

175+ [pimp (MN 0 "A") Placeholder True,

176+ pimp (MN 0 "B") Placeholder True,

175177 pexp l, pexp r])

176178 elab' ina (PDPair fc l@(PRef _ n) t r)

177179 = case t of

@@ -186,12 +188,12 @@ elab ist info pattern tcgen fn tm

186188 [pexp t,

187189 pexp (PLam n Placeholder r)])

188190 asValue = elab' ina (PApp fc (PRef fc existsCon)

189− [pimp (MN 0 "a") t,

190− pimp (MN 0 "P") Placeholder,

191+ [pimp (MN 0 "a") t False,

192+ pimp (MN 0 "P") Placeholder True,

191193 pexp l, pexp r])

192194 elab' ina (PDPair fc l t r) = elab' ina (PApp fc (PRef fc existsCon)

193− [pimp (MN 0 "a") t,

194− pimp (MN 0 "P") Placeholder,

195+ [pimp (MN 0 "a") t False,

196+ pimp (MN 0 "P") Placeholder True,

195197 pexp l, pexp r])

196198 elab' ina (PAlternative True as)

197199 = do hnf_compute

@@ -557,7 +559,7 @@ elab ist info pattern tcgen fn tm

557559 elabArgs ina failed fc r (n:ns) ((lazy, t) : args)

558560 | lazy && not pattern

559561 = do elabArg n (PApp bi (PRef bi (UN "lazy"))

560− [pimp (UN "a") Placeholder,

562+ [pimp (UN "a") Placeholder True,

561563 pexp t]);

562564 | otherwise = elabArg n t

563565 where elabArg n t

@@ -739,7 +741,7 @@ resolveTC depth fn ist

739741 -- if there's any arguments left, we've failed to resolve

740742 hs <- get_holes

741743 solve

742− where isImp (PImp p _ _ _ _) = (True, p)

744+ where isImp (PImp p _ _ _ _ _) = (True, p)

743745 isImp arg = (False, priority arg)

744746

745747collectDeferred :: Term -> State [(Name, Type)] Term

@@ -808,7 +810,7 @@ runTac autoSolve ist tac

808810 show fn')) fnimps

809811 tryAll tacs

810812 when autoSolve solveAll

811− where isImp (PImp _ _ _ _ _) = True

813+ where isImp (PImp _ _ _ _ _ _) = True

812814 isImp _ = False

813815 envArgs n = do e <- get_env

814816 case lookup n e of

src/Idris/IBC.hs+5−3

@@ -23,7 +23,7 @@ import Debug.Trace

2323import Paths_idris

2424

2525ibcVersion :: Word8

26−ibcVersion = 39

26+ibcVersion = 41

2727

2828data IBCFile = IBCFile { ver :: Word8,

2929 sourcefile :: FilePath,

@@ -1624,13 +1624,14 @@ instance (Binary t) => Binary (PDo' t) where

16241624instance (Binary t) => Binary (PArg' t) where

16251625 put x

16261626 = case x of

1627− PImp x1 x2 x3 x4 x5 ->

1627+ PImp x1 x2 x3 x4 x5 x6 ->

16281628 do putWord8 0

16291629 put x1

16301630 put x2

16311631 put x3

16321632 put x4

16331633 put x5

1634+ put x6

16341635 PExp x1 x2 x3 x4 ->

16351636 do putWord8 1

16361637 put x1

@@ -1659,7 +1660,8 @@ instance (Binary t) => Binary (PArg' t) where

16591660 x3 <- get

16601661 x4 <- get

16611662 x5 <- get

1662− return (PImp x1 x2 x3 x4 x5)

1663+ x6 <- get

1664+ return (PImp x1 x2 x3 x4 x5 x6)

16631665 1 -> do x1 <- get

16641666 x2 <- get

16651667 x3 <- get

src/Idris/ParseExpr.hs+1−1

@@ -514,7 +514,7 @@ implicitArg syn = do lchar '{'

514514 v <- option (PRef fc n) (do lchar '='

515515 expr syn)

516516 lchar '}'

517− return (pimp n v)

517+ return (pimp n v False)

518518 <?> "implicit function argument"

519519

520520{- |Parses a constraint argument (for selecting a named type class instance)