Rewrite Chamelean front-end as a Term Elaborator instead of a Command Elaborator

[ngernest]

More details in this Zulip discussion with Kyle Miller (from the Lean FRO):
https://leanprover.zulipchat.com/#narrow/channel/239415-metaprogramming-.2F-tactics/topic/Instantiating.20type.20parameters.20of.20a.20polymorphic.20inductive.20typ

Suppose we want to derive a (trivial) generator of lists which always produces the list [3].

Instead of implementing #derive_generator (fun (xs : List Nat) => xs = [3]) as a command and elaborating it (using CommandElabM), as suggested by Kyle, we should instead start with

#derive_generator funExpression

then expand that to

instance : ArbitrarySuchThat _ funExpression := derive_arbitrary_such_that%

and then use the expected type of funExpression to get the predicate. (This gives us more information about the predicate, in particular we don't have to parse the lambda-abstraction that is currently passed to #derive_generator, which the current Chamelean implementation does using the function parseInductiveApp. This parsing approach has many limitations, e.g. it fails to handle infix operators and assumes that all arguments passed to the inductive relation are variable identifiers).

Here is some scaffolding for the aforementioned frontend re-design, provided by Kyle:

open Lean Elab Term Meta

syntax (name := arbitrarySuchThatStx) "arbitrary_such_that%" : term

@[term_elab arbitrarySuchThatStx]
def elabArbitrarySuchThat : TermElab := fun stx expectedType? => do
  let expectedType ← tryPostponeIfHasMVars expectedType? "\
    Could not elaborate `arbitrary_such_that%`"
  let_expr ArbitrarySuchThat ty p ← expectedType
    | throwError "Expected type must be of the form `ArbitrarySuchThat _ _`"
  Meta.withLocalDeclD `x ty fun x => do
    let p' := p.beta #[x]
    logInfo m!"\
      for x : {ty}\n\
      predicate is{indentExpr p'}"
    -- Put into WHNF to identify predicate
    let p' ← whnf p'
    let .const c _ := p'.getAppFn
      | throwError "expecting predicate to be a constant application"
    let ival ← getConstInfoInduct c
    let args := p'.getAppArgs
    let withParams := mkAppN p'.getAppFn args[0...ival.numParams]
    logInfo m!"predicate is {withParams}"
  throwError "implementation not finished"

set_option pp.explicit true
instance : ArbitrarySuchThat _ (fun (xs : List Nat) => xs = [3]) :=
  arbitrary_such_that%
/-
for x : List Nat
predicate is
  @Eq (List Nat) x
    (@List.cons Nat (@OfNat.ofNat Nat (nat_lit 3) (instOfNatNat (nat_lit 3))) (@List.nil Nat))

predicate is @Eq (List Nat) x
-/