src/HOL/ex/Codegenerator.thy
changeset 20702 8b79d853eabb
parent 20597 65fe827aa595
child 20713 823967ef47f1
     1.1 --- a/src/HOL/ex/Codegenerator.thy	Mon Sep 25 17:04:18 2006 +0200
     1.2 +++ b/src/HOL/ex/Codegenerator.thy	Mon Sep 25 17:04:19 2006 +0200
     1.3 @@ -73,6 +73,11 @@
     1.4  
     1.5  subsection {* equalities *}
     1.6  
     1.7 +subsection {* strings *}
     1.8 +
     1.9 +definition
    1.10 +  "mystring = ''my home is my castle''"
    1.11 +
    1.12  subsection {* heavy usage of names *}
    1.13  
    1.14  definition
    1.15 @@ -88,16 +93,28 @@
    1.16    g "Mymod.A.f"
    1.17    h "Mymod.A.B.f"
    1.18  
    1.19 +definition
    1.20 +  "apply_tower = (\<lambda>x. x (\<lambda>x. x (\<lambda>x. x)))"
    1.21 +
    1.22 +definition
    1.23 +  "keywords fun datatype class instance funa classa =
    1.24 +    Suc fun + datatype * class mod instance - funa - classa"
    1.25 +
    1.26 +hide (open) const keywords
    1.27 +
    1.28 +definition
    1.29 +  "shadow keywords = keywords @ [Codegenerator.keywords 0 0 0 0 0 0]"
    1.30 +
    1.31  code_gen xor
    1.32  code_gen one
    1.33 +code_gen
    1.34 +  Pair fst snd Let split swap
    1.35  code_gen "0::int" "1::int"
    1.36    (SML) (Haskell)
    1.37  code_gen n
    1.38    (SML) (Haskell)
    1.39  code_gen fac
    1.40    (SML) (Haskell)
    1.41 -code_gen n
    1.42 -  (SML) (Haskell)
    1.43  code_gen
    1.44    "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.45    "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
    1.46 @@ -105,8 +122,6 @@
    1.47    "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
    1.48    "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
    1.49  code_gen
    1.50 -  Pair fst snd Let split swap
    1.51 -code_gen
    1.52    appl
    1.53  code_gen
    1.54    k
    1.55 @@ -151,8 +166,12 @@
    1.56    "OperationalEquality.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
    1.57    "OperationalEquality.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
    1.58  code_gen
    1.59 +  mystring
    1.60 +code_gen
    1.61    f g h
    1.62 +code_gen
    1.63 +  apply_tower Codegenerator.keywords shadow
    1.64  
    1.65 -code_gen (SML -) (SML _)
    1.66 +code_gen (SML -)
    1.67  
    1.68  end
    1.69 \ No newline at end of file