{-# LANGUAGE UndecidableInstances #-}
{-# 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)
_ = [Move' (RefInfo o) (ArgList o)]
-> IO [Move' (RefInfo o) (ArgList o)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Move' (RefInfo o) (ArgList o)]
 -> IO [Move' (RefInfo o) (ArgList o)])
-> [Move' (RefInfo o) (ArgList o)]
-> IO [Move' (RefInfo o) (ArgList o)]
forall a b. (a -> b) -> a -> b
$ (RefCreateEnv (RefInfo o) (ArgList o)
 -> Move' (RefInfo o) (ArgList o))
-> [RefCreateEnv (RefInfo o) (ArgList o)]
-> [Move' (RefInfo o) (ArgList o)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Cost
-> RefCreateEnv (RefInfo o) (ArgList o)
-> Move' (RefInfo o) (ArgList o)
forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
0) ([RefCreateEnv (RefInfo o) (ArgList o)]
 -> [Move' (RefInfo o) (ArgList o)])
-> [RefCreateEnv (RefInfo o) (ArgList o)]
-> [Move' (RefInfo o) (ArgList o)]
forall a b. (a -> b) -> a -> b
$
   [ ArgList o -> RefCreateEnv (RefInfo o) (ArgList o)
forall (m :: * -> *) a. Monad m => a -> m a
return ArgList o
forall o. ArgList o
ALNil, Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
cons Hiding
NotHidden, Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
cons Hiding
Hidden ]
   [RefCreateEnv (RefInfo o) (ArgList o)]
-> [RefCreateEnv (RefInfo o) (ArgList o)]
-> [RefCreateEnv (RefInfo o) (ArgList o)]
forall a. [a] -> [a] -> [a]
++ if [RefInfo o] -> Bool
getIsDep [RefInfo o]
infos then []
      else [ Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
proj Hiding
NotHidden, Hiding -> RefCreateEnv (RefInfo o) (ArgList o)
proj Hiding
Hidden ]

   where

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

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

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


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

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

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

  step :: ExpRefInfo o -> RefInfo o -> ExpRefInfo o
  step :: ExpRefInfo o -> RefInfo o -> ExpRefInfo o
step ExpRefInfo o
eri x :: RefInfo o
x@RIMainInfo{}           = ExpRefInfo o
eri { eriMain :: Maybe (RefInfo o)
eriMain  = RefInfo o -> Maybe (RefInfo o)
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 RefInfo o -> [RefInfo o] -> [RefInfo o]
forall a. a -> [a] -> [a]
: ExpRefInfo o -> [RefInfo o]
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 = ([UId o], [Elr o]) -> Maybe ([UId o], [Elr o])
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 = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
iota' } where
    iota' :: Bool
iota' = Bool
semif Bool -> Bool -> Bool
|| Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
False (ExpRefInfo o -> Maybe Bool
forall o. ExpRefInfo o -> Maybe Bool
eriIotaStep ExpRefInfo o
eri)
  step ExpRefInfo o
eri RefInfo o
RIPickSubsvar            = ExpRefInfo o
eri { eriPickSubsVar :: Bool
eriPickSubsVar = Bool
True }
  step ExpRefInfo o
eri (RIEqRState EqReasoningState
s)           = ExpRefInfo o
eri { eriEqRState :: Maybe EqReasoningState
eriEqRState = EqReasoningState -> Maybe EqReasoningState
forall a. a -> Maybe a
Just EqReasoningState
s }
  step ExpRefInfo o
eri RefInfo o
_ = ExpRefInfo o
forall a. HasCallStack => a
__IMPOSSIBLE__


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

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

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

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

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

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

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

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

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

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

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

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

-- | New spine of arguments potentially using placeholders

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

   ExpRefInfo { eriMain :: forall o. ExpRefInfo o -> Maybe (RefInfo o)
eriMain  = Just (RIMainInfo Nat
n HNExp o
tt Bool
iotastepdone)
              , eriUnifs :: forall o. ExpRefInfo o -> [RefInfo o]
eriUnifs = [RefInfo o]
unis
              , eriInfTypeUnknown :: forall o. ExpRefInfo o -> Bool
eriInfTypeUnknown = Bool
inftypeunknown
              , eriIsEliminand :: forall o. ExpRefInfo o -> Bool
eriIsEliminand = Bool
iseliminand
              , 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
              } = [RefInfo o] -> ExpRefInfo o
forall o. [RefInfo o] -> ExpRefInfo o
getinfo [RefInfo o]
infos

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

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

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

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

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

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

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


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

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

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

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

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

  where

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


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

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


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


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

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

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

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

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

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

prioProjIndex :: Prio
prioProjIndex = Prio
3000

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

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

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

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

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

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

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

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