michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
2848 commits 3 branches 0 tags 28 MiB
Commit graph

817 commits

Author SHA1 Message Date
Leonardo de Moura
ac03b3204a fix(kernel/formatter): add missing parentheses 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 12:07:28 -07:00
Leonardo de Moura
a70f8dd98e feat(kernel/inductive): mark parameters, type formers and indices as implicit parameters in the elimination rule 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 11:05:14 -07:00
Leonardo de Moura
cdc41244ae fix(kernel/justification): missing 'const' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-26 08:18:18 -07:00
Leonardo de Moura
acf8c13619 feat(kernel): add strict implicit arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 17:50:49 -07:00
Leonardo de Moura
1d4352aeb4 fix(kernel/converter): missing case: two constants c.{l1} and c.{l2} where l1 and l2 are structurally different but equivalent (or can be made equivalent) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 16:05:41 -07:00
Leonardo de Moura
c9133f33dd feat(kernel/expr): add flat_app auxiliary function 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 12:51:22 -07:00
Leonardo de Moura
5c40b466cc fix(kernel/type_checker): use the application to provide error location 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 10:42:58 -07:00
Leonardo de Moura
6ec5d768d0 fix(kernel/type_checker): bug in the app_delayed_justification object 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 10:09:45 -07:00
Leonardo de Moura
c427c5bdc9 feat(kernel/type_checker): improve 'declaration still has metavars' error message 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-25 08:51:33 -07:00
Leonardo de Moura
603dafbaf7 refactor(kernel): remove 'let'-expressions 
We simulate it in the following way:
1- An opaque 'let'-expressions (let x : t := v in b) is encoded as
      ((fun (x : t), b) v)
   We also use a macro (let-macro) to mark this pattern.
   Thus, the pretty-printer knows how to display it correctly.

2- Transparent 'let'-expressions are eagerly expanded by the parser.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-24 16:27:27 -07:00
Leonardo de Moura
609aeae390 feat(kernel/type_checker): expose app_delayed_justification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-24 14:54:37 -07:00
Leonardo de Moura
d915f0cc32 refactor(kernel/converter): converter should fail instead of relying on unification hints for solving a constraint, the hints must be applied by the frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-24 09:00:14 -07:00
Leonardo de Moura
d8a8300a4f fix(kernel/expr): initialization problem 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 16:55:51 -07:00
Leonardo de Moura
a0e4dccdac refactor(kernel/constraint): rename choice constraint fields 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 13:52:03 -07:00
Leonardo de Moura
6d14de76f3 feat(kernel/constraint): add 'delayed' flag to choice constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-23 12:56:06 -07:00
Leonardo de Moura
228f51dcfa feat(library/unifier): add support for choice constraint 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 17:21:24 -07:00
Leonardo de Moura
c8a07dee53 feat(library/unifier): add unifier_plugin support, and unit test with plugin implemented using Lua 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 16:27:04 -07:00
Leonardo de Moura
25cb1bf6a1 fix(kernel/converter): use type_checker::scope to make sure we restore the cache, and remove constraints when is_def_eq fails in the converter 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 14:08:54 -07:00
Leonardo de Moura
a1d94d71ec refactor(kernel/converter): eliminate converter::context, use type_checker directly 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 13:52:47 -07:00
Leonardo de Moura
edb2e85898 refactor(kernel/type_checker): remove type_checker::imp 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 13:39:58 -07:00
Leonardo de Moura
644c387cfe refactor(kernel/constraint): rename: level constraints are also equality constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 10:50:47 -07:00
Leonardo de Moura
1c47bd4847 fix(kernel/converter): remove temporary workaround, and temporarily disable unit test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 10:39:22 -07:00
Leonardo de Moura
3953d4d122 feat(kernel/type_checker): add push/pop methods to type_checker, they control the cache, and allow the type checker to reuse results even when it is used inside of a backtracking search 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 09:58:05 -07:00
Leonardo de Moura
eca22edda3 fix(kernel/type_checker): restore type checker cache when a failure occurs, do not send constraints to add_cnstr_fn when a type checker failure occurrs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-22 09:00:32 -07:00
Leonardo de Moura
aac3830e31 fix(kernel/converter): add temporary fix, we need to be able to backtrack constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-21 20:08:39 -07:00
Leonardo de Moura
f9a21166f0 feat(kernel/type_checker): add type_checker::is_def_eq method that takes a justification as argument 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-21 20:08:39 -07:00
Leonardo de Moura
fedbf8595b feat(kernel/metavar): collect unassigned metavariables while instantiating 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-21 16:58:09 -07:00
Leonardo de Moura
37bee8c852 refactor(kernel/type_checker): simplify replace constraint_handler with closure 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-21 12:25:54 -07:00
Leonardo de Moura
2c3e3cb544 refactor(kernel/abstract): add abstract_locals, and remove abstract_p 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-21 12:25:54 -07:00
Leonardo de Moura
67088b130e refactor(kernel/constraint): simplify constraint interface, and add choice constraint 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-21 12:25:54 -07:00
Leonardo de Moura
16412daf39 feat(frontends/lean): add 'using' syntax sugar for adding expressions to the goal's context 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-20 11:58:05 -07:00
Leonardo de Moura
5c17411a86 fix(kernel/converter): relax is_def_eq test, for example is_def_eq(f(?m1), a) should generate a constraint instead of returning an error 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-20 09:46:58 -07:00
Leonardo de Moura
2954d10df5 refactor(kernel/converter): remove unnecessary exception 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-19 23:06:49 -07:00
Leonardo de Moura
05d1832425 refactor(kernel/type_checker): improve ensure_pi and ensure_sort APIs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-19 22:33:58 -07:00
Leonardo de Moura
0779db7ae9 fix(kernel): set module_idx on theorems, otherwise we are not able to import theorems that use opaque definitions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 16:56:11 -07:00
Leonardo de Moura
4f3da90443 feat(frontends/lean/builtin_exprs): add 'have' and 'show' expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 15:04:29 -07:00
Leonardo de Moura
07f2379dec refactor(kernel): add mk_local function that has only two arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 14:27:26 -07:00
Leonardo de Moura
21c54755a9 fix(kernel/converter): bug in is_def_eq 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 14:09:12 -07:00
Leonardo de Moura
2312f43443 fix(kernel/abstract): propagate tags when abstracting 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-16 13:00:13 -07:00
Leonardo de Moura
64cafd6875 feat(frontends/lean/notation_cmd): add 'notation' command 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-15 10:49:05 -07:00
Leonardo de Moura
961b0bfacf feat(kernel/type_checker): use argument position when reporting application type mismatch errors 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-15 10:06:53 -07:00
Leonardo de Moura
e7019ec840 feat(frontends/lean): add infixl/infixr/postfix/precedence commands, add support for storing notation in .olean files, add support for organizing notation into namespaces 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-14 22:13:25 -07:00
Leonardo de Moura
5aca452439 feat(library/aliases): add 'exceptions' and support for universes to add_aliases procedure, add for_each_universe method to environment 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-13 08:26:05 -07:00
Leonardo de Moura
d50376249f feat(library/aliases): add level aliases 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-12 12:35:02 -07:00
Leonardo de Moura
5a008717a4 feat(frontends/lean/parser): add parse_notation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-11 21:00:34 -07:00
Leonardo de Moura
e7d7996fa9 feat(frontends/lean/parser): add parser_binder(s) and abstract methods 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-11 18:51:12 -07:00
Leonardo de Moura
1a67cc7293 fix(kernel/for_each_fn): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-11 15:06:11 -07:00
Leonardo de Moura
fe6ab51c12 feat(kernel/inductive): add APIs for retrieving information about declared inductive datatypes, intro rules, and elimination rules 
The new API is important for implementing environment transformation procedures, and export Lean environment to different systems (e.g., Coq).

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-08 17:15:21 -07:00
Leonardo de Moura
1c49b4d85f chore(*): replace unique_lock with lock_guard when we do not need to use conditional variables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-07 20:55:25 -07:00
Leonardo de Moura
15f0899efb refactor(*): replace LEAN_THREAD_LOCAL with MK_THREAD_LOCAL_GET, the new macro uses the Boost thread_local_ptr instead of 'thread_local' directive 
Motivation: clang++ on OSX does not support 'thread_local'.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-07 10:18:36 -07:00