Grammar factorized to avoid shift/reduced conflicts that were handled in

the wrong way. No more conflicts left.

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
index a98628702a0a759280434ad8ce00f4eca1827ad2..f3dc1b05e0cb001c9f03c8e5496dc184a19149c4 100644 (file)
--- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
@@ -29,6 +29,7 @@
 
  exception InvalidSuffix of string;;
  exception InductiveTypeURIExpected;;
+ exception UnknownIdentifier of string;;
  
  let uri_of_id_map = Hashtbl.create 53;;
 
@@ -56,6 +57,7 @@
 %token ALIAS
 %token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT
 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW EOF
+%right ARROW
 %start main
 %type <Cic.term option> main
 %%
@@ -64,7 +66,7 @@ main:
  | alias { None }
  | EOF   { raise CicTextualParser0.Eof }
 ;
-expr:
+expr2:
    CONURI
    { let uri = UriManager.string_of_uri $1 in
      let suff = (String.sub uri (String.length uri - 3) 3) in
@@ -87,7 +89,11 @@ expr:
        Rel (get_index_in_list (Name $1) !CicTextualParser0.binders)
      with
       Not_found ->
-       Hashtbl.find uri_of_id_map $1
+       try
+        Hashtbl.find uri_of_id_map $1
+       with
+        Not_found ->
+         raise (UnknownIdentifier $1)
    }
  | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
     { let cookingno = get_cookingno (fst $5) in
@@ -152,15 +158,19 @@ expr:
  | LPAREN expr CAST expr RPAREN { Cast ($2,$4) }
  | META { Meta $1 }
  | LPAREN expr expr exprlist RPAREN { Appl ([$2;$3]@$4) }
- | pihead expr 
+;
+expr :
+   pihead expr
     { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
       Prod (fst $1, snd $1,$2) }
- | lambdahead expr 
+ | lambdahead expr
     { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
       Lambda (fst $1, snd $1,$2) }
- | letinhead expr 
+ | letinhead expr
     { CicTextualParser0.binders := List.tl !CicTextualParser0.binders ;
       LetIn (fst $1, snd $1,$2) }
+ | expr2
+    { $1 }
 ;
 fixheader:
    FIX ID LCURLY fixfunsdecl RCURLY
@@ -192,7 +202,7 @@ pihead:
    PROD ID COLON expr DOT
     { CicTextualParser0.binders := (Name $2)::!CicTextualParser0.binders ;
       (Cic.Name $2, $4) }
- | expr ARROW
+ | expr2 ARROW
    { CicTextualParser0.binders := Anonimous::!CicTextualParser0.binders ;
      (Anonimous, $1) }
  | LPAREN expr RPAREN ARROW