+let rec absent lexp index =
You can use `fv` (in opslexp.ml) to get the set of freevars (this gets cached, so it's cheap) instead of having to traverse the term by hand.
+let rec is_positive lexp index = + match lexp with + | Lexp.Arrow (_, _, tau, _, e) -> + (* x ⊢ e pos x ∉ fv(τ) + * ---------------------- + * x ⊢ (y : τ) → e pos + *) + is_positive e (index + 1) && absent tau index + | Lexp.Builtin _ -> + true + | Lexp.Call (_, args) -> + (* x ∉ fv(e⃗) + * -------------- + * x ⊢ x e⃗ pos + *) + List.for_all (function _, arg -> absent arg index) args
Notice that the rule you quote talks about the case `Call (f, args)` where `f` is equal to `index`. Here you don't even look at the function that's called. If it's `index`, then everything's good, and if `absent f index`, everything's good as well, but otherwise we're in trouble.
+ | Lexp.Case _ -> + true
When in doubt, return `false` rather than `true` (applies to many of the other cases you have). I think we could return `true` here in *some* cases, but definitely not in general.
+ | Lexp.Metavar _ -> + true
This one should be either impossible (i.e. signal an error) or should lookup the metavar in the metavar table and recurse on the result: when we check positivity, inference is presumably done, so all metavars should have been instantiated.
+ | Lexp.Susp _ -> + true
No, here you need to apply `push_susp` and then recurse on the result.
+ | Lexp.Var _ -> + true
I think one is right ;-) Stefan