hierarchies of morphism

[gares]

No description provided.

[gares]

CI: Error: Anomaly "Uncaught exception Failure("sep_last")." this is known bugs, on coq-elpi < 1.9.0 you cannot write Definition _ := ..., you need to put a name in there. This occurs in the test file.

[gares]

One thing that is surely broken is the #[infer] attribute since we hardwire sortclass there, see #146 . I guess one may detect what the carrier is, but as a first approximation #[infer(P = "_ -> _")] may also work.

[gares]

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! [
  mk-app (global Struct) Params StructType,
  mk-app Psort Params PsortP,
  mk-app Pclass Params PclassP,
  Bo = fun `s` StructType Body,
  Ty = prod `s` StructType BodyTy,
  (@pi-decl `s` StructType s\ sigma Carrier Class\ std.do! [
      mk-app PsortP [s] Carrier,
      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),
        std.assert-ok! (coq.typecheck (Body s) (DirtyTy s)) "export-1-operation: Body illtyped",
        clean-op-ty EXI s (DirtyTy s) (BodyTy s),
      ],
  ]),
].

There is a problem/missing error message in this code. Params is used non-linearly, but in the silly test I wrote the parameters of the structure are not the same of the operation. This may not have much to do with this PR. Which is the right condition for giving an error?

In this case the structure has 2 parameters, the first occurrence, but the operation (mixin) zero.

[gares]

I think I fixed the code.
@CohenCyril is the infer thing acceptable or you have a better idea?

[gares]

It seems 8.11 has some problem, it rings a bell... I just don't recall if it was a bug in coq-elpi (for that version of Coq) or Coq itself.

[gares]

Given the prints, it is coq-elpi that declares a silly notation.

[gares]

@CohenCyril this PR is now ok, for what I can tell. You had some comments on the code I wrote during the demo you may put here.

[CohenCyril]

Looks ok but without extensive testing on mathcomp I find it a bit scary...

[gares]

Then we should merge it and document it as experimental. Otherwise it is harder to test.

[CohenCyril]

ok, let's merge the big one first!

[gares]

rebased

[CohenCyril]

I may have to rebase again after #187 ...

[gares]

About axioms_.
(* axioms_ : forall T : Type, (T -> T -> T) -> Prop

axioms_ is not universe polymorphic
Arguments axioms_ _%type_scope _%function_scope
Expands to: Inductive funclass.Magma.axioms_ *)
Notation on X1 :=  (phant_on_ _ _ (ssreflect.Phantom (forall H, _) X1) : axioms_ _ X1).
(* Error: X1 is here used in the empty scope stack while it was elsewhere used in scope function_scope *)

This looks like a real problem in Coq, but I'm not sure what it means.
I mean, I can make it pass by writing X1%function in the first occurrence of X1, but this is too hard.

[CohenCyril]

I mean, I can make it pass by writing X1%function in the first occurrence of X1, but this is too hard.

I am not sure what an automated scope inference could do to improve on this though...

[gares]

Notation on X1 := ((fun a => (phant_on_ _ _ (ssreflect.Phantom _ a) : axioms_ _ a)) X1).
(* OK *)

Seriously?

[gares]

CC rocq-prover/rocq#13965

[gares]

It is not so clear to me what to do here. The PR is ready, but logging is broken waiting for rocq-prover/rocq#13965

[gares]

I mean, it will break also in mathcomp if we start using morphisms

[gares]

look for a work around on 8.13 or postpone