Failed `require`s give unhelpful (and uncaught) errors

[sankalpgambhir]

Failed requires currently give rather unhelpful errors. Eg:

val x = variable
val y = variable
val g = function(2)
val Z = LambdaTermTerm(Seq(x), g(x, y)) // notice this has arity 1

// followed by a proof
   ...
   'P('x); 'Q('h('x, 'y)) |- 'R('y)      by Magic
   'P('x); 'Q('g('x, 'y)) |- 'R('y)      by InstFunSchema(Map(h -> Z))

is improper, since Z has arity 1 while h, 2. However, this simply returns the error:

[info]   java.lang.IllegalArgumentException: requirement failed
[info]   at scala.Predef$.require(Predef.scala:324)
[info]   at lisa.kernel.fol.Substitutions.instantiateTermSchemas(Substitutions.scala:131)
[info]   at lisa.kernel.fol.Substitutions.instantiateTermSchemas$(Substitutions.scala:130)
[info]   at lisa.kernel.fol.FOL$.instantiateTermSchemas(FOL.scala:10)
[info]   at lisa.utils.tactics.BasicStepTactic$InstFunSchema$.apply$$anonfun$7(BasicStepTactic.scala:1064)
[info]   at scala.collection.StrictOptimizedIterableOps.map(StrictOptimizedIterableOps.scala:100)
[info]   at scala.collection.StrictOptimizedIterableOps.map$(StrictOptimizedIterableOps.scala:87)
[info]   at scala.collection.immutable.Set$Set2.map(Set.scala:183)
[info]   at lisa.utils.tactics.BasicStepTactic$InstFunSchema$.apply(BasicStepTactic.scala:1064)
[info]   at lisa.utils.BasicTacticTest.testFun$proxy46$1$$anonfun$1(BasicTacticTest.scala:1219)
[info]   ...

We could probably stand to improve these errors for easier proof debugging.

[sankalpgambhir]

Probably a bigger issue, is that these are not caught during proof construction to return an InvalidProofTactic, but rather throw (currently uncaught) exceptions.

[SimonGuilloud]

Yep. Same issue is application of functions with incorrect number of parameters. Not sure yet about the best solution, but probably involves constructors from outside the kernel. That's in my mind :D