[spectec] Define IL semantics for pattern matching

spectec/doc/semantics/il/0-aux.spectec

@@ -10,6 +10,15 @@ def $equiv_(syntax X, x_1*, x_2*) = true   -- (if x_1 <- x_2*)* -- (if x_2 <- x_
 def $equiv_(syntax X, x_1*, x_2*) = false  -- otherwise
 
 
+def $concat_(syntax X, X**) : X*  hint(show (++)%2)
+def $concat_(syntax X, eps) = eps
+def $concat_(syntax X, x_1* x**) = x_1* $concat_(X, x**)
+
+
 def $transpose_(syntax X, X**) : X**
 def $transpose_(syntax X, eps^n) = eps
 def $transpose_(syntax X, (x_1 x*)*) = x_1* $transpose_(X, x**)
+
+def $transposeq_(syntax X, X*?) : X?*
+def $transposeq_(syntax X, (eps)) = eps
+def $transposeq_(syntax X, (x_1 x*)?) = x_1? $transposeq_(X, x*?)

spectec/doc/semantics/il/1-syntax.spectec

@@ -23,6 +23,7 @@ syntax typ =
   | TUP typbind*       ;; (id : typ , ... , id : typ)
   | ITER typ iter      ;; typ iter
   | VAR id arg*        ;; typid(arg*)
+  | MATCH id arg* WITH inst*  ;; `match` typid(arg*) `with` inst*
 
 syntax deftyp =
   | ALIAS typ
@@ -40,7 +41,7 @@ syntax iter =
   | QUEST              ;; `?`
   | STAR               ;; `*`
   | PLUS               ;; `+`
-  | SUP id? exp        ;; `^` (id `<`)? exp
+  | SUP id exp         ;; `^` id `<` exp
 
 
 ;; Expressions
@@ -101,33 +102,34 @@ syntax valfield = atom `= val  ;; atom `=` val
 
 
 syntax exp =
-  | num                ;; num
-  | VAR id             ;; varid
-  | BOOL bool          ;; bool
-  | TEXT text          ;; text
-  | UN unop exp        ;; unop exp
-  | BIN binop exp exp  ;; exp binop exp
-  | CMP cmpop exp exp  ;; exp cmpop exp
-  | TUP exp*           ;; ( exp* )
-  | INJ mixop exp      ;; mixop exp
-  | OPT exp?           ;; exp?
-  | LIST exp*          ;; [ exp* ]
-  | LIFT exp           ;; exp : _? <: _*
-  | STR expfield*      ;; { expfield* }
-  | SEL exp nat        ;; exp.i
-  | LEN exp            ;; | exp |
-  | MEM exp exp        ;; exp `<-` exp
-  | CAT exp exp        ;; exp `++` exp
-  | ACC exp path       ;; exp[ path ]
-  | UPD exp path exp   ;; exp[ path = exp ]
-  | EXT exp path exp   ;; exp[ path =.. exp ]
-  | CALL id arg*       ;; defid( arg* )
+  | num                     ;; num
+  | VAR id                  ;; varid
+  | BOOL bool               ;; bool
+  | TEXT text               ;; text
+  | UN unop exp             ;; unop exp
+  | BIN binop exp exp       ;; exp binop exp
+  | CMP cmpop exp exp       ;; exp cmpop exp
+  | TUP exp*                ;; ( exp* )
+  | INJ mixop exp           ;; mixop exp
+  | OPT exp?                ;; exp?
+  | LIST exp*               ;; [ exp* ]
+  | LIFT exp                ;; exp : _? <: _*
+  | STR expfield*           ;; { expfield* }
+  | SEL exp nat             ;; exp.i
+  | LEN exp                 ;; | exp |
+  | MEM exp exp             ;; exp `<-` exp
+  | CAT exp exp             ;; exp `++` exp
+  | ACC exp path            ;; exp[ path ]
+  | UPD exp path exp        ;; exp[ path = exp ]
+  | EXT exp path exp        ;; exp[ path =.. exp ]
+  | CALL id arg*            ;; defid( arg* )
   | ITER exp iter exppull*  ;; exp iter{ expiter* }
   | CVT exp numtyp numtyp   ;; exp : typ1 <:> typ2
   | SUB exp typ typ         ;; exp : typ1 <: typ2
+  | MATCH arg* WITH clause* ;; `match` arg* `with` clause*
 
-syntax expfield = atom `= exp  ;; atom `=` exp
-syntax exppull = id `<- exp    ;; id `<-` exp
+syntax expfield = atom `= exp
+syntax exppull = id `: typ `<- exp
 
 syntax path =
   | ROOT               ;;
@@ -154,23 +156,24 @@ syntax sym =
 ;; Definitions
 
 syntax arg =
-  | EXP exp
   | TYP typ
+  | EXP exp
   | FUN id
   | GRAM sym
 
 syntax param =
-  | EXP id `: typ
   | TYP id
+  | EXP id `: typ
   | FUN id `: param* `-> typ
   | GRAM id `: param* `-> typ
 
 syntax quant = param
 
 syntax prem =
-  | RULE id arg* `: exp
+  | REL id arg* `: exp
   | IF exp
   | ELSE
+  | NOT prem
   | LET exp `= exp  ;; TODO: variables/quantifiers?
   | ITER prem iter exppull*
 

spectec/doc/semantics/il/3-primitives.spectec

@@ -17,6 +17,7 @@ def $boolbin(EQUIV, b_1, b_2) = b_1 <=> b_2
 
 def $iszero(num) : bool
 def $isone(num) : bool
+def $isneg(num) : bool
 
 def $iszero(NAT n) = (n = 0)
 def $iszero(INT i) = (i = 0)
@@ -28,6 +29,11 @@ def $isone(INT i) = (i = 1)
 def $isone(RAT q) = (q = 1)
 def $isone(REAL r) = (r = 1)
 
+def $isneg(NAT n) = false
+def $isneg(INT i) = (i < 0)
+def $isneg(RAT q) = (q < 0)
+def $isneg(REAL r) = (r < 0)
+
 
 def $numcvt(numtyp, num) : num  hint(partial)
 

spectec/doc/semantics/il/4-subst.spectec

@@ -10,6 +10,11 @@ syntax subst =
   }
 
 
+def $composesubsts(subst*) : subst  hint(show (++)%)
+def $composesubsts(eps) = {}
+def $composesubsts(s_1 s*) = s_1 ++ $composesubsts(s*)
+
+
 ;; Domain
 
 syntax dom =
@@ -54,6 +59,7 @@ def $subst_typ(s, VAR x a*) = VAR x $subst_arg(s, a)*  -- otherwise
 def $subst_typ(s, optyp) = optyp
 def $subst_typ(s, TUP (x `: t)*) = TUP (x `: $subst_typ(s, t))*  ;; TODO: avoid capture
 def $subst_typ(s, ITER t it) = ITER $subst_typ(s, t) $subst_iter(s, it)
+def $subst_typ(s, MATCH x a* WITH inst*) = MATCH x $subst_arg(s, a)*  WITH $subst_inst(s, inst)*
 
 def $subst_deftyp(subst, deftyp) : deftyp
 def $subst_deftyp(s, ALIAS t) = ALIAS $subst_typ(s, t)
@@ -67,7 +73,7 @@ def $subst_iter(subst, iter) : iter
 def $subst_iter(s, QUEST) = QUEST
 def $subst_iter(s, STAR) = STAR
 def $subst_iter(s, PLUS) = PLUS
-def $subst_iter(s, SUP x? e) = SUP x? $subst_exp(s, e)  ;; TODO: avoid capture
+def $subst_iter(s, SUP x e) = SUP x $subst_exp(s, e)  ;; TODO: avoid capture
 
 
 ;; Expressions
@@ -95,9 +101,10 @@ def $subst_exp(s, ACC e_1 p) = ACC $subst_exp(s, e_1) $subst_path(s, p)
 def $subst_exp(s, UPD e_1 p e_2) = UPD $subst_exp(s, e_1) $subst_path(s, p) $subst_exp(s, e_2)
 def $subst_exp(s, EXT e_1 p e_2) = EXT $subst_exp(s, e_1) $subst_path(s, p) $subst_exp(s, e_2)
 def $subst_exp(s, CALL x a*) = CALL $subst_fun(s, x) $subst_arg(s, a)*
-def $subst_exp(s, ITER e it (x `<- e')*) = ITER $subst_exp(s, e) $subst_iter(s, it) (x `<- $subst_exp(s, e'))*  ;; TODO: avoid capture
+def $subst_exp(s, ITER e it (x `: t `<- e')*) = ITER $subst_exp(s, e) $subst_iter(s, it) (x `: $subst_typ(s, t) `<- $subst_exp(s, e'))*  ;; TODO: avoid capture
 def $subst_exp(s, CVT e nt_1 nt_2) = CVT $subst_exp(s, e) nt_1 nt_2
 def $subst_exp(s, SUB e t_1 t_2) = SUB $subst_exp(s, e) $subst_typ(s, t_1) $subst_typ(s, t_2)
+def $subst_exp(s, MATCH a* WITH clause*) = MATCH $subst_arg(s, a)* WITH $subst_clause(s, clause)*
 
 def $subst_path(subst, path) : path
 def $subst_path(s, ROOT) = ROOT
@@ -120,39 +127,66 @@ def $subst_sym(s, SEQ g*) = SEQ $subst_sym(s, g)*
 def $subst_sym(s, ALT g*) = ALT $subst_sym(s, g)*
 def $subst_sym(s, RANGE g_1 g_2) = RANGE $subst_sym(s, g_1) $subst_sym(s, g_2)
 def $subst_sym(s, ATTR e g) = ATTR $subst_exp(s, e) $subst_sym(s, g)
-def $subst_sym(s, ITER g it (x `<- e)*) = ITER $subst_sym(s, g) $subst_iter(s, it) (x `<- $subst_exp(s, e))*  ;; TODO: avoid capture
+def $subst_sym(s, ITER g it (x `: t `<- e)*) = ITER $subst_sym(s, g) $subst_iter(s, it) (x `: $subst_typ(s, t) `<- $subst_exp(s, e))*  ;; TODO: avoid capture
 
 
 ;; Definitions
 
 def $subst_arg(subst, arg) : arg
-def $subst_arg(s, EXP e) = EXP $subst_exp(s, e)
 def $subst_arg(s, TYP t) = TYP $subst_typ(s, t)
+def $subst_arg(s, EXP e) = EXP $subst_exp(s, e)
 def $subst_arg(s, FUN x) = FUN $subst_fun(s, x)
 def $subst_arg(s, GRAM g) = GRAM $subst_sym(s, g)
 
 def $subst_param(subst, param) : param
-def $subst_param(s, EXP x `: t) = EXP x `: $subst_typ(s, t)
 def $subst_param(s, TYP x) = TYP x
+def $subst_param(s, EXP x `: t) = EXP x `: $subst_typ(s, t)
 def $subst_param(s, FUN x `: p* `-> t) = FUN x `: $subst_param(s, p)* `-> $subst_typ(s, t)   ;; TODO: avoid capture
 def $subst_param(s, GRAM x `: p* `-> t) = GRAM x `: $subst_param(s, p)* `-> $subst_typ(s, t) ;; TODO: avoid capture
 
 def $subst_quant(subst, quant) : quant
 def $subst_quant(s, q) = $subst_param(s, q)
 
 def $subst_prem(subst, prem) : prem
-def $subst_prem(s, RULE x a* `: e) = RULE x $subst_arg(s, a)* `: $subst_exp(s, e)
+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 `<- e)*) = ITER $subst_prem(s, pr) $subst_iter(s, it) (x `<- $subst_exp(s, e))*  ;; 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_inst(subst, inst) : inst
+def $subst_inst(s, INST `{q*} a* `= dt) = INST `{$subst_param(s, q)*} $subst_arg(s, a)* `= $subst_deftyp(s, dt)  ;; TODO: avoid capture
+
+def $subst_rule(subst, rul) : rul
+def $subst_rule(s, RULE `{q*} e `- pr*) = RULE `{$subst_param(s, q)*} $subst_exp(s, e) `- $subst_prem(s, pr)*  ;; TODO: avoid capture
+
+def $subst_clause(subst, clause) : clause
+def $subst_clause(s, CLAUSE `{q*} a* `= e `- pr*) = CLAUSE `{$subst_param(s, q)*} $subst_arg(s, a)* `= $subst_exp(s, e) `- $subst_prem(s, pr)*  ;; TODO: avoid capture
+
+def $subst_prod(subst, prod) : prod
+def $subst_prod(s, PROD `{q*} g `=> e `- pr*) = PROD `{$subst_param(s, q)*} $subst_sym(s, g) `=> $subst_exp(s, e) `- $subst_prem(s, pr)*  ;; TODO: avoid capture
+
+
+;; Constructing substitutions for parameters
+
+def $arg_for_param(arg, param) : subst
+def $arg_for_param(TYP t, TYP x) = {TYP (x, t)}
+def $arg_for_param(EXP e, EXP x `: t) = {EXP (x, e)}
+def $arg_for_param(FUN y, FUN x `: p* `-> t) = {FUN (x, y)}
+def $arg_for_param(GRAM g, GRAM x `: p* `-> t) = {GRAM (x, g)}
+
+def $args_for_params(arg*, param*) : subst
+def $args_for_params(eps, eps) = {}
+def $args_for_params(a_1 a*, p_1 p*) = s ++ $args_for_params(a*, $subst_param(s, p)*)
+  -- if s = $arg_for_param(a_1, p_1)
 
 
 ;; Well-formedness
 
 def $paramarg(param) : arg
-def $paramarg(EXP x `: t) = EXP (VAR x)
 def $paramarg(TYP x) = TYP (VAR x)
+def $paramarg(EXP x `: t) = EXP (VAR x)
 def $paramarg(FUN x `: p* `-> t) = FUN x
 def $paramarg(GRAM x `: p* `-> t) = GRAM (VAR x)