src/Tools/code/code_wellsorted.ML
author haftmann
Fri, 20 Feb 2009 10:14:32 +0100
changeset 30010 862fc7751a15
child 30024 5e9d471afef3
permissions -rw-r--r--
tuned and incremental version of wellsorting algorithm
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30010
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
     1
(*  Title:      Tools/code/code_wellsorted.ML
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
     2
    Author:     Florian Haftmann, TU Muenchen
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
     3
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
     4
Retrieving, well-sorting and structuring code equations in graph
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
     5
with explicit dependencies -- the Waisenhaus algorithm.
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
     6
*)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
     7
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
     8
signature CODE_FUNCGR =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
     9
sig
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    10
  type T
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    11
  val eqns: T -> string -> (thm * bool) list
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    12
  val typ: T -> string -> (string * sort) list * typ
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    13
  val all: T -> string list
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    14
  val pretty: theory -> T -> Pretty.T
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    15
  val make: theory -> string list
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    16
    -> ((sort -> sort) * Sorts.algebra) * T
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    17
  val eval_conv: theory
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    18
    -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> thm)) -> cterm -> thm
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    19
  val eval_term: theory
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    20
    -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> 'a)) -> term -> 'a
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    21
end
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    22
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    23
structure Code_Funcgr : CODE_FUNCGR =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    24
struct
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    25
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    26
(** the equation graph type **)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    27
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    28
type T = (((string * sort) list * typ) * (thm * bool) list) Graph.T;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    29
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    30
fun eqns eqngr = these o Option.map snd o try (Graph.get_node eqngr);
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    31
fun typ eqngr = fst o Graph.get_node eqngr;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    32
fun all eqngr = Graph.keys eqngr;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    33
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    34
fun pretty thy eqngr =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    35
  AList.make (snd o Graph.get_node eqngr) (Graph.keys eqngr)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    36
  |> (map o apfst) (Code_Unit.string_of_const thy)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    37
  |> sort (string_ord o pairself fst)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    38
  |> map (fn (s, thms) =>
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    39
       (Pretty.block o Pretty.fbreaks) (
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    40
         Pretty.str s
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    41
         :: map (Display.pretty_thm o fst) thms
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    42
       ))
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    43
  |> Pretty.chunks;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    44
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    45
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    46
(** the Waisenhaus algorithm **)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    47
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    48
(* auxiliary *)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    49
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    50
fun complete_proper_sort thy =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    51
  Sign.complete_sort thy #> filter (can (AxClass.get_info thy));
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    52
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    53
fun inst_params thy tyco class =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    54
  map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    55
    ((#params o AxClass.get_info thy) class);
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    56
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    57
fun consts_of thy eqns = [] |> (fold o fold o fold_aterms)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    58
  (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    59
    (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns);
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    60
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    61
fun tyscm_rhss_of thy c eqns =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    62
  let
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    63
    val tyscm = case eqns of [] => Code.default_typscheme thy c
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    64
      | ((thm, _) :: _) => (snd o Code_Unit.head_eqn thy) thm;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    65
    val rhss = consts_of thy eqns;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    66
  in (tyscm, rhss) end;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    67
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    68
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    69
(* data structures *)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    70
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    71
datatype const = Fun of string | Inst of class * string;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    72
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    73
fun const_ord (Fun c1, Fun c2) = fast_string_ord (c1, c2)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    74
  | const_ord (Inst class_tyco1, Inst class_tyco2) =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    75
      prod_ord fast_string_ord fast_string_ord (class_tyco1, class_tyco2)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    76
  | const_ord (Fun _, Inst _) = LESS
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    77
  | const_ord (Inst _, Fun _) = GREATER;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    78
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    79
type var = const * int;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    80
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    81
structure Vargraph =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    82
  GraphFun(type key = var val ord = prod_ord const_ord int_ord);
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    83
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    84
datatype styp = Tyco of string * styp list | Var of var;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    85
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    86
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    87
(* computing instantiations *)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    88
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    89
fun obtain_eqns thy eqngr c =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    90
  case try (Graph.get_node eqngr) c
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    91
   of SOME ((lhs, _), eqns) => ((lhs, []), eqns)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    92
    | NONE => let
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    93
        val eqns = Code.these_eqns thy c
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    94
          |> burrow_fst (Code_Unit.norm_args thy)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    95
          |> burrow_fst (Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var);
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    96
        val ((lhs, _), rhss) = tyscm_rhss_of thy c eqns;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    97
      in ((lhs, rhss), eqns) end;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    98
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
    99
fun obtain_instance thy arities (inst as (class, tyco)) =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   100
  case AList.lookup (op =) arities inst
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   101
   of SOME classess => (classess, ([], []))
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   102
    | NONE => let
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   103
        val classess = map (complete_proper_sort thy)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   104
          (Sign.arity_sorts thy tyco [class]);
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   105
        val superclasses = [class]
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   106
          |> complete_proper_sort thy
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   107
          |> remove (op =) class;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   108
        val inst_params = inst_params thy tyco class;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   109
      in (classess, (superclasses, inst_params)) end;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   110
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   111
fun add_classes thy arities eqngr c_k new_classes vardeps_data =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   112
  let
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   113
    val (styps, old_classes) = Vargraph.get_node (fst vardeps_data) c_k;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   114
    val diff_classes = new_classes |> subtract (op =) old_classes;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   115
  in if null diff_classes then vardeps_data
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   116
  else let
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   117
    val c_ks = Vargraph.imm_succs (fst vardeps_data) c_k |> insert (op =) c_k;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   118
  in
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   119
    vardeps_data
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   120
    |> (apfst o Vargraph.map_node c_k o apsnd) (append diff_classes)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   121
    |> fold (fn styp => fold (add_typmatch_inst thy arities eqngr styp) new_classes) styps
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   122
    |> fold (fn c_k => add_classes thy arities eqngr c_k diff_classes) c_ks
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   123
  end end
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   124
and add_styp thy arities eqngr c_k tyco_styps vardeps_data =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   125
  let
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   126
    val (old_styps, classes) = Vargraph.get_node (fst vardeps_data) c_k;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   127
  in if member (op =) old_styps tyco_styps then vardeps_data
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   128
  else
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   129
    vardeps_data
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   130
    |> (apfst o Vargraph.map_node c_k o apfst) (cons tyco_styps)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   131
    |> fold (add_typmatch_inst thy arities eqngr tyco_styps) classes
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   132
  end
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   133
and add_dep thy arities eqngr c_k c_k' vardeps_data =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   134
  let
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   135
    val (_, classes) = Vargraph.get_node (fst vardeps_data) c_k;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   136
  in
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   137
    vardeps_data
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   138
    |> add_classes thy arities eqngr c_k' classes
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   139
    |> apfst (Vargraph.add_edge (c_k, c_k'))
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   140
  end
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   141
and add_typmatch_inst thy arities eqngr (tyco, styps) class vardeps_data =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   142
  if can (Sign.arity_sorts thy tyco) [class]
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   143
  then vardeps_data
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   144
    |> assert thy arities eqngr (Inst (class, tyco))
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   145
    |> fold_index (fn (k, styp) =>
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   146
         add_typmatch thy arities eqngr styp (Inst (class, tyco), k)) styps
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   147
  else vardeps_data (*permissive!*)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   148
and add_typmatch thy arities eqngr (Var c_k') c_k vardeps_data =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   149
      vardeps_data
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   150
      |> add_dep thy arities eqngr c_k c_k'
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   151
  | add_typmatch thy arities eqngr (Tyco tyco_styps) c_k vardeps_data =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   152
      vardeps_data
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   153
      |> add_styp thy arities eqngr c_k tyco_styps
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   154
and add_inst thy arities eqngr (inst as (class, tyco)) vardeps_data =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   155
  let
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   156
    val (classess, (superclasses, inst_params)) =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   157
      obtain_instance thy arities inst;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   158
  in
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   159
    vardeps_data
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   160
    |> fold (fn superclass => assert thy arities eqngr (Inst (superclass, tyco))) superclasses
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   161
    |> fold (assert thy arities eqngr o Fun) inst_params
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   162
    |> fold_index (fn (k, classes) =>
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   163
         apfst (Vargraph.new_node ((Inst (class, tyco), k), ([] ,[])))
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   164
         #> add_classes thy arities eqngr (Inst (class, tyco), k) classes
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   165
         #> fold (fn superclass =>
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   166
             add_dep thy arities eqngr (Inst (superclass, tyco), k)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   167
             (Inst (class, tyco), k)) superclasses
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   168
         #> fold (fn inst_param =>
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   169
             add_dep thy arities eqngr (Fun inst_param, k)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   170
             (Inst (class, tyco), k)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   171
             ) inst_params
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   172
         ) classess
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   173
  end
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   174
and add_const thy arities eqngr c vardeps_data =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   175
  let
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   176
    val ((lhs, rhss), eqns) = obtain_eqns thy eqngr c;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   177
    fun styp_of (Type (tyco, tys)) = Tyco (tyco, map styp_of tys)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   178
      | styp_of (TFree (v, _)) = Var (Fun c, find_index (fn (v', _) => v = v') lhs);
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   179
    val rhss' = (map o apsnd o map) styp_of rhss;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   180
  in
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   181
    vardeps_data
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   182
    |> (apsnd o apsnd) (Symtab.update_new (c, (lhs, eqns)))
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   183
    |> fold_index (fn (k, (_, sort)) =>
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   184
         apfst (Vargraph.new_node ((Fun c, k), ([] ,[])))
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   185
         #> add_classes thy arities eqngr (Fun c, k) (complete_proper_sort thy sort)) lhs
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   186
    |> fold (assert thy arities eqngr o Fun o fst) rhss'
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   187
    |> fold (fn (c', styps) => fold_index (fn (k', styp) =>
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   188
         add_typmatch thy arities eqngr styp (Fun c', k')) styps) rhss'
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   189
  end
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   190
and assert thy arities eqngr c vardeps_data =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   191
  if member (op =) ((fst o snd) vardeps_data) c then vardeps_data
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   192
  else case c
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   193
   of Fun const => vardeps_data |> (apsnd o apfst) (cons c) |> add_const thy arities eqngr const
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   194
    | Inst inst => vardeps_data |> (apsnd o apfst) (cons c) |> add_inst thy arities eqngr inst;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   195
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   196
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   197
(* applying instantiations *)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   198
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   199
fun build_algebra thy arities =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   200
  let
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   201
    val pp = Syntax.pp_global thy;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   202
    val thy_algebra = Sign.classes_of thy;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   203
    val is_proper = can (AxClass.get_info thy);
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   204
    val classrels = Sorts.classrels_of thy_algebra
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   205
      |> filter (is_proper o fst)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   206
      |> (map o apsnd) (filter is_proper);
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   207
    val instances = Sorts.instances_of thy_algebra
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   208
      |> filter (is_proper o snd);
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   209
    fun add_class (class, superclasses) algebra =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   210
      Sorts.add_class pp (class, Sorts.minimize_sort algebra superclasses) algebra;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   211
    fun add_arity (tyco, class) algebra =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   212
      case AList.lookup (op =) arities (tyco, class)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   213
       of SOME sorts => Sorts.add_arities pp
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   214
            (tyco, [(class, map (Sorts.minimize_sort algebra) sorts)]) algebra
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   215
        | NONE => if Sign.arity_number thy tyco = 0
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   216
            then Sorts.add_arities pp (tyco, [(class, [])]) algebra
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   217
            else algebra;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   218
  in
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   219
    Sorts.empty_algebra
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   220
    |> fold add_class classrels
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   221
    |> fold add_arity instances
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   222
  end;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   223
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   224
fun dicts_of thy (proj_sort, algebra) (T, sort) =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   225
  let
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   226
    fun class_relation (x, _) _ = x;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   227
    fun type_constructor tyco xs class =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   228
      inst_params thy tyco class @ (maps o maps) fst xs;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   229
    fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   230
  in
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   231
    flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   232
      { class_relation = class_relation, type_constructor = type_constructor,
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   233
        type_variable = type_variable } (T, proj_sort sort)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   234
       handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   235
  end;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   236
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   237
fun add_arities thy vardeps = Vargraph.fold (fn ((Fun _, _), _) => I
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   238
  | ((Inst (class, tyco), k), ((_, classes), _)) =>
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   239
      AList.map_default (op =)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   240
        ((tyco, class), replicate (Sign.arity_number thy tyco) [])
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   241
          (nth_map k (K classes))) vardeps;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   242
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   243
fun add_eqs thy (proj_sort, algebra) eqntab vardeps c gr =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   244
  let
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   245
    val (proto_lhs, proto_eqns) = (the o Symtab.lookup eqntab) c;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   246
    val lhs = map_index (fn (k, (v, _)) =>
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   247
      (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   248
    val inst_tab = Vartab.empty |> fold (fn (v, sort) =>
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   249
      Vartab.update ((v, 0), sort)) lhs;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   250
    val eqns = proto_eqns
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   251
      |> (map o apfst) (Code_Unit.inst_thm thy inst_tab);
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   252
    val (tyscm, rhss) = tyscm_rhss_of thy c eqns;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   253
  in
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   254
    gr
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   255
    |> Graph.new_node (c, (tyscm, eqns))
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   256
    |> fold (fn (c', Ts) => ensure_eqs_dep thy (proj_sort, algebra) eqntab vardeps c c'
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   257
        #-> (fn (vs, _) =>
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   258
          fold2 (ensure_match thy (proj_sort, algebra) eqntab vardeps c) Ts (map snd vs))) rhss
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   259
    |> pair tyscm
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   260
  end
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   261
and ensure_match thy (proj_sort, algebra) eqntab vardeps c T sort gr =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   262
  gr
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   263
  |> fold (fn c' => ensure_eqs_dep thy (proj_sort, algebra) eqntab vardeps c c' #> snd)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   264
       (dicts_of thy (proj_sort, algebra) (T, proj_sort sort))
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   265
and ensure_eqs_dep thy (proj_sort, algebra) eqntab vardeps c c' gr =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   266
  gr
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   267
  |> ensure_eqs thy (proj_sort, algebra) eqntab vardeps c'
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   268
  ||> Graph.add_edge (c, c')
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   269
and ensure_eqs thy (proj_sort, algebra) eqntab vardeps c gr =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   270
  case try (Graph.get_node gr) c
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   271
   of SOME (tyscm, _) => (tyscm, gr)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   272
    | NONE => add_eqs thy (proj_sort, algebra) eqntab vardeps c gr;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   273
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   274
fun extend_arities_eqngr thy cs (arities, eqngr) =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   275
  let
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   276
    val (vardeps, (_, eqntab)) = fold (assert thy arities eqngr o Fun)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   277
      cs (Vargraph.empty, ([], Symtab.empty));
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   278
    val arities' = add_arities thy vardeps arities;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   279
    val algebra = build_algebra thy arities';
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   280
    val proj_sort = complete_proper_sort thy #> Sorts.minimize_sort algebra;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   281
    val (_, eqngr') = fold_map (ensure_eqs thy (proj_sort, algebra) eqntab vardeps) cs eqngr;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   282
  in ((proj_sort, algebra), (arities', eqngr')) end;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   283
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   284
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   285
(** retrieval interfaces **)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   286
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   287
fun proto_eval thy cterm_of evaluator_lift evaluator proto_ct arities_eqngr =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   288
  let
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   289
    val ct = cterm_of proto_ct;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   290
    val _ = Sign.no_vars (Syntax.pp_global thy) (Thm.term_of ct);
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   291
    val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   292
    fun consts_of t =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   293
      fold_aterms (fn Const c_ty => cons c_ty | _ => I) t [];
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   294
    val thm = Code.preprocess_conv thy ct;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   295
    val ct' = Thm.rhs_of thm;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   296
    val t' = Thm.term_of ct';
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   297
    val consts = map fst (consts_of t');
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   298
    val (algebra', arities_eqngr') = extend_arities_eqngr thy consts arities_eqngr;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   299
    val (t'', evaluator_eqngr) = evaluator t';
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   300
    val consts' = consts_of t'';
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   301
    val const_matches = fold (fn (c, ty) =>
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   302
      insert (op =) (Sign.const_typargs thy (c, Logic.unvarifyT ty), c)) consts' [];
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   303
    val typ_matches = maps (fn (tys, c) =>
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   304
      tys ~~ map snd (fst (fst (Graph.get_node (snd arities_eqngr') c))))
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   305
      const_matches;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   306
    val dicts = maps (dicts_of thy algebra') typ_matches;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   307
    val (algebra'', arities_eqngr'') = extend_arities_eqngr thy dicts arities_eqngr';
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   308
  in (evaluator_lift (evaluator_eqngr algebra'') thm (snd arities_eqngr''), arities_eqngr'') end;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   309
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   310
fun proto_eval_conv thy =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   311
  let
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   312
    fun evaluator_lift evaluator thm1 eqngr =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   313
      let
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   314
        val thm2 = evaluator eqngr;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   315
        val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2);
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   316
      in
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   317
        Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   318
          error ("could not construct evaluation proof:\n"
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   319
          ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   320
      end;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   321
  in proto_eval thy I evaluator_lift end;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   322
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   323
fun proto_eval_term thy =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   324
  let
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   325
    fun evaluator_lift evaluator _ eqngr = evaluator eqngr;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   326
  in proto_eval thy (Thm.cterm_of thy) evaluator_lift end;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   327
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   328
structure Wellsorted = CodeDataFun
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   329
(
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   330
  type T = ((string * class) * sort list) list * T;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   331
  val empty = ([], Graph.empty);
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   332
  fun purge thy cs (arities, eqngr) =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   333
    let
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   334
      val del_cs = ((Graph.all_preds eqngr
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   335
        o filter (can (Graph.get_node eqngr))) cs);
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   336
      val del_arities =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   337
        map_filter (AxClass.inst_of_param thy) del_cs;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   338
      val arities' = fold (AList.delete (op =)) del_arities arities;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   339
      val eqngr' = Graph.del_nodes del_cs eqngr;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   340
    in (arities', eqngr') end;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   341
);
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   342
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   343
fun make thy = apsnd snd
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   344
  o Wellsorted.change_yield thy o extend_arities_eqngr thy;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   345
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   346
fun eval_conv thy f =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   347
  fst o Wellsorted.change_yield thy o proto_eval_conv thy f;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   348
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   349
fun eval_term thy f =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   350
  fst o Wellsorted.change_yield thy o proto_eval_term thy f;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   351
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   352
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   353
(** diagnostic commands **)
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   354
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   355
fun code_depgr thy consts =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   356
  let
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   357
    val (_, eqngr) = make thy consts;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   358
    val select = Graph.all_succs eqngr consts;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   359
  in
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   360
    eqngr
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   361
    |> not (null consts) ? Graph.subgraph (member (op =) select) 
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   362
    |> Graph.map_nodes ((apsnd o map o apfst) (AxClass.overload thy))
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   363
  end;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   364
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   365
fun code_thms thy = Pretty.writeln o pretty thy o code_depgr thy;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   366
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   367
fun code_deps thy consts =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   368
  let
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   369
    val eqngr = code_depgr thy consts;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   370
    fun mk_entry (const, (_, (_, parents))) =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   371
      let
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   372
        val name = Code_Unit.string_of_const thy const;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   373
        val nameparents = map (Code_Unit.string_of_const thy) parents;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   374
      in { name = name, ID = name, dir = "", unfold = true,
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   375
        path = "", parents = nameparents }
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   376
      end;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   377
    val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) eqngr [];
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   378
  in Present.display_graph prgr end;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   379
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   380
local
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   381
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   382
structure P = OuterParse
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   383
and K = OuterKeyword
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   384
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   385
fun code_thms_cmd thy = code_thms thy o op @ o Code_Name.read_const_exprs thy;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   386
fun code_deps_cmd thy = code_deps thy o op @ o Code_Name.read_const_exprs thy;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   387
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   388
in
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   389
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   390
val _ =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   391
  OuterSyntax.improper_command "code_thms" "print system of defining equations for code" OuterKeyword.diag
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   392
    (Scan.repeat P.term_group
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   393
      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   394
        o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   395
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   396
val _ =
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   397
  OuterSyntax.improper_command "code_deps" "visualize dependencies of defining equations for code" OuterKeyword.diag
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   398
    (Scan.repeat P.term_group
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   399
      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   400
        o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   401
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   402
end;
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   403
862fc7751a15 tuned and incremental version of wellsorting algorithm
haftmann
parents:
diff changeset
   404
end; (*struct*)