# HG changeset patch # User haftmann # Date 1195848575 -3600 # Node ID dad0291cb76aba4e758ff0eb53902ba88e01cae1 # Parent 001dfba51869e5e1ec4e19db3a08e4e4370e0ca4 rudimentary instantiation target diff -r 001dfba51869 -r dad0291cb76a src/Pure/Isar/ROOT.ML --- a/src/Pure/Isar/ROOT.ML Fri Nov 23 21:09:34 2007 +0100 +++ b/src/Pure/Isar/ROOT.ML Fri Nov 23 21:09:35 2007 +0100 @@ -44,6 +44,9 @@ (*derived theory and proof elements*) use "calculation.ML"; use "obtain.ML"; + +(*local theories and target primitives*) +use "local_theory.ML"; use "locale.ML"; use "class.ML"; @@ -52,12 +55,11 @@ use "code.ML"; (*local theories and specifications*) -use "local_theory.ML"; use "theory_target.ML"; use "subclass.ML"; -use "instance.ML"; use "spec_parse.ML"; use "specification.ML"; +use "instance.ML"; use "constdefs.ML"; (*toplevel environment*) diff -r 001dfba51869 -r dad0291cb76a src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Fri Nov 23 21:09:34 2007 +0100 +++ b/src/Pure/Isar/class.ML Fri Nov 23 21:09:35 2007 +0100 @@ -7,11 +7,7 @@ signature CLASS = sig - val axclass_cmd: bstring * xstring list - -> ((bstring * Attrib.src list) * string list) list - -> theory -> class * theory - val classrel_cmd: xstring * xstring -> theory -> Proof.state - + (*classes*) val class: bstring -> class list -> Element.context_i Locale.element list -> string list -> theory -> string * Proof.context val class_cmd: bstring -> xstring list -> Element.context Locale.element list @@ -30,8 +26,29 @@ -> theory -> theory val print_classes: theory -> unit val class_prefix: string -> string - val uncheck: bool ref + (*instances*) + val declare_overloaded: string * typ * mixfix -> theory -> term * theory + val define_overloaded: string -> string * term -> theory -> thm * theory + val unoverload: theory -> conv + val overload: theory -> conv + val unoverload_const: theory -> string * typ -> string + val inst_const: theory -> string * string -> string + val param_const: theory -> string -> (string * string) option + val instantiation: arity list -> theory -> local_theory + val proof_instantiation: (local_theory -> local_theory) -> local_theory -> Proof.state + val prove_instantiation: (Proof.context -> tactic) -> local_theory -> local_theory + val conclude_instantiation: local_theory -> local_theory + val end_instantiation: local_theory -> Proof.context + val instantiation_const: Proof.context -> string -> string option + + (*old axclass layer*) + val axclass_cmd: bstring * xstring list + -> ((bstring * Attrib.src list) * string list) list + -> theory -> class * theory + val classrel_cmd: xstring * xstring -> theory -> Proof.state + + (*old instance layer*) val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state val instance: arity list -> ((bstring * Attrib.src list) * term) list -> (thm list -> theory -> theory) @@ -43,11 +60,6 @@ val prove_instance: tactic -> arity list -> ((bstring * Attrib.src list) * term) list -> theory -> thm list * theory - val unoverload: theory -> conv - val overload: theory -> conv - val unoverload_const: theory -> string * typ -> string - val inst_const: theory -> string * string -> string - val param_const: theory -> string -> (string * string) option end; structure Class : CLASS = @@ -141,7 +153,9 @@ end; (*local*) -(** explicit constants for overloaded definitions **) +(** basic overloading **) + +(* bookkeeping *) structure InstData = TheoryDataFun ( @@ -156,8 +170,18 @@ Symtab.merge (K true) (tabb1, tabb2)); ); +val inst_tyco = Option.map fst o try (dest_Type o the_single) oo Sign.const_typargs; + +fun inst thy (c, tyco) = + (the o Symtab.lookup ((the o Symtab.lookup (fst (InstData.get thy))) c)) tyco; + +val inst_const = fst oo inst; + fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst) - (InstData.get thy) []; + (InstData.get thy) []; + +val param_const = Symtab.lookup o snd o InstData.get; + fun add_inst (c, tyco) inst = (InstData.map o apfst o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst)) #> (InstData.map o apsnd) (Symtab.update_new (fst inst, (c, tyco))); @@ -165,19 +189,65 @@ fun unoverload thy = MetaSimplifier.rewrite true (inst_thms thy); fun overload thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy)); -fun inst_const thy (c, tyco) = - (fst o the o Symtab.lookup ((the o Symtab.lookup (fst (InstData.get thy))) c)) tyco; fun unoverload_const thy (c_ty as (c, _)) = case AxClass.class_of_param thy c - of SOME class => (case Sign.const_typargs thy c_ty - of [Type (tyco, _)] => (case Symtab.lookup - ((the o Symtab.lookup (fst (InstData.get thy))) c) tyco + of SOME class => (case inst_tyco thy c_ty + of SOME tyco => (case try (inst thy) (c, tyco) of SOME (c, _) => c | NONE => c) - | [_] => c) + | NONE => c) | NONE => c; -val param_const = Symtab.lookup o snd o InstData.get; + +(* declaration and definition of instances of overloaded constants *) + +fun primitive_note kind (name, thm) = + PureThy.note_thmss_i kind [((name, []), [([thm], [])])] + #>> (fn [(_, [thm])] => thm); + +fun declare_overloaded (c, ty, mx) thy = + let + val SOME class = AxClass.class_of_param thy c; + val SOME tyco = inst_tyco thy (c, ty); + val name_inst = NameSpace.base class ^ "_" ^ NameSpace.base tyco ^ "_inst"; + val c' = NameSpace.base c; + val ty' = Type.strip_sorts ty; + in + thy + |> Sign.sticky_prefix name_inst + |> Sign.no_base_names + |> Sign.notation true Syntax.mode_default [(Const (c, ty), mx)] + |> Sign.declare_const [] (c', ty', NoSyn) + |-> (fn const' as Const (c'', _) => Thm.add_def true + (Thm.def_name c', Logic.mk_equals (Const (c, ty'), const')) + #>> Thm.varifyT + #-> (fn thm => add_inst (c, tyco) (c'', thm) + #> primitive_note Thm.internalK (c', thm) + #> snd + #> Sign.restore_naming thy + #> pair (Const (c, ty)))) + end; + +fun define_overloaded name (c, t) thy = + let + val ty = Term.fastype_of t; + val SOME tyco = inst_tyco thy (c, ty); + val (c', eq) = inst thy (c, tyco); + val [Type (_, tys)] = Sign.const_typargs thy (c, ty); + val eq' = eq + |> Drule.instantiate' (map (SOME o Thm.ctyp_of thy) tys) []; + (*FIXME proper recover_sort mechanism*) + val prop = Logic.mk_equals (Const (c', ty), t); + val name' = if name = "" then + Thm.def_name (NameSpace.base c ^ "_" ^ NameSpace.base tyco) else name; + in + thy + |> Thm.add_def false (name', prop) + |>> (fn thm => Thm.transitive eq' thm) + end; + + +(* legacy *) fun add_inst_def (class, tyco) (c, ty) thy = let @@ -206,15 +276,10 @@ let val ((lhs as Const (c, ty), args), rhs) = (apfst Term.strip_comb o Logic.dest_equals) prop; - fun (*add_inst' def ([], (Const (c_inst, ty))) = - if forall (fn TFree _ => true | _ => false) (Sign.const_typargs thy (c_inst, ty)) - then add_inst (c, tyco) (c_inst, def) - else add_inst_def (class, tyco) (c, ty) - |*) add_inst' _ t = add_inst_def (class, tyco) (c, ty); in thy |> PureThy.add_defs_i true [((name, prop), map (Attrib.attribute_i thy) atts)] - |-> (fn [def] => add_inst' def (args, rhs) #> pair def) + |-> (fn [def] => add_inst_def (class, tyco) (c, ty) #> pair def) end; @@ -690,14 +755,11 @@ |> SOME end; -val uncheck = ref true; - fun sort_term_uncheck ts ctxt = let val thy = ProofContext.theory_of ctxt; val unchecks = (#unchecks o ClassSyntax.get) ctxt; - val ts' = if ! uncheck - then map (Pattern.rewrite_term thy unchecks []) ts else ts; + val ts' = map (Pattern.rewrite_term thy unchecks []) ts; in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end; fun init_ctxt sups base_sort ctxt = @@ -896,4 +958,174 @@ |> Sign.restore_naming thy end; + +(** instantiation target **) + +(* bookkeeping *) + +datatype instantiation = Instantiation of { + arities: arity list, + params: ((string * string) * (string * typ)) list +} + +structure Instantiation = ProofDataFun +( + type T = instantiation + fun init _ = Instantiation { arities = [], params = [] }; +); + +fun mk_instantiation (arities, params) = Instantiation { + arities = arities, params = params + }; +fun map_instantiation f (Instantiation { arities, params }) = + mk_instantiation (f (arities, params)); + +fun the_instantiation ctxt = case Instantiation.get ctxt + of Instantiation { arities = [], ... } => error "No instantiation target" + | Instantiation data => data; + +fun init_instantiation arities ctxt = + let + val thy = ProofContext.theory_of ctxt; + val _ = if null arities then error "At least one arity must be given" else (); + val _ = case (duplicates (op =) o map #1) arities + of [] => () + | dupl_tycos => error ("Type constructors occur more than once in arities: " + ^ commas_quote dupl_tycos); + val ty_insts = map (fn (tyco, sorts, _) => + (tyco, Type (tyco, map TFree (Name.names Name.context Name.aT sorts)))) + arities; + val ty_inst = the o AList.lookup (op =) ty_insts; + fun type_name "*" = "prod" + | type_name "+" = "sum" + | type_name s = NameSpace.base s; (*FIXME*) + fun get_param tyco sorts (param, (c, ty)) = + ((unoverload_const thy (c, ty), tyco), + (param ^ "_" ^ type_name tyco, + map_atyps (K (ty_inst tyco)) ty)); + fun get_params (tyco, sorts, sort) = + map (get_param tyco sorts) (these_params thy sort) + val params = maps get_params arities; + in + ctxt + |> Instantiation.put (mk_instantiation (arities, params)) + |> fold (Variable.declare_term o Logic.mk_type o snd) ty_insts + |> fold (Variable.declare_term o Free o snd) params + end; + +val instantiation_params = #params o the_instantiation; + +fun instantiation_const ctxt v = instantiation_params ctxt + |> find_first (fn (_, (v', _)) => v = v') + |> Option.map (fst o fst); + + +(* syntax *) + +fun inst_term_check ts ctxt = + let + val params = instantiation_params ctxt; + val tsig = ProofContext.tsig_of ctxt; + val thy = ProofContext.theory_of ctxt; + + fun check_improve (Const (c, ty)) = (case inst_tyco thy (c, ty) + of SOME tyco => (case AList.lookup (op =) params (c, tyco) + of SOME (_, ty') => Type.typ_match tsig (ty, ty') + | NONE => I) + | NONE => I) + | check_improve _ = I; + val improvement = (fold o fold_aterms) check_improve ts Vartab.empty; + val ts' = (map o map_types) (Envir.typ_subst_TVars improvement) ts; + val ts'' = (map o map_aterms) (fn t as Const (c, ty) => (case inst_tyco thy (c, ty) + of SOME tyco => (case AList.lookup (op =) params (c, tyco) + of SOME v_ty => Free v_ty + | NONE => t) + | NONE => t) + | t => t) ts'; + in if eq_list (op aconv) (ts, ts'') then NONE else SOME (ts'', ctxt) end; + +fun inst_term_uncheck ts ctxt = + let + val params = instantiation_params ctxt; + val ts' = (map o map_aterms) (fn t as Free (v, ty) => + (case get_first (fn ((c, _), (v', _)) => if v = v' then SOME c else NONE) params + of SOME c => Const (c, ty) + | NONE => t) + | t => t) ts; + in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end; + + +(* target *) + +fun instantiation arities = + ProofContext.init + #> init_instantiation arities + #> fold ProofContext.add_arity arities + #> Context.proof_map ( + Syntax.add_term_check 0 "instance" inst_term_check + #> Syntax.add_term_uncheck 0 "instance" inst_term_uncheck); + +fun gen_proof_instantiation do_proof after_qed lthy = + let + (*FIXME should work on fresh context but continue local theory afterwards*) + val ctxt = LocalTheory.target_of lthy; + val arities = (#arities o the_instantiation) ctxt; + val arities_proof = maps + (Logic.mk_arities o Sign.cert_arity (ProofContext.theory_of ctxt)) arities; + fun after_qed' results = + LocalTheory.theory (fold (AxClass.add_arity o Thm.varifyT) results) + #> after_qed; + in + lthy + |> do_proof after_qed' arities_proof + end; + +val proof_instantiation = gen_proof_instantiation (fn after_qed => fn ts => + Proof.theorem_i NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts)); + +fun prove_instantiation tac = gen_proof_instantiation (fn after_qed => + fn ts => fn lthy => after_qed (Goal.prove_multi lthy [] [] ts + (fn {context, ...} => tac context)) lthy) I; + +fun conclude_instantiation lthy = + let + val arities = (#arities o the_instantiation) lthy; + val thy = ProofContext.theory_of lthy; + (*val _ = map (fn (tyco, sorts, sort) => + if Sign.of_sort thy + (Type (tyco, map TFree (Name.names Name.context Name.aT sorts)), sort) + then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco))) + arities; FIXME activate when old instance command is gone*) + val params_of = maps (these o try (#params o AxClass.get_info thy)) + o Sign.complete_sort thy; + val missing_params = arities + |> maps (fn (tyco, _, sort) => params_of sort |> map (rpair tyco)) + |> filter_out (can (inst thy) o apfst fst); + fun declare_missing ((c, ty), tyco) thy = + let + val SOME class = AxClass.class_of_param thy c; + val name_inst = NameSpace.base class ^ "_" ^ NameSpace.base tyco ^ "_inst"; + val vs = Name.names Name.context Name.aT (replicate (Sign.arity_number thy tyco) []); + val ty' = map_atyps (fn _ => Type (tyco, map TFree vs)) ty; + val c' = NameSpace.base c; + in + thy + |> Sign.sticky_prefix name_inst + |> Sign.no_base_names + |> Sign.declare_const [] (c', ty', NoSyn) + |-> (fn const' as Const (c'', _) => Thm.add_def true + (Thm.def_name c', Logic.mk_equals (const', Const (c, ty'))) + #>> Thm.varifyT + #-> (fn thm => add_inst (c, tyco) (c'', Thm.symmetric thm) + #> primitive_note Thm.internalK (c', thm) + #> snd + #> Sign.restore_naming thy)) + end; + in + lthy + |> LocalTheory.theory (fold declare_missing missing_params) + end; + +val end_instantiation = conclude_instantiation #> LocalTheory.target_of; + end; diff -r 001dfba51869 -r dad0291cb76a src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Fri Nov 23 21:09:34 2007 +0100 +++ b/src/Pure/Isar/code.ML Fri Nov 23 21:09:35 2007 +0100 @@ -24,6 +24,7 @@ val del_post: thm -> theory -> theory val add_datatype: (string * typ) list -> theory -> theory val add_datatype_cmd: string list -> theory -> theory + val type_interpretation: (string * string list -> theory -> theory) -> theory -> theory val add_case: thm -> theory -> theory val add_undefined: string -> theory -> theory @@ -537,18 +538,15 @@ fun aggregate f [] = NONE | aggregate f (x::xs) = SOME (aggr_neutr f x xs); -fun inter_sorts thy = - let - val algebra = Sign.classes_of thy; - val inters = curry (Sorts.inter_sort algebra); - in aggregate (map2 inters) end; +fun inter_sorts algebra = + aggregate (map2 (curry (Sorts.inter_sort algebra))); fun specific_constraints thy (class, tyco) = 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 - |> map (fn c => Class.inst_const thy (c, tyco)) + |> map_filter (fn c => try (Class.inst_const thy) (c, tyco)) |> map (Symtab.lookup ((the_funcs o the_exec) thy)) |> (map o Option.map) (Susp.force o fst o snd) |> maps these @@ -558,37 +556,53 @@ val sorts = map (sorts_of o Sign.const_typargs thy o CodeUnit.head_func) funcs; in sorts end; -fun weakest_constraints thy (class, tyco) = +fun weakest_constraints thy algebra (class, tyco) = let - val all_superclasses = Sign.complete_sort thy [class]; - in case inter_sorts thy (maps (fn class => specific_constraints thy (class, tyco)) all_superclasses) + val all_superclasses = Sorts.complete_sort algebra [class]; + in case inter_sorts algebra (maps (fn class => specific_constraints thy (class, tyco)) all_superclasses) of SOME sorts => sorts - | NONE => Sign.arity_sorts thy tyco [class] + | NONE => Sorts.mg_domain algebra tyco [class] end; -fun strongest_constraints thy (class, tyco) = +fun strongest_constraints thy algebra (class, tyco) = let - val algebra = Sign.classes_of thy; val all_subclasses = class :: Graph.all_preds ((#classes o Sorts.rep_algebra) algebra) [class]; val inst_subclasses = filter (can (Sorts.mg_domain algebra tyco) o single) all_subclasses; - in case inter_sorts thy (maps (fn class => specific_constraints thy (class, tyco)) inst_subclasses) + in case inter_sorts algebra (maps (fn class => specific_constraints thy (class, tyco)) inst_subclasses) of SOME sorts => sorts | NONE => replicate - (Sign.arity_number thy tyco) (Sign.minimize_sort thy (Sign.all_classes thy)) + (Sign.arity_number thy tyco) (Sorts.minimize_sort algebra (Sorts.all_classes algebra)) + end; + +fun get_algebra thy (class, tyco) = + let + val base_algebra = Sign.classes_of thy; + in if can (Sorts.mg_domain base_algebra tyco) [class] + then base_algebra + else let + val superclasses = Sorts.super_classes base_algebra class; + val sorts = inter_sorts base_algebra + (map_filter (fn class => try (Sorts.mg_domain base_algebra tyco) [class]) superclasses) + |> the_default (replicate (Sign.arity_number thy tyco) []) + in + base_algebra + |> Sorts.add_arities (Sign.pp thy) (tyco, [(class, sorts)]) + end end; fun gen_classparam_typ constr thy class (c, tyco) = let + val algebra = get_algebra thy (class, tyco); val cs = these (try (#params o AxClass.get_info thy) class); - val ty = (the o AList.lookup (op =) cs) c; + val SOME ty = AList.lookup (op =) cs c; val sort_args = Name.names (Name.declare Name.aT Name.context) Name.aT - (constr thy (class, tyco)); + (constr thy algebra (class, tyco)); val ty_inst = Type (tyco, map TFree sort_args); in Logic.varifyT (map_type_tfree (K ty_inst) ty) end; fun retrieve_algebra thy operational = Sorts.subalgebra (Sign.pp thy) operational - (weakest_constraints thy) + (weakest_constraints thy (Sign.classes_of thy)) (Sign.classes_of thy); in @@ -763,18 +777,22 @@ val add_default_func_attr = Attrib.internal (fn _ => Thm.declaration_attribute (fn thm => Context.mapping (add_default_func thm) I)); +structure TypeInterpretation = InterpretationFun(type T = string * string list val eq = op =); +val type_interpretation = TypeInterpretation.interpretation; + fun add_datatype raw_cs thy = let val cs = map (fn c_ty as (_, ty) => (Class.unoverload_const thy c_ty, ty)) raw_cs; val (tyco, vs_cos) = CodeUnit.constrset_of_consts thy cs; - val purge_cs = map fst (snd vs_cos); - val purge_cs' = case Symtab.lookup ((the_dtyps o the_exec) thy) tyco - of SOME (vs, cos) => if null cos then NONE else SOME (purge_cs @ map fst cos) + val cs' = map fst (snd vs_cos); + val purge_cs = case Symtab.lookup ((the_dtyps o the_exec) thy) tyco + of SOME (vs, cos) => if null cos then NONE else SOME (cs' @ map fst cos) | NONE => NONE; in thy - |> map_exec_purge purge_cs' (map_dtyps (Symtab.update (tyco, vs_cos)) + |> map_exec_purge purge_cs (map_dtyps (Symtab.update (tyco, vs_cos)) #> map_funcs (fold (Symtab.delete_safe o fst) cs)) + |> TypeInterpretation.data (tyco, cs') end; fun add_datatype_cmd raw_cs thy = @@ -837,7 +855,8 @@ add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del) || Scan.succeed (mk_attribute add)) in - add_del_attribute ("func", (add_func, del_func)) + TypeInterpretation.init + #> add_del_attribute ("func", (add_func, del_func)) #> add_del_attribute ("inline", (add_inline, del_inline)) #> add_del_attribute ("post", (add_post, del_post)) end); diff -r 001dfba51869 -r dad0291cb76a src/Pure/Isar/instance.ML --- a/src/Pure/Isar/instance.ML Fri Nov 23 21:09:34 2007 +0100 +++ b/src/Pure/Isar/instance.ML Fri Nov 23 21:09:35 2007 +0100 @@ -2,79 +2,74 @@ ID: $Id$ Author: Florian Haftmann, TU Muenchen -User-level instantiation interface for classes. -FIXME not operative for the moment +A primitive instance command, based on instantiation target. *) signature INSTANCE = sig - val begin_instantiation: arity list -> theory -> local_theory - val begin_instantiation_cmd: (xstring * string list * string) list + val instantiate: arity list -> (local_theory -> local_theory) + -> (Proof.context -> tactic) -> theory -> theory + val instance: arity list -> ((bstring * Attrib.src list) * term) list + -> (thm list -> theory -> theory) + -> theory -> Proof.state + val prove_instance: tactic -> arity list -> ((bstring * Attrib.src list) * term) list + -> theory -> thm list * theory + + val instantiation_cmd: (xstring * sort * xstring) list -> theory -> local_theory - val proof_instantiation: local_theory -> Proof.state + val instance_cmd: (xstring * sort * xstring) list -> ((bstring * Attrib.src list) * xstring) list + -> (thm list -> theory -> theory) + -> theory -> Proof.state end; structure Instance : INSTANCE = struct -structure Instantiation = ProofDataFun -( - type T = ((string * (string * sort) list) * sort) list * ((string * typ) * string) list; - fun init _ = ([], []); -); +fun instantiation_cmd raw_arities thy = + TheoryTarget.instantiation (map (Sign.read_arity thy) raw_arities) thy; + +fun instantiate arities f tac = + TheoryTarget.instantiation arities + #> f + #> Class.prove_instantiation tac + #> LocalTheory.exit + #> ProofContext.theory_of; -local - -fun gen_begin_instantiation prep_arity raw_arities thy = +fun gen_instance prep_arity prep_attr prep_term do_proof raw_arities defs after_qed thy = let - fun prep_arity' raw_arity names = + fun export_defs ctxt = + let + val ctxt_thy = ProofContext.init (ProofContext.theory_of ctxt); + in + map (snd o snd) + #> map (Assumption.export false ctxt ctxt_thy) + #> Variable.export ctxt ctxt_thy + end; + fun mk_def ctxt ((name, raw_attr), raw_t) = let - val arity as (tyco, sorts, sort) = prep_arity thy raw_arity; - val vs = Name.invents names Name.aT (length sorts); - val names' = fold Name.declare vs names; - in (((tyco, vs ~~ sorts), sort), names') end; - val (arities, _) = fold_map prep_arity' raw_arities Name.context; - fun get_param tyco ty_subst (param, (c, ty)) = - ((param ^ "_" ^ NameSpace.base tyco, map_atyps (K ty_subst) ty), - Class.unoverload_const thy (c, ty)); - fun get_params ((tyco, vs), sort) = - Class.these_params thy sort - |> map (get_param tyco (Type (tyco, map TFree vs))); - val params = maps get_params arities; - val ctxt = - ProofContext.init thy - |> Instantiation.put (arities, params); - val thy_target = TheoryTarget.begin "" ctxt; - val operations = { - pretty = LocalTheory.pretty, - axioms = LocalTheory.axioms, - abbrev = LocalTheory.abbrev, - define = LocalTheory.define, - notes = LocalTheory.notes, - type_syntax = LocalTheory.type_syntax, - term_syntax = LocalTheory.term_syntax, - declaration = LocalTheory.pretty, - reinit = LocalTheory.reinit, - exit = LocalTheory.exit - }; - in TheoryTarget.begin "" ctxt end; + val attr = map (prep_attr thy) raw_attr; + val t = prep_term ctxt raw_t; + in (NONE, ((name, attr), t)) end; + val arities = map (prep_arity thy) raw_arities; + in + thy + |> TheoryTarget.instantiation arities + |> `(fn ctxt => map (mk_def ctxt) defs) + |-> (fn defs => fold_map Specification.definition defs) + |-> (fn defs => `(fn ctxt => export_defs ctxt defs)) + ||> LocalTheory.exit + ||> ProofContext.theory_of + ||> TheoryTarget.instantiation arities + |-> (fn defs => do_proof defs (LocalTheory.theory (after_qed defs))) + end; -in - -val begin_instantiation = gen_begin_instantiation Sign.cert_arity; -val begin_instantiation_cmd = gen_begin_instantiation Sign.read_arity; +val instance = gen_instance Sign.cert_arity (K I) (K I) + (fn _ => fn after_qed => Class.proof_instantiation (after_qed #> Class.conclude_instantiation)); +val instance_cmd = gen_instance Sign.read_arity Attrib.intern_src + (fn ctxt => Syntax.parse_prop ctxt #> Syntax.check_prop ctxt) + (fn _ => fn after_qed => Class.proof_instantiation (after_qed #> Class.conclude_instantiation)); +fun prove_instance tac arities defs = gen_instance Sign.cert_arity (K I) (K I) + (fn defs => fn after_qed => Class.prove_instantiation (K tac) + #> after_qed #> Class.conclude_instantiation #> ProofContext.theory_of #> pair defs) arities defs (K I); end; - -fun gen_proof_instantiation do_proof after_qed lthy = - let - val ctxt = LocalTheory.target_of lthy; - val arities = case Instantiation.get ctxt - of ([], _) => error "no instantiation target" - | (arities, _) => map (fn ((tyco, vs), sort) => (tyco, map snd vs, sort)) arities; - val thy = ProofContext.theory_of ctxt; - in (do_proof after_qed arities) thy end; - -val proof_instantiation = gen_proof_instantiation Class.instance_arity I; - -end; diff -r 001dfba51869 -r dad0291cb76a src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Fri Nov 23 21:09:34 2007 +0100 +++ b/src/Pure/Isar/isar_syn.ML Fri Nov 23 21:09:35 2007 +0100 @@ -113,7 +113,7 @@ val _ = OuterSyntax.command "typedecl" "type declaration" K.thy_decl (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) => - Toplevel.theory (Sign.add_typedecls [(a, args, mx)]))); + Toplevel.theory (Typedecl.add (a, args, mx) #> snd))); val _ = OuterSyntax.command "types" "declare type abbreviations" K.thy_decl @@ -448,18 +448,18 @@ OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal ((P.xname -- ((P.$$$ "\\" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd || P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop) - >> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func (* FIXME ? *)))) + >> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func))) >> (Toplevel.print oo Toplevel.theory_to_proof)); val _ = OuterSyntax.command "instantiation" "prove type arity" K.thy_decl - (P.and_list1 P.arity -- P.opt_begin - >> (fn (arities, begin) => (begin ? Toplevel.print) o - Toplevel.begin_local_theory begin (Instance.begin_instantiation_cmd arities))); + (P.and_list1 P.arity --| P.begin + >> (fn arities => Toplevel.print o + Toplevel.begin_local_theory true (Instance.instantiation_cmd arities))); val _ = (* FIXME incorporate into "instance" *) OuterSyntax.command "instance_proof" "prove type arity relation" K.thy_goal - (Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE Instance.proof_instantiation)); + (Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.proof_instantiation I))); (* code generation *) diff -r 001dfba51869 -r dad0291cb76a src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Fri Nov 23 21:09:34 2007 +0100 +++ b/src/Pure/Isar/theory_target.ML Fri Nov 23 21:09:35 2007 +0100 @@ -2,15 +2,17 @@ ID: $Id$ Author: Makarius -Common theory/locale/class targets. +Common theory/locale/class/instantiation targets. *) signature THEORY_TARGET = sig - val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} + val peek: local_theory -> {target: string, is_locale: bool, + is_class: bool, instantiation: arity list} val init: string option -> theory -> local_theory val begin: string -> Proof.context -> local_theory val context: xstring -> theory -> local_theory + val instantiation: arity list -> theory -> local_theory end; structure TheoryTarget: THEORY_TARGET = @@ -18,12 +20,14 @@ (* context data *) -datatype target = Target of {target: string, is_locale: bool, is_class: bool}; +datatype target = Target of {target: string, is_locale: bool, + is_class: bool, instantiation: arity list}; -fun make_target target is_locale is_class = - Target {target = target, is_locale = is_locale, is_class = is_class}; +fun make_target target is_locale is_class instantiation = + Target {target = target, is_locale = is_locale, + is_class = is_class, instantiation = instantiation}; -val global_target = make_target "" false false; +val global_target = make_target "" false false []; structure Data = ProofDataFun ( @@ -36,7 +40,7 @@ (* pretty *) -fun pretty (Target {target, is_locale, is_class}) ctxt = +fun pretty (Target {target, is_locale, is_class, instantiation}) ctxt = let val thy = ProofContext.theory_of ctxt; val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target; @@ -186,13 +190,18 @@ Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)])))) end; -fun declare_const (ta as Target {target, is_locale, is_class}) depends ((c, T), mx) lthy = +fun declare_const (ta as Target {target, is_locale, is_class, instantiation}) depends ((c, T), mx) lthy = let val pos = ContextPosition.properties_of lthy; val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy))); val U = map #2 xs ---> T; val (mx1, mx2, mx3) = fork_mixfix ta mx; - val (const, lthy') = lthy |> LocalTheory.theory_result (Sign.declare_const pos (c, U, mx3)); + val declare_const = if null instantiation + then Sign.declare_const pos (c, U, mx3) + else case Class.instantiation_const lthy c + of SOME c' => Class.declare_overloaded (c', U, mx3) + | NONE => Sign.declare_const pos (c, U, mx3); + val (const, lthy') = lthy |> LocalTheory.theory_result declare_const; val t = Term.list_comb (const, map Free xs); in lthy' @@ -204,7 +213,7 @@ (* abbrev *) -fun abbrev (ta as Target {target, is_locale, is_class}) prmode ((c, mx), t) lthy = +fun abbrev (ta as Target {target, is_locale, is_class, instantiation}) prmode ((c, mx), t) lthy = let val pos = ContextPosition.properties_of lthy; val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy); @@ -236,7 +245,7 @@ (* define *) -fun define (ta as Target {target, is_locale, is_class}) +fun define (ta as Target {target, is_locale, is_class, instantiation}) kind ((c, mx), ((name, atts), rhs)) lthy = let val thy = ProofContext.theory_of lthy; @@ -253,12 +262,18 @@ val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def); (*def*) + val is_instantiation = not (null instantiation) + andalso is_some (Class.instantiation_const lthy c); + val define_const = if not is_instantiation + then (fn name => fn eq => Thm.add_def false (name, Logic.mk_equals eq)) + else (fn name => fn (Const (c, _), rhs) => Class.define_overloaded name (c, rhs)); val (global_def, lthy3) = lthy2 - |> LocalTheory.theory_result (Thm.add_def false (name', Logic.mk_equals (lhs', rhs'))); - val def = LocalDefs.trans_terms lthy3 + |> LocalTheory.theory_result (define_const name' (lhs', rhs')); + val def = if not is_instantiation then LocalDefs.trans_terms lthy3 [(*c == global.c xs*) local_def, (*global.c xs == rhs'*) global_def, - (*rhs' == rhs*) Thm.symmetric rhs_conv]; + (*rhs' == rhs*) Thm.symmetric rhs_conv] + else Thm.transitive local_def global_def; (*note*) val ([(res_name, [res])], lthy4) = lthy3 @@ -298,14 +313,18 @@ local fun init_target _ NONE = global_target - | init_target thy (SOME target) = make_target target true (Class.is_class thy target); + | init_target thy (SOME target) = make_target target true (Class.is_class thy target) []; + +fun init_instantiaton arities = make_target "" false false arities -fun init_ctxt (Target {target, is_locale, is_class}) = - if not is_locale then ProofContext.init - else if not is_class then Locale.init target - else Class.init target; +fun init_ctxt (Target {target, is_locale, is_class, instantiation}) = + if null instantiation then + if not is_locale then ProofContext.init + else if not is_class then Locale.init target + else Class.init target + else Class.instantiation instantiation; -fun init_lthy (ta as Target {target, ...}) = +fun init_lthy (ta as Target {target, instantiation, ...}) = Data.put ta #> LocalTheory.init (NameSpace.base target) {pretty = pretty ta, @@ -317,7 +336,7 @@ term_syntax = term_syntax ta, declaration = declaration ta, reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy), - exit = LocalTheory.target_of} + exit = if null instantiation then LocalTheory.target_of else Class.end_instantiation} and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta; in @@ -328,6 +347,9 @@ fun context "-" thy = init NONE thy | context target thy = init (SOME (Locale.intern thy target)) thy; +fun instantiation raw_arities thy = + init_lthy_ctxt (init_instantiaton (map (Sign.cert_arity thy) raw_arities)) thy; + end; end;