(*  Title:      HOL/Code_Setup.thy

    ID:         $Id$

    Author:     Florian Haftmann

*)

header {* Setup of code generators and related tools *}

theory Code_Setup

imports HOL

begin

subsection {* Generic code generator foundation *}

text {* Datatypes *}

code_datatype True False

code_datatype "TYPE('a\<Colon>{})"

code_datatype Trueprop "prop"

text {* Code equations *}

lemma [code]:

  shows "False \<and> x \<longleftrightarrow> False"

    and "True \<and> x \<longleftrightarrow> x"

    and "x \<and> False \<longleftrightarrow> False"

    and "x \<and> True \<longleftrightarrow> x" by simp_all

lemma [code]:

  shows "False \<or> x \<longleftrightarrow> x"

    and "True \<or> x \<longleftrightarrow> True"

    and "x \<or> False \<longleftrightarrow> x"

    and "x \<or> True \<longleftrightarrow> True" by simp_all

lemma [code]:

  shows "\<not> True \<longleftrightarrow> False"

    and "\<not> False \<longleftrightarrow> True" by (rule HOL.simp_thms)+

lemmas [code] = Let_def if_True if_False

lemmas [code, code unfold, symmetric, code post] = imp_conv_disj

text {* Equality *}

context eq

begin

lemma equals_eq [code inline, code]: "op = \<equiv> eq"

  by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)

declare eq [code unfold, code inline del]

declare equals_eq [symmetric, code post]

end

declare simp_thms(6) [code nbe]

hide (open) const eq

hide const eq

setup {*

  Code_Unit.add_const_alias @{thm equals_eq}

*}

text {* Cases *}

lemma Let_case_cert:

  assumes "CASE \<equiv> (\<lambda>x. Let x f)"

  shows "CASE x \<equiv> f x"

  using assms by simp_all

lemma If_case_cert:

  includes meta_conjunction_syntax

  assumes "CASE \<equiv> (\<lambda>b. If b f g)"

  shows "(CASE True \<equiv> f) && (CASE False \<equiv> g)"

  using assms by simp_all

setup {*

  Code.add_case @{thm Let_case_cert}

  #> Code.add_case @{thm If_case_cert}

  #> Code.add_undefined @{const_name undefined}

*}

code_abort undefined

subsection {* Generic code generator preprocessor *}

setup {*

  Code.map_pre (K HOL_basic_ss)

  #> Code.map_post (K HOL_basic_ss)

*}

subsection {* Generic code generator target languages *}

text {* type bool *}

code_type bool

  (SML "bool")

  (OCaml "bool")

  (Haskell "Bool")

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 {* using built-in Haskell equality *}

code_class eq

  (Haskell "Eq" where "eq_class.eq" \<equiv> "(==)")

code_const "eq_class.eq"

  (Haskell infixl 4 "==")

code_const "op ="

  (Haskell infixl 4 "==")

text {* undefined *}

code_const undefined

  (SML "!(raise/ Fail/ \"undefined\")")

  (OCaml "failwith/ \"undefined\"")

  (Haskell "error/ \"undefined\"")

subsection {* SML code generator 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 =

  let val b = one_of [false, true]

  in (b, fn () => term_of_bool b) end;

*}

  "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 dep thyname b t gr =

    (case strip_comb t of

       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE

     | (Const ("op =", _), [t, u]) =>

          let

            val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;

            val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';

            val (_, gr''') = Codegen.invoke_tycodegen thy defs dep thyname false HOLogic.boolT gr'';

          in

            SOME (Codegen.parens

              (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')

          end

     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen

         thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)

     | _ => NONE);

in

  Codegen.add_codegen "eq_codegen" eq_codegen

end

*}

subsection {* Evaluation and normalization by evaluation *}

ML {*

structure Eval_Method =

struct

val eval_ref : (unit -> bool) option ref = ref NONE;

end;

*}

oracle eval_oracle = {* fn ct =>

  let

    val thy = Thm.theory_of_cterm ct;

    val t = Thm.term_of ct;

  in

    if Code_ML.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy

      (HOLogic.dest_Trueprop t) [] 

    then ct

    else @{cprop True} (*dummy*)

  end

*}

method_setup eval = {*

let

  fun eval_tac thy = 

    CSUBGOAL (fn (ct, i) => rtac (eval_oracle ct) i)

in 

  Method.ctxt_args (fn ctxt => 

    Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))

end

*} "solve goal by evaluation"

method_setup evaluation = {*

  Method.no_args (Method.SIMPLE_METHOD' (CONVERSION Codegen.evaluation_conv THEN' rtac TrueI))

*} "solve goal by evaluation"

method_setup normalization = {*

  Method.no_args (Method.SIMPLE_METHOD'

    (CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv)

    THEN' (fn k => TRY (rtac TrueI k))

  ))

*} "solve goal by normalization"

subsection {* Quickcheck *}

quickcheck_params [size = 5, iterations = 50]

end