Do I always have to wrap anonymous functions in a definition for Coq Serapi to parse it for me?

[brando90]

I want to get the "coq ast" for lambda functions in coq. e.g. I did the following but all fail:

rlwrap sertop --printer=human

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

(Parse ((ontop 5)) "(fun n : nat => eq_refl).")
(Parse () "(fun n : nat => eq_refl).")
(Parse ((ontop 5)) "(fun n : nat => eq_refl)")

only until I do:

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

Does it work. Is it not possible parse it with serapi without wraping it in a definition?

---

Entire run:

(Add () "
Theorem add_easy_0: forall n:nat, 0 + n = n. simpl. reflexivity. Show Proof.")
(Answer 0 Ack)
(Answer 0
 (Added 2
  ((fname ToplevelInput) (line_nb 2) (bol_pos 1) (line_nb_last 2)
   (bol_pos_last 1) (bp 1) (ep 45))
  NewTip))
(Answer 0
 (Added 3
  ((fname ToplevelInput) (line_nb 2) (bol_pos 1) (line_nb_last 2)
   (bol_pos_last 1) (bp 46) (ep 52))
  NewTip))
(Answer 0
 (Added 4
  ((fname ToplevelInput) (line_nb 2) (bol_pos 1) (line_nb_last 2)
   (bol_pos_last 1) (bp 53) (ep 65))
  NewTip))
(Answer 0
 (Added 5
  ((fname ToplevelInput) (line_nb 2) (bol_pos 1) (line_nb_last 2)
   (bol_pos_last 1) (bp 66) (ep 77))
  NewTip))
(Answer 0 Completed)

(Exec 5)
(Answer 1 Ack)
(Feedback
 ((doc_id 0) (span_id 5) (route 0) (contents (ProcessingIn master))))
(Feedback
 ((doc_id 0) (span_id 4) (route 0) (contents (ProcessingIn master))))
(Feedback
 ((doc_id 0) (span_id 3) (route 0) (contents (ProcessingIn master))))
(Feedback
 ((doc_id 0) (span_id 2) (route 0) (contents (ProcessingIn master))))
(Feedback ((doc_id 0) (span_id 1) (route 0) (contents Processed)))
(Feedback ((doc_id 0) (span_id 2) (route 0) (contents Processed)))
(Feedback ((doc_id 0) (span_id 3) (route 0) (contents Processed)))
(Feedback ((doc_id 0) (span_id 4) (route 0) (contents Processed)))
(Feedback
 ((doc_id 0) (span_id 5) (route 0)
  (contents
   (Message (level Notice) (loc ())
    (pp
     (Pp_box (Pp_hovbox 1)
      (Pp_glue
       ((Pp_string "(")
        (Pp_box (Pp_hovbox 0)
         (Pp_glue
          ((Pp_box (Pp_hovbox 2)
            (Pp_glue
             ((Pp_tag constr.keyword (Pp_string fun)) (Pp_print_break 1 0)
              (Pp_box (Pp_hovbox 1)
               (Pp_glue
                ((Pp_string "n : ") (Pp_tag constr.variable (Pp_string nat))))))))
           (Pp_print_break 1 0) (Pp_string =>) (Pp_print_break 1 0)
           (Pp_tag constr.variable (Pp_string eq_refl)))))
        (Pp_string ")")))))
    (str "(fun n : nat => eq_refl)")))))
(Feedback ((doc_id 0) (span_id 5) (route 0) (contents Processed)))
(Answer 1 Completed)

(Parse ((ontop 5)) "(fun n : nat => eq_refl).")
(Answer 2 Ack)
(Answer 2
 (CoqExn
  ((loc
    (((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1)
      (bol_pos_last 0) (bp 7) (ep 8))))
   (stm_ids ()) (backtrace (Backtrace ()))
   (exn
    (Stream.Error "[input_fun] or '=>' expected (in [tactic:binder_tactic])"))
   (pp
    (Pp_box (Pp_hovbox 0)
     (Pp_glue
      ((Pp_string "Syntax error: ")
       (Pp_string "[input_fun] or '=>' expected (in [tactic:binder_tactic])")
       (Pp_string .)))))
   (str
    "Syntax error: [input_fun] or '=>' expected (in [tactic:binder_tactic])."))))
(Answer 2 Completed)

(Parse ((ontop 5)) "(fun n : nat => eq_refl)")
(Answer 3 Ack)
(Answer 3
 (CoqExn
  ((loc
    (((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1)
      (bol_pos_last 0) (bp 7) (ep 8))))
   (stm_ids ()) (backtrace (Backtrace ()))
   (exn
    (Stream.Error "[input_fun] or '=>' expected (in [tactic:binder_tactic])"))
   (pp
    (Pp_box (Pp_hovbox 0)
     (Pp_glue
      ((Pp_string "Syntax error: ")
       (Pp_string "[input_fun] or '=>' expected (in [tactic:binder_tactic])")
       (Pp_string .)))))
   (str
    "Syntax error: [input_fun] or '=>' expected (in [tactic:binder_tactic])."))))
(Answer 3 Completed)

(Parse () "(fun n : nat => eq_refl).")
(Answer 4 Ack)
(Answer 4
 (CoqExn
  ((loc
    (((fname ToplevelInput) (line_nb 1) (bol_pos 0) (line_nb_last 1)
      (bol_pos_last 0) (bp 7) (ep 8))))
   (stm_ids ()) (backtrace (Backtrace ()))
   (exn
    (Stream.Error "[input_fun] or '=>' expected (in [tactic:binder_tactic])"))
   (pp
    (Pp_box (Pp_hovbox 0)
     (Pp_glue
      ((Pp_string "Syntax error: ")
       (Pp_string "[input_fun] or '=>' expected (in [tactic:binder_tactic])")
       (Pp_string .)))))
   (str
    "Syntax error: [input_fun] or '=>' expected (in [tactic:binder_tactic])."))))
(Answer 4 Completed)

(Parse () "Definition id := (fun n : nat => eq_refl).")
(Answer 5 Ack)
(Answer 5
 (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 5 Completed)

[ejgallego]

Yup, it is not possible as of today, parse does call the non terminal for commands. It'd be easy to implement that as a parameter, so indeed we could provide an option to parse to do what you want.