# HG changeset patch # User haftmann # Date 1167242997 -3600 # Node ID d02ba728cd565b2c0e630b56b45907bd578d556c # Parent 51d8535dfec741dd3cffc2453335fb6bd34cfab2 moved code generator product setup here diff -r 51d8535dfec7 -r d02ba728cd56 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Wed Dec 27 19:09:56 2006 +0100 +++ b/src/HOL/Product_Type.thy Wed Dec 27 19:09:57 2006 +0100 @@ -773,27 +773,55 @@ subsection {* Code generator setup *} +lemmas [code func] = fst_conv snd_conv + instance unit :: eq .. lemma [code func]: "(u\unit) = v \ True" unfolding unit_eq [of u] unit_eq [of v] by rule+ +code_type unit + (SML "unit") + (OCaml "unit") + (Haskell "()") + code_instance unit :: eq (Haskell -) +code_const "op = \ unit \ unit \ bool" + (Haskell infixl 4 "==") + +code_const Unity + (SML "()") + (OCaml "()") + (Haskell "()") + +code_reserved SML + unit + +code_reserved OCaml + unit + instance * :: (eq, eq) eq .. lemma [code func]: "(x1\'a\eq, y1\'b\eq) = (x2, y2) \ x1 = x2 \ y1 = y2" by auto +code_type * + (SML infix 2 "*") + (OCaml infix 2 "*") + (Haskell "!((_),/ (_))") + code_instance * :: eq (Haskell -) -code_const "op = \ unit \ unit \ bool" +code_const "op = \ 'a\eq \ 'b\eq \ 'a \ 'b \ bool" (Haskell infixl 4 "==") -code_const "op = \ 'a\eq \ 'b\eq \ 'a \ 'b \ bool" - (Haskell infixl 4 "==") +code_const Pair + (SML "!((_),/ (_))") + (OCaml "!((_),/ (_))") + (Haskell "!((_),/ (_))") types_code "*" ("(_ */ _)") @@ -807,7 +835,9 @@ consts_code "Pair" ("(_,/ _)") -ML {* +setup {* + +let fun strip_abs_split 0 t = ([], t) | strip_abs_split i (Abs (s, T, t)) = @@ -870,18 +900,17 @@ | _ => NONE) | _ => NONE); -val prod_codegen_setup = +in + Codegen.add_codegen "let_codegen" let_codegen #> Codegen.add_codegen "split_codegen" split_codegen #> CodegenPackage.add_appconst ("Let", CodegenPackage.appgen_let) +end *} -setup prod_codegen_setup - -ML -{* +ML {* val Collect_split = thm "Collect_split"; val Compl_Times_UNIV1 = thm "Compl_Times_UNIV1"; val Compl_Times_UNIV2 = thm "Compl_Times_UNIV2";