fc57624 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Allow Elab scripts to create new metavariables

fc57624David Raymond Christiansen11 years ago

libs/prelude/Language/Reflection/Elab.idr+7−1

compare with master

unifiedsplit

@@ -120,7 +120,7 @@ data Elab : Type -> Type where

120 prim__RecursiveElab : Raw -> Elab () -> Elab (TT, TT)

121

122 prim__Debug : {a : Type} -> List ErrorReportPart -> Elab a

123−

123+ prim__Metavar : TTName -> Elab ()

124

125-------------

126-- Public API

@@ -350,6 +350,12 @@ namespace Tactics

350 debugMessage : (msg : List ErrorReportPart) -> Elab a

351 debugMessage msg = prim__Debug msg

352

353+ ||| Create a new top-level metavariable to solve the current hole.

354+ |||

355+ ||| @ name the name for the top-level variable

356+ metavar : (name : TTName) -> Elab ()

357+ metavar name = prim__Metavar name

358+

353 ||| Recursively invoke the reflected elaborator with some goal.

359 ||| Recursively invoke the reflected elaborator with some goal.

354 |||

360 |||

355 ||| The result is the final term and its type.

361 ||| The result is the final term and its type.

src/Idris/Elab/Term.hs+17−5

@@ -881,15 +881,11 @@ elab ist info emode opts fn tm

881 -- names which have been used elsewhere in the term, since we

882 -- won't be able to use them in the resulting application.

883 let unique_used = getUniqueUsed (tt_ctxt ist) ptm

884− let n' = mkN n

884+ let n' = metavarName (namespace info) n

885 attack

886 defer unique_used n'

887 solve

888 highlightSource nfc (AnnName n' (Just MetavarOutput) Nothing Nothing)

889− where mkN n@(NS _ _) = n

890− mkN n = case namespace info of

891− Just xs@(_:_) -> sNS n xs

892− _ -> n

893 elab' ina fc (PProof ts) = do compute; mapM_ (runTac True ist (elabFC info) fn) ts

889 elab' ina fc (PProof ts) = do compute; mapM_ (runTac True ist (elabFC info) fn) ts

894 elab' ina fc (PTactics ts)

890 elab' ina fc (PTactics ts)

895 | not pattern = do mapM_ (runTac False ist fc fn) ts

891 | not pattern = do mapM_ (runTac False ist fc fn) ts

@@ -1696,6 +1692,11 @@ case_ ind autoSolve ist fn tm = do

1696 else casetac (forget val)

1692 else casetac (forget val)

1697 when autoSolve solveAll

1693 when autoSolve solveAll

1698

1694

1695+-- | Compute the appropriate name for a top-level metavariable

1696+metavarName :: Maybe [String] -> Name -> Name

1697+metavarName _ n@(NS _ _) = n

1698+metavarName (Just (ns@(_:_))) n = sNS n ns

1699+metavarName _ n = n

1699

1700

1700runTactical :: IState -> FC -> Env -> Term -> [String] -> ElabD Term

1701runTactical :: IState -> FC -> Env -> Term -> [String] -> ElabD Term

1701runTactical ist fc env tm ns = do tm' <- eval tm

1702runTactical ist fc env tm ns = do tm' <- eval tm

@@ -1974,6 +1975,17 @@ runTactical ist fc env tm ns = do tm' <- eval tm

1974 fmap fst . checkClosed $

1975 fmap fst . checkClosed $

1975 rawPair (Var $ reflm "TT", Var $ reflm "TT")

1976 rawPair (Var $ reflm "TT", Var $ reflm "TT")

1976 (tm', ty')

1977 (tm', ty')

1978+ | n == tacN "prim__Metavar", [n] <- args

1979+ = do n' <- reifyTTName n

1980+ ctxt <- get_context

1981+ ptm <- get_term

1982+ -- See documentation above in the elab case for PMetavar

1983+ let unique_used = getUniqueUsed ctxt ptm

1984+ let mvn = metavarName (Just ns) n'

1985+ attack

1986+ defer unique_used mvn

1987+ solve

1988+ returnUnit

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

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

1978 = do msg' <- eval msg

1990 = do msg' <- eval msg

1979 parts <- reifyReportParts msg

1991 parts <- reifyReportParts msg