1.1 --- a/src/Pure/Isar/ROOT.ML Fri Nov 23 21:09:34 2007 +0100
1.2 +++ b/src/Pure/Isar/ROOT.ML Fri Nov 23 21:09:35 2007 +0100
1.3 @@ -44,6 +44,9 @@
1.4 (*derived theory and proof elements*)
1.5 use "calculation.ML";
1.6 use "obtain.ML";
1.7 +
1.8 +(*local theories and target primitives*)
1.9 +use "local_theory.ML";
1.10 use "locale.ML";
1.11 use "class.ML";
1.12
1.13 @@ -52,12 +55,11 @@
1.14 use "code.ML";
1.15
1.16 (*local theories and specifications*)
1.17 -use "local_theory.ML";
1.18 use "theory_target.ML";
1.19 use "subclass.ML";
1.20 -use "instance.ML";
1.21 use "spec_parse.ML";
1.22 use "specification.ML";
1.23 +use "instance.ML";
1.24 use "constdefs.ML";
1.25
1.26 (*toplevel environment*)
2.1 --- a/src/Pure/Isar/class.ML Fri Nov 23 21:09:34 2007 +0100
2.2 +++ b/src/Pure/Isar/class.ML Fri Nov 23 21:09:35 2007 +0100
2.3 @@ -7,11 +7,7 @@
2.4
2.5 signature CLASS =
2.6 sig
2.7 - val axclass_cmd: bstring * xstring list
2.8 - -> ((bstring * Attrib.src list) * string list) list
2.9 - -> theory -> class * theory
2.10 - val classrel_cmd: xstring * xstring -> theory -> Proof.state
2.11 -
2.12 + (*classes*)
2.13 val class: bstring -> class list -> Element.context_i Locale.element list
2.14 -> string list -> theory -> string * Proof.context
2.15 val class_cmd: bstring -> xstring list -> Element.context Locale.element list
2.16 @@ -30,8 +26,29 @@
2.17 -> theory -> theory
2.18 val print_classes: theory -> unit
2.19 val class_prefix: string -> string
2.20 - val uncheck: bool ref
2.21
2.22 + (*instances*)
2.23 + val declare_overloaded: string * typ * mixfix -> theory -> term * theory
2.24 + val define_overloaded: string -> string * term -> theory -> thm * theory
2.25 + val unoverload: theory -> conv
2.26 + val overload: theory -> conv
2.27 + val unoverload_const: theory -> string * typ -> string
2.28 + val inst_const: theory -> string * string -> string
2.29 + val param_const: theory -> string -> (string * string) option
2.30 + val instantiation: arity list -> theory -> local_theory
2.31 + val proof_instantiation: (local_theory -> local_theory) -> local_theory -> Proof.state
2.32 + val prove_instantiation: (Proof.context -> tactic) -> local_theory -> local_theory
2.33 + val conclude_instantiation: local_theory -> local_theory
2.34 + val end_instantiation: local_theory -> Proof.context
2.35 + val instantiation_const: Proof.context -> string -> string option
2.36 +
2.37 + (*old axclass layer*)
2.38 + val axclass_cmd: bstring * xstring list
2.39 + -> ((bstring * Attrib.src list) * string list) list
2.40 + -> theory -> class * theory
2.41 + val classrel_cmd: xstring * xstring -> theory -> Proof.state
2.42 +
2.43 + (*old instance layer*)
2.44 val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state
2.45 val instance: arity list -> ((bstring * Attrib.src list) * term) list
2.46 -> (thm list -> theory -> theory)
2.47 @@ -43,11 +60,6 @@
2.48 val prove_instance: tactic -> arity list
2.49 -> ((bstring * Attrib.src list) * term) list
2.50 -> theory -> thm list * theory
2.51 - val unoverload: theory -> conv
2.52 - val overload: theory -> conv
2.53 - val unoverload_const: theory -> string * typ -> string
2.54 - val inst_const: theory -> string * string -> string
2.55 - val param_const: theory -> string -> (string * string) option
2.56 end;
2.57
2.58 structure Class : CLASS =
2.59 @@ -141,7 +153,9 @@
2.60 end; (*local*)
2.61
2.62
2.63 -(** explicit constants for overloaded definitions **)
2.64 +(** basic overloading **)
2.65 +
2.66 +(* bookkeeping *)
2.67
2.68 structure InstData = TheoryDataFun
2.69 (
2.70 @@ -156,8 +170,18 @@
2.71 Symtab.merge (K true) (tabb1, tabb2));
2.72 );
2.73
2.74 +val inst_tyco = Option.map fst o try (dest_Type o the_single) oo Sign.const_typargs;
2.75 +
2.76 +fun inst thy (c, tyco) =
2.77 + (the o Symtab.lookup ((the o Symtab.lookup (fst (InstData.get thy))) c)) tyco;
2.78 +
2.79 +val inst_const = fst oo inst;
2.80 +
2.81 fun inst_thms thy = (Symtab.fold (Symtab.fold (cons o snd o snd) o snd) o fst)
2.82 - (InstData.get thy) [];
2.83 + (InstData.get thy) [];
2.84 +
2.85 +val param_const = Symtab.lookup o snd o InstData.get;
2.86 +
2.87 fun add_inst (c, tyco) inst = (InstData.map o apfst
2.88 o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
2.89 #> (InstData.map o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
2.90 @@ -165,19 +189,65 @@
2.91 fun unoverload thy = MetaSimplifier.rewrite true (inst_thms thy);
2.92 fun overload thy = MetaSimplifier.rewrite true (map Thm.symmetric (inst_thms thy));
2.93
2.94 -fun inst_const thy (c, tyco) =
2.95 - (fst o the o Symtab.lookup ((the o Symtab.lookup (fst (InstData.get thy))) c)) tyco;
2.96 fun unoverload_const thy (c_ty as (c, _)) =
2.97 case AxClass.class_of_param thy c
2.98 - of SOME class => (case Sign.const_typargs thy c_ty
2.99 - of [Type (tyco, _)] => (case Symtab.lookup
2.100 - ((the o Symtab.lookup (fst (InstData.get thy))) c) tyco
2.101 + of SOME class => (case inst_tyco thy c_ty
2.102 + of SOME tyco => (case try (inst thy) (c, tyco)
2.103 of SOME (c, _) => c
2.104 | NONE => c)
2.105 - | [_] => c)
2.106 + | NONE => c)
2.107 | NONE => c;
2.108
2.109 -val param_const = Symtab.lookup o snd o InstData.get;
2.110 +
2.111 +(* declaration and definition of instances of overloaded constants *)
2.112 +
2.113 +fun primitive_note kind (name, thm) =
2.114 + PureThy.note_thmss_i kind [((name, []), [([thm], [])])]
2.115 + #>> (fn [(_, [thm])] => thm);
2.116 +
2.117 +fun declare_overloaded (c, ty, mx) thy =
2.118 + let
2.119 + val SOME class = AxClass.class_of_param thy c;
2.120 + val SOME tyco = inst_tyco thy (c, ty);
2.121 + val name_inst = NameSpace.base class ^ "_" ^ NameSpace.base tyco ^ "_inst";
2.122 + val c' = NameSpace.base c;
2.123 + val ty' = Type.strip_sorts ty;
2.124 + in
2.125 + thy
2.126 + |> Sign.sticky_prefix name_inst
2.127 + |> Sign.no_base_names
2.128 + |> Sign.notation true Syntax.mode_default [(Const (c, ty), mx)]
2.129 + |> Sign.declare_const [] (c', ty', NoSyn)
2.130 + |-> (fn const' as Const (c'', _) => Thm.add_def true
2.131 + (Thm.def_name c', Logic.mk_equals (Const (c, ty'), const'))
2.132 + #>> Thm.varifyT
2.133 + #-> (fn thm => add_inst (c, tyco) (c'', thm)
2.134 + #> primitive_note Thm.internalK (c', thm)
2.135 + #> snd
2.136 + #> Sign.restore_naming thy
2.137 + #> pair (Const (c, ty))))
2.138 + end;
2.139 +
2.140 +fun define_overloaded name (c, t) thy =
2.141 + let
2.142 + val ty = Term.fastype_of t;
2.143 + val SOME tyco = inst_tyco thy (c, ty);
2.144 + val (c', eq) = inst thy (c, tyco);
2.145 + val [Type (_, tys)] = Sign.const_typargs thy (c, ty);
2.146 + val eq' = eq
2.147 + |> Drule.instantiate' (map (SOME o Thm.ctyp_of thy) tys) [];
2.148 + (*FIXME proper recover_sort mechanism*)
2.149 + val prop = Logic.mk_equals (Const (c', ty), t);
2.150 + val name' = if name = "" then
2.151 + Thm.def_name (NameSpace.base c ^ "_" ^ NameSpace.base tyco) else name;
2.152 + in
2.153 + thy
2.154 + |> Thm.add_def false (name', prop)
2.155 + |>> (fn thm => Thm.transitive eq' thm)
2.156 + end;
2.157 +
2.158 +
2.159 +(* legacy *)
2.160
2.161 fun add_inst_def (class, tyco) (c, ty) thy =
2.162 let
2.163 @@ -206,15 +276,10 @@
2.164 let
2.165 val ((lhs as Const (c, ty), args), rhs) =
2.166 (apfst Term.strip_comb o Logic.dest_equals) prop;
2.167 - fun (*add_inst' def ([], (Const (c_inst, ty))) =
2.168 - if forall (fn TFree _ => true | _ => false) (Sign.const_typargs thy (c_inst, ty))
2.169 - then add_inst (c, tyco) (c_inst, def)
2.170 - else add_inst_def (class, tyco) (c, ty)
2.171 - |*) add_inst' _ t = add_inst_def (class, tyco) (c, ty);
2.172 in
2.173 thy
2.174 |> PureThy.add_defs_i true [((name, prop), map (Attrib.attribute_i thy) atts)]
2.175 - |-> (fn [def] => add_inst' def (args, rhs) #> pair def)
2.176 + |-> (fn [def] => add_inst_def (class, tyco) (c, ty) #> pair def)
2.177 end;
2.178
2.179
2.180 @@ -690,14 +755,11 @@
2.181 |> SOME
2.182 end;
2.183
2.184 -val uncheck = ref true;
2.185 -
2.186 fun sort_term_uncheck ts ctxt =
2.187 let
2.188 val thy = ProofContext.theory_of ctxt;
2.189 val unchecks = (#unchecks o ClassSyntax.get) ctxt;
2.190 - val ts' = if ! uncheck
2.191 - then map (Pattern.rewrite_term thy unchecks []) ts else ts;
2.192 + val ts' = map (Pattern.rewrite_term thy unchecks []) ts;
2.193 in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
2.194
2.195 fun init_ctxt sups base_sort ctxt =
2.196 @@ -896,4 +958,174 @@
2.197 |> Sign.restore_naming thy
2.198 end;
2.199
2.200 +
2.201 +(** instantiation target **)
2.202 +
2.203 +(* bookkeeping *)
2.204 +
2.205 +datatype instantiation = Instantiation of {
2.206 + arities: arity list,
2.207 + params: ((string * string) * (string * typ)) list
2.208 +}
2.209 +
2.210 +structure Instantiation = ProofDataFun
2.211 +(
2.212 + type T = instantiation
2.213 + fun init _ = Instantiation { arities = [], params = [] };
2.214 +);
2.215 +
2.216 +fun mk_instantiation (arities, params) = Instantiation {
2.217 + arities = arities, params = params
2.218 + };
2.219 +fun map_instantiation f (Instantiation { arities, params }) =
2.220 + mk_instantiation (f (arities, params));
2.221 +
2.222 +fun the_instantiation ctxt = case Instantiation.get ctxt
2.223 + of Instantiation { arities = [], ... } => error "No instantiation target"
2.224 + | Instantiation data => data;
2.225 +
2.226 +fun init_instantiation arities ctxt =
2.227 + let
2.228 + val thy = ProofContext.theory_of ctxt;
2.229 + val _ = if null arities then error "At least one arity must be given" else ();
2.230 + val _ = case (duplicates (op =) o map #1) arities
2.231 + of [] => ()
2.232 + | dupl_tycos => error ("Type constructors occur more than once in arities: "
2.233 + ^ commas_quote dupl_tycos);
2.234 + val ty_insts = map (fn (tyco, sorts, _) =>
2.235 + (tyco, Type (tyco, map TFree (Name.names Name.context Name.aT sorts))))
2.236 + arities;
2.237 + val ty_inst = the o AList.lookup (op =) ty_insts;
2.238 + fun type_name "*" = "prod"
2.239 + | type_name "+" = "sum"
2.240 + | type_name s = NameSpace.base s; (*FIXME*)
2.241 + fun get_param tyco sorts (param, (c, ty)) =
2.242 + ((unoverload_const thy (c, ty), tyco),
2.243 + (param ^ "_" ^ type_name tyco,
2.244 + map_atyps (K (ty_inst tyco)) ty));
2.245 + fun get_params (tyco, sorts, sort) =
2.246 + map (get_param tyco sorts) (these_params thy sort)
2.247 + val params = maps get_params arities;
2.248 + in
2.249 + ctxt
2.250 + |> Instantiation.put (mk_instantiation (arities, params))
2.251 + |> fold (Variable.declare_term o Logic.mk_type o snd) ty_insts
2.252 + |> fold (Variable.declare_term o Free o snd) params
2.253 + end;
2.254 +
2.255 +val instantiation_params = #params o the_instantiation;
2.256 +
2.257 +fun instantiation_const ctxt v = instantiation_params ctxt
2.258 + |> find_first (fn (_, (v', _)) => v = v')
2.259 + |> Option.map (fst o fst);
2.260 +
2.261 +
2.262 +(* syntax *)
2.263 +
2.264 +fun inst_term_check ts ctxt =
2.265 + let
2.266 + val params = instantiation_params ctxt;
2.267 + val tsig = ProofContext.tsig_of ctxt;
2.268 + val thy = ProofContext.theory_of ctxt;
2.269 +
2.270 + fun check_improve (Const (c, ty)) = (case inst_tyco thy (c, ty)
2.271 + of SOME tyco => (case AList.lookup (op =) params (c, tyco)
2.272 + of SOME (_, ty') => Type.typ_match tsig (ty, ty')
2.273 + | NONE => I)
2.274 + | NONE => I)
2.275 + | check_improve _ = I;
2.276 + val improvement = (fold o fold_aterms) check_improve ts Vartab.empty;
2.277 + val ts' = (map o map_types) (Envir.typ_subst_TVars improvement) ts;
2.278 + val ts'' = (map o map_aterms) (fn t as Const (c, ty) => (case inst_tyco thy (c, ty)
2.279 + of SOME tyco => (case AList.lookup (op =) params (c, tyco)
2.280 + of SOME v_ty => Free v_ty
2.281 + | NONE => t)
2.282 + | NONE => t)
2.283 + | t => t) ts';
2.284 + in if eq_list (op aconv) (ts, ts'') then NONE else SOME (ts'', ctxt) end;
2.285 +
2.286 +fun inst_term_uncheck ts ctxt =
2.287 + let
2.288 + val params = instantiation_params ctxt;
2.289 + val ts' = (map o map_aterms) (fn t as Free (v, ty) =>
2.290 + (case get_first (fn ((c, _), (v', _)) => if v = v' then SOME c else NONE) params
2.291 + of SOME c => Const (c, ty)
2.292 + | NONE => t)
2.293 + | t => t) ts;
2.294 + in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
2.295 +
2.296 +
2.297 +(* target *)
2.298 +
2.299 +fun instantiation arities =
2.300 + ProofContext.init
2.301 + #> init_instantiation arities
2.302 + #> fold ProofContext.add_arity arities
2.303 + #> Context.proof_map (
2.304 + Syntax.add_term_check 0 "instance" inst_term_check
2.305 + #> Syntax.add_term_uncheck 0 "instance" inst_term_uncheck);
2.306 +
2.307 +fun gen_proof_instantiation do_proof after_qed lthy =
2.308 + let
2.309 + (*FIXME should work on fresh context but continue local theory afterwards*)
2.310 + val ctxt = LocalTheory.target_of lthy;
2.311 + val arities = (#arities o the_instantiation) ctxt;
2.312 + val arities_proof = maps
2.313 + (Logic.mk_arities o Sign.cert_arity (ProofContext.theory_of ctxt)) arities;
2.314 + fun after_qed' results =
2.315 + LocalTheory.theory (fold (AxClass.add_arity o Thm.varifyT) results)
2.316 + #> after_qed;
2.317 + in
2.318 + lthy
2.319 + |> do_proof after_qed' arities_proof
2.320 + end;
2.321 +
2.322 +val proof_instantiation = gen_proof_instantiation (fn after_qed => fn ts =>
2.323 + Proof.theorem_i NONE (after_qed o map the_single) (map (fn t => [(t, [])]) ts));
2.324 +
2.325 +fun prove_instantiation tac = gen_proof_instantiation (fn after_qed =>
2.326 + fn ts => fn lthy => after_qed (Goal.prove_multi lthy [] [] ts
2.327 + (fn {context, ...} => tac context)) lthy) I;
2.328 +
2.329 +fun conclude_instantiation lthy =
2.330 + let
2.331 + val arities = (#arities o the_instantiation) lthy;
2.332 + val thy = ProofContext.theory_of lthy;
2.333 + (*val _ = map (fn (tyco, sorts, sort) =>
2.334 + if Sign.of_sort thy
2.335 + (Type (tyco, map TFree (Name.names Name.context Name.aT sorts)), sort)
2.336 + then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco)))
2.337 + arities; FIXME activate when old instance command is gone*)
2.338 + val params_of = maps (these o try (#params o AxClass.get_info thy))
2.339 + o Sign.complete_sort thy;
2.340 + val missing_params = arities
2.341 + |> maps (fn (tyco, _, sort) => params_of sort |> map (rpair tyco))
2.342 + |> filter_out (can (inst thy) o apfst fst);
2.343 + fun declare_missing ((c, ty), tyco) thy =
2.344 + let
2.345 + val SOME class = AxClass.class_of_param thy c;
2.346 + val name_inst = NameSpace.base class ^ "_" ^ NameSpace.base tyco ^ "_inst";
2.347 + val vs = Name.names Name.context Name.aT (replicate (Sign.arity_number thy tyco) []);
2.348 + val ty' = map_atyps (fn _ => Type (tyco, map TFree vs)) ty;
2.349 + val c' = NameSpace.base c;
2.350 + in
2.351 + thy
2.352 + |> Sign.sticky_prefix name_inst
2.353 + |> Sign.no_base_names
2.354 + |> Sign.declare_const [] (c', ty', NoSyn)
2.355 + |-> (fn const' as Const (c'', _) => Thm.add_def true
2.356 + (Thm.def_name c', Logic.mk_equals (const', Const (c, ty')))
2.357 + #>> Thm.varifyT
2.358 + #-> (fn thm => add_inst (c, tyco) (c'', Thm.symmetric thm)
2.359 + #> primitive_note Thm.internalK (c', thm)
2.360 + #> snd
2.361 + #> Sign.restore_naming thy))
2.362 + end;
2.363 + in
2.364 + lthy
2.365 + |> LocalTheory.theory (fold declare_missing missing_params)
2.366 + end;
2.367 +
2.368 +val end_instantiation = conclude_instantiation #> LocalTheory.target_of;
2.369 +
2.370 end;
3.1 --- a/src/Pure/Isar/code.ML Fri Nov 23 21:09:34 2007 +0100
3.2 +++ b/src/Pure/Isar/code.ML Fri Nov 23 21:09:35 2007 +0100
3.3 @@ -24,6 +24,7 @@
3.4 val del_post: thm -> theory -> theory
3.5 val add_datatype: (string * typ) list -> theory -> theory
3.6 val add_datatype_cmd: string list -> theory -> theory
3.7 + val type_interpretation: (string * string list -> theory -> theory) -> theory -> theory
3.8 val add_case: thm -> theory -> theory
3.9 val add_undefined: string -> theory -> theory
3.10
3.11 @@ -537,18 +538,15 @@
3.12 fun aggregate f [] = NONE
3.13 | aggregate f (x::xs) = SOME (aggr_neutr f x xs);
3.14
3.15 -fun inter_sorts thy =
3.16 - let
3.17 - val algebra = Sign.classes_of thy;
3.18 - val inters = curry (Sorts.inter_sort algebra);
3.19 - in aggregate (map2 inters) end;
3.20 +fun inter_sorts algebra =
3.21 + aggregate (map2 (curry (Sorts.inter_sort algebra)));
3.22
3.23 fun specific_constraints thy (class, tyco) =
3.24 let
3.25 val vs = Name.invents Name.context "" (Sign.arity_number thy tyco);
3.26 val classparams = (map fst o these o try (#params o AxClass.get_info thy)) class;
3.27 val funcs = classparams
3.28 - |> map (fn c => Class.inst_const thy (c, tyco))
3.29 + |> map_filter (fn c => try (Class.inst_const thy) (c, tyco))
3.30 |> map (Symtab.lookup ((the_funcs o the_exec) thy))
3.31 |> (map o Option.map) (Susp.force o fst o snd)
3.32 |> maps these
3.33 @@ -558,37 +556,53 @@
3.34 val sorts = map (sorts_of o Sign.const_typargs thy o CodeUnit.head_func) funcs;
3.35 in sorts end;
3.36
3.37 -fun weakest_constraints thy (class, tyco) =
3.38 +fun weakest_constraints thy algebra (class, tyco) =
3.39 let
3.40 - val all_superclasses = Sign.complete_sort thy [class];
3.41 - in case inter_sorts thy (maps (fn class => specific_constraints thy (class, tyco)) all_superclasses)
3.42 + val all_superclasses = Sorts.complete_sort algebra [class];
3.43 + in case inter_sorts algebra (maps (fn class => specific_constraints thy (class, tyco)) all_superclasses)
3.44 of SOME sorts => sorts
3.45 - | NONE => Sign.arity_sorts thy tyco [class]
3.46 + | NONE => Sorts.mg_domain algebra tyco [class]
3.47 end;
3.48
3.49 -fun strongest_constraints thy (class, tyco) =
3.50 +fun strongest_constraints thy algebra (class, tyco) =
3.51 let
3.52 - val algebra = Sign.classes_of thy;
3.53 val all_subclasses = class :: Graph.all_preds ((#classes o Sorts.rep_algebra) algebra) [class];
3.54 val inst_subclasses = filter (can (Sorts.mg_domain algebra tyco) o single) all_subclasses;
3.55 - in case inter_sorts thy (maps (fn class => specific_constraints thy (class, tyco)) inst_subclasses)
3.56 + in case inter_sorts algebra (maps (fn class => specific_constraints thy (class, tyco)) inst_subclasses)
3.57 of SOME sorts => sorts
3.58 | NONE => replicate
3.59 - (Sign.arity_number thy tyco) (Sign.minimize_sort thy (Sign.all_classes thy))
3.60 + (Sign.arity_number thy tyco) (Sorts.minimize_sort algebra (Sorts.all_classes algebra))
3.61 + end;
3.62 +
3.63 +fun get_algebra thy (class, tyco) =
3.64 + let
3.65 + val base_algebra = Sign.classes_of thy;
3.66 + in if can (Sorts.mg_domain base_algebra tyco) [class]
3.67 + then base_algebra
3.68 + else let
3.69 + val superclasses = Sorts.super_classes base_algebra class;
3.70 + val sorts = inter_sorts base_algebra
3.71 + (map_filter (fn class => try (Sorts.mg_domain base_algebra tyco) [class]) superclasses)
3.72 + |> the_default (replicate (Sign.arity_number thy tyco) [])
3.73 + in
3.74 + base_algebra
3.75 + |> Sorts.add_arities (Sign.pp thy) (tyco, [(class, sorts)])
3.76 + end
3.77 end;
3.78
3.79 fun gen_classparam_typ constr thy class (c, tyco) =
3.80 let
3.81 + val algebra = get_algebra thy (class, tyco);
3.82 val cs = these (try (#params o AxClass.get_info thy) class);
3.83 - val ty = (the o AList.lookup (op =) cs) c;
3.84 + val SOME ty = AList.lookup (op =) cs c;
3.85 val sort_args = Name.names (Name.declare Name.aT Name.context) Name.aT
3.86 - (constr thy (class, tyco));
3.87 + (constr thy algebra (class, tyco));
3.88 val ty_inst = Type (tyco, map TFree sort_args);
3.89 in Logic.varifyT (map_type_tfree (K ty_inst) ty) end;
3.90
3.91 fun retrieve_algebra thy operational =
3.92 Sorts.subalgebra (Sign.pp thy) operational
3.93 - (weakest_constraints thy)
3.94 + (weakest_constraints thy (Sign.classes_of thy))
3.95 (Sign.classes_of thy);
3.96
3.97 in
3.98 @@ -763,18 +777,22 @@
3.99 val add_default_func_attr = Attrib.internal (fn _ => Thm.declaration_attribute
3.100 (fn thm => Context.mapping (add_default_func thm) I));
3.101
3.102 +structure TypeInterpretation = InterpretationFun(type T = string * string list val eq = op =);
3.103 +val type_interpretation = TypeInterpretation.interpretation;
3.104 +
3.105 fun add_datatype raw_cs thy =
3.106 let
3.107 val cs = map (fn c_ty as (_, ty) => (Class.unoverload_const thy c_ty, ty)) raw_cs;
3.108 val (tyco, vs_cos) = CodeUnit.constrset_of_consts thy cs;
3.109 - val purge_cs = map fst (snd vs_cos);
3.110 - val purge_cs' = case Symtab.lookup ((the_dtyps o the_exec) thy) tyco
3.111 - of SOME (vs, cos) => if null cos then NONE else SOME (purge_cs @ map fst cos)
3.112 + val cs' = map fst (snd vs_cos);
3.113 + val purge_cs = case Symtab.lookup ((the_dtyps o the_exec) thy) tyco
3.114 + of SOME (vs, cos) => if null cos then NONE else SOME (cs' @ map fst cos)
3.115 | NONE => NONE;
3.116 in
3.117 thy
3.118 - |> map_exec_purge purge_cs' (map_dtyps (Symtab.update (tyco, vs_cos))
3.119 + |> map_exec_purge purge_cs (map_dtyps (Symtab.update (tyco, vs_cos))
3.120 #> map_funcs (fold (Symtab.delete_safe o fst) cs))
3.121 + |> TypeInterpretation.data (tyco, cs')
3.122 end;
3.123
3.124 fun add_datatype_cmd raw_cs thy =
3.125 @@ -837,7 +855,8 @@
3.126 add_attribute (name, Args.del |-- Scan.succeed (mk_attribute del)
3.127 || Scan.succeed (mk_attribute add))
3.128 in
3.129 - add_del_attribute ("func", (add_func, del_func))
3.130 + TypeInterpretation.init
3.131 + #> add_del_attribute ("func", (add_func, del_func))
3.132 #> add_del_attribute ("inline", (add_inline, del_inline))
3.133 #> add_del_attribute ("post", (add_post, del_post))
3.134 end);
4.1 --- a/src/Pure/Isar/instance.ML Fri Nov 23 21:09:34 2007 +0100
4.2 +++ b/src/Pure/Isar/instance.ML Fri Nov 23 21:09:35 2007 +0100
4.3 @@ -2,79 +2,74 @@
4.4 ID: $Id$
4.5 Author: Florian Haftmann, TU Muenchen
4.6
4.7 -User-level instantiation interface for classes.
4.8 -FIXME not operative for the moment
4.9 +A primitive instance command, based on instantiation target.
4.10 *)
4.11
4.12 signature INSTANCE =
4.13 sig
4.14 - val begin_instantiation: arity list -> theory -> local_theory
4.15 - val begin_instantiation_cmd: (xstring * string list * string) list
4.16 + val instantiate: arity list -> (local_theory -> local_theory)
4.17 + -> (Proof.context -> tactic) -> theory -> theory
4.18 + val instance: arity list -> ((bstring * Attrib.src list) * term) list
4.19 + -> (thm list -> theory -> theory)
4.20 + -> theory -> Proof.state
4.21 + val prove_instance: tactic -> arity list -> ((bstring * Attrib.src list) * term) list
4.22 + -> theory -> thm list * theory
4.23 +
4.24 + val instantiation_cmd: (xstring * sort * xstring) list
4.25 -> theory -> local_theory
4.26 - val proof_instantiation: local_theory -> Proof.state
4.27 + val instance_cmd: (xstring * sort * xstring) list -> ((bstring * Attrib.src list) * xstring) list
4.28 + -> (thm list -> theory -> theory)
4.29 + -> theory -> Proof.state
4.30 end;
4.31
4.32 structure Instance : INSTANCE =
4.33 struct
4.34
4.35 -structure Instantiation = ProofDataFun
4.36 -(
4.37 - type T = ((string * (string * sort) list) * sort) list * ((string * typ) * string) list;
4.38 - fun init _ = ([], []);
4.39 -);
4.40 +fun instantiation_cmd raw_arities thy =
4.41 + TheoryTarget.instantiation (map (Sign.read_arity thy) raw_arities) thy;
4.42 +
4.43 +fun instantiate arities f tac =
4.44 + TheoryTarget.instantiation arities
4.45 + #> f
4.46 + #> Class.prove_instantiation tac
4.47 + #> LocalTheory.exit
4.48 + #> ProofContext.theory_of;
4.49
4.50 -local
4.51 -
4.52 -fun gen_begin_instantiation prep_arity raw_arities thy =
4.53 +fun gen_instance prep_arity prep_attr prep_term do_proof raw_arities defs after_qed thy =
4.54 let
4.55 - fun prep_arity' raw_arity names =
4.56 + fun export_defs ctxt =
4.57 + let
4.58 + val ctxt_thy = ProofContext.init (ProofContext.theory_of ctxt);
4.59 + in
4.60 + map (snd o snd)
4.61 + #> map (Assumption.export false ctxt ctxt_thy)
4.62 + #> Variable.export ctxt ctxt_thy
4.63 + end;
4.64 + fun mk_def ctxt ((name, raw_attr), raw_t) =
4.65 let
4.66 - val arity as (tyco, sorts, sort) = prep_arity thy raw_arity;
4.67 - val vs = Name.invents names Name.aT (length sorts);
4.68 - val names' = fold Name.declare vs names;
4.69 - in (((tyco, vs ~~ sorts), sort), names') end;
4.70 - val (arities, _) = fold_map prep_arity' raw_arities Name.context;
4.71 - fun get_param tyco ty_subst (param, (c, ty)) =
4.72 - ((param ^ "_" ^ NameSpace.base tyco, map_atyps (K ty_subst) ty),
4.73 - Class.unoverload_const thy (c, ty));
4.74 - fun get_params ((tyco, vs), sort) =
4.75 - Class.these_params thy sort
4.76 - |> map (get_param tyco (Type (tyco, map TFree vs)));
4.77 - val params = maps get_params arities;
4.78 - val ctxt =
4.79 - ProofContext.init thy
4.80 - |> Instantiation.put (arities, params);
4.81 - val thy_target = TheoryTarget.begin "" ctxt;
4.82 - val operations = {
4.83 - pretty = LocalTheory.pretty,
4.84 - axioms = LocalTheory.axioms,
4.85 - abbrev = LocalTheory.abbrev,
4.86 - define = LocalTheory.define,
4.87 - notes = LocalTheory.notes,
4.88 - type_syntax = LocalTheory.type_syntax,
4.89 - term_syntax = LocalTheory.term_syntax,
4.90 - declaration = LocalTheory.pretty,
4.91 - reinit = LocalTheory.reinit,
4.92 - exit = LocalTheory.exit
4.93 - };
4.94 - in TheoryTarget.begin "" ctxt end;
4.95 + val attr = map (prep_attr thy) raw_attr;
4.96 + val t = prep_term ctxt raw_t;
4.97 + in (NONE, ((name, attr), t)) end;
4.98 + val arities = map (prep_arity thy) raw_arities;
4.99 + in
4.100 + thy
4.101 + |> TheoryTarget.instantiation arities
4.102 + |> `(fn ctxt => map (mk_def ctxt) defs)
4.103 + |-> (fn defs => fold_map Specification.definition defs)
4.104 + |-> (fn defs => `(fn ctxt => export_defs ctxt defs))
4.105 + ||> LocalTheory.exit
4.106 + ||> ProofContext.theory_of
4.107 + ||> TheoryTarget.instantiation arities
4.108 + |-> (fn defs => do_proof defs (LocalTheory.theory (after_qed defs)))
4.109 + end;
4.110
4.111 -in
4.112 -
4.113 -val begin_instantiation = gen_begin_instantiation Sign.cert_arity;
4.114 -val begin_instantiation_cmd = gen_begin_instantiation Sign.read_arity;
4.115 +val instance = gen_instance Sign.cert_arity (K I) (K I)
4.116 + (fn _ => fn after_qed => Class.proof_instantiation (after_qed #> Class.conclude_instantiation));
4.117 +val instance_cmd = gen_instance Sign.read_arity Attrib.intern_src
4.118 + (fn ctxt => Syntax.parse_prop ctxt #> Syntax.check_prop ctxt)
4.119 + (fn _ => fn after_qed => Class.proof_instantiation (after_qed #> Class.conclude_instantiation));
4.120 +fun prove_instance tac arities defs = gen_instance Sign.cert_arity (K I) (K I)
4.121 + (fn defs => fn after_qed => Class.prove_instantiation (K tac)
4.122 + #> after_qed #> Class.conclude_instantiation #> ProofContext.theory_of #> pair defs) arities defs (K I);
4.123
4.124 end;
4.125 -
4.126 -fun gen_proof_instantiation do_proof after_qed lthy =
4.127 - let
4.128 - val ctxt = LocalTheory.target_of lthy;
4.129 - val arities = case Instantiation.get ctxt
4.130 - of ([], _) => error "no instantiation target"
4.131 - | (arities, _) => map (fn ((tyco, vs), sort) => (tyco, map snd vs, sort)) arities;
4.132 - val thy = ProofContext.theory_of ctxt;
4.133 - in (do_proof after_qed arities) thy end;
4.134 -
4.135 -val proof_instantiation = gen_proof_instantiation Class.instance_arity I;
4.136 -
4.137 -end;
5.1 --- a/src/Pure/Isar/isar_syn.ML Fri Nov 23 21:09:34 2007 +0100
5.2 +++ b/src/Pure/Isar/isar_syn.ML Fri Nov 23 21:09:35 2007 +0100
5.3 @@ -113,7 +113,7 @@
5.4 val _ =
5.5 OuterSyntax.command "typedecl" "type declaration" K.thy_decl
5.6 (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) =>
5.7 - Toplevel.theory (Sign.add_typedecls [(a, args, mx)])));
5.8 + Toplevel.theory (Typedecl.add (a, args, mx) #> snd)));
5.9
5.10 val _ =
5.11 OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
5.12 @@ -448,18 +448,18 @@
5.13 OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
5.14 ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
5.15 P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
5.16 - >> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func (* FIXME ? *))))
5.17 + >> (fn (arities, defs) => Class.instance_cmd arities defs (fold Code.add_default_func)))
5.18 >> (Toplevel.print oo Toplevel.theory_to_proof));
5.19
5.20 val _ =
5.21 OuterSyntax.command "instantiation" "prove type arity" K.thy_decl
5.22 - (P.and_list1 P.arity -- P.opt_begin
5.23 - >> (fn (arities, begin) => (begin ? Toplevel.print) o
5.24 - Toplevel.begin_local_theory begin (Instance.begin_instantiation_cmd arities)));
5.25 + (P.and_list1 P.arity --| P.begin
5.26 + >> (fn arities => Toplevel.print o
5.27 + Toplevel.begin_local_theory true (Instance.instantiation_cmd arities)));
5.28
5.29 val _ = (* FIXME incorporate into "instance" *)
5.30 OuterSyntax.command "instance_proof" "prove type arity relation" K.thy_goal
5.31 - (Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE Instance.proof_instantiation));
5.32 + (Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.proof_instantiation I)));
5.33
5.34
5.35 (* code generation *)
6.1 --- a/src/Pure/Isar/theory_target.ML Fri Nov 23 21:09:34 2007 +0100
6.2 +++ b/src/Pure/Isar/theory_target.ML Fri Nov 23 21:09:35 2007 +0100
6.3 @@ -2,15 +2,17 @@
6.4 ID: $Id$
6.5 Author: Makarius
6.6
6.7 -Common theory/locale/class targets.
6.8 +Common theory/locale/class/instantiation targets.
6.9 *)
6.10
6.11 signature THEORY_TARGET =
6.12 sig
6.13 - val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
6.14 + val peek: local_theory -> {target: string, is_locale: bool,
6.15 + is_class: bool, instantiation: arity list}
6.16 val init: string option -> theory -> local_theory
6.17 val begin: string -> Proof.context -> local_theory
6.18 val context: xstring -> theory -> local_theory
6.19 + val instantiation: arity list -> theory -> local_theory
6.20 end;
6.21
6.22 structure TheoryTarget: THEORY_TARGET =
6.23 @@ -18,12 +20,14 @@
6.24
6.25 (* context data *)
6.26
6.27 -datatype target = Target of {target: string, is_locale: bool, is_class: bool};
6.28 +datatype target = Target of {target: string, is_locale: bool,
6.29 + is_class: bool, instantiation: arity list};
6.30
6.31 -fun make_target target is_locale is_class =
6.32 - Target {target = target, is_locale = is_locale, is_class = is_class};
6.33 +fun make_target target is_locale is_class instantiation =
6.34 + Target {target = target, is_locale = is_locale,
6.35 + is_class = is_class, instantiation = instantiation};
6.36
6.37 -val global_target = make_target "" false false;
6.38 +val global_target = make_target "" false false [];
6.39
6.40 structure Data = ProofDataFun
6.41 (
6.42 @@ -36,7 +40,7 @@
6.43
6.44 (* pretty *)
6.45
6.46 -fun pretty (Target {target, is_locale, is_class}) ctxt =
6.47 +fun pretty (Target {target, is_locale, is_class, instantiation}) ctxt =
6.48 let
6.49 val thy = ProofContext.theory_of ctxt;
6.50 val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
6.51 @@ -186,13 +190,18 @@
6.52 Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
6.53 end;
6.54
6.55 -fun declare_const (ta as Target {target, is_locale, is_class}) depends ((c, T), mx) lthy =
6.56 +fun declare_const (ta as Target {target, is_locale, is_class, instantiation}) depends ((c, T), mx) lthy =
6.57 let
6.58 val pos = ContextPosition.properties_of lthy;
6.59 val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
6.60 val U = map #2 xs ---> T;
6.61 val (mx1, mx2, mx3) = fork_mixfix ta mx;
6.62 - val (const, lthy') = lthy |> LocalTheory.theory_result (Sign.declare_const pos (c, U, mx3));
6.63 + val declare_const = if null instantiation
6.64 + then Sign.declare_const pos (c, U, mx3)
6.65 + else case Class.instantiation_const lthy c
6.66 + of SOME c' => Class.declare_overloaded (c', U, mx3)
6.67 + | NONE => Sign.declare_const pos (c, U, mx3);
6.68 + val (const, lthy') = lthy |> LocalTheory.theory_result declare_const;
6.69 val t = Term.list_comb (const, map Free xs);
6.70 in
6.71 lthy'
6.72 @@ -204,7 +213,7 @@
6.73
6.74 (* abbrev *)
6.75
6.76 -fun abbrev (ta as Target {target, is_locale, is_class}) prmode ((c, mx), t) lthy =
6.77 +fun abbrev (ta as Target {target, is_locale, is_class, instantiation}) prmode ((c, mx), t) lthy =
6.78 let
6.79 val pos = ContextPosition.properties_of lthy;
6.80 val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
6.81 @@ -236,7 +245,7 @@
6.82
6.83 (* define *)
6.84
6.85 -fun define (ta as Target {target, is_locale, is_class})
6.86 +fun define (ta as Target {target, is_locale, is_class, instantiation})
6.87 kind ((c, mx), ((name, atts), rhs)) lthy =
6.88 let
6.89 val thy = ProofContext.theory_of lthy;
6.90 @@ -253,12 +262,18 @@
6.91 val (_, lhs') = Logic.dest_equals (Thm.prop_of local_def);
6.92
6.93 (*def*)
6.94 + val is_instantiation = not (null instantiation)
6.95 + andalso is_some (Class.instantiation_const lthy c);
6.96 + val define_const = if not is_instantiation
6.97 + then (fn name => fn eq => Thm.add_def false (name, Logic.mk_equals eq))
6.98 + else (fn name => fn (Const (c, _), rhs) => Class.define_overloaded name (c, rhs));
6.99 val (global_def, lthy3) = lthy2
6.100 - |> LocalTheory.theory_result (Thm.add_def false (name', Logic.mk_equals (lhs', rhs')));
6.101 - val def = LocalDefs.trans_terms lthy3
6.102 + |> LocalTheory.theory_result (define_const name' (lhs', rhs'));
6.103 + val def = if not is_instantiation then LocalDefs.trans_terms lthy3
6.104 [(*c == global.c xs*) local_def,
6.105 (*global.c xs == rhs'*) global_def,
6.106 - (*rhs' == rhs*) Thm.symmetric rhs_conv];
6.107 + (*rhs' == rhs*) Thm.symmetric rhs_conv]
6.108 + else Thm.transitive local_def global_def;
6.109
6.110 (*note*)
6.111 val ([(res_name, [res])], lthy4) = lthy3
6.112 @@ -298,14 +313,18 @@
6.113 local
6.114
6.115 fun init_target _ NONE = global_target
6.116 - | init_target thy (SOME target) = make_target target true (Class.is_class thy target);
6.117 + | init_target thy (SOME target) = make_target target true (Class.is_class thy target) [];
6.118 +
6.119 +fun init_instantiaton arities = make_target "" false false arities
6.120
6.121 -fun init_ctxt (Target {target, is_locale, is_class}) =
6.122 - if not is_locale then ProofContext.init
6.123 - else if not is_class then Locale.init target
6.124 - else Class.init target;
6.125 +fun init_ctxt (Target {target, is_locale, is_class, instantiation}) =
6.126 + if null instantiation then
6.127 + if not is_locale then ProofContext.init
6.128 + else if not is_class then Locale.init target
6.129 + else Class.init target
6.130 + else Class.instantiation instantiation;
6.131
6.132 -fun init_lthy (ta as Target {target, ...}) =
6.133 +fun init_lthy (ta as Target {target, instantiation, ...}) =
6.134 Data.put ta #>
6.135 LocalTheory.init (NameSpace.base target)
6.136 {pretty = pretty ta,
6.137 @@ -317,7 +336,7 @@
6.138 term_syntax = term_syntax ta,
6.139 declaration = declaration ta,
6.140 reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy),
6.141 - exit = LocalTheory.target_of}
6.142 + exit = if null instantiation then LocalTheory.target_of else Class.end_instantiation}
6.143 and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
6.144
6.145 in
6.146 @@ -328,6 +347,9 @@
6.147 fun context "-" thy = init NONE thy
6.148 | context target thy = init (SOME (Locale.intern thy target)) thy;
6.149
6.150 +fun instantiation raw_arities thy =
6.151 + init_lthy_ctxt (init_instantiaton (map (Sign.cert_arity thy) raw_arities)) thy;
6.152 +
6.153 end;
6.154
6.155 end;