IsaConsts.hs revision a2e8cca8a8217b158b0b7a760e8234c03186456d
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederModule : $Header$
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederDescription : constants for Isabelle terms
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederCopyright : (c) Sonja Groening, Christian Maeder, Uni Bremen 2004-2006
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederMaintainer : Christian.Maeder@dfki.de
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederStability : provisional
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederPortability : portable
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederconstants for Isabelle
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- possibly differentiate between HOL and HOLCF
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | a topological sort with a @uses@ predicate
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederquickSort :: (a -> a -> Bool) -> [a] -> [a]
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederquickSort f ls = case ls of
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder a : as -> let (xs, ys) = partition (f a) as in
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder quickSort f xs ++ a : quickSort f ys
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- **** STRINGS ------------------------------------------------
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- * boolean constants
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedercTrue :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedercTrue = "True"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedercFalse :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedercFalse = "False"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | Not string
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedercNot :: String
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 MaederplusS :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederplusS = "op +"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederminusS :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederminusS = "op -"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedertimesS :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedertimesS = "op *"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederdivS :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederdivS = "op div"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedermodS :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedermodS = "op mod"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederconsS :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederconsS = "Cons"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedercompS :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedercompS = "comp"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | lower case pair
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederpairC :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederpairC = "pair"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- * some stuff for Isabelle
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederpcpoS :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederpcpoS = "pcpo"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederprodS, sProdS, funS, cFunS, lFunS, sSumS, lProdS, lSumS :: TName
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederprodS = "*" -- this is printed as it is!
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederlProdS = "lprod" -- "***"