improve HB.instance (#421)

speedup toposort and instance search

Author: gares

.github/workflows/nix-action-coq-8.18.yml

@@ -11,7 +11,8 @@
       fourcolor.override.version = "master";
       odd-order.override.version = "master";
       mathcomp-finmap.override.version = "master";
-      mathcomp.analyis.override.version = "hierarchy-builder";
+      mathcomp-classical.override.version = "master";
+      mathcomp-analysis.override.version = "master";
       reglang.override.version = "master";
       coq-bits.override.version = "master";
       deriving.override.version = "master";

.github/workflows/nix-action-coq-8.19.yml

@@ -1 +1 @@
-"7e631f043d424ce82f3308824bf64fbfdee04c80"
+"816e3aa12d182f26fc6b173312ba46f2df727f90"

.github/workflows/nix-action-coq-master.yml

@@ -2,6 +2,11 @@
 
 ## Unreleased
 
+### General
+ - **Speedup** `HB.instance` does not try to infer classes that inherit from
+   a class that is known to have no instance (for the given type)
+ - **Speedup** `toposort` on `gref` uses OCaml's maps and sets rather than lists
+
 ## [1.7.0] - 2024-01-10
 
 Compatible with

.nix/config.nix

@@ -179,7 +179,7 @@ toposort-proj Proj ES In Out :- !, toposort-proj.acc Proj ES [] In Out.
 pred topo-find i:B, o:A.
 pred toposort-proj.acc i:(A -> B -> prop), i:list (pair B B), i:list B, i:list A, o:list A.
 toposort-proj.acc _ ES Acc [] Out :- !,
-  std.map {std.toposort ES Acc} topo-find Out.
+  std.map {std.gref.toposort ES Acc} topo-find Out.
 toposort-proj.acc Proj ES Acc [A|In] Out :- std.do![
   Proj A B,
   topo-find B A => toposort-proj.acc Proj ES [B|Acc] In Out
@@ -192,7 +192,7 @@ pred toposort-classes i:list classname, o:list classname.
 toposort-classes In Out :- std.do! [
   std.findall (sub-class C1_ C2_ _ _) SubClasses,
   std.map SubClasses toposort-classes.mk-class-edge ES,
-  std.toposort ES In Out,
+  std.gref.toposort ES In Out,
 ].
 
 pred findall-classes o:list class.

.nix/coq-nix-toolbox.nix

@@ -90,6 +90,32 @@ toposort ES XS XS'' :-
   toporec ES XS [] [] _ XS',
   std.filter XS' (std.mem XS) XS''.
 
+namespace gref {
+pred topovisit i: coq.gref.map coq.gref.set, i: classname,      i: coq.gref.set, i: list classname, i: coq.gref.set, o: coq.gref.set, o: list classname, o: coq.gref.set.
+topovisit _ X VS PS PSS VS PS PSS :- coq.gref.set.mem X PSS, !.
+topovisit _ X VS _ _ _ _ _ :- coq.gref.set.mem X VS, !, halt "cycle detected.".
+topovisit ES X VS PS PSS VS' [X|PS'] PSS'' :-
+  (coq.gref.map.find X ES M ; coq.gref.set.empty M),
+  toporec ES {coq.gref.set.elements M} {coq.gref.set.add X VS} PS PSS VS' PS' PSS',
+  coq.gref.set.add X PSS' PSS''.
+pred toporec   i: coq.gref.map coq.gref.set, i: list classname, i: coq.gref.set, i: list classname, i: coq.gref.set, o: coq.gref.set, o: list classname, o: coq.gref.set.
+toporec _ [] VS PS PSS VS PS PSS.
+toporec ES [X|XS] VS PS PSS VS'' PS'' PSS'' :-
+  topovisit ES X VS PS PSS VS' PS' PSS', toporec ES XS VS' PS' PSS' VS'' PS'' PSS''.
+
+pred add-to-neighbours i:coq.gref.set, i:pair gref gref, i:coq.gref.map coq.gref.set, o:coq.gref.map coq.gref.set.
+add-to-neighbours VS (pr _ V) A A :- not(coq.gref.set.mem V VS), !.
+add-to-neighbours _ (pr K V) A A1 :- coq.gref.map.find K A L, !, coq.gref.map.add K {coq.gref.set.add V L} A A1.
+add-to-neighbours _ (pr K V) A A1 :- coq.gref.map.add K {coq.gref.set.add V {coq.gref.set.empty} } A A1.
+
+pred toposort i:list (pair gref gref), i:list gref, o:list gref.
+toposort ES XS XS'' :- !, std.do! [
+  std.fold XS {coq.gref.set.empty} coq.gref.set.add VS,
+  std.fold ES {coq.gref.map.empty} (add-to-neighbours VS) EM,
+  toporec EM XS {coq.gref.set.empty} [] {coq.gref.set.empty} _ XS'' _
+].  
+}
+
 pred time-do! i:list prop.
 time-do! [].
 time-do! [P|PS] :-

Changelog.md

@@ -78,13 +78,20 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [
   acc-clauses current Clauses
 ].
 
+% [not-subclass-of X C] holds if C does not inherit from X
+pred not-subclass-of i:classname, i:class.
+not-subclass-of HasNoInstance (class C _ _) :- not(sub-class C HasNoInstance _ _).
+
 % [declare-all T CL MCSTL] given a type T and a list of class definition
 % CL in topological order (from least dep to most) looks for classes
 % for which all the dependencies (mixins) were postulated so far and skips the
 % rest. For each fulfilled class it declares a local constant inhabiting the
 % corresponding structure and declares it canonical.
 % Each mixin used in order to fulfill a class is returned together with its name.
 pred declare-all i:term, i:list class, o:list (pair id constant).
+declare-all _ [] [].
+declare-all T [class _ Struct _|Rest] L :- has-instance T Struct, !,
+  declare-all T Rest L.
 declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :-
 
   infer-class T Class Struct MLwP S Name STy Clauses,
@@ -95,19 +102,24 @@ declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :-
 
   Clauses => declare-all T Rest L.
 
-declare-all T [_|Rest] L :- declare-all T Rest L.
-declare-all _ [] [].
+declare-all T [class HasNoInstance _ _|Rest] L :-
+  % filter out classes we can't build for sure
+  std.filter Rest (not-subclass-of HasNoInstance) Rest1,
+  declare-all T Rest1 L.
 
 % for generic types, we need first to instantiate them by giving them holes,
 % so they can be used to instantiate the classes
 pred declare-all-on-type-constructor i:term, i:list class, o:list (pair id constant).
-declare-all-on-type-constructor T [class Class Struct MLwP|Rest] [pr Name CS|L] :-
+declare-all-on-type-constructor _ [] [].
+declare-all-on-type-constructor TK [class _ Struct _|Rest] L :- saturate-type-constructor TK T, has-instance T Struct, !,
+  declare-all-on-type-constructor TK Rest L.
+declare-all-on-type-constructor TK [class Class Struct MLwP|Rest] [pr Name CS|L] :-
 
   %TODO: compute the arity of the Class subject and saturate up to that point
   %      there may even be more than one possibility
-  saturate-type-constructor T Ty,
+  saturate-type-constructor TK T,
 
-  infer-class Ty Class Struct MLwP S Name _STy Clauses,
+  infer-class T Class Struct MLwP S Name _STy Clauses,
 
   !,
 
@@ -116,20 +128,23 @@ declare-all-on-type-constructor T [class Class Struct MLwP|Rest] [pr Name CS|L]
 
   decl-const-in-struct Name SC SCTy CS,
 
-  Clauses => declare-all-on-type-constructor T Rest L.
+  Clauses => declare-all-on-type-constructor TK Rest L.
 
-declare-all-on-type-constructor T [_|Rest] L :- declare-all-on-type-constructor T Rest L.
-declare-all-on-type-constructor _ [] [].
+declare-all-on-type-constructor TK [class HasNoInstance _ _|Rest] L :-
+  % filter out classes we can't build for sure
+  std.filter Rest (not-subclass-of HasNoInstance) Rest1,
+  declare-all-on-type-constructor TK Rest1 L.
 
-pred infer-class i:term, i:classname, i:gref, i:factories, o:term, o:string, o:term, o:list prop.
-infer-class T  Class Struct MLwP S Name STy Clauses:- std.do![
-
-  if (not(has-CS-instance? T Struct))
-     true % we build it
+pred has-instance i:term, i:structure.
+has-instance T Struct :-
+  if (has-CS-instance? T Struct)
      (if-verbose (coq.say {header} "skipping already existing"
                     {nice-gref->string Struct} "instance on"
-                    {coq.term->string T}),
-      fail),
+                    {coq.term->string T}))
+     fail. % we build it
+
+pred infer-class i:term, i:classname, i:gref, i:factories, o:term, o:string, o:term, o:list prop.
+infer-class T  Class Struct MLwP S Name STy Clauses:- std.do![
 
   params->holes MLwP Params,
   get-constructor Class KC,