src/HOL/ex/Codegenerator_Pretty.thy
author haftmann
Thu Aug 09 15:52:45 2007 +0200 (2007-08-09)
changeset 24195 7d1a16c77f7c
child 24249 1f60b45c5f97
permissions -rw-r--r--
tuned
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@24195
     9
imports Executable_Rat Executable_Real Efficient_Nat
haftmann@24195
    10
begin
haftmann@24195
    11
haftmann@24195
    12
definition
haftmann@24195
    13
  foo :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> rat" where
haftmann@24195
    14
  "foo r s t = (t + s) / t"
haftmann@24195
    15
haftmann@24195
    16
definition
haftmann@24195
    17
  bar :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> bool" where
haftmann@24195
    18
  "bar r s t \<longleftrightarrow> (r - s) \<le> t \<or> (s - t) \<le> r"
haftmann@24195
    19
haftmann@24195
    20
definition
haftmann@24195
    21
  "R1 = Fract 3 7"
haftmann@24195
    22
haftmann@24195
    23
definition
haftmann@24195
    24
  "R2 = Fract (-7) 5"
haftmann@24195
    25
haftmann@24195
    26
definition
haftmann@24195
    27
  "R3 = Fract 11 (-9)"
haftmann@24195
    28
haftmann@24195
    29
definition
haftmann@24195
    30
  "foobar = (foo R1 1 R3, bar R2 0 R3, foo R1 R3 R2)"
haftmann@24195
    31
haftmann@24195
    32
definition
haftmann@24195
    33
  foo' :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real" where
haftmann@24195
    34
  "foo' r s t = (t + s) / t"
haftmann@24195
    35
haftmann@24195
    36
definition
haftmann@24195
    37
  bar' :: "real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> bool" where
haftmann@24195
    38
  "bar' r s t \<longleftrightarrow> (r - s) \<le> t \<or> (s - t) \<le> r"
haftmann@24195
    39
haftmann@24195
    40
definition
haftmann@24195
    41
  "R1' = real_of_rat (Fract 3 7)"
haftmann@24195
    42
haftmann@24195
    43
definition
haftmann@24195
    44
  "R2' = real_of_rat (Fract (-7) 5)"
haftmann@24195
    45
haftmann@24195
    46
definition
haftmann@24195
    47
  "R3' = real_of_rat (Fract 11 (-9))"
haftmann@24195
    48
haftmann@24195
    49
definition
haftmann@24195
    50
  "foobar' = (foo' R1' 1 R3', bar' R2' 0 R3', foo' R1' R3' R2')"
haftmann@24195
    51
haftmann@24195
    52
code_gen foobar foobar' in SML to Foo
haftmann@24195
    53
  in OCaml file -
haftmann@24195
    54
  in Haskell file -
haftmann@24195
    55
ML {* (Foo.foobar, Foo.foobar') *}
haftmann@24195
    56
haftmann@24195
    57
end