--- a/src/HOL/Divides.thy Mon Nov 06 16:28:30 2006 +0100
+++ b/src/HOL/Divides.thy Mon Nov 06 16:28:31 2006 +0100
@@ -896,10 +896,8 @@
"m mod n = snd (divmod m n)"
unfolding divmod_def by simp
-code_constname
- "op div \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.div_nat"
- "op mod \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.mod_nat"
- Divides.divmod "IntDef.divmod_nat"
+code_modulename SML
+ Divides Integer
hide (open) const divmod
--- a/src/HOL/Integ/IntArith.thy Mon Nov 06 16:28:30 2006 +0100
+++ b/src/HOL/Integ/IntArith.thy Mon Nov 06 16:28:31 2006 +0100
@@ -364,20 +364,8 @@
subsection {* code generator setup *}
-code_typename
- "Numeral.bit" "IntDef.bit"
-
-code_constname
- "number_of \<Colon> int \<Rightarrow> int" "IntDef.number_of"
- "Numeral.pred" "IntDef.pred"
- "Numeral.succ" "IntDef.succ"
- "Numeral.Pls" "IntDef.pls"
- "Numeral.Min" "IntDef.min"
- "Numeral.Bit" "IntDef.bit"
- "Numeral.bit.bit_case" "IntDef.bit_case"
- "Code_Generator.eq \<Colon> bit \<Rightarrow> bit \<Rightarrow> bool" "IntDef.eq_bit"
- "Numeral.B0" "IntDef.b0"
- "Numeral.B1" "IntDef.b1"
+code_modulename SML
+ Numeral Integer
lemma Numeral_Pls_refl [code func]:
"Numeral.Pls = Numeral.Pls" ..
--- a/src/HOL/Integ/IntDef.thy Mon Nov 06 16:28:30 2006 +0100
+++ b/src/HOL/Integ/IntDef.thy Mon Nov 06 16:28:31 2006 +0100
@@ -946,6 +946,12 @@
code_reserved SML IntInf
code_reserved Haskell Integer negate
+code_modulename SML
+ IntDef Integer
+
+code_modulename Haskell
+ IntDef Integer
+
ML {*
fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of",
Type ("fun", [_, T as Type ("IntDef.int", [])])) $ bin) =
--- a/src/HOL/Library/EfficientNat.thy Mon Nov 06 16:28:30 2006 +0100
+++ b/src/HOL/Library/EfficientNat.thy Mon Nov 06 16:28:31 2006 +0100
@@ -32,9 +32,6 @@
"nat_of_int (int n) = n"
using zero_zle_int nat_of_int_def by simp
-code_constname
- nat_of_int "IntDef.nat_of_int"
-
text {*
Case analysis on natural numbers is rephrased using a conditional
expression:
@@ -332,4 +329,10 @@
*}
(*>*)
+subsection {* Module names *}
+
+code_modulename SML
+ Nat Integer
+ EfficientNat Integer
+
end
--- a/src/HOL/Library/ExecutableRat.thy Mon Nov 06 16:28:30 2006 +0100
+++ b/src/HOL/Library/ExecutableRat.thy Mon Nov 06 16:28:31 2006 +0100
@@ -93,31 +93,16 @@
section {* code names *}
-code_typename
- erat "Rational.erat"
-
-code_constname
- Rat "Rational.rat"
- erat_case "Rational.erat_case"
- norm "Rational.norm"
- common "Rational.common"
- of_quotient "Rational.of_quotient"
- of_rat "Rational.of_rat"
- to_rat "Rational.to_rat"
- eq_erat "Rational.eq_erat"
- div_zero "Rational.div_zero"
- "0\<Colon>erat" "Rational.erat_zero"
- "1\<Colon>erat" "Rational.erat_one"
- "op + \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat" "Rational.erat_plus"
- "uminus \<Colon> erat \<Rightarrow> erat" "Rational.erat_uminus"
- "op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat" "Rational.erat_times"
- "inverse \<Colon> erat \<Rightarrow> erat" "Rational.erat_inverse"
- "op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool" "Rational.erat_le"
- "Code_Generator.eq \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool" "Rational.erat_eq"
+code_modulename SML
+ ExecutableRat Rational
section {* rat as abstype *}
+lemma [code func]: -- {* prevents eq constraint *}
+ shows "All = All"
+ and "contents = contents" by rule+
+
code_abstype rat erat where
Fract \<equiv> of_quotient
"0 \<Colon> rat" \<equiv> "0 \<Colon> erat"
@@ -127,7 +112,7 @@
"op * \<Colon> rat \<Rightarrow> rat \<Rightarrow> rat" \<equiv> "op * \<Colon> erat \<Rightarrow> erat \<Rightarrow> erat"
"inverse \<Colon> rat \<Rightarrow> rat" \<equiv> "inverse \<Colon> erat \<Rightarrow> erat"
"op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> "op \<le> \<Colon> erat \<Rightarrow> erat \<Rightarrow> bool"
- "Code_Generator.eq \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> eq_erat
+ "Code_Generator.eq \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool" \<equiv> eq_erat
code_const div_zero
(SML "raise/ (Fail/ \"Division by zero\")")
--- a/src/HOL/Library/ExecutableSet.thy Mon Nov 06 16:28:30 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy Mon Nov 06 16:28:31 2006 +0100
@@ -235,10 +235,8 @@
nonfix union;
*}
-code_constname
- "ExecutableSet.member" "List.member"
- "ExecutableSet.insertl" "List.insertl"
- "ExecutableSet.drop_first" "List.drop_first"
+code_modulename SML
+ ExecutableSet List
definition [code inline]:
"empty_list = []"
@@ -285,7 +283,7 @@
Bex \<equiv> Blex
code_gen "{}" insert "op \<union>" "op \<inter>" "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
- image Union Inter UNION INTER Ball Bex (SML *)
+ image Union Inter UNION INTER Ball Bex (SML -)
subsection {* type serializations *}
--- a/src/HOL/Nat.thy Mon Nov 06 16:28:30 2006 +0100
+++ b/src/HOL/Nat.thy Mon Nov 06 16:28:31 2006 +0100
@@ -1121,29 +1121,4 @@
lemma [code func]:
"Code_Generator.eq 0 (Suc m) = False" unfolding eq_def by auto
-code_typename
- nat "IntDef.nat"
-
-code_instname
- nat :: eq "IntDef.eq_nat"
- nat :: zero "IntDef.zero_nat"
- nat :: one "IntDef.one_nat"
- nat :: ord "IntDef.ord_nat"
- nat :: plus "IntDef.plus_nat"
- nat :: minus "IntDef.minus_nat"
- nat :: times "IntDef.times_nat"
-
-code_constname
- "0 \<Colon> nat" "IntDef.zero_nat"
- "1 \<Colon> nat" "IntDef.one_nat"
- Suc "IntDef.succ_nat"
- "op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.plus_nat"
- "op - \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.minus_nat"
- "op * \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" "IntDef.times_nat"
- "op < \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" "IntDef.less_nat"
- "op \<le> \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" "IntDef.less_eq_nat"
- "Code_Generator.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool" "IntDef.eq_nat"
- nat_rec "IntDef.nat_rec"
- nat_case "IntDef.nat_case"
-
end
--- a/src/HOL/ex/Codegenerator.thy Mon Nov 06 16:28:30 2006 +0100
+++ b/src/HOL/ex/Codegenerator.thy Mon Nov 06 16:28:31 2006 +0100
@@ -102,21 +102,6 @@
definition
"base_case f = f list_case"
-subsection {* heavy usage of names *}
-
-definition
- f :: nat
- "f = 2"
- g :: nat
- "g = f"
- h :: nat
- "h = g"
-
-code_constname
- f "MymodA.f"
- g "MymodB.f"
- h "MymodC.f"
-
definition
"apply_tower = (\<lambda>x. x (\<lambda>x. x (\<lambda>x. x)))"
@@ -167,8 +152,6 @@
code_gen
mystring
code_gen
- f g h
-code_gen
apply_tower Codegenerator.keywords shadow base_case
code_gen
abs_let nested_let case_let
--- a/src/Pure/Tools/codegen_names.ML Mon Nov 06 16:28:30 2006 +0100
+++ b/src/Pure/Tools/codegen_names.ML Mon Nov 06 16:28:31 2006 +0100
@@ -15,13 +15,10 @@
val class_rev: theory -> class -> class option
val tyco: theory -> tyco -> tyco
val tyco_rev: theory -> tyco -> tyco option
- val tyco_force: tyco * string -> theory -> theory
val instance: theory -> class * tyco -> string
val instance_rev: theory -> string -> (class * tyco) option
- val instance_force: (class * tyco) * string -> theory -> theory
val const: theory -> CodegenConsts.const -> const
val const_rev: theory -> const -> CodegenConsts.const option
- val const_force: CodegenConsts.const * const -> theory -> theory
val purify_var: string -> string
val check_modulename: string -> string
val has_nsp: string -> string -> bool
@@ -248,42 +245,6 @@
val purify_base = purify_idf #> purify_lower;
-(* explicit given names with cache update *)
-
-fun force get defined upd_names upd errname string_of (x, name) thy =
- let
- val names = NameSpace.unpack name;
- val (prefix, base) = split_last (NameSpace.unpack name);
- val prefix' = purify_prefix prefix;
- val base' = purify_base base;
- val _ = if (base' = base) andalso forall (op =) (prefix' ~~ prefix)
- then ()
- else
- error ("Name violates naming conventions: " ^ quote name
- ^ "; perhaps try with " ^ quote (NameSpace.pack (prefix' @ [base'])))
- val names_ref = CodeName.get thy;
- val (Names names) = ! names_ref;
- val (tab, rev) = get names;
- val _ = if defined tab x
- then error ("Already named " ^ errname ^ ": " ^ string_of thy x)
- else ();
- val _ = if Symtab.defined rev name
- then error ("Name already given to other " ^ errname ^ ": " ^ quote name)
- else ();
- val _ = names_ref := upd_names (K (upd (x, name) tab,
- Symtab.update_new (name, x) rev)) (Names names);
- in
- thy
- end;
-
-val tyco_force = force #tyco Symtab.defined map_tyco Symtab.update_new
- "type constructor" (K quote);
-val instance_force = force #instance Insttab.defined map_inst Insttab.update_new
- "instance" (fn _ => fn (class, tyco) => quote class ^ ", " ^ quote tyco);
-val const_force = force #const Consttab.defined map_const Consttab.update_new
- "constant" (quote oo CodegenConsts.string_of_const);
-
-
(* naming policies *)
fun policy thy get_basename get_thyname name =
@@ -383,51 +344,4 @@
| _ => NONE))
|> Option.map (rev thy #const "constant");
-
-(* outer syntax *)
-
-local
-
-structure P = OuterParse
-and K = OuterKeyword
-
-fun const_force_e (raw_c, name) thy =
- const_force (CodegenConsts.read_const thy raw_c, name) thy;
-
-fun tyco_force_e (raw_tyco, name) thy =
- tyco_force (Sign.intern_type thy raw_tyco, name) thy;
-
-fun instance_force_e ((raw_tyco, raw_class), name) thy =
- instance_force ((Sign.intern_class thy raw_class, Sign.intern_type thy raw_tyco), name) thy;
-
-val (constnameK, typenameK, instnameK) = ("code_constname", "code_typename", "code_instname");
-
-val constnameP =
- OuterSyntax.improper_command constnameK "declare code name for constant" K.thy_decl (
- Scan.repeat1 (P.term -- P.name)
- >> (fn aliasses =>
- Toplevel.theory (fold const_force_e aliasses))
- );
-
-val typenameP =
- OuterSyntax.improper_command typenameK "declare code name for type constructor" K.thy_decl (
- Scan.repeat1 (P.xname -- P.name)
- >> (fn aliasses =>
- Toplevel.theory (fold tyco_force_e aliasses))
- );
-
-val instnameP =
- OuterSyntax.improper_command instnameK "declare code name for instance relation" K.thy_decl (
- Scan.repeat1 ((P.xname --| P.$$$ "::" -- P.xname) -- P.name)
- >> (fn aliasses =>
- Toplevel.theory (fold instance_force_e aliasses))
- );
-
-in
-
-val _ = OuterSyntax.add_parsers [constnameP, typenameP, instnameP];
-
-
-end; (*local*)
-
end;