removed debug prerr_endline

[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 431b15ae83d807617aeef459fbec3d9e621ac068..9f5fd193e9d170c05ef4fe9473e175c9805d251d 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -69,6 +69,7 @@ let alias_spec = Grammar.Entry.create grammar "alias_spec"
 let macro = Grammar.Entry.create grammar "macro"
 let script = Grammar.Entry.create grammar "script"
 let statement = Grammar.Entry.create grammar "statement"
+let statements = Grammar.Entry.create grammar "statements"
 
 let return_term loc term = CicAst.AttributedTerm (`Loc loc, term)
 
@@ -116,7 +117,7 @@ let mk_binder_ast binder typ vars body =
     vars body
 
 EXTEND
-  GLOBAL: term term0 statement;
+  GLOBAL: term term0 statement statements;
   int: [
     [ num = NUM ->
         try
@@ -147,20 +148,18 @@ EXTEND
     ]
   ];
   subst: [
-    [ subst = OPT [
-        SYMBOL "\\subst";  (* to avoid catching frequent "a [1]" cases *)
-        PAREN "[";
-        substs = LIST1 [
-          i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
-        ] SEP SYMBOL ";";
-        PAREN "]" ->
-          substs
-      ] -> subst
+    [ SYMBOL "\\subst";  (* to avoid catching frequent "a [1]" cases *)
+      PAREN "[";
+      substs = LIST1 [
+        i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
+      ] SEP SYMBOL ";";
+      PAREN "]" ->
+        substs
     ]
   ];
   substituted_name: [ (* a subs.name is an explicit substitution subject *)
-    [ s = IDENT; subst = subst -> CicAst.Ident (s, subst)
-    | s = URI; subst = subst -> CicAst.Uri (ind_expansion s, subst)
+    [ s = IDENT; subst = OPT subst -> CicAst.Ident (s, subst)
+    | s = URI; subst = OPT subst -> CicAst.Uri (ind_expansion s, subst)
     ]
   ];
   name: [ (* as substituted_name with no explicit substitution *)
@@ -250,6 +249,11 @@ EXTEND
         b = binder_low; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
           let binder = mk_binder_ast b typ vars body in
           return_term loc binder
+      | b = binder_high; (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))
       ]
     | "logic_add" LEFTA   [ (* nothing here by default *) ]
     | "logic_mult" LEFTA  [ (* nothing here by default *) ]
@@ -270,14 +274,6 @@ EXTEND
         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
-      | t1 = term; SYMBOL <:unicode<to>> (* → *); t2 = term ->
-          return_term loc (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
-      ]
     | "simple" NONA
       [ sort = sort -> CicAst.Sort sort
       | n = substituted_name -> return_term loc n
@@ -591,6 +587,10 @@ EXTEND
     | com = comment -> TacticAst.Comment (loc, com)
     ]
   ];
+  statements: [
+    [ l = LIST0 [ statement ] -> l 
+    ]  
+  ];
 END
 
 let exc_located_wrapper f =
@@ -606,6 +606,9 @@ let parse_term stream =
   exc_located_wrapper (fun () -> (Grammar.Entry.parse term0 stream))
 let parse_statement stream =
   exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream))
+let parse_statements stream =
+  exc_located_wrapper (fun () -> (Grammar.Entry.parse statements stream))
+  
 
 (**/**)