You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
For Dv recursion, without any termination check, one possibility is having a rule like:
G, f : (a -> Dv b), x:a |- e : Dv b
------------------------------------ [Rec]
G |- (let rec f x = e in f) : a -> Dv b
i.e. the simple 1-argument Dv recursion rule, and use that to get n-ary recursion like this:
G, f : (a -> b -> c -> Dv d), x:a, y:b, z:c |- e : Dv d
-------------------------------------------------------------------- [Lam]
G, f : (a -> b -> c -> Dv d), x:a |- (fun y z -> e) : b -> c -> Dv d
-------------------------------------------------------------------- [Rec]
G |- (let rec f x = fun y z -> e) : a -> Dv (b -> c -> Dv d)
And then use eta expansion to turn this into a a -> b -> c -> Dv d.
@mtzguido has added support for general recursion in stt as well as recursion with termination checking for stt_ghost. We also have support for extraction of recursive definitions.
The approach involves introducing a Pulse definition with an additional argument for the recursively bound name and then relying on a regular F* definition to tie that knot. The code that actually ties the knot is admitted currently, but our most recent discussions around this is to expose for stt a pair of coercions as_dv (s:stt a p q) : unit -> Dv (stt' a p q) and from_dv: (unit -> Dv (stt' a p q) -> stt a p q for an abstract type stt'. This should allow us to tie the knot in the general recursion case without needing to prove termination.
The text was updated successfully, but these errors were encountered: