{-# LANGUAGE CPP #-}

{-# OPTIONS_GHC -Wunused-imports #-}
{-# OPTIONS_GHC -Wno-orphans #-}
#if __GLASGOW_HASKELL__ > 907
{-# OPTIONS_GHC -Wno-x-partial #-}
#endif



module Agda.Auto.SearchControl where

import Control.Monad
import Data.IORef
import Control.Monad.State
import Data.Maybe (mapMaybe, fromMaybe)

import Agda.Syntax.Common (Hiding(..))
import Agda.Auto.NarrowingSearch
import Agda.Auto.Syntax

import Agda.Utils.Impossible

instance Refinable (ArgList o) (RefInfo o) where
 refinements :: RefInfo o
-> [RefInfo o]
-> Metavar (ArgList o) (RefInfo o)
-> IO [Move' (RefInfo o) (ArgList o)]
refinements RefInfo o
_ [RefInfo o]
infos Metavar (ArgList o) (RefInfo o)
_ = [Move' (RefInfo o) (ArgList o)]
-> IO [Move' (RefInfo o) (ArgList o)]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Move' (RefInfo o) (ArgList o)]
 -> IO [Move' (RefInfo o) (ArgList o)])
-> [Move' (RefInfo o) (ArgList o)]
-> IO [Move' (RefInfo o) (ArgList o)]
forall a b. (a -> b) -> a -> b
$ (RefCreateEnv (RefInfo o) (ArgList o)
 -> Move' (RefInfo o) (ArgList o))
-> [RefCreateEnv (RefInfo o) (ArgList o)]
-> [Move' (RefInfo o) (ArgList o)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Cost
-> RefCreateEnv (RefInfo o) (ArgList o)
-> Move' (RefInfo o) (ArgList o)
forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
0) ([RefCreateEnv (RefInfo o) (ArgList o)]
 -> [Move' (RefInfo o) (ArgList o)])
-> [RefCreateEnv (RefInfo o) (ArgList o)]
-> [Move' (RefInfo o) (ArgList o)]
forall a b. (a -> b) -> a -> b
$
   [ ArgList o -> RefCreateEnv (RefInfo o) (ArgList o)
forall a. a -> RefCreateEnv (RefInfo o) a
forall (m :: * -> *) a. Monad m => a -> m a
return ArgList o
forall o. ArgList o
ALNil, Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
cons Hiding
NotHidden, Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
cons Hiding
Hidden ]
   [RefCreateEnv (RefInfo o) (ArgList o)]
-> [RefCreateEnv (RefInfo o) (ArgList o)]
-> [RefCreateEnv (RefInfo o) (ArgList o)]
forall a. [a] -> [a] -> [a]
++ if [RefInfo o] -> Bool
getIsDep [RefInfo o]
infos then []
      else [ Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
proj Hiding
NotHidden, Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
proj Hiding
Hidden ]

   where

    getIsDep :: [RefInfo o] -> Bool
    getIsDep :: [RefInfo o] -> Bool
getIsDep (RefInfo o
x : [RefInfo o]
xs) = case RefInfo o
x of
      RICheckElim Bool
isDep -> Bool
isDep
      RefInfo o
_                 -> [RefInfo o] -> Bool
getIsDep [RefInfo o]
xs
    getIsDep [RefInfo o]
_ = Bool
forall a. HasCallStack => a
__IMPOSSIBLE__

    proj :: Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
    proj :: Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
proj Hiding
hid = MArgList o
-> MM (ConstRef o) (RefInfo o) -> Hiding -> MArgList o -> ArgList o
forall o.
MArgList o
-> MM (ConstRef o) (RefInfo o) -> Hiding -> MArgList o -> ArgList o
ALProj (MArgList o
 -> MM (ConstRef o) (RefInfo o)
 -> Hiding
 -> MArgList o
 -> ArgList o)
-> RefCreateEnv (RefInfo o) (MArgList o)
-> RefCreateEnv
     (RefInfo o)
     (MM (ConstRef o) (RefInfo o) -> Hiding -> MArgList o -> ArgList o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RefCreateEnv (RefInfo o) (MArgList o)
forall blk a. RefCreateEnv blk (MM a blk)
newPlaceholder RefCreateEnv
  (RefInfo o)
  (MM (ConstRef o) (RefInfo o) -> Hiding -> MArgList o -> ArgList o)
-> RefCreateEnv (RefInfo o) (MM (ConstRef o) (RefInfo o))
-> RefCreateEnv (RefInfo o) (Hiding -> MArgList o -> ArgList o)
forall a b.
RefCreateEnv (RefInfo o) (a -> b)
-> RefCreateEnv (RefInfo o) a -> RefCreateEnv (RefInfo o) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RefCreateEnv (RefInfo o) (MM (ConstRef o) (RefInfo o))
forall blk a. RefCreateEnv blk (MM a blk)
newPlaceholder
                      RefCreateEnv (RefInfo o) (Hiding -> MArgList o -> ArgList o)
-> RefCreateEnv (RefInfo o) Hiding
-> RefCreateEnv (RefInfo o) (MArgList o -> ArgList o)
forall a b.
RefCreateEnv (RefInfo o) (a -> b)
-> RefCreateEnv (RefInfo o) a -> RefCreateEnv (RefInfo o) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Hiding -> RefCreateEnv (RefInfo o) Hiding
forall a. a -> RefCreateEnv (RefInfo o) a
forall (m :: * -> *) a. Monad m => a -> m a
return Hiding
hid     RefCreateEnv (RefInfo o) (MArgList o -> ArgList o)
-> RefCreateEnv (RefInfo o) (MArgList o)
-> RefCreateEnv (RefInfo o) (ArgList o)
forall a b.
RefCreateEnv (RefInfo o) (a -> b)
-> RefCreateEnv (RefInfo o) a -> RefCreateEnv (RefInfo o) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RefCreateEnv (RefInfo o) (MArgList o)
forall blk a. RefCreateEnv blk (MM a blk)
newPlaceholder

    cons :: Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
    cons :: Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
cons Hiding
hid = Hiding -> MExp o -> MArgList o -> ArgList o
forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
hid (MExp o -> MArgList o -> ArgList o)
-> RefCreateEnv (RefInfo o) (MExp o)
-> RefCreateEnv (RefInfo o) (MArgList o -> ArgList o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RefCreateEnv (RefInfo o) (MExp o)
forall blk a. RefCreateEnv blk (MM a blk)
newPlaceholder RefCreateEnv (RefInfo o) (MArgList o -> ArgList o)
-> RefCreateEnv (RefInfo o) (MArgList o)
-> RefCreateEnv (RefInfo o) (ArgList o)
forall a b.
RefCreateEnv (RefInfo o) (a -> b)
-> RefCreateEnv (RefInfo o) a -> RefCreateEnv (RefInfo o) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RefCreateEnv (RefInfo o) (MArgList o)
forall blk a. RefCreateEnv blk (MM a blk)
newPlaceholder


data ExpRefInfo o = ExpRefInfo
  { forall o. ExpRefInfo o -> Maybe (RefInfo o)
eriMain           :: Maybe (RefInfo o)
  , forall o. ExpRefInfo o -> [RefInfo o]
eriUnifs          :: [RefInfo o]
  , forall o. ExpRefInfo o -> Bool
eriInfTypeUnknown :: Bool
  , forall o. ExpRefInfo o -> Bool
eriIsEliminand    :: Bool
  , forall o. ExpRefInfo o -> Maybe ([UId o], [Elr o])
eriUsedVars       :: Maybe ([UId o], [Elr o])
  , forall o. ExpRefInfo o -> Maybe Bool
eriIotaStep       :: Maybe Bool
  , forall o. ExpRefInfo o -> Bool
eriPickSubsVar    :: Bool
  , forall o. ExpRefInfo o -> Maybe EqReasoningState
eriEqRState       :: Maybe EqReasoningState
  }

initExpRefInfo :: ExpRefInfo o
initExpRefInfo :: forall o. ExpRefInfo o
initExpRefInfo = ExpRefInfo
  { eriMain :: Maybe (RefInfo o)
eriMain           = Maybe (RefInfo o)
forall a. Maybe a
Nothing
  , eriUnifs :: [RefInfo o]
eriUnifs          = []
  , eriInfTypeUnknown :: Bool
eriInfTypeUnknown = Bool
False
  , eriIsEliminand :: Bool
eriIsEliminand    = Bool
False
  , eriUsedVars :: Maybe ([UId o], [Elr o])
eriUsedVars       = Maybe ([UId o], [Elr o])
forall a. Maybe a
Nothing
  , eriIotaStep :: Maybe Bool
eriIotaStep       = Maybe Bool
forall a. Maybe a
Nothing
  , eriPickSubsVar :: Bool
eriPickSubsVar    = Bool
False
  , eriEqRState :: Maybe EqReasoningState
eriEqRState       = Maybe EqReasoningState
forall a. Maybe a
Nothing
  }

getinfo :: [RefInfo o] -> ExpRefInfo o
getinfo :: forall o. [RefInfo o] -> ExpRefInfo o
getinfo = (ExpRefInfo o -> RefInfo o -> ExpRefInfo o)
-> ExpRefInfo o -> [RefInfo o] -> ExpRefInfo o
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ExpRefInfo o -> RefInfo o -> ExpRefInfo o
forall o. ExpRefInfo o -> RefInfo o -> ExpRefInfo o
step ExpRefInfo o
forall o. ExpRefInfo o
initExpRefInfo where

  step :: ExpRefInfo o -> RefInfo o -> ExpRefInfo o
  step :: forall o. ExpRefInfo o -> RefInfo o -> ExpRefInfo o
step ExpRefInfo o
eri x :: RefInfo o
x@RIMainInfo{}           = ExpRefInfo o
eri { eriMain  = Just x }
  step ExpRefInfo o
eri x :: RefInfo o
x@RIUnifInfo{}           = ExpRefInfo o
eri { eriUnifs = x : eriUnifs eri }
  step ExpRefInfo o
eri RefInfo o
RIInferredTypeUnknown    = ExpRefInfo o
eri { eriInfTypeUnknown = True }
  step ExpRefInfo o
eri RefInfo o
RINotConstructor         = ExpRefInfo o
eri { eriIsEliminand = True }
  step ExpRefInfo o
eri (RIUsedVars [UId o]
nuids [Elr o]
nused) = ExpRefInfo o
eri { eriUsedVars = Just (nuids, nused) }
  step ExpRefInfo o
eri (RIIotaStep Bool
semif)       = ExpRefInfo o
eri { eriIotaStep = Just iota' } where
    iota' :: Bool
iota' = Bool
semif Bool -> Bool -> Bool
|| (Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
==) (ExpRefInfo o -> Maybe Bool
forall o. ExpRefInfo o -> Maybe Bool
eriIotaStep ExpRefInfo o
eri)
  step ExpRefInfo o
eri RefInfo o
RIPickSubsvar            = ExpRefInfo o
eri { eriPickSubsVar = True }
  step ExpRefInfo o
eri (RIEqRState EqReasoningState
s)           = ExpRefInfo o
eri { eriEqRState = Just s }
  step ExpRefInfo o
eri RefInfo o
_ = ExpRefInfo o
forall a. HasCallStack => a
__IMPOSSIBLE__


-- | @univar sub v@ figures out what the name of @v@ "outside" of
--   the substitution @sub@ ought to be, if anything.

univar :: [CAction o] -> Nat -> Maybe Nat
univar :: forall o. [CAction o] -> Nat -> Maybe Nat
univar [CAction o]
cl Nat
v = [CAction o] -> Nat -> Nat -> Maybe Nat
forall o. [CAction o] -> Nat -> Nat -> Maybe Nat
getOutsideName [CAction o]
cl Nat
v Nat
0 where

  getOutsideName :: [CAction o] -> Nat -> Nat -> Maybe Nat
  -- @v@ is offset by @v'@ binders
  getOutsideName :: forall o. [CAction o] -> Nat -> Nat -> Maybe Nat
getOutsideName []            Nat
v Nat
v' = Nat -> Maybe Nat
forall a. a -> Maybe a
Just (Nat
v' Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
v)
  -- @v@ was introduced by the weakening: disappears
  getOutsideName (Weak Nat
n : [CAction o]
_)  Nat
v Nat
v' | Nat
v Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
n = Maybe Nat
forall a. Maybe a
Nothing
  -- @v@ was introduced before the weakening: strengthened
  getOutsideName (Weak Nat
n : [CAction o]
xs) Nat
v Nat
v' = [CAction o] -> Nat -> Nat -> Maybe Nat
forall o. [CAction o] -> Nat -> Nat -> Maybe Nat
getOutsideName [CAction o]
xs (Nat
v Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
n) Nat
v'
  -- Name of @v@ before the substitution was pushed in
  -- had to be offset by 1
  getOutsideName (Sub ICExp o
_  : [CAction o]
xs) Nat
v Nat
v' = [CAction o] -> Nat -> Nat -> Maybe Nat
forall o. [CAction o] -> Nat -> Nat -> Maybe Nat
getOutsideName [CAction o]
xs Nat
v (Nat
v' Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1)
  -- If this is the place where @v@ was bound, it used to
  -- be called 0 + offset of all the vars substituted for
  getOutsideName (CAction o
Skip   : [CAction o]
_)  Nat
0 Nat
v' = Nat -> Maybe Nat
forall a. a -> Maybe a
Just Nat
v'
  -- Going over a binder: de Bruijn name of @v@ decreased
  -- but offset increased
  getOutsideName (CAction o
Skip   : [CAction o]
xs) Nat
v Nat
v' = [CAction o] -> Nat -> Nat -> Maybe Nat
forall o. [CAction o] -> Nat -> Nat -> Maybe Nat
getOutsideName [CAction o]
xs (Nat
v Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) (Nat
v' Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1)

-- | List of the variables instantiated by the substitution
subsvars :: [CAction o] -> [Nat]
subsvars :: forall o. [CAction o] -> [Nat]
subsvars = Nat -> [CAction o] -> [Nat]
forall o. Nat -> [CAction o] -> [Nat]
f Nat
0 where

  f :: Nat -> [CAction o] -> [Nat]
  f :: forall o. Nat -> [CAction o] -> [Nat]
f Nat
n []            = []
  f Nat
n (Weak Nat
_ : [CAction o]
xs) = Nat -> [CAction o] -> [Nat]
forall o. Nat -> [CAction o] -> [Nat]
f Nat
n [CAction o]
xs -- why?
  f Nat
n (Sub ICExp o
_  : [CAction o]
xs) = Nat
n Nat -> [Nat] -> [Nat]
forall a. a -> [a] -> [a]
: Nat -> [CAction o] -> [Nat]
forall o. Nat -> [CAction o] -> [Nat]
f (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) [CAction o]
xs
  f Nat
n (CAction o
Skip   : [CAction o]
xs) = Nat -> [CAction o] -> [Nat]
forall o. Nat -> [CAction o] -> [Nat]
f (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ Nat
1) [CAction o]
xs

-- | Moves
--   A move is composed of a @Cost@ together with an action
--   computing the refined problem.

type Move o = Move' (RefInfo o) (Exp o)

-- | New constructors
--   Taking a step towards a solution consists in picking a
--   constructor and filling in the missing parts with
--   placeholders to be discharged later on.

newAbs :: MId -> RefCreateEnv blk (Abs (MM a blk))
newAbs :: forall blk a. MId -> RefCreateEnv blk (Abs (MM a blk))
newAbs MId
mid = MId -> MM a blk -> Abs (MM a blk)
forall a. MId -> a -> Abs a
Abs MId
mid (MM a blk -> Abs (MM a blk))
-> RefCreateEnv blk (MM a blk) -> RefCreateEnv blk (Abs (MM a blk))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RefCreateEnv blk (MM a blk)
forall blk a. RefCreateEnv blk (MM a blk)
newPlaceholder

newLam :: Hiding -> MId -> RefCreateEnv (RefInfo o) (Exp o)
newLam :: forall o. Hiding -> MId -> RefCreateEnv (RefInfo o) (Exp o)
newLam Hiding
hid MId
mid = Hiding -> Abs (MExp o) -> Exp o
forall o. Hiding -> Abs (MExp o) -> Exp o
Lam Hiding
hid (Abs (MExp o) -> Exp o)
-> RefCreateEnv (RefInfo o) (Abs (MExp o))
-> RefCreateEnv (RefInfo o) (Exp o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MId -> RefCreateEnv (RefInfo o) (Abs (MExp o))
forall blk a. MId -> RefCreateEnv blk (Abs (MM a blk))
newAbs MId
mid

newPi :: UId o -> Bool -> Hiding -> RefCreateEnv (RefInfo o) (Exp o)
newPi :: forall o.
UId o -> Bool -> Hiding -> RefCreateEnv (RefInfo o) (Exp o)
newPi UId o
uid Bool
dep Hiding
hid = Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
forall o.
Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
Pi (UId o -> Maybe (UId o)
forall a. a -> Maybe a
Just UId o
uid) Hiding
hid Bool
dep (MExp o -> Abs (MExp o) -> Exp o)
-> RefCreateEnv (RefInfo o) (MExp o)
-> RefCreateEnv (RefInfo o) (Abs (MExp o) -> Exp o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RefCreateEnv (RefInfo o) (MExp o)
forall blk a. RefCreateEnv blk (MM a blk)
newPlaceholder RefCreateEnv (RefInfo o) (Abs (MExp o) -> Exp o)
-> RefCreateEnv (RefInfo o) (Abs (MExp o))
-> RefCreateEnv (RefInfo o) (Exp o)
forall a b.
RefCreateEnv (RefInfo o) (a -> b)
-> RefCreateEnv (RefInfo o) a -> RefCreateEnv (RefInfo o) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> MId -> RefCreateEnv (RefInfo o) (Abs (MExp o))
forall blk a. MId -> RefCreateEnv blk (Abs (MM a blk))
newAbs MId
NoId

foldArgs :: [(Hiding, MExp o)] -> MArgList o
foldArgs :: forall o. [(Hiding, MExp o)] -> MArgList o
foldArgs = ((Hiding, MExp o) -> MArgList o -> MArgList o)
-> MArgList o -> [(Hiding, MExp o)] -> MArgList o
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (Hiding
h, MExp o
a) MArgList o
sp -> ArgList o -> MArgList o
forall a blk. a -> MM a blk
NotM (ArgList o -> MArgList o) -> ArgList o -> MArgList o
forall a b. (a -> b) -> a -> b
$ Hiding -> MExp o -> MArgList o -> ArgList o
forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
h MExp o
a MArgList o
sp) (ArgList o -> MArgList o
forall a blk. a -> MM a blk
NotM ArgList o
forall o. ArgList o
ALNil)

-- | New spine of arguments potentially using placeholders

newArgs' :: [Hiding] -> [MExp o] -> RefCreateEnv (RefInfo o) (MArgList o)
newArgs' :: forall o.
[Hiding] -> [MExp o] -> RefCreateEnv (RefInfo o) (MArgList o)
newArgs' [Hiding]
h [MExp o]
tms = [(Hiding, MExp o)] -> MArgList o
forall o. [(Hiding, MExp o)] -> MArgList o
foldArgs ([(Hiding, MExp o)] -> MArgList o)
-> ([MExp o] -> [(Hiding, MExp o)]) -> [MExp o] -> MArgList o
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Hiding] -> [MExp o] -> [(Hiding, MExp o)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Hiding]
h ([MExp o] -> [(Hiding, MExp o)])
-> ([MExp o] -> [MExp o]) -> [MExp o] -> [(Hiding, MExp o)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([MExp o] -> [MExp o] -> [MExp o]
forall a. [a] -> [a] -> [a]
++ [MExp o]
tms) ([MExp o] -> MArgList o)
-> RefCreateEnv (RefInfo o) [MExp o]
-> RefCreateEnv (RefInfo o) (MArgList o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Nat
-> RefCreateEnv (RefInfo o) (MExp o)
-> RefCreateEnv (RefInfo o) [MExp o]
forall (m :: * -> *) a. Applicative m => Nat -> m a -> m [a]
replicateM Nat
size RefCreateEnv (RefInfo o) (MExp o)
forall blk a. RefCreateEnv blk (MM a blk)
newPlaceholder
  where size :: Nat
size = [Hiding] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Hiding]
h Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- [MExp o] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [MExp o]
tms

newArgs :: [Hiding] -> RefCreateEnv (RefInfo o) (MArgList o)
newArgs :: forall o. [Hiding] -> RefCreateEnv (RefInfo o) (MArgList o)
newArgs [Hiding]
h = [Hiding] -> [MExp o] -> RefCreateEnv (RefInfo o) (MArgList o)
forall o.
[Hiding] -> [MExp o] -> RefCreateEnv (RefInfo o) (MArgList o)
newArgs' [Hiding]
h []

-- | New @App@lication node using a new spine of arguments
--   respecting the @Hiding@ annotation

newApp' :: UId o -> ConstRef o -> [Hiding] -> [MExp o] ->
           RefCreateEnv (RefInfo o) (Exp o)
newApp' :: forall o.
UId o
-> ConstRef o
-> [Hiding]
-> [MExp o]
-> RefCreateEnv (RefInfo o) (Exp o)
newApp' UId o
meta ConstRef o
cst [Hiding]
hds [MExp o]
tms =
  Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App (UId o -> Maybe (UId o)
forall a. a -> Maybe a
Just UId o
meta) (OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o)
-> RefCreateEnv (RefInfo o) (OKHandle (RefInfo o))
-> RefCreateEnv (RefInfo o) (Elr o -> MArgList o -> Exp o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RefCreateEnv (RefInfo o) (OKHandle (RefInfo o))
forall blk. RefCreateEnv blk (OKHandle blk)
newOKHandle RefCreateEnv (RefInfo o) (Elr o -> MArgList o -> Exp o)
-> RefCreateEnv (RefInfo o) (Elr o)
-> RefCreateEnv (RefInfo o) (MArgList o -> Exp o)
forall a b.
RefCreateEnv (RefInfo o) (a -> b)
-> RefCreateEnv (RefInfo o) a -> RefCreateEnv (RefInfo o) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Elr o -> RefCreateEnv (RefInfo o) (Elr o)
forall a. a -> RefCreateEnv (RefInfo o) a
forall (m :: * -> *) a. Monad m => a -> m a
return (ConstRef o -> Elr o
forall o. ConstRef o -> Elr o
Const ConstRef o
cst) RefCreateEnv (RefInfo o) (MArgList o -> Exp o)
-> RefCreateEnv (RefInfo o) (MArgList o)
-> RefCreateEnv (RefInfo o) (Exp o)
forall a b.
RefCreateEnv (RefInfo o) (a -> b)
-> RefCreateEnv (RefInfo o) a -> RefCreateEnv (RefInfo o) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Hiding] -> [MExp o] -> RefCreateEnv (RefInfo o) (MArgList o)
forall o.
[Hiding] -> [MExp o] -> RefCreateEnv (RefInfo o) (MArgList o)
newArgs' [Hiding]
hds [MExp o]
tms

newApp :: UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
newApp :: forall o.
UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
newApp UId o
meta ConstRef o
cst [Hiding]
hds = UId o
-> ConstRef o
-> [Hiding]
-> [MExp o]
-> RefCreateEnv (RefInfo o) (Exp o)
forall o.
UId o
-> ConstRef o
-> [Hiding]
-> [MExp o]
-> RefCreateEnv (RefInfo o) (Exp o)
newApp' UId o
meta ConstRef o
cst [Hiding]
hds []

-- | Equality reasoning steps
--   The begin token is accompanied by two steps because
--   it does not make sense to have a derivation any shorter
--   than that.

eqStep :: UId o -> EqReasoningConsts o -> Move o
eqStep :: forall o. UId o -> EqReasoningConsts o -> Move o
eqStep UId o
meta EqReasoningConsts o
eqrc = Cost
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
costEqStep (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall a b. (a -> b) -> a -> b
$ UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
forall o.
UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
newApp UId o
meta (EqReasoningConsts o -> ConstRef o
forall o. EqReasoningConsts o -> ConstRef o
eqrcStep EqReasoningConsts o
eqrc)
  [Hiding
Hidden, Hiding
Hidden, Hiding
NotHidden, Hiding
Hidden, Hiding
Hidden, Hiding
NotHidden, Hiding
NotHidden]

eqEnd :: UId o -> EqReasoningConsts o -> Move o
eqEnd :: forall o. UId o -> EqReasoningConsts o -> Move o
eqEnd UId o
meta EqReasoningConsts o
eqrc = Cost
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
costEqEnd (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall a b. (a -> b) -> a -> b
$ UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
forall o.
UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
newApp UId o
meta (EqReasoningConsts o -> ConstRef o
forall o. EqReasoningConsts o -> ConstRef o
eqrcEnd EqReasoningConsts o
eqrc)
  [Hiding
Hidden, Hiding
Hidden, Hiding
NotHidden]

eqCong :: UId o -> EqReasoningConsts o -> Move o
eqCong :: forall o. UId o -> EqReasoningConsts o -> Move o
eqCong UId o
meta EqReasoningConsts o
eqrc = Cost
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
costEqCong (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall a b. (a -> b) -> a -> b
$ UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
forall o.
UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
newApp UId o
meta (EqReasoningConsts o -> ConstRef o
forall o. EqReasoningConsts o -> ConstRef o
eqrcCong EqReasoningConsts o
eqrc)
  [Hiding
Hidden, Hiding
Hidden, Hiding
Hidden, Hiding
Hidden, Hiding
NotHidden, Hiding
Hidden, Hiding
Hidden, Hiding
NotHidden]

eqSym :: UId o -> EqReasoningConsts o -> Move o
eqSym :: forall o. UId o -> EqReasoningConsts o -> Move o
eqSym UId o
meta EqReasoningConsts o
eqrc = Cost
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
costEqSym (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall a b. (a -> b) -> a -> b
$ UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
forall o.
UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
newApp UId o
meta (EqReasoningConsts o -> ConstRef o
forall o. EqReasoningConsts o -> ConstRef o
eqrcSym EqReasoningConsts o
eqrc)
  [Hiding
Hidden, Hiding
Hidden, Hiding
Hidden, Hiding
Hidden, Hiding
NotHidden]

eqBeginStep2 :: UId o -> EqReasoningConsts o -> Move o
eqBeginStep2 :: forall o. UId o -> EqReasoningConsts o -> Move o
eqBeginStep2 UId o
meta EqReasoningConsts o
eqrc = Cost
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
costEqStep (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall a b. (a -> b) -> a -> b
$ do
  Exp o
e1 <- UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
forall o.
UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
newApp UId o
meta (EqReasoningConsts o -> ConstRef o
forall o. EqReasoningConsts o -> ConstRef o
eqrcStep EqReasoningConsts o
eqrc)
          [Hiding
Hidden, Hiding
Hidden, Hiding
NotHidden, Hiding
Hidden, Hiding
Hidden, Hiding
NotHidden, Hiding
NotHidden]
  Exp o
e2 <- UId o
-> ConstRef o
-> [Hiding]
-> [MExp o]
-> RefCreateEnv (RefInfo o) (Exp o)
forall o.
UId o
-> ConstRef o
-> [Hiding]
-> [MExp o]
-> RefCreateEnv (RefInfo o) (Exp o)
newApp' UId o
meta (EqReasoningConsts o -> ConstRef o
forall o. EqReasoningConsts o -> ConstRef o
eqrcStep EqReasoningConsts o
eqrc)
          [Hiding
Hidden, Hiding
Hidden, Hiding
NotHidden, Hiding
Hidden, Hiding
Hidden, Hiding
NotHidden, Hiding
NotHidden]
          [Exp o -> MExp o
forall a blk. a -> MM a blk
NotM Exp o
e1]
  UId o
-> ConstRef o
-> [Hiding]
-> [MExp o]
-> RefCreateEnv (RefInfo o) (Exp o)
forall o.
UId o
-> ConstRef o
-> [Hiding]
-> [MExp o]
-> RefCreateEnv (RefInfo o) (Exp o)
newApp' UId o
meta (EqReasoningConsts o -> ConstRef o
forall o. EqReasoningConsts o -> ConstRef o
eqrcBegin EqReasoningConsts o
eqrc) [Hiding
Hidden, Hiding
Hidden, Hiding
Hidden, Hiding
Hidden, Hiding
NotHidden]
    [Exp o -> MExp o
forall a blk. a -> MM a blk
NotM Exp o
e2]


-- | Pick the first unused UId amongst the ones you have seen (GA: ??)
--   Defaults to the head of the seen ones.

pickUid :: forall o. [UId o] -> [Maybe (UId o)] -> (Maybe (UId o), Bool)
pickUid :: forall o. [UId o] -> [Maybe (UId o)] -> (Maybe (UId o), Bool)
pickUid [UId o]
used [Maybe (UId o)]
seen = (Maybe (UId o), Bool)
-> (Maybe (UId o) -> (Maybe (UId o), Bool))
-> Maybe (Maybe (UId o))
-> (Maybe (UId o), Bool)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ([Maybe (UId o)] -> Maybe (UId o)
forall a. HasCallStack => [a] -> a
head [Maybe (UId o)]
seen, Bool
False) (, Bool
True) (Maybe (Maybe (UId o)) -> (Maybe (UId o), Bool))
-> Maybe (Maybe (UId o)) -> (Maybe (UId o), Bool)
forall a b. (a -> b) -> a -> b
$ [Maybe (UId o)] -> Maybe (Maybe (UId o))
firstUnused [Maybe (UId o)]
seen where
  {- ?? which uid to pick -}

  firstUnused :: [Maybe (UId o)] -> Maybe (Maybe (UId o))
  firstUnused :: [Maybe (UId o)] -> Maybe (Maybe (UId o))
firstUnused []                 = Maybe (Maybe (UId o))
forall a. Maybe a
Nothing
  firstUnused (Maybe (UId o)
Nothing     : [Maybe (UId o)]
_)  = Maybe (UId o) -> Maybe (Maybe (UId o))
forall a. a -> Maybe a
Just Maybe (UId o)
forall a. Maybe a
Nothing
  firstUnused (mu :: Maybe (UId o)
mu@(Just UId o
u) : [Maybe (UId o)]
us) =
    if UId o
u UId o -> [UId o] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [UId o]
used then [Maybe (UId o)] -> Maybe (Maybe (UId o))
firstUnused [Maybe (UId o)]
us else Maybe (UId o) -> Maybe (Maybe (UId o))
forall a. a -> Maybe a
Just Maybe (UId o)
mu

instance Refinable (Exp o) (RefInfo o) where
 refinements :: RefInfo o
-> [RefInfo o]
-> Metavar (Exp o) (RefInfo o)
-> IO [Move' (RefInfo o) (Exp o)]
refinements RefInfo o
envinfo [RefInfo o]
infos Metavar (Exp o) (RefInfo o)
meta =
  let
   hints :: [(ConstRef o, HintMode)]
hints = RefInfo o -> [(ConstRef o, HintMode)]
forall o. RefInfo o -> [(ConstRef o, HintMode)]
rieHints RefInfo o
envinfo
   deffreevars :: Nat
deffreevars = RefInfo o -> Nat
forall o. RefInfo o -> Nat
rieDefFreeVars RefInfo o
envinfo

   meqr :: Maybe (EqReasoningConsts o)
meqr = RefInfo o -> Maybe (EqReasoningConsts o)
forall o. RefInfo o -> Maybe (EqReasoningConsts o)
rieEqReasoningConsts RefInfo o
envinfo

   ExpRefInfo { eriMain :: forall o. ExpRefInfo o -> Maybe (RefInfo o)
eriMain  = Just (RIMainInfo Nat
n HNExp o
tt Bool
iotastepdone)
              , eriUnifs :: forall o. ExpRefInfo o -> [RefInfo o]
eriUnifs = [RefInfo o]
unis
              , eriInfTypeUnknown :: forall o. ExpRefInfo o -> Bool
eriInfTypeUnknown = Bool
inftypeunknown
              , eriIsEliminand :: forall o. ExpRefInfo o -> Bool
eriIsEliminand = Bool
iseliminand -- TODO:: Defined but not used
              , eriUsedVars :: forall o. ExpRefInfo o -> Maybe ([UId o], [Elr o])
eriUsedVars = Just ([Metavar (Exp o) (RefInfo o)]
uids, [Elr o]
usedvars)
              , eriIotaStep :: forall o. ExpRefInfo o -> Maybe Bool
eriIotaStep = Maybe Bool
iotastep
              , eriPickSubsVar :: forall o. ExpRefInfo o -> Bool
eriPickSubsVar = Bool
picksubsvar -- TODO:: Defined but not used
              , eriEqRState :: forall o. ExpRefInfo o -> Maybe EqReasoningState
eriEqRState = Maybe EqReasoningState
meqrstate
              } = [RefInfo o] -> ExpRefInfo o
forall o. [RefInfo o] -> ExpRefInfo o
getinfo [RefInfo o]
infos

   eqrstate :: EqReasoningState
eqrstate = EqReasoningState -> Maybe EqReasoningState -> EqReasoningState
forall a. a -> Maybe a -> a
fromMaybe EqReasoningState
EqRSNone Maybe EqReasoningState
meqrstate

   set :: Nat -> m (Exp o)
set Nat
l = Exp o -> m (Exp o)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp o -> m (Exp o)) -> Exp o -> m (Exp o)
forall a b. (a -> b) -> a -> b
$ Sort -> Exp o
forall o. Sort -> Exp o
Sort (Nat -> Sort
Set Nat
l)
  in case [RefInfo o]
unis of
   [] ->
    let

     eqr :: EqReasoningConsts o
eqr = EqReasoningConsts o
-> Maybe (EqReasoningConsts o) -> EqReasoningConsts o
forall a. a -> Maybe a -> a
fromMaybe EqReasoningConsts o
forall a. HasCallStack => a
__IMPOSSIBLE__ Maybe (EqReasoningConsts o)
meqr
     eq_end :: Move' (RefInfo o) (Exp o)
eq_end         = Metavar (Exp o) (RefInfo o)
-> EqReasoningConsts o -> Move' (RefInfo o) (Exp o)
forall o. UId o -> EqReasoningConsts o -> Move o
eqEnd  Metavar (Exp o) (RefInfo o)
meta EqReasoningConsts o
eqr
     eq_step :: Move' (RefInfo o) (Exp o)
eq_step        = Metavar (Exp o) (RefInfo o)
-> EqReasoningConsts o -> Move' (RefInfo o) (Exp o)
forall o. UId o -> EqReasoningConsts o -> Move o
eqStep Metavar (Exp o) (RefInfo o)
meta EqReasoningConsts o
eqr
     eq_cong :: Move' (RefInfo o) (Exp o)
eq_cong        = Metavar (Exp o) (RefInfo o)
-> EqReasoningConsts o -> Move' (RefInfo o) (Exp o)
forall o. UId o -> EqReasoningConsts o -> Move o
eqCong Metavar (Exp o) (RefInfo o)
meta EqReasoningConsts o
eqr
     eq_sym :: Move' (RefInfo o) (Exp o)
eq_sym         = Metavar (Exp o) (RefInfo o)
-> EqReasoningConsts o -> Move' (RefInfo o) (Exp o)
forall o. UId o -> EqReasoningConsts o -> Move o
eqSym  Metavar (Exp o) (RefInfo o)
meta EqReasoningConsts o
eqr
     eq_begin_step2 :: Move' (RefInfo o) (Exp o)
eq_begin_step2 = Metavar (Exp o) (RefInfo o)
-> EqReasoningConsts o -> Move' (RefInfo o) (Exp o)
forall o. UId o -> EqReasoningConsts o -> Move o
eqBeginStep2 Metavar (Exp o) (RefInfo o)
meta EqReasoningConsts o
eqr

     adjustCost :: Cost -> Cost
adjustCost Cost
i = if Bool
inftypeunknown then Cost
costInferredTypeUnkown else Cost
i
     varcost :: Nat -> Cost
varcost Nat
v | Nat
v Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
deffreevars = Cost -> Cost
adjustCost (Cost -> Cost) -> Cost -> Cost
forall a b. (a -> b) -> a -> b
$
       if Nat
v Nat -> [Nat] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Elr o -> Maybe Nat) -> [Elr o] -> [Nat]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Elr o -> Maybe Nat
forall o. Elr o -> Maybe Nat
getVar [Elr o]
usedvars)
       then Cost
costAppVarUsed else Cost
costAppVar
     varcost Nat
v | Bool
otherwise           = Cost -> Cost
adjustCost Cost
costAppHint
     varapps :: [Move' (RefInfo o) (Exp o)]
varapps  = (Nat -> Move' (RefInfo o) (Exp o))
-> [Nat] -> [Move' (RefInfo o) (Exp o)]
forall a b. (a -> b) -> [a] -> [b]
map (\ Nat
v -> Cost
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move (Nat -> Cost
varcost Nat
v) (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall a b. (a -> b) -> a -> b
$ Nat
-> Metavar (Exp o) (RefInfo o)
-> Maybe (Metavar (Exp o) (RefInfo o))
-> Elr o
-> RefCreateEnv (RefInfo o) (Exp o)
app Nat
n Metavar (Exp o) (RefInfo o)
meta Maybe (Metavar (Exp o) (RefInfo o))
forall a. Maybe a
Nothing (Nat -> Elr o
forall o. Nat -> Elr o
Var Nat
v)) [Nat
0..Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1]
     hintapps :: [Move' (RefInfo o) (Exp o)]
hintapps = ((ConstRef o, HintMode) -> Move' (RefInfo o) (Exp o))
-> [(ConstRef o, HintMode)] -> [Move' (RefInfo o) (Exp o)]
forall a b. (a -> b) -> [a] -> [b]
map (\(ConstRef o
c, HintMode
hm) -> Cost
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move (ConstRef o -> HintMode -> Cost
cost ConstRef o
c HintMode
hm) (Nat
-> Metavar (Exp o) (RefInfo o)
-> Maybe (Metavar (Exp o) (RefInfo o))
-> Elr o
-> RefCreateEnv (RefInfo o) (Exp o)
app Nat
n Metavar (Exp o) (RefInfo o)
meta Maybe (Metavar (Exp o) (RefInfo o))
forall a. Maybe a
Nothing (ConstRef o -> Elr o
forall o. ConstRef o -> Elr o
Const ConstRef o
c))) [(ConstRef o, HintMode)]
hints
       where
         cost :: ConstRef o -> HintMode -> Cost
         cost :: ConstRef o -> HintMode -> Cost
cost ConstRef o
c HintMode
hm = Cost -> Cost
adjustCost (Cost -> Cost) -> Cost -> Cost
forall a b. (a -> b) -> a -> b
$ case (Maybe Bool
iotastep , HintMode
hm) of
           (Just Bool
_  , HintMode
_       ) -> Cost
costIotaStep
           (Maybe Bool
Nothing , HintMode
HMNormal) ->
             if ConstRef o
c ConstRef o -> [ConstRef o] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Elr o -> Maybe (ConstRef o)) -> [Elr o] -> [ConstRef o]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Elr o -> Maybe (ConstRef o)
forall o. Elr o -> Maybe (ConstRef o)
getConst [Elr o]
usedvars)
             then Cost
costAppHintUsed else Cost
costAppHint
           (Maybe Bool
Nothing , HintMode
HMRecCall) ->
             if ConstRef o
c ConstRef o -> [ConstRef o] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Elr o -> Maybe (ConstRef o)) -> [Elr o] -> [ConstRef o]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Elr o -> Maybe (ConstRef o)
forall o. Elr o -> Maybe (ConstRef o)
getConst [Elr o]
usedvars)
             then Cost
costAppRecCallUsed else Cost
costAppRecCall
     generics :: [Move' (RefInfo o) (Exp o)]
generics = [Move' (RefInfo o) (Exp o)]
varapps [Move' (RefInfo o) (Exp o)]
-> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
forall a. [a] -> [a] -> [a]
++ [Move' (RefInfo o) (Exp o)]
hintapps
    in case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
tt of

     HNExp' o
_ | EqReasoningState
eqrstate EqReasoningState -> EqReasoningState -> Bool
forall a. Eq a => a -> a -> Bool
== EqReasoningState
EqRSChain ->
      [Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Move' (RefInfo o) (Exp o)
eq_end, Move' (RefInfo o) (Exp o)
eq_step]

     HNPi Hiding
hid Bool
_ ICExp o
_ (Abs MId
id ICExp o
_) -> [Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)])
-> [Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)]
forall a b. (a -> b) -> a -> b
$
         Cost
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move (Cost -> Cost
adjustCost (if Bool
iotastepdone then Cost
costLamUnfold else Cost
costLam)) (Hiding -> MId -> RefCreateEnv (RefInfo o) (Exp o)
forall o. Hiding -> MId -> RefCreateEnv (RefInfo o) (Exp o)
newLam Hiding
hid MId
id)
       Move' (RefInfo o) (Exp o)
-> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
forall a. a -> [a] -> [a]
: Cost
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
costAbsurdLam (Exp o -> RefCreateEnv (RefInfo o) (Exp o)
forall a. a -> RefCreateEnv (RefInfo o) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp o -> RefCreateEnv (RefInfo o) (Exp o))
-> Exp o -> RefCreateEnv (RefInfo o) (Exp o)
forall a b. (a -> b) -> a -> b
$ Hiding -> Exp o
forall o. Hiding -> Exp o
AbsurdLambda Hiding
hid)
       Move' (RefInfo o) (Exp o)
-> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
forall a. a -> [a] -> [a]
: [Move' (RefInfo o) (Exp o)]
generics

     HNSort (Set Nat
l) -> [Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)])
-> [Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)]
forall a b. (a -> b) -> a -> b
$
          (Nat -> Move' (RefInfo o) (Exp o))
-> [Nat] -> [Move' (RefInfo o) (Exp o)]
forall a b. (a -> b) -> [a] -> [b]
map (Cost
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move (Cost -> Cost
adjustCost Cost
costSort) (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
-> (Nat -> RefCreateEnv (RefInfo o) (Exp o))
-> Nat
-> Move' (RefInfo o) (Exp o)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> RefCreateEnv (RefInfo o) (Exp o)
forall {m :: * -> *} {o}. Monad m => Nat -> m (Exp o)
set) [Nat
0..Nat
l Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1]
       [Move' (RefInfo o) (Exp o)]
-> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
forall a. [a] -> [a] -> [a]
++ (Hiding -> Move' (RefInfo o) (Exp o))
-> [Hiding] -> [Move' (RefInfo o) (Exp o)]
forall a b. (a -> b) -> [a] -> [b]
map (Cost
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move (Cost -> Cost
adjustCost Cost
costPi) (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
-> (Hiding -> RefCreateEnv (RefInfo o) (Exp o))
-> Hiding
-> Move' (RefInfo o) (Exp o)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Metavar (Exp o) (RefInfo o)
-> Bool -> Hiding -> RefCreateEnv (RefInfo o) (Exp o)
forall o.
UId o -> Bool -> Hiding -> RefCreateEnv (RefInfo o) (Exp o)
newPi Metavar (Exp o) (RefInfo o)
meta Bool
True) [Hiding
NotHidden, Hiding
Hidden]
       [Move' (RefInfo o) (Exp o)]
-> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
forall a. [a] -> [a] -> [a]
++ [Move' (RefInfo o) (Exp o)]
generics


     HNApp (Const ConstRef o
c) ICArgList o
_ -> do
      ConstDef o
cd <- ConstRef o -> IO (ConstDef o)
forall a. IORef a -> IO a
readIORef ConstRef o
c
      [Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)])
-> [Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)]
forall a b. (a -> b) -> a -> b
$ case ConstDef o -> DeclCont o
forall o. ConstDef o -> DeclCont o
cdcont ConstDef o
cd of

       Datatype [ConstRef o]
cons [ConstRef o]
_ | EqReasoningState
eqrstate EqReasoningState -> EqReasoningState -> Bool
forall a. Eq a => a -> a -> Bool
== EqReasoningState
EqRSNone ->
         (ConstRef o -> Move' (RefInfo o) (Exp o))
-> [ConstRef o] -> [Move' (RefInfo o) (Exp o)]
forall a b. (a -> b) -> [a] -> [b]
map (\ConstRef o
c -> Cost
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move (Cost -> Cost
adjustCost (Cost -> Cost) -> Cost -> Cost
forall a b. (a -> b) -> a -> b
$ case Maybe Bool
iotastep of
                                         Just Bool
True -> Cost
costUnification
                                         Maybe Bool
_ -> if [ConstRef o] -> Nat
forall a. [a] -> Nat
forall (t :: * -> *) a. Foldable t => t a -> Nat
length [ConstRef o]
cons Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
<= Nat
1
                                              then Cost
costAppConstructorSingle
                                              else Cost
costAppConstructor)
                         (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall a b. (a -> b) -> a -> b
$ Nat
-> Metavar (Exp o) (RefInfo o)
-> Maybe (Metavar (Exp o) (RefInfo o))
-> Elr o
-> RefCreateEnv (RefInfo o) (Exp o)
app Nat
n Metavar (Exp o) (RefInfo o)
meta Maybe (Metavar (Exp o) (RefInfo o))
forall a. Maybe a
Nothing (ConstRef o -> Elr o
forall o. ConstRef o -> Elr o
Const ConstRef o
c)) [ConstRef o]
cons
         [Move' (RefInfo o) (Exp o)]
-> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
forall a. [a] -> [a] -> [a]
++ [Move' (RefInfo o) (Exp o)]
generics
         [Move' (RefInfo o) (Exp o)]
-> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
forall a. [a] -> [a] -> [a]
++ (Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool
-> (EqReasoningConsts o -> Bool)
-> Maybe (EqReasoningConsts o)
-> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ((ConstRef o
c ConstRef o -> ConstRef o -> Bool
forall a. Eq a => a -> a -> Bool
==) (ConstRef o -> Bool)
-> (EqReasoningConsts o -> ConstRef o)
-> EqReasoningConsts o
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EqReasoningConsts o -> ConstRef o
forall o. EqReasoningConsts o -> ConstRef o
eqrcId) Maybe (EqReasoningConsts o)
meqr)
            [()] -> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
forall a b. [a] -> [b] -> [b]
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> [Move' (RefInfo o) (Exp o)
eq_sym, Move' (RefInfo o) (Exp o)
eq_cong, Move' (RefInfo o) (Exp o)
eq_begin_step2])

       DeclCont o
_ | EqReasoningState
eqrstate EqReasoningState -> EqReasoningState -> Bool
forall a. Eq a => a -> a -> Bool
== EqReasoningState
EqRSPrf1 -> [Move' (RefInfo o) (Exp o)]
generics [Move' (RefInfo o) (Exp o)]
-> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
forall a. [a] -> [a] -> [a]
++ [Move' (RefInfo o) (Exp o)
eq_sym, Move' (RefInfo o) (Exp o)
eq_cong]
       DeclCont o
_ | EqReasoningState
eqrstate EqReasoningState -> EqReasoningState -> Bool
forall a. Eq a => a -> a -> Bool
== EqReasoningState
EqRSPrf2 -> [Move' (RefInfo o) (Exp o)]
generics [Move' (RefInfo o) (Exp o)]
-> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
forall a. [a] -> [a] -> [a]
++ [Move' (RefInfo o) (Exp o)
eq_cong]

       DeclCont o
_ -> [Move' (RefInfo o) (Exp o)]
generics
     HNExp' o
_ -> [Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Move' (RefInfo o) (Exp o)]
generics
   (RIUnifInfo [CAction o]
cl HNExp o
hne : [RefInfo o]
_) ->
    let
     subsvarapps :: [Move' (RefInfo o) (Exp o)]
subsvarapps = (Nat -> Move' (RefInfo o) (Exp o))
-> [Nat] -> [Move' (RefInfo o) (Exp o)]
forall a b. (a -> b) -> [a] -> [b]
map (Cost
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
costUnification (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
-> (Nat -> RefCreateEnv (RefInfo o) (Exp o))
-> Nat
-> Move' (RefInfo o) (Exp o)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat
-> Metavar (Exp o) (RefInfo o)
-> Maybe (Metavar (Exp o) (RefInfo o))
-> Elr o
-> RefCreateEnv (RefInfo o) (Exp o)
app Nat
n Metavar (Exp o) (RefInfo o)
meta Maybe (Metavar (Exp o) (RefInfo o))
forall a. Maybe a
Nothing (Elr o -> RefCreateEnv (RefInfo o) (Exp o))
-> (Nat -> Elr o) -> Nat -> RefCreateEnv (RefInfo o) (Exp o)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Elr o
forall o. Nat -> Elr o
Var) ([CAction o] -> [Nat]
forall o. [CAction o] -> [Nat]
subsvars [CAction o]
cl)
     mlam :: [Move' (RefInfo o) (Exp o)]
mlam = case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
tt of
      HNPi Hiding
hid Bool
_ ICExp o
_ (Abs MId
id ICExp o
_) -> [Cost
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
costUnification (Hiding -> MId -> RefCreateEnv (RefInfo o) (Exp o)
forall o. Hiding -> MId -> RefCreateEnv (RefInfo o) (Exp o)
newLam Hiding
hid MId
id)]
      HNExp' o
_ -> []
     generics :: [Move' (RefInfo o) (Exp o)]
generics = [Move' (RefInfo o) (Exp o)]
mlam [Move' (RefInfo o) (Exp o)]
-> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
forall a. [a] -> [a] -> [a]
++ [Move' (RefInfo o) (Exp o)]
subsvarapps

    in
     [Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)])
-> [Move' (RefInfo o) (Exp o)] -> IO [Move' (RefInfo o) (Exp o)]
forall a b. (a -> b) -> a -> b
$ case HNExp o -> HNExp' o
forall a o. WithSeenUIds a o -> a
rawValue HNExp o
hne of
      HNApp (Var Nat
v) ICArgList o
_ ->
       let (Maybe (Metavar (Exp o) (RefInfo o))
uid, Bool
isunique) = [Metavar (Exp o) (RefInfo o)]
-> [Maybe (Metavar (Exp o) (RefInfo o))]
-> (Maybe (Metavar (Exp o) (RefInfo o)), Bool)
forall o. [UId o] -> [Maybe (UId o)] -> (Maybe (UId o), Bool)
pickUid [Metavar (Exp o) (RefInfo o)]
uids ([Maybe (Metavar (Exp o) (RefInfo o))]
 -> (Maybe (Metavar (Exp o) (RefInfo o)), Bool))
-> [Maybe (Metavar (Exp o) (RefInfo o))]
-> (Maybe (Metavar (Exp o) (RefInfo o)), Bool)
forall a b. (a -> b) -> a -> b
$ HNExp o -> [Maybe (Metavar (Exp o) (RefInfo o))]
forall a o. WithSeenUIds a o -> [Maybe (UId o)]
seenUIds HNExp o
hne
           uni :: [Move' (RefInfo o) (Exp o)]
uni = case [CAction o] -> Nat -> Maybe Nat
forall o. [CAction o] -> Nat -> Maybe Nat
univar [CAction o]
cl Nat
v of
                  Just Nat
v | Nat
v Nat -> Nat -> Bool
forall a. Ord a => a -> a -> Bool
< Nat
n -> [Cost
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move (Bool -> Cost
costUnificationIf Bool
isunique) (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall a b. (a -> b) -> a -> b
$ Nat
-> Metavar (Exp o) (RefInfo o)
-> Maybe (Metavar (Exp o) (RefInfo o))
-> Elr o
-> RefCreateEnv (RefInfo o) (Exp o)
app Nat
n Metavar (Exp o) (RefInfo o)
meta Maybe (Metavar (Exp o) (RefInfo o))
uid (Nat -> Elr o
forall o. Nat -> Elr o
Var Nat
v)]
                  Maybe Nat
_ -> []
       in [Move' (RefInfo o) (Exp o)]
uni [Move' (RefInfo o) (Exp o)]
-> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
forall a. [a] -> [a] -> [a]
++ [Move' (RefInfo o) (Exp o)]
generics
      HNApp (Const ConstRef o
c) ICArgList o
_ ->
       let (Maybe (Metavar (Exp o) (RefInfo o))
uid, Bool
isunique) = [Metavar (Exp o) (RefInfo o)]
-> [Maybe (Metavar (Exp o) (RefInfo o))]
-> (Maybe (Metavar (Exp o) (RefInfo o)), Bool)
forall o. [UId o] -> [Maybe (UId o)] -> (Maybe (UId o), Bool)
pickUid [Metavar (Exp o) (RefInfo o)]
uids ([Maybe (Metavar (Exp o) (RefInfo o))]
 -> (Maybe (Metavar (Exp o) (RefInfo o)), Bool))
-> [Maybe (Metavar (Exp o) (RefInfo o))]
-> (Maybe (Metavar (Exp o) (RefInfo o)), Bool)
forall a b. (a -> b) -> a -> b
$ HNExp o -> [Maybe (Metavar (Exp o) (RefInfo o))]
forall a o. WithSeenUIds a o -> [Maybe (UId o)]
seenUIds HNExp o
hne
       in Cost
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move (Bool -> Cost
costUnificationIf Bool
isunique) (Nat
-> Metavar (Exp o) (RefInfo o)
-> Maybe (Metavar (Exp o) (RefInfo o))
-> Elr o
-> RefCreateEnv (RefInfo o) (Exp o)
app Nat
n Metavar (Exp o) (RefInfo o)
meta Maybe (Metavar (Exp o) (RefInfo o))
uid (ConstRef o -> Elr o
forall o. ConstRef o -> Elr o
Const ConstRef o
c)) Move' (RefInfo o) (Exp o)
-> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
forall a. a -> [a] -> [a]
: [Move' (RefInfo o) (Exp o)]
generics
      HNLam{} -> [Move' (RefInfo o) (Exp o)]
generics
      HNPi Hiding
hid Bool
possdep ICExp o
_ Abs (ICExp o)
_ ->
       let (Maybe (Metavar (Exp o) (RefInfo o))
uid, Bool
isunique) = [Metavar (Exp o) (RefInfo o)]
-> [Maybe (Metavar (Exp o) (RefInfo o))]
-> (Maybe (Metavar (Exp o) (RefInfo o)), Bool)
forall o. [UId o] -> [Maybe (UId o)] -> (Maybe (UId o), Bool)
pickUid [Metavar (Exp o) (RefInfo o)]
uids ([Maybe (Metavar (Exp o) (RefInfo o))]
 -> (Maybe (Metavar (Exp o) (RefInfo o)), Bool))
-> [Maybe (Metavar (Exp o) (RefInfo o))]
-> (Maybe (Metavar (Exp o) (RefInfo o)), Bool)
forall a b. (a -> b) -> a -> b
$ HNExp o -> [Maybe (Metavar (Exp o) (RefInfo o))]
forall a o. WithSeenUIds a o -> [Maybe (UId o)]
seenUIds HNExp o
hne
       in Cost
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move (Bool -> Cost
costUnificationIf Bool
isunique) (Metavar (Exp o) (RefInfo o)
-> Bool -> Hiding -> RefCreateEnv (RefInfo o) (Exp o)
forall o.
UId o -> Bool -> Hiding -> RefCreateEnv (RefInfo o) (Exp o)
newPi (Metavar (Exp o) (RefInfo o)
-> Maybe (Metavar (Exp o) (RefInfo o))
-> Metavar (Exp o) (RefInfo o)
forall a. a -> Maybe a -> a
fromMaybe Metavar (Exp o) (RefInfo o)
meta Maybe (Metavar (Exp o) (RefInfo o))
uid) Bool
possdep Hiding
hid) Move' (RefInfo o) (Exp o)
-> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
forall a. a -> [a] -> [a]
: [Move' (RefInfo o) (Exp o)]
generics
      HNSort (Set Nat
l) -> (Nat -> Move' (RefInfo o) (Exp o))
-> [Nat] -> [Move' (RefInfo o) (Exp o)]
forall a b. (a -> b) -> [a] -> [b]
map (Cost
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
costUnification (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
-> (Nat -> RefCreateEnv (RefInfo o) (Exp o))
-> Nat
-> Move' (RefInfo o) (Exp o)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> RefCreateEnv (RefInfo o) (Exp o)
forall {m :: * -> *} {o}. Monad m => Nat -> m (Exp o)
set) [Nat
0..Nat
l] [Move' (RefInfo o) (Exp o)]
-> [Move' (RefInfo o) (Exp o)] -> [Move' (RefInfo o) (Exp o)]
forall a. [a] -> [a] -> [a]
++ [Move' (RefInfo o) (Exp o)]
generics
      HNSort Sort
_ -> [Move' (RefInfo o) (Exp o)]
generics
   [RefInfo o]
_ -> IO [Move' (RefInfo o) (Exp o)]
forall a. HasCallStack => a
__IMPOSSIBLE__

  where

    app :: Nat -> UId o -> Maybe (UId o) -> Elr o ->
           RefCreateEnv (RefInfo o) (Exp o)
    app :: Nat
-> Metavar (Exp o) (RefInfo o)
-> Maybe (Metavar (Exp o) (RefInfo o))
-> Elr o
-> RefCreateEnv (RefInfo o) (Exp o)
app Nat
n Metavar (Exp o) (RefInfo o)
meta Maybe (Metavar (Exp o) (RefInfo o))
muid Elr o
elr = do
      MM (ArgList o) (RefInfo o)
p <- RefCreateEnv (RefInfo o) (MM (ArgList o) (RefInfo o))
forall blk a. RefCreateEnv blk (MM a blk)
newPlaceholder
      MM (ArgList o) (RefInfo o)
p <- case Elr o
elr of
        Var{}   -> MM (ArgList o) (RefInfo o)
-> RefCreateEnv (RefInfo o) (MM (ArgList o) (RefInfo o))
forall a. a -> RefCreateEnv (RefInfo o) a
forall (m :: * -> *) a. Monad m => a -> m a
return MM (ArgList o) (RefInfo o)
p
        Const ConstRef o
c -> do
          ConstDef o
cd <- StateT (IORef [SubConstraints (RefInfo o)], Nat) IO (ConstDef o)
-> RefCreateEnv (RefInfo o) (ConstDef o)
forall blk a.
StateT (IORef [SubConstraints blk], Nat) IO a -> RefCreateEnv blk a
RefCreateEnv (StateT (IORef [SubConstraints (RefInfo o)], Nat) IO (ConstDef o)
 -> RefCreateEnv (RefInfo o) (ConstDef o))
-> StateT (IORef [SubConstraints (RefInfo o)], Nat) IO (ConstDef o)
-> RefCreateEnv (RefInfo o) (ConstDef o)
forall a b. (a -> b) -> a -> b
$ IO (ConstDef o)
-> StateT (IORef [SubConstraints (RefInfo o)], Nat) IO (ConstDef o)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (IORef [SubConstraints (RefInfo o)], Nat) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (ConstDef o)
 -> StateT
      (IORef [SubConstraints (RefInfo o)], Nat) IO (ConstDef o))
-> IO (ConstDef o)
-> StateT (IORef [SubConstraints (RefInfo o)], Nat) IO (ConstDef o)
forall a b. (a -> b) -> a -> b
$ ConstRef o -> IO (ConstDef o)
forall a. IORef a -> IO a
readIORef ConstRef o
c
          let dfvapp :: Nat -> Nat -> MM (ArgList o) (RefInfo o)
dfvapp Nat
0 Nat
_ = MM (ArgList o) (RefInfo o)
p
              dfvapp Nat
i Nat
n = ArgList o -> MM (ArgList o) (RefInfo o)
forall a blk. a -> MM a blk
NotM (ArgList o -> MM (ArgList o) (RefInfo o))
-> ArgList o -> MM (ArgList o) (RefInfo o)
forall a b. (a -> b) -> a -> b
$ Hiding -> MExp o -> MM (ArgList o) (RefInfo o) -> ArgList o
forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
NotHidden
                          (Exp o -> MExp o
forall a blk. a -> MM a blk
NotM (Exp o -> MExp o) -> Exp o -> MExp o
forall a b. (a -> b) -> a -> b
$ Maybe (Metavar (Exp o) (RefInfo o))
-> OKHandle (RefInfo o)
-> Elr o
-> MM (ArgList o) (RefInfo o)
-> Exp o
forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App Maybe (Metavar (Exp o) (RefInfo o))
forall a. Maybe a
Nothing (OKVal -> OKHandle (RefInfo o)
forall a blk. a -> MM a blk
NotM (OKVal -> OKHandle (RefInfo o)) -> OKVal -> OKHandle (RefInfo o)
forall a b. (a -> b) -> a -> b
$ OKVal
OKVal) (Nat -> Elr o
forall o. Nat -> Elr o
Var Nat
n) (ArgList o -> MM (ArgList o) (RefInfo o)
forall a blk. a -> MM a blk
NotM ArgList o
forall o. ArgList o
ALNil))
                          (Nat -> Nat -> MM (ArgList o) (RefInfo o)
dfvapp (Nat
i Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1) (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1))
         -- NotHidden is ok because agda reification throws these arguments
         -- away and agsy skips typechecking them
          MM (ArgList o) (RefInfo o)
-> RefCreateEnv (RefInfo o) (MM (ArgList o) (RefInfo o))
forall a. a -> RefCreateEnv (RefInfo o) a
forall (m :: * -> *) a. Monad m => a -> m a
return (MM (ArgList o) (RefInfo o)
 -> RefCreateEnv (RefInfo o) (MM (ArgList o) (RefInfo o)))
-> MM (ArgList o) (RefInfo o)
-> RefCreateEnv (RefInfo o) (MM (ArgList o) (RefInfo o))
forall a b. (a -> b) -> a -> b
$ Nat -> Nat -> MM (ArgList o) (RefInfo o)
dfvapp (ConstDef o -> Nat
forall o. ConstDef o -> Nat
cddeffreevars ConstDef o
cd) (Nat
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- Nat
1)
      OKHandle (RefInfo o)
okh <- RefCreateEnv (RefInfo o) (OKHandle (RefInfo o))
forall blk. RefCreateEnv blk (OKHandle blk)
newOKHandle
      Exp o -> RefCreateEnv (RefInfo o) (Exp o)
forall a. a -> RefCreateEnv (RefInfo o) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp o -> RefCreateEnv (RefInfo o) (Exp o))
-> Exp o -> RefCreateEnv (RefInfo o) (Exp o)
forall a b. (a -> b) -> a -> b
$ Maybe (Metavar (Exp o) (RefInfo o))
-> OKHandle (RefInfo o)
-> Elr o
-> MM (ArgList o) (RefInfo o)
-> Exp o
forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App (Metavar (Exp o) (RefInfo o) -> Maybe (Metavar (Exp o) (RefInfo o))
forall a. a -> Maybe a
Just (Metavar (Exp o) (RefInfo o)
 -> Maybe (Metavar (Exp o) (RefInfo o)))
-> Metavar (Exp o) (RefInfo o)
-> Maybe (Metavar (Exp o) (RefInfo o))
forall a b. (a -> b) -> a -> b
$ Metavar (Exp o) (RefInfo o)
-> Maybe (Metavar (Exp o) (RefInfo o))
-> Metavar (Exp o) (RefInfo o)
forall a. a -> Maybe a -> a
fromMaybe Metavar (Exp o) (RefInfo o)
meta Maybe (Metavar (Exp o) (RefInfo o))
muid) OKHandle (RefInfo o)
okh Elr o
elr MM (ArgList o) (RefInfo o)
p


extraref :: UId o -> [Maybe (UId o)] -> ConstRef o -> Move o
extraref :: forall o. UId o -> [Maybe (UId o)] -> ConstRef o -> Move o
extraref UId o
meta [Maybe (UId o)]
seenuids ConstRef o
c = Cost
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
costAppExtraRef (RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o))
-> RefCreateEnv (RefInfo o) (Exp o) -> Move' (RefInfo o) (Exp o)
forall a b. (a -> b) -> a -> b
$ Maybe (UId o) -> Elr o -> RefCreateEnv (RefInfo o) (Exp o)
app ([Maybe (UId o)] -> Maybe (UId o)
forall a. HasCallStack => [a] -> a
head [Maybe (UId o)]
seenuids) (ConstRef o -> Elr o
forall o. ConstRef o -> Elr o
Const ConstRef o
c)
 where
   app :: Maybe (UId o) -> Elr o -> RefCreateEnv (RefInfo o) (Exp o)
app Maybe (UId o)
muid Elr o
elr = Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App (UId o -> Maybe (UId o)
forall a. a -> Maybe a
Just (UId o -> Maybe (UId o)) -> UId o -> Maybe (UId o)
forall a b. (a -> b) -> a -> b
$ UId o -> Maybe (UId o) -> UId o
forall a. a -> Maybe a -> a
fromMaybe UId o
meta Maybe (UId o)
muid)
              (OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o)
-> RefCreateEnv (RefInfo o) (OKHandle (RefInfo o))
-> RefCreateEnv (RefInfo o) (Elr o -> MArgList o -> Exp o)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RefCreateEnv (RefInfo o) (OKHandle (RefInfo o))
forall blk. RefCreateEnv blk (OKHandle blk)
newOKHandle RefCreateEnv (RefInfo o) (Elr o -> MArgList o -> Exp o)
-> RefCreateEnv (RefInfo o) (Elr o)
-> RefCreateEnv (RefInfo o) (MArgList o -> Exp o)
forall a b.
RefCreateEnv (RefInfo o) (a -> b)
-> RefCreateEnv (RefInfo o) a -> RefCreateEnv (RefInfo o) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Elr o -> RefCreateEnv (RefInfo o) (Elr o)
forall a. a -> RefCreateEnv (RefInfo o) a
forall (m :: * -> *) a. Monad m => a -> m a
return Elr o
elr RefCreateEnv (RefInfo o) (MArgList o -> Exp o)
-> RefCreateEnv (RefInfo o) (MArgList o)
-> RefCreateEnv (RefInfo o) (Exp o)
forall a b.
RefCreateEnv (RefInfo o) (a -> b)
-> RefCreateEnv (RefInfo o) a -> RefCreateEnv (RefInfo o) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RefCreateEnv (RefInfo o) (MArgList o)
forall blk a. RefCreateEnv blk (MM a blk)
newPlaceholder

instance Refinable (ICExp o) (RefInfo o) where
 refinements :: RefInfo o
-> [RefInfo o]
-> Metavar (ICExp o) (RefInfo o)
-> IO [Move' (RefInfo o) (ICExp o)]
refinements RefInfo o
_ [RefInfo o]
infos Metavar (ICExp o) (RefInfo o)
_ =
  let (RICopyInfo ICExp o
e : [RefInfo o]
_) = [RefInfo o]
infos
  in [Move' (RefInfo o) (ICExp o)] -> IO [Move' (RefInfo o) (ICExp o)]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Cost
-> RefCreateEnv (RefInfo o) (ICExp o)
-> Move' (RefInfo o) (ICExp o)
forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
0 (ICExp o -> RefCreateEnv (RefInfo o) (ICExp o)
forall a. a -> RefCreateEnv (RefInfo o) a
forall (m :: * -> *) a. Monad m => a -> m a
return ICExp o
e)]


instance Refinable (ConstRef o) (RefInfo o) where
 refinements :: RefInfo o
-> [RefInfo o]
-> Metavar (ConstRef o) (RefInfo o)
-> IO [Move' (RefInfo o) (ConstRef o)]
refinements RefInfo o
_ [RICheckProjIndex [ConstRef o]
projs] Metavar (ConstRef o) (RefInfo o)
_ = [Move' (RefInfo o) (ConstRef o)]
-> IO [Move' (RefInfo o) (ConstRef o)]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Move' (RefInfo o) (ConstRef o)]
 -> IO [Move' (RefInfo o) (ConstRef o)])
-> [Move' (RefInfo o) (ConstRef o)]
-> IO [Move' (RefInfo o) (ConstRef o)]
forall a b. (a -> b) -> a -> b
$ (ConstRef o -> Move' (RefInfo o) (ConstRef o))
-> [ConstRef o] -> [Move' (RefInfo o) (ConstRef o)]
forall a b. (a -> b) -> [a] -> [b]
map (Cost
-> RefCreateEnv (RefInfo o) (ConstRef o)
-> Move' (RefInfo o) (ConstRef o)
forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
0 (RefCreateEnv (RefInfo o) (ConstRef o)
 -> Move' (RefInfo o) (ConstRef o))
-> (ConstRef o -> RefCreateEnv (RefInfo o) (ConstRef o))
-> ConstRef o
-> Move' (RefInfo o) (ConstRef o)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConstRef o -> RefCreateEnv (RefInfo o) (ConstRef o)
forall a. a -> RefCreateEnv (RefInfo o) a
forall (m :: * -> *) a. Monad m => a -> m a
return) [ConstRef o]
projs
 refinements RefInfo o
_ [RefInfo o]
_ Metavar (ConstRef o) (RefInfo o)
_ = IO [Move' (RefInfo o) (ConstRef o)]
forall a. HasCallStack => a
__IMPOSSIBLE__


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

costIncrease, costUnificationOccurs, costUnification, costAppVar,
  costAppVarUsed, costAppHint, costAppHintUsed, costAppRecCall,
  costAppRecCallUsed, costAppConstructor, costAppConstructorSingle,
  costAppExtraRef, costLam, costLamUnfold, costPi, costSort, costIotaStep,
  costInferredTypeUnkown, costAbsurdLam
  :: Cost

costUnificationIf :: Bool -> Cost
costUnificationIf :: Bool -> Cost
costUnificationIf Bool
b = if Bool
b then Cost
costUnification else Cost
costUnificationOccurs

costIncrease :: Cost
costIncrease = Cost
1000
costUnificationOccurs :: Cost
costUnificationOccurs = Cost
100 -- 1000001 -- 1 -- 100
costUnification :: Cost
costUnification = Cost
0000
costAppVar :: Cost
costAppVar = Cost
0000 -- 0, 1
costAppVarUsed :: Cost
costAppVarUsed = Cost
1000 -- 5
costAppHint :: Cost
costAppHint = Cost
3000 -- 2, 5
costAppHintUsed :: Cost
costAppHintUsed = Cost
5000
costAppRecCall :: Cost
costAppRecCall = Cost
0 -- 1000?
costAppRecCallUsed :: Cost
costAppRecCallUsed = Cost
10000 -- 1000?
costAppConstructor :: Cost
costAppConstructor = Cost
1000
costAppConstructorSingle :: Cost
costAppConstructorSingle = Cost
0000
costAppExtraRef :: Cost
costAppExtraRef = Cost
1000
costLam :: Cost
costLam = Cost
0000 -- 1, 0
costLamUnfold :: Cost
costLamUnfold = Cost
1000 -- 1, 0
costPi :: Cost
costPi = Cost
1000003 -- 100 -- 5
costSort :: Cost
costSort = Cost
1000004 -- 0
costIotaStep :: Cost
costIotaStep = Cost
3000 -- 1000005 -- 2 -- 100
costInferredTypeUnkown :: Cost
costInferredTypeUnkown = Cost
1000006 -- 100
costAbsurdLam :: Cost
costAbsurdLam = Cost
0

costEqStep, costEqEnd, costEqSym, costEqCong :: Cost
costEqStep :: Cost
costEqStep = Cost
2000
costEqEnd :: Cost
costEqEnd = Cost
0
costEqSym :: Cost
costEqSym = Cost
0
costEqCong :: Cost
costEqCong = Cost
500

prioNo, prioTypeUnknown, prioTypecheckArgList, prioInferredTypeUnknown,
  prioCompBeta, prioCompBetaStructured, prioCompareArgList, prioCompIota,
  prioCompChoice, prioCompUnif, prioCompCopy, prioNoIota, prioAbsurdLambda,
  prioProjIndex
  :: Prio
prioNo :: Prio
prioNo = (-Prio
1)
prioTypeUnknown :: Prio
prioTypeUnknown = Prio
0
prioTypecheckArgList :: Prio
prioTypecheckArgList = Prio
3000
prioInferredTypeUnknown :: Prio
prioInferredTypeUnknown = Prio
4000
prioCompBeta :: Prio
prioCompBeta = Prio
4000
prioCompBetaStructured :: Prio
prioCompBetaStructured = Prio
4000
prioCompIota :: Prio
prioCompIota = Prio
4000
prioCompChoice :: Prio
prioCompChoice = Prio
5000 -- 700 -- 5000
prioCompUnif :: Prio
prioCompUnif = Prio
6000 -- 2
prioCompCopy :: Prio
prioCompCopy = Prio
8000
prioCompareArgList :: Prio
prioCompareArgList = Prio
7000 -- 5 -- 2
prioNoIota :: Prio
prioNoIota = Prio
500 -- 500
prioAbsurdLambda :: Prio
prioAbsurdLambda = Prio
1000

prioProjIndex :: Prio
prioProjIndex = Prio
3000

prioTypecheck :: Bool -> Prio
prioTypecheck :: Bool -> Prio
prioTypecheck Bool
False = Prio
1000
prioTypecheck Bool
True = Prio
0

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

instance Trav a => Trav [a] where
  type Block [a] = Block a
  trav :: forall (m :: * -> *).
Monad m =>
(forall b. TravWith b (Block [a]) => MM b (Block b) -> m ())
-> [a] -> m ()
trav forall b. TravWith b (Block [a]) => MM b (Block b) -> m ()
_ []     = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  trav forall b. TravWith b (Block [a]) => MM b (Block b) -> m ()
f (a
x:[a]
xs) = (forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
forall a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
forall (m :: * -> *).
Monad m =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
trav MM b (Block b) -> m ()
forall b. TravWith b (Block a) => MM b (Block b) -> m ()
forall b. TravWith b (Block [a]) => MM b (Block b) -> m ()
f a
x m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (forall b. TravWith b (Block [a]) => MM b (Block b) -> m ())
-> [a] -> m ()
forall a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
forall (m :: * -> *).
Monad m =>
(forall b. TravWith b (Block [a]) => MM b (Block b) -> m ())
-> [a] -> m ()
trav MM b (Block b) -> m ()
forall b. TravWith b (Block [a]) => MM b (Block b) -> m ()
f [a]
xs

instance Trav (MId, CExp o) where
  type Block (MId, CExp o) = RefInfo o
  trav :: forall (m :: * -> *).
Monad m =>
(forall b.
 TravWith b (Block (MId, CExp o)) =>
 MM b (Block b) -> m ())
-> (MId, CExp o) -> m ()
trav forall b.
TravWith b (Block (MId, CExp o)) =>
MM b (Block b) -> m ()
f (MId
_, CExp o
ce) = (forall b. TravWith b (Block (CExp o)) => MM b (Block b) -> m ())
-> CExp o -> m ()
forall a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
forall (m :: * -> *).
Monad m =>
(forall b. TravWith b (Block (CExp o)) => MM b (Block b) -> m ())
-> CExp o -> m ()
trav MM b (Block b) -> m ()
forall b.
TravWith b (Block (MId, CExp o)) =>
MM b (Block b) -> m ()
forall b. TravWith b (Block (CExp o)) => MM b (Block b) -> m ()
f CExp o
ce

instance Trav (TrBr a o) where
  type Block (TrBr a o) = RefInfo o
  trav :: forall (m :: * -> *).
Monad m =>
(forall b. TravWith b (Block (TrBr a o)) => MM b (Block b) -> m ())
-> TrBr a o -> m ()
trav forall b. TravWith b (Block (TrBr a o)) => MM b (Block b) -> m ()
f (TrBr [MExp o]
es a
_) = (forall b. TravWith b (Block [MExp o]) => MM b (Block b) -> m ())
-> [MExp o] -> m ()
forall a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
forall (m :: * -> *).
Monad m =>
(forall b. TravWith b (Block [MExp o]) => MM b (Block b) -> m ())
-> [MExp o] -> m ()
trav MM b (Block b) -> m ()
forall b. TravWith b (Block [MExp o]) => MM b (Block b) -> m ()
forall b. TravWith b (Block (TrBr a o)) => MM b (Block b) -> m ()
f [MExp o]
es

instance Trav (Exp o) where
  type Block (Exp o) = RefInfo o
  trav :: forall (m :: * -> *).
Monad m =>
(forall b. TravWith b (Block (Exp o)) => MM b (Block b) -> m ())
-> Exp o -> m ()
trav forall b. TravWith b (Block (Exp o)) => MM b (Block b) -> m ()
f = \case
    App Maybe (UId o)
_ OKHandle (RefInfo o)
_ Elr o
_ MArgList o
args         -> (forall b.
 TravWith b (Block (MArgList o)) =>
 MM b (Block b) -> m ())
-> MArgList o -> m ()
forall a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
forall (m :: * -> *).
Monad m =>
(forall b.
 TravWith b (Block (MArgList o)) =>
 MM b (Block b) -> m ())
-> MArgList o -> m ()
trav MM b (Block b) -> m ()
forall b. TravWith b (Block (MArgList o)) => MM b (Block b) -> m ()
forall b. TravWith b (Block (Exp o)) => MM b (Block b) -> m ()
f MArgList o
args
    Lam Hiding
_ (Abs MId
_ MExp o
b)        -> (forall b. TravWith b (Block (MExp o)) => MM b (Block b) -> m ())
-> MExp o -> m ()
forall a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
forall (m :: * -> *).
Monad m =>
(forall b. TravWith b (Block (MExp o)) => MM b (Block b) -> m ())
-> MExp o -> m ()
trav MM b (Block b) -> m ()
forall b. TravWith b (Block (MExp o)) => MM b (Block b) -> m ()
forall b. TravWith b (Block (Exp o)) => MM b (Block b) -> m ()
f MExp o
b
    Pi Maybe (UId o)
_ Hiding
_ Bool
_ MExp o
it (Abs MId
_ MExp o
ot) -> (forall b. TravWith b (Block (MExp o)) => MM b (Block b) -> m ())
-> MExp o -> m ()
forall a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
forall (m :: * -> *).
Monad m =>
(forall b. TravWith b (Block (MExp o)) => MM b (Block b) -> m ())
-> MExp o -> m ()
trav MM b (Block b) -> m ()
forall b. TravWith b (Block (MExp o)) => MM b (Block b) -> m ()
forall b. TravWith b (Block (Exp o)) => MM b (Block b) -> m ()
f MExp o
it m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (forall b. TravWith b (Block (MExp o)) => MM b (Block b) -> m ())
-> MExp o -> m ()
forall a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
forall (m :: * -> *).
Monad m =>
(forall b. TravWith b (Block (MExp o)) => MM b (Block b) -> m ())
-> MExp o -> m ()
trav MM b (Block b) -> m ()
forall b. TravWith b (Block (MExp o)) => MM b (Block b) -> m ()
forall b. TravWith b (Block (Exp o)) => MM b (Block b) -> m ()
f MExp o
ot
    Sort Sort
_                 -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    AbsurdLambda{}         -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

instance Trav (ArgList o) where
  type Block (ArgList o) = RefInfo o
  trav :: forall (m :: * -> *).
Monad m =>
(forall b.
 TravWith b (Block (ArgList o)) =>
 MM b (Block b) -> m ())
-> ArgList o -> m ()
trav forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()
_ ArgList o
ALNil               = () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  trav forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()
f (ALCons Hiding
_ MExp o
arg MArgList o
args) = (forall b. TravWith b (Block (MExp o)) => MM b (Block b) -> m ())
-> MExp o -> m ()
forall a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
forall (m :: * -> *).
Monad m =>
(forall b. TravWith b (Block (MExp o)) => MM b (Block b) -> m ())
-> MExp o -> m ()
trav MM b (Block b) -> m ()
forall b. TravWith b (Block (MExp o)) => MM b (Block b) -> m ()
forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()
f MExp o
arg m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (forall b.
 TravWith b (Block (MArgList o)) =>
 MM b (Block b) -> m ())
-> MArgList o -> m ()
forall a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
forall (m :: * -> *).
Monad m =>
(forall b.
 TravWith b (Block (MArgList o)) =>
 MM b (Block b) -> m ())
-> MArgList o -> m ()
trav MM b (Block b) -> m ()
forall b. TravWith b (Block (MArgList o)) => MM b (Block b) -> m ()
forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()
f MArgList o
args
  trav forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()
f (ALProj MArgList o
eas MM (ConstRef o) (RefInfo o)
_ Hiding
_ MArgList o
as) = (forall b.
 TravWith b (Block (MArgList o)) =>
 MM b (Block b) -> m ())
-> MArgList o -> m ()
forall a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
forall (m :: * -> *).
Monad m =>
(forall b.
 TravWith b (Block (MArgList o)) =>
 MM b (Block b) -> m ())
-> MArgList o -> m ()
trav MM b (Block b) -> m ()
forall b. TravWith b (Block (MArgList o)) => MM b (Block b) -> m ()
forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()
f MArgList o
eas m () -> m () -> m ()
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (forall b.
 TravWith b (Block (MArgList o)) =>
 MM b (Block b) -> m ())
-> MArgList o -> m ()
forall a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
forall (m :: * -> *).
Monad m =>
(forall b.
 TravWith b (Block (MArgList o)) =>
 MM b (Block b) -> m ())
-> MArgList o -> m ()
trav MM b (Block b) -> m ()
forall b. TravWith b (Block (MArgList o)) => MM b (Block b) -> m ()
forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()
f MArgList o
as
  trav forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()
f (ALConPar MArgList o
args)     = (forall b.
 TravWith b (Block (MArgList o)) =>
 MM b (Block b) -> m ())
-> MArgList o -> m ()
forall a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
forall (m :: * -> *).
Monad m =>
(forall b.
 TravWith b (Block (MArgList o)) =>
 MM b (Block b) -> m ())
-> MArgList o -> m ()
trav MM b (Block b) -> m ()
forall b. TravWith b (Block (MArgList o)) => MM b (Block b) -> m ()
forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()
f MArgList o
args

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