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

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index d062ed109..d32302a13 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -23,7 +23,7 @@
  * http://helm.cs.unibo.it/
  *)
 
-let debug = true
+let debug = false
 let debug_print s =
   if debug then begin
     prerr_endline "<NEW_TEXTUAL_PARSER>";
@@ -35,12 +35,17 @@ let debug_print s =
   * thus be interpreted differently than others *)
 let use_fresh_num_instances = false
 
+  (** does the lexer return COMMENT tokens? *)
+let return_comments = false
+
 open Printf
 
 open DisambiguateTypes
 
 exception Parse_error of Token.flocation * string
 
+let cic_lexer = CicTextualLexer2.cic_lexer ~comments:return_comments ()
+
 let fresh_num_instance =
   let n = ref 0 in
   if use_fresh_num_instances then
@@ -52,7 +57,7 @@ let choice_of_uri uri =
   let term = CicUtil.term_of_uri uri in
   (uri, (fun _ _ _ -> term))
 
-let grammar = Grammar.gcreate CicTextualLexer2.cic_lexer
+let grammar = Grammar.gcreate cic_lexer
 
 let term = Grammar.Entry.create grammar "term"
 let term0 = Grammar.Entry.create grammar "term0"
@@ -97,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: [
@@ -110,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
@@ -209,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
@@ -222,25 +241,11 @@ EXTEND
       ]
     | "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 *) ]
@@ -261,6 +266,12 @@ 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
+      ]
     | "simple" NONA
       [ sort = sort -> CicAst.Sort sort
       | n = substituted_name -> return_term loc n
@@ -358,7 +369,7 @@ EXTEND
         let idents = match idents with None -> [] | Some idents -> idents in
         return_tactic loc (TacticAst.Intros (num, idents))
     | [ IDENT "intro" | IDENT "Intro" ] ->
-        return_tactic loc (TacticAst.Intros (Some 1, []))
+        return_tactic loc (TacticAst.Intros (None, []))
     | [ IDENT "left" | IDENT "Left" ] -> return_tactic loc TacticAst.Left
     | [ "let" | "Let" ];
       t = tactic_term; "in"; where = IDENT ->
@@ -400,7 +411,9 @@ EXTEND
       [ cmd = command -> return_tactical loc (TacticAst.Command cmd) ]
     | "sequence" LEFTA
       [ tactics = LIST1 NEXT SEP SYMBOL ";" ->
-          return_tactical loc (TacticAst.Seq tactics)
+          (match tactics with
+          | [tactic] -> tactic
+          | _ -> return_tactical loc (TacticAst.Seq tactics))
       ]
     | "then" NONA
       [ tac = tactical;
@@ -459,6 +472,8 @@ EXTEND
   print_kind: [
     [ [ IDENT "Env" | IDENT "env" | IDENT "Environment" | IDENT "environment" ]
       -> `Env
+    | [ IDENT "Coer" | IDENT "coer" | IDENT "Coercions" | IDENT "coercions" ]
+      -> `Coer
   ] ];
 
   command: [
@@ -523,7 +538,7 @@ EXTEND
   ];
   script_entry: [
     [ cmd = tactical0 -> Command cmd
-    | s = COMMENT -> Comment (loc, s)
+(*     | s = COMMENT -> Comment (loc, s) *)
     ]
   ];
   script: [ [ entries = LIST0 script_entry; EOI -> (loc, entries) ] ];
@@ -557,7 +572,7 @@ module EnvironmentP3 =
 
     let empty = ""
 
-    let aliases_grammar = Grammar.gcreate CicTextualLexer2.cic_lexer
+    let aliases_grammar = Grammar.gcreate cic_lexer
     let aliases = Grammar.Entry.create aliases_grammar "aliases"
 
     let to_string env =