From e6e5e8318fa01c231a2c11b6abb932a807177ff8 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 7 Oct 2022 16:42:58 +0530 Subject: [PATCH] Cache reified lemmas with LetIn (#77) Implementing a strategy devised in discussion with Andres: > Like, maybe we want to reify the cache using LetIn instead of let in, > have a variant of interp that takes a list of definitions (either > untyped or with types lifted from the syntax or maybe just with reified > types so that we can transport easily enough) that are supposed to be > equal to the cache, and proving equality with interp leaves over > subgoals for cache equality? > Have a version of interp that takes in a nat and asks for arguments > for the first n LetIns, and then does normal interp, and a lemma that > takes in n and the interps for the first n LetIns and proofs that the > values are correct, and proves that special interp equal to the normal > interp. Then we prove equality overall by App special_interp_eq [t; e; > constant1; eq_refl; constant1; eq_refl; ... ; constantn; eq_refl; > eq_refl] We use a slight variant of this, making use of the UnderLets monad to avoid the use of `nat`. --- src/Rewriter/Language/Reify.v | 125 +++++++++++++++++++++++++++++++--- 1 file changed, 115 insertions(+), 10 deletions(-) diff --git a/src/Rewriter/Language/Reify.v b/src/Rewriter/Language/Reify.v index 68a328503..242deaa4d 100644 --- a/src/Rewriter/Language/Reify.v +++ b/src/Rewriter/Language/Reify.v @@ -8,6 +8,8 @@ Require Import Ltac2.Ltac2. Require Import Ltac2.Printf. Require Import Rewriter.Language.PreCommon. Require Import Rewriter.Language.Language. +Require Import Rewriter.Language.UnderLets. +Require Import Rewriter.Language.UnderLetsCacheProofs. Require Import Rewriter.Util.LetIn. Require Import Rewriter.Util.ListUtil. Require Import Rewriter.Util.Option. @@ -29,6 +31,8 @@ Require Rewriter.Util.Tactics2.Message. Require Rewriter.Util.Tactics2.Ident. Require Rewriter.Util.Tactics2.String. Require Rewriter.Util.Tactics2.Constr. +Require Import Rewriter.Util.Tactics2.DestEvar. +Require Import Rewriter.Util.Tactics2.InstantiateEvar. Require Import Rewriter.Util.Tactics2.Constr.Unsafe.MakeAbbreviations. Require Import Rewriter.Util.Tactics2.FixNotationsForPerformance. Import Coq.Lists.List ListNotations. @@ -40,6 +44,8 @@ Import EqNotations. Module Compilers. Export Language.PreCommon. Export Language.Compilers. + Import UnderLets.Compilers. + Import UnderLetsCacheProofs.Compilers. Module Export Exports. Ltac2 Type exn ::= [ Reification_failure (message) ]. Ltac2 Type exn ::= [ Reification_panic (message) ]. @@ -890,6 +896,36 @@ Module Compilers. end in aux (List.rev (Cache.elements cache))). + Definition UnderLet_expr {base_type} {ident} {var} {T} {A} e f + := @UnderLets.UnderLet base_type ident var T A e (fun v => f (@Var base_type ident var _ v)). + Ltac2 reify_UnderLets_bind_cache (base_type : constr) (ident : constr) (var : constr) (rty_rterm : constr * constr) (cache : Cache.t) : constr (* result *) * ((constr * constr) list (* list of (reified type, interpreted cached constant) pairs, in order *)) := + Reify.debug_profile + "reify_UnderLets_bind_cache" + (fun () + => let debug_Constr_check := Reify.Constr.debug_check_strict "expr.reify_UnderLets_bind_cache" in + let (rty, rterm) := rty_rterm in + let _expr := '@expr.expr in + let expr := mkApp _expr [base_type; ident; var; rty] in + let mkUnderLet := let _UnderLet := (eval cbv delta [UnderLet_expr] in + '@UnderLet_expr) in + fun rt e f => mkApp _UnderLet [base_type; ident; var; expr; rt; e; f] in + let rec aux (elems : (_ * Cache.elem) list) (ids : ident list) + := match elems with + | [] => (mkApp '@UnderLets.Base [base_type; ident; var; expr; Constr.Unsafe.closenl ids 1 rterm], []) + | elem :: elems + => let (val, elem) := elem in + let (name, rt, rv) := (elem.(Cache.name), elem.(Cache.rty), elem.(Cache.rterm)) in + Reify.debug_let_bind "reify_UnderLets_bind_cache" name rt rv; + let (res, vals) := aux elems (name :: ids) in + let rv := Constr.Unsafe.closenl ids 1 rv in + let x := Constr.Binder.make (Some name) (mkApp _expr [base_type; ident; var; rt]) in + (mkUnderLet rt rv (mkLambda x res), (rt, val) :: vals) + end in + let (res, vals) := aux (List.rev (Cache.elements cache)) [] in + let res := debug_Constr_check (fun () => res) in + ((eval cbv beta in res), + vals)). + Ltac2 reify_in_context (base_type : constr) (ident : constr) (reify_base_type : constr -> constr) (reify_ident_opt : binder list -> constr -> constr option) (var : constr) (term : constr) (ctx_tys : binder list) (var_ty_ctx : constr list) (value_ctx : (ident * constr (* ty *) * constr (* var *)) list) (template_ctx : constr list) (cache : Cache.t option) : constr := let cache := match cache with | Some cache => cache @@ -903,8 +939,26 @@ Module Compilers. | None => Control.zero (Reification_failure (fprintf "Failed to reify: %t" term)) end. + Ltac2 reify_in_context_and_cache (base_type : constr) (ident : constr) (reify_base_type : constr -> constr) (reify_ident_opt : binder list -> constr -> constr option) (var : constr) (term : constr) (ctx_tys : binder list) (var_ty_ctx : constr list) (value_ctx : (ident * constr (* ty *) * constr (* var *)) list) (template_ctx : constr list) (cache : Cache.t option) : (constr (* rty *) * constr (* rterm *)) * ((constr * constr) list (* list of (reified type, interpreted cached constant) pairs, in order *)) := + let cache := match cache with + | Some cache => cache + | None => Cache.init term + end in + match Reify.debug_profile + "reify_in_context_opt" + (fun () => reify_in_context_opt base_type ident reify_base_type reify_ident_opt var term ctx_tys var_ty_ctx value_ctx template_ctx cache) + with + | Some v + => let (rty, _) := v in + let (res, ids) := reify_UnderLets_bind_cache base_type ident var v cache in + ((rty, res), ids) + | None => Control.zero (Reification_failure (fprintf "Failed to reify: %t" term)) + end. + Ltac2 reify (base_type : constr) (ident : constr) (reify_base_type : constr -> constr) (reify_ident_opt : binder list -> constr -> constr option) (var : constr) (term : constr) (cache : Cache.t option) : constr := reify_in_context base_type ident reify_base_type reify_ident_opt var term [] [] [] [] cache. + Ltac2 reify_and_cache (base_type : constr) (ident : constr) (reify_base_type : constr -> constr) (reify_ident_opt : binder list -> constr -> constr option) (var : constr) (term : constr) (cache : Cache.t option) : (constr (* rty *) * constr (* rval *)) * ((constr * constr) list (* list of (reified type, interpreted cached constant) pairs, in order *)) := + reify_in_context_and_cache base_type ident reify_base_type reify_ident_opt var term [] [] [] [] cache. (* TODO: come up with a better naming convention than prefix [_] to replace starting-with-capital-letters *) (* TODO: figure out how to share the cache between multiple reifications *) Ltac2 _Reify (base_type : constr) (ident : constr) (reify_base_type : constr -> constr) (reify_ident_opt : binder list -> constr -> constr option) (term : constr) : constr := @@ -915,17 +969,68 @@ Module Compilers. => let r := reify base_type ident reify_base_type reify_ident_opt (mkVar var) term None in Control.refine (fun () => r)). Ltac2 _Reify_rhs (base_type : constr) (ident : constr) (reify_base_type : constr -> constr) (reify_ident_opt : binder list -> constr -> constr option) (base_interp : constr) (interp_ident : constr) () : unit := - let rhs := lazy_match! goal with [ |- _ = ?rhs ] => rhs end in - let r := Reify.debug_profile "_Reify_rhs._Reify" (fun () => _Reify base_type ident reify_base_type reify_ident_opt rhs) in - Reify.debug_profile "_Reify_rhs.transitivity" (fun () => Std.transitivity '(@Interp $base_type $ident $base_interp $interp_ident _ $r)) + Reify.debug_fine_grained "expr._Reify_rhs" (fun () => fprintf "Initial variable bindings"); + let check c := match Constr.Unsafe.check c with + | Val v => v + | Err err => Control.throw (Reification_panic (fprintf "_Reify_rhs: failed to check %t: %a" c (fun () => Message.of_exn) err)) + end in + let type_interp := '@type.interp in + let eq_refl := '@eq_refl in + let mk_type_interp t := mkApp type_interp [base_type; base_interp; t] in + (* get the term we're reifying *) + let (t, rhs) := lazy_match! goal with [ |- @eq ?t ?lhs ?rhs ] => (t, rhs) end in + (* play some games to get an evar we can run [intro var] in for reification *) + let r := '_ in + let intermediate := Reify.debug_profile "_Reify_rhs.make intermediate" (fun () => '(@Interp $base_type $ident $base_interp $interp_ident _ $r)) in + (* in the evar, we reify the term and return the interpred constants from the cache, the reified type and the reified value *) + let (ev_r, _) := destEvar r in + let (ids, rty, under_lets_r) + := Reify.debug_profile + "_Reify_rhs.reify and refine" + (fun () + => in_evar + ev_r + (fun () + => Reify.debug_fine_grained "expr._Reify_rhs" (fun () => fprintf "intro var in %t" (Control.goal ())); + let var := Fresh.fresh (Fresh.Free.of_goal ()) @var in + intro var; + Reify.debug_fine_grained "expr._Reify_rhs" (fun () => fprintf "reify_and_cache"); + let (res, vals) := Reify.debug_profile + "_Reify_rhs.reify_and_cache" + (fun () => reify_and_cache base_type ident reify_base_type reify_ident_opt (mkVar var) rhs None) in + let (rty, r) := res in + Reify.debug_fine_grained "expr._Reify_rhs" (fun () => fprintf "adjust %I in %t" var r); + (* instantiate var to type.interp for the return value of the reified term *) + let r' := r in + let r' := Constr.Unsafe.closenl [var] 1 r' in + let r' := Constr.Unsafe.substnl ['(@type.interp $base_type $base_interp)] 0 r' in + Reify.debug_fine_grained "expr._Reify_rhs" (fun () => fprintf "cbv [UnderLets.to_expr_App]"); + let r := (eval cbv [UnderLets.to_expr_App] in + constr:(UnderLets.to_expr_App $r)) in + Reify.debug_fine_grained "expr._Reify_rhs" (fun () => fprintf "refine %t" r); + Reify.debug_profile + "_Reify_rhs.refine with reified" + (fun () => Control.refine (fun () => r)); + (vals, rty, r'))) in + Reify.debug_fine_grained "expr._Reify_rhs" (fun () => fprintf "transitivity %t" intermediate); + Reify.debug_profile "_Reify_rhs.transitivity" (fun () => Std.transitivity intermediate) > [ - | clear; - let pf := lazy_match! goal with - | [ |- @eq ?t ?orig ?reified ] - => (* we assume orig is smaller *) - mkApp '@eq_refl [t; orig] - end in - Reify.debug_profile "_Reify_rhs.abstract exact_no_check eq_refl" (fun () => abstract (Std.exact_no_check pf)) ]. + | let pf := Reify.debug_profile + "_Reify_rhs.make proof unsafe" + (fun () => + mkApp '@UnderLets.cached_interp_related_impl + (List.append + (List.append + [base_type; ident; base_interp; interp_ident; rty; under_lets_r; rhs] + (List.flat_map + (fun (rty, id) => [id; mkApp eq_refl [mk_type_interp rty; id] ]) + ids)) + [mkApp eq_refl [t; rhs] ])) in + let pf := Reify.debug_profile "_Reify_rhs.make proof check for universes" (fun () => check pf) in + Reify.debug_fine_grained "expr._Reify_rhs" (fun () => fprintf "clear"); + clear; + Reify.debug_fine_grained "expr._Reify_rhs" (fun () => fprintf "abstract exact_no_check %t" pf); + Reify.debug_profile "_Reify_rhs.abstract exact_no_check UnderLets.cached_interp_related_impl..." (fun () => abstract (Std.exact_no_check pf)) ]. #[deprecated(since="8.15",note="Use Ltac2 instead.")] Ltac reify base_type ident reify_base_type reify_ident var term :=