# HG changeset patch
# User clasohm
# Date 790425364 -3600
# Node ID b38c67991122e785c98188b82414c49c89fe9431
# Parent  d63b111b917a60f7f3de7e5b6717ce81b2574958
added optional precedence for body of binder;
removed call to infer_types from read_xrules

diff -r d63b111b917a -r b38c67991122 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Wed Jan 18 10:17:55 1995 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Wed Jan 18 11:36:04 1995 +0100
@@ -13,7 +13,7 @@
     Delimfix of string |
     Infixl of int |
     Infixr of int |
-    Binder of string * int
+    Binder of string * int * int
   val max_pri: int
 end;
 
@@ -52,7 +52,7 @@
   Delimfix of string |
   Infixl of int |
   Infixr of int |
-  Binder of string * int;
+  Binder of string * int * int
 
 
 (* type / const names *)
@@ -118,10 +118,10 @@
       | mfix_of (c, ty, Delimfix sy) = [Mfix (sy, ty, c, [], max_pri)]
       | mfix_of (sy, ty, Infixl p) = mk_infix sy ty (infix_name sy) p (p + 1) p
       | mfix_of (sy, ty, Infixr p) = mk_infix sy ty (infix_name sy) (p + 1) p p
-      | mfix_of (c, ty, Binder (sy, p)) =
-          [Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, sy, [], p)];
+      | mfix_of (c, ty, Binder (sy, p2, p)) =
+          [Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, sy, [0, p2], p)];
 
-    fun binder (c, _, Binder (sy, _)) = Some (sy, c)
+    fun binder (c, _, Binder (sy, _, _)) = Some (sy, c)
       | binder _ = None;
 
     val mfix = flat (map mfix_of const_decls);
diff -r d63b111b917a -r b38c67991122 src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Wed Jan 18 10:17:55 1995 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Wed Jan 18 11:36:04 1995 +0100
@@ -151,13 +151,14 @@
 
 (* typ_to_nonterm *)
 
+fun typ_to_nt _ (Type (c, _)) = c
+  | typ_to_nt default _ = default;
+
 (*get nonterminal for rhs*)
-fun typ_to_nonterm (Type (c, _)) = c
-  | typ_to_nonterm _ = any;
+val typ_to_nonterm = typ_to_nt any;
 
 (*get nonterminal for lhs*)
-fun typ_to_nonterm1 (Type (c, _)) = c
-  | typ_to_nonterm1 _ = logic;
+val typ_to_nonterm1 = typ_to_nt logic;
 
 
 (* mfix_to_xprod *)
diff -r d63b111b917a -r b38c67991122 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Wed Jan 18 10:17:55 1995 +0100
+++ b/src/Pure/Syntax/syntax.ML	Wed Jan 18 11:36:04 1995 +0100
@@ -43,8 +43,7 @@
     (string * (term list -> term)) list *
     (string * (term list -> term)) list *
     (string * (ast list -> ast)) list -> syntax
-  val extend_trrules: syntax ->
-    (bool -> term list * typ -> int * term * 'a) -> xrule list -> syntax
+  val extend_trrules: syntax -> xrule list -> syntax
   val merge_syntaxes: syntax -> syntax -> syntax
   val type_syn: syntax
   val pure_syn: syntax
@@ -303,7 +302,7 @@
 
 (* read_ast *)
 
-fun read_asts (Syntax tabs) print_msg xids root str =
+fun read_asts (Syntax tabs) xids root str =
   let
     val {lexicon, gram, parse_ast_trtab, logtypes, ...} = tabs;
     val root' = if root mem logtypes then logic else root;
@@ -311,7 +310,7 @@
 
     fun show_pt pt = writeln (str_of_ast (pt_to_ast (K None) pt));
   in
-    if print_msg andalso length pts > 1 then
+    if length pts > 1 then
       (writeln ("Warning: Ambiguous input " ^ quote str);
        writeln "produces the following parse trees:"; seq show_pt pts)
     else ();
@@ -324,7 +323,7 @@
 fun read (syn as Syntax tabs) ty str =
   let
     val {parse_ruletab, parse_trtab, ...} = tabs;
-    val asts = read_asts syn true false (typ_to_nonterm ty) str;
+    val asts = read_asts syn false (typ_to_nonterm ty) str;
   in
     map (ast_to_term (lookup_trtab parse_trtab))
       (map (normalize_ast (lookup_ruletab parse_ruletab)) asts)
@@ -348,10 +347,9 @@
 fun simple_read_typ str = read_typ type_syn (K []) str;
 
 
-(* read rules *)
+(* read translation rules *)
 
-fun read_rule (syn as Syntax tabs) print_msg
-              (check_types: bool -> term list * typ -> int * term * 'a)
+fun read_xrule (syn as Syntax tabs)
               (xrule as ((_, lhs_src), (_, rhs_src))) =
   let
     val Syntax {consts, ...} = syn;
@@ -362,19 +360,12 @@
       | constantify (Appl asts) = Appl (map constantify asts);
 
     fun read_pat (root, 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)
+      let val asts = read_asts syn true root str;
+      in if length asts > 1 then
+           error "Error: This should not happen while parsing a syntax \
+                  \translation rule."
+         else constantify (hd asts)
+            handle ERROR => error ("The error above occurred in " ^ quote str)
       end;
 
     val rule as (lhs, rhs) = (pairself read_pat) xrule;
@@ -393,7 +384,7 @@
   op <-| of (string * string) * (string * string) |
   op <-> of (string * string) * (string * string);
 
-fun read_xrules syn check_types xrules =
+fun read_xrules syn xrules =
   let
     fun right_rule (xpat1 |-> xpat2) = Some (xpat1, xpat2)
       | right_rule (xpat1 <-| xpat2) = None
@@ -402,12 +393,8 @@
     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 true check_types) rrules,
-     map (read_rule syn (rrules = []) check_types) lrules)
+  in (map (read_xrule syn) (mapfilter right_rule xrules),
+      map (read_xrule syn) (mapfilter left_rule xrules))
   end;
 
 
@@ -451,7 +438,7 @@
 
 val extend_trfuns = ext_syntax syn_ext_trfuns;
 
-fun extend_trrules syn check_types xrules =
-  ext_syntax syn_ext_rules syn (read_xrules syn check_types xrules);
+fun extend_trrules syn xrules =
+  ext_syntax syn_ext_rules syn (read_xrules syn xrules);
 
 end;
diff -r d63b111b917a -r b38c67991122 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Wed Jan 18 10:17:55 1995 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Wed Jan 18 11:36:04 1995 +0100
@@ -212,7 +212,12 @@
 val infxl = "infixl" $$-- !! nat >> cat "Infixl";
 val infxr = "infixr" $$-- !! nat >> cat "Infixr";
 
-val binder = "binder" $$-- !! (string -- nat) >> (cat "Binder" o mk_pair);
+fun mk_binder ((name, x), y) =
+  let val (p1, p2) = if y = "None" then ("0", x) else (x, y);
+  in mk_triple (name, p1, p2) end;
+
+val binder = "binder" $$-- !! (string -- nat -- optional nat "None") 
+             >> (cat "Binder" o mk_binder);
 
 val opt_pris = optional ("[" $$-- !! (list nat --$$ "]")) [] >> mk_list;
 
diff -r d63b111b917a -r b38c67991122 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Jan 18 10:17:55 1995 +0100
+++ b/src/Pure/sign.ML	Wed Jan 18 11:36:04 1995 +0100
@@ -428,9 +428,7 @@
   (Syntax.extend_trfuns syn trfuns, tsig, ctab);
 
 fun ext_trrules (syn, tsig, ctab) xrules =
-  (Syntax.extend_trrules syn
-  (infer_types (Sg {tsig = tsig, const_tab = ctab, syn = syn, 
-                   stamps = [ref "#"]}) (K None) (K None)) xrules, tsig, ctab);
+  (Syntax.extend_trrules syn xrules, tsig, ctab);
 
 
 (* build signature *)
@@ -530,7 +528,7 @@
    [("==", "['a::{}, 'a] => prop", Mixfix ("(_ ==/ _)", [3, 2], 2)),
     ("=?=", "['a::{}, 'a] => prop", Mixfix ("(_ =?=/ _)", [3, 2], 2)),
     ("==>", "[prop, prop] => prop", Mixfix ("(_ ==>/ _)", [2, 1], 1)),
-    ("all", "('a => prop) => prop", Binder ("!!", 0)),
+    ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
     ("TYPE", "'a itself", NoSyn)]
   |> add_name "Pure";