src/HOL/Tools/res_clause.ML
changeset 24940 8f9dea697b8d
parent 24937 340523598914
child 25243 78f8aaa27493
     1.1 --- a/src/HOL/Tools/res_clause.ML	Tue Oct 09 19:48:55 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Oct 10 10:50:11 2007 +0200
     1.3 @@ -33,18 +33,16 @@
     1.4    val make_type_class : string -> string
     1.5    datatype kind = Axiom | Conjecture
     1.6    type axiom_name = string
     1.7 -  datatype typ_var = FOLTVar of indexname | FOLTFree of string
     1.8    datatype fol_type =
     1.9        AtomV of string
    1.10      | AtomF of string
    1.11      | Comp of string * fol_type list
    1.12    val string_of_fol_type : fol_type -> string
    1.13    datatype type_literal = LTVar of string * string | LTFree of string * string
    1.14 -  val mk_typ_var_sort: typ -> typ_var * sort
    1.15    exception CLAUSE of string * term
    1.16    val isMeta : string -> bool
    1.17 -  val add_typs : (typ_var * string list) list -> type_literal list
    1.18 -  val get_tvar_strs: (typ_var * sort) list -> string list
    1.19 +  val add_typs : typ list -> type_literal list
    1.20 +  val get_tvar_strs: typ list -> string list
    1.21    datatype arLit =
    1.22        TConsLit of class * string * string list
    1.23      | TVarLit of class * string
    1.24 @@ -54,7 +52,7 @@
    1.25     {axiom_name: axiom_name, subclass: class, superclass: class}
    1.26    val make_classrel_clauses: theory -> class list -> class list -> classrelClause list
    1.27    val make_arity_clauses: theory -> string list -> class list -> class list * arityClause list
    1.28 -  val add_type_sort_preds: (typ_var * string list) * int Symtab.table -> int Symtab.table
    1.29 +  val add_type_sort_preds: typ * int Symtab.table -> int Symtab.table
    1.30    val add_classrelClause_preds : classrelClause * int Symtab.table -> int Symtab.table
    1.31    val class_of_arityLit: arLit -> class
    1.32    val add_arityClause_preds: arityClause * int Symtab.table -> int Symtab.table
    1.33 @@ -234,8 +232,6 @@
    1.34  
    1.35  (**** Isabelle FOL clauses ****)
    1.36  
    1.37 -datatype typ_var = FOLTVar of indexname | FOLTFree of string;
    1.38 -
    1.39  (*FIXME: give the constructors more sensible names*)
    1.40  datatype fol_type = AtomV of string
    1.41                    | AtomF of string
    1.42 @@ -249,12 +245,10 @@
    1.43  (*First string is the type class; the second is a TVar or TFfree*)
    1.44  datatype type_literal = LTVar of string * string | LTFree of string * string;
    1.45  
    1.46 -fun mk_typ_var_sort (TFree(a,s)) = (FOLTFree a,s)
    1.47 -  | mk_typ_var_sort (TVar(v,s)) = (FOLTVar v,s);
    1.48 -
    1.49 -
    1.50  exception CLAUSE of string * term;
    1.51  
    1.52 +fun atomic_type (TFree (a,_)) = AtomF(make_fixed_type_var a)
    1.53 +  | atomic_type (TVar (v,_))  = AtomV(make_schematic_type_var v);
    1.54  
    1.55  (*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and
    1.56    TVars it contains.*)
    1.57 @@ -262,8 +256,7 @@
    1.58        let val (folTyps, ts) = types_of Ts
    1.59            val t = make_fixed_type_const a
    1.60        in (Comp(t,folTyps), ts) end
    1.61 -  | type_of (TFree (a,s)) = (AtomF(make_fixed_type_var a), [(FOLTFree a, s)])
    1.62 -  | type_of (TVar (v, s)) = (AtomV(make_schematic_type_var v), [(FOLTVar v, s)])
    1.63 +  | type_of T = (atomic_type T, [T])
    1.64  and types_of Ts =
    1.65        let val (folTyps,ts) = ListPair.unzip (map type_of Ts)
    1.66        in (folTyps, union_all ts) end;
    1.67 @@ -274,28 +267,30 @@
    1.68  val isMeta = String.isPrefix "METAHYP1_"
    1.69  
    1.70  (*Make literals for sorted type variables*)
    1.71 -fun sorts_on_typs (_, [])   = []
    1.72 -  | sorts_on_typs (v,  s::ss) =
    1.73 -      let val sorts = sorts_on_typs (v, ss)
    1.74 +fun sorts_on_typs_aux (_, [])   = []
    1.75 +  | sorts_on_typs_aux ((x,i),  s::ss) =
    1.76 +      let val sorts = sorts_on_typs_aux ((x,i), ss)
    1.77        in
    1.78            if s = "HOL.type" then sorts
    1.79 -          else case v of
    1.80 -              FOLTVar indx => LTVar(make_type_class s, make_schematic_type_var indx) :: sorts
    1.81 -            | FOLTFree x => LTFree(make_type_class s, make_fixed_type_var x) :: sorts
    1.82 +          else if i = ~1 then LTFree(make_type_class s, make_fixed_type_var x) :: sorts
    1.83 +          else LTVar(make_type_class s, make_schematic_type_var (x,i)) :: sorts
    1.84        end;
    1.85  
    1.86 +fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
    1.87 +  | sorts_on_typs (TVar (v,s))  = sorts_on_typs_aux (v,s);
    1.88 +
    1.89  fun pred_of_sort (LTVar (s,ty)) = (s,1)
    1.90    | pred_of_sort (LTFree (s,ty)) = (s,1)
    1.91  
    1.92  (*Given a list of sorted type variables, return a list of type literals.*)
    1.93 -fun add_typs tss = foldl (op union) [] (map sorts_on_typs tss);
    1.94 +fun add_typs Ts = foldl (op union) [] (map sorts_on_typs Ts);
    1.95  
    1.96  (** make axiom and conjecture clauses. **)
    1.97  
    1.98  fun get_tvar_strs [] = []
    1.99 -  | get_tvar_strs ((FOLTVar indx,s)::tss) =
   1.100 -      insert (op =) (make_schematic_type_var indx) (get_tvar_strs tss)
   1.101 -  | get_tvar_strs((FOLTFree x,s)::tss) = get_tvar_strs tss
   1.102 +  | get_tvar_strs ((TVar (indx,s))::Ts) =
   1.103 +      insert (op =) (make_schematic_type_var indx) (get_tvar_strs Ts)
   1.104 +  | get_tvar_strs((TFree _)::Ts) = get_tvar_strs Ts
   1.105  
   1.106  
   1.107  
   1.108 @@ -405,10 +400,8 @@
   1.109  
   1.110  fun update_many (tab, keypairs) = foldl (uncurry Symtab.update) tab keypairs;
   1.111  
   1.112 -fun add_type_sort_preds ((FOLTVar indx,s), preds) =
   1.113 -      update_many (preds, map pred_of_sort (sorts_on_typs (FOLTVar indx, s)))
   1.114 -  | add_type_sort_preds ((FOLTFree x,s), preds) =
   1.115 -      update_many (preds, map pred_of_sort (sorts_on_typs (FOLTFree x, s)));
   1.116 +fun add_type_sort_preds (T, preds) =
   1.117 +      update_many (preds, map pred_of_sort (sorts_on_typs T));
   1.118  
   1.119  fun add_classrelClause_preds (ClassrelClause {subclass,superclass,...}, preds) =
   1.120    Symtab.update (subclass,1) (Symtab.update (superclass,1) preds);
   1.121 @@ -429,8 +422,8 @@
   1.122        foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys;
   1.123  
   1.124  (*TFrees are recorded as constants*)
   1.125 -fun add_type_sort_funcs ((FOLTVar _, _), funcs) = funcs
   1.126 -  | add_type_sort_funcs ((FOLTFree a, _), funcs) =
   1.127 +fun add_type_sort_funcs (TVar _, funcs) = funcs
   1.128 +  | add_type_sort_funcs (TFree (a, _), funcs) =
   1.129        Symtab.update (make_fixed_type_var a, 0) funcs
   1.130  
   1.131  fun add_arityClause_funcs (ArityClause {conclLit,...}, funcs) =