# HG changeset patch # User haftmann # Date 1158672146 -7200 # Node ID 6d75e02ed285a15ffbb7a5e5cd592450f2112e30 # Parent 65bd267ae23f3db948ac2e4d4530151b81ea9b57 added codegen_data diff -r 65bd267ae23f -r 6d75e02ed285 src/Pure/Tools/ROOT.ML --- a/src/Pure/Tools/ROOT.ML Tue Sep 19 15:22:24 2006 +0200 +++ b/src/Pure/Tools/ROOT.ML Tue Sep 19 15:22:26 2006 +0200 @@ -14,7 +14,8 @@ (*code generator, 2nd generation*) use "codegen_consts.ML"; use "codegen_names.ML"; -use "codegen_theorems.ML"; +use "codegen_data.ML"; +use "codegen_funcgr.ML"; use "codegen_thingol.ML"; use "codegen_serializer.ML"; use "codegen_simtype.ML"; diff -r 65bd267ae23f -r 6d75e02ed285 src/Pure/Tools/codegen_consts.ML --- a/src/Pure/Tools/codegen_consts.ML Tue Sep 19 15:22:24 2006 +0200 +++ b/src/Pure/Tools/codegen_consts.ML Tue Sep 19 15:22:26 2006 +0200 @@ -12,18 +12,19 @@ val const_ord: const * const -> order val eq_const: const * const -> bool structure Consttab: TABLE - val typinst_of_typ: theory -> string * typ -> const - val typ_of_typinst: theory -> const -> string * typ + val inst_of_typ: theory -> string * typ -> const + val typ_of_inst: theory -> const -> string * typ + val norm: theory -> const -> const + val norm_of_typ: theory -> string * typ -> const val find_def: theory -> const - -> ((string (*theory name*) * string (*definition name*)) * typ list) option + -> ((string (*theory name*) * thm) * typ list) option val sortinsts: theory -> typ * typ -> (typ * sort) list - val norminst_of_typ: theory -> string * typ -> const val class_of_classop: theory -> const -> class option val insts_of_classop: theory -> const -> const list val typ_of_classop: theory -> const -> typ val read_const: theory -> string -> const - val read_const_typ: theory -> string -> string * typ val string_of_const: theory -> const -> string + val raw_string_of_const: const -> string val string_of_const_typ: theory -> string * typ -> string end; @@ -46,10 +47,10 @@ (* type instantiations and overloading *) -fun typinst_of_typ thy (c_ty as (c, ty)) = +fun inst_of_typ thy (c_ty as (c, ty)) = (c, Consts.typargs (Sign.consts_of thy) c_ty); -fun typ_of_typinst thy (c_tys as (c, tys)) = +fun typ_of_inst thy (c_tys as (c, tys)) = (c, Consts.instance (Sign.consts_of thy) c_tys); fun find_def thy (c, tys) = @@ -61,11 +62,15 @@ | instance_tycos (_ , TVar _) = true | instance_tycos ty_ty = Sign.typ_instance thy ty_ty; in instance_tycos end - | NONE => Sign.typ_instance thy + | NONE => Sign.typ_instance thy; + fun get_def (_, { is_def, thyname, name, lhs, rhs }) = + if is_def andalso forall typ_instance (tys ~~ lhs) then + case try (Thm.get_axiom_i thy) name + of SOME thm => SOME ((thyname, thm), lhs) + | NONE => NONE + else NONE in - get_first (fn (_, { is_def, thyname, name, lhs, ... }) => if is_def - andalso forall typ_instance (tys ~~ lhs) - then SOME ((thyname, name), lhs) else NONE) specs + get_first get_def specs end; fun sortinsts thy (ty, ty_decl) = @@ -78,7 +83,7 @@ (c, [Type (tyco, map (fn v => TVar ((v, 0), Sign.defaultS thy (*for monotonicity*))) (Name.invents Name.context "'a" (Sign.arity_number thy tyco)))]); -fun norminst_of_typ thy (c, ty) = +fun norm thy (c, insts) = let fun disciplined _ [(Type (tyco, _))] = mk_classop_typinst thy (c, tyco) @@ -87,15 +92,15 @@ fun ad_hoc c tys = case find_def thy (c, tys) of SOME (_, tys) => (c, tys) - | NONE => typinst_of_typ thy (c, Sign.the_const_type thy c); - val tyinsts = Consts.typargs (Sign.consts_of thy) (c, ty); - in if c = "op =" then disciplined (Sign.defaultS thy) tyinsts - (*the distinction on op = will finally disappear!*) - else case AxClass.class_of_param thy c - of SOME class => disciplined [class] tyinsts - | _ => ad_hoc c tyinsts + | NONE => inst_of_typ thy (c, Sign.the_const_type thy c); + in case AxClass.class_of_param thy c + of SOME class => disciplined [class] insts + | _ => ad_hoc c insts end; +fun norm_of_typ thy (c, ty) = + norm thy (c, Consts.typargs (Sign.consts_of thy) (c, ty)); + fun class_of_classop thy (c, [TVar _]) = AxClass.class_of_param thy c | class_of_classop thy (c, [TFree _]) = @@ -148,12 +153,12 @@ let val t = Sign.read_term thy raw_t in case try dest_Const t - of SOME c_ty => c_ty + of SOME c_ty => (typ_of_inst thy o norm_of_typ thy) c_ty | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t) end; fun read_const thy = - typinst_of_typ thy o read_const_typ thy; + norm_of_typ thy o read_const_typ thy; (* printing constants *) @@ -162,6 +167,10 @@ space_implode " " (Sign.extern_const thy c :: map (enclose "[" "]" o Sign.string_of_typ thy) tys); +fun raw_string_of_const (c, tys) = + space_implode " " (c + :: map (enclose "[" "]" o Display.raw_string_of_typ) tys); + fun string_of_const_typ thy (c, ty) = string_of_const thy (c, Consts.typargs (Sign.consts_of thy) (c, ty)); diff -r 65bd267ae23f -r 6d75e02ed285 src/Pure/Tools/codegen_data.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/codegen_data.ML Tue Sep 19 15:22:26 2006 +0200 @@ -0,0 +1,755 @@ +(* Title: Pure/Tools/codegen_data.ML + ID: $Id$ + Author: Florian Haftmann, TU Muenchen + +Basic code generator data structures; abstract executable content of theory. +*) + +(* val _ = PolyML.Compiler.maxInlineSize := 0; *) + +signature CODEGEN_DATA = +sig + type lthms = thm list Susp.T; + val lazy: (unit -> thm list) -> lthms + val eval_always: bool ref + + val add_func: thm -> theory -> theory + val del_func: thm -> theory -> theory + val add_funcl: CodegenConsts.const * lthms -> theory -> theory + val add_datatype: string * (((string * sort) list * (string * typ list) list) * lthms) + -> theory -> theory + val del_datatype: string -> theory -> theory + val add_inline: thm -> theory -> theory + val del_inline: thm -> theory -> theory + val add_preproc: (theory -> thm list -> thm list) -> theory -> theory + val these_funcs: theory -> CodegenConsts.const -> thm list + val get_datatype: theory -> string + -> ((string * sort) list * (string * typ list) list) option + val get_datatype_of_constr: theory -> CodegenConsts.const -> string option + val the_datatype_constrs: theory -> CodegenConsts.const list + + val print_thms: theory -> unit + + val typ_func: theory -> thm -> typ + val rewrite_func: thm list -> thm -> thm + val preprocess_cterm: theory -> cterm -> thm + val preprocess: theory -> thm list -> thm list + + val debug: bool ref + val strict_functyp: bool ref +end; + +signature PRIVATE_CODEGEN_DATA = +sig + include CODEGEN_DATA + type data + structure CodeData: THEORY_DATA + val declare: string -> Object.T -> (Pretty.pp -> Object.T * Object.T -> Object.T) + -> (CodegenConsts.const list option -> Object.T -> Object.T) -> serial + val init: serial -> theory -> theory + val get: serial -> (Object.T -> 'a) -> data -> 'a + val put: serial -> ('a -> Object.T) -> 'a -> data -> data +end; + +structure CodegenData : PRIVATE_CODEGEN_DATA = +struct + +(** diagnostics **) + +val debug = ref false; +fun debug_msg f x = (if !debug then Output.tracing (f x) else (); x); + + + +(** lazy theorems, certificate theorems **) + +type lthms = thm list Susp.T; +val eval_always = ref false; +val _ = eval_always := true; + +fun lazy f = if !eval_always + then Susp.value (f ()) + else Susp.delay f; + +fun string_of_lthms r = case Susp.peek r + of SOME thms => (map string_of_thm o rev) thms + | NONE => ["[...]"]; + +fun pretty_lthms ctxt r = case Susp.peek r + of SOME thms => (map (ProofContext.pretty_thm ctxt) o rev) thms + | NONE => [Pretty.str "[...]"]; + +fun certificate f r = + case Susp.peek r + of SOME thms => (Susp.value o f) thms + | NONE => lazy (fn () => (f o Susp.force) r); + +fun merge' _ ([], []) = (false, []) + | merge' _ ([], ys) = (true, ys) + | merge' eq (xs, ys) = fold_rev + (fn y => fn (t, xs) => (t orelse not (member eq xs y), insert eq y xs)) ys (false, xs); + +fun merge_alist eq_key eq (xys as (xs, ys)) = + if eq_list (eq_pair eq_key eq) (xs, ys) + then (false, xs) + else (true, AList.merge eq_key eq xys); + +val merge_thms = merge' eq_thm; + +fun merge_lthms (r1, r2) = + if Susp.same (r1, r2) then (false, r1) + else case Susp.peek r1 + of SOME [] => (true, r2) + | _ => case Susp.peek r2 + of SOME [] => (true, r1) + | _ => (apsnd (lazy o K)) (merge_thms (Susp.force r1, Susp.force r2)); + + + +(** code theorems **) + +(* making function theorems *) + +fun bad_thm msg thm = + error (msg ^ ": " ^ string_of_thm thm); + +fun typ_func thy = snd o dest_Const o fst o strip_comb o fst + o Logic.dest_equals o ObjectLogic.drop_judgment thy o Drule.plain_prop_of; + +val mk_rew = + #mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of; + +val strict_functyp = ref true; + +fun mk_func thy raw_thm = + let + fun dest_func thy = dest_Const o fst o strip_comb o Envir.beta_eta_contract + o fst o Logic.dest_equals o ObjectLogic.drop_judgment thy o Drule.plain_prop_of; + fun mk_head thm = case try (dest_func thy) thm + of SOME (c_ty as (c, ty)) => + let + val is_classop = (is_some o AxClass.class_of_param thy) c; + val const = CodegenConsts.norm_of_typ thy c_ty; + val ty_decl = if is_classop + then CodegenConsts.typ_of_classop thy const + else snd (CodegenConsts.typ_of_inst thy const); + val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy); + in if Sign.typ_equiv thy (ty_decl, ty) + then (const, thm) + else ((if is_classop orelse !strict_functyp then error else warning) + ("Type\n" ^ string_of_typ ty + ^ "\nof function theorem\n" + ^ string_of_thm thm + ^ "\nis strictly less general than declared function type\n" + ^ string_of_typ ty_decl); (const, thm)) + end + | NONE => bad_thm "Not a function equation" thm; + in + mk_rew thy raw_thm + |> map mk_head + end; + +fun get_prim_def_funcs thy c = + let + fun constrain thm0 thm = case AxClass.class_of_param thy (fst c) + of SOME _ => + let + val ty_decl = CodegenConsts.typ_of_classop thy c; + val max = maxidx_of_typ ty_decl + 1; + val thm = Thm.incr_indexes max thm; + val ty = typ_func thy thm; + val (env, _) = Sign.typ_unify thy (ty_decl, ty) (Vartab.empty, max); + val instT = Vartab.fold (fn (x_i, (sort, ty)) => + cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env []; + in Thm.instantiate (instT, []) thm end + | NONE => thm + in case CodegenConsts.find_def thy c + of SOME ((_, thm), _) => + thm + |> Thm.transfer thy + |> try (map snd o mk_func thy) + |> these + |> map (constrain thm) + | NONE => [] + end; + + +(* pairs of (selected, deleted) function theorems *) + +type sdthms = lthms * thm list; + +fun add_drop_redundant thm thms = + let + val _ = writeln "add_drop 01"; + val thy = Context.check_thy (Thm.theory_of_thm thm); + val _ = writeln "add_drop 02"; + val pattern = (fst o Logic.dest_equals o Drule.plain_prop_of) thm; + fun matches thm' = if (curry (Pattern.matches thy) pattern o + fst o Logic.dest_equals o Drule.plain_prop_of) thm' + then (warning ("Dropping redundant function theorem\n" ^ string_of_thm thm'); true) + else false + in thm :: filter_out matches thms end; + +fun add_thm thm (sels, dels) = + (Susp.value (add_drop_redundant thm (Susp.force sels)), remove eq_thm thm dels); + +fun add_lthms lthms (sels, []) = + (lazy (fn () => fold add_drop_redundant + (Susp.force lthms) (Susp.force sels)), []) + | add_lthms lthms (sels, dels) = + fold add_thm (Susp.force lthms) (sels, dels); + +fun del_thm thm (sels, dels) = + (Susp.value (remove eq_thm thm (Susp.force sels)), thm :: dels); + +fun pretty_sdthms ctxt (sels, _) = pretty_lthms ctxt sels; + +fun merge_sdthms c ((sels1, dels1), (sels2, dels2)) = + let + val (dels_t, dels) = merge_thms (dels1, dels2); + in if dels_t + then let + val (_, sels) = merge_thms (Susp.force sels1, subtract eq_thm dels1 (Susp.force sels2)) + val (_, dels) = merge_thms (dels1, subtract eq_thm (Susp.force sels1) dels2) + in (true, ((lazy o K) sels, dels)) end + else let + val (sels_t, sels) = merge_lthms (sels1, sels2) + in (sels_t, (sels, dels)) end + end; + + +(** data structures **) + +structure Consttab = CodegenConsts.Consttab; + +datatype preproc = Preproc of { + inlines: thm list, + preprocs: (serial * (theory -> thm list -> thm list)) list +}; + +fun mk_preproc (inlines, preprocs) = + Preproc { inlines = inlines, preprocs = preprocs }; +fun map_preproc f (Preproc { inlines, preprocs }) = + mk_preproc (f (inlines, preprocs)); +fun merge_preproc (Preproc { inlines = inlines1, preprocs = preprocs1 }, + Preproc { inlines = inlines2, preprocs = preprocs2 }) = + let + val (touched1, inlines) = merge_thms (inlines1, inlines2); + val (touched2, preprocs) = merge_alist (op =) (K true) (preprocs1, preprocs2); + in (touched1 orelse touched2, mk_preproc (inlines, preprocs)) end; + +fun join_func_thms (tabs as (tab1, tab2)) = + let + val cs1 = Consttab.keys tab1; + val cs2 = Consttab.keys tab2; + val cs' = filter (member CodegenConsts.eq_const cs2) cs1; + val cs'' = subtract (op =) cs' cs1 @ subtract (op =) cs' cs2; + val cs''' = ref [] : CodegenConsts.const list ref; + fun merge c x = let val (touched, thms') = merge_sdthms c x in + (if touched then cs''' := cons c (!cs''') else (); thms') end; + in (cs'' @ !cs''', Consttab.join merge tabs) end; +fun merge_funcs (thms1, thms2) = + let + val (consts, thms) = join_func_thms (thms1, thms2); + in (SOME consts, thms) end; + +val eq_string = op = : string * string -> bool; +fun eq_dtyp (((vs1, cs1), _), ((vs2, cs2), _)) = + gen_eq_set (eq_pair eq_string (gen_eq_set eq_string)) (vs1, vs2) + andalso gen_eq_set (eq_pair eq_string (eq_list (is_equal o Term.typ_ord))) (cs1, cs2); +fun merge_dtyps (tabs as (tab1, tab2)) = + let + (*EXTEND: could be more clever with respect to constructors*) + val tycos1 = Symtab.keys tab1; + val tycos2 = Symtab.keys tab2; + val tycos' = filter (member eq_string tycos2) tycos1; + val touched = gen_eq_set (eq_pair (op =) (eq_dtyp)) + (AList.make (the o Symtab.lookup tab1) tycos', + AList.make (the o Symtab.lookup tab2) tycos'); + in (touched, Symtab.merge (K true) tabs) end; + +datatype spec = Spec of { + funcs: sdthms Consttab.table, + dconstrs: string Consttab.table, + dtyps: (((string * sort) list * (string * typ list) list) * lthms) Symtab.table +}; + +fun mk_spec ((funcs, dconstrs), dtyps) = + Spec { funcs = funcs, dconstrs = dconstrs, dtyps = dtyps }; +fun map_spec f (Spec { funcs = funcs, dconstrs = dconstrs, dtyps = dtyps }) = + mk_spec (f ((funcs, dconstrs), dtyps)); +fun merge_spec (Spec { funcs = funcs1, dconstrs = dconstrs1, dtyps = dtyps1 }, + Spec { funcs = funcs2, dconstrs = dconstrs2, dtyps = dtyps2 }) = + let + val (touched_cs, funcs) = merge_funcs (funcs1, funcs2); + val dconstrs = Consttab.merge (K true) (dconstrs1, dconstrs2); + val (touched', dtyps) = merge_dtyps (dtyps1, dtyps2); + val touched = if touched' then NONE else touched_cs; + in (touched, mk_spec ((funcs, dconstrs), dtyps)) end; + +datatype exec = Exec of { + preproc: preproc, + spec: spec +}; + +fun mk_exec (preproc, spec) = + Exec { preproc = preproc, spec = spec }; +fun map_exec f (Exec { preproc = preproc, spec = spec }) = + mk_exec (f (preproc, spec)); +fun merge_exec (Exec { preproc = preproc1, spec = spec1 }, + Exec { preproc = preproc2, spec = spec2 }) = + let + val (touched', preproc) = merge_preproc (preproc1, preproc2); + val (touched_cs, spec) = merge_spec (spec1, spec2); + val touched = if touched' then NONE else touched_cs; + in (touched, mk_exec (preproc, spec)) end; +val empty_exec = mk_exec (mk_preproc ([], []), + mk_spec ((Consttab.empty, Consttab.empty), Symtab.empty)); + +fun the_preproc (Exec { preproc = Preproc x, ...}) = x; +fun the_spec (Exec { spec = Spec x, ...}) = x; +val the_funcs = #funcs o the_spec; +val the_dcontrs = #dconstrs o the_spec; +val the_dtyps = #dtyps o the_spec; +val map_preproc = map_exec o apfst o map_preproc; +val map_funcs = map_exec o apsnd o map_spec o apfst o apfst; +val map_dconstrs = map_exec o apsnd o map_spec o apfst o apsnd; +val map_dtyps = map_exec o apsnd o map_spec o apsnd; + + +(** code data structures **) + +(*private copy avoids potential conflict of table exceptions*) +structure Datatab = TableFun(type key = int val ord = int_ord); + + +(* data slots *) + +local + +type kind = { + name: string, + empty: Object.T, + merge: Pretty.pp -> Object.T * Object.T -> Object.T, + purge: CodegenConsts.const list option -> Object.T -> Object.T +}; + +val kinds = ref (Datatab.empty: kind Datatab.table); + +fun invoke meth_name meth_fn k = + (case Datatab.lookup (! kinds) k of + SOME kind => meth_fn kind |> transform_failure (fn exn => + EXCEPTION (exn, "Code data method " ^ #name kind ^ "." ^ meth_name ^ " failed")) + | NONE => sys_error ("Invalid code data identifier " ^ string_of_int k)); + + +in + +fun invoke_name k = invoke "name" (K o #name) k (); +fun invoke_empty k = invoke "empty" (K o #empty) k (); +fun invoke_merge pp = invoke "merge" (fn kind => #merge kind pp); +fun invoke_purge cs = invoke "purge" (fn kind => #purge kind cs); + +fun declare name empty merge purge = + let + val k = serial (); + val kind = {name = name, empty = empty, merge = merge, purge = purge}; + val _ = conditional (Datatab.exists (equal name o #name o #2) (! kinds)) (fn () => + warning ("Duplicate declaration of code data " ^ quote name)); + val _ = change kinds (Datatab.update (k, kind)); + in k end; + +end; (*local*) + + +(* theory store *) + +type data = Object.T Datatab.table; + +structure CodeData = TheoryDataFun +(struct + val name = "Pure/codegen_data"; + type T = exec * data ref; + val empty = (empty_exec, ref Datatab.empty : data ref); + fun copy (exec, data) = (exec, ref (! data)); + val extend = copy; + fun merge pp ((exec1, data1), (exec2, data2)) = + let + val (touched, exec) = merge_exec (exec1, exec2); + val data1' = Datatab.map' (invoke_purge touched) (! data1); + val data2' = Datatab.map' (invoke_purge touched) (! data2); + val data = Datatab.join (invoke_merge pp) (data1', data2'); + in (exec, ref data) end; + fun print thy (exec, _) = + let + val ctxt = ProofContext.init thy; + fun pretty_func (s, lthms) = + (Pretty.block o Pretty.fbreaks) ( + Pretty.str s :: pretty_sdthms ctxt lthms + ); + fun pretty_dtyp (s, cos) = + (Pretty.block o Pretty.breaks) ( + Pretty.str s + :: Pretty.str "=" + :: Pretty.separate "|" (map (fn (c, []) => Pretty.str c + | (c, tys) => + Pretty.block + (Pretty.str c :: Pretty.brk 1 :: Pretty.str "of" :: Pretty.brk 1 + :: Pretty.breaks (map (Pretty.quote o Sign.pretty_typ thy) tys))) cos) + ) + val inlines = (#inlines o the_preproc) exec; + val funs = the_funcs exec + |> Consttab.dest + |> (map o apfst) (CodegenConsts.string_of_const thy) + |> sort (string_ord o pairself fst); + val dtyps = the_dtyps exec + |> Symtab.dest + |> map (fn (dtco, ((vs, cos), _)) => (Sign.string_of_typ thy (Type (dtco, map TFree vs)), cos)) + |> sort (string_ord o pairself fst) + in + (Pretty.writeln o Pretty.block o Pretty.fbreaks) ([ + Pretty.str "code theorems:", + Pretty.str "function theorems:" ] @ + map pretty_func funs @ [ + Pretty.block ( + Pretty.str "inlined theorems:" + :: Pretty.fbrk + :: (Pretty.fbreaks o map (ProofContext.pretty_thm ctxt)) inlines + ), + Pretty.block ( + Pretty.str "datatypes:" + :: Pretty.fbrk + :: (Pretty.fbreaks o map pretty_dtyp) dtyps + )] + ) + end; +end); + +fun print_thms thy = CodeData.print thy; + +fun init k = CodeData.map + (fn (exec, data) => (exec, ref (Datatab.update (k, invoke_empty k) (! data)))); + +fun get k dest data = + (case Datatab.lookup data k of + SOME x => (dest x handle Match => + error ("Failed to access code data " ^ quote (invoke_name k))) + | NONE => error ("Uninitialized code data " ^ quote (invoke_name k))); + +fun put k mk x = Datatab.update (k, mk x); + +fun map_exec_purge touched f = + CodeData.map (fn (exec, data) => + (f exec, ref (Datatab.map' (invoke_purge touched) (! data)))); + +val get_exec = fst o CodeData.get; + +val _ = Context.add_setup CodeData.init; + + + +(** theorem transformation and certification **) + +fun rewrite_func rewrites thm = + let + val rewrite = Tactic.rewrite true rewrites; + val (ct_eq, [ct_lhs, ct_rhs]) = (Drule.strip_comb o cprop_of) thm; + val Const ("==", _) = term_of ct_eq; + val (ct_f, ct_args) = Drule.strip_comb ct_lhs; + val rhs' = rewrite ct_rhs; + val args' = map rewrite ct_args; + val lhs' = Thm.symmetric (fold (fn th1 => fn th2 => Thm.combination th2 th1) + args' (Thm.reflexive ct_f)); + in + Thm.transitive (Thm.transitive lhs' thm) rhs' + end handle Bind => raise ERROR "rewrite_func" + +fun common_typ_funcs thy [] = [] + | common_typ_funcs thy [thm] = [thm] + | common_typ_funcs thy thms = + let + fun incr_thm thm max = + let + val thm' = incr_indexes max thm; + val max' = (maxidx_of_typ o fastype_of o Drule.plain_prop_of) thm' + 1; + in (thm', max') end; + val (thms', maxidx) = fold_map incr_thm thms 0; + val (ty1::tys) = map (typ_func thy) thms; + fun unify ty env = Sign.typ_unify thy (ty1, ty) env + handle Type.TUNIFY => + error ("Type unificaton failed, while unifying function equations\n" + ^ (cat_lines o map Display.string_of_thm) thms + ^ "\nwith types\n" + ^ (cat_lines o map (Sign.string_of_typ thy)) (ty1 :: tys)); + val (env, _) = fold unify tys (Vartab.empty, maxidx) + val instT = Vartab.fold (fn (x_i, (sort, ty)) => + cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env []; + in map (Thm.instantiate (instT, [])) thms end; + +fun certify_const thy c thms = + let + fun cert (c', thm) = if CodegenConsts.eq_const (c, c') + then thm else bad_thm ("Wrong head of function equation,\nexpected constant " + ^ CodegenConsts.string_of_const thy c) thm + in (map cert o maps (mk_func thy)) thms end; + +fun mk_cos tyco vs cos = + let + val dty = Type (tyco, map TFree vs); + fun mk_co (co, tys) = (Const (co, (tys ---> dty)), map I tys); + in map mk_co cos end; + +fun mk_co_args (co, tys) ctxt = + let + val names = Name.invents ctxt "a" (length tys); + val ctxt' = fold Name.declare names ctxt; + val vs = map2 (fn v => fn ty => Free (fst (v, 0), I ty)) names tys; + in (vs, ctxt') end; + +fun check_freeness thy cos thms = + let + val props = AList.make Drule.plain_prop_of thms; + fun sym_product [] = [] + | sym_product (x::xs) = map (pair x) xs @ sym_product xs; + val quodlibet = + let + val judg = ObjectLogic.fixed_judgment (the_context ()) "x"; + val [free] = fold_aterms (fn v as Free _ => cons v | _ => I) judg []; + val judg' = Term.subst_free [(free, Bound 0)] judg; + val prop = Type ("prop", []); + val prop' = fastype_of judg'; + in + Const ("all", (prop' --> prop) --> prop) $ Abs ("P", prop', judg') + end; + fun check_inj (co, []) = + NONE + | check_inj (co, tys) = + let + val ((xs, ys), _) = Name.context + |> mk_co_args (co, tys) + ||>> mk_co_args (co, tys); + val prem = Logic.mk_equals + (list_comb (co, xs), list_comb (co, ys)); + val concl = Logic.mk_conjunction_list + (map2 (curry Logic.mk_equals) xs ys); + val t = Logic.mk_implies (prem, concl); + in case find_first (curry Term.could_unify t o snd) props + of SOME (thm, _) => SOME thm + | NONE => error ("Could not prove injectiveness statement\n" + ^ Sign.string_of_term thy t + ^ "\nfor constructor " + ^ CodegenConsts.string_of_const_typ thy (dest_Const co) + ^ "\nwith theorems\n" ^ cat_lines (map string_of_thm thms)) + end; + fun check_dist ((co1, tys1), (co2, tys2)) = + let + val ((xs1, xs2), _) = Name.context + |> mk_co_args (co1, tys1) + ||>> mk_co_args (co2, tys2); + val prem = Logic.mk_equals + (list_comb (co1, xs1), list_comb (co2, xs2)); + val t = Logic.mk_implies (prem, quodlibet); + in case find_first (curry Term.could_unify t o snd) props + of SOME (thm, _) => thm + | NONE => error ("Could not prove distinctness statement\n" + ^ Sign.string_of_term thy t + ^ "\nfor constructors " + ^ CodegenConsts.string_of_const_typ thy (dest_Const co1) + ^ " and " + ^ CodegenConsts.string_of_const_typ thy (dest_Const co2) + ^ "\nwith theorems\n" ^ cat_lines (map string_of_thm thms)) + end; + in (map_filter check_inj cos, map check_dist (sym_product cos)) end; + +fun certify_datatype thy dtco cs thms = + (op @) (check_freeness thy cs thms); + + + +(** interfaces **) + +fun add_func thm thy = + let + val thms = mk_func thy thm; + val cs = map fst thms; + in + map_exec_purge (SOME cs) (map_funcs + (fold (fn (c, thm) => Consttab.map_default + (c, (Susp.value [], [])) (add_thm thm)) thms)) thy + end; + +fun del_func thm thy = + let + val thms = mk_func thy thm; + val cs = map fst thms; + in + map_exec_purge (SOME cs) (map_funcs + (fold (fn (c, thm) => Consttab.map_entry c + (del_thm thm)) thms)) thy + end; + +fun add_funcl (c, lthms) thy = + let + val c' = CodegenConsts.norm thy c; + val lthms' = certificate (certify_const thy c') lthms; + in + map_exec_purge (SOME [c]) (map_funcs (Consttab.map_default (c', (Susp.value [], [])) + (add_lthms lthms'))) thy + end; + +fun add_datatype (tyco, (vs_cos as (vs, cos), lthms)) thy = + let + val cs = mk_cos tyco vs cos; + val consts = map (CodegenConsts.norm_of_typ thy o dest_Const o fst) cs; + val add = + map_dtyps (Symtab.update_new (tyco, + (vs_cos, certificate (certify_datatype thy tyco cs) lthms))) + #> map_dconstrs (fold (fn c => Consttab.update (c, tyco)) consts) + in map_exec_purge (SOME consts) add thy end; + +fun del_datatype tyco thy = + let + val SOME ((_, cs), _) = Symtab.lookup ((the_dtyps o get_exec) thy) tyco + val del = + map_dtyps (Symtab.delete tyco) + #> map_dconstrs (fold Consttab.delete cs) + in map_exec_purge (SOME cs) del thy end; + +fun add_inline thm thy = + map_exec_purge NONE (map_preproc (apfst (fold (insert eq_thm) (mk_rew thy thm)))) thy; + +fun del_inline thm thy = + map_exec_purge NONE (map_preproc (apfst (fold (remove eq_thm) (mk_rew thy thm)))) thy ; + +fun add_preproc f = + map_exec_purge NONE (map_preproc (apsnd (cons (serial (), f)))); + +fun getf_first [] _ = NONE + | getf_first (f::fs) x = case f x + of NONE => getf_first fs x + | y as SOME x => y; + +fun getf_first_list [] x = [] + | getf_first_list (f::fs) x = case f x + of [] => getf_first_list fs x + | xs => xs; + +fun preprocess thy thms = + let + fun cmp_thms (thm1, thm2) = + not (Sign.typ_instance thy (typ_func thy thm1, typ_func thy thm2)); + in + thms + |> map (rewrite_func ((#inlines o the_preproc o get_exec) thy)) + |> fold (fn (_, f) => f thy) ((#preprocs o the_preproc o get_exec) thy) + |> map (rewrite_func ((#inlines o the_preproc o get_exec) thy)) + |> sort (make_ord cmp_thms) + |> common_typ_funcs thy + end; + +fun preprocess_cterm thy = + Tactic.rewrite false ((#inlines o the_preproc o get_exec) thy); + +fun these_funcs thy c = + let + fun test_funcs c = + Consttab.lookup ((the_funcs o get_exec) thy) c + |> Option.map (Susp.force o fst) + |> these + |> map (Thm.transfer thy); + val test_defs = get_prim_def_funcs thy; + fun drop_refl thy = filter_out (is_equal o Term.fast_term_ord o Logic.dest_equals + o ObjectLogic.drop_judgment thy o Drule.plain_prop_of); + in + getf_first_list [test_funcs, test_defs] c + |> preprocess thy + |> drop_refl thy + end; + +fun get_datatype thy tyco = + Symtab.lookup ((the_dtyps o get_exec) thy) tyco + |> Option.map (fn (spec, thms) => (Susp.force thms; spec)); + +fun get_datatype_of_constr thy c = + Consttab.lookup ((the_dcontrs o get_exec) thy) c + |> (Option.map o tap) (fn dtco => get_datatype thy dtco); + +fun the_datatype_constrs thy = + Consttab.keys ((the_dcontrs o get_exec) thy); + + + +(** code attributes **) + +local + fun add_simple_attribute (name, f) = + (Codegen.add_attribute name o (Scan.succeed o Thm.declaration_attribute)) + (Context.map_theory o f); +in + val _ = map (Context.add_setup o add_simple_attribute) [ + ("func", add_func), + ("nofunc", del_func), + ("unfold", (fn thm => Codegen.add_unfold thm #> add_inline thm)), + ("inline", add_inline), + ("noinline", del_inline) + ] +end; (*local*) + +end; (*struct*) + + + +(** type-safe interfaces for data depedent on executable content **) + +signature CODE_DATA_ARGS = +sig + val name: string + type T + val empty: T + val merge: Pretty.pp -> T * T -> T + val purge: CodegenConsts.const list option -> T -> T +end; + +signature CODE_DATA = +sig + type T + val init: theory -> theory + val get: theory -> T + val change: theory -> (T -> T) -> T + val change_yield: theory -> (T -> 'a * T) -> 'a * T +end; + +functor CodeDataFun(Data: CODE_DATA_ARGS): CODE_DATA = +struct + +type T = Data.T; +exception Data of T; +fun dest (Data x) = x + +val kind = CodegenData.declare Data.name (Data Data.empty) + (fn pp => fn (Data x1, Data x2) => Data (Data.merge pp (x1, x2))) + (fn cs => fn Data x => Data (Data.purge cs x)); + +val init = CodegenData.init kind; +fun get thy = CodegenData.get kind dest ((! o snd o CodegenData.CodeData.get) thy); +fun change thy f = + let + val data_ref = (snd o CodegenData.CodeData.get) thy; + val x = (f o CodegenData.get kind dest o !) data_ref; + val data = CodegenData.put kind Data x (! data_ref); + in (data_ref := data; x) end; +fun change_yield thy f = + let + val data_ref = (snd o CodegenData.CodeData.get) thy; + val (y, x) = (f o CodegenData.get kind dest o !) data_ref; + val data = CodegenData.put kind Data x (! data_ref); + in (data_ref := data; (y, x)) end; + +end; + +structure CodegenData : CODEGEN_DATA = +struct + +open CodegenData; + +end; diff -r 65bd267ae23f -r 6d75e02ed285 src/Pure/Tools/codegen_funcgr.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/codegen_funcgr.ML Tue Sep 19 15:22:26 2006 +0200 @@ -0,0 +1,373 @@ +(* Title: Pure/Tools/codegen_funcgr.ML + ID: $Id$ + Author: Florian Haftmann, TU Muenchen + +Retrieving and structuring code function theorems. +*) + +signature CODEGEN_FUNCGR = +sig + type T; + val mk_funcgr: theory -> CodegenConsts.const list -> (string * typ) list -> T + val get_funcs: T -> CodegenConsts.const -> thm list + val get_func_typs: T -> (CodegenConsts.const * typ) list + val preprocess: theory -> thm list -> thm list + val print_codethms: theory -> CodegenConsts.const list -> unit +end; + +structure CodegenFuncgr: CODEGEN_FUNCGR = +struct + +(** code data **) + +structure Consttab = CodegenConsts.Consttab; +structure Constgraph = GraphFun ( + type key = CodegenConsts.const; + val ord = CodegenConsts.const_ord; +); + +type T = (typ * thm list) Constgraph.T; + +structure Funcgr = CodeDataFun +(struct + val name = "Pure/codegen_funcgr"; + type T = T; + val empty = Constgraph.empty; + fun merge _ _ = Constgraph.empty; + fun purge _ _ = Constgraph.empty; +end); + +val _ = Context.add_setup Funcgr.init; + + +(** theorem purification **) + +fun abs_norm thy thm = + let + fun expvars t = + let + val lhs = (fst o Logic.dest_equals) t; + val tys = (fst o strip_type o fastype_of) lhs; + val used = fold_aterms (fn Var ((v, _), _) => insert (op =) v | _ => I) lhs []; + val vs = Name.invent_list used "x" (length tys); + in + map2 (fn v => fn ty => Var ((v, 0), ty)) vs tys + end; + fun expand ct thm = + Thm.combination thm (Thm.reflexive ct); + fun beta_norm thm = + thm + |> prop_of + |> Logic.dest_equals + |> fst + |> cterm_of thy + |> Thm.beta_conversion true + |> Thm.symmetric + |> (fn thm' => Thm.transitive thm' thm); + in + thm + |> fold (expand o cterm_of thy) ((expvars o prop_of) thm) + |> beta_norm + end; + +fun canonical_tvars thy thm = + let + fun mk_inst (v_i as (v, i), (v', sort)) (s as (maxidx, set, acc)) = + if v = v' orelse member (op =) set v then s + else let + val ty = TVar (v_i, sort) + in + (maxidx + 1, v :: set, + (ctyp_of thy ty, ctyp_of thy (TVar ((v', maxidx), sort))) :: acc) + end; + fun tvars_of thm = (fold_types o fold_atyps) + (fn TVar (v_i as (v, i), sort) => cons (v_i, (CodegenNames.purify_var v, sort)) + | _ => I) (prop_of thm) []; + val maxidx = Thm.maxidx_of thm + 1; + val (_, _, inst) = fold mk_inst (tvars_of thm) (maxidx + 1, [], []); + in Thm.instantiate (inst, []) thm end; + +fun canonical_vars thy thm = + let + fun mk_inst (v_i as (v, i), (v', ty)) (s as (maxidx, set, acc)) = + 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 + (maxidx + 1, v :: set, + (cterm_of thy t, cterm_of thy (Var ((v', maxidx), ty))) :: acc) + end; + fun vars_of thm = fold_aterms + (fn Var (v_i as (v, i), ty) => cons (v_i, (CodegenNames.purify_var v, ty)) + | _ => I) (prop_of thm) []; + val maxidx = Thm.maxidx_of thm + 1; + val (_, _, inst) = fold mk_inst (vars_of thm) (maxidx + 1, [], []); + in Thm.instantiate ([], inst) thm end; + +fun preprocess thy thms = + let + fun burrow_thms f [] = [] + | burrow_thms f thms = + thms + |> Conjunction.intr_list + |> f + |> Conjunction.elim_list; + fun unvarify thms = + #2 (#1 (Variable.import true thms (ProofContext.init thy))); + in + thms + |> CodegenData.preprocess thy + |> map (abs_norm thy) + |> burrow_thms ( + canonical_tvars thy + #> canonical_vars thy + #> Drule.zero_var_indexes + ) + end; + +fun check_thms c thms = + let + fun check_head_lhs thm (lhs, rhs) = + case strip_comb lhs + of (Const (c', _), _) => if c' = c then () + else error ("Illegal function equation for " ^ quote c + ^ ", actually defining " ^ quote c' ^ ": " ^ Display.string_of_thm thm) + | _ => error ("Illegal function equation: " ^ Display.string_of_thm thm); + fun check_vars_lhs thm (lhs, rhs) = + if has_duplicates (op =) + (fold_aterms (fn Free (v, _) => cons v | _ => I) lhs []) + then error ("Repeated variables on left hand side of function equation:" + ^ Display.string_of_thm thm) + else (); + fun check_vars_rhs thm (lhs, rhs) = + if null (subtract (op =) + (fold_aterms (fn Free (v, _) => cons v | _ => I) lhs []) + (fold_aterms (fn Free (v, _) => cons v | _ => I) rhs [])) + then () + else error ("Free variables on right hand side of function equation:" + ^ Display.string_of_thm thm) + val tts = map (Logic.dest_equals o Logic.unvarify o Thm.prop_of) thms; + in + (map2 check_head_lhs thms tts; map2 check_vars_lhs thms tts; + map2 check_vars_rhs thms tts; thms) + end; + + + +(** retrieval **) + +fun get_funcs funcgr (c_tys as (c, _)) = + (check_thms c o these o Option.map snd o try (Constgraph.get_node funcgr)) c_tys; + +fun get_func_typs funcgr = + AList.make (fst o Constgraph.get_node funcgr) (Constgraph.keys funcgr); + +local + +fun add_things_of thy f (c, thms) = + (fold o fold_aterms) + (fn Const c_ty => let + val c' = CodegenConsts.norm_of_typ thy c_ty + in if CodegenConsts.eq_const (c, c') then I + else f (c', c_ty) end + | _ => I) (maps (op :: o swap o apfst (snd o strip_comb) + o Logic.dest_equals o Drule.plain_prop_of) thms) + +fun rhs_of thy (c, thms) = + Consttab.empty + |> add_things_of thy (Consttab.update o rpair () o fst) (c, thms) + |> Consttab.keys; + +fun rhs_of' thy (c, thms) = + add_things_of thy (cons o snd) (c, thms) []; + +fun insts_of thy funcgr (c, ty) = + let + val tys = Sign.const_typargs thy (c, ty); + val c' = CodegenConsts.norm thy (c, tys); + val ty_decl = if (is_none o AxClass.class_of_param thy) c + then (fst o Constgraph.get_node funcgr) (CodegenConsts.norm thy (c, tys)) + else CodegenConsts.typ_of_classop thy (c, tys); + val tys_decl = Sign.const_typargs thy (c, ty_decl); + val pp = Sign.pp thy; + val algebra = Sign.classes_of thy; + fun classrel (x, _) _ = x; + fun constructor tyco xs class = + (tyco, class) :: maps (maps fst) xs; + fun variable (TVar (_, sort)) = map (pair []) sort + | variable (TFree (_, sort)) = map (pair []) sort; + fun mk_inst ty (TVar (_, sort)) = cons (ty, sort) + | mk_inst ty (TFree (_, sort)) = cons (ty, sort) + | mk_inst (Type (tyco1, tys1)) (Type (tyco2, tys2)) = + if tyco1 <> tyco2 then error "bad instance" + else fold2 mk_inst tys1 tys2; + in + flat (maps (Sorts.of_sort_derivation pp algebra + { classrel = classrel, constructor = constructor, variable = variable }) + (fold2 mk_inst tys tys_decl [])) + end; + +fun all_classops thy tyco class = + maps (AxClass.params_of thy) + (Graph.all_succs ((#classes o Sorts.rep_algebra o Sign.classes_of) thy) [class]) + |> AList.make (fn c => CodegenConsts.typ_of_classop thy (c, [Type (tyco, [])])) + (*typ_of_classop is very liberal in its type arguments*) + |> map (CodegenConsts.norm_of_typ thy); + +fun instdefs_of thy insts = + let + val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy; + in + Symtab.empty + |> fold (fn (tyco, class) => + Symtab.map_default (tyco, []) (insert (op =) class)) insts + |> (fn tab => Symtab.fold (fn (tyco, classes) => append (maps (all_classops thy tyco) + (Graph.all_succs thy_classes classes))) tab []) + end; + +fun insts_of_thms thy funcgr c_thms = + let + val insts = add_things_of thy (fn (_, c_ty) => fold (insert (op =)) + (insts_of thy funcgr c_ty)) c_thms []; + in instdefs_of thy insts end; + +fun ensure_const thy funcgr c auxgr = + if can (Constgraph.get_node funcgr) c + then (NONE, auxgr) + else if can (Constgraph.get_node auxgr) c + then (SOME c, auxgr) + else if is_some (CodegenData.get_datatype_of_constr thy c) then + auxgr + |> Constgraph.new_node (c, []) + |> pair (SOME c) + else let + val thms = preprocess thy (CodegenData.these_funcs thy c); + val rhs = rhs_of thy (c, thms); + in + auxgr + |> Constgraph.new_node (c, thms) + |> fold_map (ensure_const thy funcgr) rhs + |-> (fn rhs' => fold (fn SOME c' => Constgraph.add_edge (c, c') + | NONE => I) rhs') + |> pair (SOME c) + end; + +fun specialize_typs thy funcgr eqss = + let + fun max k [] = k + | max k (l::ls) = max (if k < l then l else k) ls; + fun typscheme_of (c, ty) = + try (Constgraph.get_node funcgr) (CodegenConsts.norm_of_typ thy (c, ty)) + |> Option.map fst; + fun incr_indices (c, thms) maxidx = + let + val thms' = map (Thm.incr_indexes maxidx) thms; + val maxidx' = Int.max + (maxidx, max ~1 (map Thm.maxidx_of thms') + 1); + in ((c, thms'), maxidx') end; + val tsig = Sign.tsig_of thy; + fun unify_const thms (c, ty) (env, maxidx) = + case typscheme_of (c, ty) + of SOME ty_decl => let + val ty_decl' = Logic.incr_tvar maxidx ty_decl; + val maxidx' = Int.max (Term.maxidx_of_typ ty_decl' + 1, maxidx); + in Type.unify tsig (ty_decl', ty) (env, maxidx') + handle TUNIFY => error ("Failed to instantiate\n" + ^ (Sign.string_of_typ thy o Envir.norm_type env) ty_decl' ^ "\nto\n" + ^ (Sign.string_of_typ thy o Envir.norm_type env) ty ^ ",\n" + ^ "in function theorems\n" + ^ cat_lines (map string_of_thm thms)) + end + | NONE => (env, maxidx); + fun apply_unifier unif (c, []) = (c, []) + | apply_unifier unif (c, thms as thm :: _) = + let + val ty = CodegenData.typ_func thy thm; + val ty' = Envir.norm_type unif ty; + val env = Type.typ_match (Sign.tsig_of thy) (ty, ty') Vartab.empty; + val inst = Thm.instantiate (Vartab.fold (fn (x_i, (sort, ty)) => + cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [], []); + in (c, map (Drule.zero_var_indexes o inst) thms) end; + val (eqss', maxidx) = + fold_map incr_indices eqss 0; + val (unif, _) = + fold (fn (c, thms) => fold (unify_const thms) (rhs_of' thy (c, thms))) + eqss' (Vartab.empty, maxidx); + val eqss'' = + map (apply_unifier unif) eqss'; + in eqss'' end; + +fun merge_eqsyss thy raw_eqss funcgr = + let + val eqss = specialize_typs thy funcgr raw_eqss; + val tys = map (fn (c as (name, _), []) => (case AxClass.class_of_param thy name + of SOME class => (case ClassPackage.the_consts_sign thy class of (v, cs) => + (Logic.varifyT o map_type_tfree (fn u as (w, _) => + if w = v then TFree (v, [class]) else TFree u)) + ((the o AList.lookup (op =) cs) name)) + | NONE => Sign.the_const_type thy name) + | (_, eq :: _) => CodegenData.typ_func thy eq) eqss; + val rhss = map (rhs_of thy) eqss; + in + funcgr + |> fold2 (fn (c, thms) => fn ty => Constgraph.new_node (c, (ty, thms))) eqss tys + |> `(fn funcgr => map (insts_of_thms thy funcgr) eqss) + |-> (fn rhs_insts => fold2 (fn (c, _) => fn rhs_inst => + ensure_consts thy rhs_inst #> fold (curry Constgraph.add_edge c) rhs_inst) eqss rhs_insts) + |> fold2 (fn (c, _) => fn rhs => fold (curry Constgraph.add_edge c) rhs) eqss rhss + end +and ensure_consts thy cs funcgr = + fold (snd oo ensure_const thy funcgr) cs Constgraph.empty + |> (fn auxgr => fold (merge_eqsyss thy) + (map (AList.make (Constgraph.get_node auxgr)) + (rev (Constgraph.strong_conn auxgr))) funcgr); + +in + +val ensure_consts = ensure_consts; + +fun mk_funcgr thy consts cs = + Funcgr.change thy ( + ensure_consts thy consts + #> (fn funcgr => ensure_consts thy + (instdefs_of thy (fold (fold (insert (op =)) o insts_of thy funcgr) cs [])) funcgr) + ); + +end; (*local*) + +fun print_funcgr thy funcgr = + AList.make (snd o Constgraph.get_node funcgr) (Constgraph.keys funcgr) + |> (map o apfst) (CodegenConsts.string_of_const thy) + |> sort (string_ord o pairself fst) + |> map (fn (s, thms) => + (Pretty.block o Pretty.fbreaks) ( + Pretty.str s + :: map Display.pretty_thm thms + )) + |> Pretty.chunks + |> Pretty.writeln; + +fun print_codethms thy consts = + mk_funcgr thy consts [] |> print_funcgr thy; + +fun print_codethms_e thy cs = + print_codethms thy (map (CodegenConsts.read_const thy) cs); + + +(** Isar **) + +structure P = OuterParse; + +val print_codethmsK = "print_codethms"; + +val print_codethmsP = + OuterSyntax.improper_command print_codethmsK "print code theorems of this theory" OuterKeyword.diag + (Scan.option (P.$$$ "(" |-- Scan.repeat P.term --| P.$$$ ")") + >> (fn NONE => CodegenData.print_thms + | SOME cs => fn thy => print_codethms_e thy cs) + >> (fn f => Toplevel.no_timing o Toplevel.unknown_theory + o Toplevel.keep (f o Toplevel.theory_of))); + +val _ = OuterSyntax.add_parsers [print_codethmsP]; + +end; (*struct*) diff -r 65bd267ae23f -r 6d75e02ed285 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Tue Sep 19 15:22:24 2006 +0200 +++ b/src/Pure/Tools/codegen_package.ML Tue Sep 19 15:22:26 2006 +0200 @@ -9,13 +9,12 @@ signature CODEGEN_PACKAGE = sig include BASIC_CODEGEN_THINGOL; - val codegen_term: term -> theory -> iterm * theory; - val eval_term: (string (*reference name!*) * 'a ref) * term - -> theory -> 'a * theory; + val codegen_term: theory -> term -> thm * iterm; + val eval_term: theory -> (string (*reference name!*) * 'a option ref) * term -> 'a; val is_dtcon: string -> bool; val consts_of_idfs: theory -> string list -> (string * typ) list; val idfs_of_consts: theory -> (string * typ) list -> string list; - val get_root_module: theory -> CodegenThingol.module * theory; + val get_root_module: theory -> CodegenThingol.module; val get_ml_fun_datatype: theory -> (string -> string) -> ((string * ((iterm list * iterm) list * CodegenThingol.typscheme)) list -> Pretty.T) * ((string * ((vname * sort) list * (string * itype list) list)) list -> Pretty.T); @@ -25,22 +24,21 @@ -> theory -> theory; val add_pretty_ml_string: string -> string -> string -> string -> (string -> string) -> (string -> string) -> string -> theory -> theory; - val purge_code: theory -> theory; type appgen; val add_appconst: string * appgen -> theory -> theory; val appgen_default: appgen; - val appgen_rep_bin: (theory -> term -> IntInf.int) -> appgen; + val appgen_numeral: (theory -> term -> IntInf.int) -> appgen; val appgen_char: (term -> int option) -> appgen; val appgen_case: (theory -> term -> ((string * typ) list * ((term * typ) * (term * term) list)) option) -> appgen; val appgen_let: appgen; - val appgen_wfrec: appgen; val print_code: theory -> unit; - structure CodegenData: THEORY_DATA; - structure Code: THEORY_DATA; + val purge_code: theory -> CodegenThingol.module; + structure CodegenPackageData: THEORY_DATA; + structure Code: CODE_DATA; end; structure CodegenPackage : CODEGEN_PACKAGE = @@ -106,7 +104,8 @@ (* theory data *) -type appgen = theory -> ((sort -> sort) * Sorts.algebra) * Consts.T -> CodegenTheorems.thmtab +type appgen = theory -> ((sort -> sort) * Sorts.algebra) * Consts.T + -> CodegenFuncgr.T -> bool * string list option -> (string * typ) * term list -> transact -> iterm * transact; type appgens = (int * (appgen * stamp)) Symtab.table; @@ -132,19 +131,16 @@ syntax_tyco = Symtab.merge (eq_snd (op =)) (syntax_tyco1, syntax_tyco2), syntax_const = Symtab.merge (eq_snd (op =)) (syntax_const1, syntax_const2) } : target_data; -structure Code = TheoryDataFun +structure Code = CodeDataFun (struct val name = "Pure/code"; type T = module; val empty = empty_module; - val copy = I; - val extend = I; fun merge _ = merge_module; - fun print thy module = - (Pretty.writeln o Pretty.chunks) [pretty_module module, pretty_deps module]; + fun purge _ _ = CodegenThingol.empty_module; end); -structure CodegenData = TheoryDataFun +structure CodegenPackageData = TheoryDataFun (struct val name = "Pure/codegen_package"; type T = { @@ -173,14 +169,14 @@ fun print _ _ = (); end); -val _ = Context.add_setup (Code.init #> CodegenData.init); +val _ = Context.add_setup (Code.init #> CodegenPackageData.init); fun map_codegen_data f thy = - case CodegenData.get thy + case CodegenPackageData.get thy of { appgens, target_data } => let val (appgens, target_data) = f (appgens, target_data) - in CodegenData.put { appgens = appgens, + in CodegenPackageData.put { appgens = appgens, target_data = target_data } thy end; fun check_serializer target = @@ -195,7 +191,7 @@ fun serialize thy target seri cs = let - val data = CodegenData.get thy; + val data = CodegenPackageData.get thy; val code = Code.get thy; val target_data = (the oo Symtab.lookup) (#target_data data) target; @@ -229,14 +225,12 @@ ) end; -val print_code = Code.print; - -val purge_code = Code.map (K CodegenThingol.empty_module); +fun print_code thy = + let + val code = Code.get thy; + in (Pretty.writeln o Pretty.chunks) [pretty_module code, pretty_deps code] end; -fun purge_defs NONE = purge_code - | purge_defs (SOME []) = I - | purge_defs (SOME cs) = purge_code; - +fun purge_code thy = Code.change thy (K CodegenThingol.empty_module); (* name handling *) @@ -258,15 +252,15 @@ fun inst_of_idf thy = if_nsp nsp_inst (CodegenNames.instance_rev thy); -fun idf_of_const thy thmtab (c_ty as (c, ty)) = - if is_some (CodegenTheorems.get_dtyp_of_cons thmtab c_ty) then - CodegenNames.const thy c_ty +fun idf_of_const thy c_tys = + if (is_some o CodegenData.get_datatype_of_constr thy) c_tys then + CodegenNames.const thy c_tys |> add_nsp nsp_dtcon - else if (is_some o CodegenConsts.class_of_classop thy o CodegenConsts.typinst_of_typ thy) c_ty then - CodegenNames.const thy c_ty + else if (is_some o CodegenConsts.class_of_classop thy) c_tys then + CodegenNames.const thy c_tys |> add_nsp nsp_mem else - CodegenNames.const thy c_ty + CodegenNames.const thy c_tys |> add_nsp nsp_const; fun idf_of_classop thy c_ty = @@ -293,27 +287,27 @@ | check_strict thy f x (_, SOME targets) = exists ( is_none o (fn tab => Symtab.lookup tab x) o f o the - o (Symtab.lookup ((#target_data o CodegenData.get) thy)) + o (Symtab.lookup ((#target_data o CodegenPackageData.get) thy)) ) targets | check_strict thy f x (true, _) = true; fun no_strict (_, targets) = (false, targets); -fun ensure_def_class thy algbr thmtab strct cls trns = +fun ensure_def_class thy algbr funcgr strct cls trns = let - fun defgen_class thy (algbr as ((proj_sort, _), _)) thmtab strct cls trns = + fun defgen_class thy (algbr as ((proj_sort, _), _)) funcgr strct cls trns = case class_of_idf thy cls of SOME cls => let val (v, cs) = (ClassPackage.the_consts_sign thy) cls; val superclasses = (proj_sort o Sign.super_classes thy) cls - val idfs = map (idf_of_const thy thmtab) cs; + val idfs = map (idf_of_const thy o CodegenConsts.norm_of_typ thy) cs; in trns |> debug_msg (fn _ => "trying defgen class declaration for " ^ quote cls) - |> fold_map (ensure_def_class thy algbr thmtab strct) superclasses - ||>> (fold_map (exprgen_type thy algbr thmtab strct) o map snd) cs + |> fold_map (ensure_def_class thy algbr funcgr strct) superclasses + ||>> (fold_map (exprgen_type thy algbr funcgr strct) o map snd) cs |-> (fn (supcls, memtypes) => succeed (Class (supcls, (unprefix "'" v, idfs ~~ memtypes)))) end @@ -324,24 +318,26 @@ in trns |> debug_msg (fn _ => "generating class " ^ quote cls) - |> ensure_def (defgen_class thy algbr thmtab strct) true ("generating class " ^ quote cls) cls' + |> ensure_def (defgen_class thy algbr funcgr strct) true ("generating class " ^ quote cls) cls' |> pair cls' end -and ensure_def_tyco thy algbr thmtab strct tyco trns = +and ensure_def_tyco thy algbr funcgr strct tyco trns = let val tyco' = idf_of_tyco thy tyco; val strict = check_strict thy #syntax_tyco tyco' strct; - fun defgen_datatype thy algbr thmtab strct dtco trns = + fun defgen_datatype thy algbr funcgr strct dtco trns = case tyco_of_idf thy dtco of SOME dtco => - (case CodegenTheorems.get_dtyp_spec thmtab dtco + (case CodegenData.get_datatype thy dtco of SOME (vs, cos) => trns |> debug_msg (fn _ => "trying defgen datatype for " ^ quote dtco) - |> fold_map (exprgen_tyvar_sort thy algbr thmtab strct) vs + |> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs ||>> fold_map (fn (c, tys) => - fold_map (exprgen_type thy algbr thmtab strct) tys - #-> (fn tys' => pair (idf_of_const thy thmtab (c, tys ---> Type (dtco, map TFree vs)), tys'))) cos + fold_map (exprgen_type thy algbr funcgr strct) tys + #-> (fn tys' => + pair ((idf_of_const thy o CodegenConsts.norm_of_typ thy) + (c, tys ---> Type (dtco, map TFree vs)), tys'))) cos |-> (fn (vs, cos) => succeed (Datatype (vs, cos))) | NONE => trns @@ -352,32 +348,34 @@ in trns |> debug_msg (fn _ => "generating type constructor " ^ quote tyco) - |> ensure_def (defgen_datatype thy algbr thmtab strct) strict + |> ensure_def (defgen_datatype thy algbr funcgr strct) strict ("generating type constructor " ^ quote tyco) tyco' |> pair tyco' end -and exprgen_tyvar_sort thy (algbr as ((proj_sort, _), _)) thmtab strct (v, sort) trns = +and exprgen_tyvar_sort thy (algbr as ((proj_sort, _), _)) funcgr strct (v, sort) trns = trns - |> fold_map (ensure_def_class thy algbr thmtab strct) (proj_sort sort) + |> fold_map (ensure_def_class thy algbr funcgr strct) (proj_sort sort) |-> (fn sort => pair (unprefix "'" v, sort)) -and exprgen_type thy algbr thmtab strct (TVar _) trns = +and exprgen_type thy algbr funcgr strct (TVar _) trns = error "TVar encountered in typ during code generation" - | exprgen_type thy algbr thmtab strct (TFree vs) trns = + | exprgen_type thy algbr funcgr strct (TFree vs) trns = trns - |> exprgen_tyvar_sort thy algbr thmtab strct vs + |> exprgen_tyvar_sort thy algbr funcgr strct vs |-> (fn (v, sort) => pair (ITyVar v)) - | exprgen_type thy algbr thmtab strct (Type ("fun", [t1, t2])) trns = + | exprgen_type thy algbr funcgr strct (Type ("fun", [t1, t2])) trns = trns - |> exprgen_type thy algbr thmtab strct t1 - ||>> exprgen_type thy algbr thmtab strct t2 + |> exprgen_type thy algbr funcgr strct t1 + ||>> exprgen_type thy algbr funcgr strct t2 |-> (fn (t1', t2') => pair (t1' `-> t2')) - | exprgen_type thy algbr thmtab strct (Type (tyco, tys)) trns = + | exprgen_type thy algbr funcgr strct (Type (tyco, tys)) trns = trns - |> ensure_def_tyco thy algbr thmtab strct tyco - ||>> fold_map (exprgen_type thy algbr thmtab strct) tys + |> ensure_def_tyco thy algbr funcgr strct tyco + ||>> fold_map (exprgen_type thy algbr funcgr strct) tys |-> (fn (tyco, tys) => pair (tyco `%% tys)); -fun exprgen_typinst thy (algbr as ((proj_sort, algebra), consts)) thmtab strct (ty_ctxt, sort_decl) trns = +exception CONSTRAIN of ((string * typ) * typ) * term option; + +fun exprgen_typinst thy (algbr as ((proj_sort, algebra), consts)) funcgr strct (ty_ctxt, sort_decl) trns = let val pp = Sign.pp thy; datatype inst = @@ -398,31 +396,34 @@ (ty_ctxt, proj_sort sort_decl); fun mk_dict (Inst (inst, instss)) trns = trns - |> ensure_def_inst thy algbr thmtab strct inst + |> ensure_def_inst thy algbr funcgr strct inst ||>> (fold_map o fold_map) mk_dict instss |-> (fn (inst, instss) => pair (Instance (inst, instss))) | mk_dict (Contxt ((v, sort), (classes, k))) trns = trns - |> fold_map (ensure_def_class thy algbr thmtab strct) classes + |> fold_map (ensure_def_class thy algbr funcgr strct) classes |-> (fn classes => pair (Context (classes, (unprefix "'" v, if length sort = 1 then ~1 else k)))) in trns |> fold_map mk_dict insts end -and exprgen_typinst_const thy (algbr as (_, consts)) thmtab strct (c, ty_ctxt) trns = - let - val idf = idf_of_const thy thmtab (c, ty_ctxt) +and exprgen_typinst_const thy (algbr as (_, consts)) funcgr strct (c, ty_ctxt) trns = + let + val c' = CodegenConsts.norm_of_typ thy (c, ty_ctxt) + val idf = idf_of_const thy c'; val ty_decl = Consts.declaration consts idf; val insts = (op ~~ o apsnd (map (snd o dest_TVar)) oo pairself) (curry (Consts.typargs consts) idf) (ty_ctxt, ty_decl); + val _ = if exists not (map (Sign.of_sort thy) insts) + then raise CONSTRAIN (((c, ty_decl), ty_ctxt), NONE) else (); in trns - |> fold_map (exprgen_typinst thy algbr thmtab strct) insts + |> fold_map (exprgen_typinst thy algbr funcgr strct) insts end -and ensure_def_inst thy algbr thmtab strct (cls, tyco) trns = +and ensure_def_inst thy algbr funcgr strct (cls, tyco) trns = let - fun defgen_inst thy (algbr as ((proj_sort, _), _)) thmtab strct inst trns = + fun defgen_inst thy (algbr as ((proj_sort, _), _)) funcgr strct inst trns = case inst_of_idf thy inst of SOME (class, tyco) => let @@ -432,20 +433,20 @@ val superclasses = (proj_sort o Sign.super_classes thy) class fun gen_suparity supclass trns = trns - |> ensure_def_class thy algbr thmtab strct supclass - ||>> exprgen_typinst thy algbr thmtab strct (arity_typ, [supclass]) + |> ensure_def_class thy algbr funcgr strct supclass + ||>> exprgen_typinst thy algbr funcgr strct (arity_typ, [supclass]) |-> (fn (supclass, [Instance (supints, lss)]) => pair (supclass, (supints, lss))); fun gen_membr ((m0, ty0), (m, ty)) trns = trns - |> ensure_def_const thy algbr thmtab strct (m0, ty0) - ||>> exprgen_term thy algbr thmtab strct (Const (m, ty)); + |> ensure_def_const thy algbr funcgr strct (CodegenConsts.norm_of_typ thy (m0, ty0)) + ||>> exprgen_term thy algbr funcgr strct (Const (m, ty)); in trns |> debug_msg (fn _ => "trying defgen class instance for (" ^ quote cls ^ ", " ^ quote tyco ^ ")") - |> ensure_def_class thy algbr thmtab strct class - ||>> ensure_def_tyco thy algbr thmtab strct tyco - ||>> fold_map (exprgen_tyvar_sort thy algbr thmtab strct) vs + |> ensure_def_class thy algbr funcgr strct class + ||>> ensure_def_tyco thy algbr funcgr strct tyco + ||>> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs ||>> fold_map gen_suparity superclasses ||>> fold_map gen_membr (members ~~ memdefs) |-> (fn ((((class, tyco), arity), suparities), memdefs) => @@ -457,39 +458,38 @@ in trns |> debug_msg (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco) - |> ensure_def (defgen_inst thy algbr thmtab strct) true + |> ensure_def (defgen_inst thy algbr funcgr strct) true ("generating instance " ^ quote cls ^ " / " ^ quote tyco) inst |> pair inst end -and ensure_def_const thy algbr thmtab strct (c, ty) trns = +and ensure_def_const thy algbr funcgr strct (c, tys) trns = let - fun defgen_datatypecons thy algbr thmtab strct co trns = - case CodegenTheorems.get_dtyp_of_cons thmtab ((the o const_of_idf thy) co) + fun defgen_datatypecons thy algbr funcgr strct co trns = + case CodegenData.get_datatype_of_constr thy ((the o const_of_idf thy) co) of SOME tyco => trns |> debug_msg (fn _ => "trying defgen datatype constructor for " ^ quote co) - |> ensure_def_tyco thy algbr thmtab strct tyco + |> ensure_def_tyco thy algbr funcgr strct tyco |-> (fn _ => succeed Bot) | _ => trns |> fail ("Not a datatype constructor: " - ^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty)); - fun defgen_clsmem thy algbr thmtab strct m trns = - case CodegenConsts.class_of_classop thy - ((CodegenConsts.typinst_of_typ thy o the o const_of_idf thy) m) + ^ (quote o CodegenConsts.string_of_const thy) (c, tys)); + fun defgen_clsmem thy algbr funcgr strct m trns = + case CodegenConsts.class_of_classop thy ((the o const_of_idf thy) m) of SOME class => trns |> debug_msg (fn _ => "trying defgen class member for " ^ quote m) - |> ensure_def_class thy algbr thmtab strct class + |> ensure_def_class thy algbr funcgr strct class |-> (fn _ => succeed Bot) | _ => - trns |> fail ("No class found for " ^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty)) - fun defgen_funs thy (algbr as (_, consts)) thmtab strct c' trns = - case CodegenTheorems.get_fun_thms thmtab ((the o const_of_idf thy) c') + trns |> fail ("No class operation found for " ^ (quote o CodegenConsts.string_of_const thy) (c, tys)) + fun defgen_funs thy (algbr as (_, consts)) funcgr strct c' trns = + case CodegenFuncgr.get_funcs funcgr ((the o const_of_idf thy) c') of eq_thms as eq_thm :: _ => let val msg = cat_lines ("generating code for theorems " :: map string_of_thm eq_thms); - val ty = (Logic.unvarifyT o CodegenTheorems.extr_typ thy) eq_thm; + val ty = (Logic.unvarifyT o CodegenData.typ_func thy) eq_thm; val vs = (map dest_TFree o Consts.typargs consts) (c', ty); fun dest_eqthm eq_thm = let @@ -503,8 +503,8 @@ end; fun exprgen_eq (args, rhs) trns = trns - |> fold_map (exprgen_term thy algbr thmtab strct) args - ||>> exprgen_term thy algbr thmtab strct rhs; + |> fold_map (exprgen_term thy algbr funcgr strct) args + ||>> exprgen_term thy algbr funcgr strct rhs; fun checkvars (args, rhs) = if CodegenThingol.vars_distinct args then (args, rhs) else error ("Repeated variables on left hand side of function") @@ -513,75 +513,75 @@ |> message msg (fn trns => trns |> fold_map (exprgen_eq o dest_eqthm) eq_thms |-> (fn eqs => pair (map checkvars eqs)) - ||>> fold_map (exprgen_tyvar_sort thy algbr thmtab strct) vs - ||>> exprgen_type thy algbr thmtab strct ty + ||>> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs + ||>> exprgen_type thy algbr funcgr strct ty |-> (fn ((eqs, vs), ty) => succeed (Fun (eqs, (vs, ty))))) end | [] => trns |> fail ("No defining equations found for " - ^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty)); - fun get_defgen thmtab strct idf strict = + ^ (quote o CodegenConsts.string_of_const thy) (c, tys)); + fun get_defgen funcgr strct idf strict = if (is_some oo dest_nsp) nsp_const idf - then defgen_funs thy algbr thmtab strct strict + then defgen_funs thy algbr funcgr strct strict else if (is_some oo dest_nsp) nsp_mem idf - then defgen_clsmem thy algbr thmtab strct strict + then defgen_clsmem thy algbr funcgr strct strict else if (is_some oo dest_nsp) nsp_dtcon idf - then defgen_datatypecons thy algbr thmtab strct strict + then defgen_datatypecons thy algbr funcgr strct strict else error ("Illegal shallow name space for constant: " ^ quote idf); - val idf = idf_of_const thy thmtab (c, ty); + val idf = idf_of_const thy (c, tys); val strict = check_strict thy #syntax_const idf strct; in trns |> debug_msg (fn _ => "generating constant " - ^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty)) - |> ensure_def (get_defgen thmtab strct idf) strict ("generating constant " - ^ CodegenConsts.string_of_const_typ thy (c, ty)) idf + ^ (quote o CodegenConsts.string_of_const thy) (c, tys)) + |> ensure_def (get_defgen funcgr strct idf) strict ("generating constant " + ^ CodegenConsts.string_of_const thy (c, tys)) idf |> pair idf end -and exprgen_term thy algbr thmtab strct (Const (f, ty)) trns = +and exprgen_term thy algbr funcgr strct (Const (f, ty)) trns = trns - |> appgen thy algbr thmtab strct ((f, ty), []) + |> appgen thy algbr funcgr strct ((f, ty), []) |-> (fn e => pair e) - | exprgen_term thy algbr thmtab strct (Var _) trns = + | exprgen_term thy algbr funcgr strct (Var _) trns = error "Var encountered in term during code generation" - | exprgen_term thy algbr thmtab strct (Free (v, ty)) trns = + | exprgen_term thy algbr funcgr strct (Free (v, ty)) trns = trns - |> exprgen_type thy algbr thmtab strct ty + |> exprgen_type thy algbr funcgr strct ty |-> (fn ty => pair (IVar v)) - | exprgen_term thy algbr thmtab strct (Abs (raw_v, ty, raw_t)) trns = + | exprgen_term thy algbr funcgr strct (Abs (raw_v, ty, raw_t)) trns = let val (v, t) = Syntax.variant_abs (CodegenNames.purify_var raw_v, ty, raw_t); in trns - |> exprgen_type thy algbr thmtab strct ty - ||>> exprgen_term thy algbr thmtab strct t + |> exprgen_type thy algbr funcgr strct ty + ||>> exprgen_term thy algbr funcgr strct t |-> (fn (ty, e) => pair ((v, ty) `|-> e)) end - | exprgen_term thy algbr thmtab strct (t as t1 $ t2) trns = + | exprgen_term thy algbr funcgr strct (t as t1 $ t2) trns = let val (t', ts) = strip_comb t in case t' of Const (f, ty) => trns - |> appgen thy algbr thmtab strct ((f, ty), ts) + |> appgen thy algbr funcgr strct ((f, ty), ts) |-> (fn e => pair e) | _ => trns - |> exprgen_term thy algbr thmtab strct t' - ||>> fold_map (exprgen_term thy algbr thmtab strct) ts + |> exprgen_term thy algbr funcgr strct t' + ||>> fold_map (exprgen_term thy algbr funcgr strct) ts |-> (fn (e, es) => pair (e `$$ es)) end -and appgen_default thy algbr thmtab strct ((c, ty), ts) trns = +and appgen_default thy algbr funcgr strct ((c, ty), ts) trns = trns - |> ensure_def_const thy algbr thmtab strct (c, ty) - ||>> exprgen_type thy algbr thmtab strct ty - ||>> exprgen_typinst_const thy algbr thmtab strct (c, ty) - ||>> fold_map (exprgen_term thy algbr thmtab strct) ts + |> ensure_def_const thy algbr funcgr strct (CodegenConsts.norm_of_typ thy (c, ty)) + ||>> exprgen_type thy algbr funcgr strct ty + ||>> exprgen_typinst_const thy algbr funcgr strct (c, ty) + ||>> fold_map (exprgen_term thy algbr funcgr strct) ts |-> (fn (((c, ty), ls), es) => pair (IConst (c, (ls, ty)) `$$ es)) -and appgen thy algbr thmtab strct ((f, ty), ts) trns = - case Symtab.lookup ((#appgens o CodegenData.get) thy) f +and appgen thy algbr funcgr strct ((f, ty), ts) trns = + case Symtab.lookup ((#appgens o CodegenPackageData.get) thy) f of SOME (i, (ag, _)) => if length ts < i then let @@ -589,71 +589,95 @@ val vs = Name.names (Name.declare f Name.context) "a" tys; in trns - |> fold_map (exprgen_type thy algbr thmtab strct) tys - ||>> ag thy algbr thmtab strct ((f, ty), ts @ map Free vs) + |> fold_map (exprgen_type thy algbr funcgr strct) tys + ||>> ag thy algbr funcgr strct ((f, ty), ts @ map Free vs) |-> (fn (tys, e) => pair (map2 (fn (v, _) => pair v) vs tys `|--> e)) end else if length ts > i then trns - |> ag thy algbr thmtab strct ((f, ty), Library.take (i, ts)) - ||>> fold_map (exprgen_term thy algbr thmtab strct) (Library.drop (i, ts)) + |> ag thy algbr funcgr strct ((f, ty), Library.take (i, ts)) + ||>> fold_map (exprgen_term thy algbr funcgr strct) (Library.drop (i, ts)) |-> (fn (e, es) => pair (e `$$ es)) else trns - |> ag thy algbr thmtab strct ((f, ty), ts) + |> ag thy algbr funcgr strct ((f, ty), ts) | NONE => trns - |> appgen_default thy algbr thmtab strct ((f, ty), ts); + |> appgen_default thy algbr funcgr strct ((f, ty), ts); + + +(* entry points into extraction kernel *) + +fun ensure_def_const' thy algbr funcgr strct c trns = + ensure_def_const thy algbr funcgr strct c trns + handle CONSTRAIN (((c, ty), ty_decl), NONE) => error ( + "Constant " ^ c ^ " with most general type\n" + ^ Sign.string_of_typ thy ty + ^ "\noccurs with type\n" + ^ Sign.string_of_typ thy ty_decl) + handle CONSTRAIN (((c, ty), ty_decl), SOME t) => error ("In term " ^ (quote o Sign.string_of_term thy) t + ^ ",\nconstant " ^ c ^ " with most general type\n" + ^ Sign.string_of_typ thy ty + ^ "\noccurs with type\n" + ^ Sign.string_of_typ thy ty_decl); + +fun exprgen_term' thy algbr funcgr strct t trns = + exprgen_term thy algbr funcgr strct t trns + handle CONSTRAIN (((c, ty), ty_decl), _) => error ("In term " ^ (quote o Sign.string_of_term thy) t + ^ ",\nconstant " ^ c ^ " with most general type\n" + ^ Sign.string_of_typ thy ty + ^ "\noccurs with type\n" + ^ Sign.string_of_typ thy ty_decl); (* parametrized application generators, for instantiation in object logic *) (* (axiomatic extensions of extraction kernel *) -fun appgen_rep_bin int_of_numeral thy algbr thmtab strct (app as (c, ts)) trns = +fun appgen_numeral int_of_numeral thy algbr funcgr strct (app as (c, ts)) trns = case try (int_of_numeral thy) (list_comb (Const c, ts)) - of SOME i => if i < 0 then (*preprocessor eliminates negative numerals*) + of SOME i => (*if i < 0 then (*preprocessor eliminates negative numerals*) trns - |> appgen_default thy algbr thmtab (no_strict strct) app - else + |> appgen_default thy algbr funcgr (no_strict strct) app + else*) trns - |> appgen_default thy algbr thmtab (no_strict strct) app + |> appgen_default thy algbr funcgr (no_strict strct) app |-> (fn e => pair (CodegenThingol.INum (i, e))) | NONE => trns - |> appgen_default thy algbr thmtab (no_strict strct) app; + |> appgen_default thy algbr funcgr (no_strict strct) app; -fun appgen_char char_to_index thy algbr thmtab strct (app as ((_, ty), _)) trns = +fun appgen_char char_to_index thy algbr funcgr strct (app as ((_, ty), _)) trns = case (char_to_index o list_comb o apfst Const) app of SOME i => trns - |> exprgen_type thy algbr thmtab strct ty - ||>> appgen_default thy algbr thmtab strct app + |> exprgen_type thy algbr funcgr strct ty + ||>> appgen_default thy algbr funcgr strct app |-> (fn (_, e0) => pair (IChar (chr i, e0))) | NONE => trns - |> appgen_default thy algbr thmtab strct app; + |> appgen_default thy algbr funcgr strct app; -fun appgen_case dest_case_expr thy algbr thmtab strct (app as (c_ty, ts)) trns = +fun appgen_case dest_case_expr thy algbr funcgr strct (app as (c_ty, ts)) trns = let val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts)); fun clausegen (dt, bt) trns = trns - |> exprgen_term thy algbr thmtab strct dt - ||>> exprgen_term thy algbr thmtab strct bt; + |> exprgen_term thy algbr funcgr strct dt + ||>> exprgen_term thy algbr funcgr strct bt; in trns - |> exprgen_term thy algbr thmtab strct st - ||>> exprgen_type thy algbr thmtab strct sty + |> exprgen_term thy algbr funcgr strct st + ||>> exprgen_type thy algbr funcgr strct sty ||>> fold_map clausegen ds - ||>> appgen_default thy algbr thmtab strct app + ||>> appgen_default thy algbr funcgr strct app |-> (fn (((se, sty), ds), e0) => pair (ICase (((se, sty), ds), e0))) end; -fun appgen_let thy algbr thmtab strct (app as (_, [st, ct])) trns = +fun appgen_let thy algbr funcgr strct (app as (_, [st, ct])) trns = trns - |> exprgen_term thy algbr thmtab strct ct - ||>> exprgen_term thy algbr thmtab strct st - ||>> appgen_default thy algbr thmtab strct app + |> exprgen_term thy algbr funcgr strct ct + ||>> exprgen_term thy algbr funcgr strct st + ||>> appgen_default thy algbr funcgr strct app |-> (fn (((v, ty) `|-> be, se), e0) => pair (ICase (((se, ty), case be of ICase (((IVar w, _), ds), _) => if v = w then ds else [(IVar v, be)] @@ -661,21 +685,6 @@ ), e0)) | (_, e0) => pair e0); -fun appgen_wfrec thy algbr thmtab strct ((c, ty), [_, tf, tx]) trns = - let - val ty_def = (op ---> o apfst tl o strip_type o Logic.unvarifyT o Sign.the_const_type thy) c; - val ty' = (op ---> o apfst tl o strip_type) ty; - val idf = idf_of_const thy thmtab (c, ty); - in - trns - |> ensure_def ((K o fail) "no extraction for wfrec") false ("generating wfrec") idf - |> exprgen_type thy algbr thmtab strct ty' - ||>> exprgen_type thy algbr thmtab strct ty_def - ||>> exprgen_term thy algbr thmtab strct tf - ||>> exprgen_term thy algbr thmtab strct tx - |-> (fn (((_, ty), tf), tx) => pair (IConst (idf, ([], ty)) `$ tf `$ tx)) - end; - fun add_appconst (c, appgen) thy = let val i = (length o fst o strip_type o Sign.the_const_type thy) c @@ -689,62 +698,50 @@ (** code generation interfaces **) -fun generate cs targets init gen it thy = +fun generate thy (cs, rhss) targets init gen it = let - val thmtab = CodegenTheorems.mk_thmtab thy cs; + val funcgr = CodegenFuncgr.mk_funcgr thy cs rhss; val qnaming = NameSpace.qualified_names NameSpace.default_naming val algebr = ClassPackage.operational_algebra thy; - fun ops_of_class class = - let - val (v, ops) = ClassPackage.the_consts_sign thy class; - val ops_tys = map (fn (c, ty) => - (c, (Logic.varifyT o map_type_tfree (fn u as (w, _) => - if w = v then TFree (v, [class]) else TFree u)) ty)) ops; - in - map (fn (c, ty) => (idf_of_const thy thmtab (c, ty), ty)) ops_tys - end; - val classops = maps ops_of_class (Sorts.classes (snd algebr)); val consttab = Consts.empty |> fold (fn (c, ty) => Consts.declare qnaming - (((idf_of_const thy thmtab o CodegenConsts.typ_of_typinst thy) c, ty), true)) - (CodegenTheorems.get_fun_typs thmtab) - |> fold (Consts.declare qnaming o rpair true) classops; + ((idf_of_const thy c, ty), true)) + (CodegenFuncgr.get_func_typs funcgr) val algbr = (algebr, consttab); in - thy - |> CodegenTheorems.notify_dirty - |> `Code.get - |> (fn (modl, thy) => - (start_transact init (gen thy algbr thmtab - (true, targets) it) modl, thy)) - |-> (fn (x, modl) => Code.map (K modl) #> pair x) + Code.change_yield thy (start_transact init (gen thy algbr funcgr + (true, targets) it)) + |> (fn (x, modl) => x) end; -fun consts_of t = - fold_aterms (fn Const c => cons c | _ => I) t []; +fun consts_of thy t = + fold_aterms (fn Const c => cons (CodegenConsts.norm_of_typ thy c, c) | _ => I) t [] + |> split_list; -fun codegen_term t thy = +fun codegen_term thy t = let - val _ = Thm.cterm_of thy t; + val ct = Thm.cterm_of thy t; + val thm = CodegenData.preprocess_cterm thy ct; + val t' = (snd o Logic.dest_equals o Drule.plain_prop_of) thm; + val cs_rhss = consts_of thy t'; in - thy - |> generate (consts_of t) (SOME []) NONE exprgen_term t + (thm, generate thy cs_rhss (SOME []) NONE exprgen_term' t') end; val is_dtcon = has_nsp nsp_dtcon; fun consts_of_idfs thy = - map (the o const_of_idf thy); + map (CodegenConsts.typ_of_inst thy o the o const_of_idf thy); fun idfs_of_consts thy cs = - map (idf_of_const thy (CodegenTheorems.mk_thmtab thy cs)) cs; + let + val cs' = map (CodegenConsts.norm_of_typ thy) cs; + in map (idf_of_const thy) cs' end; fun get_root_module thy = - thy - |> CodegenTheorems.notify_dirty - |> `Code.get; + Code.get thy; -fun eval_term (ref_spec, t) thy = +fun eval_term thy (ref_spec, t) = let val _ = Term.fold_atyps (fn _ => error ("Term" ^ Sign.string_of_term thy t ^ "is polymorhpic")) @@ -756,27 +753,26 @@ val eq = setmp quick_and_dirty true (SkipProof.make_thm thy) (Logic.mk_equals (x, t)); fun err () = error "preprocess_term: bad preprocessor" - in case map prop_of (CodegenTheorems.preprocess thy [eq]) + in case map prop_of (CodegenFuncgr.preprocess thy [eq]) of [Const ("==", _) $ x' $ t'] => if x = x' then t' else err () | _ => err () end; val target_data = - ((fn data => (the o Symtab.lookup data) "SML") o #target_data o CodegenData.get) thy; + ((fn data => (the o Symtab.lookup data) "SML") o #target_data o CodegenPackageData.get) thy; val eval = CodegenSerializer.eval_term nsp_eval nsp_dtcon [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_dtcon, nsp_class, nsp_mem, nsp_inst], [nsp_eval]] ((Option.map fst oo Symtab.lookup) (#syntax_tyco target_data), (Option.map fst oo Symtab.lookup) (#syntax_const target_data)) - (Symtab.keys (#syntax_tyco target_data) @ Symtab.keys (#syntax_const target_data)) + (Symtab.keys (#syntax_tyco target_data) @ Symtab.keys (#syntax_const target_data)); + val (_, t') = codegen_term thy (preprocess_term t); + val modl = Code.get thy; in - thy - |> codegen_term (preprocess_term t) - ||>> `Code.get - |-> (fn (t', modl) => `(fn _ => eval (ref_spec, t') modl)) + eval (ref_spec, t') modl end; fun get_ml_fun_datatype thy resolv = let val target_data = - ((fn data => (the o Symtab.lookup data) "SML") o #target_data o CodegenData.get) thy; + ((fn data => (the o Symtab.lookup data) "SML") o #target_data o CodegenPackageData.get) thy; in CodegenSerializer.ml_fun_datatype nsp_dtcon ((Option.map fst oo Symtab.lookup o #syntax_tyco) target_data, @@ -803,7 +799,7 @@ syntax_inst, syntax_tyco, syntax_const)) end; -fun gen_add_syntax_inst prep_class prep_tyco target (raw_class, raw_tyco) thy = +fun gen_add_syntax_inst prep_class prep_tyco target (raw_tyco, raw_class) thy = let val inst = idf_of_inst thy (prep_class thy raw_class, prep_tyco thy raw_tyco); in @@ -825,13 +821,13 @@ fun gen_add_syntax_const prep_const raw_c target syntax thy = let - val c_ty = prep_const thy raw_c; - val c = idf_of_const thy (CodegenTheorems.mk_thmtab thy [c_ty]) c_ty; + val c' = prep_const thy raw_c; + val c'' = idf_of_const thy c'; in thy |> map_target_data target (fn (syntax_class, syntax_inst, syntax_tyco, syntax_const) => (syntax_class, syntax_inst, syntax_tyco, syntax_const - |> Symtab.update (c, (syntax, stamp ())))) + |> Symtab.update (c'', (syntax, stamp ())))) end; fun read_type thy raw_tyco = @@ -843,18 +839,17 @@ fun idfs_of_const_names thy cs = let - val cs' = AList.make (fn c => Sign.the_const_type thy c) cs - val thmtab = CodegenTheorems.mk_thmtab thy cs' - in AList.make (idf_of_const thy thmtab) cs' end; + val cs' = AList.make (fn c => Sign.the_const_type thy c) cs; + val cs'' = map (CodegenConsts.norm_of_typ thy) cs'; + in AList.make (idf_of_const thy) cs'' end; fun read_quote reader consts_of target get_init gen raw_it thy = let val it = reader thy raw_it; - val cs = consts_of it; + val cs = consts_of thy it; in - thy - |> generate cs (SOME [target]) ((SOME o get_init) thy) gen [it] - |-> (fn [it'] => pair it') + generate thy cs (SOME [target]) ((SOME o get_init) thy) gen [it] + |> (fn [it'] => (it', thy)) end; fun parse_quote num_of reader consts_of target get_init gen adder = @@ -864,7 +859,7 @@ in -val add_syntax_class = gen_add_syntax_class ClassPackage.read_class CodegenConsts.read_const_typ; +val add_syntax_class = gen_add_syntax_class ClassPackage.read_class CodegenConsts.read_const; val add_syntax_inst = gen_add_syntax_inst ClassPackage.read_class read_type; fun parse_syntax_tyco target raw_tyco = @@ -875,22 +870,18 @@ fun read_typ thy = Sign.read_typ (thy, K NONE); in - parse_quote num_of read_typ (K []) target idf_of (fold_map oooo exprgen_type) + parse_quote num_of read_typ ((K o K) ([], [])) target idf_of (fold_map oooo exprgen_type) (gen_add_syntax_tyco read_type raw_tyco) end; fun parse_syntax_const target raw_const = let - fun intern thy = CodegenConsts.read_const_typ thy raw_const; + fun intern thy = CodegenConsts.read_const thy raw_const; fun num_of thy = (length o fst o strip_type o Sign.the_const_type thy o fst o intern) thy; - fun idf_of thy = - let - val c_ty = intern thy; - val c = idf_of_const thy (CodegenTheorems.mk_thmtab thy [c_ty]) c_ty; - in c end; + fun idf_of thy = (idf_of_const thy o intern) thy; in - parse_quote num_of Sign.read_term consts_of target idf_of (fold_map oooo exprgen_term) - (gen_add_syntax_const CodegenConsts.read_const_typ raw_const) + parse_quote num_of Sign.read_term consts_of target idf_of (fold_map oooo exprgen_term') + (gen_add_syntax_const CodegenConsts.read_const raw_const) end; fun add_pretty_list target nill cons mk_list mk_char_string target_cons thy = @@ -921,31 +912,24 @@ fun code raw_cs seris thy = let - val cs = map (CodegenConsts.read_const_typ thy) raw_cs; + val cs = map (CodegenConsts.read_const thy) raw_cs; val targets = case map fst seris of [] => NONE | xs => SOME xs; val seris' = map_filter (fn (target, SOME seri) => SOME (target, seri) | _ => NONE) seris; fun generate' thy = case cs - of [] => ([], thy) + of [] => [] | _ => - thy - |> generate cs targets NONE (fold_map oooo ensure_def_const) cs; + generate thy (cs, []) targets NONE (fold_map oooo ensure_def_const') cs; fun serialize' thy [] (target, seri) = serialize thy target seri NONE : unit | serialize' thy cs (target, seri) = serialize thy target seri (SOME cs) : unit; + val cs = generate' thy; in - thy - |> generate' - |-> (fn cs => tap (fn thy => map (serialize' thy cs) seris')) + (map (serialize' thy cs) seris'; ()) end; -fun purge_consts raw_ts thy = - let - val cs = map (CodegenConsts.read_const_typ thy) raw_ts; - in fold CodegenTheorems.purge_defs cs thy end; - structure P = OuterParse and K = OuterKeyword @@ -964,19 +948,17 @@ in val (codeK, - syntax_classK, syntax_instK, syntax_tycoK, syntax_constK, - purgeK) = + syntax_classK, syntax_instK, syntax_tycoK, syntax_constK) = ("code_gen", - "code_class", "code_instance", "code_type", "code_const", - "code_purge"); + "code_class", "code_instance", "code_type", "code_const"); val codeP = - OuterSyntax.command codeK "generate and serialize executable code for constants" K.thy_decl ( + OuterSyntax.command codeK "generate and serialize executable code for constants" K.diag ( Scan.repeat P.term -- Scan.repeat (P.$$$ "(" |-- P.name :-- (fn target => (get_serializer target >> SOME) || pair NONE) --| P.$$$ ")") - >> (fn (raw_cs, seris) => Toplevel.theory (code raw_cs seris)) + >> (fn (raw_cs, seris) => Toplevel.keep (code raw_cs seris o Toplevel.theory_of)) ); val syntax_classP = @@ -1013,16 +995,9 @@ >> (Toplevel.theory o (fold o fold) (fold snd o snd)) ); -val purgeP = - OuterSyntax.command purgeK "purge all incrementally generated code" K.thy_decl - (Scan.succeed (Toplevel.theory purge_code)); - val _ = OuterSyntax.add_parsers [codeP, - syntax_classP, syntax_instP, syntax_tycoP, syntax_constP, purgeP]; + syntax_classP, syntax_instP, syntax_tycoP, syntax_constP]; end; (* local *) -(*code basis change notifications*) -val _ = Context.add_setup (CodegenTheorems.add_notify purge_defs); - end; (* struct *) diff -r 65bd267ae23f -r 6d75e02ed285 src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Tue Sep 19 15:22:24 2006 +0200 +++ b/src/Pure/Tools/codegen_serializer.ML Tue Sep 19 15:22:26 2006 +0200 @@ -35,7 +35,7 @@ -> (string -> CodegenThingol.itype pretty_syntax option) * (string -> CodegenThingol.iterm pretty_syntax option) -> string list - -> (string * 'a ref) * CodegenThingol.iterm -> CodegenThingol.module + -> (string * 'a option ref) * CodegenThingol.iterm -> CodegenThingol.module -> 'a; val eval_verbose: bool ref; val ml_fun_datatype: string @@ -152,7 +152,6 @@ val parse = Scan.repeat ( (sym "_" -- sym "_" >> K (Arg NOBR)) || (sym "_" >> K (Arg BR)) - || (sym "?" >> K Ignore) || (sym "/" |-- Scan.repeat (sym " ") >> (Pretty o Pretty.brk o length)) || Scan.depend (fn ctxt => $$ "{" |-- $$ "*" |-- Scan.repeat1 ( $$ "'" |-- Scan.one Symbol.not_eof @@ -191,7 +190,7 @@ fun mk fixity mfx ctxt = let val i = (length o List.filter is_arg) mfx; - val _ = if i > num_args ctxt then error "Too many arguments in codegen syntax" else (); + val _ = if i > num_args ctxt then error "Too many arguments in code syntax" else (); in (((i, i), fillin_mixfix fixity mfx), ctxt) end; in parse @@ -437,7 +436,7 @@ from_lookup BR classes ((str o ml_from_dictvar) v) | from_inst fxy (Context (classes, (v, i))) = - from_lookup BR (string_of_int (i+1) :: classes) + from_lookup BR (classes @ [string_of_int (i+1)]) ((str o ml_from_dictvar) v) in case lss of [] => str "()" @@ -552,7 +551,7 @@ else (str o resolv) f :: map (ml_from_expr BR) es and ml_from_app fxy (app_expr as ((c, (lss, ty)), es)) = - case (map (ml_from_insts BR) o filter_out null) lss + case if is_cons c then [] else (map (ml_from_insts BR) o filter_out null) lss of [] => from_app ml_mk_app ml_from_expr const_syntax fxy app_expr | lss => @@ -643,7 +642,7 @@ str (resolv co), str " of", Pretty.brk 1, - Pretty.enum " *" "" "" (map (ml_from_type NOBR) tys) + Pretty.enum " *" "" "" (map (ml_from_type (INFX (2, L))) tys) ] fun mk_datatype definer (t, (vs, cs)) = (Pretty.block o Pretty.breaks) ( @@ -838,9 +837,13 @@ | _ => SOME) (K NONE, syntax_tyco, syntax_const) (hidden, SOME [NameSpace.pack [nsp_eval, val_name]]); val _ = serializer modl'; val val_name_struct = NameSpace.append struct_name val_name; - val _ = use_text Context.ml_output (!eval_verbose) ("val _ = (" ^ ref_name ^ " := " ^ val_name_struct ^ ")"); - val value = ! reff; - in value end; + val _ = reff := NONE; + val _ = use_text Context.ml_output (!eval_verbose) ("val _ = (" ^ ref_name ^ " := SOME (" ^ val_name_struct ^ "))"); + in case !reff + of NONE => error ("Could not retrieve value of ML reference " ^ quote ref_name + ^ " (reference probably has been shadowed)") + | SOME value => value + end; fun mk_flat_ml_resolver names = let @@ -936,7 +939,10 @@ ]) end | hs_from_expr fxy (INum (n, _)) = - (str o IntInf.toString) n + if n > 0 then + (str o IntInf.toString) n + else + brackify BR [(str o Library.prefix "-" o IntInf.toString o IntInf.~) n] | hs_from_expr fxy (IChar (c, _)) = (str o enclose "'" "'") (let val i = (Char.ord o the o Char.fromString) c diff -r 65bd267ae23f -r 6d75e02ed285 src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Tue Sep 19 15:22:24 2006 +0200 +++ b/src/Pure/Tools/codegen_thingol.ML Tue Sep 19 15:22:26 2006 +0200 @@ -28,7 +28,7 @@ | IVar of vname | `$ of iterm * iterm | `|-> of (vname * itype) * iterm - | INum of IntInf.int (*non-negative!*) * iterm + | INum of IntInf.int * iterm | IChar of string (*length one!*) * iterm | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm; (*((discriminendum term (td), discriminendum type (ty)), @@ -821,8 +821,8 @@ val add_deps_of_typparms = fold (fn (v : vname, sort : sort) => fold (insert (op =)) sort); -fun add_deps_of_classlookup (Instance (tyco, lss)) = - insert (op =) tyco +fun add_deps_of_classlookup (Instance (inst, lss)) = + insert (op =) inst #> (fold o fold) add_deps_of_classlookup lss | add_deps_of_classlookup (Context (clss, _)) = fold (insert (op =)) clss;