Hets - the Heterogeneous Tool Set

Copyright(c) Christian Maeder and Uni Bremen 2003-2005
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityexperimental
Portabilityportable
Safe HaskellSafe-Inferred

HasCASL.As

Contents

Description

abstract syntax for HasCASL, more liberal than Concrete-Syntax.txt, annotations are almost as for CASL

Synopsis

abstract syntax entities with small utility functions

data BasicSpec

annotated basic items

Constructors

BasicSpec [Annoted BasicItem] 

Instances

Data BasicSpec 
Show BasicSpec 
ShATermConvertible BasicSpec 
Monoid BasicSpec 
GetRange BasicSpec 
Pretty BasicSpec 
Typeable * BasicSpec 
ProjectSublogic Sublogic BasicSpec 
MinSublogic Sublogic BasicSpec 
Syntax HasCASL BasicSpec Symbol SymbItems SymbMapItems 
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol 
Logic HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree 
Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () 
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () 
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () 
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () 
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 
Comorphism HasCASL2Haskell HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Haskell () HsDecls (TiDecl PNT) () () Sign HaskellMorphism Symbol RawSymbol () 

data OpBrand

indicator for predicate, operation or function

Constructors

Pred 
Op 
Fun 

isPred :: OpBrand -> Bool

test if the function was declared as predicate

data ClassDecl

declaring class identifiers

Constructors

ClassDecl [Id] Kind Range 

data Variance

co- or contra- variance indicator

Constructors

InVar 
CoVar 
ContraVar 
NonVar 

data AnyKind a

(higher) kinds

Constructors

ClassKind a 
FunKind Variance (AnyKind a) (AnyKind a) Range 

Instances

Ord a => Eq (AnyKind a) 
Data a => Data (AnyKind a) 
Ord a => Ord (AnyKind a) 
Show a => Show (AnyKind a) 
ShATermConvertible a => ShATermConvertible (AnyKind a) 
Pretty a => Pretty (AnyKind a) 
Typeable (* -> *) AnyKind 

type Kind = AnyKind Id

type RawKind = AnyKind ()

data Vars

a tuple pattern for SubtypeDefn

Constructors

Var Id 
VarTuple [Vars] Range 

mapTypeOfScheme :: (Type -> Type) -> TypeScheme -> TypeScheme

change the type within a scheme

data TypeScheme

a type with bound type variables. The bound variables within the scheme should have negative numbers in the order given by the type argument list. The type arguments store proper kinds (including downsets) whereas the kind within the type names are only raw kinds.

Constructors

TypeScheme [TypeArg] Type Range 

data Partiality

indicator for partial or total functions

Constructors

Partial 
Total 

data OpItem

function declarations or definitions

data BinOpAttr

attributes without arguments for binary functions

Constructors

Assoc 
Comm 
Idem 

data OpAttr

possible function attributes (including a term as a unit element)

data DatatypeDecl

a polymorphic data type declaration with a deriving clause

data Alternative

Alternatives are subtypes or a constructor with a list of (curried) tuples as arguments. Only the components of the first tuple can be addressed by the places of the mixfix constructor.

data Component

A component is a type with on optional (only pre- or postfix) selector function.

data TypeQual

the possibly type annotations of terms

Constructors

OfType 
AsType 
InType 
Inferred 

data LetBrand

an indicator of (otherwise equivalent) let or where equations

Constructors

Let 
Where 
Program 

data BracketKind

the possible kinds of brackets (that should match when parsed)

Constructors

Parens 
Squares 
Braces 
NoBrackets 

getBrackets :: BracketKind -> (String, String)

the brackets as strings for printing

data Term

The possible terms and patterns. Formulas are also kept as terms. Local variables and constants are kept separatetly. The variant ResolvedMixTerm is an intermediate representation for type checking only.

data ProgEq

an equation or a case as pair of a pattern and a term

Constructors

ProgEq Term Term Range 

data PolyId

an identifier with an optional list of type declarations

Constructors

PolyId Id [TypeArg] Range 

data SeparatorKind

an indicator if variables were separated by commas or by separate declarations

Constructors

Comma 
Other 

data VarKind

the kind of a type variable (or a type argument in schemes)

data TypeArg

a (simple) type variable with its kind (or supertype)

symbol data types symbols

data SymbItems

Instances

Eq SymbItems 
Data SymbItems 
Ord SymbItems 
Show SymbItems 
ShATermConvertible SymbItems 
Pretty SymbItems 
Typeable * SymbItems 
ProjectSublogicM Sublogic SymbItems 
MinSublogic Sublogic SymbItems 
Syntax HasCASL BasicSpec Symbol SymbItems SymbMapItems 
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol 
Logic HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree 
Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () 
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () 
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () 
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () 
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 
Comorphism HasCASL2Haskell HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Haskell () HsDecls (TiDecl PNT) () () Sign HaskellMorphism Symbol RawSymbol () 

data SymbMapItems

mapped symbols

Instances

Eq SymbMapItems 
Data SymbMapItems 
Ord SymbMapItems 
Show SymbMapItems 
ShATermConvertible SymbMapItems 
Pretty SymbMapItems 
Typeable * SymbMapItems 
ProjectSublogicM Sublogic SymbMapItems 
MinSublogic Sublogic SymbMapItems 
Syntax HasCASL BasicSpec Symbol SymbItems SymbMapItems 
StaticAnalysis HasCASL BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol 
Logic HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 
Comorphism THFP_P2HasCASL THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 
Comorphism HasCASL2THFP_P HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree 
Comorphism HasCASL2HasCASL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () 
Comorphism PCoClTyConsHOL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () 
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () 
Comorphism PCoClTyConsHOL2PairsInIsaHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () 
Comorphism HasCASL2PCoClTyConsHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 
Comorphism CASL2HasCASL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 
Comorphism ExtModal2HasCASL ExtModal ExtModalSL EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS ExtModalSign ExtModalMorph Symbol RawSymbol () HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () 
Comorphism HasCASL2Haskell HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Haskell () HsDecls (TiDecl PNT) () () Sign HaskellMorphism Symbol RawSymbol () 

data Symb

type annotated symbols

Constructors

Symb Id (Maybe SymbType) Range 

equality instances ignoring positions

compute better position

bestRange :: GetRange a => [a] -> Range -> Range

get a reasonable position for a list with an additional position list