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. --- grammar/argextend.mlp | 7 ++-- grammar/compat5.mlp | 23 ------------- grammar/compat5b.mlp | 23 ------------- grammar/gramCompat.mlp | 86 ------------------------------------------------ grammar/q_util.mli | 2 -- grammar/q_util.mlp | 10 +++--- grammar/tacextend.mlp | 17 +++++++--- grammar/vernacextend.mlp | 14 ++++---- 8 files changed, 26 insertions(+), 156 deletions(-) delete mode 100644 grammar/compat5.mlp delete mode 100644 grammar/compat5b.mlp delete mode 100644 grammar/gramCompat.mlp (limited to 'grammar') diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp index d0ab5d803..aaf3afe43 100644 --- a/grammar/argextend.mlp +++ b/grammar/argextend.mlp @@ -7,11 +7,13 @@ (************************************************************************) open Q_util -open GramCompat -let loc = CompatLoc.ghost +let loc = Ploc.dummy let default_loc = <:expr< Loc.ghost >> +let declare_str_items loc l = + MLast.StDcl (loc, Ploc.VaVal l) (* correspond to <:str_item< declare $list:l'$ end >> *) + let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >> let rec make_wit loc = function @@ -185,7 +187,6 @@ let declare_vernac_argument loc s pr cl = >> ] open Pcaml -open PcamlSig (* necessary for camlp4 *) EXTEND GLOBAL: str_item; diff --git a/grammar/compat5.mlp b/grammar/compat5.mlp deleted file mode 100644 index 8473a1fb7..000000000 --- a/grammar/compat5.mlp +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* ] -> - [< '(KEYWORD "EXTEND", loc); my_token_filter s >] - | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >] - | [< >] -> [< >] - -let _ = - Token.Filter.define_filter (Gram.get_filter()) - (fun prev strm -> prev (my_token_filter strm)) diff --git a/grammar/compat5b.mlp b/grammar/compat5b.mlp deleted file mode 100644 index 46802a825..000000000 --- a/grammar/compat5b.mlp +++ /dev/null @@ -1,23 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* ] -> - [< 't; '(UIDENT "Gram", Loc.ghost); my_token_filter s >] - | [< 'tokloc; s >] -> [< 'tokloc; my_token_filter s >] - | [< >] -> [< >] - -let _ = - Token.Filter.define_filter (Gram.get_filter()) - (fun prev strm -> prev (my_token_filter strm)) diff --git a/grammar/gramCompat.mlp b/grammar/gramCompat.mlp deleted file mode 100644 index 6246da7bb..000000000 --- a/grammar/gramCompat.mlp +++ /dev/null @@ -1,86 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* > *) -ELSE - Ast.stSem_of_list l -END - -(** Quotation difference for match clauses *) - -let default_patt loc = - (<:patt< _ >>, vala None, <:expr< failwith "Extension: cannot occur" >>) - -IFDEF CAMLP5 THEN - -let make_fun loc cl = - let l = cl @ [default_patt loc] in - MLast.ExFun (loc, vala l) (* correspond to <:expr< fun [ $list:l$ ] >> *) - -ELSE - -let make_fun loc cl = - let mk_when = function - | Some w -> w - | None -> Ast.ExNil loc - in - let mk_clause (patt,optwhen,expr) = - (* correspond to <:match_case< ... when ... -> ... >> *) - Ast.McArr (loc, patt, mk_when optwhen, expr) in - let init = mk_clause (default_patt loc) in - let add_clause x acc = Ast.McOr (loc, mk_clause x, acc) in - let l = List.fold_right add_clause cl init in - Ast.ExFun (loc,l) (* correspond to <:expr< fun [ $l$ ] >> *) - -END diff --git a/grammar/q_util.mli b/grammar/q_util.mli index 37ec1d56a..5b3eb3202 100644 --- a/grammar/q_util.mli +++ b/grammar/q_util.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open GramCompat (* necessary for camlp4 *) - type argument_type = | ListArgType of argument_type | OptArgType of argument_type diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp index 0dd096ef7..8b930cf36 100644 --- a/grammar/q_util.mlp +++ b/grammar/q_util.mlp @@ -8,8 +8,6 @@ (* This file defines standard combinators to build ml expressions *) -open GramCompat - type argument_type = | ListArgType of argument_type | OptArgType of argument_type @@ -33,17 +31,17 @@ let mlexpr_of_list f l = List.fold_right (fun e1 e2 -> let e1 = f e1 in - let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in + let loc = Ploc.encl (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in <:expr< [$e1$ :: $e2$] >>) - l (let loc = CompatLoc.ghost in <:expr< [] >>) + l (let loc = Ploc.dummy in <:expr< [] >>) let mlexpr_of_pair m1 m2 (a1,a2) = let e1 = m1 a1 and e2 = m2 a2 in - let loc = CompatLoc.merge (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in + let loc = Ploc.encl (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in <:expr< ($e1$, $e2$) >> (* We don't give location for tactic quotation! *) -let loc = CompatLoc.ghost +let loc = Ploc.dummy let mlexpr_of_bool = function diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 8c0614a7b..f57be9022 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -10,7 +10,15 @@ open Q_util open Argextend -open GramCompat + +(** Quotation difference for match clauses *) + +let default_patt loc = + (<:patt< _ >>, Ploc.VaVal None, <:expr< failwith "Extension: cannot occur" >>) + +let make_fun loc cl = + let l = cl @ [default_patt loc] in + MLast.ExFun (loc, Ploc.VaVal l) (* correspond to <:expr< fun [ $list:l$ ] >> *) let dloc = <:expr< Loc.ghost >> @@ -41,11 +49,11 @@ let rec make_let raw e = function let make_clause (pt,_,e) = (make_patt pt, - vala None, + Ploc.VaVal None, make_let false e pt) let make_fun_clauses loc s l = - let map c = GramCompat.make_fun loc [make_clause c] in + let map c = make_fun loc [make_clause c] in mlexpr_of_list map l let get_argt e = <:expr< (fun e -> match e with [ Genarg.ExtraArg tag -> tag | _ -> assert False ]) $e$ >> @@ -100,7 +108,7 @@ let declare_tactic loc tacname ~level classification clause = match clause with whole-prof tactics like [shelve_unifiable]. *) <:expr< fun _ $lid:"ist"$ -> $tac$ >> | _ -> - let f = GramCompat.make_fun loc [patt, vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in + let f = make_fun loc [patt, Ploc.VaVal None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in <:expr< Tacinterp.lift_constr_tac_to_ml_tac $vars$ $f$ >> in (** Arguments are not passed directly to the ML tactic in the TacML node, @@ -129,7 +137,6 @@ let declare_tactic loc tacname ~level classification clause = match clause with ] open Pcaml -open PcamlSig (* necessary for camlp4 *) EXTEND GLOBAL: str_item; diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index 04b117fba..d4857b1df 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -11,7 +11,6 @@ open Q_util open Argextend open Tacextend -open GramCompat type rule = { r_head : string option; @@ -37,7 +36,7 @@ let rec make_let e = function let make_clause { r_patt = pt; r_branch = e; } = (make_patt pt, - vala None, + Ploc.VaVal None, make_let e pt) (* To avoid warnings *) @@ -55,11 +54,11 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = match c ,cg with | Some c, _ -> (make_patt pt, - vala None, + Ploc.VaVal None, make_let (mk_ignore c pt) pt) | None, Some cg -> (make_patt pt, - vala None, + Ploc.VaVal None, <:expr< fun () -> $cg$ $str:s$ >>) | None, None -> prerr_endline (("Vernac entry \""^s^"\" misses a classifier. "^ @@ -82,7 +81,7 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = ("Specific classifiers have precedence over global "^ "classifiers. Only one classifier is called.") ^ "\n"); (make_patt pt, - vala None, + Ploc.VaVal None, <:expr< fun () -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) let make_fun_clauses loc s l = @@ -91,13 +90,13 @@ let make_fun_clauses loc s l = | None -> false | Some () -> true in - let cl = GramCompat.make_fun loc [make_clause c] in + let cl = make_fun loc [make_clause c] in <:expr< ($mlexpr_of_bool depr$, $cl$)>> in mlexpr_of_list map l let make_fun_classifiers loc s c l = - let cl = List.map (fun x -> GramCompat.make_fun loc [make_clause_classifier c s x]) l in + let cl = List.map (fun x -> make_fun loc [make_clause_classifier c s x]) l in mlexpr_of_list (fun x -> x) cl let make_prod_item = function @@ -128,7 +127,6 @@ let declare_command loc s c nt cl = } >> ] open Pcaml -open PcamlSig (* necessary for camlp4 *) EXTEND GLOBAL: str_item; -- cgit v1.2.3