Dexpr: admit labels and exceptions on top of high-order expressions

src/mlw/dexpr.ml

@@ -1118,8 +1118,18 @@ let get_xs env = function
 
 let proxy_labels = Slab.singleton proxy_label
 
-type let_prexix =
-  | LD of let_defn
+type header =
+  | LS of let_defn
+  | LX of xsymbol
+  | LL of (let_defn * pvsymbol) Hpv.t
+
+let put_header e = function
+  | LS ld -> e_let_check e ld
+  | LX xs -> e_exn xs e
+  | LL ol -> Hpv.fold (fun _ (ld,_) e -> e_let ld e) ol e
+
+type let_prefix =
+  | LD of header
   | EA of expr
 
 let vl_of_mask id mask ity =
@@ -1168,7 +1178,7 @@ and try_cexp uloc env ({de_dvty = argl,res} as de0) lpl =
         let hd, vl = proxy_args ghost al lpl in
         let id = id_fresh ?loc:e.e_loc ~label:proxy_labels "o" in
         let ld, v = let_var ~ghost:(ghost || gh) id e in
-        ld::hd, v::vl
+        LS ld :: hd, v::vl
     | al, LD ld :: lpl ->
         let hd, vl = proxy_args ghost al lpl in
         ld::hd, vl
@@ -1209,7 +1219,7 @@ and try_cexp uloc env ({de_dvty = argl,res} as de0) lpl =
       let loc = Opt.get_def de0.de_loc uloc in
       let id = id_fresh ?loc ~label:proxy_labels "h" in
       let ld, s = let_sym id ~ghost:(env.ghs || env.lgh) c in
-      c_app s (LD ld :: lpl) in
+      c_app s (LD (LS ld) :: lpl) in
   match de0.de_node with
   | DEvar (n,_) -> c_app (get_rs env n) lpl
   | DEsym (RS s) -> c_app s lpl
@@ -1233,20 +1243,20 @@ and try_cexp uloc env ({de_dvty = argl,res} as de0) lpl =
       proxy (c_any (cty_of_spec env bl msk dsp dity))
   | DElet ((_,_,_,{de_dvty = ([],_)}) as dldf,de) ->
       let ld, env = var_defn uloc env dldf in
-      cexp uloc env de (LD ld :: lpl)
+      cexp uloc env de (LD (LS ld) :: lpl)
   | DElet (dldf,de) ->
       let ldl0, env = sym_defn uloc env dldf in
       let lpl0 = List.rev_map (fun ld -> LD ld) ldl0 in
       cexp uloc env de (List.rev_append lpl0 lpl)
   | DErec (drdf,de) ->
       let ld, env = rec_defn uloc env drdf in
-      cexp uloc env de (LD ld :: lpl)
-  | DEexn _ ->
-      Loc.errorm "Local exception declarations are not allowed \
-                  over higher-order expressions"
-  | DEmark _ ->
-      Loc.errorm "Label declarations are not allowed \
-                  over higher-order expressions"
+      cexp uloc env de (LD (LS ld) :: lpl)
+  | DEexn (id,dity,mask,de) ->
+      let xs = create_xsymbol id ~mask (ity_of_dity dity) in
+      cexp uloc (add_xsymbol env xs) de (LD (LX xs) :: lpl)
+  | DEmark (id,_,de) ->
+      let env, old = add_label env id.pre_name in
+      cexp uloc env de (LD (LL old) :: lpl)
   | DEsym _ | DEconst _ | DEnot _ | DEand _ | DEor _ | DEif _ | DEcase _
   | DEassign _ | DEwhile _ | DEfor _ | DEtry _ | DEraise _ | DEassert _
   | DEpure _ | DEabsurd | DEtrue | DEfalse -> assert false (* expr-only *)
@@ -1267,14 +1277,14 @@ and try_expr uloc env ({de_dvty = argl,res} as de0) =
   | DEvar _ | DEsym _ | DEls _ | 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 e_let_check e ldl
+      List.fold_left put_header e ldl
   | DElet ((_,_,_,{de_dvty = ([],_)}) as dldf,de) ->
       let ld, env = var_defn uloc env dldf in
       let e2 = expr uloc env de in
       e_let_check e2 ld
   | DElet (dldf,de) ->
       let ldl, env = sym_defn uloc env dldf in
-      List.fold_left e_let_check (expr uloc env de) ldl
+      List.fold_left put_header (expr uloc env de) ldl
   | DErec (drdf,de) ->
       let ld, env = rec_defn uloc env drdf in
       e_let_check (expr uloc env de) ld
@@ -1416,7 +1426,7 @@ and sym_defn uloc env (id,gh,kind,de) =
   let lgh = env.ghs || gh || kind = RKlemma in
   let cgh, ldl, c = cexp uloc {env with lgh = lgh} de [] in
   let ld, s = let_sym id ~ghost:(lgh || cgh) ~kind c in
-  ld::ldl, add_rsymbol env s
+  LS ld :: ldl, add_rsymbol env s
 
 and rec_defn uloc ({inr = inr} as env) {fds = dfdl} =
   let step1 env (id, gh, kind, bl, res, mask, dsp, dvl, de) =