IsaSign.hs revision 8b4c68db8b465107cabef8b9cd5b6bc216e1b156
43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder {- list of datatype definitions
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian Maeder each of these consists of a list of (mututally recursive) datatypes
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder each datatype consists of its name (Typ) and a list of constructors
25cc5fbba63f84b47e389af749f55abbbde71c8cChristian Maeder each constructor consists of its name (String) and list of argument types
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederModule : $Header$
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCopyright : (c) University of Cambridge, Cambridge, England
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder adaption (c) Till Mossakowski, Uni Bremen 2002-2004
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian MaederMaintainer : hets@tzi.de
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian MaederStability : provisional
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederPortability : portable
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder Data structures for Isabelle sigantures and theories.
68d10d143f29fcff3c637ba24f90e983995ceae6Christian Maeder Adapted from Isabelle.
a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maederimport qualified Common.Lib.Map as Map
01e383014b555bbcf639c0ca60c5810b3eff83c0Christian Maeder---------------- from src/Pure/Syntax/syntax.ML -------------------
9dac90ec2be2a72e03893095461960d483fe2fc2Christian Maedertype Syntax = () -- leave this for later
ce8b15da31cd181b7e90593cbbca98f47eda29d6Till Mossakowski-------------------- from src/Pure/term.ML ------------------------
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder{-Indexnames can be quickly renamed by adding an offset to the integer part,
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder for resolution.-}
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maedertype Indexname = (String,Int)
c0c2380bced8159ff0297ece14eba948bd236471Christian Maeder{- Types are classified by sorts. -}
8410667510a76409aca9bb24ff0eda0420088274Christian Maedertype Class = String;
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maedertype Sort = [Class]
8410667510a76409aca9bb24ff0eda0420088274Christian Maeder{- The sorts attached to TFrees and TVars specify the sort of that variable -}
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettichdata Typ = Type (String,[Typ]) -- type constructor, with name and args
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder | TFree (String, Sort) -- free type variable ('a)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder | TVar (Indexname, Sort) -- type unknown (?'a)
4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian Maeder deriving (Eq, Ord)
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederdummyT = Type("dummy",[])
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian MaederboolType :: Typ
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian MaederboolType = Type("bool",[])
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedermkOptionType :: Typ -> Typ
e593b89bfd4952698dc37feced21cefe869d87a2Christian MaedermkOptionType t = Type("option",[t])
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaedermkProductType :: Typ -> Typ -> Typ
7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian MaedermkProductType t1 t2 = Type ("*",[t1,t2])
1aee4aaddde105264c1faf394d88e302c05094ffChristian MaedermkTypeAppl :: Typ -> Typ -> Typ
f041c9a6bda23de33a38490e35b831ae18d96b45Christian MaedermkTypeAppl t1 t2 = Type ("typeAppl",[t1,t2])
1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeders --> t = Type("fun",[s,t])
c3053d57f642ca507cdf79512e604437c4546cb9Christian Maeder{-handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)-}
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder(--->) = flip $ foldr (-->)
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder{-Terms. Bound variables are indicated by depth number.
dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder Free variables, (scheme) variables and constants have names.
2c9df69accd8924e7cef3bf8f686626958499c7aChristian Maeder An term is "closed" if every bound variable of level "lev"
c2fcc35abb03cf0b4ca4b050efeb10827f38c322Christian Maeder is enclosed by at least "lev" abstractions.
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder It is possible to create meaningless terms containing loose bound vars
356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder or type mismatches. But such terms are not allowed in rules. -}
0206ab93ef846e4e0885996d052b9b73b9dc66b0Christian Maeder Const (String, Typ) -- constants
f13d1e86e58da53680e78043e8df182eed867efbChristian Maeder | Free (String, Typ) -- free variables
c2a4d8ae266aa37cc922eba97077520229a19902Christian Maeder -- | Var (Indexname, Typ)
79e80c4b3f0ebb337d84415a50f29ccfc793e68bChristian Maeder -- | Bound Int
79e80c4b3f0ebb337d84415a50f29ccfc793e68bChristian Maeder | Abs (Term, Typ, Term) -- lambda abstraction
79e80c4b3f0ebb337d84415a50f29ccfc793e68bChristian Maeder | App Term Term -- application
79e80c4b3f0ebb337d84415a50f29ccfc793e68bChristian Maeder | Case (Term, [(Term, Term)]) -- case
757e6c79ec40491d45dc72c82b5eb59a386634b0Jian Chun Wang deriving (Eq, Ord)
ecf76bc89d9a2ecd7ac7310d30654b9a79d97d62Klaus Luettichdata Sentence = Sentence { senTerm :: Term
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettichinstance Eq Sentence where
36f63902db2b3463faa9f59912ad106e2d5aaa24Klaus Luettich s1 == s2 = senTerm s1 == senTerm s2
a6db617ca58eb6a0587b6366e913107dfecb71b5Heng Jianginstance Ord Sentence where
8cacad2a09782249243b80985f28e9387019fe40Christian Maeder compare s1 s2 = compare (senTerm s1) (senTerm s2)
363939beade943a02b31004cea09dec34fa8a6d9Christian Maeder-------------------- from src/Pure/sorts.ML ------------------------
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich{-- type classes and sorts --}
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder Classes denote (possibly empty) collections of types that are
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder partially ordered by class inclusion. They are represented
d3ae0072823e2ef0d41d4431fcc768e66489c20eChristian Maeder symbolically by strings.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder Sorts are intersections of finitely many classes. They are
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder represented by lists of classes. Normal forms of sorts are sorted
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder lists of minimal classes (wrt. current class inclusion).
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder (already defined in Pure/term.ML)
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder{- sort signature information -}
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder table representing the proper subclass relation; entries (c, cs)
9e748851c150e1022fb952bab3315e869aaf0214Christian Maeder represent the superclasses cs of c;
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder table of association lists of all type arities; (t, ars) means
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder that type constructor t has the arities ars; an element (c, Ss) of
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian Maeder ars represents the arity t::(Ss)c;
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maedertype Classrel = Map.Map String [Class]
c0c2380bced8159ff0297ece14eba948bd236471Christian Maedertype Arities = Map.Map String [(Class, [Sort])]
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder-------------------- from src/Pure/type.ML ------------------------
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederdata TypeSig =
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder classes:: [Class],
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder classrel:: Classrel,
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder defaultSort:: Sort,
03a6d8f77f588dc5d3dd6653797fa2362efa1751Christian Maeder tycons:: Map.Map String Int, -- type constructor names, with arities
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder log_types:: [String],
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder univ_witness:: Maybe (Typ, Sort),
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder abbrs:: Map.Map String ([String],Typ),
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder arities:: Arities }
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder deriving (Eq)
2d130d212db7208777ca896a7ecad619a8944971Christian MaederemptyTypeSig :: TypeSig
2d130d212db7208777ca896a7ecad619a8944971Christian MaederemptyTypeSig = TySg {
a5e5b8c3e5c11177e5034ef2423813a5d28979edChristian Maeder classes = [],
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder defaultSort = [],
2d130d212db7208777ca896a7ecad619a8944971Christian Maeder log_types = [],
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder univ_witness = Nothing,
6ff7a91875597d6e4dfaa68c79187d01473e8341Christian Maeder-------------------- from src/Pure/sign.ML ------------------------
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maederdata Sign = Sign { baseSig :: String, -- like Pure, HOL, Main etc.
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder tsig :: TypeSig,
4017ebc0f692820736d796af3110c3b3018c108aChristian Maeder constTab :: Map.Map String Typ,
a9b59eb2ce961014974276cdae0e9df4419bd212Christian Maeder dataTypeTab :: DataTypeTab,
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder -- needs HOLCF, extend this with domains
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder syn :: Syntax
6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder deriving (Eq)
a3c6d8e0670bf2aa71bc8e2a3b1f45d56dd65e4cChristian Maeder {- list of datatype definitions
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder each of these consists of a list of (mututally recursive) datatypes
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder each datatype consists of its name (Typ) and a list of constructors
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder each constructor consists of its name (String) and list of argument types
363939beade943a02b31004cea09dec34fa8a6d9Christian Maedertype DataTypeTab = [DataTypeTabEntry]
363939beade943a02b31004cea09dec34fa8a6d9Christian Maedertype DataTypeTabEntry = [(Typ,[DataTypeAlt])]
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maedertype DataTypeAlt = (String,[Typ])
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederemptySign :: Sign
ca074a78b8dcccbb8c419586787882f98d0c6163Christian MaederemptySign = Sign { baseSig = "Pure",
ca074a78b8dcccbb8c419586787882f98d0c6163Christian Maeder tsig = emptyTypeSig,
b568982efd0997d877286faa592d81b03c8c67b8Christian Maeder dataTypeTab = [],