added Code_Setup
authorhaftmann
Wed Aug 15 09:02:11 2007 +0200 (2007-08-15)
changeset 24285066bb557570f
parent 24284 f5afd33f5d02
child 24286 7619080e49f0
added Code_Setup
src/HOL/Code_Setup.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Code_Setup.thy	Wed Aug 15 09:02:11 2007 +0200
     1.3 @@ -0,0 +1,164 @@
     1.4 +(*  Title:      HOL/Code_Setup.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Florian Haftmann
     1.7 +*)
     1.8 +
     1.9 +header {* Setup of code generators and derived tools *}
    1.10 +
    1.11 +theory Code_Setup
    1.12 +imports HOL
    1.13 +uses "~~/src/HOL/Tools/recfun_codegen.ML"
    1.14 +begin
    1.15 +
    1.16 +subsection {* SML code generator setup *}
    1.17 +
    1.18 +setup RecfunCodegen.setup
    1.19 +
    1.20 +types_code
    1.21 +  "bool"  ("bool")
    1.22 +attach (term_of) {*
    1.23 +fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    1.24 +*}
    1.25 +attach (test) {*
    1.26 +fun gen_bool i = one_of [false, true];
    1.27 +*}
    1.28 +  "prop"  ("bool")
    1.29 +attach (term_of) {*
    1.30 +fun term_of_prop b =
    1.31 +  HOLogic.mk_Trueprop (if b then HOLogic.true_const else HOLogic.false_const);
    1.32 +*}
    1.33 +
    1.34 +consts_code
    1.35 +  "Trueprop" ("(_)")
    1.36 +  "True"    ("true")
    1.37 +  "False"   ("false")
    1.38 +  "Not"     ("Bool.not")
    1.39 +  "op |"    ("(_ orelse/ _)")
    1.40 +  "op &"    ("(_ andalso/ _)")
    1.41 +  "If"      ("(if _/ then _/ else _)")
    1.42 +
    1.43 +setup {*
    1.44 +let
    1.45 +
    1.46 +fun eq_codegen thy defs gr dep thyname b t =
    1.47 +    (case strip_comb t of
    1.48 +       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
    1.49 +     | (Const ("op =", _), [t, u]) =>
    1.50 +          let
    1.51 +            val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
    1.52 +            val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u);
    1.53 +            val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
    1.54 +          in
    1.55 +            SOME (gr''', Codegen.parens
    1.56 +              (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
    1.57 +          end
    1.58 +     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
    1.59 +         thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
    1.60 +     | _ => NONE);
    1.61 +
    1.62 +in
    1.63 +  Codegen.add_codegen "eq_codegen" eq_codegen
    1.64 +end
    1.65 +*}
    1.66 +
    1.67 +text {* Evaluation *}
    1.68 +
    1.69 +method_setup evaluation = {*
    1.70 +  Method.no_args (Method.SIMPLE_METHOD' (CONVERSION Codegen.evaluation_conv THEN' rtac TrueI))
    1.71 +*} "solve goal by evaluation"
    1.72 +
    1.73 +
    1.74 +subsection {* Generic code generator setup *}
    1.75 +
    1.76 +
    1.77 +text {* using built-in Haskell equality *}
    1.78 +
    1.79 +code_class eq
    1.80 +  (Haskell "Eq" where "op =" \<equiv> "(==)")
    1.81 +
    1.82 +code_const "op ="
    1.83 +  (Haskell infixl 4 "==")
    1.84 +
    1.85 +
    1.86 +text {* type bool *}
    1.87 +
    1.88 +lemmas [code] = imp_conv_disj
    1.89 +
    1.90 +code_type bool
    1.91 +  (SML "bool")
    1.92 +  (OCaml "bool")
    1.93 +  (Haskell "Bool")
    1.94 +
    1.95 +code_instance bool :: eq
    1.96 +  (Haskell -)
    1.97 +
    1.98 +code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
    1.99 +  (Haskell infixl 4 "==")
   1.100 +
   1.101 +code_const True and False and Not and "op &" and "op |" and If
   1.102 +  (SML "true" and "false" and "not"
   1.103 +    and infixl 1 "andalso" and infixl 0 "orelse"
   1.104 +    and "!(if (_)/ then (_)/ else (_))")
   1.105 +  (OCaml "true" and "false" and "not"
   1.106 +    and infixl 4 "&&" and infixl 2 "||"
   1.107 +    and "!(if (_)/ then (_)/ else (_))")
   1.108 +  (Haskell "True" and "False" and "not"
   1.109 +    and infixl 3 "&&" and infixl 2 "||"
   1.110 +    and "!(if (_)/ then (_)/ else (_))")
   1.111 +
   1.112 +code_reserved SML
   1.113 +  bool true false not
   1.114 +
   1.115 +code_reserved OCaml
   1.116 +  bool not
   1.117 +
   1.118 +
   1.119 +text {* code generation for undefined as exception *}
   1.120 +
   1.121 +code_const undefined
   1.122 +  (SML "raise/ Fail/ \"undefined\"")
   1.123 +  (OCaml "failwith/ \"undefined\"")
   1.124 +  (Haskell "error/ \"undefined\"")
   1.125 +
   1.126 +
   1.127 +text {* Let and If *}
   1.128 +
   1.129 +lemmas [code func] = Let_def if_True if_False
   1.130 +
   1.131 +setup {*
   1.132 +  CodePackage.add_appconst (@{const_name Let}, CodePackage.appgen_let)
   1.133 +  #> CodePackage.add_appconst (@{const_name If}, CodePackage.appgen_if)
   1.134 +*}
   1.135 +
   1.136 +
   1.137 +subsection {* Evaluation oracle *}
   1.138 +
   1.139 +oracle eval_oracle ("term") = {* fn thy => fn t => 
   1.140 +  if CodePackage.satisfies thy (Thm.cterm_of thy (HOLogic.dest_Trueprop t)) [] 
   1.141 +  then t
   1.142 +  else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
   1.143 +*}
   1.144 +
   1.145 +method_setup eval = {*
   1.146 +let
   1.147 +  fun eval_tac thy = 
   1.148 +    SUBGOAL (fn (t, i) => rtac (eval_oracle thy t) i)
   1.149 +in 
   1.150 +  Method.ctxt_args (fn ctxt => 
   1.151 +    Method.SIMPLE_METHOD' (eval_tac (ProofContext.theory_of ctxt)))
   1.152 +end
   1.153 +*} "solve goal by evaluation"
   1.154 +
   1.155 +
   1.156 +subsection {* Normalization by evaluation *}
   1.157 +
   1.158 +setup Nbe.setup
   1.159 +
   1.160 +method_setup normalization = {*
   1.161 +  Method.no_args (Method.SIMPLE_METHOD'
   1.162 +    (CONVERSION (ObjectLogic.judgment_conv Nbe.normalization_conv)
   1.163 +      THEN' resolve_tac [TrueI, refl]))
   1.164 +*} "solve goal by normalization"
   1.165 +
   1.166 +
   1.167 +end