WhyML: "{qualid}" for logical symbols and snapshotted variables

x.{f} is allowed and can be used for unary applications
M.{f} is not allowed, use {M.f} instead

src/mlw/dexpr.ml

@@ -330,10 +330,7 @@ let spec_ity hv hr frz ity =
     | Ityapp (s,tl,rl) -> app_map dity s tl rl in
   dity ity
 
-let specialize_pv {pv_ity = ity} =
-  spec_ity (Htv.create 3) (Hreg.create 3) (ity_freeze isb_empty ity) ity
-
-let specialize_xs {xs_ity = ity} =
+let specialize_single ity =
   spec_ity (Htv.create 3) (Hreg.create 3) (ity_freeze isb_empty ity) ity
 
 let specialize_rs {rs_cty = cty} =
@@ -413,7 +410,6 @@ type dexpr = {
 and dexpr_node =
   | DEvar of string * dvty
   | DEsym of prog_symbol
-  | DEls of lsymbol
   | DEconst of Number.constant * dity
   | DEapp of dexpr * dexpr
   | DEfun of dbinder list * dity * mask * dspec later * dexpr
@@ -434,6 +430,9 @@ and dexpr_node =
   | DEexn of preid * dity * mask * dexpr
   | DEassert of assertion_kind * term later
   | DEpure of term later * dity
+  | DEvar_pure of string * dvty
+  | DEpv_pure of pvsymbol
+  | DEls_pure of lsymbol
   | DEabsurd
   | DEtrue
   | DEfalse
@@ -525,7 +524,7 @@ let denv_add_let denv (id,_,_,({de_dvty = dvty} as de)) =
   if fst dvty = [] then denv_add_mono denv id dvty else
   let rec is_value de = match de.de_node with
     | DEghost de | DEuloc (de,_) | DElabel (de,_) -> is_value de
-    | DEvar _ | DEsym _ | DEls _ | DEfun _ | DEany _ -> true
+    | DEvar _ | DEsym _ | DEls_pure _ | DEfun _ | DEany _ -> true
     | _ -> false in
   if is_value de
   then denv_add_poly denv id dvty
@@ -555,6 +554,16 @@ let denv_get denv n =
 let denv_get_opt denv n =
   Opt.map (mk_node n) (Mstr.find_opt n denv.locals)
 
+let mk_node_pure n = function
+  | _, Some tvs, dvty -> DEvar_pure (n, specialize_scheme tvs dvty)
+  | _, None,     dvty -> DEvar_pure (n, dvty)
+
+let denv_get_pure denv n =
+  mk_node_pure n (Mstr.find_exn (Dterm.UnboundVar n) n denv.locals)
+
+let denv_get_pure_opt denv n =
+  Opt.map (mk_node_pure n) (Mstr.find_opt n denv.locals)
+
 exception UnboundExn of string
 
 let denv_get_exn denv n = Mstr.find_exn (UnboundExn n) n denv.excpts
@@ -682,15 +691,19 @@ let dpattern ?loc node =
   Loc.try1 ?loc dpat node
 
 let specialize_dxs = function
-  | DEgexn xs -> specialize_xs xs
+  | DEgexn xs -> specialize_single xs.xs_ity
   | DElexn (_,dity) -> dity
 
 let dexpr ?loc node =
   let get_dvty = function
     | DEvar (_,dvty) ->
         dvty
+    | DEvar_pure (_,dvty) ->
+        let dt = dity_fresh () in
+        dity_unify_asym dt (dity_of_dvty dvty);
+        [], dt
     | DEsym (PV pv) ->
-        [], specialize_pv pv
+        [], specialize_single pv.pv_ity
     | DEsym (RS rs) ->
         specialize_rs rs
     | DEsym (OO ss) ->
@@ -701,8 +714,10 @@ let dexpr ?loc node =
         | BinOp  -> [dt;dt], dt
         | BinRel -> [dt;dt], dity_bool
         | NoOver -> assert false end
-    | DEls ls ->
+    | DEls_pure ls ->
         specialize_ls ls
+    | DEpv_pure pv ->
+        [], specialize_single (ity_purify pv.pv_ity)
     | DEconst (_, ity) -> [],ity
     | DEapp ({de_dvty = (arg::argl, res)}, de2) ->
         dexpr_expected_type de2 arg;
@@ -1224,7 +1239,7 @@ and try_cexp uloc env ({de_dvty = argl,res} as de0) lpl =
   | DEvar (n,_) -> c_app (get_rs env n) lpl
   | DEsym (RS s) -> c_app s lpl
   | DEsym (OO s) -> c_oop s lpl
-  | DEls s -> c_pur s lpl
+  | DEls_pure s  -> c_pur s lpl
   | DEapp (de1,de2) ->
       let e2 = e_ghostify env.cgh (expr uloc env de2) in
       cexp uloc env de1 (EA e2 :: lpl)
@@ -1257,6 +1272,7 @@ and try_cexp uloc env ({de_dvty = argl,res} as de0) lpl =
   | DEmark (id,de) ->
       let env, old = add_label env id.pre_name in
       cexp uloc env de (LD (LL old) :: lpl)
+  | DEvar_pure _ | DEpv_pure _
   | DEsym _ | DEconst _ | DEnot _ | DEand _ | DEor _ | DEif _ | DEcase _
   | DEassign _ | DEwhile _ | DEfor _ | DEtry _ | DEraise _ | DEassert _
   | DEpure _ | DEabsurd | DEtrue | DEfalse -> assert false (* expr-only *)
@@ -1266,15 +1282,19 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
   match de0.de_node with
   | DEvar (n,_) when argl = [] ->
       e_var (get_pv env n)
+  | DEvar_pure (n,_) ->
+      e_pure (t_var (get_pv env n).pv_vs)
   | DEsym (PV v) ->
       e_var v
+  | DEpv_pure v ->
+      e_pure (t_var v.pv_vs)
   | DEconst (c,dity) ->
       e_const c (ity_of_dity dity)
   | DEapp ({de_dvty = ([],_)} as de1, de2) ->
       let e1 = expr uloc env de1 in
       let e2 = expr uloc env de2 in
       e_app rs_func_app [e1; e2] [] (ity_of_dity res)
-  | DEvar _ | DEsym _ | DEls _ | DEapp _ | DEfun _ | DEany _ ->
+  | DEvar _ | DEsym _ | DEls_pure _ | DEapp _ | DEfun _ | DEany _ ->
       let cgh,ldl,c = try_cexp uloc env de0 [] in
       let e = e_ghostify cgh (e_exec c) in
       List.fold_left put_header e ldl

src/mlw/dexpr.mli

@@ -103,7 +103,6 @@ type dexpr = private {
 and dexpr_node =
   | DEvar of string * dvty
   | DEsym of prog_symbol
-  | DEls of lsymbol
   | DEconst of Number.constant * dity
   | DEapp of dexpr * dexpr
   | DEfun of dbinder list * dity * mask * dspec later * dexpr
@@ -124,6 +123,9 @@ and dexpr_node =
   | DEexn of preid * dity * mask * dexpr
   | DEassert of assertion_kind * term later
   | DEpure of term later * dity
+  | DEvar_pure of string * dvty
+  | DEpv_pure of pvsymbol
+  | DEls_pure of lsymbol
   | DEabsurd
   | DEtrue
   | DEfalse
@@ -158,11 +160,12 @@ val denv_add_for_index : denv -> preid -> dvty -> denv
 val denv_add_exn : denv -> preid -> dity -> denv
 
 val denv_get : denv -> string -> dexpr_node (** raises UnboundVar *)
-
 val denv_get_opt : denv -> string -> dexpr_node option
 
-val denv_get_exn : denv -> string -> dxsymbol (** raises Not_found *)
+val denv_get_pure : denv -> string -> dexpr_node (** raises UnboundVar *)
+val denv_get_pure_opt : denv -> string -> dexpr_node option
 
+val denv_get_exn : denv -> string -> dxsymbol (** raises Not_found *)
 val denv_get_exn_opt : denv -> string -> dxsymbol option
 
 val denv_names : denv -> Sstr.t

src/mlw/expr.ml

@@ -1222,9 +1222,10 @@ let ambig_ls s =
 
 let ht_rs = Hrs.create 7 (* rec_rsym -> rec_sym *)
 
-let print_apply pri print s id fmt vl = match extract_op id, vl with
+let print_capp pri ({rs_name = id} as s) fmt vl =
+  match extract_op id, vl with
   | _, [] ->
-      print fmt s
+      print_rs fmt s
   | Some o, [t1] when tight_op o ->
       fprintf fmt (protect_on (pri > 7) "%s%a") o print_pv t1
   | Some o, [t1] when String.get id.id_string 0 = 'p' ->
@@ -1249,11 +1250,29 @@ let print_apply pri print s id fmt vl = match extract_op id, vl with
         print_pv t1 print_pv t2 print_pv t3
   | _, tl ->
       fprintf fmt (protect_on (pri > 5) "@[<hov 1>%a@ %a@]")
-        print s (Pp.print_list Pp.space print_pv) tl
-
-let print_capp pri s fmt vl = print_apply pri print_rs s s.rs_name fmt vl
-
-let print_cpur pri s fmt vl = print_apply pri print_ls s s.ls_name fmt vl
+        print_rs s (Pp.print_list Pp.space print_pv) tl
+
+let print_cpur pri ({ls_name = id} as s) fmt vl =
+  let op = match extract_op id, vl with
+    | Some o, [_] when tight_op o -> Some o
+    | Some o, [_] when String.get id.id_string 0 = 'p' -> Some (o ^ "_")
+    | Some o, [_;_] -> Some o
+    | _, [_;_] when id.id_string = "mixfix []" -> Some "[]"
+    | _, [_;_;_] when id.id_string = "mixfix [<-]" -> Some "[<-]"
+    | _, [_;_;_] when id.id_string = "mixfix []<-" -> Some "[]<-"
+    | _, [_;_] when id.id_string = "mixfix [_..]" -> Some "[_..]"
+    | _, [_;_] when id.id_string = "mixfix [.._]" -> Some "[.._]"
+    | _, [_;_;_] when id.id_string = "mixfix [_.._]" -> Some "[_.._]"
+    | _ -> None in
+  match op, vl with
+  | None, [] ->
+      fprintf fmt "{%a}" print_ls s
+  | None, tl ->
+      fprintf fmt (protect_on (pri > 5) "@[<hov 1>{%a}@ %a@]")
+        print_ls s (Pp.print_list Pp.space print_pv) tl
+  | Some o, tl ->
+      fprintf fmt (protect_on (pri > 5) "@[<hov 1>{(%s)}@ %a@]")
+        o (Pp.print_list Pp.space print_pv) tl
 
 let rec print_expr fmt e = print_lexpr 0 fmt e
 

src/parser/parser.mly

@@ -835,9 +835,14 @@ expr_block:
 | LEFTBRC field_list1(expr) RIGHTBRC                { Erecord $2 }
 | LEFTBRC expr_arg WITH field_list1(expr) RIGHTBRC  { Eupdate ($2, $4) }
 
+expr_pure:
+| LEFTBRC qualid RIGHTBRC                           { Eidpur $2 }
+
 expr_sub:
 | expr_block                                        { $1 }
+| expr_pure                                         { $1 }
 | uqualid DOT mk_expr(expr_block)                   { Escope ($1, $3) }
+| expr_dot DOT mk_expr(expr_pure)                   { Eapply ($3, $1) }
 | expr_dot DOT lqualid_rich                         { Eidapp ($3, [$1]) }
 | PURE LEFTBRC term RIGHTBRC                        { Epure $3 }
 | expr_arg LEFTSQ expr RIGHTSQ

src/parser/ptree.ml

@@ -141,6 +141,7 @@ and expr_desc =
   | Ematch of expr * (pattern * expr) list
   | Eabsurd
   | Epure of term
+  | Eidpur of qualid
   | Eraise of qualid * expr option
   | Eexn of ident * pty * Ity.mask * expr
   | Etry of expr * (qualid * pattern option * expr) list

src/parser/typing.ml

@@ -589,9 +589,7 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
       DEapp (Dexpr.dexpr ~loc e1, e2)) e el
   in
   let qualid_app loc q el =
-    let e = try DEsym (find_prog_symbol muc q) with
-      | _ -> DEls (find_lsymbol muc.muc_theory q) in
-    expr_app loc e el
+    expr_app loc (DEsym (find_prog_symbol muc q)) el
   in
   let qualid_app loc q el = match q with
     | Qident {id_str = n} ->
@@ -600,6 +598,19 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
         | None -> qualid_app loc q el)
     | _ -> qualid_app loc q el
   in
+  let qualid_app_pure loc q el =
+    let e = match find_global_pv muc q with
+      | None -> DEls_pure (find_lsymbol muc.muc_theory q)
+      | Some v -> DEpv_pure v in
+    expr_app loc e el
+  in
+  let qualid_app_pure loc q el = match q with
+    | Qident {id_str = n} ->
+        (match denv_get_pure_opt denv n with
+        | Some d -> expr_app loc d el
+        | None -> qualid_app_pure loc q el)
+    | _ -> qualid_app_pure loc q el
+  in
   let find_dxsymbol q = match q with
     | Qident {id_str = n} ->
         (try denv_get_exn denv n with _
@@ -609,6 +620,8 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
   Dexpr.dexpr ~loc begin match desc with
   | Ptree.Eident q ->
       qualid_app loc q []
+  | Ptree.Eidpur q ->
+      qualid_app_pure loc q []
   | Ptree.Eidapp (q, el) ->
       qualid_app loc q (List.map (dexpr muc denv) el)
   | Ptree.Eapply (e1, e2) ->