Hets - the Heterogeneous Tool Set

Copyright(c) Robert Savu and Uni Bremen 2011
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerRobert.Savu@dfki.de
Stabilityexperimental
Portabilityportable
Safe HaskellSafe

FreeCAD.As

Description

Declaration of the abstract datatypes of FreeCAD terms

Synopsis

Documentation

data Vector3 Source #

Constructors

Vector3 

Fields

  • x :: Double
     
  • y :: Double
     
  • z :: Double
     

Instances

Eq Vector3 Source # 

Methods

(==) :: Vector3 -> Vector3 -> Bool

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

Data Vector3 Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Vector3 -> c Vector3

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Vector3

toConstr :: Vector3 -> Constr

dataTypeOf :: Vector3 -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Vector3)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Vector3)

gmapT :: (forall b. Data b => b -> b) -> Vector3 -> Vector3

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Vector3 -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Vector3 -> r

gmapQ :: (forall d. Data d => d -> u) -> Vector3 -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Vector3 -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Vector3 -> m Vector3

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Vector3 -> m Vector3

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Vector3 -> m Vector3

Ord Vector3 Source # 

Methods

compare :: Vector3 -> Vector3 -> Ordering

(<) :: Vector3 -> Vector3 -> Bool

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

(>) :: Vector3 -> Vector3 -> Bool

(>=) :: Vector3 -> Vector3 -> Bool

max :: Vector3 -> Vector3 -> Vector3

min :: Vector3 -> Vector3 -> Vector3

Show Vector3 Source # 

Methods

showsPrec :: Int -> Vector3 -> ShowS

show :: Vector3 -> String

showList :: [Vector3] -> ShowS

data Matrix33 Source #

Constructors

Matrix33 

Fields

  • a11 :: Double
     
  • a12 :: Double
     
  • a13 :: Double
     
  • a21 :: Double
     
  • a22 :: Double
     
  • a23 :: Double
     
  • a31 :: Double
     
  • a32 :: Double
     
  • a33 :: Double
     

Instances

Eq Matrix33 Source # 

Methods

(==) :: Matrix33 -> Matrix33 -> Bool

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

Data Matrix33 Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Matrix33 -> c Matrix33

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Matrix33

toConstr :: Matrix33 -> Constr

dataTypeOf :: Matrix33 -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Matrix33)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Matrix33)

gmapT :: (forall b. Data b => b -> b) -> Matrix33 -> Matrix33

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Matrix33 -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Matrix33 -> r

gmapQ :: (forall d. Data d => d -> u) -> Matrix33 -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Matrix33 -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Matrix33 -> m Matrix33

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Matrix33 -> m Matrix33

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Matrix33 -> m Matrix33

Ord Matrix33 Source # 

Methods

compare :: Matrix33 -> Matrix33 -> Ordering

(<) :: Matrix33 -> Matrix33 -> Bool

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

(>) :: Matrix33 -> Matrix33 -> Bool

(>=) :: Matrix33 -> Matrix33 -> Bool

max :: Matrix33 -> Matrix33 -> Matrix33

min :: Matrix33 -> Matrix33 -> Matrix33

Show Matrix33 Source # 

Methods

showsPrec :: Int -> Matrix33 -> ShowS

show :: Matrix33 -> String

showList :: [Matrix33] -> ShowS

data Vector4 Source #

Constructors

Vector4 

Fields

  • q0 :: Double
     
  • q1 :: Double
     
  • q2 :: Double
     
  • q3 :: Double
     

Instances

Eq Vector4 Source # 

Methods

(==) :: Vector4 -> Vector4 -> Bool

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

Data Vector4 Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Vector4 -> c Vector4

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Vector4

toConstr :: Vector4 -> Constr

dataTypeOf :: Vector4 -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Vector4)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Vector4)

gmapT :: (forall b. Data b => b -> b) -> Vector4 -> Vector4

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Vector4 -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Vector4 -> r

gmapQ :: (forall d. Data d => d -> u) -> Vector4 -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Vector4 -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Vector4 -> m Vector4

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Vector4 -> m Vector4

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Vector4 -> m Vector4

Ord Vector4 Source # 

Methods

compare :: Vector4 -> Vector4 -> Ordering

(<) :: Vector4 -> Vector4 -> Bool

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

(>) :: Vector4 -> Vector4 -> Bool

(>=) :: Vector4 -> Vector4 -> Bool

max :: Vector4 -> Vector4 -> Vector4

min :: Vector4 -> Vector4 -> Vector4

Show Vector4 Source # 

Methods

showsPrec :: Int -> Vector4 -> ShowS

show :: Vector4 -> String

showList :: [Vector4] -> ShowS

data Placement Source #

Constructors

Placement 

Fields

Instances

Eq Placement Source # 

Methods

(==) :: Placement -> Placement -> Bool

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

Data Placement Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Placement -> c Placement

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Placement

toConstr :: Placement -> Constr

dataTypeOf :: Placement -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Placement)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Placement)

gmapT :: (forall b. Data b => b -> b) -> Placement -> Placement

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Placement -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Placement -> r

gmapQ :: (forall d. Data d => d -> u) -> Placement -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Placement -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Placement -> m Placement

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Placement -> m Placement

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Placement -> m Placement

Ord Placement Source # 

Methods

compare :: Placement -> Placement -> Ordering

(<) :: Placement -> Placement -> Bool

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

(>) :: Placement -> Placement -> Bool

(>=) :: Placement -> Placement -> Bool

max :: Placement -> Placement -> Placement

min :: Placement -> Placement -> Placement

Show Placement Source # 

Methods

showsPrec :: Int -> Placement -> ShowS

show :: Placement -> String

showList :: [Placement] -> ShowS

data BaseObject Source #

Constructors

Box Double Double Double 
Cylinder Double Double Double 
Sphere Double Double Double Double 
Cone Double Double Double Double 
Torus Double Double Double Double Double 
Line Double 
Circle Double Double Double 
Rectangle Double Double 

Instances

Eq BaseObject Source # 

Methods

(==) :: BaseObject -> BaseObject -> Bool

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

Data BaseObject Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BaseObject -> c BaseObject

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BaseObject

toConstr :: BaseObject -> Constr

dataTypeOf :: BaseObject -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c BaseObject)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BaseObject)

gmapT :: (forall b. Data b => b -> b) -> BaseObject -> BaseObject

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BaseObject -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BaseObject -> r

gmapQ :: (forall d. Data d => d -> u) -> BaseObject -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> BaseObject -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> BaseObject -> m BaseObject

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BaseObject -> m BaseObject

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BaseObject -> m BaseObject

Ord BaseObject Source # 
Show BaseObject Source # 

Methods

showsPrec :: Int -> BaseObject -> ShowS

show :: BaseObject -> String

showList :: [BaseObject] -> ShowS

data Object Source #

Constructors

BaseObject BaseObject 
Cut ExtendedObject ExtendedObject 
Common ExtendedObject ExtendedObject 
Fusion ExtendedObject ExtendedObject 
Extrusion ExtendedObject Vector3 
Section ExtendedObject ExtendedObject 

Instances

Eq Object Source # 

Methods

(==) :: Object -> Object -> Bool

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

Data Object Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Object -> c Object

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Object

toConstr :: Object -> Constr

dataTypeOf :: Object -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Object)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Object)

gmapT :: (forall b. Data b => b -> b) -> Object -> Object

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Object -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Object -> r

gmapQ :: (forall d. Data d => d -> u) -> Object -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Object -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Object -> m Object

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Object -> m Object

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Object -> m Object

Ord Object Source # 

Methods

compare :: Object -> Object -> Ordering

(<) :: Object -> Object -> Bool

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

(>) :: Object -> Object -> Bool

(>=) :: Object -> Object -> Bool

max :: Object -> Object -> Object

min :: Object -> Object -> Object

Show Object Source # 

Methods

showsPrec :: Int -> Object -> ShowS

show :: Object -> String

showList :: [Object] -> ShowS

data ExtendedObject Source #

Constructors

Placed PlacedObject 
Ref String 

Instances

Eq ExtendedObject Source # 
Data ExtendedObject Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ExtendedObject -> c ExtendedObject

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ExtendedObject

toConstr :: ExtendedObject -> Constr

dataTypeOf :: ExtendedObject -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c ExtendedObject)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExtendedObject)

gmapT :: (forall b. Data b => b -> b) -> ExtendedObject -> ExtendedObject

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExtendedObject -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExtendedObject -> r

gmapQ :: (forall d. Data d => d -> u) -> ExtendedObject -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> ExtendedObject -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExtendedObject -> m ExtendedObject

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExtendedObject -> m ExtendedObject

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExtendedObject -> m ExtendedObject

Ord ExtendedObject Source # 
Show ExtendedObject Source # 

Methods

showsPrec :: Int -> ExtendedObject -> ShowS

show :: ExtendedObject -> String

showList :: [ExtendedObject] -> ShowS

data PlacedObject Source #

Constructors

PlacedObject 

Fields

Instances

Eq PlacedObject Source # 

Methods

(==) :: PlacedObject -> PlacedObject -> Bool

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

Data PlacedObject Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> PlacedObject -> c PlacedObject

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c PlacedObject

toConstr :: PlacedObject -> Constr

dataTypeOf :: PlacedObject -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c PlacedObject)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c PlacedObject)

gmapT :: (forall b. Data b => b -> b) -> PlacedObject -> PlacedObject

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> PlacedObject -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> PlacedObject -> r

gmapQ :: (forall d. Data d => d -> u) -> PlacedObject -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> PlacedObject -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> PlacedObject -> m PlacedObject

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> PlacedObject -> m PlacedObject

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> PlacedObject -> m PlacedObject

Ord PlacedObject Source # 
Show PlacedObject Source # 

Methods

showsPrec :: Int -> PlacedObject -> ShowS

show :: PlacedObject -> String

showList :: [PlacedObject] -> ShowS

data NamedObject Source #

Constructors

NamedObject 

Fields

EmptyObject 

Instances

Eq NamedObject Source # 

Methods

(==) :: NamedObject -> NamedObject -> Bool

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

Data NamedObject Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NamedObject -> c NamedObject

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c NamedObject

toConstr :: NamedObject -> Constr

dataTypeOf :: NamedObject -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c NamedObject)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c NamedObject)

gmapT :: (forall b. Data b => b -> b) -> NamedObject -> NamedObject

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NamedObject -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NamedObject -> r

gmapQ :: (forall d. Data d => d -> u) -> NamedObject -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> NamedObject -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> NamedObject -> m NamedObject

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NamedObject -> m NamedObject

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NamedObject -> m NamedObject

Ord NamedObject Source # 
Show NamedObject Source # 

Methods

showsPrec :: Int -> NamedObject -> ShowS

show :: NamedObject -> String

showList :: [NamedObject] -> ShowS

Syntax FreeCAD Document () () () Source # 
StaticAnalysis FreeCAD Document () () () Sign FCMorphism () () Source # 

Methods

basic_analysis :: FreeCAD -> Maybe ((Document, Sign, GlobalAnnos) -> Result (Document, ExtSign Sign (), [Named ()])) Source #

sen_analysis :: FreeCAD -> Maybe ((Document, Sign, ()) -> Result ()) Source #

extBasicAnalysis :: FreeCAD -> IRI -> LibName -> Document -> Sign -> GlobalAnnos -> Result (Document, ExtSign Sign (), [Named ()]) Source #

stat_symb_map_items :: FreeCAD -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: FreeCAD -> Sign -> [()] -> Result [()] Source #

convertTheory :: FreeCAD -> Maybe ((Sign, [Named ()]) -> Document) Source #

ensures_amalgamability :: FreeCAD -> ([CASLAmalgOpt], Gr Sign (Int, FCMorphism), [(Int, FCMorphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: FreeCAD -> FCMorphism -> [Named ()] -> Result (Sign, [Named ()]) Source #

signature_colimit :: FreeCAD -> Gr Sign (Int, FCMorphism) -> Result (Sign, Map Int FCMorphism) Source #

qualify :: FreeCAD -> SIMPLE_ID -> LibName -> FCMorphism -> Sign -> Result (FCMorphism, [Named ()]) Source #

symbol_to_raw :: FreeCAD -> () -> () Source #

id_to_raw :: FreeCAD -> Id -> () Source #

matches :: FreeCAD -> () -> () -> Bool Source #

empty_signature :: FreeCAD -> Sign Source #

add_symb_to_sign :: FreeCAD -> Sign -> () -> Result Sign Source #

signature_union :: FreeCAD -> Sign -> Sign -> Result Sign Source #

signatureDiff :: FreeCAD -> Sign -> Sign -> Result Sign Source #

intersection :: FreeCAD -> Sign -> Sign -> Result Sign Source #

final_union :: FreeCAD -> Sign -> Sign -> Result Sign Source #

morphism_union :: FreeCAD -> FCMorphism -> FCMorphism -> Result FCMorphism Source #

is_subsig :: FreeCAD -> Sign -> Sign -> Bool Source #

subsig_inclusion :: FreeCAD -> Sign -> Sign -> Result FCMorphism Source #

generated_sign :: FreeCAD -> Set () -> Sign -> Result FCMorphism Source #

cogenerated_sign :: FreeCAD -> Set () -> Sign -> Result FCMorphism Source #

induced_from_morphism :: FreeCAD -> EndoMap () -> Sign -> Result FCMorphism Source #

induced_from_to_morphism :: FreeCAD -> EndoMap () -> ExtSign Sign () -> ExtSign Sign () -> Result FCMorphism Source #

is_transportable :: FreeCAD -> FCMorphism -> Bool Source #

is_injective :: FreeCAD -> FCMorphism -> Bool Source #

theory_to_taxonomy :: FreeCAD -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named ()] -> Result MMiSSOntology Source #

corresp2th :: FreeCAD -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (Sign, [Named ()], Sign, Sign, EndoMap (), EndoMap ()) Source #

equiv2cospan :: FreeCAD -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap (), EndoMap ()) Source #

extract_module :: FreeCAD -> [IRI] -> (Sign, [Named ()]) -> Result (Sign, [Named ()]) Source #

Logic FreeCAD () Document () () () Sign (DefaultMorphism Sign) () () () Source # 

Methods

parse_basic_sen :: FreeCAD -> Maybe (Document -> AParser st ()) Source #

stability :: FreeCAD -> Stability Source #

data_logic :: FreeCAD -> Maybe AnyLogic Source #

top_sublogic :: FreeCAD -> () Source #

all_sublogics :: FreeCAD -> [()] Source #

bottomSublogic :: FreeCAD -> Maybe () Source #

sublogicDimensions :: FreeCAD -> [[()]] Source #

parseSublogic :: FreeCAD -> String -> Maybe () Source #

proj_sublogic_epsilon :: FreeCAD -> () -> Sign -> DefaultMorphism Sign Source #

provers :: FreeCAD -> [Prover Sign () (DefaultMorphism Sign) () ()] Source #

default_prover :: FreeCAD -> String Source #

cons_checkers :: FreeCAD -> [ConsChecker Sign () () (DefaultMorphism Sign) ()] Source #

conservativityCheck :: FreeCAD -> [ConservativityChecker Sign () (DefaultMorphism Sign)] Source #

empty_proof_tree :: FreeCAD -> () Source #

syntaxTable :: FreeCAD -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: FreeCAD -> Maybe OMCD Source #

export_symToOmdoc :: FreeCAD -> NameMap () -> () -> String -> Result TCElement Source #

export_senToOmdoc :: FreeCAD -> NameMap () -> () -> Result TCorOMElement Source #

export_theoryToOmdoc :: FreeCAD -> SigMap () -> Sign -> [Named ()] -> Result [TCElement] Source #

omdocToSym :: FreeCAD -> SigMapI () -> TCElement -> String -> Result () Source #

omdocToSen :: FreeCAD -> SigMapI () -> TCElement -> String -> Result (Maybe (Named ())) Source #

addOMadtToTheory :: FreeCAD -> SigMapI () -> (Sign, [Named ()]) -> [[OmdADT]] -> Result (Sign, [Named ()]) Source #

addOmdocToTheory :: FreeCAD -> SigMapI () -> (Sign, [Named ()]) -> [TCElement] -> Result (Sign, [Named ()]) Source #

sublogicOfTheo :: FreeCAD -> (Sign, [()]) -> () Source #

type Document = [NamedObject] Source #

data Sign Source #

Datatype for FreeCAD Signatures Signatures are just sets of named objects

Constructors

Sign 

Fields

Instances

Eq Sign Source # 

Methods

(==) :: Sign -> Sign -> Bool

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

Data Sign Source # 

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Sign -> c Sign

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Sign

toConstr :: Sign -> Constr

dataTypeOf :: Sign -> DataType

dataCast1 :: Typeable (* -> *) t => (forall d. Data d => c (t d)) -> Maybe (c Sign)

dataCast2 :: Typeable (* -> * -> *) t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Sign)

gmapT :: (forall b. Data b => b -> b) -> Sign -> Sign

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Sign -> r

gmapQ :: (forall d. Data d => d -> u) -> Sign -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Sign -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Sign -> m Sign

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Sign -> m Sign

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Sign -> m Sign

Ord Sign Source # 

Methods

compare :: Sign -> Sign -> Ordering

(<) :: Sign -> Sign -> Bool

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

(>) :: Sign -> Sign -> Bool

(>=) :: Sign -> Sign -> Bool

max :: Sign -> Sign -> Sign

min :: Sign -> Sign -> Sign

Show Sign Source # 

Methods

showsPrec :: Int -> Sign -> ShowS

show :: Sign -> String

showList :: [Sign] -> ShowS

Sentences FreeCAD () Sign FCMorphism () Source # 

Methods

map_sen :: FreeCAD -> FCMorphism -> () -> Result () Source #

simplify_sen :: FreeCAD -> Sign -> () -> () Source #

negation :: FreeCAD -> () -> Maybe () Source #

print_sign :: FreeCAD -> Sign -> Doc Source #

print_named :: FreeCAD -> Named () -> Doc Source #

sym_of :: FreeCAD -> Sign -> [Set ()] Source #

mostSymsOf :: FreeCAD -> Sign -> [()] Source #

symmap_of :: FreeCAD -> FCMorphism -> EndoMap () Source #

sym_name :: FreeCAD -> () -> Id Source #

sym_label :: FreeCAD -> () -> Maybe String Source #

fullSymName :: FreeCAD -> () -> String Source #

symKind :: FreeCAD -> () -> String Source #

symsOfSen :: FreeCAD -> Sign -> () -> [()] Source #

pair_symbols :: FreeCAD -> () -> () -> Result () Source #

StaticAnalysis FreeCAD Document () () () Sign FCMorphism () () Source # 

Methods

basic_analysis :: FreeCAD -> Maybe ((Document, Sign, GlobalAnnos) -> Result (Document, ExtSign Sign (), [Named ()])) Source #

sen_analysis :: FreeCAD -> Maybe ((Document, Sign, ()) -> Result ()) Source #

extBasicAnalysis :: FreeCAD -> IRI -> LibName -> Document -> Sign -> GlobalAnnos -> Result (Document, ExtSign Sign (), [Named ()]) Source #

stat_symb_map_items :: FreeCAD -> Sign -> Maybe Sign -> [()] -> Result (EndoMap ()) Source #

stat_symb_items :: FreeCAD -> Sign -> [()] -> Result [()] Source #

convertTheory :: FreeCAD -> Maybe ((Sign, [Named ()]) -> Document) Source #

ensures_amalgamability :: FreeCAD -> ([CASLAmalgOpt], Gr Sign (Int, FCMorphism), [(Int, FCMorphism)], Gr String String) -> Result Amalgamates Source #

quotient_term_algebra :: FreeCAD -> FCMorphism -> [Named ()] -> Result (Sign, [Named ()]) Source #

signature_colimit :: FreeCAD -> Gr Sign (Int, FCMorphism) -> Result (Sign, Map Int FCMorphism) Source #

qualify :: FreeCAD -> SIMPLE_ID -> LibName -> FCMorphism -> Sign -> Result (FCMorphism, [Named ()]) Source #

symbol_to_raw :: FreeCAD -> () -> () Source #

id_to_raw :: FreeCAD -> Id -> () Source #

matches :: FreeCAD -> () -> () -> Bool Source #

empty_signature :: FreeCAD -> Sign Source #

add_symb_to_sign :: FreeCAD -> Sign -> () -> Result Sign Source #

signature_union :: FreeCAD -> Sign -> Sign -> Result Sign Source #

signatureDiff :: FreeCAD -> Sign -> Sign -> Result Sign Source #

intersection :: FreeCAD -> Sign -> Sign -> Result Sign Source #

final_union :: FreeCAD -> Sign -> Sign -> Result Sign Source #

morphism_union :: FreeCAD -> FCMorphism -> FCMorphism -> Result FCMorphism Source #

is_subsig :: FreeCAD -> Sign -> Sign -> Bool Source #

subsig_inclusion :: FreeCAD -> Sign -> Sign -> Result FCMorphism Source #

generated_sign :: FreeCAD -> Set () -> Sign -> Result FCMorphism Source #

cogenerated_sign :: FreeCAD -> Set () -> Sign -> Result FCMorphism Source #

induced_from_morphism :: FreeCAD -> EndoMap () -> Sign -> Result FCMorphism Source #

induced_from_to_morphism :: FreeCAD -> EndoMap () -> ExtSign Sign () -> ExtSign Sign () -> Result FCMorphism Source #

is_transportable :: FreeCAD -> FCMorphism -> Bool Source #

is_injective :: FreeCAD -> FCMorphism -> Bool Source #

theory_to_taxonomy :: FreeCAD -> TaxoGraphKind -> MMiSSOntology -> Sign -> [Named ()] -> Result MMiSSOntology Source #

corresp2th :: FreeCAD -> String -> Bool -> Sign -> Sign -> [()] -> [()] -> EndoMap () -> EndoMap () -> REL_REF -> Result (Sign, [Named ()], Sign, Sign, EndoMap (), EndoMap ()) Source #

equiv2cospan :: FreeCAD -> Sign -> Sign -> [()] -> [()] -> Result (Sign, Sign, Sign, EndoMap (), EndoMap ()) Source #

extract_module :: FreeCAD -> [IRI] -> (Sign, [Named ()]) -> Result (Sign, [Named ()]) Source #

Logic FreeCAD () Document () () () Sign (DefaultMorphism Sign) () () () Source # 

Methods

parse_basic_sen :: FreeCAD -> Maybe (Document -> AParser st ()) Source #

stability :: FreeCAD -> Stability Source #

data_logic :: FreeCAD -> Maybe AnyLogic Source #

top_sublogic :: FreeCAD -> () Source #

all_sublogics :: FreeCAD -> [()] Source #

bottomSublogic :: FreeCAD -> Maybe () Source #

sublogicDimensions :: FreeCAD -> [[()]] Source #

parseSublogic :: FreeCAD -> String -> Maybe () Source #

proj_sublogic_epsilon :: FreeCAD -> () -> Sign -> DefaultMorphism Sign Source #

provers :: FreeCAD -> [Prover Sign () (DefaultMorphism Sign) () ()] Source #

default_prover :: FreeCAD -> String Source #

cons_checkers :: FreeCAD -> [ConsChecker Sign () () (DefaultMorphism Sign) ()] Source #

conservativityCheck :: FreeCAD -> [ConservativityChecker Sign () (DefaultMorphism Sign)] Source #

empty_proof_tree :: FreeCAD -> () Source #

syntaxTable :: FreeCAD -> Sign -> Maybe SyntaxTable Source #

omdoc_metatheory :: FreeCAD -> Maybe OMCD Source #

export_symToOmdoc :: FreeCAD -> NameMap () -> () -> String -> Result TCElement Source #

export_senToOmdoc :: FreeCAD -> NameMap () -> () -> Result TCorOMElement Source #

export_theoryToOmdoc :: FreeCAD -> SigMap () -> Sign -> [Named ()] -> Result [TCElement] Source #

omdocToSym :: FreeCAD -> SigMapI () -> TCElement -> String -> Result () Source #

omdocToSen :: FreeCAD -> SigMapI () -> TCElement -> String -> Result (Maybe (Named ())) Source #

addOMadtToTheory :: FreeCAD -> SigMapI () -> (Sign, [Named ()]) -> [[OmdADT]] -> Result (Sign, [Named ()]) Source #

addOmdocToTheory :: FreeCAD -> SigMapI () -> (Sign, [Named ()]) -> [TCElement] -> Result (Sign, [Named ()]) Source #

sublogicOfTheo :: FreeCAD -> (Sign, [()]) -> () Source #