1.1 --- a/src/Pure/Isar/class.ML Fri Oct 19 12:22:12 2007 +0200
1.2 +++ b/src/Pure/Isar/class.ML Fri Oct 19 15:08:33 2007 +0200
1.3 @@ -19,10 +19,10 @@
1.4 val is_class: theory -> class -> bool
1.5 val these_params: theory -> sort -> (string * (string * typ)) list
1.6 val init: class -> Proof.context -> Proof.context
1.7 - val add_logical_const: string -> (string * mixfix) * term
1.8 - -> theory -> string * theory
1.9 - val add_syntactic_const: string -> Syntax.mode -> (string * mixfix) * term
1.10 - -> theory -> string * theory
1.11 + val add_logical_const: string -> Markup.property list
1.12 + -> (string * mixfix) * term -> theory -> string * theory
1.13 + val add_syntactic_const: string -> Syntax.mode -> Markup.property list
1.14 + -> (string * mixfix) * term -> theory -> string * theory
1.15 val refresh_syntax: class -> Proof.context -> Proof.context
1.16 val intro_classes_tac: thm list -> tactic
1.17 val default_intro_classes_tac: thm list -> tactic
1.18 @@ -315,9 +315,9 @@
1.19 (*partial morphism of canonical interpretation*)
1.20 intro: thm,
1.21 defs: thm list,
1.22 - operations: (string * ((term * typ) * (typ * int))) list
1.23 - (*constant name ~> (locale term & typ,
1.24 - (constant constraint, instantiaton index of class typ))*)
1.25 + operations: (string * (((term * typ) * (typ * int)) * term)) list
1.26 + (*constant name ~> ((locale term & typ,
1.27 + (constant constraint, instantiaton index of class typ)), locale term for uncheck)*)
1.28 };
1.29
1.30 fun rep_class_data (ClassData d) = d;
1.31 @@ -439,7 +439,7 @@
1.32 (SOME o the o Symtab.lookup insttab o fst o fst)
1.33 (Locale.parameters_of_expr thy (Locale.Locale class));
1.34 val operations = map (fn (v_ty as (_, ty'), (c, ty)) =>
1.35 - (c, ((Free v_ty, ty'), (Logic.varifyT ty, 0)))) cs;
1.36 + (c, (((Free v_ty, ty'), (Logic.varifyT ty, 0)), Free v_ty))) cs;
1.37 val cs = (map o pairself) fst cs;
1.38 val add_class = Graph.new_node (class,
1.39 mk_class_data ((cs, base_sort, inst, phi, intro), ([], operations)))
1.40 @@ -448,18 +448,18 @@
1.41 ClassData.map add_class thy
1.42 end;
1.43
1.44 -fun register_operation class ((c, rhs), some_def) thy =
1.45 +fun register_operation class ((c, (dict, dict_rev)), some_def) thy =
1.46 let
1.47 val ty = Sign.the_const_constraint thy c;
1.48 val typargs = Sign.const_typargs thy (c, ty);
1.49 val typidx = find_index (fn TVar ((v, _), _) => Name.aT = v | _ => false) typargs;
1.50 - val ty' = Term.fastype_of rhs;
1.51 + val ty' = Term.fastype_of dict;
1.52 in
1.53 thy
1.54 |> (ClassData.map o Graph.map_node class o map_class_data o apsnd)
1.55 (fn (defs, operations) =>
1.56 - (case some_def of NONE => defs | SOME def => def :: defs,
1.57 - (c, ((rhs, ty'), (ty, typidx))) :: operations))
1.58 + (fold cons (the_list some_def) defs,
1.59 + (c, (((dict, ty'), (ty, typidx)), dict_rev)) :: operations))
1.60 end;
1.61
1.62
1.63 @@ -572,24 +572,24 @@
1.64 val operations = these_operations thy sups;
1.65
1.66 (* constraints *)
1.67 - fun local_constraint (c, (_, (ty, _))) =
1.68 + fun local_constraint (c, ((_, (ty, _)),_ )) =
1.69 let
1.70 val ty' = ty
1.71 |> map_atyps (fn ty as TVar ((v, 0), _) =>
1.72 if v = Name.aT then TVar ((v, 0), base_sort) else ty)
1.73 |> SOME;
1.74 in (c, ty') end
1.75 - val constraints = (map o apsnd) (fst o snd) operations;
1.76 + val constraints = (map o apsnd) (fst o snd o fst) operations;
1.77
1.78 (* check phase *)
1.79 val typargs = Consts.typargs (ProofContext.consts_of ctxt);
1.80 - fun check_const (c, ty) ((t, _), (_, idx)) =
1.81 + fun check_const (c, ty) (((t, _), (_, idx)), _) =
1.82 ((nth (typargs (c, ty)) idx), t);
1.83 fun local_operation (c_ty as (c, _)) = AList.lookup (op =) operations c
1.84 |> Option.map (check_const c_ty);
1.85
1.86 (* uncheck phase *)
1.87 - val proto_rews = map (fn (c, ((t, ty), _)) => (t, Const (c, ty))) operations;
1.88 + val proto_rews = map (fn (c, (((t, ty), _), _)) => (t, Const (c, ty))) operations;
1.89 fun rew_app f (t1 $ t2) = rew_app f t1 $ f t2
1.90 | rew_app f t = t;
1.91 val rews = (map o apfst o rew_app)
1.92 @@ -804,7 +804,7 @@
1.93
1.94 (* definition in class target *)
1.95
1.96 -fun add_logical_const class ((c, mx), dict) thy =
1.97 +fun add_logical_const class pos ((c, mx), dict) thy =
1.98 let
1.99 val prfx = class_prefix class;
1.100 val thy' = thy |> Sign.add_path prfx;
1.101 @@ -815,17 +815,18 @@
1.102 val ty' = Term.fastype_of dict';
1.103 val ty'' = Type.strip_sorts ty';
1.104 val def_eq = Logic.mk_equals (Const (c', ty'), dict');
1.105 +
1.106 val c'' = NameSpace.full (Sign.naming_of thy' |> NameSpace.add_path prfx) c;
1.107 in
1.108 thy'
1.109 - |> Sign.hide_consts_i false [c'']
1.110 - |> Sign.declare_const [] (c, ty'', mx) |> snd
1.111 + |> Sign.hide_consts_i false [c''] (*FIXME*)
1.112 + |> Sign.declare_const pos (c, ty'', mx) |> snd
1.113 |> Sign.parent_path
1.114 |> Sign.sticky_prefix prfx
1.115 |> Thm.add_def false (c, def_eq)
1.116 |>> Thm.symmetric
1.117 |-> (fn def => class_interpretation class [def] [Thm.prop_of def]
1.118 - #> register_operation class ((c', dict), SOME (Thm.varifyT def)))
1.119 + #> register_operation class ((c', (dict, dict')), SOME (Thm.varifyT def)))
1.120 |> Sign.restore_naming thy
1.121 |> Sign.add_const_constraint (c', SOME ty')
1.122 |> pair c'
1.123 @@ -834,20 +835,40 @@
1.124
1.125 (* abbreviation in class target *)
1.126
1.127 -fun add_syntactic_const class prmode ((c, mx), rhs) thy =
1.128 +fun expand_aux_abbrev thy class t =
1.129 + let
1.130 + val rews = map (Logic.dest_equals o Thm.prop_of) (these_defs thy [class]);
1.131 + val (head, ts) = strip_comb t;
1.132 + val tys = (fst o chop (length ts) o fst o strip_type o Term.fastype_of) head;
1.133 + val head' = head
1.134 + |> Pattern.eta_long tys
1.135 + |> Consts.certify (Sign.pp thy) (Sign.tsig_of thy) true (Sign.consts_of thy);
1.136 + val ts' = ts
1.137 + |> map (Pattern.rewrite_term thy rews []);
1.138 + in Term.betapplys (head', ts') end;
1.139 +
1.140 +fun add_syntactic_const class prmode pos ((c, mx), dict) thy =
1.141 let
1.142 val prfx = class_prefix class;
1.143 + val thy' = thy |> Sign.add_path prfx;
1.144 val phi = morphism thy class;
1.145
1.146 - val naming = Sign.naming_of thy |> NameSpace.add_path prfx |> NameSpace.add_path prfx;
1.147 - (*FIXME*)
1.148 - val c' = NameSpace.full naming c;
1.149 - val rhs' = (map_types Logic.unvarifyT o Morphism.term phi) rhs;
1.150 - val ty' = Term.fastype_of rhs';
1.151 + val c' = Sign.full_name thy' c;
1.152 + val dict' = (expand_aux_abbrev thy' class o Morphism.term phi) dict;
1.153 + val dict'' = map_types Logic.unvarifyT dict';
1.154 + val ty' = Term.fastype_of dict'';
1.155 +
1.156 + val c'' = NameSpace.full (Sign.naming_of thy' |> NameSpace.add_path prfx) c;
1.157 + val ty'' = (Type.strip_sorts o Logic.unvarifyT) (Sign.the_const_constraint thy' c'');
1.158 in
1.159 - thy
1.160 + thy'
1.161 + |> Sign.add_const_constraint (c'', SOME ty'') (*FIXME*)
1.162 + |> Sign.hide_consts_i false [c''] (*FIXME*)
1.163 + |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts dict') |> snd
1.164 + |> Sign.add_const_constraint (c', SOME ty')
1.165 |> Sign.notation true prmode [(Const (c', ty'), mx)]
1.166 - |> register_operation class ((c', rhs), NONE)
1.167 + |> register_operation class ((c', (dict, dict'')), NONE)
1.168 + |> Sign.restore_naming thy
1.169 |> pair c'
1.170 end;
1.171
2.1 --- a/src/Pure/Isar/theory_target.ML Fri Oct 19 12:22:12 2007 +0200
2.2 +++ b/src/Pure/Isar/theory_target.ML Fri Oct 19 15:08:33 2007 +0200
2.3 @@ -195,7 +195,7 @@
2.4 val t = Term.list_comb (const, map Free xs);
2.5 in (((c, mx12), t), thy') end;
2.6 fun class_const ((c, _), _) ((_, (mx1, _)), t) =
2.7 - LocalTheory.raw_theory_result (Class.add_logical_const target ((c, mx1), t))
2.8 + LocalTheory.raw_theory_result (Class.add_logical_const target pos ((c, mx1), t))
2.9 #> snd
2.10 #> LocalTheory.target (Class.refresh_syntax target);
2.11
2.12 @@ -218,9 +218,9 @@
2.13 |> ProofContext.add_abbrev Syntax.internalM pos (c, t) |> snd
2.14 |> LocalDefs.add_def ((c, NoSyn), t);
2.15
2.16 -fun class_abbrev target prmode ((c, mx), rhs) lthy = lthy (* FIXME pos *)
2.17 - |> LocalTheory.raw_theory_result (Class.add_syntactic_const target prmode
2.18 - ((c, mx), rhs))
2.19 +fun class_abbrev target prmode pos ((c, mx), rhs) lthy = lthy
2.20 + |> LocalTheory.raw_theory_result
2.21 + (Class.add_syntactic_const target prmode pos ((c, mx), rhs))
2.22 |> snd
2.23 |> LocalTheory.target (Class.refresh_syntax target);
2.24
2.25 @@ -248,7 +248,7 @@
2.26 |-> (fn (lhs, _) =>
2.27 let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
2.28 term_syntax ta (locale_const prmode pos ((c, mx2), lhs')) #>
2.29 - is_class ? class_abbrev target prmode ((c, mx1), lhs')
2.30 + is_class ? class_abbrev target prmode pos ((c, mx1), lhs')
2.31 end)
2.32 |> context_abbrev pos (c, raw_t)
2.33 else