The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Xavier, you asked at the coq users meeting for a way to print all definitions that the type of a term depends upon.  After 2-3 hours of Ltac hacking, I have managed to implement a version in Ltac that does this (called [get_all_terms_and_types_recursively_in_type_of] below) (it doesn't pick up everything; it has trouble with dependent expressions under [forall] and under lambdas, and it won't pick up the types of constructors of an inductive type).  I've cc'd coq-club because I thought others might be interested in this.  It's rather ugly (and I can explain bits and pieces of it if desired, but I don't feel like documenting it all now; hacking in Ltac is a pain, especially when your tactics return terms, because then there's no good way to print out intermediate computation.)  The tactic returns a list, so it should be easy to feed it in to any procedure or other tactic, if, e.g., there's a plugin that will fetch the constructors of an inductive type.

The basic idea is that it gets terms and types by pattern matching on a term, and then puts them into a list, removes duplicates using ltac, and then recurses, cutting off recursion wherever it discovers a term that is already in the list (it's actually a bit less efficient than that, as it only looks at a much more local list, so expect slowdown sooner).

Here's the code:

Require Import List.

Record Dyn := dyn { ty : Type; elem : ty }.

Notation "` a" := (@dyn _ a) (at level 5).

Ltac head term :=

  match term with

    | ?f ?x => constr:(f)

    | _ => term

  end.

Ltac unif x y :=

  match x with

    | _ => let test := constr:(eq_refl : x = y) in

           constr:(true)

    | _ => constr:(false)

  end.

Ltac syntax_match x y :=

  match x with

    | y => constr:(true)

    | _ => constr:(false)

  end.

Ltac syntax_match_in a l :=

  match eval hnf in l with

    | nil => constr:(false)

    | ?b :: ?l' => let same := syntax_match b a in

                   match same with

                     | true => constr:(true)

                     | false => syntax_match_in a l'

                   end

  end.

Ltac filter_out a l :=

  match eval hnf in l with

    | @nil ?T => constr:(@nil T)

    | ?b :: ?l' => let same := syntax_match b a in

                   let l'' := filter_out a l' in

                   match same with

                     | true => constr:(l'')

                     | false => constr:(b::l'')

                   end

  end.

Ltac uniq l :=

  lazymatch eval hnf in l with

    | @nil ?T => constr:(@nil T)

    | ?b :: ?l' => let l'' := uniq l' in

                   let is_in_b_l'' := syntax_match_in b l'' in

                   lazymatch is_in_b_l'' with

                     | true => constr:(l'')

                     | false => constr:(b::l'')

                   end

  end.

Ltac get_all_terms term :=

  lazymatch term with

    | ?f ?x => let l1 := get_all_terms f in

               let l2 := get_all_terms x in

               let l1pl2 := constr:(l1 ++ l2) in

               uniq l1pl2

    | (fun x : ?T => ?f (@?P x)) => let l1 := get_all_terms f in

                                    let l2 := get_all_terms P in

                                    let l1pl2 := constr:(l1 ++ l2) in

                                    uniq l1pl2

    | (fun x : ?T => x) => get_all_terms T

    | (fun (x : ?T) (y : @?T' x) => @?P x)

      => let l1 := get_all_terms T' in

         let l2 := get_all_terms P in

         let l1pl2 := constr:(l1 ++ l2) in

         uniq l1pl2

    | (fun (x : ?T) (y : @?T' x) => @?P y)

      => let l1 := get_all_terms T' in

         let l2 := get_all_terms P in

         let l1pl2 := constr:(l1 ++ l2) in

         uniq l1pl2

    | (fun (x : ?T) => forall (y : @?T' x), @?P x)

      => let l1 := get_all_terms T' in

         let l2 := get_all_terms P in

         let l1pl2 := constr:(l1 ++ l2) in

         uniq l1pl2

    | (fun (x : ?T) => forall (y : @?T' x), @?P y)

      => let l1 := get_all_terms T' in

         let l2 := get_all_terms P in

         let l1pl2 := constr:(l1 ++ l2) in

         uniq l1pl2

    | (fun x : ?T => ?f) => let l1 := get_all_terms T in

                            let l2 := get_all_terms f in

                            let l1pl2 := constr:(l1 ++ l2) in

                            uniq l1pl2

    | (forall x : ?T, ?f (@?P x)) => let l1 := get_all_terms f in

                                     let l2 := get_all_terms P in

                                     let l1pl2 := constr:(l1 ++ l2) in

                                     uniq l1pl2

    | (forall (x : ?T) (y : @?T' x), @?P x)

      => let l1 := get_all_terms T' in

         let l2 := get_all_terms P in

         let l1pl2 := constr:(l1 ++ l2) in

         uniq l1pl2

    | (forall (x : ?T) (y : @?T' x), @?P y)

      => let l1 := get_all_terms T' in

         let l2 := get_all_terms P in

         let l1pl2 := constr:(l1 ++ l2) in

         uniq l1pl2

    | (forall x : ?T, ?f) => let l1 := get_all_terms T in

                             let l2 := get_all_terms f in

                             let l1pl2 := constr:(l1 ++ l2) in

                             uniq l1pl2

    | _ => let term' := (eval unfold term in term) in

           let terms := get_all_terms term' in

           constr:((@dyn _ term)::terms)

    | _ => (* uh oh, can't do any better *)

      constr:((@dyn _ term)::nil)

  end.

Ltac get_all_terms_in_types term :=

  let t := type of term in

  get_all_terms t.

Ltac get_all_terms_in_types_list_recursively l :=

  lazymatch eval hnf in l with

    | @nil ?T => constr:(@nil T)

    | @dyn _ ?x::?l'

      => let t' := (type of x) in

         let is_in_l' := syntax_match_in x l' in

         let same := syntax_match x Type in

         lazymatch (eval hnf in same) with

           | true

             => let l'' := get_all_terms_in_types_list_recursively l' in

                let ret := constr:(@dyn _ x::l'') in

                uniq ret

           | false

             =>

             lazymatch (eval hnf in is_in_l') with

               | true =>

                 let l'' := get_all_terms_in_types_list_recursively l' in

                 let ret := constr:(@dyn _ x::@dyn _ t'::l'') in

                 uniq ret

               | false =>

                 let l''0 := get_all_terms_in_types x in

                 let l''1 := get_all_terms_in_types_list_recursively l''0 in

                 let l''2 := get_all_terms_in_types_list_recursively l' in

                 let ret := constr:(@dyn _ x::(l''1 ++ l''2)) in

                 uniq ret

             end

         end

  end.

Ltac get_all_terms_in_terms_and_types term :=

  let t := (type of term) in

  let l1 := get_all_terms term in

  let l2 := get_all_terms t in

  let l1pl2 := constr:(l1 ++ l2) in

  uniq l1pl2.

Ltac get_all_terms_in_terms_and_types_list_recursively l :=

  lazymatch eval hnf in l with

    | @nil ?T => constr:(@nil T)

    | @dyn _ ?x::?l'

      => let t' := (type of x) in

         let is_in_l' := syntax_match_in x l' in

         let same := syntax_match x Type in

         lazymatch (eval hnf in same) with

           | true

             => let l'' := get_all_terms_in_terms_and_types_list_recursively l' in

                let ret := constr:(@dyn _ x::l'') in

                uniq ret

           | false

             =>

             lazymatch (eval hnf in is_in_l') with

               | true =>

                 let l'' := get_all_terms_in_terms_and_types_list_recursively l' in

                 let ret := constr:(@dyn _ x::@dyn _ t'::l'') in

                 uniq ret

               | false =>

                 let l''0 := get_all_terms_in_terms_and_types x in

                 let l''0' := filter_out (@dyn _ x) l''0 in

                 let l''1 := get_all_terms_in_terms_and_types_list_recursively l''0' in

                 let l''2 := get_all_terms_in_terms_and_types_list_recursively l' in

                 let ret := constr:(@dyn _ x::(l''1 ++ l''2)) in

                 uniq ret

             end

         end

  end.

Ltac get_all_terms_and_types_recursively_in_type_of term :=

  let l := get_all_terms_in_terms_and_types term in

  get_all_terms_in_terms_and_types_list_recursively l.

Ltac get_all_terms_and_types_recursively_in_type_of term :=

  let t := type of term in

  get_all_terms_and_types_recursively_in_type_of t.

Definition eq' := @eq.

Goal True.

  let term := constr:(@eq' _ (0::1::nil) (0::1::nil)) in

  let l := get_all_terms_in_terms_and_types term in

  let l' := get_all_terms_in_terms_and_types_list_recursively l in

  idtac l'.

  (* (`eq'

 :: `eq

    :: `cons

       :: `S

          :: `0 :: `(@nil) :: `list :: `nat :: `Set :: `Prop :: `Type :: nil) *)

-Jason