source positions for locale and class expressions;
authorwenzelm
Wed Mar 14 17:52:38 2012 +0100 (2012-03-14)
changeset 469223717f3878714
parent 46921 aa862ff8a8a9
child 46923 947f63062022
source positions for locale and class expressions;
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/parse.ML
src/Pure/Isar/parse_spec.ML
src/Pure/Isar/proof_context.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Wed Mar 14 15:59:39 2012 +0100
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Wed Mar 14 17:52:38 2012 +0100
     1.3 @@ -198,10 +198,11 @@
     1.4  
     1.5  fun prep_class_spec prep_class prep_class_elems thy raw_supclasses raw_elems =
     1.6    let
     1.7 +    val thy_ctxt = Proof_Context.init_global thy;
     1.8  
     1.9      (* prepare import *)
    1.10      val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy));
    1.11 -    val sups = Sign.minimize_sort thy (map (prep_class thy) raw_supclasses);
    1.12 +    val sups = Sign.minimize_sort thy (map (prep_class thy_ctxt) raw_supclasses);
    1.13      val _ =
    1.14        (case filter_out (Class.is_class thy) sups of
    1.15          [] => ()
    1.16 @@ -219,7 +220,7 @@
    1.17      val sup_sort = inter_sort base_sort sups;
    1.18  
    1.19      (* process elements as class specification *)
    1.20 -    val class_ctxt = Class.begin sups base_sort (Proof_Context.init_global thy);
    1.21 +    val class_ctxt = Class.begin sups base_sort thy_ctxt;
    1.22      val ((_, _, syntax_elems), _) = class_ctxt
    1.23        |> Expression.cert_declaration supexpr I inferred_elems;
    1.24      fun check_vars e vs =
    1.25 @@ -243,7 +244,7 @@
    1.26    in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (elems, global_syntax)) end;
    1.27  
    1.28  val cert_class_spec = prep_class_spec (K I) cert_class_elems;
    1.29 -val read_class_spec = prep_class_spec Sign.intern_class read_class_elems;
    1.30 +val read_class_spec = prep_class_spec Proof_Context.read_class read_class_elems;
    1.31  
    1.32  
    1.33  (* class establishment *)
     2.1 --- a/src/Pure/Isar/expression.ML	Wed Mar 14 15:59:39 2012 +0100
     2.2 +++ b/src/Pure/Isar/expression.ML	Wed Mar 14 17:52:38 2012 +0100
     2.3 @@ -8,9 +8,9 @@
     2.4  sig
     2.5    (* Locale expressions *)
     2.6    datatype 'term map = Positional of 'term option list | Named of (string * 'term) list
     2.7 -  type 'term expr = (string * ((string * bool) * 'term map)) list
     2.8 -  type expression_i = term expr * (binding * typ option * mixfix) list
     2.9 -  type expression = string expr * (binding * string option * mixfix) list
    2.10 +  type ('name, 'term) expr = ('name * ((string * bool) * 'term map)) list
    2.11 +  type expression_i = (string, term) expr * (binding * typ option * mixfix) list
    2.12 +  type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list
    2.13  
    2.14    (* Processing of context statements *)
    2.15    val cert_statement: Element.context_i list -> (term * term list) list list ->
    2.16 @@ -41,7 +41,7 @@
    2.17      (term list list * (string * morphism) list * morphism) * Proof.context
    2.18    val sublocale: (local_theory -> local_theory) -> string -> expression_i ->
    2.19      (Attrib.binding * term) list -> theory -> Proof.state
    2.20 -  val sublocale_cmd: (local_theory -> local_theory) -> string -> expression ->
    2.21 +  val sublocale_cmd: (local_theory -> local_theory) -> xstring * Position.T -> expression ->
    2.22      (Attrib.binding * string) list -> theory -> Proof.state
    2.23    val interpretation: expression_i -> (Attrib.binding * term) list ->
    2.24      theory -> Proof.state
    2.25 @@ -68,15 +68,15 @@
    2.26    Positional of 'term option list |
    2.27    Named of (string * 'term) list;
    2.28  
    2.29 -type 'term expr = (string * ((string * bool) * 'term map)) list;
    2.30 +type ('name, 'term) expr = ('name * ((string * bool) * 'term map)) list;
    2.31  
    2.32 -type expression = string expr * (binding * string option * mixfix) list;
    2.33 -type expression_i = term expr * (binding * typ option * mixfix) list;
    2.34 +type expression_i = (string, term) expr * (binding * typ option * mixfix) list;
    2.35 +type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list;
    2.36  
    2.37  
    2.38  (** Internalise locale names in expr **)
    2.39  
    2.40 -fun intern thy instances =  map (apfst (Locale.intern thy)) instances;
    2.41 +fun check_expr thy instances = map (apfst (Locale.check thy)) instances;
    2.42  
    2.43  
    2.44  (** Parameters of expression **)
    2.45 @@ -343,7 +343,8 @@
    2.46  
    2.47  local
    2.48  
    2.49 -fun prep_full_context_statement parse_typ parse_prop prep_vars_elem prep_inst prep_vars_inst prep_expr
    2.50 +fun prep_full_context_statement
    2.51 +    parse_typ parse_prop prep_vars_elem prep_inst prep_vars_inst prep_expr
    2.52      {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_concl ctxt1 =
    2.53    let
    2.54      val thy = Proof_Context.theory_of ctxt1;
    2.55 @@ -417,7 +418,7 @@
    2.56  
    2.57  fun read_full_context_statement x =
    2.58    prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Proof_Context.read_vars
    2.59 -  parse_inst Proof_Context.read_vars intern x;
    2.60 +  parse_inst Proof_Context.read_vars check_expr x;
    2.61  
    2.62  end;
    2.63  
    2.64 @@ -903,10 +904,10 @@
    2.65            export thy) (deps ~~ witss))
    2.66    end;
    2.67  
    2.68 -fun gen_sublocale prep_expr intern parse_prop prep_attr
    2.69 +fun gen_sublocale prep_expr prep_loc parse_prop prep_attr
    2.70      before_exit raw_target expression equations thy =
    2.71    let
    2.72 -    val target = intern thy raw_target;
    2.73 +    val target = prep_loc thy raw_target;
    2.74      val target_ctxt = Named_Target.init before_exit target thy;
    2.75      val ((propss, deps, export), expr_ctxt) = prep_expr expression target_ctxt;
    2.76      val eqns = read_with_extended_syntax parse_prop deps expr_ctxt equations;
    2.77 @@ -923,7 +924,7 @@
    2.78  
    2.79  fun sublocale x = gen_sublocale cert_goal_expression (K I) (K I) (K I) x;
    2.80  fun sublocale_cmd x =
    2.81 -  gen_sublocale read_goal_expression Locale.intern Syntax.parse_prop Attrib.intern_src x;
    2.82 +  gen_sublocale read_goal_expression Locale.check Syntax.parse_prop Attrib.intern_src x;
    2.83  
    2.84  end;
    2.85  
     3.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Mar 14 15:59:39 2012 +0100
     3.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Mar 14 17:52:38 2012 +0100
     3.3 @@ -50,8 +50,8 @@
     3.4    val print_configs: Toplevel.transition -> Toplevel.transition
     3.5    val print_theorems: bool -> Toplevel.transition -> Toplevel.transition
     3.6    val print_locales: Toplevel.transition -> Toplevel.transition
     3.7 -  val print_locale: bool * xstring -> Toplevel.transition -> Toplevel.transition
     3.8 -  val print_registrations: string -> Toplevel.transition -> Toplevel.transition
     3.9 +  val print_locale: bool * (xstring * Position.T) -> Toplevel.transition -> Toplevel.transition
    3.10 +  val print_registrations: xstring * Position.T -> Toplevel.transition -> Toplevel.transition
    3.11    val print_dependencies: bool * Expression.expression -> Toplevel.transition
    3.12      -> Toplevel.transition
    3.13    val print_attributes: Toplevel.transition -> Toplevel.transition
     4.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Mar 14 15:59:39 2012 +0100
     4.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Mar 14 17:52:38 2012 +0100
     4.3 @@ -91,13 +91,13 @@
     4.4  val _ =
     4.5    Outer_Syntax.command "classes" "declare type classes" Keyword.thy_decl
     4.6      (Scan.repeat1 (Parse.binding -- Scan.optional ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |--
     4.7 -        Parse.!!! (Parse.list1 Parse.xname)) [])
     4.8 +        Parse.!!! (Parse.list1 Parse.class)) [])
     4.9        >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
    4.10  
    4.11  val _ =
    4.12    Outer_Syntax.command "classrel" "state inclusion of type classes (axiomatic!)" Keyword.thy_decl
    4.13 -    (Parse.and_list1 (Parse.xname -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<")
    4.14 -        |-- Parse.!!! Parse.xname))
    4.15 +    (Parse.and_list1 (Parse.class -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<")
    4.16 +        |-- Parse.!!! Parse.class))
    4.17      >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
    4.18  
    4.19  val _ =
    4.20 @@ -421,7 +421,7 @@
    4.21  val _ =
    4.22    Outer_Syntax.command "sublocale"
    4.23      "prove sublocale relation between a locale and a locale expression" Keyword.thy_goal
    4.24 -    (Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
    4.25 +    (Parse.position Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
    4.26        parse_interpretation_arguments false
    4.27        >> (fn (loc, (expr, equations)) =>
    4.28            Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd I loc expr equations)));
    4.29 @@ -445,7 +445,7 @@
    4.30  (* classes *)
    4.31  
    4.32  val class_val =
    4.33 -  Parse_Spec.class_expr --
    4.34 +  Parse_Spec.class_expression --
    4.35      Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
    4.36    Scan.repeat1 Parse_Spec.context_element >> pair [];
    4.37  
    4.38 @@ -458,7 +458,7 @@
    4.39  
    4.40  val _ =
    4.41    Outer_Syntax.local_theory_to_proof "subclass" "prove a subclass relation" Keyword.thy_goal
    4.42 -    (Parse.xname >> Class_Declaration.subclass_cmd I);
    4.43 +    (Parse.class >> Class_Declaration.subclass_cmd I);
    4.44  
    4.45  val _ =
    4.46    Outer_Syntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl
    4.47 @@ -468,8 +468,8 @@
    4.48  
    4.49  val _ =
    4.50    Outer_Syntax.command "instance" "prove type arity or subclass relation" Keyword.thy_goal
    4.51 -  ((Parse.xname -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |-- Parse.!!! Parse.xname)
    4.52 -        >> Class.classrel_cmd ||
    4.53 +  ((Parse.class --
    4.54 +    ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
    4.55      Parse.multi_arity >> Class.instance_arity_cmd)
    4.56      >> (Toplevel.print oo Toplevel.theory_to_proof) ||
    4.57      Scan.succeed
    4.58 @@ -831,12 +831,12 @@
    4.59  
    4.60  val _ =
    4.61    Outer_Syntax.improper_command "print_locale" "print locale of this theory" Keyword.diag
    4.62 -    (opt_bang -- Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_locale));
    4.63 +    (opt_bang -- Parse.position Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_locale));
    4.64  
    4.65  val _ =
    4.66    Outer_Syntax.improper_command "print_interps"
    4.67      "print interpretations of locale for this theory or proof context" Keyword.diag
    4.68 -    (Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations));
    4.69 +    (Parse.position Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations));
    4.70  
    4.71  val _ =
    4.72    Outer_Syntax.improper_command "print_dependencies"
     5.1 --- a/src/Pure/Isar/locale.ML	Wed Mar 14 15:59:39 2012 +0100
     5.2 +++ b/src/Pure/Isar/locale.ML	Wed Mar 14 17:52:38 2012 +0100
     5.3 @@ -79,8 +79,8 @@
     5.4    (* Diagnostic *)
     5.5    val all_locales: theory -> string list
     5.6    val print_locales: theory -> unit
     5.7 -  val print_locale: theory -> bool -> xstring -> unit
     5.8 -  val print_registrations: Proof.context -> string -> unit
     5.9 +  val print_locale: theory -> bool -> xstring * Position.T -> unit
    5.10 +  val print_registrations: Proof.context -> xstring * Position.T -> unit
    5.11    val print_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> unit
    5.12    val locale_deps: theory ->
    5.13      {params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list} Graph.T
    5.14 @@ -618,7 +618,7 @@
    5.15  
    5.16  fun print_locale thy show_facts raw_name =
    5.17    let
    5.18 -    val name = intern thy raw_name;
    5.19 +    val name = check thy raw_name;
    5.20      val ctxt = init name thy;
    5.21      fun cons_elem (elem as Notes _) = show_facts ? cons elem
    5.22        | cons_elem elem = cons elem;
    5.23 @@ -633,8 +633,7 @@
    5.24  fun print_registrations ctxt raw_name =
    5.25    let
    5.26      val thy = Proof_Context.theory_of ctxt;
    5.27 -    val name = intern thy raw_name;
    5.28 -    val _ = the_locale thy name;  (* error if locale unknown *)
    5.29 +    val name = check thy raw_name;
    5.30    in
    5.31      (case registrations_of (Context.Proof ctxt) (* FIXME *) name of
    5.32        [] => Pretty.str "no interpretations"
     6.1 --- a/src/Pure/Isar/parse.ML	Wed Mar 14 15:59:39 2012 +0100
     6.2 +++ b/src/Pure/Isar/parse.ML	Wed Mar 14 17:52:38 2012 +0100
     6.3 @@ -69,7 +69,9 @@
     6.4    val liberal_name: xstring parser
     6.5    val parname: string parser
     6.6    val parbinding: binding parser
     6.7 +  val class: string parser
     6.8    val sort: string parser
     6.9 +  val type_const: string parser
    6.10    val arity: (string * string list * string) parser
    6.11    val multi_arity: (string list * string list * string) parser
    6.12    val type_args: string list parser
    6.13 @@ -93,7 +95,6 @@
    6.14    val prop_group: string parser
    6.15    val term: string parser
    6.16    val prop: string parser
    6.17 -  val type_const: string parser
    6.18    val const: string parser
    6.19    val literal_fact: string parser
    6.20    val propp: (string * string list) parser
    6.21 @@ -257,14 +258,18 @@
    6.22  val parbinding = Scan.optional ($$$ "(" |-- binding --| $$$ ")") Binding.empty;
    6.23  
    6.24  
    6.25 -(* sorts and arities *)
    6.26 +(* type classes *)
    6.27 +
    6.28 +val class = group (fn () => "type class") (inner_syntax xname);
    6.29  
    6.30  val sort = group (fn () => "sort") (inner_syntax xname);
    6.31  
    6.32 -val arity = xname -- ($$$ "::" |-- !!!
    6.33 +val type_const = inner_syntax (group (fn () => "type constructor") xname);
    6.34 +
    6.35 +val arity = type_const -- ($$$ "::" |-- !!!
    6.36    (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
    6.37  
    6.38 -val multi_arity = and_list1 xname -- ($$$ "::" |-- !!!
    6.39 +val multi_arity = and_list1 type_const -- ($$$ "::" |-- !!!
    6.40    (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
    6.41  
    6.42  
    6.43 @@ -343,7 +348,6 @@
    6.44  val term = inner_syntax term_group;
    6.45  val prop = inner_syntax prop_group;
    6.46  
    6.47 -val type_const = inner_syntax (group (fn () => "type constructor") xname);
    6.48  val const = inner_syntax (group (fn () => "constant") xname);
    6.49  
    6.50  val literal_fact = inner_syntax (group (fn () => "literal fact") alt_string);
     7.1 --- a/src/Pure/Isar/parse_spec.ML	Wed Mar 14 15:59:39 2012 +0100
     7.2 +++ b/src/Pure/Isar/parse_spec.ML	Wed Mar 14 17:52:38 2012 +0100
     7.3 @@ -22,7 +22,7 @@
     7.4    val locale_mixfix: mixfix parser
     7.5    val locale_fixes: (binding * string option * mixfix) list parser
     7.6    val locale_insts: (string option list * (Attrib.binding * string) list) parser
     7.7 -  val class_expr: string list parser
     7.8 +  val class_expression: string list parser
     7.9    val locale_expression: bool -> Expression.expression parser
    7.10    val locale_keyword: string parser
    7.11    val context_element: Element.context parser
    7.12 @@ -125,11 +125,11 @@
    7.13    Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
    7.14    Parse.$$$ "defines" || Parse.$$$ "notes";
    7.15  
    7.16 -val class_expr = plus1_unless locale_keyword Parse.xname;
    7.17 +val class_expression = plus1_unless locale_keyword Parse.class;
    7.18  
    7.19  fun locale_expression mandatory =
    7.20    let
    7.21 -    val expr2 = Parse.xname;
    7.22 +    val expr2 = Parse.position Parse.xname;
    7.23      val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
    7.24        Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
    7.25      val expr0 = plus1_unless locale_keyword expr1;
     8.1 --- a/src/Pure/Isar/proof_context.ML	Wed Mar 14 15:59:39 2012 +0100
     8.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Mar 14 17:52:38 2012 +0100
     8.3 @@ -55,8 +55,6 @@
     8.4    val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
     8.5    val pretty_fact: Proof.context -> string * thm list -> Pretty.T
     8.6    val read_class: Proof.context -> xstring -> class
     8.7 -  val read_arity: Proof.context -> xstring * string list * string -> arity
     8.8 -  val cert_arity: Proof.context -> arity -> arity
     8.9    val read_typ: Proof.context -> string -> typ
    8.10    val read_typ_syntax: Proof.context -> string -> typ
    8.11    val read_typ_abbrev: Proof.context -> string -> typ
    8.12 @@ -70,6 +68,8 @@
    8.13    val read_type_name_proper: Proof.context -> bool -> string -> typ
    8.14    val read_const_proper: Proof.context -> bool -> string -> term
    8.15    val read_const: Proof.context -> bool -> typ -> string -> term
    8.16 +  val read_arity: Proof.context -> xstring * string list * string -> arity
    8.17 +  val cert_arity: Proof.context -> arity -> arity
    8.18    val allow_dummies: Proof.context -> Proof.context
    8.19    val prepare_sorts: Proof.context -> typ list -> typ list
    8.20    val check_tfree: Proof.context -> string * sort -> string * sort
    8.21 @@ -367,22 +367,6 @@
    8.22    in c end;
    8.23  
    8.24  
    8.25 -(* type arities *)
    8.26 -
    8.27 -local
    8.28 -
    8.29 -fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
    8.30 -  let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
    8.31 -  in Type.add_arity ctxt arity (tsig_of ctxt); arity end;
    8.32 -
    8.33 -in
    8.34 -
    8.35 -val read_arity = prep_arity intern_type Syntax.read_sort;
    8.36 -val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
    8.37 -
    8.38 -end;
    8.39 -
    8.40 -
    8.41  (* types *)
    8.42  
    8.43  fun read_typ_mode mode ctxt s =
    8.44 @@ -504,6 +488,23 @@
    8.45  end;
    8.46  
    8.47  
    8.48 +(* type arities *)
    8.49 +
    8.50 +local
    8.51 +
    8.52 +fun prep_arity prep_tycon prep_sort ctxt (t, Ss, S) =
    8.53 +  let val arity = (prep_tycon ctxt t, map (prep_sort ctxt) Ss, prep_sort ctxt S)
    8.54 +  in Type.add_arity ctxt arity (tsig_of ctxt); arity end;
    8.55 +
    8.56 +in
    8.57 +
    8.58 +val read_arity =
    8.59 +  prep_arity (fn ctxt => #1 o dest_Type o read_type_name_proper ctxt true) Syntax.read_sort;
    8.60 +val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
    8.61 +
    8.62 +end;
    8.63 +
    8.64 +
    8.65  (* skolem variables *)
    8.66  
    8.67  fun intern_skolem ctxt x =
     9.1 --- a/src/Pure/Thy/thy_output.ML	Wed Mar 14 15:59:39 2012 +0100
     9.2 +++ b/src/Pure/Thy/thy_output.ML	Wed Mar 14 17:52:38 2012 +0100
     9.3 @@ -586,7 +586,7 @@
     9.4      basic_entity (Binding.name "const") (Args.const_proper false) pretty_const #>
     9.5      basic_entity (Binding.name "abbrev") (Scan.lift Args.name_source) pretty_abbrev #>
     9.6      basic_entity (Binding.name "typ") Args.typ_abbrev Syntax.pretty_typ #>
     9.7 -    basic_entity (Binding.name "class") (Scan.lift Args.name) pretty_class #>
     9.8 +    basic_entity (Binding.name "class") (Scan.lift Args.name_source) pretty_class #>
     9.9      basic_entity (Binding.name "type") (Scan.lift Args.name) pretty_type #>
    9.10      basic_entity (Binding.name "text") (Scan.lift Args.name) pretty_text #>
    9.11      basic_entities (Binding.name "prf") Attrib.thms (pretty_prf false) #>