module Idris.Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,
Tactic(..), Goal(..), processTactic, nowElaboratingPS, doneElaboratingAppPS,
doneElaboratingArgPS, dropGiven, keepGiven, getProvenance) where
import Idris.Core.Typecheck
import Idris.Core.Evaluate
import Idris.Core.TT
import Idris.Core.Unify
import Idris.Core.ProofTerm
import Control.Monad.State.Strict
import Control.Applicative hiding (empty)
import Control.Arrow ((***))
import Data.List
import Debug.Trace
import Util.Pretty hiding (fill)
data ProofState = PS { thname :: Name,
holes :: [Name],
usedns :: [Name],
nextname :: Int,
pterm :: ProofTerm,
ptype :: Type,
dontunify :: [Name],
unified :: (Name, [(Name, Term)]),
notunified :: [(Name, Term)],
dotted :: [(Name, [Name])],
solved :: Maybe (Name, Term),
problems :: Fails,
injective :: [Name],
deferred :: [Name],
instances :: [Name],
autos :: [(Name, [Name])],
previous :: Maybe ProofState,
context :: Context,
plog :: String,
unifylog :: Bool,
done :: Bool,
recents :: [Name],
while_elaborating :: [FailContext]
}
data Tactic = Attack
| Claim Name Raw
| ClaimFn Name Name Raw
| Reorder Name
| Exact Raw
| Fill Raw
| MatchFill Raw
| PrepFill Name [Name]
| CompleteFill
| Regret
| Solve
| StartUnify Name
| EndUnify
| UnifyAll
| Compute
| ComputeLet Name
| Simplify
| HNF_Compute
| EvalIn Raw
| CheckIn Raw
| Intro (Maybe Name)
| IntroTy Raw (Maybe Name)
| Forall Name (Maybe ImplicitInfo) Raw
| LetBind Name Raw Raw
| ExpandLet Name Term
| Rewrite Raw
| Induction Raw
| CaseTac Raw
| Equiv Raw
| PatVar Name
| PatBind Name
| Focus Name
| Defer [Name] Name
| DeferType Name Raw [Name]
| Instance Name
| AutoArg Name
| SetInjective Name
| MoveLast Name
| MatchProblems Bool
| UnifyProblems
| UnifyGoal Raw
| ProofState
| Undo
| QED
deriving Show
instance Show ProofState where
show ps | [] <- holes ps
= show (thname ps) ++ ": no more goals"
show ps | (h : hs) <- holes ps
= let tm = pterm ps
nm = thname ps
OK g = goal (Just h) tm
wkenv = premises g in
"Other goals: " ++ show hs ++ "\n" ++
showPs wkenv (reverse wkenv) ++ "\n" ++
"-------------------------------- (" ++ show nm ++
") -------\n " ++
show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"
where showPs env [] = ""
showPs env ((n, Let t v):bs)
= " " ++ show n ++ " : " ++
showEnv env ( t) ++ " = " ++
showEnv env ( v) ++
"\n" ++ showPs env bs
showPs env ((n, b):bs)
= " " ++ show n ++ " : " ++
showEnv env ( (binderTy b)) ++
"\n" ++ showPs env bs
showG ps (Guess t v) = showEnv ps ( t) ++
" =?= " ++ showEnv ps v
showG ps b = showEnv ps (binderTy b)
instance Pretty ProofState OutputAnnotation where
pretty ps | [] <- holes ps =
pretty (thname ps) <+> colon <+> text " no more goals."
pretty ps | (h : hs) <- holes ps =
let tm = pterm ps
OK g = goal (Just h) tm
nm = thname ps in
let wkEnv = premises g in
text "Other goals" <+> colon <+> pretty hs <+>
prettyPs wkEnv (reverse wkEnv) <+>
text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" <+>
pretty h <+> colon <+> prettyGoal wkEnv (goalType g)
where
prettyGoal ps (Guess t v) =
prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v
prettyGoal ps b = prettyEnv ps $ binderTy b
prettyPs env [] = empty
prettyPs env ((n, Let t v):bs) =
nest nestingSize (pretty n <+> colon <+>
prettyEnv env t <+> text "=" <+> prettyEnv env v <+>
nest nestingSize (prettyPs env bs))
prettyPs env ((n, b):bs) =
nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+>
nest nestingSize (prettyPs env bs))
holeName i = sMN i "hole"
qshow :: Fails -> String
qshow fs = show (map (\ (x, y, hs, _, _, _, t) -> (t, x, y, hs)) fs)
match_unify' :: Context -> Env ->
(TT Name, Maybe Provenance) ->
(TT Name, Maybe Provenance) ->
StateT TState TC [(Name, TT Name)]
match_unify' ctxt env (topx, xfrom) (topy, yfrom) =
do ps <- get
let while = while_elaborating ps
let dont = dontunify ps
let inj = injective ps
traceWhen (unifylog ps)
("Matching " ++ show (topx, topy) ++
" in " ++ show env ++
"\nHoles: " ++ show (holes ps)
++ "\n"
++ "\n" ++ show (getProofTerm (pterm ps)) ++ "\n\n"
) $
case match_unify ctxt env (topx, xfrom) (topy, yfrom) inj (holes ps) while of
OK u -> traceWhen (unifylog ps)
("Matched " ++ show u) $
do let (h, ns) = unified ps
put (ps { unified = (h, u ++ ns) })
return u
Error e -> traceWhen (unifylog ps)
("No match " ++ show e) $
do put (ps { problems = (topx, topy, True,
env, e, while, Match) :
problems ps })
return []
mergeSolutions :: Env -> [(Name, TT Name)] -> StateT TState TC [(Name, TT Name)]
mergeSolutions env ns = merge [] ns
where
merge acc [] = return (reverse acc)
merge acc ((n, t) : ns)
| Just t' <- lookup n ns
= do ps <- get
let probs = problems ps
put (ps { problems = probs ++ [(t,t',True,env,
CantUnify True (t, Nothing) (t', Nothing) (Msg "") (errEnv env) 0,
[], Unify)] })
merge acc ns
| otherwise = merge ((n, t): acc) ns
unify' :: Context -> Env ->
(TT Name, Maybe Provenance) ->
(TT Name, Maybe Provenance) ->
StateT TState TC [(Name, TT Name)]
unify' ctxt env (topx, xfrom) (topy, yfrom) =
do ps <- get
let while = while_elaborating ps
let dont = dontunify ps
let inj = injective ps
(u, fails) <- traceWhen (unifylog ps)
("Trying " ++ show (topx, topy) ++
"\nNormalised " ++ show (normalise ctxt env topx,
normalise ctxt env topy) ++
" in " ++ show env ++
"\nHoles: " ++ show (holes ps)
++ "\nInjective: " ++ show (injective ps)
++ "\n") $
lift $ unify ctxt env (topx, xfrom) (topy, yfrom) inj (holes ps)
(map fst (notunified ps)) while
let notu = filter (\ (n, t) -> case t of
_ -> n `elem` dont) u
traceWhen (unifylog ps)
("Unified " ++ show (topx, topy) ++ " without " ++ show dont ++
"\nSolved: " ++ show u ++ "\nNew problems: " ++ qshow fails
++ "\nNot unified:\n" ++ show (notunified ps)
++ "\nCurrent problems:\n" ++ qshow (problems ps)
++ "\n----------") $
do let (h, ns) = unified ps
let u' = map (\(n, sol) -> (n, updateSolvedTerm u sol)) u
uns <- mergeSolutions env (u' ++ ns)
ps <- get
let (ns', probs') = updateProblems ps uns (fails ++ problems ps)
let (notu', probs_notu) = mergeNotunified env (holes ps) (notu ++ notunified ps)
traceWhen (unifylog ps)
("Now solved: " ++ show ns' ++
"\nNow problems: " ++ qshow (probs' ++ probs_notu)) $
put (ps { problems = probs' ++ probs_notu,
unified = (h, ns'),
injective = updateInj u (injective ps),
notunified = notu' })
return u
where updateInj ((n, a) : us) inj
| (P _ n' _, _) <- unApply a,
n `elem` inj = updateInj us (n':inj)
| (P _ n' _, _) <- unApply a,
n' `elem` inj = updateInj us (n:inj)
updateInj (_ : us) inj = updateInj us inj
updateInj [] inj = inj
nowElaboratingPS :: FC -> Name -> Name -> ProofState -> ProofState
nowElaboratingPS fc f arg ps = ps { while_elaborating = FailContext fc f arg : while_elaborating ps }
dropUntil :: (a -> Bool) -> [a] -> [a]
dropUntil p [] = []
dropUntil p (x:xs) | p x = xs
| otherwise = dropUntil p xs
doneElaboratingAppPS :: Name -> ProofState -> ProofState
doneElaboratingAppPS f ps = let while = while_elaborating ps
while' = dropUntil (\ (FailContext _ f' _) -> f == f') while
in ps { while_elaborating = while' }
doneElaboratingArgPS :: Name -> Name -> ProofState -> ProofState
doneElaboratingArgPS f x ps = let while = while_elaborating ps
while' = dropUntil (\ (FailContext _ f' x') -> f == f' && x == x') while
in ps { while_elaborating = while' }
getName :: Monad m => String -> StateT TState m Name
getName tag = do ps <- get
let n = nextname ps
put (ps { nextname = n+1 })
return $ sMN n tag
action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
action a = do ps <- get
put (a ps)
query :: Monad m => (ProofState -> r) -> StateT TState m r
query q = do ps <- get
return $ q ps
addLog :: Monad m => String -> StateT TState m ()
addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
newProof :: Name -> Context -> Type -> ProofState
newProof n ctxt ty = let h = holeName 0
ty' = vToP ty
in PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty')
(P Bound h ty'))) ty [] (h, []) [] []
Nothing [] []
[] [] []
Nothing ctxt "" False False [] []
type TState = ProofState
type RunTactic = RunTactic' TState
envAtFocus :: ProofState -> TC Env
envAtFocus ps
| not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
return (premises g)
| otherwise = fail "No holes"
goalAtFocus :: ProofState -> TC (Binder Type)
goalAtFocus ps
| not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
return (goalType g)
| otherwise = Error . Msg $ "No goal in " ++ show (holes ps) ++ show (getProofTerm (pterm ps))
tactic :: Hole -> RunTactic -> StateT TState TC ()
tactic h f = do ps <- get
(tm', _) <- atHole h f (context ps) [] (pterm ps)
ps <- get
put (ps { pterm = tm' })
computeLet :: Context -> Name -> Term -> Term
computeLet ctxt n tm = cl [] tm where
cl env (Bind n' (Let t v) sc)
| n' == n = let v' = normalise ctxt env v in
Bind n' (Let t v') sc
cl env (Bind n' b sc) = Bind n' (fmap (cl env) b) (cl ((n, b):env) sc)
cl env (App f a) = App (cl env f) (cl env a)
cl env t = t
attack :: RunTactic
attack ctxt env (Bind x (Hole t) sc)
= do h <- getName "hole"
action (\ps -> ps { holes = h : holes ps })
return $ Bind x (Guess t (newtm h)) sc
where
newtm h = Bind h (Hole t) (P Bound h t)
attack ctxt env _ = fail "Not an attackable hole"
claim :: Name -> Raw -> RunTactic
claim n ty ctxt env t =
do (tyv, tyt) <- lift $ check ctxt env ty
lift $ isType ctxt env tyt
action (\ps -> let (g:gs) = holes ps in
ps { holes = g : n : gs } )
return $ Bind n (Hole tyv) t
claimFn :: Name -> Name -> Raw -> RunTactic
claimFn n bn argty ctxt env t@(Bind x (Hole retty) sc) =
do (tyv, tyt) <- lift $ check ctxt env argty
lift $ isType ctxt env tyt
action (\ps -> let (g:gs) = holes ps in
ps { holes = g : n : gs } )
return $ Bind n (Hole (Bind bn (Pi Nothing tyv tyt) retty)) t
claimFn _ _ _ ctxt env _ = fail "Can't make function type here"
reorder_claims :: RunTactic
reorder_claims ctxt env t
=
let (bs, sc) = scvs t []
newbs = reverse (sortB (reverse bs)) in
traceWhen (bs /= newbs) (show bs ++ "\n ==> \n" ++ show newbs) $
return (bindAll newbs sc)
where scvs (Bind n b@(Hole _) sc) acc = scvs sc ((n, b):acc)
scvs sc acc = (reverse acc, sc)
sortB :: [(Name, Binder (TT Name))] -> [(Name, Binder (TT Name))]
sortB [] = []
sortB (x:xs) | all (noOcc x) xs = x : sortB xs
| otherwise = sortB (insertB x xs)
insertB x [] = [x]
insertB x (y:ys) | all (noOcc x) (y:ys) = x : y : ys
| otherwise = y : insertB x ys
noOcc (n, _) (_, Let t v) = noOccurrence n t && noOccurrence n v
noOcc (n, _) (_, Guess t v) = noOccurrence n t && noOccurrence n v
noOcc (n, _) (_, b) = noOccurrence n (binderTy b)
focus :: Name -> RunTactic
focus n ctxt env t = do action (\ps -> let hs = holes ps in
if n `elem` hs
then ps { holes = n : (hs \\ [n]) }
else ps)
ps <- get
return t
movelast :: Name -> RunTactic
movelast n ctxt env t = do action (\ps -> let hs = holes ps in
if n `elem` hs
then ps { holes = (hs \\ [n]) ++ [n] }
else ps)
return t
instanceArg :: Name -> RunTactic
instanceArg n ctxt env (Bind x (Hole t) sc)
= do action (\ps -> let hs = holes ps
is = instances ps in
ps { holes = (hs \\ [x]) ++ [x],
instances = x:is })
return (Bind x (Hole t) sc)
autoArg :: Name -> RunTactic
autoArg n ctxt env (Bind x (Hole t) sc)
= do action (\ps -> case lookup x (autos ps) of
Nothing ->
let hs = holes ps in
ps { holes = (hs \\ [x]) ++ [x],
autos = (x, refsIn t) : autos ps }
Just _ -> ps)
return (Bind x (Hole t) sc)
setinj :: Name -> RunTactic
setinj n ctxt env (Bind x b sc)
= do action (\ps -> let is = injective ps in
ps { injective = n : is })
return (Bind x b sc)
defer :: [Name] -> Name -> RunTactic
defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
do let env' = filter (\(n, t) -> n `notElem` dropped) env
action (\ps -> let hs = holes ps in
ps { holes = hs \\ [x] })
return (Bind n (GHole (length env') (mkTy (reverse env') t))
(mkApp (P Ref n ty) (map getP (reverse env'))))
where
mkTy [] t = t
mkTy ((n,b) : bs) t = Bind n (Pi Nothing (binderTy b) (TType (UVar 0))) (mkTy bs t)
getP (n, b) = P Bound n (binderTy b)
deferType :: Name -> Raw -> [Name] -> RunTactic
deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =
do (fty, _) <- lift $ check ctxt env fty_in
action (\ps -> let hs = holes ps
ds = deferred ps in
ps { holes = hs \\ [x],
deferred = n : ds })
return (Bind n (GHole 0 fty)
(mkApp (P Ref n ty) (map getP args)))
where
getP n = case lookup n env of
Just b -> P Bound n (binderTy b)
Nothing -> error ("deferType can't find " ++ show n)
regret :: RunTactic
regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =
do action (\ps -> let hs = holes ps in
ps { holes = hs \\ [x] })
return sc
regret ctxt env (Bind x (Hole t) _)
= fail $ show x ++ " : " ++ show t ++ " is not solved..."
unifyGoal :: Raw -> RunTactic
unifyGoal tm ctxt env h@(Bind x b sc) =
do (tmv, _) <- lift $ check ctxt env tm
ns' <- unify' ctxt env (binderTy b, Nothing) (tmv, Nothing)
return h
exact :: Raw -> RunTactic
exact guess ctxt env (Bind x (Hole ty) sc) =
do (val, valty) <- lift $ check ctxt env guess
lift $ converts ctxt env valty ty
return $ Bind x (Guess ty val) sc
exact _ _ _ _ = fail "Can't fill here."
fill :: Raw -> RunTactic
fill guess ctxt env (Bind x (Hole ty) sc) =
do (val, valty) <- lift $ check ctxt env guess
ns <- unify' ctxt env (valty, Just $ SourceTerm val)
(ty, Just (chkPurpose val ty))
ps <- get
let (uh, uns) = unified ps
return $ Bind x (Guess ty val) sc
where
chkPurpose val (Bind _ (Pi _ (P _ (MN _ _) _) _) (P _ (MN _ _) _))
= TooManyArgs val
chkPurpose _ _ = ExpectedType
fill _ _ _ _ = fail "Can't fill here."
match_fill :: Raw -> RunTactic
match_fill guess ctxt env (Bind x (Hole ty) sc) =
do (val, valty) <- lift $ check ctxt env guess
ns <- match_unify' ctxt env (valty, Just $ SourceTerm val)
(ty, Just ExpectedType)
ps <- get
let (uh, uns) = unified ps
return $ Bind x (Guess ty val) sc
match_fill _ _ _ _ = fail "Can't fill here."
prep_fill :: Name -> [Name] -> RunTactic
prep_fill f as ctxt env (Bind x (Hole ty) sc) =
do let val = mkApp (P Ref f Erased) (map (\n -> P Ref n Erased) as)
return $ Bind x (Guess ty val) sc
prep_fill f as ctxt env t = fail $ "Can't prepare fill at " ++ show t
complete_fill :: RunTactic
complete_fill ctxt env (Bind x (Guess ty val) sc) =
do let guess = forget val
(val', valty) <- lift $ check ctxt env guess
ns <- unify' ctxt env (valty, Just $ SourceTerm val')
(ty, Just ExpectedType)
ps <- get
let (uh, uns) = unified ps
return $ Bind x (Guess ty val) sc
complete_fill ctxt env t = fail $ "Can't complete fill at " ++ show t
solve :: RunTactic
solve ctxt env (Bind x (Guess ty val) sc)
= do ps <- get
let (uh, uns) = unified ps
dropdots <-
case lookup x (notunified ps) of
Just tm ->
do match_unify' ctxt env (tm, Just InferredVal)
(val, Just GivenVal)
return [x]
_ -> return []
action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping hole " ++ show x) $
holes ps \\ [x],
solved = Just (x, val),
dontunify = filter (/= x) (dontunify ps),
notunified = updateNotunified [(x,val)]
(notunified ps),
recents = x : recents ps,
instances = instances ps \\ [x],
dotted = dropUnified dropdots (dotted ps) })
let tm' = subst x val sc in
return tm'
where dropUnified ddots [] = []
dropUnified ddots ((x, es) : ds)
| x `elem` ddots || any (\e -> e `elem` ddots) es
= dropUnified ddots ds
| otherwise = (x, es) : dropUnified ddots ds
solve _ _ h@(Bind x t sc)
= do ps <- get
case findType x sc of
Just t -> lift $ tfail (CantInferType (show t))
_ -> lift $ tfail (IncompleteTerm h)
where findType x (Bind n (Let t v) sc)
= findType x v `mplus` findType x sc
findType x (Bind n t sc)
| P _ x' _ <- binderTy t, x == x' = Just n
| otherwise = findType x sc
findType x _ = Nothing
introTy :: Raw -> Maybe Name -> RunTactic
introTy ty mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
do let n = case mn of
Just name -> name
Nothing -> x
let t' = case t of
x@(Bind y (Pi _ s _) _) -> x
_ -> hnf ctxt env t
(tyv, tyt) <- lift $ check ctxt env ty
case t' of
Bind y (Pi _ s _) t -> let t' = subst y (P Bound n s) t in
do ns <- unify' ctxt env (s, Nothing) (tyv, Nothing)
ps <- get
let (uh, uns) = unified ps
return $ Bind n (Lam tyv) (Bind x (Hole t') (P Bound x t'))
_ -> lift $ tfail $ CantIntroduce t'
introTy ty n ctxt env _ = fail "Can't introduce here."
intro :: Maybe Name -> RunTactic
intro mn ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
do let n = case mn of
Just name -> name
Nothing -> x
let t' = case t of
x@(Bind y (Pi _ s _) _) -> x
_ -> hnf ctxt env t
case t' of
Bind y (Pi _ s _) t ->
let t' = subst y (P Bound n s) t in
return $ Bind n (Lam s) (Bind x (Hole t') (P Bound x t'))
_ -> lift $ tfail $ CantIntroduce t'
intro n ctxt env _ = fail "Can't introduce here."
forall :: Name -> Maybe ImplicitInfo -> Raw -> RunTactic
forall n impl ty ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
do (tyv, tyt) <- lift $ check ctxt env ty
unify' ctxt env (tyt, Nothing) (TType (UVar 0), Nothing)
unify' ctxt env (t, Nothing) (TType (UVar 0), Nothing)
return $ Bind n (Pi impl tyv (TType (UVar 0))) (Bind x (Hole t) (P Bound x t))
forall n impl ty ctxt env _ = fail "Can't pi bind here"
patvar :: Name -> RunTactic
patvar n ctxt env (Bind x (Hole t) sc) =
do action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping pattern hole " ++ show x) $
holes ps \\ [x],
solved = Just (x, P Bound n t),
dontunify = filter (/=x) (dontunify ps),
notunified = updateNotunified [(x,P Bound n t)]
(notunified ps),
injective = addInj n x (injective ps)
})
return $ Bind n (PVar t) (subst x (P Bound n t) sc)
where addInj n x ps | x `elem` ps = n : ps
| otherwise = ps
patvar n ctxt env tm = fail $ "Can't add pattern var at " ++ show tm
letbind :: Name -> Raw -> Raw -> RunTactic
letbind n ty val ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
do (tyv, tyt) <- lift $ check ctxt env ty
(valv, valt) <- lift $ check ctxt env val
lift $ isType ctxt env tyt
return $ Bind n (Let tyv valv) (Bind x (Hole t) (P Bound x t))
letbind n ty val ctxt env _ = fail "Can't let bind here"
expandLet :: Name -> Term -> RunTactic
expandLet n v ctxt env tm =
return $ subst n v tm
rewrite :: Raw -> RunTactic
rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
do (tmv, tmt) <- lift $ check ctxt env tm
let tmt' = normalise ctxt env tmt
case unApply tmt' of
(P _ (UN q) _, [lt,rt,l,r]) | q == txt "=" ->
do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)
let newt = mkP l r l t
let sc = forget $ (Bind x (Hole newt)
(mkApp (P Ref (sUN "replace") (TType (UVal 0)))
[lt, l, r, p, tmv, xp]))
(scv, sct) <- lift $ check ctxt env sc
return scv
_ -> lift $ tfail (NotEquality tmv tmt')
where rname = sMN 0 "replaced"
rewrite _ _ _ _ = fail "Can't rewrite here"
mkP :: TT Name -> TT Name -> TT Name -> TT Name -> TT Name
mkP lt l r ty | l == ty = lt
mkP lt l r (App f a) = let f' = if (r /= f) then mkP lt l r f else f
a' = if (r /= a) then mkP lt l r a else a in
App f' a'
mkP lt l r (Bind n b sc)
= let b' = mkPB b
sc' = if (r /= sc) then mkP lt l r sc else sc in
Bind n b' sc'
where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t
v' = if (r /= v) then mkP lt l r v else v in
Let t' v'
mkPB b = let ty = binderTy b
ty' = if (r /= ty) then mkP lt l r ty else ty in
b { binderTy = ty' }
mkP lt l r x = x
casetac :: Raw -> Bool -> RunTactic
casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) |x == x' = do
(tmv, tmt) <- lift $ check ctxt env tm
let tmt' = normalise ctxt env tmt
let (tacn, tacstr, tactt) = if induction
then (ElimN, "eliminator", "Induction")
else (CaseN, "case analysis", "Case analysis")
case unApply tmt' of
(P _ tnm _, tyargs) -> do
case lookupTy (SN (tacn tnm)) ctxt of
[elimTy] -> do
param_pos <- case lookupMetaInformation tnm ctxt of
[DataMI param_pos] -> return param_pos
m | length tyargs > 0 -> fail $ "Invalid meta information for " ++ show tnm ++ " where the metainformation is " ++ show m ++ " and definition is" ++ show (lookupDef tnm ctxt)
_ -> return []
let (params, indicies) = splitTyArgs param_pos tyargs
let args = getArgTys elimTy
let pmargs = take (length params) args
let args' = drop (length params) args
let propTy = head args'
let restargs = init $ tail args'
let consargs = take (length restargs length indicies) $ restargs
let indxargs = drop (length restargs length indicies) $ restargs
let scr = last $ tail args'
let indxnames = makeIndexNames indicies
currentNames <- query $ allTTNames . getProofTerm . pterm
let tmnm = case tm of
Var nm -> uniqueNameCtxt ctxt nm currentNames
_ -> uniqueNameCtxt ctxt (sMN 0 "iv") currentNames
let tmvar = P Bound tmnm tmt'
prop <- replaceIndicies indxnames indicies $ Bind tmnm (Lam tmt') (mkP tmvar tmv tmvar t)
consargs' <- query (\ps -> map (flip (uniqueNameCtxt (context ps)) (holes ps ++ allTTNames (getProofTerm (pterm ps))) *** uniqueBindersCtxt (context ps) (holes ps ++ allTTNames (getProofTerm (pterm ps)))) consargs)
let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs' (mkApp (P Ref (SN (tacn tnm)) (TType (UVal 0)))
(params ++ [prop] ++ map makeConsArg consargs' ++ indicies ++ [tmv])))
action (\ps -> ps {holes = holes ps \\ [x],
recents = x : recents ps })
mapM_ addConsHole (reverse consargs')
let res' = forget $ res
(scv, sct) <- lift $ check ctxt env res'
let (scv', _) = specialise ctxt env [] scv
return scv'
[] -> lift $ tfail $ NoEliminator tacstr tmt'
xs -> lift $ tfail $ Msg $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm
_ -> lift $ tfail $ NoEliminator (if induction then "induction" else "case analysis")
tmt'
where scname = sMN 0 "scarg"
makeConsArg (nm, ty) = P Bound nm ty
bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v
bindConsArgs [] v = v
addConsHole (nm, ty) =
action (\ps -> ps { holes = nm : holes ps })
splitTyArgs param_pos tyargs =
let (params, indicies) = partition (flip elem param_pos . fst) . zip [0..] $ tyargs
in (map snd params, map snd indicies)
makeIndexNames = foldr (\_ nms -> (uniqueNameCtxt ctxt (sMN 0 "idx") nms):nms) []
replaceIndicies idnms idxs prop = foldM (\t (idnm, idx) -> do (idxv, idxt) <- lift $ check ctxt env (forget idx)
let var = P Bound idnm idxt
return $ Bind idnm (Lam idxt) (mkP var idxv var t)) prop $ zip idnms idxs
induction tm induction ctxt env _ = do fail "Can't do induction here"
equiv :: Raw -> RunTactic
equiv tm ctxt env (Bind x (Hole t) sc) =
do (tmv, tmt) <- lift $ check ctxt env tm
lift $ converts ctxt env tmv t
return $ Bind x (Hole tmv) sc
equiv tm ctxt env _ = fail "Can't equiv here"
patbind :: Name -> RunTactic
patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =
do let t' = case t of
x@(Bind y (PVTy s) t) -> x
_ -> hnf ctxt env t
case t' of
Bind y (PVTy s) t -> let t' = subst y (P Bound n s) t in
return $ Bind n (PVar s) (Bind x (Hole t') (P Bound x t'))
_ -> fail "Nothing to pattern bind"
patbind n ctxt env _ = fail "Can't pattern bind here"
compute :: RunTactic
compute ctxt env (Bind x (Hole ty) sc) =
do return $ Bind x (Hole (normalise ctxt env ty)) sc
compute ctxt env t = return t
hnf_compute :: RunTactic
hnf_compute ctxt env (Bind x (Hole ty) sc) =
do let ty' = hnf ctxt env ty in
return $ Bind x (Hole ty') sc
hnf_compute ctxt env t = return t
simplify :: RunTactic
simplify ctxt env (Bind x (Hole ty) sc) =
do return $ Bind x (Hole (fst (specialise ctxt env [] ty))) sc
simplify ctxt env t = return t
check_in :: Raw -> RunTactic
check_in t ctxt env tm =
do (val, valty) <- lift $ check ctxt env t
addLog (showEnv env val ++ " : " ++ showEnv env valty)
return tm
eval_in :: Raw -> RunTactic
eval_in t ctxt env tm =
do (val, valty) <- lift $ check ctxt env t
let val' = normalise ctxt env val
let valty' = normalise ctxt env valty
addLog (showEnv env val ++ " : " ++
showEnv env valty ++
" ==>\n " ++
showEnv env val' ++ " : " ++
showEnv env valty')
return tm
start_unify :: Name -> RunTactic
start_unify n ctxt env tm = do
return tm
tmap f (a, b, c) = (f a, b, c)
solve_unified :: RunTactic
solve_unified ctxt env tm =
do ps <- get
let (_, ns) = unified ps
let unify = dropGiven (dontunify ps) ns (holes ps)
action (\ps -> ps { holes = traceWhen (unifylog ps) ("Dropping holes " ++ show (map fst unify)) $
holes ps \\ map fst unify,
recents = recents ps ++ map fst unify })
action (\ps -> ps { pterm = updateSolved unify (pterm ps) })
return (updateSolvedTerm unify tm)
dropGiven du [] hs = []
dropGiven du ((n, P Bound t ty) : us) hs
| n `elem` du && not (t `elem` du)
&& n `elem` hs && t `elem` hs
= (t, P Bound n ty) : dropGiven du us hs
dropGiven du (u@(n, _) : us) hs
| n `elem` du = dropGiven du us hs
dropGiven du (u : us) hs = u : dropGiven du us hs
keepGiven du [] hs = []
keepGiven du ((n, P Bound t ty) : us) hs
| n `elem` du && not (t `elem` du)
&& n `elem` hs && t `elem` hs
= keepGiven du us hs
keepGiven du (u@(n, _) : us) hs
| n `elem` du = u : keepGiven du us hs
keepGiven du (u : us) hs = keepGiven du us hs
updateEnv [] e = e
updateEnv ns [] = []
updateEnv ns ((n, b) : env)
= (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env
updateProv ns (SourceTerm t) = SourceTerm $ updateSolvedTerm ns t
updateProv ns p = p
updateError [] err = err
updateError ns (At f e) = At f (updateError ns e)
updateError ns (Elaborating s n e) = Elaborating s n (updateError ns e)
updateError ns (ElaboratingArg f a env e)
= ElaboratingArg f a env (updateError ns e)
updateError ns (CantUnify b (l,lp) (r,rp) e xs sc)
= CantUnify b (updateSolvedTerm ns l, fmap (updateProv ns) lp)
(updateSolvedTerm ns r, fmap (updateProv ns) rp) (updateError ns e) xs sc
updateError ns e = e
solveInProblems x val [] = []
solveInProblems x val ((l, r, env, err) : ps)
= ((psubst x val l, psubst x val r,
updateEnv [(x, val)] env, err) : solveInProblems x val ps)
mergeNotunified :: Env -> [Name] -> [(Name, Term)] -> ([(Name, Term)], Fails)
mergeNotunified env holes ns = mnu ns [] [] where
mnu [] ns_acc ps_acc = (reverse ns_acc, reverse ps_acc)
mnu ((n, t):ns) ns_acc ps_acc
| Just t' <- lookup n ns, t /= t'
= mnu ns ((n,t') : ns_acc)
((t,t',True, env,CantUnify True (t, Nothing) (t', Nothing) (Msg "") [] 0, [],Match) : ps_acc)
| otherwise = mnu ns ((n,t) : ns_acc) ps_acc
updateNotunified [] nu = nu
updateNotunified ns nu = up nu where
up [] = []
up ((n, t) : nus) = let t' = updateSolvedTerm ns t in
((n, t') : up nus)
getProvenance :: Err -> (Maybe Provenance, Maybe Provenance)
getProvenance (CantUnify _ (_, lp) (_, rp) _ _ _) = (lp, rp)
getProvenance _ = (Nothing, Nothing)
updateProblems :: ProofState -> [(Name, TT Name)] -> Fails
-> ([(Name, TT Name)], Fails)
updateProblems ps updates probs = up updates probs where
hs = holes ps
inj = injective ps
ctxt = context ps
ulog = unifylog ps
usupp = map fst (notunified ps)
dont = dontunify ps
up ns [] = (ns, [])
up ns (prob@(x, y, ready, env, err, while, um) : ps) =
let (x', newx) = updateSolvedTerm' ns x
(y', newy) = updateSolvedTerm' ns y
(lp, rp) = getProvenance err
err' = updateError ns err
env' = updateEnv ns env in
if newx || newy || ready ||
any (\n -> n `elem` inj) (refsIn x ++ refsIn y) then
case unify ctxt env' (x', lp) (y', rp) inj hs usupp while of
OK (v, []) -> traceWhen ulog ("DID " ++ show (x',y',ready,v,dont)) $
let v' = filter (\(n, _) -> n `notElem` dont) v in
up (ns ++ v') ps
e ->
let (ns', ps') = up ns ps in
(ns', (x',y', False, env',err', while, um) : ps')
else
let (ns', ps') = up ns ps in
(ns', (x',y', False, env',err', while, um) : ps')
matchProblems :: Bool -> ProofState -> [(Name, TT Name)] -> Fails
-> ([(Name, TT Name)], Fails)
matchProblems all ps updates probs = up updates probs where
hs = holes ps
inj = injective ps
ctxt = context ps
up ns [] = (ns, [])
up ns ((x, y, ready, env, err, while, um) : ps)
| all || um == Match =
let x' = updateSolvedTerm ns x
y' = updateSolvedTerm ns y
(lp, rp) = getProvenance err
err' = updateError ns err
env' = updateEnv ns env in
case match_unify ctxt env' (x', lp) (y', rp) inj hs while of
OK v ->
up (ns ++ v) ps
_ -> let (ns', ps') = up ns ps in
(ns', (x', y', True, env', err', while, um) : ps')
up ns (p : ps) = let (ns', ps') = up ns ps in
(ns', p : ps')
processTactic :: Tactic -> ProofState -> TC (ProofState, String)
processTactic QED ps = case holes ps of
[] -> do let tm = getProofTerm (pterm ps)
(tm', ty', _) <- recheck (context ps) [] (forget tm) tm
return (ps { done = True, pterm = mkProofTerm tm' },
"Proof complete: " ++ showEnv [] tm')
_ -> fail "Still holes to fill."
processTactic ProofState ps = return (ps, showEnv [] (getProofTerm (pterm ps)))
processTactic Undo ps = case previous ps of
Nothing -> Error . Msg $ "Nothing to undo."
Just pold -> return (pold, "")
processTactic EndUnify ps
= let (h, ns_in) = unified ps
ns = dropGiven (dontunify ps) ns_in (holes ps)
ns' = map (\ (n, t) -> (n, updateSolvedTerm ns t)) ns
(ns'', probs') = updateProblems ps ns' (problems ps)
tm' = updateSolved ns'' (pterm ps) in
traceWhen (unifylog ps) ("(EndUnify) Dropping holes: " ++ show (map fst ns'')) $
return (ps { pterm = tm',
unified = (h, []),
problems = probs',
notunified = updateNotunified ns'' (notunified ps),
recents = recents ps ++ map fst ns'',
holes = holes ps \\ map fst ns'' }, "")
processTactic UnifyAll ps
= let tm' = updateSolved (notunified ps) (pterm ps) in
return (ps { pterm = tm',
notunified = [],
recents = recents ps ++ map fst (notunified ps),
holes = holes ps \\ map fst (notunified ps) }, "")
processTactic (Reorder n) ps
= do ps' <- execStateT (tactic (Just n) reorder_claims) ps
return (ps' { previous = Just ps, plog = "" }, plog ps')
processTactic (ComputeLet n) ps
= return (ps { pterm = mkProofTerm $
computeLet (context ps) n
(getProofTerm (pterm ps)) }, "")
processTactic UnifyProblems ps
= do let (ns', probs') = updateProblems ps [] (problems ps)
pterm' = updateSolved ns' (pterm ps)
traceWhen (unifylog ps) ("(UnifyProblems) Dropping holes: " ++ show (map fst ns')) $
return (ps { pterm = pterm', solved = Nothing, problems = probs',
previous = Just ps, plog = "",
notunified = updateNotunified ns' (notunified ps),
recents = recents ps ++ map fst ns',
holes = holes ps \\ (map fst ns') }, plog ps)
processTactic (MatchProblems all) ps
= do let (ns', probs') = matchProblems all ps [] (problems ps)
(ns'', probs'') = matchProblems all ps ns' probs'
pterm' = updateSolved ns'' (pterm ps)
traceWhen (unifylog ps) ("(MatchProblems) Dropping holes: " ++ show (map fst ns'')) $
return (ps { pterm = pterm', solved = Nothing, problems = probs'',
previous = Just ps, plog = "",
notunified = updateNotunified ns'' (notunified ps),
recents = recents ps ++ map fst ns'',
holes = holes ps \\ (map fst ns'') }, plog ps)
processTactic t ps
= case holes ps of
[] -> fail "Nothing to fill in."
(h:_) -> do ps' <- execStateT (process t h) ps
let (ns_in, probs')
= case solved ps' of
Just s -> traceWhen (unifylog ps)
("SOLVED " ++ show s ++ " " ++ show (dontunify ps')) $
updateProblems ps' [s] (problems ps')
_ -> ([], problems ps')
let ns' = dropGiven (dontunify ps') ns_in (holes ps')
let pterm'' = updateSolved ns' (pterm ps')
traceWhen (unifylog ps)
("Updated problems after solve " ++ qshow probs' ++ "\n" ++
"(Toplevel) Dropping holes: " ++ show (map fst ns')) $
return (ps' { pterm = pterm'',
solved = Nothing,
problems = probs',
notunified = updateNotunified ns' (notunified ps'),
previous = Just ps, plog = "",
recents = recents ps' ++ map fst ns',
holes = holes ps' \\ (map fst ns')}, plog ps')
process :: Tactic -> Name -> StateT TState TC ()
process EndUnify _
= do ps <- get
let (h, _) = unified ps
tactic (Just h) solve_unified
process t h = tactic (Just h) (mktac t)
where mktac Attack = attack
mktac (Claim n r) = claim n r
mktac (ClaimFn n bn r) = claimFn n bn r
mktac (Exact r) = exact r
mktac (Fill r) = fill r
mktac (MatchFill r) = match_fill r
mktac (PrepFill n ns) = prep_fill n ns
mktac CompleteFill = complete_fill
mktac Solve = solve
mktac (StartUnify n) = start_unify n
mktac Compute = compute
mktac Simplify = Idris.Core.ProofState.simplify
mktac HNF_Compute = hnf_compute
mktac (Intro n) = intro n
mktac (IntroTy ty n) = introTy ty n
mktac (Forall n i t) = forall n i t
mktac (LetBind n t v) = letbind n t v
mktac (ExpandLet n b) = expandLet n b
mktac (Rewrite t) = rewrite t
mktac (Induction t) = casetac t True
mktac (CaseTac t) = casetac t False
mktac (Equiv t) = equiv t
mktac (PatVar n) = patvar n
mktac (PatBind n) = patbind n
mktac (CheckIn r) = check_in r
mktac (EvalIn r) = eval_in r
mktac (Focus n) = focus n
mktac (Defer ns n) = defer ns n
mktac (DeferType n t a) = deferType n t a
mktac (Instance n) = instanceArg n
mktac (AutoArg n) = autoArg n
mktac (SetInjective n) = setinj n
mktac (MoveLast n) = movelast n
mktac (UnifyGoal r) = unifyGoal r