tuned abbreviations in class context
authorhaftmann
Mon Oct 22 16:54:52 2007 +0200 (2007-10-22)
changeset 25146c2a41f31cacb
parent 25145 d432105e5bd0
child 25147 85463aff6dbe
tuned abbreviations in class context
src/Pure/Isar/class.ML
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/class.ML	Mon Oct 22 16:54:50 2007 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Mon Oct 22 16:54:52 2007 +0200
     1.3 @@ -315,9 +315,9 @@
     1.4      (*partial morphism of canonical interpretation*)
     1.5    intro: thm,
     1.6    defs: thm list,
     1.7 -  operations: (string * (((term * typ) * (typ * int)) * term)) list
     1.8 -    (*constant name ~> ((locale term & typ,
     1.9 -        (constant constraint, instantiaton index of class typ)), locale term for uncheck)*)
    1.10 +  operations: (string * ((term * (typ * int)) * (term * typ))) list
    1.11 +    (*constant name ~> ((locale term,
    1.12 +        (constant constraint, instantiaton index of class typ)), locale term & typ for uncheck)*)
    1.13  };
    1.14  
    1.15  fun rep_class_data (ClassData d) = d;
    1.16 @@ -439,7 +439,7 @@
    1.17        (SOME o the o Symtab.lookup insttab o fst o fst)
    1.18          (Locale.parameters_of_expr thy (Locale.Locale class));
    1.19      val operations = map (fn (v_ty as (_, ty'), (c, ty)) =>
    1.20 -      (c, (((Free v_ty, ty'), (Logic.varifyT ty, 0)), Free v_ty))) cs;
    1.21 +      (c, ((Free v_ty, (Logic.varifyT ty, 0)), (Free v_ty, ty')))) cs;
    1.22      val cs = (map o pairself) fst cs;
    1.23      val add_class = Graph.new_node (class,
    1.24          mk_class_data ((cs, base_sort, inst, phi, intro), ([], operations)))
    1.25 @@ -448,18 +448,20 @@
    1.26      ClassData.map add_class thy
    1.27    end;
    1.28  
    1.29 -fun register_operation class ((c, (dict, dict_rev)), some_def) thy =
    1.30 +fun register_operation class ((c, (t, t_rev)), some_def) thy =
    1.31    let
    1.32      val ty = Sign.the_const_constraint thy c;
    1.33      val typargs = Sign.const_typargs thy (c, ty);
    1.34      val typidx = find_index (fn TVar ((v, _), _) => Name.aT = v | _ => false) typargs;
    1.35 -    val ty' = Term.fastype_of dict;
    1.36 +    val t_rev' = (map_types o map_atyps)
    1.37 +      (fn ty as TFree (v, _) => if Name.aT = v then TFree (v, []) else ty | ty => ty) t_rev;
    1.38 +    val ty' = Term.fastype_of t_rev';
    1.39    in
    1.40      thy
    1.41      |> (ClassData.map o Graph.map_node class o map_class_data o apsnd)
    1.42        (fn (defs, operations) =>
    1.43          (fold cons (the_list some_def) defs,
    1.44 -          (c, (((dict, ty'), (ty, typidx)), dict_rev)) :: operations))
    1.45 +          (c, ((t, (ty, typidx)), (t_rev', ty'))) :: operations))
    1.46    end;
    1.47  
    1.48  
    1.49 @@ -583,17 +585,13 @@
    1.50  
    1.51      (* check phase *)
    1.52      val typargs = Consts.typargs (ProofContext.consts_of ctxt);
    1.53 -    fun check_const (c, ty) (((t, _), (_, idx)), _) =
    1.54 +    fun check_const (c, ty) ((t, (_, idx)), _) =
    1.55        ((nth (typargs (c, ty)) idx), t);
    1.56      fun local_operation (c_ty as (c, _)) = AList.lookup (op =) operations c
    1.57        |> Option.map (check_const c_ty);
    1.58  
    1.59      (* uncheck phase *)
    1.60 -    val proto_rews = map (fn (c, (((t, ty), _), _)) => (t, Const (c, ty))) operations;
    1.61 -    fun rew_app f (t1 $ t2) = rew_app f t1 $ f t2
    1.62 -      | rew_app f t = t;
    1.63 -    val rews = (map o apfst o rew_app)
    1.64 -      (Pattern.rewrite_term thy proto_rews []) proto_rews;
    1.65 +    val rews = map (fn (c, (_, (t, ty))) => (t, Const (c, ty))) operations;
    1.66    in
    1.67      ctxt
    1.68      |> fold (ProofContext.add_const_constraint o local_constraint) operations
    1.69 @@ -832,23 +830,6 @@
    1.70  
    1.71  (* abbreviation in class target *)
    1.72  
    1.73 -fun expand_aux_abbrev thy class t =
    1.74 -  let
    1.75 -    val rews = map (Logic.dest_equals o Thm.prop_of) (these_defs thy [class]);
    1.76 -    val (head, ts) = strip_comb t;
    1.77 -    val tys = (fst o chop (length ts) o fst o strip_type o Term.fastype_of) head;
    1.78 -    val head' = head
    1.79 -      |> Pattern.eta_long tys
    1.80 -      |> Consts.certify (Sign.pp thy) (Sign.tsig_of thy) true (Sign.consts_of thy);
    1.81 -    val ts' = ts
    1.82 -      |> map (Pattern.rewrite_term thy rews []);
    1.83 -  in Term.betapplys (head', ts') end;
    1.84 -
    1.85 -fun fold_aux_defs thy class =
    1.86 -  let
    1.87 -    val rews = map (Logic.dest_equals o Thm.prop_of) (these_defs thy [class])
    1.88 -  in Pattern.rewrite_term thy rews [] end;
    1.89 -
    1.90  fun add_syntactic_const class prmode pos ((c, mx), rhs) thy =
    1.91    let
    1.92      val prfx = class_prefix class;
    1.93 @@ -856,9 +837,10 @@
    1.94      val phi = morphism thy class;
    1.95  
    1.96      val c' = Sign.full_name thy' c;
    1.97 -    val dict' = (expand_aux_abbrev thy' class o Morphism.term phi) rhs;
    1.98 -    val dict'' = map_types Logic.unvarifyT dict';
    1.99 -    val ty' = Term.fastype_of dict'';
   1.100 +    val rews = map (Logic.dest_equals o Thm.prop_of) (these_defs thy' [class])
   1.101 +    val rhs' = (Pattern.rewrite_term thy rews [] o Morphism.term phi) rhs;
   1.102 +    val rhs'' = map_types Logic.unvarifyT rhs';
   1.103 +    val ty' = Term.fastype_of rhs'';
   1.104  
   1.105      val c'' = NameSpace.full (Sign.naming_of thy' |> NameSpace.add_path prfx) c;
   1.106      val ty'' = (Type.strip_sorts o Logic.unvarifyT) (Sign.the_const_constraint thy' c'');
   1.107 @@ -866,10 +848,10 @@
   1.108      thy'
   1.109      |> Sign.add_const_constraint (c'', SOME ty'') (*FIXME*)
   1.110      |> Sign.hide_consts_i false [c''] (*FIXME*)
   1.111 -    |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts dict') |> snd
   1.112 +    |> Sign.add_abbrev (#1 prmode) pos (c, map_types Type.strip_sorts rhs') |> snd
   1.113      |> Sign.add_const_constraint (c', SOME ty')
   1.114      |> Sign.notation true prmode [(Const (c', ty'), mx)]
   1.115 -    |> register_operation class ((c', (dict', dict'')), NONE)
   1.116 +    |> register_operation class ((c', (rhs, rhs'')), NONE)
   1.117      |> Sign.restore_naming thy
   1.118    end;
   1.119  
     2.1 --- a/src/Pure/Isar/theory_target.ML	Mon Oct 22 16:54:50 2007 +0200
     2.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Oct 22 16:54:52 2007 +0200
     2.3 @@ -215,6 +215,7 @@
     2.4      val u = fold_rev lambda xs t';
     2.5      val global_rhs =
     2.6        singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u;
     2.7 +    val class_t = Morphism.term (LocalTheory.target_morphism lthy) t;
     2.8    in
     2.9      lthy |>
    2.10       (if is_locale then
    2.11 @@ -223,7 +224,7 @@
    2.12            let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
    2.13              term_syntax ta (locale_const prmode pos ((c, mx2), lhs')) #>
    2.14              is_class ?
    2.15 -              class_target ta (Class.add_syntactic_const target prmode pos ((c, mx1), lhs'))
    2.16 +              class_target ta (Class.add_syntactic_const target prmode pos ((c, mx1), class_t))
    2.17            end)
    2.18        else
    2.19          LocalTheory.theory