idris-0.9.14: src/Idris/ElabTerm.hs
{-# LANGUAGE PatternGuards #-}
module Idris.ElabTerm where
import Idris.AbsSyntax
import Idris.AbsSyntaxTree
import Idris.DSL
import Idris.Delaborate
import Idris.Error
import Idris.ProofSearch
import Idris.Output (pshow)
import Idris.Core.Elaborate hiding (Tactic(..))
import Idris.Core.TT
import Idris.Core.Evaluate
import Idris.Core.Unify
import Idris.Core.Typecheck (check, recheck)
import Idris.ErrReverse (errReverse)
import Idris.ElabQuasiquote (extractUnquotes)
import Control.Applicative ((<$>))
import Control.Monad
import Control.Monad.State.Strict
import Data.List
import qualified Data.Map as M
import Data.Maybe (mapMaybe, fromMaybe)
import qualified Data.Set as S
import qualified Data.Text as T
import Debug.Trace
data ElabMode = ETyDecl | ELHS | ERHS
deriving Eq
-- Using the elaborator, convert a term in raw syntax to a fully
-- elaborated, typechecked term.
--
-- If building a pattern match, we convert undeclared variables from
-- holes to pattern bindings.
-- Also find deferred names in the term and their types
build :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->
ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
build ist info emode opts fn tm
= do elab ist info emode opts fn tm
let tmIn = tm
let inf = case lookupCtxt fn (idris_tyinfodata ist) of
[TIPartial] -> True
_ -> False
ivs <- get_instances
hs <- get_holes
ptm <- get_term
-- Resolve remaining type classes. Two passes - first to get the
-- default Num instances, second to clean up the rest
when (not pattern) $
mapM_ (\n -> when (n `elem` hs) $
do focus n
g <- goal
try (resolveTC 7 g fn ist)
(movelast n)) ivs
ivs <- get_instances
hs <- get_holes
when (not pattern) $
mapM_ (\n -> when (n `elem` hs) $
do focus n
g <- goal
resolveTC 7 g fn ist) ivs
tm <- get_term
ctxt <- get_context
probs <- get_probs
u <- getUnifyLog
hs <- get_holes
when (not pattern) $
traceWhen u ("Remaining holes:\n" ++ show hs ++ "\n" ++
"Remaining problems:\n" ++ qshow probs) $
do unify_all; matchProblems True; unifyProblems
probs <- get_probs
case probs of
[] -> return ()
((_,_,_,e,_,_):es) -> traceWhen u ("Final problems:\n" ++ show probs) $
if inf then return ()
else lift (Error e)
when tydecl (do update_term orderPats
mkPat)
-- update_term liftPats)
is <- getAux
tt <- get_term
let (tm, ds) = runState (collectDeferred (Just fn) tt) []
log <- getLog
if (log /= "") then trace log $ return (tm, ds, is)
else return (tm, ds, is)
where pattern = emode == ELHS
tydecl = emode == ETyDecl
mkPat = do hs <- get_holes
tm <- get_term
case hs of
(h: hs) -> do patvar h; mkPat
[] -> return ()
-- Build a term autogenerated as a typeclass method definition
-- (Separate, so we don't go overboard resolving things that we don't
-- know about yet on the LHS of a pattern def)
buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->
ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
buildTC ist info emode opts fn tm
= do -- set name supply to begin after highest index in tm
let ns = allNamesIn tm
let tmIn = tm
let inf = case lookupCtxt fn (idris_tyinfodata ist) of
[TIPartial] -> True
_ -> False
initNextNameFrom ns
elab ist info emode opts fn tm
probs <- get_probs
tm <- get_term
case probs of
[] -> return ()
((_,_,_,e,_,_):es) -> if inf then return ()
else lift (Error e)
is <- getAux
tt <- get_term
let (tm, ds) = runState (collectDeferred (Just fn) tt) []
log <- getLog
if (log /= "") then trace log $ return (tm, ds, is)
else return (tm, ds, is)
where pattern = emode == ELHS
-- Returns the set of declarations we need to add to complete the definition
-- (most likely case blocks to elaborate)
elab :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->
ElabD ()
elab ist info emode opts fn tm
= do let loglvl = opt_logLevel (idris_options ist)
when (loglvl > 5) $ unifyLog True
compute -- expand type synonyms, etc
elabE (False, False, False, False) tm -- (in argument, guarded, in type, in qquote)
end_unify
when pattern -- convert remaining holes to pattern vars
(do update_term orderPats
unify_all
matchProblems False -- only the ones we matched earlier
unifyProblems
mkPat)
where
pattern = emode == ELHS
bindfree = emode == ETyDecl || emode == ELHS
tcgen = Dictionary `elem` opts
reflection = Reflection `elem` opts
isph arg = case getTm arg of
Placeholder -> (True, priority arg)
tm -> (False, priority arg)
toElab ina arg = case getTm arg of
Placeholder -> Nothing
v -> Just (priority arg, elabE ina v)
toElab' ina arg = case getTm arg of
Placeholder -> Nothing
v -> Just (elabE ina v)
mkPat = do hs <- get_holes
tm <- get_term
case hs of
(h: hs) -> do patvar h; mkPat
[] -> return ()
-- | elabE elaborates an expression, possibly wrapping implicit coercions
-- and forces/delays. If you make a recursive call in elab', it is
-- normally correct to call elabE - the ones that don't are desugarings
-- typically
elabE :: (Bool, Bool, Bool, Bool) -> PTerm -> ElabD ()
elabE ina t =
--do g <- goal
--trace ("Elaborating " ++ show t ++ " : " ++ show g) $
do ct <- insertCoerce ina t
t' <- insertLazy ct
g <- goal
tm <- get_term
ps <- get_probs
hs <- get_holes
--trace ("Elaborating " ++ show t' ++ " in " ++ show g
-- ++ "\n" ++ show tm
-- ++ "\nholes " ++ show hs
-- ++ "\nproblems " ++ show ps
-- ++ "\n-----------\n") $
--trace ("ELAB " ++ show t') $
let fc = fileFC "Force"
env <- get_env
handleError (forceErr env)
(elab' ina t')
(elab' ina (PApp fc (PRef fc (sUN "Force"))
[pimp (sUN "t") Placeholder True,
pimp (sUN "a") Placeholder True,
pexp ct])) True
forceErr env (CantUnify _ t t' _ _ _)
| (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
ht == txt "Lazy'" = True
forceErr env (CantUnify _ t t' _ _ _)
| (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),
ht == txt "Lazy'" = True
forceErr env (InfiniteUnify _ t _)
| (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
ht == txt "Lazy'" = True
forceErr env (Elaborating _ _ t) = forceErr env t
forceErr env (ElaboratingArg _ _ _ t) = forceErr env t
forceErr env (At _ t) = forceErr env t
forceErr env t = False
local f = do e <- get_env
return (f `elem` map fst e)
-- | Is a constant a type?
constType :: Const -> Bool
constType (AType _) = True
constType StrType = True
constType PtrType = True
constType VoidType = True
constType _ = False
-- "guarded" means immediately under a constructor, to help find patvars
elab' :: (Bool, Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type, in a quasiquote)
-> PTerm -- ^ The term to elaborate
-> ElabD ()
elab' ina (PNoImplicits t) = elab' ina t -- skip elabE step
elab' ina PType = do apply RType []; solve
-- elab' (_,_,inty) (PConstant c)
-- | constType c && pattern && not reflection && not inty
-- = lift $ tfail (Msg "Typecase is not allowed")
elab' ina (PConstant c) = do apply (RConstant c) []; solve
elab' ina (PQuote r) = do fill r; solve
elab' ina (PTrue fc _) = try (elab' ina (PRef fc unitCon))
(elab' ina (PRef fc unitTy))
elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)
elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
= do g <- goal; resolveTC 5 g fn ist
elab' ina (PResolveTC fc)
= do c <- getNameFrom (sMN 0 "class")
instanceArg c
elab' ina (PRefl fc t)
= elab' ina (PApp fc (PRef fc eqCon) [pimp (sMN 0 "A") Placeholder True,
pimp (sMN 0 "x") t False])
elab' ina (PEq fc Placeholder Placeholder l r)
= try (do tyn <- getNameFrom (sMN 0 "aqty")
claim tyn RType
movelast tyn
elab' ina (PApp fc (PRef fc eqTy)
[pimp (sUN "A") (PRef fc tyn) True,
pimp (sUN "B") (PRef fc tyn) False,
pexp l, pexp r]))
(do atyn <- getNameFrom (sMN 0 "aqty")
btyn <- getNameFrom (sMN 0 "bqty")
claim atyn RType
movelast atyn
claim btyn RType
movelast btyn
elab' ina (PApp fc (PRef fc eqTy)
[pimp (sUN "A") (PRef fc atyn) True,
pimp (sUN "B") (PRef fc btyn) False,
pexp l, pexp r]))
elab' ina (PEq fc lt rt l r) = elab' ina (PApp fc (PRef fc eqTy)
[pimp (sUN "A") lt True,
pimp (sUN "B") rt False,
pexp l, pexp r])
elab' ina@(_, a, inty, qq) (PPair fc _ l r)
= do hnf_compute
g <- goal
case g of
TType _ -> elabE (True, a,inty, qq) (PApp fc (PRef fc pairTy)
[pexp l,pexp r])
_ -> elabE (True, a, inty, qq) (PApp fc (PRef fc pairCon)
[pimp (sMN 0 "A") Placeholder True,
pimp (sMN 0 "B") Placeholder True,
pexp l, pexp r])
elab' ina (PDPair fc p l@(PRef _ n) t r)
= case t of
Placeholder ->
do hnf_compute
g <- goal
case g of
TType _ -> asType
_ -> asValue
_ -> asType
where asType = elab' ina (PApp fc (PRef fc sigmaTy)
[pexp t,
pexp (PLam n Placeholder r)])
asValue = elab' ina (PApp fc (PRef fc existsCon)
[pimp (sMN 0 "a") t False,
pimp (sMN 0 "P") Placeholder True,
pexp l, pexp r])
elab' ina (PDPair fc p l t r) = elab' ina (PApp fc (PRef fc existsCon)
[pimp (sMN 0 "a") t False,
pimp (sMN 0 "P") Placeholder True,
pexp l, pexp r])
elab' ina (PAlternative True as)
= do hnf_compute
ty <- goal
ctxt <- get_context
let (tc, _) = unApply ty
env <- get_env
let as' = pruneByType (map fst env) tc ctxt as
-- trace (show as ++ "\n ==> " ++ showSep ", " (map showTmImpls as')) $
tryAll (zip (map (elab' ina) as') (map showHd as'))
where showHd (PApp _ (PRef _ n) _) = n
showHd (PRef _ n) = n
showHd (PApp _ h _) = showHd h
showHd x = NErased -- We probably should do something better than this here
elab' ina (PAlternative False as)
= trySeq as
where -- if none work, take the error from the first
trySeq (x : xs) = let e1 = elab' ina x in
try' e1 (trySeq' e1 xs) True
trySeq' deferr [] = proofFail deferr
trySeq' deferr (x : xs)
= try' (elab' ina x) (trySeq' deferr xs) True
elab' ina (PPatvar fc n) | bindfree = do patvar n; -- update_term liftPats
-- elab' (_, _, inty) (PRef fc f)
-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty
-- = lift $ tfail (Msg "Typecase is not allowed")
elab' (ina, guarded, inty, qq) (PRef fc n)
| (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not qq
= do ctxt <- get_context
let defined = case lookupTy n ctxt of
[] -> False
_ -> True
-- this is to stop us resolve type classes recursively
-- trace (show (n, guarded)) $
if (tcname n && ina) then erun fc $ do patvar n; -- update_term liftPats
else if (defined && not guarded)
then do apply (Var n) []; solve
else try (do apply (Var n) []; solve)
(do patvar n; ) -- update_term liftPats)
where inparamBlock n = case lookupCtxtName n (inblock info) of
[] -> False
_ -> True
bindable (NS _ _) = False
bindable (UN xs) = True
bindable n = implicitable n
elab' ina f@(PInferRef fc n) = elab' ina (PApp fc f [])
elab' ina (PRef fc n) = erun fc $ do apply (Var n) []; solve
elab' ina@(_, a, inty, qq) (PLam n Placeholder sc)
= do -- if n is a type constructor name, this makes no sense...
ctxt <- get_context
when (isTConName n ctxt) $
lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
checkPiGoal n
attack; intro (Just n);
-- trace ("------ intro " ++ show n ++ " ---- \n" ++ show ptm)
elabE (True, a, inty, qq) sc; solve
elab' ina@(_, a, inty, qq) (PLam n ty sc)
= do tyn <- getNameFrom (sMN 0 "lamty")
-- if n is a type constructor name, this makes no sense...
ctxt <- get_context
when (isTConName n ctxt) $
lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
checkPiGoal n
claim tyn RType
explicit tyn
attack
ptm <- get_term
hs <- get_holes
introTy (Var tyn) (Just n)
focus tyn
elabE (True, a, True, qq) ty
elabE (True, a, inty, qq) sc
solve
elab' ina@(_, a, _, qq) (PPi _ n Placeholder sc)
= do attack; arg n (sMN 0 "ty"); elabE (True, a, True, qq) sc; solve
elab' ina@(_, a, _, qq) (PPi _ n ty sc)
= do attack; tyn <- getNameFrom (sMN 0 "ty")
claim tyn RType
n' <- case n of
MN _ _ -> unique_hole n
_ -> return n
forall n' (Var tyn)
focus tyn
elabE (True, a, True, qq) ty
elabE (True, a, True, qq) sc
solve
elab' ina@(_, a, inty, qq) (PLet n ty val sc)
= do attack
ivs <- get_instances
tyn <- getNameFrom (sMN 0 "letty")
claim tyn RType
valn <- getNameFrom (sMN 0 "letval")
claim valn (Var tyn)
explicit valn
letbind n (Var tyn) (Var valn)
case ty of
Placeholder -> return ()
_ -> do focus tyn
explicit tyn
elabE (True, a, True, qq) ty
focus valn
elabE (True, a, True, qq) val
ivs' <- get_instances
when (not pattern) $
mapM_ (\n -> do focus n
g <- goal
hs <- get_holes
if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)
-- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))
then try (resolveTC 7 g fn ist)
(movelast n)
else movelast n)
(ivs' \\ ivs)
env <- get_env
elabE (True, a, inty, qq) sc
-- HACK: If the name leaks into its type, it may leak out of
-- scope outside, so substitute in the outer scope.
expandLet n (case lookup n env of
Just (Let t v) -> v)
solve
elab' ina@(_, a, inty, qq) (PGoal fc r n sc) = do
rty <- goal
attack
tyn <- getNameFrom (sMN 0 "letty")
claim tyn RType
valn <- getNameFrom (sMN 0 "letval")
claim valn (Var tyn)
letbind n (Var tyn) (Var valn)
focus valn
elabE (True, a, True, qq) (PApp fc r [pexp (delab ist rty)])
env <- get_env
computeLet n
elabE (True, a, inty, qq) sc
solve
-- elab' ina (PLet n Placeholder
-- (PApp fc r [pexp (delab ist rty)]) sc)
elab' ina tm@(PApp fc (PInferRef _ f) args) = do
rty <- goal
ds <- get_deferred
ctxt <- get_context
-- make a function type a -> b -> c -> ... -> rty for the
-- new function name
env <- get_env
argTys <- claimArgTys env args
fn <- getNameFrom (sMN 0 "inf_fn")
let fty = fnTy argTys rty
-- trace (show (ptm, map fst argTys)) $ focus fn
-- build and defer the function application
attack; deferType (mkN f) fty (map fst argTys); solve
-- elaborate the arguments, to unify their types. They all have to
-- be explicit.
mapM_ elabIArg (zip argTys args)
where claimArgTys env [] = return []
claimArgTys env (arg : xs) | Just n <- localVar env (getTm arg)
= do nty <- get_type (Var n)
ans <- claimArgTys env xs
return ((n, (False, forget nty)) : ans)
claimArgTys env (_ : xs)
= do an <- getNameFrom (sMN 0 "inf_argTy")
aval <- getNameFrom (sMN 0 "inf_arg")
claim an RType
claim aval (Var an)
ans <- claimArgTys env xs
return ((aval, (True, (Var an))) : ans)
fnTy [] ret = forget ret
fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi xt) (fnTy xs ret)
localVar env (PRef _ x)
= case lookup x env of
Just _ -> Just x
_ -> Nothing
localVar env _ = Nothing
elabIArg ((n, (True, ty)), def) = do focus n; elabE ina (getTm def)
elabIArg _ = return () -- already done, just a name
mkN n@(NS _ _) = n
mkN n@(SN _) = n
mkN n = case namespace info of
Just xs@(_:_) -> sNS n xs
_ -> n
elab' ina (PMatchApp fc fn)
= do (fn', imps) <- case lookupCtxtName fn (idris_implicits ist) of
[(n, args)] -> return (n, map (const True) args)
_ -> lift $ tfail (NoSuchVariable fn)
ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)
solve
elab' (_, _, inty, qq) (PApp fc (PRef _ f) args')
| isTConName f (tt_ctxt ist) && pattern && not reflection && not inty && not qq
= lift $ tfail (Msg "Typecase is not allowed")
-- if f is local, just do a simple_app
elab' (ina, g, inty, qq) tm@(PApp fc (PRef _ f) args)
= do env <- get_env
if (f `elem` map fst env && length args == 1)
then -- simple app, as below
do simple_app (elabE (ina, g, inty, qq) (PRef fc f))
(elabE (True, g, inty, qq) (getTm (head args)))
(show tm)
solve
else
do ivs <- get_instances
ps <- get_probs
-- HACK: we shouldn't resolve type classes if we're defining an instance
-- function or default definition.
let isinf = f == inferCon || tcname f
-- if f is a type class, we need to know its arguments so that
-- we can unify with them
case lookupCtxt f (idris_classes ist) of
[] -> return ()
_ -> do mapM_ setInjective (map getTm args)
-- maybe more things are solvable now
unifyProblems
ctxt <- get_context
let guarded = isConName f ctxt
-- trace ("args is " ++ show args) $ return ()
ns <- apply (Var f) (map isph args)
-- trace ("ns is " ++ show ns) $ return ()
-- mark any type class arguments as injective
mapM_ checkIfInjective (map snd ns)
unifyProblems -- try again with the new information,
-- to help with disambiguation
-- Sort so that the implicit tactics and alternatives go last
let (ns', eargs) = unzip $
sortBy cmpArg (zip ns args)
ulog <- getUnifyLog
elabArgs ist (ina || not isinf, guarded, inty, qq)
[] fc False f ns'
(f == sUN "Force")
(map (\x -> getTm x) eargs) -- TODO: remove this False arg
solve
ivs' <- get_instances
-- Attempt to resolve any type classes which have 'complete' types,
-- i.e. no holes in them
when (not pattern || (ina && not tcgen && not guarded)) $
mapM_ (\n -> do focus n
g <- goal
env <- get_env
hs <- get_holes
if all (\n -> not (n `elem` hs)) (freeNames g)
-- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))
then try (resolveTC 7 g fn ist)
(movelast n)
else movelast n)
(ivs' \\ ivs)
where -- normal < alternatives < lambdas < rewrites < tactic < default tactic
-- reason for lambdas after alternatives is that having
-- the alternative resolved can help with typechecking the lambda
-- or the rewrite. Rewrites/tactics need as much information
-- as possible about the type.
-- FIXME: Better would be to allow alternative resolution to be
-- retried after more information is in.
cmpArg (_, x) (_, y)
| constraint x && not (constraint y) = LT
| constraint y && not (constraint x) = GT
| otherwise
= compare (conDepth 0 (getTm x) + priority x + alt x)
(conDepth 0 (getTm y) + priority y + alt y)
where alt t = case getTm t of
PAlternative False _ -> 5
PAlternative True _ -> 2
PTactics _ -> 150
PLam _ _ _ -> 3
PRewrite _ _ _ _ -> 4
PResolveTC _ -> 0
_ -> 1
constraint (PConstraint _ _ _ _) = True
constraint _ = False
-- Score a point for every level where there is a non-constructor
-- function (so higher score --> done later)
-- Only relevant when on lhs
conDepth d t | not pattern = 0
conDepth d (PRef _ f) | isConName f (tt_ctxt ist) = 0
| otherwise = max (100 - d) 1
conDepth d (PApp _ f as)
= conDepth d f + sum (map (conDepth (d+1)) (map getTm as))
conDepth d (PPatvar _ _) = 0
conDepth d (PAlternative _ as) = maximum (map (conDepth d) as)
conDepth d Placeholder = 0
conDepth d (PResolveTC _) = 0
conDepth d t = max (100 - d) 1
checkIfInjective n = do
env <- get_env
case lookup n env of
Nothing -> return ()
Just b ->
case unApply (binderTy b) of
(P _ c _, args) ->
case lookupCtxt c (idris_classes ist) of
[] -> return ()
_ -> -- type class, set as injective
do mapM_ setinjArg args
-- maybe we can solve more things now...
ulog <- getUnifyLog
probs <- get_probs
traceWhen ulog ("Injective now " ++ show args ++ "\n" ++ qshow probs) $
unifyProblems
probs <- get_probs
traceWhen ulog (qshow probs) $ return ()
_ -> return ()
setinjArg (P _ n _) = setinj n
setinjArg _ = return ()
tacTm (PTactics _) = True
tacTm (PProof _) = True
tacTm _ = False
setInjective (PRef _ n) = setinj n
setInjective (PApp _ (PRef _ n) _) = setinj n
setInjective _ = return ()
elab' ina@(_, a, inty, qq) tm@(PApp fc f [arg])
= erun fc $
do simple_app (elabE ina f) (elabE (True, a, inty, qq) (getTm arg))
(show tm)
solve
elab' ina Placeholder = do (h : hs) <- get_holes
movelast h
elab' ina (PMetavar n) = let n' = mkN n in
do attack; defer n'; solve
where mkN n@(NS _ _) = n
mkN n = case namespace info of
Just xs@(_:_) -> sNS n xs
_ -> n
elab' ina (PProof ts) = do compute; mapM_ (runTac True ist fn) ts
elab' ina (PTactics ts)
| not pattern = do mapM_ (runTac False ist fn) ts
| otherwise = elab' ina Placeholder
elab' ina (PElabError e) = fail (pshow ist e)
elab' ina (PRewrite fc r sc newg)
= do attack
tyn <- getNameFrom (sMN 0 "rty")
claim tyn RType
valn <- getNameFrom (sMN 0 "rval")
claim valn (Var tyn)
letn <- getNameFrom (sMN 0 "_rewrite_rule")
letbind letn (Var tyn) (Var valn)
focus valn
elab' ina r
compute
g <- goal
rewrite (Var letn)
g' <- goal
when (g == g') $ lift $ tfail (NoRewriting g)
case newg of
Nothing -> elab' ina sc
Just t -> doEquiv t sc
solve
where doEquiv t sc =
do attack
tyn <- getNameFrom (sMN 0 "ety")
claim tyn RType
valn <- getNameFrom (sMN 0 "eqval")
claim valn (Var tyn)
letn <- getNameFrom (sMN 0 "equiv_val")
letbind letn (Var tyn) (Var valn)
focus tyn
elab' ina t
focus valn
elab' ina sc
elab' ina (PRef fc letn)
solve
elab' ina@(_, a, inty, qq) c@(PCase fc scr opts)
= do attack
tyn <- getNameFrom (sMN 0 "scty")
claim tyn RType
valn <- getNameFrom (sMN 0 "scval")
scvn <- getNameFrom (sMN 0 "scvar")
claim valn (Var tyn)
letbind scvn (Var tyn) (Var valn)
focus valn
elabE (True, a, inty, qq) scr
args <- get_env
cname <- unique_hole' True (mkCaseName fn)
let cname' = mkN cname
elab' ina (PMetavar cname')
-- if the scrutinee is one of the 'args' in env, we should
-- inspect it directly, rather than adding it as a new argument
let newdef = PClauses fc [] cname'
(caseBlock fc cname'
(map (isScr scr) (reverse args)) opts)
-- elaborate case
env <- get_env
updateAux (newdef : )
-- if we haven't got the type yet, hopefully we'll get it later!
movelast tyn
solve
where mkCaseName (NS n ns) = NS (mkCaseName n) ns
mkCaseName n = SN (CaseN n)
-- mkCaseName (UN x) = UN (x ++ "_case")
-- mkCaseName (MN i x) = MN i (x ++ "_case")
mkN n@(NS _ _) = n
mkN n = case namespace info of
Just xs@(_:_) -> sNS n xs
_ -> n
elab' ina (PUnifyLog t) = do unifyLog True
elab' ina t
unifyLog False
elab' (ina, g, inty, qq) (PQuasiquote t goal) -- TODO: goal type
= do -- First extract the unquoted subterms, replacing them with fresh
-- names in the quasiquoted term. Claim their reflections to be
-- of type TT.
(t, unq) <- extractUnquotes t
let unquoteNames = map fst unq
mapM_ (flip claim (Var tt)) unquoteNames
-- Save the old state - we need a fresh proof state to avoid
-- capturing lexically available variables in the quoted term.
ctxt <- get_context
saveState
updatePS (const .
newProof (sMN 0 "q") ctxt $
P Ref tt Erased)
-- Re-add the unquotes, letting Idris infer the (fictional)
-- types. Here, they represent the real type rather than the type
-- of their reflection.
mapM_ (\n -> do ty <- getNameFrom (sMN 0 "unqTy")
claim ty RType
movelast ty
claim n (Var ty)
movelast n)
unquoteNames
-- Determine whether there's an explicit goal type, and act accordingly
-- Establish holes for the type and value of the term to be
-- quasiquoted
qTy <- getNameFrom (sMN 0 "qquoteTy")
claim qTy RType
movelast qTy
qTm <- getNameFrom (sMN 0 "qquoteTm")
claim qTm (Var qTy)
-- Let-bind the result of elaborating the contained term, so that
-- the hole doesn't disappear
nTm <- getNameFrom (sMN 0 "quotedTerm")
letbind nTm (Var qTy) (Var qTm)
-- Fill out the goal type, if relevant
case goal of
Nothing -> return ()
Just gTy -> do focus qTy
elabE (ina, g, inty, True) gTy
-- Elaborate the quasiquoted term into the hole
focus qTm
elabE (ina, g, inty, True) t
end_unify
-- We now have an elaborated term. Reflect it and solve the
-- original goal in the original proof state.
env <- get_env
loadState
let quoted = fmap (explicitNames . binderVal) $ lookup nTm env
case quoted of
Just q -> do ctxt <- get_context
(q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q
if pattern
then reflectQuotePattern unquoteNames q'
else do fill $ reflectQuote unquoteNames q'
solve
Nothing -> lift . tfail . Msg $ "Broken elaboration of quasiquote"
-- Finally fill in the terms or patterns from the unquotes. This
-- happens last so that their holes still exist while elaborating
-- the main quotation.
mapM_ elabUnquote unq
where tt = sNS (sUN "TT") ["Reflection", "Language"]
elabUnquote (n, tm)
= do focus n
elabE (ina, g, inty, False) tm
elab' ina (PUnquote t) = fail "Found unquote outside of quasiquote"
elab' ina x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))
isScr (PRef _ n) (n', b) = (n', (n == n', b))
isScr _ (n', b) = (n', (False, b))
caseBlock :: FC -> Name ->
[(Name, (Bool, Binder Term))] -> [(PTerm, PTerm)] -> [PClause]
caseBlock fc n env opts
= let args' = findScr env
args = map mkarg (map getNmScr args') in
map (mkClause args) opts
where -- Find the variable we want as the scrutinee and mark it as
-- 'True'. If the scrutinee is in the environment, match on that
-- otherwise match on the new argument we're adding.
findScr ((n, (True, t)) : xs)
= (n, (True, t)) : scrName n xs
findScr [(n, (_, t))] = [(n, (True, t))]
findScr (x : xs) = x : findScr xs
-- [] can't happen since scrutinee is in the environment!
-- To make sure top level pattern name remains in scope, put
-- it at the end of the environment
scrName n [] = []
scrName n [(_, t)] = [(n, t)]
scrName n (x : xs) = x : scrName n xs
getNmScr (n, (s, _)) = (n, s)
mkarg (n, s) = (PRef fc n, s)
-- may be shadowed names in the new pattern - so replace the
-- old ones with an _
mkClause args (l, r)
= let args' = map (shadowed (allNamesIn l)) args
lhs = PApp (getFC fc l) (PRef (getFC fc l) n)
(map (mkLHSarg l) args') in
PClause (getFC fc l) n lhs [] r []
mkLHSarg l (tm, True) = pexp l
mkLHSarg l (tm, False) = pexp tm
shadowed new (PRef _ n, s) | n `elem` new = (Placeholder, s)
shadowed new t = t
getFC d (PApp fc _ _) = fc
getFC d (PRef fc _) = fc
getFC d (PAlternative _ (x:_)) = getFC d x
getFC d x = d
insertLazy :: PTerm -> ElabD PTerm
insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Delay" = return t
insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Force" = return t
insertLazy (PCoerced t) = return t
insertLazy t =
do ty <- goal
env <- get_env
let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty)
let tries = if pattern then [t, mkDelay env t] else [mkDelay env t, t]
case tyh of
P _ (UN l) _ | l == txt "Lazy'"
-> return (PAlternative False tries)
_ -> return t
where
mkDelay env (PAlternative b xs) = PAlternative b (map (mkDelay env) xs)
mkDelay env t
= let fc = fileFC "Delay" in
addImplBound ist (map fst env) (PApp fc (PRef fc (sUN "Delay"))
[pexp t])
-- case is tricky enough without implicit coercions! If they are needed,
-- they can go in the branches separately.
insertCoerce ina t@(PCase _ _ _) = return t
insertCoerce ina t =
do ty <- goal
-- Check for possible coercions to get to the goal
-- and add them as 'alternatives'
env <- get_env
let ty' = normalise (tt_ctxt ist) env ty
let cs = getCoercionsTo ist ty'
let t' = case (t, cs) of
(PCoerced tm, _) -> tm
(_, []) -> t
(_, cs) -> PAlternative False [t ,
PAlternative True (map (mkCoerce env t) cs)]
return t'
where
mkCoerce env t n = let fc = fileFC "Coercion" in -- line never appears!
addImplBound ist (map fst env)
(PApp fc (PRef fc n) [pexp (PCoerced t)])
-- | Elaborate the arguments to a function
elabArgs :: IState -- ^ The current Idris state
-> (Bool, Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type, in a qquote)
-> [Bool]
-> FC -- ^ Source location
-> Bool
-> Name -- ^ Name of the function being applied
-> [(Name, Name)] -- ^ (Argument Name, Hole Name)
-> Bool -- ^ under a 'force'
-> [PTerm] -- ^ (Laziness, argument)
-> ElabD ()
elabArgs ist ina failed fc retry f [] force _ = return ()
elabArgs ist ina failed fc r f (n:ns) force (Placeholder : args)
= elabArgs ist ina failed fc r f ns force args
elabArgs ist ina failed fc r f ((argName, holeName):ns) force (t : args)
= do elabArg argName holeName t
where elabArg argName holeName t =
do now_elaborating fc f argName
wrapErr f argName $ do
hs <- get_holes
tm <- get_term
-- No coercing under an explicit Force (or it can Force/Delay
-- recursively!)
let elab = if force then elab' else elabE
failed' <- -- trace (show (n, t, hs, tm)) $
-- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $
case holeName `elem` hs of
True -> do focus holeName;
g <- goal
ulog <- getUnifyLog
traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $
elab ina t; return failed
False -> return failed
done_elaborating_arg f argName
elabArgs ist ina failed fc r f ns force args
wrapErr f argName action =
do elabState <- get
while <- elaborating_app
let while' = map (\(x, y, z)-> (y, z)) while
(result, newState) <- case runStateT action elabState of
OK (res, newState) -> return (res, newState)
Error e -> do done_elaborating_arg f argName
lift (tfail (elaboratingArgErr while' e))
put newState
return result
-- For every alternative, look at the function at the head. Automatically resolve
-- any nested alternatives where that function is also at the head
pruneAlt :: [PTerm] -> [PTerm]
pruneAlt xs = map prune xs
where
prune (PApp fc1 (PRef fc2 f) as)
= PApp fc1 (PRef fc2 f) (fmap (fmap (choose f)) as)
prune t = t
choose f (PAlternative a as)
= let as' = fmap (choose f) as
fs = filter (headIs f) as' in
case fs of
[a] -> a
_ -> PAlternative a as'
choose f (PApp fc f' as) = PApp fc (choose f f') (fmap (fmap (choose f)) as)
choose f t = t
headIs f (PApp _ (PRef _ f') _) = f == f'
headIs f (PApp _ f' _) = headIs f f'
headIs f _ = True -- keep if it's not an application
-- Rule out alternatives that don't return the same type as the head of the goal
-- (If there are none left as a result, do nothing)
pruneByType :: [Name] -> Term -> Context -> [PTerm] -> [PTerm]
-- if an alternative has a locally bound name at the head, take it
pruneByType env t c as
| Just a <- locallyBound as = [a]
where
locallyBound [] = Nothing
locallyBound (t:ts)
| Just n <- getName t,
n `elem` env = Just t
| otherwise = locallyBound ts
getName (PRef _ n) = Just n
getName (PApp _ f _) = getName f
getName _ = Nothing
pruneByType env (P _ n _) c as
-- if the goal type is polymorphic, keep e
| [] <- lookupTy n c = as
| otherwise
= let asV = filter (headIs True n) as
as' = filter (headIs False n) as in
case as' of
[] -> case asV of
[] -> as
_ -> asV
_ -> as'
where
headIs var f (PApp _ (PRef _ f') _) = typeHead var f f'
headIs var f (PApp _ f' _) = headIs var f f'
headIs var f (PPi _ _ _ sc) = headIs var f sc
headIs _ _ _ = True -- keep if it's not an application
typeHead var f f'
= case lookupTy f' c of
[ty] -> let ty' = normalise c [] ty in
case unApply (getRetTy ty') of
(P _ ftyn _, _) -> ftyn == f
(V _, _) -> var -- keep, variable
_ -> False
_ -> False
pruneByType _ t _ as = as
findInstances :: IState -> Term -> [Name]
findInstances ist t
| (P _ n _, _) <- unApply t
= case lookupCtxt n (idris_classes ist) of
[CI _ _ _ _ _ ins] -> ins
_ -> []
| otherwise = []
trivial' ist
= trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
proofSearch' ist rec depth prv top n hints
= do unifyProblems
proofSearch rec prv depth
(elab ist toplevel ERHS [] (sMN 0 "tac")) top n hints ist
resolveTC :: Int -> Term -> Name -> IState -> ElabD ()
resolveTC = resTC' []
resTC' tcs 0 topg fn ist = fail $ "Can't resolve type class"
resTC' tcs 1 topg fn ist = try' (trivial' ist) (resolveTC 0 topg fn ist) True
resTC' tcs depth topg fn ist
= do hnf_compute
g <- goal
ptm <- get_term
ulog <- getUnifyLog
hs <- get_holes
traceWhen ulog ("Resolving class " ++ show g) $
try' (trivial' ist)
(do t <- goal
let (tc, ttypes) = unApply t
scopeOnly <- needsDefault t tc ttypes
let insts_in = findInstances ist t
let insts = if scopeOnly then filter chaser insts_in
else insts_in
tm <- get_term
let depth' = if scopeOnly then 2 else depth
blunderbuss t depth' insts) True
where
elabTC n | n /= fn && tcname n = (resolve n depth, show n)
| otherwise = (fail "Can't resolve", show n)
-- HACK! Rather than giving a special name, better to have some kind
-- of flag in ClassInfo structure
chaser (UN nm)
| ('@':'@':_) <- str nm = True -- old way
chaser (SN (ParentN _ _)) = True
chaser (NS n _) = chaser n
chaser _ = False
numclass = sNS (sUN "Num") ["Classes","Prelude"]
needsDefault t num@(P _ nc _) [P Bound a _] | nc == numclass
= do focus a
fill (RConstant (AType (ATInt ITBig))) -- default Integer
solve
return False
needsDefault t f as
| all boundVar as = return True -- fail $ "Can't resolve " ++ show t
needsDefault t f a = return False -- trace (show t) $ return ()
boundVar (P Bound _ _) = True
boundVar _ = False
blunderbuss t d [] = do -- c <- get_env
-- ps <- get_probs
lift $ tfail $ CantResolve topg
blunderbuss t d (n:ns)
| n /= fn && tcname n = try' (resolve n d)
(blunderbuss t d ns) True
| otherwise = blunderbuss t d ns
resolve n depth
| depth == 0 = fail $ "Can't resolve type class"
| otherwise
= do t <- goal
let (tc, ttypes) = unApply t
-- if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist
-- else do
-- if there's a hole in the goal, don't even try
let imps = case lookupCtxtName n (idris_implicits ist) of
[] -> []
[args] -> map isImp (snd args) -- won't be overloaded!
ps <- get_probs
tm <- get_term
args <- map snd <$> try' (apply (Var n) imps)
(match_apply (Var n) imps) True
ps' <- get_probs
when (length ps < length ps' || unrecoverable ps') $
fail "Can't apply type class"
-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $
mapM_ (\ (_,n) -> do focus n
t' <- goal
let (tc', ttype) = unApply t'
let got = fst (unApply t)
let depth' = if tc' `elem` tcs
then depth - 1 else depth
resTC' (got : tcs) depth' topg fn ist)
(filter (\ (x, y) -> not x) (zip (map fst imps) args))
-- if there's any arguments left, we've failed to resolve
hs <- get_holes
ulog <- getUnifyLog
solve
traceWhen ulog ("Got " ++ show n) $ return ()
where isImp (PImp p _ _ _ _) = (True, p)
isImp arg = (False, priority arg)
collectDeferred :: Maybe Name ->
Term -> State [(Name, (Int, Maybe Name, Type))] Term
collectDeferred top (Bind n (GHole i t) app) =
do ds <- get
t' <- collectDeferred top t
when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t'))])
collectDeferred top app
collectDeferred top (Bind n b t) = do b' <- cdb b
t' <- collectDeferred top t
return (Bind n b' t')
where
cdb (Let t v) = liftM2 Let (collectDeferred top t) (collectDeferred top v)
cdb (Guess t v) = liftM2 Guess (collectDeferred top t) (collectDeferred top v)
cdb b = do ty' <- collectDeferred top (binderTy b)
return (b { binderTy = ty' })
collectDeferred top (App f a) = liftM2 App (collectDeferred top f) (collectDeferred top a)
collectDeferred top t = return t
case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()
case_ ind autoSolve ist fn tm = do
attack
tyn <- getNameFrom (sMN 0 "ity")
claim tyn RType
valn <- getNameFrom (sMN 0 "ival")
claim valn (Var tyn)
letn <- getNameFrom (sMN 0 "irule")
letbind letn (Var tyn) (Var valn)
focus valn
elab ist toplevel ERHS [] (sMN 0 "tac") tm
env <- get_env
let (Just binding) = lookup letn env
let val = binderVal binding
if ind then induction (forget val)
else casetac (forget val)
when autoSolve solveAll
-- Running tactics directly
-- if a tactic adds unification problems, return an error
runTac :: Bool -> IState -> Name -> PTactic -> ElabD ()
runTac autoSolve ist fn tac
= do env <- get_env
g <- goal
let tac' = fmap (addImplBound ist (map fst env)) tac
if autoSolve
then runT tac'
else no_errors (runT tac')
(Just (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env)))
where
runT (Intro []) = do g <- goal
attack; intro (bname g)
where
bname (Bind n _ _) = Just n
bname _ = Nothing
runT (Intro xs) = mapM_ (\x -> do attack; intro (Just x)) xs
runT Intros = do g <- goal
attack; intro (bname g)
try' (runT Intros)
(return ()) True
where
bname (Bind n _ _) = Just n
bname _ = Nothing
runT (Exact tm) = do elab ist toplevel ERHS [] (sMN 0 "tac") tm
when autoSolve solveAll
runT (MatchRefine fn)
= do fnimps <-
case lookupCtxtName fn (idris_implicits ist) of
[] -> do a <- envArgs fn
return [(fn, a)]
ns -> return (map (\ (n, a) -> (n, map (const True) a)) ns)
let tacs = map (\ (fn', imps) ->
(match_apply (Var fn') (map (\x -> (x, 0)) imps),
fn')) fnimps
tryAll tacs
when autoSolve solveAll
where envArgs n = do e <- get_env
case lookup n e of
Just t -> return $ map (const False)
(getArgTys (binderTy t))
_ -> return []
runT (Refine fn [])
= do fnimps <-
case lookupCtxtName fn (idris_implicits ist) of
[] -> do a <- envArgs fn
return [(fn, a)]
ns -> return (map (\ (n, a) -> (n, map isImp a)) ns)
let tacs = map (\ (fn', imps) ->
(apply (Var fn') (map (\x -> (x, 0)) imps),
fn')) fnimps
tryAll tacs
when autoSolve solveAll
where isImp (PImp _ _ _ _ _) = True
isImp _ = False
envArgs n = do e <- get_env
case lookup n e of
Just t -> return $ map (const False)
(getArgTys (binderTy t))
_ -> return []
runT (Refine fn imps) = do ns <- apply (Var fn) (map (\x -> (x,0)) imps)
when autoSolve solveAll
runT DoUnify = do unify_all
when autoSolve solveAll
runT (Equiv tm) -- let bind tm, then
= do attack
tyn <- getNameFrom (sMN 0 "ety")
claim tyn RType
valn <- getNameFrom (sMN 0 "eqval")
claim valn (Var tyn)
letn <- getNameFrom (sMN 0 "equiv_val")
letbind letn (Var tyn) (Var valn)
focus tyn
elab ist toplevel ERHS [] (sMN 0 "tac") tm
focus valn
when autoSolve solveAll
runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that
= do attack; -- (h:_) <- get_holes
tyn <- getNameFrom (sMN 0 "rty")
-- start_unify h
claim tyn RType
valn <- getNameFrom (sMN 0 "rval")
claim valn (Var tyn)
letn <- getNameFrom (sMN 0 "rewrite_rule")
letbind letn (Var tyn) (Var valn)
focus valn
elab ist toplevel ERHS [] (sMN 0 "tac") tm
rewrite (Var letn)
when autoSolve solveAll
runT (Induction tm) -- let bind tm, similar to the others
= case_ True autoSolve ist fn tm
runT (CaseTac tm)
= case_ False autoSolve ist fn tm
runT (LetTac n tm)
= do attack
tyn <- getNameFrom (sMN 0 "letty")
claim tyn RType
valn <- getNameFrom (sMN 0 "letval")
claim valn (Var tyn)
letn <- unique_hole n
letbind letn (Var tyn) (Var valn)
focus valn
elab ist toplevel ERHS [] (sMN 0 "tac") tm
when autoSolve solveAll
runT (LetTacTy n ty tm)
= do attack
tyn <- getNameFrom (sMN 0 "letty")
claim tyn RType
valn <- getNameFrom (sMN 0 "letval")
claim valn (Var tyn)
letn <- unique_hole n
letbind letn (Var tyn) (Var valn)
focus tyn
elab ist toplevel ERHS [] (sMN 0 "tac") ty
focus valn
elab ist toplevel ERHS [] (sMN 0 "tac") tm
when autoSolve solveAll
runT Compute = compute
runT Trivial = do trivial' ist; when autoSolve solveAll
runT TCInstance = runT (Exact (PResolveTC emptyFC))
runT (ProofSearch rec prover depth top hints)
= do proofSearch' ist rec depth prover top fn hints
when autoSolve solveAll
runT (Focus n) = focus n
runT Solve = solve
runT (Try l r) = do try' (runT l) (runT r) True
runT (TSeq l r) = do runT l; runT r
runT (ApplyTactic tm) = do tenv <- get_env -- store the environment
tgoal <- goal -- store the goal
attack -- let f : List (TTName, Binder TT) -> TT -> Tactic = tm in ...
script <- getNameFrom (sMN 0 "script")
claim script scriptTy
scriptvar <- getNameFrom (sMN 0 "scriptvar" )
letbind scriptvar scriptTy (Var script)
focus script
elab ist toplevel ERHS [] (sMN 0 "tac") tm
(script', _) <- get_type_val (Var scriptvar)
-- now that we have the script apply
-- it to the reflected goal and context
restac <- getNameFrom (sMN 0 "restac")
claim restac tacticTy
focus restac
fill (raw_apply (forget script')
[reflectEnv tenv, reflect tgoal])
restac' <- get_guess
solve
-- normalise the result in order to
-- reify it
ctxt <- get_context
env <- get_env
let tactic = normalise ctxt env restac'
runReflected tactic
where tacticTy = Var (reflm "Tactic")
listTy = Var (sNS (sUN "List") ["List", "Prelude"])
scriptTy = (RBind (sMN 0 "__pi_arg")
(Pi (RApp listTy envTupleType))
(RBind (sMN 1 "__pi_arg")
(Pi (Var $ reflm "TT")) tacticTy))
runT (ByReflection tm) -- run the reflection function 'tm' on the
-- goal, then apply the resulting reflected Tactic
= do tgoal <- goal
attack
script <- getNameFrom (sMN 0 "script")
claim script scriptTy
scriptvar <- getNameFrom (sMN 0 "scriptvar" )
letbind scriptvar scriptTy (Var script)
focus script
ptm <- get_term
elab ist toplevel ERHS [] (sMN 0 "tac")
(PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])
(script', _) <- get_type_val (Var scriptvar)
-- now that we have the script apply
-- it to the reflected goal
restac <- getNameFrom (sMN 0 "restac")
claim restac tacticTy
focus restac
fill (forget script')
restac' <- get_guess
solve
-- normalise the result in order to
-- reify it
ctxt <- get_context
env <- get_env
let tactic = normalise ctxt env restac'
runReflected tactic
where tacticTy = Var (reflm "Tactic")
scriptTy = tacticTy
runT (Reflect v) = do attack -- let x = reflect v in ...
tyn <- getNameFrom (sMN 0 "letty")
claim tyn RType
valn <- getNameFrom (sMN 0 "letval")
claim valn (Var tyn)
letn <- getNameFrom (sMN 0 "letvar")
letbind letn (Var tyn) (Var valn)
focus valn
elab ist toplevel ERHS [] (sMN 0 "tac") v
(value, _) <- get_type_val (Var letn)
ctxt <- get_context
env <- get_env
let value' = hnf ctxt env value
runTac autoSolve ist fn (Exact $ PQuote (reflect value'))
runT (Fill v) = do attack -- let x = fill x in ...
tyn <- getNameFrom (sMN 0 "letty")
claim tyn RType
valn <- getNameFrom (sMN 0 "letval")
claim valn (Var tyn)
letn <- getNameFrom (sMN 0 "letvar")
letbind letn (Var tyn) (Var valn)
focus valn
elab ist toplevel ERHS [] (sMN 0 "tac") v
(value, _) <- get_type_val (Var letn)
ctxt <- get_context
env <- get_env
let value' = normalise ctxt env value
rawValue <- reifyRaw value'
runTac autoSolve ist fn (Exact $ PQuote rawValue)
runT (GoalType n tac) = do g <- goal
case unApply g of
(P _ n' _, _) ->
if nsroot n' == sUN n
then runT tac
else fail "Wrong goal type"
_ -> fail "Wrong goal type"
runT ProofState = do g <- goal
return ()
runT x = fail $ "Not implemented " ++ show x
runReflected t = do t' <- reify ist t
runTac autoSolve ist fn t'
-- | Prefix a name with the "Language.Reflection" namespace
reflm :: String -> Name
reflm n = sNS (sUN n) ["Reflection", "Language"]
-- | Reify tactics from their reflected representation
reify :: IState -> Term -> ElabD PTactic
reify _ (P _ n _) | n == reflm "Intros" = return Intros
reify _ (P _ n _) | n == reflm "Trivial" = return Trivial
reify _ (P _ n _) | n == reflm "Instance" = return TCInstance
reify _ (P _ n _) | n == reflm "Solve" = return Solve
reify _ (P _ n _) | n == reflm "Compute" = return Compute
reify ist t@(App _ _)
| (P _ f _, args) <- unApply t = reifyApp ist f args
reify _ t = fail ("Unknown tactic " ++ show t)
reifyApp :: IState -> Name -> [Term] -> ElabD PTactic
reifyApp ist t [l, r] | t == reflm "Try" = liftM2 Try (reify ist l) (reify ist r)
reifyApp _ t [Constant (I i)]
| t == reflm "Search" = return (ProofSearch True True i Nothing [])
reifyApp _ t [x]
| t == reflm "Refine" = do n <- reifyTTName x
return $ Refine n []
reifyApp ist t [l, r] | t == reflm "Seq" = liftM2 TSeq (reify ist l) (reify ist r)
reifyApp ist t [Constant (Str n), x]
| t == reflm "GoalType" = liftM (GoalType n) (reify ist x)
reifyApp _ t [n] | t == reflm "Intro" = liftM (Intro . (:[])) (reifyTTName n)
reifyApp ist t [t'] | t == reflm "Induction" = liftM (Induction . delab ist) (reifyTT t')
reifyApp ist t [t'] | t == reflm "Case" = liftM (Induction . delab ist) (reifyTT t')
reifyApp ist t [t']
| t == reflm "ApplyTactic" = liftM (ApplyTactic . delab ist) (reifyTT t')
reifyApp ist t [t']
| t == reflm "Reflect" = liftM (Reflect . delab ist) (reifyTT t')
reifyApp ist t [t']
| t == reflm "ByReflection" = liftM (ByReflection . delab ist) (reifyTT t')
reifyApp _ t [t']
| t == reflm "Fill" = liftM (Fill . PQuote) (reifyRaw t')
reifyApp ist t [t']
| t == reflm "Exact" = liftM (Exact . delab ist) (reifyTT t')
reifyApp ist t [x]
| t == reflm "Focus" = liftM Focus (reifyTTName x)
reifyApp ist t [t']
| t == reflm "Rewrite" = liftM (Rewrite . delab ist) (reifyTT t')
reifyApp ist t [n, t']
| t == reflm "LetTac" = do n' <- reifyTTName n
t'' <- reifyTT t'
return $ LetTac n' (delab ist t')
reifyApp ist t [n, tt', t']
| t == reflm "LetTacTy" = do n' <- reifyTTName n
tt'' <- reifyTT tt'
t'' <- reifyTT t'
return $ LetTacTy n' (delab ist tt'') (delab ist t'')
reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args)) -- shouldn't happen
-- | Reify terms from their reflected representation
reifyTT :: Term -> ElabD Term
reifyTT t@(App _ _)
| (P _ f _, args) <- unApply t = reifyTTApp f args
reifyTT t@(P _ n _)
| n == reflm "Erased" = return $ Erased
reifyTT t@(P _ n _)
| n == reflm "Impossible" = return $ Impossible
reifyTT t = fail ("Unknown reflection term: " ++ show t)
reifyTTApp :: Name -> [Term] -> ElabD Term
reifyTTApp t [nt, n, x]
| t == reflm "P" = do nt' <- reifyTTNameType nt
n' <- reifyTTName n
x' <- reifyTT x
return $ P nt' n' x'
reifyTTApp t [Constant (I i)]
| t == reflm "V" = return $ V i
reifyTTApp t [n, b, x]
| t == reflm "Bind" = do n' <- reifyTTName n
b' <- reifyTTBinder reifyTT (reflm "TT") b
x' <- reifyTT x
return $ Bind n' b' x'
reifyTTApp t [f, x]
| t == reflm "App" = do f' <- reifyTT f
x' <- reifyTT x
return $ App f' x'
reifyTTApp t [c]
| t == reflm "TConst" = liftM Constant (reifyTTConst c)
reifyTTApp t [t', Constant (I i)]
| t == reflm "Proj" = do t'' <- reifyTT t'
return $ Proj t'' i
reifyTTApp t [tt]
| t == reflm "TType" = liftM TType (reifyTTUExp tt)
reifyTTApp t args = fail ("Unknown reflection term: " ++ show (t, args))
-- | Reify raw terms from their reflected representation
reifyRaw :: Term -> ElabD Raw
reifyRaw t@(App _ _)
| (P _ f _, args) <- unApply t = reifyRawApp f args
reifyRaw t@(P _ n _)
| n == reflm "RType" = return $ RType
reifyRaw t = fail ("Unknown reflection raw term: " ++ show t)
reifyRawApp :: Name -> [Term] -> ElabD Raw
reifyRawApp t [n]
| t == reflm "Var" = liftM Var (reifyTTName n)
reifyRawApp t [n, b, x]
| t == reflm "RBind" = do n' <- reifyTTName n
b' <- reifyTTBinder reifyRaw (reflm "Raw") b
x' <- reifyRaw x
return $ RBind n' b' x'
reifyRawApp t [f, x]
| t == reflm "RApp" = liftM2 RApp (reifyRaw f) (reifyRaw x)
reifyRawApp t [t']
| t == reflm "RForce" = liftM RForce (reifyRaw t')
reifyRawApp t [c]
| t == reflm "RConstant" = liftM RConstant (reifyTTConst c)
reifyRawApp t args = fail ("Unknown reflection raw term: " ++ show (t, args))
reifyTTName :: Term -> ElabD Name
reifyTTName t
| (P _ f _, args) <- unApply t = reifyTTNameApp f args
reifyTTName t = fail ("Unknown reflection term name: " ++ show t)
reifyTTNameApp :: Name -> [Term] -> ElabD Name
reifyTTNameApp t [Constant (Str n)]
| t == reflm "UN" = return $ sUN n
reifyTTNameApp t [n, ns]
| t == reflm "NS" = do n' <- reifyTTName n
ns' <- reifyTTNamespace ns
return $ sNS n' ns'
reifyTTNameApp t [Constant (I i), Constant (Str n)]
| t == reflm "MN" = return $ sMN i n
reifyTTNameApp t []
| t == reflm "NErased" = return NErased
reifyTTNameApp t args = fail ("Unknown reflection term name: " ++ show (t, args))
reifyTTNamespace :: Term -> ElabD [String]
reifyTTNamespace t@(App _ _)
= case unApply t of
(P _ f _, [Constant StrType])
| f == sNS (sUN "Nil") ["List", "Prelude"] -> return []
(P _ f _, [Constant StrType, Constant (Str n), ns])
| f == sNS (sUN "::") ["List", "Prelude"] -> liftM (n:) (reifyTTNamespace ns)
_ -> fail ("Unknown reflection namespace arg: " ++ show t)
reifyTTNamespace t = fail ("Unknown reflection namespace arg: " ++ show t)
reifyTTNameType :: Term -> ElabD NameType
reifyTTNameType t@(P _ n _) | n == reflm "Bound" = return $ Bound
reifyTTNameType t@(P _ n _) | n == reflm "Ref" = return $ Ref
reifyTTNameType t@(App _ _)
= case unApply t of
(P _ f _, [Constant (I tag), Constant (I num)])
| f == reflm "DCon" -> return $ DCon tag num
| f == reflm "TCon" -> return $ TCon tag num
_ -> fail ("Unknown reflection name type: " ++ show t)
reifyTTNameType t = fail ("Unknown reflection name type: " ++ show t)
reifyTTBinder :: (Term -> ElabD a) -> Name -> Term -> ElabD (Binder a)
reifyTTBinder reificator binderType t@(App _ _)
= case unApply t of
(P _ f _, bt:args) | forget bt == Var binderType
-> reifyTTBinderApp reificator f args
_ -> fail ("Mismatching binder reflection: " ++ show t)
reifyTTBinder _ _ t = fail ("Unknown reflection binder: " ++ show t)
reifyTTBinderApp :: (Term -> ElabD a) -> Name -> [Term] -> ElabD (Binder a)
reifyTTBinderApp reif f [t]
| f == reflm "Lam" = liftM Lam (reif t)
reifyTTBinderApp reif f [t]
| f == reflm "Pi" = liftM Pi (reif t)
reifyTTBinderApp reif f [x, y]
| f == reflm "Let" = liftM2 Let (reif x) (reif y)
reifyTTBinderApp reif f [x, y]
| f == reflm "NLet" = liftM2 NLet (reif x) (reif y)
reifyTTBinderApp reif f [t]
| f == reflm "Hole" = liftM Hole (reif t)
reifyTTBinderApp reif f [t]
| f == reflm "GHole" = liftM (GHole 0) (reif t)
reifyTTBinderApp reif f [x, y]
| f == reflm "Guess" = liftM2 Guess (reif x) (reif y)
reifyTTBinderApp reif f [t]
| f == reflm "PVar" = liftM PVar (reif t)
reifyTTBinderApp reif f [t]
| f == reflm "PVTy" = liftM PVTy (reif t)
reifyTTBinderApp _ f args = fail ("Unknown reflection binder: " ++ show (f, args))
reifyTTConst :: Term -> ElabD Const
reifyTTConst (P _ n _) | n == reflm "IType" = return (AType (ATInt ITNative))
reifyTTConst (P _ n _) | n == reflm "BIType" = return (AType (ATInt ITBig))
reifyTTConst (P _ n _) | n == reflm "FlType" = return (AType ATFloat)
reifyTTConst (P _ n _) | n == reflm "ChType" = return (AType (ATInt ITChar))
reifyTTConst (P _ n _) | n == reflm "StrType" = return $ StrType
reifyTTConst (P _ n _) | n == reflm "B8Type" = return (AType (ATInt (ITFixed IT8)))
reifyTTConst (P _ n _) | n == reflm "B16Type" = return (AType (ATInt (ITFixed IT16)))
reifyTTConst (P _ n _) | n == reflm "B32Type" = return (AType (ATInt (ITFixed IT32)))
reifyTTConst (P _ n _) | n == reflm "B64Type" = return (AType (ATInt (ITFixed IT64)))
reifyTTConst (P _ n _) | n == reflm "PtrType" = return $ PtrType
reifyTTConst (P _ n _) | n == reflm "VoidType" = return $ VoidType
reifyTTConst (P _ n _) | n == reflm "Forgot" = return $ Forgot
reifyTTConst t@(App _ _)
| (P _ f _, [arg]) <- unApply t = reifyTTConstApp f arg
reifyTTConst t = fail ("Unknown reflection constant: " ++ show t)
reifyTTConstApp :: Name -> Term -> ElabD Const
reifyTTConstApp f (Constant c@(I _))
| f == reflm "I" = return $ c
reifyTTConstApp f (Constant c@(BI _))
| f == reflm "BI" = return $ c
reifyTTConstApp f (Constant c@(Fl _))
| f == reflm "Fl" = return $ c
reifyTTConstApp f (Constant c@(I _))
| f == reflm "Ch" = return $ c
reifyTTConstApp f (Constant c@(Str _))
| f == reflm "Str" = return $ c
reifyTTConstApp f (Constant c@(B8 _))
| f == reflm "B8" = return $ c
reifyTTConstApp f (Constant c@(B16 _))
| f == reflm "B16" = return $ c
reifyTTConstApp f (Constant c@(B32 _))
| f == reflm "B32" = return $ c
reifyTTConstApp f (Constant c@(B64 _))
| f == reflm "B64" = return $ c
reifyTTConstApp f arg = fail ("Unknown reflection constant: " ++ show (f, arg))
reifyTTUExp :: Term -> ElabD UExp
reifyTTUExp t@(App _ _)
= case unApply t of
(P _ f _, [Constant (I i)]) | f == reflm "UVar" -> return $ UVar i
(P _ f _, [Constant (I i)]) | f == reflm "UVal" -> return $ UVal i
_ -> fail ("Unknown reflection type universe expression: " ++ show t)
reifyTTUExp t = fail ("Unknown reflection type universe expression: " ++ show t)
-- | Create a reflected call to a named function/constructor
reflCall :: String -> [Raw] -> Raw
reflCall funName args
= raw_apply (Var (reflm funName)) args
-- | Lift a term into its Language.Reflection.TT representation
reflect :: Term -> Raw
reflect = reflectQuote []
claimTT :: Name -> ElabD Name
claimTT n = do n' <- getNameFrom n
claim n' (Var (sNS (sUN "TT") ["Reflection", "Language"]))
return n'
-- | Convert a reflected term to a more suitable form for pattern-matching.
-- In particular, the less-interesting bits are elaborated to _ patterns. This
-- happens to NameTypes, universe levels, names that are bound but not used,
-- and the type annotation field of the P constructor.
reflectQuotePattern :: [Name] -> Term -> ElabD ()
reflectQuotePattern unq (P _ n _)
| n `elem` unq = -- the unquoted names have been claimed as TT already - just use them
do fill (Var n) ; solve
| otherwise =
do tyannot <- claimTT (sMN 0 "pTyAnnot")
movelast tyannot -- use a _ pattern here
nt <- getNameFrom (sMN 0 "nt")
claim nt (Var (reflm "NameType"))
movelast nt -- use a _ pattern here
n' <- getNameFrom (sMN 0 "n")
claim n' (Var (reflm "TTName"))
fill $ reflCall "P" [Var nt, Var n', Var tyannot]
solve
focus n'; reflectNameQuotePattern n
reflectQuotePattern unq (V n)
= do fill $ reflCall "V" [RConstant (I n)]
solve
reflectQuotePattern unq (Bind n b x)
= do x' <- claimTT (sMN 0 "sc")
movelast x'
b' <- getNameFrom (sMN 0 "binder")
claim b' (RApp (Var (sNS (sUN "Binder") ["Reflection", "Language"]))
(Var (sNS (sUN "TT") ["Reflection", "Language"])))
if n `elem` freeNames x
then do fill $ reflCall "Bind"
[reflectName n,
Var b',
Var x']
solve
else do any <- getNameFrom (sMN 0 "anyName")
claim any (Var (reflm "TTName"))
movelast any
fill $ reflCall "Bind"
[Var any,
Var b',
Var x']
solve
focus x'; reflectQuotePattern unq x
focus b'; reflectBinderQuotePattern unq b
where
reflectBinderQuotePattern :: [Name] -> Binder Term -> ElabD ()
reflectBinderQuotePattern unq (Lam t)
= do t' <- claimTT (sMN 0 "ty"); movelast t'
fill $ reflCall "Lam" [Var (reflm "TT"), Var t']
solve
focus t'; reflectQuotePattern unq t
reflectBinderQuotePattern unq (Pi t)
= do t' <- claimTT (sMN 0 "ty") ; movelast t'
fill $ reflCall "Pi" [Var (reflm "TT"), Var t']
solve
focus t'; reflectQuotePattern unq t
reflectBinderQuotePattern unq (Let x y)
= do x' <- claimTT (sMN 0 "ty"); movelast x';
y' <- claimTT (sMN 0 "v"); movelast y';
fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']
solve
focus x'; reflectQuotePattern unq x
focus y'; reflectQuotePattern unq y
reflectBinderQuotePattern unq (NLet x y)
= do x' <- claimTT (sMN 0 "ty"); movelast x'
y' <- claimTT (sMN 0 "v"); movelast y'
fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']
solve
focus x'; reflectQuotePattern unq x
focus y'; reflectQuotePattern unq y
reflectBinderQuotePattern unq (Hole t)
= do t' <- claimTT (sMN 0 "ty"); movelast t'
fill $ reflCall "Hole" [Var (reflm "TT"), Var t']
solve
focus t'; reflectQuotePattern unq t
reflectBinderQuotePattern unq (GHole _ t)
= do t' <- claimTT (sMN 0 "ty"); movelast t'
fill $ reflCall "GHole" [Var (reflm "TT"), Var t']
solve
focus t'; reflectQuotePattern unq t
reflectBinderQuotePattern unq (Guess x y)
= do x' <- claimTT (sMN 0 "ty"); movelast x'
y' <- claimTT (sMN 0 "v"); movelast y'
fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']
solve
focus x'; reflectQuotePattern unq x
focus y'; reflectQuotePattern unq y
reflectBinderQuotePattern unq (PVar t)
= do t' <- claimTT (sMN 0 "ty"); movelast t'
fill $ reflCall "PVar" [Var (reflm "TT"), Var t']
solve
focus t'; reflectQuotePattern unq t
reflectBinderQuotePattern unq (PVTy t)
= do t' <- claimTT (sMN 0 "ty"); movelast t'
fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']
solve
focus t'; reflectQuotePattern unq t
reflectQuotePattern unq (App f x)
= do f' <- claimTT (sMN 0 "f"); movelast f'
x' <- claimTT (sMN 0 "x"); movelast x'
fill $ reflCall "App" [Var f', Var x']
solve
focus f'; reflectQuotePattern unq f
focus x'; reflectQuotePattern unq x
reflectQuotePattern unq (Constant c)
= do fill $ reflCall "TConst" [reflectConstant c]
solve
reflectQuotePattern unq (Proj t i)
= do t' <- claimTT (sMN 0 "t"); movelast t'
fill $ reflCall "Proj" [Var t', RConstant (I i)]
solve
focus t'; reflectQuotePattern unq t
reflectQuotePattern unq (Erased)
= do erased <- claimTT (sMN 0 "erased")
movelast erased
fill $ (Var erased)
solve
reflectQuotePattern unq (Impossible)
= do fill $ Var (reflm "Impossible")
solve
reflectQuotePattern unq (TType exp)
= do ue <- getNameFrom (sMN 0 "uexp")
claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))
movelast ue
fill $ reflCall "TType" [Var ue]
solve
-- | Create a reflected term, but leave refs to the provided name intact
reflectQuote :: [Name] -> Term -> Raw
reflectQuote unq (P nt n t)
| n `elem` unq = Var n
| otherwise = reflCall "P" [reflectNameType nt, reflectName n, reflectQuote unq t]
reflectQuote unq (V n)
= reflCall "V" [RConstant (I n)]
reflectQuote unq (Bind n b x)
= reflCall "Bind" [reflectName n, reflectBinderQuote unq b, reflectQuote unq x]
reflectQuote unq (App f x)
= reflCall "App" [reflectQuote unq f, reflectQuote unq x]
reflectQuote unq (Constant c)
= reflCall "TConst" [reflectConstant c]
reflectQuote unq (Proj t i)
= reflCall "Proj" [reflectQuote unq t, RConstant (I i)]
reflectQuote unq (Erased) = Var (reflm "Erased")
reflectQuote unq (Impossible) = Var (reflm "Impossible")
reflectQuote unq (TType exp) = reflCall "TType" [reflectUExp exp]
reflectNameType :: NameType -> Raw
reflectNameType (Bound) = Var (reflm "Bound")
reflectNameType (Ref) = Var (reflm "Ref")
reflectNameType (DCon x y)
= reflCall "DCon" [RConstant (I x), RConstant (I y)]
reflectNameType (TCon x y)
= reflCall "TCon" [RConstant (I x), RConstant (I y)]
reflectName :: Name -> Raw
reflectName (UN s)
= reflCall "UN" [RConstant (Str (str s))]
reflectName (NS n ns)
= reflCall "NS" [ reflectName n
, foldr (\ n s ->
raw_apply ( Var $ sNS (sUN "::") ["List", "Prelude"] )
[ RConstant StrType, RConstant (Str n), s ])
( raw_apply ( Var $ sNS (sUN "Nil") ["List", "Prelude"] )
[ RConstant StrType ])
(map str ns)
]
reflectName (MN i n)
= reflCall "MN" [RConstant (I i), RConstant (Str (str n))]
reflectName (NErased) = Var (reflm "NErased")
reflectName n = Var (reflm "NErased") -- special name, not yet implemented
-- | Elaborate a name to a pattern. This means that NS and UN will be intact,
-- while all others become _
reflectNameQuotePattern :: Name -> ElabD ()
reflectNameQuotePattern n@(UN s)
= do fill $ reflectName n
solve
reflectNameQuotePattern n@(NS _ _)
= do fill $ reflectName n
solve
reflectNameQuotePattern _ -- for all other names, match any
= do nameHole <- getNameFrom (sMN 0 "name")
claim nameHole (Var (reflm "TTName"))
movelast nameHole
fill (Var nameHole)
solve
reflectBinder :: Binder Term -> Raw
reflectBinder = reflectBinderQuote []
reflectBinderQuote :: [Name] -> Binder Term -> Raw
reflectBinderQuote unq (Lam t)
= reflCall "Lam" [Var (reflm "TT"), reflectQuote unq t]
reflectBinderQuote unq (Pi t)
= reflCall "Pi" [Var (reflm "TT"), reflectQuote unq t]
reflectBinderQuote unq (Let x y)
= reflCall "Let" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
reflectBinderQuote unq (NLet x y)
= reflCall "NLet" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
reflectBinderQuote unq (Hole t)
= reflCall "Hole" [Var (reflm "TT"), reflectQuote unq t]
reflectBinderQuote unq (GHole _ t)
= reflCall "GHole" [Var (reflm "TT"), reflectQuote unq t]
reflectBinderQuote unq (Guess x y)
= reflCall "Guess" [Var (reflm "TT"), reflectQuote unq x, reflectQuote unq y]
reflectBinderQuote unq (PVar t)
= reflCall "PVar" [Var (reflm "TT"), reflectQuote unq t]
reflectBinderQuote unq (PVTy t)
= reflCall "PVTy" [Var (reflm "TT"), reflectQuote unq t]
reflectConstant :: Const -> Raw
reflectConstant c@(I _) = reflCall "I" [RConstant c]
reflectConstant c@(BI _) = reflCall "BI" [RConstant c]
reflectConstant c@(Fl _) = reflCall "Fl" [RConstant c]
reflectConstant c@(Ch _) = reflCall "Ch" [RConstant c]
reflectConstant c@(Str _) = reflCall "Str" [RConstant c]
reflectConstant (AType (ATInt ITNative)) = Var (reflm "IType")
reflectConstant (AType (ATInt ITBig)) = Var (reflm "BIType")
reflectConstant (AType ATFloat) = Var (reflm "FlType")
reflectConstant (AType (ATInt ITChar)) = Var (reflm "ChType")
reflectConstant (StrType) = Var (reflm "StrType")
reflectConstant c@(B8 _) = reflCall "B8" [RConstant c]
reflectConstant c@(B16 _) = reflCall "B16" [RConstant c]
reflectConstant c@(B32 _) = reflCall "B32" [RConstant c]
reflectConstant c@(B64 _) = reflCall "B64" [RConstant c]
reflectConstant (AType (ATInt (ITFixed IT8))) = Var (reflm "B8Type")
reflectConstant (AType (ATInt (ITFixed IT16))) = Var (reflm "B16Type")
reflectConstant (AType (ATInt (ITFixed IT32))) = Var (reflm "B32Type")
reflectConstant (AType (ATInt (ITFixed IT64))) = Var (reflm "B64Type")
reflectConstant (PtrType) = Var (reflm "PtrType")
reflectConstant (VoidType) = Var (reflm "VoidType")
reflectConstant (Forgot) = Var (reflm "Forgot")
reflectUExp :: UExp -> Raw
reflectUExp (UVar i) = reflCall "UVar" [RConstant (I i)]
reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]
-- | Reflect the environment of a proof into a List (TTName, Binder TT)
reflectEnv :: Env -> Raw
reflectEnv = foldr consToEnvList emptyEnvList
where
consToEnvList :: (Name, Binder Term) -> Raw -> Raw
consToEnvList (n, b) l
= raw_apply (Var (sNS (sUN "::") ["List", "Prelude"]))
[ envTupleType
, raw_apply (Var pairCon) [ (Var $ reflm "TTName")
, (RApp (Var $ reflm "Binder")
(Var $ reflm "TT"))
, reflectName n
, reflectBinder b
]
, l
]
emptyEnvList :: Raw
emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))
[envTupleType]
-- | Reflect an error into the internal datatype of Idris -- TODO
rawBool :: Bool -> Raw
rawBool True = Var (sNS (sUN "True") ["Bool", "Prelude"])
rawBool False = Var (sNS (sUN "False") ["Bool", "Prelude"])
rawNil :: Raw -> Raw
rawNil ty = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"])) [ty]
rawCons :: Raw -> Raw -> Raw -> Raw
rawCons ty hd tl = raw_apply (Var (sNS (sUN "::") ["List", "Prelude"])) [ty, hd, tl]
rawList :: Raw -> [Raw] -> Raw
rawList ty = foldr (rawCons ty) (rawNil ty)
rawPairTy :: Raw -> Raw -> Raw
rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]
rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw
rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]
reflectCtxt :: [(Name, Type)] -> Raw
reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT"))
(map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")
(reflectName n, reflect t)))
ctxt)
reflectErr :: Err -> Raw
reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]
reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]
reflectErr (CantUnify b t1 t2 e ctxt i) =
raw_apply (Var $ reflErrName "CantUnify")
[ rawBool b
, reflect t1
, reflect t2
, reflectErr e
, reflectCtxt ctxt
, RConstant (I i)]
reflectErr (InfiniteUnify n tm ctxt) =
raw_apply (Var $ reflErrName "InfiniteUnify")
[ reflectName n
, reflect tm
, reflectCtxt ctxt
]
reflectErr (CantConvert t t' ctxt) =
raw_apply (Var $ reflErrName "CantConvert")
[ reflect t
, reflect t'
, reflectCtxt ctxt
]
reflectErr (CantSolveGoal t ctxt) =
raw_apply (Var $ reflErrName "CantSolveGoal")
[ reflect t
, reflectCtxt ctxt
]
reflectErr (UnifyScope n n' t ctxt) =
raw_apply (Var $ reflErrName "UnifyScope")
[ reflectName n
, reflectName n'
, reflect t
, reflectCtxt ctxt
]
reflectErr (CantInferType str) =
raw_apply (Var $ reflErrName "CantInferType") [RConstant (Str str)]
reflectErr (NonFunctionType t t') =
raw_apply (Var $ reflErrName "NonFunctionType") [reflect t, reflect t']
reflectErr (NotEquality t t') =
raw_apply (Var $ reflErrName "NotEquality") [reflect t, reflect t']
reflectErr (TooManyArguments n) = raw_apply (Var $ reflErrName "TooManyArguments") [reflectName n]
reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t]
reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n]
reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]
reflectErr (NotInjective t1 t2 t3) =
raw_apply (Var $ reflErrName "NotInjective")
[ reflect t1
, reflect t2
, reflect t3
]
reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]
reflectErr (CantResolveAlts ss) =
raw_apply (Var $ reflErrName "CantResolveAlts")
[rawList (Var $ (sUN "String")) (map Var ss)]
reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]
reflectErr UniverseError = Var $ reflErrName "UniverseError"
reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"
reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]
reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]
reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]
reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]
reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]
reflectErr (ProviderError str) =
raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]
reflectErr (LoadingFailed str err) =
raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
elaboratingArgErr :: [(Name, Name)] -> Err -> Err
elaboratingArgErr [] err = err
elaboratingArgErr ((f,x):during) err = fromMaybe err (rewrite err)
where rewrite (ElaboratingArg _ _ _ _) = Nothing
rewrite (ProofSearchFail e) = fmap ProofSearchFail (rewrite e)
rewrite (At fc e) = fmap (At fc) (rewrite e)
rewrite err = Just (ElaboratingArg f x during err)
withErrorReflection :: Idris a -> Idris a
withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
where handle :: Err -> Idris Err
handle e@(ReflectionError _ _) = do logLvl 3 "Skipping reflection of error reflection result"
return e -- Don't do meta-reflection of errors
handle e@(ReflectionFailed _ _) = do logLvl 3 "Skipping reflection of reflection failure"
return e
-- At and Elaborating are just plumbing - error reflection shouldn't rewrite them
handle e@(At fc err) = do logLvl 3 "Reflecting body of At"
err' <- handle err
return (At fc err')
handle e@(Elaborating what n err) = do logLvl 3 "Reflecting body of Elaborating"
err' <- handle err
return (Elaborating what n err')
handle e@(ElaboratingArg f a prev err) = do logLvl 3 "Reflecting body of ElaboratingArg"
hs <- getFnHandlers f a
err' <- if null hs
then handle err
else applyHandlers err hs
return (ElaboratingArg f a prev err')
-- ProofSearchFail is an internal detail - so don't expose it
handle (ProofSearchFail e) = handle e
-- TODO: argument-specific error handlers go here for ElaboratingArg
handle e = do ist <- getIState
logLvl 2 "Starting error reflection"
let handlers = idris_errorhandlers ist
applyHandlers e handlers
getFnHandlers :: Name -> Name -> Idris [Name]
getFnHandlers f arg = do ist <- getIState
let funHandlers = maybe M.empty id .
lookupCtxtExact f .
idris_function_errorhandlers $ ist
return . maybe [] S.toList . M.lookup arg $ funHandlers
applyHandlers e handlers =
do ist <- getIState
let err = fmap (errReverse ist) e
logLvl 3 $ "Using reflection handlers " ++
concat (intersperse ", " (map show handlers))
let reports = map (\n -> RApp (Var n) (reflectErr err)) handlers
-- Typecheck error handlers - if this fails, then something else was wrong earlier!
handlers <- case mapM (check (tt_ctxt ist) []) reports of
Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e
OK hs -> return hs
-- Normalize error handler terms to produce the new messages
ctxt <- getContext
let results = map (normalise ctxt []) (map fst handlers)
logLvl 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))
-- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent
let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)
errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of
Left err -> ierror err
Right ok -> return ok
return $ case errorparts of
[] -> e
parts -> ReflectionError errorparts e
fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a
fromTTMaybe (App (App (P (DCon _ _) (NS (UN just) _) _) ty) tm)
| just == txt "Just" = Just tm
fromTTMaybe x = Nothing
reflErrName :: String -> Name
reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]
-- | Attempt to reify a report part from TT to the internal
-- representation. Not in Idris or ElabD monads because it should be usable
-- from either.
reifyReportPart :: Term -> Either Err ErrorReportPart
reifyReportPart (App (P (DCon _ _) n _) (Constant (Str msg))) | n == reflErrName "TextPart" =
Right (TextPart msg)
reifyReportPart (App (P (DCon _ _) n _) ttn)
| n == reflErrName "NamePart" =
case runElab [] (reifyTTName ttn) (initElaborator NErased initContext Erased) of
Error e -> Left . InternalMsg $
"could not reify name term " ++
show ttn ++
" when reflecting an error:" ++ show e
OK (n', _)-> Right $ NamePart n'
reifyReportPart (App (P (DCon _ _) n _) tm)
| n == reflErrName "TermPart" =
case runElab [] (reifyTT tm) (initElaborator NErased initContext Erased) of
Error e -> Left . InternalMsg $
"could not reify reflected term " ++
show tm ++
" when reflecting an error:" ++ show e
OK (tm', _) -> Right $ TermPart tm'
reifyReportPart (App (P (DCon _ _) n _) tm)
| n == reflErrName "SubReport" =
case unList tm of
Just xs -> do subParts <- mapM reifyReportPart xs
Right (SubReport subParts)
Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm
reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x
envTupleType :: Raw
envTupleType
= raw_apply (Var pairTy) [ (Var $ reflm "TTName")
, (RApp (Var $ reflm "Binder") (Var $ reflm "TT"))
]
solveAll = try (do solve; solveAll) (return ())