--- a/src/HOL/ex/NormalForm.thy Tue Jul 25 16:43:33 2006 +0200
+++ b/src/HOL/ex/NormalForm.thy Tue Jul 25 16:43:47 2006 +0200
@@ -104,11 +104,7 @@
normal_form "last[a,b,c]"
normal_form "last([a,b,c]@xs)"
-(* FIXME
- won't work since it relies on
- polymorphically used ad-hoc overloaded function:
- normal_form "max 0 (0::nat)"
-*)
+normal_form "max 0 x"
text {*
Numerals still take their time\<dots>
--- a/src/Pure/Tools/class_package.ML Tue Jul 25 16:43:33 2006 +0200
+++ b/src/Pure/Tools/class_package.ML Tue Jul 25 16:43:47 2006 +0200
@@ -33,6 +33,7 @@
val certify_sort: theory -> sort -> sort
val read_sort: theory -> string -> sort
val operational_sort_of: theory -> sort -> sort
+ val operational_algebra: theory -> Sorts.algebra
val the_superclasses: theory -> class -> class list
val the_consts_sign: theory -> class -> string * (string * typ) list
val the_inst_sign: theory -> class * string -> (string * sort) list * (string * typ) list
@@ -133,6 +134,10 @@
|> Option.map (not o null o #consts o fst)
|> the_default false;
+fun operational_algebra thy =
+ Sorts.project_algebra (Sign.pp thy)
+ (is_operational_class thy) (Sign.classes_of thy);
+
fun operational_sort_of thy =
let
fun get_sort class =
--- a/src/Pure/Tools/codegen_package.ML Tue Jul 25 16:43:33 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML Tue Jul 25 16:43:47 2006 +0200
@@ -668,7 +668,7 @@
| SOME (funn, sorts) => fold_map (fn (sort, sort_ctxt) =>
fold_map (exprgen_classlookup thy tabs)
(ClassPackage.sortlookup thy (sort, TFree sort_ctxt)))
- (print sorts ~~ print operational_arity)
+ (sorts ~~ operational_arity)
#-> (fn lss =>
pair (idf_of_name thy nsp_mem m, ((idf_of_name thy nsp_instmem m, funn), lss))));
in
@@ -977,15 +977,18 @@
fun purge_defs NONE thy =
map_module (K CodegenThingol.empty_module) thy
+ | purge_defs (SOME []) thy =
+ thy
| purge_defs (SOME cs) thy =
- let
+ map_module (K CodegenThingol.empty_module) thy;
+ (*let
val tabs = mk_tabs thy NONE;
val idfs = map (idf_of_const' thy tabs) cs;
fun purge idfs modl =
CodegenThingol.purge_module (filter (can (get_def modl)) idfs) modl
in
map_module (purge idfs) thy
- end;
+ end;*)
fun expand_module targets init gen arg thy =
thy
@@ -1065,7 +1068,7 @@
fun read_quote get reader gen raw thy =
thy
- |> expand_module NONE ((SOME o get) thy)
+ |> expand_module (SOME (Symtab.keys (#target_data (CodegenData.get thy)))) ((SOME o get) thy)
(fn thy => fn tabs => gen thy tabs o single o reader thy) raw
|-> (fn [x] => pair x);
@@ -1216,7 +1219,7 @@
Symtab.lookup s_class,
(Option.map fst oo Symtab.lookup) s_tyco,
(Option.map fst oo Symtab.lookup) s_const
- ) ([] (*TODO: add seri_defs here*), cs) module : unit; thy)
+ ) (Symtab.keys s_class @ Symtab.keys s_tyco @ Symtab.keys s_const, cs) module : unit; thy)
end;
in
thy
--- a/src/Pure/Tools/codegen_serializer.ML Tue Jul 25 16:43:33 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML Tue Jul 25 16:43:47 2006 +0200
@@ -9,7 +9,7 @@
signature CODEGEN_SERIALIZER =
sig
type 'a pretty_syntax;
- type serializer =
+ type serializer =
string list list
-> OuterParse.token list ->
((string -> string option)
@@ -26,6 +26,12 @@
haskell: string * (string * string list -> serializer)
};
val mk_flat_ml_resolver: string list -> string -> string;
+ val eval_term: string -> string list list
+ -> (string -> CodegenThingol.itype pretty_syntax option)
+ * (string -> CodegenThingol.iterm pretty_syntax option)
+ -> string list
+ -> (string * 'a ref) * CodegenThingol.iterm -> CodegenThingol.module
+ -> 'a;
val ml_fun_datatype: string
-> ((string -> CodegenThingol.itype pretty_syntax option)
* (string -> CodegenThingol.iterm pretty_syntax option))
@@ -86,7 +92,7 @@
gen_brackify (eval_fxy (INFX infx) fxy_ctxt) (Pretty.breaks ps);
fun from_app mk_app from_expr const_syntax fxy (const as (c, _), es) =
- case (const_syntax c)
+ case const_syntax c
of NONE => brackify fxy (mk_app c es)
| SOME ((i, k), pr) =>
if i <= length es
@@ -193,7 +199,7 @@
(* generic abstract serializer *)
-type serializer =
+type serializer =
string list list
-> OuterParse.token list ->
((string -> string option)
@@ -212,6 +218,8 @@
|> postprocess (resolv name_qual);
in
module
+ |> debug_msg (fn _ => "dropping shadowed defintions...")
+ |> CodegenThingol.delete_garbage drop
|> debug_msg (fn _ => "selecting submodule...")
|> (if is_some select then (CodegenThingol.project_module o the) select else I)
|> debug_msg (fn _ => "serializing...")
@@ -227,7 +235,7 @@
andalso not (NameSpace.separator = c)
then c
else "_"
- fun suffix_it name =
+ fun suffix_it name=
name
|> member (op =) keywords ? suffix "'"
|> (fn name' => if name = name' then name else suffix_it name')
@@ -363,7 +371,7 @@
case sort
of [class] => mk_class class
| _ => Pretty.enum " *" "" "" (map mk_class sort),
- str ")"
+ str ")"
]
end;
fun ml_from_sortlookup fxy lss =
@@ -464,7 +472,7 @@
| ml_from_expr _ (IChar (c, _)) =
(str o prefix "#" o quote)
(let val i = (Char.ord o the o Char.fromString) c
- in if i < 32
+ in if i < 32
then prefix "\\" (string_of_int i)
else c
end)
@@ -474,7 +482,7 @@
fun mk_val ((ve, vty), se) = Pretty.block [
(Pretty.block o Pretty.breaks) [
str "val",
- ml_from_expr NOBR ve,
+ ml_from_expr NOBR ve,
str "=",
ml_from_expr NOBR se
],
@@ -574,7 +582,7 @@
map ml_from_tyvar sortctxt
@ map2 mk_arg pats
((curry Library.take (length pats) o fst o CodegenThingol.unfold_fun) ty))
- @ [str "=", ml_from_expr NOBR expr]
+ @ [str "=", ml_from_expr NOBR expr]
)
in
(Pretty.block o Pretty.fbreaks o shift) (
@@ -629,7 +637,7 @@
| (name, CodegenThingol.Datatypecons _) => NONE
| (name, def) => error ("datatype block containing illegal def: "
^ (Pretty.output o CodegenThingol.pretty_def) def));
- fun filter_class defs =
+ fun filter_class defs =
case map_filter
(fn (name, CodegenThingol.Class info) => SOME (name, info)
| (name, CodegenThingol.Classmember _) => NONE
@@ -659,7 +667,7 @@
fun from_membr_fun (m, _) =
(Pretty.block o Pretty.breaks) [
str "fun",
- (str o resolv) m,
+ (str o resolv) m,
Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ resolv name)],
str "=",
Pretty.block [str "#", ml_from_label m],
@@ -689,7 +697,7 @@
ml_from_type NOBR ty,
str ";"
]
- ) |> SOME
+ ) |> SOME
| ml_from_def (name, CodegenThingol.Classinst (((class, (tyco, arity)), suparities), memdefs)) =
let
val definer = if null arity then "val" else "fun"
@@ -756,9 +764,7 @@
fun is_cons c = CodegenThingol.has_nsp c nsp_dtcon;
in is_cons end;
-in
-
-fun ml_from_thingol target nsp_dtcon nspgrp =
+fun ml_serializer root_name target nsp_dtcon nspgrp =
let
fun ml_from_module resolv _ ((_, name), ps) =
Pretty.chunks ([
@@ -770,23 +776,18 @@
str ("end; (* struct " ^ name ^ " *)")
]);
val is_cons = ml_annotators nsp_dtcon;
- val serializer = abstract_serializer (target, nspgrp)
- "ROOT" (ml_from_defs is_cons, ml_from_module,
- abstract_validator reserved_ml, snd);
- fun eta_expander module const_syntax s =
- case const_syntax s
- of SOME ((i, _), _) => i
- | _ => if CodegenThingol.has_nsp s nsp_dtcon
- then case CodegenThingol.get_def module s
- of CodegenThingol.Datatypecons dtname =>
- case CodegenThingol.get_def module dtname
- of CodegenThingol.Datatype (_, cs) =>
- let val l = AList.lookup (op =) cs s |> the |> length
- in if l >= 2 then l else 0 end
- else 0;
+ in abstract_serializer (target, nspgrp)
+ root_name (ml_from_defs is_cons, ml_from_module,
+ abstract_validator reserved_ml, snd) end;
+
+in
+
+fun ml_from_thingol target nsp_dtcon nspgrp =
+ let
+ val serializer = ml_serializer "ROOT" target nsp_dtcon nspgrp
val parse_multi =
OuterParse.name
- #-> (fn "dir" =>
+ #-> (fn "dir" =>
parse_multi_file
(K o SOME o str o suffix ";" o prefix "val _ = use "
o quote o suffix ".ML" o translate_string (fn "." => "/" | s => s)) "ML" serializer
@@ -798,6 +799,19 @@
|| parse_single_file serializer
end;
+fun eval_term nsp_dtcon nspgrp (syntax_tyco, syntax_const) hidden ((ref_name, reff), e) modl =
+ let
+ val (val_name, modl') = CodegenThingol.add_eval_def e modl;
+ val struct_name = "EVAL";
+ val serializer = ml_serializer struct_name "ml" nsp_dtcon nspgrp
+ (fn "" => (fn p => (use_text Context.ml_output false (Pretty.output p); NONE))
+ | _ => SOME) (K NONE, syntax_tyco, syntax_const) (hidden, SOME [val_name]);
+ val _ = serializer modl';
+ val val_name_struct = NameSpace.append struct_name val_name;
+ val _ = use_text Context.ml_output false ("val _ = (" ^ ref_name ^ " := " ^ val_name_struct ^ ")");
+ val value = ! reff;
+ in value end;
+
fun mk_flat_ml_resolver names =
let
val mangler =
@@ -811,6 +825,9 @@
end; (* local *)
+
+(** haskell serializer **)
+
local
fun hs_from_defs (is_cons, with_typs) (class_syntax, tyco_syntax, const_syntax)
@@ -829,7 +846,7 @@
|> map (fn (v, cls) => str (from_class cls ^ " " ^ v))
|> Pretty.enum "," "(" ")"
|> (fn p => Pretty.block [p, str " => "])
- in
+ in
vs
|> map (fn (v, sort) => map (pair v) sort)
|> flat
@@ -888,7 +905,7 @@
| hs_from_expr fxy (IChar (c, _)) =
(str o enclose "'" "'")
(let val i = (Char.ord o the o Char.fromString) c
- in if i < 32
+ in if i < 32
then Library.prefix "\\" (string_of_int i)
else c
end)
@@ -995,7 +1012,7 @@
end
| hs_from_def (_, CodegenThingol.Classmember _) =
NONE
- | hs_from_def (_, CodegenThingol.Classinst (((clsname, (tyco, arity)), _), memdefs)) =
+ | hs_from_def (_, CodegenThingol.Classinst (((clsname, (tyco, arity)), _), memdefs)) =
Pretty.block [
str "instance ",
hs_from_sctxt arity,
@@ -1041,10 +1058,6 @@
end;
fun serializer with_typs = abstract_serializer (target, nspgrp)
"Main" (hs_from_defs (is_cons, with_typs), hs_from_module, abstract_validator reserved_hs, postproc);
- fun eta_expander const_syntax c =
- const_syntax c
- |> Option.map (fst o fst)
- |> the_default 0;
in
(Scan.optional (OuterParse.name >> (fn "no_typs" => false | s => Scan.fail_with (fn _ => "illegal flag: " ^ quote s) true)) true
#-> (fn with_typs => parse_multi_file ((K o K) NONE) "hs" (serializer with_typs)))
--- a/src/Pure/Tools/codegen_theorems.ML Tue Jul 25 16:43:33 2006 +0200
+++ b/src/Pure/Tools/codegen_theorems.ML Tue Jul 25 16:43:47 2006 +0200
@@ -28,14 +28,15 @@
val get_datatypes: theory -> string
-> (((string * sort) list * (string * typ list) list) * thm list) option;
- (*
type thmtab;
- val get_thmtab: (string * typ) list -> theory -> thmtab * theory;
- val get_cons: thmtab -> string -> string option;
- val get_dtyp: thmtab -> string -> (string * sort) list * (string * typ list) list;
- val get_thms: thmtab -> string * typ -> typ * thm list;
- *)
-
+ val mk_thmtab: (string * typ) list -> theory -> thmtab * theory;
+ val norm_typ: theory -> string * typ -> string * typ;
+ val get_sortalgebra: thmtab -> Sorts.algebra;
+ val get_dtyp_of_cons: thmtab -> string * typ -> string option;
+ val get_dtyp_spec: thmtab -> string
+ -> ((string * sort) list * (string * typ list) list) option;
+ val get_fun_thms: thmtab -> string * typ -> thm list;
+
val print_thms: theory -> unit;
val init_obj: (thm * thm) * (thm * thm) -> theory -> theory;
@@ -87,7 +88,7 @@
fun init_obj ((TrueI, FalseE), (conjI, atomize_eq)) thy =
case CodegenTheoremsSetup.get thy
of SOME _ => error "code generator already set up for object logic"
- | NONE =>
+ | NONE =>
let
fun strip_implies t = (Logic.strip_imp_prems t, Logic.strip_imp_concl t);
fun dest_TrueI thm =
@@ -120,7 +121,7 @@
#> apfst Term.dest_Const
)
|> (fn (v1, ((conj, _), v2)) => if v1 = v2 then conj else error "wrong premise")
- fun dest_atomize_eq thm =
+ fun dest_atomize_eq thm=
Drule.plain_prop_of thm
|> Logic.dest_equals
|> apfst (
@@ -238,7 +239,7 @@
if v = v' orelse member (op =) set v then s
else let
val t = if i = ~1 then Free (v, ty) else Var (v_i, ty)
- in
+ in
(maxidx + 1, v :: set,
(cterm_of thy t, cterm_of thy (Var ((v', maxidx), ty))) :: acc)
end;
@@ -260,7 +261,7 @@
drop (eq::eqs) (filter_out (matches eq) eqs')
in drop [] eqs end;
-fun make_eq thy =
+fun make_eq thy =
let
val ((_, atomize), _) = get_obj thy;
in rewrite_rule [atomize] end;
@@ -368,7 +369,7 @@
};
fun mk_T ((dirty, notify), (preproc, (extrs, funthms))) =
- T { dirty = dirty, notify = notify, preproc = preproc, extrs = extrs, funthms = funthms };
+ T { dirty = dirty, notify = notify, preproc= preproc, extrs = extrs, funthms = funthms };
fun map_T f (T { dirty, notify, preproc, extrs, funthms }) =
mk_T (f ((dirty, notify), (preproc, (extrs, funthms))));
fun merge_T pp (T { dirty = dirty1, notify = notify1, preproc = preproc1, extrs = extrs1, funthms = funthms1 },
@@ -405,7 +406,7 @@
Pretty.str "code generation theorems:",
Pretty.str "function theorems:" ] @
(*Pretty.fbreaks ( *)
- map (fn (c, thms) =>
+ map (fn (c, thms) =>
(Pretty.block o Pretty.fbreaks) (
Pretty.str c :: map pretty_thm (rev thms)
)
@@ -522,7 +523,7 @@
(preprocs, thm :: unfolds)), y)))
|> notify_all NONE;
-fun del_unfold thm =
+fun del_unfold thm =
map_data (fn (x, (preproc, y)) =>
(x, (preproc |> map_preproc (fn (preprocs, unfolds) =>
(preprocs, remove eq_thm thm unfolds)), y)))
@@ -546,6 +547,14 @@
fun extr_typ thy thm = case dest_fun thy thm
of (_, (ty, _)) => ty;
+fun rewrite_rhs conv thm = (case (Drule.strip_comb o cprop_of) thm
+ of (ct', [ct1, ct2]) => (case term_of ct'
+ of Const ("==", _) =>
+ Thm.equal_elim (combination (combination (reflexive ct') (reflexive ct1))
+ (conv ct2)) thm
+ | _ => raise ERROR "rewrite_rhs")
+ | _ => raise ERROR "rewrite_rhs");
+
fun common_typ thy _ [] = []
| common_typ thy _ [thm] = [thm]
| common_typ thy extract_typ thms =
@@ -566,20 +575,13 @@
fun preprocess thy thms =
let
fun burrow_thms f [] = []
- | burrow_thms f thms =
+ | burrow_thms f thms =
thms
|> Conjunction.intr_list
|> f
|> Conjunction.elim_list;
fun cmp_thms (thm1, thm2) =
not (Sign.typ_instance thy (extr_typ thy thm1, extr_typ thy thm2));
- fun rewrite_rhs conv thm = (case (Drule.strip_comb o cprop_of) thm
- of (ct', [ct1, ct2]) => (case term_of ct'
- of Const ("==", _) =>
- Thm.equal_elim (combination (combination (reflexive ct') (reflexive ct1))
- (conv ct2)) thm
- | _ => raise ERROR "rewrite_rhs")
- | _ => raise ERROR "rewrite_rhs");
fun unvarify thms =
#1 (Variable.import true thms (ProofContext.init thy));
val unfold_thms = Tactic.rewrite true (map (make_eq thy) (the_unfolds thy));
@@ -672,7 +674,7 @@
val (_, lhs) = mk_lhs vs args;
in (inj, mk_func thy (lhs, fals) :: dist) end;
fun mk_eqs (vs, cos) =
- let val cos' = rev cos
+ let val cos' = rev cos
in (op @) (fold (mk_eq vs) (product cos' cos') ([], [])) end;
fun mk_eq_thms tac vs_cos =
map (fn t => Goal.prove_global thy [] []
@@ -693,42 +695,150 @@
| _ => []
else [];
-type thmtab = ((thm list Typtab.table Symtab.table
- * string Symtab.table)
- * ((string * sort) list * (string * typ list) list) Symtab.table);
+structure ConstTab = TableFun(type key = string * typ val ord = prod_ord fast_string_ord Term.typ_ord);
+structure ConstGraph = GraphFun(type key = string * typ val ord = prod_ord fast_string_ord Term.typ_ord);
+
+type thmtab = (theory * (thm list ConstGraph.T
+ * string ConstTab.table)
+ * (Sorts.algebra * ((string * sort) list * (string * typ list) list) Symtab.table));
+
+fun thmtab_empty thy = (thy, (ConstGraph.empty, ConstTab.empty),
+ (ClassPackage.operational_algebra thy, Symtab.empty));
+
+fun norm_typ thy (c, ty) =
+ (*more clever: use ty_insts*)
+ case get_first (fn ty' => if Sign.typ_instance thy (ty, (*Logic.varifyT*) ty')
+ then SOME ty' else NONE) (map #lhs (Theory.definitions_of thy c))
+ of NONE => (c, ty)
+ | SOME ty => (c, ty);
+
+fun get_sortalgebra (_, _, (algebra, _)) =
+ algebra;
-(*
-fun mk_thmtab thy cs =
+fun get_dtyp_of_cons (thy, (_, dtcotab), _) (c, ty) =
+ let
+ val (_, ty') = norm_typ thy (c, ty);
+ in ConstTab.lookup dtcotab (c, ty') end;
+
+fun get_dtyp_spec (_, _, (_, dttab)) tyco =
+ Symtab.lookup dttab tyco;
+
+fun has_fun_thms (thy, (fungr, _), _) (c, ty) =
+ let
+ val (_, ty') = norm_typ thy (c, ty);
+ in can (ConstGraph.get_node fungr) (c, ty') end;
+
+fun get_fun_thms (thy, (fungr, _), _) (c, ty) =
+ let
+ val (_, ty') = norm_typ thy (c, ty);
+ in these (try (ConstGraph.get_node fungr) (c, ty')) end;
+
+fun mk_thmtab' thy cs =
let
- fun add_c (c, ty) gr =
- (*
- Das ist noch viel komplizierter: Zyklen
- und die aktuellen Instantiierungen muss man auch noch mitschleppen
- man sieht: man braucht zusätzlich ein Mapping
- c ~> [ty] (Symtab)
- wobei dort immer die bislang allgemeinsten... ???
- *)
- (*
- thm holen für bestimmten typ
- typ dann behalten
- typ normalisieren
- damit haben wir den key
- hier den check machen, ob schon prozessiert wurde
- NEIN:
- ablegen
- consts der rechten Seiten
- in die Rekursion gehen für alles
- JA:
- fertig
- *)
- in fold add_c cs Constgraph.empty end;
+ fun get_dtco_candidate ty =
+ case strip_type ty
+ of (_, Type (tyco, _)) => SOME tyco
+ | _ => NONE;
+ fun add_tycos (Type (tyco, tys)) = insert (op =) tyco #> fold add_tycos tys
+ | add_tycos _ = I;
+ val add_consts = fold_aterms
+ (fn Const c_ty => insert (op =) (norm_typ thy c_ty)
+ | _ => I);
+ fun add_dtyps_of_type ty thmtab =
+ let
+ val tycos = add_tycos ty [];
+ val tycos_new = filter (is_some o get_dtyp_spec thmtab) tycos;
+ fun add_dtyp_spec dtco (dtyp_spec as (vs, cs)) ((thy, (fungr, dtcotab), (algebra, dttab))) =
+ let
+ fun mk_co (c, tys) =
+ (c, Logic.varifyT (tys ---> Type (dtco, map TFree vs)));
+ in
+ (thy, (fungr, dtcotab |> fold (fn c_tys => ConstTab.update_new (mk_co c_tys, dtco)) cs),
+ (algebra, dttab |> Symtab.update_new (dtco, dtyp_spec)))
+ end;
+ in
+ thmtab
+ |> fold (fn tyco => case get_datatypes thy tyco
+ of SOME (dtyp_spec, _) => add_dtyp_spec tyco dtyp_spec
+ | NONE => I) tycos_new
+ end;
+ fun known thmtab (c, ty) =
+ is_some (get_dtyp_of_cons thmtab (c, ty)) orelse has_fun_thms thmtab (c, ty);
+ fun add_funthms (c, ty) (thmtab as (thy, (fungr, dtcotab), algebra_dttab))=
+ if known thmtab (norm_typ thy (c, ty)) then thmtab
+ else let
+ val thms = get_funs thy (c, ty)
+ val cs_dep = fold (add_consts o Thm.prop_of) thms [];
+ in
+ (thy, (fungr |> ConstGraph.new_node ((c, ty), thms)
+ , dtcotab), algebra_dttab)
+ |> fold add_c cs_dep
+ end
+ and add_c (c, ty) thmtab =
+ let
+ val (_, ty') = norm_typ thy (c, ty);
+ in
+ thmtab
+ |> add_dtyps_of_type ty
+ |> add_funthms (c, ty)
+ end;
+ fun narrow_typs fungr =
+ let
+ (*
+ (*!!!remember whether any instantiation had been applied!!!*)
+ fun narrow_thms insts thms =
+ let
+ val (c_def, ty_def) =
+ (norm_typ thy o dest_Const o fst o Logic.dest_equals o Thm.prop_of o hd) thms;
+ val cs = fold (add_consts o snd o Logic.dest_equals o Thm.prop_of) thms [];
+ fun eval_inst c (inst, ty) =
+ let
+ val inst_ctxt = Sign.const_typargs thy (c, ty);
+ val inst_zip = fold (fn (v, ty) => (ty, (the o AList.lookup (op =) inst_ctxt) v)) inst
+ fun add_inst (ty_inst, ty_ctxt) =
+ if Sign.typ_instance thy (ty_inst, ty_ctxt)
+ then I
+ else Sign.typ_match thy (ty_ctxt, ty_inst);
+ in fold add_inst inst_zip end;
+ val inst =
+ Vartab.empty
+ |> fold (fn c_ty as (c, ty) =>
+ case ConstTab.lookup insts (norm_typ thy c_ty)
+ of NONE => I
+ | SOME inst => eval_inst c (inst, ty)) cs
+ |> Vartab.dest
+ |> map (fn (v, (_, ty)) => (v, ty));
+ val instT = map (fn (v, ty) =>
+ (Thm.ctyp_of thy (TVar v, Thm.ctyp_of thy ty))) inst;
+ val thms' =
+ if null inst then NONE thms else
+ map Thm.instantiate (instT, []) thms;
+ val inst' = if null inst then NONE
+ else SOME inst;
+ in (inst', thms') end;
+ fun narrow_css [c] (insts, fungr) =
+ (* HIER GEHTS WEITER *)
+ (insts, fungr)
+ | narrow_css css (insts, fungr) =
+ (insts, fungr)
+ *)
+ val css = rev (Graph.strong_conn fungr);
+ in
+ (ConstTab.empty, fungr)
+ (*|> fold narrow_css css*)
+ |> snd
+ end;
+ in
+ thmtab_empty thy
+ |> fold add_c cs
+(* |> (apfst o apfst) narrow_typs *)
+ end;
-fun get_thmtab cs thy =
+fun mk_thmtab cs thy =
thy
|> get_reset_dirty
- |-> (fn _ => I)
- |> `mk_thmtab;
-*)
+ |> snd
+ |> `(fn thy => mk_thmtab' thy cs);
(** code attributes and setup **)
--- a/src/Pure/Tools/codegen_thingol.ML Tue Jul 25 16:43:33 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML Tue Jul 25 16:43:47 2006 +0200
@@ -67,7 +67,7 @@
datatype def =
Bot
| Fun of funn
- | Typesyn of (vname * sort) list * itype
+ | Typesyn of sortcontext * itype
| Datatype of datatyp
| Datatypecons of string
| Class of class list * (vname * (string * (sortcontext * itype)) list)
@@ -80,7 +80,7 @@
type transact;
type 'dst transact_fin;
val pretty_def: def -> Pretty.T;
- val pretty_module: module -> Pretty.T;
+ val pretty_module: module -> Pretty.T;
val pretty_deps: module -> Pretty.T;
val empty_module: module;
val get_def: module -> string -> def;
@@ -88,6 +88,8 @@
val diff_module: module * module -> (string * def) list;
val project_module: string list -> module -> module;
val purge_module: string list -> module -> module;
+ val add_eval_def: iterm -> module -> string * module;
+ val delete_garbage: string list (*hidden definitions*) -> module -> module;
val has_nsp: string -> string -> bool;
val ensure_def: (string -> transact -> def transact_fin) -> bool -> string
-> string -> transact -> transact;
@@ -232,7 +234,7 @@
| _ => NONE);
val unfold_abs = unfoldr
- (fn (v, ty) `|-> (e as ICase (((IVar w, _), [(se, be)]), _)) =>
+ (fn (v, ty) `|-> (e as ICase (((IVar w, _), [(se, be)]), _)) =>
if v = w then SOME ((se, ty), be) else SOME ((IVar v, ty), e)
| (v, ty) `|-> e => SOME ((IVar v, ty), e)
| _ => NONE)
@@ -241,7 +243,7 @@
(fn ICase (((de, dty), [(se, be)]), _) => SOME (((se, dty), de), be)
| _ => NONE);
-fun unfold_const_app e =
+fun unfold_const_app e =
case unfold_app e
of (IConst x, es) => SOME (x, es)
| _ => NONE;
@@ -323,8 +325,8 @@
add_constnames e
| add_constnames (INum _) =
I
- | add_constnames (IChar _) =
- I
+ | add_constnames (IChar (_, e)) =
+ add_constnames e
| add_constnames (ICase (_, e)) =
add_constnames e;
@@ -383,10 +385,10 @@
datatype def =
Bot
| Fun of funn
- | Typesyn of (vname * sort) list * itype
+ | Typesyn of sortcontext * itype
| Datatype of datatyp
| Datatypecons of string
- | Class of class list * (vname * (string * (sortcontext * itype)) list)
+| Class of class list * (vname * (string * (sortcontext * itype)) list)
| Classmember of class
| Classinst of ((class * (string * (vname * sort) list))
* (class * iclasslookup list) list)
@@ -633,7 +635,7 @@
fun diff_module modl12 =
let
- fun diff_entry prefix modl2 (name, Def def1) =
+ fun diff_entry prefix modl2 (name, Def def1) =
let
val e2 = try (Graph.get_node modl2) name
in if is_some e2 andalso eq_def (def1, (dest_def o the) e2)
@@ -660,7 +662,7 @@
|> (pair defs #> PN);
fun select (PN (defs, modls)) (Module module) =
module
- |> Graph.project (member (op =) (Graph.all_succs module (defs @ map fst modls)))
+ |> Graph.project (member (op =) ((*!*) Graph.all_succs module (defs @ map fst modls)))
|> fold (fn (name, modls) => Graph.map_node name (select modls)) modls
|> Module;
in
@@ -682,8 +684,10 @@
let
val (ndefs, nmodls) = split_names names;
in
- modl
+ modl
|> Graph.del_nodes (Graph.all_preds modl ndefs)
+ |> Graph.del_nodes ndefs
+ |> Graph.del_nodes (Graph.all_preds modl (map fst nmodls))
|> fold (fn (nmodl, names') => Graph.map_node nmodl (purge names')) nmodls
|> Module
end;
@@ -693,6 +697,145 @@
|> dest_modl
end;
+val add_deps_of_sortctxt =
+ fold (fn (v : vname, sort : sort) => fold (insert (op =)) sort);
+
+fun add_deps_of_classlookup (Instance (tyco, lss)) =
+ insert (op =) tyco
+ #> (fold o fold) add_deps_of_classlookup lss
+ | add_deps_of_classlookup (Lookup (clss, _)) =
+ fold (insert (op =)) clss;
+
+fun add_deps_of_type (tyco `%% tys) =
+ insert (op =) tyco
+ #> fold add_deps_of_type tys
+ | add_deps_of_type (ty1 `-> ty2) =
+ add_deps_of_type ty1
+ #> add_deps_of_type ty2
+ | add_deps_of_type (ITyVar v) =
+ I;
+
+fun add_deps_of_term (IConst (c, (lss, ty))) =
+ insert (op =) c
+ #> add_deps_of_type ty
+ #> (fold o fold) add_deps_of_classlookup lss
+ | add_deps_of_term (IVar _) =
+ I
+ | add_deps_of_term (e1 `$ e2) =
+ add_deps_of_term e1 #> add_deps_of_term e2
+ | add_deps_of_term ((_, ty) `|-> e) =
+ add_deps_of_type ty
+ #> add_deps_of_term e
+ | add_deps_of_term (INum _) =
+ I
+ | add_deps_of_term (IChar (_, e)) =
+ add_deps_of_term e
+ | add_deps_of_term (ICase (_, e)) =
+ add_deps_of_term e;
+
+fun deps_of Bot =
+ []
+ | deps_of (Fun (eqs, (sctxt, ty))) =
+ []
+ |> add_deps_of_sortctxt sctxt
+ |> add_deps_of_type ty
+ |> fold (fn (lhs, rhs) => fold add_deps_of_term lhs #> add_deps_of_term rhs) eqs
+ | deps_of (Typesyn (sctxt, ty)) =
+ []
+ |> add_deps_of_sortctxt sctxt
+ |> add_deps_of_type ty
+ | deps_of (Datatype (sctxt, cos)) =
+ []
+ |> add_deps_of_sortctxt sctxt
+ |> fold (fn (c, tys) => insert (op =) c #> fold add_deps_of_type tys) cos
+ | deps_of (Datatypecons dtco) =
+ [dtco]
+ | deps_of (Class (supclss, (_, memdecls))) =
+ []
+ |> fold (insert (op =)) supclss
+ |> fold (fn (name, (sctxt, ty)) =>
+ insert (op =) name
+ #> add_deps_of_sortctxt sctxt
+ #> add_deps_of_type ty
+ ) memdecls
+ | deps_of (Classmember class) =
+ [class]
+ | deps_of (Classinst (((class, (tyco, sctxt)), suparities), memdefs)) =
+ []
+ |> insert (op =) class
+ |> insert (op =) tyco
+ |> add_deps_of_sortctxt sctxt
+ |> fold (fn (supclass, ls) =>
+ insert (op =) supclass
+ #> fold add_deps_of_classlookup ls
+ ) suparities
+ |> fold (fn (name, ((_, (eqs, (sctxt, ty))), lss)) =>
+ insert (op =) name
+ #> add_deps_of_sortctxt sctxt
+ #> add_deps_of_type ty
+ #> fold (fn (lhs, rhs) => fold add_deps_of_term lhs #> add_deps_of_term rhs) eqs
+ #> (fold o fold) add_deps_of_classlookup lss
+ ) memdefs
+ | deps_of Classinstmember =
+ [];
+
+fun delete_garbage hidden modl =
+ let
+ fun allnames modl =
+ let
+ val entries = AList.make (Graph.get_node modl) (Graph.keys modl)
+ fun is_def (name, Module _) = NONE
+ | is_def (name, _) = SOME name;
+ fun is_modl (name, Module modl) = SOME (name, modl)
+ | is_modl (name, _) = NONE;
+ val defs = map_filter is_def entries;
+ val modls = map_filter is_modl entries;
+ in
+ defs
+ @ maps (fn (name, modl) => map (NameSpace.append name) (allnames modl)) modls
+ end;
+ fun alldeps modl =
+ let
+ val entries = AList.make (Graph.get_node modl) (Graph.keys modl)
+ fun is_def (name, Module _) = NONE
+ | is_def (name, _) = SOME name;
+ fun is_modl (name, Module modl) = SOME (name, modl)
+ | is_modl (name, _) = NONE;
+ val defs = map_filter is_def entries;
+ val modls = map_filter is_modl entries;
+ in
+ maps (fn name => map (pair (name)) (Graph.imm_succs modl name)) defs
+ @ maps (fn (name, modl) => (map o pairself) (NameSpace.append name) (alldeps modl)) modls
+ end;
+ val names = subtract (op =) hidden (allnames modl);
+ (*val _ = writeln "HIDDEN";
+ val _ = (writeln o commas) hidden;
+ val _ = writeln "NAMES";
+ val _ = (writeln o commas) names;*)
+ fun is_bot name =
+ case get_def modl name of Bot => true | _ => false;
+ val bots = filter is_bot names;
+ val defs = filter (not o is_bot) names;
+ val expldeps =
+ Graph.empty
+ |> fold (fn name => Graph.new_node (name, ())) names
+ |> fold (fn name => fold (curry Graph.add_edge name)
+ (deps_of (get_def modl name) |> subtract (op =) hidden)) names
+ val bots' = fold (insert op =) bots (Graph.all_preds expldeps bots);
+ val selected = subtract (op =) bots' names;
+(* val deps = filter (fn (x, y) => member (op =) selected x andalso member (op =) selected y) *)
+ val adddeps = maps (fn (n, ns) => map (pair n) ns) (expldeps |> Graph.del_nodes bots' |> Graph.dest);
+ (*val _ = writeln "SELECTED";
+ val _ = (writeln o commas) selected;
+ val _ = writeln "DEPS";
+ val _ = (writeln o cat_lines o map (fn (x, y) => x ^ " -> " ^ y)) adddeps;*)
+ in
+ empty_module
+ |> fold (fn name => add_def (name, get_def modl name)) selected
+(* |> fold ensure_bot (hidden @ bots') *)
+ |> fold (fn (x, y) => (writeln ("adding " ^ x ^ " -> " ^ y); add_dep (x, y))) adddeps
+ end;
+
fun allimports_of modl =
let
fun imps_of prfx (Module modl) imps tab =
@@ -704,10 +847,10 @@
|> pair []
|> fold (fn names => fn (imps', tab) =>
tab
- |> fold_map (fn name =>
+ |> fold_map (fn name =>
imps_of (prfx @ [name]) (Graph.get_node modl name) (imps' @ imps)) names
|-> (fn imps'' => pair (flat imps'' @ imps'))) name_con
- |-> (fn imps' =>
+ |-> (fn imps' =>
Symtab.update_new (this, imps' @ imps)
#> pair (this :: imps'))
end
@@ -769,7 +912,7 @@
in if eq_ityp ((sortctxt'', ty''), (sortctxt', ty'))
then (m, ((m', (check_funeqs eqs, (sortctxt', ty'))), lss))
else
- error ("inconsistent type for member definition " ^ quote m ^ " [" ^ v ^ "]: "
+ error ("inconsistent type for member definition " ^ quote m ^ " [" ^ v ^ "]: "
^ (Pretty.output o Pretty.block o Pretty.breaks) [
pretty_sortcontext sortctxt'',
Pretty.str "|=>",
@@ -826,12 +969,12 @@
fun prep_def def modl =
(check_prep_def modl def, modl);
fun invoke_generator name defgen modl =
- if ! soft_exc (*that's ! isn't a "not"...*)
+ if ! soft_exc (*that "!" isn't a "not"...*)
then defgen name (SOME name, modl)
handle FAIL (msgs, exc) =>
if strict then raise FAIL (msg' :: msgs, exc)
else (Bot, modl)
- | e => raise
+ | e => raise
FAIL (["definition generator for " ^ quote name, msg'], SOME e)
else defgen name (SOME name, modl)
handle FAIL (msgs, exc) =>
@@ -885,6 +1028,15 @@
|-> (fn x => fn (_, modl) => (x, modl))
end;
+fun add_eval_def e modl =
+ let
+ val name = hd (Name.invent_list (Graph.keys modl) "VALUE" 1);
+ in
+ modl
+ |> add_def (name, Fun ([([], e)], ([], "" `%% [])))
+ |> fold (curry add_dep name) (add_deps_of_term e [])
+ |> pair name
+ end;
(** generic serialization **)
@@ -954,7 +1106,7 @@
in ([p'], tab') end
| get_path_name [p1, p2] tab =
(case Symtab.lookup tab p1
- of SOME (N (p', SOME tab')) =>
+ of SOME (N (p', SOME tab')) =>
let
val (ps', tab'') = get_path_name [p2] tab'
in (p' :: ps', tab'') end
@@ -987,16 +1139,19 @@
let
val name_qual = NameSpace.pack (prfx @ [name])
in (name_qual, resolver prfx name_qual) end;
+ fun is_bot (_, (Def Bot)) = true
+ | is_bot _ = false;
fun mk_contents prfx module =
map_filter (seri prfx)
((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)
and seri prfx [(name, Module modl)] =
seri_module (resolver []) (map (resolver []) ((the o Symtab.lookup imptab) (NameSpace.pack (prfx @ [name]))))
(mk_name prfx name, mk_contents (prfx @ [name]) modl)
- | seri prfx [(_, Def Bot)] = NONE
| seri prfx ds =
- seri_defs sresolver (NameSpace.pack prfx)
- (map (fn (name, Def def) => (fst (mk_name prfx name), def)) ds)
+ case filter_out is_bot ds
+ of [] => NONE
+ | ds' => seri_defs sresolver (NameSpace.pack prfx)
+ (map (fn (name, Def def) => (fst (mk_name prfx name), def (*|> tap (Pretty.writeln o pretty_def)*))) ds')
in
seri_module (resolver []) (map (resolver []) ((the o Symtab.lookup imptab) ""))
(("", name_root), (mk_contents [] module))
--- a/src/Pure/Tools/nbe.ML Tue Jul 25 16:43:33 2006 +0200
+++ b/src/Pure/Tools/nbe.ML Tue Jul 25 16:43:47 2006 +0200
@@ -83,12 +83,11 @@
val _ = trace (fn () => "Input:\n" ^ Display.raw_string_of_term t);
fun compile_term t thy =
let
- val (modl_this, thy') = CodegenPackage.get_root_module thy;
+ val thy' = CodegenPackage.purge_code thy;
val nbe_tab = NBE_Data.get thy';
- val modl_old = CodegenThingol.project_module (Symtab.keys nbe_tab) modl_this;
val (t', thy'') = CodegenPackage.codegen_term t thy';
val (modl_new, thy''') = CodegenPackage.get_root_module thy'';
- val diff = CodegenThingol.diff_module (modl_new, modl_old);
+ val diff = CodegenThingol.diff_module (modl_new, CodegenThingol.empty_module);
val _ = trace (fn () => "new definitions: " ^ (commas o map fst) diff);
val _ = (tab := nbe_tab;
Library.seq (use_code o NBE_Codegen.generate defined) diff);