daca4c9 | Pierre-Yves Strub | 28 July 2015, 07:01:20 UTC | Remove unused parse rules. | 28 July 2015, 07:01:20 UTC |
445abc1 | Pierre-Yves Strub | 27 July 2015, 19:47:44 UTC | Misc. fix of pretty printer - Fix associativity of :: - Fix pretty-printer of operator names (in printing of op. decl) - Add a space between a unary operator and its argument if this last is not a terminal symbol - Warn when a unary/binary operator cannot be used in prefix/infix mode [fix #17226] | 27 July 2015, 20:46:58 UTC |
c53f776 | Pierre-Yves Strub | 26 July 2015, 21:38:07 UTC | Define BigAlg as an exntesion of BigOp. | 26 July 2015, 21:38:07 UTC |
c6cf91d | Pierre-Yves Strub | 26 July 2015, 13:59:58 UTC | Add support for pattern (op-fix) in infix form. [fix #16786] | 26 July 2015, 20:15:41 UTC |
0a937a8 | Pierre-Yves Strub | 26 July 2015, 09:14:52 UTC | Add a exn. printer for lexical errors + improve lex error msgs. [fix #17223, #17224] | 26 July 2015, 09:15:43 UTC |
54fa7c1 | Pierre-Yves Strub | 25 July 2015, 09:55:37 UTC | Use alpha-eq. when searching for a contradiction in context. [close #17179] | 25 July 2015, 09:55:37 UTC |
8853bf3 | Pierre-Yves Strub | 21 July 2015, 21:06:09 UTC | Add a pragma to restart EasyCrypt. The pragma is `restart`. W.r.t `reset`, `restart` forces the reload of the prelude. [fix #17213] | 21 July 2015, 21:06:09 UTC |
49ffdf3 | Pierre-Yves Strub | 21 July 2015, 16:27:54 UTC | Negative line selector in program tactics. Line `-1` is the last line, `-2` the penultimate one, and so on. [close #17059] | 21 July 2015, 16:27:54 UTC |
abed2a9 | Pierre-Yves Strub | 17 July 2015, 14:33:08 UTC | Better user error message when giving an invalid inv. to `call`. [fix #17110] | 17 July 2015, 14:33:08 UTC |
787e2ad | Pierre-Yves Strub | 17 July 2015, 10:46:34 UTC | In expressions (in proc.), give priority to program vars. [fix #17189] | 17 July 2015, 10:46:34 UTC |
80265d2 | Pierre-Yves Strub | 17 July 2015, 10:25:39 UTC | Activate OCaml exception based CLI interruption. This is drafty as the SIGINT signal should be masked most of the time and only unmasked at very specific cancelation points. Mainly: before each tactical invocation and during SMT calls. [ref #17082] | 17 July 2015, 10:25:39 UTC |
6336362 | Pierre-Yves Strub | 17 July 2015, 09:28:44 UTC | Detection of circular deps. [fix #17212] | 17 July 2015, 09:28:44 UTC |
f0c7ded | Pierre-Yves Strub | 17 July 2015, 07:39:10 UTC | Refactor-in printing functions. | 17 July 2015, 07:39:10 UTC |
f37ef90 | Pierre-Yves Strub | 14 July 2015, 15:43:51 UTC | Fix pretty-printing of oracle informations. [ref #17215] | 14 July 2015, 15:44:05 UTC |
9f6601d | Pierre-Yves Strub | 13 July 2015, 10:28:18 UTC | Add a command to dump the full Why3 task This dumps the full environment, no hypothesis selection is done, and the `nosmt` flag is ignored. [close #17196] | 13 July 2015, 10:28:18 UTC |
25d7504 | Pierre-Yves Strub | 11 July 2015, 19:03:40 UTC | Pretty-printing of match-fix. [fix #17219] | 12 July 2015, 12:14:23 UTC |
9b8598c | Pierre-Yves Strub | 11 July 2015, 18:16:06 UTC | Set log-level to at least Warning when loading a theory. | 12 July 2015, 12:14:13 UTC |
52c261b | Pierre-Yves Strub | 11 July 2015, 18:08:43 UTC | Fix pretty-printer of abstract predicates, Don't print their type as for boolean operators, as the parser do not accept this syntax. [ref #17219] | 12 July 2015, 12:13:46 UTC |
a56587b | Pierre-Yves Strub | 11 July 2015, 17:59:05 UTC | Add `realize name by tactics` syntax Similiar to `lemma name : spec by tactics`, but applied to realization of lemmas after a partial clone. [fix #17220] | 12 July 2015, 12:13:35 UTC |
8a89d9d | Pierre-Yves Strub | 11 July 2015, 17:31:06 UTC | Syntax change `lemma L : F by t` now takes a tactic sequence instead of a single tactic. [fix #17221] | 12 July 2015, 12:13:22 UTC |
ca59aac | Pierre-Yves Strub | 11 July 2015, 17:27:16 UTC | New reduction rule for equality over unit. `x = y --> true` when `x, y : unit`. | 12 July 2015, 12:12:48 UTC |
1a35e05 | Pierre-Yves Strub | 10 July 2015, 20:30:10 UTC | StdRing: nosmt. | 10 July 2015, 20:30:18 UTC |
e3f7ce1 | Pierre-Yves Strub | 10 July 2015, 20:12:56 UTC | Ring/Number: trivial lemmas. | 10 July 2015, 20:13:11 UTC |
d89a5af | Pierre-Yves Strub | 10 July 2015, 20:12:45 UTC | FSet: pick + trivial lemmas. | 10 July 2015, 20:13:09 UTC |
bdab7b1 | Pierre-Yves Strub | 10 July 2015, 20:12:32 UTC | Add some if-construct simplification lemmas. | 10 July 2015, 20:13:08 UTC |
536b08d | Pierre-Yves Strub | 10 July 2015, 15:37:23 UTC | finset: subset <-> card relation. | 10 July 2015, 15:37:36 UTC |
3282164 | Pierre-Yves Strub | 10 July 2015, 15:37:10 UTC | More facts on the zmodule op. | 10 July 2015, 15:37:35 UTC |
ce05b75 | Pierre-Yves Strub | 09 July 2015, 10:20:38 UTC | Remove reserved keywords from uniop | 09 July 2015, 10:21:32 UTC |
abf3561 | François Dupressoir | 09 July 2015, 09:44:00 UTC | Array: fix and prove make_append. | 09 July 2015, 09:44:00 UTC |
c61b653 | Pierre-Yves Strub | 07 July 2015, 14:32:22 UTC | NewFSet: core lemmas about cardinal. | 07 July 2015, 14:32:22 UTC |
880c7a0 | Pierre-Yves Strub | 07 July 2015, 14:07:25 UTC | Cleaning NewFSet a bit. | 07 July 2015, 14:07:25 UTC |
127bc94 | Pierre-Yves Strub | 07 July 2015, 13:37:21 UTC | Import basic theory of membership and finite sets. | 07 July 2015, 13:37:21 UTC |
483b80b | Pierre-Yves Strub | 07 July 2015, 13:15:04 UTC | Change notation for fset. | 07 July 2015, 13:15:04 UTC |
c959352 | Pierre-Yves Strub | 07 July 2015, 10:54:55 UTC | New operator notation: ` opchar+ ` (where priority is taken from opchar+) | 07 July 2015, 13:14:54 UTC |
8102b1d | Benjamin Gregoire | 01 July 2015, 17:35:37 UTC | improve error message in cloning | 01 July 2015, 17:37:08 UTC |
8e1b50a | Benjamin Gregoire | 01 July 2015, 15:40:21 UTC | fix bug in cloning of operators | 01 July 2015, 15:40:41 UTC |
632b6bd | François Dupressoir | 30 June 2015, 10:02:33 UTC | Changes to PRF to clarify interfaces. This reverts commit 0a21f1da0c5fae4d3240b44a9838a2d71e8a75ff, which was itself a partial revert of its parent. | 30 June 2015, 10:03:13 UTC |
4acb16f | Pierre-Yves Strub | 29 June 2015, 15:40:57 UTC | bigops: replaced occurences of iota_ with range. | 29 June 2015, 15:40:57 UTC |
1e645ae | Pierre-Yves Strub | 29 June 2015, 15:38:13 UTC | Syntax lint. | 29 June 2015, 15:38:13 UTC |
b3e1f6d | Pierre-Yves Strub | 26 June 2015, 15:23:27 UTC | Don't use ocamlbuild classical display on terminals. | 29 June 2015, 15:29:58 UTC |
da354a5 | François Dupressoir | 29 June 2015, 13:37:07 UTC | ProofGeneral keywords. | 29 June 2015, 13:37:44 UTC |
377ffda | François Dupressoir | 29 June 2015, 13:36:22 UTC | Including .eca files in testsuites. Fixes #17216. | 29 June 2015, 13:37:44 UTC |
b234fb8 | Benjamin Gregoire | 29 June 2015, 12:47:24 UTC | remove unused variable | 29 June 2015, 12:47:24 UTC |
8d17061 | Benjamin Gregoire | 29 June 2015, 12:31:05 UTC | remove one admit; add lemma | 29 June 2015, 12:31:05 UTC |
97ddba0 | Benjamin Gregoire | 29 June 2015, 08:12:15 UTC | add one missing lemma | 29 June 2015, 08:12:15 UTC |
6a8051e | Benjamin Gregoire | 28 June 2015, 16:58:41 UTC | instanciate ring tac for int | 28 June 2015, 16:58:41 UTC |
591aff2 | Pierre-Yves Strub | 28 June 2015, 16:18:42 UTC | Remove unused import. | 28 June 2015, 16:18:42 UTC |
963f9ee | Pierre-Yves Strub | 28 June 2015, 13:17:52 UTC | Libraries: axiom of choice (functional form). | 28 June 2015, 13:17:52 UTC |
9e4bb14 | François Dupressoir | 26 June 2015, 14:49:06 UTC | smt is finally useful! | 26 June 2015, 14:49:06 UTC |
3033738 | François Dupressoir | 26 June 2015, 14:40:31 UTC | Importing some missing definitions. | 26 June 2015, 14:40:31 UTC |
a108f3f | Pierre-Yves Strub | 26 June 2015, 13:05:18 UTC | Removing remaining Why3 imports. | 26 June 2015, 14:11:53 UTC |
83cd782 | François Dupressoir | 26 June 2015, 13:01:03 UTC | Fixing the manual import, clarifying Euclidean Division. | 26 June 2015, 14:11:49 UTC |
7ae3d64 | François Dupressoir | 26 June 2015, 09:46:35 UTC | Replacing Why3 import with manual imports. Some remain in newth/NewIntCore.ec and newth/NewRealCore.ec. smt full and smt all currently fail for different reasons. | 26 June 2015, 14:11:43 UTC |
966282e | Pierre-Yves Strub | 26 June 2015, 08:20:50 UTC | Delete unused theory: map_why / intcore / realcore | 26 June 2015, 14:11:37 UTC |
6428569 | Pierre-Yves Strub | 25 June 2015, 19:09:17 UTC | Push core/hard-coded types/ops to a Pervasive theory. Conflicts: src/ec.ml Conflicts: src/ecScope.ml | 26 June 2015, 14:11:09 UTC |
dfb2351 | Pierre-Yves Strub | 06 April 2015, 13:14:23 UTC | Remove old SMT interface & Why3 import The system is still unusable - its standard library as to be updated. Conflicts: src/ecEnv.ml src/ecEnv.mli src/ecHiGoal.ml src/ecHiGoal.mli src/ecHiTacticals.ml src/ecLowGoal.ml src/ecLowGoal.mli src/ecParser.mly src/ecParsetree.ml src/ecScope.ml src/why3/ecWhy3.ml src/why3/ecWhy3.mli | 26 June 2015, 14:08:10 UTC |
42d17e4 | Pierre-Yves Strub | 26 June 2015, 13:56:44 UTC | Recast low-level errors into user-local ones for `split`, `left` and `right`. [fix #17211] | 26 June 2015, 13:56:44 UTC |
6ff1147 | Pierre-Yves Strub | 26 June 2015, 12:36:09 UTC | `merlin` configuration file. | 26 June 2015, 12:36:09 UTC |
a4bd813 | Pierre-Yves Strub | 26 June 2015, 11:17:40 UTC | Partially revert "Fix local variables names clash in pretty-printer" This reverts commit d643e6636f04f96ff5b5b93c1316e2587bac2ebd. [fix #17214] | 26 June 2015, 11:18:25 UTC |
47fa131 | Pierre-Yves Strub | 26 June 2015, 11:02:51 UTC | Right handling of paths when requir'ing theories from prelude. Conflicts: src/ecScope.ml | 26 June 2015, 11:05:28 UTC |
c2bf74b | Pierre-Yves Strub | 26 June 2015, 07:38:28 UTC | Fix bug related to generation of fresh local hypotheses names. | 26 June 2015, 07:38:28 UTC |
843965e | Pierre-Yves Strub | 25 June 2015, 19:02:40 UTC | Remove wrongly committed files. | 25 June 2015, 19:02:40 UTC |
0cb0aaf | Pierre-Yves Strub | 25 June 2015, 14:51:26 UTC | Add `rewrite ... in ...` variant of `rewrite` Allows to use rewrite in hypotheses. The `in` only applies to the main goal (i.e. not to side goals). This construct is flagged as experimental. [fix #17208] | 25 June 2015, 15:04:58 UTC |
509fb50 | François Dupressoir | 25 June 2015, 10:23:57 UTC | Fixing the parts of the standard lib that can be fixed. | 25 June 2015, 10:23:57 UTC |
635e8fc | François Dupressoir | 25 June 2015, 09:41:38 UTC | PRP: adding a layer of abstraction to allow better black-box use. | 25 June 2015, 09:41:43 UTC |
8cc9bfd | Pierre-Yves Strub | 24 June 2015, 21:08:24 UTC | Library: lists: linking mem / nth. | 24 June 2015, 21:08:24 UTC |
2acc520 | Pierre-Yves Strub | 23 June 2015, 20:21:18 UTC | refactoring: factor out part of NewDistr. New modules are: - RealExtra: axiomatization of the real lub - RealSeq: real sequence - RealSeries: real series | 24 June 2015, 14:09:26 UTC |
1ea87c6 | Pierre-Yves Strub | 24 June 2015, 13:06:37 UTC | real/int ordering subsumed by core number theory. | 24 June 2015, 13:07:20 UTC |
6f8f464 | Pierre-Yves Strub | 24 June 2015, 10:47:41 UTC | Equip `real` with its field structure. | 24 June 2015, 10:48:10 UTC |
c876f84 | Pierre-Yves Strub | 24 June 2015, 10:47:23 UTC | Add missing copyrights + cleaning spacing. | 24 June 2015, 10:48:00 UTC |
017e0c6 | Pierre-Yves Strub | 24 June 2015, 10:16:30 UTC | Remove hard-coded tuple induction principles. | 24 June 2015, 10:16:36 UTC |
831440a | Pierre-Yves Strub | 24 June 2015, 10:14:31 UTC | prelude: temporary operators reflecting forall/exists. Should be removed when #17209 is fixed. | 24 June 2015, 10:14:57 UTC |
f37283a | Pierre-Yves Strub | 24 June 2015, 10:09:45 UTC | Library: lists: extra lemmas on `rem`. | 24 June 2015, 10:10:48 UTC |
13c9d73 | François Dupressoir | 24 June 2015, 09:37:28 UTC | PRP theory now takes the inverse permutation as parameter. Also added security notion for Strong PRP, and generic result that every Strong PRP is a PRP. | 24 June 2015, 09:37:36 UTC |
e2b0c63 | Pierre-Yves Strub | 23 June 2015, 12:55:19 UTC | pretty-printer: bug fix. Fix missing parentheses around anonymous proc. argument types. [fix #17206] | 23 June 2015, 12:55:19 UTC |
4a91204 | Pierre-Yves Strub | 23 June 2015, 12:15:00 UTC | Libraries: more on distribution (std. def.) | 23 June 2015, 12:15:00 UTC |
078b2cf | Pierre-Yves Strub | 22 June 2015, 14:34:26 UTC | Axiomatizing the def. of pr(E). | 22 June 2015, 14:34:34 UTC |
ad4f41a | François Dupressoir | 22 June 2015, 12:15:24 UTC | Cleaning up new version of ditributions on sets (form only). | 22 June 2015, 12:15:24 UTC |
4ff282c | François Dupressoir | 22 June 2015, 11:15:43 UTC | [Libraries] Only remaining instances of 'smt full' are those that do not go through with 'smt all'. Note that NewRealOrder.ec also has some admits that have been tagged as issues with the SMT-LIB connections by whoever. | 22 June 2015, 11:15:43 UTC |
2d69fa5 | Pierre-Yves Strub | 19 June 2015, 17:38:06 UTC | In proc., it is not mandatory anymore to store the result of a procedure call. [close #17204] | 19 June 2015, 17:38:06 UTC |
aa34347 | Pierre-Yves Strub | 19 June 2015, 16:14:57 UTC | parser: support for new syntax for assignments in var. declarations [fix #17205] | 19 June 2015, 16:14:57 UTC |
67310f9 | François Dupressoir | 19 June 2015, 15:34:19 UTC | [Libraries] Minor. | 19 June 2015, 15:34:23 UTC |
986f706 | Pierre-Yves Strub | 17 June 2015, 14:15:49 UTC | In pattern-matching: restore old unification state on failure. [fix #17198] | 17 June 2015, 14:15:49 UTC |
78a119c | Pierre-Yves Strub | 17 June 2015, 14:14:56 UTC | pretty-printer (bis): use new notations (<-, <$, <@) everywhere. | 17 June 2015, 14:14:56 UTC |
f00796d | Pierre-Yves Strub | 17 June 2015, 14:04:44 UTC | pretty-printer: use new notations (<-, <$, <@) everywhere. | 17 June 2015, 14:04:44 UTC |
a2dc86c | Pierre-Yves Strub | 17 June 2015, 13:22:00 UTC | Fix bugs related to operators renaming in NewDistr. | 17 June 2015, 13:22:25 UTC |
d7a5d9d | Pierre-Yves Strub | 17 June 2015, 13:21:48 UTC | Fix shadowing in pretty-printer of global op/pred names. When an operator/predicate name is shadowed by a local variable, do pretty-print a qualified name to disambiguate the resolution. This patch also add some debug functions for printing type variables instances of operators/predicates. [fix #17203] | 17 June 2015, 13:21:48 UTC |
db61759 | Pierre-Yves Strub | 17 June 2015, 09:06:28 UTC | Some facts about big summation (in a group) | 17 June 2015, 09:06:28 UTC |
e671281 | Pierre-Yves Strub | 17 June 2015, 06:20:33 UTC | Bigop: merge + nosmt + renaming - merge old BigOp theory (old theory deleted) - add `nosmt` to nearly all bigops lemmas - rename `big_nat_*` to `big_int_*` | 17 June 2015, 06:20:53 UTC |
64b8cb9 | Pierre-Yves Strub | 17 June 2015, 05:56:27 UTC | [rewrite]: all global symbols now act as a rewrite base. The rewrite base of the qsymbol `p` is composed of all accessible lemmas that `p` resolves to. | 17 June 2015, 05:56:44 UTC |
68f9520 | Pierre-Yves Strub | 16 June 2015, 19:38:28 UTC | New syntax for assignment / sampling / procedure call. Following Alley's idea: * `x <- e` stands for assigning the expression `e` in the left-value `x` * 'x <$ e` stands for assigning the result of sampling from the distribution expression `e` in the left-value `x` * 'x <@ X.f()` stands for assigning the result of the procedure call `X.f()` to the left-value `x` The old syntax (`x = e`, `x = $e`, `x = X.f()` when `X.f()` does not contain functor applications are still active. However, the pretty-printer makes use of the new notation. The unused syntax `x <- X.f()` has been removed. [fix #17184] | 16 June 2015, 19:38:44 UTC |
45ca71a | Benjamin Gregoire | 16 June 2015, 14:49:17 UTC | instantiate bigop with standard operators | 16 June 2015, 14:49:36 UTC |
d334eb3 | Pierre-Yves Strub | 16 June 2015, 10:03:42 UTC | Localization of errors encoutered in required libraries. [fix #17200] | 16 June 2015, 10:03:42 UTC |
c11fdd2 | Pierre-Yves Strub | 16 June 2015, 09:11:08 UTC | Low intro: do nothing is list of ids is empty. | 16 June 2015, 09:12:32 UTC |
aeae276 | Pierre-Yves Strub | 16 June 2015, 08:34:57 UTC | Weak form of keyed macthing. | 16 June 2015, 08:34:57 UTC |
e5933e9 | Pierre-Yves Strub | 15 June 2015, 21:06:22 UTC | PG: when no prompt is avail., should assume that weak-check is not enabled. [fix #17199] | 15 June 2015, 21:06:22 UTC |
c011738 | Pierre-Yves Strub | 15 June 2015, 20:52:11 UTC | Refactor integer intervals theory + proofs. | 15 June 2015, 20:52:11 UTC |
a79efa9 | Pierre-Yves Strub | 15 June 2015, 15:07:18 UTC | bigop: new properties about big/Z (assuming a theory of integer intervals) | 15 June 2015, 15:37:23 UTC |
6fa3c4a | Benjamin Gregoire | 15 June 2015, 14:41:18 UTC | add eta in conversion | 15 June 2015, 14:41:34 UTC |
ec0fce2 | Pierre-Yves Strub | 15 June 2015, 14:29:48 UTC | newBigop: use new Pred.ec notations. | 15 June 2015, 14:29:48 UTC |