Clean up concat

document/core/syntax/conventions.rst

@@ -79,7 +79,7 @@ When dealing with syntactic constructs the following notation is also used:
 * ${:s_1++s_2} denotes the sequence ${:s_1} concatenated with ${:s_2};
   this is equivalent to ${:s_1 s_2}, but sometimes used for clarity.
 
-* ${:$concat(s*)} denotes the flat sequence formed by concatenating all sequences ${:s_i} in ${:s*}.
+* ${:(++) s*} denotes the flat sequence formed by concatenating all sequences ${:s_i} in ${:s*}.
 
 Moreover, the following conventions are employed:
 
@@ -105,14 +105,14 @@ The following notation is adopted for manipulating such records:
 * ${:r[.FIELD = A]} denotes the same record as ${:r},
   except that the contents of the ${:FIELD} component is replaced with ${:A}.
 
-* ${:r[.FIELD =.. A^n]} denotes the same record as ${:r},
-  except that ${:A^n} is appended to the sequence of the ${:FIELD} component,
-  i.e, it is short for ${:r[.FIELD = r.FIELD A^n]}.
+* ${:r[.FIELD =++ A*]} denotes the same record as ${:r},
+  except that ${:A*} is appended to the sequence of the ${:FIELD} component,
+  i.e, it is short for ${:r[.FIELD = r.FIELD ++ A*]}.
 
 * ${:r_1++r_2} denotes the composition of two identically shaped records by concatenating each field of sequences point-wise:
 
   $${:
-    `{FIELD_ 1 A_1*, FIELD_ 2 A_2*, `...} ++ `{FIELD_ 1 B_1*, FIELD_ 2 B_2*, `...} = `{FIELD_ 1 A_1* B_1*, FIELD_ 2 A_2* B_2*, `...}
+    `{FIELD_ 1 A_1*, FIELD_ 2 A_2*, `...} ++ `{FIELD_ 1 B_1*, FIELD_ 2 B_2*, `...} = `{FIELD_ 1 (A_1* ++ B_1*), FIELD_ 2 (A_2* ++ B_2*), `...}
   }
 
 * ${:(++) r*} denotes the composition of a sequence of records, respectively; if the sequence is empty, then all fields of the resulting record are empty.

document/core/util/macros.def

@@ -104,7 +104,9 @@
 .. |subst| mathdef:: \xref{valid/conventions}{notation-subst}{\mathrel{\mathbf{:=}}}
 .. |slice| mathdef:: \xref{syntax/conventions}{notation-slice}{\mathrel{\mathbf{:}}}
 .. |with| mathdef:: \xref{syntax/conventions}{notation-replace}{\mathrel{\mbox{with}}}
-.. |concat| mathdef:: \xref{syntax/conventions}{notation-concat}{\F{concat}}
+.. |cat| mathdef:: \xref{syntax/conventions}{notation-concat}{\oplus}
+.. |bigcat| mathdef:: \xref{syntax/conventions}{notation-concat}{\bigoplus}
+.. |concat| mathdef:: \xref{syntax/conventions}{notation-concat}{\bigoplus}
 .. |compose| mathdef:: \xref{syntax/conventions}{notation-compose}{\oplus}
 .. |bigcompose| mathdef:: \xref{syntax/conventions}{notation-compose}{\bigoplus}
 

spectec/doc/Language.md

@@ -133,7 +133,7 @@ exp ::=
   exp "[" arith "]"                    list indexing
   exp "[" arith ":" arith "]"          list slicing
   exp "[" path "=" exp "]"             list update
-  exp "[" path "=.." exp "]"           list extension
+  exp "[" path "=++" exp "]"           list extension
   "{" list(atom exp, ",") "}"          record
   exp "." atom                         record access
   exp "," exp                          record extension

spectec/spec/wasm-1.0/9-module.watsup

@@ -34,7 +34,7 @@ def $mems(externval externval'*) = $mems(externval'*)
 ;; Definitions
 
 def $allocfunc(store, moduleinst, func) : (store, funcaddr)
-def $allocfunc(s, moduleinst, func) = (s[.FUNCS =.. fi], |s.FUNCS|)
+def $allocfunc(s, moduleinst, func) = (s[.FUNCS =++ fi], |s.FUNCS|)
   -- if fi = { TYPE moduleinst.TYPES[x], MODULE moduleinst, CODE func }
   -- if func = FUNC x local* expr
 
@@ -45,7 +45,7 @@ def $allocfuncs(s, moduleinst, func func'*) = (s_2, fa fa'*)
   -- if (s_2, fa'*) = $allocfuncs(s_1, moduleinst, func'*)
 
 def $allocglobal(store, globaltype, val) : (store, globaladdr)
-def $allocglobal(s, globaltype, val) = (s[.GLOBALS =.. gi], |s.GLOBALS|)
+def $allocglobal(s, globaltype, val) = (s[.GLOBALS =++ gi], |s.GLOBALS|)
   -- if gi = { TYPE globaltype, VALUE val }
 
 def $allocglobals(store, globaltype*, val*) : (store, globaladdr*)
@@ -55,7 +55,7 @@ def $allocglobals(s, globaltype globaltype'*, val val'*) = (s_2, ga ga'*)
   -- if (s_2, ga'*) = $allocglobals(s_1, globaltype'*, val'*)
 
 def $alloctable(store, tabletype) : (store, tableaddr)
-def $alloctable(s, `[i .. j]) = (s[.TABLES =.. ti], |s.TABLES|)
+def $alloctable(s, `[i .. j]) = (s[.TABLES =++ ti], |s.TABLES|)
   -- if ti = { TYPE `[i .. j], REFS eps^i }
 
 def $alloctables(store, tabletype*) : (store, tableaddr*)
@@ -65,7 +65,7 @@ def $alloctables(s, tabletype tabletype'*) = (s_2, ta ta'*)
   -- if (s_2, ta'*) = $alloctables(s_1, tabletype'*)
 
 def $allocmem(store, memtype) : (store, memaddr)
-def $allocmem(s, `[i .. j]) = (s[.MEMS =.. mi], |s.MEMS|)
+def $allocmem(s, `[i .. j]) = (s[.MEMS =++ mi], |s.MEMS|)
   -- if mi = { TYPE `[i .. j], BYTES 0^(i * $($(64 * $Ki))) }
 
 def $allocmems(store, memtype*) : (store, memaddr*)

spectec/spec/wasm-2.0/9-module.watsup

@@ -34,7 +34,7 @@ def $mems(externval externval'*) = $mems(externval'*)
 ;; Definitions
 
 def $allocfunc(store, moduleinst, func) : (store, funcaddr)
-def $allocfunc(s, moduleinst, func) = (s[.FUNCS =.. fi], |s.FUNCS|)
+def $allocfunc(s, moduleinst, func) = (s[.FUNCS =++ fi], |s.FUNCS|)
   -- if fi = { TYPE moduleinst.TYPES[x], MODULE moduleinst, CODE func }
   -- if func = FUNC x local* expr
 
@@ -45,7 +45,7 @@ def $allocfuncs(s, moduleinst, func func'*) = (s_2, fa fa'*)
   -- if (s_2, fa'*) = $allocfuncs(s_1, moduleinst, func'*)
 
 def $allocglobal(store, globaltype, val) : (store, globaladdr)
-def $allocglobal(s, globaltype, val) = (s[.GLOBALS =.. gi], |s.GLOBALS|)
+def $allocglobal(s, globaltype, val) = (s[.GLOBALS =++ gi], |s.GLOBALS|)
   -- if gi = { TYPE globaltype, VALUE val }
 
 def $allocglobals(store, globaltype*, val*) : (store, globaladdr*)
@@ -55,7 +55,7 @@ def $allocglobals(s, globaltype globaltype'*, val val'*) = (s_2, ga ga'*)
   -- if (s_2, ga'*) = $allocglobals(s_1, globaltype'*, val'*)
 
 def $alloctable(store, tabletype) : (store, tableaddr)
-def $alloctable(s, `[i .. j] rt) = (s[.TABLES =.. ti], |s.TABLES|)
+def $alloctable(s, `[i .. j] rt) = (s[.TABLES =++ ti], |s.TABLES|)
   -- if ti = { TYPE (`[i .. j] rt), REFS (REF.NULL rt)^i }
 
 def $alloctables(store, tabletype*) : (store, tableaddr*)
@@ -65,7 +65,7 @@ def $alloctables(s, tabletype tabletype'*) = (s_2, ta ta'*)
   -- if (s_2, ta'*) = $alloctables(s_1, tabletype'*)
 
 def $allocmem(store, memtype) : (store, memaddr)
-def $allocmem(s, `[i .. j] PAGE) = (s[.MEMS =.. mi], |s.MEMS|)
+def $allocmem(s, `[i .. j] PAGE) = (s[.MEMS =++ mi], |s.MEMS|)
   -- if mi = { TYPE (`[i .. j] PAGE), BYTES 0^(i * $($(64 * $Ki))) }
 
 def $allocmems(store, memtype*) : (store, memaddr*)
@@ -75,7 +75,7 @@ def $allocmems(s, memtype memtype'*) = (s_2, ma ma'*)
   -- if (s_2, ma'*) = $allocmems(s_1, memtype'*)
 
 def $allocelem(store, reftype, ref*) : (store, elemaddr)
-def $allocelem(s, rt, ref*) = (s[.ELEMS =.. ei], |s.ELEMS|)
+def $allocelem(s, rt, ref*) = (s[.ELEMS =++ ei], |s.ELEMS|)
   -- if ei = { TYPE rt, REFS ref* }
 
 def $allocelems(store, reftype*, (ref*)*) : (store, elemaddr*)
@@ -85,7 +85,7 @@ def $allocelems(s, rt rt'*, (ref*) (ref'*)*) = (s_2, ea ea'*)
   -- if (s_2, ea'*) = $allocelems(s_2, rt'*, (ref'*)*)
 
 def $allocdata(store, byte*) : (store, dataaddr)
-def $allocdata(s, byte*) = (s[.DATAS =.. di], |s.DATAS|)
+def $allocdata(s, byte*) = (s[.DATAS =++ di], |s.DATAS|)
   -- if di = { BYTES byte* }
 
 def $allocdatas(store, (byte*)*) : (store, dataaddr*)

spectec/spec/wasm-3.0/0-aux.watsup

@@ -30,14 +30,13 @@ def $min(0, j) = 0
 def $min(i, 0) = 0
 def $min($(i+1), $(j+1)) = $min(i, j)
 
-def $sum(nat*) : nat  hint(show %latex("\\Sigma\\,")#%)
+def $sum(nat*) : nat  hint(show (+) %) hint(macro none)
 def $sum(eps) = 0
 def $sum(n n'*) = $(n + $sum(n'*))
 
 
 ;; General sequence functions
 
-;; TODO(3, rossberg): replace with big (++)
-def $concat_(syntax X, (X*)*) : X*  hint(show $concat(%2))
+def $concat_(syntax X, (X*)*) : X*  hint(show (++) %2)
 def $concat_(syntax X, eps) = eps
 def $concat_(syntax X, (w*) (w'*)*) = w* $concat_(X, (w'*)*)

spectec/spec/wasm-3.0/5-runtime-aux.watsup

@@ -140,11 +140,11 @@ def $with_data((s; f), x, b*) = s[.DATAS[f.MODULE.DATAS[x]].BYTES = b*]; f
 def $with_struct((s; f), a, i, fv) = s[.STRUCTS[a].FIELDS[i] = fv]; f
 def $with_array((s; f), a, i, fv) = s[.ARRAYS[a].FIELDS[i] = fv]; f
 
-def $ext_structinst(state, structinst*) : state  hint(show %[.STRUCTS =.. %]) hint(macro "Z%")
-def $ext_arrayinst(state, arrayinst*) : state    hint(show %[.ARRAYS =.. %])  hint(macro "Z%")
+def $ext_structinst(state, structinst*) : state  hint(show %[.STRUCTS =++ %]) hint(macro "Z%")
+def $ext_arrayinst(state, arrayinst*) : state    hint(show %[.ARRAYS =++ %])  hint(macro "Z%")
 
-def $ext_structinst((s; f), si*) = s[.STRUCTS =.. si*]; f
-def $ext_arrayinst((s; f), ai*) = s[.ARRAYS =.. ai*]; f
+def $ext_structinst((s; f), si*) = s[.STRUCTS =++ si*]; f
+def $ext_arrayinst((s; f), ai*) = s[.ARRAYS =++ ai*]; f
 
 
 ;; Growing

spectec/spec/wasm-3.0/6-typing.watsup

@@ -1191,7 +1191,7 @@ rule Type_ok:
   C |- TYPE rectype : dt*
   -- if x = |C.TYPES|
   -- if dt* = $rolldt(x, rectype)
-  -- Rectype_ok: C[.TYPES =.. dt*] |- rectype : OK(x)
+  -- Rectype_ok: C ++ {TYPES dt*} |- rectype : OK(x)
 
 rule Local_ok/set:
   C |- LOCAL t : SET t
@@ -1334,12 +1334,12 @@ rule Types_ok/empty:
 rule Types_ok/cons:
   C |- type_1 type* : dt_1* dt*
   -- Type_ok: C |- type_1 : dt_1*
-  -- Types_ok: C[.TYPES =.. dt_1*] |- type* : dt*
+  -- Types_ok: C ++ {TYPES dt_1*} |- type* : dt*
 
 rule Globals_ok/empty:
   C |- eps : eps
 
 rule Globals_ok/cons:
   C |- global_1 global* : gt_1 gt*
   -- Global_ok: C |- global : gt_1
-  -- Globals_ok: C[.GLOBALS =.. gt_1] |- global* : gt*
+  -- Globals_ok: C ++ {GLOBALS gt_1} |- global* : gt*

spectec/src/backend-latex/render.ml

@@ -877,6 +877,11 @@ Printf.eprintf "[render_atom %s @ %s] id=%s def=%s macros: %s (%s)\n%!"
           | SqArrowStar -> "\\hookrightarrow^\\ast"
           | Cat -> "\\oplus"
           | Bar -> "\\mid"
+          | BigAnd -> "\\bigwedge"
+          | BigOr -> "\\bigvee"
+          | BigAdd -> "\\Sigma"
+          | BigMul -> "\\Pi"
+          | BigCat -> "\\bigoplus"
           | _ -> "\\" ^ Atom.name atom
     )
 
@@ -1046,7 +1051,7 @@ Printf.eprintf "[render %s:X @ %s] try expansion\n%!" (Source.string_of_region e
       "{}[" ^ render_path env p ^ " = " ^ render_exp env e2 ^ "]"
   | ExtE (e1, p, e2) ->
     render_exp env e1 ^
-      "{}[" ^ render_path env p ^ " = .." ^ render_exp env e2 ^ "]"
+      "{}[" ^ render_path env p ^ " \\mathrel{{=}{\\oplus}} " ^ render_exp env e2 ^ "]"
   | StrE efs ->
     "\\{ " ^
     "\\begin{array}[t]{@{}l@{}}\n" ^

spectec/src/backend-prose/render.ml

@@ -243,7 +243,7 @@ let render_al_binop = function
   | Al.Ast.AndOp -> "and"
   | Al.Ast.OrOp -> "or"
   | Al.Ast.ImplOp -> "implies"
-  | Al.Ast.EquivOp -> "is equivanlent to"
+  | Al.Ast.EquivOp -> "is equivalent to"
   | Al.Ast.AddOp -> "plus"
   | Al.Ast.SubOp -> "minus"
   | Al.Ast.MulOp -> "multiplied by"

spectec/src/el/atom.ml

@@ -39,6 +39,11 @@ and atom' =
   | Comma                        (* ``,` *)
   | Cat                          (* ``++` *)
   | Bar                          (* ``|` *)
+  | BigAnd                       (* `(/\)` *)
+  | BigOr                        (* `(\/)` *)
+  | BigAdd                       (* `(+)` *)
+  | BigMul                       (* `( * )` *)
+  | BigCat                       (* `(++)` *)
   | LParen | RParen              (* ``(` `)` *)
   | LBrack | RBrack              (* ``[` `]` *)
   | LBrace | RBrace              (* ``{` `}` *)
@@ -92,6 +97,11 @@ let to_string atom =
   | Comma -> ","
   | Cat -> "++"
   | Bar -> "|"
+  | BigAnd -> "(/\\)"
+  | BigOr -> "(\\/)"
+  | BigAdd -> "(+)"
+  | BigMul -> "(*)"
+  | BigCat -> "(++)"
   | LParen -> "("
   | LBrack -> "["
   | LBrace -> "{"
@@ -138,6 +148,11 @@ let name atom =
   | Comma -> "comma"              (* Latex: , *)
   | Cat -> "cat"                  (* Latex: \oplus *)
   | Bar -> "bar"                  (* Latex: | *)
+  | BigAnd -> "bigand"            (* Latex: \bigwedge *)
+  | BigOr -> "bigor"              (* Latex: \bigvee *)
+  | BigAdd -> "bigadd"            (* Latex: \Sigma *)
+  | BigMul -> "bigmul"            (* Latex: \Pi *)
+  | BigCat -> "bigcat"            (* Latex: \bigoplus *)
   | LParen -> "lparen"            (* Latex: brackets... *)
   | LBrack -> "lbrack"
   | LBrace -> "lbrace"

spectec/src/el/print.ml

@@ -150,7 +150,7 @@ and string_of_exp e =
       "[" ^ string_of_path p ^ " = " ^ string_of_exp e2 ^ "]"
   | ExtE (e1, p, e2) ->
     string_of_exp e1 ^
-      "[" ^ string_of_path p ^ " =.. " ^ string_of_exp e2 ^ "]"
+      "[" ^ string_of_path p ^ " =++ " ^ string_of_exp e2 ^ "]"
   | StrE efs -> "{" ^ concat ", " (map_filter_nl_list string_of_expfield efs) ^ "}"
   | DotE (e1, atom) -> string_of_exp e1 ^ "." ^ string_of_atom atom
   | CommaE (e1, e2) -> string_of_exp e1 ^ ", " ^ string_of_exp e2

spectec/src/frontend/elab.ml

@@ -399,23 +399,23 @@ let as_struct_typ phrase env dir t at : typfield list =
   | VarT (id, args) -> as_struct_typid' phrase env id args at
   | _ -> error_dir_typ env at phrase dir t "{...}"
 
-let rec as_comp_typid' phrase env dir id args at =
+let rec as_cat_typid' phrase env dir id args at =
   match as_defined_typid' env id args at with
-  | VarT (id', args'), `Alias -> as_comp_typid' phrase env dir id' args' at
+  | VarT (id', args'), `Alias -> as_cat_typid' phrase env dir id' args' at
   | IterT _, _ -> ()
   | StrT tfs, _ ->
     Convert.iter_nl_list (fun (_, (t, _), _) ->
-      as_comp_typ phrase env dir t at) tfs
+      as_cat_typ phrase env dir t at) tfs
   | _ ->
     error at (phrase ^ "'s type `" ^ string_of_typ (VarT (id, args) $ id.at) ^
-      "` is not composable")
+      "` is not concatenable")
 
-and as_comp_typ phrase env dir t at =
+and as_cat_typ phrase env dir t at =
   match expand env t with
-  | VarT (id, args) -> as_comp_typid' phrase env dir id args at
+  | VarT (id, args) -> as_cat_typid' phrase env dir id args at
   | IterT _ -> ()
   | _ ->
-    error at (phrase ^ "'s type `" ^ string_of_typ t ^ "` is not composable")
+    error at (phrase ^ "'s type `" ^ string_of_typ t ^ "` is not concatenable")
 
 let rec as_variant_typid' phrase env id args at : typcase list * dots =
   match as_defined_typid' env id args at with
@@ -970,7 +970,7 @@ and infer_exp' env e : Il.exp' * typ =
   | CommaE (e1, e2) ->
     let e1', t1 = infer_exp env e1 in
     let tfs = as_struct_typ "expression" env Infer t1 e1.at in
-    let _ = as_comp_typ "expression" env Infer t1 e.at in
+    let _ = as_cat_typ "expression" env Infer t1 e.at in
     (* TODO(4, rossberg): this is a bit of a hack, can we avoid it? *)
     (match e2.it with
     | SeqE ({it = AtomE atom; at; _} :: es2) ->
@@ -982,7 +982,7 @@ and infer_exp' env e : Il.exp' * typ =
     )
   | CatE (e1, e2) ->
     let e1', t1 = infer_exp env e1 in
-    let _ = as_comp_typ "expression" env Infer t1 e.at in
+    let _ = as_cat_typ "operand" env Infer t1 e.at in
     let e2' = elab_exp env e2 t1 in
     (if is_iter_typ env t1 then Il.CatE (e1', e2') else Il.CompE (e1', e2')), t1
   | MemE (e1, e2) ->
@@ -1111,7 +1111,7 @@ and elab_exp' env e t : Il.exp' =
   | CommaE (e1, e2) ->
     let e1' = elab_exp env e1 t in
     let tfs = as_struct_typ "expression" env Check t e1.at in
-    let _ = as_comp_typ "expression" env Check t e.at in
+    let _ = as_cat_typ "expression" env Check t e.at in
     (* TODO(4, rossberg): this is a bit of a hack, can we avoid it? *)
     (match e2.it with
     | SeqE ({it = AtomE atom; at; _} :: es2) ->
@@ -1122,7 +1122,7 @@ and elab_exp' env e t : Il.exp' =
     | _ -> error e.at "malformed comma operator"
     )
   | CatE (e1, e2) ->
-    let _ = as_comp_typ "expression" env Check t e.at in
+    let _ = as_cat_typ "expression" env Check t e.at in
     let e1' = elab_exp env e1 t in
     let e2' = elab_exp env e2 t in
     if is_iter_typ env t then Il.CatE (e1', e2') else Il.CompE (e1', e2')

spectec/src/frontend/lexer.mll

@@ -164,11 +164,16 @@ and token = parse
   | ":>" { SUP }
   | ":=" { ASSIGN }
   | "==" { EQUIV }
-  | "=.." { EQDOT2 }
+  | "=++" { EQCAT }
 
   | "~" { NOT }
   | "/\\" { AND }
   | "\\/" { OR }
+  | "(/\\)" { BIGAND }
+  | "(\\/)" { BIGOR }
+  | "(+)" { BIGADD }
+  | "(*)" { BIGMUL }
+  | "(++)" { BIGCAT }
 
   | "?" { QUEST }
   | "+" { PLUS }