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 Idris.Elab.Utils
import qualified Util.Pretty as U
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 Data.Vector.Unboxed (Vector)
import qualified Data.Vector.Unboxed as V
import Debug.Trace
data ElabMode = ETyDecl | ELHS | ERHS
deriving Eq
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
when (not pattern) $ solveAutos ist fn True
hs <- get_holes
ivs <- get_instances
ptm <- get_term
when (not pattern) $
mapM_ (\n -> when (n `elem` hs) $
do focus n
g <- goal
try (resolveTC True 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 True 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)
EState 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 ()
buildTC :: IState -> ElabInfo -> ElabMode -> FnOpts -> Name -> PTerm ->
ElabD (Term, [(Name, (Int, Maybe Name, Type))], [PDecl])
buildTC ist info emode opts fn tm
= do
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)
dots <- get_dotterm
when (not (null dots)) $
lift (Error (CantMatch (getInferTerm tm)))
EState 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
getUnmatchable :: Context -> Name -> [Bool]
getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon
= case lookupTyExact n ctxt of
Nothing -> []
Just ty -> checkArgs [] [] ty
where checkArgs :: [Name] -> [[Name]] -> Type -> [Bool]
checkArgs env ns (Bind n (Pi _ t _) sc)
= let env' = case t of
TType _ -> n : env
_ -> env in
checkArgs env' (intersect env (refsIn t) : ns)
(instantiate (P Bound n t) sc)
checkArgs env ns t
= map (not . null) (reverse ns)
getUnmatchable ctxt n = []
data ElabCtxt = ElabCtxt { e_inarg :: Bool,
e_guarded :: Bool,
e_intype :: Bool,
e_qq :: Bool,
e_nomatching :: Bool
}
initElabCtxt = ElabCtxt False False False False False
goal_polymorphic :: ElabD Bool
goal_polymorphic =
do ty <- goal
case ty of
P _ n _ -> do env <- get_env
case lookup n env of
Nothing -> return False
_ -> return True
_ -> return False
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
let fc = maybe "(unknown)"
elabE initElabCtxt (elabFC info) tm
est <- getAux
sequence_ (delayed_elab est)
end_unify
ptm <- get_term
when pattern
(do update_term orderPats
unify_all
matchProblems False
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 (elabFC info) v)
toElab' ina arg = case getTm arg of
Placeholder -> Nothing
v -> Just (elabE ina (elabFC info) v)
mkPat = do hs <- get_holes
tm <- get_term
case hs of
(h: hs) -> do patvar h; mkPat
[] -> return ()
elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()
elabE ina fc' t =
do solved <- get_recents
as <- get_autos
mapM_ (\(a, ns) -> if any (\n -> n `elem` solved) ns
then solveAuto ist fn False a
else return ()) as
itm <- if not pattern then insertImpLam t else return t
ct <- insertCoerce ina itm
t' <- insertLazy ct
g <- goal
tm <- get_term
ps <- get_probs
hs <- get_holes
let fc = fileFC "Force"
env <- get_env
handleError (forceErr env)
(elab' ina fc' t')
(elab' ina fc' (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)
constType :: Const -> Bool
constType (AType _) = True
constType StrType = True
constType PtrType = True
constType VoidType = True
constType _ = False
elab' :: ElabCtxt
-> Maybe FC
-> PTerm
-> ElabD ()
elab' ina fc (PNoImplicits t) = elab' ina fc t
elab' ina fc PType = do apply RType []; solve
elab' ina fc (PUniverse u) = do apply (RUType u) []; solve
elab' ina fc tm@(PConstant c)
| pattern && not reflection && not (e_qq ina) && not (e_intype ina)
&& isTypeConst c
= lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
| pattern && not reflection && e_nomatching ina
= lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
| otherwise = do apply (RConstant c) []; solve
elab' ina fc (PQuote r) = do fill r; solve
elab' ina _ (PTrue fc _) =
do hnf_compute
g <- goal
case g of
TType _ -> elab' ina (Just fc) (PRef fc unitTy)
_ -> elab' ina (Just fc) (PRef fc unitCon)
elab' ina fc (PResolveTC (FC "HACK" _ _))
= do g <- goal; resolveTC False 5 g fn ist
elab' ina fc (PResolveTC fc')
= do c <- getNameFrom (sMN 0 "class")
instanceArg c
elab' ina _ (PRefl fc t)
= elab' ina (Just fc) (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 (Just fc) (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 (Just fc) (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 (Just fc) (PApp fc (PRef fc eqTy)
[pimp (sUN "A") lt True,
pimp (sUN "B") rt False,
pexp l, pexp r])
elab' ina _ (PPair fc _ l r)
= do hnf_compute
g <- goal
case g of
TType _ -> elab' ina (Just fc) (PApp fc (PRef fc pairTy)
[pexp l,pexp r])
_ -> elab' ina (Just fc) (PApp fc (PRef fc pairCon)
[pimp (sUN "A") Placeholder False,
pimp (sUN "B") Placeholder False,
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 (Just fc) (PApp fc (PRef fc sigmaTy)
[pexp t,
pexp (PLam fc n Placeholder r)])
asValue = elab' ina (Just fc) (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 (Just fc) (PApp fc (PRef fc existsCon)
[pimp (sMN 0 "a") t False,
pimp (sMN 0 "P") Placeholder True,
pexp l, pexp r])
elab' ina fc (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
tryAll (zip (map (elab' ina fc) as') (map showHd as'))
where showHd (PApp _ (PRef _ n) _) = n
showHd (PRef _ n) = n
showHd (PApp _ h _) = showHd h
showHd x = NErased
elab' ina fc (PAlternative False as)
= trySeq as
where
trySeq (x : xs) = let e1 = elab' ina fc x in
try' e1 (trySeq' e1 xs) True
trySeq' deferr [] = proofFail deferr
trySeq' deferr (x : xs)
= try' (do elab' ina fc x
solveAutos ist fn False) (trySeq' deferr xs) True
elab' ina _ (PPatvar fc n) | bindfree = do patvar n; update_term liftPats
elab' ec _ tm@(PRef fc n)
| pattern && not reflection && not (e_qq ec) && not (e_intype ec)
&& isTConName n (tt_ctxt ist)
= lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
| pattern && not reflection && e_nomatching ec
= lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
| (pattern || (bindfree && bindable n)) && not (inparamBlock n) && not (e_qq ec)
= do let ina = e_inarg ec
guarded = e_guarded ec
inty = e_intype ec
ctxt <- get_context
let defined = case lookupTy n ctxt of
[] -> False
_ -> True
if (tcname n && ina) then erun fc $ do patvar n;
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 (Just fc) (PApp fc f [])
elab' ina fc' tm@(PRef fc n)
| pattern && not reflection && not (e_qq ina) && not (e_intype ina)
&& isTConName n (tt_ctxt ist)
= lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
| pattern && not reflection && e_nomatching ina
= lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
| otherwise =
do fty <- get_type (Var n)
ctxt <- get_context
env <- get_env
let a' = insertScopedImps fc (normalise ctxt env fty) []
if null a'
then erun fc $ do apply (Var n) []; solve
else elab' ina fc' (PApp fc tm [])
elab' ina _ (PLam fc n Placeholder sc)
= do
ctxt <- get_context
when (isTConName n ctxt) $
lift $ tfail (Msg $ "Can't use type constructor " ++ show n ++ " here")
checkPiGoal n
attack; intro (Just n);
elabE (ina { e_inarg = True } ) (Just fc) sc; solve
elab' ec _ (PLam fc n ty sc)
= do tyn <- getNameFrom (sMN 0 "lamty")
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 (ec { e_inarg = True, e_intype = True }) (Just fc) ty
elabE (ec { e_inarg = True }) (Just fc) sc
solve
elab' ina fc (PPi p n Placeholder sc)
= do attack; arg n (is_scoped p) (sMN 0 "ty")
elabE (ina { e_inarg = True, e_intype = True }) fc sc
solve
elab' ina fc (PPi p 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' (is_scoped p) (Var tyn)
focus tyn
let ec' = ina { e_inarg = True, e_intype = True }
elabE ec' fc ty
elabE ec' fc sc
solve
elab' ina _ (PLet fc 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 (ina { e_inarg = True, e_intype = True })
(Just fc) ty
focus valn
elabE (ina { e_inarg = True, e_intype = True })
(Just fc) val
ivs' <- get_instances
env <- get_env
elabE (ina { e_inarg = True }) (Just fc) sc
when (not pattern) $
mapM_ (\n -> do focus n
g <- goal
hs <- get_holes
if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)
then try (resolveTC True 7 g fn ist)
(movelast n)
else movelast n)
(ivs' \\ ivs)
expandLet n (case lookup n env of
Just (Let t v) -> v)
solve
elab' ina _ (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 (ina { e_inarg = True, e_intype = True }) (Just fc) (PApp fc r [pexp (delab ist rty)])
env <- get_env
computeLet n
elabE (ina { e_inarg = True }) (Just fc) sc
solve
elab' ina _ tm@(PApp fc (PInferRef _ f) args) = do
rty <- goal
ds <- get_deferred
ctxt <- get_context
env <- get_env
argTys <- claimArgTys env args
fn <- getNameFrom (sMN 0 "inf_fn")
let fty = fnTy argTys rty
attack; deferType (mkN f) fty (map fst argTys); solve
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 Nothing xt RType) (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 (Just fc) (getTm def)
elabIArg _ = return ()
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' ina _ tm@(PApp fc (PRef _ f) args_in)
| pattern && not reflection && e_nomatching ina
= lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)
| otherwise
= do env <- get_env
ty <- goal
fty <- get_type (Var f)
ctxt <- get_context
let args = insertScopedImps fc (normalise ctxt env fty) args_in
let unmatchableArgs = if pattern
then getUnmatchable (tt_ctxt ist) f
else []
when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)
&& isTConName f (tt_ctxt ist)) $
lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)
if (f `elem` map fst env && length args == 1 && length args_in == 1)
then
do simple_app (elabE ina (Just fc) (PRef fc f))
(elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))
(show tm)
solve
else
do ivs <- get_instances
ps <- get_probs
let isinf = f == inferCon || tcname f
case lookupCtxt f (idris_classes ist) of
[] -> return ()
_ -> do mapM_ setInjective (map getTm args)
unifyProblems
let guarded = isConName f ctxt
ns <- apply (Var f) (map isph args)
mapM_ checkIfInjective (map snd ns)
unifyProblems
let (ns', eargs) = unzip $
sortBy cmpArg (zip ns args)
ulog <- getUnifyLog
elabArgs ist (ina { e_inarg = e_inarg ina || not isinf })
[] fc False f
(zip ns' (unmatchableArgs ++ repeat False))
(f == sUN "Force")
(map (\x -> getTm x) eargs)
solve
ivs' <- get_instances
when (not pattern || (e_inarg ina && not tcgen &&
not (e_guarded ina))) $
mapM_ (\n -> do focus n
g <- goal
env <- get_env
hs <- get_holes
if all (\n -> not (n `elem` hs)) (freeNames g)
then try (resolveTC False 7 g fn ist)
(movelast n)
else movelast n)
(ivs' \\ ivs)
where
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
PHidden _ -> 150
_ -> 1
constraint (PConstraint _ _ _ _) = True
constraint _ = False
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 (PHidden _) = 150
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 ()
_ ->
do mapM_ setinjArg args
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 _ tm@(PApp fc f [arg])
= erun fc $
do simple_app (elabE ina (Just fc) f) (elabE (ina { e_inarg = True }) (Just fc) (getTm arg))
(show tm)
solve
elab' ina fc Placeholder
= do (h : hs) <- get_holes
movelast h
elab' ina fc (PMetavar n) =
do ptm <- get_term
let unique_used = getUniqueUsed (tt_ctxt ist) ptm
let n' = mkN n
attack
defer unique_used n'
solve
where mkN n@(NS _ _) = n
mkN n = case namespace info of
Just xs@(_:_) -> sNS n xs
_ -> n
elab' ina fc (PProof ts) = do compute; mapM_ (runTac True ist (elabFC info) fn) ts
elab' ina fc (PTactics ts)
| not pattern = do mapM_ (runTac False ist fc fn) ts
| otherwise = elab' ina fc Placeholder
elab' ina fc (PElabError e) = lift $ tfail 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 (Just fc) r
compute
g <- goal
rewrite (Var letn)
g' <- goal
when (g == g') $ lift $ tfail (NoRewriting g)
case newg of
Nothing -> elab' ina (Just fc) 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 (Just fc) t
focus valn
elab' ina (Just fc) sc
elab' ina (Just fc) (PRef fc letn)
solve
elab' ina _ 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 (ina { e_inarg = True }) (Just fc) scr
unifyProblems
matchProblems True
args <- get_env
envU <- mapM (getKind args) args
let namesUsedInRHS = nub $ scvn : concatMap (\(_,rhs) -> allNamesIn rhs) opts
let argsDropped = filter (isUnique envU) (nub $ allNamesIn scr)
let args' = filter (\(n, _) -> n `notElem` argsDropped) args
cname <- unique_hole' True (mkCaseName fn)
let cname' = mkN cname
attack; defer argsDropped cname'; solve
let newdef = PClauses fc [] cname'
(caseBlock fc cname'
(map (isScr scr) (reverse args')) opts)
updateAux (\e -> e { case_decls = newdef : case_decls e } )
movelast tyn
solve
where mkCaseName (NS n ns) = NS (mkCaseName n) ns
mkCaseName n = SN (CaseN n)
mkN n@(NS _ _) = n
mkN n = case namespace info of
Just xs@(_:_) -> sNS n xs
_ -> n
isUnique envk n = case lookup n envk of
Just u -> u
_ -> False
getKind env (n, _)
= case lookup n env of
Nothing -> return (n, False)
Just b ->
do ty <- get_type (forget (binderTy b))
case ty of
UType UniqueType -> return (n, True)
UType AllTypes -> return (n, True)
_ -> return (n, False)
tcName tm | (P _ n _, _) <- unApply tm
= case lookupCtxt n (idris_classes ist) of
[_] -> True
_ -> False
tcName _ = False
usedIn ns (n, b)
= n `elem` ns
|| any (\x -> x `elem` ns) (allTTNames (binderTy b))
elab' ina fc (PUnifyLog t) = do unifyLog True
elab' ina fc t
unifyLog False
elab' ina fc (PQuasiquote t goal)
= do
(t, unq) <- extractUnquotes 0 t
let unquoteNames = map fst unq
mapM_ (flip claim (Var tt)) unquoteNames
ctxt <- get_context
saveState
updatePS (const .
newProof (sMN 0 "q") ctxt $
P Ref tt Erased)
mapM_ (\n -> do ty <- getNameFrom (sMN 0 "unqTy")
claim ty RType
movelast ty
claim n (Var ty)
movelast n)
unquoteNames
qTy <- getNameFrom (sMN 0 "qquoteTy")
claim qTy RType
movelast qTy
qTm <- getNameFrom (sMN 0 "qquoteTm")
claim qTm (Var qTy)
nTm <- getNameFrom (sMN 0 "quotedTerm")
letbind nTm (Var qTy) (Var qTm)
case goal of
Nothing -> return ()
Just gTy -> do focus qTy
elabE (ina { e_qq = True }) fc gTy
focus qTm
elabE (ina { e_qq = True }) fc t
end_unify
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"
mapM_ elabUnquote unq
where tt = sNS (sUN "TT") ["Reflection", "Language"]
elabUnquote (n, tm)
= do focus n
elabE (ina { e_qq = False }) fc tm
elab' ina fc (PUnquote t) = fail "Found unquote outside of quasiquote"
elab' ina fc (PAs _ n t) = lift . tfail . Msg $ "@-pattern not allowed here"
elab' ina fc (PHidden t)
| reflection = elab' ina fc t
| otherwise
= do (h : hs) <- get_holes
movelast h
delayElab $ do focus h
dotterm
elab' ina fc t
elab' ina fc x = fail $ "Unelaboratable syntactic form " ++ showTmImpls x
delayElab t = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [t] })
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
findScr ((n, (True, t)) : xs)
= (n, (True, t)) : scrName n xs
findScr [(n, (_, t))] = [(n, (True, t))]
findScr (x : xs) = x : findScr xs
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)
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])
notImplicitable (PApp _ f _) = notImplicitable f
notImplicitable (PRef _ n)
| [opts] <- lookupCtxt n (idris_flags ist)
= NoImplicit `elem` opts
notImplicitable (PAlternative True as) = any notImplicitable as
notImplicitable (PCase _ _ _) = True
notImplicitable _ = False
insertScopedImps fc (Bind n (Pi im@(Just i) _ _) sc) xs
| tcinstance i
= pimp n (PResolveTC fc) True : insertScopedImps fc sc xs
| otherwise
= pimp n Placeholder True : insertScopedImps fc sc xs
insertScopedImps fc (Bind n (Pi _ _ _) sc) (x : xs)
= x : insertScopedImps fc sc xs
insertScopedImps _ _ xs = xs
insertImpLam t =
do ty <- goal
env <- get_env
let ty' = normalise (tt_ctxt ist) env ty
addLam ty' t
where
addLam (Bind n (Pi (Just _) _ _) sc) t
= do impn <- unique_hole (sMN 0 "imp")
return (PLam emptyFC impn Placeholder t)
addLam _ t = return t
insertCoerce ina t@(PCase _ _ _) = return t
insertCoerce ina t | notImplicitable t = return t
insertCoerce ina t =
do ty <- goal
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
addImplBound ist (map fst env)
(PApp fc (PRef fc n) [pexp (PCoerced t)])
elabArgs :: IState
-> ElabCtxt
-> [Bool]
-> FC
-> Bool
-> Name
-> [((Name, Name), Bool)]
-> Bool
-> [PTerm]
-> ElabD ()
elabArgs ist ina failed fc retry f [] force _ = return ()
elabArgs ist ina failed fc r f (((argName, holeName), unm):ns) force (t : args)
= do hs <- get_holes
if holeName `elem` hs then
do focus holeName
case t of
Placeholder -> do movelast holeName
elabArgs ist ina failed fc r f ns force args
_ -> elabArg t
else elabArgs ist ina failed fc r f ns force args
where elabArg t =
do
now_elaborating fc f argName
wrapErr f argName $ do
hs <- get_holes
tm <- get_term
let elab = if force then elab' else elabE
failed' <-
do focus holeName;
g <- goal
poly <- goal_polymorphic
ulog <- getUnifyLog
traceWhen ulog ("Elaborating argument " ++ show (argName, holeName, g)) $
elab (ina { e_nomatching = unm && poly }) (Just fc) t
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
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
pruneByType :: [Name] -> Term ->
Context -> [PTerm] -> [PTerm]
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 (PHidden t) = getName t
getName _ = Nothing
pruneByType env (P _ n _) ctxt as
| [] <- lookupTy n ctxt = 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 var f (PHidden t) = headIs var f t
headIs _ _ _ = True
typeHead var f f'
=
case lookupTy f' ctxt of
[ty] -> case unApply (getRetTy ty) of
(P _ ctyn _, _) | isConName ctyn ctxt -> ctyn == f
_ -> let ty' = normalise ctxt [] ty in
case unApply (getRetTy ty') of
(P _ ftyn _, _) -> ftyn == f
(V _, _) -> var
_ -> 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 = []
solveAuto :: IState -> Name -> Bool -> Name -> ElabD ()
solveAuto ist fn ambigok n
= do hs <- get_holes
when (n `elem` hs) $ do
focus n
g <- goal
isg <- is_guess
when (not isg) $
proofSearch' ist True ambigok 100 True Nothing fn []
solveAutos :: IState -> Name -> Bool -> ElabD ()
solveAutos ist fn ambigok
= do autos <- get_autos
mapM_ (solveAuto ist fn ambigok) (map fst autos)
trivial' ist
= trivial (elab ist toplevel ERHS [] (sMN 0 "tac")) ist
proofSearch' ist rec ambigok depth prv top n hints
= do unifyProblems
proofSearch rec prv ambigok (not prv) depth
(elab ist toplevel ERHS [] (sMN 0 "tac")) top n hints ist
resolveTC :: Bool -> Int -> Term -> Name -> IState -> ElabD ()
resolveTC = resTC' []
resTC' tcs def 0 topg fn ist = fail $ "Can't resolve type class"
resTC' tcs def 1 topg fn ist = try' (trivial' ist) (resolveTC def 0 topg fn ist) True
resTC' tcs defaultOn depth topg fn ist
= do 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 stk = elab_stack ist
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' stk (stk ++ insts)) True
where
elabTC n | n /= fn && tcname n = (resolve n depth, show n)
| otherwise = (fail "Can't resolve", show n)
chaser (UN nm)
| ('@':'@':_) <- str nm = True
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 && defaultOn
= do focus a
fill (RConstant (AType (ATInt ITBig)))
solve
return False
needsDefault t f as
| all boundVar as = return True
needsDefault t f a = return False
boundVar (P Bound _ _) = True
boundVar _ = False
blunderbuss t d stk [] = do
lift $ tfail $ CantResolve topg
blunderbuss t d stk (n:ns)
| n /= fn && (n `elem` stk || tcname n)
= try' (resolve n d) (blunderbuss t d stk ns) True
| otherwise = blunderbuss t d stk ns
resolve n depth
| depth == 0 = fail $ "Can't resolve type class"
| otherwise
= do t <- goal
let (tc, ttypes) = unApply t
let imps = case lookupCtxtName n (idris_implicits ist) of
[] -> []
[args] -> map isImp (snd args)
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"
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) defaultOn depth' topg fn ist)
(filter (\ (x, y) -> not x) (zip (map fst imps) args))
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
runTac :: Bool -> IState -> Maybe FC -> Name -> PTactic -> ElabD ()
runTac autoSolve ist perhapsFC 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)
= 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)
= 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 ist toplevel ERHS [] (sMN 0 "tac") tm
rewrite (Var letn)
when autoSolve solveAll
runT (Induction tm)
= 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 False 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
tgoal <- goal
attack
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)
restac <- getNameFrom (sMN 0 "restac")
claim restac tacticTy
focus restac
fill (raw_apply (forget script')
[reflectEnv tenv, reflect tgoal])
restac' <- get_guess
solve
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 Nothing (RApp listTy envTupleType) RType)
(RBind (sMN 1 "__pi_arg")
(Pi Nothing (Var $ reflm "TT") RType) tacticTy))
runT (ByReflection tm)
= 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)
restac <- getNameFrom (sMN 0 "restac")
claim restac tacticTy
focus restac
fill (forget script')
restac' <- get_guess
solve
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
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 perhapsFC fn (Exact $ PQuote (reflect value'))
runT (Fill v) = do attack
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 perhapsFC 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 Skip = return ()
runT (TFail err) = lift . tfail $ ReflectionError [err] (Msg "")
runT SourceFC =
case perhapsFC of
Nothing -> lift . tfail $ Msg "There is no source location available."
Just fc ->
do let intTy = RConstant (AType (ATInt ITNative))
fill $ raw_apply (Var (reflm "FileLoc"))
[ RConstant (Str (fc_fname fc))
, raw_apply (Var pairCon) $
[intTy, intTy] ++
map (RConstant . I)
[ fst (fc_start fc)
, snd (fc_start fc)
]
, raw_apply (Var pairCon) $
[intTy, intTy] ++
map (RConstant . I)
[ fst (fc_end fc)
, snd (fc_end fc)
]
]
solve
runT x = fail $ "Not implemented " ++ show x
runReflected t = do t' <- reify ist t
runTac autoSolve ist perhapsFC fn t'
reflm :: String -> Name
reflm n = sNS (sUN n) ["Reflection", "Language"]
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 _ (P _ n _) | n == reflm "Skip" = return Skip
reify _ (P _ n _) | n == reflm "SourceFC" = return SourceFC
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 ist t [errs]
| t == reflm "Fail" = case unList errs of
Nothing -> fail "Failed to reify errors"
Just errs' ->
let parts = mapM reifyReportPart errs' in
case parts of
Left err -> fail $ "Couldn't reify \"Fail\" tactic - " ++ show err
Right errs'' ->
return $ TFail errs''
reifyApp _ f args = fail ("Unknown tactic " ++ show (f, args))
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))
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 False
| 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, k]
| f == reflm "Pi" = liftM2 (Pi Nothing) (reif t) (reif k)
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 "StrType" = return $ StrType
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 aty
| f == reflm "AType" = fmap AType (reifyArithTy aty)
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))
reifyArithTy :: Term -> ElabD ArithTy
reifyArithTy (App (P _ n _) intTy) | n == reflm "ATInt" = fmap ATInt (reifyIntTy intTy)
reifyArithTy (P _ n _) | n == reflm "ATFloat" = return ATFloat
reifyArithTy x = fail ("Couldn't reify reflected ArithTy: " ++ show x)
reifyNativeTy :: Term -> ElabD NativeTy
reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
reifyNativeTy (P _ n _) | n == reflm "IT8" = return IT8
reifyNativeTy x = fail $ "Couldn't reify reflected NativeTy " ++ show x
reifyIntTy :: Term -> ElabD IntTy
reifyIntTy (App (P _ n _) nt) | n == reflm "ITFixed" = fmap ITFixed (reifyNativeTy nt)
reifyIntTy (P _ n _) | n == reflm "ITNative" = return ITNative
reifyIntTy (P _ n _) | n == reflm "ITBig" = return ITBig
reifyIntTy (P _ n _) | n == reflm "ITChar" = return ITChar
reifyIntTy (App (App (P _ n _) nt) (Constant (I i))) | n == reflm "ITVec" = fmap (flip ITVec i)
(reifyNativeTy nt)
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)
reflCall :: String -> [Raw] -> Raw
reflCall funName args
= raw_apply (Var (reflm funName)) args
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'
reflectQuotePattern :: [Name] -> Term -> ElabD ()
reflectQuotePattern unq (P _ n _)
| n `elem` unq =
do fill (Var n) ; solve
| otherwise =
do tyannot <- claimTT (sMN 0 "pTyAnnot")
movelast tyannot
nt <- getNameFrom (sMN 0 "nt")
claim nt (Var (reflm "NameType"))
movelast nt
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 k)
= do t' <- claimTT (sMN 0 "ty") ; movelast t'
k' <- claimTT (sMN 0 "k"); movelast k';
fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']
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
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")
reflectNameQuotePattern :: Name -> ElabD ()
reflectNameQuotePattern n@(UN s)
= do fill $ reflectName n
solve
reflectNameQuotePattern n@(NS _ _)
= do fill $ reflectName n
solve
reflectNameQuotePattern (MN _ n)
= do i <- getNameFrom (sMN 0 "mnCounter")
claim i (RConstant (AType (ATInt ITNative)))
movelast i
fill $ reflCall "MN" [Var i, RConstant (Str $ T.unpack n)]
solve
reflectNameQuotePattern _
= 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 k)
= reflCall "Pi" [Var (reflm "TT"), reflectQuote unq t, reflectQuote unq k]
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]
mkList :: Raw -> [Raw] -> Raw
mkList ty [] = RApp (Var (sNS (sUN "Nil") ["List", "Prelude"])) ty
mkList ty (x:xs) = RApp (RApp (RApp (Var (sNS (sUN "::") ["List", "Prelude"])) ty)
x)
(mkList ty xs)
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 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 (B8V ws) = reflCall "B8V" [mkList (Var (sUN "Bits8")) . map (RConstant . B8) . V.toList $ ws]
reflectConstant (B16V ws) = reflCall "B8V" [mkList (Var (sUN "Bits16")) . map (RConstant . B16) . V.toList $ ws]
reflectConstant (B32V ws) = reflCall "B8V" [mkList (Var (sUN "Bits32")) . map (RConstant . B32) . V.toList $ ws]
reflectConstant (B64V ws) = reflCall "B8V" [mkList (Var (sUN "Bits64")) . map (RConstant . B64) . V.toList $ ws]
reflectConstant (AType (ATInt ITNative)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITNative")]]
reflectConstant (AType (ATInt ITBig)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITBig")]]
reflectConstant (AType ATFloat) = reflCall "AType" [Var (reflm "ATFloat")]
reflectConstant (AType (ATInt ITChar)) = reflCall "AType" [reflCall "ATInt" [Var (reflm "ITChar")]]
reflectConstant StrType = Var (reflm "StrType")
reflectConstant (AType (ATInt (ITFixed IT8))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT8")]]]
reflectConstant (AType (ATInt (ITFixed IT16))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT16")]]]
reflectConstant (AType (ATInt (ITFixed IT32))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT32")]]]
reflectConstant (AType (ATInt (ITFixed IT64))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITFixed" [Var (reflm "IT64")]]]
reflectConstant (AType (ATInt (ITVec IT8 c))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITVec" [Var (reflm "IT8"), RConstant (I c)]]]
reflectConstant (AType (ATInt (ITVec IT16 c))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITVec" [Var (reflm "IT16"), RConstant (I c)]]]
reflectConstant (AType (ATInt (ITVec IT32 c))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITVec" [Var (reflm "IT32"), RConstant (I c)]]]
reflectConstant (AType (ATInt (ITVec IT64 c))) = reflCall "AType" [reflCall "ATInt" [reflCall "ITVec" [Var (reflm "IT64"), RConstant (I c)]]]
reflectConstant PtrType = Var (reflm "PtrType")
reflectConstant ManagedPtrType = Var (reflm "ManagedPtrType")
reflectConstant BufferType = Var (reflm "BufferType")
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)]
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]
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 (WithFnType t) = raw_apply (Var $ reflErrName "WithFnType") [reflect t]
reflectErr (CantMatch t) = raw_apply (Var $ reflErrName "CantMatch") [reflect t]
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
handle e@(ReflectionFailed _ _) = do logLvl 3 "Skipping reflection of reflection failure"
return e
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')
handle (ProofSearchFail e) = handle e
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
handlers <- case mapM (check (tt_ctxt ist) []) reports of
Error e -> ierror $ ReflectionFailed "Type error while constructing reflected error" e
OK hs -> return hs
ctxt <- getContext
let results = map (normalise ctxt []) (map fst handlers)
logLvl 3 $ "New error message info: " ++ concat (intersperse " and " (map show results))
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
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"]
reifyReportPart :: Term -> Either Err ErrorReportPart
reifyReportPart (App (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "TextPart" =
Right (TextPart msg)
reifyReportPart (App (P (DCon _ _ _) n _) ttn)
| n == reflm "NamePart" =
case runElab initEState (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 == reflm "TermPart" =
case runElab initEState (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 == reflm "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 ())