From 37e7bd7cf3eab6c2bf26167e126ac5a6bf08157d Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 16 Apr 2026 12:19:43 +0200 Subject: [PATCH 1/3] [spectec] Specify IL subsets --- spectec/doc/semantics/il/1-syntax.spectec | 68 ++++++++++++-------- spectec/doc/semantics/il/5-reduction.spectec | 4 +- 2 files changed, 44 insertions(+), 28 deletions(-) diff --git a/spectec/doc/semantics/il/1-syntax.spectec b/spectec/doc/semantics/il/1-syntax.spectec index 3fb61a8e09..7e8d36ba2b 100644 --- a/spectec/doc/semantics/il/1-syntax.spectec +++ b/spectec/doc/semantics/il/1-syntax.spectec @@ -1,3 +1,13 @@ +;; IL Subsets + +def $with_higher_order : bool +def $with_polymorphic_types : bool +def $with_dependent_types : bool +def $with_family_types : bool +def $with_grammars : bool +def $with_noncomputational : bool ;; semantic restriction + + ;; Identifiers syntax id = text @@ -23,7 +33,10 @@ syntax typ = | TUP typbind* ;; (id : typ , ... , id : typ) | ITER typ iter ;; typ iter | VAR id arg* ;; typid(arg*) + -- if arg* = eps \/ $with_polymorphic_types \/ $with_dependent_types | MATCH id arg* WITH inst* ;; `match` typid(arg*) `with` inst* + -- if arg* = eps \/ $with_polymorphic_types \/ $with_dependent_types + -- if |inst*| <= 1 \/ $with_family_types syntax deftyp = | ALIAS typ @@ -132,62 +145,65 @@ syntax expfield = atom `= exp syntax exppull = id `: typ `<- exp syntax path = - | ROOT ;; - | THE path ;; path! - | IDX path exp ;; path[ exp ] - | SLICE path exp exp ;; path[ exp : exp ] - | DOT path atom ;; path.atom - | PROJ path mixop ;; path!mixop + | ROOT ;; + | THE path ;; path! + | IDX path exp ;; path[ exp ] + | SLICE path exp exp ;; path[ exp : exp ] + | DOT path atom ;; path.atom + | PROJ path mixop ;; path!mixop ;; Grammars -syntax sym = - | VAR id arg* ;; gramid( arg* ) - | NUM nat ;; num - | TEXT text ;; text - | SEQ sym* ;; sym* - | ALT sym* ;; sym `|` sym - | RANGE sym sym ;; sym `|` `...` `|` sym - | ITER sym iter exppull* ;; sym iter{ exppull* } - | ATTR exp sym ;; exp `:` sym +syntax sym = ;; only used if $with_grammars + | VAR id arg* ;; gramid( arg* ) + -- if arg* = eps \/ $with_polymorphic_types \/ $with_dependent_types + | NUM nat ;; num + | TEXT text ;; text + | SEQ sym* ;; sym* + | ALT sym* ;; sym `|` sym + | RANGE sym sym ;; sym `|` `...` `|` sym + | ITER sym iter exppull* ;; sym iter{ exppull* } + | ATTR exp sym ;; exp `:` sym ;; Definitions syntax arg = - | TYP typ + | TYP typ -- if $with_polymorphic_types | EXP exp - | FUN id - | GRAM sym + | FUN id -- if $with_higher_order + | GRAM sym -- if $with_grammars syntax param = - | TYP id + | TYP id -- if $with_polymorphic_types | EXP id `: typ - | FUN id `: param* `-> typ - | GRAM id `: param* `-> typ + | FUN id `: param* `-> typ -- if $with_higher_order + | GRAM id `: param* `-> typ -- if $with_grammars syntax quant = param syntax prem = - | REL id arg* `: exp + | REL id arg* `: exp -- if $with_noncomputational | IF exp | ELSE | NOT prem - | LET exp `= exp ;; TODO: variables/quantifiers? + | LET exp `= exp ;; TODO: variables/quantifiers? | ITER prem iter exppull* syntax dec = - | TYP id param* `= inst* + | TYP id param* `= inst* -- if |inst*| <= 1 \/ $with_family_types | REL id param* `: typ `= rul* | FUN id param* `: typ `= clause* - | GRAM id param* `: typ `= prod* + | GRAM id param* `: typ `= prod* -- if $with_grammars | REC dec* syntax inst = INST `{quant*} arg* `=> deftyp + -- if arg* = (TYP typ)* \/ $with_dependent_types syntax rul = RULE `{quant*} exp `- prem* syntax clause = CLAUSE `{quant*} arg* `=> exp `- prem* -syntax prod = PROD `{quant*} sym `=> exp `- prem* +syntax prod = PROD `{quant*} sym `=> exp `- prem* + -- if $with_grammars ;; Scripts diff --git a/spectec/doc/semantics/il/5-reduction.spectec b/spectec/doc/semantics/il/5-reduction.spectec index 72ee64a5fa..990699ec3c 100644 --- a/spectec/doc/semantics/il/5-reduction.spectec +++ b/spectec/doc/semantics/il/5-reduction.spectec @@ -457,7 +457,7 @@ rule Step_exp/MATCH-guess: S |- MATCH a* WITH (CLAUSE `{q*} a'* `=> e `- pr*) clause* ~> MATCH a* WITH (CLAUSE `{} $subst_arg(s, a')* `=> e `- pr*) clause* -- Ok_subst: $storeenv(S) |- s : q* - ;; Note: non-computational rule + -- if $with_noncomputational rule Step_exp/MATCH-true: S |- MATCH eps WITH (CLAUSE `{} eps `=> e `- eps) clause* ~> e @@ -812,7 +812,7 @@ rule Step_prems/REL: -- 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 + -- if $with_noncomputational rule Step_prems/IF-ctx: S |- IF e ~> IF e' From 0730ba7b7d2fbc79b867d8cd4f48338eff3d31c7 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 21 Apr 2026 15:24:58 +0200 Subject: [PATCH 2/3] Tweak --- spectec/doc/semantics/il/1-syntax.spectec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spectec/doc/semantics/il/1-syntax.spectec b/spectec/doc/semantics/il/1-syntax.spectec index 7e8d36ba2b..e7d52be386 100644 --- a/spectec/doc/semantics/il/1-syntax.spectec +++ b/spectec/doc/semantics/il/1-syntax.spectec @@ -184,7 +184,7 @@ syntax param = syntax quant = param syntax prem = - | REL id arg* `: exp -- if $with_noncomputational + | REL id arg* `: exp ;; can only occur in relations | IF exp | ELSE | NOT prem From 8e35014d3eceec3467c8c1be86bed48af1f3b866 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 21 Apr 2026 15:30:05 +0200 Subject: [PATCH 3/3] Negation --- spectec/doc/semantics/il/1-syntax.spectec | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/spectec/doc/semantics/il/1-syntax.spectec b/spectec/doc/semantics/il/1-syntax.spectec index e7d52be386..add78f4535 100644 --- a/spectec/doc/semantics/il/1-syntax.spectec +++ b/spectec/doc/semantics/il/1-syntax.spectec @@ -4,6 +4,8 @@ def $with_higher_order : bool def $with_polymorphic_types : bool def $with_dependent_types : bool def $with_family_types : bool +def $with_negation : bool +def $with_else : bool def $with_grammars : bool def $with_noncomputational : bool ;; semantic restriction @@ -186,8 +188,8 @@ syntax quant = param syntax prem = | REL id arg* `: exp ;; can only occur in relations | IF exp - | ELSE - | NOT prem + | ELSE -- if $with_negation /\ $with_else + | NOT prem -- if $with_negation | LET exp `= exp ;; TODO: variables/quantifiers? | ITER prem iter exppull*