Merge pull request #556 from FissoreD/warnings+get-inst-prio-api

TC : API coq.TC.get-inst-prio, warnings on hints

Author: gares

Changelog.md

@@ -12,6 +12,7 @@
 - Change `tc-instance`, now the type is `gref -> tc-priority -> tc-instance` i.e. the priority is not an integer anymore
 - New `coq.ltac.fresh-id` to generate fresh names in the proof context
 - New `@no-tc!` attribute supported by `coq.ltac.call-ltac1`
+- New `coq.TC.get-inst-prio` returns the `tc-priority` of an instance
 
 ### Apps 
 - New `tc` app providing an implementation of a type class solver written in elpi.

apps/tc/_CoqProject.test

@@ -1,4 +1,5 @@
 -arg -w -arg -Not-added
+-arg -w -arg -TC.hints
 
 # Hack to see Coq-Elpi even if it is not installed yet
 -Q ../../theories elpi

apps/tc/elpi/alias.elpi

@@ -1,6 +1,8 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
+accumulate base.
+
 pred alias i:term, o:term.
 
 pred replace-with-alias.aux i:list term, o:list term, o:bool.

apps/tc/elpi/compiler.elpi

@@ -1,6 +1,9 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
+accumulate base.
+accumulate tc_aux.
+
 % returns the classes on which the current gref depends
 pred get-class-dependencies i:gref, o:list gref.
 get-class-dependencies GR Res :-
@@ -97,7 +100,7 @@ compile-aux (prod N T F) I RevPremises ListVar [] IsPositive IsHead Clause ff :-
         (L = [NewPremise | RevPremises])) (L = RevPremises),
     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}), !,
+  not (is-option-active oTC-use-pattern-fragment-compiler), !,
   std.rev RevPremises Premises,
   coq.mk-app I {std.rev ListVar} AppInst,
   make-tc IsHead Ty AppInst Premises Clause.

apps/tc/elpi/create_tc_predicate.elpi

@@ -1,5 +1,9 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
+
+accumulate base.
+accumulate tc_aux.
+
 pred string->coq-mode i:string, o:hint-mode.
 string->coq-mode "bang" mode-ground :- !.
 string->coq-mode "plus" mode-input :- !.
@@ -14,14 +18,19 @@ 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").
 
+% Here we build the elpi modes a class CL. If CL has either zero or more than
+% one mode, then we consider all its parameter to be in output mode. If the
+% class has exactly one mode, then it is considered for the signature of the
+% predicate for CL 
 pred modes-of-class i:gref, o:list (pair argument_mode string).
-modes-of-class ClassGr Modes :- 
-  coq.hints.modes ClassGr "typeclass_instances" CoqModesList,
+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",
+  not (CoqModesList = [_,_|_], coq.warning "TC.Modes" "At the moment we only allow TC with at most 1 hint Mode (caused by class" {coq.gref->string ClassGR} ")"),
+  CoqModesList = [HintModesFst],
   std.append {std.map HintModesFst coq-mode->elpi} [pr out "term"] Modes.
-modes-of-class ClassGr Modes :- 
-  coq.env.typeof ClassGr ClassTy,
+modes-of-class ClassGR Modes :- 
+  coq.env.typeof ClassGR ClassTy,
   N is {coq.count-prods ClassTy} + 1, % + 1 for the solution
   list-init N (x\r\ r = (pr out "term")) Modes.
 

apps/tc/elpi/parser_addInstances.elpi

@@ -1,6 +1,10 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
+accumulate base.
+accumulate tc_aux.
+accumulate compiler.
+
 kind enum type.
 type path  string -> string -> enum.
 type addInstPrio int -> string -> enum.

apps/tc/elpi/rewrite_forward.elpi

@@ -1,6 +1,8 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
+accumulate base.
+
 pred forward i:term, o:term, o:list (pair (list term) term).
 
 % Auxiliary function for rewrite-forward

apps/tc/elpi/solver.elpi

@@ -1,8 +1,18 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
+accumulate base.
+
+pred time-solve i:prop.
+time-solve P :-
+  std.time P Time,
+  if (is-option-active oTC-time) (coq.say "[TC] Total resolution time is:" Time) true.
+
 msolve L N :- !,
-  coq.ltac.all (coq.ltac.open solve) {std.rev L} N.
+  time-solve (coq.ltac.all (coq.ltac.open solve-aux) {std.rev L} N).
+
+solve A L :- time-solve (solve-aux A L).
+
 
 pred build-context-clauses i:list prop, o:list prop.
 % Add the section's definition to the given context
@@ -20,48 +30,49 @@ tc-recursive-search Ty Sol :-
   std.time (coq.safe-dest-app Ty (global TC) TL',
     std.append TL' [Sol] TL,
     coq.elpi.predicate {gref->pred-name TC} TL Q, Q) Time,
-  if (is-option-active {oTC-resolution-time}) (coq.say "Instance search" Time) true.
+  if (is-option-active oTC-time-instance-search) (coq.say "[TC] Instance search time is:" Time) true.
 
 :if "solve-print-goal"
 solve (goal Ctx _ Ty _ _) _ :-
   coq.say "Ctx" Ctx "Ty" Ty, fail.
 
-% solve (goal C _ (prod N Ty F) S _ as _G) _L GL :- !,
+pred solve-aux i:goal, o:list sealed-goal.
+% solve-aux (goal C _ (prod N Ty F) S _ as _G) _L GL :- !,
 %   @pi-decl  N Ty x\
 %     declare-evar [decl x N Ty|C] (Raw x) (F x) (Sol x),
-%     solve (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _L GL,
+%     solve-aux (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _L GL,
 %     if (Sol x = app [HD, x]) (S = HD) (S = fun N Ty Sol).
-% solve (goal C _ (prod N Ty F) XX _ as G) _L GL :- !,
+% solve-aux (goal C _ (prod N Ty F) XX _ as G) _L GL :- !,
 %   % intros_if_needed Prod C [] 
 %   (@pi-decl  N Ty x\
 %     declare-evar [decl x N Ty|C] (Raw x) (F x) (Sol x),
-%     solve (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _L _,
+%     solve-aux (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _L _,
 %     coq.safe-dest-app (Sol x) Hd (Args x)),
 %     if (pi x\ last-no-error (Args x) x, std.drop-last 1 (Args x) NewArgs)
 %     (coq.mk-app Hd NewArgs Out, refine Out G GL) (
 %       % coq.say "Not eta" (Sol x) x (fun N Ty Sol),
 %       XX = (fun N Ty Sol)).
-% solve (goal C _ (prod N _ _ as P) _ A as G) _L GL :- !,
+% solve-aux (goal C _ (prod N _ _ as P) _ A as G) _L GL :- !,
 %   declare-evar C T P S',
 %   G' = (goal C T P S' A),
 %   refine (fun N _ _) G' GL1,
-%   coq.ltac.all (coq.ltac.open solve) GL1 _,
+%   coq.ltac.all (coq.ltac.open solve-aux) GL1 _,
 %   refine S' G GL.
-solve (goal C _ (prod N Ty F) _ _ as G) GL :- !,
+solve-aux (goal C _ (prod N Ty F) _ _ as G) GL :- !,
   (@pi-decl N Ty x\
     declare-evar [decl x N Ty|C] (Raw x) (F x) (Sol x),
-    solve (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _),
+    solve-aux (goal [decl x N Ty|C] (Raw x) (F x) (Sol x) []) _),
     if (pi x\ 
       % also check the head does not contain x
       coq.safe-dest-app (Sol x) Hd (Args x), 
       last-no-error (Args x) x, 
       std.drop-last 1 (Args x) NewArgs)
     (coq.mk-app Hd NewArgs Out, refine Out G GL1) (refine (fun N _ _) G GL1),
-    coq.ltac.all (coq.ltac.open solve) GL1 GL.
-% solve (goal _ _ (prod N _ _) _ _ as G) GL :- !,
+    coq.ltac.all (coq.ltac.open solve-aux) GL1 GL.
+% solve-aux (goal _ _ (prod N _ _) _ _ as G) GL :- !,
 %   refine (fun N _ _) G GL1,
-%   coq.ltac.all (coq.ltac.open solve) GL1 GL.
-solve (goal Ctx _ Ty Sol _ as G) GL :-
+%   coq.ltac.all (coq.ltac.open solve-aux) GL1 GL.
+solve-aux (goal Ctx _ Ty Sol _ as G) GL :-
   var Sol,
   build-context-clauses Ctx Clauses,
   % @redflags! coq.redflags.beta => coq.reduction.lazy.norm Ty Ty1,
@@ -71,10 +82,10 @@ solve (goal Ctx _ Ty Sol _ as G) GL :-
       % coq.say "Solution " X "end" X' "caio",
       % std.assert! (ground_term X') "solution not complete",
       % (pi F\ (copy (fun _ _ x\ (app [F, x])) F :- !)) => copy X X',
-      if (is-option-active {oTC-ignore-eta-reduction}) 
+      if (is-option-active oTC-ignore-eta-reduction) 
         (Proof' = Proof) (coq.reduction.eta-contract Proof Proof'),
       std.time (refine Proof' G GL) Refine-Time, 
-      if (is-option-active {oTC-time-refine}) (coq.say "Refine Time" Refine-Time) true;
+      if (is-option-active oTC-time-refine) (coq.say "[TC] Refine time is:" Refine-Time) true;
       coq.error "illtyped solution:" {coq.term->string Proof}
     ) 
     (GL = [seal G]).

apps/tc/elpi/tc_aux.elpi

@@ -1,10 +1,14 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
+accumulate base.
+
 % Contains the list of classes that
 % cannot be compiled
 
 % returns the TC from the type of an instance
+% TODO: This gould be replaced with an api 
+% coq.TC.get-class-of-inst i:gref, o:gref
 pred get-TC-of-inst-type i:term, o:gref.
 get-TC-of-inst-type (prod _ _ A) GR:-
   pi x\ get-TC-of-inst-type (A x) GR.
@@ -67,12 +71,15 @@ get-last (app L) R :-
 % TC preds are on the form tc-[PATH_TO_TC].tc-[TC-Name]
 pred gref->pred-name i:gref, o:string.
 gref->pred-name Gr S :-
-  if (is-option-active {oTC-clauseNameShortName})
+  if (is-option-active oTC-clauseNameShortName)
     (Path = "")
     (coq.gref->path Gr [Hd | Tl], 
       std.fold Tl Hd (x\acc\r\ r is acc ^ "." ^ x) Path', 
       Path is Path' ^ ".tc-"),
-  S is "tc-" ^ Path ^ {coq.gref->id Gr}.
+  % CAVEAT : Non-ascii caractars can't be part of a pred
+  %          name, we replace ö with o
+  rex.replace "ö" "o" {coq.gref->id Gr} GrStr,
+  S is "tc-" ^ Path ^ GrStr.
 
 pred no-backtrack i:list prop, o:list prop. 
 no-backtrack [] [].
@@ -90,23 +97,20 @@ make-tc _IsHead Ty Inst Hyp Clause :-
       (Hyp = [Hd]) (Clause = (Q :- Hd)) 
       (Clause = (Q :- Hyp)).
 
+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.
-get-inst-prio InstGr Prio :-
-  coq.env.typeof InstGr InstTy,
-  get-TC-of-inst-type InstTy TC,
-  find-opt {coq.TC.db-for TC} 
-    (x\ tc-instance InstGr (tc-priority-given Prio) = x ;
-        tc-instance InstGr (tc-priority-computed Prio) = x)
-      (some _), !.
-get-inst-prio _ 0.
-
-% TODO: @FissoreD improve this method complexity
+get-inst-prio InstGR Prio :-
+  coq.env.typeof InstGR InstTy,
+  get-TC-of-inst-type InstTy ClassGR,
+  unwrap-prio {coq.TC.get-inst-prio ClassGR InstGR} Prio.
+
 pred get-full-path i:gref, o:string.
-% :if "get-full-path"
 get-full-path Gr Res' :-
   coq.gref->string Gr Path,
   coq.env.current-section-path SectionPath,
   std.fold SectionPath "" (e\acc\r\ r is acc ^ "." ^ e) Res,
   Res' is Res ^ Path.
-% get-full-path _ _.

apps/tc/theories/add_commands.v

@@ -3,18 +3,15 @@
 
 From elpi.apps Require Import db.
 
-From elpi.apps.tc Extra Dependency "base.elpi" as base.
+From elpi.apps.tc Extra Dependency "tc_aux.elpi" as tc_aux.
 From elpi.apps.tc Extra Dependency "compiler.elpi" as compiler.
 From elpi.apps.tc Extra Dependency "parser_addInstances.elpi" as parser_addInstances.
 From elpi.apps.tc Extra Dependency "solver.elpi" as solver.
-From elpi.apps.tc Extra Dependency "tc_aux.elpi" as tc_aux.
 From elpi.apps.tc Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate.
 
 Elpi Command TC.AddAllInstances.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
 Elpi Accumulate File compiler.
 Elpi Accumulate lp:{{  
   main L :- 
@@ -26,9 +23,6 @@ Elpi Typecheck.
 Elpi Command TC.AddInstances.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
-Elpi Accumulate File tc_aux.
-Elpi Accumulate File compiler.
 Elpi Accumulate File parser_addInstances.
 Elpi Accumulate lp:{{
   main Arguments :- 
@@ -39,21 +33,18 @@ Elpi Typecheck.
 Elpi Command TC.AddAllClasses.
 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 _ :-
-    coq.TC.db-tc TC,
-    std.forall TC (add-class-gr classic).
+  % Ignore is the list of classes we do not want to add
+  main IgnoreStr :-
+    std.map IgnoreStr (x\r\ sigma S\ str S = x, coq.locate S r) IgnoreGR,
+    std.forall {coq.TC.db-tc} (x\ if (std.mem IgnoreGR x) true (add-class-gr classic x)).
 }}.
 Elpi Typecheck.
 
 Elpi Command TC.AddClasses.
 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 L :-
@@ -67,7 +58,6 @@ Elpi Typecheck.
 Elpi Command TC.AddHook.
 Elpi Accumulate Db tc.db.
 Elpi Accumulate Db tc_options.db.
-Elpi Accumulate File base.
 Elpi Accumulate File tc_aux.
 Elpi Accumulate lp:{{
   pred addHook i:grafting, i:string. 
@@ -98,8 +88,6 @@ 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.