Factory sort tactic

.github/workflows/main.yml

@@ -19,15 +19,18 @@ jobs:
         coq_version:
           - '8.13'
         ocaml_version:
-          - 'minimal'
+          - '4.07-flambda'
     steps:
     - uses: actions/checkout@v2
     - uses: coq-community/docker-coq-action@v1
       with:
         opam_file: './coq-hierarchy-builder.opam'
         coq_version: ${{ matrix.coq_version }}
         ocaml_version: ${{ matrix.ocaml_version }}
-
+        export: 'OPAMWITHTEST'  # space-separated list of variables
+      env:
+        OPAMWITHTEST: 'true'
+
   plan-B:
     runs-on: ubuntu-latest
     steps:
@@ -36,13 +39,13 @@ jobs:
       with:
         opam_file: './coq-hierarchy-builder.opam'
         coq_version: '8.13'
-        ocaml_version: 'minimal'
+        ocaml_version: '4.07-flambda'
         script: |
           mkdir /home/coq/workspace
           cp -ra . /home/coq/workspace
           cd /home/coq/workspace
           opam install ./coq-hierarchy-builder.opam
-          sed -i.bak "s/-Q . HB//" _CoqProject.test-suite
+          sed -i.bak -e "s/-Q . HB//" -e "s|tests/factory_sort_tac.v||" _CoqProject.test-suite
           # This is what a user does to cut HB loose
           export COQ_ELPI_ATTRIBUTES="hb(log(raw))"
           make test-suite -j2

.nix/config.nix

@@ -3,9 +3,10 @@
   attribute = "hierarchy-builder";
   default-bundle = "coq-8.13";
   bundles = let common = {
-      mathcomp.override.version = "hierarchy-builder";
+      mathcomp.override.version = "hierarchy-builder+factory_sort_tac";
       mathcomp.job = false;
       mathcomp-single.job = true;
+      coq-elpi.override.version = "#257";
   }; in {
     "coq-8.13".coqPackages = {
       coq.override.version = "8.13";

.nix/coq-overlays/coq-elpi/default.nix

@@ -4,18 +4,19 @@ with builtins; with lib; let
   elpi = coq.ocamlPackages.elpi.override (lib.switch coq.coq-version [
     { case = "8.11"; out = { version = "1.11.4"; };}
     { case = "8.12"; out = { version = "1.12.0"; };}
-    { case = "8.13"; out = { version = "1.13.5"; };}
+    { case = "8.13"; out = { version = "v1.13.6"; };}
   ] {});
 in mkCoqDerivation {
   pname = "elpi";
   repo  = "coq-elpi";
   owner = "LPCIC";
   inherit version;
   defaultVersion = lib.switch coq.coq-version [
-    { case = "8.13"; out = "1.10.2"; }
+    { case = "8.13"; out = "1.10.3"; }
     { case = "8.12"; out = "1.8.3_8.12"; }
     { case = "8.11"; out = "1.6.3_8.11"; }
   ] null;
+  release."1.10.3".sha256      = "0zxhyhykg36d3jh2kmdpvs58w5ni7mnyzvxvzrprbg7q2kbw6p23";
   release."1.10.2".sha256      = "02jjxq91dr5fybkyf4dwz5hlrwxij7jbgqka2d48s0aivvsk3hbi";
   release."1.10.1".sha256      = "1zsyx26dvj7pznfd2msl2w7zbw51q1nsdw0bdvdha6dga7ijf7xk";
   release."1.9.7".sha256      = "0rvn12h9dpk9s4pxy32p8j0a1h7ib7kg98iv1cbrdg25y5vs85n1";

HB/about.elpi

@@ -48,7 +48,9 @@ main-located S (loc-gref GR) :-
   std.filter {coq.CS.db-for _ (cs-gref GR)} (private.not1 private.unif-hint?) LV,
   coq.CS.db-for GR _ LP,
   std.filter {coq.coercion.db} (c\c = coercion GR _ _ _) LC,
-  if (LV = [], LP = [], LC = []) (coq.error "HB: unknown constant" S) true,
+  if (LV = [], LP = [], LC = [])
+     (coq.error "HB: uninteresting constant" {coq.pp->string {private.pp-loc-of GR}})
+     true,
   if (not (LV = [])) (private.main-canonical-value S LV) true,
   if (not (LP = [])) (private.main-canonical-projection S GR LP) true,
   if (not (LC = [])) (private.main-coercion S LC) true.
@@ -66,8 +68,7 @@ shorten coq.pp.{ v , h, hv, hov , spc , str , box , glue , brk , empty }.
 
 pred docstring-for-file i:string, o:prop.
 docstring-for-file Rex (docstring Loc Doc) :- docstring Loc Doc,
-  std.any->string Loc LocS,
-  rex.split "," LocS [File|_],
+  loc.fields Loc File _ _ _ _,
   rex.match {calc(".*" ^ Rex)} File.
 
 pred main-canonical-value i:string, i:list cs-instance.
@@ -83,8 +84,8 @@ main-canonical-value S CanonicalValues :-
 
 pred group-by-loc i:list cs-instance, o:list (pair (option loc) (list cs-instance)).
 group-by-loc [] [].
-group-by-loc [cs-instance P V (global GR)|L] [pr (some Loc) [cs-instance P V (global GR)|SameLoc]|Rest1] :- decl-location GR Loc, !,
-  std.partition L (x\ sigma GR1\ x = cs-instance _ _ (global GR1), decl-location GR1 Loc) SameLoc Rest,
+group-by-loc [cs-instance P V GR|L] [pr (some Loc) [cs-instance P V GR|SameLoc]|Rest1] :- decl-location GR Loc, !,
+  std.partition L (x\ sigma GR1\ x = cs-instance _ _ GR1, decl-location GR1 Loc) SameLoc Rest,
   group-by-loc Rest Rest1.
 group-by-loc [I|Rest] [pr none [I]|Rest1] :- group-by-loc Rest Rest1.
 
@@ -97,7 +98,7 @@ pp-canonical-solution-list (pr (some Loc) L) Pp :-
                  [ spc, {pp-loc Loc} ] }.
 
 pred pp-canonical-solution i:cs-instance, o:coq.pp.
-pp-canonical-solution (cs-instance _Proj _Pat (global GR)) Pp :-
+pp-canonical-solution (cs-instance _Proj _Pat GR) Pp :-
   coq.env.typeof GR T,
   coq.prod-tgt->gref T F,
   if (class-def (class _ F _)) (gref->modname F 2 "." ID) (coq.gref->string F ID),
@@ -205,15 +206,14 @@ main-factory-constructor S F PhBuild Build :-
   list-w-params_list DMLwP DML,
   factory-provides (indt F) PMLwP,
   list-w-params_list PMLwP PML,
-  factory-nparams (indt F) NParams,
-  coq.CS.canonical-projections F FieldsOpts,
+  coq.env.projections F FieldsOpts,
   std.map-filter FieldsOpts (x\r\ x = some r) Fields,
-  std.map Fields (c\r\coq.gref->id (const c) r) FieldsNames,
   coq.arguments.implicit PhBuild [Implicits],
-  std.map {std.iota NParams} std.any->string Params,
-  std.map Params (i\r\r is "P" ^ i) ParamsNames,
+
+  compute-arg-type DMLwP Fields [] ParamsNames TName FieldsNames ArgsTypes,
+  compute-field-info FieldsNames Implicits FieldsNamesInfo,
   std.map ParamsNames (n\r\r = str n) ParamsPp,
-  compute-field-info FieldsNames Implicits FieldsInfo,
+
   % format
   PpOrigin = box (hov 4) [
     str "HB: ", str S, str " is a factory constructor", spc,
@@ -224,11 +224,12 @@ main-factory-constructor S F PhBuild Build :-
   PpProvides = box (v 4) [
     str "HB: ", str S, str " provides the following mixins:",
     {bulletize PML pp-module}],
-  PpUsage = box h {std.intersperse spc [
+  PpUsage = box (v 4) [box h {std.intersperse spc [
     str "HB: arguments:",
     glue {std.intersperse spc [str S | ParamsPp]},
-    str "T",
-    glue FieldsInfo]},
+    str TName,
+    glue FieldsNamesInfo]},
+    {bulletize ArgsTypes pp-arg-type}],
   % print
   coq.say {coq.pp->string PpOrigin},  
   coq.say {coq.pp->string PpRequires},  
@@ -237,10 +238,41 @@ main-factory-constructor S F PhBuild Build :-
   print-docstring Build,
   coq.say.
 
+pred compute-arg-type i:list-w-params mixinname, i:list constant, i:list term, o:list id, o:id, o:list id, o:list (pair id coq.pp).
+compute-arg-type (w-params.cons ID Ty Rest) F Acc [ID|PN] TN FN [pr ID PPTy |Xs] :-
+  coq.term->pp Ty PPTy,
+  @pi-parameter ID Ty x\ compute-arg-type (Rest x) F [x|Acc] PN TN FN Xs.
+compute-arg-type (w-params.nil ID Ty Rest) F Acc [] ID FN [pr ID PPTy|Xs] :-
+  coq.term->pp Ty PPTy,
+  @pi-parameter ID Ty x\ compute-arg-type.fields F {std.length (Rest x)} {std.rev [x|Acc]} Xs FN.
+pred compute-arg-type.fields i:list constant, i:int, i:list term, o:list (pair id coq.pp), o:list id.
+compute-arg-type.fields [] _ _ [] [].
+compute-arg-type.fields [C|Cs] NDeps Args [pr ID PPTy|Xs] [ID|FN] :- exported-op _ C OP, !,
+  coq.env.typeof (const OP) Ty,
+  coq.gref->id (const OP) ID,
+  coq.subst-prod Args Ty TyArgs,
+  @pplevel! 200 => coq.term->pp TyArgs PPTy,
+  compute-arg-type.fields Cs NDeps Args Xs FN.
+compute-arg-type.fields [OP|Cs] NDeps Args [pr ID PPTy|Xs] [ID|FN] :-
+  % factories don't get exported ops, so we hack their types :-/
+  coq.env.typeof (const OP) OrigTy,
+  copy OrigTy Ty,
+  coq.gref->id (const OP) ID,
+  coq.subst-prod Args Ty TyArgs,
+  coq.mk-n-holes NDeps Deps,
+  coq.subst-prod Deps TyArgs TyArgsDeps,
+  coq.subst-prod [_] TyArgsDeps TyArgsDepsRecord,
+  ToDrop is NDeps + 2,
+  @pplevel! 200 => coq.term->pp TyArgsDepsRecord PPTy,
+  @pi-parameter ID TyArgsDepsRecord op\
+  (pi L L1 X\
+    copy (app[global(const OP)|L]) X :- std.drop ToDrop L L1, coq.mk-app op L1 X) =>
+    compute-arg-type.fields Cs NDeps Args Xs FN.
+
 pred main-factory i:string, i:inductive.
 main-factory S Factory :-
   % fetch
-  coq.CS.canonical-projections Factory Ps,
+  coq.env.projections Factory Ps,
   std.map-filter Ps (x\r\ x = some r) Fields,
   gref-deps (indt Factory) DMLwP,
   list-w-params_list DMLwP DML,
@@ -297,6 +329,9 @@ pp-module M (str ID) :- gref->modname M 2 "." ID.
 pred pp-const i:constant, o:coq.pp.
 pp-const F (str ID) :- coq.gref->id (const F) ID.
 
+pred pp-arg-type i:pair id coq.pp, o:coq.pp.
+pp-arg-type (pr ID PPTy) (box (hov 2) [str ID, str" :", spc, PPTy]).
+
 pred pp-if-verbose o:coq.pp, i:(coq.pp -> prop).
 pp-if-verbose V P :- get-option "verbose" tt, !, P V.
 pp-if-verbose empty _.
@@ -316,10 +351,8 @@ pp-loc-of _ coq.pp.empty.
 
 pred pp-loc i:loc, o:coq.pp.
 pp-loc Loc (coq.pp.glue PP) :-
-  std.any->string Loc SLoc,
-  % VSCode friendly
-  rex.split "," SLoc [File,_,Line|_],
-  QFile is "\"" ^ File ^ "\"," ^ Line,
+  loc.fields Loc File _ _ Line _,
+  QFile is "\"" ^ File ^ "\", line " ^ {std.any->string Line},
   PP = [str "(from ", str QFile, str")"].
 
 pred docstring->pp i:string, o:coq.pp.

HB/builders.elpi

@@ -6,23 +6,23 @@ namespace builders {
 pred begin i:context-decl.
 begin CtxSkel :- std.do! [
   Name is "Builders_" ^ {std.any->string {new_int}}, % TODO?
-  if-verbose (coq.say "HB: begin module for builders"),
+  if-verbose (coq.say {header} "begin module for builders"),
   log.coq.env.begin-module Name none,
 
   builders.private.factory CtxSkel IDF GRF,
 
   % the Super module to access operations/axioms shadowed by the ones in the factory
   if (GRF = indt FRecord) (std.do! [
-    if-verbose (coq.say "HB: begin module Super"),
+    if-verbose (coq.say {header} "begin module Super"),
     log.coq.env.begin-module "Super" none,
-    std.forall {coq.CS.canonical-projections FRecord}
+    std.forall {coq.env.projections FRecord}
       builders.private.declare-shadowed-constant,
     log.coq.env.end-module-name "Super" _,
-    if-verbose (coq.say "HB: ended module Super")
+    if-verbose (coq.say {header} "ended module Super")
   ]) (true),
 
   log.coq.env.begin-section Name,
-  if-verbose (coq.say "HB: postulating factories"),
+  if-verbose (coq.say {header} "postulating factories"),
   builders.private.postulate-factories Name IDF CtxSkel,
 ].
 
@@ -55,8 +55,8 @@ builders.end :- std.do! [
   std.forall Clauses (c\ log.coq.env.accumulate current "hb.db" (clause _ _ c)),
   std.forall ExportClausesFiltered (c\ log.coq.env.accumulate current "hb.db" (clause _ _ c)),
 
-  Clauses => ExportClausesFiltered => current-mode no-builder =>
-    instance.declare-factory-sort-factory GR,
+  % Clauses => ExportClausesFiltered => current-mode no-builder =>
+  %   instance.declare-factory-sort-factory GR,
 
   log.coq.env.end-module-name Name Exports,
   log.coq.env.end-module-name ModName _,
@@ -78,10 +78,10 @@ namespace builders.private {
 % From holds the (from F Mi Bi) new clauses during folding.
 pred declare-1-builder i:builder, i:list prop, o:list prop.
 declare-1-builder (builder _ SrcFactory TgtMixin _) FromClauses FromClauses :- FromClauses => from SrcFactory TgtMixin _, !,
-  if-verbose (coq.say "HB: skipping duplicate builder from"
+  if-verbose (coq.say {header} "skipping duplicate builder from"
     {nice-gref->string SrcFactory} "to" {nice-gref->string TgtMixin}).
 declare-1-builder (builder _ SrcFactory TgtMixin B) FromClauses [from SrcFactory TgtMixin B|FromClauses] :-
-  if-verbose (coq.say "HB: declare builder from"
+  if-verbose (coq.say {header} "declare builder from"
     {nice-gref->string SrcFactory} "to" {nice-gref->string TgtMixin}).
 
 % We add breviations for all constants what will be shadowed by projections
@@ -115,7 +115,7 @@ pred define-factory-operations i:term, i:list term, i:term, i:gref.
 define-factory-operations TheType Params TheFactory (indt I) :- !,
   coq.env.indt I _ NIParams _ _ _ _,
   NHoles is NIParams - 1 - {std.length Params},
-  coq.CS.canonical-projections I PL,
+  coq.env.projections I PL,
   std.forall PL (define-factory-operation TheType Params TheFactory NHoles).
 define-factory-operations _ _ _ _.
 

HB/common/database.elpi

@@ -248,14 +248,14 @@ get-structure-coercion S T (global F) :-
 
 pred get-structure-sort-projection i:structure, o:term.
 get-structure-sort-projection (indt S) Proj :- !,
-  coq.CS.canonical-projections S L,
+  coq.env.projections S L,
   if (L = [some P, _]) true (coq.error "No canonical sort projection for" S),
   Proj = global (const P).
 get-structure-sort-projection S _ :- coq.error "get-structure-sort-projection: not a structure" S.
 
 pred get-structure-class-projection i:structure, o:term.
 get-structure-class-projection (indt S) T :- !,
-  coq.CS.canonical-projections S L,
+  coq.env.projections S L,
   if (L = [_, some P]) true (coq.error "No canonical class projection for" S),
   T = global (const P).
 get-structure-class-projection S _ :- coq.error "get-structure-class-projection: not a structure" S.
@@ -267,7 +267,7 @@ get-constructor I _ :- coq.error "get-constructor: not an inductive" I.
 
 %% finding for locally defined structures
 pred get-cs-structure i:cs-instance, o:structure.
-get-cs-structure (cs-instance _ _ (global Inst)) Struct :- std.do! [
+get-cs-structure (cs-instance _ _ Inst) Struct :- std.do! [
   coq.env.typeof Inst InstTy,
   coq.prod-tgt->gref InstTy Struct
 ].
@@ -288,7 +288,7 @@ get-local-structures TyTrm StructL :- std.do! [
 pred local-cs? i:term, i:structure.
 local-cs? TyTerm (indt Struct) :- coq.version _ _ N _, N > 12, !,
   term->gref TyTerm Value,
-  coq.CS.canonical-projections Struct [some Proj, _],
+  coq.env.projections Struct [some Proj, _],
   coq.CS.db-for (const Proj) (cs-gref Value) L,
   not(L = []).
 local-cs? TyTerm Struct :-

HB/common/log.elpi

@@ -96,7 +96,7 @@ env.add-indt Decl I :- std.do! [
   coq.env.indt I _ _ _ _ KS _,
   log.private.log-implicits-of ff (indt I),
   std.forall KS (k\ env.add-location (indc k), log.private.log-implicits-of ff (indc k)),
-  std.forall {coq.CS.canonical-projections I}
+  std.forall {coq.env.projections I}
     (p\ sigma c\ if (p = some c) (env.add-location (const c), log.private.log-implicits-of ff (const c)) true),
 ].
 
@@ -196,6 +196,22 @@ log.coq.check Skel Ty T D :- std.do! [
   log.private.log-vernac (log.private.coq.vernac.check Skel Fail),
 ].
 
+pred refine i:term, i:goal, o:list sealed-goal. % to silence a warning, since this is only in tactics
+pred log.refine i:term, i:goal, o:list sealed-goal.
+log.refine T G GL :- std.do! [
+  refine T G GL,
+  G = goal _ _ _ Solution _,
+  log.private.log-tactic Solution,
+].
+pred refine.no_check i:term, i:goal, o:list sealed-goal. % to silence a warning, since this is only in tactics
+pred log.refine.no_check i:term, i:goal, o:list sealed-goal.
+log.refine.no_check T G GL :- std.do! [
+  refine.no_check T G GL,
+  G = goal _ _ _ Solution _,
+  log.private.log-tactic Solution,
+].
+
+
 namespace log.private {
 
 %%%%% Logging Utils %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -241,6 +257,7 @@ type coq.vernac.strategy      list constant -> conversion_strategy -> coq.vernac
 
 pred with-logging i:prop.
 pred log.private.log-vernac i:log.private.coq.vernac.
+pred log.private.log-tactic i:term.
 
 /*        Hierarchy Builder: algebraic hierarchies made easy
     This software is released under the terms of the MIT license              */
@@ -249,10 +266,11 @@ pred log.private.log-vernac i:log.private.coq.vernac.
 
 with-logging P :- (get-option "elpi.hb.log" _, NICE = tt ; get-option "elpi.hb.log.raw" _, NICE = ff), !,
   get-option "elpi.loc" Loc,
-  rex_split "," Loc [FILE|_],
+  loc.fields Loc FILE _ _ _ _,
+  std.any->string Loc LocStr,
   FILENAME is FILE ^ ".hb",
   open_append FILENAME OC1,
-  std.string.concat "\n" ["","HIERARCHY BUILDER PATCH v1",Loc,""] PATCH1,
+  std.string.concat "\n" ["","HIERARCHY BUILDER PATCH v1",LocStr,""] PATCH1,
   output OC1 PATCH1,
   close_out OC1,
   log.private.logger L NICE => P,
@@ -275,6 +293,11 @@ log.private.log-vernac V :- log.private.logger L Nice, !,
   log.private.logger-extend L {PPALL => log.private.coq.vernac->pp [V]}.
 log.private.log-vernac _.
 
+log.private.log-tactic P :- log.private.logger L Nice, !,
+  if (Nice = tt) (PPALL = []) (PPALL = [@ppall!]),
+  log.private.logger-extend L {PPALL => coq.term->pp P}.
+log.private.log-tactic _.
+
 % The main entry point to print vernacular commands is coq.vernac->pp
 
 shorten log.private.coq.vernac.{ begin-module , end-module , begin-section, end-section }.
@@ -332,9 +355,9 @@ coq.vernac->pp1 (vernac.parameter Name Ty) (box (hv 2) [box h [str "Parameter ",
   coq.term->pp Ty TY.
 coq.vernac->pp1 (import-module Name) (box h [str "Import ", str Name, str "."]).
 coq.vernac->pp1 (export-module Name) (box h [str "Export ", str Name, str "."]).
-coq.vernac->pp1 (notation KM NParams Term) (box (hv 2) [box h [str "Notation \"'",str KM,str"' "|StrParams], str "\" :=", spc, B, str " (at level 1)."]) :- !,
+coq.vernac->pp1 (notation KM NParams Term) (box (hv 2) [box h [str "Notation \"'",str KM,str"' "|StrParams], str "\" := (", spc, B, str ") (at level 1)."]) :- !,
   coq.vernac->ppabbrterm NParams Term StrParams B.
-coq.vernac->pp1 (abbreviation Name NParams Term) (box (hv 2) [box h [str "Notation ",str Name|StrParams], str " :=", spc, B, str "."]) :-
+coq.vernac->pp1 (abbreviation Name NParams Term) (box (hv 2) [box h [str "Notation ",str Name|StrParams], str " := (", spc, B, str ")."]) :-
   coq.vernac->ppabbrterm NParams Term StrParams B.
 coq.vernac->pp1 (canonical Name Local) (box h [Locality, str "Canonical ", str Name, str "."]) :-
   local->locality Local Locality.

HB/common/stdpp.elpi

@@ -102,7 +102,7 @@ constraint print-ctx mixin-src {
 % approximation, it should be logical path, not the file name
 pred coq.env.current-library o:string.
 coq.env.current-library L :- coq.version _ _ N _, N >= 13, !,
-  rex_split "," {get-option "elpi.loc"} [L|_].
+  loc.fields {get-option "elpi.loc"} L _ _ _ _.
 coq.env.current-library "dummy.v".
 
 pred coq.prod-tgt->gref i:term, o:gref.