361efb5 · Idris-dev · git.iko.soy

CHANGELOG+3−1

@@ -23,7 +23,6 @@ New in 0.9.17:

2323 an extra argument of type TTName. This allows more understandable

2424 dynamic errors in DSL code and more readable code generation results.

2525* DSL notation can now be applied with $

26−<<<<<<< HEAD

2726* Added FFI_Export type which allows Idris functions to be exportoed and

2827 called from foreign code

2928* Instances can now have documentation strings.

@@ -38,6 +37,9 @@ New in 0.9.17:

3837 + `print` is now for putting showable things to STDOUT.

3938 + `printLn` is for putting showable things to STDOUT with a new line

4039 + `putCharLn` for putting a single character to STDOUT, with a new line.

40+* Classes can now be annotated with 'determining parameters' to say which

41+ must be available before resolving instances. Only determining parameters

42+ are checked when checking for overlapping instances.

4143

4244New in 0.9.16:

4345--------------

libs/base/Control/Monad/State.idr+1−1

@@ -6,7 +6,7 @@ import Control.Monad.Trans

66%access public

77

88||| A computation which runs in a context and produces an output

9−class Monad m => MonadState s (m : Type -> Type) where

9+class Monad m => MonadState s (m : Type -> Type) | m where

1010 ||| Get the context

1111 get : m s

1212 ||| Write a new context/output

libs/base/Control/Monad/Writer.idr+2−1

@@ -51,7 +51,8 @@ instance Monoid w => MonadTrans (WriterT w) where

5151

5252||| Run an action in the Writer monad and transform the written output

5353listens : MonadWriter w m => (w -> b) -> m a -> m (a, b)

54−listens f m = listens' f (listen m) where

54+listens {m} f act = listens' f (listen act) where

55+ listens' : (w -> b) -> m (a, w) -> m (a, b)

5556 listens' f' ma = do (a, w) <- ma

5657 return (a, f' w)

5758

libs/base/Data/Heap.idr+1−1

@@ -146,7 +146,7 @@ total isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h =

146146isEmptySizeZero Empty p = Refl

147147isEmptySizeZero (Node s l e r) p = ?isEmptySizeZeroNodeAbsurd

148148

149−total emptyHeapValid : Ord a => isValidHeap empty = True

149+total emptyHeapValid : Ord a => isValidHeap (empty {a}) = True

150150emptyHeapValid = Refl

151151

152152total singletonHeapValid : Ord a => (e : a) -> isValidHeap $ singleton e = True

libs/base/Decidable/Order.idr+4−4

@@ -36,12 +36,12 @@ class (Equivalence t eq) => Congruence t (f : t -> t) (eq : t -> t -> Type) wher

3636 eq (f a) (f b)

3737

3838minimum : (Ordered t to) => t -> t -> t

39−minimum x y with (order x y)

39+minimum {to} x y with (order {to} x y)

4040 | Left _ = x

4141 | Right _ = y

4242

4343maximum : (Ordered t to) => t -> t -> t

44−maximum x y with (order x y)

44+maximum {to} x y with (order {to} x y)

4545 | Left _ = y

4646 | Right _ = x

4747

@@ -103,7 +103,7 @@ total decideLTE : (n : Nat) -> (m : Nat) -> Dec (LTE n m)

103103decideLTE Z y = Yes LTEZero

104104decideLTE (S x) Z = No zeroNeverGreater

105105decideLTE (S x) (S y) with (decEq (S x) (S y))

106− | Yes eq = rewrite eq in Yes (reflexive x)

106+ | Yes eq = rewrite eq in Yes (reflexive (S y))

107107 | No _ with (decideLTE x y)

108108 | Yes nLTEm = Yes (LTESucc nLTEm)

109109 | No nGTm = No (ltesuccinjective nGTm)

@@ -122,7 +122,7 @@ shift m n mLTEn = LTESucc mLTEn

122122instance Ordered Nat LTE where

123123 order Z n = Left LTEZero

124124 order m Z = Right LTEZero

125− order (S k) (S j) with (order k j)

125+ order (S k) (S j) with (order {to=LTE} k j)

126126 order (S k) (S j) | Left prf = Left (shift k j prf)

127127 order (S k) (S j) | Right prf = Right (shift j k prf)

128128

libs/prelude/Language/Reflection.idr+6−6

@@ -416,14 +416,14 @@ instance Quotable NameType Raw where

416416 quote (TCon x y) = `(TCon ~(quote {t=Raw} x) ~(quote {t=Raw} y))

417417

418418instance Quotable a TT => Quotable (List a) TT where

419− quotedTy = `(List ~(quotedTy {a=a}))

420− quote [] = `(List.Nil {a=~quotedTy})

421− quote (x :: xs) = `(List.(::) {a=~quotedTy} ~(quote x) ~(quote xs))

419+ quotedTy = `(List ~(quotedTy {a}))

420+ quote [] = `(List.Nil {a=~(quotedTy {a})})

421+ quote (x :: xs) = `(List.(::) {a=~(quotedTy {a})} ~(quote x) ~(quote xs))

422422

423423instance Quotable a Raw => Quotable (List a) Raw where

424− quotedTy = `(List ~(quotedTy {a=a}))

425− quote [] = `(List.Nil {a=~quotedTy})

426− quote (x :: xs) = `(List.(::) {a=~quotedTy} ~(quote x) ~(quote xs))

424+ quotedTy = `(List ~(quotedTy {a}))

425+ quote [] = `(List.Nil {a=~(quotedTy {a})})

426+ quote (x :: xs) = `(List.(::) {a=~(quotedTy {a})} ~(quote x) ~(quote xs))

427427

428428instance Quotable TTName TT where

429429 quotedTy = `(TTName)

libs/prelude/Prelude/Algebra.idr+1−1

@@ -316,7 +316,7 @@ class (RingWithUnity a, AbelianGroup b) => Module a b where

316316

317317class (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where

318318 total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <.> y) <#> v

319− total moduleScalarUnityIsUnity : (v : b) -> unity <#> v = v

319+ total moduleScalarUnityIsUnity : (v : b) -> unity {a} <#> v = v

320320 total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)

321321 total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)

322322

src/Idris/AbsSyntax.hs+5−4

@@ -360,10 +360,10 @@ addInstance :: Bool -> Name -> Name -> Idris ()

360360addInstance int n i

361361 = do ist <- getIState

362362 case lookupCtxt n (idris_classes ist) of

363− [CI a b c d e ins] ->

364− do let cs = addDef n (CI a b c d e (addI i ins)) (idris_classes ist)

363+ [CI a b c d e ins fds] ->

364+ do let cs = addDef n (CI a b c d e (addI i ins) fds) (idris_classes ist)

365365 putIState $ ist { idris_classes = cs }

366− _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [i]) (idris_classes ist)

366+ _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [i] []) (idris_classes ist)

367367 putIState $ ist { idris_classes = cs }

368368 where addI i ins | int = i : ins

369369 | chaser n = ins ++ [i]

@@ -1088,12 +1088,13 @@ expandParamsD rhs ist dec ps ns (PParams f params pds)

10881088-- (map (expandParamsD ist dec ps ns) pds)

10891089expandParamsD rhs ist dec ps ns (PMutual f pds)

10901090 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)

1091−expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs decls)

1091+expandParamsD rhs ist dec ps ns (PClass doc info f cs n params pDocs fds decls)

10921092 = PClass doc info f

10931093 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)

10941094 n

10951095 (map (mapsnd (expandParams dec ps ns [])) params)

10961096 pDocs

1097+ fds

10971098 (map (expandParamsD rhs ist dec ps ns) decls)

10981099expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs n params ty cn decls)

10991100 = PInstance doc argDocs info f

src/Idris/AbsSyntaxTree.hs+7−5

@@ -603,6 +603,7 @@ data PDecl' t

603603 Name

604604 [(Name, t)] -- parameters

605605 [(Name, Docstring (Either Err PTerm))] -- parameter docstrings

606+ [Name] -- determining parameters

606607 [PDecl' t] -- declarations

607608 -- ^ Type class: arguments are documentation, syntax info, source location, constraints,

608609 -- class name, parameters, method declarations

@@ -699,7 +700,7 @@ declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]

699700declared (PParams _ _ ds) = concatMap declared ds

700701declared (PNamespace _ ds) = concatMap declared ds

701702declared (PRecord _ _ _ n _ _ _ c _) = [n, c]

702−declared (PClass _ _ _ _ n _ _ ms) = n : concatMap declared ms

703+declared (PClass _ _ _ _ n _ _ _ ms) = n : concatMap declared ms

703704declared (PInstance _ _ _ _ _ _ _ _ _ _) = []

704705declared (PDSL n _) = [n]

705706declared (PSyntax _ _) = []

@@ -718,7 +719,7 @@ tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

718719tldeclared (PParams _ _ ds) = []

719720tldeclared (PMutual _ ds) = concatMap tldeclared ds

720721tldeclared (PNamespace _ ds) = concatMap tldeclared ds

721−tldeclared (PClass _ _ _ _ n _ _ ms) = concatMap tldeclared ms

722+tldeclared (PClass _ _ _ _ n _ _ _ ms) = concatMap tldeclared ms

722723tldeclared (PInstance _ _ _ _ _ _ _ _ _ _) = []

723724tldeclared _ = []

724725

@@ -734,7 +735,7 @@ defined (PData _ _ _ _ _ (PLaterdecl n _)) = []

734735defined (PParams _ _ ds) = concatMap defined ds

735736defined (PNamespace _ ds) = concatMap defined ds

736737defined (PRecord _ _ _ n _ _ _ c _) = [n, c]

737−defined (PClass _ _ _ _ n _ _ ms) = n : concatMap defined ms

738+defined (PClass _ _ _ _ n _ _ _ ms) = n : concatMap defined ms

738739defined (PInstance _ _ _ _ _ _ _ _ _ _) = []

739740defined (PDSL n _) = [n]

740741defined (PSyntax _ _) = []

@@ -1035,7 +1036,8 @@ data ClassInfo = CI { instanceName :: Name,

10351036 class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl

10361037 class_default_superclasses :: [PDecl],

10371038 class_params :: [Name],

1038− class_instances :: [Name] }

1039+ class_instances :: [Name],

1040+ class_determiners :: [Int] }

10391041 deriving Show

10401042{-!

10411043deriving instance Binary ClassInfo

@@ -1733,7 +1735,7 @@ showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d

17331735showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)

17341736showDeclImp o (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)

17351737showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

1736−showDeclImp o (PClass _ _ _ cs n ps _ ds)

1738+showDeclImp o (PClass _ _ _ cs n ps _ _ ds)

17371739 = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds

17381740showDeclImp o (PInstance _ _ _ _ cs n _ t _ ds)

17391741 = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds

src/Idris/Core/ProofState.hs+5−5

@@ -879,6 +879,7 @@ updateProblems ps updates probs = up updates probs where

879879 ctxt = context ps

880880 ulog = unifylog ps

881881 usupp = map fst (notunified ps)

882+ dont = dontunify ps

882883

883884 up ns [] = (ns, [])

884885 up ns (prob@(x, y, ready, env, err, while, um) : ps) =

@@ -890,8 +891,9 @@ updateProblems ps updates probs = up updates probs where

890891 if newx || newy || ready ||

891892 any (\n -> n `elem` inj) (refsIn x ++ refsIn y) then

892893 case unify ctxt env' (x', lp) (y', rp) inj hs usupp while of

893− OK (v, []) -> traceWhen ulog ("DID " ++ show (x',y',ready,v)) $

894− up (ns ++ v) ps

894+ OK (v, []) -> traceWhen ulog ("DID " ++ show (x',y',ready,v,dont)) $

895+ let v' = filter (\(n, _) -> n `notElem` dont) v in

896+ up (ns ++ v') ps

895897 e -> -- trace ("FAILED " ++ show (x',y',ready,e)) $

896898 let (ns', ps') = up ns ps in

897899 (ns', (x',y', False, env',err', while, um) : ps')

@@ -940,9 +942,7 @@ processTactic EndUnify ps

940942 ns' = map (\ (n, t) -> (n, updateSolvedTerm ns t)) ns

941943 (ns'', probs') = updateProblems ps ns' (problems ps)

942944 tm' = updateSolved ns'' (pterm ps) in

943− traceWhen (unifylog ps) ("(EndUnify) Dropping holes: " ++ show (map fst ns'') ++ "\n" ++

944− show (pterm ps) ++ "\n" ++

945− show tm') $

945+ traceWhen (unifylog ps) ("(EndUnify) Dropping holes: " ++ show (map fst ns'')) $

946946 return (ps { pterm = tm',

947947 unified = (h, []),

948948 problems = probs',

src/Idris/DeepSeq.hs+4−4

@@ -149,10 +149,10 @@ instance (NFData t) => NFData (PDecl' t) where

149149 rnf x2 `seq`

150150 rnf x3 `seq`

151151 rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()

152− rnf (PClass x1 x2 x3 x4 x5 x6 x8 x7)

152+ rnf (PClass x1 x2 x3 x4 x5 x6 x8 x7 x9)

153153 = rnf x1 `seq`

154154 rnf x2 `seq`

155− rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

155+ rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()

156156 rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

157157 = rnf x1 `seq`

158158 rnf x2 `seq`

@@ -313,9 +313,9 @@ instance (NFData t) => NFData (PArg' t) where

313313 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

314314

315315instance NFData ClassInfo where

316− rnf (CI x1 x2 x3 x4 x5 x6)

316+ rnf (CI x1 x2 x3 x4 x5 x6 x7)

317317 = rnf x1 `seq`

318− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

318+ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()

319319

320320instance NFData OptInfo where

321321 rnf (Optimise x1 x2)

src/Idris/Elab/Class.hs+28−10

@@ -50,12 +50,13 @@ import Data.List.Split (splitOn)

5050

5151import Util.Pretty(pretty, text)

5252

53−data MArgTy = IA | EA | CA deriving Show

53+data MArgTy = IA Name | EA Name | CA deriving Show

5454

5555elabClass :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) ->

5656 FC -> [(Name, PTerm)] ->

57− Name -> [(Name, PTerm)] -> [(Name, Docstring (Either Err PTerm))] -> [PDecl] -> Idris ()

58−elabClass info syn_in doc fc constraints tn ps pDocs ds

57+ Name -> [(Name, PTerm)] -> [(Name, Docstring (Either Err PTerm))] ->

58+ [Name] -> [PDecl] -> Idris ()

59+elabClass info syn_in doc fc constraints tn ps pDocs fds ds

5960 = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

6061 let tty = pibind ps PType

6162 let constraint = PApp fc (PRef fc tn)

@@ -75,7 +76,6 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

7576 let (methods, imethods)

7677 = unzip (map (\ ( x,y,z) -> (x, y)) ims)

7778 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

78− addClass tn (CI cn (map nodoc imethods) defaults idecls (map fst ps) [])

7979 -- build instance constructor type

8080 -- decorate names of functions to ensure they can't be referred

8181 -- to elsewhere in the class declaration

@@ -86,6 +86,9 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

8686 let ddecl = PDatadecl tn tty cons

8787 logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)

8888 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc pDocs fc [] ddecl

89+

90+ dets <- findDets cn fds

91+ addClass tn (CI cn (map nodoc imethods) defaults idecls (map fst ps) [] dets)

8992 -- for each constraint, build a top level function to chase it

9093 logLvl 5 $ "Building functions"

9194-- let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps

@@ -94,6 +97,7 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

9497 mapM_ (rec_elabDecl info EAll info) (concat fns)

9598 -- for each method, build a top level function

9699 fns <- mapM (tfun cn constraint syn (map fst imethods)) imethods

100+ logLvl 5 $ "Functions " ++ show fns

97101 mapM_ (rec_elabDecl info EAll info) (concat fns)

98102 -- add the default definitions

99103 mapM_ (rec_elabDecl info EAll info) (concat (map (snd.snd) defs))

@@ -201,21 +205,21 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

201205 return [PTy doc [] syn fc o m ty',

202206 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

203207

204− getMArgs (PPi (Imp _ _ _ _) n ty sc) = IA : getMArgs sc

205− getMArgs (PPi (Exp _ _ _) n ty sc) = EA : getMArgs sc

208+ getMArgs (PPi (Imp _ _ _ _) n ty sc) = IA n : getMArgs sc

209+ getMArgs (PPi (Exp _ _ _) n ty sc) = EA n : getMArgs sc

206210 getMArgs (PPi (Constraint _ _) n ty sc) = CA : getMArgs sc

207211 getMArgs _ = []

208212

209213 getMeth (m:ms) (a:as) x | x == a = PRef fc m

210214 | otherwise = getMeth ms as x

211215

212− lhsArgs (EA : xs) (n : ns) = [] -- pexp (PRef fc n) : lhsArgs xs ns

213− lhsArgs (IA : xs) ns = lhsArgs xs ns

216+ lhsArgs (EA _ : xs) (n : ns) = [] -- pexp (PRef fc n) : lhsArgs xs ns

217+ lhsArgs (IA n : xs) ns = pimp n (PRef fc n) False : lhsArgs xs ns

214218 lhsArgs (CA : xs) ns = lhsArgs xs ns

215219 lhsArgs [] _ = []

216220

217− rhsArgs (EA : xs) (n : ns) = [] -- pexp (PRef fc n) : rhsArgs xs ns

218− rhsArgs (IA : xs) ns = pexp Placeholder : rhsArgs xs ns

221+ rhsArgs (EA _ : xs) (n : ns) = [] -- pexp (PRef fc n) : rhsArgs xs ns

222+ rhsArgs (IA n : xs) ns = pexp (PRef fc n) : rhsArgs xs ns

219223 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns

220224 rhsArgs [] _ = []

221225

@@ -230,3 +234,17 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

230234 | otherwise = PPi (e l s p) n ty (toExp ns e sc)

231235 toExp ns e (PPi p n ty sc) = PPi p n ty (toExp ns e sc)

232236 toExp ns e sc = sc

237+

238+findDets :: Name -> [Name] -> Idris [Int]

239+findDets n ns =

240+ do i <- getIState

241+ return $ case lookupTyExact n (tt_ctxt i) of

242+ Just ty -> getDetPos 0 ns ty

243+ Nothing -> []

244+ where

245+ getDetPos i ns (Bind n (Pi _ _ _) sc)

246+ | n `elem` ns = i : getDetPos (i + 1) ns sc

247+ | otherwise = getDetPos (i + 1) ns sc

248+ getDetPos _ _ _ = []

249+

250+

src/Idris/Elab/Instance.hs+18−8

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

7575 -- if the instance type matches any of the instances we have already,

7676 -- and it's not a named instance, then it's overlapping, so report an error

7777 case expn of

78− Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping i (delab i nty))

78+ Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping i (class_determiners ci) (delab i nty))

7979 (class_instances ci)

8080 addInstance intInst n iname

8181 Just _ -> addInstance intInst n iname

@@ -177,25 +177,35 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

177177 ctxt <- getContext

178178 (cty, _) <- recheckC fc [] tyT

179179 let nty = normalise ctxt [] cty

180− return $ any (isJust . findOverlapping i (delab i nty)) (class_instances ci)

180+ return $ any (isJust . findOverlapping i (class_determiners ci) (delab i nty)) (class_instances ci)

181181

182− findOverlapping i t n

182+ findOverlapping i dets t n

183183 | take 2 (show n) == "@@" = Nothing

184184 | otherwise

185185 = case lookupTy n (tt_ctxt i) of

186186 [t'] -> let tret = getRetType t

187187 tret' = getRetType (delab i t') in

188− case matchClause i tret' tret of

189− Right ms -> Just tret'

190− Left _ -> case matchClause i tret tret' of

191− Right ms -> Just tret'

192− Left _ -> Nothing

188+ case matchArgs i dets tret' tret of

189+ Right _ -> Just tret'

190+ Left _ -> case matchArgs i dets tret tret' of

191+ Right _ -> Just tret'

192+ Left _ -> Nothing

193193 _ -> Nothing

194194 overlapping t' = tclift $ tfail (At fc (Msg $

195195 "Overlapping instance: " ++ show t' ++ " already defined"))

196196 getRetType (PPi _ _ _ sc) = getRetType sc

197197 getRetType t = t

198198

199+ matchArgs i dets x y =

200+ let x' = keepDets dets x

201+ y' = keepDets dets y in

202+ matchClause i x' y'

203+

204+ keepDets dets (PApp fc f args)

205+ = PApp fc f $ let a' = zip [0..] args in

206+ map snd (filter (\(i, _) -> i `elem` dets) a')

207+ keepDets dets t = t

208+

199209 mkMethApp (n, _, _, ty)

200210 = lamBind 0 ty (papp fc (PRef fc n) (methArgs 0 ty))

201211 lamBind i (PPi (Constraint _ _) _ _ sc) sc'

src/Idris/ElabDecls.hs+2−2

@@ -229,10 +229,10 @@ elabDecl' what info (PNamespace n ps) = mapM_ (elabDecl' what ninfo) ps

229229 ninfo = case namespace info of

230230 Nothing -> info { namespace = Just [n] }

231231 Just ns -> info { namespace = Just (n:ns) }

232−elabDecl' what info (PClass doc s f cs n ps pdocs ds)

232+elabDecl' what info (PClass doc s f cs n ps pdocs fds ds)

233233 | what /= EDefns

234234 = do iLOG $ "Elaborating class " ++ show n

235− elabClass info (s { syn_params = [] }) doc f cs n ps pdocs ds

235+ elabClass info (s { syn_params = [] }) doc f cs n ps pdocs fds ds

236236elabDecl' what info (PInstance doc argDocs s f cs n ps t expn ds)

237237 = do iLOG $ "Elaborating instance " ++ show n

238238 elabInstance info s doc argDocs what f cs n ps t expn ds

src/Idris/ElabTerm.hs+26−18

@@ -99,6 +99,7 @@ build ist info emode opts fn tm

9999 mapM_ (\n -> when (n `elem` hs) $

100100 do focus n

101101 g <- goal

102+ ptm <- get_term

102103 resolveTC True True 7 g fn ist) ivs

103104 tm <- get_term

104105 ctxt <- get_context

@@ -994,17 +995,14 @@ elab ist info emode opts fn tm

994995 elab' ina fc (PUnifyLog t) = do unifyLog True

995996 elab' ina fc t

996997 unifyLog False

997− elab' ina fc (PQuasiquote t goal)

998+ elab' ina fc (PQuasiquote t goalt)

998999 = do -- First extract the unquoted subterms, replacing them with fresh

9991000 -- names in the quasiquoted term. Claim their reflections to be

10001001 -- an inferred type (to support polytypic quasiquotes).

1002+ qty <- goal

10011003 (t, unq) <- extractUnquotes 0 t

10021004 let unquoteNames = map fst unq

1003− mapM_ (\uqn -> do uqh <- getNameFrom (sMN 0 "uqh")

1004− claim uqh RType

1005− movelast uqh

1006− claim uqn (Var uqh)) unquoteNames

1007−

1005+ mapM_ (\uqn -> claim uqn (forget qty)) unquoteNames

10081006

10091007 -- Save the old state - we need a fresh proof state to avoid

10101008 -- capturing lexically available variables in the quoted term.

@@ -1039,7 +1037,7 @@ elab ist info emode opts fn tm

10391037 letbind nTm (Var qTy) (Var qTm)

10401038

10411039 -- Fill out the goal type, if relevant

1042− case goal of

1040+ case goalt of

10431041 Nothing -> return ()

10441042 Just gTy -> do focus qTy

10451043 elabE (ina { e_qq = True }) fc gTy

@@ -1375,7 +1373,7 @@ findInstances :: IState -> Term -> [Name]

13751373findInstances ist t

13761374 | (P _ n _, _) <- unApply t

13771375 = case lookupCtxt n (idris_classes ist) of

1378− [CI _ _ _ _ _ ins] -> ins

1376+ [CI _ _ _ _ _ ins _] -> ins

13791377 _ -> []

13801378 | otherwise = []

13811379

@@ -1411,17 +1409,18 @@ resolveTC :: Bool -- using default Int

14111409 -> Term -- top level goal

14121410 -> Name -- top level function name

14131411 -> IState -> ElabD ()

1414−resolveTC = resTC' []

1412+resolveTC def mvok depth top fn ist

1413+ = do hs <- get_holes

1414+ resTC' [] def hs depth top fn ist

14151415

1416−resTC' tcs def mvok 0 topg fn ist = fail $ "Can't resolve type class"

1417−resTC' tcs def mvok 1 topg fn ist = try' (trivial' ist) (resolveTC def mvok 0 topg fn ist) True

1418−resTC' tcs defaultOn mvok depth topg fn ist

1416+resTC' tcs def topholes 0 topg fn ist = fail $ "Can't resolve type class"

1417+resTC' tcs def topholes 1 topg fn ist = try' (trivial' ist) (resolveTC def False 0 topg fn ist) True

1418+resTC' tcs defaultOn topholes depth topg fn ist

14191419 = do compute

14201420 g <- goal

1421− hs <- get_holes

1422− let argsok = tcArgsOK g hs

1423−-- trace (show (g,hs,argsok,mvok)) $

1424− if (not argsok && not mvok)

1421+ let argsok = tcArgsOK g topholes

1422+-- trace (show (g,hs,argsok,topholes)) $

1423+ if not argsok -- && not mvok)

14251424 then lift $ tfail $ CantResolve True topg

14261425 else do

14271426 ptm <- get_term

@@ -1444,7 +1443,16 @@ resTC' tcs defaultOn mvok depth topg fn ist

14441443 = True

14451444 tcArgsOK ty hs -- if any arguments are metavariables, postpone

14461445 = let (f, as) = unApply ty in

1447− not $ any (isMeta hs) as

1446+ case f of

1447+ P _ cn _ -> case lookupCtxtExact cn (idris_classes ist) of

1448+ Just ci -> tcDetArgsOK 0 (class_determiners ci) hs as

1449+ Nothing -> not $ any (isMeta hs) as

1450+ _ -> not $ any (isMeta hs) as

1451+

1452+ tcDetArgsOK i ds hs (x : xs)

1453+ | i `elem` ds = not (isMeta hs x) && tcDetArgsOK (i + 1) ds hs xs

1454+ | otherwise = tcDetArgsOK (i + 1) ds hs xs

1455+ tcDetArgsOK _ _ _ [] = True

14481456

14491457 isMeta :: [Name] -> Term -> Bool

14501458 isMeta ns (P _ n _) = n `elem` ns

@@ -1518,7 +1526,7 @@ resTC' tcs defaultOn mvok depth topg fn ist

15181526 let got = fst (unApply t)

15191527 let depth' = if tc' `elem` tcs

15201528 then depth - 1 else depth

1521− resTC' (got : tcs) defaultOn mvok depth' topg fn ist)

1529+ resTC' (got : tcs) defaultOn topholes depth' topg fn ist)

15221530 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

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

15241532 hs <- get_holes

src/Idris/IBC.hs+10−6

@@ -37,7 +37,7 @@ import Codec.Compression.Zlib (compress)

3737import Util.Zlib (decompressEither)

3838

3939ibcVersion :: Word8

40−ibcVersion = 99

40+ibcVersion = 100

4141

4242data IBCFile = IBCFile { ver :: Word8,

4343 sourcefile :: FilePath,

@@ -365,7 +365,7 @@ pClasses cs = mapM_ (\ (n, c) ->

365365 -- Don't lose instances from previous IBCs, which

366366 -- could have loaded in any order

367367 let is = case lookupCtxtExact n (idris_classes i) of

368− Just (CI _ _ _ _ _ ins) -> ins

368+ Just (CI _ _ _ _ _ ins _) -> ins

369369 _ -> []

370370 let c' = c { class_instances =

371371 class_instances c ++ is }

@@ -1238,7 +1238,7 @@ instance (Binary t) => Binary (PDecl' t) where

12381238 put x7

12391239 put x8

12401240 put x9

1241− PClass x1 x2 x3 x4 x5 x6 x7 x8

1241+ PClass x1 x2 x3 x4 x5 x6 x7 x8 x9

12421242 -> do putWord8 7

12431243 put x1

12441244 put x2

@@ -1248,6 +1248,7 @@ instance (Binary t) => Binary (PDecl' t) where

12481248 put x6

12491249 put x7

12501250 put x8

1251+ put x9

12511252 PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 ->

12521253 do putWord8 8

12531254 put x1

@@ -1346,7 +1347,8 @@ instance (Binary t) => Binary (PDecl' t) where

13461347 x6 <- get

13471348 x7 <- get

13481349 x8 <- get

1349− return (PClass x1 x2 x3 x4 x5 x6 x7 x8)

1350+ x9 <- get

1351+ return (PClass x1 x2 x3 x4 x5 x6 x7 x8 x9)

13501352 8 -> do x1 <- get

13511353 x2 <- get

13521354 x3 <- get

@@ -2071,19 +2073,21 @@ instance (Binary t) => Binary (PArg' t) where

20712073

20722074

20732075instance Binary ClassInfo where

2074− put (CI x1 x2 x3 x4 x5 _)

2076+ put (CI x1 x2 x3 x4 x5 _ x6)

20752077 = do put x1

20762078 put x2

20772079 put x3

20782080 put x4

20792081 put x5

2082+ put x6

20802083 get

20812084 = do x1 <- get

20822085 x2 <- get

20832086 x3 <- get

20842087 x4 <- get

20852088 x5 <- get

2086− return (CI x1 x2 x3 x4 x5 [])

2089+ x6 <- get

2090+ return (CI x1 x2 x3 x4 x5 [] x6)

20872091

20882092instance Binary OptInfo where

20892093 put (Optimise x1 x2)

src/Idris/ParseHelpers.hs+2−2

@@ -585,8 +585,8 @@ collect (c@(PClauses _ o _ _) : ds)

585585collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

586586collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

587587collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds

588−collect (PClass doc f s cs n ps pdocs ds : ds')

589− = PClass doc f s cs n ps pdocs (collect ds) : collect ds'

588+collect (PClass doc f s cs n ps pdocs fds ds : ds')

589+ = PClass doc f s cs n ps pdocs fds (collect ds) : collect ds'

590590collect (PInstance doc argDocs f s cs n ps t en ds : ds')

591591 = PInstance doc argDocs f s cs n ps t en (collect ds) : collect ds'

592592collect (d : ds) = d : collect ds

src/Idris/Parser.hs+5−1

@@ -612,11 +612,15 @@ class_ syn = do (doc, argDocs, acc)

612612 n_in <- fnName

613613 let n = expandNS syn n_in

614614 cs <- many carg

615+ fds <- option (map fst cs) fundeps

615616 ds <- option [] (classBlock syn)

616617 accData acc n (concatMap declared ds)

617− return [PClass doc syn fc cons n cs argDocs ds]

618+ return [PClass doc syn fc cons n cs argDocs fds ds]

618619 <?> "type-class declaration"

619620 where

621+ fundeps :: IdrisParser [Name]

622+ fundeps = do lchar '|'; sepBy name (lchar ',')

623+

620624 carg :: IdrisParser (Name, PTerm)

621625 carg = do lchar '('; i <- name; lchar ':'; ty <- expr syn; lchar ')'

622626 return (i, ty)

src/Idris/REPL.hs+1−1

@@ -773,7 +773,7 @@ process fn (NewDefn decls) = do

773773 getName (PTy docs argdocs syn fc opts name ty) = Just name

774774 getName (PClauses fc opts name (clause:clauses)) = Just (getClauseName clause)

775775 getName (PData doc argdocs syn fc opts dataDecl) = Just (d_name dataDecl)

776− getName (PClass doc syn fc constraints name parms parmdocs decls) = Just name

776+ getName (PClass doc syn fc constraints name parms parmdocs fds decls) = Just name

777777 getName _ = Nothing

778778 -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes

779779 getClauseName (PClause fc name whole with rhs whereBlock) = name

test/basic012/basic012.idr+2−1

@@ -31,7 +31,8 @@ testfoo3 xs = foo 42 xs (bar 10)

3131AnyST : Type -> Type -> Type

3232AnyST s a = {m : _} -> Monad m => StateT s m a

3333

34−foost : AnyST Int ()

34+-- foost : AnyST Int ()

35+foost : StateT Int Maybe ()

3536foost = do x <- get

3637 put x

3738