From f25396b3a35ea5cd64b8b68670e66a14a78c418c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 19 Mar 2016 17:04:07 +0100 Subject: Further reducing the dependencies of the EXTEND macros. --- grammar/argextend.ml4 | 15 +++++---------- grammar/grammar.mllib | 7 ------- grammar/q_util.ml4 | 2 +- grammar/tacextend.ml4 | 23 ++++------------------- grammar/vernacextend.ml4 | 20 ++++++++++++-------- 5 files changed, 22 insertions(+), 45 deletions(-) (limited to 'grammar') diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index bebde706e..801229bcb 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -16,11 +16,6 @@ open Extend let loc = CompatLoc.ghost let default_loc = <:expr< Loc.ghost >> -let qualified_name loc s = - let path = CString.split '.' s in - let (name, path) = CList.sep_last path in - qualified_name loc path name - let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >> let rec make_wit loc = function @@ -56,7 +51,7 @@ let make_rule loc (prods,act) = <:expr< Extend.Rule $make_prod (List.rev prods)$ $make_act loc act prods$ >> let is_ident x = function -| <:expr< $lid:s$ >> -> CString.equal s x +| <:expr< $lid:s$ >> -> (s : string) = x | _ -> false let make_extend loc s cl wit = match cl with @@ -85,7 +80,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = let glob = match g with | None -> begin match rawtyp with - | Genarg.ExtraArgType s' when CString.equal s s' -> + | Genarg.ExtraArgType s' when s = s' -> <:expr< fun ist v -> (ist, v) >> | _ -> <:expr< fun ist v -> @@ -100,7 +95,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = let interp = match f with | None -> begin match globtyp with - | Genarg.ExtraArgType s' when CString.equal s s' -> + | Genarg.ExtraArgType s' when s = s' -> <:expr< fun ist v -> Ftactic.return v >> | _ -> <:expr< fun ist x -> @@ -120,7 +115,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = let subst = match h with | None -> begin match globtyp with - | Genarg.ExtraArgType s' when CString.equal s s' -> + | Genarg.ExtraArgType s' when s = s' -> <:expr< fun s v -> v >> | _ -> <:expr< fun s x -> @@ -132,7 +127,7 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = let dyn = match typ with | `Uniform typ -> let is_new = match typ with - | Genarg.ExtraArgType s' when CString.equal s s' -> true + | Genarg.ExtraArgType s' when s = s' -> true | _ -> false in if is_new then <:expr< None >> diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 42fc73878..9b24c9797 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -1,15 +1,8 @@ Coq_config -Hashset -Hashcons -CMap -Int -Option Store Exninfo Loc -CList -CString Tok Compat diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index d91bfd7b8..bde1e7651 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -57,7 +57,7 @@ let rec mlexpr_of_prod_entry_key f = function | Extend.Uentry e -> <:expr< Extend.Aentry $f e$ >> | Extend.Uentryl (e, l) -> (** Keep in sync with Pcoq! *) - assert (CString.equal e "tactic"); + assert (e = "tactic"); if l = 5 then <:expr< Extend.Aentry (Pcoq.name_of_entry Pcoq.Tactic.binder_tactic) >> else <:expr< Extend.Aentryl (Pcoq.name_of_entry Pcoq.Tactic.tactic_expr) $mlexpr_of_int l$ >> diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 1951b8b45..a34b880ae 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -24,15 +24,6 @@ let rec make_patt = function <:patt< [ $lid:p$ :: $make_patt l$ ] >> | _::l -> make_patt l -let rec mlexpr_of_argtype loc = function - | Genarg.ListArgType t -> <:expr< Genarg.ListArgType $mlexpr_of_argtype loc t$ >> - | Genarg.OptArgType t -> <:expr< Genarg.OptArgType $mlexpr_of_argtype loc t$ >> - | Genarg.PairArgType (t1,t2) -> - let t1 = mlexpr_of_argtype loc t1 in - let t2 = mlexpr_of_argtype loc t2 in - <:expr< Genarg.PairArgType $t1$ $t2$ >> - | Genarg.ExtraArgType s -> <:expr< Genarg.ExtraArgType $str:s$ >> - let rec make_let raw e = function | [] -> <:expr< fun $lid:"ist"$ -> $e$ >> | ExtNonTerminal (t, _, p) :: l -> @@ -44,12 +35,6 @@ let rec make_let raw e = function <:expr< let $lid:p$ = $v$ in $e$ >> | _::l -> make_let raw e l -let rec extract_signature = function - | [] -> [] - | ExtNonTerminal (t, _, _) :: l -> t :: extract_signature l - | _::l -> extract_signature l - - let make_clause (pt,_,e) = (make_patt pt, vala None, @@ -99,13 +84,13 @@ let declare_tactic loc s c cl = match cl with let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in let ml = <:expr< { Tacexpr.mltac_name = $se$; Tacexpr.mltac_index = 0 } >> in let name = mlexpr_of_string name in - let tac = + let tac = match rem with + | [] -> (** Special handling of tactics without arguments: such tactics do not do a Proofview.Goal.nf_enter to compute their arguments. It matters for some whole-prof tactics like [shelve_unifiable]. *) - if CList.is_empty rem then <:expr< fun _ $lid:"ist"$ -> $tac$ >> - else + | _ -> let f = Compat.make_fun loc [patt, vala None, <:expr< fun $lid:"ist"$ -> $tac$ >>] in <:expr< Tacinterp.lift_constr_tac_to_ml_tac $vars$ $f$ >> in @@ -178,7 +163,7 @@ EXTEND let e = parse_user_entry e sep in ExtNonTerminal (type_of_user_symbol e, e, s) | s = STRING -> - let () = if CString.is_empty s then failwith "Empty terminal." in + let () = if s = "" then failwith "Empty terminal." in ExtTerminal s ] ] ; diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 453907689..40e327c37 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -43,9 +43,11 @@ let make_clause { r_patt = pt; r_branch = e; } = (* To avoid warnings *) let mk_ignore c pt = - let names = CList.map_filter (function - | ExtNonTerminal (_, _, p) -> Some p - | _ -> None) pt in + let fold accu = function + | ExtNonTerminal (_, _, p) -> p :: accu + | _ -> accu + in + let names = List.fold_left fold [] pt in let fold accu id = <:expr< let _ = $lid:id$ in $accu$ >> in let names = List.fold_left fold <:expr< () >> names in <:expr< do { let _ = $names$ in $c$ } >> @@ -99,10 +101,12 @@ let make_fun_classifiers loc s c l = let cl = List.map (fun x -> Compat.make_fun loc [make_clause_classifier c s x]) l in mlexpr_of_list (fun x -> x) cl -let mlexpr_of_clause = - mlexpr_of_list - (fun { r_head = a; r_patt = b; } -> mlexpr_of_list make_prod_item - (Option.List.cons (Option.map (fun a -> ExtTerminal a) a) b)) +let mlexpr_of_clause cl = + let mkexpr { r_head = a; r_patt = b; } = match a with + | None -> mlexpr_of_list make_prod_item b + | Some a -> mlexpr_of_list make_prod_item (ExtTerminal a :: b) + in + mlexpr_of_list mkexpr cl let declare_command loc s c nt cl = let se = mlexpr_of_string s in @@ -160,7 +164,7 @@ EXTEND rule: [ [ "["; s = STRING; l = LIST0 args; "]"; d = OPT deprecation; c = OPT classifier; "->"; "["; e = Pcaml.expr; "]" -> - let () = if CString.is_empty s then failwith "Command name is empty." in + let () = if s = "" then failwith "Command name is empty." in let b = <:expr< fun () -> $e$ >> in { r_head = Some s; r_patt = l; r_class = c; r_branch = b; r_depr = d; } | "[" ; "-" ; l = LIST1 args ; "]" ; -- cgit v1.2.3