coq-lib.elpi

/* rocq-elpi: Coq terms as the object language of elpi                       */
/* license: GNU Lesser General Public License Version 2.1 or later           */
/* ------------------------------------------------------------------------- */

shorten std.{fatal-error, fatal-error-w-data, debug-print, unsafe-cast}.
shorten std.{rev, map, append, appendR, map2, forall-ok, take, do-ok!, lift-ok}.
shorten std.{ omap, take-last, intersperse, map-ok, string.concat }.

accumulate elpi_elpi/coq-lib-common.

:before "stop:begin"
stop S :- get-option "ltac:fail" N, !, coq.ltac.fail N S.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Helpers
%
% Pure LP code that works with the data types and API above.
% Named clauses are natural extension points, eg one can extend
% subst-prod to perform reduction in order to expose a "prod" node.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Term surgery %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

pred coq.subst-prod i:list term, i:term, o:term.
coq.subst-prod [] P P :- !.
coq.subst-prod [X|XS] (prod _ _ F) P :- !, coq.subst-prod XS (F X) P.
coq.subst-prod XS (let _ _ X F) P :- !, coq.subst-prod XS (F X) P.
:name "subst-prod:fail"
coq.subst-prod [_|_] T _ :- !,
  fatal-error-w-data "subst-prod: not a product" T.

pred coq.subst-fun i:list term, i:term, o:term.
coq.subst-fun [] T T :- !.
coq.subst-fun [X|XS] (fun _ _ F) T :- !, coq.subst-fun XS (F X) T.
coq.subst-fun XS (let _ _ X F) T :- !, coq.subst-fun XS (F X) T.
:name "subst-fun:fail"
coq.subst-fun [_|_] T _ :- !, 
  fatal-error-w-data "subst-fun: not a lambda" T.

pred coq.prod-R-fun o:term, o:term.
coq.prod-R-fun (prod N T F) (fun N T R) :- !, pi x\ coq.prod-R-fun (F x) (R x).
coq.prod-R-fun (let N T B F) (let N T B R) :- !, pi x\ coq.prod-R-fun (F x) (R x).
coq.prod-R-fun X X.

pred coq.prod->fun i:term, o:term.
coq.prod->fun (prod N T F) (fun N T R) :- !, pi x\ coq.prod->fun (F x) (R x).
coq.prod->fun (let N T B F) (let N T B R) :- !, pi x\ coq.prod->fun (F x) (R x).
coq.prod->fun X X.

pred coq.count-prods i:term, o:int.
coq.count-prods (prod N T B) C :- !,
  (@pi-decl N T x\ coq.count-prods (B x) C'), C is C' + 1.
coq.count-prods (let N T V B) C :- !,
  (@pi-def N T V x\ coq.count-prods (B x) C).
coq.count-prods T C :- !,
  coq.reduction.lazy.whd T Tr,
  if (T == Tr) (C = 0) (coq.count-prods Tr C).

pred coq.mk-n-holes  i:int, o:list A.
coq.mk-n-holes  0 [] :- !.
coq.mk-n-holes  N [HOLE_|R] :- !, M is N - 1, coq.mk-n-holes  M R.

pred coq.safe-dest-app i:term, o:term, o:list term.
coq.safe-dest-app (app [X|XS]) HD AllArgs :- !,
  coq.safe-dest-app X HD ARGS, append ARGS XS AllArgs.
coq.safe-dest-app X X [].

pred coq.mk-app i:term, i:list term, o:term.
coq.mk-app HD [] HD :- !.
coq.mk-app (app L) Args (app LArgs) :- !, append L Args LArgs.
coq.mk-app (fun _ _ F) [A|Args] R :- !, coq.mk-app (F A) Args R.
coq.mk-app (let _ _ A F) Args R :- !, coq.mk-app (F A) Args R.
coq.mk-app HD Args (app [HD|Args]).

pred coq.mk-app-uvar i:any, i:list term, o:term.
coq.mk-app-uvar HD [] HD :- !.
coq.mk-app-uvar (uvar as K) [A|Args] R :- !, unsafe-cast K K', coq.mk-app-uvar (K' A) Args R.

% coq.mk-eta n Ty T: performs up to n (when >= 0) eta expasion of T
% according to its type Ty. If n < 0 it makes as many step as
% products in Ty. There be dragons if T has not type Ty.
pred coq.mk-eta i:int, i:term, i:term, o:term.
coq.mk-eta 0 _ B B :- !.
coq.mk-eta N (prod Name Ty P) (fun _ _ F) (fun Name Ty F1) :- !, N1 is N - 1,
  pi x \ coq.mk-eta N1 (P x) (F x) (F1 x).
coq.mk-eta N (prod Name Ty P) B           (fun Name Ty B1) :- !, N1 is N - 1,
  pi x \ coq.mk-eta N1 (P x) {coq.mk-app B [x]} (B1 x).
:name "mk-eta:end"
coq.mk-eta _ _ B B :- !.

pred coq.saturate i:term, i:term, o:term.
coq.saturate Ty T O :- whd Ty [] (prod N Src Tgt) [], !,
  coq.mk-app T [Hole_] R,
  @pi-decl N Src x\ coq.saturate (Tgt x) R O.
coq.saturate _ X X.

% [copy A B] can be used to perform a replacement, eg
%   (copy (const "foo") (const "bar") :- !) => copy A B
% traverses A replacing foo with bar.
pred copy i:term, o:term.
:name "copy:start"
copy X Y :- name X, !, X = Y, !. % avoid loading "copy x x" at binders
copy (global _ as C) C :- !.
copy (pglobal _ _ as C) C :- !.
copy (sort _ as C) C :- !.
copy (fun N T F) (fun N T1 F1) :- !,
  copy T T1, pi x\ copy (F x) (F1 x).
copy (let N T B F) (let N T1 B1 F1) :- !,
  copy T T1, copy B B1, pi x\ copy (F x) (F1 x).
copy (prod N T F) (prod N T1 F1) :- !,
  copy T T1, (pi x\ copy (F x) (F1 x)).
copy (app L) (app L1) :- !, map L copy L1.
copy (fix N Rno Ty F) (fix N Rno Ty1 F1) :- !,
  copy Ty Ty1, pi x\ copy (F x) (F1 x).
copy (match T Rty B) (match T1 Rty1 B1) :- !,
  copy T T1, copy Rty Rty1, map B copy B1.
copy (primitive _ as C) C :- !.
copy (uvar M L as X) W :- var X, !, map L copy L1, coq.mk-app-uvar M L1 W.
% when used in CHR rules
copy (uvar X L) (uvar X L1) :- map L copy L1.

pred copy-ctx-item i:prop, o:prop.
copy-ctx-item (decl X N T) (decl X1 N T1) :- copy X X1, copy T T1.
copy-ctx-item (def X N T B) (def X1 N T1 B1) :-
  copy X X1, copy T T1, copy B B1.

pred copy-arity i:arity, o:arity.
copy-arity (parameter ID IMP T R) (parameter ID IMP T1 R1) :-
  copy T T1, pi x\ copy-arity (R x) (R1 x).
copy-arity (arity T) (arity T1) :- copy T T1.

pred copy-indt-decl i:indt-decl, o:indt-decl.
copy-indt-decl (parameter ID I Ty D) (parameter ID I Ty1 D1) :-
  copy Ty Ty1,
  @pi-parameter ID Ty1 x\ copy-indt-decl (D x) (D1 x).
copy-indt-decl (inductive ID CO A D) (inductive ID CO A1 D1) :-
  copy-arity A A1,
  @pi-inductive ID A1 i\ std.map (D i) copy-constructor (D1 i).
copy-indt-decl (record ID T IDK F) (record ID T1 IDK F1) :-
  copy T T1,
  copy-fields F F1.

pred copy-fields i:record-decl, o:record-decl.
copy-fields end-record end-record.
copy-fields (field Att ID T F) (field Att ID T1 F1) :-
  copy T T1,
  @pi-parameter ID T1 x\ copy-fields (F x) (F1 x).

pred copy-constructor i:indc-decl, o:indc-decl.
copy-constructor (constructor ID A) (constructor ID A1) :- copy-arity A A1.

pred fold-map i:term, i:A, o:term, o:A.
:name "fold-map:start"
fold-map X A Y A :- name X, !, X = Y, !. % avoid loading "fold-map x A x A" at binders
fold-map (global _ as C) A C A :- !.
fold-map (pglobal _ _ as C) A C A :- !.
fold-map (sort _ as C) A C A :- !.
fold-map (fun N T F) A (fun N T1 F1) A2 :- !,
  fold-map T A T1 A1, pi x\ fold-map (F x) A1 (F1 x) A2.
fold-map (let N T B F) A (let N T1 B1 F1) A3 :- !,
  fold-map T A T1 A1, fold-map B A1 B1 A2, pi x\ fold-map (F x) A2 (F1 x) A3.
fold-map (prod N T F) A (prod N T1 F1) A2 :- !,
  fold-map T A T1 A1, (pi x\ fold-map (F x) A1 (F1 x) A2).
fold-map (app L) A (app L1) A1 :- !, std.fold-map L A fold-map L1 A1.
fold-map (fix N Rno Ty F) A (fix N Rno Ty1 F1) A2 :- !,
  fold-map Ty A Ty1 A1, pi x\ fold-map (F x) A1 (F1 x) A2.
fold-map (match T Rty B) A (match T1 Rty1 B1) A3 :- !,
  fold-map T A T1 A1, fold-map Rty A1 Rty1 A2, std.fold-map B A2 fold-map B1 A3.
fold-map (primitive _ as C) A C A :- !.
fold-map (uvar M L as X) A W A1 :- var X, !, std.fold-map L A fold-map L1 A1, coq.mk-app-uvar M L1 W.
% when used in CHR rules
fold-map (uvar X L) A (uvar X L1) A1 :- std.fold-map L A fold-map L1 A1.

pred fold-map-ctx-item i:prop,  i:A, o:prop,o:A.
fold-map-ctx-item (decl X N T) A (decl X1 N T1) A2 :- fold-map X A X1 A1, fold-map T A1 T1 A2.
fold-map-ctx-item (def X N T B) A (def X1 N T1 B1) A3 :-
  fold-map X A X1 A1, fold-map T A1 T1 A2, fold-map B A2 B1 A3.

pred fold-map-arity i:arity,  i:A, o:arity, o:A.
fold-map-arity (parameter ID IMP T R) A (parameter ID IMP T1 R1) A2 :-
  fold-map T A T1 A1, pi x\ fold-map-arity (R x) A1 (R1 x) A2.
fold-map-arity (arity T) A (arity T1) A1 :- fold-map T A T1 A1.


% Bridges the gap between the data types used to read/write inductives.
% The arguments are the same of coq.env.indt plus an an extra one being
% the output (of type indt-decl).

pred coq.upoly-decl->attribute i:any, o:prop.
coq.upoly-decl->attribute (upoly-decl A B C D) (@udecl! A B C D).
coq.upoly-decl->attribute (upoly-decl-cumul A B C D) (@udecl-cumul! A B C D).

pred coq.upoly-decl.complete-constraints i:upoly-decl, o:upoly-decl.
coq.upoly-decl.complete-constraints (upoly-decl VS LV CS LC) (upoly-decl VS LV CS1 LC) :- std.do! [
  std.map VS coq.univ.variable.constraints ExtraL,
  std.flatten ExtraL Extra,
  std.filter Extra (c\not(std.mem CS c)) New,
  std.append CS New CS1,
].
pred coq.upoly-decl-cumul.complete-constraints i:upoly-decl-cumul, o:upoly-decl-cumul.
coq.upoly-decl-cumul.complete-constraints (upoly-decl-cumul VS LV CS LC) (upoly-decl-cumul VS LV CS1 LC) :- std.do! [
  std.map VS coq.upoly-decl-cumul.complete-constraints.aux ExtraL,
  std.flatten ExtraL Extra,
  std.filter Extra (c\not(std.mem CS c)) New,
  std.append CS New CS1,
].
pred coq.upoly-decl-cumul.complete-constraints.aux i:univ-variance, o:list univ-constraint.
coq.upoly-decl-cumul.complete-constraints.aux (auto V) CS :- coq.univ.variable.constraints V CS.
coq.upoly-decl-cumul.complete-constraints.aux (covariant V) CS :- coq.univ.variable.constraints V CS.
coq.upoly-decl-cumul.complete-constraints.aux (invariant V) CS :- coq.univ.variable.constraints V CS.
coq.upoly-decl-cumul.complete-constraints.aux (irrelevant V) CS :- coq.univ.variable.constraints V CS.


pred coq.build-indt-decl
  i:(pair inductive id), i:bool, i:int, i:int, i:term, i:list (pair constructor id), i:list term, o:indt-decl.

coq.build-indt-decl GR IsInd Pno UPno Arity Kns Ktys Decl :-
  coq.build-indt-decl-aux GR IsInd Pno UPno Arity Kns Ktys [] Decl.

pred coq.build-indt-decl-aux
  i:pair inductive id, i:bool, i:int, i:int, i:term, i:list (pair constructor id), i:list term, i:list term, o:indt-decl.
coq.build-indt-decl-aux (pr GR I) IsInd NUPno 0 Ty Kns KtysNu Params (inductive I IsInd Arity Ks) :- !,
  coq.term->arity Ty NUPno Arity,
  std.map KtysNu (k\coq.term->arity k NUPno) Ktys,
  rev Params ParamsR,
  (pi i\ Sub i = [ % we factor uniform parameters
    (pi x l\ copy (app[global (indt GR)|l]) (app[i|x]):- !, appendR ParamsR x l),
    (pi x l ui\ copy (app[pglobal (indt GR) ui|l]) (app[i|x]):- !, appendR ParamsR x l),
    (copy (global (indt GR)) i :- !),
    (pi ui\ copy (pglobal (indt GR) ui) i :- !) 
     ]),
  pi i\
    map2 Kns Ktys (gr_name\ ty\ res\
      sigma tmp name\
      (Sub i ==> copy-arity ty tmp),
      gr_name = pr _ name,
      res = constructor name tmp)
    (Ks i).

coq.build-indt-decl-aux GR IsInd Pno UPno (prod N S T) Kns Ktys Params (parameter NS explicit S Res) :- Pno > 0, UPno > 0, !,
  coq.name->id N NS,
  Pno1 is Pno - 1,
  UPno1 is UPno - 1,
  pi p\
    map Ktys (coq.subst-prod [p]) (Ktys1 p),
    coq.build-indt-decl-aux GR IsInd Pno1 UPno1 (T p) Kns (Ktys1 p) [p|Params] (Res p).

:name "coq.build-indt-decl-aux:fail"
coq.build-indt-decl-aux _ _ _ _ _ _ _ _ _ :- !,
  fatal-error "coq.build-indt-decl-aux: invalid declaration".

pred coq.rename-arity
  i:(id -> id -> prop),
  i:arity,
  o:arity.
coq.rename-arity RP (parameter ID I TY In) (parameter ID1 I TY Out) :-
  RP ID ID1,
  @pi-parameter ID TY p\
    coq.rename-arity RP (In p) (Out p).
coq.rename-arity _ (arity T) (arity T).

% [coq.rename-indt-decl RenameParam RenameIndType RenameIndConstr D D1]
% can be used to rename all [id] part of an inductive type declaration
pred coq.rename-indt-decl
  i:(id -> id -> prop),
  i:(id -> id -> prop),
  i:(id -> id -> prop),
  i:indt-decl, o:indt-decl.
coq.rename-indt-decl RP RI RK (parameter ID I TY In) (parameter ID1 I TY Out) :-
  RP ID ID1,
  @pi-parameter ID TY p\
    coq.rename-indt-decl RP RI RK (In p) (Out p).
coq.rename-indt-decl RP RI RK (inductive ID Ind A In) (inductive ID1 Ind A1 Out) :-
  RI ID ID1,
  coq.rename-arity RP A A1,
  coq.id->name ID Name,
  coq.arity->term A TY,
  @pi-decl Name TY i\
    std.map (In i) (coq.rename-indt-decl.aux RP RI RK) (Out i).
coq.rename-indt-decl _ RI RK (record ID A KID F) (record ID1 A KID1 F) :-
  RI ID ID1,
  RK KID KID1.

pred coq.rename-indt-decl.aux
  i:(id -> id -> prop),
  i:(id -> id -> prop),
  i:(id -> id -> prop),
  i:indc-decl, o:indc-decl.
coq.rename-indt-decl.aux RP _ RK (constructor ID A) (constructor ID1 A1) :-
  RK ID ID1,
  coq.rename-arity RP A A1.

pred coq.ensure-fresh-global-id i:string, o:string.
coq.ensure-fresh-global-id Exp S :-
  Name is Exp,
  coq.env.fresh-global-id Name S,
  if (Name = S) true
     (coq.warning "elpi" "elpi.renamed" "Global name" Name "is taken, using" S "instead").

% Lifts coq.typecheck to inductive declarations
pred coq.typecheck-indt-decl.heuristic-var-type i:term, o:diagnostic.
coq.typecheck-indt-decl.heuristic-var-type (uvar _ _ as X) D :- !,
  coq.univ.new U, coq.unify-eq X (sort (typ U)) D.
coq.typecheck-indt-decl.heuristic-var-type _ ok.

pred coq.typecheck-indt-arity i:arity, o:term, o:int, o:diagnostic.
coq.typecheck-indt-arity (parameter ID _ T D) (prod N T F) NU1 Diag :- do-ok! Diag [
  coq.typecheck-ty T _,
  (d\ @pi-parameter ID T x\ coq.typecheck-indt-arity (D x) (F x) NU d),
  lift-ok (NU1 is NU + 1) "",
  lift-ok (coq.id->name ID N) "",
].
coq.typecheck-indt-arity (arity T) T 0 Diag :- do-ok! Diag [
  coq.typecheck-ty T _,
  coq.typecheck-indt-decl.heuristic-var-type T,
].

pred coq.typecheck-indt-decl i:indt-decl, o:diagnostic.
coq.typecheck-indt-decl (parameter ID _ T Decl) Diag :- do-ok! Diag [
  coq.typecheck-ty T _,
  (d\ @pi-parameter ID T x\ coq.typecheck-indt-decl (Decl x) d),
].
coq.typecheck-indt-decl (inductive ID _ Arity KDecl) Diag :- do-ok! Diag [
  coq.typecheck-indt-arity Arity A NUPNO,
  d\ @pi-parameter ID A i\ forall-ok (KDecl i) (coq.typecheck-indt-decl-c i A NUPNO) d
].
coq.typecheck-indt-decl (record ID A _IDK FDecl) Diag :- do-ok! Diag [
  coq.typecheck-ty A _,
  d\ @pi-parameter ID A i\ do-ok! d [
    lift-ok (coq.typecheck-indt-decl-field i FDecl (K i)) "",
    coq.typecheck-indt-decl-c i A 0 (constructor "fields" (arity (K i)))
  ]
].

pred coq.typecheck-indc-arity i:arity, i:int, o:term, o:sort, o:diagnostic.
coq.typecheck-indc-arity A 0 T S Diag :- !,
  coq.arity->term A T,
  coq.typecheck-ty T S Diag.
coq.typecheck-indc-arity (parameter ID _ T D) NUPNO (prod N T F) S Diag :- do-ok! Diag [
  coq.typecheck-ty T _,
  lift-ok (NUPNO1 is NUPNO - 1) "",
  (d\ @pi-parameter ID T x\ coq.typecheck-indc-arity (D x) NUPNO1 (F x) S d),
  lift-ok (coq.id->name ID N) "",
].

pred coq.typecheck-indt-decl-c i:term, i:term, i:int, i:indc-decl, o:diagnostic.
coq.typecheck-indt-decl-c I S NUPNO (constructor _ID Arity) Diag :- do-ok! Diag [
  coq.typecheck-indc-arity Arity NUPNO T KS,
  coq.typecheck-indt-decl-c.unify-arrow-tgt I 0 S T,
  lift-ok (coq.arity->sort S IS) "",
  lift-ok (coq.sort.leq KS IS) "constructor universe too large"
].

pred coq.typecheck-indt-decl-c.unify-arrow-tgt i:term, i:int, i:term, i:term, o:diagnostic.
coq.typecheck-indt-decl-c.unify-arrow-tgt I P A (prod N S T) D :-
  @pi-decl N S x\ coq.typecheck-indt-decl-c.unify-arrow-tgt I P A (T x) D.
coq.typecheck-indt-decl-c.unify-arrow-tgt I P A (let N S B T) D :-
  @pi-def N S B x\ coq.typecheck-indt-decl-c.unify-arrow-tgt I P A (T x) D.
coq.typecheck-indt-decl-c.unify-arrow-tgt I P A Concl D :-
  coq.count-prods A N,
  coq.mk-n-holes  {calc (N + P)} Args,
  coq.mk-app I Args IArgs,
  coq.unify-eq Concl IArgs D.

pred coq.typecheck-indt-decl-field i:term, i:record-decl, o:term.
coq.typecheck-indt-decl-field I end-record I.
coq.typecheck-indt-decl-field I (field _ ID T F) (prod N T F1) :-
  coq.id->name ID N,
  @pi-decl N T a\ coq.typecheck-indt-decl-field I (F a) (F1 a).

% Lifts coq.elaborate-skeleton to inductive declarations
pred coq.elaborate-indt-decl-skeleton i:indt-decl, o:indt-decl, o:diagnostic.
coq.elaborate-indt-decl-skeleton (parameter ID Imp T Decl) (parameter ID Imp T1 Decl1) Diag :- do-ok! Diag [
  coq.elaborate-ty-skeleton T _ T1,
  (d\ @pi-parameter ID T1 x\ coq.elaborate-indt-decl-skeleton (Decl x) (Decl1 x) d),
].
coq.elaborate-indt-decl-skeleton (inductive ID I Arity KDecl) (inductive ID I Arity1 KDecl1) Diag :- do-ok! Diag [
  coq.elaborate-arity-skeleton Arity _ Arity1,
  lift-ok (coq.arity->nparams Arity1 NUPNO) "",
  d\ coq.arity->term Arity1 A1, do-ok! d [
       coq.typecheck-indt-decl.heuristic-var-type A1,
       d\ @pi-parameter ID A1 i\ map-ok (KDecl i) (coq.elaborate-indt-decl-skeleton-c i Arity1 NUPNO) (KDecl1 i) d
  ]
].
coq.elaborate-indt-decl-skeleton (record ID A IDK FDecl) (record ID A1 IDK FDecl1) Diag :- do-ok! Diag [
  coq.elaborate-ty-skeleton A _ A1,
  lift-ok (A1 = sort U) "record type is not a sort",
  d\ @pi-parameter ID A1 i\ coq.elaborate-indt-decl-skeleton-fields U FDecl FDecl1 d
].

pred coq.elaborate-indt-decl-skeleton-fields i:sort, i:record-decl, o:record-decl, o:diagnostic.
coq.elaborate-indt-decl-skeleton-fields _ end-record end-record ok.
coq.elaborate-indt-decl-skeleton-fields U (field Att ID A Fields) (field Att ID A1 Fields1) Diag :- do-ok! Diag [
  coq.elaborate-ty-skeleton A UA A1,
  lift-ok (coq.sort.leq UA U) "constructor universe too large",
  d\ @pi-parameter ID A1 p\
       coq.elaborate-indt-decl-skeleton-fields U (Fields p) (Fields1 p) d
].

pred coq.elaborate-indt-decl-skeleton-c i:term, i:arity, i:int, i:indc-decl, o:indc-decl, o:diagnostic.
coq.elaborate-indt-decl-skeleton-c I SA NUPNO (constructor ID Arity) (constructor ID Arity1) Diag :- do-ok! Diag [
  coq.elaborate-arity-skeleton-nuparams Arity NUPNO KS Arity1,
  coq.typecheck-indt-decl-c.unify-arity I 0 SA Arity1,
  lift-ok (coq.arity->sort {coq.arity->term SA} IS) "",
  lift-ok (coq.sort.leq KS IS) "constructor universe too large"
].

pred coq.typecheck-indt-decl-c.unify-arity i:term, i:int, i:arity, i:arity, o:diagnostic.
coq.typecheck-indt-decl-c.unify-arity I PNO (parameter _ _ T1 A) (parameter ID _ T C) D :- do-ok! D [
  coq.unify-eq T1 T,
  lift-ok (PNO1 is PNO + 1) "",
  d\ @pi-parameter ID T p\ coq.typecheck-indt-decl-c.unify-arity I PNO1 (A p) (C p) d
].
coq.typecheck-indt-decl-c.unify-arity I PNO (arity A) (parameter ID _ T C) D :-
  @pi-parameter ID T p\ coq.typecheck-indt-decl-c.unify-arity I PNO (arity A) (C p) D.
coq.typecheck-indt-decl-c.unify-arity I PNO (arity A) (arity C) D :-
  coq.typecheck-indt-decl-c.unify-arrow-tgt I PNO A C D.

% Lifts coq.elaborate-skeleton to arity
pred coq.elaborate-arity-skeleton i:arity, o:sort, o:arity, o:diagnostic.
coq.elaborate-arity-skeleton (parameter ID Imp T A) U3 (parameter ID Imp T1 A1) Diag :- do-ok! Diag [
  coq.elaborate-ty-skeleton T U1 T1,
  (d\ @pi-parameter ID T1 i\ coq.elaborate-arity-skeleton (A i) U2 (A1 i) d),
  lift-ok (coq.sort.pts-triple U1 U2 U3) "coq.elaborate-arity-skeleton: should not happen",
].
coq.elaborate-arity-skeleton (arity A) U (arity A1) Diag :-
  coq.elaborate-ty-skeleton A U A1 Diag.

pred coq.elaborate-arity-skeleton-nuparams i:arity, i:int, o:sort, o:arity, o:diagnostic.
coq.elaborate-arity-skeleton-nuparams (parameter ID Imp T A) 0 U3 (parameter ID Imp T1 A1) Diag :- !, do-ok! Diag [
  coq.elaborate-ty-skeleton T U1 T1,
  (d\ @pi-parameter ID T1 i\ coq.elaborate-arity-skeleton-nuparams (A i) 0 U2 (A1 i) d),
  lift-ok (coq.sort.pts-triple U1 U2 U3) "coq.elaborate-arity-skeleton-nuparams: should not happen",
].
coq.elaborate-arity-skeleton-nuparams (parameter ID Imp T A) N U (parameter ID Imp T1 A1) Diag :- do-ok! Diag [
  coq.elaborate-ty-skeleton T _ T1,
  lift-ok (M is N - 1) "",
  (d\ @pi-parameter ID T1 i\ coq.elaborate-arity-skeleton-nuparams (A i) M U (A1 i) d),
].
coq.elaborate-arity-skeleton-nuparams (arity A) _ U (arity A1) Diag :-
  coq.elaborate-ty-skeleton A U A1 Diag.

% Converts an arity to a term
pred coq.arity->term i:arity, o:term.
coq.arity->term (parameter ID _ Ty Rest) (prod Name Ty R) :-
  coq.id->name ID Name,
  @pi-decl Name Ty x\ coq.arity->term (Rest x) (R x).
coq.arity->term (arity A) A.

pred coq.term->arity i:term, i:int, o:arity.
coq.term->arity T 0 (arity T).
coq.term->arity (prod Name S T) N (parameter ID explicit S R) :-
  M is N - 1,
  coq.name->id Name ID,
  @pi-decl Name S x\ coq.term->arity (T x) M (R x).

% extracts the sort at the end of an arity
pred coq.arity->sort i:term, o:sort.
coq.arity->sort (prod N S X) Y :- !, @pi-decl N S x\ coq.arity->sort (X x) Y.
coq.arity->sort (let N T V X) Y :- !, @pi-def N T V x\ coq.arity->sort (X x) Y.
coq.arity->sort (sort X) X :- !.
coq.arity->sort X Y :- coq.reduction.lazy.whd X Xr, not (X == Xr), !,
  coq.arity->sort Xr Y.
coq.arity->sort T _ :- fatal-error-w-data "arity->sort: not a sort or prod" T.

% Counts how many parameters are there
pred coq.arity->nparams i:arity, o:int.
coq.arity->nparams (parameter _ _ _ In) O :-
  pi x\ coq.arity->nparams (In x) O1, O is O1 + 1.
coq.arity->nparams (arity _) 0.

% Prints an arity
pred coq.arity->pp o:arity, o:coq.pp.
coq.arity->pp (parameter ID Imp T Arity) (coq.pp.glue Res) :-
  Res = [coq.pp.box (coq.pp.hv 2)
           [coq.pp.str A, coq.pp.str ID,
            coq.pp.str " :", coq.pp.spc,TPP,coq.pp.str B],
         coq.pp.spc, Rest],
  if2 (Imp = explicit) (A = "(", B = ")")
      (Imp = maximal)  (A = "{", B = "}")
                       (A = "[", B = "]"),
  coq.term->pp T TPP,                       
  @pi-parameter ID T x\ coq.arity->pp (Arity x) Rest.
coq.arity->pp (arity T) (coq.pp.glue [coq.pp.str" : ",TPP]) :- coq.term->pp T TPP.

% Get impargs setting from an arity
pred coq.arity->implicits i:arity, o:list implicit_kind.
coq.arity->implicits (parameter Id I Ty F) [I|Is] :-
  @pi-parameter Id Ty x\ coq.arity->implicits (F x) Is.
coq.arity->implicits (arity _) [].

% Get impargs setting from an indt-decl
pred coq.indt-decl->implicits i:indt-decl, o:list implicit_kind, o:list (list implicit_kind).
coq.indt-decl->implicits (parameter Id I Ty F) [I|Is] R :-
  @pi-parameter Id Ty x\ coq.indt-decl->implicits (F x) Is R1,
  std.map R1 (l\r\r = [I|l]) R.
coq.indt-decl->implicits (record _ _ _ _) [] [[]].
coq.indt-decl->implicits (inductive Id _ A Ks) Is R :-
  coq.arity->implicits A Is,
  @pi-inductive Id A x\
    std.map (Ks x) (c\i\sigma a\c = constructor _ a,coq.arity->implicits a i) R.

% Check if some implicits are set
pred coq.any-implicit? i:list implicit_kind.
coq.any-implicit? L :- std.exists L (x\not(x = explicit)).

% extract gref from terms that happen to have one
pred coq.term->gref i:term, o:gref.
coq.term->gref (global GR) GR :- !.
coq.term->gref (pglobal GR _) GR :- !.
coq.term->gref (app [Hd|_]) GR :- !, coq.term->gref Hd GR.
coq.term->gref (let _ _ T x\x) GR :- !, coq.term->gref T GR.
coq.term->gref (primitive (proj Proj _)) (const C) :- coq.env.primitive-projection? Proj C _, !.
:name "term->gref:fail"
coq.term->gref Term _ :-
  fatal-error-w-data "term->gref: input has no global reference" Term.

pred coq.fresh-type o:term.
coq.fresh-type (sort (typ U)) :- coq.univ.new U.

pred coq.sort? i:term.
coq.sort? (sort _).
coq.sort? T :- whd1 T T1, coq.sort? T1.

% Map the term under a spine of fun nodes
pred coq.map-under-fun i:term,
  % InputTermUnderLams LamBoundVars TheirTypes Result
  i:(term -> list term -> list term -> term -> prop),
  o:term.
coq.map-under-fun T F R :- map-under-fun.aux T [] [] F R.

pred map-under-fun.aux i:term,
  i:list term, i:list term,
  i:(term -> list term -> list term -> term -> prop),
  o:term.
map-under-fun.aux (fun N T B) AccT AccTy F (fun N T R) :- !,
  @pi-decl N T x\ map-under-fun.aux (B x) [x|AccT] [T|AccTy] F (R x).
map-under-fun.aux (let N T X B) AccT AccTy F (let N T X R) :- !,
  @pi-def N T X x\ map-under-fun.aux (B x) AccT AccTy F (R x).
map-under-fun.aux End AccT AccTy F R :- F End {rev AccT} {rev AccTy} R.

pred coq.iter-under-fun i:term,
  % InputTermUnderLams LamBoundVars TheirTypes
  i:(term -> list term -> list term -> prop).
coq.iter-under-fun T F :- iter-under-fun.aux T [] [] F.

pred iter-under-fun.aux i:term,
  i:list term, i:list term,
  i:(term -> list term -> list term -> prop).
iter-under-fun.aux (fun N T B) AccT AccTy F :- !,
  @pi-decl N T x\ iter-under-fun.aux (B x) [x|AccT] [T|AccTy] F.
iter-under-fun.aux (let _ _ X B) AccT AccTy F :- !,
  iter-under-fun.aux (B X) AccT AccTy F.
iter-under-fun.aux End AccT AccTy F :- F End {rev AccT} {rev AccTy}.

% Build a match given the term and function to build the return type and the
% branches
pred coq.build-match
  i:term, % T, the term being matched
  i:term, % the type of T, expected to be an inductive, eventually applied
  % MkRty: IndSort LamBoundVars TheirTypes Result
  i:(term -> list term -> list term -> term -> prop),
  % MkBranch: Constructor ConstructorTyUnderLams LamBoundVars TheirTypes Result
  i:(term -> term -> list term -> list term -> term -> prop),
  o:term. % match T (.. MkRty) [ .. MkBranch K1, .. MkBranch K2, ..]
coq.build-match T Tty RtyF BranchF (match T Rty Bs) :-
  whd Tty [] HD Args,
  if2 (HD = global (indt GR)) true
      (HD = pglobal (indt GR) I) true
      fail,
  (@uinstance! I ==> coq.env.indt GR _ Lno _ Arity Kn Kt),
  take Lno Args LArgs,
  (@uinstance! I ==> coq.mk-app {coq.env.global (indt GR)} LArgs IndtLArgs),
  % Rty
  coq.subst-prod LArgs Arity ArityArgs,
  coq.bind-ind-arity-no-let IndtLArgs ArityArgs RtyF Rty,
  % Bs
  map Kt (coq.subst-prod LArgs) KtArgs,
  map KtArgs hd-beta-zeta-reduce KtArgsNorm,
  map KtArgsNorm coq.prod->fun KtArgsLam,
  map Kn (k\r\ sigma K\ coq.env.global (indc k) K, coq.mk-app K LArgs r) KnArgs,
  map2 KnArgs KtArgsLam (k\t\coq.map-under-fun t (BranchF k)) Bs.

% XXX the list of arguments are often needed in reverse order
pred coq.bind-ind-arity % calls K under (fun Arity (x : Ity Arity) =>..)
  i:term, % the inductive type
  i:term, % the arity
  i:(term -> list term -> list term -> term -> prop), % Sort Vars Tys Out
  o:term. %
pred coq.bind-ind-arity.aux 
  i:term,
  o:term,
  i:list term, i:list term, i:term,
  i:(term -> list term -> list term -> term -> prop).
coq.bind-ind-arity.aux (prod N T B) (fun N T F) AccT AccTy IT K :- !,
  @pi-decl N T x\ coq.bind-ind-arity.aux (B x) (F x) [x|AccT] [T|AccTy] IT K.
coq.bind-ind-arity.aux (let N T X B) (let N T X F) AccT AccTy IT K :- !,
  @pi-def N T X x\ coq.bind-ind-arity.aux (B x) (F x) AccT AccTy IT K.
coq.bind-ind-arity.aux (sort _ as Sort) (fun `i` ITy F) AccT AccTy IT K :-
  rev AccT Vars,
  coq.mk-app IT Vars ITy,
  @pi-decl `i` ITy x\ K Sort {append Vars [x]} {rev [ITy|AccTy]} (F x).
coq.bind-ind-arity IT Arity F R :- coq.bind-ind-arity.aux Arity R [] [] IT F.
% As above but let-ins are reduced
pred coq.bind-ind-arity-no-let i:term, i:term, i:(term -> list term -> list term -> term -> prop), o:term.
coq.bind-ind-arity-no-let IT Arity F R :-
  (pi N T X B F AccT AccTy IT K\
    coq.bind-ind-arity.aux (let N T X B) F AccT AccTy IT K :- !,
      coq.bind-ind-arity.aux (B X) F AccT AccTy IT K) =>
  coq.bind-ind-arity.aux Arity R [] [] IT F.
  
pred coq.bind-ind-parameters i:inductive, i:(term -> list term -> list term -> term -> prop), o:term.
coq.bind-ind-parameters I K O :-
  coq.env.indt I _ _ N A _ _,
  coq.bind-ind-parameters.aux N A [] [] K O.
pred coq.bind-ind-parameters.aux i:int, i:term, i:list term, i:list term, i:(term -> list term -> list term -> term -> prop), o:term.
coq.bind-ind-parameters.aux 0 Ty Vars Tys K O :- !, K Ty {std.rev Vars} {std.rev Tys} O.
coq.bind-ind-parameters.aux I (prod N T F) Vs Ts K (fun N T G) :- I > 0, !, J is I - 1,
  @pi-decl N T x\
    coq.bind-ind-parameters.aux J (F x) [x|Vs] [T|Ts] K (G x).
coq.bind-ind-parameters.aux I (let N T B F) Vs Ts K (fun N T G) :- I > 0, !, J is I - 1,
  @pi-def N T B x\
    coq.bind-ind-parameters.aux J (F x) [x|Vs] [T|Ts] K (G x).
coq.bind-ind-parameters.aux I T Vs Ts K O :- I > 0, whd1 T T', !,
  coq.bind-ind-parameters.aux I T' Vs Ts K O.

% coq.with-TC Class Instance->Clause Code: runs Code under a context augmented with
% all instances for Class transformed by Instance->Clause.
pred coq.with-TC i:term, i:(tc-instance -> prop -> prop), i:prop.
coq.with-TC Class Instance->Clause Code :-
  coq.TC.db-for {coq.term->gref Class} Instances,
  map Instances Instance->Clause Hyps, !,
  Hyps => Code.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

pred coq.replay-synterp-action i:synterp-action.
coq.replay-synterp-action (begin-module ID) :- coq.env.begin-module ID _.
coq.replay-synterp-action (end-module MP) :- coq.env.end-module MP.
coq.replay-synterp-action (begin-module-type ID) :- coq.env.begin-module-type ID.
coq.replay-synterp-action (end-module-type MTP) :- coq.env.end-module-type MTP.
coq.replay-synterp-action (apply-module-functor ID) :- coq.env.apply-module-functor ID _ _ _ _ _.
coq.replay-synterp-action (apply-module-type-functor ID) :- coq.env.apply-module-type-functor ID _ _ _ _.
coq.replay-synterp-action (include-module MP) :- coq.env.include-module MP _.
coq.replay-synterp-action (include-module-type MP) :- coq.env.include-module-type MP _.
coq.replay-synterp-action (import-module MP) :- coq.env.import-module MP.
coq.replay-synterp-action (export-module MP) :- coq.env.export-module MP.
coq.replay-synterp-action (begin-section ID) :- coq.env.begin-section ID.
coq.replay-synterp-action (end-section) :- coq.env.end-section.

pred coq.replay-next-synterp-actions.
coq.replay-next-synterp-actions :-
  coq.next-synterp-action Action, !,
  coq.replay-synterp-action Action, !,
  coq.replay-next-synterp-actions.
coq.replay-next-synterp-actions.