Record to sigma

A command that de-sugars a record type to iterated sigma types, suggested by M. Maggesi for the UniMath library.

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]

Elpi Command UM.expand.

Elpi Accumulate lp:{{ % From a record declaration to an iterated sigma type pred wrap-fields-ty record-decl -> term. wrap-fields-ty (field _ _ Ty _\ end-record) Ty. wrap-fields-ty (field _ Proj Ty Fields) {{ sigT lp:F }} :- coq.string->name Proj Name, F = fun Name Ty Bo, pi x\ decl x Name Ty ==> wrap-fields-ty (Fields x) (Bo x). % From a record declaration to a function building the iterated pairs % [wrap-fields-bo Rec Acc SigmaTypeDef SigmaTypeName Builder BuilderType] % Builder = fun arg1 .. argn => existT arg1 (existT arg2 (.. argn) ..) % Acc gathers arg1 .. argn while building the fun % SigmaTypeDef is used to fill in the implicit arguments of existT % SigmaTypeName is used for BuilderType = forall arg1 .. argn, SigmaTypeName pred wrap-fields-bo record-decl, list term, term, term -> term, term. wrap-fields-bo end-record Acc SigTy Sig T Sig :- std.rev Acc Args, wrap-fields-bo.aux Args SigTy T. wrap-fields-bo (field _ Proj Ty Fields) Acc SigTy Sig (fun Name Ty Bo) (prod Name Ty Tgt) :- coq.string->name Proj Name, pi x\ decl x Name Ty ==> wrap-fields-bo (Fields x) [x|Acc] SigTy Sig (Bo x) (Tgt x). pred wrap-fields-bo.aux list term, term -> term. wrap-fields-bo.aux [Last] _ Last. wrap-fields-bo.aux [X|XS] {{ sigT lp:F }} {{ existT lp:F lp:X lp:Rest }} :- F = fun _ _ G, wrap-fields-bo.aux XS (G X) Rest. % We declare the type and its constructor. % Missing features: % - parameters are not supported % - projections are not synthesized main [indt-decl (record Name _Sort Kname Fields)] :- wrap-fields-ty Fields T, std.assert-ok! (coq.typecheck T Ty) "oops, wrap-fields-ty is bugged", coq.env.add-const Name T Ty _ C, wrap-fields-bo Fields [] T (global (const C)) K KTy, std.assert-ok! (coq.typecheck K KTy) "oops, wrap-fields-bo is bugged", coq.env.add-const Kname K KTy _ _. }}.

Elpi Export UM.expand.

From now on UM.expand is a regular command taking as the only argument a record declaration:

UM.expand Record foo := mk_foo { f1 : Type; f2 : f1 -> Type; f3 : forall t : f1, f2 t -> bool }.

foo is defined mk_foo is defined

Print foo.

foo = {f1 : Type & {f2 : f1 -> Type & forall t : f1, f2 t -> bool}} : Type

Print mk_foo.

mk_foo = fun (f1 : Type) (f2 : f1 -> Type) (f3 : forall t : f1, f2 t -> bool) => existT (fun f4 : Type => {f5 : f4 -> Type & forall t : f4, f5 t -> bool}) f1 (existT (fun f4 : f1 -> Type => forall t : f1, f4 t -> bool) f2 f3) : forall (f1 : Type) (f2 : f1 -> Type), (forall t : f1, f2 t -> bool) -> foo Arguments mk_foo f1%_type_scope (f2 f3)%_function_scope