1.1 --- a/src/HOL/Tools/res_atp_setup.ML Wed Apr 19 10:41:37 2006 +0200
1.2 +++ b/src/HOL/Tools/res_atp_setup.ML Wed Apr 19 10:42:13 2006 +0200
1.3 @@ -325,12 +325,15 @@
1.4 SOME cls => (FOLClause cls) :: cls_axiom true name (i+1) tms
1.5 | NONE => cls_axiom true name i tms)
1.6 else
1.7 - (HOLClause (ResHolClause.make_axiom_clause tm (name,i))) :: (cls_axiom false name (i+1) tms);
1.8 + HOLClause (ResHolClause.make_axiom_clause tm (name,i)) ::
1.9 + cls_axiom false name (i+1) tms;
1.10
1.11
1.12 fun filtered_tptp_axiom is_fol name clss =
1.13 - (fst(ListPair.unzip (map clause2tptp (filter (fn c => not (isTaut c)) (cls_axiom is_fol name 0 clss)))),[])
1.14 - handle _ => ([],[name]);
1.15 + (fst
1.16 + (ListPair.unzip
1.17 + (map clause2tptp (filter (fn c => not (isTaut c)) (cls_axiom is_fol name 0 clss)))),
1.18 + []) handle _ => ([],[name]);
1.19
1.20 fun tptp_axioms_aux _ [] err = ([],err)
1.21 | tptp_axioms_aux is_fol ((name,clss)::nclss) err =
1.22 @@ -427,23 +430,26 @@
1.23 datatype mode = Auto | Fol | Hol;
1.24
1.25 fun write_out logic (claR,simpR,userR,hyp_cls,conj_cls,n,err) =
1.26 - let val is_fol = is_fol_logic logic
1.27 - val (files1,err1) = if (null claR) then ([],[]) else (atp_axioms is_fol claR (claset_file()))
1.28 - val (files2,err2) = if (null simpR) then ([],[]) else (atp_axioms is_fol simpR (simpset_file ()))
1.29 - val (files3,err3) = if (null userR) then ([],[]) else (atp_axioms is_fol userR (local_lemma_file ()))
1.30 - val files4 = atp_conjectures is_fol hyp_cls conj_cls n
1.31 - val errs = err1 @ err2 @ err3 @ err
1.32 - val logic' = if !include_combS then HOLCS
1.33 - else
1.34 - if !include_min_comb then HOLC else logic
1.35 - val _ = warning ("Problems are " ^ (string_of_logic logic'))
1.36 - val _ = if (null errs) then () else warning ("Can't clausify thms: " ^ (ResClause.paren_pack errs))
1.37 - val helpers = case logic' of FOL => []
1.38 - | HOL => [HOL_helper1 ()]
1.39 - | _ => [HOL_helper1(),HOL_comb()] (*HOLC or HOLCS*)
1.40 - in
1.41 - (helpers,files4 @ files1 @ files2 @ files3)
1.42 - end;
1.43 + let val is_fol = is_fol_logic logic
1.44 + val (files1,err1) = if (null claR) then ([],[])
1.45 + else (atp_axioms is_fol claR (claset_file()))
1.46 + val (files2,err2) = if (null simpR) then ([],[])
1.47 + else (atp_axioms is_fol simpR (simpset_file ()))
1.48 + val (files3,err3) = if (null userR) then ([],[])
1.49 + else (atp_axioms is_fol userR (local_lemma_file ()))
1.50 + val files4 = atp_conjectures is_fol hyp_cls conj_cls n
1.51 + val errs = err1 @ err2 @ err3 @ err
1.52 + val logic' = if !include_combS then HOLCS
1.53 + else
1.54 + if !include_min_comb then HOLC else logic
1.55 + val _ = warning ("Problems are " ^ (string_of_logic logic'))
1.56 + val _ = if (null errs) then () else warning ("Can't clausify thms: " ^ (ResClause.paren_pack errs))
1.57 + val helpers = case logic' of FOL => []
1.58 + | HOL => [HOL_helper1 ()]
1.59 + | _ => [HOL_helper1(),HOL_comb()] (*HOLC or HOLCS*)
1.60 + in
1.61 + (helpers,files4 @ files1 @ files2 @ files3)
1.62 + end;
1.63
1.64
1.65 fun write_out_ts is_fol ctxt (claR,simpR,userR,hyp_cls,conj_cls,n,err) =
1.66 @@ -457,7 +463,8 @@
1.67
1.68 fun prep_atp_input mode ctxt conjectures user_thms n =
1.69 let val conj_cls = map prop_of (make_clauses conjectures)
1.70 - val (userR,simpR,claR,errs) = cnf_rules_tms ctxt user_thms (!include_claset,!include_simpset)
1.71 + val (userR,simpR,claR,errs) =
1.72 + cnf_rules_tms ctxt user_thms (!include_claset,!include_simpset)
1.73 val hyp_cls = map prop_of (cnf_hyps_thms ctxt)
1.74 val logic = case mode of Auto => problem_logic (conj_cls,hyp_cls,userR,claR,simpR)
1.75 | Fol => FOL