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 ...