# HG changeset patch # User haftmann # Date 1247033887 -7200 # Node ID baa8dce5bc45b5b3e2820463abc3d3cd5cab5174 # Parent 683b5e3b31fc0591f85c772da6b0cd8c3e688d7a tuned structure Code internally diff -r 683b5e3b31fc -r baa8dce5bc45 src/HOL/Tools/recfun_codegen.ML --- a/src/HOL/Tools/recfun_codegen.ML Wed Jul 08 06:43:30 2009 +0200 +++ b/src/HOL/Tools/recfun_codegen.ML Wed Jul 08 08:18:07 2009 +0200 @@ -26,7 +26,7 @@ fun add_thm NONE thm thy = Code.add_eqn thm thy | add_thm (SOME module_name) thm thy = let - val (thm', _) = Code.mk_eqn thy (K false) (thm, true) + val (thm', _) = Code.mk_eqn thy (thm, true) in thy |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name)) diff -r 683b5e3b31fc -r baa8dce5bc45 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Wed Jul 08 06:43:30 2009 +0200 +++ b/src/Pure/Isar/code.ML Wed Jul 08 08:18:07 2009 +0200 @@ -1,18 +1,18 @@ (* Title: Pure/Isar/code.ML Author: Florian Haftmann, TU Muenchen -Abstract executable content of theory. Management of data dependent on -executable content. Cache assumes non-concurrent processing of a single theory. +Abstract executable code of theory. Management of data dependent on +executable code. Cache assumes non-concurrent processing of a single theory. *) signature CODE = sig (*constants*) - val string_of_const: theory -> string -> string - val args_number: theory -> string -> int val check_const: theory -> term -> string val read_bare_const: theory -> string -> string * typ val read_const: theory -> string -> string + val string_of_const: theory -> string -> string + val args_number: theory -> string -> int val typscheme: theory -> string * typ -> (string * sort) list * typ (*constructor sets*) @@ -25,9 +25,9 @@ val resubst_alias: theory -> string -> string (*code equations*) - val mk_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool - val mk_eqn_warning: theory -> (string -> bool) -> thm -> (thm * bool) option - val mk_eqn_liberal: theory -> (string -> bool) -> thm -> (thm * bool) option + val mk_eqn: theory -> thm * bool -> thm * bool + val mk_eqn_warning: theory -> thm -> (thm * bool) option + val mk_eqn_liberal: theory -> thm -> (thm * bool) option val assert_eqn: theory -> thm * bool -> thm * bool val assert_eqns_const: theory -> string -> (thm * bool) list -> (thm * bool) list @@ -37,7 +37,7 @@ val norm_args: theory -> thm list -> thm list val norm_varnames: theory -> thm list -> thm list - (*executable content*) + (*executable code*) val add_datatype: (string * typ) list -> theory -> theory val add_datatype_cmd: string list -> theory -> theory val type_interpretation: @@ -97,23 +97,37 @@ structure Code : PRIVATE_CODE = struct -(* auxiliary *) +(** auxiliary **) + +(* printing *) fun string_of_typ thy = setmp show_sorts true (Syntax.string_of_typ_global thy); + fun string_of_const thy c = case AxClass.inst_of_param thy c of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco) | NONE => Sign.extern_const thy c; -fun args_number thy = length o fst o strip_type o Sign.the_const_type thy; + +(* constants *) +fun check_bare_const thy t = case try dest_Const t + of SOME c_ty => c_ty + | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t); -(* utilities *) +fun check_const thy = AxClass.unoverload_const thy o check_bare_const thy; + +fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy; + +fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy; fun typscheme thy (c, ty) = let val ty' = Logic.unvarifyT ty; in (map dest_TFree (Sign.const_typargs thy (c, ty')), Type.strip_sorts ty') end; + +(* code equation transformations *) + fun expand_eta thy k thm = let val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm; @@ -221,62 +235,272 @@ end; -(* reading constants as terms *) - -fun check_bare_const thy t = case try dest_Const t - of SOME c_ty => c_ty - | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t); - -fun check_const thy = AxClass.unoverload_const thy o check_bare_const thy; - -fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy; +(** code attributes **) -fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy; - - -(* const aliasses *) - -structure ConstAlias = TheoryDataFun -( - type T = ((string * string) * thm) list * class list; - val empty = ([], []); +structure Code_Attr = TheoryDataFun ( + type T = (string * attribute parser) list; + val empty = []; val copy = I; val extend = I; - fun merge _ ((alias1, classes1), (alias2, classes2)) : T = - (Library.merge (eq_snd Thm.eq_thm_prop) (alias1, alias2), - Library.merge (op =) (classes1, classes2)); + fun merge _ = AList.merge (op = : string * string -> bool) (K true); ); -fun add_const_alias thm thy = +fun add_attribute (attr as (name, _)) = + let + fun add_parser ("", parser) attrs = attrs |> rev |> AList.update (op =) ("", parser) |> rev + | add_parser (name, parser) attrs = (name, Args.$$$ name |-- parser) :: attrs; + in Code_Attr.map (fn attrs => if not (name = "") andalso AList.defined (op =) attrs name + then error ("Code attribute " ^ name ^ " already declared") else add_parser attr attrs) + end; + +val _ = Context.>> (Context.map_theory + (Attrib.setup (Binding.name "code") + (Scan.peek (fn context => + List.foldr op || Scan.fail (map snd (Code_Attr.get (Context.theory_of context))))) + "declare theorems for code generation")); + + +(** data store **) + +(* code equations *) + +type eqns = bool * (thm * bool) list lazy; + (*default flag, theorems with proper flag (perhaps lazy)*) + +fun pretty_lthms ctxt r = case Lazy.peek r + of SOME thms => map (ProofContext.pretty_thm ctxt o fst) (Exn.release thms) + | NONE => [Pretty.str "[...]"]; + +fun certificate thy f r = + case Lazy.peek r + of SOME thms => (Lazy.value o f thy) (Exn.release thms) + | NONE => let + val thy_ref = Theory.check_thy thy; + in Lazy.lazy (fn () => (f (Theory.deref thy_ref) o Lazy.force) r) end; + +fun add_drop_redundant thy (thm, proper) thms = + let + val args_of = snd o strip_comb o map_types Type.strip_sorts + o fst o Logic.dest_equals o Thm.plain_prop_of; + val args = args_of thm; + val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1); + fun matches_args args' = length args <= length args' andalso + Pattern.matchess thy (args, (map incr_idx o curry Library.take (length args)) args'); + fun drop (thm', proper') = if (proper orelse not proper') + andalso matches_args (args_of thm') then + (warning ("Code generator: dropping redundant code equation\n" ^ Display.string_of_thm thm'); true) + else false; + in (thm, proper) :: filter_out drop thms end; + +fun add_thm thy _ thm (false, thms) = (false, Lazy.map_force (add_drop_redundant thy thm) thms) + | add_thm thy true thm (true, thms) = (true, Lazy.map_force (fn thms => thms @ [thm]) thms) + | add_thm thy false thm (true, thms) = (false, Lazy.value [thm]); + +fun add_lthms lthms _ = (false, lthms); + +fun del_thm thm = (apsnd o Lazy.map_force) (remove (eq_fst Thm.eq_thm_prop) (thm, true)); + + +(* executable code data *) + +datatype spec = Spec of { + history_concluded: bool, + aliasses: ((string * string) * thm) list * class list, + eqns: ((bool * eqns) * (serial * eqns) list) Symtab.table + (*with explicit history*), + dtyps: ((serial * ((string * sort) list * (string * typ list) list)) list) Symtab.table + (*with explicit history*), + cases: (int * (int * string list)) Symtab.table * unit Symtab.table +}; + +fun make_spec ((history_concluded, aliasses), (eqns, (dtyps, cases))) = + Spec { history_concluded = history_concluded, aliasses = aliasses, + eqns = eqns, dtyps = dtyps, cases = cases }; +fun map_spec f (Spec { history_concluded = history_concluded, aliasses = aliasses, eqns = eqns, + dtyps = dtyps, cases = cases }) = + make_spec (f ((history_concluded, aliasses), (eqns, (dtyps, cases)))); +fun merge_spec (Spec { history_concluded = _, aliasses = aliasses1, eqns = eqns1, + dtyps = dtyps1, cases = (cases1, undefs1) }, + Spec { history_concluded = _, aliasses = aliasses2, eqns = eqns2, + dtyps = dtyps2, cases = (cases2, undefs2) }) = let - val (ofclass, eqn) = case try Logic.dest_equals (Thm.prop_of thm) - of SOME ofclass_eq => ofclass_eq - | _ => error ("Bad certificate: " ^ Display.string_of_thm thm); - val (T, class) = case try Logic.dest_of_class ofclass - of SOME T_class => T_class - | _ => error ("Bad certificate: " ^ Display.string_of_thm thm); - val tvar = case try Term.dest_TVar T - of SOME tvar => tvar - | _ => error ("Bad type: " ^ Display.string_of_thm thm); - val _ = if Term.add_tvars eqn [] = [tvar] then () - else error ("Inconsistent type: " ^ Display.string_of_thm thm); - val lhs_rhs = case try Logic.dest_equals eqn - of SOME lhs_rhs => lhs_rhs - | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn); - val c_c' = case try (pairself (check_const thy)) lhs_rhs - of SOME c_c' => c_c' - | _ => error ("Not an equation with two constants: " - ^ Syntax.string_of_term_global thy eqn); - val _ = if the_list (AxClass.class_of_param thy (snd c_c')) = [class] then () - else error ("Inconsistent class: " ^ Display.string_of_thm thm); - in thy |> - ConstAlias.map (fn (alias, classes) => - ((c_c', thm) :: alias, insert (op =) class classes)) - end; + val aliasses = (Library.merge (eq_snd Thm.eq_thm_prop) (pairself fst (aliasses1, aliasses2)), + Library.merge (op =) (pairself snd (aliasses1, aliasses2))); + fun merge_eqns ((_, history1), (_, history2)) = + let + val raw_history = AList.merge (op = : serial * serial -> bool) + (K true) (history1, history2) + val filtered_history = filter_out (fst o snd) raw_history + val history = if null filtered_history + then raw_history else filtered_history; + in ((false, (snd o hd) history), history) end; + val eqns = Symtab.join (K merge_eqns) (eqns1, eqns2); + val dtyps = Symtab.join (K (AList.merge (op =) (K true))) (dtyps1, dtyps2); + val cases = (Symtab.merge (K true) (cases1, cases2), + Symtab.merge (K true) (undefs1, undefs2)); + in make_spec ((false, aliasses), (eqns, (dtyps, cases))) end; + +fun history_concluded (Spec { history_concluded, ... }) = history_concluded; +fun the_aliasses (Spec { aliasses, ... }) = aliasses; +fun the_eqns (Spec { eqns, ... }) = eqns; +fun the_dtyps (Spec { dtyps, ... }) = dtyps; +fun the_cases (Spec { cases, ... }) = cases; +val map_history_concluded = map_spec o apfst o apfst; +val map_aliasses = map_spec o apfst o apsnd; +val map_eqns = map_spec o apsnd o apfst; +val map_dtyps = map_spec o apsnd o apsnd o apfst; +val map_cases = map_spec o apsnd o apsnd o apsnd; + + +(* data slots dependent on executable code *) + +(*private copy avoids potential conflict of table exceptions*) +structure Datatab = TableFun(type key = int val ord = int_ord); + +local + +type kind = { + empty: Object.T, + purge: theory -> string list -> Object.T -> Object.T +}; + +val kinds = ref (Datatab.empty: kind Datatab.table); +val kind_keys = ref ([]: serial list); + +fun invoke f k = case Datatab.lookup (! kinds) k + of SOME kind => f kind + | NONE => sys_error "Invalid code data identifier"; + +in + +fun declare_data empty purge = + let + val k = serial (); + val kind = {empty = empty, purge = purge}; + val _ = change kinds (Datatab.update (k, kind)); + val _ = change kind_keys (cons k); + in k end; + +fun invoke_init k = invoke (fn kind => #empty kind) k; + +fun invoke_purge_all thy cs = + fold (fn k => Datatab.map_entry k + (invoke (fn kind => #purge kind thy cs) k)) (! kind_keys); + +end; (*local*) + + +(* theory store *) + +local + +type data = Object.T Datatab.table; +val empty_data = Datatab.empty : data; + +structure Code_Data = TheoryDataFun +( + type T = spec * data ref; + val empty = (make_spec ((false, ([], [])), + (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))), ref empty_data); + fun copy (spec, data) = (spec, ref (! data)); + val extend = copy; + fun merge pp ((spec1, data1), (spec2, data2)) = + (merge_spec (spec1, spec2), ref empty_data); +); + +fun thy_data f thy = f ((snd o Code_Data.get) thy); + +fun get_ensure_init kind data_ref = + case Datatab.lookup (! data_ref) kind + of SOME x => x + | NONE => let val y = invoke_init kind + in (change data_ref (Datatab.update (kind, y)); y) end; + +in + +(* access to executable code *) + +val the_exec = fst o Code_Data.get; + +fun complete_class_params thy cs = + fold (fn c => case AxClass.inst_of_param thy c + of NONE => insert (op =) c + | SOME (c', _) => insert (op =) c' #> insert (op =) c) cs []; + +fun map_exec_purge touched f thy = + Code_Data.map (fn (exec, data) => (f exec, ref (case touched + of SOME cs => invoke_purge_all thy (complete_class_params thy cs) (! data) + | NONE => empty_data))) thy; + +val purge_data = (Code_Data.map o apsnd) (K (ref empty_data)); + +fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns + o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, Lazy.value [])), []))) + o apfst) (fn (_, eqns) => (true, f eqns)); + +fun del_eqns c = change_eqns true c (K (false, Lazy.value [])); + + +(* tackling equation history *) + +fun get_eqns thy c = + Symtab.lookup ((the_eqns o the_exec) thy) c + |> Option.map (Lazy.force o snd o snd o fst) + |> these; + +fun continue_history thy = if (history_concluded o the_exec) thy + then thy + |> (Code_Data.map o apfst o map_history_concluded) (K false) + |> SOME + else NONE; + +fun conclude_history thy = if (history_concluded o the_exec) thy + then NONE + else thy + |> (Code_Data.map o apfst) + ((map_eqns o Symtab.map) (fn ((changed, current), history) => + ((false, current), + if changed then (serial (), current) :: history else history)) + #> map_history_concluded (K true)) + |> SOME; + +val _ = Context.>> (Context.map_theory (Code_Data.init + #> Theory.at_begin continue_history + #> Theory.at_end conclude_history)); + + +(* access to data dependent on abstract executable code *) + +fun get_data (kind, _, dest) = thy_data (get_ensure_init kind #> dest); + +fun change_data (kind, mk, dest) = + let + fun chnge data_ref f = + let + val data = get_ensure_init kind data_ref; + val data' = f (dest data); + in (change data_ref (Datatab.update (kind, mk data')); data') end; + in thy_data chnge end; + +fun change_yield_data (kind, mk, dest) = + let + fun chnge data_ref f = + let + val data = get_ensure_init kind data_ref; + val (x, data') = f (dest data); + in (x, (change data_ref (Datatab.update (kind, mk data')); data')) end; + in thy_data chnge end; + +end; (*local*) + + +(** retrieval interfaces **) + +(* constant aliasses *) fun resubst_alias thy = let - val alias = fst (ConstAlias.get thy); + val alias = (fst o the_aliasses o the_exec) thy; val subst_inst_param = Option.map fst o AxClass.inst_of_param thy; fun subst_alias c = get_first (fn ((c', c''), _) => if c = c'' then SOME c' else NONE) alias; @@ -285,10 +509,17 @@ #> perhaps subst_alias end; -val triv_classes = snd o ConstAlias.get; +val triv_classes = snd o the_aliasses o the_exec; -(* constructor sets *) +(** foundation **) + +(* constants *) + +fun args_number thy = length o fst o strip_type o Sign.the_const_type thy; + + +(* datatypes *) fun constrset_of_consts thy cs = let @@ -328,6 +559,22 @@ val cs''' = map (inst vs) cs''; in (tyco, (vs, rev cs''')) end; +fun get_datatype thy tyco = + case these (Symtab.lookup ((the_dtyps o the_exec) thy) tyco) + of (_, spec) :: _ => spec + | [] => Sign.arity_number thy tyco + |> Name.invents Name.context Name.aT + |> map (rpair []) + |> rpair []; + +fun get_datatype_of_constr thy c = + case (snd o strip_type o Sign.the_const_type thy) c + of Type (tyco, _) => if member (op =) ((map fst o snd o get_datatype thy) tyco) c + then SOME tyco else NONE + | _ => NONE; + +fun is_constr thy = is_some o get_datatype_of_constr thy; + (* code equations *) @@ -342,7 +589,7 @@ in not (has_duplicates (op =) ((fold o fold_aterms) (fn Var (v, _) => cons v | _ => I) args [])) end; -fun gen_assert_eqn thy is_constr_head is_constr_pat (thm, proper) = +fun gen_assert_eqn thy is_constr_pat (thm, proper) = let val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm) @@ -394,7 +641,7 @@ then () else bad_thm ("Polymorphic constant as head in equation\n" ^ Display.string_of_thm thm) - val _ = if not (is_constr_head c) + val _ = if not (is_constr thy c) then () else bad_thm ("Constructor as head in equation\n" ^ Display.string_of_thm thm) @@ -407,22 +654,21 @@ ^ string_of_typ thy ty_decl) in (thm, proper) end; -fun assert_eqn thy is_constr = error_thm (gen_assert_eqn thy is_constr is_constr); +fun assert_eqn thy = error_thm (gen_assert_eqn thy (is_constr thy)); + +fun meta_rewrite thy = LocalDefs.meta_rewrite_rule (ProofContext.init thy); +fun mk_eqn thy = error_thm (gen_assert_eqn thy (K true)) o + apfst (meta_rewrite thy); + +fun mk_eqn_warning thy = Option.map (fn (thm, _) => (thm, is_linear thm)) + o warning_thm (gen_assert_eqn thy (K true)) o rpair false o meta_rewrite thy; + +fun mk_eqn_liberal thy = Option.map (fn (thm, _) => (thm, is_linear thm)) + o try_thm (gen_assert_eqn thy (K true)) o rpair false o meta_rewrite thy; (*those following are permissive wrt. to overloaded constants!*) -fun mk_eqn thy is_constr_head = error_thm (gen_assert_eqn thy is_constr_head (K true)) o - apfst (LocalDefs.meta_rewrite_rule (ProofContext.init thy)); - -fun mk_eqn_warning thy is_constr_head = Option.map (fn (thm, _) => (thm, is_linear thm)) - o warning_thm (gen_assert_eqn thy is_constr_head (K true)) - o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy); - -fun mk_eqn_liberal thy is_constr_head = Option.map (fn (thm, _) => (thm, is_linear thm)) - o try_thm (gen_assert_eqn thy is_constr_head (K true)) - o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy); - fun const_typ_eqn thy thm = let val (c, ty) = (dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm; @@ -432,8 +678,46 @@ fun typscheme_eqn thy = typscheme thy o const_typ_eqn thy; fun const_eqn thy = fst o const_typ_eqn thy; +fun assert_eqns_const thy c eqns = + let + fun cert (eqn as (thm, _)) = if c = const_eqn thy thm + then eqn else error ("Wrong head of code equation,\nexpected constant " + ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm thm) + in map (cert o assert_eqn thy) eqns end; -(* case cerificates *) +fun common_typ_eqns thy [] = [] + | common_typ_eqns thy [thm] = [thm] + | common_typ_eqns thy (thms as thm :: _) = (*FIXME is too general*) + let + fun incr_thm thm max = + let + val thm' = incr_indexes max thm; + val max' = Thm.maxidx_of thm' + 1; + in (thm', max') end; + val (thms', maxidx) = fold_map incr_thm thms 0; + val ty1 :: tys = map (snd o const_typ_eqn thy) thms'; + fun unify ty env = Sign.typ_unify thy (ty1, ty) env + handle Type.TUNIFY => + error ("Type unificaton failed, while unifying code equations\n" + ^ (cat_lines o map Display.string_of_thm) thms + ^ "\nwith types\n" + ^ (cat_lines o map (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 these_eqns thy c = + get_eqns thy c + |> (map o apfst) (Thm.transfer thy) + |> burrow_fst (common_typ_eqns thy); + +fun all_eqns thy = + Symtab.dest ((the_eqns o the_exec) thy) + |> maps (Lazy.force o snd o snd o fst o snd); + + +(* cases *) fun case_certificate thm = let @@ -475,255 +759,12 @@ handle Bind => error "bad case certificate" | TERM _ => error "bad case certificate"; - -(** code attributes **) - -structure CodeAttr = TheoryDataFun ( - type T = (string * attribute parser) list; - val empty = []; - val copy = I; - val extend = I; - fun merge _ = AList.merge (op = : string * string -> bool) (K true); -); - -fun add_attribute (attr as (name, _)) = - let - fun add_parser ("", parser) attrs = attrs |> rev |> AList.update (op =) ("", parser) |> rev - | add_parser (name, parser) attrs = (name, Args.$$$ name |-- parser) :: attrs; - in CodeAttr.map (fn attrs => if not (name = "") andalso AList.defined (op =) attrs name - then error ("Code attribute " ^ name ^ " already declared") else add_parser attr attrs) - end; - -val _ = Context.>> (Context.map_theory - (Attrib.setup (Binding.name "code") - (Scan.peek (fn context => - List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context))))) - "declare theorems for code generation")); - - - -(** logical and syntactical specification of executable code **) - -(* code equations *) - -type eqns = bool * (thm * bool) list lazy; - (*default flag, theorems with proper flag (perhaps lazy)*) - -fun pretty_lthms ctxt r = case Lazy.peek r - of SOME thms => map (ProofContext.pretty_thm ctxt o fst) (Exn.release thms) - | NONE => [Pretty.str "[...]"]; - -fun certificate thy f r = - case Lazy.peek r - of SOME thms => (Lazy.value o f thy) (Exn.release thms) - | NONE => let - val thy_ref = Theory.check_thy thy; - in Lazy.lazy (fn () => (f (Theory.deref thy_ref) o Lazy.force) r) end; +fun get_case_scheme thy = Symtab.lookup ((fst o the_cases o the_exec) thy); -fun add_drop_redundant thy (thm, proper) thms = - let - val args_of = snd o strip_comb o map_types Type.strip_sorts - o fst o Logic.dest_equals o Thm.plain_prop_of; - val args = args_of thm; - val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1); - fun matches_args args' = length args <= length args' andalso - Pattern.matchess thy (args, (map incr_idx o curry Library.take (length args)) args'); - fun drop (thm', proper') = if (proper orelse not proper') - andalso matches_args (args_of thm') then - (warning ("Code generator: dropping redundant code equation\n" ^ Display.string_of_thm thm'); true) - else false; - in (thm, proper) :: filter_out drop thms end; - -fun add_thm thy _ thm (false, thms) = (false, Lazy.map_force (add_drop_redundant thy thm) thms) - | add_thm thy true thm (true, thms) = (true, Lazy.map_force (fn thms => thms @ [thm]) thms) - | add_thm thy false thm (true, thms) = (false, Lazy.value [thm]); - -fun add_lthms lthms _ = (false, lthms); - -fun del_thm thm = (apsnd o Lazy.map_force) (remove (eq_fst Thm.eq_thm_prop) (thm, true)); - - -(* specification data *) - -datatype spec = Spec of { - concluded_history: bool, - eqns: ((bool * eqns) * (serial * eqns) list) Symtab.table - (*with explicit history*), - dtyps: ((serial * ((string * sort) list * (string * typ list) list)) list) Symtab.table - (*with explicit history*), - cases: (int * (int * string list)) Symtab.table * unit Symtab.table -}; - -fun make_spec ((concluded_history, eqns), (dtyps, cases)) = - Spec { concluded_history = concluded_history, eqns = eqns, dtyps = dtyps, cases = cases }; -fun map_spec f (Spec { concluded_history = concluded_history, eqns = eqns, - dtyps = dtyps, cases = cases }) = - make_spec (f ((concluded_history, eqns), (dtyps, cases))); -fun merge_spec (Spec { concluded_history = _, eqns = eqns1, dtyps = dtyps1, cases = (cases1, undefs1) }, - Spec { concluded_history = _, eqns = eqns2, dtyps = dtyps2, cases = (cases2, undefs2) }) = - let - fun merge_eqns ((_, history1), (_, history2)) = - let - val raw_history = AList.merge (op = : serial * serial -> bool) - (K true) (history1, history2) - val filtered_history = filter_out (fst o snd) raw_history - val history = if null filtered_history - then raw_history else filtered_history; - in ((false, (snd o hd) history), history) end; - val eqns = Symtab.join (K merge_eqns) (eqns1, eqns2); - val dtyps = Symtab.join (K (AList.merge (op =) (K true))) (dtyps1, dtyps2); - val cases = (Symtab.merge (K true) (cases1, cases2), - Symtab.merge (K true) (undefs1, undefs2)); - in make_spec ((false, eqns), (dtyps, cases)) end; - - -(* code setup data *) - -fun the_spec (Spec x) = x; -fun the_eqns (Spec { eqns, ... }) = eqns; -fun the_dtyps (Spec { dtyps, ... }) = dtyps; -fun the_cases (Spec { cases, ... }) = cases; -fun history_concluded (Spec { concluded_history, ... }) = concluded_history; -val map_concluded_history = map_spec o apfst o apfst; -val map_eqns = map_spec o apfst o apsnd; -val map_dtyps = map_spec o apsnd o apfst; -val map_cases = map_spec o apsnd o apsnd; +val undefineds = Symtab.keys o snd o the_cases o the_exec; -(* data slots dependent on executable content *) - -(*private copy avoids potential conflict of table exceptions*) -structure Datatab = TableFun(type key = int val ord = int_ord); - -local - -type kind = { - empty: Object.T, - purge: theory -> string list -> Object.T -> Object.T -}; - -val kinds = ref (Datatab.empty: kind Datatab.table); -val kind_keys = ref ([]: serial list); - -fun invoke f k = case Datatab.lookup (! kinds) k - of SOME kind => f kind - | NONE => sys_error "Invalid code data identifier"; - -in - -fun declare_data empty purge = - let - val k = serial (); - val kind = {empty = empty, purge = purge}; - val _ = change kinds (Datatab.update (k, kind)); - val _ = change kind_keys (cons k); - in k end; - -fun invoke_init k = invoke (fn kind => #empty kind) k; - -fun invoke_purge_all thy cs = - fold (fn k => Datatab.map_entry k - (invoke (fn kind => #purge kind thy cs) k)) (! kind_keys); - -end; (*local*) - - -(** theory store **) - -local - -type data = Object.T Datatab.table; -val empty_data = Datatab.empty : data; - -structure Code_Data = TheoryDataFun -( - type T = spec * data ref; - val empty = (make_spec ((false, Symtab.empty), - (Symtab.empty, (Symtab.empty, Symtab.empty))), ref empty_data); - fun copy (spec, data) = (spec, ref (! data)); - val extend = copy; - fun merge pp ((spec1, data1), (spec2, data2)) = - (merge_spec (spec1, spec2), ref empty_data); -); - -fun thy_data f thy = f ((snd o Code_Data.get) thy); - -fun get_ensure_init kind data_ref = - case Datatab.lookup (! data_ref) kind - of SOME x => x - | NONE => let val y = invoke_init kind - in (change data_ref (Datatab.update (kind, y)); y) end; - -in - -(* access to executable content *) - -val the_exec = fst o Code_Data.get; - -fun complete_class_params thy cs = - fold (fn c => case AxClass.inst_of_param thy c - of NONE => insert (op =) c - | SOME (c', _) => insert (op =) c' #> insert (op =) c) cs []; - -fun map_exec_purge touched f thy = - Code_Data.map (fn (exec, data) => (f exec, ref (case touched - of SOME cs => invoke_purge_all thy (complete_class_params thy cs) (! data) - | NONE => empty_data))) thy; - -val purge_data = (Code_Data.map o apsnd) (K (ref empty_data)); - - -(* tackling equation history *) - -fun get_eqns thy c = - Symtab.lookup ((the_eqns o the_exec) thy) c - |> Option.map (Lazy.force o snd o snd o fst) - |> these; - -fun continue_history thy = if (history_concluded o the_exec) thy - then thy - |> (Code_Data.map o apfst o map_concluded_history) (K false) - |> SOME - else NONE; - -fun conclude_history thy = if (history_concluded o the_exec) thy - then NONE - else thy - |> (Code_Data.map o apfst) - ((map_eqns o Symtab.map) (fn ((changed, current), history) => - ((false, current), - if changed then (serial (), current) :: history else history)) - #> map_concluded_history (K true)) - |> SOME; - -val _ = Context.>> (Context.map_theory (Code_Data.init - #> Theory.at_begin continue_history - #> Theory.at_end conclude_history)); - - -(* access to data dependent on abstract executable content *) - -fun get_data (kind, _, dest) = thy_data (get_ensure_init kind #> dest); - -fun change_data (kind, mk, dest) = - let - fun chnge data_ref f = - let - val data = get_ensure_init kind data_ref; - val data' = f (dest data); - in (change data_ref (Datatab.update (kind, mk data')); data') end; - in thy_data chnge end; - -fun change_yield_data (kind, mk, dest) = - let - fun chnge data_ref f = - let - val data = get_ensure_init kind data_ref; - val (x, data') = f (dest data); - in (x, (change data_ref (Datatab.update (kind, mk data')); data')) end; - in thy_data chnge end; - -end; (*local*) +(* diagnostic *) fun print_codesetup thy = let @@ -772,102 +813,41 @@ end; -(** theorem transformation and certification **) +(** declaring executable ingredients **) + +(* constant aliasses *) -fun common_typ_eqns thy [] = [] - | common_typ_eqns thy [thm] = [thm] - | common_typ_eqns thy (thms as thm :: _) = (*FIXME is too general*) - let - fun incr_thm thm max = - let - val thm' = incr_indexes max thm; - val max' = Thm.maxidx_of thm' + 1; - in (thm', max') end; - val (thms', maxidx) = fold_map incr_thm thms 0; - val ty1 :: tys = map (snd o const_typ_eqn thy) thms'; - fun unify ty env = Sign.typ_unify thy (ty1, ty) env - handle Type.TUNIFY => - error ("Type unificaton failed, while unifying code equations\n" - ^ (cat_lines o map Display.string_of_thm) thms - ^ "\nwith types\n" - ^ (cat_lines o map (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 add_const_alias thm thy = + let + val (ofclass, eqn) = case try Logic.dest_equals (Thm.prop_of thm) + of SOME ofclass_eq => ofclass_eq + | _ => error ("Bad certificate: " ^ Display.string_of_thm thm); + val (T, class) = case try Logic.dest_of_class ofclass + of SOME T_class => T_class + | _ => error ("Bad certificate: " ^ Display.string_of_thm thm); + val tvar = case try Term.dest_TVar T + of SOME tvar => tvar + | _ => error ("Bad type: " ^ Display.string_of_thm thm); + val _ = if Term.add_tvars eqn [] = [tvar] then () + else error ("Inconsistent type: " ^ Display.string_of_thm thm); + val lhs_rhs = case try Logic.dest_equals eqn + of SOME lhs_rhs => lhs_rhs + | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn); + val c_c' = case try (pairself (check_const thy)) lhs_rhs + of SOME c_c' => c_c' + | _ => error ("Not an equation with two constants: " + ^ Syntax.string_of_term_global thy eqn); + val _ = if the_list (AxClass.class_of_param thy (snd c_c')) = [class] then () + else error ("Inconsistent class: " ^ Display.string_of_thm thm); + in thy |> + (map_exec_purge NONE o map_aliasses) (fn (alias, classes) => + ((c_c', thm) :: alias, insert (op =) class classes)) + end; -(** interfaces and attributes **) - -fun get_datatype thy tyco = - case these (Symtab.lookup ((the_dtyps o the_exec) thy) tyco) - of (_, spec) :: _ => spec - | [] => Sign.arity_number thy tyco - |> Name.invents Name.context Name.aT - |> map (rpair []) - |> rpair []; - -fun get_datatype_of_constr thy c = - case (snd o strip_type o Sign.the_const_type thy) c - of Type (tyco, _) => if member (op =) ((map fst o snd o get_datatype thy) tyco) c - then SOME tyco else NONE - | _ => NONE; - -fun is_constr thy = is_some o get_datatype_of_constr thy; - -val assert_eqn = fn thy => assert_eqn thy (is_constr thy); - -fun assert_eqns_const thy c eqns = - let - fun cert (eqn as (thm, _)) = if c = const_eqn thy thm - then eqn else error ("Wrong head of code equation,\nexpected constant " - ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm thm) - in map (cert o assert_eqn thy) eqns end; - -fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns - o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, Lazy.value [])), []))) - o apfst) (fn (_, eqns) => (true, f eqns)); - -fun gen_add_eqn default (eqn as (thm, _)) thy = - let val c = const_eqn thy thm - in change_eqns false c (add_thm thy default eqn) thy end; +(* datatypes *) -fun add_eqn thm thy = - gen_add_eqn false (mk_eqn thy (is_constr thy) (thm, true)) thy; - -fun add_warning_eqn thm thy = - case mk_eqn_warning thy (is_constr thy) thm - of SOME eqn => gen_add_eqn false eqn thy - | NONE => thy; - -fun add_default_eqn thm thy = - case mk_eqn_liberal thy (is_constr thy) thm - of SOME eqn => gen_add_eqn true eqn thy - | NONE => thy; - -fun add_nbe_eqn thm thy = - gen_add_eqn false (mk_eqn thy (is_constr thy) (thm, false)) thy; - -fun add_eqnl (c, lthms) thy = - let - val lthms' = certificate thy (fn thy => assert_eqns_const thy c) lthms; - in change_eqns false c (add_lthms lthms') thy end; - -val add_default_eqn_attribute = Thm.declaration_attribute - (fn thm => Context.mapping (add_default_eqn thm) I); -val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute); - -fun del_eqn thm thy = case mk_eqn_liberal thy (is_constr thy) thm - of SOME (thm, _) => change_eqns true (const_eqn thy thm) (del_thm thm) thy - | NONE => thy; - -fun del_eqns c = change_eqns true c (K (false, Lazy.value [])); - -fun get_case_scheme thy = Symtab.lookup ((fst o the_cases o the_exec) thy); - -val undefineds = Symtab.keys o snd o the_cases o the_exec; - -structure TypeInterpretation = InterpretationFun(type T = string * serial val eq = eq_snd (op =) : T * T -> bool); +structure Type_Interpretation = InterpretationFun(type T = string * serial val eq = eq_snd (op =) : T * T -> bool); fun add_datatype raw_cs thy = let @@ -884,10 +864,10 @@ |> map_exec_purge NONE ((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos)) #> (map_cases o apfst) drop_outdated_cases) - |> TypeInterpretation.data (tyco, serial ()) + |> Type_Interpretation.data (tyco, serial ()) end; -fun type_interpretation f = TypeInterpretation.interpretation +fun type_interpretation f = Type_Interpretation.interpretation (fn (tyco, _) => fn thy => f (tyco, get_datatype thy tyco) thy); fun add_datatype_cmd raw_cs thy = @@ -895,6 +875,59 @@ val cs = map (read_bare_const thy) raw_cs; in add_datatype cs thy end; + +(* code equations *) + +fun gen_add_eqn default (eqn as (thm, _)) thy = + let val c = const_eqn thy thm + in change_eqns false c (add_thm thy default eqn) thy end; + +fun add_eqn thm thy = + gen_add_eqn false (mk_eqn thy (thm, true)) thy; + +fun add_warning_eqn thm thy = + case mk_eqn_warning thy thm + of SOME eqn => gen_add_eqn false eqn thy + | NONE => thy; + +fun add_default_eqn thm thy = + case mk_eqn_liberal thy thm + of SOME eqn => gen_add_eqn true eqn thy + | NONE => thy; + +fun add_nbe_eqn thm thy = + gen_add_eqn false (mk_eqn thy (thm, false)) thy; + +fun add_eqnl (c, lthms) thy = + let + val lthms' = certificate thy (fn thy => assert_eqns_const thy c) lthms; + in change_eqns false c (add_lthms lthms') thy end; + +val add_default_eqn_attribute = Thm.declaration_attribute + (fn thm => Context.mapping (add_default_eqn thm) I); +val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute); + +fun del_eqn thm thy = case mk_eqn_liberal thy thm + of SOME (thm, _) => change_eqns true (const_eqn thy thm) (del_thm thm) thy + | NONE => thy; + +val _ = Context.>> (Context.map_theory + (let + fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I); + fun add_simple_attribute (name, f) = + add_attribute (name, Scan.succeed (mk_attribute f)); + fun add_del_attribute (name, (add, del)) = + add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del) + || Scan.succeed (mk_attribute add)) + in + Type_Interpretation.init + #> add_del_attribute ("", (add_warning_eqn, del_eqn)) + #> add_simple_attribute ("nbe", add_nbe_eqn) + end)); + + +(* cases *) + fun add_case thm thy = let val (c, (k, case_pats)) = case_cert thm; @@ -907,35 +940,12 @@ fun add_undefined c thy = (map_exec_purge (SOME [c]) o map_cases o apsnd) (Symtab.update (c, ())) thy; -val _ = Context.>> (Context.map_theory - (let - fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I); - fun add_simple_attribute (name, f) = - add_attribute (name, Scan.succeed (mk_attribute f)); - fun add_del_attribute (name, (add, del)) = - add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del) - || Scan.succeed (mk_attribute add)) - in - TypeInterpretation.init - #> add_del_attribute ("", (add_warning_eqn, del_eqn)) - #> add_simple_attribute ("nbe", add_nbe_eqn) - end)); - -fun these_eqns thy c = - get_eqns thy c - |> (map o apfst) (Thm.transfer thy) - |> burrow_fst (common_typ_eqns thy); - -fun all_eqns thy = - Symtab.dest ((the_eqns o the_exec) thy) - |> maps (Lazy.force o snd o snd o fst o snd); - end; (*struct*) -(** type-safe interfaces for data depedent on executable content **) +(** type-safe interfaces for data depedent on executable code **) -functor CodeDataFun(Data: CODE_DATA_ARGS): CODE_DATA = +functor Code_Data_Fun(Data: CODE_DATA_ARGS): CODE_DATA = struct type T = Data.T; diff -r 683b5e3b31fc -r baa8dce5bc45 src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Wed Jul 08 06:43:30 2009 +0200 +++ b/src/Tools/Code/code_preproc.ML Wed Jul 08 08:18:07 2009 +0200 @@ -450,7 +450,7 @@ (** store for preprocessed arities and code equations **) -structure Wellsorted = CodeDataFun +structure Wellsorted = Code_Data_Fun ( type T = ((string * class) * sort list) list * code_graph; val empty = ([], Graph.empty); diff -r 683b5e3b31fc -r baa8dce5bc45 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Wed Jul 08 06:43:30 2009 +0200 +++ b/src/Tools/Code/code_thingol.ML Wed Jul 08 08:18:07 2009 +0200 @@ -722,15 +722,15 @@ ensure_inst thy algbr funcgr inst ##>> (fold_map o fold_map) mk_dict yss #>> (fn (inst, dss) => DictConst (inst, dss)) - | mk_dict (Local (classrels, (v, (k, sort)))) = + | mk_dict (Local (classrels, (v, (n, sort)))) = fold_map (ensure_classrel thy algbr funcgr) classrels - #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort)))) + #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (n, length sort)))) in fold_map mk_dict typargs end; (* store *) -structure Program = CodeDataFun +structure Program = Code_Data_Fun ( type T = naming * program; val empty = (empty_naming, Graph.empty); diff -r 683b5e3b31fc -r baa8dce5bc45 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Wed Jul 08 06:43:30 2009 +0200 +++ b/src/Tools/nbe.ML Wed Jul 08 08:18:07 2009 +0200 @@ -408,7 +408,7 @@ (* function store *) -structure Nbe_Functions = CodeDataFun +structure Nbe_Functions = Code_Data_Fun ( type T = Code_Thingol.naming * ((Univ option * int) Graph.T * (int * string Inttab.table)); val empty = (Code_Thingol.empty_naming, (Graph.empty, (0, Inttab.empty)));