diff --git a/tests/sources/eta_as.elpi b/tests/sources/eta_as.elpi index e44b3a44..9b9647bd 100644 --- a/tests/sources/eta_as.elpi +++ b/tests/sources/eta_as.elpi @@ -38,6 +38,7 @@ unif_2 (x\ y\ X x y). type u any. +:untyped tests-uvar :- print "--------- uvar_1", not(uvar_1 (bar (x \ u))), diff --git a/tests/sources/hyp_uvar.elpi b/tests/sources/hyp_uvar.elpi index 1c37459a..b89ff1cc 100644 --- a/tests/sources/hyp_uvar.elpi +++ b/tests/sources/hyp_uvar.elpi @@ -1,5 +1,6 @@ pred f i:any. +:untyped main :- (f uvar :- print "ok") => (f X, not(f 1)), var X. \ No newline at end of file diff --git a/tests/sources/lyp/lyp_machine.elpi b/tests/sources/lyp/lyp_machine.elpi index 52f37ef7..0d6f9570 100644 --- a/tests/sources/lyp/lyp_machine.elpi +++ b/tests/sources/lyp/lyp_machine.elpi @@ -235,7 +235,7 @@ conv_t T1 S1 S2 X2 :- def_l X2 T2, !, % print "d", % Implied conversion %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -type conv_i id -> term -> stack -> stack -> term -> id -> prop. +pred conv_i i:id, o:term, o:stack, o:stack, o:term, i:id. conv_i X1 _ S1 S2 T2 X2 :- X1 < X2, !, conv_t X1 S1 S2 T2. diff --git a/tests/sources/map.elpi b/tests/sources/map.elpi index a5f52564..c382e5b2 100644 --- a/tests/sources/map.elpi +++ b/tests/sources/map.elpi @@ -6,7 +6,7 @@ build N M X X1 :- std.map.add N N X XR, build N1 M XR X1. -pred test i:int, i:int, i:(int -> A -> int -> prop), i:A. +pred test i:int, i:int, i:(pred i:int, i:A, o:int), i:A. test N N _ _ :- !. test N M F X :- N1 is N + 1, diff --git a/tests/sources/map_list.elpi b/tests/sources/map_list.elpi index 94fa6b46..c00a9cf7 100644 --- a/tests/sources/map_list.elpi +++ b/tests/sources/map_list.elpi @@ -26,14 +26,14 @@ build N M X X1 :- add N N X XR, build N1 M XR X1. -pred test i:int, i:int, i:(int -> A -> int -> prop), i:A. +pred test i:int, i:int, i:(pred i:int, i:A, o:int), i:A. test N N _ _ :- !. test N M F X :- N1 is N + 1, std.assert! (F N X N) "not found", test N1 M F X. -pred test2 i:int, i:int, i:(int -> A -> A -> prop), i:A. +pred test2 i:int, i:int, i:(pred i:int, i:A, o:A), i:A. test2 N N _ _ :- !. test2 N M F X :- N1 is N + 1,