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 and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.