@@ -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
@@ -94,12 +121,13 @@ build ist info emode opts fn tm
94121 when tydecl (do update_term orderPats
95122 mkPat)
96123-- update_term liftPats)
97− EState is _ <- getAux
124+ EState is _ impls <- getAux
98125 tt <- get_term
99126 let (tm, ds) = runState (collectDeferred (Just fn) tt) []
100127 log <- getLog
101− if (log /= "") then trace log $ return (tm, ds, is)
102− else return (tm, ds, is)
128+ ctxt <- get_context
129+ if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)
130+ else return (ElabResult tm ds is ctxt impls)
103131 where pattern = emode == ELHS
104132 tydecl = emode == ETyDecl
105133
@@ -114,7 +142,7 @@ build ist info emode opts fn tm
114142-- know about yet on the LHS of a pattern def)
115143
116144buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->
117− ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
145+ ElabD ElabResult
118146buildTC ist info emode opts fn tm
119147 = do -- set name supply to begin after highest index in tm
120148 let ns = allNamesIn tm
@@ -135,12 +163,13 @@ buildTC ist info emode opts fn tm
135163 -- unification
136164 when (not (null dots)) $
137165 lift (Error (CantMatch (getInferTerm tm)))
138− EState is _ <- getAux
166+ EState is _ impls <- getAux
139167 tt <- get_term
140168 let (tm, ds) = runState (collectDeferred (Just fn) tt) []
141169 log <- getLog
142− if (log /= "") then trace log $ return (tm, ds, is)
143− else return (tm, ds, is)
170+ ctxt <- get_context
171+ if (log /= "") then trace log $ return (ElabResult tm ds is ctxt impls)
172+ else return (ElabResult tm ds is ctxt impls)
144173 where pattern = emode == ELHS
145174
146175-- return whether arguments of the given constructor name can be
@@ -183,9 +212,9 @@ goal_polymorphic =
183212 _ -> return True
184213 _ -> return False
185214
186−-- Returns the set of declarations we need to add to complete the definition
187−-- (most likely case blocks to elaborate)
188−
215+-- | Returns the set of declarations we need to add to complete the
216+-- definition (most likely case blocks to elaborate) as well as
217+-- declarations resulting from user tactic scripts (%runTactics)
189218elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->
190219 ElabD ()
191220elab ist info emode opts fn tm
@@ -1077,8 +1106,8 @@ elab ist info emode opts fn tm
10771106 focus n
10781107 elab' ina (Just fc') tm
10791108 env <- get_env
1080− ctxt <- get_context
1081− runTactical (maybe fc' id fc) ctxt env (P Bound n' Erased)
1109+ runTactical (maybe fc' id fc) env (P Bound n' Erased)
1110+ EState _ _ todo <- getAux
10821111 solve
10831112 elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
10841113
@@ -1505,11 +1534,17 @@ case_ ind autoSolve ist fn tm = do
15051534 else casetac (forget val)
15061535 when autoSolve solveAll
15071536
1508−runTactical :: FC -> Context -> Env -> Term -> ElabD ()
1509−runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
1537+tacN :: String -> Name
1538+tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]
1539+
1540+runTactical :: FC -> Env -> Term -> ElabD ()
1541+runTactical fc env tm = do tm' <- eval tm
1542+ runTacTm tm'
1543+ return ()
15101544 where
1511− eval = normaliseAll ctxt env . finalise
1512− tacN str = sNS (sUN str) ["Tactical", "Reflection", "Language"]
1545+ eval tm = do ctxt <- get_context
1546+ return $ normaliseAll ctxt env (finalise tm)
1547+
15131548 returnUnit = fmap fst $ get_type_val (Var unitCon)
15141549
15151550 -- | 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 ()
15471582 = do env <- get_env
15481583 fmap fst . get_type_val $ reflectEnv env
15491584 | n == tacN "prim__Fail", [_a, errs] <- args
1550− = do parts <- reifyReportParts (eval errs)
1585+ = do errs' <- eval errs
1586+ parts <- reifyReportParts errs'
15511587 lift . tfail $ ReflectionError [parts] (Msg "")
15521588 | n == tacN "prim__PureTactical", [_a, tm] <- args
15531589 = return tm
15541590 | n == tacN "prim__BindTactical", [_a, _b, first, andThen] <- args
1555− = do let first' = eval first
1591+ = do first' <- eval first
15561592 res <- runTacTm first'
1557− let next = eval (App andThen res)
1593+ next <- eval (App andThen res)
15581594 runTacTm next
15591595 | n == tacN "prim__Try", [_a, first, alt] <- args
1560− = do let first' = eval first
1561− let alt' = eval alt
1596+ = do first' <- eval first
1597+ alt' <- eval alt
15621598 try' (runTacTm first') (runTacTm alt') True
15631599 | n == tacN "prim__Fill", [raw] <- args
15641600 = do raw' <- reifyRaw raw
15651601 apply raw' []
15661602 returnUnit
1567− | n == tacN "prim__Gensym", [eval -> Constant (Str hint)] <- args
1568− = do n <- getNameFrom (sMN 0 hint)
1569− fmap fst $ get_type_val (reflectName n)
1603+ | n == tacN "prim__Gensym", [hint] <- args
1604+ = do hintStr <- eval hint
1605+ case hintStr of
1606+ Constant (Str h) -> do
1607+ n <- getNameFrom (sMN 0 h)
1608+ fmap fst $ get_type_val (reflectName n)
1609+ _ -> fail "no hint"
15701610 | n == tacN "prim__Claim", [n, ty] <- args
15711611 = do n' <- reifyTTName n
15721612 ty' <- reifyRaw ty
@@ -1596,6 +1636,29 @@ runTactical fc ctxt env tm = runTacTm (eval tm) >> return ()
15961636 Just name -> fmap Just $ reifyTTName name
15971637 intro n
15981638 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
15991662 | n == tacN "prim__Debug", [ty, msg] <- args
16001663 = do let msg' = fromTTMaybe msg
16011664 case msg' of
@@ -2749,6 +2812,28 @@ reifyReportPart (App (P (DCon _ _ _) n _) tm)
27492812 Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm
27502813reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x
27512814
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+
27522837envTupleType :: Raw
27532838envTupleType
27542839 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")