--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Matrix/eq_codegen.ML Fri Sep 03 17:10:36 2004 +0200
@@ -0,0 +1,493 @@
+fun inst_cterm inst ct = fst (Drule.dest_equals
+ (Thm.cprop_of (Thm.instantiate inst (reflexive ct))));
+fun tyinst_cterm tyinst = inst_cterm (tyinst, []);
+
+val bla = ref ([] : term list);
+
+(******************************************************)
+(* Code generator for equational proofs *)
+(******************************************************)
+fun my_mk_meta_eq thm =
+ let
+ val (_, eq) = Thm.dest_comb (cprop_of thm);
+ val (ct, rhs) = Thm.dest_comb eq;
+ val (_, lhs) = Thm.dest_comb ct
+ in Thm.implies_elim (Drule.instantiate' [Some (ctyp_of_term lhs)]
+ [Some lhs, Some rhs] eq_reflection) thm
+ end;
+
+structure SimprocsCodegen =
+struct
+
+val simp_thms = ref ([] : thm list);
+
+fun parens b = if b then Pretty.enclose "(" ")" else Pretty.block;
+
+fun gen_mk_val f xs ps = Pretty.block ([Pretty.str "val ",
+ f (length xs > 1) (flat
+ (separate [Pretty.str ",", Pretty.brk 1] (map (single o Pretty.str) xs))),
+ Pretty.str " =", Pretty.brk 1] @ ps @ [Pretty.str ";"]);
+
+val mk_val = gen_mk_val parens;
+val mk_vall = gen_mk_val (K (Pretty.enclose "[" "]"));
+
+fun rename s = if s mem ThmDatabase.ml_reserved then s ^ "'" else s;
+
+fun mk_decomp_name (Var ((s, i), _)) = rename (if i=0 then s else s ^ string_of_int i)
+ | mk_decomp_name (Const (s, _)) = rename (Codegen.mk_id (Sign.base_name s))
+ | mk_decomp_name _ = "ct";
+
+fun decomp_term_code cn ((vs, bs, ps), (v, t)) =
+ if exists (equal t o fst) bs then (vs, bs, ps)
+ else (case t of
+ Var _ => (vs, bs @ [(t, v)], ps)
+ | Const _ => (vs, if cn then bs @ [(t, v)] else bs, ps)
+ | Bound _ => (vs, bs, ps)
+ | Abs (s, T, t) =>
+ let
+ val v1 = variant vs s;
+ val v2 = variant (v1 :: vs) (mk_decomp_name t)
+ in
+ decomp_term_code cn ((v1 :: v2 :: vs,
+ bs @ [(Free (s, T), v1)],
+ ps @ [mk_val [v1, v2] [Pretty.str "Thm.dest_abs", Pretty.brk 1,
+ Pretty.str "None", Pretty.brk 1, Pretty.str v]]), (v2, t))
+ end
+ | t $ u =>
+ let
+ val v1 = variant vs (mk_decomp_name t);
+ val v2 = variant (v1 :: vs) (mk_decomp_name u);
+ val (vs', bs', ps') = decomp_term_code cn ((v1 :: v2 :: vs, bs,
+ ps @ [mk_val [v1, v2] [Pretty.str "Thm.dest_comb", Pretty.brk 1,
+ Pretty.str v]]), (v1, t));
+ val (vs'', bs'', ps'') = decomp_term_code cn ((vs', bs', ps'), (v2, u))
+ in
+ if bs'' = bs then (vs, bs, ps) else (vs'', bs'', ps'')
+ end);
+
+val strip_tv = implode o tl o explode;
+
+fun mk_decomp_tname (TVar ((s, i), _)) =
+ strip_tv ((if i=0 then s else s ^ string_of_int i) ^ "T")
+ | mk_decomp_tname (Type (s, _)) = Codegen.mk_id (Sign.base_name s) ^ "T"
+ | mk_decomp_tname _ = "cT";
+
+fun decomp_type_code ((vs, bs, ps), (v, TVar (ixn, _))) =
+ if exists (equal ixn o fst) bs then (vs, bs, ps)
+ else (vs, bs @ [(ixn, v)], ps)
+ | decomp_type_code ((vs, bs, ps), (v, Type (_, Ts))) =
+ let
+ val vs' = variantlist (map mk_decomp_tname Ts, vs);
+ val (vs'', bs', ps') =
+ foldl decomp_type_code ((vs @ vs', bs, ps @
+ [mk_vall vs' [Pretty.str "Thm.dest_ctyp", Pretty.brk 1,
+ Pretty.str v]]), vs' ~~ Ts)
+ in
+ if bs' = bs then (vs, bs, ps) else (vs'', bs', ps')
+ end;
+
+fun gen_mk_bindings s dest decomp ((vs, bs, ps), (v, x)) =
+ let
+ val s' = variant vs s;
+ val (vs', bs', ps') = decomp ((s' :: vs, bs, ps @
+ [mk_val [s'] (dest v)]), (s', x))
+ in
+ if bs' = bs then (vs, bs, ps) else (vs', bs', ps')
+ end;
+
+val mk_term_bindings = gen_mk_bindings "ct"
+ (fn s => [Pretty.str "cprop_of", Pretty.brk 1, Pretty.str s])
+ (decomp_term_code true);
+
+val mk_type_bindings = gen_mk_bindings "cT"
+ (fn s => [Pretty.str "Thm.ctyp_of_term", Pretty.brk 1, Pretty.str s])
+ decomp_type_code;
+
+fun pretty_pattern b (Const (s, _)) = Pretty.block [Pretty.str "Const",
+ Pretty.brk 1, Pretty.str ("(\"" ^ s ^ "\", _)")]
+ | pretty_pattern b (t as _ $ _) = parens b
+ (flat (separate [Pretty.str " $", Pretty.brk 1]
+ (map (single o pretty_pattern true) (op :: (strip_comb t)))))
+ | pretty_pattern b _ = Pretty.str "_";
+
+fun term_consts' t = foldl_aterms
+ (fn (cs, c as Const _) => c ins cs | (cs, _) => cs) ([], t);
+
+fun mk_apps s b p [] = p
+ | mk_apps s b p (q :: qs) =
+ mk_apps s b (parens (b orelse not (null qs))
+ [Pretty.str s, Pretty.brk 1, p, Pretty.brk 1, q]) qs;
+
+fun mk_refleq eq ct = mk_val [eq] [Pretty.str ("Thm.reflexive " ^ ct)];
+
+fun mk_tyinst ((s, i), s') =
+ Pretty.block [Pretty.str ("((" ^ quote s ^ ","), Pretty.brk 1,
+ Pretty.str (string_of_int i ^ "),"), Pretty.brk 1,
+ Pretty.str (s' ^ ")")];
+
+fun inst_ty b ty_bs t s = (case term_tvars t of
+ [] => Pretty.str s
+ | Ts => parens b [Pretty.str "tyinst_cterm", Pretty.brk 1,
+ Pretty.list "[" "]" (map (fn (ixn, _) => mk_tyinst
+ (ixn, the (assoc (ty_bs, ixn)))) Ts),
+ Pretty.brk 1, Pretty.str s]);
+
+fun mk_cterm_code b ty_bs ts xs (vals, t $ u) =
+ let
+ val (vals', p1) = mk_cterm_code true ty_bs ts xs (vals, t);
+ val (vals'', p2) = mk_cterm_code true ty_bs ts xs (vals', u)
+ in
+ (vals'', parens b [Pretty.str "Thm.capply", Pretty.brk 1,
+ p1, Pretty.brk 1, p2])
+ end
+ | mk_cterm_code b ty_bs ts xs (vals, Abs (s, T, t)) =
+ let
+ val u = Free (s, T);
+ val Some s' = assoc (ts, u);
+ val p = Pretty.str s';
+ val (vals', p') = mk_cterm_code true ty_bs ts (p :: xs)
+ (if null (typ_tvars T) then vals
+ else vals @ [(u, (("", s'), [mk_val [s'] [inst_ty true ty_bs u s']]))], t)
+ in (vals',
+ parens b [Pretty.str "Thm.cabs", Pretty.brk 1, p, Pretty.brk 1, p'])
+ end
+ | mk_cterm_code b ty_bs ts xs (vals, Bound i) = (vals, nth_elem (i, xs))
+ | mk_cterm_code b ty_bs ts xs (vals, t) = (case assoc (vals, t) of
+ None =>
+ let val Some s = assoc (ts, t)
+ in (if is_Const t andalso not (null (term_tvars t)) then
+ vals @ [(t, (("", s), [mk_val [s] [inst_ty true ty_bs t s]]))]
+ else vals, Pretty.str s)
+ end
+ | Some ((_, s), _) => (vals, Pretty.str s));
+
+fun get_cases sg =
+ Symtab.foldl (fn (tab, (k, {case_rewrites, ...})) => Symtab.update_new
+ ((fst (dest_Const (head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
+ (prop_of (hd case_rewrites))))))), map my_mk_meta_eq case_rewrites), tab))
+ (Symtab.empty, DatatypePackage.get_datatypes_sg sg);
+
+fun decomp_case th =
+ let
+ val (lhs, _) = Logic.dest_equals (prop_of th);
+ val (f, ts) = strip_comb lhs;
+ val (us, u) = split_last ts;
+ val (Const (s, _), vs) = strip_comb u
+ in (us, s, vs, u) end;
+
+fun rename vs t =
+ let
+ fun mk_subst ((vs, subs), Var ((s, i), T)) =
+ let val s' = variant vs s
+ in if s = s' then (vs, subs)
+ else (s' :: vs, ((s, i), Var ((s', i), T)) :: subs)
+ end;
+ val (vs', subs) = foldl mk_subst ((vs, []), term_vars t)
+ in (vs', subst_Vars subs t) end;
+
+fun is_instance sg t u = t = subst_TVars_Vartab
+ (Type.typ_match (Sign.tsig_of sg) (Vartab.empty,
+ (fastype_of u, fastype_of t))) u handle Type.TYPE_MATCH => false;
+
+(*
+fun lookup sg fs t = apsome snd (Library.find_first
+ (is_instance sg t o fst) fs);
+*)
+
+fun lookup sg fs t = (case Library.find_first (is_instance sg t o fst) fs of
+ None => (bla := (t ins !bla); None)
+ | Some (_, x) => Some x);
+
+fun unint sg fs t = forall (is_none o lookup sg fs) (term_consts' t);
+
+fun mk_let s i xs ys =
+ Pretty.blk (0, [Pretty.blk (i, separate Pretty.fbrk (Pretty.str s :: xs)),
+ Pretty.fbrk,
+ Pretty.blk (i, ([Pretty.str "in", Pretty.fbrk] @ ys)),
+ Pretty.fbrk, Pretty.str "end"]);
+
+(*****************************************************************************)
+(* Generate bindings for simplifying term t *)
+(* mkeq: whether to generate reflexivity theorem for uninterpreted terms *)
+(* fs: interpreted functions *)
+(* ts: atomic terms *)
+(* vs: used identifiers *)
+(* vals: list of bindings of the form ((eq, ct), ps) where *)
+(* eq: name of equational theorem *)
+(* ct: name of simplified cterm *)
+(* ps: ML code for creating the above two items *)
+(*****************************************************************************)
+
+fun mk_simpl_code sg case_tab mkeq fs ts ty_bs thm_bs ((vs, vals), t) =
+ (case assoc (vals, t) of
+ Some ((eq, ct), ps) => (* binding already generated *)
+ if mkeq andalso eq="" then
+ let val eq' = variant vs "eq"
+ in ((eq' :: vs, overwrite (vals,
+ (t, ((eq', ct), ps @ [mk_refleq eq' ct])))), (eq', ct))
+ end
+ else ((vs, vals), (eq, ct))
+ | None => (case assoc (ts, t) of
+ Some v => (* atomic term *)
+ let val xs = if not (null (term_tvars t)) andalso is_Const t then
+ [mk_val [v] [inst_ty false ty_bs t v]] else []
+ in
+ if mkeq then
+ let val eq = variant vs "eq"
+ in ((eq :: vs, vals @
+ [(t, ((eq, v), xs @ [mk_refleq eq v]))]), (eq, v))
+ end
+ else ((vs, if null xs then vals else vals @
+ [(t, (("", v), xs))]), ("", v))
+ end
+ | None => (* complex term *)
+ let val (f as Const (cname, _), us) = strip_comb t
+ in case Symtab.lookup (case_tab, cname) of
+ Some cases => (* case expression *)
+ let
+ val (us', u) = split_last us;
+ val b = unint sg fs u;
+ val ((vs1, vals1), (eq, ct)) =
+ mk_simpl_code sg case_tab (not b) fs ts ty_bs thm_bs ((vs, vals), u);
+ val xs = variantlist (replicate (length us') "f", vs1);
+ val (vals2, ps) = foldl_map
+ (mk_cterm_code false ty_bs ts []) (vals1, us');
+ val fvals = map (fn (x, p) => mk_val [x] [p]) (xs ~~ ps);
+ val uT = fastype_of u;
+ val (us'', _, _, u') = decomp_case (hd cases);
+ val (vs2, ty_bs', ty_vals) = mk_type_bindings
+ (mk_type_bindings ((vs1 @ xs, [], []),
+ (hd xs, fastype_of (hd us''))), (ct, fastype_of u'));
+ val insts1 = map mk_tyinst ty_bs';
+ val i = length vals2;
+
+ fun mk_case_code ((vs, vals), (f, (name, eqn))) =
+ let
+ val (fvs, cname, cvs, _) = decomp_case eqn;
+ val Ts = binder_types (fastype_of f);
+ val ys = variantlist (map (fst o fst o dest_Var) cvs, vs);
+ val cvs' = map Var (map (rpair 0) ys ~~ Ts);
+ val rs = cvs' ~~ cvs;
+ val lhs = list_comb (Const (cname, Ts ---> uT), cvs');
+ val rhs = foldl betapply (f, cvs');
+ val (vs', tm_bs, tm_vals) = decomp_term_code false
+ ((vs @ ys, [], []), (ct, lhs));
+ val ((vs'', all_vals), (eq', ct')) = mk_simpl_code sg case_tab
+ false fs (tm_bs @ ts) ty_bs thm_bs ((vs', vals), rhs);
+ val (old_vals, eq_vals) = splitAt (i, all_vals);
+ val vs''' = vs @ filter (fn v => exists
+ (fn (_, ((v', _), _)) => v = v') old_vals) (vs'' \\ vs');
+ val insts2 = map (fn (t, s) => Pretty.block [Pretty.str "(",
+ inst_ty false ty_bs' t (the (assoc (thm_bs, t))), Pretty.str ",",
+ Pretty.brk 1, Pretty.str (s ^ ")")]) ((fvs ~~ xs) @
+ (map (fn (v, s) => (the (assoc (rs, v)), s)) tm_bs));
+ val eq'' = if null insts1 andalso null insts2 then Pretty.str name
+ else parens (eq' <> "") [Pretty.str
+ (if null cvs then "Thm.instantiate" else "Drule.instantiate"),
+ Pretty.brk 1, Pretty.str "(", Pretty.list "[" "]" insts1,
+ Pretty.str ",", Pretty.brk 1, Pretty.list "[" "]" insts2,
+ Pretty.str ")", Pretty.brk 1, Pretty.str name];
+ val eq''' = if eq' = "" then eq'' else
+ Pretty.block [Pretty.str "Thm.transitive", Pretty.brk 1,
+ eq'', Pretty.brk 1, Pretty.str eq']
+ in
+ ((vs''', old_vals), Pretty.block [pretty_pattern false lhs,
+ Pretty.str " =>",
+ Pretty.brk 1, mk_let "let" 2 (tm_vals @ flat (map (snd o snd) eq_vals))
+ [Pretty.str ("(" ^ ct' ^ ","), Pretty.brk 1, eq''', Pretty.str ")"]])
+ end;
+
+ val case_names = map (fn i => Sign.base_name cname ^ "_" ^
+ string_of_int i) (1 upto length cases);
+ val ((vs3, vals3), case_ps) = foldl_map mk_case_code
+ ((vs2, vals2), us' ~~ (case_names ~~ cases));
+ val eq' = variant vs3 "eq";
+ val ct' = variant (eq' :: vs3) "ct";
+ val eq'' = variant (eq' :: ct' :: vs3) "eq";
+ val case_vals =
+ fvals @ ty_vals @
+ [mk_val [ct', eq'] ([Pretty.str "(case", Pretty.brk 1,
+ Pretty.str ("term_of " ^ ct ^ " of"), Pretty.brk 1] @
+ flat (separate [Pretty.brk 1, Pretty.str "| "]
+ (map single case_ps)) @ [Pretty.str ")"])]
+ in
+ if b then
+ ((eq' :: ct' :: vs3, vals3 @
+ [(t, ((eq', ct'), case_vals))]), (eq', ct'))
+ else
+ let val ((vs4, vals4), (_, ctcase)) = mk_simpl_code sg case_tab false
+ fs ts ty_bs thm_bs ((eq' :: eq'' :: ct' :: vs3, vals3), f)
+ in
+ ((vs4, vals4 @ [(t, ((eq'', ct'), case_vals @
+ [mk_val [eq''] [Pretty.str "Thm.transitive", Pretty.brk 1,
+ Pretty.str "(Thm.combination", Pretty.brk 1,
+ Pretty.str "(Thm.reflexive", Pretty.brk 1,
+ mk_apps "Thm.capply" true (Pretty.str ctcase)
+ (map Pretty.str xs),
+ Pretty.str ")", Pretty.brk 1, Pretty.str (eq ^ ")"),
+ Pretty.brk 1, Pretty.str eq']]))]), (eq'', ct'))
+ end
+ end
+
+ | None =>
+ let
+ val b = forall (unint sg fs) us;
+ val (q, eqs) = foldl_map
+ (mk_simpl_code sg case_tab (not b) fs ts ty_bs thm_bs) ((vs, vals), us);
+ val ((vs', vals'), (eqf, ctf)) = if is_some (lookup sg fs f) andalso b
+ then (q, ("", ""))
+ else mk_simpl_code sg case_tab (not b) fs ts ty_bs thm_bs (q, f);
+ val ct = variant vs' "ct";
+ val eq = variant (ct :: vs') "eq";
+ val ctv = mk_val [ct] [mk_apps "Thm.capply" false
+ (Pretty.str ctf) (map (Pretty.str o snd) eqs)];
+ fun combp b = mk_apps "Thm.combination" b
+ (Pretty.str eqf) (map (Pretty.str o fst) eqs)
+ in
+ case (lookup sg fs f, b) of
+ (None, true) => (* completely uninterpreted *)
+ if mkeq then ((ct :: eq :: vs', vals' @
+ [(t, ((eq, ct), [ctv, mk_refleq eq ct]))]), (eq, ct))
+ else ((ct :: vs', vals' @ [(t, (("", ct), [ctv]))]), ("", ct))
+ | (None, false) => (* function uninterpreted *)
+ ((eq :: ct :: vs', vals' @
+ [(t, ((eq, ct), [ctv, mk_val [eq] [combp false]]))]), (eq, ct))
+ | (Some (s, _, _), true) => (* arguments uninterpreted *)
+ ((eq :: ct :: vs', vals' @
+ [(t, ((eq, ct), [mk_val [ct, eq] (separate (Pretty.brk 1)
+ (Pretty.str s :: map (Pretty.str o snd) eqs))]))]), (eq, ct))
+ | (Some (s, _, _), false) => (* function and arguments interpreted *)
+ let val eq' = variant (eq :: ct :: vs') "eq"
+ in ((eq' :: eq :: ct :: vs', vals' @ [(t, ((eq', ct),
+ [mk_val [ct, eq] (separate (Pretty.brk 1)
+ (Pretty.str s :: map (Pretty.str o snd) eqs)),
+ mk_val [eq'] [Pretty.str "Thm.transitive", Pretty.brk 1,
+ combp true, Pretty.brk 1, Pretty.str eq]]))]), (eq', ct))
+ end
+ end
+ end));
+
+fun lhs_of thm = fst (Logic.dest_equals (prop_of thm));
+fun rhs_of thm = snd (Logic.dest_equals (prop_of thm));
+
+fun mk_funs_code sg case_tab fs fs' =
+ let
+ val case_thms = mapfilter (fn s => (case Symtab.lookup (case_tab, s) of
+ None => None
+ | Some thms => Some (unsuffix "_case" (Sign.base_name s) ^ ".cases",
+ map (fn i => Sign.base_name s ^ "_" ^ string_of_int i)
+ (1 upto length thms) ~~ thms)))
+ (foldr add_term_consts (map (prop_of o snd)
+ (flat (map (#3 o snd) fs')), []));
+ val case_vals = map (fn (s, cs) => mk_vall (map fst cs)
+ [Pretty.str "map my_mk_meta_eq", Pretty.brk 1,
+ Pretty.str ("(thms \"" ^ s ^ "\")")]) case_thms;
+ val (vs, thm_bs, thm_vals) = foldl mk_term_bindings (([], [], []),
+ flat (map (map (apsnd prop_of) o #3 o snd) fs') @
+ map (apsnd prop_of) (flat (map snd case_thms)));
+
+ fun mk_fun_code (prfx, (fname, d, eqns)) =
+ let
+ val (f, ts) = strip_comb (lhs_of (snd (hd eqns)));
+ val args = variantlist (replicate (length ts) "ct", vs);
+ val (vs', ty_bs, ty_vals) = foldl mk_type_bindings
+ ((vs @ args, [], []), args ~~ map fastype_of ts);
+ val insts1 = map mk_tyinst ty_bs;
+
+ fun mk_eqn_code (name, eqn) =
+ let
+ val (_, argts) = strip_comb (lhs_of eqn);
+ val (vs'', tm_bs, tm_vals) = foldl (decomp_term_code false)
+ ((vs', [], []), args ~~ argts);
+ val ((vs''', eq_vals), (eq, ct)) = mk_simpl_code sg case_tab false fs
+ (tm_bs @ filter_out (is_Var o fst) thm_bs) ty_bs thm_bs
+ ((vs'', []), rhs_of eqn);
+ val insts2 = map (fn (t, s) => Pretty.block [Pretty.str "(",
+ inst_ty false ty_bs t (the (assoc (thm_bs, t))), Pretty.str ",", Pretty.brk 1,
+ Pretty.str (s ^ ")")]) tm_bs
+ val eq' = if null insts1 andalso null insts2 then Pretty.str name
+ else parens (eq <> "") [Pretty.str "Thm.instantiate",
+ Pretty.brk 1, Pretty.str "(", Pretty.list "[" "]" insts1,
+ Pretty.str ",", Pretty.brk 1, Pretty.list "[" "]" insts2,
+ Pretty.str ")", Pretty.brk 1, Pretty.str name];
+ val eq'' = if eq = "" then eq' else
+ Pretty.block [Pretty.str "Thm.transitive", Pretty.brk 1,
+ eq', Pretty.brk 1, Pretty.str eq]
+ in
+ Pretty.block [parens (length argts > 1)
+ (Pretty.commas (map (pretty_pattern false) argts)),
+ Pretty.str " =>",
+ Pretty.brk 1, mk_let "let" 2 (ty_vals @ tm_vals @ flat (map (snd o snd) eq_vals))
+ [Pretty.str ("(" ^ ct ^ ","), Pretty.brk 1, eq'', Pretty.str ")"]]
+ end;
+
+ val default = if d then
+ let
+ val Some s = assoc (thm_bs, f);
+ val ct = variant vs' "ct"
+ in [Pretty.brk 1, Pretty.str "handle", Pretty.brk 1,
+ Pretty.str "Match =>", Pretty.brk 1, mk_let "let" 2
+ (ty_vals @ (if null (term_tvars f) then [] else
+ [mk_val [s] [inst_ty false ty_bs f s]]) @
+ [mk_val [ct] [mk_apps "Thm.capply" false (Pretty.str s)
+ (map Pretty.str args)]])
+ [Pretty.str ("(" ^ ct ^ ","), Pretty.brk 1,
+ Pretty.str "Thm.reflexive", Pretty.brk 1, Pretty.str (ct ^ ")")]]
+ end
+ else []
+ in
+ ("and ", Pretty.block (separate (Pretty.brk 1)
+ (Pretty.str (prfx ^ fname) :: map Pretty.str args) @
+ [Pretty.str " =", Pretty.brk 1, Pretty.str "(case", Pretty.brk 1,
+ Pretty.list "(" ")" (map (fn s => Pretty.str ("term_of " ^ s)) args),
+ Pretty.str " of", Pretty.brk 1] @
+ flat (separate [Pretty.brk 1, Pretty.str "| "]
+ (map (single o mk_eqn_code) eqns)) @ [Pretty.str ")"] @ default))
+ end;
+
+ val (_, decls) = foldl_map mk_fun_code ("fun ", map snd fs')
+ in
+ mk_let "local" 2 (case_vals @ thm_vals) (separate Pretty.fbrk decls)
+ end;
+
+fun mk_simprocs_code sg eqns =
+ let
+ val case_tab = get_cases sg;
+ fun get_head th = head_of (fst (Logic.dest_equals (prop_of th)));
+ fun attach_term (x as (_, _, (_, th) :: _)) = (get_head th, x);
+ val eqns' = map attach_term eqns;
+ fun mk_node (s, _, (_, th) :: _) = (s, get_head th);
+ fun mk_edges (s, _, ths) = map (pair s) (distinct
+ (mapfilter (fn t => apsome #1 (lookup sg eqns' t))
+ (flat (map (term_consts' o prop_of o snd) ths))));
+ val gr = foldr (uncurry Graph.add_edge)
+ (map (pair "" o #1) eqns @ flat (map mk_edges eqns),
+ foldr (uncurry Graph.new_node)
+ (("", Bound 0) :: map mk_node eqns, Graph.empty));
+ val keys = rev (Graph.all_succs gr [""] \ "");
+ fun gr_ord (x :: _, y :: _) =
+ int_ord (find_index (equal x) keys, find_index (equal y) keys);
+ val scc = map (fn xs => filter (fn (_, (s, _, _)) => s mem xs) eqns')
+ (sort gr_ord (Graph.strong_conn gr \ [""]));
+ in
+ flat (separate [Pretty.str ";", Pretty.fbrk, Pretty.str " ", Pretty.fbrk]
+ (map (fn eqns'' => [mk_funs_code sg case_tab eqns' eqns'']) scc)) @
+ [Pretty.str ";", Pretty.fbrk]
+ end;
+
+fun use_simprocs_code sg eqns =
+ let
+ fun attach_name (i, x) = (i+1, ("simp_thm_" ^ string_of_int i, x));
+ fun attach_names (i, (s, b, eqs)) =
+ let val (i', eqs') = foldl_map attach_name (i, eqs)
+ in (i', (s, b, eqs')) end;
+ val (_, eqns') = foldl_map attach_names (1, eqns);
+ val (names, thms) = split_list (flat (map #3 eqns'));
+ val s = setmp print_mode [] Pretty.string_of
+ (mk_let "local" 2 [mk_vall names [Pretty.str "!SimprocsCodegen.simp_thms"]]
+ (mk_simprocs_code sg eqns'))
+ in
+ (simp_thms := thms; use_text Context.ml_output false s)
+ end;
+
+end;