c2dc6ec · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Allow new-style tactics to declare function signatures

c2dc6ecDavid Raymond Christiansen12 years ago

idris.cabal+1

compare with master

unifiedsplit

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

725 , Idris.ProofSearch

726 , Idris.Prover

727 , Idris.Providers

728+ , Idris.Reflection

728 , Idris.REPL

729 , Idris.REPL

729 , Idris.REPLParser

730 , Idris.REPLParser

730 , Idris.Transforms

731 , 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,

@@ -631,10 +635,12 @@ deriving instance NFData PDecl'

631-- For elaborator state

635-- For elaborator state

632data EState = EState {

636data EState = EState {

633 case_decls :: [PDecl],

637 case_decls :: [PDecl],

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

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

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

635 }

640 }

636

641

637−initEState = EState [] []

642+initEState :: EState

643+initEState = EState [] [] []

638

644

639type ElabD a = Elab' EState a

645type ElabD a = Elab' EState a

640

646

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

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

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

508 concatMap (Map.toList) allns

509

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

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

511addAlist [] ctxt = ctxt

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

513

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+110−25

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

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

94 when tydecl (do update_term orderPats

121 when tydecl (do update_term orderPats

95 mkPat)

122 mkPat)

96-- update_term liftPats)

123-- update_term liftPats)

97− EState is _ <- getAux

124+ EState is _ impls <- getAux

98 tt <- get_term

125 tt <- get_term

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

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

100 log <- getLog

127 log <- getLog

128+ ctxt <- get_context

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

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

102− else return (tm, ds, is)

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

103 where pattern = emode == ELHS

131 where pattern = emode == ELHS

104 tydecl = emode == ETyDecl

132 tydecl = emode == ETyDecl

105

133

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

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

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

115

143

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

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

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

145+ ElabD ElabResult

118buildTC ist info emode opts fn tm

146buildTC ist info emode opts fn tm

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

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

120 let ns = allNamesIn tm

148 let ns = allNamesIn tm

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

135 -- unification

163 -- unification

136 when (not (null dots)) $

164 when (not (null dots)) $

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

165 lift (Error (CantMatch (getInferTerm tm)))

138− EState is _ <- getAux

166+ EState is _ impls <- getAux

139 tt <- get_term

167 tt <- get_term

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

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

141 log <- getLog

169 log <- getLog

170+ ctxt <- get_context

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

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

143− else return (tm, ds, is)

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

144 where pattern = emode == ELHS

173 where pattern = emode == ELHS

145

174

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

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

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

183 _ -> return True

212 _ -> return True

184 _ -> return False

213 _ -> return False

185

214

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

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

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

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

188−

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

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

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

190 ElabD ()

219 ElabD ()

191elab ist info emode opts fn tm

220elab ist info emode opts fn tm

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

1077 focus n

1106 focus n

1078 elab' ina (Just fc') tm

1107 elab' ina (Just fc') tm

1079 env <- get_env

1108 env <- get_env

1080− ctxt <- get_context

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

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

1110+ EState _ _ todo <- getAux

1082 solve

1111 solve

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

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

1084

1113

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

1505 else casetac (forget val)

1534 else casetac (forget val)

1506 when autoSolve solveAll

1535 when autoSolve solveAll

1507

1536

1537+tacN :: String -> Name

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

1539+

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

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

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

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

1542+ runTacTm tm'

1543+ return ()

1510 where

1544 where

1545+ eval tm = do ctxt <- get_context

1511− eval = normaliseAll ctxt env . finalise

1546+ return $ normaliseAll ctxt env (finalise tm)

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

1547+

1513 returnUnit = fmap fst $ get_type_val (Var unitCon)

1548 returnUnit = fmap fst $ get_type_val (Var unitCon)

1514

1549

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

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

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

1547 = do env <- get_env

1582 = do env <- get_env

1548 fmap fst . get_type_val $ reflectEnv env

1583 fmap fst . get_type_val $ reflectEnv env

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

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

1585+ = do errs' <- eval errs

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

1586+ parts <- reifyReportParts errs'

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

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

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

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

1553 = return tm

1589 = return tm

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

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

1555− = do let first' = eval first

1591+ = do first' <- eval first

1556 res <- runTacTm first'

1592 res <- runTacTm first'

1557− let next = eval (App andThen res)

1593+ next <- eval (App andThen res)

1558 runTacTm next

1594 runTacTm next

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

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

1560− = do let first' = eval first

1596+ = do first' <- eval first

1561− let alt' = eval alt

1597+ alt' <- eval alt

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

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

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

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

1564 = do raw' <- reifyRaw raw

1600 = do raw' <- reifyRaw raw

1565 apply raw' []

1601 apply raw' []

1566 returnUnit

1602 returnUnit

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

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

1604+ = do hintStr <- eval hint

1605+ case hintStr of

1606+ Constant (Str h) -> do

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

1607+ n <- getNameFrom (sMN 0 h)

1569− fmap fst $ get_type_val (reflectName n)

1608+ fmap fst $ get_type_val (reflectName n)

1609+ _ -> fail "no hint"

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

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

1571 = do n' <- reifyTTName n

1611 = do n' <- reifyTTName n

1572 ty' <- reifyRaw ty

1612 ty' <- reifyRaw ty

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

1596 Just name -> fmap Just $ reifyTTName name

1636 Just name -> fmap Just $ reifyTTName name

1597 intro n

1637 intro n

1598 returnUnit

1638 returnUnit

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

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

1641+ ctxt <- get_context

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

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

1644+ res

1645+ rty = foldr mkPi res args

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

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

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

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

1650+ _ -> return ()

1651+ case lookupDefExact n ctxt of

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

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

1654+ Nothing -> return ()

1655+ let decl = TyDecl Ref checked

1656+ ctxt' = addCtxtDef n decl ctxt

1657+ set_context ctxt'

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

1659+ new_tyDecls e }

1660+ aux <- getAux

1661+ returnUnit

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

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

1600 = do let msg' = fromTTMaybe msg

1663 = do let msg' = fromTTMaybe msg

1601 case msg' of

1664 case msg' of

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

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

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

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

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

2751

2814

2815+reifyTyDecl :: Term -> ElabD RTyDecl

2816+reifyTyDecl (App (App (App (P (DCon _ _ _) n _) tyN) args) ret)

2817+ | n == tacN "Declare" =

2818+ do tyN' <- reifyTTName tyN

2819+ args' <- case unList args of

2820+ Nothing -> fail $ "Couldn't reify " ++ show args ++ " as an arglist."

2821+ Just xs -> mapM reifyRArg xs

2822+ ret' <- reifyRaw ret

2823+ return $ RDeclare tyN' args' ret'

2824+ where reifyRArg :: Term -> ElabD RArg

2825+ reifyRArg (App (App (P (DCon _ _ _) n _) argN) argTy)

2826+ | n == tacN "Explicit" = liftM2 RExplicit

2827+ (reifyTTName argN)

2828+ (reifyRaw argTy)

2829+ | n == tacN "Implicit" = liftM2 RImplicit

2830+ (reifyTTName argN)

2831+ (reifyRaw argTy) | n == tacN "Constraint" = liftM2 RConstraint

2832+ (reifyTTName argN)

2833+ (reifyRaw argTy)

2834+ reifyRArg aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RArg."

2835+reifyTyDecl tm = fail $ "Couldn't reify " ++ show tm ++ " as a type declaration."

2836+

2752envTupleType :: Raw

2837envTupleType :: Raw

2753envTupleType

2838envTupleType

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

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