Merge pull request #282 from ejgallego/v8.16+allow_coqconstr

[serapi] Allow to parse different entries (expressions added)

CHANGES.md

@@ -3,6 +3,8 @@
  - [sertop] Allow to set `--coqlib` using the `COQLIB` environment
             variable. The cmdline argument option still has
             precedence.
+ - [serapi] Allow to parse expressions too with
+            `(Parse (entry Constr) $text)` (@ejgallego, fixes #272)
 
 ## Version 0.16.0:
 

serapi/serapi_protocol.ml

@@ -643,16 +643,21 @@ let obj_limit limit objs =
 let doc_id = ref 0
 
 (* XXX: Needs to take into account possibly local proof state *)
-let pstate_of_st m = match m with
+let proof_state_of_st m = match m with
   | Stm.Valid (Some { Vernacstate.lemmas; _ } ) ->
     lemmas
   | _ -> None
 
+let parsing_state_of_st m = match m with
+  | Stm.Valid (Some { Vernacstate.parsing; _ } ) ->
+    Some parsing
+  | _ -> None
+
 let exec_query opt cmd =
   let doc = Stm.get_doc !doc_id in
   let st = Stm.state_of_id ~doc opt.sid in
   let sigma, env = Extcoq.context_of_st st in
-  let pstate = pstate_of_st st in
+  let pstate = proof_state_of_st st in
 
   let pstate = Option.map (Vernacstate.LemmaStack.with_top ~f:(fun p -> p)) pstate in
   let res = obj_query ~doc ~pstate ~env opt cmd in
@@ -686,8 +691,13 @@ let coq_protect st e =
     (* let msg = str msg ++ fnl () ++ CErrors.print ~info e in *)
     (* Richpp.richpp_of_pp msg *)
 
+type parse_entry = Vernac | Constr
+
+(** parse [ontop] of the given sentence with entry [entry] *)
 type parse_opt =
-  { ontop  : Stateid.t option [@sexp.option] }
+  { ontop  : Stateid.t option [@sexp.option]
+  ; entry : parse_entry [@default Vernac]
+  }
 
 type add_opts = {
   lim    : int       option [@sexp.option];
@@ -708,12 +718,26 @@ module ControlUtil = struct
   let _dump_doc () =
     Format.eprintf "%a@\n%!" pp_doc !cur_doc
 
-  let parse_sentence ~doc ~(opt : parse_opt) sent =
-    let ontop = Extra.value opt.ontop ~default:(Stm.get_current_state ~doc) in
+  let parse_expr ~doc ~ontop str =
+    let ontop = Extra.value ontop ~default:(Stm.get_current_state ~doc) in
+    parsing_state_of_st (Stm.state_of_id ~doc ontop)
+    |> Option.map (fun pstate ->
+        let entry = Pcoq.Constr.lconstr in
+        let pa = Pcoq.Parsable.make (Ser_stream.of_string str) in
+        Vernacstate.Parser.parse pstate entry pa)
+
+  let parse_sentence ~doc ~ontop sent =
+    let ontop = Extra.value ontop ~default:(Stm.get_current_state ~doc) in
     let pa = Pcoq.Parsable.make (Ser_stream.of_string sent) in
     let entry = Pvernac.main_entry in
     Stm.parse_sentence ~doc ontop ~entry pa
 
+  let parse_entry ~doc ~(opt : parse_opt) str =
+    let ontop = opt.ontop in
+    match opt.entry with
+    | Vernac -> Option.map (fun x -> [CoqAst x]) (parse_sentence ~doc ~ontop str)
+    | Constr -> Option.map (fun x -> [CoqExpr x]) (parse_expr ~doc ~ontop str)
+
   exception End_of_input
 
   let add_sentences ~doc opts sent =
@@ -907,7 +931,7 @@ let exec_cmd (st : State.t) (cmd : cmd) : answer_kind list * State.t =
         in
         let _doc = Stm.observe ~doc opts.sid in
         let pst = Stm.state_of_id ~doc opts.sid in
-        let pstate = pstate_of_st pst in
+        let pstate = proof_state_of_st pst in
         Serapi_doc.save_vo ~doc ~pstate ~in_file ?ldir:st.ldir (); []
     end
   | Add (opt, s) ->
@@ -922,8 +946,8 @@ let exec_cmd (st : State.t) (cmd : cmd) : answer_kind list * State.t =
     let sigma, env = Extcoq.context_of_st st in
     [ObjList [obj_print env sigma opts.pp obj]]
   | Parse(opt,s) ->
-    Option.cata (fun ast -> [ObjList [CoqAst ast]]) []
-      ControlUtil.(parse_sentence ~doc ~opt s)
+    ControlUtil.(parse_entry ~doc ~opt s)
+    |> Option.cata (fun objs -> [ObjList objs]) []
   | Join              -> ignore(Stm.join ~doc); []
   | Finish            -> ignore(Stm.finish ~doc); []
   (*  *)

serapi/serapi_protocol.mli

@@ -187,7 +187,7 @@ type coq_object =
   | CoqDP        of Names.DirPath.t
   (** Coq "Logical" Paths, used for module and section names *)
   | CoqAst       of Vernacexpr.vernac_control
-  (** Coq Abstract Syntax tress, as produced by the parser *)
+  (** Coq Abstract Syntax trees for statements, as produced by the parser *)
   | CoqOption    of Goptions.option_name * Goptions.option_state
   (** Coq Options, as in [Set Resolution Depth] *)
   | CoqConstr    of Constr.constr
@@ -377,12 +377,14 @@ end
 
 (** {4 Adding a new sentence } *)
 
+type parse_entry = Vernac | Constr
+
+(** parse [ontop] of the given sentence with entry [entry] *)
 type parse_opt =
   { ontop  : Stateid.t option [@sexp.option]
-  (** parse [ontop] of the given sentence *)
+  ; entry : parse_entry [@default Vernac]
   }
 
-
 (** [Add] will take a string and parse all the sentences on it, until an error of the end is found.
     Options for [Add] are: *)
 type add_opts = {

sertop/sertop_ser.ml

@@ -273,6 +273,10 @@ type save_opts =
   [%import: Serapi.Serapi_protocol.save_opts]
   [@@deriving sexp]
 
+type parse_entry =
+  [%import: Serapi.Serapi_protocol.parse_entry]
+  [@@deriving sexp]
+
 type parse_opt =
   [%import: Serapi.Serapi_protocol.parse_opt
   [@with