Merge pull request #94 from SkyLabsAI/janno/level-env

ltac2-extra: evar and LevelEnv improvements.

Author: Janno

ltac2-extra/plugin/tac2constr.ml

@@ -36,17 +36,30 @@ let evar_tag : _ Tac2core.map_tag =
 let define s =
   define Tac2expr.{ mltac_plugin = "sl.Constr"; mltac_tactic = s }
 
+let collect_context ctx =
+  let fn acc decl =
+    let open Context.Named.Declaration in
+    let binder =
+      Context.make_annot (Names.Name.Name (get_id decl)) (get_relevance decl), get_type decl
+    in
+    (binder, get_value decl) :: acc
+  in
+  Context.Named.fold_inside fn ~init:[] ctx
+
 (* [evar_context] returns the context of an evar, i.e. the context at the time
    it was defined. *)
 let _ =
-  define "evar_context" (evar @-> eret (list (triple ident (option constr) constr))) @@ fun e _ sigma ->
+  define "evar_context" (evar @-> eret (list (pair binder (option constr)))) @@ fun e _ sigma ->
     let (EvarInfo e) = Evd.find sigma e in
     let ctx = Evd.evar_context e in
-    let fn acc decl =
-      let open Context.Named.Declaration in
-      (get_id decl, get_value decl, get_type decl) :: acc
-    in
-    Context.Named.fold_inside fn ~init:[] ctx
+    collect_context ctx
+
+(* [evar_filtered_context] returns the filtered context of an evar. *)
+let _ =
+  define "evar_filtered_context" (evar @-> eret (list (pair binder (option constr)))) @@ fun e _ sigma ->
+    let (EvarInfo e) = Evd.find sigma e in
+    let ctx = Evd.evar_filtered_context e in
+    collect_context ctx
 
 (* [compare] must be kept in sync with whatever is used in [ConstrSet] and [ConstrMap] *)
 let _ =

ltac2-extra/tests/test_constr.v

@@ -122,7 +122,7 @@ Module Evar_Test.
       match kind l with
       | Evar e inst =>
           let ctx := Evar.context e in
-          let ids := List.map (fun (id, _, _) => id) ctx in
+          let ids := List.map (fun (b, _) => Option.get (Binder.name b)) ctx in
           Control.assert_true (List.equal Ident.equal ids [@a; @b]);
           let inst := Array.to_list inst in
           (* printf "inst:"; *)

ltac2-extra/tests/test_level_env.v

@@ -33,53 +33,84 @@ Module Substitute.
     | _, _ => throw_invalid! "%a and %a disagree on having a value" RelDecl.pp a RelDecl.pp b
     end.
 
-  Goal True.
+  Ltac2 test_env_with_let offset :=
+    let make_rel i := make_rel (Int.add i offset) in
+    let e := LevelEnv.empty_w_offset offset in
+    let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @a) 'nat)) in
+    let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @A) (make_app1 '(@eq nat 1) (make_rel 1)))) in
+    let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @b) 'nat)) in
+    let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @B) (make_app1 '(@eq nat 2) (make_rel 3)))) in
+    let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @C) (make_app1 '(@eq nat 3) '3))) in
+    let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @d) 'nat)) in
+    let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @D) (make_app1 '(@eq nat 4) (make_rel 6)))) in
+    (* printf "%a" LevelEnv.pp_named e; *)
+    e.
+
+  Ltac2 test_env_wo_let offset :=
+    let make_rel i := make_rel (Int.add i offset) in
+    let e := LevelEnv.empty_w_offset offset in
+    let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @a) 'nat)) in
+    let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @A) (make_app1 '(@eq nat 1) (make_rel 1)))) in
+    let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @b) 'nat)) in
+    let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @B) (make_app1 '(@eq nat 2) (make_rel 3)))) in
+    let e := LevelEnv.add_decl_level e (RelDecl.Def (Binder.make (Some @c) 'nat) '3) in
+    let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @C) (make_app1 '(@eq nat 3) (make_rel 5)))) in
+    let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @d) 'nat)) in
+    let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @D) (make_app1 '(@eq nat 4) (make_rel 7)))) in
+    (* printf "%a" LevelEnv.pp_named e; *)
+    e.
+
+  Ltac2 test_substitute_def offset :=
+    let make_rel i := make_rel (Int.add i offset) in
     let (ref_env, ref_term) :=
-      let e := LevelEnv.empty in
-      let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @a) 'nat)) in
-      let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @A) (make_app1 '(@eq nat 1) (make_rel 1)))) in
-      let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @b) 'nat)) in
-      let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @B) (make_app1 '(@eq nat 2) (make_rel 3)))) in
-      let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @C) (make_app1 '(@eq nat 3) '3))) in
-      let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @d) 'nat)) in
-      let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @D) (make_app1 '(@eq nat 4) (make_rel 6)))) in
+      let e := test_env_with_let offset in
       let t := make_app4 '@test (make_rel 1) (make_rel 3) '3 (make_rel 6) in
       (e, t)
     in
 
     let (env, term) :=
-      let e := LevelEnv.empty in
-      let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @a) 'nat)) in
-      let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @A) (make_app1 '(@eq nat 1) (make_rel 1)))) in
-      let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @b) 'nat)) in
-      let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @B) (make_app1 '(@eq nat 2) (make_rel 3)))) in
-      let e := LevelEnv.add_decl_level e (RelDecl.Def (Binder.make (Some @c) 'nat) '3) in
-      let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @C) (make_app1 '(@eq nat 3) (make_rel 5)))) in
-      let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @d) 'nat)) in
-      let e := LevelEnv.add_decl_level e (RelDecl.Assum (Binder.make (Some @D) (make_app1 '(@eq nat 4) (make_rel 7)))) in
+      let e := test_env_wo_let offset in
       let t := make_app4 '@test (make_rel 1) (make_rel 3) (make_rel 5) (make_rel 7) in
-      (* printf "%a" LevelEnv.pp_named e; *)
       let (e, subs) := LevelEnv.substitute_defs e in
       (* printf "%a" (pp_list pp_constr) subs; *)
-      (e, substnl subs 0 t)
+      (e, substnl subs offset t)
     in
     (* printf "%a" LevelEnv.pp_named ref_env; *)
     (* printf "%t" ref_term; *)
     (* printf "%a" LevelEnv.pp_named env; *)
     (* printf "%t" term; *)
     List.iter2 assert_rel_decl_eq (LevelEnv.to_list ref_env) (LevelEnv.to_list env);
-    assert_constr_eq ref_term term
-    .
+    assert_constr_eq ref_term term.
+
 
+  Goal True.
+  Proof.
+    test_substitute_def 0.
+    test_substitute_def 1.
+    test_substitute_def 2.
+    test_substitute_def 3.
+    test_substitute_def 4.
+    test_substitute_def 5.
+    test_substitute_def 6.
+    test_substitute_def 7.
+    exact I.
+  Qed.
+
+
+  Goal True.
+  Proof.
+    let e := test_env_with_let 1 in
+    let (p,s) := LevelEnv.cut e 2 in
+    let e' := LevelEnv.append p s in
+    List.iter2 assert_rel_decl_eq (LevelEnv.to_list e) (LevelEnv.to_list e').
     exact I.
   Qed.
 
   Goal True.
     intros.
     let e := LevelEnv.empty in
       let e := LevelEnv.add_decl_level e (RelDecl.Def (Binder.make (Some @c) 'nat) '3) in
-    let (ev, inst) := make_evar_in_level_env true e 'nat in
-    printf "%t" (make_evar ev inst);
+    let (ev, _) := make_evar_in_level_env true e 'nat in
     Control.new_goal ev > [|exact &c] > [exact I].
   Qed.
 

ltac2-extra/theories/internal/constr.v

@@ -143,10 +143,25 @@ Module Constr.
       "ltac2_extensions" "restrict_evar".
 
     (** See [Evd.evar_context].
+
+        WARNING: Ltac2 evar instances are always filtered.
+        If you are working with those, you need [evar_filtered_context].
+
+        NOTE: The [binder]s returned are guaranteed to be named. The reason to
+        return [binders] and not pairs of [ident] and [constr] is to correctly
+        track the relevance of the binders.
+
         NOTE: The context is returned from outermost to innermost binder, i.e.
         the same order as in [Control.hyps]. *)
-    Ltac2 @ external context : evar -> (ident * constr option * constr) list :=
+    Ltac2 @ external context : evar -> (binder * constr option) list :=
       "sl.Constr" "evar_context".
+
+    (** See [Evd.evar_filtered_context] and notes in [evar_context] above.
+
+        NOTE: The filtered context will have the same length as the Ltac2
+        representation of the evar's instance. *)
+    Ltac2 @ external filtered_context : evar -> (binder * constr option) list :=
+      "sl.Constr" "evar_filtered_context".
   End Evar.
 
   (** [subst_evars c] returns [Some c'], where [c'] is a copy of [c] where all