whyml: exception declarations

src/whyml/mlw_decl.ml

@@ -44,6 +44,7 @@ and pdecl_node =
   | PDdata of data_decl list
   | PDlet  of let_defn
   | PDrec  of rec_defn list
+  | PDexn  of xsymbol
 
 let pd_equal : pdecl -> pdecl -> bool = (==)
 
@@ -146,6 +147,11 @@ let create_rec_decl rdl =
   let syms = List.fold_left add_rd Sid.empty rdl in
   mk_decl (PDrec rdl) syms news
 
+let create_exn_decl xs =
+  let news = Sid.singleton xs.xs_name in
+  let syms = Sid.empty (* FIXME!!! *) in
+  mk_decl (PDexn xs) syms news
+
 (** {2 Known identifiers} *)
 
 type known_map = pdecl Mid.t
@@ -179,4 +185,4 @@ let find_constructors kn its =
   match (Mid.find its.its_pure.ts_name kn).pd_node with
   | PDtype _ -> []
   | PDdata dl -> List.assq its dl
-  | PDlet _ | PDrec _ -> assert false
+  | PDlet _ | PDrec _ | PDexn _ -> assert false

src/whyml/mlw_decl.mli

@@ -46,6 +46,7 @@ and pdecl_node = private
   | PDdata of data_decl list
   | PDlet  of let_defn
   | PDrec  of rec_defn list
+  | PDexn  of xsymbol
 
 (** {2 Declaration constructors} *)
 
@@ -61,6 +62,8 @@ val create_let_decl : let_defn -> pdecl
 
 val create_rec_decl : rec_defn list -> pdecl
 
+val create_exn_decl : xsymbol -> pdecl
+
 (** {2 Known identifiers} *)
 
 type known_map = pdecl Mid.t

src/whyml/mlw_module.ml

@@ -46,6 +46,7 @@ type prgsymbol =
   | PV of pvsymbol
   | PS of psymbol
   | PL of plsymbol
+  | PX of xsymbol
 
 type namespace = {
   ns_it : itysymbol Mstr.t;  (* type symbols *)
@@ -71,6 +72,7 @@ let prg_equal p1 p2 = match p1,p2 with
   | PV p1, PV p2 -> pv_equal p1 p2
   | PS p1, PS p2 -> ps_equal p1 p2
   | PL p1, PL p2 -> pl_equal p1 p2
+  | PX p1, PX p2 -> xs_equal p1 p2
   | _, _ -> false
 
 let rec merge_ns chk ns1 ns2 =
@@ -242,6 +244,9 @@ let add_let uc = function
 let add_rec uc { rec_ps = ps } =
   add_symbol add_ps ps.ps_name (PS ps) uc
 
+let add_exn uc xs =
+  add_symbol add_ps xs.xs_name (PX xs) uc
+
 let add_pdecl uc d =
   let uc =  { uc with
     muc_decls = d :: uc.muc_decls;
@@ -263,6 +268,8 @@ let add_pdecl uc d =
       add_let uc ld.let_var
   | PDrec rdl ->
       List.fold_left add_rec uc rdl
+  | PDexn xs ->
+      add_exn uc xs
 
 let add_pdecl_with_tuples uc d =
   let ids = Mid.set_diff d.pd_syms uc.muc_known in

src/whyml/mlw_module.mli

@@ -34,6 +34,7 @@ type prgsymbol =
   | PV of pvsymbol
   | PS of psymbol
   | PL of plsymbol
+  | PX of xsymbol
 
 type namespace = private {
   ns_it : itysymbol Mstr.t;  (* type symbols *)
@@ -75,6 +76,7 @@ val get_known : module_uc -> known_map
 val use_export : module_uc -> modul -> module_uc
 
 (** Clone *)
+
 val clone_export : module_uc -> modul -> th_inst -> module_uc
 
 (** Logic decls *)

src/whyml/mlw_pretty.ml

@@ -326,6 +326,10 @@ let print_rec_decl fst fmt rd =
   print_rec fst fmt rd;
   forget_tvs_regs ()
 
+let print_exn_decl fmt xs =
+  fprintf fmt "@[<hov 2>exception %a of@ %a@]"
+    print_xs xs print_ity xs.xs_ity
+
 (* Declarations *)
 
 let print_pdecl fmt d = match d.pd_node with
@@ -333,6 +337,7 @@ let print_pdecl fmt d = match d.pd_node with
   | PDdata tl -> print_list_next newline print_data_decl fmt tl
   | PDlet  ld -> print_let_decl fmt ld
   | PDrec rdl -> print_list_next newline print_rec_decl fmt rdl
+  | PDexn  xs -> print_exn_decl fmt xs
 
 let print_next_data_decl = print_data_decl false
 let print_data_decl      = print_data_decl true

src/whyml/mlw_ty.ml

@@ -460,6 +460,8 @@ type xsymbol = {
 exception PolymorphicException of ident * ity
 exception MutableException of ident * ity
 
+let xs_equal : xsymbol -> xsymbol -> bool = (==)
+
 let create_xsymbol id ity =
   let id = id_register id in
   if not (ity_closed ity) then raise (PolymorphicException (id, ity));

src/whyml/mlw_ty.mli

@@ -178,6 +178,8 @@ type xsymbol = private {
   xs_ity  : ity; (* closed and pure *)
 }
 
+val xs_equal : xsymbol -> xsymbol -> bool
+
 val create_xsymbol : preid -> ity -> xsymbol
 
 module Mexn: Map.S with type key = xsymbol

src/whyml/mlw_typing.ml

@@ -32,6 +32,7 @@ open Mlw_ty
 open Mlw_ty.T
 open Mlw_expr
 open Mlw_decl
+open Mlw_pretty
 open Mlw_module
 open Mlw_dty
 
@@ -96,11 +97,12 @@ type denv = {
   denv   : Typing.denv; (* for user type variables only *)
 }
 
-let create_denv uc =
-  { uc = uc;
-    locals = Mstr.empty;
-    tvars = empty_tvars;
-    denv = Typing.create_denv (); }
+let create_denv uc = {
+  uc     = uc;
+  locals = Mstr.empty;
+  tvars  = empty_tvars;
+  denv   = Typing.create_denv ();
+}
 
 (** Typing type expressions *)
 
@@ -170,7 +172,7 @@ let find_field ~loc uc (p,e) =
   let x = Typing.string_list_of_qualid [] p in
   try match ns_find_ps (get_namespace uc) x with
     | PL pl -> (pl,e)
-    | PV _ | PS _ -> errorm ~loc "bad record field %a" Typing.print_qualid p
+    | _ -> errorm ~loc "bad record field %a" Typing.print_qualid p
   with Not_found -> errorm ~loc "unbound symbol %a" Typing.print_qualid p
 
 let find_pure_field ~loc uc (p,e) =
@@ -215,7 +217,6 @@ let mk_let ~loc ~userloc e (desc,dity) =
   DElet ({ id = "q"; id_lab = []; id_loc = loc }, e, e1), dity
 
 (* patterns *)
-let id_user x = id_user x.id x.id_loc
 
 let add_var id dity denv =
   let tvars = add_tvars denv.tvars dity in
@@ -228,6 +229,7 @@ let specialize_qualid ~loc uc p =
     | PV pv -> DEglobal_pv pv, specialize_pvsymbol pv
     | PS ps -> DEglobal_ps ps, specialize_psymbol  ps
     | PL pl -> DEglobal_pl pl, specialize_plsymbol pl
+    | PX xs -> errorm ~loc "unexpected exception symbol %a" print_xs xs
   with Not_found -> try
     let ls = ns_find_ls (Theory.get_namespace (get_theory uc)) x in
     DEglobal_ls ls, specialize_lsymbol ls
@@ -242,7 +244,7 @@ let rec dpattern denv ({ pat_loc = loc } as pp) = match pp.pat_desc with
       PPwild, create_type_variable (), denv
   | Ptree.PPpvar id ->
       let dity = create_type_variable () in
-      PPvar (id_user id), dity, add_var id dity denv
+      PPvar (Denv.create_user_id id), dity, add_var id dity denv
   | Ptree.PPpapp (q,ppl) ->
       let sym, dity = specialize_qualid ~loc denv.uc q in
       dpat_app denv (mk_dexpr sym dity loc []) ppl
@@ -269,7 +271,7 @@ let rec dpattern denv ({ pat_loc = loc } as pp) = match pp.pat_desc with
       PPor (pp1, pp2), dity1, denv
   | Ptree.PPpas (pp, id) ->
       let pp, dity, denv = dpattern denv pp in
-      PPas (pp, id_user id), dity, add_var id dity denv
+      PPas (pp, Denv.create_user_id id), dity, add_var id dity denv
 
 and dpat_app denv ({ dexpr_loc = loc } as de) ppl =
   let add_pp pp (ppl, tyl, denv) =
@@ -278,10 +280,8 @@ and dpat_app denv ({ dexpr_loc = loc } as de) ppl =
   let pp = match de.dexpr_desc with
     | DEglobal_pl pl -> Mlw_expr.PPpapp (pl, ppl)
     | DEglobal_ls ls -> PPlapp (ls, ppl)
-    | DEglobal_pv pv ->
-        errorm ~loc "%a is not a constructor" Mlw_pretty.print_pv pv
-    | DEglobal_ps ps ->
-        errorm ~loc "%a is not a constructor" Mlw_pretty.print_ps ps
+    | DEglobal_pv pv -> errorm ~loc "%a is not a constructor" print_pv pv
+    | DEglobal_ps ps -> errorm ~loc "%a is not a constructor" print_ps ps
     | _ -> assert false
   in
   let res = create_type_variable () in
@@ -494,7 +494,7 @@ let rec expr locals de = match de.dexpr_desc with
       e_rec [def] e2
   | DElet (x, de1, de2) ->
       let e1 = expr locals de1 in
-      let def1 = create_let_defn (id_user x) e1 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 e2 = expr locals de2 in
       e_let def1 e2
@@ -548,7 +548,7 @@ and expr_rec locals rdl =
     let vta = match vty_of_dity dity with
       | VTarrow vta -> vta
       | VTvalue _ -> assert false in
-    let ps = create_psymbol (id_user id) vta vars_empty 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)
   in
   let locals, rdl = Util.map_fold_left step1 locals rdl in
@@ -557,12 +557,12 @@ and expr_rec locals rdl =
 
 and expr_fun locals x bl tr =
   let lam = expr_lam locals bl [] tr in
-  create_fun_defn (id_user x) lam
+  create_fun_defn (Denv.create_user_id x) lam
 
 and expr_lam locals bl _var (_, e, _) =
   let binder (id, ghost, dity) =
     let vtv = vty_value ~ghost (ity_of_dity dity) in
-    create_pvsymbol (id_user id) vtv 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 locals = List.fold_right add_binder pvl locals in
@@ -1047,7 +1047,7 @@ let add_module lib path mm mt m =
               create_rec_decl [def]
           | _ ->
               let e = expr Mstr.empty e in
-              let def = create_let_defn (id_user id) 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
@@ -1056,9 +1056,15 @@ let add_module lib path mm mt m =
         let rdl = expr_rec Mstr.empty rdl in
         let pd = create_rec_decl rdl in
         Loc.try2 loc add_pdecl_with_tuples uc pd
-    | Dparam _ | Dexn _ ->
-        assert false (* TODO *)
-    | Duse _ ->
+    | Dexn (id, pty) ->
+        let ity = match pty with
+          | Some pty ->
+              ity_of_dity (dity_of_pty ~user:false (create_denv uc) pty)
+          | None -> ity_unit in
+        let xs = create_xsymbol (Denv.create_user_id id) ity in
+        let pd = create_exn_decl xs in
+        Loc.try2 loc add_pdecl_with_tuples uc pd
+    | Dparam _ | Duse _ ->
         assert false (*TO BE REMOVED EVENTUALLY *)
   in
   let uc = List.fold_left add_decl uc m.mod_decl in

tests/test-pgm-jcf.mlx

@@ -25,6 +25,8 @@ module N
 
   type myrec 'a = {| f1 : int ; ghost f2 : tree 'a |}
 
+  exception Exit (tree int)
+
   let myfun r =
     let rec on_tree t = match t with
       | Node {| contents = v |} f -> v + on_forest f