X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=d32302a131e11c2d67ce292c4744ec6e18d995c1;hb=44d302801af535a58c207b33960b7cfdb116a933;hp=44587104554a7955fcd0bab31da800b232cf8036;hpb=89c46fa15cd1dd1c9b180e569a27df490c28443d;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 445871045..d32302a13 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -102,6 +102,13 @@ let ind_expansion uri =
   else
     uri
 
+let mk_binder_ast binder typ vars body =
+  List.fold_right
+    (fun var body ->
+       let name = name_of_string var in
+       CicAst.Binder (binder, (name, typ), body))
+    vars body
+
 EXTEND
   GLOBAL: term term0 tactic tactical tactical0 command script;
   int: [
@@ -115,12 +122,12 @@ EXTEND
     [ s = SYMBOL "_" -> None
     | t = term -> Some t ]
   ];
-  binder: [
-    [ SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda
-    | SYMBOL <:unicode<Pi>>     (* Π *) -> `Pi
+  binder_low: [
+    [ SYMBOL <:unicode<Pi>>     (* Π *) -> `Pi
     | SYMBOL <:unicode<exists>> (* ∃ *) -> `Exists
     | SYMBOL <:unicode<forall>> (* ∀ *) -> `Forall ]
   ];
+  binder_high: [ [ SYMBOL <:unicode<lambda>> (* λ *) -> `Lambda ] ];
   sort: [
     [ "Prop" -> `Prop
     | "Set" -> `Set
@@ -214,6 +221,13 @@ EXTEND
       ] SEP "and" -> defs
     ]];
   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
+  binder_vars: [
+      [ vars = LIST1 IDENT SEP SYMBOL ",";
+        typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
+      | PAREN "("; vars = LIST1 IDENT SEP SYMBOL ",";
+        typ = OPT [ SYMBOL ":"; t = term -> t ]; PAREN ")" -> (vars, typ)
+      ]
+  ];
   term0: [ [ t = term; EOI -> return_term loc t ] ];
   term:
     [ "letin" NONA
@@ -225,35 +239,13 @@ EXTEND
         defs = let_defs; "in"; body = term ->
             return_term loc (CicAst.LetRec (ind_kind, defs, body))
       ]
-    | "apply" LEFTA
-      [ t1 = term; t2 = term ->
-        let rec aux = function
-          | CicAst.Appl (hd :: tl) -> aux hd @ tl
-          | term -> [term]
-        in
-        CicAst.Appl (aux t1 @ [t2])
-      ]
     | "binder" RIGHTA
       [
-        b = binder;
-        (vars, typ) =
-          [ vars = LIST1 IDENT SEP SYMBOL ",";
-            typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
-          | PAREN "("; vars = LIST1 IDENT SEP SYMBOL ",";
-            typ = OPT [ SYMBOL ":"; t = term -> t ]; PAREN ")" -> (vars, typ)
-          ];
-        SYMBOL "."; body = term ->
-          let binder =
-            List.fold_right
-              (fun var body ->
-                let name = name_of_string var in
-                CicAst.Binder (b, (name, typ), body))
-              vars body
-          in
+        b = binder_low; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
+          let binder = mk_binder_ast b typ vars body in
           return_term loc binder
       | t1 = term; SYMBOL <:unicode<to>> (* → *); t2 = term ->
-            return_term loc
-              (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
+          return_term loc (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
       ]
     | "logic_add" LEFTA   [ (* nothing here by default *) ]
     | "logic_mult" LEFTA  [ (* nothing here by default *) ]
@@ -266,6 +258,20 @@ EXTEND
     | "mult" LEFTA    [ (* nothing here by default *) ]
     | "power" LEFTA   [ (* nothing here by default *) ]
     | "inv" NONA      [ (* nothing here by default *) ]
+    | "apply" LEFTA
+      [ t1 = term; t2 = term ->
+        let rec aux = function
+          | CicAst.Appl (hd :: tl) -> aux hd @ tl
+          | term -> [term]
+        in
+        CicAst.Appl (aux t1 @ [t2])
+      ]
+    | "binder" RIGHTA
+      [
+        b = binder_high; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
+          let binder = mk_binder_ast b typ vars body in
+          return_term loc binder
+      ]
     | "simple" NONA
       [ sort = sort -> CicAst.Sort sort
       | n = substituted_name -> return_term loc n