Commit a3139b50 authored by MARCHE Claude's avatar MARCHE Claude

reorganize again parsers, works better like this

parent 2e1247a3
......@@ -342,7 +342,7 @@ endif
.PHONY: initialize_messages update-parsing-error-handling
PARSERS=src/parser/parser.mly src/parser/mlw_parser.mly src/parser/parsing_only.mly
PARSERS=src/parser/parser_common.mly src/parser/parser.mly
src/parser/parser_messages.ml: src/parser/handcrafted.messages
rm -f src/parser/parser_messages.ml src/parser/parser_messages.ml.tmp
......@@ -512,7 +512,7 @@ PLUG_TRANSFORM =
PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer tptp_printer
PLUG_PYTHON = py_ast py_parser py_lexer py_main
PLUG_MICROC = mc_ast mc_parser mc_lexer mc_printer mc_main
PLUG_CFG = cfg_ast cfg_parser cfg_main
PLUG_CFG = cfg_ast cfg_tokens cfg_parser cfg_main
PLUGINS = genequlin dimacs tptp python microc cfg
......@@ -2141,13 +2141,14 @@ clean::
src/parser/parser.ml src/parser/parser.mli: $(PARSERS)
$(SHOW) 'Menhir $<'
$(HIDE)$(MENHIR) --table --explain --strict --base src/parser/parser $<
$(HIDE)$(MENHIR) --table --explain --strict --base src/parser/parser \
$^
plugins/cfg/cfg_parser.ml plugins/cfg/cfg_parser.mli: plugins/cfg/cfg_parser.mly
$(SHOW) 'Menhir $<'
$(HIDE)$(MENHIR) --table --explain --strict --base plugins/cfg/cfg_parser \
--external-tokens Why3.Parser \
src/parser/parser.mly $<
$(HIDE)$(MENHIR) --table --explain --base plugins/cfg/cfg_parser \
--external-tokens Cfg_tokens \
src/parser/parser_common.mly $^
%.dep: %.ml %.mli
......
......@@ -11,13 +11,14 @@
open Why3
open Pmodule
open Mc_ast
open Cfg_ast
open Ptree
open Wstdlib
let debug = Debug.register_flag "micro-C"
~desc:"micro-C plugin debug flag"
let debug = Debug.register_flag "CFG"
~desc:"CFG plugin debug flag"
(*
let mk_id ~loc name =
{ id_str = name; id_ats = []; id_loc = loc }
......@@ -342,11 +343,13 @@ let read_channel env path file c =
Ident.Mid.iter print_m (Mstr.fold add_m mm Ident.Mid.empty)
end;
mm
*)
let () =
Env.register_format mlw_language "micro-C" ["c"] read_channel
~desc:"micro-C format"
Env.register_format mlw_language "CFG" ["cfg"] read_channel
~desc:"CFG format"
(*
(* Add an extension of task printing *)
let () = Itp_server.add_registered_lang "micro-C"
(fun _ -> Mc_printer.microc_ext_printer)
......@@ -359,3 +362,4 @@ let () = Args_wrapper.set_argument_parsing_functions "micro-C"
(* TODO for qualids, add a similar funciton *)
~parse_qualid:(fun lb -> Lexer.parse_qualid lb)
~parse_list_qualid:(fun lb -> Lexer.parse_list_qualid lb)
*)
......@@ -11,17 +11,20 @@
%{
open Why3
open Cfg_ast
let mk_cfgexpr d s e = { cfgexpr_desc = d; cfgexpr_loc = floc s e }
let floc s e = Loc.extract (s,e)
let mk_cfgexpr d s e = { cfg_expr_desc = d; cfg_expr_loc = floc s e }
%}
(* extra token *)
%token CFG
(* extra tokens *)
%token CFG GOTO
%start cfgfile
%type <Cfg_ast.cfg> cfgfile
%type <Cfg_ast.cfg_file> cfgfile
%%
......@@ -35,14 +38,14 @@ cfgmodule:
cfgdecl:
| module_decl_parsing_only { Dmlw_decl $1 }
| LET CFG with_list1(recdefn) { Dletcfg $2 }
| LET CFG dl=with_list1(recdefn) { Dletcfg dl }
;
recdefn:
| id=attrs(lident_rich) args=binders COLON ret=return_named sp=spec EQUAL b=body
{ let pat, ty, _mask = ret in
let spec = apply_return pat sp in
(id, args, ret, ty, pat, spec, b) }
(id, args, ty, pat, spec, [], b) }
;
body:
......
(* The type of tokens. *)
open Why3
type token =
| CFG
| GOTO
| WRITES
| WITH
| WHILE
| VARIANT
| VAL
| USE
| UNDERSCORE
| UIDENT of (string)
| TYPE
| TRY
| TRUE
| TO
| THEORY
| THEN
| STRING of (string)
| SO
| SEMICOLON
| SCOPE
| RIGHTSQ_QUOTE of (string)
| RIGHTSQ
| RIGHTPAR_USCORE of (string)
| RIGHTPAR_QUOTE of (string)
| RIGHTPAR
| RIGHTBRC
| RETURNS
| RETURN
| REQUIRES
| REF
| REC
| REAL of (Number.real_constant)
| READS
| RANGE
| RAISES
| RAISE
| QUOTE_LIDENT of (string)
| PURE
| PRIVATE
| PREDICATE
| POSITION of (Loc.position)
| PARTIAL
| OR
| OPPREF of (string)
| OP4 of (string)
| OP3 of (string)
| OP2 of (string)
| OP1 of (string)
| OLD
| NOT
| MUTABLE
| MODULE
| MINUS
| META
| MATCH
| LTGT
| LT
| LRARROW
| LIDENT of (string)
| LET
| LEMMA
| LEFTSQ
| LEFTPAR
| LEFTBRC
| LARROW
| LABEL
| INVARIANT
| INTEGER of (Number.int_constant)
| INDUCTIVE
| IN
| IMPORT
| IF
| GT
| GOAL
| GHOST
| FUNCTION
| FUN
| FORALL
| FOR
| FLOAT
| FALSE
| EXPORT
| EXISTS
| EXCEPTION
| EQUAL
| EPSILON
| EOF
| ENSURES
| END
| ELSE
| DOWNTO
| DOTDOT
| DOT
| DONE
| DO
| DIVERGES
| CORE_UIDENT of (string)
| CORE_LIDENT of (string)
| CONTINUE
| CONSTANT
| COMMA
| COLON
| COINDUCTIVE
| CLONE
| CHECK
| BY
| BREAK
| BEGIN
| BARBAR
| BAR
| AXIOM
| ATTRIBUTE of (string)
| AT
| ASSUME
| ASSERT
| AS
| ARROW
| ANY
| AND
| AMPAMP
| AMP
| ALIAS
| ABSURD
| ABSTRACT
This diff is collapsed.
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2020 -- 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. *)
(* *)
(********************************************************************)
(**
This is an extension of the main grammar, to be used for parsing only and
producing [Ptree]
*)
%{
(* no new tokens! *)
%}
(* One new entry point *)
%start <Ptree.mlw_file> mlw_file_parsing_only
%%
(* new rules *)
mlw_file_parsing_only:
| EOF { (Modules([])) }
| mlw_module_parsing_only mlw_module_no_decl_parsing_only* EOF { (Modules( [$1] @ $2)) }
| module_decl_parsing_only module_decl_no_head_parsing_only* EOF { (Decls( [$1] @ $2)) }
mlw_module_parsing_only:
| module_head_parsing_only module_decl_no_head_parsing_only* END { ($1,$2) }
module_head_parsing_only:
| THEORY attrs(uident_nq) { $2 }
| MODULE attrs(uident_nq) { $2 }
scope_head_parsing_only:
| SCOPE boption(IMPORT) attrs(uident_nq)
{ let loc = floc $startpos $endpos in (loc, $2, $3) }
module_decl_parsing_only:
| scope_head_parsing_only module_decl_parsing_only* END
{ let loc,import,qid = $1 in (Dscope(loc,import,qid,$2))}
| IMPORT uqualid { (Dimport $2) }
| d = pure_decl | d = prog_decl | d = meta_decl { d }
| use_clone_parsing_only { $1 }
mlw_module_no_decl_parsing_only:
| SCOPE | IMPORT | USE | CLONE | pure_decl | prog_decl | meta_decl
{ let loc = floc $startpos $endpos in
Loc.errorm ~loc "trying to open a module inside another module" }
| mlw_module_parsing_only
{ $1 }
module_decl_no_head_parsing_only:
| THEORY | MODULE
{ let loc = floc $startpos $endpos in
Loc.errorm ~loc "trying to open a module inside another module" }
| module_decl_parsing_only
{ $1 }
(* Use and clone *)
use_clone_parsing_only:
| USE EXPORT tqualid
{ (Duseexport $3) }
| CLONE EXPORT tqualid clone_subst
{ (Dcloneexport ($3, $4)) }
| USE boption(IMPORT) m_as_list = comma_list1(use_as)
{ let loc = floc $startpos $endpos in
let exists_as = List.exists (fun (_, q) -> q <> None) m_as_list in
if $2 && not exists_as then Warning.emit ~loc
"the keyword `import' is redundant here and can be omitted";
(Duseimport (loc, $2, m_as_list)) }
| CLONE boption(IMPORT) tqualid option(preceded(AS, uident)) clone_subst
{ let loc = floc $startpos $endpos in
if $2 && $4 = None then Warning.emit ~loc
"the keyword `import' is redundant here and can be omitted";
(Dcloneimport (loc, $2, $3, $4, $5)) }
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment