symmetry of equality NOT used in auto

[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 a539fef6c238783365912191b037985ec8a75a3d..fddf27e9995a100f72df291fcc478def9cf601fd 100644 (file)
--- 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
 
@@ -158,12 +158,12 @@ EXTEND
       [
         b = binder;
         (vars, typ) =
-          [ vars = LIST1 IDENT;
+          [ vars = LIST1 IDENT SEP SYMBOL ",";
             typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
-          | PAREN "("; vars = LIST1 IDENT;
+          | PAREN "("; vars = LIST1 IDENT SEP SYMBOL ",";
             typ = OPT [ SYMBOL ":"; t = term -> t ]; PAREN ")" -> (vars, typ)
           ];
-        SYMBOL ","; body = term ->
+        SYMBOL "."; body = term ->
           let binder =
             List.fold_right
               (fun var body ->
@@ -240,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 ->
@@ -265,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;
@@ -281,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" ];
@@ -294,7 +296,20 @@ EXTEND
     | [ "let" | "Let" ];
       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" ];
@@ -312,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) ]
@@ -369,6 +384,10 @@ EXTEND
         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