Commit 3804bb49 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove deprecated version of whyml.

parent d9195919
......@@ -359,35 +359,6 @@ install_no_local::
mkdir -p $(LIBDIR)/why3/plugins
cp -f $(foreach f,$(LIBPLUGCMO) $(LIBPLUGCMXS),$(wildcard $(f))) $(LIBDIR)/why3/plugins
########
# Whyml (old API)
########
PGM_FILES = pgm_ttree pgm_types pgm_pretty \
pgm_module pgm_wp pgm_typing pgm_main
PGMMODULES = $(addprefix src/programs/, $(PGM_FILES))
PGMDEP = $(addsuffix .dep, $(PGMMODULES))
PGMCMO = $(addsuffix .cmo, $(PGMMODULES))
PGMCMX = $(addsuffix .cmx, $(PGMMODULES))
$(PGMDEP): DEPFLAGS += -I src/programs
$(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
# depend and clean targets
ifneq "$(MAKECMDGOALS)" "clean"
include $(PGMDEP)
endif
depend: $(PGMDEP)
clean::
rm -f src/programs/*.cm[iox] src/programs/*.o
rm -f src/programs/*.annot src/programs/*.dep src/programs/*~
######
# Why3
######
......
o get rid of types Pgm_ttree.{ipattern, pattern} (use logical patterns instead)
o bug in test-pgm-jcf: scope
o freshness analysis
o no `old' in loop invariants
o use of old in loop invariant should be reported as an error (correctly)
o syntactic sugar for postcondition:
{ pat | q } stands for { let pat = result in q }
particular case { x | ... } to use x instead of result
but also { a,b | ... }, etc.
Andrei: bad idea
o automatically add a label pre_f at entrance of each function f
and then replace (old t) by (at t pre_f)
(so that there is no more 'old' in the abstract syntax)
o what about pervasives old, at, label, unit = ()
in particular, how to prevent old and at from being used in programs?
can we get rid of theories/programs.why?
o program alias, e.g.
let f = String.create
o library
x Array
x String
x Buffer
x Char
- Hashtbl
x Queue
x Stack
- List
- Map
- Set
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2012 -- 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. *)
(* *)
(********************************************************************)
(* CURRENTLY DEAD CODE; FOR LATER USE... *)
open Format
open Why3
open Ident
open Ty
open Term
open Decl
open Theory
open Pgm_ttree
open Pgm_typing
module E = Pgm_types.E
module State : sig
type t
val create : env -> E.t -> t
val push_label : env -> ?label:label -> t -> label * t
val havoc : env -> ?pre:label -> E.t -> t -> t
val term : env -> t -> term -> term
val fmla : env -> ?old:label -> t -> fmla -> fmla
val quantify : env -> t -> E.t -> fmla -> fmla
end = struct
type t = {
current : vsymbol E.Mref.t;
old : vsymbol E.Mref.t Mvs.t;
}
let unref_ty env ty = match ty.ty_node with
| Tyapp (ts, [ty]) when ts_equal ts (ts_ref env) -> ty
| _ -> assert false
let var_of_reference env = function
| E.Rlocal vs ->
create_vsymbol (id_fresh vs.vs_name.id_string) (unref_ty env vs.vs_ty)
| E.Rglobal { ls_name = id; ls_value = Some ty } ->
create_vsymbol (id_fresh id.id_string) (unref_ty env ty)
| E.Rglobal { ls_value = None } ->
assert false
let havoc1 env r m =
let v = var_of_reference env r in
E.Mref.add r v m
let create env ef =
let s = E.Sref.union ef.E.reads ef.E.writes in
{ current = E.Sref.fold (havoc1 env) s E.Mref.empty; old = Mvs.empty; }
let havoc env ?pre ef s =
let l = match pre with
| None -> fresh_label env
| Some l -> l
in
{ current = E.Sref.fold (havoc1 env) ef.E.writes s.current;
old = Mvs.add l s.current s.old; }
let push_label env ?label s =
let l = match label with None -> fresh_label env | Some l -> l in
l, havoc env ~pre:l E.empty s
let ref_at cur s r =
let m = match cur with
| None -> s.current
| Some l -> assert (Mvs.mem l s.old); Mvs.find l s.old
in
assert (E.Mref.mem r m);
E.Mref.find r m
(* old = label for old state, if any
cur = label for current state, if any *)
let rec term_at env old cur s t = match t.t_node with
| Tapp (ls, [t]) when ls_equal ls (ls_bang env) ->
let r = reference_of_term t in
t_var (ref_at cur s r)
(* TODO: old, at *)
| _ ->
t_map (term_at env old cur s) (fmla_at env old cur s) t
and fmla_at env old cur s f =
t_map (term_at env old cur s) (fmla_at env old cur s) f
let term env s t = term_at env None None s t
let fmla env ?old s f = fmla_at env old None s f
let quantify _env s ef f =
let quant r f = wp_forall [ref_at None s r] [] f in
let s = E.Sref.union ef.E.reads ef.E.writes in
E.Sref.fold quant s f
let print _fmt _s = assert false (*TODO*)
end
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2012 -- 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. *)
(* *)
(********************************************************************)
(* main module for whyl *)
open Format
open Why3
open Stdlib
open Typing
open Ptree
open Pgm_module
exception ClashModule of string
let () = Exn_printer.register (fun fmt e -> match e with
| ClashModule m -> fprintf fmt "clash with previous module %s" m
| _ -> raise e)
type theory_ast = {
pth_name : Ptree.ident;
pth_decl : (Ptree.loc * Pgm_typing.program_decl) list;
}
type module_ast = {
mod_name : Ptree.ident;
mod_decl : (Ptree.loc * Pgm_typing.program_decl) list;
}
type theory_module_ast =
| Ptheory of theory_ast
| Pmodule of module_ast
let add_theory env path lenv m =
let id = m.pth_name in
let env = Lexer.library_of_env (Env.env_of_library env) in
let th = Theory.create_theory ~path (Denv.create_user_id id) in
let rec add_decl th (loc,dcl) = match dcl with
| Pgm_typing.PDdecl d ->
Typing.add_decl loc th d
| Pgm_typing.PDuseclone d ->
Typing.add_use_clone env lenv th loc d
| Pgm_typing.PDnamespace (name, import, dl) ->
let th = Theory.open_namespace th name in
let th = List.fold_left add_decl th dl in
Typing.close_namespace loc import th
| Pgm_typing.PDpdecl _ -> assert false
in
let th = List.fold_left add_decl th m.pth_decl in
close_theory lenv th
let add_module ?(type_only=false) env path (ltm, lmod) m =
let id = m.mod_name in
let loc = id.id_loc in
if Mstr.mem id.id lmod then raise (Loc.Located (loc, ClashModule id.id));
let wp = not type_only in
let uc = create_module ~path (Ident.id_user id.id loc) in
let logic_env = Lexer.library_of_env (Env.env_of_library env) in
let prelude = Env.read_lib_theory logic_env ["bool"] "Bool" in
let uc = use_export_theory uc prelude in
let uc = List.fold_left (Pgm_typing.decl ~wp env ltm lmod) uc m.mod_decl in
let md = close_module uc in
Mstr.add ("WP " ^ id.id) md.m_pure ltm, (* avoids a theory/module clash *)
Mstr.add id.id md lmod
let add_theory_module ?(type_only=false) env path (ltm, lmod) = function
| Ptheory t -> add_theory env path ltm t, lmod
| Pmodule m -> add_module ~type_only env path (ltm, lmod) m
open Pgm_typing
let open_file, close_file =
let ids = Stack.create () in
let muc = Stack.create () in
let prf = Stack.create () in
let lenv = Stack.create () in
let open_file () =
Stack.push [] lenv;
let open_theory id = Stack.push id ids; Stack.push [] muc in
let open_module id = Stack.push id ids; Stack.push [] muc in
let close_theory () =
let tast = { pth_name = Stack.pop ids;
pth_decl = List.rev (Stack.pop muc) } in
Stack.push (Ptheory tast :: Stack.pop lenv) lenv in
let close_module () =
let mast = { mod_name = Stack.pop ids;
mod_decl = List.rev (Stack.pop muc) } in
Stack.push (Pmodule mast :: Stack.pop lenv) lenv in
let open_namespace s =
Stack.push s prf; Stack.push [] muc in
let close_namespace loc imp =
let name = Stack.pop prf in
let decl = List.rev (Stack.pop muc) in
Stack.push ((loc, PDnamespace (name,imp,decl)) :: Stack.pop muc) muc in
let new_decl loc d =
Stack.push ((loc, PDdecl d) :: Stack.pop muc) muc in
let new_pdecl loc d =
Stack.push ((loc, PDpdecl d) :: Stack.pop muc) muc in
let use_clone loc use =
Stack.push ((loc, PDuseclone use) :: Stack.pop muc) muc in
{ open_theory = open_theory;
close_theory = close_theory;
open_module = open_module;
close_module = close_module;
open_namespace = open_namespace;
close_namespace = close_namespace;
new_decl = new_decl;
new_pdecl = new_pdecl;
use_clone = use_clone; }
in
let close_file () = List.rev (Stack.pop lenv) in
open_file, close_file
let retrieve env path file c =
let lb = Lexing.from_channel c in
Loc.set_file file lb;
let inc = open_file () in
Lexer.parse_program_file inc lb;
let ml = close_file () in
if Debug.test_flag Typing.debug_parse_only then
Mstr.empty, Mstr.empty
else
let type_only = Debug.test_flag Typing.debug_type_only in
List.fold_left (add_theory_module ~type_only env path)
(Mstr.empty, Mstr.empty) ml
let read_channel env path file c =
let tm, mm = retrieve env path file c in
mm, tm
let read_channel =
let one_time_hack = ref true in
fun env path file c ->
let env =
if !one_time_hack then begin
one_time_hack := false;
let genv = Env.env_of_library env in
Env.register_format "whyml-old-library" ["mlw"] read_channel genv
~desc:"for internal use"
end
else env
in
read_channel env path file c
let library_of_env = Env.register_format "whyml-old" [] read_channel
~desc:"WhyML@ programming@ language@ (obsolete@ implementation)"
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. testl"
End:
*)
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2012 -- 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
open Stdlib
open Ident
open Ty
open Theory
open Term
open Pgm_types
open Pgm_types.T
open Pgm_ttree
type namespace = {
ns_ex : esymbol Mstr.t; (* exceptions*)
ns_ns : namespace Mstr.t; (* inner namespaces *)
}
let empty_ns = {
ns_ex = Mstr.empty;
ns_ns = Mstr.empty;
}
exception ClashSymbol of string
let ns_replace eq chk x vo vn =
if not chk then vn else
if eq vo vn then vo else
raise (ClashSymbol x)
let ns_union eq chk =
Mstr.union (fun x vn vo -> Some (ns_replace eq chk x vo vn))
let rec merge_ns chk ns1 ns2 =
let fusion _ ns1 ns2 = Some (merge_ns chk ns1 ns2) in
{ ns_ex = ns_union ls_equal chk ns1.ns_ex ns2.ns_ex;
ns_ns = Mstr.union fusion ns1.ns_ns ns2.ns_ns; }
let nm_add chk x ns m = Mstr.change (function
| None -> Some ns
| Some os -> Some (merge_ns chk ns os)) x m
let ns_add eq chk x v m = Mstr.change (function
| None -> Some v
| Some vo -> Some (ns_replace eq chk x vo v)) x m
let ex_add = ns_add ls_equal
(* dead code
let mt_add = ns_add mt_equal
*)
let add_ex chk x ls ns = { ns with ns_ex = ex_add chk x ls ns.ns_ex }
let add_ns chk x nn ns = { ns with ns_ns = nm_add chk x nn ns.ns_ns }
let rec ns_find get_map ns = function
| [] -> assert false
| [a] -> Mstr.find a (get_map ns)
| a::l -> ns_find get_map (Mstr.find a ns.ns_ns) l
let ns_find_ex = ns_find (fun ns -> ns.ns_ex)
let ns_find_ns = ns_find (fun ns -> ns.ns_ns)
(* modules under construction *)
type uc = {
uc_name : Ident.ident;
uc_impure : theory_uc; (* the theory used for program types *)
uc_effect : theory_uc; (* the theory used for typing effects *)
uc_pure : theory_uc; (* the logic theory used to type annotations *)
uc_decls : decl list; (* the program declarations *)
uc_prefix : string list;
uc_import : namespace list;
uc_export : namespace list;
}
let namespace uc = List.hd uc.uc_import
let impure_uc uc = uc.uc_impure
let effect_uc uc = uc.uc_effect
let pure_uc uc = uc.uc_pure
(* dead code
let add_pervasives uc =
(* type unit = () *)
let ts =
Ty.create_tysymbol
(id_fresh "unit") [] (Some (Ty.ty_app (Ty.ts_tuple 0) []))
in
add_ty_decl uc ts
*)
let open_namespace uc s = match uc.uc_import with
| ns :: _ -> { uc with
uc_impure = Theory.open_namespace uc.uc_impure s;
uc_effect = Theory.open_namespace uc.uc_effect s;
uc_pure = Theory.open_namespace uc.uc_pure s;
uc_prefix = s :: uc.uc_prefix;
uc_import = ns :: uc.uc_import;
uc_export = empty_ns :: uc.uc_export; }
| [] -> assert false
exception NoOpenedNamespace
let close_namespace uc import =
match uc.uc_prefix, uc.uc_import, uc.uc_export with
| s :: prf, _ :: i1 :: sti, e0 :: e1 :: ste ->
let i1 = if import then merge_ns false e0 i1 else i1 in
let _ = if import then merge_ns true e0 e1 else e1 in
let i1 = add_ns false s e0 i1 in
let e1 = add_ns true s e0 e1 in
let ith = Theory.close_namespace uc.uc_impure import in
let eth = Theory.close_namespace uc.uc_effect import in
let pth = Theory.close_namespace uc.uc_pure import in
{ uc with uc_impure = ith; uc_effect = eth; uc_pure = pth;
uc_import = i1 :: sti; uc_export = e1 :: ste;
uc_prefix = prf; }
| [], [_], [_] -> raise NoOpenedNamespace
| _ -> assert false
(** Insertion of new declarations *)
let add_symbol add id v uc =
match uc.uc_import, uc.uc_export with
| i0 :: sti, e0 :: ste -> { uc with
uc_import = add false id.id_string v i0 :: sti;
uc_export = add true id.id_string v e0 :: ste }
| _ -> assert false
let add_esymbol ls uc =
add_symbol add_ex ls.ls_name ls uc
let add_decl d uc =
{ uc with uc_decls = d :: uc.uc_decls }
let add_impure_decl d uc =
let th = Theory.add_decl_with_tuples uc.uc_impure d in
{ uc with uc_impure = th }
let add_effect_decl d uc =
let th = Theory.add_decl_with_tuples uc.uc_effect d in
{ uc with uc_effect = th }
let add_pure_decl d uc =
let th = Theory.add_decl_with_tuples uc.uc_pure d in
{ uc with uc_pure = th }
(**
let add_psymbol ps uc =
let uc = add_impure_decl (Decl.create_logic_decl [ps.ps_impure, None]) uc in
let uc = add_effect_decl (Decl.create_logic_decl [ps.ps_effect, None]) uc in
let uc = add_pure_decl (Decl.create_logic_decl [ps.ps_pure, None]) uc in
uc
**)
let ls_Exit = create_lsymbol (id_fresh "%Exit") [] (Some ty_exn)
(* type unit = () *)
let ty_unit = ty_tuple []
let ts_unit = create_tysymbol (id_fresh "unit") [] (Some ty_unit)
(* logic ignore 'a : () *)
let ts_mark = create_tysymbol (id_fresh "'mark") [] None
let ty_mark = ty_app ts_mark []
let fs_at =
let ty = ty_var (create_tvsymbol (id_fresh "a")) in
create_lsymbol (id_fresh "at") [ty; ty_mark] (Some ty)
let fs_old =
let ty = ty_var (create_tvsymbol (id_fresh "a")) in
create_lsymbol (id_fresh "old") [ty] (Some ty)
let vs_old = create_vsymbol (id_fresh "'old") ty_mark
let vs_now = create_vsymbol (id_fresh "'now") ty_mark
let th_prelude =
let uc = create_theory (id_fresh "Prelude") in
let uc = use_export uc (tuple_theory 0) in
let uc = add_ty_decl uc ts_unit in
let uc = add_ty_decl uc ts_mark in
let uc = add_param_decl uc fs_at in
let uc = add_param_decl uc fs_old in
close_theory uc
let empty_module path n =
let m = {
uc_name = id_register n;
uc_impure = Theory.create_theory ~path n;
uc_effect = Theory.create_theory ~path n;
uc_pure = Theory.create_theory ~path n;
uc_decls = [];
uc_prefix = [];
uc_import = [empty_ns];
uc_export = [empty_ns]; }
in
(* pervasives *)
let m = add_esymbol ls_Exit m in
(***
let m = add_mtsymbol mt_ghost m in
let m = add_psymbol ps_ghost m in
let m = add_psymbol ps_unghost m in
***)
m
(** Modules *)
type t = {
m_name : Ident.ident;
m_impure : theory;
m_effect : theory;
m_pure : theory;
m_decls : decl list;
m_export : namespace;
}
exception CloseModule
let close_module uc = match uc.uc_export with
| [e] ->
{ m_name = uc.uc_name;
m_decls = List.rev uc.uc_decls;
m_export = e;
m_impure = close_theory uc.uc_impure;
m_effect = close_theory uc.uc_effect;
m_pure = close_theory uc.uc_pure;
}
| _ ->
raise CloseModule
(** Use *)
let use_export uc m =
match uc.uc_import, uc.uc_export with
| i0 :: sti, e0 :: ste -> { uc with
uc_import = merge_ns false m.m_export i0 :: sti;
uc_export = merge_ns true m.m_export e0 :: ste;
uc_impure = Theory.use_export uc.uc_impure m.m_impure;
uc_effect = Theory.use_export uc.uc_effect m.m_effect;
uc_pure = Theory.use_export uc.uc_pure m.m_pure; }
| _ -> assert false
let use_export_theory uc th =
let uc =
{ uc with
uc_impure = Theory.use_export uc.uc_impure th;
uc_effect = Theory.use_export uc.uc_effect th;
uc_pure = Theory.use_export uc.uc_pure th; }
in
(* all type symbols from th are added as (pure) mtsymbols *)
let add_ts _ ts =
ignore
(create_mtsymbol ~impure:ts ~effect:ts ~pure:ts ~singleton:false)
in
let rec add_ns ns uc =
Mstr.iter add_ts ns.Theory.ns_ts;
Mstr.fold (fun _ -> add_ns) ns.Theory.ns_ns uc
in
add_ns th.th_export uc
let create_module ?(path=[]) id =
let uc = empty_module path id in
use_export_theory uc th_prelude
let add_impure_pdecl loc d uc =
{ uc with uc_impure = Typing.add_decl loc uc.uc_impure d }
let add_effect_pdecl loc d uc =
{ uc with uc_effect = Typing.add_decl loc uc.uc_effect d; }
let add_pure_pdecl loc d uc =
{ uc with uc_pure = Typing.add_decl loc uc.uc_pure d; }
let add_use_clone env ltm loc d uc =
let env = Lexer.library_of_env (Env.env_of_library env) in
{ uc with
uc_impure = Typing.add_use_clone env ltm uc.uc_impure loc d;
uc_effect = Typing.add_use_clone env ltm uc.uc_effect loc d;
uc_pure = Typing.add_use_clone env ltm uc.uc_pure loc d; }
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. testl"
End:
*)
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2012 -- 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
open Stdlib
open Ident
open Ty
open Term
open Theory
open Pgm_types
open Pgm_types.T
type namespace = private {
ns_ex : esymbol Mstr.t; (* exception symbols *)
ns_ns : namespace Mstr.t; (* inner namespaces *)
}
val ns_find_ex : namespace -> string list -> esymbol
val ns_find_ns : namespace -> string list -> namespace
(** a module under construction *)
type uc
val namespace : uc -> namespace