changed Pure's grammar and the way types are converted to nonterminals

--- a/src/Pure/Syntax/mixfix.ML	Thu Dec 08 12:45:28 1994 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Thu Dec 08 12:46:25 1994 +0100
@@ -78,7 +78,7 @@
 
 (* syn_ext_types *)
 
-fun syn_ext_types all_roots type_decls =
+fun syn_ext_types logtypes type_decls =
   let
     fun name_of (t, _, mx) = type_name t mx;
 
@@ -95,13 +95,13 @@
     val mfix = mapfilter mfix_of type_decls;
     val xconsts = map name_of type_decls;
   in
-    syn_ext all_roots [] mfix xconsts ([], [], [], []) ([], [])
+    syn_ext logtypes mfix xconsts ([], [], [], []) ([], [])
   end;
 
 
 (* syn_ext_consts *)
 
-fun syn_ext_consts all_roots const_decls =
+fun syn_ext_consts logtypes const_decls =
   let
     fun name_of (c, _, mx) = const_name c mx;
 
@@ -130,7 +130,7 @@
     val binder_trs = map mk_binder_tr binders;
     val binder_trs' = map (mk_binder_tr' o swap) binders;
   in
-    syn_ext all_roots [] mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
+    syn_ext logtypes mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
   end;
 
 
@@ -140,7 +140,7 @@
 val pure_types =
   map (fn t => (t, 0, NoSyn))
     (terminals @ [logic, "type", "types", "sort", "classes", args, "idt",
-      "idts", "aprop", "asms", "any"]);
+      "idts", "aprop", "asms"]);
 
 val pure_syntax =
  [("_lambda",   "[idts, 'a] => ('b => 'a)",       Mixfix ("(3%_./ _)", [], 0)),
@@ -163,7 +163,6 @@
   ("_K",        "'a",                             NoSyn),
   ("",          "id => logic",                    Delimfix "_"),
   ("",          "var => logic",                   Delimfix "_"),
-  ("_appl",     "[logic, args] => logic",         Mixfix ("(1_/(1'(_')))", [max_pri, 0], max_pri)),
-  ("_constrain", "[logic, type] => logic",        Mixfix ("_::_", [4, 0], 3))]
+  ("_appl",     "[logic, args] => logic",         Mixfix ("(1_/(1'(_')))", [max_pri, 0], max_pri))]
 
 end;

--- a/src/Pure/Syntax/parser.ML	Thu Dec 08 12:45:28 1994 +0100
+++ b/src/Pure/Syntax/parser.ML	Thu Dec 08 12:46:25 1994 +0100
@@ -260,40 +260,15 @@
 
 fun extend_gram (gram1 as Gram (prods1, _)) roots xprods2 =
   let
-    fun simplify preserve s = 
-      if preserve then 
-        (if s mem (roots \\ ["type", "prop", "any"]) then "logic" else s)
-      else (if s = "prop" then "@prop_H" else
-              (if s mem (roots \\ ["type", "prop", "any"]) then 
-                 "@logic_H" 
-               else s));
-
-    fun not_delim (Delim _) = false
-      | not_delim _ = true
-
-    fun symb_of _ (Delim s) = Some (Terminal (Token s))
-      | symb_of preserve (Argument (s, p)) =
+    fun symb_of (Delim s) = Some (Terminal (Token s))
+      | symb_of (Argument (s, p)) =
           (case predef_term s of
-            None => Some (Nonterminal (simplify preserve s, p))
+            None => Some (Nonterminal (s, p))
           | Some tk => Some (Terminal tk))
-      | symb_of _ _ = None;
+      | symb_of _ = None;
 
     fun prod_of (XProd (lhs, xsymbs, const, pri)) =
-      let val copy_prod = (lhs = "prop" andalso forall not_delim xsymbs andalso
-                           const <> "");
-
-          val preserve = copy_prod 
-                         orelse pri = chain_pri andalso lhs = "logic"
-                         orelse lhs mem ["@prop_H", "@logic_H", "any"];
-
-          val lhs' = if copy_prod then "@prop_H" else
-                     if lhs = "logic" andalso pri = chain_pri
-                        then "@logic_H"
-                     else if lhs mem ("logic1" :: (roots \\ ["type", "prop"])) 
-                        then "logic"
-                     else lhs;
-      in (lhs', (mapfilter (symb_of preserve) xsymbs, const, pri))
-      end;
+      (lhs, (mapfilter symb_of xsymbs, const, pri));
 
     val prods2 = distinct (map prod_of xprods2);
   in
@@ -583,10 +558,6 @@
 
 fun earley grammar startsymbol indata =
   let
-    val startsymbol' = case startsymbol of
-                           "logic" => "@logic_H"
-                         | "prop"  => "@prop_H"
-                         | other   => other;
     val rhss_ref = case assoc (grammar, startsymbol) of
                        Some r => r
                      | None   => error ("parse: Unknown startsymbol " ^ 

--- a/src/Pure/Syntax/syn_ext.ML	Thu Dec 08 12:45:28 1994 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Thu Dec 08 12:46:25 1994 +0100
@@ -32,7 +32,7 @@
     datatype mfix = Mfix of string * typ * string * int list * int
     datatype syn_ext =
       SynExt of {
-        roots: string list,
+        logtypes: string list,
         xprods: xprod list,
         consts: string list,
         parse_ast_translation: (string * (ast list -> ast)) list,
@@ -41,17 +41,23 @@
         print_translation: (string * (term list -> term)) list,
         print_rules: (ast * ast) list,
         print_ast_translation: (string * (ast list -> ast)) list}
-    val syn_ext: string list -> string list -> mfix list -> string list ->
+    val mk_syn_ext: bool -> string list -> mfix list ->
+      string list -> (string * (ast list -> ast)) list * 
+      (string * (term list -> term)) list *
+      (string * (term list -> term)) list * (string * (ast list -> ast)) list
+      -> (ast * ast) list * (ast * ast) list -> syn_ext
+    val syn_ext: string list -> mfix list -> string list ->
       (string * (ast list -> ast)) list * (string * (term list -> term)) list *
       (string * (term list -> term)) list * (string * (ast list -> ast)) list
       -> (ast * ast) list * (ast * ast) list -> syn_ext
-    val syn_ext_roots: string list -> string list -> syn_ext
+    val syn_ext_logtypes: string list -> syn_ext
     val syn_ext_const_names: string list -> string list -> syn_ext
     val syn_ext_rules: string list -> (ast * ast) list * (ast * ast) list -> syn_ext
     val syn_ext_trfuns: string list ->
       (string * (ast list -> ast)) list * (string * (term list -> term)) list *
       (string * (term list -> term)) list * (string * (ast list -> ast)) list
       -> syn_ext
+    val pure_ext: syn_ext
   end
 end;
 
@@ -70,19 +76,18 @@
 val logicT = Type (logic, []);
 
 val logic1 = "logic1";
-val logic1T = Type (logic1, []);
 
 val args = "args";
 val argsT = Type (args, []);
 
 val typeT = Type ("type", []);
 
-val funT = Type ("fun", []);
+val sprop = "#prop";
+val spropT = Type (sprop, []);
 
-val any = "any"
+val any = "any";
 val anyT = Type (any, []);
 
-
 (* constants *)
 
 val applC = "_appl";
@@ -145,19 +150,22 @@
 
 (* typ_to_nonterm *)
 
-fun typ_to_nonterm (Type (c, _)) = c
+(*get nonterminal for rhs*)
+fun typ_to_nonterm (Type (c, _)) = if c="fun" then logic else c
   | typ_to_nonterm _ = any;
 
-fun typ_to_nonterm1 (Type (c, _)) = c
-  | typ_to_nonterm1 _ = logic1;
+(*get nonterminal for lhs*)
+fun typ_to_nonterm1 (ty as Type (c, _)) = typ_to_nonterm ty
+  | typ_to_nonterm1 _ = logic;
 
 
 (* mfix_to_xprod *)
 
-fun mfix_to_xprod (Mfix (sy, typ, const, pris, pri)) =
+fun mfix_to_xprod convert logtypes (Mfix (sy, typ, const, pris, pri)) =
   let
     fun err msg =
-      (writeln ("Error in mixfix annotation " ^ quote sy ^ " for " ^ quote const);
+      (writeln ("Error in mixfix annotation " ^ quote sy ^ " for " 
+                ^ quote const);
         error msg);
 
     fun check_pri p =
@@ -218,21 +226,37 @@
     fun rem_pri (Argument (s, _)) = Argument (s, chain_pri)
       | rem_pri sym = sym;
 
+    fun is_delim (Delim _) = true
+      | is_delim _ = false;
+
+    (*replace logical types on rhs by "logic"*)
+    fun unify_logtypes copy_prod (a as (Argument (s, p))) =
+          if s mem logtypes then Argument (logic, p)
+          else a
+      | unify_logtypes _ a = a;
 
     val (raw_symbs, _) = repeat scan_symb (explode sy);
     val (symbs, lhs) = add_args raw_symbs typ pris;
-    val xprod = XProd (lhs, symbs, const, pri);
+    val copy_prod = lhs mem ["prop", "logic"]
+          andalso const <> ""
+          andalso not (exists is_delim symbs);
+    val lhs' = if convert andalso not copy_prod then
+                 (if lhs mem logtypes then logic
+                  else if lhs = "prop" then sprop else lhs)
+               else lhs;
+    val symbs' = map (unify_logtypes copy_prod) symbs;
+    val xprod = XProd (lhs', symbs', const, pri);
   in
     seq check_pri pris;
     check_pri pri;
-    check_blocks symbs;
+    check_blocks symbs';
 
-    if is_terminal lhs then err ("illegal lhs: " ^ lhs)
+    if is_terminal lhs' then err ("illegal lhs: " ^ lhs')
     else if const <> "" then xprod
-    else if length (filter is_arg symbs) <> 1 then
+    else if length (filter is_arg symbs') <> 1 then
       err "copy production must have exactly one argument"
-    else if exists is_term symbs then xprod
-    else XProd (lhs, map rem_pri symbs, "", chain_pri)
+    else if exists is_term symbs' then xprod
+    else XProd (lhs', map rem_pri symbs', "", chain_pri)
   end;
 
 
@@ -240,7 +264,7 @@
 
 datatype syn_ext =
   SynExt of {
-    roots: string list,
+    logtypes: string list,
     xprods: xprod list,
     consts: string list,
     parse_ast_translation: (string * (ast list -> ast)) list,
@@ -253,31 +277,18 @@
 
 (* syn_ext *)
 
-fun syn_ext all_roots new_roots mfixes consts trfuns rules =
+fun mk_syn_ext convert logtypes mfixes consts trfuns rules =
   let
     val (parse_ast_translation, parse_translation, print_translation,
       print_ast_translation) = trfuns;
     val (parse_rules, print_rules) = rules;
+    val logtypes' = logtypes \ "prop";
 
     val mfix_consts = distinct (map (fn (Mfix (_, _, c, _, _)) => c) mfixes);
-    val mfixes' = (if "prop" mem new_roots then
-                     [Mfix ("'(_')", Type ("@prop_H", [])
-                            --> Type ("@prop_H", []), "", [0], max_pri),
-                      Mfix ("'(_')", Type ("@logic_H", []) 
-                            --> Type ("@logic_H", []), "", [0], max_pri),
-                      Mfix ("'(_')", anyT --> anyT, "", [0], max_pri),
-                      Mfix ("_", propT --> Type ("@prop_H", []), "", [0], 0),
-                      Mfix ("_", propT --> anyT, "", [0], 0)]
-                   else []) @
-                   (if all_roots = new_roots then
-                     [Mfix ("_", logicT --> Type ("@logic_H", []), "", [0], 0),
-                      Mfix ("_", logicT --> anyT, "", [0], 0)]
-                    else [])    
-    val xprods = map mfix_to_xprod mfixes 
-                 @ map mfix_to_xprod mfixes';
+    val xprods = map (mfix_to_xprod convert logtypes') mfixes;
   in
     SynExt {
-      roots = new_roots,
+      logtypes = logtypes',
       xprods = xprods,
       consts = filter is_xid (consts union mfix_consts),
       parse_ast_translation = parse_ast_translation,
@@ -288,18 +299,32 @@
       print_ast_translation = print_ast_translation}
   end;
 
+val syn_ext = mk_syn_ext true;
 
-fun syn_ext_roots roots new_roots =
-  syn_ext roots new_roots [] [] ([], [], [], []) ([], []);
+fun syn_ext_logtypes logtypes =
+  syn_ext logtypes [] [] ([], [], [], []) ([], []);
+
+fun syn_ext_const_names logtypes cs =
+  syn_ext logtypes [] cs ([], [], [], []) ([], []);
 
-fun syn_ext_const_names roots cs =
-  syn_ext roots [] [] cs ([], [], [], []) ([], []);
+fun syn_ext_rules logtypes rules =
+  syn_ext logtypes [] [] ([], [], [], []) rules;
+
+fun syn_ext_trfuns logtypes trfuns =
+  syn_ext logtypes [] [] trfuns ([], []);
 
-fun syn_ext_rules roots rules =
-  syn_ext roots [] [] [] ([], [], [], []) rules;
+(* pure_ext *)
 
-fun syn_ext_trfuns roots trfuns =
-  syn_ext roots [] [] [] trfuns ([], []);
-
+val pure_ext = mk_syn_ext 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)]
+  []
+  ([], [], [], [])
+  ([], []);
 
 end;

--- a/src/Pure/Syntax/syntax.ML	Thu Dec 08 12:45:28 1994 +0100
+++ b/src/Pure/Syntax/syntax.ML	Thu Dec 08 12:46:25 1994 +0100
@@ -47,6 +47,7 @@
     (bool -> term list * typ -> int * term * 'a) -> xrule list -> syntax
   val merge_syntaxes: syntax -> syntax -> syntax
   val type_syn: syntax
+  val pure_syn: syntax
   val print_gram: syntax -> unit
   val print_trans: syntax -> unit
   val print_syntax: syntax -> unit
@@ -134,7 +135,7 @@
 datatype syntax =
   Syntax of {
     lexicon: lexicon,
-    roots: string list,
+    logtypes: string list,
     gram: gram,
     consts: string list,
     parse_ast_trtab: ast trtab,
@@ -151,7 +152,7 @@
 val empty_syntax =
   Syntax {
     lexicon = empty_lexicon,
-    roots = [],
+    logtypes = [],
     gram = empty_gram,
     consts = [],
     parse_ast_trtab = empty_trtab,
@@ -167,17 +168,17 @@
 
 fun extend_syntax (Syntax tabs) syn_ext =
   let
-    val {lexicon, roots = roots1, gram, consts = consts1, parse_ast_trtab,
+    val {lexicon, logtypes = logtypes1, gram, consts = consts1, parse_ast_trtab,
       parse_ruletab, parse_trtab, print_trtab, print_ruletab, print_ast_trtab,
       prtab} = tabs;
-    val SynExt {roots = roots2, xprods, consts = consts2, parse_ast_translation,
+    val SynExt {logtypes = logtypes2, xprods, consts = consts2, parse_ast_translation,
       parse_rules, parse_translation, print_translation, print_rules,
       print_ast_translation} = syn_ext;
   in
     Syntax {
       lexicon = extend_lexicon lexicon (delims_of xprods),
-      roots = extend_list roots1 roots2,
-      gram = extend_gram gram (roots1 @ roots2) xprods,
+      logtypes = extend_list logtypes1 logtypes2,
+      gram = extend_gram gram (logtypes1 @ logtypes2) xprods,
       consts = consts2 union consts1,
       parse_ast_trtab =
         extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation",
@@ -195,13 +196,13 @@
 
 fun merge_syntaxes (Syntax tabs1) (Syntax tabs2) =
   let
-    val {lexicon = lexicon1, roots = roots1, gram = gram1, consts = consts1,
+    val {lexicon = lexicon1, logtypes = logtypes1, gram = gram1, consts = consts1,
       parse_ast_trtab = parse_ast_trtab1, parse_ruletab = parse_ruletab1,
       parse_trtab = parse_trtab1, print_trtab = print_trtab1,
       print_ruletab = print_ruletab1, print_ast_trtab = print_ast_trtab1,
       prtab = prtab1} = tabs1;
 
-    val {lexicon = lexicon2, roots = roots2, gram = gram2, consts = consts2,
+    val {lexicon = lexicon2, logtypes = logtypes2, gram = gram2, consts = consts2,
       parse_ast_trtab = parse_ast_trtab2, parse_ruletab = parse_ruletab2,
       parse_trtab = parse_trtab2, print_trtab = print_trtab2,
       print_ruletab = print_ruletab2, print_ast_trtab = print_ast_trtab2,
@@ -209,7 +210,7 @@
   in
     Syntax {
       lexicon = merge_lexicons lexicon1 lexicon2,
-      roots = merge_lists roots1 roots2,
+      logtypes = merge_lists logtypes1 logtypes2,
       gram = merge_grams gram1 gram2,
       consts = merge_lists consts1 consts2,
       parse_ast_trtab =
@@ -227,7 +228,7 @@
 (* type_syn *)
 
 val type_syn = extend_syntax empty_syntax type_ext;
-
+val pure_syn = extend_syntax type_syn pure_ext;
 
 
 (** inspect syntax **)
@@ -240,10 +241,10 @@
 
 fun print_gram (Syntax tabs) =
   let
-    val {lexicon, roots, gram, ...} = tabs;
+    val {lexicon, logtypes, gram, ...} = tabs;
   in
     Pretty.writeln (pretty_strs_qs "lexicon:" (dest_lexicon lexicon));
-    Pretty.writeln (Pretty.strs ("roots:" :: roots));
+    Pretty.writeln (Pretty.strs ("logtypes:" :: logtypes));
     Pretty.writeln (Pretty.big_list "prods:" (pretty_gram gram))
   end;
 
@@ -304,9 +305,8 @@
 
 fun read_asts (Syntax tabs) print_msg xids root str =
   let
-    val {lexicon, gram, parse_ast_trtab, roots, ...} = tabs;
-    val root' = if root mem (roots \\ ["type", "prop"]) then "@logic_H"
-                else if root = "prop" then "@prop_H" else root;
+    val {lexicon, gram, parse_ast_trtab, logtypes, ...} = tabs;
+    val root' = if root mem logtypes then logic else root;
     val pts = parse gram root' (tokenize lexicon xids str);
 
     fun show_pt pt = writeln (str_of_ast (pt_to_ast (K None) pt));
@@ -436,12 +436,12 @@
 
 (** extend syntax (external interfaces) **)
 
-fun ext_syntax mk_syn_ext (syn as Syntax {roots, ...}) decls =
-  extend_syntax syn (mk_syn_ext roots decls);
+fun ext_syntax mk_syn_ext (syn as Syntax {logtypes, ...}) decls =
+  extend_syntax syn (mk_syn_ext logtypes decls);
 
 
-fun extend_log_types (syn as Syntax {roots, ...}) all_roots =
-  extend_syntax syn (syn_ext_roots all_roots (all_roots \\ roots));
+fun extend_log_types syn logtypes =
+  extend_syntax syn (syn_ext_logtypes logtypes);
 
 val extend_type_gram = ext_syntax syn_ext_types;
 

--- a/src/Pure/Syntax/type_ext.ML	Thu Dec 08 12:45:28 1994 +0100
+++ b/src/Pure/Syntax/type_ext.ML	Thu Dec 08 12:46:25 1994 +0100
@@ -157,8 +157,7 @@
 val classesT = Type ("classes", []);
 val typesT = Type ("types", []);
 
-val type_ext = syn_ext
-  [logic, "type"] [logic, "type"]
+val type_ext = mk_syn_ext false []
   [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
    Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
    Mfix ("_",           idT --> typeT,                 "", [], max_pri),
@@ -185,4 +184,3 @@
 
 
 end;
-