# HG changeset patch
# User haftmann
# Date 1187161331 -7200
# Node ID 066bb557570f9f23ad5da521eb2bd042dea16c7b
# Parent  f5afd33f5d02ad8628759a2a63de8582b1c35c06
added Code_Setup

diff -r f5afd33f5d02 -r 066bb557570f src/HOL/Code_Setup.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Code_Setup.thy	Wed Aug 15 09:02:11 2007 +0200
@@ -0,0 +1,164 @@
+(*  Title:      HOL/Code_Setup.thy
+    ID:         $Id$
+    Author:     Florian Haftmann
+*)
+
+header {* Setup of code generators and derived tools *}
+
+theory Code_Setup
+imports HOL
+uses "~~/src/HOL/Tools/recfun_codegen.ML"
+begin
+
+subsection {* SML code generator setup *}
+
+setup RecfunCodegen.setup
+
+types_code
+  "bool"  ("bool")
+attach (term_of) {*
+fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
+*}
+attach (test) {*
+fun gen_bool i = one_of [false, true];
+*}
+  "prop"  ("bool")
+attach (term_of) {*
+fun term_of_prop b =
+  HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
+*}
+
+consts_code
+  "Trueprop" ("(_)")
+  "True"    ("true")
+  "False"   ("false")
+  "Not"     ("Bool.not")
+  "op |"    ("(_ orelse/ _)")
+  "op &"    ("(_ andalso/ _)")
+  "If"      ("(if _/ then _/ else _)")
+
+setup {*
+let
+
+fun eq_codegen thy defs gr dep thyname b t =
+    (case strip_comb t of
+       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
+     | (Const ("op =", _), [t, u]) =>
+          let
+            val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
+            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u);
+            val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
+          in
+            SOME (gr''', Codegen.parens
+              (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
+          end
+     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
+         thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
+     | _ => NONE);
+
+in
+  Codegen.add_codegen "eq_codegen" eq_codegen
+end
+*}
+
+text {* Evaluation *}
+
+method_setup evaluation = {*
+  Method.no_args (Method.SIMPLE_METHOD' (CONVERSION Codegen.evaluation_conv THEN' rtac TrueI))
+*} "solve goal by evaluation"
+
+
+subsection {* Generic code generator setup *}
+
+
+text {* using built-in Haskell equality *}
+
+code_class eq
+  (Haskell "Eq" where "op =" \<equiv> "(==)")
+
+code_const "op ="
+  (Haskell infixl 4 "==")
+
+
+text {* type bool *}
+
+lemmas [code] = imp_conv_disj
+
+code_type bool
+  (SML "bool")
+  (OCaml "bool")
+  (Haskell "Bool")
+
+code_instance bool :: eq
+  (Haskell -)
+
+code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
+  (Haskell infixl 4 "==")
+
+code_const True and False and Not and "op &" and "op |" and If
+  (SML "true" and "false" and "not"
+    and infixl 1 "andalso" and infixl 0 "orelse"
+    and "!(if (_)/ then (_)/ else (_))")
+  (OCaml "true" and "false" and "not"
+    and infixl 4 "&&" and infixl 2 "||"
+    and "!(if (_)/ then (_)/ else (_))")
+  (Haskell "True" and "False" and "not"
+    and infixl 3 "&&" and infixl 2 "||"
+    and "!(if (_)/ then (_)/ else (_))")
+
+code_reserved SML
+  bool true false not
+
+code_reserved OCaml
+  bool not
+
+
+text {* code generation for undefined as exception *}
+
+code_const undefined
+  (SML "raise/ Fail/ \"undefined\"")
+  (OCaml "failwith/ \"undefined\"")
+  (Haskell "error/ \"undefined\"")
+
+
+text {* Let and If *}
+
+lemmas [code func] = Let_def if_True if_False
+
+setup {*
+  CodePackage.add_appconst (@{const_name Let}, CodePackage.appgen_let)
+  #> CodePackage.add_appconst (@{const_name If}, CodePackage.appgen_if)
+*}
+
+
+subsection {* Evaluation oracle *}
+
+oracle eval_oracle ("term") = {* fn thy => fn t => 
+  if CodePackage.satisfies thy (Thm.cterm_of thy (HOLogic.dest_Trueprop t)) [] 
+  then t
+  else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
+*}
+
+method_setup eval = {*
+let
+  fun eval_tac thy = 
+    SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i)
+in 
+  Method.ctxt_args (fn ctxt => 
+    Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
+end
+*} "solve goal by evaluation"
+
+
+subsection {* Normalization by evaluation *}
+
+setup Nbe.setup
+
+method_setup normalization = {*
+  Method.no_args (Method.SIMPLE_METHOD'
+    (CONVERSION (ObjectLogic.judgment_conv Nbe.normalization_conv)
+      THEN' resolve_tac [TrueI, refl]))
+*} "solve goal by normalization"
+
+
+end