aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/extend.ml
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-12-03 08:33:12 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-12-03 08:33:12 +0000
commit98b16fa6af9fd6c37120b29d96ea0785a8598335 (patch)
tree0ef1354cedbe5f977e77692ffa9ee6deca877560 /parsing/extend.ml
parent72f121c514c0dc2f8942a1e4395ec5843d5e901c (diff)
Calcul de l'associativité même pour les Grammar avec plusieurs clauses
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3360 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/extend.ml')
-rw-r--r--parsing/extend.ml18
1 files changed, 9 insertions, 9 deletions
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 64d8cc7cd..a49ec01b0 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -245,18 +245,18 @@ let border = function
| NonTerm (ProdPrimitive (ETConstr(_,BorderProd (_,a))),_) :: _ -> a
| _ -> None
-let clever_assoc ass = function
- | [g] when g.gr_production <> [] ->
- (match border g.gr_production, border (List.rev g.gr_production) with
- | Some LeftA, Some RightA -> ass (* Untractable; we cheat *)
- | Some LeftA, _ -> Some LeftA
- | _, Some RightA -> Some RightA
- | _ -> Some NonA)
- | _ -> ass
+let clever_assoc ass g =
+ if g.gr_production <> [] then
+ (match border g.gr_production, border (List.rev g.gr_production) with
+ | Some LeftA, Some RightA -> ass (* Untractable; we cheat *)
+ | Some LeftA, _ -> Some LeftA
+ | _, Some RightA -> Some RightA
+ | _ -> Some NonA)
+ else ass
let gram_entry univ (nt, ass, rl) =
let l = List.map (gram_rule (univ,nt)) rl in
- let ass = clever_assoc ass l in
+ let ass = List.fold_left clever_assoc ass l in
{ ge_name = nt;
gl_assoc = ass;
gl_rules = l }