src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
changeset 35825 a6aad5a70ed4
parent 35092 cfe605c54e50
child 35826 1590abc3d42a
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Wed Mar 17 18:16:31 2010 +0100
     1.3 @@ -0,0 +1,534 @@
     1.4 +(*  Title:      HOL/Tools/res_clause.ML
     1.5 +    Author:     Jia Meng, Cambridge University Computer Laboratory
     1.6 +
     1.7 +Storing/printing FOL clauses and arity clauses.  Typed equality is
     1.8 +treated differently.
     1.9 +
    1.10 +FIXME: combine with res_hol_clause!
    1.11 +*)
    1.12 +
    1.13 +signature RES_CLAUSE =
    1.14 +sig
    1.15 +  val schematic_var_prefix: string
    1.16 +  val fixed_var_prefix: string
    1.17 +  val tvar_prefix: string
    1.18 +  val tfree_prefix: string
    1.19 +  val clause_prefix: string
    1.20 +  val const_prefix: string
    1.21 +  val tconst_prefix: string
    1.22 +  val class_prefix: string
    1.23 +  val union_all: ''a list list -> ''a list
    1.24 +  val const_trans_table: string Symtab.table
    1.25 +  val type_const_trans_table: string Symtab.table
    1.26 +  val ascii_of: string -> string
    1.27 +  val undo_ascii_of: string -> string
    1.28 +  val paren_pack : string list -> string
    1.29 +  val make_schematic_var : string * int -> string
    1.30 +  val make_fixed_var : string -> string
    1.31 +  val make_schematic_type_var : string * int -> string
    1.32 +  val make_fixed_type_var : string -> string
    1.33 +  val make_fixed_const : bool -> string -> string
    1.34 +  val make_fixed_type_const : bool -> string -> string
    1.35 +  val make_type_class : string -> string
    1.36 +  datatype kind = Axiom | Conjecture
    1.37 +  type axiom_name = string
    1.38 +  datatype fol_type =
    1.39 +      AtomV of string
    1.40 +    | AtomF of string
    1.41 +    | Comp of string * fol_type list
    1.42 +  val string_of_fol_type : fol_type -> string
    1.43 +  datatype type_literal = LTVar of string * string | LTFree of string * string
    1.44 +  exception CLAUSE of string * term
    1.45 +  val add_typs : typ list -> type_literal list
    1.46 +  val get_tvar_strs: typ list -> string list
    1.47 +  datatype arLit =
    1.48 +      TConsLit of class * string * string list
    1.49 +    | TVarLit of class * string
    1.50 +  datatype arityClause = ArityClause of
    1.51 +   {axiom_name: axiom_name, conclLit: arLit, premLits: arLit list}
    1.52 +  datatype classrelClause = ClassrelClause of
    1.53 +   {axiom_name: axiom_name, subclass: class, superclass: class}
    1.54 +  val make_classrel_clauses: theory -> class list -> class list -> classrelClause list
    1.55 +  val make_arity_clauses_dfg: bool -> theory -> string list -> class list -> class list * arityClause list
    1.56 +  val make_arity_clauses: theory -> string list -> class list -> class list * arityClause list
    1.57 +  val add_type_sort_preds: typ * int Symtab.table -> int Symtab.table
    1.58 +  val add_classrelClause_preds : classrelClause * int Symtab.table -> int Symtab.table
    1.59 +  val class_of_arityLit: arLit -> class
    1.60 +  val add_arityClause_preds: arityClause * int Symtab.table -> int Symtab.table
    1.61 +  val add_foltype_funcs: fol_type * int Symtab.table -> int Symtab.table
    1.62 +  val add_arityClause_funcs: arityClause * int Symtab.table -> int Symtab.table
    1.63 +  val init_functab: int Symtab.table
    1.64 +  val dfg_sign: bool -> string -> string
    1.65 +  val dfg_of_typeLit: bool -> type_literal -> string
    1.66 +  val gen_dfg_cls: int * string * kind * string list * string list * string list -> string
    1.67 +  val string_of_preds: (string * Int.int) list -> string
    1.68 +  val string_of_funcs: (string * int) list -> string
    1.69 +  val string_of_symbols: string -> string -> string
    1.70 +  val string_of_start: string -> string
    1.71 +  val string_of_descrip : string -> string
    1.72 +  val dfg_tfree_clause : string -> string
    1.73 +  val dfg_classrelClause: classrelClause -> string
    1.74 +  val dfg_arity_clause: arityClause -> string
    1.75 +  val tptp_sign: bool -> string -> string
    1.76 +  val tptp_of_typeLit : bool -> type_literal -> string
    1.77 +  val gen_tptp_cls : int * string * kind * string list * string list -> string
    1.78 +  val tptp_tfree_clause : string -> string
    1.79 +  val tptp_arity_clause : arityClause -> string
    1.80 +  val tptp_classrelClause : classrelClause -> string
    1.81 +end
    1.82 +
    1.83 +structure Res_Clause: RES_CLAUSE =
    1.84 +struct
    1.85 +
    1.86 +val schematic_var_prefix = "V_";
    1.87 +val fixed_var_prefix = "v_";
    1.88 +
    1.89 +val tvar_prefix = "T_";
    1.90 +val tfree_prefix = "t_";
    1.91 +
    1.92 +val clause_prefix = "cls_";
    1.93 +val arclause_prefix = "clsarity_"
    1.94 +val clrelclause_prefix = "clsrel_";
    1.95 +
    1.96 +val const_prefix = "c_";
    1.97 +val tconst_prefix = "tc_";
    1.98 +val class_prefix = "class_";
    1.99 +
   1.100 +fun union_all xss = List.foldl (uncurry (union (op =))) [] xss;
   1.101 +
   1.102 +(*Provide readable names for the more common symbolic functions*)
   1.103 +val const_trans_table =
   1.104 +      Symtab.make [(@{const_name "op ="}, "equal"),
   1.105 +                   (@{const_name Orderings.less_eq}, "lessequals"),
   1.106 +                   (@{const_name "op &"}, "and"),
   1.107 +                   (@{const_name "op |"}, "or"),
   1.108 +                   (@{const_name "op -->"}, "implies"),
   1.109 +                   (@{const_name "op :"}, "in"),
   1.110 +                   ("ATP_Linkup.fequal", "fequal"),
   1.111 +                   ("ATP_Linkup.COMBI", "COMBI"),
   1.112 +                   ("ATP_Linkup.COMBK", "COMBK"),
   1.113 +                   ("ATP_Linkup.COMBB", "COMBB"),
   1.114 +                   ("ATP_Linkup.COMBC", "COMBC"),
   1.115 +                   ("ATP_Linkup.COMBS", "COMBS"),
   1.116 +                   ("ATP_Linkup.COMBB'", "COMBB_e"),
   1.117 +                   ("ATP_Linkup.COMBC'", "COMBC_e"),
   1.118 +                   ("ATP_Linkup.COMBS'", "COMBS_e")];
   1.119 +
   1.120 +val type_const_trans_table =
   1.121 +      Symtab.make [("*", "prod"),
   1.122 +                   ("+", "sum"),
   1.123 +                   ("~=>", "map")];
   1.124 +
   1.125 +(*Escaping of special characters.
   1.126 +  Alphanumeric characters are left unchanged.
   1.127 +  The character _ goes to __
   1.128 +  Characters in the range ASCII space to / go to _A to _P, respectively.
   1.129 +  Other printing characters go to _nnn where nnn is the decimal ASCII code.*)
   1.130 +val A_minus_space = Char.ord #"A" - Char.ord #" ";
   1.131 +
   1.132 +fun stringN_of_int 0 _ = ""
   1.133 +  | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10);
   1.134 +
   1.135 +fun ascii_of_c c =
   1.136 +  if Char.isAlphaNum c then String.str c
   1.137 +  else if c = #"_" then "__"
   1.138 +  else if #" " <= c andalso c <= #"/"
   1.139 +       then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
   1.140 +  else if Char.isPrint c
   1.141 +       then ("_" ^ stringN_of_int 3 (Char.ord c))  (*fixed width, in case more digits follow*)
   1.142 +  else ""
   1.143 +
   1.144 +val ascii_of = String.translate ascii_of_c;
   1.145 +
   1.146 +(** Remove ASCII armouring from names in proof files **)
   1.147 +
   1.148 +(*We don't raise error exceptions because this code can run inside the watcher.
   1.149 +  Also, the errors are "impossible" (hah!)*)
   1.150 +fun undo_ascii_aux rcs [] = String.implode(rev rcs)
   1.151 +  | undo_ascii_aux rcs [#"_"] = undo_ascii_aux (#"_"::rcs) []  (*ERROR*)
   1.152 +      (*Three types of _ escapes: __, _A to _P, _nnn*)
   1.153 +  | undo_ascii_aux rcs (#"_" :: #"_" :: cs) = undo_ascii_aux (#"_"::rcs) cs
   1.154 +  | undo_ascii_aux rcs (#"_" :: c :: cs) =
   1.155 +      if #"A" <= c andalso c<= #"P"  (*translation of #" " to #"/"*)
   1.156 +      then undo_ascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
   1.157 +      else
   1.158 +        let val digits = List.take (c::cs, 3) handle Subscript => []
   1.159 +        in
   1.160 +            case Int.fromString (String.implode digits) of
   1.161 +                NONE => undo_ascii_aux (c:: #"_"::rcs) cs  (*ERROR*)
   1.162 +              | SOME n => undo_ascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
   1.163 +        end
   1.164 +  | undo_ascii_aux rcs (c::cs) = undo_ascii_aux (c::rcs) cs;
   1.165 +
   1.166 +val undo_ascii_of = undo_ascii_aux [] o String.explode;
   1.167 +
   1.168 +(* convert a list of strings into one single string; surrounded by brackets *)
   1.169 +fun paren_pack [] = ""   (*empty argument list*)
   1.170 +  | paren_pack strings = "(" ^ commas strings ^ ")";
   1.171 +
   1.172 +(*TSTP format uses (...) rather than the old [...]*)
   1.173 +fun tptp_pack strings = "(" ^ space_implode " | " strings ^ ")";
   1.174 +
   1.175 +
   1.176 +(*Remove the initial ' character from a type variable, if it is present*)
   1.177 +fun trim_type_var s =
   1.178 +  if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
   1.179 +  else error ("trim_type: Malformed type variable encountered: " ^ s);
   1.180 +
   1.181 +fun ascii_of_indexname (v,0) = ascii_of v
   1.182 +  | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i;
   1.183 +
   1.184 +fun make_schematic_var v = schematic_var_prefix ^ (ascii_of_indexname v);
   1.185 +fun make_fixed_var x = fixed_var_prefix ^ (ascii_of x);
   1.186 +
   1.187 +fun make_schematic_type_var (x,i) =
   1.188 +      tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
   1.189 +fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
   1.190 +
   1.191 +(*HACK because SPASS truncates identifiers to 63 characters :-(( *)
   1.192 +(*32-bit hash,so we expect no collisions unless there are around 65536 long identifiers...*)
   1.193 +fun controlled_length dfg_format s =
   1.194 +  if size s > 60 andalso dfg_format
   1.195 +  then Word.toString (Polyhash.hashw_string(s,0w0))
   1.196 +  else s;
   1.197 +
   1.198 +fun lookup_const dfg c =
   1.199 +    case Symtab.lookup const_trans_table c of
   1.200 +        SOME c' => c'
   1.201 +      | NONE => controlled_length dfg (ascii_of c);
   1.202 +
   1.203 +fun lookup_type_const dfg c =
   1.204 +    case Symtab.lookup type_const_trans_table c of
   1.205 +        SOME c' => c'
   1.206 +      | NONE => controlled_length dfg (ascii_of c);
   1.207 +
   1.208 +fun make_fixed_const _ "op =" = "equal"   (*MUST BE "equal" because it's built-in to ATPs*)
   1.209 +  | make_fixed_const dfg c      = const_prefix ^ lookup_const dfg c;
   1.210 +
   1.211 +fun make_fixed_type_const dfg c = tconst_prefix ^ lookup_type_const dfg c;
   1.212 +
   1.213 +fun make_type_class clas = class_prefix ^ ascii_of clas;
   1.214 +
   1.215 +
   1.216 +(***** definitions and functions for FOL clauses, for conversion to TPTP or DFG format. *****)
   1.217 +
   1.218 +datatype kind = Axiom | Conjecture;
   1.219 +
   1.220 +type axiom_name = string;
   1.221 +
   1.222 +(**** Isabelle FOL clauses ****)
   1.223 +
   1.224 +(*FIXME: give the constructors more sensible names*)
   1.225 +datatype fol_type = AtomV of string
   1.226 +                  | AtomF of string
   1.227 +                  | Comp of string * fol_type list;
   1.228 +
   1.229 +fun string_of_fol_type (AtomV x) = x
   1.230 +  | string_of_fol_type (AtomF x) = x
   1.231 +  | string_of_fol_type (Comp(tcon,tps)) =
   1.232 +      tcon ^ (paren_pack (map string_of_fol_type tps));
   1.233 +
   1.234 +(*First string is the type class; the second is a TVar or TFfree*)
   1.235 +datatype type_literal = LTVar of string * string | LTFree of string * string;
   1.236 +
   1.237 +exception CLAUSE of string * term;
   1.238 +
   1.239 +fun atomic_type (TFree (a,_)) = AtomF(make_fixed_type_var a)
   1.240 +  | atomic_type (TVar (v,_))  = AtomV(make_schematic_type_var v);
   1.241 +
   1.242 +(*Flatten a type to a fol_type while accumulating sort constraints on the TFrees and
   1.243 +  TVars it contains.*)
   1.244 +fun type_of dfg (Type (a, Ts)) =
   1.245 +      let val (folTyps, ts) = types_of dfg Ts
   1.246 +          val t = make_fixed_type_const dfg a
   1.247 +      in (Comp(t,folTyps), ts) end
   1.248 +  | type_of dfg T = (atomic_type T, [T])
   1.249 +and types_of dfg Ts =
   1.250 +      let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
   1.251 +      in (folTyps, union_all ts) end;
   1.252 +
   1.253 +(*Make literals for sorted type variables*)
   1.254 +fun sorts_on_typs_aux (_, [])   = []
   1.255 +  | sorts_on_typs_aux ((x,i),  s::ss) =
   1.256 +      let val sorts = sorts_on_typs_aux ((x,i), ss)
   1.257 +      in
   1.258 +          if s = "HOL.type" then sorts
   1.259 +          else if i = ~1 then LTFree(make_type_class s, make_fixed_type_var x) :: sorts
   1.260 +          else LTVar(make_type_class s, make_schematic_type_var (x,i)) :: sorts
   1.261 +      end;
   1.262 +
   1.263 +fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
   1.264 +  | sorts_on_typs (TVar (v,s))  = sorts_on_typs_aux (v,s);
   1.265 +
   1.266 +fun pred_of_sort (LTVar (s,ty)) = (s,1)
   1.267 +  | pred_of_sort (LTFree (s,ty)) = (s,1)
   1.268 +
   1.269 +(*Given a list of sorted type variables, return a list of type literals.*)
   1.270 +fun add_typs Ts = List.foldl (uncurry (union (op =))) [] (map sorts_on_typs Ts);
   1.271 +
   1.272 +(*The correct treatment of TFrees like 'a in lemmas (axiom clauses) is not clear.
   1.273 +  * Ignoring them leads to unsound proofs, since we do nothing to ensure that 'a
   1.274 +    in a lemma has the same sort as 'a in the conjecture.
   1.275 +  * Deleting such clauses will lead to problems with locales in other use of local results
   1.276 +    where 'a is fixed. Probably we should delete clauses unless the sorts agree.
   1.277 +  * Currently we include a class constraint in the clause, exactly as with TVars.
   1.278 +*)
   1.279 +
   1.280 +(** make axiom and conjecture clauses. **)
   1.281 +
   1.282 +fun get_tvar_strs [] = []
   1.283 +  | get_tvar_strs ((TVar (indx,s))::Ts) =
   1.284 +      insert (op =) (make_schematic_type_var indx) (get_tvar_strs Ts)
   1.285 +  | get_tvar_strs((TFree _)::Ts) = get_tvar_strs Ts
   1.286 +
   1.287 +
   1.288 +
   1.289 +(**** Isabelle arities ****)
   1.290 +
   1.291 +exception ARCLAUSE of string;
   1.292 +
   1.293 +datatype arLit = TConsLit of class * string * string list
   1.294 +               | TVarLit of class * string;
   1.295 +
   1.296 +datatype arityClause =
   1.297 +         ArityClause of {axiom_name: axiom_name,
   1.298 +                         conclLit: arLit,
   1.299 +                         premLits: arLit list};
   1.300 +
   1.301 +
   1.302 +fun gen_TVars 0 = []
   1.303 +  | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1);
   1.304 +
   1.305 +fun pack_sort(_,[])  = []
   1.306 +  | pack_sort(tvar, "HOL.type"::srt) = pack_sort(tvar, srt)   (*IGNORE sort "type"*)
   1.307 +  | pack_sort(tvar, cls::srt) =  (cls, tvar) :: pack_sort(tvar, srt);
   1.308 +
   1.309 +(*Arity of type constructor tcon :: (arg1,...,argN)res*)
   1.310 +fun make_axiom_arity_clause dfg (tcons, axiom_name, (cls,args)) =
   1.311 +   let val tvars = gen_TVars (length args)
   1.312 +       val tvars_srts = ListPair.zip (tvars,args)
   1.313 +   in
   1.314 +      ArityClause {axiom_name = axiom_name, 
   1.315 +                   conclLit = TConsLit (cls, make_fixed_type_const dfg tcons, tvars),
   1.316 +                   premLits = map TVarLit (union_all(map pack_sort tvars_srts))}
   1.317 +   end;
   1.318 +
   1.319 +
   1.320 +(**** Isabelle class relations ****)
   1.321 +
   1.322 +datatype classrelClause =
   1.323 +         ClassrelClause of {axiom_name: axiom_name,
   1.324 +                            subclass: class,
   1.325 +                            superclass: class};
   1.326 +
   1.327 +(*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
   1.328 +fun class_pairs thy [] supers = []
   1.329 +  | class_pairs thy subs supers =
   1.330 +      let val class_less = Sorts.class_less(Sign.classes_of thy)
   1.331 +          fun add_super sub (super,pairs) =
   1.332 +                if class_less (sub,super) then (sub,super)::pairs else pairs
   1.333 +          fun add_supers (sub,pairs) = List.foldl (add_super sub) pairs supers
   1.334 +      in  List.foldl add_supers [] subs  end;
   1.335 +
   1.336 +fun make_classrelClause (sub,super) =
   1.337 +  ClassrelClause {axiom_name = clrelclause_prefix ^ ascii_of sub ^ "_" ^ ascii_of super,
   1.338 +                  subclass = make_type_class sub,
   1.339 +                  superclass = make_type_class super};
   1.340 +
   1.341 +fun make_classrel_clauses thy subs supers =
   1.342 +  map make_classrelClause (class_pairs thy subs supers);
   1.343 +
   1.344 +
   1.345 +(** Isabelle arities **)
   1.346 +
   1.347 +fun arity_clause dfg _ _ (tcons, []) = []
   1.348 +  | arity_clause dfg seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
   1.349 +      arity_clause dfg seen n (tcons,ars)
   1.350 +  | arity_clause dfg seen n (tcons, (ar as (class,_)) :: ars) =
   1.351 +      if class mem_string seen then (*multiple arities for the same tycon, class pair*)
   1.352 +          make_axiom_arity_clause dfg (tcons, lookup_type_const dfg tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
   1.353 +          arity_clause dfg seen (n+1) (tcons,ars)
   1.354 +      else
   1.355 +          make_axiom_arity_clause dfg (tcons, lookup_type_const dfg tcons ^ "_" ^ class, ar) ::
   1.356 +          arity_clause dfg (class::seen) n (tcons,ars)
   1.357 +
   1.358 +fun multi_arity_clause dfg [] = []
   1.359 +  | multi_arity_clause dfg ((tcons,ars) :: tc_arlists) =
   1.360 +      arity_clause dfg [] 1 (tcons, ars)  @  multi_arity_clause dfg tc_arlists
   1.361 +
   1.362 +(*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
   1.363 +  provided its arguments have the corresponding sorts.*)
   1.364 +fun type_class_pairs thy tycons classes =
   1.365 +  let val alg = Sign.classes_of thy
   1.366 +      fun domain_sorts (tycon,class) = Sorts.mg_domain alg tycon [class]
   1.367 +      fun add_class tycon (class,pairs) =
   1.368 +            (class, domain_sorts(tycon,class))::pairs
   1.369 +            handle Sorts.CLASS_ERROR _ => pairs
   1.370 +      fun try_classes tycon = (tycon, List.foldl (add_class tycon) [] classes)
   1.371 +  in  map try_classes tycons  end;
   1.372 +
   1.373 +(*Proving one (tycon, class) membership may require proving others, so iterate.*)
   1.374 +fun iter_type_class_pairs thy tycons [] = ([], [])
   1.375 +  | iter_type_class_pairs thy tycons classes =
   1.376 +      let val cpairs = type_class_pairs thy tycons classes
   1.377 +          val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
   1.378 +            |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
   1.379 +          val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
   1.380 +      in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
   1.381 +
   1.382 +fun make_arity_clauses_dfg dfg thy tycons classes =
   1.383 +  let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
   1.384 +  in  (classes', multi_arity_clause dfg cpairs)  end;
   1.385 +val make_arity_clauses = make_arity_clauses_dfg false;
   1.386 +
   1.387 +(**** Find occurrences of predicates in clauses ****)
   1.388 +
   1.389 +(*FIXME: multiple-arity checking doesn't work, as update_new is the wrong
   1.390 +  function (it flags repeated declarations of a function, even with the same arity)*)
   1.391 +
   1.392 +fun update_many (tab, keypairs) = List.foldl (uncurry Symtab.update) tab keypairs;
   1.393 +
   1.394 +fun add_type_sort_preds (T, preds) =
   1.395 +      update_many (preds, map pred_of_sort (sorts_on_typs T));
   1.396 +
   1.397 +fun add_classrelClause_preds (ClassrelClause {subclass,superclass,...}, preds) =
   1.398 +  Symtab.update (subclass,1) (Symtab.update (superclass,1) preds);
   1.399 +
   1.400 +fun class_of_arityLit (TConsLit (tclass, _, _)) = tclass
   1.401 +  | class_of_arityLit (TVarLit (tclass, _)) = tclass;
   1.402 +
   1.403 +fun add_arityClause_preds (ArityClause {conclLit,premLits,...}, preds) =
   1.404 +  let val classes = map (make_type_class o class_of_arityLit) (conclLit::premLits)
   1.405 +      fun upd (class,preds) = Symtab.update (class,1) preds
   1.406 +  in  List.foldl upd preds classes  end;
   1.407 +
   1.408 +(*** Find occurrences of functions in clauses ***)
   1.409 +
   1.410 +fun add_foltype_funcs (AtomV _, funcs) = funcs
   1.411 +  | add_foltype_funcs (AtomF a, funcs) = Symtab.update (a,0) funcs
   1.412 +  | add_foltype_funcs (Comp(a,tys), funcs) =
   1.413 +      List.foldl add_foltype_funcs (Symtab.update (a, length tys) funcs) tys;
   1.414 +
   1.415 +(*TFrees are recorded as constants*)
   1.416 +fun add_type_sort_funcs (TVar _, funcs) = funcs
   1.417 +  | add_type_sort_funcs (TFree (a, _), funcs) =
   1.418 +      Symtab.update (make_fixed_type_var a, 0) funcs
   1.419 +
   1.420 +fun add_arityClause_funcs (ArityClause {conclLit,...}, funcs) =
   1.421 +  let val TConsLit (_, tcons, tvars) = conclLit
   1.422 +  in  Symtab.update (tcons, length tvars) funcs  end;
   1.423 +
   1.424 +(*This type can be overlooked because it is built-in...*)
   1.425 +val init_functab = Symtab.update ("tc_itself", 1) Symtab.empty;
   1.426 +
   1.427 +
   1.428 +(**** String-oriented operations ****)
   1.429 +
   1.430 +fun string_of_clausename (cls_id,ax_name) =
   1.431 +    clause_prefix ^ ascii_of ax_name ^ "_" ^ Int.toString cls_id;
   1.432 +
   1.433 +fun string_of_type_clsname (cls_id,ax_name,idx) =
   1.434 +    string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
   1.435 +
   1.436 +
   1.437 +(**** Producing DFG files ****)
   1.438 +
   1.439 +(*Attach sign in DFG syntax: false means negate.*)
   1.440 +fun dfg_sign true s = s
   1.441 +  | dfg_sign false s = "not(" ^ s ^ ")"
   1.442 +
   1.443 +fun dfg_of_typeLit pos (LTVar (s,ty))  = dfg_sign pos (s ^ "(" ^ ty ^ ")")
   1.444 +  | dfg_of_typeLit pos (LTFree (s,ty)) = dfg_sign pos (s ^ "(" ^ ty ^ ")");
   1.445 +
   1.446 +(*Enclose the clause body by quantifiers, if necessary*)
   1.447 +fun dfg_forall [] body = body
   1.448 +  | dfg_forall vars body = "forall([" ^ commas vars ^ "],\n" ^ body ^ ")"
   1.449 +
   1.450 +fun gen_dfg_cls (cls_id, ax_name, Axiom, lits, tylits, vars) =
   1.451 +      "clause( %(axiom)\n" ^
   1.452 +      dfg_forall vars ("or(" ^ commas (tylits@lits) ^ ")") ^ ",\n" ^
   1.453 +      string_of_clausename (cls_id,ax_name) ^  ").\n\n"
   1.454 +  | gen_dfg_cls (cls_id, ax_name, Conjecture, lits, _, vars) =
   1.455 +      "clause( %(negated_conjecture)\n" ^
   1.456 +      dfg_forall vars ("or(" ^ commas lits ^ ")") ^ ",\n" ^
   1.457 +      string_of_clausename (cls_id,ax_name) ^  ").\n\n";
   1.458 +
   1.459 +fun string_of_arity (name, num) =  "(" ^ name ^ "," ^ Int.toString num ^ ")"
   1.460 +
   1.461 +fun string_of_preds [] = ""
   1.462 +  | string_of_preds preds = "predicates[" ^ commas(map string_of_arity preds) ^ "].\n";
   1.463 +
   1.464 +fun string_of_funcs [] = ""
   1.465 +  | string_of_funcs funcs = "functions[" ^ commas(map string_of_arity funcs) ^ "].\n" ;
   1.466 +
   1.467 +fun string_of_symbols predstr funcstr =
   1.468 +  "list_of_symbols.\n" ^ predstr  ^ funcstr  ^ "end_of_list.\n\n";
   1.469 +
   1.470 +fun string_of_start name = "begin_problem(" ^ name ^ ").\n\n";
   1.471 +
   1.472 +fun string_of_descrip name =
   1.473 +  "list_of_descriptions.\nname({*" ^ name ^
   1.474 +  "*}).\nauthor({*Isabelle*}).\nstatus(unknown).\ndescription({*auto-generated*}).\nend_of_list.\n\n"
   1.475 +
   1.476 +fun dfg_tfree_clause tfree_lit =
   1.477 +  "clause( %(negated_conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ").\n\n"
   1.478 +
   1.479 +fun dfg_of_arLit (TConsLit (c,t,args)) =
   1.480 +      dfg_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
   1.481 +  | dfg_of_arLit (TVarLit (c,str)) =
   1.482 +      dfg_sign false (make_type_class c ^ "(" ^ str ^ ")")
   1.483 +
   1.484 +fun dfg_classrelLits sub sup =  "not(" ^ sub ^ "(T)), " ^ sup ^ "(T)";
   1.485 +
   1.486 +fun dfg_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) =
   1.487 +  "clause(forall([T],\nor( " ^ dfg_classrelLits subclass superclass ^ ")),\n" ^
   1.488 +  axiom_name ^ ").\n\n";
   1.489 +
   1.490 +fun string_of_ar axiom_name = arclause_prefix ^ ascii_of axiom_name;
   1.491 +
   1.492 +fun dfg_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) =
   1.493 +  let val TConsLit (_,_,tvars) = conclLit
   1.494 +      val lits = map dfg_of_arLit (conclLit :: premLits)
   1.495 +  in
   1.496 +      "clause( %(axiom)\n" ^
   1.497 +      dfg_forall tvars ("or( " ^ commas lits ^ ")") ^ ",\n" ^
   1.498 +      string_of_ar axiom_name ^ ").\n\n"
   1.499 +  end;
   1.500 +
   1.501 +
   1.502 +(**** Produce TPTP files ****)
   1.503 +
   1.504 +(*Attach sign in TPTP syntax: false means negate.*)
   1.505 +fun tptp_sign true s = s
   1.506 +  | tptp_sign false s = "~ " ^ s
   1.507 +
   1.508 +fun tptp_of_typeLit pos (LTVar (s,ty))  = tptp_sign pos (s ^ "(" ^ ty ^ ")")
   1.509 +  | tptp_of_typeLit pos (LTFree (s,ty)) = tptp_sign pos  (s ^ "(" ^ ty ^ ")");
   1.510 +
   1.511 +fun gen_tptp_cls (cls_id,ax_name,Axiom,lits,tylits) =
   1.512 +      "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ ",axiom," ^ 
   1.513 +               tptp_pack (tylits@lits) ^ ").\n"
   1.514 +  | gen_tptp_cls (cls_id,ax_name,Conjecture,lits,_) =
   1.515 +      "cnf(" ^ string_of_clausename (cls_id,ax_name) ^ ",negated_conjecture," ^ 
   1.516 +               tptp_pack lits ^ ").\n";
   1.517 +
   1.518 +fun tptp_tfree_clause tfree_lit =
   1.519 +    "cnf(" ^ "tfree_tcs," ^ "negated_conjecture" ^ "," ^ tptp_pack[tfree_lit] ^ ").\n";
   1.520 +
   1.521 +fun tptp_of_arLit (TConsLit (c,t,args)) =
   1.522 +      tptp_sign true (make_type_class c ^ "(" ^ t ^ paren_pack args ^ ")")
   1.523 +  | tptp_of_arLit (TVarLit (c,str)) =
   1.524 +      tptp_sign false (make_type_class c ^ "(" ^ str ^ ")")
   1.525 +
   1.526 +fun tptp_arity_clause (ArityClause{axiom_name,conclLit,premLits,...}) =
   1.527 +  "cnf(" ^ string_of_ar axiom_name ^ ",axiom," ^
   1.528 +  tptp_pack (map tptp_of_arLit (conclLit :: premLits)) ^ ").\n";
   1.529 +
   1.530 +fun tptp_classrelLits sub sup =
   1.531 +  let val tvar = "(T)"
   1.532 +  in  tptp_pack [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)]  end;
   1.533 +
   1.534 +fun tptp_classrelClause (ClassrelClause {axiom_name,subclass,superclass,...}) =
   1.535 +  "cnf(" ^ axiom_name ^ ",axiom," ^ tptp_classrelLits subclass superclass ^ ").\n"
   1.536 +
   1.537 +end;