(WIP) Expose type_context_old as a monad.

[EdAyers]

what?

Under the hood, tactic uses a C++ class called type_context_old.This PR introduces meta constant tco : Type -> Type which lets you use this directly. This lets you do more 'unsafe' operations like directly declaring and assigning metavariables, as well as use temporary metavariables. type_context_old is mutable, but all of the mutation occurs through interacting with the monad.

why?

On my tactic writing adventures, I found there were situations where it was very frustrating to always go via tactic and not be able to manipulate the mvar context. tactic deliberately limits how you interact with the metavariable context so you can't produce dodgy terms that are rejected by the kernel.

This also means that some constants like intro_core and match_pattern can be implemented entirely in Lean (see test/lean/tco.lean). Although of course this will incur a performance penalty.

should it be merged at all?

There is a fair case that this doesn't belong in Lean, because it is exposing an internal class and just adds cruft. But I have written the code so I thought I should present it as a potential feature for Lean 3.5c.

what needs to happen before merging?

• naming. lc is a terrible name for local_context. As is the name tco, maybe call it mvar_context_monad?. I think it would make sense to put it all in a namespace like unsafe so that it doesn't break anything and beginners know that they can ignore it.
• Feature parity with tactic where it makes sense. At the moment I have just been adding constants as I need them. It would be cool if in principle you could implement tactic from tco.
• type_context_old is a mutable class so need to double check that it doesn't cause tactic_state to mutate or some other pureness-breaking.
• is it efficient? It will never be as fast as C++ but maybe the way I am implementing it causes avoidable allocations or boxing/unboxing.

[gebner]

As is the name tco, maybe call it mvar_context_monad

Please just ignore the _old at the end, and call it tc. For most of Lean 3's life, this class was called type_context. It only got renamed to type_context_old in the preparation for Lean 4.

EDIT: or maybe don't abbreviate it at all, and call it type_context and local_context.

[EdAyers]

Any ideas why this test would be failing on just one configuration of travis?

380/1327 Test #284: leantest_non_meta_rec_fn.lean ...............................***Failed    0.05 sec

-- testing non_meta_rec_fn.lean

-- using result from test_all.sh

--- non_meta_rec_fn.lean.expected.out	2019-10-28 00:12:20.000000000 +0000

+++ non_meta_rec_fn.lean.produced.out	2019-10-28 00:25:23.000000000 +0000

@@ -1,4 +1,4 @@

-non_meta_rec_fn.lean:3:36: error: failed to prove recursive application is decreasing, well founded relation

+non_meta_rec_fn.lean:3:0: error: failed to prove recursive application is decreasing, well founded relation

   @has_well_founded.r true (@has_well_founded_of_has_sizeof true (default_has_sizeof true))

 Possible solutions: 

   - Use 'using_well_founded' keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs.

ERROR: file non_meta_rec_fn.lean.produced.out does not match non_meta_rec_fn.lean.expected.out

[bryangingechen]

I've seen this sort of thing before on the macOS builds, where the build produces n:0 instead of n:m. (Here, the test expects 3:36, but the build produced 3:0). It would be good to track down exactly what's going wrong here, but for now I'd suggest re-running that job and seeing if it goes away.