code: import java.io.*;
  import java.util.regex.Pattern;
  import java.util.regex.Matcher;
  import java.util.ArrayList;
  import java.util.TreeMap;
  import java.util.TreeSet;
  
  public class DetectEq {
  
      static class Annotation {
          String type;
          String op;
          String code;
          int from, to, line, true_line;
          void print () {
              System.out.println("from: "+from+", to: "+to+
                      ", type: "+type+", op: "+op);
              System.out.println("line: "+true_line+", code: "+code);
              System.out.println("");
          }
          public boolean equals(Annotation a) {
              return a.from == from && a.to == to;
          }
      }
  
      static void skip (StringBuffer s) {
          for (int i=0; i<s.length(); i++)
            if (Character.isDigit(s.charAt(i))) {
                s.delete(0, i);
                break;
            }
      }
  
      static int readnum (StringBuffer s) {
          for (int i=0; ; i++)
            if (i == s.length() || !Character.isDigit(s.charAt(i))) {
                int num = Integer.parseInt(s.substring(0, i));
                s.delete(0, i);
                return num;
            }
      }
  
      static Pattern thm_patterns[] =
              new Pattern[] {
                  Pattern.compile("(.*thm.*) (\\*|->) (.*thm.*) -> bool"),
                  Pattern.compile("(.*injust.*) (\\*|->) (.*injust.*) -> bool"),
                  Pattern.compile("(.*lineq.*) (\\*|->) (.*lineq.*) -> bool"),
                  Pattern.compile("(.*goal.*) (\\*|->) (.*goal.*) -> bool")
              };
  
      static Pattern typattern = Pattern.compile(".*(thm|injust|lineq|goal).*");
  
      static String thm_funcs[] = {
          "union", "intersect", "subtract", "subset", "set_eq", "unions", "assoc", "rev_assoc", "assoc2",
          "uniq", "setify", "set_insert", "set_merge", "munion", "msubtract", "assocd", "rev_assocd",
          "apply", "|->", "dom", "graph"
      };
  
      static void readtype(String s, Annotation a) {
          String t1, t2;
          s = s.trim();
          for (int i=0; i<thm_patterns.length; i++) {
              Matcher matcher = thm_patterns[i].matcher(s);
              while (matcher.find()) {
                  t1 = matcher.group(1).trim();
                  t2 = matcher.group(3).trim();
                  if (t1.equals(t2)) {
                      a.type = t1;
                      a.op = matcher.group(2);
                      break;
                  }
              }
          }
      }
  
      static Annotation parseAnnotation(LineNumberReader r, MLFile mlfile) throws Exception {
          Annotation annot = new Annotation();
          String line1 = r.readLine();
          if (line1 == null) return null;
          if (r.readLine() == null) return null;
          String line2 = "";
          do {
              String l = r.readLine();
              if (l == null) return null;
              l = l.trim();
              if (")".equals(l)) break;
              line2 = line2+" "+l;
          } while (true);
          line2 = line2.trim();
          readtype(line2, annot);
          StringBuffer buf = new StringBuffer(line1);
          skip(buf); annot.line = readnum(buf);
          skip(buf); readnum(buf);
          skip(buf); annot.from = readnum(buf);
          skip(buf); readnum(buf);
          skip(buf); readnum(buf);
          skip(buf); annot.to = readnum(buf);
          annot.code = mlfile.get(annot.from, annot.to);
          annot.true_line = mlfile.line(annot.from);
          Matcher matcher = typattern.matcher(line2);
          if (annot.type == null && matcher.find()) {
              String s = mlfile.get(annot.from,  annot.to);
              for (int i=0; i<thm_funcs.length; i++) {
                  if (s.equals(thm_funcs[i])) {
                      annot.type = line2;
                      annot.op = thm_funcs[i];
                  }
              }
          }
          return annot;
      }
  
      static Annotation[] readAnnotations(LineNumberReader r, MLFile mlfile) throws Exception {
          ArrayList array = new ArrayList(100);
          Annotation a;
          do {
              a = parseAnnotation(r, mlfile);
              if (a != null) {
  //                if (!(array.size() > 0 && ((Annotation)array.get(array.size()-1)).equals(a))) {
                      array.add(a);
                      if (a.type != null) a.print();
    //              }
              }
          } while (a != null);
          Annotation as[] = new Annotation[array.size()];
          for (int i=0; i<as.length; i++) as[i] = (Annotation) array.get(i);
          return as;
      }
  
      static class Interval implements Comparable {
          int line;
          int from, to;
          Interval(int l, int f, int t) { line = l; from = f; to = t;}
          public int compareTo(Object o) {
              Interval y = (Interval) o;
              if ((y.from <= from && y.to >= to) ||
                  (from <= y.from && to >= y.from))
                  return 0;
              if (from < y.from) return -1;
              else if (from > y.from) return 1;
              else if (to < y.to) return -1;
              else return 1;
          }
      }
  
      static class MLFile {
          File f;
          byte[] data;
          TreeMap lines;
  
         MLFile (File f) throws Exception {
              this.f = f;
              data = new byte[(int)f.length()];
              FileInputStream in = new FileInputStream(f);
              in.read(data);
              in.close();
              prepareLineLookup();
          }
          void prepareLineLookup() {
              lines = new TreeMap();
              int line = 1;
              int from = 0;
              for (int i=0; i<data.length; i++) {
                  if ((char) data[i] == '\n') {
                      Interval v = new Interval (line, from, i);
                      lines.put(v, v);
                      line++;
                      from = i+1;
                  }
              }
              Interval v = new Interval(line, from, data.length);
              lines.put(v,v);
          }
          String get(int from, int to) {
              StringBuffer buf = new StringBuffer(to-from);
              for (int i=from; i<to; i++) {
                  int c = data[i];
                  if (c < 0) c += 256;
                  buf.append((char) c);
              }
              return buf.toString();
          }
          int line(int pos) {
              return ((Interval)lines.get(new Interval(0,pos, pos))).line;
          }
      }
  
      public static void main (String args[]) throws Exception {
          File annot = new File(args[0], "core.annot");
          File ml = new File(args[0], "core.ml");
          MLFile mlfile = new MLFile(ml);
          LineNumberReader in_annot = new LineNumberReader(new FileReader(annot));
          Annotation as[] = readAnnotations(in_annot,mlfile);
          in_annot.close();
          System.out.println("count: "+as.length);
          BufferedReader reader = new BufferedReader(new InputStreamReader(System.in));
          mainloop: do {
              String s = reader.readLine();
              int line = Integer.parseInt(s);
              for (int i=0; i<as.length; i++) {
                  if (as[i].line == line) {
                      System.out.println(line+" -> "+as[i].true_line);
                      //as[i].print();
                      continue mainloop;
                  }
              }
              System.out.println("line not found");
          } while (true);
      }
  
  
  }
  