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

namespace instance {

% [declare-existing T F] equips T with all the canonical structures that can be
% built using factory instance F
pred declare-existing i:argument, i:argument.
declare-existing T0 F0 :- std.do! [
  argument->ty T0 T, % TODO: change this when supporting morphism hierarchies
  argument->term F0 F,
  std.assert-ok! (coq.typecheck F FTy)
    "HB: declare-existing illtyped factory instance",
  std.assert! (coq.safe-dest-app FTy (global FactoryAlias) _)
     "The type of the instance is not a factory",
  std.assert-ok! (factory-alias->gref FactoryAlias Factory) "HB: ",
  private.declare-instance Factory T F Clauses _ _,
  acc-clauses current Clauses,
].

% [declare-const N B Ty CFL CSL] adds a Definition N : Ty := B where Ty is a factory
% and equips the type the factory is used on with all the canonical structures
% that can be built using factory instance B. CFL contains the list of
% factories being defined, CSL the list of canonical structures being defined.
pred declare-const i:id, i:term, i:arity, o:list (pair id constant), o:list (pair id constant).
declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [
  std.assert-ok! (coq.elaborate-arity-skeleton TyWPSkel _ TyWP) "Definition type illtyped",
  coq.arity->term TyWP Ty,
  std.assert-ok! (coq.elaborate-skeleton BodySkel Ty Body) "Definition illtyped",

  % handle parameters via a section -- begin
  if (TyWP = arity SectionTy) (
     % Do not open a section when it is not necessary (no parameters)
     % A side effect of opening a section is loosing meta data associated
     % with instances, in particular builder tags are lost
     if-verbose (coq.say  "HB: skipping section opening"),
     SectionBody = Body
   ) (
    std.assert! (coq.next-synterp-action (begin-section SectionName)) "synterp code did not open section",
    log.coq.env.begin-section SectionName,
    private.postulate-arity TyWP [] Body SectionBody SectionTy
  ),

  % identify the factory
  std.assert! (coq.safe-dest-app SectionTy (global FactoryAlias) Args) "The type of the instance is not a factory",
  std.assert-ok! (factory-alias->gref FactoryAlias Factory) "HB",
  std.assert! (factory-nparams Factory NParams) "Not a factory synthesized by HB",

  % declare the constant for the factory instance
  private.hack-section-discharging SectionBody SectionBodyHack,
  private.optimize-body SectionBodyHack OptimizedBody,
  if (Name = "_") (RealName is "HB_unnamed_factory_" ^ {std.any->string {new_int} }) (RealName = Name),

  % unfold local instances in the type of C
  if (current-mode (builder-from _ _ _ _)) (std.do![
    findall-local-canonical LocalCSL,
    coq.copy-clauses-for-unfold LocalCSL UnfoldClauses,
    UnfoldClauses => copy SectionTy SectionTyUnfolded,
  ]) (SectionTy = SectionTyUnfolded),

  % call HB.instance TheType TheFactory
  std.drop NParams Args [TheType|_],

  if (var TheType)
    (coq.error "HB: The instance subject must be explicitly given.\nUse:\n  HB.instance Definition _ : M <subject> := ...\n  HB.instance Definition _ := M.Build <subject> ...")
    true,

  log.coq.env.add-const-noimplicits-failondup RealName OptimizedBody
    SectionTyUnfolded @transparent! C,
  TheFactory = (global (const C)),

  private.check-non-forgetful-inheritance TheType Factory,

  private.declare-instance Factory TheType TheFactory Clauses CFL CSL,

  if (CSL = [])
     (coq.warning "HB" "HB.no-new-instance" "HB: no new instance is generated")
     true,

  % handle parameters via a section -- end
  if (TyWP = arity _) true (
    if-verbose (coq.say {header} "closing instance section"),
    log.coq.env.end-section-name SectionName
  ),

  % we accumulate clauses now that the section is over
  acc-clauses current Clauses
].

% [not-subclass-of X C] holds if C does not inherit from X
pred not-subclass-of i:classname, i:class.
not-subclass-of HasNoInstance (class C _ _) :- not(sub-class C HasNoInstance _ _).

% [declare-all T CL MCSTL] given a type T and a list of class definition
% CL in topological order (from least dep to most) looks for classes
% for which all the dependencies (mixins) were postulated so far and skips the
% rest. For each fulfilled class it declares a local constant inhabiting the
% corresponding structure and declares it canonical.
% Each mixin used in order to fulfill a class is returned together with its name.
pred declare-all i:term, i:list class, o:list (pair id constant).
declare-all _ [] [].
declare-all T [class _ Struct _|Rest] L :- has-instance T Struct, !,
  declare-all T Rest L.
declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :-

  infer-class T Class Struct MLwP S Name STy Clauses,

  !,

  decl-const-in-struct Name S STy CS,

  Clauses => declare-all T Rest L.

declare-all T [class HasNoInstance _ _|Rest] L :-
  % filter out classes we can't build for sure
  std.filter Rest (not-subclass-of HasNoInstance) Rest1,
  declare-all T Rest1 L.

% for generic types, we need first to instantiate them by giving them holes,
% so they can be used to instantiate the classes
pred declare-all-on-type-constructor i:term, i:list class, o:list (pair id constant).
declare-all-on-type-constructor _ [] [].
declare-all-on-type-constructor TK [class _ Struct _|Rest] L :- saturate-type-constructor TK T, has-instance T Struct, !,
  declare-all-on-type-constructor TK Rest L.
declare-all-on-type-constructor TK [class Class Struct MLwP|Rest] [pr Name CS|L] :-

  %TODO: compute the arity of the Class subject and saturate up to that point
  %      there may even be more than one possibility
  saturate-type-constructor TK T,

  infer-class T Class Struct MLwP S Name _STy Clauses,

  !,

  abstract-holes.main S SC,
  std.assert-ok! (coq.typecheck SC SCTy) "declare-all-on-type-constructor: badly closed",
  
  decl-const-in-struct Name SC SCTy CS,

  Clauses => declare-all-on-type-constructor TK Rest L.

declare-all-on-type-constructor TK [class HasNoInstance _ _|Rest] L :-
  % filter out classes we can't build for sure
  std.filter Rest (not-subclass-of HasNoInstance) Rest1,
  declare-all-on-type-constructor TK Rest1 L.

pred has-instance i:term, i:structure.
has-instance T Struct :-
  if (has-CS-instance? T Struct)
     (if-verbose (coq.say {header} "skipping already existing"
                    {nice-gref->string Struct} "instance on"
                    {coq.term->string T}))
     fail. % we build it

pred infer-class i:term, i:classname, i:gref, i:factories, o:term, o:string, o:term, o:list prop.
infer-class T  Class Struct MLwP S Name STy Clauses:- std.do![

  params->holes MLwP Params,
  get-constructor Class KC,

  if (synthesis.infer-all-args-let Params T KC KCApp ok)
     (if-verbose (coq.say {header} "we can build a" {nice-gref->string Struct} "on"
        {coq.term->string T}))
     fail,

  Name is {cs-pattern->name {term->cs-pattern T}}
    ^ "__canonical__" ^ {gref->modname Struct 2 "_" },

  if-verbose (coq.say {header} "declare canonical structure instance" Name),

  get-constructor Struct KS,
  coq.safe-dest-app T THD _,
  private.optimize-class-body THD {std.length Params} KCApp KCAppNames Clauses,
  coq.mk-app (global KS) {std.append Params [T, KCAppNames]} S,
  if-verbose (coq.say {header} "structure instance for" Name "is" {coq.term->string S}),

  coq.typecheck S STy ok, % failure may be due to a parameter not rich enough see #435
     
].

pred decl-const-in-struct i:string, i:term, i:term, i:constant.
decl-const-in-struct Name S STy CS:- std.do![

  if (ground_term S) (S1 = S, STy1 = STy)
    (abstract-holes.main S S1,
     std.assert-ok! (coq.typecheck S1 STy1) "HB: structure instance illtyped after generalizing over holes"),

  log.coq.env.add-const-noimplicits Name S1 STy1 @transparent! CS, % Bug coq/coq#11155, could be a Let
  with-locality (log.coq.CS.declare-instance CS), % Bug coq/coq#11155, should be local
  acc-clause current (local-canonical CS),
  if-verbose (coq.say {header} "structure instance" Name "declared"),
].


pred declare-factory-sort-deps i:gref.
declare-factory-sort-deps  GR :- std.do! [
  if-verbose (coq.say {header} "required instances on factory sort for" GR),
  Name is "SortInstances" ^ {std.any->string {new_int}},
  log.coq.env.begin-module Name none,
  log.coq.env.begin-section Name,
  mk-factory-sort-deps GR CSL,
  log.coq.env.end-section-name Name,
  log.coq.env.end-module-name Name _,
  std.forall CSL (x\ sigma CS\ x = pr _ CS, log.coq.CS.declare-instance CS)
].

pred declare-factory-sort-factory i:gref.
declare-factory-sort-factory GR :- std.do! [
  if-verbose (coq.say {header} "required instances on factory sort for" GR),
  Name is "SortInstances" ^ {std.any->string {new_int}},
  log.coq.env.begin-module Name none,
  log.coq.env.begin-section Name,
  mk-factory-sort-factory GR CFL CSL,
  log.coq.env.end-section-name Name,
  log.coq.env.end-module-name Name _,
  std.forall {std.append CFL CSL} (x\ sigma CS\ x = pr _ CS, log.coq.CS.declare-instance CS)
].

pred context.declare i:factories, o:mixins, o:list term, o:term, o:list prop, o:list constant.

pred mk-factory-sort-deps i:gref, o:list (pair id constant).
mk-factory-sort-deps AliasGR CSL :- std.do! [
  std.assert-ok! (factory-alias->gref AliasGR GR) "HB: mk-factory-sort-deps",
  gref-deps GR MLwPRaw,
  context.declare MLwPRaw MLwP SortParams SortKey SortMSL _,
  SortMSL => synthesis.infer-all-gref-deps SortParams SortKey GR FSort,
  log.coq.env.add-section-variable-noimplicits "f" FSort CF,
  GCF = global (const CF),
  factory-sort (coercion GRFSort _ GR _),
  SortMSL => synthesis.infer-all-gref-deps SortParams SortKey GRFSort KSort,
  coq.mk-app KSort [GCF] KFSortEta,
  list-w-params_list MLwP ML,
  std.length ML NMLArgs,
  coq.mk-n-holes NMLArgs SortMLHoles,
  std.append {std.append SortParams [SortKey|SortMLHoles]} [GCF] KFSortArgs,
  coq.mk-app (global GRFSort) KFSortArgs KFSort,
  std.assert-ok! (coq.unify-eq KFSortEta KFSort) "HB: KRSort not an app",
  std.map SortMSL
    (c\ o\ sigma m t\ c = mixin-src _ m t, o = mixin-src KFSort m t)
    KFSortMSL,
  KFSortMSL =>
    synthesis.under-mixin-src-from-factory.do! KFSort GCF
      [declare-all KFSort {findall-classes-for ML} CSL]
].

pred mk-factory-sort-factory i:gref, o:list (pair id constant), o:list (pair id constant).
mk-factory-sort-factory AliasGR CFL CSL :- std.do! [
  std.assert-ok! (factory-alias->gref AliasGR GR) "HB",
  gref-deps GR MLwPRaw,
  context.declare MLwPRaw MLwP SortParams SortKey SortMSL _,
  SortMSL => synthesis.infer-all-gref-deps SortParams SortKey GR FSort,
  log.coq.env.add-section-variable-noimplicits "f" FSort CF,
  std.length {list-w-params_list MLwP} NMLArgs,
  coq.mk-n-holes NMLArgs SortMLHoles,
  GCF = global (const CF),
  coq.mk-app (global GR) {std.append SortParams [GCF|SortMLHoles]} FGCF,
  declare-const "_" GCF (arity FGCF) CFL CSL
].

% create instances for all possible combinations of types and structure compatible 
pred saturate-instances i:cs-pattern.
saturate-instances Filter :- std.do! [

  findall-has-mixin-instance Filter ClausesHas,

  std.map ClausesHas has-mixin-instance_key KL,
  undup-cs-patterns KL UKL,
  std.map UKL cs-pattern->term TL,

  findall-classes AllClasses,

  std.map ClausesHas has-mixin-instance->mixin-src Clauses,
  
  Clauses => std.forall2 TL UKL (t\k\sigma Classes\
    std.filter AllClasses (no-instance-for k) Classes,
    declare-all-on-type-constructor t Classes _),
].

pred no-instance-for i:cs-pattern, i:class.
no-instance-for K (class _ S _) :-
  get-structure-sort-projection S (global Proj),
  coq.CS.db-for Proj K [].

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

namespace private {

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

pred declare-instance i:factoryname, i:term, i:term,
  o:list prop, o:list (pair id constant), o:list (pair id constant).
declare-instance Factory T F Clauses CFL CSL :-
  current-mode (builder-from T TheFactory FGR _), !,
  if (get-option "local" tt)
    (coq.error "HB: declare-instance: cannot make builders local.
    If you want temporary instances, make an alias, e.g. with let T' := T") true,
  !,
  declare-canonical-instances-from-factory-and-local-builders Factory
    T F TheFactory FGR Clauses CFL CSL.
declare-instance Factory T F Clauses CFL CSL :-
  declare-canonical-instances-from-factory Factory T F Clauses1 CFL CSL,
  if (get-option "export" tt)
     (coq.env.current-library File,
      std.map {std.append CFL CSL} (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) Clauses2)
     (Clauses2 = []),
     std.append Clauses1 Clauses2 Clauses.

% [add-mixin T F _ M Cl] adds a constant being the mixin instance for M on type
% T built from factory F
pred add-mixin i:term, i:factoryname, i:bool, i:mixinname,
  o:list prop, o:list (pair id constant).
add-mixin T FGR MakeCanon MissingMixin [MixinSrcCl, BuilderDeclCl] CSL :- std.do! [
  new_int N, % timestamp

  synthesis.assert!-infer-mixin T MissingMixin Bo,
  MixinSrcCl = mixin-src T MixinName (global (const C)),
  BuilderDeclCl = builder-decl (builder N FGR MixinName (const C)),

  std.assert-ok! (coq.typecheck Bo Ty) "declare-instances: mixin illtyped",
  safe-dest-app Ty (global MixinNameAlias) _,
  std.assert-ok! (factory-alias->gref MixinNameAlias MixinName) "HB",

  std.assert! (MissingMixin = MixinName) "HB: anomaly: we built the wrong mixin",

  % If the mixin instance is already a constant there is no need to
  % alias it.
  if (Bo = global (const C)) true
    (Name is {gref->modname FGR 2 "_"} ^"__to__" ^ {gref->modname MixinName 2 "_"},
     if-verbose (coq.say {header} "declare mixin instance" Name),
     log.coq.env.add-const-noimplicits Name Bo Ty @transparent! C),
  if (MakeCanon = tt, whd (global (const C)) [] (global (indc _)) _)
     (std.do! [
         if-verbose (coq.say {header} "declare canonical mixin instance" C),
         with-locality (log.coq.CS.declare-instance C),
         CSL = [pr "_" C]
     ]) (CSL = []),
].

pred add-all-mixins i:term, i:factoryname, i:list mixinname, i:bool,
  o:list prop, o:list (pair id constant).
add-all-mixins T FGR ML MakeCanon Clauses CSL :- std.do! [
  std.map ML (m\ o\ sigma ClL CSL\
    add-mixin T FGR MakeCanon m ClL CSL, o = pr ClL CSL) ClLxCSL_L,
  std.unzip ClLxCSL_L ClLL CSLL,
  std.flatten ClLL Clauses,
  std.flatten CSLL CSL
].

% [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, o:term.
postulate-arity (parameter ID _ S A) Acc T T1 Ty :-
  std.assert-ok! (coq.typecheck-ty S _) "arity parameter illtyped",
  if-verbose (coq.say {header} "postulating" ID),
  if (var S) (coq.fresh-type S) true,
  log.coq.env.add-section-variable-noimplicits ID S C,
  Var = global (const C),
  postulate-arity (A Var) [Var|Acc] T T1 Ty.
postulate-arity (arity Ty) ArgsRev X T Ty :-
  hd-beta X {std.rev ArgsRev} X1 Stack1,
  unwind X1 Stack1 T.


% We find the new mixins that F build, we build them and shedule them
% for becoming builders at section closing time. We also declare
% all canonical instances these new mixins allow for, so that the user
% can access their theory and notations
pred declare-canonical-instances-from-factory-and-local-builders
   i:factoryname, i:term, i:term, i:term, i:factoryname,
   o:list prop, o:list (pair id constant), o:list (pair id constant).
declare-canonical-instances-from-factory-and-local-builders
    Factory T F _TheFactory FGR Clauses CFL CSL :- std.do! [
  synthesis.under-new-mixin-src-from-factory.do! T F (NewMixins\ std.do! [
      add-all-mixins T FGR NewMixins ff Clauses CFL,
  ]),
  list-w-params_list {factory-provides Factory} ML,
  Clauses => declare-all T {findall-classes-for ML} CSL,
].

% [declare-canonical-instances-from-factory T F] given a factory F
% it uses all known builders to declare canonical instances of structures
% on T
pred declare-canonical-instances-from-factory
  i:factoryname, i:term, i:term, o: list prop, o:list (pair id constant), o:list (pair id constant).
declare-canonical-instances-from-factory Factory T F ClausesHas CFL CSL :- std.do! [
  % The order of the following two "under...do!"  is crucial,
  % priority must be given to canonical mixins
  % as they are the ones which guarantee forgetful inheritance
  % hence we add these clauses last.
  synthesis.under-mixin-src-from-factory.do! T F [
    synthesis.under-local-canonical-mixins-of.do! T [
      list-w-params_list {factory-provides Factory} ML,
      add-all-mixins T Factory ML tt Clauses CFL,
      std.map-filter Clauses (mixin-src->has-mixin-instance ) ClausesHas,
      ClausesHas => declare-all T {findall-classes-for ML} CSL, % declare-all-on-type-constructor doesn't work here
    ]
  ],
].

% If you don't mention the factory in a builder, then Coq won't make
% a lambda for it at section closing time.
pred hack-section-discharging i:term, o:term.
hack-section-discharging B B :- current-mode no-builder, !.
hack-section-discharging B B1 :- current-mode (builder-from _ TheFactory _ _), !,
  std.assert-ok! (coq.typecheck TheFactory TheFactoryTy) "TheFactory is illtyped (BUG)",
  B1 = {{ let _ : lp:TheFactoryTy := lp:TheFactory in lp:B }}.
hack-section-discharging B B.

% unfolds the constant used for the phant abbreviation to avoid storing all
% the phantom abstrctions and idfun that were used to trigger inference
pred optimize-body i:term, o:term.
optimize-body (app[global (const C)| Args]) Red :- (phant-abbrev _ (const C) _ ; (rex_match "phant_" {coq.gref->id (const C)})), !,
  coq.env.const C (some B) _,
  hd-beta B Args HD Stack,
  unwind HD Stack Red.
optimize-body (let _ _ T x\x) Red :- !, optimize-body T Red.
optimize-body X X.

pred hnf i:term, o:term.
hnf X R :- get-option "hnf" tt, !, unwind {whd X []} R.
hnf X X.

pred optimize-class-body i:term, i:int, i:term, o:term, o:list prop.
optimize-class-body T NParams (let _ _ MBo R) R1 Clauses :- std.do! [
  declare-mixin-name {hnf MBo} MC CL1,
  if (T = global (indt _), MC = global (const C), not(coq.env.opaque? C))
     (log.coq.strategy.set [C] (level 1000)) true, % opaque stops simpl
  optimize-class-body T NParams (R MC) R1 CL2,
  std.append CL1 CL2 Clauses,
].
optimize-class-body _ _ (app L) (app L) [].

pred declare-mixin-name i:term, o:term, o:list prop.
declare-mixin-name (global _ as T) T [].
declare-mixin-name T (global GR) [] :- mixin-mem T GR.
declare-mixin-name T T [] :- coq.safe-dest-app T (global GR) _, not (from _ _ GR), not (get-option "hnf" tt).
declare-mixin-name T (global (const C)) [mixin-mem T (const C)] :- std.do! [
  Name is "HB_unnamed_mixin_" ^ {std.any->string {new_int}},
  if-verbose (coq.say {header} "Giving name" Name "to mixin instance" {coq.term->string T}),
  log.coq.env.add-const-noimplicits Name T _ @transparent! C,
].

pred check-non-forgetful-inheritance i:term, i:gref.
check-non-forgetful-inheritance _ _ :-
  get-option "non_forgetful_inheritance" tt, !.
check-non-forgetful-inheritance T Factory :- std.do! [
  if (coq.safe-dest-app T (global (const HdSym)) _, structure-key HdSym _ Super) (
    coq.warning "HB" "HB.non-forgetful-inheritance"
      "non forgetful inheritance detected.\n"
      "You have two solutions:"
      "1. (Best practice) Reorganize your hierarchy to make"
      {nice-gref->string Factory}
      "depend on"
      { calc ({nice-gref->string Super} ^ ".") }
      "See the paper \"Competing inheritance paths in"
      "dependent type theory\" (https://hal.inria.fr/hal-02463336) for more"
      "explanations"
      "2. Use the attribute #[non_forgetful_inheritance] to disable this check."
      "We strongly advise you encapsulate this instance inside a module,"
      "in order to isolate it from the rest of the code, and to be able"
      "to import it on demand. See the above paper and the file"
      "https://github.com/math-comp/hierarchy-builder/blob/master/tests/non_forgetful_inheritance.v"
      "to witness devastating effects."
    ) true
].

}}