Static.GTheory

Description

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, Monad 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 :: AnyComorphism -> G_theory -> Result G_theory
• translateG_theory :: GMorphism -> G_theory -> Result G_theory
• joinG_sentences :: Monad m => G_theory -> G_theory -> m G_theory
• flatG_sentences :: Monad 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