The test that is meant to succeed suceeds:
- use "test";
[opening test]
o : type.
k1 : o.
k2 : o.
l : o.
a : (o -> (o -> type)).
- mc : {* x:o} ((a x) x).
c : (((a k1) k1) -> type).
d : (c (mc *)).
val it = () : unit
val it = () : unit
And the test that is meant to be rejected is rejected:
- use "test2";
[opening test2]
o : type.
k1 : o.
k2 : o.
l : o.
a : (o -> (o -> type)).
- mc : {* x:o} ((a x) x).
c : (((a k1) k2) -> type).
XXX Matching: c+ head mismatch
val it = () : unit
val it = () : unit
-
oh, REJECTURE!
All this despite the code not exactly being, shall we say, polished and done with:
...
pp_ispat (s,shift)
end
(* prepattern: convert a subst list into a ppsubst *)
fun prepattern sl = pp_comp (map pp_normalize sl)
fun pp_invert ([],0) = Id (* XXX ahahaha *)
fun flex_left ((r as ref NONE,a), sl, rhs, lev) =
let
val pps = prepattern sl
val _ = if pp_ispat pps then () else raise NonPattern
...