elpi_elaborator.elpi

/* Type inference and unification                                            */
/* license: GNU Lesser General Public License Version 2.1 or later           */
/* ------------------------------------------------------------------------- */

shorten std.{rev, append, ignore-failure!, mem, map2, split-at, map, assert!}.

% Entry points
pred unify-eq i:term, i:term.
pred unify-list-eq i:list term, i:list term.
pred unify-leq i:term, i:term.
pred of i:term, o:term, o:term. % of Term Type(i/o) RefinedTerm

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%% Reduction %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:before "hd-beta:end"
hd-beta (uvar as K) [A|AS] X C :- !, % auto-intro
  assert! (of A TA _) "already typed",
  unify-eq K (fun `hd_beta_auto` TA F),
  hd-beta (F A) AS X C.

:before "hd-beta-zeta:end"
hd-beta-zeta (uvar as K) [A|AS] X C :- !, % auto-intro
  assert! (of A TA _) "already typed",
  unify-eq K (fun `hd_beta_zeta_auto` TA F),
  hd-beta-zeta (F A) AS X C.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%% Unification %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% invariant: hd-beta terms
% we start with ff, tt to handle symmetric cases
% NOTE: rec-calls with unify (ensured hd-beta + ff) , symmetric rules are typically !
% NOTE: asymmetric rules are not ! otherwise the flip rule is killed
% NOTE: whd are !
% names: unif X C  T D M
kind cumul type.
type eq cumul.
type leq cumul.

macro @tail-cut-if Option Hd Hyps :- (
  (Hd :- get-option Option tt,      Hyps, !),
  (Hd :- not(get-option Option tt), Hyps   )
).

pred unif i:term, i:stack, i:term, i:stack, i:bool, i:cumul.
:if "DBG:unif"
unif X CX Y CY D M :-
  coq.say {counter "run"} "unif" X CX "==" Y CY "(flipped?" D "cumul:" M ")", fail.

pred swap i:bool, i:(A -> B -> prop), i:A, i:B.
swap tt F A B :- F B A.
swap ff F A B :- F A B.

% flexible cases
@tail-cut-if "unif:greedy" (unif (uvar V L) [] T D _ _) (!, (bind-list L {unwind T D} V)).
@tail-cut-if "unif:greedy" (unif X C (uvar V L) [] _ _) (!, bind-list L {unwind X C} V).

unif (sort prop) [] (sort (uvar as Y)) [] _ _ :- !, Y = prop.
unif X [] (sort (uvar as Y)) [] M U :- !,
  coq.univ.new Lvl,
  Y = typ Lvl,
  unif X [] (sort Y) [] M U.
unif (sort (uvar as X)) [] Y [] M U :- !,
  coq.univ.new Lvl,
  X = typ Lvl,
  unif (sort X) [] Y [] M U.

unif (sort S1) [] (sort S2) [] M eq  :- !, swap M coq.sort.eq S1 S2.
unif (sort S1) [] (sort S2) [] M leq :- !, swap M coq.sort.leq S1 S2.

unif (primitive X) [] (primitive X) [] ff _ :- !.

unif (global (indt GR1)) C (global (indt GR2)) D _ _ :- !, GR1 = GR2, unify-ctxs C D.
unif (global (indc GR1)) C (global (indc GR2)) D _ _ :- !, GR1 = GR2, unify-ctxs C D.
unif (pglobal (indt GR1) I1) C (pglobal (indt GR2) I2) D _ eq :- !,
  GR1 = GR2,
  coq.univ-instance.unify-eq (indt GR1) I1 I2 ok,
  unify-ctxs C D.
unif (pglobal (indt GR1) I1) C (pglobal (indt GR2) I2) D _ leq :- !,
  GR1 = GR2,
  coq.univ-instance.unify-leq (indt GR1) I1 I2 ok,
  unify-ctxs C D.

% fast path for stuck term on the right
unif X C (global (indt _) as T) D ff U :- !, unif T D {whd X C} tt U. % TODO:1
unif X C (global (indc _) as T) D ff U :- !, unif T D {whd X C} tt U. % TODO:1
unif X C (pglobal (indt _) _ as T) D ff U :- !, unif T D {whd X C} tt U. % TODO:1
unif X C (pglobal (indc _) _ as T) D ff U :- !, unif T D {whd X C} tt U. % TODO:1

% congruence rules TODO: is the of assumption really needed?
unif (fun N T1 F1) [] (fun M T2 F2) [] _ _ :- !, ignore-failure! (N = M),
  unify T1 T2 eq,
  pi x\ (decl x N T1) => unify (F1 x) (F2 x) eq.
unif (prod N T1 F1) [] (prod M T2 F2) [] _ U :- !, ignore-failure! (N = M),
  unify T1 T2 eq,
  pi x\ (decl x N T1) => unify (F1 x) (F2 x) U.
unif (fix N Rno Ty1 F1) B1 (fix M Rno Ty2 F2) B2 _ _ :- !, ignore-failure! (N = M),
  unify Ty1 Ty2 eq,
  (pi f\ (decl f N Ty1) => unify (F1 f) (F2 f) eq),
  unify-ctxs B1 B2.
unif (match A1 R1 L1) B1 (match A2 R2 L2) B2 _ _ :- !,
  unify A1 A2 eq, unify R1 R2 eq, unify-list L1 L2, unify-ctxs B1 B2.

% congruence heuristic (same maybe-non-normal head)
unif (let N T1 B1 F1) C1 (let M T2 B2 F2) C2 _ _ :- ignore-failure! (N = M),
  unify T1 T2 eq, unify B1 B2 eq,
  (@pi-def N T1 B1 x\ unify (F1 x) (F2 x) eq),
  unify-ctxs C1 C2, !.
unif (global (const GR)) C (global (const GR)) D _ _ :- unify-ctxs C D, !.
unif (pglobal (const GR) I1) C (pglobal (const GR) I2) D _ eq :-
  coq.univ-instance.unify-eq (const GR) I1 I2 ok,
  unify-ctxs C D, !.
unif (pglobal (const GR) I1) C (pglobal (const GR) I2) D _ leq :-
  coq.univ-instance.unify-leq (const GR) I1 I2 ok,
  unify-ctxs C D, !.
unif X C T D _ _ :- name X, name T, X = T, unify-ctxs C D.

% 1 step reduction  TODO:1
unif (global (const GR)) C T D M U :- unfold GR none C X1 C1, !, unif X1 C1 T D M U.
unif (pglobal (const GR) I) C T D M U :- unfold GR (some I) C X1 C1, !, unif X1 C1 T D M U.
unif (let N TB B F) C1 T C2 M U :- !,
  @pi-def N TB B x\ unif {hd-beta (F x) C1} T C2 M U.
unif (match A _ L) C T D M U :- whd-indc A GR KA, !,
  unif {match-red GR KA L C} T D M U.
unif (fix _ N _ F as X) C T D M U :- nth-stack N C LA A RA, whd-indc A GR KA, !,
  unif {fix-red F X LA GR KA RA} T D M U.
unif X C T D M U :- name X, def X _ _ V, !, unif {hd-beta V C} T D M U.
  % TODO we could use _VN if nonflex
% TODO:1 turn into (if reducible then reduce1 else fully-reduce2 tt)

% symmetry
unif X C T D ff U :- !, unif T D X C tt U.

% error
% unif X C1 Y C2 _tt :- !,
%   print "Error: " {coq.term->string {unwind X C1}} "vs" {coq.term->string {unwind Y C2}}. %, halt.

% Contexts happens to be lists, so we just reuse the code
pred unify-list i:list term, i:list term.
unify-list L1 L2 :- unify-ctxs L1 L2.

% the entry points of rec calls: unify unify-ctxs
pred unify-ctxs i:list term, i:list term.
unify-ctxs [] [].
unify-ctxs [X|XS] [Y|YS] :- unify X Y eq, !, unify-ctxs XS YS.

pred unify i:term, i:term, i:cumul.
unify A B C :- unif {hd-beta A []} {hd-beta B []} ff C.

%%%%%% entry points for clients %%%%%%%
unify-eq  X Y :- unify X Y eq.
unify-leq X Y :- unify X Y leq.
unify-list-eq L1 L2 :- unify-list L1 L2.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%% Flexible case %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Binding a list of terms (delift in Matita, invert subst in Coq) 

% We use a keyd discipline, i.e. we only bind terms with a rigid head
pred key i:term.
key (global _) :- !.
key (pglobal _ _) :- !.
key C :- name C, !.
key (primitive _) :- !.

pred bind-list i:list term, i:term, o:A.
bind-list [] T T' :- bind T T1, T1 = T'.
bind-list [app [C| AS] |VS] T R :- key C, !,
  pi x\
    (pi L X\ bind (app[C|L]) X :- get-option "unif:greedy" tt,      unify-list-eq L AS, X = x, !) =>
    (pi L X\ bind (app[C|L]) X :- not (get-option "unif:greedy" tt),unify-list-eq L AS, X = x) =>
    bind-list VS T (R x).
bind-list [C|VS] T R :- key C, def C _ _ V, key V, !,
  pi x\ @tail-cut-if "unif:greedy" (bind C x) true => 
        @tail-cut-if "unif:greedy" (bind V x) true => 
        bind-list VS T (R x).
bind-list [C|VS] T R :- key C, !,
  pi x\ @tail-cut-if "unif:greedy" (bind C x) true => bind-list VS T (R x).
bind-list [ _ |VS] T R :- !, pi x\ bind-list VS T (R x).

% CAVEAT: (app FLEX), (match _ _ FLEX) are not terms!
pred bind i:term, o:term.
bind X Y :- name X, X = Y, !.
bind X Y :- name X, def X _ _ T, !, bind T Y.
bind (global _ as C) C :- !.
bind (pglobal _ _ as C) C :- !.
bind (sort _ as C) C :- !.
bind (fix N Rno Ty F) (fix N Rno Ty1 F1) :- !,
  bind Ty Ty1, pi x\ decl x N Ty => bind (F x) (F1 x).
bind (match T Rty B) X :- !,
  bind T T1, bind Rty Rty1, map B bind B1, X = (match T1 Rty1 B1).
bind (app L) X :- !, map L bind L1, X = app L1.
bind (fun N T F) (fun N T1 F1) :- !,
  bind T T1, pi x\ decl x N T => bind (F x) (F1 x).
bind (let N T B F) (let N T1 B1 F1) :- !,
  bind T T1, bind B B1, @pi-def N T B x\ bind (F x) (F1 x).
bind (prod N T F) X :- !,
  bind T T1, (@pi-decl N T x\ bind (F x) (F1 x)), X = (prod N T1 F1).
bind (uvar M L) W :- map L bind L1, coq.mk-app-uvar M L1 W.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% Type checking %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%% eat-prod head head-ty args-done todo-args refined-app refined-ty %%%%%%%%



pred bidir-app i:term, i:term, i:list term, o:term.
:name "of:bidirectional-app"
bidir-app _ _ _ _.

pred saturate-dummy i:term, o:term.
saturate-dummy (prod _ _ F) R :- pi x\ saturate-dummy (F x) R.
saturate-dummy X X.  

pred ensure-prod.aux i:list A, i:term, o:term, o:bool.
ensure-prod.aux [] X X _.
ensure-prod.aux [_|Args] (prod N S T) (prod N S T1) NU :- !,
  pi x\ ensure-prod.aux Args (T x) (T1 x) NU.
ensure-prod.aux [_|Args] uvar (prod Name_ Src_ R) tt :- !,
  pi x\ ensure-prod.aux Args (R x) (R x) tt.
ensure-prod.aux Args X R NU :-
  whd1 X Y, ensure-prod.aux Args Y R NU.

% TODO: do not fail if whd1 fails and the term is not flexible since it
% may just need to be passed a concrete argument

pred ensure-prod i:list A, i:term.
ensure-prod Args Ty :-
  ensure-prod.aux Args Ty R NeedsUnif,
  if (var NeedsUnif) true (of R _ R1, unify-eq Ty R1).


pred eat-prod i:list term, i:term, i:term, o:list term, o:term, o:term.
:if "DBG:of" eat-prod [] Hd Prod Adone Res ResTy :-
coq.say "eat-prod" Hd {rev Adone} "==" Res ";" Prod "=<=" ResTy, fail.

eat-prod [] Hd Prod Adone Res ResTy :- !,
  rev Adone Args,
  unify-eq Res {coq.mk-app Hd Args},
  unify-leq Prod ResTy.

% XXX why not unif?
eat-prod [A|AS] Hd (prod _ Src Tgt as Prod) Adone Res ResTy :-
  bidir-app Hd Prod Adone ResTy,
  of A Src ResA,
  eat-prod AS Hd (Tgt ResA) [ResA|Adone] Res ResTy.
% TODO: add a whd1 eg in case of a n-ary function

:if "DBG:of"
of X Tx Rx :- coq.say {counter "run"} "of" X Tx Rx, fail.

of X Tx R :- name X, (decl X _ T ; def X _ T _), unify-leq T Tx, R = X.

of (fun N S F) LamTy (fun M S2 F2) :-
  of (prod N S _) (sort _U) (prod M S2 T),
  unify-leq (prod M S2 T) LamTy,
  pi x\ decl x M S2 => of (F x) (T x) (F2 x).

of (app [X]) Ty R :- !, of X Ty R.

of (app [Hd|Args]) TyApp App :-
  of Hd Prod Hd1,
  ensure-prod Args Prod,
  eat-prod Args Hd1 Prod [] App TyApp.

of (prod N S F) ProdTy (prod N ResS ResF) :-
  closed_term U1, closed_term U2, closed_term U,
  of S (sort U1) ResS,
  (pi x\ decl x N ResS => of (F x) (sort U2) (ResF x)),
  pts U1 U2 U,
  unify-leq (sort U) ProdTy.

of (match T Rty Bs) ResRtyInst (match ResT ResRty ResBs) :-
  of T TyT ResT,
  % T : TyT = (indt GR) LArgs RArgs, and (indt GR) : Ty
  coq.safe-dest-app TyT (global (indt GR)) Args,
  coq.env.indt GR _IsInd Lno _Luno Ty Kn Ks, % TODO LUno
  split-at Lno Args LArgs RArgs, % TODO: not a failure, just type err
  % fix LArgs on ind ty and constructors ty
  coq.subst-prod LArgs Ty TyLArgs,
  map Ks (coq.subst-prod LArgs) KsLArgs,
  % Rty skeleton (uknown ending) = fun rargs, fun e : indt largs rargs, ?
  mk-rty [] {coq.mk-app (global (indt GR)) LArgs} TyLArgs ResRtyRaw, 
  of ResRtyRaw _ ResRty, unify-eq Rty ResRty,
  % Rty must type each branch
  map2 KsLArgs Kn (mk-bty Rty Lno) BsTy,
  map2 Bs BsTy of ResBs,
  % Outside type
  unify-leq {coq.mk-app ResRty {append RArgs [ResT]}} ResRtyInst.

of (let N Ty Bo F) TyFx (let N ResTy ResBo ResF) :-
  of Ty (sort _) ResTy, of Bo ResTy ResBo,
  pi x\ def x N ResTy ResBo => cache x T_ => of (F x) TyFx (ResF x).

of (fix N Rno Ty BoF) ResTy (fix N Rno RTy ResBoF) :-
  of Ty (sort _) RTy,
  unify-leq RTy ResTy,
  pi f\ decl f N RTy => of (BoF f) ResTy (ResBoF f).
 
of (sort S) (sort S1) (sort S) :- coq.sort.sup S S1.

of (global GR as X) T X :- coq.env.typeof GR T1, unify-leq T1 T.
of (pglobal GR I as X) T X :-
  @uinstance! I => coq.env.typeof GR T1, unify-leq T1 T.

of (primitive (uint63 _) as X) T X :- unify-leq {{ lib:elpi.uint63 }} T.
of (primitive (float64 _) as X) T X :- unify-leq {{ lib:elpi.float64 }} T.
of (primitive (pstring _) as X) T X :- unify-leq {{ lib:elpi.pstring }} T.

of (uvar as X) T Y :- !, evar X T Y.

:if "OVERRIDE_COQ_ELABORATOR"
:name "refiner-assign-evar"
:before "default-assign-evar"
evar X Ty S :- !, of X Ty S.

pred coerce     o:term, o:term, o:term, o:term.
pred coerced    i:term, i:term, i:term, o:term.
pred coerceible i:term, o:term, i:term, o:term.
of X T R :- get-option "of:coerce" tt, not (var T), of X XT Y, coerced XT T Y R.

:if "DBG:of"
of X Tx Rx :- coq.say {counter "run"} "of [FAIL]" X Tx Rx, fail.

pred utc % Uniqueness of typing
  i:list term, % names (canonical)
  i:term,      % type living in names
  i:list term, % values (explicit subst on names)
  i:term,      % type living in values
  o:prop.      % goal checking compatibility of the two types
utc [] T1 [] T2 (unify-eq T1V T2) :- !, copy T1 T1V.
utc [N|NS] T1 [V|VS] T2 C :- !, copy N V => utc NS T1 VS T2 C.
utc [] T1 VS T2 C :- !, utc [] {coq.subst-prod VS T1} [] T2 C. % FIXME: reduction
utc [_|NS] (prod _ _ F) [] T2 C :- !,                      % FIXME: reduction
  assert! (pi x\ F x = F1) "restriction bug", utc NS F1 [] T2 C.

% This could be done in ML
pred canonical? i:list term.
canonical? [].
canonical? [N|NS] :- name N, not(mem NS N), canonical? NS.

constraint declare-evar evar decl def cache rm-evar {
 rule (E1 : G1 ?- evar _ T1 (uvar K L1)) % canonical
    \ (E2 : G2 ?- evar _ T2 (uvar K L2)) % actual
    | (canonical? L1, utc L1 T1 L2 T2 Condition,
        coq.say "CHR: Uniqueness of typing of" K "+" L1 "<->" L2,
        coq.say E1 "|>" G1 "|-" K L1 ":" T1,
        coq.say E2 "|>" G2 "|-" K L2 ":" T2,
        coq.say E2 "|>" G2 "|-" Condition "\n"
       )
  <=> (E2 : G2 ?- Condition).
}


% typing match %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
type mk-rty list term -> term -> term -> term -> prop. 
mk-rty ARGS HD (prod N S T) (fun N S F) :- !,
  pi x\ mk-rty [x|ARGS] HD (T x) (F x).
mk-rty ARGS HD _ (fun _ IndApp _FRESH) :-
  coq.mk-app HD {rev ARGS} IndApp.

type mk-bty term -> int -> term -> constructor -> term -> prop.
mk-bty Rty Lno (prod N S T) Ki (prod N S B) :- !,
  pi x\ mk-bty Rty Lno (T x) Ki (B x).
mk-bty Rty Lno T Ki AppRtyNorm :-
  coq.safe-dest-app T (global (indt _)) Args,
  split-at Lno Args LArgs RArgs,
  coq.mk-app Rty {append RArgs [{coq.mk-app (global (indc Ki)) {append LArgs RArgs}}]} AppRty,
  hd-beta-zeta-reduce AppRty AppRtyNorm.
mk-bty Rty Lno T Ki AppRtyNorm :-
  coq.safe-dest-app T (pglobal (indt _) I) Args,
  split-at Lno Args LArgs RArgs,
  coq.mk-app Rty {append RArgs [{coq.mk-app (pglobal (indc Ki) I) {append LArgs RArgs}}]} AppRty,
  hd-beta-zeta-reduce AppRty AppRtyNorm.

% PTS sorts %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

pred pts i:sort, i:sort, o:sort.
pts  X Y U :- coq.sort.pts-triple X Y U.