IsaSign.hs revision fe19deda2fe2570f9d599e58fdbc991248d08325
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$
81d182b21020b815887e9057959228546cf61b6bChristian MaederCopyright : (c) University of Cambridge, Cambridge, England
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maeder adaption (c) Till Mossakowski, Uni Bremen 2002-2004
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : hets@tzi.de
ce2eda9624349a4c191dca61cb478b039ab00998Christian MaederStability : provisional
410ff490af511ffa09b52e4de631d36a154b9730Christian MaederPortability : portable
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder Data structures for Isabelle sigantures and theories.
ce2eda9624349a4c191dca61cb478b039ab00998Christian Maeder Adapted from Isabelle.
b1719ef0353b9eb5a00dec8e5119a99eaad718e0Christian Maederimport qualified Common.Lib.Map as Map
0bc67ab104bfc3aa3233035b1c35bb7fa11cd9e3Christian Maederbracketize :: Bool -> String -> String
b1719ef0353b9eb5a00dec8e5119a99eaad718e0Christian Maederbracketize b s = if b then "("++s++")" else s
ce2eda9624349a4c191dca61cb478b039ab00998Christian Maeder---------------- from src/Pure/Syntax/syntax.ML -------------------
ce2eda9624349a4c191dca61cb478b039ab00998Christian Maedertype Syntax = () -- leave this for later
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder-------------------- from src/Pure/term.ML ------------------------
950e053ba55ac9c7d9c26a1ab48bd00202b29511Christian Maeder{-Indexnames can be quickly renamed by adding an offset to the integer part,
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder for resolution.-}
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maedertype Indexname = (String,Int)
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder{- Types are classified by sorts. -}
ad270004874ce1d0697fb30d7309f180553bb315Christian Maedertype Class = String;
ad270004874ce1d0697fb30d7309f180553bb315Christian Maedertype Sort = [Class]
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder{- The sorts attached to TFrees and TVars specify the sort of that variable -}
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederdata Typ = Type (String,[Typ])
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder | TFree (String, Sort)
c200224a127278d54634ca4a5079591cb989aaf3Christian Maeder -- | TVar (Indexname, Sort)
c200224a127278d54634ca4a5079591cb989aaf3Christian Maeder deriving (Eq, Ord)
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maederinstance Show Typ where
950e053ba55ac9c7d9c26a1ab48bd00202b29511Christian Maeder show = showTyp 1000
abae801b829b32e32fff31d106245cf3b8c0a21fChristian MaedershowTyp pri (Type ("fun",[s,t])) =
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder bracketize (pri<=10) (showTyp 10 s ++ "=>" ++ showTyp 11 t)
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian MaedershowTyp pri (Type (t,args)) = "("++concat (map ((" "++).show) args)++")"++t
ce2eda9624349a4c191dca61cb478b039ab00998Christian MaedershowTyp pri (TFree (v,_)) = v
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian MaederdummyT = Type("dummy",[])
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskiboolType :: Typ
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskiboolType = Type("bool",[])
ce2eda9624349a4c191dca61cb478b039ab00998Christian Maeders --> t = Type("fun",[s,t])
ce2eda9624349a4c191dca61cb478b039ab00998Christian Maeder{-handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)-}
ce2eda9624349a4c191dca61cb478b039ab00998Christian Maeder(--->) = flip $ foldr (-->)
ce2eda9624349a4c191dca61cb478b039ab00998Christian Maeder{-Terms. Bound variables are indicated by depth number.
ce2eda9624349a4c191dca61cb478b039ab00998Christian Maeder Free variables, (scheme) variables and constants have names.
ce2eda9624349a4c191dca61cb478b039ab00998Christian Maeder An term is "closed" if every bound variable of level "lev"
3bffe0f10ad93403e36288a1a4a92d50356956b5Christian Maeder is enclosed by at least "lev" abstractions.
3bffe0f10ad93403e36288a1a4a92d50356956b5Christian Maeder It is possible to create meaningless terms containing loose bound vars
52c28508167eb774d9b7286d585c250078d65818Christian Maeder or type mismatches. But such terms are not allowed in rules. -}
3bffe0f10ad93403e36288a1a4a92d50356956b5Christian Maeder Const (String, Typ)
96edb3a8e970c02cc10a75d70b96a9165a4e1b91Christian Maeder | Free (String, Typ)
410ff490af511ffa09b52e4de631d36a154b9730Christian Maeder -- | Var (Indexname, Typ)
31400d19240b9a9ce78e7f8a495f8d4951a21e30Christian Maeder -- | Bound Int
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder | Abs (String, Typ, Term)
96edb3a8e970c02cc10a75d70b96a9165a4e1b91Christian Maeder | App Term Term
ce2eda9624349a4c191dca61cb478b039ab00998Christian Maeder deriving (Eq, Ord)
ce2eda9624349a4c191dca61cb478b039ab00998Christian Maederinstance Show Term where
31400d19240b9a9ce78e7f8a495f8d4951a21e30Christian Maeder show = showTerm 1000
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian MaedershowTerm :: Int -> Term -> String
410ff490af511ffa09b52e4de631d36a154b9730Christian MaedershowTerm pri (Const (c,_)) = c
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian MaedershowTerm pri (Free (v,_)) = v
410ff490af511ffa09b52e4de631d36a154b9730Christian MaedershowTerm pri (Abs (v,_,t)) = "%"++v++" . "++show t
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedershowTerm pri (Abs (v,_,t)) = "%"++v++" . "++show t
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedershowTerm pri (Const ("All",_) `App` Abs (v,_,t)) = "!"++v++" . "++show t
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian MaedershowTerm pri (Const ("Ex",_) `App` Abs (v,_,t)) = "?"++v++" . "++show t
dc4bfcb8a5092af158e8a5691c8de8d6bc8b8724Christian MaedershowTerm pri (Const ("Ex1",_) `App` Abs (v,_,t)) = "?!"++v++" . "++show t
e0dba81bd8957764e49d5f15b5e0ab1f9411aadfChristian MaedershowTerm pri (t1 `App` t2) =
8338fbf3cfb9cf981261d893286f070bd9fa17efChristian Maeder bracketize (pri<=10) (showTerm 11 t1 ++ " " ++ showTerm 10 t2)
410ff490af511ffa09b52e4de631d36a154b9730Christian Maederdata Sentence = Sentence { senTerm :: Term
9d515512054aaaf9c8785360391ab73091ad962dChristian Maederinstance Eq Sentence where
0a070d04a5d89ffc97147ab6f5fbbb6994afc1ccChristian Maeder s1 == s2 = senTerm s1 == senTerm s2
410ff490af511ffa09b52e4de631d36a154b9730Christian Maederinstance Ord Sentence where
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder compare s1 s2 = compare (senTerm s1) (senTerm s2)
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maederinstance Show Sentence where
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder show s = show (senTerm s)
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maederinstance PrettyPrint Sign where
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder printText0 _ sig = ptext (show sig)
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maederinstance PrintLaTeX Sign where
ad97909f160c13effd3bc73155aaa2c29902a5a1Christian Maeder printLatex0 = printText0
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder-------------------- from src/Pure/sorts.ML ------------------------
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder{-- type classes and sorts --}
227dec9850d66655627ce8b7d443898896597aa9Christian Maeder Classes denote (possibly empty) collections of types that are
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder partially ordered by class inclusion. They are represented
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder symbolically by strings.
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder Sorts are intersections of finitely many classes. They are
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder represented by lists of classes. Normal forms of sorts are sorted
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder lists of minimal classes (wrt. current class inclusion).
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder (already defined in Pure/term.ML)
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder{- sort signature information -}
a18e8529c133e17b95180bdd2bc2abbea232f698Christian Maeder table representing the proper subclass relation; entries (c, cs)
15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder represent the superclasses cs of c;
c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder table of association lists of all type arities; (t, ars) means
0dddb504c4375042bc256a7a9b4bd803d1dc18adChristian Maeder that type constructor t has the arities ars; an element (c, Ss) of
0dddb504c4375042bc256a7a9b4bd803d1dc18adChristian Maeder ars represents the arity t::(Ss)c;
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maedertype Classrel = Map.Map String [Class]
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maedertype Arities = Map.Map String [(Class, [Sort])]
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maeder-------------------- from src/Pure/type.ML ------------------------
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maederdata TypeSig =
414eef40244ffc227c16c59a1904e48611617103Christian Maeder classes:: [Class],
7551e65ddba3503270d1bf54712217cbd6b8d5fcChristian Maeder classrel:: Classrel,
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder defaultSort:: Sort,
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maeder tycons:: Map.Map String Int,
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maeder log_types:: [String],
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maeder univ_witness:: Maybe (Typ, Sort),
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maeder abbrs:: Map.Map String ([String],Typ),
414eef40244ffc227c16c59a1904e48611617103Christian Maeder arities:: Arities }
414eef40244ffc227c16c59a1904e48611617103Christian Maeder deriving (Eq)
414eef40244ffc227c16c59a1904e48611617103Christian MaederemptyTypeSig :: TypeSig
f85f722d95f8a5f928aa34b38894e9a4f60dfe84Christian MaederemptyTypeSig = TySg {
f85f722d95f8a5f928aa34b38894e9a4f60dfe84Christian Maeder classes = [],
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder defaultSort = [],
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder log_types = [],
f85f722d95f8a5f928aa34b38894e9a4f60dfe84Christian Maeder univ_witness = Nothing,
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maederinstance Show TypeSig where
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder if Map.isEmpty (tycons tysig) then ""
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder else "types\n" ++ Map.foldWithKey showTycon "" (tycons tysig)
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder where showTycon t arity rest =
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder (if arity>0 then "("++concat (map ((" 'a"++).show) [1..arity])++")"
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder-------------------- from src/Pure/sign.ML ------------------------
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maederdata Sign = Sign { baseSig :: String, -- like Pure, HOL etc.
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder tsig :: TypeSig,
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder constTab :: Map.Map String Typ,
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder syn :: Syntax
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder deriving (Eq)
03a4f2609d91287af8de36c1b06842b40638b1dfChristian MaederemptySign :: Sign
03a4f2609d91287af8de36c1b06842b40638b1dfChristian MaederemptySign = Sign { baseSig = "Pure",
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maeder tsig = emptyTypeSig,
03a4f2609d91287af8de36c1b06842b40638b1dfChristian Maederinstance Show Sign where
5124a921afd8ade94cfc339a34026cc2d339287eChristian Maeder baseSig sig ++":\n"++
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maeder shows (tsig sig)
0dddb504c4375042bc256a7a9b4bd803d1dc18adChristian Maeder (showsConstTab (constTab sig))
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maeder showsConstTab tab =
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maeder else "consts\n" ++ Map.foldWithKey showConst "" tab
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maeder showConst c t rest = show c ++ " :: " ++ "\"" ++ show t ++ "\"" ++ rest
f85f722d95f8a5f928aa34b38894e9a4f60dfe84Christian MaedersentenceTc, signTc :: TyCon
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedersentenceTc = mkTyCon "Isabelle.Sign.Sentence"
03a4f2609d91287af8de36c1b06842b40638b1dfChristian MaedersignTc = mkTyCon "Isabelle.Sign.Sign"
a681f9b62698853816145d9f8cfef33f3aea1550Christian Maederinstance Typeable Sentence where
7703df65ea5ba02e596d409de284a64739ffd317Christian Maeder typeOf _ = mkAppTy sentenceTc []
36cd83d825e16386e8bedf45be3b0670c9322594Christian Maederinstance Typeable Sign where
7703df65ea5ba02e596d409de284a64739ffd317Christian Maeder typeOf _ = mkAppTy signTc []