check for reference markers in illegal positions

Also, make let-functions with reference parameters
inhibit auto-dereference in logic.

src/mlw/dexpr.ml

@@ -559,7 +559,8 @@ let bl_type bl = List.map (fun (_,_,t) -> t) bl
 let pv_dref pv = attr_dref pv.pv_vs.vs_name.id_attrs
 
 let id_nref {pre_loc = loc; pre_attrs = attrs} =
-  if attr_dref attrs then Loc.errorm ?loc "illegal reference marker";
+  if attr_dref attrs then Loc.errorm ?loc
+    "reference markers are only admitted over program variables";
   false
 
 let id_dref id dity =

src/parser/parser.mly

@@ -183,6 +183,10 @@
     (* TODO: recognize and fail on core idents *)
     Some id
 
+  let lq_as_ref = function
+    | Qident {id_str = "ref"} -> true
+    | _ -> raise Error
+
   let error_param loc =
     Loc.errorm ~loc "cannot determine the type of the parameter"
 
@@ -453,19 +457,31 @@ abstract:
 | ABSTRACT          { Abstract }
 
 type_field:
-| attrs(lident_nq) cast
-  { { f_ident = $1; f_mutable = false; f_ghost = false;
-      f_pty = $2; f_loc = floc $startpos $endpos } }
-| field_modifiers attrs(lident_nq) cast
-  { { f_ident = $2; f_mutable = fst $1; f_ghost = snd $1;
-      f_pty = $3; f_loc = floc $startpos $endpos } }
-
-field_modifiers:
+| field_modifiers ref_amp_id cast
+  { let mut, ghs = $1 and rff, id = $2 in
+    let ty = if rff then PTref [$3] else $3 in
+    { f_ident = id; f_mutable = mut; f_ghost = ghs;
+      f_pty = ty; f_loc = floc $startpos $endpos } }
+
+%inline field_modifiers:
+| (* epsilon *) { false, false }
 | MUTABLE       { true,  false }
 | GHOST         { false, true  }
 | GHOST MUTABLE { true,  true  }
 | MUTABLE GHOST { true,  true  }
 
+(* we have to use lqualid instead of REF after field_modifiers
+   to avoid a conflict with ty. However, if the given lqualid
+   is not REF, then we want to fail as soon as possible: either
+   at AMP, if it occurs after the lqualid, or else at COLON. *)
+ref_amp_id:
+| lq_as_ref AMP attrs(lident_nq)  { $1, set_ref (set_ref $3) }
+| lqualid attrs(lident_nq)        { lq_as_ref $1, set_ref $2 }
+| AMP attrs(lident_nq)            { false, set_ref $2 }
+| attrs(lident_nq)                { false, $1 }
+
+lq_as_ref:  lqualid               { lq_as_ref $1 }
+
 type_case:
 | attrs(uident_nq) params { floc $startpos $endpos, $1, $2 }
 
@@ -597,7 +613,7 @@ binder:
 
 binder_vars:
 | binder_vars_head  { fst $1, match snd $1 with
-                        | [] -> Loc.error ~loc:(floc $endpos $endpos) Error
+                        | [] -> raise Error
                         | bl -> List.rev bl }
 | binder_vars_rest  { $1 }
 
@@ -607,7 +623,7 @@ binder_vars_rest:
       fst $1, List.rev_append (match snd $1 with
         | (l, Some id) :: bl ->
             (Loc.join l l2, Some (add_attr id $2)) :: bl
-        | _ -> Loc.error ~loc:l2 Error) $3 }
+        | _ -> error_loc l2) $3 }
 | binder_vars_head special_binder binder_var*
     { fst $1, List.rev_append (snd $1) ($2 :: $3) }
 | special_binder binder_var*
@@ -618,13 +634,13 @@ binder_vars_head:
     let of_id id = id.id_loc, binder_of_id id in
     let push acc = function
       | PTtyapp (Qident id, []) -> of_id id :: acc
-      | _ -> Loc.error ~loc:(floc $endpos $endpos) Error in
+      | _ -> raise Error in
     match $1 with
       | PTtyapp (Qident {id_str = "ref"}, l) ->
           true, List.fold_left push [] l
       | PTtyapp (Qident id, l) ->
           false, List.fold_left push [of_id id] l
-      | _ -> Loc.error ~loc:(floc $endpos $endpos) Error }
+      | _ -> raise Error }
 
 binder_var:
 | attrs(lident_nq)      { floc $startpos $endpos, Some $1 }

src/parser/typing.ml

@@ -146,12 +146,18 @@ let dty_of_opt ns = function
 
 (** Typing patterns, terms, and formulas *)
 
-let create_user_id {id_str = n; id_ats = attrs; id_loc = loc} =
+let create_user_prog_id {id_str = n; id_ats = attrs; id_loc = loc} =
   let get_attrs (attrs, loc) = function
     | ATstr attr -> Sattr.add attr attrs, loc | ATpos loc -> attrs, loc in
   let attrs, loc = List.fold_left get_attrs (Sattr.empty, loc) attrs in
   id_user ~attrs n loc
 
+let create_user_id id =
+  let id = create_user_prog_id id in
+  if Sattr.mem Pmodule.ref_attr id.pre_attrs then Loc.errorm ?loc:id.pre_loc
+    "reference markers are only admitted over program variables";
+  id
+
 let parse_record ~loc ns km get_val fl =
   let fl = List.map (fun (q,e) -> find_lsymbol_ns ns q, e) fl in
   let cs,pjl,flm = Loc.try2 ~loc parse_record km fl in
@@ -224,15 +230,41 @@ let mk_closure crcmap loc ls =
 
 let vs_dref vs = Sattr.mem Pmodule.ref_attr vs.vs_name.id_attrs
 
-let undereference dt =
-  let to_deref = function
-    | DTvar _ -> true (* needed for DEpure *)
-    | DTgvar vs -> vs_dref vs
-    | _ -> false in
-  match dt.dt_node with
-  | DTapp (ls, [dt])
-    when ls_equal ls ls_ref_proj && to_deref dt.dt_node -> dt
-  | _ -> Loc.errorm ?loc:dt.dt_loc "not a reference variable"
+let to_deref = function
+  | DTvar _ -> true (* needed for DEpure *)
+  | DTgvar vs -> vs_dref vs
+  | _ -> false
+
+let rec underef ({dt_loc = loc} as dt) = match dt.dt_node with
+  | DTuloc (dt,l) -> Dterm.dterm ?loc Coercion.empty (DTuloc (underef dt, l))
+  | DTattr (dt,a) -> Dterm.dterm ?loc Coercion.empty (DTattr (underef dt, a))
+  | DTcast (dt,_) -> underef dt (* already unified *)
+  | DTapp (ls, [dt]) when ls_equal ls ls_ref_proj && to_deref dt.dt_node -> dt
+  | _ -> raise Not_found
+
+let undereference dt = try underef dt with Not_found ->
+  Loc.errorm ?loc:dt.dt_loc "not a reference variable"
+
+let to_underef ls el e =
+  let rec down al el = match al, el with
+    | (_::al), (_::el) -> down al el
+    | a::_, [] when vs_dref a.pv_vs ->
+        (try underef e with Not_found -> e)
+    | _::_, [] -> e
+    | _ -> assert false in
+  match Expr.restore_rs ls with
+  | rs -> down rs.rs_cty.cty_args el
+  | exception Not_found -> e
+
+let dt_app ls el =
+  let rec apply al l el = match l, el with
+    | ({ty_node = Tyapp (ts,_)}::l), (e::el)
+      when ts_equal ts Pmodule.ts_ref ->
+        (* ls may be a let-function with ref params *)
+        apply (to_underef ls al e::al) l el
+    | (_::l), (e::el) -> apply (e::al) l el
+    | _ -> DTapp (ls, List.rev_append al el) in
+  apply [] ls.ls_args el
 
 (* track the use of labels *)
 let at_uses = Hstr.create 5
@@ -243,6 +275,10 @@ let rec dterm ns km crcmap gvars at denv {term_desc = desc; term_loc = loc} =
       DTfapp (Dterm.dterm crcmap ~loc e1, e2)) e el
   in
   let rec apply_ls loc ls al l el = match l, el with
+    | ({ty_node = Tyapp (ts,_)}::l), ((loc_e,e)::el)
+      when ts_equal ts Pmodule.ts_ref ->
+        (* ls may be a let-function with ref params *)
+        apply_ls loc ls ((loc_e, to_underef ls al e)::al) l el
     | (_::l), (e::el) -> apply_ls loc ls (e::al) l el
     | [], _ -> func_app (DTapp (ls, List.rev_map snd al)) el
     | _, [] -> func_app (mk_closure crcmap loc ls) (List.rev_append al el)
@@ -287,7 +323,7 @@ let rec dterm ns km crcmap gvars at denv {term_desc = desc; term_loc = loc} =
       qualid_app q []
   | Ptree.Tidapp (q, tl) ->
       let tl = List.map (dterm ns km crcmap gvars at denv) tl in
-      DTapp (find_lsymbol_ns ns q, tl)
+      dt_app (find_lsymbol_ns ns q) tl
   | Ptree.Tapply (e1, e2) ->
       unfold_app e1 (dterm ns km crcmap gvars at denv e2) []
   | Ptree.Ttuple tl ->
@@ -299,9 +335,9 @@ let rec dterm ns km crcmap gvars at denv {term_desc = desc; term_loc = loc} =
         if op.id_str = Ident.op_neq then
           let op = { op with id_str = Ident.op_equ } in
           let ls = find_lsymbol_ns ns (Qident op) in
-          DTnot (Dterm.dterm crcmap ~loc (DTapp (ls, [de1;de2])))
+          DTnot (Dterm.dterm crcmap ~loc (dt_app ls [de1;de2]))
         else
-          DTapp (find_lsymbol_ns ns (Qident op), [de1;de2]) in
+          dt_app (find_lsymbol_ns ns (Qident op)) [de1;de2] in
       let rec chain loc de1 op1 = function
         | { term_desc = Ptree.Tinfix (e2, op2, e3); term_loc = loc23 } ->
             let de2 = dterm ns km crcmap gvars at denv e2 in
@@ -540,7 +576,7 @@ let rec dpattern muc gh { pat_desc = desc; pat_loc = loc } =
     | Ptree.Pparen _ | Ptree.Pscope _
     | Ptree.Pghost _ -> assert false (* never *)
     | Ptree.Pwild -> DPwild
-    | Ptree.Pvar x -> DPvar (create_user_id x, gh)
+    | Ptree.Pvar x -> DPvar (create_user_prog_id x, gh)
     | Ptree.Papp (q,pl) ->
         DPapp (find_constructor muc q, List.map (dpattern muc gh) pl)
     | Ptree.Prec fl ->
@@ -551,9 +587,12 @@ let rec dpattern muc gh { pat_desc = desc; pat_loc = loc } =
         DPapp (cs,fl)
     | Ptree.Ptuple pl ->
         DPapp (rs_tuple (List.length pl), List.map (dpattern muc gh) pl)
-    | Ptree.Pcast (p,pty) -> DPcast (dpattern muc gh p, dity_of_pty muc pty)
-    | Ptree.Pas (p,x,g) -> DPas (dpattern muc gh p, create_user_id x, gh || g)
-    | Ptree.Por (p,q) -> DPor (dpattern muc gh p, dpattern muc gh q))
+    | Ptree.Pcast (p,pty) ->
+        DPcast (dpattern muc gh p, dity_of_pty muc pty)
+    | Ptree.Pas (p,x,g) ->
+        DPas (dpattern muc gh p, create_user_prog_id x, gh || g)
+    | Ptree.Por (p,q) ->
+        DPor (dpattern muc gh p, dpattern muc gh q))
 
 let dpattern muc pat = dpattern muc false pat
 
@@ -688,10 +727,10 @@ let dinvariant muc f lvm _xsm old = dpre muc f lvm old
 (* abstract values *)
 
 let dparam muc (_,id,gh,pty) =
-  Opt.map create_user_id id, gh, dity_of_pty muc pty
+  Opt.map create_user_prog_id id, gh, dity_of_pty muc pty
 
 let dbinder muc (_,id,gh,opt) =
-  Opt.map create_user_id id, gh, dity_of_opt muc opt
+  Opt.map create_user_prog_id id, gh, dity_of_opt muc opt
 
 (* expressions *)
 
@@ -868,7 +907,7 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
   | Ptree.Elet (id, gh, kind, e1, e2) ->
       let e1 = update_any kind e1 in
       let kind = local_kind kind in
-      let ld = create_user_id id, gh, kind, dexpr muc denv e1 in
+      let ld = create_user_prog_id id, gh, kind, dexpr muc denv e1 in
       DElet (ld, dexpr muc (denv_add_let denv ld) e2)
   | Ptree.Erec (fdl, e1) ->
       let update_kind (id, gh, k, bl, pty, msk, sp, e) =
@@ -949,7 +988,7 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
       let efrom = dexpr muc denv efrom in
       let eto = dexpr muc denv eto in
       let inv = dinvariant muc inv in
-      let id = create_user_id id in
+      let id = create_user_prog_id id in
       let denv = denv_add_for_index denv id efrom.de_dvty in
       DEfor (id, efrom, dir, eto, inv, dexpr muc denv e1)
   | Ptree.Eassign asl ->
@@ -1022,7 +1061,7 @@ and drec_defn muc denv fdl =
       let denv = denv_add_args denv bl in
       let dv = dvariant muc sp.sp_variant in
       dspec muc sp, dv, dexpr muc denv e in
-    create_user_id id, gh, kind, bl, dity, msk, pre in
+    create_user_prog_id id, gh, kind, bl, dity, msk, pre in
   Dexpr.drec_defn denv (List.map prep fdl)
 
 
@@ -1411,7 +1450,7 @@ let add_decl muc env file d =
       add_meta muc (lookup_meta id.id_str) (List.map convert al)
   | Ptree.Dlet (id, gh, kind, e) ->
       let e = update_any kind e in
-      let ld = create_user_id id, gh, kind, dexpr muc denv_empty e in
+      let ld = create_user_prog_id id, gh, kind, dexpr muc denv_empty e in
       add_pdecl ~vc muc (create_let_decl (let_defn ~keep_loc:true ld))
   | Ptree.Drec fdl ->
       let _, rd = drec_defn muc denv_empty fdl in