--- a/src/HOL/Integ/cooper_dec.ML Thu Apr 26 13:33:09 2007 +0200
+++ b/src/HOL/Integ/cooper_dec.ML Thu Apr 26 13:33:12 2007 +0200
@@ -512,16 +512,13 @@
(*list_disj[conj] makes a disj[conj] of a given list. used with conjucts or disjuncts
it liearises iterated conj[disj]unctions. *)
-fun disj_help p q = HOLogic.disj $ p $ q ;
-
-fun list_disj l =
- if l = [] then HOLogic.false_const else Utils.end_itlist disj_help l;
-
-fun conj_help p q = HOLogic.conj $ p $ q ;
-
-fun list_conj l =
- if l = [] then HOLogic.true_const else Utils.end_itlist conj_help l;
-
+fun list_disj [] = HOLogic.false_const
+ | list_disj ps = foldr1 (fn (p, q) => HOLogic.disj $ p $ q) ps;
+
+fun list_conj [] = HOLogic.true_const
+ | list_conj ps = foldr1 (fn (p, q) => HOLogic.conj $ p $ q) ps;
+
+
(*Simplification of Formulas *)
(*Function q_bnd_chk checks if a quantified Formula makes sens : Means if in
--- a/src/HOL/Library/EfficientNat.thy Thu Apr 26 13:33:09 2007 +0200
+++ b/src/HOL/Library/EfficientNat.thy Thu Apr 26 13:33:12 2007 +0200
@@ -6,7 +6,7 @@
header {* Implementation of natural numbers by integers *}
theory EfficientNat
-imports Main
+imports Main Pretty_Int
begin
text {*
@@ -34,7 +34,7 @@
lemma nat_of_int_of_number_of:
fixes k
assumes "k \<ge> 0"
- shows "number_of k = nat_of_int k"
+ shows "number_of k = nat_of_int (number_of k)"
unfolding nat_of_int_def [OF prems] nat_number_of_def number_of_is_id ..
lemma nat_of_int_of_number_of_aux:
@@ -154,15 +154,15 @@
code_datatype nat_of_int
-code_const "0::nat"
- (SML "!(0 : IntInf.int)")
- (OCaml "Big'_int.big'_int'_of'_int/ 0")
- (Haskell "0")
+lemma [code func]: "0 = nat_of_int 0"
+ by (auto simp add: nat_of_int_def)
+lemma [code func]: "Suc n = nat_of_int (int n + 1)"
+ by (auto simp add: nat_of_int_def)
-code_const "Suc"
- (SML "IntInf.+ ((_), 1)")
- (OCaml "Big_int.succ'_big'_int")
- (Haskell "!((_) + 1)")
+code_type nat
+ (SML "IntInf.int")
+ (OCaml "Big'_int.big'_int")
+ (Haskell "Integer")
types_code
nat ("int")
@@ -173,11 +173,6 @@
fun gen_nat i = random_range 0 i;
*}
-code_type nat
- (SML "IntInf.int")
- (OCaml "Big'_int.big'_int")
- (Haskell "Integer")
-
consts_code
"HOL.zero" :: nat ("0")
Suc ("(_ + 1)")
--- a/src/HOL/Library/Eval.thy Thu Apr 26 13:33:09 2007 +0200
+++ b/src/HOL/Library/Eval.thy Thu Apr 26 13:33:12 2007 +0200
@@ -109,28 +109,20 @@
in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
*}
-text {* Disable for @{typ char}acters and @{typ ml_string}s *}
+text {* Adaption for @{typ ml_string}s *}
-code_const "typ_of \<Colon> char itself \<Rightarrow> typ" and "term_of \<Colon> char \<Rightarrow> term"
- (SML "!((_); raise Fail \"typ'_of'_char\")"
- and "!((_); raise Fail \"term'_of'_char\")")
- (OCaml "!((_); failwith \"typ'_of'_char\")"
- and "!((_); failwith \"term'_of'_char\")")
- (Haskell "error/ \"typ'_of'_char\""
- and "error/ \"term'_of'_char\"")
+lemmas [code func, code nofunc] = term_of_ml_string_def
-code_const "term_of \<Colon> ml_string \<Rightarrow> term"
- (SML "!((_); raise Fail \"term'_of'_ml'_string\")")
- (OCaml "!((_); failwith \"term'_of'_ml'_string\")")
subsection {* Evaluation infrastructure *}
ML {*
signature EVAL =
sig
+ val eval_ref: term option ref
val eval_term: theory -> term -> term
- val term: string -> unit
- val eval_ref: term option ref
+ val print: (theory -> term -> term) -> string
+ -> Toplevel.transition -> Toplevel.transition
end;
structure Eval : EVAL =
@@ -142,13 +134,29 @@
CodegenPackage.eval_term
thy (("Eval.eval_ref", eval_ref), TermOf.mk_term_of t);
-fun term t =
+fun print eval s = Toplevel.keep (fn state =>
let
- val thy = the_context ();
- val t = eval_term thy (Sign.read_term thy t);
- in (writeln o Sign.string_of_term thy) t end;
+ val ctxt = Toplevel.context_of state;
+ val thy = ProofContext.theory_of ctxt;
+ val t = eval thy (ProofContext.read_term ctxt s);
+ val T = Term.type_of t;
+ in
+ writeln (Pretty.string_of
+ (Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk,
+ Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)]))
+ end);
end;
*}
+ML {*
+val valueP =
+ OuterSyntax.improper_command "value" "read, evaluate and print term" OuterKeyword.diag
+ ((OuterParse.opt_keyword "overloaded" -- OuterParse.term)
+ >> (fn (b, t) => (Toplevel.no_timing o Eval.print
+ (if b then Eval.eval_term else Codegen.eval_term) t)));
+
+val _ = OuterSyntax.add_parsers [valueP];
+*}
+
end
--- a/src/HOL/Library/Pure_term.thy Thu Apr 26 13:33:09 2007 +0200
+++ b/src/HOL/Library/Pure_term.thy Thu Apr 26 13:33:12 2007 +0200
@@ -90,15 +90,10 @@
"(op \<mapsto>) (v, ty) = Absp v ty"
by rule (auto simp add: Absp_def)
-definition
- "term_case' f g h k l = term_case f g h (\<lambda>(v, ty). k v ty) (\<lambda>n. l (int n))"
-
-lemma term_case' [code inline, code func]:
- "term_case = (\<lambda>f g h k l. term_case' f g h (\<lambda>v ty. k (v, ty)) (\<lambda>v. l (nat v)))"
- unfolding term_case'_def by auto
-
code_datatype Const App Fix Absp Bound
lemmas [code func] = Bnd_Bound Abs_Absp
+lemmas [code nofunc] = term.recs term.cases term.size
+lemma [code func, code nofunc]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" ..
code_type "typ" and "term"
(SML "Term.typ" and "Term.term")
@@ -109,23 +104,8 @@
code_const Const and App and Fix
and Absp and Bound
(SML "Term.Const/ (_, _)" and "Term.$/ (_, _)" and "Term.Free/ (_, _)"
- and "Term.Abs/ (_, _, _)" and "Term.Bound/ (IntInf.toInt/ _)")
-
-code_const term_rec and term_case and "size \<Colon> term \<Rightarrow> nat"
- and "op = \<Colon> term \<Rightarrow> term \<Rightarrow> bool"
- (SML "!(_; _; _; _; _; raise Fail \"term'_rec\")"
- and "!(_; _; _; _; _; raise Fail \"term'_case\")"
- and "!(_; raise Fail \"size'_term\")"
- and "!(_; _; raise Fail \"eq'_term\")")
- (OCaml "!(_; _; _; _; _; failwith \"term'_rec\")"
- and "!(_; _; _; _; _; failwith \"term'_case\")"
- and "!(_; failwith \"size'_term\")"
- and "!(_; _; failwith \"eq'_term\")")
- (Haskell "error/ \"term'_rec\""
- and "error/ \"term'_case\""
- and "error/ \"size'_term\""
- and "error/ \"eq'_term\"")
-
+ and "Term.Abs/ (_, _, _)" and "!((_); Term.Bound/ (raise Fail \"Bound\"))")
+
code_reserved SML Term
end
--- a/src/HOL/Tools/Presburger/cooper_dec.ML Thu Apr 26 13:33:09 2007 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML Thu Apr 26 13:33:12 2007 +0200
@@ -512,16 +512,13 @@
(*list_disj[conj] makes a disj[conj] of a given list. used with conjucts or disjuncts
it liearises iterated conj[disj]unctions. *)
-fun disj_help p q = HOLogic.disj $ p $ q ;
-
-fun list_disj l =
- if l = [] then HOLogic.false_const else Utils.end_itlist disj_help l;
-
-fun conj_help p q = HOLogic.conj $ p $ q ;
-
-fun list_conj l =
- if l = [] then HOLogic.true_const else Utils.end_itlist conj_help l;
-
+fun list_disj [] = HOLogic.false_const
+ | list_disj ps = foldr1 (fn (p, q) => HOLogic.disj $ p $ q) ps;
+
+fun list_conj [] = HOLogic.true_const
+ | list_conj ps = foldr1 (fn (p, q) => HOLogic.conj $ p $ q) ps;
+
+
(*Simplification of Formulas *)
(*Function q_bnd_chk checks if a quantified Formula makes sens : Means if in
--- a/src/HOL/ex/Eval_examples.thy Thu Apr 26 13:33:09 2007 +0200
+++ b/src/HOL/ex/Eval_examples.thy Thu Apr 26 13:33:12 2007 +0200
@@ -15,10 +15,11 @@
text {* term evaluation *}
-ML {* Eval.term "(Suc 2 + 1) * 4" *}
-ML {* Eval.term "(Suc 2 + Suc 0) * Suc 3" *}
-ML {* Eval.term "[]::nat list" *}
-ML {* Eval.term "fst ([]::nat list, Suc 0) = []" *}
+value (overloaded) "(Suc 2 + 1) * 4"
+value (overloaded) "(Suc 2 + 1) * 4"
+value (overloaded) "(Suc 2 + Suc 0) * Suc 3"
+value (overloaded) "[]::nat list"
+value (overloaded) "fst ([]::nat list, Suc 0) = []"
text {* a fancy datatype *}
@@ -29,6 +30,6 @@
and ('a, 'b) cair =
Cair 'a 'b
-ML {* Eval.term "Shift (Cair (4::nat) [Suc 0])" *}
+value (overloaded) "Shift (Cair (4::nat) [Suc 0])"
end
\ No newline at end of file
--- a/src/Pure/Tools/codegen_func.ML Thu Apr 26 13:33:09 2007 +0200
+++ b/src/Pure/Tools/codegen_func.ML Thu Apr 26 13:33:12 2007 +0200
@@ -81,8 +81,10 @@
fun assert_func thm =
let
val thy = Thm.theory_of_thm thm;
- val args = (snd o strip_comb o fst o Logic.dest_equals
+ val (head, args) = (strip_comb o fst o Logic.dest_equals
o ObjectLogic.drop_judgment thy o Thm.plain_prop_of) thm;
+ val _ = case head of Const _ => () | _ =>
+ bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm);
val _ =
if has_duplicates (op =)
((fold o fold_aterms) (fn Var (v, _) => cons v