[TC] error predicate call solver

LPCIC · Jul 10, 2024 · 1a9bf3c · 1a9bf3c
1 parent 1ea3935
commit 1a9bf3c
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/apps/tc/tests/test.v b/apps/tc/tests/test.v
@@ -292,9 +292,9 @@ Module HO_scope_check1.
 
   Elpi Query TC.Solver lp:{{
     sigma X Q\ % To avoid printing in console
-      build-query-from-goal {{c1 (fun x => f x lp:X)}} _ Q _,
+      tc.build-query-from-goal {{c1 (fun x => f x lp:X)}} _ Q _,
       (pi A L T\ 
-        tc.link.scope-check (uvar _ L) (fun _ _ (x\ app [{{g}}|_] as T)) :- !, 
+        tc.link.eta.scope-check (uvar _ L) (fun _ _ (x\ app [{{g}}|_] as T)) :- !, 
           std.assert! (not (prune A L, A = T)) "[TC] Should fail by Scope Check", 
           fail) =>
       not Q.
@@ -411,7 +411,7 @@ Module Llam_4.
 
   Fail Elpi Query TC.Solver lp:{{
     sigma X Q\ % To avoid printing in console
-      build-query-from-goal {{c1 (fun x => f x lp:X)}} _ Q _,
+      tc.build-query-from-goal {{c1 (fun x => f x lp:X)}} _ Q _,
       not Q.
   }}.
 End Llam_4.

diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v
@@ -78,6 +78,7 @@ Elpi Db tc.db lp:{{
 
     % [class ClassGR PredName SearchMode Modes], for each class GR, it contains
     % the name of its predicate and its SearchMode 
+    :index (5)
     pred class o:gref, o:string, o:search-mode, o:list string.
 
     % pred on which we graft instances in the database