1.1 --- a/src/Tools/code/code_funcgr.ML	Tue Jun 10 15:30:01 2008 +0200
     1.2 +++ b/src/Tools/code/code_funcgr.ML	Tue Jun 10 15:30:06 2008 +0200
     1.3 @@ -14,7 +14,6 @@
     1.4    val all: T -> string list
     1.5    val pretty: theory -> T -> Pretty.T
     1.6    val make: theory -> string list -> T
     1.7 -  val make_consts: theory -> string list -> string list * T
     1.8    val eval_conv: theory -> (term -> term * (T -> term -> thm)) -> cterm -> thm
     1.9    val eval_term: theory -> (term -> term * (T -> term -> 'a)) -> term -> 'a
    1.10    val timing: bool ref
    1.11 @@ -219,12 +218,6 @@
    1.12  
    1.13  val ensure_consts = ensure_consts;
    1.14  
    1.15 -fun check_consts thy consts funcgr =
    1.16 -  let
    1.17 -    val algebra = Code.coregular_algebra thy;
    1.18 -    fun try_const const funcgr = (const, ensure_consts thy algebra [const] funcgr);
    1.19 -  in fold_map try_const consts funcgr end;
    1.20 -
    1.21  fun proto_eval thy cterm_of evaluator_fr evaluator proto_ct funcgr =
    1.22    let
    1.23      val ct = cterm_of proto_ct;
    1.24 @@ -278,13 +271,63 @@
    1.25  fun make thy =
    1.26    Funcgr.change thy o ensure_consts thy (Code.coregular_algebra thy);
    1.27  
    1.28 -fun make_consts thy =
    1.29 -  Funcgr.change_yield thy o check_consts thy;
    1.30 -
    1.31  fun eval_conv thy f =
    1.32    fst o Funcgr.change_yield thy o proto_eval_conv thy f;
    1.33  
    1.34  fun eval_term thy f =
    1.35    fst o Funcgr.change_yield thy o proto_eval_term thy f;
    1.36  
    1.37 +
    1.38 +(** diagnostic commands **)
    1.39 +
    1.40 +fun code_depgr thy [] = make thy []
    1.41 +  | code_depgr thy consts =
    1.42 +      let
    1.43 +        val gr = make thy consts;
    1.44 +        val select = Graph.all_succs gr consts;
    1.45 +      in
    1.46 +        gr
    1.47 +        |> Graph.subgraph (member (op =) select) 
    1.48 +        |> Graph.map_nodes ((apsnd o map) (AxClass.overload thy))
    1.49 +      end;
    1.50 +
    1.51 +fun code_thms thy = Pretty.writeln o pretty thy o code_depgr thy;
    1.52 +
    1.53 +fun code_deps thy consts =
    1.54 +  let
    1.55 +    val gr = code_depgr thy consts;
    1.56 +    fun mk_entry (const, (_, (_, parents))) =
    1.57 +      let
    1.58 +        val name = CodeUnit.string_of_const thy const;
    1.59 +        val nameparents = map (CodeUnit.string_of_const thy) parents;
    1.60 +      in { name = name, ID = name, dir = "", unfold = true,
    1.61 +        path = "", parents = nameparents }
    1.62 +      end;
    1.63 +    val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr [];
    1.64 +  in Present.display_graph prgr end;
    1.65 +
    1.66 +local
    1.67 +
    1.68 +structure P = OuterParse
    1.69 +and K = OuterKeyword
    1.70 +
    1.71 +fun code_thms_cmd thy = code_thms thy o op @ o CodeName.read_const_exprs thy;
    1.72 +fun code_deps_cmd thy = code_deps thy o op @ o CodeName.read_const_exprs thy;
    1.73 +
    1.74 +in
    1.75 +
    1.76 +val _ =
    1.77 +  OuterSyntax.improper_command "code_thms" "print system of defining equations for code" OuterKeyword.diag
    1.78 +    (Scan.repeat P.term
    1.79 +      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
    1.80 +        o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
    1.81 +
    1.82 +val _ =
    1.83 +  OuterSyntax.improper_command "code_deps" "visualize dependencies of defining equations for code" OuterKeyword.diag
    1.84 +    (Scan.repeat P.term
    1.85 +      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
    1.86 +        o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
    1.87 +
    1.88 +end;
    1.89 +
    1.90  end; (*struct*)