moved part of normalization oracle here
authorhaftmann
Tue Sep 19 15:22:29 2006 +0200 (2006-09-19)
changeset 2060296fa2cf465f5
parent 20601 3e1caf5a07c6
child 20603 37dfd7af2746
moved part of normalization oracle here
src/Pure/Tools/nbe.ML
     1.1 --- a/src/Pure/Tools/nbe.ML	Tue Sep 19 15:22:28 2006 +0200
     1.2 +++ b/src/Pure/Tools/nbe.ML	Tue Sep 19 15:22:29 2006 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  signature NBE =
     1.5  sig
     1.6    val norm_term: theory -> term -> term
     1.7 +  val normalization_conv: cterm -> thm
     1.8    val lookup: string -> NBE_Eval.Univ
     1.9    val update: string * NBE_Eval.Univ -> unit
    1.10    val trace_nbe: bool ref
    1.11 @@ -83,17 +84,18 @@
    1.12      val _ = trace (fn () => "Input:\n" ^ Display.raw_string_of_term t);
    1.13      fun compile_term t thy =
    1.14        let
    1.15 -        val thy' = CodegenPackage.purge_code thy;
    1.16 -        val nbe_tab = NBE_Data.get thy';
    1.17 -        val (t', thy'') = CodegenPackage.codegen_term t thy';
    1.18 -        val (modl_new, thy''') = CodegenPackage.get_root_module thy'';
    1.19 +        val _ = CodegenPackage.purge_code thy;
    1.20 +        val nbe_tab = NBE_Data.get thy;
    1.21 +        val (eq_thm, t'') = CodegenPackage.codegen_term thy t;
    1.22 +        val t' = (snd o Logic.dest_equals o Drule.plain_prop_of) eq_thm;
    1.23 +        val modl_new = CodegenPackage.get_root_module thy;
    1.24          val diff = CodegenThingol.diff_module (modl_new, CodegenThingol.empty_module);
    1.25          val _ = trace (fn () => "new definitions: " ^ (commas o map fst) diff);
    1.26          val _ = (tab := nbe_tab;
    1.27               Library.seq (use_code o NBE_Codegen.generate defined) diff);
    1.28 -        val thy'''' = NBE_Data.put (!tab) thy''';
    1.29 -        val nt' = NBE_Eval.nbe (!tab) t';
    1.30 -      in (nt', thy'''') end;
    1.31 +        val thy' = NBE_Data.put (!tab) thy;
    1.32 +        val nt' = NBE_Eval.nbe (!tab) t'';
    1.33 +      in ((t', nt'), thy') end;
    1.34      fun eval_term t nt thy =
    1.35        let
    1.36          val vtab = var_tab t;
    1.37 @@ -114,13 +116,24 @@
    1.38    in
    1.39      thy
    1.40      |> compile_term t
    1.41 -    |-> (fn nt => eval_term t nt)
    1.42 +    |-> (fn (t, nt) => eval_term t nt)
    1.43    end;
    1.44  
    1.45  fun norm_print' s thy = norm_print (Sign.read_term thy s) thy;
    1.46  
    1.47  fun norm_term thy t = fst (norm_print t (Theory.copy thy));
    1.48  
    1.49 +exception Normalization of term;
    1.50 +
    1.51 +fun normalization_oracle (thy, Normalization t) =
    1.52 +  Logic.mk_equals (t, norm_term thy t);
    1.53 +
    1.54 +fun normalization_conv ct =
    1.55 +  let val {sign, t, ...} = rep_cterm ct
    1.56 +  in Thm.invoke_oracle_i sign "Pure.Normalization" (sign, Normalization t) end;
    1.57 +
    1.58 +val _ = Context.add_setup
    1.59 +  (Theory.add_oracle ("Normalization", normalization_oracle));
    1.60  
    1.61  (* Isar setup *)
    1.62