jcreed

How Sweet the Sound



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

LJ Video