hb.elpi

/*        Hierarchy Builder: algebraic hierarchies made easy
    This software is released under the terms of the MIT license              */

%%%%%%% Naming converntions %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

/*
   - under-foobar.do! Arg [ Code ]
     enriches the context with foobar, the runs std.do! [ Code ]
   - under-foobar.then Arg F Out
     enriches the context with foobar, the runs F Out, as a consequence
     the spilling expression {under-foobar.then Arg F} can be used
   - foo_bar
     projection from foo to its field bar
   - foo->bar
     conversion from type foo to type bar (it can be arbitrarily complex)
   - get-foobar
     reads foobar from the Coq world
   - findall-foobar
     reads foobar from hb.db, the output is sorted whenever it makes sense
   - main-foobar
     main entry point for a user facing (or almost user facing) command foobar
   - declare-foobar
     predicate adding to the Coq ennvironment a foobar
   - postulate-foobar
     predicate assuming a foobar (declaring a Coq section variable)
   - TheType, TheClass, TheFoobar
     the thing the current code is working on, eg the type of the structure
     begin defined
   - FooAlias
     see phant-abbrev, used to talk about the non canonical name of Foo
   - when foo is the constructor of a data type with type A1 -> .. -> AN -> t
     we define mk-foo as:
       mk-foo A1 .. AN (foo A1 .. AN)
*/

shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }.

%%%%%%%%% Elpi Utils %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% This code could be moved in Elpi's standard library

% printing the local mixin context
pred print-ctx.
print-ctx :- declare_constraint print-ctx [].
constraint print-ctx mixin-src {
  rule \ (G ?- print-ctx) | (coq.say "The context is:" G).
}

% TODO: pred toposort i:(A -> A -> prop), i:list A, o:list A.
%       pred edge? i:int, i:int.
%       toposort edge? [1,2,3,4] TopoList
pred topovisit i: list (pair A A), i: A,      i: list A, i: list A, o: list A, o: list A.
topovisit _ X VS PS VS PS :- std.mem PS X, !.
topovisit _ X VS _ _ _ :- std.mem VS X, !, halt "cycle detected.".
topovisit ES X VS PS VS' [X|PS'] :-
  toporec ES {std.map {std.filter ES (e\ fst e X)} snd} [X|VS] PS VS' PS'.
pred toporec   i: list (pair A A), i: list A, i: list A, i: list A, o: list A, o: list A.
toporec _ [] VS PS VS PS.
toporec ES [X|XS] VS PS VS'' PS'' :-
  topovisit ES X VS PS VS' PS', toporec ES XS VS' PS' VS'' PS''.
pred toposort i: list (pair A A), i: list A, o: list A.
toposort ES XS XS'' :-
  toporec ES XS [] [] _ XS',
  std.filter XS' (std.mem XS) XS''.

pred bubblesort i:list A, i:(A -> A -> prop), o:list A.
bubblesort [] _ [] :- !.
bubblesort [X] _ [X] :- !.
bubblesort [X,Y|TL] Rel [X|Rest1] :- Rel X Y, !, bubblesort [Y|TL] Rel Rest1.
bubblesort [X,Y|TL] Rel [Y|Rest1] :- bubblesort [X|TL] Rel Rest1.

pred list-diff i:list A, i:list A, o:list A.
list-diff X [] X.
list-diff L [D|DS] R :-
  std.filter L (x\ not(x = D)) L1,
  list-diff L1 DS R.

pred list-eq-set i:list A, i:list A.
list-eq-set L1 L2 :- list-diff L1 L2 [], list-diff L2 L1 [].

pred mk-n-holes i:int, o:list A.
mk-n-holes 0 [] :- !.
mk-n-holes N [HOLE_|R] :- M is N - 1, mk-n-holes M R.

pred under.do! i:((A -> Prop) -> A -> prop), i:list prop.
under.do! Then LP :- Then (_\ std.do! LP) _.

%%%%% HB Utils %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% API, compat between 8.10 and 8.11
pred add-abbrev i:id, i:int, i:term, i:global?, i:bool, o:abbreviation.
add-abbrev N NParams AbbrevT Global OnlyParse Abbrev :-
  if (coq.version _ 8 10 _)
     (std.unsafe-cast coq.notation.add-abbreviation F, F N NParams AbbrevT Global OnlyParse Abbrev)
     (std.unsafe-cast coq.notation.add-abbreviation G, G N NParams AbbrevT Global OnlyParse _ Abbrev). % 8.11 has a deprecation flag

% runs P in a context where Coq #[attributes] are parsed
pred with-attributes i:prop.
with-attributes P :-
  attributes A, coq.parse-attributes A [att "verbose" bool] Opts, !,
  Opts => P.

pred if-verbose i:prop.
if-verbose P :- get-option "verbose" tt, !, P.
if-verbose _.

% TODO: Should this only be used for gref that are factories? (and check in the first/second branch so?)
% Should we make this an HO predicate, eg "located->gref S L is-factory? GR"
pred located->gref i:string, i:list located, o:gref.
located->gref _ [loc-gref GR|_] GR.
located->gref _ [loc-abbreviation Abbrev|_] GR :- phant-abbrev GR _ Abbrev, !.
located->gref S [loc-abbreviation _|_] _ :- coq.error S "is an abbreviation out of the control of HB".
located->gref S [loc-modpath _|_] _ :- coq.error S "should be a factory, but is a module".
located->gref S [loc-modtypath _|_] _ :- coq.error S "should be a factory, but is a module type".
located->gref S [] _ :- coq.error "Could not locate name" S.

% TODO: generalize/rename when we support parameters
pred argument->gref i:argument, o:gref.
argument->gref (str S) GR :- located->gref S {coq.locate-all S} GR.
argument->gref X _ :- coq.error "Argument" X "is expected to be a string".

pred argument->term i:argument, o:term.
argument->term (str S) (global GR) :- !, argument->gref (str S) GR.
argument->term (trm T) T :- !, std.assert-ok! (coq.typecheck T _) "not well typed term".
argument->term X _ :- coq.error "Argument" X " is expected to be a term or a string".

% Type to share code between HB.mixin and HB.factory (that supports alias factories)
kind asset type.
type asset-mixin asset.
type asset-factory asset.

kind asset-decl type.
type asset-parameter  id -> term -> (term -> asset-decl) -> asset-decl.
type asset-record     id -> term -> id -> record-decl    -> asset-decl.
type asset-alias      id -> term                         -> asset-decl.

pred name-of-asset-decl i:asset-decl, o:string.
name-of-asset-decl (asset-parameter _ _ R) X :-
  pi x\ name-of-asset-decl (R x) X.
name-of-asset-decl (asset-record X _ _ _) X.
name-of-asset-decl (asset-alias X _) X.

pred argument->asset i:argument, o:asset-decl.
argument->asset (indt-decl (parameter ID _ImplicitStatus Ty I)) (asset-parameter ID Ty A) :- !,
  % Should we check that _ImplicitStatus is explicit?
  coq.string->name ID Name,
  @pi-decl Name Ty a\
    argument->asset (indt-decl (I a)) (A a).
argument->asset (indt-decl (record Rid Ty Kid F)) (asset-record Rid Ty Kid F) :- !.
argument->asset (const-decl Id (some (fun _ _ Bo)) (parameter ID _ Src Ty)) (asset-parameter ID Src A) :- !,
  coq.id->name ID Name,
  @pi-decl Name Src a\
    argument->asset (const-decl Id (some (Bo a)) (Ty a)) (A a).
argument->asset (const-decl Id (some Bo) (arity Ty)) (asset-alias Id Bo) :- !,
  std.assert! (var Ty) "Factories aliases should not be given a type".
argument->asset X _ :- coq.error "Unsupported asset:" X.

pred builder->string i:builder, o:string.
builder->string (builder _ _ B) S :- coq.term->string B S.

pred nice-gref->string i:gref, o:string.
nice-gref->string X Mod :-
  coq.gref->path X Path,
  std.rev Path [_,Mod|_].
nice-gref->string X S :-
  coq.term->string (global X) S.

pred target-gref i:term, o:gref.
target-gref T GR :- whd1 T T1, !, target-gref T1 GR.
target-gref (prod N Src Tgt) GR :- !, @pi-decl N Src x\ target-gref (Tgt x) GR.
target-gref End GR :- term->gref End GR.

% Sometimes section variables are unused, hence the lambda may not be there
pred subst-fun-opt i:term, i:term, o:term.
subst-fun-opt T (fun _ _ _ as F) O :- !, subst-fun [T] F O.
subst-fun-opt T (let _ _ _ _ as F) O :- !, subst-fun [T] F O.
subst-fun-opt _ X X.

pred append-phant-unify i:phant-term, o:phant-term.
append-phant-unify (phant-term LP T) (phant-term LPU T) :-
  std.append LP [unify-arg] LPU.

pred copy-fields i:record-decl, o:record-decl.
copy-fields end-record end-record.
copy-fields (field C N T R) (field C N T1 R1) :-
  copy T T1,
  pi x\ copy x x => copy-fields (R x) (R1 x).

pred copy-triple i:(A -> A1 -> prop), i:(B -> B1 -> prop), i:(C -> C1 -> prop), i:triple A B C, o:triple A1 B1 C1.
copy-triple F G H (triple X Y Z) (triple X1 Y1 Z1) :- F X X1, G Y Y1, H Z Z1.

pred triple_1 i:triple A B C, o:A.
triple_1 (triple A _ _) A.

pred copy-list i:(A -> A1 -> prop), i:list A, o: list A1.
copy-list _ [] [].
copy-list F [X|XS] [Y|YS] :- F X Y, copy-list F XS YS.

pred gref->modname i:mixinname, o:id.
gref->modname GR ModName :-
  coq.gref->path GR Path,
  if (std.rev Path [_,ModName|_]) true (coq.error "No enclosing module for " GR).

pred term->modname i:structure, o:id.
term->modname T ModName :- gref->modname {term->gref T} ModName.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% function to predicate generic constructions %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

pred mk-nil o:any.
mk-nil [].
pred mk0 i:any, o:any.
mk0 F R :- constant R F [].
pred mk1 i:any, i:any, o:any.
mk1 F X1 R :- constant R F [X1].
pred mk2 i:any, i:any, i:any, o:any.
mk2 F X1 X2 R :- constant R F [X1, X2].
pred mk3 i:any, i:any, i:any, i:any, o:any.
mk3 F X1 X2 X3 R :- constant R F [X1, X2, X3].
pred mk4 i:any, i:any, i:any, i:any, i:any, o:any.
mk4 F X1 X2 X3 X4 R :- constant R F [X1, X2, X3,X4].

pred mk-fun i:name, i:term, i:(term -> term), o:term.
mk-fun N Ty Body (fun N Ty Body).

% generic argument to pass to w-params
pred ignore i:name, i:term, i:(term -> A), o:A.
ignore _ _ F X :- (pi x y\ F x = F y), X = F (sort prop).

% combining body and type
pred mk-fun-prod i:name, i:term, o:(term -> pair term term), o:pair term term.
mk-fun-prod N Ty (x\ pr (Body x) (Type x)) (pr (fun N Ty Body) (prod N Ty Type)).

pred mk-parameter i:implicit_kind, i:name, i:term, i:(term -> indt-decl), o:indt-decl.
mk-parameter IK Name X F Decl :- !, Decl = parameter {coq.name->id Name} IK X F.

%%%%%%%%%%%%%%%%%%%%%%
% w-params interface %
%%%%%%%%%%%%%%%%%%%%%%

pred apply-w-params i:w-params A, i:list term, i:term, o:A.
apply-w-params (w-params.cons _ _ PL) [P|PS] T R :- !, apply-w-params (PL P) PS T R.
apply-w-params (w-params.nil _ _ L) [] T R :- !, R = L T.
apply-w-params _ _ _ _ :- coq.error "apply-w-params".

pred w-params.nparams i:w-params A, o:int.
w-params.nparams (w-params.cons _ _ F) N :- pi x\ w-params.nparams (F x) M, N is M + 1.
w-params.nparams (w-params.nil _ _ _) 0.

% [w-params.fold AwP Cons Nil Out] states that Out has shape
%   Cons `x_1` T_1 p_1 \ .. \ Nil [p_1 .. p_n] `T` Ty F
%   where AwP = w-params.cons `x_1` T_1 p_1 \ ... \ w-params.nil `T` Ty F
pred w-params.fold i:w-params A, i:(name -> term -> (term -> B) -> B -> prop),
   i:(list term -> name -> term -> (term -> A) -> B -> prop), o:B.
w-params.fold L Cons Nil Out :- w-params.fold.params L Cons Nil [] Out.

pred w-params.fold.params i:w-params A,
   i:(name -> term -> (term -> B) -> B -> prop),
   i:(list term -> name -> term -> (term -> A) -> B -> prop),
   i:list term, % accumulator
   o:B.
w-params.fold.params (w-params.cons N PTy F) Cons Nil RevPs Out :- !, std.do! [
  (@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 NT TTy F) _ Nil RevParams Out :- !,
  std.rev RevParams Params, !, Nil Params NT 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
%   where Pred [p_1 .. p_n] T Body
%   and AwP = w-params.cons `x_1` T_1 p_1 \ ... \ w-params.nil `T` Ty F
pred w-params.then i:w-params A,
   i:(name -> term -> (term -> C) -> C -> prop),
   i:(name -> term -> (term -> B) -> C -> prop),
   i:(list term -> term -> A -> B -> prop),
   o:C.
w-params.then L Cons Nil Pred Out :-
  w-params.fold L Cons (ps\ n\ ty\ f\ out\ sigma Body\
    (@pi-decl n ty t\ Pred ps t (f t) (Body t)),
    Nil n ty Body out) Out.

pred w-params.map i:w-params A, i:(list term -> term -> A -> B -> prop), o:w-params B.
w-params.map AL F BL :- w-params.then AL (mk3 w-params.cons) (mk3 w-params.nil) F BL.

% on the fly abstraction
pred bind-nil i:name, i:term, i:term, i:A, o:w-params A.
bind-nil N T X V (w-params.nil N T A) :- V = A X.

pred bind-cons i:name, i:term, i:term, i:w-params A, o:w-params A.
bind-cons N T X V (w-params.cons N T A) :- V = A X.

% Specific to list-w-params
pred list-w-params_list i:list-w-params A, o:list A.
list-w-params_list AwP R :- w-params.then AwP ignore ignore
   (p\ t\ x\ std.map x triple_1) R.

pred list-w-params.append i:list-w-params A, i:list-w-params A, o:list-w-params A.
list-w-params.append (w-params.nil N T ML1) (w-params.nil N T ML2) (w-params.nil N T ML) :-
  pi x\ std.append (ML1 x) (ML2 x) (ML x).
list-w-params.append (w-params.cons N Ty ML1) (w-params.cons N Ty ML2) (w-params.cons N Ty ML) :-
  pi x\ list-w-params.append (ML1 x) (ML2 x) (ML x).

pred list-w-params.flatten-map
  i:list-w-params A,
  i:(A -> list-w-params B -> prop),
  o:list-w-params B.
list-w-params.flatten-map (w-params.cons N T L) F (w-params.cons N T L1) :-
  @pi-decl N T p\
    list-w-params.flatten-map (L p) F (L1 p).
list-w-params.flatten-map (w-params.nil N TTy L) F (w-params.nil N TTy L1) :-
  @pi-decl N TTy t\
    list-w-params.flatten-map.aux (L t) F (L1 t).

pred list-w-params.flatten-map.aux
  i:list (w-args A), i:(A -> list-w-params B -> prop), o:list (w-args B).
list-w-params.flatten-map.aux [] _ [].
list-w-params.flatten-map.aux [triple M Ps T|L] F Res1 :-
  F M MwP,
  apply-w-params MwP Ps T ML,
  list-w-params.flatten-map.aux L F Res,
  std.append ML Res Res1.

% [build-list-w-params TheParams TheType Factorties ListWParams]
% Params is a list of pairs (section variable, its type).
% ListWParams has as many w-params.cons as TheParams and the terms
% in Factories are abstracted wrt the first component of TheParams.
pred build-list-w-params i:list (pair term term), i:term, i:list (w-args A), o: list-w-params A.
build-list-w-params [pr P Pty|PS] TheType Factories (w-params.cons `p` Pty1 R) :- std.do! [
  copy Pty Pty1,
  (pi p\ (copy P p :- !) => build-list-w-params PS TheType Factories (R p)),
].
build-list-w-params [] TheType Factories (w-params.nil `t` TT R) :- std.do! [
  std.assert-ok! (coq.typecheck TheType TT) "BUG: TheType does not typecheck",
  (pi t\ (copy TheType t :- !) =>
         std.map Factories (copy-triple (=) (copy-list copy) copy) (R t)),
].

pred distribute-w-params i:list-w-params A, o:list (one-w-params A).
distribute-w-params (w-params.cons N T F) L :-
  pi x\ distribute-w-params (F x) (L1 x), std.map (L1 x) (bind-cons N T x) L.
distribute-w-params (w-params.nil N T F) L :-
  pi x\ std.map (F x) (bind-nil N T x) L.

% Specific to one-w-params
pred w-params_1 i:one-w-params A, o:A.
w-params_1 X Y :- w-params.then X ignore ignore (p\ t\ triple_1) Y.

%%%%%%%%% HB database %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%Specialize coq.elpi.accumulate to "hiearchy.db"
pred acc i:scope, i:clause.
acc S CL :- coq.elpi.accumulate S "hb.db" CL.

pred from_mixin i:prop, o:mixinname.
from_mixin (from _ X _) X.

pred from_builder i:prop, o:term.
from_builder (from _ _ X) X.

pred mixin-src_mixin i:prop, o:mixinname.
mixin-src_mixin (mixin-src _ M _) M.

pred extract-builder i:prop, o:builder.
extract-builder (builder-decl B) B.

pred leq-builder i:builder, i:builder.
leq-builder (builder N _ _) (builder M _ _) :- N =< M.

% [factory-alias->gref X GR] when X is already a factory X = GR
% however, when X is a phantom abbreviated gref, we find the underlying
% factory gref GR associated to it.
pred factory-alias->gref i:gref, o:gref.
factory-alias->gref PhGR GR :- phant-abbrev GR PhGR _, !.
factory-alias->gref GR GR :- phant-abbrev GR _ _, !.

pred sub-class? i:class, i:class.
sub-class? (class _ _ ML1P) (class _ _ ML2P) :-
  list-w-params_list ML1P ML1,
  list-w-params_list ML2P ML2,
  std.forall ML2 (m2\ std.exists ML1 (m1\ m1 = m2)).

% TODO: maybe the right API is to have this
% pred factory-provides i:factoryname, i:list-w-params mixiname.
% one can use w-params.then now!
% [factory-provides F ML] computes the mixins ML generated by F
pred factory-provides i:factoryname, o:list-w-params mixinname.
factory-provides FactoryAlias MLwP :- std.do! [
  factory-alias->gref FactoryAlias Factory,
  factory-requires Factory RMLwP,
  w-params.map RMLwP (factory-provides.base Factory) MLwP
].

pred factory-provides.base i:factoryname, i:list term, i: term,
  i:list (w-args mixinname), o:list (w-args mixinname).
factory-provides.base Factory Params T _RMLwP MLwP :- std.do! [
  std.findall (from Factory T_ F_) All,
  std.map All from_mixin ML,
  std.map All from_builder BL,
  std.map2 BL ML (factory-provides.one Params T) MLwP,
].

pred factory-provides.one i:list term, i:term, i:term, i:mixinname, o:w-args mixinname.
factory-provides.one Params T B M (triple M PL T) :- std.do! [
  std.assert-ok! (coq.typecheck B Ty) "Builder illtyped",
  subst-prod [T] {subst-prod Params Ty} TyParams,
  std.assert! (extract-conclusion-params TyParams PL) "The conclusion of a builder is a mixin whose parameters depend on other mixins",
].

pred extract-conclusion-params i:term, o:list term.
extract-conclusion-params (prod _ S T) R :- !,
  @pi-decl _ S x\ extract-conclusion-params (T x) R.
extract-conclusion-params (app [global GR|Args]) R :- !,
  factory-alias->gref GR Factory,
  factory-nparams Factory NP,
  std.take NP Args R.
extract-conclusion-params T R :- whd1 T T1, !, extract-conclusion-params T1 R.


% [factories-provide FL ML] computes the mixins ML generated by all F in FL
%
%  cons tp p\ nil t\ [pr f1 [p,t]]
%    f1 p t = m1 t, m2 p t
%  cons tp p\ nil t\ [pr m1 [t], pr m2 [p,t]]
pred factories-provide i:list-w-params factoryname, o:list-w-params mixinname.
factories-provide FLwP MLwP :-
  list-w-params.flatten-map FLwP factory-provides UnsortedMLwP,
  w-params.map UnsortedMLwP (p\t\ toposort-mixins) MLwP.

% Mixins can be topologically sorted according to their dependencies
pred toposort-mixins.mk-mixin-edge i:prop, o:list (pair mixinname mixinname).
toposort-mixins.mk-mixin-edge (factory-requires M Deps) L :-
  std.map {list-w-params_list Deps} (d\r\ r = pr d M) L.

pred toposort-mixins i:list (w-args mixinname), o:list (w-args mixinname).
toposort-mixins In Out :- std.do! [
  std.findall (factory-requires M_ Deps_) AllMixins,
  std.flatten {std.map AllMixins toposort-mixins.mk-mixin-edge} ES,
  toposort-proj triple_1 ES In Out,
].

pred toposort-proj i:(A -> B -> prop), i:list (pair B B), i:list A, o:list A.
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 {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
].

% Classes can be topologically sorted according to the subclass relation
pred toposort-classes.mk-class-edge i:prop, o:pair class class.
toposort-classes.mk-class-edge (sub-class C1 C2) (pr C2 C1).
pred toposort-classes i:list class, o:list class.
toposort-classes In Out :- std.do! [
  std.findall (sub-class C1_ C2_) SubClasses,
  std.map SubClasses toposort-classes.mk-class-edge ES,
  toposort ES In Out,
].

pred findall-classes o:list class.
findall-classes CLSorted :- std.do! [
  std.findall (class-def C_) All,
  std.map All (x\r\ x = class-def r) CL,
  toposort-classes CL CLSorted
].

pred findall-builders o:list builder.
findall-builders LFIL :-
  std.map {std.findall (builder-decl B_)} extract-builder LFILunsorted,
  bubblesort LFILunsorted leq-builder LFIL.

% [distinct-pairs-below C AllSuper C1 C2] finds C1 and C2 in
% AllSuper (all super classes of C) such that C1 != C2
% and for which there is no join C3.
% If there exists a join C3 of C1 and C2 then C is a subclass
% of C3 (otherwise C should have been declared before C3)
%
%        / --- /-- C1
%    C -- no C3    !=
%        \ --- \-- C2
%
% [findall-newjoins C AllSuper] finds all C1 and C2 such that C is a (new) join for
% them
pred distinct-pairs-below i:class, i:list class, o:class, o:class.
distinct-pairs-below CurrentClass AllSuper C1 C2 :-
  std.mem AllSuper C1, std.mem AllSuper C2,
  % no cut until here, since we don't know which C1 and C2 to pick
  std.do! [
    cmp_term C1 C2 lt,
    C1 = class C1n _ _,
    C2 = class C2n _ _ ,
    not(sub-class? C1 C2),
    not(sub-class? C2 C1),
    if (join C1n C2n C3n)
       (assert-building-bottom-up CurrentClass C3n, fail) % a join, not a valid pair
       true, % no join, valid pair
  ].

pred assert-building-bottom-up i:class, i:classname.
assert-building-bottom-up CurrentClass C3n :-
  class-def (class C3n X Y),
  if (not (sub-class? CurrentClass (class C3n X Y)))
     (coq.error "You must declare" CurrentClass "before" C3n)
     true.

pred distinct-pairs_pair i:prop, o:pair class class.
distinct-pairs_pair (distinct-pairs-below _ _ X Y) (pr X Y).

pred findall-newjoins i:class, i:list class, o:list (pair class class).
findall-newjoins CurrentClass AllSuper TodoJoins :-
  std.findall (distinct-pairs-below CurrentClass AllSuper C1_ C2_) JoinOf,
  std.map JoinOf distinct-pairs_pair TodoJoins.

%%%%% Coq Database %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% [get-structure-coercion S1 S2 F] finds the coecion F from the structure S1 to S2
pred get-structure-coercion i:structure, i:structure, o:term.
get-structure-coercion (global S) (global T) (global F) :-
  coq.coercion.db-for (grefclass S) (grefclass T) L,
  if (L = [pr F 0]) true (coq.error "No one step coercion from" S "to" T).

pred get-structure-sort-projection i:structure, o:term.
get-structure-sort-projection (global (indt S)) (global (const P)) :-
  coq.CS.canonical-projections S L,
  if (L = [some P, _]) true (coq.error "No canonical sort projection for" S).

pred get-structure-class-projection i:structure, o:term.
get-structure-class-projection (global (indt S)) (global (const P)) :-
  coq.CS.canonical-projections S L,
  if (L = [_, some P]) true (coq.error "No canonical class projection for" S).

pred get-constructor i:term, o:gref.
get-constructor (global (indt R) as S) (indc K) :- !,
 if (coq.env.indt R _ _ _ _ [K] _) true (coq.error "Not a record" S).

pred safe-head i:term, o:term.
safe-head (prod N T Body) Hd :-
  @pi-decl N T x\
    safe-head (Body x) (Hd' x),
    std.assert! (Hd' x = Hd) "safe-head: the head symbol is a bound variable".
safe-head T Hd :- whd1 T T', safe-head T' Hd.
safe-head T Hd :- safe-dest-app T Hd _.

%% finding for locally defined structures
pred get-cs-structure i:cs-instance, o:term.
get-cs-structure (cs-instance _ _ (global Inst)) Struct :- std.do! [
  coq.env.typeof Inst InstTy,
  safe-head InstTy Struct
].

pred has-cs-instance i:gref, i:cs-instance.
has-cs-instance GTy (cs-instance _ (cs-gref GTy) _).

pred get-local-structures i:term, o:list term.
get-local-structures TyTrm StructL :- std.do! [
  std.filter {coq.CS.db} (has-cs-instance {term->gref TyTrm}) DBGTyL,
  std.map DBGTyL get-cs-structure RecL,
  std.filter RecL is-structure StructL
].

pred local-cs? i:term, i:term.
local-cs? TyTerm Struct :-
  get-local-structures TyTerm StructL,
  std.mem! StructL Struct.

pred get-canonical-mixins-of i:term, i:structure, o:list prop.
get-canonical-mixins-of T S MSL :- std.do! [
  get-structure-sort-projection S Sort,
  std.assert-ok! (coq.unify-eq T (app [Sort, ST])) "HB: get-canonical-mixins-of: T = sort ST",
  % Hum, this unification problem is not super trivial. TODO replace by something simpler
  get-constructor S KS,
  std.assert-ok! (coq.unify-eq ST (app [global KS, _, C])) "HB: get-canonical-mixins-of: ST = _ _ C",
  C = app [_, _ | MIL],
  std.map MIL (mixin-srcs T) MSLL,
  std.flatten MSLL MSL
].

pred under-canonical-mixins-of.do! i:term, i:list prop.
under-canonical-mixins-of.do! T P :-
  get-local-structures T CS,
  std.map CS (get-canonical-mixins-of T) MSLL,
  std.flatten MSLL MSL,
  MSL => std.do! P.

%%%%% mterm %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% mterm is always of the form [mterm P T ML F], which is the data of
% parameters PL a type T, and a list of mixins ML and a term F
% where F should applied to PL, T and instances of the mixins in ML
kind mterm type.
type mterm list term -> term -> list mixinname -> term -> mterm.

% Notations /à la/ *pack* are always of the shape
% [Notation N x_0 .. x_n := C x_0 .. _ _ id .. x_i .. _ id _ _ id]
% with a variable number of [_] between each [id], and where
% - [x_i] is given by the user
% - [_]   correspond to arguments that are left implicit,
% - [id]  trigger unification as described in
% /Canonical Structures for the working Coq user/ by Mahboubi and Tassi
%
% phant-arg encode these three kind of arguments
% - [x_i] is encoded using [real-arg x_i]
% - [_]              using [implicit-arg]
% - [id]             using [unify-arg]
kind phant-arg type.
type real-arg name -> phant-arg.
type implicit-arg phant-arg.
type unify-arg phant-arg.

% phant-term is a pair of a list of argument kinds together with a term
kind phant-term type.
type phant-term list phant-arg -> term -> phant-term.

pred phant-fun i:phant-arg, i:term, i:(term -> phant-term), o:phant-term.
phant-fun Arg Ty PhF (phant-term [Arg|ArgL] (fun N Ty F)) :-
  if (Arg = real-arg N) true (N = `_`),
  @pi-decl N Ty x\ PhF x = phant-term ArgL (F x).

pred phant-fun-real i:name, i:term, i:(term -> phant-term), o:phant-term.
phant-fun-real N T F Res :- !, phant-fun (real-arg N) T F Res.

% [phant-fun-unify N X1 X2 PF PUF] states that PUF is a phant-term that
% is starts with unifing X1 and X2 and then outputs PF.
% N is ignored
pred phant-fun-unify i:term, i:term, i:term, i:phant-term, o:phant-term.
phant-fun-unify Msg X1 X2 (phant-term AL F) (phant-term [unify-arg|AL] UF) :-
  std.assert-ok! (coq.typecheck X1 T1) "mk-phant-abbrev: X1 illtyped",
  std.assert-ok! (coq.typecheck X2 T2) "mk-phant-abbrev: X2 illtyped",
  UF = {{fun unif_arbitrary : lib:hb.unify lp:T1 lp:T2 lp:X1 lp:X2 lp:Msg => lp:F}}.

% [phant-fun-implicit N Ty PF PUF] states that PUF is a phant-term
% which quantifies [PF x] over [x : Ty] (with name N)
pred phant-fun-implicit i:name, i:term, i:(term -> phant-term), o:phant-term.
phant-fun-implicit N Ty PF (phant-term [implicit-arg|AL] (fun N Ty F)) :- !,
  @pi-decl N Ty t\ PF t = phant-term AL (F t).

pred phant-fun-unify-mixin i:term, i:name, i:term, i:(term -> phant-term), o:phant-term.
phant-fun-unify-mixin T N Ty PF Out :- !, std.do! [
  safe-dest-app Ty (global M) _,
  mixin-src T M Mstr,
  (@pi-decl `m` Ty m\ phant-fun-unify {{lib:hb.nomsg}} m Mstr (PF m) (PFM m)),
  phant-fun-implicit N Ty PFM Out
].

% [phant-fun-struct T SI PF PSF] states that PSF is a phant-term
% which postulate a structure [s : SI] such that [T = sort s]
% and then outputs [PF s]
pred phant-fun-struct i:term, i:name, i:term, i:(term -> phant-term), o:phant-term.
phant-fun-struct T Name SI PF Out :- std.do! [
  get-structure-sort-projection SI Sort,
  % Msg = {{lib:hb.nomsg}},
  Msg = {{lib:hb.some (lib:hb.pair "is not canonically a"%string lp:SI)}},
  (@pi-decl Name SI s\ phant-fun-unify Msg T {mk-app Sort [s]} (PF s) (UnifSI s)),
  phant-fun-implicit Name SI UnifSI Out
].

% [builder->term Params T Src Tgt MF] provides a term which is
% a function to transform Src into Tgt under the right mixin-src.
pred builder->term i:list term, i:term, i:factoryname, i:mixinname, o:term.
builder->term Ps T Src Tgt FT :- !, std.do! [
  from Src Tgt F,
  factory-requires Src MLwP,
  list-w-params_list MLwP ML,
  mterm->term (mterm Ps T ML F) FT].

% [instantiate-mixin T F M_i TFX] where mixin-for T M_i X_i states that
% if    F  ~  fun xs (m_0 : M_0 T) .. (m_n : M_n T ..) ys
%            => F xs m_0 .. m_{i-1} m_i m_{i+1} .. m_n ys
% then TFX := fun xs m_0 .. m_{i-1}     m_{i+1} .. m_n ys
%            => F xs m_0 .. m_{i-1} X_i m_{i+1} .. m_n ys
% thus instanciating an abstraction on mixin M_i with X_i
pred instantiate-mixin i:term, i:mixinname, i:term, o:term.
instantiate-mixin T M (fun _ Tm F) R :-
  safe-dest-app Tm (global TmGR) _,
  factory-alias->gref TmGR M, !,
  mixin-for T M X, !,
  R = F X.
instantiate-mixin T M (fun N Ty F) (fun N Ty FX) :- !,
  pi m\ instantiate-mixin T M (F m) (FX m).
instantiate-mixin _ _ F F.

% [mterm->term MF TFX] assumes that MF is a mterm
% (mterm ML F) and perform the substitution as above
% for every mixin-for entry out of the list ML = [M_0, .., M_n].
pred mterm->term i:mterm, o:term.
mterm->term (mterm Ps T ML F) SFX :- std.do! [
  std.assert-ok! (coq.typecheck F Ty) "mterm->term: F illtyped",
  mk-eta (-1) Ty F EtaF,
  subst-fun {std.append Ps [T]} EtaF FT,
  std.fold ML FT (instantiate-mixin T) SFX
].

% [mgref->term Params T GR X] computes the dependencies of GR in mixins,
% (through factory-requires if it exist, otherwise gr-deps)
% and instanciates all of them through mixin-src, and fails if it cannot.
pred mgref->term i:list term, i:term, i:gref, o:term.
mgref->term Ps T GR X :- factory-requires GR MLwP, !, std.do! [
  list-w-params_list MLwP ML,
  mterm->term (mterm Ps T ML (global GR)) X
].
mgref->term Ps T GR X :- !, std.do! [
  std.assert! (gr-deps GR MLwP) "BUG: gr-deps should never fail",
  list-w-params_list MLwP ML,
  mterm->term (mterm Ps T ML (global GR)) X
].

% [mixin-srcs T X MSL] states that MSL is a list of [mixin-src T m X]
% where m ranges all the mixins that the factory Src can provide,
% where Src is the type of X.
pred mixin-srcs i:term, i:term, o:list prop.
mixin-srcs T X MSL :- std.do! [
  std.assert-ok! (coq.typecheck X XTy) "mixin-src: X illtyped",
  if (not (safe-dest-app XTy (global _) _))
     (coq.error "Term:\n" {coq.term->string X}
                "\nhas type:\n" {coq.term->string XTy}
                "\nwhich is not a record")
     true,
  term->gref XTy Src,
  factory-provides Src MLwP,
  list-w-params_list MLwP ML,
  % TODO: skip mixins for which there is already a source.
  std.map ML (m\r\ r = mixin-src T m X) MSL
].

pred under-mixin-src-from-factory.then i:term, i:term, i:(term -> prop), o:term.
under-mixin-src-from-factory.then TheType TheFactory P X :- std.do![
  mixin-srcs TheType TheFactory ML,
  ML => P X
].

pred under-mixin-src-from-factory.do! i:term, i:term, i:list prop.
under-mixin-src-from-factory.do! TheType TheFactory LP :-
  under.do! (under-mixin-src-from-factory.then TheType TheFactory) LP.

pred under-mixin-src-from-factories.then i:term, i:list term, i:(term -> prop), o:term.
under-mixin-src-from-factories.then TheType Factories P X :-
  std.map Factories (mixin-srcs TheType) MLL,
  std.flatten MLL ML,
  ML => P X.

pred under-mixin-src-from-factories.do! i:term, i:list term, i:list prop.
under-mixin-src-from-factories.do! TheType Factories LP :-
  under.do! (under-mixin-src-from-factories.then TheType Factories) LP.

% [mixin-for T M X] states that X has type [M T ...]
% it is reconstructed from two databases [mixin-src] and [from]
pred mixin-for o:term, o:mixinname, o:term.
mixin-for T M MI :- mixin-src T M Tm, !, std.do! [
  std.assert-ok! (coq.typecheck Tm Ty) "mixin-for: Tm illtyped",

  factory? Ty (triple Factory Params _),

  if (M = Factory) (MI = Tm) (
      builder->term Params T Factory M F,
      subst-fun [Tm] F MI
  )
].

% ----------- Finding and instantiating mixin arguments -------------------

% [ty-deps Ty ML] states that ML is the list of
% mixins which the type Ty rely on, i.e.
% Ty = forall p_1 ... p_n (T : Type) (m_0 : M_0 T) ... (m_n : M_n T ..), (zero : T), ..... axioms_ T
% ML = [M_0, .., M_n]
% pred ty-deps i:term, o:list-w-params mixinname.
% ty-deps (prod N S R) ML' :- !,
%   @pi-decl N S x\
%     ty-deps (R x) ML,
%     safe-dest-app S HD _,
%     if (HD = global GR, factory-alias->gref GR F, from  _ F _, !)
%       (ML' = [F|ML]) (ML' = ML).
% ty-deps Ty ML :- whd1 Ty Ty1, !, ty-deps Ty1 ML.
% ty-deps _Ty [].

pred factory? i:term, o:w-args factoryname.
factory? S (triple F Params T) :-
  safe-dest-app S (global GR) Args, factory-alias->gref GR F, factory-nparams F NP, !,
  std.split-at NP Args Params [T|_].

pred prod-src-is-factory i:term.
prod-src-is-factory (prod _ S _) :- factory? S _.
prod-src-is-factory Ty :- whd1 Ty Ty1, !, prod-src-is-factory Ty1.

pred ty-deps i:term, o:list-w-params mixinname.
ty-deps Ty ML :- ty-deps.aux Ty ML, !.
ty-deps (prod N T _) (w-params.nil N T _\[]) :- T = {{Type}}, !.
ty-deps T _ :- % TODO: forall p1 ... pn (T : indexed Type) with indexed being the id function
  coq.error "ty-deps: BUG: could not get the parameters and the dependencies of"
    {coq.term->string T}.
pred ty-deps.aux i:term, o:list-w-params mixinname.
ty-deps.aux (prod N S R) ML :- !,
  @pi-decl N S x\
    if (prod-src-is-factory (R x); S = {{ lib:hb.indexed Type }})
      (ML = w-params.nil  N S MLP, ty-deps.factories (R x) (MLP x))
      (ML = w-params.cons N S ML1, ty-deps.aux (R x) (ML1 x)).
ty-deps.aux Ty ML :- whd1 Ty Ty1, !, ty-deps.aux Ty1 ML.

pred ty-deps.factories i:term, o:list (w-args factoryname).
ty-deps.factories (prod N S R) FS :-
  @pi-decl N S x\
    if (factory? S FwP) (FS = [FwP|FS1]) (FS = FS1),
    ty-deps.factories (R x) FS1.
ty-deps.factories Ty FS :- whd1 Ty Ty1, !, ty-deps.factories Ty1 FS.
ty-deps.factories _ [].

% [term-deps T ML] states that ML is the list of
% mixins which the term T rely on, i.e. T has type
% forall (m_0 : M_0 T) ... (m_n : M_n T ..), _ and ML = [M_0, .., M_n]
pred term-deps i:term, o:list-w-params mixinname.
term-deps T ML :-
  std.assert-ok! (coq.typecheck T Ty) "term-deps: T illtyped",
  ty-deps Ty ML.

% shorthand for gref.
pred gr-deps i:gref, o:list-w-params mixinname.
gr-deps GR ML :- term-deps (global GR) ML.

% [find-max-classes Mixins Classes] states that Classes is a list of classes
%   which contain all the mixins in Mixins.
% Although it is not strictly necessary, but desirable for debugging,
% we use a heuristic that tries to minimize the number
% of classes by assuming Mixins are reversed topologically sorted.
% Note: works with flat mixins, no params
pred find-max-classes i:list mixinname, o:list classname.
find-max-classes [] [].
find-max-classes [M|Mixins] [C|Classes] :-
  mixin-first-class M C,
  std.do! [
    class-def (class C _ MLwP),
    list-w-params_list MLwP ML,
    std.filter Mixins (x\ not (std.mem! ML x)) Mixins',
    find-max-classes Mixins' Classes
  ].
find-max-classes [M|_] _ :- coq.error "cannot find a class containing mixin" M.

pred under-mixins.then i:list (w-args mixinname),
    i:(name -> term -> (term -> A) -> A -> prop),
    i:(A -> prop), o:A.
under-mixins.then [] _ Pred Body :- !, Pred Body.
under-mixins.then [triple M Args T|ML] Mixin Pred Out :- std.do! [
  mgref->term Args T M MTy,
  (@pi-decl `m` MTy m\ mixin-src T M m =>
    under-mixins.then ML Mixin Pred (Body m)),
  Mixin `m` MTy Body Out
].

% [mk-mixin-fun.then MLwP Pred F] states that F has shape
%   fun p_1 .. p_k T,
%      (m_0 : M_0 ..p.. T) .. (m_n : M_n ..p.. T m_i0 .. m_ik) =>
%      Body m_0 .. m_n
% where  MLwP contains M_0, .., M_n (under p_1 .. p_k)
%   and  Body is such that [..,mixin-src T M_i m_i,..] => Pred Body
%   and  ..p.. is a list of terms built using p_1 .. p_k and T
pred mk-mixin-fun.then i:list-w-params mixinname, i:(list term -> term -> term -> prop), o:term.
mk-mixin-fun.then L P Out :- !,
  w-params.then L mk-fun mk-fun
    (p\ t\ ml\ under-mixins.then ml mk-fun (P p t)) Out.

% A *pack* notation can be easiliy produced from a phant-term using
% [mk-phant-abbrev N PT C], which states that C is a new constant
% which name is phant_N, and which produces a simple notation
% with name N using the data of the phant-term PT to reconstruct a notation
% [Notation N x0 .. xn := C x0 _ _ id .. xi .. _ id _ _ id]
% as described above.
pred mk-phant-abbrev.term i:int, i:term, i:list phant-arg, o:int, o:term.
mk-phant-abbrev.term K F [] K F.
mk-phant-abbrev.term K F [real-arg N|AL] K'' (fun N _ AbbrevFx) :- !,
  pi x\ mk-phant-abbrev.term K {mk-app F [x]} AL K' (AbbrevFx x),
  K'' is K' + 1.
mk-phant-abbrev.term K F [implicit-arg|AL] K' FAbbrev :- !,
  mk-phant-abbrev.term K {mk-app F [_]} AL K' FAbbrev.
mk-phant-abbrev.term K F [unify-arg|AL] K' FAbbrev :- !,
  mk-phant-abbrev.term K {mk-app F [{{lib:@hb.id _ _}}]} AL K' FAbbrev.

pred mk-phant-abbrev i:string, i:phant-term, o:constant, o:abbreviation.
mk-phant-abbrev N (phant-term AL T) C Abbrev :- std.do! [
  NC is "phant_" ^ N,
  std.assert-ok! (coq.typecheck T TTy) "mk-phant-abbrev: T illtyped",
  coq.env.add-const NC T TTy ff ff C,
  mk-phant-abbrev.term 0 (global (const C)) AL NParams AbbrevT,
  add-abbrev N NParams AbbrevT tt tt Abbrev,
].

% [acc-phant-abbrev Str GR PhGR Abbrev] makes a phantom abbreviation for F
pred acc-phant-abbrev i:string, i:gref, o:gref, o:abbreviation.
acc-phant-abbrev Str GR (const PhC) Abbrev :- !, std.do! [
  mk-phant-term (global GR) PhGR,
  mk-phant-abbrev Str PhGR PhC Abbrev
].

% [mk-phant-term F PF] states that
% if F = fun p1 .. p_k T m_0 .. m_n => _
% then PF = phant-term
%   [real-arg p_1, ... real-arg p_k, real-arg T, implicit-arg, .., implicit-arg,
%       implicit-arg, .., implicit-arg,
%         implicit-arg, unify-arg,
%         implicit-arg, unify-arg,
%         implicit-arg, .., implicit-arg, unify-arg,
%         unify-arg, ..., unify-arg,
%       ...,
%       implicit-arg, .., implicit-arg,
%         implicit-arg, unify-arg,
%         implicit-arg, unify-arg,
%         implicit-arg, .., implicit-arg, unify-arg,
%         unify-arg, ..., unify-arg]
%   {{fun p_1 ... p_k T m_0 .. m_n =>
%       fun q_1 .. q_l =>
%         [find s_0 | T ~ s_0]
%         [find c_0 | s_0 ~ SK q_1 .. q_l T c_0]
%         [find m'_{i_0_0}, .., m'_{i_0_n0} | c_0 ~ CK m'_{i_0_0} .. m'_{i_0_n0}]
%         fun of hb.unify m_{i_0_0} m'_{i_0_0} & ... & hb.unify m_{i_0_n0} m'_{i_0_n0} =>
%       ...
%       fun q'_1 .. q'_l' =>
%         [find s_k | T ~ s_k]
%         [find c_k | s_k ~ SK q'_1 .. q'_l' T c_k]
%         [find m'_{i_k_0}, .., m'_{i_k_nk} | c_0 ~ CK m'_{i_k_0} .. m'_{i_k_nk}]
%         fun of hb.unify m_{i_0_0} m'_{i_0_0} & ... & hb.unify m_{i_k_nk} m'_{i_k_nk} =>
%       F p_1 ... p_k T m_i0_j0 .. m_il_jl}}
pred mk-phant-term.mixins i:term, i:classname, i:phant-term,
  i:list term, i:name, i:term, i:(term -> list (w-args mixinname)), o:phant-term.
mk-phant-term.mixins T CN PF Params N Ty MLwA Out :- std.do! [
  class-def (class CN SI _),
  NoMsg = {{lib:hb.nomsg}},
  (@pi-decl N Ty t\ sigma SK KC ML\ std.do! [
    std.map (MLwA t) triple_1 ML,
    std.append Params [T] ParamsT,
    SKPT = app [global {get-constructor SI} | ParamsT],
    ClassTy = app [global CN | ParamsT],
    (@pi-decl `s` SI s\ @pi-decl `c` ClassTy c\ sigma PF2\ std.do![
       under-mixins.then (MLwA t) (phant-fun-unify-mixin T)
          (x\ sigma KC KCM\ std.do![
            get-constructor (global CN) KC,
            mgref->term Params t KC KCM,
            phant-fun-unify NoMsg KCM c PF x
          ]) PF2,
       phant-fun-unify NoMsg s {mk-app SKPT [c]} PF2 (PFU t s c)])
  ]),
  Out = {phant-fun-struct T `s` SI s\
          {phant-fun-implicit `c` ClassTy (PFU T s)}}
].

pred mk-phant-term.class i:term, i:classname, i:phant-term, o:phant-term.
mk-phant-term.class T CN PF CPF :- !, std.do! [
  class-def (class CN _ CMLwP),
  w-params.fold CMLwP phant-fun-implicit (mk-phant-term.mixins T CN PF) CPF
].

pred mk-phant-term.classes i:term, i:list classname, i:list term, i:term,
                      i:list (w-args mixinname), o:phant-term.
mk-phant-term.classes EtaF CNF PL T MLwA PhF :- !, std.do! [
  std.map MLwA triple_1 ML,
  under-mixins.then MLwA phant-fun-implicit (out\ sigma FPLTM\ std.do! [
    mterm->term (mterm PL T ML EtaF) FPLTM,
    std.fold CNF (phant-term [] FPLTM) (mk-phant-term.class T) out]) PhF
].

pred mk-phant-term i:term, o:phant-term.
mk-phant-term F PhBody:- !, std.do! [
  std.assert-ok! (coq.typecheck F FTy) "mk-phant-term: F illtyped",
  ty-deps FTy MLwP,
  mk-eta (-1) FTy F EtaF,
%  toposort-mixins ML MLSorted,
  MLwP = MLwPSorted, % Assumes we give them already sorted in dep order.
  std.rev {list-w-params_list MLwPSorted} MLSortedRev,
  find-max-classes MLSortedRev CNL,
  w-params.then MLwP phant-fun-real phant-fun-real
    (mk-phant-term.classes EtaF CNL) PhBody,
].

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                              Synthesis                                     %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

pred params->holes i:list-w-params A, o:list term.
params->holes (w-params.nil _ _ _) [].
params->holes (w-params.cons _ _ F) [_|PS] :- pi x\ params->holes (F x) PS.

% Given a type T, a list of class definition in topological order (from least dep to most)
% it consumes the list all the classes for which all the dependencies
% (mixins) were postulated so far (skips the rest) and declares a local
% constant inhabiting the corresponding structure and declares it canonical.
pred declare-instances i:term, i:list class.
declare-instances T [class Class Struct MLwP|Rest] :-
  params->holes MLwP Params,
  get-constructor (global Class) KC,
  mgref->term Params T KC KCApp, % we can build it
  not (local-cs? T Struct), % not already built
  !,
  term->gref T TGR,
  coq.gref->id TGR TID,
  Name is TID ^ "_is_a_" ^ {term->modname Struct},

  if-verbose (coq.say "HB: declare canonical instance" Name),

  get-constructor Struct KS,
  mk-app (global KS) {std.append Params [T, KCApp]} S,
  std.assert-ok! (coq.typecheck S STy) "declare-instances: S illtyped",

  coq.env.add-const Name S STy ff ff CS, % Bug coq/coq#11155, could be a Let
  coq.CS.declare-instance (const CS), % Bug coq/coq#11155, should be local
  declare-instances T Rest.
declare-instances T [_|Rest] :- declare-instances T Rest.
declare-instances _ [].

kind factory-name-or-alias type.
type factory-by-classname gref -> factory-name-or-alias.
type factory-by-phantabbrev abbreviation -> factory-name-or-alias.

pred declare-factory-abbrev i:id, i:factory-name-or-alias.
declare-factory-abbrev Name (factory-by-classname GR) :-
  % looks fishy (the parameters are not taken into account)
  add-abbrev Name 1 (fun _ _ t\ app[global GR,t]) tt tt _.
declare-factory-abbrev Name (factory-by-phantabbrev Abbr) :-
  coq.notation.abbreviation-body Abbr Nargs AbbrTrm,
  add-abbrev Name Nargs AbbrTrm tt tt _.

% [main-factory-requires Str GR FL CL SN]
% computes the list of mixins ML provided by FL,
% creates a clause in CL stating that GR requires ML (factory-requires ..), and
% creates an abbreviation for GR names Str and creates a phant-abbrev clause in CL.
% SN is the short name for the factory (either an alias of the class record)
pred main-factory-requires i:string, i:gref, i:list-w-params factoryname, o:list prop, o:factory-name-or-alias.
main-factory-requires Str GR GRFS [FactoryRequires|Aliases] SN :- !, std.do! [
  factories-provide GRFS ML,
  FactoryRequires = factory-requires GR ML,
  if (factory-alias->gref GR _)
     (Aliases = [],
      SN = factory-by-classname GR)
     (acc-phant-abbrev Str GR PhGR Abbrv,
      Aliases = [phant-abbrev GR PhGR Abbrv],
      SN = factory-by-phantabbrev Abbrv),
].

% [main-mixin-requires S GR FL CL SN]
% calls main-factory-requires and appends the identity builders for the mixin
pred main-mixin-requires i:string, i:gref, i:list-w-params factoryname, o:list prop, o:factory-name-or-alias.
main-mixin-requires Str GR GRFS [From|PO] SN :- !, std.do! [
  main-factory-requires Str GR GRFS PO SN,
  % register factory
  PO => std.do! [
    mk-mixin-fun.then {factory-requires GR}
      (params\ t\ body\ sigma MTy\
        mgref->term params t GR MTy,
        body = fun `x` MTy x\x)
      IDBody
  ],
  std.assert-ok! (coq.typecheck IDBody _) "identity builder illtyped",
  From = from GR GR IDBody,
].

% [postulate-arity A Acc T TS] postulates section variables
% corresponding to parameters in arity A. TS is T applied
% to all section variables (and hd-beta reduced). Acc should
% be [] at call site.
pred postulate-arity i:arity, i:list term, i:term, o:term.
postulate-arity (parameter ID _ S A) Acc T T1 :-
  coq.env.add-const ID _ S tt tt C,
  Var = global (const C),
  postulate-arity (A Var) [Var|Acc] T T1.
postulate-arity (arity _) ArgsRev X T :-
  hd-beta X {std.rev ArgsRev} X1 Stack1,
  unwind X1 Stack1 T.

% Given a type T, a fresh number N, and a mixin M it postulates
% a variable "mN" inhabiting M applied to T and
% all its dependencies, previously postulated and associated
% to the corresponding mixin using mixin-for
pred postulate-mixin i:w-args mixinname, i:list prop, o:list prop.
postulate-mixin (triple M Ps T) MSL [mixin-src T M (global (const C))|MSL] :- MSL => std.do! [
  Name is "mixin_" ^ {gref->modname M},

  if-verbose (coq.say "HB: postulate" Name "on" {coq.term->string T}),

  mgref->term Ps T M Ty,
  std.assert-ok! (coq.typecheck Ty _) "postulate-mixin: Ty illtyped",
  coq.env.add-const Name _ Ty tt tt C % no body, local -> a variable
].

% Postulates a context with all the mixins provided by the factories
pred main-declare-context i:term, i:list term, i:list-w-params factoryname, o:list prop.
main-declare-context TheType TheParams GRFSwP MSL :-  std.do! [
  factories-provide GRFSwP MLwP,
  apply-w-params MLwP TheParams TheType MLwAllArgs,
  std.fold MLwAllArgs [] postulate-mixin MSL,
  MSL => declare-instances TheType {findall-classes},
  std.forall MSL (ms\ acc current (clause _ _ ms)),
].

% [factory-comp SrcFactory MB MiddleFactory TgtMixin B1] synthesizes
%   B1 = MB o B
% where MB is the builder from MiddleFactory to TgtMixin and
% B is a builder from SrcFactory to MiddleFactory
pred factory-comp i:list mixinname, i:factoryname, i:term, i:factoryname,
  i:mixinname, i:list term, i:term, o:term.
factory-comp ML SrcFactory B MiddleFactory TgtMixin Params Type Comp :-
  mgref->term Params Type SrcFactory Src,
  MB = mterm Params Type ML B,
  Comp = {{
    fun src : lp:Src => lp:{{
      {under-mixin-src-from-factory.then Type {{src}}
        (factory-comp-body {{src}} MB MiddleFactory TgtMixin)} }}
  }}.

pred factory-comp-body i:term, i:mterm, i:factoryname, i:mixinname, o:term.
factory-comp-body TheFactory (mterm TheParams TheType _ _ as MB) MiddleFactory TgtMixin Comp :- std.do! [
  mterm->term MB MB1,
  subst-fun-opt TheFactory MB1 MB2,
  builder->term TheParams TheType MiddleFactory TgtMixin B2,
  subst-fun [MB2] B2 Comp
].

% [declare-builder Src SrcRequires F Fty Mid Tgt FromI FromO]
% declares a builder by composing F and Mid.
pred declare-builder
  i:gref, i:list-w-params mixinname, i:term, i:term, i:gref, i:gref, i:list prop, o:list prop.
declare-builder SrcFactory SrcFactoryRequires F FTy MiddleFactory TgtMixin FromI [NewFrom|FromI] :- !, FromI => std.do! [
  std.assert! (FTy = prod _ _ _) "declare-builder: B is not a function",

  list-w-params_list SrcFactoryRequires ML, % args of F we can fulfill with the context

  GoF = {mk-mixin-fun.then SrcFactoryRequires
          (factory-comp ML SrcFactory F MiddleFactory TgtMixin)},

  std.assert-ok! (coq.typecheck GoF _GoFTy) "declare-builder: GoF illtyped",
  Name is {gref->modname SrcFactory} ^ "_to_" ^ {gref->modname TgtMixin} ^ {term_to_string {new_int}},
  coq.env.add-const Name GoF _GoFTy ff ff GoFC,
  NewFrom = from SrcFactory TgtMixin (global (const GoFC)),
].

% [main-declare-builder (builder _ F B) From MoreFrom] Given B of type FB, it
% generates all the builders for mixins in FB from F via components of B.
% From holds the (from F Mi Bi) predicates during folding.
pred main-declare-builder i:builder, i:list prop, o:list prop.
main-declare-builder (builder _ SrcFactory B) FromClauses MoreFromClauses :- !, std.do! [
  FromClauses => std.do! [
    std.assert-ok! (coq.typecheck B BTy) "main-declare-builder: B illtyped",
    factory-alias->gref {target-gref BTy} MiddleFactory,
    factory-requires SrcFactory SrcFactoryRequireswP,
    list-w-params_list SrcFactoryRequireswP SrcFactoryRequires,

    factory-provides MiddleFactory AllTgtMixinswP,
    list-w-params_list AllTgtMixinswP AllTgtMixins,

    std.filter AllTgtMixins (t\ not (std.mem! SrcFactoryRequires t)) TgtMixins,
  ],
  if-verbose (coq.say "HB: declare builders from" {nice-gref->string SrcFactory}
                      "to" {std.map TgtMixins nice-gref->string}),
  std.fold TgtMixins FromClauses (declare-builder SrcFactory SrcFactoryRequireswP B BTy MiddleFactory) MoreFromClauses,
].

% [export Module] exports a Module now adds it to the collection of
% modules to export in the end
pred to-export o:modpath.
pred export i:modpath.
export Module :- !,
  coq.env.export-module Module,
  acc current (clause _ _ (to-export Module)).

pred mk-mixin-fun i:list-w-params mixinname, i:term, o:term.
mk-mixin-fun ML X MLX :- mk-mixin-fun.then ML (p\ t\ body\ body = X) MLX.

% 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
pred clean-op-ty i:list prop, i:term, i:term, o:term.
clean-op-ty [] _ T1 T2 :- copy T1 T2.
clean-op-ty [exported-op _ Po C|Ops] S T1 T2 :-
  gr-deps (const Po) MLwP,
  w-params.nparams MLwP NParams,
  std.length {list-w-params_list MLwP} NMixins,

  (pi L L1 Params Rest PoArgs\
    copy (app [global (const Po)| L]) (app [global (const C) | L1]) :-
      std.split-at NParams L Params [_|Rest],
      std.drop NMixins Rest PoArgs,
      std.append Params [S|PoArgs] L1) =>

  clean-op-ty Ops S T1 T2.

pred operation-body-and-ty i:list prop, i:constant, i:term, 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 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,
      under-mixin-src-from-factory.do! Carrier Class [
        % just in case..
        mgref->term 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),
      ],
  ]),
].

% given an operation (a mixin projection) we generate a constant projection the
% same operation out of the package structure (out of the class field of the
% structure). We also provide all the other mixin dependencies (other misins)
% of the package structure.
pred export-1-operation i:mixinname, i:term, i:term, i:term, i:one-w-params mixinname, i:option constant, i:list prop, o:list prop.
export-1-operation _ _ _ _ _ none EX EX :- !. % not a projection, no operation
export-1-operation M Struct Psort Pclass MwP (some Poperation) EXI EXO :- !, std.do! [
  coq.gref->id (const Poperation) Name,

  w-params.then MwP mk-fun-prod ignore (operation-body-and-ty EXI Poperation Struct Psort Pclass) (pr Body BodyTy),

  if-verbose (coq.say "HB: export operation" Name),
  coq.env.add-const Name Body BodyTy ff ff C,

  w-params.nparams MwP NP,
  NImplicits is NP + 1,
  std.map {std.iota NImplicits} (_\r\ r = maximal) Implicits,
  coq.arguments.set-implicit (const C) [Implicits] tt,

  EXO = [exported-op M Poperation C|EXI]
].

% Given a list of mixins, it exports all operations in there
pred export-operations.aux i:term, i:term, i:term, i:one-w-params mixinname, i:list prop, o:list prop.
export-operations.aux Struct ProjSort ProjClass MwP EX1 EX2 :- !, std.do! [
  w-params_1 MwP (indt M),
  coq.CS.canonical-projections M Poperations,
  std.fold Poperations EX1 (export-1-operation (indt M) Struct ProjSort ProjClass MwP) EX2,
].

pred mixin-not-already-declared i:one-w-params mixinname.
mixin-not-already-declared MwP :-
  w-params_1 MwP M, not(mixin-first-class M _), M = indt _.

pred export-operations i:term, i:term, i:term, i:list-w-params mixinname, i:list prop, o:list prop, o:list mixinname.
export-operations Structure ProjSort ProjClass MLwP EX1 EX2 MLToExport :- std.do! [
  distribute-w-params MLwP LMwP,
  std.filter LMwP mixin-not-already-declared LMwPToExport,
  std.fold LMwPToExport EX1 (export-operations.aux Structure ProjSort ProjClass) EX2,
  std.map LMwPToExport w-params_1 MLToExport,
].

pred reexport-1-operation i:prop.
reexport-1-operation (exported-op _M _P C) :-
  add-abbrev {coq.gref->id (const C)} 0 (global (const C)) tt ff _.
pred reexport-operations i:list mixinname.
reexport-operations ML :- std.do! [
  std.flatten {std.map ML (m\ std.findall (exported-op m Poperation_ C_))} PL,
  std.forall PL reexport-1-operation
].

pred mk-coe-class-body
  i:factoryname, % From class
  i:factoryname, % To class
  i:list-w-params mixinname, % To mixins
  i:list term, i:term, % Params, T
  i:list (w-args mixinname),
  o:term.
mk-coe-class-body FC TC TMLwP Params T _ CoeBody :- std.do! [
  mk-app (global FC) {std.append Params [T]} Class,

  list-w-params_list TMLwP TML,
  std.map TML (from FC) Builders,
  std.map Builders (x\r\mk-app x Params r) BuildersP,

  mk-app (global {get-constructor (global TC)})
    {mk-n-holes {factory-nparams TC}} KCHoles,

  (pi c\ sigma Mixes\
    std.map BuildersP (builder\r\ r = app[builder, T, c]) Mixes,
    mk-app KCHoles [T | Mixes] (ClassCoercion c)),

  CoeBody = {{ fun (c : lp:Class) => lp:(ClassCoercion c) }}
].

pred mk-coe-structure-body
  i:structure, % From structure
  i:structure, % To structure
  i:factoryname, % To factory (for nparams)
  i:term, % class coercion
  i:term, % sort projection
  i:term, % class projection
  i:list term, i:term, % Params, T
  i:list (w-args mixinname),
  o:term.
mk-coe-structure-body StructureF StructureT TC Coercion SortProjection ClassProjection
    Params _T _ SCoeBody :- std.do! [

  mk-app StructureF      Params StructureP,
  mk-app SortProjection  Params SortP,
  mk-app ClassProjection Params ClassP,
  mk-app Coercion        Params CoercionP,

  mk-app (global {get-constructor StructureT})
    {mk-n-holes {factory-nparams TC}} PackPH,

  SCoeBody = {{ fun s : lp:StructureP =>
     let T : Type := lp:SortP s in
     lp:PackPH T (lp:CoercionP T (lp:ClassP s)) }},
].

% [declare-coercion P1 P2 C1 C2] declares a structure and a class coercion
% from C1 to C2 given P1 P2 the two projections from the structure of C1
pred declare-coercion i:term, i:term, i:class, i:class.
declare-coercion SortProjection ClassProjection
    (class FC StructureF FMLwP as FCDef) (class TC StructureT TMLwP as TCDef) :- std.do! [

  acc current (clause _ _ (sub-class FCDef TCDef)),

  term->modname StructureF ModNameF,
  term->modname StructureT ModNameT,
  CName is ModNameF ^ "_class_to_" ^ ModNameT ^ "_class",
  SName is ModNameF ^ "_to_" ^ ModNameT,

  if-verbose (coq.say "HB: declare coercion" SName),

  w-params.then FMLwP mk-fun mk-fun
    (mk-coe-class-body FC TC TMLwP) CoeBody,

  std.assert-ok! (coq.typecheck CoeBody Ty) "declare-coercion: CoeBody illtyped",

  if-verbose (coq.say "HB: declare coercion hint" CName),

  coq.env.add-const CName CoeBody Ty ff ff C,
  coq.coercion.declare (coercion (const C) 1 FC (grefclass TC)) tt,

  Coercion = global (const C),
  w-params.then FMLwP mk-fun ignore
    (mk-coe-structure-body StructureF StructureT TC Coercion SortProjection ClassProjection)
    SCoeBody,

  std.assert-ok! (coq.typecheck SCoeBody STy) "declare-coercion: SCoeBody illtyped",

  if-verbose (coq.say "HB: declare unification hint" SName),

  coq.env.add-const SName SCoeBody STy ff ff SC,
  coq.coercion.declare (coercion (const SC) 0 {term->gref StructureF} (grefclass {term->gref StructureT})) tt,
  coq.CS.declare-instance (const SC), % TODO: API in Elpi, take a @constant instead of gref
].

pred declare-join i:class, i:pair class class, o:prop.
declare-join (class C3 S3 _) (pr (class C1 S1 _) (class C2 S2 _)) (join C1 C2 C3) :-
  Name is {term->modname S1} ^ "_to_" ^ {term->modname S2},

  get-structure-coercion S3 S2 S3_to_S2,
  get-structure-coercion S3 S1 S3_to_S1,
  get-structure-sort-projection S1 S1_sort,
  get-structure-class-projection S2 S2_class,
  get-constructor S2 S2_Pack,

  % Cyril: /!\ BUG /!\ missing parameters!
  JoinBody = {{ fun s : lp:S3 =>
                   lp:{global S2_Pack} (lp:S1_sort (lp:S3_to_S1 s))
                              (lp:S2_class (lp:S3_to_S2 s)) }},

  std.assert-ok! (coq.typecheck JoinBody Ty) "declare-join: JoinBody illtyped",

  if-verbose (coq.say "HB: declare unification hint" Name),

  coq.env.add-const Name JoinBody Ty ff ff J,
  coq.CS.declare-instance (const J).

% TODO: this works under the invariant: we never have two classes that
% contain exactly the same mixins. hb.structure should enforce this
% and eventually just alias the existing one rather than failing.
% TODO: hb.structure should check we are not inserting the class
% in the middle of existing ones. Possible fix: always declare all intermediate
% possibilities but without proper names (requires the previous TODO about
% aliasing already existing stuff).
pred declare-unification-hints i:term, i:term, i:class, o:list prop.
declare-unification-hints SortProj ClassProj CurrentClass NewJoins :- std.do! [
  findall-classes All,

  std.filter All (sub-class? CurrentClass) AllSuper,
  std.forall AllSuper (declare-coercion SortProj ClassProj CurrentClass),

  findall-newjoins CurrentClass AllSuper TodoJoins,

  std.map TodoJoins (declare-join CurrentClass) NewJoins
].

% For each mixin we declare a field and apply the mixin to its dependencies
% (that are previously declared fields recorded via field-for-mixin)
pred synthesize-fields i:term, i:list (w-args mixinname), o:record-decl.
synthesize-fields _T []     end-record.
synthesize-fields T  [triple M Args _|ML] (field _ Name MTy Fields) :- std.do! [
  Name is {gref->modname M} ^ "_mixin",
  mgref->term Args T M MTy,
  @pi-decl `m` MTy m\ mixin-src T M m => synthesize-fields T ML (Fields m)
].

pred synthesize-fields.body i:list term, i:term, i:list (w-args mixinname), o:indt-decl.
synthesize-fields.body _Params T ML (record "axioms" {{ Type }} "Class" FS) :-
  synthesize-fields T ML FS.

pred mk-record+sort-field i:name, i:term, i:(term -> record-decl), o:indt-decl.
mk-record+sort-field _ T F (record "type" {{ Type }} "Pack" (field _ "sort" T F)).

pred mk-class-field i:classname, i:list term, i:term, i:list (w-args mixinname), o:record-decl.
mk-class-field ClassName Params T _ (field _ "class" (app [global ClassName|Args]) _\end-record) :-
  std.append Params [T] Args.

% Builds the axioms record and the factories from this class to each mixin
% TODO params
pred declare-class+structure i:list-w-params mixinname, o:factoryname, o:term, o:term, o:term, o:list prop.
declare-class+structure MLwP (indt ClassInd) Structure SortProjection ClassProjection AllFactories :- std.do! [

  if-verbose (coq.say "HB: declare axioms record"),

  w-params.then MLwP (mk-parameter explicit) (mk-parameter explicit)
    synthesize-fields.body ClassDeclaration,

  std.assert-ok! (coq.typecheck-indt-decl ClassDeclaration) "declare-class: illtyped",
  coq.env.add-indt ClassDeclaration ClassInd,
  coq.CS.canonical-projections ClassInd Projs,
  % TODO: put this code in a named clause
  w-params.nparams MLwP NParams,
  std.map2 {list-w-params_list MLwP} Projs (m\ p\ r\ sigma P\
    p = some P,
    r = from (indt ClassInd) m (global (const P))) Factories,
  AllFactories = [factory-nparams (indt ClassInd) NParams | Factories],

  if-verbose (coq.say "HB: declare type record"),

  w-params.then MLwP (mk-parameter explicit) mk-record+sort-field
    (mk-class-field (indt ClassInd)) StructureDeclaration,

  std.assert-ok! (coq.typecheck-indt-decl StructureDeclaration) "declare-structure: illtyped",
  coq.env.add-indt StructureDeclaration StructureName,

  coq.CS.canonical-projections StructureName [some SortP, some ClassP],
  Structure = global (indt StructureName),
  SortProjection = global (const SortP),
  ClassProjection = global (const ClassP),
].

% Declares "sort" as a coercion Structurename >-> Sortclass
pred declare-sort-coercion i:term, i:term.
declare-sort-coercion (global StructureName) (global Proj) :-

  if-verbose (coq.say "HB: declare sort coercion"),

  coq.coercion.declare (coercion Proj 0 StructureName sortclass) tt.

pred if-class-already-exists-error i:Name, i:list class, i:list mixinname.
if-class-already-exists-error _ [] _.
if-class-already-exists-error N [class _ S ML1wP|CS] ML2 :-
  list-w-params_list ML1wP ML1,
  if (list-eq-set ML1 ML2)
     (coq.error "Structure" {coq.term->string S} "contains the same mixins of" N)
     (if-class-already-exists-error N CS ML2).

% HB.structure Definition S P1 P2 := { T of F1 P1 T & F2 P1 (P2*P2) T }
%  cons p1\ cons p2\ nil t\ [triple f1 [p1] t,triple f2 [p1, {{p1 * p2}}] t]
pred main-declare-structure i:string, i:list-w-params gref, i:bool.
main-declare-structure Module GRFSwP ClosureCheck :- std.do! [
  factories-provide GRFSwP PMLwP,

  list-w-params.flatten-map GRFSwP factory-requires RMLwP, % TODO: extract code from factories-provide
  list-w-params.append PMLwP RMLwP UnsortedMLwP,
  w-params.map UnsortedMLwP (p\t\ toposort-mixins) MLwP,

  list-w-params_list PMLwP PML,
  list-w-params_list MLwP ML,

  if (ClosureCheck = tt, not({std.length PML} = {std.length ML}))
     (coq.warn "HB: pulling in dependencies:" {std.map {list-diff ML PML} nice-gref->string}
               "\nPlease list them or end the declaration with '&'")
     true,

  if-class-already-exists-error Module {findall-classes} ML,

  % TODO: check we never define the superclass of an exising class

  if-verbose (coq.say "HB: start module" Module),

  coq.env.begin-module Module none,

  declare-class+structure MLwP
    ClassName Structure SortProjection ClassProjection Factories,

  w-params.map MLwP (_\_\_\ mk-nil) NilwP,
  ClassRequires = factory-requires (ClassName) NilwP,
  ClassAlias = (factory-alias->gref ClassName ClassName),
  CurrentClass = (class ClassName Structure MLwP),

  %declare-structure MLwP ClassName  Structure SortProjection ClassProjection,

  if-verbose (coq.say "HB: start module Exports"),

  coq.env.begin-module "Exports" none,
  declare-sort-coercion Structure SortProjection,
  if-verbose (coq.say "HB: exporting operations"),
  ClassAlias => ClassRequires => Factories =>
    export-operations Structure SortProjection ClassProjection MLwP [] EX MLToExport,
  if-verbose (coq.say "HB: exporting unification hints"),
  ClassAlias => ClassRequires => Factories =>
    declare-unification-hints SortProjection ClassProjection CurrentClass NewJoins,
  % Register in Elpi's DB the new structure
  % NOT TODO: All these acc are correctly locaed in an Export Module
  if-verbose (coq.say "HB: accumulating various props"),
  std.forall MLToExport (m\  acc current (clause _ _ (mixin-first-class m ClassName))),
  std.forall EX (ex\ acc current (clause _ _ ex)),
  std.forall Factories (f\ acc current (clause _ _ f)),
  acc current (clause _ _ ClassRequires),
  acc current (clause _ _ ClassAlias),
  acc current (clause _ _ (is-structure Structure)),
  std.forall NewJoins (j\ acc current (clause _ _ j)),
  acc current (clause _ _ (class-def CurrentClass)),

  if-verbose (coq.say "HB: stop module Exports"),
  coq.env.end-module Exports,

  if-verbose (coq.say "HB: reexporting previous operations as notations"),
  EX => reexport-operations ML,

  coq.env.end-module _,

  if-verbose (coq.say "HB: end modules; export" Exports),

  export Exports,

  declare-factory-abbrev Module (factory-by-classname ClassName),
].

/* HB.context?
pred main-begin-declare i:string, i:string, i:list gref, i:declaration.
main-begin-declare Module TName GRFS Decl :- std.do! [

  if-verbose (coq.say "HB: start module and section" Module),

  coq.env.begin-module Module none,
  coq.env.begin-section Module,

  if-verbose (coq.say "HB: postulate type" TName),

  coq.fresh-type Ty,
  coq.env.add-const TName _ Ty tt tt T, % no body, local -> a variable
  main-declare-context (global (const T)) [] GRFS _, % TODO params
  acc current (clause _ _ (current-decl Decl))
].
*/

pred main-end-declare-builders.
main-end-declare-builders :- std.do! [
  current-decl (builders-for-factory GR),

  coq.env.end-section,

  findall-builders LFIL,

  if-verbose (coq.say "HB: declare builders from factory" {nice-gref->string GR}
              "using" {std.map LFIL builder->string}),

  std.fold LFIL [] main-declare-builder Clauses,

  if (Clauses = [])
     (coq.error "No builders to declare, did you forget HB.instance?")
     true,

  % TODO: Do we need this module?
  gref->modname GR M,
  Name is M ^ "_Exports",
  coq.env.begin-module Name none,
  (std.forall Clauses c\ acc current (clause _ _ c)),

  coq.env.end-module Exports,
  coq.env.end-module _,
  export Exports,
].

pred main-declare-canonical-instances i:term, i:term.
main-declare-canonical-instances T F :- std.do! [
  if (current-decl (builders-for-factory FGR))
     (new_int N, acc current (clause _ _ (builder-decl (builder N FGR F))))
     true,
  under-mixin-src-from-factory.do! T F [
    under-canonical-mixins-of.do! T [
      declare-instances T {findall-classes}
  ]],
].

pred declare-old-located i:string, i:located.
declare-old-located Id (loc-gref GR) :-
  add-abbrev Id 0 (global GR) tt ff _.
declare-old-located Id (loc-abbreviation Abbrev) :-
  coq.notation.abbreviation Abbrev [] T,
  % FIXME: this assumes the abbreviation has no arg
  % we should fix it.
  add-abbrev Id 0 T tt ff _.

pred declare-old-constant i:option constant.
declare-old-constant none.
declare-old-constant (some C) :-
  coq.gref->id (const C) Id,
  std.forall {coq.locate-all Id} (declare-old-located Id).
declare-old-constant _ :- true.

pred context->factory i:context-decl, o:factoryname.
context->factory (context-item IDT _ TTy none t\ context-item _ _ (TF t) none _\ context-end) GRF :- !,
  coq.id->name IDT NameT,
  @pi-decl NameT TTy t\
    std.assert! (factory? (TF t) (triple GRF _Params t))
      "the last argument must be a factory applied to the type variable".
context->factory (context-item ID _ T none Factories) GRF :- !,
  coq.id->name ID Name, @pi-decl Name T x\ context->factory (Factories x) GRF.
context->factory (context-item ID _ _ (some _) _) _ :-
  coq.error "context item cannot be given a body:" ID.

pred main-begin-declare-builders i:context-decl.
main-begin-declare-builders Ctx :- std.do! [
  Name is "Builders_" ^ {term_to_string {new_int}}, % TODO?
  context->factory Ctx GRF,
  coq.env.begin-module Name none,
  if (GRF = indt FRecord) (std.do! [
    coq.env.begin-module "Super" none,
    std.forall {coq.CS.canonical-projections FRecord} declare-old-constant,
    coq.env.end-module _]) (true),
  coq.env.begin-section Name,
  builders-postulate-factories Ctx,
].

pred postulate-factory-abbrev i:term, i:id, i:factoryname, o:term.
postulate-factory-abbrev TheType Name Falias TheFactory :- std.do! [
  factory-alias->gref Falias F,
  phant-abbrev F _ Fabv,
  coq.notation.abbreviation Fabv [TheType] Package,
  Msg is "Unable to declare factory " ^ Name,
  std.assert-ok! (coq.typecheck-ty Package _) Msg,
  coq.env.add-const Name _ Package tt tt C,
  TheFactory = global (const C),
].

% Only record fields can be exported as operations.
pred define-factory-operations i:term, i:term, i:gref.
define-factory-operations TheType TheFactory (indt I) :- !,
  coq.env.indt I _ NParams _ _ _ _,
  NHoles is NParams - 1,
  coq.CS.canonical-projections I PL,
  std.forall PL (define-factory-operation TheType TheFactory NHoles).
define-factory-operations _ _ _.

pred define-factory-operation i:term, i:term, i:int, i:option constant.
define-factory-operation _ _ _ none.
define-factory-operation TheType TheFactory NHoles (some P) :-
  mk-n-holes NHoles Holes,
  std.append Holes [TheFactory] Holes_Factory,
  T = app[global (const P), TheType|Holes_Factory],
  std.assert-ok! (coq.typecheck T _) "Illtyped applied factory operation",
  coq.gref->id (const P) Name,
  add-abbrev Name 0 T ff ff _.

pred builders-postulate-factories i:context-decl.
builders-postulate-factories (context-item IDT _ TTy none t\ context-item IDF _ (TF t) none _\ context-end) :- !, std.do! [
  % TODO we should allow T to be anything.
  std.assert! (TTy = sort (typ _)) "The last context item before the factory must be a type variable",
  coq.fresh-type Ty,
  coq.env.add-const IDT _ Ty tt tt C, % no body, local -> a variable
  TheType = global (const C),

  std.assert! (factory? (TF TheType) (triple GRF Params TheType))
    "the last argument must be a factory applied to the type variable",
  factory-requires GRF GRFMLwP, % TODO: remove, pass to main-declare-context the list-w-params-eta-expansion of GRF
  main-declare-context TheType Params GRFMLwP _,
  postulate-factory-abbrev TheType IDF GRF TheFactory,
  define-factory-operations TheType TheFactory GRF,
  acc current (clause _ _ (current-decl (builders-for-factory GRF))),
].

builders-postulate-factories (context-item ID _ T none Factories) :- std.do! [
  coq.env.add-const ID _ T tt tt P, % no body, local -> a variable
  TheParam = global (const P),
  builders-postulate-factories (Factories TheParam),
].

builders-postulate-factories (context-item ID _ _ (some _) _) :-
  coq.error "context item cannot be given a body:" ID.

% In an asset like HB.mixing Recoord P1 .. PN A of F1 .. & FK ..
% we call "named" P1 .. PN A, hence A is the last named asset param
pred is-last-named-asset-param i:asset-decl.
is-last-named-asset-param (asset-parameter _ {{ lib:hb.indexed _ }} _) :- !.
is-last-named-asset-param (asset-parameter _ _ p\ asset-parameter _ (M p) _) :- pi p\ factory? (M p) _, !.
is-last-named-asset-param (asset-parameter _ _ _\ asset-record _ _ _ _) :- !.
is-last-named-asset-param (asset-parameter _ _ _\ asset-alias _ _) :- !.

% main-declare-asset Asset AssetKind
pred main-declare-asset i:asset-decl, i:asset.
main-declare-asset Asset AssetKind :- std.do! [
  name-of-asset-decl Asset Module,

  if-verbose (coq.say "HB: start module and section" Module),

  coq.env.begin-module Module none,
  coq.env.begin-section Module,

  process-asset-named-parameters Asset AssetKind Module [],
].

pred process-asset-named-parameters i:asset-decl, i:asset, i:id, i:list (pair term term).
% We reached TheType
process-asset-named-parameters (asset-parameter Name _ Rest as R) D Module Params :- is-last-named-asset-param R, !, std.do! [

  if-verbose (coq.say "HB: postulate type" Name),

  coq.fresh-type Ty,
  coq.env.add-const Name _ Ty tt tt C, % no body, local -> a variable
  TheType = global (const C),
  process-asset-unnamed-parameters (Rest TheType) [] Module TheType D {std.rev Params}
].
% This is a real parameter
process-asset-named-parameters (asset-parameter Name T Rest) D Module Params :- std.do! [
  std.assert-ok! (coq.typecheck-ty T _) "Illtyped parameter",
  coq.env.add-const Name _ T tt tt C, % no body, local -> a variable
  TheParam = global (const C),
  process-asset-named-parameters (Rest TheParam) D Module [pr TheParam T|Params],
].

pred process-asset-unnamed-parameters
  i:asset-decl, i:list (w-args factoryname), i:id, i:term, i:asset, i:list (pair term term).
process-asset-unnamed-parameters (asset-parameter _ T Rest) FS Module TheType D Params :- std.do! [
  std.assert! (factory? T (triple F Ps TheType)) "Not a factory applied to the type variable",
  std.assert! (pi x y\ Rest y = Rest x) "Factories cannot be explicitly mentioned in the mixin",
  Dummy = sort prop,
  process-asset-unnamed-parameters (Rest Dummy) [triple F Ps TheType|FS] Module TheType D Params,
].

% (*) We did substitute bound variables by terms, we would end up outside the pattern fragment
%  X x = (global(cont "foo"))        X := _\ (global ...)     1 solution
%  X x = x                           X := a\a                 1 solution
%  X x (global(cont "foo")) = (global(cont "foo"))   X := _\a\a   or   X := _\_\ (global ...)  2 solution, bad

process-asset-unnamed-parameters (asset-alias _ Ty) GRFS Module TheType D Params :- std.do! [
  std.assert! (D = asset-factory) "Mixins cannot be aliases",
  % refresh implicit arguments, since many binders are now gone (*)
  (pi X Y\ copy X Y :- var X, !) => copy Ty Ty1,
  build-list-w-params Params  TheType {std.rev GRFS} GRFSwParams,
  declare-factory-alias Ty1 GRFSwParams Module TheType {std.map Params fst},
].

process-asset-unnamed-parameters (asset-record _ Sort _ Fields) GRFS Module TheType D Params :- std.do! [
  % refresh implicit arguments, since many binders are now gone
  (pi X Y\ copy X Y :- var X, !) => (copy-fields Fields Fields0, copy Sort Sort1),
  build-list-w-params Params  TheType {std.rev GRFS} GRFSwParams,
  declare-mixin-or-factory Sort1 Fields0 GRFSwParams Module TheType D {std.map Params fst},
].

pred declare-factory-alias i:term, i:list-w-params factoryname, i:id, i:term, i:list term.
declare-factory-alias Ty1 GRFSwP Module TheType TheParams :- std.do! [

  % TODO maybe main-declare-context should just take GRFSwP and postulate
  % the parameters and the type
  main-declare-context TheType TheParams GRFSwP Hyps,

  std.assert-ok! (coq.typecheck-ty Ty1 _) "Illtyped alias factory",
  coq.env.add-const "axioms_" Ty1 _ ff ff C,

  std.assert! (safe-dest-app Ty1 (global PhF) _Args) "Argument must be a factory",
  std.assert! (factory-alias->gref PhF F) "BUG: Factory alias declaration missing",
  std.assert! (factory-constructor F FK) "BUG: Factory constructor missing",

  Hyps => mgref->term TheParams TheType FK MFK,
  std.assert-ok! (coq.typecheck MFK MFKTy) "BUG: typecking of former factory constructor failed",
  (pi Args\ copy (app [global F|Args]) (global (const C))) => copy MFKTy MFKTyC,
  coq.env.add-const "Axioms_" MFK MFKTyC ff ff CK,
  GRK = const CK,

  coq.env.end-section,

  mk-phant-term (global GRK) PhGRK0,
  if (mixin-first-class F _) (PhGRK = PhGRK0) (append-phant-unify PhGRK0 PhGRK),
  mk-phant-abbrev "Build" PhGRK BuildConst _,

  % std.map Hyps mixin-src_mixin ML,
  factories-provide GRFSwP MLwP,
  main-factory-requires "axioms" (const C) MLwP Props SN,

  if-verbose (coq.say "HB: start module Exports"),

  coq.env.begin-module "Exports" none,
  (std.forall Props c\ acc current (clause _ _ c)),
  % std.map {gr-deps GRK} (_\ r\ r = maximal) Implicits,
  % coq.arguments.set-implicit GRK [[maximal|Implicits]] tt,
  w-params.nparams MLwP NParams,
  acc current (clause _ _ (factory-nparams (const C) NParams)),
  acc current (clause _ _ (factory-constructor (const C) GRK)),
  acc current (clause _ _ (factory-builder-nparams BuildConst NParams)),
  coq.env.end-module Exports,
  coq.env.end-module _Module,

  if-verbose (coq.say "HB: end modules and sections; export" Exports),

  export Exports,

  declare-factory-abbrev Module SN,
].

pred declare-mixin-or-factory i:term, i:record-decl, i:list-w-params factoryname, i:id, i:term, i:asset, i:list term.
declare-mixin-or-factory Sort1 Fields0 GRFSwP Module TheType D TheParams :- std.do! [
  if (D = asset-mixin) (Fields1 = Fields0)
      (Fields1 = (field _ "_" {{ lib:hb.unify Type Type lp:TheType lp:TheType
        lib:hb.nomsg }} _\ Fields0)),
  main-declare-context TheType TheParams GRFSwP _Hyps,

  if-verbose (coq.say "HB: declare record axioms_"),

  Kname = "Axioms_",
  RDecl = record "axioms_" Sort1 Kname Fields1,
  std.assert-ok! (coq.typecheck-indt-decl RDecl) "record declaration illtyped",
  coq.env.add-indt RDecl R,
  coq.env.end-section,
  coq.env.indt R tt _ _ _ [K] _,
  GRK = indc K,

  % TODO: should this be in the Exports module?
  if-verbose (coq.say "HB: declare notation axioms"),

  mk-phant-term (global GRK) PhGRK0,

  if-verbose (coq.say "HB: declare notation Axioms"),

  if (D = asset-mixin) (PhGRK = PhGRK0) (append-phant-unify PhGRK0 PhGRK),
  mk-phant-abbrev "Build" PhGRK BuildConst _,

  % std.map Hyps mixin-src_mixin ML,
  factories-provide GRFSwP MLwP,
  if (D = asset-mixin)
     (main-mixin-requires "axioms" (indt R) MLwP Props SN)
     (main-factory-requires "axioms" (indt R) MLwP Props SN),

  if-verbose (coq.say "HB: start module Exports"),

  coq.env.begin-module "Exports" none,
  (std.forall Props c\ acc current (clause _ _ c)),
  w-params.nparams MLwP NParams,
  acc current (clause _ _ (factory-nparams (indt R) NParams)),
  std.map {list-w-params_list {gr-deps GRK}} (_\ r\ r = maximal) Implicits,
  coq.arguments.set-implicit GRK [[maximal|Implicits]] tt,
  acc current (clause _ _ (factory-constructor (indt R) GRK)),
  acc current (clause _ _ (factory-builder-nparams BuildConst NParams)),
  coq.env.end-module Exports,
  coq.env.end-module _Module,

  if-verbose (coq.say "HB: end modules and sections; export" Exports),

  export Exports,

  declare-factory-abbrev Module SN,
].