{-# 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)
_ = 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

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