Sublocale: removed public after_qed; identifiers private to NewLocale.
authorballarin
Wed Dec 03 15:27:41 2008 +0100 (2008-12-03)
changeset 28951e89dde5f365c
parent 28950 b2db06eb214d
child 28953 48cd567f6940
child 28993 829e684b02ef
Sublocale: removed public after_qed; identifiers private to NewLocale.
src/Pure/Isar/expression.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/new_locale.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Wed Dec 03 15:26:46 2008 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Wed Dec 03 15:27:41 2008 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      Pure/Isar/expression.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Clemens Ballarin, TU Muenchen
     1.7  
     1.8  New locale development --- experimental.
     1.9 @@ -25,10 +24,8 @@
    1.10      string * Proof.context
    1.11  
    1.12    (* Interpretation *)
    1.13 -  val sublocale_cmd: (thm list list -> Proof.context -> Proof.context) ->
    1.14 -    string -> expression -> theory -> Proof.state;
    1.15 -  val sublocale: (thm list list -> Proof.context -> Proof.context) ->
    1.16 -    string -> expression_i -> theory -> Proof.state;
    1.17 +  val sublocale_cmd: string -> expression -> theory -> Proof.state;
    1.18 +  val sublocale: string -> expression_i -> theory -> Proof.state;
    1.19  
    1.20    (* Debugging and development *)
    1.21    val parse_expression: OuterParse.token list -> expression * OuterParse.token list
    1.22 @@ -434,7 +431,7 @@
    1.23  
    1.24      val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import);
    1.25  
    1.26 -    fun prep_inst (loc, (prfx, inst)) (i, marked, insts, ctxt) =
    1.27 +    fun prep_inst (loc, (prfx, inst)) (i, insts, ctxt) =
    1.28        let
    1.29          val (parm_names, parm_types) = NewLocale.params_of thy loc |>
    1.30            map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
    1.31 @@ -443,11 +440,11 @@
    1.32            Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types;
    1.33          val inst'' = map2 TypeInfer.constrain parm_types' inst';
    1.34          val insts' = insts @ [(loc, (prfx, inst''))];
    1.35 -        val (insts'', _, _, ctxt') = check_autofix insts' [] [] ctxt;
    1.36 +        val (insts'', _, _, ctxt' (* FIXME not used *) ) = check_autofix insts' [] [] ctxt;
    1.37          val inst''' = insts'' |> List.last |> snd |> snd;
    1.38          val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt;
    1.39 -        val (marked', ctxt'') = NewLocale.activate_declarations thy (loc, morph) (marked, ctxt);
    1.40 -      in (i+1, marked', insts', ctxt'') end;
    1.41 +        val ctxt'' = NewLocale.activate_declarations thy (loc, morph) ctxt;
    1.42 +      in (i+1, insts', ctxt'') end;
    1.43    
    1.44      fun prep_elem raw_elem (insts, elems, ctxt) =
    1.45        let
    1.46 @@ -465,7 +462,7 @@
    1.47  
    1.48      val fors = prep_vars fixed context |> fst;
    1.49      val ctxt = context |> ProofContext.add_fixes_i fors |> snd;
    1.50 -    val (_, _, insts', ctxt') = fold prep_inst raw_insts (0, NewLocale.empty, [], ctxt);
    1.51 +    val (_, insts', ctxt') = fold prep_inst raw_insts (0, [], NewLocale.clear_idents ctxt);
    1.52      val (_, elems'', ctxt'') = fold prep_elem raw_elems (insts', [], ctxt');
    1.53      val (insts, elems, concl, ctxt) = prep_concl raw_concl (insts', elems'', ctxt'');
    1.54  
    1.55 @@ -542,7 +539,7 @@
    1.56      (* Declare parameters and imported facts *)
    1.57      val context' = context |>
    1.58        ProofContext.add_fixes_i fixed |> snd |>
    1.59 -      pair NewLocale.empty |> fold (NewLocale.activate_facts thy) deps |> snd;
    1.60 +      NewLocale.clear_idents |> fold (NewLocale.activate_facts thy) deps;
    1.61      val ((elems', _), _) = activate elems (ProofContext.set_stmt true context');
    1.62    in ((fixed, deps, elems'), (parms, spec, defs)) end;
    1.63  
    1.64 @@ -804,7 +801,7 @@
    1.65  local
    1.66  
    1.67  fun gen_sublocale prep_expr intern
    1.68 -    after_qed raw_target expression thy =
    1.69 +    raw_target expression thy =
    1.70    let
    1.71      val target = intern thy raw_target;
    1.72      val target_ctxt = NewLocale.init target thy;
    1.73 @@ -814,13 +811,10 @@
    1.74      fun store_dep ((name, morph), thms) =
    1.75        NewLocale.add_dependency target (name, morph $> Element.satisfy_morphism thms $> export);
    1.76  
    1.77 -    fun after_qed' results =
    1.78 -      fold store_dep (deps ~~ prep_result propss results) #>
    1.79 -      after_qed results;
    1.80 -
    1.81 +    fun after_qed results = fold store_dep (deps ~~ prep_result propss results);
    1.82    in
    1.83      goal_ctxt |>
    1.84 -      Proof.theorem_i NONE after_qed' (prep_propp propss) |>
    1.85 +      Proof.theorem_i NONE after_qed (prep_propp propss) |>
    1.86        Element.refine_witness |> Seq.hd
    1.87    end;
    1.88  
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Dec 03 15:26:46 2008 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Dec 03 15:27:41 2008 +0100
     2.3 @@ -403,7 +403,7 @@
     2.4      "prove sublocale relation between a locale and a locale expression" K.thy_goal
     2.5      (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! Expression.parse_expression
     2.6        >> (fn (loc, expr) =>
     2.7 -        Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale_cmd (K I) loc expr))));
     2.8 +        Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr))));
     2.9  
    2.10  val _ =
    2.11    OuterSyntax.command "interpretation"
     3.1 --- a/src/Pure/Isar/new_locale.ML	Wed Dec 03 15:26:46 2008 +0100
     3.2 +++ b/src/Pure/Isar/new_locale.ML	Wed Dec 03 15:27:41 2008 +0100
     3.3 @@ -1,5 +1,4 @@
     3.4 -(*  Title:      Pure/Isar/expression.ML
     3.5 -    ID:         $Id$
     3.6 +(*  Title:      Pure/Isar/new_locale.ML
     3.7      Author:     Clemens Ballarin, TU Muenchen
     3.8  
     3.9  New locale development --- experimental.
    3.10 @@ -7,11 +6,9 @@
    3.11  
    3.12  signature NEW_LOCALE =
    3.13  sig
    3.14 -  type identifiers
    3.15 -  val empty: identifiers
    3.16 -
    3.17    type locale
    3.18  
    3.19 +  val clear_idents: Proof.context -> Proof.context
    3.20    val test_locale: theory -> string -> bool
    3.21    val register_locale: string ->
    3.22      (string * sort) list * (Name.binding * typ option * mixfix) list ->
    3.23 @@ -39,9 +36,9 @@
    3.24  
    3.25    (* Activation *)
    3.26    val activate_declarations: theory -> string * Morphism.morphism ->
    3.27 -    identifiers * Proof.context -> identifiers * Proof.context
    3.28 +    Proof.context -> Proof.context
    3.29    val activate_facts: theory -> string * Morphism.morphism ->
    3.30 -    identifiers * Proof.context -> identifiers * Proof.context
    3.31 +    Proof.context -> Proof.context
    3.32  (*  val activate: string -> theory -> (Element.context_i -> 'a -> 'a) -> 'a -> 'a *)
    3.33    val init: string -> theory -> Proof.context
    3.34  
    3.35 @@ -57,6 +54,8 @@
    3.36  end;
    3.37  
    3.38  
    3.39 +(*** Theorem list extensible via attribute --- to control intro_locales_tac ***)
    3.40 +
    3.41  (* FIXME: consider moving named_thms.ML up in the build hierarchy and using that *)
    3.42  functor ThmsFun() =
    3.43  struct
    3.44 @@ -184,15 +183,36 @@
    3.45  
    3.46  (*** Activate context elements of locale ***)
    3.47  
    3.48 -(** Resolve locale dependencies in a depth-first fashion **)
    3.49 +(** Identifiers: activated locales in theory or proof context **)
    3.50  
    3.51  type identifiers = (string * term list) list;
    3.52  
    3.53  val empty = ([] : identifiers);
    3.54  
    3.55 +fun ident_eq thy ((n, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
    3.56 +
    3.57  local
    3.58  
    3.59 -fun ident_eq thy ((n, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts);
    3.60 +structure IdentifiersData = GenericDataFun
    3.61 +(
    3.62 +  type T = identifiers;
    3.63 +  val empty = empty;
    3.64 +  val extend = I;
    3.65 +  fun merge _ = Library.merge (op =);  (* FIXME cannot do this properly without theory context *)
    3.66 +);
    3.67 +
    3.68 +in
    3.69 +
    3.70 +val get_idents = IdentifiersData.get o Context.Proof;
    3.71 +val put_idents = Context.proof_map o IdentifiersData.put;
    3.72 +val clear_idents = put_idents empty;
    3.73 +
    3.74 +end;
    3.75 +
    3.76 +
    3.77 +(** Resolve locale dependencies in a depth-first fashion **)
    3.78 +
    3.79 +local
    3.80  
    3.81  val roundup_bound = 120;
    3.82  
    3.83 @@ -220,18 +240,17 @@
    3.84  
    3.85  in
    3.86  
    3.87 -fun roundup thy activate_dep (name, morph) (marked, ctxt) =
    3.88 +fun roundup thy activate_dep (name, morph) (marked, input) =
    3.89    let
    3.90 -    val Loc {dependencies, ...} = the_locale thy name;
    3.91      val (dependencies', marked') = add thy 0 (name, morph) ([], marked);
    3.92    in
    3.93 -    (marked', ctxt |> fold_rev (activate_dep thy) dependencies')
    3.94 +    (marked', input |> fold_rev (activate_dep thy) dependencies')
    3.95    end;
    3.96  
    3.97  end;
    3.98  
    3.99  
   3.100 -(* Declarations and facts *)
   3.101 +(* Declarations, facts and entire locale content *)
   3.102  
   3.103  fun activate_decls thy (name, morph) ctxt =
   3.104    let
   3.105 @@ -252,10 +271,7 @@
   3.106      fold_rev activate notes input
   3.107    end;
   3.108  
   3.109 -
   3.110 -(* Entire locale content *)
   3.111 -
   3.112 -fun activate name thy activ_elem input =
   3.113 +fun activate_all name thy activ_elem (marked, input) =
   3.114    let
   3.115      val Loc {parameters = (_, params), spec = (asm, defs), dependencies, ...} =
   3.116        the_locale thy name;
   3.117 @@ -267,7 +283,7 @@
   3.118        (if not (null defs)
   3.119          then activ_elem (Defines (map (fn def => (Attrib.no_binding, (def, []))) defs))
   3.120          else I) |>
   3.121 -      pair empty |> roundup thy (activate_notes activ_elem) (name, Morphism.identity) |> snd
   3.122 +      pair marked |> roundup thy (activate_notes activ_elem) (name, Morphism.identity)
   3.123    end;
   3.124  
   3.125  
   3.126 @@ -302,11 +318,14 @@
   3.127  
   3.128  in
   3.129  
   3.130 -fun activate_declarations thy = roundup thy activate_decls;
   3.131 +fun activate_declarations thy dep ctxt =
   3.132 +  roundup thy activate_decls dep (get_idents ctxt, ctxt) |> uncurry put_idents;
   3.133 +  
   3.134 +fun activate_facts thy dep ctxt =
   3.135 +  roundup thy (activate_notes init_elem) dep (get_idents ctxt, ctxt) |> uncurry put_idents;
   3.136  
   3.137 -fun activate_facts thy = roundup thy (activate_notes init_elem);
   3.138 -
   3.139 -fun init name thy = activate name thy init_elem (ProofContext.init thy);
   3.140 +fun init name thy = activate_all name thy init_elem (empty, ProofContext.init thy) |>
   3.141 +  uncurry put_idents;
   3.142  
   3.143  fun print_locale thy show_facts name =
   3.144    let
   3.145 @@ -314,7 +333,7 @@
   3.146      val ctxt = init name' thy
   3.147    in
   3.148      Pretty.big_list "locale elements:"
   3.149 -      (activate name' thy (cons_elem show_facts) [] |> rev |> 
   3.150 +      (activate_all name' thy (cons_elem show_facts) (empty, []) |> snd |> rev |> 
   3.151          map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln
   3.152    end
   3.153