diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/extrawit.ml | 44 | ||||
| -rw-r--r-- | parsing/extrawit.mli | 27 | ||||
| -rw-r--r-- | parsing/parsing.mllib | 1 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 36 |
4 files changed, 25 insertions, 83 deletions
diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml deleted file mode 100644 index c20f43bd5..000000000 --- a/parsing/extrawit.ml +++ /dev/null @@ -1,44 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Pp -open Genarg - -(* This file defines extra argument types *) - -(* Tactics as arguments *) - -let tactic_main_level = 5 - -let wit_tactic0 = create_arg None "tactic0" -let wit_tactic1 = create_arg None "tactic1" -let wit_tactic2 = create_arg None "tactic2" -let wit_tactic3 = create_arg None "tactic3" -let wit_tactic4 = create_arg None "tactic4" -let wit_tactic5 = create_arg None "tactic5" - -let wit_tactic = function - | 0 -> wit_tactic0 - | 1 -> wit_tactic1 - | 2 -> wit_tactic2 - | 3 -> wit_tactic3 - | 4 -> wit_tactic4 - | 5 -> wit_tactic5 - | n -> Errors.anomaly (str "Unavailable tactic level:" ++ spc () ++ int n) - -let tactic_genarg_level s = - if Int.equal (String.length s) 7 && String.sub s 0 6 = "tactic" then - let c = s.[6] in if '5' >= c && c >= '0' then Some (Char.code c - 48) - else None - else None - -let () = - for i = 0 to 5 do - let name = Printf.sprintf "Extrawit.wit_tactic%i" i in - Genarg.register_name0 (wit_tactic i) name - done diff --git a/parsing/extrawit.mli b/parsing/extrawit.mli deleted file mode 100644 index 1bd5cdb89..000000000 --- a/parsing/extrawit.mli +++ /dev/null @@ -1,27 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Genarg -open Tacexpr - -(** This file defines extra argument types *) - -(** Tactics as arguments *) - -val tactic_main_level : int - -val wit_tactic : int -> (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type - -val wit_tactic0 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type -val wit_tactic1 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type -val wit_tactic2 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type -val wit_tactic3 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type -val wit_tactic4 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type -val wit_tactic5 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type - -val tactic_genarg_level : string -> int option diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib index 2f0851164..500d7dde9 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -1,7 +1,6 @@ Tok Compat Lexer -Extrawit Pcoq Egramml Egramcoq diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 2769612d5..211bf2632 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -16,7 +16,6 @@ open Genarg open Stdarg open Constrarg open Tacexpr -open Extrawit (** The parser of Coq *) @@ -398,7 +397,7 @@ module Tactic = let tactic_expr = Gram.entry_create "tactic:tactic_expr" let binder_tactic = Gram.entry_create "tactic:binder_tactic" - let tactic = make_gen_entry utactic (rawwit (wit_tactic tactic_main_level)) "tactic" + let tactic = make_gen_entry utactic (rawwit wit_tactic) "tactic" (* Main entry for quotations *) let tactic_eoi = eoi_entry tactic @@ -756,6 +755,15 @@ let coincide s pat off = done; !break +let tactic_level s = + if Int.equal (String.length s) 7 && String.sub s 0 6 = "tactic" then + let c = s.[6] in if '5' >= c && c >= '0' then Some (Char.code c - 48) + else None + else None + +let type_of_entry u s = + type_of_typed_entry (get_entry u s) + let rec interp_entry_name static up_level s sep = let l = String.length s in if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then @@ -784,20 +792,26 @@ let rec interp_entry_name static up_level s sep = | Some m -> Int.equal m n && not (Int.equal m 5) in let t, se = - match Extrawit.tactic_genarg_level s with - | Some n when check_lvl n -> None, Aself - | Some n when check_lvl (n + 1) -> None, Anext - | Some n -> None, Atactic n - | None -> - try Some (get_entry uprim s), Aentry ("prim",s) with Not_found -> - try Some (get_entry uconstr s), Aentry ("constr",s) with Not_found -> - try Some (get_entry utactic s), Aentry ("tactic",s) with Not_found -> + match tactic_level s with + | Some n -> + (** Quite ad-hoc *) + let t = unquote (rawwit wit_tactic) in + let se = + if check_lvl n then Aself + else if check_lvl (n + 1) then Anext + else Atactic n + in + (Some t, se) + | None -> + try Some (type_of_entry uprim s), Aentry ("prim",s) with Not_found -> + try Some (type_of_entry uconstr s), Aentry ("constr",s) with Not_found -> + try Some (type_of_entry utactic s), Aentry ("tactic",s) with Not_found -> if static then error ("Unknown entry "^s^".") else None, Aentry ("",s) in let t = match t with - | Some t -> type_of_typed_entry t + | Some t -> t | None -> ExtraArgType s in t, se |