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

-- 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 (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 () -- can only use user given names

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


-- | 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 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 -- ^ 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
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)

-- | Modify the auxiliary state
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)

-- | Get the auxiliary state
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

-- | Set whether to show the unifier log
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)

-- | Process a tactic within the current elaborator state
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)

-- 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 (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))

-- | 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 (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 the proof term
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)))

-- | 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 (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 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 (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))

-- | 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 (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)

-- | get the current goal type
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 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 (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"

-- | Typecheck locally
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 holes we've deferred for later definition
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 implementation argument names
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 auto argument names
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))

-- | 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 (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

-- 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
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)

-- | 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
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 }
--                         trace ("DOTTING " ++ show (h, outer) ++ "\n" ++
--                                show tm) $
                        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)

-- | 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 (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 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 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 claims = getArgs ty imps
       -- claims <- mkClaims (normalise ctxt env ty) imps []
       -- Count arguments to check if we need to normalise the type
       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 <- -- trace (show (fn, imps, ty, map fst env, normalise ctxt env (finalise ty))) $
                 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
       -- reverse the claims we made so that args go left to right
       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   -- ^ 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
           Name
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
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 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 [(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)
       -- _Don't_ solve the arguments we're specifying by hand.
       -- (remove from unified list before calling end_unify)
       [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) = -- trace ("AVOID UNIFY: " ++ show (fn, dont)) $
                        ProofState -> (Name, [(Name, TT Name)])
unified ProofState
p
       let unify :: [(Name, TT Name)]
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 :: [(Name, TT Name)]
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
       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
_ -> -- don't solve by unification as there is an explicit value
                         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

-- 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 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
       -- 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)
       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
       -- 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.
       [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
            -- 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"
       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

       -- 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.
       [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

-- 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 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)

-- 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 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 -> -- 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
            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 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 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
_)
             = -- 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 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 prunStateT 999999 False ps t1 s of
       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

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

-- 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 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 -- so we don't need to remember the hole order
                         [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