Expr: definition and creation of program symbols

Makefile.in

@@ -142,7 +142,7 @@ LIB_CORE = ident ty term pattern decl theory \
 LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
 	     whyconf autodetection
 
-LIB_MLW = ity
+LIB_MLW = ity expr
 
 LIB_PARSER = ptree glob parser typing lexer
 

src/mlw/expr.ml

+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2014   --   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 Term
+open Ity
+
+type psymbol = {
+  ps_name  : ident;
+  ps_cty   : cty;
+  ps_ghost : bool;
+  ps_logic : ps_logic;
+}
+
+and ps_logic =
+  | PLnone            (* non-pure symbol *)
+  | PLvs of vsymbol   (* local let-function *)
+  | PLls of lsymbol   (* top-level let-function or let-predicate *)
+  | PLlemma           (* top-level or local let-lemma *)
+
+module Psym = MakeMSHW (struct
+  type t = psymbol
+  let tag ps = ps.ps_name.id_tag
+end)
+
+module Sps = Psym.S
+module Mps = Psym.M
+module Hps = Psym.H
+module Wps = Psym.W
+
+let ps_equal : psymbol -> psymbol -> bool = (==)
+let ps_hash ps = id_hash ps.ps_name
+let ps_compare ps1 ps2 = id_compare ps1.ps_name ps2.ps_name
+
+let mk_ps id cty gh lg = {
+  ps_name  = id;
+  ps_cty   = cty;
+  ps_ghost = gh;
+  ps_logic = lg;
+}
+
+type ps_kind =
+  | PKnone            (* non-pure symbol *)
+  | PKlocal           (* local let-function *)
+  | PKfunc of int     (* top-level let-function or constructor *)
+  | PKpred            (* top-level let-predicate *)
+  | PKlemma           (* top-level or local let-lemma *)
+
+let create_psymbol id ?(ghost=false) ?(kind=PKnone) c =
+  let add_arg a t = ity_func (ity_purify a.pv_ity) t in
+  let mk_arg a = ty_of_ity a.pv_ity in
+  let check_effects { cty_effect = e } =
+  (* TODO/FIXME: prove that we can indeed ignore resets.
+     Normally, resets neither consult nor change the
+     external state, and do not affect the specification. *)
+    if not (Mreg.is_empty e.eff_writes &&
+            Sexn.is_empty e.eff_raises &&
+            not e.eff_diverg) then
+      Loc.errorm "this function has side effects, \
+                  it cannot be declared as pure" in
+  let check_reads { cty_freeze = isb } =
+    if not (Mreg.is_empty isb.isb_reg) then
+      Loc.errorm "this function depends on the global state, \
+                  it cannot be declared as pure" in
+  match kind with
+  | PKnone ->
+      mk_ps (id_register id) c ghost PLnone
+  | PKlocal ->
+      check_effects c; check_reads c;
+      let ity = ity_purify c.cty_result in
+      let ity = List.fold_right add_arg c.cty_args ity in
+      (* When declaring local let-functions, we need to create a
+         mapping vsymbol to use in assertions. As vsymbols are not
+         generalisable, we have to freeze the type variables (but
+         not regions) of the psymbol, and the easiest way to do that
+         is to make these type variables appear in c.cty_reads.
+         Moreover, we want to maintain the invariant that every
+         variable that occurs freely in an assertion comes from
+         a pvsymbol. Therefore, we create a pvsymbol whose type
+         is a snapshot of the appropriate mapping type, and put
+         its pv_vs into the ps_logic field. This pvsymbol cannot
+         be used in the program, as it has lost all preconditions,
+         which is why we declare it as ghost. In other words,
+         this pvsymbol behaves exactly as Epure of its pv_vs. *)
+      let pv = create_pvsymbol ~ghost:true id ity in
+      let c = cty_add_reads c (Spv.singleton pv) in
+      mk_ps pv.pv_vs.vs_name c ghost (PLvs pv.pv_vs)
+  | PKfunc constr ->
+      check_effects c; check_reads c;
+      let ls = create_fsymbol id ~constr
+        (List.map mk_arg c.cty_args) (ty_of_ity c.cty_result) in
+      mk_ps ls.ls_name c ghost (PLls ls)
+  | PKpred ->
+      check_effects c; check_reads c;
+      if not (ity_equal c.cty_result ity_bool) then
+        Loc.errorm "this function does not return a boolean value, \
+                    it cannot be declared as a pure predicate";
+      let ls = create_psymbol id (List.map mk_arg c.cty_args) in
+      mk_ps ls.ls_name c ghost (PLls ls)
+  | PKlemma ->
+      check_effects c;
+      mk_ps (id_register id) c ghost PLlemma

src/mlw/expr.mli

+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2014   --   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 Term
+open Ity
+
+(** {2 Program symbols} *)
+
+type psymbol = private {
+  ps_name  : ident;
+  ps_cty   : cty;
+  ps_ghost : bool;
+  ps_logic : ps_logic;
+}
+
+and ps_logic =
+  | PLnone            (* non-pure symbol *)
+  | PLvs of vsymbol   (* local let-function *)
+  | PLls of lsymbol   (* top-level let-function or let-predicate *)
+  | PLlemma           (* top-level or local let-lemma *)
+
+module Mps : Extmap.S with type key = psymbol
+module Sps : Extset.S with module M = Mps
+module Hps : Exthtbl.S with type key = psymbol
+module Wps : Weakhtbl.S with type key = psymbol
+
+val ps_compare : psymbol -> psymbol -> int
+val ps_equal : psymbol -> psymbol -> bool
+val ps_hash : psymbol -> int
+
+type ps_kind =
+  | PKnone            (* non-pure symbol *)
+  | PKlocal           (* local let-function *)
+  | PKfunc of int     (* top-level let-function or constructor *)
+  | PKpred            (* top-level let-predicate *)
+  | PKlemma           (* top-level or local let-lemma *)
+
+val create_psymbol : preid -> ?ghost:bool -> ?kind:ps_kind -> cty -> psymbol
+(** If [?kind] is supplied and is not [PKnone], then [cty]
+    must have no effects except for resets which are ignored.
+    If [?kind] is [PKnone] or [PKlemma], external mutable reads
+    are allowed, otherwise [cty.cty_freeze.isb_reg] must be empty.
+    If [?kind] is [PKlocal], the type variables in [cty] are frozen
+    but regions are instantiable. If [?kind] is [PKpred] the result
+    type must be [ity_bool]. If [?kind] is [PKlemma] and the result
+    type is not [ity_unit], an existential premise is generated. *)

src/mlw/ity.ml

@@ -109,6 +109,11 @@ let ity_hash ity = Weakhtbl.tag_hash ity.ity_tag
 let reg_hash reg = id_hash reg.reg_name
 let pv_hash  pv  = id_hash pv.pv_vs.vs_name
 
+let its_compare its1 its2 = id_compare its1.its_ts.ts_name its2.its_ts.ts_name
+let ity_compare ity1 ity2 = Pervasives.compare (ity_hash ity1) (ity_hash ity2)
+let reg_compare reg1 reg2 = id_compare reg1.reg_name reg2.reg_name
+let pv_compare  pv1  pv2  = id_compare pv1.pv_vs.vs_name pv2.pv_vs.vs_name
+
 exception NonUpdatable of itysymbol * ity
 
 let check_its_args s tl =
@@ -529,6 +534,8 @@ let create_pvsymbol, restore_pv =
     pv),
   (fun vs -> Wvs.find vs_to_pv vs)
 
+let freeze_pv v s = ity_freeze s v.pv_ity
+
 let pvs_of_vss pvs vss =
   Mvs.fold (fun vs _ s -> Spv.add (restore_pv vs) s) vss pvs
 
@@ -590,6 +597,8 @@ exception PolymorphicException of ident * ity
 exception MutableException of ident * ity
 
 let xs_equal : xsymbol -> xsymbol -> bool = (==)
+let xs_hash xs = id_hash xs.xs_name
+let xs_compare xs1 xs2 = id_compare xs1.xs_name xs2.xs_name
 
 let create_xsymbol id ity =
   let id = id_register id in
@@ -802,8 +811,20 @@ let spec_t_fold fn_t acc pre post xpost =
   let acc = fn_l (fn_l acc pre) post in
   Mexn.fold (fun _ l a -> fn_l a l) xpost acc
 
+let check_tvs reads result pre post xpost =
+  (* every type variable in spec comes either from a known vsymbol
+     or from the result type. We need this to ensure that we always
+     can do a full instantiation. TODO: do we really need this? *)
+  let add_pv v s = ity_freevars s v.pv_ity in
+  let tvs = Spv.fold add_pv reads (ity_freevars Stv.empty result) in
+  let check_tvs () t =
+    let ttv = t_ty_freevars Stv.empty t in
+    if not (Stv.subset ttv tvs) then Loc.error ?loc:t.t_loc
+      (UnboundTypeVar (Stv.choose (Stv.diff ttv tvs))) in
+  spec_t_fold check_tvs () pre post xpost
+
 let create_cty args pre post xpost reads effect result =
-  let exn = Invalid_argument "Ity.cty" in
+  let exn = Invalid_argument "Ity.create_cty" in
   (* pre, post, and xpost are well-typed *)
   let check_post ity f = match f.t_node with
     | Teps _ -> Ty.ty_equal_check (ty_of_ity ity) (t_type f)
@@ -815,23 +836,18 @@ let create_cty args pre post xpost reads effect result =
   (* the arguments must be pairwise distinct *)
   let sarg = List.fold_right (Spv.add_new exn) args Spv.empty in
   (* complete reads and freeze the external context *)
-  let pv_freeze pv frz = ity_freeze frz pv.pv_ity in
   let reads = spec_t_fold t_freepvs reads pre post xpost in
-  let freeze = Spv.fold pv_freeze (Spv.diff reads sarg) isb_empty in
+  let freeze = Spv.fold freeze_pv (Spv.diff reads sarg) isb_empty in
   let reads = Spv.union reads sarg in
-  (* every type variable in spec comes from a known vsymbol.
-     We need this to ensure that we always can do a full inst.
-     TODO: do we really need this? *)
-  let add_pv v s = ty_freevars s v.pv_vs.vs_ty in
-  let tvs = ty_freevars Stv.empty (ty_of_ity result) in
-  let tvs = Spv.fold add_pv reads tvs in
-  let check_tvs () t =
-    let ttv = t_ty_freevars Stv.empty t in
-    if not (Stv.subset ttv tvs) then Loc.error ?loc:t.t_loc
-      (UnboundTypeVar (Stv.choose (Stv.diff ttv tvs))) in
-  spec_t_fold check_tvs () pre post xpost;
+  check_tvs reads result pre post xpost;
+  (* remove exceptions whose postcondition is False *)
+  let is_false _ xq = List.exists (t_equal t_false) xq in
+  let nothrow = Mexn.filter is_false xpost in
+  let xpost = Mexn.set_diff xpost nothrow in
+  let raises = Mexn.set_diff effect.eff_raises nothrow in
+  let effect = { effect with eff_raises = raises } in
   (* remove effects on unknown regions *)
-  let known = (Spv.fold pv_freeze sarg freeze).isb_reg in
+  let known = (Spv.fold freeze_pv sarg freeze).isb_reg in
   let filter m = Mreg.set_inter m known in
   let effect = { effect with
     eff_writes = filter effect.eff_writes;
@@ -856,9 +872,8 @@ let cty_apply c pvl args res =
         let vsb = Mvs.add a.pv_vs (t_var v.pv_vs) vsb in
         apply isb same gh vsb al vl
     | al, [] when List.length al = List.length args ->
-        let freeze_pv s v = ity_freeze s v.pv_ity in
         let freeze = if same (*so far*) then isb else
-          List.fold_left freeze_pv c.cty_freeze pvl in
+          List.fold_right freeze_pv pvl c.cty_freeze in
         let same = same && ity_equal c.cty_result res &&
           List.for_all2 (fun a t -> ity_equal a.pv_ity t) al args in
         if same && pvl = [] then gh, c (*what was the point?*) else
@@ -885,3 +900,18 @@ let cty_apply c pvl args res =
     | _ ->
         invalid_arg "Ity.cty_apply" in
   apply c.cty_freeze true false Mvs.empty c.cty_args pvl
+
+let cty_add_reads c pvs =
+  (* the external reads are already frozen and
+     the arguments should stay instantiable *)
+  let pvs = Spv.diff pvs c.cty_reads in
+  { c with cty_reads  = Spv.union c.cty_reads pvs;
+           cty_freeze = Spv.fold freeze_pv pvs c.cty_freeze }
+
+let cty_add_pre c pre =
+  List.iter (fun f -> if f.t_ty <> None then
+    Loc.error ?loc:f.t_loc (Term.FmlaExpected f)) pre;
+  let pvs = List.fold_left t_freepvs Spv.empty pre in
+  let c = cty_add_reads c pvs in
+  check_tvs c.cty_reads c.cty_result pre [] Mexn.empty;
+  { c with cty_pre = pre @ c.cty_pre }

src/mlw/ity.mli

@@ -76,6 +76,11 @@ module Spv  : Extset.S with module M = Mpv
 module Hpv  : Exthtbl.S with type key = pvsymbol
 module Wpv  : Weakhtbl.S with type key = pvsymbol
 
+val its_compare : itysymbol -> itysymbol -> int
+val ity_compare : ity -> ity -> int
+val reg_compare : region -> region -> int
+val pv_compare  : pvsymbol -> pvsymbol -> int
+
 val its_equal : itysymbol -> itysymbol -> bool
 val ity_equal : ity -> ity -> bool
 val reg_equal : region -> region -> bool
@@ -235,7 +240,9 @@ type xsymbol = private {
   xs_ity  : ity; (** closed and immutable *)
 }
 
+val xs_compare : xsymbol -> xsymbol -> int
 val xs_equal : xsymbol -> xsymbol -> bool
+val xs_hash: xsymbol -> int
 
 exception PolymorphicException of ident * ity
 exception MutableException of ident * ity
@@ -314,3 +321,15 @@ val cty_apply : cty -> pvsymbol list -> ity list -> ity -> bool * cty
     region in [pvl] freezed. The combined length of [pvl] and [rest]
     must be equal to the length of [cty.cty_args]. The instantiation
     must be compatible with [cty.cty_freeze]. *)
+
+val cty_add_reads : cty -> Spv.t -> cty
+(** [cty_add_reads cty pvs] adds variables in [pvs] to [cty.cty_reads].
+    This function performs capture: if some variables in [pvs] occur
+    in [cty.cty_args], no renaming is made, and the corresponding type
+    variables and regions are not frozen. *)
+
+val cty_add_pre : cty -> pre list -> cty
+(** [cty_add_pre cty fl] appends pre-conditions in [fl] to [cty.cty_pre].
+    This function performs capture: the formulas in [fl] may refer to
+    the variables in [cty.cty_args]. Only the new external dependencies
+    in [fl] are added to [cty.cty_reads] and frozen. *)