Record expansion

Sketches a procedure to translate a term abstracted over a specific record to a term abstracted over the components of that record.

Example:

Record r := mk { proj1 : T1; proj2 : T2 }.
Definition f (x : r) := Body(proj1 x,proj2 x).

is expanded to:

Definition f1 v1 v2 := Body(v1,v2).

And recursively, if g uses f, then g1 must use f1...

The idea is to take f, replace (x : r) with as many abstractions as needed in order to write mk v1 v2, then replace x with mk v1 v2, finally fire iota reductions such as proj1 (mk v1 v2) = v1 to obtain f1.

Then record a global replacement f x = f1 v2 v2 whenever x = mk v1 v2.

Note

The expand predicate below is used before all of its clauses are known (new ones are added at runtime via coq.elpi.accumulate), so Elpi's static analysis cannot fully check it and emits a benign elpi.flex-clause warning. As the tutorials already do for elpi.linear-variable, it is silenced with Set Warnings.

From elpi Require Import elpi.
[Loading ML file ppx_deriving.runtime (implicit dependency) ... done]
[Loading ML file re (implicit dependency) ... done]
[Loading ML file re.str (implicit dependency) ... done]
[Loading ML file elpi.util (implicit dependency) ... done]
[Loading ML file elpi.lexer_config (implicit dependency) ... done]
[Loading ML file menhirLib (implicit dependency) ... done]
[Loading ML file stdlib-shims (implicit dependency) ... done]
[Loading ML file elpi.parser (implicit dependency) ... done]
[Loading ML file camlp-streams (implicit dependency) ... done]
[Loading ML file easy-format (implicit dependency) ... done]
[Loading ML file biniou (implicit dependency) ... done]
[Loading ML file yojson (implicit dependency) ... done]
[Loading ML file atdgen-runtime (implicit dependency) ... done]
[Loading ML file elpi.trace.atd (implicit dependency) ... done]
[Loading ML file elpi.trace.runtime (implicit dependency) ... done]
[Loading ML file elpi.runtime (implicit dependency) ... done]
[Loading ML file elpi.compiler (implicit dependency) ... done]
[Loading ML file elpi (implicit dependency) ... done]
[Loading ML file rocq-elpi.elpi ... done]



Set Warnings "-elpi.flex-clause".


Elpi Db record.expand.db lp:{{
  % This data base will contain all the expansions performed previously.
  % For example, if f was expandded to f1 we would have this clause:

  % expand (app[f, R | L]) (app[f1, V1, V2 | L1]) :-
  %   expand R (app[k, V1, V2]), std.map L expand L1.

% [expand A B] can be used to perform a replacement, eg
%   (expand (const "foo") (const "bar") :- !) ==> expand A B
pred expand term -> term.

}}.
Elpi Accumulate record.expand.db lp:{{
shorten std.{ map }.

:name "expand:start"
expand (global _ as C) C :- !.
expand (pglobal _ _ as C) C :- !.
expand (sort _ as C) C :- !.
expand (fun N T F) (fun N T1 F1) :- !,
  expand T T1, pi x\ expand x x ==> expand (F x) (F1 x).
expand (let N T B F) (let N T1 B1 F1) :- !,
  expand T T1, expand B B1, pi x\ expand x x ==> expand (F x) (F1 x).
expand (prod N T F) (prod N T1 F1) :- !,
  expand T T1, (pi x\ expand x x ==> expand (F x) (F1 x)).
expand (app L) (app L1) :- !, map L expand L1.
expand (fix N Rno Ty F) (fix N Rno Ty1 F1) :- !,
  expand Ty Ty1, pi x\ expand x x ==> expand (F x) (F1 x).
expand (match T Rty B) (match T1 Rty1 B1) :- !,
  expand T T1, expand Rty Rty1, map B expand B1.
expand (primitive _ as C) C :- !.

}}.
Elpi Command record.expand.
Elpi Accumulate Db record.expand.db.
Elpi Accumulate lp:{{

% This builds a clause to replace "proji (k y1..yn)" by "yi"
pred build-iotared-clause term, (pair constant term) -> (pred).
build-iotared-clause T   (pr Proj Var) C :-
  coq.env.global (const Proj) HD, % HD is the global term for Proj
  C = (pi L AppVar\ expand(app [HD,T|L]) AppVar :- coq.mk-app Var L AppVar).

% The core algorithm ----------------------------------------------------------

% It is idiomatic in λProlog to perform a single recursion over the data and
% perform multiple tasks while going. Here we both obtain the expanded term
% and the clause that records that expansion. Indeed the binders introduced
% in the new term (standing for the record fialds) and the quantifications
% introduced in the clause are very similar.

% missing in std
pred cons_assoc_opt option A, B, list (pair A B) -> list (pair A B).
cons_assoc_opt none _ X X.
cons_assoc_opt (some A) B X [pr A B|X].

% a package of data that we need to carry but rarely fully access
data info.
symb info :
    inductive % the record to expand
 -> gref % the term being expanded
 -> gref % the term being expanded and its expanded name
 -> list (option constant) % canonical projections
 -> constructor % record constructor
 -> term % record constructor type
 -> info.

% This predicate turns the OldBo in "fun x : r => OldBo" into
% "fun v1 v2 => NewBo". It is fueled by "KTY" (corresponding to the type
% of the record constructor). In parallel it consumes the list of projections,
% so that it can record that the i-th projection should be replaced by
% the variable standing for the i-th record field (accumulator called Iota)
pred expand-abstraction
  info,
  term, % the varibale binding the record in the input term

  % fuel
  term, % the type of the record constructor
  list (option constant), % projections

  term, % the Old body

  term, % constructor applied to all arguments treated so far
  list (pair constant term), % iota rules for reductions so far

  % used by expand-spine, accumulated here
  list term, list term, % variables for the head of the clause (LHS and RHS)
  list prop % accumulator for the premises of the clause
  ->
  term, % the New body
  prop. % the clause

expand-abstraction Info Rec (prod N S F) [P|PS] OldBo KArgs Iota AccL AccR Premises (fun N S Bo) (pi x\ Clause x) :- !,
  pi x\ expand x x ==>
    expand-abstraction Info Rec
      (F x) PS OldBo {coq.mk-app KArgs [x]} {cons_assoc_opt P x Iota} AccL [x|AccR] Premises (Bo x) (Clause x).

expand-abstraction Info Rec (let N S B F) [P|PS] OldBo KArgs Iota AccL AccR Premises (let N S B Bo) Clause :- !,
  pi x\ expand x x ==>
    % a let in is not a real argument to KArgs, but may need a "iota" redex, since the projection could exist
    expand-abstraction Info Rec
      (F x) PS OldBo KArgs {cons_assoc_opt P x Iota} AccL AccR Premises (Bo x) Clause.

expand-abstraction Info Rec _ [] OldBo ExpandedRecord Iota AccL AccR Premises Result Clause :-
  % generate all substitutions
  std.map Iota (build-iotared-clause ExpandedRecord) IotaClauses,
  ExpansionClause = expand Rec ExpandedRecord,
  % eta expand the record to obtain a new body (that typechecks)
  (ExpansionClause ==> expand OldBo NewBo), !,
  % continue, but schedule iota reductions (pre-existing projections became iota redexes)
  IotaClauses ==>
    expand-spine Info NewBo AccL AccR [ExpansionClause|Premises] Result Clause.

% This predicate travrses the spine of lambdas. When it finds an abstraction
% on the record R is calls expand-abstraction. Finally it copies the term,
% applying all substitutions accumulated while descending the spine.
pred expand-spine
  info,
  term, % input term
  list term, list term, % variables for the LHS and RHS of the clause head
  list prop
  ->
  term, % output term
  prop. % premises and final clause

% if we find a lambda over the record R we expand
expand-spine (info R _ _ Projs K KTY as Info) (fun _ LTy Bo) AccL AccR Premises Result (pi r\ Clause r) :- coq.env.global (indt R) LTy, !,
  pi r\ expand-abstraction Info r KTY Projs (Bo r) {coq.env.global (indc K)} [] [r|AccL] AccR Premises Result (Clause r).

% otherwise we traverse the spine
expand-spine Info (fun Name Ty Bo) AccL AccR Premises (fun Name Ty1 Bo1) (pi x y\ Clause x y) :- !,
  expand Ty Ty1, !,
  pi x y\ expand x y ==> expand y y ==> expand-spine Info (Bo x) [x|AccL] [y|AccR] [expand x y|Premises] (Bo1 y) (Clause x y).
expand-spine Info (let Name Ty V Bo) AccL AccR Premises (let Name Ty1 V1 Bo1) (pi x y\ Clause x y) :- !,
  expand Ty Ty1, !,
  expand V V1, !,
  pi x y\ expand x y ==> expand y y ==> expand-spine Info (Bo x) [x|AccL] [y|AccR] [expand x y|Premises] (Bo1 y) (Clause x y).

% at the end of the spine we fire the iota redexes and complete the clause
expand-spine (info _ GR NGR _ _ _) X AccL AccR Premises Y Clause :-
  expand X Y, !,
  % we build "app[f,x1..xn|rest]"
  (pi rest1\ coq.mk-app (global GR)  {std.append {std.rev AccL} rest1} (L rest1)),
  (pi rest2\ coq.mk-app (global NGR) {std.append {std.rev AccR} rest2} (R rest2)),
  % we can now build the clause "expand (app[f,L1..Ln|Rest1]) (app[f1,R1..Rn|Rest2])"
  % here we quantify only the tails, the other variables were quantified during
  % expand-*
  Clause = (pi rest1 rest2\ expand (L rest1) (R rest2) :- [!, std.map rest1 expand rest2 | Premises]).

% The entry point of the main algorithm, just fetchs some data and passes initial
% values for the accumulators.
pred expand-record inductive, gref, gref, term -> term, (pred).
expand-record R GR NGR X Y Clause :-
  std.assert! (coq.env.indt R tt 0 0 _ [K] [KTY]) "record is too complex for this example",
  coq.env.projections R Projs,
  expand-spine (info R GR NGR Projs K KTY) X [] [] [] Y Clause.

% This simply dispatches between global references ----------------------------

% The only cleverness is that "expand" also builds the clause to be added to
% the data base, and that clause has to mention the name of the constant to be
% generated. Since we don't know it yet (Rocq tells us in response to coq.env.add-const)
% we postulate a name for that constant "nc" and later replace it with the real one "NC"
pred expand-gref inductive, gref, string -> (pred).
expand-gref Record (const C) Name Clause :- !, std.do! [
  std.assert! (coq.env.const C (some Bo) _) "only transparent constants can be expanded",
  (pi nc\ expand-record Record (const C) nc Bo NewBo (NClause nc)),
  std.assert-ok! (coq.typecheck NewBo _) "illtyped",
  coq.env.add-const Name NewBo _ _ NC,
  Clause = NClause (const NC),
].

expand-gref _ (indt _) _ _ :- coq.error "Not implemented yet".

expand-gref _ (indc _) _ _ :- coq.error "It makes no sense to expand a constructor alone, expand the inductive instead".

% Entry point -----------------------------------------------------------------
main [str R, str In, str Prefix] :- !,
  std.assert! (coq.locate R (indt Record)) "The first argument must be a record name",
  std.assert! (coq.locate In GR) "The second argument must be a global term",
  NewName is Prefix ^ {coq.gref->id GR},

  expand-gref Record GR NewName Clause,

  % We want our clauses to take precensence over the structural ones of "expand"
  coq.elpi.accumulate _ "record.expand.db" (clause _ (before "expand:start") Clause).

main _ :- coq.error "usage: Elpi record.expand record_name global_term prefix".
}}.

Usage:

Record r := { T :> Type; X := T; op : T -> X -> bool }.
r is defined
T is defined
X is defined
op is defined

Definition f b (t : r) (q := negb b) := fix rec (l1 l2 : list t) :=
  match l1, l2 with
  | nil, nil => b
  | cons x xs, cons y ys => andb (op _ x y) (rec xs ys)
  | _, _ => q
  end.
f is defined

Elpi record.expand r f "expanded_".
expanded_f is defined

Print f.
f =
fun (b : bool) (t : r) =>
let q := negb b in
fix rec (l1 l2 : list t) {struct l1} : bool :=
  match l1 with
  | nil => match l2 with
           | nil => b
           | (_ :: _)%list => q
           end
  | (x :: xs)%list =>
      match l2 with
      | nil => q
      | (y :: ys)%list => (op t x y && rec xs ys)%bool
      end
  end
     : bool -> forall t : r, list t -> list t -> bool

Arguments f b%_bool_scope t (l1 l2)%_list_scope

Print expanded_f.
expanded_f =
fun (b : bool) (T : Type) =>
let X := T in
fun op : T -> X -> bool =>
let q := negb b in
fix rec (l1 l2 : list T) {struct l1} : bool :=
  match l1 with
  | nil => match l2 with
           | nil => b
           | (_ :: _)%list => q
           end
  | (x :: xs)%list =>
      match l2 with
      | nil => q
      | (y :: ys)%list => (op x y && rec xs ys)%bool
      end
  end
     : bool -> forall T : Type, (T -> T -> bool) -> list T -> list T -> bool

Arguments expanded_f b%_bool_scope T%_type_scope op%_function_scope
  (l1 l2)%_list_scope

Definition g t l s h := (forall x y, op t x y = false) /\ f true t l s = h.
g is defined

Elpi record.expand r g "expanded_".
expanded_g is defined

Print expanded_g.
expanded_g =
fun T : Type =>
let X := T in
fun (op : T -> X -> bool) (l s : list T) (h : bool) =>
(forall (x : T) (y : X), op x y = false) /\ expanded_f true T op l s = h
     : forall T : Type, (T -> T -> bool) -> list T -> list T -> bool -> Prop

Arguments expanded_g T%_type_scope op%_function_scope 
  (l s)%_list_scope h%_bool_scope