# HG changeset patch # User haftmann # Date 1162826911 -3600 # Node ID c00161fbf9905702c332739bbece1b86a90906aa # Parent 08ec81dfc7fb383cfc5d6b20ff9c4fae6f9536b6 code generator module naming improved diff -r 08ec81dfc7fb -r c00161fbf990 src/HOL/Divides.thy --- 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 \ nat \ nat \ nat" "IntDef.div_nat" - "op mod \ nat \ nat \ nat" "IntDef.mod_nat" - Divides.divmod "IntDef.divmod_nat" +code_modulename SML + Divides Integer hide (open) const divmod diff -r 08ec81dfc7fb -r c00161fbf990 src/HOL/Integ/IntArith.thy --- 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 \ int \ 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 \ bit \ bit \ 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" .. diff -r 08ec81dfc7fb -r c00161fbf990 src/HOL/Integ/IntDef.thy --- 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) = diff -r 08ec81dfc7fb -r c00161fbf990 src/HOL/Library/EfficientNat.thy --- 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 diff -r 08ec81dfc7fb -r c00161fbf990 src/HOL/Library/ExecutableRat.thy --- 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\erat" "Rational.erat_zero" - "1\erat" "Rational.erat_one" - "op + \ erat \ erat \ erat" "Rational.erat_plus" - "uminus \ erat \ erat" "Rational.erat_uminus" - "op * \ erat \ erat \ erat" "Rational.erat_times" - "inverse \ erat \ erat" "Rational.erat_inverse" - "op \ \ erat \ erat \ bool" "Rational.erat_le" - "Code_Generator.eq \ erat \ erat \ 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 \ of_quotient "0 \ rat" \ "0 \ erat" @@ -127,7 +112,7 @@ "op * \ rat \ rat \ rat" \ "op * \ erat \ erat \ erat" "inverse \ rat \ rat" \ "inverse \ erat \ erat" "op \ \ rat \ rat \ bool" \ "op \ \ erat \ erat \ bool" - "Code_Generator.eq \ rat \ rat \ bool" \ eq_erat + "Code_Generator.eq \ rat \ rat \ bool" \ eq_erat code_const div_zero (SML "raise/ (Fail/ \"Division by zero\")") diff -r 08ec81dfc7fb -r c00161fbf990 src/HOL/Library/ExecutableSet.thy --- 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 \ Blex code_gen "{}" insert "op \" "op \" "op - \ 'a set \ 'a set \ 'a set" - image Union Inter UNION INTER Ball Bex (SML *) + image Union Inter UNION INTER Ball Bex (SML -) subsection {* type serializations *} diff -r 08ec81dfc7fb -r c00161fbf990 src/HOL/Nat.thy --- 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 \ nat" "IntDef.zero_nat" - "1 \ nat" "IntDef.one_nat" - Suc "IntDef.succ_nat" - "op + \ nat \ nat \ nat" "IntDef.plus_nat" - "op - \ nat \ nat \ nat" "IntDef.minus_nat" - "op * \ nat \ nat \ nat" "IntDef.times_nat" - "op < \ nat \ nat \ bool" "IntDef.less_nat" - "op \ \ nat \ nat \ bool" "IntDef.less_eq_nat" - "Code_Generator.eq \ nat \ nat \ bool" "IntDef.eq_nat" - nat_rec "IntDef.nat_rec" - nat_case "IntDef.nat_case" - end diff -r 08ec81dfc7fb -r c00161fbf990 src/HOL/ex/Codegenerator.thy --- 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 = (\x. x (\x. x (\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 diff -r 08ec81dfc7fb -r c00161fbf990 src/Pure/Tools/codegen_names.ML --- 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;