aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/egrammar.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/egrammar.ml')
-rw-r--r--parsing/egrammar.ml160
1 files changed, 102 insertions, 58 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 731bb5e64..cec7e4458 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -12,20 +12,25 @@ open Pp
open Util
open Extend
open Pcoq
-open Coqast
+open Topconstr
open Ast
open Genarg
+open Libnames
(* State of the grammar extensions *)
type all_grammar_command =
- | AstGrammar of grammar_command
+ | Notation of (string * notation * prod_item list)
+ | Delimiters of (scope_name * prod_item list * prod_item list)
+ | Grammar of grammar_command
| TacticGrammar of
(string * (string * grammar_production list) * Tacexpr.raw_tactic_expr)
list
let subst_all_grammar_command subst = function
- | AstGrammar gc -> AstGrammar (subst_grammar_command subst gc)
+ | Notation _ -> anomaly "Notation not in GRAMMAR summary"
+ | Delimiters _ -> anomaly "Delimiters not in GRAMMAR summary"
+ | Grammar gc -> Grammar (subst_grammar_command subst gc)
| TacticGrammar g -> TacticGrammar g (* TODO ... *)
let (grammar_state : all_grammar_command list ref) = ref []
@@ -45,24 +50,8 @@ let specify_name name e =
Failure("during interpretation of grammar rule "^name^", "^s)
| e -> e
-let gram_action (name, etyp) env act dloc =
- try
- let v = Ast.eval_act dloc env act in
- match etyp, v with
- | (PureAstType, PureAstNode ast) -> Obj.repr ast
- | (AstListType, AstListNode astl) -> Obj.repr astl
- | (GenAstType ConstrArgType, PureAstNode ast) -> Obj.repr ast
- | _ -> grammar_type_error (dloc, "Egrammar.gram_action")
- with e ->
- let (loc, exn) =
- match e with
- | Stdpp.Exc_located (loce, lexn) -> (loce, lexn)
- | e -> (dloc, e)
- in
- Stdpp.raise_with_loc loc (specify_name name exn)
-
(* Translation of environments: a production
- * [ nt1($x1) ... nti($xi) ] -> act($x1..$xi)
+ * [ nt1(x1) ... nti(xi) ] -> act(x1..xi)
* is written (with camlp4 conventions):
* (fun vi -> .... (fun v1 -> act(v1 .. vi) )..)
* where v1..vi are the values generated by non-terminals nt1..nti.
@@ -75,23 +64,42 @@ let gram_action (name, etyp) env act dloc =
*
* (fun v1 ->
* (fun env -> gram_action .. env act)
- * (($x1,v1)::env))
+ * ((x1,v1)::env))
* ...)
- * (($xi,vi)::env)))
+ * ((xi,vi)::env)))
* [])
*)
-let make_act name_typ a pil =
- let act_without_arg env = Gramext.action (gram_action name_typ env a)
- and make_prod_item act_tl = function
- | None -> (* parse a non-binding item *)
- (fun env -> Gramext.action (fun _ -> act_tl env))
- | Some (p, ETast) -> (* non-terminal *)
- (fun env -> Gramext.action (fun v -> act_tl((p,PureAstNode v)::env)))
- | Some (p, ETastl) -> (* non-terminal *)
- (fun env -> Gramext.action (fun v -> act_tl((p,AstListNode v)::env)))
- in
- (List.fold_left make_prod_item act_without_arg pil) []
+open Names
+
+let make_act f pil =
+ let rec make env = function
+ | [] ->
+ Gramext.action (fun loc -> f loc env)
+ | None :: tl -> (* parse a non-binding item *)
+ Gramext.action (fun _ -> make env tl)
+ | Some (p, ETConstr) :: tl -> (* non-terminal *)
+ Gramext.action (fun (v:constr_expr) -> make ((p,v) :: env) tl)
+ | Some (p, ETReference) :: tl -> (* non-terminal *)
+ Gramext.action (fun (v:reference) -> make ((p,CRef v) :: env) tl)
+ | Some (p, ETIdent) :: tl -> (* non-terminal *)
+ Gramext.action (fun (v:identifier) ->
+ make ((p,CRef (Ident (dummy_loc,v))) :: env) tl) in
+ make [] (List.rev pil)
+
+let make_cases_pattern_act f pil =
+ let rec make env = function
+ | [] ->
+ Gramext.action (fun loc -> f loc env)
+ | None :: tl -> (* parse a non-binding item *)
+ Gramext.action (fun _ -> make env tl)
+ | Some (p, ETConstr) :: tl -> (* non-terminal *)
+ Gramext.action (fun v -> make ((p,v) :: env) tl)
+ | Some (p, ETReference) :: tl -> (* non-terminal *)
+ Gramext.action (fun v -> make ((p,CPatAtom (dummy_loc,Some v)) :: env) tl)
+ | Some (p, ETIdent) :: tl ->
+ error "ident entry not admitted in patterns cases syntax extensions" in
+ make [] (List.rev pil)
(* Grammar extension command. Rules are assumed correct.
* Type-checking of grammar rules is done during the translation of
@@ -101,7 +109,8 @@ let make_act name_typ a pil =
* Extend.of_ast) *)
let get_entry_type (u,n) =
- Gram.Entry.obj (object_of_typed_entry (get_entry (get_univ u) n))
+ if u = "constr" & n = "pattern" then Gram.Entry.obj Constr.pattern
+ else Gram.Entry.obj (object_of_typed_entry (get_entry (get_univ u) n))
let rec build_prod_item univ = function
| ProdList0 s -> Gramext.Slist0 (build_prod_item univ s)
@@ -117,26 +126,36 @@ let symbol_of_prod_item univ = function
let eobj = build_prod_item univ nt in
(eobj, ovar)
+(*
let make_rule univ etyp rule =
let pil = List.map (symbol_of_prod_item univ) rule.gr_production in
let (symbs,ntl) = List.split pil in
let act = make_act (rule.gr_name,etyp) rule.gr_action ntl in
(symbs, act)
+*)
+
+let make_rule univ etyp rule =
+ let pil = List.map (symbol_of_prod_item univ) rule.gr_production in
+ let (symbs,ntl) = List.split pil in
+ let f loc env = CGrammar (loc, rule.gr_action, env) in
+ let act = make_act f ntl in
+ (symbs, act)
+
(* Rules of a level are entered in reverse order, so that the first rules
are applied before the last ones *)
let extend_entry univ (te, etyp, ass, rls) =
let rules = List.rev (List.map (make_rule univ etyp) rls) in
- grammar_extend te None [(None, ass, rules)]
+ grammar_extend (object_of_typed_entry te) None [(None, ass, rules)]
(* Defines new entries. If the entry already exists, check its type *)
let define_entry univ {ge_name=n; ge_type=typ; gl_assoc=ass; gl_rules=rls} =
- let typ = if typ = ETast then GenAstType ConstrArgType else AstListType in
+ let typ = entry_type_of_constr_entry_type typ in
let e = force_entry_type univ n typ in
(e,typ,ass,rls)
(* Add a bunch of grammar rules. Does not check if it is well formed *)
-let extend_grammar gram =
+let extend_grammar_rules gram =
let univ = get_univ gram.gc_univ in
let tl = List.map (define_entry univ) gram.gc_entries in
List.iter (extend_entry univ) tl
@@ -154,32 +173,56 @@ let make_prod_item = function
let make_gen_act f pil =
let rec make env = function
| [] ->
- Gramext.action (fun loc -> f env)
+ Gramext.action (fun loc -> f loc env)
| None :: tl -> (* parse a non-binding item *)
Gramext.action (fun _ -> make env tl)
| Some (p, t) :: tl -> (* non-terminal *)
Gramext.action (fun v -> make ((p,in_generic t v) :: env) tl) in
make [] (List.rev pil)
-let make_rule univ f g (s',pt) =
- let hd = Gramext.Stoken ("IDENT", s') in
+let extend_constr entry make_act pt =
+ let univ = get_univ "constr" in
+ let pil = List.map (symbol_of_prod_item univ) pt in
+ let (symbs,ntl) = List.split pil in
+ let act = make_act ntl in
+ grammar_extend entry None [(None, None, [symbs, act])]
+
+let constr_entry name =
+ object_of_typed_entry (get_entry (get_univ "constr") name)
+
+let extend_constr_notation (name,ntn,rule) =
+ let mkact loc env = CNotation (loc,ntn,env) in
+ extend_constr (constr_entry name) (make_act mkact) rule
+
+let extend_constr_grammar (name,c,rule) =
+ let mkact loc env = CGrammar (loc,c,env) in
+ extend_constr (constr_entry name) (make_act mkact) rule
+
+let extend_constr_delimiters (sc,rule,pat_rule) =
+ let mkact loc env = CDelimiters (loc,sc,snd (List.hd env)) in
+ extend_constr (constr_entry "constr8") (make_act mkact) rule;
+ let mkact loc env = CPatDelimiters (loc,sc,snd (List.hd env)) in
+ extend_constr Constr.pattern (make_cases_pattern_act mkact) pat_rule
+
+(* These grammars are not a removable *)
+let make_rule univ f g (s,pt) =
+ let hd = Gramext.Stoken ("IDENT", s) in
let pil = (hd,None) :: List.map g pt in
let (symbs,ntl) = List.split pil in
let act = make_gen_act f ntl in
(symbs, act)
-(* These grammars are not a removable *)
let extend_tactic_grammar s gl =
let univ = get_univ "tactic" in
- let make_act l = Tacexpr.TacExtend (s,List.map snd l) in
- let rules = List.rev (List.map (make_rule univ make_act make_prod_item) gl)
- in Gram.extend Tactic.simple_tactic None [(None, None, rules)]
+ let make_act loc l = Tacexpr.TacExtend (loc,s,List.map snd l) in
+ let rules = List.map (make_rule univ make_act make_prod_item) gl in
+ Gram.extend Tactic.simple_tactic None [(None, None, List.rev rules)]
let extend_vernac_command_grammar s gl =
let univ = get_univ "vernac" in
- let make_act l = Vernacexpr.VernacExtend (s,List.map snd l) in
- let rules = List.rev (List.map (make_rule univ make_act make_prod_item) gl)
- in Gram.extend Vernac_.command None [(None, None, rules)]
+ let make_act loc l = Vernacexpr.VernacExtend (s,List.map snd l) in
+ let rules = List.map (make_rule univ make_act make_prod_item) gl in
+ Gram.extend Vernac_.command None [(None, None, List.rev rules)]
let rec interp_entry_name u s =
let l = String.length s in
@@ -196,9 +239,7 @@ let rec interp_entry_name u s =
let n = Extend.rename_command s in
let e = get_entry (get_univ u) n in
let o = object_of_typed_entry e in
- let t = match type_of_typed_entry e with
- | GenAstType t -> t
- | _ -> failwith "Only entries of generic type can be used in alias" in
+ let t = type_of_typed_entry e in
t, Gramext.Snterm (Pcoq.Gram.Entry.obj o)
let qualified_nterm current_univ = function
@@ -214,16 +255,17 @@ let make_vprod_item univ = function
let add_tactic_entries gl =
let univ = get_univ "tactic" in
- let make_act s tac l = Tacexpr.TacAlias (s,l,tac) in
- let rules =
- List.rev (List.map (fun (s,l,tac) -> make_rule univ (make_act s tac) (make_vprod_item "tactic") l) gl)
- in
- let tacentry = get_entry (get_univ "tactic") "simple_tactic" in
- grammar_extend tacentry None [(None, None, rules)]
+ let make_act s tac loc l = Tacexpr.TacAlias (s,l,tac) in
+ let f (s,l,tac) =
+ make_rule univ (make_act s tac) (make_vprod_item "tactic") l in
+ let rules = List.map f gl in
+ grammar_extend Tactic.simple_tactic None [(None, None, List.rev rules)]
let extend_grammar gram =
(match gram with
- | AstGrammar g -> extend_grammar g
+ | Notation a -> extend_constr_notation a
+ | Delimiters a -> extend_constr_delimiters a
+ | Grammar g -> extend_grammar_rules g
| TacticGrammar l -> add_tactic_entries l);
grammar_state := gram :: !grammar_state
@@ -243,7 +285,9 @@ let factorize_grams l1 l2 =
let number_of_entries gcl =
List.fold_left
(fun n -> function
- | AstGrammar gc -> n + (List.length gc.gc_entries)
+ | Notation _ -> n + 1
+ | Delimiters _ -> n + 2 (* One rule for constr, one for pattern *)
+ | Grammar gc -> n + (List.length gc.gc_entries)
| TacticGrammar l -> n + 1)
0 gcl
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 00:39:12 +0000