--- 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;
--- 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 =
--- 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;
--- 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;
--- 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;
--- 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));
--- 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 ()