# HG changeset patch # User haftmann # Date 1222412992 -7200 # Node ID 8437fb3952941c7c5a6376739159b17240be49e1 # Parent 10ea34297962690e020a2da9ee0511a6c599ba00 clarified function transformator interface diff -r 10ea34297962 -r 8437fb395294 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Fri Sep 26 09:09:51 2008 +0200 +++ b/src/Pure/Isar/code.ML Fri Sep 26 09:09:52 2008 +0200 @@ -8,14 +8,14 @@ signature CODE = sig - val add_func: thm -> theory -> theory - val add_nonlinear_func: thm -> theory -> theory - val add_liberal_func: thm -> theory -> theory - val add_default_func: thm -> theory -> theory - val add_default_func_attr: Attrib.src - val del_func: thm -> theory -> theory - val del_funcs: string -> theory -> theory - val add_funcl: string * (thm * bool) list Susp.T -> theory -> theory + val add_eqn: thm -> theory -> theory + val add_nonlinear_eqn: thm -> theory -> theory + val add_liberal_eqn: thm -> theory -> theory + val add_default_eqn: thm -> theory -> theory + val add_default_eqn_attr: Attrib.src + val del_eqn: thm -> theory -> theory + val del_eqns: string -> theory -> theory + val add_eqnl: string * (thm * bool) list Susp.T -> theory -> theory val map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory val map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory val add_inline: thm -> theory -> theory @@ -35,7 +35,7 @@ val coregular_algebra: theory -> Sorts.algebra val operational_algebra: theory -> (sort -> sort) * Sorts.algebra - val these_funcs: theory -> string -> (thm * bool) list + val these_eqns: theory -> string -> (thm * bool) list val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list) val get_datatype_of_constr: theory -> string -> string option val get_case_data: theory -> string -> (int * string list) option @@ -172,23 +172,23 @@ (* specification data *) datatype spec = Spec of { - funcs: (bool * (thm * bool) list Susp.T) Symtab.table, + eqns: (bool * (thm * bool) list Susp.T) Symtab.table, dtyps: ((string * sort) list * (string * typ list) list) Symtab.table, cases: (int * string list) Symtab.table * unit Symtab.table }; -fun mk_spec (funcs, (dtyps, cases)) = - Spec { funcs = funcs, dtyps = dtyps, cases = cases }; -fun map_spec f (Spec { funcs = funcs, dtyps = dtyps, cases = cases }) = - mk_spec (f (funcs, (dtyps, cases))); -fun merge_spec (Spec { funcs = funcs1, dtyps = dtyps1, cases = (cases1, undefs1) }, - Spec { funcs = funcs2, dtyps = dtyps2, cases = (cases2, undefs2) }) = +fun mk_spec (eqns, (dtyps, cases)) = + Spec { eqns = eqns, dtyps = dtyps, cases = cases }; +fun map_spec f (Spec { eqns = eqns, dtyps = dtyps, cases = cases }) = + mk_spec (f (eqns, (dtyps, cases))); +fun merge_spec (Spec { eqns = eqns1, dtyps = dtyps1, cases = (cases1, undefs1) }, + Spec { eqns = eqns2, dtyps = dtyps2, cases = (cases2, undefs2) }) = let - val funcs = Symtab.join (K merge_defthms) (funcs1, funcs2); + val eqns = Symtab.join (K merge_defthms) (eqns1, eqns2); val dtyps = merge_dtyps (dtyps1, dtyps2); val cases = (Symtab.merge (K true) (cases1, cases2), Symtab.merge (K true) (undefs1, undefs2)); - in mk_spec (funcs, (dtyps, cases)) end; + in mk_spec (eqns, (dtyps, cases)) end; (* pre- and postprocessor *) @@ -234,11 +234,11 @@ fun the_thmproc (Exec { thmproc = Thmproc x, ...}) = x; fun the_spec (Exec { spec = Spec x, ...}) = x; -val the_funcs = #funcs o the_spec; +val the_eqns = #eqns o the_spec; val the_dtyps = #dtyps o the_spec; val the_cases = #cases o the_spec; val map_thmproc = map_exec o apfst o map_thmproc; -val map_funcs = map_exec o apsnd o map_spec o apfst; +val map_eqns = map_exec o apsnd o map_spec o apfst; val map_dtyps = map_exec o apsnd o map_spec o apsnd o apfst; val map_cases = map_exec o apsnd o map_spec o apsnd o apsnd; @@ -358,7 +358,7 @@ let val ctxt = ProofContext.init thy; val exec = the_exec thy; - fun pretty_func (s, (_, lthms)) = + fun pretty_eqn (s, (_, lthms)) = (Pretty.block o Pretty.fbreaks) ( Pretty.str s :: pretty_lthms ctxt lthms ); @@ -378,7 +378,7 @@ val pre = (#pre o the_thmproc) exec; val post = (#post o the_thmproc) exec; val functrans = (map fst o #functrans o the_thmproc) exec; - val funcs = the_funcs exec + val eqns = the_eqns exec |> Symtab.dest |> (map o apfst) (Code_Unit.string_of_const thy) |> sort (string_ord o pairself fst); @@ -392,7 +392,7 @@ Pretty.block ( Pretty.str "defining equations:" :: Pretty.fbrk - :: (Pretty.fbreaks o map pretty_func) funcs + :: (Pretty.fbreaks o map pretty_eqn) eqns ), Pretty.block [ Pretty.str "preprocessing simpset:", @@ -421,14 +421,13 @@ (** theorem transformation and certification **) -fun const_of thy = dest_Const o fst o strip_comb o fst o Logic.dest_equals - o ObjectLogic.drop_judgment thy o Thm.plain_prop_of; +fun const_of thy = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of; + +fun const_of_eqn thy = AxClass.unoverload_const thy o const_of thy; -fun const_of_func thy = AxClass.unoverload_const thy o const_of thy; - -fun common_typ_funcs [] = [] - | common_typ_funcs [thm] = [thm] - | common_typ_funcs (thms as thm :: _) = (*FIXME is too general*) +fun common_typ_eqns [] = [] + | common_typ_eqns [thm] = [thm] + | common_typ_eqns (thms as thm :: _) = (*FIXME is too general*) let val thy = Thm.theory_of_thm thm; fun incr_thm thm max = @@ -451,7 +450,7 @@ fun certify_const thy const thms = let - fun cert thm = if const = const_of_func thy thm + fun cert thm = if const = const_of_eqn thy thm then thm else error ("Wrong head of defining equation,\nexpected constant " ^ Code_Unit.string_of_const thy const ^ "\n" ^ Display.string_of_thm thm) in map cert thms end; @@ -475,15 +474,15 @@ let val vs = Name.invents Name.context "" (Sign.arity_number thy tyco); val classparams = (map fst o these o try (#params o AxClass.get_info thy)) class; - val funcs = classparams + val eqns = classparams |> map_filter (fn c => try (AxClass.param_of_inst thy) (c, tyco)) - |> map (Symtab.lookup ((the_funcs o the_exec) thy)) + |> map (Symtab.lookup ((the_eqns o the_exec) thy)) |> (map o Option.map) (map fst o Susp.force o snd) |> maps these |> map (Thm.transfer thy); fun sorts_of [Type (_, tys)] = map (snd o dest_TVar) tys | sorts_of tys = map (snd o dest_TVar) tys; - val sorts = map (sorts_of o Sign.const_typargs thy o const_of thy) funcs; + val sorts = map (sorts_of o Sign.const_typargs thy o const_of thy) eqns; in sorts end; fun weakest_constraints thy algebra (class, tyco) = @@ -548,7 +547,12 @@ val classparam_weakest_typ = gen_classparam_typ weakest_constraints; val classparam_strongest_typ = gen_classparam_typ strongest_constraints; -fun assert_func_typ thm = +fun assert_eqn_linear (eqn as (thm, linear)) = + if linear then eqn else Code_Unit.bad_thm + ("Duplicate variables on left hand side of defining equation:\n" + ^ Display.string_of_thm thm); + +fun assert_eqn_typ (thm, linear) = let val thy = Thm.theory_of_thm thm; fun check_typ_classparam tyco (c, thm) = @@ -597,12 +601,18 @@ case AxClass.inst_of_param thy c of SOME (c, tyco) => check_typ_classparam tyco (c, thm) | NONE => check_typ_fun (c, thm); - in check_typ (const_of_func thy thm, thm) end; + val c = const_of_eqn thy thm; + val thm' = check_typ (c, thm); + in (thm', linear) end; -fun mk_func linear = Code_Unit.error_thm (assert_func_typ o Code_Unit.mk_func linear); -val mk_liberal_func = Code_Unit.warning_thm (assert_func_typ o Code_Unit.mk_func true); -val mk_syntactic_func = Code_Unit.warning_thm (assert_func_typ o Code_Unit.mk_func false); -val mk_default_func = Code_Unit.try_thm (assert_func_typ o Code_Unit.mk_func true); +fun mk_eqn linear = Code_Unit.error_thm + (assert_eqn_typ o (if linear then assert_eqn_linear else I) o Code_Unit.mk_eqn); +val mk_liberal_eqn = Code_Unit.warning_thm + (assert_eqn_typ o assert_eqn_linear o Code_Unit.mk_eqn); +val mk_syntactic_eqn = Code_Unit.warning_thm + (assert_eqn_typ o Code_Unit.mk_eqn); +val mk_default_eqn = Code_Unit.try_thm + (assert_eqn_typ o assert_eqn_linear o Code_Unit.mk_eqn); end; (*local*) @@ -641,54 +651,54 @@ val is_undefined = Symtab.defined o snd o the_cases o the_exec; -fun gen_add_func linear strict default thm thy = - case (if strict then SOME o mk_func linear else mk_liberal_func) thm - of SOME func => +fun gen_add_eqn linear strict default thm thy = + case (if strict then SOME o mk_eqn linear else mk_liberal_eqn) thm + of SOME (thm, _) => let - val c = const_of_func thy func; + val c = const_of_eqn thy thm; val _ = if strict andalso (is_some o AxClass.class_of_param thy) c then error ("Rejected polymorphic equation for overloaded constant:\n" ^ Display.string_of_thm thm) else (); val _ = if strict andalso (is_some o get_datatype_of_constr thy) c then error ("Rejected equation for datatype constructor:\n" - ^ Display.string_of_thm func) + ^ Display.string_of_thm thm) else (); in - (map_exec_purge (SOME [c]) o map_funcs) (Symtab.map_default - (c, (true, Susp.value [])) (add_thm default (func, linear))) thy + (map_exec_purge (SOME [c]) o map_eqns) (Symtab.map_default + (c, (true, Susp.value [])) (add_thm default (thm, linear))) thy end | NONE => thy; -val add_func = gen_add_func true true false; -val add_liberal_func = gen_add_func true false false; -val add_default_func = gen_add_func true false true; -val add_nonlinear_func = gen_add_func false true false; +val add_eqn = gen_add_eqn true true false; +val add_liberal_eqn = gen_add_eqn true false false; +val add_default_eqn = gen_add_eqn true false true; +val add_nonlinear_eqn = gen_add_eqn false true false; -fun del_func thm thy = case mk_syntactic_func thm - of SOME func => let - val c = const_of_func thy func; - in map_exec_purge (SOME [c]) (map_funcs - (Symtab.map_entry c (del_thm func))) thy +fun del_eqn thm thy = case mk_syntactic_eqn thm + of SOME (thm, _) => let + val c = const_of_eqn thy thm; + in map_exec_purge (SOME [c]) (map_eqns + (Symtab.map_entry c (del_thm thm))) thy end | NONE => thy; -fun del_funcs c = map_exec_purge (SOME [c]) - (map_funcs (Symtab.map_entry c (K (false, Susp.value [])))); +fun del_eqns c = map_exec_purge (SOME [c]) + (map_eqns (Symtab.map_entry c (K (false, Susp.value [])))); -fun add_funcl (c, lthms) thy = +fun add_eqnl (c, lthms) thy = let val lthms' = certificate thy (fn thy => certify_const thy c) lthms; (*FIXME must check compatibility with sort algebra; alas, naive checking results in non-termination!*) in map_exec_purge (SOME [c]) - (map_funcs (Symtab.map_default (c, (true, Susp.value [])) + (map_eqns (Symtab.map_default (c, (true, Susp.value [])) (add_lthms lthms'))) thy end; -val add_default_func_attr = Attrib.internal (fn _ => Thm.declaration_attribute - (fn thm => Context.mapping (add_default_func thm) I)); +val add_default_eqn_attr = Attrib.internal (fn _ => Thm.declaration_attribute + (fn thm => Context.mapping (add_default_eqn thm) I)); structure TypeInterpretation = InterpretationFun(type T = string * serial val eq = eq_snd (op =) : T * T -> bool); @@ -703,7 +713,7 @@ in thy |> map_exec_purge purge_cs (map_dtyps (Symtab.update (tyco, vs_cos)) - #> map_funcs (fold (Symtab.delete_safe o fst) cs)) + #> map_eqns (fold (Symtab.delete_safe o fst) cs)) |> TypeInterpretation.data (tyco, serial ()) end; @@ -762,8 +772,8 @@ || Scan.succeed (mk_attribute add)) in TypeInterpretation.init - #> add_del_attribute ("func", (add_func, del_func)) - #> add_simple_attribute ("nbe", add_nonlinear_func) + #> add_del_attribute ("func", (add_eqn, del_eqn)) + #> add_simple_attribute ("nbe", add_nonlinear_eqn) #> add_del_attribute ("inline", (add_inline, del_inline)) #> add_del_attribute ("post", (add_post, del_post)) end)); @@ -776,16 +786,12 @@ fun apply_functrans thy [] = [] | apply_functrans thy (thms as (thm, _) :: _) = let - val const = const_of_func thy thm; + val const = const_of_eqn thy thm; val functrans = (map (fn (_, (_, f)) => f thy) o #functrans o the_thmproc o the_exec) thy; val thms' = perhaps (perhaps_loop (perhaps_apply functrans)) (map fst thms); val thms'' = certify_const thy const thms'; - val linears = map snd thms; - in (*FIXME temporary workaround*) if length thms'' = length linears - then thms'' ~~ linears - else map (rpair true) thms'' - end; + in map Code_Unit.add_linear thms'' end; fun rhs_conv conv thm = let @@ -807,10 +813,10 @@ in thms |> apply_functrans thy - |> (map o apfst) (Code_Unit.rewrite_func pre) + |> (map o apfst) (Code_Unit.rewrite_eqn pre) (*FIXME - must check here: rewrite rule, defining equation, proper constant *) |> (map o apfst) (AxClass.unoverload thy) - |> burrow_fst common_typ_funcs + |> burrow_fst common_typ_eqns end; @@ -850,28 +856,28 @@ local -fun get_funcs thy const = - Symtab.lookup ((the_funcs o the_exec) thy) const +fun get_eqns thy const = + Symtab.lookup ((the_eqns o the_exec) thy) const |> Option.map (Susp.force o snd) |> these |> (map o apfst) (Thm.transfer thy); in -fun these_funcs thy const = +fun these_eqns thy const = let - fun drop_refl thy = filter_out (is_equal o Term.fast_term_ord o Logic.dest_equals - o ObjectLogic.drop_judgment thy o Thm.plain_prop_of o fst); + val drop_refl = filter_out + (is_equal o Term.fast_term_ord o Logic.dest_equals o Thm.plain_prop_of o fst); in - get_funcs thy const + get_eqns thy const |> preprocess thy - |> drop_refl thy + |> drop_refl end; fun default_typ thy c = case default_typ_proto thy c of SOME ty => Code_Unit.typscheme thy (c, ty) - | NONE => (case get_funcs thy c - of (thm, _) :: _ => snd (Code_Unit.head_func (AxClass.unoverload thy thm)) + | NONE => (case get_eqns thy c + of (thm, _) :: _ => snd (Code_Unit.head_eqn (AxClass.unoverload thy thm)) | [] => Code_Unit.typscheme thy (c, Sign.the_const_type thy c)); end; (*local*) diff -r 10ea34297962 -r 8437fb395294 src/Pure/Isar/code_unit.ML --- a/src/Pure/Isar/code_unit.ML Fri Sep 26 09:09:51 2008 +0200 +++ b/src/Pure/Isar/code_unit.ML Fri Sep 26 09:09:52 2008 +0200 @@ -9,9 +9,9 @@ sig (*generic non-sense*) val bad_thm: string -> 'a - val error_thm: (thm -> thm) -> thm -> thm - val warning_thm: (thm -> thm) -> thm -> thm option - val try_thm: (thm -> thm) -> thm -> thm option + val error_thm: ('a -> 'b) -> 'a -> 'b + val warning_thm: ('a -> 'b) -> 'a -> 'b option + val try_thm: ('a -> 'b) -> 'a -> 'b option (*typ instantiations*) val typscheme: theory -> string * typ -> (string * sort) list * typ @@ -38,10 +38,11 @@ (*defining equations*) val assert_rew: thm -> thm val mk_rew: thm -> thm - val mk_func: bool -> thm -> thm - val head_func: thm -> string * ((string * sort) list * typ) + val add_linear: thm -> thm * bool + val mk_eqn: thm -> thm * bool + val head_eqn: thm -> string * ((string * sort) list * typ) val expand_eta: int -> thm -> thm - val rewrite_func: simpset -> thm -> thm + val rewrite_eqn: simpset -> thm -> thm val rewrite_head: thm list -> thm -> thm val norm_args: thm list -> thm list val norm_varnames: (string -> string) -> (string -> string) -> thm list -> thm list @@ -135,7 +136,7 @@ |> Conv.fconv_rule Drule.beta_eta_conversion end; -fun func_conv conv = +fun eqn_conv conv = let fun lhs_conv ct = if can Thm.dest_comb ct then (Conv.combination_conv lhs_conv conv) ct @@ -149,7 +150,7 @@ else conv ct; in Conv.fun_conv (Conv.arg_conv lhs_conv) end; -val rewrite_func = Conv.fconv_rule o func_conv o Simplifier.rewrite; +val rewrite_eqn = Conv.fconv_rule o eqn_conv o Simplifier.rewrite; val rewrite_head = Conv.fconv_rule o head_conv o MetaSimplifier.rewrite false; fun norm_args thms = @@ -361,21 +362,19 @@ (* defining equations *) -fun assert_func linear thm = +fun add_linear thm = + let + val (_, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm; + val linear = not (has_duplicates (op =) + ((fold o fold_aterms) (fn Var (v, _) => cons v | _ => I) args [])) + in (thm, linear) end; + +fun assert_eqn thm = let val thy = Thm.theory_of_thm thm; - val (head, args) = (strip_comb o fst o Logic.dest_equals - o ObjectLogic.drop_judgment thy o Thm.plain_prop_of) thm; + val (head, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm; val _ = case head of Const _ => () | _ => bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm); - val _ = - if linear andalso has_duplicates (op =) - ((fold o fold_aterms) (fn Var (v, _) => cons v - | _ => I - ) args []) - then bad_thm ("Duplicated variables on left hand side of equation\n" - ^ Display.string_of_thm thm) - else () fun check _ (Abs _) = bad_thm ("Abstraction on left hand side of equation\n" ^ Display.string_of_thm thm) @@ -390,11 +389,13 @@ ^ Display.string_of_thm thm) else (); val _ = map (check 0) args; - in thm end; + val linear = not (has_duplicates (op =) + ((fold o fold_aterms) (fn Var (v, _) => cons v | _ => I ) args [])) + in add_linear thm end; -fun mk_func linear = assert_func linear o mk_rew; +val mk_eqn = assert_eqn o mk_rew; -fun head_func thm = +fun head_eqn thm = let val thy = Thm.theory_of_thm thm; val Const (c, ty) = (fst o strip_comb o fst o Logic.dest_equals