--- 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";
--- 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));
--- /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;
--- /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*)
--- 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 *)
--- 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
--- 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;