Class declare tc command

apps/tc/README.md

@@ -8,11 +8,12 @@ to make instance search on coq goals.
 
 - [The compiler](#the-compiler)
   - [Class compilation](#class-compilation)
-  - [Deterministic search](#deterministic-search)
+    - [Deterministic search](#deterministic-search)
+    - [Hint modes](#hint-modes)
   - [Instance compilation](#instance-compilation)
-  - [Instance priorities](#instance-priorities)
+    - [Instance priorities](#instance-priorities)
     - [Technical details](#technical-details)
-  - [Instance locality](#instance-locality)
+    - [Instance locality](#instance-locality)
 - [Goal resolution](#goal-resolution)
 - [Commands](#commands)
 - [Flags](#flags)
@@ -71,7 +72,7 @@ $N + 1$ terms where:
 The set of rules allowing to add new type-class predicates in elpi are grouped
 in [create_tc_predicate.elpi](elpi/create_tc_predicate.elpi).
 
-### Deterministic search 
+#### Deterministic search 
 
 Sometimes, it could be interesting to disable the backtracking search for some
 type classes, for performances issues or design choices. In coq the flag
@@ -84,11 +85,8 @@ In the example below, we want the `NoBacktrack` type class not to backtrack if
 a solution is found.
 
 ```coq
-Class NoBacktrack (n: nat).
-Elpi TC.Set_deterministic NoBacktrack.
-(* Ideally
-       #[backtrack(off)] Class NoBacktrack (n : nat).
- *)
+#[deterministic] TC.declare Class NoBacktrack (n: nat).
+
 Class A (n: nat).
 
 Instance a0 : A 0. Qed.
@@ -124,6 +122,34 @@ do-once P :- P, !.
 as implementation. The cut (`!`) operator is in charge to avoid backtracking on 
 the query `tc-NoBacktrack A B`
 
+#### Hint modes
+
+Instance search is done looking to the arguments passed to the class. If there
+is an instance $I$ unifying to it, the premises of $I$ are tried to be solved to
+commit $I$ as the solution of the current goal (modulo backtracking). Concerning
+the parameters of a type class, coq type class solver allows to constrain the
+argument to be ground, in input or output modes (see
+[here](https://coq.inria.fr/refman/proofs/automatic-tactics/auto.html#coq:cmd.Hint-Mode)).
+We provide a similar behavior in elpi: classes represent elpi predicates where
+the parameters can be in input `i` or output `o` mode (see
+[here](https://github.com/LPCIC/elpi/blob/master/ELPI.md#modes)). We translate
+coq modes in the following way: `+` and `!` become `i` in elpi and `-` becomes
+`o` (see
+[here](https://github.com/FissoreD/coq-elpi/blob/c3cce183c3b2727ef82178454f0c583196ee2c21/apps/tc/elpi/create_tc_predicate.elpi#L12)).
+
+In elpi we allow type classes to have at most one mode, if that mode is not
+defined, all parameters are considered in `o` mode. The command to be used 
+to let elpi compile classes with modes is done via the command `TC.Declare`.
+
+```coq
+#[mode(i, o, i)] TC.Declare Class (T1: Type) (T2: Type) (N : nat).
+```
+
+The pragma `mode` is taken into account to make `T1` and `N` in input mode and 
+`T2` in output mode. The command `TC.Declare` both create the class in elpi and 
+in coq. Note that the accepted list arguments for the attribute `mode` are 
+`i, o, +, -` and `!` with their respective meaning.
+
 ### Instance compilation
 
 Instances are compiled in elpi from their type. In particular, since the
@@ -189,7 +215,7 @@ variables.
 The set of rules allowing to compile instances in elpi are grouped in 
 [compiler.elpi](elpi/compiler.elpi).
 ****
-### Instance priorities
+#### Instance priorities
 
 To reproduce coq behavior, instances need to respect a notion of priority:
 sometime multiple instances can be applied on a goal, but, for sake of
@@ -265,7 +291,7 @@ get its priority (see
 
     by default, once registered, the elpi program `PROG` is activated
 
-### Instance locality
+#### Instance locality
 
 The instances in the elpi database respect the locality given by the user. This
 is possible thanks to the attributes from
@@ -438,7 +464,17 @@ A small recap of the available elpi commands:
     <code>TC.AddHook G OldName NewName</code> (click to expand)
   </summary>
 
-  See [](#technical-details)
+  See [here](#technical-details)
+
+</details>
+
+<details>
+  <summary>
+    <code>TC.Declare ClassDef</code> (click to expand)
+  </summary>
+
+  See [here](#deterministic-search) and [here](#hint-modes) for respectively
+  deterministic type class and mode declaration
 
 </details>
 
@@ -515,10 +551,7 @@ Here the list of the flags available (all of them are `off` by default):
 ## WIP
 
 1. Mode management: 
-   - Classes with a single user defined should be taken into account to use the 
-    elpi modes
-   - Classes with multiple modes ??
+   - Classes with multiple modes 
 2. Clarify pattern fragment unification 
 3. Topological sort of premises in modes are activated 
-4. Option to disable auto compiler (maybe)
 

apps/tc/_CoqProject.test

@@ -9,6 +9,7 @@
 -R tests    elpi.apps.tc.tests
 -I src
 
+tests/classes_declare.v
 
 # Register (de-)activation
 tests/register/f1.v

apps/tc/elpi/compiler.elpi

@@ -98,9 +98,9 @@ compile-aux (prod N T F) I RevPremises ListVar [] IsPositive IsHead Clause ff :-
     compile-aux (F p) I L [p | ListVar] [] IsPositive IsHead (C p) _.
 compile-aux Ty I RevPremises ListVar [] _ IsHead Clause tt :- 
   not (is-option-active {oTC-use-pattern-fragment-compiler}), !,
-  std.rev RevPremises RevRHS,
+  std.rev RevPremises Premises,
   coq.mk-app I {std.rev ListVar} AppInst,
-  make-tc IsHead Ty AppInst RevRHS Clause.
+  make-tc IsHead Ty AppInst Premises Clause.
 compile-aux Ty I RevPremises ListVar [] IsPositive IsHead Clause tt :- !,
   std.rev RevPremises Premises,
   coq.mk-app I {std.rev ListVar} AppInst,

apps/tc/elpi/create_tc_predicate.elpi

@@ -1,49 +1,80 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
+pred string->coq-mode i:string, o:hint-mode.
+string->coq-mode "bang" mode-ground :- !.
+string->coq-mode "plus" mode-input :- !.
+string->coq-mode "minus" mode-output :- !.
+string->coq-mode "i" mode-input :- !.
+string->coq-mode "o" mode-output :- !.
+string->coq-mode A _ :- coq.error A "is not a valid mode".
 
-pred bool->mode-term i:bool, o:pair argument_mode string.
-% TODO: here every mode is declared to O;term. 
-% If you want to make it work as intended,
-% replace the output of tt with "i:term"
-:name "bool->mode-term"
-bool->mode-term tt (pr in "term").
-bool->mode-term ff (pr out "term").
-
-pred modes->string i:list bool, o:list (pair argument_mode string).
-modes->string L S :-
-  std.map L bool->mode-term S.
-
-pred make-tc-modes i:int, o:list (pair argument_mode string).
-make-tc-modes NB_args ModesStr :-
-  list-init NB_args (x\r\ r = ff) ModesBool,
-  modes->string ModesBool ModesStr.
-
-pred build-modes i:gref, o:list (pair argument_mode string).
-build-modes ClassGr Modes :- 
-  is-option-active {oTC-addModes},
-  coq.hints.modes ClassGr "typeclass_instances" ModesProv,
-  not (ModesProv = []),
-  coq.hints.modes ClassGr "typeclass_instances" ModesProv,
-  std.assert! (ModesProv = [HintModes]) "At the moment we only allow TC with one Hint Mode",
-  std.map {std.append HintModes [mode-output]} (x\r\ if (x = mode-output) (r = ff) (r = tt)) ModesBool,
-  modes->string ModesBool Modes.
-build-modes ClassGr Modes :- 
+pred coq-mode->elpi i:hint-mode, o:pair argument_mode string.
+:name "coq-mode->elpi"
+coq-mode->elpi mode-ground (pr in "term"). % approximation
+coq-mode->elpi mode-input (pr in "term").
+coq-mode->elpi mode-output (pr out "term").
+
+pred modes-of-class i:gref, o:list (pair argument_mode string).
+modes-of-class ClassGr Modes :- 
+  coq.hints.modes ClassGr "typeclass_instances" CoqModesList,
+  not (CoqModesList = []),
+  std.assert! (CoqModesList = [HintModesFst]) "At the moment we only allow TC with one Hint Mode",
+  std.append {std.map HintModesFst coq-mode->elpi} [pr out "term"] Modes.
+modes-of-class ClassGr Modes :- 
   coq.env.typeof ClassGr ClassTy,
-  coq.count-prods ClassTy N',
-  N is N' + 1, % Plus one for the solution
-  make-tc-modes N Modes.
+  N is {coq.count-prods ClassTy} + 1, % + 1 for the solution
+  list-init N (x\r\ r = (pr out "term")) Modes.
 
 pred add-class-gr i:search-mode, i:gref.
-add-class-gr SearchMode ClassGr :-
-  std.assert! (coq.TC.class? ClassGr) "Only gref of type classes can be added as new predicates",
-  if (class ClassGr _ _) true 
-    (build-modes ClassGr Modes, 
-      gref->pred-name ClassGr PredName,
+add-class-gr SearchMode ClassGR :-
+  std.assert! (coq.TC.class? ClassGR) "Only gref of type classes can be added as new predicates",
+  if (class ClassGR _ _) true 
+    (modes-of-class ClassGR Modes, 
+      gref->pred-name ClassGR PredName,
       coq.elpi.add-predicate "tc.db" _ PredName Modes,
-      add-tc-db _ _ (tc-mode ClassGr Modes),
-      @global! => coq.elpi.accumulate _ "tc.db" (clause _ _ (class ClassGr PredName SearchMode :- !))).
+      add-tc-db _ _ (tc-mode ClassGR Modes),
+      @global! => add-tc-db _ _ (class ClassGR PredName SearchMode)).
 
 pred add-class-str i:search-mode, i:string.
-add-class-str SearchMode TC_Name :-
-  coq.locate TC_Name TC_Gr,
-  add-class-gr SearchMode TC_Gr.
+add-class-str SearchMode ClassStr :-
+  coq.locate ClassStr ClassGR,
+  add-class-gr SearchMode ClassGR.
+
+% Following are predicates for TC.declare
+
+pred attr->deterministic o:search-mode. 
+attr->deterministic deterministic :- get-option "deterministic" tt, !.
+attr->deterministic classic.
+
+pred attr->modes o:list hint-mode.
+attr->modes CoqModes :- 
+  get-option "mode" L,
+  std.map L get-key-from-option RawModes, 
+  std.map RawModes string->coq-mode CoqModes, !.
+attr->modes [].
+
+pred get-key-from-option i:prop, o:string. 
+get-key-from-option (get-option A tt) A :- !.
+get-key-from-option (get-option "i" ff) "o" :- !.
+get-key-from-option (get-option "o" ff) "i" :- !.
+get-key-from-option A _ :- coq.error A "should be an option".
+
+pred declare-class-in-coq i:gref.
+declare-class-in-coq ClassGR :- 
+  attr->modes CoqModes,
+  if (CoqModes = []) true 
+    (@global! => coq.hints.add-mode ClassGR "typeclass_instances" CoqModes),
+  % CAVEAT: this triggers the observer
+  coq.TC.declare-class ClassGR,
+  attr->deterministic SearchMode, 
+  gref->pred-name ClassGR PredName,
+  % HACK: we override the clauses added by the observer, since it does not know
+  % the SearchMode.
+  @global! => add-tc-db _ (after "0") (class ClassGR PredName SearchMode :- !).
+
+pred declare-class i:indt-decl. 
+declare-class D :- !, 
+  coq.env.add-indt D I,
+  coq.parse-attributes {attributes} 
+    [ att "mode" attlist, att "deterministic" bool ] Opts,
+  Opts => declare-class-in-coq (indt I).

apps/tc/tests/classes_declare.v

@@ -0,0 +1,75 @@
+From elpi.apps Require Import tc.
+
+Elpi Override TC TC.Solver All.
+
+(* Base test *)
+Section S1.
+
+  TC.Declare Class class1 (n : nat).
+
+  (* TODO: here coq can solve the goal without applying Build_class1 *)
+  Instance inst1 : class1 3. Proof. apply Build_class1. Qed.
+
+  Goal exists x, class1 x. Proof. eexists. apply _. Qed.
+
+End S1.
+
+(* Deterministic class test *)
+Section S2.
+
+  #[deterministic] TC.Declare Class class2 (n : nat).
+
+  Instance inst2  : class2 1 | 0. Proof. apply Build_class2. Qed.
+  Instance inst2' : class2 2 | 1. Proof. apply Build_class2. Qed.
+
+  Class aux (i: nat).
+
+  Instance inst_aux  : forall n, class2 n -> aux n -> aux 3. Qed.
+  Section S2'.
+    Local Instance inst_aux' : aux 1. Qed.
+    Goal aux 3. apply _. Qed.
+  End S2'.
+
+  Section S2'.
+    Local Instance inst_aux'' : aux 2. Qed.
+    Goal aux 3. 
+    Proof. 
+      Succeed apply (inst_aux 2 inst2' inst_aux'').
+      (* Note: since class2 is deterministic we cannot backtrack. 
+               The first hypothesis of inst_aux is unified to inst2, 
+               this causes `aux 2` to fail. The instance inst2' is not tried 
+               due to the deterministic class  *)
+      Fail apply _.
+    Abort.
+  End S2'.
+
+End S2.
+
+(* Mode test *)
+Section S3.
+  #[mode(i)] TC.Declare Class class3 (n : nat).
+  Instance inst3 : class3 0. Proof. apply Build_class3. Qed.
+
+  Goal exists x, class3 x. 
+  Proof.
+    eexists.
+    Succeed apply inst3.
+    Fail apply _.
+  Abort.
+
+End S3.
+
+Section S31.
+  #[mode(o=ff)] TC.Declare Class class31 (n : nat).
+  Instance inst31 : class31 0. Proof. apply Build_class31. Qed.
+
+  Goal exists x, class31 x. 
+  Proof.
+    eexists.
+    Succeed apply inst31.
+    Fail apply _.
+  Abort.
+
+End S31.
+
+

apps/tc/theories/add_commands.v

@@ -95,8 +95,21 @@ Elpi Accumulate lp:{{
 }}.
 Elpi Typecheck.
 
+Elpi Command TC.Declare.
+Elpi Accumulate Db tc.db.
+Elpi Accumulate Db tc_options.db.
+Elpi Accumulate File base.
+Elpi Accumulate File tc_aux.
+Elpi Accumulate File create_tc_predicate.
+Elpi Accumulate lp:{{
+  main [indt-decl D] :- declare-class D.
+  main _ :- coq.error "Argument should be an inductive type".
+}}.
+Elpi Typecheck.
+
 Elpi Export TC.AddAllClasses.
 Elpi Export TC.AddAllInstances.
 Elpi Export TC.AddClasses.
 Elpi Export TC.AddInstances.
-Elpi Export TC.AddHook.
+Elpi Export TC.AddHook.
+Elpi Export TC.Declare.

apps/tc/theories/db.v

@@ -22,9 +22,6 @@ Elpi Db tc_options.db lp:{{
 
   pred oTC-debug o:list string.
   oTC-debug ["TC", "Debug"].
-
-  pred oTC-addModes o:list string.
-  oTC-addModes ["TC", "AddModes"].
 
   pred oTC-use-pattern-fragment-compiler o:list string. 
   oTC-use-pattern-fragment-compiler ["TC", "CompilerWithPatternFragment"].