Skip to content

Commit

Permalink
[TC] refactor of build-eta-llam-links
Browse files Browse the repository at this point in the history
  • Loading branch information
@FissoreD
FissoreD committed Aug 10, 2024
1 parent ae8804c commit 268a8b3
Show file tree
Hide file tree
Showing 4 changed files with 54 additions and 76 deletions.
42 changes: 3 additions & 39 deletions apps/tc/elpi/compile_goal.elpi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,11 +35,6 @@ namespace tc {
pred maybe-eta i:term.
maybe-eta (fun _ _ B) :- pi x\ maybe-eta-aux (B x) [x].

pred split-pf i:list term, i:list term, o:list term, o:list term.
split-pf [] _ [] [] :- !.
split-pf [X|Xs] Old [X|Ys] L :- name X, not (std.mem! Old X), !, split-pf Xs [X|Old] Ys L.
split-pf Xs _ [] Xs.

pred used i:term, i:term.
used X (uvar _ S) :- std.mem! S X, !.
used X (fun _ _ Bo) :- pi x\ used X (Bo x).
Expand Down Expand Up @@ -86,41 +81,10 @@ namespace tc {
compile-full-aux Ty L Ty' LTy,
compile-full-aux-close Bo Ty LTy Bo' L'.

% NOTE: when compiling t = (app [X, x, y]) and [x,y] are distinct_names,
% then the coq variable has not [x,y] in scope, it is applied to
% them. Note also that t is a problematic term that cannot be
% exposed to the else unification algorithm.
% The solution is to build the following links:
% X =η (λa.Y a)
% a |- Y a =η (λb.Z a b)
% and expose a variable W at toplevel having Z has head and [x, y]
% as scope

% NOTE: when compiling t = (app [X, a, x]) where a is a constant and x a
% name, we build a llam link.
% The link will be: T x =L X a x
% the exposed variable in the term will be T x

% NOTE: here a combination of eta and llam:
% let t = (app [X x y, z, c, w, d]) where X is a coq var with x and
% y in scope, z and w are names and c, d are constants.
% In this case, the links should be:
% X x y =η (λa.Y x y a)
% a |- Z x y a w =L (app[Y x y a, c w d])
% The returned variable is Z x y a w

% Link for beta-redex (Uvar in PF)
% BUILD CHAIN OF LINKS-ETA from X to V...
% TODO: to avoid too many chain for the same var, maybe pass a list into the fold
compile-full-aux (app [(uvar _ Scope as V) | S] as T) L G' L'' :- !,
% By construction the scope of a uvar is a list of distinct name
std.fold-map S L compile-full-aux S' L', % LS = Links built for S
coq.typecheck V Ty ok,
split-pf S' Scope PF NPF,
free-names T Names,
tc.link.build-eta-llam-links V Scope Ty Names PF NPF L' G'' L'',
prune G' Names,
var G' G'' Names.
compile-full-aux (app [(uvar _ _ as V) | S]) L G' L'' :- !,
std.fold-map S L compile-full-aux S' L', % L' = Links built for S
tc.link.build-eta-llam-links (app [V|S']) L' G' L''.

compile-full-aux (app L) A (app L1) A1 :- !, std.fold-map L A compile-full-aux L1 A1.

Expand Down
28 changes: 6 additions & 22 deletions apps/tc/elpi/compile_instance.elpi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,7 @@ namespace tc {
(pi x\ is-name x => precompile-aux is_neg_fix (B x) N' (B' x) M).

precompile-aux _ (app [X|XS]) N (tc.maybe-llam-tm (app [app[X | PF] | NPF1]) Scope) (s M) :-
if (is-uvar X) (Sc = []) (var X _ Sc), split-pf XS Sc PF NPF,
is-uvar X, split-pf XS [] PF NPF,
not (NPF = []), !, % else XS is a list of distinct names, i.e. `app [X|XS]` is in PF
free-var Scope,
std.fold-map NPF N (precompile-aux is_neg_fix) NPF1 M.
Expand Down Expand Up @@ -237,27 +237,11 @@ namespace tc {
std.fold-map NPF (pr XS L1) decompile-term-aux Tl (pr XS' L2),
NL = tc.link.llam Y (app [Hd|Tl]).

% Maybe-llam when H is a hole appearing in the shelved goals
% This happens when the instance to be compiled comes from the context
% Example: Goal exists (X : T1 -> T2), forall a, c (X a) -> ...
% intros; eexists. (* In the context we have the instance `H: c (?X a)` *)
decompile-term-aux (tc.maybe-llam-tm (app[app[V | PF] | NPF] as T) S_) L G'' (pr XS' L'') :- !,
var V _ Scope, !,
std.fold-map NPF L decompile-term-aux NPF' (pr XS' L'),
free-names T Names,
coq.typecheck V Ty ok,
tc.link.build-eta-llam-links V Scope Ty Names PF NPF' L' G' L'',
prune G'' Names,
var G'' G' Names.

% HO var when H is a hole appearing in the shelved goals
decompile-term-aux (app [V|PF] as T) (pr XS' L') G'' (pr XS' L'') :-
var V _ Scope, !,
free-names T Names,
coq.typecheck V Ty ok,
tc.link.build-eta-llam-links V Scope Ty Names PF [] L' G' L'',
prune G'' Names,
var G'' G' Names.
% Here we have a coq evar applied to some terms. In this case, we build
% eta-llam links after the decompilation of S.
decompile-term-aux (app [(uvar _ _ as V)|S]) PR H (pr XS L') :- !,
std.fold-map S PR decompile-term-aux S' (pr XS L),
tc.link.build-eta-llam-links (app [V|S']) L H L'.

decompile-term-aux (fun Name Ty Bo) (pr XS L) (fun Name Ty' Bo') (pr XS2 L3) :- !,
(pi x\ is-name x => decompile-term-aux (Bo x) (pr XS []) (Bo' x) (pr XS1 (L1x x))),
Expand Down
58 changes: 44 additions & 14 deletions apps/tc/elpi/link.elpi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,28 +9,58 @@ namespace tc {
(pi X H L Ign\ fold-map X L X [H|L] :- var X H Ign, !) =>
fold-map T [] _ R.

% [build-eta-llam-links LHS Scope Ty Names PF NPF OldLinks NewVar NewLinks]
% Builds the eta/llam links at runtime for a term having the shape
% `app[(uvar X Scope as V) | L]`.
% LHS should be V, Scope the scope of V, TODO: finish to document this...
pred split-pf i:list term, i:list term, o:list term, o:list term.
split-pf [] _ [] [] :- !.
split-pf [X|Xs] Old [X|Ys] L :- name X, not (std.mem! Old X), !, split-pf Xs [X|Old] Ys L.
split-pf Xs _ [] Xs.

% [build-eta-llam-links.aux LHS Scope Ty Names PF NPF OldLinks NewVar NewLinks]
:index(_ _ _ _ 3)
% TODO: the argument Ty is unused, i.e. the binders of the eta links have no type...
% LHS Scope Ty Names PF NPF OldLinks NewVar
pred build-eta-llam-links i:term, i:list term, o:term, i:list term, i:list term, i:list term, i:list prop, o:term, o:list prop.
build-eta-llam-links LHS _ _ Names [] NPF OL HD [tc.link.llam T (app [LHS | NPF]) | OL] :- !,
pred build-eta-llam-links.aux i:term, i:list term, o:term, i:list term, i:list term, i:list term, i:list prop, o:term, o:list prop.
build-eta-llam-links.aux LHS _ _ Names [] NPF OL HD [llam T (app [LHS | NPF]) | OL] :- !,
std.assert! (not (NPF = [])) "[TC] NPF List should not be empty",
prune T Names,
var T HD _.
build-eta-llam-links LHS SC (prod _ Ty _) _ [X] [] OL HD [tc.link.eta LHS (fun `_` Ty (x\ V x)) | OL] :- !,
build-eta-llam-links.aux LHS SC (prod _ Ty _) _ [X] [] OL HD [eta LHS (fun `_` Ty (x\ V x)) | OL] :- !,
prune V SC, var (V X) HD _.
build-eta-llam-links LHS SC (prod _ Ty Bo) Names [X|XS] NPF OL HD [tc.link.eta LHS (fun `_` Ty (x\ LHS' x)) | L] :- !,
build-eta-llam-links.aux LHS SC (prod _ Ty Bo) Names [X|XS] NPF OL HD [eta LHS (fun `_` Ty (x\ LHS' x)) | L] :- !,
% TODO: unfold Ty if needed...
std.append SC [X] SC',
prune LHS' SC, build-eta-llam-links (LHS' X) SC' (Bo X) Names XS NPF OL HD L.
build-eta-llam-links LHS SC Ty Names ([_|_] as PF) NPF OL HD L :-
prune LHS' SC, build-eta-llam-links.aux (LHS' X) SC' (Bo X) Names XS NPF OL HD L.
build-eta-llam-links.aux LHS SC Ty Names ([_|_] as PF) NPF OL HD L :-
Ty' = prod _ _ _, coq.unify-eq Ty Ty' ok, !,
build-eta-llam-links LHS SC Ty' Names PF NPF OL HD L.

build-eta-llam-links.aux LHS SC Ty' Names PF NPF OL HD L.

% [build-eta-llam-links T OldLinks X NewLinks]
% T = app[(uvar _ Scope) | S] this term is problematic and asks for the
% creation of eta- and/or llam-links. Below some examples:

% eta: when compiling t = (app [X, x, y]) and [x,y] are distinct_names, then
% the coq variable has not [x,y] in scope: it is applied to them.
% The solution is to build the following links:
% NewLinks = [X =η (λa.Y a), a |- Y a =η (λb.Z a b)]
% and the exposed variable is G, given by `var G Z [x, y]`

% llam: when compiling t = (app [X, a, x]) where a is a constant and x a
% name, we build a llam link.
% The link will be: NewLinks ] = [T x =L X a x]
% and the exposed variable is G, given by `var G T [x]`

% eta-llam: here a combination of eta and llam:
% let t = (app [X x y, z, c, w, d]) where X is a coq var with x and y
% in scope, z and w are names and c, d are constants.
% In this case, the links should be:
% NewLinks = [X x y =η (λa.Y x y a), a |- Z x y a w =L (app[Y x y a, c w d])]
% and the exposed variable is G, given by `var Z T [x, y, z, w]`
pred build-eta-llam-links i:term, i:list prop, o:term, o:list prop.
build-eta-llam-links (app[(uvar _ Scope as V) | S] as T) Links G NewLinks :- !,
coq.typecheck V Ty ok,
split-pf S Scope PF NPF,
free-names T Names,
build-eta-llam-links.aux V Scope Ty Names PF NPF Links LhsHd NewLinks,
prune G Names,
var G LhsHd Names.
build-eta-llam-links T _ _ _ :- coq.error "[TC] invalid call to build-eta-llam-links:" T.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% ETA LINK %
Expand Down
2 changes: 1 addition & 1 deletion apps/tc/tests/test.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -596,7 +596,7 @@ Module CoqUvar4.
tc.precomp.instance {{c1 (fun x y => lp:X (lp:A x y) y)}} C _ _ _,
Expected = app [{{c1}}, tc.maybe-eta-tm (fun _ _ Body1) _],
Body1 = (x\ tc.maybe-eta-tm (fun _ _ (Body2 x)) [x]),
Body2 = (x\y\ tc.maybe-llam-tm (app [app [X], (Y x y), y]) [y,x]),
Body2 = (x\y\ app [X, (Y x y), y]),
std.assert! (C = Expected) "[TC] invalid compilation".
}}.

Expand Down

0 comments on commit 268a8b3

Please sign in to comment.