Skip to content

[spectec] Formalise binding semantics for let premises (WIP) #2109

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 6 commits into
base: spectec.match
Choose a base branch
from
Open

[spectec] Formalise binding semantics for let premises (WIP) #2109

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
7844356
[spectec] Binding semantics for IL LET
rossberg Mar 11, 2026
3797f61
Scope let premises over clause/rule r.h.s.'s
rossberg Mar 11, 2026
106145c
Merge branch 'spectec.match' into spectec.let
rossberg Mar 12, 2026
2125953
Merge branch 'spectec.match' into spectec.let
rossberg Mar 12, 2026
f5279ea
Merge branch 'spectec.match' into spectec.let
rossberg Mar 12, 2026
dbbf5d8
Merge branch 'spectec.match' into spectec.let
rossberg Mar 12, 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
5 changes: 3 additions & 2 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 @@ -130,6 +130,7 @@ syntax exp =

syntax expfield = atom `= exp
syntax exppull = id `: typ `<- exp
syntax exppush = exp `-> id `: typ

syntax path =
| ROOT ;;
Expand Down Expand Up @@ -174,8 +175,8 @@ syntax prem =
| IF exp
| ELSE
| NOT prem
| LET exp `= exp ;; TODO: variables/quantifiers?
| ITER prem iter exppull*
| LET `{quant*} exp `= exp
| ITER prem iter exppull* exppush*

syntax dec =
| TYP id param* `= inst*
Expand Down
8 changes: 6 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 @@ -151,8 +151,12 @@ def $subst_prem(subst, prem) : prem
def $subst_prem(s, REL x a* `: e) = REL x $subst_arg(s, a)* `: $subst_exp(s, e)
def $subst_prem(s, IF e) = IF $subst_exp(s, e)
def $subst_prem(s, ELSE) = ELSE
def $subst_prem(s, LET e_1 `= e_2) = LET $subst_exp(s, e_1) `= $subst_exp(s, e_2) ;; TODO: avoid capture
def $subst_prem(s, ITER pr it (x `: t `<- e)*) = ITER $subst_prem(s, pr) $subst_iter(s, it) (x `: $subst_typ(s, t) `<- $subst_exp(s, e))* ;; TODO: avoid capture
def $subst_prem(s, LET `{q*} e_1 `= e_2) = LET `{$subst_param(s, q)*} $subst_exp(s, e_1) `= $subst_exp(s, e_2) ;; TODO: avoid capture
def $subst_prem(s, ITER pr it (x_1 `: t_1 `<- e_1)* (e_2 `-> x_2 `: t_2)*) = ;; TODO: avoid capture
ITER $subst_prem(s, pr) $subst_iter(s, it) (x_1 `: $subst_typ(s, t_1) `<- $subst_exp(s, e_1))* ($subst_exp(s, e_2) `-> x_2 `: $subst_typ(s, t_2))*

def $subst_exppush(subst, exppush) : exppush
def $subst_exppush(s, e `-> x `: t) = $subst_exp(s, e) `-> x `: $subst_typ(s, t)


def $subst_inst(subst, inst) : inst
Expand Down
84 changes: 55 additions & 29 deletions spectec/doc/semantics/il/5-reduction.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -80,6 +80,7 @@ rule Step_typ/ITER-ctx:

relation Step_iter: S |- iter ~> iter
relation Step_exppull: S |- exppull ~> exppull
relation Step_exppush: S |- exppush ~> exppush

rule Step_iter/SUP-ctx:
S |- SUP x e ~> SUP x e'
Expand All @@ -94,6 +95,14 @@ rule Step_exppull/ctx2:
S |- x `: t `<- e ~> x `: t `<- e'
-- Step_exp: S |- e ~> e'

rule Step_exppush/ctx1:
S |- e `-> x `: t ~> e' `-> x `: t
-- Step_exp: S |- e ~> e'

rule Step_exppush/ctx2:
S |- e `-> x `: t ~> e `-> x `: t'
-- Step_typ: S |- t ~> t'


;; Expressions

Expand Down Expand Up @@ -746,8 +755,8 @@ rule Step_clause/CLAUSE-ctx2:
-- Step_exp: S |- e ~> e'

rule Step_clause/CLAUSE-ctx3:
S |- CLAUSE `{q*} a* `= e `- pr* ~> CLAUSE `{q*} a* `= e `- pr'*
-- Step_prems: S |- pr* ~> pr'*
S |- CLAUSE `{q*} a* `= e `- pr* ~> CLAUSE `{q*} a* `= $subst_exp(s, e) `- pr'*
-- Step_prems: S |- pr* ~>_s pr'*


;; Arguments
Expand Down Expand Up @@ -785,7 +794,7 @@ rule Step_arg/TYP-ctx:
;; Premises

relation Reduce_prems: S |- prem* ~>* prem*
relation Step_prems: S |- prem* ~> prem*
relation Step_prems: S |- prem* ~>_subst prem*
relation Eq_prems: S |- prem* == prem*


Expand All @@ -801,74 +810,91 @@ rule Reduce_prems/refl:

rule Reduce_prems/step:
S |- pr* ~>* pr''*
-- Step_prems: S |- pr* ~> pr'*
-- Step_prems: S |- pr* ~>_s pr'*
-- Reduce_prems: S |- pr'* ~>* pr''*


rule Step_prems/ctx:
S |- pr* ~> pr*[0 : n] pr'_n* pr*[n : |pr*| - n]
-- Step_prems: S |- pr*[n] ~> pr'_n*
rule Step_prems/seq:
S |- pr_1* pr pr_2* ~>_s pr_1* pr'* $subst_prem(s, pr_2)*
-- Step_prems: S |- pr ~>_s pr'*


rule Step_prems/REL:
S |- REL x a* `: e ~> $subst_prem(s, pr)* (IF (CMP EQ $subst_exp(s, e') e))
S |- REL x a* `: e ~>_{} $subst_prem(s, pr)* (IF (CMP EQ $subst_exp(s, e') e))
-- if (x, p* `-> t `= rul*) <- S.REL
-- if (RULE `{q*} e' `- pr*) <- $subst_rule($args_for_params(a*, p*), rul)*
-- Ok_subst: $storeenv(S) |- s : q*
;; Note: non-computational rule

rule Step_prems/IF-ctx:
S |- IF e ~> IF e'
S |- IF e ~>_{} IF e'
-- Step_exp: S |- e ~> e'

rule Step_prems/IF-true:
S |- IF (BOOL true) ~> eps
S |- IF (BOOL true) ~>_{} eps

rule Step_prems/ELSE:
S |- ELSE ~> IF (BOOL true)
S |- ELSE ~>_{} IF (BOOL true)

rule Step_prems/LET-ctx:
S |- LET e_1 `= e_2 ~> LET e_1 `= e'_2
S |- LET `{q*} e_1 `= e_2 ~>_{} LET `{q*} e_1 `= e'_2
-- Step_exp: S |- e_2 ~> e'_2

rule Step_prems/LET:
S |- LET e `= e ~> eps
S |- LET `{(EXP x `: t)*} e_1 `= e_2 ~>_{EXP (x, e)*} eps
-- (if e = MATCH (EXP e_2) WITH (CLAUSE `{(EXP x `: t)*} (EXP e_1) `= (VAR x) `- eps))*

rule Step_prems/NOT-ctx:
S |- NOT pr ~> NOT pr'
-- Step_prems: S |- pr ~> pr'
S |- NOT pr ~>_{} NOT pr'
-- Step_prems: S |- pr ~>_s pr'

rule Step_prems/NOT-true:
S |- NOT (IF (BOOL true)) ~> IF (BOOL false)
S |- NOT (IF (BOOL true)) ~>_{} IF (BOOL false)

rule Step_prems/NOT-false:
S |- NOT (IF (BOOL false)) ~> IF (BOOL true)
S |- NOT (IF (BOOL false)) ~>_{} IF (BOOL true)

var ep : exppull
var eq : exppush

rule Step_prems/ITER-ctx1:
S |- ITER pr it ep* ~> ITER pr' it ep*
-- Step_prems: S |- pr ~> pr'
S |- ITER pr it ep* eq* ~>_{} ITER pr' it ep* $subst_exppush(s, eq)*
-- Step_prems: S |- pr ~>_s pr'

rule Step_prems/ITER-ctx2:
S |- ITER pr it ep* ~> ITER pr it' ep*
S |- ITER pr it ep* eq* ~>_{} ITER pr it' ep* eq*
-- Step_iter: S |- it ~> it'

rule Step_prems/ITER-ctx3:
S |- ITER pr it ep* ~> ITER pr it ep*[[n] = ep'_n]
S |- ITER pr it ep* eq* ~>_{} ITER pr it ep*[[n] = ep'_n] eq*
-- Step_exppull: S |- ep*[n] ~> ep'_n

rule Step_prems/ITER-ctx4:
S |- ITER pr it ep* eq* ~>_{} ITER pr it ep* eq*[[n] = eq'_n]
-- Step_exppush: S |- eq*[n] ~> eq'_n

rule Step_prems/ITER-QUEST:
S |- ITER pr QUEST (x `: t `<- OPT e?)* ~> $subst_prem({EXP (x, e')*}, pr)?
-- if e'*? = $transpose_(exp, e?*)
S |- ITER pr QUEST (x_1 `: t_1 `<- OPT e_1?)* (e_2 `-> x_2 `: t_2)* ~>_{EXP (x_2, OPT e''_2?)*}
$subst_prem({EXP (x_1, e'_1)*}, pr)?
-- if e'_1*? = $transpose_(exp, e_1?*)
-- if e'_2*? = $transpose_(exp, e''_2?*)
-- (if |e_1?| = |e''_2?|)*
-- (if e'_2 = e_2)*?

rule Step_prems/ITER-PLUS:
S |- ITER pr PLUS (x `: t `<- LIST e*)* ~> ITER pr STAR (x `: t `<- LIST e*)*
-- if |e**[0]| >= 1
S |- ITER pr PLUS (x_1 `: t_1 `<- LIST e_1*)* (e_2 `-> x_2 `: t_2)* ~>_{}
ITER pr STAR (x_1 `: t_1 `<- LIST e_1*)* (e_2 `-> x_2 `: t_2)*
-- if |e_1**[0]| >= 1

rule Step_prems/ITER-STAR:
S |- ITER pr STAR (x `: t `<- LIST e*)* ~> ITER pr (SUP y (NAT n)) (x `: t `<- LIST e*)*
-- if |e**[0]| = n
S |- ITER pr STAR (x_1 `: t_1 `<- LIST e_1*)* (e_2 `-> x_2 `: t_2)* ~>_{}
ITER pr (SUP y (NAT n)) (x_1 `: t_1 `<- LIST e_1*)* (e_2 `-> x_2 `: t_2)*
-- if |e_1**[0]| = n
;; TODO: y fresh

rule Step_prems/ITER-SUP:
S |- ITER pr (SUP y (NAT n)) (x `: t `<- LIST e^n)* ~> $subst_prem({EXP (x, e')* (y, NAT i)}, pr)^(i<n)
-- if e'*^n = $transpose_(exp, e^n*)
S |- ITER pr (SUP y (NAT n)) (x_1 `: t_1 `<- LIST e_1^n)* ~>_{EXP (x_2, LIST e''_2^n)*}
$subst_prem({EXP (x_1, e'_1)* (y, NAT i)}, pr)^(i<n)
-- if e'_1*^n = $transpose_(exp, e_1^n*)
-- if e'_2*^n = $transpose_(exp, e''_2^n*)
-- (if e'_2 = e_2)*^n
58 changes: 33 additions & 25 deletions spectec/doc/semantics/il/6-typing.spectec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -156,14 +156,14 @@ rule Ok_typfield:
E |- (a `: t `- `{q*} pr*) : OK
-- Ok_typ: E |- t : OK
-- Ok_params: E ++ $tupenv(t) |- q* : OK
-- Ok_prems: E ++ $tupenv(t) ++ $paramenv(q*) |- pr* : OK
-- Ok_prems: E ++ $tupenv(t) ++ $paramenv(q*) |- pr* : OK -| E'


rule Ok_typcase:
E |- (m `: t `- `{q*} pr*) : OK
-- Ok_typ: E |- t : OK
-- Ok_params: E ++ $tupenv(t) |- q* : OK
-- Ok_prems: E ++ $tupenv(t) ++ $paramenv(q*) |- pr* : OK
-- Ok_prems: E ++ $tupenv(t) ++ $paramenv(q*) |- pr* : OK -| E'


;; Iterators
Expand Down Expand Up @@ -487,42 +487,50 @@ rule Ok_sym/conv:

;; Premises

relation Ok_prem: E |- prem : OK
relation Ok_prems: E |- prem* : OK
relation Ok_prem: E |- prem : OK -| E
relation Ok_prems: E |- prem* : OK -| E


rule Ok_prems/eps:
E |- eps : OK -| {}

rule Ok_prems/cons:
E |- pr_1 pr* : OK -| E_1 ++ E'
-- Ok_prem: E |- pr_1 : OK -| E_1
-- Ok_prems: E ++ E_1 |- pr* : OK -| E'


rule Ok_prem/REL:
E |- REL x a* `: e : OK
E |- REL x a* `: e : OK -| {}
-- if (x, (p* `-> t `= rul*)) <- E.REL
-- Ok_args: E |- a* : p* => s
-- Ok_exp: E |- e : $subst_typ(s, t)

rule Ok_prem/IF:
E |- IF e : OK
E |- IF e : OK -| {}
-- Ok_exp: E |- e : BOOL

rule Ok_prem/ELSE:
E |- ELSE : OK
E |- ELSE : OK -| {}

rule Ok_prem/NOT:
E |- NOT pr : OK
-- Ok_prem: E |- pr : OK
E |- NOT pr : OK -| {}
-- Ok_prem: E |- pr : OK -| {}

rule Ok_prem/LET:
E |- LET e_1 `= e_2 : OK
-- Ok_exp: E |- e_1 : t
E |- LET `{q*} e_1 `= e_2 : OK -| $paramenv(q*)
-- Ok_exp: E ++ $paramenv(q*) |- e_1 : t
-- Ok_exp: E |- e_2 : t

rule Ok_prem/ITER:
E |- ITER pr it (x `: t `<- e)* : OK
E |- ITER pr it (x_1 `: t_1 `<- e_1)* (e_2 `-> x_2 `: t_2)* : OK -| {EXP (x_2, t_2)*}
-- Ok_iter: E |- it : it' -| E'
-- (Ok_typ: E |- t : OK)*
-- (Ok_exp: E |- e : ITER t it')*
-- Ok_prem: E ++ {EXP (x, t)*} ++ E' |- pr : OK


rule Ok_prems:
E |- prem* : OK
-- (Ok_prem: E |- prem : OK)*
-- (Ok_typ: E |- t_1 : OK)*
-- (Ok_exp: E |- e_1 : ITER t_1 it')*
-- Ok_prem: E ++ {EXP (x_1, t_1)*} ++ E' |- pr : OK -| E'
-- (Ok_typ: E |- t_2 : OK)*
-- (Eq_typ: E |- t_2 == ITER t'_2 it')*
-- (Ok_exp: E ++ E' |- e_2 : t'_2)*


;; Parameters and Arguments
Expand Down Expand Up @@ -644,25 +652,25 @@ rule Ok_rule:
E |- RULE `{q*} e `- pr* : t
-- Ok_params: E |- q* : OK
-- Ok_exp: E ++ $paramenv(q*) |- e : t
-- Ok_prems: E ++ $paramenv(q*) |- pr* : OK
-- Ok_prems: E ++ $paramenv(q*) |- pr* : OK -| E'

relation Ok_clause: E |- clause : param* -> typ

rule Ok_clause:
E |- CLAUSE `{q*} a* `= e `- pr* : p* -> t
-- Ok_params: E |- q* : OK
-- Ok_args: E ++ $paramenv(q*) |- a* : p* => s
-- Ok_exp: E ++ $paramenv(q*) |- e : t
-- Ok_prems: E ++ $paramenv(q*) |- pr* : OK
-- Ok_prems: E ++ $paramenv(q*) |- pr* : OK -| E'
-- Ok_exp: E ++ $paramenv(q*) ++ E' |- e : t

relation Ok_prod: E |- prod : typ

rule Ok_prod:
E |- PROD `{q*} g `=> e `- pr* : t
-- Ok_params: E |- q* : OK
-- Ok_sym: E ++ $paramenv(q*) |- g : t'
-- Ok_exp: E ++ $paramenv(q*) |- e : t
-- Ok_prems: E ++ $paramenv(q*) |- pr* : OK
-- Ok_prems: E ++ $paramenv(q*) |- pr* : OK -| E'
-- Ok_exp: E ++ $paramenv(q*) ++ E' |- e : t


;; Scripts
Expand Down