Merge pull request #179 from math-comp/demo-2021-03-05

hierarchies of morphism

Author: gares

.gitignore

@@ -39,7 +39,7 @@ Makefile.test-suite.coq.conf
 .coqdeps.test-suite
 *.v.hb
 *.v.hb.old
-hb
+coq.hb
 HB/common/log.compat.elpi
 
 _minted-*

Changelog.md

@@ -6,6 +6,10 @@
   (re)declared by `HB.reexport`.
 - `#[compress_coercions]` attribute (off by default) to shorten coercions paths
   in the synthesis of instances.
+- `HB.check` is like `Check` but supports logging and can be disabled on a
+  selection of Coq versions.
+- Experimental support for structures with a function as the carrier, that is
+  hierarchies of morphisms.
 - `HB.instance K F` deprecated in favor of `HB.instance Definition`
 - `#[log]` and `#[log(raw)]` to get printed Coq commands equivalent to what HB
   is doing. The raw print has higher changes to be reparsable.
@@ -17,8 +21,9 @@
   the key of the mixin/factory
 - `#[infer(P)]` can be used to tell `HB.structure` to set things up so that
   parameter `P` is automatically inferred. E.g. if `P : Ring.type` then
-  `Structure.type` will take a `t : Type` and trigger a canonical inference
+  `Structure.type` will take a `t : Type` and trigger a canonical inference.
   to infer the `t_is_a_Ring : Ring.type` associated to `t`.
+  If `Structure` has a function carrier, one has to write `#[infer(P = "_ -> _")]`.
 
 ## [1.0.0] - 2020-12-16
 

HB/builders.elpi

@@ -147,8 +147,7 @@ pred postulate-factories i:id, i:context-decl.
 postulate-factories ModName (context-item IDT _ TySkel none t\ context-item IDF _ (TF t) none _\ context-end) :- !, std.do! [
   % TODO we should allow T to be anything.
   std.assert-ok! (coq.elaborate-ty-skeleton TySkel _ Ty) "builders-postulate-factory: illtyped context",
-  if (var Ty) (fresh-type Ty)
-     (std.assert-ok! (coq.unify-eq Ty {{Type}}) "The last context item before the factory must be a type variable"),
+  if (var Ty) (fresh-type Ty) true,
   if-verbose (coq.say "HB: postulating type" IDT),
   log.coq.env.add-section-variable-noimplicits IDT Ty C,
   TheType = global (const C),

HB/common/log.compat.current.elpi

@@ -35,7 +35,7 @@ log.private.log-vernac _.
 
 shorten log.private.coq.vernac.{ begin-module , end-module , begin-section, end-section }.
 shorten log.private.coq.vernac.{ import-module , export-module }.
-shorten log.private.coq.vernac.{ definition , variable , comment }.
+shorten log.private.coq.vernac.{ definition , variable , comment , check }.
 shorten log.private.coq.{ vernac.inductive , vernac.implicit }.
 shorten log.private.coq.vernac.{ canonical , abbreviation , notation , coercion }.
 shorten log.private.{ coq.vernac }.
@@ -100,6 +100,8 @@ coq.vernac->pp1 (vernac.implicit Local Name [L]) (box h [Locality, str "Argument
   std.intersperse spc PP1 PP.
 coq.vernac->pp1 (comment A) (box (hov 2) [str"(*", str S, str"*)"]) :-
   std.any->string A S.
+coq.vernac->pp1 (check T) (box (hov 2) [str"Check", spc, PPT, str"."]) :-
+  @holes! => coq.term->pp T PPT.
 
 pred local->locality i:bool, o:coq.pp.
 local->locality tt (str "Local ").

HB/common/log.elpi

@@ -125,6 +125,12 @@ log.coq.env.accumulate S DB CL :- std.do! [
   if-verbose (log.private.log-vernac (log.private.coq.vernac.comment CL)),
 ].
 
+pred log.coq.check i:term, o:term, o:term.
+log.coq.check Skel Ty T :- std.do! [
+  std.assert-ok! (coq.elaborate-skeleton Skel Ty T) "Check fails",
+  log.private.log-vernac (log.private.coq.vernac.check Skel),
+].
+
 namespace log.private {
 
 %%%%% Logging Utils %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -160,6 +166,7 @@ type coq.vernac.coercion      string -> gref -> class       -> coq.vernac.
 type coq.vernac.canonical     string                        -> coq.vernac.
 type coq.vernac.implicit      bool -> string -> list (list implicit_kind)  -> coq.vernac.
 type coq.vernac.comment       A                             -> coq.vernac.
+type coq.vernac.check         term                          -> coq.vernac.
 
 }
 

HB/common/phant-abbreviation.elpi

@@ -77,10 +77,16 @@ fun-implicit N Ty (t\private.phant-term AL (F t))
 % [fun-infer-type N T Ph Ph1] Adds an argument N of type T such that one passes 
 % a value V of type {{ Type }} the corresponding canonical VC of type T is passed
 % for N , eg `fun T (phT : phant T) => Ph`
-pred fun-infer-type i:name, i:term, i:(term -> phant-term), o:phant-term.
-fun-infer-type N Ty (t\private.phant-term AL (Bo t)) Out :-
+pred fun-infer-type i:class, i:name, i:term, i:(term -> phant-term), o:phant-term.
+fun-infer-type sortclass N Ty (t\private.phant-term AL (Bo t)) Out :-
   coq.name-suffix N "ph" PhN,
-  fun-implicit N Ty (t\private.phant-term [private.infer-type N|AL] (fun PhN {{ lib:@hb.phant lp:t }} _\ Bo t)) Out.
+  fun-implicit N Ty (t\private.phant-term [private.infer-type N sortclass|AL]
+                                          (fun PhN {{ lib:@hb.phant lp:t }} _\ Bo t)) Out.
+fun-infer-type funclass N Ty (t\private.phant-term AL (Bo t)) Out :-
+  coq.name-suffix N "ph" PhN,
+  fun-implicit N Ty (t\private.phant-term [private.infer-type N funclass|AL]
+                                          (fun PhN {{ lib:@hb.phantom (_ -> _) lp:t }} _\ Bo t)) Out.
+fun-infer-type C _ _ _ _  :- coq.error "HB: inference of parameters of call" C "not implemented yet".
 
 % TODO: this looks like a hack to remove
 pred append-fun-unify i:phant-term, o:phant-term.
@@ -104,7 +110,7 @@ type phant-term list phant-arg -> term -> phant-term.
 % - [Phant x]        using [infer-type]
 kind phant-arg type.
 type real name -> phant-arg.
-type infer-type name -> phant-arg.
+type infer-type name -> class -> phant-arg.
 type implicit phant-arg.
 type unify phant-arg.
 
@@ -162,9 +168,13 @@ build-abbreviation K F [] K F.
 build-abbreviation K F [real N|AL] K'' (fun N _ AbbrevFx) :- !,
   pi x\ build-abbreviation K {mk-app F [x]} AL K' (AbbrevFx x),
   K'' is K' + 1.
-build-abbreviation K F [infer-type N|AL] K'' (fun N _ AbbrevFx) :- !,
+build-abbreviation K F [infer-type N sortclass|AL] K'' (fun N _ AbbrevFx) :- !,
   pi x\ build-abbreviation K {mk-app F [{{ lib:hb.Phant lp:x }}]} AL K' (AbbrevFx x),
   K'' is K' + 1.
+build-abbreviation K F [infer-type N funclass|AL] K'' (fun N _ AbbrevFx) :- !,
+  pi x\ build-abbreviation K {mk-app F [{{ lib:hb.Phantom (_ -> _) lp:x }}]} AL K' (AbbrevFx x),
+  K'' is K' + 1.
+build-abbreviation _ _ [infer-type _ (grefclass _)|_] _ _ :- coq.error "TODO".
 build-abbreviation K F [implicit|AL] K' FAbbrev :- !,
   build-abbreviation K {mk-app F [_]} AL K' FAbbrev.
 build-abbreviation K F [unify|AL] K' FAbbrev :- !,
@@ -240,4 +250,4 @@ mk-phant-term.classes EtaF CNF PL T MLwA PhF :- !, std.do! [
 ].
 
 
-}}
+}}

HB/common/stdpp.elpi

@@ -133,7 +133,7 @@ pred copy-constructor i:indc-decl, o:indc-decl.
 copy-constructor (constructor ID A) (constructor ID A1) :- copy-arity A A1.
 
 % TODO: move to coq-elpi proper
-pred coq.gref.list->set i:list mixinname, o:coq.gref.set.
+pred coq.gref.list->set i:list gref, o:coq.gref.set.
 coq.gref.list->set L S :-
   std.fold L {coq.gref.set.empty} coq.gref.set.add S.
 

HB/common/utils.elpi

@@ -34,6 +34,7 @@ with-attributes P :-
     att "log.raw" bool,
     att "compress_coercions" bool,
     att "export" bool,
+    att "skip" string,
   ] Opts, !,
   Opts => P.
 
@@ -88,7 +89,7 @@ nice-gref->string X Mod :-
 nice-gref->string X S :-
   coq.term->string (global X) S.
 
-pred gref->modname i:mixinname, o:id.
+pred gref->modname i:gref, o:id.
 gref->modname GR ModName :-
   coq.gref->path GR Path,
   if (std.rev Path [_,ModName|_]) true (coq.error "No enclosing module for " GR).
@@ -162,9 +163,11 @@ w-params.fold.params (w-params.cons ID PTy F) Cons Nil RevPs Out :- !, std.do! [
   coq.id->name ID N,
   (@pi-decl N PTy p\ w-params.fold.params (F p) Cons Nil [p|RevPs] (Body p)),
   Cons N PTy Body Out].
-w-params.fold.params (w-params.nil ID TTy F) _ Nil RevParams Out :- !,
+w-params.fold.params (w-params.nil ID TTy F) _ Nil RevParams Out :- !, std.do! [
   coq.id->name ID N,
-  std.rev RevParams Params, !, Nil Params N TTy F Out.
+  std.rev RevParams Params,
+  Nil Params N TTy F Out,
+].
 
 % [w-params.then AwP Cons Nil Out] states that Out has shape
 %   Cons `x_1` T_1 p_1 \ .. \ Nil [p_1 .. p_n] `T` Ty t \ Body

HB/structure.elpi

@@ -61,8 +61,10 @@ declare Module B :- std.do! [
   if-verbose (coq.say "HB: start module Exports"),
 
   log.coq.env.begin-module "Exports",
-  if-arg-sort (private.declare-sort-coercion Structure (global (const ArgSortCst))),
-  private.declare-sort-coercion Structure SortProjection,
+
+  private.infer-coercion-tgt MLwP CoeClass,
+  if-arg-sort (private.declare-sort-coercion CoeClass Structure (global (const ArgSortCst))),
+  private.declare-sort-coercion CoeClass Structure SortProjection,
 
   if-verbose (coq.say "HB: exporting unification hints"),
   ClassAlias => Factories => GRDepsClauses =>
@@ -92,7 +94,7 @@ declare Module B :- std.do! [
 
   if-verbose (coq.say "HB: declaring on_ abbreviation"),
 
-  private.mk-infer-key ClassProjection NilwP (global Structure) PhClass,
+  private.mk-infer-key CoeClass ClassProjection NilwP (global Structure) PhClass,
 
   phant.add-abbreviation "on_" PhClass _ ClassOfAbbrev,
   (pi c\ coq.notation.abbreviation ClassOfAbbrev [c] (ClassOfAbbrev_ c)),
@@ -101,13 +103,12 @@ declare Module B :- std.do! [
 
   coq.mk-app (global ClassName) {params->holes NilwP} AppClassHoles,
   @global! => log.coq.notation.add-abbreviation "Build" 2
-    {{fun T C => (lp:(ClassOfAbbrev_ C) : (lp:AppClassHoles T))}} tt ClassForAbbrev,
+    {{fun T C => (lp:(ClassOfAbbrev_ C) : (lp:AppClassHoles T)) }} tt _,
 
   if-verbose (coq.say "HB: declaring on abbreviation"),
 
-  (pi t\ coq.notation.abbreviation ClassForAbbrev [t, t] (ClassForAbbrevDiag t)),
   @global! => log.coq.notation.add-abbreviation "on" 1
-    {{fun T => lp:(ClassForAbbrevDiag T)}} tt _,
+    {{fun T => (lp:{{ ClassOfAbbrev_ {{_}} }} : (lp:AppClassHoles T)) }} tt _,
 
   log.coq.env.end-module-name Module ModulePath,
 
@@ -146,6 +147,14 @@ namespace private {
 
 shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }.
 
+
+pred infer-coercion-tgt i:list-w-params mixinname, o:class.
+infer-coercion-tgt (w-params.cons ID Ty F) CoeClass :-
+  @pi-parameter ID Ty x\ infer-coercion-tgt (F x) CoeClass.
+infer-coercion-tgt (w-params.nil _ {{ Type }} _) sortclass.
+infer-coercion-tgt (w-params.nil _ {{ _ -> _ }} _) funclass.
+infer-coercion-tgt (w-params.nil _ _ _) _ :- coq.error "TODO1".
+
 % const Po : forall p1 .. pm T m1 .. mn, Extra  (Eg Extra = forall x y, x + y = y + z)
 % const C : forall p1 .. pm s, Extra
 % Po P1 .. PM T M1 .. MN PoArgs -> C P1 .. PM S PoArgs
@@ -166,7 +175,7 @@ clean-op-ty [exported-op _ Po C|Ops] S T1 T2 :-
 
 pred operation-body-and-ty i:list prop, i:constant, i:structure, i:term, i:term,
   i:list term, i:term, i:w-args A, o:pair term term.
-operation-body-and-ty EXI Poperation Struct Psort Pclass Params _T (triple _ Params _) (pr Bo Ty) :- std.do! [
+operation-body-and-ty EXI Poperation Struct Psort Pclass Params _T (triple _ ParamsOp _) (pr Bo Ty) :- std.do! [
   mk-app (global Struct) Params StructType,
   mk-app Psort Params PsortP,
   mk-app Pclass Params PclassP,
@@ -177,7 +186,7 @@ operation-body-and-ty EXI Poperation Struct Psort Pclass Params _T (triple _ Par
       mk-app PclassP [s] Class,
       synthesis.under-mixin-src-from-factory.do! Carrier Class [
         % just in case..
-        synthesis.infer-all-mixin-args Params Carrier (const Poperation) (Body s),
+        synthesis.infer-all-mixin-args ParamsOp Carrier (const Poperation) (Body s),
         std.assert-ok! (coq.typecheck (Body s) (DirtyTy s)) "export-1-operation: Body illtyped",
         clean-op-ty EXI s (DirtyTy s) (BodyTy s),
       ],
@@ -272,7 +281,7 @@ mk-coe-structure-body StructureF StructureT TC Coercion SortProjection ClassProj
     {coq.mk-n-holes {factory-nparams TC}} PackPH,
 
   SCoeBody = {{ fun s : lp:StructureP =>
-     let T : Type := lp:SortP s in
+     let T := lp:SortP s in
      lp:PackPH T (lp:CoercionP T (lp:ClassP s)) }},
 ].
 
@@ -461,13 +470,13 @@ declare-class+structure MLwP (indt ClassInd) (indt StructureInd) SortProjection
   global (const ClassP) = ClassProjection,
 ].
 
-% Declares "sort" as a coercion Structurename >-> Sortclass
-pred declare-sort-coercion i:structure, i:term.
-declare-sort-coercion StructureName (global Proj) :-
+% Declares "sort" as a Coercion Proj : Structurename >-> CoeClass.
+pred declare-sort-coercion i:class, i:structure, i:term.
+declare-sort-coercion CoeClass StructureName (global Proj) :-
 
   if-verbose (coq.say "HB: declare sort coercion"),
 
-  log.coq.coercion.declare (coercion Proj 0 StructureName sortclass).
+  log.coq.coercion.declare (coercion Proj 0 StructureName CoeClass).
 
 pred if-class-already-exists-error i:id, i:list class, i:list mixinname.
 if-class-already-exists-error _ [] _.
@@ -566,19 +575,22 @@ pred mk-infer i:term, i:list-w-params mixinname, o:phant-term.
 mk-infer T (w-params.nil _ _ _) PH :- phant.init T PH.
 mk-infer T (w-params.cons ID Ty W) R :- (get-option ID "Type" ; get-option ID ""), !,
   @pi-parameter ID Ty t\ mk-infer {mk-app T [t]} (W t) (PhT t),
-  phant.fun-infer-type {coq.id->name ID} Ty PhT R.
+  phant.fun-infer-type sortclass {coq.id->name ID} Ty PhT R.
+mk-infer T (w-params.cons ID Ty W) R :- (get-option ID "_ -> _"), !,
+  @pi-parameter ID Ty t\ mk-infer {mk-app T [t]} (W t) (PhT t),
+  phant.fun-infer-type funclass {coq.id->name ID} Ty PhT R.
 mk-infer T (w-params.cons ID Ty W) R :- not (get-option ID _), !,
   @pi-parameter ID Ty t\ mk-infer {mk-app T [t]} (W t) (PhT t),
   phant.fun-real {coq.id->name ID} Ty PhT R.
 mk-infer _ (w-params.cons ID _ _) _ :- get-option ID Infer,
   coq.error "Automatic inference of paramter" ID "from" Infer "not supported".
 
-pred mk-infer-key i:term, i:list-w-params mixinname, i:term, o:phant-term.
-mk-infer-key K (w-params.nil ID _ _) St PhK :-
+pred mk-infer-key i:class, i:term, i:list-w-params mixinname, i:term, o:phant-term.
+mk-infer-key CoeClass K (w-params.nil ID _ _) St PhK :-
   @pi-parameter ID St t\ phant.init {mk-app K [t]} (PhKBo t),
-  phant.fun-infer-type {coq.id->name ID} St PhKBo PhK.
-mk-infer-key K (w-params.cons ID Ty W) St R :-
-  @pi-parameter ID Ty t\ mk-infer-key {mk-app K [t]} (W t) {mk-app St [t]} (PhT t),
+  phant.fun-infer-type CoeClass {coq.id->name ID} St PhKBo PhK.
+mk-infer-key CoeClass K (w-params.cons ID Ty W) St R :-
+  @pi-parameter ID Ty t\ mk-infer-key CoeClass {mk-app K [t]} (W t) {mk-app St [t]} (PhT t),
   phant.fun-implicit {coq.id->name ID} Ty PhT R.
 
 pred if-coverage-not-good-error i:list mixinname.

README.md

@@ -71,8 +71,6 @@ Proof. by rewrite example. Qed.
 
 The software is beta-quality, it works but error messages should be improved.
 
-The current version forces the carrier to be a type, ruling hierarchies of morphisms out.
-
 This [draft paper](https://hal.inria.fr/hal-02478907) describes the language
 in full detail.