{-|
Module      : Idris.Core.Elaborate
Description : A high level language of tactic composition, for building elaborators from a high level language into the core theory.

License     : BSD3
Maintainer  : The Idris Community.

This is our interface to proof construction, rather than ProofState,
because this gives us a language to build derived tactics out of the
primitives.
-}

{-# 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

-- Insert a 'proofSearchFail' error if necessary to shortcut any further
-- fruitless searching
proofFail :: Elab' aux a -> Elab' aux a
proofFail :: forall aux a. Elab' aux a -> Elab' aux a
proofFail Elab' aux a
e = do s <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                 case runStateT e 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 (p, a) s m <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                let p' = ProofState
p { dontunify = n : dontunify p }
                put (ES (p', a) s m)

-- Add a name that's okay to use in proof search (typically either because
-- it was given explicitly on the lhs, or intrduced as an explicit lambda
-- or let binding)
addPSname :: Name -> Elab' aux ()
addPSname :: forall aux. Name -> Elab' aux ()
addPSname n :: Name
n@(UN Text
_)
     = do ES (p, a) s m <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
          let p' = ProofState
p { psnames = n : psnames p }
          put (ES (p', a) s m)
addPSname Name
_ = () -> StateT (ElabState aux) TC ()
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return () -- can only use user given names

getPSnames :: Elab' aux [Name]
getPSnames :: forall aux. Elab' aux [Name]
getPSnames = do ES (p, a) s m <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                return (psnames p)

saveState :: Elab' aux ()
saveState :: forall aux. Elab' aux ()
saveState = do e@(ES p s _) <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
               put (ES p s (Just e))

loadState :: Elab' aux ()
loadState :: forall aux. Elab' aux ()
loadState = do (ES p s e) <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
               case e of
                  Just ElabState aux
st -> ElabState aux -> StateT (ElabState aux) TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ElabState aux
st
                  Maybe (ElabState aux)
_ -> TC () -> StateT (ElabState aux) TC ()
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 () -> StateT (ElabState aux) TC ())
-> TC () -> StateT (ElabState aux) TC ()
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 (p, a) s e) <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                   let next = ProofState -> Int
nextname ProofState
p
                   let p' = ProofState
p { nextname = next + 1 }
                   put (ES (p', a) s e)
                   let 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
                   return $! n'

setNextName :: Elab' aux ()
setNextName :: forall aux. Elab' aux ()
setNextName = do env <- Elab' aux Env
forall aux. Elab' aux Env
get_env
                 ES (p, a) s e <- get
                 let 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))
                 initNextNameFrom (pargs ++ map fstEnv env)

initNextNameFrom :: [Name] -> Elab' aux ()
initNextNameFrom :: forall aux. [Name] -> Elab' aux ()
initNextNameFrom [Name]
ns = do ES (p, a) s e <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                         let n' = Int -> [Name] -> Int
maxName (ProofState -> Int
nextname ProofState
p) [Name]
ns
                         put (ES (p { nextname = n' }, a) s 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


-- | Transform the error returned by an elaboration script, preserving
-- location information and proof search failure messages.
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 s <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                         case runStateT elab 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 s <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
         case runStateT elab 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 <- Elab' aux aux
forall aux. Elab' aux aux
getAux
                                 return $! (a, aux)
            Error (ProofSearchFail (At FC
f Err
e))
                           -> TC (a, aux) -> StateT (ElabState aux) TC (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) -> StateT (ElabState aux) TC (a, aux))
-> TC (a, aux) -> StateT (ElabState aux) TC (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) -> StateT (ElabState aux) TC (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) -> StateT (ElabState aux) TC (a, aux))
-> TC (a, aux) -> StateT (ElabState aux) TC (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) -> StateT (ElabState aux) TC (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) -> StateT (ElabState aux) TC (a, aux))
-> TC (a, aux) -> StateT (ElabState aux) TC (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 (x, _) <- 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
              return 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 -- ^ the name of what's to be elaborated
               -> String -- ^ the current source file
               -> Context -- ^ the current global context
               -> Ctxt TypeInfo -- ^ the value of the idris_datatypes field of IState
               -> Int -- ^ the value of the idris_name field of IState
               -> Type -- ^ the goal 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, ES ps' str _) <- 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
     return $! (a, str)

-- | Modify the auxiliary state
updateAux :: (aux -> aux) -> Elab' aux ()
updateAux :: forall aux. (aux -> aux) -> Elab' aux ()
updateAux aux -> aux
f = do ES (ps, a) l p <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                 put (ES (ps, f a) l p)

-- | Get the auxiliary state
getAux :: Elab' aux aux
getAux :: forall aux. Elab' aux aux
getAux = do ES (ps, a) _ _ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
            return $! a

-- | Set whether to show the unifier log
unifyLog :: Bool -> Elab' aux ()
unifyLog :: forall aux. Bool -> Elab' aux ()
unifyLog Bool
log = do ES (ps, a) l p <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                  put (ES (ps { unifylog = log }, a) l p)

getUnifyLog :: Elab' aux Bool
getUnifyLog :: forall aux. Elab' aux Bool
getUnifyLog = do ES (ps, a) l p <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                 return (unifylog ps)

-- | Process a tactic within the current elaborator state
processTactic' :: Tactic -> Elab' aux ()
processTactic' :: forall aux. Tactic -> Elab' aux ()
processTactic' Tactic
t = do ES (p, a) logs prev <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                      (p', log) <- lift $ processTactic t p
                      put (ES (p', a) (logs ++ log) prev)
                      return $! ()

updatePS :: (ProofState -> ProofState) -> Elab' aux ()
updatePS :: forall aux. (ProofState -> ProofState) -> Elab' aux ()
updatePS ProofState -> ProofState
f = do ES (ps, a) logs prev <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                put $ ES (f ps, a) logs 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 (ps, _) _ _ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                     return $ map (\ (FailContext FC
x Name
y Name
z) -> (FC
x, Name
y, Name
z))
                                  (while_elaborating ps)

-- Some handy gadgets for pulling out bits of state

-- | Get the global context
get_context :: Elab' aux Context
get_context :: forall aux. Elab' aux Context
get_context = do ES p _ _ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                 return $! (context (fst p))

-- | Update the context.
-- (should only be used for adding temporary definitions or all sorts of
--  stuff could go wrong)
set_context :: Context -> Elab' aux ()
set_context :: forall aux. Context -> Elab' aux ()
set_context Context
ctxt = do ES (p, a) logs prev <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                      put (ES (p { context = ctxt }, a) logs prev)

get_datatypes :: Elab' aux (Ctxt TypeInfo)
get_datatypes :: forall aux. Elab' aux (Ctxt TypeInfo)
get_datatypes = do ES p _ _ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                   return $! (datatypes (fst p))

set_datatypes :: Ctxt TypeInfo -> Elab' aux ()
set_datatypes :: forall aux. Ctxt TypeInfo -> Elab' aux ()
set_datatypes Ctxt TypeInfo
ds = do ES (p, a) logs prev <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                      put (ES (p { datatypes = ds }, a) logs prev)

get_global_nextname :: Elab' aux Int
get_global_nextname :: forall aux. Elab' aux Int
get_global_nextname = do ES (ps, _) _ _ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                         return (global_nextname ps)

set_global_nextname :: Int -> Elab' aux ()
set_global_nextname :: forall aux. Int -> Elab' aux ()
set_global_nextname Int
i = do ES (ps, a) logs prev <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                           put $ ES (ps { global_nextname = i}, a) logs prev

-- | get the proof term
get_term :: Elab' aux Term
get_term :: forall aux. Elab' aux (TT Name)
get_term = do ES p _ _ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
              return $! (getProofTerm (pterm (fst p)))

-- | modify the proof term
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 (p,a) logs prev <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                   let p' = ProofState
p { pterm = mkProofTerm (f (getProofTerm (pterm p))) }
                   put (ES (p', a) logs prev)

-- | get the local context at the currently in focus hole
get_env :: Elab' aux Env
get_env :: forall aux. Elab' aux Env
get_env = do ES p _ _ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
             lift $ envAtFocus (fst p)

get_inj :: Elab' aux [Name]
get_inj :: forall aux. Elab' aux [Name]
get_inj = do ES p _ _ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
             return $! (injective (fst p))

get_holes :: Elab' aux [Name]
get_holes :: forall aux. Elab' aux [Name]
get_holes = do ES p _ _ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
               return $! (holes (fst p))

get_usedns :: Elab' aux [Name]
get_usedns :: forall aux. Elab' aux [Name]
get_usedns = do ES p _ _ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                let 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 = 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)
                return $! nouse

get_probs :: Elab' aux Fails
get_probs :: forall aux. Elab' aux Fails
get_probs = do ES p _ _ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
               return $! (problems (fst p))

-- | Return recently solved names (that is, the names solved since the
-- last call to get_recents)
get_recents :: Elab' aux [Name]
get_recents :: forall aux. Elab' aux [Name]
get_recents = do ES (p, a) l prev <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                 put (ES (p { recents = [] }, a) l prev)
                 return (recents p)

-- | get the current goal type
goal :: Elab' aux Type
goal :: forall aux. Elab' aux (TT Name)
goal = do ES p _ _ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
          b <- lift $ goalAtFocus (fst p)
          return $! (binderTy b)

is_guess :: Elab' aux Bool
is_guess :: forall aux. Elab' aux Bool
is_guess = do ES p _ _ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
              b <- lift $ goalAtFocus (fst p)
              case b of
                   Guess TT Name
_ TT Name
_ -> Bool -> StateT (ElabState aux) TC Bool
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                   Binder (TT Name)
_ -> Bool -> StateT (ElabState aux) TC Bool
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False

-- | Get the guess at the current hole, if there is one
get_guess :: Elab' aux Term
get_guess :: forall aux. Elab' aux (TT Name)
get_guess = do ES p _ _ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
               b <- lift $ goalAtFocus (fst p)
               case b of
                    Guess TT Name
t TT Name
v -> TT Name -> StateT (ElabState aux) TC (TT Name)
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return (TT Name -> StateT (ElabState aux) TC (TT Name))
-> TT Name -> StateT (ElabState aux) TC (TT Name)
forall a b. (a -> b) -> a -> b
$! TT Name
v
                    Binder (TT Name)
_ -> String -> StateT (ElabState aux) TC (TT Name)
forall a. String -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"Not a guess"

-- | Typecheck locally
get_type :: Raw -> Elab' aux Type
get_type :: forall aux. Raw -> Elab' aux (TT Name)
get_type Raw
tm = do ctxt <- Elab' aux Context
forall aux. Elab' aux Context
get_context
                 env <- get_env
                 (val, ty) <- lift $ check ctxt env tm
                 return $! (finalise 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 ctxt <- Elab' aux Context
forall aux. Elab' aux Context
get_context
                     env <- get_env
                     (val, ty) <- lift $ check ctxt env tm
                     return $! (finalise val, finalise ty)

-- | get holes we've deferred for later definition
get_deferred :: Elab' aux [Name]
get_deferred :: forall aux. Elab' aux [Name]
get_deferred = do ES p _ _ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                  return $! (deferred (fst 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 ctxt <- Elab' aux Context
forall aux. Elab' aux Context
get_context
                               if isInj ctxt tm then return $! ()
                                else lift $ tfail (NotInjective tm l 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 implementation argument names
get_implementations :: Elab' aux [Name]
get_implementations :: forall aux. Elab' aux [Name]
get_implementations = do ES p _ _ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                         return $! (implementations (fst p))

-- | get auto argument names
get_autos :: Elab' aux [(Name, ([FailContext], [Name]))]
get_autos :: forall aux. Elab' aux [(Name, ([FailContext], [Name]))]
get_autos = do ES p _ _ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
               return $! (autos (fst p))

-- | given a desired hole name, return a unique hole name
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 p _ _ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
           let 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 = 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)
           n' <- return $! uniqueNameCtxt (context (fst p)) n nouse
           ES (p, a) s u <- get
           case 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
$! ()
           return $! n'

elog :: String -> Elab' aux ()
elog :: forall aux. String -> Elab' aux ()
elog String
str = do ES p logs prev <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
              put (ES p (logs ++ str ++ "\n") prev)

getLog :: Elab' aux String
getLog :: forall aux. Elab' aux String
getLog = do ES p logs _ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
            return $! logs

-- The primitives, from ProofState

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

-- Clear the list of variables not to unify, and try to solve them
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)

-- | Turn the current hole into a pattern variable with the provided
-- name, made unique if not the same as the head of the hole queue
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 <- Elab' aux Env
forall aux. Elab' aux Env
get_env
              hs <- get_holes
              if (n `elem` map fstEnv env) then do apply (Var n) []; solve
                else do n' <- case 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
                        processTactic' (PatVar n)

-- | Turn the current hole into a pattern variable with the provided
-- name, but don't make MNs unique.
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 <- Elab' aux Env
forall aux. Elab' aux Env
get_env
               hs <- get_holes
               if (n `elem` map fstEnv env) then do apply (Var n) [] ; solve
                  else processTactic' (PatVar 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 (p, a) s m <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
             tm <- get_term
             case holes p of
                  [] -> () -> StateT (ElabState aux) TC ()
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 }
--                         trace ("DOTTING " ++ show (h, outer) ++ "\n" ++
--                                show tm) $
                        ElabState aux -> StateT (ElabState aux) TC ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put (ElabState aux -> StateT (ElabState aux) TC ())
-> ElabState aux -> StateT (ElabState aux) TC ()
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 (p, a) s m <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                 return (dotted p)

-- | Set the zipper in the proof state to point at the current sub term
-- (This currently happens automatically, so this will have no effect...)
zipHere :: Elab' aux ()
zipHere :: forall aux. Elab' aux ()
zipHere = do ES (ps, a) s m <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
             let 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)
             put (ES (ps { pterm = pt' }, a) s 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 n' <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
unique_hole Name
n
         processTactic' (Defer ds ls n')
         return 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 p _ _ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
         return $! (getProofTerm (pterm (fst p)))

undo :: Elab' aux ()
undo :: forall aux. Elab' aux ()
undo = Tactic -> Elab' aux ()
forall aux. Tactic -> Elab' aux ()
processTactic' Tactic
Undo

-- | Prepare to apply a function by creating holes to be filled by the arguments
prepare_apply :: Raw    -- ^ The operation being applied
              -> [Bool] -- ^ Whether arguments are implicit
              -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes to be filled with elaborated argument values
prepare_apply :: forall aux. Raw -> [Bool] -> Elab' aux [(Name, Name)]
prepare_apply Raw
fn [Bool]
imps =
    do ty <- Raw -> Elab' aux (TT Name)
forall aux. Raw -> Elab' aux (TT Name)
get_type Raw
fn
       ctxt <- get_context
       env <- get_env
       -- let claims = getArgs ty imps
       -- claims <- mkClaims (normalise ctxt env ty) imps []
       -- Count arguments to check if we need to normalise the type
       let 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)
       claims <- -- trace (show (fn, imps, ty, map fst env, normalise ctxt env (finalise ty))) $
                 mkClaims usety imps [] (map fstEnv env)
       ES (p, a) s prev <- get
       -- reverse the claims we made so that args go left to right
       let 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 (h : hs) = holes p
       put (ES (p { holes = h : (reverse (take n hs) ++ drop n hs) }, a) s prev)
       return $! 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   -- ^ The type of the operation being applied
             -> [Bool] -- ^ Whether the arguments are implicit
             -> [(Name, Name)] -- ^ Accumulator for produced claims
             -> [Name] -- ^ Hypotheses
             -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes, resp.
    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
           n <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
getNameFrom (Name -> Name
mkMN Name
n')
--            when (null claims) (start_unify n)
           let 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 <- get_env
           claim n (forgetEnv (map fstEnv env) t)
           when i (movelast n)
           mkClaims sc' is ((n', n) : claims) 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 ctxt <- Elab' aux Context
forall aux. Elab' aux Context
get_context
                        lift $ tfail $ TooManyArguments 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 an operator, solving some arguments by unification or matching.
apply, match_apply :: Raw -- ^ The operator to apply
                   -> [(Bool, Int)] -- ^ For each argument, whether to
                                    -- attempt to solve it and the
                                    -- priority in which to do so
                   -> 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 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)
       -- _Don't_ solve the arguments we're specifying by hand.
       -- (remove from unified list before calling end_unify)
       hs <- get_holes
       ES (p, a) s prev <- get
       let 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 (n, hunis) = -- trace ("AVOID UNIFY: " ++ show (fn, dont)) $
                        unified p
       let unify = -- trace ("Not done " ++ show hs) $
                   [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 = -- trace ("Not done " ++ show (hs, hunis)) $
                      [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
       put (ES (p { dontunify = dont, unified = (n, unify),
                    notunified = notunify ++ notunified p }, a) s prev)
       fillt (raw_apply fn (map (Var . snd) args))
       ulog <- getUnifyLog
       g <- goal
       traceWhen ulog
                 ("Goal " ++ show g ++ " -- when elaborating " ++ show fn)
                 end_unify
       return $! (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)) 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 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)
       fill (raw_apply fn (map (Var . snd) args))
       elabArgs (map snd args) elabs
       ES (p, a) s prev <- get
       end_unify
       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 ty <- Raw -> Elab' aux (TT Name)
forall aux. Raw -> Elab' aux (TT Name)
get_type (Name -> Raw
Var Name
n)
       ctxt <- get_context
       env <- get_env
       claims <- doClaims (normalise ctxt env ty) args []
       prep_fill n (map fst claims)
       elabClaims [] False claims
       complete_fill
       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 n <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
unique_hole (Name -> Name
mkMN Name
n')
           when (null claims) (start_unify n)
           let 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
           claim n (forget t)
           case 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
_ -> -- don't solve by unification as there is an explicit value
                         do ES (p, a) s prev <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                            put (ES (p { dontunify = n : dontunify p }, a) s prev)
           doClaims sc' is ((n, i) : 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 p _ _ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                      focus n; elaboration; elabClaims failed r 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 p _ _ <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
                         focus n; elaboration; elabClaims failed r 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

-- If the goal is not a Pi-type, invent some names and make it a pi type
checkPiGoal :: Name -> Elab' aux ()
checkPiGoal :: forall aux. Name -> Elab' aux ()
checkPiGoal Name
n
            = do g <- Elab' aux (TT Name)
forall aux. Elab' aux (TT Name)
goal
                 ctxt <- get_context
                 env <- get_env
                 case (normalise ctxt env g) of
                    Bind Name
_ (Pi RigCount
_ Maybe ImplicitInfo
_ TT Name
_ TT Name
_) TT Name
_ -> () -> StateT (ElabState aux) TC ()
forall a. a -> StateT (ElabState aux) TC a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                    TT Name
_ -> do a <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"__pargTy")
                            b <- getNameFrom (sMN 0 "__pretTy")
                            f <- getNameFrom (sMN 0 "pf")
                            claim a RType
                            claim b RType
                            claim f (RBind n (Pi RigW Nothing (Var a) RType) (Var b))
                            movelast a
                            movelast b
                            fill (Var f)
                            solve
                            focus 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 a <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"__argTy")
       b <- getNameFrom (sMN 0 "__retTy")
       f <- getNameFrom (sMN 0 "f")
       s <- getNameFrom (sMN 0 "is")
       claim a RType
       claim b RType
       claim f (RBind (sMN 0 "_aX") (Pi RigW Nothing (Var a) RType) (Var b))
       tm <- get_term
       start_unify s
       -- if 'infer' is set, we're assuming it's a simply typed application
       -- so safe to unify with the goal type (as there'll be no dependencies)
       when infer $ unifyGoal (Var b)
       hs <- get_holes
       claim s (Var a)
       prep_fill f [s]
       focus f; fun
       focus s; arg
       tm <- get_term
       ps <- get_probs
       ty <- goal
       hs <- get_holes
       complete_fill
       env <- get_env
       -- We don't need a and b in the hole queue any more since they were
       -- just for checking f, so move them to the end. If they never end up
       -- getting solved, we'll get an 'Incomplete term' error.
       hs <- get_holes
       when (a `elem` hs) $ do movelast a
       when (b `elem` hs) $ do movelast b
       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 a <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
getNameFrom (Int -> String -> Name
sMN Int
0 String
"__argTy")
       b <- getNameFrom (sMN 0 "__retTy")
       fty <- getNameFrom (sMN 0 "__fnTy")
       f <- getNameFrom (sMN 0 "f")
       s <- getNameFrom (sMN 0 "ds")
       claim a RType
       claim fty RType
       claim f (Var fty)
       tm <- get_term
       g <- goal
       start_unify s
       claim s (Var a)

       prep_fill f [s]
       focus f; attack; fun
       end_unify
       fty <- goal
       solve
       focus s; attack;
       ctxt <- get_context
       env <- get_env
       case normalise ctxt env fty of
            -- if f gives a function type, unify our argument type with
            -- f's expected argument type
            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)
            -- Can't infer a type for 'f', so fail here (and drop back to
            -- simply typed application where we infer the type for f)
            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"
       end_unify
       arg
       solve
       complete_fill

       -- We don't need a and b in the hole queue any more since they were
       -- just for checking f, so move them to the end. If they never end up
       -- getting solved, we'll get an 'Incomplete term' error.
       hs <- get_holes
       when (a `elem` hs) $ do movelast a
       when (b `elem` hs) $ do movelast b
       end_unify

-- Abstract over an argument of unknown type, giving a name for the hole
-- which we'll fill with the argument type too.
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 ty <- Name -> Elab' aux Name
forall aux. Name -> Elab' aux Name
unique_hole Name
tyhole
                      claim ty RType
                      movelast ty
                      forAll n r i (Var ty)

-- try a tactic, if it adds any unification problem, return an error
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 ps <- Elab' aux Fails
forall aux. Elab' aux Fails
get_probs
            s <- get
            case err of
                 Maybe Err
Nothing -> Elab' aux ()
tac
                 Just Err
e -> -- update the error, if there is one.
                     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
            unifyProblems
            ps' <- get_probs
            if (length ps' > length ps) then
               case reverse 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 return $! ()

-- Try a tactic, if it fails, try another
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 s <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
               ps <- get_probs
               case runStateT t1 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 s <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
       ps <- get_probs
       ulog <- getUnifyLog
       ivs <- get_implementations
       case prunStateT 999999 False ps Nothing t1 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
_)
             = -- traceWhen r (show err) $
               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 s <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
       ps <- get_probs
       ulog <- getUnifyLog
--        case prunStateT 999999 False ps t1 s of
       case runStateT t1 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

-- Bool says whether it's okay to create new unification problems. If set
-- to False, then the whole tactic fails if there are any new problems
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] -> -- successes
             Int -> -- most problems
             [(Elab' aux a, Name)] -> -- still to try
             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 s <- StateT (ElabState aux) TC (ElabState aux)
forall s (m :: * -> *). MonadState s m => m s
get
            ps <- get_probs
            ivs <- get_implementations
            g <- goal
            case prunStateT pmax True ps (if constrok then Nothing
                                                      else Just ivs) x 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

-- Run an elaborator, and fail if any problems or constraints are introduced
prunStateT
  :: Int
     -> Bool
     -> [a]
     -> Maybe [b] -- constraints left, if we're interested
     -> 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)) -- length ps == 0 && newpmax > 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 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
                         saveState -- so we don't need to remember the hole order
                         hs <- get_holes
                         holeInfo <- mapM getHoleInfo hs
                         loadState
                         lift . Error $ ElabScriptDebug msg (getProofTerm (pterm ps)) 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
                           g <- Elab' aux (TT Name)
forall aux. Elab' aux (TT Name)
goal
                           env <- get_env
                           return (h, g, envBinders 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