--- a/src/Pure/Isar/theory_target.ML Fri Feb 23 08:39:25 2007 +0100
+++ b/src/Pure/Isar/theory_target.ML Fri Feb 23 08:39:26 2007 +0100
@@ -8,7 +8,7 @@
signature THEORY_TARGET =
sig
val peek: local_theory -> string option
- val begin: bool -> bstring -> Proof.context -> local_theory
+ val begin: bstring -> Proof.context -> local_theory
val init: xstring option -> theory -> local_theory
val init_i: string option -> theory -> local_theory
end;
@@ -60,7 +60,7 @@
LocalTheory.term_syntax (ProofContext.target_abbrev prmode ((c, mx), t)) #>
ProofContext.add_abbrev Syntax.internalM (c, t) #> snd;
-fun consts is_class is_loc depends decls lthy =
+fun consts is_loc some_class depends decls lthy =
let
val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
@@ -68,7 +68,7 @@
let
val U = map #2 xs ---> T;
val t = Term.list_comb (Const (Sign.full_name thy c, U), map Free xs);
- val (mx1, mx2) = ClassPackage.fork_mixfix is_class is_loc mx;
+ val (mx1, mx2) = ClassPackage.fork_mixfix is_loc some_class mx;
val thy' = Sign.add_consts_authentic [(c, U, mx1)] thy;
in (((c, mx2), t), thy') end;
@@ -87,7 +87,7 @@
#1 (ProofContext.inferred_fixes ctxt)
|> filter (member (op =) (fold (Variable.add_fixed ctxt) ts []));
-fun abbrev is_class is_loc prmode ((raw_c, mx), raw_t) lthy =
+fun abbrev is_loc some_class prmode ((raw_c, mx), raw_t) lthy =
let
val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
val target = LocalTheory.target_of lthy;
@@ -102,7 +102,7 @@
val ((lhs as Const (full_c, _), rhs), lthy1) = lthy
|> LocalTheory.theory_result (Sign.add_abbrev (#1 prmode) (c, u'));
- val (mx1, mx2) = ClassPackage.fork_mixfix is_class is_loc mx;
+ val (mx1, mx2) = ClassPackage.fork_mixfix is_loc some_class mx;
in
lthy1
|> LocalTheory.theory (Sign.add_notation prmode [(lhs, mx1)])
@@ -129,7 +129,7 @@
in
-fun defs loc is_class kind args lthy0 =
+fun defs loc some_class kind args lthy0 =
let
fun def ((c, mx), ((name, atts), rhs)) lthy1 =
let
@@ -147,12 +147,12 @@
[(*c == loc.c xs*) lhs_def,
(*lhs' == rhs'*) def,
(*rhs' == rhs*) Thm.symmetric rhs_conv];
- val lthy4 = if is_class
- then
- LocalTheory.raw_theory
- (ClassPackage.add_def_in_class lthy3 loc
- ((c, mx), ((name, atts), (rhs, eq)))) lthy3
- else lthy3;
+ val lthy4 = case some_class
+ of SOME class =>
+ LocalTheory.raw_theory
+ (ClassPackage.add_def_in_class lthy3 class
+ ((c, mx), ((name, atts), (rhs, eq)))) lthy3
+ | _ => lthy3;
in ((lhs, ((name', atts), [([eq], [])])), lthy4) end;
val ((lhss, facts), lthy') = lthy0 |> fold_map def args |>> split_list;
@@ -298,15 +298,20 @@
(* init and exit *)
-fun begin is_class loc =
- let val is_loc = loc <> "" in
- Data.put (if is_loc then SOME loc else NONE) #>
- LocalTheory.init (NameSpace.base loc)
+fun begin loc ctxt =
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val is_loc = loc <> "";
+ val some_class = ClassPackage.class_of_locale thy loc;
+ in
+ ctxt
+ |> Data.put (if is_loc then SOME loc else NONE)
+ |> LocalTheory.init (NameSpace.base loc)
{pretty = pretty loc,
- consts = consts is_class is_loc,
+ consts = consts is_loc some_class,
axioms = axioms,
- abbrev = abbrev is_class is_loc,
- defs = defs loc is_class,
+ abbrev = abbrev is_loc some_class,
+ defs = defs loc some_class,
notes = notes loc,
type_syntax = type_syntax loc,
term_syntax = term_syntax loc,
@@ -314,14 +319,12 @@
target_morphism = target_morphism loc,
target_naming = target_naming loc,
reinit = fn _ =>
- begin is_class loc o (if is_loc then Locale.init loc else ProofContext.init),
+ begin loc o (if is_loc then Locale.init loc else ProofContext.init),
exit = LocalTheory.target_of}
end;
-fun init_i NONE thy = begin false "" (ProofContext.init thy)
- | init_i (SOME loc) thy =
- begin ((is_some o ClassPackage.class_of_locale thy) loc)
- loc (Locale.init loc thy);
+fun init_i NONE thy = begin "" (ProofContext.init thy)
+ | init_i (SOME loc) thy = begin loc (Locale.init loc thy);
fun init (SOME "-") thy = init_i NONE thy
| init loc thy = init_i (Option.map (Locale.intern thy) loc) thy;
--- a/src/Pure/Tools/class_package.ML Fri Feb 23 08:39:25 2007 +0100
+++ b/src/Pure/Tools/class_package.ML Fri Feb 23 08:39:26 2007 +0100
@@ -7,7 +7,7 @@
signature CLASS_PACKAGE =
sig
- val fork_mixfix: bool -> bool -> mixfix -> mixfix * mixfix
+ val fork_mixfix: bool -> string option -> mixfix -> mixfix * mixfix
val class: bstring -> class list -> Element.context_i Locale.element list -> theory ->
string * Proof.context
@@ -44,12 +44,12 @@
(** auxiliary **)
-fun fork_mixfix is_class is_loc mx =
+fun fork_mixfix is_loc some_class mx =
let
val mx' = Syntax.unlocalize_mixfix mx;
- val mx1 = if is_class orelse (is_loc andalso mx = mx') then NoSyn else mx';
- val mx2 = if is_loc then mx else NoSyn;
- in (mx1, mx2) end;
+ val mx_global = if is_some some_class orelse (is_loc andalso mx = mx') then NoSyn else mx';
+ val mx_local = if is_loc then mx else NoSyn;
+ in (mx_global, mx_local) end;
(** AxClasses with implicit parameter handling **)
@@ -100,7 +100,7 @@
#-> (fn axioms_prop => AxClass.define_class_i (name, superclasses) (map fst cs) axioms_prop
#-> (fn class => `(fn thy => AxClass.get_definition thy class)
#-> (fn {intro, axioms, ...} => fold (add_constraint class) cs
- #> pair (class, ((intro, (maps snd axioms_prop, axioms)), cs))))))
+ #> pair (class, ((intro, (map Thm.prop_of axioms, axioms)), cs))))))
end;
@@ -471,7 +471,7 @@
in
(map (fst o fst) params, params
|> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (AxClass.param_tyvarname, Sign.defaultS thy)))
- |> (map o apsnd) (fork_mixfix false true #> fst)
+ |> (map o apsnd) (fork_mixfix true NONE #> fst)
|> chop (length supconsts)
|> snd)
end;
@@ -501,7 +501,7 @@
fun make_witness t thm = Element.make_witness t (Goal.protect thm);
in
thy
- |> add_locale bname supexpr ((*elems_constrains @*) elems)
+ |> add_locale (SOME (bname ^ "_pred")) bname supexpr ((*elems_constrains @*) elems)
|-> (fn name_locale => ProofContext.theory_result (
`(fn thy => extract_params thy name_locale)
#-> (fn (param_names, params) =>
@@ -513,7 +513,7 @@
(name_locale, map (fst o fst) params ~~ map fst consts,
map2 make_witness ax_terms ax_axioms, axiom_names))
#> prove_interpretation ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
- (Logic.const_of_class bname, []) (Locale.Locale name_locale)
+ ((true, Logic.const_of_class bname), []) (Locale.Locale name_locale)
(mk_instT name_axclass, mk_inst name_axclass param_names (map snd supconsts @ consts))
#> pair name_axclass
)))))
@@ -521,8 +521,8 @@
in
-val class_cmd = gen_class (Locale.add_locale true) read_class;
-val class = gen_class (Locale.add_locale_i true) certify_class;
+val class_cmd = gen_class Locale.add_locale read_class;
+val class = gen_class Locale.add_locale_i certify_class;
end; (*local*)
@@ -558,11 +558,24 @@
(** experimental class target **)
-fun add_def_in_class lthy loc ((c, syn), ((name, atts), (rhs, eq))) thy =
+fun print_witness wit =
let
- val SOME class = class_of_locale thy loc;
+ val (t, thm) = Element.dest_witness wit;
+ val prop = Thm.prop_of thm;
+ fun string_of_tfree (v, sort) = v ^ "::" ^ Display.raw_string_of_sort sort;
+ fun string_of_tvar (v, sort) = Library.string_of_indexname v ^ "::" ^ Display.raw_string_of_sort sort;
+ fun print_term t =
+ let
+ val term = Display.raw_string_of_term t;
+ val tfrees = map string_of_tfree (Term.add_tfrees t []);
+ val tvars = map string_of_tvar (Term.add_tvars t []);
+ in term :: tfrees @ tvars end;
+ in (map Output.info (print_term t); map Output.info (print_term prop)) end;
+
+fun add_def_in_class lthy class ((c, syn), ((name, atts), (rhs, eq))) thy =
+ let
val rhs' = global_term thy [class] rhs;
- val (syn', _) = fork_mixfix true true syn;
+ val (syn', _) = fork_mixfix true NONE syn;
val ty = Term.fastype_of rhs';
fun add_const (c, ty, syn) =
Sign.add_consts_authentic [(c, ty, syn)]
@@ -581,7 +594,9 @@
val witness = the_witness thy class;
val _ = Output.info "------ WIT ------";
fun print_wit (t, thm) = "(" ^ Sign.string_of_term thy t ^ ", " ^ Display.string_of_thm thm ^ ")"
+ fun print_raw_wit (t, thm) = "(" ^ Display.raw_string_of_term t ^ ", " ^ (Display.raw_string_of_term o Thm.prop_of) thm ^ ")"
val _ = (Output.info o cat_lines o map (print_wit o Element.dest_witness)) witness;
+ val _ = map print_witness witness;
val _ = (Output.info o string_of_thm) eq';
val eq'' = Element.satisfy_thm witness eq';
val _ = (Output.info o string_of_thm) eq'';*)