--- a/src/Tools/code/code_funcgr.ML Fri Aug 24 14:14:18 2007 +0200
+++ b/src/Tools/code/code_funcgr.ML Fri Aug 24 14:14:20 2007 +0200
@@ -10,17 +10,14 @@
sig
type T
val timing: bool ref
- val funcs: T -> CodeUnit.const -> thm list
- val typ: T -> CodeUnit.const -> typ
- val all: T -> CodeUnit.const list
+ val funcs: T -> string -> thm list
+ val typ: T -> string -> typ
+ val all: T -> string list
val pretty: theory -> T -> Pretty.T
- val make: theory -> CodeUnit.const list -> T
- val make_consts: theory -> CodeUnit.const list -> CodeUnit.const list * T
+ val make: theory -> string list -> T
+ val make_consts: theory -> string list -> string list * T
val eval_conv: theory -> (T -> cterm -> thm) -> cterm -> thm
val eval_term: theory -> (T -> cterm -> 'a) -> cterm -> 'a
- val intervene: theory -> T -> T
- (*FIXME drop intervene as soon as possible*)
- structure Constgraph : GRAPH
end
structure CodeFuncgr : CODE_FUNCGR =
@@ -28,23 +25,18 @@
(** the graph type **)
-structure Constgraph = GraphFun (
- type key = CodeUnit.const;
- val ord = CodeUnit.const_ord;
-);
-
-type T = (typ * thm list) Constgraph.T;
+type T = (typ * thm list) Graph.T;
fun funcs funcgr =
- these o Option.map snd o try (Constgraph.get_node funcgr);
+ these o Option.map snd o try (Graph.get_node funcgr);
fun typ funcgr =
- fst o Constgraph.get_node funcgr;
+ fst o Graph.get_node funcgr;
-fun all funcgr = Constgraph.keys funcgr;
+fun all funcgr = Graph.keys funcgr;
fun pretty thy funcgr =
- AList.make (snd o Constgraph.get_node funcgr) (Constgraph.keys funcgr)
+ AList.make (snd o Graph.get_node funcgr) (Graph.keys funcgr)
|> (map o apfst) (CodeUnit.string_of_const thy)
|> sort (string_ord o pairself fst)
|> map (fn (s, thms) =>
@@ -63,13 +55,9 @@
|> (fold o fold_aterms) (fn Const c => f c | _ => I);
fun consts_of (const, []) = []
- | consts_of (const, thms as thm :: _) =
+ | consts_of (const, thms as _ :: _) =
let
- val thy = Thm.theory_of_thm thm;
- val is_refl = curry CodeUnit.eq_const const;
- fun the_const c = case try (CodeUnit.const_of_cexpr thy) c
- of SOME const => if is_refl const then I else insert CodeUnit.eq_const const
- | NONE => I
+ fun the_const (c, _) = if c = const then I else insert (op =) c
in fold_consts the_const thms [] end;
fun insts_of thy algebra c ty_decl ty =
@@ -114,7 +102,7 @@
local
-exception INVALID of CodeUnit.const list * string;
+exception INVALID of string list * string;
fun resort_thms algebra tap_typ [] = []
| resort_thms algebra tap_typ (thms as thm :: _) =
@@ -123,11 +111,11 @@
val cs = fold_consts (insert (op =)) thms [];
fun match_const c (ty, ty_decl) =
let
- val tys = CodeUnit.typargs thy (c, ty);
- val sorts = map (snd o dest_TVar) (CodeUnit.typargs thy (c, ty_decl));
+ val tys = Sign.const_typargs thy (c, ty);
+ val sorts = map (snd o dest_TVar) (Sign.const_typargs thy (c, ty_decl));
in fold2 (curry (CodeUnit.typ_sort_inst algebra)) tys sorts end;
- fun match (c_ty as (c, ty)) =
- case tap_typ c_ty
+ fun match (c, ty) =
+ case tap_typ c
of SOME ty_decl => match_const c (ty, ty_decl)
| NONE => I;
val tvars = fold match cs Vartab.empty;
@@ -135,7 +123,7 @@
fun resort_funcss thy algebra funcgr =
let
- val typ_funcgr = try (fst o Constgraph.get_node funcgr o CodeUnit.const_of_cexpr thy);
+ val typ_funcgr = try (fst o Graph.get_node funcgr);
fun resort_dep (const, thms) = (const, resort_thms algebra typ_funcgr thms)
handle Sorts.CLASS_ERROR e => raise INVALID ([const], Sorts.msg_class_error (Sign.pp thy) e
^ ",\nfor constant " ^ CodeUnit.string_of_const thy const
@@ -150,12 +138,11 @@
in (Sign.typ_equiv thy (ty, ty'), (const, thms')) end;
fun resort_recs funcss =
let
- fun tap_typ c_ty = case try (CodeUnit.const_of_cexpr thy) c_ty
- of SOME const => AList.lookup (CodeUnit.eq_const) funcss const
- |> these
- |> try hd
- |> Option.map (snd o CodeUnit.head_func)
- | NONE => NONE;
+ fun tap_typ c =
+ AList.lookup (op =) funcss c
+ |> these
+ |> try hd
+ |> Option.map (snd o CodeUnit.head_func);
val (unchangeds, funcss') = split_list (map (resort_rec tap_typ) funcss);
val unchanged = fold (fn x => fn y => x andalso y) unchangeds true;
in (unchanged, funcss') end;
@@ -172,7 +159,7 @@
try (AxClass.params_of_class thy) class
|> Option.map snd
|> these
- |> map (fn (c, _) => (c, SOME tyco))
+ |> map (fn (c, _) => Class.inst_const thy (c, tyco))
in
Symtab.empty
|> fold (fn (tyco, class) =>
@@ -184,8 +171,7 @@
fun instances_of_consts thy algebra funcgr consts =
let
fun inst (cexpr as (c, ty)) = insts_of thy algebra c
- ((fst o Constgraph.get_node funcgr o CodeUnit.const_of_cexpr thy) cexpr)
- ty handle CLASS_ERROR => [];
+ ((fst o Graph.get_node funcgr) c) ty handle CLASS_ERROR => [];
in
[]
|> fold (fold (insert (op =)) o inst) consts
@@ -193,13 +179,13 @@
end;
fun ensure_const' thy algebra funcgr const auxgr =
- if can (Constgraph.get_node funcgr) const
+ if can (Graph.get_node funcgr) const
then (NONE, auxgr)
- else if can (Constgraph.get_node auxgr) const
+ else if can (Graph.get_node auxgr) const
then (SOME const, auxgr)
else if is_some (Code.get_datatype_of_constr thy const) then
auxgr
- |> Constgraph.new_node (const, [])
+ |> Graph.new_node (const, [])
|> pair (SOME const)
else let
val thms = Code.these_funcs thy const
@@ -208,9 +194,9 @@
val rhs = consts_of (const, thms);
in
auxgr
- |> Constgraph.new_node (const, thms)
+ |> Graph.new_node (const, thms)
|> fold_map (ensure_const thy algebra funcgr) rhs
- |-> (fn rhs' => fold (fn SOME const' => Constgraph.add_edge (const, const')
+ |-> (fn rhs' => fold (fn SOME const' => Graph.add_edge (const, const')
| NONE => I) rhs')
|> pair (SOME const)
end
@@ -225,24 +211,25 @@
let
val funcss = raw_funcss
|> resort_funcss thy algebra funcgr
- |> filter_out (can (Constgraph.get_node funcgr) o fst);
- fun typ_func const [] = Code.default_typ thy const
- | typ_func (_, NONE) (thm :: _) = (snd o CodeUnit.head_func) thm
- | typ_func (const as (c, SOME tyco)) (thms as (thm :: _)) =
- let
- val (_, ty) = CodeUnit.head_func thm;
- val SOME class = AxClass.class_of_param thy c;
- val sorts_decl = Sorts.mg_domain algebra tyco [class];
- val tys = CodeUnit.typargs thy (c, ty);
- val sorts = map (snd o dest_TVar) tys;
- in if sorts = sorts_decl then ty
- else raise INVALID ([const], "Illegal instantation for class operation "
- ^ CodeUnit.string_of_const thy const
- ^ "\nin defining equations\n"
- ^ (cat_lines o map string_of_thm) thms)
- end;
+ |> filter_out (can (Graph.get_node funcgr) o fst);
+ fun typ_func c [] = Code.default_typ thy c
+ | typ_func c (thms as thm :: _) = case Class.param_const thy c
+ of SOME (c', tyco) =>
+ let
+ val (_, ty) = CodeUnit.head_func thm;
+ val SOME class = AxClass.class_of_param thy c';
+ val sorts_decl = Sorts.mg_domain algebra tyco [class];
+ val tys = Sign.const_typargs thy (c, ty);
+ val sorts = map (snd o dest_TVar) tys;
+ in if sorts = sorts_decl then ty
+ else raise INVALID ([c], "Illegal instantation for class operation "
+ ^ CodeUnit.string_of_const thy c
+ ^ "\nin defining equations\n"
+ ^ (cat_lines o map string_of_thm) thms)
+ end
+ | NONE => (snd o CodeUnit.head_func) thm;
fun add_funcs (const, thms) =
- Constgraph.new_node (const, (typ_func const thms, thms));
+ Graph.new_node (const, (typ_func const thms, thms));
fun add_deps (funcs as (const, thms)) funcgr =
let
val deps = consts_of funcs;
@@ -251,8 +238,8 @@
in
funcgr
|> ensure_consts' thy algebra insts
- |> fold (curry Constgraph.add_edge const) deps
- |> fold (curry Constgraph.add_edge const) insts
+ |> fold (curry Graph.add_edge const) deps
+ |> fold (curry Graph.add_edge const) insts
end;
in
funcgr
@@ -261,29 +248,24 @@
end
and ensure_consts' thy algebra cs funcgr =
let
- val auxgr = Constgraph.empty
+ val auxgr = Graph.empty
|> fold (snd oo ensure_const thy algebra funcgr) cs;
in
funcgr
|> fold (merge_funcss thy algebra)
- (map (AList.make (Constgraph.get_node auxgr))
- (rev (Constgraph.strong_conn auxgr)))
+ (map (AList.make (Graph.get_node auxgr))
+ (rev (Graph.strong_conn auxgr)))
end handle INVALID (cs', msg)
- => raise INVALID (fold (insert CodeUnit.eq_const) cs' cs, msg);
-
-fun ensure_consts thy consts funcgr =
- let
- val algebra = Code.coregular_algebra thy
- in ensure_consts' thy algebra consts funcgr
- handle INVALID (cs', msg) => error (msg ^ ",\nwhile preprocessing equations for constant(s) "
- ^ commas (map (CodeUnit.string_of_const thy) cs'))
- end;
+ => raise INVALID (fold (insert (op =)) cs' cs, msg);
in
(** retrieval interfaces **)
-val ensure_consts = ensure_consts;
+fun ensure_consts thy algebra consts funcgr =
+ ensure_consts' thy algebra consts funcgr
+ handle INVALID (cs', msg) => error (msg ^ ",\nwhile preprocessing equations for constant(s) "
+ ^ commas (map (CodeUnit.string_of_const thy) cs'));
fun check_consts thy consts funcgr =
let
@@ -294,25 +276,20 @@
val (consts', funcgr') = fold_map try_const consts funcgr;
in (map_filter I consts', funcgr') end;
-fun ensure_consts_term_proto thy f ct funcgr =
+fun raw_eval thy f ct funcgr =
let
- fun consts_of thy t =
- fold_aterms (fn Const c => cons (CodeUnit.const_of_cexpr thy c) | _ => I) t []
- fun rhs_conv conv thm =
- let
- val thm' = (conv o Thm.rhs_of) thm;
- in Thm.transitive thm thm' end
+ val algebra = Code.coregular_algebra thy;
+ fun consts_of ct = fold_aterms (fn Const c_ty => cons c_ty | _ => I)
+ (Thm.term_of ct) [];
val _ = Sign.no_vars (Sign.pp thy) (Thm.term_of ct);
val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
val thm1 = Code.preprocess_conv ct;
val ct' = Thm.rhs_of thm1;
- val consts = consts_of thy (Thm.term_of ct');
- val funcgr' = ensure_consts thy consts funcgr;
- val algebra = Code.coregular_algebra thy;
+ val cs = map fst (consts_of ct');
+ val funcgr' = ensure_consts thy algebra cs funcgr;
val (_, thm2) = Thm.varifyT' [] thm1;
val thm3 = Thm.reflexive (Thm.rhs_of thm2);
- val typ_funcgr = try (fst o Constgraph.get_node funcgr' o CodeUnit.const_of_cexpr thy);
- val [thm4] = resort_thms algebra typ_funcgr [thm3];
+ val [thm4] = resort_thms algebra (try (fst o Graph.get_node funcgr')) [thm3];
val tfrees = Term.add_tfrees (Thm.prop_of thm1) [];
fun inst thm =
let
@@ -323,56 +300,54 @@
val thm5 = inst thm2;
val thm6 = inst thm4;
val ct'' = Thm.rhs_of thm6;
- val cs = fold_aterms (fn Const c => cons c | _ => I) (Thm.term_of ct'') [];
+ val c_exprs = consts_of ct'';
val drop = drop_classes thy tfrees;
- val instdefs = instances_of_consts thy algebra funcgr' cs;
- val funcgr'' = ensure_consts thy instdefs funcgr';
- in (f funcgr'' drop ct'' thm5, funcgr'') end;
+ val instdefs = instances_of_consts thy algebra funcgr' c_exprs;
+ val funcgr'' = ensure_consts thy algebra instdefs funcgr';
+ in (f drop thm5 funcgr'' ct'' , funcgr'') end;
-fun ensure_consts_eval thy conv =
+fun raw_eval_conv thy conv =
let
- fun conv' funcgr drop_classes ct thm1 =
+ fun conv' drop_classes thm1 funcgr ct =
let
val thm2 = conv funcgr ct;
val thm3 = Code.postprocess_conv (Thm.rhs_of thm2);
val thm23 = drop_classes (Thm.transitive thm2 thm3);
in
Thm.transitive thm1 thm23 handle THM _ =>
- error ("eval_conv - could not construct proof:\n"
+ error ("could not construct proof:\n"
^ (cat_lines o map string_of_thm) [thm1, thm2, thm3])
end;
- in ensure_consts_term_proto thy conv' end;
+ in raw_eval thy conv' end;
-fun ensure_consts_term thy f =
+fun raw_eval_term thy f =
let
- fun f' funcgr drop_classes ct thm1 = f funcgr ct;
- in ensure_consts_term_proto thy f' end;
+ fun f' _ _ funcgr ct = f funcgr ct;
+ in raw_eval thy f' end;
end; (*local*)
structure Funcgr = CodeDataFun
(struct
type T = T;
- val empty = Constgraph.empty;
- fun merge _ _ = Constgraph.empty;
- fun purge _ NONE _ = Constgraph.empty
+ val empty = Graph.empty;
+ fun merge _ _ = Graph.empty;
+ fun purge _ NONE _ = Graph.empty
| purge _ (SOME cs) funcgr =
- Constgraph.del_nodes ((Constgraph.all_preds funcgr
- o filter (can (Constgraph.get_node funcgr))) cs) funcgr;
+ Graph.del_nodes ((Graph.all_preds funcgr
+ o filter (can (Graph.get_node funcgr))) cs) funcgr;
end);
fun make thy =
- Funcgr.change thy o ensure_consts thy;
+ Funcgr.change thy o ensure_consts thy (Code.coregular_algebra thy);
fun make_consts thy =
Funcgr.change_yield thy o check_consts thy;
fun eval_conv thy f =
- fst o Funcgr.change_yield thy o ensure_consts_eval thy f;
+ fst o Funcgr.change_yield thy o raw_eval_conv thy f;
fun eval_term thy f =
- fst o Funcgr.change_yield thy o ensure_consts_term thy f;
-
-fun intervene thy funcgr = Funcgr.change thy (K funcgr);
+ fst o Funcgr.change_yield thy o raw_eval_term thy f;
end; (*struct*)