merged
authorhaftmann
Mon Aug 23 11:57:32 2010 +0200 (2010-08-23)
changeset 386751c483d137371
parent 38643 8782e4f0cdc8
parent 38674 cd9b59cb1b75
child 38676 975e4f729127
child 38768 ecc713816e33
merged
     1.1 --- a/src/HOL/HOL.thy	Mon Aug 23 11:56:12 2010 +0200
     1.2 +++ b/src/HOL/HOL.thy	Mon Aug 23 11:57:32 2010 +0200
     1.3 @@ -1998,7 +1998,7 @@
     1.4    "solve goal by evaluation"
     1.5  
     1.6  method_setup normalization = {*
     1.7 -  Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))))
     1.8 +  Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.dynamic_eval_conv THEN' (fn k => TRY (rtac TrueI k)))))
     1.9  *} "solve goal by normalization"
    1.10  
    1.11  
     2.1 --- a/src/Pure/Isar/code.ML	Mon Aug 23 11:56:12 2010 +0200
     2.2 +++ b/src/Pure/Isar/code.ML	Mon Aug 23 11:57:32 2010 +0200
     2.3 @@ -78,7 +78,6 @@
     2.4  
     2.5    (*infrastructure*)
     2.6    val set_code_target_attr: (string -> thm -> theory -> theory) -> theory -> theory
     2.7 -  val purge_data: theory -> theory
     2.8  end;
     2.9  
    2.10  signature CODE_DATA_ARGS =
    2.11 @@ -266,8 +265,6 @@
    2.12  
    2.13  fun map_exec_purge f = Code_Data.map (fn (exec, _) => (f exec, empty_dataref ()));
    2.14  
    2.15 -val purge_data = (Code_Data.map o apsnd) (fn _ => empty_dataref ());
    2.16 -
    2.17  fun change_fun_spec delete c f = (map_exec_purge o map_functions
    2.18    o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, empty_fun_spec), [])))
    2.19      o apfst) (fn (_, spec) => (true, f spec));
     3.1 --- a/src/Pure/conv.ML	Mon Aug 23 11:56:12 2010 +0200
     3.2 +++ b/src/Pure/conv.ML	Mon Aug 23 11:57:32 2010 +0200
     3.3 @@ -48,6 +48,7 @@
     3.4    val concl_conv: int -> conv -> conv
     3.5    val fconv_rule: conv -> thm -> thm
     3.6    val gconv_rule: conv -> int -> thm -> thm
     3.7 +  val tap_thy: (theory -> conv) -> conv
     3.8  end;
     3.9  
    3.10  structure Conv: CONV =
    3.11 @@ -211,6 +212,9 @@
    3.12        end
    3.13    | NONE => raise THM ("gconv_rule", i, [th]));
    3.14  
    3.15 +
    3.16 +fun tap_thy conv ct = conv (Thm.theory_of_cterm ct) ct;
    3.17 +
    3.18  end;
    3.19  
    3.20  structure Basic_Conv: BASIC_CONV = Conv;
     4.1 --- a/src/Tools/Code/code_eval.ML	Mon Aug 23 11:56:12 2010 +0200
     4.2 +++ b/src/Tools/Code/code_eval.ML	Mon Aug 23 11:57:32 2010 +0200
     4.3 @@ -62,7 +62,7 @@
     4.4          val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
     4.5            ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
     4.6        in ML_Context.evaluate ctxt false reff sml_code end;
     4.7 -  in Code_Thingol.eval thy postproc evaluator t end;
     4.8 +  in Code_Thingol.dynamic_eval_value thy postproc evaluator t end;
     4.9  
    4.10  
    4.11  (** instrumentalization by antiquotation **)
     5.1 --- a/src/Tools/Code/code_preproc.ML	Mon Aug 23 11:56:12 2010 +0200
     5.2 +++ b/src/Tools/Code/code_preproc.ML	Mon Aug 23 11:57:32 2010 +0200
     5.3 @@ -24,11 +24,12 @@
     5.4    val all: code_graph -> string list
     5.5    val pretty: theory -> code_graph -> Pretty.T
     5.6    val obtain: theory -> string list -> term list -> code_algebra * code_graph
     5.7 -  val eval_conv: theory
     5.8 -    -> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm
     5.9 -  val eval: theory -> ((term -> term) -> 'a -> 'a)
    5.10 +  val dynamic_eval_conv: theory
    5.11 +    -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
    5.12 +  val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a)
    5.13      -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
    5.14 -  val pre_post_conv: theory -> (cterm -> thm) -> cterm -> thm
    5.15 +  val static_eval_conv: theory -> string list
    5.16 +    -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
    5.17  
    5.18    val setup: theory -> theory
    5.19  end
    5.20 @@ -74,8 +75,7 @@
    5.21    if AList.defined (op =) xs key then AList.delete (op =) key xs
    5.22    else error ("No such " ^ msg ^ ": " ^ quote key);
    5.23  
    5.24 -fun map_data f = Code.purge_data
    5.25 -  #> (Code_Preproc_Data.map o map_thmproc) f;
    5.26 +val map_data = Code_Preproc_Data.map o map_thmproc;
    5.27  
    5.28  val map_pre_post = map_data o apfst;
    5.29  val map_pre = map_pre_post o apfst;
    5.30 @@ -422,10 +422,12 @@
    5.31  
    5.32  (** retrieval and evaluation interfaces **)
    5.33  
    5.34 -fun obtain thy cs ts = apsnd snd
    5.35 -  (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts));
    5.36 +fun obtain thy consts ts = apsnd snd
    5.37 +  (Wellsorted.change_yield thy (extend_arities_eqngr thy consts ts));
    5.38  
    5.39 -fun gen_eval thy cterm_of conclude_evaluation evaluator proto_ct =
    5.40 +fun dest_cterm ct = let val t = Thm.term_of ct in (Term.add_tfrees t [], t) end;
    5.41 +
    5.42 +fun dynamic_eval thy cterm_of conclude_evaluation evaluator proto_ct =
    5.43    let
    5.44      val pp = Syntax.pp_global thy;
    5.45      val ct = cterm_of proto_ct;
    5.46 @@ -433,17 +435,13 @@
    5.47        (Thm.term_of ct);
    5.48      val thm = preprocess_conv thy ct;
    5.49      val ct' = Thm.rhs_of thm;
    5.50 -    val t' = Thm.term_of ct';
    5.51 -    val vs = Term.add_tfrees t' [];
    5.52 +    val (vs', t') = dest_cterm ct';
    5.53      val consts = fold_aterms
    5.54        (fn Const (c, _) => insert (op =) c | _ => I) t' [];
    5.55      val (algebra', eqngr') = obtain thy consts [t'];
    5.56 -  in conclude_evaluation (evaluator algebra' eqngr' vs t' ct') thm end;
    5.57 +  in conclude_evaluation (evaluator algebra' eqngr' vs' t' ct') thm end;
    5.58  
    5.59 -fun simple_evaluator evaluator algebra eqngr vs t ct =
    5.60 -  evaluator algebra eqngr vs t;
    5.61 -
    5.62 -fun eval_conv thy =
    5.63 +fun dynamic_eval_conv thy =
    5.64    let
    5.65      fun conclude_evaluation thm2 thm1 =
    5.66        let
    5.67 @@ -453,12 +451,22 @@
    5.68            error ("could not construct evaluation proof:\n"
    5.69            ^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
    5.70        end;
    5.71 -  in gen_eval thy I conclude_evaluation end;
    5.72 +  in dynamic_eval thy I conclude_evaluation end;
    5.73 +
    5.74 +fun dynamic_eval_value thy postproc evaluator = dynamic_eval thy (Thm.cterm_of thy)
    5.75 +  (K o postproc (postprocess_term thy)) (K oooo evaluator);
    5.76  
    5.77 -fun eval thy postproc evaluator = gen_eval thy (Thm.cterm_of thy)
    5.78 -  (K o postproc (postprocess_term thy)) (simple_evaluator evaluator);
    5.79 -
    5.80 -fun pre_post_conv thy conv = (preprocess_conv thy) then_conv conv then_conv (postprocess_conv thy);
    5.81 +fun static_eval_conv thy consts conv =
    5.82 +  let
    5.83 +    val (algebra, eqngr) = obtain thy consts [];
    5.84 +    fun conv' ct =
    5.85 +      let
    5.86 +        val (vs, t) = dest_cterm ct;
    5.87 +      in
    5.88 +        Conv.tap_thy (fn thy => (preprocess_conv thy)
    5.89 +          then_conv (conv algebra eqngr vs t) then_conv (postprocess_conv thy)) ct
    5.90 +      end;
    5.91 +  in conv' end;
    5.92  
    5.93  
    5.94  (** setup **)
     6.1 --- a/src/Tools/Code/code_simp.ML	Mon Aug 23 11:56:12 2010 +0200
     6.2 +++ b/src/Tools/Code/code_simp.ML	Mon Aug 23 11:57:32 2010 +0200
     6.3 @@ -8,11 +8,11 @@
     6.4  sig
     6.5    val no_frees_conv: conv -> conv
     6.6    val map_ss: (simpset -> simpset) -> theory -> theory
     6.7 -  val current_conv: theory -> conv
     6.8 -  val current_tac: theory -> int -> tactic
     6.9 -  val current_value: theory -> term -> term
    6.10 -  val make_conv: theory -> simpset option -> string list -> conv
    6.11 -  val make_tac: theory -> simpset option -> string list -> int -> tactic
    6.12 +  val dynamic_eval_conv: theory -> conv
    6.13 +  val dynamic_eval_tac: theory -> int -> tactic
    6.14 +  val dynamic_eval_value: theory -> term -> term
    6.15 +  val static_eval_conv: theory -> simpset option -> string list -> conv
    6.16 +  val static_eval_tac: theory -> simpset option -> string list -> int -> tactic
    6.17    val setup: theory -> theory
    6.18  end;
    6.19  
    6.20 @@ -67,25 +67,25 @@
    6.21  
    6.22  (* evaluation with current code context *)
    6.23  
    6.24 -fun current_conv thy = no_frees_conv (Code_Thingol.eval_conv thy
    6.25 +fun dynamic_eval_conv thy = no_frees_conv (Code_Thingol.dynamic_eval_conv thy
    6.26    (fn naming => fn program => fn t => fn deps => rewrite_modulo thy NONE program));
    6.27  
    6.28 -fun current_tac thy = CONVERSION (current_conv thy) THEN' conclude_tac thy NONE;
    6.29 +fun dynamic_eval_tac thy = CONVERSION (dynamic_eval_conv thy) THEN' conclude_tac thy NONE;
    6.30  
    6.31 -fun current_value thy = snd o Logic.dest_equals o Thm.prop_of o current_conv thy o Thm.cterm_of thy;
    6.32 +fun dynamic_eval_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_eval_conv thy o Thm.cterm_of thy;
    6.33  
    6.34  val setup = Method.setup (Binding.name "code_simp")
    6.35 -  (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo current_tac o ProofContext.theory_of)))
    6.36 +  (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_eval_tac o ProofContext.theory_of)))
    6.37    "simplification with code equations"
    6.38 -  #> Value.add_evaluator ("simp", current_value o ProofContext.theory_of);
    6.39 +  #> Value.add_evaluator ("simp", dynamic_eval_value o ProofContext.theory_of);
    6.40  
    6.41  
    6.42  (* evaluation with freezed code context *)
    6.43  
    6.44 -fun make_conv thy some_ss consts = no_frees_conv (Code_Preproc.pre_post_conv thy
    6.45 -  ((rewrite_modulo thy some_ss o snd o snd o Code_Thingol.consts_program thy false) consts));
    6.46 +fun static_eval_conv thy some_ss consts = no_frees_conv
    6.47 +  (Code_Thingol.static_eval_conv_simple thy consts (rewrite_modulo thy some_ss));
    6.48  
    6.49 -fun make_tac thy some_ss consts = CONVERSION (make_conv thy some_ss consts)
    6.50 +fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts)
    6.51    THEN' conclude_tac thy some_ss;
    6.52  
    6.53  end;
     7.1 --- a/src/Tools/Code/code_thingol.ML	Mon Aug 23 11:56:12 2010 +0200
     7.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Aug 23 11:57:32 2010 +0200
     7.3 @@ -92,12 +92,17 @@
     7.4  
     7.5    val read_const_exprs: theory -> string list -> string list * string list
     7.6    val consts_program: theory -> bool -> string list -> string list * (naming * program)
     7.7 -  val eval_conv: theory
     7.8 -    -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> cterm -> thm)
     7.9 -    -> cterm -> thm
    7.10 -  val eval: theory -> ((term -> term) -> 'a -> 'a)
    7.11 +  val dynamic_eval_conv: theory
    7.12 +    -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
    7.13 +    -> conv
    7.14 +  val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a)
    7.15      -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
    7.16      -> term -> 'a
    7.17 +  val static_eval_conv: theory -> string list
    7.18 +    -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
    7.19 +    -> conv
    7.20 +  val static_eval_conv_simple: theory -> string list
    7.21 +    -> (program -> conv) -> conv
    7.22  end;
    7.23  
    7.24  structure Code_Thingol: CODE_THINGOL =
    7.25 @@ -846,7 +851,7 @@
    7.26  
    7.27  fun consts_program thy permissive cs =
    7.28    let
    7.29 -    fun project_consts cs (naming, program) =
    7.30 +    fun project_consts cs (naming, program) = (*FIXME only necessary for cache_generation*)
    7.31        let
    7.32          val cs_all = Graph.all_succs program cs;
    7.33        in (cs, (naming, Graph.subgraph (member (op =) cs_all) program)) end;
    7.34 @@ -895,8 +900,17 @@
    7.35      val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs';
    7.36    in evaluator naming program ((vs'', (vs', ty')), t') deps end;
    7.37  
    7.38 -fun eval_conv thy = Code_Preproc.eval_conv thy o base_evaluator thy;
    7.39 -fun eval thy postproc = Code_Preproc.eval thy postproc o base_evaluator thy;
    7.40 +fun dynamic_eval_conv thy = Code_Preproc.dynamic_eval_conv thy o base_evaluator thy;
    7.41 +fun dynamic_eval_value thy postproc = Code_Preproc.dynamic_eval_value thy postproc o base_evaluator thy;
    7.42 +
    7.43 +fun static_eval_conv thy consts conv =
    7.44 +  Code_Preproc.static_eval_conv thy consts (base_evaluator thy conv); (*FIXME avoid re-generation*)
    7.45 +
    7.46 +fun static_eval_conv_simple thy consts conv =
    7.47 +  Code_Preproc.static_eval_conv thy consts (fn algebra => fn eqngr => fn _ => fn _ => fn ct =>
    7.48 +    conv ((NONE, (empty_naming, Graph.empty)) (*FIXME provide abstraction for this kind of invocation*)
    7.49 +      |> fold_map (ensure_const thy algebra eqngr false) consts
    7.50 +      |> (snd o snd o snd)) ct);
    7.51  
    7.52  
    7.53  (** diagnostic commands **)
     8.1 --- a/src/Tools/nbe.ML	Mon Aug 23 11:56:12 2010 +0200
     8.2 +++ b/src/Tools/nbe.ML	Mon Aug 23 11:57:32 2010 +0200
     8.3 @@ -6,8 +6,8 @@
     8.4  
     8.5  signature NBE =
     8.6  sig
     8.7 -  val norm_conv: cterm -> thm
     8.8 -  val norm: theory -> term -> term
     8.9 +  val dynamic_eval_conv: conv
    8.10 +  val dynamic_eval_value: theory -> term -> term
    8.11  
    8.12    datatype Univ =
    8.13        Const of int * Univ list               (*named (uninterpreted) constants*)
    8.14 @@ -574,12 +574,11 @@
    8.15      val rhs = Thm.cterm_of thy raw_rhs;
    8.16    in Thm.mk_binop eq lhs rhs end;
    8.17  
    8.18 -val (_, raw_norm_oracle) = Context.>>> (Context.map_theory_result
    8.19 +val (_, raw_oracle) = Context.>>> (Context.map_theory_result
    8.20    (Thm.add_oracle (Binding.name "norm", fn (thy, program, vsp_ty_t, deps, ct) =>
    8.21      mk_equals thy ct (normalize thy program vsp_ty_t deps))));
    8.22  
    8.23 -fun norm_oracle thy program vsp_ty_t deps ct =
    8.24 -  raw_norm_oracle (thy, program, vsp_ty_t, deps, ct);
    8.25 +fun oracle thy program vsp_ty_t deps ct = raw_oracle (thy, program, vsp_ty_t, deps, ct);
    8.26  
    8.27  fun no_frees_rew rew t =
    8.28    let
    8.29 @@ -591,12 +590,11 @@
    8.30      |> (fn t' => Term.betapplys (t', frees))
    8.31    end;
    8.32  
    8.33 -val norm_conv = Code_Simp.no_frees_conv (fn ct =>
    8.34 -  let
    8.35 -    val thy = Thm.theory_of_cterm ct;
    8.36 -  in lift_triv_classes_conv thy (Code_Thingol.eval_conv thy (K (norm_oracle thy))) ct end);
    8.37 +val dynamic_eval_conv = Code_Simp.no_frees_conv (Conv.tap_thy
    8.38 +  (fn thy => lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy (K (oracle thy)))));
    8.39  
    8.40 -fun norm thy = lift_triv_classes_rew thy (no_frees_rew (Code_Thingol.eval thy I (K (normalize thy))));
    8.41 +fun dynamic_eval_value thy = lift_triv_classes_rew thy
    8.42 +  (no_frees_rew (Code_Thingol.dynamic_eval_value thy I (K (normalize thy))));
    8.43  
    8.44  
    8.45  (* evaluation command *)
    8.46 @@ -604,7 +602,7 @@
    8.47  fun norm_print_term ctxt modes t =
    8.48    let
    8.49      val thy = ProofContext.theory_of ctxt;
    8.50 -    val t' = norm thy t;
    8.51 +    val t' = dynamic_eval_value thy t;
    8.52      val ty' = Term.type_of t';
    8.53      val ctxt' = Variable.auto_fixes t ctxt;
    8.54      val p = Print_Mode.with_modes modes (fn () =>
    8.55 @@ -619,7 +617,7 @@
    8.56    let val ctxt = Toplevel.context_of state
    8.57    in norm_print_term ctxt modes (Syntax.read_term ctxt s) end;
    8.58  
    8.59 -val setup = Value.add_evaluator ("nbe", norm o ProofContext.theory_of);
    8.60 +val setup = Value.add_evaluator ("nbe", dynamic_eval_value o ProofContext.theory_of);
    8.61  
    8.62  val opt_modes =
    8.63    Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];