-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathbnf.html
139 lines (117 loc) · 5.8 KB
/
bnf.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
<!DOCTYPE html>
<html lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1">
<link href="base-min.css" rel="stylesheet"/>
<link href="style.css" rel="stylesheet"/>
<title>TIP BNF</title>
</head>
<body>
<div class="header">
<h1>TIP BNF</h1>
</div>
<div class="content">
<p>This document contains the BNF of the <a href="index.html">TIP</a> format, which is an extension of <a href="http://smt-lib.org">SMT-LIB</a> for expression inductive problems. The grammar is written in <a href="http://bnfc.digitalgrammars.com/">BNFC</a> syntax. The format is also decribed in <a href="format.html">prose</a> with examples.</p>
<pre class="bnfc"><code>comment ";";
Start. Start ::= [Decl];
[]. [Decl] ::= ;
(:). [Decl] ::= "(" Decl ")" [Decl];
DeclareDatatype. Decl ::= "declare-datatype" AttrSymbol Datatype;
DeclareDatatypes. Decl ::= "declare-datatypes" "(" [DatatypeName] ")" "(" [Datatype] ")";
DeclareSort. Decl ::= "declare-sort" AttrSymbol Integer;
DeclareConst. Decl ::= "declare-const" AttrSymbol ConstType ;
DeclareFun. Decl ::= "declare-fun" AttrSymbol FunType;
DefineFun. Decl ::= "define-fun" FunDec Expr;
DefineFunRec. Decl ::= "define-fun-rec" FunDec Expr;
DefineFunsRec. Decl ::= "define-funs-rec" "(" [BracketedFunDec] ")" "(" [Expr] ")";
Formula. Decl ::= Assertion [Attr] Expr;
FormulaPar. Decl ::= Assertion [Attr] "(" Par Expr ")";
Assert. Assertion ::= "assert";
Prove. Assertion ::= "prove";
Par. Par ::= "par" "(" [Symbol] ")";
ConstTypeMono. ConstType ::= Type;
ConstTypePoly. ConstType ::= "(" Par Type ")";
InnerFunType. InnerFunType ::= "(" [Type] ")" Type;
FunTypeMono. FunType ::= InnerFunType;
FunTypePoly. FunType ::= "(" Par "(" InnerFunType ")" ")";
InnerFunDec. InnerFunDec ::= "(" [Binding] ")" Type;
FunDecMono. FunDec ::= AttrSymbol InnerFunDec;
FunDecPoly. FunDec ::= AttrSymbol "(" Par "(" InnerFunDec ")" ")";
BracketedFunDec. BracketedFunDec ::= "(" FunDec ")";
DatatypeName. DatatypeName ::= "(" AttrSymbol Integer ")";
InnerDatatype. InnerDatatype ::= "(" [Constructor] ")";
DatatypeMono. Datatype ::= InnerDatatype;
DatatypePoly. Datatype ::= "(" Par InnerDatatype ")";
Constructor. Constructor ::= "(" AttrSymbol [Binding] ")";
Binding. Binding ::= "(" Symbol Type ")";
LetDecl. LetDecl ::= "(" Symbol Expr ")";
TyVar. Type ::= Symbol;
TyApp. Type ::= "(" Symbol [Type] ")";
ArrowTy. Type ::= "(" "=>" [Type] ")";
IntTy. Type ::= "Int";
RealTy. Type ::= "Real";
BoolTy. Type ::= "Bool";
Var. Expr ::= PolySymbol;
App. Expr ::= "(" Head [Expr] ")";
Match. Expr ::= "(" "match" Expr "(" [Case] ")" ")";
Let. Expr ::= "(" "let" "(" [LetDecl] ")" Expr ")";
Binder. Expr ::= "(" Binder "(" [Binding] ")" Expr ")";
Lit. Expr ::= Lit;
LitInt. Lit ::= Integer;
LitNegInt. Lit ::= "-" Integer;
LitTrue. Lit ::= "true";
LitFalse. Lit ::= "false";
Lambda. Binder ::= "lambda";
Forall. Binder ::= "forall";
Exists. Binder ::= "exists";
Case. Case ::= "(" Pattern Expr ")";
Default. Pattern ::= "_";
ConPat. Pattern ::= "(" Symbol [Symbol] ")";
SimplePat. Pattern ::= Symbol;
LitPat. Pattern ::= Lit;
Const. Head ::= PolySymbol;
At. Head ::= "@";
IfThenElse. Head ::= "ite";
And. Head ::= "and";
Or. Head ::= "or";
Not. Head ::= "not";
Implies. Head ::= "=>";
Equal. Head ::= "=";
Distinct. Head ::= "distinct";
NumAdd. Head ::= "+";
NumSub. Head ::= "-";
NumMul. Head ::= "*";
NumDiv. Head ::= "/";
IntDiv. Head ::= "div";
IntMod. Head ::= "mod";
NumGt. Head ::= ">";
NumGe. Head ::= ">=";
NumLt. Head ::= "<";
NumLe. Head ::= "<=";
NumWiden. Head ::= "to_real";
NoAs. PolySymbol ::= Symbol;
As. PolySymbol ::= "(" "_" Symbol [Type] ")";
AttrSymbol. AttrSymbol ::= Symbol [Attr];
NoValue. Attr ::= Keyword;
Value. Attr ::= Keyword Symbol;
terminator LetDecl "";
terminator Case "";
terminator Expr "";
terminator Datatype "";
terminator Constructor "";
terminator Binding "";
terminator Symbol "";
terminator Type "";
terminator FunDec "";
terminator BracketedFunDec "";
terminator Attr "";
terminator DatatypeName "";
Unquoted. Symbol ::= UnquotedSymbol;
Quoted. Symbol ::= QuotedSymbol;
position token UnquotedSymbol (letter|["~!@$%^&*_+=<>.?/"])(letter|digit|["~!@$%^&*_-+=<>.?/"])*;
position token QuotedSymbol '|'((char - '|') | ('\\' char))*'|';
token Keyword ':'(letter|digit|["-"])*;</code></pre>
</div>
</body>
</html>