diff options
| -rw-r--r-- | parsing/egrammar.ml | 18 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 23 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 2 |
4 files changed, 23 insertions, 22 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index e7a6bdd1b..126baea71 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -223,9 +223,8 @@ let extend_entry univ (te, etyp, pos, name, ass, p4ass, rls) = (* Defines new entries. If the entry already exists, check its type *) let define_entry univ {ge_name=n; gl_assoc=ass; gl_rules=rls} = let typ = explicitize_entry (fst univ) n in - let e,lev = get_constr_entry typ in - let other = match typ with ETOther _ -> true | _ -> false in - let pos,p4ass,name = find_position other ass lev in + let e,lev,keepassoc = get_constr_entry typ in + let pos,p4ass,name = find_position keepassoc ass lev in (e,typ,pos,name,ass,p4ass,rls) (* Add a bunch of grammar rules. Does not check if it is well formed *) @@ -254,24 +253,25 @@ let make_gen_act f pil = Gramext.action (fun v -> make ((p,in_generic t v) :: env) tl) in make [] (List.rev pil) -let extend_constr entry (level,assoc) make_act pt = +let extend_constr entry (level,assoc,keepassoc) make_act pt = let univ = get_univ "constr" in let pil = List.map (symbol_of_prod_item univ assoc) pt in let (symbs,ntl) = List.split pil in let act = make_act ntl in - let pos,p4assoc,name = find_position false assoc level in + let pos,p4assoc,name = find_position keepassoc assoc level in grammar_extend entry pos [(name, p4assoc, [symbs, act])] let extend_constr_notation (n,assoc,ntn,rule) = let mkact loc env = CNotation (loc,ntn,env) in - let (e,level) = get_constr_entry (ETConstr (n,())) in - extend_constr e (level,assoc) (make_act mkact) rule + let (e,level,keepassoc) = get_constr_entry (ETConstr (n,())) in + extend_constr e (level,assoc,keepassoc) (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.constr (Some 0,Some Gramext.NonA) (make_act mkact) rule; + extend_constr Constr.constr (Some 0,Some Gramext.NonA,false) + (make_act mkact) rule; let mkact loc env = CPatDelimiters (loc,sc,snd (List.hd env)) in - extend_constr Constr.pattern (None,None) + extend_constr Constr.pattern (None,None,false) (make_cases_pattern_act mkact) pat_rule (* These grammars are not a removable *) diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index fa67fe675..72eb7dca1 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -522,21 +522,22 @@ let adjust_level assoc = function | (n,InternalProd) -> Some (Some n) let compute_entry allow_create adjust = function - | ETConstr (10,_) -> weaken_entry Constr.lconstr, None - | ETConstr (9,_) -> weaken_entry Constr.constr9, None - | ETConstr (n,q) -> weaken_entry Constr.constr, adjust (n,q) - | ETIdent -> weaken_entry Constr.ident, None - | ETBigint -> weaken_entry Prim.bigint, None - | ETReference -> weaken_entry Constr.global, None - | ETPattern -> weaken_entry Constr.pattern, None + | ETConstr (10,_) -> weaken_entry Constr.lconstr, None, true + | ETConstr (9,_) -> weaken_entry Constr.constr9, None, true + | ETConstr (n,q) -> weaken_entry Constr.constr, adjust (n,q), false + | ETIdent -> weaken_entry Constr.ident, None, false + | ETBigint -> weaken_entry Prim.bigint, None, false + | ETReference -> weaken_entry Constr.global, None, false + | ETPattern -> weaken_entry Constr.pattern, None, false | ETOther (u,n) -> let u = get_univ u in let e = try get_entry u n with e when allow_create -> create_entry u n ConstrArgType in - object_of_typed_entry e, None + object_of_typed_entry e, None, true let get_constr_entry = compute_entry true (fun (n,()) -> Some n) + let get_constr_production_entry ass = compute_entry false (adjust_level ass) let constr_prod_level = function @@ -546,7 +547,7 @@ let constr_prod_level = function let symbol_of_production assoc typ = match get_constr_production_entry assoc typ with - | (eobj,None) -> Gramext.Snterm (Gram.Entry.obj eobj) - | (eobj,Some None) -> Gramext.Snext - | (eobj,Some (Some lev)) -> + | (eobj,None,_) -> Gramext.Snterm (Gram.Entry.obj eobj) + | (eobj,Some None,_) -> Gramext.Snext + | (eobj,Some (Some lev),_) -> Gramext.Snterml (Gram.Entry.obj eobj,constr_prod_level lev) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index f643b408d..7409a9e80 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -33,7 +33,7 @@ val object_of_typed_entry : typed_entry -> grammar_object Gram.Entry.e val weaken_entry : 'a Gram.Entry.e -> grammar_object Gram.Entry.e val get_constr_entry : - constr_entry -> grammar_object Gram.Entry.e * int option + constr_entry -> grammar_object Gram.Entry.e * int option * bool val symbol_of_production : Gramext.g_assoc option -> constr_production_entry -> Token.t Gramext.g_symbol diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 564fc48d8..02148a53e 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -187,7 +187,7 @@ let add_tactic_grammar g = let print_grammar univ entry = let u = get_univ univ in let typ = explicitize_entry (fst u) entry in - let te,_ = get_constr_entry typ in + let te,_,_ = get_constr_entry typ in Gram.Entry.print te (* Infix, distfix, notations *) |