Copyright	(c) Till Mossakowski Uni Bremen 2002-2006
License	GPLv2 or higher, see LICENSE.txt
Maintainer	till@informatik.uni-bremen.de
Stability	provisional
Portability	non-portable(Logic)
Safe Haskell	None

Static.GTheory

Description

theory datastructure for development graphs

Synopsis

newtype ThId = ThId Int
startThId :: ThId
data G_theory = forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree.Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_theory {
- gTheoryLogic :: lid
- gTheorySyntax :: Maybe IRI
- gTheorySign :: ExtSign sign symbol
- gTheorySignIdx :: SigId
- gTheorySens :: ThSens sentence (AnyComorphism, BasicProof)
- gTheorySelfIdx :: ThId
}
createGThWith :: G_theory -> SigId -> ThId -> G_theory
coerceThSens :: (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, MonadFail m, Typeable b) => lid1 -> lid2 -> String -> ThSens sentence1 b -> m (ThSens sentence2 b)
prettyFullGTheory :: Maybe IRI -> G_theory -> Doc
prettyGTheorySL :: G_theory -> Doc
prettyGTheory :: Maybe IRI -> G_theory -> Doc
sublogicOfTh :: G_theory -> G_sublogics
getThGoals :: G_theory -> [(String, Maybe BasicProof)]
getThAxioms :: G_theory -> [(String, Bool)]
getThSens :: G_theory -> [String]
simplifyTh :: G_theory -> G_theory
mapG_theory :: Bool -> AnyComorphism -> G_theory -> Result G_theory
gEmbedGTC :: AnyComorphism -> G_theory -> Result GMorphism
translateG_theory :: GMorphism -> G_theory -> Result G_theory
joinG_sentences :: MonadFail m => G_theory -> G_theory -> m G_theory
intersectG_sentences :: MonadFail m => G_sign -> G_theory -> G_theory -> m G_theory
flatG_sentences :: MonadFail m => G_theory -> [G_theory] -> m G_theory
signOf :: G_theory -> G_sign
noSensGTheory :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> ExtSign sign symbol -> SigId -> G_theory
data BasicProof
- = forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree.Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => BasicProof lid (ProofStatus proof_tree)
- | Guessed
- | Conjectured
- | Handwritten
isProvenSenStatus :: SenStatus a (AnyComorphism, BasicProof) -> Bool
isProvedBasically :: BasicProof -> Bool
getValidAxioms :: G_theory -> G_theory -> [String]
invalidateProofs :: G_theory -> G_theory -> G_theory -> (Bool, G_theory)
proveSens :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> ThSens sentence (AnyComorphism, BasicProof) -> ThSens sentence (AnyComorphism, BasicProof)
proveLocalSens :: G_theory -> G_theory -> G_theory
proveSensAux :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> ThSens sentence (AnyComorphism, BasicProof) -> ThSens sentence (AnyComorphism, BasicProof) -> ThSens sentence (AnyComorphism, BasicProof)
propagateProofs :: G_theory -> G_theory -> G_theory
type GDiagram = Gr G_theory (Int, GMorphism)
isHomogeneousGDiagram :: GDiagram -> Bool
homogeniseGDiagram :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> GDiagram -> Result (Gr sign (Int, morphism))
homogeniseSink :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> [(Node, GMorphism)] -> Result [(Node, morphism)]
gEnsuresAmalgamability :: [CASLAmalgOpt] -> GDiagram -> [(Int, GMorphism)] -> Result Amalgamates

Documentation

newtype ThId Source #

Constructors

ThId Int

Instances

Instances details

Enum ThId Source #
Instance details Defined in Static.GTheory Methods succ :: ThId -> ThId pred :: ThId -> ThId toEnum :: Int -> ThId fromEnum :: ThId -> Int enumFrom :: ThId -> [ThId] enumFromThen :: ThId -> ThId -> [ThId] enumFromTo :: ThId -> ThId -> [ThId] enumFromThenTo :: ThId -> ThId -> ThId -> [ThId]
Eq ThId Source #
Instance details Defined in Static.GTheory Methods (==) :: ThId -> ThId -> Bool (/=) :: ThId -> ThId -> Bool
Ord ThId Source #
Instance details Defined in Static.GTheory Methods compare :: ThId -> ThId -> Ordering (<) :: ThId -> ThId -> Bool (<=) :: ThId -> ThId -> Bool (>) :: ThId -> ThId -> Bool (>=) :: ThId -> ThId -> Bool max :: ThId -> ThId -> ThId min :: ThId -> ThId -> ThId
Show ThId Source #
Instance details Defined in Static.GTheory Methods showsPrec :: Int -> ThId -> ShowS show :: ThId -> String showList :: [ThId] -> ShowS
ShATermConvertible ThId Source #
Instance details Defined in Static.GTheory Methods toShATermAux :: ATermTable -> ThId -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [ThId] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, ThId) fromShATermList' :: Int -> ATermTable -> (ATermTable, [ThId])

startThId :: ThId Source #

data G_theory Source #

Grothendieck theories with lookup indices

Constructors

forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree.Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_theory
Fields gTheoryLogic :: lid gTheorySyntax :: Maybe IRI gTheorySign :: ExtSign sign symbol gTheorySignIdx :: SigId index to lookup `G_sign` (using `signOf`) gTheorySens :: ThSens sentence (AnyComorphism, BasicProof) gTheorySelfIdx :: ThId index to lookup this `G_theory` in theory map

Instances

Instances details

Eq G_theory Source #
Instance details Defined in Static.GTheory Methods (==) :: G_theory -> G_theory -> Bool (/=) :: G_theory -> G_theory -> Bool
Show G_theory Source #
Instance details Defined in Static.GTheory Methods showsPrec :: Int -> G_theory -> ShowS show :: G_theory -> String showList :: [G_theory] -> ShowS
Pretty G_theory Source #
Instance details Defined in Static.GTheory Methods pretty :: G_theory -> Doc Source # pretties :: [G_theory] -> Doc Source #
ShATermLG G_theory Source #
Instance details Defined in ATC.Grothendieck Methods toShATermLG :: ATermTable -> G_theory -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, G_theory) Source #

createGThWith :: G_theory -> SigId -> ThId -> G_theory Source #

coerceThSens :: (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1, Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, MonadFail m, Typeable b) => lid1 -> lid2 -> String -> ThSens sentence1 b -> m (ThSens sentence2 b) Source #

prettyFullGTheory :: Maybe IRI -> G_theory -> Doc Source #

prettyGTheorySL :: G_theory -> Doc Source #

prettyGTheory :: Maybe IRI -> G_theory -> Doc Source #

sublogicOfTh :: G_theory -> G_sublogics Source #

compute sublogic of a theory

getThGoals :: G_theory -> [(String, Maybe BasicProof)] Source #

get theorem names with their best proof results

getThAxioms :: G_theory -> [(String, Bool)] Source #

get axiom names plus True for former theorem

getThSens :: G_theory -> [String] Source #

get sentence names

simplifyTh :: G_theory -> G_theory Source #

simplify a theory (throw away qualifications)

mapG_theory :: Bool -> AnyComorphism -> G_theory -> Result G_theory Source #

apply a comorphism to a theory

gEmbedGTC :: AnyComorphism -> G_theory -> Result GMorphism Source #

Embedding of GTCs as Grothendieck sig mors

translateG_theory :: GMorphism -> G_theory -> Result G_theory Source #

Translation of a G_theory along a GMorphism

joinG_sentences :: MonadFail m => G_theory -> G_theory -> m G_theory Source #

Join the sentences of two G_theories

intersectG_sentences :: MonadFail m => G_sign -> G_theory -> G_theory -> m G_theory Source #

Intersect the sentences of two G_theories, G_sign is the intersection of their signatures

flatG_sentences :: MonadFail m => G_theory -> [G_theory] -> m G_theory Source #

flattening the sentences form a list of G_theories

signOf :: G_theory -> G_sign Source #

Get signature of a theory

noSensGTheory :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> ExtSign sign symbol -> SigId -> G_theory Source #

create theory without sentences

data BasicProof Source #

Constructors

forall lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree.Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => BasicProof lid (ProofStatus proof_tree)
Guessed
Conjectured
Handwritten

Instances

Instances details

Eq BasicProof Source #
Instance details Defined in Static.GTheory Methods (==) :: BasicProof -> BasicProof -> Bool (/=) :: BasicProof -> BasicProof -> Bool
Ord BasicProof Source #
Instance details Defined in Static.GTheory Methods compare :: BasicProof -> BasicProof -> Ordering (<) :: BasicProof -> BasicProof -> Bool (<=) :: BasicProof -> BasicProof -> Bool (>) :: BasicProof -> BasicProof -> Bool (>=) :: BasicProof -> BasicProof -> Bool max :: BasicProof -> BasicProof -> BasicProof min :: BasicProof -> BasicProof -> BasicProof
Show BasicProof Source #
Instance details Defined in Static.GTheory Methods showsPrec :: Int -> BasicProof -> ShowS show :: BasicProof -> String showList :: [BasicProof] -> ShowS
ShATermLG BasicProof Source #
Instance details Defined in ATC.Grothendieck Methods toShATermLG :: ATermTable -> BasicProof -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, BasicProof) Source #

isProvenSenStatus :: SenStatus a (AnyComorphism, BasicProof) -> Bool Source #

test a theory sentence

isProvedBasically :: BasicProof -> Bool Source #

getValidAxioms Source #

Arguments

:: G_theory	old global theory
-> G_theory	new global theory
-> [String]	unchanged axioms

invalidateProofs Source #

Arguments

:: G_theory	old global theory
-> G_theory	new global theory
-> G_theory	local theory with proven goals
-> (Bool, G_theory)	no changes and new local theory with deleted proofs

proveSens :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> ThSens sentence (AnyComorphism, BasicProof) -> ThSens sentence (AnyComorphism, BasicProof) Source #

mark sentences as proven if an identical axiom or other proven sentence is part of the same theory.

proveLocalSens :: G_theory -> G_theory -> G_theory Source #

proveSensAux :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> ThSens sentence (AnyComorphism, BasicProof) -> ThSens sentence (AnyComorphism, BasicProof) -> ThSens sentence (AnyComorphism, BasicProof) Source #

mark sentences as proven if an identical axiom or other proven sentence is part of a given global theory.

propagateProofs :: G_theory -> G_theory -> G_theory Source #

mark all sentences of a local theory that have been proven via a prover over a global theory (with the same signature) as proven. Also mark duplicates of proven sentences as proven. Assume that the sentence names of the local theory are identical to the global theory.

type GDiagram = Gr G_theory (Int, GMorphism) Source #

Grothendieck diagrams

isHomogeneousGDiagram :: GDiagram -> Bool Source #

checks whether a connected GDiagram is homogeneous

homogeniseGDiagram Source #

Arguments

:: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree
=> lid	the target logic to be coerced to
-> GDiagram	the GDiagram to be homogenised
-> Result (Gr sign (Int, morphism))

homogenise a GDiagram to a targeted logic

homogeniseSink Source #

Arguments

:: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree
=> lid	the target logic to which morphisms will be coerced
-> [(Node, GMorphism)]	the list of edges to be homogenised
-> Result [(Node, morphism)]

Coerce GMorphisms in the list of (diagram node, GMorphism) pairs to morphisms in given logic

gEnsuresAmalgamability :: [CASLAmalgOpt] -> GDiagram -> [(Int, GMorphism)] -> Result Amalgamates Source #