Copyright	(c) Sonja Groening C. Maeder Uni Bremen 2003-2006
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	non-portable (imports Logic.Logic)
Safe Haskell	None

Comorphisms.HasCASL2IsabelleHOL

Contents

Signature
translation of a type in an operation declaration
translation of a datatype declaration
Formulas
translation of lambda abstractions
translation of case alternatives

Description

This embedding comorphism from HasCASL to Isabelle-HOL is an old version that can be deleted as soon as case terms are implemented elsewhere

Synopsis

data HasCASL2IsabelleHOL = HasCASL2IsabelleHOL
baseSign :: BaseSig
transSignature :: Env -> Result (Sign, [Named Sentence])
transOpInfo :: OpInfo -> Maybe Typ
transOpType :: TypeScheme -> Typ
transType :: Type -> Typ
transDatatype :: TypeMap -> DomainTab
transDataEntry :: DataEntry -> [DomainEntry]
transTypeArg :: TypeArg -> Typ
transAltDefn :: AltDefn -> (VName, [Typ])
transVar :: Id -> VName
transSentence :: Env -> Sentence -> Maybe Term
transOpId :: Env -> Id -> TypeScheme -> String
transProgEq :: Env -> ProgEq -> (Term, Term)
transTerm :: Env -> Term -> Term
transAppl :: Env -> Maybe Type -> Term -> Term -> Term
mkApp :: String -> Env -> Term -> Term -> Term
transApplOp :: Env -> Type -> Term -> Term -> Term
transLog :: Env -> Id -> Term -> Term -> Term
transWhenElse :: Env -> Term -> Term
abstraction :: Env -> Term -> Term -> Term
transPattern :: Env -> Term -> Term
transTotalLambda :: Env -> Term -> Term
arangeCaseAlts :: Env -> [ProgEq] -> [(Term, Term)]
sortCaseAlts :: Env -> [ProgEq] -> [(Term, Term)]
getCons :: Env -> Id -> [Id]
getName :: ProgEq -> Id
getTypeName :: Term -> Id
groupCons :: [ProgEq] -> Id -> [ProgEq]
flattenPattern :: Env -> [ProgEq] -> (Term, Term)
data CaseMatrix = CaseMatrix {
- patBrand :: PatBrand
- cons :: Maybe Term
- args :: [Term]
- newArgs :: [Term]
- term :: Term
}
data PatBrand
- = Appl
- | Tuple
- | QuOp
- | QuVar
matricize :: [ProgEq] -> [CaseMatrix]
matriPEq :: ProgEq -> CaseMatrix
matriArg :: Term -> Term -> CaseMatrix
concentrate :: [CaseMatrix] -> Env -> CaseMatrix
groupByArgs :: [CaseMatrix] -> Int -> [CaseMatrix]
redArgs :: Env -> [CaseMatrix] -> CaseMatrix
redAppl :: [CaseMatrix] -> Env -> CaseMatrix
recArgs :: Env -> [ProgEq] -> [ProgEq]
shrinkPat :: CaseMatrix -> Term
patIsVar :: ProgEq -> Bool
termIsVar :: Term -> Bool
patHasNoArg :: ProgEq -> Bool
termHasNoArg :: Term -> Bool
transCaseAlt :: Env -> ProgEq -> (Term, Term)
transPat :: Env -> Term -> Term
binConst :: String -> Term -> Term -> Term
isaPair :: String

Documentation

data HasCASL2IsabelleHOL Source #

The identity of the comorphism

Constructors

HasCASL2IsabelleHOL

Instances

Instances details

Show HasCASL2IsabelleHOL Source #
Instance details Defined in Comorphisms.HasCASL2IsabelleHOL Methods showsPrec :: Int -> HasCASL2IsabelleHOL -> ShowS show :: HasCASL2IsabelleHOL -> String showList :: [HasCASL2IsabelleHOL] -> ShowS
Language HasCASL2IsabelleHOL Source #
Instance details Defined in Comorphisms.HasCASL2IsabelleHOL Methods language_name :: HasCASL2IsabelleHOL -> String Source # description :: HasCASL2IsabelleHOL -> String Source #
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.HasCASL2IsabelleHOL Methods sourceLogic :: HasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: HasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: HasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: HasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: HasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: HasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: HasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: HasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: HasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: HasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: HasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: HasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: HasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: HasCASL2IsabelleHOL -> Bool Source # constituents :: HasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: HasCASL2IsabelleHOL -> Bool Source # rps :: HasCASL2IsabelleHOL -> Bool Source # eps :: HasCASL2IsabelleHOL -> Bool Source # isGTC :: HasCASL2IsabelleHOL -> Bool Source #

Signature

baseSign :: BaseSig Source #

transSignature :: Env -> Result (Sign, [Named Sentence]) Source #

translation of a type in an operation declaration

transOpInfo :: OpInfo -> Maybe Typ Source #

transOpType :: TypeScheme -> Typ Source #

transType :: Type -> Typ Source #

translation of a datatype declaration

transDatatype :: TypeMap -> DomainTab Source #

transDataEntry :: DataEntry -> [DomainEntry] Source #

transTypeArg :: TypeArg -> Typ Source #

transAltDefn :: AltDefn -> (VName, [Typ]) Source #

Formulas

transVar :: Id -> VName Source #

transSentence :: Env -> Sentence -> Maybe Term Source #

transOpId :: Env -> Id -> TypeScheme -> String Source #

transProgEq :: Env -> ProgEq -> (Term, Term) Source #

transTerm :: Env -> Term -> Term Source #

transAppl :: Env -> Maybe Type -> Term -> Term -> Term Source #

mkApp :: String -> Env -> Term -> Term -> Term Source #

transApplOp :: Env -> Type -> Term -> Term -> Term Source #

transLog :: Env -> Id -> Term -> Term -> Term Source #

transWhenElse :: Env -> Term -> Term Source #

when else statement

translation of lambda abstractions

abstraction :: Env -> Term -> Term -> Term Source #

transPattern :: Env -> Term -> Term Source #

transTotalLambda :: Env -> Term -> Term Source #

translation of case alternatives

arangeCaseAlts :: Env -> [ProgEq] -> [(Term, Term)] Source #

sortCaseAlts :: Env -> [ProgEq] -> [(Term, Term)] Source #

getCons :: Env -> Id -> [Id] Source #

getName :: ProgEq -> Id Source #

getTypeName :: Term -> Id Source #

groupCons :: [ProgEq] -> Id -> [ProgEq] Source #

flattenPattern :: Env -> [ProgEq] -> (Term, Term) Source #

data CaseMatrix Source #

Constructors

CaseMatrix
Fields patBrand :: PatBrand cons :: Maybe Term args :: [Term] newArgs :: [Term] term :: Term

Instances

Instances details

Eq CaseMatrix Source #
Instance details Defined in Comorphisms.HasCASL2IsabelleHOL Methods (==) :: CaseMatrix -> CaseMatrix -> Bool (/=) :: CaseMatrix -> CaseMatrix -> Bool
Ord CaseMatrix Source #
Instance details Defined in Comorphisms.HasCASL2IsabelleHOL Methods compare :: CaseMatrix -> CaseMatrix -> Ordering (<) :: CaseMatrix -> CaseMatrix -> Bool (<=) :: CaseMatrix -> CaseMatrix -> Bool (>) :: CaseMatrix -> CaseMatrix -> Bool (>=) :: CaseMatrix -> CaseMatrix -> Bool max :: CaseMatrix -> CaseMatrix -> CaseMatrix min :: CaseMatrix -> CaseMatrix -> CaseMatrix
Show CaseMatrix Source #
Instance details Defined in Comorphisms.HasCASL2IsabelleHOL Methods showsPrec :: Int -> CaseMatrix -> ShowS show :: CaseMatrix -> String showList :: [CaseMatrix] -> ShowS

data PatBrand Source #

Constructors

Appl
Tuple
QuOp
QuVar

Instances

Instances details

Eq PatBrand Source #
Instance details Defined in Comorphisms.HasCASL2IsabelleHOL Methods (==) :: PatBrand -> PatBrand -> Bool (/=) :: PatBrand -> PatBrand -> Bool
Ord PatBrand Source #
Instance details Defined in Comorphisms.HasCASL2IsabelleHOL Methods compare :: PatBrand -> PatBrand -> Ordering (<) :: PatBrand -> PatBrand -> Bool (<=) :: PatBrand -> PatBrand -> Bool (>) :: PatBrand -> PatBrand -> Bool (>=) :: PatBrand -> PatBrand -> Bool max :: PatBrand -> PatBrand -> PatBrand min :: PatBrand -> PatBrand -> PatBrand
Show PatBrand Source #
Instance details Defined in Comorphisms.HasCASL2IsabelleHOL Methods showsPrec :: Int -> PatBrand -> ShowS show :: PatBrand -> String showList :: [PatBrand] -> ShowS