    {-# LANGUAGE CPP #-}

    module Agda.Auto.Convert where

    import Control.Applicative hiding (getConst, Const(..))
    import Data.IORef
    import Data.Maybe (catMaybes)
    import Data.Map (Map)
    import qualified Data.Map as Map
    import Data.Traversable (traverse)
    import Control.Monad.State

    import Agda.Syntax.Common (Hiding(..), getHiding)
    import Agda.Syntax.Concrete (exprFieldA)
    import qualified Agda.Syntax.Internal as I
    import qualified Agda.Syntax.Internal.Pattern as IP
    import qualified Agda.Syntax.Common as Cm
    import Agda.Syntax.Common (Dom(..),domInfo,unDom)
    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.Utils.Permutation (Permutation(Perm), permute, takeP, compactP)
    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.TypeChecking.Errors ( stringTCErr )

    import Agda.Interaction.MakeCase (getClauseZipperForIP)

    import Agda.Auto.NarrowingSearch
    import Agda.Auto.Syntax hiding (getConst)

    import Agda.Auto.CaseSplit hiding (lift)

    import Agda.Utils.Either
    import Agda.Utils.Except ( ExceptT , MonadError(throwError) )
    import Agda.Utils.Lens
    import Agda.Utils.Pretty ( prettyShow )

    import Agda.Utils.Impossible
    #include "undefined.h"

    data Hint = Hint
      { hintIsConstructor :: Bool
      , hintQName         :: I.QName
      }

    type O = (Maybe Int, 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 Eq

    type MapS a b = (Map a b, [a])

    initMapS :: MapS a b
    initMapS = (Map.empty, [])

    popMapS :: (S -> (a, [b])) -> ((a, [b]) -> S -> S) -> TOM (Maybe b)
    popMapS r w = do (m, xs) <- gets r
                     case xs of
                      [] -> return Nothing
                      (x:xs) -> do
                       modify (w (m, xs))
                       return $ Just x

    data S = S {sConsts :: MapS AN.QName (TMode, ConstRef O),
                sMetas :: MapS I.MetaId (Metavar (Exp O) (RefInfo O), Maybe (MExp O, [MExp O]), [I.MetaId]),
                sEqs :: MapS Int (Maybe (Bool, MExp O, MExp O)),
                sCurMeta :: Maybe I.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 imi icns typs = do
     eqs <- getEqs
     let
      r :: [AN.QName] -> TOM [AN.QName]
      r projfcns = do
       nxt <- popMapS sConsts (\x y -> y {sConsts = x})
       case nxt of
        Just cn -> do
         cmap <- fst `liftM` gets sConsts
         let (mode, c) = cmap Map.! cn
         def <- lift $ getConstInfo cn
         let typ = MB.defType def
             defn = MB.theDef def
         typ <- lift $ normalise typ
         typ' <- convert typ
         let clausesToDef clauses = do
               clauses' <- convert clauses
               let narg = case clauses of
                            [] -> 0
                            I.Clause {I.namedClausePats = xs} : _ -> length xs
               return (Def narg clauses' Nothing Nothing, [])
         (cont, projfcns2) <- case defn of
          MB.Axiom {} -> return (Postulate, [])
          MB.DataOrRecSig{} -> return (Postulate, [])
          MB.GeneralizableVar{} -> __IMPOSSIBLE__
          MB.AbstractDefn{} -> return (Postulate, [])
          MB.Function {MB.funClauses = clauses} -> clausesToDef clauses
          -- MB.Primitive {MB.primClauses = []} -> throwError $ strMsg "Auto: Primitive functions are not supported" -- Andreas, 2013-06-17 breaks interaction/AutoMisc
          MB.Primitive {MB.primClauses = clauses} -> clausesToDef clauses
          MB.Datatype {MB.dataCons = cons} -> do
           cons2 <- mapM (\con -> getConst True con TMAll) cons
           return (Datatype cons2 [], [])
          MB.Record {MB.recFields = fields, MB.recTel = tel} -> do -- the value of recPars seems unreliable or don't know what it signifies
           let pars n (I.El _ (I.Pi it typ)) = Cm.Arg (Cm.domInfo it) (I.var n) :
                                               pars (n - 1) (I.unAbs typ)
               pars _ (I.El _ _) = []
               contyp npar I.EmptyTel = I.El (I.mkType 0 {- arbitrary -}) $
                                          I.Def cn $ map I.Apply $ pars (npar - 1) typ
               contyp npar (I.ExtendTel it (I.Abs v tel)) = I.El (I.mkType 0 {- arbitrary -}) (I.Pi it (I.Abs v (contyp (npar + 1) tel)))
               contyp npar (I.ExtendTel it I.NoAbs{})     = __IMPOSSIBLE__
           contyp' <- convert $ contyp 0 tel
           cc <- lift $ liftIO $ readIORef c
           let Datatype [con] [] = cdcont cc
           lift $ liftIO $ modifyIORef con (\cdef -> cdef {cdtype = contyp'})

           projfcns <- mapM (\name -> getConst False name TMAll) (map Cm.unArg fields)

           return (Datatype [con] projfcns, []{-map snd fields-})
          MB.Constructor {MB.conData = dt} -> do
           _ <- getConst False dt TMAll -- make sure that datatype is included
           cc <- lift $ liftIO $ readIORef c
           let (Just nomi, _) = cdorigin cc
           return (Constructor (nomi - cddeffreevars cc), [])
         lift $ liftIO $ modifyIORef c (\cdef -> cdef {cdtype = typ', cdcont = cont})
         r $ projfcns2 ++ projfcns
        Nothing -> do
         nxt <- popMapS sMetas (\x y -> y {sMetas = x})
         case nxt of
          Just mi -> do
           mapM_ (\((_, e, i), eqi) -> do
             when (fmExp mi e || fmExp mi i) $ do
              (eqsm, eqsl) <- gets sEqs
              when (Map.notMember eqi eqsm) $ do
               modify $ \s -> s {sEqs = (Map.insert eqi Nothing eqsm, eqi : eqsl)}
            ) (zip eqs [0..])
           mv <- lift $ lookupMeta mi
           msol <- case MB.mvInstantiation mv of
                         MB.InstV{} ->
                          lift $ withMetaInfo (getMetaInfo mv) $ do
                           args <- getContextArgs
                           --sol <- norm (I.MetaV mi args)
                           sol <- instantiate $ I.MetaV mi $ map I.Apply $ permute (takeP (length args) $ mvPermutation mv) args
                           return $ Just sol
                         _ -> return Nothing
           case msol of
            Nothing -> return ()
            Just sol -> do
             m <- getMeta mi
             sol' <- convert sol
             modify $ \s -> s {sEqs = (Map.insert (Map.size (fst $ sEqs s)) (Just (False, Meta m, sol')) (fst $ sEqs s), snd $ sEqs s)}
           let tt = MB.jMetaType $ mvJudgement mv
               minfo = getMetaInfo mv
               localVars = map (snd . Cm.unDom) . envContext . clEnv $ minfo
           (targettype, localVars) <- lift $ withMetaInfo minfo $ do
            vs <- getContextArgs
            targettype <- tt `piApplyM` permute (takeP (length vs) $ mvPermutation mv) vs
            targettype <- normalise targettype
            localVars <- mapM normalise localVars
            return (targettype, localVars)
           modify (\s -> s {sCurMeta = Just mi})
           typ' <- convert targettype
           ctx' <- mapM convert localVars
           modify (\s -> s {sCurMeta = Nothing})
           modify (\s -> s {sMetas = (Map.adjust (\(m, _, deps) -> (m, Just (typ', ctx'), deps)) mi (fst $ sMetas s), snd $ sMetas s)})
           r projfcns
          Nothing -> do
           nxt <- popMapS sEqs (\x y -> y {sEqs = x})
           case nxt of
            Just eqi -> do
             let (ineq, e, i) = eqs !! eqi
             e' <- convert e
             i' <- convert i
             modify (\s -> s {sEqs = (Map.adjust (\_ -> Just (ineq, e', i')) eqi (fst $ sEqs s), snd $ sEqs s)})
             r projfcns
            Nothing ->
             return projfcns
     ((icns', typs'), s) <- runStateT
      (do _ <- getMeta imi
          icns' <- mapM (\ (Hint iscon name) -> getConst iscon name TMAll) icns
          typs' <- mapM convert typs
          projfcns <- r []
          projfcns' <- mapM (\name -> getConst False name TMAll) projfcns
          [] <- r []
          return (projfcns' ++ icns', typs')
      ) (S {sConsts = initMapS, sMetas = initMapS, sEqs = initMapS, sCurMeta = Nothing, sMainMeta = imi})
     lift $ liftIO $ mapM_ categorizedecl icns'
     return (icns', typs', Map.map flatten (fst (sMetas s)), map fromJust $ Map.elems (fst (sEqs s)), fst (sConsts s))
     where
     flatten (x, Just (y, z), w) = (x, y, z, w)
     flatten (x, Nothing, w) = __IMPOSSIBLE__

     fromJust (Just x) = x
     fromJust Nothing = __IMPOSSIBLE__

    getConst :: Bool -> AN.QName -> TMode -> TOM (ConstRef O)
    getConst iscon name mode = do
     def <- lift $ getConstInfo name
     case MB.theDef def of
      MB.Record {MB.recConHead = con} -> do
       let conname = I.conName con
       cmap <- fst `liftM` gets sConsts
       case Map.lookup name cmap of
        Just (mode', c) ->
         if iscon then do
          cd <- lift $ liftIO $ readIORef c
          let Datatype [con] _ = cdcont cd
          return con
         else
          return c
        Nothing -> do
         mainm <- gets sMainMeta
         dfv <- lift $ getdfv mainm name
         let nomi = I.arity (MB.defType def)
         ccon <- lift $ liftIO $ newIORef (ConstDef {cdname = prettyShow name ++ ".CONS", cdorigin = (Just nomi, conname), cdtype = __IMPOSSIBLE__, cdcont = Constructor (nomi - dfv), cddeffreevars = dfv}) -- ?? correct value of deffreevars for records?
         c <- lift $ liftIO $ newIORef (ConstDef {cdname = prettyShow name, cdorigin = (Nothing, name), cdtype = __IMPOSSIBLE__, cdcont = Datatype [ccon] [], cddeffreevars = dfv}) -- ?? correct value of deffreevars for records?
         modify (\s -> s {sConsts = (Map.insert name (mode, c) cmap, name : snd (sConsts s))})
         return $ if iscon then ccon else c
      _ -> do
       cmap <- fst `liftM` gets sConsts
       case Map.lookup name cmap of
        Just (mode', c) ->
         return c
        Nothing -> do
         (miscon, sname) <- if iscon then do
           let MB.Constructor {MB.conPars = npar, MB.conData = dname} = MB.theDef def
           return (Just npar, prettyShow dname ++ "." ++ prettyShow (I.qnameName name))
          else
           return (Nothing, prettyShow name)
         mainm <- gets sMainMeta
         dfv <- lift $ getdfv mainm name
         c <- lift $ liftIO $ newIORef (ConstDef {cdname = sname, cdorigin = (miscon, name), cdtype = __IMPOSSIBLE__, cdcont = __IMPOSSIBLE__, cddeffreevars = dfv})
         modify (\s -> s {sConsts = (Map.insert name (mode, c) cmap, name : snd (sConsts s))})
         return c

    getdfv :: I.MetaId -> A.QName -> MB.TCM Cm.Nat
    getdfv mainm name = do
     mv <- lookupMeta mainm
     withMetaInfo (getMetaInfo mv) $ getDefFreeVars name

    getMeta :: I.MetaId -> TOM (Metavar (Exp O) (RefInfo O))
    getMeta name = do
     mmap <- fst `liftM` gets sMetas
     case Map.lookup name mmap of
      Just (m, _, _) ->
       return m
      Nothing -> do
       m <- lift $ liftIO initMeta
       modify (\s -> s {sMetas = (Map.insert name (m, Nothing, []) mmap, name : snd (sMetas s))})
       return m

    getEqs :: MB.TCM [(Bool, I.Term, I.Term)]
    getEqs = do
     eqs <- getAllConstraints
     let r = mapM (\eqc -> do
              neqc <- normalise eqc
              case MB.clValue $ MB.theConstraint neqc of
               MB.ValueCmp ineq _ i e -> do
                ei <- etaContract i
                ee <- etaContract e
                return [(tomyIneq ineq, ee, ei)]
               MB.TypeCmp ineq i e -> do
                I.El _ ei <- etaContract i
                I.El _ ee <- etaContract e
                return [(tomyIneq ineq, ee, ei)]
               MB.Guarded (MB.UnBlock _) pid -> return []
               _ -> return []
             )
     eqs' <- r eqs
     return $ concat eqs'

    copatternsNotImplemented :: MB.TCM a
    copatternsNotImplemented = MB.typeError $ MB.NotImplemented $
      "The Agda synthesizer (Agsy) does not support copatterns yet"

    literalsNotImplemented :: MB.TCM a
    literalsNotImplemented = MB.typeError $ MB.NotImplemented $
      "The Agda synthesizer (Agsy) does not support literals yet"

    hitsNotImplemented :: MB.TCM a
    hitsNotImplemented = MB.typeError $ MB.NotImplemented $
      "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 = fmap catMaybes . mapM convert

    instance Conversion TOM I.Clause (Maybe ([Pat O], MExp O)) where
      convert 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 = I.clauseBody cl
            pats = I.clausePats cl
        pats' <- mapM convert (IP.unnumberPatVars pats :: [Cm.Arg I.Pattern])
        body' <- traverse convert =<< lift (normalise body)
        return $ (pats',) <$> body'

    instance Conversion TOM (Cm.Arg I.Pattern) (Pat O) where
      convert p = case Cm.unArg p of
        I.IApplyP _ _ _ n  -> return $ PatVar (show n)
        I.VarP _ n  -> return $ PatVar (show n)
        I.DotP _ _  -> return $ PatVar "_"
          -- because Agda includes these when referring to variables in the body
        I.ConP con _ pats -> do
          let n = I.conName con
          c     <- getConst True n TMAll
          pats' <- mapM (convert . fmap Cm.namedThing) pats
          def   <- lift $ getConstInfo n
          cc    <- lift $ liftIO $ readIORef c
          let Just npar = fst $ cdorigin cc
          return $ PatConApp c (replicate npar PatExp ++ pats')

        -- UNSUPPORTED CASES
        I.ProjP{}   -> lift copatternsNotImplemented
        I.LitP _    -> lift literalsNotImplemented
        I.DefP{}    -> lift hitsNotImplemented

    instance Conversion TOM I.Type (MExp O) where
      convert (I.El _ t) = convert t -- sort info is thrown away

    instance Conversion TOM I.Term (MExp O) where
      convert v0 =
        case I.unSpine v0 of
          I.Var v es -> do
            let Just as = I.allApplyElims es
            as' <- convert as
            return $ NotM $ App Nothing (NotM OKVal) (Var v) as'
          I.Lam info b -> do
            b' <- convert (I.absBody b)
            return $ NotM $ Lam (getHiding info) (Abs (Id $ I.absName b) b')
          t@I.Lit{} -> do
            t <- lift $ constructorForm t
            case t of
              I.Lit{} -> lift literalsNotImplemented
              _       -> convert t
          I.Level l -> convert =<< lift (reallyUnLevelView l)
          I.Def name es -> do
            let Just as = I.allApplyElims es
            c   <- getConst False name TMAll
            as' <- convert as
            return $ NotM $ App Nothing (NotM OKVal) (Const c) as'
          I.Con con ci es -> do
            let Just as = I.allApplyElims es
            let name = I.conName con
            c   <- getConst True name TMAll
            as' <- convert as
            def <- lift $ getConstInfo name
            cc  <- lift $ liftIO $ readIORef c
            let Just npar = fst $ cdorigin cc
            return $ NotM $ App Nothing (NotM OKVal) (Const c) (foldl (\x _ -> NotM $ ALConPar x) as' [1..npar])
          I.Pi (Cm.Dom{domInfo = info, unDom = x}) b -> do
            let y    = I.absBody b
                name = I.absName b
            x' <- convert x
            y' <- convert y
            return $ NotM $ Pi Nothing (getHiding info) (Free.freeIn 0 y) x' (Abs (Id name) y')
          I.Sort (I.Type (I.Max [I.ClosedLevel l])) -> return $ NotM $ Sort $ Set $ fromIntegral l
          I.Sort _ -> return $ NotM $ Sort UnknownSort
          I.Dummy{}-> return $ NotM $ Sort UnknownSort
          t@I.MetaV{} -> do
            t <- lift $ instantiate t
            case t of
              I.MetaV mid _ -> do
                mcurmeta <- gets sCurMeta
                case mcurmeta of
                  Nothing -> return ()
                  Just curmeta ->
                    modify $ \ s -> s { sMetas = ( Map.adjust (\(m, x, deps) -> (m, x, mid : deps)) curmeta (fst $ sMetas s)
                                               , snd $ sMetas s
                                               ) }
                m <- getMeta mid
                return $ Meta m
              _ -> convert t
          I.DontCare _ -> return $ NotM dontCare

    instance Conversion TOM a b => Conversion TOM (Cm.Arg a) (Hiding, b) where
      convert (Cm.Arg info a) = (getHiding info,) <$> convert a

    instance Conversion TOM I.Args (MM (ArgList O) (RefInfo O)) where
      convert as = NotM . foldr (\ (hid,t) -> ALCons hid t . NotM) ALNil
                   <$> mapM convert as

    tomyIneq :: MB.Comparison -> Bool
    tomyIneq MB.CmpEq = False
    tomyIneq MB.CmpLeq = True

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

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

    fmExp :: I.MetaId -> I.Term -> Bool
    fmExp m (I.Var _ as) = fmExps m $ I.argsFromElims as
    fmExp m (I.Lam _ b) = fmExp m (I.unAbs b)
    fmExp m (I.Lit _) = False
    fmExp m (I.Level (I.Max as)) = any (fmLevel m) as
    fmExp m (I.Def _ as) = fmExps m $ I.argsFromElims as
    fmExp m (I.Con _ ci as) = fmExps m $ I.argsFromElims as
    fmExp m (I.Pi x y)  = fmType m (Cm.unDom x) || fmType m (I.unAbs y)
    fmExp m (I.Sort _) = False
    fmExp m (I.MetaV mid _) = mid == m
    fmExp m (I.DontCare _) = False
    fmExp _ I.Dummy{} = False

    fmExps :: I.MetaId -> I.Args -> Bool
    fmExps m [] = False
    fmExps m (a : as) = fmExp m (Cm.unArg a) || fmExps m as

    fmLevel :: I.MetaId -> I.PlusLevel -> Bool
    fmLevel m I.ClosedLevel{} = False
    fmLevel m (I.Plus _ l) = case l of
      I.MetaLevel m' _   -> m == m'
      I.NeutralLevel _ v -> fmExp m v
      I.BlockedLevel _ v -> fmExp m v
      I.UnreducedLevel v -> fmExp m v

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

    icnvh :: Hiding -> Cm.ArgInfo
    icnvh h = Cm.setHiding h $
              Cm.setOrigin o $
              Cm.defaultArgInfo
        where
        -- Andreas, 2017-01-18, issue #819.
        -- Visible arguments are made UserWritten,
        -- otherwise they might not be printed in patterns.
        o = case h of
              NotHidden  -> Cm.UserWritten
              Instance{} -> Cm.Inserted
              Hidden     -> Cm.Inserted

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

    instance Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b where
      convert meta = case meta of
        NotM a -> convert a
        Meta m -> do
          ma <- lift $ readIORef $ mbind m
          case ma of
            Nothing -> throwError "meta not bound"
            Just a  -> convert a

    instance Conversion MOT a b => Conversion MOT (Abs a) (I.Abs b) where
      convert (Abs mid t) = I.Abs id <$> convert t where
        id = case mid of
               NoId  -> "x"
               Id id -> id

    instance Conversion MOT (Exp O) I.Type where
      convert e = I.El (I.mkType 0) <$> convert e
                  -- 0 is arbitrary, sort not read by Agda when reifying

    instance Conversion MOT (Exp O) I.Term where
      convert e = case e of
        App _ _ (Var v) as -> frommyExps 0 as (I.Var v [])
        App _ _ (Const c) as -> do
          cdef <- lift $ readIORef c
          let (iscon, name) = cdorigin cdef
    {-
       case iscon of
          Just n -> do
            v <- getConTerm name -- We are not in TCM
            frommyExps n as v
    -}
              (ndrop, h) = case iscon of
                             Just n -> (n, \ q -> I.Con (I.ConHead q Cm.Inductive []) Cm.ConOSystem) -- TODO: restore fields
                             Nothing -> (0, \ f vs -> I.Def f vs)
          frommyExps ndrop as (h name [])
        Lam hid t -> I.Lam (icnvh hid) <$> convert t
        Pi _ hid _ x y -> do
          x' <- convert x
          let dom = (Cm.defaultDom x') {domInfo = icnvh hid}
          I.Pi dom <$> convert 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 l) -> return $ I.Sort (I.mkType (fromIntegral l))
        Sort Type -> __IMPOSSIBLE__
        Sort UnknownSort -> return $ I.Sort (I.mkType 0) -- hoping it's thrown away

        AbsurdLambda hid -> return $ I.Lam (icnvh hid)
                                   $ I.Abs abslamvarname (I.Var 0 [])

    frommyExps :: Nat -> MArgList O -> I.Term -> ExceptT String IO I.Term
    frommyExps ndrop (Meta m) trm = do
     bind <- lift $ readIORef $ mbind m
     case bind of
      Nothing -> throwError "meta not bound"
      Just e -> frommyExps ndrop (NotM e) trm
    frommyExps ndrop (NotM as) trm =
     case as of
      ALNil -> return trm
      ALCons _ _ xs | ndrop > 0 -> frommyExps (ndrop - 1) xs trm
      ALCons hid x xs -> do
       x' <- convert x
       frommyExps ndrop xs (addend (Cm.Arg (icnvh hid) x') trm)

      -- Andreas, 2013-10-19 TODO: restore postfix projections
      ALProj eas idx hid xs -> do
       idx <- lift $ expandbind idx
       c <- case idx of
                NotM c -> return c
                Meta{} -> throwError "meta not bound"
       cdef <- lift $ readIORef c
       let name = snd $ cdorigin cdef
       trm2 <- frommyExps 0 eas (I.Def name [])
       frommyExps 0 xs (addend (Cm.Arg (icnvh hid) trm) trm2)

      ALConPar xs | ndrop > 0 -> frommyExps (ndrop - 1) xs trm
      ALConPar _ -> __IMPOSSIBLE__
     where
      addend x (I.Var h xs) = I.Var h (xs ++ [I.Apply x])
      addend x (I.Con h ci xs) = I.Con h ci (xs ++ [I.Apply x])
      addend x (I.Def h xs) = I.Def h (xs ++ [I.Apply x])
      addend _ _ = __IMPOSSIBLE__

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

    abslamvarname :: String
    abslamvarname = "\0absurdlambda"

    modifyAbstractExpr :: A.Expr -> A.Expr
    modifyAbstractExpr = f
     where
      f (A.App i e1 (Cm.Arg info (Cm.Named n e2))) =
            A.App i (f e1) (Cm.Arg info (Cm.Named n (f e2)))
      f (A.Lam i (A.DomainFree x) _)
         | A.BindName n <- Cm.namedArg x
         , prettyShow (A.nameConcrete n) == abslamvarname =
            A.AbsurdLam i $ Cm.getHiding x
      f (A.Lam i b e) = A.Lam i b (f e)
      f (A.Rec i xs) = A.Rec i (map (mapLeft (over exprFieldA f)) xs)
      f (A.RecUpdate i e xs) = A.RecUpdate i (f e) (map (over exprFieldA f) xs)
      f (A.ScopedExpr i e) = A.ScopedExpr i (f e)
      f e = e

    modifyAbstractClause :: A.Clause -> A.Clause
    modifyAbstractClause (A.Clause lhs spats (A.RHS e mc) decls catchall) =
      A.Clause lhs spats (A.RHS (modifyAbstractExpr e) mc) decls catchall
    modifyAbstractClause cl = cl

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

    constructPats :: Map AN.QName (TMode, ConstRef O) -> I.MetaId -> I.Clause -> MB.TCM ([(Hiding, MId)], [CSPat O])
    constructPats cmap mainm clause = do
     let cnvps ns [] = return (ns, [])
         cnvps ns (p : ps) = do
          (ns', ps') <- cnvps ns ps
          (ns'', p') <- cnvp ns' p
          return (ns'', p' : ps')
         cnvp ns p =
          let hid = getHiding $ Cm.argInfo p
          in case Cm.namedArg p of
           I.VarP _ n -> return ((hid, Id n) : ns, HI hid (CSPatVar $ length ns))
           I.IApplyP _ _ _ n -> return ((hid, Id n) : ns, HI hid (CSPatVar $ length ns))
           I.ConP con _ ps -> do
            let c = I.conName con
            (c2, _) <- runStateT (getConst True c TMAll) (S {sConsts = (cmap, []), sMetas = initMapS, sEqs = initMapS, sCurMeta = Nothing, sMainMeta = mainm})
            (ns', ps') <- cnvps ns ps
            cc <- liftIO $ readIORef c2
            let Just npar = fst $ cdorigin cc
            return (ns', HI hid (CSPatConApp c2 (replicate npar (HI Hidden CSOmittedArg) ++ ps')))
           I.DotP _ t -> do
            (t2, _) <- runStateT (convert t) (S {sConsts = (cmap, []), sMetas = initMapS, sEqs = initMapS, sCurMeta = Nothing, sMainMeta = mainm})
            return (ns, HI hid (CSPatExp t2))
           I.ProjP{} -> copatternsNotImplemented
           I.LitP{} -> literalsNotImplemented
           I.DefP{} -> hitsNotImplemented

     (names, pats) <- cnvps [] (IP.unnumberPatVars $ I.namedClausePats clause)
     return (reverse names, pats)

    frommyClause :: (CSCtx O, [CSPat O], Maybe (MExp O)) -> ExceptT String IO I.Clause
    frommyClause (ids, pats, mrhs) = do
     let ctel [] = return I.EmptyTel
         ctel (HI hid (mid, t) : ctx) = do
          let Id id = mid
          tel <- ctel ctx
          t' <- convert t
          let dom = (Cm.defaultDom t') {domInfo = icnvh hid}
          return $ I.ExtendTel dom (I.Abs id tel)
     tel <- ctel $ reverse ids
     let getperms 0 [] perm nv = return (perm, nv)
         getperms n [] _ _ = __IMPOSSIBLE__
         getperms 0 (p : ps) perm nv = do
          (perm, nv) <- getperm p perm nv
          getperms 0 ps perm nv
         getperms n (HI _ CSPatExp{} : ps) perm nv = getperms (n - 1) ps perm nv
         getperms n (HI _ CSOmittedArg{} : ps) perm nv = getperms (n - 1) ps perm nv
         getperms n (_ : _) _ _ = __IMPOSSIBLE__
         getperm (HI _ p) perm nv =
          case p of
           --CSPatVar v -> return (length ids + nv - 1 - v : perm, nv)
           CSPatVar v -> return ((length ids - 1 - v, nv) : perm, nv + 1)
           CSPatConApp c ps -> do
            cdef <- lift $ readIORef c
            let (Just ndrop, _) = cdorigin cdef
            getperms ndrop ps perm nv
           CSPatExp e -> return (perm, nv + 1)
           _ -> __IMPOSSIBLE__
     (rperm, nv) <- getperms 0 pats [] 0
     let --perm = reverse rperm
         perm = map (\i -> let Just x = lookup i rperm in x) [0..length ids - 1]
         --renperm = map (\i -> length ids + nv - 1 - i) rperm
         --renm = rename (\i -> renperm !! i)
         cnvps 0 [] = return []
         cnvps n [] = __IMPOSSIBLE__
         cnvps 0 (p : ps) = do
          p' <- cnvp p
          ps' <- cnvps 0 ps
          return (p' : ps')
         cnvps n (HI _ CSPatExp{} : ps) = cnvps (n - 1) ps
         cnvps n (HI _ CSOmittedArg{} : ps) = cnvps (n - 1) ps
         cnvps n (_ : _) = __IMPOSSIBLE__
         cnvp (HI hid p) = do
          p' <- case p of
           CSPatVar v -> return (I.varP $ let HI _ (Id n, _) = ids !! v in n)
           CSPatConApp c ps -> do
            cdef <- lift $ readIORef c
            let (Just ndrop, name) = cdorigin cdef
            ps' <- cnvps ndrop ps
            let con = I.ConHead name Cm.Inductive [] -- TODO: restore record fields!
            return (I.ConP con I.noConPatternInfo ps')
           CSPatExp e -> do
            e' <- convert e {- renm e -} -- renaming before adding to clause below
            return (I.dotP e')
           CSAbsurd -> __IMPOSSIBLE__ -- CSAbsurd not used
           _ -> __IMPOSSIBLE__
          return $ Cm.Arg (icnvh hid) $ Cm.unnamed p'   -- TODO: recover names
     ps <- cnvps 0 pats
     body <- case mrhs of
              Nothing -> return $ Nothing
              Just e -> Just <$> convert e
     let cperm =  Perm nv perm
     return $ I.Clause
       { I.clauseLHSRange  = SP.noRange
       , I.clauseFullRange = SP.noRange
       , I.clauseTel       = tel
       , I.namedClausePats = IP.numberPatVars __IMPOSSIBLE__ cperm $ applySubst (renamingR $ compactP cperm) ps
       , I.clauseBody  = body
       , I.clauseType  = Nothing -- TODO: compute clause type
       , I.clauseCatchall = False
       , I.clauseUnreachable = Nothing -- TODO: Don't know here whether reachable or not !?
       }

    contains_constructor :: [CSPat O] -> Bool
    contains_constructor = any f
     where
      f (HI _ p) = case p of
             CSPatConApp{} -> True
             _ -> False

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

    freeIn :: Nat -> MExp o -> Bool
    freeIn = f
     where
      mr x = let NotM x' = x in x'
      f v e = case mr e of
       App _ _ elr args -> case elr of
        Var v' | v' == v -> False
        _ -> fs v args
       Lam _ (Abs _ b) -> f (v + 1) b
       Pi _ _ _ it (Abs _ ot) -> f v it && f (v + 1) ot
       Sort{} -> True

       AbsurdLambda{} -> True

      fs v es = case mr es of
       ALNil -> True
       ALCons _ a as -> f v a && fs v as

       ALProj{} -> __IMPOSSIBLE__

       ALConPar as -> fs v as

    negtype :: ConstRef o -> MExp o -> MExp o
    negtype ee = f (0 :: Int)
     where
      mr x = let NotM x' = x in x'
      f n e = case mr e of
       Pi uid hid possdep it (Abs id ot) -> NotM $ Pi uid hid possdep it (Abs id (f (n + 1) ot))
       _ -> NotM $ Pi Nothing NotHidden False (NotM $ Pi Nothing NotHidden False e (Abs NoId (NotM $ Pi Nothing NotHidden True (NotM $ Sort (Set 0)) (Abs NoId (NotM $ App Nothing (NotM OKVal) (Var 0) (NotM ALNil)))))) (Abs NoId (NotM $ App Nothing (NotM OKVal) (Const ee) (NotM ALNil)))

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

    findClauseDeep :: Cm.InteractionId -> MB.TCM (Maybe (AN.QName, I.Clause, Bool))
    findClauseDeep ii = ignoreAbstractMode $ do  -- Andreas, 2016-09-04, issue #2162
      MB.InteractionPoint { MB.ipClause = ipCl} <- lookupInteractionPoint ii
      case ipCl of
        MB.IPNoClause -> return Nothing
        MB.IPClause f clauseNo _ -> do
          (_, (_, c, _)) <- getClauseZipperForIP f clauseNo
          return $ Just (f, c, maybe __IMPOSSIBLE__ toplevel $ I.clauseBody c)
      where
        toplevel e =
         case e of
          I.MetaV{} -> True
          _ -> 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 cdfv tctx ctyp ttyp = trmodps cdfv ctyp
     where
      trmodps 0 ctyp = tr 0 0 ctyp
      trmodps n ctyp = case I.unEl ctyp of
       I.Pi _ ot -> trmodps (n - 1) (I.absBody ot)
       _ -> __IMPOSSIBLE__
      tr narg na ctyp =
       case ft 0 0 Just ctyp ttyp of
        Just n -> Just (n, narg)
        Nothing -> case I.unEl ctyp of
         I.Pi _ (I.Abs _ ot) -> tr (narg + 1) (na + 1) ot
         I.Pi _ (I.NoAbs _ ot) -> tr (narg + 1) na ot
         _ -> Nothing
       where
        ft nl n c (I.El _ e1) (I.El _ e2) = f nl n c e1 e2
        f nl n c e1 e2 = case e1 of
         I.Var v1 as1 | v1 < nl -> case e2 of
          I.Var v2 as2 | v1 == v2 -> fes nl (n + 1) c as1 as2
          _ -> Nothing
         I.Var v1 _ | v1 < nl + na -> c n -- unify vars with no args?
         I.Var v1 as1 -> case e2 of
          I.Var v2 as2 | cdfv + na + nl - v1 == tctx + nl - v2 -> fes nl (n + 1) c as1 as2
          _ -> Nothing
         _ -> case (e1, e2) of
          (I.MetaV{}, _) -> c n
          (_, I.MetaV{}) -> c n
          (I.Lam hid1 b1, I.Lam hid2 b2) | hid1 == hid2 -> f (nl + 1) n c (I.absBody b1) (I.absBody b2)
          (I.Lit lit1, I.Lit lit2) | lit1 == lit2 -> c (n + 1)
          (I.Def n1 as1, I.Def n2 as2) | n1 == n2 -> fes nl (n + 1) c as1 as2
          (I.Con n1 _ as1, I.Con n2 _ as2) | n1 == n2 -> fs nl (n + 1) c as1 as2
          (I.Pi (Cm.Dom{domInfo = info1, unDom = it1})  ot1, I.Pi (Cm.Dom{domInfo = info2, unDom = it2})  ot2) | Cm.argInfoHiding info1 == Cm.argInfoHiding info2 -> ft nl n (\n -> ft (nl + 1) n c (I.absBody ot1) (I.absBody ot2)) it1 it2
          (I.Sort{}, I.Sort{}) -> c n -- sloppy
          _ -> Nothing
        fs nl n c es1 es2 = case (es1, es2) of
         ([], []) -> c n
         (I.Apply (Cm.Arg info1 e1) : es1, I.Apply (Cm.Arg info2 e2) : es2) | Cm.argInfoHiding info1 == Cm.argInfoHiding info2 -> f nl n (\n -> fs nl n c es1 es2) e1 e2
         _ -> Nothing
        fes nl n c es1 es2 = case (es1, es2) of
         ([], []) -> c n
         (I.Proj _ f : es1, I.Proj _ f' : es2) | f == f' -> fes nl n c es1 es2
         (I.Apply (Cm.Arg info1 e1) : es1, I.Apply (Cm.Arg info2 e2) : es2) | Cm.argInfoHiding info1 == Cm.argInfoHiding info2 -> f nl n (\n -> fes nl n c es1 es2) e1 e2
         _ -> Nothing