/*        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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

func from_factory prop -> factoryname.
from_factory (from X _ _) X.

func from_mixin prop -> mixinname.
from_mixin (from _ X _) X.

func from_builder prop -> term.
from_builder (from _ _ X) (global X).

func mixin-src_mixin prop -> mixinname.
mixin-src_mixin (mixin-src _ M _) M.

func mixin-src_src prop -> term.
mixin-src_src (mixin-src _ _ S) S.

func local-canonical-gref prop -> constant.
local-canonical-gref (local-canonical C) C.

func class_name hbclass -> classname.
class_name (class N _ _) N.

func class_structure hbclass -> structure.
class_structure (class _ S _) S.

func class-def_name prop -> classname.
class-def_name (class-def (class N _ _)) N.

func mixin-class_class prop -> classname.
mixin-class_class (mixin-class _ C) C.

func mixin-class_mixin prop -> mixinname.
mixin-class_mixin (mixin-class M _) M.

func classname->def classname -> hbclass.
classname->def CN (class CN S ML) :- class-def (class CN S ML), !.

func classname->mixins classname -> mixins.
classname->mixins CN MLwP :- class-def (class CN _ MLwP), !.

func module-to-export_module prop -> modpath.
module-to-export_module (module-to-export _ _ M) M.

func module-to-export_module-nice prop -> id.
module-to-export_module-nice (module-to-export _ M _) M.

func instance-to-export_instance prop -> constant.
instance-to-export_instance (instance-to-export _ _ M) M.

func instance-to-export_instance-nice prop -> id.
instance-to-export_instance-nice (instance-to-export _ M _) M.

func abbrev-to-export_name prop -> id.
abbrev-to-export_name (abbrev-to-export _ N _) N.
func abbrev-to-export_body prop -> term.
abbrev-to-export_body (abbrev-to-export _ _ B) (global B).

func clause-to-export_clause prop -> prop.
clause-to-export_clause (clause-to-export _ C) C.

func extract-builder prop -> builder.
extract-builder (builder-decl B) B.

func leq-builder builder, builder ->.
leq-builder (builder N _ _ _) (builder M _ _ _) :- N =< M.

func sub-class? hbclass, hbclass ->.
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
func factory-provides factoryname -> 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
].

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

:index(1)
func factory-provides.base factoryname, list term, term,
  list (w-args mixinname) -> 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,
].

func factory-provides.one list term, term, term, mixinname -> 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",
].

func extract-conclusion-params term, term -> 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]]
func factories-provide list-w-params factoryname -> mixins.
factories-provide FLwP MLwP :-
  list-w-params.flatten-map FLwP factory-provides UnsortedMLwP,
  w-params.map UnsortedMLwP (p\t\ toposort-mixins) MLwP.

func undup-grefs list gref -> list gref.
undup-grefs  L UL :-
  coq.gref.list->set L S,
  coq.gref.set.elements S UL.

func undup-sorts list sort -> list sort.
undup-sorts L R :-

  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
func undup-cs-patterns  list cs-pattern -> list cs-pattern.
undup-cs-patterns L R :-
  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
func toposort-mixins list (w-args mixinname) -> list (w-args mixinname).
toposort-mixins In Out :-
  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.

func toposort-proj (func A -> gref), list (pair gref gref), list A -> list A.
toposort-proj Proj ES In Out :- !, toposort-proj.acc Proj ES [] In Out.
func topo-find B -> A.
func toposort-proj.acc (pred i:A, o:gref), list (pair gref gref), list gref, list A -> 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
func toposort-classes.mk-class-edge prop -> pair classname classname.
toposort-classes.mk-class-edge (sub-class C1 C2 _ _) (pr C2 C1).
func toposort-classes list classname -> 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,
].

func findall-classes -> list hbclass.
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,
].

func findall-classes-for.unsorted
  list mixinname, list classname -> 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
].

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

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

func findall-has-mixin-instance cs-pattern -> list prop.
findall-has-mixin-instance P CL :-
   std.findall (has-mixin-instance P _ _) CL.

func has-mixin-instance_key prop -> cs-pattern.
has-mixin-instance_key (has-mixin-instance P _ _) P.

func findall-mixin-src term -> list mixinname.
findall-mixin-src T ML :-
  std.map {std.findall (mixin-src T M_ V_)} mixin-src_mixin ML.

func findall-factory->constructor -> list prop.
findall-factory->constructor L :-
  std.map {std.findall (findall-factory->constructor.aux _)} findall-factory->constructor.make L.
func findall-factory->constructor.aux -> prop.
findall-factory->constructor.aux (factory->constructor F C) :-
  is-factory F, !, factory->constructor F C.
func findall-factory->constructor.make prop -> prop.
findall-factory->constructor.make (findall-factory->constructor.aux P) P.

func findall-local-canonical -> 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:hbclass, i:list hbclass, o:hbclass, o:hbclass.
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:hbclass, 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.

func distinct-pairs_pair prop -> pair hbclass hbclass.
distinct-pairs_pair (distinct-pairs-below _ _ X Y) (pr X Y).

func findall-newjoins hbclass, list hbclass -> list (pair hbclass hbclass).
findall-newjoins CurrentClass AllSuper TodoJoins :-
  std.findall (distinct-pairs-below CurrentClass AllSuper C1_ C2_) JoinOf,
  std.map JoinOf distinct-pairs_pair TodoJoins.

func class-coverage list classname -> 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.

func assert-good-coverage! list mixinname, 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
func get-structure-coercion structure, structure -> 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).

func get-structure-sort-projection structure -> 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.

func get-structure-class-projection structure -> 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.

func get-constructor gref -> 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
func get-cs-structure cs-instance -> 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,
].

func get-cs-instance cs-instance -> constant.
get-cs-instance (cs-instance _ _ (const Inst)) Inst.

func has-cs-instance gref, cs-instance ->.
has-cs-instance GTy (cs-instance _ (cs-gref GTy) _).


func mixin-src->has-mixin-instance prop -> 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
func mixin-instance-type->mixin-src.aux
  list term, % list of arguments
  term, % head of the original application
  mixinname, % name of mixin
  term, % instance body
  list prop % Cond list
  -> 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
:index (1)
func mixin-instance-type->mixin-src
  term, % type of the instance Ty
  mixinname, % name of mixin
  term, % instance body I of type Ty
  list prop % Cond list
  -> 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).

func has-mixin-instance->mixin-src prop -> 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,
].

func get-canonical-structures term -> 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,
].

func get-canonical-instances term -> list constant.
get-canonical-instances TyTrm StructL :-
  term->cs-pattern TyTrm Pat,
  coq.CS.db-for _ Pat DBGTyL,
  std.map-filter DBGTyL get-cs-instance StructL.

func has-CS-instance? term, structure ->.
has-CS-instance? TyTerm (indt Struct) :-
  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.

func factory? term -> 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.