# HG changeset patch # User wenzelm # Date 1302277537 -7200 # Node ID 6cca0343ea48909aa5ecb922ea67c582a73c1492 # Parent b3196458428bab7b4aa71d3e840add48e1048cfd renamed sprop "prop#" to "prop'" -- proper identifier; eliminated spurious symbolic string bindings (logic, any etc.); hardwired special "prop" vs. "prop'" conversion; tuned; diff -r b3196458428b -r 6cca0343ea48 doc-src/Codegen/Thy/Setup.thy --- a/doc-src/Codegen/Thy/Setup.thy Fri Apr 08 16:38:46 2011 +0200 +++ b/doc-src/Codegen/Thy/Setup.thy Fri Apr 08 17:45:37 2011 +0200 @@ -10,15 +10,13 @@ setup {* let val typ = Simple_Syntax.read_typ; - val typeT = Syntax_Ext.typeT; - val spropT = Syntax_Ext.spropT; in - Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [ - ("_constrain", typ "logic => type => logic", Mixfix ("_\_", [4, 0], 3)), - ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\_", [4, 0], 3))] - #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [ - ("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), - ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \ _", [4, 0], 3))] + Sign.del_modesyntax_i (Symbol.xsymbolsN, false) + [("_constrain", typ "logic => type => logic", Mixfix ("_\_", [4, 0], 3)), + ("_constrain", typ "prop' => type => prop'", Mixfix ("_\_", [4, 0], 3))] #> + Sign.add_modesyntax_i (Symbol.xsymbolsN, false) + [("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), + ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \ _", [4, 0], 3))] end *} diff -r b3196458428b -r 6cca0343ea48 src/HOL/Imperative_HOL/Overview.thy --- a/src/HOL/Imperative_HOL/Overview.thy Fri Apr 08 16:38:46 2011 +0200 +++ b/src/HOL/Imperative_HOL/Overview.thy Fri Apr 08 17:45:37 2011 +0200 @@ -11,15 +11,13 @@ setup {* let val typ = Simple_Syntax.read_typ; - val typeT = Syntax_Ext.typeT; - val spropT = Syntax_Ext.spropT; in - Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [ - ("_constrain", typ "logic => type => logic", Mixfix ("_\_", [4, 0], 3)), - ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\_", [4, 0], 3))] - #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [ - ("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), - ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \ _", [4, 0], 3))] + Sign.del_modesyntax_i (Symbol.xsymbolsN, false) + [("_constrain", typ "logic => type => logic", Mixfix ("_\_", [4, 0], 3)), + ("_constrain", typ "prop' => type => prop'", Mixfix ("_\_", [4, 0], 3))] #> + Sign.add_modesyntax_i (Symbol.xsymbolsN, false) + [("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), + ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \ _", [4, 0], 3))] end *}(*>*) diff -r b3196458428b -r 6cca0343ea48 src/HOL/Library/OptionalSugar.thy --- a/src/HOL/Library/OptionalSugar.thy Fri Apr 08 16:38:46 2011 +0200 +++ b/src/HOL/Library/OptionalSugar.thy Fri Apr 08 17:45:37 2011 +0200 @@ -51,15 +51,13 @@ setup {* let val typ = Simple_Syntax.read_typ; - val typeT = Syntax_Ext.typeT; - val spropT = Syntax_Ext.spropT; in - Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [ - ("_constrain", typ "logic => type => logic", Mixfix ("_\_", [4, 0], 3)), - ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\_", [4, 0], 3))] - #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [ - ("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), - ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \ _", [4, 0], 3))] + Sign.del_modesyntax_i (Symbol.xsymbolsN, false) + [("_constrain", typ "logic => type => logic", Mixfix ("_\_", [4, 0], 3)), + ("_constrain", typ "prop' => type => prop'", Mixfix ("_\_", [4, 0], 3))] #> + Sign.add_modesyntax_i (Symbol.xsymbolsN, false) + [("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), + ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \ _", [4, 0], 3))] end *} diff -r b3196458428b -r 6cca0343ea48 src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Fri Apr 08 16:38:46 2011 +0200 +++ b/src/Pure/Syntax/mixfix.ML Fri Apr 08 17:45:37 2011 +0200 @@ -88,7 +88,8 @@ (* syn_ext_types *) -fun make_type n = replicate n Syntax_Ext.typeT ---> Syntax_Ext.typeT; +val typeT = Type ("type", []); +fun make_type n = replicate n typeT ---> typeT; fun syn_ext_types type_decls = let @@ -150,8 +151,7 @@ |> map (Syntax_Ext.stamp_trfun binder_stamp o apsnd (K o Syntax_Trans.non_typed_tr') o Syntax_Trans.mk_binder_tr' o swap); in - Syntax_Ext.syn_ext' true is_logtype - mfix xconsts ([], binder_trs, binder_trs', []) ([], []) + Syntax_Ext.syn_ext' is_logtype mfix xconsts ([], binder_trs, binder_trs', []) ([], []) end; end; diff -r b3196458428b -r 6cca0343ea48 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Fri Apr 08 16:38:46 2011 +0200 +++ b/src/Pure/Syntax/syntax.ML Fri Apr 08 17:45:37 2011 +0200 @@ -155,7 +155,7 @@ (* configuration options *) -val root = Config.string (Config.declare "syntax_root" (K (Config.String Syntax_Ext.any))); +val root = Config.string (Config.declare "syntax_root" (K (Config.String "any"))); val positions_raw = Config.declare "syntax_positions" (fn _ => Config.Bool true); val positions = Config.bool positions_raw; @@ -602,10 +602,10 @@ val basic_syntax = update_syntax mode_default Syntax_Ext.pure_ext empty_syntax; val basic_nonterms = - (Lexicon.terminals @ [Syntax_Ext.logic, "type", "types", "sort", "classes", - Syntax_Ext.args, Syntax_Ext.cargs, "pttrn", "pttrns", "idt", "idts", "aprop", - "asms", Syntax_Ext.any, Syntax_Ext.sprop, "num_const", "float_const", "index", - "struct", "id_position", "longid_position", "type_name", "class_name"]); + (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes", + "args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms", + "any", "prop'", "num_const", "float_const", "index", "struct", + "id_position", "longid_position", "type_name", "class_name"]); diff -r b3196458428b -r 6cca0343ea48 src/Pure/Syntax/syntax_ext.ML --- a/src/Pure/Syntax/syntax_ext.ML Fri Apr 08 16:38:46 2011 +0200 +++ b/src/Pure/Syntax/syntax_ext.ML Fri Apr 08 17:45:37 2011 +0200 @@ -7,13 +7,6 @@ signature SYNTAX_EXT = sig val dddot_indexname: indexname - val logic: string - val args: string - val cargs: string - val typeT: typ - val any: string - val sprop: string - val spropT: typ val max_pri: int datatype mfix = Mfix of string * typ * string * int list * int val err_in_mfix: string -> mfix -> 'a @@ -39,7 +32,7 @@ val mfix_delims: string -> string list val mfix_args: string -> int val escape: string -> string - val syn_ext': bool -> (string -> bool) -> mfix list -> + val syn_ext': (string -> bool) -> mfix list -> string list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list * (string * ((Proof.context -> term list -> term) * stamp)) list * (string * ((Proof.context -> typ -> term list -> term) * stamp)) list * @@ -79,24 +72,6 @@ val dddot_indexname = ("dddot", 0); -(* syntactic categories *) - -val logic = "logic"; -val logicT = Type (logic, []); - -val args = "args"; -val cargs = "cargs"; - -val typeT = Type ("type", []); - -val sprop = "#prop"; -val spropT = Type (sprop, []); - -val any = "any"; -val anyT = Type (any, []); - - - (** datatype xprod **) (*Delim s: delimiter s @@ -165,10 +140,10 @@ | typ_to_nt default _ = default; (*get nonterminal for rhs*) -val typ_to_nonterm = typ_to_nt any; +val typ_to_nonterm = typ_to_nt "any"; (*get nonterminal for lhs*) -val typ_to_nonterm1 = typ_to_nt logic; +val typ_to_nonterm1 = typ_to_nt "logic"; (* read mixfix annotations *) @@ -219,7 +194,7 @@ (* mfix_to_xprod *) -fun mfix_to_xprod convert is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) = +fun mfix_to_xprod is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) = let fun check_pri p = if p >= 0 andalso p <= max_pri then () @@ -255,7 +230,7 @@ | rem_pri sym = sym; fun logify_types (a as (Argument (s, p))) = - if s <> "prop" andalso is_logtype s then Argument (logic, p) else a + if s <> "prop" andalso is_logtype s then Argument ("logic", p) else a | logify_types a = a; @@ -287,8 +262,9 @@ andalso not (null symbs) andalso not (exists is_delim symbs); val lhs' = - if convert andalso not copy_prod then - (if lhs = "prop" then sprop else if is_logtype lhs then logic else lhs) + if copy_prod orelse lhs = "prop" andalso symbs = [Argument ("prop'", 0)] then lhs + else if lhs = "prop" then "prop'" + else if is_logtype lhs then "logic" else lhs; val symbs' = map logify_types symbs; val xprod = XProd (lhs', symbs', const', pri); @@ -322,12 +298,12 @@ (* syn_ext *) -fun syn_ext' convert is_logtype mfixes consts trfuns (parse_rules, print_rules) = +fun syn_ext' is_logtype mfixes consts trfuns (parse_rules, print_rules) = let val (parse_ast_translation, parse_translation, print_translation, print_ast_translation) = trfuns; - val (xprods, parse_rules') = map (mfix_to_xprod convert is_logtype) mfixes + val (xprods, parse_rules') = map (mfix_to_xprod is_logtype) mfixes |> split_list |> apsnd (rev o flat); val mfix_consts = distinct (op =) (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods); @@ -344,7 +320,7 @@ end; -val syn_ext = syn_ext' true (K false); +val syn_ext = syn_ext' (K false); fun syn_ext_const_names cs = syn_ext [] cs ([], [], [], []) ([], []); fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) rules; @@ -365,14 +341,16 @@ val token_markers = ["_tfree", "_tvar", "_free", "_bound", "_var", "_numeral", "_inner_string"]; -val pure_ext = syn_ext' false (K false) - [Mfix ("_", spropT --> propT, "", [0], 0), - Mfix ("_", logicT --> anyT, "", [0], 0), - Mfix ("_", spropT --> anyT, "", [0], 0), - Mfix ("'(_')", logicT --> logicT, "", [0], max_pri), - Mfix ("'(_')", spropT --> spropT, "", [0], max_pri), - Mfix ("_::_", [logicT, typeT] ---> logicT, "_constrain", [4, 0], 3), - Mfix ("_::_", [spropT, typeT] ---> spropT, "_constrain", [4, 0], 3)] +val typ = Simple_Syntax.read_typ; + +val pure_ext = syn_ext' (K false) + [Mfix ("_", typ "prop' => prop", "", [0], 0), + Mfix ("_", typ "logic => any", "", [0], 0), + Mfix ("_", typ "prop' => any", "", [0], 0), + Mfix ("'(_')", typ "logic => logic", "", [0], max_pri), + Mfix ("'(_')", typ "prop' => prop'", "", [0], max_pri), + Mfix ("_::_", typ "logic => type => logic", "_constrain", [4, 0], 3), + Mfix ("_::_", typ "prop' => type => prop'", "_constrain", [4, 0], 3)] token_markers ([], [], [], []) ([], []); diff -r b3196458428b -r 6cca0343ea48 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Fri Apr 08 16:38:46 2011 +0200 +++ b/src/Pure/pure_thy.ML Fri Apr 08 17:45:37 2011 +0200 @@ -19,9 +19,6 @@ val tycon = Lexicon.mark_type; val const = Lexicon.mark_const; -val typeT = Syntax_Ext.typeT; -val spropT = Syntax_Ext.spropT; - (* application syntax variants *) @@ -143,7 +140,7 @@ ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\ _)", [0, 0], 0)), ("_ofsort", typ "tid => sort => type", Mixfix ("_\\_", [1000, 0], 1000)), ("_constrain", typ "logic => type => logic", Mixfix ("_\\_", [4, 0], 3)), - ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\\_", [4, 0], 3)), + ("_constrain", typ "prop' => type => prop'", Mixfix ("_\\_", [4, 0], 3)), ("_idtyp", typ "id_position => type => idt", Mixfix ("_\\_", [], 0)), ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\_", [], 0)), ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\_./ _)", [0, 3], 3)),