(* *********************************************************************** *)
(* *)
(* Project: HOLZ: Structure Preserving Encoding of Z in Isabelle *)
(* Author: B.Wolff, F.Rittinger, Albert-Ludwigs-Universität Freiburg *)
(* $Date: 2002/08/06 12:56:58 $ *)
(* $Id: ZAbsy.sml,v 1.61 2002/08/06 12:56:58 wolff Exp $ *)
(* Purpose of this file: Abstract Syntax for ZETA-Z, Converter, Loader *)
(* *)
(* *********************************************************************** *)
(* structure ZAbsy : ZABSY = *)
structure ZAbsy =
struct
open ZPrelude HOLogic;
datatype QuantorKind = Exists | Exists1 | Forall | Let | Set | Lambda
| Mu;
datatype FactKind = True | False;
datatype UnaryKind = Power | Theta | Not | Delta | Xi | Pre
| Hide | Decorate;
datatype BinaryKind = And | Or | Iff | Implies | Apply | Compose
| Pipe | Project;
datatype Branch = Constant of string
| Function of string * Expr
and Expr = Number of string
| Denotation of string
| NameAppl of string * Expr list (* variables *)
| Tuple of Expr list
| Product of Expr list
| Binding of Expr list
| Signature of (string * Expr) list
| Display of Expr list
| Cond of Expr * Expr * Expr
| Quantor of QuantorKind * Expr list *
Expr list * Expr
| SchemaText of Expr list * Expr list
| Select of Expr * Expr * Expr
| Unary of UnaryKind * Expr
| Binary of BinaryKind * Expr * Expr
| GivenType of string
| FreeType of string * Branch list
| Test of Expr * Expr
| Fact of FactKind
| Eqn of string * Expr * Expr
| Direct of string list * Expr
| Gen of string list * Expr
| Type of Expr
| EmbeddedText of string
| ZedFixity of string
| Renaming of Expr * (Expr * string) list
| SchemaName of string * Expr * Expr list
type Item = Expr
(* type Item = Expr * Expr *)
datatype Section = ZSection of string * string list * Item list
end