IsaConsts.hs revision 10a92a06296c3c8d522543de7e3a4534bf528505
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
d6025ee06343191f356a59704d467866afa29900Paolo TorriniconT :: String -> Term
ae59cddaa1f9e2dd031cae95a3ba867b9e8e095dPaolo TorriniconT s = Const s noType
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | construct a constant with no type
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedercon :: String -> Term
ae59cddaa1f9e2dd031cae95a3ba867b9e8e095dPaolo Torrinicon s = Const s noType
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- * some stuff
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedersomeS :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedersomeS = "Some"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederconSomeT :: Typ -> Term
ae59cddaa1f9e2dd031cae95a3ba867b9e8e095dPaolo TorriniconSomeT t = Const 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
10a92a06296c3c8d522543de7e3a4534bf528505Paolo Torrinicappl :: String
10a92a06296c3c8d522543de7e3a4534bf528505Paolo Torrinicappl = "op $"
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
ae59cddaa1f9e2dd031cae95a3ba867b9e8e095dPaolo Torrinitrue = Const "True" boolType
ae59cddaa1f9e2dd031cae95a3ba867b9e8e095dPaolo Torrinifalse = Const "False" boolType
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | pair stuff
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederpairC :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederpairC = "pair"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederisaPair :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederisaPair = "Pair"
7f39d44f0b8c39a92606ba06fd668dc0cc2752caPaolo TorriniboolT = Type "boolT" dom []
7f39d44f0b8c39a92606ba06fd668dc0cc2752caPaolo TorriniisaOr = Const "OR" (mkContFun boolT (mkContFun boolT boolT))
7f39d44f0b8c39a92606ba06fd668dc0cc2752caPaolo TorrinimkIsaOr :: Term -> Term -> Term
7f39d44f0b8c39a92606ba06fd668dc0cc2752caPaolo TorrinimkIsaOr t1 t2 = App (App isaOr t1 IsCont) t2 IsCont