src/Pure/Isar/theory_target.ML
changeset 25053 2b86fac03ec5
parent 25040 4e54c5ae6852
child 25064 c6664770ef6c
equal deleted inserted replaced
25052:a014d544f54d 25053:2b86fac03ec5
   159   end;
   159   end;
   160 
   160 
   161 
   161 
   162 (* consts *)
   162 (* consts *)
   163 
   163 
   164 fun target_abbrev prmode ((c, mx), rhs) phi =
   164 fun locale_const (prmode as (mode, _)) pos ((c, mx), rhs) phi =
   165   let
   165   let
   166     val c' = Morphism.name phi c;
   166     val c' = Morphism.name phi c;
   167     val rhs' = Morphism.term phi rhs;
   167     val rhs' = Morphism.term phi rhs;
   168     val arg' = (c', rhs');
   168     val legacy_arg = (c', Term.close_schematic_term (Logic.legacy_varify rhs'));
   169     val eq_heads =
   169     val arg = (c', Term.close_schematic_term rhs');
   170       (case pairself Term.head_of (rhs, rhs') of
   170   in
   171         (Const (a, _), Const (a', _)) => a = a'
   171     Context.mapping_result
   172       | _ => false);
   172       (Sign.add_abbrev Syntax.internalM pos legacy_arg)
   173   in
   173       (ProofContext.add_abbrev Syntax.internalM pos arg)
   174     eq_heads ? (Context.mapping_result
   174     #-> (fn (lhs' as Const (d, _), _) =>
   175         (Sign.add_abbrev Syntax.internalM [] arg')
       
   176         (ProofContext.add_abbrev Syntax.internalM [] arg')
       
   177       #-> (fn (lhs, _) =>
       
   178         Type.similar_types (rhs, rhs') ?
   175         Type.similar_types (rhs, rhs') ?
   179           Morphism.form (ProofContext.target_notation true prmode [(lhs, mx)])))
   176           (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
   180   end;
   177            Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)])))
   181 
   178   end;
   182 fun internal_abbrev ta prmode ((c, mx), t) lthy = lthy
       
   183   (* FIXME really permissive *)
       
   184   |> term_syntax ta (perhaps o try o target_abbrev prmode ((c, mx), t))
       
   185   |> ProofContext.add_abbrev Syntax.internalM (ContextPosition.properties_of lthy) (c, t)
       
   186   |> snd;
       
   187 
   179 
   188 fun declare_consts (ta as Target {target, is_locale, is_class}) depends decls lthy =
   180 fun declare_consts (ta as Target {target, is_locale, is_class}) depends decls lthy =
   189   let
   181   let
       
   182     val pos = ContextPosition.properties_of lthy;
   190     val thy = ProofContext.theory_of lthy;
   183     val thy = ProofContext.theory_of lthy;
   191     val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
   184     val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
   192 
   185 
   193     fun const ((c, T), mx) thy =
   186     fun const ((c, T), mx) thy =
   194       let
   187       let
   195         val U = map #2 xs ---> T;
   188         val U = map #2 xs ---> T;
   196         val (mx1, mx2) = Class.fork_mixfix is_locale is_class mx;
   189         val (mx1, mx2) = Class.fork_mixfix is_locale is_class mx;
   197         val mx3 = if is_locale then NoSyn else mx1;
   190         val mx3 = if is_locale then NoSyn else mx1;
   198         val (const, thy') = Sign.declare_const (ContextPosition.properties_of lthy) (c, U, mx3) thy;
   191         val (const, thy') = Sign.declare_const pos (c, U, mx3) thy;
   199         val t = Term.list_comb (const, map Free xs);
   192         val t = Term.list_comb (const, map Free xs);
   200       in (((c, mx2), t), thy') end;
   193       in (((c, mx2), t), thy') end;
   201     val local_const = NameSpace.full (LocalTheory.target_naming lthy);
   194     val local_const = NameSpace.full (LocalTheory.target_naming lthy);
   202     fun class_const ((c, _), mx) (_, t) =
   195     fun class_const ((c, _), mx) (_, t) =
   203       LocalTheory.raw_theory_result (Class.add_const_in_class target ((c, mx), (local_const c, t)))
   196       LocalTheory.raw_theory_result (Class.add_const_in_class target ((c, mx), (local_const c, t)))
   205 
   198 
   206     val (abbrs, lthy') = lthy
   199     val (abbrs, lthy') = lthy
   207       |> LocalTheory.theory_result (fold_map const decls)
   200       |> LocalTheory.theory_result (fold_map const decls)
   208   in
   201   in
   209     lthy'
   202     lthy'
   210     |> is_locale ? fold (internal_abbrev ta Syntax.mode_default) abbrs
   203     |> is_locale ? fold (term_syntax ta o locale_const Syntax.mode_default pos) abbrs
   211     |> is_class ? fold2 class_const decls abbrs
   204     |> is_class ? fold2 class_const decls abbrs
   212     |> fold_map (apfst (apsnd snd) oo LocalDefs.add_def) abbrs
   205     |> fold_map (apfst (apsnd snd) oo LocalDefs.add_def) abbrs
   213   end;
   206   end;
   214 
   207 
   215 
   208 
   216 (* abbrev *)
   209 (* abbrev *)
   217 
   210 
       
   211 local
       
   212 
       
   213 fun context_abbrev pos (c, t) lthy = lthy
       
   214   |> ProofContext.add_abbrev Syntax.internalM pos (c, t) |> snd
       
   215   |> LocalDefs.add_def ((c, NoSyn), t);
       
   216 
       
   217 fun class_abbrev target prmode ((c, mx), rhs) lthy = lthy   (* FIXME pos *)
       
   218   |> LocalTheory.raw_theory_result (Class.add_abbrev_in_class target prmode
       
   219       ((c, mx), (NameSpace.full (LocalTheory.target_naming lthy) c, rhs)))
       
   220   |-> Class.remove_constraint target;
       
   221 
       
   222 in
       
   223 
   218 fun abbrev (ta as Target {target, is_locale, is_class}) prmode ((raw_c, mx), raw_t) lthy =
   224 fun abbrev (ta as Target {target, is_locale, is_class}) prmode ((raw_c, mx), raw_t) lthy =
   219   let
   225   let
   220     val thy = ProofContext.theory_of lthy;
   226     val pos = ContextPosition.properties_of lthy;
   221     val thy_ctxt = ProofContext.init thy;
   227     val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
   222     val target_ctxt = LocalTheory.target_of lthy;
   228     val target_ctxt = LocalTheory.target_of lthy;
   223     val target_morphism = LocalTheory.target_morphism lthy;
   229     val target_morphism = LocalTheory.target_morphism lthy;
   224 
       
   225     val c = Morphism.name target_morphism raw_c;
   230     val c = Morphism.name target_morphism raw_c;
   226     val t = Morphism.term target_morphism raw_t;
   231     val t = Morphism.term target_morphism raw_t;
   227     val xs = map Free (Variable.add_fixed target_ctxt t []);
   232 
   228     val u = fold_rev lambda xs t;
   233     val xs = map Free (rev (Variable.add_fixed target_ctxt t []));
   229     val U = Term.fastype_of u;
   234     val global_rhs =
   230     val u' = singleton (Variable.export_terms (Variable.declare_term u target_ctxt) thy_ctxt) u;
   235       singleton (Variable.export_terms (Variable.declare_term t target_ctxt) thy_ctxt)
       
   236         (fold_rev lambda xs t);
   231     val (mx1, mx2) = Class.fork_mixfix is_locale is_class mx;
   237     val (mx1, mx2) = Class.fork_mixfix is_locale is_class mx;
   232     val mx3 = if is_locale then NoSyn else mx1;
   238   in
   233 
   239     if is_locale then
   234     val local_const = NameSpace.full (LocalTheory.target_naming lthy);
   240       lthy
   235     fun class_abbrev ((c, mx), t) =
   241       |> LocalTheory.theory_result (Sign.add_abbrev Syntax.internalM pos (c, global_rhs))
   236       LocalTheory.raw_theory_result (Class.add_abbrev_in_class target prmode
   242       |-> (fn (lhs, _) =>
   237         ((c, mx), (local_const c, t)))
   243         let val lhs' = Term.list_comb (Logic.unvarify lhs, xs) in
   238       #-> Class.remove_constraint target;
   244           term_syntax ta (locale_const prmode pos ((c, mx2), lhs')) #>
   239   in
   245           is_class ? class_abbrev target prmode ((c, mx1), lhs')
   240     lthy
   246         end)
   241     |> LocalTheory.theory_result
   247       |> context_abbrev pos (c, raw_t)
   242         (Sign.add_abbrev (#1 prmode) (ContextPosition.properties_of lthy) (c, u'))
   248     else
   243     |-> (fn (lhs, rhs) =>
   249       lthy
   244           LocalTheory.theory (Sign.notation true prmode [(lhs, mx3)])
   250       |> LocalTheory.theory
   245           #> is_locale ? internal_abbrev ta prmode ((c, mx2), Term.list_comb (lhs, xs))
   251         (Sign.add_abbrev (#1 prmode) pos (c, global_rhs)
   246           #> is_class ? class_abbrev ((c, mx1), Term.list_comb (lhs, xs)))
   252           #-> (fn (lhs, _) => Sign.notation true prmode [(lhs, mx1)]))
   247     |> LocalDefs.add_def ((c, NoSyn), raw_t)
   253       |> context_abbrev pos (c, raw_t)
   248   end;
   254   end;
       
   255 
       
   256 end;
   249 
   257 
   250 
   258 
   251 (* define *)
   259 (* define *)
   252 
   260 
   253 fun define (ta as Target {target, is_locale, is_class})
   261 fun define (ta as Target {target, is_locale, is_class})