# HG changeset patch # User haftmann # Date 1153838627 -7200 # Node ID b43fd26e1aaa8edd756b023494a3536ffa233ba3 # Parent 03a8d7c070d3af9abb3114330bd772f84d8cb2d6 improvements for lazy code generation diff -r 03a8d7c070d3 -r b43fd26e1aaa src/HOL/ex/NormalForm.thy --- 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\ diff -r 03a8d7c070d3 -r b43fd26e1aaa src/Pure/Tools/class_package.ML --- 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 = diff -r 03a8d7c070d3 -r b43fd26e1aaa src/Pure/Tools/codegen_package.ML --- 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 diff -r 03a8d7c070d3 -r b43fd26e1aaa src/Pure/Tools/codegen_serializer.ML --- 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))) diff -r 03a8d7c070d3 -r b43fd26e1aaa src/Pure/Tools/codegen_theorems.ML --- 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 **) diff -r 03a8d7c070d3 -r b43fd26e1aaa src/Pure/Tools/codegen_thingol.ML --- 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)) diff -r 03a8d7c070d3 -r b43fd26e1aaa src/Pure/Tools/nbe.ML --- 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);