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

51 commits

Author SHA1 Message Date
Leonardo de Moura
de7c850782 feat(kernel/converter): relax is_def_eq test for local constants and meta-variables 2014-10-14 15:31:57 -07:00
Leonardo de Moura
d4236e40b4 feat(kernel/type_checker): expose is_opaque 2014-09-25 11:19:54 -07:00
Leonardo de Moura
da481c3274 refactor(kernel): explicit initialization/finalization 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-09-24 10:12:28 -07:00
Leonardo de Moura
49d5af473d refactor(kernel): remove support for proof irrelevant classes 
Motivation: we can use Prop
 2014-09-19 07:32:07 -07:00
Leonardo de Moura
ea1bae0143 refactor(kernel/converter): replace extra_opaque_set with predicate 
It gives us more flexibility.
 2014-09-17 17:05:13 -07:00
Leonardo de Moura
79acd3e1b7 fix(kernel/converter): missing case 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-28 15:21:57 -07:00
Leonardo de Moura
04d9eb17d1 feat(kernel/conveter): improve support for proof irrelevant in the converter 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-25 11:19:18 -07:00
Leonardo de Moura
9588336c15 refactor(kernel/type_checker): remove "global" constraint buffer from type_checker, and use constraint_seq instead 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-20 16:46:19 -07:00
Leonardo de Moura
562926e7ad refactor(kernel/instantiate): add functions instantiate_value_univ_params and instantiate_type_univ_params 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-12 17:40:30 -07:00
Leonardo de Moura
4986226e41 fix(kernel/converter): missing delay_check case 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-09 08:07:41 -07:00
Leonardo de Moura
8e222e6244 fix(kernel/converter): missing constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-31 12:25:35 -07:00
Leonardo de Moura
450131692a fix(library/converter): missing constraint on eta expansion 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-30 10:43:47 -07:00
Leonardo de Moura
faee08591f fix(*): make sure elaborator and type_checker use the same "rules" for treating opaque definitions 
This is a big change because we have to store in constraints whether we can use the "relaxed" rules or not.
The "relaxed" case says that when type checking the value of an opaque definition we can treat other opaque definitions in the same module as transparent.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-27 12:12:54 -07:00
Leonardo de Moura
5ad6d5cbc4 feat(kernel/converter): add eta-expansion to converter, this is important when terms contains metavariables 
For example, consider the unification constrains

    fun (x : A), f (?m x)  =?=  f

Eta-reduction is not applicable since (?m x) is not a variable.
However, if we eta-expand the left-hand-side, we get

   fun (x : A), f (?m x)  =?=  fun (x : A), f x

which is reduced to

      (?m x) =?= x

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-22 16:24:02 -07:00
Leonardo de Moura
5eaf04518b refactor(*): rename Bool to Prop 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-22 09:43:18 -07:00
Leonardo de Moura
c97b4c7725 perf(kernel/converter): improve is_def_eq_binding 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-16 07:33:45 +01:00
Leonardo de Moura
80d1a6b993 perf(kernel/converter): do not cache easy cases 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-12 05:39:14 +01:00
Leonardo de Moura
59755289e4 feat(library/unifier): case split on constraints of the form (f ...) =?= (f ...), where f can be unfolded, and there are metavariables in the arguments 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-05 15:52:40 -07:00
Leonardo de Moura
e366aadad0 refactor(library/converter): expose is_opaque predicate in the converter interface 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-05 12:05:23 -07:00
Leonardo de Moura
a52c9f4e2b feat(library/unifier): add option 'unifier.unfold_opaque', remove option 'unifier.use_exceptions' (the user should not be able to change this) 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-05 09:43:16 -07:00
Leonardo de Moura
7fb2b0f6d8 feat(kernel): add method 'may_reduce_later' to normalizer_extension, and improve unifier 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-07-03 22:31:05 -07:00
Leonardo de Moura
6e6f778ecf fix(kernel/converter): missing case for local constants 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-30 12:57:25 -07:00
Leonardo de Moura
cb000eda13 refactor(kernel): store binder_infor in local constants 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-30 11:37:46 -07:00
Leonardo de Moura
a8f9594046 refactor(kernel/instantiate): rename instantiate_params to instantiate_univ_params 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-29 12:09:55 -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
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
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
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
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
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
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
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
33bbcd9526 chore(kernel/declaration): rename declaration::get_params to declaration::get_univ_params 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-06-02 16:20:34 -07:00
Leonardo de Moura
e206fcc1af perf(kernel/type_checker): reduce the overhead of creating delayed_justification objects, a huge number of them is created when type checking applications 
We reduce the cost by avoiding the allocation of std::functional objects, and the unnecessary increment/decrement of reference counters.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-27 23:16:52 -07:00
Leonardo de Moura
8872d4a531 refactor(kernel): rename definition class to declaration 
The name was misleading since not every declaration is a definition.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-20 10:41:38 -07:00
Leonardo de Moura
edc8af7bb3 refactor(kernel): reduce code duplication 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-19 11:11:19 -07:00
Leonardo de Moura
5ce134e24e chore(kernel): binder => binding where appropriate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-17 11:37:27 -07:00
Leonardo de Moura
69e72c278d feat(kernel): add proof irrelevance for classes 
We can use this feature to implement proof irrelevance for Identity types.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 15:30:32 -07:00
Leonardo de Moura
862c5e354d feat(kernel/expr): attach auxiliary name (for pretty printing) into local constants 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 13:08:09 -07:00
Leonardo de Moura
40b3129e7b refactor(kernel): improve names 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-16 11:28:05 -07:00
Leonardo de Moura
3a19d9fee1 refactor(kernel): revise macro_definition API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 13:53:10 -07:00
Leonardo de Moura
08ac9c1f05 feat(kernel): add is_def_eq predicate in the extension_context API 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-15 13:53:10 -07:00
Leonardo de Moura
7b15e558a2 refactor(kernel/converter): implement eta in whnf instead of is_def_eq. 
Without cumulativity, we do not have problems with Eta at whnf anymore.
When we had cumulativity, we could not not simply reduce
     (fun x : A, f x) ==> f
This step is correct only if domain(f) was definitionally equal to f.
Here is a problematic example for systems with cumulativity
Given, f : Type.{2} -> Bool
     (fun x : Type.{1}, f x)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-12 17:49:53 -07:00
Leonardo de Moura
ff9004dae2 refactor(kernel): add level normalizer, is_equivalent predicate, switch to is_equivalent in the type checker, fix bugs in is_lt predicate 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-11 18:05:02 -07:00
Leonardo de Moura
7176181b42 refactor(kernel/converter): cleanup and remove universe cumulativity support 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-09 20:43:11 -07:00
Leonardo de Moura
9d96f24766 refactor(kernel): remove convertability constraints 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-09 20:25:27 -07:00
Leonardo de Moura
6fb7039746 refactor(kernel): use structural hashing in type_checker and converter 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-05-01 10:41:53 -07:00