Hets - the Heterogeneous Tool Set

Copyright(c) Till Mossakowski Uni Bremen 2002-2006
LicenseGPLv2 or higher, see LICENSE.txt
Maintainertill@informatik.uni-bremen.de
Stabilityprovisional
Portabilitynon-portable(Logic)
Safe HaskellNone

Static.GTheory

Description

theory datastructure for development graphs

Synopsis

Documentation

newtype ThId Source #

Constructors

ThId Int 

Instances

Enum ThId Source # 

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 # 

Methods

(==) :: ThId -> ThId -> Bool

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

Ord ThId Source # 

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 # 

Methods

showsPrec :: Int -> ThId -> ShowS

show :: ThId -> String

showList :: [ThId] -> ShowS

ShATermConvertible ThId Source # 

Methods

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

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

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

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

data G_theory Source #

Grothendieck theories with lookup indices

Constructors

Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_theory 

Fields

Instances

Eq G_theory Source # 

Methods

(==) :: G_theory -> G_theory -> Bool

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

Show G_theory Source # 

Methods

showsPrec :: Int -> G_theory -> ShowS

show :: G_theory -> String

showList :: [G_theory] -> ShowS

Pretty G_theory Source # 
ShATermLG G_theory Source # 

Methods

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

fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, 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, Monad m, Typeable b) => lid1 -> lid2 -> String -> ThSens sentence1 b -> m (ThSens sentence2 b) 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

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

Translation of a G_theory along a GMorphism

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

Join the sentences of two G_theories

intersectG_sentences :: Monad 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 :: Monad 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

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

Eq BasicProof Source # 

Methods

(==) :: BasicProof -> BasicProof -> Bool

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

Ord BasicProof Source # 
Show BasicProof Source # 

Methods

showsPrec :: Int -> BasicProof -> ShowS

show :: BasicProof -> String

showList :: [BasicProof] -> ShowS

ShATermLG BasicProof Source # 

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

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.

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