TC solver example

Author: manmatteo

tcsolver.elpi

@@ -1,28 +1,44 @@
-msolve L :- std.forall L (open tc).
+msolve L :- 
+  compile_all [{{eqdec}}] Cl,
+  Cl => std.forall L (open tc).
 
-pred open i:(list prop -> term -> term -> prop), i:sealed-goal.
+pred open i:(term -> term -> prop), i:sealed-goal.
 open P (nabla F) :- pi x\ open P (F x).
 open P (seal (goal Ctx Ty Wit)) :-
   print "TC PROBLEM:\n" Ctx "|-\n" Wit ":" Ty "\n",
-  Ctx => P Ctx Ty Wit,
+  Ctx => P Ty Wit,
   print "TC INSTANCE:\n" Ctx "|-\n" Wit ":" Ty "\n".
 
 :index(_ 4)
-pred tc i:list prop, i:term, o:term.
-tc _ {{ eqdec bool }} {{ bool_eqdec }}.
-tc _ {{ eqdec nat }} {{ nat_eqdec }}.
-tc C {{ eqdec (pair $A $B) }} {{ pair_eqdec $A $B $FA $FB }} :-
-  tc C (appl {{eqdec}} A) FA,
-  tc C (appl {{eqdec}} B) FB.
+pred tc o:term, o:term.
 
-/* brainstorm
+pred is_typeclass o:term.
+is_typeclass {{eqdec}}.
 
-compile_rule_lambdapi R (pi c\ tc c (app {{eqdec}} {{bool}})).
-compile_rule_coq R (pi c\ tc c (app {{eqdec}} {{bool}})).
+pred instances o:term o:list term.
+instances {{eqdec}} [{{bool_eqdec}}, {{nat_eqdec}}, {{pair_eqdec}}].
 
-abstract G GA,
-interp [R1,R2] GA PA,
-instantiate PA P,
-of P G
+pred compile i:term, i:list prop, i:term, o:prop.
+compile (prod (appl T U) F) TODO H (pi x\ C x) :-
+  is_typeclass T,
+  !,
+  pi x\
+    compile (F x) [tc (appl T U) x |TODO] (appl H x) (C x).
 
-*/
+compile (prod _ F) TODO H (pi x\ C x) :-
+  !,
+  pi x\
+    compile (F x) TODO (appl H x) (C x).
+
+compile End TODO HD (tc End HD :- TODO).
+
+pred compile_all i:list term, o:list prop.
+compile_all Refs Props :-
+  std.map Refs instances LList,
+  std.flatten LList Candidates,
+  std.map Candidates
+    (cand\claus\ sigma T\ sigma N\
+    cand = (symb N),
+    lp.sig N T,
+    compile T [] cand claus)
+    Props.

tests/OK/elpitest.lp

@@ -1,5 +1,4 @@
 /* dune exec lambdapi check tests/OK/elpitest.lp */
-
 require open tests.OK.logic;
 require open tests.OK.bool;
 require open tests.OK.nat;
@@ -11,8 +10,8 @@ flag "print_meta_types" on; // default is off
 
 constant typeclass symbol eqdec : U → TYPE;
 constant symbol mk_eqdec [i] :
-  /* Π f : */ (T i → T i → B) →
-  /* (Π x y : T i, (f x y = true → x = y) {|and|} (x = y → f x y = true)) → */
+  Π (f : T i → T i → B),
+  // (Π (x y : T i), P ({|and|} (imp (x = y) (f x y = true))(imp (f x y = true) (x = y))))  →
   eqdec i;
 
 symbol == [i:U] [j:eqdec i] : T i → T i → B;
@@ -23,7 +22,6 @@ symbol eq_bool : B → B → B ≔ λ b1 b2, bool_neg (bool_xor b1 b2);
 symbol Pair : U → U → TYPE;
 symbol mk_Pair [i] [j] : T i → T j → Pair i j;
 symbol pair : U → U → U;
-
 rule T (pair $i $j) ↪ Pair $i $j;
 
 /* instance */ symbol bool_eqdec : eqdec bool ≔ mk_eqdec eq_bool /* p */;