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)
  -- Nothing - Def
  -- Just npar - Con with npar parameters which don't appear in Agda

data TMode = TMAll -- can be extended to distinguish between different modes (all, only def)
 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 S -> (a, [b])
r (a, [b]) -> S -> S
w = do (a
m, [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
                  (b
x:[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 MetaId
imi [Hint]
icns [Type]
typs = do
 [(Bool, Term, Term)]
eqs <- TCM [(Bool, Term, Term)]
getEqs
 let
  r :: [AN.QName] -> TOM [AN.QName]
  r :: [QName] -> TOM [QName]
r [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 (\MapS QName (TMode, ConstRef O)
x S
y -> S
y {sConsts :: MapS QName (TMode, ConstRef O)
sConsts = MapS QName (TMode, ConstRef O)
x})
   case Maybe QName
nxt of
    Just 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 (TMode
mode, 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 [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
                        [] -> Int
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, [])
     (DeclCont O
cont, [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 {MB.primClauses = []} -> throwError $ strMsg "Auto: Primitive functions are not supported" -- Andreas, 2013-06-17 breaks interaction/AutoMisc
      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 (\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 -- the value of recPars seems unreliable or don't know what it signifies
       let pars :: Int -> Type -> [Arg Term]
pars Int
n (I.El Sort' Term
_ (I.Pi Dom Type
it 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
- Int
1) (Abs Type -> Type
forall a. Abs a -> a
I.unAbs Abs Type
typ)
           pars Int
_ (I.El Sort' Term
_ Term
_) = []
           contyp :: Int -> Telescope -> Type
contyp Int
npar Telescope
I.EmptyTel = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
I.El (Integer -> Sort' Term
I.mkType Integer
0 {- arbitrary -}) (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
- Int
1) Type
typ
           contyp Int
npar (I.ExtendTel Dom Type
it (I.Abs ArgName
v Telescope
tel)) = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
I.El (Integer -> Sort' Term
I.mkType Integer
0 {- arbitrary -}) (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
+ Int
1) Telescope
tel)))
           contyp Int
npar (I.ExtendTel 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 Int
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 [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 (\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 (\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, []{-map snd fields-})
      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 -- make sure that datatype is included
       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 (Int
nomi,[Arg QName]
_), QName
_) = 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 (\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
    Maybe QName
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 (\MapS
  MetaId
  (Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
x 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 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_ (\((Bool
_, Term
e, Term
i), 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
          (Map Int (Maybe (Bool, MExp O, MExp O))
eqsm, [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 {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 [Int
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
                       --sol <- norm (I.MetaV mi args)
                       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
                     MetaInstantiation
_ -> 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
        Maybe Term
Nothing -> () -> StateT S TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
        Just 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 {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
       (Type
targettype, [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 {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 {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 {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 (\(Metavar (Exp O) (RefInfo O)
m, Maybe (MExp O, [MExp O])
_, [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
      Maybe MetaId
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 (\MapS Int (Maybe (Bool, MExp O, MExp O))
x 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 Int
eqi -> do
         let (Bool
ineq, Term
e, 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 {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 (\Maybe (Bool, MExp O, MExp O)
_ -> (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
        Maybe Int
Nothing ->
         [QName] -> TOM [QName]
forall (m :: * -> *) a. Monad m => a -> m a
return [QName]
projfcns
 (([ConstRef O]
icns', [MExp O]
typs'), 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 Bool
iscon 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 (\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 (a
x, Just (b
y, c
z), d
w) = (a
x, b
y, c
z, d
w)
 flatten (a
x, Maybe (b, c)
Nothing, d
w) = (a, b, c, d)
forall a. HasCallStack => a
__IMPOSSIBLE__

 fromJust :: Maybe p -> p
fromJust (Just p
x) = p
x
 fromJust Maybe p
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 Bool
iscon QName
name 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 (TMode
mode', 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 [ConstRef O
con] [ConstRef O]
_ = 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
    Maybe (TMode, ConstRef O)
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]
++ ArgName
".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}) -- ?? correct value of deffreevars for records?
     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}) -- ?? correct value of deffreevars for records?
     (S -> S) -> StateT S TCM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\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
  Defn
_ -> 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 (TMode
mode', ConstRef O
c) ->
     ConstRef O -> StateT S TCM (ConstRef O)
forall (m :: * -> *) a. Monad m => a -> m a
return ConstRef O
c
    Maybe (TMode, ConstRef O)
Nothing -> do
     (Maybe (Int, [Arg QName])
miscon, 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 -> 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 {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 MetaId
mainm 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 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 (Metavar (Exp O) (RefInfo O)
m, Maybe (MExp O, [MExp O])
_, [MetaId]
_) ->
   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
  Maybe
  (Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
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 { 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
$ \ 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 Comparison
ineq CompareAs
_ Term
i 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 MetaId
_) 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
    Constraint
_ -> 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
$
  ArgName
"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
$
  ArgName
"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
$
  ArgName
"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 Clause
cl = do
    let -- Jesper, 2016-07-28:
     -- I can't figure out if this should be the old or new
     -- clause body (i.e. relative to the positions of pattern variables or
     -- relative to the clauseTel). Both options pass the test suite, so I
     -- have the impression it doesn't actually matter.
     -- ALTERNATIVE CODE:
     -- perm = fromMaybe __IMPOSSIBLE__ $ IP.clausePerm cl
     -- body = applySubst (renamingR perm) $ I.clauseBody cl
        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 Arg Pattern
p = case Arg Pattern -> Pattern
forall e. Arg e -> e
Cm.unArg Arg Pattern
p of
    I.IApplyP PatternInfo
_ Term
_ Term
_ 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 PatternInfo
_ 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 PatternInfo
_ Term
_  -> 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
"_"
      -- because Agda includes these when referring to variables in the body
    I.ConP ConHead
con ConPatternInfo
_ [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 (Int
npar,[Arg QName]
_) = 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')

    -- UNSUPPORTED CASES
    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 Sort' Term
_ Term
t) = Term -> StateT S TCM (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Term
t -- sort info is thrown away

instance Conversion TOM I.Term (MExp O) where
  convert :: Term -> StateT S TCM (MExp O)
convert Term
v0 =
    case Term -> Term
I.unSpine Term
v0 of
      I.Var Int
v Elims
es -> do
        let Just [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 ArgInfo
info 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
_       -> Term -> StateT S TCM (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Term
t
      I.Level 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 QName
name Elims
es -> do
        let Just [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 ConHead
con ConInfo
ci Elims
es -> do
        let Just [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 (Int
npar,[Arg QName]
_) = 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 (\MArgList O
x Int
_ -> 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' [Int
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}) 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 Int
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 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 Sort' Term
_ -> 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 MetaId
mid Elims
_ -> 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
              Maybe MetaId
Nothing -> () -> StateT S TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
              Just 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 { 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 (\(Metavar (Exp O) (RefInfo O)
m, Maybe (MExp O, [MExp O])
x, [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
_ -> Term -> StateT S TCM (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Term
t
      I.DontCare Term
_ -> 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 ArgInfo
info 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 [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 (\ (Hiding
hid,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 Comparison
MB.CmpEq = Bool
False
tomyIneq Comparison
MB.CmpLeq = Bool
True

-- ---------------------------------------------

fmType :: I.MetaId -> I.Type -> Bool
fmType :: MetaId -> Type -> Bool
fmType MetaId
m (I.El Sort' Term
_ Term
t) = MetaId -> Term -> Bool
fmExp MetaId
m Term
t

fmExp :: I.MetaId -> I.Term -> Bool
fmExp :: MetaId -> Term -> Bool
fmExp MetaId
m (I.Var Int
_ 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 MetaId
m (I.Lam ArgInfo
_ Abs Term
b) = MetaId -> Term -> Bool
fmExp MetaId
m (Abs Term -> Term
forall a. Abs a -> a
I.unAbs Abs Term
b)
fmExp MetaId
m (I.Lit Literal
_) = Bool
False
fmExp MetaId
m (I.Level (I.Max Integer
_ [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 MetaId
m (I.Def QName
_ 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 MetaId
m (I.Con ConHead
_ ConInfo
ci 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 MetaId
m (I.Pi Dom Type
x 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 MetaId
m (I.Sort Sort' Term
_) = Bool
False
fmExp MetaId
m (I.MetaV MetaId
mid Elims
_) = MetaId
mid MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
m
fmExp MetaId
m (I.DontCare Term
_) = Bool
False
fmExp MetaId
_ I.Dummy{} = Bool
False

fmExps :: I.MetaId -> I.Args -> Bool
fmExps :: MetaId -> [Arg Term] -> Bool
fmExps MetaId
m [] = Bool
False
fmExps MetaId
m (Arg Term
a : [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 MetaId
m (I.Plus Integer
_ LevelAtom' Term
l) = case LevelAtom' Term
l of
  I.MetaLevel MetaId
m' Elims
_   -> MetaId
m MetaId -> MetaId -> Bool
forall a. Eq a => a -> a -> Bool
== MetaId
m'
  I.NeutralLevel NotBlocked
_ Term
v -> MetaId -> Term -> Bool
fmExp MetaId
m Term
v
  I.BlockedLevel MetaId
_ Term
v -> MetaId -> Term -> Bool
fmExp MetaId
m Term
v
  I.UnreducedLevel Term
v -> MetaId -> Term -> Bool
fmExp MetaId
m Term
v

-- ---------------------------------------------

icnvh :: Hiding -> Cm.ArgInfo
icnvh :: Hiding -> ArgInfo
icnvh 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
    -- Andreas, 2017-01-18, issue #819.
    -- Visible arguments are made UserWritten,
    -- otherwise they might not be printed in patterns.
    o :: Origin
o = case Hiding
h of
          Hiding
NotHidden  -> Origin
Cm.UserWritten
          Instance{} -> Origin
Cm.Inserted
          Hiding
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 MM a (RefInfo O)
meta = case MM a (RefInfo O)
meta of
    NotM a
a -> a -> MOT b
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert a
a
    Meta 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
        Maybe a
Nothing -> ArgName -> MOT b
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArgName
"meta not bound"
        Just 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 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
           MId
NoId  -> ArgName
"x"
           Id ArgName
id -> ArgName
id

instance Conversion MOT (Exp O) I.Type where
  convert :: Exp O -> MOT Type
convert Exp O
e = Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
I.El (Integer -> Sort' Term
I.mkType Integer
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
              -- 0 is arbitrary, sort not read by Agda when reifying

instance Conversion MOT (Exp O) I.Term where
  convert :: Exp O -> ExceptT ArgName IO Term
convert Exp O
e = case Exp O
e of
    App Maybe (Metavar (Exp O) (RefInfo O))
_ OKHandle (RefInfo O)
_ (Var Int
v) MArgList O
as -> Int -> MArgList O -> Term -> ExceptT ArgName IO Term
frommyExps Int
0 MArgList O
as (Int -> Elims -> Term
I.Var Int
v [])
    App Maybe (Metavar (Exp O) (RefInfo O))
_ OKHandle (RefInfo O)
_ (Const ConstRef O
c) 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 (Maybe (Int, [Arg QName])
iscon, QName
name) = ConstDef O -> O
forall o. ConstDef o -> o
cdorigin ConstDef O
cdef
{-
   case iscon of
      Just n -> do
        v <- getConTerm name -- We are not in TCM
        frommyExps n as v
-}
          (Int
ndrop, QName -> Elims -> Term
h) = case Maybe (Int, [Arg QName])
iscon of
                         Just (Int
n,[Arg QName]
fs) -> (Int
n, \ 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)
                         Maybe (Int, [Arg QName])
Nothing -> (Int
0, \ QName
f 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 Hiding
hid 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 Maybe (Metavar (Exp O) (RefInfo O))
_ Hiding
hid Bool
_ MExp O
x 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
   -- maybe have case for Pi where possdep is False which produces Fun (and has to unweaken y), return $ I.Fun (Cm.Arg (icnvh hid) x') y'
    Sort (Set 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 Sort
Type -> ExceptT ArgName IO Term
forall a. HasCallStack => a
__IMPOSSIBLE__
    Sort 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 Integer
0) -- hoping it's thrown away

    AbsurdLambda 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 Int
0 [])

frommyExps :: Nat -> MArgList O -> I.Term -> ExceptT String IO I.Term
frommyExps :: Int -> MArgList O -> Term -> ExceptT ArgName IO Term
frommyExps Int
ndrop (Meta Metavar (ArgList O) (RefInfo O)
m) 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
  Maybe (ArgList O)
Nothing -> ArgName -> ExceptT ArgName IO Term
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ArgName
"meta not bound"
  Just 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 Int
ndrop (NotM ArgList O
as) Term
trm =
 case ArgList O
as of
  ArgList O
ALNil -> Term -> ExceptT ArgName IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return Term
trm
  ALCons Hiding
_ MExp O
_ MArgList O
xs | Int
ndrop Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 -> Int -> MArgList O -> Term -> ExceptT ArgName IO Term
frommyExps (Int
ndrop Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) MArgList O
xs Term
trm
  ALCons Hiding
hid MExp O
x 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)

  -- Andreas, 2013-10-19 TODO: restore postfix projections
  ALProj MArgList O
eas MM (ConstRef O) (RefInfo O)
idx Hiding
hid 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 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 ArgName
"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 Int
0 MArgList O
eas (QName -> Elims -> Term
I.Def QName
name [])
   Int -> MArgList O -> Term -> ExceptT ArgName IO Term
frommyExps Int
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 MArgList O
xs | Int
ndrop Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 -> Int -> MArgList O -> Term -> ExceptT ArgName IO Term
frommyExps (Int
ndrop Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) MArgList O
xs Term
trm
  ALConPar MArgList O
_ -> ExceptT ArgName IO Term
forall a. HasCallStack => a
__IMPOSSIBLE__
 where
  addend :: Arg Term -> Term -> Term
addend Arg Term
x (I.Var Int
h 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 Arg Term
x (I.Con ConHead
h ConInfo
ci 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 Arg Term
x (I.Def QName
h 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 Arg Term
_ Term
_ = Term
forall a. HasCallStack => a
__IMPOSSIBLE__

-- --------------------------------

abslamvarname :: String
abslamvarname :: ArgName
abslamvarname = ArgName
"\0absurdlambda"

modifyAbstractExpr :: A.Expr -> A.Expr
modifyAbstractExpr :: Expr -> Expr
modifyAbstractExpr = Expr -> Expr
f
 where
  f :: Expr -> Expr
f (A.App AppInfo
i Expr
e1 (Cm.Arg ArgInfo
info (Cm.Named Maybe NamedName
n 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 ExprInfo
i (A.DomainFree TacticAttr
_ NamedArg Binder
x) Expr
_)
     | A.Binder Maybe Pattern
_ (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 ExprInfo
i LamBinding
b Expr
e) = ExprInfo -> LamBinding -> Expr -> Expr
A.Lam ExprInfo
i LamBinding
b (Expr -> Expr
f Expr
e)
  f (A.Rec ExprInfo
i 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 ExprInfo
i Expr
e 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 ScopeInfo
i Expr
e) = ScopeInfo -> Expr -> Expr
A.ScopedExpr ScopeInfo
i (Expr -> Expr
f Expr
e)
  f Expr
e = Expr
e

modifyAbstractClause :: A.Clause -> A.Clause
modifyAbstractClause :: Clause -> Clause
modifyAbstractClause (A.Clause LHS
lhs [ProblemEq]
spats (A.RHS Expr
e Maybe Expr
mc) WhereDeclarations
decls 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 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 Map QName (TMode, ConstRef O)
cmap MetaId
mainm Clause
clause = do
 let cnvps :: [(Hiding, MId)]
-> [NamedArg Pattern] -> TCM ([(Hiding, MId)], [CSPat O])
cnvps [(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 [(Hiding, MId)]
ns (NamedArg Pattern
p : [NamedArg Pattern]
ps) = do
      ([(Hiding, MId)]
ns', [CSPat O]
ps') <- [(Hiding, MId)]
-> [NamedArg Pattern] -> TCM ([(Hiding, MId)], [CSPat O])
cnvps [(Hiding, MId)]
ns [NamedArg Pattern]
ps
      ([(Hiding, MId)]
ns'', 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 [(Hiding, MId)]
ns 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 PatternInfo
_ 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 PatternInfo
_ Term
_ Term
_ 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 ConHead
con ConPatternInfo
_ [NamedArg Pattern]
ps -> do
        let c :: QName
c = ConHead -> QName
I.conName ConHead
con
        (ConstRef O
c2, S
_) <- 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})
        ([(Hiding, MId)]
ns', [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 (Int
npar,[Arg QName]
_) = 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 PatternInfo
_ Term
t -> do
        (MExp O
t2, S
_) <- 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

 ([(Hiding, MId)]
names, [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 (CSCtx O
ids, [CSPat O]
pats, 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 Hiding
hid (MId
mid, a
t) : [HI (MId, a)]
ctx) = do
      let 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 a
0 [] [(Int, b)]
perm 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 a
n [] [(Int, b)]
_ b
_ = t IO ([(Int, b)], b)
forall a. HasCallStack => a
__IMPOSSIBLE__
     getperms a
0 (HI (CSPatI (Maybe (a, b), b))
p : [HI (CSPatI (Maybe (a, b), b))]
ps) [(Int, b)]
perm b
nv = do
      ([(Int, b)]
perm, 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 a
0 [HI (CSPatI (Maybe (a, b), b))]
ps [(Int, b)]
perm b
nv
     getperms a
n (HI Hiding
_ CSPatExp{} : [HI (CSPatI (Maybe (a, b), b))]
ps) [(Int, b)]
perm 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
- a
1) [HI (CSPatI (Maybe (a, b), b))]
ps [(Int, b)]
perm b
nv
     getperms a
n (HI Hiding
_ CSOmittedArg{} : [HI (CSPatI (Maybe (a, b), b))]
ps) [(Int, b)]
perm 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
- a
1) [HI (CSPatI (Maybe (a, b), b))]
ps [(Int, b)]
perm b
nv
     getperms a
n (HI (CSPatI (Maybe (a, b), b))
_ : [HI (CSPatI (Maybe (a, b), b))]
_) [(Int, b)]
_ b
_ = 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 Hiding
_ CSPatI (Maybe (a, b), b)
p) [(Int, b)]
perm b
nv =
      case CSPatI (Maybe (a, b), b)
p of
       --CSPatVar v -> return (length ids + nv - 1 - v : perm, nv)
       CSPatVar 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
- Int
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
+ b
1)
       CSPatConApp ConstRef (Maybe (a, b), b)
c [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 (a
ndrop,b
_), b
_) = 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 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
+ b
1)
       CSPatI (Maybe (a, b), b)
_ -> t IO ([(Int, b)], b)
forall a. HasCallStack => a
__IMPOSSIBLE__
 ([(Int, Int)]
rperm, 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 Int
0 [CSPat O]
pats [] Int
0
 let --perm = reverse rperm
     perm :: [Int]
perm = (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> let Just 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) [Int
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
- Int
1]
     --renperm = map (\i -> length ids + nv - 1 - i) rperm
     --renm = rename (\i -> renperm !! i)
     cnvps :: a -> [HI (CSPatI (Maybe (a, b), QName))] -> t IO [NamedArg Pattern]
cnvps a
0 [] = [NamedArg Pattern] -> t IO [NamedArg Pattern]
forall (m :: * -> *) a. Monad m => a -> m a
return []
     cnvps a
n [] = t IO [NamedArg Pattern]
forall a. HasCallStack => a
__IMPOSSIBLE__
     cnvps a
0 (HI (CSPatI (Maybe (a, b), QName))
p : [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 a
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 a
n (HI Hiding
_ CSPatExp{} : [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
- a
1) [HI (CSPatI (Maybe (a, b), QName))]
ps
     cnvps a
n (HI Hiding
_ CSOmittedArg{} : [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
- a
1) [HI (CSPatI (Maybe (a, b), QName))]
ps
     cnvps a
n (HI (CSPatI (Maybe (a, b), QName))
_ : [HI (CSPatI (Maybe (a, b), QName))]
_) = t IO [NamedArg Pattern]
forall a. HasCallStack => a
__IMPOSSIBLE__
     cnvp :: HI (CSPatI (Maybe (a, b), QName)) -> t IO (NamedArg Pattern)
cnvp (HI Hiding
hid CSPatI (Maybe (a, b), QName)
p) = do
      Pattern
p' <- case CSPatI (Maybe (a, b), QName)
p of
       CSPatVar 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 Hiding
_ (Id ArgName
n, MExp O
_) = CSCtx O
ids CSCtx O -> Int -> HI (MId, MExp O)
forall a. [a] -> Int -> a
!! Int
v in ArgName
n)
       CSPatConApp ConstRef (Maybe (a, b), QName)
c [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 (a
ndrop,b
_), 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 [] -- TODO: restore record fields!
        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 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 {- renm e -} -- renaming before adding to clause below
        Pattern -> t IO Pattern
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Pattern
forall a. Term -> Pattern' a
I.dotP Term
e')
       CSPatI (Maybe (a, b), QName)
CSAbsurd -> t IO Pattern
forall a. HasCallStack => a
__IMPOSSIBLE__ -- CSAbsurd not used
       CSPatI (Maybe (a, b), QName)
_ -> 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'   -- TODO: recover names
 [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 Int
0 [CSPat O]
pats
 Maybe Term
body <- case Maybe (MExp O)
mrhs of
          Maybe (MExp O)
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 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 -- TODO: compute clause type
   , clauseCatchall :: Bool
I.clauseCatchall = Bool
False
   , clauseRecursive :: Maybe Bool
I.clauseRecursive   = Maybe Bool
forall a. Maybe a
Nothing -- TODO: Don't know here whether recursive or not !?
   , clauseUnreachable :: Maybe Bool
I.clauseUnreachable = Maybe Bool
forall a. Maybe a
Nothing -- TODO: Don't know here whether reachable or not !?
   , 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 Hiding
_ CSPatI o
p) = case CSPatI o
p of
         CSPatConApp{} -> Bool
True
         CSPatI o
_ -> 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 MM a blk
x = let NotM a
x' = MM a blk
x in a
x'
  f :: Int -> MExp o -> Bool
f Int
v MExp o
e = case MExp o -> Exp o
forall a blk. MM a blk -> a
mr MExp o
e of
   App Maybe (UId o)
_ OKHandle (RefInfo o)
_ Elr o
elr MArgList o
args -> case Elr o
elr of
    Var Int
v' | Int
v' Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
v -> Bool
False
    Elr o
_ -> Int -> MArgList o -> Bool
fs Int
v MArgList o
args
   Lam Hiding
_ (Abs MId
_ MExp o
b) -> Int -> MExp o -> Bool
f (Int
v Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) MExp o
b
   Pi Maybe (UId o)
_ Hiding
_ Bool
_ MExp o
it (Abs MId
_ 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
+ Int
1) MExp o
ot
   Sort{} -> Bool
True

   AbsurdLambda{} -> Bool
True


  fs :: Int -> MArgList o -> Bool
fs Int
v MArgList o
es = case MArgList o -> ArgList o
forall a blk. MM a blk -> a
mr MArgList o
es of
   ArgList o
ALNil -> Bool
True
   ALCons Hiding
_ MExp o
a 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 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 ConstRef o
ee = Int -> MExp o -> MExp o
forall t. Num t => t -> MExp o -> MExp o
f (Int
0 :: Int)
 where
  mr :: MM a blk -> a
mr MM a blk
x = let NotM a
x' = MM a blk
x in a
x'
  f :: t -> MExp o -> MExp o
f t
n MExp o
e = case MExp o -> Exp o
forall a blk. MM a blk -> a
mr MExp o
e of
   Pi Maybe (UId o)
uid Hiding
hid Bool
possdep MExp o
it (Abs MId
id 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
+ t
1) MExp o
ot))
   Exp o
_ -> 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 Int
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 Int
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 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  -- Andreas, 2016-09-04, issue #2162
  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
    IPClause
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 QName
f Int
clauseNo Type
_ Maybe (Substitution' Term)
_ SpineClause
_ Closure ()
_ [Closure IPBoundary]
_ -> do
      (CaseContext
_, ([Clause]
_, Clause
c, [Clause]
_)) <- 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 Term
e =
     case Term
e of
      I.MetaV{} -> Bool
True
      Term
_ -> Bool
False

-- ---------------------------------------

matchType :: Int -> Int -> I.Type -> I.Type -> Maybe (Nat, Nat) -- Nat is deffreevars of const, Nat is ctx length of target type, left arg is const type, right is target type
matchType :: Int -> Int -> Type -> Type -> Maybe (Int, Int)
matchType Int
cdfv Int
tctx Type
ctyp 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 t
0 Type
ctyp = a -> Int -> Type -> Maybe (a, a)
forall a a. (Num a, Num a) => a -> Int -> Type -> Maybe (a, a)
tr a
0 Int
0 Type
ctyp
  trmodps t
n Type
ctyp = case Type -> Term
forall t a. Type'' t a -> a
I.unEl Type
ctyp of
   I.Pi Dom Type
_ Abs Type
ot -> t -> Type -> Maybe (a, a)
trmodps (t
n t -> t -> t
forall a. Num a => a -> a -> a
- t
1) (Abs Type -> Type
forall t a. Subst t a => Abs a -> a
I.absBody Abs Type
ot)
   Term
_ -> Maybe (a, a)
forall a. HasCallStack => a
__IMPOSSIBLE__
  tr :: a -> Int -> Type -> Maybe (a, a)
tr a
narg Int
na 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 Int
0 a
0 a -> Maybe a
forall a. a -> Maybe a
Just Type
ctyp Type
ttyp of
    Just a
n -> (a, a) -> Maybe (a, a)
forall a. a -> Maybe a
Just (a
n, a
narg)
    Maybe a
Nothing -> case Type -> Term
forall t a. Type'' t a -> a
I.unEl Type
ctyp of
     I.Pi Dom Type
_ (I.Abs ArgName
_ Type
ot) -> a -> Int -> Type -> Maybe (a, a)
tr (a
narg a -> a -> a
forall a. Num a => a -> a -> a
+ a
1) (Int
na Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Type
ot
     I.Pi Dom Type
_ (I.NoAbs ArgName
_ Type
ot) -> a -> Int -> Type -> Maybe (a, a)
tr (a
narg a -> a -> a
forall a. Num a => a -> a -> a
+ a
1) Int
na Type
ot
     Term
_ -> Maybe (a, a)
forall a. Maybe a
Nothing
   where
    ft :: Int -> t -> (t -> Maybe a) -> Type -> Type -> Maybe a
ft Int
nl t
n t -> Maybe a
c (I.El Sort' Term
_ Term
e1) (I.El Sort' Term
_ 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 Int
nl t
n t -> Maybe a
c Term
e1 Term
e2 = case Term
e1 of
     I.Var Int
v1 Elims
as1 | Int
v1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
nl -> case Term
e2 of
      I.Var Int
v2 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
+ t
1) t -> Maybe a
c Elims
as1 Elims
as2
      Term
_ -> Maybe a
forall a. Maybe a
Nothing
     I.Var Int
v1 Elims
_ | 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 -- unify vars with no args?
     I.Var Int
v1 Elims
as1 -> case Term
e2 of
      I.Var Int
v2 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
+ t
1) t -> Maybe a
c Elims
as1 Elims
as2
      Term
_ -> Maybe a
forall a. Maybe a
Nothing
     Term
_ -> case (Term
e1, Term
e2) of
      (I.MetaV{}, Term
_) -> t -> Maybe a
c t
n
      (Term
_, I.MetaV{}) -> t -> Maybe a
c t
n
      (I.Lam ArgInfo
hid1 Abs Term
b1, I.Lam ArgInfo
hid2 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
+ Int
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 Literal
lit1, I.Lit 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
+ t
1)
      (I.Def QName
n1 Elims
as1, I.Def QName
n2 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
+ t
1) t -> Maybe a
c Elims
as1 Elims
as2
      (I.Con ConHead
n1 ConInfo
_ Elims
as1, I.Con ConHead
n2 ConInfo
_ 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
+ t
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})  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})  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 (\t
n -> Int -> t -> (t -> Maybe a) -> Type -> Type -> Maybe a
ft (Int
nl Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
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 -- sloppy
      (Term, Term)
_ -> Maybe a
forall a. Maybe a
Nothing
    fs :: Int -> t -> (t -> Maybe a) -> Elims -> Elims -> Maybe a
fs Int
nl t
n t -> Maybe a
c Elims
es1 Elims
es2 = case (Elims
es1, Elims
es2) of
     ([], []) -> t -> Maybe a
c t
n
     (I.Apply (Cm.Arg ArgInfo
info1 Term
e1) : Elims
es1, I.Apply (Cm.Arg ArgInfo
info2 Term
e2) : 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 (\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
     (Elims, Elims)
_ -> Maybe a
forall a. Maybe a
Nothing
    fes :: Int -> t -> (t -> Maybe a) -> Elims -> Elims -> Maybe a
fes Int
nl t
n t -> Maybe a
c Elims
es1 Elims
es2 = case (Elims
es1, Elims
es2) of
     ([], []) -> t -> Maybe a
c t
n
     (I.Proj ProjOrigin
_ QName
f : Elims
es1, I.Proj ProjOrigin
_ QName
f' : 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 ArgInfo
info1 Term
e1) : Elims
es1, I.Apply (Cm.Arg ArgInfo
info2 Term
e2) : 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 (\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
     (Elims, Elims)
_ -> Maybe a
forall a. Maybe a
Nothing