src/HOL/Tools/res_clause.ML
changeset 24310 af4af9993922
parent 24183 a46b758941a4
child 24322 dc7336b8c54c
     1.1 --- a/src/HOL/Tools/res_clause.ML	Fri Aug 17 23:10:39 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Fri Aug 17 23:10:41 2007 +0200
     1.3 @@ -2,72 +2,93 @@
     1.4      ID: $Id$
     1.5      Copyright 2004 University of Cambridge
     1.6  
     1.7 -ML data structure for storing/printing FOL clauses and arity clauses.
     1.8 +Storing/printing FOL clauses and arity clauses.
     1.9  Typed equality is treated differently.
    1.10  *)
    1.11  
    1.12 -(*FIXME: is this signature necessary? Or maybe define and open a Basic_ResClause?*)
    1.13  (*FIXME: combine with res_hol_clause!*)
    1.14  signature RES_CLAUSE =
    1.15 -  sig
    1.16 -  exception CLAUSE of string * term
    1.17 -  type arityClause and classrelClause
    1.18 -  datatype fol_type = AtomV of string
    1.19 -                    | AtomF of string
    1.20 -                    | Comp of string * fol_type list;
    1.21 -  datatype kind = Axiom | Conjecture;
    1.22 -  val name_of_kind : kind -> string
    1.23 -  type typ_var and type_literal 
    1.24 -  val add_typs_aux : (typ_var * string list) list -> type_literal list * type_literal list
    1.25 -  val ascii_of : string -> string
    1.26 -  val tptp_pack : string list -> string
    1.27 -  val make_arity_clauses: theory -> (class list * arityClause list)
    1.28 -  val make_classrel_clauses: theory -> class list -> class list -> classrelClause list 
    1.29 -  val clause_prefix : string 
    1.30 -  val const_prefix : string
    1.31 -  val fixed_var_prefix : string
    1.32 -  val gen_tptp_cls : int * string * string * string list -> string
    1.33 -  val init : theory -> unit
    1.34 -  val isMeta : string -> bool
    1.35 -  val make_fixed_const : string -> string		
    1.36 -  val make_fixed_type_const : string -> string   
    1.37 -  val make_fixed_type_var : string -> string
    1.38 +sig
    1.39 +  val schematic_var_prefix: string
    1.40 +  val fixed_var_prefix: string
    1.41 +  val tvar_prefix: string
    1.42 +  val tfree_prefix: string
    1.43 +  val clause_prefix: string
    1.44 +  val const_prefix: string
    1.45 +  val tconst_prefix: string
    1.46 +  val class_prefix: string
    1.47 +  val union_all: ''a list list -> ''a list
    1.48 +  val const_trans_table: string Symtab.table
    1.49 +  val type_const_trans_table: string Symtab.table
    1.50 +  val ascii_of: string -> string
    1.51 +  val undo_ascii_of: string -> string
    1.52 +  val paren_pack : string list -> string
    1.53 +  val make_schematic_var : string * int -> string
    1.54    val make_fixed_var : string -> string
    1.55    val make_schematic_type_var : string * int -> string
    1.56 -  val make_schematic_var : string * int -> string
    1.57 +  val make_fixed_type_var : string -> string
    1.58 +  val dfg_format: bool ref
    1.59 +  val make_fixed_const : string -> string
    1.60 +  val make_fixed_type_const : string -> string
    1.61    val make_type_class : string -> string
    1.62 -  val mk_typ_var_sort : Term.typ -> typ_var * sort
    1.63 -  val paren_pack : string list -> string
    1.64 -  val schematic_var_prefix : string
    1.65 +  datatype kind = Axiom | Conjecture
    1.66 +  val name_of_kind : kind -> string
    1.67 +  type axiom_name = string
    1.68 +  datatype typ_var = FOLTVar of indexname | FOLTFree of string
    1.69 +  datatype fol_type =
    1.70 +      AtomV of string
    1.71 +    | AtomF of string
    1.72 +    | Comp of string * fol_type list
    1.73    val string_of_fol_type : fol_type -> string
    1.74 -  val tconst_prefix : string 
    1.75 -  val tfree_prefix : string
    1.76 -  val tvar_prefix : string
    1.77 -  val tptp_arity_clause : arityClause -> string
    1.78 -  val tptp_classrelClause : classrelClause -> string
    1.79 -  val tptp_of_typeLit : type_literal -> string
    1.80 -  val tptp_tfree_clause : string -> string
    1.81 -  val union_all : ''a list list -> ''a list
    1.82 -  val writeln_strs: TextIO.outstream -> TextIO.vector list -> unit
    1.83 +  datatype type_literal = LTVar of string * string | LTFree of string * string
    1.84 +  val mk_typ_var_sort: typ -> typ_var * sort
    1.85 +  exception CLAUSE of string * term
    1.86 +  val init : theory -> unit
    1.87 +  val isMeta : string -> bool
    1.88 +  val add_typs_aux : (typ_var * string list) list -> type_literal list * type_literal list
    1.89 +  val get_tvar_strs: (typ_var * sort) list -> string list
    1.90 +  datatype arLit =
    1.91 +      TConsLit of class * string * string list
    1.92 +    | TVarLit of class * string
    1.93 +  datatype arityClause = ArityClause of
    1.94 +   {axiom_name: axiom_name,
    1.95 +    kind: kind,
    1.96 +    conclLit: arLit,
    1.97 +    premLits: arLit list}
    1.98 +  datatype classrelClause = ClassrelClause of
    1.99 +   {axiom_name: axiom_name,
   1.100 +    subclass: class,
   1.101 +    superclass: class}
   1.102 +  val make_classrel_clauses: theory -> class list -> class list -> classrelClause list
   1.103 +  val make_arity_clauses: theory -> string list -> class list -> class list * arityClause list
   1.104 +  val add_type_sort_preds: (typ_var * string list) * int Symtab.table -> int Symtab.table
   1.105 +  val add_classrelClause_preds : classrelClause * int Symtab.table -> int Symtab.table
   1.106 +  val class_of_arityLit: arLit -> class
   1.107 +  val add_arityClause_preds: arityClause * int Symtab.table -> int Symtab.table
   1.108 +  val add_foltype_funcs: fol_type * int Symtab.table -> int Symtab.table
   1.109 +  val add_arityClause_funcs: arityClause * int Symtab.table -> int Symtab.table
   1.110 +  val init_functab: int Symtab.table
   1.111 +  val writeln_strs: TextIO.outstream -> string list -> unit
   1.112    val dfg_sign: bool -> string -> string
   1.113    val dfg_of_typeLit: type_literal -> string
   1.114 -  val get_tvar_strs: (typ_var * sort) list -> string list
   1.115    val gen_dfg_cls: int * string * string * string * string list -> string
   1.116 -  val add_foltype_funcs: fol_type * int Symtab.table -> int Symtab.table
   1.117 -  val add_arityClause_funcs: arityClause * int Symtab.table -> int Symtab.table
   1.118 -  val add_arityClause_preds: arityClause * int Symtab.table -> int Symtab.table
   1.119 -  val add_classrelClause_preds : classrelClause * int Symtab.table -> int Symtab.table
   1.120 -  val dfg_tfree_clause : string -> string
   1.121 +  val string_of_preds: (string * Int.int) list -> string
   1.122 +  val string_of_funcs: (string * int) list -> string
   1.123 +  val string_of_symbols: string -> string -> string
   1.124    val string_of_start: string -> string
   1.125    val string_of_descrip : string -> string
   1.126 -  val string_of_symbols: string -> string -> string
   1.127 -  val string_of_funcs: (string * int) list -> string
   1.128 -  val string_of_preds: (string * Int.int) list -> string
   1.129 +  val dfg_tfree_clause : string -> string
   1.130    val dfg_classrelClause: classrelClause -> string
   1.131    val dfg_arity_clause: arityClause -> string
   1.132 -end;
   1.133 +  val tptp_sign: bool -> string -> string
   1.134 +  val tptp_of_typeLit : type_literal -> string
   1.135 +  val gen_tptp_cls : int * string * kind * string list -> string
   1.136 +  val tptp_tfree_clause : string -> string
   1.137 +  val tptp_arity_clause : arityClause -> string
   1.138 +  val tptp_classrelClause : classrelClause -> string
   1.139 +end
   1.140  
   1.141 -structure ResClause =
   1.142 +structure ResClause: RES_CLAUSE =
   1.143  struct
   1.144  
   1.145  val schematic_var_prefix = "V_";
   1.146 @@ -76,48 +97,48 @@
   1.147  val tvar_prefix = "T_";
   1.148  val tfree_prefix = "t_";
   1.149  
   1.150 -val clause_prefix = "cls_"; 
   1.151 -val arclause_prefix = "clsarity_" 
   1.152 +val clause_prefix = "cls_";
   1.153 +val arclause_prefix = "clsarity_"
   1.154  val clrelclause_prefix = "clsrel_";
   1.155  
   1.156  val const_prefix = "c_";
   1.157 -val tconst_prefix = "tc_"; 
   1.158 -val class_prefix = "class_"; 
   1.159 +val tconst_prefix = "tc_";
   1.160 +val class_prefix = "class_";
   1.161  
   1.162  fun union_all xss = foldl (op union) [] xss;
   1.163  
   1.164  (*Provide readable names for the more common symbolic functions*)
   1.165  val const_trans_table =
   1.166        Symtab.make [("op =", "equal"),
   1.167 -	  	   (@{const_name HOL.less_eq}, "lessequals"),
   1.168 -		   (@{const_name HOL.less}, "less"),
   1.169 -		   ("op &", "and"),
   1.170 -		   ("op |", "or"),
   1.171 -		   (@{const_name HOL.plus}, "plus"),
   1.172 -		   (@{const_name HOL.minus}, "minus"),
   1.173 -		   (@{const_name HOL.times}, "times"),
   1.174 -		   (@{const_name Divides.div}, "div"),
   1.175 -		   (@{const_name HOL.divide}, "divide"),
   1.176 -		   ("op -->", "implies"),
   1.177 -		   ("{}", "emptyset"),
   1.178 -		   ("op :", "in"),
   1.179 -		   ("op Un", "union"),
   1.180 -		   ("op Int", "inter"),
   1.181 -		   ("List.append", "append"),
   1.182 -		   ("ATP_Linkup.fequal", "fequal"),
   1.183 -		   ("ATP_Linkup.COMBI", "COMBI"),
   1.184 -		   ("ATP_Linkup.COMBK", "COMBK"),
   1.185 -		   ("ATP_Linkup.COMBB", "COMBB"),
   1.186 -		   ("ATP_Linkup.COMBC", "COMBC"),
   1.187 -		   ("ATP_Linkup.COMBS", "COMBS"),
   1.188 -		   ("ATP_Linkup.COMBB'", "COMBB_e"),
   1.189 -		   ("ATP_Linkup.COMBC'", "COMBC_e"),
   1.190 -		   ("ATP_Linkup.COMBS'", "COMBS_e")];
   1.191 +                   (@{const_name HOL.less_eq}, "lessequals"),
   1.192 +                   (@{const_name HOL.less}, "less"),
   1.193 +                   ("op &", "and"),
   1.194 +                   ("op |", "or"),
   1.195 +                   (@{const_name HOL.plus}, "plus"),
   1.196 +                   (@{const_name HOL.minus}, "minus"),
   1.197 +                   (@{const_name HOL.times}, "times"),
   1.198 +                   (@{const_name Divides.div}, "div"),
   1.199 +                   (@{const_name HOL.divide}, "divide"),
   1.200 +                   ("op -->", "implies"),
   1.201 +                   ("{}", "emptyset"),
   1.202 +                   ("op :", "in"),
   1.203 +                   ("op Un", "union"),
   1.204 +                   ("op Int", "inter"),
   1.205 +                   ("List.append", "append"),
   1.206 +                   ("ATP_Linkup.fequal", "fequal"),
   1.207 +                   ("ATP_Linkup.COMBI", "COMBI"),
   1.208 +                   ("ATP_Linkup.COMBK", "COMBK"),
   1.209 +                   ("ATP_Linkup.COMBB", "COMBB"),
   1.210 +                   ("ATP_Linkup.COMBC", "COMBC"),
   1.211 +                   ("ATP_Linkup.COMBS", "COMBS"),
   1.212 +                   ("ATP_Linkup.COMBB'", "COMBB_e"),
   1.213 +                   ("ATP_Linkup.COMBC'", "COMBC_e"),
   1.214 +                   ("ATP_Linkup.COMBS'", "COMBS_e")];
   1.215  
   1.216  val type_const_trans_table =
   1.217        Symtab.make [("*", "prod"),
   1.218 -	  	   ("+", "sum"),
   1.219 -		   ("~=>", "map")];
   1.220 +                   ("+", "sum"),
   1.221 +                   ("~=>", "map")];
   1.222  
   1.223  (*Escaping of special characters.
   1.224    Alphanumeric characters are left unchanged.
   1.225 @@ -132,9 +153,9 @@
   1.226  fun ascii_of_c c =
   1.227    if Char.isAlphaNum c then String.str c
   1.228    else if c = #"_" then "__"
   1.229 -  else if #" " <= c andalso c <= #"/" 
   1.230 +  else if #" " <= c andalso c <= #"/"
   1.231         then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
   1.232 -  else if Char.isPrint c 
   1.233 +  else if Char.isPrint c
   1.234         then ("_" ^ stringN_of_int 3 (Char.ord c))  (*fixed width, in case more digits follow*)
   1.235    else ""
   1.236  
   1.237 @@ -148,12 +169,12 @@
   1.238    | undo_ascii_aux rcs [#"_"] = undo_ascii_aux (#"_"::rcs) []  (*ERROR*)
   1.239        (*Three types of _ escapes: __, _A to _P, _nnn*)
   1.240    | undo_ascii_aux rcs (#"_" :: #"_" :: cs) = undo_ascii_aux (#"_"::rcs) cs
   1.241 -  | undo_ascii_aux rcs (#"_" :: c :: cs) = 
   1.242 +  | undo_ascii_aux rcs (#"_" :: c :: cs) =
   1.243        if #"A" <= c andalso c<= #"P"  (*translation of #" " to #"/"*)
   1.244        then undo_ascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
   1.245 -      else 
   1.246 +      else
   1.247          let val digits = List.take (c::cs, 3) handle Subscript => []
   1.248 -        in  
   1.249 +        in
   1.250              case Int.fromString (String.implode digits) of
   1.251                  NONE => undo_ascii_aux (c:: #"_"::rcs) cs  (*ERROR*)
   1.252                | SOME n => undo_ascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
   1.253 @@ -181,7 +202,7 @@
   1.254  fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v);
   1.255  fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x);
   1.256  
   1.257 -fun make_schematic_type_var (x,i) = 
   1.258 +fun make_schematic_type_var (x,i) =
   1.259        tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
   1.260  fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
   1.261  
   1.262 @@ -190,7 +211,7 @@
   1.263  
   1.264  (*32-bit hash,so we expect no collisions unless there are around 65536 long identifiers...*)
   1.265  fun controlled_length s =
   1.266 -  if size s > 60 andalso !dfg_format   
   1.267 +  if size s > 60 andalso !dfg_format
   1.268    then Word.toString (Polyhash.hashw_string(s,0w0))
   1.269    else s;
   1.270  
   1.271 @@ -199,7 +220,7 @@
   1.272          SOME c' => c'
   1.273        | NONE => controlled_length (ascii_of c);
   1.274  
   1.275 -fun lookup_type_const c = 
   1.276 +fun lookup_type_const c =
   1.277      case Symtab.lookup type_const_trans_table c of
   1.278          SOME c' => c'
   1.279        | NONE => controlled_length (ascii_of c);
   1.280 @@ -227,14 +248,14 @@
   1.281  
   1.282  (*FIXME: give the constructors more sensible names*)
   1.283  datatype fol_type = AtomV of string
   1.284 -		  | AtomF of string
   1.285 -		  | Comp of string * fol_type list;
   1.286 +                  | AtomF of string
   1.287 +                  | Comp of string * fol_type list;
   1.288  
   1.289  fun string_of_fol_type (AtomV x) = x
   1.290    | string_of_fol_type (AtomF x) = x
   1.291 -  | string_of_fol_type (Comp(tcon,tps)) = 
   1.292 +  | string_of_fol_type (Comp(tcon,tps)) =
   1.293        tcon ^ (paren_pack (map string_of_fol_type tps));
   1.294 -      
   1.295 +
   1.296  (*First string is the type class; the second is a TVar or TFfree*)
   1.297  datatype type_literal = LTVar of string * string | LTFree of string * string;
   1.298  
   1.299 @@ -253,30 +274,28 @@
   1.300  (*Initialize the type suppression mechanism with the current theory before
   1.301      producing any clauses!*)
   1.302  fun init thy = (const_typargs := Sign.const_typargs thy);
   1.303 -    
   1.304 +
   1.305  
   1.306  (*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and
   1.307 -  TVars it contains.*)    
   1.308 -fun type_of (Type (a, Ts)) = 
   1.309 -      let val (folTyps, ts) = types_of Ts 
   1.310 -	  val t = make_fixed_type_const a
   1.311 +  TVars it contains.*)
   1.312 +fun type_of (Type (a, Ts)) =
   1.313 +      let val (folTyps, ts) = types_of Ts
   1.314 +          val t = make_fixed_type_const a
   1.315        in (Comp(t,folTyps), ts) end
   1.316 -  | type_of (TFree (a,s)) = (AtomF(make_fixed_type_var a), [(FOLTFree a, s)]) 
   1.317 +  | type_of (TFree (a,s)) = (AtomF(make_fixed_type_var a), [(FOLTFree a, s)])
   1.318    | type_of (TVar (v, s)) = (AtomV(make_schematic_type_var v), [(FOLTVar v, s)])
   1.319  and types_of Ts =
   1.320        let val (folTyps,ts) = ListPair.unzip (map type_of Ts)
   1.321        in (folTyps, union_all ts) end;
   1.322  
   1.323  
   1.324 -fun const_types_of (c,T) = types_of (!const_typargs (c,T));
   1.325 -
   1.326  (* Any variables created via the METAHYPS tactical should be treated as
   1.327     universal vars, although it is represented as "Free(...)" by Isabelle *)
   1.328  val isMeta = String.isPrefix "METAHYP1_"
   1.329  
   1.330 -(*Make literals for sorted type variables*) 
   1.331 +(*Make literals for sorted type variables*)
   1.332  fun sorts_on_typs (_, [])   = []
   1.333 -  | sorts_on_typs (v,  s::ss) = 
   1.334 +  | sorts_on_typs (v,  s::ss) =
   1.335        let val sorts = sorts_on_typs (v, ss)
   1.336        in
   1.337            if s = "HOL.type" then sorts
   1.338 @@ -291,40 +310,37 @@
   1.339  (*Given a list of sorted type variables, return two separate lists.
   1.340    The first is for TVars, the second for TFrees.*)
   1.341  fun add_typs_aux [] = ([],[])
   1.342 -  | add_typs_aux ((FOLTVar indx, s) :: tss) = 
   1.343 +  | add_typs_aux ((FOLTVar indx, s) :: tss) =
   1.344        let val vs = sorts_on_typs (FOLTVar indx, s)
   1.345 -	  val (vss,fss) = add_typs_aux tss
   1.346 +          val (vss,fss) = add_typs_aux tss
   1.347        in  (vs union vss, fss)  end
   1.348    | add_typs_aux ((FOLTFree x, s) :: tss) =
   1.349        let val fs = sorts_on_typs (FOLTFree x, s)
   1.350 -	  val (vss,fss) = add_typs_aux tss
   1.351 +          val (vss,fss) = add_typs_aux tss
   1.352        in  (vss, fs union fss)  end;
   1.353  
   1.354  
   1.355  (** make axiom and conjecture clauses. **)
   1.356  
   1.357  fun get_tvar_strs [] = []
   1.358 -  | get_tvar_strs ((FOLTVar indx,s)::tss) = 
   1.359 +  | get_tvar_strs ((FOLTVar indx,s)::tss) =
   1.360        insert (op =) (make_schematic_type_var indx) (get_tvar_strs tss)
   1.361    | get_tvar_strs((FOLTFree x,s)::tss) = get_tvar_strs tss
   1.362  
   1.363 -    
   1.364 +
   1.365  
   1.366  (**** Isabelle arities ****)
   1.367  
   1.368  exception ARCLAUSE of string;
   1.369 - 
   1.370 -type class = string; 
   1.371 -type tcons = string; 
   1.372  
   1.373 -datatype arLit = TConsLit of class * tcons * string list
   1.374 +datatype arLit = TConsLit of class * string * string list
   1.375                 | TVarLit of class * string;
   1.376 - 
   1.377 -datatype arityClause =  
   1.378 -	 ArityClause of {axiom_name: axiom_name,
   1.379 -			 kind: kind,
   1.380 -			 conclLit: arLit,
   1.381 -			 premLits: arLit list};
   1.382 +
   1.383 +datatype arityClause =
   1.384 +         ArityClause of {axiom_name: axiom_name,
   1.385 +                         kind: kind,
   1.386 +                         conclLit: arLit,
   1.387 +                         premLits: arLit list};
   1.388  
   1.389  
   1.390  fun gen_TVars 0 = []
   1.391 @@ -333,37 +349,37 @@
   1.392  fun pack_sort(_,[])  = []
   1.393    | pack_sort(tvar, "HOL.type"::srt) = pack_sort(tvar, srt)   (*IGNORE sort "type"*)
   1.394    | pack_sort(tvar, cls::srt) =  (cls, tvar) :: pack_sort(tvar, srt);
   1.395 -    
   1.396 +
   1.397  (*Arity of type constructor tcon :: (arg1,...,argN)res*)
   1.398  fun make_axiom_arity_clause (tcons, axiom_name, (cls,args)) =
   1.399     let val tvars = gen_TVars (length args)
   1.400         val tvars_srts = ListPair.zip (tvars,args)
   1.401     in
   1.402 -      ArityClause {axiom_name = axiom_name, kind = Axiom, 
   1.403 -                   conclLit = TConsLit (cls, make_fixed_type_const tcons, tvars), 
   1.404 +      ArityClause {axiom_name = axiom_name, kind = Axiom,
   1.405 +                   conclLit = TConsLit (cls, make_fixed_type_const tcons, tvars),
   1.406                     premLits = map TVarLit (union_all(map pack_sort tvars_srts))}
   1.407     end;
   1.408  
   1.409  
   1.410  (**** Isabelle class relations ****)
   1.411  
   1.412 -datatype classrelClause = 
   1.413 -	 ClassrelClause of {axiom_name: axiom_name,
   1.414 -			    subclass: class,
   1.415 -			    superclass: class};
   1.416 - 
   1.417 +datatype classrelClause =
   1.418 +         ClassrelClause of {axiom_name: axiom_name,
   1.419 +                            subclass: class,
   1.420 +                            superclass: class};
   1.421 +
   1.422  (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
   1.423  fun class_pairs thy [] supers = []
   1.424    | class_pairs thy subs supers =
   1.425        let val class_less = Sorts.class_less(Sign.classes_of thy)
   1.426 -	  fun add_super sub (super,pairs) = 
   1.427 -		if class_less (sub,super) then (sub,super)::pairs else pairs
   1.428 -	  fun add_supers (sub,pairs) = foldl (add_super sub) pairs supers
   1.429 +          fun add_super sub (super,pairs) =
   1.430 +                if class_less (sub,super) then (sub,super)::pairs else pairs
   1.431 +          fun add_supers (sub,pairs) = foldl (add_super sub) pairs supers
   1.432        in  foldl add_supers [] subs  end;
   1.433  
   1.434  fun make_classrelClause (sub,super) =
   1.435    ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super,
   1.436 -                  subclass = make_type_class sub, 
   1.437 +                  subclass = make_type_class sub,
   1.438                    superclass = make_type_class super};
   1.439  
   1.440  fun make_classrel_clauses thy subs supers =
   1.441 @@ -377,23 +393,23 @@
   1.442        arity_clause seen n (tcons,ars)
   1.443    | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
   1.444        if class mem_string seen then (*multiple arities for the same tycon, class pair*)
   1.445 -	  make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) :: 
   1.446 -	  arity_clause seen (n+1) (tcons,ars)
   1.447 +          make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
   1.448 +          arity_clause seen (n+1) (tcons,ars)
   1.449        else
   1.450 -	  make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class, ar) :: 
   1.451 -	  arity_clause (class::seen) n (tcons,ars)
   1.452 +          make_axiom_arity_clause (tcons, lookup_type_const tcons ^ "_" ^ class, ar) ::
   1.453 +          arity_clause (class::seen) n (tcons,ars)
   1.454  
   1.455  fun multi_arity_clause [] = []
   1.456    | multi_arity_clause ((tcons,ars) :: tc_arlists) =
   1.457 -      arity_clause [] 1 (tcons, ars)  @  multi_arity_clause tc_arlists 
   1.458 +      arity_clause [] 1 (tcons, ars)  @  multi_arity_clause tc_arlists
   1.459  
   1.460  (*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
   1.461    provided its arguments have the corresponding sorts.*)
   1.462  fun type_class_pairs thy tycons classes =
   1.463    let val alg = Sign.classes_of thy
   1.464        fun domain_sorts (tycon,class) = Sorts.mg_domain alg tycon [class]
   1.465 -      fun add_class tycon (class,pairs) = 
   1.466 -            (class, domain_sorts(tycon,class))::pairs 
   1.467 +      fun add_class tycon (class,pairs) =
   1.468 +            (class, domain_sorts(tycon,class))::pairs
   1.469              handle Sorts.CLASS_ERROR _ => pairs
   1.470        fun try_classes tycon = (tycon, foldl (add_class tycon) [] classes)
   1.471    in  map try_classes tycons  end;
   1.472 @@ -403,24 +419,24 @@
   1.473    | iter_type_class_pairs thy tycons classes =
   1.474        let val cpairs = type_class_pairs thy tycons classes
   1.475            val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs))) \\ classes \\ HOLogic.typeS
   1.476 -          val _ = if null newclasses then () 
   1.477 +          val _ = if null newclasses then ()
   1.478                    else Output.debug (fn _ => "New classes: " ^ space_implode ", " newclasses)
   1.479 -          val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses  
   1.480 +          val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
   1.481        in  (classes' union classes, cpairs' union cpairs)  end;
   1.482 -      
   1.483 +
   1.484  fun make_arity_clauses thy tycons classes =
   1.485 -  let val (classes', cpairs) = iter_type_class_pairs thy tycons classes  
   1.486 +  let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
   1.487    in  (classes', multi_arity_clause cpairs)  end;
   1.488  
   1.489  
   1.490  (**** Find occurrences of predicates in clauses ****)
   1.491  
   1.492 -(*FIXME: multiple-arity checking doesn't work, as update_new is the wrong 
   1.493 +(*FIXME: multiple-arity checking doesn't work, as update_new is the wrong
   1.494    function (it flags repeated declarations of a function, even with the same arity)*)
   1.495  
   1.496  fun update_many (tab, keypairs) = foldl (uncurry Symtab.update) tab keypairs;
   1.497  
   1.498 -fun add_type_sort_preds ((FOLTVar indx,s), preds) = 
   1.499 +fun add_type_sort_preds ((FOLTVar indx,s), preds) =
   1.500        update_many (preds, map pred_of_sort (sorts_on_typs (FOLTVar indx, s)))
   1.501    | add_type_sort_preds ((FOLTFree x,s), preds) =
   1.502        update_many (preds, map pred_of_sort (sorts_on_typs (FOLTFree x, s)));
   1.503 @@ -440,12 +456,12 @@
   1.504  
   1.505  fun add_foltype_funcs (AtomV _, funcs) = funcs
   1.506    | add_foltype_funcs (AtomF a, funcs) = Symtab.update (a,0) funcs
   1.507 -  | add_foltype_funcs (Comp(a,tys), funcs) = 
   1.508 +  | add_foltype_funcs (Comp(a,tys), funcs) =
   1.509        foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys;
   1.510  
   1.511  (*TFrees are recorded as constants*)
   1.512  fun add_type_sort_funcs ((FOLTVar _, _), funcs) = funcs
   1.513 -  | add_type_sort_funcs ((FOLTFree a, _), funcs) = 
   1.514 +  | add_type_sort_funcs ((FOLTFree a, _), funcs) =
   1.515        Symtab.update (make_fixed_type_var a, 0) funcs
   1.516  
   1.517  fun add_arityClause_funcs (ArityClause {conclLit,...}, funcs) =
   1.518 @@ -458,32 +474,31 @@
   1.519  
   1.520  (**** String-oriented operations ****)
   1.521  
   1.522 -fun string_of_clausename (cls_id,ax_name) = 
   1.523 +fun string_of_clausename (cls_id,ax_name) =
   1.524      clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id;
   1.525  
   1.526 -fun string_of_type_clsname (cls_id,ax_name,idx) = 
   1.527 +fun string_of_type_clsname (cls_id,ax_name,idx) =
   1.528      string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
   1.529  
   1.530 -(*Write a list of strings to a file*)
   1.531 -fun writeln_strs os = List.app (fn s => TextIO.output (os,s));
   1.532 +fun writeln_strs os = List.app (fn s => TextIO.output (os, s));
   1.533  
   1.534 -    
   1.535 +
   1.536  (**** Producing DFG files ****)
   1.537  
   1.538  (*Attach sign in DFG syntax: false means negate.*)
   1.539  fun dfg_sign true s = s
   1.540 -  | dfg_sign false s = "not(" ^ s ^ ")"  
   1.541 +  | dfg_sign false s = "not(" ^ s ^ ")"
   1.542  
   1.543  fun dfg_of_typeLit (LTVar (s,ty)) = "not(" ^ s ^ "(" ^ ty ^ "))"
   1.544    | dfg_of_typeLit (LTFree (s,ty)) = s ^ "(" ^ ty ^ ")";
   1.545 - 
   1.546 +
   1.547  (*Enclose the clause body by quantifiers, if necessary*)
   1.548 -fun dfg_forall [] body = body  
   1.549 +fun dfg_forall [] body = body
   1.550    | dfg_forall vars body = "forall([" ^ commas vars ^ "],\n" ^ body ^ ")"
   1.551  
   1.552 -fun gen_dfg_cls (cls_id, ax_name, knd, lits, vars) = 
   1.553 -    "clause( %(" ^ knd ^ ")\n" ^ 
   1.554 -    dfg_forall vars ("or(" ^ lits ^ ")") ^ ",\n" ^ 
   1.555 +fun gen_dfg_cls (cls_id, ax_name, knd, lits, vars) =
   1.556 +    "clause( %(" ^ knd ^ ")\n" ^
   1.557 +    dfg_forall vars ("or(" ^ lits ^ ")") ^ ",\n" ^
   1.558      string_of_clausename (cls_id,ax_name) ^  ").\n\n";
   1.559  
   1.560  fun string_of_arity (name, num) =  "(" ^ name ^ "," ^ Int.toString num ^ ")"
   1.561 @@ -494,13 +509,13 @@
   1.562  fun string_of_funcs [] = ""
   1.563    | string_of_funcs funcs = "functions[" ^ commas(map string_of_arity funcs) ^ "].\n" ;
   1.564  
   1.565 -fun string_of_symbols predstr funcstr = 
   1.566 +fun string_of_symbols predstr funcstr =
   1.567    "list_of_symbols.\n" ^ predstr  ^ funcstr  ^ "end_of_list.\n\n";
   1.568  
   1.569  fun string_of_start name = "begin_problem(" ^ name ^ ").\n\n";
   1.570  
   1.571 -fun string_of_descrip name = 
   1.572 -  "list_of_descriptions.\nname({*" ^ name ^ 
   1.573 +fun string_of_descrip name =
   1.574 +  "list_of_descriptions.\nname({*" ^ name ^
   1.575    "*}).\nauthor({*Isabelle*}).\nstatus(unknown).\ndescription({*auto-generated*}).\nend_of_list.\n\n"
   1.576  
   1.577  fun dfg_tfree_clause tfree_lit =
   1.578 @@ -510,20 +525,20 @@
   1.579        dfg_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
   1.580    | dfg_of_arLit (TVarLit (c,str)) =
   1.581        dfg_sign false (make_type_class c ^ "(" ^ str ^ ")")
   1.582 -    
   1.583 +
   1.584  fun dfg_classrelLits sub sup =  "not(" ^ sub ^ "(T)), " ^ sup ^ "(T)";
   1.585  
   1.586  fun dfg_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) =
   1.587    "clause(forall([T],\nor( " ^ dfg_classrelLits subclass superclass ^ ")),\n" ^
   1.588    axiom_name ^ ").\n\n";
   1.589 -      
   1.590 +
   1.591  fun string_of_ar axiom_name = arclause_prefix ^ ascii_of axiom_name;
   1.592  
   1.593 -fun dfg_arity_clause (ArityClause{axiom_name,kind,conclLit,premLits,...}) = 
   1.594 +fun dfg_arity_clause (ArityClause{axiom_name,kind,conclLit,premLits,...}) =
   1.595    let val TConsLit (_,_,tvars) = conclLit
   1.596        val lits = map dfg_of_arLit (conclLit :: premLits)
   1.597    in
   1.598 -      "clause( %(" ^ name_of_kind kind ^ ")\n" ^ 
   1.599 +      "clause( %(" ^ name_of_kind kind ^ ")\n" ^
   1.600        dfg_forall tvars ("or( " ^ commas lits ^ ")") ^ ",\n" ^
   1.601        string_of_ar axiom_name ^ ").\n\n"
   1.602    end;
   1.603 @@ -537,28 +552,28 @@
   1.604  
   1.605  fun tptp_of_typeLit (LTVar (s,ty))  = tptp_sign false (s ^ "(" ^ ty ^ ")")
   1.606    | tptp_of_typeLit (LTFree (s,ty)) = tptp_sign true  (s ^ "(" ^ ty ^ ")");
   1.607 - 
   1.608 -fun gen_tptp_cls (cls_id,ax_name,knd,lits) = 
   1.609 -    "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^ 
   1.610 +
   1.611 +fun gen_tptp_cls (cls_id,ax_name,knd,lits) =
   1.612 +    "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^
   1.613      name_of_kind knd ^ "," ^ tptp_pack lits ^ ").\n";
   1.614  
   1.615  fun tptp_tfree_clause tfree_lit =
   1.616      "cnf(" ^ "tfree_tcs," ^ "negated_conjecture" ^ "," ^ tptp_pack[tfree_lit] ^ ").\n";
   1.617 -    
   1.618 +
   1.619  fun tptp_of_arLit (TConsLit (c,t,args)) =
   1.620        tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
   1.621    | tptp_of_arLit (TVarLit (c,str)) =
   1.622        tptp_sign false (make_type_class c ^ "(" ^ str ^ ")")
   1.623 -    
   1.624 -fun tptp_arity_clause (ArityClause{axiom_name,kind,conclLit,premLits,...}) = 
   1.625 -  "cnf(" ^ string_of_ar axiom_name ^ "," ^ name_of_kind kind ^ "," ^ 
   1.626 +
   1.627 +fun tptp_arity_clause (ArityClause{axiom_name,kind,conclLit,premLits,...}) =
   1.628 +  "cnf(" ^ string_of_ar axiom_name ^ "," ^ name_of_kind kind ^ "," ^
   1.629    tptp_pack (map tptp_of_arLit (conclLit :: premLits)) ^ ").\n";
   1.630  
   1.631 -fun tptp_classrelLits sub sup = 
   1.632 +fun tptp_classrelLits sub sup =
   1.633    let val tvar = "(T)"
   1.634    in  tptp_pack [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)]  end;
   1.635  
   1.636  fun tptp_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) =
   1.637 -  "cnf(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n" 
   1.638 +  "cnf(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n"
   1.639  
   1.640  end;