aa33865 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge remote-tracking branch 'upstream/master' into issue2004

aa33865Andreas Reuleaux12 years ago

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.

42New in 0.9.16:

44New in 0.9.16:

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

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

Setup.hs+9−2

@@ -57,6 +57,13 @@ usesGMP flags =

57 Just False -> False

58 Nothing -> True

60+execOnly :: S.ConfigFlags -> Bool

61+execOnly flags =

62+ case lookup (FlagName "execonly") (S.configConfigurationsFlags flags) of

63+ Just True -> True

64+ Just False -> False

65+ Nothing -> True

66+

60isRelease :: S.ConfigFlags -> Bool

67isRelease :: S.ConfigFlags -> Bool

61isRelease flags =

68isRelease flags =

62 case lookup (FlagName "release") (S.configConfigurationsFlags flags) of

69 case lookup (FlagName "release") (S.configConfigurationsFlags flags) of

@@ -176,7 +183,7 @@ getVersion args flags = do

176 let buildinfo = (emptyBuildInfo { cppOptions = ["-DVERSION="++hash] }) :: BuildInfo

183 let buildinfo = (emptyBuildInfo { cppOptions = ["-DVERSION="++hash] }) :: BuildInfo

177 return (Just buildinfo, [])

184 return (Just buildinfo, [])

178

185

179−idrisBuild _ flags _ local = do

186+idrisBuild _ flags _ local = unless (execOnly (configFlags local)) $ do

180 buildStdLib

187 buildStdLib

181 buildRTS

188 buildRTS

182 where

189 where

@@ -199,7 +206,7 @@ idrisBuild _ flags _ local = do

199-- -----------------------------------------------------------------------------

206-- -----------------------------------------------------------------------------

200-- Copy/Install

207-- Copy/Install

201

208

202−idrisInstall verbosity copy pkg local = do

209+idrisInstall verbosity copy pkg local = unless (execOnly (configFlags local)) $ do

203 installStdLib

210 installStdLib

204 installRTS

211 installRTS

205 where

212 where

idris.cabal+6

@@ -658,6 +658,11 @@ Flag CI

658 Default: False

659 manual: True

660

661+Flag execonly

662+ Description: Build executables only, skip the libraries and RTS

663+ Default: False

664+ manual: True

665+

661Library

666Library

662 hs-source-dirs: src

667 hs-source-dirs: src

663 Exposed-modules:

668 Exposed-modules:

@@ -725,6 +730,7 @@ Library

725 , Idris.ProofSearch

730 , Idris.ProofSearch

726 , Idris.Prover

731 , Idris.Prover

727 , Idris.Providers

732 , Idris.Providers

733+ , Idris.Reflection

728 , Idris.REPL

734 , Idris.REPL

729 , Idris.REPLParser

735 , Idris.REPLParser

730 , Idris.Transforms

736 , Idris.Transforms

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

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

6%access public

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

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)

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)

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

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

@@ -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/base/Language/Reflection/Utils.idr+1

@@ -272,6 +272,7 @@ instance Show Err where

272 show (CantResolve tm) = "CantResolve " ++ show tm

273 show (CantResolveAlts xs) = "CantResolveAlts " ++ show xs

274 show (IncompleteTerm tm) = "IncompleteTerm " ++ show tm

275+ show (NoEliminator s tm) = "NoEliminator " ++ show s ++ " " ++ show tm

275 show UniverseError = "UniverseError"

276 show UniverseError = "UniverseError"

276 show ProgramLineComment = "ProgramLineComment"

277 show ProgramLineComment = "ProgramLineComment"

277 show (Inaccessible n) = "Inaccessible " ++ show n

278 show (Inaccessible n) = "Inaccessible " ++ show n

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/Language/Reflection/Errors.idr+1

@@ -31,6 +31,7 @@ data Err = Msg String

31 | CantResolve TT

32 | CantResolveAlts (List TTName)

33 | IncompleteTerm TT

34+ | NoEliminator String TT

34 | UniverseError

35 | UniverseError

35 | ProgramLineComment

36 | ProgramLineComment

36 | Inaccessible TTName

37 | Inaccessible TTName

libs/prelude/Language/Reflection/Tactical.idr+14

@@ -8,6 +8,14 @@ import Prelude.Maybe

8import Prelude.Monad

9import Language.Reflection

11+data Arg : Type where

12+ Explicit : TTName -> Raw -> Arg

13+ Implicit : TTName -> Raw -> Arg

14+ Constraint : TTName -> Raw -> Arg

15+

16+data TyDecl : Type where

17+ Declare : TTName -> List Arg -> Raw -> TyDecl

18+

11abstract

19abstract

12data Tactical : Type -> Type where

20data Tactical : Type -> Type where

13 -- obligatory control stuff

21 -- obligatory control stuff

@@ -39,8 +47,11 @@ data Tactical : Type -> Type where

39 prim__Claim : TTName -> Raw -> Tactical ()

47 prim__Claim : TTName -> Raw -> Tactical ()

40 prim__Intro : Maybe TTName -> Tactical ()

48 prim__Intro : Maybe TTName -> Tactical ()

50+ prim__DeclareType : TyDecl -> Tactical ()

51+

42 prim__Debug : {a : Type} -> Maybe String -> Tactical a

52 prim__Debug : {a : Type} -> Maybe String -> Tactical a

54+

44-------------

55-------------

45-- Public API

56-- Public API

46-------------

57-------------

@@ -117,6 +128,9 @@ sourceLocation = do loc <- getSourceLocation

117rewriteWith : Raw -> Tactical ()

128rewriteWith : Raw -> Tactical ()

118rewriteWith rule = prim__Rewrite rule

129rewriteWith rule = prim__Rewrite rule

119

130

131+declareType : TyDecl -> Tactical ()

132+declareType decl = prim__DeclareType decl

133+

120debug : Tactical a

134debug : Tactical a

121debug = prim__Debug Nothing

135debug = prim__Debug Nothing

122

136

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+19−5

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

@@ -455,6 +455,10 @@ getIState = get

455putIState :: IState -> Idris ()

456putIState = put

457

458+updateIState :: (IState -> IState) -> Idris ()

459+updateIState f = do i <- getIState

460+ putIState $ f i

461+

458withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b

462withContext :: (IState -> Ctxt a) -> Name -> b -> (a -> Idris b) -> Idris b

459withContext ctx name dflt action = do

463withContext ctx name dflt action = do

460 ist <- getIState

464 ist <- getIState

@@ -547,7 +551,16 @@ addConstraints fc (v, cs)

547addDeferred = addDeferred' Ref

551addDeferred = addDeferred' Ref

548addDeferredTyCon = addDeferred' (TCon 0 0)

552addDeferredTyCon = addDeferred' (TCon 0 0)

549

553

554+-- | Save information about a name that is not yet defined

555+addDeferred' :: NameType

550−addDeferred' :: NameType -> [(Name, (Int, Maybe Name, Type, Bool))] -> Idris ()

556+ -> [(Name, (Int, Maybe Name, Type, Bool))]

557+ -- ^ The Name is the name being made into a metavar,

558+ -- the Int is the number of vars that are part of a

559+ -- putative proof context, the Maybe Name is the

560+ -- top-level function containing the new metavariable,

561+ -- the Type is its type, and the Bool is whether :p is

562+ -- allowed

563+ -> Idris ()

551addDeferred' nt ns

564addDeferred' nt ns

552 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns

565 = do mapM_ (\(n, (i, _, t, _)) -> updateContext (addTyDecl n nt (tidyNames S.empty t))) ns

553 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns

566 mapM_ (\(n, _) -> when (not (n `elem` primDefs)) $ addIBC (IBCMetavar n)) ns

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

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

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

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

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

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

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

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

1079 = PClass doc info f

1092 = PClass doc info f

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

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

1081 n

1094 n

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

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

1083 pDocs

1096 pDocs

1097+ fds

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

1098 (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)

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

1086 = PInstance doc argDocs info f

1100 = PInstance doc argDocs info f

src/Idris/AbsSyntaxTree.hs+16−8

@@ -186,7 +186,11 @@ data IState = IState {

186 idris_name :: Int,

187 idris_lineapps :: [((FilePath, Int), PTerm)],

188 -- ^ Full application LHS on source line

189+ idris_metavars :: [(Name, (Maybe Name, Int, Bool))],

189− idris_metavars :: [(Name, (Maybe Name, Int, Bool))], -- ^ The currently defined but not proven metavariables

190+ -- ^ The currently defined but not proven metavariables. The Int

191+ -- is the number of vars to display as a context, the Maybe Name

192+ -- is its top-level function, and the Bool is whether :p is

193+ -- allowed

190 idris_coercions :: [Name],

194 idris_coercions :: [Name],

191 idris_errRev :: [(Term, Term)],

195 idris_errRev :: [(Term, Term)],

192 syntax_rules :: SyntaxRules,

196 syntax_rules :: SyntaxRules,

@@ -602,6 +606,7 @@ data PDecl' t

602 Name

606 Name

603 [(Name, t)] -- parameters

607 [(Name, t)] -- parameters

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

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

609+ [Name] -- determining parameters

605 [PDecl' t] -- declarations

610 [PDecl' t] -- declarations

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

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

607 -- class name, parameters, method declarations

612 -- class name, parameters, method declarations

@@ -634,10 +639,12 @@ deriving instance NFData PDecl'

634-- For elaborator state

639-- For elaborator state

635data EState = EState {

640data EState = EState {

636 case_decls :: [PDecl],

641 case_decls :: [PDecl],

637− delayed_elab :: [Elab' EState ()]

642+ delayed_elab :: [Elab' EState ()],

643+ new_tyDecls :: [(Name, FC, [PArg], Type)]

638 }

644 }

639

645

640−initEState = EState [] []

646+initEState :: EState

647+initEState = EState [] [] []

641

648

642type ElabD a = Elab' EState a

649type ElabD a = Elab' EState a

643

650

@@ -696,7 +703,7 @@ declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]

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

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

697declared (PNamespace _ ds) = concatMap declared ds

704declared (PNamespace _ ds) = concatMap declared ds

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

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

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

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

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

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

701declared (PDSL n _) = [n]

708declared (PDSL n _) = [n]

702declared (PSyntax _ _) = []

709declared (PSyntax _ _) = []

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

715tldeclared (PParams _ _ ds) = []

722tldeclared (PParams _ _ ds) = []

716tldeclared (PMutual _ ds) = concatMap tldeclared ds

723tldeclared (PMutual _ ds) = concatMap tldeclared ds

717tldeclared (PNamespace _ ds) = concatMap tldeclared ds

724tldeclared (PNamespace _ ds) = concatMap tldeclared ds

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

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

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

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

720tldeclared _ = []

727tldeclared _ = []

721

728

@@ -731,7 +738,7 @@ defined (PData _ _ _ _ _ (PLaterdecl n _)) = []

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

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

732defined (PNamespace _ ds) = concatMap defined ds

739defined (PNamespace _ ds) = concatMap defined ds

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

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

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

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

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

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

736defined (PDSL n _) = [n]

743defined (PDSL n _) = [n]

737defined (PSyntax _ _) = []

744defined (PSyntax _ _) = []

@@ -1032,7 +1039,8 @@ data ClassInfo = CI { instanceName :: Name,

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

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

1033 class_default_superclasses :: [PDecl],

1040 class_default_superclasses :: [PDecl],

1034 class_params :: [Name],

1041 class_params :: [Name],

1035− class_instances :: [Name] }

1042+ class_instances :: [Name],

1043+ class_determiners :: [Int] }

1036 deriving Show

1044 deriving Show

1037{-!

1045{-!

1038deriving instance Binary ClassInfo

1046deriving instance Binary ClassInfo

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

src/Idris/Core/Binary.hs+9−3

@@ -91,8 +91,8 @@ instance Binary a => Binary (Err' a) where

91 put x

92 put y

93 put z

94− put (CantResolve t) = do putWord8 15

94+ put (CantResolve _ t) = do putWord8 15

95− put t

95+ put t

96 put (CantResolveAlts ns) = do putWord8 16

97 put ns

98 put (IncompleteTerm t) = do putWord8 17

@@ -146,6 +146,9 @@ instance Binary a => Binary (Err' a) where

146 put x1

147 put x2

148 put x3

149+ put (NoEliminator s t) = do putWord8 37

150+ put s

151+ put t

149

152

150 get = do i <- getWord8

153 get = do i <- getWord8

151 case i of

154 case i of

@@ -172,7 +175,7 @@ instance Binary a => Binary (Err' a) where

172 13 -> fmap NoTypeDecl get

175 13 -> fmap NoTypeDecl get

173 14 -> do x <- get ; y <- get ; z <- get

176 14 -> do x <- get ; y <- get ; z <- get

174 return $ NotInjective x y z

177 return $ NotInjective x y z

175− 15 -> fmap CantResolve get

178+ 15 -> fmap (CantResolve False) get

176 16 -> fmap CantResolveAlts get

179 16 -> fmap CantResolveAlts get

177 17 -> fmap IncompleteTerm get

180 17 -> fmap IncompleteTerm get

178 18 -> return UniverseError

181 18 -> return UniverseError

@@ -205,6 +208,9 @@ instance Binary a => Binary (Err' a) where

205 x2 <- get

208 x2 <- get

206 x3 <- get

209 x3 <- get

207 return (ElabDebug x1 x2 x3)

210 return (ElabDebug x1 x2 x3)

211+ 37 -> do x1 <- get

212+ x2 <- get

213+ return (NoEliminator x1 x2)

208 _ -> error "Corrupted binary data for Err'"

214 _ -> error "Corrupted binary data for Err'"

209----- Generated by 'derive'

215----- Generated by 'derive'

210

216

src/Idris/Core/DeepSeq.hs+2−1

@@ -80,9 +80,10 @@ instance NFData Err where

80 rnf (NoTypeDecl x1) = rnf x1 `seq` ()

81 rnf (NotInjective x1 x2 x3)

82 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

83− rnf (CantResolve x1) = rnf x1 `seq` ()

83+ rnf (CantResolve x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

84 rnf (CantResolveAlts x1) = rnf x1 `seq` ()

85 rnf (IncompleteTerm x1) = rnf x1 `seq` ()

86+ rnf (NoEliminator x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

86 rnf UniverseError = ()

87 rnf UniverseError = ()

87 rnf ProgramLineComment = ()

88 rnf ProgramLineComment = ()

88 rnf (Inaccessible x1) = rnf x1 `seq` ()

89 rnf (Inaccessible x1) = rnf x1 `seq` ()

src/Idris/Core/Elaborate.hs+30−14

@@ -756,20 +756,20 @@ handleError p t1 t2 proofSearch

756

757try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a

758try' t1 t2 proofSearch

759− = do s <- get

759+ = do s <- get

760− ps <- get_probs

760+ ps <- get_probs

761− ulog <- getUnifyLog

761+ ulog <- getUnifyLog

762− case prunStateT 999999 False ps t1 s of

762+ case prunStateT 999999 False ps t1 s of

763− OK ((v, _, _), s') -> do put s'

763+ OK ((v, _, _), s') -> do put s'

764− return $! v

764+ return $! v

765− Error e1 -> traceWhen ulog ("try failed " ++ show e1) $

765+ Error e1 -> traceWhen ulog ("try failed " ++ show e1) $

766− if recoverableErr e1 then

766+ if recoverableErr e1 then

767− do case runStateT t2 s of

767+ do case runStateT t2 s of

768− OK (v, s') -> do put s'; return $! v

768+ OK (v, s') -> do put s'; return $! v

769− Error e2 -> if score e1 >= score e2

769+ Error e2 -> if score e1 >= score e2

770− then lift (tfail e1)

770+ then lift (tfail e1)

771− else lift (tfail e2)

771+ else lift (tfail e2)

772− else lift (tfail e1)

772+ else lift (tfail e1)

773 where recoverableErr err@(CantUnify r x y _ _ _)

774 = -- traceWhen r (show err) $

775 r || proofSearch

@@ -782,6 +782,22 @@ try' t1 t2 proofSearch

782 recoverableErr (ElabDebug _ _ _) = False

783 recoverableErr _ = True

784

785+tryCatch :: Elab' aux a -> (Err -> Elab' aux a) -> Elab' aux a

786+tryCatch t1 t2

787+ = do s <- get

788+ ps <- get_probs

789+ ulog <- getUnifyLog

790+ case prunStateT 999999 False ps t1 s of

791+ OK ((v, _, _), s') -> do put s'

792+ return $! v

793+ Error e1 -> traceWhen ulog ("tryCatch failed " ++ show e1) $

794+ case runStateT (t2 e1) s of

795+ OK (v, s') -> do put s'

796+ return $! v

797+ Error e2 -> if score e1 >= score e2

798+ then lift (tfail e1)

799+ else lift (tfail e2)

800+

785tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a

801tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a

786tryWhen True a b = try a b

802tryWhen True a b = try a b

787tryWhen False a b = a

803tryWhen False a b = a

src/Idris/Core/ProofState.hs+9−6

@@ -681,8 +681,8 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

681 (tmv, tmt) <- lift $ check ctxt env tm

682 let tmt' = normalise ctxt env tmt

683 let (tacn, tacstr, tactt) = if induction

684− then (ElimN, "an eliminator", "Induction")

684+ then (ElimN, "eliminator", "Induction")

685− else (CaseN, "a case function", "Case analysis")

685+ else (CaseN, "case analysis", "Case analysis")

686 case unApply tmt' of

687 (P _ tnm _, tyargs) -> do

688 case lookupTy (SN (tacn tnm)) ctxt of

@@ -717,9 +717,10 @@ casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

717 (scv, sct) <- lift $ check ctxt env res'

718 let (scv', _) = specialise ctxt env [] scv

719 return scv'

720− [] -> lift $ tfail $ Msg $ tactt ++ " needs " ++ tacstr ++ " for " ++ show tnm

720+ [] -> lift $ tfail $ NoEliminator tacstr tmt'

721 xs -> lift $ tfail $ Msg $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm

722− _ -> fail $ "Unkown type for " ++ if induction then "induction" else "case analysis"

722+ _ -> lift $ tfail $ NoEliminator (if induction then "induction" else "case analysis")

723+ tmt'

723 where scname = sMN 0 "scarg"

724 where scname = sMN 0 "scarg"

724 makeConsArg (nm, ty) = P Bound nm ty

725 makeConsArg (nm, ty) = P Bound nm ty

725 bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v

726 bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v

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

878 ctxt = context ps

879 ctxt = context ps

879 ulog = unifylog ps

880 ulog = unifylog ps

880 usupp = map fst (notunified ps)

881 usupp = map fst (notunified ps)

882+ dont = dontunify ps

881

883

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

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

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

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

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

889 if newx || newy || ready ||

891 if newx || newy || ready ||

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

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

891 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

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

893− up (ns ++ v) ps

896+ up (ns ++ v') ps

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

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

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

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

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

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

src/Idris/Core/ProofTerm.hs+3

@@ -172,6 +172,9 @@ updateSolvedTerm' xs x = updateSolved' xs x where

172 else (t, False)

173 updateSolved' xs t@(P _ n@(MN _ _) _)

174 | Just v <- lookup n xs = (v, True)

175+ updateSolved' xs t@(P nt n ty)

176+ = let (ty', ut) = updateSolved' xs ty in

177+ if ut then (P nt n ty', True) else (t, False)

175 updateSolved' xs t = (t, False)

178 updateSolved' xs t = (t, False)

176

179

177 updateSolvedB' xs b@(Let t v) = let (t', ut) = updateSolved' xs t

180 updateSolvedB' xs b@(Let t v) = let (t', ut) = updateSolved' xs t

src/Idris/Core/TT.hs+11−4

@@ -155,9 +155,11 @@ data Err' t

155 | WithFnType t

156 | NoTypeDecl Name

157 | NotInjective t t t

158− | CantResolve t

158+ | CantResolve Bool -- True if postponed, False if fatal

159+ t

159 | CantResolveAlts [Name]

160 | CantResolveAlts [Name]

160 | IncompleteTerm t

161 | IncompleteTerm t

162+ | NoEliminator String t

161 | UniverseError

163 | UniverseError

162 | UniqueError Universe Name

164 | UniqueError Universe Name

163 | UniqueKindError Universe Name

165 | UniqueKindError Universe Name

@@ -231,7 +233,7 @@ instance Sized Err where

231 size (NoSuchVariable name) = size name

233 size (NoSuchVariable name) = size name

232 size (NoTypeDecl name) = size name

234 size (NoTypeDecl name) = size name

233 size (NotInjective l c r) = size l + size c + size r

235 size (NotInjective l c r) = size l + size c + size r

234− size (CantResolve trm) = size trm

236+ size (CantResolve _ trm) = size trm

235 size (NoRewriting trm) = size trm

237 size (NoRewriting trm) = size trm

236 size (CantResolveAlts _) = 1

238 size (CantResolveAlts _) = 1

237 size (IncompleteTerm trm) = size trm

239 size (IncompleteTerm trm) = size trm

@@ -246,7 +248,7 @@ instance Sized Err where

246

248

247score :: Err -> Int

249score :: Err -> Int

248score (CantUnify _ _ _ m _ s) = s + score m

250score (CantUnify _ _ _ m _ s) = s + score m

249−score (CantResolve _) = 20

251+score (CantResolve _ _) = 20

250score (NoSuchVariable _) = 1000

252score (NoSuchVariable _) = 1000

251score (ProofSearchFail e) = score e

253score (ProofSearchFail e) = score e

252score (CantSolveGoal _ _) = 100000

254score (CantSolveGoal _ _) = 100000

@@ -507,7 +509,7 @@ toAlist :: Ctxt a -> [(Name, a)]

507toAlist ctxt = let allns = map snd (Map.toList ctxt) in

509toAlist ctxt = let allns = map snd (Map.toList ctxt) in

508 concatMap (Map.toList) allns

510 concatMap (Map.toList) allns

509

511

510−addAlist :: Show a => [(Name, a)] -> Ctxt a -> Ctxt a

512+addAlist :: [(Name, a)] -> Ctxt a -> Ctxt a

511addAlist [] ctxt = ctxt

513addAlist [] ctxt = ctxt

512addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)

514addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)

513

515

@@ -934,6 +936,7 @@ vinstances i t = 0

934-- | Replace the outermost (index 0) de Bruijn variable with the given term

936-- | Replace the outermost (index 0) de Bruijn variable with the given term

935instantiate :: TT n -> TT n -> TT n

937instantiate :: TT n -> TT n -> TT n

936instantiate e = subst 0 where

938instantiate e = subst 0 where

939+ subst i (P nt x ty) = P nt x (subst i ty)

937 subst i (V x) | i == x = e

940 subst i (V x) | i == x = e

938 subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)

941 subst i (Bind x b sc) = Bind x (fmap (subst i) b) (subst (i+1) sc)

939 subst i (App f a) = App (subst i f) (subst i a)

942 subst i (App f a) = App (subst i f) (subst i a)

@@ -945,6 +948,7 @@ instantiate e = subst 0 where

945-- that has been substituted.

948-- that has been substituted.

946substV :: TT n -> TT n -> TT n

949substV :: TT n -> TT n -> TT n

947substV x tm = dropV 0 (instantiate x tm) where

950substV x tm = dropV 0 (instantiate x tm) where

951+ subst i (P nt x ty) = P nt x (subst i ty)

948 dropV i (V x) | x > i = V (x - 1)

952 dropV i (V x) | x > i = V (x - 1)

949 | otherwise = V x

953 | otherwise = V x

950 dropV i (Bind x b sc) = Bind x (fmap (dropV i) b) (dropV (i+1) sc)

954 dropV i (Bind x b sc) = Bind x (fmap (dropV i) b) (dropV (i+1) sc)

@@ -1038,6 +1042,9 @@ subst n v tm = fst $ subst' 0 tm

1038 -- substitution happens...)

1042 -- substitution happens...)

1039 subst' i (V x) | i == x = (v, True)

1043 subst' i (V x) | i == x = (v, True)

1040 subst' i (P _ x _) | n == x = (v, True)

1044 subst' i (P _ x _) | n == x = (v, True)

1045+ subst' i t@(P nt x ty)

1046+ = let (ty', ut) = subst' i ty in

1047+ if ut then (P nt x ty', True) else (t, False)

1041 subst' i t@(Bind x b sc) | x /= n

1048 subst' i t@(Bind x b sc) | x /= n

1042 = let (b', ub) = substB' i b

1049 = let (b', ub) = substB' i b

1043 (sc', usc) = subst' (i+1) sc in

1050 (sc', usc) = subst' (i+1) sc in

src/Idris/Core/Unify.hs+2−2

@@ -100,7 +100,7 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

100 | (P (TCon _ _) _ _, _) <- unApply x,

101 holeIn env f || f `elem` holes

102 = let n' = uniqueName (sMN 0 "mv") (map fst env) in

103− checkCycle names (f, Bind n' (Lam t) x)

103+ checkCycle names (f, Bind n' (Lam t) x)

104 un names tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a) x

105 | (P (TCon _ _) _ _, _) <- unApply x,

106 holeIn env f || f `elem` holes

@@ -110,7 +110,7 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

110 | (P (DCon _ _ _) _ _, _) <- unApply x,

111 holeIn env f || f `elem` holes

112 = let n' = uniqueName (sMN 0 "mv") (map fst env) in

113− checkCycle names (f, Bind n' (Lam t) x)

113+ checkCycle names (f, Bind n' (Lam t) x)

114 un names tm@(App (P _ f (Bind fn (Pi _ t _) sc)) a) x

115 | (P (DCon _ _ _) _ _, _) <- unApply x,

116 holeIn env f || f `elem` holes

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/Delaborate.hs+7−1

@@ -289,7 +289,7 @@ pprintErr' i (NotInjective p x y) =

289 text "Can't verify injectivity of" <+> annTm p (pprintTerm i (delab i p)) <+>

290 text " when unifying" <+> annTm x (pprintTerm i (delab i x)) <+> text "and" <+>

291 annTm y (pprintTerm i (delab i y))

292−pprintErr' i (CantResolve c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

292+pprintErr' i (CantResolve _ c) = text "Can't resolve type class" <+> pprintTerm i (delab i c)

293pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

294 align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i) . annName) as)))

295pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

@@ -299,6 +299,12 @@ pprintErr' i (WithFnType ty) =

299pprintErr' i (CantMatch t) =

300 text "Can't match on" <+> annTm t (pprintTerm i (delab i t))

301pprintErr' i (IncompleteTerm t) = text "Incomplete term" <+> annTm t (pprintTerm i (delab i t))

302+pprintErr' i (NoEliminator s t)

303+ = text "No " <> text s <> text " for type " <+>

304+ annTm t (pprintTerm i (delab i t)) <$>

305+ text "Please note that 'induction' is experimental." <$>

306+ text "Only types declared with '%elim' can be used." <$>

307+ text "Consider writing a pattern matching definition instead."

302pprintErr' i UniverseError = text "Universe inconsistency"

308pprintErr' i UniverseError = text "Universe inconsistency"

303pprintErr' i (UniqueError NullType n)

309pprintErr' i (UniqueError NullType n)

304 = text "Borrowed name" <+> annName' n (showbasic n)

310 = text "Borrowed name" <+> annName' n (showbasic n)

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

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

51import Util.Pretty(pretty, text)

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

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

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/Clause.hs+34−22

@@ -455,8 +455,10 @@ checkPossible info fc tcgen fname lhs_in

455 -- if the LHS type checks, it is possible

456 case elaborate ctxt (sMN 0 "patLHS") infP initEState

457 (erun fc (buildTC i info ELHS [] fname (infTerm lhs))) of

458− OK ((lhs', _, _), _) ->

458+ OK (ElabResult lhs' _ _ ctxt' newDecls, _) ->

459+ do setContext ctxt'

460+ processTacticDecls newDecls

459− do let lhs_tm = orderPats (getInferTerm lhs')

461+ let lhs_tm = orderPats (getInferTerm lhs')

460 case recheck ctxt [] (forget lhs_tm) lhs_tm of

462 case recheck ctxt [] (forget lhs_tm) lhs_tm of

461 OK _ -> return True

463 OK _ -> return True

462 err -> return False

464 err -> return False

@@ -579,14 +581,15 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

579 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in ++

581 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show lhs_in ++

580 "\n" ++ show (fn_ty, fn_is))

582 "\n" ++ show (fn_ty, fn_is))

581

583

582− (((lhs', dlhs, []), probs, inj), _) <-

584+ ((ElabResult lhs' dlhs [] ctxt' newDecls, probs, inj), _) <-

583− tclift $ elaborate ctxt (sMN 0 "patLHS") infP initEState

585+ tclift $ elaborate ctxt (sMN 0 "patLHS") infP initEState

584− (do res <- errAt "left hand side of " fname

586+ (do res <- errAt "left hand side of " fname

585− (erun fc (buildTC i info ELHS opts fname (infTerm lhs)))

587+ (erun fc (buildTC i info ELHS opts fname (infTerm lhs)))

586− probs <- get_probs

588+ probs <- get_probs

587− inj <- get_inj

589+ inj <- get_inj

588− return (res, probs, inj))

590+ return (res, probs, inj))

589−

591+ setContext ctxt'

592+ processTacticDecls newDecls

590 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

593 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

591

594

592 let lhs_tm = orderPats (getInferTerm lhs')

595 let lhs_tm = orderPats (getInferTerm lhs')

@@ -653,13 +656,14 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

653 logLvl 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs

656 logLvl 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs

654 ctxt <- getContext -- new context with where block added

657 ctxt <- getContext -- new context with where block added

655 logLvl 5 "STARTING CHECK"

658 logLvl 5 "STARTING CHECK"

656− ((rhs', defer, is, probs), _) <-

659+ ((rhs', defer, is, probs, ctxt', newDecls), _) <-

657 tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty initEState

660 tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty initEState

658 (do pbinds ist lhs_tm

661 (do pbinds ist lhs_tm

659 mapM_ setinj (nub (params ++ inj))

662 mapM_ setinj (nub (params ++ inj))

660 setNextName

663 setNextName

664+ (ElabResult _ _ is ctxt' newDecls) <-

661− (_, _, is) <- errAt "right hand side of " fname

665+ errAt "right hand side of " fname

662− (erun fc (build i winfo ERHS opts fname rhs))

666+ (erun fc (build i winfo ERHS opts fname rhs))

663 errAt "right hand side of " fname

667 errAt "right hand side of " fname

664 (erun fc $ psolve lhs_tm)

668 (erun fc $ psolve lhs_tm)

665 hs <- get_holes

669 hs <- get_holes

@@ -668,8 +672,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

668 tt <- get_term

672 tt <- get_term

669 let (tm, ds) = runState (collectDeferred (Just fname) tt) []

673 let (tm, ds) = runState (collectDeferred (Just fname) tt) []

670 probs <- get_probs

674 probs <- get_probs

671− return (tm, ds, is, probs))

675+ return (tm, ds, is, probs, ctxt', newDecls))

672−

676+ setContext ctxt'

677+ processTacticDecls newDecls

673 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

678 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

674

679

675 logLvl 5 "DONE CHECK"

680 logLvl 5 "DONE CHECK"

@@ -812,10 +817,12 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

812 let params = getParamsInType i [] fn_is fn_ty

817 let params = getParamsInType i [] fn_is fn_ty

813 let lhs = stripLinear i $ stripUnmatchable i $ propagateParams i params fn_ty (addImplPat i lhs_in)

818 let lhs = stripLinear i $ stripUnmatchable i $ propagateParams i params fn_ty (addImplPat i lhs_in)

814 logLvl 2 ("LHS: " ++ show lhs)

819 logLvl 2 ("LHS: " ++ show lhs)

815− ((lhs', dlhs, []), _) <-

820+ (ElabResult lhs' dlhs [] ctxt' newDecls, _) <-

816 tclift $ elaborate ctxt (sMN 0 "patLHS") infP initEState

821 tclift $ elaborate ctxt (sMN 0 "patLHS") infP initEState

817 (errAt "left hand side of with in " fname

822 (errAt "left hand side of with in " fname

818 (erun fc (buildTC i info ELHS opts fname (infTerm lhs))) )

823 (erun fc (buildTC i info ELHS opts fname (infTerm lhs))) )

824+ setContext ctxt'

825+ processTacticDecls newDecls

819 let lhs_tm = orderPats (getInferTerm lhs')

826 let lhs_tm = orderPats (getInferTerm lhs')

820 let lhs_ty = getInferType lhs'

827 let lhs_ty = getInferType lhs'

821 let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))

828 let ret_ty = getRetTy (explicitNames (normalise ctxt [] lhs_ty))

@@ -827,17 +834,19 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

827 let wval = addImplBound i (map fst bargs) wval_in

834 let wval = addImplBound i (map fst bargs) wval_in

828 logLvl 5 ("Checking " ++ showTmImpls wval)

835 logLvl 5 ("Checking " ++ showTmImpls wval)

829 -- Elaborate wval in this context

836 -- Elaborate wval in this context

830− ((wval', defer, is), _) <-

837+ ((wval', defer, is, ctxt', newDecls), _) <-

831 tclift $ elaborate ctxt (sMN 0 "withRHS")

838 tclift $ elaborate ctxt (sMN 0 "withRHS")

832 (bindTyArgs PVTy bargs infP) initEState

839 (bindTyArgs PVTy bargs infP) initEState

833 (do pbinds i lhs_tm

840 (do pbinds i lhs_tm

834 setNextName

841 setNextName

835 -- TODO: may want where here - see winfo abpve

842 -- TODO: may want where here - see winfo abpve

836− (_', d, is) <- errAt "with value in " fname

843+ (ElabResult _ d is ctxt' newDecls) <- errAt "with value in " fname

837 (erun fc (build i info ERHS opts fname (infTerm wval)))

844 (erun fc (build i info ERHS opts fname (infTerm wval)))

838 erun fc $ psolve lhs_tm

845 erun fc $ psolve lhs_tm

839 tt <- get_term

846 tt <- get_term

840− return (tt, d, is))

847+ return (tt, d, is, ctxt', newDecls))

848+ setContext ctxt'

849+ processTacticDecls newDecls

841 def' <- checkDef fc defer

850 def' <- checkDef fc defer

842 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

851 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

843 addDeferred def''

852 addDeferred def''

@@ -923,14 +932,17 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

923 logLvl 5 ("New RHS " ++ showTmImpls rhs)

932 logLvl 5 ("New RHS " ++ showTmImpls rhs)

924 ctxt <- getContext -- New context with block added

933 ctxt <- getContext -- New context with block added

925 i <- getIState

934 i <- getIState

926− ((rhs', defer, is), _) <-

935+ ((rhs', defer, is, ctxt', newDecls), _) <-

927 tclift $ elaborate ctxt (sMN 0 "wpatRHS") clhsty initEState

936 tclift $ elaborate ctxt (sMN 0 "wpatRHS") clhsty initEState

928 (do pbinds i lhs_tm

937 (do pbinds i lhs_tm

929 setNextName

938 setNextName

930− (_, d, is) <- erun fc (build i info ERHS opts fname rhs)

939+ (ElabResult _ d is ctxt' newDecls) <- erun fc (build i info ERHS opts fname rhs)

931 psolve lhs_tm

940 psolve lhs_tm

932 tt <- get_term

941 tt <- get_term

933− return (tt, d, is))

942+ return (tt, d, is, ctxt', newDecls))

943+ setContext ctxt'

944+ processTacticDecls newDecls

945+

934 def' <- checkDef fc defer

946 def' <- checkDef fc defer

935 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

947 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, False))) def'

936 addDeferred def''

948 addDeferred def''

src/Idris/Elab/Instance.hs+23−11

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

@@ -169,31 +169,43 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

169 ty' <- implicit info syn iname ty'

170 let ty = addImpl i ty'

171 ctxt <- getContext

172− ((tyT, _, _), _) <-

172+ (ElabResult tyT _ _ ctxt' newDecls, _) <-

173− tclift $ elaborate ctxt iname (TType (UVal 0)) initEState

173+ tclift $ elaborate ctxt iname (TType (UVal 0)) initEState

174− (errAt "type of " iname (erun fc (build i info ERHS [] iname ty)))

174+ (errAt "type of " iname (erun fc (build i info ERHS [] iname ty)))

175+ setContext ctxt'

176+ processTacticDecls newDecls

175 ctxt <- getContext

177 ctxt <- getContext

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

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

177 let nty = normalise ctxt [] cty

179 let nty = normalise ctxt [] cty

178− 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)

179

181

180− findOverlapping i t n

182+ findOverlapping i dets t n

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

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

182 | otherwise

184 | otherwise

183 = case lookupTy n (tt_ctxt i) of

185 = case lookupTy n (tt_ctxt i) of

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

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

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

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

186− case matchClause i tret' tret of

188+ case matchArgs i dets tret' tret of

187− Right ms -> Just tret'

189+ Right _ -> Just tret'

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

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

189− Right ms -> Just tret'

191+ Right _ -> Just tret'

190− Left _ -> Nothing

192+ Left _ -> Nothing

191 _ -> Nothing

193 _ -> Nothing

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

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

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

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

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

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

195 getRetType t = t

197 getRetType t = t

196

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+

197 mkMethApp (n, _, _, ty)

209 mkMethApp (n, _, _, ty)

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

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

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

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

src/Idris/Elab/Transform.hs+10−4

@@ -53,10 +53,12 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

53 = do ctxt <- getContext

54 i <- getIState

55 let lhs = addImplPat i lhs_in

56− ((lhs', dlhs, []), _) <-

56+ (ElabResult lhs' dlhs [] ctxt' newDecls, _) <-

57 tclift $ elaborate ctxt (sMN 0 "transLHS") infP initEState

58 (erun fc (buildTC i info ELHS [] (sUN "transform")

59 (infTerm lhs)))

60+ setContext ctxt'

61+ processTacticDecls newDecls

60 let lhs_tm = orderPats (getInferTerm lhs')

62 let lhs_tm = orderPats (getInferTerm lhs')

61 let lhs_ty = getInferType lhs'

63 let lhs_ty = getInferType lhs'

62 let newargs = pvars i lhs_tm

64 let newargs = pvars i lhs_tm

@@ -66,14 +68,18 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

66 logLvl 3 ("Transform LHS " ++ show clhs_tm)

68 logLvl 3 ("Transform LHS " ++ show clhs_tm)

68 let rhs = addImplBound i (map fst newargs) rhs_in

70 let rhs = addImplBound i (map fst newargs) rhs_in

69− ((rhs', defer), _) <-

71+ ((rhs', defer, ctxt', newDecls), _) <-

70 tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty initEState

72 tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty initEState

71 (do pbinds i lhs_tm

73 (do pbinds i lhs_tm

72 setNextName

74 setNextName

73− erun fc (build i info ERHS [] (sUN "transform") rhs)

75+ (ElabResult _ _ _ ctxt' newDecls) <- erun fc (build i info ERHS [] (sUN "transform") rhs)

74 erun fc $ psolve lhs_tm

76 erun fc $ psolve lhs_tm

75 tt <- get_term

77 tt <- get_term

76− return (runState (collectDeferred Nothing tt) []))

78+ let (rhs', defer) = runState (collectDeferred Nothing tt) []

79+ return (rhs', defer, ctxt', newDecls))

80+ setContext ctxt'

81+ processTacticDecls newDecls

82+

77 (crhs_tm_in, crhs_ty) <- recheckC fc [] rhs'

83 (crhs_tm_in, crhs_ty) <- recheckC fc [] rhs'

78 let crhs_tm = renamepats pnames crhs_tm_in

84 let crhs_tm = renamepats pnames crhs_tm_in

79 logLvl 3 ("Transform RHS " ++ show crhs_tm)

85 logLvl 3 ("Transform RHS " ++ show crhs_tm)

src/Idris/Elab/Type.hs+10−6

@@ -65,9 +65,11 @@ buildType info syn fc opts n ty' = do

65 logLvl 3 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

66 logLvl 3 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

68− ((tyT', defer, is), log) <-

68+ (ElabResult tyT' defer is ctxt' newDecls, log) <-

69− tclift $ elaborate ctxt n (TType (UVal 0)) initEState

69+ tclift $ elaborate ctxt n (TType (UVal 0)) initEState

70− (errAt "type of " n (erun fc (build i info ETyDecl [] n ty)))

70+ (errAt "type of " n (erun fc (build i info ETyDecl [] n ty)))

71+ setContext ctxt'

72+ processTacticDecls newDecls

72 let tyT = patToImp tyT'

74 let tyT = patToImp tyT'

@@ -114,12 +116,14 @@ buildType info syn fc opts n ty' = do

114 param_pos i ns t = []

116 param_pos i ns t = []

115

117

116-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

118-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

119+elabType :: ElabInfo -> SyntaxInfo

117−elabType :: ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm)-> [(Name, Docstring (Either Err PTerm))] ->

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

118− FC -> FnOpts -> Name -> PTerm -> Idris Type

121+ -> FC -> FnOpts -> Name -> PTerm -> Idris Type

119elabType = elabType' False

122elabType = elabType' False

120

123

121elabType' :: Bool -> -- normalise it

124elabType' :: Bool -> -- normalise it

125+ ElabInfo -> SyntaxInfo ->

122− ElabInfo -> SyntaxInfo -> Docstring (Either Err PTerm) -> [(Name, Docstring (Either Err PTerm))] ->

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

123 FC -> FnOpts -> Name -> PTerm -> Idris Type

127 FC -> FnOpts -> Name -> PTerm -> Idris Type

124elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

128elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params info) ty_in

125 n = liftname info n_in in -}

129 n = liftname info n_in in -}

src/Idris/Elab/Utils.hs+10−8

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

23import qualified Data.Map as Map

25−recheckC = recheckC_borrowing False []

25+recheckC = recheckC_borrowing False []

27recheckC_borrowing uniq_check bs fc env t

28 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)

@@ -34,9 +34,13 @@ recheckC_borrowing uniq_check bs fc env t

34 addConstraints fc cs

35 return (tm, ty)

37−

37+checkDef :: FC -> [(Name, (Int, Maybe Name, Type))]

38+ -> Idris [(Name, (Int, Maybe Name, Type))]

38checkDef fc ns = checkAddDef False True fc ns

39checkDef fc ns = checkAddDef False True fc ns

41+checkAddDef :: Bool -> Bool -> FC

42+ -> [(Name, (Int, Maybe Name, Type))]

43+ -> Idris [(Name, (Int, Maybe Name, Type))]

40checkAddDef add toplvl fc [] = return []

44checkAddDef add toplvl fc [] = return []

41checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

45checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

42 = do ctxt <- getContext

46 = do ctxt <- getContext

@@ -46,7 +50,7 @@ checkAddDef add toplvl fc ((n, (i, top, t)) : ns)

46 ns' <- checkAddDef add toplvl fc ns

50 ns' <- checkAddDef add toplvl fc ns

47 return ((n, (i, top, t')) : ns')

51 return ((n, (i, top, t')) : ns')

49−-- Get the list of (index, name) of inaccessible arguments from an elaborated

53+-- | Get the list of (index, name) of inaccessible arguments from an elaborated

50-- type

54-- type

51inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)]

55inaccessibleImps :: Int -> Type -> [Bool] -> [(Int, Name)]

52inaccessibleImps i (Bind n (Pi _ t _) sc) (inacc : ins)

56inaccessibleImps i (Bind n (Pi _ t _) sc) (inacc : ins)

@@ -54,7 +58,7 @@ inaccessibleImps i (Bind n (Pi _ t _) sc) (inacc : ins)

54 | otherwise = inaccessibleImps (i + 1) sc ins

58 | otherwise = inaccessibleImps (i + 1) sc ins

55inaccessibleImps _ _ _ = []

59inaccessibleImps _ _ _ = []

57−-- Get the list of (index, name) of inaccessible arguments from the type.

61+-- | Get the list of (index, name) of inaccessible arguments from the type.

58inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]

62inaccessibleArgs :: Int -> PTerm -> [(Int, Name)]

59inaccessibleArgs i (PPi (Imp _ _ _ _) n Placeholder t)

63inaccessibleArgs i (PPi (Imp _ _ _ _) n Placeholder t)

60 = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit

64 = (i,n) : inaccessibleArgs (i+1) t -- unbound implicit

@@ -74,10 +78,9 @@ elabCaseBlock info opts d@(PClauses f o n ps)

74 when (AssertTotal `elem` opts) $ setFlags n [AssertTotal]

78 when (AssertTotal `elem` opts) $ setFlags n [AssertTotal]

75 rec_elabDecl info EAll info (PClauses f opts' n ps )

79 rec_elabDecl info EAll info (PClauses f opts' n ps )

77−-- Check that the result of type checking matches what the programmer wrote

81+-- | Check that the result of type checking matches what the programmer wrote

78-- (i.e. - if we inferred any arguments that the user provided, make sure

82-- (i.e. - if we inferred any arguments that the user provided, make sure

79-- they are the same!)

83-- they are the same!)

80−

81checkInferred :: FC -> PTerm -> PTerm -> Idris ()

84checkInferred :: FC -> PTerm -> PTerm -> Idris ()

82checkInferred fc inf user =

85checkInferred fc inf user =

83 do logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n\nFROM\n\n" ++

86 do logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n\nFROM\n\n" ++

@@ -92,9 +95,8 @@ checkInferred fc inf user =

92 logLvl 10 $ "Checked match"

95 logLvl 10 $ "Checked match"

93-- ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user)

96-- ++ "\n" ++ showImp True inf ++ "\n" ++ showImp True user)

95−-- Return whether inferred term is different from given term

98+-- | Return whether inferred term is different from given term

96-- (as above, but return a Bool)

99-- (as above, but return a Bool)

97−

98inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool

100inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool

99inferredDiff fc inf user =

101inferredDiff fc inf user =

100 do i <- getIState

102 do i <- getIState

src/Idris/Elab/Value.hs+8−3

@@ -63,9 +63,14 @@ elabValBind info aspat norm tm_in

63 -- * elaboration as a Type

64 -- * elaboration as a function a -> b

66− ((tm', defer, is), _) <-

66+ (ElabResult tm' defer is ctxt' newDecls, _) <-

67− tclift (elaborate ctxt (sMN 0 "val") infP initEState

67+ tclift (elaborate ctxt (sMN 0 "val") infP initEState

68− (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))

68+ (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))

69+

70+ -- Extend the context with new definitions created

71+ setContext ctxt'

72+ processTacticDecls newDecls

73+

69 let vtm = orderPats (getInferTerm tm')

74 let vtm = orderPats (getInferTerm tm')

71 def' <- checkDef (fileFC "(input)") defer

76 def' <- checkDef (fileFC "(input)") defer

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+209−81

@@ -18,6 +18,7 @@ import Idris.Core.Typecheck (check, recheck)

18import Idris.ErrReverse (errReverse)

19import Idris.ElabQuasiquote (extractUnquotes)

20import Idris.Elab.Utils

21+import Idris.Reflection

21import qualified Util.Pretty as U

22import qualified Util.Pretty as U

23import Control.Applicative ((<$>))

24import Control.Applicative ((<$>))

@@ -36,6 +37,32 @@ import Debug.Trace

36data ElabMode = ETyDecl | ELHS | ERHS

37data ElabMode = ETyDecl | ELHS | ERHS

37 deriving Eq

38 deriving Eq

40+data ElabResult =

41+ ElabResult { resultTerm :: Term -- ^ The term resulting from elaboration

42+ , resultMetavars :: [(Name, (Int, Maybe Name, Type))]

43+ -- ^ Information about new metavariables

44+ , resultCaseDecls :: [PDecl]

45+ -- ^ Deferred declarations as the meaning of case blocks

46+ , resultContext :: Context

47+ -- ^ The potentially extended context from new definitions

48+ , resultTyDecls :: [(Name, FC, [PArg], Type)]

49+ -- ^ Meta-info about the new type declarations

50+ }

51+

52+processTacticDecls :: [(Name, FC, [PArg], Type)] -> Idris ()

53+processTacticDecls info =

54+ forM_ info $ \(n, fc, impls, ty) ->

55+ do logLvl 3 $ "Declaration from tactics: " ++ show n ++ " : " ++ show ty

56+ logLvl 3 $ " It has impls " ++ show impls

57+ updateIState $ \i -> i { idris_implicits =

58+ addDef n impls (idris_implicits i) }

59+ addIBC (IBCImp n)

60+ ds <- checkDef fc [(n, (-1, Nothing, ty))]

61+ addIBC (IBCDef n)

62+ let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

63+ addDeferred ds'

64+

65+

39-- Using the elaborator, convert a term in raw syntax to a fully

66-- Using the elaborator, convert a term in raw syntax to a fully

40-- elaborated, typechecked term.

67-- elaborated, typechecked term.

41--

68--

@@ -45,7 +72,7 @@ data ElabMode = ETyDecl | ELHS | ERHS

45-- Also find deferred names in the term and their types

72-- Also find deferred names in the term and their types

47build :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

74build :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

48− ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

75+ ElabD ElabResult

49build ist info emode opts fn tm

76build ist info emode opts fn tm

50 = do elab ist info emode opts fn tm

77 = do elab ist info emode opts fn tm

51 let tmIn = tm

78 let tmIn = tm

@@ -64,7 +91,7 @@ build ist info emode opts fn tm

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

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

65 do focus n

92 do focus n

66 g <- goal

93 g <- goal

67− try (resolveTC True 7 g fn ist)

94+ try (resolveTC True False 7 g fn ist)

68 (movelast n)) ivs

95 (movelast n)) ivs

69 ivs <- get_instances

96 ivs <- get_instances

70 hs <- get_holes

97 hs <- get_holes

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

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

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

73 do focus n

100 do focus n

74 g <- goal

101 g <- goal

102+ ptm <- get_term

75− resolveTC True 7 g fn ist) ivs

103+ resolveTC True True 7 g fn ist) ivs

76 tm <- get_term

104 tm <- get_term

77 ctxt <- get_context

105 ctxt <- get_context

78 probs <- get_probs

106 probs <- get_probs

@@ -94,12 +122,13 @@ build ist info emode opts fn tm

94 when tydecl (do update_term orderPats

122 when tydecl (do update_term orderPats

95 mkPat)

123 mkPat)

96-- update_term liftPats)

124-- update_term liftPats)

97− EState is _ <- getAux

125+ EState is _ impls <- getAux

98 tt <- get_term

126 tt <- get_term

99 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

127 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

100 log <- getLog

128 log <- getLog

129+ ctxt <- get_context

101− if (log /= "") then trace log $ return (tm, ds, is)

130+ if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)

102− else return (tm, ds, is)

131+ else return (ElabResult tm ds is ctxt impls)

103 where pattern = emode == ELHS

132 where pattern = emode == ELHS

104 tydecl = emode == ETyDecl

133 tydecl = emode == ETyDecl

105

134

@@ -114,7 +143,7 @@ build ist info emode opts fn tm

114-- know about yet on the LHS of a pattern def)

143-- know about yet on the LHS of a pattern def)

115

144

116buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

145buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

117− ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])

146+ ElabD ElabResult

118buildTC ist info emode opts fn tm

147buildTC ist info emode opts fn tm

119 = do -- set name supply to begin after highest index in tm

148 = do -- set name supply to begin after highest index in tm

120 let ns = allNamesIn tm

149 let ns = allNamesIn tm

@@ -135,12 +164,13 @@ buildTC ist info emode opts fn tm

135 -- unification

164 -- unification

136 when (not (null dots)) $

165 when (not (null dots)) $

137 lift (Error (CantMatch (getInferTerm tm)))

166 lift (Error (CantMatch (getInferTerm tm)))

138− EState is _ <- getAux

167+ EState is _ impls <- getAux

139 tt <- get_term

168 tt <- get_term

140 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

169 let (tm, ds) = runState (collectDeferred (Just fn) tt) []

141 log <- getLog

170 log <- getLog

171+ ctxt <- get_context

142− if (log /= "") then trace log $ return (tm, ds, is)

172+ if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)

143− else return (tm, ds, is)

173+ else return (ElabResult tm ds is ctxt impls)

144 where pattern = emode == ELHS

174 where pattern = emode == ELHS

145

175

146-- return whether arguments of the given constructor name can be

176-- return whether arguments of the given constructor name can be

@@ -183,9 +213,9 @@ goal_polymorphic =

183 _ -> return True

213 _ -> return True

184 _ -> return False

214 _ -> return False

185

215

186−-- Returns the set of declarations we need to add to complete the definition

216+-- | Returns the set of declarations we need to add to complete the

187−-- (most likely case blocks to elaborate)

217+-- definition (most likely case blocks to elaborate) as well as

188−

218+-- declarations resulting from user tactic scripts (%runTactics)

189elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

219elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->

190 ElabD ()

220 ElabD ()

191elab ist info emode opts fn tm

221elab ist info emode opts fn tm

@@ -321,7 +351,7 @@ elab ist info emode opts fn tm

321 UType _ -> elab' ina (Just fc) (PRef fc unitTy)

351 UType _ -> elab' ina (Just fc) (PRef fc unitTy)

322 _ -> elab' ina (Just fc) (PRef fc unitCon)

352 _ -> elab' ina (Just fc) (PRef fc unitCon)

323 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

353 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

324− = do g <- goal; resolveTC False 5 g fn ist

354+ = do g <- goal; resolveTC False False 5 g fn ist

325 elab' ina fc (PResolveTC fc')

355 elab' ina fc (PResolveTC fc')

326 = do c <- getNameFrom (sMN 0 "class")

356 = do c <- getNameFrom (sMN 0 "class")

327 instanceArg c

357 instanceArg c

@@ -540,7 +570,7 @@ elab ist info emode opts fn tm

540 g <- goal

570 g <- goal

541 hs <- get_holes

571 hs <- get_holes

542 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)

572 if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)

543− then try (resolveTC True 7 g fn ist)

573+ then try (resolveTC True False 7 g fn ist)

544 (movelast n)

574 (movelast n)

545 else movelast n)

575 else movelast n)

546 (ivs' \\ ivs)

576 (ivs' \\ ivs)

@@ -700,7 +730,7 @@ elab ist info emode opts fn tm

700 env <- get_env

730 env <- get_env

701 hs <- get_holes

731 hs <- get_holes

702 if all (\n -> not (n `elem` hs)) (freeNames g)

732 if all (\n -> not (n `elem` hs)) (freeNames g)

703− then try (resolveTC False 7 g fn ist)

733+ then try (resolveTC False False 7 g fn ist)

704 (movelast n)

734 (movelast n)

705 else movelast n)

735 else movelast n)

706 (ivs' \\ ivs)

736 (ivs' \\ ivs)

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

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

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

966 elab' ina fc t

996 elab' ina fc t

967 unifyLog False

997 unifyLog False

968− elab' ina fc (PQuasiquote t goal)

998+ elab' ina fc (PQuasiquote t goalt)

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

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

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

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

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

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

1002+ finalTy <- goal

972 (t, unq) <- extractUnquotes 0 t

1003 (t, unq) <- extractUnquotes 0 t

973 let unquoteNames = map fst unq

1004 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

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

978−

979

1006

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

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

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

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

1010 letbind nTm (Var qTy) (Var qTm)

1037 letbind nTm (Var qTy) (Var qTm)

1011

1038

1012 -- Fill out the goal type, if relevant

1039 -- Fill out the goal type, if relevant

1013− case goal of

1040+ case goalt of

1014 Nothing -> return ()

1041 Nothing -> return ()

1015 Just gTy -> do focus qTy

1042 Just gTy -> do focus qTy

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

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

@@ -1025,18 +1052,20 @@ elab ist info emode opts fn tm

1025 env <- get_env

1052 env <- get_env

1026 loadState

1053 loadState

1027 let quoted = fmap (explicitNames . binderVal) $ lookup nTm env

1054 let quoted = fmap (explicitNames . binderVal) $ lookup nTm env

1028−

1055+ isRaw = case unApply (normaliseAll ctxt env finalTy) of

1056+ (P _ n _, []) | n == reflm "Raw" -> True

1057+ _ -> False

1029 case quoted of

1058 case quoted of

1030 Just q -> do ctxt <- get_context

1059 Just q -> do ctxt <- get_context

1031 (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q

1060 (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q

1032 if pattern

1061 if pattern

1062+ then if isRaw

1063+ then reflectRawQuotePattern unquoteNames (forget q')

1033− then do try' (reflectTTQuotePattern unquoteNames q')

1064+ else reflectTTQuotePattern unquoteNames q'

1034− (reflectRawQuotePattern unquoteNames (forget q'))

1065+ else do if isRaw

1035− True

1036− else do try' (fill $ reflectTTQuote unquoteNames q')

1037− -- we forget q' instead of using q to ensure rechecking

1066+ then -- we forget q' instead of using q to ensure rechecking

1038− (fill $ reflectRawQuote unquoteNames (forget q'))

1067+ fill $ reflectRawQuote unquoteNames (forget q')

1039− True -- ignore errors like proof search does

1068+ else fill $ reflectTTQuote unquoteNames q'

1040 solve

1069 solve

1041

1070

1042 Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"

1071 Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"

@@ -1077,8 +1106,8 @@ elab ist info emode opts fn tm

1077 focus n

1106 focus n

1078 elab' ina (Just fc') tm

1107 elab' ina (Just fc') tm

1079 env <- get_env

1108 env <- get_env

1080− ctxt <- get_context

1081− runTactical (maybe fc' id fc) ctxt env (P Bound n' Erased)

1109+ runTactical (maybe fc' id fc) env (P Bound n' Erased)

1110+ EState _ _ todo <- getAux

1082 solve

1111 solve

1083 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

1112 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x

1084

1113

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

1346findInstances ist t

1375findInstances ist t

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

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

1348 = case lookupCtxt n (idris_classes ist) of

1377 = case lookupCtxt n (idris_classes ist) of

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

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

1350 _ -> []

1379 _ -> []

1351 | otherwise = []

1380 | otherwise = []

1352

1381

@@ -1376,14 +1405,26 @@ proofSearch' ist rec ambigok depth prv top n hints

1376-- Resolve type classes. This will only pick up 'normal' instances, never

1405-- Resolve type classes. This will only pick up 'normal' instances, never

1377-- named instances (hence using 'tcname' to check it's a generated instance

1406-- named instances (hence using 'tcname' to check it's a generated instance

1378-- name).

1407-- name).

1408+resolveTC :: Bool -- using default Int

1409+ -> Bool -- allow metavariables in the goal

1410+ -> Int -- depth

1411+ -> Term -- top level goal

1412+ -> Name -- top level function name

1379−resolveTC :: Bool -> Int -> Term -> Name -> IState -> ElabD ()

1413+ -> IState -> ElabD ()

1380−resolveTC = resTC' []

1414+resolveTC def mvok depth top fn ist

1381−

1415+ = do hs <- get_holes

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

1417+

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

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

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

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

1384−resTC' tcs defaultOn depth topg fn ist

1420+resTC' tcs defaultOn topholes depth topg fn ist

1385− = do compute

1421+ = do compute

1386− g <- goal

1422+ g <- goal

1423+ let argsok = tcArgsOK g topholes

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

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

1426+ then lift $ tfail $ CantResolve True topg

1427+ else do

1387 ptm <- get_term

1428 ptm <- get_term

1388 ulog <- getUnifyLog

1429 ulog <- getUnifyLog

1389 hs <- get_holes

1430 hs <- get_holes

@@ -1400,6 +1441,31 @@ resTC' tcs defaultOn depth topg fn ist

1400 let depth' = if scopeOnly then 2 else depth

1441 let depth' = if scopeOnly then 2 else depth

1401 blunderbuss t depth' stk (stk ++ insts)) True

1442 blunderbuss t depth' stk (stk ++ insts)) True

1402 where

1443 where

1444+ tcArgsOK ty hs | (P _ nc _, as) <- unApply ty, nc == numclass && defaultOn

1445+ = True

1446+ tcArgsOK ty hs -- if any arguments are metavariables, postpone

1447+ = let (f, as) = unApply ty in

1448+ case f of

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

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

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

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

1453+

1454+ tcDetArgsOK i ds hs (x : xs)

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

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

1457+ tcDetArgsOK _ _ _ [] = True

1458+

1459+ isMeta :: [Name] -> Term -> Bool

1460+ isMeta ns (P _ n _) = n `elem` ns

1461+ isMeta _ _ = False

1462+

1463+ notHole hs (P _ n _, c)

1464+ | (P _ cn _, _) <- unApply c,

1465+ n `elem` hs && isConName cn (tt_ctxt ist) = False

1466+ | Constant _ <- c = not (n `elem` hs)

1467+ notHole _ _ = True

1468+

1403 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

1469 elabTC n | n /= fn && tcname n = (resolve n depth, show n)

1404 | otherwise = (fail "Can't resolve", show n)

1470 | otherwise = (fail "Can't resolve", show n)

1405

1471

@@ -1427,10 +1493,13 @@ resTC' tcs defaultOn depth topg fn ist

1427

1493

1428 blunderbuss t d stk [] = do -- c <- get_env

1494 blunderbuss t d stk [] = do -- c <- get_env

1429 -- ps <- get_probs

1495 -- ps <- get_probs

1430− lift $ tfail $ CantResolve topg

1496+ lift $ tfail $ CantResolve False topg

1431 blunderbuss t d stk (n:ns)

1497 blunderbuss t d stk (n:ns)

1432 | n /= fn && (n `elem` stk || tcname n)

1498 | n /= fn && (n `elem` stk || tcname n)

1499+ = tryCatch (resolve n d)

1500+ (\e -> case e of

1501+ CantResolve True _ -> lift $ tfail e

1433− = try' (resolve n d) (blunderbuss t d stk ns) True

1502+ _ -> blunderbuss t d stk ns)

1434 | otherwise = blunderbuss t d stk ns

1503 | otherwise = blunderbuss t d stk ns

1435

1504

1436 resolve n depth

1505 resolve n depth

@@ -1459,7 +1528,7 @@ resTC' tcs defaultOn depth topg fn ist

1459 let got = fst (unApply t)

1528 let got = fst (unApply t)

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

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

1461 then depth - 1 else depth

1530 then depth - 1 else depth

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

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

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

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

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

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

1465 hs <- get_holes

1534 hs <- get_holes

@@ -1505,11 +1574,17 @@ case_ ind autoSolve ist fn tm = do

1505 else casetac (forget val)

1574 else casetac (forget val)

1506 when autoSolve solveAll

1575 when autoSolve solveAll

1507

1576

1577+tacN :: String -> Name

1578+tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]

1579+

1508−runTactical :: FC -> Context -> Env -> Term -> ElabD ()

1580+runTactical :: FC -> Env -> Term -> ElabD ()

1509−runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

1581+runTactical fc env tm = do tm' <- eval tm

1582+ runTacTm tm'

1583+ return ()

1510 where

1584 where

1585+ eval tm = do ctxt <- get_context

1511− eval = normaliseAll ctxt env . finalise

1586+ return $ normaliseAll ctxt env (finalise tm)

1512− tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]

1587+

1513 returnUnit = fmap fst $ get_type_val (Var unitCon)

1588 returnUnit = fmap fst $ get_type_val (Var unitCon)

1514

1589

1515 -- | Do a step in the reflected elaborator monad. The input is the

1590 -- | Do a step in the reflected elaborator monad. The input is the

@@ -1547,26 +1622,31 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

1547 = do env <- get_env

1622 = do env <- get_env

1548 fmap fst . get_type_val $ reflectEnv env

1623 fmap fst . get_type_val $ reflectEnv env

1549 | n == tacN "prim__Fail", [_a, errs] <- args

1624 | n == tacN "prim__Fail", [_a, errs] <- args

1625+ = do errs' <- eval errs

1550− = do parts <- reifyReportParts (eval errs)

1626+ parts <- reifyReportParts errs'

1551 lift . tfail $ ReflectionError [parts] (Msg "")

1627 lift . tfail $ ReflectionError [parts] (Msg "")

1552 | n == tacN "prim__PureTactical", [_a, tm] <- args

1628 | n == tacN "prim__PureTactical", [_a, tm] <- args

1553 = return tm

1629 = return tm

1554 | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args

1630 | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args

1555− = do let first' = eval first

1631+ = do first' <- eval first

1556 res <- runTacTm first'

1632 res <- runTacTm first'

1557− let next = eval (App andThen res)

1633+ next <- eval (App andThen res)

1558 runTacTm next

1634 runTacTm next

1559 | n == tacN "prim__Try", [_a, first, alt] <- args

1635 | n == tacN "prim__Try", [_a, first, alt] <- args

1560− = do let first' = eval first

1636+ = do first' <- eval first

1561− let alt' = eval alt

1637+ alt' <- eval alt

1562 try' (runTacTm first') (runTacTm alt') True

1638 try' (runTacTm first') (runTacTm alt') True

1563 | n == tacN "prim__Fill", [raw] <- args

1639 | n == tacN "prim__Fill", [raw] <- args

1564 = do raw' <- reifyRaw raw

1640 = do raw' <- reifyRaw raw

1565 apply raw' []

1641 apply raw' []

1566 returnUnit

1642 returnUnit

1567− | n == tacN "prim__Gensym", [eval -> Constant (Str hint)] <- args

1643+ | n == tacN "prim__Gensym", [hint] <- args

1644+ = do hintStr <- eval hint

1645+ case hintStr of

1646+ Constant (Str h) -> do

1568− = do n <- getNameFrom (sMN 0 hint)

1647+ n <- getNameFrom (sMN 0 h)

1569− fmap fst $ get_type_val (reflectName n)

1648+ fmap fst $ get_type_val (reflectName n)

1649+ _ -> fail "no hint"

1570 | n == tacN "prim__Claim", [n, ty] <- args

1650 | n == tacN "prim__Claim", [n, ty] <- args

1571 = do n' <- reifyTTName n

1651 = do n' <- reifyTTName n

1572 ty' <- reifyRaw ty

1652 ty' <- reifyRaw ty

@@ -1596,6 +1676,29 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()

1596 Just name -> fmap Just $ reifyTTName name

1676 Just name -> fmap Just $ reifyTTName name

1597 intro n

1677 intro n

1598 returnUnit

1678 returnUnit

1679+ | n == tacN "prim__DeclareType", [decl] <- args

1680+ = do (RDeclare n args res) <- reifyTyDecl decl

1681+ ctxt <- get_context

1682+ let mkPi arg res = RBind (argName arg)

1683+ (Pi Nothing (argTy arg) (RUType AllTypes))

1684+ res

1685+ rty = foldr mkPi res args

1686+ (checked, ty') <- lift $ check ctxt [] rty

1687+ case normaliseAll ctxt [] (finalise ty') of

1688+ TType _ -> lift . tfail . InternalMsg $

1689+ show checked ++ " is not a type: it's " ++ show ty'

1690+ _ -> return ()

1691+ case lookupDefExact n ctxt of

1692+ Just _ -> lift . tfail . InternalMsg $

1693+ show n ++ " is already defined."

1694+ Nothing -> return ()

1695+ let decl = TyDecl Ref checked

1696+ ctxt' = addCtxtDef n decl ctxt

1697+ set_context ctxt'

1698+ updateAux $ \e -> e { new_tyDecls = (n, fc, map rArgToPArg args, checked) :

1699+ new_tyDecls e }

1700+ aux <- getAux

1701+ returnUnit

1599 | n == tacN "prim__Debug", [ty, msg] <- args

1702 | n == tacN "prim__Debug", [ty, msg] <- args

1600 = do let msg' = fromTTMaybe msg

1703 = do let msg' = fromTTMaybe msg

1601 case msg' of

1704 case msg' of

@@ -2362,7 +2465,7 @@ reflectTTQuote unq (P nt n t)

2362reflectTTQuote unq (V n)

2465reflectTTQuote unq (V n)

2363 = reflCall "V" [RConstant (I n)]

2466 = reflCall "V" [RConstant (I n)]

2364reflectTTQuote unq (Bind n b x)

2467reflectTTQuote unq (Bind n b x)

2365− = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote unq b, reflectTTQuote unq x]

2468+ = reflCall "Bind" [reflectName n, reflectBinderQuote reflectTTQuote (reflm "TT") unq b, reflectTTQuote unq x]

2366reflectTTQuote unq (App f x)

2469reflectTTQuote unq (App f x)

2367 = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]

2470 = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]

2368reflectTTQuote unq (Constant c)

2471reflectTTQuote unq (Constant c)

@@ -2379,7 +2482,7 @@ reflectRawQuote unq (Var n)

2379 | n `elem` unq = Var n

2482 | n `elem` unq = Var n

2380 | otherwise = reflCall "Var" [reflectName n]

2483 | otherwise = reflCall "Var" [reflectName n]

2381reflectRawQuote unq (RBind n b r) =

2484reflectRawQuote unq (RBind n b r) =

2382− reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote unq b, reflectRawQuote unq r]

2485+ reflCall "RBind" [reflectName n, reflectBinderQuote reflectRawQuote (reflm "Raw") unq b, reflectRawQuote unq r]

2383reflectRawQuote unq (RApp f x) =

2486reflectRawQuote unq (RApp f x) =

2384 reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]

2487 reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]

2385reflectRawQuote unq RType = Var (reflm "RType")

2488reflectRawQuote unq RType = Var (reflm "RType")

@@ -2437,27 +2540,27 @@ reflectNameQuotePattern _ -- for all other names, match any

2437 solve

2540 solve

2438

2541

2439reflectBinder :: Binder Term -> Raw

2542reflectBinder :: Binder Term -> Raw

2440−reflectBinder = reflectBinderQuote reflectTTQuote []

2543+reflectBinder = reflectBinderQuote reflectTTQuote (reflm "TT") []

2441−

2544+

2442−reflectBinderQuote :: ([Name] -> a -> Raw) -> [Name] -> Binder a -> Raw

2545+reflectBinderQuote :: ([Name] -> a -> Raw) -> Name -> [Name] -> Binder a -> Raw

2443−reflectBinderQuote q unq (Lam t)

2546+reflectBinderQuote q ty unq (Lam t)

2444− = reflCall "Lam" [Var (reflm "TT"), q unq t]

2547+ = reflCall "Lam" [Var ty, q unq t]

2445−reflectBinderQuote q unq (Pi _ t k)

2548+reflectBinderQuote q ty unq (Pi _ t k)

2446− = reflCall "Pi" [Var (reflm "TT"), q unq t, q unq k]

2549+ = reflCall "Pi" [Var ty, q unq t, q unq k]

2447−reflectBinderQuote q unq (Let x y)

2550+reflectBinderQuote q ty unq (Let x y)

2448− = reflCall "Let" [Var (reflm "TT"), q unq x, q unq y]

2551+ = reflCall "Let" [Var ty, q unq x, q unq y]

2449−reflectBinderQuote q unq (NLet x y)

2552+reflectBinderQuote q ty unq (NLet x y)

2450− = reflCall "NLet" [Var (reflm "TT"), q unq x, q unq y]

2553+ = reflCall "NLet" [Var ty, q unq x, q unq y]

2451−reflectBinderQuote q unq (Hole t)

2554+reflectBinderQuote q ty unq (Hole t)

2452− = reflCall "Hole" [Var (reflm "TT"), q unq t]

2555+ = reflCall "Hole" [Var ty, q unq t]

2453−reflectBinderQuote q unq (GHole _ t)

2556+reflectBinderQuote q ty unq (GHole _ t)

2454− = reflCall "GHole" [Var (reflm "TT"), q unq t]

2557+ = reflCall "GHole" [Var ty, q unq t]

2455−reflectBinderQuote q unq (Guess x y)

2558+reflectBinderQuote q ty unq (Guess x y)

2456− = reflCall "Guess" [Var (reflm "TT"), q unq x, q unq y]

2559+ = reflCall "Guess" [Var ty, q unq x, q unq y]

2457−reflectBinderQuote q unq (PVar t)

2560+reflectBinderQuote q ty unq (PVar t)

2458− = reflCall "PVar" [Var (reflm "TT"), q unq t]

2561+ = reflCall "PVar" [Var ty, q unq t]

2459−reflectBinderQuote q unq (PVTy t)

2562+reflectBinderQuote q ty unq (PVTy t)

2460− = reflCall "PVTy" [Var (reflm "TT"), q unq t]

2563+ = reflCall "PVTy" [Var ty, q unq t]

2461

2564

2462mkList :: Raw -> [Raw] -> Raw

2565mkList :: Raw -> [Raw] -> Raw

2463mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty

2566mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty

@@ -2604,11 +2707,14 @@ reflectErr (NotInjective t1 t2 t3) =

2604 , reflect t2

2707 , reflect t2

2605 , reflect t3

2708 , reflect t3

2606 ]

2709 ]

2607−reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

2710+reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

2608reflectErr (CantResolveAlts ss) =

2711reflectErr (CantResolveAlts ss) =

2609 raw_apply (Var $ reflErrName "CantResolveAlts")

2712 raw_apply (Var $ reflErrName "CantResolveAlts")

2610 [rawList (Var $ reflm "TTName") (map reflectName ss)]

2713 [rawList (Var $ reflm "TTName") (map reflectName ss)]

2611reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

2714reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]

2715+reflectErr (NoEliminator str t)

2716+ = raw_apply (Var $ reflErrName "NoEliminator") [RConstant (Str str),

2717+ reflect t]

2612reflectErr UniverseError = Var $ reflErrName "UniverseError"

2718reflectErr UniverseError = Var $ reflErrName "UniverseError"

2613reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

2719reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

2614reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]

2720reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]

@@ -2749,6 +2855,28 @@ reifyReportPart (App (P (DCon _ _ _) n _) tm)

2749 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm

2855 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm

2750reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

2856reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

2751

2857

2858+reifyTyDecl :: Term -> ElabD RTyDecl

2859+reifyTyDecl (App (App (App (P (DCon _ _ _) n _) tyN) args) ret)

2860+ | n == tacN "Declare" =

2861+ do tyN' <- reifyTTName tyN

2862+ args' <- case unList args of

2863+ Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."

2864+ Just xs -> mapM reifyRArg xs

2865+ ret' <- reifyRaw ret

2866+ return $ RDeclare tyN' args' ret'

2867+ where reifyRArg :: Term -> ElabD RArg

2868+ reifyRArg (App (App (P (DCon _ _ _) n _) argN) argTy)

2869+ | n == tacN "Explicit" = liftM2 RExplicit

2870+ (reifyTTName argN)

2871+ (reifyRaw argTy)

2872+ | n == tacN "Implicit" = liftM2 RImplicit

2873+ (reifyTTName argN)

2874+ (reifyRaw argTy) | n == tacN "Constraint" = liftM2 RConstraint

2875+ (reifyTTName argN)

2876+ (reifyRaw argTy)

2877+ reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."

2878+reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."

2879+

2752envTupleType :: Raw

2880envTupleType :: Raw

2753envTupleType

2881envTupleType

2754 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")

2882 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")

src/Idris/IBC.hs+10−6

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

37import Util.Zlib (decompressEither)

39ibcVersion :: Word8

40−ibcVersion = 99

40+ibcVersion = 100

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

src/Idris/Reflection.hsnew file+18

@@ -0,0 +1,18 @@

1+{-|

2+Handy tools for doing reflection.

3+-}

4+module Idris.Reflection where

6+import Idris.Core.TT

7+import Idris.AbsSyntaxTree (PArg'(..), PArg, PTerm(Placeholder))

9+data RArg = RExplicit { argName :: Name, argTy :: Raw }

10+ | RImplicit { argName :: Name, argTy :: Raw }

11+ | RConstraint { argName :: Name, argTy :: Raw }

12+

13+data RTyDecl = RDeclare Name [RArg] Raw

14+

15+rArgToPArg :: RArg -> PArg

16+rArgToPArg (RExplicit n _) = PExp 0 [] n Placeholder

17+rArgToPArg (RImplicit n _) = PImp 0 False [] n Placeholder

18+rArgToPArg (RConstraint n _) = PConstraint 0 [] n Placeholder

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

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

test/tactics001/Tactics.idr+14

@@ -2,6 +2,9 @@ module Tactics

3import Language.Reflection.Tactical

5+import Data.Vect

5%default total

8%default total

7-- Test that basic proofs with new-style tactics work

10-- Test that basic proofs with new-style tactics work

@@ -25,3 +28,14 @@ plusSuccRightSuccNew (S j) k =

25 %runTactics (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k")))

28 %runTactics (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k")))

26 fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))

29 fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))

27 solve)

30 solve)

31+

32+-- Test that side effects in new tactics work

33+

34+mkDecl : ()

35+mkDecl = %runTactics (do declareType $ Declare (NS (UN "repUnit") ["Tactics"])

36+ [Implicit (UN "z") `(Nat)]

37+ `(Vect ~(Var (UN "z")) ())

38+ fill `(() : ())

39+ solve)

40+

41+repUnit = pure ()