IsaConsts.hs revision afbcbe836333fac8c832afa778caa10f4b53b3e9
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederModule : $Header$
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederDescription : constants for Isabelle terms
cd7372fc7e6e43c389619f63daa6eb872d9d5b16Christian MaederCopyright : (c) Sonja Groening, Christian Maeder, Uni Bremen 2004-2006
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.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
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder-- | a topological sort with a @uses@ predicate
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaederquickSort :: (a -> a -> Bool) -> [a] -> [a]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniquickSort f ls = case ls of
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder a : as -> let (xs, ys) = partition (f a) as in
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder quickSort f xs ++ a : quickSort f ys
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- **** STRINGS ------------------------------------------------
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- * boolean constants
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 ###"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicompS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicompS = "comp"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | lower case pair
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinipairC :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinipairC = "pair"
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"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- **** CLASSES & SORTS ---------------------------------------
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- * Predifined 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
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini--------------------- POLY TYPES --------------------------------------
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinilistT :: Continuity -> Typ -> Typ
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaederlistT a t = case a of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont _ -> Type "llist" (sortT a) [t]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini NotCont -> Type "list" (sortT a) [t]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicharT :: Continuity -> Typ
c730c28919b53f940ed319ebb42780244c528e29Paolo TorrinicharT a = case a of
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini IsCont _ -> Type "charT" (sortT a) []
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini NotCont -> Type "char" (sortT a) []
c730c28919b53f940ed319ebb42780244c528e29Paolo TorriniratT :: Continuity -> Typ
c730c28919b53f940ed319ebb42780244c528e29Paolo TorriniratT a = case a of
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini IsCont _ -> Type "ratT" (sortT a) []
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini NotCont -> Type "rat" (sortT a) []
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinifracT :: Continuity -> Typ
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinifracT a = Type "fracT" (sortT a) []
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniintegerT :: Continuity -> Typ
c730c28919b53f940ed319ebb42780244c528e29Paolo TorriniintegerT a = case a of
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini IsCont _ -> Type "integerT" (sortT a) []
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini NotCont -> Type "int" (sortT a) []
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniboolT :: Continuity -> Typ
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniboolT a = case a of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont _ -> Type "lBool" (sortT a) []
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini NotCont -> Type "bool" (sortT a) []
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniorderingT :: Continuity -> Typ
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniorderingT a = case a of
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini IsCont _ -> Type "lOrdering" (sortT a) []
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini NotCont -> Type "sOrdering" (sortT a) []
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniintT :: Continuity -> Typ
c730c28919b53f940ed319ebb42780244c528e29Paolo TorriniintT a = case a of
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini IsCont _ -> Type "intT" (sortT a) []
c730c28919b53f940ed319ebb42780244c528e29Paolo Torrini NotCont -> Type "int" (sortT a) []
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniprodT :: Continuity -> Typ -> Typ -> Typ
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaederprodT a t1 t2 = case a of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont _ -> mkContProduct t1 t2
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini NotCont -> prodType t1 t2
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinifunT :: Continuity -> Typ -> Typ -> Typ
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinifunT c a b = case c of
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini IsCont _ -> mkContFun a b
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini NotCont -> mkFunType a b
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinicurryFunT :: Continuity -> [Typ] -> Typ -> Typ
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinicurryFunT c ls x = case c of
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini IsCont _ -> mkCurryContFun ls x
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini NotCont -> mkCurryFunType ls x
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- **** predefinded HOL TYPES ----------------------------------
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrininoTypeT :: Typ
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrininoTypeT = Type "dummy" holType []
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
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkListType t = Type "list" holType [t]
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
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini{-handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)-}
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkCurryFunType :: [Typ] -> Typ -> Typ
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkCurryFunType = flip $ foldr mkFunType -- was "--->" before
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- **** predefinded HOLCF TYPES --------------------------------------
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedervoidDom :: Typ
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedervoidDom = Type "void" dom []
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder{- should this be included (as primitive)? -}
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederflatDom :: Typ
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederflatDom = Type "flat" dom []
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitLift :: Typ -> Typ
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitLift t = Type "lift" dom [t]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder{- sort is ok? -}
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkContFun :: Typ -> Typ -> Typ
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkContFun t1 t2 = Type lFunS dom [t1,t2]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkStrictProduct :: Typ -> Typ -> Typ
62dd3cd58cda003c32ac69ff12dc82b0a6f5d9d3Christian MaedermkStrictProduct t1 t2 = Type sProdS dom [t1,t2]
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkContProduct :: Typ -> Typ -> Typ
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkContProduct t1 t2 = Type lProdS dom [t1,t2]
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini{-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
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkStrictSum t1 t2 = Type lSumS dom [t1,t2]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- **** TERM FORMATION -------------------------------------------
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
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkConstV s t = Const (mkVName s) t
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkConstD :: VName -> Typ -> Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkConstD s t = Const s $ hideNN t
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkConst :: VName -> DTyp -> Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkConst s t = Const s t
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkFree :: String -> Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkFree s = Free $ mkVName s
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
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinibinVNameAppl v t1 t2 = termAppl (termAppl (con v) t1) t2
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- * TERM CONSTRUCTORS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | binary junctors
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinibinConj, binDisj, binImpl, binEqv, binEq :: Term -> Term -> Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinibinConj = binVNameAppl conjV
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinibinDisj = binVNameAppl disjV
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinibinImpl = binVNameAppl implV
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinibinEq = binVNameAppl eqV
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinibinEqv = binEq
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | HOL function application
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitermAppl :: Term -> Term -> Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitermAppl t1 t2 = App t1 t2 NotCont
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- **** Poly 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
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder NotCont -> "arbitrary"
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
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian 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"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini 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"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont False -> conDoubleC "lsnd"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinipairPT :: Continuity -> Term
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaederpairPT a = case a of
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini NotCont -> conDoubleC "pair"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini IsCont True -> conDouble "llpair"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini 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
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinieqTPT t = mkConstVD "eqH" t
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinineqTPT :: Typ -> Term
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinineqTPT t = mkConstVD "neqH" t
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- **** TERMS ---------------------------------------------------
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"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- **** VNAMES -------------------------------------------------
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | Not VName
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrininotV = VName cNot $ Just $ AltSyntax "~/ _" [40] 40
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- * VNames of binary operators
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
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
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaedercompV :: VName
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaedercompV = VName compS $ Just $ AltSyntax "(_ o/ _)" [55, 56] 55
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- **** 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"
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederinstanceS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederinstanceS = "instance"
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"
c4ba3e20a432419afff01558e425e00be42871d8Christian MaederdotDot :: 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
e96fb97935ac710a295b04d60b8ac90ef8364079Christian Maeder , "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", "."
99c923311eab71a85f1dcc4785d349609c828da4Christian 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"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , "fixes", "constrains", "assumes", "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"
99c923311eab71a85f1dcc4785d349609c828da4Christian 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]
ac53ffcb7dda01eb1faca2c4ef726b06bf7076fbChristian MaederisaKeywords = "::" : andS : theoryS : map (:[]) ":=<|"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ++ usedTopKeys ++ ignoredKeys