# HG changeset patch # User wenzelm # Date 1121263644 -7200 # Node ID 014090d1e64b1b4113b9288d92d91987f77895e1 # Parent 6eeee59dac4cceb34e2ec1b2d4cee1ec7fe412f2 tuned; diff -r 6eeee59dac4c -r 014090d1e64b src/HOL/Tools/ATP/recon_prelim.ML --- a/src/HOL/Tools/ATP/recon_prelim.ML Wed Jul 13 16:07:23 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_prelim.ML Wed Jul 13 16:07:24 2005 +0200 @@ -3,29 +3,30 @@ Copyright 2004 University of Cambridge *) -val gcounter = ref 0; - +structure ReconPrelim = +struct fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg}; fun dest_neg(Const("Not",_) $ M) = M | dest_neg _ = raise USYN_ERR "dest_neg" "not a negation"; +fun iscomb a = + if is_Free a then + false + else if is_Var a then + false + else if USyntax.is_conj a then + false + else if USyntax.is_disj a then + false + else if USyntax.is_forall a then + false + else if USyntax.is_exists a then + false + else + true; -fun iscomb a = if is_Free a then - false - else if is_Var a then - false - else if USyntax.is_conj a then - false - else if USyntax.is_disj a then - false - else if USyntax.is_forall a then - false - else if USyntax.is_exists a then - false - else - true; fun getstring (Var (v,T)) = fst v |getstring (Free (v,T))= v; @@ -37,123 +38,95 @@ fun fstequal a b = a = fst b; -fun takeout (i,[]) = [] - | takeout (i,(x::xs)) = if (i>0) then - (x::(takeout(i-1,xs))) - else - []; - - - (* Presumably here, we would allow is_Var f for doing HOL, i.e. can subst for propositions *) fun is_Abs (Abs _) = true | is_Abs _ = false; fun is_Bound (Bound _) = true | is_Bound _ = false; - - - fun is_hol_tm t = - if (is_Free t) then - true - else if (is_Var t) then - true - else if (is_Const t) then - true - else if (is_Abs t) then - true - else if (is_Bound t) then - true - else - let val (f, args) = strip_comb t in - if ((is_Free f) orelse (is_Var f)) andalso (forall is_hol_tm args) then - true (* should be is_const *) - else - false - end; + if (is_Free t) then + true + else if (is_Var t) then + true + else if (is_Const t) then + true + else if (is_Abs t) then + true + else if (is_Bound t) then + true + else + let val (f, args) = strip_comb t in + if ((is_Free f) orelse (is_Var f)) andalso (forall is_hol_tm args) then + true (* should be is_const *) + else + false + end; -fun is_hol_fm f = if USyntax.is_neg f then - let val newf = USyntax.dest_neg f in - is_hol_fm newf - end - - else if USyntax.is_disj f then - let val {disj1,disj2} = USyntax.dest_disj f in - (is_hol_fm disj1) andalso (is_hol_fm disj2) (* shouldn't this be and ? *) - end - else if USyntax.is_conj f then - let val {conj1,conj2} = USyntax.dest_conj f in - (is_hol_fm conj1) andalso (is_hol_fm conj2) - end - else if (USyntax.is_forall f) then - let val {Body, Bvar} = USyntax.dest_forall f in - is_hol_fm Body - end - else if (USyntax.is_exists f) then - let val {Body, Bvar} = USyntax.dest_exists f in - is_hol_fm Body - end - else if (iscomb f) then - let val (P, args) = strip_comb f in - ((is_hol_tm P)) andalso (forall is_hol_fm args) - end - else - is_hol_tm f; (* should be is_const, nee -d to check args *) - +fun is_hol_fm f = + if USyntax.is_neg f then + let val newf = USyntax.dest_neg f in + is_hol_fm newf + end + else if USyntax.is_disj f then + let val {disj1,disj2} = USyntax.dest_disj f in + (is_hol_fm disj1) andalso (is_hol_fm disj2) (* shouldn't this be and ? *) + end + else if USyntax.is_conj f then + let val {conj1,conj2} = USyntax.dest_conj f in + (is_hol_fm conj1) andalso (is_hol_fm conj2) + end + else if (USyntax.is_forall f) then + let val {Body, Bvar} = USyntax.dest_forall f in + is_hol_fm Body + end + else if (USyntax.is_exists f) then + let val {Body, Bvar} = USyntax.dest_exists f in + is_hol_fm Body + end + else if (iscomb f) then + let val (P, args) = strip_comb f in + ((is_hol_tm P)) andalso (forall is_hol_fm args) + end + else + is_hol_tm f; (* should be is_const, need to check args *) -fun hol_literal t = - (is_hol_fm t) andalso - ( not ((USyntax.is_conj t) orelse (USyntax.is_disj t) orelse (USyntax.is_forall t) orelse (USyntax.is_exists t))); - - +fun hol_literal t = + is_hol_fm t andalso + (not (USyntax.is_conj t orelse USyntax.is_disj t orelse USyntax.is_forall t + orelse USyntax.is_exists t)); (*PROBLEM HERE WITH THINGS THAT HAVE TWO RANDS e.g. P x y *) -fun getcombvar a = let val {Rand = rand, Rator = rator} = USyntax.dest_comb a in - if (iscomb rand) then - getcombvar rand - else - rand - end; - - - -fun free2var v = let val thing = dest_Free v - val (name,vtype) = thing - val index = (name,0) in - Var (index,vtype) - end; +fun getcombvar a = + let val {Rand = rand, Rator = rator} = USyntax.dest_comb a in + if (iscomb rand) then + getcombvar rand + else + rand + end; -fun var2free v = let val (index, tv) = dest_Var v - val istr = fst index in - Free (istr,tv) - end; - -fun is_empty_seq thisseq = case Seq.chop (1, thisseq) of - ([],_) => true - | _ => false +fun free2var v = + let val (name, vtype) = dest_Free v + in Var ((name, 0), vtype) end; -fun getnewenv thisseq = - let val seqlist = Seq.list_of thisseq - val envpair =hd seqlist in - fst envpair - end; +fun var2free v = + let val ((x, _), tv) = dest_Var v + in Free (x, tv) end; -fun getnewsubsts thisseq = let val seqlist = Seq.list_of thisseq - val envpair =hd seqlist in - snd envpair - end; +val is_empty_seq = is_none o Seq.pull; - +fun getnewenv seq = fst (fst (the (Seq.pull seq))); +fun getnewsubsts seq = snd (fst (the (Seq.pull seq))); fun prover s = prove_goal HOL.thy s (fn _ => [blast_tac HOL_cs 1]); - +fun int_of_string str = + (case Int.fromString str of SOME n => n + | NONE => error ("int_of_string: " ^ str)); -fun int_of_string str = valOf (Int.fromString str) - handle Option => error ("int_of_string: " ^ str); - - +val no_lines = filter_out (equal "\n"); + exception ASSERTION of string; + +end; diff -r 6eeee59dac4c -r 014090d1e64b src/HOL/Tools/ATP/recon_transfer_proof.ML --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Wed Jul 13 16:07:23 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Wed Jul 13 16:07:24 2005 +0200 @@ -9,11 +9,11 @@ structure Recon_Transfer = struct + open Recon_Parse + infixr 8 ++; infixr 7 >>; infixr 6 ||; -fun not_newline ch = not (ch = "\n"); - (* @@ -51,14 +51,9 @@ (* Versions that include type information *) +(* FIXME rename to str_of_thm *) fun string_of_thm thm = - let val _ = set show_sorts - val str = Display.string_of_thm thm - val no_returns =List.filter not_newline (explode str) - val _ = reset show_sorts - in - implode no_returns - end + setmp show_sorts true (Pretty.str_of o Display.pretty_thm) thm; (* check separate args in the watcher program for separating strings with a * or ; or something *) @@ -377,31 +372,16 @@ \1453[0:Rew:1279.0,1430.0,1242.0,1430.0,1279.0,1430.0] || equal(const_0,const_0)* -> .\ \1454[0:Obv:1453.0] || -> .";*) -fun remove_linebreaks str = let val strlist = explode str - val nonewlines = filter (not_equal "\n") strlist - in - implode nonewlines - end - +fun subst_for a b [] = "" + | subst_for a b (x :: xs) = + if x = a + then + b ^ subst_for a b xs + else + x ^ subst_for a b xs; -fun subst_for a b [] = "" -| subst_for a b (x::xs) = if (x = a) - then - (b^(subst_for a b xs)) - else - x^(subst_for a b xs) - - -fun remove_linebreaks str = let val strlist = explode str - in - subst_for "\n" "\t" strlist - end - -fun restore_linebreaks str = let val strlist = explode str - in - subst_for "\t" "\n" strlist - end - +val remove_linebreaks = subst_for "\n" "\t" o explode; +val restore_linebreaks = subst_for "\t" "\n" o explode; fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses = diff -r 6eeee59dac4c -r 014090d1e64b src/HOL/Tools/ATP/recon_translate_proof.ML --- a/src/HOL/Tools/ATP/recon_translate_proof.ML Wed Jul 13 16:07:23 2005 +0200 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Wed Jul 13 16:07:24 2005 +0200 @@ -3,6 +3,11 @@ Copyright 2004 University of Cambridge *) +structure ReconTranslateProof = +struct + +open ReconPrelim; + fun add_in_order (x:string) [] = [x] | add_in_order (x:string) ((y:string)::ys) = if (x < y) then @@ -15,10 +20,6 @@ fun thm_vars thm = map (fn ((name,ix),_) => name) (Drule.vars_of thm); -Goal "False ==> False"; -by Auto_tac; -qed "False_imp"; - exception Reflex_equal; (********************************) @@ -28,7 +29,7 @@ datatype Side = Left |Right - datatype Proofstep = ExtraAxiom +datatype Proofstep = ExtraAxiom | OrigAxiom | VampInput | Axiom @@ -424,15 +425,13 @@ end -fun not_newline ch = not (ch = "\n"); - (* fun follow clauses [] allvars thml recons = let (* val _ = reset show_sorts*) val thmstring = Meson.concat_with_and (map string_of_thm (map snd thml)) val thmproofstring = proofstring ( thmstring) - val no_returns =List.filter not_newline ( thmproofstring) + val no_returns = no_lines thmproofstring val thmstr = implode no_returns val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "thml_file"))) val _ = TextIO.output(outfile, "thmstr is "^thmstr) @@ -502,3 +501,5 @@ fun remove_tinfo [] = [] | remove_tinfo ( (clausenum, step, T_info, newstrs)::xs) = (clausenum, step , newstrs)::(remove_tinfo xs) + +end; diff -r 6eeee59dac4c -r 014090d1e64b src/HOL/Tools/res_skolem_function.ML --- a/src/HOL/Tools/res_skolem_function.ML Wed Jul 13 16:07:23 2005 +0200 +++ b/src/HOL/Tools/res_skolem_function.ML Wed Jul 13 16:07:24 2005 +0200 @@ -2,55 +2,28 @@ ID: $Id$ Copyright 2004 University of Cambridge -Generation of unique Skolem functions (with types) as Term.term. +Generation of unique Skolem functions (with types) as term. *) signature RES_SKOLEM_FUNCTION = sig - -val gen_skolem: Term.term list -> Term.typ -> Term.term - + val gen_skolem: term list -> typ -> term end; structure ResSkolemFunction: RES_SKOLEM_FUNCTION = - struct val skolem_prefix = "sk_"; - -(* internal reference starting from 0. *) val skolem_id = ref 0; - -fun gen_skolem_name () = - let val new_id = !skolem_id - val sk_fun = skolem_prefix ^ (string_of_int new_id) - in - (skolem_id := new_id + 1; sk_fun) (* increment id by 1. *) - end; - -fun sk_type_of_aux [Var(_,tp1)] tp = Type("fun",[tp1,tp]) - | sk_type_of_aux (Var(_,tp1)::vars) tp = - let val tp' = sk_type_of_aux vars tp - in - Type("fun",[tp1,tp']) - end; - +fun gen_skolem_name () = + let val sk_fun = skolem_prefix ^ string_of_int (! skolem_id); + in inc skolem_id; sk_fun end; -fun sk_type_of [] tp = tp - | sk_type_of vars tp = sk_type_of_aux vars tp; - - +fun gen_skolem univ_vars tp = + let + val skolem_type = map Term.fastype_of univ_vars ---> tp + val skolem_term = Const (gen_skolem_name (), skolem_type) + in Term.list_comb (skolem_term, univ_vars) end; -fun gen_skolem univ_vars tp = - let val new_sk_name = gen_skolem_name () - val new_sk_type = sk_type_of univ_vars tp - val skolem_term = Const(new_sk_name,new_sk_type) - fun app [] sf = sf - | app (var::vars) sf= app vars (sf $ var) - in - app univ_vars skolem_term - end; - - -end; \ No newline at end of file +end; diff -r 6eeee59dac4c -r 014090d1e64b src/HOL/Tools/res_types_sorts.ML --- a/src/HOL/Tools/res_types_sorts.ML Wed Jul 13 16:07:23 2005 +0200 +++ b/src/HOL/Tools/res_types_sorts.ML Wed Jul 13 16:07:24 2005 +0200 @@ -10,20 +10,16 @@ sig exception ARITIES of string val arity_clause: string * (string * string list list) list -> ResClause.arityClause list - val arity_clause_sg: Sign.sg -> ResClause.arityClause list list * (string * 'a list) list val arity_clause_thy: theory -> ResClause.arityClause list list * (string * 'a list) list type classrelClauses val classrel_clause: string * string list -> ResClause.classrelClause list val classrel_clauses_classrel: Sorts.classes -> ResClause.classrelClause list list - val classrel_clauses_sg: Sign.sg -> ResClause.classrelClause list list val classrel_clauses_thy: theory -> ResClause.classrelClause list list - val classrel_of_sg: Sign.sg -> Sorts.classes val multi_arity_clause: (string * (string * string list list) list) list -> (string * 'a list) list -> ResClause.arityClause list list * (string * 'a list) list val tptp_arity_clause_thy: theory -> string list list - val tptp_classrel_clauses_sg : Sign.sg -> string list list end; structure ResTypesSorts: RES_TYPES_SORTS = @@ -45,12 +41,10 @@ let val result = multi_arity_clause tcons_ars expts in ((arity_clause tcon_ar :: fst result), snd result) end; -fun arity_clause_sg sg = - let val arities = #arities (Type.rep_tsig (Sign.tsig_of sg)) +fun arity_clause_thy thy = + let val arities = #arities (Type.rep_tsig (Sign.tsig_of thy)) in multi_arity_clause (Symtab.dest arities) [] end; -fun arity_clause_thy thy = arity_clause_sg (Theory.sign_of thy); - fun tptp_arity_clause_thy thy = map (map ResClause.tptp_arity_clause) (#1 (arity_clause_thy thy)); @@ -59,13 +53,12 @@ type classrelClauses = ResClause.classrelClause list Symtab.table; -val classrel_of_sg = #2 o #classes o Type.rep_tsig o Sign.tsig_of; +val classrel_of = #2 o #classes o Type.rep_tsig o Sign.tsig_of; val classrel_clause = ResClause.classrelClauses_of; fun classrel_clauses_classrel (C: Sorts.classes) = map classrel_clause (Graph.dest C); -val classrel_clauses_sg = classrel_clauses_classrel o classrel_of_sg; -val classrel_clauses_thy = classrel_clauses_sg o Theory.sign_of; +val classrel_clauses_thy = classrel_clauses_classrel o classrel_of; -val tptp_classrel_clauses_sg = - map (map ResClause.tptp_classrelClause) o classrel_clauses_sg; +val tptp_classrel_clauses_thy = + map (map ResClause.tptp_classrelClause) o classrel_clauses_thy; end; diff -r 6eeee59dac4c -r 014090d1e64b src/Pure/General/scan.ML --- a/src/Pure/General/scan.ML Wed Jul 13 16:07:23 2005 +0200 +++ b/src/Pure/General/scan.ML Wed Jul 13 16:07:24 2005 +0200 @@ -259,7 +259,7 @@ in if exists is_stopper input then raise ABORT "Stopper may not occur in input of finite scan!" - else (force scan --| lift stop) (state, List.revAppend (rev input, [stopper])) + else (force scan --| lift stop) (state, input @ [stopper]) end; fun finite stopper scan = unlift (finite' stopper (lift scan)); diff -r 6eeee59dac4c -r 014090d1e64b src/Pure/theory.ML --- a/src/Pure/theory.ML Wed Jul 13 16:07:23 2005 +0200 +++ b/src/Pure/theory.ML Wed Jul 13 16:07:24 2005 +0200 @@ -179,7 +179,7 @@ val axioms_of = Symtab.dest o #2 o #axioms o rep_theory; fun all_axioms_of thy = List.concat (map axioms_of (thy :: ancestors_of thy)); -fun defs_of thy = (case rep_theory thy of {defs=D, ...} => D) +val defs_of = #defs o rep_theory; fun requires thy name what = if Context.exists_name name thy then ()