From 0dc788321d41a1d0bd641c3c74d59c174ff130bf Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Mon, 30 May 2011 18:05:51 +0200 Subject: [PATCH] no more prelude theory for programs --- src/parser/denv.ml | 13 ++++++- src/parser/denv.mli | 2 +- src/parser/typing.ml | 29 +++++----------- src/parser/typing.mli | 2 -- src/programs/pgm_main.ml | 20 +++++------ src/programs/pgm_module.ml | 64 +++++++++++++++++++++++++--------- src/programs/pgm_module.mli | 22 +++++++++--- src/programs/pgm_typing.ml | 46 ++++++++++--------------- src/programs/pgm_typing.mli | 8 ++--- src/programs/pgm_wp.ml | 68 ++++++++++++++----------------------- tests/test-jcf.why | 1 + theories/programs.why | 19 ----------- 12 files changed, 147 insertions(+), 147 deletions(-) delete mode 100644 theories/programs.why diff --git a/src/parser/denv.ml b/src/parser/denv.ml index 0c9f14f34..90b923379 100644 --- a/src/parser/denv.ml +++ b/src/parser/denv.ml @@ -51,7 +51,18 @@ and type_var = { } let tyvar v = Tyvar v -let tyapp (s, tyl) = Tyapp (s, tyl) + +let rec type_inst s ty = match ty.ty_node with + | Ty.Tyvar n -> Mtv.find n s + | Ty.Tyapp (ts, tyl) -> Tyapp (ts, List.map (type_inst s) tyl) + +let tyapp ts tyl = match ts.ts_def with + | None -> + Tyapp (ts, tyl) + | Some ty -> + let add m v t = Mtv.add v t m in + let s = List.fold_left2 add Mtv.empty ts.ts_args tyl in + type_inst s ty type dty = dty_view diff --git a/src/parser/denv.mli b/src/parser/denv.mli index 5c145659f..cc0319b22 100644 --- a/src/parser/denv.mli +++ b/src/parser/denv.mli @@ -32,7 +32,7 @@ val create_ty_decl_var : ?loc:Ptree.loc -> user:bool -> tvsymbol -> type_var type dty val tyvar : type_var -> dty -val tyapp : tysymbol * dty list -> dty +val tyapp : tysymbol -> dty list -> dty type dty_view = | Tyvar of type_var diff --git a/src/parser/typing.ml b/src/parser/typing.ml index 91110f1f4..02451a3c4 100644 --- a/src/parser/typing.ml +++ b/src/parser/typing.ml @@ -198,10 +198,6 @@ let add_ind_decls = with_tuples ~reset:true add_ind_decl let add_prop_decl = with_tuples ~reset:true add_prop_decl -let rec type_inst s ty = match ty.ty_node with - | Ty.Tyvar n -> Mtv.find n s - | Ty.Tyapp (ts, tyl) -> tyapp (ts, List.map (type_inst s) tyl) - let rec dty uc env = function | PPTtyvar {id=x} -> tyvar (find_user_type_var x env) @@ -211,17 +207,10 @@ let rec dty uc env = function let np = List.length p in if np <> a then error ~loc (TypeArity (x, a, np)); let tyl = List.map (dty uc env) p in - begin match ts.ts_def with - | None -> - tyapp (ts, tyl) - | Some ty -> - let add m v t = Mtv.add v t m in - let s = List.fold_left2 add Mtv.empty ts.ts_args tyl in - type_inst s ty - end + tyapp ts tyl | PPTtuple tyl -> let ts = ts_tuple (List.length tyl) in - tyapp (ts, List.map (dty uc env) tyl) + tyapp ts (List.map (dty uc env) tyl) let find_ns find p ns = let loc = qloc p in @@ -407,7 +396,7 @@ and dpat_node loc uc env = function let s = fs_tuple n in let tyl = List.map (fun _ -> fresh_type_var loc) pl in let env, pl = dpat_args s.ls_name loc uc env tyl pl in - let ty = tyapp (ts_tuple n, tyl) in + let ty = tyapp (ts_tuple n) tyl in env, Papp (s, pl), ty | PPpas (p, x) -> let env, p = dpat uc env p in @@ -493,16 +482,16 @@ and dterm_node ~localize loc uc env = function let s = fs_tuple n in let tyl = List.map (fun _ -> fresh_type_var loc) tl in let tl = dtype_args s.ls_name loc uc env tyl tl in - let ty = tyapp (ts_tuple n, tyl) in + let ty = tyapp (ts_tuple n) tyl in Tapp (s, tl), ty | PPinfix (e1, x, e2) -> let s, tyl, ty = specialize_fsymbol (Qident x) uc in let tl = dtype_args s.ls_name loc uc env tyl [e1; e2] in Tapp (s, tl), ty | PPconst (ConstInt _ as c) -> - Tconst c, tyapp (Ty.ts_int, []) + Tconst c, tyapp Ty.ts_int [] | PPconst (ConstReal _ as c) -> - Tconst c, tyapp (Ty.ts_real, []) + Tconst c, tyapp Ty.ts_real [] | PPlet (x, e1, e2) -> let e1 = dterm ~localize uc env e1 in let ty = e1.dt_ty in @@ -574,7 +563,7 @@ and dterm_node ~localize loc uc env = function | TRterm t -> let id = { id = "fc"; id_lab = []; id_loc = loc } in let tyl,ty = List.fold_right (fun (_,uty) (tyl,ty) -> - let nty = tyapp (ts_func, [uty;ty]) in ty :: tyl, nty) + let nty = tyapp ts_func [uty;ty] in ty :: tyl, nty) uqu ([],t.dt_ty) in let h = { dt_node = Tvar id.id ; dt_ty = ty } in @@ -591,8 +580,8 @@ and dterm_node ~localize loc uc env = function | [] -> assert false in let tyl,ty = List.fold_right (fun (_,uty) (tyl,ty) -> - let nty = tyapp (ts_func, [uty;ty]) in ty :: tyl, nty) - uqu ([],tyapp (ts_pred, [uty])) + let nty = tyapp ts_func [uty;ty] in ty :: tyl, nty) + uqu ([], tyapp ts_pred [uty]) in let h = { dt_node = Tvar id.id ; dt_ty = ty } in let h = List.fold_left2 (fun h (uid,uty) ty -> diff --git a/src/parser/typing.mli b/src/parser/typing.mli index 627708ea8..374ef739f 100644 --- a/src/parser/typing.mli +++ b/src/parser/typing.mli @@ -59,8 +59,6 @@ val create_denv : unit -> denv val create_user_type_var : string -> Denv.type_var val find_user_type_var : string -> denv -> Denv.type_var -val type_inst : Denv.dty Ty.Mtv.t -> Ty.ty -> Denv.dty - val mem_var : string -> denv -> bool val find_var : string -> denv -> Denv.dty val add_var : string -> Denv.dty -> denv -> denv diff --git a/src/programs/pgm_main.ml b/src/programs/pgm_main.ml index 49d0132d3..14f1b2de8 100644 --- a/src/programs/pgm_main.ml +++ b/src/programs/pgm_main.ml @@ -39,10 +39,10 @@ let add_module ?(type_only=false) env penv (ltm, lmod) m = if Mnm.mem id.id lmod then raise (Loc.Located (loc, ClashModule id.id)); let wp = not type_only in let uc = create_module (Ident.id_user id.id loc) in - let prelude = Env.find_theory env ["programs"] "Prelude" in + let prelude = Env.find_theory env ["bool"] "Bool" in let uc = use_export_theory uc prelude in - let uc = - List.fold_left (Pgm_typing.decl ~wp env penv ltm lmod) uc m.mod_decl + let uc = + List.fold_left (Pgm_typing.decl ~wp env penv ltm lmod) uc m.mod_decl in let m = close_module uc in Mnm.add id.id m.m_pure ltm, @@ -57,17 +57,17 @@ let retrieve penv file c = else let type_only = Debug.test_flag Typing.debug_type_only in let env = Pgm_env.get_env penv in - List.fold_left (add_module ~type_only env penv) + List.fold_left (add_module ~type_only env penv) (Mnm.empty, Mnm.empty) ml let pgm_env_of_env = let h = Env.Wenv.create 17 in - fun env -> - try - Env.Wenv.find h env - with Not_found -> - let penv = Pgm_env.create env retrieve in - Env.Wenv.set h env penv; + fun env -> + try + Env.Wenv.find h env + with Not_found -> + let penv = Pgm_env.create env retrieve in + Env.Wenv.set h env penv; penv let read_channel env file c = diff --git a/src/programs/pgm_module.ml b/src/programs/pgm_module.ml index 39e22404a..266f29c28 100644 --- a/src/programs/pgm_module.ml +++ b/src/programs/pgm_module.ml @@ -20,6 +20,8 @@ open Why open Util open Ident +open Ty +open Decl open Theory open Term @@ -93,8 +95,8 @@ let pure_uc uc = uc.uc_pure let add_pervasives uc = (* type unit = () *) - let ts = - Ty.create_tysymbol + let ts = + Ty.create_tysymbol (id_fresh "unit") [] (Some (Ty.ty_app (Ty.ts_tuple 0) [])) in add_ty_decl uc [ts, Decl.Tabstract] @@ -162,15 +164,41 @@ let add_psymbol ps uc = let ls_Exit = create_lsymbol (id_fresh "%Exit") [] (Some ty_exn) -let create_module n = - let m = { +(* type unit = () *) +let ty_unit = ty_tuple [] +let ts_unit = create_tysymbol (id_fresh "unit") [] (Some ty_unit) + +(* logic ignore 'a : () *) + +let ts_label = create_tysymbol (id_fresh "label") [] None +let ty_label = ty_app ts_label [] + +let fs_at = + let ty = ty_var (create_tvsymbol (id_fresh "a")) in + create_lsymbol (id_fresh "at") [ty; ty_label] (Some ty) + +let fs_old = + let ty = ty_var (create_tvsymbol (id_fresh "a")) in + create_lsymbol (id_fresh "old") [ty] (Some ty) + +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, Tabstract] in + let uc = add_ty_decl uc [ts_label, Tabstract] in + let uc = add_logic_decl uc [fs_at, None] in + let uc = add_logic_decl uc [fs_old, None] in + close_theory uc + +let empty_module n = + let m = { uc_name = id_register n; uc_impure = Theory.create_theory n; uc_effect = Theory.create_theory n; uc_pure = Theory.create_theory n; uc_decls = []; uc_import = [empty_ns]; - uc_export = [empty_ns]; } + uc_export = [empty_ns]; } in (* pervasives *) let m = add_esymbol ls_Exit m in @@ -199,9 +227,9 @@ let close_module uc = match uc.uc_export with { 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; + m_impure = close_theory uc.uc_impure; + m_effect = close_theory uc.uc_effect; + m_pure = close_theory uc.uc_pure; } | _ -> raise CloseModule @@ -213,21 +241,21 @@ let use_export uc m = | 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_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 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 + let add_ts _ ts = + ignore (create_mtsymbol ~impure:ts ~effect:ts ~pure:ts ~singleton:false) in let rec add_ns ns uc = @@ -236,6 +264,10 @@ let use_export_theory uc th = in add_ns th.th_export uc +let create_module id = + let uc = empty_module id in + use_export_theory uc th_prelude + let add_impure_pdecl env ltm d uc = { uc with uc_impure = Typing.add_decl env ltm uc.uc_impure d } @@ -246,14 +278,14 @@ let add_pure_pdecl env ltm d uc = { uc with uc_pure = Typing.add_decl env ltm uc.uc_pure d; } let add_pdecl env ltm d uc = - { uc with + { uc with uc_impure = Typing.add_decl env ltm uc.uc_impure d; uc_effect = Typing.add_decl env ltm uc.uc_effect d; uc_pure = Typing.add_decl env ltm uc.uc_pure d; } (* -Local Variables: +Local Variables: compile-command: "unset LANG; make -C ../.. testl" -End: +End: *) diff --git a/src/programs/pgm_module.mli b/src/programs/pgm_module.mli index 1f54977c3..d97699443 100644 --- a/src/programs/pgm_module.mli +++ b/src/programs/pgm_module.mli @@ -19,6 +19,7 @@ open Why open Ident +open Ty open Term open Theory open Pgm_types @@ -72,17 +73,30 @@ 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_pdecl : +val add_impure_pdecl : Env.env -> Theory.theory Theory.Mnm.t -> Ptree.decl -> uc -> uc -val add_effect_pdecl : +val add_effect_pdecl : Env.env -> Theory.theory Theory.Mnm.t -> Ptree.decl -> uc -> uc -val add_pure_pdecl : +val add_pure_pdecl : Env.env -> Theory.theory Theory.Mnm.t -> Ptree.decl -> uc -> uc -val add_pdecl : +val add_pdecl : Env.env -> Theory.theory Theory.Mnm.t -> Ptree.decl -> uc -> uc (** add in impure, effect and pure *) +(** builtins *) + +val ts_label : tysymbol +val ty_label : ty + +val ts_unit : tysymbol +val ty_unit : ty + +val fs_old : lsymbol +val fs_at : lsymbol + +val th_prelude : theory + (** exceptions *) exception CloseModule diff --git a/src/programs/pgm_typing.ml b/src/programs/pgm_typing.ml index a9edc20a2..14455436a 100644 --- a/src/programs/pgm_typing.ml +++ b/src/programs/pgm_typing.ml @@ -80,18 +80,16 @@ let is_mutable_field ts i = (* phase 1: typing programs (using destructive type inference) **************) -let dty_app (ts, tyl) = assert (ts.ts_def = None); tyapp (ts, tyl) - let find_ts ~pure uc s = ns_find_ts (get_namespace (if pure then pure_uc uc else impure_uc uc)) [s] let find_ls ~pure uc s = ns_find_ls (get_namespace (if pure then pure_uc uc else impure_uc uc)) [s] (* TODO: improve efficiency *) -let dty_bool uc = dty_app (find_ts ~pure:true uc "bool", []) -let dty_int _uc = dty_app (Ty.ts_int, []) -let dty_unit _uc = dty_app (ts_tuple 0, []) -let dty_label uc = dty_app (find_ts ~pure:true uc "label_", []) +let dty_bool uc = tyapp (find_ts ~pure:true uc "bool") [] +let dty_int _uc = tyapp Ty.ts_int [] +let dty_unit _uc = tyapp (ts_tuple 0) [] +let dty_label _uc = tyapp ts_label [] (* note: local variables are simultaneously in locals (to type programs) and in denv (to type logic elements) *) @@ -111,7 +109,7 @@ let loc_of_id id = Util.of_option id.Ident.id_loc let loc_of_ls ls = ls.ls_name.Ident.id_loc let dcurrying tyl ty = - let make_arrow_type ty1 ty2 = dty_app (ts_arrow, [ty1; ty2]) in + let make_arrow_type ty1 ty2 = tyapp ts_arrow [ty1; ty2] in List.fold_right make_arrow_type tyl ty type region_policy = Region_var | Region_ret | Region_glob @@ -176,7 +174,7 @@ let rec specialize_ty ?(policy=Region_var) ~loc htv ty = match ty.ty_node with in let regions = List.map mk_region (Util.prefix n tl) in let tl = List.map (specialize_ty ~policy ~loc htv) (Util.chop n tl) in - tyapp (ts, regions @ tl) + tyapp ts (regions @ tl) let rec specialize_type_v ?(policy=Region_var) ~loc htv = function | Tpure ty -> @@ -245,7 +243,7 @@ let dexception uc qid = let sl = Typing.string_list_of_qualid [] qid in let loc = Typing.qloc qid in let _, _, ty as r = specialize_exception loc sl uc in - let ty_exn = dty_app (ts_exn, []) in + let ty_exn = tyapp ts_exn [] in if not (Denv.unify ty ty_exn) then errorm ~loc "@[this expression has type %a,@ but is expected to be an exception@]" @@ -291,17 +289,10 @@ let rec dtype ~user env = function print_qualid x (a - mt.mt_regions) np; let tyl = List.map (dtype ~user env) p in let tyl = create_regions ~user mt.mt_regions @ tyl in - begin match ts.ts_def with - | None -> - tyapp (ts, tyl) - | Some ty -> - let add m v t = Mtv.add v t m in - let s = List.fold_left2 add Mtv.empty ts.ts_args tyl in - Typing.type_inst s ty - end + tyapp ts tyl | PPTtuple tyl -> let ts = ts_tuple (List.length tyl) in - tyapp (ts, List.map (dtype ~user env) tyl) + tyapp ts (List.map (dtype ~user env) tyl) let rec dutype_v env = function | Ptree.Tpure pt -> @@ -389,9 +380,9 @@ let rec dexpr ~ghost env e = and dexpr_desc ~ghost env loc = function | Ptree.Econstant (ConstInt _ as c) -> - DEconstant c, dty_app (Ty.ts_int, []) + DEconstant c, tyapp Ty.ts_int [] | Ptree.Econstant (ConstReal _ as c) -> - DEconstant c, dty_app (Ty.ts_real, []) + DEconstant c, tyapp Ty.ts_real [] | Ptree.Eident (Qident {id=x}) when Mstr.mem x env.locals -> (* local variable *) let tyv = Mstr.find x env.locals in @@ -437,7 +428,7 @@ and dexpr_desc ~ghost env loc = function let ghost = ghost (* || is_ps_ghost e1 *) in let e2 = dexpr ~ghost env e2 in let ty2 = create_type_var loc and ty = create_type_var loc in - if not (Denv.unify e1.dexpr_type (dty_app (ts_arrow, [ty2; ty]))) then + if not (Denv.unify e1.dexpr_type (tyapp ts_arrow [ty2; ty])) then errorm ~loc:e1.dexpr_loc "this expression is not a function"; expected_type e2 ty2; DEapply (e1, e2), ty @@ -461,13 +452,13 @@ and dexpr_desc ~ghost env loc = function let n = List.length el in let s = Typing.fs_tuple n in let tyl = List.map (fun _ -> create_type_var loc) el in - let ty = dty_app (Typing.ts_tuple n, tyl) in + let ty = tyapp (Typing.ts_tuple n) tyl in let create d ty = { dexpr_desc = d; dexpr_type = ty; dexpr_loc = loc } in let apply e1 e2 ty2 = let e2 = dexpr ~ghost env e2 in assert (Denv.unify e2.dexpr_type ty2); let ty = create_type_var loc in - assert (Denv.unify e1.dexpr_type (dty_app (ts_arrow, [ty2; ty]))); + assert (Denv.unify e1.dexpr_type (tyapp ts_arrow [ty2; ty])); create (DEapply (e1, e2)) ty in let e = create (DElogic s) (dcurrying tyl ty) in @@ -484,7 +475,7 @@ and dexpr_desc ~ghost env loc = function let f = dexpr ~ghost env f in assert (Denv.unify f.dexpr_type tyf); let ty = create_type_var loc in - assert (Denv.unify d.dexpr_type (dty_app (ts_arrow, [tyf; ty]))); + assert (Denv.unify d.dexpr_type (tyapp ts_arrow [tyf; ty])); create (DEapply (d, f)) ty | None -> errorm ~loc "some record fields are missing" @@ -704,7 +695,7 @@ let rec dty_of_ty denv ty = match ty.ty_node with | Ty.Tyvar v -> Denv.tyvar (Typing.find_user_type_var v.tv_name.id_string denv) | Ty.Tyapp (ts, tyl) -> - Denv.tyapp (ts, List.map (dty_of_ty denv) tyl) + Denv.tyapp ts (List.map (dty_of_ty denv) tyl) let iadd_local env x ty = let v = create_ivsymbol x ty in @@ -1165,8 +1156,7 @@ and iexpr_desc gl env loc ty = function let f = ifmla env f in IEassert (k, f) | DElabel (s, e1) -> - let ty = Ty.ty_app (find_ts ~pure:true gl "label_") [] in - let env, v = iadd_local env (id_fresh s) ty in + let env, v = iadd_local env (id_fresh s) ty_label in IElabel (v.i_impure, iexpr gl env e1) | DEany c -> let c = iutype_c gl env c in @@ -1408,7 +1398,7 @@ let mk_false loc gl = mk_bool_constant loc gl (find_ls ~pure:true gl "False") let mk_true loc gl = mk_bool_constant loc gl (find_ls ~pure:true gl "True") (* check that variables occurring in 'old' and 'at' are not local variables *) -let check_at_fmla f = +let check_at_fmla _f = assert false (*TODO*) (* Saturation of postconditions: a postcondition must be set for diff --git a/src/programs/pgm_typing.mli b/src/programs/pgm_typing.mli index e2435cec1..5665ee0e9 100644 --- a/src/programs/pgm_typing.mli +++ b/src/programs/pgm_typing.mli @@ -22,8 +22,8 @@ open Util val debug : Debug.flag -val decl : - wp:bool -> Env.env -> Pgm_env.t -> - Theory.theory Theory.Mnm.t -> - Pgm_module.t Theory.Mnm.t -> +val decl : + wp:bool -> Env.env -> Pgm_env.t -> + Theory.theory Theory.Mnm.t -> + Pgm_module.t Theory.Mnm.t -> Pgm_module.uc -> Ptree.program_decl -> Pgm_module.uc diff --git a/src/programs/pgm_wp.ml b/src/programs/pgm_wp.ml index 9b2ca23f3..6794b52a2 100644 --- a/src/programs/pgm_wp.ml +++ b/src/programs/pgm_wp.ml @@ -99,9 +99,8 @@ let wp_forall v f = (* utility functions for building WPs *) -let fresh_label env = - let ty = ty_app (find_ts ~pure:true env "label_") [] in - create_vsymbol (id_fresh "label") ty +let fresh_label () = + create_vsymbol (id_fresh "label") ty_label let wp_binder x f = match x.pv_tv with | Tpure _ -> wp_forall x.pv_pure f @@ -121,46 +120,31 @@ let add_binder x rm = let add_binders = List.fold_right add_binder (* replace old(t) with at(t,lab) everywhere in formula f *) -let rec old_label env lab f = - TermTF.t_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 (find_ls ~pure:true env "old") -> - let t = old_label_term env lab t in (* NECESSARY? *) - t_app (find_ls ~pure:true env "at") [t; t_var lab] t.t_ty +let rec old_label lab t = match t.t_node with + | Tapp (ls, [t]) when ls_equal ls fs_old -> + let t = old_label lab t in (* NECESSARY? *) + t_app fs_at [t; t_var lab] t.t_ty | _ -> - TermTF.t_map (old_label_term env lab) (old_label env lab) t + t_map (old_label lab) t (* replace at(t,lab) with t everywhere in formula f *) -let rec erase_label env lab f = - TermTF.t_map (erase_label_term env lab) (erase_label env lab) f - -and erase_label_term env lab t = match t.t_node with +let rec erase_label lab t = match t.t_node with | Tapp (ls, [t; {t_node = Tvar l}]) - when ls_equal ls (find_ls ~pure:true env "at") && vs_equal l lab -> - erase_label_term env lab t + when ls_equal ls fs_at && vs_equal l lab -> + erase_label lab t | _ -> - TermTF.t_map (erase_label_term env lab) (erase_label env lab) t - -let rec unref env s f = - TermTF.t_map (unref_term env s) (unref env s) f - -and unref_term env s t = match t.t_node with -(*** - | R.Rglobal {p_ls=ls1}, Tapp (ls2, _) when ls_equal ls1 ls2 -> - t_var v - | R.Rlocal {pv_vs=vs1}, Tvar vs2 when vs_equal vs1 vs2 -> - t_var v -***) + t_map (erase_label lab) t + +let rec unref s t = match t.t_node with | Tvar vs -> begin try t_var (Mvs.find vs s) with Not_found -> t end - | Tapp (ls, _) when ls_equal ls (find_ls ~pure:true env "old") -> + | Tapp (ls, _) when ls_equal ls fs_old -> assert false - | Tapp (ls, _) when ls_equal ls (find_ls ~pure:true env "at") -> + | Tapp (ls, _) when ls_equal ls fs_at -> (* do not recurse in at(...) *) t | _ -> - TermTF.t_map (unref_term env s) (unref env s) t + t_map (unref s) t let find_constructor env ts = let km = get_known (pure_uc env) in @@ -268,7 +252,7 @@ let quantify env rm sreg f = in Spv.fold add vars Mvs.empty in - let f = unref env vv' f in + let f = unref vv' f in let f = let add_update x f = let v' = Mvs.find x.pv_pure vv' in @@ -338,10 +322,10 @@ let abstract_wp env rm ef (q',ql') (q,ql) = wp_ands (f :: List.map2 quantify_h ql' ql) let opaque_wp env rm ef q' q = - let lab = fresh_label env in - let q' = post_map (old_label env lab) q' in + let lab = fresh_label () in + let q' = post_map (old_label lab) q' in let f = abstract_wp env rm ef q' q in - erase_label env lab f + erase_label lab f (*s [filter_post k q] removes exc. postconditions from [q] which do not appear in effect [ef] *) @@ -445,10 +429,10 @@ let add_expl msg f = *) let rec wp_expr env rm e q = - let lab = fresh_label env in - let q = post_map (old_label env lab) q in + let lab = fresh_label () in + let q = post_map (old_label lab) q in let f = wp_desc env rm e q in - let f = erase_label env lab f in + let f = erase_label lab f in let f = wp_label ~loc:e.expr_loc f in if Debug.test_flag debug then begin eprintf "@[--------@\n@[e = %a@]@\n" Pgm_pretty.print_expr e; @@ -502,11 +486,11 @@ and wp_desc env rm e q = match e.expr_desc with wp_expr env rm e1 q1 | Eloop ({ loop_invariant = inv; loop_variant = var }, e1) -> let wfr = well_founded_rel var in - let lab = fresh_label env in + let lab = fresh_label () in let q1 = while_post_block env inv var lab e1 in let q1 = sup q1 q in (* exc. posts taken from [q] *) let we = wp_expr env rm e1 q1 in - let we = erase_label env lab we in + let we = erase_label lab we in let sreg = e.expr_effect.E.writes in let w = match inv with | None -> @@ -615,7 +599,7 @@ and wp_desc env rm e q = match e.expr_desc with wp_implies f q | Elabel (lab, e1) -> let w1 = wp_expr env rm e1 q in - erase_label env lab w1 + erase_label lab w1 | Eany c -> (* TODO: propagate call labels into c.c_post *) let w = opaque_wp env rm c.c_effect.E.writes c.c_post q in diff --git a/tests/test-jcf.why b/tests/test-jcf.why index 7932db172..dc60786d8 100644 --- a/tests/test-jcf.why +++ b/tests/test-jcf.why @@ -1,3 +1,4 @@ + theory Order type t logic (<=) t t diff --git a/theories/programs.why b/theories/programs.why deleted file mode 100644 index 218749510..000000000 --- a/theories/programs.why +++ /dev/null @@ -1,19 +0,0 @@ - -theory Prelude - use export bool.Bool - - type unit = () - logic ignore 'a : () - - type label_ - logic at 'a label_ : 'a - logic old 'a : 'a - -end - - -(* -Local Variables: -compile-command: "make -C .. theories/programs" -End: -*) -- GitLab