module Agda.Auto.Convert where
import Control.Monad.State
import Data.IORef
import Data.Maybe (catMaybes)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Traversable (traverse)
import Agda.Syntax.Common (Hiding(..), getHiding, Arg)
import Agda.Syntax.Concrete (exprFieldA)
import qualified Agda.Syntax.Internal as I
import Agda.Syntax.Internal (Dom'(..),domInfo,unDom)
import qualified Agda.Syntax.Internal.Pattern as IP
import qualified Agda.Syntax.Common as Cm
import qualified Agda.Syntax.Abstract.Name as AN
import qualified Agda.Syntax.Abstract as A
import qualified Agda.Syntax.Position as SP
import qualified Agda.TypeChecking.Monad.Base as MB
import Agda.TypeChecking.Monad.Signature (getConstInfo, getDefFreeVars, ignoreAbstractMode)
import Agda.TypeChecking.Level (reallyUnLevelView)
import Agda.TypeChecking.Monad.Base (mvJudgement, mvPermutation, getMetaInfo, envContext, clEnv)
import Agda.TypeChecking.Monad.MetaVars (lookupMeta, withMetaInfo, lookupInteractionPoint)
import Agda.TypeChecking.Monad.Context (getContextArgs)
import Agda.TypeChecking.Monad.Constraints (getAllConstraints)
import Agda.TypeChecking.Substitute (applySubst, renamingR)
import Agda.TypeChecking.Telescope (piApplyM)
import qualified Agda.TypeChecking.Substitute as I (absBody)
import Agda.TypeChecking.Reduce (normalise, instantiate)
import Agda.TypeChecking.EtaContract (etaContract)
import Agda.TypeChecking.Monad.Builtin (constructorForm)
import Agda.TypeChecking.Free as Free (freeIn)
import Agda.Interaction.MakeCase (getClauseZipperForIP)
import Agda.Auto.NarrowingSearch
import Agda.Auto.Syntax hiding (getConst)
import Agda.Auto.CaseSplit hiding (lift)
import Agda.Utils.Either
import Agda.Utils.Except ( ExceptT , MonadError(throwError) )
import Agda.Utils.Lens
import Agda.Utils.Monad ( forMaybeMM )
import Agda.Utils.Permutation ( Permutation(Perm), permute, takeP, compactP )
import Agda.Utils.Pretty ( prettyShow )
import Agda.Utils.Impossible
data Hint = Hint
{ Hint -> Bool
hintIsConstructor :: Bool
, Hint -> QName
hintQName :: I.QName
}
type O = (Maybe (Int, [Arg AN.QName]),AN.QName)
data TMode = TMAll
deriving TMode -> TMode -> Bool
(TMode -> TMode -> Bool) -> (TMode -> TMode -> Bool) -> Eq TMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TMode -> TMode -> Bool
$c/= :: TMode -> TMode -> Bool
== :: TMode -> TMode -> Bool
$c== :: TMode -> TMode -> Bool
Eq
type MapS a b = (Map a b, [a])
initMapS :: MapS a b
initMapS :: MapS a b
initMapS = (Map a b
forall k a. Map k a
Map.empty, [])
popMapS :: (S -> (a, [b])) -> ((a, [b]) -> S -> S) -> TOM (Maybe b)
popMapS :: (S -> (a, [b])) -> ((a, [b]) -> S -> S) -> TOM (Maybe b)
popMapS r :: S -> (a, [b])
r w :: (a, [b]) -> S -> S
w = do (m :: a
m, xs :: [b]
xs) <- (S -> (a, [b])) -> StateT S TCM (a, [b])
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets S -> (a, [b])
r
case [b]
xs of
[] -> Maybe b -> TOM (Maybe b)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe b
forall a. Maybe a
Nothing
(x :: b
x:xs :: [b]
xs) -> do
(S -> S) -> StateT S TCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((a, [b]) -> S -> S
w (a
m, [b]
xs))
Maybe b -> TOM (Maybe b)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe b -> TOM (Maybe b)) -> Maybe b -> TOM (Maybe b)
forall a b. (a -> b) -> a -> b
$ b -> Maybe b
forall a. a -> Maybe a
Just b
x
data S = S {S -> MapS QName (TMode, ConstRef O)
sConsts :: MapS AN.QName (TMode, ConstRef O),
S
-> MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
sMetas :: MapS I.MetaId (Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [I.MetaId]),
S -> MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs :: MapS Int (Maybe (Bool, MExp O, MExp O)),
S -> Maybe MetaId
sCurMeta :: Maybe I.MetaId,
S -> MetaId
sMainMeta :: I.MetaId
}
type TOM = StateT S MB.TCM
type MOT = ExceptT String IO
tomy :: I.MetaId -> [Hint] -> [I.Type] ->
MB.TCM ([ConstRef O]
, [MExp O]
, Map I.MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [I.MetaId])
, [(Bool, MExp O, MExp O)]
, Map AN.QName (TMode, ConstRef O))
tomy :: MetaId
-> [Hint]
-> [Type]
-> TCM
([ConstRef O], [MExp O],
Map
MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId]),
[(Bool, MExp O, MExp O)], Map QName (TMode, ConstRef O))
tomy imi :: MetaId
imi icns :: [Hint]
icns typs :: [Type]
typs = do
[(Bool, Term, Term)]
eqs <- TCM [(Bool, Term, Term)]
getEqs
let
r :: [AN.QName] -> TOM [AN.QName]
r :: [QName] -> TOM [QName]
r projfcns :: [QName]
projfcns = do
Maybe QName
nxt <- (S -> MapS QName (TMode, ConstRef O))
-> (MapS QName (TMode, ConstRef O) -> S -> S) -> TOM (Maybe QName)
forall a b.
(S -> (a, [b])) -> ((a, [b]) -> S -> S) -> TOM (Maybe b)
popMapS S -> MapS QName (TMode, ConstRef O)
sConsts (\x :: MapS QName (TMode, ConstRef O)
x y :: S
y -> S
y {sConsts :: MapS QName (TMode, ConstRef O)
sConsts = MapS QName (TMode, ConstRef O)
x})
case Maybe QName
nxt of
Just cn :: QName
cn -> do
Map QName (TMode, ConstRef O)
cmap <- MapS QName (TMode, ConstRef O) -> Map QName (TMode, ConstRef O)
forall a b. (a, b) -> a
fst (MapS QName (TMode, ConstRef O) -> Map QName (TMode, ConstRef O))
-> StateT S TCM (MapS QName (TMode, ConstRef O))
-> StateT S TCM (Map QName (TMode, ConstRef O))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` (S -> MapS QName (TMode, ConstRef O))
-> StateT S TCM (MapS QName (TMode, ConstRef O))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets S -> MapS QName (TMode, ConstRef O)
sConsts
let (mode :: TMode
mode, c :: ConstRef O
c) = Map QName (TMode, ConstRef O)
cmap Map QName (TMode, ConstRef O) -> QName -> (TMode, ConstRef O)
forall k a. Ord k => Map k a -> k -> a
Map.! QName
cn
Definition
def <- TCM Definition -> StateT S TCM Definition
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Definition -> StateT S TCM Definition)
-> TCM Definition -> StateT S TCM Definition
forall a b. (a -> b) -> a -> b
$ QName -> TCM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
cn
let typ :: Type
typ = Definition -> Type
MB.defType Definition
def
defn :: Defn
defn = Definition -> Defn
MB.theDef Definition
def
Type
typ <- TCM Type -> StateT S TCM Type
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Type -> StateT S TCM Type) -> TCM Type -> StateT S TCM Type
forall a b. (a -> b) -> a -> b
$ Type -> TCM Type
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Type
typ
MExp O
typ' <- Type -> StateT S TCM (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Type
typ
let clausesToDef :: [Clause] -> m (DeclCont o, [a])
clausesToDef clauses :: [Clause]
clauses = do
[Clause o]
clauses' <- [Clause] -> m [Clause o]
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert [Clause]
clauses
let narg :: Int
narg = case [Clause]
clauses of
[] -> 0
I.Clause {I.namedClausePats = xs} : _ -> [NamedArg DeBruijnPattern] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedArg DeBruijnPattern]
xs
(DeclCont o, [a]) -> m (DeclCont o, [a])
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> [Clause o] -> Maybe Int -> Maybe Int -> DeclCont o
forall o. Int -> [Clause o] -> Maybe Int -> Maybe Int -> DeclCont o
Def Int
narg [Clause o]
clauses' Maybe Int
forall a. Maybe a
Nothing Maybe Int
forall a. Maybe a
Nothing, [])
(cont :: DeclCont O
cont, projfcns2 :: [QName]
projfcns2) <- case Defn
defn of
MB.Axiom {} -> (DeclCont O, [QName]) -> StateT S TCM (DeclCont O, [QName])
forall (m :: * -> *) a. Monad m => a -> m a
return (DeclCont O
forall o. DeclCont o
Postulate, [])
MB.DataOrRecSig{} -> (DeclCont O, [QName]) -> StateT S TCM (DeclCont O, [QName])
forall (m :: * -> *) a. Monad m => a -> m a
return (DeclCont O
forall o. DeclCont o
Postulate, [])
MB.GeneralizableVar{} -> StateT S TCM (DeclCont O, [QName])
forall a. HasCallStack => a
__IMPOSSIBLE__
MB.AbstractDefn{} -> (DeclCont O, [QName]) -> StateT S TCM (DeclCont O, [QName])
forall (m :: * -> *) a. Monad m => a -> m a
return (DeclCont O
forall o. DeclCont o
Postulate, [])
MB.Function {funClauses :: Defn -> [Clause]
MB.funClauses = [Clause]
clauses} -> [Clause] -> StateT S TCM (DeclCont O, [QName])
forall (m :: * -> *) o a.
(Monad m, Conversion m [Clause] [Clause o]) =>
[Clause] -> m (DeclCont o, [a])
clausesToDef [Clause]
clauses
MB.Primitive {primClauses :: Defn -> [Clause]
MB.primClauses = [Clause]
clauses} -> [Clause] -> StateT S TCM (DeclCont O, [QName])
forall (m :: * -> *) o a.
(Monad m, Conversion m [Clause] [Clause o]) =>
[Clause] -> m (DeclCont o, [a])
clausesToDef [Clause]
clauses
MB.Datatype {dataCons :: Defn -> [QName]
MB.dataCons = [QName]
cons} -> do
[ConstRef O]
cons2 <- (QName -> StateT S TCM (ConstRef O))
-> [QName] -> StateT S TCM [ConstRef O]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\con :: QName
con -> Bool -> QName -> TMode -> StateT S TCM (ConstRef O)
getConst Bool
True QName
con TMode
TMAll) [QName]
cons
(DeclCont O, [QName]) -> StateT S TCM (DeclCont O, [QName])
forall (m :: * -> *) a. Monad m => a -> m a
return ([ConstRef O] -> [ConstRef O] -> DeclCont O
forall o. [ConstRef o] -> [ConstRef o] -> DeclCont o
Datatype [ConstRef O]
cons2 [], [])
MB.Record {recFields :: Defn -> [Dom QName]
MB.recFields = [Dom QName]
fields, recTel :: Defn -> Telescope
MB.recTel = Telescope
tel} -> do
let pars :: Int -> Type -> [Arg Term]
pars n :: Int
n (I.El _ (I.Pi it :: Dom Type
it typ :: Abs Type
typ)) = ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Cm.Arg (Dom Type -> ArgInfo
forall t e. Dom' t e -> ArgInfo
I.domInfo Dom Type
it) (Int -> Term
I.var Int
n) Arg Term -> [Arg Term] -> [Arg Term]
forall a. a -> [a] -> [a]
:
Int -> Type -> [Arg Term]
pars (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) (Abs Type -> Type
forall a. Abs a -> a
I.unAbs Abs Type
typ)
pars _ (I.El _ _) = []
contyp :: Int -> Telescope -> Type
contyp npar :: Int
npar I.EmptyTel = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
I.El (Integer -> Sort' Term
I.mkType 0 ) (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$
QName -> Elims -> Term
I.Def QName
cn (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
I.Apply ([Arg Term] -> Elims) -> [Arg Term] -> Elims
forall a b. (a -> b) -> a -> b
$ Int -> Type -> [Arg Term]
pars (Int
npar Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) Type
typ
contyp npar :: Int
npar (I.ExtendTel it :: Dom Type
it (I.Abs v :: ArgName
v tel :: Telescope
tel)) = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
I.El (Integer -> Sort' Term
I.mkType 0 ) (Dom Type -> Abs Type -> Term
I.Pi Dom Type
it (ArgName -> Type -> Abs Type
forall a. ArgName -> a -> Abs a
I.Abs ArgName
v (Int -> Telescope -> Type
contyp (Int
npar Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) Telescope
tel)))
contyp npar :: Int
npar (I.ExtendTel it :: Dom Type
it I.NoAbs{}) = Type
forall a. HasCallStack => a
__IMPOSSIBLE__
MExp O
contyp' <- Type -> StateT S TCM (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert (Type -> StateT S TCM (MExp O)) -> Type -> StateT S TCM (MExp O)
forall a b. (a -> b) -> a -> b
$ Int -> Telescope -> Type
contyp 0 Telescope
tel
ConstDef O
cc <- TCM (ConstDef O) -> StateT S TCM (ConstDef O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (ConstDef O) -> StateT S TCM (ConstDef O))
-> TCM (ConstDef O) -> StateT S TCM (ConstDef O)
forall a b. (a -> b) -> a -> b
$ IO (ConstDef O) -> TCM (ConstDef O)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ConstDef O) -> TCM (ConstDef O))
-> IO (ConstDef O) -> TCM (ConstDef O)
forall a b. (a -> b) -> a -> b
$ ConstRef O -> IO (ConstDef O)
forall a. IORef a -> IO a
readIORef ConstRef O
c
let Datatype [con :: ConstRef O
con] [] = ConstDef O -> DeclCont O
forall o. ConstDef o -> DeclCont o
cdcont ConstDef O
cc
TCM () -> StateT S TCM ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> StateT S TCM ()) -> TCM () -> StateT S TCM ()
forall a b. (a -> b) -> a -> b
$ IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$ ConstRef O -> (ConstDef O -> ConstDef O) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef ConstRef O
con (\cdef :: ConstDef O
cdef -> ConstDef O
cdef {cdtype :: MExp O
cdtype = MExp O
contyp'})
[ConstRef O]
projfcns <- (QName -> StateT S TCM (ConstRef O))
-> [QName] -> StateT S TCM [ConstRef O]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\name :: QName
name -> Bool -> QName -> TMode -> StateT S TCM (ConstRef O)
getConst Bool
False QName
name TMode
TMAll) ((Dom QName -> QName) -> [Dom QName] -> [QName]
forall a b. (a -> b) -> [a] -> [b]
map Dom QName -> QName
forall t e. Dom' t e -> e
I.unDom [Dom QName]
fields)
(DeclCont O, [QName]) -> StateT S TCM (DeclCont O, [QName])
forall (m :: * -> *) a. Monad m => a -> m a
return ([ConstRef O] -> [ConstRef O] -> DeclCont O
forall o. [ConstRef o] -> [ConstRef o] -> DeclCont o
Datatype [ConstRef O
con] [ConstRef O]
projfcns, [])
MB.Constructor {conData :: Defn -> QName
MB.conData = QName
dt} -> do
ConstRef O
_ <- Bool -> QName -> TMode -> StateT S TCM (ConstRef O)
getConst Bool
False QName
dt TMode
TMAll
ConstDef O
cc <- TCM (ConstDef O) -> StateT S TCM (ConstDef O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (ConstDef O) -> StateT S TCM (ConstDef O))
-> TCM (ConstDef O) -> StateT S TCM (ConstDef O)
forall a b. (a -> b) -> a -> b
$ IO (ConstDef O) -> TCM (ConstDef O)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ConstDef O) -> TCM (ConstDef O))
-> IO (ConstDef O) -> TCM (ConstDef O)
forall a b. (a -> b) -> a -> b
$ ConstRef O -> IO (ConstDef O)
forall a. IORef a -> IO a
readIORef ConstRef O
c
let (Just (nomi :: Int
nomi,_), _) = ConstDef O -> O
forall o. ConstDef o -> o
cdorigin ConstDef O
cc
(DeclCont O, [QName]) -> StateT S TCM (DeclCont O, [QName])
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> DeclCont O
forall o. Int -> DeclCont o
Constructor (Int
nomi Int -> Int -> Int
forall a. Num a => a -> a -> a
- ConstDef O -> Int
forall o. ConstDef o -> Int
cddeffreevars ConstDef O
cc), [])
TCM () -> StateT S TCM ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> StateT S TCM ()) -> TCM () -> StateT S TCM ()
forall a b. (a -> b) -> a -> b
$ IO () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$ ConstRef O -> (ConstDef O -> ConstDef O) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef ConstRef O
c (\cdef :: ConstDef O
cdef -> ConstDef O
cdef {cdtype :: MExp O
cdtype = MExp O
typ', cdcont :: DeclCont O
cdcont = DeclCont O
cont})
[QName] -> TOM [QName]
r ([QName] -> TOM [QName]) -> [QName] -> TOM [QName]
forall a b. (a -> b) -> a -> b
$ [QName]
projfcns2 [QName] -> [QName] -> [QName]
forall a. [a] -> [a] -> [a]
++ [QName]
projfcns
Nothing -> do
Maybe MetaId
nxt <- (S
-> MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId]))
-> (MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> S -> S)
-> TOM (Maybe MetaId)
forall a b.
(S -> (a, [b])) -> ((a, [b]) -> S -> S) -> TOM (Maybe b)
popMapS S
-> MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
sMetas (\x :: MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
x y :: S
y -> S
y {sMetas :: MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
sMetas = MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
x})
case Maybe MetaId
nxt of
Just mi :: MetaId
mi -> do
(((Bool, Term, Term), Int) -> StateT S TCM ())
-> [((Bool, Term, Term), Int)] -> StateT S TCM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\((_, e :: Term
e, i :: Term
i), eqi :: Int
eqi) -> do
Bool -> StateT S TCM () -> StateT S TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (MetaId -> Term -> Bool
fmExp MetaId
mi Term
e Bool -> Bool -> Bool
|| MetaId -> Term -> Bool
fmExp MetaId
mi Term
i) (StateT S TCM () -> StateT S TCM ())
-> StateT S TCM () -> StateT S TCM ()
forall a b. (a -> b) -> a -> b
$ do
(eqsm :: Map Int (Maybe (Bool, MExp O, MExp O))
eqsm, eqsl :: [Int]
eqsl) <- (S -> MapS Int (Maybe (Bool, MExp O, MExp O)))
-> StateT S TCM (MapS Int (Maybe (Bool, MExp O, MExp O)))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets S -> MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs
Bool -> StateT S TCM () -> StateT S TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int -> Map Int (Maybe (Bool, MExp O, MExp O)) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.notMember Int
eqi Map Int (Maybe (Bool, MExp O, MExp O))
eqsm) (StateT S TCM () -> StateT S TCM ())
-> StateT S TCM () -> StateT S TCM ()
forall a b. (a -> b) -> a -> b
$ do
(S -> S) -> StateT S TCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((S -> S) -> StateT S TCM ()) -> (S -> S) -> StateT S TCM ()
forall a b. (a -> b) -> a -> b
$ \s :: S
s -> S
s {sEqs :: MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs = (Int
-> Maybe (Bool, MExp O, MExp O)
-> Map Int (Maybe (Bool, MExp O, MExp O))
-> Map Int (Maybe (Bool, MExp O, MExp O))
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
eqi Maybe (Bool, MExp O, MExp O)
forall a. Maybe a
Nothing Map Int (Maybe (Bool, MExp O, MExp O))
eqsm, Int
eqi Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
eqsl)}
) ([(Bool, Term, Term)] -> [Int] -> [((Bool, Term, Term), Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Bool, Term, Term)]
eqs [0..])
MetaVariable
mv <- TCM MetaVariable -> StateT S TCM MetaVariable
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM MetaVariable -> StateT S TCM MetaVariable)
-> TCM MetaVariable -> StateT S TCM MetaVariable
forall a b. (a -> b) -> a -> b
$ MetaId -> TCM MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
mi
Maybe Term
msol <- case MetaVariable -> MetaInstantiation
MB.mvInstantiation MetaVariable
mv of
MB.InstV{} ->
TCMT IO (Maybe Term) -> StateT S TCM (Maybe Term)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO (Maybe Term) -> StateT S TCM (Maybe Term))
-> TCMT IO (Maybe Term) -> StateT S TCM (Maybe Term)
forall a b. (a -> b) -> a -> b
$ Closure Range -> TCMT IO (Maybe Term) -> TCMT IO (Maybe Term)
forall a. Closure Range -> TCM a -> TCM a
withMetaInfo (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mv) (TCMT IO (Maybe Term) -> TCMT IO (Maybe Term))
-> TCMT IO (Maybe Term) -> TCMT IO (Maybe Term)
forall a b. (a -> b) -> a -> b
$ do
[Arg Term]
args <- TCMT IO [Arg Term]
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Arg Term]
getContextArgs
Term
sol <- Term -> TCMT IO Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate (Term -> TCMT IO Term) -> Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
I.MetaV MetaId
mi (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
I.Apply ([Arg Term] -> Elims) -> [Arg Term] -> Elims
forall a b. (a -> b) -> a -> b
$ Permutation -> [Arg Term] -> [Arg Term]
forall a. Permutation -> [a] -> [a]
permute (Int -> Permutation -> Permutation
takeP ([Arg Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
args) (Permutation -> Permutation) -> Permutation -> Permutation
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Permutation
mvPermutation MetaVariable
mv) [Arg Term]
args
Maybe Term -> TCMT IO (Maybe Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Term -> TCMT IO (Maybe Term))
-> Maybe Term -> TCMT IO (Maybe Term)
forall a b. (a -> b) -> a -> b
$ Term -> Maybe Term
forall a. a -> Maybe a
Just Term
sol
_ -> Maybe Term -> StateT S TCM (Maybe Term)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Term
forall a. Maybe a
Nothing
case Maybe Term
msol of
Nothing -> () -> StateT S TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just sol :: Term
sol -> do
Metavar (Exp O) (RefInfo O)
m <- MetaId -> TOM (Metavar (Exp O) (RefInfo O))
getMeta MetaId
mi
MExp O
sol' <- Term -> StateT S TCM (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Term
sol
(S -> S) -> StateT S TCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((S -> S) -> StateT S TCM ()) -> (S -> S) -> StateT S TCM ()
forall a b. (a -> b) -> a -> b
$ \s :: S
s -> S
s {sEqs :: MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs = (Int
-> Maybe (Bool, MExp O, MExp O)
-> Map Int (Maybe (Bool, MExp O, MExp O))
-> Map Int (Maybe (Bool, MExp O, MExp O))
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Map Int (Maybe (Bool, MExp O, MExp O)) -> Int
forall k a. Map k a -> Int
Map.size (MapS Int (Maybe (Bool, MExp O, MExp O))
-> Map Int (Maybe (Bool, MExp O, MExp O))
forall a b. (a, b) -> a
fst (MapS Int (Maybe (Bool, MExp O, MExp O))
-> Map Int (Maybe (Bool, MExp O, MExp O)))
-> MapS Int (Maybe (Bool, MExp O, MExp O))
-> Map Int (Maybe (Bool, MExp O, MExp O))
forall a b. (a -> b) -> a -> b
$ S -> MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs S
s)) ((Bool, MExp O, MExp O) -> Maybe (Bool, MExp O, MExp O)
forall a. a -> Maybe a
Just (Bool
False, Metavar (Exp O) (RefInfo O) -> MExp O
forall a blk. Metavar a blk -> MM a blk
Meta Metavar (Exp O) (RefInfo O)
m, MExp O
sol')) (MapS Int (Maybe (Bool, MExp O, MExp O))
-> Map Int (Maybe (Bool, MExp O, MExp O))
forall a b. (a, b) -> a
fst (MapS Int (Maybe (Bool, MExp O, MExp O))
-> Map Int (Maybe (Bool, MExp O, MExp O)))
-> MapS Int (Maybe (Bool, MExp O, MExp O))
-> Map Int (Maybe (Bool, MExp O, MExp O))
forall a b. (a -> b) -> a -> b
$ S -> MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs S
s), MapS Int (Maybe (Bool, MExp O, MExp O)) -> [Int]
forall a b. (a, b) -> b
snd (MapS Int (Maybe (Bool, MExp O, MExp O)) -> [Int])
-> MapS Int (Maybe (Bool, MExp O, MExp O)) -> [Int]
forall a b. (a -> b) -> a -> b
$ S -> MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs S
s)}
let tt :: Type
tt = Judgement MetaId -> Type
forall a. Judgement a -> Type
MB.jMetaType (Judgement MetaId -> Type) -> Judgement MetaId -> Type
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Judgement MetaId
mvJudgement MetaVariable
mv
minfo :: Closure Range
minfo = MetaVariable -> Closure Range
getMetaInfo MetaVariable
mv
localVars :: [Type]
localVars = (Dom' Term (Name, Type) -> Type)
-> [Dom' Term (Name, Type)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type) -> Type
forall a b. (a, b) -> b
snd ((Name, Type) -> Type)
-> (Dom' Term (Name, Type) -> (Name, Type))
-> Dom' Term (Name, Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (Name, Type) -> (Name, Type)
forall t e. Dom' t e -> e
I.unDom) ([Dom' Term (Name, Type)] -> [Type])
-> (Closure Range -> [Dom' Term (Name, Type)])
-> Closure Range
-> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEnv -> [Dom' Term (Name, Type)]
envContext (TCEnv -> [Dom' Term (Name, Type)])
-> (Closure Range -> TCEnv)
-> Closure Range
-> [Dom' Term (Name, Type)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure Range -> TCEnv
forall a. Closure a -> TCEnv
clEnv (Closure Range -> [Type]) -> Closure Range -> [Type]
forall a b. (a -> b) -> a -> b
$ Closure Range
minfo
(targettype :: Type
targettype, localVars :: [Type]
localVars) <- TCMT IO (Type, [Type]) -> StateT S TCM (Type, [Type])
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO (Type, [Type]) -> StateT S TCM (Type, [Type]))
-> TCMT IO (Type, [Type]) -> StateT S TCM (Type, [Type])
forall a b. (a -> b) -> a -> b
$ Closure Range -> TCMT IO (Type, [Type]) -> TCMT IO (Type, [Type])
forall a. Closure Range -> TCM a -> TCM a
withMetaInfo Closure Range
minfo (TCMT IO (Type, [Type]) -> TCMT IO (Type, [Type]))
-> TCMT IO (Type, [Type]) -> TCMT IO (Type, [Type])
forall a b. (a -> b) -> a -> b
$ do
[Arg Term]
vs <- TCMT IO [Arg Term]
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Arg Term]
getContextArgs
Type
targettype <- Type
tt Type -> [Arg Term] -> TCM Type
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m) =>
Type -> a -> m Type
`piApplyM` Permutation -> [Arg Term] -> [Arg Term]
forall a. Permutation -> [a] -> [a]
permute (Int -> Permutation -> Permutation
takeP ([Arg Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
vs) (Permutation -> Permutation) -> Permutation -> Permutation
forall a b. (a -> b) -> a -> b
$ MetaVariable -> Permutation
mvPermutation MetaVariable
mv) [Arg Term]
vs
Type
targettype <- Type -> TCM Type
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Type
targettype
[Type]
localVars <- (Type -> TCM Type) -> [Type] -> TCMT IO [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> TCM Type
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise [Type]
localVars
(Type, [Type]) -> TCMT IO (Type, [Type])
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
targettype, [Type]
localVars)
(S -> S) -> StateT S TCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\s :: S
s -> S
s {sCurMeta :: Maybe MetaId
sCurMeta = MetaId -> Maybe MetaId
forall a. a -> Maybe a
Just MetaId
mi})
MExp O
typ' <- Type -> StateT S TCM (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Type
targettype
[MExp O]
ctx' <- (Type -> StateT S TCM (MExp O)) -> [Type] -> StateT S TCM [MExp O]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> StateT S TCM (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert [Type]
localVars
(S -> S) -> StateT S TCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\s :: S
s -> S
s {sCurMeta :: Maybe MetaId
sCurMeta = Maybe MetaId
forall a. Maybe a
Nothing})
(S -> S) -> StateT S TCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\s :: S
s -> S
s {sMetas :: MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
sMetas = (((Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> (Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]),
[MetaId]))
-> MetaId
-> Map
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> Map
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust (\(m :: Metavar (Exp O) (RefInfo O)
m, _, deps :: [MetaId]
deps) -> (Metavar (Exp O) (RefInfo O)
m, (MExp O, [MExp O]) -> Maybe (MExp O, [MExp O])
forall a. a -> Maybe a
Just (MExp O
typ', [MExp O]
ctx'), [MetaId]
deps)) MetaId
mi (MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> Map
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
forall a b. (a, b) -> a
fst (MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> Map
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId]))
-> MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> Map
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
forall a b. (a -> b) -> a -> b
$ S
-> MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
sMetas S
s), MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> [MetaId]
forall a b. (a, b) -> b
snd (MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> [MetaId])
-> MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> [MetaId]
forall a b. (a -> b) -> a -> b
$ S
-> MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
sMetas S
s)})
[QName] -> TOM [QName]
r [QName]
projfcns
Nothing -> do
Maybe Int
nxt <- (S -> MapS Int (Maybe (Bool, MExp O, MExp O)))
-> (MapS Int (Maybe (Bool, MExp O, MExp O)) -> S -> S)
-> TOM (Maybe Int)
forall a b.
(S -> (a, [b])) -> ((a, [b]) -> S -> S) -> TOM (Maybe b)
popMapS S -> MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs (\x :: MapS Int (Maybe (Bool, MExp O, MExp O))
x y :: S
y -> S
y {sEqs :: MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs = MapS Int (Maybe (Bool, MExp O, MExp O))
x})
case Maybe Int
nxt of
Just eqi :: Int
eqi -> do
let (ineq :: Bool
ineq, e :: Term
e, i :: Term
i) = [(Bool, Term, Term)]
eqs [(Bool, Term, Term)] -> Int -> (Bool, Term, Term)
forall a. [a] -> Int -> a
!! Int
eqi
MExp O
e' <- Term -> StateT S TCM (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Term
e
MExp O
i' <- Term -> StateT S TCM (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Term
i
(S -> S) -> StateT S TCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\s :: S
s -> S
s {sEqs :: MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs = ((Maybe (Bool, MExp O, MExp O) -> Maybe (Bool, MExp O, MExp O))
-> Int
-> Map Int (Maybe (Bool, MExp O, MExp O))
-> Map Int (Maybe (Bool, MExp O, MExp O))
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust (\_ -> (Bool, MExp O, MExp O) -> Maybe (Bool, MExp O, MExp O)
forall a. a -> Maybe a
Just (Bool
ineq, MExp O
e', MExp O
i')) Int
eqi (MapS Int (Maybe (Bool, MExp O, MExp O))
-> Map Int (Maybe (Bool, MExp O, MExp O))
forall a b. (a, b) -> a
fst (MapS Int (Maybe (Bool, MExp O, MExp O))
-> Map Int (Maybe (Bool, MExp O, MExp O)))
-> MapS Int (Maybe (Bool, MExp O, MExp O))
-> Map Int (Maybe (Bool, MExp O, MExp O))
forall a b. (a -> b) -> a -> b
$ S -> MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs S
s), MapS Int (Maybe (Bool, MExp O, MExp O)) -> [Int]
forall a b. (a, b) -> b
snd (MapS Int (Maybe (Bool, MExp O, MExp O)) -> [Int])
-> MapS Int (Maybe (Bool, MExp O, MExp O)) -> [Int]
forall a b. (a -> b) -> a -> b
$ S -> MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs S
s)})
[QName] -> TOM [QName]
r [QName]
projfcns
Nothing ->
[QName] -> TOM [QName]
forall (m :: * -> *) a. Monad m => a -> m a
return [QName]
projfcns
((icns' :: [ConstRef O]
icns', typs' :: [MExp O]
typs'), s :: S
s) <- StateT S TCM ([ConstRef O], [MExp O])
-> S -> TCM (([ConstRef O], [MExp O]), S)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT
(do Metavar (Exp O) (RefInfo O)
_ <- MetaId -> TOM (Metavar (Exp O) (RefInfo O))
getMeta MetaId
imi
[ConstRef O]
icns' <- (Hint -> StateT S TCM (ConstRef O))
-> [Hint] -> StateT S TCM [ConstRef O]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (Hint iscon :: Bool
iscon name :: QName
name) -> Bool -> QName -> TMode -> StateT S TCM (ConstRef O)
getConst Bool
iscon QName
name TMode
TMAll) [Hint]
icns
[MExp O]
typs' <- (Type -> StateT S TCM (MExp O)) -> [Type] -> StateT S TCM [MExp O]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> StateT S TCM (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert [Type]
typs
[QName]
projfcns <- [QName] -> TOM [QName]
r []
[ConstRef O]
projfcns' <- (QName -> StateT S TCM (ConstRef O))
-> [QName] -> StateT S TCM [ConstRef O]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\name :: QName
name -> Bool -> QName -> TMode -> StateT S TCM (ConstRef O)
getConst Bool
False QName
name TMode
TMAll) [QName]
projfcns
[] <- [QName] -> TOM [QName]
r []
([ConstRef O], [MExp O]) -> StateT S TCM ([ConstRef O], [MExp O])
forall (m :: * -> *) a. Monad m => a -> m a
return ([ConstRef O]
projfcns' [ConstRef O] -> [ConstRef O] -> [ConstRef O]
forall a. [a] -> [a] -> [a]
++ [ConstRef O]
icns', [MExp O]
typs')
) (S :: MapS QName (TMode, ConstRef O)
-> MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> MapS Int (Maybe (Bool, MExp O, MExp O))
-> Maybe MetaId
-> MetaId
-> S
S {sConsts :: MapS QName (TMode, ConstRef O)
sConsts = MapS QName (TMode, ConstRef O)
forall a b. MapS a b
initMapS, sMetas :: MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
sMetas = MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
forall a b. MapS a b
initMapS, sEqs :: MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs = MapS Int (Maybe (Bool, MExp O, MExp O))
forall a b. MapS a b
initMapS, sCurMeta :: Maybe MetaId
sCurMeta = Maybe MetaId
forall a. Maybe a
Nothing, sMainMeta :: MetaId
sMainMeta = MetaId
imi})
IO () -> TCM ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> TCM ()) -> IO () -> TCM ()
forall a b. (a -> b) -> a -> b
$ IO () -> IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ (ConstRef O -> IO ()) -> [ConstRef O] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ConstRef O -> IO ()
forall o. ConstRef o -> IO ()
categorizedecl [ConstRef O]
icns'
([ConstRef O], [MExp O],
Map
MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId]),
[(Bool, MExp O, MExp O)], Map QName (TMode, ConstRef O))
-> TCM
([ConstRef O], [MExp O],
Map
MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId]),
[(Bool, MExp O, MExp O)], Map QName (TMode, ConstRef O))
forall (m :: * -> *) a. Monad m => a -> m a
return ([ConstRef O]
icns', [MExp O]
typs', ((Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId]))
-> Map
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> Map
MetaId (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> (Metavar (Exp O) (RefInfo O), MExp O, [MExp O], [MetaId])
forall a b c d. (a, Maybe (b, c), d) -> (a, b, c, d)
flatten (MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> Map
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
forall a b. (a, b) -> a
fst (S
-> MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
sMetas S
s)), (Maybe (Bool, MExp O, MExp O) -> (Bool, MExp O, MExp O))
-> [Maybe (Bool, MExp O, MExp O)] -> [(Bool, MExp O, MExp O)]
forall a b. (a -> b) -> [a] -> [b]
map Maybe (Bool, MExp O, MExp O) -> (Bool, MExp O, MExp O)
forall p. Maybe p -> p
fromJust ([Maybe (Bool, MExp O, MExp O)] -> [(Bool, MExp O, MExp O)])
-> [Maybe (Bool, MExp O, MExp O)] -> [(Bool, MExp O, MExp O)]
forall a b. (a -> b) -> a -> b
$ Map Int (Maybe (Bool, MExp O, MExp O))
-> [Maybe (Bool, MExp O, MExp O)]
forall k a. Map k a -> [a]
Map.elems (MapS Int (Maybe (Bool, MExp O, MExp O))
-> Map Int (Maybe (Bool, MExp O, MExp O))
forall a b. (a, b) -> a
fst (S -> MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs S
s)), MapS QName (TMode, ConstRef O) -> Map QName (TMode, ConstRef O)
forall a b. (a, b) -> a
fst (S -> MapS QName (TMode, ConstRef O)
sConsts S
s))
where
flatten :: (a, Maybe (b, c), d) -> (a, b, c, d)
flatten (x :: a
x, Just (y :: b
y, z :: c
z), w :: d
w) = (a
x, b
y, c
z, d
w)
flatten (x :: a
x, Nothing, w :: d
w) = (a, b, c, d)
forall a. HasCallStack => a
__IMPOSSIBLE__
fromJust :: Maybe p -> p
fromJust (Just x :: p
x) = p
x
fromJust Nothing = p
forall a. HasCallStack => a
__IMPOSSIBLE__
getConst :: Bool -> AN.QName -> TMode -> TOM (ConstRef O)
getConst :: Bool -> QName -> TMode -> StateT S TCM (ConstRef O)
getConst iscon :: Bool
iscon name :: QName
name mode :: TMode
mode = do
Definition
def <- TCM Definition -> StateT S TCM Definition
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Definition -> StateT S TCM Definition)
-> TCM Definition -> StateT S TCM Definition
forall a b. (a -> b) -> a -> b
$ QName -> TCM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
name
case Definition -> Defn
MB.theDef Definition
def of
MB.Record {recConHead :: Defn -> ConHead
MB.recConHead = ConHead
con} -> do
let conname :: QName
conname = ConHead -> QName
I.conName ConHead
con
conflds :: [Arg QName]
conflds = ConHead -> [Arg QName]
I.conFields ConHead
con
Map QName (TMode, ConstRef O)
cmap <- MapS QName (TMode, ConstRef O) -> Map QName (TMode, ConstRef O)
forall a b. (a, b) -> a
fst (MapS QName (TMode, ConstRef O) -> Map QName (TMode, ConstRef O))
-> StateT S TCM (MapS QName (TMode, ConstRef O))
-> StateT S TCM (Map QName (TMode, ConstRef O))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` (S -> MapS QName (TMode, ConstRef O))
-> StateT S TCM (MapS QName (TMode, ConstRef O))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets S -> MapS QName (TMode, ConstRef O)
sConsts
case QName -> Map QName (TMode, ConstRef O) -> Maybe (TMode, ConstRef O)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
name Map QName (TMode, ConstRef O)
cmap of
Just (mode' :: TMode
mode', c :: ConstRef O
c) ->
if Bool
iscon then do
ConstDef O
cd <- TCM (ConstDef O) -> StateT S TCM (ConstDef O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (ConstDef O) -> StateT S TCM (ConstDef O))
-> TCM (ConstDef O) -> StateT S TCM (ConstDef O)
forall a b. (a -> b) -> a -> b
$ IO (ConstDef O) -> TCM (ConstDef O)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ConstDef O) -> TCM (ConstDef O))
-> IO (ConstDef O) -> TCM (ConstDef O)
forall a b. (a -> b) -> a -> b
$ ConstRef O -> IO (ConstDef O)
forall a. IORef a -> IO a
readIORef ConstRef O
c
let Datatype [con :: ConstRef O
con] _ = ConstDef O -> DeclCont O
forall o. ConstDef o -> DeclCont o
cdcont ConstDef O
cd
ConstRef O -> StateT S TCM (ConstRef O)
forall (m :: * -> *) a. Monad m => a -> m a
return ConstRef O
con
else
ConstRef O -> StateT S TCM (ConstRef O)
forall (m :: * -> *) a. Monad m => a -> m a
return ConstRef O
c
Nothing -> do
MetaId
mainm <- (S -> MetaId) -> StateT S TCM MetaId
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets S -> MetaId
sMainMeta
Int
dfv <- TCMT IO Int -> StateT S TCM Int
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Int -> StateT S TCM Int)
-> TCMT IO Int -> StateT S TCM Int
forall a b. (a -> b) -> a -> b
$ MetaId -> QName -> TCMT IO Int
getdfv MetaId
mainm QName
name
let nomi :: Int
nomi = Type -> Int
I.arity (Definition -> Type
MB.defType Definition
def)
ConstRef O
ccon <- TCM (ConstRef O) -> StateT S TCM (ConstRef O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (ConstRef O) -> StateT S TCM (ConstRef O))
-> TCM (ConstRef O) -> StateT S TCM (ConstRef O)
forall a b. (a -> b) -> a -> b
$ IO (ConstRef O) -> TCM (ConstRef O)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ConstRef O) -> TCM (ConstRef O))
-> IO (ConstRef O) -> TCM (ConstRef O)
forall a b. (a -> b) -> a -> b
$ ConstDef O -> IO (ConstRef O)
forall a. a -> IO (IORef a)
newIORef (ConstDef :: forall o. ArgName -> o -> MExp o -> DeclCont o -> Int -> ConstDef o
ConstDef {cdname :: ArgName
cdname = QName -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow QName
name ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ ".CONS", cdorigin :: O
cdorigin = ((Int, [Arg QName]) -> Maybe (Int, [Arg QName])
forall a. a -> Maybe a
Just (Int
nomi,[Arg QName]
conflds), QName
conname), cdtype :: MExp O
cdtype = MExp O
forall a. HasCallStack => a
__IMPOSSIBLE__, cdcont :: DeclCont O
cdcont = Int -> DeclCont O
forall o. Int -> DeclCont o
Constructor (Int
nomi Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
dfv), cddeffreevars :: Int
cddeffreevars = Int
dfv})
ConstRef O
c <- TCM (ConstRef O) -> StateT S TCM (ConstRef O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (ConstRef O) -> StateT S TCM (ConstRef O))
-> TCM (ConstRef O) -> StateT S TCM (ConstRef O)
forall a b. (a -> b) -> a -> b
$ IO (ConstRef O) -> TCM (ConstRef O)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ConstRef O) -> TCM (ConstRef O))
-> IO (ConstRef O) -> TCM (ConstRef O)
forall a b. (a -> b) -> a -> b
$ ConstDef O -> IO (ConstRef O)
forall a. a -> IO (IORef a)
newIORef (ConstDef :: forall o. ArgName -> o -> MExp o -> DeclCont o -> Int -> ConstDef o
ConstDef {cdname :: ArgName
cdname = QName -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow QName
name, cdorigin :: O
cdorigin = (Maybe (Int, [Arg QName])
forall a. Maybe a
Nothing, QName
name), cdtype :: MExp O
cdtype = MExp O
forall a. HasCallStack => a
__IMPOSSIBLE__, cdcont :: DeclCont O
cdcont = [ConstRef O] -> [ConstRef O] -> DeclCont O
forall o. [ConstRef o] -> [ConstRef o] -> DeclCont o
Datatype [ConstRef O
ccon] [], cddeffreevars :: Int
cddeffreevars = Int
dfv})
(S -> S) -> StateT S TCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\s :: S
s -> S
s {sConsts :: MapS QName (TMode, ConstRef O)
sConsts = (QName
-> (TMode, ConstRef O)
-> Map QName (TMode, ConstRef O)
-> Map QName (TMode, ConstRef O)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert QName
name (TMode
mode, ConstRef O
c) Map QName (TMode, ConstRef O)
cmap, QName
name QName -> [QName] -> [QName]
forall a. a -> [a] -> [a]
: MapS QName (TMode, ConstRef O) -> [QName]
forall a b. (a, b) -> b
snd (S -> MapS QName (TMode, ConstRef O)
sConsts S
s))})
ConstRef O -> StateT S TCM (ConstRef O)
forall (m :: * -> *) a. Monad m => a -> m a
return (ConstRef O -> StateT S TCM (ConstRef O))
-> ConstRef O -> StateT S TCM (ConstRef O)
forall a b. (a -> b) -> a -> b
$ if Bool
iscon then ConstRef O
ccon else ConstRef O
c
_ -> do
Map QName (TMode, ConstRef O)
cmap <- MapS QName (TMode, ConstRef O) -> Map QName (TMode, ConstRef O)
forall a b. (a, b) -> a
fst (MapS QName (TMode, ConstRef O) -> Map QName (TMode, ConstRef O))
-> StateT S TCM (MapS QName (TMode, ConstRef O))
-> StateT S TCM (Map QName (TMode, ConstRef O))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` (S -> MapS QName (TMode, ConstRef O))
-> StateT S TCM (MapS QName (TMode, ConstRef O))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets S -> MapS QName (TMode, ConstRef O)
sConsts
case QName -> Map QName (TMode, ConstRef O) -> Maybe (TMode, ConstRef O)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup QName
name Map QName (TMode, ConstRef O)
cmap of
Just (mode' :: TMode
mode', c :: ConstRef O
c) ->
ConstRef O -> StateT S TCM (ConstRef O)
forall (m :: * -> *) a. Monad m => a -> m a
return ConstRef O
c
Nothing -> do
(miscon :: Maybe (Int, [Arg QName])
miscon, sname :: ArgName
sname) <- if Bool
iscon then do
let MB.Constructor {conPars :: Defn -> Int
MB.conPars = Int
npar, conData :: Defn -> QName
MB.conData = QName
dname, conSrcCon :: Defn -> ConHead
MB.conSrcCon = ConHead
ch} = Definition -> Defn
MB.theDef Definition
def
(Maybe (Int, [Arg QName]), ArgName)
-> StateT S TCM (Maybe (Int, [Arg QName]), ArgName)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Int, [Arg QName]) -> Maybe (Int, [Arg QName])
forall a. a -> Maybe a
Just (Int
npar,ConHead -> [Arg QName]
I.conFields ConHead
ch), QName -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow QName
dname ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ "." ArgName -> ArgName -> ArgName
forall a. [a] -> [a] -> [a]
++ Name -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow (QName -> Name
I.qnameName QName
name))
else
(Maybe (Int, [Arg QName]), ArgName)
-> StateT S TCM (Maybe (Int, [Arg QName]), ArgName)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Int, [Arg QName])
forall a. Maybe a
Nothing, QName -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow QName
name)
MetaId
mainm <- (S -> MetaId) -> StateT S TCM MetaId
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets S -> MetaId
sMainMeta
Int
dfv <- TCMT IO Int -> StateT S TCM Int
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Int -> StateT S TCM Int)
-> TCMT IO Int -> StateT S TCM Int
forall a b. (a -> b) -> a -> b
$ MetaId -> QName -> TCMT IO Int
getdfv MetaId
mainm QName
name
ConstRef O
c <- TCM (ConstRef O) -> StateT S TCM (ConstRef O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (ConstRef O) -> StateT S TCM (ConstRef O))
-> TCM (ConstRef O) -> StateT S TCM (ConstRef O)
forall a b. (a -> b) -> a -> b
$ IO (ConstRef O) -> TCM (ConstRef O)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ConstRef O) -> TCM (ConstRef O))
-> IO (ConstRef O) -> TCM (ConstRef O)
forall a b. (a -> b) -> a -> b
$ ConstDef O -> IO (ConstRef O)
forall a. a -> IO (IORef a)
newIORef (ConstDef :: forall o. ArgName -> o -> MExp o -> DeclCont o -> Int -> ConstDef o
ConstDef {cdname :: ArgName
cdname = ArgName
sname, cdorigin :: O
cdorigin = (Maybe (Int, [Arg QName])
miscon, QName
name), cdtype :: MExp O
cdtype = MExp O
forall a. HasCallStack => a
__IMPOSSIBLE__, cdcont :: DeclCont O
cdcont = DeclCont O
forall a. HasCallStack => a
__IMPOSSIBLE__, cddeffreevars :: Int
cddeffreevars = Int
dfv})
(S -> S) -> StateT S TCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\s :: S
s -> S
s {sConsts :: MapS QName (TMode, ConstRef O)
sConsts = (QName
-> (TMode, ConstRef O)
-> Map QName (TMode, ConstRef O)
-> Map QName (TMode, ConstRef O)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert QName
name (TMode
mode, ConstRef O
c) Map QName (TMode, ConstRef O)
cmap, QName
name QName -> [QName] -> [QName]
forall a. a -> [a] -> [a]
: MapS QName (TMode, ConstRef O) -> [QName]
forall a b. (a, b) -> b
snd (S -> MapS QName (TMode, ConstRef O)
sConsts S
s))})
ConstRef O -> StateT S TCM (ConstRef O)
forall (m :: * -> *) a. Monad m => a -> m a
return ConstRef O
c
getdfv :: I.MetaId -> A.QName -> MB.TCM Cm.Nat
getdfv :: MetaId -> QName -> TCMT IO Int
getdfv mainm :: MetaId
mainm name :: QName
name = do
MetaVariable
mv <- MetaId -> TCM MetaVariable
forall (m :: * -> *).
(MonadFail m, ReadTCState m) =>
MetaId -> m MetaVariable
lookupMeta MetaId
mainm
Closure Range -> TCMT IO Int -> TCMT IO Int
forall a. Closure Range -> TCM a -> TCM a
withMetaInfo (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mv) (TCMT IO Int -> TCMT IO Int) -> TCMT IO Int -> TCMT IO Int
forall a b. (a -> b) -> a -> b
$ QName -> TCMT IO Int
forall (m :: * -> *).
(Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
QName -> m Int
getDefFreeVars QName
name
getMeta :: I.MetaId -> TOM (Metavar (Exp O) (RefInfo O))
getMeta :: MetaId -> TOM (Metavar (Exp O) (RefInfo O))
getMeta name :: MetaId
name = do
Map
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
mmap <- MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> Map
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
forall a b. (a, b) -> a
fst (MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> Map
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId]))
-> StateT
S
TCM
(MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId]))
-> StateT
S
TCM
(Map
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId]))
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
`liftM` (S
-> MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId]))
-> StateT
S
TCM
(MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId]))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets S
-> MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
sMetas
case MetaId
-> Map
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> Maybe
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup MetaId
name Map
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
mmap of
Just (m :: Metavar (Exp O) (RefInfo O)
m, _, _) ->
Metavar (Exp O) (RefInfo O) -> TOM (Metavar (Exp O) (RefInfo O))
forall (m :: * -> *) a. Monad m => a -> m a
return Metavar (Exp O) (RefInfo O)
m
Nothing -> do
Metavar (Exp O) (RefInfo O)
m <- TCM (Metavar (Exp O) (RefInfo O))
-> TOM (Metavar (Exp O) (RefInfo O))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (Metavar (Exp O) (RefInfo O))
-> TOM (Metavar (Exp O) (RefInfo O)))
-> TCM (Metavar (Exp O) (RefInfo O))
-> TOM (Metavar (Exp O) (RefInfo O))
forall a b. (a -> b) -> a -> b
$ IO (Metavar (Exp O) (RefInfo O))
-> TCM (Metavar (Exp O) (RefInfo O))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO (Metavar (Exp O) (RefInfo O))
forall a blk. IO (Metavar a blk)
initMeta
(S -> S) -> StateT S TCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((S -> S) -> StateT S TCM ()) -> (S -> S) -> StateT S TCM ()
forall a b. (a -> b) -> a -> b
$ \ s :: S
s -> S
s { sMetas :: MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
sMetas = (MetaId
-> (Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]),
[MetaId])
-> Map
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> Map
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert MetaId
name (Metavar (Exp O) (RefInfo O)
m, Maybe (MExp O, [MExp O])
forall a. Maybe a
Nothing, []) Map
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
mmap, MetaId
name MetaId -> [MetaId] -> [MetaId]
forall a. a -> [a] -> [a]
: MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> [MetaId]
forall a b. (a, b) -> b
snd (S
-> MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
sMetas S
s)) }
Metavar (Exp O) (RefInfo O) -> TOM (Metavar (Exp O) (RefInfo O))
forall (m :: * -> *) a. Monad m => a -> m a
return Metavar (Exp O) (RefInfo O)
m
getEqs :: MB.TCM [(Bool, I.Term, I.Term)]
getEqs :: TCM [(Bool, Term, Term)]
getEqs = TCMT IO [ProblemConstraint]
-> (ProblemConstraint -> TCMT IO (Maybe (Bool, Term, Term)))
-> TCM [(Bool, Term, Term)]
forall (m :: * -> *) a b.
Monad m =>
m [a] -> (a -> m (Maybe b)) -> m [b]
forMaybeMM TCMT IO [ProblemConstraint]
forall (m :: * -> *). ReadTCState m => m [ProblemConstraint]
getAllConstraints ((ProblemConstraint -> TCMT IO (Maybe (Bool, Term, Term)))
-> TCM [(Bool, Term, Term)])
-> (ProblemConstraint -> TCMT IO (Maybe (Bool, Term, Term)))
-> TCM [(Bool, Term, Term)]
forall a b. (a -> b) -> a -> b
$ \ eqc :: ProblemConstraint
eqc -> do
ProblemConstraint
neqc <- ProblemConstraint -> TCMT IO ProblemConstraint
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise ProblemConstraint
eqc
case Closure Constraint -> Constraint
forall a. Closure a -> a
MB.clValue (Closure Constraint -> Constraint)
-> Closure Constraint -> Constraint
forall a b. (a -> b) -> a -> b
$ ProblemConstraint -> Closure Constraint
MB.theConstraint ProblemConstraint
neqc of
MB.ValueCmp ineq :: Comparison
ineq _ i :: Term
i e :: Term
e -> do
Term
ei <- Term -> TCMT IO Term
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) =>
a -> m a
etaContract Term
i
Term
ee <- Term -> TCMT IO Term
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) =>
a -> m a
etaContract Term
e
Maybe (Bool, Term, Term) -> TCMT IO (Maybe (Bool, Term, Term))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Bool, Term, Term) -> TCMT IO (Maybe (Bool, Term, Term)))
-> Maybe (Bool, Term, Term) -> TCMT IO (Maybe (Bool, Term, Term))
forall a b. (a -> b) -> a -> b
$ (Bool, Term, Term) -> Maybe (Bool, Term, Term)
forall a. a -> Maybe a
Just (Comparison -> Bool
tomyIneq Comparison
ineq, Term
ee, Term
ei)
MB.Guarded (MB.UnBlock _) _pid :: ProblemId
_pid -> Maybe (Bool, Term, Term) -> TCMT IO (Maybe (Bool, Term, Term))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Bool, Term, Term)
forall a. Maybe a
Nothing
_ -> Maybe (Bool, Term, Term) -> TCMT IO (Maybe (Bool, Term, Term))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Bool, Term, Term)
forall a. Maybe a
Nothing
copatternsNotImplemented :: MB.TCM a
copatternsNotImplemented :: TCM a
copatternsNotImplemented = TypeError -> TCM a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
MB.typeError (TypeError -> TCM a) -> TypeError -> TCM a
forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
MB.NotImplemented (ArgName -> TypeError) -> ArgName -> TypeError
forall a b. (a -> b) -> a -> b
$
"The Agda synthesizer (Agsy) does not support copatterns yet"
literalsNotImplemented :: MB.TCM a
literalsNotImplemented :: TCM a
literalsNotImplemented = TypeError -> TCM a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
MB.typeError (TypeError -> TCM a) -> TypeError -> TCM a
forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
MB.NotImplemented (ArgName -> TypeError) -> ArgName -> TypeError
forall a b. (a -> b) -> a -> b
$
"The Agda synthesizer (Agsy) does not support literals yet"
hitsNotImplemented :: MB.TCM a
hitsNotImplemented :: TCM a
hitsNotImplemented = TypeError -> TCM a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
MB.typeError (TypeError -> TCM a) -> TypeError -> TCM a
forall a b. (a -> b) -> a -> b
$ ArgName -> TypeError
MB.NotImplemented (ArgName -> TypeError) -> ArgName -> TypeError
forall a b. (a -> b) -> a -> b
$
"The Agda synthesizer (Agsy) does not support HITs yet"
class Conversion m a b where
convert :: a -> m b
instance Conversion TOM [I.Clause] [([Pat O], MExp O)] where
convert :: [Clause] -> TOM [([Pat O], MExp O)]
convert = ([Maybe ([Pat O], MExp O)] -> [([Pat O], MExp O)])
-> StateT S TCM [Maybe ([Pat O], MExp O)]
-> TOM [([Pat O], MExp O)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Maybe ([Pat O], MExp O)] -> [([Pat O], MExp O)]
forall a. [Maybe a] -> [a]
catMaybes (StateT S TCM [Maybe ([Pat O], MExp O)] -> TOM [([Pat O], MExp O)])
-> ([Clause] -> StateT S TCM [Maybe ([Pat O], MExp O)])
-> [Clause]
-> TOM [([Pat O], MExp O)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Clause -> StateT S TCM (Maybe ([Pat O], MExp O)))
-> [Clause] -> StateT S TCM [Maybe ([Pat O], MExp O)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Clause -> StateT S TCM (Maybe ([Pat O], MExp O))
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert
instance Conversion TOM I.Clause (Maybe ([Pat O], MExp O)) where
convert :: Clause -> StateT S TCM (Maybe ([Pat O], MExp O))
convert cl :: Clause
cl = do
let
body :: Maybe Term
body = Clause -> Maybe Term
I.clauseBody Clause
cl
pats :: [Arg DeBruijnPattern]
pats = Clause -> [Arg DeBruijnPattern]
I.clausePats Clause
cl
[Pat O]
pats' <- (Arg Pattern -> StateT S TCM (Pat O))
-> [Arg Pattern] -> StateT S TCM [Pat O]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Arg Pattern -> StateT S TCM (Pat O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert ([Arg DeBruijnPattern] -> [Arg Pattern]
forall a b i. LabelPatVars a b i => b -> a
IP.unnumberPatVars [Arg DeBruijnPattern]
pats :: [Cm.Arg I.Pattern])
Maybe (MExp O)
body' <- (Term -> StateT S TCM (MExp O))
-> Maybe Term -> StateT S TCM (Maybe (MExp O))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Term -> StateT S TCM (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert (Maybe Term -> StateT S TCM (Maybe (MExp O)))
-> StateT S TCM (Maybe Term) -> StateT S TCM (Maybe (MExp O))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO (Maybe Term) -> StateT S TCM (Maybe Term)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Maybe Term -> TCMT IO (Maybe Term)
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Maybe Term
body)
Maybe ([Pat O], MExp O) -> StateT S TCM (Maybe ([Pat O], MExp O))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([Pat O], MExp O) -> StateT S TCM (Maybe ([Pat O], MExp O)))
-> Maybe ([Pat O], MExp O)
-> StateT S TCM (Maybe ([Pat O], MExp O))
forall a b. (a -> b) -> a -> b
$ ([Pat O]
pats',) (MExp O -> ([Pat O], MExp O))
-> Maybe (MExp O) -> Maybe ([Pat O], MExp O)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (MExp O)
body'
instance Conversion TOM (Cm.Arg I.Pattern) (Pat O) where
convert :: Arg Pattern -> StateT S TCM (Pat O)
convert p :: Arg Pattern
p = case Arg Pattern -> Pattern
forall e. Arg e -> e
Cm.unArg Arg Pattern
p of
I.IApplyP _ _ _ n :: ArgName
n -> Pat O -> StateT S TCM (Pat O)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pat O -> StateT S TCM (Pat O)) -> Pat O -> StateT S TCM (Pat O)
forall a b. (a -> b) -> a -> b
$ ArgName -> Pat O
forall o. ArgName -> Pat o
PatVar (ArgName -> ArgName
forall a. Show a => a -> ArgName
show ArgName
n)
I.VarP _ n :: ArgName
n -> Pat O -> StateT S TCM (Pat O)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pat O -> StateT S TCM (Pat O)) -> Pat O -> StateT S TCM (Pat O)
forall a b. (a -> b) -> a -> b
$ ArgName -> Pat O
forall o. ArgName -> Pat o
PatVar (ArgName -> ArgName
forall a. Show a => a -> ArgName
show ArgName
n)
I.DotP _ _ -> Pat O -> StateT S TCM (Pat O)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pat O -> StateT S TCM (Pat O)) -> Pat O -> StateT S TCM (Pat O)
forall a b. (a -> b) -> a -> b
$ ArgName -> Pat O
forall o. ArgName -> Pat o
PatVar "_"
I.ConP con :: ConHead
con _ pats :: [NamedArg Pattern]
pats -> do
let n :: QName
n = ConHead -> QName
I.conName ConHead
con
ConstRef O
c <- Bool -> QName -> TMode -> StateT S TCM (ConstRef O)
getConst Bool
True QName
n TMode
TMAll
[Pat O]
pats' <- (NamedArg Pattern -> StateT S TCM (Pat O))
-> [NamedArg Pattern] -> StateT S TCM [Pat O]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Arg Pattern -> StateT S TCM (Pat O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert (Arg Pattern -> StateT S TCM (Pat O))
-> (NamedArg Pattern -> Arg Pattern)
-> NamedArg Pattern
-> StateT S TCM (Pat O)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName Pattern -> Pattern)
-> NamedArg Pattern -> Arg Pattern
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName Pattern -> Pattern
forall name a. Named name a -> a
Cm.namedThing) [NamedArg Pattern]
pats
Definition
def <- TCM Definition -> StateT S TCM Definition
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Definition -> StateT S TCM Definition)
-> TCM Definition -> StateT S TCM Definition
forall a b. (a -> b) -> a -> b
$ QName -> TCM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
n
ConstDef O
cc <- TCM (ConstDef O) -> StateT S TCM (ConstDef O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (ConstDef O) -> StateT S TCM (ConstDef O))
-> TCM (ConstDef O) -> StateT S TCM (ConstDef O)
forall a b. (a -> b) -> a -> b
$ IO (ConstDef O) -> TCM (ConstDef O)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ConstDef O) -> TCM (ConstDef O))
-> IO (ConstDef O) -> TCM (ConstDef O)
forall a b. (a -> b) -> a -> b
$ ConstRef O -> IO (ConstDef O)
forall a. IORef a -> IO a
readIORef ConstRef O
c
let Just (npar :: Int
npar,_) = O -> Maybe (Int, [Arg QName])
forall a b. (a, b) -> a
fst (O -> Maybe (Int, [Arg QName])) -> O -> Maybe (Int, [Arg QName])
forall a b. (a -> b) -> a -> b
$ ConstDef O -> O
forall o. ConstDef o -> o
cdorigin ConstDef O
cc
Pat O -> StateT S TCM (Pat O)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pat O -> StateT S TCM (Pat O)) -> Pat O -> StateT S TCM (Pat O)
forall a b. (a -> b) -> a -> b
$ ConstRef O -> [Pat O] -> Pat O
forall o. ConstRef o -> [Pat o] -> Pat o
PatConApp ConstRef O
c (Int -> Pat O -> [Pat O]
forall a. Int -> a -> [a]
replicate Int
npar Pat O
forall o. Pat o
PatExp [Pat O] -> [Pat O] -> [Pat O]
forall a. [a] -> [a] -> [a]
++ [Pat O]
pats')
I.ProjP{} -> TCMT IO (Pat O) -> StateT S TCM (Pat O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCMT IO (Pat O)
forall a. TCM a
copatternsNotImplemented
I.LitP{} -> TCMT IO (Pat O) -> StateT S TCM (Pat O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCMT IO (Pat O)
forall a. TCM a
literalsNotImplemented
I.DefP{} -> TCMT IO (Pat O) -> StateT S TCM (Pat O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCMT IO (Pat O)
forall a. TCM a
hitsNotImplemented
instance Conversion TOM I.Type (MExp O) where
convert :: Type -> StateT S TCM (MExp O)
convert (I.El _ t :: Term
t) = Term -> StateT S TCM (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Term
t
instance Conversion TOM I.Term (MExp O) where
convert :: Term -> StateT S TCM (MExp O)
convert v0 :: Term
v0 =
case Term -> Term
I.unSpine Term
v0 of
I.Var v :: Int
v es :: Elims
es -> do
let Just as :: [Arg Term]
as = Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
I.allApplyElims Elims
es
MArgList O
as' <- [Arg Term] -> StateT S TCM (MArgList O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert [Arg Term]
as
MExp O -> StateT S TCM (MExp O)
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp O -> StateT S TCM (MExp O))
-> MExp O -> StateT S TCM (MExp O)
forall a b. (a -> b) -> a -> b
$ Exp O -> MExp O
forall a blk. a -> MM a blk
NotM (Exp O -> MExp O) -> Exp O -> MExp O
forall a b. (a -> b) -> a -> b
$ Maybe (Metavar (Exp O) (RefInfo O))
-> OKHandle (RefInfo O) -> Elr O -> MArgList O -> Exp O
forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (Metavar (Exp O) (RefInfo O))
forall a. Maybe a
Nothing (OKVal -> OKHandle (RefInfo O)
forall a blk. a -> MM a blk
NotM OKVal
OKVal) (Int -> Elr O
forall o. Int -> Elr o
Var Int
v) MArgList O
as'
I.Lam info :: ArgInfo
info b :: Abs Term
b -> do
MExp O
b' <- Term -> StateT S TCM (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert (Abs Term -> Term
forall t a. Subst t a => Abs a -> a
I.absBody Abs Term
b)
MExp O -> StateT S TCM (MExp O)
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp O -> StateT S TCM (MExp O))
-> MExp O -> StateT S TCM (MExp O)
forall a b. (a -> b) -> a -> b
$ Exp O -> MExp O
forall a blk. a -> MM a blk
NotM (Exp O -> MExp O) -> Exp O -> MExp O
forall a b. (a -> b) -> a -> b
$ Hiding -> Abs (MExp O) -> Exp O
forall o. Hiding -> Abs (MExp o) -> Exp o
Lam (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info) (MId -> MExp O -> Abs (MExp O)
forall a. MId -> a -> Abs a
Abs (ArgName -> MId
Id (ArgName -> MId) -> ArgName -> MId
forall a b. (a -> b) -> a -> b
$ Abs Term -> ArgName
forall a. Abs a -> ArgName
I.absName Abs Term
b) MExp O
b')
t :: Term
t@I.Lit{} -> do
Term
t <- TCMT IO Term -> StateT S TCM Term
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Term -> StateT S TCM Term)
-> TCMT IO Term -> StateT S TCM Term
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
Term -> m Term
constructorForm Term
t
case Term
t of
I.Lit{} -> TCMT IO (MExp O) -> StateT S TCM (MExp O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCMT IO (MExp O)
forall a. TCM a
literalsNotImplemented
_ -> Term -> StateT S TCM (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Term
t
I.Level l :: Level
l -> Term -> StateT S TCM (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert (Term -> StateT S TCM (MExp O))
-> StateT S TCM Term -> StateT S TCM (MExp O)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Term -> StateT S TCM Term
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Level -> TCMT IO Term
forall (m :: * -> *). HasBuiltins m => Level -> m Term
reallyUnLevelView Level
l)
I.Def name :: QName
name es :: Elims
es -> do
let Just as :: [Arg Term]
as = Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
I.allApplyElims Elims
es
ConstRef O
c <- Bool -> QName -> TMode -> StateT S TCM (ConstRef O)
getConst Bool
False QName
name TMode
TMAll
MArgList O
as' <- [Arg Term] -> StateT S TCM (MArgList O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert [Arg Term]
as
MExp O -> StateT S TCM (MExp O)
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp O -> StateT S TCM (MExp O))
-> MExp O -> StateT S TCM (MExp O)
forall a b. (a -> b) -> a -> b
$ Exp O -> MExp O
forall a blk. a -> MM a blk
NotM (Exp O -> MExp O) -> Exp O -> MExp O
forall a b. (a -> b) -> a -> b
$ Maybe (Metavar (Exp O) (RefInfo O))
-> OKHandle (RefInfo O) -> Elr O -> MArgList O -> Exp O
forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (Metavar (Exp O) (RefInfo O))
forall a. Maybe a
Nothing (OKVal -> OKHandle (RefInfo O)
forall a blk. a -> MM a blk
NotM OKVal
OKVal) (ConstRef O -> Elr O
forall o. ConstRef o -> Elr o
Const ConstRef O
c) MArgList O
as'
I.Con con :: ConHead
con ci :: ConInfo
ci es :: Elims
es -> do
let Just as :: [Arg Term]
as = Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
I.allApplyElims Elims
es
let name :: QName
name = ConHead -> QName
I.conName ConHead
con
ConstRef O
c <- Bool -> QName -> TMode -> StateT S TCM (ConstRef O)
getConst Bool
True QName
name TMode
TMAll
MArgList O
as' <- [Arg Term] -> StateT S TCM (MArgList O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert [Arg Term]
as
Definition
def <- TCM Definition -> StateT S TCM Definition
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Definition -> StateT S TCM Definition)
-> TCM Definition -> StateT S TCM Definition
forall a b. (a -> b) -> a -> b
$ QName -> TCM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
name
ConstDef O
cc <- TCM (ConstDef O) -> StateT S TCM (ConstDef O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (ConstDef O) -> StateT S TCM (ConstDef O))
-> TCM (ConstDef O) -> StateT S TCM (ConstDef O)
forall a b. (a -> b) -> a -> b
$ IO (ConstDef O) -> TCM (ConstDef O)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ConstDef O) -> TCM (ConstDef O))
-> IO (ConstDef O) -> TCM (ConstDef O)
forall a b. (a -> b) -> a -> b
$ ConstRef O -> IO (ConstDef O)
forall a. IORef a -> IO a
readIORef ConstRef O
c
let Just (npar :: Int
npar,_) = O -> Maybe (Int, [Arg QName])
forall a b. (a, b) -> a
fst (O -> Maybe (Int, [Arg QName])) -> O -> Maybe (Int, [Arg QName])
forall a b. (a -> b) -> a -> b
$ ConstDef O -> O
forall o. ConstDef o -> o
cdorigin ConstDef O
cc
MExp O -> StateT S TCM (MExp O)
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp O -> StateT S TCM (MExp O))
-> MExp O -> StateT S TCM (MExp O)
forall a b. (a -> b) -> a -> b
$ Exp O -> MExp O
forall a blk. a -> MM a blk
NotM (Exp O -> MExp O) -> Exp O -> MExp O
forall a b. (a -> b) -> a -> b
$ Maybe (Metavar (Exp O) (RefInfo O))
-> OKHandle (RefInfo O) -> Elr O -> MArgList O -> Exp O
forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (Metavar (Exp O) (RefInfo O))
forall a. Maybe a
Nothing (OKVal -> OKHandle (RefInfo O)
forall a blk. a -> MM a blk
NotM OKVal
OKVal) (ConstRef O -> Elr O
forall o. ConstRef o -> Elr o
Const ConstRef O
c) ((MArgList O -> Int -> MArgList O)
-> MArgList O -> [Int] -> MArgList O
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\x :: MArgList O
x _ -> ArgList O -> MArgList O
forall a blk. a -> MM a blk
NotM (ArgList O -> MArgList O) -> ArgList O -> MArgList O
forall a b. (a -> b) -> a -> b
$ MArgList O -> ArgList O
forall o. MArgList o -> ArgList o
ALConPar MArgList O
x) MArgList O
as' [1..Int
npar])
I.Pi (I.Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info, unDom :: forall t e. Dom' t e -> e
unDom = Type
x}) b :: Abs Type
b -> do
let y :: Type
y = Abs Type -> Type
forall t a. Subst t a => Abs a -> a
I.absBody Abs Type
b
name :: ArgName
name = Abs Type -> ArgName
forall a. Abs a -> ArgName
I.absName Abs Type
b
MExp O
x' <- Type -> StateT S TCM (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Type
x
MExp O
y' <- Type -> StateT S TCM (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Type
y
MExp O -> StateT S TCM (MExp O)
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp O -> StateT S TCM (MExp O))
-> MExp O -> StateT S TCM (MExp O)
forall a b. (a -> b) -> a -> b
$ Exp O -> MExp O
forall a blk. a -> MM a blk
NotM (Exp O -> MExp O) -> Exp O -> MExp O
forall a b. (a -> b) -> a -> b
$ Maybe (Metavar (Exp O) (RefInfo O))
-> Hiding -> Bool -> MExp O -> Abs (MExp O) -> Exp O
forall o.
Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
Pi Maybe (Metavar (Exp O) (RefInfo O))
forall a. Maybe a
Nothing (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info) (Int -> Type -> Bool
forall a. Free a => Int -> a -> Bool
Free.freeIn 0 Type
y) MExp O
x' (MId -> MExp O -> Abs (MExp O)
forall a. MId -> a -> Abs a
Abs (ArgName -> MId
Id ArgName
name) MExp O
y')
I.Sort (I.Type (I.ClosedLevel l :: Integer
l)) -> MExp O -> StateT S TCM (MExp O)
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp O -> StateT S TCM (MExp O))
-> MExp O -> StateT S TCM (MExp O)
forall a b. (a -> b) -> a -> b
$ Exp O -> MExp O
forall a blk. a -> MM a blk
NotM (Exp O -> MExp O) -> Exp O -> MExp O
forall a b. (a -> b) -> a -> b
$ Sort -> Exp O
forall o. Sort -> Exp o
Sort (Sort -> Exp O) -> Sort -> Exp O
forall a b. (a -> b) -> a -> b
$ Int -> Sort
Set (Int -> Sort) -> Int -> Sort
forall a b. (a -> b) -> a -> b
$ Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
l
I.Sort _ -> MExp O -> StateT S TCM (MExp O)
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp O -> StateT S TCM (MExp O))
-> MExp O -> StateT S TCM (MExp O)
forall a b. (a -> b) -> a -> b
$ Exp O -> MExp O
forall a blk. a -> MM a blk
NotM (Exp O -> MExp O) -> Exp O -> MExp O
forall a b. (a -> b) -> a -> b
$ Sort -> Exp O
forall o. Sort -> Exp o
Sort Sort
UnknownSort
I.Dummy{}-> MExp O -> StateT S TCM (MExp O)
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp O -> StateT S TCM (MExp O))
-> MExp O -> StateT S TCM (MExp O)
forall a b. (a -> b) -> a -> b
$ Exp O -> MExp O
forall a blk. a -> MM a blk
NotM (Exp O -> MExp O) -> Exp O -> MExp O
forall a b. (a -> b) -> a -> b
$ Sort -> Exp O
forall o. Sort -> Exp o
Sort Sort
UnknownSort
t :: Term
t@I.MetaV{} -> do
Term
t <- TCMT IO Term -> StateT S TCM Term
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Term -> StateT S TCM Term)
-> TCMT IO Term -> StateT S TCM Term
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Term
forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate Term
t
case Term
t of
I.MetaV mid :: MetaId
mid _ -> do
Maybe MetaId
mcurmeta <- (S -> Maybe MetaId) -> TOM (Maybe MetaId)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets S -> Maybe MetaId
sCurMeta
case Maybe MetaId
mcurmeta of
Nothing -> () -> StateT S TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just curmeta :: MetaId
curmeta ->
(S -> S) -> StateT S TCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((S -> S) -> StateT S TCM ()) -> (S -> S) -> StateT S TCM ()
forall a b. (a -> b) -> a -> b
$ \ s :: S
s -> S
s { sMetas :: MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
sMetas = ( ((Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> (Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]),
[MetaId]))
-> MetaId
-> Map
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> Map
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust (\(m :: Metavar (Exp O) (RefInfo O)
m, x :: Maybe (MExp O, [MExp O])
x, deps :: [MetaId]
deps) -> (Metavar (Exp O) (RefInfo O)
m, Maybe (MExp O, [MExp O])
x, MetaId
mid MetaId -> [MetaId] -> [MetaId]
forall a. a -> [a] -> [a]
: [MetaId]
deps)) MetaId
curmeta (MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> Map
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
forall a b. (a, b) -> a
fst (MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> Map
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId]))
-> MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> Map
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
forall a b. (a -> b) -> a -> b
$ S
-> MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
sMetas S
s)
, MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> [MetaId]
forall a b. (a, b) -> b
snd (MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> [MetaId])
-> MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> [MetaId]
forall a b. (a -> b) -> a -> b
$ S
-> MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
sMetas S
s
) }
Metavar (Exp O) (RefInfo O)
m <- MetaId -> TOM (Metavar (Exp O) (RefInfo O))
getMeta MetaId
mid
MExp O -> StateT S TCM (MExp O)
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp O -> StateT S TCM (MExp O))
-> MExp O -> StateT S TCM (MExp O)
forall a b. (a -> b) -> a -> b
$ Metavar (Exp O) (RefInfo O) -> MExp O
forall a blk. Metavar a blk -> MM a blk
Meta Metavar (Exp O) (RefInfo O)
m
_ -> Term -> StateT S TCM (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Term
t
I.DontCare _ -> MExp O -> StateT S TCM (MExp O)
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp O -> StateT S TCM (MExp O))
-> MExp O -> StateT S TCM (MExp O)
forall a b. (a -> b) -> a -> b
$ Exp O -> MExp O
forall a blk. a -> MM a blk
NotM Exp O
forall o. Exp o
dontCare
instance Conversion TOM a b => Conversion TOM (Cm.Arg a) (Hiding, b) where
convert :: Arg a -> TOM (Hiding, b)
convert (Cm.Arg info :: ArgInfo
info a :: a
a) = (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info,) (b -> (Hiding, b)) -> StateT S TCM b -> TOM (Hiding, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> StateT S TCM b
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert a
a
instance Conversion TOM I.Args (MM (ArgList O) (RefInfo O)) where
convert :: [Arg Term] -> StateT S TCM (MArgList O)
convert as :: [Arg Term]
as = ArgList O -> MArgList O
forall a blk. a -> MM a blk
NotM (ArgList O -> MArgList O)
-> ([(Hiding, MExp O)] -> ArgList O)
-> [(Hiding, MExp O)]
-> MArgList O
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Hiding, MExp O) -> ArgList O -> ArgList O)
-> ArgList O -> [(Hiding, MExp O)] -> ArgList O
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (hid :: Hiding
hid,t :: MExp O
t) -> Hiding -> MExp O -> MArgList O -> ArgList O
forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
hid MExp O
t (MArgList O -> ArgList O)
-> (ArgList O -> MArgList O) -> ArgList O -> ArgList O
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ArgList O -> MArgList O
forall a blk. a -> MM a blk
NotM) ArgList O
forall o. ArgList o
ALNil
([(Hiding, MExp O)] -> MArgList O)
-> StateT S TCM [(Hiding, MExp O)] -> StateT S TCM (MArgList O)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Arg Term -> StateT S TCM (Hiding, MExp O))
-> [Arg Term] -> StateT S TCM [(Hiding, MExp O)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Arg Term -> StateT S TCM (Hiding, MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert [Arg Term]
as
tomyIneq :: MB.Comparison -> Bool
tomyIneq :: Comparison -> Bool
tomyIneq MB.CmpEq = Bool
False
tomyIneq MB.CmpLeq = Bool
True
fmType :: I.MetaId -> I.Type -> Bool
fmType :: MetaId -> Type -> Bool
fmType m :: MetaId
m (I.El _ t :: Term
t) = MetaId -> Term -> Bool
fmExp MetaId
m Term
t
fmExp :: I.MetaId -> I.Term -> Bool
fmExp :: MetaId -> Term -> Bool
fmExp m :: MetaId
m (I.Var _ as :: Elims
as) = MetaId -> [Arg Term] -> Bool
fmExps MetaId
m ([Arg Term] -> Bool) -> [Arg Term] -> Bool
forall a b. (a -> b) -> a -> b
$ Elims -> [Arg Term]
I.argsFromElims Elims
as
fmExp m :: MetaId
m (I.Lam _ b :: Abs Term
b) = MetaId -> Term -> Bool
fmExp MetaId
m (Abs Term -> Term
forall a. Abs a -> a
I.unAbs Abs Term
b)
fmExp m :: MetaId
m (I.Lit _) = Bool
False
fmExp m :: MetaId
m (I.Level (I.Max _ as :: [PlusLevel' Term]
as)) = (PlusLevel' Term -> Bool) -> [PlusLevel' Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (MetaId -> PlusLevel' Term -> Bool
fmLevel MetaId
m) [PlusLevel' Term]
as
fmExp m :: MetaId
m (I.Def _ as :: Elims
as) = MetaId -> [Arg Term] -> Bool
fmExps MetaId
m ([Arg Term] -> Bool) -> [Arg Term] -> Bool
forall a b. (a -> b) -> a -> b
$ Elims -> [Arg Term]
I.argsFromElims Elims
as
fmExp m :: MetaId
m (I.Con _ ci :: ConInfo
ci as :: Elims
as) = MetaId -> [Arg Term] -> Bool
fmExps MetaId
m ([Arg Term] -> Bool) -> [Arg Term] -> Bool
forall a b. (a -> b) -> a -> b
$ Elims -> [Arg Term]
I.argsFromElims Elims
as
fmExp m :: MetaId
m (I.Pi x :: Dom Type
x y :: Abs Type
y) = MetaId -> Type -> Bool
fmType MetaId
m (Dom Type -> Type
forall t e. Dom' t e -> e
I.unDom Dom Type
x) Bool -> Bool -> Bool
|| MetaId -> Type -> Bool
fmType MetaId
m (Abs Type -> Type
forall a. Abs a -> a
I.unAbs Abs Type
y)
fmExp m :: MetaId
m (I.Sort _) = Bool
False
fmExp m :: MetaId
m (I.MetaV mid :: MetaId
mid _) = MetaId
mid MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
m
fmExp m :: MetaId
m (I.DontCare _) = Bool
False
fmExp _ I.Dummy{} = Bool
False
fmExps :: I.MetaId -> I.Args -> Bool
fmExps :: MetaId -> [Arg Term] -> Bool
fmExps m :: MetaId
m [] = Bool
False
fmExps m :: MetaId
m (a :: Arg Term
a : as :: [Arg Term]
as) = MetaId -> Term -> Bool
fmExp MetaId
m (Arg Term -> Term
forall e. Arg e -> e
Cm.unArg Arg Term
a) Bool -> Bool -> Bool
|| MetaId -> [Arg Term] -> Bool
fmExps MetaId
m [Arg Term]
as
fmLevel :: I.MetaId -> I.PlusLevel -> Bool
fmLevel :: MetaId -> PlusLevel' Term -> Bool
fmLevel m :: MetaId
m (I.Plus _ l :: LevelAtom' Term
l) = case LevelAtom' Term
l of
I.MetaLevel m' :: MetaId
m' _ -> MetaId
m MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
m'
I.NeutralLevel _ v :: Term
v -> MetaId -> Term -> Bool
fmExp MetaId
m Term
v
I.BlockedLevel _ v :: Term
v -> MetaId -> Term -> Bool
fmExp MetaId
m Term
v
I.UnreducedLevel v :: Term
v -> MetaId -> Term -> Bool
fmExp MetaId
m Term
v
icnvh :: Hiding -> Cm.ArgInfo
icnvh :: Hiding -> ArgInfo
icnvh h :: Hiding
h = Hiding -> ArgInfo -> ArgInfo
forall a. LensHiding a => Hiding -> a -> a
Cm.setHiding Hiding
h (ArgInfo -> ArgInfo) -> ArgInfo -> ArgInfo
forall a b. (a -> b) -> a -> b
$
Origin -> ArgInfo -> ArgInfo
forall a. LensOrigin a => Origin -> a -> a
Cm.setOrigin Origin
o (ArgInfo -> ArgInfo) -> ArgInfo -> ArgInfo
forall a b. (a -> b) -> a -> b
$
ArgInfo
Cm.defaultArgInfo
where
o :: Origin
o = case Hiding
h of
NotHidden -> Origin
Cm.UserWritten
Instance{} -> Origin
Cm.Inserted
Hidden -> Origin
Cm.Inserted
instance Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b where
convert :: MM a (RefInfo O) -> MOT b
convert meta :: MM a (RefInfo O)
meta = case MM a (RefInfo O)
meta of
NotM a :: a
a -> a -> MOT b
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert a
a
Meta m :: Metavar a (RefInfo O)
m -> do
Maybe a
ma <- IO (Maybe a) -> ExceptT ArgName IO (Maybe a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Maybe a) -> ExceptT ArgName IO (Maybe a))
-> IO (Maybe a) -> ExceptT ArgName IO (Maybe a)
forall a b. (a -> b) -> a -> b
$ IORef (Maybe a) -> IO (Maybe a)
forall a. IORef a -> IO a
readIORef (IORef (Maybe a) -> IO (Maybe a))
-> IORef (Maybe a) -> IO (Maybe a)
forall a b. (a -> b) -> a -> b
$ Metavar a (RefInfo O) -> IORef (Maybe a)
forall a blk. Metavar a blk -> IORef (Maybe a)
mbind Metavar a (RefInfo O)
m
case Maybe a
ma of
Nothing -> ArgName -> MOT b
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError "meta not bound"
Just a :: a
a -> a -> MOT b
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert a
a
instance Conversion MOT a b => Conversion MOT (Abs a) (I.Abs b) where
convert :: Abs a -> MOT (Abs b)
convert (Abs mid :: MId
mid t :: a
t) = ArgName -> b -> Abs b
forall a. ArgName -> a -> Abs a
I.Abs ArgName
id (b -> Abs b) -> ExceptT ArgName IO b -> MOT (Abs b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> ExceptT ArgName IO b
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert a
t where
id :: ArgName
id = case MId
mid of
NoId -> "x"
Id id :: ArgName
id -> ArgName
id
instance Conversion MOT (Exp O) I.Type where
convert :: Exp O -> MOT Type
convert e :: Exp O
e = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
I.El (Integer -> Sort' Term
I.mkType 0) (Term -> Type) -> ExceptT ArgName IO Term -> MOT Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp O -> ExceptT ArgName IO Term
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Exp O
e
instance Conversion MOT (Exp O) I.Term where
convert :: Exp O -> ExceptT ArgName IO Term
convert e :: Exp O
e = case Exp O
e of
App _ _ (Var v :: Int
v) as :: MArgList O
as -> Int -> MArgList O -> Term -> ExceptT ArgName IO Term
frommyExps 0 MArgList O
as (Int -> Elims -> Term
I.Var Int
v [])
App _ _ (Const c :: ConstRef O
c) as :: MArgList O
as -> do
ConstDef O
cdef <- IO (ConstDef O) -> ExceptT ArgName IO (ConstDef O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (ConstDef O) -> ExceptT ArgName IO (ConstDef O))
-> IO (ConstDef O) -> ExceptT ArgName IO (ConstDef O)
forall a b. (a -> b) -> a -> b
$ ConstRef O -> IO (ConstDef O)
forall a. IORef a -> IO a
readIORef ConstRef O
c
let (iscon :: Maybe (Int, [Arg QName])
iscon, name :: QName
name) = ConstDef O -> O
forall o. ConstDef o -> o
cdorigin ConstDef O
cdef
(ndrop :: Int
ndrop, h :: QName -> Elims -> Term
h) = case Maybe (Int, [Arg QName])
iscon of
Just (n :: Int
n,fs :: [Arg QName]
fs) -> (Int
n, \ q :: QName
q -> ConHead -> ConInfo -> Elims -> Term
I.Con (QName -> Induction -> [Arg QName] -> ConHead
I.ConHead QName
q Induction
Cm.Inductive [Arg QName]
fs) ConInfo
Cm.ConOSystem)
Nothing -> (0, \ f :: QName
f vs :: Elims
vs -> QName -> Elims -> Term
I.Def QName
f Elims
vs)
Int -> MArgList O -> Term -> ExceptT ArgName IO Term
frommyExps Int
ndrop MArgList O
as (QName -> Elims -> Term
h QName
name [])
Lam hid :: Hiding
hid t :: Abs (MExp O)
t -> ArgInfo -> Abs Term -> Term
I.Lam (Hiding -> ArgInfo
icnvh Hiding
hid) (Abs Term -> Term)
-> ExceptT ArgName IO (Abs Term) -> ExceptT ArgName IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs (MExp O) -> ExceptT ArgName IO (Abs Term)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Abs (MExp O)
t
Pi _ hid :: Hiding
hid _ x :: MExp O
x y :: Abs (MExp O)
y -> do
Type
x' <- MExp O -> MOT Type
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert MExp O
x
let dom :: Dom Type
dom = (Type -> Dom Type
forall a. a -> Dom a
I.defaultDom Type
x') {domInfo :: ArgInfo
domInfo = Hiding -> ArgInfo
icnvh Hiding
hid}
Dom Type -> Abs Type -> Term
I.Pi Dom Type
dom (Abs Type -> Term)
-> ExceptT ArgName IO (Abs Type) -> ExceptT ArgName IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs (MExp O) -> ExceptT ArgName IO (Abs Type)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Abs (MExp O)
y
Sort (Set l :: Int
l) -> Term -> ExceptT ArgName IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> ExceptT ArgName IO Term)
-> Term -> ExceptT ArgName IO Term
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term
I.Sort (Integer -> Sort' Term
I.mkType (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
l))
Sort Type -> ExceptT ArgName IO Term
forall a. HasCallStack => a
__IMPOSSIBLE__
Sort UnknownSort -> Term -> ExceptT ArgName IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> ExceptT ArgName IO Term)
-> Term -> ExceptT ArgName IO Term
forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term
I.Sort (Integer -> Sort' Term
I.mkType 0)
AbsurdLambda hid :: Hiding
hid -> Term -> ExceptT ArgName IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> ExceptT ArgName IO Term)
-> Term -> ExceptT ArgName IO Term
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Abs Term -> Term
I.Lam (Hiding -> ArgInfo
icnvh Hiding
hid)
(Abs Term -> Term) -> Abs Term -> Term
forall a b. (a -> b) -> a -> b
$ ArgName -> Term -> Abs Term
forall a. ArgName -> a -> Abs a
I.Abs ArgName
abslamvarname (Int -> Elims -> Term
I.Var 0 [])
frommyExps :: Nat -> MArgList O -> I.Term -> ExceptT String IO I.Term
frommyExps :: Int -> MArgList O -> Term -> ExceptT ArgName IO Term
frommyExps ndrop :: Int
ndrop (Meta m :: Metavar (ArgList O) (RefInfo O)
m) trm :: Term
trm = do
Maybe (ArgList O)
bind <- IO (Maybe (ArgList O)) -> ExceptT ArgName IO (Maybe (ArgList O))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Maybe (ArgList O)) -> ExceptT ArgName IO (Maybe (ArgList O)))
-> IO (Maybe (ArgList O)) -> ExceptT ArgName IO (Maybe (ArgList O))
forall a b. (a -> b) -> a -> b
$ IORef (Maybe (ArgList O)) -> IO (Maybe (ArgList O))
forall a. IORef a -> IO a
readIORef (IORef (Maybe (ArgList O)) -> IO (Maybe (ArgList O)))
-> IORef (Maybe (ArgList O)) -> IO (Maybe (ArgList O))
forall a b. (a -> b) -> a -> b
$ Metavar (ArgList O) (RefInfo O) -> IORef (Maybe (ArgList O))
forall a blk. Metavar a blk -> IORef (Maybe a)
mbind Metavar (ArgList O) (RefInfo O)
m
case Maybe (ArgList O)
bind of
Nothing -> ArgName -> ExceptT ArgName IO Term
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError "meta not bound"
Just e :: ArgList O
e -> Int -> MArgList O -> Term -> ExceptT ArgName IO Term
frommyExps Int
ndrop (ArgList O -> MArgList O
forall a blk. a -> MM a blk
NotM ArgList O
e) Term
trm
frommyExps ndrop :: Int
ndrop (NotM as :: ArgList O
as) trm :: Term
trm =
case ArgList O
as of
ALNil -> Term -> ExceptT ArgName IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
trm
ALCons _ _ xs :: MArgList O
xs | Int
ndrop Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 -> Int -> MArgList O -> Term -> ExceptT ArgName IO Term
frommyExps (Int
ndrop Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) MArgList O
xs Term
trm
ALCons hid :: Hiding
hid x :: MExp O
x xs :: MArgList O
xs -> do
Term
x' <- MExp O -> ExceptT ArgName IO Term
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert MExp O
x
Int -> MArgList O -> Term -> ExceptT ArgName IO Term
frommyExps Int
ndrop MArgList O
xs (Arg Term -> Term -> Term
addend (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Cm.Arg (Hiding -> ArgInfo
icnvh Hiding
hid) Term
x') Term
trm)
ALProj eas :: MArgList O
eas idx :: MM (ConstRef O) (RefInfo O)
idx hid :: Hiding
hid xs :: MArgList O
xs -> do
MM (ConstRef O) (RefInfo O)
idx <- IO (MM (ConstRef O) (RefInfo O))
-> ExceptT ArgName IO (MM (ConstRef O) (RefInfo O))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (MM (ConstRef O) (RefInfo O))
-> ExceptT ArgName IO (MM (ConstRef O) (RefInfo O)))
-> IO (MM (ConstRef O) (RefInfo O))
-> ExceptT ArgName IO (MM (ConstRef O) (RefInfo O))
forall a b. (a -> b) -> a -> b
$ MM (ConstRef O) (RefInfo O) -> IO (MM (ConstRef O) (RefInfo O))
forall a blk. MM a blk -> MetaEnv (MM a blk)
expandbind MM (ConstRef O) (RefInfo O)
idx
ConstRef O
c <- case MM (ConstRef O) (RefInfo O)
idx of
NotM c :: ConstRef O
c -> ConstRef O -> ExceptT ArgName IO (ConstRef O)
forall (m :: * -> *) a. Monad m => a -> m a
return ConstRef O
c
Meta{} -> ArgName -> ExceptT ArgName IO (ConstRef O)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError "meta not bound"
ConstDef O
cdef <- IO (ConstDef O) -> ExceptT ArgName IO (ConstDef O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (ConstDef O) -> ExceptT ArgName IO (ConstDef O))
-> IO (ConstDef O) -> ExceptT ArgName IO (ConstDef O)
forall a b. (a -> b) -> a -> b
$ ConstRef O -> IO (ConstDef O)
forall a. IORef a -> IO a
readIORef ConstRef O
c
let name :: QName
name = O -> QName
forall a b. (a, b) -> b
snd (O -> QName) -> O -> QName
forall a b. (a -> b) -> a -> b
$ ConstDef O -> O
forall o. ConstDef o -> o
cdorigin ConstDef O
cdef
Term
trm2 <- Int -> MArgList O -> Term -> ExceptT ArgName IO Term
frommyExps 0 MArgList O
eas (QName -> Elims -> Term
I.Def QName
name [])
Int -> MArgList O -> Term -> ExceptT ArgName IO Term
frommyExps 0 MArgList O
xs (Arg Term -> Term -> Term
addend (ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Cm.Arg (Hiding -> ArgInfo
icnvh Hiding
hid) Term
trm) Term
trm2)
ALConPar xs :: MArgList O
xs | Int
ndrop Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 0 -> Int -> MArgList O -> Term -> ExceptT ArgName IO Term
frommyExps (Int
ndrop Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1) MArgList O
xs Term
trm
ALConPar _ -> ExceptT ArgName IO Term
forall a. HasCallStack => a
__IMPOSSIBLE__
where
addend :: Arg Term -> Term -> Term
addend x :: Arg Term
x (I.Var h :: Int
h xs :: Elims
xs) = Int -> Elims -> Term
I.Var Int
h (Elims
xs Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ [Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
I.Apply Arg Term
x])
addend x :: Arg Term
x (I.Con h :: ConHead
h ci :: ConInfo
ci xs :: Elims
xs) = ConHead -> ConInfo -> Elims -> Term
I.Con ConHead
h ConInfo
ci (Elims
xs Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ [Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
I.Apply Arg Term
x])
addend x :: Arg Term
x (I.Def h :: QName
h xs :: Elims
xs) = QName -> Elims -> Term
I.Def QName
h (Elims
xs Elims -> Elims -> Elims
forall a. [a] -> [a] -> [a]
++ [Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
I.Apply Arg Term
x])
addend _ _ = Term
forall a. HasCallStack => a
__IMPOSSIBLE__
abslamvarname :: String
abslamvarname :: ArgName
abslamvarname = "\0absurdlambda"
modifyAbstractExpr :: A.Expr -> A.Expr
modifyAbstractExpr :: Expr -> Expr
modifyAbstractExpr = Expr -> Expr
f
where
f :: Expr -> Expr
f (A.App i :: AppInfo
i e1 :: Expr
e1 (Cm.Arg info :: ArgInfo
info (Cm.Named n :: Maybe NamedName
n e2 :: Expr
e2))) =
AppInfo -> Expr -> Arg (Named_ Expr) -> Expr
A.App AppInfo
i (Expr -> Expr
f Expr
e1) (ArgInfo -> Named_ Expr -> Arg (Named_ Expr)
forall e. ArgInfo -> e -> Arg e
Cm.Arg ArgInfo
info (Maybe NamedName -> Expr -> Named_ Expr
forall name a. Maybe name -> a -> Named name a
Cm.Named Maybe NamedName
n (Expr -> Expr
f Expr
e2)))
f (A.Lam i :: ExprInfo
i (A.DomainFree _ x :: NamedArg Binder
x) _)
| A.Binder _ (A.BindName{unBind :: BindName -> Name
unBind = Name
n}) <- NamedArg Binder -> Binder
forall a. NamedArg a -> a
Cm.namedArg NamedArg Binder
x
, Name -> ArgName
forall a. Pretty a => a -> ArgName
prettyShow (Name -> Name
A.nameConcrete Name
n) ArgName -> ArgName -> Bool
forall a. Eq a => a -> a -> Bool
== ArgName
abslamvarname =
ExprInfo -> Hiding -> Expr
A.AbsurdLam ExprInfo
i (Hiding -> Expr) -> Hiding -> Expr
forall a b. (a -> b) -> a -> b
$ NamedArg Binder -> Hiding
forall a. LensHiding a => a -> Hiding
Cm.getHiding NamedArg Binder
x
f (A.Lam i :: ExprInfo
i b :: LamBinding
b e :: Expr
e) = ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
i LamBinding
b (Expr -> Expr
f Expr
e)
f (A.Rec i :: ExprInfo
i xs :: RecordAssigns
xs) = ExprInfo -> RecordAssigns -> Expr
A.Rec ExprInfo
i ((Either Assign ModuleName -> Either Assign ModuleName)
-> RecordAssigns -> RecordAssigns
forall a b. (a -> b) -> [a] -> [b]
map ((Assign -> Assign)
-> Either Assign ModuleName -> Either Assign ModuleName
forall a c b. (a -> c) -> Either a b -> Either c b
mapLeft (Lens' Expr Assign -> LensMap Expr Assign
forall i o. Lens' i o -> LensMap i o
over forall a. Lens' a (FieldAssignment' a)
Lens' Expr Assign
exprFieldA Expr -> Expr
f)) RecordAssigns
xs)
f (A.RecUpdate i :: ExprInfo
i e :: Expr
e xs :: Assigns
xs) = ExprInfo -> Expr -> Assigns -> Expr
A.RecUpdate ExprInfo
i (Expr -> Expr
f Expr
e) ((Assign -> Assign) -> Assigns -> Assigns
forall a b. (a -> b) -> [a] -> [b]
map (Lens' Expr Assign -> LensMap Expr Assign
forall i o. Lens' i o -> LensMap i o
over forall a. Lens' a (FieldAssignment' a)
Lens' Expr Assign
exprFieldA Expr -> Expr
f) Assigns
xs)
f (A.ScopedExpr i :: ScopeInfo
i e :: Expr
e) = ScopeInfo -> Expr -> Expr
A.ScopedExpr ScopeInfo
i (Expr -> Expr
f Expr
e)
f e :: Expr
e = Expr
e
modifyAbstractClause :: A.Clause -> A.Clause
modifyAbstractClause :: Clause -> Clause
modifyAbstractClause (A.Clause lhs :: LHS
lhs spats :: [ProblemEq]
spats (A.RHS e :: Expr
e mc :: Maybe Expr
mc) decls :: WhereDeclarations
decls catchall :: Bool
catchall) =
LHS -> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause
forall lhs.
lhs
-> [ProblemEq] -> RHS -> WhereDeclarations -> Bool -> Clause' lhs
A.Clause LHS
lhs [ProblemEq]
spats (Expr -> Maybe Expr -> RHS
A.RHS (Expr -> Expr
modifyAbstractExpr Expr
e) Maybe Expr
mc) WhereDeclarations
decls Bool
catchall
modifyAbstractClause cl :: Clause
cl = Clause
cl
constructPats :: Map AN.QName (TMode, ConstRef O) -> I.MetaId -> I.Clause -> MB.TCM ([(Hiding, MId)], [CSPat O])
constructPats :: Map QName (TMode, ConstRef O)
-> MetaId -> Clause -> TCM ([(Hiding, MId)], [CSPat O])
constructPats cmap :: Map QName (TMode, ConstRef O)
cmap mainm :: MetaId
mainm clause :: Clause
clause = do
let cnvps :: [(Hiding, MId)]
-> [NamedArg Pattern] -> TCM ([(Hiding, MId)], [CSPat O])
cnvps ns :: [(Hiding, MId)]
ns [] = ([(Hiding, MId)], [CSPat O]) -> TCM ([(Hiding, MId)], [CSPat O])
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Hiding, MId)]
ns, [])
cnvps ns :: [(Hiding, MId)]
ns (p :: NamedArg Pattern
p : ps :: [NamedArg Pattern]
ps) = do
(ns' :: [(Hiding, MId)]
ns', ps' :: [CSPat O]
ps') <- [(Hiding, MId)]
-> [NamedArg Pattern] -> TCM ([(Hiding, MId)], [CSPat O])
cnvps [(Hiding, MId)]
ns [NamedArg Pattern]
ps
(ns'' :: [(Hiding, MId)]
ns'', p' :: CSPat O
p') <- [(Hiding, MId)]
-> NamedArg Pattern -> TCM ([(Hiding, MId)], CSPat O)
cnvp [(Hiding, MId)]
ns' NamedArg Pattern
p
([(Hiding, MId)], [CSPat O]) -> TCM ([(Hiding, MId)], [CSPat O])
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Hiding, MId)]
ns'', CSPat O
p' CSPat O -> [CSPat O] -> [CSPat O]
forall a. a -> [a] -> [a]
: [CSPat O]
ps')
cnvp :: [(Hiding, MId)]
-> NamedArg Pattern -> TCM ([(Hiding, MId)], CSPat O)
cnvp ns :: [(Hiding, MId)]
ns p :: NamedArg Pattern
p =
let hid :: Hiding
hid = ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding (ArgInfo -> Hiding) -> ArgInfo -> Hiding
forall a b. (a -> b) -> a -> b
$ NamedArg Pattern -> ArgInfo
forall e. Arg e -> ArgInfo
Cm.argInfo NamedArg Pattern
p
in case NamedArg Pattern -> Pattern
forall a. NamedArg a -> a
Cm.namedArg NamedArg Pattern
p of
I.VarP _ n :: ArgName
n -> ([(Hiding, MId)], CSPat O) -> TCM ([(Hiding, MId)], CSPat O)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Hiding
hid, ArgName -> MId
Id ArgName
n) (Hiding, MId) -> [(Hiding, MId)] -> [(Hiding, MId)]
forall a. a -> [a] -> [a]
: [(Hiding, MId)]
ns, Hiding -> CSPatI O -> CSPat O
forall a. Hiding -> a -> HI a
HI Hiding
hid (Int -> CSPatI O
forall o. Int -> CSPatI o
CSPatVar (Int -> CSPatI O) -> Int -> CSPatI O
forall a b. (a -> b) -> a -> b
$ [(Hiding, MId)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Hiding, MId)]
ns))
I.IApplyP _ _ _ n :: ArgName
n -> ([(Hiding, MId)], CSPat O) -> TCM ([(Hiding, MId)], CSPat O)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Hiding
hid, ArgName -> MId
Id ArgName
n) (Hiding, MId) -> [(Hiding, MId)] -> [(Hiding, MId)]
forall a. a -> [a] -> [a]
: [(Hiding, MId)]
ns, Hiding -> CSPatI O -> CSPat O
forall a. Hiding -> a -> HI a
HI Hiding
hid (Int -> CSPatI O
forall o. Int -> CSPatI o
CSPatVar (Int -> CSPatI O) -> Int -> CSPatI O
forall a b. (a -> b) -> a -> b
$ [(Hiding, MId)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Hiding, MId)]
ns))
I.ConP con :: ConHead
con _ ps :: [NamedArg Pattern]
ps -> do
let c :: QName
c = ConHead -> QName
I.conName ConHead
con
(c2 :: ConstRef O
c2, _) <- StateT S TCM (ConstRef O) -> S -> TCM (ConstRef O, S)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Bool -> QName -> TMode -> StateT S TCM (ConstRef O)
getConst Bool
True QName
c TMode
TMAll) (S :: MapS QName (TMode, ConstRef O)
-> MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> MapS Int (Maybe (Bool, MExp O, MExp O))
-> Maybe MetaId
-> MetaId
-> S
S {sConsts :: MapS QName (TMode, ConstRef O)
sConsts = (Map QName (TMode, ConstRef O)
cmap, []), sMetas :: MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
sMetas = MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
forall a b. MapS a b
initMapS, sEqs :: MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs = MapS Int (Maybe (Bool, MExp O, MExp O))
forall a b. MapS a b
initMapS, sCurMeta :: Maybe MetaId
sCurMeta = Maybe MetaId
forall a. Maybe a
Nothing, sMainMeta :: MetaId
sMainMeta = MetaId
mainm})
(ns' :: [(Hiding, MId)]
ns', ps' :: [CSPat O]
ps') <- [(Hiding, MId)]
-> [NamedArg Pattern] -> TCM ([(Hiding, MId)], [CSPat O])
cnvps [(Hiding, MId)]
ns [NamedArg Pattern]
ps
ConstDef O
cc <- IO (ConstDef O) -> TCM (ConstDef O)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ConstDef O) -> TCM (ConstDef O))
-> IO (ConstDef O) -> TCM (ConstDef O)
forall a b. (a -> b) -> a -> b
$ ConstRef O -> IO (ConstDef O)
forall a. IORef a -> IO a
readIORef ConstRef O
c2
let Just (npar :: Int
npar,_) = O -> Maybe (Int, [Arg QName])
forall a b. (a, b) -> a
fst (O -> Maybe (Int, [Arg QName])) -> O -> Maybe (Int, [Arg QName])
forall a b. (a -> b) -> a -> b
$ ConstDef O -> O
forall o. ConstDef o -> o
cdorigin ConstDef O
cc
([(Hiding, MId)], CSPat O) -> TCM ([(Hiding, MId)], CSPat O)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Hiding, MId)]
ns', Hiding -> CSPatI O -> CSPat O
forall a. Hiding -> a -> HI a
HI Hiding
hid (ConstRef O -> [CSPat O] -> CSPatI O
forall o. ConstRef o -> [CSPat o] -> CSPatI o
CSPatConApp ConstRef O
c2 (Int -> CSPat O -> [CSPat O]
forall a. Int -> a -> [a]
replicate Int
npar (Hiding -> CSPatI O -> CSPat O
forall a. Hiding -> a -> HI a
HI Hiding
Hidden CSPatI O
forall o. CSPatI o
CSOmittedArg) [CSPat O] -> [CSPat O] -> [CSPat O]
forall a. [a] -> [a] -> [a]
++ [CSPat O]
ps')))
I.DotP _ t :: Term
t -> do
(t2 :: MExp O
t2, _) <- StateT S TCM (MExp O) -> S -> TCM (MExp O, S)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Term -> StateT S TCM (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Term
t) (S :: MapS QName (TMode, ConstRef O)
-> MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
-> MapS Int (Maybe (Bool, MExp O, MExp O))
-> Maybe MetaId
-> MetaId
-> S
S {sConsts :: MapS QName (TMode, ConstRef O)
sConsts = (Map QName (TMode, ConstRef O)
cmap, []), sMetas :: MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
sMetas = MapS
MetaId
(Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
forall a b. MapS a b
initMapS, sEqs :: MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs = MapS Int (Maybe (Bool, MExp O, MExp O))
forall a b. MapS a b
initMapS, sCurMeta :: Maybe MetaId
sCurMeta = Maybe MetaId
forall a. Maybe a
Nothing, sMainMeta :: MetaId
sMainMeta = MetaId
mainm})
([(Hiding, MId)], CSPat O) -> TCM ([(Hiding, MId)], CSPat O)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Hiding, MId)]
ns, Hiding -> CSPatI O -> CSPat O
forall a. Hiding -> a -> HI a
HI Hiding
hid (MExp O -> CSPatI O
forall o. MExp o -> CSPatI o
CSPatExp MExp O
t2))
I.ProjP{} -> TCM ([(Hiding, MId)], CSPat O)
forall a. TCM a
copatternsNotImplemented
I.LitP{} -> TCM ([(Hiding, MId)], CSPat O)
forall a. TCM a
literalsNotImplemented
I.DefP{} -> TCM ([(Hiding, MId)], CSPat O)
forall a. TCM a
hitsNotImplemented
(names :: [(Hiding, MId)]
names, pats :: [CSPat O]
pats) <- [(Hiding, MId)]
-> [NamedArg Pattern] -> TCM ([(Hiding, MId)], [CSPat O])
cnvps [] ([NamedArg DeBruijnPattern] -> [NamedArg Pattern]
forall a b i. LabelPatVars a b i => b -> a
IP.unnumberPatVars ([NamedArg DeBruijnPattern] -> [NamedArg Pattern])
-> [NamedArg DeBruijnPattern] -> [NamedArg Pattern]
forall a b. (a -> b) -> a -> b
$ Clause -> [NamedArg DeBruijnPattern]
I.namedClausePats Clause
clause)
([(Hiding, MId)], [CSPat O]) -> TCM ([(Hiding, MId)], [CSPat O])
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Hiding, MId)] -> [(Hiding, MId)]
forall a. [a] -> [a]
reverse [(Hiding, MId)]
names, [CSPat O]
pats)
frommyClause :: (CSCtx O, [CSPat O], Maybe (MExp O)) -> ExceptT String IO I.Clause
frommyClause :: (CSCtx O, [CSPat O], Maybe (MExp O)) -> ExceptT ArgName IO Clause
frommyClause (ids :: CSCtx O
ids, pats :: [CSPat O]
pats, mrhs :: Maybe (MExp O)
mrhs) = do
let ctel :: [HI (MId, a)] -> m (Tele (Dom' Term a))
ctel [] = Tele (Dom' Term a) -> m (Tele (Dom' Term a))
forall (m :: * -> *) a. Monad m => a -> m a
return Tele (Dom' Term a)
forall a. Tele a
I.EmptyTel
ctel (HI hid :: Hiding
hid (mid :: MId
mid, t :: a
t) : ctx :: [HI (MId, a)]
ctx) = do
let Id id :: ArgName
id = MId
mid
Tele (Dom' Term a)
tel <- [HI (MId, a)] -> m (Tele (Dom' Term a))
ctel [HI (MId, a)]
ctx
a
t' <- a -> m a
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert a
t
let dom :: Dom' Term a
dom = (a -> Dom' Term a
forall a. a -> Dom a
I.defaultDom a
t') {domInfo :: ArgInfo
domInfo = Hiding -> ArgInfo
icnvh Hiding
hid}
Tele (Dom' Term a) -> m (Tele (Dom' Term a))
forall (m :: * -> *) a. Monad m => a -> m a
return (Tele (Dom' Term a) -> m (Tele (Dom' Term a)))
-> Tele (Dom' Term a) -> m (Tele (Dom' Term a))
forall a b. (a -> b) -> a -> b
$ Dom' Term a -> Abs (Tele (Dom' Term a)) -> Tele (Dom' Term a)
forall a. a -> Abs (Tele a) -> Tele a
I.ExtendTel Dom' Term a
dom (ArgName -> Tele (Dom' Term a) -> Abs (Tele (Dom' Term a))
forall a. ArgName -> a -> Abs a
I.Abs ArgName
id Tele (Dom' Term a)
tel)
Telescope
tel <- CSCtx O -> ExceptT ArgName IO Telescope
forall (m :: * -> *) a a.
(Monad m, Conversion m a a) =>
[HI (MId, a)] -> m (Tele (Dom' Term a))
ctel (CSCtx O -> ExceptT ArgName IO Telescope)
-> CSCtx O -> ExceptT ArgName IO Telescope
forall a b. (a -> b) -> a -> b
$ CSCtx O -> CSCtx O
forall a. [a] -> [a]
reverse CSCtx O
ids
let getperms :: a
-> [HI (CSPatI (Maybe (a, b), b))]
-> [(Int, b)]
-> b
-> t IO ([(Int, b)], b)
getperms 0 [] perm :: [(Int, b)]
perm nv :: b
nv = ([(Int, b)], b) -> t IO ([(Int, b)], b)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Int, b)]
perm, b
nv)
getperms n :: a
n [] _ _ = t IO ([(Int, b)], b)
forall a. HasCallStack => a
__IMPOSSIBLE__
getperms 0 (p :: HI (CSPatI (Maybe (a, b), b))
p : ps :: [HI (CSPatI (Maybe (a, b), b))]
ps) perm :: [(Int, b)]
perm nv :: b
nv = do
(perm :: [(Int, b)]
perm, nv :: b
nv) <- HI (CSPatI (Maybe (a, b), b))
-> [(Int, b)] -> b -> t IO ([(Int, b)], b)
getperm HI (CSPatI (Maybe (a, b), b))
p [(Int, b)]
perm b
nv
a
-> [HI (CSPatI (Maybe (a, b), b))]
-> [(Int, b)]
-> b
-> t IO ([(Int, b)], b)
getperms 0 [HI (CSPatI (Maybe (a, b), b))]
ps [(Int, b)]
perm b
nv
getperms n :: a
n (HI _ CSPatExp{} : ps :: [HI (CSPatI (Maybe (a, b), b))]
ps) perm :: [(Int, b)]
perm nv :: b
nv = a
-> [HI (CSPatI (Maybe (a, b), b))]
-> [(Int, b)]
-> b
-> t IO ([(Int, b)], b)
getperms (a
n a -> a -> a
forall a. Num a => a -> a -> a
- 1) [HI (CSPatI (Maybe (a, b), b))]
ps [(Int, b)]
perm b
nv
getperms n :: a
n (HI _ CSOmittedArg{} : ps :: [HI (CSPatI (Maybe (a, b), b))]
ps) perm :: [(Int, b)]
perm nv :: b
nv = a
-> [HI (CSPatI (Maybe (a, b), b))]
-> [(Int, b)]
-> b
-> t IO ([(Int, b)], b)
getperms (a
n a -> a -> a
forall a. Num a => a -> a -> a
- 1) [HI (CSPatI (Maybe (a, b), b))]
ps [(Int, b)]
perm b
nv
getperms n :: a
n (_ : _) _ _ = t IO ([(Int, b)], b)
forall a. HasCallStack => a
__IMPOSSIBLE__
getperm :: HI (CSPatI (Maybe (a, b), b))
-> [(Int, b)] -> b -> t IO ([(Int, b)], b)
getperm (HI _ p :: CSPatI (Maybe (a, b), b)
p) perm :: [(Int, b)]
perm nv :: b
nv =
case CSPatI (Maybe (a, b), b)
p of
CSPatVar v :: Int
v -> ([(Int, b)], b) -> t IO ([(Int, b)], b)
forall (m :: * -> *) a. Monad m => a -> m a
return ((CSCtx O -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length CSCtx O
ids Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
v, b
nv) (Int, b) -> [(Int, b)] -> [(Int, b)]
forall a. a -> [a] -> [a]
: [(Int, b)]
perm, b
nv b -> b -> b
forall a. Num a => a -> a -> a
+ 1)
CSPatConApp c :: ConstRef (Maybe (a, b), b)
c ps :: [HI (CSPatI (Maybe (a, b), b))]
ps -> do
ConstDef (Maybe (a, b), b)
cdef <- IO (ConstDef (Maybe (a, b), b))
-> t IO (ConstDef (Maybe (a, b), b))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (ConstDef (Maybe (a, b), b))
-> t IO (ConstDef (Maybe (a, b), b)))
-> IO (ConstDef (Maybe (a, b), b))
-> t IO (ConstDef (Maybe (a, b), b))
forall a b. (a -> b) -> a -> b
$ ConstRef (Maybe (a, b), b) -> IO (ConstDef (Maybe (a, b), b))
forall a. IORef a -> IO a
readIORef ConstRef (Maybe (a, b), b)
c
let (Just (ndrop :: a
ndrop,_), _) = ConstDef (Maybe (a, b), b) -> (Maybe (a, b), b)
forall o. ConstDef o -> o
cdorigin ConstDef (Maybe (a, b), b)
cdef
a
-> [HI (CSPatI (Maybe (a, b), b))]
-> [(Int, b)]
-> b
-> t IO ([(Int, b)], b)
getperms a
ndrop [HI (CSPatI (Maybe (a, b), b))]
ps [(Int, b)]
perm b
nv
CSPatExp e :: MExp (Maybe (a, b), b)
e -> ([(Int, b)], b) -> t IO ([(Int, b)], b)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Int, b)]
perm, b
nv b -> b -> b
forall a. Num a => a -> a -> a
+ 1)
_ -> t IO ([(Int, b)], b)
forall a. HasCallStack => a
__IMPOSSIBLE__
(rperm :: [(Int, Int)]
rperm, nv :: Int
nv) <- Int
-> [CSPat O]
-> [(Int, Int)]
-> Int
-> ExceptT ArgName IO ([(Int, Int)], Int)
forall a (t :: (* -> *) -> * -> *) b b b.
(Eq a, Monad (t IO), Num a, Num b, MonadTrans t) =>
a
-> [HI (CSPatI (Maybe (a, b), b))]
-> [(Int, b)]
-> b
-> t IO ([(Int, b)], b)
getperms 0 [CSPat O]
pats [] 0
let
perm :: [Int]
perm = (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (\i :: Int
i -> let Just x :: Int
x = Int -> [(Int, Int)] -> Maybe Int
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
i [(Int, Int)]
rperm in Int
x) [0..CSCtx O -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length CSCtx O
ids Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1]
cnvps :: a -> [HI (CSPatI (Maybe (a, b), QName))] -> t IO [NamedArg Pattern]
cnvps 0 [] = [NamedArg Pattern] -> t IO [NamedArg Pattern]
forall (m :: * -> *) a. Monad m => a -> m a
return []
cnvps n :: a
n [] = t IO [NamedArg Pattern]
forall a. HasCallStack => a
__IMPOSSIBLE__
cnvps 0 (p :: HI (CSPatI (Maybe (a, b), QName))
p : ps :: [HI (CSPatI (Maybe (a, b), QName))]
ps) = do
NamedArg Pattern
p' <- HI (CSPatI (Maybe (a, b), QName)) -> t IO (NamedArg Pattern)
cnvp HI (CSPatI (Maybe (a, b), QName))
p
[NamedArg Pattern]
ps' <- a -> [HI (CSPatI (Maybe (a, b), QName))] -> t IO [NamedArg Pattern]
cnvps 0 [HI (CSPatI (Maybe (a, b), QName))]
ps
[NamedArg Pattern] -> t IO [NamedArg Pattern]
forall (m :: * -> *) a. Monad m => a -> m a
return (NamedArg Pattern
p' NamedArg Pattern -> [NamedArg Pattern] -> [NamedArg Pattern]
forall a. a -> [a] -> [a]
: [NamedArg Pattern]
ps')
cnvps n :: a
n (HI _ CSPatExp{} : ps :: [HI (CSPatI (Maybe (a, b), QName))]
ps) = a -> [HI (CSPatI (Maybe (a, b), QName))] -> t IO [NamedArg Pattern]
cnvps (a
n a -> a -> a
forall a. Num a => a -> a -> a
- 1) [HI (CSPatI (Maybe (a, b), QName))]
ps
cnvps n :: a
n (HI _ CSOmittedArg{} : ps :: [HI (CSPatI (Maybe (a, b), QName))]
ps) = a -> [HI (CSPatI (Maybe (a, b), QName))] -> t IO [NamedArg Pattern]
cnvps (a
n a -> a -> a
forall a. Num a => a -> a -> a
- 1) [HI (CSPatI (Maybe (a, b), QName))]
ps
cnvps n :: a
n (_ : _) = t IO [NamedArg Pattern]
forall a. HasCallStack => a
__IMPOSSIBLE__
cnvp :: HI (CSPatI (Maybe (a, b), QName)) -> t IO (NamedArg Pattern)
cnvp (HI hid :: Hiding
hid p :: CSPatI (Maybe (a, b), QName)
p) = do
Pattern
p' <- case CSPatI (Maybe (a, b), QName)
p of
CSPatVar v :: Int
v -> Pattern -> t IO Pattern
forall (m :: * -> *) a. Monad m => a -> m a
return (ArgName -> Pattern
forall a. a -> Pattern' a
I.varP (ArgName -> Pattern) -> ArgName -> Pattern
forall a b. (a -> b) -> a -> b
$ let HI _ (Id n :: ArgName
n, _) = CSCtx O
ids CSCtx O -> Int -> HI (MId, MExp O)
forall a. [a] -> Int -> a
!! Int
v in ArgName
n)
CSPatConApp c :: ConstRef (Maybe (a, b), QName)
c ps :: [HI (CSPatI (Maybe (a, b), QName))]
ps -> do
ConstDef (Maybe (a, b), QName)
cdef <- IO (ConstDef (Maybe (a, b), QName))
-> t IO (ConstDef (Maybe (a, b), QName))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (ConstDef (Maybe (a, b), QName))
-> t IO (ConstDef (Maybe (a, b), QName)))
-> IO (ConstDef (Maybe (a, b), QName))
-> t IO (ConstDef (Maybe (a, b), QName))
forall a b. (a -> b) -> a -> b
$ ConstRef (Maybe (a, b), QName)
-> IO (ConstDef (Maybe (a, b), QName))
forall a. IORef a -> IO a
readIORef ConstRef (Maybe (a, b), QName)
c
let (Just (ndrop :: a
ndrop,_), name :: QName
name) = ConstDef (Maybe (a, b), QName) -> (Maybe (a, b), QName)
forall o. ConstDef o -> o
cdorigin ConstDef (Maybe (a, b), QName)
cdef
[NamedArg Pattern]
ps' <- a -> [HI (CSPatI (Maybe (a, b), QName))] -> t IO [NamedArg Pattern]
cnvps a
ndrop [HI (CSPatI (Maybe (a, b), QName))]
ps
let con :: ConHead
con = QName -> Induction -> [Arg QName] -> ConHead
I.ConHead QName
name Induction
Cm.Inductive []
Pattern -> t IO Pattern
forall (m :: * -> *) a. Monad m => a -> m a
return (ConHead -> ConPatternInfo -> [NamedArg Pattern] -> Pattern
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
I.ConP ConHead
con ConPatternInfo
I.noConPatternInfo [NamedArg Pattern]
ps')
CSPatExp e :: MExp (Maybe (a, b), QName)
e -> do
Term
e' <- MExp (Maybe (a, b), QName) -> t IO Term
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert MExp (Maybe (a, b), QName)
e
Pattern -> t IO Pattern
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Pattern
forall a. Term -> Pattern' a
I.dotP Term
e')
CSAbsurd -> t IO Pattern
forall a. HasCallStack => a
__IMPOSSIBLE__
_ -> t IO Pattern
forall a. HasCallStack => a
__IMPOSSIBLE__
NamedArg Pattern -> t IO (NamedArg Pattern)
forall (m :: * -> *) a. Monad m => a -> m a
return (NamedArg Pattern -> t IO (NamedArg Pattern))
-> NamedArg Pattern -> t IO (NamedArg Pattern)
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Named NamedName Pattern -> NamedArg Pattern
forall e. ArgInfo -> e -> Arg e
Cm.Arg (Hiding -> ArgInfo
icnvh Hiding
hid) (Named NamedName Pattern -> NamedArg Pattern)
-> Named NamedName Pattern -> NamedArg Pattern
forall a b. (a -> b) -> a -> b
$ Pattern -> Named NamedName Pattern
forall a name. a -> Named name a
Cm.unnamed Pattern
p'
[NamedArg Pattern]
ps <- Int -> [CSPat O] -> ExceptT ArgName IO [NamedArg Pattern]
forall a (t :: (* -> *) -> * -> *) b.
(Eq a, Num a, Monad (t IO), MonadTrans t,
Conversion (t IO) (MExp (Maybe (a, b), QName)) Term) =>
a -> [HI (CSPatI (Maybe (a, b), QName))] -> t IO [NamedArg Pattern]
cnvps 0 [CSPat O]
pats
Maybe Term
body <- case Maybe (MExp O)
mrhs of
Nothing -> Maybe Term -> ExceptT ArgName IO (Maybe Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Term -> ExceptT ArgName IO (Maybe Term))
-> Maybe Term -> ExceptT ArgName IO (Maybe Term)
forall a b. (a -> b) -> a -> b
$ Maybe Term
forall a. Maybe a
Nothing
Just e :: MExp O
e -> Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term)
-> ExceptT ArgName IO Term -> ExceptT ArgName IO (Maybe Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MExp O -> ExceptT ArgName IO Term
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert MExp O
e
let cperm :: Permutation
cperm = Int -> [Int] -> Permutation
Perm Int
nv [Int]
perm
Clause -> ExceptT ArgName IO Clause
forall (m :: * -> *) a. Monad m => a -> m a
return (Clause -> ExceptT ArgName IO Clause)
-> Clause -> ExceptT ArgName IO Clause
forall a b. (a -> b) -> a -> b
$ Clause :: Range
-> Range
-> Telescope
-> [NamedArg DeBruijnPattern]
-> Maybe Term
-> Maybe (Arg Type)
-> Bool
-> Maybe Bool
-> Maybe Bool
-> ExpandedEllipsis
-> Clause
I.Clause
{ clauseLHSRange :: Range
I.clauseLHSRange = Range
forall a. Range' a
SP.noRange
, clauseFullRange :: Range
I.clauseFullRange = Range
forall a. Range' a
SP.noRange
, clauseTel :: Telescope
I.clauseTel = Telescope
tel
, namedClausePats :: [NamedArg DeBruijnPattern]
I.namedClausePats = Int
-> Permutation -> [NamedArg Pattern] -> [NamedArg DeBruijnPattern]
forall a b. LabelPatVars a b Int => Int -> Permutation -> a -> b
IP.numberPatVars Int
forall a. HasCallStack => a
__IMPOSSIBLE__ Permutation
cperm ([NamedArg Pattern] -> [NamedArg DeBruijnPattern])
-> [NamedArg Pattern] -> [NamedArg DeBruijnPattern]
forall a b. (a -> b) -> a -> b
$ Substitution' Term -> [NamedArg Pattern] -> [NamedArg Pattern]
forall t a. Subst t a => Substitution' t -> a -> a
applySubst (Permutation -> Substitution' Term
forall a. DeBruijn a => Permutation -> Substitution' a
renamingR (Permutation -> Substitution' Term)
-> Permutation -> Substitution' Term
forall a b. (a -> b) -> a -> b
$ Permutation -> Permutation
compactP Permutation
cperm) [NamedArg Pattern]
ps
, clauseBody :: Maybe Term
I.clauseBody = Maybe Term
body
, clauseType :: Maybe (Arg Type)
I.clauseType = Maybe (Arg Type)
forall a. Maybe a
Nothing
, clauseCatchall :: Bool
I.clauseCatchall = Bool
False
, clauseRecursive :: Maybe Bool
I.clauseRecursive = Maybe Bool
forall a. Maybe a
Nothing
, clauseUnreachable :: Maybe Bool
I.clauseUnreachable = Maybe Bool
forall a. Maybe a
Nothing
, clauseEllipsis :: ExpandedEllipsis
I.clauseEllipsis = ExpandedEllipsis
Cm.NoEllipsis
}
contains_constructor :: [CSPat O] -> Bool
contains_constructor :: [CSPat O] -> Bool
contains_constructor = (CSPat O -> Bool) -> [CSPat O] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any CSPat O -> Bool
forall o. HI (CSPatI o) -> Bool
f
where
f :: HI (CSPatI o) -> Bool
f (HI _ p :: CSPatI o
p) = case CSPatI o
p of
CSPatConApp{} -> Bool
True
_ -> Bool
False
freeIn :: Nat -> MExp o -> Bool
freeIn :: Int -> MExp o -> Bool
freeIn = Int -> MExp o -> Bool
forall o. Int -> MExp o -> Bool
f
where
mr :: MM a blk -> a
mr x :: MM a blk
x = let NotM x' :: a
x' = MM a blk
x in a
x'
f :: Int -> MExp o -> Bool
f v :: Int
v e :: MExp o
e = case MExp o -> Exp o
forall a blk. MM a blk -> a
mr MExp o
e of
App _ _ elr :: Elr o
elr args :: MArgList o
args -> case Elr o
elr of
Var v' :: Int
v' | Int
v' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
v -> Bool
False
_ -> Int -> MArgList o -> Bool
fs Int
v MArgList o
args
Lam _ (Abs _ b :: MExp o
b) -> Int -> MExp o -> Bool
f (Int
v Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) MExp o
b
Pi _ _ _ it :: MExp o
it (Abs _ ot :: MExp o
ot) -> Int -> MExp o -> Bool
f Int
v MExp o
it Bool -> Bool -> Bool
&& Int -> MExp o -> Bool
f (Int
v Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) MExp o
ot
Sort{} -> Bool
True
AbsurdLambda{} -> Bool
True
fs :: Int -> MArgList o -> Bool
fs v :: Int
v es :: MArgList o
es = case MArgList o -> ArgList o
forall a blk. MM a blk -> a
mr MArgList o
es of
ALNil -> Bool
True
ALCons _ a :: MExp o
a as :: MArgList o
as -> Int -> MExp o -> Bool
f Int
v MExp o
a Bool -> Bool -> Bool
&& Int -> MArgList o -> Bool
fs Int
v MArgList o
as
ALProj{} -> Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
ALConPar as :: MArgList o
as -> Int -> MArgList o -> Bool
fs Int
v MArgList o
as
negtype :: ConstRef o -> MExp o -> MExp o
negtype :: ConstRef o -> MExp o -> MExp o
negtype ee :: ConstRef o
ee = Int -> MExp o -> MExp o
forall t. Num t => t -> MExp o -> MExp o
f (0 :: Int)
where
mr :: MM a blk -> a
mr x :: MM a blk
x = let NotM x' :: a
x' = MM a blk
x in a
x'
f :: t -> MExp o -> MExp o
f n :: t
n e :: MExp o
e = case MExp o -> Exp o
forall a blk. MM a blk -> a
mr MExp o
e of
Pi uid :: Maybe (UId o)
uid hid :: Hiding
hid possdep :: Bool
possdep it :: MExp o
it (Abs id :: MId
id ot :: MExp o
ot) -> Exp o -> MExp o
forall a blk. a -> MM a blk
NotM (Exp o -> MExp o) -> Exp o -> MExp o
forall a b. (a -> b) -> a -> b
$ Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
forall o.
Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
Pi Maybe (UId o)
uid Hiding
hid Bool
possdep MExp o
it (MId -> MExp o -> Abs (MExp o)
forall a. MId -> a -> Abs a
Abs MId
id (t -> MExp o -> MExp o
f (t
n t -> t -> t
forall a. Num a => a -> a -> a
+ 1) MExp o
ot))
_ -> Exp o -> MExp o
forall a blk. a -> MM a blk
NotM (Exp o -> MExp o) -> Exp o -> MExp o
forall a b. (a -> b) -> a -> b
$ Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
forall o.
Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
Pi Maybe (UId o)
forall a. Maybe a
Nothing Hiding
NotHidden Bool
False (Exp o -> MExp o
forall a blk. a -> MM a blk
NotM (Exp o -> MExp o) -> Exp o -> MExp o
forall a b. (a -> b) -> a -> b
$ Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
forall o.
Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
Pi Maybe (UId o)
forall a. Maybe a
Nothing Hiding
NotHidden Bool
False MExp o
e (MId -> MExp o -> Abs (MExp o)
forall a. MId -> a -> Abs a
Abs MId
NoId (Exp o -> MExp o
forall a blk. a -> MM a blk
NotM (Exp o -> MExp o) -> Exp o -> MExp o
forall a b. (a -> b) -> a -> b
$ Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
forall o.
Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
Pi Maybe (UId o)
forall a. Maybe a
Nothing Hiding
NotHidden Bool
True (Exp o -> MExp o
forall a blk. a -> MM a blk
NotM (Exp o -> MExp o) -> Exp o -> MExp o
forall a b. (a -> b) -> a -> b
$ Sort -> Exp o
forall o. Sort -> Exp o
Sort (Int -> Sort
Set 0)) (MId -> MExp o -> Abs (MExp o)
forall a. MId -> a -> Abs a
Abs MId
NoId (Exp o -> MExp o
forall a blk. a -> MM a blk
NotM (Exp o -> MExp o) -> Exp o -> MExp o
forall a b. (a -> b) -> a -> b
$ Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (UId o)
forall a. Maybe a
Nothing (OKVal -> OKHandle (RefInfo o)
forall a blk. a -> MM a blk
NotM OKVal
OKVal) (Int -> Elr o
forall o. Int -> Elr o
Var 0) (ArgList o -> MArgList o
forall a blk. a -> MM a blk
NotM ArgList o
forall o. ArgList o
ALNil)))))) (MId -> MExp o -> Abs (MExp o)
forall a. MId -> a -> Abs a
Abs MId
NoId (Exp o -> MExp o
forall a blk. a -> MM a blk
NotM (Exp o -> MExp o) -> Exp o -> MExp o
forall a b. (a -> b) -> a -> b
$ Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (UId o)
forall a. Maybe a
Nothing (OKVal -> OKHandle (RefInfo o)
forall a blk. a -> MM a blk
NotM OKVal
OKVal) (ConstRef o -> Elr o
forall o. ConstRef o -> Elr o
Const ConstRef o
ee) (ArgList o -> MArgList o
forall a blk. a -> MM a blk
NotM ArgList o
forall o. ArgList o
ALNil)))
findClauseDeep :: Cm.InteractionId -> MB.TCM (Maybe (AN.QName, I.Clause, Bool))
findClauseDeep :: InteractionId -> TCM (Maybe (QName, Clause, Bool))
findClauseDeep ii :: InteractionId
ii = TCM (Maybe (QName, Clause, Bool))
-> TCM (Maybe (QName, Clause, Bool))
forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode (TCM (Maybe (QName, Clause, Bool))
-> TCM (Maybe (QName, Clause, Bool)))
-> TCM (Maybe (QName, Clause, Bool))
-> TCM (Maybe (QName, Clause, Bool))
forall a b. (a -> b) -> a -> b
$ do
MB.InteractionPoint { ipClause :: InteractionPoint -> IPClause
MB.ipClause = IPClause
ipCl} <- InteractionId -> TCMT IO InteractionPoint
forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
ii
case IPClause
ipCl of
MB.IPNoClause -> Maybe (QName, Clause, Bool) -> TCM (Maybe (QName, Clause, Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (QName, Clause, Bool)
forall a. Maybe a
Nothing
MB.IPClause f :: QName
f clauseNo :: Int
clauseNo _ _ _ _ _ -> do
(_, (_, c :: Clause
c, _)) <- QName -> Int -> TCM (CaseContext, ClauseZipper)
getClauseZipperForIP QName
f Int
clauseNo
Maybe (QName, Clause, Bool) -> TCM (Maybe (QName, Clause, Bool))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (QName, Clause, Bool) -> TCM (Maybe (QName, Clause, Bool)))
-> Maybe (QName, Clause, Bool) -> TCM (Maybe (QName, Clause, Bool))
forall a b. (a -> b) -> a -> b
$ (QName, Clause, Bool) -> Maybe (QName, Clause, Bool)
forall a. a -> Maybe a
Just (QName
f, Clause
c, Bool -> (Term -> Bool) -> Maybe Term -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
forall a. HasCallStack => a
__IMPOSSIBLE__ Term -> Bool
toplevel (Maybe Term -> Bool) -> Maybe Term -> Bool
forall a b. (a -> b) -> a -> b
$ Clause -> Maybe Term
I.clauseBody Clause
c)
where
toplevel :: Term -> Bool
toplevel e :: Term
e =
case Term
e of
I.MetaV{} -> Bool
True
_ -> Bool
False
matchType :: Int -> Int -> I.Type -> I.Type -> Maybe (Nat, Nat)
matchType :: Int -> Int -> Type -> Type -> Maybe (Int, Int)
matchType cdfv :: Int
cdfv tctx :: Int
tctx ctyp :: Type
ctyp ttyp :: Type
ttyp = Int -> Type -> Maybe (Int, Int)
forall a a t.
(Num a, Num a, Num t, Eq t) =>
t -> Type -> Maybe (a, a)
trmodps Int
cdfv Type
ctyp
where
trmodps :: t -> Type -> Maybe (a, a)
trmodps 0 ctyp :: Type
ctyp = a -> Int -> Type -> Maybe (a, a)
forall a a. (Num a, Num a) => a -> Int -> Type -> Maybe (a, a)
tr 0 0 Type
ctyp
trmodps n :: t
n ctyp :: Type
ctyp = case Type -> Term
forall t a. Type'' t a -> a
I.unEl Type
ctyp of
I.Pi _ ot :: Abs Type
ot -> t -> Type -> Maybe (a, a)
trmodps (t
n t -> t -> t
forall a. Num a => a -> a -> a
- 1) (Abs Type -> Type
forall t a. Subst t a => Abs a -> a
I.absBody Abs Type
ot)
_ -> Maybe (a, a)
forall a. HasCallStack => a
__IMPOSSIBLE__
tr :: a -> Int -> Type -> Maybe (a, a)
tr narg :: a
narg na :: Int
na ctyp :: Type
ctyp =
case Int -> a -> (a -> Maybe a) -> Type -> Type -> Maybe a
forall t a.
Num t =>
Int -> t -> (t -> Maybe a) -> Type -> Type -> Maybe a
ft 0 0 a -> Maybe a
forall a. a -> Maybe a
Just Type
ctyp Type
ttyp of
Just n :: a
n -> (a, a) -> Maybe (a, a)
forall a. a -> Maybe a
Just (a
n, a
narg)
Nothing -> case Type -> Term
forall t a. Type'' t a -> a
I.unEl Type
ctyp of
I.Pi _ (I.Abs _ ot :: Type
ot) -> a -> Int -> Type -> Maybe (a, a)
tr (a
narg a -> a -> a
forall a. Num a => a -> a -> a
+ 1) (Int
na Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) Type
ot
I.Pi _ (I.NoAbs _ ot :: Type
ot) -> a -> Int -> Type -> Maybe (a, a)
tr (a
narg a -> a -> a
forall a. Num a => a -> a -> a
+ 1) Int
na Type
ot
_ -> Maybe (a, a)
forall a. Maybe a
Nothing
where
ft :: Int -> t -> (t -> Maybe a) -> Type -> Type -> Maybe a
ft nl :: Int
nl n :: t
n c :: t -> Maybe a
c (I.El _ e1 :: Term
e1) (I.El _ e2 :: Term
e2) = Int -> t -> (t -> Maybe a) -> Term -> Term -> Maybe a
f Int
nl t
n t -> Maybe a
c Term
e1 Term
e2
f :: Int -> t -> (t -> Maybe a) -> Term -> Term -> Maybe a
f nl :: Int
nl n :: t
n c :: t -> Maybe a
c e1 :: Term
e1 e2 :: Term
e2 = case Term
e1 of
I.Var v1 :: Int
v1 as1 :: Elims
as1 | Int
v1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
nl -> case Term
e2 of
I.Var v2 :: Int
v2 as2 :: Elims
as2 | Int
v1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
v2 -> Int -> t -> (t -> Maybe a) -> Elims -> Elims -> Maybe a
fes Int
nl (t
n t -> t -> t
forall a. Num a => a -> a -> a
+ 1) t -> Maybe a
c Elims
as1 Elims
as2
_ -> Maybe a
forall a. Maybe a
Nothing
I.Var v1 :: Int
v1 _ | Int
v1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
nl Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
na -> t -> Maybe a
c t
n
I.Var v1 :: Int
v1 as1 :: Elims
as1 -> case Term
e2 of
I.Var v2 :: Int
v2 as2 :: Elims
as2 | Int
cdfv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
na Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nl Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
v1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
tctx Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
nl Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
v2 -> Int -> t -> (t -> Maybe a) -> Elims -> Elims -> Maybe a
fes Int
nl (t
n t -> t -> t
forall a. Num a => a -> a -> a
+ 1) t -> Maybe a
c Elims
as1 Elims
as2
_ -> Maybe a
forall a. Maybe a
Nothing
_ -> case (Term
e1, Term
e2) of
(I.MetaV{}, _) -> t -> Maybe a
c t
n
(_, I.MetaV{}) -> t -> Maybe a
c t
n
(I.Lam hid1 :: ArgInfo
hid1 b1 :: Abs Term
b1, I.Lam hid2 :: ArgInfo
hid2 b2 :: Abs Term
b2) | ArgInfo
hid1 ArgInfo -> ArgInfo -> Bool
forall a. Eq a => a -> a -> Bool
== ArgInfo
hid2 -> Int -> t -> (t -> Maybe a) -> Term -> Term -> Maybe a
f (Int
nl Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) t
n t -> Maybe a
c (Abs Term -> Term
forall t a. Subst t a => Abs a -> a
I.absBody Abs Term
b1) (Abs Term -> Term
forall t a. Subst t a => Abs a -> a
I.absBody Abs Term
b2)
(I.Lit lit1 :: Literal
lit1, I.Lit lit2 :: Literal
lit2) | Literal
lit1 Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
lit2 -> t -> Maybe a
c (t
n t -> t -> t
forall a. Num a => a -> a -> a
+ 1)
(I.Def n1 :: QName
n1 as1 :: Elims
as1, I.Def n2 :: QName
n2 as2 :: Elims
as2) | QName
n1 QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
n2 -> Int -> t -> (t -> Maybe a) -> Elims -> Elims -> Maybe a
fes Int
nl (t
n t -> t -> t
forall a. Num a => a -> a -> a
+ 1) t -> Maybe a
c Elims
as1 Elims
as2
(I.Con n1 :: ConHead
n1 _ as1 :: Elims
as1, I.Con n2 :: ConHead
n2 _ as2 :: Elims
as2) | ConHead
n1 ConHead -> ConHead -> Bool
forall a. Eq a => a -> a -> Bool
== ConHead
n2 -> Int -> t -> (t -> Maybe a) -> Elims -> Elims -> Maybe a
fs Int
nl (t
n t -> t -> t
forall a. Num a => a -> a -> a
+ 1) t -> Maybe a
c Elims
as1 Elims
as2
(I.Pi (I.Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info1, unDom :: forall t e. Dom' t e -> e
unDom = Type
it1}) ot1 :: Abs Type
ot1, I.Pi (I.Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
domInfo = ArgInfo
info2, unDom :: forall t e. Dom' t e -> e
unDom = Type
it2}) ot2 :: Abs Type
ot2) | ArgInfo -> Hiding
Cm.argInfoHiding ArgInfo
info1 Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== ArgInfo -> Hiding
Cm.argInfoHiding ArgInfo
info2 -> Int -> t -> (t -> Maybe a) -> Type -> Type -> Maybe a
ft Int
nl t
n (\n :: t
n -> Int -> t -> (t -> Maybe a) -> Type -> Type -> Maybe a
ft (Int
nl Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) t
n t -> Maybe a
c (Abs Type -> Type
forall t a. Subst t a => Abs a -> a
I.absBody Abs Type
ot1) (Abs Type -> Type
forall t a. Subst t a => Abs a -> a
I.absBody Abs Type
ot2)) Type
it1 Type
it2
(I.Sort{}, I.Sort{}) -> t -> Maybe a
c t
n
_ -> Maybe a
forall a. Maybe a
Nothing
fs :: Int -> t -> (t -> Maybe a) -> Elims -> Elims -> Maybe a
fs nl :: Int
nl n :: t
n c :: t -> Maybe a
c es1 :: Elims
es1 es2 :: Elims
es2 = case (Elims
es1, Elims
es2) of
([], []) -> t -> Maybe a
c t
n
(I.Apply (Cm.Arg info1 :: ArgInfo
info1 e1 :: Term
e1) : es1 :: Elims
es1, I.Apply (Cm.Arg info2 :: ArgInfo
info2 e2 :: Term
e2) : es2 :: Elims
es2) | ArgInfo -> Hiding
Cm.argInfoHiding ArgInfo
info1 Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== ArgInfo -> Hiding
Cm.argInfoHiding ArgInfo
info2 -> Int -> t -> (t -> Maybe a) -> Term -> Term -> Maybe a
f Int
nl t
n (\n :: t
n -> Int -> t -> (t -> Maybe a) -> Elims -> Elims -> Maybe a
fs Int
nl t
n t -> Maybe a
c Elims
es1 Elims
es2) Term
e1 Term
e2
_ -> Maybe a
forall a. Maybe a
Nothing
fes :: Int -> t -> (t -> Maybe a) -> Elims -> Elims -> Maybe a
fes nl :: Int
nl n :: t
n c :: t -> Maybe a
c es1 :: Elims
es1 es2 :: Elims
es2 = case (Elims
es1, Elims
es2) of
([], []) -> t -> Maybe a
c t
n
(I.Proj _ f :: QName
f : es1 :: Elims
es1, I.Proj _ f' :: QName
f' : es2 :: Elims
es2) | QName
f QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
f' -> Int -> t -> (t -> Maybe a) -> Elims -> Elims -> Maybe a
fes Int
nl t
n t -> Maybe a
c Elims
es1 Elims
es2
(I.Apply (Cm.Arg info1 :: ArgInfo
info1 e1 :: Term
e1) : es1 :: Elims
es1, I.Apply (Cm.Arg info2 :: ArgInfo
info2 e2 :: Term
e2) : es2 :: Elims
es2) | ArgInfo -> Hiding
Cm.argInfoHiding ArgInfo
info1 Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== ArgInfo -> Hiding
Cm.argInfoHiding ArgInfo
info2 -> Int -> t -> (t -> Maybe a) -> Term -> Term -> Maybe a
f Int
nl t
n (\n :: t
n -> Int -> t -> (t -> Maybe a) -> Elims -> Elims -> Maybe a
fes Int
nl t
n t -> Maybe a
c Elims
es1 Elims
es2) Term
e1 Term
e2
_ -> Maybe a
forall a. Maybe a
Nothing