added reserved words for Haskell
authorhaftmann
Fri Oct 20 17:07:27 2006 +0200 (2006-10-20)
changeset 21079747d716e98d0
parent 21078 101aefd61aac
child 21080 7d73aa966207
added reserved words for Haskell
src/HOL/Code_Generator.thy
src/HOL/Datatype.thy
src/HOL/Integ/IntDef.thy
src/HOL/Library/MLString.thy
src/HOL/List.thy
src/HOL/ex/CodeEmbed.thy
     1.1 --- a/src/HOL/Code_Generator.thy	Fri Oct 20 17:07:26 2006 +0200
     1.2 +++ b/src/HOL/Code_Generator.thy	Fri Oct 20 17:07:27 2006 +0200
     1.3 @@ -106,6 +106,8 @@
     1.4  code_const arbitrary
     1.5    (Haskell target_atom "(error \"arbitrary\")")
     1.6  
     1.7 +code_reserved SML Fail
     1.8 +code_reserved Haskell error
     1.9  
    1.10  subsection {* Operational equality for code generation *}
    1.11  
    1.12 @@ -169,6 +171,8 @@
    1.13  code_const "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
    1.14    (Haskell infixl 4 "==")
    1.15  
    1.16 +code_reserved Haskell
    1.17 +  Eq eq
    1.18  
    1.19  subsection {* normalization by evaluation *}
    1.20  
     2.1 --- a/src/HOL/Datatype.thy	Fri Oct 20 17:07:26 2006 +0200
     2.2 +++ b/src/HOL/Datatype.thy	Fri Oct 20 17:07:27 2006 +0200
     2.3 @@ -807,6 +807,12 @@
     2.4  code_const "Code_Generator.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
     2.5    (Haskell infixl 4 "==")
     2.6  
     2.7 +code_reserved SML
     2.8 +  bool true false not unit option NONE SOME
     2.9 +
    2.10 +code_reserved Haskell
    2.11 +  Bool True False not Maybe Nothing Just
    2.12 +
    2.13  ML
    2.14  {*
    2.15  val apfst_conv = thm "apfst_conv";
     3.1 --- a/src/HOL/Integ/IntDef.thy	Fri Oct 20 17:07:26 2006 +0200
     3.2 +++ b/src/HOL/Integ/IntDef.thy	Fri Oct 20 17:07:27 2006 +0200
     3.3 @@ -943,6 +943,9 @@
     3.4    (SML target_atom "IntInf.~")
     3.5    (Haskell target_atom "negate")
     3.6  
     3.7 +code_reserved SML IntInf
     3.8 +code_reserved Haskell Integer negate
     3.9 +
    3.10  ML {*
    3.11  fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of",
    3.12        Type ("fun", [_, T as Type ("IntDef.int", [])])) $ bin) =
     4.1 --- a/src/HOL/Library/MLString.thy	Fri Oct 20 17:07:26 2006 +0200
     4.2 +++ b/src/HOL/Library/MLString.thy	Fri Oct 20 17:07:27 2006 +0200
     4.3 @@ -74,4 +74,7 @@
     4.4    (SML target_atom "String.explode")
     4.5    (Haskell "_")
     4.6  
     4.7 +code_reserved SML string explode
     4.8 +code_reserved Haskell string
     4.9 +
    4.10  end
     5.1 --- a/src/HOL/List.thy	Fri Oct 20 17:07:26 2006 +0200
     5.2 +++ b/src/HOL/List.thy	Fri Oct 20 17:07:27 2006 +0200
     5.3 @@ -2648,6 +2648,12 @@
     5.4  code_const "Code_Generator.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
     5.5    (Haskell infixl 4 "==")
     5.6  
     5.7 +code_reserved SML
     5.8 +  list char
     5.9 +
    5.10 +code_reserved Haskell
    5.11 +  Char
    5.12 +
    5.13  setup {*
    5.14  let
    5.15  
    5.16 @@ -2682,7 +2688,7 @@
    5.17  subsubsection {* Generation of efficient code *}
    5.18  
    5.19  consts
    5.20 -  mem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl 55)
    5.21 +  memberl :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55)
    5.22    null:: "'a list \<Rightarrow> bool"
    5.23    list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
    5.24    list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
    5.25 @@ -2693,7 +2699,7 @@
    5.26  
    5.27  primrec
    5.28    "x mem [] = False"
    5.29 -  "x mem (y#ys) = (if y = x then True else x mem ys)"
    5.30 +  "x mem (y#ys) = (x = y \<or> x mem ys)"
    5.31  
    5.32  primrec
    5.33    "null [] = True"
     6.1 --- a/src/HOL/ex/CodeEmbed.thy	Fri Oct 20 17:07:26 2006 +0200
     6.2 +++ b/src/HOL/ex/CodeEmbed.thy	Fri Oct 20 17:07:27 2006 +0200
     6.3 @@ -85,4 +85,6 @@
     6.4    (SML "Term.Type (_, _)" and "Term.TFree (_, _)"
     6.5      and "Term.Const (_, _)" and "Term.$ (_, _)" and "Term.Free (_, _)")
     6.6  
     6.7 +code_reserved SML Term
     6.8 +
     6.9  end
    6.10 \ No newline at end of file