Andrei Paskevich
b8fb2e85c1
WhyML: "alias { t1 with t2, t3 with t4 }" annotation
...
Forces aliasing between the arguments, external reads and the
result (denoted "result"). Cannot be used for exceptional results.
Currently, is only used for "any" and "val", and is silently ignored
otherwise.
2017-12-13 18:47:53 +01:00
Guillaume Melquiond
3293552356
Merge branch 'master' into new_system
2017-11-24 17:25:45 +01:00
Guillaume Melquiond
609cfacf05
Rename functions int_const_* into int_literal_* to reflect their types.
...
This commit also gets rid of `int_const_dec (string_of_int ...)`.
2017-11-23 19:17:25 +01:00
Guillaume Melquiond
3aae32e7bc
Backport support for negative literals.
2017-11-22 17:57:32 +01:00
Guillaume Melquiond
8c20ed74e1
Remove some uses of Number.int_const_dec.
2017-11-07 10:47:02 +01:00
Andrei Paskevich
6aace6618f
WhyML: match ... with exception ... end
2017-06-11 02:15:45 +02:00
Claude Marche
b676212680
support for negative literals, first step
...
- requires a lot more testing
- support in extraction missing (exception raised)
- interaction with "syntax literal" remains to investigate
2017-06-09 15:19:22 +02:00
Andrei Paskevich
c6933a1f1d
python: update for new_system
2017-04-25 17:02:29 +02:00
Andrei Paskevich
3c062899e5
Python: tentative update for new_system
2017-04-24 15:43:45 +02:00
Guillaume Melquiond
4822694f3b
Merge branch 'master' into new_system
2017-04-14 17:45:25 +02:00
Claude Marche
216f2ecd71
update header for year 2017
2017-04-12 14:17:56 +02:00
Claude Marche
929db309dc
Remove a few compilation warnings
2017-04-05 14:22:24 +02:00
Jean-Christophe Filliatre
272e253a0f
python: functions and predicates
2017-03-17 17:04:29 +01:00
Jean-Christophe Filliatre
fec2cd7b3a
python plugin: parse function in Py_lexer
2017-03-09 11:11:54 +01:00
Andrei Paskevich
194dfa81de
reinitialise indentation stack
2017-03-07 16:45:19 +01:00
Andrei Paskevich
817c5367d5
python: fix an off-by-one in "for ... in range()"
2017-03-07 15:54:23 +01:00
Andrei Paskevich
d1784bcc91
fix py_parser.mly for older menhir
2017-02-22 01:08:11 +01:00
Jean-Christophe Filliatre
257e127406
python examples moved to tests/
2017-02-20 15:51:09 +01:00
Jean-Christophe Filliatre
1bf178c8eb
python: support for 'for x in range(i,j)'
2017-02-02 21:52:15 +01:00
Andrei Paskevich
3c54dbd330
python: make all locations mandatory and set a starting location
2017-02-01 13:48:49 +01:00
Andrei Paskevich
50513e7094
python: add the element preservation property for insertion sort
...
In a different file, so that we can show the simpler ordering property
first.
Also, I cheat, and add an appropriate lemma to modules/python.mlw.
Maybe this is a good lemma to have in map.Occ, too.
2017-02-01 00:06:12 +01:00
Jean-Christophe Filliatre
820c7bbd1e
python: fixed for loop
2017-01-31 22:56:00 +01:00
Jean-Christophe Filliatre
d1798364b6
python: a slight change in sort
2017-01-31 22:35:25 +01:00
Jean-Christophe Filliatre
645747d4cb
cleaning up
2017-01-31 22:29:40 +01:00
Jean-Christophe Filliatre
bd52075c22
ascii art
2017-01-31 22:25:59 +01:00
