remove grammar, clean structure
This commit is contained in:
parent
7ad49a45a5
commit
9ff0030f15
5 changed files with 2 additions and 84 deletions
|
@ -12,7 +12,6 @@
|
|||
- [Comments](./concepts/comments.md)
|
||||
|
||||
- [Reference](reference/index.md)
|
||||
- [Grammar](reference/grammar.md)
|
||||
- [CLI](reference/cli.md)
|
||||
- [Verification](reference/verification.md)
|
||||
|
||||
|
|
|
@ -1 +1 @@
|
|||
# Programming Concepts
|
||||
# Programming Concepts
|
||||
|
|
1
zokrates_book/src/concepts/index.md
Normal file
1
zokrates_book/src/concepts/index.md
Normal file
|
@ -0,0 +1 @@
|
|||
# Programming Concepts
|
|
@ -1,81 +0,0 @@
|
|||
# Grammar
|
||||
|
||||
The current syntax of ZoKrates is the following
|
||||
```k
|
||||
module ZOKRATES-SYNTAX
|
||||
imports DOMAINS-SYNTAX
|
||||
|
||||
syntax Prog ::= Impts FunDecls [klabel(#Prog)] // should not be required, cf https://github.com/kframework/k-legacy/issues/1839
|
||||
|
||||
syntax ImptBody ::= "import" String
|
||||
syntax Alias ::= "as" Id
|
||||
syntax Impt ::= ImptBody [klabel(#Impt)]
|
||||
| ImptBody Alias [klabel(#AliasedImpt)]
|
||||
syntax Impts ::= List{Impt,""}
|
||||
|
||||
syntax Id ::= "main" [token]
|
||||
|
||||
syntax Arg ::= Type Id
|
||||
| "private" Type Id
|
||||
|
||||
syntax Type ::= "field"
|
||||
| "bool"
|
||||
syntax ReturnTypes ::= List{Type,","}
|
||||
|
||||
syntax Args ::= List{Arg,","}
|
||||
syntax FunDecl ::= "def" Id "(" Args ")" "->" "(" ReturnTypes ")" ":" Stmts
|
||||
syntax FunDecls ::= FunDecl
|
||||
| FunDecl FunDecls [right]
|
||||
|
||||
syntax Stmt ::= Assert
|
||||
| Define
|
||||
| Declare
|
||||
| DeclareDefine
|
||||
| Return
|
||||
| For
|
||||
| Destructure
|
||||
|
||||
syntax HintId ::= Id
|
||||
| Type Id
|
||||
|
||||
syntax HintIds ::= List{HintId,","}
|
||||
|
||||
syntax Destructure ::= HintId "," HintIds "=" FCall
|
||||
|
||||
syntax Stmts ::= List{Stmt,""}
|
||||
|
||||
syntax Assert ::= Exp "==" Exp
|
||||
syntax Declare ::= Type Id
|
||||
syntax Define ::= Id "=" Exp
|
||||
syntax DeclareDefine ::= Type Id "=" Exp // should be sugar for Declare then Define
|
||||
syntax Return ::= "return" Exps
|
||||
syntax For ::= "for" Type Id "in" Int ".." Int "do" Stmts "endfor"
|
||||
|
||||
|
||||
syntax Exps ::= List{Exp,","} [strict]
|
||||
syntax Exp ::= Int | Bool | Id
|
||||
| "(" Exp ")" [bracket]
|
||||
> Exp "(" Exps ")" [strict]
|
||||
> left:
|
||||
Exp "*" Exp [strict, left]
|
||||
| Exp "/" Exp [strict, left]
|
||||
| Exp "**" Exp [strict, left]
|
||||
> left:
|
||||
Exp "+" Exp [strict, left]
|
||||
| Exp "-" Exp [strict, left]
|
||||
| IfElse
|
||||
> non-assoc:
|
||||
Exp "<" Exp [strict, non-assoc]
|
||||
| Exp "<=" Exp [strict, non-assoc]
|
||||
| Exp ">" Exp [strict, non-assoc]
|
||||
| Exp ">=" Exp [strict, non-assoc]
|
||||
| Exp "==" Exp [strict, non-assoc]
|
||||
> IfElse
|
||||
> FCall
|
||||
|
||||
syntax FCall ::= Id "(" Exps ")"
|
||||
|
||||
syntax IfElse ::= "if" Exp "then" Exp "else" Exp "fi" [strict(1)]
|
||||
|
||||
endmodule
|
||||
```
|
|
@ -3,6 +3,5 @@
|
|||
The reference covers the details of various areas of ZoKrates.
|
||||
|
||||
- [ZoKrates Reference](index.md)
|
||||
- [Grammar](grammar.md)
|
||||
- [CLI](cli.md)
|
||||
- [Verification](verification.md)
|
||||
|
|
Loading…
Reference in a new issue