IsaConsts.hs revision a2e8cca8a8217b158b0b7a760e8234c03186456d
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 = "Cons"
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaedercompS :: String
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinicompS = "comp"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | lower case pair
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinipairC :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinipairC = "pair"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- * some stuff for Isabelle
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinipcpoS :: String
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillypcpoS = "pcpo"
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillyprodS, sProdS, funS, cFunS, lFunS, sSumS, lProdS, lSumS :: TName
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'ReillyprodS = "*" -- this is printed as it is!
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'ReillylProdS = "lprod" -- "***"
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillylSumS = "either"
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly-- * some stuff for HasCASL
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillyaptS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniappS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederpAppS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederpAppS = "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
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinipcpo :: IsaClass
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinipcpo = IsaClass pcpoS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniisaTerm :: IsaClass
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniisaTerm = IsaClass "type"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- * predefined SORTS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniholType :: Sort
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniholType = [isaTerm]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisortT :: Continuity -> Sort
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinisortT a = case a of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini NotCont -> holType
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont _ -> dom
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini--------------------- POLY TYPES ----------------------------------------
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederlistT :: Continuity -> Typ -> Typ
99c923311eab71a85f1dcc4785d349609c828da4Christian 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
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicharT a = Type "charT" (sortT a) []
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo TorriniboolT :: Continuity -> Typ
d4e8d3a0ddb1a63754edc3571b6a3a54a7b62d04Paolo TorriniboolT a = case a of
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder IsCont _ -> Type "lBool" (sortT a) []
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder NotCont -> Type "bool" (sortT a) []
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniintT :: Continuity -> Typ
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaederintT a = Type "intT" (sortT a) []
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniprodT :: Continuity -> Typ -> Typ -> Typ
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniprodT a t1 t2 = case a of
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini IsCont _ -> mkContProduct t1 t2
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini NotCont -> prodType t1 t2
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder-- **** predefinded HOL TYPES ----------------------------------
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrininoTypeT :: Typ
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrininoTypeT = Type "dummy" holType []
c730c28919b53f940ed319ebb42780244c528e29Paolo TorrininoType :: DTyp
c730c28919b53f940ed319ebb42780244c528e29Paolo TorrininoType = Hide noTypeT NA Nothing
c730c28919b53f940ed319ebb42780244c528e29Paolo TorrininoTypeC :: DTyp
c730c28919b53f940ed319ebb42780244c528e29Paolo TorrininoTypeC = Hide noTypeT TCon Nothing
c730c28919b53f940ed319ebb42780244c528e29Paolo TorrinihideNN :: Typ -> DTyp
c730c28919b53f940ed319ebb42780244c528e29Paolo TorrinihideNN t = Hide t NA Nothing
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinihideCN :: Typ -> DTyp
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinihideCN t = Hide t TCon Nothing
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinidispNN :: Typ -> DTyp
c730c28919b53f940ed319ebb42780244c528e29Paolo TorrinidispNN t = Disp t NA Nothing
c730c28919b53f940ed319ebb42780244c528e29Paolo TorrinidispMN :: Typ -> DTyp
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinidispMN t = Disp t TMet Nothing
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniboolType :: Typ
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniboolType = boolT NotCont
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkListType :: Typ -> Typ
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinimkListType t = Type "list" holType [t]
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinimkOptionType :: Typ -> Typ
c730c28919b53f940ed319ebb42780244c528e29Paolo TorrinimkOptionType t = Type "option" holType [t]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniprodType :: Typ -> Typ -> Typ
c730c28919b53f940ed319ebb42780244c528e29Paolo TorriniprodType t1 t2 = Type prodS holType [t1,t2]
c730c28919b53f940ed319ebb42780244c528e29Paolo TorrinimkFunType :: Typ -> Typ -> Typ
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkFunType s t = Type funS holType [s,t] -- was "-->" before
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder{-handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)-}
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkCurryFunType :: [Typ] -> Typ -> Typ
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkCurryFunType = flip $ foldr mkFunType -- was "--->" before
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- **** predefinded HOLCF TYPES --------------------------------------
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinivoidDom :: Typ
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinivoidDom = Type "void" dom []
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini{- should this be included (as primitive)? -}
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniflatDom :: Typ
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniflatDom = Type "flat" dom []
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinitLift :: Typ -> Typ
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitLift t = Type "lift" dom [t]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini{- sort is ok? -}
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkContFun :: Typ -> Typ -> Typ
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkContFun t1 t2 = Type lFunS dom [t1,t2]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkStrictProduct :: Typ -> Typ -> Typ
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkStrictProduct t1 t2 = Type sProdS dom [t1,t2]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkContProduct :: Typ -> Typ -> Typ
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkContProduct t1 t2 = Type lProdS dom [t1,t2]
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder{-handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)-}
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkCurryContFun :: [Typ] -> Typ -> Typ
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkCurryContFun = flip $ foldr mkContFun -- was "--->" before
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkStrictSum :: Typ -> Typ -> Typ
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkStrictSum t1 t2 = Type lSumS dom [t1,t2]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- **** TERM FORMATION -------------------------------------------
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermaxPrio :: Int
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimaxPrio = 1000
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinilowPrio :: Int
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederisaEqPrio :: Int
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederisaEqPrio = 2 -- left assoc
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- | construct constants and variables
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkConstVD :: String -> Typ -> Term
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkConstVD s t = Const (mkVName s) $ hideNN t
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinimkConstV :: String -> DTyp -> Term
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkConstV s t = Const (mkVName s) t
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkConstD :: VName -> Typ -> Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinimkConstD s t = Const s $ hideNN t
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkConst :: VName -> DTyp -> Term
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkConst s t = Const s t
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkFree :: String -> Term
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaedermkFree s = Free $ mkVName s
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- | construct a constant with no type
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinicon :: VName -> Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinicon s = mkConst s noType
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederconC :: VName -> Term
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederconC s = mkConst s noTypeC
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederconDouble :: String -> Term
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederconDouble = con . mkVName
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederconDoubleC :: String -> Term
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederconDoubleC = conC . mkVName
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- | apply VName operator to two term
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinibinVNameAppl :: VName -> Term -> Term -> Term
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederbinVNameAppl v t1 t2 = termAppl (termAppl (con v) t1) t2
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- * TERM CONSTRUCTORS
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- | binary junctors
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinibinConj, binDisj, binImpl, binEqv, binEq :: Term -> Term -> Term
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederbinConj = binVNameAppl conjV
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederbinDisj = binVNameAppl disjV
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinibinImpl = binVNameAppl implV
120c9bff9059626735fc12b0399dcc9e5a62c345Christian MaederbinEq = binVNameAppl eqV
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederbinEqv = binEq
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder-- | HOL function application
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaedertermAppl :: Term -> Term -> Term
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedertermAppl t1 t2 = App t1 t2 NotCont
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder-- **** Poly terms for HOL-HOLCF ----------------------------------
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaederandPT :: Continuity -> Term
74e146c7cfad97817d7e065dcd937cada89b257dChristian MaederandPT a = case a of
74e146c7cfad97817d7e065dcd937cada89b257dChristian Maeder NotCont -> con conjV
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont _ -> conDouble "andH"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniorPT :: Continuity -> Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniorPT a = case a of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini NotCont -> con disjV
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont _ -> conDouble "orH"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrininotPT :: Continuity -> Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrininotPT a = case a of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini NotCont -> con notV
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont _ -> conDouble "notH"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinibottomPT :: Continuity -> Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinibottomPT a = conDouble $ case a of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini NotCont -> "arbitrary"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder IsCont _ -> "UU"
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaedernilPT :: Continuity -> Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrininilPT a = conDouble $ case a of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini NotCont -> "[]"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont _ -> "lNil"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederconsPT :: Continuity -> Term
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederconsPT a = con $ case a of
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian Maeder NotCont -> consV
cd7372fc7e6e43c389619f63daa6eb872d9d5b16Christian Maeder IsCont _ -> lconsV
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitruePT :: Continuity -> Term
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedertruePT a = conDouble $ case a of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini NotCont -> "True"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont _ -> "TRUE"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederfalsePT :: Continuity -> Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinifalsePT a = conDouble $ case a of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini NotCont -> "False"
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly IsCont _ -> "FALSE"
33bdce26495121cdbce30331ef90a1969126a840Liam O'ReillyunitPT :: Continuity -> Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniunitPT a = case a of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini NotCont -> conDouble "()"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont _ -> termAppl (conDouble "Def") (conDouble "()")
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinifstPT :: Continuity -> Term
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'ReillyfstPT a = case a of
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'Reilly NotCont -> conDouble "fst"
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly IsCont True -> conDouble "llfst"
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly IsCont False -> conDoubleC "lfst"
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillysndPT :: Continuity -> Term
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'ReillysndPT a = case a of
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder NotCont -> conDouble "snd"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont True -> conDouble "llsnd"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini IsCont False -> conDoubleC "lsnd"
5e4812721f9026ae4ae54381a5fdeb163489087dChristian MaederpairPT :: Continuity -> Term
5e4812721f9026ae4ae54381a5fdeb163489087dChristian MaederpairPT a = case a of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini NotCont -> conDouble "pair"
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder IsCont _ -> conDouble "llpair"
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder-- **** TERMS ---------------------------------------------------
5e4812721f9026ae4ae54381a5fdeb163489087dChristian Maeder-- * Boolean constants
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinitrue = mkConstVD cTrue boolType
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrinifalse = mkConstVD cFalse boolType
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maeder-- * UNTYPED terms
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | defOp constant
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaederdefOp = conDouble defOpS
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | Not constant
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrininotOp = con notV
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | some constant
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniconSome :: Term
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniconSome = conDouble someS
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaederliftString :: Term
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniliftString = conDouble "liftList"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinilpairTerm :: Term
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinilpairTerm = conDoubleC "lpair"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- **** VNAMES -------------------------------------------------
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- | Not VName
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrininotV = VName cNot $ Just $ AltSyntax "~/ _" [40] 40
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini-- * VNames of binary operators
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniconjV :: VName
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniconjV = VName conj $ Just $ AltSyntax "(_ &/ _)" [36, 35] 35
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinidisjV :: VName
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinidisjV = VName disj $ Just $ AltSyntax "(_ |/ _)" [31, 30] 30
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniimplV :: VName
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniimplV = VName impl $ Just $ AltSyntax "(_ -->/ _)" [26, 25] 25
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinieqV = VName eq $ Just $ AltSyntax "(_ =/ _)" [50, 51] 50
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniplusV :: VName
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniplusV = VName plusS $ Just $ AltSyntax "(_ +/ _)" [65, 66] 65
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniminusV :: VName
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniminusV = VName minusS $ Just $ AltSyntax "(_ -/ _)" [65, 66] 65
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinidivV = VName divS $ Just $ AltSyntax "(_ div/ _)" [70, 71] 70
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinimodV = VName modS $ Just $ AltSyntax "(_ mod/ _)" [70, 71] 70
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitimesV :: VName
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitimesV = VName timesS $ Just $ AltSyntax "(_ */ _)" [70, 71] 70
ce31795240d8fb340bc984b8b35147c955e29afaChristian MaederconsV :: VName
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniconsV = VName consS $ Just $ AltSyntax "(_ #/ _)" [66, 65] 65
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinilconsV :: VName
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinilconsV = VName "llCons" $ Just $ AltSyntax "(_ ###/ _)" [66, 65] 65
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaedercompV :: VName
c730c28919b53f940ed319ebb42780244c528e29Paolo TorrinicompV = VName compS $ Just $ AltSyntax "(_ o/ _)" [55, 56] 55
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- **** keywords in theory files from the Isar Reference Manual 2005
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniendS :: String
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaederheaderS :: String
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniheaderS = "header"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinitheoryS :: String
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinitheoryS = "theory"
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaederimportsS :: String
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniimportsS = "imports"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniusesS :: String
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniusesS = "uses"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinibeginS :: String
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinibeginS = "begin"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinicontextS :: String
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinicontextS = "context"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniaxiomsS :: String
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorriniaxiomsS = "axioms"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinidefsS :: String
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinidefsS = "defs"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinioopsS :: String
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo TorrinioopsS = "oops"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniandS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinilemmasS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinilemmasS = "lemmas"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinilemmaS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinilemmaS = "lemma"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedercorollaryS :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedercorollaryS = "corollary"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederrefuteS :: String
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederrefuteS = "refute"
4ef05f4edeb290beb89845f57156baa5298af7c4Christian MaedertheoremsS :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedertheoremsS = "theorems"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitheoremS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitheoremS = "theorem"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniaxclassS :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederaxclassS = "axclass"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniclassesS :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederclassesS = "classes"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniinstanceS :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederinstanceS = "instance"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedertypedeclS :: String
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitypedeclS = "typedecl"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinitypesS :: String
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaedertypesS = "types"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederconstsS :: String
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederconstsS = "consts"
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederstructureS :: String
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederstructureS = "structure"
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederconstdefsS :: String
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederconstdefsS = "constdefs"
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederdomainS :: String
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederdomainS = "domain"
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederdatatypeS :: String
4ef05f4edeb290beb89845f57156baa5298af7c4Christian MaederdatatypeS = "datatype"
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederfixrecS :: String
4ef05f4edeb290beb89845f57156baa5298af7c4Christian MaederfixrecS = "fixrec"
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian MaederprimrecS :: String
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo TorriniprimrecS = "primrec"
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo TorrinideclareS :: String
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo TorrinideclareS = "declare"
65e28321f4dbba7bcc6cfe5c900e59f705ebdd12Paolo TorrinisimpS :: String
4ef05f4edeb290beb89845f57156baa5298af7c4Christian MaedersimpS = "simp"
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maedermarkups :: [String]
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder [ "--", "chapter" , "section", "subsection", "subsubsection", "text"
9e5d738f1fb98e67d8b24c1db27a41a0c5dff8edChristian Maeder , "text_raw", "sect", "subsect", "subsubsect", "txt", "txt_raw"]
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini-- | toplevel keys that are currently ignored
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniignoredKeys :: [String]
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder [ domainS, oopsS, refuteS, fixrecS, primrecS, declareS
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder , "sorry", "done", "by", "proof", "apply", "qed"
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly , "classrel", "defaultsort", "nonterminls", "arities"
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly , "syntax", "no_syntax", "translations"
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder , "global", "local", "hide", "use", "setup", "method_setup"
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'Reilly , "ML_command", "ML_setup", "oracle"
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'Reilly , "fix", "assume", "presume", "def", "note", "then", "from", "with"
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'Reilly , "using", "have", "show", "hence", "thus", "shows", ".", ".."
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- , "rule", "iprover","OF", "of", "where", "assumption", "this", "-"
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly , "let", "is", "next", "apply_end", "defer", "prefer", "back"
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly , "pr", "thm", "prf", "term", "prop", "typ", "full_prf"
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly , "undo", "redo", "kill", "thms_containing", "thms_deps"
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly , "cd", "pwd", "use_thy", "use_thy_only", "update_thy", "update_thy_only"
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly , "display_drafts", "in", "locale" -- "intro_classes"
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly , "fixes", "constrains", "assumes", "defines", "notes", "includes"
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly , "interpretation", "interpret", "obtain", "also", "finally"
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly , "moreover", "ultimately" -- "trans", "sym", "symmetric"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , "case", "judgment", "typedef", "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")
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder [ "parse_ast", "parse", "print", "print_ast", "typed_print", "token" ]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ++ map ("print_" ++)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder [ "commands", "syntax", "methods", "attributes", "theorems", "tcset"
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
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , constdefsS, lemmasS, theoremsS, lemmaS, corollaryS, theoremS, datatypeS
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder , classesS, axclassS, instanceS, typesS, typedeclS, endS ]
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- | all Isabelle keywords
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederisaKeywords :: [String]
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederisaKeywords = "::" : andS : theoryS : map (:[]) ":=<|"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder ++ usedTopKeys ++ ignoredKeys