Hets - the Heterogeneous Tool Set

Copyright(c) Sonja Groening C. Maeder Uni Bremen 2003-2006
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilitynon-portable (imports Logic.Logic)
Safe HaskellNone

Comorphisms.HasCASL2IsabelleHOL

Contents

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

Documentation

data HasCASL2IsabelleHOL Source #

The identity of the comorphism

Constructors

HasCASL2IsabelleHOL 

Instances

Show HasCASL2IsabelleHOL Source # 

Methods

showsPrec :: Int -> HasCASL2IsabelleHOL -> ShowS

show :: HasCASL2IsabelleHOL -> String

showList :: [HasCASL2IsabelleHOL] -> ShowS

Language HasCASL2IsabelleHOL Source # 
Comorphism HasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source # 

Signature

translation of a type in an operation declaration

translation of a datatype declaration

Formulas

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

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

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

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

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

when else statement

translation of lambda abstractions

translation of case alternatives

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

data CaseMatrix Source #

Constructors

CaseMatrix 

Fields

Instances

Eq CaseMatrix Source # 

Methods

(==) :: CaseMatrix -> CaseMatrix -> Bool

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

Ord CaseMatrix Source # 
Show CaseMatrix Source # 

Methods

showsPrec :: Int -> CaseMatrix -> ShowS

show :: CaseMatrix -> String

showList :: [CaseMatrix] -> ShowS

data PatBrand Source #

Constructors

Appl 
Tuple 
QuOp 
QuVar 

Instances

Eq PatBrand Source # 

Methods

(==) :: PatBrand -> PatBrand -> Bool

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

Ord PatBrand Source # 

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 # 

Methods

showsPrec :: Int -> PatBrand -> ShowS

show :: PatBrand -> String

showList :: [PatBrand] -> ShowS

patIsVar :: ProgEq -> Bool Source #

termIsVar :: Term -> Bool Source #

binConst :: String -> Term -> Term -> Term Source #

apply binary operation to arguments

isaPair :: String Source #

upper case curried pair constructor