IsaSign.hs revision 4ef05f4edeb290beb89845f57156baa5298af7c4
4632N/A{- |
4632N/AModule : $Header$
4632N/ACopyright : (c) University of Cambridge, Cambridge, England
4632N/A adaption (c) Till Mossakowski, Uni Bremen 2002-2005
4632N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
4632N/A
4632N/AMaintainer : maeder@tzi.de
4632N/AStability : provisional
4632N/APortability : portable
4632N/A
4632N/AData structures for Isabelle signatures and theories.
4632N/A Adapted from Isabelle.
4632N/A
4632N/A
4632N/A-}
4632N/A
4632N/Amodule Isabelle.IsaSign where
4632N/A
4632N/Aimport qualified Common.Lib.Map as Map
4632N/A
4632N/A-------------------- not quite from src/Pure/term.ML ------------------------
4632N/A----------------------------- Names -----------------------------------------
4632N/A
4632N/A-- | type names
4632N/Atype TName = String
4632N/A
4632N/A-- | names for values or constants (non-classes and non-types)
4632N/Adata VName = VName
4632N/A { new :: String -- ^ name within Isabelle
4632N/A , altSyn :: Maybe AltSyntax -- ^ mixfix template syntax
4632N/A } deriving Show
4632N/A
4632N/Adata AltSyntax = AltSyntax String [Int] Int deriving Show
4632N/A
4632N/AmkVName :: String -> VName
4632N/AmkVName s = VName { new = s, altSyn = Nothing }
4632N/A
4632N/A-- | the original (Haskell) name
4632N/Aorig :: VName -> String
4632N/Aorig = new
4632N/A
4632N/Ainstance Eq VName where
4632N/A v1 == v2 = new v1 == new v2
4632N/A
4632N/Ainstance Ord VName where
4632N/A v1 <= v2 = new v1 <= new v2
4632N/A
4632N/A{- | Indexnames can be quickly renamed by adding an offset to the integer part,
4632N/A for resolution. -}
4632N/Adata Indexname = Indexname
4632N/A { unindexed :: String
4632N/A , indexOffset :: Int
4632N/A } deriving (Ord, Eq, Show)
4632N/A
4632N/A--------- Classes
4632N/A{- Types are classified by sorts. -}
4632N/A
4632N/Adata IsaClass = IsaClass String
4632N/A deriving (Ord, Eq, Show)
4632N/A
4632N/Atype Sort = [IsaClass]
4632N/A
4632N/A----------- Kinds
4632N/A
4632N/Adata ExKind = IKind IsaKind | IClass | PLogic
4632N/A
4632N/Adata IsaKind = Star
4632N/A | Kfun IsaKind IsaKind
4632N/A deriving (Ord, Eq, Show)
4632N/A
4632N/A------------------------------------------------------------------------------
4632N/A
4632N/A{- The sorts attached to TFrees and TVars specify the sort of that variable -}
4632N/Adata Typ = Type { typeId :: TName,
4632N/A typeSort :: Sort,
4632N/A typeArgs :: [Typ] }
4632N/A | TFree { typeId :: TName,
4632N/A typeSort :: Sort }
4632N/A | TVar { indexname :: Indexname,
4632N/A typeSort :: Sort }
4632N/A deriving (Eq, Ord, Show)
4632N/A
4632N/A
4632N/A{-Terms. Bound variables are indicated by depth number.
4632N/A Free variables, (scheme) variables and constants have names.
4632N/A A term is "closed" if every bound variable of level "lev"
4632N/A is enclosed by at least "lev" abstractions.
4632N/A
4632N/A It is possible to create meaningless terms containing loose bound vars
4632N/A or type mismatches. But such terms are not allowed in rules. -}
4632N/A
4632N/Adata Continuity = IsCont | NotCont deriving (Eq, Ord ,Show)
4632N/A
4632N/Adata Term =
4632N/A Const { termName :: VName,
4632N/A termType :: Typ }
4632N/A | Free { termName :: VName,
4632N/A termType :: Typ }
4632N/A | Var Indexname Typ
4632N/A | Bound Int
4632N/A | Abs { absVar :: Term,
4632N/A termType :: Typ,
4632N/A termId :: Term,
4632N/A continuity :: Continuity } -- lambda abstraction
4632N/A | App { funId :: Term,
4632N/A argId :: Term,
4632N/A continuity :: Continuity } -- application
4632N/A | MixfixApp { funId :: Term,
4632N/A argIds :: [Term],
4632N/A continuity :: Continuity } -- mixfix application
4632N/A | If { ifId :: Term,
4632N/A thenId :: Term,
4632N/A elseId :: Term,
4632N/A continuity :: Continuity }
4632N/A | Case { termId :: Term,
4632N/A caseSubst :: [(Term, Term)] }
4632N/A | Let { letSubst :: [(Term, Term)],
4632N/A inId :: Term }
4632N/A | IsaEq { firstTerm :: Term,
4632N/A secondTerm :: Term }
4632N/A | Tuplex [Term] Continuity
4632N/A | Fix Term
4632N/A | Bottom
4632N/A | Paren Term
4632N/A | Wildcard
4632N/A deriving (Eq, Ord, Show)
4632N/A
4632N/Adata Sentence = Sentence { isSimp :: Bool -- True for "[simp]"
4632N/A , isRefuteAux :: Bool
4632N/A , senTerm :: Term
4632N/A , thmProof :: Maybe String }
4632N/A | ConstDef { senTerm :: Term }
4632N/A | RecDef { keyWord :: String
4632N/A , senTerms :: [[Term]] }
4632N/A deriving (Eq, Ord, Show)
4632N/A
4632N/AmkSen :: Term -> Sentence
4632N/AmkSen t = Sentence
4632N/A { isSimp = False
4632N/A , isRefuteAux = False
4632N/A , thmProof = Nothing
4632N/A , senTerm = t }
4632N/A
4632N/AmkRefuteSen :: Term -> Sentence
4632N/AmkRefuteSen t = (mkSen t) { isRefuteAux = True }
4632N/A
4632N/AisRefute :: Sentence -> Bool
4632N/AisRefute s = case s of
4632N/A Sentence { isRefuteAux = b } -> b
4632N/A _ -> False
4632N/A
4632N/A-------------------- from src/Pure/sorts.ML ------------------------
4632N/A
4632N/A{-- type classes and sorts --}
4632N/A
4632N/A{- Classes denote (possibly empty) collections of types that are
4632N/A partially ordered by class inclusion. They are represented
4632N/A symbolically by strings.
4632N/A
4632N/A Sorts are intersections of finitely many classes. They are
4632N/A represented by lists of classes. Normal forms of sorts are sorted
4632N/A lists of minimal classes (wrt. current class inclusion).
4632N/A
4632N/A (already defined in Pure/term.ML)
4632N/A
4632N/A classrel:
4632N/A table representing the proper subclass relation; entries (c, cs)
4632N/A represent the superclasses cs of c;
4632N/A
4632N/A arities:
4632N/A table of association lists of all type arities; (t, ars) means
4632N/A that type constructor t has the arities ars; an element (c, Ss) of
4632N/A ars represents the arity t::(Ss)c;
4632N/A-}
4632N/A
4632N/Atype Classrel = Map.Map IsaClass (Maybe [IsaClass])
4632N/Atype Arities = Map.Map TName [(IsaClass, [(Typ, Sort)])]
4632N/Atype Abbrs = Map.Map TName ([TName], Typ)
4632N/A
4632N/Adata TypeSig =
4632N/A TySg {
4632N/A classrel:: Classrel, -- domain of the map yields the classes
4632N/A defaultSort:: Sort,
4632N/A log_types:: [TName],
4632N/A univ_witness:: Maybe (Typ, Sort),
4632N/A abbrs:: Abbrs, -- constructor name, variable names, type.
4632N/A arities:: Arities }
4632N/A -- actually isa-instances. the former field tycons can be computed.
4632N/A deriving (Eq, Show)
4632N/A
4632N/AemptyTypeSig :: TypeSig
4632N/AemptyTypeSig = TySg {
4632N/A classrel = Map.empty,
4632N/A defaultSort = [],
4632N/A log_types = [],
4632N/A univ_witness = Nothing,
4632N/A abbrs = Map.empty,
4632N/A arities = Map.empty }
4632N/A
4632N/A-------------------- from src/Pure/sign.ML ------------------------
4632N/A
4632N/Adata BaseSig = Main_thy -- ^ main theory of higher order logic (HOL)
4632N/A | MainHC_thy -- ^ extend main theory of HOL logic for HasCASL
4632N/A | HOLCF_thy -- ^ higher order logic for continuous functions
4632N/A | HsHOLCF_thy -- ^ HOLCF for Haskell
4632N/A deriving (Eq, Ord, Show)
4632N/A {- possibly simply supply a theory like MainHC as string
4632N/A or recursively as Isabelle.Sign -}
4632N/A
4632N/Adata Sign = Sign
4632N/A { baseSig :: BaseSig, -- like Main etc.
4632N/A tsig :: TypeSig,
4632N/A constTab :: ConstTab, -- value cons with type
4632N/A domainTab :: DomainTab,
4632N/A showLemmas :: Bool
4632N/A } deriving (Eq, Show)
4632N/A
4632N/A {- list of datatype definitions
4632N/A each of these consists of a list of (mutually recursive) datatypes
4632N/A each datatype consists of its name (Typ) and a list of constructors
4632N/A each constructor consists of its name (String) and list of argument types
4632N/A -}
4632N/A
4632N/Atype ConstTab = Map.Map VName Typ
4632N/A
4632N/A-- same types for data types and domains
4632N/A
4632N/Atype DomainTab = [[DomainEntry]]
4632N/Atype DomainEntry = (Typ, [(VName, [Typ])])
4632N/A
4632N/AemptySign :: Sign
4632N/AemptySign = Sign { baseSig = Main_thy,
4632N/A tsig = emptyTypeSig,
4632N/A constTab = Map.empty,
4632N/A domainTab = [],
4632N/A showLemmas = False }
4632N/A
4632N/A------------------------ Sentence -------------------------------------
4632N/A
4632N/A{- Instances in Haskell have form:
4632N/A
4632N/Ainstance (MyClass a, MyClass b) => MyClass (MyTypeConst a b)
4632N/A
4632N/AIn Isabelle:
4632N/A
4632N/Ainstance MyTypeConst :: (MyClass, MyClass) MyClass
4632N/A
4632N/ANote that the Isabelle syntax does not allows for multi-parameter classes.
4632N/ARather, it subsumes the syntax for arities.
4632N/A
4632N/AType constraints are applied to value constructors in Haskell as follows:
4632N/A
4632N/AMyValCon :: (MyClass a, MyClass b) => MyTypeConst a b
4632N/A
4632N/AIn Isabelle:
4632N/A
4632N/AMyValCon :: MyTypeConst (a::MyClass) (b::MyClass)
4632N/A
4632N/AIn both cases, the typing expressions may be encoded as schemes.
4632N/ASchemes and instances allows for the inference of type constraints over
4632N/Avalues of functions.
4632N/A-}
4632N/A