IsaConsts.hs revision ce31795240d8fb340bc984b8b35147c955e29afa
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederModule : $Header$
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederDescription : constants for Isabelle terms
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian 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
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder-- | a topological sort with a @uses@ predicate
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederquickSort :: (a -> a -> Bool) -> [a] -> [a]
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederquickSort f ls = case ls of
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder a : as -> let (xs, ys) = partition (f a) as in
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder quickSort f xs ++ a : quickSort f ys
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- **** STRINGS ------------------------------------------------
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- * boolean constants
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedercTrue :: String
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaedercTrue = "True"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedercFalse :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedercFalse = "False"
ae59cddaa1f9e2dd031cae95a3ba867b9e8e095dPaolo Torrini-- | Not string
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedercNot :: String
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder-- * quantor strings
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederallS, exS, ex1S :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- * Strings of binary ops
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederconj :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederdisj :: String
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian 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
10a92a06296c3c8d522543de7e3a4534bf528505Paolo TorrinimodS = "op mod"
10a92a06296c3c8d522543de7e3a4534bf528505Paolo TorriniconsS :: 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" -- "***"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederlSumS = "either"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- * some stuff for HasCASL
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederaptS :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederappS :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederpAppS :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederpAppS = "pApp"