M.()

src/parser/parser.mly

@@ -574,13 +574,17 @@ term_dot_:
 | o = oppref ; a = term_dot { Tidapp (Qident o, [a]) }
 | term_sub_                 { $1 }
 
-term_sub_:
-| term_dot DOT lqualid_rich                         { Tidapp ($3,[$1]) }
+term_block:
 | LEFTPAR term RIGHTPAR                             { $2.term_desc }
 | LEFTPAR RIGHTPAR                                  { Ttuple [] }
 | LEFTPAR comma_list2(term) RIGHTPAR                { Ttuple $2 }
 | LEFTBRC field_list1(term) RIGHTBRC                { Trecord $2 }
 | LEFTBRC term_arg WITH field_list1(term) RIGHTBRC  { Tupdate ($2,$4) }
+
+term_sub_:
+| term_block                                        { $1 }
+| uqualid DOT mk_term(term_block)                   { Tscope ($1, $3) }
+| term_dot DOT lqualid_rich                         { Tidapp ($3,[$1]) }
 | term_arg LEFTSQ term RIGHTSQ
     { Tidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
 | term_arg LEFTSQ term LARROW term RIGHTSQ
@@ -803,7 +807,7 @@ expr_dot_:
 | o = oppref ; a = expr_dot { Eidapp (Qident o, [a]) }
 | expr_sub                  { $1 }
 
-expr_sub:
+expr_block:
 | BEGIN single_spec spec seq_expr END
     { Efun ([], None, Ity.MaskVisible, spec_union $2 $3, $4) }
 | BEGIN single_spec spec END
@@ -816,8 +820,12 @@ expr_sub:
 | LEFTPAR comma_list2(expr) RIGHTPAR                { Etuple $2 }
 | LEFTBRC field_list1(expr) RIGHTBRC                { Erecord $2 }
 | LEFTBRC expr_arg WITH field_list1(expr) RIGHTBRC  { Eupdate ($2, $4) }
-| PURE LEFTBRC term RIGHTBRC                        { Epure $3 }
+
+expr_sub:
+| expr_block                                        { $1 }
+| uqualid DOT mk_expr(expr_block)                   { Escope ($1, $3) }
 | expr_dot DOT lqualid_rich                         { Eidapp ($3, [$1]) }
+| PURE LEFTBRC term RIGHTBRC                        { Epure $3 }
 | expr_arg LEFTSQ expr RIGHTSQ
     { Eidapp (get_op $startpos($2) $endpos($2), [$1;$3]) }
 | expr_arg LEFTSQ expr LARROW expr RIGHTSQ

src/parser/ptree.ml

@@ -85,6 +85,7 @@ and term_desc =
   | Ttuple of term list
   | Trecord of (qualid * term) list
   | Tupdate of term * (qualid * term) list
+  | Tscope of qualid * term
   | Tat of term * ident
 
 (*s Program expressions *)
@@ -150,6 +151,7 @@ and expr_desc =
   | Ecast of expr * pty
   | Eghost of expr
   | Enamed of label * expr
+  | Escope of qualid * expr
 
 and fundef = ident * ghost * Expr.rs_kind *
   binder list * pty option * Ity.mask * spec * expr

src/parser/typing.ml

@@ -376,6 +376,10 @@ let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} =
       if re then d else mk_let tuc ~loc "q " e1 d
   | Ptree.Tat (e1, l) ->
       DTlabel (dterm tuc gvars (Some l.id_str) denv e1, Slab.empty)
+  | Ptree.Tscope (q, e1) ->
+      let tuc = Theory.open_scope tuc "dummy" in
+      let tuc = Theory.import_scope tuc (string_list_of_qualid q) in
+      DTlabel (dterm tuc gvars at denv e1, Slab.empty)
   | Ptree.Tnamed (Lpos uloc, e1) ->
       DTuloc (dterm tuc gvars at denv e1, uloc)
   | Ptree.Tnamed (Lstr lab, e1) ->
@@ -781,6 +785,10 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
       let id = create_user_id id in
       let denv = denv_add_exn denv id dity in
       DEmark (id, dity, dexpr muc denv e1)
+  | Ptree.Escope (q, e1) ->
+      let muc = open_scope muc "dummy" in
+      let muc = import_scope muc (string_list_of_qualid q) in
+      DElabel (dexpr muc denv e1, Slab.empty)
   | Ptree.Enamed (Lpos uloc, e1) ->
       DEuloc (dexpr muc denv e1, uloc)
   | Ptree.Enamed (Lstr lab, e1) ->