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