# HG changeset patch # User haftmann # Date 1177587192 -7200 # Node ID d3c23b90c6c64f15ef2b74b2d059f60fa75257e4 # Parent 5129e02f4df2c70ae269e99738f82bc6d7992aa2 tuned diff -r 5129e02f4df2 -r d3c23b90c6c6 src/HOL/Integ/cooper_dec.ML --- 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 diff -r 5129e02f4df2 -r d3c23b90c6c6 src/HOL/Library/EfficientNat.thy --- 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 \ 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)") diff -r 5129e02f4df2 -r d3c23b90c6c6 src/HOL/Library/Eval.thy --- 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 \ char itself \ typ" and "term_of \ char \ 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 \ ml_string \ 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 diff -r 5129e02f4df2 -r d3c23b90c6c6 src/HOL/Library/Pure_term.thy --- 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 \) (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 (\(v, ty). k v ty) (\n. l (int n))" - -lemma term_case' [code inline, code func]: - "term_case = (\f g h k l. term_case' f g h (\v ty. k (v, ty)) (\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\term) = t2 \ 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 \ term \ nat" - and "op = \ term \ term \ 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 diff -r 5129e02f4df2 -r d3c23b90c6c6 src/HOL/Tools/Presburger/cooper_dec.ML --- 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 diff -r 5129e02f4df2 -r d3c23b90c6c6 src/HOL/ex/Eval_examples.thy --- 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 diff -r 5129e02f4df2 -r d3c23b90c6c6 src/Pure/Tools/codegen_func.ML --- 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