src/HOL/Tools/res_clause.ML
changeset 21813 06a06f6d3166
parent 21790 9d2761d09d91
child 21858 05f57309170c
     1.1 --- a/src/HOL/Tools/res_clause.ML	Wed Dec 13 12:10:54 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Dec 13 12:42:26 2006 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4    datatype fol_type = AtomV of string
     1.5                      | AtomF of string
     1.6                      | Comp of string * fol_type list;
     1.7 -  datatype fol_term = UVar of string * fol_type
     1.8 +  datatype fol_term = UVar of string
     1.9                      | Fun of string * fol_type list * fol_term list;
    1.10    datatype predicate = Predicate of string * fol_type list * fol_term list;
    1.11    datatype kind = Axiom | Conjecture;
    1.12 @@ -55,13 +55,13 @@
    1.13    val string_of_fol_type : fol_type -> string
    1.14    val tconst_prefix : string 
    1.15    val tfree_prefix : string
    1.16 +  val tvar_prefix : string
    1.17    val tptp_arity_clause : arityClause -> string
    1.18    val tptp_classrelClause : classrelClause -> string
    1.19    val tptp_of_typeLit : type_literal -> string
    1.20    val tptp_tfree_clause : string -> string
    1.21    val tptp_write_file: thm list -> string -> 
    1.22         ((thm * (string * int)) list * classrelClause list * arityClause list) -> string list
    1.23 -  val tvar_prefix : string
    1.24    val union_all : ''a list list -> ''a list
    1.25    val writeln_strs: TextIO.outstream -> TextIO.vector list -> unit
    1.26    val dfg_sign: bool -> string -> string
    1.27 @@ -230,7 +230,7 @@
    1.28  (*First string is the type class; the second is a TVar or TFfree*)
    1.29  datatype type_literal = LTVar of string * string | LTFree of string * string;
    1.30  
    1.31 -datatype fol_term = UVar of string * fol_type
    1.32 +datatype fol_term = UVar of string
    1.33                    | Fun of string * fol_type list * fol_term list;
    1.34  datatype predicate = Predicate of string * fol_type list * fol_term list;
    1.35  
    1.36 @@ -304,14 +304,6 @@
    1.37    | pred_name_type (v as Var _) = raise CLAUSE("Predicate Not First Order 2", v)
    1.38    | pred_name_type t        = raise CLAUSE("Predicate input unexpected", t);
    1.39  
    1.40 -
    1.41 -(* For typed equality *)
    1.42 -(* here "arg_typ" is the type of "="'s argument's type, not the type of the equality *)
    1.43 -(* Find type of equality arg *)
    1.44 -fun eq_arg_type (Type("fun",[T,_])) = 
    1.45 -    let val (folT,_) = type_of T;
    1.46 -    in  folT  end;
    1.47 -
    1.48  fun fun_name_type (Const(c,T)) args = (make_fixed_const c, const_types_of (c,T))
    1.49    | fun_name_type (Free(x,T)) args  = 
    1.50         if isMeta x then raise CLAUSE("Function Not First Order", Free(x,T))
    1.51 @@ -321,13 +313,13 @@
    1.52  (*Convert a term to a fol_term while accumulating sort constraints on the TFrees and
    1.53    TVars it contains.*)    
    1.54  fun term_of (Var(ind_nm,T)) = 
    1.55 -      let val (folType,ts) = type_of T
    1.56 -      in (UVar(make_schematic_var ind_nm, folType), ts) end
    1.57 +      let val (_,ts) = type_of T
    1.58 +      in (UVar(make_schematic_var ind_nm), ts) end
    1.59    | term_of (Free(x,T)) = 
    1.60 -      let val (folType, ts) = type_of T
    1.61 +      let val (_,ts) = type_of T
    1.62        in
    1.63 -	  if isMeta x then (UVar(make_schematic_var(x,0),folType), ts)
    1.64 -	  else (Fun(make_fixed_var x, [], []), ts)  (*Frees don't need types!*)
    1.65 +	  if isMeta x then (UVar(make_schematic_var(x,0)), ts)
    1.66 +	  else (Fun(make_fixed_var x, [], []), ts)
    1.67        end
    1.68    | term_of app = 
    1.69        let val (f,args) = strip_comb app
    1.70 @@ -340,11 +332,9 @@
    1.71  
    1.72  (*Create a predicate value, again accumulating sort constraints.*)    
    1.73  fun pred_of (Const("op =", typ), args) =
    1.74 -      let val arg_typ = eq_arg_type typ 
    1.75 -	  val (args',ts) = terms_of args
    1.76 -	  val equal_name = make_fixed_const "op ="
    1.77 +      let val (args',ts) = terms_of args
    1.78        in
    1.79 -	  (Predicate(equal_name,[arg_typ],args'),
    1.80 +	  (Predicate(make_fixed_const "op =", [], args'),
    1.81  	   union_all ts)
    1.82        end
    1.83    | pred_of (pred,args) = 
    1.84 @@ -595,7 +585,7 @@
    1.85    | add_foltype_funcs (Comp(a,tys), funcs) = 
    1.86        foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys;
    1.87  
    1.88 -fun add_folterm_funcs (UVar(_,ty), funcs) = add_foltype_funcs (ty, funcs)
    1.89 +fun add_folterm_funcs (UVar _, funcs) = funcs
    1.90    | add_folterm_funcs (Fun(a,tys,tms), funcs) = 
    1.91        foldl add_foltype_funcs 
    1.92  	    (foldl add_folterm_funcs (Symtab.update (a, length tys + length tms) funcs) 
    1.93 @@ -629,7 +619,7 @@
    1.94  
    1.95  (**** String-oriented operations ****)
    1.96  
    1.97 -fun string_of_term (UVar(x,_)) = x
    1.98 +fun string_of_term (UVar x) = x
    1.99    | string_of_term (Fun (name,typs,terms)) = 
   1.100        name ^ (paren_pack (map string_of_term terms @ map string_of_fol_type typs));
   1.101  
   1.102 @@ -688,7 +678,7 @@
   1.103    let val Predicate (_, _, folterms) = pred
   1.104    in  folterms  end
   1.105  
   1.106 -fun get_uvars (UVar(a,typ)) = [a] 
   1.107 +fun get_uvars (UVar a) = [a] 
   1.108    | get_uvars (Fun (_,typ,tlist)) = union_all(map get_uvars tlist)
   1.109  
   1.110  fun dfg_vars (Clause {literals,...}) =