new signature declaration for mquery; similar to query but has added depth bound (e.g. --mquery <expected> <tries> <depth> <comp_typ>)
Accepts the following comp_typ's: Comp.TypBase, Comp.TypBox, Comp.TypPiBox, and Comp.TypArr
examples have been added to examples/aps to test mquery
module CSolver added to logic.ml
in addition to the LF signature being processed, the Comp signature (including constants and theorems) is now also processed; each declaration is transformed into a clause whose structure allows easy access to the head of the type and meta-variables that require instantiation
mqueries are transformed into a sgnMQuery record
msolve is called on each sgnMQuery; it creates the success-continuation function which, when called, will check the synthesized proof term against the synthesized meta-sub (containing instantiations for the MVars) applied to the queried type as well as ensure that the number of solutions found doesn't exceed the tries bound
the proof-search loop cgSolve is then called to find a proof term; each recursive call to cgSolve will increment the current depth count by 1
cgSolve follows a uniform/ focusing proof loop; first we enter into the uniform right phase which collects global and local assumptions, adding them to cD and cG (and cPool) respectively
cPool holds our dynamic assumptions, that is, the current state of cG; an assumption is considered part of cG when it is tagged with boxed in cPool
we then enter the uniform left phase where local-boxed assumptions are unboxed and put into the cD (thus no longer considered to be in cG)
we enter into the focusing phase, which depending on the goal type can go several ways; we either enter into proof search on the LF level (for box-types), focus on the comp. signature (for atomic-types), focus on comp. theorems, or on assumptions from cPool
in each of the focusing cases we focus on an assumption whose head matches our goal; a meta-sub is created for the matched assumption containing the MVars that require instantiation and the head and type are then unified
if the assumption has a non-empty list of subgoals, we proceed to solve them recursively, building our proof term using the success-continuation
Changes
--mquery <expected> <tries> <depth> <comp_typ>)msolveis called on each sgnMQuery; it creates the success-continuation function which, when called, will check the synthesized proof term against the synthesized meta-sub (containing instantiations for the MVars) applied to the queried type as well as ensure that the number of solutions found doesn't exceed the tries boundcgSolveis then called to find a proof term; each recursive call tocgSolvewill increment the current depth count by 1cgSolvefollows a uniform/ focusing proof loop; first we enter into the uniform right phase which collects global and local assumptions, adding them to cD and cG (and cPool) respectively