2a2468f · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #2009 from david-christiansen/wip/tactical

2a2468fDavid Christiansen12 years ago

idris.cabal+1

compare with master

unifiedsplit

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

730 , Idris.ProofSearch

731 , Idris.Prover

732 , Idris.Providers

733+ , Idris.Reflection

733 , Idris.REPL

734 , Idris.REPL

734 , Idris.REPLParser

735 , Idris.REPLParser

735 , Idris.Transforms

736 , Idris.Transforms

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

src/Idris/AbsSyntax.hs+14−1

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

src/Idris/AbsSyntaxTree.hs+9−3

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

184 idris_name :: Int,

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

186 -- ^ Full application LHS on source line

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

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

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

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

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

191+ -- allowed

188 idris_coercions :: [Name],

192 idris_coercions :: [Name],

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

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

190 syntax_rules :: SyntaxRules,

194 syntax_rules :: SyntaxRules,

@@ -632,10 +636,12 @@ deriving instance NFData PDecl'

632-- For elaborator state

636-- For elaborator state

633data EState = EState {

637data EState = EState {

634 case_decls :: [PDecl],

638 case_decls :: [PDecl],

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

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

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

636 }

641 }

637

642

638−initEState = EState [] []

643+initEState :: EState

644+initEState = EState [] [] []

639

645

640type ElabD a = Elab' EState a

646type ElabD a = Elab' EState a

641

647

src/Idris/Core/TT.hs+1−1

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

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

510 concatMap (Map.toList) allns

511

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

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

513addAlist [] ctxt = ctxt

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

515

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

@@ -169,9 +169,11 @@ 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

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/ElabTerm.hs+145−58

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

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

95 when tydecl (do update_term orderPats

122 when tydecl (do update_term orderPats

96 mkPat)

123 mkPat)

97-- update_term liftPats)

124-- update_term liftPats)

98− EState is _ <- getAux

125+ EState is _ impls <- getAux

99 tt <- get_term

126 tt <- get_term

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

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

101 log <- getLog

128 log <- getLog

129+ ctxt <- get_context

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

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

103− else return (tm, ds, is)

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

104 where pattern = emode == ELHS

132 where pattern = emode == ELHS

105 tydecl = emode == ETyDecl

133 tydecl = emode == ETyDecl

106

134

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

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

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

116

144

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

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

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

146+ ElabD ElabResult

119buildTC ist info emode opts fn tm

147buildTC ist info emode opts fn tm

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

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

121 let ns = allNamesIn tm

149 let ns = allNamesIn tm

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

136 -- unification

164 -- unification

137 when (not (null dots)) $

165 when (not (null dots)) $

138 lift (Error (CantMatch (getInferTerm tm)))

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

139− EState is _ <- getAux

167+ EState is _ impls <- getAux

140 tt <- get_term

168 tt <- get_term

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

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

142 log <- getLog

170 log <- getLog

171+ ctxt <- get_context

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

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

144− else return (tm, ds, is)

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

145 where pattern = emode == ELHS

174 where pattern = emode == ELHS

146

175

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

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

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

184 _ -> return True

213 _ -> return True

185 _ -> return False

214 _ -> return False

186

215

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

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

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

189−

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

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

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

191 ElabD ()

220 ElabD ()

192elab ist info emode opts fn tm

221elab ist info emode opts fn tm

@@ -970,10 +999,10 @@ elab ist info emode opts fn tm

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

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

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

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

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

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

973− qty <- goal

1002+ finalTy <- goal

974 (t, unq) <- extractUnquotes 0 t

1003 (t, unq) <- extractUnquotes 0 t

975 let unquoteNames = map fst unq

1004 let unquoteNames = map fst unq

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

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

977

1006

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

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

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

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

1023 env <- get_env

1052 env <- get_env

1024 loadState

1053 loadState

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

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

1026−

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

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

1057+ _ -> False

1027 case quoted of

1058 case quoted of

1028 Just q -> do ctxt <- get_context

1059 Just q -> do ctxt <- get_context

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

1030 if pattern

1061 if pattern

1062+ then if isRaw

1063+ then reflectRawQuotePattern unquoteNames (forget q')

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

1064+ else reflectTTQuotePattern unquoteNames q'

1032− (reflectRawQuotePattern unquoteNames (forget q'))

1065+ else do if isRaw

1033− True

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

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

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

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

1067+ fill $ reflectRawQuote unquoteNames (forget q')

1037− True -- ignore errors like proof search does

1068+ else fill $ reflectTTQuote unquoteNames q'

1038 solve

1069 solve

1039

1070

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

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

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

1075 focus n

1106 focus n

1076 elab' ina (Just fc') tm

1107 elab' ina (Just fc') tm

1077 env <- get_env

1108 env <- get_env

1078− ctxt <- get_context

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

1080 solve

1111 solve

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

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

1082

1113

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

1543 else casetac (forget val)

1574 else casetac (forget val)

1544 when autoSolve solveAll

1575 when autoSolve solveAll

1545

1576

1577+tacN :: String -> Name

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

1579+

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

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

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

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

1582+ runTacTm tm'

1583+ return ()

1548 where

1584 where

1585+ eval tm = do ctxt <- get_context

1549− eval = normaliseAll ctxt env . finalise

1586+ return $ normaliseAll ctxt env (finalise tm)

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

1587+

1551 returnUnit = fmap fst $ get_type_val (Var unitCon)

1588 returnUnit = fmap fst $ get_type_val (Var unitCon)

1552

1589

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

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

1585 = do env <- get_env

1622 = do env <- get_env

1586 fmap fst . get_type_val $ reflectEnv env

1623 fmap fst . get_type_val $ reflectEnv env

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

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

1625+ = do errs' <- eval errs

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

1626+ parts <- reifyReportParts errs'

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

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

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

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

1591 = return tm

1629 = return tm

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

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

1593− = do let first' = eval first

1631+ = do first' <- eval first

1594 res <- runTacTm first'

1632 res <- runTacTm first'

1595− let next = eval (App andThen res)

1633+ next <- eval (App andThen res)

1596 runTacTm next

1634 runTacTm next

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

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

1598− = do let first' = eval first

1636+ = do first' <- eval first

1599− let alt' = eval alt

1637+ alt' <- eval alt

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

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

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

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

1602 = do raw' <- reifyRaw raw

1640 = do raw' <- reifyRaw raw

1603 apply raw' []

1641 apply raw' []

1604 returnUnit

1642 returnUnit

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

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

1647+ n <- getNameFrom (sMN 0 h)

1607− fmap fst $ get_type_val (reflectName n)

1648+ fmap fst $ get_type_val (reflectName n)

1649+ _ -> fail "no hint"

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

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

1609 = do n' <- reifyTTName n

1651 = do n' <- reifyTTName n

1610 ty' <- reifyRaw ty

1652 ty' <- reifyRaw ty

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

1634 Just name -> fmap Just $ reifyTTName name

1676 Just name -> fmap Just $ reifyTTName name

1635 intro n

1677 intro n

1636 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

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

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

1638 = do let msg' = fromTTMaybe msg

1703 = do let msg' = fromTTMaybe msg

1639 case msg' of

1704 case msg' of

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

2400reflectTTQuote unq (V n)

2465reflectTTQuote unq (V n)

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

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

2402reflectTTQuote unq (Bind n b x)

2467reflectTTQuote unq (Bind n b x)

2403− = 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]

2404reflectTTQuote unq (App f x)

2469reflectTTQuote unq (App f x)

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

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

2406reflectTTQuote unq (Constant c)

2471reflectTTQuote unq (Constant c)

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

2417 | n `elem` unq = Var n

2482 | n `elem` unq = Var n

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

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

2419reflectRawQuote unq (RBind n b r) =

2484reflectRawQuote unq (RBind n b r) =

2420− 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]

2421reflectRawQuote unq (RApp f x) =

2486reflectRawQuote unq (RApp f x) =

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

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

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

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

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

2475 solve

2540 solve

2476

2541

2477reflectBinder :: Binder Term -> Raw

2542reflectBinder :: Binder Term -> Raw

2478−reflectBinder = reflectBinderQuote reflectTTQuote []

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

2479−

2544+

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

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

2481−reflectBinderQuote q unq (Lam t)

2546+reflectBinderQuote q ty unq (Lam t)

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

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

2483−reflectBinderQuote q unq (Pi _ t k)

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

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

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

2485−reflectBinderQuote q unq (Let x y)

2550+reflectBinderQuote q ty unq (Let x y)

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

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

2487−reflectBinderQuote q unq (NLet x y)

2552+reflectBinderQuote q ty unq (NLet x y)

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

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

2489−reflectBinderQuote q unq (Hole t)

2554+reflectBinderQuote q ty unq (Hole t)

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

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

2491−reflectBinderQuote q unq (GHole _ t)

2556+reflectBinderQuote q ty unq (GHole _ t)

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

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

2493−reflectBinderQuote q unq (Guess x y)

2558+reflectBinderQuote q ty unq (Guess x y)

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

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

2495−reflectBinderQuote q unq (PVar t)

2560+reflectBinderQuote q ty unq (PVar t)

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

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

2497−reflectBinderQuote q unq (PVTy t)

2562+reflectBinderQuote q ty unq (PVTy t)

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

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

2499

2564

2500mkList :: Raw -> [Raw] -> Raw

2565mkList :: Raw -> [Raw] -> Raw

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

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

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

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

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

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

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

2792

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+

2793envTupleType :: Raw

2880envTupleType :: Raw

2794envTupleType

2881envTupleType

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

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

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