src/HOL/ex/Codegenerator.thy
changeset 21911 e29bcab0c81c
parent 21898 46be40d304d7
child 21922 76e1fce071aa
     1.1 --- a/src/HOL/ex/Codegenerator.thy	Wed Dec 27 19:09:59 2006 +0100
     1.2 +++ b/src/HOL/ex/Codegenerator.thy	Wed Dec 27 19:10:00 2006 +0100
     1.3 @@ -5,77 +5,14 @@
     1.4  header {* Tests and examples for code generator *}
     1.5  
     1.6  theory Codegenerator
     1.7 -imports
     1.8 -  Main
     1.9 -  "~~/src/HOL/ex/Records"
    1.10 -  AssocList
    1.11 -  Binomial
    1.12 -  Commutative_Ring
    1.13 -  GCD
    1.14 -  List_Prefix
    1.15 -  Nat_Infinity
    1.16 -  NatPair
    1.17 -  Nested_Environment
    1.18 -  Permutation
    1.19 -  Primes
    1.20 -  Product_ord
    1.21 -  SetsAndFunctions
    1.22 -  State_Monad
    1.23 -  While_Combinator
    1.24 -  Word
    1.25 -  (*a lot of stuff to test*)
    1.26 +imports ExecutableContent
    1.27  begin
    1.28  
    1.29 -definition
    1.30 -  n :: nat where
    1.31 -  "n = 42"
    1.32 -
    1.33 -definition
    1.34 -  k :: "int" where
    1.35 -  "k = -42"
    1.36 -
    1.37 -datatype mut1 = Tip | Top mut2
    1.38 -  and mut2 = Tip | Top mut1
    1.39 -
    1.40 -consts
    1.41 -  mut1 :: "mut1 \<Rightarrow> mut1"
    1.42 -  mut2 :: "mut2 \<Rightarrow> mut2"
    1.43 -
    1.44 -primrec
    1.45 -  "mut1 mut1.Tip = mut1.Tip"
    1.46 -  "mut1 (mut1.Top x) = mut1.Top (mut2 x)"
    1.47 -  "mut2 mut2.Tip = mut2.Tip"
    1.48 -  "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
    1.49 -
    1.50 -definition
    1.51 -  "mystring = ''my home is my castle''"
    1.52 -
    1.53 -text {* nested lets and such *}
    1.54 +code_gen "*" (SML #) (Haskell -)
    1.55  
    1.56 -definition
    1.57 -  "abs_let x = (let (y, z) = x in (\<lambda>u. case u of () \<Rightarrow> (y + y)))"
    1.58 -
    1.59 -definition
    1.60 -  "nested_let x = (let (y, z) = x in let w = y z in w * w)"
    1.61 -
    1.62 -definition
    1.63 -  "case_let x = (let (y, z) = x in case y of () => z)"
    1.64 -
    1.65 -definition
    1.66 -  "base_case f = f list_case"
    1.67 +ML {* set Toplevel.debug *}
    1.68 +code_gen (OCaml "~/projects/codegen/test/OCaml/ROOT.ocaml")
    1.69  
    1.70 -definition
    1.71 -  "apply_tower = (\<lambda>x. x (\<lambda>x. x (\<lambda>x. x)))"
    1.72 -
    1.73 -definition
    1.74 -  "keywords fun datatype x instance funa classa =
    1.75 -    Suc fun + datatype * x mod instance - funa - classa"
    1.76 -
    1.77 -hide (open) const keywords
    1.78 -
    1.79 -definition
    1.80 -  "shadow keywords = keywords @ [Codegenerator.keywords 0 0 0 0 0 0]"
    1.81 -
    1.82 -(*code_gen "*" (Haskell -) (SML #)*)
    1.83 +code_gen "*"(OCaml "~/projects/codegen/test/OCaml/ROOT.ocaml")
    1.84  
    1.85  end
    1.86 \ No newline at end of file