whyml: e_assert, e_absurd

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

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

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
 

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) =

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
+

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) ->