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

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

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

pred from_factory i:prop, o:factoryname.
from_factory (from X _ _) X.

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

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

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

pred mixin-src_src i:prop, o:term.
mixin-src_src (mixin-src _ _ S) S.

pred local-canonical-gref i:prop, o:constant.
local-canonical-gref (local-canonical C) C.

pred class_name i:class, o:classname.
class_name (class N _ _) N.

pred class_structure i:class, o:structure.
class_structure (class _ S _) S.

pred class-def_name i:prop, o:classname.
class-def_name (class-def (class N _ _)) N.

pred mixin-class_class i:prop, o:classname.
mixin-class_class (mixin-class _ C) C.

pred mixin-class_mixin i:prop, o:mixinname.
mixin-class_mixin (mixin-class M _) M.

pred classname->def i:classname, o:class.
classname->def CN (class CN S ML) :- class-def (class CN S ML).

pred classname->mixins i:classname, o:mixins.
classname->mixins CN MLwP :- class-def (class CN _ MLwP).

pred module-to-export_module i:prop, o:modpath.
module-to-export_module (module-to-export _ _ M) M.

pred module-to-export_module-nice i:prop, o:id.
module-to-export_module-nice (module-to-export _ M _) M.

pred instance-to-export_instance i:prop, o:constant.
instance-to-export_instance (instance-to-export _ _ M) M.

pred instance-to-export_instance-nice i:prop, o:id.
instance-to-export_instance-nice (instance-to-export _ M _) M.

pred abbrev-to-export_name i:prop, o:id.
abbrev-to-export_name (abbrev-to-export _ N _) N.
pred abbrev-to-export_body i:prop, o:term.
abbrev-to-export_body (abbrev-to-export _ _ B) (global B).

pred clause-to-export_clause i:prop, o:prop.
clause-to-export_clause (clause-to-export _ C) C.

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.

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

% [factory-provides F MLwP] computes the mixins MLwP generated by F
pred factory-provides i:factoryname, o:mixins.
factory-provides FactoryAlias MLwP :- std.do! [
  std.assert-ok! (factory-alias->gref FactoryAlias Factory) "HB",
  gref-deps Factory RMLwP,
  w-params.map RMLwP (factory-provides.base Factory) MLwP
].

pred mixin->factories i:mixinname, o:list factoryname.
mixin->factories M FL :- std.do! [
  std.findall (from F_ M B_) AllF,
  std.map AllF from_factory FL
].

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 T TyParams PL) "The conclusion of a builder is a mixin whose parameters depend on other mixins",
].

pred extract-conclusion-params i:term, i:term, o:list term.
extract-conclusion-params TheType (prod _ S T) R :- !,
  @pi-decl _ S x\ extract-conclusion-params TheType (T x) R.
extract-conclusion-params TheType (app [global GR|Args]) R :- !, std.do! [
  std.assert-ok! (factory-alias->gref GR Factory) "HB",
  factory-nparams Factory NP,
  std.map Args (copy-pack-holes TheType TheType) NewArgs,
  std.take NP NewArgs R].
extract-conclusion-params TheType T R :- whd1 T T1, !, extract-conclusion-params TheType 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:mixins.
factories-provide FLwP MLwP :- std.do! [
  list-w-params.flatten-map FLwP factory-provides UnsortedMLwP,
  w-params.map UnsortedMLwP (p\t\ toposort-mixins) MLwP,
].

pred undup-grefs  i:list gref, o:list gref.
undup-grefs  L UL :- std.do! [
  coq.gref.list->set L S,
  coq.gref.set.elements S UL,
].

pred undup-sorts i:list sort, o:list sort.
undup-sorts L R :- std.do! [

  if (std.mem L prop) (R1 = [prop]) (R1 = []),
  if (std.mem L sprop) (R2 = [sprop]) (R2 = []),
  if (std.mem L (typ _)) (R3 = [typ _]) (R3 = []),

  std.flatten [R1, R2, R3] R,
].

% also prunes cs-default
pred undup-cs-patterns  i:list cs-pattern, o:list cs-pattern.
undup-cs-patterns L R :- std.do! [
  std.map-filter L (x\r\ x = cs-gref r) LGR,
  undup-grefs LGR ULGR,
  std.map ULGR (x\r\ r = cs-gref x) R1,

  std.map-filter L (x\r\ x = cs-sort r) LS,
  undup-sorts LS ULS,
  std.map ULS (x\r\ r = cs-sort x) R2,

  if (std.mem L cs-prod) (R3 = [cs-prod]) (R3 = []),

  std.flatten [R1, R2, R3] R,
].

% Mixins can be topologically sorted according to their dependencies
pred toposort-mixins i:list (w-args mixinname), o:list (w-args mixinname).
toposort-mixins In Out :- std.do! [
  std.map In triple_1 ML,
  std.map ML (m\r\sigma D D1\ gref-deps m D1, list-w-params_list D1 D, std.map D (d\r\r = pr d m) r) ES2,
  std.flatten ES2 ES,
  toposort-proj triple_1 ES In Out,
].

pred toposort-proj i:(A -> gref -> prop), i:list (pair gref gref), 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 -> gref -> prop), i:list (pair gref gref), i:list gref, i:list A, o:list A.
toposort-proj.acc _ ES Acc [] Out :- !,
  std.map {std.gref.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 classname classname.
toposort-classes.mk-class-edge (sub-class C1 C2 _ _) (pr C2 C1).
pred toposort-classes i:list classname, o:list classname.
toposort-classes In Out :- std.do! [
  std.findall (sub-class C1_ C2_ _ _) SubClasses,
  std.map SubClasses toposort-classes.mk-class-edge ES,
  std.gref.toposort ES In Out,
].

pred findall-classes o:list class.
findall-classes CLSortedDef :- std.do! [
  std.findall (class-def C_) All,
  std.map All class-def_name CL,
  toposort-classes CL CLSorted,
  std.map CLSorted classname->def CLSortedDef,
].

pred findall-classes-for.unsorted
  i:list mixinname, i:list classname, o:list classname.
findall-classes-for.unsorted [] CL CL :- !.
findall-classes-for.unsorted [M|ML] CLAcc Out :- std.do! [
  std.findall (mixin-class M C_) All,
  std.map All mixin-class_class CL,
  findall-classes-for.unsorted ML {std.append CL CLAcc} Out
].

pred findall-classes-for i:list mixinname, o:list class.
findall-classes-for ML CLSortedDef :- std.do! [
  findall-classes-for.unsorted ML [] CL,
  toposort-classes CL CLSorted,
  std.map CLSorted classname->def CLSortedDef,
].

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

pred findall-has-mixin-instance i:cs-pattern,  o:list prop.
findall-has-mixin-instance P CL :-
   std.findall (has-mixin-instance P _ _) CL.

pred has-mixin-instance_key i:prop, o:cs-pattern.
has-mixin-instance_key (has-mixin-instance P _ _) P.

pred findall-mixin-src i:term, o:list mixinname.
findall-mixin-src T ML :-
  std.map {std.findall (mixin-src T M_ V_)} mixin-src_mixin ML.

pred findall-local-canonical o:list constant.
findall-local-canonical CL :-
  std.map {std.findall (local-canonical C_)} local-canonical-gref CL.

% [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 C1n C2n, fail) % a join, not a valid pair
       true, % no join, valid pair
  ].

pred assert-building-bottom-up i:class, i:classname, i:classname, i:classname.
assert-building-bottom-up CurrentClass C3n C1n C2n :-
  class-def (class C3n X Y),
  CurrentClass = class CC _ _,
  if (not (sub-class? CurrentClass (class C3n X Y)))
     (gref->modname CC 1 "." Before, gref->modname_short C3n "." After,
      gref->modname_short C1n "." C1nS, gref->modname_short C2n "." C2nS,
      Msg1 is "- declare structure " ^ Before ^ " before structure " ^ After ^ " if " ^ After ^ " inherits from it;",
      Msg2 is "- declare an additional structure that inherits from both "
        ^ C1nS ^ " and " ^ C2nS
        ^ " and from which " ^ Before ^ " and/or " ^ After ^ " inherit.",
      coq.error "You must declare the hierarchy bottom-up or add a missing join."
       "There are two ways out:"
       Msg1
       Msg2)
     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.

pred class-coverage i:list classname, o:coq.gref.set.
class-coverage CNL CSet :-
  std.map CNL classname->mixins CMLLwP,
  std.map CMLLwP list-w-params_list CMLL,
  coq.gref.list->set {std.flatten CMLL} CSet.

pred assert-good-coverage! i:list mixinname, i:list classname.
assert-good-coverage! MLSortedRev CNL :- std.do! [
  coq.gref.list->set MLSortedRev MLSet,
  class-coverage CNL CMLSet,
  if (not(coq.gref.set.equal MLSet CMLSet))
     (coq.gref.set.diff CMLSet MLSet Extra,
      coq.error "I could not find classes covering exactly mixins:"
        {std.any->string MLSortedRev}
        "In particular the covering" CNL "also includes mixins:"
        {coq.gref.set.elements Extra}
        "This should never happen, please report a bug.")
     true
].

%%%%% 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 S T (global F) :-
  coq.coercion.db-for (grefclass S) (grefclass T) L,
  if (L = [pr F _]) true (coq.error "No one step coercion from" S "to" T).

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

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

pred get-constructor i:gref, o:gref.
get-constructor (indt R) (indc K) :- !,
 if (coq.env.indt R _ _ _ _ [K] _) true (coq.error "Not a record" R).
get-constructor I _ :- coq.error "get-constructor: not an inductive" I.

% finding for locally defined structures
pred get-cs-structure i:cs-instance, o:structure.
get-cs-structure (cs-instance _ _ (const Inst)) Struct :- std.do! [
  coq.env.typeof (const Inst) InstTy,
  coq.prod-tgt->gref InstTy Struct,
  is-structure Struct,
].

pred get-cs-instance i:cs-instance, o:constant.
get-cs-instance (cs-instance _ _ (const Inst)) Inst.

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


pred mixin-src->has-mixin-instance i:prop, o:prop.
mixin-src->has-mixin-instance  (mixin-src (global GR) M I) (has-mixin-instance (cs-gref GR) M IHd) :-
  term->gref I IHd.

mixin-src->has-mixin-instance (mixin-src (app [global GR|_] ) M I) (has-mixin-instance (cs-gref GR) M IHd) :-
  term->gref I IHd.

mixin-src->has-mixin-instance (mixin-src (prod _ _ _ ) M I) (has-mixin-instance cs-prod M IHd):-
  term->gref I IHd.

mixin-src->has-mixin-instance (mixin-src (sort U) M I) (has-mixin-instance (cs-sort U) M IHd):-
  term->gref I IHd.

% this auxiliary function iterates over the list of arguments of an application,
% and create the necessary unify condition for each arguments
% and at the end returns the mixin-src clause with all the conditions
pred mixin-instance-type->mixin-src.aux
  i:list term, % list of arguments
  i:term, % head of the original application
  i:mixinname, % name of mixin
  i:term, % instance body
  i:list prop, % Cond list
  o:prop.
mixin-instance-type->mixin-src.aux [] T M I Cond (mixin-src T M I :- Cond).
mixin-instance-type->mixin-src.aux [A|Args] T M I Cond  (pi a \ C a) :-
  pi a \
  sigma Ta\
    coq.mk-app T [a] Ta,
    mixin-instance-type->mixin-src.aux Args Ta M I [coq.unify-eq A a ok|Cond] (C a).


% transforms the type of a mixin instance into a
% mixin-src clause with eventual conditions regarding its parameters
pred mixin-instance-type->mixin-src
  i:term, % type of the instance Ty
  i:mixinname, % name of mixin
  i:term, % instance body I of type Ty
  i:list prop, % Cond list
  o:prop.

mixin-instance-type->mixin-src (app _ as F) M I Cond C :-
  factory? F (triple _ _ Subject),
  safe-dest-app Subject Hd Args,
  mixin-instance-type->mixin-src.aux Args Hd M I Cond C.

mixin-instance-type->mixin-src (prod N_ _ F) M I Cond (pi a \ C a) :-
  pi a\
  sigma  Ia \
  coq.mk-app I [a] Ia,
    mixin-instance-type->mixin-src (F a) M Ia Cond (C a).

pred has-mixin-instance->mixin-src i:prop, o:prop.
has-mixin-instance->mixin-src (has-mixin-instance _ M IHd) C :- std.do![
  T = global IHd,
  coq.env.typeof IHd Ty,
  mixin-instance-type->mixin-src Ty M T [] C,
].

pred get-canonical-structures i:term, o:list structure.
get-canonical-structures TyTrm StructL :- std.do! [
  term->cs-pattern TyTrm Pat, !,
  coq.CS.db-for _ Pat DBGTyL,
  std.map-filter DBGTyL get-cs-structure StructL,
].

pred get-canonical-instances i:term, o:list constant.
get-canonical-instances TyTrm StructL :- std.do! [
  term->cs-pattern TyTrm Pat, !,
  coq.CS.db-for _ Pat DBGTyL,
  std.map-filter DBGTyL get-cs-instance StructL,
].

pred has-CS-instance? i:term, i:structure.
has-CS-instance? TyTerm (indt Struct) :- std.do! [
  term->cs-pattern TyTerm Pat,
  coq.env.projections Struct [some Proj, _],
  coq.CS.db-for (const Proj) Pat L,
  not(L = [])
].

pred structure-nparams i:structure, o:int.
structure-nparams Structure NParams :-
  class-def (class Class Structure _),
  factory-nparams Class NParams.

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

% [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 "HB: cannot find a class containing mixin" M.