Skip to content

GitLab

why3
why3
Commit afd48213 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files
Options

programs: more efficient access to pre-defined symbols; typing is now... 

programs: more efficient access to pre-defined symbols; typing is now state-less (to be re-entrant, if necessary)
parent 3185e298
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 379 additions and 259 deletions
Makefile.in
View file @ afd48213
......@@ -194,11 +194,11 @@ clean::
# Whyml
########
PGMGENERATED = src/programs/pgm_parser.mli src/programs/pgm_parser.ml \
PGMGENERATED = src/programs/pgm_parser.mli src/programs/pgm_parser.ml \
src/programs/pgm_parser.output src/programs/pgm_lexer.ml
PGM_FILES = pgm_ttree pgm_ptree pgm_parser pgm_lexer pgm_effect pgm_typing \
pgm_itree pgm_wp pgm_main
PGM_FILES = pgm_ttree pgm_ptree pgm_parser pgm_lexer pgm_effect \
pgm_types pgm_typing pgm_itree pgm_wp pgm_main
PGMMODULES = $(addprefix src/programs/, $(PGM_FILES))
......@@ -517,6 +517,7 @@ test: bin/why.byte $(TOOLS)
testl: bin/whyml.byte
ocamlrun -bt bin/whyml.byte tests/test-pgm-jcf.mlw
ocamlrun -bt bin/whyml.byte -P alt-ergo tests/test-pgm-jcf.mlw
testl-type: bin/whyml.byte
ocamlrun -bt bin/whyml.byte --type-only tests/test-pgm-jcf.mlw
......
src/programs/pgm_itree.ml
View file @ afd48213
......@@ -31,7 +31,7 @@ type variant = Pgm_ttree.variant
type reference = Pgm_ttree.reference
type effect = Pgm_ttree.effect
type effect = Pgm_effect.t
type pre = Pgm_ttree.pre
......
src/programs/pgm_ttree.ml
View file @ afd48213
......@@ -105,26 +105,15 @@ type variant = Term.term * Term.lsymbol
type reference = Pgm_effect.reference
type effect = Pgm_effect.t
type pre = Pgm_types.pre
type pre = Term.fmla
type post = Pgm_types.post
type post_fmla = Term.vsymbol (* result *) * Term.fmla
type exn_post_fmla = Term.vsymbol (* result *) option * Term.fmla
type type_v = Pgm_types.type_v
type post = post_fmla * (Term.lsymbol * exn_post_fmla) list
type type_c = Pgm_types.type_c
type type_v =
| Tpure of Ty.ty
| Tarrow of binder list * type_c
and type_c =
{ c_result_type : type_v;
c_effect : effect;
c_pre : pre;
c_post : post; }
and binder = Term.vsymbol * type_v
type binder = Pgm_types.binder
type loop_annotation = {
loop_invariant : Term.fmla option;
......
src/programs/pgm_types.ml 0 → 100644
View file @ afd48213
open Why
open Ident
open Theory
open Term
open Ty
open Pgm_typing
type effect = Pgm_effect.t
type pre = Term.fmla
type post_fmla = Term.vsymbol (* result *) * Term.fmla
type exn_post_fmla = Term.vsymbol (* result *) option * Term.fmla
type post = post_fmla * (Term.lsymbol * exn_post_fmla) list
type type_v =
| Tpure of Ty.ty
| Tarrow of binder list * type_c
and type_c =
{ c_result_type : type_v;
c_effect : effect;
c_pre : pre;
c_post : post; }
and binder = Term.vsymbol * type_v
type env = {
uc : theory_uc;
globals : type_v Mls.t;
locals : type_v Mvs.t;
ts_arrow: tysymbol;
ts_label: tysymbol;
ts_ref: tysymbol;
ls_at : lsymbol;
ls_bang : lsymbol;
ls_old : lsymbol;
}
let empty_env uc = {
uc = uc; globals = Mls.empty; locals = Mvs.empty;
(* types *)
ts_arrow = ns_find_ts (get_namespace uc) ["arrow"];
ts_label = ns_find_ts (get_namespace uc) ["label"];
ts_ref = ns_find_ts (get_namespace uc) ["ref"];
(* functions *)
ls_at = ns_find_ls (get_namespace uc) ["at"];
ls_bang = ns_find_ls (get_namespace uc) ["prefix !"];
ls_old = ns_find_ls (get_namespace uc) ["old"];
}
let add_local x v env = { env with locals = Mvs.add x v env.locals }
let add_global x v env = { env with globals = Mls.add x v env.globals }
let add_decl d env = { env with uc = add_decl env.uc d }
let ts_arrow uc = ns_find_ts (get_namespace uc) ["arrow"]
let currying uc tyl ty =
let make_arrow_type ty1 ty2 = Ty.ty_app (ts_arrow uc) [ty1; ty2] in
List.fold_right make_arrow_type tyl ty
let rec purify uc = function
| Tpure ty ->
ty
| Tarrow (bl, c) ->
currying uc (List.map (fun (v,_) -> v.vs_ty) bl)
(purify uc c.c_result_type)
let post_map f ((v, q), ql) =
(v, f q), List.map (fun (e,(v,q)) -> e, (v, f q)) ql
let v_result ty = create_vsymbol (id_fresh "result") ty
let type_c_of_type_v env = function
| Tarrow ([], c) ->
c
| v ->
let ty = purify env.uc v in
{ c_result_type = v;
c_effect = Pgm_effect.empty;
c_pre = f_true;
c_post = (v_result ty, f_true), []; }
let subst1 vs1 vs2 = Mvs.add vs1 (t_var vs2) Mvs.empty
let rec subst_type_c s c =
{ c_result_type = subst_type_v s c.c_result_type;
c_effect = c.c_effect;
c_pre = f_subst s c.c_pre;
c_post = post_map (f_subst s) c.c_post; }
and subst_type_v s = function
| Tpure _ as v -> v
| Tarrow (bl, c) -> Tarrow (bl, subst_type_c s c)
let apply_type_v env v vs = match v with
| Tarrow ((x, _) :: bl, c) ->
let c = type_c_of_type_v env (Tarrow (bl, c)) in
subst_type_c (subst1 x vs) c
| Tarrow ([], _) | Tpure _ ->
assert false
(* pretty-printers *)
open Pp
open Format
open Pretty
let print_post fmt ((_,q), el) =
let print_exn_post fmt (l,(_,q)) =
fprintf fmt "| %a -> {%a}" print_ls l print_fmla q
in
fprintf fmt "{%a} %a" print_fmla q (print_list space print_exn_post) el
let rec print_type_v fmt = function
| Tpure ty ->
print_ty fmt ty
| Tarrow (bl, c) ->
fprintf fmt "@[<hov 2>%a ->@ %a@]"
(print_list arrow print_binder) bl print_type_c c
and print_type_c fmt c =
fprintf fmt "@[{%a}@ %a%a@ %a@]" print_fmla c.c_pre
print_type_v c.c_result_type Pgm_effect.print c.c_effect
print_post c.c_post
and print_binder fmt (x, v) =
fprintf fmt "(%a:%a)" print_vs x print_type_v v
src/programs/pgm_types.mli 0 → 100644
View file @ afd48213
open Why
open Ty
open Theory
open Term
open Decl
(* types *)
type effect = Pgm_effect.t
type pre = Term.fmla
type post_fmla = Term.vsymbol (* result *) * Term.fmla
type exn_post_fmla = Term.vsymbol (* result *) option * Term.fmla
type post = post_fmla * (Term.lsymbol * exn_post_fmla) list
type type_v =
| Tpure of Ty.ty
| Tarrow of binder list * type_c
and type_c =
{ c_result_type : type_v;
c_effect : effect;
c_pre : pre;
c_post : post; }
and binder = Term.vsymbol * type_v
type env = private {
uc : theory_uc;
globals : type_v Mls.t;
locals : type_v Mvs.t;
(* predefined symbols *)
ts_arrow: tysymbol;
ts_label: tysymbol;
ts_ref : tysymbol;
ls_at : lsymbol;
ls_bang : lsymbol;
ls_old : lsymbol;
}
val purify : theory_uc -> type_v -> ty
val apply_type_v : env -> type_v -> vsymbol -> type_c
val empty_env : theory_uc -> env
val add_local : vsymbol -> type_v -> env -> env
val add_global : lsymbol -> type_v -> env -> env
val add_decl : decl -> env -> env
val v_result : ty -> vsymbol
val post_map : (fmla -> fmla) -> post -> post
(* pretty-printers *)
val print_type_v : Format.formatter -> type_v -> unit
src/programs/pgm_typing.ml
View file @ afd48213
This diff is collapsed.
src/programs/pgm_typing.mli
View file @ afd48213
......@@ -30,6 +30,4 @@ val report : Format.formatter -> error -> unit
val file : Env.env -> theory_uc -> Pgm_ptree.file -> theory_uc * Pgm_ttree.file
val print_type_v : Format.formatter -> Pgm_ttree.type_v -> unit
val purify : theory_uc -> Pgm_ttree.type_v -> Ty.ty
src/programs/pgm_wp.ml
View file @ afd48213
......@@ -28,27 +28,10 @@ open Theory
open Pgm_ttree
open Pgm_itree
open Pgm_typing
open Pgm_types
module E = Pgm_effect
type env = {
uc : theory_uc;
globals : type_v Mls.t;
locals : type_v Mvs.t;
}
let empty_env uc = { uc = uc; globals = Mls.empty; locals = Mvs.empty }
let add_local x v env = { env with locals = Mvs.add x v env.locals }
let add_global x v env = { env with globals = Mls.add x v env.globals }
let ts_arrow uc = ns_find_ts (get_namespace uc) ["arrow"]
let ts_ref env = ns_find_ts (get_namespace env.uc) ["ref"]
let ts_label env = ns_find_ts (get_namespace env.uc) ["label"]
let ls_old env = ns_find_ls (get_namespace env.uc) ["old"]
let ls_at env = ns_find_ls (get_namespace env.uc) ["at"]
let ls_bang env = ns_find_ls (get_namespace env.uc) ["prefix !"]
(* phase 3: translation to intermediate trees and effect inference **********)
let reference_of_term t = match t.t_node with
......@@ -57,7 +40,7 @@ let reference_of_term t = match t.t_node with
| _ -> assert false
let rec term_effect env ef t = match t.t_node with
| Tapp (ls, [t]) when ls_equal ls (ls_bang env) ->
| Tapp (ls, [t]) when ls_equal ls env.ls_bang ->
let r = reference_of_term t in
E.add_read r ef
| _ ->
......@@ -73,40 +56,6 @@ let post_effect env ef ((_,q),ql) =
let add_binder env (x, v) = add_local x v env
let add_binders = List.fold_left add_binder
let v_result ty = create_vsymbol (id_fresh "result") ty
let post_map f ((v, q), ql) =
(v, f q), List.map (fun (e,(v,q)) -> e, (v, f q)) ql
let type_c_of_type_v env = function
| Tarrow ([], c) ->
c
| v ->
let ty = purify env.uc v in
{ c_result_type = v;
c_effect = E.empty;
c_pre = f_true;
c_post = (v_result ty, f_true), []; }
let subst1 vs1 vs2 = Mvs.add vs1 (t_var vs2) Mvs.empty
let rec subst_type_c s c =
{ c_result_type = subst_type_v s c.c_result_type;
c_effect = c.c_effect;
c_pre = f_subst s c.c_pre;
c_post = post_map (f_subst s) c.c_post; }
and subst_type_v s = function
| Tpure _ as v -> v
| Tarrow (bl, c) -> Tarrow (bl, subst_type_c s c)
let apply_type_v env v vs = match v with
| Tarrow ((x, _) :: bl, c) ->
let c = type_c_of_type_v env (Tarrow (bl, c)) in
subst_type_c (subst1 x vs) c
| Tarrow ([], _) | Tpure _ ->
assert false
let rec expr env e =
let ty = e.Pgm_ttree.expr_type in
let loc = e.Pgm_ttree.expr_loc in
......@@ -136,7 +85,7 @@ and expr_desc env _loc ty = function
Efun (bl, t), Tarrow (bl, c), E.empty
| Pgm_ttree.Elet (v, e1, e2) ->
let e1 = expr env e1 in
let env = { env with locals = Mvs.add v e1.expr_type_v env.locals } in
let env = add_local v e1.expr_type_v env in
let e2 = expr env e2 in
let ef = E.union e1.expr_effect e2.expr_effect in
Elet (v, e1, e2), e2.expr_type_v, ef
......@@ -187,7 +136,7 @@ let wp_forall = f_forall_simp
(* utility functions for building WPs *)
let fresh_label env =
let ty = ty_app (ts_label env) [] in
let ty = ty_app env.ts_label [] in
create_vsymbol (id_fresh "label") ty
let wp_binder (x, tv) f = match tv with
......@@ -201,9 +150,9 @@ let rec old_label env lab f =
f_map (old_label_term env lab) (old_label env lab) f
and old_label_term env lab t = match t.t_node with
| Tapp (ls, [t]) when ls_equal ls (ls_old env) ->
| Tapp (ls, [t]) when ls_equal ls env.ls_old ->
let t = old_label_term env lab t in (* NECESSARY? *)
t_app (ls_at env) [t; t_var lab] t.t_ty
t_app env.ls_at [t; t_var lab] t.t_ty
| _ ->
t_map (old_label_term env lab) (old_label env lab) t
......@@ -213,13 +162,13 @@ let rec erase_label env lab f =
and erase_label_term env lab t = match t.t_node with
| Tapp (ls, [t; {t_node = Tvar l}])
when ls_equal ls (ls_at env) && vs_equal l lab ->
when ls_equal ls env.ls_at && vs_equal l lab ->
erase_label_term env lab t
| _ ->
t_map (erase_label_term env lab) (erase_label env lab) t
let unref_ty env ty = match ty.ty_node with
| Tyapp (ts, [ty]) when ts_equal ts (ts_ref env) -> ty
| Tyapp (ts, [ty]) when ts_equal ts env.ts_ref -> ty
| _ -> assert false
(* replace !r by v everywhere in formula f *)
......@@ -227,12 +176,12 @@ let rec unref env r v f =
f_map (unref_term env r v) (unref env r v) f
and unref_term env r v t = match t.t_node with
| Tapp (ls, [t]) when ls_equal ls (ls_bang env) ->
| Tapp (ls, [t]) when ls_equal ls env.ls_bang ->
let rt = reference_of_term t in
if E.ref_equal rt r then t_var v else t
| Tapp (ls, _) when ls_equal ls (ls_old env) ->
| Tapp (ls, _) when ls_equal ls env.ls_old ->
assert false
| Tapp (ls, _) when ls_equal ls (ls_at env) -> (* do not recurse in at(...) *)
| Tapp (ls, _) when ls_equal ls env.ls_at -> (* do not recurse in at(...) *)
t
| _ ->
t_map (unref_term env r v) (unref env r v) t
......@@ -330,7 +279,7 @@ let wp_recfun _env _l _def = f_true (* TODO *)
let add_wp_decl l f env =
let pr = create_prsymbol (id_fresh ("WP_" ^ l.ls_name.id_string)) in
let d = create_prop_decl Pgoal pr f in
{ env with uc = add_decl env.uc d }
add_decl d env
let decl env = function
| Pgm_ttree.Dlet (ls, e) ->
......
tests/test-pgm-jcf.mlw
View file @ afd48213
......@@ -16,13 +16,9 @@ parameter write : v:int -> {} unit writes r { !r = v }
let ff () =
{ true }
1+2
{ result = 3 }
write 3
{ !r = 3 }
let gg () =
{ true }
3-1
{ result = 2 }
(*
......
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