Agda-2.6.3.20230930: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Auto.NarrowingSearch

Synopsis

Documentation

newtype Prio Source #

Constructors

Prio 

Fields

Instances

Instances details
Num Prio Source # 
Instance details

Defined in Agda.Auto.NarrowingSearch

Methods

(+) :: Prio -> Prio -> Prio

(-) :: Prio -> Prio -> Prio

(*) :: Prio -> Prio -> Prio

negate :: Prio -> Prio

abs :: Prio -> Prio

signum :: Prio -> Prio

fromInteger :: Integer -> Prio

Eq Prio Source # 
Instance details

Defined in Agda.Auto.NarrowingSearch

Methods

(==) :: Prio -> Prio -> Bool

(/=) :: Prio -> Prio -> Bool

Ord Prio Source # 
Instance details

Defined in Agda.Auto.NarrowingSearch

Methods

compare :: Prio -> Prio -> Ordering

(<) :: Prio -> Prio -> Bool

(<=) :: Prio -> Prio -> Bool

(>) :: Prio -> Prio -> Bool

(>=) :: Prio -> Prio -> Bool

max :: Prio -> Prio -> Prio

min :: Prio -> Prio -> Prio

class Trav a where Source #

Associated Types

type Block a Source #

Methods

trav :: Monad m => (forall b. TravWith b (Block a) => MM b (Block b) -> m ()) -> a -> m () Source #

Instances

Instances details
Trav (ArgList o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Associated Types

type Block (ArgList o) Source #

Methods

trav :: Monad m => (forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()) -> ArgList o -> m () Source #

Trav (Exp o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Associated Types

type Block (Exp o) Source #

Methods

trav :: Monad m => (forall b. TravWith b (Block (Exp o)) => MM b (Block b) -> m ()) -> Exp o -> m () Source #

Trav a => Trav [a] Source # 
Instance details

Defined in Agda.Auto.SearchControl

Associated Types

type Block [a] Source #

Methods

trav :: Monad m => (forall b. TravWith b (Block [a]) => MM b (Block b) -> m ()) -> [a] -> m () Source #

TravWith a blk => Trav (MM a blk) Source # 
Instance details

Defined in Agda.Auto.NarrowingSearch

Associated Types

type Block (MM a blk) Source #

Methods

trav :: Monad m => (forall b. TravWith b (Block (MM a blk)) => MM b (Block b) -> m ()) -> MM a blk -> m () Source #

Trav (TrBr a o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Associated Types

type Block (TrBr a o) Source #

Methods

trav :: Monad m => (forall b. TravWith b (Block (TrBr a o)) => MM b (Block b) -> m ()) -> TrBr a o -> m () Source #

Trav (MId, CExp o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Associated Types

type Block (MId, CExp o) Source #

Methods

trav :: Monad m => (forall b. TravWith b (Block (MId, CExp o)) => MM b (Block b) -> m ()) -> (MId, CExp o) -> m () Source #

type TravWith a blk = (Trav a, Block a ~ blk) Source #

Trav instance a with block type blk

data Term blk Source #

Constructors

forall a.TravWith a blk => Term a 

data Prop blk Source #

Result of type-checking.

Constructors

OK

Success.

Error String

Definite failure.

forall a. AddExtraRef String (Metavar a blk) (Move' blk a)

Experimental.

And (Maybe [Term blk]) (MetaEnv (PB blk)) (MetaEnv (PB blk))

Parallel conjunction of constraints.

Sidecondition (MetaEnv (PB blk)) (MetaEnv (PB blk))

Experimental, related to mcompoint. First arg is sidecondition.

Or Prio (MetaEnv (PB blk)) (MetaEnv (PB blk))

Forking proof on something that is not part of the term language. E.g. whether a term will reduce or not.

ConnectHandle (OKHandle blk) (MetaEnv (PB blk))

Obsolete.

data OKVal Source #

Constructors

OKVal 

Instances

Instances details
Refinable OKVal blk Source # 
Instance details

Defined in Agda.Auto.NarrowingSearch

Methods

refinements :: blk -> [blk] -> Metavar OKVal blk -> IO [Move' blk OKVal] Source #

type OKHandle blk = MM OKVal blk Source #

type OKMeta blk = Metavar OKVal blk Source #

data Metavar a blk Source #

Agsy's meta variables.

a the type of the metavariable (what it can be instantiated with). blk the search control information (e.g. the scope of the meta).

Constructors

Metavar 

Fields

  • mbind :: IORef (Maybe a)

    Maybe an instantiation (refinement). It is usually shallow, i.e., just one construct(or) with arguments again being metas.

  • mprincipalpresent :: IORef Bool

    Does this meta block a principal constraint (i.e., a type-checking constraint).

  • mobs :: IORef [(QPB a blk, Maybe (CTree blk))]

    List of observers, i.e., constraints blocked by this meta.

  • mcompoint :: IORef [SubConstraints blk]

    Used for experiments with independence of subproofs.

  • mextrarefs :: IORef [Move' blk a]

    Experimental.

Instances

Instances details
Eq (Metavar a blk) Source # 
Instance details

Defined in Agda.Auto.NarrowingSearch

Methods

(==) :: Metavar a blk -> Metavar a blk -> Bool

(/=) :: Metavar a blk -> Metavar a blk -> Bool

hequalMetavar :: Metavar a1 blk1 -> Metavar a2 bkl2 -> Bool Source #

newMeta :: IORef [SubConstraints blk] -> IO (Metavar a blk) Source #

initMeta :: IO (Metavar a blk) Source #

data CTree blk Source #

Constructors

CTree 

Fields

data SubConstraints blk Source #

Constructors

SubConstraints 

Fields

newCTree :: Maybe (CTree blk) -> IO (CTree blk) Source #

data PrioMeta blk Source #

Constructors

forall a.Refinable a blk => PrioMeta Prio (Metavar a blk) 
NoPrio Bool 

Instances

Instances details
Eq (PrioMeta blk) Source # 
Instance details

Defined in Agda.Auto.NarrowingSearch

Methods

(==) :: PrioMeta blk -> PrioMeta blk -> Bool

(/=) :: PrioMeta blk -> PrioMeta blk -> Bool

data Restore Source #

Constructors

forall a. Restore (IORef a) a 

type Undo = StateT [Restore] IO Source #

ureadIORef :: IORef a -> Undo a Source #

uwriteIORef :: IORef a -> a -> Undo () Source #

umodifyIORef :: IORef a -> (a -> a) -> Undo () Source #

ureadmodifyIORef :: IORef a -> (a -> a) -> Undo a Source #

runUndo :: Undo a -> IO a Source #

newtype RefCreateEnv blk a Source #

Constructors

RefCreateEnv 

Fields

Instances

Instances details
Applicative (RefCreateEnv blk) Source # 
Instance details

Defined in Agda.Auto.NarrowingSearch

Methods

pure :: a -> RefCreateEnv blk a

(<*>) :: RefCreateEnv blk (a -> b) -> RefCreateEnv blk a -> RefCreateEnv blk b #

liftA2 :: (a -> b -> c) -> RefCreateEnv blk a -> RefCreateEnv blk b -> RefCreateEnv blk c

(*>) :: RefCreateEnv blk a -> RefCreateEnv blk b -> RefCreateEnv blk b

(<*) :: RefCreateEnv blk a -> RefCreateEnv blk b -> RefCreateEnv blk a

Functor (RefCreateEnv blk) Source # 
Instance details

Defined in Agda.Auto.NarrowingSearch

Methods

fmap :: (a -> b) -> RefCreateEnv blk a -> RefCreateEnv blk b

(<$) :: a -> RefCreateEnv blk b -> RefCreateEnv blk a #

Monad (RefCreateEnv blk) Source # 
Instance details

Defined in Agda.Auto.NarrowingSearch

Methods

(>>=) :: RefCreateEnv blk a -> (a -> RefCreateEnv blk b) -> RefCreateEnv blk b

(>>) :: RefCreateEnv blk a -> RefCreateEnv blk b -> RefCreateEnv blk b

return :: a -> RefCreateEnv blk a

newtype Cost Source #

Constructors

Cost 

Fields

Instances

Instances details
Num Cost Source # 
Instance details

Defined in Agda.Auto.NarrowingSearch

Methods

(+) :: Cost -> Cost -> Cost

(-) :: Cost -> Cost -> Cost

(*) :: Cost -> Cost -> Cost

negate :: Cost -> Cost

abs :: Cost -> Cost

signum :: Cost -> Cost

fromInteger :: Integer -> Cost

Eq Cost Source # 
Instance details

Defined in Agda.Auto.NarrowingSearch

Methods

(==) :: Cost -> Cost -> Bool

(/=) :: Cost -> Cost -> Bool

Ord Cost Source # 
Instance details

Defined in Agda.Auto.NarrowingSearch

Methods

compare :: Cost -> Cost -> Ordering

(<) :: Cost -> Cost -> Bool

(<=) :: Cost -> Cost -> Bool

(>) :: Cost -> Cost -> Bool

(>=) :: Cost -> Cost -> Bool

max :: Cost -> Cost -> Cost

min :: Cost -> Cost -> Cost

data Move' blk a Source #

Constructors

Move 

Fields

class Refinable a blk where Source #

Methods

refinements :: blk -> [blk] -> Metavar a blk -> IO [Move' blk a] Source #

Instances

Instances details
Refinable Choice blk Source # 
Instance details

Defined in Agda.Auto.NarrowingSearch

Methods

refinements :: blk -> [blk] -> Metavar Choice blk -> IO [Move' blk Choice] Source #

Refinable OKVal blk Source # 
Instance details

Defined in Agda.Auto.NarrowingSearch

Methods

refinements :: blk -> [blk] -> Metavar OKVal blk -> IO [Move' blk OKVal] Source #

Refinable (ArgList o) (RefInfo o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Methods

refinements :: RefInfo o -> [RefInfo o] -> Metavar (ArgList o) (RefInfo o) -> IO [Move' (RefInfo o) (ArgList o)] Source #

Refinable (ConstRef o) (RefInfo o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Methods

refinements :: RefInfo o -> [RefInfo o] -> Metavar (ConstRef o) (RefInfo o) -> IO [Move' (RefInfo o) (ConstRef o)] Source #

Refinable (Exp o) (RefInfo o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Methods

refinements :: RefInfo o -> [RefInfo o] -> Metavar (Exp o) (RefInfo o) -> IO [Move' (RefInfo o) (Exp o)] Source #

Refinable (ICExp o) (RefInfo o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Methods

refinements :: RefInfo o -> [RefInfo o] -> Metavar (ICExp o) (RefInfo o) -> IO [Move' (RefInfo o) (ICExp o)] Source #

type BlkInfo blk = (Bool, Prio, Maybe blk) Source #

data MM a blk Source #

Constructors

NotM a 
Meta (Metavar a blk) 

Instances

Instances details
Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #

Conversion TOM Term (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Term -> TOM (MExp O) Source #

Conversion TOM Type (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (MExp O) Source #

Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) Source #

Conversion TOM [Clause] [([Pat O], MExp O)] Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: [Clause] -> TOM [([Pat O], MExp O)] Source #

Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: MM a (RefInfo O) -> MOT b Source #

LocalTerminationEnv (MArgList o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Methods

sizeAndBoundVars :: MArgList o -> (Sum Nat, [Nat]) Source #

LocalTerminationEnv (MExp o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Methods

sizeAndBoundVars :: MExp o -> (Sum Nat, [Nat]) Source #

Replace (Exp o) (MExp o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Associated Types

type ReplaceWith (Exp o) (MExp o) Source #

Methods

replace' :: Nat -> MExp (ReplaceWith (Exp o) (MExp o)) -> Exp o -> Reader (Nat, Nat) (MExp o) Source #

Refinable (ICExp o) (RefInfo o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Methods

refinements :: RefInfo o -> [RefInfo o] -> Metavar (ICExp o) (RefInfo o) -> IO [Move' (RefInfo o) (ICExp o)] Source #

Lift t => Lift (MM t r) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Methods

lift' :: Nat -> Nat -> MM t r -> MM t r Source #

(Unify t, o ~ UnifiesTo t) => Unify (MM t (RefInfo o)) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Associated Types

type UnifiesTo (MM t (RefInfo o)) Source #

Methods

unify' :: MM t (RefInfo o) -> MM t (RefInfo o) -> StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) Maybe () Source #

notequal' :: MM t (RefInfo o) -> MM t (RefInfo o) -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) IO) Bool Source #

TravWith a blk => Trav (MM a blk) Source # 
Instance details

Defined in Agda.Auto.NarrowingSearch

Associated Types

type Block (MM a blk) Source #

Methods

trav :: Monad m => (forall b. TravWith b (Block (MM a blk)) => MM b (Block b) -> m ()) -> MM a blk -> m () Source #

Trav (MId, CExp o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Associated Types

type Block (MId, CExp o) Source #

Methods

trav :: Monad m => (forall b. TravWith b (Block (MId, CExp o)) => MM b (Block b) -> m ()) -> (MId, CExp o) -> m () Source #

ExpandMetas t => ExpandMetas (MM t a) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

expandMetas :: MM t a -> IO (MM t a) Source #

FreeVars t => FreeVars (MM t a) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

freeVarsOffset :: Nat -> MM t a -> Set Nat Source #

MetaliseOKH t => MetaliseOKH (MM t a) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

metaliseOKH :: MM t a -> IO (MM t a) Source #

Renaming t => Renaming (MM t a) Source # 
Instance details

Defined in Agda.Auto.Syntax

Methods

renameOffset :: Nat -> (Nat -> Nat) -> MM t a -> MM t a Source #

Replace t u => Replace (MM t (RefInfo o)) u Source # 
Instance details

Defined in Agda.Auto.CaseSplit

Associated Types

type ReplaceWith (MM t (RefInfo o)) u Source #

Methods

replace' :: Nat -> MExp (ReplaceWith (MM t (RefInfo o)) u) -> MM t (RefInfo o) -> Reader (Nat, Nat) u Source #

type ReplaceWith (Exp o) (MExp o) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

type ReplaceWith (Exp o) (MExp o) = o
type UnifiesTo (MM t (RefInfo o)) Source # 
Instance details

Defined in Agda.Auto.CaseSplit

type UnifiesTo (MM t (RefInfo o)) = o
type Block (MM a blk) Source # 
Instance details

Defined in Agda.Auto.NarrowingSearch

type Block (MM a blk) = blk
type Block (MId, CExp o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

type Block (MId, CExp o) = RefInfo o
type ReplaceWith (MM t (RefInfo o)) u Source # 
Instance details

Defined in Agda.Auto.CaseSplit

type ReplaceWith (MM t (RefInfo o)) u = ReplaceWith t u

rm :: Empty -> MM a b -> a Source #

type MetaEnv = IO Source #

data MB a blk Source #

Constructors

NotB a 
forall b.Refinable b blk => Blocked (Metavar b blk) (MetaEnv (MB a blk)) 
Failed String 

data PB blk Source #

Constructors

NotPB (Prop blk) 
forall b.Refinable b blk => PBlocked (Metavar b blk) (BlkInfo blk) (MetaEnv (PB blk)) 
forall b1 b2.(Refinable b1 blk, Refinable b2 blk) => PDoubleBlocked (Metavar b1 blk) (Metavar b2 blk) (MetaEnv (PB blk)) 

data QPB b blk Source #

Constructors

QPBlocked (BlkInfo blk) (MetaEnv (PB blk)) 
QPDoubleBlocked (IORef Bool) (MetaEnv (PB blk)) 

mmcase :: Refinable a blk => MM a blk -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk) Source #

mmmcase :: MM a blk -> MetaEnv (MB b blk) -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk) Source #

mmpcase :: Refinable a blk => BlkInfo blk -> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk) Source #

doubleblock :: (Refinable a blk, Refinable b blk) => MM a blk -> MM b blk -> MetaEnv (PB blk) -> MetaEnv (PB blk) Source #

mbcase :: MetaEnv (MB a blk) -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk) Source #

mbpcase :: Prio -> Maybe blk -> MetaEnv (MB a blk) -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk) Source #

mmbpcase :: MetaEnv (MB a blk) -> (forall b. Refinable b blk => MM b blk -> MetaEnv (PB blk)) -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk) Source #

waitok :: OKHandle blk -> MetaEnv (MB b blk) -> MetaEnv (MB b blk) Source #

mbret :: a -> MetaEnv (MB a blk) Source #

mbfailed :: String -> MetaEnv (MB a blk) Source #

mpret :: Prop blk -> MetaEnv (PB blk) Source #

expandbind :: MM a blk -> MetaEnv (MM a blk) Source #

type HandleSol = IO () Source #

type SRes = Either Bool Int Source #

topSearch :: forall blk. IORef Int -> IORef Int -> HandleSol -> blk -> MetaEnv (PB blk) -> Cost -> Cost -> IO Bool Source #

extractblkinfos :: Metavar a blk -> IO [blk] Source #

recalcs :: [(QPB a blk, Maybe (CTree blk))] -> Undo Bool Source #

seqc :: Undo Bool -> Undo Bool -> Undo Bool Source #

recalc :: (QPB a blk, Maybe (CTree blk)) -> Undo Bool Source #

reccalc :: MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo Bool Source #

calc :: forall blk. MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo (Maybe [OKMeta blk]) Source #

choosePrioMeta :: Bool -> PrioMeta blk -> PrioMeta blk -> PrioMeta blk Source #

data Choice Source #

Instances

Instances details
Refinable Choice blk Source # 
Instance details

Defined in Agda.Auto.NarrowingSearch

Methods

refinements :: blk -> [blk] -> Metavar Choice blk -> IO [Move' blk Choice] Source #

choose :: MM Choice blk -> Prio -> MetaEnv (PB blk) -> MetaEnv (PB blk) -> MetaEnv (PB blk) Source #