After type-checking, SpecTec converts the input specification into a more explicit internal representation called the IL (internal language). The abstract syntax tree of the IL can be printed in an easily machine-readable S-expression format by invoking SpecTec in AST mode.
The structure of the IL is described by the following grammar. See the description of the SpecTec language for details on the constructs.
bool ::= "true" | "false" text ::= """ char* """ id ::= text mixop ::= text sign ::= "+" | "-" nat ::= digit+ int ::= sign nat rat ::= sign? nat "/" nat real ::= sign? nat "." nat num ::= "nat" nat | "int" int | "rat" rat | "real" real
Mixfix operators (mixop) are constructed by the frontend from the notation used in definitions of types or relations. Essentially, they are a concatenation of the atom names occurring, with interleaving % indicating the position of operands or nested expressions. For example, the notation defined by the relation
relation Expr_ok: context |- exp : typ
will be represented by the mixfix operator "%|-%:%", applied to a triple of arguments.
unop ::= "not" | "plus" | "minus" | "plusminus" | "minusplus" binop ::= "and" | "or" | "impl" | "equiv" | "add" | "sub" | "mul" | "div" | "mod" | "pow" cmpop ::= "eq" | "ne" | "lt" | "gt" | "le" | "ge"
iter ::= "opt" ;; ? "list" ;; * "list1" ;; + "listn" exp id? ;; ^n, ^(i<n)
booltyp ::= "bool"
numtyp ::= "nat" | "int" | "rat" | "real"
texttyp ::= "text"
optyp ::= booltyp | numtyp
typ ::=
"var" id ;; t
booltyp ;; bool
numtyp ;; nat, int, ...
texttyp ;; text
"tup" typbind* ;; ( typ , ... , typ )
"iter" typ iter ;; typ*, typ+, ...
deftyp ::=
"alias" typ ;; typ
"struct" typfield* ;; { field , ... , field }
"variant" typcase* ;; case | ... | case
typbind ::= "bind" exp typ
typfield ::= "field" mixop bind* typ prem*
typcase ::= "case" mixop bind* typ prem*
exp ::=
"var" id ;; x
"bool" bool ;; true, false
"num" num ;; 0, -2
"text" text ;; "text"
"un" unop optyp exp ;; <op> exp
"bin" binop optyp exp exp ;; exp <op> exp
"cmp" cmpop optyp exp exp ;; exp <cmp> exp
"idx" exp exp ;; exp[exp]
"slice" exp exp exp ;; exp[exp : exp]
"upd" exp path exp ;; exp[path = exp]
"ext" exp path exp ;; exp[path =++ exp]
"struct" expfield* ;; { atom exp, ... , atom exp }
"dot" exp mixop ;; exp.atom
"comp" exp exp ;; exp ++ exp (on records)
"mem" exp exp ;; exp <- exp
"len" exp ;; |exp|
"tup" exp* ;; (exp, ..., exp)
"call" id arg* ;; $x(arg, ..., arg)?
"iter" exp iter dom* ;; exp?, exp*, ...
"case" mixop exp ;; atom exp
"list" exp? ;; exp ... exp or [exp ... exp]
"cat" exp exp ;; exp ++ exp (on lists)
expfield ::= "field" mixop exp e
path ::=
"root" ;; .
"idx" path exp ;; path[exp]
"slice" path exp exp ;; path[exp : exp]
"dot" path mixop ;; path.atom
In addition to these explicit expressions, the IL also contains internal expressions that are inserted by the type checker:
exp ::= ... "proj" exp nat ;; tuple projection exp.i "uncase" exp mixop ;; inverse of "case" "opt" exp? ;; option value (eps or singletong value) "unopt" exp ;; inverse of "opt" "lift" exp ;; conversion from t? to t* "cvt" numtyp numtyp exp ;; conversion from first to second numeric type "sub" typ typ exp ;; subsumption from first to second type
Moreover, the IL explicitly annotates the variables iterated over by an iteration (its domain), and expressions denoting the values they are drawn from:
dom ::= "dom" id exp ;; x <- exp
For the source input, these will typically take the form x' <- x, where x' is an auxiliary introduced by the SpecTec frontend. However, the upshot of this representation is that it is closed under substitution: that is, x' is locally bound, while the r.h.s. can be substituted by arbitrary expressions, for example, when rewriting or reducing a term.
sym ::= "var" id arg* ;; x(arg, ..., arg) "num" nat ;; 0x12 "text" text ;; "text" "eps" ;; eps "seq" sym* ;; sym ... sym "alt" sym* ;; sym | ... | sym "range" sym sym ;; sym | "..." | sym "iter" sym iter dom ;; sym?, sym+, ... "attr" exp sym ;; exp:sym
prem ::= "rule" id mixop exp ;; -- id: mixop-exp "if" exp ;; -- if exp "else" ;; -- otherwise "let" exp exp ;; -- if exp = exp (when one side introduces variables) "iter" prem iter dom ;; -- prem*
def ::= "typ" id param* inst* ;; syntax x(param*) with instance definitions "rel" id mixop typ rule* ;; relation x: mixop-typ with rules "def" id param* typ clause* ;; def $x(param*) : typ with clauses "gram" id param* typ prod* ;; grammar x(param*) : typ with productions "rec" def* ;; inferred recursion group inst ::= "inst" bind* arg* deftyp dt ;; syntax _(arg*) = deftyp rule ::= "rule" id bind* mixop exp prem* ;; rule _/x mixop-exp -- prem* clause ::= "clause" bind* arg* exp* prem* ;; def $_(arg*) = exp -- prem* prod ::= "prod" bind* sym exp prem* ;; | sym => exp -- prem* param ::= "exp", id typ ;; x : typ "typ", id ;; syntax x "def", id param* typ ;; def $x(param*) : typ "gram", id typ ;; grammar x : typ arg ::= "exp" exp ;; exp "typ" typ ;; syntax typ "def" id ;; def $x "gram" sym ;; grammar sym bind ::= "exp" id typ "typ" id "def" id param* typ "gram" id param* typ
The binds are binders for the free variables in a definition and are inferred by the SpecTec frontend.
script ::= def*