Initial version of the Helena Checker

[helm.git] / helm / software / lambda-delta / automath / autLexer.mll

diff --git a/helm/software/lambda-delta/automath/autLexer.mll b/helm/software/lambda-delta/automath/autLexer.mll
new file mode 100644 (file)
index 0000000..f0ae1ae
--- /dev/null
+++ b/helm/software/lambda-delta/automath/autLexer.mll
@@ -0,0 +1,89 @@
+(* Copyright (C) 2000, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+{ 
+   module P = AutParser
+   
+   let debug = false
+   let out s = if debug then print_endline s else ()
+}
+
+let LC  = ['#' '%']
+let OC  = "{"
+let CC  = "}"
+let SPC = [' ' '\t' '\n']+
+let NL  = "\n"
+let ID  = ['0'-'9' 'A'-'Z' 'a'-'z' '_' '\'' '`']+
+
+rule line_comment = parse
+   | NL  { () }
+   | OC  { block_comment lexbuf; line_comment lexbuf }
+   | _   { line_comment lexbuf }
+   | eof  { () } 
+and block_comment = parse
+   | CC  { () }
+   | OC  { block_comment lexbuf; block_comment lexbuf }
+   | LC  { line_comment lexbuf; block_comment lexbuf  }
+   | _   { block_comment lexbuf }
+   | eof { () } 
+and token = parse
+   | SPC      { token lexbuf } 
+   | LC       { line_comment lexbuf; token lexbuf  }
+   | OC       { block_comment lexbuf; token lexbuf }
+   | "_E"     { out "E"; P.E         }
+   | "'_E'"   { out "E"; P.E         }
+   | "---"    { out "EB"; P.EB       }
+   | "'eb'"   { out "EB"; P.EB       }
+   | "EB"     { out "EB"; P.EB       }
+   | "--"     { out "EXIT"; P.EXIT   }
+   | "PN"     { out "PN"; P.PN       }
+   | "'pn'"   { out "PN"; P.PN       }
+   | "PRIM"   { out "PN"; P.PN       }
+   | "'prim'" { out "PN"; P.PN       }
+   | "???"    { out "PN"; P.PN       }
+   | "PROP"   { out "PROP"; P.PROP   }
+   | "'prop'" { out "PROP"; P.PROP   }
+   | "TYPE"   { out "TYPE"; P.TYPE   }
+   | "'type'" { out "TYPE"; P.TYPE   }
+   | ID       { out "ID"; P.IDENT (Lexing.lexeme lexbuf) }   
+   | ":="     { out "DEF"; P.DEF     }
+   | "("      { out "OP"; P.OP       }
+   | ")"      { out "CP"; P.CP       }
+   | "["      { out "OB"; P.OB       }
+   | "]"      { out "CB"; P.CB       }
+   | "<"      { out "OA"; P.OA       }
+   | ">"      { out "CA"; P.CA       }
+   | "@"      { out "AT"; P.AT       }
+   | "~"      { out "TD"; P.TD       }
+   | "\""     { out "QT"; P.QT       }
+   | ":"      { out "CN"; P.CN       }   
+   | ","      { out "CM"; P.CM       }
+   | ";"      { out "SC"; P.SC       }
+   | "."      { out "FS"; P.FS       }   
+   | "+"      { out "PLUS"; P.PLUS   }
+   | "-"      { out "MINUS"; P.MINUS }
+   | "*"      { out "TIMES"; P.TIMES }
+   | "="      { out "DEF"; P.DEF     }
+   | eof      { out "EOF"; P.EOF     }