Skip to content

Commit

Permalink
Merge pull request #427 from ppedrot/we-will-rocq-you-pcoq
Browse files Browse the repository at this point in the history
Adapt w.r.t. coq/coq#19736.
  • Loading branch information
SkySkimmer authored Oct 23, 2024
2 parents 5e8d6ad + 91aa5e7 commit ee470bb
Show file tree
Hide file tree
Showing 4 changed files with 13 additions and 13 deletions.
18 changes: 9 additions & 9 deletions serapi/serapi_protocol.ml
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ module Extra = struct

(* Custom tokenizer *)
let rec stream_tok n_tok acc lstr =
let e = Gramlib.LStream.next (Pcoq.get_keyword_state()) lstr in
let e = Gramlib.LStream.next (Procq.get_keyword_state()) lstr in
let loc = Gramlib.LStream.get_loc n_tok lstr in
let l_tok = CAst.make ~loc e in
if Tok.(equal e EOI) then
Expand Down Expand Up @@ -541,7 +541,7 @@ module QueryUtil = struct
(* This should be moved Coq upstream *)
let _comments = ref []
let add_comments pa =
let comments = Pcoq.Parsable.comments pa |> List.rev in
let comments = Procq.Parsable.comments pa |> List.rev in
_comments := comments :: !_comments

let libobjects () =
Expand Down Expand Up @@ -584,7 +584,7 @@ let obj_query ~doc ~pstate ~env (opt : query_opt) (cmd : query_cmd) : coq_object
| TypeOf id -> snd (QueryUtil.info_of_id env id)
| Search -> [CoqString "Not Implemented"]
(* XXX: should set printing options in all queries *)
| Vernac q -> let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string q) in
| Vernac q -> let pa = Procq.Parsable.make (Gramlib.Stream.of_string q) in
Stm.query ~doc ~at:opt.sid ~route:opt.route pa; []
(* XXX: Should set the proper sid state *)
| Env -> [CoqEnv env]
Expand Down Expand Up @@ -699,14 +699,14 @@ module ControlUtil = struct
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 (Gramlib.Stream.of_string str) in
Pcoq.unfreeze pstate;
Pcoq.Entry.parse entry pa)
let entry = Procq.Constr.lconstr in
let pa = Procq.Parsable.make (Gramlib.Stream.of_string str) in
Procq.unfreeze pstate;
Procq.Entry.parse 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 (Gramlib.Stream.of_string sent) in
let pa = Procq.Parsable.make (Gramlib.Stream.of_string sent) in
let entry = Pvernac.main_entry in
Stm.parse_sentence ~doc ontop ~entry pa

Expand All @@ -719,7 +719,7 @@ module ControlUtil = struct
exception End_of_input

let add_sentences ~doc opts sent =
let pa = Pcoq.Parsable.make (Gramlib.Stream.of_string sent) in
let pa = Procq.Parsable.make (Gramlib.Stream.of_string sent) in
let i = ref 1 in
let acc = ref [] in
let stt = ref (Extra.value opts.ontop ~default:(Stm.get_current_state ~doc)) in
Expand Down
2 changes: 1 addition & 1 deletion sertop/sercomp.ml
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ let input_doc ~input ~in_file ~in_chan ~process ~doc ~sid =
| I_vernac ->
begin
let in_strm = Gramlib.Stream.of_channel in_chan in
let in_pa = Pcoq.Parsable.make ~loc:(Loc.initial (InFile { dirpath = None; file = in_file} )) in_strm in
let in_pa = Procq.Parsable.make ~loc:(Loc.initial (InFile { dirpath = None; file = in_file} )) in_strm in
try while true do
let doc, sid = !stt in
let east =
Expand Down
2 changes: 1 addition & 1 deletion sertop/sername.ml
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ let sername_doc = "sername Coq tool"
let do_require ~doc ~sid ~require_lib ~in_file =
let sent = Printf.sprintf "Require %s." require_lib in
let in_strm = Gramlib.Stream.of_string sent in
let in_pa = Pcoq.Parsable.make ~loc:(Loc.initial (InFile { dirpath = None; file = in_file})) in_strm in
let in_pa = Procq.Parsable.make ~loc:(Loc.initial (InFile { dirpath = None; file = in_file})) in_strm in
match Stm.parse_sentence ~doc ~entry:Pvernac.main_entry sid in_pa with
| Some ast ->
let doc, sid, tip = Stm.add ~doc ~ontop:sid false ast in
Expand Down
4 changes: 2 additions & 2 deletions sertop/sertok.ml
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ let load_file f =
(s)

let rec stream_tok n_tok acc str source begin_line begin_char =
let e = Gramlib.LStream.next (Pcoq.get_keyword_state()) str in
let e = Gramlib.LStream.next (Procq.get_keyword_state()) str in
let pre_loc : Loc.t = Gramlib.LStream.get_loc n_tok str in
let loc =
{ pre_loc with
Expand All @@ -48,7 +48,7 @@ let input_doc ~pp ~in_file ~in_chan ~doc ~sid =
let stt = ref (doc, sid) in
let in_strm = Gramlib.Stream.of_channel in_chan in
let source = Loc.InFile { dirpath = None; file = in_file } in
let in_pa = Pcoq.Parsable.make ~loc:(Loc.initial source) in_strm in
let in_pa = Procq.Parsable.make ~loc:(Loc.initial source) in_strm in
let in_bytes = load_file in_file in
try while true do
let l_pre_st = CLexer.Lexer.State.get () in
Expand Down

0 comments on commit ee470bb

Please sign in to comment.