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

namespace structure {

% 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 declare i:string, i:term, i:sort.
declare Module BSkel Sort :- std.do! [
  disable-id-phant BSkel BSkelNoId,
  std.assert-ok! (coq.elaborate-skeleton BSkelNoId _ BNoId) "illtyped structure definition",
  re-enable-id-phant BNoId B,
  private.sigT->list-w-params B GRFSwP ClosureCheck,
  
  factories-provide GRFSwP PMLwP,

  list-w-params.flatten-map GRFSwP gref-deps 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,

  synthesis.list-w-params.check-key MLwP,

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

  private.if-class-already-exists-error Module {findall-classes-for ML} ML,
  private.if-coverage-not-good-error ML,

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

  if-verbose (coq.say {header} "start module" Module),

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

  private.declare-class+structure MLwP Sort
    ClassName Structure SortProjection ClassProjection Factories StructKeyClause,

  w-params.map MLwP (_\_\_\ mk-nil) NilwP,
  ClassAlias = (factory-alias->gref ClassName ClassName ok),
  CurrentClass = (class ClassName Structure MLwP),
  ClassName = indt ClassInd, coq.env.indt ClassInd _ _ _ _ [ClassK] _,
  GRDepsClauses =
    [gref-deps (indt ClassInd) NilwP, gref-deps (indc ClassK) MLwP],
  std.map ML (m\ o\ o = mixin-class m ClassName) MixinMems,
  std.filter ML (m\ not (mixin-first-class m _)) NewMixins,
  std.map NewMixins (m\ r\ r = mixin-first-class m ClassName) MixinFirstClass,


  if-verbose (coq.say {header} "structure: new mixins" NewMixins),
  if-verbose (coq.say {header} "structure: mixin first class" MixinFirstClass),


  if-verbose (coq.say {header} "declaring clone abbreviation"),
  w-params.then MLwP phant.fun-real phant.fun-real
    (private.clone-phant-body ClassName SortProjection Structure) PhClone,
  phant.add-abbreviation "clone" PhClone _ _,

  if-verbose (coq.say {header} "declaring pack_ constant"),
  (ClassAlias => class-def CurrentClass => GRDepsClauses => MixinMems =>
    w-params.then MLwP mk-fun mk-fun (private.pack-body ClassName) Pack),
  if-verbose (coq.say {header} "declaring pack_ constant =" Pack),
  log.coq.env.add-const-noimplicits "pack_" Pack _ @transparent! ConstPack,
  GRPack = const ConstPack,

  if-arg-sort (
    if-verbose (coq.say {header} "define arg_sort"),
    std.assert-ok! (coq.typecheck SortProjection SortProjTy)
      "HB: BUG: cannot retype projection",
    log.coq.env.add-const-noimplicits "arg_sort" SortProjection SortProjTy ff ArgSortCst
  ),

  if-verbose (coq.say {header} "start module Exports"),

  log.coq.env.begin-module "Exports" none,

  %(ClassAlias => class-def CurrentClass =>
  %  GRDepsClauses => MixinFirstClass => gref-deps GRPack MLwP =>
  %    phant.of-gref tt GRPack [] PhRepack),
  %if-verbose (coq.say {header} "declaring pack abbreviation =" PhRepack),
  % phant.add-abbreviation "pack" PhRepack _ PackAbbrev,
  
  if (get-option "short.type" ShortType) (
    if-verbose (coq.say {header} "short name for type:" ShortType),
    (@global! => log.coq.notation.add-abbreviation
      ShortType 0 (global Structure) ff _)) true,

  coq.mk-app (global Structure) {coq.mk-n-holes {w-params.nparams MLwP}} HB_Instance,
  if (get-option "short.pack" ShortPack) (std.do! [
    if-verbose (coq.say {header} "declaring pack abbreviation:" ShortPack),
    % coq.notation.abbreviation-body PackAbbrev NPackAbbrev PackAbbrevTrm,
    % @global! => log.coq.notation.add-abbreviation
    %  ShortPack NPackAbbrev PackAbbrevTrm ff _
      coq.notation.add-abbreviation-for-tactic ShortPack "HB.pack_for" [trm HB_Instance]
    ]) true,
  %  (std.do! [
  %  PackAbbrevName is Module ^ ".pack",
  %  if-verbose (coq.say {header} "declaring pack abbreviation:" PackAbbrevName),
  %  coq.notation.add-abbreviation-for-tactic PackAbbrevName "HB.pack_for" [trm HB_Instance],
  %]),

  if-verbose (coq.say {header} "making coercion from type to target"),
  synthesis.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 {header} "exporting unification hints"),
  ClassAlias => Factories => GRDepsClauses =>
    private.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 (ClassName = indt ClassInd) (std.do![
    if-verbose (coq.say {header} "exporting coercions from class to mixins"),
    std.forall {coq.env.projections ClassInd}
      (private.export-mixin-coercion ClassName)
    ])
    (coq.say "declare:" ClassName "should be an inductive", fail),

  if-verbose (coq.say {header} "accumulating various props"),
  std.flatten [
      Factories, [is-structure Structure],
      NewJoins, [class-def CurrentClass], GRDepsClauses,
      [gref-deps GRPack MLwP], MixinMems, [StructKeyClause]
    ]
    NewClauses,
  acc-clauses current NewClauses,

  if-verbose (coq.say {header} "stop module Exports"),
  log.coq.env.end-module-name "Exports" Exports,

  log.coq.env.import-module "Exports" Exports,

  if-verbose (coq.say {header} "declaring on_ abbreviation"),

  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)),

  if-verbose (coq.say {header} "declaring `copy` abbreviation"),

  coq.mk-app (global ClassName) {params->holes NilwP} AppClassHoles,
  @global! => log.coq.notation.add-abbreviation "copy" 2
    {{fun T C => (lp:(ClassOfAbbrev_ C) : (lp:AppClassHoles T)) }} tt _,

  if-verbose (coq.say {header} "declaring on abbreviation"),

  @global! => log.coq.notation.add-abbreviation "on" 1
    {{fun T => (lp:{{ ClassOfAbbrev_ {{_}} }} : (lp:AppClassHoles T)) }} tt
    _OnAbbrev,

  log.coq.env.end-module-name Module ModulePath,

  if-verbose (coq.say {header} "end modules; export" Exports),

  export.module {calc (Module ^ ".Exports")} Exports,

  if-verbose (coq.say {header} "exporting operations"),
    ClassAlias => Factories => GRDepsClauses =>
      private.export-operations Structure SortProjection ClassProjection MLwP [] EX MLToExport,
    % TODO: issue an Arguments op T : rename, where T is the name written by
    %   the user in Definition foo := { T of ... }

  if-verbose (coq.say {header} "operations meta-data module: ElpiOperations"),

  ElpiOperationModName is {calc (Module ^ "ElpiOperations")},
  log.coq.env.begin-module ElpiOperationModName none,
  acc-clauses current {std.append EX MixinFirstClass},
  log.coq.env.end-module-name ElpiOperationModName ElpiOperations,
  export.module ElpiOperationModName ElpiOperations,

  if-verbose (coq.say {header} "abbreviation factory-by-classname"),

  ClassAlias => NewClauses => factory.declare-abbrev Module (factory.by-classname ClassName) ClassAbbrev,
  export.clause (phant-abbrev ClassName ClassName ClassAbbrev),

  NewClauses => if-MC-compat (private.mc-compat-structure Module ModulePath MLToExport
    {w-params.nparams MLwP} ClassProjection GRPack),

% Automatic saturation disabled since it is expensive
%  NewClauses => instance.saturate-instances,
].

/* ------------------------------------------------------------------------- */
/* ----------------------------- private code ------------------------------ */
/* ------------------------------------------------------------------------- */

namespace private {

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

% 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 :-
  gref-deps (const Po) MLwP,
  w-params.nparams MLwP NParams,
  std.length {list-w-params_list MLwP} NMixins,

  (pi L L1 L2 Params Rest PoArgs\
    copy (app [global (const Po)| L]) (app [global (const C) | L2]) :-
      std.split-at NParams L Params [_|Rest],
      std.drop NMixins Rest PoArgs,
      std.append Params [S|PoArgs] L1,
      std.map L1 copy L2) =>
  clean-op-ty 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 _ ParamsOp _) (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-gref-deps 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),
      ],
  ]),
].

% 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:structure, 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 {header} "export operation" Name),
  log.coq.env.add-const-noimplicits Name Body BodyTy @transparent! C,

  w-params.nparams MwP NP,
  NImplicits is NP + 1,
  std.iota NImplicits INI,
  std.map INI (_\r\ r = maximal) Implicits,
  @global! => log.coq.arguments.set-implicit (const C) [Implicits],

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

% Given a list of mixins, it exports all operations in there
pred export-operations.aux i:structure, 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.env.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:structure, i:term, i:term, i:mixins, 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 mk-coe-class-body
  i:factoryname, % From class
  i:factoryname, % To class
  i:mixins, % 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 (global x) Params r) BuildersP,

  factory-nparams TC TCNP,
  mk-app (global {get-constructor TC})
    {coq.mk-n-holes TCNP} 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 (global StructureF) Params StructureP,
  mk-app     SortProjection  Params SortP,
  mk-app     ClassProjection Params ClassP,
  mk-app     Coercion        Params CoercionP,

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

  SCoeBody = {{ fun s : lp:StructureP =>
     (* let T := lp:SortP s in*)
     lp:PackPH (lp:SortP s) (lp:CoercionP (lp:SortP s) (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) (class TC StructureT TMLwP) :- std.do! [

  gref->modname StructureF 2 "_" ModNameF,
  gref->modname StructureT 2 "_" ModNameT,
  CName is ModNameF ^ "_class__to__" ^ ModNameT ^ "_class",
  SName is ModNameF ^ "__to__" ^ ModNameT,

  if-verbose (coq.say {header} "declare coercion" SName),

  w-params.then FMLwP mk-fun mk-fun
    (mk-coe-class-body FC TC TMLwP) CoeBody,
  ErrorMessage is "The structures " ^ ModNameF ^ " and " ^ ModNameT ^ " are incompatible: the coercion between them cannot be synthesized",
  std.assert-ok! (coq.elaborate-skeleton CoeBody Ty CoeBody') ErrorMessage,

  if-verbose (coq.say {header} "declare coercion hint" CName),

  log.coq.env.add-const-noimplicits CName CoeBody' Ty @transparent! C,
  log.coq.coercion.declare (coercion (const C) 1 FC (grefclass TC)),

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

 ErrorMessage is "The structures " ^ ModNameF ^ " and " ^ ModNameT ^ " are incompatible: the coercion between them cannot be synthesized",
  std.assert-ok! (coq.elaborate-skeleton SCoeBody STy SCoeBody') ErrorMessage,

  if-verbose (coq.say {header} "declare unification hint" SName),

  log.coq.env.add-const-noimplicits SName SCoeBody' STy @transparent! SC,
  log.coq.coercion.declare (coercion (const SC) 0 StructureF (grefclass StructureT)),

  log.coq.CS.declare-instance SC,

  w-params.nparams FMLwP NparamsSC,
  acc-clause current (sub-class FC TC SC NparamsSC)
].

pred join-body i:int, i:int, i:structure, i:term, i:term, i:term, i:term, i:term,
  i:list term, i:name, i:term, i:(term -> A), o:term.
join-body N1 N2 S3 S2_Pack S1_sort S3_to_S1 S2_class S3_to_S2
  P N _Ty _F (fun N S3P Pack) :- !,
  mk-app (global S3) P S3P, !,
  @pi-decl N S3P s\
  sigma S3_to_S1_Ps S3_to_S2_Ps S1_sortS3Ps S2_classS3Ps Holes1 Holes2 \ std.do! [
    coq.mk-n-holes N2 Holes2,
    coq.mk-n-holes N1 Holes1,
    mk-app S3_to_S1 {std.append P [s]} S3_to_S1_Ps,
    mk-app S1_sort {std.append Holes1 [S3_to_S1_Ps]} S1_sortS3Ps,
    mk-app S3_to_S2 {std.append P [s]} S3_to_S2_Ps,
    mk-app S2_class {std.append Holes2 [S3_to_S2_Ps]} S2_classS3Ps ,
    mk-app S2_Pack {std.append Holes2 [S1_sortS3Ps, S2_classS3Ps]} (Pack s)
  ].

pred declare-join i:class, i:pair class class, o:prop.
declare-join (class C3 S3 MLwP3) (pr (class C1 S1 _) (class C2 S2 _)) (join C1 C2 C3) :-
  Name is "join_" ^ {gref->modname S3 2 "_"} ^
    "_between_" ^ {gref->modname S1 2 "_"} ^ "_and_" ^ {gref->modname S2 2 "_"},

  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,

  factory-nparams C1 N1,
  factory-nparams C2 N2,

  if-verbose (coq.say {header} "declare unification hint" Name),
  w-params.fold MLwP3 mk-fun (join-body N1 N2 S3
    (global S2_Pack) S1_sort S3_to_S1 S2_class S3_to_S2) JoinBody,
  std.assert-ok! (coq.typecheck JoinBody Ty) "declare-join: JoinBody illtyped",
  log.coq.env.add-const-noimplicits Name JoinBody Ty @transparent! J,
  log.coq.CS.declare-instance 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 2 "_"} ^ "_mixin",
  if-verbose (coq.say {header} "typing class field" M),
  std.assert! (synthesis.infer-all-gref-deps Args T M MTy) "anomaly: a field type cannot be solved",
  @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:sort, i:name, i:term, i:(term -> record-decl), o:indt-decl.
mk-record+sort-field Sort _ T F (record "type" (sort Sort) "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 [canonical ff] "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
pred declare-class+structure i:mixins, i:sort, o:factoryname, o:structure, o:term, o:term, o:list prop, o:prop.
declare-class+structure MLwP Sort
    (indt ClassInd) (indt StructureInd) SortProjection ClassProjection AllFactories
    (structure-key SortP ClassP (indt StructureInd)):- std.do! [

  if-verbose (coq.say {header} "declare axioms record"MLwP ),

  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",
  (@primitive! => log.coq.env.add-indt ClassDeclaration ClassInd),

  coq.env.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\
    std.assert! (p = some P) "BUG: we build a class with an anonymous field",
    r = from (indt ClassInd) m (const P)) Factories,
  AllFactories = [factory-nparams (indt ClassInd) NParams | Factories],

  if-verbose (coq.say {header} "declare type record"),

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

  std.assert-ok! (coq.typecheck-indt-decl StructureDeclaration) "declare: illtyped",
  if (get-option "primitive" tt)
    (@primitive! => log.coq.env.add-indt StructureDeclaration StructureInd)
    (log.coq.env.add-indt StructureDeclaration StructureInd),

  coq.env.projections StructureInd [some SortP, some ClassP],
  global (const SortP) = SortProjection,
  global (const ClassP) = ClassProjection,
].

% 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 {header} "declare sort coercion"),

  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 _ [] _.
if-class-already-exists-error N [class _ S ML1wP|CS] ML2 :-
  list-w-params_list ML1wP ML1,
  if (std.list-eq-set ML1 ML2)
     (coq.error "Structure" {nice-gref->string S} "contains the same mixins as" N)
     (if-class-already-exists-error N CS ML2).

pred export-mixin-coercion i:classname, i:option constant.
export-mixin-coercion _ none.
export-mixin-coercion ClassName (some C) :-
  coq.env.typeof (const C) CTy,
  coq.prod-tgt->gref CTy MixinGR,
  if-verbose (coq.say {header} "export class to mixin coercion for mixin" {nice-gref->string MixinGR}),
  log.coq.coercion.declare (coercion (const C) _ ClassName (grefclass MixinGR)).

pred mc-compat-structure i:string, i:modpath, i:list mixinname, i:int, i:term, i:gref, i:option gref.
mc-compat-structure ModuleName _Module NewMixins CNParams ClassProjection GRPack Axioms :- std.do! [
  CompatModuleName is "MathCompCompat" ^ ModuleName,
  log.coq.env.begin-module CompatModuleName none, % to avoid collisions
  log.coq.env.begin-module ModuleName none,

  if (Axioms = some GR)
    (@global! => log.coq.notation.add-abbreviation "axiom" 0 (global GR) ff _)
    true,

  if (NewMixins = [NewMixin]) (std.do! [
    if-verbose (coq.say "mc-compat-structure: declaring notations 'axioms', 'mixin_of' and 'Mixin'"),
    factory-nparams NewMixin NewMixinNP,
    MArgs is NewMixinNP + 1,
    mk-eta MArgs {coq.env.typeof NewMixin} (global NewMixin) EtaNewMixin,
    @global! => log.coq.notation.add-abbreviation "axioms" MArgs EtaNewMixin ff _,
    @deprecated! "mathcomp 2.0.0" "use the factory instead" =>
    @global! => log.coq.notation.add-abbreviation "mixin_of" MArgs EtaNewMixin ff _,
    std.assert! (factory-constructor NewMixin FK) "BUG: Factory constructor missing",
    std.assert! (phant-abbrev FK _ PhAbb) "BUG: missing phant-abbrev",
    @deprecated! "mathcomp 2.0.0" "use the F.Build instead" =>
      @global! => log.coq.notation.add-abbreviation "Mixin" 0
        {coq.notation.abbreviation PhAbb {coq.mk-n-holes MArgs}} ff _,
    if-verbose (coq.say "mc-compat-structure: declaring pack abbreviation"),
    @deprecated! "mathcomp 2.0.0" "use native HB Structure.pack instead" =>
    phant.add-abbreviation "mcpack" {phant.of-gref ff GRPack [NewMixin]} _ _,
    ])
    (if-verbose (coq.say "mc-compat-structure: not exactly one new mixin")),

  if-verbose (coq.say "mc-compat-structure: declaring notation 'class_of'"),
  std.assert-ok! (coq.typecheck ClassProjection ClassProjectionTy) "wtf",
  CArgs is CNParams + 1,
  mk-eta CArgs ClassProjectionTy ClassProjection EtaClassProjection,
  @global! => log.coq.notation.add-abbreviation "class_of" CArgs EtaClassProjection ff _,

  log.coq.env.end-module-name ModuleName _,
  log.coq.env.end-module-name CompatModuleName MCCompat,
  log.coq.env.export-module CompatModuleName MCCompat,
  %coq.env.import-module Module,
].

pred clone-phant-body i:factoryname, i:term, i:structure, i:list term, i:term, i:list (w-args mixinname), o:phant-term.
clone-phant-body ClassName SortProjection ((indt I) as Structure) PL T _ PhF :- std.do! [
  std.assert! (coq.env.indt I _ _ _ _ [PackC] _) "wtf",
  mk-app (global (indc PackC)) {std.append PL [T]} PackPLT,
  mk-app (global Structure) PL SPL,
  (@pi-decl `cT` SPL cT\
  mk-app (global ClassName) {std.append PL [T]} CPL,
  @pi-decl `c` CPL c\
  (Ph cT c) =
    {phant.fun-unify none T {mk-app {mk-app SortProjection PL} [cT]}
      {phant.fun-unify none cT {mk-app PackPLT [c]}
        {phant.init {mk-app PackPLT [c]}} }}),
  PhF = {phant.fun-real `cT` SPL cT\ {phant.fun-implicit `c` CPL c\ Ph cT c }}
].

% [pack-body ClassName P T MLwA B] asserts
%  B = fun m0 ... mn => Pack P T (Class P T m0 ... mn)
% under a context with P and T
pred pack-body i:classname, i:list term, i:term, i:list (w-args mixinname), o:term.
pack-body ClassName PL T MLwA F :- std.do! [
  class-def (class ClassName S _),
  get-constructor ClassName BuildC,
  get-constructor S PackS,
  synthesis.under-mixins.then MLwA mk-fun
    (pack-body.aux PL T BuildC PackS) F,
].
pack-body.aux PL T BuildC PackS  Body :- !, std.do! [
  synthesis.infer-all-gref-deps PL T BuildC Class,
  mk-app (global PackS) {std.append PL [T, Class]} Body
].

pred mk-infer-key i:class, i:term, i:mixins, 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 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.
if-coverage-not-good-error ML :-
  coq.gref.list->set ML MS,
  std.forall ML (if-coverage-not-good-error.one MS).

pred if-coverage-not-good-error.one i:coq.gref.set, i:mixinname.
if-coverage-not-good-error.one MS M :- mixin-first-class M C, !,
  class-coverage [C] CMS,
  if (coq.gref.set.subset CMS MS)
     true
     (coq.gref.set.elements {coq.gref.set.remove M CMS} MissinFromCurrent,
      coq.error "HB: the first structure declared in this hierarchy containing" {nice-gref->string M} "is" {nice-gref->string C}
       "which also contains" {std.map MissinFromCurrent nice-gref->string} "."
       "\nThe are two ways to fix this problem:"
       "1) change the current structure to contain" {std.map MissinFromCurrent nice-gref->string} "as well;"
       "2) amend the hierarchy by declaring a structure before" {nice-gref->string C}
       "which contains at most" {std.map {coq.gref.set.elements {coq.gref.set.inter CMS MS}} nice-gref->string}).
if-coverage-not-good-error.one _ _. % new class is the first covering M

pred product->triples i:term, o:list (w-args factoryname), o:bool.
product->triples  {{ lib:hb.prod lp:A lp:B  }} L ClosureCheck :- !,
  product->triples B GRB ClosureCheck,
  product->triples A GRA _,
  std.append GRA GRB L.
product->triples {{ True }} [] tt :- !.
product->triples {{ False }} [] ff :- !.
product->triples A [GR] tt :- std.assert! (factory? A GR) "A structure can only mention known factories".

pred sigT->list-w-params i:term, o:list-w-params factoryname, o:bool.
sigT->list-w-params (fun N T B) L C :-
  coq.name->id N ID, % TODO: we should read the ID from the definition type which is an arity containing ids
  L = w-params.cons ID T Rest,
  @pi-decl N T p\
    sigT->list-w-params (B p) (Rest p) C.
sigT->list-w-params {{ lib:@hb.sigT _ lp:{{ fun N Ty B }} }} L C :-
  coq.name->id N ID, % TODO: we should read the ID from the definition type which is an arity containing ids
  L = w-params.nil ID Ty Rest,
  @pi-decl N Ty t\
    product->triples (B t) (Rest t) C.

}}