dot-syntax for application

src/parser/parser.pre.mly

@@ -598,6 +598,24 @@ lexpr_arg:
    { mk_pp PPtrue }
 | FALSE
    { mk_pp PPfalse }
+| OPPREF lexpr_arg
+   { mk_pp (PPapp (Qident (mk_id (prefix $1) (loc_i 2)), [$2])) }
+| lexpr_sub
+   { $1 }
+;
+
+lexpr_dot:
+| lqualid_rich
+   { mk_pp (PPvar $1) }
+| OPPREF lexpr_dot
+   { mk_pp (PPapp (Qident (mk_id (prefix $1) (loc_i 2)), [$2])) }
+| lexpr_sub
+   { $1 }
+;
+
+lexpr_sub:
+| lexpr_dot DOT lqualid
+   { mk_pp (PPapp ($3, [$1])) }
 | LEFTPAR lexpr RIGHTPAR
    { $2 }
 | LEFTPAR RIGHTPAR
@@ -606,8 +624,6 @@ lexpr_arg:
    { mk_pp (PPtuple ($2 :: $4)) }
 | LEFTREC list1_field_value opt_semicolon RIGHTREC
    { mk_pp (PPrecord (List.rev $2)) }
-| OPPREF lexpr_arg
-   { mk_pp (PPapp (Qident (mk_id (prefix $1) (loc_i 2)), [$2])) }
 | lexpr_arg LEFTSQ lexpr RIGHTSQ
    { mk_pp (PPapp (Qident (mk_id (misfix "[]") (loc ())), [$1; $3])) }
 | lexpr_arg LEFTSQ lexpr OP1 lexpr RIGHTSQ
@@ -834,6 +850,11 @@ tqualid:
 | any_qualid DOT uident { Qdot ($1, $3) }
 ;
 
+lqualid_rich:
+| lident_rich             { Qident $1 }
+| uqualid DOT lident_rich { Qdot ($1, $3) }
+;
+
 qualid:
 | ident_rich             { Qident $1 }
 | uqualid DOT ident_rich { Qdot ($1, $3) }

tests/test-jcf.why

@@ -7,9 +7,11 @@ theory Records
   use import bool.Bool
   use import int.Int
 
-  type t 'a 'b = {| a : 'a; b : list 'b; |}
+  namespace import R
+    type t 'a 'b = {| a : 'a; b : list 'b; |}
+  end
 
-  goal g1 : let t = {| b = Cons True Nil; a = 1;  |} in a t = 1
+  goal g1 : let t = {| b = Cons True Nil; a = 1; |} in t.R.a = 1
 
 end