From 1d0eb5d4d6fea88abc29798ee2004b2e27e952c6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 8 Mar 2017 03:22:22 +0100 Subject: [camlpX] Remove camlp4 compat layer. We remove the camlp4 compatibility layer, and try to clean up most structures. `parsing/compat` is gone. We added some documentation to the lexer/parser interfaces that are often obscured by module includes. --- plugins/funind/g_indfun.ml4 | 2 +- plugins/ltac/g_ltac.ml4 | 5 ++--- plugins/ltac/g_tactic.ml4 | 35 +++++++++++++++++------------------ plugins/ssrmatching/ssrmatching.ml4 | 8 +++----- 4 files changed, 23 insertions(+), 27 deletions(-) (limited to 'plugins') diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 368b23be3..cf2e42d2c 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -7,7 +7,6 @@ (************************************************************************) (*i camlp4deps: "grammar/grammar.cma" i*) open Ltac_plugin -open Compat open Util open Term open Pp @@ -17,6 +16,7 @@ open Indfun open Genarg open Stdarg open Misctypes +open Pcoq open Pcoq.Prim open Pcoq.Constr open Pltac diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index fd33a779d..ece0adb07 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -12,7 +12,6 @@ DECLARE PLUGIN "ltac_plugin" open Util open Pp -open Compat open Constrexpr open Tacexpr open Misctypes @@ -68,9 +67,9 @@ let _ = let test_bracket_ident = Gram.Entry.of_parser "test_bracket_ident" (fun strm -> - match get_tok (stream_nth 0 strm) with + match stream_nth 0 strm with | KEYWORD "[" -> - (match get_tok (stream_nth 1 strm) with + (match stream_nth 1 strm with | IDENT _ -> () | _ -> raise Stream.Failure) | _ -> raise Stream.Failure) diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index fa01baab7..4b3ca80af 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -14,7 +14,6 @@ open Genredexpr open Constrexpr open Libnames open Tok -open Compat open Misctypes open Locus open Decl_kinds @@ -34,11 +33,11 @@ let err () = raise Stream.Failure let test_lpar_id_coloneq = Gram.Entry.of_parser "lpar_id_coloneq" (fun strm -> - match get_tok (stream_nth 0 strm) with + match stream_nth 0 strm with | KEYWORD "(" -> - (match get_tok (stream_nth 1 strm) with + (match stream_nth 1 strm with | IDENT _ -> - (match get_tok (stream_nth 2 strm) with + (match stream_nth 2 strm with | KEYWORD ":=" -> () | _ -> err ()) | _ -> err ()) @@ -48,11 +47,11 @@ let test_lpar_id_coloneq = let test_lpar_id_rpar = Gram.Entry.of_parser "lpar_id_coloneq" (fun strm -> - match get_tok (stream_nth 0 strm) with + match stream_nth 0 strm with | KEYWORD "(" -> - (match get_tok (stream_nth 1 strm) with + (match stream_nth 1 strm with | IDENT _ -> - (match get_tok (stream_nth 2 strm) with + (match stream_nth 2 strm with | KEYWORD ")" -> () | _ -> err ()) | _ -> err ()) @@ -62,11 +61,11 @@ let test_lpar_id_rpar = let test_lpar_idnum_coloneq = Gram.Entry.of_parser "test_lpar_idnum_coloneq" (fun strm -> - match get_tok (stream_nth 0 strm) with + match stream_nth 0 strm with | KEYWORD "(" -> - (match get_tok (stream_nth 1 strm) with + (match stream_nth 1 strm with | IDENT _ | INT _ -> - (match get_tok (stream_nth 2 strm) with + (match stream_nth 2 strm with | KEYWORD ":=" -> () | _ -> err ()) | _ -> err ()) @@ -76,11 +75,11 @@ let test_lpar_idnum_coloneq = let test_lpar_id_colon = Gram.Entry.of_parser "lpar_id_colon" (fun strm -> - match get_tok (stream_nth 0 strm) with + match stream_nth 0 strm with | KEYWORD "(" -> - (match get_tok (stream_nth 1 strm) with + (match stream_nth 1 strm with | IDENT _ -> - (match get_tok (stream_nth 2 strm) with + (match stream_nth 2 strm with | KEYWORD ":" -> () | _ -> err ()) | _ -> err ()) @@ -91,30 +90,30 @@ let check_for_coloneq = Gram.Entry.of_parser "lpar_id_colon" (fun strm -> let rec skip_to_rpar p n = - match get_tok (List.last (Stream.npeek n strm)) with + match List.last (Stream.npeek n strm) with | KEYWORD "(" -> skip_to_rpar (p+1) (n+1) | KEYWORD ")" -> if Int.equal p 0 then n+1 else skip_to_rpar (p-1) (n+1) | KEYWORD "." -> err () | _ -> skip_to_rpar p (n+1) in let rec skip_names n = - match get_tok (List.last (Stream.npeek n strm)) with + match List.last (Stream.npeek n strm) with | IDENT _ | KEYWORD "_" -> skip_names (n+1) | KEYWORD ":" -> skip_to_rpar 0 (n+1) (* skip a constr *) | _ -> err () in let rec skip_binders n = - match get_tok (List.last (Stream.npeek n strm)) with + match List.last (Stream.npeek n strm) with | KEYWORD "(" -> skip_binders (skip_names (n+1)) | IDENT _ | KEYWORD "_" -> skip_binders (n+1) | KEYWORD ":=" -> () | _ -> err () in - match get_tok (stream_nth 0 strm) with + match stream_nth 0 strm with | KEYWORD "(" -> skip_binders 2 | _ -> err ()) let lookup_at_as_comma = Gram.Entry.of_parser "lookup_at_as_comma" (fun strm -> - match get_tok (stream_nth 0 strm) with + match stream_nth 0 strm with | KEYWORD (","|"at"|"as") -> () | _ -> err ()) diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 4d5594633..3d0232d94 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -10,7 +10,7 @@ (* Defining grammar rules with "xx" in it automatically declares keywords too, * we thus save the lexer to restore it at the end of the file *) -let frozen_lexer = CLexer.freeze () ;; +let frozen_lexer = CLexer.get_keyword_state () ;; (*i camlp4use: "pa_extend.cmo" i*) (*i camlp4deps: "grammar/grammar.cma" i*) @@ -1040,7 +1040,7 @@ let interp_open_constr ist gl gc = let pf_intern_term ist gl (_, c) = glob_constr ist (pf_env gl) c let interp_term ist gl (_, c) = (interp_open_constr ist gl c) let pr_ssrterm _ _ _ = pr_term -let input_ssrtermkind strm = match Compat.get_tok (stream_nth 0 strm) with +let input_ssrtermkind strm = match stream_nth 0 strm with | Tok.KEYWORD "(" -> '(' | Tok.KEYWORD "@" -> '@' | _ -> ' ' @@ -1057,8 +1057,6 @@ ARGUMENT EXTEND cpattern | [ "Qed" constr(c) ] -> [ mk_lterm c ] END -let (!@) = Compat.to_coqloc - GEXTEND Gram GLOBAL: cpattern; cpattern: [[ k = ssrtermkind; c = constr -> @@ -1444,6 +1442,6 @@ END (* The user is supposed to Require Import ssreflect or Require ssreflect *) (* and Import ssreflect.SsrSyntax to obtain these keywords and as a *) (* consequence the extended ssreflect grammar. *) -let () = CLexer.unfreeze frozen_lexer ;; +let () = CLexer.set_keyword_state frozen_lexer ;; (* vim: set filetype=ocaml foldmethod=marker: *) -- cgit v1.2.3