src/HOL/Main.thy
changeset 15063 a43d771c18ac
parent 14981 e73f8140af78
child 15131 c69542757a4d
equal deleted inserted replaced
15062:8049f217428e 15063:a43d771c18ac
    15 subsection {* Configuration of the code generator *}
    15 subsection {* Configuration of the code generator *}
    16 
    16 
    17 types_code
    17 types_code
    18   "bool"  ("bool")
    18   "bool"  ("bool")
    19   "*"     ("(_ */ _)")
    19   "*"     ("(_ */ _)")
    20   "list"  ("_ list")
       
    21 
    20 
    22 consts_code
    21 consts_code
    23   "True"    ("true")
    22   "True"    ("true")
    24   "False"   ("false")
    23   "False"   ("false")
    25   "Not"     ("not")
    24   "Not"     ("not")
    29 
    28 
    30   "Pair"    ("(_,/ _)")
    29   "Pair"    ("(_,/ _)")
    31   "fst"     ("fst")
    30   "fst"     ("fst")
    32   "snd"     ("snd")
    31   "snd"     ("snd")
    33 
    32 
    34   "Nil"     ("[]")
       
    35   "Cons"    ("(_ ::/ _)")
       
    36 
       
    37   "wfrec"   ("wf'_rec?")
    33   "wfrec"   ("wf'_rec?")
    38 
    34 
    39 quickcheck_params [default_type = int]
    35 quickcheck_params [default_type = int]
    40 
    36 
    41 ML {*
    37 ML {*
    42 fun wf_rec f x = f (wf_rec f) x;
    38 fun wf_rec f x = f (wf_rec f) x;
    43 
    39 
    44 fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    40 fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    45 val term_of_list = HOLogic.mk_list;
       
    46 val term_of_int = HOLogic.mk_int;
    41 val term_of_int = HOLogic.mk_int;
    47 fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y;
    42 fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y;
    48 fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
    43 fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
    49 
    44 
    50 val eq_codegen_setup = [Codegen.add_codegen "eq_codegen"
    45 val eq_codegen_setup = [Codegen.add_codegen "eq_codegen"
    62      | (t as Const ("op =", _), ts) => Some (Codegen.invoke_codegen
    57      | (t as Const ("op =", _), ts) => Some (Codegen.invoke_codegen
    63          thy dep b (gr, Codegen.eta_expand t ts 2))
    58          thy dep b (gr, Codegen.eta_expand t ts 2))
    64      | _ => None))];
    59      | _ => None))];
    65 
    60 
    66 fun gen_bool i = one_of [false, true];
    61 fun gen_bool i = one_of [false, true];
    67 
       
    68 fun gen_list' aG i j = frequency
       
    69   [(i, fn () => aG j :: gen_list' aG (i-1) j), (1, fn () => [])] ()
       
    70 and gen_list aG i = gen_list' aG i i;
       
    71 
    62 
    72 fun gen_int i = one_of [~1, 1] * random_range 0 i;
    63 fun gen_int i = one_of [~1, 1] * random_range 0 i;
    73 
    64 
    74 fun gen_id_42 aG bG i = (aG i, bG i);
    65 fun gen_id_42 aG bG i = (aG i, bG i);
    75 
    66