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

CHANGELOG+2

compare with master

unifiedsplit

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

14Internal changes

15

16* New module/dependency tree checking

17+* Improved type class resolution

17* Compiling Nat via GMP integers

18* Compiling Nat via GMP integers

19+* Performance improvements in elaboration

18

20

19New in 0.9.9:

21New in 0.9.9:

20-------------

22-------------

src/Idris/AbsSyntax.hs+10−10

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

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

579 (PRef bi inferTy)), bi)]

580

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]

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

583

584getInferTerm, getInferType :: Term -> Term

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

621 PType)

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

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

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

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

625− pimp (n "b") Placeholder,

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

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

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

628 where n a = MN 0 a

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

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

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

955 (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,

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

958 imps True (n:env) sc

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

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

1152 PConstraint p l tm d : insertImpl ps given

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

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

1156 case find n given [] of

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

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

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

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

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

1160 case find n given [] of

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

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

1166 insertImpl _ given = given

1167

1168 find n [] acc = Nothing

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

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

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

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

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

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

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

1197 args' <- mapM slA args

1198 return $ PApp fc fn' args'

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

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

1200− return $ PImp p l n t' d

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

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

1202 return $ PExp p l t' d

1203 slA (PConstraint p l t d)

src/Idris/AbsSyntaxTree.hs+6−5

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

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

660

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

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

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

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

663 pargdoc :: String }

664 pargdoc :: String }

664 | PExp { priority :: Int,

665 | PExp { priority :: Int,

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

675 deriving (Show, Eq, Functor)

676 deriving (Show, Eq, Functor)

676

677

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

678instance 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

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

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

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

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

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

682 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

684deriving instance Binary PArg'

685deriving instance Binary PArg'

685!-}

686!-}

686

687

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

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

688pexp t = PExp 1 False t ""

689pexp t = PExp 1 False t ""

689pconst t = PConstraint 1 False t ""

690pconst t = PConstraint 1 False t ""

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

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

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

851

852

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

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

853getImps [] = []

854getImps [] = []

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

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

855getImps (_ : xs) = getImps xs

856getImps (_ : xs) = getImps xs

856

857

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

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

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

1043

1044

1044 prettySe p _ = text "test"

1045 prettySe p _ = text "test"

1045

1046

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

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

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

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

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

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

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

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

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

1214

1215

1215 natns = "Prelude.Nat."

1216 natns = "Prelude.Nat."

1216

1217

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

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

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

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

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

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

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

1221 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')

117 | length as == length as'

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

119quickEq Placeholder Placeholder = True

120−quickEq _ _ = False

120+quickEq x y = False

121

122qelem x [] = False

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

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

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

178 otherPats o@(PPair fc l r)

179 = ops fc pairCon

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

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

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

181 [pexp l, pexp r]) o

182 [pexp l, pexp r]) o

182 otherPats o@(PDPair fc t _ v)

183 otherPats o@(PDPair fc t _ v)

183 = ops fc (UN "Ex_intro")

184 = 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] ++

185 [pexp t,pexp v]) o

187 [pexp t,pexp v]) o

186 otherPats o@(PConstant c) = return o

188 otherPats o@(PConstant c) = return o

187 otherPats arg = return Placeholder

189 otherPats arg = return Placeholder

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

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

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

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

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

192 let xs = dropForce force xs_in 0

194 let xs = dropForce force xs_in 0

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

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

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

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

195 let tyn = getTy n (tt_ctxt i)

197 let tyn = getTy n (tt_ctxt i)

196 case lookupCtxt tyn (idris_datatypes i) of

198 case lookupCtxt tyn (idris_datatypes i) of

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

198 _ -> [p]

200 _ -> [p]

199 ops fc n arg o = return Placeholder

201 ops fc n arg o = return Placeholder

200

202

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

204+ getExpTm t = getTm t

205+

201 -- put it back to its original form

206 -- put it back to its original form

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

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

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

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

42 | otherwise = PRef un (dens n)

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

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

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

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

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

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

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

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

90

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

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

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

94 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

41 = Just $ "Class constraint " ++

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

43 ++ "\n"

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

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

45 | not (null doc)

46 = Just $ "(implicit) " ++

47 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

414 = getImplB k sc

415 getImplB k _ = k

416

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

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

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

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

420 renameBs _ t = t

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

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

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

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

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

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

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

937 addP t = t

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

940 propagateParams ps x = x

941

942elabClause 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

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

1345 lamBind i _ sc = sc

1346 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

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

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

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

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

1360 = do ps' <- getWParams ps

1361 ctxt <- getContext

1362 case lookupP n ctxt of

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

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

1364 _ -> return ps'

1365 getWParams (_ : ps) = getWParams ps

1366

src/Idris/ElabTerm.hs+16−14

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

158 try (resolveTC 2 fn ist)

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

160 instanceArg c)

161+ elab' ina (PRefl fc t)

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

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

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

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

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

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

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

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

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

165− pexp l, pexp r])

167+ pexp l, pexp r])

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

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

167 = do hnf_compute

169 = do hnf_compute

168 g <- goal

170 g <- goal

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

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

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

171 [pexp l,pexp r])

173 [pexp l,pexp r])

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

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

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

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

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

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

175 pexp l, pexp r])

177 pexp l, pexp r])

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

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

177 = case t of

179 = case t of

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

186 [pexp t,

188 [pexp t,

187 pexp (PLam n Placeholder r)])

189 pexp (PLam n Placeholder r)])

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

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

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

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

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

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

191 pexp l, pexp r])

193 pexp l, pexp r])

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

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

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

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

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

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

195 pexp l, pexp r])

197 pexp l, pexp r])

196 elab' ina (PAlternative True as)

198 elab' ina (PAlternative True as)

197 = do hnf_compute

199 = do hnf_compute

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

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

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

558 | lazy && not pattern

560 | lazy && not pattern

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

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

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

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

561 pexp t]);

563 pexp t]);

562 | otherwise = elabArg n t

564 | otherwise = elabArg n t

563 where elabArg n t

565 where elabArg n t

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

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

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

740 hs <- get_holes

742 hs <- get_holes

741 solve

743 solve

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

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

743 isImp arg = (False, priority arg)

745 isImp arg = (False, priority arg)

744

746

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

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

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

808 show fn')) fnimps

810 show fn')) fnimps

809 tryAll tacs

811 tryAll tacs

810 when autoSolve solveAll

812 when autoSolve solveAll

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

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

812 isImp _ = False

814 isImp _ = False

813 envArgs n = do e <- get_env

815 envArgs n = do e <- get_env

814 case lookup n e of

816 case lookup n e of

src/Idris/IBC.hs+5−3

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

23import Paths_idris

24

25ibcVersion :: Word8

26−ibcVersion = 39

26+ibcVersion = 41

27

28data IBCFile = IBCFile { ver :: Word8,

29 sourcefile :: FilePath,

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

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

1625 put x

1626 = case x of

1627− PImp x1 x2 x3 x4 x5 ->

1627+ PImp x1 x2 x3 x4 x5 x6 ->

1628 do putWord8 0

1629 put x1

1630 put x2

1631 put x3

1632 put x4

1633 put x5

1634+ put x6

1634 PExp x1 x2 x3 x4 ->

1635 PExp x1 x2 x3 x4 ->

1635 do putWord8 1

1636 do putWord8 1

1636 put x1

1637 put x1

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

1659 x3 <- get

1660 x3 <- get

1660 x4 <- get

1661 x4 <- get

1661 x5 <- get

1662 x5 <- get

1663+ x6 <- get

1662− return (PImp x1 x2 x3 x4 x5)

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

1663 1 -> do x1 <- get

1665 1 -> do x1 <- get

1664 x2 <- get

1666 x2 <- get

1665 x3 <- get

1667 x3 <- get

src/Idris/ParseExpr.hs+1−1

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

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

515 expr syn)

516 lchar '}'

517− return (pimp n v)

517+ return (pimp n v False)

518 <?> "implicit function argument"

519

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