clarified relationship of code generator conversions and evaluations
authorhaftmann
Thu Oct 04 19:41:49 2007 +0200 (2007-10-04)
changeset 248358c26128f8997
parent 24834 5684cbf8c895
child 24836 dab06e93ec28
clarified relationship of code generator conversions and evaluations
src/HOL/Code_Setup.thy
src/HOL/Library/Eval.thy
src/HOL/Library/Eval_Witness.thy
src/HOL/ex/Eval_Examples.thy
src/Tools/code/code_funcgr.ML
src/Tools/code/code_package.ML
     1.1 --- a/src/HOL/Code_Setup.thy	Thu Oct 04 16:59:30 2007 +0200
     1.2 +++ b/src/HOL/Code_Setup.thy	Thu Oct 04 19:41:49 2007 +0200
     1.3 @@ -136,7 +136,7 @@
     1.4  subsection {* Evaluation oracle *}
     1.5  
     1.6  oracle eval_oracle ("term") = {* fn thy => fn t => 
     1.7 -  if CodePackage.satisfies thy (Thm.cterm_of thy (HOLogic.dest_Trueprop t)) [] 
     1.8 +  if CodePackage.satisfies thy (HOLogic.dest_Trueprop t) [] 
     1.9    then t
    1.10    else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
    1.11  *}
    1.12 @@ -156,7 +156,7 @@
    1.13  
    1.14  method_setup normalization = {*
    1.15    Method.no_args (Method.SIMPLE_METHOD'
    1.16 -    (CONVERSION (ObjectLogic.judgment_conv Nbe.normalization_conv)
    1.17 +    (CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv)
    1.18        THEN' resolve_tac [TrueI, refl]))
    1.19  *} "solve goal by normalization"
    1.20  
     2.1 --- a/src/HOL/Library/Eval.thy	Thu Oct 04 16:59:30 2007 +0200
     2.2 +++ b/src/HOL/Library/Eval.thy	Thu Oct 04 19:41:49 2007 +0200
     2.3 @@ -157,9 +157,10 @@
     2.4  signature EVAL =
     2.5  sig
     2.6    val eval_ref: (unit -> term) option ref
     2.7 -  val eval_conv: cterm -> thm
     2.8 -  val eval_print: (cterm -> thm) -> Proof.context -> term -> unit
     2.9 -  val eval_print_cmd: (cterm -> thm) -> string -> Toplevel.state -> unit
    2.10 +  val eval_term: theory -> term -> term
    2.11 +  val evaluate: Proof.context -> term -> unit
    2.12 +  val evaluate': string -> Proof.context -> term -> unit
    2.13 +  val evaluate_cmd: string option -> Toplevel.state -> unit
    2.14  end;
    2.15  
    2.16  structure Eval =
    2.17 @@ -167,61 +168,46 @@
    2.18  
    2.19  val eval_ref = ref (NONE : (unit -> term) option);
    2.20  
    2.21 -end;
    2.22 -*}
    2.23 +fun eval_invoke thy code ((_, ty), t) deps _ =
    2.24 +  CodePackage.eval_invoke thy ("Eval.eval_ref", eval_ref) code (t, ty) [];
    2.25  
    2.26 -oracle eval_oracle ("term * CodeThingol.code * (CodeThingol.typscheme * CodeThingol.iterm) * cterm") =
    2.27 -{* fn thy => fn (t0, code, ((vs, ty), t), ct) => 
    2.28 -let
    2.29 -  val _ = (Term.map_types o Term.map_atyps) (fn _ =>
    2.30 -    error ("Term " ^ Sign.string_of_term thy t0 ^ " contains polymorphic type"))
    2.31 -    t0;
    2.32 -in
    2.33 -  Logic.mk_equals (t0,
    2.34 -    CodePackage.eval_invoke thy ("Eval.eval_ref", Eval.eval_ref) code (t, ty) [])
    2.35 -end;
    2.36 -*}
    2.37 +fun eval_term thy =
    2.38 +  TermOf.mk_term_of
    2.39 +  #> CodePackage.eval_term thy (eval_invoke thy)
    2.40 +  #> Code.postprocess_term thy;
    2.41  
    2.42 -ML {*
    2.43 -structure Eval : EVAL =
    2.44 -struct
    2.45 -
    2.46 -open Eval;
    2.47 -
    2.48 -fun eval_invoke thy t0 code vs_ty_t _ ct = eval_oracle thy (t0, code, vs_ty_t, ct);
    2.49 +val evaluators = [
    2.50 +  ("code", eval_term),
    2.51 +  ("SML", Codegen.eval_term),
    2.52 +  ("normal_form", Nbe.norm_term)
    2.53 +];
    2.54  
    2.55 -fun eval_conv ct =
    2.56 -  let
    2.57 -    val thy = Thm.theory_of_cterm ct;
    2.58 -    val ct' = (Thm.cterm_of thy o TermOf.mk_term_of o Thm.term_of) ct;
    2.59 -  in
    2.60 -    CodePackage.eval_term thy
    2.61 -      (eval_invoke thy (Thm.term_of ct)) ct'
    2.62 -  end;
    2.63 -
    2.64 -fun eval_print conv ctxt t =
    2.65 +fun gen_evaluate evaluators ctxt t =
    2.66    let
    2.67      val thy = ProofContext.theory_of ctxt;
    2.68 -    val ct = Thm.cterm_of thy t;
    2.69 -    val (_, t') = (Logic.dest_equals o Thm.prop_of o conv) ct;
    2.70 -    val ty = Term.type_of t';
    2.71 -    val p = 
    2.72 -      Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), Pretty.fbrk,
    2.73 -        Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty)];
    2.74 +    val (evls, evl) = split_last evaluators;
    2.75 +    val t' = case get_first (fn f => try (f thy) t) evls
    2.76 +     of SOME t' => t'
    2.77 +      | NONE => evl thy t;
    2.78 +    val ty' = Term.type_of t';
    2.79 +    val p = Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'),
    2.80 +      Pretty.fbrk, Pretty.str "::", Pretty.brk 1,
    2.81 +      Pretty.quote (ProofContext.pretty_typ ctxt ty')];
    2.82    in Pretty.writeln p end;
    2.83  
    2.84 -fun eval_print_cmd conv raw_t state =
    2.85 +val evaluate = gen_evaluate (map snd evaluators);
    2.86 +
    2.87 +fun evaluate' name = gen_evaluate
    2.88 +  [(the o AList.lookup (op =) evaluators) name];
    2.89 +
    2.90 +fun evaluate_cmd some_name raw_t state =
    2.91    let
    2.92      val ctxt = Toplevel.context_of state;
    2.93      val t = Syntax.read_term ctxt raw_t;
    2.94 -    val thy = ProofContext.theory_of ctxt;
    2.95 -    val ct = Thm.cterm_of thy t;
    2.96 -    val (_, t') = (Logic.dest_equals o Thm.prop_of o conv) ct;
    2.97 -    val ty = Term.type_of t';
    2.98 -    val p = 
    2.99 -      Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), Pretty.fbrk,
   2.100 -        Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty)];
   2.101 -  in Pretty.writeln p end;
   2.102 +  in case some_name
   2.103 +   of NONE => evaluate ctxt t
   2.104 +    | SOME name => evaluate' name ctxt t
   2.105 +  end;
   2.106  
   2.107  end;
   2.108  *}
   2.109 @@ -229,11 +215,10 @@
   2.110  ML {*
   2.111  val valueP =
   2.112    OuterSyntax.improper_command "value" "read, evaluate and print term" OuterKeyword.diag
   2.113 -    (OuterParse.term
   2.114 -      >> (fn t => Toplevel.no_timing o Toplevel.keep
   2.115 -           (Eval.eval_print_cmd (fn ct => case try Eval.eval_conv ct
   2.116 -     of SOME thm => thm
   2.117 -      | NONE => Codegen.evaluation_conv ct) t)));
   2.118 +    (Scan.option (OuterParse.$$$ "(" |-- OuterParse.name --| OuterParse.$$$ ")")
   2.119 +    -- OuterParse.term
   2.120 +      >> (fn (some_name, t) => Toplevel.no_timing o Toplevel.keep
   2.121 +           (Eval.evaluate_cmd some_name t)));
   2.122  
   2.123  val _ = OuterSyntax.add_parsers [valueP];
   2.124  *}
     3.1 --- a/src/HOL/Library/Eval_Witness.thy	Thu Oct 04 16:59:30 2007 +0200
     3.2 +++ b/src/HOL/Library/Eval_Witness.thy	Thu Oct 04 19:41:49 2007 +0200
     3.3 @@ -57,12 +57,11 @@
     3.4      | dest_exs n (Const ("Ex", _) $ Abs (v,T,b)) = 
     3.5        Abs (v, check_type T, dest_exs (n - 1) b)
     3.6      | dest_exs _ _ = sys_error "dest_exs";
     3.7 -
     3.8 -  val ct = Thm.cterm_of thy (dest_exs (length ws) (HOLogic.dest_Trueprop goal))
     3.9 +  val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
    3.10  in
    3.11 -  if CodePackage.satisfies thy ct ws
    3.12 +  if CodePackage.satisfies thy t ws
    3.13    then goal
    3.14 -  else HOLogic.Trueprop $ (HOLogic.true_const) (*dummy*)
    3.15 +  else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
    3.16  end
    3.17  *}
    3.18  
     4.1 --- a/src/HOL/ex/Eval_Examples.thy	Thu Oct 04 16:59:30 2007 +0200
     4.2 +++ b/src/HOL/ex/Eval_Examples.thy	Thu Oct 04 19:41:49 2007 +0200
     4.3 @@ -27,14 +27,44 @@
     4.4  text {* term evaluation *}
     4.5  
     4.6  value "(Suc 2 + 1) * 4"
     4.7 -value "(Suc 2 + 1) * 4"
     4.8 +value (code) "(Suc 2 + 1) * 4"
     4.9 +value (SML) "(Suc 2 + 1) * 4"
    4.10 +value ("normal_form") "(Suc 2 + 1) * 4"
    4.11 +
    4.12  value "(Suc 2 + Suc 0) * Suc 3"
    4.13 +value (code) "(Suc 2 + Suc 0) * Suc 3"
    4.14 +value (SML) "(Suc 2 + Suc 0) * Suc 3"
    4.15 +value ("normal_form") "(Suc 2 + Suc 0) * Suc 3"
    4.16 +
    4.17  value "nat 100"
    4.18 +value (code) "nat 100"
    4.19 +value (SML) "nat 100"
    4.20 +value ("normal_form") "nat 100"
    4.21 +
    4.22  value "(10\<Colon>int) \<le> 12"
    4.23 +value (code) "(10\<Colon>int) \<le> 12"
    4.24 +value (SML) "(10\<Colon>int) \<le> 12"
    4.25 +value ("normal_form") "(10\<Colon>int) \<le> 12"
    4.26 +
    4.27 +value "max (2::int) 4"
    4.28 +value (code) "max (2::int) 4"
    4.29 +value (SML) "max (2::int) 4"
    4.30 +value ("normal_form") "max (2::int) 4"
    4.31 +
    4.32 +value "of_int 2 / of_int 4 * (1::rat)"
    4.33 +(*value (code) "of_int 2 / of_int 4 * (1::rat)" FIXME*)
    4.34 +value (SML) "of_int 2 / of_int 4 * (1::rat)"
    4.35 +value ("normal_form") "of_int 2 / of_int 4 * (1::rat)"
    4.36 +
    4.37  value "[]::nat list"
    4.38 +value (code) "[]::nat list"
    4.39 +(*value (SML) "[]::nat list" FIXME*)
    4.40 +value ("normal_form") "[]::nat list"
    4.41 +
    4.42  value "[(nat 100, ())]"
    4.43 -value "max (2::int) 4"
    4.44 -value "of_int 2 / of_int 4 * (1::rat)"
    4.45 +value (code) "[(nat 100, ())]"
    4.46 +(*value (SML) "[(nat 100, ())]" FIXME*)
    4.47 +value ("normal_form") "[(nat 100, ())]"
    4.48  
    4.49  
    4.50  text {* a fancy datatype *}
    4.51 @@ -47,5 +77,8 @@
    4.52      Cair 'a 'b
    4.53  
    4.54  value "Shift (Cair (4::nat) [Suc 0])"
    4.55 +value (code) "Shift (Cair (4::nat) [Suc 0])"
    4.56 +value (SML) "Shift (Cair (4::nat) [Suc 0])"
    4.57 +value ("normal_form") "Shift (Cair (4::nat) [Suc 0])"
    4.58  
    4.59  end
     5.1 --- a/src/Tools/code/code_funcgr.ML	Thu Oct 04 16:59:30 2007 +0200
     5.2 +++ b/src/Tools/code/code_funcgr.ML	Thu Oct 04 19:41:49 2007 +0200
     5.3 @@ -17,7 +17,7 @@
     5.4    val make: theory -> string list -> T
     5.5    val make_consts: theory -> string list -> string list * T
     5.6    val eval_conv: theory -> (T -> cterm -> thm) -> cterm -> thm
     5.7 -  val eval_term: theory -> (T -> cterm -> 'a) -> cterm -> 'a
     5.8 +  val eval_term: theory -> (T -> term -> 'a) -> term -> 'a
     5.9  end
    5.10  
    5.11  structure CodeFuncgr : CODE_FUNCGR =
    5.12 @@ -155,7 +155,7 @@
    5.13  fun instances_of thy algebra insts =
    5.14    let
    5.15      val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy;
    5.16 -    fun all_classops tyco class =
    5.17 +    fun all_classparams tyco class =
    5.18        try (AxClass.params_of_class thy) class
    5.19        |> Option.map snd
    5.20        |> these
    5.21 @@ -164,7 +164,7 @@
    5.22      Symtab.empty
    5.23      |> fold (fn (tyco, class) =>
    5.24          Symtab.map_default (tyco, []) (insert (op =) class)) insts
    5.25 -    |> (fn tab => Symtab.fold (fn (tyco, classes) => append (maps (all_classops tyco)
    5.26 +    |> (fn tab => Symtab.fold (fn (tyco, classes) => append (maps (all_classparams tyco)
    5.27           (Graph.all_succs thy_classes classes))) tab [])
    5.28    end;
    5.29  
    5.30 @@ -320,10 +320,10 @@
    5.31        end;
    5.32    in raw_eval thy conv' end;
    5.33  
    5.34 -fun raw_eval_term thy f =
    5.35 +fun raw_eval_term thy f t =
    5.36    let
    5.37 -    fun f' _ _ funcgr ct = f funcgr ct;
    5.38 -  in raw_eval thy f' end;
    5.39 +    fun f' _ _ funcgr ct = f funcgr (Thm.term_of ct);
    5.40 +  in raw_eval thy f' (Thm.cterm_of thy t) end;
    5.41  
    5.42  end; (*local*)
    5.43  
     6.1 --- a/src/Tools/code/code_package.ML	Thu Oct 04 16:59:30 2007 +0200
     6.2 +++ b/src/Tools/code/code_package.ML	Thu Oct 04 19:41:49 2007 +0200
     6.3 @@ -13,10 +13,10 @@
     6.4      -> cterm -> thm;
     6.5    val eval_term: theory
     6.6      -> (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm
     6.7 -       -> string list -> cterm -> 'a)
     6.8 -    -> cterm -> 'a;
     6.9 +       -> string list -> term -> 'a)
    6.10 +    -> term -> 'a;
    6.11    val satisfies_ref: (unit -> bool) option ref;
    6.12 -  val satisfies: theory -> cterm -> string list -> bool;
    6.13 +  val satisfies: theory -> term -> string list -> bool;
    6.14    val eval_invoke: theory -> (string * (unit -> 'a) option ref) -> CodeThingol.code
    6.15      -> CodeThingol.iterm * CodeThingol.itype -> string list -> 'a;
    6.16    val codegen_command: theory -> string -> unit;
    6.17 @@ -213,20 +213,20 @@
    6.18  and ensure_def_inst thy (algbr as ((_, algebra), _)) funcgr (class, tyco) =
    6.19    let
    6.20      val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
    6.21 -    val (var, classops) = try (AxClass.params_of_class thy) class |> the_default ("'a", [])
    6.22 +    val (var, classparams) = try (AxClass.params_of_class thy) class |> the_default ("'a", [])
    6.23      val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
    6.24      val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
    6.25      val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
    6.26        Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
    6.27      val arity_typ = Type (tyco, map TFree vs);
    6.28      val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
    6.29 -    fun gen_superarity superclass =
    6.30 +    fun exprgen_superarity superclass =
    6.31        ensure_def_class thy algbr funcgr superclass
    6.32        ##>> ensure_def_classrel thy algbr funcgr (class, superclass)
    6.33        ##>> exprgen_dicts thy algbr funcgr (arity_typ, [superclass])
    6.34        #>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
    6.35              (superclass, (classrel, (inst, dss))));
    6.36 -    fun gen_classop_def (c, ty) =
    6.37 +    fun exprgen_classparam_inst (c, ty) =
    6.38        let
    6.39          val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
    6.40          val thm = Class.unoverload thy (Thm.cterm_of thy c_inst);
    6.41 @@ -241,10 +241,10 @@
    6.42        ensure_def_class thy algbr funcgr class
    6.43        ##>> ensure_def_tyco thy algbr funcgr tyco
    6.44        ##>> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
    6.45 -      ##>> fold_map gen_superarity superclasses
    6.46 -      ##>> fold_map gen_classop_def classops
    6.47 -      #>> (fn ((((class, tyco), arity), superarities), classops) =>
    6.48 -             CodeThingol.Classinst ((class, (tyco, arity)), (superarities, classops)));
    6.49 +      ##>> fold_map exprgen_superarity superclasses
    6.50 +      ##>> fold_map exprgen_classparam_inst classparams
    6.51 +      #>> (fn ((((class, tyco), arity), superarities), classparams) =>
    6.52 +             CodeThingol.Classinst ((class, (tyco, arity)), (superarities, classparams)));
    6.53      val inst = CodeName.instance thy (class, tyco);
    6.54    in
    6.55      ensure_def thy defgen_inst inst
    6.56 @@ -256,9 +256,9 @@
    6.57      fun defgen_datatypecons tyco =
    6.58        ensure_def_tyco thy algbr funcgr tyco
    6.59        #>> K (CodeThingol.Datatypecons c');
    6.60 -    fun defgen_classop class =
    6.61 +    fun defgen_classparam class =
    6.62        ensure_def_class thy algbr funcgr class
    6.63 -      #>> K (CodeThingol.Classop c');
    6.64 +      #>> K (CodeThingol.Classparam c');
    6.65      fun defgen_fun trns =
    6.66        let
    6.67          val raw_thms = CodeFuncgr.funcs funcgr c;
    6.68 @@ -277,14 +277,14 @@
    6.69      val defgen = case Code.get_datatype_of_constr thy c
    6.70       of SOME tyco => defgen_datatypecons tyco
    6.71        | NONE => (case AxClass.class_of_param thy c
    6.72 -         of SOME class => defgen_classop class
    6.73 +         of SOME class => defgen_classparam class
    6.74            | NONE => defgen_fun)
    6.75    in
    6.76      ensure_def thy defgen c'
    6.77      #> pair c'
    6.78    end
    6.79  and exprgen_term thy algbr funcgr (Const (c, ty)) =
    6.80 -      select_appgen thy algbr funcgr ((c, ty), [])
    6.81 +      exprgen_app thy algbr funcgr ((c, ty), [])
    6.82    | exprgen_term thy algbr funcgr (Free (v, _)) =
    6.83        pair (IVar v)
    6.84    | exprgen_term thy algbr funcgr (Abs (abs as (_, ty, _))) =
    6.85 @@ -298,7 +298,7 @@
    6.86    | exprgen_term thy algbr funcgr (t as _ $ _) =
    6.87        case strip_comb t
    6.88         of (Const (c, ty), ts) =>
    6.89 -            select_appgen thy algbr funcgr ((c, ty), ts)
    6.90 +            exprgen_app thy algbr funcgr ((c, ty), ts)
    6.91          | (t', ts) =>
    6.92              exprgen_term thy algbr funcgr t'
    6.93              ##>> fold_map (exprgen_term thy algbr funcgr) ts
    6.94 @@ -313,7 +313,7 @@
    6.95    exprgen_const thy algbr funcgr c_ty
    6.96    ##>> fold_map (exprgen_term thy algbr funcgr) ts
    6.97    #>> (fn (t, ts) => t `$$ ts)
    6.98 -and select_appgen thy algbr funcgr ((c, ty), ts) =
    6.99 +and exprgen_app thy algbr funcgr ((c, ty), ts) =
   6.100    case Symtab.lookup (Appgens.get thy) c
   6.101     of SOME (i, (appgen, _)) =>
   6.102          if length ts < i then
   6.103 @@ -430,10 +430,10 @@
   6.104      val code = Program.get thy;
   6.105      val seris' = map (fn (((target, module), file), args) =>
   6.106        CodeTarget.get_serializer thy target permissive module file args
   6.107 -        CodeName.labelled_name (K false) cs) seris;
   6.108 +        CodeName.labelled_name cs) seris;
   6.109    in (map (fn f => f code) seris' : unit list; ()) end;
   6.110  
   6.111 -fun raw_eval f thy g =
   6.112 +fun raw_eval evaluate term_of thy g =
   6.113    let
   6.114      val value_name = "Isabelle_Eval.EVAL.EVAL";
   6.115      fun ensure_eval thy algbr funcgr t = 
   6.116 @@ -459,23 +459,23 @@
   6.117        end;
   6.118      fun h funcgr ct =
   6.119        let
   6.120 -        val (code, vs_ty_t, deps) = generate thy funcgr ensure_eval (Thm.term_of ct);
   6.121 +        val (code, vs_ty_t, deps) = generate thy funcgr ensure_eval (term_of ct);
   6.122        in g code vs_ty_t deps ct end;
   6.123 -  in f thy h end;
   6.124 +  in evaluate thy h end;
   6.125  
   6.126 -fun eval_conv thy = raw_eval CodeFuncgr.eval_conv thy;
   6.127 -fun eval_term thy = raw_eval CodeFuncgr.eval_term thy;
   6.128 +fun eval_conv thy = raw_eval CodeFuncgr.eval_conv Thm.term_of thy;
   6.129 +fun eval_term thy = raw_eval CodeFuncgr.eval_term I thy;
   6.130  
   6.131 -fun eval_invoke thy = CodeTarget.eval_invoke thy CodeName.labelled_name (K false);
   6.132 +fun eval_invoke thy = CodeTarget.eval_invoke thy CodeName.labelled_name;
   6.133  
   6.134  val satisfies_ref : (unit -> bool) option ref = ref NONE;
   6.135  
   6.136 -fun satisfies thy ct witnesses =
   6.137 +fun satisfies thy t witnesses =
   6.138    let
   6.139      fun evl code ((vs, ty), t) deps ct =
   6.140        eval_invoke thy ("CodePackage.satisfies_ref", satisfies_ref)
   6.141          code (t, ty) witnesses;
   6.142 -  in eval_term thy evl ct end;
   6.143 +  in eval_term thy evl t end;
   6.144  
   6.145  fun filter_generatable thy consts =
   6.146    let