Change the notation for first-class module projections to handle poly…

…morphic fields

OCaml/Basics.v

@@ -5,7 +5,7 @@ Local Open Scope Z_scope.
 Import ListNotations.
 Set Implicit Arguments.
 
-Notation "record .[ field ]" := (field (projT2 record)) (at level 5).
+Notation "(| record |)" := (projT2 record).
 
 Module Primitive.
   Set Primitive Projections.

src/mixedPath.ml

@@ -79,6 +79,12 @@ let of_path
 let rec to_coq (path : t) : SmartPrint.t =
   match path with
   | Access (path, field_path_name, is_local) ->
-    to_coq path ^-^ !^ "." ^-^
-    (if is_local then parens else brakets) (PathName.to_coq field_path_name)
+    let path = to_coq path in
+    let path =
+      if is_local then
+        path
+      else
+        parens (!^ "|" ^-^ path ^-^ !^ "|") in
+    path ^-^ !^ "." ^-^
+    parens (PathName.to_coq field_path_name)
   | PathName path_name -> PathName.to_coq path_name

tests/first_class_modules.v

@@ -138,25 +138,26 @@ Module UsingTriple.
 End UsingTriple.
 
 Definition set_update {a : Set} (v : a) (b : bool) (Box : set a) : set a :=
-  let elt_ty := Box.[Boxed_set.elt_ty] in
-  let OPS := Box.[Boxed_set.OPS] in
+  let elt_ty := (|Box|).(Boxed_set.elt_ty) in
+  let OPS := (|Box|).(Boxed_set.OPS) in
   let boxed :=
     if b then
-      Box.[Boxed_set.OPS].(S.SET.add) v Box.[Boxed_set.boxed]
+      (|Box|).(Boxed_set.OPS).(S.SET.add) v (|Box|).(Boxed_set.boxed)
     else
-      Box.[Boxed_set.OPS].(S.SET.remove) v Box.[Boxed_set.boxed] in
+      (|Box|).(Boxed_set.OPS).(S.SET.remove) v (|Box|).(Boxed_set.boxed) in
   let size :=
-    let mem := Box.[Boxed_set.OPS].(S.SET.mem) v Box.[Boxed_set.boxed] in
+    let mem := (|Box|).(Boxed_set.OPS).(S.SET.mem) v (|Box|).(Boxed_set.boxed)
+      in
     if mem then
       if b then
-        Box.[Boxed_set.size]
+        (|Box|).(Boxed_set.size)
       else
-        Z.sub Box.[Boxed_set.size] 1
+        Z.sub (|Box|).(Boxed_set.size) 1
     else
       if b then
-        Z.add Box.[Boxed_set.size] 1
+        Z.add (|Box|).(Boxed_set.size) 1
       else
-        Box.[Boxed_set.size] in
+        (|Box|).(Boxed_set.size) in
   existT _ _
     {|
       Boxed_set.elt_ty := elt_ty;
@@ -165,10 +166,11 @@ Definition set_update {a : Set} (v : a) (b : bool) (Box : set a) : set a :=
       |}.
 
 Definition set_mem {elt : Set} (v : elt) (Box : set elt) : bool :=
-  Box.[Boxed_set.OPS].(S.SET.mem) v Box.[Boxed_set.boxed].
+  (|Box|).(Boxed_set.OPS).(S.SET.mem) v (|Box|).(Boxed_set.boxed).
 
 Definition set_fold {acc elt : Set} (f : elt -> acc -> acc) (Box : set elt)
-  : acc -> acc := Box.[Boxed_set.OPS].(S.SET.fold) f Box.[Boxed_set.boxed].
+  : acc -> acc :=
+  (|Box|).(Boxed_set.OPS).(S.SET.fold) f (|Box|).(Boxed_set.boxed).
 
 Module MAP.
   Record signature {key : Set} {t : Set -> Set} := {

tests/functor.v

@@ -35,7 +35,7 @@ End S.
 
 Parameter Make :
   forall (P : {t : _ & COMPARABLE.signature t}),
-    {_ : unit & S.signature P.[COMPARABLE.t]}.
+    {_ : unit & S.signature (|P|).(COMPARABLE.t)}.
 
 Parameter Char : {_ : unit & S.signature ascii}.