# HG changeset patch
# User haftmann
# Date 1239950094 -7200
# Node ID 1e246776f876cb5bb20fa56cde52e3d92770a73f
# Parent  705bb15b236508eef0b33b1b581a6007baba8eca
diagnostic commands now in code_thingol; tuned code of funny continuations

diff -r 705bb15b2365 -r 1e246776f876 src/Tools/code/code_thingol.ML
--- a/src/Tools/code/code_thingol.ML	Fri Apr 17 08:34:53 2009 +0200
+++ b/src/Tools/code/code_thingol.ML	Fri Apr 17 08:34:54 2009 +0200
@@ -84,10 +84,10 @@
   val consts_program: theory -> string list -> string list * (naming * program)
   val cached_program: theory -> naming * program
   val eval_conv: theory
-    -> (term -> term * (naming -> program -> typscheme * iterm -> string list -> thm))
+    -> (term -> term) -> (term -> naming -> program -> typscheme * iterm -> string list -> thm)
     -> cterm -> thm
   val eval_term: theory
-    -> (term -> term * (naming -> program -> typscheme * iterm -> string list -> 'a))
+    -> (term -> term) -> (term -> naming -> program -> typscheme * iterm -> string list -> 'a)
     -> term -> 'a
 end;
 
@@ -733,14 +733,14 @@
     fun generate_consts thy algebra funcgr =
       fold_map (ensure_const thy algebra funcgr);
   in
-    invoke_generation thy (Code_Wellsorted.make thy cs) generate_consts cs
+    invoke_generation thy (Code_Wellsorted.obtain thy cs []) generate_consts cs
     |-> project_consts
   end;
 
 
 (* value evaluation *)
 
-fun ensure_value thy algbr funcgr t = 
+fun ensure_value thy algbr funcgr t =
   let
     val ty = fastype_of t;
     val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
@@ -766,18 +766,72 @@
     #> term_value
   end;
 
-fun eval thy evaluator t =
+fun eval thy evaluator raw_t algebra funcgr t =
+  let
+    val (((naming, program), (vs_ty_t, deps)), _) =
+      invoke_generation thy (algebra, funcgr) ensure_value t;
+  in evaluator raw_t naming program vs_ty_t deps end;
+
+fun eval_conv thy preproc = Code_Wellsorted.eval_conv thy preproc o eval thy;
+fun eval_term thy preproc = Code_Wellsorted.eval_term thy preproc o eval thy;
+
+
+(** diagnostic commands **)
+
+fun code_depgr thy consts =
+  let
+    val (_, eqngr) = Code_Wellsorted.obtain thy consts [];
+    val select = Graph.all_succs eqngr consts;
+  in
+    eqngr
+    |> not (null consts) ? Graph.subgraph (member (op =) select) 
+    |> Graph.map_nodes ((apsnd o map o apfst) (AxClass.overload thy))
+  end;
+
+fun code_thms thy = Pretty.writeln o Code_Wellsorted.pretty thy o code_depgr thy;
+
+fun code_deps thy consts =
   let
-    val (t', evaluator'') = evaluator t;
-    fun evaluator' algebra funcgr =
-      let
-        val (((naming, program), (vs_ty_t, deps)), _) =
-          invoke_generation thy (algebra, funcgr) ensure_value t';
-      in evaluator'' naming program vs_ty_t deps end;
-  in (t', evaluator') end
+    val eqngr = code_depgr thy consts;
+    val constss = Graph.strong_conn eqngr;
+    val mapping = Symtab.empty |> fold (fn consts => fold (fn const =>
+      Symtab.update (const, consts)) consts) constss;
+    fun succs consts = consts
+      |> maps (Graph.imm_succs eqngr)
+      |> subtract (op =) consts
+      |> map (the o Symtab.lookup mapping)
+      |> distinct (op =);
+    val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
+    fun namify consts = map (Code_Unit.string_of_const thy) consts
+      |> commas;
+    val prgr = map (fn (consts, constss) =>
+      { name = namify consts, ID = namify consts, dir = "", unfold = true,
+        path = "", parents = map namify constss }) conn;
+  in Present.display_graph prgr end;
+
+local
 
-fun eval_conv thy = Code_Wellsorted.eval_conv thy o eval thy;
-fun eval_term thy = Code_Wellsorted.eval_term thy o eval thy;
+structure P = OuterParse
+and K = OuterKeyword
+
+fun code_thms_cmd thy = code_thms thy o op @ o Code_Name.read_const_exprs thy;
+fun code_deps_cmd thy = code_deps thy o op @ o Code_Name.read_const_exprs thy;
+
+in
+
+val _ =
+  OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag
+    (Scan.repeat P.term_group
+      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
+        o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
+
+val _ =
+  OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag
+    (Scan.repeat P.term_group
+      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
+        o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
+
+end;
 
 end; (*struct*)
 
diff -r 705bb15b2365 -r 1e246776f876 src/Tools/code/code_wellsorted.ML
--- a/src/Tools/code/code_wellsorted.ML	Fri Apr 17 08:34:53 2009 +0200
+++ b/src/Tools/code/code_wellsorted.ML	Fri Apr 17 08:34:54 2009 +0200
@@ -12,12 +12,13 @@
   val typ: T -> string -> (string * sort) list * typ
   val all: T -> string list
   val pretty: theory -> T -> Pretty.T
-  val make: theory -> string list
-    -> ((sort -> sort) * Sorts.algebra) * T
+  val obtain: theory -> string list -> term list -> ((sort -> sort) * Sorts.algebra) * T
+  val preprocess: theory -> cterm list -> (cterm * (thm -> thm)) list
+  val preprocess_term: theory -> term list -> (term * (term -> term)) list
   val eval_conv: theory
-    -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> thm)) -> cterm -> thm
+    -> (term -> term) -> (term -> (sort -> sort) * Sorts.algebra -> T -> term -> thm) -> cterm -> thm
   val eval_term: theory
-    -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> 'a)) -> term -> 'a
+    -> (term -> term) -> (term -> (sort -> sort) * Sorts.algebra -> T -> term -> 'a) -> term -> 'a
 end
 
 structure Code_Wellsorted : CODE_WELLSORTED =
@@ -47,8 +48,10 @@
 
 (* auxiliary *)
 
+fun is_proper_class thy = can (AxClass.get_info thy);
+
 fun complete_proper_sort thy =
-  Sign.complete_sort thy #> filter (can (AxClass.get_info thy));
+  Sign.complete_sort thy #> filter (is_proper_class thy);
 
 fun inst_params thy tyco =
   map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
@@ -232,8 +235,7 @@
     ((class, tyco), map (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k))
       (0 upto Sign.arity_number thy tyco - 1));
 
-fun add_eqs thy (proj_sort, algebra) vardeps
-    (c, (proto_lhs, proto_eqns)) (rhss, eqngr) =
+fun add_eqs thy vardeps (c, (proto_lhs, proto_eqns)) (rhss, eqngr) =
   if can (Graph.get_node eqngr) c then (rhss, eqngr)
   else let
     val lhs = map_index (fn (k, (v, _)) =>
@@ -246,68 +248,26 @@
     val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr;
   in (map (pair c) rhss' @ rhss, eqngr') end;
 
-fun extend_arities_eqngr thy cs cs_rhss (arities, eqngr) =
+fun extend_arities_eqngr thy cs ts (arities, eqngr) =
   let
-    val cs_rhss' = (map o apsnd o map) (styp_of NONE) cs_rhss;
+    val cs_rhss = (fold o fold_aterms) (fn Const (c_ty as (c, _)) =>
+      insert (op =) (c, (map (styp_of NONE) o Sign.const_typargs thy) c_ty) | _ => I) ts [];
     val (vardeps, (eqntab, insts)) = empty_vardeps_data
       |> fold (assert_fun thy arities eqngr) cs
-      |> fold (assert_rhs thy arities eqngr) cs_rhss';
+      |> fold (assert_rhs thy arities eqngr) cs_rhss;
     val arities' = fold (add_arity thy vardeps) insts arities;
     val pp = Syntax.pp_global thy;
-    val is_proper_class = can (AxClass.get_info thy);
-    val (proj_sort, algebra) = Sorts.subalgebra pp is_proper_class
+    val algebra = Sorts.subalgebra pp (is_proper_class thy)
       (AList.lookup (op =) arities') (Sign.classes_of thy);
-    val (rhss, eqngr') = Symtab.fold
-      (add_eqs thy (proj_sort, algebra) vardeps) eqntab ([], eqngr);
-    fun deps_of (c, rhs) = c ::
-      maps (dicts_of thy (proj_sort, algebra))
-        (rhs ~~ (map snd o fst o fst o Graph.get_node eqngr') c);
+    val (rhss, eqngr') = Symtab.fold (add_eqs thy vardeps) eqntab ([], eqngr);
+    fun deps_of (c, rhs) = c :: maps (dicts_of thy algebra)
+      (rhs ~~ (map snd o fst o fst o Graph.get_node eqngr') c);
     val eqngr'' = fold (fn (c, rhs) => fold
       (curry Graph.add_edge c) (deps_of rhs)) rhss eqngr';
-  in ((proj_sort, algebra), (arities', eqngr'')) end;
+  in (algebra, (arities', eqngr'')) end;
 
 
-(** retrieval interfaces **)
-
-fun proto_eval thy cterm_of evaluator_lift evaluator proto_ct arities_eqngr =
-  let
-    val ct = cterm_of proto_ct;
-    val _ = Sign.no_vars (Syntax.pp_global thy) (Thm.term_of ct);
-    val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
-    fun consts_of t =
-      fold_aterms (fn Const c_ty => cons c_ty | _ => I) t [];
-    val thm = Code.preprocess_conv thy ct;
-    val ct' = Thm.rhs_of thm;
-    val t' = Thm.term_of ct';
-    val (t'', evaluator_eqngr) = evaluator t';
-    val consts = map fst (consts_of t');
-    val consts' = consts_of t'';
-    val const_matches' = fold (fn (c, ty) =>
-      insert (op =) (c, Sign.const_typargs thy (c, ty))) consts' [];
-    val (algebra', arities_eqngr') =
-      extend_arities_eqngr thy consts const_matches' arities_eqngr;
-  in
-    (evaluator_lift (evaluator_eqngr algebra') thm (snd arities_eqngr'),
-      arities_eqngr')
-  end;
-
-fun proto_eval_conv thy =
-  let
-    fun evaluator_lift evaluator thm1 eqngr =
-      let
-        val thm2 = evaluator eqngr;
-        val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2);
-      in
-        Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
-          error ("could not construct evaluation proof:\n"
-          ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
-      end;
-  in proto_eval thy I evaluator_lift end;
-
-fun proto_eval_term thy =
-  let
-    fun evaluator_lift evaluator _ eqngr = evaluator eqngr;
-  in proto_eval thy (Thm.cterm_of thy) evaluator_lift end;
+(** store **)
 
 structure Wellsorted = CodeDataFun
 (
@@ -327,71 +287,62 @@
     in (arities', eqngr') end;
 );
 
-fun make thy cs = apsnd snd
-  (Wellsorted.change_yield thy (extend_arities_eqngr thy cs []));
 
-fun eval_conv thy f =
-  fst o Wellsorted.change_yield thy o proto_eval_conv thy f;
+(** retrieval interfaces **)
 
-fun eval_term thy f =
-  fst o Wellsorted.change_yield thy o proto_eval_term thy f;
-
-
-(** diagnostic commands **)
+fun obtain thy cs ts = apsnd snd
+  (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts));
 
-fun code_depgr thy consts =
+fun preprocess thy cts =
   let
-    val (_, eqngr) = make thy consts;
-    val select = Graph.all_succs eqngr consts;
-  in
-    eqngr
-    |> not (null consts) ? Graph.subgraph (member (op =) select) 
-    |> Graph.map_nodes ((apsnd o map o apfst) (AxClass.overload thy))
-  end;
+    val ts = map Thm.term_of cts;
+    val _ = map
+      (Sign.no_vars (Syntax.pp_global thy) o Term.map_types Type.no_tvars) ts;
+    fun make thm1 = (Thm.rhs_of thm1, fn thm2 =>
+      let
+        val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2);
+      in
+        Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
+          error ("could not construct evaluation proof:\n"
+          ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
+      end);
+  in map (make o Code.preprocess_conv thy) cts end;
 
-fun code_thms thy = Pretty.writeln o pretty thy o code_depgr thy;
-
-fun code_deps thy consts =
+fun preprocess_term thy ts =
   let
-    val eqngr = code_depgr thy consts;
-    val constss = Graph.strong_conn eqngr;
-    val mapping = Symtab.empty |> fold (fn consts => fold (fn const =>
-      Symtab.update (const, consts)) consts) constss;
-    fun succs consts = consts
-      |> maps (Graph.imm_succs eqngr)
-      |> subtract (op =) consts
-      |> map (the o Symtab.lookup mapping)
-      |> distinct (op =);
-    val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
-    fun namify consts = map (Code_Unit.string_of_const thy) consts
-      |> commas;
-    val prgr = map (fn (consts, constss) =>
-      { name = namify consts, ID = namify consts, dir = "", unfold = true,
-        path = "", parents = map namify constss }) conn;
-  in Present.display_graph prgr end;
+    val cts = map (Thm.cterm_of thy) ts;
+    val postprocess = Code.postprocess_term thy;
+  in map (fn (ct, _) => (Thm.term_of ct, postprocess)) (preprocess thy cts) end;
 
-local
+(*FIXME rearrange here*)
 
-structure P = OuterParse
-and K = OuterKeyword
-
-fun code_thms_cmd thy = code_thms thy o op @ o Code_Name.read_const_exprs thy;
-fun code_deps_cmd thy = code_deps thy o op @ o Code_Name.read_const_exprs thy;
-
-in
+fun proto_eval thy cterm_of evaluator_lift preproc evaluator proto_ct =
+  let
+    val ct = cterm_of proto_ct;
+    val _ = Sign.no_vars (Syntax.pp_global thy) (Thm.term_of ct);
+    val _ = Term.map_types Type.no_tvars (Thm.term_of ct);
+    fun consts_of t =
+      fold_aterms (fn Const c_ty => cons c_ty | _ => I) t [];
+    val thm = Code.preprocess_conv thy ct;
+    val ct' = Thm.rhs_of thm;
+    val t' = Thm.term_of ct';
+    val consts = map fst (consts_of t');
+    val t'' = preproc t';
+    val (algebra', eqngr') = obtain thy consts [t''];
+  in evaluator_lift (evaluator t' algebra' eqngr' t'') thm end;
 
-val _ =
-  OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag
-    (Scan.repeat P.term_group
-      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
-        o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
+fun eval_conv thy =
+  let
+    fun evaluator_lift thm2 thm1 =
+      let
+        val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2);
+      in
+        Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
+          error ("could not construct evaluation proof:\n"
+          ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
+      end;
+  in proto_eval thy I evaluator_lift end;
 
-val _ =
-  OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag
-    (Scan.repeat P.term_group
-      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
-        o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
-
-end;
+fun eval_term thy = proto_eval thy (Thm.cterm_of thy) (fn t => K t);
 
 end; (*struct*)
diff -r 705bb15b2365 -r 1e246776f876 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Fri Apr 17 08:34:53 2009 +0200
+++ b/src/Tools/nbe.ML	Fri Apr 17 08:34:54 2009 +0200
@@ -431,7 +431,7 @@
 
 (* evaluation with type reconstruction *)
 
-fun eval thy t naming program vs_ty_t deps =
+fun norm thy t naming program vs_ty_t deps =
   let
     fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty)
       | t => t);
@@ -463,10 +463,6 @@
 
 (* evaluation oracle *)
 
-val (_, norm_oracle) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (Binding.name "norm", fn (thy, t, naming, program, vs_ty_t, deps) =>
-    Thm.cterm_of thy (Logic.mk_equals (t, eval thy t naming program vs_ty_t deps)))));
-
 fun add_triv_classes thy =
   let
     val inters = curry (Sorts.inter_sort (Sign.classes_of thy))
@@ -476,19 +472,20 @@
         | TFree (v, sort) => TFree (v, f sort));
   in map_sorts inters end;
 
+val (_, raw_norm_oracle) = Context.>>> (Context.map_theory_result
+  (Thm.add_oracle (Binding.name "norm", fn (thy, t, naming, program, vs_ty_t, deps) =>
+    Thm.cterm_of thy (Logic.mk_equals (t, norm thy t naming program vs_ty_t deps)))));
+
+fun norm_oracle thy t naming program vs_ty_t deps =
+  raw_norm_oracle (thy, t, naming, program, vs_ty_t, deps);
+
 fun norm_conv ct =
   let
     val thy = Thm.theory_of_cterm ct;
-    fun evaluator' t naming program vs_ty_t deps =
-      norm_oracle (thy, t, naming, program, vs_ty_t, deps);
-    fun evaluator t = (add_triv_classes thy t, evaluator' t);
-  in Code_Thingol.eval_conv thy evaluator ct end;
+  in Code_Thingol.eval_conv thy (add_triv_classes thy) (norm_oracle thy) ct end;
 
-fun norm_term thy t =
-  let
-    fun evaluator' t naming program vs_ty_t deps = eval thy t naming program vs_ty_t deps;
-    fun evaluator t = (add_triv_classes thy t, evaluator' t);
-  in (Code.postprocess_term thy o Code_Thingol.eval_term thy evaluator) t end;
+fun norm_term thy = Code.postprocess_term thy
+  o Code_Thingol.eval_term thy (add_triv_classes thy) (norm thy);
 
 (* evaluation command *)