src/HOL/Tools/res_clause.ML
changeset 18863 a113b6839df1
parent 18856 4669dec681f4
child 18868 7cfc21ee0370
     1.1 --- a/src/HOL/Tools/res_clause.ML	Tue Jan 31 00:51:15 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Tue Jan 31 10:39:13 2006 +0100
     1.3 @@ -25,9 +25,6 @@
     1.4    val isTaut : clause -> bool
     1.5    val num_of_clauses : clause -> int
     1.6  
     1.7 -  val clauses2dfg : string -> clause list -> clause list -> string
     1.8 -  val tfree_dfg_clause : string -> string
     1.9 -
    1.10    val arity_clause_thy: theory -> arityClause list 
    1.11    val classrel_clauses_thy: theory -> classrelClause list 
    1.12  
    1.13 @@ -35,7 +32,7 @@
    1.14    val tptp_classrelClause : classrelClause -> string
    1.15    val tptp_clause : clause -> string list
    1.16    val clause2tptp : clause -> string * string list
    1.17 -  val tfree_clause : string -> string
    1.18 +  val tptp_tfree_clause : string -> string
    1.19    val schematic_var_prefix : string
    1.20    val fixed_var_prefix : string
    1.21    val tvar_prefix : string
    1.22 @@ -76,9 +73,16 @@
    1.23    val types_ord : fol_type list * fol_type list -> order
    1.24    val string_of_fol_type : fol_type -> string
    1.25    val mk_fol_type: string * string * fol_type list -> fol_type
    1.26 -  val types_eq :fol_type list * fol_type list ->
    1.27 -   (string * string) list * (string * string) list -> bool * ((string * string) list * (string * string) list)
    1.28 +  val types_eq: fol_type list * fol_type list -> 
    1.29 +        (string*string) list * (string*string) list -> 
    1.30 +        bool * ((string*string) list * (string*string) list)
    1.31    val check_var_pairs: ''a * ''b -> (''a * ''b) list -> int
    1.32 +
    1.33 +  val dfg_write_file: thm list -> string -> 
    1.34 +        (clause list * classrelClause list * arityClause list) -> unit
    1.35 +  val tptp_write_file: thm list -> string -> 
    1.36 +        (clause list * classrelClause list * arityClause list) -> unit
    1.37 +  val writeln_strs: TextIO.outstream -> TextIO.vector list -> unit
    1.38    end;
    1.39  
    1.40  structure ResClause : RES_CLAUSE =
    1.41 @@ -794,17 +798,21 @@
    1.42  
    1.43  fun string_of_type_clsname (cls_id,ax_name,idx) = 
    1.44      string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
    1.45 +
    1.46 +(*Write a list of strings to a file*)
    1.47 +fun writeln_strs os = List.app (fn s => TextIO.output (os,s));
    1.48 +
    1.49      
    1.50  
    1.51  (********************************)
    1.52  (* Code for producing DFG files *)
    1.53  (********************************)
    1.54  
    1.55 -fun dfg_literal (Literal(pol,pred,tag)) =
    1.56 -    let val pred_string = string_of_predicate pred
    1.57 -    in
    1.58 -	if pol then pred_string else "not(" ^pred_string ^ ")"  
    1.59 -    end;
    1.60 +(*Attach sign in DFG syntax: false means negate.*)
    1.61 +fun dfg_sign true s = s
    1.62 +  | dfg_sign false s = "not(" ^ s ^ ")"  
    1.63 +
    1.64 +fun dfg_literal (Literal(pol,pred,tag)) = dfg_sign pol (string_of_predicate pred)
    1.65  
    1.66  fun dfg_of_typeLit (LTVar (s,ty)) = "not(" ^ s ^ "(" ^ ty ^ "))"
    1.67    | dfg_of_typeLit (LTFree (s,ty)) = s ^ "(" ^ ty ^ ")";
    1.68 @@ -819,13 +827,13 @@
    1.69  fun gen_dfg_cls (cls_id,ax_name,knd,lits,tvars,vars) = 
    1.70      "clause( %(" ^ knd ^ ")\n" ^ forall_open(vars,tvars) ^ 
    1.71      "or(" ^ lits ^ ")" ^ forall_close(vars,tvars) ^ ",\n" ^ 
    1.72 -    string_of_clausename (cls_id,ax_name) ^  ").";
    1.73 +    string_of_clausename (cls_id,ax_name) ^  ").\n\n";
    1.74  
    1.75  (*FIXME: UNUSED*)
    1.76  fun gen_dfg_type_cls (cls_id,ax_name,knd,tfree_lit,idx,tvars,vars) = 
    1.77      "clause( %(" ^ knd ^ ")\n" ^ forall_open(vars,tvars) ^ 
    1.78      "or( " ^ tfree_lit ^ ")" ^ forall_close(vars,tvars) ^ ",\n" ^ 
    1.79 -    string_of_type_clsname (cls_id,ax_name,idx) ^  ").";
    1.80 +    string_of_type_clsname (cls_id,ax_name,idx) ^  ").\n\n";
    1.81  
    1.82  fun dfg_clause_aux (Clause cls) = 
    1.83    let val lits = map dfg_literal (#literals cls)
    1.84 @@ -887,35 +895,24 @@
    1.85  fun string_of_symbols predstr funcstr = 
    1.86    "list_of_symbols.\n" ^ predstr  ^ funcstr  ^ "end_of_list.\n\n";
    1.87  
    1.88 -fun string_of_axioms axstr = 
    1.89 -  "list_of_clauses(axioms,cnf).\n" ^ axstr ^ "end_of_list.\n\n";
    1.90 +fun write_axioms (out, strs) = 
    1.91 +  (TextIO.output (out, "list_of_clauses(axioms,cnf).\n");
    1.92 +   writeln_strs out strs;
    1.93 +   TextIO.output (out, "end_of_list.\n\n"));
    1.94  
    1.95 -fun string_of_conjectures conjstr = 
    1.96 -  "list_of_clauses(conjectures,cnf).\n" ^ conjstr ^ "end_of_list.\n\n";
    1.97 +fun write_conjectures (out, strs) = 
    1.98 +  (TextIO.output (out, "list_of_clauses(conjectures,cnf).\n");
    1.99 +   writeln_strs out strs;
   1.100 +   TextIO.output (out, "end_of_list.\n\n"));
   1.101  
   1.102  fun string_of_start name = "begin_problem(" ^ name ^ ").\n\n";
   1.103  
   1.104 -fun string_of_descrip name = "list_of_descriptions.\nname({*" ^ name ^ "*}).\nauthor({*Isabelle*}).\nstatus(unknown).\ndescription({*auto-generated*}).\nend_of_list.\n\n"
   1.105 -
   1.106 -fun tfree_dfg_clause tfree_lit =
   1.107 -  "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ")."
   1.108 +fun string_of_descrip name = 
   1.109 +  "list_of_descriptions.\nname({*" ^ name ^ "*}).\nauthor({*Isabelle*}).\nstatus(unknown).\ndescription({*auto-generated*}).\nend_of_list.\n\n"
   1.110  
   1.111 -fun gen_dfg_file probname axioms conjectures funcs preds = 
   1.112 -    let val axstrs_tfrees = (map clause2dfg axioms)
   1.113 -	val (axstrs, atfrees) = ListPair.unzip axstrs_tfrees
   1.114 -        val axstr = (space_implode "\n" axstrs) ^ "\n\n"
   1.115 -	val (conjstrs, atfrees) = ListPair.unzip (map clause2dfg conjectures)
   1.116 -        val tfree_clss = map tfree_dfg_clause (union_all atfrees) 
   1.117 -        val conjstr = (space_implode "\n" (tfree_clss@conjstrs)) ^ "\n\n"
   1.118 -        val funcstr = string_of_funcs funcs
   1.119 -        val predstr = string_of_preds preds
   1.120 -    in
   1.121 -       string_of_start probname ^ string_of_descrip probname ^
   1.122 -       string_of_symbols funcstr predstr ^  
   1.123 -       string_of_axioms axstr ^
   1.124 -       string_of_conjectures conjstr ^ "end_problem.\n"
   1.125 -    end;
   1.126 -   
   1.127 +fun dfg_tfree_clause tfree_lit =
   1.128 +  "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ").\n\n"
   1.129 +
   1.130  
   1.131  (*** Find all occurrences of predicates in types, terms, literals... ***)
   1.132  
   1.133 @@ -969,42 +966,34 @@
   1.134  
   1.135  val funcs_of_clauses = Symtab.dest o (foldl add_clause_funcs Symtab.empty)
   1.136  
   1.137 -
   1.138 -fun clauses2dfg probname axioms conjectures = 
   1.139 -  let val clss = conjectures @ axioms
   1.140 -  in
   1.141 -     gen_dfg_file probname axioms conjectures 
   1.142 -       (funcs_of_clauses clss) (preds_of_clauses clss)
   1.143 -  end
   1.144 -
   1.145 -
   1.146  fun string_of_arClauseID (ArityClause {clause_id,axiom_name,...}) =
   1.147      arclause_prefix ^ ascii_of axiom_name ^ "_" ^ Int.toString clause_id;
   1.148  
   1.149  fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls);
   1.150  
   1.151 -(*FIXME!!! currently is TPTP format!*)
   1.152 -fun dfg_of_arLit (TConsLit(b,(c,t,args))) =
   1.153 -      let val pol = if b then "++" else "--"
   1.154 -	  val arg_strs = paren_pack args
   1.155 -      in 
   1.156 -	  pol ^ c ^ "(" ^ t ^ arg_strs ^ ")"
   1.157 -      end
   1.158 -  | dfg_of_arLit (TVarLit(b,(c,str))) =
   1.159 -      let val pol = if b then "++" else "--"
   1.160 -      in
   1.161 -	  pol ^ c ^ "(" ^ str ^ ")"
   1.162 -      end;
   1.163 +fun dfg_of_arLit (TConsLit(pol,(c,t,args))) =
   1.164 +      dfg_sign pol (c ^ "(" ^ t ^ paren_pack args ^ ")")
   1.165 +  | dfg_of_arLit (TVarLit(pol,(c,str))) =
   1.166 +      dfg_sign pol (c ^ "(" ^ str ^ ")")
   1.167      
   1.168 -
   1.169  fun dfg_of_conclLit (ArityClause arcls) = dfg_of_arLit (#conclLit arcls);
   1.170       
   1.171 -
   1.172  fun dfg_of_premLits (ArityClause arcls) = map dfg_of_arLit (#premLits arcls);
   1.173  		
   1.174 -
   1.175 +fun dfg_classrelLits sub sup = 
   1.176 +    let val tvar = "(T)"
   1.177 +    in 
   1.178 +	"not(" ^ sub ^ tvar ^ "), " ^ sup ^ tvar
   1.179 +    end;
   1.180  
   1.181 -(*FIXME: would this have variables in a forall? *)
   1.182 +fun dfg_classrelClause (ClassrelClause {clause_id,subclass,superclass,...}) =
   1.183 +  let val relcls_id = clrelclause_prefix ^ ascii_of subclass ^ "_" ^ 
   1.184 +		      Int.toString clause_id
   1.185 +      val lits = dfg_classrelLits (make_type_class subclass) (make_type_class superclass)
   1.186 +  in
   1.187 +      "clause(\nor( " ^ lits ^ ")),\n" ^
   1.188 +      relcls_id ^ ").\n\n"
   1.189 +  end; 
   1.190  
   1.191  fun dfg_arity_clause arcls = 
   1.192    let val arcls_id = string_of_arClauseID arcls
   1.193 @@ -1013,8 +1002,35 @@
   1.194        val knd = string_of_arKind arcls
   1.195        val all_lits = concl_lit :: prems_lits
   1.196    in
   1.197 -      "clause( %(" ^ knd ^ ")\n" ^  "or( " ^ (bracket_pack all_lits) ^ ")),\n" ^
   1.198 -       arcls_id ^  ")."
   1.199 +      "clause( %(" ^ knd ^ ")\n" ^  "or( " ^ bracket_pack all_lits ^ ")),\n" ^
   1.200 +       arcls_id ^ ").\n\n"
   1.201 +  end;
   1.202 +
   1.203 +(* write out a subgoal in DFG format to the file "xxxx_N"*)
   1.204 +fun dfg_write_file ths filename (axclauses,classrel_clauses,arity_clauses) = 
   1.205 +  let 
   1.206 +    val conjectures = make_conjecture_clauses (map prop_of ths)
   1.207 +    val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
   1.208 +    val classrel_cls = map dfg_classrelClause classrel_clauses
   1.209 +    val arity_cls = map dfg_arity_clause arity_clauses
   1.210 +    val clss = conjectures @ axclauses
   1.211 +    val funcs = (funcs_of_clauses clss)
   1.212 +    and preds = (preds_of_clauses clss)
   1.213 +    val out = TextIO.openOut filename
   1.214 +    and probname = Path.pack (Path.base (Path.unpack filename))
   1.215 +    val axstrs_tfrees = (map clause2dfg axclauses)
   1.216 +    val (axstrs, _) = ListPair.unzip axstrs_tfrees
   1.217 +    val tfree_clss = map dfg_tfree_clause (union_all tfree_litss) 
   1.218 +    val funcstr = string_of_funcs funcs
   1.219 +    val predstr = string_of_preds preds
   1.220 +  in
   1.221 +      TextIO.output (out, string_of_start probname); 
   1.222 +      TextIO.output (out, string_of_descrip probname); 
   1.223 +      TextIO.output (out, string_of_symbols funcstr predstr); 
   1.224 +      write_axioms (out, axstrs); 
   1.225 +      write_conjectures (out, tfree_clss@dfg_clss); 
   1.226 +      TextIO.output (out, "end_problem.\n");
   1.227 +      TextIO.closeOut out
   1.228    end;
   1.229  
   1.230  
   1.231 @@ -1037,11 +1053,11 @@
   1.232  
   1.233  fun gen_tptp_cls (cls_id,ax_name,knd,lits) = 
   1.234      "input_clause(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^ 
   1.235 -    knd ^ "," ^ lits ^ ").";
   1.236 +    knd ^ "," ^ lits ^ ").\n";
   1.237  
   1.238  fun gen_tptp_type_cls (cls_id,ax_name,knd,tfree_lit,idx) = 
   1.239      "input_clause(" ^ string_of_type_clsname (cls_id,ax_name,idx) ^ "," ^ 
   1.240 -    knd ^ ",[" ^ tfree_lit ^ "]).";
   1.241 +    knd ^ ",[" ^ tfree_lit ^ "]).\n";
   1.242  
   1.243  fun tptp_type_lits (Clause cls) = 
   1.244      let val lits = map tptp_literal (#literals cls)
   1.245 @@ -1086,8 +1102,8 @@
   1.246      end;
   1.247  
   1.248  
   1.249 -fun tfree_clause tfree_lit =
   1.250 -    "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "]).";
   1.251 +fun tptp_tfree_clause tfree_lit =
   1.252 +    "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "]).\n";
   1.253  
   1.254  
   1.255  fun tptp_of_arLit (TConsLit(b,(c,t,args))) =
   1.256 @@ -1115,7 +1131,7 @@
   1.257  	val all_lits = concl_lit :: prems_lits
   1.258      in
   1.259  	"input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ 
   1.260 -	(bracket_pack all_lits) ^ ")."
   1.261 +	(bracket_pack all_lits) ^ ").\n"
   1.262      end;
   1.263  
   1.264  fun tptp_classrelLits sub sup = 
   1.265 @@ -1129,7 +1145,26 @@
   1.266                          Int.toString clause_id
   1.267  	val lits = tptp_classrelLits (make_type_class subclass) (make_type_class superclass)
   1.268      in
   1.269 -	"input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")."
   1.270 +	"input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ").\n"
   1.271      end; 
   1.272  
   1.273 +(* write out a subgoal as tptp clauses to the file "xxxx_N"*)
   1.274 +fun tptp_write_file ths filename (axclauses,classrel_clauses,arity_clauses) =
   1.275 +  let
   1.276 +    val clss = make_conjecture_clauses (map prop_of ths)
   1.277 +    val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss)
   1.278 +    val tfree_clss = map tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
   1.279 +    val classrel_cls = map tptp_classrelClause classrel_clauses
   1.280 +    val arity_cls = map tptp_arity_clause arity_clauses
   1.281 +    val out = TextIO.openOut filename
   1.282 +  in
   1.283 +    List.app (writeln_strs out o tptp_clause) axclauses;
   1.284 +    writeln_strs out tfree_clss;
   1.285 +    writeln_strs out tptp_clss;
   1.286 +    writeln_strs out classrel_cls;
   1.287 +    writeln_strs out arity_cls;
   1.288 +    TextIO.closeOut out
   1.289 +  end;
   1.290 +
   1.291 +
   1.292  end;