How to have serapi return to me coq human strings from arbitrary subterms in a coq-ast?

[brando90]

I want to get the human string after I extract valid sub trees from a coq-serapi ast. e.g. I have

(GenArg raw (ExtraArg tactic)
           (TacArg
            ((v
              (TacCall
               ((v
                 (((v (Ser_Qualid (DirPath ()) (Id ___hole)))
                   (loc
                    (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                      (line_nb_last 1) (bol_pos_last 0) (bp 1) (ep 8)))))
                  ((Reference
                    ((v (Ser_Qualid (DirPath ()) (Id O)))
                     (loc
                      (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                        (line_nb_last 1) (bol_pos_last 0) (bp 9) (ep 10))))) )) ))
                (loc
                 (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                   (line_nb_last 1) (bol_pos_last 0) (bp 1) (ep 10)))))))
             (loc
              (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                (line_nb_last 1) (bol_pos_last 0) (bp 1) (ep 10)))))))

I want to get the human representation O by feeding

((Reference
                    ((v (Ser_Qualid (DirPath ()) (Id O)))
                     (loc
                      (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                        (line_nb_last 1) (bol_pos_last 0) (bp 9) (ep 10))))) ))

to serapi, but it seems whenever I try to serapi returns errors to me. How do you do this with serapi?

[brando90]

why doesn't this work:

(Print ((sid 6) (pp ((pp_format PpStr)))) 
(CoqGenArg
(GenArg raw (ExtraArg tactic)
(TacArg
(Reference
                    ((v (Ser_Qualid (DirPath ()) (Id O)))
                     (loc
                      (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                        (line_nb_last 1) (bol_pos_last 0) (bp 9) (ep 10))))) )

)
)
)

)

error msg is confusing to me:

(Of_sexp_error
 "serlib/ser_cAst.ml.L.t_of_sexp: record conversion: only pairs expected, their first element must be an atom"
 (invalid_sexp Reference))

[brando90]

why does the above fail but this work?

(Print ((sid 6) (pp ((pp_format PpStr))))
(
CoqGenArg
(GenArg raw (ExtraArg tactic)
           (TacArg
            ((v
              (TacCall
               ((v
                 (((v (Ser_Qualid (DirPath ()) (Id ___hole)))
                   (loc
                    (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                      (line_nb_last 1) (bol_pos_last 0) (bp 1) (ep 8)))))
                  ((Reference
                    ((v (Ser_Qualid (DirPath ()) (Id O)))
                     (loc
                      (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                        (line_nb_last 1) (bol_pos_last 0) (bp 9) (ep 10))))) )) ))
                (loc
                 (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                   (line_nb_last 1) (bol_pos_last 0) (bp 1) (ep 10)))))))
             (loc
              (((fname ToplevelInput) (line_nb 1) (bol_pos 0)
                (line_nb_last 1) (bol_pos_last 0) (bp 1) (ep 10)))))))
)
)
(Answer 9 Ack)
(Answer 9 (ObjList ((CoqString "___hole O"))))
(Answer 9 Completed)

[brando90]

I want to traverse arbitrary cast trees and extract whatever argument/part I want and get it back as a coq human string.

[ejgallego]

That's a reasonable feature request, however note that it would require to extend CoqObject. You can indeed use the CoqAst object to print sub-asts , but you'll need to do the full wrapping.

[ejgallego]

Duplicate of #272