Removing term from Pulse AST, instead use F* reflection terms and expose a term view to the Pulse checker #30
Conversation
| ) ss l | ||
|
|
||
| let eq_tm_unascribe (g:env) (p q:term) |
There was a problem hiding this comment.
vprop matching is now working on F* reflection terms. In some cases, we do try to match p <: vprop with p in the context. If we just did syntactic matching, the ascriptions come in the way.
To get around this, the function eq_tm_unascribe unascribes and then does eq_tm, it returns an equiv proof for the two terms, by using magic () for the equiv token.
Going forward, we could move it to calling F* Rel (in some restricted config, no delta, no smt etc.), and get the token from there.
src/checker/Pulse.Syntax.Pure.fst
Outdated
There was a problem hiding this comment.
Pulse.Synatx.Pure contains all the pure syntax utilities, including pure syntax builders, term_view, inspect and pack, etc.
| fail_doc pst.pg None msg | ||
| | Some pst -> prover pst // a little wasteful? | ||
| | hd::unsolved' -> | ||
| match inspect_term hd with |
There was a problem hiding this comment.
Sample use of inspect API.
| @@ -315,12 +297,8 @@ let compute_term_type (g:env) (t:term) | |||
| match res with | |||
| | None -> | |||
| maybe_fail_doc issues | |||
| g t.range (ill_typed_term t None None) | |||
| | Some (| rt, eff, ty', tok |) -> | |||
| match readback_ty rt, readback_ty ty' with | |||
There was a problem hiding this comment.
In pure checker, we don't need to readback.
The PR removes the term AST from Pulse syntax and replaces it with the F* reflection term. We were using the Pulse term node for pure F* terms, including vprops (Tm_Emp, Tm_Star, etc.). Instead, the PR uses F* reflection term for such terms.
To help checker code inspect, for example, the vprop structure, the PR introduces a term_view (which is essentially earlier Pulse term), and an inspect function to go from F* reflection term to term_view, that code can match on.
The advantage is that, we get rid of a lot of boiler plate code (ln, freevars, subst, ...) for Pulse terms, instead all those are just corresponding F* reflection functions.