summaryrefslogtreecommitdiff
path: root/parsing/pcoq.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/pcoq.ml')
-rw-r--r--parsing/pcoq.ml299
1 files changed, 165 insertions, 134 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 258c4bb1..eb3e6338 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -17,9 +17,17 @@ let curry f x y = f (x, y)
let uncurry f (x,y) = f x y
(** Location Utils *)
+let ploc_file_of_coq_file = function
+| Loc.ToplevelInput -> ""
+| Loc.InFile f -> f
+
let coq_file_of_ploc_file s =
if s = "" then Loc.ToplevelInput else Loc.InFile s
+let of_coqloc loc =
+ let open Loc in
+ Ploc.make_loc (ploc_file_of_coq_file loc.fname) loc.line_nb loc.bol_pos (loc.bp, loc.ep) ""
+
let to_coqloc loc =
{ Loc.fname = coq_file_of_ploc_file (Ploc.file_name loc);
Loc.line_nb = Ploc.line_nb loc;
@@ -78,24 +86,15 @@ module type S =
type internal_entry = Tok.t Gramext.g_entry
type symbol = Tok.t Gramext.g_symbol
type action = Gramext.g_action
- type production_rule = symbol list * action
- type single_extend_statment =
- string option * Gramext.g_assoc option * production_rule list
- type extend_statment =
- Gramext.position option * single_extend_statment list
type coq_parsable
- val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
+ val coq_parsable : ?file:Loc.source -> char Stream.t -> coq_parsable
val action : 'a -> action
val entry_create : string -> 'a entry
val entry_parse : 'a entry -> coq_parsable -> 'a
- val entry_print : Format.formatter -> 'a entry -> unit
val comment_state : coq_parsable -> ((int * int) * string) list
- val srules' : production_rule list -> symbol
- val parse_tokens_after_filter : 'a entry -> Tok.t Stream.t -> 'a
-
end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
include Grammar.GMake(CLexer)
@@ -104,15 +103,10 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
type internal_entry = Tok.t Gramext.g_entry
type symbol = Tok.t Gramext.g_symbol
type action = Gramext.g_action
- type production_rule = symbol list * action
- type single_extend_statment =
- string option * Gramext.g_assoc option * production_rule list
- type extend_statment =
- Gramext.position option * single_extend_statment list
type coq_parsable = parsable * CLexer.lexer_state ref
- let parsable ?(file=Loc.ToplevelInput) c =
+ let coq_parsable ?(file=Loc.ToplevelInput) c =
let state = ref (CLexer.init_lexer_state file) in
CLexer.set_lexer_state !state;
let a = parsable c in
@@ -137,14 +131,25 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct
let comment_state (p,state) =
CLexer.get_comment_state !state
- let entry_print ft x = Entry.print ft x
-
- (* Not used *)
- let srules' = Gramext.srules
- let parse_tokens_after_filter = Entry.parse_token
+end
+module Parsable =
+struct
+ type t = G.coq_parsable
+ let make = G.coq_parsable
+ let comment_state = G.comment_state
end
+module Entry =
+struct
+
+ type 'a t = 'a Grammar.GMake(CLexer).Entry.e
+
+ let create = G.Entry.create
+ let parse = G.entry_parse
+ let print = G.Entry.print
+
+end
let warning_verbose = Gramext.warning_verbose
@@ -208,9 +213,9 @@ let camlp5_verbosity silent f x =
(** Grammar extensions *)
-(** NB: [extend_statment =
- gram_position option * single_extend_statment list]
- and [single_extend_statment =
+(** NB: [extend_statement =
+ gram_position option * single_extend_statement list]
+ and [single_extend_statement =
string option * gram_assoc option * production_rule list]
and [production_rule = symbol list * action]
@@ -237,9 +242,9 @@ let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function
| Aentry e ->
Symbols.snterm (G.Entry.obj e)
| Aentryl (e, n) ->
- Symbols.snterml (G.Entry.obj e, string_of_int n)
+ Symbols.snterml (G.Entry.obj e, n)
| Arules rs ->
- G.srules' (List.map symbol_of_rules rs)
+ Gramext.srules (List.map symbol_of_rules rs)
and symbol_of_rule : type s a r. (s, a, r) Extend.rule -> _ = function
| Stop -> fun accu -> accu
@@ -264,16 +269,23 @@ let of_coq_extend_statement (pos, st) =
type gram_reinit = gram_assoc * gram_position
type extend_rule =
-| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statment -> extend_rule
+| ExtendRule : 'a G.entry * gram_reinit option * 'a extend_statement -> extend_rule
+
+module EntryCommand = Dyn.Make ()
+module EntryData = struct type _ t = Ex : 'b G.entry String.Map.t -> ('a * 'b) t end
+module EntryDataMap = EntryCommand.Map(EntryData)
type ext_kind =
| ByGrammar of extend_rule
| ByEXTEND of (unit -> unit) * (unit -> unit)
+ | ByEntry : ('a * 'b) EntryCommand.tag * string * 'b G.entry -> ext_kind
(** The list of extensions *)
let camlp5_state = ref []
+let camlp5_entries = ref EntryDataMap.empty
+
(** Deletion *)
let grammar_delete e reinit (pos,rls) =
@@ -329,6 +341,7 @@ module Gram =
I'm not entirely sure it makes sense, but at least it would be more correct.
*)
G.delete_rule e pil
+ let gram_extend e ext = grammar_extend e None ext
end
(** Remove extensions
@@ -338,7 +351,7 @@ module Gram =
let rec remove_grammars n =
if n>0 then
- (match !camlp5_state with
+ match !camlp5_state with
| [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove.")
| ByGrammar (ExtendRule (g, reinit, ext)) :: t ->
grammar_delete g reinit (of_coq_extend_statement ext);
@@ -349,21 +362,31 @@ let rec remove_grammars n =
camlp5_state := t;
remove_grammars n;
redo();
- camlp5_state := ByEXTEND (undo,redo) :: !camlp5_state)
+ camlp5_state := ByEXTEND (undo,redo) :: !camlp5_state
+ | ByEntry (tag, name, e) :: t ->
+ G.Unsafe.clear_entry e;
+ camlp5_state := t;
+ let EntryData.Ex entries =
+ try EntryDataMap.find tag !camlp5_entries
+ with Not_found -> EntryData.Ex String.Map.empty
+ in
+ let entries = String.Map.remove name entries in
+ camlp5_entries := EntryDataMap.add tag (EntryData.Ex entries) !camlp5_entries;
+ remove_grammars (n - 1)
let make_rule r = [None, None, r]
(** An entry that checks we reached the end of the input. *)
let eoi_entry en =
- let e = Gram.entry_create ((Gram.Entry.name en) ^ "_eoi") in
+ let e = Entry.create ((Gram.Entry.name en) ^ "_eoi") in
let symbs = [Symbols.snterm (Gram.Entry.obj en); Symbols.stoken Tok.EOI] in
let act = Gram.action (fun _ x loc -> x) in
uncurry (Gram.extend e) (None, make_rule [symbs, act]);
e
let map_entry f en =
- let e = Gram.entry_create ((Gram.Entry.name en) ^ "_map") in
+ let e = Entry.create ((Gram.Entry.name en) ^ "_map") in
let symbs = [Symbols.snterm (Gram.Entry.obj en)] in
let act = Gram.action (fun x loc -> f x) in
uncurry (Gram.extend e) (None, make_rule [symbs, act]);
@@ -373,7 +396,7 @@ let map_entry f en =
(use eoi_entry) *)
let parse_string f x =
- let strm = Stream.of_string x in Gram.entry_parse f (Gram.parsable strm)
+ let strm = Stream.of_string x in Gram.entry_parse f (Gram.coq_parsable strm)
type gram_universe = string
@@ -387,7 +410,6 @@ let create_universe u =
let uprim = create_universe "prim"
let uconstr = create_universe "constr"
let utactic = create_universe "tactic"
-let uvernac = create_universe "vernac"
let get_univ u =
if Hashtbl.mem utables u then u
@@ -395,14 +417,14 @@ let get_univ u =
let new_entry u s =
let ename = u ^ ":" ^ s in
- let e = Gram.entry_create ename in
+ let e = Entry.create ename in
e
let make_gen_entry u s = new_entry u s
module GrammarObj =
struct
- type ('r, _, _) obj = 'r Gram.entry
+ type ('r, _, _) obj = 'r Entry.t
let name = "grammar"
let default _ = None
end
@@ -412,7 +434,7 @@ module Grammar = Register(GrammarObj)
let register_grammar = Grammar.register0
let genarg_grammar = Grammar.obj
-let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Gram.entry =
+let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Entry.t =
let e = new_entry u s in
let Rawwit t = etyp in
let () = Grammar.register0 t e in
@@ -424,38 +446,38 @@ module Prim =
struct
let gec_gen n = make_gen_entry uprim n
- (* Entries that can be referred via the string -> Gram.entry table *)
+ (* Entries that can be referred via the string -> Entry.t table *)
(* Typically for tactic or vernac extensions *)
let preident = gec_gen "preident"
let ident = gec_gen "ident"
let natural = gec_gen "natural"
let integer = gec_gen "integer"
- let bigint = Gram.entry_create "Prim.bigint"
+ let bigint = Entry.create "Prim.bigint"
let string = gec_gen "string"
- let lstring = Gram.entry_create "Prim.lstring"
+ let lstring = Entry.create "Prim.lstring"
let reference = make_gen_entry uprim "reference"
- let by_notation = Gram.entry_create "by_notation"
- let smart_global = Gram.entry_create "smart_global"
+ let by_notation = Entry.create "by_notation"
+ let smart_global = Entry.create "smart_global"
(* parsed like ident but interpreted as a term *)
let var = gec_gen "var"
- let name = Gram.entry_create "Prim.name"
- let identref = Gram.entry_create "Prim.identref"
- let univ_decl = Gram.entry_create "Prim.univ_decl"
- let ident_decl = Gram.entry_create "Prim.ident_decl"
- let pattern_ident = Gram.entry_create "pattern_ident"
- let pattern_identref = Gram.entry_create "pattern_identref"
+ let name = Entry.create "Prim.name"
+ let identref = Entry.create "Prim.identref"
+ let univ_decl = Entry.create "Prim.univ_decl"
+ let ident_decl = Entry.create "Prim.ident_decl"
+ let pattern_ident = Entry.create "pattern_ident"
+ let pattern_identref = Entry.create "pattern_identref"
(* A synonym of ident - maybe ident will be located one day *)
- let base_ident = Gram.entry_create "Prim.base_ident"
+ let base_ident = Entry.create "Prim.base_ident"
- let qualid = Gram.entry_create "Prim.qualid"
- let fullyqualid = Gram.entry_create "Prim.fullyqualid"
- let dirpath = Gram.entry_create "Prim.dirpath"
+ let qualid = Entry.create "Prim.qualid"
+ let fullyqualid = Entry.create "Prim.fullyqualid"
+ let dirpath = Entry.create "Prim.dirpath"
- let ne_string = Gram.entry_create "Prim.ne_string"
- let ne_lstring = Gram.entry_create "Prim.ne_lstring"
+ let ne_string = Entry.create "Prim.ne_string"
+ let ne_lstring = Entry.create "Prim.ne_lstring"
end
@@ -463,7 +485,7 @@ module Constr =
struct
let gec_constr = make_gen_entry uconstr
- (* Entries that can be referred via the string -> Gram.entry table *)
+ (* Entries that can be referred via the string -> Entry.t table *)
let constr = gec_constr "constr"
let operconstr = gec_constr "operconstr"
let constr_eoi = eoi_entry constr
@@ -474,67 +496,29 @@ module Constr =
let universe_level = make_gen_entry uconstr "universe_level"
let sort = make_gen_entry uconstr "sort"
let sort_family = make_gen_entry uconstr "sort_family"
- let pattern = Gram.entry_create "constr:pattern"
+ let pattern = Entry.create "constr:pattern"
let constr_pattern = gec_constr "constr_pattern"
let lconstr_pattern = gec_constr "lconstr_pattern"
- let closed_binder = Gram.entry_create "constr:closed_binder"
- let binder = Gram.entry_create "constr:binder"
- let binders = Gram.entry_create "constr:binders"
- let open_binders = Gram.entry_create "constr:open_binders"
- let binders_fixannot = Gram.entry_create "constr:binders_fixannot"
- let typeclass_constraint = Gram.entry_create "constr:typeclass_constraint"
- let record_declaration = Gram.entry_create "constr:record_declaration"
- let appl_arg = Gram.entry_create "constr:appl_arg"
+ let closed_binder = Entry.create "constr:closed_binder"
+ let binder = Entry.create "constr:binder"
+ let binders = Entry.create "constr:binders"
+ let open_binders = Entry.create "constr:open_binders"
+ let binders_fixannot = Entry.create "constr:binders_fixannot"
+ let typeclass_constraint = Entry.create "constr:typeclass_constraint"
+ let record_declaration = Entry.create "constr:record_declaration"
+ let appl_arg = Entry.create "constr:appl_arg"
end
module Module =
struct
- let module_expr = Gram.entry_create "module_expr"
- let module_type = Gram.entry_create "module_type"
+ let module_expr = Entry.create "module_expr"
+ let module_type = Entry.create "module_type"
end
-module Vernac_ =
- struct
- let gec_vernac s = Gram.entry_create ("vernac:" ^ s)
-
- (* The different kinds of vernacular commands *)
- let gallina = gec_vernac "gallina"
- let gallina_ext = gec_vernac "gallina_ext"
- let command = gec_vernac "command"
- let syntax = gec_vernac "syntax_command"
- let vernac_control = gec_vernac "Vernac.vernac_control"
- let rec_definition = gec_vernac "Vernac.rec_definition"
- let red_expr = make_gen_entry utactic "red_expr"
- let hint_info = gec_vernac "hint_info"
- (* Main vernac entry *)
- let main_entry = Gram.entry_create "vernac"
- let noedit_mode = gec_vernac "noedit_command"
-
- let () =
- let act_vernac = Gram.action (fun v loc -> Some (to_coqloc loc, v)) in
- let act_eoi = Gram.action (fun _ loc -> None) in
- let rule = [
- ([ Symbols.stoken Tok.EOI ], act_eoi);
- ([ Symbols.snterm (Gram.Entry.obj vernac_control) ], act_vernac );
- ] in
- uncurry (Gram.extend main_entry) (None, make_rule rule)
-
- let command_entry_ref = ref noedit_mode
- let command_entry =
- Gram.Entry.of_parser "command_entry"
- (fun strm -> Gram.parse_tokens_after_filter !command_entry_ref strm)
-
- end
-
-let main_entry = Vernac_.main_entry
-
-let set_command_entry e = Vernac_.command_entry_ref := e
-let get_command_entry () = !Vernac_.command_entry_ref
-
let epsilon_value f e =
let r = Rule (Next (Stop, e), fun x _ -> f x) in
let ext = of_coq_extend_statement (None, [None, None, [r]]) in
- let entry = G.entry_create "epsilon" in
+ let entry = Gram.entry_create "epsilon" in
let () = uncurry (G.extend entry) ext in
try Some (parse_string entry "") with _ -> None
@@ -550,59 +534,119 @@ module GrammarInterpMap = GrammarCommand.Map(GrammarInterp)
let grammar_interp = ref GrammarInterpMap.empty
-let (grammar_stack : (int * GrammarCommand.t * GramState.t) list ref) = ref []
+type ('a, 'b) entry_extension = 'a -> GramState.t -> string list * GramState.t
+
+module EntryInterp = struct type _ t = Ex : ('a, 'b) entry_extension -> ('a * 'b) t end
+module EntryInterpMap = EntryCommand.Map(EntryInterp)
+
+let entry_interp = ref EntryInterpMap.empty
+
+type grammar_entry =
+| GramExt of int * GrammarCommand.t
+| EntryExt : int * ('a * 'b) EntryCommand.tag * 'a -> grammar_entry
+
+let (grammar_stack : (grammar_entry * GramState.t) list ref) = ref []
type 'a grammar_command = 'a GrammarCommand.tag
+type ('a, 'b) entry_command = ('a * 'b) EntryCommand.tag
let create_grammar_command name interp : _ grammar_command =
let obj = GrammarCommand.create name in
let () = grammar_interp := GrammarInterpMap.add obj interp !grammar_interp in
obj
+let create_entry_command name (interp : ('a, 'b) entry_extension) : ('a, 'b) entry_command =
+ let obj = EntryCommand.create name in
+ let () = entry_interp := EntryInterpMap.add obj (EntryInterp.Ex interp) !entry_interp in
+ obj
+
let extend_grammar_command tag g =
let modify = GrammarInterpMap.find tag !grammar_interp in
let grammar_state = match !grammar_stack with
| [] -> GramState.empty
- | (_, _, st) :: _ -> st
+ | (_, st) :: _ -> st
in
let (rules, st) = modify g grammar_state in
let iter (ExtendRule (e, reinit, ext)) = grammar_extend_sync e reinit ext in
let () = List.iter iter rules in
let nb = List.length rules in
- grammar_stack := (nb, GrammarCommand.Dyn (tag, g), st) :: !grammar_stack
+ grammar_stack := (GramExt (nb, GrammarCommand.Dyn (tag, g)), st) :: !grammar_stack
-let recover_grammar_command (type a) (tag : a grammar_command) : a list =
- let filter : _ -> a option = fun (_, GrammarCommand.Dyn (tag', v), _) ->
- match GrammarCommand.eq tag tag' with
- | None -> None
- | Some Refl -> Some v
+let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) : b Gram.entry list =
+ let EntryInterp.Ex modify = EntryInterpMap.find tag !entry_interp in
+ let grammar_state = match !grammar_stack with
+ | [] -> GramState.empty
+ | (_, st) :: _ -> st
+ in
+ let (names, st) = modify g grammar_state in
+ let entries = List.map (fun name -> Gram.entry_create name) names in
+ let iter name e =
+ camlp5_state := ByEntry (tag, name, e) :: !camlp5_state;
+ let EntryData.Ex old =
+ try EntryDataMap.find tag !camlp5_entries
+ with Not_found -> EntryData.Ex String.Map.empty
+ in
+ let entries = String.Map.add name e old in
+ camlp5_entries := EntryDataMap.add tag (EntryData.Ex entries) !camlp5_entries
in
- List.map_filter filter !grammar_stack
+ let () = List.iter2 iter names entries in
+ let nb = List.length entries in
+ let () = grammar_stack := (EntryExt (nb, tag, g), st) :: !grammar_stack in
+ entries
+
+let find_custom_entry tag name =
+ let EntryData.Ex map = EntryDataMap.find tag !camlp5_entries in
+ String.Map.find name map
+
+let extend_dyn_grammar (e, _) = match e with
+| GramExt (_, (GrammarCommand.Dyn (tag, g))) -> extend_grammar_command tag g
+| EntryExt (_, tag, g) -> ignore (extend_entry_command tag g)
+
+(** Registering extra grammar *)
-let extend_dyn_grammar (GrammarCommand.Dyn (tag, g)) = extend_grammar_command tag g
+type any_entry = AnyEntry : 'a Gram.entry -> any_entry
+
+let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty
-(* Summary functions: the state of the lexer is included in that of the parser.
+let register_grammars_by_name name grams =
+ grammar_names := String.Map.add name grams !grammar_names
+
+let find_grammars_by_name name =
+ try String.Map.find name !grammar_names
+ with Not_found ->
+ let fold (EntryDataMap.Any (tag, EntryData.Ex map)) accu =
+ try AnyEntry (String.Map.find name map) :: accu
+ with Not_found -> accu
+ in
+ EntryDataMap.fold fold !camlp5_entries []
+
+(** Summary functions: the state of the lexer is included in that of the parser.
Because the grammar affects the set of keywords when adding or removing
grammar rules. *)
-type frozen_t = (int * GrammarCommand.t * GramState.t) list * CLexer.keyword_state
+type frozen_t =
+ (grammar_entry * GramState.t) list *
+ CLexer.keyword_state
-let freeze _ : frozen_t = (!grammar_stack, CLexer.get_keyword_state ())
+let freeze _ : frozen_t =
+ (!grammar_stack, CLexer.get_keyword_state ())
(* We compare the current state of the grammar and the state to unfreeze,
by computing the longest common suffixes *)
let factorize_grams l1 l2 =
if l1 == l2 then ([], [], l1) else List.share_tails l1 l2
-let number_of_entries gcl =
- List.fold_left (fun n (p,_,_) -> n + p) 0 gcl
+let rec number_of_entries accu = function
+| [] -> accu
+| ((GramExt (p, _) | EntryExt (p, _, _)), _) :: rem ->
+ number_of_entries (p + accu) rem
let unfreeze (grams, lex) =
let (undo, redo, common) = factorize_grams !grammar_stack grams in
- let n = number_of_entries undo in
+ let n = number_of_entries 0 undo in
remove_grammars n;
grammar_stack := common;
CLexer.set_keyword_state lex;
- List.iter extend_dyn_grammar (List.rev_map pi2 redo)
+ List.iter extend_dyn_grammar (List.rev redo)
(** No need to provide an init function : the grammar state is
statically available, and already empty initially, while
@@ -635,17 +679,4 @@ let () =
Grammar.register0 wit_ref (Prim.reference);
Grammar.register0 wit_sort_family (Constr.sort_family);
Grammar.register0 wit_constr (Constr.constr);
- Grammar.register0 wit_red_expr (Vernac_.red_expr);
()
-
-(** Registering extra grammar *)
-
-type any_entry = AnyEntry : 'a Gram.entry -> any_entry
-
-let grammar_names : any_entry list String.Map.t ref = ref String.Map.empty
-
-let register_grammars_by_name name grams =
- grammar_names := String.Map.add name grams !grammar_names
-
-let find_grammars_by_name name =
- String.Map.find name !grammar_names
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 23:26:46 +0000