module Agda.Auto.Convert where

import Prelude hiding ((!!))

import Control.Monad          ( when )
import Control.Monad.Except
import Control.Monad.IO.Class ( MonadIO(..) )
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.List
import Agda.Utils.Monad       ( forMaybeMM )
import Agda.Utils.Permutation ( Permutation(Perm), permute, takeP, compactP )
import Agda.Syntax.Common.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
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 = (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) <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets S -> (a, [b])
r
                 case [b]
xs of
                  [] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
                  (b
x:[b]
xs) -> do
                   forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((a, [b]) -> S -> S
w (a
m, [b]
xs))
                   forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> 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 <- 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 <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (forall a b. (a, b) -> a
fst 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 forall k a. Ord k => Map k a -> k -> a
Map.! QName
cn
     Definition
def <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ 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 <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Type'' Term Term
typ
     MExp O
typ' <- 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' <- 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]
_ -> forall (t :: * -> *) a. Foldable t => t a -> Int
length NAPs
xs
           forall (m :: * -> *) a. Monad m => a -> m a
return (forall o. Int -> [Clause o] -> Maybe Int -> Maybe Int -> DeclCont o
Def Int
narg [Clause o]
clauses' forall a. Maybe a
Nothing forall a. Maybe a
Nothing, [])
     (DeclCont O
cont, [QName]
projfcns2) <- case Defn
defn of
      MB.Axiom {} -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall o. DeclCont o
Postulate, [])
      MB.DataOrRecSig{} -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall o. DeclCont o
Postulate, [])
      MB.GeneralizableVar{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
      MB.AbstractDefn{} -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall o. DeclCont o
Postulate, [])
      MB.Function {funClauses :: Defn -> [Clause]
MB.funClauses = [Clause]
clauses} -> 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} -> forall {m :: * -> *} {o} {a}.
(Monad m, Conversion m [Clause] [Clause o]) =>
[Clause] -> m (DeclCont o, [a])
clausesToDef [Clause]
clauses
      MB.PrimitiveSort{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
      MB.Datatype {dataCons :: Defn -> [QName]
MB.dataCons = [QName]
cons} -> do
       [ConstRef O]
cons2 <- 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
       forall (m :: * -> *) a. Monad m => a -> m a
return (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)) = forall e. ArgInfo -> e -> Arg e
Cm.Arg (forall t e. Dom' t e -> ArgInfo
I.domInfo Dom (Type'' Term Term)
it) (Int -> Term
I.var Int
n) forall a. a -> [a] -> [a]
:
                                           Int -> Type'' Term Term -> [Arg Term]
pars (Int
n forall a. Num a => a -> a -> a
- Int
1) (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 = forall t a. Sort' t -> a -> Type'' t a
I.El (Integer -> Sort' Term
I.mkType Integer
0 {- arbitrary -}) forall a b. (a -> b) -> a -> b
$
                                      QName -> Elims -> Term
I.Def QName
cn forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
I.Apply forall a b. (a -> b) -> a -> b
$ Int -> Type'' Term Term -> [Arg Term]
pars (Int
npar 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)) = 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 (forall a. String -> a -> Abs a
I.Abs String
v (Int -> Telescope -> Type'' Term Term
contyp (Int
npar forall a. Num a => a -> a -> a
+ Int
1) Telescope
tel)))
           contyp Int
npar (I.ExtendTel Dom (Type'' Term Term)
it I.NoAbs{})     = forall a. HasCallStack => a
__IMPOSSIBLE__
       MExp O
contyp' <- forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert forall a b. (a -> b) -> a -> b
$ Int -> Telescope -> Type'' Term Term
contyp Int
0 Telescope
tel
       ConstDef O
cc <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef ConstRef O
c
       let Datatype [ConstRef O
con] [] = forall o. ConstDef o -> DeclCont o
cdcont ConstDef O
cc
       forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ 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 <- 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 (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

       forall (m :: * -> *) a. Monad m => a -> m a
return (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 <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef ConstRef O
c
       let (Just (Int
nomi,[Arg QName]
_), QName
_) = forall o. ConstDef o -> o
cdorigin ConstDef O
cc
       forall (m :: * -> *) a. Monad m => a -> m a
return (forall o. Int -> DeclCont o
Constructor (Int
nomi forall a. Num a => a -> a -> a
- forall o. ConstDef o -> Int
cddeffreevars ConstDef O
cc), [])
     forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ [QName]
projfcns2 forall a. [a] -> [a] -> [a]
++ [QName]
projfcns
    Maybe QName
Nothing -> do
     Maybe MetaId
nxt <- 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
       forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\((Bool
_, Term
e, Term
i), Int
eqi) -> do
         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) forall a b. (a -> b) -> a -> b
$ do
          (Map Int (Maybe (Bool, MExp O, MExp O))
eqsm, [Int]
eqsl) <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets S -> MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall k a. Ord k => k -> Map k a -> Bool
Map.notMember Int
eqi Map Int (Maybe (Bool, MExp O, MExp O))
eqsm) forall a b. (a -> b) -> a -> b
$ do
           forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \S
s -> S
s {sEqs :: MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs = (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Int
eqi forall a. Maybe a
Nothing Map Int (Maybe (Bool, MExp O, MExp O))
eqsm, Int
eqi forall a. a -> [a] -> [a]
: [Int]
eqsl)}
        ) (forall a b. [a] -> [b] -> [(a, b)]
zip [(Bool, Term, Term)]
eqs [Int
0..])
       MetaVariable
mv <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ MetaId -> TCM MetaVariable
lookupLocalMetaAuto MetaId
mi
       Maybe Term
msol <- case MetaVariable -> MetaInstantiation
MB.mvInstantiation MetaVariable
mv of
                     MB.InstV{} ->
                      forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mv) forall a b. (a -> b) -> a -> b
$ do
                       [Arg Term]
args <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Arg Term]
getContextArgs
                       --sol <- norm (I.MetaV mi args)
                       Term
sol <- forall a (m :: * -> *). (Instantiate a, MonadReduce m) => a -> m a
instantiate forall a b. (a -> b) -> a -> b
$ MetaId -> Elims -> Term
I.MetaV MetaId
mi forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
I.Apply forall a b. (a -> b) -> a -> b
$ forall a. Permutation -> [a] -> [a]
permute (Int -> Permutation -> Permutation
takeP (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
args) forall a b. (a -> b) -> a -> b
$ MetaVariable -> Permutation
mvPermutation MetaVariable
mv) [Arg Term]
args
                       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just Term
sol
                     MetaInstantiation
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
       case Maybe Term
msol of
        Maybe Term
Nothing -> 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' <- forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Term
sol
         forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ \S
s -> S
s {sEqs :: MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs = forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (forall k a. Map k a -> Int
Map.size (forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ S -> MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs S
s)) (forall a. a -> Maybe a
Just (Bool
False, 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 = forall a. Judgement a -> Type'' Term Term
MB.jMetaType 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 = forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
I.unDom) forall b c a. (b -> c) -> (a -> b) -> a -> c
. TCEnv -> [Dom' Term (Name, Type'' Term Term)]
envContext forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Closure a -> TCEnv
clEnv forall a b. (a -> b) -> a -> b
$ Closure Range
minfo
       (Type'' Term Term
targettype, [Type'' Term Term]
localVars) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo Closure Range
minfo forall a b. (a -> b) -> a -> b
$ do
        [Arg Term]
vs <- forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m [Arg Term]
getContextArgs
        Type'' Term Term
targettype <- Type'' Term Term
tt forall a (m :: * -> *).
(PiApplyM a, MonadReduce m, HasBuiltins m) =>
Type'' Term Term -> a -> m (Type'' Term Term)
`piApplyM` forall a. Permutation -> [a] -> [a]
permute (Int -> Permutation -> Permutation
takeP (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Arg Term]
vs) forall a b. (a -> b) -> a -> b
$ MetaVariable -> Permutation
mvPermutation MetaVariable
mv) [Arg Term]
vs
        Type'' Term Term
targettype <- forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Type'' Term Term
targettype
        [Type'' Term Term]
localVars <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise [Type'' Term Term]
localVars
        forall (m :: * -> *) a. Monad m => a -> m a
return (Type'' Term Term
targettype, [Type'' Term Term]
localVars)
       forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\S
s -> S
s {sCurMeta :: Maybe MetaId
sCurMeta = forall a. a -> Maybe a
Just MetaId
mi})
       MExp O
typ' <- forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Type'' Term Term
targettype
       [MExp O]
ctx' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert [Type'' Term Term]
localVars
       forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\S
s -> S
s {sCurMeta :: Maybe MetaId
sCurMeta = forall a. Maybe a
Nothing})
       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 = forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (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, 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 <- 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 forall a. HasCallStack => [a] -> Int -> a
!! Int
eqi
         MExp O
e' <- forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Term
e
         MExp O
i' <- forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Term
i
         forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\S
s -> S
s {sEqs :: MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs = forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust (\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 ->
         forall (m :: * -> *) a. Monad m => a -> m a
return [QName]
projfcns
 (([ConstRef O]
icns', [MExp O]
typs'), S
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' <- 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' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM 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' <- 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 []
      forall (m :: * -> *) a. Monad m => a -> m a
return ([ConstRef O]
projfcns' forall a. [a] -> [a] -> [a]
++ [ConstRef O]
icns', [MExp O]
typs')
  ) (S {sConsts :: MapS QName (TMode, ConstRef O)
sConsts = forall a b. MapS a b
initMapS, sMetas :: MapS
  MetaId
  (Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
sMetas = forall a b. MapS a b
initMapS, sEqs :: MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs = forall a b. MapS a b
initMapS, sCurMeta :: Maybe MetaId
sCurMeta = forall a. Maybe a
Nothing, sMainMeta :: MetaId
sMainMeta = MetaId
imi})
 forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall o. ConstRef o -> IO ()
categorizedecl [ConstRef O]
icns'
 forall (m :: * -> *) a. Monad m => a -> m a
return ([ConstRef O]
icns', [MExp O]
typs', forall a b k. (a -> b) -> Map k a -> Map k b
Map.map forall {a} {b} {c} {d}. (a, Maybe (b, c), d) -> (a, b, c, d)
flatten (forall a b. (a, b) -> a
fst (S
-> MapS
     MetaId
     (Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
sMetas S
s)), forall a b. (a -> b) -> [a] -> [b]
map forall {a}. Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [a]
Map.elems (forall a b. (a, b) -> a
fst (S -> MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs S
s)), 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) = forall a. HasCallStack => a
__IMPOSSIBLE__

 fromJust :: Maybe a -> a
fromJust (Just a
x) = a
x
 fromJust Maybe a
Nothing = 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 <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ 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 <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. S -> MapS QName (TMode, ConstRef O)
sConsts)
   case 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 <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef ConstRef O
c
      let Datatype [ConstRef O
con] [ConstRef O]
_ = forall o. ConstDef o -> DeclCont o
cdcont ConstDef O
cd
      forall (m :: * -> *) a. Monad m => a -> m a
return ConstRef O
con
     else
      forall (m :: * -> *) a. Monad m => a -> m a
return ConstRef O
c
    Maybe (TMode, ConstRef O)
Nothing -> do
     MetaId
mainm <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets S -> MetaId
sMainMeta
     Int
dfv <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ MetaId -> QName -> TCM 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 <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. a -> IO (IORef a)
newIORef (ConstDef {cdname :: String
cdname = forall a. Pretty a => a -> String
prettyShow QName
name forall a. [a] -> [a] -> [a]
++ String
".CONS", cdorigin :: O
cdorigin = (forall a. a -> Maybe a
Just (Int
nomi,[Arg QName]
conflds), QName
conname), cdtype :: MExp O
cdtype = forall a. HasCallStack => a
__IMPOSSIBLE__, cdcont :: DeclCont O
cdcont = forall o. Int -> DeclCont o
Constructor (Int
nomi forall a. Num a => a -> a -> a
- Int
dfv), cddeffreevars :: Int
cddeffreevars = Int
dfv}) -- ?? correct value of deffreevars for records?
     ConstRef O
c <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. a -> IO (IORef a)
newIORef (ConstDef {cdname :: String
cdname = forall a. Pretty a => a -> String
prettyShow QName
name, cdorigin :: O
cdorigin = (forall a. Maybe a
Nothing, QName
name), cdtype :: MExp O
cdtype = forall a. HasCallStack => a
__IMPOSSIBLE__, cdcont :: DeclCont O
cdcont = forall o. [ConstRef o] -> [ConstRef o] -> DeclCont o
Datatype [ConstRef O
ccon] [], cddeffreevars :: Int
cddeffreevars = Int
dfv}) -- ?? correct value of deffreevars for records?
     forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\S
s -> S
s {sConsts :: MapS QName (TMode, ConstRef O)
sConsts = (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 forall a. a -> [a] -> [a]
: forall a b. (a, b) -> b
snd (S -> MapS QName (TMode, ConstRef O)
sConsts S
s))})
     forall (m :: * -> *) a. Monad m => a -> m a
return 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 <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. S -> MapS QName (TMode, ConstRef O)
sConsts)
   case 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) ->
     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
       forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (Int
npar,ConHead -> [Arg QName]
I.conFields ConHead
ch), forall a. Pretty a => a -> String
prettyShow QName
dname forall a. [a] -> [a] -> [a]
++ String
"." forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> String
prettyShow (QName -> Name
I.qnameName QName
name))
      else
       forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Maybe a
Nothing, forall a. Pretty a => a -> String
prettyShow QName
name)
     MetaId
mainm <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets S -> MetaId
sMainMeta
     Int
dfv <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ MetaId -> QName -> TCM Int
getdfv MetaId
mainm QName
name
     ConstRef O
c <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ 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 = forall a. HasCallStack => a
__IMPOSSIBLE__, cdcont :: DeclCont O
cdcont = forall a. HasCallStack => a
__IMPOSSIBLE__, cddeffreevars :: Int
cddeffreevars = Int
dfv})
     forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\S
s -> S
s {sConsts :: MapS QName (TMode, ConstRef O)
sConsts = (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 forall a. a -> [a] -> [a]
: forall a b. (a, b) -> b
snd (S -> MapS QName (TMode, ConstRef O)
sConsts S
s))})
     forall (m :: * -> *) a. Monad m => a -> m a
return ConstRef O
c

getdfv :: I.MetaId -> A.QName -> MB.TCM Cm.Nat
getdfv :: MetaId -> QName -> TCM Int
getdfv MetaId
mainm QName
name = do
 MetaVariable
mv <- MetaId -> TCM MetaVariable
lookupLocalMetaAuto MetaId
mainm
 forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadTrace m) =>
Closure Range -> m a -> m a
withMetaInfo (MetaVariable -> Closure Range
getMetaInfo MetaVariable
mv) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
QName -> m Int
getDefFreeVars QName
name

-- | A variant of 'lookupLocalMeta' that, if applied to a remote
-- meta-variable, raises a special error message noting that remote
-- meta-variables are not handled by the auto command.

lookupLocalMetaAuto :: I.MetaId -> MB.TCM MB.MetaVariable
lookupLocalMetaAuto :: MetaId -> TCM MetaVariable
lookupLocalMetaAuto MetaId
m = do
  Maybe (Either RemoteMetaVariable MetaVariable)
mv <- forall (m :: * -> *).
ReadTCState m =>
MetaId -> m (Maybe (Either RemoteMetaVariable MetaVariable))
lookupMeta MetaId
m
  case Maybe (Either RemoteMetaVariable MetaVariable)
mv of
    Just (Right MetaVariable
mv) -> forall (m :: * -> *) a. Monad m => a -> m a
return MetaVariable
mv
    Maybe (Either RemoteMetaVariable MetaVariable)
Nothing         -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Just Left{}     -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
MB.typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
MB.GenericError forall a b. (a -> b) -> a -> b
$
      String
"The auto command does not support remote meta-variables," forall a. [a] -> [a] -> [a]
++
      String
"consider using --no-save-metas"

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 <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (forall a b. (a, b) -> a
fst 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 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]
_) ->
   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 <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a blk. IO (Metavar a blk)
initMeta
   forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify 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 = (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert MetaId
name (Metavar (Exp O) (RefInfo O)
m, forall a. Maybe a
Nothing, []) Map
  MetaId
  (Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
mmap, MetaId
name forall a. a -> [a] -> [a]
: forall a b. (a, b) -> b
snd (S
-> MapS
     MetaId
     (Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [MetaId])
sMetas S
s)) }
   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 = forall (m :: * -> *) a b.
Monad m =>
m [a] -> (a -> m (Maybe b)) -> m [b]
forMaybeMM forall (m :: * -> *). ReadTCState m => m Constraints
getAllConstraints forall a b. (a -> b) -> a -> b
$ \ ProblemConstraint
eqc -> do
  ProblemConstraint
neqc <- forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise ProblemConstraint
eqc
  case forall a. Closure a -> a
MB.clValue 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 <- forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) =>
a -> m a
etaContract Term
i
      Term
ee <- forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) =>
a -> m a
etaContract Term
e
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (Comparison -> Bool
tomyIneq Comparison
ineq, Term
ee, Term
ei)
    Constraint
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

literalsNotImplemented :: MB.TCM a
literalsNotImplemented :: forall a. TCM a
literalsNotImplemented = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
MB.typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
MB.NotImplemented 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 = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
MB.typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
MB.NotImplemented 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 = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. [Maybe a] -> [a]
catMaybes forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM 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 -> TOM (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' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert (forall a b. LabelPatVars a b => b -> a
IP.unnumberPatVars [Arg DeBruijnPattern]
pats :: [Cm.Arg I.Pattern])
    Maybe (MExp O)
body' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Maybe Term
body)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ([Pat O]
pats',) 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) -> TOM (Pat O)
convert Arg (Pattern' String)
p = case forall e. Arg e -> e
Cm.unArg Arg (Pattern' String)
p of
    I.IApplyP PatternInfo
_ Term
_ Term
_ String
n  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall o. String -> Pat o
PatVar (forall a. Pretty a => a -> String
prettyShow String
n)
    I.VarP PatternInfo
_ String
n  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall o. String -> Pat o
PatVar (forall a. Pretty a => a -> String
prettyShow String
n)
    I.DotP PatternInfo
_ Term
_  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall name a. Named name a -> a
Cm.namedThing) [NamedArg (Pattern' String)]
pats
      Definition
def   <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
n
      ConstDef O
cc    <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef ConstRef O
c
      let Just (Int
npar,[Arg QName]
_) = forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall o. ConstDef o -> o
cdorigin ConstDef O
cc
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall o. ConstRef o -> [Pat o] -> Pat o
PatConApp ConstRef O
c (forall a. Int -> a -> [a]
replicate Int
npar forall o. Pat o
PatExp forall a. [a] -> [a] -> [a]
++ [Pat O]
pats')
    I.ProjP ProjOrigin
_ QName
q -> forall o. ConstRef o -> Pat o
PatProj forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> QName -> TMode -> StateT S (TCMT IO) (ConstRef O)
getConst Bool
True QName
q TMode
TMAll

    -- UNSUPPORTED CASES
    I.LitP{}    -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a. TCM a
literalsNotImplemented
    I.DefP{}    -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift 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) = 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 = forall a. [Elim' a] -> Maybe [Arg a]
I.allApplyElims Elims
es
        MArgList O
as' <- forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert [Arg Term]
as
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App forall a. Maybe a
Nothing (forall a blk. a -> MM a blk
NotM OKVal
OKVal) (forall o. Int -> Elr o
Var Int
v) MArgList O
as'
      I.Lam ArgInfo
info Abs Term
b -> do
        MExp O
b' <- forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert (forall a. Subst a => Abs a -> a
I.absBody Abs Term
b)
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o. Hiding -> Abs (MExp o) -> Exp o
Lam (forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info) (forall a. MId -> a -> Abs a
Abs (String -> MId
Id forall a b. (a -> b) -> a -> b
$ forall a. Abs a -> String
I.absName Abs Term
b) MExp O
b')
      t :: Term
t@I.Lit{} -> do
        Term
t <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm Term
t
        case Term
t of
          I.Lit{} -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a. TCM a
literalsNotImplemented
          Term
_       -> forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Term
t
      I.Level Level
l -> forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall (m :: * -> *). HasBuiltins m => Level -> m Term
reallyUnLevelView Level
l)
      I.Def QName
name Elims
es -> do
        let Just [Arg Term]
as = 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' <- forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert [Arg Term]
as
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App forall a. Maybe a
Nothing (forall a blk. a -> MM a blk
NotM OKVal
OKVal) (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 = 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' <- forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert [Arg Term]
as
        Definition
def <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
name
        ConstDef O
cc  <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef ConstRef O
c
        let Just (Int
npar,[Arg QName]
_) = forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall o. ConstDef o -> o
cdorigin ConstDef O
cc
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App forall a. Maybe a
Nothing (forall a blk. a -> MM a blk
NotM OKVal
OKVal) (forall o. ConstRef o -> Elr o
Const ConstRef O
c) (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\MArgList O
x Int
_ -> forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ 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    = forall a. Subst a => Abs a -> a
I.absBody Abs (Type'' Term Term)
b
            name :: String
name = forall a. Abs a -> String
I.absName Abs (Type'' Term Term)
b
        MExp O
x' <- forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Type'' Term Term
x
        MExp O
y' <- forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Type'' Term Term
y
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
Pi forall a. Maybe a
Nothing (forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info) (forall a. Free a => Int -> a -> Bool
Free.freeIn Int
0 Type'' Term Term
y) MExp O
x' (forall a. MId -> a -> Abs a
Abs (String -> MId
Id String
name) MExp O
y')
      I.Sort (I.Type (I.ClosedLevel Integer
l)) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o. Sort -> Exp o
Sort forall a b. (a -> b) -> a -> b
$ Int -> Sort
Set forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
l
      I.Sort Sort' Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o. Sort -> Exp o
Sort Sort
UnknownSort
      I.Dummy{}-> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o. Sort -> Exp o
Sort Sort
UnknownSort
      t :: Term
t@I.MetaV{} -> do
        Term
t <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ 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 <- forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets S -> Maybe MetaId
sCurMeta
            case Maybe MetaId
mcurmeta of
              Maybe MetaId
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
              Just MetaId
curmeta ->
                forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify 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 = forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (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 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
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a blk. Metavar a blk -> MM a blk
Meta Metavar (Exp O) (RefInfo O)
m
          Term
_ -> forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert Term
t
      I.DontCare Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a blk. a -> MM a blk
NotM 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) = (forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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] -> TOM (MArgList O)
convert [Arg Term]
as = forall a blk. a -> MM a blk
NotM forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (Hiding
hid,MExp O
t) -> forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
hid MExp O
t forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a blk. a -> MM a blk
NotM) forall o. ArgList o
ALNil
               forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM 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 forall a b. (a -> b) -> a -> b
$ 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 (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)) = 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 forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ 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 (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 (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 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 = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (MetaId -> Term -> Bool
fmExp MetaId
m forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a. LensHiding a => Hiding -> a -> a
Cm.setHiding Hiding
h forall a b. (a -> b) -> a -> b
$
          forall a. LensOrigin a => Origin -> a -> a
Cm.setOrigin Origin
o 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 -> forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert a
a
    Meta Metavar a (RefInfo O)
m -> do
      Maybe a
ma <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef forall a b. (a -> b) -> a -> b
$ forall a blk. Metavar a blk -> IORef (Maybe a)
mbind Metavar a (RefInfo O)
m
      case Maybe a
ma of
        Maybe a
Nothing -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"meta not bound"
        Just a
a  -> 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) = forall a. String -> a -> Abs a
I.Abs String
id forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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 = forall t a. Sort' t -> a -> Type'' t a
I.El (Integer -> Sort' Term
I.mkType Integer
0) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 -> MOT Term
convert = \case
    App Maybe (Metavar (Exp O) (RefInfo O))
_ OKHandle (RefInfo O)
_ (Var Int
v) MArgList O
as -> Int -> MArgList O -> Term -> MOT 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 <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef ConstRef O
c
      let (Maybe (Int, [Arg QName])
iscon, QName
name) = 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 forall p. DataOrRecord' p
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 -> MOT 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) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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' <- forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert MExp O
x
      let dom :: Dom (Type'' Term Term)
dom = (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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort' Term -> Term
I.Sort (Integer -> Sort' Term
I.mkType (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
l))
    Sort Sort
Type -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Sort Sort
UnknownSort -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ ArgInfo -> Abs Term -> Term
I.Lam (Hiding -> ArgInfo
icnvh Hiding
hid)
                               forall a b. (a -> b) -> a -> b
$ 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 -> MOT Term
frommyExps Int
ndrop (Meta Metavar (ArgList O) (RefInfo O)
m) Term
trm = do
 Maybe (ArgList O)
bind <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef forall a b. (a -> b) -> a -> b
$ 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 -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"meta not bound"
  Just ArgList O
e -> Int -> MArgList O -> Term -> MOT Term
frommyExps Int
ndrop (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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Term
trm
  ALCons Hiding
_ MExp O
_ MArgList O
xs | Int
ndrop forall a. Ord a => a -> a -> Bool
> Int
0 -> Int -> MArgList O -> Term -> MOT Term
frommyExps (Int
ndrop 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' <- forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert MExp O
x
   Int -> MArgList O -> Term -> MOT Term
frommyExps Int
ndrop MArgList O
xs (Arg Term -> Term -> Term
addend (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 <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return ConstRef O
c
            Meta{} -> forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"meta not bound"
   ConstDef O
cdef <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef ConstRef O
c
   let name :: QName
name = forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall o. ConstDef o -> o
cdorigin ConstDef O
cdef
   Term
trm2 <- Int -> MArgList O -> Term -> MOT Term
frommyExps Int
0 MArgList O
eas (QName -> Elims -> Term
I.Def QName
name [])
   Int -> MArgList O -> Term -> MOT Term
frommyExps Int
0 MArgList O
xs (Arg Term -> Term -> Term
addend (forall e. ArgInfo -> e -> Arg e
Cm.Arg (Hiding -> ArgInfo
icnvh Hiding
hid) Term
trm) Term
trm2)

  ALConPar MArgList O
xs | Int
ndrop forall a. Ord a => a -> a -> Bool
> Int
0 -> Int -> MArgList O -> Term -> MOT Term
frommyExps (Int
ndrop forall a. Num a => a -> a -> a
- Int
1) MArgList O
xs Term
trm
  ALConPar MArgList O
_ -> 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 forall a. [a] -> [a] -> [a]
++ [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 forall a. [a] -> [a] -> [a]
++ [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 forall a. [a] -> [a] -> [a]
++ [forall a. Arg a -> Elim' a
I.Apply Arg Term
x])
  addend Arg 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) (forall e. ArgInfo -> e -> Arg e
Cm.Arg ArgInfo
info (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}) <- forall a. NamedArg a -> a
Cm.namedArg NamedArg Binder
x
     , forall a. Pretty a => a -> String
prettyShow (Name -> Name
A.nameConcrete Name
n) forall a. Eq a => a -> a -> Bool
== String
abslamvarname =
        ExprInfo -> Hiding -> Expr
A.AbsurdLam ExprInfo
i forall a b. (a -> b) -> a -> b
$ 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 (forall a b. (a -> b) -> [a] -> [b]
map (forall a c b. (a -> c) -> Either a b -> Either c b
mapLeft (forall o i. Lens' o i -> LensMap o i
over forall a. Lens' (FieldAssignment' a) a
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) (forall a b. (a -> b) -> [a] -> [b]
map (forall o i. Lens' o i -> LensMap o i
over forall a. Lens' (FieldAssignment' a) a
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) =
  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 [] = 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
      forall (m :: * -> *) a. Monad m => a -> m a
return ([(Hiding, MId)]
ns'', CSPat O
p' 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 = forall a. LensHiding a => a -> Hiding
getHiding forall a b. (a -> b) -> a -> b
$ forall e. Arg e -> ArgInfo
Cm.argInfo NamedArg (Pattern' String)
p
      in case forall a. NamedArg a -> a
Cm.namedArg NamedArg (Pattern' String)
p of
       I.VarP PatternInfo
_ String
n -> forall (m :: * -> *) a. Monad m => a -> m a
return ((Hiding
hid, String -> MId
Id String
n) forall a. a -> [a] -> [a]
: [(Hiding, MId)]
ns, forall a. Hiding -> a -> HI a
HI Hiding
hid (forall o. Int -> CSPatI o
CSPatVar forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Hiding, MId)]
ns))
       I.IApplyP PatternInfo
_ Term
_ Term
_ String
n -> forall (m :: * -> *) a. Monad m => a -> m a
return ((Hiding
hid, String -> MId
Id String
n) forall a. a -> [a] -> [a]
: [(Hiding, MId)]
ns, forall a. Hiding -> a -> HI a
HI Hiding
hid (forall o. Int -> CSPatI o
CSPatVar forall a b. (a -> b) -> a -> b
$ 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
_) <- 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 = forall a b. MapS a b
initMapS, sEqs :: MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs = forall a b. MapS a b
initMapS, sCurMeta :: Maybe MetaId
sCurMeta = 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 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef ConstRef O
c2
        let Just (Int
npar,[Arg QName]
_) = forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall o. ConstDef o -> o
cdorigin ConstDef O
cc
        forall (m :: * -> *) a. Monad m => a -> m a
return ([(Hiding, MId)]
ns', forall a. Hiding -> a -> HI a
HI Hiding
hid (forall o. ConstRef o -> [CSPat o] -> CSPatI o
CSPatConApp ConstRef O
c2 (forall a. Int -> a -> [a]
replicate Int
npar (forall a. Hiding -> a -> HI a
HI Hiding
Hidden forall o. CSPatI o
CSOmittedArg) forall a. [a] -> [a] -> [a]
++ [CSPat O]
ps')))
       I.DotP PatternInfo
_ Term
t -> do
        (MExp O
t2, S
_) <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (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 = forall a b. MapS a b
initMapS, sEqs :: MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs = forall a b. MapS a b
initMapS, sCurMeta :: Maybe MetaId
sCurMeta = forall a. Maybe a
Nothing, sMainMeta :: MetaId
sMainMeta = MetaId
mainm})
        forall (m :: * -> *) a. Monad m => a -> m a
return ([(Hiding, MId)]
ns, forall a. Hiding -> a -> HI a
HI Hiding
hid (forall o. MExp o -> CSPatI o
CSPatExp MExp O
t2))
       I.ProjP ProjOrigin
po QName
c -> do
        (ConstRef O
c2, 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 = forall a b. MapS a b
initMapS, sEqs :: MapS Int (Maybe (Bool, MExp O, MExp O))
sEqs = forall a b. MapS a b
initMapS, sCurMeta :: Maybe MetaId
sCurMeta = forall a. Maybe a
Nothing, sMainMeta :: MetaId
sMainMeta = MetaId
mainm})
        ConstDef O
cc <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef ConstRef O
c2
        forall (m :: * -> *) a. Monad m => a -> m a
return ([(Hiding, MId)]
ns, forall a. Hiding -> a -> HI a
HI Hiding
hid (forall o. ConstRef o -> CSPatI o
CSPatProj ConstRef O
c2))
       I.LitP{} -> forall a. TCM a
literalsNotImplemented
       I.DefP{} -> forall a. TCM a
hitsNotImplemented

 ([(Hiding, MId)]
names, [CSPat O]
pats) <- [(Hiding, MId)]
-> [NamedArg (Pattern' String)] -> TCM ([(Hiding, MId)], [CSPat O])
cnvps [] (forall a b. LabelPatVars a b => b -> a
IP.unnumberPatVars forall a b. (a -> b) -> a -> b
$ Clause -> NAPs
I.namedClausePats Clause
clause)
 forall (m :: * -> *) a. Monad m => a -> m a
return (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 [] = forall (m :: * -> *) a. Monad m => a -> m a
return 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' <- forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert a
t
      let dom :: Dom' Term e
dom = (forall a. a -> Dom a
I.defaultDom e
t') {domInfo :: ArgInfo
domInfo = Hiding -> ArgInfo
icnvh Hiding
hid}
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Abs (Tele a) -> Tele a
I.ExtendTel Dom' Term e
dom (forall a. String -> a -> Abs a
I.Abs String
id Tele (Dom' Term e)
tel)
 Telescope
tel <- forall {m :: * -> *} {a} {e}.
(Monad m, Conversion m a e) =>
[HI (MId, a)] -> m (Tele (Dom' Term e))
ctel forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *) a. Monad m => a -> m a
return ([(Int, Int)]
perm, Int
nv)
     getperms Int
n [] [(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 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 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
_ = 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return ((forall (t :: * -> *) a. Foldable t => t a -> Int
length CSCtx O
ids forall a. Num a => a -> a -> a
- Int
1 forall a. Num a => a -> a -> a
- Int
v, Int
nv) forall a. a -> [a] -> [a]
: [(Int, Int)]
perm, Int
nv forall a. Num a => a -> a -> a
+ Int
1)
       CSPatConApp ConstRef O
c [CSPat O]
ps -> do
        ConstDef O
cdef <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef ConstRef O
c
        let (Just (Int
ndrop,[Arg QName]
_), QName
_) = 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return ([(Int, Int)]
perm, Int
nv forall a. Num a => a -> a -> a
+ Int
1)
       CSPatI O
_ -> 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 = forall a b. (a -> b) -> [a] -> [b]
map (\Int
i -> let Just Int
x = forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Int
i [(Int, Int)]
rperm in Int
x) [Int
0..forall (t :: * -> *) a. Foldable t => t a -> Int
length CSCtx O
ids 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 [] = forall (m :: * -> *) a. Monad m => a -> m a
return []
     cnvps Int
n [] = 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
      forall (m :: * -> *) a. Monad m => a -> m a
return (NamedArg (Pattern' String)
p' 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 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 forall a. Num a => a -> a -> a
- Int
1) [CSPat O]
ps
     cnvps Int
n (CSPat O
_ : [CSPat O]
_) = 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Pattern' a
I.varP forall a b. (a -> b) -> a -> b
$ let HI Hiding
_ (Id String
n, MExp O
_) = CSCtx O
ids forall a. HasCallStack => [a] -> Int -> a
!! Int
v in String
n)
       CSPatConApp ConstRef O
c [CSPat O]
ps -> do
        ConstDef O
cdef <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef ConstRef O
c
        let (Just (Int
ndrop,[Arg QName]
_), QName
name) = 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 forall p. DataOrRecord' p
I.IsData Induction
Cm.Inductive [] -- TODO: restore DataOrRecord and record fields!
        forall (m :: * -> *) a. Monad m => a -> m a
return (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' <- forall (m :: * -> *) a b. Conversion m a b => a -> m b
convert MExp O
e {- renm e -} -- renaming before adding to clause below
        forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. Term -> Pattern' a
I.dotP Term
e')
       CSPatI O
CSAbsurd -> forall a. HasCallStack => a
__IMPOSSIBLE__ -- CSAbsurd not used
       CSPatI O
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall e. ArgInfo -> e -> Arg e
Cm.Arg (Hiding -> ArgInfo
icnvh Hiding
hid) forall a b. (a -> b) -> a -> b
$ 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Maybe a
Nothing
          Just MExp O
e -> forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
 forall (m :: * -> *) a. Monad m => a -> m a
return I.Clause
   { clauseLHSRange :: Range
I.clauseLHSRange  = forall a. Range' a
SP.noRange
   , clauseFullRange :: Range
I.clauseFullRange = forall a. Range' a
SP.noRange
   , clauseTel :: Telescope
I.clauseTel       = Telescope
tel
   , namedClausePats :: NAPs
I.namedClausePats = forall a b.
(LabelPatVars a b, PatVarLabel b ~ Int) =>
Int -> Permutation -> a -> b
IP.numberPatVars forall a. HasCallStack => a
__IMPOSSIBLE__ Permutation
cperm forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (forall a. DeBruijn a => Permutation -> Substitution' a
renamingR 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      = forall a. Maybe a
Nothing -- TODO: compute clause type
   , clauseCatchall :: Bool
I.clauseCatchall    = Bool
False
   , clauseExact :: Maybe Bool
I.clauseExact       = forall a. Maybe a
Nothing -- TODO
   , clauseRecursive :: Maybe Bool
I.clauseRecursive   = forall a. Maybe a
Nothing -- TODO: Don't know here whether recursive or not !?
   , clauseUnreachable :: Maybe Bool
I.clauseUnreachable = forall a. Maybe a
Nothing -- TODO: Don't know here whether reachable or not !?
   , clauseEllipsis :: ExpandedEllipsis
I.clauseEllipsis    = ExpandedEllipsis
Cm.NoEllipsis
   , clauseWhereModule :: Maybe ModuleName
I.clauseWhereModule = forall a. Maybe a
Nothing
   }

contains_constructor :: [CSPat O] -> Bool
contains_constructor :: [CSPat O] -> Bool
contains_constructor = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any 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 = 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 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' 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 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 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 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{} -> 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 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) -> forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ 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 (forall a. MId -> a -> Abs a
Abs MId
id (Int -> MExp o -> MExp o
f (Int
n forall a. Num a => a -> a -> a
+ Int
1) MExp o
ot))
   Exp o
_ -> forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
Pi forall a. Maybe a
Nothing Hiding
NotHidden Bool
False (forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
Pi forall a. Maybe a
Nothing Hiding
NotHidden Bool
False MExp o
e (forall a. MId -> a -> Abs a
Abs MId
NoId (forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
Pi forall a. Maybe a
Nothing Hiding
NotHidden Bool
True (forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o. Sort -> Exp o
Sort (Int -> Sort
Set Int
0)) (forall a. MId -> a -> Abs a
Abs MId
NoId (forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App forall a. Maybe a
Nothing (forall a blk. a -> MM a blk
NotM OKVal
OKVal) (forall o. Int -> Elr o
Var Int
0) (forall a blk. a -> MM a blk
NotM forall o. ArgList o
ALNil)))))) (forall a. MId -> a -> Abs a
Abs MId
NoId (forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App forall a. Maybe a
Nothing (forall a blk. a -> MM a blk
NotM OKVal
OKVal) (forall o. ConstRef o -> Elr o
Const ConstRef o
ee) (forall a blk. a -> MM a blk
NotM 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 = forall (m :: * -> *) a. MonadTCEnv m => m a -> m a
ignoreAbstractMode forall a b. (a -> b) -> a -> b
$ do  -- Andreas, 2016-09-04, issue #2162
  MB.InteractionPoint { ipClause :: InteractionPoint -> IPClause
MB.ipClause = IPClause
ipCl} <- forall (m :: * -> *).
(MonadFail m, ReadTCState m, MonadError TCErr m) =>
InteractionId -> m InteractionPoint
lookupInteractionPoint InteractionId
ii
  case IPClause
ipCl of
    IPClause
MB.IPNoClause -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    MB.IPClause QName
f Int
clauseNo Type'' Term Term
_ Maybe Substitution
_ SpineClause
_ Closure ()
_ -> do
      (CaseContext
_, ([Clause]
_, Clause
c, [Clause]
_)) <- QName -> Int -> TCM (CaseContext, ClauseZipper)
getClauseZipperForIP QName
f Int
clauseNo
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (QName
f, Clause
c, forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. HasCallStack => a
__IMPOSSIBLE__ Term -> Bool
toplevel 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 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 forall a. Num a => a -> a -> a
- Int
1) (forall a. Subst a => Abs a -> a
I.absBody Abs (Type'' Term Term)
ot)
   Term
_ -> 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 forall a. a -> Maybe a
Just Type'' Term Term
ctyp Type'' Term Term
ttyp of
    Just Int
n -> forall a. a -> Maybe a
Just (Int
n, Int
narg)
    Maybe Int
Nothing -> case 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 forall a. Num a => a -> a -> a
+ Int
1) (Int
na 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 forall a. Num a => a -> a -> a
+ Int
1) Int
na Type'' Term Term
ot
     Term
_ -> 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 forall a. Ord a => a -> a -> Bool
< Int
nl -> case Term
e2 of
      I.Var Int
v2 Elims
as2 | Int
v1 forall a. Eq a => a -> a -> Bool
== Int
v2 -> Int -> Int -> (Int -> Maybe Int) -> Elims -> Elims -> Maybe Int
fes Int
nl (Int
n forall a. Num a => a -> a -> a
+ Int
1) Int -> Maybe Int
c Elims
as1 Elims
as2
      Term
_ -> forall a. Maybe a
Nothing
     I.Var Int
v1 Elims
_ | Int
v1 forall a. Ord a => a -> a -> Bool
< Int
nl 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 forall a. Num a => a -> a -> a
+ Int
na forall a. Num a => a -> a -> a
+ Int
nl forall a. Num a => a -> a -> a
- Int
v1 forall a. Eq a => a -> a -> Bool
== Int
tctx forall a. Num a => a -> a -> a
+ Int
nl forall a. Num a => a -> a -> a
- Int
v2 -> Int -> Int -> (Int -> Maybe Int) -> Elims -> Elims -> Maybe Int
fes Int
nl (Int
n forall a. Num a => a -> a -> a
+ Int
1) Int -> Maybe Int
c Elims
as1 Elims
as2
      Term
_ -> 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 forall a. Eq a => a -> a -> Bool
== ArgInfo
hid2 -> Int -> Int -> (Int -> Maybe Int) -> Term -> Term -> Maybe Int
f (Int
nl forall a. Num a => a -> a -> a
+ Int
1) Int
n Int -> Maybe Int
c (forall a. Subst a => Abs a -> a
I.absBody Abs Term
b1) (forall a. Subst a => Abs a -> a
I.absBody Abs Term
b2)
      (I.Lit Literal
lit1, I.Lit Literal
lit2) | Literal
lit1 forall a. Eq a => a -> a -> Bool
== Literal
lit2 -> Int -> Maybe Int
c (Int
n forall a. Num a => a -> a -> a
+ Int
1)
      (I.Def QName
n1 Elims
as1, I.Def QName
n2 Elims
as2) | QName
n1 forall a. Eq a => a -> a -> Bool
== QName
n2 -> Int -> Int -> (Int -> Maybe Int) -> Elims -> Elims -> Maybe Int
fes Int
nl (Int
n 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 forall a. Eq a => a -> a -> Bool
== ConHead
n2 -> Int -> Int -> (Int -> Maybe Int) -> Elims -> Elims -> Maybe Int
fs Int
nl (Int
n 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 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 forall a. Num a => a -> a -> a
+ Int
1) Int
n Int -> Maybe Int
c (forall a. Subst a => Abs a -> a
I.absBody Abs (Type'' Term Term)
ot1) (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)
_ -> 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 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)
_ -> 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 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 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)
_ -> forall a. Maybe a
Nothing