@@ -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
@@ -95,12 +122,13 @@ build ist info emode opts fn tm
95122 when tydecl (do update_term orderPats
96123 mkPat)
97124-- update_term liftPats)
98− EState is _ <- getAux
125+ EState is _ impls <- getAux
99126 tt <- get_term
100127 let (tm, ds) = runState (collectDeferred (Just fn) tt) []
101128 log <- getLog
102− if (log /= "") then trace log $ return (tm, ds, is)
103− 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)
104132 where pattern = emode == ELHS
105133 tydecl = emode == ETyDecl
106134
@@ -115,7 +143,7 @@ build ist info emode opts fn tm
115143-- know about yet on the LHS of a pattern def)
116144
117145buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->
118− ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
146+ ElabD ElabResult
119147buildTC ist info emode opts fn tm
120148 = do -- set name supply to begin after highest index in tm
121149 let ns = allNamesIn tm
@@ -136,12 +164,13 @@ buildTC ist info emode opts fn tm
136164 -- unification
137165 when (not (null dots)) $
138166 lift (Error (CantMatch (getInferTerm tm)))
139− EState is _ <- getAux
167+ EState is _ impls <- getAux
140168 tt <- get_term
141169 let (tm, ds) = runState (collectDeferred (Just fn) tt) []
142170 log <- getLog
143− if (log /= "") then trace log $ return (tm, ds, is)
144− 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)
145174 where pattern = emode == ELHS
146175
147176-- return whether arguments of the given constructor name can be
@@ -184,9 +213,9 @@ goal_polymorphic =
184213 _ -> return True
185214 _ -> return False
186215
187−-- Returns the set of declarations we need to add to complete the definition
188−-- (most likely case blocks to elaborate)
189−
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)
190219elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->
191220 ElabD ()
192221elab ist info emode opts fn tm
@@ -970,10 +999,10 @@ elab ist info emode opts fn tm
970999 = do -- First extract the unquoted subterms, replacing them with fresh
9711000 -- names in the quasiquoted term. Claim their reflections to be
9721001 -- an inferred type (to support polytypic quasiquotes).
973− qty <- goal
1002+ finalTy <- goal
9741003 (t, unq) <- extractUnquotes 0 t
9751004 let unquoteNames = map fst unq
976− mapM_ (\uqn -> claim uqn (forget qty)) unquoteNames
1005+ mapM_ (\uqn -> claim uqn (forget finalTy)) unquoteNames
9771006
9781007 -- Save the old state - we need a fresh proof state to avoid
9791008 -- capturing lexically available variables in the quoted term.
@@ -1023,18 +1052,20 @@ elab ist info emode opts fn tm
10231052 env <- get_env
10241053 loadState
10251054 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
10271058 case quoted of
10281059 Just q -> do ctxt <- get_context
10291060 (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q
10301061 if pattern
1031− then do try' (reflectTTQuotePattern unquoteNames q')
1032− (reflectRawQuotePattern unquoteNames (forget q'))
1033− True
1034− else do try' (fill $ reflectTTQuote unquoteNames q')
1035− -- we forget q' instead of using q to ensure rechecking
1036− (fill $ reflectRawQuote unquoteNames (forget q'))
1037− 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'
10381069 solve
10391070
10401071 Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"
@@ -1075,8 +1106,8 @@ elab ist info emode opts fn tm
10751106 focus n
10761107 elab' ina (Just fc') tm
10771108 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
10801111 solve
10811112 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
10821113
@@ -1543,11 +1574,17 @@ case_ ind autoSolve ist fn tm = do
15431574 else casetac (forget val)
15441575 when autoSolve solveAll
15451576
1546−runTactical :: FC -> Context -> Env -> Term -> ElabD ()
1547−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 ()
15481584 where
1549− eval = normaliseAll ctxt env . finalise
1550− tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]
1585+ eval tm = do ctxt <- get_context
1586+ return $ normaliseAll ctxt env (finalise tm)
1587+
15511588 returnUnit = fmap fst $ get_type_val (Var unitCon)
15521589
15531590 -- | 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 ()
15851622 = do env <- get_env
15861623 fmap fst . get_type_val $ reflectEnv env
15871624 | n == tacN "prim__Fail", [_a, errs] <- args
1588− = do parts <- reifyReportParts (eval errs)
1625+ = do errs' <- eval errs
1626+ parts <- reifyReportParts errs'
15891627 lift . tfail $ ReflectionError [parts] (Msg "")
15901628 | n == tacN "prim__PureTactical", [_a, tm] <- args
15911629 = return tm
15921630 | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args
1593− = do let first' = eval first
1631+ = do first' <- eval first
15941632 res <- runTacTm first'
1595− let next = eval (App andThen res)
1633+ next <- eval (App andThen res)
15961634 runTacTm next
15971635 | n == tacN "prim__Try", [_a, first, alt] <- args
1598− = do let first' = eval first
1599− let alt' = eval alt
1636+ = do first' <- eval first
1637+ alt' <- eval alt
16001638 try' (runTacTm first') (runTacTm alt') True
16011639 | n == tacN "prim__Fill", [raw] <- args
16021640 = do raw' <- reifyRaw raw
16031641 apply raw' []
16041642 returnUnit
1605− | n == tacN "prim__Gensym", [eval -> Constant (Str hint)] <- args
1606− = do n <- getNameFrom (sMN 0 hint)
1607− 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"
16081650 | n == tacN "prim__Claim", [n, ty] <- args
16091651 = do n' <- reifyTTName n
16101652 ty' <- reifyRaw ty
@@ -1634,6 +1676,29 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
16341676 Just name -> fmap Just $ reifyTTName name
16351677 intro n
16361678 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
16371702 | n == tacN "prim__Debug", [ty, msg] <- args
16381703 = do let msg' = fromTTMaybe msg
16391704 case msg' of
@@ -2400,7 +2465,7 @@ reflectTTQuote unq (P nt n t)
24002465reflectTTQuote unq (V n)
24012466 = reflCall "V" [RConstant (I n)]
24022467reflectTTQuote 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]
24042469reflectTTQuote unq (App f x)
24052470 = reflCall "App" [reflectTTQuote unq f, reflectTTQuote unq x]
24062471reflectTTQuote unq (Constant c)
@@ -2417,7 +2482,7 @@ reflectRawQuote unq (Var n)
24172482 | n `elem` unq = Var n
24182483 | otherwise = reflCall "Var" [reflectName n]
24192484reflectRawQuote 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]
24212486reflectRawQuote unq (RApp f x) =
24222487 reflCall "RApp" [reflectRawQuote unq f, reflectRawQuote unq x]
24232488reflectRawQuote unq RType = Var (reflm "RType")
@@ -2475,27 +2540,27 @@ reflectNameQuotePattern _ -- for all other names, match any
24752540 solve
24762541
24772542reflectBinder :: Binder Term -> Raw
2478−reflectBinder = reflectBinderQuote reflectTTQuote []
2479−
2480−reflectBinderQuote :: ([Name] -> a -> Raw) -> [Name] -> Binder a -> Raw
2481−reflectBinderQuote q unq (Lam t)
2482− = reflCall "Lam" [Var (reflm "TT"), q unq t]
2483−reflectBinderQuote q unq (Pi _ t k)
2484− = reflCall "Pi" [Var (reflm "TT"), q unq t, q unq k]
2485−reflectBinderQuote q unq (Let x y)
2486− = reflCall "Let" [Var (reflm "TT"), q unq x, q unq y]
2487−reflectBinderQuote q unq (NLet x y)
2488− = reflCall "NLet" [Var (reflm "TT"), q unq x, q unq y]
2489−reflectBinderQuote q unq (Hole t)
2490− = reflCall "Hole" [Var (reflm "TT"), q unq t]
2491−reflectBinderQuote q unq (GHole _ t)
2492− = reflCall "GHole" [Var (reflm "TT"), q unq t]
2493−reflectBinderQuote q unq (Guess x y)
2494− = reflCall "Guess" [Var (reflm "TT"), q unq x, q unq y]
2495−reflectBinderQuote q unq (PVar t)
2496− = reflCall "PVar" [Var (reflm "TT"), q unq t]
2497−reflectBinderQuote q unq (PVTy t)
2498− = 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]
24992564
25002565mkList :: Raw -> [Raw] -> Raw
25012566mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty
@@ -2790,6 +2855,28 @@ reifyReportPart (App (P (DCon _ _ _) n _) tm)
27902855 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm
27912856reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x
27922857
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+
27932880envTupleType :: Raw
27942881envTupleType
27952882 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")