wrecked old code_funcgr module
authorhaftmann
Wed Apr 15 15:34:54 2009 +0200 (2009-04-15)
changeset 30927bc51b343f80d
parent 30926 3a30613aa469
child 30928 983dfcce45ad
wrecked old code_funcgr module
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/Tools/code/code_funcgr.ML
     1.1 --- a/src/HOL/HOL.thy	Wed Apr 15 15:34:00 2009 +0200
     1.2 +++ b/src/HOL/HOL.thy	Wed Apr 15 15:34:54 2009 +0200
     1.3 @@ -29,7 +29,6 @@
     1.4    ("~~/src/Tools/induct_tacs.ML")
     1.5    "~~/src/Tools/value.ML"
     1.6    "~~/src/Tools/code/code_name.ML"
     1.7 -  "~~/src/Tools/code/code_funcgr.ML" (*formal dependency*)
     1.8    "~~/src/Tools/code/code_wellsorted.ML" 
     1.9    "~~/src/Tools/code/code_thingol.ML"
    1.10    "~~/src/Tools/code/code_printer.ML"
     2.1 --- a/src/HOL/IsaMakefile	Wed Apr 15 15:34:00 2009 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Wed Apr 15 15:34:54 2009 +0200
     2.3 @@ -89,7 +89,6 @@
     2.4    $(SRC)/Tools/IsaPlanner/rw_tools.ML \
     2.5    $(SRC)/Tools/IsaPlanner/zipper.ML \
     2.6    $(SRC)/Tools/atomize_elim.ML \
     2.7 -  $(SRC)/Tools/code/code_funcgr.ML \
     2.8    $(SRC)/Tools/code/code_haskell.ML \
     2.9    $(SRC)/Tools/code/code_ml.ML \
    2.10    $(SRC)/Tools/code/code_name.ML \
     3.1 --- a/src/Tools/code/code_funcgr.ML	Wed Apr 15 15:34:00 2009 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,335 +0,0 @@
     3.4 -(*  Title:      Tools/code/code_funcgr.ML
     3.5 -    Author:     Florian Haftmann, TU Muenchen
     3.6 -
     3.7 -Retrieving, normalizing and structuring code equations in graph
     3.8 -with explicit dependencies.
     3.9 -
    3.10 -Legacy.  To be replaced by Tools/code/code_wellsorted.ML
    3.11 -*)
    3.12 -
    3.13 -signature CODE_WELLSORTED =
    3.14 -sig
    3.15 -  type T
    3.16 -  val eqns: T -> string -> (thm * bool) list
    3.17 -  val typ: T -> string -> (string * sort) list * typ
    3.18 -  val all: T -> string list
    3.19 -  val pretty: theory -> T -> Pretty.T
    3.20 -  val make: theory -> string list
    3.21 -    -> ((sort -> sort) * Sorts.algebra) * T
    3.22 -  val eval_conv: theory
    3.23 -    -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> thm)) -> cterm -> thm
    3.24 -  val eval_term: theory
    3.25 -    -> (term -> term * (((sort -> sort) * Sorts.algebra) -> T -> 'a)) -> term -> 'a
    3.26 -  val timing: bool ref
    3.27 -end
    3.28 -
    3.29 -structure Code_Wellsorted : CODE_WELLSORTED =
    3.30 -struct
    3.31 -
    3.32 -(** the graph type **)
    3.33 -
    3.34 -type T = (((string * sort) list * typ) * (thm * bool) list) Graph.T;
    3.35 -
    3.36 -fun eqns funcgr =
    3.37 -  these o Option.map snd o try (Graph.get_node funcgr);
    3.38 -
    3.39 -fun typ funcgr =
    3.40 -  fst o Graph.get_node funcgr;
    3.41 -
    3.42 -fun all funcgr = Graph.keys funcgr;
    3.43 -
    3.44 -fun pretty thy funcgr =
    3.45 -  AList.make (snd o Graph.get_node funcgr) (Graph.keys funcgr)
    3.46 -  |> (map o apfst) (Code_Unit.string_of_const thy)
    3.47 -  |> sort (string_ord o pairself fst)
    3.48 -  |> map (fn (s, thms) =>
    3.49 -       (Pretty.block o Pretty.fbreaks) (
    3.50 -         Pretty.str s
    3.51 -         :: map (Display.pretty_thm o fst) thms
    3.52 -       ))
    3.53 -  |> Pretty.chunks;
    3.54 -
    3.55 -
    3.56 -(** generic combinators **)
    3.57 -
    3.58 -fun fold_consts f thms =
    3.59 -  thms
    3.60 -  |> maps (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of)
    3.61 -  |> (fold o fold_aterms) (fn Const c => f c | _ => I);
    3.62 -
    3.63 -fun consts_of (const, []) = []
    3.64 -  | consts_of (const, thms as _ :: _) = 
    3.65 -      let
    3.66 -        fun the_const (c, _) = if c = const then I else insert (op =) c
    3.67 -      in fold_consts the_const (map fst thms) [] end;
    3.68 -
    3.69 -fun insts_of thy algebra tys sorts =
    3.70 -  let
    3.71 -    fun class_relation (x, _) _ = x;
    3.72 -    fun type_constructor tyco xs class =
    3.73 -      (tyco, class) :: (maps o maps) fst xs;
    3.74 -    fun type_variable (TVar (_, sort)) = map (pair []) sort
    3.75 -      | type_variable (TFree (_, sort)) = map (pair []) sort;
    3.76 -    fun of_sort_deriv ty sort =
    3.77 -      Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
    3.78 -        { class_relation = class_relation, type_constructor = type_constructor,
    3.79 -          type_variable = type_variable }
    3.80 -        (ty, sort) handle Sorts.CLASS_ERROR _ => [] (*permissive!*)
    3.81 -  in (flat o flat) (map2 of_sort_deriv tys sorts) end;
    3.82 -
    3.83 -fun meets_of thy algebra =
    3.84 -  let
    3.85 -    fun meet_of ty sort tab =
    3.86 -      Sorts.meet_sort algebra (ty, sort) tab
    3.87 -        handle Sorts.CLASS_ERROR _ => tab (*permissive!*);
    3.88 -  in fold2 meet_of end;
    3.89 -
    3.90 -
    3.91 -(** graph algorithm **)
    3.92 -
    3.93 -val timing = ref false;
    3.94 -
    3.95 -local
    3.96 -
    3.97 -fun resort_thms thy algebra typ_of thms =
    3.98 -  let
    3.99 -    val cs = fold_consts (insert (op =)) thms [];
   3.100 -    fun meets (c, ty) = case typ_of c
   3.101 -       of SOME (vs, _) =>
   3.102 -            meets_of thy algebra (Sign.const_typargs thy (c, ty)) (map snd vs)
   3.103 -        | NONE => I;
   3.104 -    val tab = fold meets cs Vartab.empty;
   3.105 -  in map (Code_Unit.inst_thm thy tab) thms end;
   3.106 -
   3.107 -fun resort_eqnss thy algebra funcgr =
   3.108 -  let
   3.109 -    val typ_funcgr = try (fst o Graph.get_node funcgr);
   3.110 -    val resort_dep = (apsnd o burrow_fst) (resort_thms thy algebra typ_funcgr);
   3.111 -    fun resort_rec typ_of (c, []) = (true, (c, []))
   3.112 -      | resort_rec typ_of (c, thms as (thm, _) :: _) = if is_some (AxClass.inst_of_param thy c)
   3.113 -          then (true, (c, thms))
   3.114 -          else let
   3.115 -            val (_, (vs, ty)) = Code_Unit.head_eqn thy thm;
   3.116 -            val thms' as (thm', _) :: _ = burrow_fst (resort_thms thy algebra typ_of) thms
   3.117 -            val (_, (vs', ty')) = Code_Unit.head_eqn thy thm'; (*FIXME simplify check*)
   3.118 -          in (Sign.typ_equiv thy (ty, ty'), (c, thms')) end;
   3.119 -    fun resort_recs eqnss =
   3.120 -      let
   3.121 -        fun typ_of c = case these (AList.lookup (op =) eqnss c)
   3.122 -         of (thm, _) :: _ => (SOME o snd o Code_Unit.head_eqn thy) thm
   3.123 -          | [] => NONE;
   3.124 -        val (unchangeds, eqnss') = split_list (map (resort_rec typ_of) eqnss);
   3.125 -        val unchanged = fold (fn x => fn y => x andalso y) unchangeds true;
   3.126 -      in (unchanged, eqnss') end;
   3.127 -    fun resort_rec_until eqnss =
   3.128 -      let
   3.129 -        val (unchanged, eqnss') = resort_recs eqnss;
   3.130 -      in if unchanged then eqnss' else resort_rec_until eqnss' end;
   3.131 -  in map resort_dep #> resort_rec_until end;
   3.132 -
   3.133 -fun instances_of thy algebra insts =
   3.134 -  let
   3.135 -    val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy;
   3.136 -    fun all_classparams tyco class =
   3.137 -      these (try (#params o AxClass.get_info thy) class)
   3.138 -      |> map_filter (fn (c, _) => try (AxClass.param_of_inst thy) (c, tyco))
   3.139 -  in
   3.140 -    Symtab.empty
   3.141 -    |> fold (fn (tyco, class) =>
   3.142 -        Symtab.map_default (tyco, []) (insert (op =) class)) insts
   3.143 -    |> (fn tab => Symtab.fold (fn (tyco, classes) => append (maps (all_classparams tyco)
   3.144 -         (Graph.all_succs thy_classes classes))) tab [])
   3.145 -  end;
   3.146 -
   3.147 -fun instances_of_consts thy algebra funcgr consts =
   3.148 -  let
   3.149 -    fun inst (cexpr as (c, ty)) = insts_of thy algebra
   3.150 -      (Sign.const_typargs thy (c, ty)) ((map snd o fst) (typ funcgr c));
   3.151 -  in
   3.152 -    []
   3.153 -    |> fold (fold (insert (op =)) o inst) consts
   3.154 -    |> instances_of thy algebra
   3.155 -  end;
   3.156 -
   3.157 -fun ensure_const' thy algebra funcgr const auxgr =
   3.158 -  if can (Graph.get_node funcgr) const
   3.159 -    then (NONE, auxgr)
   3.160 -  else if can (Graph.get_node auxgr) const
   3.161 -    then (SOME const, auxgr)
   3.162 -  else if is_some (Code.get_datatype_of_constr thy const) then
   3.163 -    auxgr
   3.164 -    |> Graph.new_node (const, [])
   3.165 -    |> pair (SOME const)
   3.166 -  else let
   3.167 -    val thms = Code.these_eqns thy const
   3.168 -      |> burrow_fst (Code_Unit.norm_args thy)
   3.169 -      |> burrow_fst (Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var);
   3.170 -    val rhs = consts_of (const, thms);
   3.171 -  in
   3.172 -    auxgr
   3.173 -    |> Graph.new_node (const, thms)
   3.174 -    |> fold_map (ensure_const thy algebra funcgr) rhs
   3.175 -    |-> (fn rhs' => fold (fn SOME const' => Graph.add_edge (const, const')
   3.176 -                           | NONE => I) rhs')
   3.177 -    |> pair (SOME const)
   3.178 -  end
   3.179 -and ensure_const thy algebra funcgr const =
   3.180 -  let
   3.181 -    val timeap = if !timing
   3.182 -      then Output.timeap_msg ("time for " ^ Code_Unit.string_of_const thy const)
   3.183 -      else I;
   3.184 -  in timeap (ensure_const' thy algebra funcgr const) end;
   3.185 -
   3.186 -fun merge_eqnss thy algebra raw_eqnss funcgr =
   3.187 -  let
   3.188 -    val eqnss = raw_eqnss
   3.189 -      |> resort_eqnss thy algebra funcgr
   3.190 -      |> filter_out (can (Graph.get_node funcgr) o fst);
   3.191 -    fun typ_eqn c [] = Code.default_typscheme thy c
   3.192 -      | typ_eqn c (thms as (thm, _) :: _) = (snd o Code_Unit.head_eqn thy) thm;
   3.193 -    fun add_eqns (const, thms) =
   3.194 -      Graph.new_node (const, (typ_eqn const thms, thms));
   3.195 -    fun add_deps (eqns as (const, thms)) funcgr =
   3.196 -      let
   3.197 -        val deps = consts_of eqns;
   3.198 -        val insts = instances_of_consts thy algebra funcgr
   3.199 -          (fold_consts (insert (op =)) (map fst thms) []);
   3.200 -      in
   3.201 -        funcgr
   3.202 -        |> ensure_consts thy algebra insts
   3.203 -        |> fold (curry Graph.add_edge const) deps
   3.204 -        |> fold (curry Graph.add_edge const) insts
   3.205 -       end;
   3.206 -  in
   3.207 -    funcgr
   3.208 -    |> fold add_eqns eqnss
   3.209 -    |> fold add_deps eqnss
   3.210 -  end
   3.211 -and ensure_consts thy algebra cs funcgr =
   3.212 -  let
   3.213 -    val auxgr = Graph.empty
   3.214 -      |> fold (snd oo ensure_const thy algebra funcgr) cs;
   3.215 -  in
   3.216 -    funcgr
   3.217 -    |> fold (merge_eqnss thy algebra)
   3.218 -         (map (AList.make (Graph.get_node auxgr))
   3.219 -         (rev (Graph.strong_conn auxgr)))
   3.220 -  end;
   3.221 -
   3.222 -in
   3.223 -
   3.224 -(** retrieval interfaces **)
   3.225 -
   3.226 -val ensure_consts = ensure_consts;
   3.227 -
   3.228 -fun proto_eval thy cterm_of evaluator_lift evaluator proto_ct funcgr =
   3.229 -  let
   3.230 -    val ct = cterm_of proto_ct;
   3.231 -    val _ = Sign.no_vars (Syntax.pp_global thy) (Thm.term_of ct);
   3.232 -    val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
   3.233 -    fun consts_of t =
   3.234 -      fold_aterms (fn Const c_ty => cons c_ty | _ => I) t [];
   3.235 -    val algebra = Code.coregular_algebra thy;
   3.236 -    val thm = Code.preprocess_conv thy ct;
   3.237 -    val ct' = Thm.rhs_of thm;
   3.238 -    val t' = Thm.term_of ct';
   3.239 -    val consts = map fst (consts_of t');
   3.240 -    val funcgr' = ensure_consts thy algebra consts funcgr;
   3.241 -    val (t'', evaluator_funcgr) = evaluator t';
   3.242 -    val consts' = consts_of t'';
   3.243 -    val dicts = instances_of_consts thy algebra funcgr' consts';
   3.244 -    val funcgr'' = ensure_consts thy algebra dicts funcgr';
   3.245 -  in (evaluator_lift (evaluator_funcgr (Code.operational_algebra thy)) thm funcgr'', funcgr'') end;
   3.246 -
   3.247 -fun proto_eval_conv thy =
   3.248 -  let
   3.249 -    fun evaluator_lift evaluator thm1 funcgr =
   3.250 -      let
   3.251 -        val thm2 = evaluator funcgr;
   3.252 -        val thm3 = Code.postprocess_conv thy (Thm.rhs_of thm2);
   3.253 -      in
   3.254 -        Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
   3.255 -          error ("could not construct evaluation proof:\n"
   3.256 -          ^ (cat_lines o map Display.string_of_thm) [thm1, thm2, thm3])
   3.257 -      end;
   3.258 -  in proto_eval thy I evaluator_lift end;
   3.259 -
   3.260 -fun proto_eval_term thy =
   3.261 -  let
   3.262 -    fun evaluator_lift evaluator _ funcgr = evaluator funcgr;
   3.263 -  in proto_eval thy (Thm.cterm_of thy) evaluator_lift end;
   3.264 -
   3.265 -end; (*local*)
   3.266 -
   3.267 -structure Funcgr = CodeDataFun
   3.268 -(
   3.269 -  type T = T;
   3.270 -  val empty = Graph.empty;
   3.271 -  fun purge _ cs funcgr =
   3.272 -    Graph.del_nodes ((Graph.all_preds funcgr 
   3.273 -      o filter (can (Graph.get_node funcgr))) cs) funcgr;
   3.274 -);
   3.275 -
   3.276 -fun make thy =
   3.277 -  pair (Code.operational_algebra thy)
   3.278 -  o Funcgr.change thy o ensure_consts thy (Code.coregular_algebra thy);
   3.279 -
   3.280 -fun eval_conv thy f =
   3.281 -  fst o Funcgr.change_yield thy o proto_eval_conv thy f;
   3.282 -
   3.283 -fun eval_term thy f =
   3.284 -  fst o Funcgr.change_yield thy o proto_eval_term thy f;
   3.285 -
   3.286 -
   3.287 -(** diagnostic commands **)
   3.288 -
   3.289 -fun code_depgr thy consts =
   3.290 -  let
   3.291 -    val (_, gr) = make thy consts;
   3.292 -    val select = Graph.all_succs gr consts;
   3.293 -  in
   3.294 -    gr
   3.295 -    |> not (null consts) ? Graph.subgraph (member (op =) select) 
   3.296 -    |> Graph.map_nodes ((apsnd o map o apfst) (AxClass.overload thy))
   3.297 -  end;
   3.298 -
   3.299 -fun code_thms thy = Pretty.writeln o pretty thy o code_depgr thy;
   3.300 -
   3.301 -fun code_deps thy consts =
   3.302 -  let
   3.303 -    val gr = code_depgr thy consts;
   3.304 -    fun mk_entry (const, (_, (_, parents))) =
   3.305 -      let
   3.306 -        val name = Code_Unit.string_of_const thy const;
   3.307 -        val nameparents = map (Code_Unit.string_of_const thy) parents;
   3.308 -      in { name = name, ID = name, dir = "", unfold = true,
   3.309 -        path = "", parents = nameparents }
   3.310 -      end;
   3.311 -    val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr [];
   3.312 -  in Present.display_graph prgr end;
   3.313 -
   3.314 -local
   3.315 -
   3.316 -structure P = OuterParse
   3.317 -and K = OuterKeyword
   3.318 -
   3.319 -fun code_thms_cmd thy = code_thms thy o op @ o Code_Name.read_const_exprs thy;
   3.320 -fun code_deps_cmd thy = code_deps thy o op @ o Code_Name.read_const_exprs thy;
   3.321 -
   3.322 -in
   3.323 -
   3.324 -val _ =
   3.325 -  OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag
   3.326 -    (Scan.repeat P.term_group
   3.327 -      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
   3.328 -        o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
   3.329 -
   3.330 -val _ =
   3.331 -  OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag
   3.332 -    (Scan.repeat P.term_group
   3.333 -      >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
   3.334 -        o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
   3.335 -
   3.336 -end;
   3.337 -
   3.338 -end; (*struct*)