# HG changeset patch
# User haftmann
# Date 1208335837 -7200
# Node ID a3ae088dc20f07e6e8717c5aba5320858a7c7247
# Parent  ab629324081cdb7113bcc6468dc991c4d84424e3
educated guess for infix syntax

diff -r ab629324081c -r a3ae088dc20f src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Wed Apr 16 02:25:06 2008 +0200
+++ b/src/Pure/Syntax/parser.ML	Wed Apr 16 10:50:37 2008 +0200
@@ -17,6 +17,7 @@
     Node of string * parsetree list |
     Tip of Lexicon.token
   val parse: gram -> string -> Lexicon.token list -> parsetree list
+  val guess_infix_lr: gram -> string -> (string * bool * bool * int) option
   val branching_level: int ref
 end;
 
@@ -832,6 +833,20 @@
   (case earley prods tags chains start (toks @ [Lexicon.EndToken]) of
     [] => sys_error "parse: no parse trees"
   | pts => pts);
-in r end
+in r end;
+
+
+fun guess_infix_lr (Gram gram) c = (*based on educated guess*)
+  let
+    fun freeze a = map (curry Array.sub a) (0 upto Array.length a - 1);
+    val prods = (maps snd o maps snd o freeze o #prods) gram;
+    fun guess (SOME ([Nonterminal (_, k), Terminal (Token s), Nonterminal (_, l)], _, j)) =
+          if k = j andalso l = j + 1 then SOME (s, true, false, j)
+          else if k = j + 1 then if l = j then SOME (s, false, true, j)
+            else if l = j + 1 then SOME (s, false, false, j)
+            else NONE
+          else NONE
+      | guess _ = NONE;
+  in guess (find_first (fn (_, s, _) => s = c) prods) end;
 
 end;
diff -r ab629324081c -r a3ae088dc20f src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Wed Apr 16 02:25:06 2008 +0200
+++ b/src/Pure/Syntax/syntax.ML	Wed Apr 16 10:50:37 2008 +0200
@@ -141,6 +141,7 @@
   val string_of_sort: Proof.context -> sort -> string
   val string_of_classrel: Proof.context -> class list -> string
   val string_of_arity: Proof.context -> arity -> string
+  val guess_infix: syntax -> string -> mixfix option
   val pp: Proof.context -> Pretty.pp
 end;
 
@@ -833,6 +834,13 @@
   fn x => pretty_classrel ctxt x,
   fn x => pretty_arity ctxt x);
 
+(*educated guess for reconstructing infixes*)
+fun guess_infix (Syntax (syn, _)) c = case Parser.guess_infix_lr (#gram syn) c
+ of SOME (s, l, r, j) => SOME (if l then Mixfix.InfixlName (s, j)
+      else if r then Mixfix.InfixrName (s, j)
+      else Mixfix.InfixName (s, j))
+  | NONE => NONE
+
 (*export parts of internal Syntax structures*)
 open Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;