Guillaume Melquiond
53926bbbf5
Update headers.
2022-04-26 16:33:42 +02:00
Jean-Christophe Filliatre
1c08c1987f
micro Python: added def for function/predicate and type variables
2021-09-30 14:32:03 +02:00
Jean-Christophe Filliatre
d6010c82eb
micro Python: types in quantifiers
2021-09-28 14:36:47 +02:00
Jean-Christophe Filliatre
d517234610
micro Python: type annotations in programs
2021-09-24 18:27:07 +02:00
Jean-Christophe Filliatre
cd46b54253
micrp Python: more types
2021-09-24 18:14:59 +02:00
Jean-Christophe Filliatre
8a373ad80b
micro Python : syntax for types in function and predicate
2021-09-24 16:12:45 +02:00
Guillaume Melquiond
534dcdd5f5
Do not call fprintf when the string does not contain any format modifier.
2021-09-10 14:11:20 +02:00
Jean-Christophe Filliatre
33c7457915
micro-Python: fixed parsing of transformation arguments
2021-09-08 17:53:48 +02:00
paulpatault
2cc29e8963
Micro Python : syntax improvements & added functions
...
- added break and continue
- added range with one, two or three argument(s)
- added slice (`list[i1:i2]`)
- added negative index (`list[n], with -len(list) ≤ n < len(list)`)
- added lists methods:
- `list.append(n)`
- `list.pop()`
- `list.clear()`
- `list.sort()`
- `list.reverse()`
- added `is_permutation(list1, list2)` predicate
- added assignment operators `+=`, `-=`, `*=`, `//=`, `%=`
- functions can now return `bool` and `list`
2021-06-24 11:44:07 +02:00
Guillaume Melquiond
1fc6be8459
Update headers.
2021-03-13 07:55:14 +01:00
Guillaume Melquiond
0070b9408d
Update headers.
2020-03-17 09:52:33 +01:00
Cláudio Belo Lourenço
83b02e04ac
Merge branch 'master' into 28-string-literals
2019-10-21 15:05:46 +02:00
Sylvain
c454feef96
external printer: fix nim.py
2019-09-25 17:48:44 +02:00
Sylvain
ea286888a6
External printer/parser: proof of concept on python plugin
2019-09-25 16:31:23 +02:00
Cláudio Belo Lourenço
372ec5a396
All constant literals under the same data type: integer, reals, and strings
2019-09-20 10:42:31 +02:00
Jean-Christophe Filliatre
42c2e450b9
Python/micro-C: at/old/labels now supported
...
makes use of auto-dereference
2019-07-06 14:54:56 +02:00
Jean-Christophe Filliatre
c8a111a2ec
Python/micro-C: at/old/labels not yet supported
2019-07-06 12:41:28 +02:00
Guillaume Melquiond
d3d7c7ac09
Rework numerical constants.
...
Main changes are:
- Real constants now offer a normalized representation usable for internal
computations.
- Constants are no longer stored in textual form.
2019-02-18 16:55:08 +01:00
Guillaume Melquiond
abf9c043cf
Update headers.
2019-02-11 15:35:11 +01:00
Raphael Rieu-Helft
17ed127006
Add support for partial functions
...
Program functions can be declared as partial with "let/val partial".
Similarly to "diverges", partial code cannot be ghost, however it does not need to be
explicitly specified as partial.
Fixes #184 .
2018-09-28 10:31:26 +02:00
Andrei Paskevich
295cacf443
Ident: disambiguated symbolic notation
...
It is possible to append an arbitary number of quote symbols
at the end of an prefix/infix/mixfix operator:
applied form standalone form
-' 42 (-'_)
x +' y (+')
a[0]' <- 1 ([]'<-)
Pretty-printing will use the quote symbols for disambiguation.
The derived symbols can be produced by Why3 by appending
a suffix of the form "_toto" or "'toto". These symbols can
be parsed/printed as "(+)_toto" or "(+)'toto", respectively.
2018-07-17 23:53:22 +02:00
Andrei Paskevich
0fea401c50
confine all notation handling inside Ident
...
This commit removes all hard-coded "infix ..", "prefix ..",
and "mixfix .." from the rest of the code, and handles the
symbolic notation entirely inside Ident. It does not change
the notation itself.
2018-07-07 16:20:06 +02:00
Andrei Paskevich
35c1b010d7
WhyML: allow "ghost" over arbitrary subpatterns
...
This lets us write "let ghost (x, y) = 0, 0"
instead of "let ghost x, ghost y = 0, 0".
2018-06-18 17:29:12 +02:00
Andrei Paskevich
b0cef7e3f2
s/label/attribute/g
2018-06-01 21:03:01 +02:00
Guillaume Melquiond
fc1b4fe530
Merge branch 'new_ide'
...
# Conflicts:
# bench/ce/
2018-02-17 10:46:39 +01:00
