X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=775f13f7d7e0f8803baa7f1a58f9408fd17cc8fa;hb=142d3076f2a4dc17d9045c2bba4d4b01eddfd008;hp=8eca106304e96def0c883fa11885889751abcfcd;hpb=7a72e5c5129c814e567f03e14d752eff4086fb52;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 8eca10630..775f13f7d 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
 
@@ -65,13 +65,18 @@ let return_tactic loc tactic = TacticAst.LocatedTactic (loc, tactic)
 let return_tactical loc tactical = TacticAst.LocatedTactical (loc, tactical)
 let return_command loc cmd = cmd
 
-let fail (x, y) msg =
+let fail floc msg =
+  let (x, y) = CicAst.loc_of_floc floc in
   failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
 
 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: [
@@ -79,7 +84,7 @@ EXTEND
         try
           int_of_string num
         with Failure _ ->
-          let (x, y) = loc in
+          let (x, y) = CicAst.loc_of_floc loc in
           raise (Parse_error (sprintf
             "integer literal expected at characters %d-%d" x y))
     ]
@@ -107,9 +112,9 @@ 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 *)
+        SYMBOL "\\subst";  (* to avoid catching frequent "a [1]" cases *)
         PAREN "[";
         substs = LIST1 [
           i = IDENT; SYMBOL <:unicode<Assign>> (* ≔ *); t = term -> (i, t)
@@ -132,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 [
@@ -148,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
@@ -185,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;
@@ -222,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: [
@@ -237,11 +245,13 @@ 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 "auto" | IDENT "Auto" ] -> return_tactic loc TacticAst.Auto
     | [ IDENT "change" | IDENT "Change" ];
       t1 = tactic_term; "with"; t2 = tactic_term;
       where = tactic_where ->
@@ -257,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;
@@ -273,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" ];
@@ -280,9 +290,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" ] ->
@@ -302,9 +314,11 @@ EXTEND
         return_tactic loc (TacticAst.Transitivity t)
     ]
   ];
-  tactical0: [ [ t = tactical; SYMBOL "." -> t ] ];
+  tactical0: [ [ t = tactical; SYMBOL ";;" -> return_tactical loc t ] ];
   tactical:
-    [ "sequence" LEFTA
+    [ "command" NONA
+      [ cmd = command -> return_tactical loc (TacticAst.Command cmd) ]
+    | "sequence" LEFTA
       [ tactics = LIST1 NEXT SEP SYMBOL ";" ->
           return_tactical loc (TacticAst.Seq tactics)
       ]
@@ -329,7 +343,6 @@ EXTEND
       | [ IDENT "id" | IDENT "Id" ] -> return_tactical loc TacticAst.IdTac
       | PAREN "("; tac = tactical; PAREN ")" -> return_tactical loc tac
       | tac = tactic -> return_tactical loc (TacticAst.Tactic tac)
-      | cmd = command -> return_tactical loc (TacticAst.Command cmd)
       ]
     ];
   theorem_flavour: [  (* all flavours but Goal *)
@@ -341,7 +354,8 @@ EXTEND
     ]
   ];
   command: [
-    [ [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof
+    [ [ IDENT "abort" | IDENT "Abort" ] -> return_command loc TacticAst.Abort
+    | [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof
     | [ IDENT "quit"  | IDENT "Quit"  ] -> return_command loc TacticAst.Quit
     | [ IDENT "qed"   | IDENT "Qed"   ] ->
         return_command loc (TacticAst.Qed None)
@@ -353,6 +367,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
@@ -360,7 +382,8 @@ END
 let exc_located_wrapper f =
   try
     Lazy.force f
-  with Stdpp.Exc_located ((x, y), exn) ->
+  with Stdpp.Exc_located (floc, exn) ->
+    let (x, y) = CicAst.loc_of_floc floc in
     raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
         (Printexc.to_string exn)))
 
@@ -437,7 +460,8 @@ module EnvironmentP3 =
       else
         try
           Grammar.Entry.parse aliases (Stream.of_string s)
-        with Stdpp.Exc_located ((x, y), exn) ->
+        with Stdpp.Exc_located (floc, exn) ->
+          let (x, y) = CicAst.loc_of_floc floc in
           raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
           (Printexc.to_string exn)))
   end