aa33865 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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

commitaa338657ccf8e8ab7bb35c2b434f6a521b690f02 authorAndreas Reuleaux <arx@a-rx.info> dateWed 18 Mar 2015, 09:55 (12 years ago) parent1bf2731 2a2468f

39 files changed+547−223

compare with master

unifiedsplit

CHANGELOG+3−1 Setup.hs+9−2 idris.cabal+6 libs/base/Control/Monad/State.idr+1−1 libs/base/Control/Monad/Writer.idr+2−1 libs/base/Data/Heap.idr+1−1 libs/base/Decidable/Order.idr+4−4 libs/base/Language/Reflection/Utils.idr+1 libs/prelude/Language/Reflection.idr+6−6 libs/prelude/Language/Reflection/Errors.idr+1 libs/prelude/Language/Reflection/Tactical.idr+14 libs/prelude/Prelude/Algebra.idr+1−1 src/Idris/AbsSyntax.hs+19−5 src/Idris/AbsSyntaxTree.hs+16−8 src/Idris/Core/Binary.hs+9−3 src/Idris/Core/DeepSeq.hs+2−1 src/Idris/Core/Elaborate.hs+30−14 src/Idris/Core/ProofState.hs+9−6 src/Idris/Core/ProofTerm.hs+3 src/Idris/Core/TT.hs+11−4 src/Idris/Core/Unify.hs+2−2 src/Idris/DeepSeq.hs+4−4 src/Idris/Delaborate.hs+7−1 src/Idris/Elab/Class.hs+28−10 src/Idris/Elab/Clause.hs+34−22 src/Idris/Elab/Instance.hs+23−11 src/Idris/Elab/Transform.hs+10−4 src/Idris/Elab/Type.hs+10−6 src/Idris/Elab/Utils.hs+10−8 src/Idris/Elab/Value.hs+8−3 src/Idris/ElabDecls.hs+2−2 src/Idris/ElabTerm.hs+209−81 src/Idris/IBC.hs+10−6 src/Idris/ParseHelpers.hs+2−2 src/Idris/Parser.hs+5−1 src/Idris/REPL.hs+1−1 src/Idris/Reflection.hs+18 test/basic012/basic012.idr+2−1 test/tactics001/Tactics.idr+14

CHANGELOG+3−1

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

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

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

2525* DSL notation can now be applied with $

26−<<<<<<< HEAD

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

2827 called from foreign code

2928* Instances can now have documentation strings.

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

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

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

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

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

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

42+ are checked when checking for overlapping instances.

4143

4244New in 0.9.16:

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

Setup.hs+9−2

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

5757 Just False -> False

5858 Nothing -> True

5959

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+

6067isRelease :: S.ConfigFlags -> Bool

6168isRelease flags =

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

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

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

177184 return (Just buildinfo, [])

178185

179−idrisBuild _ flags _ local = do

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

180187 buildStdLib

181188 buildRTS

182189 where

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

199206-- -----------------------------------------------------------------------------

200207-- Copy/Install

201208

202−idrisInstall verbosity copy pkg local = do

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

203210 installStdLib

204211 installRTS

205212 where

idris.cabal+6

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

658658 Default: False

659659 manual: True

660660

661+Flag execonly

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

663+ Default: False

664+ manual: True

665+

661666Library

662667 hs-source-dirs: src

663668 Exposed-modules:

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

725730 , Idris.ProofSearch

726731 , Idris.Prover

727732 , Idris.Providers

733+ , Idris.Reflection

728734 , Idris.REPL

729735 , Idris.REPLParser

730736 , Idris.Transforms

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

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

66%access public

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

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

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

1010 ||| Get the context

1111 get : m s

1212 ||| Write a new context/output

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

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

5151

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

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

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

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

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

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

5657 return (a, f' w)

5758

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

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

146146isEmptySizeZero Empty p = Refl

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

148148

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

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

150150emptyHeapValid = Refl

151151

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

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

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

3636 eq (f a) (f b)

3737

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

39−minimum x y with (order x y)

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

4040 | Left _ = x

4141 | Right _ = y

4242

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

44−maximum x y with (order x y)

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

4545 | Left _ = y

4646 | Right _ = x

4747

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

103103decideLTE Z y = Yes LTEZero

104104decideLTE (S x) Z = No zeroNeverGreater

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

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

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

107107 | No _ with (decideLTE x y)

108108 | Yes nLTEm = Yes (LTESucc nLTEm)

109109 | No nGTm = No (ltesuccinjective nGTm)

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

122122instance Ordered Nat LTE where

123123 order Z n = Left LTEZero

124124 order m Z = Right LTEZero

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

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

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

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

128128

libs/base/Language/Reflection/Utils.idr+1

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

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

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

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

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

275276 show UniverseError = "UniverseError"

276277 show ProgramLineComment = "ProgramLineComment"

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

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

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

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

417417

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

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

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

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

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

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

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

422422

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

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

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

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

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

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

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

427427

428428instance Quotable TTName TT where

429429 quotedTy = `(TTName)

libs/prelude/Language/Reflection/Errors.idr+1

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

3131 | CantResolve TT

3232 | CantResolveAlts (List TTName)

3333 | IncompleteTerm TT

34+ | NoEliminator String TT

3435 | UniverseError

3536 | ProgramLineComment

3637 | Inaccessible TTName

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

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

88import Prelude.Monad

99import Language.Reflection

1010

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+

1119abstract

1220data Tactical : Type -> Type where

1321 -- obligatory control stuff

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

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

4048 prim__Intro : Maybe TTName -> Tactical ()

4149

50+ prim__DeclareType : TyDecl -> Tactical ()

51+

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

4353

54+

4455-------------

4556-- Public API

4657-------------

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

117128rewriteWith : Raw -> Tactical ()

118129rewriteWith rule = prim__Rewrite rule

119130

131+declareType : TyDecl -> Tactical ()

132+declareType decl = prim__DeclareType decl

133+

120134debug : Tactical a

121135debug = prim__Debug Nothing

122136

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

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

316316

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

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

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

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

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

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

322322

src/Idris/AbsSyntax.hs+19−5

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

360360addInstance int n i

361361 = do ist <- getIState

362362 case lookupCtxt n (idris_classes ist) of

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

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

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

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

365365 putIState $ ist { idris_classes = cs }

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

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

367367 putIState $ ist { idris_classes = cs }

368368 where addI i ins | int = i : ins

369369 | chaser n = ins ++ [i]

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

455455putIState :: IState -> Idris ()

456456putIState = put

457457

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

459+updateIState f = do i <- getIState

460+ putIState $ f i

461+

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

459463withContext ctx name dflt action = do

460464 ist <- getIState

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

547551addDeferred = addDeferred' Ref

548552addDeferredTyCon = addDeferred' (TCon 0 0)

549553

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

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

555+addDeferred' :: NameType

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

551564addDeferred' nt ns

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

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

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

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

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

10791092 = PClass doc info f

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

10811094 n

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

10831096 pDocs

1097+ fds

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

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

10861100 = PInstance doc argDocs info f

src/Idris/AbsSyntaxTree.hs+16−8

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

186186 idris_name :: Int,

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

188188 -- ^ Full application LHS on source line

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

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

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

190194 idris_coercions :: [Name],

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

192196 syntax_rules :: SyntaxRules,

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

602606 Name

603607 [(Name, t)] -- parameters

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

609+ [Name] -- determining parameters

605610 [PDecl' t] -- declarations

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

607612 -- class name, parameters, method declarations

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

634639-- For elaborator state

635640data EState = EState {

636641 case_decls :: [PDecl],

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

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

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

638644 }

639645

640−initEState = EState [] []

646+initEState :: EState

647+initEState = EState [] [] []

641648

642649type ElabD a = Elab' EState a

643650

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

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

697704declared (PNamespace _ ds) = concatMap declared ds

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

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

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

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

701708declared (PDSL n _) = [n]

702709declared (PSyntax _ _) = []

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

715722tldeclared (PParams _ _ ds) = []

716723tldeclared (PMutual _ ds) = concatMap tldeclared ds

717724tldeclared (PNamespace _ ds) = concatMap tldeclared ds

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

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

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

720727tldeclared _ = []

721728

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

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

732739defined (PNamespace _ ds) = concatMap defined ds

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

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

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

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

736743defined (PDSL n _) = [n]

737744defined (PSyntax _ _) = []

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

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

10331040 class_default_superclasses :: [PDecl],

10341041 class_params :: [Name],

1035− class_instances :: [Name] }

1042+ class_instances :: [Name],

1043+ class_determiners :: [Int] }

10361044 deriving Show

10371045{-!

10381046deriving instance Binary ClassInfo

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

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

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

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

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

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

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

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

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

9191 put x

9292 put y

9393 put z

94− put (CantResolve t) = do putWord8 15

95− put t

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

95+ put t

9696 put (CantResolveAlts ns) = do putWord8 16

9797 put ns

9898 put (IncompleteTerm t) = do putWord8 17

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

146146 put x1

147147 put x2

148148 put x3

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

150+ put s

151+ put t

149152

150153 get = do i <- getWord8

151154 case i of

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

172175 13 -> fmap NoTypeDecl get

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

174177 return $ NotInjective x y z

175− 15 -> fmap CantResolve get

178+ 15 -> fmap (CantResolve False) get

176179 16 -> fmap CantResolveAlts get

177180 17 -> fmap IncompleteTerm get

178181 18 -> return UniverseError

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

205208 x2 <- get

206209 x3 <- get

207210 return (ElabDebug x1 x2 x3)

211+ 37 -> do x1 <- get

212+ x2 <- get

213+ return (NoEliminator x1 x2)

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

209215----- Generated by 'derive'

210216

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

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

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

8181 rnf (NotInjective x1 x2 x3)

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

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

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

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

8687 rnf UniverseError = ()

8788 rnf ProgramLineComment = ()

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

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

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

756756

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

758758try' t1 t2 proofSearch

759− = do s <- get

760− ps <- get_probs

761− ulog <- getUnifyLog

762− case prunStateT 999999 False ps t1 s of

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

764− return $! v

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

766− if recoverableErr e1 then

767− do case runStateT t2 s of

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

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

770− then lift (tfail e1)

771− else lift (tfail e2)

772− else lift (tfail e1)

759+ = do s <- get

760+ ps <- get_probs

761+ ulog <- getUnifyLog

762+ case prunStateT 999999 False ps t1 s of

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

764+ return $! v

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

766+ if recoverableErr e1 then

767+ do case runStateT t2 s of

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

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

770+ then lift (tfail e1)

771+ else lift (tfail e2)

772+ else lift (tfail e1)

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

774774 = -- traceWhen r (show err) $

775775 r || proofSearch

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

782782 recoverableErr (ElabDebug _ _ _) = False

783783 recoverableErr _ = True

784784

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+

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

786802tryWhen True a b = try a b

787803tryWhen 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

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

682682 let tmt' = normalise ctxt env tmt

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

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

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

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

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

686686 case unApply tmt' of

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

688688 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

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

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

719719 return scv'

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

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

721721 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'

723724 where scname = sMN 0 "scarg"

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

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

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

878879 ctxt = context ps

879880 ulog = unifylog ps

880881 usupp = map fst (notunified ps)

882+ dont = dontunify ps

881883

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

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

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

889891 if newx || newy || ready ||

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

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

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

893− up (ns ++ v) ps

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

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

896+ up (ns ++ v') ps

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

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

896899 (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

172172 else (t, False)

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

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

175178 updateSolved' xs t = (t, False)

176179

177180 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

155155 | WithFnType t

156156 | NoTypeDecl Name

157157 | NotInjective t t t

158− | CantResolve t

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

159+ t

159160 | CantResolveAlts [Name]

160161 | IncompleteTerm t

162+ | NoEliminator String t

161163 | UniverseError

162164 | UniqueError Universe Name

163165 | UniqueKindError Universe Name

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

231233 size (NoSuchVariable name) = size name

232234 size (NoTypeDecl name) = size name

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

234− size (CantResolve trm) = size trm

236+ size (CantResolve _ trm) = size trm

235237 size (NoRewriting trm) = size trm

236238 size (CantResolveAlts _) = 1

237239 size (IncompleteTerm trm) = size trm

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

246248

247249score :: Err -> Int

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

249−score (CantResolve _) = 20

251+score (CantResolve _ _) = 20

250252score (NoSuchVariable _) = 1000

251253score (ProofSearchFail e) = score e

252254score (CantSolveGoal _ _) = 100000

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

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

508510 concatMap (Map.toList) allns

509511

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

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

511513addAlist [] ctxt = ctxt

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

513515

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

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

935937instantiate :: TT n -> TT n -> TT n

936938instantiate e = subst 0 where

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

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

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

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

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

945948-- that has been substituted.

946949substV :: TT n -> TT n -> TT n

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

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

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

949953 | otherwise = V x

950954 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

10381042 -- substitution happens...)

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

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

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

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

10431050 (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 =

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

101101 holeIn env f || f `elem` holes

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

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

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

106106 holeIn env f || f `elem` holes

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

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

111111 holeIn env f || f `elem` holes

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

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

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

116116 holeIn env f || f `elem` holes

src/Idris/DeepSeq.hs+4−4

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

149149 rnf x2 `seq`

150150 rnf x3 `seq`

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

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

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

153153 = rnf x1 `seq`

154154 rnf x2 `seq`

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

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

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

157157 = rnf x1 `seq`

158158 rnf x2 `seq`

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

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

314314

315315instance NFData ClassInfo where

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

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

317317 = rnf x1 `seq`

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

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

319319

320320instance NFData OptInfo where

321321 rnf (Optimise x1 x2)

src/Idris/Delaborate.hs+7−1

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

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

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

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

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

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

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

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

299299pprintErr' i (CantMatch t) =

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

301301pprintErr' 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."

302308pprintErr' i UniverseError = text "Universe inconsistency"

303309pprintErr' i (UniqueError NullType n)

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

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

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

5050

5151import Util.Pretty(pretty, text)

5252

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

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

5454

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

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

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

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

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

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

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

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

6061 let tty = pibind ps PType

6162 let constraint = PApp fc (PRef fc tn)

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

7576 let (methods, imethods)

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

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

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

7979 -- build instance constructor type

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

8181 -- to elsewhere in the class declaration

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

8686 let ddecl = PDatadecl tn tty cons

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

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

89+

90+ dets <- findDets cn fds

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

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

9093 logLvl 5 $ "Building functions"

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

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

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

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

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

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

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

98102 -- add the default definitions

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

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

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

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

203207

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

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

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

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

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

207211 getMArgs _ = []

208212

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

210214 | otherwise = getMeth ms as x

211215

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

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

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

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

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

215219 lhsArgs [] _ = []

216220

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

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

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

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

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

220224 rhsArgs [] _ = []

221225

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

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

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

232236 toExp ns e sc = sc

237+

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

239+findDets n ns =

240+ do i <- getIState

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

242+ Just ty -> getDetPos 0 ns ty

243+ Nothing -> []

244+ where

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

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

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

248+ getDetPos _ _ _ = []

249+

250+

src/Idris/Elab/Clause.hs+34−22

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

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

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

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

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

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

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

459+ do setContext ctxt'

460+ processTacticDecls newDecls

461+ let lhs_tm = orderPats (getInferTerm lhs')

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

461463 OK _ -> return True

462464 err -> return False

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

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

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

581583

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

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

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

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

586− probs <- get_probs

587− inj <- get_inj

588− return (res, probs, inj))

589−

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

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

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

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

588+ probs <- get_probs

589+ inj <- get_inj

590+ return (res, probs, inj))

591+ setContext ctxt'

592+ processTacticDecls newDecls

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

591594

592595 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

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

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

655658 logLvl 5 "STARTING CHECK"

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

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

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

658661 (do pbinds ist lhs_tm

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

660663 setNextName

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

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

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

665+ errAt "right hand side of " fname

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

663667 errAt "right hand side of " fname

664668 (erun fc $ psolve lhs_tm)

665669 hs <- get_holes

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

668672 tt <- get_term

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

670674 probs <- get_probs

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

672−

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

676+ setContext ctxt'

677+ processTacticDecls newDecls

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

674679

675680 logLvl 5 "DONE CHECK"

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

812817 let params = getParamsInType i [] fn_is fn_ty

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

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

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

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

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

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

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

824+ setContext ctxt'

825+ processTacticDecls newDecls

819826 let lhs_tm = orderPats (getInferTerm lhs')

820827 let lhs_ty = getInferType lhs'

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

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

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

829836 -- Elaborate wval in this context

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

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

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

832839 (bindTyArgs PVTy bargs infP) initEState

833840 (do pbinds i lhs_tm

834841 setNextName

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

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

838845 erun fc $ psolve lhs_tm

839846 tt <- get_term

840− return (tt, d, is))

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

848+ setContext ctxt'

849+ processTacticDecls newDecls

841850 def' <- checkDef fc defer

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

843852 addDeferred def''

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

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

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

925934 i <- getIState

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

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

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

928937 (do pbinds i lhs_tm

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

931940 psolve lhs_tm

932941 tt <- get_term

933− return (tt, d, is))

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

943+ setContext ctxt'

944+ processTacticDecls newDecls

945+

934946 def' <- checkDef fc defer

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

936948 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

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

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

7777 case expn of

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

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

7979 (class_instances ci)

8080 addInstance intInst n iname

8181 Just _ -> addInstance intInst n iname

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

169169 ty' <- implicit info syn iname ty'

170170 let ty = addImpl i ty'

171171 ctxt <- getContext

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

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

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

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

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

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

175+ setContext ctxt'

176+ processTacticDecls newDecls

175177 ctxt <- getContext

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

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

179181

180− findOverlapping i t n

182+ findOverlapping i dets t n

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

182184 | otherwise

183185 = case lookupTy n (tt_ctxt i) of

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

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

186− case matchClause i tret' tret of

187− Right ms -> Just tret'

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

189− Right ms -> Just tret'

190− Left _ -> Nothing

188+ case matchArgs i dets tret' tret of

189+ Right _ -> Just tret'

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

191+ Right _ -> Just tret'

192+ Left _ -> Nothing

191193 _ -> Nothing

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

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

194196 getRetType (PPi _ _ _ sc) = getRetType sc

195197 getRetType t = t

196198

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+

197209 mkMethApp (n, _, _, ty)

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

199211 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

5353 = do ctxt <- getContext

5454 i <- getIState

5555 let lhs = addImplPat i lhs_in

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

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

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

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

5959 (infTerm lhs)))

60+ setContext ctxt'

61+ processTacticDecls newDecls

6062 let lhs_tm = orderPats (getInferTerm lhs')

6163 let lhs_ty = getInferType lhs'

6264 let newargs = pvars i lhs_tm

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

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

6769

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

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

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

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

7173 (do pbinds i lhs_tm

7274 setNextName

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

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

7476 erun fc $ psolve lhs_tm

7577 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+

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

7884 let crhs_tm = renamepats pnames crhs_tm_in

7985 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

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

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

6767

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

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

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

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

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

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

71+ setContext ctxt'

72+ processTacticDecls newDecls

7173

7274 let tyT = patToImp tyT'

7375

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

114116 param_pos i ns t = []

115117

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

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

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

119+elabType :: ElabInfo -> SyntaxInfo

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

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

119122elabType = elabType' False

120123

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

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

125+ ElabInfo -> SyntaxInfo ->

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

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

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

125129 n = liftname info n_in in -}

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

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

2222

2323import qualified Data.Map as Map

2424

25−recheckC = recheckC_borrowing False []

25+recheckC = recheckC_borrowing False []

2626

2727recheckC_borrowing uniq_check bs fc env t

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

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

3434 addConstraints fc cs

3535 return (tm, ty)

3636

37−

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

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

3839checkDef fc ns = checkAddDef False True fc ns

3940

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

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

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

4044checkAddDef add toplvl fc [] = return []

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

4246 = do ctxt <- getContext

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

4650 ns' <- checkAddDef add toplvl fc ns

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

4852

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

5054-- type

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

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

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

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

5559inaccessibleImps _ _ _ = []

5660

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.

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

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

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

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

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

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

7680

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

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

7983-- they are the same!)

80−

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

8285checkInferred fc inf user =

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

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

9295 logLvl 10 $ "Checked match"

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

9497

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

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

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

97−

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

99101inferredDiff fc inf user =

100102 do i <- getIState

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

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

6363 -- * elaboration as a Type

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

6565

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

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

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

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

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

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+

6974 let vtm = orderPats (getInferTerm tm')

7075

7176 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

229229 ninfo = case namespace info of

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

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

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

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

233233 | what /= EDefns

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

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

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

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

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

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

src/Idris/ElabTerm.hs+209−81

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

1818import Idris.ErrReverse (errReverse)

1919import Idris.ElabQuasiquote (extractUnquotes)

2020import Idris.Elab.Utils

21+import Idris.Reflection

2122import qualified Util.Pretty as U

2223

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

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

3637data ElabMode = ETyDecl | ELHS | ERHS

3738 deriving Eq

3839

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+

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

4067-- elaborated, typechecked term.

4168--

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

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

4673

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

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

75+ ElabD ElabResult

4976build ist info emode opts fn tm

5077 = do elab ist info emode opts fn tm

5178 let tmIn = tm

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

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

6592 do focus n

6693 g <- goal

67− try (resolveTC True 7 g fn ist)

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

6895 (movelast n)) ivs

6996 ivs <- get_instances

7097 hs <- get_holes

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

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

73100 do focus n

74101 g <- goal

75− resolveTC True 7 g fn ist) ivs

102+ ptm <- get_term

103+ resolveTC True True 7 g fn ist) ivs

76104 tm <- get_term

77105 ctxt <- get_context

78106 probs <- get_probs

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

94122 when tydecl (do update_term orderPats

95123 mkPat)

96124-- update_term liftPats)

97− EState is _ <- getAux

125+ EState is _ impls <- getAux

98126 tt <- get_term

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

100128 log <- getLog

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

102− else return (tm, ds, is)

129+ ctxt <- get_context

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

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

103132 where pattern = emode == ELHS

104133 tydecl = emode == ETyDecl

105134

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

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

115144

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

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

146+ ElabD ElabResult

118147buildTC ist info emode opts fn tm

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

120149 let ns = allNamesIn tm

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

135164 -- unification

136165 when (not (null dots)) $

137166 lift (Error (CantMatch (getInferTerm tm)))

138− EState is _ <- getAux

167+ EState is _ impls <- getAux

139168 tt <- get_term

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

141170 log <- getLog

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

143− else return (tm, ds, is)

171+ ctxt <- get_context

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

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

144174 where pattern = emode == ELHS

145175

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

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

183213 _ -> return True

184214 _ -> return False

185215

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

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

188−

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

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

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

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

190220 ElabD ()

191221elab ist info emode opts fn tm

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

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

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

323353 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

325355 elab' ina fc (PResolveTC fc')

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

327357 instanceArg c

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

540570 g <- goal

541571 hs <- get_holes

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

544574 (movelast n)

545575 else movelast n)

546576 (ivs' \\ ivs)

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

700730 env <- get_env

701731 hs <- get_holes

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

704734 (movelast n)

705735 else movelast n)

706736 (ivs' \\ ivs)

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

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

966996 elab' ina fc t

967997 unifyLog False

968− elab' ina fc (PQuasiquote t goal)

998+ elab' ina fc (PQuasiquote t goalt)

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

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

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

1002+ finalTy <- goal

9721003 (t, unq) <- extractUnquotes 0 t

9731004 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

978−

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

9791006

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

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

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

10101037 letbind nTm (Var qTy) (Var qTm)

10111038

10121039 -- Fill out the goal type, if relevant

1013− case goal of

1040+ case goalt of

10141041 Nothing -> return ()

10151042 Just gTy -> do focus qTy

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

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

10251052 env <- get_env

10261053 loadState

10271054 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

10291058 case quoted of

10301059 Just q -> do ctxt <- get_context

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

10321061 if pattern

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

1034− (reflectRawQuotePattern unquoteNames (forget q'))

1035− True

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

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

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

1039− True -- ignore errors like proof search does

1062+ then if isRaw

1063+ then reflectRawQuotePattern unquoteNames (forget q')

1064+ else reflectTTQuotePattern unquoteNames q'

1065+ else do if isRaw

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

1067+ fill $ reflectRawQuote unquoteNames (forget q')

1068+ else fill $ reflectTTQuote unquoteNames q'

10401069 solve

10411070

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

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

10771106 focus n

10781107 elab' ina (Just fc') tm

10791108 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

10821111 solve

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

10841113

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

13461375findInstances ist t

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

13481377 = case lookupCtxt n (idris_classes ist) of

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

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

13501379 _ -> []

13511380 | otherwise = []

13521381

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

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

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

13781407-- name).

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

1380−resolveTC = resTC' []

1381−

1382−resTC' tcs def 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

1384−resTC' tcs defaultOn depth topg fn ist

1385− = do compute

1386− g <- goal

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

1413+ -> IState -> ElabD ()

1414+resolveTC def mvok depth top fn ist

1415+ = do hs <- get_holes

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

1417+

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

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

1420+resTC' tcs defaultOn topholes depth topg fn ist

1421+ = do compute

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

13871428 ptm <- get_term

13881429 ulog <- getUnifyLog

13891430 hs <- get_holes

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

14001441 let depth' = if scopeOnly then 2 else depth

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

14021443 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+

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

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

14051471

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

14271493

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

14291495 -- ps <- get_probs

1430− lift $ tfail $ CantResolve topg

1496+ lift $ tfail $ CantResolve False topg

14311497 blunderbuss t d stk (n:ns)

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

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

1499+ = tryCatch (resolve n d)

1500+ (\e -> case e of

1501+ CantResolve True _ -> lift $ tfail e

1502+ _ -> blunderbuss t d stk ns)

14341503 | otherwise = blunderbuss t d stk ns

14351504

14361505 resolve n depth

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

14591528 let got = fst (unApply t)

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

14611530 then depth - 1 else depth

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

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

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

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

14651534 hs <- get_holes

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

15051574 else casetac (forget val)

15061575 when autoSolve solveAll

15071576

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

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

1577+tacN :: String -> Name

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

1579+

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

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

1582+ runTacTm tm'

1583+ return ()

15101584 where

1511− eval = normaliseAll ctxt env . finalise

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

1585+ eval tm = do ctxt <- get_context

1586+ return $ normaliseAll ctxt env (finalise tm)

1587+

15131588 returnUnit = fmap fst $ get_type_val (Var unitCon)

15141589

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

15471622 = do env <- get_env

15481623 fmap fst . get_type_val $ reflectEnv env

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

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

1625+ = do errs' <- eval errs

1626+ parts <- reifyReportParts errs'

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

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

15531629 = return tm

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

1555− = do let first' = eval first

1631+ = do first' <- eval first

15561632 res <- runTacTm first'

1557− let next = eval (App andThen res)

1633+ next <- eval (App andThen res)

15581634 runTacTm next

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

1560− = do let first' = eval first

1561− let alt' = eval alt

1636+ = do first' <- eval first

1637+ alt' <- eval alt

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

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

15641640 = do raw' <- reifyRaw raw

15651641 apply raw' []

15661642 returnUnit

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

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

1569− fmap fst $ get_type_val (reflectName n)

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

1644+ = do hintStr <- eval hint

1645+ case hintStr of

1646+ Constant (Str h) -> do

1647+ n <- getNameFrom (sMN 0 h)

1648+ fmap fst $ get_type_val (reflectName n)

1649+ _ -> fail "no hint"

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

15711651 = do n' <- reifyTTName n

15721652 ty' <- reifyRaw ty

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

15961676 Just name -> fmap Just $ reifyTTName name

15971677 intro n

15981678 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

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

16001703 = do let msg' = fromTTMaybe msg

16011704 case msg' of

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

23622465reflectTTQuote unq (V n)

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

23642467reflectTTQuote 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]

23662469reflectTTQuote unq (App f x)

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

23682471reflectTTQuote unq (Constant c)

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

23792482 | n `elem` unq = Var n

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

23812484reflectRawQuote 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]

23832486reflectRawQuote unq (RApp f x) =

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

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

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

24372540 solve

24382541

24392542reflectBinder :: Binder Term -> Raw

2440−reflectBinder = reflectBinderQuote reflectTTQuote []

2441−

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

2443−reflectBinderQuote q unq (Lam t)

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

2445−reflectBinderQuote q unq (Pi _ t k)

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

2447−reflectBinderQuote q unq (Let x y)

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

2449−reflectBinderQuote q unq (NLet x y)

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

2451−reflectBinderQuote q unq (Hole t)

2452− = reflCall "Hole" [Var (reflm "TT"), q unq t]

2453−reflectBinderQuote q unq (GHole _ t)

2454− = reflCall "GHole" [Var (reflm "TT"), q unq t]

2455−reflectBinderQuote q unq (Guess x y)

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

2457−reflectBinderQuote q unq (PVar t)

2458− = reflCall "PVar" [Var (reflm "TT"), q unq t]

2459−reflectBinderQuote q unq (PVTy t)

2460− = reflCall "PVTy" [Var (reflm "TT"), q unq t]

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

2544+

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

2546+reflectBinderQuote q ty unq (Lam t)

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

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

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

2550+reflectBinderQuote q ty unq (Let x y)

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

2552+reflectBinderQuote q ty unq (NLet x y)

2553+ = reflCall "NLet" [Var ty, q unq x, q unq y]

2554+reflectBinderQuote q ty unq (Hole t)

2555+ = reflCall "Hole" [Var ty, q unq t]

2556+reflectBinderQuote q ty unq (GHole _ t)

2557+ = reflCall "GHole" [Var ty, q unq t]

2558+reflectBinderQuote q ty unq (Guess x y)

2559+ = reflCall "Guess" [Var ty, q unq x, q unq y]

2560+reflectBinderQuote q ty unq (PVar t)

2561+ = reflCall "PVar" [Var ty, q unq t]

2562+reflectBinderQuote q ty unq (PVTy t)

2563+ = reflCall "PVTy" [Var ty, q unq t]

24612564

24622565mkList :: Raw -> [Raw] -> Raw

24632566mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty

@@ -2604,11 +2707,14 @@ reflectErr (NotInjective t1 t2 t3) =

26042707 , reflect t2

26052708 , reflect t3

26062709 ]

2607−reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

2710+reflectErr (CantResolve _ t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]

26082711reflectErr (CantResolveAlts ss) =

26092712 raw_apply (Var $ reflErrName "CantResolveAlts")

26102713 [rawList (Var $ reflm "TTName") (map reflectName ss)]

26112714reflectErr (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]

26122718reflectErr UniverseError = Var $ reflErrName "UniverseError"

26132719reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"

26142720reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]

@@ -2749,6 +2855,28 @@ reifyReportPart (App (P (DCon _ _ _) n _) tm)

27492855 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm

27502856reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

27512857

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+

27522880envTupleType :: Raw

27532881envTupleType

27542882 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")

src/Idris/IBC.hs+10−6

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

3737import Util.Zlib (decompressEither)

3838

3939ibcVersion :: Word8

40−ibcVersion = 99

40+ibcVersion = 100

4141

4242data IBCFile = IBCFile { ver :: Word8,

4343 sourcefile :: FilePath,

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

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

366366 -- could have loaded in any order

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

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

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

369369 _ -> []

370370 let c' = c { class_instances =

371371 class_instances c ++ is }

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

12381238 put x7

12391239 put x8

12401240 put x9

1241− PClass x1 x2 x3 x4 x5 x6 x7 x8

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

12421242 -> do putWord8 7

12431243 put x1

12441244 put x2

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

12481248 put x6

12491249 put x7

12501250 put x8

1251+ put x9

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

12521253 do putWord8 8

12531254 put x1

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

13461347 x6 <- get

13471348 x7 <- get

13481349 x8 <- get

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

1350+ x9 <- get

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

13501352 8 -> do x1 <- get

13511353 x2 <- get

13521354 x3 <- get

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

20712073

20722074

20732075instance Binary ClassInfo where

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

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

20752077 = do put x1

20762078 put x2

20772079 put x3

20782080 put x4

20792081 put x5

2082+ put x6

20802083 get

20812084 = do x1 <- get

20822085 x2 <- get

20832086 x3 <- get

20842087 x4 <- get

20852088 x5 <- get

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

2089+ x6 <- get

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

20872091

20882092instance Binary OptInfo where

20892093 put (Optimise x1 x2)

src/Idris/ParseHelpers.hs+2−2

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

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

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

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

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

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

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

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

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

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

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

src/Idris/Parser.hs+5−1

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

612612 n_in <- fnName

613613 let n = expandNS syn n_in

614614 cs <- many carg

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

615616 ds <- option [] (classBlock syn)

616617 accData acc n (concatMap declared ds)

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

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

618619 <?> "type-class declaration"

619620 where

621+ fundeps :: IdrisParser [Name]

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

623+

620624 carg :: IdrisParser (Name, PTerm)

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

622626 return (i, ty)

src/Idris/REPL.hs+1−1

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

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

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

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

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

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

777777 getName _ = Nothing

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

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

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)

3131AnyST : Type -> Type -> Type

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

3333

34−foost : AnyST Int ()

34+-- foost : AnyST Int ()

35+foost : StateT Int Maybe ()

3536foost = do x <- get

3637 put x

3738

test/tactics001/Tactics.idr+14

@@ -2,6 +2,9 @@ module Tactics

33import Language.Reflection.Tactical

5+import Data.Vect

58%default total

710-- Test that basic proofs with new-style tactics work

@@ -25,3 +28,14 @@ plusSuccRightSuccNew (S j) k =

2528 %runTactics (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k")))

2629 fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))

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