Commit e53e78b4 authored by Rehan MALAK's avatar Rehan MALAK

This is an experimental branch to play with Ptree's

0) opam install ppx_optcomp

1) build why3 with --enable-local :

git clean -dffx && ./autogen.sh && ./configure --enable-local && make -j8

2) play with ptree's api

cd examples/use_api
make

3) why3_ptree is a program parsing a *.mlw file that returns the complete ptree (list of modules) and then print the ptree in debug mode and with a pretty printer :

  ./why3_ptree ../examples/logic/real.why

In particular, it has a ptree ast debug printer

  Why3ml_pp.Output_ast.print_mlw_file

and a ptree pretty printer

  Why3ml_pp.Output_mlw.print_mlw_file
parent 05b27250
.merlin
why3_ptree
why3_prove
mlw_tree
S ../../src/util
S ../../src/core
S ../../src/driver
S ../../src/mlw
S ../../src/parser
S ../../src/transform
S ../../src/printer
S ../../src/whyml
S ../../src/session
S ../../src/tools
S ../../src/ide
S ../../src/why3session
S ../../src/why3doc
S ../../src/jessie
S ../../src/trywhy3
S ../../plugins/parser
S ../../plugins/printer
S ../../plugins/transform
S ../../plugins/tptp
S ../../plugins/python
B ../../src/util
B ../../src/core
B ../../src/driver
B ../../src/mlw
B ../../src/parser
B ../../src/transform
B ../../src/printer
B ../../src/whyml
B ../../src/session
B ../../src/tools
B ../../src/ide
B ../../src/why3session
B ../../src/why3doc
B ../../src/jessie
B ../../src/trywhy3
B ../../plugins/parser
B ../../plugins/printer
B ../../plugins/transform
B ../../plugins/tptp
B ../../plugins/python
B ../../lib/why3
PKG zip
PKG menhirlib
FLG -package ppx_optcomp
OCAMLC=ocamlc.opt
OCAMLOPT=ocamlopt.opt
COMP=$(OCAMLOPT)
COMP=$(OCAMLC)
ROOT=../..
OPAM_LIB=$(shell opam config var lib)
PPXFLAGS=-ppx "$(OPAM_LIB)/ppx_deriving/ppx_deriving package:ppx_optcomp"
FLAGS=$(PPXFLAGS) -g
EXE=\
mlw_tree \
why3_prove \
why3_ptree
INCLUDES=-I $(ROOT)/lib/why3 -I $(ROOT)/lib/why3 -I $(OPAM_LIB)/zip -I $(OPAM_LIB)/menhirLib
LIBS=\
menhirLib.cma \
str.cma \
unix.cma \
nums.cma \
dynlink.cma \
zip.cma \
$(ROOT)/lib/why3/why3.cma
all: clean $(EXE)
mlw_tree: mlw_tree.ml
$(COMP) $(FLAGS) -o $@ $(INCLUDES) $(LIBS) $(ROOT)/examples/use_api/mlw_tree.ml
why3_prove: why3_prove.ml
$(COMP) $(FLAGS) -o $@ $(INCLUDES) $(LIBS) $(ROOT)/examples/use_api/why3_prove.ml
why3_ptree: why3ml_pp.ml why3_ptree.ml
$(COMP) $(FLAGS) -o $@ $(INCLUDES) $(LIBS) $(ROOT)/examples/use_api/why3ml_pp.ml $(ROOT)/examples/use_api/why3_ptree.ml
clean:
rm -fv *.cm* *.o $(EXE)
[%%define WHY3VERSION 130]
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2019 -- 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 file builds some MLW modules, using parse trees instead of direct
API calls
******************)
(* BEGIN{buildenv} *)
open Why3
let config : Whyconf.config = Whyconf.read_config None
let main : Whyconf.main = Whyconf.get_main config
let env : Env.env = Env.create_env (Whyconf.loadpath main)
open Ptree
(* END{buildenv} *)
(* printing *)
let get_and_print_mods () =
let fname = Sys.argv.(1) in
let path = [] in
let lb = Lexing.from_channel (open_in fname) in
Loc.set_file fname lb;
let mlw_file = Lexer.parse_mlw_file lb in
let mods =
try
Typing.type_mlw_file env path fname mlw_file
with
e -> ignore (Typing.discard_file ()); raise e
in
if path = [] then begin
let print_m _ m = Format.eprintf "%a@\n@." Pmodule.print_module m in
let add_m _ m mods = Ident.Mid.add m.Pmodule.mod_theory.Theory.th_name m mods in
Ident.Mid.iter print_m (Wstdlib.Mstr.fold add_m mods Ident.Mid.empty)
end;
mods
let mods =
if Array.length Sys.argv >= 3 then
(
match Sys.argv.(2) with
| "--type-only" -> Debug.set_flag Typing.debug_parse_only ; Printf.printf "TYPE ONLY !\n"
| "--parse-only" -> Debug.set_flag Typing.debug_type_only ; Printf.printf "PARSE ONLY !\n"
| "--type-parse-only" -> Debug.set_flag Typing.debug_type_only ; Debug.set_flag Typing.debug_parse_only ; Printf.printf "TYPE AND PARSE ONLY !\n"
| _ -> Printf.eprintf "error flag" ; exit 2
);
get_and_print_mods ()
(* BEGIN{checkingvcs} *)
let my_tasks : Task.task list =
let mods =
Wstdlib.Mstr.fold
(fun _ m acc ->
List.rev_append
(Task.split_theory m.Pmodule.mod_theory None None) acc)
mods []
in List.rev mods
(*
open Format
let () =
printf "Tasks are:@.";
let _ =
List.fold_left
(fun i t -> printf "Task %d: %a@." i Pretty.print_task t; i+1)
1 my_tasks
in ()
let provers : Whyconf.config_prover Whyconf.Mprover.t =
Whyconf.get_provers config
let alt_ergo : Whyconf.config_prover =
let fp = Whyconf.parse_filter_prover "Alt-Ergo" in
(** all provers that have the name "Alt-Ergo" *)
let provers = Whyconf.filter_provers config fp in
if Whyconf.Mprover.is_empty provers then begin
eprintf "Prover Alt-Ergo not installed or not configured@.";
exit 0
end else
snd (Whyconf.Mprover.max_binding provers)
let alt_ergo_driver : Driver.driver =
try
Whyconf.load_driver main env alt_ergo.Whyconf.driver []
with e ->
eprintf "Failed to load driver for alt-ergo: %a@."
Exn_printer.exn_printer e;
exit 1
let () =
let _ =
List.fold_left
(fun i t ->
let r =
Call_provers.wait_on_call
(Driver.prove_task ~limit:Call_provers.empty_limit
~command:alt_ergo.Whyconf.command
alt_ergo_driver t)
in
printf "@[On task %d, alt-ergo answers %a@."
i (Call_provers.print_prover_result ~json_model:false) r;
i+1
)
1 my_tasks
in ()
(* END{checkingvcs} *)
*)
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2019 -- 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 Why3
(* printing *)
open Format
open Pp
let usage = "why3_ptree <optional \"term\" or \"decl\"> <string|file>"
module J = struct
let log ?(level=0) = Format.printf
let fatal ?(level=0) = log
let result ?(level=0) = log
end
let error e= J.log "error : %s : %s\n" e usage
let () =
try
match Array.length Sys.argv with
| 2 ->
let ast = let lb = Lexing.from_channel (open_in Sys.argv.(1)) in Lexer.parse_mlw_file lb in
J.log "%a@." Why3ml_pp.Output_ast.print_mlw_file ast;
J.log "\n";
J.log "%a@." Why3ml_pp.Output_mlw.print_mlw_file ast
| 3 ->
let arg = Sys.argv.(2) in (
match Sys.argv.(1) with
| "term" ->
let ast = let lb = Lexing.from_string arg in Lexer.parse_term lb in
J.log "%a@." Why3ml_pp.Output_ast.print_term ast;
J.log "\n";
J.log "%a@." Why3ml_pp.Output_mlw.print_term ast
| "decl" ->
let ast = let lb = Lexing.from_string arg in Lexer.parse_decl lb in
J.log "%a@." Why3ml_pp.Output_ast.print_decl ast;
J.log "\n";
J.log "%a@." Why3ml_pp.Output_mlw.print_decl ast
| _ -> error "" )
| _ -> error ""
with
| Invalid_argument e -> error e
This diff is collapsed.
......@@ -11,6 +11,8 @@
val parse_term : Lexing.lexbuf -> Ptree.term
val parse_decl : Lexing.lexbuf -> Ptree.decl
val parse_term_list: Lexing.lexbuf -> Ptree.term list
val parse_qualid: Lexing.lexbuf -> Ptree.qualid
......@@ -19,6 +21,7 @@ val parse_list_qualid: Lexing.lexbuf -> Ptree.qualid list
val parse_list_ident: Lexing.lexbuf -> Ptree.ident list
val parse_mlw_file: Lexing.lexbuf -> Ptree.mlw_file
(*
val parse_program_file : Ptree.incremental -> Lexing.lexbuf -> unit
*)
......@@ -271,6 +271,8 @@ rule token = parse
let parse_term = build_parsing_function Parser.term_eof
let parse_decl = build_parsing_function Parser.decl_eof
let parse_term_list = build_parsing_function Parser.term_comma_list_eof
let parse_qualid = build_parsing_function Parser.qualid_eof
......@@ -279,6 +281,8 @@ rule token = parse
let parse_list_qualid = build_parsing_function Parser.qualid_comma_list_eof
let parse_mlw_file = build_parsing_function Parser.mlw_file_parsing_only
open Wstdlib
open Ident
open Theory
......
......@@ -279,7 +279,9 @@
(* Entry points *)
%start <Pmodule.pmodule Wstdlib.Mstr.t> mlw_file
%start <Ptree.mlw_file> mlw_file_parsing_only
%start <Ptree.term> term_eof
%start <Ptree.decl> decl_eof
%start <Ptree.qualid> qualid_eof
%start <Ptree.qualid list> qualid_comma_list_eof
%start <Ptree.term list> term_comma_list_eof
......@@ -287,11 +289,15 @@
%%
(* parsing of a single term *)
(* parsing of a single term or a single decl *)
term_eof:
| term EOF { $1 }
decl_eof:
| pure_decl EOF { $1 }
| prog_decl EOF { $1 }
(* Modules and scopes *)
mlw_file:
......@@ -302,18 +308,34 @@ mlw_file:
{ let loc = floc $startpos($3) $endpos($3) in
Typing.close_module loc; Typing.close_file () }
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:
| module_head module_decl_no_head* END
{ Typing.close_module (floc $startpos($3) $endpos($3)) }
mlw_module_parsing_only:
| module_head_parsing_only module_decl_no_head_parsing_only* END { ($1,$2) }
module_head:
| THEORY attrs(uident_nq) { Typing.open_module $2 }
| MODULE attrs(uident_nq) { Typing.open_module $2 }
module_head_parsing_only:
| THEORY attrs(uident_nq) { $2 }
| MODULE attrs(uident_nq) { $2 }
scope_head:
| SCOPE boption(IMPORT) uident
| SCOPE boption(IMPORT) attrs(uident_nq)
{ Typing.open_scope (floc $startpos $endpos) $3; $2 }
scope_head_parsing_only:
| SCOPE boption(IMPORT) attrs(uident_nq)
{ let loc = floc $startpos $endpos in (loc, $2, $3) }
module_decl:
| scope_head module_decl* END
{ Typing.close_scope (floc $startpos($1) $endpos($1)) ~import:$1 }
......@@ -325,6 +347,15 @@ module_decl:
}
| use_clone { () }
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 }
(* Do not open inside another module *)
mlw_module_no_decl:
| SCOPE | IMPORT | USE | CLONE | pure_decl | prog_decl | meta_decl
{ let loc = floc $startpos $endpos in
......@@ -332,6 +363,13 @@ mlw_module_no_decl:
| mlw_module
{ $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:
| THEORY | MODULE
{ let loc = floc $startpos $endpos in
......@@ -339,6 +377,13 @@ module_decl_no_head:
| module_decl
{ $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:
......@@ -370,6 +415,22 @@ use_clone:
let decl = Ptree.Dcloneimport(loc,import,$3,as_opt,$5) in
Typing.add_decl loc decl
}
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)) }
use_as:
| n = tqualid q = option(preceded(AS, uident)) { (n, q) }
......
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