{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, PatternGuards #-}
module Idris.Core.Elaborate (
module Idris.Core.Elaborate
, module Idris.Core.ProofState
) where
import Idris.Core.Evaluate
import Idris.Core.ProofState
import Idris.Core.ProofTerm (bound_in, bound_in_term, getProofTerm, mkProofTerm,
refocus)
import Idris.Core.TT
import Idris.Core.Typecheck
import Idris.Core.Unify
import Control.Monad
import Control.Monad.State.Strict
import Data.List
data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))
deriving Int -> ElabState aux -> ShowS
[ElabState aux] -> ShowS
ElabState aux -> String
(Int -> ElabState aux -> ShowS)
-> (ElabState aux -> String)
-> ([ElabState aux] -> ShowS)
-> Show (ElabState aux)
forall aux. Show aux => Int -> ElabState aux -> ShowS
forall aux. Show aux => [ElabState aux] -> ShowS
forall aux. Show aux => ElabState aux -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall aux. Show aux => Int -> ElabState aux -> ShowS
showsPrec :: Int -> ElabState aux -> ShowS
$cshow :: forall aux. Show aux => ElabState aux -> String
show :: ElabState aux -> String
$cshowList :: forall aux. Show aux => [ElabState aux] -> ShowS
showList :: [ElabState aux] -> ShowS
Show
type Elab' aux a = StateT (ElabState aux) TC a
type Elab a = Elab' () a
proof :: ElabState aux -> ProofState
proof :: forall aux. ElabState aux -> ProofState
proof (ES (ProofState
p, aux
_) String
_ Maybe (ElabState aux)
_) = ProofState
p
proofFail :: Elab' aux a -> Elab' aux a
proofFail :: forall aux a. Elab' aux a -> Elab' aux a
proofFail Elab' aux a
e = do ElabState aux
s <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
case Elab' aux a -> ElabState aux -> TC (a, ElabState aux)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT Elab' aux a
e ElabState aux
s of
OK (a
a, ElabState aux
s') -> do ElabState aux -> StateT (ElabState aux) TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ElabState aux
s'
a -> Elab' aux a
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Elab' aux a) -> a -> Elab' aux a
forall a b. (a -> b) -> a -> b
$! a
a
Error Err
err -> TC a -> Elab' aux a
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC a -> Elab' aux a) -> TC a -> Elab' aux a
forall a b. (a -> b) -> a -> b
$ Err -> TC a
forall a. Err -> TC a
Error (Err -> Err
forall t. Err' t -> Err' t
ProofSearchFail Err
err)
explicit :: Name -> Elab' aux ()
explicit :: forall aux. Name -> Elab' aux ()
explicit Name
n = do ES (ProofState
p, aux
a) String
s Maybe (ElabState aux)
m <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
let p' :: ProofState
p' = ProofState
p { dontunify = n : dontunify p }
ElabState aux -> Elab' aux ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
p', aux
a) String
s Maybe (ElabState aux)
m)
addPSname :: Name -> Elab' aux ()
addPSname :: forall aux. Name -> Elab' aux ()
addPSname n :: Name
n@(UN Text
_)
= do ES (ProofState
p, aux
a) String
s Maybe (ElabState aux)
m <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
let p' :: ProofState
p' = ProofState
p { psnames = n : psnames p }
ElabState aux -> Elab' aux ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
p', aux
a) String
s Maybe (ElabState aux)
m)
addPSname Name
_ = () -> Elab' aux ()
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
getPSnames :: Elab' aux [Name]
getPSnames :: forall aux. Elab' aux [Name]
getPSnames = do ES (ProofState
p, aux
a) String
s Maybe (ElabState aux)
m <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
[Name] -> Elab' aux [Name]
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofState -> [Name]
psnames ProofState
p)
saveState :: Elab' aux ()
saveState :: forall aux. Elab' aux ()
saveState = do e :: ElabState aux
e@(ES (ProofState, aux)
p String
s Maybe (ElabState aux)
_) <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
ElabState aux -> Elab' aux ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState, aux)
p String
s (ElabState aux -> Maybe (ElabState aux)
forall a. a -> Maybe a
Just ElabState aux
e))
loadState :: Elab' aux ()
loadState :: forall aux. Elab' aux ()
loadState = do (ES (ProofState, aux)
p String
s Maybe (ElabState aux)
e) <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
case Maybe (ElabState aux)
e of
Just ElabState aux
st -> ElabState aux -> Elab' aux ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ElabState aux
st
Maybe (ElabState aux)
_ -> TC () -> Elab' aux ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> Elab' aux ()) -> TC () -> Elab' aux ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
Error (Err -> TC ()) -> (String -> Err) -> String -> TC ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Err
forall t. String -> Err' t
Msg (String -> TC ()) -> String -> TC ()
forall a b. (a -> b) -> a -> b
$ String
"Nothing to undo"
getNameFrom :: Name -> Elab' aux Name
getNameFrom :: forall aux. Name -> Elab' aux Name
getNameFrom Name
n = do (ES (ProofState
p, aux
a) String
s Maybe (ElabState aux)
e) <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
let next :: Int
next = ProofState -> Int
nextname ProofState
p
let p' :: ProofState
p' = ProofState
p { nextname = next + 1 }
ElabState aux -> StateT (ElabState aux) TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
p', aux
a) String
s Maybe (ElabState aux)
e)
let n' :: Name
n' = case Name
n of
UN Text
x -> Int -> Text -> Name
MN (Int
nextInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
100) Text
x
MN Int
i Text
x -> if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
99999
then Int -> Text -> Name
MN (Int
nextInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
500) Text
x
else Int -> Text -> Name
MN (Int
nextInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
100) Text
x
NS (UN Text
x) [Text]
s -> Int -> Text -> Name
MN (Int
nextInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
100) Text
x
Name
_ -> Name
n
Name -> Elab' aux Name
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Elab' aux Name) -> Name -> Elab' aux Name
forall a b. (a -> b) -> a -> b
$! Name
n'
setNextName :: Elab' aux ()
setNextName :: forall aux. Elab' aux ()
setNextName = do Env
env <- Elab' aux Env
forall aux. Elab' aux Env
get_env
ES (ProofState
p, aux
a) String
s Maybe (ElabState aux)
e <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
let pargs :: [Name]
pargs = ((Name, TT Name) -> Name) -> [(Name, TT Name)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, TT Name) -> Name
forall a b. (a, b) -> a
fst (TT Name -> [(Name, TT Name)]
forall n. TT n -> [(n, TT n)]
getArgTys (ProofState -> TT Name
ptype ProofState
p))
[Name] -> Elab' aux ()
forall aux. [Name] -> Elab' aux ()
initNextNameFrom ([Name]
pargs [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ ((Name, RigCount, Binder (TT Name)) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name)) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
env)
initNextNameFrom :: [Name] -> Elab' aux ()
initNextNameFrom :: forall aux. [Name] -> Elab' aux ()
initNextNameFrom [Name]
ns = do ES (ProofState
p, aux
a) String
s Maybe (ElabState aux)
e <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
let n' :: Int
n' = Int -> [Name] -> Int
maxName (ProofState -> Int
nextname ProofState
p) [Name]
ns
ElabState aux -> Elab' aux ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
p { nextname = n' }, aux
a) String
s Maybe (ElabState aux)
e)
where
maxName :: Int -> [Name] -> Int
maxName Int
m ((MN Int
i Text
_) : [Name]
xs) = Int -> [Name] -> Int
maxName (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
m Int
i) [Name]
xs
maxName Int
m (Name
_ : [Name]
xs) = Int -> [Name] -> Int
maxName Int
m [Name]
xs
maxName Int
m [] = Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
transformErr :: (Err -> Err) -> Elab' aux a -> Elab' aux a
transformErr :: forall aux a. (Err -> Err) -> Elab' aux a -> Elab' aux a
transformErr Err -> Err
f Elab' aux a
elab = do ElabState aux
s <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
case Elab' aux a -> ElabState aux -> TC (a, ElabState aux)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT Elab' aux a
elab ElabState aux
s of
OK (a
a, ElabState aux
s') -> do ElabState aux -> StateT (ElabState aux) TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ElabState aux
s'
a -> Elab' aux a
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Elab' aux a) -> a -> Elab' aux a
forall a b. (a -> b) -> a -> b
$! a
a
Error Err
e -> TC a -> Elab' aux a
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC a -> Elab' aux a) -> TC a -> Elab' aux a
forall a b. (a -> b) -> a -> b
$ Err -> TC a
forall a. Err -> TC a
Error (Err -> Err
rewriteErr Err
e)
where
rewriteErr :: Err -> Err
rewriteErr (At FC
f Err
e) = FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
f (Err -> Err
rewriteErr Err
e)
rewriteErr (ProofSearchFail Err
e) = Err -> Err
forall t. Err' t -> Err' t
ProofSearchFail (Err -> Err
rewriteErr Err
e)
rewriteErr Err
e = Err -> Err
f Err
e
errAt :: String -> Name -> Maybe Type -> Elab' aux a -> Elab' aux a
errAt :: forall aux a.
String -> Name -> Maybe (TT Name) -> Elab' aux a -> Elab' aux a
errAt String
thing Name
n Maybe (TT Name)
ty = (Err -> Err) -> Elab' aux a -> Elab' aux a
forall aux a. (Err -> Err) -> Elab' aux a -> Elab' aux a
transformErr (String -> Name -> Maybe (TT Name) -> Err -> Err
forall t. String -> Name -> Maybe t -> Err' t -> Err' t
Elaborating String
thing Name
n Maybe (TT Name)
ty)
erunAux :: FC -> Elab' aux a -> Elab' aux (a, aux)
erunAux :: forall aux a. FC -> Elab' aux a -> Elab' aux (a, aux)
erunAux FC
f Elab' aux a
elab
= do ElabState aux
s <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
case Elab' aux a -> ElabState aux -> TC (a, ElabState aux)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT Elab' aux a
elab ElabState aux
s of
OK (a
a, ElabState aux
s') -> do ElabState aux -> StateT (ElabState aux) TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ElabState aux
s'
aux
aux <- Elab' aux aux
forall aux. Elab' aux aux
getAux
(a, aux) -> Elab' aux (a, aux)
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ((a, aux) -> Elab' aux (a, aux)) -> (a, aux) -> Elab' aux (a, aux)
forall a b. (a -> b) -> a -> b
$! (a
a, aux
aux)
Error (ProofSearchFail (At FC
f Err
e))
-> TC (a, aux) -> Elab' aux (a, aux)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (a, aux) -> Elab' aux (a, aux))
-> TC (a, aux) -> Elab' aux (a, aux)
forall a b. (a -> b) -> a -> b
$ Err -> TC (a, aux)
forall a. Err -> TC a
Error (Err -> Err
forall t. Err' t -> Err' t
ProofSearchFail (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
f Err
e))
Error (At FC
f Err
e) -> TC (a, aux) -> Elab' aux (a, aux)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (a, aux) -> Elab' aux (a, aux))
-> TC (a, aux) -> Elab' aux (a, aux)
forall a b. (a -> b) -> a -> b
$ Err -> TC (a, aux)
forall a. Err -> TC a
Error (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
f Err
e)
Error Err
e -> TC (a, aux) -> Elab' aux (a, aux)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (a, aux) -> Elab' aux (a, aux))
-> TC (a, aux) -> Elab' aux (a, aux)
forall a b. (a -> b) -> a -> b
$ Err -> TC (a, aux)
forall a. Err -> TC a
Error (FC -> Err -> Err
forall t. FC -> Err' t -> Err' t
At FC
f Err
e)
erun :: FC -> Elab' aux a -> Elab' aux a
erun :: forall aux a. FC -> Elab' aux a -> Elab' aux a
erun FC
f Elab' aux a
e = do (a
x, aux
_) <- FC -> Elab' aux a -> Elab' aux (a, aux)
forall aux a. FC -> Elab' aux a -> Elab' aux (a, aux)
erunAux FC
f Elab' aux a
e
a -> Elab' aux a
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return a
x
runElab :: aux -> Elab' aux a -> ProofState -> TC (a, ElabState aux)
runElab :: forall aux a.
aux -> Elab' aux a -> ProofState -> TC (a, ElabState aux)
runElab aux
a Elab' aux a
e ProofState
ps = Elab' aux a -> ElabState aux -> TC (a, ElabState aux)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT Elab' aux a
e ((ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
ps, aux
a) String
"" Maybe (ElabState aux)
forall a. Maybe a
Nothing)
execElab :: aux -> Elab' aux a -> ProofState -> TC (ElabState aux)
execElab :: forall aux a.
aux -> Elab' aux a -> ProofState -> TC (ElabState aux)
execElab aux
a Elab' aux a
e ProofState
ps = Elab' aux a -> ElabState aux -> TC (ElabState aux)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m s
execStateT Elab' aux a
e ((ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
ps, aux
a) String
"" Maybe (ElabState aux)
forall a. Maybe a
Nothing)
initElaborator :: Name
-> String
-> Context
-> Ctxt TypeInfo
-> Int
-> Type
-> ProofState
initElaborator :: Name
-> String
-> Context
-> Ctxt TypeInfo
-> Int
-> TT Name
-> ProofState
initElaborator = Name
-> String
-> Context
-> Ctxt TypeInfo
-> Int
-> TT Name
-> ProofState
newProof
elaborate :: String -> Context -> Ctxt TypeInfo -> Int -> Name -> Type -> aux -> Elab' aux a -> TC (a, String)
elaborate :: forall aux a.
String
-> Context
-> Ctxt TypeInfo
-> Int
-> Name
-> TT Name
-> aux
-> Elab' aux a
-> TC (a, String)
elaborate String
tcns Context
ctxt Ctxt TypeInfo
datatypes Int
globalNames Name
n TT Name
ty aux
d Elab' aux a
elab =
do let ps :: ProofState
ps = Name
-> String
-> Context
-> Ctxt TypeInfo
-> Int
-> TT Name
-> ProofState
initElaborator Name
n String
tcns Context
ctxt Ctxt TypeInfo
datatypes Int
globalNames TT Name
ty
(a
a, ES (ProofState, aux)
ps' String
str Maybe (ElabState aux)
_) <- aux -> Elab' aux a -> ProofState -> TC (a, ElabState aux)
forall aux a.
aux -> Elab' aux a -> ProofState -> TC (a, ElabState aux)
runElab aux
d Elab' aux a
elab ProofState
ps
(a, String) -> TC (a, String)
forall a. a -> TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ((a, String) -> TC (a, String)) -> (a, String) -> TC (a, String)
forall a b. (a -> b) -> a -> b
$! (a
a, String
str)
updateAux :: (aux -> aux) -> Elab' aux ()
updateAux :: forall aux. (aux -> aux) -> Elab' aux ()
updateAux aux -> aux
f = do ES (ProofState
ps, aux
a) String
l Maybe (ElabState aux)
p <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
ElabState aux -> Elab' aux ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
ps, aux -> aux
f aux
a) String
l Maybe (ElabState aux)
p)
getAux :: Elab' aux aux
getAux :: forall aux. Elab' aux aux
getAux = do ES (ProofState
ps, aux
a) String
_ Maybe (ElabState aux)
_ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
aux -> Elab' aux aux
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (aux -> Elab' aux aux) -> aux -> Elab' aux aux
forall a b. (a -> b) -> a -> b
$! aux
a
unifyLog :: Bool -> Elab' aux ()
unifyLog :: forall aux. Bool -> Elab' aux ()
unifyLog Bool
log = do ES (ProofState
ps, aux
a) String
l Maybe (ElabState aux)
p <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
ElabState aux -> Elab' aux ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
ps { unifylog = log }, aux
a) String
l Maybe (ElabState aux)
p)
getUnifyLog :: Elab' aux Bool
getUnifyLog :: forall aux. Elab' aux Bool
getUnifyLog = do ES (ProofState
ps, aux
a) String
l Maybe (ElabState aux)
p <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
Bool -> Elab' aux Bool
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofState -> Bool
unifylog ProofState
ps)
processTactic' :: Tactic -> Elab' aux ()
processTactic' :: forall aux. Tactic -> Elab' aux ()
processTactic' Tactic
t = do ES (ProofState
p, aux
a) String
logs Maybe (ElabState aux)
prev <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
(ProofState
p', String
log) <- TC (ProofState, String)
-> StateT (ElabState aux) TC (ProofState, String)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (ProofState, String)
-> StateT (ElabState aux) TC (ProofState, String))
-> TC (ProofState, String)
-> StateT (ElabState aux) TC (ProofState, String)
forall a b. (a -> b) -> a -> b
$ Tactic -> ProofState -> TC (ProofState, String)
processTactic Tactic
t ProofState
p
ElabState aux -> Elab' aux ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
p', aux
a) (String
logs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
log) Maybe (ElabState aux)
prev)
() -> Elab' aux ()
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> Elab' aux ()) -> () -> Elab' aux ()
forall a b. (a -> b) -> a -> b
$! ()
updatePS :: (ProofState -> ProofState) -> Elab' aux ()
updatePS :: forall aux. (ProofState -> ProofState) -> Elab' aux ()
updatePS ProofState -> ProofState
f = do ES (ProofState
ps, aux
a) String
logs Maybe (ElabState aux)
prev <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
ElabState aux -> Elab' aux ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (ElabState aux -> Elab' aux ()) -> ElabState aux -> Elab' aux ()
forall a b. (a -> b) -> a -> b
$ (ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState -> ProofState
f ProofState
ps, aux
a) String
logs Maybe (ElabState aux)
prev
now_elaborating :: FC -> Name -> Name -> Elab' aux ()
now_elaborating :: forall aux. FC -> Name -> Name -> Elab' aux ()
now_elaborating FC
fc Name
f Name
a = (ProofState -> ProofState) -> Elab' aux ()
forall aux. (ProofState -> ProofState) -> Elab' aux ()
updatePS (FC -> Name -> Name -> ProofState -> ProofState
nowElaboratingPS FC
fc Name
f Name
a)
done_elaborating_app :: Name -> Elab' aux ()
done_elaborating_app :: forall aux. Name -> Elab' aux ()
done_elaborating_app Name
f = (ProofState -> ProofState) -> Elab' aux ()
forall aux. (ProofState -> ProofState) -> Elab' aux ()
updatePS (Name -> ProofState -> ProofState
doneElaboratingAppPS Name
f)
done_elaborating_arg :: Name -> Name -> Elab' aux ()
done_elaborating_arg :: forall aux. Name -> Name -> Elab' aux ()
done_elaborating_arg Name
f Name
a = (ProofState -> ProofState) -> Elab' aux ()
forall aux. (ProofState -> ProofState) -> Elab' aux ()
updatePS (Name -> Name -> ProofState -> ProofState
doneElaboratingArgPS Name
f Name
a)
elaborating_app :: Elab' aux [(FC, Name, Name)]
elaborating_app :: forall aux. Elab' aux [(FC, Name, Name)]
elaborating_app = do ES (ProofState
ps, aux
_) String
_ Maybe (ElabState aux)
_ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
[(FC, Name, Name)] -> Elab' aux [(FC, Name, Name)]
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(FC, Name, Name)] -> Elab' aux [(FC, Name, Name)])
-> [(FC, Name, Name)] -> Elab' aux [(FC, Name, Name)]
forall a b. (a -> b) -> a -> b
$ (FailContext -> (FC, Name, Name))
-> [FailContext] -> [(FC, Name, Name)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (FailContext FC
x Name
y Name
z) -> (FC
x, Name
y, Name
z))
(ProofState -> [FailContext]
while_elaborating ProofState
ps)
get_context :: Elab' aux Context
get_context :: forall aux. Elab' aux Context
get_context = do ES (ProofState, aux)
p String
_ Maybe (ElabState aux)
_ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
Context -> Elab' aux Context
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Context -> Elab' aux Context) -> Context -> Elab' aux Context
forall a b. (a -> b) -> a -> b
$! (ProofState -> Context
context ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p))
set_context :: Context -> Elab' aux ()
set_context :: forall aux. Context -> Elab' aux ()
set_context Context
ctxt = do ES (ProofState
p, aux
a) String
logs Maybe (ElabState aux)
prev <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
ElabState aux -> Elab' aux ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
p { context = ctxt }, aux
a) String
logs Maybe (ElabState aux)
prev)
get_datatypes :: Elab' aux (Ctxt TypeInfo)
get_datatypes :: forall aux. Elab' aux (Ctxt TypeInfo)
get_datatypes = do ES (ProofState, aux)
p String
_ Maybe (ElabState aux)
_ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
Ctxt TypeInfo -> Elab' aux (Ctxt TypeInfo)
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Ctxt TypeInfo -> Elab' aux (Ctxt TypeInfo))
-> Ctxt TypeInfo -> Elab' aux (Ctxt TypeInfo)
forall a b. (a -> b) -> a -> b
$! (ProofState -> Ctxt TypeInfo
datatypes ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p))
set_datatypes :: Ctxt TypeInfo -> Elab' aux ()
set_datatypes :: forall aux. Ctxt TypeInfo -> Elab' aux ()
set_datatypes Ctxt TypeInfo
ds = do ES (ProofState
p, aux
a) String
logs Maybe (ElabState aux)
prev <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
ElabState aux -> Elab' aux ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
p { datatypes = ds }, aux
a) String
logs Maybe (ElabState aux)
prev)
get_global_nextname :: Elab' aux Int
get_global_nextname :: forall aux. Elab' aux Int
get_global_nextname = do ES (ProofState
ps, aux
_) String
_ Maybe (ElabState aux)
_ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
Int -> Elab' aux Int
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofState -> Int
global_nextname ProofState
ps)
set_global_nextname :: Int -> Elab' aux ()
set_global_nextname :: forall aux. Int -> Elab' aux ()
set_global_nextname Int
i = do ES (ProofState
ps, aux
a) String
logs Maybe (ElabState aux)
prev <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
ElabState aux -> Elab' aux ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (ElabState aux -> Elab' aux ()) -> ElabState aux -> Elab' aux ()
forall a b. (a -> b) -> a -> b
$ (ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
ps { global_nextname = i}, aux
a) String
logs Maybe (ElabState aux)
prev
get_term :: Elab' aux Term
get_term :: forall aux. Elab' aux (TT Name)
get_term = do ES (ProofState, aux)
p String
_ Maybe (ElabState aux)
_ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
TT Name -> Elab' aux (TT Name)
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> Elab' aux (TT Name)) -> TT Name -> Elab' aux (TT Name)
forall a b. (a -> b) -> a -> b
$! (ProofTerm -> TT Name
getProofTerm (ProofState -> ProofTerm
pterm ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p)))
update_term :: (Term -> Term) -> Elab' aux ()
update_term :: forall aux. (TT Name -> TT Name) -> Elab' aux ()
update_term TT Name -> TT Name
f = do ES (ProofState
p,aux
a) String
logs Maybe (ElabState aux)
prev <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
let p' :: ProofState
p' = ProofState
p { pterm = mkProofTerm (f (getProofTerm (pterm p))) }
ElabState aux -> Elab' aux ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
p', aux
a) String
logs Maybe (ElabState aux)
prev)
get_env :: Elab' aux Env
get_env :: forall aux. Elab' aux Env
get_env = do ES (ProofState, aux)
p String
_ Maybe (ElabState aux)
_ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
TC Env -> Elab' aux Env
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC Env -> Elab' aux Env) -> TC Env -> Elab' aux Env
forall a b. (a -> b) -> a -> b
$ ProofState -> TC Env
envAtFocus ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p)
get_inj :: Elab' aux [Name]
get_inj :: forall aux. Elab' aux [Name]
get_inj = do ES (ProofState, aux)
p String
_ Maybe (ElabState aux)
_ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
[Name] -> Elab' aux [Name]
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name] -> Elab' aux [Name]) -> [Name] -> Elab' aux [Name]
forall a b. (a -> b) -> a -> b
$! (ProofState -> [Name]
injective ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p))
get_holes :: Elab' aux [Name]
get_holes :: forall aux. Elab' aux [Name]
get_holes = do ES (ProofState, aux)
p String
_ Maybe (ElabState aux)
_ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
[Name] -> Elab' aux [Name]
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name] -> Elab' aux [Name]) -> [Name] -> Elab' aux [Name]
forall a b. (a -> b) -> a -> b
$! (ProofState -> [Name]
holes ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p))
get_usedns :: Elab' aux [Name]
get_usedns :: forall aux. Elab' aux [Name]
get_usedns = do ES (ProofState, aux)
p String
_ Maybe (ElabState aux)
_ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
let bs :: [Name]
bs = ProofTerm -> [Name]
bound_in (ProofState -> ProofTerm
pterm ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p)) [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++
TT Name -> [Name]
bound_in_term (ProofState -> TT Name
ptype ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p))
let nouse :: [Name]
nouse = ProofState -> [Name]
holes ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p) [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
bs [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ ProofState -> [Name]
dontunify ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p) [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ ProofState -> [Name]
usedns ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p)
[Name] -> Elab' aux [Name]
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name] -> Elab' aux [Name]) -> [Name] -> Elab' aux [Name]
forall a b. (a -> b) -> a -> b
$! [Name]
nouse
get_probs :: Elab' aux Fails
get_probs :: forall aux. Elab' aux Fails
get_probs = do ES (ProofState, aux)
p String
_ Maybe (ElabState aux)
_ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
Fails -> Elab' aux Fails
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Fails -> Elab' aux Fails) -> Fails -> Elab' aux Fails
forall a b. (a -> b) -> a -> b
$! (ProofState -> Fails
problems ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p))
get_recents :: Elab' aux [Name]
get_recents :: forall aux. Elab' aux [Name]
get_recents = do ES (ProofState
p, aux
a) String
l Maybe (ElabState aux)
prev <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
ElabState aux -> StateT (ElabState aux) TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
p { recents = [] }, aux
a) String
l Maybe (ElabState aux)
prev)
[Name] -> Elab' aux [Name]
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofState -> [Name]
recents ProofState
p)
goal :: Elab' aux Type
goal :: forall aux. Elab' aux (TT Name)
goal = do ES (ProofState, aux)
p String
_ Maybe (ElabState aux)
_ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
Binder (TT Name)
b <- TC (Binder (TT Name))
-> StateT (ElabState aux) TC (Binder (TT Name))
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Binder (TT Name))
-> StateT (ElabState aux) TC (Binder (TT Name)))
-> TC (Binder (TT Name))
-> StateT (ElabState aux) TC (Binder (TT Name))
forall a b. (a -> b) -> a -> b
$ ProofState -> TC (Binder (TT Name))
goalAtFocus ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p)
TT Name -> Elab' aux (TT Name)
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> Elab' aux (TT Name)) -> TT Name -> Elab' aux (TT Name)
forall a b. (a -> b) -> a -> b
$! (Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
b)
is_guess :: Elab' aux Bool
is_guess :: forall aux. Elab' aux Bool
is_guess = do ES (ProofState, aux)
p String
_ Maybe (ElabState aux)
_ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
Binder (TT Name)
b <- TC (Binder (TT Name))
-> StateT (ElabState aux) TC (Binder (TT Name))
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Binder (TT Name))
-> StateT (ElabState aux) TC (Binder (TT Name)))
-> TC (Binder (TT Name))
-> StateT (ElabState aux) TC (Binder (TT Name))
forall a b. (a -> b) -> a -> b
$ ProofState -> TC (Binder (TT Name))
goalAtFocus ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p)
case Binder (TT Name)
b of
Guess TT Name
_ TT Name
_ -> Bool -> Elab' aux Bool
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Binder (TT Name)
_ -> Bool -> Elab' aux Bool
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
get_guess :: Elab' aux Term
get_guess :: forall aux. Elab' aux (TT Name)
get_guess = do ES (ProofState, aux)
p String
_ Maybe (ElabState aux)
_ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
Binder (TT Name)
b <- TC (Binder (TT Name))
-> StateT (ElabState aux) TC (Binder (TT Name))
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (Binder (TT Name))
-> StateT (ElabState aux) TC (Binder (TT Name)))
-> TC (Binder (TT Name))
-> StateT (ElabState aux) TC (Binder (TT Name))
forall a b. (a -> b) -> a -> b
$ ProofState -> TC (Binder (TT Name))
goalAtFocus ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p)
case Binder (TT Name)
b of
Guess TT Name
t TT Name
v -> TT Name -> Elab' aux (TT Name)
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> Elab' aux (TT Name)) -> TT Name -> Elab' aux (TT Name)
forall a b. (a -> b) -> a -> b
$! TT Name
v
Binder (TT Name)
_ -> String -> Elab' aux (TT Name)
forall a. String -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Not a guess"
get_type :: Raw -> Elab' aux Type
get_type :: forall aux. Raw -> Elab' aux (TT Name)
get_type Raw
tm = do Context
ctxt <- Elab' aux Context
forall aux. Elab' aux Context
get_context
Env
env <- Elab' aux Env
forall aux. Elab' aux Env
get_env
(TT Name
val, TT Name
ty) <- TC (TT Name, TT Name)
-> StateT (ElabState aux) TC (TT Name, TT Name)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (TT Name, TT Name)
-> StateT (ElabState aux) TC (TT Name, TT Name))
-> TC (TT Name, TT Name)
-> StateT (ElabState aux) TC (TT Name, TT Name)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (TT Name, TT Name)
check Context
ctxt Env
env Raw
tm
TT Name -> Elab' aux (TT Name)
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> Elab' aux (TT Name)) -> TT Name -> Elab' aux (TT Name)
forall a b. (a -> b) -> a -> b
$! (TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
ty)
get_type_val :: Raw -> Elab' aux (Term, Type)
get_type_val :: forall aux. Raw -> Elab' aux (TT Name, TT Name)
get_type_val Raw
tm = do Context
ctxt <- Elab' aux Context
forall aux. Elab' aux Context
get_context
Env
env <- Elab' aux Env
forall aux. Elab' aux Env
get_env
(TT Name
val, TT Name
ty) <- TC (TT Name, TT Name) -> Elab' aux (TT Name, TT Name)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC (TT Name, TT Name) -> Elab' aux (TT Name, TT Name))
-> TC (TT Name, TT Name) -> Elab' aux (TT Name, TT Name)
forall a b. (a -> b) -> a -> b
$ Context -> Env -> Raw -> TC (TT Name, TT Name)
check Context
ctxt Env
env Raw
tm
(TT Name, TT Name) -> Elab' aux (TT Name, TT Name)
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ((TT Name, TT Name) -> Elab' aux (TT Name, TT Name))
-> (TT Name, TT Name) -> Elab' aux (TT Name, TT Name)
forall a b. (a -> b) -> a -> b
$! (TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
val, TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
ty)
get_deferred :: Elab' aux [Name]
get_deferred :: forall aux. Elab' aux [Name]
get_deferred = do ES (ProofState, aux)
p String
_ Maybe (ElabState aux)
_ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
[Name] -> Elab' aux [Name]
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name] -> Elab' aux [Name]) -> [Name] -> Elab' aux [Name]
forall a b. (a -> b) -> a -> b
$! (ProofState -> [Name]
deferred ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p))
checkInjective :: (Term, Term, Term) -> Elab' aux ()
checkInjective :: forall aux. (TT Name, TT Name, TT Name) -> Elab' aux ()
checkInjective (TT Name
tm, TT Name
l, TT Name
r) = do Context
ctxt <- Elab' aux Context
forall aux. Elab' aux Context
get_context
if Context -> TT Name -> Bool
isInj Context
ctxt TT Name
tm then () -> Elab' aux ()
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> Elab' aux ()) -> () -> Elab' aux ()
forall a b. (a -> b) -> a -> b
$! ()
else TC () -> Elab' aux ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> Elab' aux ()) -> TC () -> Elab' aux ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (TT Name -> TT Name -> TT Name -> Err
forall t. t -> t -> t -> Err' t
NotInjective TT Name
tm TT Name
l TT Name
r)
where isInj :: Context -> TT Name -> Bool
isInj Context
ctxt (P NameType
_ Name
n TT Name
_)
| Name -> Context -> Bool
isConName Name
n Context
ctxt = Bool
True
isInj Context
ctxt (App AppStatus Name
_ TT Name
f TT Name
a) = Context -> TT Name -> Bool
isInj Context
ctxt TT Name
f
isInj Context
ctxt (Constant Const
_) = Bool
True
isInj Context
ctxt (TType UExp
_) = Bool
True
isInj Context
ctxt (Bind Name
_ (Pi RigCount
_ Maybe ImplicitInfo
_ TT Name
_ TT Name
_) TT Name
sc) = Bool
True
isInj Context
ctxt TT Name
_ = Bool
False
get_implementations :: Elab' aux [Name]
get_implementations :: forall aux. Elab' aux [Name]
get_implementations = do ES (ProofState, aux)
p String
_ Maybe (ElabState aux)
_ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
[Name] -> Elab' aux [Name]
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Name] -> Elab' aux [Name]) -> [Name] -> Elab' aux [Name]
forall a b. (a -> b) -> a -> b
$! (ProofState -> [Name]
implementations ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p))
get_autos :: Elab' aux [(Name, ([FailContext], [Name]))]
get_autos :: forall aux. Elab' aux [(Name, ([FailContext], [Name]))]
get_autos = do ES (ProofState, aux)
p String
_ Maybe (ElabState aux)
_ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
[(Name, ([FailContext], [Name]))]
-> Elab' aux [(Name, ([FailContext], [Name]))]
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, ([FailContext], [Name]))]
-> Elab' aux [(Name, ([FailContext], [Name]))])
-> [(Name, ([FailContext], [Name]))]
-> Elab' aux [(Name, ([FailContext], [Name]))]
forall a b. (a -> b) -> a -> b
$! (ProofState -> [(Name, ([FailContext], [Name]))]
autos ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p))
unique_hole :: Name -> Elab' aux Name
unique_hole :: forall aux. Name -> Elab' aux Name
unique_hole = Bool -> Name -> Elab' aux Name
forall aux. Bool -> Name -> Elab' aux Name
unique_hole' Bool
False
unique_hole' :: Bool -> Name -> Elab' aux Name
unique_hole' :: forall aux. Bool -> Name -> Elab' aux Name
unique_hole' Bool
reusable Name
n
= do ES (ProofState, aux)
p String
_ Maybe (ElabState aux)
_ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
let bs :: [Name]
bs = ProofTerm -> [Name]
bound_in (ProofState -> ProofTerm
pterm ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p)) [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++
TT Name -> [Name]
bound_in_term (ProofState -> TT Name
ptype ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p))
let nouse :: [Name]
nouse = ProofState -> [Name]
holes ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p) [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [Name]
bs [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ ProofState -> [Name]
dontunify ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p) [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ ProofState -> [Name]
usedns ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p)
Name
n' <- Name -> Elab' aux Name
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Elab' aux Name) -> Name -> Elab' aux Name
forall a b. (a -> b) -> a -> b
$! Context -> Name -> [Name] -> Name
uniqueNameCtxt (ProofState -> Context
context ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p)) Name
n [Name]
nouse
ES (ProofState
p, aux
a) String
s Maybe (ElabState aux)
u <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
case Name
n' of
MN Int
i Text
_ -> Bool
-> StateT (ElabState aux) TC () -> StateT (ElabState aux) TC ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= ProofState -> Int
nextname ProofState
p) (StateT (ElabState aux) TC () -> StateT (ElabState aux) TC ())
-> StateT (ElabState aux) TC () -> StateT (ElabState aux) TC ()
forall a b. (a -> b) -> a -> b
$
ElabState aux -> StateT (ElabState aux) TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
p { nextname = i + 1 }, aux
a) String
s Maybe (ElabState aux)
u)
Name
_ -> () -> StateT (ElabState aux) TC ()
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> StateT (ElabState aux) TC ())
-> () -> StateT (ElabState aux) TC ()
forall a b. (a -> b) -> a -> b
$! ()
Name -> Elab' aux Name
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Elab' aux Name) -> Name -> Elab' aux Name
forall a b. (a -> b) -> a -> b
$! Name
n'
elog :: String -> Elab' aux ()
elog :: forall aux. String -> Elab' aux ()
elog String
str = do ES (ProofState, aux)
p String
logs Maybe (ElabState aux)
prev <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
ElabState aux -> Elab' aux ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState, aux)
p (String
logs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
str String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n") Maybe (ElabState aux)
prev)
getLog :: Elab' aux String
getLog :: forall aux. Elab' aux String
getLog = do ES (ProofState, aux)
p String
logs Maybe (ElabState aux)
_ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
String -> Elab' aux String
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Elab' aux String) -> String -> Elab' aux String
forall a b. (a -> b) -> a -> b
$! String
logs
attack :: Elab' aux ()
attack :: forall aux. Elab' aux ()
attack = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' Tactic
Attack
claim :: Name -> Raw -> Elab' aux ()
claim :: forall aux. Name -> Raw -> Elab' aux ()
claim Name
n Raw
t = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Name -> Raw -> Tactic
Claim Name
n Raw
t)
claimFn :: Name -> Name -> Raw -> Elab' aux ()
claimFn :: forall aux. Name -> Name -> Raw -> Elab' aux ()
claimFn Name
n Name
bn Raw
t = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Name -> Name -> Raw -> Tactic
ClaimFn Name
n Name
bn Raw
t)
unifyGoal :: Raw -> Elab' aux ()
unifyGoal :: forall aux. Raw -> Elab' aux ()
unifyGoal Raw
t = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Raw -> Tactic
UnifyGoal Raw
t)
unifyTerms :: Raw -> Raw -> Elab' aux ()
unifyTerms :: forall aux. Raw -> Raw -> Elab' aux ()
unifyTerms Raw
t1 Raw
t2 = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Raw -> Raw -> Tactic
UnifyTerms Raw
t1 Raw
t2)
exact :: Raw -> Elab' aux ()
exact :: forall aux. Raw -> Elab' aux ()
exact Raw
t = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Raw -> Tactic
Exact Raw
t)
fill :: Raw -> Elab' aux ()
fill :: forall aux. Raw -> Elab' aux ()
fill Raw
t = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Raw -> Tactic
Fill Raw
t)
match_fill :: Raw -> Elab' aux ()
match_fill :: forall aux. Raw -> Elab' aux ()
match_fill Raw
t = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Raw -> Tactic
MatchFill Raw
t)
prep_fill :: Name -> [Name] -> Elab' aux ()
prep_fill :: forall aux. Name -> [Name] -> Elab' aux ()
prep_fill Name
n [Name]
ns = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Name -> [Name] -> Tactic
PrepFill Name
n [Name]
ns)
complete_fill :: Elab' aux ()
complete_fill :: forall aux. Elab' aux ()
complete_fill = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' Tactic
CompleteFill
solve :: Elab' aux ()
solve :: forall aux. Elab' aux ()
solve = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' Tactic
Solve
start_unify :: Name -> Elab' aux ()
start_unify :: forall aux. Name -> Elab' aux ()
start_unify Name
n = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Name -> Tactic
StartUnify Name
n)
end_unify :: Elab' aux ()
end_unify :: forall aux. Elab' aux ()
end_unify = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' Tactic
EndUnify
unify_all :: Elab' aux ()
unify_all :: forall aux. Elab' aux ()
unify_all = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' Tactic
UnifyAll
regret :: Elab' aux ()
regret :: forall aux. Elab' aux ()
regret = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' Tactic
Regret
compute :: Elab' aux ()
compute :: forall aux. Elab' aux ()
compute = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' Tactic
Compute
computeLet :: Name -> Elab' aux ()
computeLet :: forall aux. Name -> Elab' aux ()
computeLet Name
n = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Name -> Tactic
ComputeLet Name
n)
simplify :: Elab' aux ()
simplify :: forall aux. Elab' aux ()
simplify = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' Tactic
Simplify
whnf_compute :: Elab' aux ()
whnf_compute :: forall aux. Elab' aux ()
whnf_compute = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' Tactic
WHNF_Compute
whnf_compute_args :: Elab' aux ()
whnf_compute_args :: forall aux. Elab' aux ()
whnf_compute_args = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' Tactic
WHNF_ComputeArgs
eval_in :: Raw -> Elab' aux ()
eval_in :: forall aux. Raw -> Elab' aux ()
eval_in Raw
t = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Raw -> Tactic
EvalIn Raw
t)
check_in :: Raw -> Elab' aux ()
check_in :: forall aux. Raw -> Elab' aux ()
check_in Raw
t = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Raw -> Tactic
CheckIn Raw
t)
intro :: Maybe Name -> Elab' aux ()
intro :: forall aux. Maybe Name -> Elab' aux ()
intro Maybe Name
n = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Maybe Name -> Tactic
Intro Maybe Name
n)
introTy :: Raw -> Maybe Name -> Elab' aux ()
introTy :: forall aux. Raw -> Maybe Name -> Elab' aux ()
introTy Raw
ty Maybe Name
n = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Raw -> Maybe Name -> Tactic
IntroTy Raw
ty Maybe Name
n)
forAll :: Name -> RigCount -> Maybe ImplicitInfo -> Raw -> Elab' aux ()
forAll :: forall aux.
Name -> RigCount -> Maybe ImplicitInfo -> Raw -> Elab' aux ()
forAll Name
n RigCount
r Maybe ImplicitInfo
i Raw
t = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Name -> RigCount -> Maybe ImplicitInfo -> Raw -> Tactic
Forall Name
n RigCount
r Maybe ImplicitInfo
i Raw
t)
letbind :: Name -> RigCount -> Raw -> Raw -> Elab' aux ()
letbind :: forall aux. Name -> RigCount -> Raw -> Raw -> Elab' aux ()
letbind Name
n RigCount
rig Raw
t Raw
v = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Name -> RigCount -> Raw -> Raw -> Tactic
LetBind Name
n RigCount
rig Raw
t Raw
v)
expandLet :: Name -> Term -> Elab' aux ()
expandLet :: forall aux. Name -> TT Name -> Elab' aux ()
expandLet Name
n TT Name
v = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Name -> TT Name -> Tactic
ExpandLet Name
n TT Name
v)
rewrite :: Raw -> Elab' aux ()
rewrite :: forall aux. Raw -> Elab' aux ()
rewrite Raw
tm = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Raw -> Tactic
Rewrite Raw
tm)
equiv :: Raw -> Elab' aux ()
equiv :: forall aux. Raw -> Elab' aux ()
equiv Raw
tm = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Raw -> Tactic
Equiv Raw
tm)
patvar :: Name -> Elab' aux ()
patvar :: forall aux. Name -> Elab' aux ()
patvar n :: Name
n@(SN SpecialName
_) = do Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
forall aux. Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
apply (Name -> Raw
Var Name
n) []; Elab' aux ()
forall aux. Elab' aux ()
solve
patvar Name
n = do Env
env <- Elab' aux Env
forall aux. Elab' aux Env
get_env
[Name]
hs <- Elab' aux [Name]
forall aux. Elab' aux [Name]
get_holes
if (Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Name, RigCount, Binder (TT Name)) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name)) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
env) then do Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
forall aux. Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
apply (Name -> Raw
Var Name
n) []; Elab' aux ()
forall aux. Elab' aux ()
solve
else do Name
n' <- case [Name]
hs of
(Name
h : [Name]
hs) -> if Name
n Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
h then Name -> StateT (ElabState aux) TC Name
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
n
else Name -> StateT (ElabState aux) TC Name
forall aux. Name -> Elab' aux Name
unique_hole Name
n
[Name]
_ -> Name -> StateT (ElabState aux) TC Name
forall aux. Name -> Elab' aux Name
unique_hole Name
n
Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Name -> Tactic
PatVar Name
n)
patvar' :: Name -> Elab' aux ()
patvar' :: forall aux. Name -> Elab' aux ()
patvar' n :: Name
n@(SN SpecialName
_) = do Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
forall aux. Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
apply (Name -> Raw
Var Name
n) [] ; Elab' aux ()
forall aux. Elab' aux ()
solve
patvar' Name
n = do Env
env <- Elab' aux Env
forall aux. Elab' aux Env
get_env
[Name]
hs <- Elab' aux [Name]
forall aux. Elab' aux [Name]
get_holes
if (Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Name, RigCount, Binder (TT Name)) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name)) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
env) then do Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
forall aux. Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
apply (Name -> Raw
Var Name
n) [] ; Elab' aux ()
forall aux. Elab' aux ()
solve
else Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Name -> Tactic
PatVar Name
n)
patbind :: Name -> RigCount -> Elab' aux ()
patbind :: forall aux. Name -> RigCount -> Elab' aux ()
patbind Name
n RigCount
r = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Name -> RigCount -> Tactic
PatBind Name
n RigCount
r)
focus :: Name -> Elab' aux ()
focus :: forall aux. Name -> Elab' aux ()
focus Name
n = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Name -> Tactic
Focus Name
n)
movelast :: Name -> Elab' aux ()
movelast :: forall aux. Name -> Elab' aux ()
movelast Name
n = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Name -> Tactic
MoveLast Name
n)
dotterm :: Elab' aux ()
dotterm :: forall aux. Elab' aux ()
dotterm = do ES (ProofState
p, aux
a) String
s Maybe (ElabState aux)
m <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
TT Name
tm <- Elab' aux (TT Name)
forall aux. Elab' aux (TT Name)
get_term
case ProofState -> [Name]
holes ProofState
p of
[] -> () -> Elab' aux ()
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(Name
h : [Name]
hs) ->
do let outer :: [Name]
outer = Name -> [Name] -> TT Name -> [Name]
forall {a}. Eq a => a -> [a] -> TT a -> [a]
findOuter Name
h [] TT Name
tm
let p' :: ProofState
p' = ProofState
p { dotted = (h, outer) : dotted p }
ElabState aux -> Elab' aux ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (ElabState aux -> Elab' aux ()) -> ElabState aux -> Elab' aux ()
forall a b. (a -> b) -> a -> b
$ (ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
p', aux
a) String
s Maybe (ElabState aux)
m
where
findOuter :: a -> [a] -> TT a -> [a]
findOuter a
h [a]
env (P NameType
_ a
n TT a
_) | a
h a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
n = [a]
env
findOuter a
h [a]
env (Bind a
n Binder (TT a)
b TT a
sc)
= [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
union (Binder (TT a) -> [a]
foB Binder (TT a)
b)
(a -> [a] -> TT a -> [a]
findOuter a
h [a]
env (TT a -> TT a -> TT a
forall n. TT n -> TT n -> TT n
instantiate (NameType -> a -> TT a -> TT a
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound a
n (Binder (TT a) -> TT a
forall b. Binder b -> b
binderTy Binder (TT a)
b)) TT a
sc))
where foB :: Binder (TT a) -> [a]
foB (Guess TT a
t TT a
v) = [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
union (a -> [a] -> TT a -> [a]
findOuter a
h [a]
env TT a
t) (a -> [a] -> TT a -> [a]
findOuter a
h (a
na -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
env) TT a
v)
foB (Let RigCount
_ TT a
t TT a
v) = [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
union (a -> [a] -> TT a -> [a]
findOuter a
h [a]
env TT a
t) (a -> [a] -> TT a -> [a]
findOuter a
h [a]
env TT a
v)
foB Binder (TT a)
b = a -> [a] -> TT a -> [a]
findOuter a
h [a]
env (Binder (TT a) -> TT a
forall b. Binder b -> b
binderTy Binder (TT a)
b)
findOuter a
h [a]
env (App AppStatus a
_ TT a
f TT a
a)
= [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
union (a -> [a] -> TT a -> [a]
findOuter a
h [a]
env TT a
f) (a -> [a] -> TT a -> [a]
findOuter a
h [a]
env TT a
a)
findOuter a
h [a]
env TT a
_ = []
get_dotterm :: Elab' aux [(Name, [Name])]
get_dotterm :: forall aux. Elab' aux [(Name, [Name])]
get_dotterm = do ES (ProofState
p, aux
a) String
s Maybe (ElabState aux)
m <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
[(Name, [Name])] -> Elab' aux [(Name, [Name])]
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofState -> [(Name, [Name])]
dotted ProofState
p)
zipHere :: Elab' aux ()
zipHere :: forall aux. Elab' aux ()
zipHere = do ES (ProofState
ps, aux
a) String
s Maybe (ElabState aux)
m <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
let pt' :: ProofTerm
pt' = Maybe Name -> ProofTerm -> ProofTerm
refocus (Name -> Maybe Name
forall a. a -> Maybe a
Just ([Name] -> Name
forall a. HasCallStack => [a] -> a
head (ProofState -> [Name]
holes ProofState
ps))) (ProofState -> ProofTerm
pterm ProofState
ps)
ElabState aux -> Elab' aux ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
ps { pterm = pt' }, aux
a) String
s Maybe (ElabState aux)
m)
matchProblems :: Bool -> Elab' aux ()
matchProblems :: forall aux. Bool -> Elab' aux ()
matchProblems Bool
all = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Bool -> Tactic
MatchProblems Bool
all)
unifyProblems :: Elab' aux ()
unifyProblems :: forall aux. Elab' aux ()
unifyProblems = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' Tactic
UnifyProblems
defer :: [Name] -> [Name] -> Name -> Elab' aux Name
defer :: forall aux. [Name] -> [Name] -> Name -> Elab' aux Name
defer [Name]
ds [Name]
ls Name
n
= do Name
n' <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
unique_hole Name
n
Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' ([Name] -> [Name] -> Name -> Tactic
Defer [Name]
ds [Name]
ls Name
n')
Name -> Elab' aux Name
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Name
n'
deferType :: Name -> Raw -> [Name] -> Elab' aux ()
deferType :: forall aux. Name -> Raw -> [Name] -> Elab' aux ()
deferType Name
n Raw
ty [Name]
ns = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Name -> Raw -> [Name] -> Tactic
DeferType Name
n Raw
ty [Name]
ns)
implementationArg :: Name -> Elab' aux ()
implementationArg :: forall aux. Name -> Elab' aux ()
implementationArg Name
n = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Name -> Tactic
Implementation Name
n)
autoArg :: Name -> Elab' aux ()
autoArg :: forall aux. Name -> Elab' aux ()
autoArg Name
n = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Name -> Tactic
AutoArg Name
n)
setinj :: Name -> Elab' aux ()
setinj :: forall aux. Name -> Elab' aux ()
setinj Name
n = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Name -> Tactic
SetInjective Name
n)
proofstate :: Elab' aux ()
proofstate :: forall aux. Elab' aux ()
proofstate = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' Tactic
ProofState
reorder_claims :: Name -> Elab' aux ()
reorder_claims :: forall aux. Name -> Elab' aux ()
reorder_claims Name
n = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' (Name -> Tactic
Reorder Name
n)
qed :: Elab' aux Term
qed :: forall aux. Elab' aux (TT Name)
qed = do Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' Tactic
QED
ES (ProofState, aux)
p String
_ Maybe (ElabState aux)
_ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
TT Name -> Elab' aux (TT Name)
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> Elab' aux (TT Name)) -> TT Name -> Elab' aux (TT Name)
forall a b. (a -> b) -> a -> b
$! (ProofTerm -> TT Name
getProofTerm (ProofState -> ProofTerm
pterm ((ProofState, aux) -> ProofState
forall a b. (a, b) -> a
fst (ProofState, aux)
p)))
undo :: Elab' aux ()
undo :: forall aux. Elab' aux ()
undo = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' Tactic
Undo
prepare_apply :: Raw
-> [Bool]
-> Elab' aux [(Name, Name)]
prepare_apply :: forall aux. Raw -> [Bool] -> Elab' aux [(Name, Name)]
prepare_apply Raw
fn [Bool]
imps =
do TT Name
ty <- Raw -> Elab' aux (TT Name)
forall aux. Raw -> Elab' aux (TT Name)
get_type Raw
fn
Context
ctxt <- Elab' aux Context
forall aux. Elab' aux Context
get_context
Env
env <- Elab' aux Env
forall aux. Elab' aux Env
get_env
let usety :: TT Name
usety = if TT Name -> [Bool] -> Bool
forall a. TT Name -> [a] -> Bool
argsOK (TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
ty) [Bool]
imps
then TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
ty
else Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env (TT Name -> TT Name
forall n. Eq n => TT n -> TT n
finalise TT Name
ty)
[(Name, Name)]
claims <-
TT Name
-> [Bool] -> [(Name, Name)] -> [Name] -> Elab' aux [(Name, Name)]
forall aux.
TT Name
-> [Bool] -> [(Name, Name)] -> [Name] -> Elab' aux [(Name, Name)]
mkClaims TT Name
usety [Bool]
imps [] (((Name, RigCount, Binder (TT Name)) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name)) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
env)
ES (ProofState
p, aux
a) String
s Maybe (ElabState aux)
prev <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
let n :: Int
n = [Bool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Bool -> Bool) -> [Bool] -> [Bool]
forall a. (a -> Bool) -> [a] -> [a]
filter Bool -> Bool
not [Bool]
imps)
let (Name
h : [Name]
hs) = ProofState -> [Name]
holes ProofState
p
ElabState aux -> StateT (ElabState aux) TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
p { holes = h : (reverse (take n hs) ++ drop n hs) }, aux
a) String
s Maybe (ElabState aux)
prev)
[(Name, Name)] -> Elab' aux [(Name, Name)]
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, Name)] -> Elab' aux [(Name, Name)])
-> [(Name, Name)] -> Elab' aux [(Name, Name)]
forall a b. (a -> b) -> a -> b
$! [(Name, Name)]
claims
where
argsOK :: Type -> [a] -> Bool
argsOK :: forall a. TT Name -> [a] -> Bool
argsOK (Bind Name
n (Pi RigCount
_ Maybe ImplicitInfo
_ TT Name
_ TT Name
_) TT Name
sc) (a
i : [a]
is) = TT Name -> [a] -> Bool
forall a. TT Name -> [a] -> Bool
argsOK TT Name
sc [a]
is
argsOK TT Name
_ (a
i : [a]
is) = Bool
False
argsOK TT Name
_ [] = Bool
True
mkClaims :: Type
-> [Bool]
-> [(Name, Name)]
-> [Name]
-> Elab' aux [(Name, Name)]
mkClaims :: forall aux.
TT Name
-> [Bool] -> [(Name, Name)] -> [Name] -> Elab' aux [(Name, Name)]
mkClaims (Bind Name
n' (Pi RigCount
_ Maybe ImplicitInfo
_ TT Name
t_in TT Name
_) TT Name
sc) (Bool
i : [Bool]
is) [(Name, Name)]
claims [Name]
hs =
do let t :: TT Name
t = [Name] -> TT Name -> TT Name
rebind [Name]
hs TT Name
t_in
Name
n <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
getNameFrom (Name -> Name
mkMN Name
n')
let sc' :: TT Name
sc' = TT Name -> TT Name -> TT Name
forall n. TT n -> TT n -> TT n
instantiate (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n TT Name
t) TT Name
sc
Env
env <- Elab' aux Env
forall aux. Elab' aux Env
get_env
Name -> Raw -> Elab' aux ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
n ([Name] -> TT Name -> Raw
forgetEnv (((Name, RigCount, Binder (TT Name)) -> Name) -> Env -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, RigCount, Binder (TT Name)) -> Name
forall {a} {b} {c}. (a, b, c) -> a
fstEnv Env
env) TT Name
t)
Bool -> Elab' aux () -> Elab' aux ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
i (Name -> Elab' aux ()
forall aux. Name -> Elab' aux ()
movelast Name
n)
TT Name
-> [Bool] -> [(Name, Name)] -> [Name] -> Elab' aux [(Name, Name)]
forall aux.
TT Name
-> [Bool] -> [(Name, Name)] -> [Name] -> Elab' aux [(Name, Name)]
mkClaims TT Name
sc' [Bool]
is ((Name
n', Name
n) (Name, Name) -> [(Name, Name)] -> [(Name, Name)]
forall a. a -> [a] -> [a]
: [(Name, Name)]
claims) [Name]
hs
mkClaims TT Name
t [] [(Name, Name)]
claims [Name]
_ = [(Name, Name)] -> Elab' aux [(Name, Name)]
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, Name)] -> Elab' aux [(Name, Name)])
-> [(Name, Name)] -> Elab' aux [(Name, Name)]
forall a b. (a -> b) -> a -> b
$! ([(Name, Name)] -> [(Name, Name)]
forall a. [a] -> [a]
reverse [(Name, Name)]
claims)
mkClaims TT Name
_ [Bool]
_ [(Name, Name)]
_ [Name]
_
| Var Name
n <- Raw
fn
= do Context
ctxt <- Elab' aux Context
forall aux. Elab' aux Context
get_context
TC [(Name, Name)] -> Elab' aux [(Name, Name)]
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC [(Name, Name)] -> Elab' aux [(Name, Name)])
-> TC [(Name, Name)] -> Elab' aux [(Name, Name)]
forall a b. (a -> b) -> a -> b
$ Err -> TC [(Name, Name)]
forall a. Err -> TC a
tfail (Err -> TC [(Name, Name)]) -> Err -> TC [(Name, Name)]
forall a b. (a -> b) -> a -> b
$ Name -> Err
forall t. Name -> Err' t
TooManyArguments Name
n
| Bool
otherwise = String -> Elab' aux [(Name, Name)]
forall a. String -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> Elab' aux [(Name, Name)])
-> String -> Elab' aux [(Name, Name)]
forall a b. (a -> b) -> a -> b
$ String
"Too many arguments for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Raw -> String
forall a. Show a => a -> String
show Raw
fn
mkMN :: Name -> Name
mkMN n :: Name
n@(MN Int
i Text
_) = Name
n
mkMN n :: Name
n@(UN Text
x) = Int -> Text -> Name
MN Int
99999 Text
x
mkMN n :: Name
n@(SN SpecialName
s) = Int -> String -> Name
sMN Int
99999 (SpecialName -> String
forall a. Show a => a -> String
show SpecialName
s)
mkMN (NS Name
n [Text]
xs) = Name -> [Text] -> Name
NS (Name -> Name
mkMN Name
n) [Text]
xs
rebind :: [Name] -> TT Name -> TT Name
rebind [Name]
hs (Bind Name
n Binder (TT Name)
t TT Name
sc)
| Name
n Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
hs = let n' :: Name
n' = Name -> [Name] -> Name
uniqueName Name
n [Name]
hs in
Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n' ((TT Name -> TT Name) -> Binder (TT Name) -> Binder (TT Name)
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Name] -> TT Name -> TT Name
rebind [Name]
hs) Binder (TT Name)
t) ([Name] -> TT Name -> TT Name
rebind (Name
n'Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
hs) TT Name
sc)
| Bool
otherwise = Name -> Binder (TT Name) -> TT Name -> TT Name
forall n. n -> Binder (TT n) -> TT n -> TT n
Bind Name
n ((TT Name -> TT Name) -> Binder (TT Name) -> Binder (TT Name)
forall a b. (a -> b) -> Binder a -> Binder b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Name] -> TT Name -> TT Name
rebind [Name]
hs) Binder (TT Name)
t) ([Name] -> TT Name -> TT Name
rebind (Name
nName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
hs) TT Name
sc)
rebind [Name]
hs (App AppStatus Name
s TT Name
f TT Name
a) = AppStatus Name -> TT Name -> TT Name -> TT Name
forall n. AppStatus n -> TT n -> TT n -> TT n
App AppStatus Name
s ([Name] -> TT Name -> TT Name
rebind [Name]
hs TT Name
f) ([Name] -> TT Name -> TT Name
rebind [Name]
hs TT Name
a)
rebind [Name]
hs TT Name
t = TT Name
t
apply, match_apply :: Raw
-> [(Bool, Int)]
-> Elab' aux [(Name, Name)]
apply :: forall aux. Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
apply = (Raw -> Elab' aux ())
-> Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
forall aux.
(Raw -> Elab' aux ())
-> Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
apply' Raw -> Elab' aux ()
forall aux. Raw -> Elab' aux ()
fill
match_apply :: forall aux. Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
match_apply = (Raw -> Elab' aux ())
-> Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
forall aux.
(Raw -> Elab' aux ())
-> Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
apply' Raw -> Elab' aux ()
forall aux. Raw -> Elab' aux ()
match_fill
apply' :: (Raw -> Elab' aux ()) -> Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
apply' :: forall aux.
(Raw -> Elab' aux ())
-> Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]
apply' Raw -> Elab' aux ()
fillt Raw
fn [(Bool, Int)]
imps =
do [(Name, Name)]
args <- Raw -> [Bool] -> Elab' aux [(Name, Name)]
forall aux. Raw -> [Bool] -> Elab' aux [(Name, Name)]
prepare_apply Raw
fn (((Bool, Int) -> Bool) -> [(Bool, Int)] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Bool, Int) -> Bool
forall a b. (a, b) -> a
fst [(Bool, Int)]
imps)
[Name]
hs <- Elab' aux [Name]
forall aux. Elab' aux [Name]
get_holes
ES (ProofState
p, aux
a) String
s Maybe (ElabState aux)
prev <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
let dont :: [Name]
dont = if [(Bool, Int)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Bool, Int)]
imps
then [Name] -> Name
forall a. HasCallStack => [a] -> a
head [Name]
hs Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: ProofState -> [Name]
dontunify ProofState
p
else [Name] -> [(Bool, Int)] -> [(Name, Name)] -> [Name]
forall {a} {b} {a}. [a] -> [(Bool, b)] -> [(a, a)] -> [a]
getNonUnify ([Name] -> Name
forall a. HasCallStack => [a] -> a
head [Name]
hs Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: ProofState -> [Name]
dontunify ProofState
p) [(Bool, Int)]
imps [(Name, Name)]
args
let (Name
n, [(Name, TT Name)]
hunis) =
ProofState -> (Name, [(Name, TT Name)])
unified ProofState
p
let unify :: [(Name, TT Name)]
unify =
[Name] -> [(Name, TT Name)] -> [Name] -> [(Name, TT Name)]
forall {a} {t1 :: * -> *} {t2 :: * -> *}.
(Eq a, Foldable t1, Foldable t2) =>
t1 a -> [(a, TT a)] -> t2 a -> [(a, TT a)]
dropGiven [Name]
dont [(Name, TT Name)]
hunis [Name]
hs
let notunify :: [(Name, TT Name)]
notunify =
[Name] -> [(Name, TT Name)] -> [Name] -> [(Name, TT Name)]
forall {a} {t1 :: * -> *} {t2 :: * -> *}.
(Eq a, Foldable t1, Foldable t2) =>
t1 a -> [(a, TT a)] -> t2 a -> [(a, TT a)]
keepGiven [Name]
dont [(Name, TT Name)]
hunis [Name]
hs
ElabState aux -> Elab' aux ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
p { dontunify = dont, unified = (n, unify),
notunified = notunify ++ notunified p }, aux
a) String
s Maybe (ElabState aux)
prev)
Raw -> Elab' aux ()
fillt (Raw -> [Raw] -> Raw
raw_apply Raw
fn (((Name, Name) -> Raw) -> [(Name, Name)] -> [Raw]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Raw
Var (Name -> Raw) -> ((Name, Name) -> Name) -> (Name, Name) -> Raw
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Name) -> Name
forall a b. (a, b) -> b
snd) [(Name, Name)]
args))
Bool
ulog <- Elab' aux Bool
forall aux. Elab' aux Bool
getUnifyLog
TT Name
g <- Elab' aux (TT Name)
forall aux. Elab' aux (TT Name)
goal
Bool -> String -> Elab' aux () -> Elab' aux ()
forall {a}. Bool -> String -> a -> a
traceWhen Bool
ulog
(String
"Goal " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TT Name -> String
forall a. Show a => a -> String
show TT Name
g String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -- when elaborating " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Raw -> String
forall a. Show a => a -> String
show Raw
fn)
Elab' aux ()
forall aux. Elab' aux ()
end_unify
[(Name, Name)] -> Elab' aux [(Name, Name)]
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, Name)] -> Elab' aux [(Name, Name)])
-> [(Name, Name)] -> Elab' aux [(Name, Name)]
forall a b. (a -> b) -> a -> b
$! (((Name, Name) -> (Name, Name)) -> [(Name, Name)] -> [(Name, Name)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
argName, Name
argHole) -> (Name
argName, [(Name, TT Name)] -> Name -> Name
forall {n}. Eq n => [(n, TT n)] -> n -> n
updateUnify [(Name, TT Name)]
unify Name
argHole)) [(Name, Name)]
args)
where updateUnify :: [(n, TT n)] -> n -> n
updateUnify [(n, TT n)]
us n
n = case n -> [(n, TT n)] -> Maybe (TT n)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup n
n [(n, TT n)]
us of
Just (P NameType
_ n
t TT n
_) -> n
t
Maybe (TT n)
_ -> n
n
getNonUnify :: [a] -> [(Bool, b)] -> [(a, a)] -> [a]
getNonUnify [a]
acc [] [(a, a)]
_ = [a]
acc
getNonUnify [a]
acc [(Bool, b)]
_ [] = [a]
acc
getNonUnify [a]
acc ((Bool
i,b
_):[(Bool, b)]
is) ((a
a, a
t):[(a, a)]
as)
| Bool
i = [a] -> [(Bool, b)] -> [(a, a)] -> [a]
getNonUnify [a]
acc [(Bool, b)]
is [(a, a)]
as
| Bool
otherwise = [a] -> [(Bool, b)] -> [(a, a)] -> [a]
getNonUnify (a
t a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
acc) [(Bool, b)]
is [(a, a)]
as
apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()
apply2 :: forall aux. Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()
apply2 Raw
fn [Maybe (Elab' aux ())]
elabs =
do [(Name, Name)]
args <- Raw -> [Bool] -> Elab' aux [(Name, Name)]
forall aux. Raw -> [Bool] -> Elab' aux [(Name, Name)]
prepare_apply Raw
fn ((Maybe (Elab' aux ()) -> Bool) -> [Maybe (Elab' aux ())] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map Maybe (Elab' aux ()) -> Bool
forall {a}. Maybe a -> Bool
isJust [Maybe (Elab' aux ())]
elabs)
Raw -> Elab' aux ()
forall aux. Raw -> Elab' aux ()
fill (Raw -> [Raw] -> Raw
raw_apply Raw
fn (((Name, Name) -> Raw) -> [(Name, Name)] -> [Raw]
forall a b. (a -> b) -> [a] -> [b]
map (Name -> Raw
Var (Name -> Raw) -> ((Name, Name) -> Name) -> (Name, Name) -> Raw
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, Name) -> Name
forall a b. (a, b) -> b
snd) [(Name, Name)]
args))
[Name] -> [Maybe (Elab' aux ())] -> Elab' aux ()
forall {aux} {a}.
[Name]
-> [Maybe (StateT (ElabState aux) TC a)]
-> StateT (ElabState aux) TC ()
elabArgs (((Name, Name) -> Name) -> [(Name, Name)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Name) -> Name
forall a b. (a, b) -> b
snd [(Name, Name)]
args) [Maybe (Elab' aux ())]
elabs
ES (ProofState
p, aux
a) String
s Maybe (ElabState aux)
prev <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
Elab' aux ()
forall aux. Elab' aux ()
end_unify
Elab' aux ()
forall aux. Elab' aux ()
solve
where elabArgs :: [Name]
-> [Maybe (StateT (ElabState aux) TC a)]
-> StateT (ElabState aux) TC ()
elabArgs [] [] = () -> StateT (ElabState aux) TC ()
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> StateT (ElabState aux) TC ())
-> () -> StateT (ElabState aux) TC ()
forall a b. (a -> b) -> a -> b
$! ()
elabArgs (Name
n:[Name]
ns) (Just StateT (ElabState aux) TC a
e:[Maybe (StateT (ElabState aux) TC a)]
es) = do Name -> StateT (ElabState aux) TC ()
forall aux. Name -> Elab' aux ()
focus Name
n; StateT (ElabState aux) TC a
e
[Name]
-> [Maybe (StateT (ElabState aux) TC a)]
-> StateT (ElabState aux) TC ()
elabArgs [Name]
ns [Maybe (StateT (ElabState aux) TC a)]
es
elabArgs (Name
n:[Name]
ns) (Maybe (StateT (ElabState aux) TC a)
_:[Maybe (StateT (ElabState aux) TC a)]
es) = [Name]
-> [Maybe (StateT (ElabState aux) TC a)]
-> StateT (ElabState aux) TC ()
elabArgs [Name]
ns [Maybe (StateT (ElabState aux) TC a)]
es
isJust :: Maybe a -> Bool
isJust (Just a
_) = Bool
False
isJust Maybe a
_ = Bool
True
apply_elab :: Name -> [Maybe (Int, Elab' aux ())] -> Elab' aux ()
apply_elab :: forall aux. Name -> [Maybe (Int, Elab' aux ())] -> Elab' aux ()
apply_elab Name
n [Maybe (Int, Elab' aux ())]
args =
do TT Name
ty <- Raw -> Elab' aux (TT Name)
forall aux. Raw -> Elab' aux (TT Name)
get_type (Name -> Raw
Var Name
n)
Context
ctxt <- Elab' aux Context
forall aux. Elab' aux Context
get_context
Env
env <- Elab' aux Env
forall aux. Elab' aux Env
get_env
[(Name, Maybe (Int, Elab' aux ()))]
claims <- TT Name
-> [Maybe (Int, Elab' aux ())]
-> [(Name, Maybe (Int, Elab' aux ()))]
-> StateT (ElabState aux) TC [(Name, Maybe (Int, Elab' aux ()))]
forall {a} {aux}.
TT Name
-> [Maybe a]
-> [(Name, Maybe a)]
-> StateT (ElabState aux) TC [(Name, Maybe a)]
doClaims (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
ty) [Maybe (Int, Elab' aux ())]
args []
Name -> [Name] -> Elab' aux ()
forall aux. Name -> [Name] -> Elab' aux ()
prep_fill Name
n (((Name, Maybe (Int, Elab' aux ())) -> Name)
-> [(Name, Maybe (Int, Elab' aux ()))] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Name, Maybe (Int, Elab' aux ())) -> Name
forall a b. (a, b) -> a
fst [(Name, Maybe (Int, Elab' aux ()))]
claims)
[(Name, Maybe (Int, Elab' aux ()))]
-> Bool -> [(Name, Maybe (Int, Elab' aux ()))] -> Elab' aux ()
forall {a} {aux} {a}.
[(Name, Maybe (a, StateT (ElabState aux) TC a))]
-> Bool
-> [(Name, Maybe (a, StateT (ElabState aux) TC a))]
-> StateT (ElabState aux) TC ()
elabClaims [] Bool
False [(Name, Maybe (Int, Elab' aux ()))]
claims
Elab' aux ()
forall aux. Elab' aux ()
complete_fill
Elab' aux ()
forall aux. Elab' aux ()
end_unify
where
doClaims :: TT Name
-> [Maybe a]
-> [(Name, Maybe a)]
-> StateT (ElabState aux) TC [(Name, Maybe a)]
doClaims (Bind Name
n' (Pi RigCount
_ Maybe ImplicitInfo
_ TT Name
t TT Name
_) TT Name
sc) (Maybe a
i : [Maybe a]
is) [(Name, Maybe a)]
claims =
do Name
n <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
unique_hole (Name -> Name
mkMN Name
n')
Bool
-> StateT (ElabState aux) TC () -> StateT (ElabState aux) TC ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([(Name, Maybe a)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, Maybe a)]
claims) (Name -> StateT (ElabState aux) TC ()
forall aux. Name -> Elab' aux ()
start_unify Name
n)
let sc' :: TT Name
sc' = TT Name -> TT Name -> TT Name
forall n. TT n -> TT n -> TT n
instantiate (NameType -> Name -> TT Name -> TT Name
forall n. NameType -> n -> TT n -> TT n
P NameType
Bound Name
n TT Name
t) TT Name
sc
Name -> Raw -> StateT (ElabState aux) TC ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
n (TT Name -> Raw
forget TT Name
t)
case Maybe a
i of
Maybe a
Nothing -> () -> StateT (ElabState aux) TC ()
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> StateT (ElabState aux) TC ())
-> () -> StateT (ElabState aux) TC ()
forall a b. (a -> b) -> a -> b
$! ()
Just a
_ ->
do ES (ProofState
p, aux
a) String
s Maybe (ElabState aux)
prev <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
ElabState aux -> StateT (ElabState aux) TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ((ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
forall aux.
(ProofState, aux)
-> String -> Maybe (ElabState aux) -> ElabState aux
ES (ProofState
p { dontunify = n : dontunify p }, aux
a) String
s Maybe (ElabState aux)
prev)
TT Name
-> [Maybe a]
-> [(Name, Maybe a)]
-> StateT (ElabState aux) TC [(Name, Maybe a)]
doClaims TT Name
sc' [Maybe a]
is ((Name
n, Maybe a
i) (Name, Maybe a) -> [(Name, Maybe a)] -> [(Name, Maybe a)]
forall a. a -> [a] -> [a]
: [(Name, Maybe a)]
claims)
doClaims TT Name
t [] [(Name, Maybe a)]
claims = [(Name, Maybe a)] -> StateT (ElabState aux) TC [(Name, Maybe a)]
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Name, Maybe a)] -> StateT (ElabState aux) TC [(Name, Maybe a)])
-> [(Name, Maybe a)] -> StateT (ElabState aux) TC [(Name, Maybe a)]
forall a b. (a -> b) -> a -> b
$! ([(Name, Maybe a)] -> [(Name, Maybe a)]
forall a. [a] -> [a]
reverse [(Name, Maybe a)]
claims)
doClaims TT Name
_ [Maybe a]
_ [(Name, Maybe a)]
_ = String -> StateT (ElabState aux) TC [(Name, Maybe a)]
forall a. String -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail (String -> StateT (ElabState aux) TC [(Name, Maybe a)])
-> String -> StateT (ElabState aux) TC [(Name, Maybe a)]
forall a b. (a -> b) -> a -> b
$ String
"Wrong number of arguments for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
n
elabClaims :: [(Name, Maybe (a, StateT (ElabState aux) TC a))]
-> Bool
-> [(Name, Maybe (a, StateT (ElabState aux) TC a))]
-> StateT (ElabState aux) TC ()
elabClaims [(Name, Maybe (a, StateT (ElabState aux) TC a))]
failed Bool
r []
| [(Name, Maybe (a, StateT (ElabState aux) TC a))] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Name, Maybe (a, StateT (ElabState aux) TC a))]
failed = () -> StateT (ElabState aux) TC ()
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> StateT (ElabState aux) TC ())
-> () -> StateT (ElabState aux) TC ()
forall a b. (a -> b) -> a -> b
$! ()
| Bool
otherwise = if Bool
r then [(Name, Maybe (a, StateT (ElabState aux) TC a))]
-> Bool
-> [(Name, Maybe (a, StateT (ElabState aux) TC a))]
-> StateT (ElabState aux) TC ()
elabClaims [] Bool
False [(Name, Maybe (a, StateT (ElabState aux) TC a))]
failed
else () -> StateT (ElabState aux) TC ()
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> StateT (ElabState aux) TC ())
-> () -> StateT (ElabState aux) TC ()
forall a b. (a -> b) -> a -> b
$! ()
elabClaims [(Name, Maybe (a, StateT (ElabState aux) TC a))]
failed Bool
r ((Name
n, Maybe (a, StateT (ElabState aux) TC a)
Nothing) : [(Name, Maybe (a, StateT (ElabState aux) TC a))]
xs) = [(Name, Maybe (a, StateT (ElabState aux) TC a))]
-> Bool
-> [(Name, Maybe (a, StateT (ElabState aux) TC a))]
-> StateT (ElabState aux) TC ()
elabClaims [(Name, Maybe (a, StateT (ElabState aux) TC a))]
failed Bool
r [(Name, Maybe (a, StateT (ElabState aux) TC a))]
xs
elabClaims [(Name, Maybe (a, StateT (ElabState aux) TC a))]
failed Bool
r (e :: (Name, Maybe (a, StateT (ElabState aux) TC a))
e@(Name
n, Just (a
_, StateT (ElabState aux) TC a
elaboration)) : [(Name, Maybe (a, StateT (ElabState aux) TC a))]
xs)
| Bool
r = StateT (ElabState aux) TC ()
-> StateT (ElabState aux) TC () -> StateT (ElabState aux) TC ()
forall aux a. Elab' aux a -> Elab' aux a -> Elab' aux a
try (do ES (ProofState, aux)
p String
_ Maybe (ElabState aux)
_ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
Name -> StateT (ElabState aux) TC ()
forall aux. Name -> Elab' aux ()
focus Name
n; StateT (ElabState aux) TC a
elaboration; [(Name, Maybe (a, StateT (ElabState aux) TC a))]
-> Bool
-> [(Name, Maybe (a, StateT (ElabState aux) TC a))]
-> StateT (ElabState aux) TC ()
elabClaims [(Name, Maybe (a, StateT (ElabState aux) TC a))]
failed Bool
r [(Name, Maybe (a, StateT (ElabState aux) TC a))]
xs)
([(Name, Maybe (a, StateT (ElabState aux) TC a))]
-> Bool
-> [(Name, Maybe (a, StateT (ElabState aux) TC a))]
-> StateT (ElabState aux) TC ()
elabClaims ((Name, Maybe (a, StateT (ElabState aux) TC a))
e (Name, Maybe (a, StateT (ElabState aux) TC a))
-> [(Name, Maybe (a, StateT (ElabState aux) TC a))]
-> [(Name, Maybe (a, StateT (ElabState aux) TC a))]
forall a. a -> [a] -> [a]
: [(Name, Maybe (a, StateT (ElabState aux) TC a))]
failed) Bool
r [(Name, Maybe (a, StateT (ElabState aux) TC a))]
xs)
| Bool
otherwise = do ES (ProofState, aux)
p String
_ Maybe (ElabState aux)
_ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
Name -> StateT (ElabState aux) TC ()
forall aux. Name -> Elab' aux ()
focus Name
n; StateT (ElabState aux) TC a
elaboration; [(Name, Maybe (a, StateT (ElabState aux) TC a))]
-> Bool
-> [(Name, Maybe (a, StateT (ElabState aux) TC a))]
-> StateT (ElabState aux) TC ()
elabClaims [(Name, Maybe (a, StateT (ElabState aux) TC a))]
failed Bool
r [(Name, Maybe (a, StateT (ElabState aux) TC a))]
xs
mkMN :: Name -> Name
mkMN n :: Name
n@(MN Int
_ Text
_) = Name
n
mkMN n :: Name
n@(UN Text
x) = Int -> Text -> Name
MN Int
0 Text
x
mkMN (NS Name
n [Text]
ns) = Name -> [Text] -> Name
NS (Name -> Name
mkMN Name
n) [Text]
ns
checkPiGoal :: Name -> Elab' aux ()
checkPiGoal :: forall aux. Name -> Elab' aux ()
checkPiGoal Name
n
= do TT Name
g <- Elab' aux (TT Name)
forall aux. Elab' aux (TT Name)
goal
Context
ctxt <- Elab' aux Context
forall aux. Elab' aux Context
get_context
Env
env <- Elab' aux Env
forall aux. Elab' aux Env
get_env
case (Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
g) of
Bind Name
_ (Pi RigCount
_ Maybe ImplicitInfo
_ TT Name
_ TT Name
_) TT Name
_ -> () -> Elab' aux ()
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
TT Name
_ -> do Name
a <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"__pargTy")
Name
b <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"__pretTy")
Name
f <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"pf")
Name -> Raw -> Elab' aux ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
a Raw
RType
Name -> Raw -> Elab' aux ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
b Raw
RType
Name -> Raw -> Elab' aux ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
f (Name -> Binder Raw -> Raw -> Raw
RBind Name
n (RigCount -> Maybe ImplicitInfo -> Raw -> Raw -> Binder Raw
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW Maybe ImplicitInfo
forall a. Maybe a
Nothing (Name -> Raw
Var Name
a) Raw
RType) (Name -> Raw
Var Name
b))
Name -> Elab' aux ()
forall aux. Name -> Elab' aux ()
movelast Name
a
Name -> Elab' aux ()
forall aux. Name -> Elab' aux ()
movelast Name
b
Raw -> Elab' aux ()
forall aux. Raw -> Elab' aux ()
fill (Name -> Raw
Var Name
f)
Elab' aux ()
forall aux. Elab' aux ()
solve
Name -> Elab' aux ()
forall aux. Name -> Elab' aux ()
focus Name
f
simple_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
simple_app :: forall aux.
Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
simple_app Bool
infer Elab' aux ()
fun Elab' aux ()
arg String
str =
Elab' aux () -> Elab' aux () -> Elab' aux ()
forall aux a. Elab' aux a -> Elab' aux a -> Elab' aux a
try (Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
forall aux. Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
dep_app Elab' aux ()
fun Elab' aux ()
arg String
str)
(Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
forall aux.
Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
infer_app Bool
infer Elab' aux ()
fun Elab' aux ()
arg String
str)
infer_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
infer_app :: forall aux.
Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
infer_app Bool
infer Elab' aux ()
fun Elab' aux ()
arg String
str =
do Name
a <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"__argTy")
Name
b <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"__retTy")
Name
f <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"f")
Name
s <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"is")
Name -> Raw -> Elab' aux ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
a Raw
RType
Name -> Raw -> Elab' aux ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
b Raw
RType
Name -> Raw -> Elab' aux ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
f (Name -> Binder Raw -> Raw -> Raw
RBind (Int -> String -> Name
sMN Int
0 String
"_aX") (RigCount -> Maybe ImplicitInfo -> Raw -> Raw -> Binder Raw
forall b. RigCount -> Maybe ImplicitInfo -> b -> b -> Binder b
Pi RigCount
RigW Maybe ImplicitInfo
forall a. Maybe a
Nothing (Name -> Raw
Var Name
a) Raw
RType) (Name -> Raw
Var Name
b))
TT Name
tm <- Elab' aux (TT Name)
forall aux. Elab' aux (TT Name)
get_term
Name -> Elab' aux ()
forall aux. Name -> Elab' aux ()
start_unify Name
s
Bool -> Elab' aux () -> Elab' aux ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
infer (Elab' aux () -> Elab' aux ()) -> Elab' aux () -> Elab' aux ()
forall a b. (a -> b) -> a -> b
$ Raw -> Elab' aux ()
forall aux. Raw -> Elab' aux ()
unifyGoal (Name -> Raw
Var Name
b)
[Name]
hs <- Elab' aux [Name]
forall aux. Elab' aux [Name]
get_holes
Name -> Raw -> Elab' aux ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
s (Name -> Raw
Var Name
a)
Name -> [Name] -> Elab' aux ()
forall aux. Name -> [Name] -> Elab' aux ()
prep_fill Name
f [Name
s]
Name -> Elab' aux ()
forall aux. Name -> Elab' aux ()
focus Name
f; Elab' aux ()
fun
Name -> Elab' aux ()
forall aux. Name -> Elab' aux ()
focus Name
s; Elab' aux ()
arg
TT Name
tm <- Elab' aux (TT Name)
forall aux. Elab' aux (TT Name)
get_term
Fails
ps <- Elab' aux Fails
forall aux. Elab' aux Fails
get_probs
TT Name
ty <- Elab' aux (TT Name)
forall aux. Elab' aux (TT Name)
goal
[Name]
hs <- Elab' aux [Name]
forall aux. Elab' aux [Name]
get_holes
Elab' aux ()
forall aux. Elab' aux ()
complete_fill
Env
env <- Elab' aux Env
forall aux. Elab' aux Env
get_env
[Name]
hs <- Elab' aux [Name]
forall aux. Elab' aux [Name]
get_holes
Bool -> Elab' aux () -> Elab' aux ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Name
a Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
hs) (Elab' aux () -> Elab' aux ()) -> Elab' aux () -> Elab' aux ()
forall a b. (a -> b) -> a -> b
$ do Name -> Elab' aux ()
forall aux. Name -> Elab' aux ()
movelast Name
a
Bool -> Elab' aux () -> Elab' aux ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Name
b Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
hs) (Elab' aux () -> Elab' aux ()) -> Elab' aux () -> Elab' aux ()
forall a b. (a -> b) -> a -> b
$ do Name -> Elab' aux ()
forall aux. Name -> Elab' aux ()
movelast Name
b
Elab' aux ()
forall aux. Elab' aux ()
end_unify
dep_app :: Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
dep_app :: forall aux. Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
dep_app Elab' aux ()
fun Elab' aux ()
arg String
str =
do Name
a <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"__argTy")
Name
b <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"__retTy")
Name
fty <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"__fnTy")
Name
f <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"f")
Name
s <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"ds")
Name -> Raw -> Elab' aux ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
a Raw
RType
Name -> Raw -> Elab' aux ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
fty Raw
RType
Name -> Raw -> Elab' aux ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
f (Name -> Raw
Var Name
fty)
TT Name
tm <- Elab' aux (TT Name)
forall aux. Elab' aux (TT Name)
get_term
TT Name
g <- Elab' aux (TT Name)
forall aux. Elab' aux (TT Name)
goal
Name -> Elab' aux ()
forall aux. Name -> Elab' aux ()
start_unify Name
s
Name -> Raw -> Elab' aux ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
s (Name -> Raw
Var Name
a)
Name -> [Name] -> Elab' aux ()
forall aux. Name -> [Name] -> Elab' aux ()
prep_fill Name
f [Name
s]
Name -> Elab' aux ()
forall aux. Name -> Elab' aux ()
focus Name
f; Elab' aux ()
forall aux. Elab' aux ()
attack; Elab' aux ()
fun
Elab' aux ()
forall aux. Elab' aux ()
end_unify
TT Name
fty <- Elab' aux (TT Name)
forall aux. Elab' aux (TT Name)
goal
Elab' aux ()
forall aux. Elab' aux ()
solve
Name -> Elab' aux ()
forall aux. Name -> Elab' aux ()
focus Name
s; Elab' aux ()
forall aux. Elab' aux ()
attack;
Context
ctxt <- Elab' aux Context
forall aux. Elab' aux Context
get_context
Env
env <- Elab' aux Env
forall aux. Elab' aux Env
get_env
case Context -> Env -> TT Name -> TT Name
normalise Context
ctxt Env
env TT Name
fty of
Bind Name
_ (Pi RigCount
_ Maybe ImplicitInfo
_ TT Name
argty TT Name
_) TT Name
_ -> Raw -> Elab' aux ()
forall aux. Raw -> Elab' aux ()
unifyGoal (TT Name -> Raw
forget TT Name
argty)
TT Name
_ -> String -> Elab' aux ()
forall a. String -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Can't make type"
Elab' aux ()
forall aux. Elab' aux ()
end_unify
Elab' aux ()
arg
Elab' aux ()
forall aux. Elab' aux ()
solve
Elab' aux ()
forall aux. Elab' aux ()
complete_fill
[Name]
hs <- Elab' aux [Name]
forall aux. Elab' aux [Name]
get_holes
Bool -> Elab' aux () -> Elab' aux ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Name
a Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
hs) (Elab' aux () -> Elab' aux ()) -> Elab' aux () -> Elab' aux ()
forall a b. (a -> b) -> a -> b
$ do Name -> Elab' aux ()
forall aux. Name -> Elab' aux ()
movelast Name
a
Bool -> Elab' aux () -> Elab' aux ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Name
b Name -> [Name] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Name]
hs) (Elab' aux () -> Elab' aux ()) -> Elab' aux () -> Elab' aux ()
forall a b. (a -> b) -> a -> b
$ do Name -> Elab' aux ()
forall aux. Name -> Elab' aux ()
movelast Name
b
Elab' aux ()
forall aux. Elab' aux ()
end_unify
arg :: Name -> RigCount -> Maybe ImplicitInfo -> Name -> Elab' aux ()
arg :: forall aux.
Name -> RigCount -> Maybe ImplicitInfo -> Name -> Elab' aux ()
arg Name
n RigCount
r Maybe ImplicitInfo
i Name
tyhole = do Name
ty <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
unique_hole Name
tyhole
Name -> Raw -> Elab' aux ()
forall aux. Name -> Raw -> Elab' aux ()
claim Name
ty Raw
RType
Name -> Elab' aux ()
forall aux. Name -> Elab' aux ()
movelast Name
ty
Name -> RigCount -> Maybe ImplicitInfo -> Raw -> Elab' aux ()
forall aux.
Name -> RigCount -> Maybe ImplicitInfo -> Raw -> Elab' aux ()
forAll Name
n RigCount
r Maybe ImplicitInfo
i (Name -> Raw
Var Name
ty)
no_errors :: Elab' aux () -> Maybe Err -> Elab' aux ()
no_errors :: forall aux. Elab' aux () -> Maybe Err -> Elab' aux ()
no_errors Elab' aux ()
tac Maybe Err
err
= do Fails
ps <- Elab' aux Fails
forall aux. Elab' aux Fails
get_probs
ElabState aux
s <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
case Maybe Err
err of
Maybe Err
Nothing -> Elab' aux ()
tac
Just Err
e ->
case Elab' aux () -> ElabState aux -> TC ((), ElabState aux)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT Elab' aux ()
tac ElabState aux
s of
Error Err
_ -> TC () -> Elab' aux ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> Elab' aux ()) -> TC () -> Elab' aux ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
Error Err
e
OK (()
a, ElabState aux
s') -> do ElabState aux -> Elab' aux ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ElabState aux
s'
() -> Elab' aux ()
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
a
Elab' aux ()
forall aux. Elab' aux ()
unifyProblems
Fails
ps' <- Elab' aux Fails
forall aux. Elab' aux Fails
get_probs
if (Fails -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Fails
ps' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Fails -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Fails
ps) then
case Fails -> Fails
forall a. [a] -> [a]
reverse Fails
ps' of
((TT Name
x, TT Name
y, Bool
_, Env
env, Err
inerr, [FailContext]
while, FailAt
_) : Fails
_) ->
let (Maybe Provenance
xp, Maybe Provenance
yp) = Err -> (Maybe Provenance, Maybe Provenance)
getProvenance Err
inerr
env' :: [(Name, TT Name)]
env' = ((Name, RigCount, Binder (TT Name)) -> (Name, TT Name))
-> Env -> [(Name, TT Name)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Name
x, RigCount
rig, Binder (TT Name)
b) -> (Name
x, Binder (TT Name) -> TT Name
forall b. Binder b -> b
binderTy Binder (TT Name)
b)) Env
env in
TC () -> Elab' aux ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC () -> Elab' aux ()) -> TC () -> Elab' aux ()
forall a b. (a -> b) -> a -> b
$ Err -> TC ()
forall a. Err -> TC a
tfail (Err -> TC ()) -> Err -> TC ()
forall a b. (a -> b) -> a -> b
$
case Maybe Err
err of
Maybe Err
Nothing -> Bool
-> (TT Name, Maybe Provenance)
-> (TT Name, Maybe Provenance)
-> Err
-> [(Name, TT Name)]
-> Int
-> Err
forall t.
Bool
-> (t, Maybe Provenance)
-> (t, Maybe Provenance)
-> Err' t
-> [(Name, t)]
-> Int
-> Err' t
CantUnify Bool
False (TT Name
x, Maybe Provenance
xp) (TT Name
y, Maybe Provenance
yp) Err
inerr [(Name, TT Name)]
env' Int
0
Just Err
e -> Err
e
else () -> Elab' aux ()
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> Elab' aux ()) -> () -> Elab' aux ()
forall a b. (a -> b) -> a -> b
$! ()
try :: Elab' aux a -> Elab' aux a -> Elab' aux a
try :: forall aux a. Elab' aux a -> Elab' aux a -> Elab' aux a
try Elab' aux a
t1 Elab' aux a
t2 = Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
forall aux a. Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
try' Elab' aux a
t1 Elab' aux a
t2 Bool
False
handleError :: (Err -> Bool) -> Elab' aux a -> Elab' aux a -> Elab' aux a
handleError :: forall aux a.
(Err -> Bool) -> Elab' aux a -> Elab' aux a -> Elab' aux a
handleError Err -> Bool
p Elab' aux a
t1 Elab' aux a
t2
= do ElabState aux
s <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
Fails
ps <- Elab' aux Fails
forall aux. Elab' aux Fails
get_probs
case Elab' aux a -> ElabState aux -> TC (a, ElabState aux)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT Elab' aux a
t1 ElabState aux
s of
OK (a
v, ElabState aux
s') -> do ElabState aux -> StateT (ElabState aux) TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ElabState aux
s'
a -> Elab' aux a
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Elab' aux a) -> a -> Elab' aux a
forall a b. (a -> b) -> a -> b
$! a
v
Error Err
e1 -> if Err -> Bool
p Err
e1 then
do case Elab' aux a -> ElabState aux -> TC (a, ElabState aux)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT Elab' aux a
t2 ElabState aux
s of
OK (a
v, ElabState aux
s') -> do ElabState aux -> StateT (ElabState aux) TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ElabState aux
s'; a -> Elab' aux a
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Elab' aux a) -> a -> Elab' aux a
forall a b. (a -> b) -> a -> b
$! a
v
Error Err
e2 -> TC a -> Elab' aux a
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Err -> TC a
forall a. Err -> TC a
tfail Err
e2)
else TC a -> Elab' aux a
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Err -> TC a
forall a. Err -> TC a
tfail Err
e1)
try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
try' :: forall aux a. Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a
try' Elab' aux a
t1 Elab' aux a
t2 Bool
proofSearch
= do ElabState aux
s <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
Fails
ps <- Elab' aux Fails
forall aux. Elab' aux Fails
get_probs
Bool
ulog <- Elab' aux Bool
forall aux. Elab' aux Bool
getUnifyLog
[Name]
ivs <- Elab' aux [Name]
forall aux. Elab' aux [Name]
get_implementations
case Int
-> Bool
-> Fails
-> Maybe [Any]
-> Elab' aux a
-> ElabState aux
-> TC ((a, Int, Fails), ElabState aux)
forall a b t t1.
Int
-> Bool
-> [a]
-> Maybe [b]
-> StateT (ElabState t) TC t1
-> ElabState t
-> TC ((t1, Int, Fails), ElabState t)
prunStateT Int
999999 Bool
False Fails
ps Maybe [Any]
forall a. Maybe a
Nothing Elab' aux a
t1 ElabState aux
s of
OK ((a
v, Int
_, Fails
_), ElabState aux
s') -> do ElabState aux -> StateT (ElabState aux) TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ElabState aux
s'
a -> Elab' aux a
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Elab' aux a) -> a -> Elab' aux a
forall a b. (a -> b) -> a -> b
$! a
v
Error Err
e1 -> Bool -> String -> Elab' aux a -> Elab' aux a
forall {a}. Bool -> String -> a -> a
traceWhen Bool
ulog (String
"try failed " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Err -> String
forall a. Show a => a -> String
show Err
e1) (Elab' aux a -> Elab' aux a) -> Elab' aux a -> Elab' aux a
forall a b. (a -> b) -> a -> b
$
if Err -> Bool
forall {t}. Err' t -> Bool
recoverableErr Err
e1 then
do case Elab' aux a -> ElabState aux -> TC (a, ElabState aux)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT Elab' aux a
t2 ElabState aux
s of
OK (a
v, ElabState aux
s') -> do ElabState aux -> StateT (ElabState aux) TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ElabState aux
s'; a -> Elab' aux a
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Elab' aux a) -> a -> Elab' aux a
forall a b. (a -> b) -> a -> b
$! a
v
Error Err
e2 -> TC a -> Elab' aux a
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Err -> TC a
forall a. Err -> TC a
tfail Err
e2)
else TC a -> Elab' aux a
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Err -> TC a
forall a. Err -> TC a
tfail Err
e1)
where recoverableErr :: Err' t -> Bool
recoverableErr err :: Err' t
err@(CantUnify Bool
r (t, Maybe Provenance)
x (t, Maybe Provenance)
y Err' t
_ [(Name, t)]
_ Int
_)
=
Bool
r Bool -> Bool -> Bool
|| Bool
proofSearch
recoverableErr (CantSolveGoal t
_ [(Name, t)]
_) = Bool
False
recoverableErr (CantResolveAlts [Name]
_) = Bool
proofSearch
recoverableErr (ProofSearchFail (Msg String
_)) = Bool
True
recoverableErr (ProofSearchFail Err' t
_) = Bool
False
recoverableErr (ElaboratingArg Name
_ Name
_ [(Name, Name)]
_ Err' t
e) = Err' t -> Bool
recoverableErr Err' t
e
recoverableErr (At FC
_ Err' t
e) = Err' t -> Bool
recoverableErr Err' t
e
recoverableErr (ElabScriptDebug [ErrorReportPart]
_ t
_ [(Name, t, [(Name, Binder t)])]
_) = Bool
False
recoverableErr Err' t
_ = Bool
True
tryCatch :: Elab' aux a -> (Err -> Elab' aux a) -> Elab' aux a
tryCatch :: forall aux a. Elab' aux a -> (Err -> Elab' aux a) -> Elab' aux a
tryCatch Elab' aux a
t1 Err -> Elab' aux a
t2
= do ElabState aux
s <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
Fails
ps <- Elab' aux Fails
forall aux. Elab' aux Fails
get_probs
Bool
ulog <- Elab' aux Bool
forall aux. Elab' aux Bool
getUnifyLog
case Elab' aux a -> ElabState aux -> TC (a, ElabState aux)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT Elab' aux a
t1 ElabState aux
s of
OK (a
v, ElabState aux
s') -> do ElabState aux -> StateT (ElabState aux) TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ElabState aux
s'
a -> Elab' aux a
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Elab' aux a) -> a -> Elab' aux a
forall a b. (a -> b) -> a -> b
$! a
v
Error Err
e1 -> Bool -> String -> Elab' aux a -> Elab' aux a
forall {a}. Bool -> String -> a -> a
traceWhen Bool
ulog (String
"tryCatch failed " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Err -> String
forall a. Show a => a -> String
show Err
e1) (Elab' aux a -> Elab' aux a) -> Elab' aux a -> Elab' aux a
forall a b. (a -> b) -> a -> b
$
case Elab' aux a -> ElabState aux -> TC (a, ElabState aux)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Err -> Elab' aux a
t2 Err
e1) ElabState aux
s of
OK (a
v, ElabState aux
s') -> do ElabState aux -> StateT (ElabState aux) TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ElabState aux
s'
a -> Elab' aux a
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Elab' aux a) -> a -> Elab' aux a
forall a b. (a -> b) -> a -> b
$! a
v
Error Err
e2 -> TC a -> Elab' aux a
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Err -> TC a
forall a. Err -> TC a
tfail Err
e2)
tryWhen :: Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a
tryWhen :: forall aux a. Bool -> Elab' aux a -> Elab' aux a -> Elab' aux a
tryWhen Bool
True Elab' aux a
a Elab' aux a
b = Elab' aux a -> Elab' aux a -> Elab' aux a
forall aux a. Elab' aux a -> Elab' aux a -> Elab' aux a
try Elab' aux a
a Elab' aux a
b
tryWhen Bool
False Elab' aux a
a Elab' aux a
b = Elab' aux a
a
tryAll :: [(Elab' aux a, Name)] -> Elab' aux a
tryAll :: forall aux a. [(Elab' aux a, Name)] -> Elab' aux a
tryAll = Bool -> [(Elab' aux a, Name)] -> Elab' aux a
forall aux a. Bool -> [(Elab' aux a, Name)] -> Elab' aux a
tryAll' Bool
True
tryAll' :: Bool -> [(Elab' aux a, Name)] -> Elab' aux a
tryAll' :: forall aux a. Bool -> [(Elab' aux a, Name)] -> Elab' aux a
tryAll' Bool
_ [(Elab' aux a
x, Name
_)] = Elab' aux a
x
tryAll' Bool
constrok [(Elab' aux a, Name)]
xs = [Elab' aux a] -> Int -> [(Elab' aux a, Name)] -> Elab' aux a
forall aux a.
[Elab' aux a] -> Int -> [(Elab' aux a, Name)] -> Elab' aux a
doAll [] Int
999999 [(Elab' aux a, Name)]
xs
where
cantResolve :: Elab' aux a
cantResolve :: forall aux a. Elab' aux a
cantResolve = TC a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC a -> StateT (ElabState aux) TC a)
-> TC a -> StateT (ElabState aux) TC a
forall a b. (a -> b) -> a -> b
$ Err -> TC a
forall a. Err -> TC a
tfail (Err -> TC a) -> Err -> TC a
forall a b. (a -> b) -> a -> b
$ [Name] -> Err
forall t. [Name] -> Err' t
CantResolveAlts (((Elab' aux a, Name) -> Name) -> [(Elab' aux a, Name)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Elab' aux a, Name) -> Name
forall a b. (a, b) -> b
snd [(Elab' aux a, Name)]
xs)
noneValid :: Elab' aux a
noneValid :: forall aux a. Elab' aux a
noneValid = TC a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC a -> StateT (ElabState aux) TC a)
-> TC a -> StateT (ElabState aux) TC a
forall a b. (a -> b) -> a -> b
$ Err -> TC a
forall a. Err -> TC a
tfail (Err -> TC a) -> Err -> TC a
forall a b. (a -> b) -> a -> b
$ [Name] -> Err
forall t. [Name] -> Err' t
NoValidAlts (((Elab' aux a, Name) -> Name) -> [(Elab' aux a, Name)] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map (Elab' aux a, Name) -> Name
forall a b. (a, b) -> b
snd [(Elab' aux a, Name)]
xs)
doAll :: [Elab' aux a] ->
Int ->
[(Elab' aux a, Name)] ->
Elab' aux a
doAll :: forall aux a.
[Elab' aux a] -> Int -> [(Elab' aux a, Name)] -> Elab' aux a
doAll [Elab' aux a
res] Int
pmax [] = Elab' aux a
res
doAll (Elab' aux a
_:[Elab' aux a]
_) Int
pmax [] = Elab' aux a
forall aux a. Elab' aux a
cantResolve
doAll [] Int
pmax [] = Elab' aux a
forall aux a. Elab' aux a
noneValid
doAll [Elab' aux a]
cs Int
pmax ((Elab' aux a
x, Name
msg):[(Elab' aux a, Name)]
xs)
= do ElabState aux
s <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
Fails
ps <- Elab' aux Fails
forall aux. Elab' aux Fails
get_probs
[Name]
ivs <- Elab' aux [Name]
forall aux. Elab' aux [Name]
get_implementations
TT Name
g <- Elab' aux (TT Name)
forall aux. Elab' aux (TT Name)
goal
case Int
-> Bool
-> Fails
-> Maybe [Name]
-> Elab' aux a
-> ElabState aux
-> TC ((a, Int, Fails), ElabState aux)
forall a b t t1.
Int
-> Bool
-> [a]
-> Maybe [b]
-> StateT (ElabState t) TC t1
-> ElabState t
-> TC ((t1, Int, Fails), ElabState t)
prunStateT Int
pmax Bool
True Fails
ps (if Bool
constrok then Maybe [Name]
forall a. Maybe a
Nothing
else [Name] -> Maybe [Name]
forall a. a -> Maybe a
Just [Name]
ivs) Elab' aux a
x ElabState aux
s of
OK ((a
v, Int
newps, Fails
probs), ElabState aux
s') ->
do let cs' :: [Elab' aux a]
cs' = if (Int
newps Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
pmax)
then [do ElabState aux -> StateT (ElabState aux) TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ElabState aux
s'; a -> Elab' aux a
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Elab' aux a) -> a -> Elab' aux a
forall a b. (a -> b) -> a -> b
$! a
v]
else (do ElabState aux -> StateT (ElabState aux) TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ElabState aux
s'; a -> Elab' aux a
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Elab' aux a) -> a -> Elab' aux a
forall a b. (a -> b) -> a -> b
$! a
v) Elab' aux a -> [Elab' aux a] -> [Elab' aux a]
forall a. a -> [a] -> [a]
: [Elab' aux a]
cs
ElabState aux -> StateT (ElabState aux) TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ElabState aux
s
[Elab' aux a] -> Int -> [(Elab' aux a, Name)] -> Elab' aux a
forall aux a.
[Elab' aux a] -> Int -> [(Elab' aux a, Name)] -> Elab' aux a
doAll [Elab' aux a]
cs' Int
newps [(Elab' aux a, Name)]
xs
Error Err
err -> do ElabState aux -> StateT (ElabState aux) TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ElabState aux
s
[Elab' aux a] -> Int -> [(Elab' aux a, Name)] -> Elab' aux a
forall aux a.
[Elab' aux a] -> Int -> [(Elab' aux a, Name)] -> Elab' aux a
doAll [Elab' aux a]
cs Int
pmax [(Elab' aux a, Name)]
xs
prunStateT
:: Int
-> Bool
-> [a]
-> Maybe [b]
-> Control.Monad.State.Strict.StateT
(ElabState t) TC t1
-> ElabState t
-> TC ((t1, Int, Idris.Core.Unify.Fails), ElabState t)
prunStateT :: forall a b t t1.
Int
-> Bool
-> [a]
-> Maybe [b]
-> StateT (ElabState t) TC t1
-> ElabState t
-> TC ((t1, Int, Fails), ElabState t)
prunStateT Int
pmax Bool
zok [a]
ps Maybe [b]
ivs StateT (ElabState t) TC t1
x ElabState t
s
= case StateT (ElabState t) TC t1 -> ElabState t -> TC (t1, ElabState t)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT (ElabState t) TC t1
x ElabState t
s of
OK (t1
v, s' :: ElabState t
s'@(ES (ProofState
p, t
_) String
_ Maybe (ElabState t)
_)) ->
let newps :: Int
newps = Fails -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (ProofState -> Fails
problems ProofState
p) Int -> Int -> Int
forall a. Num a => a -> a -> a
- [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ps
ibad :: Bool
ibad = [Name] -> Maybe [b] -> Bool
forall {t :: * -> *} {t :: * -> *} {a} {a}.
(Foldable t, Foldable t) =>
t a -> Maybe (t a) -> Bool
badImplementations (ProofState -> [Name]
implementations ProofState
p) Maybe [b]
ivs
newpmax :: Int
newpmax = if Int
newps Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0 then Int
0 else Int
newps in
if (Int
newpmax Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
pmax Bool -> Bool -> Bool
|| (Bool -> Bool
not Bool
zok Bool -> Bool -> Bool
&& Int
newps Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0))
then case Fails -> Fails
forall a. [a] -> [a]
reverse (ProofState -> Fails
problems ProofState
p) of
((TT Name
_,TT Name
_,Bool
_,Env
_,Err
e,[FailContext]
_,FailAt
_):Fails
_) -> Err -> TC ((t1, Int, Fails), ElabState t)
forall a. Err -> TC a
Error Err
e
else if Bool
ibad
then Err -> TC ((t1, Int, Fails), ElabState t)
forall a. Err -> TC a
Error (String -> Err
forall t. String -> Err' t
InternalMsg String
"Constraint introduced in disambiguation")
else ((t1, Int, Fails), ElabState t)
-> TC ((t1, Int, Fails), ElabState t)
forall a. a -> TC a
OK ((t1
v, Int
newpmax, ProofState -> Fails
problems ProofState
p), ElabState t
s')
Error Err
e -> Err -> TC ((t1, Int, Fails), ElabState t)
forall a. Err -> TC a
Error Err
e
where
badImplementations :: t a -> Maybe (t a) -> Bool
badImplementations t a
_ Maybe (t a)
Nothing = Bool
False
badImplementations t a
inow (Just t a
ithen) = t a -> Int
forall a. t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
inow Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> t a -> Int
forall a. t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
ithen
debugElaborator :: [ErrorReportPart] -> Elab' aux a
debugElaborator :: forall aux a. [ErrorReportPart] -> Elab' aux a
debugElaborator [ErrorReportPart]
msg = do ProofState
ps <- (ElabState aux -> ProofState)
-> StateT (ElabState aux) TC (ElabState aux)
-> StateT (ElabState aux) TC ProofState
forall a b.
(a -> b)
-> StateT (ElabState aux) TC a -> StateT (ElabState aux) TC b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ElabState aux -> ProofState
forall aux. ElabState aux -> ProofState
proof StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
Elab' aux ()
forall aux. Elab' aux ()
saveState
[Name]
hs <- Elab' aux [Name]
forall aux. Elab' aux [Name]
get_holes
[(Name, TT Name, [(Name, Binder (TT Name))])]
holeInfo <- (Name
-> StateT
(ElabState aux) TC (Name, TT Name, [(Name, Binder (TT Name))]))
-> [Name]
-> StateT
(ElabState aux) TC [(Name, TT Name, [(Name, Binder (TT Name))])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Name
-> StateT
(ElabState aux) TC (Name, TT Name, [(Name, Binder (TT Name))])
forall aux.
Name -> Elab' aux (Name, TT Name, [(Name, Binder (TT Name))])
getHoleInfo [Name]
hs
Elab' aux ()
forall aux. Elab' aux ()
loadState
TC a -> Elab' aux a
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (ElabState aux) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TC a -> Elab' aux a) -> (Err -> TC a) -> Err -> Elab' aux a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Err -> TC a
forall a. Err -> TC a
Error (Err -> Elab' aux a) -> Err -> Elab' aux a
forall a b. (a -> b) -> a -> b
$ [ErrorReportPart]
-> TT Name -> [(Name, TT Name, [(Name, Binder (TT Name))])] -> Err
forall t.
[ErrorReportPart] -> t -> [(Name, t, [(Name, Binder t)])] -> Err' t
ElabScriptDebug [ErrorReportPart]
msg (ProofTerm -> TT Name
getProofTerm (ProofState -> ProofTerm
pterm ProofState
ps)) [(Name, TT Name, [(Name, Binder (TT Name))])]
holeInfo
where getHoleInfo :: Name -> Elab' aux (Name, Type, [(Name, Binder Type)])
getHoleInfo :: forall aux.
Name -> Elab' aux (Name, TT Name, [(Name, Binder (TT Name))])
getHoleInfo Name
h = do Name -> Elab' aux ()
forall aux. Name -> Elab' aux ()
focus Name
h
TT Name
g <- Elab' aux (TT Name)
forall aux. Elab' aux (TT Name)
goal
Env
env <- Elab' aux Env
forall aux. Elab' aux Env
get_env
(Name, TT Name, [(Name, Binder (TT Name))])
-> Elab' aux (Name, TT Name, [(Name, Binder (TT Name))])
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (Name
h, TT Name
g, Env -> [(Name, Binder (TT Name))]
forall {a} {b1} {b2}. [(a, b1, b2)] -> [(a, b2)]
envBinders Env
env)
qshow :: Fails -> String
qshow :: Fails -> String
qshow Fails
fs = [(TT Name, TT Name)] -> String
forall a. Show a => a -> String
show (((TT Name, TT Name, Bool, Env, Err, [FailContext], FailAt)
-> (TT Name, TT Name))
-> Fails -> [(TT Name, TT Name)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (TT Name
x, TT Name
y, Bool
_, Env
_, Err
_, [FailContext]
_, FailAt
_) -> (TT Name
x, TT Name
y)) Fails
fs)
dumpprobs :: [(a, b, c, a)] -> String
dumpprobs [] = String
""
dumpprobs ((a
_,b
_,c
_,a
e):[(a, b, c, a)]
es) = a -> String
forall a. Show a => a -> String
show a
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(a, b, c, a)] -> String
dumpprobs [(a, b, c, a)]
es