Skip to content

[spectec] Dynamically check side conditions on type fields/cases #2158

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
rossberg wants to merge 2 commits into
base: main
Choose a base branch
from
Open

[spectec] Dynamically check side conditions on type fields/cases #2158

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
a9b1393
[spectec] Dynamically check side conditions on type fields/cases
rossberg May 6, 2026
0f4085a
Add missing constraint on premises in values
rossberg May 6, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Binary file modified spectec/doc/example/output/NanoWasm.pdf
View file
Open in desktop
Binary file not shown.
30 changes: 17 additions & 13 deletions spectec/doc/semantics/il/1-syntax.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,11 @@ syntax deftyp =
syntax typbind = id `: typ
syntax typfield = atom `: typprems
syntax typcase = mixop `: typprems
syntax typprems = typ `- `{quant*} prem*
syntax typprems = typ `- quantprems
syntax quantprems = `{quant*} prem*

def $trueqpr : quantprems
def $trueqpr = `{eps} eps


;; Iterators
Expand Down Expand Up @@ -90,16 +94,16 @@ syntax cmpop = polycmpop | numcmpop


syntax val =
| num ;; num
| BOOL bool ;; bool
| TEXT text ;; text
| TUP val* ;; ( val* )
| INJ mixop val ;; mixop val
| OPT val? ;; val?
| LIST val* ;; [ val* ]
| STR valfield* ;; { valfield* }
| num ;; num
| BOOL bool ;; bool
| TEXT text ;; text
| TUP val* ;; ( val* )
| INJ typ mixop val `- quantprems? -- if quantprems? = $trueqpr ;; mixop val
| OPT val? ;; val?
| LIST val* ;; [ val* ]
| STR typ valfield* ;; { valfield* }

syntax valfield = atom `= val ;; atom `=` val
syntax valfield = atom `= val `- quantprems? -- if quantprems? = $trueqpr ;; atom `=` val


syntax exp =
Expand All @@ -111,11 +115,11 @@ syntax exp =
| BIN binop exp exp ;; exp binop exp
| CMP cmpop exp exp ;; exp cmpop exp
| TUP exp* ;; ( exp* )
| INJ mixop exp ;; mixop exp
| INJ typ mixop exp `- quantprems? ;; mixop exp (no prems = not yet checked)
| OPT exp? ;; exp?
| LIST exp* ;; [ exp* ]
| LIFT exp ;; exp : _? <: _*
| STR expfield* ;; { expfield* }
| STR typ expfield* ;; { expfield* }
| SEL exp nat ;; exp.n
| LEN exp ;; | exp |
| MEM exp exp ;; exp `<-` exp
Expand All @@ -129,7 +133,7 @@ syntax exp =
| SUB exp typ typ ;; exp : typ1 <: typ2
| MATCH arg* WITH clause* ;; `match` arg* `with` clause*

syntax expfield = atom `= exp
syntax expfield = atom `= exp `- quantprems? ;; atom `=` val (no prems = not yet checked)
syntax exppull = id `: typ `<- exp
syntax exppush = exp `-> id `: typ
syntax expprems = exp `- prem*
Expand Down
12 changes: 10 additions & 2 deletions spectec/doc/semantics/il/4-subst.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -202,11 +202,11 @@ def $subst_exp(s, UN op e) = UN op $subst_exp(s, e)
def $subst_exp(s, BIN op e_1 e_2) = BIN op $subst_exp(s, e_1) $subst_exp(s, e_2)
def $subst_exp(s, CMP op e_1 e_2) = CMP op $subst_exp(s, e_1) $subst_exp(s, e_2)
def $subst_exp(s, TUP e*) = TUP $subst_exp(s, e)*
def $subst_exp(s, INJ m e) = INJ m $subst_exp(s, e)
def $subst_exp(s, INJ t m e `- qpr?) = INJ $subst_typ(s, t) m $subst_exp(s, e) `- $subst_quantprems(s, qpr)?
def $subst_exp(s, OPT e?) = OPT $subst_exp(s, e)?
def $subst_exp(s, LIST e*) = LIST $subst_exp(s, e)*
def $subst_exp(s, LIFT e) = LIFT $subst_exp(s, e)
def $subst_exp(s, STR (a `= e)*) = STR (a `= $subst_exp(s, e))*
def $subst_exp(s, STR t (a `= e `- qpr?)*) = STR $subst_typ(s, t) (a `= $subst_exp(s, e) `- $subst_quantprems(s, qpr)?)*
def $subst_exp(s, SEL e n) = SEL $subst_exp(s, e) n
def $subst_exp(s, LEN e) = LEN $subst_exp(s, e)
def $subst_exp(s, MEM e_1 e_2) = MEM $subst_exp(s, e_1) $subst_exp(s, e_2)
Expand Down Expand Up @@ -279,6 +279,9 @@ def $subst_prem(s, ITER pr it ep* eq*) = ITER $subst_prem(s ++ s' ++ s'', pr') $
-- if (ep'*, s'') = $refresh_exppulls(ep*)
-- if (pr', s''') = $refresh_prem(pr)

def $subst_quantprems(subst, quantprems) : quantprems
def $subst_quantprems(s, `{q*} pr*) = `{$subst_param(s, q')*} $subst_prem(s ++ s', pr)*
-- if (q'*, s') = $refresh_params(q*)

def $subst_typprems(subst, typprems) : typprems
def $subst_typprems(s, t `- `{q*} pr*) = $subst_typ(s, t') `- `{$subst_param(s ++ s', q')*} $subst_prem(s ++ s' ++ s'', pr')*
Expand Down Expand Up @@ -324,6 +327,11 @@ def $args_for_params(a_1 a*, p_1 p*) = s ++ $args_for_params(a*, $subst_param(s,
-- if s = $arg_for_param(a_1, p_1)


def $tupsubst(exp, typ) : subst
def $tupsubst(e, TUP (x `: t)^n) = {EXP (x, SEL e i)^(i<n)}
def $tupsubst(e, t) = {} -- otherwise


;; Well-formedness

def $paramarg(param) : arg
Expand Down
Loading
Loading