renamed sprop "prop#" to "prop'" -- proper identifier;
authorwenzelm
Fri Apr 08 17:45:37 2011 +0200 (2011-04-08)
changeset 422936cca0343ea48
parent 42292 b3196458428b
child 42294 0f4372a2d2e4
renamed sprop "prop#" to "prop'" -- proper identifier;
eliminated spurious symbolic string bindings (logic, any etc.);
hardwired special "prop" vs. "prop'" conversion;
tuned;
doc-src/Codegen/Thy/Setup.thy
src/HOL/Imperative_HOL/Overview.thy
src/HOL/Library/OptionalSugar.thy
src/Pure/Syntax/mixfix.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_ext.ML
src/Pure/pure_thy.ML
     1.1 --- a/doc-src/Codegen/Thy/Setup.thy	Fri Apr 08 16:38:46 2011 +0200
     1.2 +++ b/doc-src/Codegen/Thy/Setup.thy	Fri Apr 08 17:45:37 2011 +0200
     1.3 @@ -10,15 +10,13 @@
     1.4  setup {*
     1.5  let
     1.6    val typ = Simple_Syntax.read_typ;
     1.7 -  val typeT = Syntax_Ext.typeT;
     1.8 -  val spropT = Syntax_Ext.spropT;
     1.9  in
    1.10 -  Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
    1.11 -    ("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
    1.12 -    ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))]
    1.13 -  #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
    1.14 -      ("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
    1.15 -      ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \<Colon> _", [4, 0], 3))]
    1.16 +  Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
    1.17 +   [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
    1.18 +    ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
    1.19 +  Sign.add_modesyntax_i (Symbol.xsymbolsN, false)
    1.20 +   [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
    1.21 +    ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
    1.22  end
    1.23  *}
    1.24  
     2.1 --- a/src/HOL/Imperative_HOL/Overview.thy	Fri Apr 08 16:38:46 2011 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Overview.thy	Fri Apr 08 17:45:37 2011 +0200
     2.3 @@ -11,15 +11,13 @@
     2.4  setup {*
     2.5  let
     2.6    val typ = Simple_Syntax.read_typ;
     2.7 -  val typeT = Syntax_Ext.typeT;
     2.8 -  val spropT = Syntax_Ext.spropT;
     2.9  in
    2.10 -  Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
    2.11 -    ("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
    2.12 -    ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))]
    2.13 -  #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
    2.14 -      ("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
    2.15 -      ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \<Colon> _", [4, 0], 3))]
    2.16 +  Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
    2.17 +   [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
    2.18 +    ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
    2.19 +  Sign.add_modesyntax_i (Symbol.xsymbolsN, false)
    2.20 +   [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
    2.21 +    ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
    2.22  end
    2.23  *}(*>*)
    2.24  
     3.1 --- a/src/HOL/Library/OptionalSugar.thy	Fri Apr 08 16:38:46 2011 +0200
     3.2 +++ b/src/HOL/Library/OptionalSugar.thy	Fri Apr 08 17:45:37 2011 +0200
     3.3 @@ -51,15 +51,13 @@
     3.4  setup {*
     3.5  let
     3.6    val typ = Simple_Syntax.read_typ;
     3.7 -  val typeT = Syntax_Ext.typeT;
     3.8 -  val spropT = Syntax_Ext.spropT;
     3.9  in
    3.10 -  Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
    3.11 -    ("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
    3.12 -    ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))]
    3.13 -  #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
    3.14 -      ("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
    3.15 -      ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \<Colon> _", [4, 0], 3))]
    3.16 +  Sign.del_modesyntax_i (Symbol.xsymbolsN, false)
    3.17 +   [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
    3.18 +    ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
    3.19 +  Sign.add_modesyntax_i (Symbol.xsymbolsN, false)
    3.20 +   [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
    3.21 +    ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
    3.22  end
    3.23  *}
    3.24  
     4.1 --- a/src/Pure/Syntax/mixfix.ML	Fri Apr 08 16:38:46 2011 +0200
     4.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Apr 08 17:45:37 2011 +0200
     4.3 @@ -88,7 +88,8 @@
     4.4  
     4.5  (* syn_ext_types *)
     4.6  
     4.7 -fun make_type n = replicate n Syntax_Ext.typeT ---> Syntax_Ext.typeT;
     4.8 +val typeT = Type ("type", []);
     4.9 +fun make_type n = replicate n typeT ---> typeT;
    4.10  
    4.11  fun syn_ext_types type_decls =
    4.12    let
    4.13 @@ -150,8 +151,7 @@
    4.14        |> map (Syntax_Ext.stamp_trfun binder_stamp o
    4.15            apsnd (K o Syntax_Trans.non_typed_tr') o Syntax_Trans.mk_binder_tr' o swap);
    4.16    in
    4.17 -    Syntax_Ext.syn_ext' true is_logtype
    4.18 -      mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
    4.19 +    Syntax_Ext.syn_ext' is_logtype mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
    4.20    end;
    4.21  
    4.22  end;
     5.1 --- a/src/Pure/Syntax/syntax.ML	Fri Apr 08 16:38:46 2011 +0200
     5.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Apr 08 17:45:37 2011 +0200
     5.3 @@ -155,7 +155,7 @@
     5.4  
     5.5  (* configuration options *)
     5.6  
     5.7 -val root = Config.string (Config.declare "syntax_root" (K (Config.String Syntax_Ext.any)));
     5.8 +val root = Config.string (Config.declare "syntax_root" (K (Config.String "any")));
     5.9  
    5.10  val positions_raw = Config.declare "syntax_positions" (fn _ => Config.Bool true);
    5.11  val positions = Config.bool positions_raw;
    5.12 @@ -602,10 +602,10 @@
    5.13  val basic_syntax = update_syntax mode_default Syntax_Ext.pure_ext empty_syntax;
    5.14  
    5.15  val basic_nonterms =
    5.16 -  (Lexicon.terminals @ [Syntax_Ext.logic, "type", "types", "sort", "classes",
    5.17 -    Syntax_Ext.args, Syntax_Ext.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
    5.18 -    "asms", Syntax_Ext.any, Syntax_Ext.sprop, "num_const", "float_const", "index",
    5.19 -    "struct", "id_position", "longid_position", "type_name", "class_name"]);
    5.20 +  (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
    5.21 +    "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
    5.22 +    "any", "prop'", "num_const", "float_const", "index", "struct",
    5.23 +    "id_position", "longid_position", "type_name", "class_name"]);
    5.24  
    5.25  
    5.26  
     6.1 --- a/src/Pure/Syntax/syntax_ext.ML	Fri Apr 08 16:38:46 2011 +0200
     6.2 +++ b/src/Pure/Syntax/syntax_ext.ML	Fri Apr 08 17:45:37 2011 +0200
     6.3 @@ -7,13 +7,6 @@
     6.4  signature SYNTAX_EXT =
     6.5  sig
     6.6    val dddot_indexname: indexname
     6.7 -  val logic: string
     6.8 -  val args: string
     6.9 -  val cargs: string
    6.10 -  val typeT: typ
    6.11 -  val any: string
    6.12 -  val sprop: string
    6.13 -  val spropT: typ
    6.14    val max_pri: int
    6.15    datatype mfix = Mfix of string * typ * string * int list * int
    6.16    val err_in_mfix: string -> mfix -> 'a
    6.17 @@ -39,7 +32,7 @@
    6.18    val mfix_delims: string -> string list
    6.19    val mfix_args: string -> int
    6.20    val escape: string -> string
    6.21 -  val syn_ext': bool -> (string -> bool) -> mfix list ->
    6.22 +  val syn_ext': (string -> bool) -> mfix list ->
    6.23      string list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
    6.24      (string * ((Proof.context -> term list -> term) * stamp)) list *
    6.25      (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
    6.26 @@ -79,24 +72,6 @@
    6.27  val dddot_indexname = ("dddot", 0);
    6.28  
    6.29  
    6.30 -(* syntactic categories *)
    6.31 -
    6.32 -val logic = "logic";
    6.33 -val logicT = Type (logic, []);
    6.34 -
    6.35 -val args = "args";
    6.36 -val cargs = "cargs";
    6.37 -
    6.38 -val typeT = Type ("type", []);
    6.39 -
    6.40 -val sprop = "#prop";
    6.41 -val spropT = Type (sprop, []);
    6.42 -
    6.43 -val any = "any";
    6.44 -val anyT = Type (any, []);
    6.45 -
    6.46 -
    6.47 -
    6.48  (** datatype xprod **)
    6.49  
    6.50  (*Delim s: delimiter s
    6.51 @@ -165,10 +140,10 @@
    6.52    | typ_to_nt default _ = default;
    6.53  
    6.54  (*get nonterminal for rhs*)
    6.55 -val typ_to_nonterm = typ_to_nt any;
    6.56 +val typ_to_nonterm = typ_to_nt "any";
    6.57  
    6.58  (*get nonterminal for lhs*)
    6.59 -val typ_to_nonterm1 = typ_to_nt logic;
    6.60 +val typ_to_nonterm1 = typ_to_nt "logic";
    6.61  
    6.62  
    6.63  (* read mixfix annotations *)
    6.64 @@ -219,7 +194,7 @@
    6.65  
    6.66  (* mfix_to_xprod *)
    6.67  
    6.68 -fun mfix_to_xprod convert is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) =
    6.69 +fun mfix_to_xprod is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) =
    6.70    let
    6.71      fun check_pri p =
    6.72        if p >= 0 andalso p <= max_pri then ()
    6.73 @@ -255,7 +230,7 @@
    6.74        | rem_pri sym = sym;
    6.75  
    6.76      fun logify_types (a as (Argument (s, p))) =
    6.77 -          if s <> "prop" andalso is_logtype s then Argument (logic, p) else a
    6.78 +          if s <> "prop" andalso is_logtype s then Argument ("logic", p) else a
    6.79        | logify_types a = a;
    6.80  
    6.81  
    6.82 @@ -287,8 +262,9 @@
    6.83          andalso not (null symbs)
    6.84          andalso not (exists is_delim symbs);
    6.85      val lhs' =
    6.86 -      if convert andalso not copy_prod then
    6.87 -       (if lhs = "prop" then sprop else if is_logtype lhs then logic else lhs)
    6.88 +      if copy_prod orelse lhs = "prop" andalso symbs = [Argument ("prop'", 0)] then lhs
    6.89 +      else if lhs = "prop" then "prop'"
    6.90 +      else if is_logtype lhs then "logic"
    6.91        else lhs;
    6.92      val symbs' = map logify_types symbs;
    6.93      val xprod = XProd (lhs', symbs', const', pri);
    6.94 @@ -322,12 +298,12 @@
    6.95  
    6.96  (* syn_ext *)
    6.97  
    6.98 -fun syn_ext' convert is_logtype mfixes consts trfuns (parse_rules, print_rules) =
    6.99 +fun syn_ext' is_logtype mfixes consts trfuns (parse_rules, print_rules) =
   6.100    let
   6.101      val (parse_ast_translation, parse_translation, print_translation,
   6.102        print_ast_translation) = trfuns;
   6.103  
   6.104 -    val (xprods, parse_rules') = map (mfix_to_xprod convert is_logtype) mfixes
   6.105 +    val (xprods, parse_rules') = map (mfix_to_xprod is_logtype) mfixes
   6.106        |> split_list |> apsnd (rev o flat);
   6.107      val mfix_consts =
   6.108        distinct (op =) (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
   6.109 @@ -344,7 +320,7 @@
   6.110    end;
   6.111  
   6.112  
   6.113 -val syn_ext = syn_ext' true (K false);
   6.114 +val syn_ext = syn_ext' (K false);
   6.115  
   6.116  fun syn_ext_const_names cs = syn_ext [] cs ([], [], [], []) ([], []);
   6.117  fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) rules;
   6.118 @@ -365,14 +341,16 @@
   6.119  val token_markers =
   6.120    ["_tfree", "_tvar", "_free", "_bound", "_var", "_numeral", "_inner_string"];
   6.121  
   6.122 -val pure_ext = syn_ext' false (K false)
   6.123 -  [Mfix ("_", spropT --> propT, "", [0], 0),
   6.124 -   Mfix ("_", logicT --> anyT, "", [0], 0),
   6.125 -   Mfix ("_", spropT --> anyT, "", [0], 0),
   6.126 -   Mfix ("'(_')", logicT --> logicT, "", [0], max_pri),
   6.127 -   Mfix ("'(_')", spropT --> spropT, "", [0], max_pri),
   6.128 -   Mfix ("_::_",  [logicT, typeT] ---> logicT, "_constrain", [4, 0], 3),
   6.129 -   Mfix ("_::_",  [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)]
   6.130 +val typ = Simple_Syntax.read_typ;
   6.131 +
   6.132 +val pure_ext = syn_ext' (K false)
   6.133 +  [Mfix ("_", typ "prop' => prop", "", [0], 0),
   6.134 +   Mfix ("_", typ "logic => any", "", [0], 0),
   6.135 +   Mfix ("_", typ "prop' => any", "", [0], 0),
   6.136 +   Mfix ("'(_')", typ "logic => logic", "", [0], max_pri),
   6.137 +   Mfix ("'(_')", typ "prop' => prop'", "", [0], max_pri),
   6.138 +   Mfix ("_::_", typ "logic => type => logic", "_constrain", [4, 0], 3),
   6.139 +   Mfix ("_::_", typ "prop' => type => prop'", "_constrain", [4, 0], 3)]
   6.140    token_markers
   6.141    ([], [], [], [])
   6.142    ([], []);
     7.1 --- a/src/Pure/pure_thy.ML	Fri Apr 08 16:38:46 2011 +0200
     7.2 +++ b/src/Pure/pure_thy.ML	Fri Apr 08 17:45:37 2011 +0200
     7.3 @@ -19,9 +19,6 @@
     7.4  val tycon = Lexicon.mark_type;
     7.5  val const = Lexicon.mark_const;
     7.6  
     7.7 -val typeT = Syntax_Ext.typeT;
     7.8 -val spropT = Syntax_Ext.spropT;
     7.9 -
    7.10  
    7.11  (* application syntax variants *)
    7.12  
    7.13 @@ -143,7 +140,7 @@
    7.14      ("_bracket",          typ "types => type => type",  Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
    7.15      ("_ofsort",           typ "tid => sort => type",    Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
    7.16      ("_constrain",        typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
    7.17 -    ("_constrain",        [spropT, typeT] ---> spropT,  Mixfix ("_\\<Colon>_", [4, 0], 3)),
    7.18 +    ("_constrain",        typ "prop' => type => prop'", Mixfix ("_\\<Colon>_", [4, 0], 3)),
    7.19      ("_idtyp",            typ "id_position => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
    7.20      ("_idtypdummy",       typ "type => idt",            Mixfix ("'_()\\<Colon>_", [], 0)),
    7.21      ("_lambda",           typ "pttrns => 'a => logic",  Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),