getting rid of type typ_var
authorpaulson
Wed Oct 10 10:50:11 2007 +0200 (2007-10-10)
changeset 249408f9dea697b8d
parent 24939 6dd60d1191bf
child 24941 9ab032df81c8
getting rid of type typ_var
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/res_clause.ML
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/metis_tools.ML	Tue Oct 09 19:48:55 2007 +0200
     1.2 +++ b/src/HOL/Tools/metis_tools.ML	Wed Oct 10 10:50:11 2007 +0200
     1.3 @@ -101,8 +101,8 @@
     1.4    fun metis_of_typeLit pos (ResClause.LTVar (s,x))  = metis_lit pos s [Metis.Term.Var x]
     1.5      | metis_of_typeLit pos (ResClause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
     1.6  
     1.7 -  fun default_sort ctxt (ResClause.FOLTVar _, _) = false
     1.8 -    | default_sort ctxt (ResClause.FOLTFree x, ss) = (ss = Option.getOpt (Variable.def_sort ctxt (x,~1), []));
     1.9 +  fun default_sort ctxt (TVar _) = false
    1.10 +    | default_sort ctxt (TFree(x,s)) = (s = Option.getOpt (Variable.def_sort ctxt (x,~1), []));
    1.11  
    1.12    fun metis_of_tfree tf = 
    1.13      Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf));
    1.14 @@ -503,7 +503,7 @@
    1.15  
    1.16    (*Extract TFree constraints from context to include as conjecture clauses*)
    1.17    fun init_tfrees ctxt =
    1.18 -    let fun add ((a,i),s) ys = if i = ~1 then (ResClause.FOLTFree a,s) :: ys else ys
    1.19 +    let fun add ((a,i),s) Ts = if i = ~1 then TFree(a,s) :: Ts else Ts
    1.20      in  ResClause.add_typs (Vartab.fold add (#2 (Variable.constraints_of ctxt)) []) end;
    1.21  
    1.22    (*transform isabelle clause to metis clause *)
     2.1 --- a/src/HOL/Tools/res_clause.ML	Tue Oct 09 19:48:55 2007 +0200
     2.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Oct 10 10:50:11 2007 +0200
     2.3 @@ -33,18 +33,16 @@
     2.4    val make_type_class : string -> string
     2.5    datatype kind = Axiom | Conjecture
     2.6    type axiom_name = string
     2.7 -  datatype typ_var = FOLTVar of indexname | FOLTFree of string
     2.8    datatype fol_type =
     2.9        AtomV of string
    2.10      | AtomF of string
    2.11      | Comp of string * fol_type list
    2.12    val string_of_fol_type : fol_type -> string
    2.13    datatype type_literal = LTVar of string * string | LTFree of string * string
    2.14 -  val mk_typ_var_sort: typ -> typ_var * sort
    2.15    exception CLAUSE of string * term
    2.16    val isMeta : string -> bool
    2.17 -  val add_typs : (typ_var * string list) list -> type_literal list
    2.18 -  val get_tvar_strs: (typ_var * sort) list -> string list
    2.19 +  val add_typs : typ list -> type_literal list
    2.20 +  val get_tvar_strs: typ list -> string list
    2.21    datatype arLit =
    2.22        TConsLit of class * string * string list
    2.23      | TVarLit of class * string
    2.24 @@ -54,7 +52,7 @@
    2.25     {axiom_name: axiom_name, subclass: class, superclass: class}
    2.26    val make_classrel_clauses: theory -> class list -> class list -> classrelClause list
    2.27    val make_arity_clauses: theory -> string list -> class list -> class list * arityClause list
    2.28 -  val add_type_sort_preds: (typ_var * string list) * int Symtab.table -> int Symtab.table
    2.29 +  val add_type_sort_preds: typ * int Symtab.table -> int Symtab.table
    2.30    val add_classrelClause_preds : classrelClause * int Symtab.table -> int Symtab.table
    2.31    val class_of_arityLit: arLit -> class
    2.32    val add_arityClause_preds: arityClause * int Symtab.table -> int Symtab.table
    2.33 @@ -234,8 +232,6 @@
    2.34  
    2.35  (**** Isabelle FOL clauses ****)
    2.36  
    2.37 -datatype typ_var = FOLTVar of indexname | FOLTFree of string;
    2.38 -
    2.39  (*FIXME: give the constructors more sensible names*)
    2.40  datatype fol_type = AtomV of string
    2.41                    | AtomF of string
    2.42 @@ -249,12 +245,10 @@
    2.43  (*First string is the type class; the second is a TVar or TFfree*)
    2.44  datatype type_literal = LTVar of string * string | LTFree of string * string;
    2.45  
    2.46 -fun mk_typ_var_sort (TFree(a,s)) = (FOLTFree a,s)
    2.47 -  | mk_typ_var_sort (TVar(v,s)) = (FOLTVar v,s);
    2.48 -
    2.49 -
    2.50  exception CLAUSE of string * term;
    2.51  
    2.52 +fun atomic_type (TFree (a,_)) = AtomF(make_fixed_type_var a)
    2.53 +  | atomic_type (TVar (v,_))  = AtomV(make_schematic_type_var v);
    2.54  
    2.55  (*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and
    2.56    TVars it contains.*)
    2.57 @@ -262,8 +256,7 @@
    2.58        let val (folTyps, ts) = types_of Ts
    2.59            val t = make_fixed_type_const a
    2.60        in (Comp(t,folTyps), ts) end
    2.61 -  | type_of (TFree (a,s)) = (AtomF(make_fixed_type_var a), [(FOLTFree a, s)])
    2.62 -  | type_of (TVar (v, s)) = (AtomV(make_schematic_type_var v), [(FOLTVar v, s)])
    2.63 +  | type_of T = (atomic_type T, [T])
    2.64  and types_of Ts =
    2.65        let val (folTyps,ts) = ListPair.unzip (map type_of Ts)
    2.66        in (folTyps, union_all ts) end;
    2.67 @@ -274,28 +267,30 @@
    2.68  val isMeta = String.isPrefix "METAHYP1_"
    2.69  
    2.70  (*Make literals for sorted type variables*)
    2.71 -fun sorts_on_typs (_, [])   = []
    2.72 -  | sorts_on_typs (v,  s::ss) =
    2.73 -      let val sorts = sorts_on_typs (v, ss)
    2.74 +fun sorts_on_typs_aux (_, [])   = []
    2.75 +  | sorts_on_typs_aux ((x,i),  s::ss) =
    2.76 +      let val sorts = sorts_on_typs_aux ((x,i), ss)
    2.77        in
    2.78            if s = "HOL.type" then sorts
    2.79 -          else case v of
    2.80 -              FOLTVar indx => LTVar(make_type_class s, make_schematic_type_var indx) :: sorts
    2.81 -            | FOLTFree x => LTFree(make_type_class s, make_fixed_type_var x) :: sorts
    2.82 +          else if i = ~1 then LTFree(make_type_class s, make_fixed_type_var x) :: sorts
    2.83 +          else LTVar(make_type_class s, make_schematic_type_var (x,i)) :: sorts
    2.84        end;
    2.85  
    2.86 +fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
    2.87 +  | sorts_on_typs (TVar (v,s))  = sorts_on_typs_aux (v,s);
    2.88 +
    2.89  fun pred_of_sort (LTVar (s,ty)) = (s,1)
    2.90    | pred_of_sort (LTFree (s,ty)) = (s,1)
    2.91  
    2.92  (*Given a list of sorted type variables, return a list of type literals.*)
    2.93 -fun add_typs tss = foldl (op union) [] (map sorts_on_typs tss);
    2.94 +fun add_typs Ts = foldl (op union) [] (map sorts_on_typs Ts);
    2.95  
    2.96  (** make axiom and conjecture clauses. **)
    2.97  
    2.98  fun get_tvar_strs [] = []
    2.99 -  | get_tvar_strs ((FOLTVar indx,s)::tss) =
   2.100 -      insert (op =) (make_schematic_type_var indx) (get_tvar_strs tss)
   2.101 -  | get_tvar_strs((FOLTFree x,s)::tss) = get_tvar_strs tss
   2.102 +  | get_tvar_strs ((TVar (indx,s))::Ts) =
   2.103 +      insert (op =) (make_schematic_type_var indx) (get_tvar_strs Ts)
   2.104 +  | get_tvar_strs((TFree _)::Ts) = get_tvar_strs Ts
   2.105  
   2.106  
   2.107  
   2.108 @@ -405,10 +400,8 @@
   2.109  
   2.110  fun update_many (tab, keypairs) = foldl (uncurry Symtab.update) tab keypairs;
   2.111  
   2.112 -fun add_type_sort_preds ((FOLTVar indx,s), preds) =
   2.113 -      update_many (preds, map pred_of_sort (sorts_on_typs (FOLTVar indx, s)))
   2.114 -  | add_type_sort_preds ((FOLTFree x,s), preds) =
   2.115 -      update_many (preds, map pred_of_sort (sorts_on_typs (FOLTFree x, s)));
   2.116 +fun add_type_sort_preds (T, preds) =
   2.117 +      update_many (preds, map pred_of_sort (sorts_on_typs T));
   2.118  
   2.119  fun add_classrelClause_preds (ClassrelClause {subclass,superclass,...}, preds) =
   2.120    Symtab.update (subclass,1) (Symtab.update (superclass,1) preds);
   2.121 @@ -429,8 +422,8 @@
   2.122        foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys;
   2.123  
   2.124  (*TFrees are recorded as constants*)
   2.125 -fun add_type_sort_funcs ((FOLTVar _, _), funcs) = funcs
   2.126 -  | add_type_sort_funcs ((FOLTFree a, _), funcs) =
   2.127 +fun add_type_sort_funcs (TVar _, funcs) = funcs
   2.128 +  | add_type_sort_funcs (TFree (a, _), funcs) =
   2.129        Symtab.update (make_fixed_type_var a, 0) funcs
   2.130  
   2.131  fun add_arityClause_funcs (ArityClause {conclLit,...}, funcs) =
     3.1 --- a/src/HOL/Tools/res_hol_clause.ML	Tue Oct 09 19:48:55 2007 +0200
     3.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Wed Oct 10 10:50:11 2007 +0200
     3.3 @@ -28,7 +28,7 @@
     3.4      | CombApp of combterm * combterm
     3.5    datatype literal = Literal of polarity * combterm
     3.6    val strip_comb: combterm -> combterm * combterm list
     3.7 -  val literals_of_term: theory -> term -> literal list * (ResClause.typ_var * sort) list
     3.8 +  val literals_of_term: theory -> term -> literal list * typ list
     3.9    val tptp_write_file: theory -> bool -> thm list -> string ->
    3.10      (thm * (axiom_name * clause_id)) list * ResClause.classrelClause list *
    3.11        ResClause.arityClause list -> string list -> axiom_name list
    3.12 @@ -97,7 +97,7 @@
    3.13                      th: thm,
    3.14                      kind: RC.kind,
    3.15                      literals: literal list,
    3.16 -                    ctypes_sorts: (RC.typ_var * Term.sort) list};
    3.17 +                    ctypes_sorts: typ list};
    3.18  
    3.19  
    3.20  (*********************************************************************)
    3.21 @@ -120,9 +120,9 @@
    3.22        let val (folTypes,ts) = types_of Ts
    3.23        in  (RC.Comp(RC.make_fixed_type_const a, folTypes), ts)  end
    3.24    | type_of (tp as (TFree(a,s))) =
    3.25 -      (RC.AtomF (RC.make_fixed_type_var a), [RC.mk_typ_var_sort tp])
    3.26 +      (RC.AtomF (RC.make_fixed_type_var a), [tp])
    3.27    | type_of (tp as (TVar(v,s))) =
    3.28 -      (RC.AtomV (RC.make_schematic_type_var v), [RC.mk_typ_var_sort tp])
    3.29 +      (RC.AtomV (RC.make_schematic_type_var v), [tp])
    3.30  and types_of Ts =
    3.31        let val (folTyps,ts) = ListPair.unzip (map type_of Ts)
    3.32        in  (folTyps, RC.union_all ts)  end;