Merge branch 'master' of gitlab.com:gabriel.alfour/ligo
This commit is contained in:
commit
a94bf665f3
@ -12,37 +12,32 @@ before_script:
|
|||||||
- chmod +x /usr/local/bin/opam
|
- chmod +x /usr/local/bin/opam
|
||||||
- export PATH="/usr/local/bin${PATH:+:}${PATH:-}"
|
- export PATH="/usr/local/bin${PATH:+:}${PATH:-}"
|
||||||
|
|
||||||
# Show environment
|
# Initialise opam
|
||||||
- echo "$PATH"
|
|
||||||
- printf '' | opam init --bare
|
- printf '' | opam init --bare
|
||||||
- eval $(opam config env)
|
- eval $(opam config env)
|
||||||
|
|
||||||
# Create switch
|
# Create switch
|
||||||
- printf '' | opam switch create toto ocaml-base-compiler.4.06.1
|
- printf '' | opam switch create toto ocaml-base-compiler.4.06.1
|
||||||
- eval $(opam config env)
|
- eval $(opam config env)
|
||||||
|
|
||||||
# Show versions and current switch
|
# Show versions and current switch
|
||||||
|
- echo "$PATH"
|
||||||
- opam --version
|
- opam --version
|
||||||
- printf '' | ocaml
|
- printf '' | ocaml
|
||||||
- opam switch
|
- opam switch
|
||||||
|
|
||||||
# default-job:
|
|
||||||
# script:
|
|
||||||
# - (cd src/lib_utils && opam install -y --build-test --working-dir .)
|
|
||||||
# - (cd src/ligo && opam install -y --build-test --working-dir .)
|
|
||||||
# - (cd src/ligo && dune build && dune build -p ligo && dune build @ligo-test)
|
|
||||||
# artifacts:
|
|
||||||
# paths:
|
|
||||||
# - src/ligo/bin/cli.ml
|
|
||||||
|
|
||||||
local-dune-job:
|
local-dune-job:
|
||||||
script:
|
script:
|
||||||
- vendors/ligo-opam-repository/rewrite-local-opam-repository.sh
|
- vendors/ligo-opam-repository/rewrite-local-opam-repository.sh
|
||||||
- opam repository add localrepo "file://$PWD/vendors/ligo-opam-repository-local/"
|
- opam repository add localrepo "file://$PWD/vendors/ligo-opam-repository-local/"
|
||||||
- opam install -y --build-test --deps-only ./src/
|
- opam install -y --build-test --deps-only ./src/
|
||||||
- (dune build -p ligo)
|
- dune build -p ligo
|
||||||
# TODO: also try instead from time to time:
|
# TODO: also try instead from time to time:
|
||||||
#- (cd ./src/; dune build -p ligo)
|
#- (cd ./src/; dune build -p ligo)
|
||||||
- dune build @ligo-test
|
- dune build @ligo-test
|
||||||
|
# artifacts:
|
||||||
|
# paths:
|
||||||
|
# - src/ligo/bin/cli.ml
|
||||||
|
|
||||||
local-repo-job:
|
local-repo-job:
|
||||||
script:
|
script:
|
||||||
|
3
.gitmodules
vendored
3
.gitmodules
vendored
@ -1,9 +1,12 @@
|
|||||||
[submodule "vendors/ligo-opam-repository"]
|
[submodule "vendors/ligo-opam-repository"]
|
||||||
path = vendors/ligo-opam-repository
|
path = vendors/ligo-opam-repository
|
||||||
url = https://gitlab.com/gabriel.alfour/ligo-opam-repository.git
|
url = https://gitlab.com/gabriel.alfour/ligo-opam-repository.git
|
||||||
|
pushurl = git@gitlab.com:gabriel.alfour/ligo-opam-repository.git
|
||||||
[submodule "vendors/ligo-utils"]
|
[submodule "vendors/ligo-utils"]
|
||||||
path = vendors/ligo-utils
|
path = vendors/ligo-utils
|
||||||
url = https://gitlab.com/gabriel.alfour/ligo-utils.git
|
url = https://gitlab.com/gabriel.alfour/ligo-utils.git
|
||||||
|
pushurl = git@gitlab.com:gabriel.alfour/ligo-utils.git
|
||||||
[submodule "vendors/tezos-modded"]
|
[submodule "vendors/tezos-modded"]
|
||||||
path = vendors/tezos-modded
|
path = vendors/tezos-modded
|
||||||
url = https://gitlab.com/gabriel.alfour/tezos-modded.git
|
url = https://gitlab.com/gabriel.alfour/tezos-modded.git
|
||||||
|
pushurl = git@gitlab.com:gabriel.alfour/tezos-modded.git
|
||||||
|
@ -44,7 +44,7 @@ let rec expression ppf (e:expression) = match e with
|
|||||||
| E_look_up (ds, ind) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression ind
|
| E_look_up (ds, ind) -> fprintf ppf "(%a)[%a]" annotated_expression ds annotated_expression ind
|
||||||
| E_lambda {binder;input_type;output_type;result;body} ->
|
| E_lambda {binder;input_type;output_type;result;body} ->
|
||||||
fprintf ppf "lambda (%s:%a) : %a {@; @[<v>%a@]@;} return %a"
|
fprintf ppf "lambda (%s:%a) : %a {@; @[<v>%a@]@;} return %a"
|
||||||
binder type_expression input_type type_expression output_type
|
binder type_annotation input_type type_annotation output_type
|
||||||
block body annotated_expression result
|
block body annotated_expression result
|
||||||
| E_matching (ae, m) ->
|
| E_matching (ae, m) ->
|
||||||
fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m
|
fprintf ppf "match %a with %a" annotated_expression ae (matching annotated_expression) m
|
||||||
|
@ -137,8 +137,8 @@ let e_lambda (binder : string)
|
|||||||
: expression =
|
: expression =
|
||||||
E_lambda {
|
E_lambda {
|
||||||
binder = (make_name binder) ;
|
binder = (make_name binder) ;
|
||||||
input_type = input_type ;
|
input_type = Some input_type ;
|
||||||
output_type = output_type ;
|
output_type = Some output_type ;
|
||||||
result = (make_e_a result) ;
|
result = (make_e_a result) ;
|
||||||
body ;
|
body ;
|
||||||
}
|
}
|
||||||
|
@ -47,8 +47,8 @@ and type_expression =
|
|||||||
|
|
||||||
and lambda = {
|
and lambda = {
|
||||||
binder: name ;
|
binder: name ;
|
||||||
input_type: type_expression ;
|
input_type: type_expression option;
|
||||||
output_type: type_expression ;
|
output_type: type_expression option;
|
||||||
result: ae ;
|
result: ae ;
|
||||||
body: block ;
|
body: block ;
|
||||||
}
|
}
|
||||||
|
@ -1,7 +1,7 @@
|
|||||||
$HOME/git/OCaml-build/Makefile
|
$HOME/git/OCaml-build/Makefile
|
||||||
$HOME/git/OCaml-build/Makefile.cfg
|
$HOME/git/OCaml-build/Makefile.cfg
|
||||||
$HOME/git/tezos/src/lib_utils/pos.mli
|
$HOME/git/ligo/vendors/ligo-utils/simple-utils/pos.mli
|
||||||
$HOME/git/tezos/src/lib_utils/pos.ml
|
$HOME/git/ligo/vendors/ligo-utils/simple-utils/pos.ml
|
||||||
$HOME/git/tezos/src/lib_utils/region.mli
|
$HOME/git/ligo/vendors/ligo-utils/simple-utils/region.mli
|
||||||
$HOME/git/tezos/src/lib_utils/region.ml
|
$HOME/git/ligo/vendors/ligo-utils/simple-utils/region.ml
|
||||||
Stubs/Tezos_utils.ml
|
Stubs/Simple_utils.ml
|
||||||
|
@ -199,10 +199,9 @@ and type_expr =
|
|||||||
|
|
||||||
and cartesian = (type_expr, times) nsepseq reg
|
and cartesian = (type_expr, times) nsepseq reg
|
||||||
|
|
||||||
and variant = { (* TODO: Constant constructors *)
|
and variant = {
|
||||||
constr : constr;
|
constr : constr;
|
||||||
kwd_of : kwd_of;
|
args : (kwd_of * cartesian) option
|
||||||
product : cartesian
|
|
||||||
}
|
}
|
||||||
|
|
||||||
and record_type = field_decl reg injection reg
|
and record_type = field_decl reg injection reg
|
||||||
|
@ -184,9 +184,8 @@ and type_expr =
|
|||||||
and cartesian = (type_expr, times) nsepseq reg
|
and cartesian = (type_expr, times) nsepseq reg
|
||||||
|
|
||||||
and variant = {
|
and variant = {
|
||||||
constr : constr;
|
constr : constr;
|
||||||
kwd_of : kwd_of;
|
args : (kwd_of * cartesian) option
|
||||||
product : cartesian
|
|
||||||
}
|
}
|
||||||
|
|
||||||
and record_type = field_decl reg injection reg
|
and record_type = field_decl reg injection reg
|
||||||
|
393
src/parser/pascaligo/Doc/pascaligo.txt
Normal file
393
src/parser/pascaligo/Doc/pascaligo.txt
Normal file
@ -0,0 +1,393 @@
|
|||||||
|
INTERNAL DOCUMENTATION OF THE PARSER OF PASCALIGO (Pascal-like LIGO)
|
||||||
|
|
||||||
|
This document describes the source code in the directory
|
||||||
|
ligo/src/parser/pascaligo and some maintenance workflows.
|
||||||
|
|
||||||
|
The directory contains the following:
|
||||||
|
|
||||||
|
Doc
|
||||||
|
The directory containing this documentation.
|
||||||
|
|
||||||
|
Tests
|
||||||
|
The directory containing tests.
|
||||||
|
|
||||||
|
Version.ml
|
||||||
|
A source containing a commit hash. It should be deleted, as Dune
|
||||||
|
knows how to generate and updated version.
|
||||||
|
|
||||||
|
dune
|
||||||
|
The Dune file for building the Pascaligo parser.
|
||||||
|
|
||||||
|
pascaligo.ml
|
||||||
|
A source needed for building the parser with Dune.
|
||||||
|
|
||||||
|
check_dot_git_is_dir.sh
|
||||||
|
A shell initially made to distinguish a git worktree from the
|
||||||
|
working directory (currently broken).
|
||||||
|
|
||||||
|
Stubs
|
||||||
|
A directory containing Tezos_utils.ml, which is ignored by Dune,
|
||||||
|
but linked from the parent directory ligo/src/parser/pascaligo
|
||||||
|
when building with the Christian's Makefile for OCaml
|
||||||
|
projects. (See http://github.com/rinderknecht/OCaml-build) Ignore
|
||||||
|
them.
|
||||||
|
|
||||||
|
.LexerMain.tag
|
||||||
|
.Lexer.ml.tag
|
||||||
|
.ParserMain.tag
|
||||||
|
.Parser.mly.tag
|
||||||
|
.links
|
||||||
|
As ligo/src/parser/pascaligo/Stubs/Tezos_utils.ml, these files
|
||||||
|
are only used by Christian's build system. Ignore them.
|
||||||
|
|
||||||
|
LexerMain.ml
|
||||||
|
ParserMain.ml
|
||||||
|
Source for two entry points enabling Christian's build system to
|
||||||
|
build only a standalone lexer or a standalone parser. Do not
|
||||||
|
change, unless you change EvalOpt and use Christian's build system.
|
||||||
|
|
||||||
|
LexerLog.ml
|
||||||
|
LexerLog.mli
|
||||||
|
Source for instantiating a standalone lexer for LexerMain.ml and
|
||||||
|
ParserMain.ml. Ignore them.
|
||||||
|
|
||||||
|
ParserLog.mli
|
||||||
|
ParserLog.ml
|
||||||
|
Source for printing the AST. Used by ParserMain.ml, pascaligo.ml
|
||||||
|
and the translator from this AST to the one needed by the
|
||||||
|
type-checker (see directory ligo/src/simplify).
|
||||||
|
|
||||||
|
Utils.mli
|
||||||
|
Utils.ml
|
||||||
|
Some utility types and functions.
|
||||||
|
|
||||||
|
AST.mli
|
||||||
|
AST.ml
|
||||||
|
The abstract syntax tree of Pascaligo.
|
||||||
|
|
||||||
|
EvalOpt.mli
|
||||||
|
EvalOpt.ml
|
||||||
|
The module EvalOpt parses the command-line for options to the
|
||||||
|
parser. That action is performed as a side-effect when the module
|
||||||
|
is initialised at run-time: this is ugly and easy to fix. See
|
||||||
|
ligo/src/parser/ligodity/EvalOpt.ml{i} for the right way to do
|
||||||
|
it. Ignore them: the file actually calling directly the parser is
|
||||||
|
ligo/src/parser/parser.ml. Note that, as a consequence, no option
|
||||||
|
is currently passed to the parser when building Pascaligo with
|
||||||
|
Dune. This should be made available.
|
||||||
|
|
||||||
|
Markup.mli
|
||||||
|
Markup.ml
|
||||||
|
The definition of markup in Pascaligo source files, and some some
|
||||||
|
functions to print or convert it to strings. You are unlikely
|
||||||
|
going to modify those files, as markup is pretty much the same for
|
||||||
|
all LIGO flavours.
|
||||||
|
|
||||||
|
FQueue.mli
|
||||||
|
FQueue.ml
|
||||||
|
A naive implementation of purely functional queues. Replace by an
|
||||||
|
imperative implementation if worst-case performance of single
|
||||||
|
operations (queue/enqueue) is an issue.
|
||||||
|
|
||||||
|
Error.mli
|
||||||
|
The definition of the open type for errors: the lexer will add its
|
||||||
|
own errors, the downside being that matching on errors requires a
|
||||||
|
catch-all clause "| _ -> assert false" at the end. Note: the rest
|
||||||
|
of the compiler uses an error monad.
|
||||||
|
|
||||||
|
Lexer.mli
|
||||||
|
Lexer.mll
|
||||||
|
The Pascaligo lexer is generated from two ocamllex
|
||||||
|
specifications. Lexer.mll is the first-level lexer. It exports a
|
||||||
|
functor [Make] parameterised over a module [Token] defining the
|
||||||
|
tokens, and returning a module whose signature is [Lexer.S]. (See
|
||||||
|
Lexer.mli for a rationale.) If you write a new flavour of LIGO,
|
||||||
|
this lexer is likely to be reused as is. Note that a great deal of
|
||||||
|
the complexity of this lexer stems from its purpose to report
|
||||||
|
stylistic errors (hence keeping temporarily scanned markup) and
|
||||||
|
handling UTF-8 encoded comments. The first goal implies sometimes
|
||||||
|
reading more than one token, and an extra-buffer has to be managed
|
||||||
|
above the ocamllex one, so the parser is not confused about the
|
||||||
|
location (region) of the token it has just read.
|
||||||
|
|
||||||
|
LexToken.mli
|
||||||
|
LexToken.mll
|
||||||
|
The second-level lexer of Pascaligo, scanning the (lexical)
|
||||||
|
tokens, and used to instantiate the first-level lexer
|
||||||
|
(Lexer.mll). If you write a new flavour of LIGO, this lexer is
|
||||||
|
likely to be modified, also if you plan to add new lexemes (beware
|
||||||
|
that if you add a new token constructor to the type [LexToken.t],
|
||||||
|
you may have to change the signature [Lexer.S] so you an instantiate
|
||||||
|
the first-level lexer.
|
||||||
|
|
||||||
|
Parser.mly
|
||||||
|
The Menhir specification of the grammar of Pascaligo and the
|
||||||
|
semantic actions building the AST. The syntax is actually a mix of
|
||||||
|
two sub-flavours: one in which compound structures, like blocks,
|
||||||
|
records, lists etc., are opened by a keyword denoting the kind of
|
||||||
|
structure, like "block", "record", "list" etc., and are closed by
|
||||||
|
the key word "end", and one in which those structures are opened
|
||||||
|
by a keyword followed by a symbol, like "{", "[" etc. and closed
|
||||||
|
by a symbol, lik "}", "]" etc. For instance,
|
||||||
|
"record x : t; y : u end" versus "record {x : t; y : u}".
|
||||||
|
In the future, these two styles should be separated and, in the
|
||||||
|
meantime, it is advise to keep to one style per LIGO contract, for
|
||||||
|
readability's sake. A first maintenance task would be to separate
|
||||||
|
this file in two, so each parses only one style, and share the
|
||||||
|
common parts of the grammar.
|
||||||
|
However you change this file, the grammar must remain without LR
|
||||||
|
conflicts, without resorting %prec or %assoc annotations.
|
||||||
|
|
||||||
|
|
||||||
|
PASCALIGO
|
||||||
|
|
||||||
|
Generalities
|
||||||
|
|
||||||
|
Pascaligo is an imperative language for writing smart contracts on the
|
||||||
|
Tezos blockchain. As such, it is compiled to Michelson, the native
|
||||||
|
language of the Tezos blockchain. Its design is inspired by Pascal,
|
||||||
|
OCaml and Michelson.
|
||||||
|
|
||||||
|
An imperative language is a language in which the value bound to a
|
||||||
|
variable can change over time, as opposed to a constant. That change,
|
||||||
|
called _side-effect_, is often leveraged through loops, enabling data
|
||||||
|
to be modified and accumulated repeatedly. For example, here is how
|
||||||
|
the integer value associated to the variable "x" is incremented by an
|
||||||
|
instruction, called _assignment_:
|
||||||
|
|
||||||
|
x := x + 1;
|
||||||
|
|
||||||
|
A loop computing the sum of all integers from 1 to 10 would be written
|
||||||
|
as follows:
|
||||||
|
|
||||||
|
y := 0;
|
||||||
|
for x := 1 to 10
|
||||||
|
begin
|
||||||
|
y := y + x
|
||||||
|
end
|
||||||
|
|
||||||
|
(Note that this is useless in practice, as a closed-form formula
|
||||||
|
exists for that computation.)
|
||||||
|
|
||||||
|
In Pascaligo, expressions and instructions are
|
||||||
|
distinguished. Expressions are evaluated and yield values, whilst
|
||||||
|
instructions are evaluated but do not yield values. Instructions are
|
||||||
|
meant to perform side-effects, like changing the value of a variable,
|
||||||
|
whereas expressions are purely computational, like calculating a an
|
||||||
|
arithmetic means. Instructions and expressions can be compounded, and
|
||||||
|
instructions can evaluate expressions as a means to perform
|
||||||
|
side-effects.
|
||||||
|
|
||||||
|
Pascaligo is strongly and statically typed, which means that the
|
||||||
|
composition of data and functions is contrained so the compiler can
|
||||||
|
check that no such composition can fail at run-time, e.g., because of
|
||||||
|
a meaningless expression. Pascaligo requires that variables are
|
||||||
|
declared together with their type and an initial value.
|
||||||
|
|
||||||
|
Declarations of values come in two kinds: either constants or
|
||||||
|
variables. The former are assigned only once at their declaration, and
|
||||||
|
the latter can be reassigned. The syntax is slightly different for
|
||||||
|
both. For example, the variables "x" and "y" above could have been
|
||||||
|
declared as follows:
|
||||||
|
|
||||||
|
var x : nat := 0;
|
||||||
|
var y : nat := 0;
|
||||||
|
|
||||||
|
It is possible to specify that the value of a variable will not change
|
||||||
|
(the name "variable" is misleading in that context), that is, they
|
||||||
|
remain constant:
|
||||||
|
|
||||||
|
const ten : nat = 10;
|
||||||
|
const eleven : nat = ten + 1;
|
||||||
|
|
||||||
|
Similarly, function declarations have their parameters and return
|
||||||
|
value annotated with their types. For instance,
|
||||||
|
|
||||||
|
function sum (const n : nat; const m : nat) : nat is
|
||||||
|
begin
|
||||||
|
end with n + m;
|
||||||
|
|
||||||
|
declarares the function "sum" that takes as argument two constant
|
||||||
|
natural numbers and return their sum. The expression whose value is
|
||||||
|
the result of calling the function is given after the keyword "with".
|
||||||
|
|
||||||
|
A another example would be
|
||||||
|
|
||||||
|
function factorial (const n : nat) : nat is
|
||||||
|
var m : nat := 0;
|
||||||
|
var f : nat := 1;
|
||||||
|
begin
|
||||||
|
if n <= 0 then f := 1
|
||||||
|
else
|
||||||
|
for m := 1 to n
|
||||||
|
begin
|
||||||
|
f := f * m
|
||||||
|
end
|
||||||
|
end with f
|
||||||
|
|
||||||
|
Like Pascal, Pascaligo offers procedures, as well as functions. The
|
||||||
|
difference follows the divide between expressions and instructions:
|
||||||
|
function calls are expressions, procedure calls are instructions.
|
||||||
|
|
||||||
|
A special case of functions are entry points, which are functions that
|
||||||
|
can be called when interacting with the contract after it has been
|
||||||
|
originated on the chain. The only difference with function is that
|
||||||
|
they are introduced by a keyword "entrypoint", instead of "function",
|
||||||
|
and they (currently) must have a special parameter for the storage,
|
||||||
|
and the return type must be a pair made of a new storage and a list of
|
||||||
|
operations. For example,
|
||||||
|
|
||||||
|
entrypoint contribute (storage store : store; ...)
|
||||||
|
: store * list (operation) is
|
||||||
|
var operations : list (operation) := nil
|
||||||
|
begin
|
||||||
|
...
|
||||||
|
end with (store, operations)
|
||||||
|
|
||||||
|
where "storage" is a keyword.
|
||||||
|
|
||||||
|
Pascaligo features predefined types, like integers, natural numbers,
|
||||||
|
mutez, strings, maps, lists etc. and constructs to combine those into
|
||||||
|
structured types. Amongst those constructs are the records, which
|
||||||
|
group and map names (_fields_) to values of potentially different
|
||||||
|
types. For instance,
|
||||||
|
|
||||||
|
type point is
|
||||||
|
record
|
||||||
|
x : int;
|
||||||
|
y : int
|
||||||
|
end
|
||||||
|
|
||||||
|
defines a record type "store" with three fields, each made of a name
|
||||||
|
and a type. Values of record types are made by assigning a value to
|
||||||
|
each field (in any order). Like so:
|
||||||
|
|
||||||
|
const origin : point =
|
||||||
|
record
|
||||||
|
x = 0;
|
||||||
|
y = 0
|
||||||
|
end
|
||||||
|
|
||||||
|
At this point it is perhaps useful to remark that there are actually
|
||||||
|
two flavours of Pascaligo recognised by the same parser: they should
|
||||||
|
be separated in the future, and, for now, it is best to not mix both
|
||||||
|
styles. Those style differ in the manner compound constructs are
|
||||||
|
delimited
|
||||||
|
|
||||||
|
For example, the type "point" above could have been alternatively
|
||||||
|
defined as follows:
|
||||||
|
|
||||||
|
type point is
|
||||||
|
record [
|
||||||
|
x : int;
|
||||||
|
y : int
|
||||||
|
]
|
||||||
|
|
||||||
|
and the value as
|
||||||
|
|
||||||
|
const origin : point = record [x = 0; y = 0];
|
||||||
|
|
||||||
|
When updating the contents of a record, Pascaligo offers some
|
||||||
|
syntactic support. Instead of writing all the assignments, most of
|
||||||
|
which are left unchanged, there is the record patch, which corresponds
|
||||||
|
to a functional update in OCaml. For example,
|
||||||
|
|
||||||
|
var p : point := origin;
|
||||||
|
|
||||||
|
patch p with record y = 10 end;
|
||||||
|
|
||||||
|
will update only the field "y" of "p". Of course, this example is not
|
||||||
|
impressive, but imagine that one has to update a small number of
|
||||||
|
fields in a large record. An alternative syntax is
|
||||||
|
|
||||||
|
patch p with record [y = 10];
|
||||||
|
|
||||||
|
Another way to combine types are disjunctive types, which are a
|
||||||
|
generalisation of enumerated types found in OCaml. They can be
|
||||||
|
interpreted as being a disjoint partition of value sets, each being
|
||||||
|
disinguished by a unique tag, or _data constructor_. For example,
|
||||||
|
|
||||||
|
type u = unit
|
||||||
|
type t = A | B of u | C of int * string
|
||||||
|
|
||||||
|
See OCaml.
|
||||||
|
|
||||||
|
As in OCaml, their values can be matched against patterns:
|
||||||
|
|
||||||
|
match v with
|
||||||
|
A -> "A"
|
||||||
|
| B Unit -> "B"
|
||||||
|
| C (_, s) -> s
|
||||||
|
|
||||||
|
Of course, we also find type aliases, which simply rename a type. More
|
||||||
|
importantly, Pascaligo has predefined types that cannot be defined by
|
||||||
|
the contract programmer. Indeed, user-defined types are monomorphic
|
||||||
|
and non-recursive, in other words, they are not parameterised and
|
||||||
|
cannot be defined in terms of themselves. This limitation precludes
|
||||||
|
defining lists of values, as a list is an inductive data type: a list
|
||||||
|
is either empty or a pair made of an item (the first item) and another
|
||||||
|
list (the remaining items). That is why Pascaligo features a native
|
||||||
|
polymorphic list type, with the condition that all list values must
|
||||||
|
instantiate the type of the items it contains. Another useful data
|
||||||
|
abstraction, native to Pascaligo, is the map, which relates values of
|
||||||
|
a given type to values of another given type. The last type predefined
|
||||||
|
by Pascaligo is the set.
|
||||||
|
|
||||||
|
Pascaligo is inspired by Pascal and OCaml. Semi-colons are separators,
|
||||||
|
but they can be used as terminators as well.
|
||||||
|
|
||||||
|
For example
|
||||||
|
|
||||||
|
type store is
|
||||||
|
record
|
||||||
|
goal : nat;
|
||||||
|
deadline : timestamp;
|
||||||
|
backers : map (address, nat);
|
||||||
|
funded : bool;
|
||||||
|
end
|
||||||
|
|
||||||
|
can alternatively be written
|
||||||
|
|
||||||
|
type store is
|
||||||
|
record
|
||||||
|
goal : nat;
|
||||||
|
deadline : timestamp;
|
||||||
|
backers : map (address, nat);
|
||||||
|
funded : bool
|
||||||
|
end
|
||||||
|
|
||||||
|
Only non-recursive types are user-definable in LIGO.
|
||||||
|
|
||||||
|
A predefined recursive and polymorphic type is the list (or
|
||||||
|
stack). The syntax is the same as in OCaml, with some extra syntax for
|
||||||
|
convenience. For example, the empty list can be written in three
|
||||||
|
different ways (only one is recommended by contract):
|
||||||
|
|
||||||
|
list end
|
||||||
|
list []
|
||||||
|
nil
|
||||||
|
|
||||||
|
A non-empty list starts with the keyword "list" and comes in two
|
||||||
|
flavours (only one is recommended by contract):
|
||||||
|
|
||||||
|
list 1; 2; 3 end
|
||||||
|
list [1; 2; 3]
|
||||||
|
|
||||||
|
To push (cons) and element in a list, the infix operator is "::", as
|
||||||
|
in OCaml:
|
||||||
|
|
||||||
|
1::2::l
|
||||||
|
|
||||||
|
All user-definable values in Pascaligo are monomorphic and must be
|
||||||
|
annotated with a their types, except in arithmetic or boolean
|
||||||
|
expressions, or at their declaration (since their type is given in the
|
||||||
|
left-hand side). In particular, empty lists need to be annotated, like
|
||||||
|
so
|
||||||
|
|
||||||
|
1 :: (nil : list (int))
|
||||||
|
|
||||||
|
But
|
||||||
|
|
||||||
|
var l : list (int) := list [];
|
||||||
|
|
||||||
|
works, as the type is available.
|
@ -213,9 +213,11 @@ sum_type:
|
|||||||
variant:
|
variant:
|
||||||
Constr Of cartesian {
|
Constr Of cartesian {
|
||||||
let region = cover $1.region $3.region
|
let region = cover $1.region $3.region
|
||||||
and value = {constr = $1; kwd_of = $2; product = $3}
|
and value = {constr = $1; args = Some ($2, $3)}
|
||||||
in {region; value} }
|
in {region; value}
|
||||||
(* TODO: Unary constructors *)
|
}
|
||||||
|
| Constr {
|
||||||
|
{region=$1.region; value= {constr=$1; args=None}} }
|
||||||
|
|
||||||
record_type:
|
record_type:
|
||||||
Record series(field_decl,End) {
|
Record series(field_decl,End) {
|
||||||
@ -367,7 +369,6 @@ param_type:
|
|||||||
cartesian { TProd $1 }
|
cartesian { TProd $1 }
|
||||||
|
|
||||||
block:
|
block:
|
||||||
(* Begin sequence(statement,SEMI) End { failwith "TODO" } *)
|
|
||||||
Begin series(statement,End) {
|
Begin series(statement,End) {
|
||||||
let first, (others, terminator, closing) = $2 in
|
let first, (others, terminator, closing) = $2 in
|
||||||
let region = cover $1 closing
|
let region = cover $1 closing
|
||||||
@ -706,7 +707,7 @@ assignment:
|
|||||||
in {region; value}}
|
in {region; value}}
|
||||||
|
|
||||||
rhs:
|
rhs:
|
||||||
expr { Expr $1 }
|
expr { Expr $1 }
|
||||||
|
|
||||||
lhs:
|
lhs:
|
||||||
path { Path $1 }
|
path { Path $1 }
|
||||||
@ -768,7 +769,7 @@ interactive_expr:
|
|||||||
|
|
||||||
expr:
|
expr:
|
||||||
case(expr) { ECase ($1 expr_to_region) }
|
case(expr) { ECase ($1 expr_to_region) }
|
||||||
| annot_expr { $1 }
|
| annot_expr { $1 }
|
||||||
|
|
||||||
annot_expr:
|
annot_expr:
|
||||||
LPAR disj_expr COLON type_expr RPAR {
|
LPAR disj_expr COLON type_expr RPAR {
|
||||||
|
@ -98,10 +98,13 @@ and print_cartesian {value; _} =
|
|||||||
print_nsepseq "*" print_type_expr value
|
print_nsepseq "*" print_type_expr value
|
||||||
|
|
||||||
and print_variant {value; _} =
|
and print_variant {value; _} =
|
||||||
let {constr; kwd_of; product} = value in
|
let {constr; args} = value in
|
||||||
print_constr constr;
|
print_constr constr;
|
||||||
print_token kwd_of "of";
|
match args with
|
||||||
print_cartesian product
|
None -> ()
|
||||||
|
| Some (kwd_of, product) ->
|
||||||
|
print_token kwd_of "of";
|
||||||
|
print_cartesian product
|
||||||
|
|
||||||
and print_sum_type {value; _} =
|
and print_sum_type {value; _} =
|
||||||
print_nsepseq "|" print_variant value
|
print_nsepseq "|" print_variant value
|
||||||
|
@ -14,7 +14,7 @@ entrypoint contribute (storage store : store;
|
|||||||
// const s : list (int) = list [1; 2; 3]
|
// const s : list (int) = list [1; 2; 3]
|
||||||
//const t : set (int) = set []
|
//const t : set (int) = set []
|
||||||
begin
|
begin
|
||||||
if now > store.deadline then
|
if now (Unit) > store.deadline then
|
||||||
fail "Deadline passed";
|
fail "Deadline passed";
|
||||||
else
|
else
|
||||||
case store.backers[sender] of [
|
case store.backers[sender] of [
|
||||||
|
@ -456,16 +456,17 @@ let let_entry : _ -> _ result = fun l ->
|
|||||||
List.mapi aux [ (param_name , param_ty) ; ((unwrap storage_name) , storage_ty)]
|
List.mapi aux [ (param_name , param_ty) ; ((unwrap storage_name) , storage_ty)]
|
||||||
in
|
in
|
||||||
let%bind (body' , result) = expression_last_instruction (unwrap e) in
|
let%bind (body' , result) = expression_last_instruction (unwrap e) in
|
||||||
|
let input_type' = input_nty.type_expression in
|
||||||
|
let output_type' = O.(t_pair (t_list t_operation , storage_ty)) in
|
||||||
let lambda =
|
let lambda =
|
||||||
let output_type = O.(t_pair (t_list t_operation , storage_ty)) in
|
|
||||||
O.{
|
O.{
|
||||||
binder = input_nty.type_name ;
|
binder = input_nty.type_name ;
|
||||||
input_type = input_nty.type_expression ;
|
input_type = Some input_type';
|
||||||
output_type ;
|
output_type = Some output_type';
|
||||||
result ;
|
result ;
|
||||||
body = tpl_declarations @ body' ;
|
body = tpl_declarations @ body' ;
|
||||||
} in
|
} in
|
||||||
let type_annotation = Some (O.T_function (lambda.input_type , lambda.output_type)) in
|
let type_annotation = Some (O.T_function (input_type', output_type')) in
|
||||||
ok @@ O.Declaration_constant {name = (unwrap n) ; annotated_expression = {expression = O.E_lambda lambda ; type_annotation}}
|
ok @@ O.Declaration_constant {name = (unwrap n) ; annotated_expression = {expression = O.E_lambda lambda ; type_annotation}}
|
||||||
|
|
||||||
let let_init_storage : _ -> _ result = fun l ->
|
let let_init_storage : _ -> _ result = fun l ->
|
||||||
|
@ -58,8 +58,13 @@ let rec simpl_type_expression (t:Raw.type_expr) : type_expression result =
|
|||||||
ok @@ T_record m
|
ok @@ T_record m
|
||||||
| TSum s ->
|
| TSum s ->
|
||||||
let aux (v:Raw.variant Raw.reg) =
|
let aux (v:Raw.variant Raw.reg) =
|
||||||
|
let args =
|
||||||
|
match v.value.args with
|
||||||
|
None -> []
|
||||||
|
| Some (_, product) ->
|
||||||
|
npsseq_to_list product.value in
|
||||||
let%bind te = simpl_list_type_expression
|
let%bind te = simpl_list_type_expression
|
||||||
@@ npseq_to_list v.value.product.value in
|
@@ args in
|
||||||
ok (v.value.constr.value, te)
|
ok (v.value.constr.value, te)
|
||||||
in
|
in
|
||||||
let%bind lst = bind_list
|
let%bind lst = bind_list
|
||||||
@ -345,7 +350,8 @@ and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x ->
|
|||||||
let%bind result = simpl_expression return in
|
let%bind result = simpl_expression return in
|
||||||
let%bind output_type = simpl_type_expression ret_type in
|
let%bind output_type = simpl_type_expression ret_type in
|
||||||
let body = local_declarations @ instructions in
|
let body = local_declarations @ instructions in
|
||||||
let expression = E_lambda {binder ; input_type ; output_type ; result ; body } in
|
let expression = E_lambda {binder ; input_type = Some input_type;
|
||||||
|
output_type = Some output_type; result ; body } in
|
||||||
let type_annotation = Some (T_function (input_type, output_type)) in
|
let type_annotation = Some (T_function (input_type, output_type)) in
|
||||||
ok {name;annotated_expression = {expression;type_annotation}}
|
ok {name;annotated_expression = {expression;type_annotation}}
|
||||||
)
|
)
|
||||||
@ -384,7 +390,8 @@ and simpl_fun_declaration : Raw.fun_decl -> named_expression result = fun x ->
|
|||||||
|
|
||||||
let body = tpl_declarations @ local_declarations @ instructions in
|
let body = tpl_declarations @ local_declarations @ instructions in
|
||||||
let%bind result = simpl_expression return in
|
let%bind result = simpl_expression return in
|
||||||
let expression = E_lambda {binder ; input_type ; output_type ; result ; body } in
|
let expression = E_lambda {binder ; input_type = Some input_type;
|
||||||
|
output_type = Some output_type; result ; body } in
|
||||||
let type_annotation = Some (T_function (input_type, output_type)) in
|
let type_annotation = Some (T_function (input_type, output_type)) in
|
||||||
ok {name = name.value;annotated_expression = {expression;type_annotation}}
|
ok {name = name.value;annotated_expression = {expression;type_annotation}}
|
||||||
)
|
)
|
||||||
|
@ -246,6 +246,14 @@ and translate_annotated_expression (ae:AST.annotated_expression) : expression re
|
|||||||
let return ?(tv = tv) expr = ok @@ Combinators.Expression.make_tpl (expr, tv) in
|
let return ?(tv = tv) expr = ok @@ Combinators.Expression.make_tpl (expr, tv) in
|
||||||
let f = translate_annotated_expression in
|
let f = translate_annotated_expression in
|
||||||
match ae.expression with
|
match ae.expression with
|
||||||
|
(* Optimise immediate application as a let-in *)
|
||||||
|
| E_application ({expression = E_lambda {binder; input_type; output_type=_; body=[]; result}; _},
|
||||||
|
rhs) ->
|
||||||
|
let%bind ty' = translate_type input_type in
|
||||||
|
let%bind rhs' = translate_annotated_expression env rhs in
|
||||||
|
let result_env = Environment.(add (binder, ty') env) in
|
||||||
|
let%bind result' = translate_annotated_expression result_env result in
|
||||||
|
return (E_let_in ((binder, ty'), rhs', result'))
|
||||||
| E_failwith ae -> (
|
| E_failwith ae -> (
|
||||||
let%bind ae' = translate_annotated_expression ae in
|
let%bind ae' = translate_annotated_expression ae in
|
||||||
return @@ E_constant ("FAILWITH" , [ae'])
|
return @@ E_constant ("FAILWITH" , [ae'])
|
||||||
|
2
vendors/tezos-modded
vendored
2
vendors/tezos-modded
vendored
@ -1 +1 @@
|
|||||||
Subproject commit 378e4a590407517482952984571fba2e52962900
|
Subproject commit 044f4dfa5974e627eab9bc1e3578b199182670fc
|
Loading…
x
Reference in New Issue
Block a user