Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

Agda.Auto.NarrowingSearch

Synopsis

Documentation

newtype Prio Source #

Constructors

Prio 

Fields

Instances
Eq Prio Source # 
Instance details

Defined in Agda.Auto.NarrowingSearch

Methods

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

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

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

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 blk | a -> blk where Source #

Methods

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

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

Defined in Agda.Auto.SearchControl

Methods

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

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

Defined in Agda.Auto.SearchControl

Methods

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

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

Defined in Agda.Auto.SearchControl

Methods

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

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

Defined in Agda.Auto.NarrowingSearch

Methods

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

Trav (MId, CExp o) (RefInfo o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Methods

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

Trav (TrBr a o) (RefInfo o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Methods

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

data Term blk Source #

Constructors

Trav a blk => Term a 

data Prop blk Source #

Result of type-checking.

Constructors

OK

Success.

Error String

Definite failure.

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
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
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

Refinable a blk => PrioMeta Prio (Metavar a blk) 
NoPrio Bool 
Instances
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

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
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

fail :: String -> 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 #

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

newtype Cost Source #

Constructors

Cost 

Fields

Instances
Eq Cost Source # 
Instance details

Defined in Agda.Auto.NarrowingSearch

Methods

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

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

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

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
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 (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 #

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 (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 (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 #

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

data MM a blk Source #

Constructors

NotM a 
Meta (Metavar a blk) 
Instances
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 Type (MExp O) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (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 Args (MM (ArgList O) (RefInfo O)) Source # 
Instance details

Defined in Agda.Auto.Convert

Methods

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

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

Defined in Agda.Auto.CaseSplit

Methods

replace' :: Nat -> MExp o -> Exp o -> Reader (Nat, Nat) (MExp 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 #

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

Defined in Agda.Auto.CaseSplit

Methods

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

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

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

Defined in Agda.Auto.CaseSplit

Methods

replace' :: Nat -> MExp o -> MM t (RefInfo o) -> Reader (Nat, Nat) u 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 #

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 #

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 #

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

Defined in Agda.Auto.Syntax

Methods

freeVarsOffset :: Nat -> MM t a -> Set Nat 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 #

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

Defined in Agda.Auto.Syntax

Methods

metaliseOKH :: MM t a -> IO (MM t a) 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 #

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

Defined in Agda.Auto.NarrowingSearch

Methods

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

Trav (MId, CExp o) (RefInfo o) Source # 
Instance details

Defined in Agda.Auto.SearchControl

Methods

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

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

type MetaEnv = IO Source #

data MB a blk Source #

Constructors

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

data PB blk Source #

Constructors

NotPB (Prop blk) 
Refinable b blk => PBlocked (Metavar b blk) (BlkInfo blk) (MetaEnv (PB blk)) 
(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
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 #