--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/zterm.ML Thu Nov 30 23:15:18 2023 +0100
@@ -0,0 +1,171 @@
+(* Title: Pure/zterm.ML
+ Author: Makarius
+
+Tight representation of types / terms / proof terms, notably for proof recording.
+*)
+
+(* global datatypes *)
+
+datatype ztyp =
+ ZTFree of string * sort
+ | ZTVar of indexname * sort
+ | ZFun of ztyp * ztyp
+ | ZProp
+ | ZItself of ztyp
+ | ZType0 of string (*type constant*)
+ | ZType1 of string * ztyp (*type constructor: 1 argument*)
+ | ZType of string * ztyp list (*type constructor: >= 2 arguments*)
+
+datatype zterm =
+ ZFree of string * ztyp
+ | ZVar of indexname * ztyp
+ | ZBound of int
+ | ZConst0 of string (*monomorphic constant*)
+ | ZConst1 of string * ztyp (*polymorphic constant: 1 type argument*)
+ | ZConst of string * ztyp list (*polymorphic constant: >= 2 type arguments*)
+ | ZAbs of string * ztyp * zterm
+ | ZApp of zterm * zterm
+ | ZClass of ztyp * class (*OFCLASS proposition*)
+
+datatype zproof =
+ ZDummy (*dummy proof*)
+ | ZConstP of serial * ztyp list (*proof constant: local box, global axiom or thm*)
+ | ZBoundP of int
+ | ZHyp of zterm
+ | ZAbst of string * ztyp * zproof
+ | ZAbsP of string * zterm * zproof
+ | ZAppt of zproof * zterm
+ | ZAppP of zproof * zproof
+ | ZClassP of ztyp * class (*OFCLASS proof from sorts algebra*)
+ | ZOracle of serial * zterm * ztyp list
+and zproof_body = ZPBody of
+ {boxes: (zterm * zproof future) Inttab.table,
+ consts: serial Ord_List.T,
+ oracles: ((string * Position.T) * zterm option) Ord_List.T,
+ proof: zproof}
+
+
+signature ZTERM =
+sig
+ datatype ztyp = datatype ztyp
+ datatype zterm = datatype zterm
+ datatype zproof = datatype zproof
+ val ztyp_ord: ztyp * ztyp -> order
+ val zaconv: zterm * zterm -> bool
+ val ztyp_of: typ -> ztyp
+ val typ_of: ztyp -> typ
+ val zterm_of: Consts.T -> term -> zterm
+ val term_of: Consts.T -> zterm -> term
+end;
+
+structure ZTerm: ZTERM =
+struct
+
+datatype ztyp = datatype ztyp;
+datatype zterm = datatype zterm;
+datatype zproof = datatype zproof;
+
+
+(* orderings *)
+
+local
+
+fun cons_nr (ZTFree _) = 0
+ | cons_nr (ZTVar _) = 1
+ | cons_nr (ZFun _) = 2
+ | cons_nr ZProp = 3
+ | cons_nr (ZItself _) = 4
+ | cons_nr (ZType0 _) = 5
+ | cons_nr (ZType1 _) = 6
+ | cons_nr (ZType _) = 7;
+
+val fast_indexname_ord = Term_Ord.fast_indexname_ord;
+val sort_ord = Term_Ord.sort_ord;
+
+in
+
+fun ztyp_ord TU =
+ if pointer_eq TU then EQUAL
+ else
+ (case TU of
+ (ZTFree (a, A), ZTFree (b, B)) =>
+ (case fast_string_ord (a, b) of EQUAL => sort_ord (A, B) | ord => ord)
+ | (ZTVar (a, A), ZTVar (b, B)) =>
+ (case fast_indexname_ord (a, b) of EQUAL => Term_Ord.sort_ord (A, B) | ord => ord)
+ | (ZFun (T, T'), ZFun (U, U')) =>
+ (case ztyp_ord (T, U) of EQUAL => ztyp_ord (T', U') | ord => ord)
+ | (ZProp, ZProp) => EQUAL
+ | (ZItself T, ZItself U) => ztyp_ord (T, U)
+ | (ZType0 a, ZType0 b) => fast_string_ord (a, b)
+ | (ZType1 (a, T), ZType1 (b, U)) =>
+ (case fast_string_ord (a, b) of EQUAL => ztyp_ord (T, U) | ord => ord)
+ | (ZType (a, Ts), ZType (b, Us)) =>
+ (case fast_string_ord (a, b) of EQUAL => dict_ord ztyp_ord (Ts, Us) | ord => ord)
+ | (T, U) => int_ord (cons_nr T, cons_nr U));
+
+end;
+
+
+(* alpha conversion *)
+
+fun zaconv (tm1, tm2) =
+ pointer_eq (tm1, tm2) orelse
+ (case (tm1, tm2) of
+ (ZApp (t1, u1), ZApp (t2, u2)) => zaconv (t1, t2) andalso zaconv (u1, u2)
+ | (ZAbs (_, T1, t1), ZAbs (_, T2, t2)) => zaconv (t1, t2) andalso T1 = T2
+ | (a1, a2) => a1 = a2);
+
+
+(* convert ztyp / zterm vs. regular typ / term *)
+
+fun ztyp_of (TFree v) = ZTFree v
+ | ztyp_of (TVar v) = ZTVar v
+ | ztyp_of (Type ("fun", [T, U])) = ZFun (ztyp_of T, ztyp_of U)
+ | ztyp_of (Type (c, [])) = if c = "prop" then ZProp else ZType0 c
+ | ztyp_of (Type (c, [T])) = if c = "itself" then ZItself (ztyp_of T) else ZType1 (c, ztyp_of T)
+ | ztyp_of (Type (c, ts)) = ZType (c, map ztyp_of ts);
+
+fun typ_of (ZTFree v) = TFree v
+ | typ_of (ZTVar v) = TVar v
+ | typ_of (ZFun (T, U)) = typ_of T --> typ_of U
+ | typ_of ZProp = propT
+ | typ_of (ZItself T) = Term.itselfT (typ_of T)
+ | typ_of (ZType0 c) = Type (c, [])
+ | typ_of (ZType1 (c, T)) = Type (c, [typ_of T])
+ | typ_of (ZType (c, Ts)) = Type (c, map typ_of Ts);
+
+fun zterm_of consts =
+ let
+ val typargs = Consts.typargs consts;
+ fun zterm (Free (x, T)) = ZFree (x, ztyp_of T)
+ | zterm (Var (xi, T)) = ZVar (xi, ztyp_of T)
+ | zterm (Bound i) = ZBound i
+ | zterm (Const (c, T)) =
+ (case typargs (c, T) of
+ [] => ZConst0 c
+ | [T] => ZConst1 (c, ztyp_of T)
+ | Ts => ZConst (c, map ztyp_of Ts))
+ | zterm (Abs (a, T, b)) = ZAbs (a, ztyp_of T, zterm b)
+ | zterm ((t as Const (c, _)) $ (u as Const ("Pure.type", _))) =
+ if String.isSuffix Logic.class_suffix c then
+ ZClass (ztyp_of (Logic.dest_type u), Logic.class_of_const c)
+ else ZApp (zterm t, zterm u)
+ | zterm (t $ u) = ZApp (zterm t, zterm u);
+ in zterm end;
+
+fun term_of consts =
+ let
+ val instance = Consts.instance consts;
+ fun const (c, Ts) = Const (c, instance (c, Ts));
+ fun term (ZFree (x, T)) = Free (x, typ_of T)
+ | term (ZVar (xi, T)) = Var (xi, typ_of T)
+ | term (ZBound i) = Bound i
+ | term (ZConst0 c) = const (c, [])
+ | term (ZConst1 (c, T)) = const (c, [typ_of T])
+ | term (ZConst (c, Ts)) = const (c, map typ_of Ts)
+ | term (ZAbs (a, T, b)) = Abs (a, typ_of T, term b)
+ | term (ZApp (t, u)) = term t $ term u
+ | term (ZClass (T, c)) = Logic.mk_of_class (typ_of T, c);
+ in term end;
+
+end;