X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=fddf27e9995a100f72df291fcc478def9cf601fd;hb=1fe616bda25a6208c4d19f61220e570c71bcc25a;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..fddf27e99 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: [
@@ -233,16 +240,18 @@ EXTEND
     [ PAREN "["; idents = LIST1 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]
   ];
   reduction_kind: [
-    [ "reduce" -> `Reduce
-    | "simpl" -> `Simpl
-    | "whd" -> `Whd ]
+    [ [ IDENT "reduce" | IDENT "Reduce" ] -> `Reduce
+    | [ IDENT "simplify" | IDENT "Simplify" ] -> `Simpl
+    | [ IDENT "whd" | IDENT "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 "auto" | IDENT "Auto" ] -> return_tactic loc TacticAst.Auto
     | [ IDENT "change" | IDENT "Change" ];
       t1 = tactic_term; "with"; t2 = tactic_term;
       where = tactic_where ->
@@ -258,8 +267,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 +282,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,11 +290,26 @@ 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 *)
+    | kind = reduction_kind;
+      pat = OPT [
+        "in"; pat = [ IDENT "goal" -> `Goal | IDENT "hyp" -> `Everywhere ] ->
+          pat
+      ];
+      terms = LIST0 term SEP SYMBOL "," ->
+        let tac =
+          (match (pat, terms) with
+          | None, [] -> TacticAst.Reduce (kind, None)
+          | None, terms -> TacticAst.Reduce (kind, Some (terms, `Goal))
+          | Some pat, [] -> TacticAst.Reduce (kind, Some ([], pat))
+          | Some pat, terms -> TacticAst.Reduce (kind, Some (terms, pat)))
+        in
+        return_tactic loc tac
     | [ IDENT "reflexivity" | IDENT "Reflexivity" ] ->
         return_tactic loc TacticAst.Reflexivity
     | [ IDENT "replace" | IDENT "Replace" ];
@@ -303,7 +327,7 @@ EXTEND
         return_tactic loc (TacticAst.Transitivity t)
     ]
   ];
-  tactical0: [ [ t = tactical; SYMBOL "." -> t ] ];
+  tactical0: [ [ t = tactical; SYMBOL ";;" -> return_tactical loc t ] ];
   tactical:
     [ "command" NONA
       [ cmd = command -> return_tactical loc (TacticAst.Command cmd) ]
@@ -356,6 +380,14 @@ 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 "baseuri"   | IDENT "Baseuri" ]; uri = OPT QSTRING ->
+        return_command loc (TacticAst.Baseuri uri)
+    | [ IDENT "check"   | IDENT "Check" ]; t = term ->
+        return_command loc (TacticAst.Check t)
     ]
   ];
 END