--- a/NEWS Thu Aug 31 23:01:16 2006 +0200
+++ b/NEWS Fri Sep 01 08:36:51 2006 +0200
@@ -48,16 +48,45 @@
Haskell-like type classes in Isabelle. See HOL/ex/Classpackage.thy for examples.
* Yet another code generator framework allows to generate executable code
-for ML and Haskell (including "class"es). Most basic use cases:
+for ML and Haskell (including "class"es). A short usage sketch:
internal compilation:
- code_serialize ml <list of constants (term syntax)> (-)
- writing ML code to a file:
- code_serialize ml <list of constants (term syntax)> (<filename>)
+ code_gen <list of constants (term syntax)> (SML -)
+ writing SML code to a file:
+ code_gen <list of constants (term syntax)> (SML <filename>)
writing Haskell code to a bunch of files:
- code_serialize haskell <list of constants (term syntax)> (<filename>)
-
-See HOL/ex/Codegenerator.thy for examples.
+ code_gen <list of constants (term syntax)> (Haskell <filename>)
+
+Reasonable default setup of framework in HOL/Main.
+
+See HOL/ex/Code*.thy for examples.
+
+Theorem attributs for selecting and transforming function equations theorems:
+
+ [code fun]: select a theorem as function equation for a specific constant
+ [code nofun]: deselect a theorem as function equation for a specific constant
+ [code inline]: select an equation theorem for unfolding (inlining) in place
+ [code noinline]: deselect an equation theorem for unfolding (inlining) in place
+
+User-defined serializations (target in {SML, Haskell}):
+
+ code_const <and-list of constants (term syntax)>
+ {(target) <and-list of const target syntax>}+
+
+ code_type <and-list of type constructors>
+ {(target) <and-list of type target syntax>}+
+
+ code_instance <and-list of instances>
+ {(target)}+
+ where instance ::= <type constructor> :: <class>
+
+ code_class <and_list of classes>
+ {(target) <and-list of class target syntax>}+
+ where class target syntax ::= <class name> {where {<classop> == <target syntax>}+}?
+
+For code_instance and code_class, target SML is silently ignored.
+
+See HOL theories and HOL/ex/Code*.thy for usage examples.
* Command 'no_translations' removes translation rules from theory
syntax.
--- a/etc/isar-keywords-HOL-Nominal.el Thu Aug 31 23:01:16 2006 +0200
+++ b/etc/isar-keywords-HOL-Nominal.el Fri Sep 01 08:36:51 2006 +0200
@@ -43,8 +43,9 @@
"classrel"
"clear_undos"
"code_class"
- "code_constapp"
+ "code_const"
"code_constname"
+ "code_gen"
"code_generate"
"code_instance"
"code_library"
@@ -52,7 +53,7 @@
"code_purge"
"code_serialize"
"code_simtype"
- "code_typapp"
+ "code_type"
"code_typename"
"coinductive"
"commit"
@@ -368,15 +369,16 @@
"classes"
"classrel"
"code_class"
- "code_constapp"
+ "code_const"
"code_constname"
+ "code_gen"
"code_generate"
"code_instance"
"code_library"
"code_module"
"code_purge"
"code_serialize"
- "code_typapp"
+ "code_type"
"code_typename"
"coinductive"
"const_syntax"
--- a/etc/isar-keywords-ZF.el Thu Aug 31 23:01:16 2006 +0200
+++ b/etc/isar-keywords-ZF.el Fri Sep 01 08:36:51 2006 +0200
@@ -41,8 +41,9 @@
"clear_undos"
"codatatype"
"code_class"
- "code_constapp"
+ "code_const"
"code_constname"
+ "code_gen"
"code_generate"
"code_instance"
"code_library"
@@ -50,7 +51,7 @@
"code_purge"
"code_serialize"
"code_simtype"
- "code_typapp"
+ "code_type"
"code_typename"
"coinductive"
"commit"
@@ -354,15 +355,16 @@
"classrel"
"codatatype"
"code_class"
- "code_constapp"
+ "code_const"
"code_constname"
+ "code_gen"
"code_generate"
"code_instance"
"code_library"
"code_module"
"code_purge"
"code_serialize"
- "code_typapp"
+ "code_type"
"code_typename"
"coinductive"
"const_syntax"
--- a/etc/isar-keywords.el Thu Aug 31 23:01:16 2006 +0200
+++ b/etc/isar-keywords.el Fri Sep 01 08:36:51 2006 +0200
@@ -43,8 +43,9 @@
"classrel"
"clear_undos"
"code_class"
- "code_constapp"
+ "code_const"
"code_constname"
+ "code_gen"
"code_generate"
"code_instance"
"code_library"
@@ -52,7 +53,7 @@
"code_purge"
"code_serialize"
"code_simtype"
- "code_typapp"
+ "code_type"
"code_typename"
"coinductive"
"commit"
@@ -389,15 +390,16 @@
"classes"
"classrel"
"code_class"
- "code_constapp"
+ "code_const"
"code_constname"
+ "code_gen"
"code_generate"
"code_instance"
"code_library"
"code_module"
"code_purge"
"code_serialize"
- "code_typapp"
+ "code_type"
"code_typename"
"coinductive"
"const_syntax"
--- a/src/HOL/Datatype.thy Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/Datatype.thy Fri Sep 01 08:36:51 2006 +0200
@@ -261,61 +261,40 @@
"split = prod_case"
by (simp add: expand_fun_eq split_def prod.cases)
-code_typapp bool
- ml (target_atom "bool")
- haskell (target_atom "Bool")
+code_type bool
+ (SML target_atom "bool")
+ (Haskell target_atom "Bool")
-code_constapp
- True
- ml (target_atom "true")
- haskell (target_atom "True")
- False
- ml (target_atom "false")
- haskell (target_atom "False")
- Not
- ml (target_atom "not")
- haskell (target_atom "not")
- "op &"
- ml (infixl 1 "andalso")
- haskell (infixl 3 "&&")
- "op |"
- ml (infixl 0 "orelse")
- haskell (infixl 2 "||")
- If
- ml (target_atom "(if __/ then __/ else __)")
- haskell (target_atom "(if __/ then __/ else __)")
+code_const True and False and Not and "op &" and "op |" and If
+ (SML target_atom "true" and target_atom "false" and target_atom "not"
+ and infixl 1 "andalso" and infixl 0 "orelse"
+ and target_atom "(if __/ then __/ else __)")
+ (Haskell target_atom "True" and target_atom "False" and target_atom "not"
+ and infixl 3 "&&" and infixl 2 "||"
+ and target_atom "(if __/ then __/ else __)")
+
+code_type *
+ (SML infix 2 "*")
+ (Haskell target_atom "(__,/ __)")
-code_typapp
- *
- ml (infix 2 "*")
- haskell (target_atom "(__,/ __)")
+code_const Pair
+ (SML target_atom "(__,/ __)")
+ (Haskell target_atom "(__,/ __)")
-code_constapp
- Pair
- ml (target_atom "(__,/ __)")
- haskell (target_atom "(__,/ __)")
-
-code_typapp
- unit
- ml (target_atom "unit")
- haskell (target_atom "()")
+code_type unit
+ (SML target_atom "unit")
+ (Haskell target_atom "()")
-code_constapp
- Unity
- ml (target_atom "()")
- haskell (target_atom "()")
+code_const Unity
+ (SML target_atom "()")
+ (Haskell target_atom "()")
-code_typapp
- option
- ml ("_ option")
- haskell ("Maybe _")
+code_type option
+ (SML "_ option")
+ (Haskell "Maybe _")
-code_constapp
- None
- ml (target_atom "NONE")
- haskell (target_atom "Nothing")
- Some
- ml (target_atom "SOME")
- haskell (target_atom "Just")
+code_const None and Some
+ (SML target_atom "NONE" and target_atom "SOME")
+ (Haskell target_atom "Nothing" and target_atom "Just")
end
--- a/src/HOL/HOL.thy Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/HOL.thy Fri Sep 01 08:36:51 2006 +0200
@@ -1420,9 +1420,8 @@
CodegenTheorems.init_obj ((TrueI, FalseE), (conjI, thm "HOL.atomize_eq" |> Thm.symmetric))
*}
-code_constapp
- "op =" (* an intermediate solution for polymorphic equality *)
- ml (infixl 6 "=")
- haskell (infixl 4 "==")
+code_const "op =" (* an intermediate solution for polymorphic equality *)
+ (SML infixl 6 "=")
+ (Haskell infixl 4 "==")
end
--- a/src/HOL/Integ/IntDef.thy Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy Fri Sep 01 08:36:51 2006 +0200
@@ -902,26 +902,29 @@
"Orderings.less_eq" :: "int => int => bool" ("(_ <=/ _)")
"neg" ("(_ < 0)")
-code_typapp int
- ml (target_atom "IntInf.int")
- haskell (target_atom "Integer")
+code_type int
+ (SML target_atom "IntInf.int")
+ (Haskell target_atom "Integer")
+
+code_const "op + :: int \<Rightarrow> int \<Rightarrow> int"
+ (SML "IntInf.+ (_, _)")
+ (Haskell infixl 6 "+")
+
+code_const "op * :: int \<Rightarrow> int \<Rightarrow> int"
+ (SML "IntInf.* (_, _)")
+ (Haskell infixl 7 "*")
-code_constapp
- "op + :: int \<Rightarrow> int \<Rightarrow> int"
- ml ("IntInf.+ (_, _)")
- haskell (infixl 6 "+")
- "op * :: int \<Rightarrow> int \<Rightarrow> int"
- ml ("IntInf.* (_, _)")
- haskell (infixl 7 "*")
- "uminus :: int \<Rightarrow> int"
- ml (target_atom "IntInf.~")
- haskell (target_atom "negate")
- "op = :: int \<Rightarrow> int \<Rightarrow> bool"
- ml ("(op =) (_ : IntInf.int, _)")
- haskell (infixl 4 "==")
- "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
- ml ("IntInf.<= (_, _)")
- haskell (infix 4 "<=")
+code_const "uminus :: int \<Rightarrow> int"
+ (SML target_atom "IntInf.~")
+ (Haskell target_atom "negate")
+
+code_const "op = :: int \<Rightarrow> int \<Rightarrow> bool"
+ (SML "(op =) (_ : IntInf.int, _)")
+ (Haskell infixl 4 "==")
+
+code_const "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
+ (SML "IntInf.<= (_, _)")
+ (Haskell infix 4 "<=")
ML {*
fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of",
--- a/src/HOL/Lambda/WeakNorm.thy Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy Fri Sep 01 08:36:51 2006 +0200
@@ -501,9 +501,9 @@
arbitrary :: "'a" ("(error \"arbitrary\")")
arbitrary :: "'a \<Rightarrow> 'b" ("(fn '_ => error \"arbitrary\")")
-code_constapp
- "arbitrary :: 'a" ml (target_atom "(error \"arbitrary\")")
- "arbitrary :: 'a \<Rightarrow> 'b" ml (target_atom "(fn '_ => error \"arbitrary\")")
+code_const "arbitrary :: 'a" and "arbitrary :: 'a \<Rightarrow> 'b"
+ (SML target_atom "(error \"arbitrary\")"
+ and target_atom "(fn '_ => error \"arbitrary\")")
code_module Norm
contains
--- a/src/HOL/Library/EfficientNat.thy Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/Library/EfficientNat.thy Fri Sep 01 08:36:51 2006 +0200
@@ -61,23 +61,17 @@
"nat_less_equal m n = (int m <= int n)"
"nat_eq m n = (int m = int n)"
-code_typapp nat
- ml (target_atom "IntInf.int")
- haskell (target_atom "Integer")
+code_type nat
+ (SML target_atom "IntInf.int")
+ (Haskell target_atom "Integer")
-code_constapp
- "0::nat" (* all constructors of nat must be hidden *)
- ml (target_atom "(0 :: IntInf.int)")
- haskell (target_atom "0")
- Suc (* all constructors of nat must be hidden *)
- ml ("IntInf.+ (_, 1)")
- haskell ("(+) 1 _")
- nat
- ml (target_atom "(fn n : IntInf.int => if n < 0 then 0 else n)")
- haskell (target_atom "(\\n :: Int -> if n < 0 then 0 else n)")
- int
- ml ("_")
- haskell ("_")
+code_const "0::nat" and Suc (*all constructors of nat must be hidden*)
+ (SML target_atom "(0 :: IntInf.int)" and "IntInf.+ (_, 1)")
+ (Haskell target_atom "0" and "(+) 1 _")
+
+code_const nat and int
+ (SML target_atom "(fn n : IntInf.int => if n < 0 then 0 else n)" and "_")
+ (Haskell target_atom "(\\n :: Int -> if n < 0 then 0 else n)" and "_")
text {*
Eliminate @{const "0::nat"} and @{const "1::nat"}
--- a/src/HOL/Library/ExecutableRat.thy Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/Library/ExecutableRat.thy Fri Sep 01 08:36:51 2006 +0200
@@ -81,11 +81,12 @@
types_code
rat ("{*erat*}")
-code_generate (ml, haskell) Rat
+code_gen Rat
+ (SML) (Haskell)
-code_typapp rat
- ml ("{*erat*}")
- haskell ("{*erat*}")
+code_type rat
+ (SML "{*erat*}")
+ (Haskell "{*erat*}")
section {* const serializations *}
@@ -103,12 +104,11 @@
Orderings.less_eq :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
"op =" :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("{*eq_rat*}")
-code_constapp
- "arbitrary :: erat"
- ml ("raise/ (Fail/ \"non-defined rational number\")")
- haskell ("error/ \"non-defined rational number\"")
+code_const "arbitrary :: erat"
+ (SML "raise/ (Fail/ \"non-defined rational number\")")
+ (Haskell "error/ \"non-defined rational number\"")
-code_generate (ml, haskell)
+code_gen
of_quotient
"0::erat"
"1::erat"
@@ -118,37 +118,46 @@
"inverse :: erat \<Rightarrow> erat"
"op <= :: erat \<Rightarrow> erat \<Rightarrow> bool"
eq_rat
+ (SML) (Haskell)
-code_constapp
- Fract
- ml ("{*of_quotient*}")
- haskell ("{*of_quotient*}")
- "0 :: rat"
- ml ("{*0::erat*}")
- haskell ("{*1::erat*}")
- "1 :: rat"
- ml ("{*1::erat*}")
- haskell ("{*1::erat*}")
- "op + :: rat \<Rightarrow> rat \<Rightarrow> rat"
- ml ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
- haskell ("{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
- "uminus :: rat \<Rightarrow> rat"
- ml ("{*uminus :: erat \<Rightarrow> erat*}")
- haskell ("{*uminus :: erat \<Rightarrow> erat*}")
- "op * :: rat \<Rightarrow> rat \<Rightarrow> rat"
- ml ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
- haskell ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
- "inverse :: rat \<Rightarrow> rat"
- ml ("{*inverse :: erat \<Rightarrow> erat*}")
- haskell ("{*inverse :: erat \<Rightarrow> erat*}")
- "divide :: rat \<Rightarrow> rat \<Rightarrow> rat"
- ml ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)")
- haskell ("{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)")
- "op <= :: rat \<Rightarrow> rat \<Rightarrow> bool"
- ml ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
- haskell ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
- "op = :: rat \<Rightarrow> rat \<Rightarrow> bool"
- ml ("{*eq_rat*}")
- haskell ("{*eq_rat*}")
+code_const Fract
+ (SML "{*of_quotient*}")
+ (Haskell "{*of_quotient*}")
+
+code_const "0 :: rat"
+ (SML "{*0::erat*}")
+ (Haskell "{*1::erat*}")
+
+code_const "1 :: rat"
+ (SML "{*1::erat*}")
+ (Haskell "{*1::erat*}")
+
+code_const "op + :: rat \<Rightarrow> rat \<Rightarrow> rat"
+ (SML "{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
+ (Haskell "{*op + :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
+
+code_const "uminus :: rat \<Rightarrow> rat"
+ (SML "{*uminus :: erat \<Rightarrow> erat*}")
+ (Haskell "{*uminus :: erat \<Rightarrow> erat*}")
+
+code_const "op * :: rat \<Rightarrow> rat \<Rightarrow> rat"
+ (SML "{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
+ (Haskell "{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}")
+
+code_const "inverse :: rat \<Rightarrow> rat"
+ (SML "{*inverse :: erat \<Rightarrow> erat*}")
+ (Haskell "{*inverse :: erat \<Rightarrow> erat*}")
+
+code_const "divide :: rat \<Rightarrow> rat \<Rightarrow> rat"
+ (SML "{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)")
+ (Haskell "{*op * :: erat \<Rightarrow> erat \<Rightarrow> erat*}/ _/ ({*inverse :: erat \<Rightarrow> erat*}/ _)")
+
+code_const "op <= :: rat \<Rightarrow> rat \<Rightarrow> bool"
+ (SML "{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
+ (Haskell "{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
+
+code_const "op = :: rat \<Rightarrow> rat \<Rightarrow> bool"
+ (SML "{*eq_rat*}")
+ (Haskell "{*eq_rat*}")
end
--- a/src/HOL/Library/ExecutableSet.thy Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/Library/ExecutableSet.thy Fri Sep 01 08:36:51 2006 +0200
@@ -234,9 +234,9 @@
and gen_set aG i = gen_set' aG i i;
*}
-code_typapp set
- ml ("_ list")
- haskell (target_atom "[_]")
+code_type set
+ (SML "_ list")
+ (Haskell target_atom "[_]")
subsection {* const serializations *}
@@ -261,46 +261,57 @@
"ExecutableSet.insertl" "List.insertl"
"ExecutableSet.drop_first" "List.drop_first"
-code_generate (ml, haskell)
+code_gen
insertl unionl intersect flip subtract map_distinct
unions intersects map_union map_inter Blall Blex
+ (SML) (Haskell)
-code_constapp
- "{}"
- ml (target_atom "[]")
- haskell (target_atom "[]")
- insert
- ml ("{*insertl*}")
- haskell ("{*insertl*}")
- "op \<union>"
- ml ("{*unionl*}")
- haskell ("{*unionl*}")
- "op \<inter>"
- ml ("{*intersect*}")
- haskell ("{*intersect*}")
- "op - :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
- ml ("{*flip subtract*}")
- haskell ("{*flip subtract*}")
- image
- ml ("{*map_distinct*}")
- haskell ("{*map_distinct*}")
- "Union"
- ml ("{*unions*}")
- haskell ("{*unions*}")
- "Inter"
- ml ("{*intersects*}")
- haskell ("{*intersects*}")
- UNION
- ml ("{*map_union*}")
- haskell ("{*map_union*}")
- INTER
- ml ("{*map_inter*}")
- haskell ("{*map_inter*}")
- Ball
- ml ("{*Blall*}")
- haskell ("{*Blall*}")
- Bex
- ml ("{*Blex*}")
- haskell ("{*Blex*}")
+code_const "{}"
+ (SML target_atom "[]")
+ (Haskell target_atom "[]")
+
+code_const insert
+ (SML "{*insertl*}")
+ (Haskell "{*insertl*}")
+
+code_const "op \<union>"
+ (SML "{*unionl*}")
+ (Haskell "{*unionl*}")
+
+code_const "op \<inter>"
+ (SML "{*intersect*}")
+ (Haskell "{*intersect*}")
+
+code_const "op - :: 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+ (SML "{*flip subtract*}")
+ (Haskell "{*flip subtract*}")
+
+code_const image
+ (SML "{*map_distinct*}")
+ (Haskell "{*map_distinct*}")
+
+code_const "Union"
+ (SML "{*unions*}")
+ (Haskell "{*unions*}")
+
+code_const "Inter"
+ (SML "{*intersects*}")
+ (Haskell "{*intersects*}")
+
+code_const UNION
+ (SML "{*map_union*}")
+ (Haskell "{*map_union*}")
+
+code_const INTER
+ (SML "{*map_inter*}")
+ (Haskell "{*map_inter*}")
+
+code_const Ball
+ (SML "{*Blall*}")
+ (Haskell "{*Blall*}")
+
+code_const Bex
+ (SML "{*Blex*}")
+ (Haskell "{*Blex*}")
end
--- a/src/HOL/Library/MLString.thy Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/Library/MLString.thy Fri Sep 01 08:36:51 2006 +0200
@@ -5,7 +5,7 @@
header {* Monolithic strings for ML *}
theory MLString
-imports Main
+imports List
begin
section {* Monolithic strings for ML *}
@@ -58,31 +58,20 @@
subsection {* Code serialization *}
-code_typapp ml_string
- ml (target_atom "string")
- haskell (target_atom "String")
+code_type ml_string
+ (SML target_atom "string")
+ (Haskell target_atom "String")
-code_constapp STR
- haskell ("_")
+code_const STR
+ (Haskell "_")
setup {*
-let
- fun print_char c =
- let
- val i = ord c
- in if i < 32
- then prefix "\\" (string_of_int i)
- else c
- end;
- val print_string = quote;
-in
- CodegenPackage.add_pretty_ml_string "ml" "List.list.Nil" "List.list.Cons" "MLString.ml_string.STR"
- print_char print_string "String.implode"
-end
+ CodegenPackage.add_pretty_ml_string "SML" "List.list.Nil" "List.list.Cons" "MLString.ml_string.STR"
+ HOList.print_char HOList.print_string "String.implode"
*}
-code_constapp explode
- ml (target_atom "String.explode")
- haskell ("_")
+code_const explode
+ (SML target_atom "String.explode")
+ (Haskell "_")
-end
\ No newline at end of file
+end
--- a/src/HOL/List.thy Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/List.thy Fri Sep 01 08:36:51 2006 +0200
@@ -2650,6 +2650,28 @@
fun nibble_of_int i =
if i <= 9 then chr (ord "0" + i) else chr (ord "A" + i - 10);
+fun dest_char (Const ("List.char.Char", _) $ c1 $ c2) =
+ let
+ fun dest_nibble (Const (s, _)) = (int_of_nibble o unprefix "List.nibble.Nibble") s
+ | dest_nibble _ = raise Match;
+ in
+ (SOME (dest_nibble c1 * 16 + dest_nibble c2)
+ handle Fail _ => NONE | Match => NONE)
+ end
+ | dest_char _ = NONE;
+
+val print_list = Pretty.enum "," "[" "]";
+
+fun print_char c =
+ let
+ val i = ord c
+ in if i < 32
+ then prefix "\\" (string_of_int i)
+ else c
+ end;
+
+val print_string = quote;
+
fun term_string s =
let
val ty_n = Type ("List.nibble", []);
@@ -2693,61 +2715,9 @@
in [("Char", char_ast_tr'), ("@list", list_ast_tr')] end;
*}
+
subsubsection {* Code generator setup *}
-ML {*
-local
-
-fun list_codegen thy defs gr dep thyname b t =
- let val (gr', ps) = foldl_map (Codegen.invoke_codegen thy defs dep thyname false)
- (gr, HOLogic.dest_list t)
- in SOME (gr', Pretty.list "[" "]" ps) end handle TERM _ => NONE;
-
-fun dest_char (Const ("List.char.Char", _) $ c1 $ c2) =
- let
- fun dest_nibble (Const (s, _)) = (HOList.int_of_nibble o unprefix "List.nibble.Nibble") s
- | dest_nibble _ = raise Match;
- in
- (SOME (dest_nibble c1 * 16 + dest_nibble c2)
- handle Fail _ => NONE | Match => NONE)
- end
- | dest_char _ = NONE;
-
-fun char_codegen thy defs gr dep thyname b t =
- case (Option.map chr o dest_char) t
- of SOME c =>
- if Symbol.is_printable c
- then SOME (gr, (Pretty.quote o Pretty.str) c)
- else NONE
- | NONE => NONE;
-
-val print_list = Pretty.enum "," "[" "]";
-
-fun print_char c =
- let
- val i = ord c
- in if i < 32
- then prefix "\\" (string_of_int i)
- else c
- end;
-
-val print_string = quote;
-
-in
-
-val list_codegen_setup =
- Codegen.add_codegen "list_codegen" list_codegen
- #> Codegen.add_codegen "char_codegen" char_codegen
- #> CodegenPackage.add_pretty_list "ml" "List.list.Nil" "List.list.Cons"
- print_list NONE (7, "::")
- #> CodegenPackage.add_pretty_list "haskell" "List.list.Nil" "List.list.Cons"
- print_list (SOME (print_char, print_string)) (5, ":")
- #> CodegenPackage.add_appconst
- ("List.char.Char", CodegenPackage.appgen_char dest_char);
-
-end;
-*}
-
types_code
"list" ("_ list")
attach (term_of) {*
@@ -2773,26 +2743,50 @@
consts_code "Cons" ("(_ ::/ _)")
-code_typapp
- list
- ml ("_ list")
- haskell (target_atom "[_]")
-
-code_constapp
- Nil
- ml (target_atom "[]")
- haskell (target_atom "[]")
-
-code_typapp
- char
- ml (target_atom "char")
- haskell (target_atom "Char")
-
-code_constapp
- Char
- ml (target_atom "(__,/ __)")
- haskell (target_atom "(__,/ __)")
-
-setup list_codegen_setup
+code_type list
+ (SML "_ list")
+ (Haskell target_atom "[_]")
+
+code_const Nil
+ (SML target_atom "[]")
+ (Haskell target_atom "[]")
+
+code_type char
+ (SML target_atom "char")
+ (Haskell target_atom "Char")
+
+code_const Char
+ (SML target_atom "(__,/ __)")
+ (Haskell target_atom "(__,/ __)")
+
+setup {*
+let
+
+fun list_codegen thy defs gr dep thyname b t =
+ let val (gr', ps) = foldl_map (Codegen.invoke_codegen thy defs dep thyname false)
+ (gr, HOLogic.dest_list t)
+ in SOME (gr', Pretty.list "[" "]" ps) end handle TERM _ => NONE;
+
+fun char_codegen thy defs gr dep thyname b t =
+ case (Option.map chr o HOList.dest_char) t
+ of SOME c =>
+ if Symbol.is_printable c
+ then SOME (gr, (Pretty.quote o Pretty.str) c)
+ else NONE
+ | NONE => NONE;
+
+in
+
+ Codegen.add_codegen "list_codegen" list_codegen
+ #> Codegen.add_codegen "char_codegen" char_codegen
+ #> CodegenPackage.add_pretty_list "SML" "List.list.Nil" "List.list.Cons"
+ HOList.print_list NONE (7, "::")
+ #> CodegenPackage.add_pretty_list "Haskell" "List.list.Nil" "List.list.Cons"
+ HOList.print_list (SOME (HOList.print_char, HOList.print_string)) (5, ":")
+ #> CodegenPackage.add_appconst
+ ("List.char.Char", CodegenPackage.appgen_char HOList.dest_char)
+
+end;
+*}
end
--- a/src/HOL/Wellfounded_Recursion.thy Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/Wellfounded_Recursion.thy Fri Sep 01 08:36:51 2006 +0200
@@ -295,10 +295,9 @@
CodegenPackage.add_appconst ("Wellfounded_Recursion.wfrec", CodegenPackage.appgen_wfrec)
*}
-code_constapp
- wfrec
- ml (target_atom "(let fun wfrec f x = f (wfrec f) x in wfrec end)")
- haskell (target_atom "(let wfrec f x = f (wfrec f) x in wfrec)")
+code_const wfrec
+ (SML target_atom "(let fun wfrec f x = f (wfrec f) x in wfrec end)")
+ (Haskell target_atom "(let wfrec f x = f (wfrec f) x in wfrec)")
subsection{*Variants for TFL: the Recdef Package*}
--- a/src/HOL/ex/Classpackage.thy Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/ex/Classpackage.thy Fri Sep 01 08:36:51 2006 +0200
@@ -319,10 +319,10 @@
"x2 = X (1::int) 2 3"
"y2 = Y (1::int) 2 3"
-code_generate "op \<otimes>" \<one> inv
-code_generate (ml, haskell) X Y
-code_generate (ml, haskell) x1 x2 y2
+code_gen "op \<otimes>" \<one> inv
+code_gen X Y (SML) (Haskell)
+code_gen x1 x2 y2 (SML) (Haskell)
-code_serialize ml (-)
+code_gen (SML -)
end
--- a/src/HOL/ex/CodeCollections.thy Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/ex/CodeCollections.thy Fri Sep 01 08:36:51 2006 +0200
@@ -402,16 +402,16 @@
"test1 = sum [None, Some True, None, Some False]"
"test2 = (inf :: nat \<times> unit)"
-code_generate eq
-code_generate "op <<="
-code_generate "op <<"
-code_generate inf
-code_generate between
-code_generate index
-code_generate sum
-code_generate test1
-code_generate test2
+code_gen eq
+code_gen "op <<="
+code_gen "op <<"
+code_gen inf
+code_gen between
+code_gen index
+code_gen sum
+code_gen test1
+code_gen test2
-code_serialize ml (-)
+code_gen (SML -)
end
\ No newline at end of file
--- a/src/HOL/ex/CodeEmbed.thy Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/ex/CodeEmbed.thy Fri Sep 01 08:36:51 2006 +0200
@@ -77,15 +77,12 @@
subsection {* Code serialization setup *}
-code_typapp
- "typ" ml (target_atom "Term.typ")
- "term" ml (target_atom "Term.term")
+code_type "typ" and "term"
+ (SML target_atom "Term.typ" and target_atom "Term.term")
-code_constapp
- Type ml ("Term.Type (_, _)")
- TFix ml ("Term.TFree (_, _)")
- Const ml ("Term.Const (_, _)")
- App ml ("Term.$ (_, _)")
- Fix ml ("Term.Free (_, _)")
+code_const Type and TFix
+ and Const and App and Fix
+ (SML "Term.Type (_, _)" and "Term.TFree (_, _)"
+ and "Term.Const (_, _)" and "Term.$ (_, _)" and "Term.Free (_, _)")
end
\ No newline at end of file
--- a/src/HOL/ex/CodeEval.thy Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/ex/CodeEval.thy Fri Sep 01 08:36:51 2006 +0200
@@ -194,7 +194,7 @@
and ('a, 'b) cair =
Cair 'a 'b
-code_generate term_of
+code_gen term_of
ML {* Eval.term "Shift (Cair (4::nat) [Suc 0])" *}
--- a/src/HOL/ex/CodeOperationalEquality.thy Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/ex/CodeOperationalEquality.thy Fri Sep 01 08:36:51 2006 +0200
@@ -117,9 +117,9 @@
"eq k l = eq_integer k l"
unfolding eq_integer_def eq_def ..
-code_constapp eq_integer
- ml (infixl 6 "=")
- haskell (infixl 4 "==")
+code_const eq_integer
+ (SML infixl 6 "=")
+ (Haskell infixl 4 "==")
subsection {* codegenerator setup *}
@@ -134,33 +134,34 @@
subsection {* haskell setup *}
code_class eq
- haskell "Eq" (eq "(==)")
+ (Haskell "Eq" where eq \<equiv> "(==)")
+
+code_instance eq :: bool and eq :: unit and eq :: *
+ and eq :: option and eq :: list and eq :: char and eq :: int
+ (Haskell - and - and - and - and - and - and -)
-code_instance
- (eq :: bool) haskell
- (eq :: unit) haskell
- (eq :: *) haskell
- (eq :: option) haskell
- (eq :: list) haskell
- (eq :: char) haskell
- (eq :: int) haskell
+code_const "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
+ (Haskell infixl 4 "==")
+
+code_const "eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
+ (Haskell infixl 4 "==")
+
+code_const "eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
+ (Haskell infixl 4 "==")
-code_constapp
- "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
- haskell (infixl 4 "==")
- "eq \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
- haskell (infixl 4 "==")
- "eq \<Colon> 'a\<Colon>eq \<times> 'b\<Colon>eq \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
- haskell (infixl 4 "==")
- "eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
- haskell (infixl 4 "==")
- "eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
- haskell (infixl 4 "==")
- "eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
- haskell (infixl 4 "==")
- "eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
- haskell (infixl 4 "==")
- "eq"
- haskell (infixl 4 "==")
+code_const "eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
+ (Haskell infixl 4 "==")
+
+code_const "eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
+ (Haskell infixl 4 "==")
+
+code_const "eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+ (Haskell infixl 4 "==")
+
+code_const "eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
+ (Haskell infixl 4 "==")
+
+code_const "eq"
+ (Haskell infixl 4 "==")
end
\ No newline at end of file
--- a/src/HOL/ex/CodeRandom.thy Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/ex/CodeRandom.thy Fri Sep 01 08:36:51 2006 +0200
@@ -167,12 +167,13 @@
end;
*}
-code_typapp randseed
- ml (target_atom "Random.seed")
+code_type randseed
+ (SML target_atom "Random.seed")
-code_constapp random_int
- ml (target_atom "Random.value")
+code_const random_int
+ (SML target_atom "Random.value")
-code_serialize ml select select_weight (-)
+code_gen select select_weight
+ (SML -)
end
\ No newline at end of file
--- a/src/HOL/ex/Codegenerator.thy Thu Aug 31 23:01:16 2006 +0200
+++ b/src/HOL/ex/Codegenerator.thy Fri Sep 01 08:36:51 2006 +0200
@@ -90,21 +90,19 @@
g "Mymod.A.f"
h "Mymod.A.B.f"
-code_generate (ml, haskell)
- n one "0::int" "0::nat" "1::int" "1::nat"
-code_generate (ml, haskell)
- fac
-code_generate
- xor
-code_generate
+code_gen xor
+code_gen one "0::nat" "1::nat"
+code_gen "0::int" "1::int" n fac
+ (SML) (Haskell)
+code_gen
"op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
"op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
"op * :: nat \<Rightarrow> nat \<Rightarrow> nat"
"op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
"op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
-code_generate
+code_gen
Pair fst snd Let split swap swapp appl
-code_generate (ml, haskell)
+code_gen
k
"op + :: int \<Rightarrow> int \<Rightarrow> int"
"op - :: int \<Rightarrow> int \<Rightarrow> int"
@@ -114,15 +112,16 @@
fac
"op div :: int \<Rightarrow> int \<Rightarrow> int"
"op mod :: int \<Rightarrow> int \<Rightarrow> int"
-code_generate
+ (SML) (Haskell)
+code_gen
Inl Inr
-code_generate
+code_gen
None Some
-code_generate
+code_gen
hd tl "op @" ps qs
-code_generate
+code_gen
mut1 mut2
-code_generate (ml, haskell)
+code_gen
"op @" filter concat foldl foldr hd tl
last butlast list_all2
map
@@ -143,9 +142,10 @@
rotate1
rotate
splice
-code_generate
+ (SML) (Haskell)
+code_gen
foo1 foo3
-code_generate (ml, haskell)
+code_gen
"op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
"op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
"op = :: int \<Rightarrow> int \<Rightarrow> bool"
@@ -156,9 +156,9 @@
"op = :: point \<Rightarrow> point \<Rightarrow> bool"
"op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
"op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
-code_generate
+code_gen
f g h
-code_serialize ml (-)
+code_gen (SML -)
end
\ No newline at end of file