switch to Menhir for parsing

.gitignore

@@ -158,13 +158,13 @@ pvsbin/
 /src/driver/driver_lexer.ml
 /src/driver/driver_parser.ml
 /src/driver/driver_parser.mli
-/src/driver/driver_parser.output
+/src/driver/driver_parser.conflicts
 
 # /src/parser/
 /src/parser/lexer.ml
 /src/parser/parser.ml
 /src/parser/parser.mli
-/src/parser/parser.output
+/src/parser/parser.conflicts
 
 # /src/why3doc/
 /src/why3doc/doc_lexer.ml
@@ -186,7 +186,7 @@ pvsbin/
 /plugins/tptp/tptp_lexer.ml
 /plugins/tptp/tptp_parser.ml
 /plugins/tptp/tptp_parser.mli
-/plugins/tptp/tptp_parser.output
+/plugins/tptp/tptp_parser.conflicts
 /plugins/parser/dimacs.ml
 
 # /drivers

Makefile.in

@@ -50,6 +50,12 @@ COQDEP    = @COQDEP@
 CAMLP5O   = @CAMLP5O@
 FRAMAC_LIBDIR = $(DESTDIR)@FRAMAC_LIBDIR@
 
+ifeq (@enable_menhirLib@,yes)
+MENHIR	  = @MENHIR@ --table
+else
+MENHIR	  = @MENHIR@
+endif
+
 DEPFLAGS  = -slash -I lib/why3
 ifeq (@OCAMLBEST@,opt)
 DEPFLAGS += -native
@@ -63,7 +69,7 @@ EMACS = @EMACS@
 #PSVIEWER  = @PSVIEWER@
 #PDFVIEWER = @PDFVIEWER@
 
-INCLUDES = @ZIPINCLUDE@
+INCLUDES = @ZIPINCLUDE@ @MENHIRINCLUDE@
 OFLAGS = -w Aer-41-44-45 -dtypes -g -I lib/why3 $(INCLUDES)
 BFLAGS = -w Aer-41-44-45 -dtypes -g -I lib/why3 $(INCLUDES)
 
@@ -81,14 +87,14 @@ endif
 
 # external libraries common to all binaries
 
-EXTOBJS =
+EXTOBJS = @MENHIRLIB@
 EXTLIBS = str unix nums dynlink @ZIPLIB@
 
 EXTCMA	= $(addsuffix .cma,$(EXTLIBS)) $(addsuffix .cmo,$(EXTOBJS))
 EXTCMXA = $(addsuffix .cmxa,$(EXTLIBS)) $(addsuffix .cmx,$(EXTOBJS))
 
 INSTALLED_LIB_EXTS = a cma cmx cmi cmxa cmxs
-COMPILED_LIB_EXTS = $(INSTALLED_LIB_EXTS) o cmo cmt cmti annot dep output
+COMPILED_LIB_EXTS = $(INSTALLED_LIB_EXTS) o cmo cmt cmti annot dep conflicts
 
 TARGET_EMACS = share/emacs/why3.elc
 
@@ -770,13 +776,19 @@ opt:  src/coq-tactic/.why3-vo-opt
 src/coq-tactic/coqCompat.ml: src/coq-tactic/coqCompat@coq_compat_version@.ml
 	cp -f $< $@
 
+lib/coq-tactic/why3tac.cmxs: OFLAGS += $(addsuffix .cmxa, @ZIPLIB@)
+lib/coq-tactic/why3tac.cmxs: OFLAGS += $(addsuffix .cmx,  @MENHIRLIB@)
+
+lib/coq-tactic/why3tac.cma:  BFLAGS += $(addsuffix .cma,  @ZIPLIB@)
+lib/coq-tactic/why3tac.cma:  BFLAGS += $(addsuffix .cma,  @MENHIRLIB@)
+
 lib/coq-tactic/why3tac.cmxs: lib/why3/why3.cmxa $(COQPCMX)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
-	    $(OCAMLOPT) $(OFLAGS) -o $@ -shared $(addsuffix .cmxa, @ZIPLIB@) $^
+	    $(OCAMLOPT) $(OFLAGS) -o $@ -shared $^
 
 lib/coq-tactic/why3tac.cma: lib/why3/why3.cma $(COQPCMO)
 	$(if $(QUIET),@echo 'Linking  $@' &&) \
-	    $(OCAMLC) -a $(BFLAGS) -o $@ $(addsuffix .cma, @ZIPLIB@) $^
+	    $(OCAMLC) -a $(BFLAGS) -o $@ $^
 
 src/coq-tactic/g_why3tac.ml: src/coq-tactic/g_why3tac.ml4
 	$(if $(QUIET),@echo 'Camlp5   $<' &&) \
@@ -1632,6 +1644,14 @@ clean::
 %.cmi: %.mli
 	$(if $(QUIET),@echo 'Ocamlc   $<' &&) $(OCAMLC) -c $(BFLAGS) $<
 
+# supress "unused rec" warning for Menhir-produced files
+%.cmo: %.ml %.mly
+	$(if $(QUIET),@echo 'Ocamlc   $<' &&) $(OCAMLC) -c $(BFLAGS) -w -39 $<
+
+# supress "unused rec" warning for Menhir-produced files
+%.cmx: %.ml %.mly
+	$(if $(QUIET),@echo 'Ocamlopt $<' &&) $(OCAMLOPT) -c $(OFLAGS) -w -39 $<
+
 %.cmo: %.ml
 	$(if $(QUIET),@echo 'Ocamlc   $<' &&) $(OCAMLC) -c $(BFLAGS) $<
 
@@ -1651,7 +1671,7 @@ clean::
 	$(if $(QUIET),@echo 'Ocamllex $<' &&) $(OCAMLLEX) $<
 
 %.ml %.mli: %.mly
-	$(if $(QUIET),@echo 'Ocamlyacc $<' &&) $(OCAMLYACC) -v $<
+	$(if $(QUIET),@echo 'Menhir $<' &&) $(MENHIR) --explain --strict $<
 
 %.dep: %.ml %.mli
 	$(if $(QUIET),@echo 'Ocamldep $<' &&) $(OCAMLDEP) $(DEPFLAGS) $< $<i > $@

configure.in

@@ -25,20 +25,6 @@
 # See the GNU Library General Public License version 2 for more details
 # (enclosed in the file LGPL).
 
-# the script generated by autoconf from this input will set the following
-# variables:
-#   OCAMLC        "ocamlc" if present in the path, or a failure, or
-#                 "ocamlc.opt" if present with same version number as ocamlc
-#   OCAMLOPT      "ocamlopt" (or "ocamlopt.opt" if present), or "no"
-#   OCAMLBEST     "opt" if a native compiler was found; "byte" otherwise
-#   OCAMLDEP      "ocamldep" or "ocamldep.opt"
-#   OCAMLLEX      "ocamllex" or "ocamllex.opt"
-#   OCAMLYACC     "ocamlyacc"
-#   OCAMLDOC      "ocamldoc" or "ocamldoc.opt"
-#   OCAMLLIB      the path to the ocaml standard library
-#   OCAMLVERSION  the ocaml version number
-#   OCAMLWEB      "ocamlweb" (not mandatory)
-
 AC_INIT([Why3], m4_esyscmd([. ./Version; echo -n "$VERSION"]))
 
 # verbosemake
@@ -78,6 +64,11 @@ AC_ARG_ENABLE(zip,
     AS_HELP_STRING([--enable-zip], [use LZ compression to store session files]),,
     enable_zip=yes)
 
+# menhirLib
+
+AC_ARG_ENABLE(menhirLib,
+    AS_HELP_STRING([--enable-menhirLib], [use MenhirLib parsing library]),,
+    enable_menhirLib=yes)
 
 # IDE
 
@@ -279,6 +270,11 @@ else
     fi
 fi
 
+AC_CHECK_PROG(MENHIR,menhir,menhir,no)
+if test "$MENHIR" = no ; then
+	AC_MSG_ERROR(Cannot find menhir.)
+fi
+
 AC_CHECK_PROG(CAMLP5O,camlp5o,camlp5o,no)
 
 ## Where are the library we need
@@ -372,8 +368,6 @@ else
    BIGINTLIB=nums
 fi
 
-
-
 # checking for camlzip
 if test "$enable_zip" = yes; then
    if test "$USEOCAMLFIND" = yes; then
@@ -399,6 +393,30 @@ else
    ZIPLIB=
 fi
 
+if test "$enable_menhirLib" = yes; then
+  if test "$USEOCAMLFIND" = yes; then
+     MENHIRINCLUDE=$(ocamlfind query menhirLib)
+  fi
+  if test -n "$MENHIRINCLUDE"; then
+     echo "ocamlfind found menhirLib in $MENHIRINCLUDE"
+     MENHIRINCLUDE="-I $MENHIRINCLUDE"
+  else
+     AC_CHECK_FILE($OCAMLLIB/menhirLib/menhirLib.cmx,,enable_menhirLib=no)
+     if test "$enable_menhirLib" = no; then
+        AC_MSG_WARN([Lib menhirLib not found, parser source files will be bigger.])
+        reason_menhirLib=" (menhirLib not found)"
+     else
+        MENHIRINCLUDE="-I +menhirLib"
+     fi
+   fi
+fi
+
+if test "$enable_menhirLib" = yes; then
+   MENHIRLIB=menhirLib
+else
+   MENHIRLIB=
+fi
+
 # checking for lablgtk2
 if test "$enable_ide" = yes ; then
    if test "$USEOCAMLFIND" = yes; then
@@ -697,6 +715,7 @@ dnl AC_SUBST(OCAMLV)
 dnl AC_SUBST(FORPACK)
 AC_SUBST(OCAMLGRAPHLIB)
 dnl AC_SUBST(OCAMLWEB)
+AC_SUBST(MENHIR)
 
 AC_SUBST(enable_profiling)
 AC_SUBST(enable_bin_annot)
@@ -717,6 +736,10 @@ AC_SUBST(enable_zip)
 AC_SUBST(ZIPINCLUDE)
 AC_SUBST(ZIPLIB)
 
+AC_SUBST(enable_menhirLib)
+AC_SUBST(MENHIRINCLUDE)
+AC_SUBST(MENHIRLIB)
+
 AC_SUBST(enable_coq_tactic)
 AC_SUBST(enable_coq_libs)
 AC_SUBST(enable_coq_fp_libs)
@@ -792,6 +815,7 @@ echo "Components"
 echo "    IDE command             : $enable_ide$reason_ide"
 echo "    GMP arithmetic          : $enable_zarith$reason_zarith"
 echo "    Compressed sessions     : $enable_zip$reason_zip"
+echo "    MenhirLib support       : $enable_menhirLib$reason_menhirLib"
 echo "    Hypothesis selection    : $enable_hypothesis_selection$reason_hypothesis_selection"
 echo "    Frama-C support         : $enable_frama_c$reason_frama_c"
 if test "$enable_frama_c" = yes ; then

misc/headache_config.txt

@@ -5,7 +5,7 @@
 # Objective Caml source
 | ".*\\.ml[il4]?" -> frame width:62 open:"(*" line:"*" close:"*)"
 | ".*\\.ml[il4]?\\.in" -> frame width:62 open:"(*" line:"*" close:"*)"
-| ".*\\.mly"      -> frame width:62 open:"/*" line:"*" close:"*/"
+| ".*\\.mly"      -> frame width:62 open:"(*" line:"*" close:"*)"
 # C source
 | ".*\\.c"      -> frame width:62 open:"/*" line:"*" close:"*/"
 # Misc

plugins/tptp/tptp_lexer.mll

@@ -20,19 +20,15 @@
   (* lexical errors *)
 
   exception IllegalCharacter of char
+  exception IllegalLexeme of string
   exception UnterminatedComment
-(* dead code
-  exception UnterminatedString
-*)
   exception UnknownDDW of string
   exception UnknownDW of string
 
   let () = Exn_printer.register (fun fmt e -> match e with
     | IllegalCharacter c -> fprintf fmt "illegal character %c" c
+    | IllegalLexeme s -> fprintf fmt "illegal lexeme %s" s
     | UnterminatedComment -> fprintf fmt "unterminated comment"
-(* dead code
-    | UnterminatedString -> fprintf fmt "unterminated string"
-*)
     | UnknownDDW s -> fprintf fmt "unknown system_word %s" s
     | UnknownDW s -> fprintf fmt "unknown defined_word %s" s
     | _ -> raise e)
@@ -86,16 +82,16 @@
   let () = List.iter (fun (x,y) -> Hashtbl.add keywords x y) [
     "assumption", ASSUMPTION;
     "axiom", AXIOM;
-    "cnf", CNF;
+    "cnf", CNFK;
     "conjecture", CONJECTURE;
     "corollary", COROLLARY;
     "definition", DEFINITION;
-    "fof", FOF;
+    "fof", FOFK;
     "hypothesis", HYPOTHESIS;
     "include", INCLUDE;
     "lemma", LEMMA;
     "negated_conjecture", NEGATED_CONJECTURE;
-    "tff", TFF;
+    "tff", TFFK;
     "theorem", THEOREM;
     "type", TYPE;
   ]
@@ -164,7 +160,7 @@ rule token = parse
   | '-'  (natural as i) ('.' (digit+ as f))? (['e' 'E'] ('-'   natural as e))?
       { REALNEGNUM (i,f,e) }
   | "/*/"
-      { SLASH_STAR_SLASH }
+      { raise (IllegalLexeme "/*/") }
   | "/*"
       { comment_start_loc := loc lexbuf; comment_block lexbuf; token lexbuf }
   | "%"

src/driver/driver_parser.mly

-/********************************************************************/
-/*                                                                  */
-/*  The Why3 Verification Platform   /   The Why3 Development Team  */
-/*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  */
-/*                                                                  */
-/*  This software is distributed under the terms of the GNU Lesser  */
-/*  General Public License version 2.1, with the special exception  */
-/*  on linking described in file LICENSE.                           */
-/*                                                                  */
-/********************************************************************/
+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2014   --   INRIA - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
 
 %{
   open Driver_ast
 
-  let loc () = Loc.extract (symbol_start_pos (), symbol_end_pos ())
-  let loc_i i = Loc.extract (rhs_start_pos i, rhs_end_pos i)
   let infix s  = "infix " ^ s
   let prefix s = "prefix " ^ s
   let mixfix s = "mixfix " ^ s
 %}
 
-%token <string> INPUT /* never reaches the parser */
-
 %token <int> INTEGER
 %token <string> IDENT
 %token <string> STRING
 %token <string> OPERATOR
+%token <string> INPUT (* never reaches the parser *)
 %token THEORY END SYNTAX REMOVE META PRELUDE PRINTER
 %token VALID INVALID TIMEOUT OUTOFMEMORY UNKNOWN FAIL TIME
 %token UNDERSCORE LEFTPAR RIGHTPAR DOT QUOTE EOF
@@ -37,25 +34,19 @@
 %nonassoc SYNTAX REMOVE PRELUDE
 %nonassoc prec_pty
 
-%type <Driver_ast.file> file
-%start file
-%type <Driver_ast.file_extract> file_extract
-%start file_extract
-
+%start <Driver_ast.file> file
+%start <Driver_ast.file_extract> file_extract
 %%
 
-file:
-| list0_global_theory EOF
-    { $1 }
-;
+file: list0_global_theory EOF { $1 }
 
 list0_global_theory:
-| /* epsilon */      { { f_global = []; f_rules = [] } }
-| global list0_global_theory
-    { {$2 with f_global = (loc_i 1, $1) :: ($2.f_global)} }
+| (* epsilon *)
+    { { f_global = []; f_rules = [] } }
+| loc(global) list0_global_theory
+    { {$2 with f_global = $1 :: ($2.f_global)} }
 | theory list0_global_theory
     { {$2 with f_rules = $1 :: ($2.f_rules)} }
-;
 
 global:
 | PRELUDE STRING { Prelude $2 }
@@ -75,18 +66,12 @@ global:
 | FILENAME STRING { Filename $2 }
 | TRANSFORM STRING { Transform $2 }
 | PLUGIN STRING STRING { Plugin ($2,$3) }
-| BLACKLIST list1_string_list { Blacklist $2 }
-;
+| BLACKLIST STRING+ { Blacklist $2 }
+| INPUT { assert false }
 
 theory:
-| THEORY tqualid list0_trule END
+| THEORY loc(tqualid) loc(trule)+ END
     { { thr_name = $2; thr_rules = $3 } }
-;
-
-list0_trule:
-| /* epsilon */     { [] }
-| trule list0_trule { (loc_i 1, $1) :: $2 }
-;
 
 trule:
 | PRELUDE STRING                   { Rprelude  ($2) }
@@ -97,38 +82,34 @@ trule:
 | REMOVE PROP qualid               { Rremovepr ($3) }
 | META ident meta_args             { Rmeta     ($2, $3) }
 | META STRING meta_args            { Rmeta     ($2, $3) }
-;
 
-meta_args:
-| meta_arg                 { [$1] }
-| meta_arg COMMA meta_args { $1 :: $3 }
-;
+meta_args: separated_nonempty_list(COMMA,meta_arg) { $1 }
 
 meta_arg:
-| TYPE primitive_type_top { PMAty $2 }
+| TYPE   meta_type { PMAty  $2 }
 | FUNCTION  qualid { PMAfs  $2 }
 | PREDICATE qualid { PMAps  $2 }
 | PROP      qualid { PMApr  $2 }
 | STRING           { PMAstr $1 }
 | INTEGER          { PMAint $1 }
-;
 
 tqualid:
-| ident              { loc (), [$1] }
-| ident DOT tqualid  { loc (), ($1 :: snd $3) }
-| STRING DOT tqualid { loc (), ($1 :: snd $3) }
-;
+| ident              { [$1] }
+| ident DOT tqualid  { $1 :: $3 }
+| STRING DOT tqualid { $1 :: $3 }
+
+qualid:  loc(qualid_)  { $1 }
 
-qualid:
-| ident_rich        { loc (), [$1] }
-| ident DOT qualid  { loc (), ($1 :: snd $3) }
-;
+qualid_:
+| ident_rich         { [$1] }
+| ident DOT qualid_  { ($1 :: $3) }
 
 ident:
 | IDENT     { $1 }
 | SYNTAX    { "syntax" }
 | REMOVE    { "remove" }
 | PRELUDE   { "prelude" }
+| BLACKLIST { "blacklist" }
 | PRINTER   { "printer" }
 | VALID     { "valid" }
 | INVALID   { "invalid" }
@@ -138,13 +119,11 @@ ident:
 | FILENAME  { "filename" }
 | TRANSFORM { "transformation" }
 | PLUGIN    { "plugin" }
-;
 
 ident_rich:
 | ident                     { $1 }
 | LEFTPAR_STAR_RIGHTPAR     { infix "*" }
 | LEFTPAR operator RIGHTPAR { $2 }
-;
 
 operator:
 | OPERATOR              { infix $1 }
@@ -152,94 +131,63 @@ operator:
 | LEFTSQ RIGHTSQ        { mixfix "[]" }
 | LEFTSQ LARROW RIGHTSQ { mixfix "[<-]" }
 | LEFTSQ RIGHTSQ LARROW { mixfix "[]<-" }
-;
 
-list1_string_list:
-| STRING                   { [$1] }
-| list1_string_list STRING { $2 :: $1 }
-;
+(* Types *)
 
-/* Types */
-
-primitive_type_top:
-| qualid primitive_type_args_top  { PTyapp ($1, $2) }
+meta_type:
+| qualid meta_type_args       { PTyapp ($1, $2) }
 | primitive_type_arg_common   { $1 }
-;
 
-primitive_type_args_top:
-| /* epsilon */ %prec prec_pty                { [] }
-| primitive_type_arg primitive_type_args_top  { $1 :: $2 }
-;
+meta_type_args:
+| (* epsilon *) %prec prec_pty        { [] }
+| primitive_type_arg meta_type_args   { $1 :: $2 }
 
 primitive_type:
-| qualid primitive_type_args  { PTyapp ($1, $2) }
+| qualid primitive_type_arg+  { PTyapp ($1, $2) }
 | primitive_type_arg          { $1 }
-;
-
-primitive_type_args:
-| primitive_type_arg                      { [$1] }
-| primitive_type_arg primitive_type_args  { $1 :: $2 }
-;
 
 primitive_type_arg:
 | qualid                    { PTyapp ($1, []) }
 | primitive_type_arg_common { $1 }
-;
 
 primitive_type_arg_common:
-| type_var                          { PTyvar $1 }
+| QUOTE ident                       { PTyvar $2 }
 | LEFTPAR primitive_types RIGHTPAR  { PTuple $2 }
 | LEFTPAR RIGHTPAR                  { PTuple [] }
 | LEFTPAR primitive_type RIGHTPAR   { $2 }
-;
 
 primitive_types:
 | primitive_type COMMA primitive_type  { [$1; $3] }
 | primitive_type COMMA primitive_types { $1 :: $3 }
-;
 
-type_var:
-| QUOTE ident { $2 }
-;
-
-/* WhyML */
+(* WhyML *)
 
 file_extract:
-| list0_global_theory_module EOF
-{ $1 }
-;
+| list0_global_theory_module EOF { $1 }
 
 list0_global_theory_module:
-| /* epsilon */
+| (* epsilon *)
     { { fe_global = []; fe_th_rules = []; fe_mo_rules = [] } }
-| global_extract list0_global_theory_module
-    { {$2 with fe_global = (loc_i 1, $1) :: ($2.fe_global)} }
+| loc(global_extract) list0_global_theory_module
+    { {$2 with fe_global = $1 :: ($2.fe_global)} }
 | theory list0_global_theory_module
     { {$2 with fe_th_rules = $1 :: ($2.fe_th_rules)} }
 | module_ list0_global_theory_module
     { {$2 with fe_mo_rules = $1 :: ($2.fe_mo_rules)} }
-;
 
 global_extract:
 | PRELUDE STRING    { EPrelude $2 }
 | PRINTER STRING    { EPrinter $2 }
-| BLACKLIST list1_string_list { EBlacklist $2 }
-;
+| BLACKLIST STRING+ { EBlacklist $2 }
 
 module_:
-| MODULE tqualid list0_mrule END
+| MODULE loc(tqualid) nonempty_list(loc(mrule)) END
     { { mor_name = $2; mor_rules = $3 } }
-;
-
-list0_mrule:
-| /* epsilon */     { [] }
-| mrule list0_mrule { (loc_i 1, $1) :: $2 }
-;
 
 mrule:
 | trule                          { MRtheory $1 }
 | SYNTAX EXCEPTION qualid STRING { MRexception ($3, $4) }
 | SYNTAX VAL qualid STRING       { MRval ($3, $4) }
 | SYNTAX CONVERTER qualid STRING { MRconverter ($3, $4) }
-;
 
+loc(X): X { Loc.extract ($startpos,$endpos), $1 }