IsaConsts.hs revision eaa2614d79ad5ef6a6b9b08c7e6dde46c5ad1fb3
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederModule : $Header$
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederCopyright : (c) Sonja Groening, Christian Maeder, Uni Bremen 2004
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederMaintainer : hets@tzi.de
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederStability : provisional
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederPortability : portable
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder utilities for the HasCASL to Isabelle comorphism
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | application
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedertermAppl :: Term -> Term -> Term
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedertermAppl t1 t2 = App t1 t2 NotCont
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | apply binary operation to arguments
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederbinConst :: String -> Term -> Term -> Term
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederbinConst s t1 t2 = termAppl (termAppl (con s) t1) t2
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | construct a constant
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederconT :: String -> Typ -> Term
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederconT s t = Const s t isaTerm
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | construct a constant with no type
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedercon :: String -> Term
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedercon s = conT s noType
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- * some stuff
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedersomeS :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedersomeS = "Some"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederconSomeT :: Typ -> Term
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederconSomeT t = conT someS t
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | some constant with no type
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederconSome :: Term
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederconSome = con someS
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | defOp constant
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederdefOp = con "defOp"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | not constant
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedernotOp = con "Not"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- * quantor strings
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederallS, exS, ex1S :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- * strings of binary ops
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederconj :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederdisj :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimpl :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimpl = "op -->"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- * binary junctors
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederbinConj, binDisj, binImpl, binEqv, binEq :: Term -> Term -> Term
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederbinConj= binConst conj
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederbinDisj = binConst disj
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederbinImpl = binConst impl
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederbinEq = binConst eq
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederbinEqv = binConst eqv
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- * boolean constants
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedertrue, false :: Term
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedertrue = con "True"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederfalse = con "False"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | pair stuff
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederpairC :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederpairC = "pair"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederisaPair :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederisaPair = "Pair"