src/HOL/ex/Codegenerator.thy
author haftmann
Tue Sep 26 13:34:16 2006 +0200 (2006-09-26)
changeset 20713 823967ef47f1
parent 20702 8b79d853eabb
child 20807 bd3b60f9a343
permissions -rw-r--r--
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
     1 (*  ID:         $Id$
     2     Author:     Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 header {* Test and Examples for code generator *}
     6 
     7 theory Codegenerator
     8 imports Main "~~/src/HOL/ex/Records"
     9 begin
    10 
    11 subsection {* booleans *}
    12 
    13 definition
    14   xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
    15   "xor p q = ((p | q) & \<not> (p & q))"
    16 
    17 subsection {* natural numbers *}
    18 
    19 definition
    20   n :: nat
    21   "n = 42"
    22 
    23 subsection {* pairs *}
    24 
    25 definition
    26   swap :: "'a * 'b \<Rightarrow> 'b * 'a"
    27   "swap p = (let (x, y) = p in (y, x))"
    28   appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b"
    29   "appl p = (let (f, x) = p in f x)"
    30 
    31 subsection {* integers *}
    32 
    33 definition
    34   k :: "int"
    35   "k = -42"
    36 
    37 consts
    38   fac :: "int => int"
    39 
    40 recdef fac "measure nat"
    41   "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
    42 
    43 subsection {* sums *}
    44 
    45 subsection {* options *}
    46 
    47 subsection {* lists *}
    48 
    49 definition
    50   ps :: "nat list"
    51   "ps = [2, 3, 5, 7, 11]"
    52   qs :: "nat list"
    53   "qs == rev ps"
    54 
    55 subsection {* mutual datatypes *}
    56 
    57 datatype mut1 = Tip | Top mut2
    58   and mut2 = Tip | Top mut1
    59 
    60 consts
    61   mut1 :: "mut1 \<Rightarrow> mut1"
    62   mut2 :: "mut2 \<Rightarrow> mut2"
    63 
    64 primrec
    65   "mut1 mut1.Tip = mut1.Tip"
    66   "mut1 (mut1.Top x) = mut1.Top (mut2 x)"
    67   "mut2 mut2.Tip = mut2.Tip"
    68   "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
    69 
    70 subsection {* records *}
    71 
    72 subsection {* equalities *}
    73 
    74 subsection {* strings *}
    75 
    76 definition
    77   "mystring = ''my home is my castle''"
    78 
    79 subsection {* heavy usage of names *}
    80 
    81 definition
    82   f :: nat
    83   "f = 2"
    84   g :: nat
    85   "g = f"
    86   h :: nat
    87   "h = g"
    88 
    89 code_constname
    90   f "Mymod.f"
    91   g "Mymod.A.f"
    92   h "Mymod.A.B.f"
    93 
    94 definition
    95   "apply_tower = (\<lambda>x. x (\<lambda>x. x (\<lambda>x. x)))"
    96 
    97 definition
    98   "keywords fun datatype class instance funa classa =
    99     Suc fun + datatype * class mod instance - funa - classa"
   100 
   101 hide (open) const keywords
   102 
   103 definition
   104   "shadow keywords = keywords @ [Codegenerator.keywords 0 0 0 0 0 0]"
   105 
   106 code_gen
   107   xor
   108 code_gen
   109   "0::nat" "1::nat"
   110 code_gen
   111   Pair fst snd Let split swap
   112 code_gen "0::int" "1::int"
   113   (SML) (Haskell)
   114 code_gen n
   115   (SML) (Haskell)
   116 code_gen fac
   117   (SML) (Haskell)
   118 code_gen
   119   "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
   120   "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
   121   "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"
   122   "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
   123   "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
   124 code_gen
   125   appl
   126 code_gen
   127   k
   128   "op + :: int \<Rightarrow> int \<Rightarrow> int"
   129   "op - :: int \<Rightarrow> int \<Rightarrow> int"
   130   "op * :: int \<Rightarrow> int \<Rightarrow> int"
   131   "op < :: int \<Rightarrow> int \<Rightarrow> bool"
   132   "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
   133   fac
   134   "op div :: int \<Rightarrow> int \<Rightarrow> int"
   135   "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
   136   (SML) (Haskell)
   137 code_gen
   138   Inl Inr
   139 code_gen
   140   None Some
   141 code_gen
   142   hd tl "op @" ps qs
   143 code_gen
   144   mut1 mut2
   145 code_gen
   146   remove1
   147   null
   148   replicate
   149   rotate1
   150   rotate
   151   splice
   152 code_gen
   153   remdups
   154   "distinct"
   155 code_gen
   156   foo1 foo3
   157 code_gen
   158   "OperationalEquality.eq :: bool \<Rightarrow> bool \<Rightarrow> bool"
   159   "OperationalEquality.eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
   160   "OperationalEquality.eq :: int \<Rightarrow> int \<Rightarrow> bool"
   161   "OperationalEquality.eq :: ('a\<Colon>eq) * ('b\<Colon>eq) \<Rightarrow> 'a * 'b \<Rightarrow> bool"
   162   "OperationalEquality.eq :: ('a\<Colon>eq) + ('b\<Colon>eq) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
   163   "OperationalEquality.eq :: ('a\<Colon>eq) option \<Rightarrow> 'a option \<Rightarrow> bool"
   164   "OperationalEquality.eq :: ('a\<Colon>eq) list \<Rightarrow> 'a list \<Rightarrow> bool"
   165   "OperationalEquality.eq :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
   166   "OperationalEquality.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
   167   "OperationalEquality.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
   168 code_gen
   169   mystring
   170 code_gen
   171   f g h
   172 code_gen
   173   apply_tower Codegenerator.keywords shadow
   174 
   175 code_gen (SML -)
   176 
   177 end