made major changes to grammar;
added call of Type.infer_types to automatically eliminate ambiguities

--- a/src/Pure/Syntax/mixfix.ML	Tue Oct 04 13:01:17 1994 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Tue Oct 04 13:02:16 1994 +0100
@@ -140,7 +140,7 @@
 val pure_types =
   map (fn t => (t, 0, NoSyn))
     (terminals @ [logic, "type", "types", "sort", "classes", args, "idt",
-      "idts", "aprop", "asms"]);
+      "idts", "aprop", "asms", "any"]);
 
 val pure_syntax =
  [("_lambda",   "[idts, 'a] => ('b => 'a)",       Mixfix ("(3%_./ _)", [], 0)),
@@ -162,8 +162,10 @@
   ("_ofclass",  "[type, 'a] => prop",             Delimfix "(1OFCLASS/(1'(_,/ _')))"),
   ("_K",        "'a",                             NoSyn),
   ("_explode",  "'a",                             NoSyn),
-  ("_implode",  "'a",                             NoSyn)];
-
+  ("_implode",  "'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 ("_::_", [max_pri, 0], 999))]
 
 end;
-

--- a/src/Pure/Syntax/parser.ML	Tue Oct 04 13:01:17 1994 +0100
+++ b/src/Pure/Syntax/parser.ML	Tue Oct 04 13:02:16 1994 +0100
@@ -12,7 +12,7 @@
   local open Lexicon SynExt SynExt.Ast in
     type gram
     val empty_gram: gram
-    val extend_gram: gram -> xprod list -> gram
+    val extend_gram: gram -> string list -> xprod list -> gram
     val merge_grams: gram -> gram -> gram
     val pretty_gram: gram -> Pretty.T list
     datatype parsetree =
@@ -257,17 +257,42 @@
 
 val empty_gram = mk_gram [];
 
-fun extend_gram (gram1 as Gram (prods1, _)) xprods2 =
+fun extend_gram (gram1 as Gram (prods1, _)) roots xprods2 =
   let
-    fun symb_of (Delim s) = Some (Terminal (Token s))
-      | symb_of (Argument (s, p)) =
+    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)) =
           (case predef_term s of
-            None => Some (Nonterminal (s, p))
+            None => Some (Nonterminal (simplify preserve s, p))
           | Some tk => Some (Terminal tk))
-      | symb_of _ = None;
+      | symb_of _ _ = None;
 
     fun prod_of (XProd (lhs, xsymbs, const, pri)) =
-      (lhs, (mapfilter symb_of 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;
 
     val prods2 = distinct (map prod_of xprods2);
   in
@@ -553,10 +578,14 @@
 
 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 " ^ 
-                                      quote startsymbol);
+                     | None   => error ("parse: Unknown startsymbol " ^ 
+                                        quote startsymbol);
     val S0 = [(ref [], 0, [], [Nonterm (rhss_ref, 0), Term EndToken], "", 0)];
     val s = length indata + 1;
     val Estate = Array.array (s, []);
@@ -564,15 +593,17 @@
     Array.update (Estate, 0, S0);
     let
       val l = produce Estate 0 indata EndToken(*dummy*);
+
       val p_trees = get_trees l;
     in p_trees end
   end;
 
 
 fun parse (Gram (_, prod_tab)) start toks =
+let val r =
   (case earley prod_tab start toks of
     [] => sys_error "parse: no parse trees"
   | pts => pts);
+in r end
 
 end;
-

--- a/src/Pure/Syntax/syn_ext.ML	Tue Oct 04 13:01:17 1994 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Tue Oct 04 13:02:16 1994 +0100
@@ -79,6 +79,9 @@
 
 val funT = Type ("fun", []);
 
+val any = "any"
+val anyT = Type (any, []);
+
 
 (* constants *)
 
@@ -143,7 +146,7 @@
 (* typ_to_nonterm *)
 
 fun typ_to_nonterm (Type (c, _)) = c
-  | typ_to_nonterm _ = logic;
+  | typ_to_nonterm _ = any;
 
 fun typ_to_nonterm1 (Type (c, _)) = c
   | typ_to_nonterm1 _ = logic1;
@@ -256,78 +259,26 @@
       print_ast_translation) = trfuns;
     val (parse_rules, print_rules) = rules;
 
-    val Troots = map (apr (Type, [])) new_roots;
-    val Troots' = Troots \\ [typeT, propT];
-
-    fun change_name T ext =
-      let val Type (name, ts) = T
-      in Type ("@" ^ name ^ ext, ts) end;
-
-    (* Append "_H" to lhs if production is not a copy or chain production *)
-    fun hide_xprod roots (XProd (lhs, symbs, const, pri)) =
-      let fun is_delim (Delim _) = true
-            | is_delim _ = false
-      in if const <> "" andalso lhs mem roots andalso exists is_delim symbs then
-           XProd ("@" ^ lhs ^ "_H", symbs, const, pri)
-         else XProd (lhs, symbs, const, pri)
-      end;
-
-    (* Make descend production and append "_H" to rhs nonterminal *)
-    fun descend_right (from, to) =
-      Mfix ("_", change_name to "_H" --> from, "", [0], 0);
-
-    (* Make descend production and append "_H" to lhs *)
-    fun descend_left (from, to) =
-      Mfix ("_", to --> change_name from "_H", "", [0], 0);
-
-    (* Make descend production and append "_A" to lhs *)
-    fun descend1 (from, to) =
-      Mfix ("_", to --> change_name from "_A", "", [0], 0);
-
-    (* Make parentheses production for 'hidden' and 'automatic' nonterminal *)
-    fun parents T =
-      if T = typeT then
-        [Mfix ("'(_')", T --> T, "", [0], max_pri)]
-      else
-        [Mfix ("'(_')", change_name T "_H" --> change_name T "_H", "", [0], max_pri),
-         Mfix ("'(_')", change_name T "_A" --> change_name T "_A", "", [0], max_pri)];
-
-    fun mkappl T =
-      Mfix ("(1_/(1'(_')))", [funT, argsT] ---> change_name T "_A", applC,
-            [max_pri, 0], max_pri);
-
-    fun mkid T =
-      Mfix ("_", idT --> change_name T "_A", "", [], max_pri);
-
-    fun mkvar T =
-      Mfix ("_", varT --> change_name T "_A", "", [], max_pri);
-
-    fun constrain T =
-      Mfix ("_::_", [T, typeT] ---> change_name T "_A", constrainC,
-            [4, 0], 3)
-
-    fun unhide T =
-      if T <> logicT then
-        [Mfix ("_", change_name T "_H" --> T, "", [0], 0),
-         Mfix ("_", change_name T "_A" --> T, "", [0], 0)]
-      else
-        [Mfix ("_", change_name T "_A" --> T, "", [0], 0)];
-
-    val mfixes' = flat (map parents Troots) @ map mkappl Troots' @
-      map mkid Troots' @ map mkvar Troots' @ map constrain Troots' @
-      map (apl (logicT, descend_right)) (Troots \\ [logicT, typeT]) @
-      map (apr (descend1, logic1T)) (Troots') @
-      flat (map unhide (Troots \\ [typeT]));
-    val mfix_consts =
-      distinct (map (fn (Mfix (_, _, c, _, _)) => c) (mfixes @ mfixes'));
-    val xprods = map mfix_to_xprod mfixes;
-    val xprods' = map mfix_to_xprod mfixes';
+    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';
   in
     SynExt {
       roots = new_roots,
-      xprods = (map (hide_xprod (all_roots \\ ["logic", "type"])) xprods)
-               @ xprods',    (* hide only productions that weren't created
-                                automatically *)
+      xprods = xprods,
       consts = filter is_xid (consts union mfix_consts),
       parse_ast_translation = parse_ast_translation,
       parse_rules = parse_rules,
@@ -352,4 +303,3 @@
 
 
 end;
-

--- a/src/Pure/Syntax/syntax.ML	Tue Oct 04 13:01:17 1994 +0100
+++ b/src/Pure/Syntax/syntax.ML	Tue Oct 04 13:02:16 1994 +0100
@@ -43,14 +43,15 @@
     (string * (term list -> term)) list *
     (string * (term list -> term)) list *
     (string * (ast list -> ast)) list -> syntax
-  val extend_trrules: syntax -> xrule list -> syntax
+  val extend_trrules: syntax ->
+    (bool -> term list * typ -> int * term * 'a) -> xrule list -> syntax
   val merge_syntaxes: syntax -> syntax -> syntax
   val type_syn: syntax
   val print_gram: syntax -> unit
   val print_trans: syntax -> unit
   val print_syntax: syntax -> unit
   val test_read: syntax -> string -> string -> unit
-  val read: syntax -> typ -> string -> term
+  val read: syntax -> typ -> string -> term list
   val read_typ: syntax -> (indexname -> sort) -> string -> typ
   val simple_read_typ: string -> typ
   val pretty_term: syntax -> term -> Pretty.T
@@ -176,7 +177,7 @@
     Syntax {
       lexicon = extend_lexicon lexicon (delims_of xprods),
       roots = extend_list roots1 roots2,
-      gram = extend_gram gram xprods,
+      gram = extend_gram gram (roots1 @ roots2) xprods,
       consts = consts2 union consts1,
       parse_ast_trtab =
         extend_trtab parse_ast_trtab parse_ast_translation "parse ast translation",
@@ -285,7 +286,7 @@
     val {lexicon, gram, parse_ast_trtab, parse_ruletab, ...} = tabs;
 
     val toks = tokenize lexicon false str;
-    val _ = writeln ("tokens: " ^ space_implode " " (map display_token toks))
+    val _ = writeln ("tokens: " ^ space_implode " " (map display_token toks));
 
     fun show_pt pt =
       let
@@ -301,20 +302,20 @@
 
 (* read_ast *)
 
-fun read_ast (Syntax tabs) xids root str =
+fun read_asts (Syntax tabs) print_msg xids root str =
   let
-    val {lexicon, gram, parse_ast_trtab, ...} = tabs;
-    val pts = parse gram root (tokenize lexicon xids str);
+    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 pts = parse gram root' (tokenize lexicon xids str);
 
-    fun show_pt pt =
-      writeln (str_of_ast (pt_to_ast (K None) pt));
+    fun show_pt pt = writeln (str_of_ast (pt_to_ast (K None) pt));
   in
-    (case pts of
-      [pt] => pt_to_ast (lookup_trtab parse_ast_trtab) pt
-    | _ =>
-      (writeln ("Ambiguous input " ^ quote str);
-        writeln "produces the following parse trees:"; seq show_pt pts;
-        error "Please disambiguate the grammar or your input."))
+    if print_msg andalso length pts > 1 then
+      (writeln ("Warning: Ambiguous input " ^ quote str);
+       writeln "produces the following parse trees:"; seq show_pt pts)
+    else ();
+    map (pt_to_ast (lookup_trtab parse_ast_trtab)) pts
   end;
 
 
@@ -323,10 +324,10 @@
 fun read (syn as Syntax tabs) ty str =
   let
     val {parse_ruletab, parse_trtab, ...} = tabs;
-    val ast = read_ast syn false (typ_to_nonterm ty) str;
+    val asts = read_asts syn true false (typ_to_nonterm ty) str;
   in
-    ast_to_term (lookup_trtab parse_trtab)
-      (normalize_ast (lookup_ruletab parse_ruletab) ast)
+    map (ast_to_term (lookup_trtab parse_trtab))
+      (map (normalize_ast (lookup_ruletab parse_ruletab)) asts)
   end;
 
 
@@ -334,7 +335,11 @@
 
 fun read_typ syn def_sort str =
   let
-    val t = read syn typeT str;
+    val ts = read syn typeT str;
+    val t = case ts of
+                [t'] => t'
+              | _ => error "This should not happen while parsing a type.\n\
+                           \Please check your type syntax for ambiguities!";
     val sort_env = raw_term_sorts t;
   in
     typ_of_term sort_env def_sort t
@@ -345,7 +350,9 @@
 
 (* read rules *)
 
-fun read_rule syn (xrule as ((_, lhs_src), (_, rhs_src))) =
+fun read_rule (syn as Syntax tabs) print_msg
+              (check_types: bool -> term list * typ -> int * term * 'a)
+              (xrule as ((_, lhs_src), (_, rhs_src))) =
   let
     val Syntax {consts, ...} = syn;
 
@@ -355,8 +362,20 @@
       | constantify (Appl asts) = Appl (map constantify asts);
 
     fun read_pat (root, str) =
-      constantify (read_ast syn true root str)
-        handle ERROR => error ("The error above occurred in " ^ quote str);
+      let val {parse_ruletab, parse_trtab, ...} = tabs;
+          val asts = read_asts syn print_msg true root str;
+          val ts = map (ast_to_term (lookup_trtab parse_trtab))
+                     (map (normalize_ast (lookup_ruletab parse_ruletab)) asts);
+
+          val idx = if length ts = 1 then 0
+            else (if print_msg then
+                    writeln ("This occured in syntax translation rule: " ^
+                             quote lhs_src ^ "  ->  " ^ quote rhs_src)
+                  else ();
+                  #1 (check_types print_msg (ts, Type (root, []))))
+      in constantify (nth_elem (idx, asts))
+           handle ERROR => error ("The error above occurred in " ^ quote str)
+      end;
 
     val rule as (lhs, rhs) = (pairself read_pat) xrule;
   in
@@ -374,7 +393,7 @@
   op <-| of (string * string) * (string * string) |
   op <-> of (string * string) * (string * string);
 
-fun read_xrules syn xrules =
+fun read_xrules syn check_types xrules =
   let
     fun right_rule (xpat1 |-> xpat2) = Some (xpat1, xpat2)
       | right_rule (xpat1 <-| xpat2) = None
@@ -383,9 +402,12 @@
     fun left_rule (xpat1 |-> xpat2) = None
       | left_rule (xpat1 <-| xpat2) = Some (xpat2, xpat1)
       | left_rule (xpat1 <-> xpat2) = Some (xpat2, xpat1);
+
+    val rrules = mapfilter right_rule xrules;
+    val lrules = mapfilter left_rule xrules;
   in
-    (map (read_rule syn) (mapfilter right_rule xrules),
-     map (read_rule syn) (mapfilter left_rule xrules))
+    (map (read_rule syn true check_types) rrules,
+     map (read_rule syn (rrules = []) check_types) lrules)
   end;
 
 
@@ -429,9 +451,7 @@
 
 val extend_trfuns = ext_syntax syn_ext_trfuns;
 
-fun extend_trrules syn xrules =
-  ext_syntax syn_ext_rules syn (read_xrules syn xrules);
-
+fun extend_trrules syn check_types xrules =
+  ext_syntax syn_ext_rules syn (read_xrules syn check_types xrules);
 
 end;
-

--- a/src/Pure/Syntax/type_ext.ML	Tue Oct 04 13:01:17 1994 +0100
+++ b/src/Pure/Syntax/type_ext.ML	Tue Oct 04 13:02:16 1994 +0100
@@ -177,7 +177,8 @@
    Mfix ("_",           typeT --> typesT,              "", [], max_pri),
    Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
    Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
-   Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0)]
+   Mfix ("([_]/ => _)", [typesT, typeT] ---> typeT,    "_bracket", [0, 0], 0),
+   Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri)]
   []
   ([("_tapp", tapp_ast_tr), ("_tappl", tappl_ast_tr), ("_bracket", bracket_ast_tr)],
    [],