[spectec] Support record extension analogous to variant extension

Author: rossberg

spectec/doc/Language.md

@@ -236,22 +236,22 @@ not administrative ones.
 In addition to the basic grammar shown above,
 definitions of syntax variants can also be split into multiple _fragments_:
 ```
-def ::=
-  "syntax" varid subid* "=" deftyp-frag        syntax fragment definition
+deftyp ::= ...
+  deftyp-frag                                  syntax fragment definition
 
 deftyp-frag ::=
   "..."
   ("..." "|")? casetyp*"|" ("|" "...")?        variant fragment
 ```
 A variant with dots "..." at the end can be extended further by later variant definitions of the same name.
-This definition must start with dots, accordingly.
+These definitions must start with dots, accordingly.
 A variant is completed by a fragment without trailing dots.
 Each fragment must be named uniquely by amending the type name with a (possibly empty) list of hierarchical sub-identifiers of the form `x/y`,
 which can be used to refer to a fragment from splices.
 Currently, variant types defined in fragments cannot have parameters.
 
 **Example:**
-The instruction syntax above could be defined in two fragments:
+The instruction syntax above could be defined in multiple fragments:
 ```
 syntax instr/stack = DROP | ...
 syntax instr/arith = ... | CONST numtyp const | ...
@@ -297,6 +297,32 @@ syntax person = {NAME text, AGE nat, ADDRESS text}
 SpecTec provides special syntax for accessing values of record type,
 in particular, dot notation for field access.
 
+In addition to the basic grammar shown above,
+like [variant types](#variant-types),
+definitions of record syntax can also be split into multiple _fragments_:
+```
+deftyp-frag ::=
+  "{" "..." "}"
+  "{" ("..." ",")? fieldtyp*"," (...")? "}"        record fragment
+```
+A record with dots "..." at the end can be extended further by later record definitions of the same name.
+These definitions must start with dots, accordingly.
+A record is completed by a fragment without trailing dots.
+Each fragment must be named uniquely by amending the type name with a (possibly empty) list of hierarchical sub-identifiers of the form `x/y`,
+which can be used to refer to a fragment from splices.
+Currently, record types defined in fragments cannot have parameters.
+
+**Example:**
+The person record above could be defined in multiple fragments:
+```
+syntax person/name = { NAME text, ... }
+syntax person/age = { ..., AGE nat, ... }
+syntax person/address = { ..., ADDRESS text }
+```
+
+Semantically, a record definition split into fragments is equivalent to a combined one.
+Splitting a definition only has organisational purpose.
+
 
 ##### Premises
 

spectec/doc/example/output/NanoWasm.pdf

@@ -288,9 +288,15 @@ let env_typdef env tid t : typ list option =
   | VarT (id, _) ->
     map_append tid.it (Map.find id.it !(env.atoms)) env.atoms;
     Some [t]
-  | StrT tfs ->
+  | StrT (dots1, ts, tfs, _) ->
     iter_nl_list (env_typfield env tid) tfs;
-    Some []
+    iter_nl_list (fun t ->
+      match t.it with
+      | VarT (id, _) ->
+        map_append tid.it (Map.find id.it !(env.atoms)) env.atoms
+      | _ -> ()
+    ) ts;
+    if dots1 = Dots && ts = [] then None else Some (filter_nl ts)
   | CaseT (dots1, ts, tcs, _) ->
     iter_nl_list (env_typcase env tid) tcs;
     iter_nl_list (fun t ->
@@ -1168,11 +1174,21 @@ and render_nottyp env t : table =
     (string_of_region t.at) (El.Print.string_of_typ t);
   *)
   match t.it with
-  | StrT tfs ->
+  | StrT (dots1, ts, tfs, _dots2) ->
+    let render env = function
+      | `Dots -> render_dots Dots
+      | `Typ t -> render_nottyp env t
+      | `TypField tf -> render_typfield env tf
+    in
     [Row [Col (
       "\\{ " ^
       render_table env "@{}" ["l"; "l"] 0 0
-        (concat_table "" (render_nl_list env (`H, ", ") render_typfield tfs) [Row [Col " \\}"]])
+        (concat_table "" (render_nl_list env (`H, ", ") render (
+          (match dots1 with Dots -> [Elem `Dots] | NoDots -> []) @
+          map_nl_list (fun t -> `Typ t) ts @
+          map_nl_list (fun tf -> `TypField tf) tfs @
+          [] (* (match dots2 with Dots -> [Elem `Dots] | NoDots -> []) *)
+        )) [Row [Col " \\}"]])
     )]]
   | CaseT (dots1, ts, tcs, _dots2) ->
     let render env = function

spectec/src/backend-latex/render.ml

@@ -84,7 +84,7 @@ let env_hintdef ?(partial = false) hd =
 let env_typ id t =
   let open El.Ast in
   match t.it with
-  | El.Ast.StrT l ->
+  | El.Ast.StrT (_, _, l, _) ->
     List.iter (function
     | Nl -> ()
     | Elem (atom, _, hints) ->

spectec/src/backend-prose/prose_util.ml

@@ -46,7 +46,7 @@ and typ' =
   | TupT of typ list             (* `(` list2(typ, `,`) `)` *)
   | IterT of typ * iter          (* typ iter *)
   (* The forms below are only allowed in type definitions *)
-  | StrT of typfield nl_list     (* `{` list(typfield,`,`') `}` *)
+  | StrT of dots * typ nl_list * typfield nl_list * dots (* `{` list(`...`|typ|typfield, `,`) `}` *)
   | CaseT of dots * typ nl_list * typcase nl_list * dots (* `|` list(`...`|typ|typcase, `|`) *)
   | ConT of typcon               (* typ prem* *)
   | RangeT of typenum nl_list    (* exp `|` `...` `|` exp *)

spectec/src/el/ast.ml

@@ -71,7 +71,7 @@ let rec typ_of_exp e =
   | ParenE e1 -> ParenT (typ_of_exp e1)
   | TupE es -> TupT (List.map typ_of_exp es)
   | IterE (e1, iter) -> IterT (typ_of_exp e1, iter)
-  | StrE efs -> StrT (map_nl_list typfield_of_expfield efs)
+  | StrE efs -> StrT (NoDots, [], map_nl_list typfield_of_expfield efs, NoDots)
   | AtomE atom -> AtomT atom
   | SeqE es -> SeqT (List.map typ_of_exp es)
   | InfixE (e1, atom, e2) -> InfixT (typ_of_exp e1, atom, typ_of_exp e2)
@@ -90,12 +90,12 @@ let rec exp_of_typ t =
   | ParenT t1 -> ParenE (exp_of_typ t1)
   | TupT ts -> TupE (List.map exp_of_typ ts)
   | IterT (t1, iter) -> IterE (exp_of_typ t1, iter)
-  | StrT tfs -> StrE (map_nl_list expfield_of_typfield tfs)
+  | StrT (NoDots, [], tfs, NoDots) -> StrE (map_nl_list expfield_of_typfield tfs)
   | AtomT atom -> AtomE atom
   | SeqT ts -> SeqE (List.map exp_of_typ ts)
   | InfixT (t1, atom, t2) -> InfixE (exp_of_typ t1, atom, exp_of_typ t2)
   | BrackT (l, t1, r) -> BrackE (l, exp_of_typ t1, r)
-  | CaseT _ | ConT _ | RangeT _ -> error t.at "malformed expression"
+  | StrT _ | CaseT _ | ConT _ | RangeT _ -> error t.at "malformed expression"
   ) $ t.at
 
 and expfield_of_typfield (atom, (t, _prems), _) =

spectec/src/el/convert.ml

@@ -47,7 +47,9 @@ and eq_typ t1 t2 =
   | TupT ts1, TupT ts2 -> eq_list eq_typ ts1 ts2
   | IterT (t11, iter1), IterT (t21, iter2) ->
     eq_typ t11 t21 && eq_iter iter1 iter2
-  | StrT tfs1, StrT tfs2 -> eq_nl_list eq_typfield tfs1 tfs2
+  | StrT (dots11, ts1, tfs1, dots12), StrT (dots21, ts2, tfs2, dots22) ->
+    dots11 = dots21 && eq_nl_list eq_typ ts1 ts2 &&
+    eq_nl_list eq_typfield tfs1 tfs2 && dots12 = dots22
   | CaseT (dots11, ts1, tcs1, dots12), CaseT (dots21, ts2, tcs2, dots22) ->
     dots11 = dots21 && eq_nl_list eq_typ ts1 ts2 &&
     eq_nl_list eq_typcase tcs1 tcs2 && dots12 = dots22

spectec/src/el/eq.ml

@@ -102,8 +102,9 @@ and free_typ t =
   | ParenT t1 -> free_typ t1
   | TupT ts -> free_list free_typ ts
   | IterT (t1, iter) -> free_typ t1 + free_iter iter
-  | StrT tfs ->
-    free_nl_list (fun tf -> free_typfield tf - det_typfield tf) tfs
+  | StrT (_, ts, tfs, _) ->
+    free_nl_list free_typ ts +
+      free_nl_list (fun tf -> free_typfield tf - det_typfield tf) tfs
   | CaseT (_, ts, tcs, _) ->
     free_nl_list free_typ ts +
       free_nl_list (fun tc -> free_typcase tc - det_typcase tc) tcs

spectec/src/el/free.ml

@@ -100,7 +100,8 @@ and typ t =
   | ParenT t1 -> typ t1
   | TupT ts -> list typ ts
   | IterT (t1, it) -> typ t1; iter it
-  | StrT tfs -> nl_list typfield tfs
+  | StrT (dots1, ts, tfs, dots2) ->
+    dots dots1; nl_list typ ts; nl_list typfield tfs; dots dots2
   | CaseT (dots1, ts, tcs, dots2) ->
     dots dots1; nl_list typ ts; nl_list typcase tcs; dots dots2
   | ConT tc -> typcon tc
@@ -263,7 +264,7 @@ and clone_typ t =
   | SeqT ts -> SeqT (List.map clone_typ ts)
   | InfixT (t1, atom, t2) -> InfixT (clone_typ t1, clone_atom atom, clone_typ t2)
   | BrackT (atom1, t1, atom2) -> BrackT (clone_atom atom1, clone_typ t1, clone_atom atom2)
-  | StrT tfs -> StrT (Convert.map_nl_list clone_typfield tfs)
+  | StrT (dots1, ts, tfs, dots2) -> StrT (dots1, Convert.map_nl_list clone_typ ts, Convert.map_nl_list clone_typfield tfs, dots2)
   | CaseT (dots1, ts, tcs, dots2) -> CaseT (dots1, Convert.map_nl_list clone_typ ts, Convert.map_nl_list clone_typcase tcs, dots2)
   | ConT tc -> ConT (clone_typcon tc)
   | RangeT tes -> RangeT (Convert.map_nl_list clone_typenum tes)

spectec/src/el/iter.ml

@@ -78,10 +78,20 @@ and string_of_typ ?(short=false) t =
   | ParenT t -> "(" ^ string_of_typ t ^ ")"
   | TupT ts -> "(" ^ string_of_typs ", " ts ^ ")"
   | IterT (t1, iter) -> string_of_typ t1 ^ string_of_iter iter
-  | StrT tfs when short && List.length tfs > 3 ->
-    "{" ^ concat ", " (map_filter_nl_list (string_of_typfield ~short) (Lib.List.take 3 tfs)) ^ ", ..}"
-  | StrT tfs ->
-    "{" ^ concat ", " (map_filter_nl_list (string_of_typfield ~short) tfs) ^ "}"
+  | StrT (dots1, ts, tfs, dots2) when short && List.length tfs > 3 ->
+    "{" ^ concat ", " (
+      strings_of_dots dots1 @
+      map_filter_nl_list string_of_typ ts @
+      map_filter_nl_list (string_of_typfield ~short) (Lib.List.take 3 tfs) @
+      ".." :: strings_of_dots dots2
+    ) ^ "}"
+  | StrT (dots1, ts, tfs, dots2) ->
+    "{" ^ concat ", " (
+      strings_of_dots dots1 @
+      map_filter_nl_list string_of_typ ts @
+      map_filter_nl_list (string_of_typfield ~short) tfs @
+      strings_of_dots dots2
+    ) ^ "}"
   | CaseT (dots1, ts, tcs, dots2) when short && List.length tcs > 3 ->
     "| " ^ concat " | " (
       strings_of_dots dots1 @