147149b · 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]

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

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

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

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

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

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

1079 = PClass doc info f

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

1081 n

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

1083 pDocs

1084+ fds

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

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

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

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

1086 = PInstance doc argDocs info f

1087 = PInstance doc argDocs info f

src/Idris/AbsSyntaxTree.hs+7−5

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

599 Name

600 [(Name, t)] -- parameters

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

602+ [Name] -- determining parameters

602 [PDecl' t] -- declarations

603 [PDecl' t] -- declarations

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

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

604 -- class name, parameters, method declarations

605 -- class name, parameters, method declarations

@@ -693,7 +694,7 @@ declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]

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

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

694declared (PNamespace _ ds) = concatMap declared ds

695declared (PNamespace _ ds) = concatMap declared ds

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

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

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

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

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

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

698declared (PDSL n _) = [n]

699declared (PDSL n _) = [n]

699declared (PSyntax _ _) = []

700declared (PSyntax _ _) = []

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

712tldeclared (PParams _ _ ds) = []

713tldeclared (PParams _ _ ds) = []

713tldeclared (PMutual _ ds) = concatMap tldeclared ds

714tldeclared (PMutual _ ds) = concatMap tldeclared ds

714tldeclared (PNamespace _ ds) = concatMap tldeclared ds

715tldeclared (PNamespace _ ds) = concatMap tldeclared ds

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

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

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

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

717tldeclared _ = []

718tldeclared _ = []

718

719

@@ -728,7 +729,7 @@ defined (PData _ _ _ _ _ (PLaterdecl n _)) = []

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

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

729defined (PNamespace _ ds) = concatMap defined ds

730defined (PNamespace _ ds) = concatMap defined ds

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

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

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

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

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

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

733defined (PDSL n _) = [n]

734defined (PDSL n _) = [n]

734defined (PSyntax _ _) = []

735defined (PSyntax _ _) = []

@@ -1029,7 +1030,8 @@ data ClassInfo = CI { instanceName :: Name,

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

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

1030 class_default_superclasses :: [PDecl],

1031 class_default_superclasses :: [PDecl],

1031 class_params :: [Name],

1032 class_params :: [Name],

1032− class_instances :: [Name] }

1033+ class_instances :: [Name],

1034+ class_determiners :: [Int] }

1033 deriving Show

1035 deriving Show

1034{-!

1036{-!

1035deriving instance Binary ClassInfo

1037deriving instance Binary ClassInfo

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

175 ctxt <- getContext

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

177 let nty = normalise ctxt [] cty

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

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

179

180− findOverlapping i t n

180+ findOverlapping i dets t n

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

182 | otherwise

183 = case lookupTy n (tt_ctxt i) of

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

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

186− case matchClause i tret' tret of

186+ case matchArgs i dets tret' tret of

187− Right ms -> Just tret'

187+ Right _ -> Just tret'

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

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

189− Right ms -> Just tret'

189+ Right _ -> Just tret'

190− Left _ -> Nothing

190+ Left _ -> Nothing

191 _ -> Nothing

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

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

194 getRetType (PPi _ _ _ sc) = getRetType sc

195 getRetType t = t

196

197+ matchArgs i dets x y =

198+ let x' = keepDets dets x

199+ y' = keepDets dets y in

200+ matchClause i x' y'

201+

202+ keepDets dets (PApp fc f args)

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

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

205+ keepDets dets t = t

206+

197 mkMethApp (n, _, _, ty)

207 mkMethApp (n, _, _, ty)

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

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

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

209 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

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

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

73 do focus n

74 g <- goal

75+ ptm <- get_term

75 resolveTC True True 7 g fn ist) ivs

76 resolveTC True True 7 g fn ist) ivs

76 tm <- get_term

77 tm <- get_term

77 ctxt <- get_context

78 ctxt <- get_context

@@ -965,17 +966,14 @@ elab ist info emode opts fn tm

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

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

966 elab' ina fc t

967 elab' ina fc t

967 unifyLog False

968 unifyLog False

968− elab' ina fc (PQuasiquote t goal)

969+ elab' ina fc (PQuasiquote t goalt)

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

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

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

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

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

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

973+ qty <- goal

972 (t, unq) <- extractUnquotes 0 t

974 (t, unq) <- extractUnquotes 0 t

973 let unquoteNames = map fst unq

975 let unquoteNames = map fst unq

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

975− claim uqh RType

976− movelast uqh

977− claim uqn (Var uqh)) unquoteNames

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

978−

979

977

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

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

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

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

@@ -1010,7 +1008,7 @@ elab ist info emode opts fn tm

1010 letbind nTm (Var qTy) (Var qTm)

1008 letbind nTm (Var qTy) (Var qTm)

1011

1009

1012 -- Fill out the goal type, if relevant

1010 -- Fill out the goal type, if relevant

1013− case goal of

1011+ case goalt of

1014 Nothing -> return ()

1012 Nothing -> return ()

1015 Just gTy -> do focus qTy

1013 Just gTy -> do focus qTy

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

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

@@ -1346,7 +1344,7 @@ findInstances :: IState -> Term -> [Name]

1346findInstances ist t

1344findInstances ist t

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

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

1348 = case lookupCtxt n (idris_classes ist) of

1346 = case lookupCtxt n (idris_classes ist) of

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

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

1350 _ -> []

1348 _ -> []

1351 | otherwise = []

1349 | otherwise = []

1352

1350

@@ -1382,17 +1380,18 @@ resolveTC :: Bool -- using default Int

1382 -> Term -- top level goal

1380 -> Term -- top level goal

1383 -> Name -- top level function name

1381 -> Name -- top level function name

1384 -> IState -> ElabD ()

1382 -> IState -> ElabD ()

1385−resolveTC = resTC' []

1383+resolveTC def mvok depth top fn ist

1384+ = do hs <- get_holes

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

1386

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

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

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

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

1389−resTC' tcs defaultOn mvok depth topg fn ist

1389+resTC' tcs defaultOn topholes depth topg fn ist

1390 = do compute

1391 g <- goal

1392− hs <- get_holes

1393− let argsok = tcArgsOK g hs

1392+ let argsok = tcArgsOK g topholes

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

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

1395− if (not argsok && not mvok)

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

1396 then lift $ tfail $ CantResolve True topg

1395 then lift $ tfail $ CantResolve True topg

1397 else do

1396 else do

1398 ptm <- get_term

1397 ptm <- get_term

@@ -1415,7 +1414,16 @@ resTC' tcs defaultOn mvok depth topg fn ist

1415 = True

1414 = True

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

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

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

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

1417+ case f of

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

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

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

1418− not $ any (isMeta hs) as

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

1422+

1423+ tcDetArgsOK i ds hs (x : xs)

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

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

1426+ tcDetArgsOK _ _ _ [] = True

1419

1427

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

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

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

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

@@ -1489,7 +1497,7 @@ resTC' tcs defaultOn mvok depth topg fn ist

1489 let got = fst (unApply t)

1497 let got = fst (unApply t)

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

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

1491 then depth - 1 else depth

1499 then depth - 1 else depth

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

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

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

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

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

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

1495 hs <- get_holes

1503 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