Added functions for fol_type; also put some functions to the signature, used by ResHolClause.
authormengj
Tue Dec 20 04:27:46 2005 +0100 (2005-12-20)
changeset 184394b517881ac7e
parent 18438 b8d867177916
child 18440 72ee07f4b56b
Added functions for fol_type; also put some functions to the signature, used by ResHolClause.
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/res_clause.ML	Mon Dec 19 16:07:19 2005 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Tue Dec 20 04:27:46 2005 +0100
     1.3 @@ -73,6 +73,14 @@
     1.4    val clause_eq : clause * clause -> bool
     1.5    val hash1_clause : clause -> word
     1.6  
     1.7 +  val list_ord : ('a * 'b -> order) -> 'a list * 'b list -> order
     1.8 +  type fol_type
     1.9 +  val types_ord : fol_type list * fol_type list -> order
    1.10 +  val string_of_fol_type : fol_type -> string
    1.11 +  val mk_fol_type: string * string * fol_type list -> fol_type
    1.12 +  val types_eq :fol_type list * fol_type list ->
    1.13 +   (string * string) list * (string * string) list -> bool * ((string * string) list * (string * string) list)
    1.14 +  val check_var_pairs: ''a * ''b -> (''a * ''b) list -> int
    1.15    end;
    1.16  
    1.17  structure ResClause : RES_CLAUSE =
    1.18 @@ -233,6 +241,11 @@
    1.19  	tcon ^ (paren_pack tstrs)
    1.20      end;
    1.21  
    1.22 +fun mk_fol_type ("Var",x,_) = AtomV(x)
    1.23 +  | mk_fol_type ("Fixed",x,_) = AtomF(x)
    1.24 +  | mk_fol_type ("Comp",con,args) = Comp(con,args)
    1.25 +
    1.26 +
    1.27  
    1.28  datatype type_literal = LTVar of string | LTFree of string;
    1.29  
    1.30 @@ -342,6 +355,7 @@
    1.31        end;
    1.32  
    1.33  
    1.34 +
    1.35  fun const_types_of (c,T) = types_of (!const_typargs (c,T));
    1.36  
    1.37  (* Any variables created via the METAHYPS tactical should be treated as