Merge pull request #656 from FissoreD/premise_with_solution

[TC] premise not run if rigid solution

Author: gares

apps/tc/elpi/tc_aux.elpi

@@ -111,23 +111,34 @@ namespace tc {
   get-mode ClassGR M :- tc.class ClassGR _ _ M, !.
   get-mode ClassGR _ :- coq.error "[TC]" ClassGR "is an unknown class".
 
-  pred make-tc.aux i:bool, i:prop, i:list prop, o:prop.
-  make-tc.aux _ Head [] Head.
-  make-tc.aux tt Head Body (Head :- Body).
-  make-tc.aux ff Head Body (Body => Head).
+  /* 
+  [make-tc.aux B Sol Head Body Rule] builds the rule with the given Head and body
+                                    paying attention to the positivity of the
+                                    clause  
+  Note: if the Rule being constructed is negative (B = ff), then Rules returns a
+        solution Sol used inside the proof. If the solution is already given, we
+        do not run the premise. This would ask Sol to be ground (ground_term S).
+        Here, for performance issues, we simply check that the solution is not a
+        flexible term
+  */
+  pred make-tc.aux i:bool, i:term, i:prop, i:list prop, o:prop.
+  make-tc.aux tt _ Head [] Head :- !.
+  make-tc.aux ff Sol Head [] P :- !, P = if (var Sol) Head true.
+  make-tc.aux tt _ Head Body (Head :- Body) :- !.
+  make-tc.aux ff Sol Head Body P :- !, P = if (var Sol) (Body => Head) true.
 
   pred make-tc i:term, i:term, i:list prop, i:bool, o:prop.
-  make-tc Ty Inst Body IsPositive Clause :-
-    coq.safe-dest-app Ty HD TL,
-    get-TC-of-inst-type HD ClassGR,
+  make-tc Goal Sol RuleBody IsPositive Rule :-
+    coq.safe-dest-app Goal Class Args,
+    get-TC-of-inst-type Class ClassGR,
     gref->pred-name ClassGR ClassStr,
-    std.append TL [Inst] Args, 
-    coq.elpi.predicate ClassStr Args Head,
-    make-tc.aux IsPositive Head Body Clause.
+    std.append Args [Sol] ArgsSol, 
+    coq.elpi.predicate ClassStr ArgsSol RuleHead,
+    make-tc.aux IsPositive Sol RuleHead RuleBody Rule.
 
-  pred unwrap-prio i:tc-priority, o:int.
-  unwrap-prio (tc-priority-given Prio) Prio.
-  unwrap-prio (tc-priority-computed Prio) Prio.
+    pred unwrap-prio i:tc-priority, o:int.
+    unwrap-prio (tc-priority-given Prio) Prio.
+    unwrap-prio (tc-priority-computed Prio) Prio.
 
   % returns the priority of an instance from the gref of an instance
   pred get-inst-prio i:gref, o:int.

apps/tc/tests/hyp_in_conl.v

@@ -0,0 +1,81 @@
+From elpi.apps Require Import tc.
+
+(* 
+  Here we want to test that if the solution of a premise is rigid
+  then the premise is not run
+*)
+
+Module M1.
+  Structure ofe := Ofe { ofe_car : Type; }.
+
+  Class D (I : ofe).
+
+  Class C (X : ofe) (I : D X).
+
+  Definition ofe_nat : ofe := Ofe nat.
+
+  Instance c : forall (H : D (Ofe nat)), C ofe_nat H := {}.
+
+  Goal forall (H : D (Ofe nat)), True -> exists H, C (ofe_nat) H.
+    intros.
+    notypeclasses refine (ex_intro _ _ _ ).
+    apply _.
+  Qed.
+End M1.
+
+Module M2.
+
+  Class A.
+  Class B (I : A).
+  Class C (A : A) (I : B A).
+
+  Instance c : forall (A : A) (B : B A), C A B := {}.
+
+  Goal forall (A : A) (B : B A), exists A B, C A B.
+    intros.
+    do 2 notypeclasses refine (ex_intro _ _ _ ).
+    apply _.
+  Qed.
+
+End M2.
+
+Module M3.
+
+  Class A.
+  Class B (I : A).
+  Class C (A : A) (I : B A).
+
+  Instance c : forall (A : A) (B : B A), C A B := {}.
+
+  Set Warnings "+elpi".
+
+  Section s.
+    Elpi Accumulate TC.Solver lp:{{
+      :before "0" tc-elpi.apps.tc.tests.hyp_in_conl.M3.tc-A _   :- coq.say "In tc-A", fail.
+      :before "0" tc-elpi.apps.tc.tests.hyp_in_conl.M3.tc-B _ _ :- coq.say "In tc-B", fail.
+    }}.
+    Elpi Typecheck TC.Solver.
+    Local Instance AX : A := {}.
+    Local Instance BX : A -> (B AX) := {}.
+
+    Definition d : C AX (BX _) := _.
+    Definition d' : C _ (BX _) := _.
+    Definition d'' : C AX _ := _.
+
+    Check (c _ _) : C AX _.
+
+    (* 
+      Here we give the solver a partial solution with a hole in it. This hole
+      correspond to the premise of the typeclass B (an instance of A). Due to
+      the var condition on the resolution of rule's premises, the premise of
+      `C`, that is, `B X` is not solved since we have the partial solution `BX
+      _`. (see: [here](https://github.com/LPCIC/coq-elpi/blob/889bd3fc16c31f35c850edf5a0df2f70ea9c655a/apps/tc/elpi/tc_aux.elpi#L124))
+    *)
+    Elpi Query TC.Solver lp:{{
+      S = {{c AX (BX _)}},
+      tc.solve-aux1 [] {{C _ _}} S.
+    }}.
+
+  End s.
+
+End M3.