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

namespace factory {

pred declare i:argument.
declare A :- private.declare-asset A private.asset-factory.

pred declare-mixin i:argument.
declare-mixin A :- private.declare-asset A private.asset-mixin.

kind factory-abbrev type.
type by-classname gref -> factory-abbrev.
type by-phantabbrev abbreviation -> factory-abbrev.

pred declare-abbrev i:id, i:factory-abbrev, o:abbreviation.
declare-abbrev Name (by-classname GR) Abbrev :-
  % looks fishy (the parameters are not taken into account)
  @global! => log.coq.notation.add-abbreviation Name 1 (fun _ _ t\ app[global GR,t]) tt Abbrev.
declare-abbrev Name (by-phantabbrev Abbr) Abbrev :- std.do! [
  coq.notation.abbreviation-body Abbr Nargs AbbrTrm,
  @global! => log.coq.notation.add-abbreviation Name Nargs AbbrTrm tt Abbrev,
].

pred argument->w-mixins i:argument, o:w-mixins argument.
argument->w-mixins (indt-decl Decl) (pr MLwP ArgwP) :- !, std.do! [
  pdecl->w-mixins Decl (pr MLwP DeclwP),
  w-params.map DeclwP (_\ _\ x\ y\ y = indt-decl x) ArgwP
].
argument->w-mixins (const-decl Id none Decl) (pr MLwP ArgwP) :- !, std.do! [
  pdecl->w-mixins Decl (pr MLwP DeclwP),
  w-params.map DeclwP (_\ _\ x\ y\ y = const-decl Id none x) ArgwP,
].
argument->w-mixins (const-decl Id (some Body) Decl as CDecl)
    (pr MLwP ArgwP) :- !, std.do! [
  if-verbose (coq.say {header} "arguments->w-mixins on const-decl Decl=" CDecl),
  pdecl->w-mixins Decl (pr MLwP DeclwP),
  if-verbose (coq.say {header} "arguments->w-mixins on const-decl Decl=" Decl
    "\nwith MLwP =" MLwP),
  std.length {list-w-params_list MLwP} NML,
  if-verbose (coq.say "ML length =" NML),
  w-params.map DeclwP (ps\ t\ x\ y\ sigma Dummies Args AppBody\ std.do! [
    std.nlist NML (sort prop) Dummies,
    std.append ps [t|Dummies] Args,
    coq.subst-fun Args Body AppBody,
    y = const-decl Id (some AppBody) x]) ArgwP
].
argument->w-mixins (ctx-decl Decl) (pr MLwP ArgwP) :- !, std.do! [
  cdecl->w-mixins Decl (pr MLwP DeclwP),
  w-params.map DeclwP (_\ _\ x\ y\ y = ctx-decl x) ArgwP
].

pred argument-name i:argument, o:string.
argument-name (const-decl Id _ _) Id :- !.
argument-name (indt-decl (parameter _ _ _ R)) Id :- !,
argument-name (indt-decl (R (sort prop))) Id.
argument-name (indt-decl (record Id _ _ _)) Id :- !.
argument-name (indt-decl (inductive Id _ _ _)) Id :- !.
argument-name (ctx-decl _) "_" :- !.

pred pdecl->w-mixins i:indt-decl, o:w-mixins indt-decl.
pred pdecl->w-mixins i:arity, o:w-mixins arity.
pdecl->w-mixins (parameter ID _ TySkel Rest as Decl) Out :-
  private.is-key Decl, !,
  private.key-decl-w-mixins "parameter"
    ID TySkel Rest private.pdecl->w-mixins.mixins Out.
pdecl->w-mixins (parameter ID _ TySkel Rest) Out :- !,
  private.param-decl-w-mixins "parameter"
    ID TySkel Rest pdecl->w-mixins Out.
pdecl->w-mixins _ _ :- !,
  coq.error "HB: declaration must have at least one parameter".

pred cdecl->w-mixins i:context-decl, o:w-mixins context-decl.
cdecl->w-mixins (context-item _ _ _ (some _) _) _ :- !,
  coq.error "HB: local definition is not supported in this context".
cdecl->w-mixins (context-item ID _ TySkel none Rest as Decl) Out :-
  private.is-key Decl, !,
  private.key-decl-w-mixins "context-item"
    ID TySkel Rest private.cdecl->w-mixins.mixins Out.
cdecl->w-mixins (context-item ID _ TySkel none Rest) Out :- !,
  private.param-decl-w-mixins "context-item"
    ID TySkel Rest cdecl->w-mixins Out.
cdecl->w-mixins _ _ :- !,
  coq.error "HB: declaration must have at least one parameter".

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

namespace private {

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

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

pred check-key-attribute-consistency i:id.
check-key-attribute-consistency _ :- not(get-option "key" _), !.
check-key-attribute-consistency ID :- get-option "key" ID, !.
check-key-attribute-consistency ID :- get-option "key" ID1,
  coq.error "HB:" {calc ("The #[key=\"" ^ ID1 ^ "\"] attribute")}
    "does not match the selected subject" ID.

pred is-key i:indt-decl.
pred is-key i:arity.
pred is-key i:context-decl.
is-key (parameter ID _ _ _\ record _ _ _ _) :- !, check-key-attribute-consistency ID.
is-key (parameter ID _ _ _\ inductive _ _ _ _) :- !, check-key-attribute-consistency ID.
is-key (parameter ID _ _ _\ arity _) :- !, check-key-attribute-consistency ID.
is-key (context-item ID _ _ _ _\ context-end) :- !, check-key-attribute-consistency ID.
is-key (parameter ID _ _ _) :- get-option "key" ID, !.
is-key (context-item ID _ _ _ _) :- get-option "key" ID, !.
is-key (parameter ID _ _ p\ parameter _ _ (M p) _) :-
  pi p\ factory? (M p) _, !, check-key-attribute-consistency ID.
is-key (context-item ID _ _ _ p\ context-item _ _ (M p) _ _) :-
  pi p\ factory? (M p) _, !, check-key-attribute-consistency ID.

pred mixin-decl-w-mixins i:string, i:string, i:term, i:(term -> A),
  i:(A -> pair (list (w-args mixinname)) A -> prop),
  o:pair (list (w-args mixinname)) A.
mixin-decl-w-mixins DeclKind ID TySkel Rest Conv Out :- std.do! [
  if-verbose (coq.say {header} "processing mixin" DeclKind ID),
  std.assert! (not (var TySkel)) "HB: no type provided for mixin",
  disable-id-phant TySkel TySkelNoId,
  std.assert-ok! (coq.elaborate-ty-skeleton TySkelNoId _ TyNoId)
    "HB: mixin illtyped",
  re-enable-id-phant TyNoId Ty,
  std.assert! (factory? Ty (triple F Ps T))
    "HB: Not a factory applied to the key variable",
  std.assert! (pi x y\ Rest y = Rest x)
    "HB: Factories cannot be explicitly mentioned in the subsequent declaration",
  Dummy = sort prop, Conv (Rest Dummy) (pr MLwA R),
  Out = pr [triple F Ps T|MLwA] R
].
pred key-decl-w-mixins i:string, i:string, i:term, i:(term -> A),
  i:(A -> pair (list (w-args mixinname)) A -> prop),
  o:pair mixins (w-params A).
key-decl-w-mixins DeclKind ID TySkel Rest Conv Out :- std.do! [
  if-verbose (coq.say {header} "processing key" DeclKind),
  std.assert-ok! (coq.elaborate-ty-skeleton TySkel _ Ty) "key illtyped",
  coq.string->name ID N, @pi-decl N Ty t\ Conv (Rest t) (pr (MLwA t) (R t)),
  if (var Ty) (fresh-type Ty) true,
  Out = pr (w-params.nil ID Ty MLwA) (w-params.nil ID Ty R)
].
pred param-decl-w-mixins i:string, i:string, i:term, i:(term -> A),
  i:(A -> pair mixins (w-params A) -> prop), o:pair mixins (w-params A).
param-decl-w-mixins DeclKind ID TySkel Rest Conv Out :- std.do! [
  if-verbose (coq.say {header} "processing param" DeclKind),
  std.assert-ok! (coq.elaborate-ty-skeleton TySkel _ Ty) "param illtyped",
  coq.string->name ID N, @pi-decl N Ty p\ Conv (Rest p) (pr (MLwP p) (R p)),
  if (var Ty) (fresh-type Ty) true,
  Out = pr (w-params.cons ID Ty MLwP) (w-params.cons ID Ty R)
].

pred pdecl->w-mixins.mixins i:indt-decl,
  o:pair (list (w-args mixinname)) indt-decl.
pred pdecl->w-mixins.mixins i:arity,
  o:pair (list (w-args mixinname)) arity.
pdecl->w-mixins.mixins (parameter ID _ TySkel Rest) Out :- !,
  mixin-decl-w-mixins "parameter" ID TySkel Rest pdecl->w-mixins.mixins Out.
pdecl->w-mixins.mixins R (pr [] R) :- !.

pred cdecl->w-mixins.mixins i:context-decl,
  o:pair (list (w-args mixinname)) context-decl.
cdecl->w-mixins.mixins context-end (pr [] context-end) :- !.
cdecl->w-mixins.mixins (context-item _ _ _ (some _) _) _ :- !,
  coq.error "HB: local definition is not supported in this context".
cdecl->w-mixins.mixins (context-item ID _ TySkel none Rest) Out :- !,
  mixin-decl-w-mixins "parameter" ID TySkel Rest cdecl->w-mixins.mixins Out.

% The identity builder
pred declare-id-builder i:factoryname, o:prop.
declare-id-builder GR (from GR GR (const C)) :- std.do! [
  gref-deps GR GRD,
  synthesis.mixins-w-params.fun GRD (declare-id-builder.aux GR) IDBodySkel,
  std.assert-ok! (coq.elaborate-skeleton IDBodySkel IDType IDBody) "identity builder illtyped",
  log.coq.env.add-const-noimplicits "identity_builder" IDBody IDType @transparent! C,
].
declare-id-builder.aux GR Params TheType (fun `x` Ty x\x) :-
  synthesis.infer-all-gref-deps Params TheType GR Ty.

% [mk-factory-abbrev Str GR CL FactAbbrev]
% creates an abbreviation for GR names Str and creates a phant-abbrev clause in CL.
% FactAbbrev is the short name for the factory (either an alias of the class record)
pred mk-factory-abbrev i:string, i:gref, o:list prop, o:factory-abbrev.
mk-factory-abbrev Str GR Aliases FactAbbrev :- !, std.do! [
  if (factory-alias->gref GR _ ok)
     (Aliases = [],
      FactAbbrev = by-classname GR)
     (phant.of-gref ff GR [] PhTerm,
      phant.add-abbreviation Str PhTerm PhC Abbrv,
      Aliases = [phant-abbrev GR (const PhC) Abbrv],
      FactAbbrev = by-phantabbrev Abbrv),
].

% [declare-asset Asset AssetKind] unifies the code paths for
% mixins, factories (and alias factories)
pred declare-asset i:argument, i:asset.
declare-asset Arg AssetKind :- std.do! [
  argument-name Arg Module,
  if-verbose (coq.say {header} "start module and section" Module),
  log.coq.env.begin-module Module none,
  log.coq.env.begin-section Module,

  if-verbose (coq.say {header} "converting arguments" Arg "to factories"),
  argument->w-mixins Arg (pr FLwP ArgwP),

  if-verbose (coq.say {header} "converting factories" FLwP "to mixins"),
  %%% factories-provide FLwP MLwP,

  if-verbose (coq.say {header} "declaring context" FLwP),
  context.declare FLwP MLwP Params TheKey MixinSrcClauses SectionCanonicalInstance,

  if (Arg = indt-decl _) (
    apply-w-params ArgwP Params TheKey (indt-decl (record _ Sort _ Fields)),
    if-verbose (coq.say {header} "declare mixin or factory"),
    declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
      Params TheKey Sort Fields MLwP Module AssetKind
  ) (
    apply-w-params ArgwP Params TheKey (const-decl _ (some Sort) _),
    if-verbose (coq.say {header} "declare factory alias"),
    declare-factory-alias MixinSrcClauses SectionCanonicalInstance
      Params TheKey Sort MLwP Module
  )
].

pred declare-mixin-or-factory i:list prop, i:list constant, i:list term, i:term,
  i:term, i:record-decl, i:list-w-params factoryname, i:id, i:asset.
declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
    TheParams TheType Sort1 Fields GRFSwP Module D :- std.do! [

  if-verbose (coq.say {header} "declare record axioms_"),
  Kname = "Axioms_",
  RDeclSkel = record "axioms_" Sort1 Kname Fields,
  std.assert-ok! (coq.elaborate-indt-decl-skeleton RDeclSkel RDecl) "record declaration illtyped",

  abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-indt-decl RDecl RDeclClosed _,


  if (get-option "primitive" tt)
    (@primitive! => log.coq.env.add-indt RDeclClosed R)
    (log.coq.env.add-indt RDeclClosed R),

  log.coq.env.end-section-name Module, % We need to anyway declare the record inside the section
    % since closing the section purges the unused universe level we may have
    % allocated by typechecking the skeleton just above

  coq.env.indt R tt _ _ _ [K] _,
  GRK = indc K,
  @global! => log.coq.arguments.set-implicit (indt R) [[]],
  @global! => log.coq.arguments.set-implicit GRK [[]],

  factories-provide GRFSwP MLwP,
  w-params.nparams MLwP NParams,
  build-deps-for-projections R MLwP GRDepsClausesProjs,
  GRDepsClauses = [gref-deps (indt R) MLwP, gref-deps (indc K) MLwP|GRDepsClausesProjs],

  % GRDepsClauses => mk-factory-sort MLwP (indt R) _ FactorySortCoe,
  % FactorySortCoe = coercion GRFSort _ _ _,

  % TODO: should this be in the Exports module?

  if-verbose (coq.say {header} "declare notation Build"),

  GRDepsClauses => phant.of-gref ff GRK [] PhGRK,
  GRDepsClauses => phant.add-abbreviation "Build" PhGRK BuildConst BuildAbbrev,

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

  if (D = asset-mixin)
     ((GRDepsClauses => mk-factory-abbrev "axioms" (indt R) FRClauses FactAbbrev),
      (GRDepsClauses => FRClauses => declare-id-builder (indt R) IdBuilderClause),
      Clauses = [IdBuilderClause|FRClauses])
     (GRDepsClauses => mk-factory-abbrev "axioms" (indt R) Clauses FactAbbrev),

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

  log.coq.env.begin-module "Exports" none,
  std.flatten [Clauses, GRDepsClauses, [
    factory-constructor (indt R) GRK,
    factory-nparams (indt R) NParams,
    factory-builder-nparams BuildConst NParams,
    phant-abbrev GRK (const BuildConst) BuildAbbrev,
    % gref-deps GRFSort MLwP,
    % factory-sort FactorySortCoe,
  ]] NewClauses,
  acc-clauses current NewClauses,

  list-w-params_list MLwP MLwoP,
  std.map MLwoP (_\ r\ r = maximal) Implicits,
  /* std.map {list-w-params_list MLwP} (_\ r\ r = maximal) Implicits, */
  @global! => log.coq.arguments.set-implicit GRK [[maximal|Implicits]],
  % @global! => log.coq.coercion.declare FactorySortCoe,

  % NewClauses => instance.declare-factory-sort-deps (indt R),

  log.coq.env.end-module-name "Exports" Exports,
  log.coq.env.end-module-name Module _,

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

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

  GRDepsClauses => declare-abbrev Module FactAbbrev _,
].


pred declare-factory-alias  i:list prop, i:list constant, i:list term, i:term,
  i:term, i:list-w-params factoryname, i:id.
declare-factory-alias MixinSrcClauses SectionCanonicalInstance
    TheParams TheType Ty1Skel GRFSwP Module :- std.do! [

  if-verbose (coq.say {header} "declare constant axioms_"),
  std.assert-ok! (coq.elaborate-ty-skeleton Ty1Skel _ Ty1) "Illtyped alias factory",

  abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-const-decl (pr Ty1 _) (pr Ty1Closed _) Section,
  log.coq.env.add-const-noimplicits "axioms_" Ty1Closed _ @transparent! C,

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

  MixinSrcClauses => synthesis.infer-all-gref-deps 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]) (app[global (const C)|Section])) => copy MFKTy MFKTyC,

  abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-const-decl (pr MFK MFKTyC) (pr MFKClosed MFKTyCClosed) _,
  log.coq.env.add-const-noimplicits "Axioms_" MFKClosed MFKTyCClosed @transparent! CK,

  GRK = const CK,

  log.coq.env.end-section-name Module,

  @global! => log.coq.arguments.set-implicit GRK [[]],

  factories-provide GRFSwP MLwP,
  GRDepsClauses = [gref-deps (const C) MLwP, gref-deps (const CK) MLwP],

  GRDepsClauses => phant.of-gref ff GRK [] PhGRK0,

  % GRDepsClauses => mk-factory-sort MLwP (const C) _ FactorySortCoe,
  % FactorySortCoe = coercion GRFSort _ _ _,

  if (mixin-first-class F _) (PhGRK = PhGRK0)
    (phant.append-fun-unify PhGRK0 PhGRK),
  GRDepsClauses => phant.add-abbreviation "Build" PhGRK BuildConst _,

  GRDepsClauses => mk-factory-abbrev "axioms" (const C) Clauses FactAbbrev,

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

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

  w-params.nparams MLwP NParams,
  std.flatten [ Clauses, GRDepsClauses,
      [ factory-nparams (const C) NParams,
        factory-constructor (const C) GRK,
        factory-builder-nparams BuildConst NParams,
        % gref-deps GRFSort MLwP,
        % factory-sort FactorySortCoe
      ]
    ] NewClauses,

  acc-clauses current NewClauses,
  %@global! => log.coq.coercion.declare FactorySortCoe,

  % NewClauses => instance.declare-factory-sort-deps (const C),

  log.coq.env.end-module-name "Exports" Exports,
  log.coq.env.end-module-name Module _,

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

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

  GRDepsClauses => declare-abbrev Module FactAbbrev _,
].

% [build-deps-for-projections I ML CL] builds a [gref-dep] for each projection P
% of I such that P depends on "ML @ [I]" (each operation depends on the the
% deps of the record plus the record itself)
pred build-deps-for-projections i:inductive, i:mixins, o:list prop.
build-deps-for-projections R MLwP CL :- std.do! [
  compat.map-filter {coq.env.projections R} (x\y\x = some y) MixinOps,
  list-w-params.rcons MLwP (pl\t\r\ r = triple (indt R) pl t) MLRwP,
  std.map MixinOps (gr\r\ r = gref-deps (const gr) MLRwP) CL,
].

% Section handling in Coq is smart, in the sense it it only abstracts over
% variables that aoccur. We don't want that for mixin/factories, so we implement
% our own discharging. Note that definitions (like canonical instance) have
% to be abstracted too.
pred abstract-over-section i:list term, i:term, i:list prop, i:list constant, i:(list constant -> A -> A -> prop), i:A, o:A, o:list term.
abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance F X X1 Section :-
  % compute section variables to be used for discharging
  std.map MixinSrcClauses mixin-src_src Mixins,
  std.append TheParams [TheType|{std.rev Mixins}] Section,
  std.map Section (x\r\ x = global (const r)) SectionVars,
  % We discharge by hand the record declaration so that we can be sure all
  % parameters and mixins are abstracted (even if unused).
  coq.copy-clauses-for-unfold SectionCanonicalInstance CopyUnfold,
  CopyUnfold => F SectionVars X X1.

pred mk-factory-sort i:mixins, i:gref, o:gref, o:coercion.
mk-factory-sort MLwP GR (const FactorySortCst) Coe :-
  if-verbose (coq.say {header} "declaring tagged sort for GR=" GR),
  synthesis.mixins-w-params.fun MLwP (mk-factory-sort.term GR) FactorySort,
  std.assert-ok! (coq.typecheck FactorySort FactorySortTy) "HB: cannot elaborate sort",
  log.coq.env.add-const-noimplicits "sort" FactorySort FactorySortTy ff FactorySortCst,
  synthesis.mixins-w-params.length MLwP MLwPLength,
  std.nlist {calc (MLwPLength + 1)} implicit MLwPImplicits,
  (@global! => log.coq.arguments.set-implicit (const FactorySortCst) [MLwPImplicits]),
  synthesis.infer-coercion-tgt MLwP CoeClass,
  Coe = coercion (const FactorySortCst) MLwPLength GR CoeClass.
pred mk-factory-sort.term i:gref, i:list term, i:term, o:term.
mk-factory-sort.term GR P T (fun `_` Ty _\ T) :- synthesis.infer-all-gref-deps P T GR Ty.



}}