A bit more structure in definition files

spectec/spec/2-aux.watsup

@@ -1,3 +1,7 @@
+;;
+;; General definitions
+;;
+
 ;; General constants
 
 def $Ki : nat
@@ -12,7 +16,11 @@ def $min(i, 0) = 0
 def $min($(i+1), $(j+1)) = $min(i, j)
 
 
+;;
 ;; Auxiliary Definitions on Types
+;;
+
+;; Size
 
 ;; def |I n| = |F n| = |V n| = n        ;; ????
 
@@ -24,7 +32,10 @@ def $size(F64) = 64
 def $size(V128) = 128
 
 
+;;
 ;; Some notation tests
+;; TODO: remove
+;;
 
 def $test_sub_ATOM_22(n_3_ATOM_y) : nat
 def $test_sub_ATOM_22(n_3_ATOM_y) = 0

spectec/spec/3-typing.watsup

@@ -1,4 +1,6 @@
+;;
 ;; Contexts
+;;
 
 syntax context hint(desc "context") =
   { FUNC functype*, GLOBAL globaltype*, TABLE tabletype*, MEM memtype*,
@@ -9,7 +11,9 @@ var C : context
 
 
 
+;;
 ;; Types
+;;
 
 relation Limits_ok: |- limits : nat         hint(show "K-limits")
 relation Functype_ok: |- functype : OK      hint(show "K-func")
@@ -56,7 +60,11 @@ rule Externtype_ok/mem:
 
 
 
+;;
 ;; Subtyping
+;;
+
+;; Value types
 
 relation Valtype_sub: |- valtype <: valtype       hint(show "S")
 relation Resulttype_sub: |- valtype* <: valtype*  hint(show "S-result")
@@ -72,6 +80,8 @@ rule Resulttype_sub:
   -- (Valtype_sub: |- t_1 <: t_2)*
 
 
+;; External types
+
 relation Limits_sub: |- limits <: limits             hint(show "S-limits")
 relation Functype_sub: |- functype <: functype       hint(show "S-func")
 relation Globaltype_sub: |- globaltype <: globaltype hint(show "S-global")
@@ -118,18 +128,24 @@ rule Externtype_sub/mem:
 
 
 
+;;
 ;; Instructions
+;;
 
 relation Instr_ok: context |- instr : functype     hint(show "T")
 relation InstrSeq_ok: context |- instr* : functype hint(show "T*")
 relation Expr_ok: context |- expr : resulttype     hint(show "T-expr")
 
 
+;; Expressions
+
 rule Expr_ok:
   C |- instr* : t*
   -- InstrSeq_ok: C |- instr* : epsilon -> t*
 
 
+;; Instruction sequences
+
 rule InstrSeq_ok/empty:
   C |- epsilon : epsilon -> epsilon
 
@@ -150,6 +166,8 @@ rule InstrSeq_ok/frame:
   -- InstrSeq_ok: C |- instr* : t_1* -> t_2*
 
 
+;; Polymorphic instructions
+
 rule Instr_ok/unreachable:
   C |- UNREACHABLE : t_1* -> t_2*
 
@@ -169,6 +187,8 @@ rule Instr_ok/select-impl:
   -- if t' = numtype \/ t' = vectype
 
 
+;; Block instructions
+
 relation Blocktype_ok: context |- blocktype : functype hint(show "K-block")
 
 rule Blocktype_ok:
@@ -192,6 +212,8 @@ rule Instr_ok/if:
   -- InstrSeq_ok: C, LABEL (t_2*) |- instr_2* : t_1* -> t_2*
 
 
+;; Branch instructions
+
 rule Instr_ok/br:
   C |- BR l : t_1* t* -> t_2*
   -- if C.LABEL[l] = t*
@@ -205,6 +227,9 @@ rule Instr_ok/br_table:
   -- (Resulttype_sub: |- t* <: C.LABEL[l])*
   -- Resulttype_sub: |- t* <: C.LABEL[l']
 
+
+;; Function instructions
+
 rule Instr_ok/return:
   C |- RETURN : t_1* t* -> t_2*
   -- if C.RETURN = (t*)
@@ -219,6 +244,8 @@ rule Instr_ok/call_indirect:
   -- if ft = t_1* -> t_2*
 
 
+;; Numeric instructions
+
 rule Instr_ok/const:
   C |- CONST nt c_nt : epsilon -> nt
 
@@ -254,6 +281,8 @@ rule Instr_ok/convert-f:
   -- if fn_1 =/= fn_2
 
 
+;; Reference instructions
+
 rule Instr_ok/ref.null:
   C |- REF.NULL rt : epsilon -> rt
 
@@ -265,6 +294,8 @@ rule Instr_ok/ref.is_null:
   C |- REF.IS_NULL : rt -> I32
 
 
+;; Local instructions
+
 rule Instr_ok/local.get:
   C |- LOCAL.GET x : epsilon -> t
   -- if C.LOCAL[x] = t
@@ -278,6 +309,8 @@ rule Instr_ok/local.tee:
   -- if C.LOCAL[x] = t
 
 
+;; Global instructions
+
 rule Instr_ok/global.get:
   C |- GLOBAL.GET x : epsilon -> t
   -- if C.GLOBAL[x] = MUT? t
@@ -287,6 +320,8 @@ rule Instr_ok/global.set:
   -- if C.GLOBAL[x] = MUT t
 
 
+;; Table instructions
+
 rule Instr_ok/table.get:
   C |- TABLE.GET x : I32 -> rt
   -- if C.TABLE[x] = lim rt
@@ -322,6 +357,8 @@ rule Instr_ok/elem.drop:
   -- if C.ELEM[x] = rt
 
 
+;; Memory instructions
+
 rule Instr_ok/memory.size:
   C |- MEMORY.SIZE : epsilon -> I32
   -- if C.MEM[0] = mt
@@ -362,7 +399,9 @@ rule Instr_ok/store:
   -- if n? = epsilon \/ nt = in
 
 
+;;
 ;; Constant Expressions
+;;
 
 relation Instr_const: context |- instr CONST             hint(show "C-instr")
 relation Expr_const: context |- expr CONST               hint(show "C-expr")
@@ -392,7 +431,9 @@ rule Expr_ok_const:
   -- Expr_const: C |- expr CONST
 
 
+;;
 ;; Modules
+;;
 
 relation Func_ok: context |- func : functype         hint(show "T-func")
 relation Global_ok: context |- global : globaltype   hint(show "T-global")
@@ -405,6 +446,8 @@ relation Datamode_ok: context |- datamode : OK       hint(show "T-datamode")
 relation Start_ok: context |- start : OK             hint(show "T-start")
 
 
+;; Module definitions
+
 rule Func_ok:
   C |- FUNC ft t* expr : ft
   -- if ft = t_1* -> t_2*
@@ -452,6 +495,8 @@ rule Start_ok:
   -- if C.FUNC[x] = epsilon -> epsilon
 
 
+;; Module im/exports
+
 relation Import_ok: context |- import : externtype        hint(show "T-import")
 relation Export_ok: context |- export : externtype        hint(show "T-export")
 relation Externuse_ok: context |- externuse : externtype  hint(show "T-externuse")
@@ -481,6 +526,8 @@ rule Externuse_ok/mem:
   -- if C.MEM[x] = mt
 
 
+;; Modules proper
+
 relation Module_ok: |- module : OK      hint(show "T-module")
 
 rule Module_ok:

spectec/spec/4-runtime.watsup

@@ -1,4 +1,6 @@
+;;
 ;; Addresses
+;;
 
 syntax addr hint(desc "address") = nat
 syntax funcaddr hint(desc "function address") = addr
@@ -19,7 +21,11 @@ var ea : elemaddr
 var da : dataaddr
 
 
+;;
 ;; Values
+;;
+
+;; Basic values
 
 syntax num hint(desc "number") =
   | CONST numtype c_numtype
@@ -35,12 +41,17 @@ var r : ref
 var v : val
 var res : result
 
+
+;; External values
+
 syntax externval hint(desc "external value") =
   | FUNC funcaddr | GLOBAL globaladdr | TABLE tableaddr | MEM memaddr
 
 var xv : externval
 
 
+;; Auxiliary definition: default values
+
 def $default_(valtype) : val  hint(partial)
 def $default_(I32) = (CONST I32 0)
 def $default_(I64) = (CONST I64 0)
@@ -50,7 +61,11 @@ def $default_(FUNCREF) = (REF.NULL FUNCREF)
 def $default_(EXTERNREF) = (REF.NULL EXTERNREF) ;; TODO: All reference types should be caught by one pattern.
 
 
+;;
 ;; Configurations
+;;
+
+;; Instances
 
 syntax funcinst hint(desc "function instance") =
   { MODULE moduleinst,
@@ -73,14 +88,6 @@ syntax exportinst hint(desc "export instance") =
   { NAME name,
     VALUE externval }
 
-syntax store hint(desc "store") =
-  { FUNC funcinst*,
-    GLOBAL globalinst*,
-    TABLE tableinst*,
-    MEM meminst*,
-    ELEM eleminst*,
-    DATA datainst* }
-
 syntax moduleinst hint(desc "module instance") =
   { FUNC funcaddr*,
     GLOBAL globaladdr*,
@@ -90,27 +97,39 @@ syntax moduleinst hint(desc "module instance") =
     DATA dataaddr*,
     EXPORT exportinst* }
 
+var m : moduleinst
+var fi : funcinst
+var gi : globalinst
+var ti : tableinst
+var mi : meminst
+var ei : eleminst
+var di : datainst
+var xi : exportinst
+
+
+;; Configurations proper
+
+syntax store hint(desc "store") =
+  { FUNC funcinst*,
+    GLOBAL globalinst*,
+    TABLE tableinst*,
+    MEM meminst*,
+    ELEM eleminst*,
+    DATA datainst* }
+
 syntax frame hint(desc "frame") =
   { LOCAL val*,
     MODULE moduleinst }
+
 syntax state hint(desc "state") = store; frame
 syntax config hint(desc "configuration") = state; admininstr*
 
 var s : store
 var f : frame
 var z : state
 
-var m : moduleinst
-var fi : funcinst
-var gi : globalinst
-var ti : tableinst
-var mi : meminst
-var ei : eleminst
-var di : datainst
-var xi : exportinst
 
-
-;; Auxiliary notation
+;; Auxiliary notation: short-hands
 
 def $funcaddr(state) : funcaddr*  hint(show %.MODULE.FUNC)
 def $funcaddr((s; f)) = f.MODULE.FUNC
@@ -164,6 +183,9 @@ def $with_meminst((s; f), x, mi) = s[.MEM[f.MODULE.MEM[x]] = mi]; f
 def $with_elem((s; f), x, r*) = s[.ELEM[f.MODULE.ELEM[x]].ELEM = r*]; f
 def $with_data((s; f), x, b*) = s[.DATA[f.MODULE.DATA[x]].DATA = b*]; f
 
+
+;; Auxiliary definitions: Growing store objects
+
 def $grow_table(tableinst, nat, ref) : tableinst hint(partial)
 def $grow_memory(meminst, nat) : meminst hint(partial)
 
@@ -172,13 +194,17 @@ def $grow_table(ti, n, r) = ti'
   -- if i' = $(|r'*| + n)
   -- if ti' = { TYPE `[i' .. j] rt, ELEM r'* r^n }
   -- Tabletype_ok: |- ti'.TYPE : OK
+
 def $grow_memory(mi, n) = mi'
   -- if mi = { TYPE (`[i .. j] I8), DATA b* }
   -- if i' = $(|b*| / (64 * $Ki) + n)
   -- if mi' = { TYPE (`[i' .. j] I8), DATA b* 0^(n * 64 * $Ki) }
   -- Memtype_ok: |- mi'.TYPE : OK
 
+
+;;
 ;; Administrative Instructions
+;;
 
 syntax admininstr hint(show instr) hint(desc "administrative instruction") =
   | instr