src/HOL/ex/Codegenerator.thy
author haftmann
Thu Dec 21 13:55:12 2006 +0100 (2006-12-21)
changeset 21892 af35b480916e
parent 21877 e871f57b1adb
child 21898 46be40d304d7
permissions -rw-r--r--
import path made absolute
haftmann@19281
     1
(*  ID:         $Id$
haftmann@19281
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@19281
     3
*)
haftmann@19281
     4
haftmann@21877
     5
header {* Tests and examples for code generator *}
haftmann@19281
     6
haftmann@19281
     7
theory Codegenerator
haftmann@21877
     8
imports
haftmann@21877
     9
  Main
haftmann@21892
    10
  "~~/src/HOL/ex/Records"
haftmann@21877
    11
  AssocList
haftmann@21877
    12
  Binomial
haftmann@21877
    13
  Commutative_Ring
haftmann@21877
    14
  GCD
haftmann@21877
    15
  List_Prefix
haftmann@21877
    16
  Nat_Infinity
haftmann@21877
    17
  NatPair
haftmann@21877
    18
  Nested_Environment
haftmann@21877
    19
  Permutation
haftmann@21877
    20
  Primes
haftmann@21877
    21
  Product_ord
haftmann@21877
    22
  SetsAndFunctions
haftmann@21877
    23
  State_Monad
haftmann@21877
    24
  While_Combinator
haftmann@21877
    25
  Word
haftmann@21877
    26
  (*a lot of stuff to test*)
haftmann@19281
    27
begin
haftmann@19281
    28
haftmann@19281
    29
definition
wenzelm@21404
    30
  n :: nat where
haftmann@19281
    31
  "n = 42"
haftmann@19281
    32
haftmann@19281
    33
definition
wenzelm@21404
    34
  k :: "int" where
haftmann@20351
    35
  "k = -42"
haftmann@19281
    36
haftmann@19281
    37
datatype mut1 = Tip | Top mut2
haftmann@19281
    38
  and mut2 = Tip | Top mut1
haftmann@19281
    39
haftmann@19281
    40
consts
haftmann@19281
    41
  mut1 :: "mut1 \<Rightarrow> mut1"
haftmann@19281
    42
  mut2 :: "mut2 \<Rightarrow> mut2"
haftmann@19281
    43
haftmann@19281
    44
primrec
haftmann@19281
    45
  "mut1 mut1.Tip = mut1.Tip"
haftmann@19281
    46
  "mut1 (mut1.Top x) = mut1.Top (mut2 x)"
haftmann@19281
    47
  "mut2 mut2.Tip = mut2.Tip"
haftmann@19281
    48
  "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
haftmann@19281
    49
haftmann@20702
    50
definition
haftmann@20702
    51
  "mystring = ''my home is my castle''"
haftmann@20702
    52
haftmann@21877
    53
text {* nested lets and such *}
haftmann@20968
    54
haftmann@20968
    55
definition
haftmann@20968
    56
  "abs_let x = (let (y, z) = x in (\<lambda>u. case u of () \<Rightarrow> (y + y)))"
haftmann@20968
    57
haftmann@20968
    58
definition
haftmann@20968
    59
  "nested_let x = (let (y, z) = x in let w = y z in w * w)"
haftmann@20968
    60
haftmann@20968
    61
definition
haftmann@20968
    62
  "case_let x = (let (y, z) = x in case y of () => z)"
haftmann@20968
    63
haftmann@21155
    64
definition
haftmann@21155
    65
  "base_case f = f list_case"
haftmann@21155
    66
haftmann@20702
    67
definition
haftmann@20702
    68
  "apply_tower = (\<lambda>x. x (\<lambda>x. x (\<lambda>x. x)))"
haftmann@20702
    69
haftmann@20702
    70
definition
haftmann@21877
    71
  "keywords fun datatype x instance funa classa =
haftmann@21877
    72
    Suc fun + datatype * x mod instance - funa - classa"
haftmann@20702
    73
haftmann@20702
    74
hide (open) const keywords
haftmann@20702
    75
haftmann@20702
    76
definition
haftmann@20702
    77
  "shadow keywords = keywords @ [Codegenerator.keywords 0 0 0 0 0 0]"
haftmann@20702
    78
haftmann@21877
    79
code_gen "*" (Haskell -) (SML #)
haftmann@19281
    80
haftmann@19281
    81
end