From d334f75272a29dae279ce5ef48f3dc9f3026ddb5 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 28 Nov 2002 01:21:07 +0000 Subject: Affinement encore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3316 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/egrammar.ml | 8 ++++++-- parsing/extend.ml | 17 ++++++++++++++++- 2 files changed, 22 insertions(+), 3 deletions(-) (limited to 'parsing') diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 84b1aa0f0..a7cfcc591 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -50,6 +50,10 @@ let constr_level assoc = function | 8 -> assert (assoc <> Some Gramext.LeftA); "top" | n -> (string_of_int n)^(assoc_level (canonise_assoc assoc)) +let constr_prod_level = function + | 8 -> "top" + | n -> string_of_int n + let numeric_levels = ref [8,Some Gramext.RightA; 1,Some Gramext.RightA; 0,Some Gramext.RightA] @@ -67,7 +71,7 @@ let eq_assoc a b = match (canonise_assoc a, canonise_assoc b) with let find_position assoc = function | None -> None, Some (canonise_assoc assoc) | Some n -> - if n = 8 & assoc = Some Gramext.LeftA then + if n = 8 & canonise_assoc assoc = Gramext.LeftA then error "Left associativity not allowed at level 8"; let after = ref (8,Some Gramext.RightA) in let rec add_level q = function @@ -176,7 +180,7 @@ let rec build_prod_item univ assoc = function match get_constr_production_entry assoc typ with | (eobj,None) -> Gramext.Snterm (Gram.Entry.obj eobj) | (eobj,Some lev) -> - Gramext.Snterml (Gram.Entry.obj eobj,constr_level assoc lev) + Gramext.Snterml (Gram.Entry.obj eobj,constr_prod_level lev) let symbol_of_prod_item univ assoc = function | Term tok -> (Gramext.Stoken tok, None) diff --git a/parsing/extend.ml b/parsing/extend.ml index 04a31fa49..ae3561c1f 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -234,10 +234,25 @@ let gram_rule univ (name,pil,act) = let a = to_act_check_vars act_env act in { gr_name = name; gr_production = pilc; gr_action = a } +let border = function + | NonTerm (ProdPrimitive (ETConstr(_,BorderProd (_,a))),_) :: _ -> a + | _ -> None + +let clever_assoc = function + | [g] when g.gr_production <> [] -> + (match border g.gr_production, border (List.rev g.gr_production) with + Some RightA, Some LeftA -> Some NonA + | a, b when a=b -> a + | Some LeftA, Some RightA -> Some LeftA (* since LR *) + | _ -> None) + | _ -> None + let gram_entry univ (nt, ass, rl) = + let l = List.map (gram_rule (univ,nt)) rl in + let ass = if ass = None then clever_assoc l else ass in { ge_name = nt; gl_assoc = ass; - gl_rules = List.map (gram_rule (univ,nt)) rl } + gl_rules = l } let interp_grammar_command univ ge entryl = { gc_univ = univ; -- cgit v1.2.3