5
$\begingroup$

I want to be able to (tree) traverse Coq terms (e.g. in OCaml or using their s-expression representation in any language).

My main challenge is to figure out how to do this systematically because I noticed two things that make arbitrary tree traversal difficult (or at least none obvious to me):

  1. There might be arbitrary OCaml records with any size in the OCaml data type. Thus, I don't know what the "key" names or the length of the record (represented as a list in the s-exp) would be.
  2. There are types that could be any type -- due to type variables 'a. Therefore making pattern matching challenging in a programmatically (since I don't know what constructors might appear before hand).

Thus, I am unsure how to traverse "Coq ASTs" programmatically in a systematic way in code that I write (say in OCaml, Coq or even Python).

So: How do I programmatically traverse Coq AST terms from their ocaml representation?


More details

For example, let me give you a concrete example when interacting with coq-serapi:

Run the proof script first (why not):

(Add () "
Theorem add_easy_0: forall n:nat, 0 + n = n. simpl. reflexivity. Show Proof.")
(Exec 5)

then send the proof term back (a lambda term) to coq-serapi to parse into a "nice" AST for us (argh had to wrap it in a definition of coq returns a syntax error):

(Parse () "Definition id := (fun n : nat => eq_refl).")

then one gets the coq-ast (from the OCaml code I believe):

(Answer 2 Ack)
(Answer 2
 (ObjList
  ((CoqAst
    ((v
      ((control ()) (attrs ())
       (expr
        (VernacDefinition (NoDischarge Definition)
         (((v (Name (Id id)))
           (loc
            (((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1)
              (bol_pos_last 0) (bp 11) (ep 13)))))
          ())
         (DefineBody () ()
          ((v
            (CLambdaN
             ((CLocalAssum
               (((v (Name (Id n)))
                 (loc
                  (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                    (line_nb_last 1) (bol_pos_last 0) (bp 22) (ep 23))))))
               (Default Explicit)
               ((v
                 (CRef
                  ((v (Ser_Qualid (DirPath ()) (Id nat)))
                   (loc
                    (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                      (line_nb_last 1) (bol_pos_last 0) (bp 26) (ep 29)))))
                  ()))
                (loc
                 (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                   (line_nb_last 1) (bol_pos_last 0) (bp 26) (ep 29)))))))
             ((v
               (CRef
                ((v (Ser_Qualid (DirPath ()) (Id eq_refl)))
                 (loc
                  (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                    (line_nb_last 1) (bol_pos_last 0) (bp 33) (ep 40)))))
                ()))
              (loc
               (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                 (line_nb_last 1) (bol_pos_last 0) (bp 33) (ep 40)))))))
           (loc
            (((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1)
              (bol_pos_last 0) (bp 18) (ep 40)))))
          ())))))
     (loc
      (((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1)
        (bol_pos_last 0) (bp 0) (ep 42)))))))))
(Answer 2 Completed)

but if you inspect the s-expression more carefully there are potential issues. For example, reading the coq-serapi documentation we know we are getting a coq_object in the reply:

| CoqAst of Vernacexpr.vernac_control   (*
Coq Abstract Syntax tress, as produced by the parser

and thus the first thing is likely a vernac_control (or a CAst.t honestly I'm not sure what the and vernac_control = vernac_control_r CAst.t ocaml syntax means. But there are only two options so it's easy to systematize). The main issue is if we get the type CAst.t. Look at it's def:

type 'a t = private {
v : 'a;
loc : Loc.t option;
}

so basically v can be any type due to the type variable 'a. Which seems like a nightmare since how do I write a pattern match? Or a python if statement to detect what even the constructor options might be? I think this is the most serious issue if I want to even attempt to write a traversal for this. My fear is definitively confirmed since if you look at the s-expression I copy pasted we received plenty of v names in it...which makes we wonder how do I even traverse the coq-ast.

The other issue (which seems a bit more minor) is that we might get a record. Which is shown as a list in an s-expression...and I suppose we could infer what type of ocaml coq record it is from the lenght and the names of the "indices" but if I receive one that I didn't expect my code will crash.

So how does one traverse a s-expression/ocaml ast systematically?


Appendix 1:

I think this question is extremely related to this other one: What are Generic Arguments in Coq and how are they structured in their OCaml code? . I think so because this one is about coq term traversal but the other one points out the (apparent?) inconsistencies coq-serapi might give. Thus, there can't be a systematic coq traversal if the terms given to the user from the OCaml code is incosnsistent.

$\endgroup$
4
  • 3
    $\begingroup$ OCaml (and the other MLs) have had the glorious idea of placing type arguments to parametrized types before the type constructor. What is list int in Coq is int list in OCaml. vernac_control = vernac_control_r CAst.t means a vernac_control is a CAst.t (which gives location info) where 'a is vernac_control_r... OCaml is a statically typed language... if you just trace the type definitions there should never be confusion about what goes where. $\endgroup$
    – HTNW
    Jul 10 at 5:18
  • $\begingroup$ @HTNW fantastic answer! thank you. Not I realized that when I saw and vernac_control = vernac_control_r CAst.t in the mutual recursion definition, that I didn't know what that meant but now I see what it means. Thanks again! $\endgroup$ Jul 12 at 21:25
  • $\begingroup$ @HTNW curious, when we define 'a list in ocaml but I create an object Cons(1. []) -- 'a is known at run time, right? I feel there must be something wrong because OCaml is compiled but the current example you provided (and I provided) only seems to get around it because the new type defined defined it explicitly defined by the user e.g. as if we did type my_int_list = int list. This is the reason in the Coq AST it might work...but does this work in general? What about the runtime example I provided? $\endgroup$ Jul 12 at 21:32
  • $\begingroup$ I think this question is extremely related to this other one: proofassistants.stackexchange.com/questions/1601/… . I think so because this one is about coq term traversal but the other one points out the (apparent?) inconsistencies coq-serapi might give. Thus, there can't be a systematic coq traversal if the terms given to the user from the OCaml code is incosnsistent. $\endgroup$ Jul 15 at 15:44

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy