Commit bef75e8d authored by Andrei Paskevich's avatar Andrei Paskevich

remove src/whyml

parent eed540a1
......@@ -1898,8 +1898,7 @@ MODULESTODOC = \
transform/args_wrapper \
session/session_itp session/controller_itp \
session/itp_communication session/itp_server \
whyml/mlw_ty whyml/mlw_expr whyml/mlw_decl whyml/mlw_module \
whyml/mlw_wp
mlw/ity mlw/expr mlw/pdecl mlw/pmodule mlw/vc
FILESTODOC = $(addsuffix .mli, $(addprefix src/, $(MODULESTODOC)))
......
This diff is collapsed.
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2017 -- 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. *)
(* *)
(********************************************************************)
(** {1 Program Declarations} *)
open Ident
open Term
open Mlw_ty
open Mlw_ty.T
open Mlw_expr
(** {2 Type declaration} *)
type constructor = plsymbol * plsymbol option list
type data_decl = itysymbol * constructor list * post
(** {2 Declaration type} *)
type pdecl = private {
pd_node : pdecl_node;
pd_syms : Sid.t; (* idents used in declaration *)
pd_news : Sid.t; (* idents introduced in declaration *)
pd_tag : int; (* unique tag *)
}
and pdecl_node = private
| PDtype of itysymbol
| PDdata of data_decl list
| PDval of let_sym
| PDlet of let_defn
| PDrec of fun_defn list
| PDexn of xsymbol
(** {2 Marks} *)
val ts_mark : Ty.tysymbol
val ty_mark : Ty.ty
val ity_mark : ity
val pv_old : pvsymbol
(** {2 Declaration constructors} *)
type pre_field = preid option * field
type pre_constructor = preid * pre_field list
type pre_data_decl = itysymbol * pre_constructor list
val create_data_decl : pre_data_decl list -> pdecl
val create_ty_decl : itysymbol -> pdecl
val create_val_decl : let_sym -> pdecl
val create_let_decl : let_defn -> pdecl
val create_rec_decl : fun_defn list -> pdecl
val create_exn_decl : xsymbol -> pdecl
(** {2 Type invariants} *)
val null_invariant : itysymbol -> post
val add_invariant : pdecl -> itysymbol -> post -> pdecl
(** {2 Cloning} *)
val clone_data_decl : Mlw_expr.symbol_map -> pdecl -> pdecl
(** {2 Known identifiers} *)
type known_map = pdecl Mid.t
val known_id : known_map -> ident -> unit
val known_add_decl : Decl.known_map -> known_map -> pdecl -> known_map
val merge_known : known_map -> known_map -> known_map
val find_constructors : known_map -> itysymbol -> constructor list
val find_invariant : known_map -> itysymbol -> post
val find_definition : known_map -> psymbol -> fun_defn option
exception NonupdatableType of ity
val inst_constructors :
Decl.known_map -> known_map -> ity -> (lsymbol * field list) list
This diff is collapsed.
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2017 -- 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 Stdlib
open Ident
open Ty
open Term
open Mlw_ty
open Mlw_ty.T
open Mlw_expr
(** Program types *)
type dity
val dity_fresh : unit -> dity
val dity_of_ity : ity -> dity
type dvty = dity list * dity (* A -> B -> C == ([A;B],C) *)
val dity_is_bool : dity -> bool
val dvty_is_chainable : dvty -> bool
(** Patterns *)
type dpattern = private {
dp_pat : pre_ppattern;
dp_dity : dity;
dp_vars : dity Mstr.t;
dp_loc : Loc.position option;
}
type dpattern_node =
| DPwild
| DPvar of preid
| DPlapp of lsymbol * dpattern list
| DPpapp of plsymbol * dpattern list
| DPor of dpattern * dpattern
| DPas of dpattern * preid
| DPcast of dpattern * ity
(** Binders *)
type ghost = bool
type opaque = Stv.t
type dbinder = preid option * ghost * opaque * dity
(** Specifications *)
type 'a later = vsymbol Mstr.t -> 'a
(* Specification terms are parsed and typechecked after the program
expressions, when the types of locally bound program variables are
already established. *)
type dspec_final = {
ds_pre : term list;
ds_post : (vsymbol option * term) list;
ds_xpost : (vsymbol option * term) list Mexn.t;
ds_reads : vsymbol list;
ds_writes : term list;
ds_variant : variant list;
ds_checkrw : bool;
ds_diverge : bool;
}
type dspec = ty -> dspec_final
(* Computation specification is also parametrized by the result type.
All vsymbols in the postcondition clauses in the [ds_post] field
must have this type. All vsymbols in the exceptional postcondition
clauses must have the type of the corresponding exception. *)
type dtype_v =
| DSpecV of dity
| DSpecA of dbinder list * dtype_c
and dtype_c = dtype_v * dspec later
(** Expressions *)
type dinvariant = term list
type dlazy_op = DEand | DEor
type dexpr = private {
de_node : dexpr_node;
de_dvty : dvty;
de_loc : Loc.position option;
}
and dexpr_node =
| DEvar of string * dvty
| DEgpvar of pvsymbol
| DEgpsym of psymbol
| DEplapp of plsymbol * dexpr list
| DElsapp of lsymbol * dexpr list
| DEapply of dexpr * dexpr
| DEconst of Number.constant * ity
| DElam of dbinder list * dexpr * dspec later
| DElet of dlet_defn * dexpr
| DEfun of dfun_defn * dexpr
| DErec of drec_defn * dexpr
| DEif of dexpr * dexpr * dexpr
| DEcase of dexpr * (dpattern * dexpr) list
| DEassign of plsymbol * dexpr * dexpr
| DElazy of dlazy_op * dexpr * dexpr
| DEnot of dexpr
| DEtrue
| DEfalse
| DEraise of xsymbol * dexpr
| DEtry of dexpr * (xsymbol * dpattern * dexpr) list
| DEfor of preid * dexpr * for_direction * dexpr * dinvariant later * dexpr
| DEwhile of dexpr * (variant list * dinvariant) later * dexpr
| DEloop of (variant list * dinvariant) later * dexpr
| DEabsurd
| DEassert of assertion_kind * term later
| DEabstract of dexpr * dspec later
| DEmark of preid * dexpr
| DEghost of dexpr
| DEany of dtype_v * dspec later option
| DEcast of dexpr * ity
| DEuloc of dexpr * Loc.position
| DElabel of dexpr * Slab.t
and dlet_defn = preid * ghost * dexpr
and dfun_defn = preid * ghost * dbinder list * dexpr * dspec later
and drec_defn = private { fds : dfun_defn list }
type dval_decl = preid * ghost * dtype_v
(** Environment *)
type denv
val denv_empty : denv
val denv_add_var : denv -> preid -> dity -> denv
val denv_add_let : denv -> dlet_defn -> denv
val denv_add_fun : denv -> dfun_defn -> denv
val denv_add_args : denv -> dbinder list -> denv
val denv_add_pat : denv -> dpattern -> denv
val denv_get : denv -> string -> dexpr_node (** raises UnboundVar *)
val denv_get_opt : denv -> string -> dexpr_node option
(** Constructors *)
val dpattern : ?loc:Loc.position -> dpattern_node -> dpattern
val dexpr : ?loc:Loc.position -> dexpr_node -> dexpr
type pre_fun_defn =
preid * ghost * dbinder list * dity * (denv -> dexpr * dspec later)
val drec_defn : denv -> pre_fun_defn list -> denv * drec_defn
(** Final stage *)
val expr : keep_loc:bool ->
Decl.known_map -> Mlw_decl.known_map -> dexpr -> expr
val let_defn : keep_loc:bool ->
Decl.known_map -> Mlw_decl.known_map -> dlet_defn -> let_defn
val fun_defn : keep_loc:bool ->
Decl.known_map -> Mlw_decl.known_map -> dfun_defn -> fun_defn
val rec_defn : keep_loc:bool ->
Decl.known_map -> Mlw_decl.known_map -> drec_defn -> fun_defn list
val val_decl : keep_loc:bool ->
Decl.known_map -> Mlw_decl.known_map -> dval_decl -> let_sym
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2017 -- 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 Ident
open Ty
open Term
open Theory
open Printer
open Driver_ast
open Mlw_ty
open Mlw_expr
open Mlw_module
type driver = {
drv_env : Env.env;
drv_printer : string option;
drv_prelude : Printer.prelude;
drv_thprelude : Printer.prelude_map;
drv_blacklist : Printer.blacklist;
drv_syntax : Printer.syntax_map;
drv_converter : Printer.syntax_map;
}
let load_file file =
let c = open_in file in
let lb = Lexing.from_channel c in
Loc.set_file file lb;
let to_close = Stack.create () in
Stack.push c to_close;
let input_lexer filename =
let c = open_in filename in
Stack.push c to_close;
let lb = Lexing.from_channel c in
Loc.set_file filename lb;
lb
in
let f = Driver_lexer.parse_file_extract input_lexer lb in
Stack.iter close_in to_close;
f
exception Duplicate of string
exception UnknownType of (string list * string list)
exception UnknownLogic of (string list * string list)
exception UnknownProp of (string list * string list)
exception UnknownVal of (string list * string list)
exception UnknownExn of (string list * string list)
exception FSymExpected of lsymbol
exception PSymExpected of lsymbol
let load_driver env file extra_files =
let prelude = ref [] in
let printer = ref None in
let blacklist = Queue.create () in
let set_or_raise loc r v error = match !r with
| Some _ -> raise (Loc.Located (loc, Duplicate error))
| None -> r := Some v
in
let add_to_list r v = (r := v :: !r) in
let add_global (loc, g) = match g with
| EPrelude s -> add_to_list prelude s
| EPrinter s -> set_or_raise loc printer s "printer"
| EBlacklist sl -> List.iter (fun s -> Queue.add s blacklist) sl
in
let f = load_file file in
List.iter add_global f.fe_global;
let thprelude = ref Mid.empty in
let syntax_map = ref Mid.empty in
let converter_map = ref Mid.empty in
let qualid = ref [] in
let find_pr th (loc,q) = try Theory.ns_find_pr th.th_export q
with Not_found -> raise (Loc.Located (loc, UnknownProp (!qualid,q)))
in
let find_ls th (loc,q) = try Theory.ns_find_ls th.th_export q
with Not_found -> raise (Loc.Located (loc, UnknownLogic (!qualid,q)))
in
let find_ts th (loc,q) = try Theory.ns_find_ts th.th_export q
with Not_found -> raise (Loc.Located (loc, UnknownType (!qualid,q)))
in
let find_fs th q =
let ls = find_ls th q in
if ls.ls_value = None then raise (FSymExpected ls) else ls in
let find_ps th q =
let ls = find_ls th q in
if ls.ls_value <> None then raise (PSymExpected ls) else ls in
let add_syntax id s b =
syntax_map := Mid.add id (s,if b then 1 else 0) !syntax_map in
let add_converter id s b =
converter_map := Mid.add id (s,if b then 1 else 0) !converter_map in
let add_local th = function
| Rprelude s ->
let l = Mid.find_def [] th.th_name !thprelude in
thprelude := Mid.add th.th_name (s::l) !thprelude
| Rsyntaxts (q,s,b) ->
let ts = find_ts th q in
check_syntax_type ts s;
add_syntax ts.ts_name s b
| Rsyntaxfs (q,s,b) ->
let fs = find_fs th q in
check_syntax_logic fs s;
add_syntax fs.ls_name s b
| Rsyntaxps (q,s,b) ->
let ps = find_ps th q in
check_syntax_logic ps s;
add_syntax ps.ls_name s b
| Rconverter _ ->
Loc.errorm "Syntax converter cannot be used in pure theories"
| Rliteral _ ->
Loc.errorm "Syntax literal cannot be used in pure theories"
| Rremovepr (q) ->
ignore (find_pr th q)
| Rremoveall ->
let it key _ = match (Mid.find key th.th_known).Decl.d_node with
| Decl.Dprop (_,symb,_) -> ignore symb
| _ -> ()
in
Mid.iter it th.th_local
| Rmeta (s,al) ->
let rec ty_of_pty = function
| PTyvar x ->
Ty.ty_var (Ty.tv_of_string x)
| PTyapp ((loc,_) as q,tyl) ->
let ts = find_ts th q in
let tyl = List.map ty_of_pty tyl in
Loc.try2 ~loc Ty.ty_app ts tyl
| PTuple tyl ->
let ts = Ty.ts_tuple (List.length tyl) in
Ty.ty_app ts (List.map ty_of_pty tyl)
in
let convert = function
| PMAty (PTyapp (q,[]))
-> MAts (find_ts th q)
| PMAty ty -> MAty (ty_of_pty ty)
| PMAfs q -> MAls (find_fs th q)
| PMAps q -> MAls (find_ps th q)
| PMApr q -> MApr (find_pr th q)
| PMAstr s -> MAstr s
| PMAint i -> MAint i
in
let m = lookup_meta s in
ignore (create_meta m (List.map convert al))
in
let add_local th (loc,rule) = Loc.try2 ~loc add_local th rule in
let find_val m (loc,q) =
try match ns_find_prog_symbol m.mod_export q with
| PV pv -> pv.pv_vs.vs_name
| PS ps -> ps.ps_name
| PL _ | XS _ | LS _ -> raise Not_found
with Not_found -> raise (Loc.Located (loc, UnknownVal (!qualid,q)))
in
let find_xs m (loc,q) =
try ns_find_xs m.mod_export q
with Not_found -> raise (Loc.Located (loc, UnknownExn (!qualid,q)))
in
let add_local_module loc m = function
| MRexception (q,s) ->
let xs = find_xs m q in
add_syntax xs.xs_name s false
| MRval (q,s) ->
let id = find_val m q in
add_syntax id s false
| MRtheory (Rconverter (q,s,b)) ->
let id = find_val m q in
add_converter id s b
| MRtheory trule ->
add_local m.mod_theory (loc,trule)
in
let add_local_module m (loc,rule) =
Loc.try3 ~loc add_local_module loc m rule
in
let add_theory { thr_name = (loc,q); thr_rules = trl } =
let f,id = let l = List.rev q in List.rev (List.tl l),List.hd l in
let th = Loc.try3 ~loc Env.read_theory env f id in
qualid := q;
List.iter (add_local th) trl
in
let add_module { mor_name = (loc,q); mor_rules = mrl } =
let f,id = let l = List.rev q in List.rev (List.tl l),List.hd l in
let m = Loc.try3 ~loc read_module env f id in
qualid := q;
List.iter (add_local_module m) mrl
in
List.iter add_theory f.fe_th_rules;
List.iter add_module f.fe_mo_rules;
List.iter (fun f ->
let fe = load_file f in
List.iter add_theory fe.fe_th_rules;
List.iter add_module fe.fe_mo_rules)
extra_files;
{
drv_env = env;
drv_printer = !printer;
drv_prelude = List.rev !prelude;
drv_thprelude = Mid.map List.rev !thprelude;
drv_blacklist = Queue.fold (fun l s -> s :: l) [] blacklist;
drv_syntax = !syntax_map;
drv_converter = !converter_map;
}
(* exception report *)
let string_of_qualid thl idl =
String.concat "." thl ^ "." ^ String.concat "." idl
let () = Exn_printer.register (fun fmt exn -> match exn with
| Duplicate s -> Format.fprintf fmt
"Duplicate %s specification" s
| UnknownType (thl,idl) -> Format.fprintf fmt
"Unknown type symbol %s" (string_of_qualid thl idl)
| UnknownLogic (thl,idl) -> Format.fprintf fmt
"Unknown logical symbol %s" (string_of_qualid thl idl)
| UnknownProp (thl,idl) -> Format.fprintf fmt
"Unknown proposition %s" (string_of_qualid thl idl)
| UnknownVal (thl,idl) -> Format.fprintf fmt
"Unknown val %s" (string_of_qualid thl idl)
| UnknownExn (thl,idl) -> Format.fprintf fmt
"Unknown exception %s" (string_of_qualid thl idl)
| FSymExpected ls -> Format.fprintf fmt
"%a is not a function symbol" Pretty.print_ls ls
| PSymExpected ls -> Format.fprintf fmt
"%a is not a predicate symbol" Pretty.print_ls ls
| e -> raise e)
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2017 -- 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. *)
(* *)
(********************************************************************)
type driver = private {
drv_env : Env.env;
drv_printer : string option;
drv_prelude : Printer.prelude;
drv_thprelude : Printer.prelude_map;
drv_blacklist : Printer.blacklist;
drv_syntax : Printer.syntax_map;
drv_converter : Printer.syntax_map;
}
val load_driver : Env.env -> string -> string list -> driver
(** loads a driver from a file
@param env environment to interpret theories and modules
@param string driver file name
@param string list additional drivers containing only theories/modules *)
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2017 -- 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. *)
(* *)
(********************************************************************)
(* First implementation by Jacques-Pascal Deplaix
during an internship at LRI, May-August 2014 *)
open Ty
open Ident
open Term
open Decl
type t = {
driver : Mlw_driver.driver;
th_known_map: Decl.known_map;
mo_known_map: Mlw_decl.known_map;
is_exec_id : bool Hid.t; (* cache *)
}
let create dr thkm mokm =
{ driver = dr;
th_known_map = thkm;
mo_known_map = mokm;
is_exec_id = Hid.create 17; }
let has_syntax ctx id =
Mid.mem id ctx.driver.Mlw_driver.drv_syntax ||
Mid.mem id ctx.driver.Mlw_driver.drv_converter
let is_exec_id ctx id f =
try
Hid.find ctx.is_exec_id id
with Not_found ->
let b = has_syntax ctx id || f ctx id in Hid.add ctx.is_exec_id id b; b
let declare_id ctx id b =
Hid.add ctx.is_exec_id id b
(** Logic *)
let is_exec_const = function
| Number.ConstInt _ -> true
| Number.ConstReal _ -> false
let rec is_exec_term ctx t = match t.t_node with
| Ttrue
| Tfalse
| Tvar _ ->
true
| Tconst c ->
is_exec_const c
| Tapp (ls, tl) when ls.ls_constr > 0 ->
begin match try Some (Mlw_expr.restore_pl ls) with Not_found -> None with
| Some pl ->
let test fd arg = fd.Mlw_expr.fd_ghost || is_exec_term ctx arg in
List.for_all2 test pl.Mlw_expr.pl_args tl
| None -> List.for_all (is_exec_term ctx) tl
end
| Tapp (ls, tl) ->
is_exec_lsymbol ctx ls && List.for_all (is_exec_term ctx) tl
| Tif (t1, t2, t3) ->
is_exec_term ctx t1 && is_exec_term ctx t2 && is_exec_term ctx t3
| Tbinop (_, t1, t2) ->
is_exec_term ctx t1 && is_exec_term ctx t2
| Tnot t ->
is_exec_term ctx t
| Tlet (t1, b2) ->
is_exec_term ctx t1 && is_exec_bound ctx b2
| Tcase (t1, bl) ->
is_exec_term ctx t1 && List.for_all (is_exec_branch ctx) bl
| Teps _ when t_is_lambda t ->
let _, _, t1 = t_open_lambda t in is_exec_term ctx t1
| Teps _ | Tquant _ ->
false
and is_exec_branch ctx b =
let _, t = t_open_branch b in is_exec_term ctx t
and is_exec_bound ctx b =
let _, t = t_open_bound b in is_exec_term ctx t
and is_exec_lsymbol ctx ls =
is_exec_id ctx ls.ls_name
(fun _ _ -> match Mid.find_opt ls.ls_name ctx.th_known_map with
| None -> false
| Some d -> ignore (is_exec_decl ctx d); is_exec_lsymbol ctx ls)
and is_exec_decl ctx d =
let allow_ts ts = declare_id ctx ts.ts_name true in
let allow_ls ls = declare_id ctx ls.ls_name true in
let forbid_ls ls = declare_id ctx ls.ls_name false in
match d.d_node with
| Dtype ts ->
allow_ts ts; true
| Ddata ddl ->
let constructor (ls, prl) =
allow_ls ls; List.iter (Opt.iter allow_ls) prl in