diff --git a/apps/tc/README.md b/apps/tc/README.md index bf03a8a5c..571aa29d5 100644 --- a/apps/tc/README.md +++ b/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: TC.AddHook G OldName NewName (click to expand) - See [](#technical-details) + See [here](#technical-details) + + + +
+ + TC.Declare ClassDef (click to expand) + + + See [here](#deterministic-search) and [here](#hint-modes) for respectively + deterministic type class and mode declaration
@@ -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) diff --git a/apps/tc/_CoqProject.test b/apps/tc/_CoqProject.test index 2eb1886e8..ed130c2f6 100644 --- a/apps/tc/_CoqProject.test +++ b/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 diff --git a/apps/tc/elpi/compiler.elpi b/apps/tc/elpi/compiler.elpi index 6c9b2c5bb..504160b98 100644 --- a/apps/tc/elpi/compiler.elpi +++ b/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, diff --git a/apps/tc/elpi/create_tc_predicate.elpi b/apps/tc/elpi/create_tc_predicate.elpi index 28ee4ea93..34c36b804 100644 --- a/apps/tc/elpi/create_tc_predicate.elpi +++ b/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. \ No newline at end of file +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). \ No newline at end of file diff --git a/apps/tc/tests/classes_declare.v b/apps/tc/tests/classes_declare.v new file mode 100644 index 000000000..db1f9f1b3 --- /dev/null +++ b/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. + + diff --git a/apps/tc/theories/add_commands.v b/apps/tc/theories/add_commands.v index 6e4457582..ac5bd8629 100644 --- a/apps/tc/theories/add_commands.v +++ b/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. \ No newline at end of file +Elpi Export TC.AddHook. +Elpi Export TC.Declare. \ No newline at end of file diff --git a/apps/tc/theories/db.v b/apps/tc/theories/db.v index 2e76b2ef3..a51fd422c 100644 --- a/apps/tc/theories/db.v +++ b/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"]. diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v index 94f98e0f4..65f422da9 100644 --- a/apps/tc/theories/tc.v +++ b/apps/tc/theories/tc.v @@ -46,7 +46,7 @@ Elpi Accumulate File solver. Elpi Query lp:{{ sigma Options\ Options = [oTC-ignore-eta-reduction, oTC-resolution-time, - oTC-clauseNameShortName, oTC-time-refine, oTC-debug, oTC-addModes, + oTC-clauseNameShortName, oTC-time-refine, oTC-debug, oTC-use-pattern-fragment-compiler], std.forall Options (x\ sigma Args\ x Args, coq.option.add Args (coq.option.bool ff) ff). @@ -93,11 +93,12 @@ Elpi Accumulate Db tc_options.db. Elpi Accumulate File base. Elpi Accumulate File tc_aux. Elpi Accumulate lp:{{ - main [str ClStr] :- - coq.locate ClStr Gr, - std.assert! (coq.TC.class? Gr) "Should pass the name of a type class", - std.assert! (class Gr PredName _) "Cannot find `class GR _ _` in the db", - add-tc-db _ (after "0") (class Gr PredName deterministic :- !). + main [str ClassStr] :- + coq.locate ClassStr ClassGR, + std.assert! (coq.TC.class? ClassGR) "Should pass the name of a type class", + std.assert! (class ClassGR PredName _) "Cannot find `class ClassGR _ _` in the db", + std.assert! (not (instance _ _ ClassGR)) "Cannot set deterministic a class with more than one instance", + add-tc-db _ (after "0") (class ClassGR PredName deterministic :- !). }}. Elpi Typecheck. diff --git a/apps/tc/theories/wip.v b/apps/tc/theories/wip.v index a676988a6..6a77906b9 100644 --- a/apps/tc/theories/wip.v +++ b/apps/tc/theories/wip.v @@ -46,32 +46,7 @@ Elpi Accumulate File base. Elpi Accumulate File tc_aux. Elpi Accumulate File alias. Elpi Accumulate lp:{{ - main [trm New, trm Old] :- add-tc-db _ _ (alias New Old). }}. -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] :- - attributes A, - coq.say A, - Opts => - get-option "modes" [tt,ff,tt], - coq.env.add-indt D I, - coq.say I. -}}. -Elpi Typecheck. -Elpi Export TC.declare. - -#[mode(i,i,o)] TC.declare - Class foo (A : Type) . -*) +Elpi Typecheck. \ No newline at end of file diff --git a/elpi/coq-lib.elpi b/elpi/coq-lib.elpi index 917e174da..84962ebb2 100644 --- a/elpi/coq-lib.elpi +++ b/elpi/coq-lib.elpi @@ -663,6 +663,7 @@ type string attribute-type. type bool attribute-type. type oneof list attribute-mapping -> attribute-type. type attmap attribute-type. +type attlist attribute-type. type loc attribute-type. kind attribute-mapping type. @@ -713,28 +714,37 @@ coq.typecheck-attribute N (oneof L) K _ (error Msg) :- std.fold S "" (s\ a\ calc (a ^ " " ^ s)) OneOf, Msg is "Attribute " ^ N ^ " takes one of " ^ OneOf ^ ", got: " ^ K. +pred append-string i:string, i:string, o:string. +append-string "" A A :- !. +append-string A B R :- R is A ^ "." ^ B. coq.parse-attributes L S O :- std.map S (x\r\ r = supported-attribute x) CS, CS => parse-attributes.aux L "" O, !. parse-attributes.aux [] _ []. -parse-attributes.aux [attribute S (node L)|AS] Prefix R :- if (Prefix = "") (PS = S) (PS is Prefix ^ "." ^ S), supported-attribute (att PS attmap), !, +parse-attributes.aux [attribute S (node L)|AS] Prefix R :- + append-string Prefix S PS, supported-attribute (att PS attlist), !, + parse-attributes.aux AS Prefix R1, + (pi x\ supported-attribute (att x bool) :- !) => parse-attributes.aux L "" Map, + std.append R1 [get-option PS Map] R. +parse-attributes.aux [attribute S (node L)|AS] Prefix R :- + append-string Prefix S PS, supported-attribute (att PS attmap), !, parse-attributes.aux AS Prefix R1, (pi x\ supported-attribute (att x string) :- !) => parse-attributes.aux L "" Map, std.append R1 [get-option PS Map] R. parse-attributes.aux [attribute S (node L)|AS] Prefix R :- !, parse-attributes.aux AS Prefix R1, - if (Prefix = "") (PS = S) (PS is Prefix ^ "." ^ S), + append-string Prefix S PS, parse-attributes.aux L PS R2, std.append R1 R2 R. parse-attributes.aux [attribute S (leaf-str V)|AS] Prefix CLS :- !, - if (Prefix = "") (PS = S) (PS is Prefix ^ "." ^ S), + append-string Prefix S PS, coq.valid-str-attribute PS V V1 Diag, if (Diag = error Msg) (coq.error Msg) true, if (V1 = some Val) (CLS = [get-option PS Val|R]) (CLS = R), % ignored parse-attributes.aux AS Prefix R. parse-attributes.aux [attribute S (leaf-loc V)|AS] Prefix CLS :- !, - if (Prefix = "") (PS = S) (PS is Prefix ^ "." ^ S), + append-string Prefix S PS, coq.valid-loc-attribute PS V Diag, if (Diag = error Msg) (coq.error Msg) true, CLS = [get-option PS V|R],