From 70a028ad81434d6fd2bccd152be1ed8a8f4662b1 Mon Sep 17 00:00:00 2001
From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre@lri.fr>
Date: Fri, 15 Jun 2012 14:12:26 +0200
Subject: [PATCH] whyml: e_assert, e_absurd
---
src/parser/typing.ml | 10 +++----
src/parser/typing.mli | 2 +-
src/programs/pgm_typing.ml | 2 +-
src/whyml/mlw_expr.ml | 15 +++++++++-
src/whyml/mlw_expr.mli | 6 ++++
src/whyml/mlw_typing.ml | 60 ++++++++++++++++++++++++++++----------
6 files changed, 71 insertions(+), 24 deletions(-)
diff --git a/src/parser/typing.ml b/src/parser/typing.ml
index 95ecbcf892..bf3001afb1 100644
--- a/src/parser/typing.ml
+++ b/src/parser/typing.ml
@@ -120,9 +120,7 @@ type denv = {
dvars : dty Mstr.t; (* local variables, to be bound later *)
}
-let create_denv () = {
- dvars = Mstr.empty;
-}
+let denv_empty = { dvars = Mstr.empty }
let mem_var x denv = Mstr.mem x denv.dvars
let find_var x denv = Mstr.find x denv.dvars
@@ -936,7 +934,7 @@ let add_logics dl th =
let create_symbol th d =
let id = d.ld_ident.id in
let v = create_user_id d.ld_ident in
- let denv = create_denv () in
+ let denv = denv_empty in
Hashtbl.add denvs id denv;
let type_ty (_,t) = ty_of_dty (dty th t) in
let pl = List.map type_ty d.ld_params in
@@ -1020,14 +1018,14 @@ let type_fmla uc denv env f =
let add_prop k loc s f th =
let pr = create_prsymbol (create_user_id s) in
- let f = type_fmla th (create_denv ()) Mstr.empty f in
+ let f = type_fmla th denv_empty Mstr.empty f in
Loc.try4 loc add_prop_decl th k pr f
let loc_of_id id = of_option id.Ident.id_loc
let add_inductives s dl th =
(* 1. create all symbols and make an environment with these symbols *)
- let denv = create_denv () in
+ let denv = denv_empty in
let psymbols = Hashtbl.create 17 in
let create_symbol th d =
let id = d.in_ident.id in
diff --git a/src/parser/typing.mli b/src/parser/typing.mli
index 5a0ea9290a..2bac3abfcf 100644
--- a/src/parser/typing.mli
+++ b/src/parser/typing.mli
@@ -61,7 +61,7 @@ val create_user_type_var : string -> Denv.dty
type denv
-val create_denv : unit -> denv
+val denv_empty : denv
val mem_var : string -> denv -> bool
val find_var : string -> denv -> Denv.dty
diff --git a/src/programs/pgm_typing.ml b/src/programs/pgm_typing.ml
index 4550a711a1..793ce0ab54 100644
--- a/src/programs/pgm_typing.ml
+++ b/src/programs/pgm_typing.ml
@@ -86,7 +86,7 @@ type denv = {
let create_denv uc =
{ uc = uc;
locals = Mstr.empty;
- denv = Typing.create_denv (); }
+ denv = Typing.denv_empty; }
let loc_of_id id = Util.of_option id.Ident.id_loc
diff --git a/src/whyml/mlw_expr.ml b/src/whyml/mlw_expr.ml
index 75bf7efaa2..17e4ce41cb 100644
--- a/src/whyml/mlw_expr.ml
+++ b/src/whyml/mlw_expr.ml
@@ -273,6 +273,7 @@ let make_ppattern pp vtv =
type pre = term (* precondition *)
type post = term (* postcondition *)
type xpost = post Mexn.t (* exceptional postconditions *)
+type assertion_kind = Ptree.assertion_kind
type expr = {
e_node : expr_node;
@@ -297,6 +298,8 @@ and expr_node =
| Eany of any_effect
| Eraise of xsymbol * pvsymbol
| Etry of expr * (xsymbol * pvsymbol * expr) list
+ | Eassert of assertion_kind * term
+ | Eabsurd
and let_defn = {
let_var : let_var;
@@ -779,6 +782,15 @@ let e_try d bl =
in
branch dvtv.vtv_ghost eff_empty Mid.empty bl
+let e_absurd ity =
+ let vty = VTvalue (vty_value ity) in
+ mk_expr Eabsurd vty eff_empty Mid.empty
+
+let e_assert ass f =
+ let eff, vars = assert false (*TODO*) in
+ let vty = VTvalue (vty_value ity_unit) in
+ mk_expr (Eassert (ass, f)) vty eff vars
+
(* Compute the fixpoint on recursive definitions *)
let vars_equal vs1 vs2 =
@@ -847,7 +859,8 @@ let rec expr_subst psm e = match e.e_node with
| Etry (e,bl) ->
let branch (xs,pv,e) = xs, pv, expr_subst psm e in
e_try (expr_subst psm e) (List.map branch bl)
- | Elogic _ | Evalue _ | Earrow _ | Eassign _ | Eraise _ -> e
+ | Elogic _ | Evalue _ | Earrow _ | Eassign _ | Eraise _
+ | Eabsurd | Eassert _ -> e
and create_rec_defn defl =
let conv m (ps,lam) =
diff --git a/src/whyml/mlw_expr.mli b/src/whyml/mlw_expr.mli
index d3559f25fc..a0cd2b0dc6 100644
--- a/src/whyml/mlw_expr.mli
+++ b/src/whyml/mlw_expr.mli
@@ -113,6 +113,7 @@ val make_ppattern : pre_ppattern -> vty_value -> pvsymbol Mstr.t * ppattern
type pre = term (* precondition *)
type post (* postcondition: a formula with a bound variable *)
type xpost = post Mexn.t (* exceptional postconditions *)
+type assertion_kind = Ptree.assertion_kind
val create_post : vsymbol -> term -> post
val open_post : post -> vsymbol * term
@@ -140,6 +141,8 @@ and expr_node = private
| Eany of any_effect
| Eraise of xsymbol * pvsymbol
| Etry of expr * (xsymbol * pvsymbol * expr) list
+ | Eassert of assertion_kind * term
+ | Eabsurd
and let_defn = private {
let_var : let_var;
@@ -231,3 +234,6 @@ val e_not : expr -> expr
val e_raise : xsymbol -> expr -> expr
val e_try : expr -> (xsymbol * pvsymbol * expr) list -> expr
+val e_absurd : ity -> expr
+val e_assert : assertion_kind -> term -> expr
+
diff --git a/src/whyml/mlw_typing.ml b/src/whyml/mlw_typing.ml
index 340f18b9f5..2fde16af52 100644
--- a/src/whyml/mlw_typing.ml
+++ b/src/whyml/mlw_typing.ml
@@ -101,7 +101,7 @@ let create_denv uc = {
uc = uc;
locals = Mstr.empty;
tvars = empty_tvars;
- denv = Typing.create_denv ();
+ denv = Typing.denv_empty;
}
(** Typing type expressions *)
@@ -480,16 +480,43 @@ and dlambda ~userloc denv bl _var (p, e, q) =
and dpost _denv (q, _ql) =
q, [] (* TODO *)
+type locals = {
+ let_vars: let_var Mstr.t;
+ log_vars: vsymbol Mstr.t;
+ log_denv: Typing.denv;
+}
+
+let locals_empty = {
+ let_vars = Mstr.empty;
+ log_vars = Mstr.empty;
+ log_denv = Typing.denv_empty;
+}
+
+let rec dty_of_ty ty = match ty.ty_node with
+ | Ty.Tyvar v ->
+ Typing.create_user_type_var v.tv_name.id_string
+ | Ty.Tyapp (ts, tyl) ->
+ Denv.tyapp ts (List.map dty_of_ty tyl)
+
+let add_local x lv locals = match lv with
+ | LetA _ ->
+ { locals with let_vars = Mstr.add x lv locals.let_vars }
+ | LetV pv ->
+ let dty = dty_of_ty pv.pv_vs.vs_ty in
+ { let_vars = Mstr.add x lv locals.let_vars;
+ log_vars = Mstr.add x pv.pv_vs locals.log_vars;
+ log_denv = Typing.add_var x dty locals.log_denv }
+
let rec expr uc locals de = match de.dexpr_desc with
| DElocal x ->
- assert (Mstr.mem x locals);
- begin match Mstr.find x locals with
+ assert (Mstr.mem x locals.let_vars);
+ begin match Mstr.find x locals.let_vars with
| LetV pv -> e_value pv
| LetA ps -> e_cast ps (vty_of_dity de.dexpr_type)
end
| DElet (x, { dexpr_desc = DEfun (bl, tr) }, de2) ->
let def1 = expr_fun uc locals x bl tr in
- let locals = Mstr.add x.id (LetA def1.rec_ps) locals in
+ let locals = add_local x.id (LetA def1.rec_ps) locals in
let e2 = expr uc locals de2 in
e_rec [def1] e2
| DEfun (bl, tr) ->
@@ -500,12 +527,12 @@ let rec expr uc locals de = match de.dexpr_desc with
| DElet (x, de1, de2) ->
let e1 = expr uc locals de1 in
let def1 = create_let_defn (Denv.create_user_id x) e1 in
- let locals = Mstr.add x.id def1.let_var locals in
+ let locals = add_local x.id def1.let_var locals in
let e2 = expr uc locals de2 in
e_let def1 e2
| DEletrec (rdl, de1) ->
let rdl = expr_rec uc locals rdl in
- let add_rd { rec_ps = ps } = Mstr.add ps.ps_name.id_string (LetA ps) in
+ let add_rd { rec_ps = ps } = add_local ps.ps_name.id_string (LetA ps) in
let e1 = expr uc (List.fold_right add_rd rdl locals) de1 in
e_rec rdl e1
| DEapply (de1, del) ->
@@ -542,12 +569,15 @@ let rec expr uc locals de = match de.dexpr_desc with
let vtv = vtv_of_expr e1 in
let branch (pp,de) =
let vm, pp = make_ppattern pp vtv in
- let locals = Mstr.fold (fun s pv -> Mstr.add s (LetV pv)) vm locals in
+ let locals = Mstr.fold (fun s pv -> add_local s (LetV pv)) vm locals in
pp, expr uc locals de in
e_case e1 (List.map branch bl)
- | DEassert (ass, lexpr) ->
- (* let f = Typing.type_fmla (get_theory uc) *)
-assert false (*TODO*)
+ | DEassert (ass, f) ->
+ let f =
+ Typing.type_fmla (get_theory uc) locals.log_denv locals.log_vars f in
+ e_assert ass f
+ | DEabsurd ->
+ e_absurd (ity_of_dity de.dexpr_type)
| _ ->
assert false (*TODO*)
@@ -557,7 +587,7 @@ and expr_rec uc locals rdl =
| VTarrow vta -> vta
| VTvalue _ -> assert false in
let ps = create_psymbol (Denv.create_user_id id) vta vars_empty in
- Mstr.add id.id (LetA ps) locals, (ps, bl, var, tr)
+ add_local id.id (LetA ps) locals, (ps, bl, var, tr)
in
let locals, rdl = Util.map_fold_left step1 locals rdl in
let step2 (ps, bl, var, tr) = ps, expr_lam uc locals bl var tr in
@@ -572,7 +602,7 @@ and expr_lam uc locals bl _var (_, e, _) =
let vtv = vty_value ~ghost (ity_of_dity dity) in
create_pvsymbol (Denv.create_user_id id) vtv in
let pvl = List.map binder bl in
- let add_binder pv = Mstr.add pv.pv_vs.vs_name.id_string (LetV pv) in
+ let add_binder pv = add_local pv.pv_vs.vs_name.id_string (LetV pv) in
let locals = List.fold_right add_binder pvl locals in
let e = expr uc locals e in
let ty = match e.e_vty with
@@ -1051,17 +1081,17 @@ let add_module lib path mm mt m =
let e = dexpr ~userloc:None (create_denv uc) e in
let pd = match e.dexpr_desc with
| DEfun (bl, tr) ->
- let def = expr_fun uc Mstr.empty id bl tr in
+ let def = expr_fun uc locals_empty id bl tr in
create_rec_decl [def]
| _ ->
- let e = expr uc Mstr.empty e in
+ let e = expr uc locals_empty e in
let def = create_let_defn (Denv.create_user_id id) e in
create_let_decl def
in
Loc.try2 loc add_pdecl_with_tuples uc pd
| Dletrec rdl ->
let rdl = dletrec ~userloc:None (create_denv uc) rdl in
- let rdl = expr_rec uc Mstr.empty rdl in
+ let rdl = expr_rec uc locals_empty rdl in
let pd = create_rec_decl rdl in
Loc.try2 loc add_pdecl_with_tuples uc pd
| Dexn (id, pty) ->
--
GitLab