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