Skip to content

GitLab

why3
why3
Commit 9b255042 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

Parser: merge "why" and "whyml" formats, move to Mlw

parent a3109482
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 235 additions and 336 deletions
Makefile.in
View file @ 9b255042
......@@ -154,7 +154,7 @@ LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
LIB_MLW = ity expr dexpr pdecl pmodule
LIB_PARSER = ptree glob parser typing lexer
LIB_PARSER = ptree glob typing parser lexer
LIB_TRANSFORM = simplify_formula inlining split_goal induction \
detect_polymorphism \
......@@ -173,10 +173,6 @@ LIB_TRANSFORM = simplify_formula inlining split_goal induction \
LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs isabelle \
simplify gappa cvc3 yices mathematica
LIB_WHYML = mlw_ty mlw_expr mlw_decl mlw_pretty mlw_wp mlw_module \
mlw_dexpr mlw_typing mlw_driver mlw_exec mlw_ocaml \
mlw_main mlw_interp
LIB_SESSION = compress xml termcode session session_tools strategy \
strategy_parser session_scheduler
......@@ -187,10 +183,9 @@ LIBMODULES = $(addprefix src/util/, $(LIB_UTIL)) \
$(addprefix src/parser/, $(LIB_PARSER)) \
$(addprefix src/transform/, $(LIB_TRANSFORM)) \
$(addprefix src/printer/, $(LIB_PRINTER)) \
$(addprefix src/whyml/, $(LIB_WHYML)) \
$(addprefix src/session/, $(LIB_SESSION))
LIBDIRS = util core driver mlw parser transform printer whyml session
LIBDIRS = util core driver mlw parser transform printer session
LIBINCLUDES = $(addprefix -I src/, $(LIBDIRS))
LIBDEP = $(addsuffix .dep, $(LIBMODULES))
......@@ -453,7 +448,10 @@ install_no_local::
TOOLSGENERATED = src/tools/why3wc.ml
TOOLS_BIN = why3config why3execute why3extract why3prove \
# TODO
#TOOLS_BIN = why3config why3execute why3extract why3prove \
# why3realize why3replay why3wc
TOOLS_BIN = why3config why3prove \
why3realize why3replay why3wc
TOOLS_FILES = main $(TOOLS_BIN)
......@@ -1384,8 +1382,9 @@ $(WHY3DOCDEP): $(WHY3DOCGENERATED)
# build targets
byte: bin/why3doc.byte
opt: bin/why3doc.opt
# TODO
#byte: bin/why3doc.byte
#opt: bin/why3doc.opt
bin/why3doc.opt: lib/why3/why3.cmxa $(WHY3DOCCMX)
$(if $(QUIET),@echo 'Linking $@' &&) \
......@@ -1412,7 +1411,8 @@ clean_old_install::
install_no_local::
cp -f bin/why3doc.@OCAMLBEST@ $(TOOLDIR)/why3doc$(EXE)
install_local:: bin/why3doc
# TODO
#install_local:: bin/why3doc
########
# bench
......@@ -1602,8 +1602,6 @@ MODULESTODOC = \
core/env core/task \
driver/whyconf driver/driver \
session/session session/session_tools session/session_scheduler \
whyml/mlw_ty whyml/mlw_expr whyml/mlw_decl whyml/mlw_module \
whyml/mlw_main
# transform/introduction \
# ide/db
......
src/mlw/dexpr.ml
View file @ 9b255042
......@@ -795,6 +795,8 @@ let check_spec dsp ecty e =
if check_rwd && bad_write eeff ueff then
Loc.errorm ?loc:(e_locate_effect (fun eff -> bad_write eff ueff) e)
"this@ expression@ produces@ an@ unlisted@ write@ effect";
(* TODO FIXME : revise the requirements for explicit "raises".
Should we only require them at the top level? *)
if ecty.cty_args <> [] && bad_raise eeff ueff then Sexn.iter (fun xs ->
Loc.errorm ?loc:(e_locate_effect (fun eff -> Sexn.mem xs eff.eff_raises) e)
"this@ expression@ raises@ unlisted@ exception@ %a"
......
src/mlw/pdecl.ml
View file @ 9b255042
......@@ -368,3 +368,7 @@ let known_add_decl kn0 d =
let unk = Mid.set_diff d.pd_syms kn in
if Sid.is_empty unk then kn else
raise (Decl.UnknownIdent (Sid.choose unk))
(** {2 Pretty-printing} *)
let print_pdecl _fmt _d = assert false (* TODO *)
src/mlw/pdecl.mli
View file @ 9b255042
......@@ -82,3 +82,7 @@ type known_map = pdecl Mid.t
val known_id : known_map -> ident -> unit
val known_add_decl : known_map -> pdecl -> known_map
val merge_known : known_map -> known_map -> known_map
(** {2 Pretty-printing *)
val print_pdecl : Format.formatter -> pdecl -> unit
src/mlw/pmodule.ml
View file @ 9b255042
......@@ -297,10 +297,11 @@ let add_pdecl_with_tuples _uc _md = assert false (*TODO*)
(** {2 WhyML language} *)
type mlw_file = pmodule Mstr.t * theory Mstr.t
type mlw_file = pmodule Mstr.t
let mlw_language =
(Env.register_language Env.base_language snd : mlw_file Env.language)
let conv mm = Mstr.map (fun m -> m.mod_theory) mm in
(Env.register_language Env.base_language conv : mlw_file Env.language)
(* TODO
let () = Env.add_builtin mlw_language (function
......@@ -314,7 +315,7 @@ exception ModuleNotFound of Env.pathname * string
let read_module env path s =
let path = if path = [] then ["why3"; s] else path in
let mm, _ = Env.read_library mlw_language env path in
let mm = Env.read_library mlw_language env path in
Mstr.find_exn (ModuleNotFound (path,s)) s mm
let print_path fmt sl =
......
src/mlw/pmodule.mli
View file @ 9b255042
......@@ -120,7 +120,7 @@ val add_pdecl_with_tuples : pmodule_uc -> pdecl -> pmodule_uc
open Env
type mlw_file = pmodule Mstr.t * theory Mstr.t
type mlw_file = pmodule Mstr.t
val mlw_language : mlw_file language
......
src/parser/lexer.mli
View file @ 9b255042
......@@ -8,5 +8,3 @@
(* on linking described in file LICENSE. *)
(* *)
(********************************************************************)
val parse_program_file : Ptree.incremental -> Lexing.lexbuf -> unit
src/parser/lexer.mll
View file @ 9b255042
......@@ -75,7 +75,6 @@
"ghost", GHOST;
"invariant", INVARIANT;
"loop", LOOP;
"model", MODEL;
"module", MODULE;
"mutable", MUTABLE;
"private", PRIVATE;
......@@ -157,8 +156,6 @@ rule token = parse
{ LEFTPAR_STAR_RIGHTPAR }
| "(*"
{ Lexlib.comment lexbuf; token lexbuf }
| "~'" (lident as id)
{ OPAQUE_QUOTE_LIDENT id }
| "'" (lident as id)
{ QUOTE_LIDENT id }
| "'" (uident as id)
......@@ -225,27 +222,38 @@ rule token = parse
{ raise (IllegalCharacter c) }
{
let parse_logic_file env path lb =
open_file token (Lexing.from_string "") (Typing.open_file env path);
Loc.with_location (logic_file token) lb;
Typing.close_file ()
let debug = Debug.register_info_flag "print_modules"
~desc:"Print@ program@ modules@ after@ typechecking."
let parse_program_file inc lb =
open_file token (Lexing.from_string "") inc;
Loc.with_location (program_file token) lb
open Stdlib
open Ident
open Theory
open Pmodule
let read_channel env path file c =
let lb = Lexing.from_channel c in
Loc.set_file file lb;
parse_logic_file env path lb
Typing.open_file ~pure:false env path;
let mm = Loc.with_location (mlw_file token) lb in
if path = [] && Debug.test_flag debug then begin
let add_m _ m mm = Mid.add m.mod_theory.th_name m mm in
let mm = Mstr.fold add_m mm Mid.empty in
let print_m _ m = Format.eprintf
"@[<hov 2>module %a@\n%a@]@\nend@\n@." Pretty.print_th m.mod_theory
(Pp.print_list Pp.newline2 Pdecl.print_pdecl) m.mod_decls in
Mid.iter print_m mm
end;
mm
let () = Env.register_format Env.base_language "why" ["why"] read_channel
~desc:"WhyML@ logical@ language"
}
let () = Env.register_format mlw_language "whyml" ["mlw"] read_channel
~desc:"WhyML@ programming@ and@ specification@ language"
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. test"
End:
*)
let read_channel env path file c =
let lb = Lexing.from_channel c in
Loc.set_file file lb;
Typing.open_file ~pure:true env path;
Loc.with_location (mlw_file token) lb
let () = Env.register_format mlw_language "whyml_spec" ["why"] read_channel
~desc:"WhyML@ specification@ sublanguage"
}
src/parser/parser.mly
View file @ 9b255042
......@@ -10,21 +10,6 @@
(********************************************************************)
%{
module Incremental = struct
let stack = Stack.create ()
let open_file inc = Stack.push inc stack
let close_file () = ignore (Stack.pop stack)
let open_theory id = (Stack.top stack).Ptree.open_theory id
let close_theory () = (Stack.top stack).Ptree.close_theory ()
let open_module id = (Stack.top stack).Ptree.open_module id
let close_module () = (Stack.top stack).Ptree.close_module ()
let open_namespace n = (Stack.top stack).Ptree.open_namespace n
let close_namespace l b = (Stack.top stack).Ptree.close_namespace l b
let new_decl loc d = (Stack.top stack).Ptree.new_decl loc d
let new_pdecl loc d = (Stack.top stack).Ptree.new_pdecl loc d
let use_clone loc use = (Stack.top stack).Ptree.use_clone loc use
end
open Ptree
let infix s = "infix " ^ s
......@@ -111,7 +96,7 @@ end
%token <Ptree.real_constant> FLOAT
%token <string> STRING
%token <Loc.position> POSITION
%token <string> QUOTE_UIDENT QUOTE_LIDENT OPAQUE_QUOTE_LIDENT
%token <string> QUOTE_UIDENT QUOTE_LIDENT
(* keywords *)
......@@ -125,7 +110,7 @@ end
%token ABSTRACT ABSURD ANY ASSERT ASSUME BEGIN CHECK
%token DIVERGES DO DONE DOWNTO ENSURES EXCEPTION FOR
%token FUN GHOST INVARIANT LOOP MODEL MODULE MUTABLE
%token FUN GHOST INVARIANT LOOP MODULE MUTABLE
%token PRIVATE RAISE RAISES READS REC REQUIRES RETURNS
%token TO TRY VAL VARIANT WHILE WRITES
......@@ -173,51 +158,33 @@ end
(* Entry points *)
%start <Ptree.incremental -> unit> open_file
%start <unit> logic_file program_file
%start <Pmodule.pmodule Stdlib.Mstr.t> mlw_file
%%
(* Theories, modules, namespaces *)
open_file:
(* Dummy token. Menhir does not accept epsilon. *)
| EOF { Incremental.open_file }
logic_file:
| theory* EOF { Incremental.close_file () }
program_file:
| theory_or_module* EOF { Incremental.close_file () }
theory:
| theory_head theory_decl* END { Incremental.close_theory () }
mlw_file:
| theory_or_module* EOF { Typing.close_file () }
(* TODO
| module_decl* EOF { Typing.close_file () }
*)
theory_or_module:
| theory { () }
| module_head module_decl* END { Incremental.close_module () }
theory_head:
| THEORY labels(uident) { Incremental.open_theory $2 }
| module_head module_decl* END
{ Typing.close_module (floc $startpos($3) $endpos($3)) }
module_head:
| MODULE labels(uident) { Incremental.open_module $2 }
theory_decl:
| decl { Incremental.new_decl (floc $startpos $endpos) $1 }
| use_clone { Incremental.use_clone (floc $startpos $endpos) $1 }
| namespace_head theory_decl* END
{ Incremental.close_namespace (floc $startpos($1) $endpos($1)) $1 }
| THEORY labels(uident) { Typing.open_module $2 ~theory:true }
| MODULE labels(uident) { Typing.open_module $2 ~theory:false }
module_decl:
| decl { Incremental.new_decl (floc $startpos $endpos) $1 }
| pdecl { Incremental.new_pdecl (floc $startpos $endpos) $1 }
| use_clone { Incremental.use_clone (floc $startpos $endpos) $1 }
| decl { Typing.add_decl (floc $startpos $endpos) $1 }
| use_clone { Typing.use_clone (floc $startpos $endpos) $1 }
| namespace_head module_decl* END
{ Incremental.close_namespace (floc $startpos($1) $endpos($1)) $1 }
{ Typing.close_namespace (floc $startpos($1) $endpos($1)) ~import:$1 }
namespace_head:
| NAMESPACE boption(IMPORT) uident
{ Incremental.open_namespace $3.id_str; $2 }
| NAMESPACE boption(IMPORT) uident { Typing.open_namespace $3; $2 }
(* Use and clone *)
......@@ -252,7 +219,6 @@ ns:
decl:
| TYPE with_list1(type_decl) { Dtype $2 }
| TYPE late_invariant { Dtype [$2] }
| CONSTANT constant_decl { Dlogic [$2] }
| FUNCTION function_decl with_logic_decl* { Dlogic ($2::$3) }
| PREDICATE predicate_decl with_logic_decl* { Dlogic ($2::$3) }
......@@ -262,6 +228,7 @@ decl:
| LEMMA labels(ident) COLON term { Dprop (Decl.Plemma, $2, $4) }
| GOAL labels(ident) COLON term { Dprop (Decl.Pgoal, $2, $4) }
| META sident comma_list1(meta_arg) { Dmeta ($2, $3) }
| pdecl { $1 }
meta_arg:
| TYPE ty { Mty $2 }
......@@ -275,40 +242,44 @@ meta_arg:
(* Type declarations *)
type_decl:
| labels(lident) ty_var* typedefn
{ let model, vis, def, inv = $3 in
let vis = if model then Abstract else vis in
| labels(lident) ty_var* typedefn invariant*
{ let (vis, mut), def = $3 in
{ td_ident = $1; td_params = $2;
td_model = model; td_vis = vis; td_def = def;
td_inv = inv; td_loc = floc $startpos $endpos } }
late_invariant:
| labels(lident) ty_var* invariant+
{ { td_ident = $1; td_params = $2;
td_model = false; td_vis = Public; td_def = TDabstract;
td_inv = $3; td_loc = floc $startpos $endpos } }
td_vis = vis; td_mut = mut;
td_inv = $4; td_def = def;
td_loc = floc $startpos $endpos } }
ty_var:
| labels(quote_lident) { $1 }
(* TODO: should global "mutable" imply "private"?
"type t 'a = mutable { x : int }"
- if "x" is immutable then the type can only be private
- if "x" is automatically mutable then I don't like it
- if there are known mutable fields, then a global "mutable"
is redundant, unless it also means "private" *)
(* TODO: what should be the syntax for mutable private records
without known fields? *)
typedefn:
| (* epsilon *)
{ false, Public, TDabstract, [] }
| model abstract bar_list1(type_case) invariant*
{ $1, $2, TDalgebraic $3, $4 }
| model abstract LEFTBRC semicolon_list1(type_field) RIGHTBRC invariant*
{ $1, $2, TDrecord $4, $6 }
| model abstract ty invariant*
{ $1, $2, TDalias $3, $4 }
model:
| EQUAL { false }
| MODEL { true }
{ (Public, false), TDabstract }
| EQUAL vis_mut bar_list1(type_case)
{ $2, TDalgebraic $3 }
| EQUAL vis_mut LEFTBRC semicolon_list1(type_field) RIGHTBRC
{ $2, TDrecord $4 }
| EQUAL vis_mut ty
{ $2, TDalias $3 }
vis_mut:
| (* epsilon *) { Public, false }
| MUTABLE { Public, true }
| abstract { $1, false }
| abstract MUTABLE { $1, true }
| MUTABLE abstract { $2, true }
abstract:
| (* epsilon *) { Public }
| PRIVATE { Private }
| ABSTRACT { Abstract }
| PRIVATE { Private }
| ABSTRACT { Abstract }
type_field:
| field_modifiers labels(lident) cast
......@@ -370,8 +341,7 @@ ty:
ty_arg:
| lqualid { PTtyapp ($1, []) }
| quote_lident { PTtyvar ($1, false) }
| opaque_quote_lident { PTtyvar ($1, true) }
| quote_lident { PTtyvar $1 }
| LEFTPAR comma_list2(ty) RIGHTPAR { PTtuple $2 }
| LEFTPAR RIGHTPAR { PTtuple [] }
| LEFTPAR ty RIGHTPAR { PTparen $2 }
......@@ -886,10 +856,6 @@ uident:
lident:
| LIDENT { mk_id $1 $startpos $endpos }
| lident_keyword { mk_id $1 $startpos $endpos }
lident_keyword:
| MODEL { "model" }
quote_uident:
| QUOTE_UIDENT { mk_id ("'" ^ $1) $startpos $endpos }
......@@ -897,9 +863,6 @@ quote_uident:
quote_lident:
| QUOTE_LIDENT { mk_id $1 $startpos $endpos }
opaque_quote_lident:
| OPAQUE_QUOTE_LIDENT { mk_id $1 $startpos $endpos }
(* Idents + symbolic operation names *)
ident_rich:
......
src/parser/ptree.ml
View file @ 9b255042
......@@ -42,10 +42,8 @@ type qualid =
| Qident of ident
| Qdot of qualid * ident
type opacity = bool
type pty =
| PTtyvar of ident * opacity
| PTtyvar of ident
| PTtyapp of qualid * pty list
| PTtuple of pty list
| PTarrow of pty * pty
......@@ -127,7 +125,7 @@ type type_def =
| TDalgebraic of (loc * ident * param list) list
| TDrecord of field list
type visibility = Public | Private | Abstract
type visibility = Public | Private | Abstract (* = Private + ghost fields *)
type invariant = term list
......@@ -135,10 +133,10 @@ type type_decl = {
td_loc : loc;
td_ident : ident;
td_params : ident list;
td_model : bool;
td_vis : visibility;
td_vis : visibility; (* records only *)
td_mut : bool; (* records or abstract types *)
td_inv : invariant; (* records only *)
td_def : type_def;
td_inv : invariant;
}
type logic_decl = {
......@@ -166,13 +164,6 @@ type metarg =
type use_clone = use * clone_subst list option
type decl =
| Dtype of type_decl list
| Dlogic of logic_decl list
| Dind of Decl.ind_sign * ind_decl list
| Dprop of Decl.prop_kind * ident * term
| Dmeta of ident * metarg list
(* program files *)
type assertion_kind = Aassert | Aassume | Acheck
......@@ -259,23 +250,14 @@ and fundef = ident * top_ghost * lambda
and lambda = binder list * pty option * expr * spec
type pdecl =
type decl =
| Dtype of type_decl list
| Dlogic of logic_decl list
| Dind of Decl.ind_sign * ind_decl list
| Dprop of Decl.prop_kind * ident * term
| Dmeta of ident * metarg list
| Dval of ident * top_ghost * type_v
| Dlet of ident * top_ghost * expr
| Dfun of ident * top_ghost * lambda
| Drec of fundef list
| Dexn of ident * pty
(* incremental parsing *)
type incremental = {
open_theory : ident -> unit;
close_theory : unit -> unit;
open_module : ident -> unit;
close_module : unit -> unit;
open_namespace : string -> unit;
close_namespace : loc -> bool (*import:*) -> unit;
new_decl : loc -> decl -> unit;
new_pdecl : loc -> pdecl -> unit;
use_clone : loc -> use_clone -> unit;
}
src/parser/typing.ml
View file @ 9b255042
This diff is collapsed.
src/parser/typing.mli
View file @ 9b255042
......@@ -9,50 +9,22 @@
(* *)
(********************************************************************)
(** Typing environments *)
open Stdlib
open Term
open Theory
val debug_parse_only : Debug.flag
val debug_type_only : Debug.flag
(** incremental parsing *)
val add_decl : Loc.position -> theory_uc -> Ptree.decl -> theory_uc
val add_use_clone :
Env.env -> theory Mstr.t -> theory_uc ->
Loc.position -> Ptree.use_clone -> theory_uc
val close_namespace : Loc.position -> bool -> theory_uc -> theory_uc
val close_theory : theory Mstr.t -> theory_uc -> theory Mstr.t
val open_file : Env.env -> Env.pathname -> Ptree.incremental
val close_file : unit -> theory Mstr.t
(***************************************************************************)
(** The following is exported for program typing (src/whyml/mlw_typing.ml) *)
(***************************************************************************)
val debug_type_only : Debug.flag
val create_user_id : Ptree.ident -> Ident.preid
val open_file : Env.env -> Env.pathname -> pure:bool -> unit
val qloc : Ptree.qualid -> Loc.position
val string_list_of_qualid : Ptree.qualid -> string list
val print_qualid : Format.formatter -> Ptree.qualid -> unit
val close_file : unit -> Pmodule.pmodule Stdlib.Mstr.t
exception UnboundSymbol of Ptree.qualid
val open_module : Ptree.ident -> theory:bool -> unit
val find_qualid :
('a -> Ident.ident) -> ('b -> string list -> 'a) -> 'b -> Ptree.qualid -> 'a
val close_module : Ptree.loc -> unit
type global_vs = Ptree.qualid -> vsymbol option
val open_namespace : Ptree.ident -> unit
val type_term : theory_uc -> global_vs -> Ptree.term -> term
val close_namespace : Ptree.loc -> import:bool -> unit
val type_fmla : theory_uc -> global_vs -> Ptree.term -> term
val add_decl : Ptree.loc -> Ptree.decl -> unit
val type_inst : theory_uc -> theory -> Ptree.clone_subst list -> th_inst
val use_clone : Ptree.loc -> Ptree.use_clone -> unit
src/tools/why3prove.ml
View file @ 9b255042
......@@ -330,8 +330,10 @@ let do_theory env drv fname tname th glist elist =
let l,t = Decl.open_ls_defn d in
match l with
| [] ->
(* TODO
let t = Mlw_interp.eval_global_term env th.th_known t in
printf "@[<hov 2>Evaluation of %s:@ %a@]@." x Mlw_interp.print_value t
*) ()
| _ ->
eprintf "Symbol '%s' is not a constant in theory '%s'.@." x tname;
exit 1
......
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