From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 10 Mar 2003 09:53:12 +0000 (+0000)
Subject: Big change: parenthesis can now be put in any place to disambiguate the
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fb12bdf2cf0ecbf50726b70d6a3097cb933319a0;p=helm.git

Big change: parenthesis can now be put in any place to disambiguate the
expression. The case "(expr) -> expr" is no more an exception. An application
node is generated iff more than one expression is put inside the parenthesis.
---

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
index 11313aeff..5afd56ed9 100644
--- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
@@ -297,14 +297,16 @@ expr2:
     { let dom,mk_substitutionlist = $3 in
        dom, function interp -> Meta ($1, mk_substitutionlist interp)
     } 
- | LPAREN expr expr exprlist RPAREN
-    { let dom1,mk_expr1 = $2 in
-      let dom2,mk_expr2 = $3 in
-      let dom3,mk_exprlist = $4 in
-       let dom = union dom1 (union dom2 dom3) in
-        dom,
-         function interp ->
-          Appl ([mk_expr1 interp ; mk_expr2 interp]@(mk_exprlist interp))
+ | LPAREN expr exprlist RPAREN
+    { let length,dom2,mk_exprlist = $3 in
+       match length with
+          0 -> $2
+        | _ ->
+          let dom1,mk_expr1 = $2 in
+           let dom = union dom1 dom2 in
+            dom,
+             function interp ->
+              Appl ((mk_expr1 interp)::(mk_exprlist interp))
     }
 ;
 exp_named_subst :
@@ -417,11 +419,6 @@ pihead:
      let dom,mk_expr = $1 in
       Anonymous, (dom, function interp -> mk_expr interp)
    }
- | LPAREN expr RPAREN ARROW
-   { CicTextualParser0.binders := (Some Anonymous)::!CicTextualParser0.binders ;
-     let dom,mk_expr = $2 in
-      Anonymous, (dom, function interp -> mk_expr interp)
-   }
  | PROD ID DOT
     { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
       let newmeta = new_meta () in
@@ -478,12 +475,12 @@ branches:
 ;
 exprlist:
     
-    { [], function _ -> [] }
+    { 0, [], function _ -> [] }
  | expr exprlist
     { let dom1,mk_expr = $1 in
-      let dom2,mk_exprlist = $2 in
+      let length,dom2,mk_exprlist = $2 in
        let dom = union dom1 dom2 in
-        dom, function interp -> (mk_expr interp)::(mk_exprlist interp)
+        length+1, dom, function interp -> (mk_expr interp)::(mk_exprlist interp)
     }
 ;
 exprseplist: