src/HOL/ex/Codegenerator_Pretty.thy
author haftmann
Wed Mar 12 19:38:14 2008 +0100 (2008-03-12)
changeset 26265 4b63b9e9b10d
parent 26022 b30a342a6e29
child 26446 6abb5ed522a6
permissions -rw-r--r--
separated Random.thy from Quickcheck.thy
haftmann@24195
     1
(*  Title:      HOL/ex/Codegenerator_Pretty.thy
haftmann@24195
     2
    ID:         $Id$
haftmann@24195
     3
    Author:     Florian Haftmann, TU Muenchen
haftmann@24195
     4
*)
haftmann@24195
     5
haftmann@24195
     6
header {* Simple examples for pretty numerals and such *}
haftmann@24195
     7
haftmann@24195
     8
theory Codegenerator_Pretty
haftmann@25963
     9
imports ExecutableContent Code_Char Efficient_Nat
haftmann@24195
    10
begin
haftmann@24195
    11
haftmann@26022
    12
setup {*
haftmann@26022
    13
  Code.del_funcs
haftmann@26022
    14
    (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "index"}))
haftmann@26022
    15
  #> Code.del_funcs
haftmann@26022
    16
    (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "char"}))
haftmann@26022
    17
  #> Code.del_funcs
haftmann@26022
    18
    (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "int"}))
haftmann@26022
    19
  #> Code.del_funcs
haftmann@26022
    20
    (AxClass.param_of_inst @{theory} (@{const_name "Eval.term_of"}, @{type_name "nat"}))
haftmann@26022
    21
*}
haftmann@25933
    22
haftmann@25963
    23
declare char.recs [code func del]
haftmann@25963
    24
  char.cases [code func del]
haftmann@25963
    25
  char.size [code func del]
haftmann@24195
    26
haftmann@25963
    27
declare isnorm.simps [code func del]
haftmann@25933
    28
haftmann@25963
    29
ML {* (*FIXME get rid of this*)
haftmann@25963
    30
nonfix union;
haftmann@25963
    31
nonfix inter;
haftmann@25963
    32
nonfix upto;
haftmann@25963
    33
*}
haftmann@25933
    34
haftmann@25963
    35
export_code * in SML module_name CodegenTest
haftmann@25963
    36
  in OCaml module_name CodegenTest file -
haftmann@25963
    37
  in Haskell file -
haftmann@25616
    38
haftmann@25963
    39
ML {*
haftmann@25963
    40
infix union;
haftmann@25963
    41
infix inter;
haftmann@25963
    42
infix 4 upto;
haftmann@25963
    43
*}
haftmann@24195
    44
haftmann@24195
    45
end