Changed input interface of dfg_write_file.
authormengj
Thu May 25 08:08:38 2006 +0200 (2006-05-25)
changeset 19719837025cc6317
parent 19718 e709f643c578
child 19720 f68f6f958a1d
Changed input interface of dfg_write_file.
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/res_clause.ML	Thu May 25 08:08:04 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Thu May 25 08:08:38 2006 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4    val clause_prefix : string 
     1.5    val clause2tptp : clause -> string * string list
     1.6    val const_prefix : string
     1.7 -  val dfg_write_file: thm list -> string -> (clause list * classrelClause list * arityClause list) -> unit
     1.8 +  val dfg_write_file:  thm list -> string -> ((thm * (string * int)) list * classrelClause list * arityClause list) -> unit
     1.9    val fixed_var_prefix : string
    1.10    val gen_tptp_cls : int * string * string * string -> string
    1.11    val gen_tptp_type_cls : int * string * string * string * int -> string
    1.12 @@ -61,7 +61,23 @@
    1.13    val types_ord : fol_type list * fol_type list -> order
    1.14    val union_all : ''a list list -> ''a list
    1.15    val writeln_strs: TextIO.outstream -> TextIO.vector list -> unit
    1.16 -  end;
    1.17 +  val dfg_sign: bool -> string -> string
    1.18 +  val dfg_of_typeLit: type_literal -> string
    1.19 +  val get_tvar_strs: (typ_var * sort) list -> string list
    1.20 +  val gen_dfg_cls: int * string * string * string * string list -> string
    1.21 +  val add_foltype_funcs: fol_type * int Symtab.table -> int Symtab.table
    1.22 +  val add_arityClause_funcs: arityClause * int Symtab.table -> int Symtab.table
    1.23 +  val add_arityClause_preds: arityClause * int Symtab.table -> int Symtab.table
    1.24 +  val add_classrelClause_preds : classrelClause * int Symtab.table -> int Symtab.table
    1.25 +  val dfg_tfree_clause : string -> string
    1.26 +  val string_of_start: string -> string
    1.27 +  val string_of_descrip : string -> string
    1.28 +  val string_of_symbols: string -> string -> string
    1.29 +  val string_of_funcs: (string * int) list -> string
    1.30 +  val string_of_preds: (string * Int.int) list -> string
    1.31 +  val dfg_classrelClause: classrelClause -> string
    1.32 +  val dfg_arity_clause: arityClause -> string
    1.33 +end;
    1.34  
    1.35  structure ResClause : RES_CLAUSE =
    1.36  struct
    1.37 @@ -928,16 +944,17 @@
    1.38    end;
    1.39  
    1.40  (* write out a subgoal in DFG format to the file "xxxx_N"*)
    1.41 -fun dfg_write_file ths filename (axclauses,classrel_clauses,arity_clauses) = 
    1.42 +fun dfg_write_file thms filename (axclauses,classrel_clauses,arity_clauses) = 
    1.43    let 
    1.44      val _ = Output.debug ("Preparing to write the DFG file " ^ filename)
    1.45 -    val conjectures = make_conjecture_clauses ths
    1.46 +    val conjectures = make_conjecture_clauses thms
    1.47 +    val axclauses' = make_axiom_clauses axclauses
    1.48      val (dfg_clss, tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
    1.49 -    val clss = conjectures @ axclauses
    1.50 +    val clss = conjectures @ axclauses'
    1.51      val funcs = funcs_of_clauses clss arity_clauses
    1.52      and preds = preds_of_clauses clss classrel_clauses arity_clauses
    1.53      and probname = Path.pack (Path.base (Path.unpack filename))
    1.54 -    val (axstrs, _) = ListPair.unzip (map clause2dfg axclauses)
    1.55 +    val (axstrs, _) = ListPair.unzip (map clause2dfg axclauses')
    1.56      val tfree_clss = map dfg_tfree_clause (union_all tfree_litss) 
    1.57      val out = TextIO.openOut filename
    1.58    in