module Agda.Auto.Convert where

import Control.Monad.Except
import Control.Monad.State

import Data.Bifunctor (first)
import Data.IORef
import Data.Maybe (catMaybes)
import Data.Map (Map)
import qualified Data.Map as Map

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.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 :: forall a b. 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 :: forall a b.
(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 (TCMT IO) (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 (TCMT IO) ()
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'' Term Term]
-> 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'' Term Term]
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 <- (S -> Map QName (TMode, ConstRef O))
-> StateT S (TCMT IO) (Map QName (TMode, ConstRef O))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (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))
-> (S -> MapS QName (TMode, ConstRef O))
-> S
-> Map QName (TMode, ConstRef O)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (TCMT IO) Definition
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Definition -> StateT S (TCMT IO) Definition)
-> TCM Definition -> StateT S (TCMT IO) Definition
forall a b. (a -> b) -> a -> b
$ QName -> TCM Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
cn
     let typ :: Type'' Term Term
typ = Definition -> Type'' Term Term
MB.defType Definition
def
         defn :: Defn
defn = Definition -> Defn
MB.theDef Definition
def
     Type'' Term Term
typ <- TCM (Type'' Term Term) -> StateT S (TCMT IO) (Type'' Term Term)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (Type'' Term Term) -> StateT S (TCMT IO) (Type'' Term Term))
-> TCM (Type'' Term Term) -> StateT S (TCMT IO) (Type'' Term Term)
forall a b. (a -> b) -> a -> b
$ Type'' Term Term -> TCM (Type'' Term Term)
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Type'' Term Term
typ
     MExp O
typ' <- Type'' Term Term -> StateT S (TCMT IO) (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Type'' Term Term
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 {namedClausePats :: Clause -> NAPs
I.namedClausePats = NAPs
xs} : [Clause]
_ -> NAPs -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length NAPs
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 (TCMT IO) (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 (TCMT IO) (DeclCont O, [QName])
forall (m :: * -> *) a. Monad m => a -> m a
return (DeclCont O
forall o. DeclCont o
Postulate, [])
      MB.GeneralizableVar{} -> StateT S (TCMT IO) (DeclCont O, [QName])
forall a. HasCallStack => a
__IMPOSSIBLE__
      MB.AbstractDefn{} -> (DeclCont O, [QName]) -> StateT S (TCMT IO) (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 (TCMT IO) (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 (TCMT IO) (DeclCont O, [QName])
forall {m :: * -> *} {o} {a}.
(Monad m, Conversion m [Clause] [Clause o]) =>
[Clause] -> m (DeclCont o, [a])
clausesToDef [Clause]
clauses
      MB.PrimitiveSort{} -> StateT S (TCMT IO) (DeclCont O, [QName])
forall a. HasCallStack => a
__IMPOSSIBLE__
      MB.Datatype {dataCons :: Defn -> [QName]
MB.dataCons = [QName]
cons} -> do
       [ConstRef O]
cons2 <- (QName -> StateT S (TCMT IO) (ConstRef O))
-> [QName] -> StateT S (TCMT IO) [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 (TCMT IO) (ConstRef O)
getConst Bool
True QName
con TMode
TMAll) [QName]
cons
       (DeclCont O, [QName]) -> StateT S (TCMT IO) (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'' Term Term -> [Arg Term]
pars Int
n (I.El Sort' Term
_ (I.Pi Dom (Type'' Term Term)
it Abs (Type'' Term Term)
typ)) = ArgInfo -> Term -> Arg Term
forall e. ArgInfo -> e -> Arg e
Cm.Arg (Dom (Type'' Term Term) -> ArgInfo
forall t e. Dom' t e -> ArgInfo
I.domInfo Dom (Type'' Term Term)
it) (Int -> Term
I.var Int
n) Arg Term -> [Arg Term] -> [Arg Term]
forall a. a -> [a] -> [a]
:
                                           Int -> Type'' Term Term -> [Arg Term]
pars (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Abs (Type'' Term Term) -> Type'' Term Term
forall a. Abs a -> a
I.unAbs Abs (Type'' Term Term)
typ)
           pars Int
_ (I.El Sort' Term
_ Term
_) = []
           contyp :: Int -> Telescope -> Type'' Term Term
contyp Int
npar Telescope
I.EmptyTel = Sort' Term -> Term -> Type'' Term Term
forall t a. Sort' t -> a -> Type'' t a
I.El (Integer -> Sort' Term
I.mkType Integer
0 {- arbitrary -}) (Term -> Type'' Term Term) -> Term -> Type'' Term Term
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) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
forall a. Arg a -> Elim' a
I.Apply ([Arg Term] -> Elims) -> [Arg Term] -> Elims
forall a b. (a -> b) -> a -> b
$ Int -> Type'' Term Term -> [Arg Term]
pars (Int
npar Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Type'' Term Term
typ
           contyp Int
npar (I.ExtendTel Dom (Type'' Term Term)
it (I.Abs String
v Telescope
tel)) = Sort' Term -> Term -> Type'' Term Term
forall t a. Sort' t -> a -> Type'' t a
I.El (Integer -> Sort' Term
I.mkType Integer
0 {- arbitrary -}) (Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> Term
I.Pi Dom (Type'' Term Term)
it (String -> Type'' Term Term -> Abs (Type'' Term Term)
forall a. String -> a -> Abs a
I.Abs String
v (Int -> Telescope -> Type'' Term Term
contyp (Int
npar Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Telescope
tel)))
           contyp Int
npar (I.ExtendTel Dom (Type'' Term Term)
it I.NoAbs{})     = Type'' Term Term
forall a. HasCallStack => a
__IMPOSSIBLE__
       MExp O
contyp' <- Type'' Term Term -> StateT S (TCMT IO) (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert (Type'' Term Term -> StateT S (TCMT IO) (MExp O))
-> Type'' Term Term -> StateT S (TCMT IO) (MExp O)
forall a b. (a -> b) -> a -> b
$ Int -> Telescope -> Type'' Term Term
contyp Int
0 Telescope
tel
       ConstDef O
cc <- TCM (ConstDef O) -> StateT S (TCMT IO) (ConstDef O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (ConstDef O) -> StateT S (TCMT IO) (ConstDef O))
-> TCM (ConstDef O) -> StateT S (TCMT IO) (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 (TCMT IO) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> StateT S (TCMT IO) ())
-> TCM () -> StateT S (TCMT IO) ()
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 <- (Dom QName -> StateT S (TCMT IO) (ConstRef O))
-> [Dom QName] -> StateT S (TCMT IO) [ConstRef O]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ Dom QName
dom -> Bool -> QName -> TMode -> StateT S (TCMT IO) (ConstRef O)
getConst Bool
False (Dom QName -> QName
forall t e. Dom' t e -> e
I.unDom Dom QName
dom) TMode
TMAll) [Dom QName]
fields
       -- Equivalently projfcns <- mapM (($ TMAll) . getConst False . I.unDom) fields

       (DeclCont O, [QName]) -> StateT S (TCMT IO) (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 (TCMT IO) (ConstRef O)
getConst Bool
False QName
dt TMode
TMAll -- make sure that datatype is included
       ConstDef O
cc <- TCM (ConstDef O) -> StateT S (TCMT IO) (ConstDef O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (ConstDef O) -> StateT S (TCMT IO) (ConstDef O))
-> TCM (ConstDef O) -> StateT S (TCMT IO) (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 (TCMT IO) (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 (TCMT IO) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM () -> StateT S (TCMT IO) ())
-> TCM () -> StateT S (TCMT IO) ()
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 (TCMT IO) ())
-> [((Bool, Term, Term), Int)] -> StateT S (TCMT IO) ()
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 (TCMT IO) () -> StateT S (TCMT IO) ()
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 (TCMT IO) () -> StateT S (TCMT IO) ())
-> StateT S (TCMT IO) () -> StateT S (TCMT IO) ()
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 (TCMT IO) (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 (TCMT IO) () -> StateT S (TCMT IO) ()
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 (TCMT IO) () -> StateT S (TCMT IO) ())
-> StateT S (TCMT IO) () -> StateT S (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ do
           (S -> S) -> StateT S (TCMT IO) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((S -> S) -> StateT S (TCMT IO) ())
-> (S -> S) -> StateT S (TCMT IO) ()
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 (TCMT IO) MetaVariable
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM MetaVariable -> StateT S (TCMT IO) MetaVariable)
-> TCM MetaVariable -> StateT S (TCMT IO) 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{} ->
                      TCM (Maybe Term) -> StateT S (TCMT IO) (Maybe Term)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (Maybe Term) -> StateT S (TCMT IO) (Maybe Term))
-> TCM (Maybe Term) -> StateT S (TCMT IO) (Maybe Term)
forall a b. (a -> b) -> a -> b
$ Closure Range -> TCM (Maybe Term) -> TCM (Maybe Term)
forall a. Closure Range -> TCM a -> TCM a
withMetaInfo (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mv) (TCM (Maybe Term) -> TCM (Maybe Term))
-> TCM (Maybe Term) -> TCM (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) -> [Arg Term] -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim
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 -> TCM (Maybe Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Term -> TCM (Maybe Term)) -> Maybe Term -> TCM (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 (TCMT IO) (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 (TCMT IO) ()
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 (TCMT IO) (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Term
sol
         (S -> S) -> StateT S (TCMT IO) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((S -> S) -> StateT S (TCMT IO) ())
-> (S -> S) -> StateT S (TCMT IO) ()
forall a b. (a -> b) -> a -> b
$ \S
s -> S
s {sEqs :: MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs = (Map Int (Maybe (Bool, MExp O, MExp O))
 -> Map Int (Maybe (Bool, MExp O, MExp O)))
-> MapS Int (Maybe (Bool, MExp O, MExp O))
-> MapS Int (Maybe (Bool, MExp O, MExp O))
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (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'))) (S -> MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs S
s)}
       let tt :: Type'' Term Term
tt = Judgement MetaId -> Type'' Term Term
forall a. Judgement a -> Type'' Term Term
MB.jMetaType (Judgement MetaId -> Type'' Term Term)
-> Judgement MetaId -> Type'' Term Term
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'' Term Term]
localVars = (Dom' Term (Name, Type'' Term Term) -> Type'' Term Term)
-> [Dom' Term (Name, Type'' Term Term)] -> [Type'' Term Term]
forall a b. (a -> b) -> [a] -> [b]
map ((Name, Type'' Term Term) -> Type'' Term Term
forall a b. (a, b) -> b
snd ((Name, Type'' Term Term) -> Type'' Term Term)
-> (Dom' Term (Name, Type'' Term Term) -> (Name, Type'' Term Term))
-> Dom' Term (Name, Type'' Term Term)
-> Type'' Term Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom' Term (Name, Type'' Term Term) -> (Name, Type'' Term Term)
forall t e. Dom' t e -> e
I.unDom) ([Dom' Term (Name, Type'' Term Term)] -> [Type'' Term Term])
-> (Closure Range -> [Dom' Term (Name, Type'' Term Term)])
-> Closure Range
-> [Type'' Term Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEnv -> [Dom' Term (Name, Type'' Term Term)]
envContext (TCEnv -> [Dom' Term (Name, Type'' Term Term)])
-> (Closure Range -> TCEnv)
-> Closure Range
-> [Dom' Term (Name, Type'' Term Term)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Closure Range -> TCEnv
forall a. Closure a -> TCEnv
clEnv (Closure Range -> [Type'' Term Term])
-> Closure Range -> [Type'' Term Term]
forall a b. (a -> b) -> a -> b
$ Closure Range
minfo
       (Type'' Term Term
targettype, [Type'' Term Term]
localVars) <- TCM (Type'' Term Term, [Type'' Term Term])
-> StateT S (TCMT IO) (Type'' Term Term, [Type'' Term Term])
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (Type'' Term Term, [Type'' Term Term])
 -> StateT S (TCMT IO) (Type'' Term Term, [Type'' Term Term]))
-> TCM (Type'' Term Term, [Type'' Term Term])
-> StateT S (TCMT IO) (Type'' Term Term, [Type'' Term Term])
forall a b. (a -> b) -> a -> b
$ Closure Range
-> TCM (Type'' Term Term, [Type'' Term Term])
-> TCM (Type'' Term Term, [Type'' Term Term])
forall a. Closure Range -> TCM a -> TCM a
withMetaInfo Closure Range
minfo (TCM (Type'' Term Term, [Type'' Term Term])
 -> TCM (Type'' Term Term, [Type'' Term Term]))
-> TCM (Type'' Term Term, [Type'' Term Term])
-> TCM (Type'' Term Term, [Type'' Term Term])
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'' Term Term
targettype <- Type'' Term Term
tt Type'' Term Term -> [Arg Term] -> TCM (Type'' Term Term)
forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type'' Term Term -> a -> m (Type'' Term Term)
`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'' Term Term
targettype <- Type'' Term Term -> TCM (Type'' Term Term)
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Type'' Term Term
targettype
        [Type'' Term Term]
localVars <- (Type'' Term Term -> TCM (Type'' Term Term))
-> [Type'' Term Term] -> TCMT IO [Type'' Term Term]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type'' Term Term -> TCM (Type'' Term Term)
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise [Type'' Term Term]
localVars
        (Type'' Term Term, [Type'' Term Term])
-> TCM (Type'' Term Term, [Type'' Term Term])
forall (m :: * -> *) a. Monad m => a -> m a
return (Type'' Term Term
targettype, [Type'' Term Term]
localVars)
       (S -> S) -> StateT S (TCMT IO) ()
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'' Term Term -> StateT S (TCMT IO) (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Type'' Term Term
targettype
       [MExp O]
ctx' <- (Type'' Term Term -> StateT S (TCMT IO) (MExp O))
-> [Type'' Term Term] -> StateT S (TCMT IO) [MExp O]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type'' Term Term -> StateT S (TCMT IO) (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert [Type'' Term Term]
localVars
       (S -> S) -> StateT S (TCMT IO) ()
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 (TCMT IO) ()
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 = (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]))
-> 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])
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (((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) (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 (TCMT IO) (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Term
e
         MExp O
i' <- Term -> StateT S (TCMT IO) (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Term
i
         (S -> S) -> StateT S (TCMT IO) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\S
s -> S
s {sEqs :: MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs = (Map Int (Maybe (Bool, MExp O, MExp O))
 -> Map Int (Maybe (Bool, MExp O, MExp O)))
-> MapS Int (Maybe (Bool, MExp O, MExp O))
-> MapS Int (Maybe (Bool, MExp O, MExp O))
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ((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) (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 (TCMT IO) ([ConstRef O], [MExp O])
-> S -> TCMT IO (([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 (TCMT IO) (ConstRef O))
-> [Hint] -> StateT S (TCMT IO) [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 (TCMT IO) (ConstRef O)
getConst Bool
iscon QName
name TMode
TMAll) [Hint]
icns
      [MExp O]
typs' <- (Type'' Term Term -> StateT S (TCMT IO) (MExp O))
-> [Type'' Term Term] -> StateT S (TCMT IO) [MExp O]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type'' Term Term -> StateT S (TCMT IO) (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert [Type'' Term Term]
typs
      [QName]
projfcns <- [QName] -> TOM [QName]
r []
      [ConstRef O]
projfcns' <- (QName -> StateT S (TCMT IO) (ConstRef O))
-> [QName] -> StateT S (TCMT IO) [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 (TCMT IO) (ConstRef O)
getConst Bool
False QName
name TMode
TMAll) [QName]
projfcns
      [] <- [QName] -> TOM [QName]
r []
      ([ConstRef O], [MExp O])
-> StateT S (TCMT IO) ([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 {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 {a}. Maybe a -> a
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 a -> a
fromJust (Just a
x) = a
x
 fromJust Maybe a
Nothing = a
forall a. HasCallStack => a
__IMPOSSIBLE__

getConst :: Bool -> AN.QName -> TMode -> TOM (ConstRef O)
getConst :: Bool -> QName -> TMode -> StateT S (TCMT IO) (ConstRef O)
getConst Bool
iscon QName
name TMode
mode = do
 Definition
def <- TCM Definition -> StateT S (TCMT IO) Definition
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Definition -> StateT S (TCMT IO) Definition)
-> TCM Definition -> StateT S (TCMT IO) 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 <- (S -> Map QName (TMode, ConstRef O))
-> StateT S (TCMT IO) (Map QName (TMode, ConstRef O))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (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))
-> (S -> MapS QName (TMode, ConstRef O))
-> S
-> Map QName (TMode, ConstRef O)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (TCMT IO) (ConstDef O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (ConstDef O) -> StateT S (TCMT IO) (ConstDef O))
-> TCM (ConstDef O) -> StateT S (TCMT IO) (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 (TCMT IO) (ConstRef O)
forall (m :: * -> *) a. Monad m => a -> m a
return ConstRef O
con
     else
      ConstRef O -> StateT S (TCMT IO) (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 (TCMT IO) MetaId
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets S -> MetaId
sMainMeta
     Int
dfv <- TCMT IO Int -> StateT S (TCMT IO) Int
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Int -> StateT S (TCMT IO) Int)
-> TCMT IO Int -> StateT S (TCMT IO) Int
forall a b. (a -> b) -> a -> b
$ MetaId -> QName -> TCMT IO Int
getdfv MetaId
mainm QName
name
     let nomi :: Int
nomi = Type'' Term Term -> Int
I.arity (Definition -> Type'' Term Term
MB.defType Definition
def)
     ConstRef O
ccon <- TCM (ConstRef O) -> StateT S (TCMT IO) (ConstRef O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (ConstRef O) -> StateT S (TCMT IO) (ConstRef O))
-> TCM (ConstRef O) -> StateT S (TCMT IO) (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 {cdname :: String
cdname = QName -> String
forall a. Pretty a => a -> String
prettyShow QName
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".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 (TCMT IO) (ConstRef O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (ConstRef O) -> StateT S (TCMT IO) (ConstRef O))
-> TCM (ConstRef O) -> StateT S (TCMT IO) (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 {cdname :: String
cdname = QName -> String
forall a. Pretty a => a -> String
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 (TCMT IO) ()
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 (TCMT IO) (ConstRef O)
forall (m :: * -> *) a. Monad m => a -> m a
return (ConstRef O -> StateT S (TCMT IO) (ConstRef O))
-> ConstRef O -> StateT S (TCMT IO) (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 <- (S -> Map QName (TMode, ConstRef O))
-> StateT S (TCMT IO) (Map QName (TMode, ConstRef O))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (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))
-> (S -> MapS QName (TMode, ConstRef O))
-> S
-> Map QName (TMode, ConstRef O)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (TCMT IO) (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, String
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]), String)
-> StateT S (TCMT IO) (Maybe (Int, [Arg QName]), String)
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 -> String
forall a. Pretty a => a -> String
prettyShow QName
dname String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"." String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Pretty a => a -> String
prettyShow (QName -> Name
I.qnameName QName
name))
      else
       (Maybe (Int, [Arg QName]), String)
-> StateT S (TCMT IO) (Maybe (Int, [Arg QName]), String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Int, [Arg QName])
forall a. Maybe a
Nothing, QName -> String
forall a. Pretty a => a -> String
prettyShow QName
name)
     MetaId
mainm <- (S -> MetaId) -> StateT S (TCMT IO) MetaId
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets S -> MetaId
sMainMeta
     Int
dfv <- TCMT IO Int -> StateT S (TCMT IO) Int
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Int -> StateT S (TCMT IO) Int)
-> TCMT IO Int -> StateT S (TCMT IO) 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 (TCMT IO) (ConstRef O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (ConstRef O) -> StateT S (TCMT IO) (ConstRef O))
-> TCM (ConstRef O) -> StateT S (TCMT IO) (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 {cdname :: String
cdname = String
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 (TCMT IO) ()
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 (TCMT IO) (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 <- (S
 -> Map
      MetaId
      (Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId]))
-> StateT
     S
     (TCMT IO)
     (Map
        MetaId
        (Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId]))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (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]))
-> (S
    -> MapS
         MetaId
         (Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId]))
-> S
-> Map
     MetaId
     (Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (TCMT IO) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((S -> S) -> StateT S (TCMT IO) ())
-> (S -> S) -> StateT S (TCMT IO) ()
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)
    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 :: forall a. TCM a
copatternsNotImplemented = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
MB.typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ String -> TypeError
MB.NotImplemented (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$
  String
"The Agda synthesizer (Agsy) does not support copatterns yet"

literalsNotImplemented :: MB.TCM a
literalsNotImplemented :: forall a. TCM a
literalsNotImplemented = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
MB.typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ String -> TypeError
MB.NotImplemented (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$
  String
"The Agda synthesizer (Agsy) does not support literals yet"

hitsNotImplemented :: MB.TCM a
hitsNotImplemented :: forall a. TCM a
hitsNotImplemented = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
MB.typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ String -> TypeError
MB.NotImplemented (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$
  String
"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 [Clause O]
convert = ([Maybe (Clause O)] -> [Clause O])
-> StateT S (TCMT IO) [Maybe (Clause O)] -> TOM [Clause O]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Maybe (Clause O)] -> [Clause O]
forall a. [Maybe a] -> [a]
catMaybes (StateT S (TCMT IO) [Maybe (Clause O)] -> TOM [Clause O])
-> ([Clause] -> StateT S (TCMT IO) [Maybe (Clause O)])
-> [Clause]
-> TOM [Clause O]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Clause -> StateT S (TCMT IO) (Maybe (Clause O)))
-> [Clause] -> StateT S (TCMT IO) [Maybe (Clause O)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Clause -> StateT S (TCMT IO) (Maybe (Clause 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 (TCMT IO) (Maybe (Clause 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' String) -> StateT S (TCMT IO) (Pat O))
-> [Arg (Pattern' String)] -> StateT S (TCMT IO) [Pat O]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Arg (Pattern' String) -> StateT S (TCMT IO) (Pat O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert ([Arg DeBruijnPattern] -> [Arg (Pattern' String)]
forall a b. LabelPatVars a b => b -> a
IP.unnumberPatVars [Arg DeBruijnPattern]
pats :: [Cm.Arg I.Pattern])
    Maybe (MExp O)
body' <- (Term -> StateT S (TCMT IO) (MExp O))
-> Maybe Term -> StateT S (TCMT IO) (Maybe (MExp O))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Term -> StateT S (TCMT IO) (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert (Maybe Term -> StateT S (TCMT IO) (Maybe (MExp O)))
-> StateT S (TCMT IO) (Maybe Term)
-> StateT S (TCMT IO) (Maybe (MExp O))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM (Maybe Term) -> StateT S (TCMT IO) (Maybe Term)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Maybe Term -> TCM (Maybe Term)
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Maybe Term
body)
    Maybe (Clause O) -> StateT S (TCMT IO) (Maybe (Clause O))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Clause O) -> StateT S (TCMT IO) (Maybe (Clause O)))
-> Maybe (Clause O) -> StateT S (TCMT IO) (Maybe (Clause O))
forall a b. (a -> b) -> a -> b
$ ([Pat O]
pats',) (MExp O -> Clause O) -> Maybe (MExp O) -> Maybe (Clause 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' String) -> StateT S (TCMT IO) (Pat O)
convert Arg (Pattern' String)
p = case Arg (Pattern' String) -> Pattern' String
forall e. Arg e -> e
Cm.unArg Arg (Pattern' String)
p of
    I.IApplyP PatternInfo
_ Term
_ Term
_ String
n  -> Pat O -> StateT S (TCMT IO) (Pat O)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pat O -> StateT S (TCMT IO) (Pat O))
-> Pat O -> StateT S (TCMT IO) (Pat O)
forall a b. (a -> b) -> a -> b
$ String -> Pat O
forall o. String -> Pat o
PatVar (String -> String
forall a. Pretty a => a -> String
prettyShow String
n)
    I.VarP PatternInfo
_ String
n  -> Pat O -> StateT S (TCMT IO) (Pat O)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pat O -> StateT S (TCMT IO) (Pat O))
-> Pat O -> StateT S (TCMT IO) (Pat O)
forall a b. (a -> b) -> a -> b
$ String -> Pat O
forall o. String -> Pat o
PatVar (String -> String
forall a. Pretty a => a -> String
prettyShow String
n)
    I.DotP PatternInfo
_ Term
_  -> Pat O -> StateT S (TCMT IO) (Pat O)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pat O -> StateT S (TCMT IO) (Pat O))
-> Pat O -> StateT S (TCMT IO) (Pat O)
forall a b. (a -> b) -> a -> b
$ String -> Pat O
forall o. String -> Pat o
PatVar String
"_"
      -- because Agda includes these when referring to variables in the body
    I.ConP ConHead
con ConPatternInfo
_ [NamedArg (Pattern' String)]
pats -> do
      let n :: QName
n = ConHead -> QName
I.conName ConHead
con
      ConstRef O
c     <- Bool -> QName -> TMode -> StateT S (TCMT IO) (ConstRef O)
getConst Bool
True QName
n TMode
TMAll
      [Pat O]
pats' <- (NamedArg (Pattern' String) -> StateT S (TCMT IO) (Pat O))
-> [NamedArg (Pattern' String)] -> StateT S (TCMT IO) [Pat O]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Arg (Pattern' String) -> StateT S (TCMT IO) (Pat O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert (Arg (Pattern' String) -> StateT S (TCMT IO) (Pat O))
-> (NamedArg (Pattern' String) -> Arg (Pattern' String))
-> NamedArg (Pattern' String)
-> StateT S (TCMT IO) (Pat O)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named NamedName (Pattern' String) -> Pattern' String)
-> NamedArg (Pattern' String) -> Arg (Pattern' String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Named NamedName (Pattern' String) -> Pattern' String
forall name a. Named name a -> a
Cm.namedThing) [NamedArg (Pattern' String)]
pats
      Definition
def   <- TCM Definition -> StateT S (TCMT IO) Definition
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Definition -> StateT S (TCMT IO) Definition)
-> TCM Definition -> StateT S (TCMT IO) 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 (TCMT IO) (ConstDef O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (ConstDef O) -> StateT S (TCMT IO) (ConstDef O))
-> TCM (ConstDef O) -> StateT S (TCMT IO) (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 (TCMT IO) (Pat O)
forall (m :: * -> *) a. Monad m => a -> m a
return (Pat O -> StateT S (TCMT IO) (Pat O))
-> Pat O -> StateT S (TCMT IO) (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{}   -> TCM (Pat O) -> StateT S (TCMT IO) (Pat O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCM (Pat O)
forall a. TCM a
copatternsNotImplemented
    I.LitP{}    -> TCM (Pat O) -> StateT S (TCMT IO) (Pat O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCM (Pat O)
forall a. TCM a
literalsNotImplemented
    I.DefP{}    -> TCM (Pat O) -> StateT S (TCMT IO) (Pat O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCM (Pat O)
forall a. TCM a
hitsNotImplemented

instance Conversion TOM I.Type (MExp O) where
  convert :: Type'' Term Term -> StateT S (TCMT IO) (MExp O)
convert (I.El Sort' Term
_ Term
t) = Term -> StateT S (TCMT IO) (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 (TCMT IO) (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 (TCMT IO) (MArgList O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert [Arg Term]
as
        MExp O -> StateT S (TCMT IO) (MExp O)
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp O -> StateT S (TCMT IO) (MExp O))
-> MExp O -> StateT S (TCMT IO) (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 (TCMT IO) (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert (Abs Term -> Term
forall a. Subst a => Abs a -> a
I.absBody Abs Term
b)
        MExp O -> StateT S (TCMT IO) (MExp O)
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp O -> StateT S (TCMT IO) (MExp O))
-> MExp O -> StateT S (TCMT IO) (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 (String -> MId
Id (String -> MId) -> String -> MId
forall a b. (a -> b) -> a -> b
$ Abs Term -> String
forall a. Abs a -> String
I.absName Abs Term
b) MExp O
b')
      t :: Term
t@I.Lit{} -> do
        Term
t <- TCMT IO Term -> StateT S (TCMT IO) Term
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Term -> StateT S (TCMT IO) Term)
-> TCMT IO Term -> StateT S (TCMT IO) Term
forall a b. (a -> b) -> a -> b
$ Term -> TCMT IO Term
forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm Term
t
        case Term
t of
          I.Lit{} -> TCM (MExp O) -> StateT S (TCMT IO) (MExp O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift TCM (MExp O)
forall a. TCM a
literalsNotImplemented
          Term
_       -> Term -> StateT S (TCMT IO) (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Term
t
      I.Level Level
l -> Term -> StateT S (TCMT IO) (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert (Term -> StateT S (TCMT IO) (MExp O))
-> StateT S (TCMT IO) Term -> StateT S (TCMT IO) (MExp O)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO Term -> StateT S (TCMT IO) 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 (TCMT IO) (ConstRef O)
getConst Bool
False QName
name TMode
TMAll
        MArgList O
as' <- [Arg Term] -> StateT S (TCMT IO) (MArgList O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert [Arg Term]
as
        MExp O -> StateT S (TCMT IO) (MExp O)
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp O -> StateT S (TCMT IO) (MExp O))
-> MExp O -> StateT S (TCMT IO) (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 (TCMT IO) (ConstRef O)
getConst Bool
True QName
name TMode
TMAll
        MArgList O
as' <- [Arg Term] -> StateT S (TCMT IO) (MArgList O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert [Arg Term]
as
        Definition
def <- TCM Definition -> StateT S (TCMT IO) Definition
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM Definition -> StateT S (TCMT IO) Definition)
-> TCM Definition -> StateT S (TCMT IO) 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 (TCMT IO) (ConstDef O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCM (ConstDef O) -> StateT S (TCMT IO) (ConstDef O))
-> TCM (ConstDef O) -> StateT S (TCMT IO) (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 (TCMT IO) (MExp O)
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp O -> StateT S (TCMT IO) (MExp O))
-> MExp O -> StateT S (TCMT IO) (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'' Term Term
x}) Abs (Type'' Term Term)
b -> do
        let y :: Type'' Term Term
y    = Abs (Type'' Term Term) -> Type'' Term Term
forall a. Subst a => Abs a -> a
I.absBody Abs (Type'' Term Term)
b
            name :: String
name = Abs (Type'' Term Term) -> String
forall a. Abs a -> String
I.absName Abs (Type'' Term Term)
b
        MExp O
x' <- Type'' Term Term -> StateT S (TCMT IO) (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Type'' Term Term
x
        MExp O
y' <- Type'' Term Term -> StateT S (TCMT IO) (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Type'' Term Term
y
        MExp O -> StateT S (TCMT IO) (MExp O)
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp O -> StateT S (TCMT IO) (MExp O))
-> MExp O -> StateT S (TCMT IO) (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'' Term Term -> Bool
forall a. Free a => Int -> a -> Bool
Free.freeIn Int
0 Type'' Term Term
y) MExp O
x' (MId -> MExp O -> Abs (MExp O)
forall a. MId -> a -> Abs a
Abs (String -> MId
Id String
name) MExp O
y')
      I.Sort (I.Type (I.ClosedLevel Integer
l)) -> MExp O -> StateT S (TCMT IO) (MExp O)
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp O -> StateT S (TCMT IO) (MExp O))
-> MExp O -> StateT S (TCMT IO) (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 (TCMT IO) (MExp O)
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp O -> StateT S (TCMT IO) (MExp O))
-> MExp O -> StateT S (TCMT IO) (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 (TCMT IO) (MExp O)
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp O -> StateT S (TCMT IO) (MExp O))
-> MExp O -> StateT S (TCMT IO) (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 (TCMT IO) Term
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TCMT IO Term -> StateT S (TCMT IO) Term)
-> TCMT IO Term -> StateT S (TCMT IO) 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 (TCMT IO) ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
              Just MetaId
curmeta ->
                (S -> S) -> StateT S (TCMT IO) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((S -> S) -> StateT S (TCMT IO) ())
-> (S -> S) -> StateT S (TCMT IO) ()
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 = (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]))
-> 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])
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (((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) (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 (TCMT IO) (MExp O)
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp O -> StateT S (TCMT IO) (MExp O))
-> MExp O -> StateT S (TCMT IO) (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 (TCMT IO) (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Term
t
      I.DontCare Term
_ -> MExp O -> StateT S (TCMT IO) (MExp O)
forall (m :: * -> *) a. Monad m => a -> m a
return (MExp O -> StateT S (TCMT IO) (MExp O))
-> MExp O -> StateT S (TCMT IO) (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 (TCMT IO) b -> TOM (Hiding, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> StateT S (TCMT IO) 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 (TCMT IO) (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 (TCMT IO) [(Hiding, MExp O)]
-> StateT S (TCMT IO) (MArgList O)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Arg Term -> StateT S (TCMT IO) (Hiding, MExp O))
-> [Arg Term] -> StateT S (TCMT IO) [(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 (TCMT IO) (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'' Term Term -> 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]
forall t. [Elim' t] -> [Arg t]
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]
forall t. [Elim' t] -> [Arg t]
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]
forall t. [Elim' t] -> [Arg t]
I.argsFromElims Elims
as
fmExp MetaId
m (I.Pi Dom (Type'' Term Term)
x Abs (Type'' Term Term)
y)  = MetaId -> Type'' Term Term -> Bool
fmType MetaId
m (Dom (Type'' Term Term) -> Type'' Term Term
forall t e. Dom' t e -> e
I.unDom Dom (Type'' Term Term)
x) Bool -> Bool -> Bool
|| MetaId -> Type'' Term Term -> Bool
fmType MetaId
m (Abs (Type'' Term Term) -> Type'' Term Term
forall a. Abs a -> a
I.unAbs Abs (Type'' Term Term)
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 [Arg Term]
as = (Arg Term -> Bool) -> [Arg Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (MetaId -> Term -> Bool
fmExp MetaId
m (Term -> Bool) -> (Arg Term -> Term) -> Arg Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Arg Term -> Term
forall e. Arg e -> e
Cm.unArg) [Arg Term]
as

fmLevel :: I.MetaId -> I.PlusLevel -> Bool
fmLevel :: MetaId -> PlusLevel' Term -> Bool
fmLevel MetaId
m (I.Plus Integer
_ Term
l) = MetaId -> Term -> Bool
fmExp MetaId
m Term
l

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

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 String IO (Maybe a)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Maybe a) -> ExceptT String IO (Maybe a))
-> IO (Maybe a) -> ExceptT String 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 -> String -> MOT b
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"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) = String -> b -> Abs b
forall a. String -> a -> Abs a
I.Abs String
id (b -> Abs b) -> ExceptT String IO b -> MOT (Abs b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> ExceptT String IO b
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert a
t where
    id :: String
id = case MId
mid of
           MId
NoId  -> String
"x"
           Id String
id -> String
id

instance Conversion MOT (Exp O) I.Type where
  convert :: Exp O -> MOT (Type'' Term Term)
convert Exp O
e = Sort' Term -> Term -> Type'' Term Term
forall t a. Sort' t -> a -> Type'' t a
I.El (Integer -> Sort' Term
I.mkType Integer
0) (Term -> Type'' Term Term)
-> ExceptT String IO Term -> MOT (Type'' Term Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Exp O -> ExceptT String 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 String IO Term
convert = \case
    App Maybe (Metavar (Exp O) (RefInfo O))
_ OKHandle (RefInfo O)
_ (Var Int
v) MArgList O
as -> Int -> MArgList O -> Term -> ExceptT String 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 String IO (ConstDef O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (ConstDef O) -> ExceptT String IO (ConstDef O))
-> IO (ConstDef O) -> ExceptT String 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 -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
I.ConHead QName
q DataOrRecord
I.IsData 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 String 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 String IO (Abs Term) -> ExceptT String IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs (MExp O) -> ExceptT String 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'' Term Term
x' <- MExp O -> MOT (Type'' Term Term)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert MExp O
x
      let dom :: Dom (Type'' Term Term)
dom = (Type'' Term Term -> Dom (Type'' Term Term)
forall a. a -> Dom a
I.defaultDom Type'' Term Term
x') {domInfo :: ArgInfo
domInfo = Hiding -> ArgInfo
icnvh Hiding
hid}
      Dom (Type'' Term Term) -> Abs (Type'' Term Term) -> Term
I.Pi Dom (Type'' Term Term)
dom (Abs (Type'' Term Term) -> Term)
-> ExceptT String IO (Abs (Type'' Term Term))
-> ExceptT String IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Abs (MExp O) -> ExceptT String IO (Abs (Type'' Term Term))
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 String IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> ExceptT String IO Term) -> Term -> ExceptT String 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 String IO Term
forall a. HasCallStack => a
__IMPOSSIBLE__
    Sort Sort
UnknownSort -> Term -> ExceptT String IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> ExceptT String IO Term) -> Term -> ExceptT String 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 String IO Term
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> ExceptT String IO Term) -> Term -> ExceptT String 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
$ String -> Term -> Abs Term
forall a. String -> a -> Abs a
I.Abs String
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 String IO Term
frommyExps Int
ndrop (Meta Metavar (ArgList O) (RefInfo O)
m) Term
trm = do
 Maybe (ArgList O)
bind <- IO (Maybe (ArgList O)) -> ExceptT String IO (Maybe (ArgList O))
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (Maybe (ArgList O)) -> ExceptT String IO (Maybe (ArgList O)))
-> IO (Maybe (ArgList O)) -> ExceptT String 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 -> String -> ExceptT String IO Term
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"meta not bound"
  Just ArgList O
e -> Int -> MArgList O -> Term -> ExceptT String 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 String 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 String 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 String IO Term
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert MExp O
x
   Int -> MArgList O -> Term -> ExceptT String 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 String 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 String IO (MM (ConstRef O) (RefInfo O)))
-> IO (MM (ConstRef O) (RefInfo O))
-> ExceptT String 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 String IO (ConstRef O)
forall (m :: * -> *) a. Monad m => a -> m a
return ConstRef O
c
            Meta{} -> String -> ExceptT String IO (ConstRef O)
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"meta not bound"
   ConstDef O
cdef <- IO (ConstDef O) -> ExceptT String IO (ConstDef O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (ConstDef O) -> ExceptT String IO (ConstDef O))
-> IO (ConstDef O) -> ExceptT String 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 String IO Term
frommyExps Int
0 MArgList O
eas (QName -> Elims -> Term
I.Def QName
name [])
   Int -> MArgList O -> Term -> ExceptT String 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 String 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 String 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
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
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
forall a. Arg a -> Elim' a
I.Apply Arg Term
x])
  addend Arg Term
_ Term
_ = Term
forall a. HasCallStack => a
__IMPOSSIBLE__

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

abslamvarname :: String
abslamvarname :: String
abslamvarname = String
"\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 -> String
forall a. Pretty a => a -> String
prettyShow (Name -> Name
A.nameConcrete Name
n) String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
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' String)] -> 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' String)
p : [NamedArg (Pattern' String)]
ps) = do
      ([(Hiding, MId)]
ns', [CSPat O]
ps') <- [(Hiding, MId)]
-> [NamedArg (Pattern' String)] -> TCM ([(Hiding, MId)], [CSPat O])
cnvps [(Hiding, MId)]
ns [NamedArg (Pattern' String)]
ps
      ([(Hiding, MId)]
ns'', CSPat O
p') <- [(Hiding, MId)]
-> NamedArg (Pattern' String) -> TCM ([(Hiding, MId)], CSPat O)
cnvp [(Hiding, MId)]
ns' NamedArg (Pattern' String)
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' String) -> TCM ([(Hiding, MId)], CSPat O)
cnvp [(Hiding, MId)]
ns NamedArg (Pattern' String)
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' String) -> ArgInfo
forall e. Arg e -> ArgInfo
Cm.argInfo NamedArg (Pattern' String)
p
      in case NamedArg (Pattern' String) -> Pattern' String
forall a. NamedArg a -> a
Cm.namedArg NamedArg (Pattern' String)
p of
       I.VarP PatternInfo
_ String
n -> ([(Hiding, MId)], CSPat O) -> TCM ([(Hiding, MId)], CSPat O)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Hiding
hid, String -> MId
Id String
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
_ String
n -> ([(Hiding, MId)], CSPat O) -> TCM ([(Hiding, MId)], CSPat O)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Hiding
hid, String -> MId
Id String
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' String)]
ps -> do
        let c :: QName
c = ConHead -> QName
I.conName ConHead
con
        (ConstRef O
c2, S
_) <- StateT S (TCMT IO) (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 (TCMT IO) (ConstRef O)
getConst Bool
True QName
c TMode
TMAll) (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' String)] -> TCM ([(Hiding, MId)], [CSPat O])
cnvps [(Hiding, MId)]
ns [NamedArg (Pattern' String)]
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 (TCMT IO) (MExp O) -> S -> TCM (MExp O, S)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (Term -> StateT S (TCMT IO) (MExp O)
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Term
t) (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' String)] -> TCM ([(Hiding, MId)], [CSPat O])
cnvps [] (NAPs -> [NamedArg (Pattern' String)]
forall a b. LabelPatVars a b => b -> a
IP.unnumberPatVars (NAPs -> [NamedArg (Pattern' String)])
-> NAPs -> [NamedArg (Pattern' String)]
forall a b. (a -> b) -> a -> b
$ Clause -> NAPs
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 String IO Clause
frommyClause (CSCtx O
ids, [CSPat O]
pats, Maybe (MExp O)
mrhs) = do
 let ctel :: [HI (MId, a)] -> m (Tele (Dom' Term e))
ctel [] = Tele (Dom' Term e) -> m (Tele (Dom' Term e))
forall (m :: * -> *) a. Monad m => a -> m a
return Tele (Dom' Term e)
forall a. Tele a
I.EmptyTel
     ctel (HI Hiding
hid (MId
mid, a
t) : [HI (MId, a)]
ctx) = do
      let Id String
id = MId
mid
      Tele (Dom' Term e)
tel <- [HI (MId, a)] -> m (Tele (Dom' Term e))
ctel [HI (MId, a)]
ctx
      e
t' <- a -> m e
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert a
t
      let dom :: Dom' Term e
dom = (e -> Dom' Term e
forall a. a -> Dom a
I.defaultDom e
t') {domInfo :: ArgInfo
domInfo = Hiding -> ArgInfo
icnvh Hiding
hid}
      Tele (Dom' Term e) -> m (Tele (Dom' Term e))
forall (m :: * -> *) a. Monad m => a -> m a
return (Tele (Dom' Term e) -> m (Tele (Dom' Term e)))
-> Tele (Dom' Term e) -> m (Tele (Dom' Term e))
forall a b. (a -> b) -> a -> b
$ Dom' Term e -> Abs (Tele (Dom' Term e)) -> Tele (Dom' Term e)
forall a. a -> Abs (Tele a) -> Tele a
I.ExtendTel Dom' Term e
dom (String -> Tele (Dom' Term e) -> Abs (Tele (Dom' Term e))
forall a. String -> a -> Abs a
I.Abs String
id Tele (Dom' Term e)
tel)
 Telescope
tel <- CSCtx O -> ExceptT String IO Telescope
forall {m :: * -> *} {a} {e}.
(Monad m, Conversion m a e) =>
[HI (MId, a)] -> m (Tele (Dom' Term e))
ctel (CSCtx O -> ExceptT String IO Telescope)
-> CSCtx O -> ExceptT String IO Telescope
forall a b. (a -> b) -> a -> b
$ CSCtx O -> CSCtx O
forall a. [a] -> [a]
reverse CSCtx O
ids
 let getperms :: Int
-> [CSPat O]
-> [(Int, Int)]
-> Int
-> ExceptT String IO ([(Int, Int)], Int)
getperms Int
0 [] [(Int, Int)]
perm Int
nv = ([(Int, Int)], Int) -> ExceptT String IO ([(Int, Int)], Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Int, Int)]
perm, Int
nv)
     getperms Int
n [] [(Int, Int)]
_ Int
_ = ExceptT String IO ([(Int, Int)], Int)
forall a. HasCallStack => a
__IMPOSSIBLE__
     getperms Int
0 (CSPat O
p : [CSPat O]
ps) [(Int, Int)]
perm Int
nv = do
      ([(Int, Int)]
perm, Int
nv) <- CSPat O
-> [(Int, Int)] -> Int -> ExceptT String IO ([(Int, Int)], Int)
getperm CSPat O
p [(Int, Int)]
perm Int
nv
      Int
-> [CSPat O]
-> [(Int, Int)]
-> Int
-> ExceptT String IO ([(Int, Int)], Int)
getperms Int
0 [CSPat O]
ps [(Int, Int)]
perm Int
nv
     getperms Int
n (HI Hiding
_ CSPatExp{} : [CSPat O]
ps) [(Int, Int)]
perm Int
nv = Int
-> [CSPat O]
-> [(Int, Int)]
-> Int
-> ExceptT String IO ([(Int, Int)], Int)
getperms (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [CSPat O]
ps [(Int, Int)]
perm Int
nv
     getperms Int
n (HI Hiding
_ CSOmittedArg{} : [CSPat O]
ps) [(Int, Int)]
perm Int
nv = Int
-> [CSPat O]
-> [(Int, Int)]
-> Int
-> ExceptT String IO ([(Int, Int)], Int)
getperms (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [CSPat O]
ps [(Int, Int)]
perm Int
nv
     getperms Int
n (CSPat O
_ : [CSPat O]
_) [(Int, Int)]
_ Int
_ = ExceptT String IO ([(Int, Int)], Int)
forall a. HasCallStack => a
__IMPOSSIBLE__
     getperm :: CSPat O
-> [(Int, Int)] -> Int -> ExceptT String IO ([(Int, Int)], Int)
getperm (HI Hiding
_ CSPatI O
p) [(Int, Int)]
perm Int
nv =
      case CSPatI O
p of
       --CSPatVar v -> return (length ids + nv - 1 - v : perm, nv)
       CSPatVar Int
v -> ([(Int, Int)], Int) -> ExceptT String IO ([(Int, Int)], Int)
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, Int
nv) (Int, Int) -> [(Int, Int)] -> [(Int, Int)]
forall a. a -> [a] -> [a]
: [(Int, Int)]
perm, Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
       CSPatConApp ConstRef O
c [CSPat O]
ps -> do
        ConstDef O
cdef <- IO (ConstDef O) -> ExceptT String IO (ConstDef O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (ConstDef O) -> ExceptT String IO (ConstDef O))
-> IO (ConstDef O) -> ExceptT String 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 (Just (Int
ndrop,[Arg QName]
_), QName
_) = ConstDef O -> O
forall o. ConstDef o -> o
cdorigin ConstDef O
cdef
        Int
-> [CSPat O]
-> [(Int, Int)]
-> Int
-> ExceptT String IO ([(Int, Int)], Int)
getperms Int
ndrop [CSPat O]
ps [(Int, Int)]
perm Int
nv
       CSPatExp MExp O
e -> ([(Int, Int)], Int) -> ExceptT String IO ([(Int, Int)], Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Int, Int)]
perm, Int
nv Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
       CSPatI O
_ -> ExceptT String IO ([(Int, Int)], Int)
forall a. HasCallStack => a
__IMPOSSIBLE__
 ([(Int, Int)]
rperm, Int
nv) <- Int
-> [CSPat O]
-> [(Int, Int)]
-> Int
-> ExceptT String IO ([(Int, Int)], Int)
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 :: Int -> [CSPat O] -> ExceptT String IO [NamedArg (Pattern' String)]
cnvps Int
0 [] = [NamedArg (Pattern' String)]
-> ExceptT String IO [NamedArg (Pattern' String)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
     cnvps Int
n [] = ExceptT String IO [NamedArg (Pattern' String)]
forall a. HasCallStack => a
__IMPOSSIBLE__
     cnvps Int
0 (CSPat O
p : [CSPat O]
ps) = do
      NamedArg (Pattern' String)
p' <- CSPat O -> ExceptT String IO (NamedArg (Pattern' String))
cnvp CSPat O
p
      [NamedArg (Pattern' String)]
ps' <- Int -> [CSPat O] -> ExceptT String IO [NamedArg (Pattern' String)]
cnvps Int
0 [CSPat O]
ps
      [NamedArg (Pattern' String)]
-> ExceptT String IO [NamedArg (Pattern' String)]
forall (m :: * -> *) a. Monad m => a -> m a
return (NamedArg (Pattern' String)
p' NamedArg (Pattern' String)
-> [NamedArg (Pattern' String)] -> [NamedArg (Pattern' String)]
forall a. a -> [a] -> [a]
: [NamedArg (Pattern' String)]
ps')
     cnvps Int
n (HI Hiding
_ CSPatExp{} : [CSPat O]
ps) = Int -> [CSPat O] -> ExceptT String IO [NamedArg (Pattern' String)]
cnvps (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [CSPat O]
ps
     cnvps Int
n (HI Hiding
_ CSOmittedArg{} : [CSPat O]
ps) = Int -> [CSPat O] -> ExceptT String IO [NamedArg (Pattern' String)]
cnvps (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [CSPat O]
ps
     cnvps Int
n (CSPat O
_ : [CSPat O]
_) = ExceptT String IO [NamedArg (Pattern' String)]
forall a. HasCallStack => a
__IMPOSSIBLE__
     cnvp :: CSPat O -> ExceptT String IO (NamedArg (Pattern' String))
cnvp (HI Hiding
hid CSPatI O
p) = do
      Pattern' String
p' <- case CSPatI O
p of
       CSPatVar Int
v -> Pattern' String -> ExceptT String IO (Pattern' String)
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Pattern' String
forall a. a -> Pattern' a
I.varP (String -> Pattern' String) -> String -> Pattern' String
forall a b. (a -> b) -> a -> b
$ let HI Hiding
_ (Id String
n, MExp O
_) = CSCtx O
ids CSCtx O -> Int -> HI (MId, MExp O)
forall a. [a] -> Int -> a
!! Int
v in String
n)
       CSPatConApp ConstRef O
c [CSPat O]
ps -> do
        ConstDef O
cdef <- IO (ConstDef O) -> ExceptT String IO (ConstDef O)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (ConstDef O) -> ExceptT String IO (ConstDef O))
-> IO (ConstDef O) -> ExceptT String 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 (Just (Int
ndrop,[Arg QName]
_), QName
name) = ConstDef O -> O
forall o. ConstDef o -> o
cdorigin ConstDef O
cdef
        [NamedArg (Pattern' String)]
ps' <- Int -> [CSPat O] -> ExceptT String IO [NamedArg (Pattern' String)]
cnvps Int
ndrop [CSPat O]
ps
        let con :: ConHead
con = QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
I.ConHead QName
name DataOrRecord
I.IsData Induction
Cm.Inductive [] -- TODO: restore DataOrRecord and record fields!
        Pattern' String -> ExceptT String IO (Pattern' String)
forall (m :: * -> *) a. Monad m => a -> m a
return (ConHead
-> ConPatternInfo
-> [NamedArg (Pattern' String)]
-> Pattern' String
forall x.
ConHead -> ConPatternInfo -> [NamedArg (Pattern' x)] -> Pattern' x
I.ConP ConHead
con ConPatternInfo
I.noConPatternInfo [NamedArg (Pattern' String)]
ps')
       CSPatExp MExp O
e -> do
        Term
e' <- MExp O -> ExceptT String IO Term
forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert MExp O
e {- renm e -} -- renaming before adding to clause below
        Pattern' String -> ExceptT String IO (Pattern' String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> Pattern' String
forall a. Term -> Pattern' a
I.dotP Term
e')
       CSPatI O
CSAbsurd -> ExceptT String IO (Pattern' String)
forall a. HasCallStack => a
__IMPOSSIBLE__ -- CSAbsurd not used
       CSPatI O
_ -> ExceptT String IO (Pattern' String)
forall a. HasCallStack => a
__IMPOSSIBLE__
      NamedArg (Pattern' String)
-> ExceptT String IO (NamedArg (Pattern' String))
forall (m :: * -> *) a. Monad m => a -> m a
return (NamedArg (Pattern' String)
 -> ExceptT String IO (NamedArg (Pattern' String)))
-> NamedArg (Pattern' String)
-> ExceptT String IO (NamedArg (Pattern' String))
forall a b. (a -> b) -> a -> b
$ ArgInfo
-> Named NamedName (Pattern' String) -> NamedArg (Pattern' String)
forall e. ArgInfo -> e -> Arg e
Cm.Arg (Hiding -> ArgInfo
icnvh Hiding
hid) (Named NamedName (Pattern' String) -> NamedArg (Pattern' String))
-> Named NamedName (Pattern' String) -> NamedArg (Pattern' String)
forall a b. (a -> b) -> a -> b
$ Pattern' String -> Named NamedName (Pattern' String)
forall a name. a -> Named name a
Cm.unnamed Pattern' String
p'   -- TODO: recover names
 [NamedArg (Pattern' String)]
ps <- Int -> [CSPat O] -> ExceptT String IO [NamedArg (Pattern' String)]
cnvps Int
0 [CSPat O]
pats
 Maybe Term
body <- case Maybe (MExp O)
mrhs of
          Maybe (MExp O)
Nothing -> Maybe Term -> ExceptT String IO (Maybe Term)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Term -> ExceptT String IO (Maybe Term))
-> Maybe Term -> ExceptT String 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 String IO Term -> ExceptT String IO (Maybe Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MExp O -> ExceptT String 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 String IO Clause
forall (m :: * -> *) a. Monad m => a -> m a
return (Clause -> ExceptT String IO Clause)
-> Clause -> ExceptT String IO Clause
forall a b. (a -> b) -> a -> b
$ 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 :: NAPs
I.namedClausePats = Int -> Permutation -> [NamedArg (Pattern' String)] -> NAPs
forall a b.
(LabelPatVars a b, PatVarLabel b ~ Int) =>
Int -> Permutation -> a -> b
IP.numberPatVars Int
forall a. HasCallStack => a
__IMPOSSIBLE__ Permutation
cperm ([NamedArg (Pattern' String)] -> NAPs)
-> [NamedArg (Pattern' String)] -> NAPs
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg [NamedArg (Pattern' String)])
-> [NamedArg (Pattern' String)] -> [NamedArg (Pattern' String)]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Permutation
-> Substitution' (SubstArg [NamedArg (Pattern' String)])
forall a. DeBruijn a => Permutation -> Substitution' a
renamingR (Permutation
 -> Substitution' (SubstArg [NamedArg (Pattern' String)]))
-> Permutation
-> Substitution' (SubstArg [NamedArg (Pattern' String)])
forall a b. (a -> b) -> a -> b
$ Permutation -> Permutation
compactP Permutation
cperm) [NamedArg (Pattern' String)]
ps
   , clauseBody :: Maybe Term
I.clauseBody  = Maybe Term
body
   , clauseType :: Maybe (Arg (Type'' Term Term))
I.clauseType  = Maybe (Arg (Type'' Term Term))
forall a. Maybe a
Nothing -- TODO: compute clause type
   , clauseCatchall :: Bool
I.clauseCatchall = Bool
False
   , clauseExact :: Maybe Bool
I.clauseExact       = Maybe Bool
forall a. Maybe a
Nothing -- TODO
   , 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 :: forall o. 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 :: forall o. ConstRef o -> MExp o -> MExp o
negtype ConstRef o
ee = Int -> 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 :: Int -> MExp o -> MExp o
f Int
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 (Int -> MExp o -> MExp o
f (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
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'' Term Term
_ Maybe Substitution
_ 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'' Term Term -> Type'' Term Term -> Maybe (Int, Int)
matchType Int
cdfv Int
tctx Type'' Term Term
ctyp Type'' Term Term
ttyp = Int -> Type'' Term Term -> Maybe (Int, Int)
trmodps Int
cdfv Type'' Term Term
ctyp
 where
  trmodps :: Int -> Type'' Term Term -> Maybe (Int, Int)
trmodps Int
0 Type'' Term Term
ctyp = Int -> Int -> Type'' Term Term -> Maybe (Int, Int)
tr Int
0 Int
0 Type'' Term Term
ctyp
  trmodps Int
n Type'' Term Term
ctyp = case Type'' Term Term -> Term
forall t a. Type'' t a -> a
I.unEl Type'' Term Term
ctyp of
   I.Pi Dom (Type'' Term Term)
_ Abs (Type'' Term Term)
ot -> Int -> Type'' Term Term -> Maybe (Int, Int)
trmodps (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Abs (Type'' Term Term) -> Type'' Term Term
forall a. Subst a => Abs a -> a
I.absBody Abs (Type'' Term Term)
ot)
   Term
_ -> Maybe (Int, Int)
forall a. HasCallStack => a
__IMPOSSIBLE__
  tr :: Int -> Int -> Type'' Term Term -> Maybe (Int, Int)
tr Int
narg Int
na Type'' Term Term
ctyp =
   case Int
-> Int
-> (Int -> Maybe Int)
-> Type'' Term Term
-> Type'' Term Term
-> Maybe Int
ft Int
0 Int
0 Int -> Maybe Int
forall a. a -> Maybe a
Just Type'' Term Term
ctyp Type'' Term Term
ttyp of
    Just Int
n -> (Int, Int) -> Maybe (Int, Int)
forall a. a -> Maybe a
Just (Int
n, Int
narg)
    Maybe Int
Nothing -> case Type'' Term Term -> Term
forall t a. Type'' t a -> a
I.unEl Type'' Term Term
ctyp of
     I.Pi Dom (Type'' Term Term)
_ (I.Abs String
_ Type'' Term Term
ot) -> Int -> Int -> Type'' Term Term -> Maybe (Int, Int)
tr (Int
narg Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int
na Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Type'' Term Term
ot
     I.Pi Dom (Type'' Term Term)
_ (I.NoAbs String
_ Type'' Term Term
ot) -> Int -> Int -> Type'' Term Term -> Maybe (Int, Int)
tr (Int
narg Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
na Type'' Term Term
ot
     Term
_ -> Maybe (Int, Int)
forall a. Maybe a
Nothing
   where
    ft :: Int
-> Int
-> (Int -> Maybe Int)
-> Type'' Term Term
-> Type'' Term Term
-> Maybe Int
ft Int
nl Int
n Int -> Maybe Int
c (I.El Sort' Term
_ Term
e1) (I.El Sort' Term
_ Term
e2) = Int -> Int -> (Int -> Maybe Int) -> Term -> Term -> Maybe Int
f Int
nl Int
n Int -> Maybe Int
c Term
e1 Term
e2
    f :: Int -> Int -> (Int -> Maybe Int) -> Term -> Term -> Maybe Int
f Int
nl Int
n Int -> Maybe Int
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 -> Int -> (Int -> Maybe Int) -> Elims -> Elims -> Maybe Int
fes Int
nl (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int -> Maybe Int
c Elims
as1 Elims
as2
      Term
_ -> Maybe Int
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 -> Int -> Maybe Int
c Int
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 -> Int -> (Int -> Maybe Int) -> Elims -> Elims -> Maybe Int
fes Int
nl (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int -> Maybe Int
c Elims
as1 Elims
as2
      Term
_ -> Maybe Int
forall a. Maybe a
Nothing
     Term
_ -> case (Term
e1, Term
e2) of
      (I.MetaV{}, Term
_) -> Int -> Maybe Int
c Int
n
      (Term
_, I.MetaV{}) -> Int -> Maybe Int
c Int
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 -> Int -> (Int -> Maybe Int) -> Term -> Term -> Maybe Int
f (Int
nl Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
n Int -> Maybe Int
c (Abs Term -> Term
forall a. Subst a => Abs a -> a
I.absBody Abs Term
b1) (Abs Term -> Term
forall a. Subst 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 -> Int -> Maybe Int
c (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
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 -> Int -> (Int -> Maybe Int) -> Elims -> Elims -> Maybe Int
fes Int
nl (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int -> Maybe Int
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 -> Int -> (Int -> Maybe Int) -> Elims -> Elims -> Maybe Int
fs Int
nl (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int -> Maybe Int
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'' Term Term
it1})  Abs (Type'' Term Term)
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'' Term Term
it2})  Abs (Type'' Term Term)
ot2) | ArgInfo -> Hiding
Cm.argInfoHiding ArgInfo
info1 Hiding -> Hiding -> Bool
forall a. Eq a => a -> a -> Bool
== ArgInfo -> Hiding
Cm.argInfoHiding ArgInfo
info2 -> Int
-> Int
-> (Int -> Maybe Int)
-> Type'' Term Term
-> Type'' Term Term
-> Maybe Int
ft Int
nl Int
n (\Int
n -> Int
-> Int
-> (Int -> Maybe Int)
-> Type'' Term Term
-> Type'' Term Term
-> Maybe Int
ft (Int
nl Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
n Int -> Maybe Int
c (Abs (Type'' Term Term) -> Type'' Term Term
forall a. Subst a => Abs a -> a
I.absBody Abs (Type'' Term Term)
ot1) (Abs (Type'' Term Term) -> Type'' Term Term
forall a. Subst a => Abs a -> a
I.absBody Abs (Type'' Term Term)
ot2)) Type'' Term Term
it1 Type'' Term Term
it2
      (I.Sort{}, I.Sort{}) -> Int -> Maybe Int
c Int
n -- sloppy
      (Term, Term)
_ -> Maybe Int
forall a. Maybe a
Nothing
    fs :: Int -> Int -> (Int -> Maybe Int) -> Elims -> Elims -> Maybe Int
fs Int
nl Int
n Int -> Maybe Int
c Elims
es1 Elims
es2 = case (Elims
es1, Elims
es2) of
     ([], []) -> Int -> Maybe Int
c Int
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 -> Int -> (Int -> Maybe Int) -> Term -> Term -> Maybe Int
f Int
nl Int
n (\Int
n -> Int -> Int -> (Int -> Maybe Int) -> Elims -> Elims -> Maybe Int
fs Int
nl Int
n Int -> Maybe Int
c Elims
es1 Elims
es2) Term
e1 Term
e2
     (Elims, Elims)
_ -> Maybe Int
forall a. Maybe a
Nothing
    fes :: Int -> Int -> (Int -> Maybe Int) -> Elims -> Elims -> Maybe Int
fes Int
nl Int
n Int -> Maybe Int
c Elims
es1 Elims
es2 = case (Elims
es1, Elims
es2) of
     ([], []) -> Int -> Maybe Int
c Int
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 -> Int -> (Int -> Maybe Int) -> Elims -> Elims -> Maybe Int
fes Int
nl Int
n Int -> Maybe Int
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 -> Int -> (Int -> Maybe Int) -> Term -> Term -> Maybe Int
f Int
nl Int
n (\Int
n -> Int -> Int -> (Int -> Maybe Int) -> Elims -> Elims -> Maybe Int
fes Int
nl Int
n Int -> Maybe Int
c Elims
es1 Elims
es2) Term
e1 Term
e2
     (Elims, Elims)
_ -> Maybe Int
forall a. Maybe a
Nothing