src/HOL/Code_Setup.thy

make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules

(*  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 "(True \<Longrightarrow> PROP P) \<equiv> PROP P" 
    and "(False \<Longrightarrow> Q) \<equiv> Trueprop True" 
    and "(PROP P \<Longrightarrow> True) \<equiv> Trueprop True" 
    and "(Q \<Longrightarrow> False) \<equiv> Trueprop (\<not> Q)" by (auto intro!: equal_intr_rule)

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:
  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")

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 *}

setup {*
  Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of)
*}

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;
    val dummy = @{cprop True};
  in case try HOLogic.dest_Trueprop t
   of SOME t' => if Code_ML.eval_term
         ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy t' [] 
       then Thm.capply (Thm.capply @{cterm "op \<equiv> \<Colon> prop \<Rightarrow> prop \<Rightarrow> prop"} ct) dummy
       else dummy
    | NONE => dummy
  end
*}

ML {*
fun gen_eval_method conv = Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD'
  (CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
    THEN' rtac TrueI))
*}

method_setup eval = {* gen_eval_method eval_oracle *}
  "solve goal by evaluation"

method_setup evaluation = {* gen_eval_method Codegen.evaluation_conv *}
  "solve goal by evaluation"

method_setup normalization = {* (Method.no_args o Method.SIMPLE_METHOD')
  (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))
*} "solve goal by normalization"


subsection {* Quickcheck *}

setup {*
  Quickcheck.add_generator ("SML", Codegen.test_term)
*}

quickcheck_params [size = 5, iterations = 50]

end