param2.elpi

/* Binary parametricity translation                                          */
/* license: GNU Lesser General Public License Version 2.1 or later           */
/* ------------------------------------------------------------------------- */

% Author: Cyril Cohen

shorten std.{forall, forall2, do!, rev, map2, map}.

:before "subst-fun:fail"
coq.subst-fun XS T TXS :- !, coq.mk-app T XS TXS.

% this is outside the namespace since the predicate is also the db-one
param (sort prop as P) P (fun `s` P x\ fun `s` P y\ prod `s1` x _\ prod `s2` y _\ P) :- !.
param (sort _ as P) P
  (fun `u` (sort (typ U)) x\ fun `v` (sort (typ V)) y\ prod `s1` x _\ prod `s2` y _\ P) :- !,
  coq.univ.new [] U, coq.univ.new [] V.

param (fun N T B) (fun N T1 B1)
      (fun N T x\ fun N T1 x1\ fun N (TRsubst x x1) xR\ BR x x1 xR) :- !, do! [
  param T T1 TR,
  (pi x x1 xR\ param x x1 xR => param (B x) (B1 x1) (BR x x1 xR)),
  (TRsubst = x\ x1\ {coq.subst-fun [x,x1] TR})
].

param (prod N T P as Prod) Prod1 ProdR :- !, do! [
  param T T1 TR,
  (pi x x1 xR\ param x x1 xR => param (P x) (P1 x1) (PR x x1 xR)),
  Prod1 = prod N T1 P1,
  ProdR = fun `f` Prod f\ fun `g` Prod1 g\
       prod N T x\ prod N T1 x1\ prod N {coq.subst-fun [x,x1] TR} xR\
       {coq.subst-fun [{coq.mk-app f [x]}, {coq.mk-app g [x1]}] (PR x x1 xR)}
].

param (app [A|Bs]) (app [A1|Bs1]) ARBsR :- !, do! [
   param A A1 AR,
   derive.param2.param-args Bs Bs1 BsR,
   coq.mk-app AR BsR ARBsR
].

param (let N T V B) Let1 LetR :- !, do! [
  param T T1 TR,
  param V V1 VR,
  (pi x x1 xR\ param x x1 xR => param (B x) (B1 x1) (BR x x1 xR)),
  Let1 = let N T1 V1 B1,
  LetR = let N T V x\ let N T1 V1 x1\ let N {coq.mk-app TR [x,x1]} VR xR\ BR x x1 xR
].

param (match T P Bs) M1 MR :- !, do! [
  param T T1 TR,
  derive.param2.param-match P P1 PRM,
  param T T1 TR => derive.param2.map-param Bs Bs1 BsR,
  M1 = match T1 P1 Bs1,
  MR = match TR (PRM (x\ match x P Bs) (x\ match x P1 Bs1)) BsR
].

param (fix N Rno T F as Fix) Fix1 FixR :- !, do! [
  RnoR is 3 * Rno + 2, RnoR1 is RnoR + 1,
  param T T1 TR,
  (pi x x1 xR\ param x x1 xR => param (F x) (F1 x1) (FR x x1 xR)),
  Fix1 = fix N Rno T1 F1,
  (TRsubst = f\ f1\ {coq.subst-fun [f, f1] TR}),
  (pi f f1 xR\ FixBody f f1 xR =
     let N (TRsubst (F f) (F1 f1)) (FR f f1 xR) fr\
      {paramX.mk-trivial-match RnoR (TRsubst f f1) [] fr}),
  (pi f f1 xR\ coq.mk-eta RnoR1 (TRsubst f f1) (FixBody f f1 xR)
              (EtaFixBody f f1 xR)),
  FixR = (let N T Fix f\ let N T1 Fix1 f1\
          fix N RnoR (TRsubst f f1) xR\ EtaFixBody f f1 xR)
].

namespace derive.param2 {

pred param-args o:list term, o:list term, o:list term.
param-args [] [] [] :- !.
param-args [X|Xs] [X1|Xs1] [X,X1,XR|XsR] :- !,
  param X X1 XR, !, param-args Xs Xs1 XsR, !.

pred map-param o:list term, o:list term, o:list term.
map-param [] [] [] :- !.
map-param [X|Xs] [X1|Xs1] [XR|XsR]:- !,
  param X X1 XR, !, map-param Xs Xs1 XsR, !.


% helpers for match return type
pred param-match i:term, o:term, o:((term -> term) -> (term -> term) -> term).
param-match (fun N T B) P1 PRM :- pi x\ not (B x = fun _ _ _), !,
  param T T1 TR, !,
  (pi x x1 xR\ param x x1 xR => param (B x) (B1 x1) (BR x x1 xR)), !,
  P1 = fun N T1 B1,
  (pi z z1\ PRM z z1 = fun N T x\ fun N T1 x1\
                       fun N {coq.subst-fun [x,x1] TR} xR\
		       {coq.mk-app (BR x x1 xR) [z x, z1 x1]}).

param-match (fun N T B) P1 PRM :-
  param T T1 TR, !,
  (pi x x1 xR\ param x x1 xR => param-match (B x) (B1 x1) (BR x x1 xR)), !,
  P1 = fun N T1 B1,
  (pi z z1\ PRM z z1 = fun N T x\ fun N T1 x1\
                       fun N {coq.subst-fun [x,x1] TR} xR\
		       BR x x1 xR z z1).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% translation of inductive types %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

pred param-indt i:inductive, i:bool, i:int, i:int, i:term, i:list term, i:list term,
     i:inductive, o:bool, o:int, o:int, o:term, o:list term.
param-indt GR IsInd Lno _ Ty Knames Ktypes
 	   NameR IsInd LnoR LunoR TyR KtypesR :- do! [
  LnoR is 3 * Lno, LunoR = LnoR,
  param (global (indt GR)) (global (indt GR)) (global (indt NameR)) => do! [
    param Ty _ TyR,
    map2 Knames Ktypes param-indc KtypesR
  ]
].

pred rename-indc i:string, i:constructor, o:pair constructor id.
rename-indc Suffix GR (pr GR NameR) :-
  coq.gref->id (indc GR) Name,
  NameR is Name ^ Suffix.

pred param-indc i:term, i:term, o:term.
param-indc K T TRK :- !,
  param T _ TR, coq.subst-fun [K, K] TR TRK.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Class storage functions: %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%

pred store-param i:string, i:term, i:term, i:term.
store-param N X X1 XR :- !,
  Nparam is "param_" ^ N,
  Args = [_, _, _, X, X1, XR],
  T1 = app [{{ lib:@param2.store_param }}|Args],
  std.assert-ok! (coq.typecheck T1 T2) "store-param: T1 illtyped",
  coq.env.add-const Nparam T1 T2 _ C,
  @global! => coq.TC.declare-instance (const C) 0.

pred store-param-indc i:string, i:constructor, i:constructor.
store-param-indc Suffix K KR :-
  store-param {calc ({coq.gref->id (indc K)} ^ Suffix)}
    (global (indc K)) (global (indc K)) (global (indc KR)).

%%%%%%%%%%%%%%%%%%%%%%%
% toplevel predicates %
%%%%%%%%%%%%%%%%%%%%%%%

pred dispatch i:gref, i:string, o:list prop.

dispatch (const GR as C) Suffix Clauses :- do! [
  Term = global C,
  NameR is {coq.gref->id C} ^ Suffix,
  coq.env.const GR (some X) Ty,

  param Ty _ TyR,
  coq.mk-app TyR [Term, Term] TyRTermTerm,
  param X _ XR,
  % apparently calling the type checker with the expected type is weaker in this case
  std.assert-ok! (coq.typecheck XR XRTy) "param2: illtyped constant",
  std.assert-ok! (coq.unify-leq XRTy TyRTermTerm) "param2: constant does not have the right type",

  coq.env.add-const NameR XR TyRTermTerm _ TermR,

  store-param NameR Term Term (global (const TermR)),

  C1 = (param Term Term (global (const TermR)) :- !),
  coq.elpi.accumulate _ "derive.param2.db" (clause _ (before "param:fail") C1),
  C2 = (paramR Term Term (global (const TermR)) :- !),
  coq.elpi.accumulate _ "derive.param2.db" (clause _ (before "paramR:fail") C1),
  Clauses = [C1, C2]
].

dispatch (indt I as GR) Suffix Clauses :- do! [
  Ind = global GR,
  coq.env.indt I IsInd Lno Luno Ty Knames Ktypes,
  NameR is {coq.gref->id GR} ^ Suffix,
  map Knames (rename-indc Suffix) KnamesR,

  std.map Knames (k\r\ r = global (indc k)) Ks,
  pi new_name\ sigma KtypesR TyR\ (
      (param-indt I IsInd Lno Luno Ty Ks Ktypes
 	    	 new_name IsIndR LnoR LunoR TyR KtypesR),
    coq.build-indt-decl
      (pr new_name NameR) IsIndR LnoR LunoR {coq.subst-fun [Ind, Ind] TyR} KnamesR KtypesR DeclR
  ),

  std.assert-ok! (coq.typecheck-indt-decl DeclR) "derive.param2 generates illtyped term",

  coq.env.add-indt DeclR GRR,

  store-param NameR Ind Ind (global (indt GRR)),
  coq.env.indt GRR _ _ _ _ RealNamesR _,

  forall2 Knames RealNamesR (store-param-indc Suffix),

  C1 = (param Ind Ind (global (indt GRR)) :- !),
  coq.elpi.accumulate _ "derive.param2.db" (clause _ (before "param:fail") C1),
  C2 = (paramR Ind Ind (global (indt GRR)) :- !),
  coq.elpi.accumulate _ "derive.param2.db" (clause _ (before "paramR:fail") C2),
  map2 Knames RealNamesR (a\ b\ r\ r = param (global (indc a)) (global (indc a)) (global (indc b))) CK,
  forall CK (c\
    coq.elpi.accumulate _ "derive.param2.db" (clause _ (before "param:fail") c)),

 Clauses = [C1,C2|CK]
 ].

dispatch (indc _) _ _ :-
  coq.error "derive.param2: cannot translate a constructor".

pred main i:gref, i:string, o:list prop.
main T Out Clauses :- dispatch T Out Clauses.

}

/*

%%%%%%%%%%%%%%%%%%%%%
% Tactic entrypoint %
%%%%%%%%%%%%%%%%%%%%%

% We disable coq-refiner
:before "refiner-assign-evar"
  evar _ _ _ :- !.

pred ctx->TC i:(list prop), o:(list (pair term term)).
ctx->TC [] [] :- !.
ctx->TC [decl X _ Ty |Xs] [pr X Ty|Is] :- !, ctx->TC Xs Is.
ctx->TC [def X _ _ _ Ty |Xs] [pr X Ty|Is] :- !, ctx->TC Xs Is.

solve _ [goal Ctx Ev (app[{{@param}}, T, TR, X, XR]) _] _ :- !,
  coq.sigma.print,
  coq.say "goal->TC" {ctx->TC Ctx},
  coq.say "searching param for" X,
   (param T _ TR),
   (param X _ XR),
  Ev = app [{{@Param}}, T, TR, X, XR],
  coq.typecheck Ev Ty ok,
  coq.say "Ty=" Ty.

*/