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

1115 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
cb06d0a959 test(frontends/lean): add example showing higher order matching is working, and is useful 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 20:18:48 -07:00
Leonardo de Moura
02c22e509d fix(tests/lean): remove obsolete comments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 20:16:02 -07:00
Leonardo de Moura
250cf70410 test(frontends/lean): all 'bad' examples can be solved 
Move them to the main test directory

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 20:12:58 -07:00
Leonardo de Moura
c1c1af4b98 fix(tests/lean): add parenthesis 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 20:04:50 -07:00
Leonardo de Moura
f0e149d77b fix(frontends/lean/pp): fix how Type expressions are pretty printed 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 20:02:34 -07:00
Leonardo de Moura
a5c3829d1b feat(kernel): add unexpected_metavar_occurrence exception 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 19:56:44 -07:00
Leonardo de Moura
83907d7c73 fix(elaborator): max constraints 
elaborator was not handling max constraints where one of the arguments was a Bool. Example:
      ctx |- max(Bool, Type) == ?M

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 19:27:57 -07:00
Leonardo de Moura
46b9b2114a fix(tests/lean): adjust error messages in the expected output 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 19:27:26 -07:00
Leonardo de Moura
65a514ad8a fix(frontends/lean/parser): option propagation 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 19:04:06 -07:00
Leonardo de Moura
576b4e2169 fix(frontends/lean/pp): missing comma when printing contexts 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 19:00:24 -07:00
Leonardo de Moura
df07a84d11 feat(frontends/lean/parser): display elaborator error messages 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 18:48:53 -07:00
Leonardo de Moura
ca6a6d71e5 fix(kernel/printer): bug when printing let expression 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 18:05:23 -07:00
Leonardo de Moura
e55fb4f165 fix(tests/lean): adjust expected results, the new result is also acceptable 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 17:54:09 -07:00
Leonardo de Moura
e3efe39eeb fix(elaborator): fix bug in higher-order matching/unification 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 17:53:37 -07:00
Leonardo de Moura
d1a2a4ea7e feat(frontends/lean/elaborator): add support for coercions in let declarations 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 17:01:06 -07:00
Leonardo de Moura
872b698bc3 feat(elaborator): add option m_assume_injectivity for getting more concise solutions 
We may miss solutions, but the solutions found are much more readable.
For example, without this option, for elaboration problem

Theorem Example4 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧ d = c)) : (h a c) = (h c a) :=
    DisjCases H
              (fun H1 : _,
                   let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1))
                   in CongrH AeqC (Symm AeqC))
              (fun H1 : _,
                   let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1)
                   in CongrH AeqC (Symm AeqC))

the elaborator generates

Theorem Example4 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : (h a c) = (h c a) :=
    DisjCases
        H
        (λ H1 : if
               Bool
               (if Bool (a = b) (if Bool (if Bool (if Bool (b = e) (if Bool (b = c) ⊥ ⊤) ⊤) ⊥ ⊤) ⊥ ⊤) ⊤)
               ⊥
               ⊤,
           let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1)) in CongrH AeqC (Symm AeqC))
        (λ H1 : if Bool (if Bool (a = d) (if Bool (d = c) ⊥ ⊤) ⊤) ⊥ ⊤,
           let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1) in CongrH AeqC (Symm AeqC))

The solution is correct, but it is not very readable. The problem is that the elaborator expands the definitions of \/ and /\.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 16:47:50 -07:00
Leonardo de Moura
d2f9c24d3c fix(tests/lean): adjust tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 15:42:17 -07:00
Leonardo de Moura
a7f94b55db fix(frontends/lean/elaborator): fix bugs and adjust tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 15:29:56 -07:00
Leonardo de Moura
bbc265ded4 feat(frontends/lean): hook new elaborator in the default frontend 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 15:14:29 -07:00
Leonardo de Moura
c9f7b8bce2 feat(frontends/lean): add get_coercions method 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 14:38:09 -07:00
Leonardo de Moura
71ccec5b9e refactor(frontends/lean/elaborator): delete old_elaborator, and create frontend_elaborator class that will be based on library/elaborator/elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-24 10:45:59 -07:00
Leonardo de Moura
449454efdb fix(debug): remove typeid information from assertion, the names are mangled and are not very useful 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 16:41:51 -07:00
Leonardo de Moura
434c33f225 feat(metavar): automatically apply beta-reduction when instantiating metavariable applications (i.e., expressions of the form (?m a)), when the metavariable is a lambda 
This feature is useful for problems that require higher-order matching and/or unification.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 16:35:50 -07:00
Leonardo de Moura
873e56844a refactor(beta_reduction): add function apply_beta 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 16:03:52 -07:00
Leonardo de Moura
f1e0d6ec29 refactor(beta_reduction): move beta reduction functions to the kernel, delete reduce.cpp file and tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 15:44:26 -07:00
Leonardo de Moura
c1e451151a feat(replace_visitor): add an abstract class for applying transformations on expressions 
I also removed replace_using_ctx since it is subsumed by the new class.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 15:01:37 -07:00
Leonardo de Moura
13531b7d3e refactor(kernel): rename trace to justification 
Motivations:

- We have been writing several comments of the form "... trace/justification..." and "this trace object justify ...".
- Avoid confusion with util/trace.h

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 13:42:17 -07:00
Leonardo de Moura
8e1a75ce1c feat(elaborator): only process upper bound constraints when the corresponding metavariable does not have lower bound and max constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 13:09:13 -07:00
Leonardo de Moura
172567a2fb feat(elaborator): add support for upper bounds, max constraints, and fix bugs 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 12:01:39 -07:00
Leonardo de Moura
17b48010b7 fix(unification_constraint): fix printer for max constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 12:00:29 -07:00
Leonardo de Moura
274b11530f feat(metavar): improve apply_local_context 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 11:59:36 -07:00
Leonardo de Moura
b57f492e2d fix(kernel/printer): improve printer for Type expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-23 11:58:49 -07:00
Leonardo de Moura
c635c16637 refactor(ho_unifier): remove ho_unifier, it has been subsumed by the elaborator class 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 17:51:54 -07:00
Leonardo de Moura
019f64671b fix(elaborator): add basic support for flex-flex pairs, add more tests, fix bug when enumerating different solutions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 17:49:37 -07:00
Leonardo de Moura
80a507cf45 refactor(tests/frontends/lean/implicit_args): remove implicit_args unit tests from frontends/lean, all tests were moved to tests/library/elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 16:42:07 -07:00
Leonardo de Moura
7ad256131e feat(elaborator): add support for constraints of the form ?m[inst, ...] == t, fix bugs, add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 16:39:22 -07:00
Leonardo de Moura
891d22b3de feat(kernel/context): add method for remove context entries at positions [s, s+n). 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 15:52:24 -07:00
Leonardo de Moura
3fa4eac4ef fix(replace_using_ctx_fn): typo 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 15:46:11 -07:00
Leonardo de Moura
8142726923 fix(type_inferer): bug when inferring the type of free variables 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 15:41:22 -07:00
Leonardo de Moura
874f67c605 feat(normalizer): remove normalization rule t == t ==> true 
This normalization rule is not really a computational rule.
It is essentially encoding the reflexivity axiom as computation.
It can also be abaused. For example, with this rule,
the following definition is valid:

Theorem Th : a = a := Refl b

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 14:02:48 -07:00
Leonardo de Moura
5e61496381 test(elaborator): add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 13:45:20 -07:00
Leonardo de Moura
a5b4908f71 fix(elaborator): process_simple_ho_match and missing cases 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 13:45:04 -07:00
Leonardo de Moura
cb2c73cf37 feat(elaborator): add higher-order matching support to elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 11:22:00 -07:00
Leonardo de Moura
f4592da87f feat(elaborator): solve more unification constraints, add more tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:37 -07:00
Leonardo de Moura
c3e87f106f fix(kernel/trace): fix typo in depends_on 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:37 -07:00
Leonardo de Moura
dc51d35dc0 feat(library/type_inferer): add support for metavariables at type_inferer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:37 -07:00
Leonardo de Moura
7f96c07a01 refactor(library): rename light_checker to type_inferer 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
183f5a1ccf feat(elaborator): solve unification constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
a1710aeeb9 feat(elaborator): add trace objects for elaborator 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00
Leonardo de Moura
dc0e7a4472 feat(pos_info_provider): add position information provider for expressions 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2013-10-22 08:15:36 -07:00