X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=0c00d869809435ce403d5ce4e5c0130237bc2406;hb=b6658a4a5c874be0223f44c7c1b99900185cbc60;hp=c64fcd42cb96faad16d4efb759b3fcb52324ffe1;hpb=e3ce9e2940a9e9c736209517e20e4c4292fdd0c3;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index c64fcd42c..0c00d8698 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -47,9 +47,9 @@ let fresh_num_instance =
   else
     (fun () -> 0)
 
-let choice_of_uri (uri: string) =
-  let cic = HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri) in
-  (uri, (fun _ _ _ -> cic))
+let choice_of_uri uri =
+  let term = CicUtil.term_of_uri uri in
+  (uri, (fun _ _ _ -> term))
 
 let grammar = Grammar.gcreate CicTextualLexer2.cic_lexer
 
@@ -73,6 +73,10 @@ let name_of_string = function
   | "_" -> Cic.Anonymous
   | s -> Cic.Name s
 
+let int_opt = function
+  | None -> None
+  | Some lexeme -> Some (int_of_string lexeme)
+
 EXTEND
   GLOBAL: term term0 tactic tactical tactical0 command;
   int: [
@@ -108,7 +112,7 @@ EXTEND
     ]
   ];
   substituted_name: [ (* a subs.name is an explicit substitution subject *)
-    [ s = [ IDENT | SYMBOL ];
+    [ s = IDENT;
       subst = OPT [
         SYMBOL "\\subst";  (* to avoid catching frequent "a [1]" cases *)
         PAREN "[";
@@ -133,12 +137,9 @@ EXTEND
   term0: [ [ t = term; EOI -> return_term loc t ] ];
   term:
     [ "letin" NONA
-        (* actually "in" and "and" are _not_ keywords. Parsing works anyway
-         * since applications are required to be bound by parens *)
       [ "let"; var = typed_name;
         SYMBOL "="; (* SYMBOL <:unicode<def>> (* ≝ *); *)
-        t1 = term;
-        IDENT "in"; t2 = term ->
+        t1 = term; "in"; t2 = term ->
           return_term loc (CicAst.LetIn (var, t1, t2))
       | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
           defs = LIST1 [
@@ -149,8 +150,8 @@ EXTEND
             SYMBOL "="; (* SYMBOL <:unicode<def>> (* ≝ *); *)
             t1 = term ->
               (var, t1, (match index with None -> 0 | Some i -> i))
-          ] SEP (IDENT "and");
-          IDENT "in"; body = term ->
+          ] SEP "and";
+          "in"; body = term ->
             return_term loc (CicAst.LetRec (ind_kind, defs, body))
       ]
     | "binder" RIGHTA
@@ -186,11 +187,17 @@ 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])
+      ]
     | "simple" NONA
       [ sort = sort -> CicAst.Sort sort
       | n = substituted_name -> return_term loc n
-      | PAREN "("; head = term; args = LIST1 term; PAREN ")" ->
-          return_term loc (CicAst.Appl (head :: args))
       | i = NUM -> return_term loc (CicAst.Num (i, (fresh_num_instance ())))
       | IMPLICIT -> return_term loc CicAst.Implicit
       | m = META;
@@ -223,7 +230,7 @@ EXTEND
       ]
     ];
   tactic_where: [
-    [ where = OPT [ IDENT "in"; ident = IDENT -> ident ] -> where ]
+    [ where = OPT [ "in"; ident = IDENT -> ident ] -> where ]
   ];
   tactic_term: [ [ t = term -> t ] ];
   ident_list0: [
@@ -238,9 +245,10 @@ EXTEND
     | "whd" -> `Whd ]
   ];
   tactic: [
-    [ [ IDENT "absurd" | IDENT "Absurd" ] -> return_tactic loc TacticAst.Absurd
-    | [ IDENT "apply" | IDENT "Apply" ];
-      t = tactic_term -> return_tactic loc (TacticAst.Apply t)
+    [ [ IDENT "absurd" | IDENT "Absurd" ]; t = tactic_term ->
+        return_tactic loc (TacticAst.Absurd t)
+    | [ IDENT "apply" | IDENT "Apply" ]; t = tactic_term ->
+        return_tactic loc (TacticAst.Apply t)
     | [ IDENT "assumption" | IDENT "Assumption" ] ->
         return_tactic loc TacticAst.Assumption
     | [ IDENT "change" | IDENT "Change" ];
@@ -258,8 +266,7 @@ EXTEND
     | [ IDENT "discriminate" | IDENT "Discriminate" ];
       hyp = IDENT ->
         return_tactic loc (TacticAst.Discriminate hyp)
-    | [ IDENT "elim" | IDENT "Elim" ]; IDENT "type";
-      t = tactic_term ->
+    | [ IDENT "elimType" | IDENT "ElimType" ]; t = tactic_term ->
         return_tactic loc (TacticAst.ElimType t)
     | [ IDENT "elim" | IDENT "Elim" ];
       t1 = tactic_term;
@@ -274,6 +281,7 @@ EXTEND
         return_tactic loc (TacticAst.Fold (kind, t))
     | [ IDENT "fourier" | IDENT "Fourier" ] ->
         return_tactic loc TacticAst.Fourier
+    | [ IDENT "hint" | IDENT "Hint" ] -> return_tactic loc TacticAst.Hint
     | [ IDENT "injection" | IDENT "Injection" ]; ident = IDENT ->
         return_tactic loc (TacticAst.Injection ident)
     | [ IDENT "intros" | IDENT "Intros" ];
@@ -281,9 +289,11 @@ EXTEND
       idents = OPT ident_list0 ->
         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, []))
     | [ IDENT "left" | IDENT "Left" ] -> return_tactic loc TacticAst.Left
     | [ "let" | "Let" ];
-      t = tactic_term; IDENT "in"; where = IDENT ->
+      t = tactic_term; "in"; where = IDENT ->
         return_tactic loc (TacticAst.LetIn (t, where))
     (* TODO Reduce *)
     | [ IDENT "reflexivity" | IDENT "Reflexivity" ] ->
@@ -303,7 +313,7 @@ EXTEND
         return_tactic loc (TacticAst.Transitivity t)
     ]
   ];
-  tactical0: [ [ t = tactical; SYMBOL "." -> t ] ];
+  tactical0: [ [ t = tactical; SYMBOL ";;" -> t ] ];
   tactical:
     [ "command" NONA
       [ cmd = command -> return_tactical loc (TacticAst.Command cmd) ]
@@ -356,6 +366,12 @@ EXTEND
     | [ IDENT "goal" | IDENT "Goal" ]; typ = term;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
         return_command loc (TacticAst.Theorem (`Goal, None, typ, body))
+    | [ IDENT "undo"   | IDENT "Undo" ]; steps = OPT NUM ->
+        return_command loc (TacticAst.Undo (int_opt steps))
+    | [ IDENT "redo"   | IDENT "Redo" ]; steps = OPT NUM ->
+        return_command loc (TacticAst.Redo (int_opt steps))
+    | [ IDENT "check"   | IDENT "Check" ]; t = term ->
+        return_command loc (TacticAst.Check t)
     ]
   ];
 END