The Coq mailing list

[Kenneth Roe <kendroe AT hotmail.com>]

I found (and adapted the following piece of code to traverse declarations in the current environment:

let print_full_pure_context () =

  let rec prec = function

  | ((_,kn),Lib.Leaf lobj)::rest ->

      let pp = match object_tag lobj with

      | "CONSTANT" ->

          let con = Global.constant_of_delta_kn kn in

          let cb = Global.lookup_constant con in

          let typ = ungeneralized_type_of_constant_type cb.const_type in

          hov 0 (

            match cb.const_body with

              | Undef _ ->

                str "Parameter " ++

                print_basename con ++ str " : " ++ cut () ++ pr_ltype typ

              | OpaqueDef lc ->

                str "Theorem " ++ print_basename con ++ cut () ++

                str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++

                str "Proof " ++ pr_lconstr (Opaqueproof.force_proof (Global.opaque_tables ()) lc)

              | Def c ->

                str "Definition " ++ print_basename con ++ cut () ++

                str "  : " ++ pr_ltype typ ++ cut () ++ str " := " ++

                pr_lconstr (Mod_subst.force_constr c))

          ++ str "." ++ fnl () ++ fnl ()

      | "INDUCTIVE" ->

          let mind = Global.mind_of_delta_kn kn in

          let mib = Global.lookup_mind mind in

          pr_mutual_inductive_body (Global.env()) mind mib ++

            str "." ++ fnl () ++ fnl ()

      | "MODULE" ->

          (* TODO: make it reparsable *)

          let (mp,_,l) = repr_kn kn in

          print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()

      | "MODULE TYPE" ->

          (* TODO: make it reparsable *)

          (* TODO: make it reparsable *)

          let (mp,_,l) = repr_kn kn in

          print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl ()

      | x -> (str "Unknown ") ++ (str x) ++ str " " ++ str (KerName.debug_to_string kn) ++ str "\n" ++ cut () ++ (mt ()) in

      prec rest ++ pp

  | ((_,kn),(Lib.CompilingLibrary (d,(m,d2))))::rest -> (str "Compiling Library ") ++ (str (DirPath.to_string d)) ++ (str " ") ++ (str (ModPath.to_string m)) ++ (str " ") ++ (str (DirPath.to_string d2)) ++ (str "\n") ++ prec rest

  | ((_,kn),(Lib.OpenedModule (a,b,c,d)))::rest -> (str "Opened module\n") ++ prec rest

  | ((_,kn),(Lib.ClosedModule ls))::rest -> (str "Closed module\n") ++ prec rest

  | ((_,kn),(Lib.OpenedSection (a,b)))::rest -> (str "Opened section\n") ++ prec rest

  | ((_,kn),(Lib.ClosedSection ls))::rest -> (str "Closed section\n") ++ prec rest

  | _ -> mt () in

  prec (Lib.contents ())

This code works well for printing out all the declarations in the top level environment.  However, if I have done something like:

Coq < Require Export AdvancedRewrite.advancedRewrite.

[Loading ML file theplug.cmxs ... done]

Coq < Require Export List.

Coq < Theorem x: 1=2.

1 subgoal

  

  ============================

  1 = 2

x < arewrite.

Environment:

Compiling Library Top Top <>

Unknown REQUIRE Top._2

Unknown TOKEN Top._4

Unknown TOKEN Top._5

Unknown REQUIRE Top._3

Unknown REQUIRE Top._6

Unknown REQUIRE Top._7

Unknown REQUIRE Top._8

END

2 subgoals

  

  ============================

  False

subgoal 2 is:

 False = (1 = 2)

x <

You will notice that I pick up all the top level declarations.  My "arewrite" tactic calls print_full_pure_context.  I would like to also pick up the declarations in all included libraries.  In this case, I would like to pick up the declarations in Arewrite.arewrite and List.  How can I do this?

                 - Ken