src/HOL/ex/Codegenerator_Rat.thy
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 22845 5f9138bcb3d7
child 23811 b18557301bf9
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
haftmann@22071
     1
(*  Title:      HOL/Library/ExecutableRat.thy
haftmann@22071
     2
    ID:         $Id$
haftmann@22071
     3
    Author:     Florian Haftmann, TU Muenchen
haftmann@22071
     4
*)
haftmann@22071
     5
haftmann@22071
     6
header {* Simple example for executable rational numbers *}
haftmann@22071
     7
haftmann@22071
     8
theory Codegenerator_Rat
haftmann@22803
     9
imports ExecutableRat EfficientNat
haftmann@22071
    10
begin
haftmann@22071
    11
haftmann@22071
    12
definition
haftmann@22071
    13
  foo :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> rat" where
haftmann@22071
    14
  "foo r s t = (t + s) / t"
haftmann@22071
    15
haftmann@22071
    16
definition
haftmann@22071
    17
  bar :: "rat \<Rightarrow> rat \<Rightarrow> rat \<Rightarrow> bool" where
haftmann@22071
    18
  "bar r s t \<longleftrightarrow> (r - s) \<le> t \<or> (s - t) \<le> r"
haftmann@22071
    19
haftmann@22071
    20
definition
haftmann@22071
    21
  "R1 = Fract 3 7"
haftmann@22071
    22
haftmann@22071
    23
definition
haftmann@22071
    24
  "R2 = Fract (-7) 5"
haftmann@22071
    25
haftmann@22071
    26
definition
haftmann@22071
    27
  "R3 = Fract 11 (-9)"
haftmann@22071
    28
haftmann@22071
    29
definition
haftmann@22071
    30
  "foobar = (foo R1 1 R3, bar R2 0 R3, foo R1 R3 R2)"
haftmann@22071
    31
haftmann@22845
    32
code_gen foobar in SML in OCaml file - in Haskell file -
haftmann@22071
    33
ML {* ROOT.Codegenerator_Rat.foobar *}
haftmann@22071
    34
haftmann@22071
    35
code_module Foo
haftmann@22071
    36
  contains foobar
haftmann@22071
    37
ML {* Foo.foobar *}
haftmann@22071
    38
haftmann@22071
    39
end