# HG changeset patch # User haftmann # Date 1196860551 -3600 # Node ID 01753a9444335fb7b3f9a69df67f0bafd22cde5c # Parent 4975b7529a14528c0e996880f8caf7f62a595f24 improved diff -r 4975b7529a14 -r 01753a944433 src/HOL/Library/Eval.thy --- a/src/HOL/Library/Eval.thy Wed Dec 05 14:15:48 2007 +0100 +++ b/src/HOL/Library/Eval.thy Wed Dec 05 14:15:51 2007 +0100 @@ -18,47 +18,64 @@ structure TypOf = struct -val class_typ_of = Sign.intern_class @{theory} "typ_of"; - -fun term_typ_of_type ty = +fun mk ty = Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ}) $ Logic.mk_type ty; -fun mk_typ_of_def ty = - let - val lhs = Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ}) - $ Free ("x", Term.itselfT ty) - val rhs = Pure_term.mk_typ (fn v => term_typ_of_type (TFree v)) ty - in Logic.mk_equals (lhs, rhs) end; - -end; +end *} -instance "prop" :: typ_of - "typ_of (T\prop itself) \ STR ''prop'' {\} []" .. - -instance itself :: (typ_of) typ_of - "typ_of (T\'a itself itself) \ STR ''itself'' {\} [typ_of TYPE('a\typ_of)]" .. - -instance set :: (typ_of) typ_of - "typ_of (T\'a set itself) \ STR ''set'' {\} [typ_of TYPE('a\typ_of)]" .. - -instance int :: typ_of - "typ_of (T\int itself) \ STR ''IntDef.int'' {\} []" .. - setup {* let - fun mk arities _ thy = - (maps (fn (tyco, asorts, _) => [(("", []), TypOf.mk_typ_of_def - (Type (tyco, - map TFree (Name.names Name.context "'a" asorts))))]) arities, thy); - fun hook specs = - DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac []) - (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) - [TypOf.class_typ_of] mk ((K o K) (fold Code.add_default_func)) -in DatatypeCodegen.add_codetypes_hook hook end + fun define_typ_of ty lthy = + let + val lhs = Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ}) + $ Free ("T", Term.itselfT ty); + val rhs = Pure_term.mk_typ (fn v => TypOf.mk (TFree v)) ty; + val eq = Class.prep_spec lthy (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))) + in lthy |> Specification.definition (NONE, (("", []), eq)) end; + fun interpretator tyco thy = + let + val sorts = replicate (Sign.arity_number thy tyco) @{sort typ_of}; + val ty = Type (tyco, map TFree (Name.names Name.context "'a" sorts)); + in + thy + |> Instance.instantiate ([tyco], sorts, @{sort typ_of}) + (define_typ_of ty) ((K o K) (Class.intro_classes_tac [])) + end; +in TypedefPackage.interpretation interpretator end *} +instantiation "prop" :: typ_of +begin + +definition + "typ_of (T\prop itself) = STR ''prop'' {\} []" + +instance .. + +end + +instantiation itself :: (typ_of) typ_of +begin + +definition + "typ_of (T\'a itself itself) = STR ''itself'' {\} [typ_of TYPE('a\typ_of)]" + +instance .. + +end + +instantiation set :: (typ_of) typ_of +begin + +definition + "typ_of (T\'a set itself) = STR ''set'' {\} [typ_of TYPE('a\typ_of)]" + +instance .. + +end + subsection {* @{text term_of} class *} @@ -83,7 +100,7 @@ val lhs : term = term_term_of dty $ c; val rhs : term = Pure_term.mk_term (fn (v, ty) => term_term_of ty $ Free (v, ty)) - (Pure_term.mk_typ (fn (v, sort) => TypOf.term_typ_of_type (TFree (v, sort)))) c + (Pure_term.mk_typ (fn (v, sort) => TypOf.mk (TFree (v, sort)))) c in HOLogic.mk_eq (lhs, rhs) end; @@ -101,24 +118,43 @@ PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms)); fun thy_def ((name, atts), t) = PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm)); - fun mk arities css _ thy = + fun prep_dtyp thy vs tyco = + let + val (_, cs) = DatatypePackage.the_datatype_spec thy tyco; + val prep_typ = map_atyps (fn TFree (v, sort) => + TFree (v, (the o AList.lookup (op =) vs) v)); + fun prep_c (c, tys) = list_comb (Const (c, tys ---> Type (tyco, map TFree vs)), + map Free (Name.names Name.context "a" tys)); + in (tyco, map (prep_c o (apsnd o map) prep_typ) cs) end; + fun prep thy tycos = let - val (_, asorts, _) :: _ = arities; - val vs = Name.names Name.context "'a" asorts; + val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of}; + val tyco = hd tycos; + val (vs_proto, _) = DatatypePackage.the_datatype_spec thy tyco; + val all_typs = maps (maps snd o snd o DatatypePackage.the_datatype_spec thy) tycos; + fun add_tycos (Type (tyco, tys)) = insert (op =) tyco #> + fold add_tycos tys + | add_tycos _ = I; + val dep_tycos = [] |> fold add_tycos all_typs |> subtract (op =) tycos; + val sorts = map (inter_sort o snd) vs_proto; + val vs = map fst vs_proto ~~ sorts; + val css = map (prep_dtyp thy vs) tycos; val defs = map (TermOf.mk_terms_of_defs vs) css; val defs' = (map (pair ("", []) o ObjectLogic.ensure_propT thy) o flat) defs; - in - thy - |> PrimrecPackage.gen_primrec thy_note thy_def "" defs' - |> snd + in if forall (fn tyco => can (Sign.arity_sorts thy tyco) @{sort term_of}) dep_tycos + andalso not (tycos = [@{type_name typ}]) + then SOME (sorts, defs') + else NONE end; - fun hook specs = - if null specs orelse (fst o hd) specs = (fst o dest_Type) @{typ typ} then I - else - DatatypeCodegen.prove_codetypes_arities (Class.intro_classes_tac []) - (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) - [TermOf.class_term_of] ((K o K o pair) []) mk -in DatatypeCodegen.add_codetypes_hook hook end + fun interpretator tycos thy = case prep thy tycos + of SOME (sorts, defs) => + thy + |> Instance.instantiate (tycos, sorts, @{sort term_of}) + (pair ()) ((K o K) (Class.intro_classes_tac [])) + |> PrimrecPackage.gen_primrec thy_note thy_def "" defs + |> snd + | NONE => thy; + in DatatypePackage.interpretation interpretator end *} abbreviation diff -r 4975b7529a14 -r 01753a944433 src/HOL/ex/ExecutableContent.thy --- a/src/HOL/ex/ExecutableContent.thy Wed Dec 05 14:15:48 2007 +0100 +++ b/src/HOL/ex/ExecutableContent.thy Wed Dec 05 14:15:51 2007 +0100 @@ -7,7 +7,7 @@ theory ExecutableContent imports Main - (*Eval*) + Eval "~~/src/HOL/ex/Records" AssocList Binomial diff -r 4975b7529a14 -r 01753a944433 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Wed Dec 05 14:15:48 2007 +0100 +++ b/src/Pure/Isar/class.ML Wed Dec 05 14:15:51 2007 +0100 @@ -31,7 +31,8 @@ val print_classes: theory -> unit (*instances*) - val init_instantiation: arity list -> theory -> local_theory + val init_instantiation: string list * sort list * sort -> theory -> local_theory + val prep_spec: local_theory -> term -> term val instantiation_instance: (local_theory -> local_theory) -> local_theory -> Proof.state val prove_instantiation_instance: (Proof.context -> tactic) -> local_theory -> local_theory val conclude_instantiation: local_theory -> local_theory @@ -56,8 +57,8 @@ val classrel_cmd: xstring * xstring -> theory -> Proof.state (*old instance layer*) - val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state - val instance_arity_cmd: (bstring * xstring list * xstring) list -> theory -> Proof.state + val instance_arity: (theory -> theory) -> arity -> theory -> Proof.state + val instance_arity_cmd: bstring * xstring list * xstring -> theory -> Proof.state end; structure Class : CLASS = @@ -134,7 +135,7 @@ thy |> ProofContext.init |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])]) - o maps (mk_prop thy)) insts) + o mk_prop thy) insts) end; in @@ -144,11 +145,9 @@ val instance_arity_cmd = gen_instance (Logic.mk_arities oo Sign.read_arity) AxClass.add_arity I; val classrel = - gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel)) - AxClass.add_classrel I o single; + gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel)) AxClass.add_classrel I; val classrel_cmd = - gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) - AxClass.add_classrel I o single; + gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) AxClass.add_classrel I; end; (*local*) @@ -826,14 +825,14 @@ (* bookkeeping *) datatype instantiation = Instantiation of { - arities: arity list, + arities: string list * sort list * sort, params: ((string * string) * (string * typ)) list } structure Instantiation = ProofDataFun ( type T = instantiation - fun init _ = Instantiation { arities = [], params = [] }; + fun init _ = Instantiation { arities = ([], [], []), params = [] }; ); fun mk_instantiation (arities, params) = @@ -844,7 +843,7 @@ (fn Instantiation { arities, params } => mk_instantiation (f (arities, params))); fun the_instantiation lthy = case get_instantiation lthy - of { arities = [], ... } => error "No instantiation target" + of { arities = ([], [], []), ... } => error "No instantiation target" | data => data; val instantiation_params = #params o get_instantiation; @@ -859,6 +858,19 @@ (* syntax *) +fun subst_param thy params = 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); + +fun prep_spec lthy = + let + val thy = ProofContext.theory_of lthy; + val params = instantiation_params lthy; + in subst_param thy params end; + fun inst_term_check ts lthy = let val params = instantiation_params lthy; @@ -873,12 +885,7 @@ | 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'; + val ts'' = map (subst_param thy params) ts'; in if eq_list (op aconv) (ts, ts'') then NONE else SOME (ts'', lthy) end; fun inst_term_uncheck ts lthy = @@ -908,33 +915,24 @@ explode #> scan_valids #> implode end; -fun init_instantiation arities thy = +fun init_instantiation (tycos, sorts, sort) thy = let - 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 _ = map (map (the_class_data thy) o #3) arities; - 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; + val _ = if null tycos then error "At least one arity must be given" else (); + val _ = map (the_class_data thy) sort; + val vs = map TFree (Name.names Name.context Name.aT sorts); fun type_name "*" = "prod" | type_name "+" = "sum" | type_name s = sanatize_name (NameSpace.base s); (*FIXME*) - fun get_param tyco sorts (param, (c, ty)) = if can (inst thy) (c, tyco) + fun get_param tyco (param, (c, ty)) = if can (inst thy) (c, tyco) then NONE else SOME ((unoverload_const thy (c, ty), tyco), - (param ^ "_" ^ type_name tyco, map_atyps (K (ty_inst tyco)) ty)); - fun get_params (tyco, sorts, sort) = - map_filter (get_param tyco sorts) (these_params thy sort) - val params = maps get_params arities; + (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, vs))) ty)); + val params = map_product get_param tycos (these_params thy sort) |> map_filter I; in thy |> ProofContext.init - |> Instantiation.put (mk_instantiation (arities, params)) - |> fold (Variable.declare_term o Logic.mk_type o snd) ty_insts - |> fold ProofContext.add_arity arities + |> Instantiation.put (mk_instantiation ((tycos, sorts, sort), params)) + |> fold (Variable.declare_term o Logic.mk_type) vs + |> fold (fn tyco => ProofContext.add_arity (tyco, sorts, sort)) tycos |> Context.proof_map ( Syntax.add_term_check 0 "instance" inst_term_check #> Syntax.add_term_uncheck 0 "instance" inst_term_uncheck) @@ -942,8 +940,8 @@ fun gen_instantiation_instance do_proof after_qed lthy = let - val arities = (#arities o the_instantiation) lthy; - val arities_proof = maps Logic.mk_arities arities; + val (tycos, sorts, sort) = (#arities o the_instantiation) lthy; + val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos; fun after_qed' results = LocalTheory.theory (fold (AxClass.add_arity o Thm.varifyT) results) #> after_qed; @@ -962,6 +960,7 @@ fun conclude_instantiation lthy = let val { arities, params } = the_instantiation lthy; + val (tycos, sorts, sort) = arities; val thy = ProofContext.theory_of lthy; (*val _ = map (fn (tyco, sorts, sort) => if Sign.of_sort thy @@ -970,8 +969,8 @@ 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)) + val missing_params = tycos + |> maps (fn tyco => params_of sort |> map (rpair tyco)) |> filter_out (can (inst thy) o apfst fst); fun declare_missing ((c, ty0), tyco) thy = (*fun declare_missing ((c, tyco), (_, ty)) thy =*) diff -r 4975b7529a14 -r 01753a944433 src/Pure/Isar/instance.ML --- a/src/Pure/Isar/instance.ML Wed Dec 05 14:15:48 2007 +0100 +++ b/src/Pure/Isar/instance.ML Wed Dec 05 14:15:51 2007 +0100 @@ -7,35 +7,38 @@ signature INSTANCE = sig - val instantiate: arity list -> (local_theory -> local_theory) - -> (Proof.context -> tactic) -> theory -> theory - val instance: arity list -> ((bstring * Attrib.src list) * term) list - -> theory -> Proof.state - val prove_instance: tactic -> arity list -> ((bstring * Attrib.src list) * term) list - -> theory -> thm list * theory + val instantiate: string list * sort list * sort -> (local_theory -> 'a * local_theory) + -> (Proof.context -> 'a -> tactic) -> theory -> theory - val instantiation_cmd: (xstring * sort * xstring) list - -> theory -> local_theory - val instance_cmd: (xstring * sort * xstring) list -> ((bstring * Attrib.src list) * xstring) list + val instantiation_cmd: xstring list * sort * xstring -> theory -> local_theory + val instance_cmd: xstring * sort * xstring -> ((bstring * Attrib.src list) * xstring) list -> theory -> Proof.state end; structure Instance : INSTANCE = struct +fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) = + let + val all_arities = map (fn raw_tyco => Sign.read_arity thy + (raw_tyco, raw_sorts, raw_sort)) raw_tycos; + val tycos = map #1 all_arities; + val (_, sorts, sort) = hd all_arities; + in (tycos, sorts, sort) end; + fun instantiation_cmd raw_arities thy = - TheoryTarget.instantiation (map (Sign.read_arity thy) raw_arities) thy; + TheoryTarget.instantiation (read_multi_arity thy raw_arities) thy; fun instantiate arities f tac = TheoryTarget.instantiation arities #> f - #> Class.prove_instantiation_instance tac + #-> (fn result => Class.prove_instantiation_instance (fn ctxt => tac ctxt result)) #> LocalTheory.exit #> ProofContext.theory_of; fun gen_instance prep_arity prep_attr parse_term do_proof do_proof' raw_arities defs thy = let - val arities = map (prep_arity thy) raw_arities; + val (tyco, sorts, sort) = prep_arity thy raw_arities; fun export_defs ctxt = let val ctxt_thy = ProofContext.init (ProofContext.theory_of ctxt); @@ -53,32 +56,21 @@ let val def' = (apsnd o apsnd) (Syntax.check_prop ctxt) def; in Specification.definition def' ctxt end; - in if not (null defs) orelse forall (fn (_, _, sort) => - forall (Class.is_class thy) sort) arities + in if not (null defs) orelse forall (Class.is_class thy) sort then thy - |> TheoryTarget.instantiation arities + |> TheoryTarget.instantiation ([tyco], sorts, sort) |> `(fn ctxt => map (mk_def ctxt) defs) |-> (fn defs => fold_map Specification.definition defs) |-> (fn defs => `(fn ctxt => export_defs ctxt defs)) ||> LocalTheory.reinit - (*||> ProofContext.theory_of - ||> TheoryTarget.instantiation arities*) |-> (fn defs => do_proof defs) else thy - |> do_proof' arities + |> do_proof' (tyco, sorts, sort) end; -val instance = gen_instance Sign.cert_arity (K I) (K I) - (fn _ => Class.instantiation_instance Class.conclude_instantiation) (Class.instance_arity I); val instance_cmd = gen_instance Sign.read_arity Attrib.intern_src Syntax.parse_prop (fn _ => Class.instantiation_instance Class.conclude_instantiation) (Class.instance_arity I); -fun prove_instance tac arities defs = gen_instance Sign.cert_arity (K I) (K I) - (fn defs => Class.prove_instantiation_instance (K tac) - #> Class.conclude_instantiation #> ProofContext.theory_of #> pair defs) - (pair [] o ProofContext.theory_of o Proof.global_terminal_proof - (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE) - oo Class.instance_arity I) arities defs; end; diff -r 4975b7529a14 -r 01753a944433 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Wed Dec 05 14:15:48 2007 +0100 +++ b/src/Pure/Isar/isar_syn.ML Wed Dec 05 14:15:51 2007 +0100 @@ -446,15 +446,15 @@ val _ = OuterSyntax.command "instantiation" "instantiate and prove type arity" K.thy_decl - (P.and_list1 P.arity --| P.begin + (P.multi_arity --| P.begin >> (fn arities => Toplevel.print o Toplevel.begin_local_theory true (Instance.instantiation_cmd arities))); val _ = 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) => Instance.instance_cmd arities defs)) + P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop) + >> (fn (arity, defs) => Instance.instance_cmd arity defs)) >> (Toplevel.print oo Toplevel.theory_to_proof) || Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I))); diff -r 4975b7529a14 -r 01753a944433 src/Pure/Isar/overloading.ML --- a/src/Pure/Isar/overloading.ML Wed Dec 05 14:15:48 2007 +0100 +++ b/src/Pure/Isar/overloading.ML Wed Dec 05 14:15:51 2007 +0100 @@ -8,6 +8,7 @@ signature OVERLOADING = sig val init: ((string * typ) * (string * bool)) list -> theory -> local_theory + val prep_spec: local_theory -> term -> term val conclude: local_theory -> local_theory val declare: string * typ -> theory -> term * theory val confirm: string -> local_theory -> local_theory @@ -45,14 +46,21 @@ (* syntax *) +fun subst_operation overloading = map_aterms (fn t as Const (c, ty) => + (case AList.lookup (op =) overloading (c, ty) + of SOME (v, _) => Free (v, ty) + | NONE => t) + | t => t); + +fun prep_spec lthy = + let + val overloading = get_overloading lthy; + in subst_operation overloading end; + fun term_check ts lthy = let val overloading = get_overloading lthy; - fun subst (t as Const (c, ty)) = (case AList.lookup (op =) overloading (c, ty) - of SOME (v, _) => Free (v, ty) - | NONE => t) - | subst t = t; - val ts' = (map o map_aterms) subst ts; + val ts' = map (subst_operation overloading) ts; in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', lthy) end; fun term_uncheck ts lthy =