--- a/src/HOL/Tools/metis_tools.ML Tue Oct 09 19:48:55 2007 +0200
+++ b/src/HOL/Tools/metis_tools.ML Wed Oct 10 10:50:11 2007 +0200
@@ -101,8 +101,8 @@
fun metis_of_typeLit pos (ResClause.LTVar (s,x)) = metis_lit pos s [Metis.Term.Var x]
| metis_of_typeLit pos (ResClause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
- fun default_sort ctxt (ResClause.FOLTVar _, _) = false
- | default_sort ctxt (ResClause.FOLTFree x, ss) = (ss = Option.getOpt (Variable.def_sort ctxt (x,~1), []));
+ fun default_sort ctxt (TVar _) = false
+ | default_sort ctxt (TFree(x,s)) = (s = Option.getOpt (Variable.def_sort ctxt (x,~1), []));
fun metis_of_tfree tf =
Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf));
@@ -503,7 +503,7 @@
(*Extract TFree constraints from context to include as conjecture clauses*)
fun init_tfrees ctxt =
- let fun add ((a,i),s) ys = if i = ~1 then (ResClause.FOLTFree a,s) :: ys else ys
+ let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
in ResClause.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
(*transform isabelle clause to metis clause *)
--- a/src/HOL/Tools/res_clause.ML Tue Oct 09 19:48:55 2007 +0200
+++ b/src/HOL/Tools/res_clause.ML Wed Oct 10 10:50:11 2007 +0200
@@ -33,18 +33,16 @@
val make_type_class : string -> string
datatype kind = Axiom | Conjecture
type axiom_name = string
- datatype typ_var = FOLTVar of indexname | FOLTFree of string
datatype fol_type =
AtomV of string
| AtomF of string
| Comp of string * fol_type list
val string_of_fol_type : fol_type -> string
datatype type_literal = LTVar of string * string | LTFree of string * string
- val mk_typ_var_sort: typ -> typ_var * sort
exception CLAUSE of string * term
val isMeta : string -> bool
- val add_typs : (typ_var * string list) list -> type_literal list
- val get_tvar_strs: (typ_var * sort) list -> string list
+ val add_typs : typ list -> type_literal list
+ val get_tvar_strs: typ list -> string list
datatype arLit =
TConsLit of class * string * string list
| TVarLit of class * string
@@ -54,7 +52,7 @@
{axiom_name: axiom_name, subclass: class, superclass: class}
val make_classrel_clauses: theory -> class list -> class list -> classrelClause list
val make_arity_clauses: theory -> string list -> class list -> class list * arityClause list
- val add_type_sort_preds: (typ_var * string list) * int Symtab.table -> int Symtab.table
+ val add_type_sort_preds: typ * int Symtab.table -> int Symtab.table
val add_classrelClause_preds : classrelClause * int Symtab.table -> int Symtab.table
val class_of_arityLit: arLit -> class
val add_arityClause_preds: arityClause * int Symtab.table -> int Symtab.table
@@ -234,8 +232,6 @@
(**** Isabelle FOL clauses ****)
-datatype typ_var = FOLTVar of indexname | FOLTFree of string;
-
(*FIXME: give the constructors more sensible names*)
datatype fol_type = AtomV of string
| AtomF of string
@@ -249,12 +245,10 @@
(*First string is the type class; the second is a TVar or TFfree*)
datatype type_literal = LTVar of string * string | LTFree of string * string;
-fun mk_typ_var_sort (TFree(a,s)) = (FOLTFree a,s)
- | mk_typ_var_sort (TVar(v,s)) = (FOLTVar v,s);
-
-
exception CLAUSE of string * term;
+fun atomic_type (TFree (a,_)) = AtomF(make_fixed_type_var a)
+ | atomic_type (TVar (v,_)) = AtomV(make_schematic_type_var v);
(*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and
TVars it contains.*)
@@ -262,8 +256,7 @@
let val (folTyps, ts) = types_of Ts
val t = make_fixed_type_const a
in (Comp(t,folTyps), ts) end
- | type_of (TFree (a,s)) = (AtomF(make_fixed_type_var a), [(FOLTFree a, s)])
- | type_of (TVar (v, s)) = (AtomV(make_schematic_type_var v), [(FOLTVar v, s)])
+ | type_of T = (atomic_type T, [T])
and types_of Ts =
let val (folTyps,ts) = ListPair.unzip (map type_of Ts)
in (folTyps, union_all ts) end;
@@ -274,28 +267,30 @@
val isMeta = String.isPrefix "METAHYP1_"
(*Make literals for sorted type variables*)
-fun sorts_on_typs (_, []) = []
- | sorts_on_typs (v, s::ss) =
- let val sorts = sorts_on_typs (v, ss)
+fun sorts_on_typs_aux (_, []) = []
+ | sorts_on_typs_aux ((x,i), s::ss) =
+ let val sorts = sorts_on_typs_aux ((x,i), ss)
in
if s = "HOL.type" then sorts
- else case v of
- FOLTVar indx => LTVar(make_type_class s, make_schematic_type_var indx) :: sorts
- | FOLTFree x => LTFree(make_type_class s, make_fixed_type_var x) :: sorts
+ else if i = ~1 then LTFree(make_type_class s, make_fixed_type_var x) :: sorts
+ else LTVar(make_type_class s, make_schematic_type_var (x,i)) :: sorts
end;
+fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
+ | sorts_on_typs (TVar (v,s)) = sorts_on_typs_aux (v,s);
+
fun pred_of_sort (LTVar (s,ty)) = (s,1)
| pred_of_sort (LTFree (s,ty)) = (s,1)
(*Given a list of sorted type variables, return a list of type literals.*)
-fun add_typs tss = foldl (op union) [] (map sorts_on_typs tss);
+fun add_typs Ts = foldl (op union) [] (map sorts_on_typs Ts);
(** make axiom and conjecture clauses. **)
fun get_tvar_strs [] = []
- | get_tvar_strs ((FOLTVar indx,s)::tss) =
- insert (op =) (make_schematic_type_var indx) (get_tvar_strs tss)
- | get_tvar_strs((FOLTFree x,s)::tss) = get_tvar_strs tss
+ | get_tvar_strs ((TVar (indx,s))::Ts) =
+ insert (op =) (make_schematic_type_var indx) (get_tvar_strs Ts)
+ | get_tvar_strs((TFree _)::Ts) = get_tvar_strs Ts
@@ -405,10 +400,8 @@
fun update_many (tab, keypairs) = foldl (uncurry Symtab.update) tab keypairs;
-fun add_type_sort_preds ((FOLTVar indx,s), preds) =
- update_many (preds, map pred_of_sort (sorts_on_typs (FOLTVar indx, s)))
- | add_type_sort_preds ((FOLTFree x,s), preds) =
- update_many (preds, map pred_of_sort (sorts_on_typs (FOLTFree x, s)));
+fun add_type_sort_preds (T, preds) =
+ update_many (preds, map pred_of_sort (sorts_on_typs T));
fun add_classrelClause_preds (ClassrelClause {subclass,superclass,...}, preds) =
Symtab.update (subclass,1) (Symtab.update (superclass,1) preds);
@@ -429,8 +422,8 @@
foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys;
(*TFrees are recorded as constants*)
-fun add_type_sort_funcs ((FOLTVar _, _), funcs) = funcs
- | add_type_sort_funcs ((FOLTFree a, _), funcs) =
+fun add_type_sort_funcs (TVar _, funcs) = funcs
+ | add_type_sort_funcs (TFree (a, _), funcs) =
Symtab.update (make_fixed_type_var a, 0) funcs
fun add_arityClause_funcs (ArityClause {conclLit,...}, funcs) =
--- a/src/HOL/Tools/res_hol_clause.ML Tue Oct 09 19:48:55 2007 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML Wed Oct 10 10:50:11 2007 +0200
@@ -28,7 +28,7 @@
| CombApp of combterm * combterm
datatype literal = Literal of polarity * combterm
val strip_comb: combterm -> combterm * combterm list
- val literals_of_term: theory -> term -> literal list * (ResClause.typ_var * sort) list
+ val literals_of_term: theory -> term -> literal list * typ list
val tptp_write_file: theory -> bool -> thm list -> string ->
(thm * (axiom_name * clause_id)) list * ResClause.classrelClause list *
ResClause.arityClause list -> string list -> axiom_name list
@@ -97,7 +97,7 @@
th: thm,
kind: RC.kind,
literals: literal list,
- ctypes_sorts: (RC.typ_var * Term.sort) list};
+ ctypes_sorts: typ list};
(*********************************************************************)
@@ -120,9 +120,9 @@
let val (folTypes,ts) = types_of Ts
in (RC.Comp(RC.make_fixed_type_const a, folTypes), ts) end
| type_of (tp as (TFree(a,s))) =
- (RC.AtomF (RC.make_fixed_type_var a), [RC.mk_typ_var_sort tp])
+ (RC.AtomF (RC.make_fixed_type_var a), [tp])
| type_of (tp as (TVar(v,s))) =
- (RC.AtomV (RC.make_schematic_type_var v), [RC.mk_typ_var_sort tp])
+ (RC.AtomV (RC.make_schematic_type_var v), [tp])
and types_of Ts =
let val (folTyps,ts) = ListPair.unzip (map type_of Ts)
in (folTyps, RC.union_all ts) end;