Auxiliary functions to be used in generated code are now defined using "attach".
authorberghofe
Tue Jul 12 11:51:31 2005 +0200 (2005-07-12)
changeset 167701f1b1fae30e4
parent 16769 7f188f2127f7
child 16771 2b534c5b5625
Auxiliary functions to be used in generated code are now defined using "attach".
src/HOL/Integ/IntDef.thy
src/HOL/Library/EfficientNat.thy
src/HOL/List.thy
src/HOL/Main.thy
src/HOL/MicroJava/J/JListExample.thy
src/HOL/MicroJava/JVM/JVMListExample.thy
src/HOL/Product_Type.thy
     1.1 --- a/src/HOL/Integ/IntDef.thy	Tue Jul 12 11:41:24 2005 +0200
     1.2 +++ b/src/HOL/Integ/IntDef.thy	Tue Jul 12 11:51:31 2005 +0200
     1.3 @@ -855,17 +855,16 @@
     1.4  
     1.5  subsection {* Configuration of the code generator *}
     1.6  
     1.7 -ML {*
     1.8 -infix 7 `*;
     1.9 -infix 6 `+;
    1.10 -
    1.11 -val op `* = op * : int * int -> int;
    1.12 -val op `+ = op + : int * int -> int;
    1.13 -val `~ = ~ : int -> int;
    1.14 -*}
    1.15 +(*FIXME: the IntInf.fromInt below hides a dependence on fixed-precision ints!*)
    1.16  
    1.17  types_code
    1.18    "int" ("int")
    1.19 +attach (term_of) {*
    1.20 +val term_of_int = HOLogic.mk_int o IntInf.fromInt;
    1.21 +*}
    1.22 +attach (test) {*
    1.23 +fun gen_int i = one_of [~1, 1] * random_range 0 i;
    1.24 +*}
    1.25  
    1.26  constdefs
    1.27    int_aux :: "int \<Rightarrow> nat \<Rightarrow> int"
    1.28 @@ -889,9 +888,9 @@
    1.29  consts_code
    1.30    "0" :: "int"                  ("0")
    1.31    "1" :: "int"                  ("1")
    1.32 -  "uminus" :: "int => int"      ("`~")
    1.33 -  "op +" :: "int => int => int" ("(_ `+/ _)")
    1.34 -  "op *" :: "int => int => int" ("(_ `*/ _)")
    1.35 +  "uminus" :: "int => int"      ("~")
    1.36 +  "op +" :: "int => int => int" ("(_ +/ _)")
    1.37 +  "op *" :: "int => int => int" ("(_ */ _)")
    1.38    "op <" :: "int => int => bool" ("(_ </ _)")
    1.39    "op <=" :: "int => int => bool" ("(_ <=/ _)")
    1.40    "neg"                         ("(_ < 0)")
     2.1 --- a/src/HOL/Library/EfficientNat.thy	Tue Jul 12 11:41:24 2005 +0200
     2.2 +++ b/src/HOL/Library/EfficientNat.thy	Tue Jul 12 11:51:31 2005 +0200
     2.3 @@ -30,16 +30,26 @@
     2.4  returns @{text "0"}.
     2.5  *}
     2.6  
     2.7 -types_code nat ("int")
     2.8 +types_code
     2.9 +  nat ("int")
    2.10 +attach (term_of) {*
    2.11 +fun term_of_nat 0 = Const ("0", HOLogic.natT)
    2.12 +  | term_of_nat 1 = Const ("1", HOLogic.natT)
    2.13 +  | term_of_nat i = HOLogic.number_of_const HOLogic.natT $
    2.14 +      HOLogic.mk_bin (IntInf.fromInt i);
    2.15 +*}
    2.16 +attach (test) {*
    2.17 +fun gen_nat i = random_range 0 i;
    2.18 +*}
    2.19 +
    2.20  consts_code
    2.21    0 :: nat ("0")
    2.22    Suc ("(_ + 1)")
    2.23 -  nat ("nat")
    2.24 -  int ("(_)")
    2.25 -
    2.26 -ML {*
    2.27 +  nat ("\<module>nat")
    2.28 +attach {*
    2.29  fun nat i = if i < 0 then 0 else i;
    2.30  *}
    2.31 +  int ("(_)")
    2.32  
    2.33  text {*
    2.34  Case analysis on natural numbers is rephrased using a conditional
     3.1 --- a/src/HOL/List.thy	Tue Jul 12 11:41:24 2005 +0200
     3.2 +++ b/src/HOL/List.thy	Tue Jul 12 11:51:31 2005 +0200
     3.3 @@ -2282,27 +2282,31 @@
     3.4     Codegen.add_codegen "char_codegen" char_codegen];
     3.5  
     3.6  end;
     3.7 -
     3.8 +*}
     3.9 +
    3.10 +types_code
    3.11 +  "list" ("_ list")
    3.12 +attach (term_of) {*
    3.13  val term_of_list = HOLogic.mk_list;
    3.14 -
    3.15 +*}
    3.16 +attach (test) {*
    3.17  fun gen_list' aG i j = frequency
    3.18    [(i, fn () => aG j :: gen_list' aG (i-1) j), (1, fn () => [])] ()
    3.19  and gen_list aG i = gen_list' aG i i;
    3.20 -
    3.21 +*}
    3.22 +  "char" ("string")
    3.23 +attach (term_of) {*
    3.24  val nibbleT = Type ("List.nibble", []);
    3.25  
    3.26  fun term_of_char c =
    3.27    Const ("List.char.Char", nibbleT --> nibbleT --> Type ("List.char", [])) $
    3.28      Const ("List.nibble.Nibble" ^ nibble_of_int (ord c div 16), nibbleT) $
    3.29      Const ("List.nibble.Nibble" ^ nibble_of_int (ord c mod 16), nibbleT);
    3.30 -
    3.31 +*}
    3.32 +attach (test) {*
    3.33  fun gen_char i = chr (random_range (ord "a") (Int.min (ord "a" + i, ord "z")));
    3.34  *}
    3.35  
    3.36 -types_code
    3.37 -  "list" ("_ list")
    3.38 -  "char" ("string")
    3.39 -
    3.40  consts_code "Cons" ("(_ ::/ _)")
    3.41  
    3.42  setup list_codegen_setup
     4.1 --- a/src/HOL/Main.thy	Tue Jul 12 11:41:24 2005 +0200
     4.2 +++ b/src/HOL/Main.thy	Tue Jul 12 11:51:31 2005 +0200
     4.3 @@ -19,6 +19,12 @@
     4.4  
     4.5  types_code
     4.6    "bool"  ("bool")
     4.7 +attach (term_of) {*
     4.8 +fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
     4.9 +*}
    4.10 +attach (test) {*
    4.11 +fun gen_bool i = one_of [false, true];
    4.12 +*}
    4.13  
    4.14  consts_code
    4.15    "True"    ("true")
    4.16 @@ -28,18 +34,14 @@
    4.17    "op &"    ("(_ andalso/ _)")
    4.18    "HOL.If"      ("(if _/ then _/ else _)")
    4.19  
    4.20 -  "wfrec"   ("wf'_rec?")
    4.21 +  "wfrec"   ("\<module>wf'_rec?")
    4.22 +attach {*
    4.23 +fun wf_rec f x = f (wf_rec f) x;
    4.24 +*}
    4.25  
    4.26  quickcheck_params [default_type = int]
    4.27  
    4.28 -(*FIXME: the IntInf.fromInt below hides a dependence on fixed-precision ints!*)
    4.29  ML {*
    4.30 -fun wf_rec f x = f (wf_rec f) x;
    4.31 -
    4.32 -fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    4.33 -val term_of_int = HOLogic.mk_int o IntInf.fromInt;
    4.34 -fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
    4.35 -
    4.36  local
    4.37  
    4.38  fun eq_codegen thy defs gr dep thyname b t =
    4.39 @@ -62,20 +64,6 @@
    4.40  val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" eq_codegen];
    4.41  
    4.42  end;
    4.43 -
    4.44 -fun gen_bool i = one_of [false, true];
    4.45 -
    4.46 -fun gen_int i = one_of [~1, 1] * random_range 0 i;
    4.47 -
    4.48 -fun gen_fun_type _ G i =
    4.49 -  let
    4.50 -    val f = ref (fn x => raise ERROR);
    4.51 -    val _ = (f := (fn x =>
    4.52 -      let
    4.53 -        val y = G i;
    4.54 -        val f' = !f
    4.55 -      in (f := (fn x' => if x = x' then y else f' x'); y) end))
    4.56 -  in (fn x => !f x) end;
    4.57  *}
    4.58  
    4.59  setup eq_codegen_setup
     5.1 --- a/src/HOL/MicroJava/J/JListExample.thy	Tue Jul 12 11:41:24 2005 +0200
     5.2 +++ b/src/HOL/MicroJava/J/JListExample.thy	Tue Jul 12 11:51:31 2005 +0200
     5.3 @@ -65,7 +65,12 @@
     5.4    loc_ ("int")
     5.5  
     5.6  consts_code
     5.7 -  "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *} {* Loc *}")
     5.8 +  "new_Addr" ("\<module>new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *} {* Loc *}")
     5.9 +attach {*
    5.10 +fun new_addr p none loc hp =
    5.11 +  let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1);
    5.12 +  in nr 0 end;
    5.13 +*}
    5.14  
    5.15    "arbitrary" ("(raise ERROR)")
    5.16    "arbitrary" :: "val" ("{* Unit *}")
    5.17 @@ -82,12 +87,6 @@
    5.18    "l3_nam" ("\"l3\"")
    5.19    "l4_nam" ("\"l4\"")
    5.20  
    5.21 -ML {*
    5.22 -fun new_addr p none loc hp =
    5.23 -  let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1);
    5.24 -  in nr 0 end;
    5.25 -*}
    5.26 -
    5.27  generate_code
    5.28    test = "example_prg\<turnstile>Norm (empty, empty)
    5.29      -(Expr (l1_name::=NewC list_name);;
     6.1 --- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Jul 12 11:41:24 2005 +0200
     6.2 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Jul 12 11:51:31 2005 +0200
     6.3 @@ -94,7 +94,12 @@
     6.4    loc_ ("int")
     6.5  
     6.6  consts_code
     6.7 -  "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}")
     6.8 +  "new_Addr" ("\<module>new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}")
     6.9 +attach {*
    6.10 +fun new_addr p none loc hp =
    6.11 +  let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1);
    6.12 +  in nr 0 end;
    6.13 +*}
    6.14  
    6.15    "arbitrary" ("(raise ERROR)")
    6.16    "arbitrary" :: "val" ("{* Unit *}")
    6.17 @@ -107,12 +112,6 @@
    6.18    "val_nam" ("\"val\"")
    6.19    "next_nam" ("\"next\"")
    6.20  
    6.21 -ML {*
    6.22 -fun new_addr p none loc hp =
    6.23 -  let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1);
    6.24 -  in nr 0 end;
    6.25 -*}
    6.26 -
    6.27  subsection {* Single step execution *}
    6.28  
    6.29  generate_code
     7.1 --- a/src/HOL/Product_Type.thy	Tue Jul 12 11:41:24 2005 +0200
     7.2 +++ b/src/HOL/Product_Type.thy	Tue Jul 12 11:51:31 2005 +0200
     7.3 @@ -773,6 +773,12 @@
     7.4  
     7.5  types_code
     7.6    "*"     ("(_ */ _)")
     7.7 +attach (term_of) {*
     7.8 +fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y;
     7.9 +*}
    7.10 +attach (test) {*
    7.11 +fun gen_id_42 aG bG i = (aG i, bG i);
    7.12 +*}
    7.13  
    7.14  consts_code
    7.15    "Pair"    ("(_,/ _)")
    7.16 @@ -780,10 +786,6 @@
    7.17    "snd"     ("snd")
    7.18  
    7.19  ML {*
    7.20 -fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y;
    7.21 -
    7.22 -fun gen_id_42 aG bG i = (aG i, bG i);
    7.23 -
    7.24  local
    7.25  
    7.26  fun strip_abs 0 t = ([], t)