Tactics: allow Reflection.Typing primitives to raise guards #3011
Conversation
mtzguido
force-pushed
the
refl-typing-guards
branch
from
ae08b5f to
46c2237
Compare
| @@ -2106,7 +2106,26 @@ let dbg_refl (g:env) (msg:unit -> string) = | |||
| then BU.print_string (msg ()) | |||
|
|
|||
| let issues = list Errors.issue | |||
| let refl_typing_builtin_wrapper (f:unit -> 'a) : tac (option 'a & issues) = | |||
|
|
|||
| let rec iter (f : 'a -> tac unit) (xs : list 'a) : tac unit = | |||
There was a problem hiding this comment.
FStar.Tactics.Monad.iter_tac ()?
| The caller will discharge them if needed. *) | ||
| let gs = | ||
| if Some? r then | ||
| List.map (fun (e,g) -> e, SC.deep_compress false g) (snd (Some?.v r)) |
There was a problem hiding this comment.
A very minor nit, for readability we could write it as: let allow_uvars = false in SC.deep_compress allow_uvars ... etc.
| Rel.force_trivial_guard g | ||
| {Env.trivial_guard with guard_f = NonTrivial guard}; | ||
| true in | ||
| (* FIXME: this is kinda ugly, we store all the guards |
There was a problem hiding this comment.
Yeah ... the callback to the core API could be proc_guard_formula here and then the meta function could return [] ... though that is not uniform with other callbacks.
There was a problem hiding this comment.
I think we can't do that since these must be pure (non-tac) functions, both the callback that the core typechecker receives and the function wrapped by refl_typing_builtin_wrapper--- but proc_guard_formula must be in tac.
| @@ -2385,14 +2445,18 @@ let refl_instantiate_implicits (g:env) (e:term) : tac (option (term & typ) & iss | |||
| let must_tot = true in | |||
| let g = {g with instantiate_imp=false; phase1=true; lax=true} in | |||
| let e, t, guard = g.typeof_tot_or_gtot_term g e must_tot in | |||
| (* We force this guard here, and do not delay it, since we | |||
| will return this term and it MUST be compressed. We could | |||
| split the logical part away and return that, though. *) | |||
There was a problem hiding this comment.
This is a lax call though, so dropping the logical payload of the guard, if exists, is totally fine.
There was a problem hiding this comment.
Good point! I changed that comment slightly.
|
|
||
| let refl_typing_guard (e:env) (g:typ) : tac unit = | ||
| let reason = "refl_typing_guard" in | ||
| proc_guard_formula "refl_typing_guard" e g None Range.dummyRange |
There was a problem hiding this comment.
So we just process the guards according to the policy, and then they will be handled by the Tactics.Monad.run at the end as usual?
There was a problem hiding this comment.
Yes, the policy dictates whether a guard is to be solves immediately by SMT (SMTSync), or immediately without SMT (Force) or added as a goal (Goal / SMT, the latter should probably be called SMTGoal). Once it's in the proofstate the engine will keep track of it, and force it be discharged at some point. In Pulse, after this PR, they would all be solved at the end.
Note that if the policy is not Force/SMTSync, then a reflection call could 'succeed' returning some unprovable goal, which I think is expected with this interface. This can always be avoided by temporarily changing the policy, as here https://github.com/FStarLang/steel/pull/65/files#diff-34e0e2aac381e650cef38feb50f4420ca101eff6b609e240a18c077ba7663300R6
|
Thanks @aseemr ! Just pushed some changes. |
No description provided.