--- a/src/Tools/code/code_wellsorted.ML Sun Feb 22 10:53:10 2009 -0800
+++ b/src/Tools/code/code_wellsorted.ML Sun Feb 22 12:03:20 2009 -0800
@@ -1,7 +1,7 @@
(* Title: Tools/code/code_wellsorted.ML
Author: Florian Haftmann, TU Muenchen
-Retrieving, well-sorting and structuring code equations in graph
+Producing well-sorted systems of code equations in a graph
with explicit dependencies -- the Waisenhaus algorithm.
*)
@@ -81,19 +81,25 @@
structure Vargraph =
GraphFun(type key = var val ord = prod_ord const_ord int_ord);
-datatype styp = Tyco of string * styp list | Var of var;
+datatype styp = Tyco of string * styp list | Var of var | Free;
+
+fun styp_of c_lhs (Type (tyco, tys)) = Tyco (tyco, map (styp_of c_lhs) tys)
+ | styp_of c_lhs (TFree (v, _)) = case c_lhs
+ of SOME (c, lhs) => Var (Fun c, find_index (fn (v', _) => v = v') lhs)
+ | NONE => Free;
-val empty_vardeps : ((string * styp list) list * class list) Vargraph.T
- * (const list * ((string * sort) list * (thm * bool) list) Symtab.table) =
- (Vargraph.empty, ([], Symtab.empty));
- (*FIXME: user table with proto equations as assertor for functions,
- add dummy to styp which allows to process consts of terms directly*)
+type vardeps_data = ((string * styp list) list * class list) Vargraph.T
+ * (((string * sort) list * (thm * bool) list) Symtab.table
+ * (class * string) list);
-(* computing instantiations *)
+val empty_vardeps_data : vardeps_data =
+ (Vargraph.empty, (Symtab.empty, []));
+
+(* retrieving equations and instances from the background context *)
fun obtain_eqns thy eqngr c =
case try (Graph.get_node eqngr) c
- of SOME ((lhs, _), eqns) => ((lhs, []), eqns)
+ of SOME ((lhs, _), eqns) => ((lhs, []), [])
| NONE => let
val eqns = Code.these_eqns thy c
|> burrow_fst (Code_Unit.norm_args thy)
@@ -112,6 +118,9 @@
val inst_params = inst_params thy tyco all_classes;
in (classess, (superclasses, inst_params)) end;
+
+(* computing instantiations *)
+
fun add_classes thy arities eqngr c_k new_classes vardeps_data =
let
val (styps, old_classes) = Vargraph.get_node (fst vardeps_data) c_k;
@@ -122,7 +131,7 @@
in
vardeps_data
|> (apfst o Vargraph.map_node c_k o apsnd) (append diff_classes)
- |> fold (fn styp => fold (add_typmatch_inst thy arities eqngr styp) new_classes) styps
+ |> fold (fn styp => fold (assert_typmatch_inst thy arities eqngr styp) new_classes) styps
|> fold (fn c_k => add_classes thy arities eqngr c_k diff_classes) c_ks
end end
and add_styp thy arities eqngr c_k tyco_styps vardeps_data =
@@ -132,7 +141,7 @@
else
vardeps_data
|> (apfst o Vargraph.map_node c_k o apfst) (cons tyco_styps)
- |> fold (add_typmatch_inst thy arities eqngr tyco_styps) classes
+ |> fold (assert_typmatch_inst thy arities eqngr tyco_styps) classes
end
and add_dep thy arities eqngr c_k c_k' vardeps_data =
let
@@ -142,27 +151,23 @@
|> add_classes thy arities eqngr c_k' classes
|> apfst (Vargraph.add_edge (c_k, c_k'))
end
-and add_typmatch_inst thy arities eqngr (tyco, styps) class vardeps_data =
+and assert_typmatch_inst thy arities eqngr (tyco, styps) class vardeps_data =
if can (Sign.arity_sorts thy tyco) [class]
then vardeps_data
- |> assert thy arities eqngr (Inst (class, tyco))
+ |> assert_inst thy arities eqngr (class, tyco)
|> fold_index (fn (k, styp) =>
- add_typmatch thy arities eqngr styp (Inst (class, tyco), k)) styps
+ assert_typmatch thy arities eqngr styp (Inst (class, tyco), k)) styps
else vardeps_data (*permissive!*)
-and add_typmatch thy arities eqngr (Var c_k') c_k vardeps_data =
- vardeps_data
- |> add_dep thy arities eqngr c_k c_k'
- | add_typmatch thy arities eqngr (Tyco tyco_styps) c_k vardeps_data =
- vardeps_data
- |> add_styp thy arities eqngr c_k tyco_styps
-and add_inst thy arities eqngr (inst as (class, tyco)) vardeps_data =
- let
+and assert_inst thy arities eqngr (inst as (class, tyco)) (vardeps_data as (_, (_, insts))) =
+ if member (op =) insts inst then vardeps_data
+ else let
val (classess, (superclasses, inst_params)) =
obtain_instance thy arities inst;
in
vardeps_data
- |> fold (fn superclass => assert thy arities eqngr (Inst (superclass, tyco))) superclasses
- |> fold (assert thy arities eqngr o Fun) inst_params
+ |> (apsnd o apsnd) (insert (op =) inst)
+ |> fold (fn superclass => assert_inst thy arities eqngr (superclass, tyco)) superclasses
+ |> fold (assert_fun thy arities eqngr) inst_params
|> fold_index (fn (k, classes) =>
apfst (Vargraph.new_node ((Inst (class, tyco), k), ([] ,[])))
#> add_classes thy arities eqngr (Inst (class, tyco), k) classes
@@ -175,27 +180,32 @@
) inst_params
) classess
end
-and add_const thy arities eqngr c vardeps_data =
- let
+and assert_typmatch thy arities eqngr (Tyco tyco_styps) c_k vardeps_data =
+ vardeps_data
+ |> add_styp thy arities eqngr c_k tyco_styps
+ | assert_typmatch thy arities eqngr (Var c_k') c_k vardeps_data =
+ vardeps_data
+ |> add_dep thy arities eqngr c_k c_k'
+ | assert_typmatch thy arities eqngr Free c_k vardeps_data =
+ vardeps_data
+and assert_rhs thy arities eqngr (c', styps) vardeps_data =
+ vardeps_data
+ |> assert_fun thy arities eqngr c'
+ |> fold_index (fn (k, styp) =>
+ assert_typmatch thy arities eqngr styp (Fun c', k)) styps
+and assert_fun thy arities eqngr c (vardeps_data as (_, (eqntab, _))) =
+ if Symtab.defined eqntab c then vardeps_data
+ else let
val ((lhs, rhss), eqns) = obtain_eqns thy eqngr c;
- fun styp_of (Type (tyco, tys)) = Tyco (tyco, map styp_of tys)
- | styp_of (TFree (v, _)) = Var (Fun c, find_index (fn (v', _) => v = v') lhs);
- val rhss' = (map o apsnd o map) styp_of rhss;
+ val rhss' = (map o apsnd o map) (styp_of (SOME (c, lhs))) rhss;
in
vardeps_data
- |> (apsnd o apsnd) (Symtab.update_new (c, (lhs, eqns)))
+ |> (apsnd o apfst) (Symtab.update_new (c, (lhs, eqns)))
|> fold_index (fn (k, (_, sort)) =>
apfst (Vargraph.new_node ((Fun c, k), ([] ,[])))
#> add_classes thy arities eqngr (Fun c, k) (complete_proper_sort thy sort)) lhs
- |> fold (assert thy arities eqngr o Fun o fst) rhss'
- |> fold (fn (c', styps) => fold_index (fn (k', styp) =>
- add_typmatch thy arities eqngr styp (Fun c', k')) styps) rhss'
- end
-and assert thy arities eqngr c vardeps_data =
- if member (op =) ((fst o snd) vardeps_data) c then vardeps_data
- else case c
- of Fun const => vardeps_data |> (apsnd o apfst) (cons c) |> add_const thy arities eqngr const
- | Inst inst => vardeps_data |> (apsnd o apfst) (cons c) |> add_inst thy arities eqngr inst;
+ |> fold (assert_rhs thy arities eqngr) rhss'
+ end;
(* applying instantiations *)
@@ -209,16 +219,14 @@
|> filter (is_proper o fst)
|> (map o apsnd) (filter is_proper);
val instances = Sorts.instances_of thy_algebra
- |> filter (is_proper o snd);
+ |> filter (is_proper o snd)
+ |> map swap (*FIXME*)
fun add_class (class, superclasses) algebra =
Sorts.add_class pp (class, Sorts.minimize_sort algebra superclasses) algebra;
- fun add_arity (tyco, class) algebra =
- case AList.lookup (op =) arities (tyco, class)
- of SOME sorts => Sorts.add_arities pp
- (tyco, [(class, map (Sorts.minimize_sort algebra) sorts)]) algebra
- | NONE => if Sign.arity_number thy tyco = 0
- then Sorts.add_arities pp (tyco, [(class, [])]) algebra
- else algebra;
+ fun add_arity (class, tyco) algebra = case AList.lookup (op =) arities (class, tyco)
+ of SOME sorts => Sorts.add_arities pp
+ (tyco, [(class, map (Sorts.minimize_sort algebra) sorts)]) algebra
+ | NONE => algebra;
in
Sorts.empty_algebra
|> fold add_class classrels
@@ -229,7 +237,8 @@
let
fun class_relation (x, _) _ = x;
fun type_constructor tyco xs class =
- inst_params thy tyco (Sorts.complete_sort algebra [class]) @ (maps o maps) fst xs;
+ inst_params thy tyco (Sorts.complete_sort algebra [class])
+ @ (maps o maps) fst xs;
fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
in
flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
@@ -238,74 +247,46 @@
handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
end;
-fun add_arities thy vardeps = Vargraph.fold (fn ((Fun _, _), _) => I
- | ((Inst (class, tyco), k), ((_, classes), _)) =>
- AList.map_default (op =)
- ((tyco, class), replicate (Sign.arity_number thy tyco) [])
- (nth_map k (K classes))) vardeps;
+fun add_arity thy vardeps (class, tyco) =
+ AList.default (op =)
+ ((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) eqntab vardeps c gr =
- let
- val (proto_lhs, proto_eqns) = (the o Symtab.lookup eqntab) c;
+fun add_eqs thy (proj_sort, algebra) 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, _)) =>
(v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs;
val inst_tab = Vartab.empty |> fold (fn (v, sort) =>
Vartab.update ((v, 0), sort)) lhs;
val eqns = proto_eqns
|> (map o apfst) (Code_Unit.inst_thm thy inst_tab);
- val (tyscm, rhss) = tyscm_rhss_of thy c eqns;
- in
- gr
- |> Graph.new_node (c, (tyscm, eqns))
- |> fold (fn (c', Ts) => ensure_eqs_dep thy (proj_sort, algebra) eqntab vardeps c c'
- #-> (fn (vs, _) =>
- fold2 (ensure_match thy (proj_sort, algebra) eqntab vardeps c) Ts (map snd vs))) rhss
- |> pair tyscm
- end
-and ensure_match thy (proj_sort, algebra) eqntab vardeps c T sort gr =
- gr
- |> fold (fn c' => ensure_eqs_dep thy (proj_sort, algebra) eqntab vardeps c c' #> snd)
- (dicts_of thy (proj_sort, algebra) (T, proj_sort sort))
-and ensure_eqs_dep thy (proj_sort, algebra) eqntab vardeps c c' gr =
- gr
- |> ensure_eqs thy (proj_sort, algebra) eqntab vardeps c'
- ||> Graph.add_edge (c, c')
-and ensure_eqs thy (proj_sort, algebra) eqntab vardeps c gr =
- case try (Graph.get_node gr) c
- of SOME (tyscm, _) => (tyscm, gr)
- | NONE => add_eqs thy (proj_sort, algebra) eqntab vardeps c gr;
+ val (tyscm, rhss') = tyscm_rhss_of thy c eqns;
+ val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr;
+ in (map (pair c) rhss' @ rhss, eqngr') end;
-fun extend_arities_eqngr thy cs insts (arities, eqngr) =
+fun extend_arities_eqngr thy cs cs_rhss (arities, eqngr) =
let
- val (vardeps, (_, eqntab)) = empty_vardeps
- |> fold (assert thy arities eqngr o Fun) cs
- |> fold (assert thy arities eqngr o Inst) insts;
- val arities' = add_arities thy vardeps arities;
+ val cs_rhss' = (map o apsnd o map) (styp_of NONE) cs_rhss;
+ val (vardeps, (eqntab, insts)) = empty_vardeps_data
+ |> fold (assert_fun thy arities eqngr) cs
+ |> fold (assert_rhs thy arities eqngr) cs_rhss';
+ val arities' = fold (add_arity thy vardeps) insts arities;
val algebra = build_algebra thy arities';
val proj_sort = complete_proper_sort thy #> Sorts.minimize_sort algebra;
- fun complete_inst_params (class, tyco) =
- inst_params thy tyco (Sorts.complete_sort algebra [class]);
- val cs' = maps complete_inst_params insts @ cs; (*FIXME*)
- val (_, eqngr') =
- fold_map (ensure_eqs thy (proj_sort, algebra) eqntab vardeps) cs' eqngr;
- in ((proj_sort, algebra), (arities', eqngr')) end;
+ 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 eqngr'' = fold (fn (c, rhs) => fold
+ (curry Graph.add_edge c) (deps_of rhs)) rhss eqngr';
+ in ((proj_sort, algebra), (arities', eqngr'')) end;
(** retrieval interfaces **)
-fun instance_dicts_of thy (proj_sort, algebra) (T, sort) = (*FIXME vs. consts_dicts_of *)
- let
- fun class_relation (x, _) _ = x;
- fun type_constructor tyco xs class =
- (class, tyco) :: (maps o maps) fst xs;
- fun type_variable (TFree (_, sort)) = map (pair []) (proj_sort sort);
- in
- flat (Sorts.of_sort_derivation (Syntax.pp_global thy) algebra
- { class_relation = class_relation, type_constructor = type_constructor,
- type_variable = type_variable } (T, proj_sort sort)
- handle Sorts.CLASS_ERROR _ => [] (*permissive!*))
- end;
-
fun proto_eval thy cterm_of evaluator_lift evaluator proto_ct arities_eqngr =
let
val ct = cterm_of proto_ct;
@@ -316,18 +297,17 @@
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 (algebra', arities_eqngr') = extend_arities_eqngr thy consts [] arities_eqngr;
- val (t'', evaluator_eqngr) = evaluator t';
val consts' = consts_of t'';
- val const_matches = fold (fn (c, ty) =>
- insert (op =) (Sign.const_typargs thy (c, Logic.unvarifyT ty), c)) consts' [];
- val typ_matches = maps (fn (tys, c) =>
- tys ~~ map snd (fst (fst (Graph.get_node (snd arities_eqngr') c))))
- const_matches;
- val insts = maps (instance_dicts_of thy algebra') typ_matches;
- val (algebra'', arities_eqngr'') = extend_arities_eqngr thy [] insts arities_eqngr';
- in (evaluator_lift (evaluator_eqngr algebra'') thm (snd arities_eqngr''), arities_eqngr'') end;
+ 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