Skip to content

GitLab

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

programs: one module = three theories

parent f1b63493
Hide whitespace changes
Inline Side-by-side
Showing with 234 additions and 244 deletions
modules/stdlib.mlw
View file @ 9f981b82
......@@ -7,9 +7,9 @@ module Ref
parameter ref : v:'a -> {} ref 'a { result=v }
parameter (!) : r:ref 'a -> {} 'a reads r.contents { result=r }
parameter (!) : r:ref 'a -> {} 'a reads r { result=r }
parameter (:=) : r:ref 'a -> v:'a -> {} unit writes r.contents { r=v }
parameter (:=) : r:ref 'a -> v:'a -> {} unit writes r { r=v }
end
......@@ -18,40 +18,14 @@ module Refint
use export int.Int
use export module Ref
parameter incr : r:ref int -> {} unit writes r.contents { r = old r + 1 }
parameter incr : r:ref int -> {} unit writes r { r = old r + 1 }
parameter decr : r:ref int -> {} unit writes r.contents { r = old r - 1 }
parameter decr : r:ref int -> {} unit writes r { r = old r - 1 }
end
(* Arrays *)
module Array
use import int.Int
use import array.ArrayLength as A
use import module Ref
type map 'a = t int 'a
type array 'a model ref (map 'a)
logic length (a : array 'a) : int = A.length a
logic ([]) (a : array 'a) (i : int) : 'a = get a i
parameter ([]) : a:array 'a -> i:int ->
{ 0 <= i < length a } 'a reads a.contents { result = a[i] }
parameter set : a:array 'a -> i:int -> v:'a ->
{ 0 <= i < length a } unit writes a.contents { a = (old a)[i <- v] }
parameter length : a:array 'a -> {} int { result = length a }
parameter make : n:int -> v:'a ->
{}
array 'a
{ length result = n and forall i:int. 0 <= i < n -> result[i] = v}
end
(***
module Array
use import int.Int
......@@ -60,20 +34,20 @@ module Array
type array 'a model {| length : int; mutable elts : map 'a |}
logic ([]) (a : array 'a) (i : int) : 'a = get a.elts i
logic ([]) (a: array 'a) (i :int) : 'a = get a.elts i
parameter ([]) : a:array 'a -> i:int ->
{ 0 <= i < a.length } 'a reads a.elts { result = a[i] }
{ 0 <= i < length a } 'a reads a { result = a[i] }
parameter set : a:array 'a -> i:int -> v:'a ->
{ 0 <= i < a.length } unit writes a.elts { a.elts = (old a.elts)[i <- v] }
parameter ([<-]) : a:array 'a -> i:int -> v:'a ->
{ 0 <= i < length a } unit writes a { a.elts = (old a.elts)[i <- v] }
parameter length : a:array 'a -> {} int { result = a.length }
parameter make : n:int -> v:'a ->
{}
array 'a
{ result.length = n and forall i:int. 0 <= i < n -> result[i] = v}
{ length result = n and forall i:int. 0 <= i < n -> result[i] = v}
parameter append : a1:array 'a -> a2:array 'a ->
{}
......@@ -97,10 +71,10 @@ module Array
parameter fill : a:array 'a -> ofs:int -> len:int -> v:'a ->
{ 0 <= ofs and ofs + len <= length a }
unit
writes a.elts
{ (forall i:int.
(0 <= i < ofs or ofs + len <= i < length a) -> a[i] = (old a)[i])
and
writes a
{ (forall i:int.
(0 <= i < ofs or ofs + len <= i < length a) -> a[i] = (old a)[i])
and
(forall i:int.
ofs <= i < ofs + len -> a[i] = v) }
......@@ -109,10 +83,10 @@ module Array
{ 0 <= ofs1 and ofs1 + len <= length a1 and
0 <= ofs2 and ofs2 + len <= length a2 }
unit
writes a2.elts
{ (forall i:int.
(0 <= i < ofs2 or ofs2 + len <= i < length a2) -> a2[i] = (old a2)[i])
and
writes a2
{ (forall i:int.
(0 <= i < ofs2 or ofs2 + len <= i < length a2) -> a2[i] = (old a2)[i])
and
(forall i:int.
ofs2 <= i < ofs2 + len -> a2[i] = a1[ofs1 + i - ofs2]) }
......@@ -132,7 +106,7 @@ module TestArray
let test_append () =
let a1 = make 17 2 in
assert { a1[3] = 2 };
set a1 3 4;
a1[3 <- 4];
assert { a1[3] = 4 };
let a2 = make 25 3 in
assert { a2[0] = 3 }; (* needed to prove a[17]=3 below *)
......@@ -158,7 +132,6 @@ module TestArray
assert { a2[24] = False }
end
***)
(*
Local Variables:
......
src/programs/pgm_module.ml
View file @ 9f981b82
......@@ -10,16 +10,12 @@ open Pgm_types.T
open Pgm_ttree
type namespace = {
ns_pr : psymbol Mnm.t; (* program symbols *)
ns_ex : esymbol Mnm.t; (* exceptions*)
ns_mt : mtsymbol Mnm.t; (* types *)
ns_ns : namespace Mnm.t; (* inner namespaces *)
}
let empty_ns = {
ns_pr = Mnm.empty;
ns_ex = Mnm.empty;
ns_mt = Mnm.empty;
ns_ns = Mnm.empty;
}
......@@ -35,9 +31,7 @@ let ns_union eq chk =
let rec merge_ns chk ns1 ns2 =
let fusion _ ns1 ns2 = Some (merge_ns chk ns1 ns2) in
{ ns_pr = ns_union ps_equal chk ns1.ns_pr ns2.ns_pr;
ns_ex = ns_union ls_equal chk ns1.ns_ex ns2.ns_ex;
ns_mt = ns_union mt_equal chk ns1.ns_mt ns2.ns_mt;
{ ns_ex = ns_union ls_equal chk ns1.ns_ex ns2.ns_ex;
ns_ns = Mnm.union fusion ns1.ns_ns ns2.ns_ns; }
let nm_add chk x ns m = Mnm.change x (function
......@@ -48,13 +42,10 @@ let ns_add eq chk x v m = Mnm.change x (function
| None -> Some v
| Some vo -> Some (ns_replace eq chk x vo v)) m
let pr_add = ns_add ps_equal
let ex_add = ns_add ls_equal
let mt_add = ns_add mt_equal
let add_pr chk x ts ns = { ns with ns_pr = pr_add chk x ts ns.ns_pr }
let add_ex chk x ls ns = { ns with ns_ex = ex_add chk x ls ns.ns_ex }
let add_mt chk x mt ns = { ns with ns_mt = mt_add chk x mt ns.ns_mt }
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
......@@ -62,9 +53,7 @@ let rec ns_find get_map ns = function
| [a] -> Mnm.find a (get_map ns)
| a::l -> ns_find get_map (Mnm.find a ns.ns_ns) l
let ns_find_pr = ns_find (fun ns -> ns.ns_pr)
let ns_find_ex = ns_find (fun ns -> ns.ns_ex)
let ns_find_mt = ns_find (fun ns -> ns.ns_mt)
let ns_find_ns = ns_find (fun ns -> ns.ns_ns)
(* modules under construction *)
......@@ -127,42 +116,29 @@ let add_symbol add id v uc =
uc_export = add true id.id_string v e0 :: ste }
| _ -> assert false
let add_psymbol ps uc =
add_symbol add_pr (ps_name ps) ps uc
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_pure_decl d uc =
let th = Typing.with_tuples Theory.add_decl uc.uc_pure d in
{ uc with uc_pure = th }
let add_impure_decl d uc =
let th = Typing.with_tuples Theory.add_decl uc.uc_impure d in
{ uc with uc_impure = th }
let add_effect_decl d uc =
let th = Typing.with_tuples Theory.add_decl uc.uc_effect d in
{ uc with uc_effect = th }
let add_mtsymbol mt uc =
(***
(* added in the logic as an abstract type *)
let uc =
let d = Decl.create_ty_decl [mt.mt_abstr, Decl.Tabstract] in
add_logic_decl d uc
in
***)
add_symbol add_mt mt.mt_impure.Ty.ts_name mt uc
(***
let add_rtsymbol rt uc =
(* added in the logic as an abstract type *)
let uc =
let d = Decl.create_ty_decl [rt.rt_abstr, Decl.Tabstract] in
add_logic_decl d uc
in
add_symbol add_rt rt.rt_name rt uc
***)
let add_pure_decl d uc =
let th = Typing.with_tuples Theory.add_decl 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)
......@@ -230,12 +206,12 @@ let use_export_theory uc th =
uc_pure = Theory.use_export uc.uc_pure th; }
in
(* all type symbols from th are added as (pure) mtsymbols *)
let add _ ts uc =
add_mtsymbol
(create_mtsymbol ~impure:ts ~effect:ts ~pure:ts ~singleton:false) uc
let add_ts _ ts =
ignore
(create_mtsymbol ~impure:ts ~effect:ts ~pure:ts ~singleton:false)
in
let rec add_ns ns uc =
let uc = Mnm.fold add ns.Theory.ns_ts uc in
Mnm.iter add_ts ns.Theory.ns_ts;
Mnm.fold (fun _ -> add_ns) ns.Theory.ns_ns uc
in
add_ns th.th_export uc
......
src/programs/pgm_module.mli
View file @ 9f981b82
......@@ -7,15 +7,11 @@ open Pgm_types
open Pgm_types.T
type namespace = private {
ns_pr : psymbol Mnm.t; (* program symbols *)
ns_ex : esymbol Mnm.t; (* exception symbols *)
ns_mt : mtsymbol Mnm.t; (* types *)
ns_ns : namespace Mnm.t; (* inner namespaces *)
}
val ns_find_pr : namespace -> string list -> psymbol
val ns_find_ex : namespace -> string list -> esymbol
val ns_find_mt : namespace -> string list -> mtsymbol
val ns_find_ns : namespace -> string list -> namespace
(** a module under construction *)
......@@ -51,10 +47,12 @@ exception ClashSymbol of string
val add_psymbol : psymbol -> uc -> uc
val add_esymbol : esymbol -> uc -> uc
val add_mtsymbol : mtsymbol -> uc -> uc
(* val add_mtsymbol : mtsymbol -> uc -> uc *)
val add_decl : Pgm_ttree.decl -> uc -> uc
val add_pure_decl : Decl.decl -> uc -> uc
val add_impure_decl : Decl.decl -> uc -> uc
val add_effect_decl : Decl.decl -> uc -> uc
val add_pure_decl : Decl.decl -> uc -> uc
val add_impure_typedecl : Env.env -> Ptree.type_decl list -> uc -> uc
val add_effect_typedecl : Env.env -> Ptree.type_decl list -> uc -> uc
......
src/programs/pgm_pretty.ml
View file @ 9f981b82
......@@ -16,10 +16,12 @@ let rec print_expr fmt e = match e.expr_desc with
Pretty.print_ty t.t_ty
| Elocal v ->
fprintf fmt "%a" print_pv v
| Eglobal (PSvar v) ->
| Eglobal { ps_kind = PSvar v } ->
fprintf fmt "<global var %a>" print_pv v
| Eglobal (PSfun f) ->
fprintf fmt "<global %a>" print_ls f.p_ls
| Eglobal { ps_kind = PSfun tv } ->
fprintf fmt "<global %a>" print_type_v tv
| Eglobal { ps_kind = PSlogic } ->
assert false
| Efun (bl, t) ->
fprintf fmt "@[<hov 2>fun %a ->@ %a@]"
(print_list space print_pv) bl print_triple t
......
src/programs/pgm_ttree.ml
View file @ 9f981b82
......@@ -279,9 +279,9 @@ and recfun = pvsymbol * pvsymbol list * rec_variant option * triple
and triple = pre * expr * post
type decl =
| Dlet of T.psymbol_fun * expr
| Dletrec of (T.psymbol_fun * recfun) list
| Dparam of T.psymbol * type_v
| Dlet of T.psymbol * expr
| Dletrec of (T.psymbol * recfun) list
| Dparam of T.psymbol
type file = decl list
......
src/programs/pgm_types.ml
View file @ 9f981b82
......@@ -162,18 +162,25 @@ module rec T : sig
(* program symbols *)
type psymbol_fun = private {
p_name : ident;
p_tv : type_v;
p_ty : ty; (* as a logic type, for typing purposes only *)
p_ls : lsymbol; (* for use in the logic *)
type psymbol_kind =
| PSvar of pvsymbol
| PSfun of type_v
| PSlogic
type psymbol = {
ps_impure : lsymbol;
ps_effect : lsymbol;
ps_pure : lsymbol;
ps_kind : psymbol_kind;
}
type psymbol =
| PSvar of pvsymbol
| PSfun of psymbol_fun
val create_psymbol_fun : preid -> type_v -> psymbol_fun
val create_psymbol:
impure:lsymbol -> effect:lsymbol -> pure:lsymbol -> kind:psymbol_kind ->
psymbol
val create_psymbol_fun: preid -> type_v -> psymbol
val create_psymbol_var: pvsymbol -> psymbol
val get_psymbol: lsymbol -> psymbol
val ps_name : psymbol -> ident
val ps_equal : psymbol -> psymbol -> bool
......@@ -183,8 +190,7 @@ module rec T : sig
val purify : ty -> ty
val effectify : ty -> ty
val purify_type_v : ?logic:bool -> type_v -> ty
(** when [logic] is [true], mutable types are turned into their models *)
val trans_type_v : ?effect:bool -> ?pure:bool -> type_v -> ty
(* operations on program types *)
......@@ -258,52 +264,87 @@ end = struct
let purify = purify
let effectify = effectify
let rec uncurry_type ?(logic=false) = function
let rec uncurry_type ?(effect=false) ?(pure=false) = function
| Tpure ty ->
[], if logic then purify ty else effectify ty
[], if pure then purify ty else if effect then effectify ty else ty
| Tarrow (bl, c) ->
let tyl1 =
List.map
(fun v -> if logic then v.pv_pure.vs_ty else v.pv_effect.vs_ty)
(fun v ->
if pure then v.pv_pure.vs_ty
else if effect then v.pv_effect.vs_ty
else trans_type_v ~effect ~pure v.pv_tv)
bl
in
let tyl2, ty = uncurry_type ~logic c.c_result_type in
let tyl2, ty = uncurry_type ~effect ~pure c.c_result_type in
tyl1 @ tyl2, ty (* TODO: improve efficiency? *)
let purify_type_v ?(logic=false) v =
let tyl, ty = uncurry_type ~logic v in
and trans_type_v ?(effect=false) ?(pure=false) v =
if effect && pure then invalid_arg "trans_type_v";
let tyl, ty = uncurry_type ~effect ~pure v in
make_arrow_type tyl ty
(* symbols *)
type psymbol_fun = {
p_name : ident;
p_tv : type_v;
p_ty : ty; (* program type, as a logic type *)
p_ls : lsymbol; (* for use in the logic *)
type psymbol_kind =
| PSvar of pvsymbol
| PSfun of type_v
| PSlogic
type psymbol = {
ps_impure : lsymbol;
ps_effect : lsymbol;
ps_pure : lsymbol;
ps_kind : psymbol_kind;
}
type psymbol =
| PSvar of pvsymbol
| PSfun of psymbol_fun
let create_psymbol_fun name v =
{
p_name = id_register name;
p_tv = v;
p_ty = purify_type_v v;
p_ls =
let tyl, ty = uncurry_type ~logic:true v in
create_lsymbol name tyl (Some ty); }
let ps_name = function
| PSvar v -> v.pv_name
| PSfun f -> f.p_name
let psymbols = Hls.create 17
let create_psymbol ~impure ~effect ~pure ~kind =
let ps = {
ps_impure = impure;
ps_effect = effect;
ps_pure = pure;
ps_kind = kind;
}
in
Hls.add psymbols impure ps;
Hls.add psymbols effect ps;
Hls.add psymbols pure ps;
ps
let create_psymbol_fun id v =
let create ?effect ?pure v =
let tyl, ty = uncurry_type ?effect ?pure v in
create_lsymbol id tyl (Some ty)
in
let impure = create v in
let effect = create ~effect:true v in
let pure = create ~pure: true v in
create_psymbol ~impure ~effect ~pure ~kind:(PSfun v)
let create_psymbol_var pv =
let name = pv.pv_name in
let tv = trans_type_v pv.pv_tv in
let impure = create_lsymbol (id_clone name) [] (Some tv) in
let effect = create_lsymbol (id_clone name) [] (Some pv.pv_effect.vs_ty) in
let pure = create_lsymbol (id_clone name) [] (Some pv.pv_pure.vs_ty) in
create_psymbol ~impure ~effect ~pure ~kind:(PSvar pv)
let get_psymbol ls =
try
Hls.find psymbols ls
with Not_found ->
(* Format.eprintf "ls = %a@." Pretty.print_ls ls; *)
let ps = { ps_impure = ls; ps_effect = ls;
ps_pure = ls; ps_kind = PSlogic }
in
Hls.add psymbols ls ps;
ps
let ps_name ps = ps.ps_impure.ls_name
let ps_equal ps1 ps2 = match ps1, ps2 with
| PSvar v1, PSvar v2 -> equal_pvsymbol v1 v2
| PSfun s1, PSfun s2 -> s1 == s2
| _ -> false
let ps_equal ps1 ps2 = ls_equal ps1.ps_impure ps2.ps_impure
let rec subst_var ts s vs =
let ty' = ty_inst ts vs.vs_ty in
......@@ -378,7 +419,7 @@ end = struct
| Tarrow ([], c) ->
c
| v ->
let ty = purify_type_v v in
let ty = trans_type_v v in
{ c_result_type = v;
c_effect = E.empty;
c_pre = f_true;
......
src/programs/pgm_types.mli
View file @ 9f981b82
......@@ -84,18 +84,25 @@ module rec T : sig
(* program symbols *)
type psymbol_fun = private {
p_name : ident;
p_tv : type_v;
p_ty : ty; (* as a logic type, for typing purposes only *)
p_ls : lsymbol; (* for use in the logic *)
type psymbol_kind =
| PSvar of pvsymbol
| PSfun of type_v
| PSlogic
type psymbol = {
ps_impure : lsymbol;
ps_effect : lsymbol;
ps_pure : lsymbol;
ps_kind : psymbol_kind;
}
type psymbol =
| PSvar of pvsymbol
| PSfun of psymbol_fun
val create_psymbol:
impure:lsymbol -> effect:lsymbol -> pure:lsymbol -> kind:psymbol_kind ->
psymbol
val create_psymbol_fun: preid -> type_v -> psymbol
val create_psymbol_var: pvsymbol -> psymbol
val create_psymbol_fun : preid -> type_v -> psymbol_fun
val get_psymbol: lsymbol -> psymbol
val ps_name : psymbol -> ident
val ps_equal : psymbol -> psymbol -> bool
......@@ -105,8 +112,7 @@ module rec T : sig
val purify : ty -> ty
val effectify : ty -> ty
val purify_type_v : ?logic:bool -> type_v -> ty
(** when [logic] is [true], mutable types are turned into their models *)
val trans_type_v : ?effect:bool -> ?pure:bool -> type_v -> ty
(* operations on program types *)
......
src/programs/pgm_typing.ml
View file @ 9f981b82
......@@ -200,14 +200,17 @@ and specialize_binder ~loc htv v =
let v = specialize_type_v ~loc htv v.pv_tv in
id, dpurify_type_v v, v
let specialize_global loc x uc =
region_vars := Htv.create 17 :: !region_vars;
let p = ns_find_pr (namespace uc) x in
match p with
| PSvar v ->
p, specialize_type_v ~loc ~policy:Region_glob (Htv.create 17) v.pv_tv
| PSfun f ->
p, specialize_type_v ~loc (Htv.create 17) f.p_tv
(* let specialize_global loc x uc = *)
(* region_vars := Htv.create 17 :: !region_vars; *)
(* let ls = ns_find_ls (get_namespace (impure_uc uc)) x in *)
(* let ps = get_psymbol ls in *)
(* match ps.ps_kind with *)
(* | PSvar v -> *)
(* ps, specialize_type_v ~loc ~policy:Region_glob (Htv.create 17) v.pv_tv *)
(* | PSfun tv -> *)
(* ps, specialize_type_v ~loc (Htv.create 17) tv *)
(* | PSlogic -> *)
(* ps, *)
let dot fmt () = pp_print_string fmt "."
let print_qualids = print_list dot pp_print_string
......@@ -417,19 +420,30 @@ and dexpr_desc ~ghost env loc = function
let tyv = Mstr.find x env.locals in
DElocal (x, tyv), tyv
| Ptree.Eident p ->
begin try
(* global variable *)
let x = Typing.string_list_of_qualid [] p in
let s, tyv = specialize_global loc x env.uc in
let dty = dpurify_type_v tyv in
DEglobal (s, tyv), dty
with Not_found ->
let s,tyl,ty = Typing.specialize_lsymbol p (pure_uc env.uc) in
let ty = match ty with
| Some ty -> ty
| None -> dty_bool env.uc
in
DElogic s, dcurrying tyl ty
(* global variable *)
region_vars := Htv.create 17 :: !region_vars;
let x = Typing.string_list_of_qualid [] p in
let ls =
try ns_find_ls (get_namespace (impure_uc env.uc)) x
with Not_found -> errorm ~loc "unbound symbol %a" print_qualid p
in
let ps = get_psymbol ls in
begin match ps.ps_kind with
| PSvar v ->
let tyv =
specialize_type_v ~loc ~policy:Region_glob (Htv.create 17) v.pv_tv
in
DEglobal (ps, tyv), dpurify_type_v tyv
| PSfun tv ->
let tyv = specialize_type_v ~loc (Htv.create 17) tv in
DEglobal (ps, tyv), dpurify_type_v tyv
| PSlogic ->
let tyl, ty = Denv.specialize_lsymbol ~loc ps.ps_pure in
let ty = match ty with
| Some ty -> ty
| None -> dty_bool env.uc
in
DElogic ps.ps_pure, dcurrying tyl ty
end
| Ptree.Elazy (op, e1, e2) ->
let e1 = dexpr ~ghost env e1 in
......@@ -938,7 +952,7 @@ let make_logic_app gl loc ty ls el =
make (t :: args) r
| ({ iexpr_desc = IElocal v }, _) :: r ->
make (t_var v.i_pure :: args) r
| ({ iexpr_desc = IEglobal (PSvar v, _) }, _) :: r ->
| ({ iexpr_desc = IEglobal ({ ps_kind = PSvar v }, _) }, _) :: r ->
make (t_var v.pv_pure :: args) r
| (e, _) :: r ->
let v = create_ivsymbol (id_user "x" loc) e.iexpr_type in
......@@ -959,9 +973,9 @@ let make_app _gl loc ty f el =
begin match e.iexpr_desc with
| IElocal v ->
make (fun f -> mk_iexpr loc tye (IEapply_var (k f, v))) r
| IEglobal (PSvar v, _) ->
| IEglobal ({ ps_kind = PSvar v }, _) ->
make (fun f -> mk_iexpr loc tye (IEapply_glob (k f, v))) r
| IEglobal (PSfun _, _) ->
| IEglobal ({ ps_kind = PSfun _ }, _) ->
errorm ~loc "higher-order programs not yet implemented"
| _ ->