New ATP option: full types
authornipkow
Wed Jun 24 15:51:07 2009 +0200 (2009-06-24)
changeset 31791c9a1caf218c8
parent 31790 05c92381363c
child 31792 d5a6096b94ad
child 31908 67224d7d4448
New ATP option: full types
src/HOL/Tools/atp_manager.ML
src/HOL/Tools/atp_wrapper.ML
src/HOL/Tools/res_hol_clause.ML
     1.1 --- a/src/HOL/Tools/atp_manager.ML	Wed Jun 24 09:41:14 2009 +0200
     1.2 +++ b/src/HOL/Tools/atp_manager.ML	Wed Jun 24 15:51:07 2009 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4    val set_max_atps: int -> unit
     1.5    val get_timeout: unit -> int
     1.6    val set_timeout: int -> unit
     1.7 +  val get_full_types: unit -> bool
     1.8    val kill: unit -> unit
     1.9    val info: unit -> unit
    1.10    val messages: int option -> unit
    1.11 @@ -42,6 +43,7 @@
    1.12  val atps = ref "e remote_vampire";
    1.13  val max_atps = ref 5;   (* ~1 means infinite number of atps *)
    1.14  val timeout = ref 60;
    1.15 +val full_types = ref false;
    1.16  
    1.17  in
    1.18  
    1.19 @@ -54,6 +56,8 @@
    1.20  fun get_timeout () = CRITICAL (fn () => ! timeout);
    1.21  fun set_timeout time = CRITICAL (fn () => timeout := time);
    1.22  
    1.23 +fun get_full_types () = CRITICAL (fn () => ! full_types);
    1.24 +
    1.25  val _ =
    1.26    ProofGeneralPgip.add_preference Preferences.category_proof
    1.27      (Preferences.string_pref atps
    1.28 @@ -69,6 +73,11 @@
    1.29      (Preferences.int_pref timeout
    1.30        "ATP: timeout" "ATPs will be interrupted after this time (in seconds)");
    1.31  
    1.32 +val _ =
    1.33 +  ProofGeneralPgip.add_preference Preferences.category_proof
    1.34 +    (Preferences.bool_pref full_types
    1.35 +      "ATP: full types" "ATPs will use full type information");
    1.36 +
    1.37  end;
    1.38  
    1.39  
     2.1 --- a/src/HOL/Tools/atp_wrapper.ML	Wed Jun 24 09:41:14 2009 +0200
     2.2 +++ b/src/HOL/Tools/atp_wrapper.ML	Wed Jun 24 15:51:07 2009 +0200
     2.3 @@ -109,7 +109,7 @@
     2.4    external_prover
     2.5    (ResAtp.get_relevant max_new theory_const)
     2.6    (ResAtp.prepare_clauses false)
     2.7 -  (ResHolClause.tptp_write_file)
     2.8 +  (ResHolClause.tptp_write_file (AtpManager.get_full_types()))
     2.9    command
    2.10    ResReconstruct.find_failure
    2.11    (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp)
    2.12 @@ -173,7 +173,7 @@
    2.13  fun spass_opts max_new theory_const timeout ax_clauses fcls name n goal = external_prover
    2.14    (ResAtp.get_relevant max_new theory_const)
    2.15    (ResAtp.prepare_clauses true)
    2.16 -  ResHolClause.dfg_write_file
    2.17 +  (ResHolClause.dfg_write_file (AtpManager.get_full_types()))
    2.18    (Path.explode "$SPASS_HOME/SPASS",
    2.19      "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout)
    2.20    ResReconstruct.find_failure
     3.1 --- a/src/HOL/Tools/res_hol_clause.ML	Wed Jun 24 09:41:14 2009 +0200
     3.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Wed Jun 24 15:51:07 2009 +0200
     3.3 @@ -37,9 +37,9 @@
     3.4         bool ->
     3.5         clause list * (thm * (axiom_name * clause_id)) list * string list ->
     3.6         clause list
     3.7 -  val tptp_write_file: string ->
     3.8 +  val tptp_write_file: bool -> string ->
     3.9      clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit
    3.10 -  val dfg_write_file: string -> 
    3.11 +  val dfg_write_file: bool -> string -> 
    3.12      clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit
    3.13  end
    3.14  
    3.15 @@ -227,8 +227,8 @@
    3.16  fun head_needs_hBOOL const_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL const_needs_hBOOL c
    3.17    | head_needs_hBOOL const_needs_hBOOL _ = true;
    3.18  
    3.19 -fun wrap_type (s, tp) =
    3.20 -  if typ_level=T_FULL then
    3.21 +fun wrap_type t_full (s, tp) =
    3.22 +  if t_full then
    3.23        type_wrapper ^ RC.paren_pack [s, RC.string_of_fol_type tp]
    3.24    else s;
    3.25  
    3.26 @@ -241,7 +241,7 @@
    3.27  
    3.28  (*Apply an operator to the argument strings, using either the "apply" operator or
    3.29    direct function application.*)
    3.30 -fun string_of_applic cma (CombConst(c,tp,tvars), args) =
    3.31 +fun string_of_applic t_full cma (CombConst(c,tp,tvars), args) =
    3.32        let val c = if c = "equal" then "c_fequal" else c
    3.33            val nargs = min_arity_of cma c
    3.34            val args1 = List.take(args, nargs)
    3.35 @@ -249,35 +249,37 @@
    3.36                                           Int.toString nargs ^ " but is applied to " ^
    3.37                                           space_implode ", " args)
    3.38            val args2 = List.drop(args, nargs)
    3.39 -          val targs = if typ_level = T_CONST then map RC.string_of_fol_type tvars
    3.40 +          val targs = if not t_full then map RC.string_of_fol_type tvars
    3.41                        else []
    3.42        in
    3.43            string_apply (c ^ RC.paren_pack (args1@targs), args2)
    3.44        end
    3.45 -  | string_of_applic cma (CombVar(v,tp), args) = string_apply (v, args)
    3.46 -  | string_of_applic _ _ = error "string_of_applic";
    3.47 -
    3.48 -fun wrap_type_if cnh (head, s, tp) = if head_needs_hBOOL cnh head then wrap_type (s, tp) else s;
    3.49 +  | string_of_applic _ cma (CombVar(v,tp), args) = string_apply (v, args)
    3.50 +  | string_of_applic _ _ _ = error "string_of_applic";
    3.51  
    3.52 -fun string_of_combterm cma cnh t =
    3.53 +fun wrap_type_if t_full cnh (head, s, tp) =
    3.54 +  if head_needs_hBOOL cnh head then wrap_type t_full (s, tp) else s;
    3.55 +
    3.56 +fun string_of_combterm t_full cma cnh t =
    3.57    let val (head, args) = strip_comb t
    3.58 -  in  wrap_type_if cnh (head,
    3.59 -                    string_of_applic cma (head, map (string_of_combterm cma cnh) args),
    3.60 +  in  wrap_type_if t_full cnh (head,
    3.61 +                    string_of_applic t_full cma (head, map (string_of_combterm t_full cma cnh) args),
    3.62                      type_of_combterm t)
    3.63    end;
    3.64  
    3.65  (*Boolean-valued terms are here converted to literals.*)
    3.66 -fun boolify cma cnh t = "hBOOL" ^ RC.paren_pack [string_of_combterm cma cnh t];
    3.67 +fun boolify t_full cma cnh t =
    3.68 +  "hBOOL" ^ RC.paren_pack [string_of_combterm t_full cma cnh t];
    3.69  
    3.70 -fun string_of_predicate cma cnh t =
    3.71 +fun string_of_predicate t_full cma cnh t =
    3.72    case t of
    3.73        (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) =>
    3.74            (*DFG only: new TPTP prefers infix equality*)
    3.75 -          ("equal" ^ RC.paren_pack [string_of_combterm cma cnh t1, string_of_combterm cma cnh t2])
    3.76 +          ("equal" ^ RC.paren_pack [string_of_combterm t_full cma cnh t1, string_of_combterm t_full cma cnh t2])
    3.77      | _ =>
    3.78            case #1 (strip_comb t) of
    3.79 -              CombConst(c,_,_) => if needs_hBOOL cnh c then boolify cma cnh t else string_of_combterm cma cnh t
    3.80 -            | _ => boolify cma cnh t;
    3.81 +              CombConst(c,_,_) => if needs_hBOOL cnh c then boolify t_full cma cnh t else string_of_combterm t_full cma cnh t
    3.82 +            | _ => boolify t_full cma cnh t;
    3.83  
    3.84  fun string_of_clausename (cls_id,ax_name) =
    3.85      RC.clause_prefix ^ RC.ascii_of ax_name ^ "_" ^ Int.toString cls_id;
    3.86 @@ -288,23 +290,23 @@
    3.87  
    3.88  (*** tptp format ***)
    3.89  
    3.90 -fun tptp_of_equality cma cnh pol (t1,t2) =
    3.91 +fun tptp_of_equality t_full cma cnh pol (t1,t2) =
    3.92    let val eqop = if pol then " = " else " != "
    3.93 -  in  string_of_combterm cma cnh t1 ^ eqop ^ string_of_combterm cma cnh t2  end;
    3.94 +  in  string_of_combterm t_full cma cnh t1 ^ eqop ^ string_of_combterm t_full cma cnh t2  end;
    3.95  
    3.96 -fun tptp_literal cma cnh (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) =
    3.97 -      tptp_of_equality cma cnh pol (t1,t2)
    3.98 -  | tptp_literal cma cnh (Literal(pol,pred)) =
    3.99 -      RC.tptp_sign pol (string_of_predicate cma cnh pred);
   3.100 +fun tptp_literal t_full cma cnh (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) =
   3.101 +      tptp_of_equality t_full cma cnh pol (t1,t2)
   3.102 +  | tptp_literal t_full cma cnh (Literal(pol,pred)) =
   3.103 +      RC.tptp_sign pol (string_of_predicate t_full cma cnh pred);
   3.104  
   3.105  (*Given a clause, returns its literals paired with a list of literals concerning TFrees;
   3.106    the latter should only occur in conjecture clauses.*)
   3.107 -fun tptp_type_lits cma cnh pos (Clause{literals, ctypes_sorts, ...}) =
   3.108 -      (map (tptp_literal cma cnh) literals, 
   3.109 +fun tptp_type_lits t_full cma cnh pos (Clause{literals, ctypes_sorts, ...}) =
   3.110 +      (map (tptp_literal t_full cma cnh) literals, 
   3.111         map (RC.tptp_of_typeLit pos) (RC.add_typs ctypes_sorts));
   3.112  
   3.113 -fun clause2tptp (cma, cnh) (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
   3.114 -  let val (lits,tylits) = tptp_type_lits cma cnh (kind = RC.Conjecture) cls
   3.115 +fun clause2tptp (t_full, cma, cnh) (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
   3.116 +  let val (lits,tylits) = tptp_type_lits t_full cma cnh (kind = RC.Conjecture) cls
   3.117    in
   3.118        (RC.gen_tptp_cls(clause_id,axiom_name,kind,lits,tylits), tylits)
   3.119    end;
   3.120 @@ -312,10 +314,10 @@
   3.121  
   3.122  (*** dfg format ***)
   3.123  
   3.124 -fun dfg_literal cma cnh (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate cma cnh pred);
   3.125 +fun dfg_literal t_full cma cnh (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate t_full cma cnh pred);
   3.126  
   3.127 -fun dfg_type_lits cma cnh pos (Clause{literals, ctypes_sorts, ...}) =
   3.128 -      (map (dfg_literal cma cnh) literals, 
   3.129 +fun dfg_type_lits t_full cma cnh pos (Clause{literals, ctypes_sorts, ...}) =
   3.130 +      (map (dfg_literal t_full cma cnh) literals, 
   3.131         map (RC.dfg_of_typeLit pos) (RC.add_typs ctypes_sorts));
   3.132  
   3.133  fun get_uvars (CombConst _) vars = vars
   3.134 @@ -326,8 +328,8 @@
   3.135  
   3.136  fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals);
   3.137  
   3.138 -fun clause2dfg (cma, cnh) (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
   3.139 -  let val (lits,tylits) = dfg_type_lits cma cnh (kind = RC.Conjecture) cls
   3.140 +fun clause2dfg (t_full, cma, cnh) (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
   3.141 +  let val (lits,tylits) = dfg_type_lits t_full cma cnh (kind = RC.Conjecture) cls
   3.142        val vars = dfg_vars cls
   3.143        val tvars = RC.get_tvar_strs ctypes_sorts
   3.144    in
   3.145 @@ -339,30 +341,30 @@
   3.146  
   3.147  fun addtypes tvars tab = List.foldl RC.add_foltype_funcs tab tvars;
   3.148  
   3.149 -fun add_decls cma cnh (CombConst(c,tp,tvars), (funcs,preds)) =
   3.150 +fun add_decls t_full cma cnh (CombConst(c,tp,tvars), (funcs,preds)) =
   3.151        if c = "equal" then (addtypes tvars funcs, preds)
   3.152        else
   3.153  	let val arity = min_arity_of cma c
   3.154 -	    val ntys = if typ_level = T_CONST then length tvars else 0
   3.155 +	    val ntys = if not t_full then length tvars else 0
   3.156  	    val addit = Symtab.update(c, arity+ntys)
   3.157  	in
   3.158  	    if needs_hBOOL cnh c then (addtypes tvars (addit funcs), preds)
   3.159  	    else (addtypes tvars funcs, addit preds)
   3.160  	end
   3.161 -  | add_decls _ _ (CombVar(_,ctp), (funcs,preds)) =
   3.162 +  | add_decls _ _ _ (CombVar(_,ctp), (funcs,preds)) =
   3.163        (RC.add_foltype_funcs (ctp,funcs), preds)
   3.164 -  | add_decls cma cnh (CombApp(P,Q),decls) = add_decls cma cnh (P,add_decls cma cnh (Q,decls));
   3.165 +  | add_decls t_full cma cnh (CombApp(P,Q),decls) = add_decls t_full cma cnh (P,add_decls t_full cma cnh (Q,decls));
   3.166  
   3.167 -fun add_literal_decls cma cnh (Literal(_,c), decls) = add_decls cma cnh (c,decls);
   3.168 +fun add_literal_decls t_full cma cnh (Literal(_,c), decls) = add_decls t_full cma cnh (c,decls);
   3.169  
   3.170 -fun add_clause_decls cma cnh (Clause {literals, ...}, decls) =
   3.171 -    List.foldl (add_literal_decls cma cnh) decls literals
   3.172 +fun add_clause_decls t_full cma cnh (Clause {literals, ...}, decls) =
   3.173 +    List.foldl (add_literal_decls t_full cma cnh) decls literals
   3.174      handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
   3.175  
   3.176 -fun decls_of_clauses (cma, cnh) clauses arity_clauses =
   3.177 +fun decls_of_clauses (t_full, cma, cnh) clauses arity_clauses =
   3.178    let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) RC.init_functab)
   3.179        val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
   3.180 -      val (functab,predtab) = (List.foldl (add_clause_decls cma cnh) (init_functab, init_predtab) clauses)
   3.181 +      val (functab,predtab) = (List.foldl (add_clause_decls t_full cma cnh) (init_functab, init_predtab) clauses)
   3.182    in
   3.183        (Symtab.dest (List.foldl RC.add_arityClause_funcs functab arity_clauses),
   3.184         Symtab.dest predtab)
   3.185 @@ -471,37 +473,39 @@
   3.186  
   3.187  (* tptp format *)
   3.188  
   3.189 -fun tptp_write_file filename clauses =
   3.190 +fun tptp_write_file t_full filename clauses =
   3.191    let
   3.192      val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
   3.193 -    val const_counts = count_constants clauses
   3.194 -    val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp const_counts) conjectures)
   3.195 +    val (cma, cnh) = count_constants clauses
   3.196 +    val params = (t_full, cma, cnh)
   3.197 +    val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
   3.198      val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss)
   3.199      val out = TextIO.openOut filename
   3.200    in
   3.201 -    List.app (curry TextIO.output out o #1 o (clause2tptp const_counts)) axclauses;
   3.202 +    List.app (curry TextIO.output out o #1 o (clause2tptp params)) axclauses;
   3.203      RC.writeln_strs out tfree_clss;
   3.204      RC.writeln_strs out tptp_clss;
   3.205      List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses;
   3.206      List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses;
   3.207 -    List.app (curry TextIO.output out o #1 o (clause2tptp const_counts)) helper_clauses;
   3.208 +    List.app (curry TextIO.output out o #1 o (clause2tptp params)) helper_clauses;
   3.209      TextIO.closeOut out
   3.210    end;
   3.211  
   3.212  
   3.213  (* dfg format *)
   3.214  
   3.215 -fun dfg_write_file filename clauses =
   3.216 +fun dfg_write_file t_full filename clauses =
   3.217    let
   3.218      val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
   3.219 -    val const_counts = count_constants clauses
   3.220 -    val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg const_counts) conjectures)
   3.221 +    val (cma, cnh) = count_constants clauses
   3.222 +    val params = (t_full, cma, cnh)
   3.223 +    val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
   3.224      and probname = Path.implode (Path.base (Path.explode filename))
   3.225 -    val axstrs = map (#1 o (clause2dfg const_counts)) axclauses
   3.226 +    val axstrs = map (#1 o (clause2dfg params)) axclauses
   3.227      val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss)
   3.228      val out = TextIO.openOut filename
   3.229 -    val helper_clauses_strs = map (#1 o (clause2dfg const_counts)) helper_clauses
   3.230 -    val (funcs,cl_preds) = decls_of_clauses const_counts (helper_clauses @ conjectures @ axclauses) arity_clauses
   3.231 +    val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses
   3.232 +    val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
   3.233      and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
   3.234    in
   3.235      TextIO.output (out, RC.string_of_start probname);