Hets - the Heterogeneous Tool Set
Copyright(c) Till Mossakowski Klaus Luettich Uni Bremen 2002-2005
LicenseGPLv2 or higher, see LICENSE.txt
Maintainertill@informatik.uni-bremen.de
Stabilityprovisional
Portabilitynon-portable (deriving Typeable)
Safe HaskellNone

Logic.Prover

Description

General datastructures for theorem prover interfaces

Synopsis

pack sentences with their proofs

type SenStatus a tStatus = SenAttr a (ThmStatus tStatus) Source #

instead of the sentence name (that will be the key into the order map) the theorem status will be stored as attribute. The theorem status will be a (wrapped) list of pairs (AnyComorphism, BasicProof) in G_theory, but a wrapped list of (ProofStatus proof_tree) in a logic specific Theory.

thmStatus :: SenStatus a tStatus -> [tStatus] Source #

data ThmStatus a Source #

the wrapped list of proof scripts or (AnyComorphism, BasicProof) pairs

Constructors

ThmStatus 

Fields

Instances

Instances details
Eq a => Eq (ThmStatus a) Source # 
Instance details

Defined in Logic.Prover

Methods

(==) :: ThmStatus a -> ThmStatus a -> Bool

(/=) :: ThmStatus a -> ThmStatus a -> Bool

Ord a => Ord (ThmStatus a) Source # 
Instance details

Defined in Logic.Prover

Methods

compare :: ThmStatus a -> ThmStatus a -> Ordering

(<) :: ThmStatus a -> ThmStatus a -> Bool

(<=) :: ThmStatus a -> ThmStatus a -> Bool

(>) :: ThmStatus a -> ThmStatus a -> Bool

(>=) :: ThmStatus a -> ThmStatus a -> Bool

max :: ThmStatus a -> ThmStatus a -> ThmStatus a

min :: ThmStatus a -> ThmStatus a -> ThmStatus a

Show a => Show (ThmStatus a) Source # 
Instance details

Defined in Logic.Prover

Methods

showsPrec :: Int -> ThmStatus a -> ShowS

show :: ThmStatus a -> String

showList :: [ThmStatus a] -> ShowS

Generic (ThmStatus a) 
Instance details

Defined in ATC.Prover

Associated Types

type Rep (ThmStatus a) :: Type -> Type

Methods

from :: ThmStatus a -> Rep (ThmStatus a) x

to :: Rep (ThmStatus a) x -> ThmStatus a

FromJSON a => FromJSON (ThmStatus a) 
Instance details

Defined in ATC.Prover

Methods

parseJSON :: Value -> Parser (ThmStatus a)

parseJSONList :: Value -> Parser [ThmStatus a]

ToJSON a => ToJSON (ThmStatus a) 
Instance details

Defined in ATC.Prover

Methods

toJSON :: ThmStatus a -> Value

toEncoding :: ThmStatus a -> Encoding

toJSONList :: [ThmStatus a] -> Value

toEncodingList :: [ThmStatus a] -> Encoding

ShATermConvertible a => ShATermConvertible (ThmStatus a) 
Instance details

Defined in ATC.Prover

Methods

toShATermAux :: ATermTable -> ThmStatus a -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [ThmStatus a] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, ThmStatus a)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [ThmStatus a])

ShATermLG a => ShATermLG (ThmStatus a) Source # 
Instance details

Defined in ATC.Grothendieck

Methods

toShATermLG :: ATermTable -> ThmStatus a -> IO (ATermTable, Int) Source #

fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, ThmStatus a) Source #

type Rep (ThmStatus a) 
Instance details

Defined in ATC.Prover

type Rep (ThmStatus a) = D1 ('MetaData "ThmStatus" "Logic.Prover" "main" 'False) (C1 ('MetaCons "ThmStatus" 'PrefixI 'True) (S1 ('MetaSel ('Just "getThmStatus") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [a])))

type ThSens a b = OMap String (SenStatus a b) Source #

the map from labels to the theorem plus status (and position)

mapThSensValueM :: Monad m => (a -> m b) -> ThSens a c -> m (ThSens b c) Source #

joinSensAux :: (Ord a, Eq b) => ThSens a b -> ThSens a b -> (ThSens a b, [(String, String)]) Source #

join and disambiguate

  • separate Axioms from Theorems
  • don't merge sentences with same key but different contents?

joinSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b -> ThSens a b Source #

intersectSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b -> ThSens a b Source #

reduceSens :: (Ord a, Eq b) => ThSens a b -> ThSens a b Source #

cmpSnd :: Ord a1 => (String, ElemWOrd (SenStatus a1 b)) -> (String, ElemWOrd (SenStatus a1 b)) -> Ordering Source #

cmpSenEle :: Ord a1 => ElemWOrd (SenStatus a1 b) -> ElemWOrd (SenStatus a1 b) -> Ordering Source #

mapValue :: (a -> b) -> SenStatus a c -> SenStatus b c Source #

markAsAxiom :: Ord a => Bool -> ThSens a b -> ThSens a b Source #

sets the field isAxiom according to the boolean value; if isAxiom is False for a sentence and set to True, the field wasTheorem is set to True.

markAsGoal :: Ord a => ThSens a b -> ThSens a b Source #

toNamed :: String -> SenStatus a b -> Named a Source #

toThSens :: Ord a => [Named a] -> ThSens a b Source #

putting Sentences from a list into a map

data Theory sign sen proof_tree Source #

theories with a signature and sentences with proof states

Constructors

Theory sign (ThSens sen (ProofStatus proof_tree)) 

Instances

Instances details
Generic (Theory sign sen proof_tree) 
Instance details

Defined in ATC.Prover

Associated Types

type Rep (Theory sign sen proof_tree) :: Type -> Type

Methods

from :: Theory sign sen proof_tree -> Rep (Theory sign sen proof_tree) x

to :: Rep (Theory sign sen proof_tree) x -> Theory sign sen proof_tree

(FromJSON sign, FromJSON sen, FromJSON proof_tree) => FromJSON (Theory sign sen proof_tree) 
Instance details

Defined in ATC.Prover

Methods

parseJSON :: Value -> Parser (Theory sign sen proof_tree)

parseJSONList :: Value -> Parser [Theory sign sen proof_tree]

(ToJSON sign, ToJSON sen, ToJSON proof_tree) => ToJSON (Theory sign sen proof_tree) 
Instance details

Defined in ATC.Prover

Methods

toJSON :: Theory sign sen proof_tree -> Value

toEncoding :: Theory sign sen proof_tree -> Encoding

toJSONList :: [Theory sign sen proof_tree] -> Value

toEncodingList :: [Theory sign sen proof_tree] -> Encoding

(ShATermConvertible sign, ShATermConvertible sen, ShATermConvertible proof_tree) => ShATermConvertible (Theory sign sen proof_tree) 
Instance details

Defined in ATC.Prover

Methods

toShATermAux :: ATermTable -> Theory sign sen proof_tree -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Theory sign sen proof_tree] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Theory sign sen proof_tree)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Theory sign sen proof_tree])

type Rep (Theory sign sen proof_tree) 
Instance details

Defined in ATC.Prover

type Rep (Theory sign sen proof_tree) = D1 ('MetaData "Theory" "Logic.Prover" "main" 'False) (C1 ('MetaCons "Theory" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 sign) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ThSens sen (ProofStatus proof_tree)))))

data TacticScript Source #

Constructors

TacticScript String 

Instances

Instances details
Eq TacticScript Source # 
Instance details

Defined in Logic.Prover

Methods

(==) :: TacticScript -> TacticScript -> Bool

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

Ord TacticScript Source # 
Instance details

Defined in Logic.Prover

Show TacticScript Source # 
Instance details

Defined in Logic.Prover

Methods

showsPrec :: Int -> TacticScript -> ShowS

show :: TacticScript -> String

showList :: [TacticScript] -> ShowS

Generic TacticScript 
Instance details

Defined in ATC.Prover

Associated Types

type Rep TacticScript :: Type -> Type

FromJSON TacticScript 
Instance details

Defined in ATC.Prover

Methods

parseJSON :: Value -> Parser TacticScript

parseJSONList :: Value -> Parser [TacticScript]

ToJSON TacticScript 
Instance details

Defined in ATC.Prover

Methods

toJSON :: TacticScript -> Value

toEncoding :: TacticScript -> Encoding

toJSONList :: [TacticScript] -> Value

toEncodingList :: [TacticScript] -> Encoding

ShATermConvertible TacticScript 
Instance details

Defined in ATC.Prover

Methods

toShATermAux :: ATermTable -> TacticScript -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TacticScript] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TacticScript)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TacticScript])

type Rep TacticScript 
Instance details

Defined in ATC.Prover

type Rep TacticScript = D1 ('MetaData "TacticScript" "Logic.Prover" "main" 'False) (C1 ('MetaCons "TacticScript" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))

data Reason Source #

failure reason

Constructors

Reason [String] 

Instances

Instances details
Eq Reason Source # 
Instance details

Defined in Logic.Prover

Methods

(==) :: Reason -> Reason -> Bool

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

Ord Reason Source # 
Instance details

Defined in Logic.Prover

Methods

compare :: Reason -> Reason -> Ordering

(<) :: Reason -> Reason -> Bool

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

(>) :: Reason -> Reason -> Bool

(>=) :: Reason -> Reason -> Bool

max :: Reason -> Reason -> Reason

min :: Reason -> Reason -> Reason

Generic Reason 
Instance details

Defined in ATC.Prover

Associated Types

type Rep Reason :: Type -> Type

Methods

from :: Reason -> Rep Reason x

to :: Rep Reason x -> Reason

FromJSON Reason 
Instance details

Defined in ATC.Prover

Methods

parseJSON :: Value -> Parser Reason

parseJSONList :: Value -> Parser [Reason]

ToJSON Reason 
Instance details

Defined in ATC.Prover

Methods

toJSON :: Reason -> Value

toEncoding :: Reason -> Encoding

toJSONList :: [Reason] -> Value

toEncodingList :: [Reason] -> Encoding

ShATermConvertible Reason 
Instance details

Defined in ATC.Prover

Methods

toShATermAux :: ATermTable -> Reason -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [Reason] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, Reason)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [Reason])

type Rep Reason 
Instance details

Defined in ATC.Prover

type Rep Reason = D1 ('MetaData "Reason" "Logic.Prover" "main" 'False) (C1 ('MetaCons "Reason" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])))

data GoalStatus Source #

enumeration type representing the status of a goal

Constructors

Open Reason

failure reason

Disproved 
Proved Bool

True means consistent; False inconsistent

Instances

Instances details
Eq GoalStatus Source # 
Instance details

Defined in Logic.Prover

Methods

(==) :: GoalStatus -> GoalStatus -> Bool

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

Ord GoalStatus Source # 
Instance details

Defined in Logic.Prover

Show GoalStatus Source # 
Instance details

Defined in Logic.Prover

Methods

showsPrec :: Int -> GoalStatus -> ShowS

show :: GoalStatus -> String

showList :: [GoalStatus] -> ShowS

Generic GoalStatus 
Instance details

Defined in ATC.Prover

Associated Types

type Rep GoalStatus :: Type -> Type

Methods

from :: GoalStatus -> Rep GoalStatus x

to :: Rep GoalStatus x -> GoalStatus

FromJSON GoalStatus 
Instance details

Defined in ATC.Prover

Methods

parseJSON :: Value -> Parser GoalStatus

parseJSONList :: Value -> Parser [GoalStatus]

ToJSON GoalStatus 
Instance details

Defined in ATC.Prover

Methods

toJSON :: GoalStatus -> Value

toEncoding :: GoalStatus -> Encoding

toJSONList :: [GoalStatus] -> Value

toEncodingList :: [GoalStatus] -> Encoding

ShATermConvertible GoalStatus 
Instance details

Defined in ATC.Prover

Methods

toShATermAux :: ATermTable -> GoalStatus -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [GoalStatus] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, GoalStatus)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [GoalStatus])

type Rep GoalStatus 
Instance details

Defined in ATC.Prover

type Rep GoalStatus = D1 ('MetaData "GoalStatus" "Logic.Prover" "main" 'False) (C1 ('MetaCons "Open" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Reason)) :+: (C1 ('MetaCons "Disproved" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Proved" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))

data ProofStatus proof_tree Source #

data type representing the proof status for a goal

Constructors

ProofStatus 

Fields

Instances

Instances details
Eq proof_tree => Eq (ProofStatus proof_tree) Source # 
Instance details

Defined in Logic.Prover

Methods

(==) :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool

(/=) :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool

Ord proof_tree => Ord (ProofStatus proof_tree) Source # 
Instance details

Defined in Logic.Prover

Methods

compare :: ProofStatus proof_tree -> ProofStatus proof_tree -> Ordering

(<) :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool

(<=) :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool

(>) :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool

(>=) :: ProofStatus proof_tree -> ProofStatus proof_tree -> Bool

max :: ProofStatus proof_tree -> ProofStatus proof_tree -> ProofStatus proof_tree

min :: ProofStatus proof_tree -> ProofStatus proof_tree -> ProofStatus proof_tree

Show proof_tree => Show (ProofStatus proof_tree) Source # 
Instance details

Defined in Logic.Prover

Methods

showsPrec :: Int -> ProofStatus proof_tree -> ShowS

show :: ProofStatus proof_tree -> String

showList :: [ProofStatus proof_tree] -> ShowS

Generic (ProofStatus proof_tree) 
Instance details

Defined in ATC.Prover

Associated Types

type Rep (ProofStatus proof_tree) :: Type -> Type

Methods

from :: ProofStatus proof_tree -> Rep (ProofStatus proof_tree) x

to :: Rep (ProofStatus proof_tree) x -> ProofStatus proof_tree

FromJSON proof_tree => FromJSON (ProofStatus proof_tree) 
Instance details

Defined in ATC.Prover

Methods

parseJSON :: Value -> Parser (ProofStatus proof_tree)

parseJSONList :: Value -> Parser [ProofStatus proof_tree]

ToJSON proof_tree => ToJSON (ProofStatus proof_tree) 
Instance details

Defined in ATC.Prover

Methods

toJSON :: ProofStatus proof_tree -> Value

toEncoding :: ProofStatus proof_tree -> Encoding

toJSONList :: [ProofStatus proof_tree] -> Value

toEncodingList :: [ProofStatus proof_tree] -> Encoding

ShATermConvertible proof_tree => ShATermConvertible (ProofStatus proof_tree) 
Instance details

Defined in ATC.Prover

Methods

toShATermAux :: ATermTable -> ProofStatus proof_tree -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [ProofStatus proof_tree] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, ProofStatus proof_tree)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [ProofStatus proof_tree])

type Rep (ProofStatus proof_tree) 
Instance details

Defined in ATC.Prover

type Rep (ProofStatus proof_tree) = D1 ('MetaData "ProofStatus" "Logic.Prover" "main" 'False) (C1 ('MetaCons "ProofStatus" 'PrefixI 'True) (((S1 ('MetaSel ('Just "goalName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: S1 ('MetaSel ('Just "goalStatus") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GoalStatus)) :*: (S1 ('MetaSel ('Just "usedAxioms") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String]) :*: S1 ('MetaSel ('Just "usedProver") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) :*: ((S1 ('MetaSel ('Just "proofTree") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 proof_tree) :*: S1 ('MetaSel ('Just "usedTime") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TimeOfDay)) :*: (S1 ('MetaSel ('Just "tacticScript") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TacticScript) :*: S1 ('MetaSel ('Just "proofLines") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [String])))))

openProofStatus Source #

Arguments

:: Ord pt 
=> String

name of the goal

-> String

name of the prover

-> pt 
-> ProofStatus pt 

constructs an open proof status with basic information filled in; make sure to set proofTree to a useful value before you access it.

isProvedStat :: ProofStatus proof_tree -> Bool Source #

data ProverKind Source #

different kinds of prover interfaces

Instances

Instances details
Generic ProverKind 
Instance details

Defined in ATC.Prover

Associated Types

type Rep ProverKind :: Type -> Type

Methods

from :: ProverKind -> Rep ProverKind x

to :: Rep ProverKind x -> ProverKind

FromJSON ProverKind 
Instance details

Defined in ATC.Prover

Methods

parseJSON :: Value -> Parser ProverKind

parseJSONList :: Value -> Parser [ProverKind]

ToJSON ProverKind 
Instance details

Defined in ATC.Prover

Methods

toJSON :: ProverKind -> Value

toEncoding :: ProverKind -> Encoding

toJSONList :: [ProverKind] -> Value

toEncodingList :: [ProverKind] -> Encoding

ShATermConvertible ProverKind 
Instance details

Defined in ATC.Prover

Methods

toShATermAux :: ATermTable -> ProverKind -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [ProverKind] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, ProverKind)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [ProverKind])

type Rep ProverKind 
Instance details

Defined in ATC.Prover

type Rep ProverKind = D1 ('MetaData "ProverKind" "Logic.Prover" "main" 'False) (C1 ('MetaCons "ProveGUI" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ProveCMDLautomatic" 'PrefixI 'False) (U1 :: Type -> Type))

hasProverKind :: ProverKind -> ProverTemplate x s m y z -> Bool Source #

determine if a prover kind is implemented

data FreeDefMorphism sentence morphism Source #

Constructors

FreeDefMorphism 

Fields

Instances

Instances details
(Eq morphism, Eq sentence) => Eq (FreeDefMorphism sentence morphism) Source # 
Instance details

Defined in Logic.Prover

Methods

(==) :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> Bool

(/=) :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> Bool

(Ord morphism, Ord sentence) => Ord (FreeDefMorphism sentence morphism) Source # 
Instance details

Defined in Logic.Prover

Methods

compare :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> Ordering

(<) :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> Bool

(<=) :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> Bool

(>) :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> Bool

(>=) :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> Bool

max :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism

min :: FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism -> FreeDefMorphism sentence morphism

(Show morphism, Show sentence) => Show (FreeDefMorphism sentence morphism) Source # 
Instance details

Defined in Logic.Prover

Methods

showsPrec :: Int -> FreeDefMorphism sentence morphism -> ShowS

show :: FreeDefMorphism sentence morphism -> String

showList :: [FreeDefMorphism sentence morphism] -> ShowS

Generic (FreeDefMorphism sentence morphism) 
Instance details

Defined in ATC.Prover

Associated Types

type Rep (FreeDefMorphism sentence morphism) :: Type -> Type

Methods

from :: FreeDefMorphism sentence morphism -> Rep (FreeDefMorphism sentence morphism) x

to :: Rep (FreeDefMorphism sentence morphism) x -> FreeDefMorphism sentence morphism

(FromJSON sentence, FromJSON morphism) => FromJSON (FreeDefMorphism sentence morphism) 
Instance details

Defined in ATC.Prover

Methods

parseJSON :: Value -> Parser (FreeDefMorphism sentence morphism)

parseJSONList :: Value -> Parser [FreeDefMorphism sentence morphism]

(ToJSON sentence, ToJSON morphism) => ToJSON (FreeDefMorphism sentence morphism) 
Instance details

Defined in ATC.Prover

Methods

toJSON :: FreeDefMorphism sentence morphism -> Value

toEncoding :: FreeDefMorphism sentence morphism -> Encoding

toJSONList :: [FreeDefMorphism sentence morphism] -> Value

toEncodingList :: [FreeDefMorphism sentence morphism] -> Encoding

(ShATermConvertible sentence, ShATermConvertible morphism) => ShATermConvertible (FreeDefMorphism sentence morphism) 
Instance details

Defined in ATC.Prover

Methods

toShATermAux :: ATermTable -> FreeDefMorphism sentence morphism -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [FreeDefMorphism sentence morphism] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, FreeDefMorphism sentence morphism)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [FreeDefMorphism sentence morphism])

type Rep (FreeDefMorphism sentence morphism) 
Instance details

Defined in ATC.Prover

type Rep (FreeDefMorphism sentence morphism) = D1 ('MetaData "FreeDefMorphism" "Logic.Prover" "main" 'False) (C1 ('MetaCons "FreeDefMorphism" 'PrefixI 'True) ((S1 ('MetaSel ('Just "freeDefMorphism") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 morphism) :*: S1 ('MetaSel ('Just "pathFromFreeDef") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 morphism)) :*: (S1 ('MetaSel ('Just "freeTheory") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Named sentence]) :*: S1 ('MetaSel ('Just "isCofree") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))))

data ProverTemplate theory sentence morphism sublogics proof_tree Source #

prover or consistency checker

Constructors

Prover 

Fields

type Prover sign sentence morphism sublogics proof_tree = ProverTemplate (Theory sign sentence proof_tree) sentence morphism sublogics proof_tree Source #

mkProverTemplate :: String -> sublogics -> (String -> theory -> [FreeDefMorphism sentence morphism] -> IO [ProofStatus proof_tree]) -> ProverTemplate theory sentence morphism sublogics proof_tree Source #

mkUsableProver :: String -> String -> sublogics -> (String -> theory -> [FreeDefMorphism sentence morphism] -> IO [ProofStatus proof_tree]) -> ProverTemplate theory sentence morphism sublogics proof_tree Source #

mkAutomaticProver :: String -> String -> sublogics -> (String -> theory -> [FreeDefMorphism sentence morphism] -> IO [ProofStatus proof_tree]) -> (Bool -> Bool -> MVar (Result [ProofStatus proof_tree]) -> String -> TacticScript -> theory -> [FreeDefMorphism sentence morphism] -> IO (ThreadId, MVar ())) -> ProverTemplate theory sentence morphism sublogics proof_tree Source #

data TheoryMorphism sign sen mor proof_tree Source #

theory morphisms between two theories

Constructors

TheoryMorphism 

Fields

Instances

Instances details
Generic (TheoryMorphism sign sen mor proof_tree) 
Instance details

Defined in ATC.Prover

Associated Types

type Rep (TheoryMorphism sign sen mor proof_tree) :: Type -> Type

Methods

from :: TheoryMorphism sign sen mor proof_tree -> Rep (TheoryMorphism sign sen mor proof_tree) x

to :: Rep (TheoryMorphism sign sen mor proof_tree) x -> TheoryMorphism sign sen mor proof_tree

(FromJSON sign, FromJSON sen, FromJSON mor, FromJSON proof_tree) => FromJSON (TheoryMorphism sign sen mor proof_tree) 
Instance details

Defined in ATC.Prover

Methods

parseJSON :: Value -> Parser (TheoryMorphism sign sen mor proof_tree)

parseJSONList :: Value -> Parser [TheoryMorphism sign sen mor proof_tree]

(ToJSON sign, ToJSON sen, ToJSON mor, ToJSON proof_tree) => ToJSON (TheoryMorphism sign sen mor proof_tree) 
Instance details

Defined in ATC.Prover

Methods

toJSON :: TheoryMorphism sign sen mor proof_tree -> Value

toEncoding :: TheoryMorphism sign sen mor proof_tree -> Encoding

toJSONList :: [TheoryMorphism sign sen mor proof_tree] -> Value

toEncodingList :: [TheoryMorphism sign sen mor proof_tree] -> Encoding

(ShATermConvertible sign, ShATermConvertible sen, ShATermConvertible mor, ShATermConvertible proof_tree) => ShATermConvertible (TheoryMorphism sign sen mor proof_tree) 
Instance details

Defined in ATC.Prover

Methods

toShATermAux :: ATermTable -> TheoryMorphism sign sen mor proof_tree -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [TheoryMorphism sign sen mor proof_tree] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, TheoryMorphism sign sen mor proof_tree)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [TheoryMorphism sign sen mor proof_tree])

type Rep (TheoryMorphism sign sen mor proof_tree) 
Instance details

Defined in ATC.Prover

type Rep (TheoryMorphism sign sen mor proof_tree) = D1 ('MetaData "TheoryMorphism" "Logic.Prover" "main" 'False) (C1 ('MetaCons "TheoryMorphism" 'PrefixI 'True) (S1 ('MetaSel ('Just "tSource") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Theory sign sen proof_tree)) :*: (S1 ('MetaSel ('Just "tTarget") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Theory sign sen proof_tree)) :*: S1 ('MetaSel ('Just "tMorphism") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 mor))))

data CCStatus proof_tree Source #

Constructors

CCStatus 

Fields

Instances

Instances details
Generic (CCStatus proof_tree) 
Instance details

Defined in ATC.Prover

Associated Types

type Rep (CCStatus proof_tree) :: Type -> Type

Methods

from :: CCStatus proof_tree -> Rep (CCStatus proof_tree) x

to :: Rep (CCStatus proof_tree) x -> CCStatus proof_tree

FromJSON proof_tree => FromJSON (CCStatus proof_tree) 
Instance details

Defined in ATC.Prover

Methods

parseJSON :: Value -> Parser (CCStatus proof_tree)

parseJSONList :: Value -> Parser [CCStatus proof_tree]

ToJSON proof_tree => ToJSON (CCStatus proof_tree) 
Instance details

Defined in ATC.Prover

Methods

toJSON :: CCStatus proof_tree -> Value

toEncoding :: CCStatus proof_tree -> Encoding

toJSONList :: [CCStatus proof_tree] -> Value

toEncodingList :: [CCStatus proof_tree] -> Encoding

ShATermConvertible proof_tree => ShATermConvertible (CCStatus proof_tree) 
Instance details

Defined in ATC.Prover

Methods

toShATermAux :: ATermTable -> CCStatus proof_tree -> IO (ATermTable, Int)

toShATermList' :: ATermTable -> [CCStatus proof_tree] -> IO (ATermTable, Int)

fromShATermAux :: Int -> ATermTable -> (ATermTable, CCStatus proof_tree)

fromShATermList' :: Int -> ATermTable -> (ATermTable, [CCStatus proof_tree])

type Rep (CCStatus proof_tree) 
Instance details

Defined in ATC.Prover

type Rep (CCStatus proof_tree) = D1 ('MetaData "CCStatus" "Logic.Prover" "main" 'False) (C1 ('MetaCons "CCStatus" 'PrefixI 'True) (S1 ('MetaSel ('Just "ccProofTree") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 proof_tree) :*: (S1 ('MetaSel ('Just "ccUsedTime") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TimeOfDay) :*: S1 ('MetaSel ('Just "ccResult") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool)))))

data ConsChecker sign sentence sublogics morphism proof_tree Source #

Constructors

ConsChecker 

Fields

mkConsChecker :: String -> sublogics -> (String -> TacticScript -> TheoryMorphism sign sentence morphism proof_tree -> [FreeDefMorphism sentence morphism] -> IO (CCStatus proof_tree)) -> ConsChecker sign sentence sublogics morphism proof_tree Source #

mkUsableConsChecker :: String -> String -> sublogics -> (String -> TacticScript -> TheoryMorphism sign sentence morphism proof_tree -> [FreeDefMorphism sentence morphism] -> IO (CCStatus proof_tree)) -> ConsChecker sign sentence sublogics morphism proof_tree Source #

Orphan instances

Pretty a => Pretty (ElemWOrd a) Source # 
Instance details