1
$\begingroup$

See the argument for TacArg:

  | TacArg of ('t, 'dtrm, 'p, 'c, 'r, 'n, 'tacexpr, 'l) gen_tactic_arg

but the reply has a type CAst.t as an argument for TacArg:

(Parse () "(___hole O).")
(Answer 24 Ack)
(Answer 24
 (ObjList
  ((CoqAst
    ((v
      ((control ()) (attrs ())
       (expr
        (VernacExtend (VernacSolve 0)
         ((GenArg raw (OptArg (ExtraArg ltac_selector)) ())
          (GenArg raw (OptArg (ExtraArg ltac_info)) ())
          (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)))))))
          (GenArg raw (ExtraArg ltac_use_default) false))))))
     (loc
      (((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1)
        (bol_pos_last 0) (bp 0) (ep 12)))))))))
(Answer 24 Completed

doesn't make sense to me. Why?


In addition if I send it some TacArg with value CAst.t it parses it correctly but I think it shouldn't:

(Print ((sid 6) (pp ((pp_format PpStr))))
(CoqGenArg
(GenArg raw (ExtraArg tactic)
 (TacArg
  ((v
    (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)))))))
)
)
(Answer 23 Ack)
(Answer 23 (ObjList ((CoqString O))))
(Answer 23 Completed)

I suppose this is in an attempt to do: How does one systematically traverse OCaml representations of Coq ASTs terms?


cross: https://github.com/ejgallego/coq-serapi/issues/275

$\endgroup$

0

Your Answer

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

Browse other questions tagged or ask your own question.