{-# 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 :: [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
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)
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
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'
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)
getOutsideName (CAction o
Skip : [CAction o]
_) Nat
0 Nat
v' = forall a. a -> Maybe a
Just Nat
v'
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)
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
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
type Move o = Move' (RefInfo o) (Exp o)
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)
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 []
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 []
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]
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
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
, 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
, 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))
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
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
costUnification :: Cost
costUnification = Cost
0000
costAppVar :: Cost
costAppVar = Cost
0000
costAppVarUsed :: Cost
costAppVarUsed = Cost
1000
costAppHint :: Cost
costAppHint = Cost
3000
costAppHintUsed :: Cost
costAppHintUsed = Cost
5000
costAppRecCall :: Cost
costAppRecCall = Cost
0
costAppRecCallUsed :: Cost
costAppRecCallUsed = Cost
10000
costAppConstructor :: Cost
costAppConstructor = Cost
1000
costAppConstructorSingle :: Cost
costAppConstructorSingle = Cost
0000
= Cost
1000
costLam :: Cost
costLam = Cost
0000
costLamUnfold :: Cost
costLamUnfold = Cost
1000
costPi :: Cost
costPi = Cost
1000003
costSort :: Cost
costSort = Cost
1000004
costIotaStep :: Cost
costIotaStep = Cost
3000
costInferredTypeUnkown :: Cost
costInferredTypeUnkown = Cost
1000006
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
prioCompUnif :: Prio
prioCompUnif = Prio
6000
prioCompCopy :: Prio
prioCompCopy = Prio
8000
prioCompareArgList :: Prio
prioCompareArgList = Prio
7000
prioNoIota :: Prio
prioNoIota = Prio
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