# HG changeset patch # User haftmann # Date 1242306701 -7200 # Node ID 6e1e8e19456241db0e81b51aba0d0b03bf146c57 # Parent 25a3a0dd4bdac7f4bfaf25bd47a48e3ecf884479# Parent 90fed3d4430fff5262070f18f8697720c3aa4642 merged diff -r 25a3a0dd4bda -r 6e1e8e194562 doc-src/Codegen/Thy/ML.thy --- a/doc-src/Codegen/Thy/ML.thy Thu May 14 11:00:42 2009 +0200 +++ b/doc-src/Codegen/Thy/ML.thy Thu May 14 15:11:41 2009 +0200 @@ -78,16 +78,16 @@ text %mlref {* \begin{mldecls} - @{index_ML Code_Unit.read_const: "theory -> string -> string"} \\ - @{index_ML Code_Unit.rewrite_eqn: "simpset -> thm -> thm"} \\ + @{index_ML Code.read_const: "theory -> string -> string"} \\ + @{index_ML Code.rewrite_eqn: "simpset -> thm -> thm"} \\ \end{mldecls} \begin{description} - \item @{ML Code_Unit.read_const}~@{text thy}~@{text s} + \item @{ML Code.read_const}~@{text thy}~@{text s} reads a constant as a concrete term expression @{text s}. - \item @{ML Code_Unit.rewrite_eqn}~@{text ss}~@{text thm} + \item @{ML Code.rewrite_eqn}~@{text ss}~@{text thm} rewrites a code equation @{text thm} with a simpset @{text ss}; only arguments and right hand side are rewritten, not the head of the code equation. diff -r 25a3a0dd4bda -r 6e1e8e194562 doc-src/Codegen/Thy/document/Adaptation.tex --- a/doc-src/Codegen/Thy/document/Adaptation.tex Thu May 14 11:00:42 2009 +0200 +++ b/doc-src/Codegen/Thy/document/Adaptation.tex Thu May 14 15:11:41 2009 +0200 @@ -166,7 +166,7 @@ \isa{index} which is mapped to target-language built-in integers. Useful for code setups which involve e.g. indexing of target-language arrays. - \item[\hyperlink{theory.Code-Message}{\mbox{\isa{Code{\isacharunderscore}Message}}}] provides an additional datatype + \item[\hyperlink{theory.String}{\mbox{\isa{String}}}] provides an additional datatype \isa{message{\isacharunderscore}string} which is isomorphic to strings; \isa{message{\isacharunderscore}string}s are mapped to target-language strings. Useful for code setups which involve e.g. printing (error) messages. diff -r 25a3a0dd4bda -r 6e1e8e194562 doc-src/Codegen/Thy/document/Codegen.tex --- a/doc-src/Codegen/Thy/document/Codegen.tex Thu May 14 11:00:42 2009 +0200 +++ b/doc-src/Codegen/Thy/document/Codegen.tex Thu May 14 15:11:41 2009 +0200 @@ -1550,20 +1550,20 @@ % \begin{isamarkuptext}% \begin{mldecls} - \indexml{Code\_Unit.read\_const}\verb|Code_Unit.read_const: theory -> string -> string| \\ - \indexml{Code\_Unit.head\_func}\verb|Code_Unit.head_func: thm -> string * ((string * sort) list * typ)| \\ - \indexml{Code\_Unit.rewrite\_func}\verb|Code_Unit.rewrite_func: MetaSimplifier.simpset -> thm -> thm| \\ + \indexml{Code\_Unit.read\_const}\verb|Code.read_const: theory -> string -> string| \\ + \indexml{Code\_Unit.head\_func}\verb|Code.head_func: thm -> string * ((string * sort) list * typ)| \\ + \indexml{Code\_Unit.rewrite\_func}\verb|Code.rewrite_func: MetaSimplifier.simpset -> thm -> thm| \\ \end{mldecls} \begin{description} - \item \verb|Code_Unit.read_const|~\isa{thy}~\isa{s} + \item \verb|Code.read_const|~\isa{thy}~\isa{s} reads a constant as a concrete term expression \isa{s}. - \item \verb|Code_Unit.head_func|~\isa{thm} + \item \verb|Code.head_func|~\isa{thm} extracts the constant and its type from a defining equation \isa{thm}. - \item \verb|Code_Unit.rewrite_func|~\isa{ss}~\isa{thm} + \item \verb|Code.rewrite_func|~\isa{ss}~\isa{thm} rewrites a defining equation \isa{thm} with a simpset \isa{ss}; only arguments and right hand side are rewritten, not the head of the defining equation. diff -r 25a3a0dd4bda -r 6e1e8e194562 doc-src/Codegen/Thy/document/ML.tex --- a/doc-src/Codegen/Thy/document/ML.tex Thu May 14 11:00:42 2009 +0200 +++ b/doc-src/Codegen/Thy/document/ML.tex Thu May 14 15:11:41 2009 +0200 @@ -55,11 +55,11 @@ \indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\ \indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\ \indexdef{}{ML}{Code.add\_eqnl}\verb|Code.add_eqnl: string * (thm * bool) list lazy -> theory -> theory| \\ - \indexdef{}{ML}{Code.map\_pre}\verb|Code.map_pre: (simpset -> simpset) -> theory -> theory| \\ - \indexdef{}{ML}{Code.map\_post}\verb|Code.map_post: (simpset -> simpset) -> theory -> theory| \\ - \indexdef{}{ML}{Code.add\_functrans}\verb|Code.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline% + \indexdef{}{ML}{Code\_Preproc.map\_pre}\verb|Code_Preproc.map_pre: (simpset -> simpset) -> theory -> theory| \\ + \indexdef{}{ML}{Code\_Preproc.map\_post}\verb|Code_Preproc.map_post: (simpset -> simpset) -> theory -> theory| \\ + \indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline% \verb| -> theory -> theory| \\ - \indexdef{}{ML}{Code.del\_functrans}\verb|Code.del_functrans: string -> theory -> theory| \\ + \indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\ \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\ \indexdef{}{ML}{Code.get\_datatype}\verb|Code.get_datatype: theory -> string|\isasep\isanewline% \verb| -> (string * sort) list * (string * typ list) list| \\ @@ -78,10 +78,10 @@ suspended code equations \isa{lthms} for constant \isa{const} to executable content. - \item \verb|Code.map_pre|~\isa{f}~\isa{thy} changes + \item \verb|Code_Preproc.map_pre|~\isa{f}~\isa{thy} changes the preprocessor simpset. - \item \verb|Code.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds + \item \verb|Code_Preproc.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds function transformer \isa{f} (named \isa{name}) to executable content; \isa{f} is a transformer of the code equations belonging to a certain function definition, depending on the @@ -89,7 +89,7 @@ transformation took place; otherwise, the whole process will be iterated with the new code equations. - \item \verb|Code.del_functrans|~\isa{name}~\isa{thy} removes + \item \verb|Code_Preproc.del_functrans|~\isa{name}~\isa{thy} removes function transformer named \isa{name} from executable content. \item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds @@ -124,20 +124,16 @@ % \begin{isamarkuptext}% \begin{mldecls} - \indexdef{}{ML}{Code\_Unit.read\_const}\verb|Code_Unit.read_const: theory -> string -> string| \\ - \indexdef{}{ML}{Code\_Unit.head\_eqn}\verb|Code_Unit.head_eqn: theory -> thm -> string * ((string * sort) list * typ)| \\ - \indexdef{}{ML}{Code\_Unit.rewrite\_eqn}\verb|Code_Unit.rewrite_eqn: simpset -> thm -> thm| \\ + \indexdef{}{ML}{Code\_Unit.read\_const}\verb|Code.read_const: theory -> string -> string| \\ + \indexdef{}{ML}{Code\_Unit.rewrite\_eqn}\verb|Code.rewrite_eqn: simpset -> thm -> thm| \\ \end{mldecls} \begin{description} - \item \verb|Code_Unit.read_const|~\isa{thy}~\isa{s} + \item \verb|Code.read_const|~\isa{thy}~\isa{s} reads a constant as a concrete term expression \isa{s}. - \item \verb|Code_Unit.head_eqn|~\isa{thy}~\isa{thm} - extracts the constant and its type from a code equation \isa{thm}. - - \item \verb|Code_Unit.rewrite_eqn|~\isa{ss}~\isa{thm} + \item \verb|Code.rewrite_eqn|~\isa{ss}~\isa{thm} rewrites a code equation \isa{thm} with a simpset \isa{ss}; only arguments and right hand side are rewritten, not the head of the code equation. diff -r 25a3a0dd4bda -r 6e1e8e194562 doc-src/Codegen/Thy/document/Program.tex --- a/doc-src/Codegen/Thy/document/Program.tex Thu May 14 11:00:42 2009 +0200 +++ b/doc-src/Codegen/Thy/document/Program.tex Thu May 14 15:11:41 2009 +0200 @@ -891,8 +891,8 @@ \hspace*{0pt}fun null [] = true\\ \hspace*{0pt} ~| null (x ::~xs) = false;\\ \hspace*{0pt}\\ -\hspace*{0pt}fun eq{\char95}nat (Suc a) Zero{\char95}nat = false\\ -\hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat (Suc a) = false\\ +\hspace*{0pt}fun eq{\char95}nat (Suc nat') Zero{\char95}nat = false\\ +\hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat (Suc nat') = false\\ \hspace*{0pt} ~| eq{\char95}nat (Suc nat) (Suc nat') = eq{\char95}nat nat nat'\\ \hspace*{0pt} ~| eq{\char95}nat Zero{\char95}nat Zero{\char95}nat = true;\\ \hspace*{0pt}\\ diff -r 25a3a0dd4bda -r 6e1e8e194562 doc-src/more_antiquote.ML --- a/doc-src/more_antiquote.ML Thu May 14 11:00:42 2009 +0200 +++ b/doc-src/more_antiquote.ML Thu May 14 15:11:41 2009 +0200 @@ -87,7 +87,7 @@ fun pretty_code_thm src ctxt raw_const = let val thy = ProofContext.theory_of ctxt; - val const = Code_Unit.check_const thy raw_const; + val const = Code.check_const thy raw_const; val (_, funcgr) = Code_Preproc.obtain thy [const] []; fun holize thm = @{thm meta_eq_to_obj_eq} OF [thm]; val thms = Code_Preproc.eqns funcgr const @@ -108,7 +108,7 @@ local val parse_const_terms = Scan.repeat1 Args.term - >> (fn ts => fn thy => map (Code_Unit.check_const thy) ts); + >> (fn ts => fn thy => map (Code.check_const thy) ts); val parse_consts = Scan.lift (Args.parens (Args.$$$ "consts")) |-- parse_const_terms >> (fn mk_cs => fn thy => fn naming => map_filter (Code_Thingol.lookup_const naming) (mk_cs thy)); val parse_types = Scan.lift (Args.parens (Args.$$$ "types") |-- Scan.repeat1 Args.name) diff -r 25a3a0dd4bda -r 6e1e8e194562 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu May 14 11:00:42 2009 +0200 +++ b/src/HOL/HOL.thy Thu May 14 15:11:41 2009 +0200 @@ -1331,7 +1331,7 @@ of Abs (_, _, t') => count_loose t' 0 <= 1 | _ => true; in fn _ => fn ss => fn ct => if is_trivial_let (Thm.term_of ct) - then SOME @{thm Let_def} (*no or one ocurrenc of bound variable*) + then SOME @{thm Let_def} (*no or one ocurrence of bound variable*) else let (*Norbert Schirmer's case*) val ctxt = Simplifier.the_context ss; val thy = ProofContext.theory_of ctxt; @@ -1775,6 +1775,13 @@ end *} +subsubsection {* Generic code generator preprocessor setup *} + +setup {* + Code_Preproc.map_pre (K HOL_basic_ss) + #> Code_Preproc.map_post (K HOL_basic_ss) +*} + subsubsection {* Equality *} class eq = @@ -1788,7 +1795,7 @@ lemma eq_refl: "eq x x \ True" unfolding eq by rule+ -lemma equals_eq [code inline]: "(op =) \ eq" +lemma equals_eq: "(op =) \ eq" by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals) declare equals_eq [symmetric, code post] @@ -1797,6 +1804,14 @@ declare equals_eq [code] +setup {* + Code_Preproc.map_pre (fn simpset => + simpset addsimprocs [Simplifier.simproc_i @{theory} "eq" [@{term "op ="}] + (fn thy => fn _ => fn t as Const (_, T) => case strip_type T + of ((T as Type _) :: _, _) => SOME @{thm equals_eq} + | _ => NONE)]) +*} + subsubsection {* Generic code generator foundation *} @@ -1851,18 +1866,17 @@ "eq_class.eq TYPE('a) TYPE('a) \ True" by (simp add: eq) - text {* Equality *} declare simp_thms(6) [code nbe] +setup {* + Code.add_const_alias @{thm equals_eq} +*} + hide (open) const eq hide const eq -setup {* - Code_Unit.add_const_alias @{thm equals_eq} -*} - text {* Cases *} lemma Let_case_cert: @@ -1883,13 +1897,6 @@ code_abort undefined -subsubsection {* Generic code generator preprocessor *} - -setup {* - Code_Preproc.map_pre (K HOL_basic_ss) - #> Code_Preproc.map_post (K HOL_basic_ss) -*} - subsubsection {* Generic code generator target languages *} text {* type bool *} diff -r 25a3a0dd4bda -r 6e1e8e194562 src/HOL/Library/Quickcheck.thy --- a/src/HOL/Library/Quickcheck.thy Thu May 14 11:00:42 2009 +0200 +++ b/src/HOL/Library/Quickcheck.thy Thu May 14 15:11:41 2009 +0200 @@ -75,7 +75,7 @@ val tys = (map snd o fst o strip_abs) t; val t' = mk_generator_expr thy t tys; val f = Code_ML.eval (SOME target) ("Quickcheck.eval_ref", eval_ref) - (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' []; + (fn proc => fn g => fn s => g (s + 1) #>> (Option.map o map) proc) thy t' []; in f #> Random_Engine.run end; end diff -r 25a3a0dd4bda -r 6e1e8e194562 src/HOL/List.thy --- a/src/HOL/List.thy Thu May 14 11:00:42 2009 +0200 +++ b/src/HOL/List.thy Thu May 14 15:11:41 2009 +0200 @@ -3646,10 +3646,14 @@ lemmas in_set_code [code unfold] = mem_iff [symmetric] -lemma empty_null [code inline]: +lemma empty_null: "xs = [] \ null xs" by (cases xs) simp_all +lemma [code inline]: + "eq_class.eq xs [] \ null xs" +by (simp add: eq empty_null) + lemmas null_empty [code post] = empty_null [symmetric] diff -r 25a3a0dd4bda -r 6e1e8e194562 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Thu May 14 11:00:42 2009 +0200 +++ b/src/HOL/Nat.thy Thu May 14 15:11:41 2009 +0200 @@ -1199,7 +1199,7 @@ definition funpow :: "nat \ ('a \ 'a) \ 'a \ 'a" where funpow_code_def [code post]: "funpow = compow" -lemmas [code inline] = funpow_code_def [symmetric] +lemmas [code unfold] = funpow_code_def [symmetric] lemma [code]: "funpow 0 f = id" diff -r 25a3a0dd4bda -r 6e1e8e194562 src/HOL/Option.thy --- a/src/HOL/Option.thy Thu May 14 11:00:42 2009 +0200 +++ b/src/HOL/Option.thy Thu May 14 15:11:41 2009 +0200 @@ -63,10 +63,8 @@ lemma set_empty_eq [simp]: "(set xo = {}) = (xo = None)" by (cases xo) auto -definition - map :: "('a \ 'b) \ 'a option \ 'b option" -where - [code del]: "map = (%f y. case y of None => None | Some x => Some (f x))" +definition map :: "('a \ 'b) \ 'a option \ 'b option" where + "map = (%f y. case y of None => None | Some x => Some (f x))" lemma option_map_None [simp, code]: "map f None = None" by (simp add: map_def) @@ -95,14 +93,21 @@ subsubsection {* Code generator setup *} -definition - is_none :: "'a option \ bool" where - is_none_none [code post, symmetric, code inline]: "is_none x \ x = None" +definition is_none :: "'a option \ bool" where + [code post]: "is_none x \ x = None" lemma is_none_code [code]: shows "is_none None \ True" and "is_none (Some x) \ False" - unfolding is_none_none [symmetric] by simp_all + unfolding is_none_def by simp_all + +lemma is_none_none: + "is_none x \ x = None" + by (simp add: is_none_def) + +lemma [code inline]: + "eq_class.eq x None \ is_none x" + by (simp add: eq is_none_none) hide (open) const is_none diff -r 25a3a0dd4bda -r 6e1e8e194562 src/HOL/Power.thy --- a/src/HOL/Power.thy Thu May 14 11:00:42 2009 +0200 +++ b/src/HOL/Power.thy Thu May 14 15:11:41 2009 +0200 @@ -452,4 +452,13 @@ from power_strict_increasing_iff [OF this] less show ?thesis .. qed + +subsection {* Code generator tweak *} + +lemma power_power_power [code, code unfold, code inline del]: + "power = power.power (1::'a::{power}) (op *)" + unfolding power_def power.power_def .. + +declare power.power.simps [code] + end diff -r 25a3a0dd4bda -r 6e1e8e194562 src/HOL/Tools/datatype_codegen.ML --- a/src/HOL/Tools/datatype_codegen.ML Thu May 14 11:00:42 2009 +0200 +++ b/src/HOL/Tools/datatype_codegen.ML Thu May 14 15:11:41 2009 +0200 @@ -368,8 +368,7 @@ addsimps (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms)) addsimprocs [DatatypePackage.distinct_simproc]); fun prove prop = Goal.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset))) - |> Simpdata.mk_eq - |> Simplifier.rewrite_rule [@{thm equals_eq}]; + |> Simpdata.mk_eq; in map (rpair true o prove) (triv_injects @ injects @ distincts) @ [(prove refl, false)] end; fun add_equality vs dtcos thy = @@ -414,7 +413,7 @@ let val cs = map (fn (c, tys) => (c, tys ---> Type (dtco, map TFree vs))) cos; val cs' = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) cs; - in if is_some (try (Code_Unit.constrset_of_consts thy) cs') + in if is_some (try (Code.constrset_of_consts thy) cs') then SOME cs else NONE end; diff -r 25a3a0dd4bda -r 6e1e8e194562 src/HOL/Tools/recfun_codegen.ML --- a/src/HOL/Tools/recfun_codegen.ML Thu May 14 11:00:42 2009 +0200 +++ b/src/HOL/Tools/recfun_codegen.ML Thu May 14 15:11:41 2009 +0200 @@ -26,10 +26,10 @@ fun add_thm NONE thm thy = Code.add_eqn thm thy | add_thm (SOME module_name) thm thy = let - val (thm', _) = Code_Unit.mk_eqn thy (K false) (thm, true) + val (thm', _) = Code.mk_eqn thy (K false) (thm, true) in thy - |> ModuleData.map (Symtab.update (Code_Unit.const_eqn thy thm', module_name)) + |> ModuleData.map (Symtab.update (Code.const_eqn thy thm', module_name)) |> Code.add_eqn thm' end; @@ -44,10 +44,10 @@ fun expand_eta thy [] = [] | expand_eta thy (thms as thm :: _) = let - val (_, ty) = Code_Unit.const_typ_eqn thm; + val (_, ty) = Code.const_typ_eqn thm; in if null (Term.add_tvarsT ty []) orelse (null o fst o strip_type) ty then thms - else map (Code_Unit.expand_eta thy 1) thms + else map (Code.expand_eta thy 1) thms end; fun retrieve_equations thy (c, T) = if c = @{const_name "op ="} then NONE else @@ -58,7 +58,7 @@ |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE) |> expand_eta thy |> map_filter (meta_eq_to_obj_eq thy) - |> Code_Unit.norm_varnames thy + |> Code.norm_varnames thy |> map (rpair opt_name) in if null thms then NONE else SOME thms end; diff -r 25a3a0dd4bda -r 6e1e8e194562 src/HOL/ex/predicate_compile.ML --- a/src/HOL/ex/predicate_compile.ML Thu May 14 11:00:42 2009 +0200 +++ b/src/HOL/ex/predicate_compile.ML Thu May 14 15:11:41 2009 +0200 @@ -1405,7 +1405,7 @@ in val code_pred = generic_code_pred (K I); -val code_pred_cmd = generic_code_pred Code_Unit.read_const +val code_pred_cmd = generic_code_pred Code.read_const val setup = Attrib.setup @{binding code_ind_intros} (Scan.succeed (attrib add_intro_thm)) diff -r 25a3a0dd4bda -r 6e1e8e194562 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Thu May 14 11:00:42 2009 +0200 +++ b/src/Pure/IsaMakefile Thu May 14 15:11:41 2009 +0200 @@ -56,7 +56,7 @@ General/table.ML General/url.ML General/xml.ML General/yxml.ML \ Isar/ROOT.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \ Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML \ - Isar/code_unit.ML Isar/constdefs.ML Isar/context_rules.ML \ + Isar/constdefs.ML Isar/context_rules.ML \ Isar/element.ML Isar/expression.ML Isar/isar_cmd.ML \ Isar/isar_document.ML Isar/isar_syn.ML Isar/local_defs.ML \ Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML \ diff -r 25a3a0dd4bda -r 6e1e8e194562 src/Pure/Isar/ROOT.ML --- a/src/Pure/Isar/ROOT.ML Thu May 14 11:00:42 2009 +0200 +++ b/src/Pure/Isar/ROOT.ML Thu May 14 15:11:41 2009 +0200 @@ -61,7 +61,6 @@ use "../simplifier.ML"; (*executable theory content*) -use "code_unit.ML"; use "code.ML"; (*specifications*) diff -r 25a3a0dd4bda -r 6e1e8e194562 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Thu May 14 11:00:42 2009 +0200 +++ b/src/Pure/Isar/code.ML Thu May 14 15:11:41 2009 +0200 @@ -7,6 +7,55 @@ signature CODE = sig + (*constructor sets*) + val constrset_of_consts: theory -> (string * typ) list + -> string * ((string * sort) list * (string * typ list) list) + + (*typ instantiations*) + val typscheme: theory -> string * typ -> (string * sort) list * typ + val inst_thm: theory -> sort Vartab.table -> thm -> thm + + (*constants*) + val string_of_typ: theory -> typ -> string + val string_of_const: theory -> string -> string + val no_args: theory -> string -> int + val check_const: theory -> term -> string + val read_bare_const: theory -> string -> string * typ + val read_const: theory -> string -> string + + (*constant aliasses*) + val add_const_alias: thm -> theory -> theory + val triv_classes: theory -> class list + val resubst_alias: theory -> string -> string + + (*code equations*) + val mk_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool + val mk_eqn_liberal: theory -> (string -> bool) -> thm -> (thm * bool) option + val assert_eqn: theory -> thm * bool -> thm * bool + val assert_eqns_const: theory -> string + -> (thm * bool) list -> (thm * bool) list + val const_typ_eqn: thm -> string * typ + val const_eqn: theory -> thm -> string + val typscheme_eqn: theory -> thm -> (string * sort) list * typ + val expand_eta: theory -> int -> thm -> thm + val rewrite_eqn: simpset -> thm -> thm + val rewrite_head: thm list -> thm -> thm + val norm_args: theory -> thm list -> thm list + val norm_varnames: theory -> thm list -> thm list + + (*case certificates*) + val case_cert: thm -> string * (int * string list) + + (*infrastructure*) + val add_attribute: string * attribute parser -> theory -> theory + val purge_data: theory -> theory + + (*executable content*) + val add_datatype: (string * typ) list -> theory -> theory + val add_datatype_cmd: string list -> theory -> theory + val type_interpretation: + (string * ((string * sort) list * (string * typ list) list) + -> theory -> theory) -> theory -> theory val add_eqn: thm -> theory -> theory val add_nbe_eqn: thm -> theory -> theory val add_default_eqn: thm -> theory -> theory @@ -15,27 +64,16 @@ val del_eqn: thm -> theory -> theory val del_eqns: string -> theory -> theory val add_eqnl: string * (thm * bool) list lazy -> theory -> theory - val add_datatype: (string * typ) list -> theory -> theory - val add_datatype_cmd: string list -> theory -> theory - val type_interpretation: - (string * ((string * sort) list * (string * typ list) list) - -> theory -> theory) -> theory -> theory val add_case: thm -> theory -> theory val add_undefined: string -> theory -> theory - val purge_data: theory -> theory - val these_eqns: theory -> string -> (thm * bool) list + (*data retrieval*) val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list) val get_datatype_of_constr: theory -> string -> string option + val default_typscheme: theory -> string -> (string * sort) list * typ + val these_eqns: theory -> string -> (thm * bool) list val get_case_scheme: theory -> string -> (int * (int * string list)) option val is_undefined: theory -> string -> bool - val default_typscheme: theory -> string -> (string * sort) list * typ - val assert_eqn: theory -> thm * bool -> thm * bool - val assert_eqns_const: theory -> string - -> (thm * bool) list -> (thm * bool) list - - val add_attribute: string * attribute parser -> theory -> theory - val print_codesetup: theory -> unit end; @@ -70,6 +108,400 @@ structure Code : PRIVATE_CODE = struct +(* auxiliary *) + +fun string_of_typ thy = setmp show_sorts true (Syntax.string_of_typ_global thy); +fun string_of_const thy c = case AxClass.inst_of_param thy c + of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco) + | NONE => Sign.extern_const thy c; + +fun no_args thy = length o fst o strip_type o Sign.the_const_type thy; + + +(* utilities *) + +fun typscheme thy (c, ty) = + let + val ty' = Logic.unvarifyT ty; + fun dest (TFree (v, sort)) = (v, sort) + | dest ty = error ("Illegal type parameter in type scheme: " ^ Syntax.string_of_typ_global thy ty); + val vs = map dest (Sign.const_typargs thy (c, ty')); + in (vs, Type.strip_sorts ty') end; + +fun inst_thm thy tvars' thm = + let + val tvars = (Term.add_tvars o Thm.prop_of) thm []; + val inter_sort = Sorts.inter_sort (Sign.classes_of thy); + fun mk_inst (tvar as (v, sort)) = case Vartab.lookup tvars' v + of SOME sort' => SOME (pairself (Thm.ctyp_of thy o TVar) + (tvar, (v, inter_sort (sort, sort')))) + | NONE => NONE; + val insts = map_filter mk_inst tvars; + in Thm.instantiate (insts, []) thm end; + +fun expand_eta thy k thm = + let + val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm; + val (head, args) = strip_comb lhs; + val l = if k = ~1 + then (length o fst o strip_abs) rhs + else Int.max (0, k - length args); + val used = Name.make_context (map (fst o fst) (Term.add_vars lhs [])); + fun get_name _ 0 = pair [] + | get_name (Abs (v, ty, t)) k = + Name.variants [v] + ##>> get_name t (k - 1) + #>> (fn ([v'], vs') => (v', ty) :: vs') + | get_name t k = + let + val (tys, _) = (strip_type o fastype_of) t + in case tys + of [] => raise TERM ("expand_eta", [t]) + | ty :: _ => + Name.variants [""] + #-> (fn [v] => get_name (t $ Var ((v, 0), ty)) (k - 1) + #>> (fn vs' => (v, ty) :: vs')) + end; + val (vs, _) = get_name rhs l used; + fun expand (v, ty) thm = Drule.fun_cong_rule thm + (Thm.cterm_of thy (Var ((v, 0), ty))); + in + thm + |> fold expand vs + |> Conv.fconv_rule Drule.beta_eta_conversion + end; + +fun eqn_conv conv = + let + fun lhs_conv ct = if can Thm.dest_comb ct + then (Conv.combination_conv lhs_conv conv) ct + else Conv.all_conv ct; + in Conv.combination_conv (Conv.arg_conv lhs_conv) conv end; + +fun head_conv conv = + let + fun lhs_conv ct = if can Thm.dest_comb ct + then (Conv.fun_conv lhs_conv) ct + else conv ct; + in Conv.fun_conv (Conv.arg_conv lhs_conv) end; + +val rewrite_eqn = Conv.fconv_rule o eqn_conv o Simplifier.rewrite; +val rewrite_head = Conv.fconv_rule o head_conv o MetaSimplifier.rewrite false; + +fun norm_args thy thms = + let + val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals; + val k = fold (curry Int.max o num_args_of o Thm.prop_of) thms 0; + in + thms + |> map (expand_eta thy k) + |> map (Conv.fconv_rule Drule.beta_eta_conversion) + end; + +fun canonical_tvars thy thm = + let + val ctyp = Thm.ctyp_of thy; + val purify_tvar = unprefix "'" #> Name.desymbolize false #> prefix "'"; + fun tvars_subst_for thm = (fold_types o fold_atyps) + (fn TVar (v_i as (v, _), sort) => let + val v' = purify_tvar v + in if v = v' then I + else insert (op =) (v_i, (v', sort)) end + | _ => I) (prop_of thm) []; + fun mk_inst (v_i, (v', sort)) (maxidx, acc) = + let + val ty = TVar (v_i, sort) + in + (maxidx + 1, (ctyp ty, ctyp (TVar ((v', maxidx), sort))) :: acc) + end; + val maxidx = Thm.maxidx_of thm + 1; + val (_, inst) = fold mk_inst (tvars_subst_for thm) (maxidx + 1, []); + in Thm.instantiate (inst, []) thm end; + +fun canonical_vars thy thm = + let + val cterm = Thm.cterm_of thy; + val purify_var = Name.desymbolize false; + fun vars_subst_for thm = fold_aterms + (fn Var (v_i as (v, _), ty) => let + val v' = purify_var v + in if v = v' then I + else insert (op =) (v_i, (v', ty)) end + | _ => I) (prop_of thm) []; + fun mk_inst (v_i as (v, i), (v', ty)) (maxidx, acc) = + let + val t = Var (v_i, ty) + in + (maxidx + 1, (cterm t, cterm (Var ((v', maxidx), ty))) :: acc) + end; + val maxidx = Thm.maxidx_of thm + 1; + val (_, inst) = fold mk_inst (vars_subst_for thm) (maxidx + 1, []); + in Thm.instantiate ([], inst) thm end; + +fun canonical_absvars thm = + let + val t = Thm.plain_prop_of thm; + val purify_var = Name.desymbolize false; + val t' = Term.map_abs_vars purify_var t; + in Thm.rename_boundvars t t' thm end; + +fun norm_varnames thy thms = + let + fun burrow_thms f [] = [] + | burrow_thms f thms = + thms + |> Conjunction.intr_balanced + |> f + |> Conjunction.elim_balanced (length thms) + in + thms + |> map (canonical_vars thy) + |> map canonical_absvars + |> map Drule.zero_var_indexes + |> burrow_thms (canonical_tvars thy) + |> Drule.zero_var_indexes_list + end; + + +(* const aliasses *) + +structure ConstAlias = TheoryDataFun +( + type T = ((string * string) * thm) list * class list; + val empty = ([], []); + val copy = I; + val extend = I; + fun merge _ ((alias1, classes1), (alias2, classes2)) : T = + (Library.merge (eq_snd Thm.eq_thm_prop) (alias1, alias2), + Library.merge (op =) (classes1, classes2)); +); + +fun add_const_alias thm thy = + let + val lhs_rhs = case try Logic.dest_equals (Thm.prop_of thm) + of SOME lhs_rhs => lhs_rhs + | _ => error ("Not an equation: " ^ Display.string_of_thm thm); + val c_c' = case try (pairself (AxClass.unoverload_const thy o dest_Const)) lhs_rhs + of SOME c_c' => c_c' + | _ => error ("Not an equation with two constants: " ^ Display.string_of_thm thm); + val some_class = the_list (AxClass.class_of_param thy (snd c_c')); + in thy |> + ConstAlias.map (fn (alias, classes) => + ((c_c', thm) :: alias, fold (insert (op =)) some_class classes)) + end; + +fun resubst_alias thy = + let + val alias = fst (ConstAlias.get thy); + val subst_inst_param = Option.map fst o AxClass.inst_of_param thy; + fun subst_alias c = + get_first (fn ((c', c''), _) => if c = c'' then SOME c' else NONE) alias; + in + perhaps subst_inst_param + #> perhaps subst_alias + end; + +val triv_classes = snd o ConstAlias.get; + + +(* reading constants as terms *) + +fun check_bare_const thy t = case try dest_Const t + of SOME c_ty => c_ty + | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t); + +fun check_const thy = AxClass.unoverload_const thy o check_bare_const thy; + +fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy; + +fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy; + + +(* constructor sets *) + +fun constrset_of_consts thy cs = + let + val _ = map (fn (c, _) => if (is_some o AxClass.class_of_param thy) c + then error ("Is a class parameter: " ^ string_of_const thy c) else ()) cs; + fun no_constr (c, ty) = error ("Not a datatype constructor: " ^ string_of_const thy c + ^ " :: " ^ string_of_typ thy ty); + fun last_typ c_ty ty = + let + val frees = OldTerm.typ_tfrees ty; + val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) ty + handle TYPE _ => no_constr c_ty + val _ = if has_duplicates (eq_fst (op =)) vs then no_constr c_ty else (); + val _ = if length frees <> length vs then no_constr c_ty else (); + in (tyco, vs) end; + fun ty_sorts (c, ty) = + let + val ty_decl = (Logic.unvarifyT o Sign.the_const_type thy) c; + val (tyco, _) = last_typ (c, ty) ty_decl; + val (_, vs) = last_typ (c, ty) ty; + in ((tyco, map snd vs), (c, (map fst vs, ty))) end; + fun add ((tyco', sorts'), c) ((tyco, sorts), cs) = + let + val _ = if tyco' <> tyco + then error "Different type constructors in constructor set" + else (); + val sorts'' = map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts + in ((tyco, sorts), c :: cs) end; + fun inst vs' (c, (vs, ty)) = + let + val the_v = the o AList.lookup (op =) (vs ~~ vs'); + val ty' = map_atyps (fn TFree (v, _) => TFree (the_v v)) ty; + in (c, (fst o strip_type) ty') end; + val c' :: cs' = map ty_sorts cs; + val ((tyco, sorts), cs'') = fold add cs' (apsnd single c'); + val vs = Name.names Name.context Name.aT sorts; + val cs''' = map (inst vs) cs''; + in (tyco, (vs, rev cs''')) end; + + +(* code equations *) + +exception BAD_THM of string; +fun bad_thm msg = raise BAD_THM msg; +fun error_thm f thm = f thm handle BAD_THM msg => error msg; +fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE; + +fun is_linear thm = + let val (_, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm + in not (has_duplicates (op =) ((fold o fold_aterms) + (fn Var (v, _) => cons v | _ => I) args [])) end; + +fun gen_assert_eqn thy is_constr_head is_constr_pat (thm, proper) = + let + val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm + handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm) + | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm); + fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v + | Free _ => bad_thm ("Illegal free variable in equation\n" + ^ Display.string_of_thm thm) + | _ => I) t []; + fun tvars_of t = fold_term_types (fn _ => + fold_atyps (fn TVar (v, _) => insert (op =) v + | TFree _ => bad_thm + ("Illegal free type variable in equation\n" ^ Display.string_of_thm thm))) t []; + val lhs_vs = vars_of lhs; + val rhs_vs = vars_of rhs; + val lhs_tvs = tvars_of lhs; + val rhs_tvs = tvars_of rhs; + val _ = if null (subtract (op =) lhs_vs rhs_vs) + then () + else bad_thm ("Free variables on right hand side of equation\n" + ^ Display.string_of_thm thm); + val _ = if null (subtract (op =) lhs_tvs rhs_tvs) + then () + else bad_thm ("Free type variables on right hand side of equation\n" + ^ Display.string_of_thm thm) val (head, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm; + val (c, ty) = case head + of Const (c_ty as (_, ty)) => (AxClass.unoverload_const thy c_ty, ty) + | _ => bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm); + fun check _ (Abs _) = bad_thm + ("Abstraction on left hand side of equation\n" + ^ Display.string_of_thm thm) + | check 0 (Var _) = () + | check _ (Var _) = bad_thm + ("Variable with application on left hand side of equation\n" + ^ Display.string_of_thm thm) + | check n (t1 $ t2) = (check (n+1) t1; check 0 t2) + | check n (Const (c_ty as (c, ty))) = if n = (length o fst o strip_type) ty + then if not proper orelse is_constr_pat (AxClass.unoverload_const thy c_ty) + then () + else bad_thm (quote c ^ " is not a constructor, on left hand side of equation\n" + ^ Display.string_of_thm thm) + else bad_thm + ("Partially applied constant " ^ quote c ^ " on left hand side of equation\n" + ^ Display.string_of_thm thm); + val _ = map (check 0) args; + val _ = if not proper orelse is_linear thm then () + else bad_thm ("Duplicate variables on left hand side of equation\n" + ^ Display.string_of_thm thm); + val _ = if (is_none o AxClass.class_of_param thy) c + then () + else bad_thm ("Polymorphic constant as head in equation\n" + ^ Display.string_of_thm thm) + val _ = if not (is_constr_head c) + then () + else bad_thm ("Constructor as head in equation\n" + ^ Display.string_of_thm thm) + val ty_decl = Sign.the_const_type thy c; + val _ = if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty) + then () else bad_thm ("Type\n" ^ string_of_typ thy ty + ^ "\nof equation\n" + ^ Display.string_of_thm thm + ^ "\nis incompatible with declared function type\n" + ^ string_of_typ thy ty_decl) + in (thm, proper) end; + +fun assert_eqn thy is_constr = error_thm (gen_assert_eqn thy is_constr is_constr); + +val const_typ_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of; + + +(*those following are permissive wrt. to overloaded constants!*) + +fun mk_eqn thy is_constr_head = error_thm (gen_assert_eqn thy is_constr_head (K true)) o + apfst (LocalDefs.meta_rewrite_rule (ProofContext.init thy)); + +fun mk_eqn_liberal thy is_constr_head = Option.map (fn (thm, _) => (thm, is_linear thm)) + o try_thm (gen_assert_eqn thy is_constr_head (K true)) + o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy); + +fun const_typ_eqn_unoverload thy thm = + let + val (c, ty) = const_typ_eqn thm; + val c' = AxClass.unoverload_const thy (c, ty); + in (c', ty) end; + +fun typscheme_eqn thy = typscheme thy o const_typ_eqn_unoverload thy; +fun const_eqn thy = fst o const_typ_eqn_unoverload thy; + + +(* case cerificates *) + +fun case_certificate thm = + let + val ((head, raw_case_expr), cases) = (apfst Logic.dest_equals + o apsnd Logic.dest_conjunctions o Logic.dest_implies o Thm.prop_of) thm; + val _ = case head of Free _ => true + | Var _ => true + | _ => raise TERM ("case_cert", []); + val ([(case_var, _)], case_expr) = Term.strip_abs_eta 1 raw_case_expr; + val (Const (case_const, _), raw_params) = strip_comb case_expr; + val n = find_index (fn Free (v, _) => v = case_var | _ => false) raw_params; + val _ = if n = ~1 then raise TERM ("case_cert", []) else (); + val params = map (fst o dest_Var) (nth_drop n raw_params); + fun dest_case t = + let + val (head' $ t_co, rhs) = Logic.dest_equals t; + val _ = if head' = head then () else raise TERM ("case_cert", []); + val (Const (co, _), args) = strip_comb t_co; + val (Var (param, _), args') = strip_comb rhs; + val _ = if args' = args then () else raise TERM ("case_cert", []); + in (param, co) end; + fun analyze_cases cases = + let + val co_list = fold (AList.update (op =) o dest_case) cases []; + in map (the o AList.lookup (op =) co_list) params end; + fun analyze_let t = + let + val (head' $ arg, Var (param', _) $ arg') = Logic.dest_equals t; + val _ = if head' = head then () else raise TERM ("case_cert", []); + val _ = if arg' = arg then () else raise TERM ("case_cert", []); + val _ = if [param'] = params then () else raise TERM ("case_cert", []); + in [] end; + fun analyze (cases as [let_case]) = + (analyze_cases cases handle Bind => analyze_let let_case) + | analyze cases = analyze_cases cases; + in (case_const, (n, analyze cases)) end; + +fun case_cert thm = case_certificate thm + handle Bind => error "bad case certificate" + | TERM _ => error "bad case certificate"; + + (** code attributes **) structure CodeAttr = TheoryDataFun ( @@ -116,7 +548,8 @@ fun add_drop_redundant thy (thm, proper) thms = let - val args_of = snd o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of; + val args_of = snd o strip_comb o map_types Type.strip_sorts + o fst o Logic.dest_equals o Thm.plain_prop_of; val args = args_of thm; val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1); fun matches_args args' = length args <= length args' andalso @@ -332,16 +765,16 @@ (Pretty.block o Pretty.breaks) ( Pretty.str s :: Pretty.str "=" - :: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str (Code_Unit.string_of_const thy c) + :: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str (string_of_const thy c) | (c, tys) => (Pretty.block o Pretty.breaks) - (Pretty.str (Code_Unit.string_of_const thy c) + (Pretty.str (string_of_const thy c) :: Pretty.str "of" :: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos) ); val eqns = the_eqns exec |> Symtab.dest - |> (map o apfst) (Code_Unit.string_of_const thy) + |> (map o apfst) (string_of_const thy) |> (map o apsnd) (snd o fst) |> sort (string_ord o pairself fst); val dtyps = the_dtyps exec @@ -377,13 +810,13 @@ val max' = Thm.maxidx_of thm' + 1; in (thm', max') end; val (thms', maxidx) = fold_map incr_thm thms 0; - val ty1 :: tys = map (snd o Code_Unit.const_typ_eqn) thms'; + val ty1 :: tys = map (snd o const_typ_eqn) thms'; fun unify ty env = Sign.typ_unify thy (ty1, ty) env handle Type.TUNIFY => error ("Type unificaton failed, while unifying code equations\n" ^ (cat_lines o map Display.string_of_thm) thms ^ "\nwith types\n" - ^ (cat_lines o map (Code_Unit.string_of_typ thy)) (ty1 :: tys)); + ^ (cat_lines o map (string_of_typ thy)) (ty1 :: tys)); val (env, _) = fold unify tys (Vartab.empty, maxidx) val instT = Vartab.fold (fn (x_i, (sort, ty)) => cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env []; @@ -408,13 +841,13 @@ fun is_constr thy = is_some o get_datatype_of_constr thy; -fun assert_eqn thy = Code_Unit.assert_eqn thy (is_constr thy); +val assert_eqn = fn thy => assert_eqn thy (is_constr thy); fun assert_eqns_const thy c eqns = let - fun cert (eqn as (thm, _)) = if c = Code_Unit.const_eqn thy thm + fun cert (eqn as (thm, _)) = if c = const_eqn thy thm then eqn else error ("Wrong head of code equation,\nexpected constant " - ^ Code_Unit.string_of_const thy c ^ "\n" ^ Display.string_of_thm thm) + ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm thm) in map (cert o assert_eqn thy) eqns end; fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns @@ -422,19 +855,19 @@ o apfst) (fn (_, eqns) => (true, f eqns)); fun gen_add_eqn default (eqn as (thm, _)) thy = - let val c = Code_Unit.const_eqn thy thm + let val c = const_eqn thy thm in change_eqns false c (add_thm thy default eqn) thy end; fun add_eqn thm thy = - gen_add_eqn false (Code_Unit.mk_eqn thy (is_constr thy) (thm, true)) thy; + gen_add_eqn false (mk_eqn thy (is_constr thy) (thm, true)) thy; fun add_default_eqn thm thy = - case Code_Unit.mk_eqn_liberal thy (is_constr thy) thm + case mk_eqn_liberal thy (is_constr thy) thm of SOME eqn => gen_add_eqn true eqn thy | NONE => thy; fun add_nbe_eqn thm thy = - gen_add_eqn false (Code_Unit.mk_eqn thy (is_constr thy) (thm, false)) thy; + gen_add_eqn false (mk_eqn thy (is_constr thy) (thm, false)) thy; fun add_eqnl (c, lthms) thy = let @@ -445,8 +878,8 @@ (fn thm => Context.mapping (add_default_eqn thm) I); val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute); -fun del_eqn thm thy = case Code_Unit.mk_eqn_liberal thy (is_constr thy) thm - of SOME (thm, _) => change_eqns true (Code_Unit.const_eqn thy thm) (del_thm thm) thy +fun del_eqn thm thy = case mk_eqn_liberal thy (is_constr thy) thm + of SOME (thm, _) => change_eqns true (const_eqn thy thm) (del_thm thm) thy | NONE => thy; fun del_eqns c = change_eqns true c (K (false, Lazy.value [])); @@ -460,7 +893,7 @@ fun add_datatype raw_cs thy = let val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs; - val (tyco, vs_cos) = Code_Unit.constrset_of_consts thy cs; + val (tyco, vs_cos) = constrset_of_consts thy cs; val old_cs = (map fst o snd o get_datatype thy) tyco; fun drop_outdated_cases cases = fold Symtab.delete_safe (Symtab.fold (fn (c, (_, (_, cos))) => @@ -480,12 +913,12 @@ fun add_datatype_cmd raw_cs thy = let - val cs = map (Code_Unit.read_bare_const thy) raw_cs; + val cs = map (read_bare_const thy) raw_cs; in add_datatype cs thy end; fun add_case thm thy = let - val (c, (k, case_pats)) = Code_Unit.case_cert thm; + val (c, (k, case_pats)) = case_cert thm; val _ = case filter_out (is_constr thy) case_pats of [] => () | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs)); @@ -516,7 +949,7 @@ fun default_typscheme thy c = let - fun the_const_typscheme c = (curry (Code_Unit.typscheme thy) c o snd o dest_Const + fun the_const_typscheme c = (curry (typscheme thy) c o snd o dest_Const o TermSubst.zero_var_indexes o curry Const "" o Sign.the_const_type thy) c; fun strip_sorts (vs, ty) = (map (fn (v, _) => (v, [])) vs, ty); in case AxClass.class_of_param thy c @@ -524,7 +957,7 @@ | NONE => if is_constr thy c then strip_sorts (the_const_typscheme c) else case get_eqns thy c - of (thm, _) :: _ => (Code_Unit.typscheme_eqn thy o Drule.zero_var_indexes) thm + of (thm, _) :: _ => (typscheme_eqn thy o Drule.zero_var_indexes) thm | [] => strip_sorts (the_const_typscheme c) end; end; (*struct*) diff -r 25a3a0dd4bda -r 6e1e8e194562 src/Pure/Isar/code_unit.ML --- a/src/Pure/Isar/code_unit.ML Thu May 14 11:00:42 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,444 +0,0 @@ -(* Title: Pure/Isar/code_unit.ML - Author: Florian Haftmann, TU Muenchen - -Basic notions of code generation. Auxiliary. -*) - -signature CODE_UNIT = -sig - (*typ instantiations*) - val typscheme: theory -> string * typ -> (string * sort) list * typ - val inst_thm: theory -> sort Vartab.table -> thm -> thm - - (*constant aliasses*) - val add_const_alias: thm -> theory -> theory - val triv_classes: theory -> class list - val resubst_alias: theory -> string -> string - - (*constants*) - val string_of_typ: theory -> typ -> string - val string_of_const: theory -> string -> string - val no_args: theory -> string -> int - val check_const: theory -> term -> string - val read_bare_const: theory -> string -> string * typ - val read_const: theory -> string -> string - - (*constructor sets*) - val constrset_of_consts: theory -> (string * typ) list - -> string * ((string * sort) list * (string * typ list) list) - - (*code equations*) - val mk_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool - val mk_eqn_liberal: theory -> (string -> bool) -> thm -> (thm * bool) option - val assert_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool - val const_typ_eqn: thm -> string * typ - val const_eqn: theory -> thm -> string - val typscheme_eqn: theory -> thm -> (string * sort) list * typ - val expand_eta: theory -> int -> thm -> thm - val rewrite_eqn: simpset -> thm -> thm - val rewrite_head: thm list -> thm -> thm - val norm_args: theory -> thm list -> thm list - val norm_varnames: theory -> thm list -> thm list - - (*case certificates*) - val case_cert: thm -> string * (int * string list) -end; - -structure Code_Unit: CODE_UNIT = -struct - - -(* auxiliary *) - -fun string_of_typ thy = setmp show_sorts true (Syntax.string_of_typ_global thy); -fun string_of_const thy c = case AxClass.inst_of_param thy c - of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco) - | NONE => Sign.extern_const thy c; - -fun no_args thy = length o fst o strip_type o Sign.the_const_type thy; - - -(* utilities *) - -fun typscheme thy (c, ty) = - let - val ty' = Logic.unvarifyT ty; - fun dest (TFree (v, sort)) = (v, sort) - | dest ty = error ("Illegal type parameter in type scheme: " ^ Syntax.string_of_typ_global thy ty); - val vs = map dest (Sign.const_typargs thy (c, ty')); - in (vs, Type.strip_sorts ty') end; - -fun inst_thm thy tvars' thm = - let - val tvars = (Term.add_tvars o Thm.prop_of) thm []; - val inter_sort = Sorts.inter_sort (Sign.classes_of thy); - fun mk_inst (tvar as (v, sort)) = case Vartab.lookup tvars' v - of SOME sort' => SOME (pairself (Thm.ctyp_of thy o TVar) - (tvar, (v, inter_sort (sort, sort')))) - | NONE => NONE; - val insts = map_filter mk_inst tvars; - in Thm.instantiate (insts, []) thm end; - -fun expand_eta thy k thm = - let - val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm; - val (head, args) = strip_comb lhs; - val l = if k = ~1 - then (length o fst o strip_abs) rhs - else Int.max (0, k - length args); - val used = Name.make_context (map (fst o fst) (Term.add_vars lhs [])); - fun get_name _ 0 = pair [] - | get_name (Abs (v, ty, t)) k = - Name.variants [v] - ##>> get_name t (k - 1) - #>> (fn ([v'], vs') => (v', ty) :: vs') - | get_name t k = - let - val (tys, _) = (strip_type o fastype_of) t - in case tys - of [] => raise TERM ("expand_eta", [t]) - | ty :: _ => - Name.variants [""] - #-> (fn [v] => get_name (t $ Var ((v, 0), ty)) (k - 1) - #>> (fn vs' => (v, ty) :: vs')) - end; - val (vs, _) = get_name rhs l used; - fun expand (v, ty) thm = Drule.fun_cong_rule thm - (Thm.cterm_of thy (Var ((v, 0), ty))); - in - thm - |> fold expand vs - |> Conv.fconv_rule Drule.beta_eta_conversion - end; - -fun eqn_conv conv = - let - fun lhs_conv ct = if can Thm.dest_comb ct - then (Conv.combination_conv lhs_conv conv) ct - else Conv.all_conv ct; - in Conv.combination_conv (Conv.arg_conv lhs_conv) conv end; - -fun head_conv conv = - let - fun lhs_conv ct = if can Thm.dest_comb ct - then (Conv.fun_conv lhs_conv) ct - else conv ct; - in Conv.fun_conv (Conv.arg_conv lhs_conv) end; - -val rewrite_eqn = Conv.fconv_rule o eqn_conv o Simplifier.rewrite; -val rewrite_head = Conv.fconv_rule o head_conv o MetaSimplifier.rewrite false; - -fun norm_args thy thms = - let - val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals; - val k = fold (curry Int.max o num_args_of o Thm.prop_of) thms 0; - in - thms - |> map (expand_eta thy k) - |> map (Conv.fconv_rule Drule.beta_eta_conversion) - end; - -fun canonical_tvars thy thm = - let - val ctyp = Thm.ctyp_of thy; - val purify_tvar = unprefix "'" #> Name.desymbolize false #> prefix "'"; - fun tvars_subst_for thm = (fold_types o fold_atyps) - (fn TVar (v_i as (v, _), sort) => let - val v' = purify_tvar v - in if v = v' then I - else insert (op =) (v_i, (v', sort)) end - | _ => I) (prop_of thm) []; - fun mk_inst (v_i, (v', sort)) (maxidx, acc) = - let - val ty = TVar (v_i, sort) - in - (maxidx + 1, (ctyp ty, ctyp (TVar ((v', maxidx), sort))) :: acc) - end; - val maxidx = Thm.maxidx_of thm + 1; - val (_, inst) = fold mk_inst (tvars_subst_for thm) (maxidx + 1, []); - in Thm.instantiate (inst, []) thm end; - -fun canonical_vars thy thm = - let - val cterm = Thm.cterm_of thy; - val purify_var = Name.desymbolize false; - fun vars_subst_for thm = fold_aterms - (fn Var (v_i as (v, _), ty) => let - val v' = purify_var v - in if v = v' then I - else insert (op =) (v_i, (v', ty)) end - | _ => I) (prop_of thm) []; - fun mk_inst (v_i as (v, i), (v', ty)) (maxidx, acc) = - let - val t = Var (v_i, ty) - in - (maxidx + 1, (cterm t, cterm (Var ((v', maxidx), ty))) :: acc) - end; - val maxidx = Thm.maxidx_of thm + 1; - val (_, inst) = fold mk_inst (vars_subst_for thm) (maxidx + 1, []); - in Thm.instantiate ([], inst) thm end; - -fun canonical_absvars thm = - let - val t = Thm.plain_prop_of thm; - val purify_var = Name.desymbolize false; - val t' = Term.map_abs_vars purify_var t; - in Thm.rename_boundvars t t' thm end; - -fun norm_varnames thy thms = - let - fun burrow_thms f [] = [] - | burrow_thms f thms = - thms - |> Conjunction.intr_balanced - |> f - |> Conjunction.elim_balanced (length thms) - in - thms - |> map (canonical_vars thy) - |> map canonical_absvars - |> map Drule.zero_var_indexes - |> burrow_thms (canonical_tvars thy) - |> Drule.zero_var_indexes_list - end; - - -(* const aliasses *) - -structure ConstAlias = TheoryDataFun -( - type T = ((string * string) * thm) list * class list; - val empty = ([], []); - val copy = I; - val extend = I; - fun merge _ ((alias1, classes1), (alias2, classes2)) : T = - (Library.merge (eq_snd Thm.eq_thm_prop) (alias1, alias2), - Library.merge (op =) (classes1, classes2)); -); - -fun add_const_alias thm thy = - let - val lhs_rhs = case try Logic.dest_equals (Thm.prop_of thm) - of SOME lhs_rhs => lhs_rhs - | _ => error ("Not an equation: " ^ Display.string_of_thm thm); - val c_c' = case try (pairself (AxClass.unoverload_const thy o dest_Const)) lhs_rhs - of SOME c_c' => c_c' - | _ => error ("Not an equation with two constants: " ^ Display.string_of_thm thm); - val some_class = the_list (AxClass.class_of_param thy (snd c_c')); - in thy |> - ConstAlias.map (fn (alias, classes) => - ((c_c', thm) :: alias, fold (insert (op =)) some_class classes)) - end; - -fun resubst_alias thy = - let - val alias = fst (ConstAlias.get thy); - val subst_inst_param = Option.map fst o AxClass.inst_of_param thy; - fun subst_alias c = - get_first (fn ((c', c''), _) => if c = c'' then SOME c' else NONE) alias; - in - perhaps subst_inst_param - #> perhaps subst_alias - end; - -val triv_classes = snd o ConstAlias.get; - - -(* reading constants as terms *) - -fun check_bare_const thy t = case try dest_Const t - of SOME c_ty => c_ty - | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t); - -fun check_const thy = AxClass.unoverload_const thy o check_bare_const thy; - -fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy; - -fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy; - - -(* constructor sets *) - -fun constrset_of_consts thy cs = - let - val _ = map (fn (c, _) => if (is_some o AxClass.class_of_param thy) c - then error ("Is a class parameter: " ^ string_of_const thy c) else ()) cs; - fun no_constr (c, ty) = error ("Not a datatype constructor: " ^ string_of_const thy c - ^ " :: " ^ string_of_typ thy ty); - fun last_typ c_ty ty = - let - val frees = OldTerm.typ_tfrees ty; - val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) ty - handle TYPE _ => no_constr c_ty - val _ = if has_duplicates (eq_fst (op =)) vs then no_constr c_ty else (); - val _ = if length frees <> length vs then no_constr c_ty else (); - in (tyco, vs) end; - fun ty_sorts (c, ty) = - let - val ty_decl = (Logic.unvarifyT o Sign.the_const_type thy) c; - val (tyco, _) = last_typ (c, ty) ty_decl; - val (_, vs) = last_typ (c, ty) ty; - in ((tyco, map snd vs), (c, (map fst vs, ty))) end; - fun add ((tyco', sorts'), c) ((tyco, sorts), cs) = - let - val _ = if tyco' <> tyco - then error "Different type constructors in constructor set" - else (); - val sorts'' = map2 (curry (Sorts.inter_sort (Sign.classes_of thy))) sorts' sorts - in ((tyco, sorts), c :: cs) end; - fun inst vs' (c, (vs, ty)) = - let - val the_v = the o AList.lookup (op =) (vs ~~ vs'); - val ty' = map_atyps (fn TFree (v, _) => TFree (the_v v)) ty; - in (c, (fst o strip_type) ty') end; - val c' :: cs' = map ty_sorts cs; - val ((tyco, sorts), cs'') = fold add cs' (apsnd single c'); - val vs = Name.names Name.context Name.aT sorts; - val cs''' = map (inst vs) cs''; - in (tyco, (vs, rev cs''')) end; - - -(* code equations *) - -exception BAD_THM of string; -fun bad_thm msg = raise BAD_THM msg; -fun error_thm f thm = f thm handle BAD_THM msg => error msg; -fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE; - -fun is_linear thm = - let val (_, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm - in not (has_duplicates (op =) ((fold o fold_aterms) - (fn Var (v, _) => cons v | _ => I) args [])) end; - -fun gen_assert_eqn thy is_constr_head is_constr_pat (thm, proper) = - let - val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm - handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm) - | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm); - fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v - | Free _ => bad_thm ("Illegal free variable in equation\n" - ^ Display.string_of_thm thm) - | _ => I) t []; - fun tvars_of t = fold_term_types (fn _ => - fold_atyps (fn TVar (v, _) => insert (op =) v - | TFree _ => bad_thm - ("Illegal free type variable in equation\n" ^ Display.string_of_thm thm))) t []; - val lhs_vs = vars_of lhs; - val rhs_vs = vars_of rhs; - val lhs_tvs = tvars_of lhs; - val rhs_tvs = tvars_of rhs; - val _ = if null (subtract (op =) lhs_vs rhs_vs) - then () - else bad_thm ("Free variables on right hand side of equation\n" - ^ Display.string_of_thm thm); - val _ = if null (subtract (op =) lhs_tvs rhs_tvs) - then () - else bad_thm ("Free type variables on right hand side of equation\n" - ^ Display.string_of_thm thm) val (head, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm; - val (c, ty) = case head - of Const (c_ty as (_, ty)) => (AxClass.unoverload_const thy c_ty, ty) - | _ => bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm); - fun check _ (Abs _) = bad_thm - ("Abstraction on left hand side of equation\n" - ^ Display.string_of_thm thm) - | check 0 (Var _) = () - | check _ (Var _) = bad_thm - ("Variable with application on left hand side of equation\n" - ^ Display.string_of_thm thm) - | check n (t1 $ t2) = (check (n+1) t1; check 0 t2) - | check n (Const (c_ty as (c, ty))) = if n = (length o fst o strip_type) ty - then if not proper orelse is_constr_pat (AxClass.unoverload_const thy c_ty) - then () - else bad_thm (quote c ^ " is not a constructor, on left hand side of equation\n" - ^ Display.string_of_thm thm) - else bad_thm - ("Partially applied constant " ^ quote c ^ " on left hand side of equation\n" - ^ Display.string_of_thm thm); - val _ = map (check 0) args; - val _ = if not proper orelse is_linear thm then () - else bad_thm ("Duplicate variables on left hand side of equation\n" - ^ Display.string_of_thm thm); - val _ = if (is_none o AxClass.class_of_param thy) c - then () - else bad_thm ("Polymorphic constant as head in equation\n" - ^ Display.string_of_thm thm) - val _ = if not (is_constr_head c) - then () - else bad_thm ("Constructor as head in equation\n" - ^ Display.string_of_thm thm) - val ty_decl = Sign.the_const_type thy c; - val _ = if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty) - then () else bad_thm ("Type\n" ^ string_of_typ thy ty - ^ "\nof equation\n" - ^ Display.string_of_thm thm - ^ "\nis incompatible with declared function type\n" - ^ string_of_typ thy ty_decl) - in (thm, proper) end; - -fun assert_eqn thy is_constr = error_thm (gen_assert_eqn thy is_constr is_constr); - -val const_typ_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of; - - -(*those following are permissive wrt. to overloaded constants!*) - -fun mk_eqn thy is_constr_head = error_thm (gen_assert_eqn thy is_constr_head (K true)) o - apfst (LocalDefs.meta_rewrite_rule (ProofContext.init thy)); - -fun mk_eqn_liberal thy is_constr_head = Option.map (fn (thm, _) => (thm, is_linear thm)) - o try_thm (gen_assert_eqn thy is_constr_head (K true)) - o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy); - -fun const_typ_eqn_unoverload thy thm = - let - val (c, ty) = const_typ_eqn thm; - val c' = AxClass.unoverload_const thy (c, ty); - in (c', ty) end; - -fun typscheme_eqn thy = typscheme thy o const_typ_eqn_unoverload thy; -fun const_eqn thy = fst o const_typ_eqn_unoverload thy; - - -(* case cerificates *) - -fun case_certificate thm = - let - val ((head, raw_case_expr), cases) = (apfst Logic.dest_equals - o apsnd Logic.dest_conjunctions o Logic.dest_implies o Thm.prop_of) thm; - val _ = case head of Free _ => true - | Var _ => true - | _ => raise TERM ("case_cert", []); - val ([(case_var, _)], case_expr) = Term.strip_abs_eta 1 raw_case_expr; - val (Const (case_const, _), raw_params) = strip_comb case_expr; - val n = find_index (fn Free (v, _) => v = case_var | _ => false) raw_params; - val _ = if n = ~1 then raise TERM ("case_cert", []) else (); - val params = map (fst o dest_Var) (nth_drop n raw_params); - fun dest_case t = - let - val (head' $ t_co, rhs) = Logic.dest_equals t; - val _ = if head' = head then () else raise TERM ("case_cert", []); - val (Const (co, _), args) = strip_comb t_co; - val (Var (param, _), args') = strip_comb rhs; - val _ = if args' = args then () else raise TERM ("case_cert", []); - in (param, co) end; - fun analyze_cases cases = - let - val co_list = fold (AList.update (op =) o dest_case) cases []; - in map (the o AList.lookup (op =) co_list) params end; - fun analyze_let t = - let - val (head' $ arg, Var (param', _) $ arg') = Logic.dest_equals t; - val _ = if head' = head then () else raise TERM ("case_cert", []); - val _ = if arg' = arg then () else raise TERM ("case_cert", []); - val _ = if [param'] = params then () else raise TERM ("case_cert", []); - in [] end; - fun analyze (cases as [let_case]) = - (analyze_cases cases handle Bind => analyze_let let_case) - | analyze cases = analyze_cases cases; - in (case_const, (n, analyze cases)) end; - -fun case_cert thm = case_certificate thm - handle Bind => error "bad case certificate" - | TERM _ => error "bad case certificate"; - -end; diff -r 25a3a0dd4bda -r 6e1e8e194562 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Thu May 14 11:00:42 2009 +0200 +++ b/src/Pure/codegen.ML Thu May 14 15:11:41 2009 +0200 @@ -329,7 +329,7 @@ end; val assoc_const_i = gen_assoc_const (K I); -val assoc_const = gen_assoc_const Code_Unit.read_bare_const; +val assoc_const = gen_assoc_const Code.read_bare_const; (**** associate types with target language types ****) diff -r 25a3a0dd4bda -r 6e1e8e194562 src/Tools/code/code_haskell.ML --- a/src/Tools/code/code_haskell.ML Thu May 14 11:00:42 2009 +0200 +++ b/src/Tools/code/code_haskell.ML Thu May 14 15:11:41 2009 +0200 @@ -480,7 +480,7 @@ fun add_monad target' raw_c_bind thy = let - val c_bind = Code_Unit.read_const thy raw_c_bind; + val c_bind = Code.read_const thy raw_c_bind; in if target = target' then thy |> Code_Target.add_syntax_const target c_bind diff -r 25a3a0dd4bda -r 6e1e8e194562 src/Tools/code/code_ml.ML --- a/src/Tools/code/code_ml.ML Thu May 14 11:00:42 2009 +0200 +++ b/src/Tools/code/code_ml.ML Thu May 14 15:11:41 2009 +0200 @@ -996,7 +996,7 @@ val (ml_code, target_names) = eval_code_of NONE thy naming program (consts' @ tycos'); val (consts'', tycos'') = chop (length consts') target_names; val consts_map = map2 (fn const => fn NONE => - error ("Constant " ^ (quote o Code_Unit.string_of_const thy) const + error ("Constant " ^ (quote o Code.string_of_const thy) const ^ "\nhas a user-defined serialization") | SOME const'' => (const, const'')) consts consts'' val tycos_map = map2 (fn tyco => fn NONE => @@ -1050,7 +1050,7 @@ fun ml_code_antiq raw_const {struct_name, background} = let - val const = Code_Unit.check_const (ProofContext.theory_of background) raw_const; + val const = Code.check_const (ProofContext.theory_of background) raw_const; val is_first = is_first_occ background; val background' = register_const const background; in (print_code struct_name is_first (print_const const), background') end; @@ -1059,7 +1059,7 @@ let val thy = ProofContext.theory_of background; val tyco = Sign.intern_type thy raw_tyco; - val constrs = map (Code_Unit.check_const thy) raw_constrs; + val constrs = map (Code.check_const thy) raw_constrs; val constrs' = (map fst o snd o Code.get_datatype thy) tyco; val _ = if gen_eq_set (op =) (constrs, constrs') then () else error ("Type " ^ quote tyco ^ ": given constructors diverge from real constructors") diff -r 25a3a0dd4bda -r 6e1e8e194562 src/Tools/code/code_preproc.ML --- a/src/Tools/code/code_preproc.ML Thu May 14 11:00:42 2009 +0200 +++ b/src/Tools/code/code_preproc.ML Thu May 14 15:11:41 2009 +0200 @@ -117,11 +117,11 @@ in eqns |> apply_functrans thy c functrans - |> (map o apfst) (Code_Unit.rewrite_eqn pre) + |> (map o apfst) (Code.rewrite_eqn pre) |> (map o apfst) (AxClass.unoverload thy) |> map (Code.assert_eqn thy) - |> burrow_fst (Code_Unit.norm_args thy) - |> burrow_fst (Code_Unit.norm_varnames thy) + |> burrow_fst (Code.norm_args thy) + |> burrow_fst (Code.norm_varnames thy) end; fun preprocess_conv thy ct = @@ -186,7 +186,7 @@ fun pretty thy eqngr = AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr) - |> (map o apfst) (Code_Unit.string_of_const thy) + |> (map o apfst) (Code.string_of_const thy) |> sort (string_ord o pairself fst) |> map (fn (s, thms) => (Pretty.block o Pretty.fbreaks) ( @@ -216,7 +216,7 @@ fun tyscm_rhss_of thy c eqns = let val tyscm = case eqns of [] => Code.default_typscheme thy c - | ((thm, _) :: _) => Code_Unit.typscheme_eqn thy thm; + | ((thm, _) :: _) => Code.typscheme_eqn thy thm; val rhss = consts_of thy eqns; in (tyscm, rhss) end; @@ -394,7 +394,7 @@ val inst_tab = Vartab.empty |> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) lhs; val eqns = proto_eqns - |> (map o apfst) (Code_Unit.inst_thm thy inst_tab); + |> (map o apfst) (Code.inst_thm thy inst_tab); val (tyscm, rhss') = tyscm_rhss_of thy c eqns; val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr; in (map (pair c) rhss' @ rhss, eqngr') end; diff -r 25a3a0dd4bda -r 6e1e8e194562 src/Tools/code/code_target.ML --- a/src/Tools/code/code_target.ML Thu May 14 11:00:42 2009 +0200 +++ b/src/Tools/code/code_target.ML Thu May 14 15:11:41 2009 +0200 @@ -286,7 +286,7 @@ fun gen_add_syntax_const prep_const target raw_c raw_syn thy = let val c = prep_const thy raw_c; - fun check_args (syntax as (n, _)) = if n > Code_Unit.no_args thy c + fun check_args (syntax as (n, _)) = if n > Code.no_args thy c then error ("Too many arguments in syntax for constant " ^ quote c) else syntax; in case raw_syn @@ -319,8 +319,8 @@ | add (name, NONE) incls = Symtab.delete name incls; in map_includes target (add args) thy end; -val add_include = gen_add_include Code_Unit.check_const; -val add_include_cmd = gen_add_include Code_Unit.read_const; +val add_include = gen_add_include Code.check_const; +val add_include_cmd = gen_add_include Code.read_const; fun add_module_alias target (thyname, modlname) = let @@ -363,11 +363,11 @@ val allow_abort = gen_allow_abort (K I); val add_reserved = add_reserved; -val add_syntax_class_cmd = gen_add_syntax_class read_class Code_Unit.read_const; +val add_syntax_class_cmd = gen_add_syntax_class read_class Code.read_const; val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco; val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco; -val add_syntax_const_cmd = gen_add_syntax_const Code_Unit.read_const; -val allow_abort_cmd = gen_allow_abort Code_Unit.read_const; +val add_syntax_const_cmd = gen_add_syntax_const Code.read_const; +val allow_abort_cmd = gen_allow_abort Code.read_const; fun the_literals thy = let @@ -387,15 +387,15 @@ local fun labelled_name thy program name = case Graph.get_node program name - of Code_Thingol.Fun (c, _) => quote (Code_Unit.string_of_const thy c) + of Code_Thingol.Fun (c, _) => quote (Code.string_of_const thy c) | Code_Thingol.Datatype (tyco, _) => "type " ^ quote (Sign.extern_type thy tyco) - | Code_Thingol.Datatypecons (c, _) => quote (Code_Unit.string_of_const thy c) + | Code_Thingol.Datatypecons (c, _) => quote (Code.string_of_const thy c) | Code_Thingol.Class (class, _) => "class " ^ quote (Sign.extern_class thy class) | Code_Thingol.Classrel (sub, super) => let val Code_Thingol.Class (sub, _) = Graph.get_node program sub val Code_Thingol.Class (super, _) = Graph.get_node program super in quote (Sign.extern_class thy sub ^ " < " ^ Sign.extern_class thy super) end - | Code_Thingol.Classparam (c, _) => quote (Code_Unit.string_of_const thy c) + | Code_Thingol.Classparam (c, _) => quote (Code.string_of_const thy c) | Code_Thingol.Classinst ((class, (tyco, _)), _) => let val Code_Thingol.Class (class, _) = Graph.get_node program class val Code_Thingol.Datatype (tyco, _) = Graph.get_node program tyco diff -r 25a3a0dd4bda -r 6e1e8e194562 src/Tools/code/code_thingol.ML --- a/src/Tools/code/code_thingol.ML Thu May 14 11:00:42 2009 +0200 +++ b/src/Tools/code/code_thingol.ML Thu May 14 15:11:41 2009 +0200 @@ -498,7 +498,7 @@ let val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty then raw_thms - else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms; + else (map o apfst) (Code.expand_eta thy 1) raw_thms; in fold_map (translate_tyvar_sort thy algbr funcgr) vs ##>> translate_typ thy algbr funcgr ty @@ -634,7 +634,7 @@ Term.strip_abs_eta 1 (the_single ts_clause) in [(true, (Free v_ty, body))] end else map (uncurry mk_clause) - (AList.make (Code_Unit.no_args thy) case_pats ~~ ts_clause); + (AList.make (Code.no_args thy) case_pats ~~ ts_clause); fun retermify ty (_, (IVar x, body)) = (x, ty) `|-> body | retermify _ (_, (pat, body)) = @@ -812,7 +812,7 @@ fun read_const_expr "*" = ([], consts_of NONE) | read_const_expr s = if String.isSuffix ".*" s then ([], consts_of (SOME (unsuffix ".*" s))) - else ([Code_Unit.read_const thy s], []); + else ([Code.read_const thy s], []); in pairself flat o split_list o map read_const_expr end; fun code_depgr thy consts = @@ -839,7 +839,7 @@ |> map (the o Symtab.lookup mapping) |> distinct (op =); val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss; - fun namify consts = map (Code_Unit.string_of_const thy) consts + fun namify consts = map (Code.string_of_const thy) consts |> commas; val prgr = map (fn (consts, constss) => { name = namify consts, ID = namify consts, dir = "", unfold = true, diff -r 25a3a0dd4bda -r 6e1e8e194562 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Thu May 14 11:00:42 2009 +0200 +++ b/src/Tools/nbe.ML Thu May 14 15:11:41 2009 +0200 @@ -436,7 +436,7 @@ let fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty) | t => t); - val resubst_triv_consts = subst_const (Code_Unit.resubst_alias thy); + val resubst_triv_consts = subst_const (Code.resubst_alias thy); val ty' = typ_of_itype program vs0 ty; fun type_infer t = singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I @@ -459,7 +459,7 @@ (* evaluation oracle *) fun add_triv_classes thy = curry (Sorts.inter_sort (Sign.classes_of thy)) - (Code_Unit.triv_classes thy); + (Code.triv_classes thy); fun mk_equals thy lhs raw_rhs = let diff -r 25a3a0dd4bda -r 6e1e8e194562 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Thu May 14 11:00:42 2009 +0200 +++ b/src/Tools/quickcheck.ML Thu May 14 15:11:41 2009 +0200 @@ -104,12 +104,12 @@ of NONE => if quiet then mk_testers ctxt t' else mk_testers_strict ctxt t' | SOME name => [mk_tester_select name ctxt t']; fun iterate f 0 = NONE - | iterate f k = case f () handle Match => (if quiet then () + | iterate f j = case f () handle Match => (if quiet then () else warning "Exception Match raised during quickcheck"; NONE) - of NONE => iterate f (k - 1) | SOME q => SOME q; + of NONE => iterate f (j - 1) | SOME q => SOME q; fun with_testers k [] = NONE | with_testers k (tester :: testers) = - case iterate (fn () => tester k) i + case iterate (fn () => tester (k - 1)) i of NONE => with_testers k testers | SOME q => SOME q; fun with_size k = if k > size then NONE