wip

src/compiler.ml

@@ -972,10 +972,7 @@ end = struct
   let global_type env ~loc c : ret TypeAssignment.overloading =
     try TypeAssignment.fresh_overloaded @@ F.Map.find c env
     with Not_found ->
-      if Re.Str.(string_match (regexp ".*\\.aux")) F.(show c) 0 then
-        TypeAssignment.(Single Prop)
-      else
-        error ~loc (Format.asprintf "Unknown global: %a" F.pp c)
+      error ~loc (Format.asprintf "Unknown global: %a" F.pp c)
 
   let local_type ctx ~loc c : ret TypeAssignment.overloading =
     try TypeAssignment.Single (F.Map.find c ctx)
@@ -3670,7 +3667,9 @@ end = struct
     (* TODO: make this callable on a unit (+ its base) *)
     let t0 = Unix.gettimeofday () in
     clauses |> List.iter (fun { Ast.Clause.body; loc; attributes = { Ast.Structured.typecheck } } ->
-      if typecheck then TypeChecker.check ~type_abbrevs ~kinds ~env:types body ~exp:TypeAssignment.(Val Prop));
+      if typecheck then
+        TypeChecker.check ~type_abbrevs ~kinds ~env:types body ~exp:TypeAssignment.(Val Prop)
+    );
     let t1 = Unix.gettimeofday () in
     let total_type_checking_time = total_type_checking_time +. t1 -. t0 in
 

tests/sources/GH_issue_19.elpi

@@ -1,15 +1,18 @@
-type transl A -> prop.
-
+type transl any -> prop.
+type p any -> any.
+type pp any -> any.
 transl (y \ _\ M y) :- % strip the hole
  P = (w \ p w),
  transl (z \ M (P z)).
 
 transl (x \ pp (X x)).
 
 % with a hole
+pred test1.
 test1 :- transl (x0 \ _ \ pp (p x0)).
 
 % with no hole
+pred test2.
 test2 :- transl (x0 \     pp (p x0)).
 
 main :- test1, test2.

tests/sources/accumulate_twice2.elpi

@@ -1,4 +1,3 @@
-pred doomed o:int.
 accumulate accumulated.
 namespace other { accumulate accumulated. }
 main :-

tests/sources/accumulated.elpi

@@ -1,2 +1,3 @@
+pred doomed i:int.
 doomed 0 :- fail.
 doomed N :- N > 0, M is N - 1, doomed M.

tests/sources/bug-256.elpi

@@ -9,10 +9,18 @@ main :-
   t3,
   true.
 
+pred p o:any.
+pred q o:any.
+type f any -> any.
+type g any -> any -> any -> any -> any.
+
+pred t1.
 t1 :- pi x\ u (y\ X x y), std.assert! (X 1 2 = 2) "bug".
 
+pred t2.
 t2 :-
   (pi X\ p ( a\f (X a))) => pi x y\ p ( a\f (g x y a)). 
 
+pred t3.
 t3 :-
   (pi X\ q ( a\b\c\d\f (X a))) => pi x y\ q ( a\b\c\d\f (g x y a)). 

tests/sources/bug_226.elpi

@@ -1,5 +1,6 @@
 
 kind term type.
+type fun (term -> term) -> term.
 pred f o:(term -> term) o:term.
 f R (fun d\ R d).
 %f R N :- N = (fun d\ R d).

tests/sources/chr.elpi

@@ -12,6 +12,7 @@ term (app HD ARG) TGT :- term HD (arr SRC TGT), term ARG SRC.
 term (lam F) (arr SRC TGT) :- pi x\ term x SRC => term (F x) TGT.
 term (uvar as X) T :- declare_constraint (term X T) [X].
 
+pred len i:list A, o:int.
 len [] 0.
 len [_|XS] N :- len XS M, N is M + 1.
 
@@ -29,6 +30,7 @@ constraint term {
 
 }
 
+pred compatible o:list prop, o:list term,o:list prop,o:list term,o:list prop.
 compatible _ [] _ [] [] :- !.
 compatible GX [X|XS] GY [Y|YS] [TX = TY | K] :-
  (GX => term X TX),

tests/sources/chr_nokey2.elpi

@@ -1,3 +1,7 @@
+type foo any.
+type bar any -> any.
+
 main :- declare_constraint foo [], declare_constraint (bar X) [], X.
 
 constraint foo bar { rule foo (bar _) <=> false. rule (bar X) <=> (X = true). }
+

tests/sources/chr_sem.elpi

@@ -1,3 +1,4 @@
+type a, b, c, d any.
 main :- declare_constraint a [_],
         declare_constraint b [_],
         declare_constraint b [_],

tests/sources/cut2.elpi

@@ -4,14 +4,21 @@
    ; A B :- A.
    ; A B :- B
 */
+:untyped
 q X :- c Y, !, x Y X ; e X.
+:untyped
 q ok.
 
+:untyped
 c one.
+:untyped
 c two.
 
+:untyped
 x two ko1.
 
+:untyped
 e ko2.
 
+:untyped
 main :- q X, X = ok.

tests/sources/cut3.elpi

@@ -1,13 +1,13 @@
 % Test with q X; should yield X=ok
 
-q X :- a X, b, c X.
+:untyped q X :- a X, b, c X.
 
-a ko.
-a ok.
+:untyped a ko.
+:untyped a ok.
 
-b :- !.
-b.
+:untyped b :- !.
+:untyped b.
 
-c ok.
+:untyped c ok.
 
-main :- q X, X = ok.
+:untyped main :- q X, X = ok.

tests/sources/cut5.elpi

@@ -1,16 +1,11 @@
 /* To test: query q X. The only answer should be X = ok. */
-q X :- a X.
-q ok.
-
-a ko :- b Y, !, d Z, !, c Z.
-a two.
-
-b three.
-b four.
-
-c four.
-
-d three.
-d four.
-
-main :- q X, X = ok.
+:untyped q X :- a X.
+:untyped q ok.
+:untyped a ko :- b Y, !, d Z, !, c Z.
+:untyped a two.
+:untyped b three.
+:untyped b four.
+:untyped c four.
+:untyped d three.
+:untyped d four.
+:untyped main :- q X, X = ok.

tests/sources/cut6.elpi

@@ -1,13 +1,9 @@
 % q X should yield X=ok
 
-q X :- a X, !.
-q X :- b X.
-
-a X :- c X, !.
-
-c ok.
-c ko.
-
-b ko.
-
-main :- q X, X = ok.
+:untyped q X :- a X, !.
+:untyped q X :- b X.
+:untyped a X :- c X, !.
+:untyped c ok.
+:untyped c ko.
+:untyped b ko.
+:untyped main :- q X, X = ok.

tests/sources/discard.elpi

@@ -1,3 +1,5 @@
+type foo int.
+type bar int.
 main :-
   foo = _,
   _ = 4,

tests/sources/elpi_only_llam.elpi

@@ -1 +1 @@
-main :- p (F X) F X => p (f x) f x.
+:untyped main :- p (F X) F X => p (f x) f x.

tests/sources/eta_as.elpi

@@ -9,11 +9,14 @@ pred uvar_4 i:A.
 pred uvar_5 i:A.
 pred uvar_6 i:A.
 
-pred test-as.
-pred test-uvar.
-pred test-var.
-pred test-declare-constraint.
+pred tests-as.
+pred tests-uvar.
+pred tests-var.
+pred tests-unif.
+pred tests-declare-constraint.
 
+type bar variadic any any.
+type c variadic any any.
 uvar_1 (bar (uvar K Args)) :- std.assert! (var K) "uvar_1 bar X, not a var", print K Args.
 uvar_2 (bar X) :- std.assert! (var X K Args) "uvar_2 bar X, not a var", print K Args.
 uvar_3 (uvar K) :- std.assert! (var K) "uvar_3 X, not a var", print K.
@@ -27,12 +30,13 @@ as_1 (bar (uvar as K)) :- std.assert! (var K) "bar (uvar as_1 X), not a var", pr
 as_2 (uvar as K) :- std.assert! (var K) "uvar as_2 X, not a var", print K.
 as_3 (uvar as K) :- std.assert! (var K) "uvar as_3 X, not a var", print K.
 
-pred unif_1 o:A.
-pred unif_2 o:A.
+pred unif_1 o:any.
+pred unif_2 o:any.
 
 unif_1 (x\ X x).
 unif_2 (x\ y\ X x y).
 
+type u any.
 
 tests-uvar :-
   print "--------- uvar_1",
@@ -70,7 +74,7 @@ tests-as :-
   print "---------- as_3",
   not (as_3 (x \ X0)).
 
-test-unif :-
+tests-unif :-
     print "---------- unif_1",
     unif_1 X,
     print "---------- unif_1 bis",
@@ -86,16 +90,16 @@ test-unif :-
     print "---------- unif_zero",
     (x\ X6 x) = X6.
 
-test-var :-
+tests-var :-
     print "---------- var 1",
    pi x \ (var (y \ X x y)),
     print "---------- var 2",
    pi x \ (var (y \ X c y)), 
     print "---------- var 3",
    pi x z \ (var (y \ X x y)).
 
-test-declare-constraint :-
+tests-declare-constraint :-
   declare_constraint false [x\ X x],
   not(X = 1).
 
-main :- tests-uvar, tests-as, test-unif, test-var, test-declare-constraint.
+main :- tests-uvar, tests-as, tests-unif, tests-var, tests-declare-constraint.

tests/sources/fragment_exit.elpi

@@ -1,5 +1,3 @@
-q Y :- pi d\ r Y.
-
-r _.
-
-main :- pi c\ q (x\ X c x).
+:untyped q Y :- pi d\ r Y.
+:untyped r _.
+:untyped main :- pi c\ q (x\ X c x).

tests/sources/fragment_exit2.elpi

@@ -1,2 +1,2 @@
-ignore _.
-main :- pi c\ Y c = (x\ X c x), ignore (Y c d).
+:untyped ignore _.
+:untyped main :- pi c\ Y c = (x\ X c x), ignore (Y c d).

tests/sources/fragment_exit3.elpi

@@ -1,2 +1,2 @@
-ignore _.
-main :- (pi c\ sigma Y\ X c = Y), ignore (X (f d)).
+:untyped ignore _.
+:untyped main :- (pi c\ sigma Y\ X c = Y), ignore (X (f d)).

tests/sources/general_case.elpi

@@ -1,6 +1,6 @@
-app F X :- F X. 
-c.
-ignore _.
-foo P :- pi d\ ignore P.
-main :- app (x\x) c, F = (y\y), F c, (pi d\ F c),
+:untyped app F X :- F X. 
+:untyped c.
+:untyped ignore _.
+:untyped foo P :- pi d\ ignore P.
+:untyped main :- app (x\x) c, F = (y\y), F c, (pi d\ F c),
         foo (G c).

tests/sources/general_case2.elpi

@@ -1,5 +1,3 @@
-p F :- F (x\ c x).
-
-q (x\ c x).
-
-main :- p (y\ pi z\ q y).
+:untyped p F :- F (x\ c x).
+:untyped q (x\ c x).
+:untyped main :- p (y\ pi z\ q y).

tests/sources/general_case3.elpi

@@ -1,3 +1,3 @@
-main :-
+:untyped main :-
  (pi c\ sigma X\ pi d\ (X d = f c d, Y c = X)),
  Y = c\ d\ f c d.