whyml: handle abstract types

src/parser/parser.mly

@@ -435,6 +435,7 @@ list1_type_decl:
 type_decl:
 | lident labels type_args typedefn
   { let model, vis, def = $4 in
+    let vis = if model then Abstract else vis in
     { td_loc = floc (); td_ident = add_lab $1 $2;
       td_params = $3; td_model = model; td_vis = vis; td_def = def } }
 ;

src/whyml/mlw_decl.ml

@@ -99,14 +99,15 @@ let create_data_decl tdl =
     in
     ignore (List.for_all check_arg vtvs);
     (* build the constructor ps *)
+    let hidden = its.its_abst in
     let tvl = List.map ity_var its.its_args in
     let res = vty_value (ity_app its tvl its.its_regs) in
-    let pls = create_plsymbol id vtvs res in
+    let pls = create_plsymbol ~hidden id vtvs res in
     news := Sid.add pls.pl_ls.ls_name !news;
     (* build the projections, if any *)
     let build_proj id vtv =
       try Hid.find projections id with Not_found ->
-      let pls = create_plsymbol (id_clone id) [res] vtv in
+      let pls = create_plsymbol ~hidden (id_clone id) [res] vtv in
       news := Sid.add pls.pl_ls.ls_name !news;
       Hid.add projections id pls;
       pls

src/whyml/mlw_expr.ml

@@ -74,11 +74,12 @@ type plsymbol = {
   pl_args   : vty_value list;
   pl_value  : vty_value;
   pl_effect : effect;
+  pl_hidden : bool;
 }
 
 let pl_equal : plsymbol -> plsymbol -> bool = (==)
 
-let create_plsymbol id args value =
+let create_plsymbol ?(hidden=false) id args value =
   let ty_of_vtv vtv = ty_of_ity vtv.vtv_ity in
   let pure_args = List.map ty_of_vtv args in
   let ls = create_fsymbol id pure_args (ty_of_vtv value) in
@@ -90,6 +91,7 @@ let create_plsymbol id args value =
     pl_args   = args;
     pl_value  = value;
     pl_effect = effect;
+    pl_hidden = hidden;
   }
 
 let ity_of_ty_opt ty = ity_of_ty (Util.def_option ty_bool ty)
@@ -98,7 +100,10 @@ let fake_pls = Wls.memoize 17 (fun ls ->
   { pl_ls     = ls;
     pl_args   = List.map (fun ty -> vty_value (ity_of_ty ty)) ls.ls_args;
     pl_value  = vty_value (ity_of_ty_opt ls.ls_value);
-    pl_effect = eff_empty })
+    pl_effect = eff_empty;
+    pl_hidden = false })
+
+exception HiddenPLS of lsymbol
 
 (** specification *)
 
@@ -259,6 +264,7 @@ let ppat_is_wild pp = match pp.ppat_pattern.pat_node with
 let ppat_plapp pls ppl vtv =
   if vtv.vtv_mut <> None then
     Loc.errorm "Only variable patterns can be mutable";
+  if pls.pl_hidden then raise (HiddenPLS pls.pl_ls);
   (* FIXME? Since pls is a constructor, the result type vtv will
      cover every type variable and region in the signature of pls.
      Then the following ity_match call is enough to build the full
@@ -353,6 +359,7 @@ let make_ppattern pp vtv =
         ppat_vtv     = vtv;
         ppat_effect  = eff_empty; }
     | PPpapp (pls,ppl) ->
+        if pls.pl_hidden then raise (HiddenPLS pls.pl_ls);
         (* FIXME? Since pls is a constructor, the result type vtv will
            cover every type variable and region in the signature of pls.
            Then the following ity_match call is enough to build the full
@@ -638,6 +645,7 @@ let vtv_of_expr e = match e.e_vty with
   | VTarrow _ -> Loc.error ?loc:e.e_loc (ValueExpected e)
 
 let e_plapp pls el ity =
+  if pls.pl_hidden then raise (HiddenPLS pls.pl_ls);
   let rec app tl vars ghost eff sbs vtvl argl =
     match vtvl, argl with
       | [],[] ->

src/whyml/mlw_expr.mli

@@ -75,14 +75,18 @@ type plsymbol = private {
   pl_args   : vty_value list;
   pl_value  : vty_value;
   pl_effect : effect;
+  pl_hidden : bool;
 }
 
 val pl_equal : plsymbol -> plsymbol -> bool
 
-val create_plsymbol : preid -> vty_value list -> vty_value -> plsymbol
+val create_plsymbol :
+  ?hidden:bool -> preid -> vty_value list -> vty_value -> plsymbol
   (* FIXME? Effect calculation is hardwired to correspond to constructors
      and projections: mutable arguments are reset, mutable result is read. *)
 
+exception HiddenPLS of lsymbol
+
 (** specification *)
 
 type pre = term          (* precondition *)

src/whyml/mlw_module.ml

@@ -232,7 +232,7 @@ let add_data uc (its,csl) =
   let add_proj = option_fold add_pls in
   let add_constr uc (ps,pjl) = List.fold_left add_proj (add_pls uc ps) pjl in
   let uc = add_symbol add_it its.its_pure.ts_name its uc in
-  List.fold_left add_constr uc csl
+  if its.its_abst then uc else List.fold_left add_constr uc csl
 
 let add_let uc = function
   | LetV pv -> add_symbol add_ps pv.pv_vs.vs_name (PV pv) uc
@@ -245,7 +245,7 @@ let add_exn uc xs =
   add_symbol add_ps xs.xs_name (PX xs) uc
 
 let add_pdecl uc d =
-  let uc =  { uc with
+  let uc = { uc with
     muc_decls = d :: uc.muc_decls;
     muc_known = known_add_decl (Theory.get_known uc.muc_theory) uc.muc_known d;
     muc_local = Sid.union uc.muc_local d.pd_news }

src/whyml/mlw_pretty.ml

@@ -459,6 +459,9 @@ let () = Exn_printer.register
       fprintf fmt "The type of exception %s has mutable components" id.id_string
   | Mlw_ty.IllegalAlias _reg ->
       fprintf fmt "This application creates an illegal alias"
+  | Mlw_expr.HiddenPLS ls ->
+      fprintf fmt "`%a' is a constructor/field of an abstract type \
+      and cannot be used in a program" print_ls ls;
   | Mlw_expr.GhostWrite (_e, _reg) ->
       fprintf fmt "This expression stores a ghost value in a non-ghost location"
   | Mlw_expr.GhostRaise (_e, xs) ->

src/whyml/mlw_ty.ml

@@ -434,7 +434,9 @@ let create_itysymbol name ?(abst=false) ?(priv=false) args regs def =
   (* all regions in [def] must be in [regs] *)
   let check r = Sreg.mem r sregs || raise (UnboundRegion r) in
   ignore (option_map (ity_v_all Util.ttrue check) def);
-  (* if a type is an alias then abst and priv will be ignored *)
+  (* if a type is an alias then it cannot be abstract or private *)
+  if abst && def <> None then Loc.errorm "Type alias cannot be abstract";
+  if priv && def <> None then Loc.errorm "Type alias cannot be private";
   { its_pure  = purets;
     its_args  = args;
     its_regs  = regs;

src/whyml/mlw_typing.ml

@@ -156,6 +156,33 @@ let rec decompose_app args e = match e.Ptree.expr_desc with
   | Eapply (e1, e2) -> decompose_app (e2 :: args) e1
   | _ -> e, args
 
+(* namespace lookup *)
+
+let uc_find_ls uc p =
+  let x = Typing.string_list_of_qualid [] p in
+  ns_find_ls (Theory.get_namespace (get_theory uc)) x
+
+let uc_find_prgs uc p =
+  let x = Typing.string_list_of_qualid [] p in
+  ns_find_ps (get_namespace uc) x
+
+exception LS of lsymbol
+
+let uc_find_ps_or_ls uc p =
+  let x = Typing.string_list_of_qualid [] p in
+  try ns_find_ps (get_namespace uc) x with Not_found ->
+  (* we didn't find p in the module namespace *)
+  let ls = ns_find_ls (Theory.get_namespace (get_theory uc)) x in
+  (* and we did find it in the pure theory *)
+  if Mid.mem ls.ls_name (get_known uc) then
+    (* but it was defined in a program declaration! *)
+    error ~loc:(qloc p) (HiddenPLS ls);
+  (* fine, it's just a pure lsymbol *)
+  raise (LS ls)
+
+let uc_find_ps uc p =
+  try uc_find_ps_or_ls uc p with LS _ -> raise Not_found
+
 (* record parsing *)
 
 let parse_record uc fll =
@@ -176,24 +203,17 @@ let parse_record uc fll =
   in
   cs,pjl,flm
 
-let find_field 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)
-    | _ -> errorm ~loc:(qloc p) "bad record field %a" print_qualid p
+let find_field uc (p,e) = try match uc_find_ps uc p with
+  | PL pl -> (pl,e)
+  | _ -> errorm ~loc:(qloc p) "bad record field %a" print_qualid p
   with Not_found -> errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
 
-let find_pure_field uc (p,e) =
-  let x = Typing.string_list_of_qualid [] p in
-  try ns_find_ls (Theory.get_namespace (get_theory uc)) x, e
+let find_pure_field uc (p,e) = try uc_find_ls uc p, e
   with Not_found -> errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
 
 let pure_record uc = function
   | [] -> raise Decl.EmptyRecord
-  | (p,_)::_ ->
-      let x = Typing.string_list_of_qualid [] p in
-      begin try ignore (ns_find_ps (get_namespace uc) x); false
-      with Not_found -> true end
+  | (p,_)::_ -> (try ignore (uc_find_ps uc p); false with Not_found -> true)
 
 let hidden_pl ~loc pl =
   { de_desc = DEglobal_pl pl;
@@ -236,45 +256,28 @@ let add_var id dity denv =
   let locals = Mstr.add id.id (tvars,dity) denv.locals in
   { denv with locals = locals; tvars = tvars }
 
-let specialize_qualid uc p =
-  let x = Typing.string_list_of_qualid [] p in
-  try match ns_find_ps (get_namespace uc) x with
-    | 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:(qloc p) "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
-  with Not_found ->
-    errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
+let specialize_qualid uc p = try match uc_find_ps_or_ls uc p with
+  | 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:(qloc p) "unexpected exception symbol %a" print_xs xs
+  with
+  | LS ls -> DEglobal_ls ls, specialize_lsymbol ls
+  | Not_found -> errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
 
-let find_xsymbol uc p =
-  let x = Typing.string_list_of_qualid [] p in
-  try match ns_find_ps (get_namespace uc) x with
-    | PX xs -> xs
-    | _ -> errorm ~loc:(qloc p) "exception symbol expected"
-  with Not_found ->
-    errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
+let find_xsymbol uc p = try match uc_find_prgs uc p with
+  | PX xs -> xs
+  | _ -> errorm ~loc:(qloc p) "exception symbol expected"
+  with Not_found -> errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
 
-let find_variant_ls uc p =
-  let x = Typing.string_list_of_qualid [] p in
-  try match ns_find_ps (get_namespace uc) x with
-    | _ -> errorm ~loc:(qloc p) "%a is not a binary relation" print_qualid p
-  with Not_found -> try
-    match ns_find_ls (Theory.get_namespace (get_theory uc)) x with
-      | { ls_args = [u;v]; ls_value = None } as ls when ty_equal u v -> ls
-      | ls ->
-          errorm ~loc:(qloc p) "%a is not a binary relation" Pretty.print_ls ls
-  with Not_found ->
-    errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
+let find_variant_ls uc p = try match uc_find_ls uc p with
+  | { ls_args = [u;v]; ls_value = None } as ls when ty_equal u v -> ls
+  | ls -> errorm ~loc:(qloc p) "%a is not a binary relation" Pretty.print_ls ls
+  with Not_found -> errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
 
-let find_global_vs uc p =
-  let x = Typing.string_list_of_qualid [] p in
-  try match ns_find_ps (get_namespace uc) x with
-    | PV pv -> Some pv.pv_vs
-    | _ -> None
+let find_global_vs uc p = try match uc_find_prgs uc p with
+  | PV pv -> Some pv.pv_vs
+  | _ -> None
   with Not_found -> None
 
 let rec dpattern denv ({ pat_loc = loc } as pp) = match pp.pat_desc with
@@ -659,46 +662,53 @@ let xpost lenv xq =
 let rec get_eff_expr lenv { pp_desc = d; pp_loc = loc } = match d with
   | Ptree.PPvar (Ptree.Qident {id=x}) when Mstr.mem x lenv.let_vars ->
       begin match Mstr.find x lenv.let_vars with
-        | LetV pv -> e_value pv
+        | LetV pv -> pv.pv_vtv
         | LetA _ -> errorm ~loc "%s must be a first-order value" x
       end
   | Ptree.PPvar p ->
-      let x = Typing.string_list_of_qualid [] p in
-      begin try match ns_find_ps (get_namespace lenv.mod_uc) x with
-        | PV pv -> e_value pv
+      begin try match uc_find_prgs lenv.mod_uc p with
+        | PV pv -> pv.pv_vtv
         | _ -> errorm ~loc:(qloc p) "%a is not a variable" print_qualid p
       with Not_found -> errorm ~loc "unbound variable %a" print_qualid p end
   | Ptree.PPapp (p, [le]) ->
-      let e = get_eff_expr lenv le in
-      let ity = (vtv_of_expr e).vtv_ity in
-      let x = Typing.string_list_of_qualid [] p in
-      let quit () =
-        errorm ~loc:(qloc p) "%a is not a projection symbol" print_qualid p in
-      begin try match ns_find_ps (get_namespace lenv.mod_uc) x with
-        | PL ({pl_args = [{vtv_ity = ta}]; pl_value = {vtv_ity = tr}} as pl) ->
-            let sbs = unify_loc le.pp_loc (ity_match ity_subst_empty) ta ity in
-            let res = try ity_full_inst sbs tr with Not_found -> quit () in
-            e_plapp pl [e] res
+      let vtv = get_eff_expr lenv le in
+      let quit () = errorm ~loc:le.pp_loc "This expression is not a record" in
+      let pjm = match vtv.vtv_ity.ity_node with
+        | Ityapp (its,_,_) ->
+            let pjl = match find_constructors (get_known lenv.mod_uc) its with
+              | (_,pjl)::_ -> pjl | _ -> quit () in
+            let add_pj m pj = match pj with
+              | Some { pl_ls = ls; pl_args = [vtva]; pl_value = vtvv } ->
+                  Mls.add ls (vtva.vtv_ity, vtvv) m
+              | Some _ -> assert false
+              | None -> m in
+            List.fold_left add_pj Mls.empty pjl
+        | Itypur (ts,_) ->
+            let kn = Theory.get_known (get_theory lenv.mod_uc) in
+            let pjl = match Decl.find_constructors kn ts with
+              | (_,pjl)::_ -> pjl | _ -> quit () in
+            let add_pj m pj = match pj with
+              | Some ({ ls_args = [tya]; ls_value = Some tyv } as ls) ->
+                  Mls.add ls (ity_of_ty tya, vty_value (ity_of_ty tyv)) m
+              | Some _ -> assert false
+              | None -> m in
+            List.fold_left add_pj Mls.empty pjl
         | _ -> quit ()
-      with Not_found -> try
-        let th = get_theory lenv.mod_uc in
-        match ns_find_ls (Theory.get_namespace th) x with
-        | { ls_args = [ta]; ls_value = Some tr } as ls ->
-            let sbs = ity_match ity_subst_empty (ity_of_ty ta) ity in
-            let res = try ity_full_inst sbs (ity_of_ty tr) with _ -> quit () in
-            e_lapp ls [e] res
-        | _ -> quit ()
-      with Not_found ->
-        errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
-      end
+      in
+      let itya, vtvv =
+        try Mls.find (uc_find_ls lenv.mod_uc p) pjm with Not_found ->
+          errorm ~loc:(qloc p) "%a is not a field name" print_qualid p in
+      let sbs = unify_loc loc (ity_match ity_subst_empty) itya vtv.vtv_ity in
+      let mut = Util.option_map (reg_full_inst sbs) vtvv.vtv_mut in
+      let ghost = vtv.vtv_ghost || vtvv.vtv_ghost in
+      vty_value ~ghost ?mut (ity_full_inst sbs vtvv.vtv_ity)
   | Ptree.PPcast (e,_) | Ptree.PPnamed (_,e) ->
       get_eff_expr lenv e
   | _ ->
       errorm ~loc "unsupported effect expression"
 
 let get_eff_regs lenv fn eff ghost le =
-  let e = get_eff_expr lenv le in
-  let vtv = vtv_of_expr e in
+  let vtv = get_eff_expr lenv le in
   let ghost = ghost || vtv.vtv_ghost in
   match vtv.vtv_mut, vtv.vtv_ity.ity_node with
   | Some reg, _ ->
@@ -1078,7 +1088,7 @@ let add_types uc tdl =
                     try
                       let pv = Hashtbl.find projs id.id in
                       let ty = pv.pv_vtv.vtv_ity in
-                      (* once we have ghost/mutable fields in algebraics,
+                      (* TODO: once we have ghost/mutable fields in algebraics,
                          don't forget to check here that they coincide, too *)
                       ignore (Loc.try3 id.id_loc ity_match sbs ty ity);
                       s, (pv, true)