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

CHANGELOG+3−1

compare with master

unifiedsplit

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

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

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

25* DSL notation can now be applied with $

26−<<<<<<< HEAD

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

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

28 called from foreign code

27 called from foreign code

29* Instances can now have documentation strings.

28* Instances can now have documentation strings.

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

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

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

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

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

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

39 + `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.

41

43

42New in 0.9.16:

44New in 0.9.16:

43--------------

45--------------

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

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

6%access public

7

8||| 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

10 ||| Get the context

11 get : m s

12 ||| Write a new context/output

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

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

51

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

53listens : 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)

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

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

56 return (a, f' w)

57 return (a, f' w)

57

58

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

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

146isEmptySizeZero Empty p = Refl

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

148

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

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

150emptyHeapValid = Refl

151

152total 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

36 eq (f a) (f b)

37

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

39−minimum x y with (order x y)

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

40 | Left _ = x

41 | Right _ = y

42

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

44−maximum x y with (order x y)

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

45 | Left _ = y

46 | Right _ = x

47

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

103decideLTE Z y = Yes LTEZero

104decideLTE (S x) Z = No zeroNeverGreater

105decideLTE (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))

107 | No _ with (decideLTE x y)

108 | Yes nLTEm = Yes (LTESucc nLTEm)

109 | No nGTm = No (ltesuccinjective nGTm)

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

122instance Ordered Nat LTE where

123 order Z n = Left LTEZero

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

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

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

128

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

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

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

417

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

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

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

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

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

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

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

422

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

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

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

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

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

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

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

427

428instance Quotable TTName TT where

429 quotedTy = `(TTName)

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

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

316

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

318 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

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

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

322

src/Idris/AbsSyntax.hs+5−4

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

360addInstance int n i

361 = do ist <- getIState

362 case lookupCtxt n (idris_classes ist) of

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

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

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

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

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

367 putIState $ ist { idris_classes = cs }

368 where addI i ins | int = i : ins

369 | chaser n = ins ++ [i]

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

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

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

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

1092 = PClass doc info f

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

1094 n

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

1096 pDocs

1097+ fds

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

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

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

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

1099 = PInstance doc argDocs info f

1100 = PInstance doc argDocs info f

src/Idris/AbsSyntaxTree.hs+7−5

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

603 Name

604 [(Name, t)] -- parameters

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

606+ [Name] -- determining parameters

606 [PDecl' t] -- declarations

607 [PDecl' t] -- declarations

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

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

608 -- class name, parameters, method declarations

609 -- class name, parameters, method declarations

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

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

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

700declared (PNamespace _ ds) = concatMap declared ds

701declared (PNamespace _ ds) = concatMap declared ds

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

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

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

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

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

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

704declared (PDSL n _) = [n]

705declared (PDSL n _) = [n]

705declared (PSyntax _ _) = []

706declared (PSyntax _ _) = []

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

718tldeclared (PParams _ _ ds) = []

719tldeclared (PParams _ _ ds) = []

719tldeclared (PMutual _ ds) = concatMap tldeclared ds

720tldeclared (PMutual _ ds) = concatMap tldeclared ds

720tldeclared (PNamespace _ ds) = concatMap tldeclared ds

721tldeclared (PNamespace _ ds) = concatMap tldeclared ds

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

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

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

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

723tldeclared _ = []

724tldeclared _ = []

724

725

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

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

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

735defined (PNamespace _ ds) = concatMap defined ds

736defined (PNamespace _ ds) = concatMap defined ds

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

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

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

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

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

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

739defined (PDSL n _) = [n]

740defined (PDSL n _) = [n]

740defined (PSyntax _ _) = []

741defined (PSyntax _ _) = []

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

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

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

1036 class_default_superclasses :: [PDecl],

1037 class_default_superclasses :: [PDecl],

1037 class_params :: [Name],

1038 class_params :: [Name],

1038− class_instances :: [Name] }

1039+ class_instances :: [Name],

1040+ class_determiners :: [Int] }

1039 deriving Show

1041 deriving Show

1040{-!

1042{-!

1041deriving instance Binary ClassInfo

1043deriving instance Binary ClassInfo

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

879 ctxt = context ps

880 ulog = unifylog ps

881 usupp = map fst (notunified ps)

882+ dont = dontunify ps

882

883

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

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

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

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

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

890 if newx || newy || ready ||

891 if newx || newy || ready ||

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

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

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

893 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+ OK (v, []) -> traceWhen ulog ("DID " ++ show (x',y',ready,v,dont)) $

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

894− up (ns ++ v) ps

896+ up (ns ++ v') ps

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

945− show tm') $

946 return (ps { pterm = tm',

947 unified = (h, []),

948 problems = probs',

src/Idris/DeepSeq.hs+4−4

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

149 rnf x2 `seq`

150 rnf x3 `seq`

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

153 = rnf x1 `seq`

154 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` ()

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

157 = rnf x1 `seq`

158 rnf x2 `seq`

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

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

314

315instance NFData ClassInfo where

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

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

317 = 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` ()

319

320instance NFData OptInfo where

321 rnf (Optimise x1 x2)

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

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

50

51import Util.Pretty(pretty, text)

52

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

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

54

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

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

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

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

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

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

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

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

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

60 let tty = pibind ps PType

61 let tty = pibind ps PType

61 let constraint = PApp fc (PRef fc tn)

62 let constraint = PApp fc (PRef fc tn)

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

75 let (methods, imethods)

76 let (methods, imethods)

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

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

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

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

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

79 -- build instance constructor type

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

81 -- to elsewhere in the class declaration

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

86 let ddecl = PDatadecl tn tty cons

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

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

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

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

90 logLvl 5 $ "Building functions"

93 logLvl 5 $ "Building functions"

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

94-- 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

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

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

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

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

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

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

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

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

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

98 -- add the default definitions

102 -- add the default definitions

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

103 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

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

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

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

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

203

207

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

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

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

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

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

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

207 getMArgs _ = []

211 getMArgs _ = []

208

212

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

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

210 | otherwise = getMeth ms as x

214 | otherwise = getMeth ms as x

211

215

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

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

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

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

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

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

215 lhsArgs [] _ = []

219 lhsArgs [] _ = []

216

220

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

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

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

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

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

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

220 rhsArgs [] _ = []

224 rhsArgs [] _ = []

221

225

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

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

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

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

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

232 toExp ns e sc = sc

236 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

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

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

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

79 (class_instances ci)

80 addInstance intInst n iname

81 Just _ -> addInstance intInst n iname

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

177 ctxt <- getContext

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

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

181

182− findOverlapping i t n

182+ findOverlapping i dets t n

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

184 | otherwise

185 = case lookupTy n (tt_ctxt i) of

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

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

188− case matchClause i tret' tret of

188+ case matchArgs i dets tret' tret of

189− Right ms -> Just tret'

189+ Right _ -> Just tret'

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

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

191− Right ms -> Just tret'

191+ Right _ -> Just tret'

192− Left _ -> Nothing

192+ Left _ -> Nothing

193 _ -> Nothing

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

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

196 getRetType (PPi _ _ _ sc) = getRetType sc

197 getRetType t = t

198

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+

199 mkMethApp (n, _, _, ty)

209 mkMethApp (n, _, _, ty)

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

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

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

211 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

229 ninfo = case namespace info of

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

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

233 | what /= EDefns

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

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

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

238 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

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

100 do focus n

101 g <- goal

102+ ptm <- get_term

102 resolveTC True True 7 g fn ist) ivs

103 resolveTC True True 7 g fn ist) ivs

103 tm <- get_term

104 tm <- get_term

104 ctxt <- get_context

105 ctxt <- get_context

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

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

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

995 elab' ina fc t

996 elab' ina fc t

996 unifyLog False

997 unifyLog False

997− elab' ina fc (PQuasiquote t goal)

998+ elab' ina fc (PQuasiquote t goalt)

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

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

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

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

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

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

1002+ qty <- goal

1001 (t, unq) <- extractUnquotes 0 t

1003 (t, unq) <- extractUnquotes 0 t

1002 let unquoteNames = map fst unq

1004 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

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

1007−

1008

1006

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

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

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

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

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

1039 letbind nTm (Var qTy) (Var qTm)

1037 letbind nTm (Var qTy) (Var qTm)

1040

1038

1041 -- Fill out the goal type, if relevant

1039 -- Fill out the goal type, if relevant

1042− case goal of

1040+ case goalt of

1043 Nothing -> return ()

1041 Nothing -> return ()

1044 Just gTy -> do focus qTy

1042 Just gTy -> do focus qTy

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

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

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

1375findInstances ist t

1373findInstances ist t

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

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

1377 = case lookupCtxt n (idris_classes ist) of

1375 = case lookupCtxt n (idris_classes ist) of

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

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

1379 _ -> []

1377 _ -> []

1380 | otherwise = []

1378 | otherwise = []

1381

1379

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

1411 -> Term -- top level goal

1409 -> Term -- top level goal

1412 -> Name -- top level function name

1410 -> Name -- top level function name

1413 -> IState -> ElabD ()

1411 -> 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

1415

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

1416+resTC' tcs def topholes 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

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

1418−resTC' tcs defaultOn mvok depth topg fn ist

1418+resTC' tcs defaultOn topholes depth topg fn ist

1419 = do compute

1420 g <- goal

1421− hs <- get_holes

1422− let argsok = tcArgsOK g hs

1421+ let argsok = tcArgsOK g topholes

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

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

1424− if (not argsok && not mvok)

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

1425 then lift $ tfail $ CantResolve True topg

1424 then lift $ tfail $ CantResolve True topg

1426 else do

1425 else do

1427 ptm <- get_term

1426 ptm <- get_term

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

1444 = True

1443 = True

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

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

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

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

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

1447− 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

1448

1456

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

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

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

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

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

1518 let got = fst (unApply t)

1526 let got = fst (unApply t)

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

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

1520 then depth - 1 else depth

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

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

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

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

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

1524 hs <- get_holes

1532 hs <- get_holes

src/Idris/IBC.hs+10−6

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

37import Util.Zlib (decompressEither)

38

39ibcVersion :: Word8

40−ibcVersion = 99

40+ibcVersion = 100

41

42data IBCFile = IBCFile { ver :: Word8,

43 sourcefile :: FilePath,

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

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

366 -- could have loaded in any order

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

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

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

369 _ -> []

370 let c' = c { class_instances =

371 class_instances c ++ is }

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

1238 put x7

1239 put x8

1240 put x9

1241− PClass x1 x2 x3 x4 x5 x6 x7 x8

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

1242 -> do putWord8 7

1243 put x1

1244 put x2

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

1248 put x6

1249 put x7

1250 put x8

1251+ put x9

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

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

1252 do putWord8 8

1253 do putWord8 8

1253 put x1

1254 put x1

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

1346 x6 <- get

1347 x6 <- get

1347 x7 <- get

1348 x7 <- get

1348 x8 <- get

1349 x8 <- get

1350+ x9 <- get

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

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

1350 8 -> do x1 <- get

1352 8 -> do x1 <- get

1351 x2 <- get

1353 x2 <- get

1352 x3 <- get

1354 x3 <- get

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

2071

2073

2072

2074

2073instance Binary ClassInfo where

2075instance Binary ClassInfo where

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

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

2075 = do put x1

2077 = do put x1

2076 put x2

2078 put x2

2077 put x3

2079 put x3

2078 put x4

2080 put x4

2079 put x5

2081 put x5

2082+ put x6

2080 get

2083 get

2081 = do x1 <- get

2084 = do x1 <- get

2082 x2 <- get

2085 x2 <- get

2083 x3 <- get

2086 x3 <- get

2084 x4 <- get

2087 x4 <- get

2085 x5 <- get

2088 x5 <- get

2089+ x6 <- get

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

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

2087

2091

2088instance Binary OptInfo where

2092instance Binary OptInfo where

2089 put (Optimise x1 x2)

2093 put (Optimise x1 x2)

src/Idris/ParseHelpers.hs+2−2

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

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

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

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

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

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

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

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

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

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

592collect (d : ds) = d : collect ds

src/Idris/Parser.hs+5−1

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

612 n_in <- fnName

613 let n = expandNS syn n_in

614 cs <- many carg

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

615 ds <- option [] (classBlock syn)

616 ds <- option [] (classBlock syn)

616 accData acc n (concatMap declared ds)

617 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]

618 <?> "type-class declaration"

619 <?> "type-class declaration"

619 where

620 where

621+ fundeps :: IdrisParser [Name]

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

623+

620 carg :: IdrisParser (Name, PTerm)

624 carg :: IdrisParser (Name, PTerm)

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

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

622 return (i, ty)

626 return (i, ty)

src/Idris/REPL.hs+1−1

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

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

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

775 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

777 getName _ = Nothing

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

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

31AnyST : Type -> Type -> Type

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

33

34−foost : AnyST Int ()

34+-- foost : AnyST Int ()

35+foost : StateT Int Maybe ()

35foost = do x <- get

36foost = do x <- get

36 put x

37 put x

37

38