src/HOL/Code_Generator.thy
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 21454 a1937c51ed88
child 21546 268b6bed0cc8
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
     1 (*  ID:         $Id$
     2     Author:     Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 header {* Setup of code generator tools *}
     6 
     7 theory Code_Generator
     8 imports HOL
     9 begin
    10 
    11 subsection {* ML code generator *}
    12 
    13 types_code
    14   "bool"  ("bool")
    15 attach (term_of) {*
    16 fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    17 *}
    18 attach (test) {*
    19 fun gen_bool i = one_of [false, true];
    20 *}
    21   "prop"  ("bool")
    22 attach (term_of) {*
    23 fun term_of_prop b =
    24   HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
    25 *}
    26 
    27 consts_code
    28   "Trueprop" ("(_)")
    29   "True"    ("true")
    30   "False"   ("false")
    31   "Not"     ("not")
    32   "op |"    ("(_ orelse/ _)")
    33   "op &"    ("(_ andalso/ _)")
    34   "HOL.If"      ("(if _/ then _/ else _)")
    35 
    36 setup {*
    37 let
    38 
    39 fun eq_codegen thy defs gr dep thyname b t =
    40     (case strip_comb t of
    41        (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
    42      | (Const ("op =", _), [t, u]) =>
    43           let
    44             val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
    45             val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u);
    46             val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
    47           in
    48             SOME (gr''', Codegen.parens
    49               (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
    50           end
    51      | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
    52          thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
    53      | _ => NONE);
    54 
    55 in
    56 
    57 Codegen.add_codegen "eq_codegen" eq_codegen
    58 
    59 end
    60 *}
    61 
    62 text {* Evaluation *}
    63 
    64 setup {*
    65 let
    66 
    67 fun evaluation_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
    68   (Drule.goals_conv (equal i) Codegen.evaluation_conv));
    69 
    70 val evaluation_meth =
    71   Method.no_args (Method.METHOD (fn _ => evaluation_tac 1 THEN rtac HOL.TrueI 1));
    72 
    73 in
    74 
    75 Method.add_method ("evaluation", evaluation_meth, "solve goal by evaluation")
    76 
    77 end;
    78 *}
    79 
    80 
    81 subsection {* Generic code generator setup *}
    82 
    83 text {* itself as a code generator datatype *}
    84 
    85 setup {*
    86 let fun add_itself thy =
    87   let
    88     val v = ("'a", []);
    89     val t = Logic.mk_type (TFree v);
    90     val Const (c, ty) = t;
    91     val (_, Type (dtco, _)) = strip_type ty;
    92   in
    93     thy
    94     |> CodegenData.add_datatype (dtco, (([v], [(c, [])]), CodegenData.lazy (fn () => [])))
    95   end
    96 in add_itself end;
    97 *} 
    98 
    99 
   100 text {* code generation for arbitrary as exception *}
   101 
   102 setup {*
   103   CodegenSerializer.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
   104 *}
   105 
   106 code_const arbitrary
   107   (Haskell "error/ \"arbitrary\"")
   108 
   109 code_reserved SML Fail
   110 code_reserved Haskell error
   111 
   112 
   113 subsection {* Evaluation oracle *}
   114 
   115 ML {*
   116 signature HOL_EVAL =
   117 sig
   118   val eval_ref: bool option ref
   119   val oracle: string * (theory * exn -> term)
   120   val tac: int -> tactic
   121   val method: Method.src -> Proof.context -> Method.method
   122 end;
   123 
   124 structure HOLEval : HOL_EVAL =
   125 struct
   126 
   127 val eval_ref : bool option ref = ref NONE;
   128 
   129 fun eval_prop thy t =
   130   CodegenPackage.eval_term
   131     thy (("HOLEval.eval_ref", eval_ref), t);
   132 
   133 exception Eval of term;
   134 
   135 val oracle = ("Eval", fn (thy, Eval t) =>
   136   Logic.mk_equals (t, if eval_prop thy t then HOLogic.true_const else HOLogic.false_const));
   137 
   138 val oracle_name = NameSpace.pack [Context.theory_name (the_context ()), fst oracle];
   139 
   140 fun conv ct =
   141   let
   142     val {thy, t, ...} = rep_cterm ct;
   143   in Thm.invoke_oracle_i thy oracle_name (thy, Eval t) end;
   144 
   145 fun tac i = Tactical.PRIMITIVE (Drule.fconv_rule
   146   (Drule.goals_conv (equal i) (HOL.Trueprop_conv conv)));
   147 
   148 val method =
   149   Method.no_args (Method.METHOD (fn _ =>
   150     tac 1 THEN rtac TrueI 1));
   151 
   152 end;
   153 *}
   154 
   155 setup {*
   156   Theory.add_oracle HOLEval.oracle
   157   #> Method.add_method ("eval", HOLEval.method, "solve goal by evaluation")
   158 *}
   159 
   160 
   161 subsection {* Normalization by evaluation *}
   162 
   163 setup {*
   164 let
   165   fun normalization_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
   166     (Drule.goals_conv (equal i) (HOL.Trueprop_conv
   167       NBE.normalization_conv)));
   168   val normalization_meth =
   169     Method.no_args (Method.METHOD (fn _ => normalization_tac 1 THEN resolve_tac [TrueI, refl] 1));
   170 in
   171   Method.add_method ("normalization", normalization_meth, "solve goal by normalization")
   172 end;
   173 *}
   174 
   175 text {* lazy @{const If} *}
   176 
   177 definition
   178   if_delayed :: "bool \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> (bool \<Rightarrow> 'a) \<Rightarrow> 'a" where
   179   "if_delayed b f g = (if b then f True else g False)"
   180 
   181 lemma [code func]:
   182   shows "if_delayed True f g = f True"
   183     and "if_delayed False f g = g False"
   184   unfolding if_delayed_def by simp_all
   185 
   186 lemma [normal pre, symmetric, normal post]:
   187   "(if b then x else y) = if_delayed b (\<lambda>_. x) (\<lambda>_. y)"
   188   unfolding if_delayed_def ..
   189 
   190 
   191 subsection {* Operational equality for code generation *}
   192 
   193 subsubsection {* eq class *}
   194 
   195 axclass eq \<subseteq> type
   196   attach "op ="
   197 
   198 
   199 subsubsection {* bool type *}
   200 
   201 instance bool :: eq ..
   202 
   203 lemma [code func]:
   204   "True = P \<longleftrightarrow> P" by simp
   205 
   206 lemma [code func]:
   207   "False = P \<longleftrightarrow> \<not> P" by simp
   208 
   209 lemma [code func]:
   210   "P = True \<longleftrightarrow> P" by simp
   211 
   212 lemma [code func]:
   213   "P = False \<longleftrightarrow> \<not> P" by simp
   214 
   215 
   216 subsubsection {* Haskell *}
   217 
   218 code_class eq
   219   (Haskell "Eq" where "op =" \<equiv> "(==)")
   220 
   221 code_const "op ="
   222   (Haskell infixl 4 "==")
   223 
   224 code_instance bool :: eq
   225   (Haskell -)
   226 
   227 code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
   228   (Haskell infixl 4 "==")
   229 
   230 code_reserved Haskell
   231   Eq eq
   232 
   233 
   234 hide (open) const if_delayed
   235 
   236 end