IsaConsts.hs revision 4ef05f4edeb290beb89845f57156baa5298af7c4
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederModule : $Header$
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederCopyright : (c) Sonja Groening, Christian Maeder, Uni Bremen 2004-2005
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : maeder@tzi.de
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederStability : provisional
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederPortability : portable
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederutilities for the (Has)CASL, Haskell to Isabelle comorphisms
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- possibly differentiate between HOL and HOLCF
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- * predefined sorts
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederholType :: Sort
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederholType = [IsaClass "hol_type"]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederisaTerm :: IsaClass
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederisaTerm = IsaClass "type"
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederpcpo :: IsaClass
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederpcpo = IsaClass "pcpo"
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- * predefinded types
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedernoType = Type "dummy" holType []
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederboolType :: Typ
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederboolType = Type "bool" holType []
603e326e7b189de8c1e4ea8c89470b3a61154019Christian MaederintType :: Typ
603e326e7b189de8c1e4ea8c89470b3a61154019Christian MaederintType = Type "int" holType []
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkOptionType :: Typ -> Typ
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkOptionType t = Type "option" holType [t]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederprodType :: Typ -> Typ -> Typ
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederprodType t1 t2 = Type prodS holType [t1,t2]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkFunType :: Typ -> Typ -> Typ
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkFunType s t = Type funS holType [s,t] -- was "-->" before
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder{-handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)-}
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkCurryFunType :: [Typ] -> Typ -> Typ
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkCurryFunType = flip $ foldr mkFunType -- was "--->" before
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedervoidDom :: Typ
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedervoidDom = Type "void" dom []
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder{- should this be included (as primitive)? -}
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederflatDom :: Typ
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederflatDom = Type "flat" dom []
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder{- sort is ok? -}
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkContFun :: Typ -> Typ -> Typ
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian MaedermkContFun t1 t2 = Type cFunS dom [t1,t2]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkStrictProduct :: Typ -> Typ -> Typ
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian MaedermkStrictProduct t1 t2 = Type sProdS dom [t1,t2]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkContProduct :: Typ -> Typ -> Typ
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian MaedermkContProduct t1 t2 = Type prodS dom [t1,t2]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder{-handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)-}
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkCurryContFun :: [Typ] -> Typ -> Typ
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkCurryContFun = flip $ foldr mkContFun -- was "--->" before
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkStrictSum :: Typ -> Typ -> Typ
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian MaedermkStrictSum t1 t2 = Type sSumS dom [t1,t2]
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian MaederprodS, sProdS, funS, cFunS, sSumS :: TName
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederprodS = "*" -- this is printed as it is!
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- * functions for term formation
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaedermaxPrio :: Int
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaedermaxPrio = 1000
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaederlowPrio :: Int
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaederisaEqPrio :: Int
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaederisaEqPrio = 2 -- left assoc
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedertermAppl :: Term -> Term -> Term
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaedertermAppl t1 t2 = MixfixApp t1 [t2] NotCont
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaedertermMixfixAppl :: Term -> [Term] -> Term
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaedertermMixfixAppl t1 t2 = MixfixApp t1 t2 NotCont
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | apply binary operation to arguments
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederbinConst :: String -> Term -> Term -> Term
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederbinConst s t1 t2 = MixfixApp (conDouble s) [t1,t2] NotCont
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | construct a constant with no type
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maedercon :: VName -> Term
ae59cddaa1f9e2dd031cae95a3ba867b9e8e095dPaolo Torrinicon s = Const s noType
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederconDouble :: String -> Term
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederconDouble = con . mkVName
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- * some stuff
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedersomeS :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedersomeS = "Some"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederconSomeT :: Typ -> Term
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederconSomeT t = Const (mkVName someS) t
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | some constant with no type
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederconSome :: Term
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederconSome = conDouble someS
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | defOp constant
c36dc42a63287db1e3e81b03ee5655aed69e7cdeChristian MaederdefOp = conDouble "defOp"
4ef05f4edeb290beb89845f57156baa5298af7c4Christian MaedernotS :: String
4ef05f4edeb290beb89845f57156baa5298af7c4Christian MaedernotV = VName notS $ Just $ AltSyntax "~/ _" [40] 40
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | not constant
4ef05f4edeb290beb89845f57156baa5298af7c4Christian MaedernotOp = con notV
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 -->"
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederconjV :: VName
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederconjV = VName conj $ Just $ AltSyntax "(_ &/ _)" [36, 35] 35
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederdisjV :: VName
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederdisjV = VName disj $ Just $ AltSyntax "(_ |/ _)" [31, 30] 30
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederimplV :: VName
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederimplV = VName impl $ Just $ AltSyntax "(_ -->/ _)" [26, 25] 25
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaedereqV = VName eq $ Just $ AltSyntax "(_ =/ _)" [50, 51] 50
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederplusS :: String
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederplusS = "op +"
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederminusS :: String
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederminusS = "op -"
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaedertimesS :: String
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaedertimesS = "op *"
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederconsS :: String
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederconsS = "Cons"
4ef05f4edeb290beb89845f57156baa5298af7c4Christian MaederplusV :: VName
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederplusV = VName plusS $ Just $ AltSyntax "(_ +/ _)" [65, 66] 65
4ef05f4edeb290beb89845f57156baa5298af7c4Christian MaederminusV :: VName
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederminusV = VName minusS $ Just $ AltSyntax "(_ -/ _)" [65, 66] 65
4ef05f4edeb290beb89845f57156baa5298af7c4Christian MaedertimesV :: VName
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaedertimesV = VName timesS $ Just $ AltSyntax "(_ */ _)" [70, 71] 70
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederconsV :: VName
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederconsV = VName consS $ Just $ AltSyntax "(_ #/ _)" [66, 65] 65
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaederbinVNameAppl :: VName -> Term -> Term -> Term
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaederbinVNameAppl v t1 t2 = MixfixApp (con v) [t1,t2] NotCont
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- * binary junctors
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederbinConj, binDisj, binImpl, binEqv, binEq :: Term -> Term -> Term
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederbinConj = binVNameAppl conjV
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederbinDisj = binVNameAppl disjV
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederbinImpl = binVNameAppl implV
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederbinEq = binVNameAppl eqV
613bf0ed7d98a961755408ead328687ec17f74fdChristian MaederbinEqv = binEq
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- * boolean constants
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maedertrue, false :: Term
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maedertrue = Const (mkVName "True") boolType
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederfalse = Const (mkVName "False") boolType
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | pair stuff
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederpairC :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederpairC = "pair"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederisaPair :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederisaPair = "Pair"