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

% This file implements a simple form of "type inference" for arguments which
% are mixins and can be inferred looking at the \lambda Prolog context, in
% particular [mixins-src] context entries (the one of Coq looks at CS databases
% and such, which cannot be easily manipulated on the fly).
%
% If provides function to infer this kind of arguments and to declare a context
% made of mixins to be used for such inference. The idea is that one has
% a bunch of mixins at hand and does want to pass them down to other terms,
% without explictly saying exactly where they should be used.

namespace synthesis {

% [infer-all-these-mixin-args Ps T ML F X] fills in all the arguments of F
% which are misxins in ML, abstracts the others
pred infer-all-these-mixin-args i:list term, i:term, i:list mixinname, i:term, o:term.
infer-all-these-mixin-args Ps T ML F SFX :- std.do! [
  std.assert-ok! (coq.typecheck F Ty) "try-infer-these-mixin-args: F illtyped",
  coq.mk-eta (-1) Ty F EtaF,
  coq.subst-fun {std.append Ps [T]} EtaF FT,
  private.instantiate-all-these-mixin-args FT T ML SFX,
].

% [infer-all-gref-deps Ps T GR X] fills in all the arguments of GR
% which are misxins in gref-deps GR, other arguments are abstracted
pred infer-all-gref-deps i:list term, i:term, i:gref, o:term.
infer-all-gref-deps Ps T GR X :- std.do! [
  std.assert! (gref-deps GR MLwP) "BUG: gref-deps should never fail",
  list-w-params_list MLwP ML,
  coq.env.typeof GR Ty,
  coq.mk-eta (-1) Ty (global GR) EtaF,
  coq.subst-fun {std.append Ps [T]} EtaF FT,
  private.instantiate-all-these-mixin-args FT T ML Xraw,
  infer-holes-depending-on-params T Xraw X,
].

% [infer-holes-depending-on-params TheType T NewT]
pred infer-holes-depending-on-params i:term, i:term, o:term.
infer-holes-depending-on-params T (app [global GR|Args]) (app [global GR|Args1]) :- !,
  std.map Args (infer-holes-depending-on-pack T) Args1.
infer-holes-depending-on-params _ X X.

pred class-of-phant i:term, o:gref, o:gref, o:gref.
class-of-phant (prod N T F) X Y Z :- @pi-decl N T x\ class-of-phant (F x) X Y Z.
class-of-phant (global GR) Y Z X :- class-def (class X GR _), get-constructor X Y, get-constructor GR Z.
class-of-phant (app[global GR|_]) Y Z X :- class-def (class X GR _), get-constructor X Y, get-constructor GR Z.

pred infer-holes-depending-on-pack i:term, i:term, o:term.
infer-holes-depending-on-pack T (app [global GR | Args]) S :-
  ((coq.gref->id GR GRS, rex.match "phant.*" GRS /*TODO: phant-clone? GR N*/);
    pack? GR _),
  coq.env.typeof GR Ty, class-of-phant Ty KC SC C,
  factory-nparams C N,
  std.take N Args Params, !,
  std.do! [
    infer-all-args-let Params T KC ClassInstance ok,
    std.rev [ClassInstance,T|{std.rev Params}] NewArgs,
    S = app[global SC| NewArgs ]
  ].
infer-holes-depending-on-pack _ X X.

% [infer-all-args-let Ps T GR X Diagnostic] fills in all the Args in
%   app[global GR, Ps, T | Args]
% and generates a term
%   let `a1` ty1 t1 a1\ .... app[global GR, p1, .. pn, T, a1, .. , an]
% if Diagnostic is ok, else X is unassigned
pred infer-all-args-let i:list term, i:term, i:gref, o:term, o:diagnostic.
infer-all-args-let Ps T GR X Diag :- std.do! [
  coq.env.typeof GR Ty,
  coq.mk-eta (-1) Ty (global GR) EtaF,
  coq.subst-fun {std.append Ps [T]} EtaF FT,
  private.instantiate-all-args-let FT T X Diag,
].


% [assert!-infer-mixin TheType M Out] infers one mixin M on TheType and
% aborts with an error message if the mixin cannot be inferred
pred assert!-infer-mixin i:term, i:mixinname, o:term.
assert!-infer-mixin T M B :-
  if (private.mixin-for T M B)
     true
     (coq.error "HB: cannot inhabit mixin"
       {nice-gref->string M} "on"{coq.term->string T}).

% Given TheType it looks all canonical structure instances on it and makes
% all their mixins available for inference
pred under-local-canonical-mixins-of.do! i:term, i:list prop.
under-local-canonical-mixins-of.do! T P :- std.do! [
  get-canonical-structures T CS,
  std.map CS (private.structure-instance->mixin-srcs T) MSLL,
  std.flatten MSLL MSL,
  MSL => std.do! P
].

% Given TheType and a factory instance (on it), makes all the mixins provided by
% the factory available for inference.
pred under-mixin-src-from-factory.do! i:term, i:term, i:list prop.
under-mixin-src-from-factory.do! TheType TheFactory LP :- std.do! [
  private.factory-instance->new-mixins [] TheFactory ML,
  std.map ML (m\c\ c = mixin-src TheType m TheFactory) MLClauses,
  MLClauses => std.do! LP
].

% Given TheType and a factory instance (on it), builds all the *new* mixins
% provided by the factory available for and passes them to the given
% continuation
pred under-new-mixin-src-from-factory.do! i:term, i:term, i:(list mixinname -> prop).
under-new-mixin-src-from-factory.do! TheType TheFactory LP :-
  findall-mixin-src TheType OldMixins,
  private.factory-instance->new-mixins OldMixins TheFactory NewML,
  std.map NewML (m\c\ c = mixin-src TheType m TheFactory) NewMLClauses,
  NewMLClauses => std.do! [ LP NewML ].

% [under-mixins.then MLwP Pred F] states that F has shape
%   fun p_1 .. p_k T,
%      (m_0 : M_0 ..p.. T) .. (m_n : M_n ..p.. T m_i0 .. m_ik) =>
%      Body m_0 .. m_n
% where  MLwP contains M_0, .., M_n (under p_1 .. p_k)
%   and  Body is such that [..,mixin-src T M_i m_i,..] => Pred Body
%   and  ..p.. is a list of terms built using p_1 .. p_k and T
pred under-mixins.then i:list (w-args mixinname),
    i:(name -> term -> (term -> A) -> A -> prop),
    i:(A -> prop), o:A.
under-mixins.then [] _ Pred Body :- !, Pred Body.
under-mixins.then [triple M Args T|ML] MkFun Pred Out :- std.do! [
  infer-all-gref-deps Args T M MTy,
  (@pi-decl `m` MTy m\ mixin-src T M m =>
    under-mixins.then ML MkFun Pred (Body m)),
  MkFun `m` MTy Body Out,
].

% [mixins-w-params.fun MLwP Pred F] states that F has shape
%   fun p_1 .. p_k T,
%      (m_0 : M_0 ..p.. T) .. (m_n : M_n ..p.. T m_i0 .. m_ik) =>
%      Body m_0 .. m_n
% where  MLwP contains M_0, .., M_n (under p_1 .. p_k)
%   and  Body is such that [..,mixin-src T M_i m_i,..] => Pred Body
%   and  ..p.. is a list of terms built using p_1 .. p_k and T
pred mixins-w-params.fun i:mixins, i:(list term -> term -> term -> prop), o:term.
mixins-w-params.fun L P Out :- !,
  w-params.then L mk-fun mk-fun (p\ t\ ml\ under-mixins.then ml mk-fun (P p t)) Out.

% [mixins-w-params.length LwP N] states N is Nmixins+Nparams
pred mixins-w-params.length i:mixins, o:int.
mixins-w-params.length MLwP N :-
  w-params.nparams MLwP Nparams,
  std.length {list-w-params_list MLwP} Nmixins,
  N is Nparams + Nmixins.

pred infer-coercion-tgt i:mixins, o:class.
infer-coercion-tgt (w-params.cons ID Ty F) CoeClass :-
  @pi-parameter ID Ty x\ infer-coercion-tgt (F x) CoeClass.
infer-coercion-tgt (w-params.nil _ {{ Type }} _) sortclass.
infer-coercion-tgt (w-params.nil _ {{ forall x, _ }} _) funclass. % do not use {{ _ -> _ }} since Funclass can be a dependent function!
infer-coercion-tgt (w-params.nil _ T _) (grefclass GR) :- coq.term->gref T GR.

pred w-args.check-key i:list term, i:term, i:list (w-args A), o:prop.
w-args.check-key _PS _T [] true :- !.
w-args.check-key  PS  T [triple _ _ T|LwA] P :- !, w-args.check-key PS  T LwA P.
w-args.check-key _PS _T _LwA false :- !, coq.error "HB: all mixins must have the same key".

pred list-w-params.check-key i:list-w-params A.
list-w-params.check-key MLwP :- !,
  w-params.then MLwP ignore ignore w-args.check-key _.

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

namespace private {

% [mixin-for T M MI] synthesizes an instance of mixin M on type T using
% the databases [mixin-src] and [from]
pred mixin-for i:term, i:mixinname, o:term.
mixin-for T M MICompressed :- mixin-src T M Tm, !, std.do! [
  %if-verbose (coq.say {header} "Trying to infer mixin for" M),
  std.assert-ok! (coq.typecheck Tm Ty) "mixin-for: Tm illtyped",

%%%%% mterm %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  factory? Ty (triple Factory Params _),

  if (M = Factory) (MI = Tm) (
      private.builder->term Params T Factory M B,
      coq.subst-fun [Tm] B MI
  ),

  %if-verbose (coq.say {header} "Trying to compress mixin for" {coq.term->string MI}),
  compress-coercion-paths MI MICompressed,
].

pred drop i:int, i:list A, o:list A.
drop 0 L L :- !.
drop N [_|XS] L :- !, N1 is N - 1, drop N1 XS L.

pred compress-copy o:term, o:term.
compress-copy (app [global (const C) | L]) R :-
  sub-class C2 C3 C NparamsC,
  drop NparamsC L [app [global (const C') | L']],
  sub-class C1 C2 C' NparamsC',
  drop NparamsC' L' L'',
  sub-class C1 C3 C'' NparamsC'',
  std.append {coq.mk-n-holes NparamsC''} L'' HL'',
  CHL'' = app [global (const C'') | HL''],
  coq.typecheck CHL'' _ ok, !,
  compress-copy CHL'' R.
compress-copy (app L) (app L1) :- !, std.map L compress-copy L1.
compress-copy X X.


pred compress-coercion-paths i:term, o:term.
compress-coercion-paths MI MICompressed :-
  if (get-option "compress_coercions" tt)
     (compress-copy MI MICompressed)
     (MI = MICompressed).

pred mixin-for_mixin-builder i:prop, o:term.
mixin-for_mixin-builder (mixin-for _ _ B) B.

% [builder->term Params TheType Src Tgt MF] finds a builder from Src to Tgt
% and fills in all the mixins required by the builder using mixin-src, obtaining
% a function (MF = Builder Params TheType InferredStuff : Src -> Tgt)
pred builder->term i:list term, i:term, i:factoryname, i:mixinname, o:term.
builder->term Ps T Src Tgt B :- !, std.do! [
  from Src Tgt FGR,
  F = global FGR,
  gref-deps Src MLwP,
  list-w-params_list MLwP ML,
  infer-all-these-mixin-args Ps T ML F B,
].

% [instantiate-all-these-mixin-args T F M_i TFX] where mixin-for T M_i X_i states that
% if    F  ~  fun xs (m_0 : M_0 T) .. (m_n : M_n T ..) ys
%            => F xs m_0 .. m_{i-1} m_i m_{i+1} .. m_n ys
% then TFX := fun xs m_0 .. m_{i-1}     m_{i+1} .. m_n ys
%            => F xs m_0 .. m_{i-1} X_i m_{i+1} .. m_n ys
% thus instanciating an abstraction on mixin M_i with X_i
pred instantiate-all-these-mixin-args i:term, i:term, i:list mixinname, o:term.
instantiate-all-these-mixin-args (fun _ Tm F) T ML R :-
  coq.safe-dest-app Tm (global TmGR) _,
  factory-alias->gref TmGR M ok,
  std.mem! ML M,
  !,
  if (mixin-for T M X) true (coq.error "HB: Unable to find mixin" {nice-gref->string M} "on subject" {coq.term->string T}), !,
  instantiate-all-these-mixin-args (F X) T ML R.
instantiate-all-these-mixin-args (fun N Ty F) T ML (fun N Ty FX) :- !,
  @pi-decl N Ty m\ instantiate-all-these-mixin-args (F m) T ML (FX m).
instantiate-all-these-mixin-args F _ _ F.

pred instantiate-all-args-let i:term, i:term, o:term, o:diagnostic.
instantiate-all-args-let (fun N Tm F) T (let N Tm X R) Diag :- !, std.do! [
  coq.safe-dest-app Tm (global TmGR) _,
  factory-alias->gref TmGR M ok,
  if (mixin-for T M X)
     (@pi-def N Tm X m\ instantiate-all-args-let (F m) T (R m) Diag)
     (Diag = error Msg,
      Msg is "cannot synthesize mixin " ^ {nice-gref->string M} ^
             " for " ^ {coq.term->string T}),
].
instantiate-all-args-let F _ F ok.

% [structure-instance->mixin-srcs TheType Structure] finds a CS instance for
% Structure on TheType (if any) and builds mixin-src clauses for all the mixins
% which can be candidates from that class instance. It finds instances which are
% concrete, that is not by projecting a rich type (a variable) to its class.
pred structure-instance->mixin-srcs i:term, i:structure, o:list prop.
structure-instance->mixin-srcs T S MSLC :- std.do! [
  structure-key SortProj _ S,
  class-def (class (indt Class) S CMLwP),
  structure-nparams S NParams,
  coq.mk-n-holes NParams Holes,
  std.append Holes [ST] HolesST,
  coq.mk-app (global (const SortProj)) HolesST SortHolesST,
  % find an instance in ST
  coq.unify-eq T SortHolesST ok,
  % we look for an instance which is concrete, we take the parts
  get-constructor S KS,
  coq.mk-app (global KS) {std.append Holes [T, CT]} KSHolesC,
  coq.unify-eq ST KSHolesC ok,
  % if the class instance is concrete, we take the parts
  get-constructor (indt Class) KC,
  std.length {list-w-params_list CMLwP} CMixinsN,
  coq.mk-n-holes CMixinsN MIL,
  coq.mk-app (global KC) {std.append Holes [T | MIL]} CBody,
  coq.unify-eq CT CBody ok,
  % we finally generare micin-src clauses for all mixins
  std.map MIL (structure-instance->mixin-srcs.aux T) MSLL,
  std.flatten MSLL MSLC,
].
% this catch all sucks a bit, but is very relevant. Some instance, like
% unification hints (canonical coercions) which require a type which is too rich
% fail the second unif problem
structure-instance->mixin-srcs _ _ [].

structure-instance->mixin-srcs.aux2 Params T Class (some P) M :-
  coq.mk-app (global (const P)) {std.append Params [T,Class]} M.
structure-instance->mixin-srcs.aux T  F CL :-
  factory-instance->new-mixins [] F ML,
  std.map ML (m\c\ c = mixin-src T m F) CL.

% [factory-instance->new-mixins OldMixins FI MSL] find all the mixins
% which can be generated by the factory instance FI which are not part of
% OldMixins (that is, the contribution of FI to the current context)
pred factory-instance->new-mixins i:list mixinname, i:term, o:list mixinname.
factory-instance->new-mixins OldMixins X NewML :- std.do! [
  std.assert-ok! (coq.typecheck X XTy) "mixin-src: X illtyped",
  if (not (coq.safe-dest-app XTy (global _) _))
     (coq.error "Term:\n" {coq.term->string X}
                "\nhas type:\n" {coq.term->string XTy}
                "\nwhich is not a record")
     true,
  coq.term->gref XTy Src,
  factory-provides Src MLwP,
  list-w-params_list MLwP ML,
  std.filter ML (m\ not(std.mem! OldMixins m)) NewML,
].

}}