[elpi] minor improvements

Author: gares

src/core/elpi_lambdapi.ml

@@ -254,7 +254,9 @@ let lambdapi_builtin_declarations : BuiltIn.declaration list =
 
   LPDoc "---- Elpi predicates ----";
 
-] @ Elpi.Builtin.core_builtins @ Elpi.Builtin.elpi_builtins
+] @ Elpi.Builtin.core_builtins
+  @ Elpi.Builtin.elpi_builtins
+  @ Elpi.Builtin.elpi_nonlogical_builtins
 
 let lambdapi_builtins =
   BuiltIn.declare ~file_name:"lambdap.elpi" lambdapi_builtin_declarations
@@ -296,7 +298,7 @@ fun ss file predicate arg ->
   | Execute.Success { Data.state; pp_ctx; constraints; _ } ->
       let _ = readback_assignments state in
       Console.out 1 "\nelpi: after: %a\n" Print.pp_term arg;
-      Console.out 1 "elpi: constraints: %a\n"
+      Console.out 1 "elpi: constraints:@ @[<v>%a@]\n"
         Pp.(constraints pp_ctx) constraints
   | Failure -> Console.fatal_no_pos "elpi: failure"
   | NoMoreSteps -> assert false

tests/OK/elpitest.elpi

@@ -20,8 +20,7 @@ of (appl H A) Ta :-
   Ta = T A.
 
 % suspension of typing on holes (type constraint)
-of (uvar as U) T :-
-  declare_constraint (of U T) [U].
+of U T :- var U, declare_constraint (of U T) [U].
 
 % uniqueness of typing
 constraint of {

tests/OK/elpitest.lp

@@ -2,4 +2,5 @@ require open tests.OK.logic
 require open tests.OK.bool
 require open tests.OK.nat
 
-elpi "tests/OK/elpitest.elpi" "main" (Πx y, P (eq ?T[x;y] x y) → P (eq ?T[x;y] y x))
+elpi "tests/OK/elpitest.elpi" "main"
+  (Πx y, P (eq ?T[x;y] x y) → P (eq ?T[x;y] y x))