+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