clarified check of internal names;
authorwenzelm
Thu Mar 06 10:53:14 2014 +0100 (2014-03-06)
changeset 559494766342e8376
parent 55948 bb21b380f65d
child 55950 3bb5c7179234
clarified check of internal names;
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/name.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Mar 06 10:12:47 2014 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Mar 06 10:53:14 2014 +0100
     1.3 @@ -422,19 +422,6 @@
     1.4  
     1.5  
     1.6  
     1.7 -(** prepare variables **)
     1.8 -
     1.9 -(* check Skolem constants *)
    1.10 -
    1.11 -fun no_skolem internal x =
    1.12 -  if Name.is_skolem x then
    1.13 -    error ("Illegal reference to internal Skolem constant: " ^ quote x)
    1.14 -  else if not internal andalso Name.is_internal x then
    1.15 -    error ("Illegal reference to internal variable: " ^ quote x)
    1.16 -  else x;
    1.17 -
    1.18 -
    1.19 -
    1.20  (** prepare terms and propositions **)
    1.21  
    1.22  (* inferred types of parameters *)
    1.23 @@ -515,7 +502,7 @@
    1.24  fun read_const ctxt strict ty text =
    1.25    let
    1.26      val (c, pos) = Symbol_Pos.source_content (Syntax.read_token text);
    1.27 -    val _ = no_skolem false c;
    1.28 +    val _ = Name.reject_internal (c, [pos]);
    1.29    in
    1.30      (case (Variable.lookup_fixed ctxt c, Variable.is_const ctxt c) of
    1.31        (SOME x, false) =>
    1.32 @@ -550,13 +537,12 @@
    1.33  
    1.34  fun intern_skolem ctxt x =
    1.35    let
    1.36 -    val _ = no_skolem false x;
    1.37 -    val sko = Variable.lookup_fixed ctxt x;
    1.38 +    val skolem = Variable.lookup_fixed ctxt x;
    1.39      val is_const = can (read_const_proper ctxt false) x orelse Long_Name.is_qualified x;
    1.40      val is_declared = is_some (Variable.def_type ctxt false (x, ~1));
    1.41    in
    1.42      if Variable.is_const ctxt x then NONE
    1.43 -    else if is_some sko then sko
    1.44 +    else if is_some skolem then skolem
    1.45      else if not is_const orelse is_declared then SOME x
    1.46      else NONE
    1.47    end;
    1.48 @@ -1033,8 +1019,10 @@
    1.49    fold_map (fn (b, raw_T, mx) => fn ctxt =>
    1.50      let
    1.51        val x = Variable.check_name b;
    1.52 -      val _ = Symbol_Pos.is_identifier (no_skolem internal x) orelse
    1.53 -        error ("Illegal variable name: " ^ Binding.print b);
    1.54 +      val check_name = if internal then Name.reject_skolem else Name.reject_internal;
    1.55 +      val _ =
    1.56 +        if can check_name (x, []) andalso Symbol_Pos.is_identifier x then ()
    1.57 +        else error ("Bad name: " ^ Binding.print b);
    1.58  
    1.59        fun cond_tvars T =
    1.60          if internal then T
     2.1 --- a/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 10:12:47 2014 +0100
     2.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Thu Mar 06 10:53:14 2014 +0100
     2.3 @@ -257,7 +257,8 @@
     2.4                      val _ = report ps (markup_const ctxt) c;
     2.5                    in Const (c, T) end)
     2.6            | decode ps _ _ (Free (a, T)) =
     2.7 -              (case (get_free a, get_const a) of
     2.8 +              (Name.reject_internal (a, ps);
     2.9 +               case (get_free a, get_const a) of
    2.10                  (SOME x, _) => (report ps (markup_free ctxt) x; Free (x, T))
    2.11                | (_, (true, c)) => (report ps (markup_const ctxt) c; Const (c, T))
    2.12                | (_, (false, c)) =>
     3.1 --- a/src/Pure/name.ML	Thu Mar 06 10:12:47 2014 +0100
     3.2 +++ b/src/Pure/name.ML	Thu Mar 06 10:53:14 2014 +0100
     3.3 @@ -14,9 +14,11 @@
     3.4    val internal: string -> string
     3.5    val dest_internal: string -> string
     3.6    val is_internal: string -> bool
     3.7 +  val reject_internal: string * Position.T list -> unit
     3.8    val skolem: string -> string
     3.9    val dest_skolem: string -> string
    3.10    val is_skolem: string -> bool
    3.11 +  val reject_skolem: string * Position.T list -> unit
    3.12    val clean_index: string * int -> string * int
    3.13    val clean: string -> string
    3.14    type context
    3.15 @@ -61,15 +63,19 @@
    3.16  val is_bound = String.isPrefix ":";
    3.17  
    3.18  
    3.19 -(* internal names *)
    3.20 +(* internal names -- NB: internal subsumes skolem *)
    3.21  
    3.22  val internal = suffix "_";
    3.23  val dest_internal = unsuffix "_";
    3.24  val is_internal = String.isSuffix "_";
    3.25 +fun reject_internal (x, ps) =
    3.26 +  if is_internal x then error ("Bad name: " ^ quote x ^ Position.here_list ps) else ();
    3.27  
    3.28  val skolem = suffix "__";
    3.29  val dest_skolem = unsuffix "__";
    3.30  val is_skolem = String.isSuffix "__";
    3.31 +fun reject_skolem (x, ps) =
    3.32 +  if is_skolem x then error ("Bad name: " ^ quote x ^ Position.here_list ps) else ();
    3.33  
    3.34  fun clean_index (x, i) =
    3.35    (case try dest_internal x of