IsaConsts.hs revision 65b2ea4773bb729446afa803ad14ae2c011e29be
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederModule : $Header$
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederDescription : constants for Isabelle terms
cd7372fc7e6e43c389619f63daa6eb872d9d5b16Christian MaederCopyright : (c) Sonja Groening, Christian Maeder, Uni Bremen 2004-2006
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederMaintainer : Christian.Maeder@dfki.de
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederStability : provisional
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederPortability : portable
99c923311eab71a85f1dcc4785d349609c828da4Christian Maederconstants for Isabelle
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- possibly differentiate between HOL and HOLCF
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maederimport qualified Data.Set as Set
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroederimport qualified Data.Map as Map
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder-- | a topological sort with a @uses@ predicate
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaedertopSort :: (a -> a -> Bool) -> [a] -> [a]
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaedertopSort f ls = case ls of
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder a : as -> let
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder (directPreds, rest) = partition (f a) as
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder in if null directPreds then a : topSort f as else
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder topSort f $ filter (not . flip f a) directPreds ++ a : rest
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- | extends a dependency relation to lists using any
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaederliftDep :: (a -> a -> Bool) -> [a] -> [a] -> Bool
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaederliftDep f as bs = any (\ a -> any (f a) bs) as
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaedergetTypeIds :: Typ -> Set.Set TName
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaedergetTypeIds ty = case ty of
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder Type { typeId = n, typeArgs = args }
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder -> Set.insert n $ Set.unions $ map getTypeIds args
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaederdeDepOn :: DomainEntry -> DomainEntry -> Bool
90d97972167d142dde6ee8b18d9625332040261fJonathan von SchroederdeDepOn (_, l) (t, _) =
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder Set.member (typeId t) $ Set.unions $ concatMap (map getTypeIds . snd) l
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaederordDoms :: DomainTab -> DomainTab
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaederordDoms = topSort (liftDep deDepOn)
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- * boolean constants strings
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicTrue :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicTrue = "True"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicFalse :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicFalse = "False"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | Not string
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicNot :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- * quantor strings
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniallS, exS, ex1S :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- * Strings of binary ops
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torriniconj :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinidisj :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torriniimpl :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torriniimpl = "op -->"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniplusS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniplusS = "op +"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniminusS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniminusS = "op -"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitimesS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitimesS = "op *"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinidivS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinidivS = "op div"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimodS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimodS = "op mod"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniconsS :: String
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniconsS = "op #"
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaederlconsS :: String
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinilconsS = "op ###"
65b2ea4773bb729446afa803ad14ae2c011e29beSoeren D. SchulzeappendS :: String
65b2ea4773bb729446afa803ad14ae2c011e29beSoeren D. SchulzeappendS = "op @"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicompS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicompS = "comp"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | lower case pair
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinipairC :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinipairC = "pair"
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillyeqvSimS :: String
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillyeqvSimS = "eqvS"
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'ReillyunionS :: String
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'ReillyunionS = "op Un"
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- Set membership
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillymembershipS :: String
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillymembershipS = "op :"
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly-- | Imange of functions
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillyimageS :: String
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillyimageS = "image"
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillyrangeS :: String
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillyrangeS = "range"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- * some stuff for Isabelle
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederpcpoS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederpcpoS = "pcpo"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniprodS, sProdS, funS, cFunS, lFunS, sSumS, lProdS, lSumS :: TName
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniprodS = "*" -- this is printed as it is!
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinilProdS = "lprod" -- "***"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinilSumS = "either"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- * some stuff for HasCASL
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniaptS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniappS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinipAppS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinipAppS = "pApp"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinidefOpS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinidefOpS = "defOp"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | Some string
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisomeS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisomeS = "Some"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- * strings for HOLCF lifting functions
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinilliftbinS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinilliftbinS = "lliftbin"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinifliftbinS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinifliftbinS = "fliftbin"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torriniflift2S :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torriniflift2S = "flift2"
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- * Predefined CLASSES
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maederpcpo :: IsaClass
99c923311eab71a85f1dcc4785d349609c828da4Christian Maederpcpo = IsaClass pcpoS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniisaTerm :: IsaClass
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniisaTerm = IsaClass "type"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- * predefined SORTS
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo TorriniholType :: Sort
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo TorriniholType = [isaTerm]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisortT :: Continuity -> Sort
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaedersortT a = case a of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini NotCont -> holType
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont _ -> dom
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaedermkSTypeT :: Continuity -> String -> Typ
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaedermkSTypeT a s = Type s (sortT a) []
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- ------------------- POLY TYPES --------------------------------------
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinilistT :: Continuity -> Typ -> Typ
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaederlistT a t = Type (case a of
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder IsCont _ -> "llist"
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder NotCont -> "list") (sortT a) [t]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicharT :: Continuity -> Typ
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaedercharT a = mkSTypeT a $ case a of
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder IsCont _ -> "charT"
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder NotCont -> "char"
c730c28919b53f940ed319ebb42780244c528e29Paolo TorriniratT :: Continuity -> Typ
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaederratT a = mkSTypeT a $ case a of
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder IsCont _ -> "ratT"
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder NotCont -> "rat"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinifracT :: Continuity -> Typ
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaederfracT a = mkSTypeT a "fracT"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniintegerT :: Continuity -> Typ
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaederintegerT a = mkSTypeT a $ case a of
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder IsCont _ -> "integerT"
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder NotCont -> "int"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniboolT :: Continuity -> Typ
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaederboolT a = mkSTypeT a $ case a of
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder IsCont _ -> "lBool"
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder NotCont -> "bool"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniorderingT :: Continuity -> Typ
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaederorderingT a = mkSTypeT a $ case a of
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder IsCont _ -> "lOrdering"
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder NotCont -> "sOrdering"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniintT :: Continuity -> Typ
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaederintT a = mkSTypeT a $ case a of
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder IsCont _ -> "intT"
8fdd06d4f6530909e3e24547893a62b042117fb4Christian Maeder NotCont -> "int"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniprodT :: Continuity -> Typ -> Typ -> Typ
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaederprodT a t1 t2 = case a of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont _ -> mkContProduct t1 t2
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder NotCont -> prodType t1 t2
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinifunT :: Continuity -> Typ -> Typ -> Typ
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinifunT c a b = case c of
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini IsCont _ -> mkContFun a b
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder NotCont -> mkFunType a b
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinicurryFunT :: Continuity -> [Typ] -> Typ -> Typ
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinicurryFunT c ls x = case c of
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini IsCont _ -> mkCurryContFun ls x
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder NotCont -> mkCurryFunType ls x
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- * predefined types
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaedermkSType :: String -> Typ
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaedermkSType = mkSTypeT NotCont
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrininoTypeT :: Typ
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaedernoTypeT = mkSType "dummy"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrininoType :: DTyp
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrininoType = Hide noTypeT NA Nothing
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrininoTypeC :: DTyp
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrininoTypeC = Hide noTypeT TCon Nothing
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinihideNN :: Typ -> DTyp
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaederhideNN t = Hide t NA Nothing
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinihideCN :: Typ -> DTyp
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaederhideCN t = Hide t TCon Nothing
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinidispNN :: Typ -> DTyp
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaederdispNN t = Disp t NA Nothing
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinidispMN :: Typ -> DTyp
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaederdispMN t = Disp t TMet Nothing
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederboolType :: Typ
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniboolType = boolT NotCont
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkListType :: Typ -> Typ
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaedermkListType = listT NotCont
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkOptionType :: Typ -> Typ
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkOptionType t = Type "option" holType [t]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederprodType :: Typ -> Typ -> Typ
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaederprodType t1 t2 = Type prodS holType [t1, t2]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkFunType :: Typ -> Typ -> Typ
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaedermkFunType s t = Type funS holType [s, t] -- was "-->" before
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkCurryFunType :: [Typ] -> Typ -> Typ
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkCurryFunType = flip $ foldr mkFunType -- was "--->" before
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- * predefinded HOLCF types
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaedermkSDomType :: String -> Typ
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaedermkSDomType s = Type s dom []
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedervoidDom :: Typ
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaedervoidDom = mkSDomType "void"
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- should this be included (as primitive)?
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederflatDom :: Typ
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaederflatDom = mkSDomType "flat"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitLift :: Typ -> Typ
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitLift t = Type "lift" dom [t]
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaedermkBinDomType :: String -> Typ -> Typ -> Typ
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaedermkBinDomType s t1 t2 = Type s dom [t1, t2]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkContFun :: Typ -> Typ -> Typ
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaedermkContFun = mkBinDomType lFunS
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkStrictProduct :: Typ -> Typ -> Typ
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaedermkStrictProduct = mkBinDomType sProdS
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkContProduct :: Typ -> Typ -> Typ
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaedermkContProduct = mkBinDomType lProdS
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkCurryContFun :: [Typ] -> Typ -> Typ
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaedermkCurryContFun = flip $ foldr mkContFun
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkStrictSum :: Typ -> Typ -> Typ
8fdd06d4f6530909e3e24547893a62b042117fb4Christian MaedermkStrictSum = mkBinDomType lSumS
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- * term construction
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaedermaxPrio :: Int
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaedermaxPrio = 1000
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaederlowPrio :: Int
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaederisaEqPrio :: Int
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaederisaEqPrio = 2 -- left assoc
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | construct constants and variables
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkConstVD :: String -> Typ -> Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkConstVD s t = Const (mkVName s) $ hideNN t
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkConstV :: String -> DTyp -> Term
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaedermkConstV = Const . mkVName
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkConstD :: VName -> Typ -> Term
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaedermkConstD s = Const s . hideNN
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkConst :: VName -> DTyp -> Term
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaedermkConst = Const
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkFree :: String -> Term
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaedermkFree = Free . mkVName
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | construct a constant with no type
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maedercon :: VName -> Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinicon s = mkConst s noType
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniconC :: VName -> Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniconC s = mkConst s noTypeC
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederconDouble :: String -> Term
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederconDouble = con . mkVName
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniconDoubleC :: String -> Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniconDoubleC = conC . mkVName
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | apply VName operator to two term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinibinVNameAppl :: VName -> Term -> Term -> Term
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaederbinVNameAppl v = termAppl . termAppl (con v)
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- * binary junctors
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillybinConj, binDisj, binImpl, binEqv, binEq, binEqvSim, binUnion,
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly binMembership, binImageOp
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly :: Term -> Term -> Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinibinConj = binVNameAppl conjV
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinibinDisj = binVNameAppl disjV
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinibinImpl = binVNameAppl implV
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinibinEq = binVNameAppl eqV
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinibinEqv = binEq
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillybinEqvSim = binVNameAppl eqvSimV
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'ReillybinUnion = binVNameAppl unionV
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillybinMembership = binVNameAppl membershipV
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillybinImageOp = binVNameAppl imageV
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillyrangeOp :: Term -> Term
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaederrangeOp = termAppl (con rangeV)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | HOL function application
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitermAppl :: Term -> Term -> Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitermAppl t1 t2 = App t1 t2 NotCont
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- * terms for HOL-HOLCF
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniandPT :: Continuity -> Term
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaederandPT a = case a of
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder NotCont -> con conjV
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont _ -> conDouble "andH"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniorPT :: Continuity -> Term
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaederorPT a = case a of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini NotCont -> con disjV
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont _ -> conDouble "orH"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrininotPT :: Continuity -> Term
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaedernotPT a = case a of
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder NotCont -> con notV
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont _ -> conDouble "notH"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinibottomPT :: Continuity -> Term
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaederbottomPT a = conDouble $ case a of
ec59d0f6f0e61272419be22982155bde741bf5b3Jonathan von Schroeder NotCont -> "undefined"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont _ -> "UU"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrininilPT :: Continuity -> Term
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrininilPT a = conDoubleC $ case a of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini NotCont -> "[]"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont _ -> "lNil"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniconsPT :: Continuity -> Term
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaederconsPT a = case a of
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder NotCont -> conC consV
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder IsCont True -> conDouble "llCons"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini IsCont False -> conC lconsV
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitruePT :: Continuity -> Term
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinitruePT a = conDoubleC $ case a of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini NotCont -> "True"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont _ -> "TRUE"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinifalsePT :: Continuity -> Term
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinifalsePT a = conDoubleC $ case a of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini NotCont -> "False"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont _ -> "FALSE"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniheadPT :: Continuity -> Term
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniheadPT a = conDouble $ case a of
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini NotCont -> "hd"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini IsCont _ -> "llHd"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinitailPT :: Continuity -> Term
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinitailPT a = conDouble $ case a of
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini NotCont -> "tl"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini IsCont _ -> "llTl"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniunitPT :: Continuity -> Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniunitPT a = case a of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini NotCont -> conDouble "()"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont _ -> termAppl (conDouble "Def") (conDouble "()")
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinifstPT :: Continuity -> Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinifstPT a = case a of
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini NotCont -> conDoubleC "fst"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont True -> conDouble "llfst"
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder IsCont False -> conDoubleC "lfst"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisndPT :: Continuity -> Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisndPT a = case a of
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini NotCont -> conDoubleC "snd"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont True -> conDouble "llsnd"
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder IsCont False -> conDoubleC "lsnd"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinipairPT :: Continuity -> Term
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaederpairPT a = case a of
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder NotCont -> conDoubleC "pair"
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder IsCont True -> conDouble "llpair"
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder IsCont False -> conDoubleC "lpair"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrininothingPT :: Continuity -> Term
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaedernothingPT a = conDouble $ if a == NotCont
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini then "None" else "lNothing"
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaederjustPT :: Continuity -> Term
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinijustPT a = case a of
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini NotCont -> conDouble "Some"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini IsCont True -> conDouble "llJust"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini IsCont False -> conDoubleC "lJust"
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaederleftPT :: Continuity -> Term
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinileftPT a = case a of
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini NotCont -> conDouble "left"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini IsCont True -> conDouble "llLeft"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini IsCont False -> conDoubleC "lLeft"
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaederrightPT :: Continuity -> Term
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinirightPT a = case a of
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini NotCont -> conDouble "right"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini IsCont True -> conDouble "llRight"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini IsCont False -> conDoubleC "lRight"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinicompPT :: Term
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinicompPT = conDouble "compH"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinieqPT = conDouble "eqH"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinineqPT = conDouble "neqH"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinieqTPT :: Typ -> Term
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaedereqTPT = mkConstVD "eqH"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinineqTPT :: Typ -> Term
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaederneqTPT = mkConstVD "neqH"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- * Boolean constants
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinitrue = mkConstVD cTrue boolType
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinifalse = mkConstVD cFalse boolType
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- * UNTYPED terms
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder-- | defOp constant
5e4812721f9026ae4ae54381a5fdeb163489087dChristian MaederdefOp = conDouble defOpS
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | Not constant
4ef05f4edeb290beb89845f57156baa5298af7c4Christian MaedernotOp = con notV
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | some constant
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniconSome :: Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniconSome = conDouble someS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniliftString :: Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniliftString = conDouble "liftList"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinilpairTerm :: Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinilpairTerm = conDoubleC "lpair"
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- * constant names
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | Not VName
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrininotV = VName cNot $ Just $ AltSyntax "~/ _" [40] 40
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- * VNames of binary operators
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederconjV :: VName
f4a74236e18cc4f4b905bc1dba94919bd97950f4Christian MaederconjV = VName conj $ Just $ AltSyntax "(_ &/ _)" [36, 35] 35
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederdisjV :: VName
f4a74236e18cc4f4b905bc1dba94919bd97950f4Christian MaederdisjV = VName disj $ Just $ AltSyntax "(_ |/ _)" [31, 30] 30
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederimplV :: VName
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederimplV = VName impl $ Just $ AltSyntax "(_ -->/ _)" [26, 25] 25
f4a74236e18cc4f4b905bc1dba94919bd97950f4Christian MaedereqV = VName eq $ Just $ AltSyntax "(_ =/ _)" [50, 51] 50
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von SchroederneqV = VName neq $ Just $ AltSyntax "(_ ~=/ _)" [50, 51] 50
4ef05f4edeb290beb89845f57156baa5298af7c4Christian MaederplusV :: VName
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaederplusV = VName plusS $ Just $ AltSyntax "(_ +/ _)" [65, 66] 65
4ef05f4edeb290beb89845f57156baa5298af7c4Christian MaederminusV :: VName
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederminusV = VName minusS $ Just $ AltSyntax "(_ -/ _)" [65, 66] 65
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo TorrinidivV = VName divS $ Just $ AltSyntax "(_ div/ _)" [70, 71] 70
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo TorrinimodV = VName modS $ Just $ AltSyntax "(_ mod/ _)" [70, 71] 70
4ef05f4edeb290beb89845f57156baa5298af7c4Christian MaedertimesV :: VName
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaedertimesV = VName timesS $ Just $ AltSyntax "(_ */ _)" [70, 71] 70
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederconsV :: VName
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederconsV = VName consS $ Just $ AltSyntax "(_ #/ _)" [66, 65] 65
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinilconsV :: VName
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinilconsV = VName lconsS $ Just $ AltSyntax "(_ ###/ _)" [66, 65] 65
65b2ea4773bb729446afa803ad14ae2c011e29beSoeren D. SchulzeappendV :: VName
65b2ea4773bb729446afa803ad14ae2c011e29beSoeren D. SchulzeappendV = VName appendS $ Just $ AltSyntax "(_ @ _)" [66, 65] 65
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaedercompV :: VName
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaedercompV = VName compS $ Just $ AltSyntax "(_ o/ _)" [55, 56] 55
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillyeqvSimV :: VName
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaedereqvSimV = VName eqvSimS $ Just $ AltSyntax "(_ \\<sim>/ _)" [50, 51] 50
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'ReillyunionV :: VName
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaederunionV = VName unionS $ Just $ AltSyntax "(_ \\<union>/ _)" [65, 66] 65
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillymembershipV :: VName
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaedermembershipV = VName membershipS $ Just $ AltSyntax "(_ \\<in>/ _)" [65, 66] 65
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillyimageV :: VName
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaederimageV = VName imageS $ Just $ AltSyntax "(_ `/ _)" [65, 66] 65
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillyrangeV :: VName
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillyrangeV = VName rangeS Nothing
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von SchroedervMap' :: Map.Map String VName
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von SchroedervMap' = Map.fromList [(conj,conjV), (disj,disjV), (impl,implV), (eq,eqV),
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder (neq,neqV), (plusS,plusV), (minusS,minusV), (divS,divV), (modS,modV),
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder (timesS,timesV), (consS,consV), (lconsS,lconsV), (compS,compV),
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder (eqvSimS,eqvSimV), (unionS,unionV), (membershipS,membershipV),
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder (imageS,imageV), (rangeS,rangeV)]
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von SchroedervMap :: Map.Map String VName
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder (map (\(k,v) -> if take 3 k == "op "
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder then (drop 3 k,v)
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder else (k,v)) (Map.toList vMap')))
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- * keywords in theory files from the Isar Reference Manual 2005
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederendS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederheaderS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederheaderS = "header"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedertheoryS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedertheoryS = "theory"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederimportsS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederimportsS = "imports"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederusesS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederusesS = "uses"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederbeginS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederbeginS = "begin"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedercontextS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedercontextS = "context"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederaxiomsS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederaxiomsS = "axioms"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederdefsS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederdefsS = "defs"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederoopsS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederoopsS = "oops"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederandS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederlemmasS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederlemmasS = "lemmas"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederlemmaS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederlemmaS = "lemma"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedercorollaryS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedercorollaryS = "corollary"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederrefuteS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederrefuteS = "refute"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedertheoremsS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedertheoremsS = "theorems"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedertheoremS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedertheoremS = "theorem"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederaxclassS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederaxclassS = "axclass"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederclassesS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederclassesS = "classes"
269c98e2ccf268d3d5d19d46d3d242fad726b882Liam O'ReillydefinitionS :: String
269c98e2ccf268d3d5d19d46d3d242fad726b882Liam O'ReillydefinitionS = "definition"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederinstanceS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederinstanceS = "instance"
269c98e2ccf268d3d5d19d46d3d242fad726b882Liam O'ReillyinstantiationS :: String
269c98e2ccf268d3d5d19d46d3d242fad726b882Liam O'ReillyinstantiationS = "instantiation"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedertypedeclS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedertypedeclS = "typedecl"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedertypesS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedertypesS = "types"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederconstsS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederconstsS = "consts"
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaederstructureS :: String
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaederstructureS = "structure"
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaederconstdefsS :: String
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaederconstdefsS = "constdefs"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederdomainS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederdomainS = "domain"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederdatatypeS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederdatatypeS = "datatype"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederfixrecS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederfixrecS = "fixrec"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederprimrecS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederprimrecS = "primrec"
cbac0a99fd23a43b4e94d30e58ebf93a6af6caa0Christian MaederdeclareS :: String
cbac0a99fd23a43b4e94d30e58ebf93a6af6caa0Christian MaederdeclareS = "declare"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedersimpS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedersimpS = "simp"
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'ReillyapplyS :: String
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'ReillyapplyS = "apply"
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'ReillybackS :: String
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'ReillybackS = "back"
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'ReillydeferS :: String
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'ReillydeferS = "defer"
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'ReillypreferS :: String
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'ReillypreferS = "prefer"
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'ReillydoneS :: String
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'ReillydoneS = "done"
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'ReillysorryS :: String
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'ReillysorryS = "sorry"
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'ReillyautoS :: String
fdd2ea0556081ab3fdca6cd8846c4f1eee74fd3aLiam O'ReillyautoS = "auto"
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'ReillyinductS :: String
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'ReillyinductS = "induct"
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'ReillycaseTacS :: String
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'ReillycaseTacS = "case_tac"
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'ReillyinsertS :: String
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'ReillyinsertS = "insert"
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'ReillysubgoalTacS :: String
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'ReillysubgoalTacS = "subgoal_tac"
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'ReillytypedefS :: String
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'ReillytypedefS = "typedef"
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'ReillypremiseOpenS :: String
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'ReillypremiseOpenS = "[|"
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'ReillypremiseCloseS :: String
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'ReillypremiseCloseS = "|]"
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'ReillymetaImplS :: String
72aaab1105e454ec9f49103874cd8006dc2a358cLiam O'ReillymetaImplS = "==>"
c4ba3e20a432419afff01558e425e00be42871d8Christian MaederusingS :: String
c4ba3e20a432419afff01558e425e00be42871d8Christian MaederusingS = "using"
16ae470521210b4f13feaa15e6de1b343a8e4e7aLiam O'ReillywhereS :: String
16ae470521210b4f13feaa15e6de1b343a8e4e7aLiam O'ReillywhereS = "where"
c4ba3e20a432419afff01558e425e00be42871d8Christian MaederdotDot :: String
16ae470521210b4f13feaa15e6de1b343a8e4e7aLiam O'ReillybarS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian Maedermarkups :: [String]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder [ "--", "chapter" , "section", "subsection", "subsubsection", "text"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "text_raw", "sect", "subsect", "subsubsect", "txt", "txt_raw"]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | toplevel keys that are currently ignored
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederignoredKeys :: [String]
afbcbe836333fac8c832afa778caa10f4b53b3e9Christian Maeder [ domainS, oopsS, refuteS, fixrecS, primrecS, declareS, usingS
afbcbe836333fac8c832afa778caa10f4b53b3e9Christian Maeder , dotDot, typedefS
7e6edfa96b1fd1b4fca1e9dcd336a8328f50b882Liam O'Reilly , "open", "sorry", "done", "by", "proof", "apply", "qed"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "classrel", "defaultsort", "nonterminls", "arities"
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder , "syntax", "no_syntax", "translations"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "global", "local", "hide", "use", "setup", "method_setup"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "ML_command", "ML_setup", "oracle"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "fix", "assume", "presume", "def", "note", "then", "from", "with"
c4ba3e20a432419afff01558e425e00be42871d8Christian Maeder , "have", "show", "hence", "thus", "shows", "."
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder-- , "rule", "iprover","OF", "of", "where", "assumption", "this", "-"
cbac0a99fd23a43b4e94d30e58ebf93a6af6caa0Christian Maeder , "let", "is", "next", "apply_end", "defer", "prefer", "back"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "pr", "thm", "prf", "term", "prop", "typ", "full_prf"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "undo", "redo", "kill", "thms_containing", "thms_deps"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini , "cd", "pwd", "use_thy", "use_thy_only", "update_thy"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini , "update_thy_only"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "display_drafts", "in", "locale" -- "intro_classes"
a81140cdef15cb5de8256e310eae035f98a054bfChristian Maeder , "fixes", "constrains" -- "assumes"
a81140cdef15cb5de8256e310eae035f98a054bfChristian Maeder , "defines", "notes", "includes"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "interpretation", "interpret", "obtain", "also", "finally"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "moreover", "ultimately" -- "trans", "sym", "symmetric"
afbcbe836333fac8c832afa778caa10f4b53b3e9Christian Maeder , "case", "judgment", "morphisms", "record", "rep_datatype"
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian Maeder , "recdef", "recdef_tc", "specification", "ax_specification"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "inductive", "coinductive", "inductive_cases", "codatatype"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "code_module", "code_library", "consts_code", "types_code" ]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ++ map (++ "_translation")
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini [ "parse_ast", "parse", "print", "print_ast", "typed_print"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ++ map ("print_" ++)
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini [ "commands", "syntax", "methods", "attributes", "theorems"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "facts", "binds", "drafts", "locale", "locales", "interps"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "trans_rules", "simp_set", "claset", "cases", "induct_rules" ]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | toplevel keywords currently recognized by IsaParse
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederusedTopKeys :: [String]
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederusedTopKeys = markups ++
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder [ importsS, usesS, beginS, contextS, mlS, axiomsS, defsS, constsS
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini , constdefsS, lemmasS, theoremsS, lemmaS, corollaryS, theoremS
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , classesS, axclassS, instanceS, typesS, typedeclS, endS ]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | all Isabelle keywords
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederisaKeywords :: [String]
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaederisaKeywords = "::" : andS : theoryS : map (: []) ":=<|"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ++ usedTopKeys ++ ignoredKeys
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von SchroedermkVName :: String -> VName
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von SchroedermkVName s = case Map.lookup s vMap of
1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder Nothing -> VName { new = s, altSyn = Nothing }