diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/entry.ml | 63 | ||||
| -rw-r--r-- | parsing/entry.mli | 50 | ||||
| -rw-r--r-- | parsing/parsing.mllib | 1 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 103 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 12 |
5 files changed, 180 insertions, 49 deletions
diff --git a/parsing/entry.ml b/parsing/entry.ml new file mode 100644 index 000000000..97d601320 --- /dev/null +++ b/parsing/entry.ml @@ -0,0 +1,63 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Errors +open Util + +type 'a t = string * string + +type repr = +| Static of string * string +| Dynamic of string + +type universe = string + +(* The univ_tab is not part of the state. It contains all the grammars that + exist or have existed before in the session. *) + +let univ_tab = (Hashtbl.create 7 : (string, unit) Hashtbl.t) + +let create_univ s = + Hashtbl.add univ_tab s (); s + +let univ_name s = s + +let uprim = create_univ "prim" +let uconstr = create_univ "constr" +let utactic = create_univ "tactic" +let uvernac = create_univ "vernac" + +let get_univ s = + try + Hashtbl.find univ_tab s; s + with Not_found -> + anomaly (Pp.str ("Unknown grammar universe: "^s)) + +(** Entries are registered with a unique name *) + +let entries = ref String.Set.empty + +let create u name = + let uname = u ^ ":" ^ name in + let () = + if String.Set.mem uname !entries then + anomaly (Pp.str ("Entry " ^ uname ^ " already defined")) + in + let () = entries := String.Set.add uname !entries in + (u, name) + +let dynamic name = ("", name) + +let unsafe_of_name (u, s) = + let uname = u ^ ":" ^ s in + assert (String.Set.mem uname !entries); + (u, s) + +let repr = function +| ("", u) -> Dynamic u +| (u, s) -> Static (u, s) diff --git a/parsing/entry.mli b/parsing/entry.mli new file mode 100644 index 000000000..6854a5cb4 --- /dev/null +++ b/parsing/entry.mli @@ -0,0 +1,50 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Typed grammar entries *) + +type 'a t +(** Typed grammar entries. We need to defined them here so that they are + marshallable and defined before the Pcoq.Gram module. They are basically + unique names made of a universe and an entry name. They should be kept + synchronized with the {!Pcoq} entries though. *) + +type repr = +| Static of string * string +| Dynamic of string +(** Representation of entries. *) + +(** Table of Coq statically defined grammar entries *) + +type universe + +(** There are four predefined universes: "prim", "constr", "tactic", "vernac" *) + +val get_univ : string -> universe +val univ_name : universe -> string + +val uprim : universe +val uconstr : universe +val utactic : universe +val uvernac : universe + +(** {5 Uniquely defined entries} *) + +val create : universe -> string -> 'a t +(** Create an entry. They should be synchronized with the entries defined in + {!Pcoq}. *) + +(** {5 Meta-programming} *) + +val dynamic : string -> 'a t +(** Dynamic entries. They refer to entries defined in the code source and may + only be used in meta-programming definitions from the grammar directory. *) + +val repr : 'a t -> repr + +val unsafe_of_name : (string * string) -> 'a t diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib index a0cb83193..024d8607f 100644 --- a/parsing/parsing.mllib +++ b/parsing/parsing.mllib @@ -1,6 +1,7 @@ Tok Compat Lexer +Entry Pcoq Egramml Egramcoq diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index b244a021e..5b980b348 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -76,8 +76,8 @@ type ('self, _) entry_key = | Amodifiers : ('self, 'a) entry_key -> ('self, 'a list) entry_key | Aself : ('self, 'self) entry_key | Anext : ('self, 'self) entry_key -| Aentry : (string * string) -> ('self, 'a) entry_key -| Aentryl : (string * string) * int -> ('self, 'a) entry_key +| Aentry : 'a Entry.t -> ('self, 'a) entry_key +| Aentryl : 'a Entry.t * int -> ('self, 'a) entry_key type entry_name = EntryName : entry_type * ('self, 'a) entry_key -> entry_name @@ -217,45 +217,58 @@ let map_entry f en = let parse_string f x = let strm = Stream.of_string x in Gram.entry_parse f (Gram.parsable strm) -type gram_universe = string * (string, typed_entry) Hashtbl.t +type gram_universe = Entry.universe let trace = ref false -(* The univ_tab is not part of the state. It contains all the grammars that - exist or have existed before in the session. *) +let uprim = Entry.uprim +let uconstr = Entry.uconstr +let utactic = Entry.utactic +let uvernac = Entry.uvernac +let get_univ = Entry.get_univ -let univ_tab = (Hashtbl.create 7 : (string, gram_universe) Hashtbl.t) +let utables : (string, (string, typed_entry) Hashtbl.t) Hashtbl.t = + Hashtbl.create 97 -let create_univ s = - let u = s, Hashtbl.create 29 in Hashtbl.add univ_tab s u; u - -let uprim = create_univ "prim" -let uconstr = create_univ "constr" -let utactic = create_univ "tactic" -let uvernac = create_univ "vernac" - -let get_univ s = - try - Hashtbl.find univ_tab s +let get_utable u = + let u = Entry.univ_name u in + try Hashtbl.find utables u with Not_found -> - anomaly (Pp.str ("Unknown grammar universe: "^s)) - -let get_entry (u, utab) s = Hashtbl.find utab s - -let new_entry etyp (u, utab) s = - if !trace then (Printf.eprintf "[Creating entry %s:%s]\n" u s; flush stderr); - let ename = u ^ ":" ^ s in + let table = Hashtbl.create 97 in + Hashtbl.add utables u table; + table + +let get_entry u s = + let utab = get_utable u in + Hashtbl.find utab s + +let get_typed_entry e = + let (u, s) = match Entry.repr e with + | Entry.Dynamic _ -> assert false + | Entry.Static (u, s) -> (u, s) + in + let u = Entry.get_univ u in + get_entry u s + +let new_entry etyp u s = + let utab = get_utable u in + let uname = Entry.univ_name u in + if !trace then (Printf.eprintf "[Creating entry %s:%s]\n" uname s; flush stderr); + let _ = Entry.create u s in + let ename = uname ^ ":" ^ s in let e = in_typed_entry etyp (Gram.entry_create ename) in Hashtbl.add utab s e; e -let create_entry (u, utab) s etyp = +let create_entry u s etyp = + let utab = get_utable u in try let e = Hashtbl.find utab s in + let u = Entry.univ_name u in if not (argument_type_eq (type_of_typed_entry e) etyp) then failwith ("Entry " ^ u ^ ":" ^ s ^ " already exists with another type"); e with Not_found -> - new_entry etyp (u, utab) s + new_entry etyp u s let create_constr_entry s = outGramObj (rawwit wit_constr) (create_entry uconstr s ConstrArgType) @@ -266,8 +279,11 @@ let create_generic_entry s wit = (* [make_gen_entry] builds entries extensible by giving its name (a string) *) (* For entries extensible only via the ML name, Gram.entry_create is enough *) -let make_gen_entry (u,univ) rawwit s = - let e = Gram.entry_create (u ^ ":" ^ s) in +let make_gen_entry u rawwit s = + let univ = get_utable u in + let uname = Entry.univ_name u in + let e = Gram.entry_create (uname ^ ":" ^ s) in + let _ = Entry.create u s in Hashtbl.add univ s (inGramObj rawwit e); e (* Initial grammar entries *) @@ -355,7 +371,7 @@ module Tactic = make_gen_entry utactic (rawwit wit_bindings) "bindings" let hypident = Gram.entry_create "hypident" let constr_may_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval" - let constr_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_may_eval" + let constr_eval = make_gen_entry utactic (rawwit wit_constr_may_eval) "constr_eval" let uconstr = make_gen_entry utactic (rawwit wit_uconstr) "uconstr" let quantified_hypothesis = @@ -707,11 +723,11 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) entry_key -> _ = function Gram.action (fun _ l _ _loc -> l))] | Aself -> Symbols.sself | Anext -> Symbols.snext - | Aentry (u,s) -> - let e = get_entry (get_univ u) s in + | Aentry e -> + let e = get_typed_entry e in Symbols.snterm (Gram.Entry.obj (object_of_typed_entry e)) - | Aentryl ((u, s), n) -> - let e = get_entry (get_univ u) s in + | Aentryl (e, n) -> + let e = get_typed_entry e in Symbols.snterml (Gram.Entry.obj (object_of_typed_entry e), string_of_int n) let level_of_snterml e = int_of_string (Symbols.snterml_level e) @@ -741,13 +757,18 @@ let type_of_entry u s = type_of_typed_entry (get_entry u s) let name_of_entry e = match String.split ':' (Gram.Entry.name e) with -| u :: s :: [] -> (u, s) +| u :: s :: [] -> Entry.unsafe_of_name (u, s) | _ -> assert false let atactic n = if n = 5 then Aentry (name_of_entry Tactic.binder_tactic) else Aentryl (name_of_entry Tactic.tactic_expr, n) +let try_get_entry u s = + (** Order the effects: type_of_entry can raise Not_found *) + let typ = type_of_entry u s in + Some typ, Aentry (Entry.unsafe_of_name (Entry.univ_name 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 @@ -789,13 +810,13 @@ let rec interp_entry_name static up_level s sep = 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 -> + try try_get_entry uprim s with Not_found -> + try try_get_entry uconstr s with Not_found -> + try try_get_entry utactic s with Not_found -> if static then error ("Unknown entry "^s^".") else - None, Aentry ("",s) in + None, Aentry (Entry.dynamic s) in let t = match t with | Some t -> t @@ -804,6 +825,6 @@ let rec interp_entry_name static up_level s sep = let list_entry_names () = let add_entry key (entry, _) accu = (key, entry) :: accu in - let ans = Hashtbl.fold add_entry (snd uprim) [] in - let ans = Hashtbl.fold add_entry (snd uconstr) ans in - Hashtbl.fold add_entry (snd utactic) ans + let ans = Hashtbl.fold add_entry (get_utable uprim) [] in + let ans = Hashtbl.fold add_entry (get_utable uconstr) ans in + Hashtbl.fold add_entry (get_utable utactic) ans diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 959c039d3..18eb3eed3 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -137,11 +137,7 @@ val parse_string : 'a Gram.entry -> string -> 'a val eoi_entry : 'a Gram.entry -> 'a Gram.entry val map_entry : ('a -> 'b) -> 'a Gram.entry -> 'b Gram.entry -(** Table of Coq statically defined grammar entries *) - -type gram_universe - -(** There are four predefined universes: "prim", "constr", "tactic", "vernac" *) +type gram_universe = Entry.universe val get_univ : string -> gram_universe @@ -273,10 +269,10 @@ type ('self, _) entry_key = | Amodifiers : ('self, 'a) entry_key -> ('self, 'a list) entry_key | Aself : ('self, 'self) entry_key | Anext : ('self, 'self) entry_key -| Aentry : (string * string) -> ('self, 'a) entry_key -| Aentryl : (string * string) * int -> ('self, 'a) entry_key +| Aentry : 'a Entry.t -> ('self, 'a) entry_key +| Aentryl : 'a Entry.t * int -> ('self, 'a) entry_key -val name_of_entry : 'a Gram.entry -> string * string +val name_of_entry : 'a Gram.entry -> 'a Entry.t (** Binding general entry keys to symbols *) |