Add Sleek parser into the system to support Sleek specification

.gitignore

@@ -319,3 +319,12 @@ trywhy3.tar.gz
 # Opam
 
 _opam/
+
+# /src/sleek/
+/src/sleek/lexer_sleek.ml
+/src/sleek/parser_sleek.ml
+/src/sleek/parser_sleek.mli
+/src/sleek/parser_sleek.conflicts
+/src/sleek/lexlib_sleek.ml
+/src/sleek/parser_sleek_tokens.ml
+/src/sleek/parser_sleek_tokens.mli

Makefile.in

@@ -222,6 +222,7 @@ GENERATED =
 # Why3 library
 ##############
 
+# sleek support
 LIBGENERATED = \
 	src/util/config.ml \
 	src/util/rc.ml src/util/lexlib.ml src/util/mysexplib.ml \
@@ -235,7 +236,11 @@ LIBGENERATED = \
 	src/driver/driver_lexer.ml \
 	src/driver/sexp.ml \
 	src/session/compress.ml src/session/xml.ml \
-	src/session/strategy_parser.ml
+	src/session/strategy_parser.ml \
+	src/sleek/lexer_sleek.ml \
+	src/sleek/lexlib_sleek.ml \
+	src/sleek/parser_sleek_tokens.mli src/sleek/parser_sleek_tokens.ml \
+	src/sleek/parser_sleek.mli src/sleek/parser_sleek.ml
 
 LIB_UTIL = exn_printer mysexplib config bigInt mlmpfr_wrapper util opt lists strings \
 	   pp extmap extset exthtbl weakhtbl diffmap hcpt \
@@ -303,8 +308,14 @@ LIB_SESSION = compress xml termcode session_itp \
 	      server_utils itp_communication \
 	      itp_server json_util unix_scheduler
 
+# sleek support
+LIB_SLEEK = \
+	ptree_sleek lexlib_sleek parser_sleek_tokens parser_sleek \
+	keywords_sleek lexer_sleek
+
 LIB_CMIONLY = driver/driver_ast
 
+# sleek support
 LIBMODULES =  $(addprefix src/util/, $(LIB_UTIL)) \
 	      $(addprefix src/core/, $(LIB_CORE)) \
 	      $(addprefix src/driver/, $(LIB_DRIVER)) \
@@ -315,9 +326,11 @@ LIBMODULES =  $(addprefix src/util/, $(LIB_UTIL)) \
 	      $(addprefix src/parser/, $(LIB_PARSER)) \
 	      $(addprefix src/transform/, $(LIB_TRANSFORM)) \
 	      $(addprefix src/printer/, $(LIB_PRINTER)) \
-	      $(addprefix src/session/, $(LIB_SESSION))
+	      $(addprefix src/session/, $(LIB_SESSION)) \
+		  $(addprefix src/sleek/, $(LIB_SLEEK))
 
-LIBDIRS = util core driver mlw extract parser transform printer session
+# sleek support
+LIBDIRS = util core driver mlw extract parser transform printer session sleek
 
 ifeq (@enable_infer@,yes)
 	LIBDIRS += infer
@@ -339,6 +352,8 @@ $(LIBCMX): OFLAGS += -for-pack Why3
 
 $(LIBDEP): $(LIBGENERATED)
 
+# TODO: sleek support for ptree_sleek?
+
 src/parser/ptree.cmx src/parser/ptree.cmo: FLAGS += -w -70
 src/util/mysexplib.cmx src/util/mysexplib.cmo: FLAGS += -w -70
 
@@ -1573,6 +1588,41 @@ install-bin::
 
 install_local:: bin/why3pp.$(SHAREDBEST)
 
+# sleek support
+#################
+# why3pp_sleek #
+#################
+
+PP_SLEEK_FILES = why3pp_sleek
+PP_SLEEK_MODULES = $(addprefix src/tools/, $(PP_SLEEK_FILES))
+
+PP_SLEEK_DEP = $(addsuffix .dep, $(PP_SLEEK_MODULES))
+PP_SLEEK_CMO = $(addsuffix .cmo, $(PP_SLEEK_MODULES))
+PP_SLEEK_CMX = $(addsuffix .cmx, $(PP_SLEEK_MODULES))
+
+$(PP_SLEEK_DEP) $(PP_SLEEK_CMO) $(PP_SLEEK_CMX): INCLUDES += -I src/tools
+
+# build targets
+
+byte: bin/why3pp_sleek.cma
+opt:  bin/why3pp_sleek.cmxs
+
+bin/why3pp_sleek.cmxs: $(PP_SLEEK_CMX)
+bin/why3pp_sleek.cma:  $(PP_SLEEK_CMO)
+
+# depend and clean targets
+
+MAKEINC += $(PP_SLEEK_DEP)
+
+uninstall-bin::
+	rm -f $(TOOLDIR)/why3pp_sleek.$(SHAREDBEST)
+
+install-bin::
+	$(MKDIR_P) $(TOOLDIR)
+	$(INSTALL_DATA) bin/why3pp_sleek.$(SHAREDBEST) $(TOOLDIR)
+
+install_local:: bin/why3pp_sleek.$(SHAREDBEST)
+
 #########
 # why3doc
 #########
@@ -2107,6 +2157,16 @@ pl%gins/cfg/cfg_parser.ml pl%gins/cfg/cfg_parser.mli: src/parser/parser_common.m
 	$(HIDE)$(MENHIR) --table --explain --strict --base plugins/cfg/cfg_parser $^
 	$(HIDE)for f in plugins/cfg/cfg_parser.mli plugins/cfg/cfg_parser.ml; do (echo "open Why3"; cat $$f) > $$f.new && mv $$f.new $$f; done
 
+# sleek support
+src/s%eek/parser_sleek_tokens.ml src/s%eek/parser_sleek_tokens.mli: src/sleek/parser_sleek_common.mly
+	$(SHOW) 'Menhir $^'
+	$(HIDE)$(MENHIR) --base src/sleek/parser_sleek_tokens --only-tokens $^
+
+src/s%eek/parser_sleek.ml src/s%eek/parser_sleek.mli: src/sleek/parser_sleek_common.mly src/sleek/parser_sleek.mly
+	$(SHOW) 'Menhir $^'
+	$(HIDE)$(MENHIR) --table --explain --strict --base src/sleek/parser_sleek \
+		--external-tokens Parser_sleek_tokens $^
+
 %.ml %.mli: %.mly
 	$(SHOW) 'Menhir $<'
 	$(HIDE)$(MENHIR) --table --explain --strict $<

genmake.sh

@@ -0,0 +1,5 @@
+#!/bin/sh -eux
+
+autoconf
+./configure --enable-local --disable-ide --disable-web-ide --disable-coq-libs --disable-pvs-libs --disable-isabelle-libs --disable-doc --disable-emacs-compilation
+

src/sleek/keywords_sleek.ml

@@ -0,0 +1,110 @@
+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2023 --  Inria - CNRS - Paris-Saclay 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 Parser_sleek_tokens
+
+(* keep the following files synchronized:
+
+  doc/ext/why3.py
+  plugins/cfg/cfg_lexer.mll
+  share/emacs/why3.el
+  share/vim/syntax/why3.vim
+  src/trywhy3/mode-why3.js
+*)
+
+let plain = [
+    "abstract", ABSTRACT;
+    "absurd", ABSURD;
+    "alias", ALIAS;
+    "any", ANY;
+    "as", AS;
+    "assert", ASSERT;
+    "assume", ASSUME;
+    "at", AT;
+    "axiom", AXIOM;
+    "begin", BEGIN;
+    "break", BREAK;
+    "by", BY;
+    "check", CHECK;
+    "clone", CLONE;
+    "coinductive", COINDUCTIVE;
+    "constant", CONSTANT;
+    "continue", CONTINUE;
+    "diverges", DIVERGES;
+    "do", DO;
+    "done", DONE;
+    "downto", DOWNTO;
+    "else", ELSE;
+    "end", END;
+    "ensures", ENSURES;
+    "epsilon", EPSILON;
+    "exception", EXCEPTION;
+    "exists", EXISTS;
+    "export", EXPORT;
+    "false", FALSE;
+    "for", FOR;
+    "forall", FORALL;
+    "fun", FUN;
+    "function", FUNCTION;
+    "ghost", GHOST;
+    "goal", GOAL;
+    "if", IF;
+    "import", IMPORT;
+    "in", IN;
+    "inductive", INDUCTIVE;
+    "invariant", INVARIANT;
+    "label", LABEL;
+    "lemma", LEMMA;
+    "let", LET;
+    "match", MATCH;
+    "meta", META;
+    "module", MODULE;
+    "mutable", MUTABLE;
+    "not", NOT;
+    "old", OLD;
+    "partial", PARTIAL;
+    "predicate", PREDICATE;
+    "private", PRIVATE;
+    "pure", PURE;
+    "raise", RAISE;
+    "raises", RAISES;
+    "reads", READS;
+    "rec", REC;
+    "requires", REQUIRES;
+    "return", RETURN;
+    "returns", RETURNS;
+    "scope", SCOPE;
+    "so", SO;
+    "then", THEN;
+    "theory", THEORY;
+    "to", TO;
+    "true", TRUE;
+    "try", TRY;
+    "type", TYPE;
+    "use", USE;
+    "val", VAL;
+    "variant", VARIANT;
+    "while", WHILE;
+    "with", WITH;
+    "writes", WRITES;
+  ]
+
+let contextual = [
+    "float", FLOAT;
+    "range", RANGE;
+    "ref", REF;
+  ]
+
+let keyword_tokens =
+  plain @ contextual
+
+let keywords =
+  List.map fst plain

src/sleek/keywords_sleek.mli

@@ -0,0 +1,15 @@
+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2023 --  Inria - CNRS - Paris-Saclay 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.                           *)
+(*                                                                  *)
+(********************************************************************)
+
+val keyword_tokens: (string * Parser_sleek.token) list
+
+(* does not include contextual tokens *)
+val keywords: string list

src/sleek/lexer_sleek.mli

@@ -0,0 +1,34 @@
+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2023 --  Inria - CNRS - Paris-Saclay 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.                           *)
+(*                                                                  *)
+(********************************************************************)
+
+val parse_term : Lexing.lexbuf -> Ptree_sleek.term
+
+val parse_expr : Lexing.lexbuf -> Ptree_sleek.expr
+
+val parse_decl : Lexing.lexbuf -> Ptree_sleek.decl
+
+val parse_term_list: Lexing.lexbuf -> Ptree_sleek.term list
+
+val parse_qualid: Lexing.lexbuf -> Ptree_sleek.qualid
+
+val parse_list_qualid: Lexing.lexbuf -> Ptree_sleek.qualid list
+
+val parse_list_ident: Lexing.lexbuf -> Ptree_sleek.ident list
+
+(* TODO: mlws file instead of mlw file *)
+val parse_mlw_file: Lexing.lexbuf -> Ptree_sleek.mlw_file
+
+(* TODO: no longer return Pmodule.mlw_file *)
+(* val read_channel: Env.env -> Env.pathname -> string -> in_channel ->
+  Pmodule.mlw_file *)
+
+(* Name of the registered format for whyml *)
+val whyml_sleek_format: Env.fformat