How to have serapi return to me coq human strings from arbitrary subterms in a coq-ast?
brando90 opened this issue · 5 comments
brando90 commented
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 commented
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 commented
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 commented
I want to traverse arbitrary cast trees and extract whatever argument/part I want and get it back as a coq human string.
ejgallego commented
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.