{-# OPTIONS_GHC -fno-warn-orphans #-}

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)
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
0) forall a b. (a -> b) -> a -> b
$
   [ forall (m :: * -> *) a. Monad m => a -> m a
return forall o. ArgList o
ALNil, Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
cons Hiding
NotHidden, Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
cons Hiding
Hidden ]
   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]
_ = forall a. HasCallStack => a
__IMPOSSIBLE__

    proj :: Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
    proj :: Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
proj Hiding
hid = forall o.
MArgList o
-> MM (ConstRef o) (RefInfo o) -> Hiding -> MArgList o -> ArgList o
ALProj forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall blk a. RefCreateEnv blk (MM a blk)
newPlaceholder forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall blk a. RefCreateEnv blk (MM a blk)
newPlaceholder
                      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return Hiding
hid     forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 = forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
hid forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall blk a. RefCreateEnv blk (MM a blk)
newPlaceholder forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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           = 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       = forall a. Maybe a
Nothing
  , eriIotaStep :: Maybe Bool
eriIotaStep       = forall a. Maybe a
Nothing
  , eriPickSubsVar :: Bool
eriPickSubsVar    = Bool
False
  , eriEqRState :: Maybe EqReasoningState
eriEqRState       = forall a. Maybe a
Nothing
  }

getinfo :: [RefInfo o] -> ExpRefInfo o
getinfo :: forall o. [RefInfo o] -> ExpRefInfo o
getinfo = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall o. ExpRefInfo o -> RefInfo o -> ExpRefInfo o
step 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 :: Maybe (RefInfo o)
eriMain  = forall a. a -> Maybe a
Just RefInfo o
x }
  step ExpRefInfo o
eri x :: RefInfo o
x@RIUnifInfo{}           = ExpRefInfo o
eri { eriUnifs :: [RefInfo o]
eriUnifs = RefInfo o
x forall a. a -> [a] -> [a]
: forall o. ExpRefInfo o -> [RefInfo o]
eriUnifs ExpRefInfo o
eri }
  step ExpRefInfo o
eri RefInfo o
RIInferredTypeUnknown    = ExpRefInfo o
eri { eriInfTypeUnknown :: Bool
eriInfTypeUnknown = Bool
True }
  step ExpRefInfo o
eri RefInfo o
RINotConstructor         = ExpRefInfo o
eri { eriIsEliminand :: Bool
eriIsEliminand = Bool
True }
  step ExpRefInfo o
eri (RIUsedVars [UId o]
nuids [Elr o]
nused) = ExpRefInfo o
eri { eriUsedVars :: Maybe ([UId o], [Elr o])
eriUsedVars = forall a. a -> Maybe a
Just ([UId o]
nuids, [Elr o]
nused) }
  step ExpRefInfo o
eri (RIIotaStep Bool
semif)       = ExpRefInfo o
eri { eriIotaStep :: Maybe Bool
eriIotaStep = forall a. a -> Maybe a
Just Bool
iota' } where
    iota' :: Bool
iota' = Bool
semif Bool -> Bool -> Bool
|| (forall a. a -> Maybe a
Just Bool
True forall a. Eq a => a -> a -> Bool
==) (forall o. ExpRefInfo o -> Maybe Bool
eriIotaStep ExpRefInfo o
eri)
  step ExpRefInfo o
eri RefInfo o
RIPickSubsvar            = ExpRefInfo o
eri { eriPickSubsVar :: Bool
eriPickSubsVar = Bool
True }
  step ExpRefInfo o
eri (RIEqRState EqReasoningState
s)           = ExpRefInfo o
eri { eriEqRState :: Maybe EqReasoningState
eriEqRState = forall a. a -> Maybe a
Just EqReasoningState
s }
  step ExpRefInfo o
eri RefInfo 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 = 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' = forall a. a -> Maybe a
Just (Nat
v' 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 forall a. Ord a => a -> a -> Bool
< Nat
n = forall a. Maybe a
Nothing
  -- @v@ was introduced before the weakening: strengthened
  getOutsideName (Weak Nat
n : [CAction o]
xs) Nat
v Nat
v' = forall o. [CAction o] -> Nat -> Nat -> Maybe Nat
getOutsideName [CAction o]
xs (Nat
v 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' = forall o. [CAction o] -> Nat -> Nat -> Maybe Nat
getOutsideName [CAction o]
xs Nat
v (Nat
v' 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' = 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' = forall o. [CAction o] -> Nat -> Nat -> Maybe Nat
getOutsideName [CAction o]
xs (Nat
v forall a. Num a => a -> a -> a
- Nat
1) (Nat
v' 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 = 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) = forall o. Nat -> [CAction o] -> [Nat]
f Nat
n [CAction o]
xs -- why?
  f Nat
n (Sub ICExp o
_  : [CAction o]
xs) = Nat
n forall a. a -> [a] -> [a]
: forall o. Nat -> [CAction o] -> [Nat]
f (Nat
n forall a. Num a => a -> a -> a
+ Nat
1) [CAction o]
xs
  f Nat
n (CAction o
Skip   : [CAction o]
xs) = forall o. Nat -> [CAction o] -> [Nat]
f (Nat
n 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 = forall a. MId -> a -> Abs a
Abs MId
mid forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall o. Hiding -> Abs (MExp o) -> Exp o
Lam Hiding
hid forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall o.
Maybe (UId o) -> Hiding -> Bool -> MExp o -> Abs (MExp o) -> Exp o
Pi (forall a. a -> Maybe a
Just UId o
uid) Hiding
hid Bool
dep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall blk a. RefCreateEnv blk (MM a blk)
newPlaceholder forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (Hiding
h, MExp o
a) MArgList o
sp -> forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
h MExp o
a MArgList o
sp) (forall a blk. a -> MM a blk
NotM 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 = forall o. [(Hiding, MExp o)] -> MArgList o
foldArgs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [a] -> [b] -> [(a, b)]
zip [Hiding]
h forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. [a] -> [a] -> [a]
++ [MExp o]
tms) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. Applicative m => Nat -> m a -> m [a]
replicateM Nat
size forall blk a. RefCreateEnv blk (MM a blk)
newPlaceholder
  where size :: Nat
size = forall (t :: * -> *) a. Foldable t => t a -> Nat
length [Hiding]
h forall a. Num a => a -> a -> a
- 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 = 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 =
  forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App (forall a. a -> Maybe a
Just UId o
meta) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall blk. RefCreateEnv blk (OKHandle blk)
newOKHandle forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return (forall o. ConstRef o -> Elr o
Const ConstRef o
cst) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 = 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 = forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
costEqStep forall a b. (a -> b) -> a -> b
$ forall o.
UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
newApp UId o
meta (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 = forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
costEqEnd forall a b. (a -> b) -> a -> b
$ forall o.
UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
newApp UId o
meta (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 = forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
costEqCong forall a b. (a -> b) -> a -> b
$ forall o.
UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
newApp UId o
meta (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 = forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
costEqSym forall a b. (a -> b) -> a -> b
$ forall o.
UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
newApp UId o
meta (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 = forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
costEqStep forall a b. (a -> b) -> a -> b
$ do
  Exp o
e1 <- forall o.
UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
newApp UId o
meta (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 <- forall o.
UId o
-> ConstRef o
-> [Hiding]
-> [MExp o]
-> RefCreateEnv (RefInfo o) (Exp o)
newApp' UId o
meta (forall o. EqReasoningConsts o -> ConstRef o
eqrcStep EqReasoningConsts o
eqrc)
          [Hiding
Hidden, Hiding
Hidden, Hiding
NotHidden, Hiding
Hidden, Hiding
Hidden, Hiding
NotHidden, Hiding
NotHidden]
          [forall a blk. a -> MM a blk
NotM Exp o
e1]
  forall o.
UId o
-> ConstRef o
-> [Hiding]
-> [MExp o]
-> RefCreateEnv (RefInfo o) (Exp o)
newApp' UId o
meta (forall o. EqReasoningConsts o -> ConstRef o
eqrcBegin EqReasoningConsts o
eqrc) [Hiding
Hidden, Hiding
Hidden, Hiding
Hidden, Hiding
Hidden, Hiding
NotHidden]
    [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 = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (forall a. [a] -> a
head [Maybe (UId o)]
seen, Bool
False) (, Bool
True) 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 []                 = forall a. Maybe a
Nothing
  firstUnused (Maybe (UId o)
Nothing     : [Maybe (UId o)]
_)  = forall a. a -> Maybe a
Just forall a. Maybe a
Nothing
  firstUnused (mu :: Maybe (UId o)
mu@(Just UId o
u) : [Maybe (UId o)]
us) =
    if UId o
u 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 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 = forall o. RefInfo o -> [(ConstRef o, HintMode)]
rieHints RefInfo o
envinfo
   deffreevars :: Nat
deffreevars = forall o. RefInfo o -> Nat
rieDefFreeVars RefInfo o
envinfo

   meqr :: Maybe (EqReasoningConsts o)
meqr = 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
              } = forall o. [RefInfo o] -> ExpRefInfo o
getinfo [RefInfo o]
infos

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

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

     eqr :: EqReasoningConsts o
eqr = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ Maybe (EqReasoningConsts o)
meqr
     eq_end :: Move' (RefInfo o) (Exp o)
eq_end         = 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        = 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        = 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         = 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 = 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 forall a. Ord a => a -> a -> Bool
< Nat
n forall a. Num a => a -> a -> a
- Nat
deffreevars = Cost -> Cost
adjustCost forall a b. (a -> b) -> a -> b
$
       if Nat
v forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe 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  = forall a b. (a -> b) -> [a] -> [b]
map (\ Nat
v -> forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move (Nat -> Cost
varcost Nat
v) 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 forall a. Maybe a
Nothing (forall o. Nat -> Elr o
Var Nat
v)) [Nat
0..Nat
n forall a. Num a => a -> a -> a
- Nat
1]
     hintapps :: [Move' (RefInfo o) (Exp o)]
hintapps = forall a b. (a -> b) -> [a] -> [b]
map (\(ConstRef o
c, HintMode
hm) -> 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 forall a. Maybe a
Nothing (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 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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe 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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe 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 forall a. [a] -> [a] -> [a]
++ [Move' (RefInfo o) (Exp o)]
hintapps
    in case forall a o. WithSeenUIds a o -> a
rawValue HNExp o
tt of

     HNExp' o
_ | EqReasoningState
eqrstate forall a. Eq a => a -> a -> Bool
== EqReasoningState
EqRSChain ->
      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
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
         forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move (Cost -> Cost
adjustCost (if Bool
iotastepdone then Cost
costLamUnfold else Cost
costLam)) (forall o. Hiding -> MId -> RefCreateEnv (RefInfo o) (Exp o)
newLam Hiding
hid MId
id)
       forall a. a -> [a] -> [a]
: forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
costAbsurdLam (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall o. Hiding -> Exp o
AbsurdLambda Hiding
hid)
       forall a. a -> [a] -> [a]
: [Move' (RefInfo o) (Exp o)]
generics

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


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

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

       DeclCont o
_ -> [Move' (RefInfo o) (Exp o)]
generics
     HNExp' o
_ -> 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 = forall a b. (a -> b) -> [a] -> [b]
map (forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
costUnification 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 forall a. Maybe a
Nothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall o. Nat -> Elr o
Var) (forall o. [CAction o] -> [Nat]
subsvars [CAction o]
cl)
     mlam :: [Move' (RefInfo o) (Exp o)]
mlam = case forall a o. WithSeenUIds a o -> a
rawValue HNExp o
tt of
      HNPi Hiding
hid Bool
_ ICExp o
_ (Abs MId
id ICExp o
_) -> [forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
costUnification (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 forall a. [a] -> [a] -> [a]
++ [Move' (RefInfo o) (Exp o)]
subsvarapps

    in
     forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case 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) = forall o. [UId o] -> [Maybe (UId o)] -> (Maybe (UId o), Bool)
pickUid [Metavar (Exp o) (RefInfo o)]
uids forall a b. (a -> b) -> a -> b
$ forall a o. WithSeenUIds a o -> [Maybe (UId o)]
seenUIds HNExp o
hne
           uni :: [Move' (RefInfo o) (Exp o)]
uni = case forall o. [CAction o] -> Nat -> Maybe Nat
univar [CAction o]
cl Nat
v of
                  Just Nat
v | Nat
v forall a. Ord a => a -> a -> Bool
< Nat
n -> [forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move (Bool -> Cost
costUnificationIf Bool
isunique) 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 (forall o. Nat -> Elr o
Var Nat
v)]
                  Maybe Nat
_ -> []
       in [Move' (RefInfo o) (Exp o)]
uni 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) = forall o. [UId o] -> [Maybe (UId o)] -> (Maybe (UId o), Bool)
pickUid [Metavar (Exp o) (RefInfo o)]
uids forall a b. (a -> b) -> a -> b
$ forall a o. WithSeenUIds a o -> [Maybe (UId o)]
seenUIds HNExp o
hne
       in 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 (forall o. ConstRef o -> Elr o
Const ConstRef o
c)) 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) = forall o. [UId o] -> [Maybe (UId o)] -> (Maybe (UId o), Bool)
pickUid [Metavar (Exp o) (RefInfo o)]
uids forall a b. (a -> b) -> a -> b
$ forall a o. WithSeenUIds a o -> [Maybe (UId o)]
seenUIds HNExp o
hne
       in forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move (Bool -> Cost
costUnificationIf Bool
isunique) (forall o.
UId o -> Bool -> Hiding -> RefCreateEnv (RefInfo o) (Exp o)
newPi (forall a. a -> Maybe a -> a
fromMaybe Metavar (Exp o) (RefInfo o)
meta Maybe (Metavar (Exp o) (RefInfo o))
uid) Bool
possdep Hiding
hid) forall a. a -> [a] -> [a]
: [Move' (RefInfo o) (Exp o)]
generics
      HNSort (Set Nat
l) -> forall a b. (a -> b) -> [a] -> [b]
map (forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
costUnification forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {m :: * -> *} {o}. Monad m => Nat -> m (Exp o)
set) [Nat
0..Nat
l] forall a. [a] -> [a] -> [a]
++ [Move' (RefInfo o) (Exp o)]
generics
      HNSort Sort
_ -> [Move' (RefInfo o) (Exp o)]
generics
   [RefInfo 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 <- forall blk a. RefCreateEnv blk (MM a blk)
newPlaceholder
      MM (ArgList o) (RefInfo o)
p <- case Elr o
elr of
        Var{}   -> forall (m :: * -> *) a. Monad m => a -> m a
return MM (ArgList o) (RefInfo o)
p
        Const ConstRef o
c -> do
          ConstDef o
cd <- forall blk a.
StateT (IORef [SubConstraints blk], Nat) IO a -> RefCreateEnv blk a
RefCreateEnv forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef ConstRef o
c
          let dfvapp :: Nat -> Nat -> MM (ArgList o) (RefInfo o)
dfvapp Nat
0 Nat
_ = MM (ArgList o) (RefInfo o)
p
              dfvapp Nat
i Nat
n = forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o. Hiding -> MExp o -> MArgList o -> ArgList o
ALCons Hiding
NotHidden
                          (forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App forall a. Maybe a
Nothing (forall a blk. a -> MM a blk
NotM forall a b. (a -> b) -> a -> b
$ OKVal
OKVal) (forall o. Nat -> Elr o
Var Nat
n) (forall a blk. a -> MM a blk
NotM forall o. ArgList o
ALNil))
                          (Nat -> Nat -> MM (ArgList o) (RefInfo o)
dfvapp (Nat
i forall a. Num a => a -> a -> a
- Nat
1) (Nat
n forall a. Num a => a -> a -> a
- Nat
1))
         -- NotHidden is ok because agda reification throws these arguments
         -- away and agsy skips typechecking them
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Nat -> Nat -> MM (ArgList o) (RefInfo o)
dfvapp (forall o. ConstDef o -> Nat
cddeffreevars ConstDef o
cd) (Nat
n forall a. Num a => a -> a -> a
- Nat
1)
      MM OKVal (RefInfo o)
okh <- forall blk. RefCreateEnv blk (OKHandle blk)
newOKHandle
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe Metavar (Exp o) (RefInfo o)
meta Maybe (Metavar (Exp o) (RefInfo o))
muid) MM OKVal (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 = forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
costAppExtraRef forall a b. (a -> b) -> a -> b
$ Maybe (UId o) -> Elr o -> RefCreateEnv (RefInfo o) (Exp o)
app (forall a. [a] -> a
head [Maybe (UId o)]
seenuids) (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 = forall o.
Maybe (UId o)
-> OKHandle (RefInfo o) -> Elr o -> MArgList o -> Exp o
App (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe UId o
meta Maybe (UId o)
muid)
              forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall blk. RefCreateEnv blk (OKHandle blk)
newOKHandle forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *) a. Monad m => a -> m a
return Elr o
elr forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 forall (m :: * -> *) a. Monad m => a -> m a
return [forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
0 (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)
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => a -> m a
return) [ConstRef o]
projs
 refinements RefInfo o
_ [RefInfo o]
_ Metavar (ConstRef o) (RefInfo 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 ()
_ []     = 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 a (m :: * -> *).
(Trav a, 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 ()
f a
x forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Trav a, 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 ()
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 a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
trav forall b.
TravWith b (Block (MId, 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 a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
trav 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 a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
trav forall b. TravWith b (Block (Exp o)) => MM b (Block b) -> m ()
f MArgList o
args
    Lam Hiding
_ (Abs MId
_ MExp o
b)        -> forall a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
trav 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 a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
trav forall b. TravWith b (Block (Exp o)) => MM b (Block b) -> m ()
f MExp o
it forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
trav forall b. TravWith b (Block (Exp o)) => MM b (Block b) -> m ()
f MExp o
ot
    Sort Sort
_                 -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    AbsurdLambda{}         -> 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               = 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 a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
trav forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()
f MExp o
arg forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
trav 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 a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
trav forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()
f MArgList o
eas forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
trav 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 a (m :: * -> *).
(Trav a, Monad m) =>
(forall b. TravWith b (Block a) => MM b (Block b) -> m ())
-> a -> m ()
trav forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()
f MArgList o
args

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