Make registrations generic data.
authorballarin
Sat Jul 31 21:14:20 2010 +0200 (2010-07-31)
changeset 381073a46cebd7983
parent 38106 d44a5f602b8c
child 38108 b4115423c049
Make registrations generic data.
src/Pure/Isar/class.ML
src/Pure/Isar/class_target.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/locale.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/Pure/Isar/class.ML	Fri Jul 30 15:03:42 2010 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Sat Jul 31 21:14:20 2010 +0200
     1.3 @@ -293,8 +293,8 @@
     1.4      |-> (fn (param_map, params, assm_axiom) =>
     1.5         `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
     1.6      #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) =>
     1.7 -       Locale.add_registration (class, base_morph)
     1.8 -         (Option.map (rpair true) eq_morph) export_morph
     1.9 +       Context.theory_map (Locale.add_registration (class, base_morph)
    1.10 +         (Option.map (rpair true) eq_morph) export_morph)
    1.11      #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
    1.12      |> Theory_Target.init (SOME class)
    1.13      |> pair class
     2.1 --- a/src/Pure/Isar/class_target.ML	Fri Jul 30 15:03:42 2010 +0200
     2.2 +++ b/src/Pure/Isar/class_target.ML	Sat Jul 31 21:14:20 2010 +0200
     2.3 @@ -205,8 +205,8 @@
     2.4  
     2.5  fun activate_defs class thms thy = case Element.eq_morphism thy thms
     2.6   of SOME eq_morph => fold (fn cls => fn thy =>
     2.7 -      Locale.amend_registration (cls, base_morphism thy cls)
     2.8 -        (eq_morph, true) (export_morphism thy cls) thy) (heritage thy [class]) thy
     2.9 +      Context.theory_map (Locale.amend_registration (cls, base_morphism thy cls)
    2.10 +        (eq_morph, true) (export_morphism thy cls)) thy) (heritage thy [class]) thy
    2.11    | NONE => thy;
    2.12  
    2.13  fun register_operation class (c, (t, some_def)) thy =
     3.1 --- a/src/Pure/Isar/expression.ML	Fri Jul 30 15:03:42 2010 +0200
     3.2 +++ b/src/Pure/Isar/expression.ML	Sat Jul 31 21:14:20 2010 +0200
     3.3 @@ -821,10 +821,11 @@
     3.4  
     3.5      fun after_qed witss eqns = ProofContext.theory (note_eqns eqns
     3.6        #-> (fn eqns => fold (fn ((dep, morph), wits) =>
     3.7 -        fn thy => Locale.add_registration (dep, morph $> Element.satisfy_morphism
     3.8 -            (map (Element.morph_witness export') wits))
     3.9 -          (Element.eq_morphism thy eqns |> Option.map (rpair true))
    3.10 -          export thy) (deps ~~ witss)));
    3.11 +        fn thy => Context.theory_map
    3.12 +          (Locale.add_registration (dep, morph $> Element.satisfy_morphism
    3.13 +              (map (Element.morph_witness export') wits))
    3.14 +            (Element.eq_morphism thy eqns |> Option.map (rpair true))
    3.15 +            export) thy) (deps ~~ witss)));
    3.16  
    3.17    in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;
    3.18  
     4.1 --- a/src/Pure/Isar/locale.ML	Fri Jul 30 15:03:42 2010 +0200
     4.2 +++ b/src/Pure/Isar/locale.ML	Sat Jul 31 21:14:20 2010 +0200
     4.3 @@ -67,10 +67,10 @@
     4.4  
     4.5    (* Registrations and dependencies *)
     4.6    val add_registration: string * morphism -> (morphism * bool) option ->
     4.7 -    morphism -> theory -> theory
     4.8 +    morphism -> Context.generic -> Context.generic
     4.9    val amend_registration: string * morphism -> morphism * bool ->
    4.10 -    morphism -> theory -> theory
    4.11 -  val get_registrations: theory -> string -> morphism list
    4.12 +    morphism -> Context.generic -> Context.generic
    4.13 +  val registrations_of_locale: Context.generic -> string -> (string * morphism) list
    4.14    val add_dependency: string -> string * morphism -> morphism -> theory -> theory
    4.15  
    4.16    (* Diagnostic *)
    4.17 @@ -349,7 +349,7 @@
    4.18  
    4.19  structure Idtab = Table(type key = string * term list val ord = ident_ord);
    4.20  
    4.21 -structure Registrations = Theory_Data
    4.22 +structure Registrations = Generic_Data
    4.23  (
    4.24    type T = ((morphism * morphism) * serial) Idtab.table *
    4.25      (* registrations, indexed by locale name and instance;
    4.26 @@ -391,9 +391,10 @@
    4.27    (* registration to be amended identified by its serial id *)
    4.28    Registrations.map (apsnd (Inttab.map_default (serial', []) (cons (mixin, serial ()))));
    4.29  
    4.30 -fun get_mixins thy (name, morph) =
    4.31 +fun get_mixins context (name, morph) =
    4.32    let
    4.33 -    val (regs, mixins) = Registrations.get thy;
    4.34 +    val thy = Context.theory_of context;
    4.35 +    val (regs, mixins) = Registrations.get context;
    4.36    in
    4.37      case Idtab.lookup regs (name, instance_of thy name morph) of
    4.38        NONE => []
    4.39 @@ -403,32 +404,35 @@
    4.40  fun compose_mixins mixins =
    4.41    fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
    4.42  
    4.43 -fun collect_mixins thy (name, morph) =
    4.44 -  roundup thy (fn dep => fn mixins => merge (eq_snd op =) (mixins, get_mixins thy dep))
    4.45 -    Morphism.identity (name, morph) ([(name, instance_of thy name morph)], [])
    4.46 -  |> snd |> filter (snd o fst)  (* only inheritable mixins *)
    4.47 -  |> (fn x => merge (eq_snd op =) (x, get_mixins thy (name, morph)))
    4.48 -  |> compose_mixins;
    4.49 +fun collect_mixins context (name, morph) =
    4.50 +  let
    4.51 +    val thy = Context.theory_of context;
    4.52 +  in
    4.53 +    roundup thy (fn dep => fn mixins => merge (eq_snd op =) (mixins, get_mixins context dep))
    4.54 +      Morphism.identity (name, morph) ([(name, instance_of thy name morph)], [])
    4.55 +    |> snd |> filter (snd o fst)  (* only inheritable mixins *)
    4.56 +    |> (fn x => merge (eq_snd op =) (x, get_mixins context (name, morph)))
    4.57 +    |> compose_mixins
    4.58 +  end;
    4.59  
    4.60 -fun gen_get_registrations thy select = Registrations.get thy
    4.61 +fun get_registrations context select = Registrations.get context
    4.62    |>> Idtab.dest |>> select
    4.63    (* with inherited mixins *)
    4.64    |-> (fn regs => fn _ => map (fn ((name, _), ((base, export) ,_)) =>
    4.65 -    (name, base $> (collect_mixins thy (name, base $> export)) $> export)) regs);
    4.66 +    (name, base $> (collect_mixins context (name, base $> export)) $> export)) regs);
    4.67  
    4.68 -fun registrations_for_locale thy name =
    4.69 -  gen_get_registrations thy (filter (curry (op =) name o fst o fst));
    4.70 +fun registrations_of_locale context name =
    4.71 +  get_registrations context (filter (curry (op =) name o fst o fst));
    4.72  
    4.73 -val get_registrations = map snd oo registrations_for_locale;
    4.74 +fun all_registrations context = get_registrations context I;
    4.75  
    4.76 -fun all_registrations thy = gen_get_registrations thy I;
    4.77 -
    4.78 -fun activate_notes' activ_elem transfer thy export (name, morph) input =
    4.79 +fun activate_notes' activ_elem transfer context export (name, morph) input =
    4.80    let
    4.81 +    val thy = Context.theory_of context;
    4.82      val {notes, ...} = the_locale thy name;
    4.83      fun activate ((kind, facts), _) input =
    4.84        let
    4.85 -        val mixin = collect_mixins thy (name, morph $> export);
    4.86 +        val mixin = collect_mixins context (name, morph $> export);
    4.87          val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin $> export))
    4.88        in activ_elem (Notes (kind, facts')) input end;
    4.89    in
    4.90 @@ -438,15 +442,16 @@
    4.91  fun activate_facts' export dep context =
    4.92    let
    4.93      val thy = Context.theory_of context;
    4.94 -    val activate = activate_notes' Element.init (Element.transfer_morphism o Context.theory_of) thy export;
    4.95 +    val activate = activate_notes' Element.init (Element.transfer_morphism o Context.theory_of) context export;
    4.96    in roundup thy activate export dep (get_idents context, context) |-> put_idents end;
    4.97  
    4.98  
    4.99  (* Add and extend registrations *)
   4.100  
   4.101 -fun amend_registration (name, morph) mixin export thy =
   4.102 +fun amend_registration (name, morph) mixin export context =
   4.103    let
   4.104 -    val regs = Registrations.get thy |> fst;
   4.105 +    val thy = Context.theory_of context;
   4.106 +    val regs = Registrations.get context |> fst;
   4.107      val base = instance_of thy name (morph $> export);
   4.108    in
   4.109      case Idtab.lookup regs (name, base) of
   4.110 @@ -454,23 +459,24 @@
   4.111            quote (extern thy name) ^ " and\nparameter instantiation " ^
   4.112            space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
   4.113            " available")
   4.114 -      | SOME (_, serial') => add_mixin serial' mixin thy
   4.115 +      | SOME (_, serial') => add_mixin serial' mixin context
   4.116    end;
   4.117  
   4.118  (* Note that a registration that would be subsumed by an existing one will not be
   4.119     generated, and it will not be possible to amend it. *)
   4.120  
   4.121 -fun add_registration (name, base_morph) mixin export thy =
   4.122 +fun add_registration (name, base_morph) mixin export context =
   4.123    let
   4.124 +    val thy = Context.theory_of context;
   4.125      val mix = case mixin of NONE => Morphism.identity
   4.126            | SOME (mix, _) => mix;
   4.127      val morph = base_morph $> mix;
   4.128      val inst = instance_of thy name morph;
   4.129    in
   4.130 -    if member (ident_le thy) (get_idents (Context.Theory thy)) (name, inst)
   4.131 -    then thy
   4.132 +    if member (ident_le thy) (get_idents context) (name, inst)
   4.133 +    then context
   4.134      else
   4.135 -      (get_idents (Context.Theory thy), thy)
   4.136 +      (get_idents context, context)
   4.137        (* add new registrations with inherited mixins *)
   4.138        |> roundup thy (add_reg thy export) export (name, morph)
   4.139        |> snd
   4.140 @@ -478,7 +484,7 @@
   4.141        |> (case mixin of NONE => I
   4.142             | SOME mixin => amend_registration (name, morph) mixin export)
   4.143        (* activate import hierarchy as far as not already active *)
   4.144 -      |> Context.theory_map (activate_facts' export (name, morph))
   4.145 +      |> activate_facts' export (name, morph)
   4.146    end;
   4.147  
   4.148  
   4.149 @@ -487,11 +493,12 @@
   4.150  fun add_dependency loc (name, morph) export thy =
   4.151    let
   4.152      val thy' = (change_locale loc o apsnd) (cons ((name, (morph, export)), serial ())) thy;
   4.153 +    val context' = Context.Theory thy';
   4.154      val (_, regs) = fold_rev (roundup thy' cons export)
   4.155 -      (all_registrations thy') (get_idents (Context.Theory thy'), []);
   4.156 +      (all_registrations context') (get_idents (context'), []);
   4.157    in
   4.158      thy'
   4.159 -    |> fold_rev (fn dep => add_registration dep NONE export) regs
   4.160 +    |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs
   4.161    end;
   4.162  
   4.163  
   4.164 @@ -511,7 +518,7 @@
   4.165                val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
   4.166                  Attrib.map_facts (Attrib.attribute_i thy)
   4.167              in PureThy.note_thmss kind args'' #> snd end)
   4.168 -        (registrations_for_locale thy loc) thy))
   4.169 +        (registrations_of_locale (Context.Theory thy) loc) thy))
   4.170    in ctxt'' end;
   4.171  
   4.172  
   4.173 @@ -594,7 +601,7 @@
   4.174    end;
   4.175  
   4.176  fun print_registrations thy raw_name =
   4.177 -  (case registrations_for_locale thy (intern thy raw_name) of
   4.178 +  (case registrations_of_locale (Context.Theory thy) (intern thy raw_name) of
   4.179        [] => Pretty.str ("no interpretations")
   4.180      | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
   4.181    |> Pretty.writeln;
   4.182 @@ -607,7 +614,7 @@
   4.183          val params = params_of thy name;
   4.184          val axioms = (these o Option.map (Logic.strip_imp_prems o Thm.prop_of) o fst o intros_of thy) name;
   4.185          val registrations = map (instance_of thy name o snd)
   4.186 -          (registrations_for_locale thy name);
   4.187 +          (registrations_of_locale (Context.Theory thy) name);
   4.188        in 
   4.189          Graph.new_node (name, { params = params, axioms = axioms, registrations = registrations })
   4.190        end;
     5.1 --- a/src/Tools/quickcheck.ML	Fri Jul 30 15:03:42 2010 +0200
     5.2 +++ b/src/Tools/quickcheck.ML	Sat Jul 31 21:14:20 2010 +0200
     5.3 @@ -228,7 +228,7 @@
     5.4      val proto_goal = Logic.list_implies (map Thm.term_of assms, subst_bounds (frees, strip gi));
     5.5      val check_goals = case some_locale
     5.6       of NONE => [proto_goal]
     5.7 -      | SOME locale => map (fn phi => Morphism.term phi proto_goal) (Locale.get_registrations thy locale);
     5.8 +      | SOME locale => map (fn (_, phi) => Morphism.term phi proto_goal) (Locale.registrations_of_locale (Context.Theory thy) (*FIXME*) locale);
     5.9      val inst_goals = maps (fn check_goal => map (fn T =>
    5.10        Term ((Object_Logic.atomize_term thy o monomorphic_term thy insts T) check_goal)
    5.11          handle WELLSORTED s => Wellsorted_Error s) default_Ts) check_goals