misc cleanup of abbrev/local_const;
authorwenzelm
Tue Oct 16 17:06:19 2007 +0200 (2007-10-16)
changeset 250532b86fac03ec5
parent 25052 a014d544f54d
child 25054 b15a9a5dc9fe
misc cleanup of abbrev/local_const;
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Tue Oct 16 17:06:18 2007 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Tue Oct 16 17:06:19 2007 +0200
     1.3 @@ -161,32 +161,25 @@
     1.4  
     1.5  (* consts *)
     1.6  
     1.7 -fun target_abbrev prmode ((c, mx), rhs) phi =
     1.8 +fun locale_const (prmode as (mode, _)) pos ((c, mx), rhs) phi =
     1.9    let
    1.10      val c' = Morphism.name phi c;
    1.11      val rhs' = Morphism.term phi rhs;
    1.12 -    val arg' = (c', rhs');
    1.13 -    val eq_heads =
    1.14 -      (case pairself Term.head_of (rhs, rhs') of
    1.15 -        (Const (a, _), Const (a', _)) => a = a'
    1.16 -      | _ => false);
    1.17 +    val legacy_arg = (c', Term.close_schematic_term (Logic.legacy_varify rhs'));
    1.18 +    val arg = (c', Term.close_schematic_term rhs');
    1.19    in
    1.20 -    eq_heads ? (Context.mapping_result
    1.21 -        (Sign.add_abbrev Syntax.internalM [] arg')
    1.22 -        (ProofContext.add_abbrev Syntax.internalM [] arg')
    1.23 -      #-> (fn (lhs, _) =>
    1.24 +    Context.mapping_result
    1.25 +      (Sign.add_abbrev Syntax.internalM pos legacy_arg)
    1.26 +      (ProofContext.add_abbrev Syntax.internalM pos arg)
    1.27 +    #-> (fn (lhs' as Const (d, _), _) =>
    1.28          Type.similar_types (rhs, rhs') ?
    1.29 -          Morphism.form (ProofContext.target_notation true prmode [(lhs, mx)])))
    1.30 +          (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
    1.31 +           Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)])))
    1.32    end;
    1.33  
    1.34 -fun internal_abbrev ta prmode ((c, mx), t) lthy = lthy
    1.35 -  (* FIXME really permissive *)
    1.36 -  |> term_syntax ta (perhaps o try o target_abbrev prmode ((c, mx), t))
    1.37 -  |> ProofContext.add_abbrev Syntax.internalM (ContextPosition.properties_of lthy) (c, t)
    1.38 -  |> snd;
    1.39 -
    1.40  fun declare_consts (ta as Target {target, is_locale, is_class}) depends decls lthy =
    1.41    let
    1.42 +    val pos = ContextPosition.properties_of lthy;
    1.43      val thy = ProofContext.theory_of lthy;
    1.44      val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
    1.45  
    1.46 @@ -195,7 +188,7 @@
    1.47          val U = map #2 xs ---> T;
    1.48          val (mx1, mx2) = Class.fork_mixfix is_locale is_class mx;
    1.49          val mx3 = if is_locale then NoSyn else mx1;
    1.50 -        val (const, thy') = Sign.declare_const (ContextPosition.properties_of lthy) (c, U, mx3) thy;
    1.51 +        val (const, thy') = Sign.declare_const pos (c, U, mx3) thy;
    1.52          val t = Term.list_comb (const, map Free xs);
    1.53        in (((c, mx2), t), thy') end;
    1.54      val local_const = NameSpace.full (LocalTheory.target_naming lthy);
    1.55 @@ -207,7 +200,7 @@
    1.56        |> LocalTheory.theory_result (fold_map const decls)
    1.57    in
    1.58      lthy'
    1.59 -    |> is_locale ? fold (internal_abbrev ta Syntax.mode_default) abbrs
    1.60 +    |> is_locale ? fold (term_syntax ta o locale_const Syntax.mode_default pos) abbrs
    1.61      |> is_class ? fold2 class_const decls abbrs
    1.62      |> fold_map (apfst (apsnd snd) oo LocalDefs.add_def) abbrs
    1.63    end;
    1.64 @@ -215,38 +208,53 @@
    1.65  
    1.66  (* abbrev *)
    1.67  
    1.68 +local
    1.69 +
    1.70 +fun context_abbrev pos (c, t) lthy = lthy
    1.71 +  |> ProofContext.add_abbrev Syntax.internalM pos (c, t) |> snd
    1.72 +  |> LocalDefs.add_def ((c, NoSyn), t);
    1.73 +
    1.74 +fun class_abbrev target prmode ((c, mx), rhs) lthy = lthy   (* FIXME pos *)
    1.75 +  |> LocalTheory.raw_theory_result (Class.add_abbrev_in_class target prmode
    1.76 +      ((c, mx), (NameSpace.full (LocalTheory.target_naming lthy) c, rhs)))
    1.77 +  |-> Class.remove_constraint target;
    1.78 +
    1.79 +in
    1.80 +
    1.81  fun abbrev (ta as Target {target, is_locale, is_class}) prmode ((raw_c, mx), raw_t) lthy =
    1.82    let
    1.83 -    val thy = ProofContext.theory_of lthy;
    1.84 -    val thy_ctxt = ProofContext.init thy;
    1.85 +    val pos = ContextPosition.properties_of lthy;
    1.86 +    val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
    1.87      val target_ctxt = LocalTheory.target_of lthy;
    1.88      val target_morphism = LocalTheory.target_morphism lthy;
    1.89 -
    1.90      val c = Morphism.name target_morphism raw_c;
    1.91      val t = Morphism.term target_morphism raw_t;
    1.92 -    val xs = map Free (Variable.add_fixed target_ctxt t []);
    1.93 -    val u = fold_rev lambda xs t;
    1.94 -    val U = Term.fastype_of u;
    1.95 -    val u' = singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u;
    1.96 -    val (mx1, mx2) = Class.fork_mixfix is_locale is_class mx;
    1.97 -    val mx3 = if is_locale then NoSyn else mx1;
    1.98  
    1.99 -    val local_const = NameSpace.full (LocalTheory.target_naming lthy);
   1.100 -    fun class_abbrev ((c, mx), t) =
   1.101 -      LocalTheory.raw_theory_result (Class.add_abbrev_in_class target prmode
   1.102 -        ((c, mx), (local_const c, t)))
   1.103 -      #-> Class.remove_constraint target;
   1.104 +    val xs = map Free (rev (Variable.add_fixed target_ctxt t []));
   1.105 +    val global_rhs =
   1.106 +      singleton (Variable.export_terms (Variable.declare_term t target_ctxt) thy_ctxt)
   1.107 +        (fold_rev lambda xs t);
   1.108 +    val (mx1, mx2) = Class.fork_mixfix is_locale is_class mx;
   1.109    in
   1.110 -    lthy
   1.111 -    |> LocalTheory.theory_result
   1.112 -        (Sign.add_abbrev (#1 prmode) (ContextPosition.properties_of lthy) (c, u'))
   1.113 -    |-> (fn (lhs, rhs) =>
   1.114 -          LocalTheory.theory (Sign.notation true prmode [(lhs, mx3)])
   1.115 -          #> is_locale ? internal_abbrev ta prmode ((c, mx2), Term.list_comb (lhs, xs))
   1.116 -          #> is_class ? class_abbrev ((c, mx1), Term.list_comb (lhs, xs)))
   1.117 -    |> LocalDefs.add_def ((c, NoSyn), raw_t)
   1.118 +    if is_locale then
   1.119 +      lthy
   1.120 +      |> LocalTheory.theory_result (Sign.add_abbrev Syntax.internalM pos (c, global_rhs))
   1.121 +      |-> (fn (lhs, _) =>
   1.122 +        let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
   1.123 +          term_syntax ta (locale_const prmode pos ((c, mx2), lhs')) #>
   1.124 +          is_class ? class_abbrev target prmode ((c, mx1), lhs')
   1.125 +        end)
   1.126 +      |> context_abbrev pos (c, raw_t)
   1.127 +    else
   1.128 +      lthy
   1.129 +      |> LocalTheory.theory
   1.130 +        (Sign.add_abbrev (#1 prmode) pos (c, global_rhs)
   1.131 +          #-> (fn (lhs, _) => Sign.notation true prmode [(lhs, mx1)]))
   1.132 +      |> context_abbrev pos (c, raw_t)
   1.133    end;
   1.134  
   1.135 +end;
   1.136 +
   1.137  
   1.138  (* define *)
   1.139