max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
11595 commits 1 branch 0 tags 5.3 GiB
Commit graph

168 commits

Author SHA1 Message Date
Leonardo de Moura
19cf5e916b chore(script/gen_constants_cpp): generates a warning if automatically generated C++ function is not used in the source code 2017-02-21 12:05:41 -08:00
Leonardo de Moura
d1d5428808 feat(library): add check_constants.lean validation, cleanup unused names, minor stdlib fixes 2017-02-21 10:45:31 -08:00
Sebastian Ullrich
d15591a2d8 feat(library,frontends/lean): expose parser to Lean and use for parsing tactic parameters 2017-02-17 13:45:56 +01:00
Leonardo de Moura
edd5e97045 feat(frontends/lean/elaborator): coercion from (decidable) Prop to bool 
This is a hard coded extra case. It is not an instance of has_coe.
Even if we change has_coe to accomodate this case, it will not be a
satisfactory solution because this coercion depends on the element and
not the type, and the element usually contains metavariables.

We should eventually write a tactic for synthesizing coercions.
 2017-02-14 18:41:32 -08:00
Leonardo de Moura
1a698d9065 refactor(library/arith_instance_manager): rename to arith_instance, avoid copy&paste, and add support for norm_num 2017-02-12 19:11:58 -08:00
Rob Lewis
46a46c9ee0 feat(norm_num): handle nat subtraction as a special case 2017-02-12 17:15:08 -08:00
Leonardo de Moura
9210e45da0 feat(frontends/lean): add notation for ';' and '<|>' in the tactic interactive mode 2017-02-10 22:53:30 -08:00
Leonardo de Moura
c8bbb34e2a feat(frontends/lean): add auto_param gadget 2017-02-09 15:49:10 -08:00
Leonardo de Moura
a8c91aa6fc fix(library/compiler/preprocess): expand eq.cases_on 
The code generator was failing to erase eq.cases_on.
 2017-02-07 21:19:01 -08:00
Leonardo de Moura
55aa2023f4 feat(frontends/lean): add support for monad_fail type class in 'do' blocks 2017-02-05 20:09:08 -08:00
Gabriel Ebner
95068e4e79 feat(library/sorry): make sorry a macro 2017-02-05 14:01:03 +01:00
Leonardo de Moura
6e7929252f feat(frontends/lean, library/init): add 'thunk' gadget 
We can now write
   trace "hello" t
instead of
   trace "hello" (fun _, t)
 2017-01-31 18:41:59 -08:00
Leonardo de Moura
5da8b205b9 feat(library/type_context, frontends/lean/elaborator): type classes with output parameters 2017-01-30 18:32:54 -08:00
Leonardo de Moura
d34386fef7 perf(frontends/lean/tactic_notation): closes #1345 
We can now elaborate
https://gist.github.com/gebner/439273deee592603190d4f8b4447295b
in 1.6 secs and using less than 500Kb of stack space.
It was takins 44 secs and 5Mb before this commit.

Two modifications:
1) Use pre_monad.seq instead of pre_monad.and_then.
They have the same implementation, but seq is not marked as [inline].

2) Modify how we concatenate the tactics in a begin...end block.
Before: (((a_1 ++ a_2) ++ a_3) ++ a_4)
After:  ((a_1 ++ a_2) ++ (a_3 ++ a_4))
 2017-01-30 14:13:53 -08:00
Leonardo de Moura
a6f26f0b74 chore(library): poly_unit ==> punit 
psum, pprod and punit are used internally.

see #1341
 2017-01-30 11:54:00 -08:00
Leonardo de Moura
bf9f7560f7 feat(frontends/lean): (Type u) can't be a proposition 
(Type u)  is the old (Type (u+1))
(PType u) is the old (Type u)
Type*     is the old (Type (_+1))
PType*    is the old Type*

The stdlib can be compiled, but we still have > 70 broken tests

See discussion at #1341
 2017-01-30 11:54:00 -08:00
Leonardo de Moura
9107439bce feat(frontends/lean/elaborator): default parameter prototype 
See #1340
 2017-01-27 16:32:22 -08:00
Leonardo de Moura
cce88c6190 refactor(frontends/lean): interactive tactic support 
After this commit, new interactice tactic classes can be added without
writing C++ code (see example: tests/lean/run/my_tac_class.lean).

The tactic_evaluator was simplified, and all the complexity has been
moved to tactic_notation, and lean code.

We can now inspect the intermediate states produced by the rewrite
tactic.

The function (@scope_trace _ line col thunk) can be used to position trace
messages produced by thunk. If line/col are not provided (i.e., we
just write (scope_trace thunk)), then line/col are filled with the
position of this term by the elaborator.

We can visualize the intermediate tactic states inside nested blocks
such as (try { ... })

The new infrastructure can be used to implement custom tactic_state
pretty printers.
 2017-01-21 22:38:47 -08:00
Leonardo de Moura
e8839cbcdc feat(library/app_builder): add mk_eq_mpr that removes unnecessary propext 2017-01-20 20:27:41 -08:00
Leonardo de Moura
5e3f26ec95 feat(library/tactic/smt/congruence_closure): propagate not_exists 2017-01-06 14:00:36 -08:00
Leonardo de Moura
7ba889b5cf feat(frontends/lean/tactic_notation): try/repeat for smt_tactic in interactive mode 2017-01-05 18:31:57 -08:00
Leonardo de Moura
5f2b247af9 feat(frontends/lean/tactic_evaluator): step-by-step evaluation for 'begin [smt] ... end' blocks 2017-01-04 14:06:44 -08:00
Leonardo de Moura
ca6d3743c7 feat(library/tactic/smt): add mk_eq_true_intro mk_of_eq_true mk_eq_false_intro mk_not_of_eq_false 2017-01-02 13:39:16 -08:00
Leonardo de Moura
5d825483c4 refactor(library/init/meta/interactive): tactic.interactive.types ==> interactive.types 
Motivation: we will use auto-quotation for other tactic monads
 2016-12-30 18:06:41 -08:00
Leonardo de Moura
bb37b33237 fix(library/tactic/ac_tactics): binary.left_comm ==> left_comm 2016-12-28 21:23:07 -08:00
Leonardo de Moura
b5c1b429e7 feat(library/tactic/ac_tactics): add ac_manager helper class 2016-12-27 17:57:56 -08:00
Leonardo de Moura
9b35adfc8c feat(library/tactic/congruence/congruence_closure): add support for constructor equalities 2016-12-25 12:47:17 -08:00
Leonardo de Moura
3061d8b9a3 feat(library): add mk_int_val_ne_proof 2016-12-24 15:22:31 -08:00
Leonardo de Moura
b1b694a532 fix(library/tactic/congruence/congruence_closure): bugs, and add basic cc tactic 2016-12-23 19:30:45 -08:00
Leonardo de Moura
d431d7274a feat(library/tactic/congruence/congruence_closure): hard code support for ne 2016-12-23 15:37:05 -08:00
Leonardo de Moura
48cd421852 feat(library/tactic/congruence): add congruence closure basics 2016-12-21 20:46:25 -08:00
Leonardo de Moura
cc077554b5 fix(library/tactic/change_tactic): use id_locked in the change tactic to create checkpoint 
closes #1260
 2016-12-21 11:29:03 -08:00
Leonardo de Moura
6577cc87a3 feat(library): add pre_monad 
closes #1235
 2016-12-08 12:48:55 -08:00
Leonardo de Moura
98fbe76f30 feat(library/comp_val): add mk_string_val_ne_proof 2016-11-23 13:19:24 -08:00
Leonardo de Moura
680bab8bb8 feat(library/comp_val): add mk_fin_val_ne_proof and mk_char_val_ne_proof 2016-11-23 10:25:04 -08:00
Leonardo de Moura
f4b1413cee feat(library/comp_val): add mk_nat_val_lt_proof and mk_nat_val_le_proof 2016-11-22 15:14:10 -08:00
Leonardo de Moura
227e16ea6b feat(library): add mk_nat_val_ne_proof 
Procedure for building an efficient disequality proof for natural
number values encoded in binary.
 2016-11-19 17:02:48 -08:00
Leonardo de Moura
88d2f07567 feat(frontends/lean/tactic_notation): switch to proof-term mode when calc/suppose/assume/have/show occurs in a tactic block 2016-11-18 16:57:31 -08:00
Leonardo de Moura
e16e9880f7 chore(library/system): enforce Lean naming conventions IO ==> io 2016-11-17 11:27:37 -08:00
Leonardo de Moura
3628870121 feat(library/tactic/vm_monitor): extend VM introspection API 2016-11-15 15:05:46 -08:00
Leonardo de Moura
fffe69fdf9 feat(library/vm,library/tactic/vm_monitor): use optionT to define vm monad 2016-11-14 16:13:56 -08:00
Leonardo de Moura
7232e3a076 feat(library/vm/vm): invoke debugger (aka vm_monitor) 2016-11-14 14:45:49 -08:00
Leonardo de Moura
205d524409 refactor(library/tactic/simplify): delete old simplifier 2016-10-19 14:03:14 -07:00
Leonardo de Moura
4d52de6f33 refactor(library/tactic/simplify): add simplify subclasses, and use new simplifier at nested 2016-10-18 16:18:25 -07:00
Leonardo de Moura
7465529445 feat(library/tactic): 'eval_expr' tactic skeleton 2016-10-03 16:26:28 -07:00
Leonardo de Moura
c0022253a7 feat(frontends/lean/tactic_notation): allow lemmas to be removed 2016-09-30 19:53:51 -07:00
Leonardo de Moura
fd6dc8154a feat(library/init/meta/interactive): add interactive tactics 2016-09-30 19:02:45 -07:00
Leonardo de Moura
23ce2b0587 feat(frontends/lean/tactic_notation, library/init/meta/interactive): add "interactive" versions of define/assert/definev/assertv/note tactics 2016-09-29 18:48:32 -07:00
Leonardo de Moura
c6ec659bf5 feat(frontends/lean): improve 'begin...end' blocks 2016-09-27 13:34:11 -07:00
Leonardo de Moura
c6609543d0 chore(library/init): minor changes 2016-09-27 07:23:51 -07:00