added tactic and tactical (still heavily bugged!!!)

diff --git a/helm/ocaml/cic_disambiguation/.depend b/helm/ocaml/cic_disambiguation/.depend
index 2a5719e54894ca4689b3dd0277f063fbf2427389..b8c5c9ccff4470314f547603340c4104cd69dfff 100644 (file)
--- a/helm/ocaml/cic_disambiguation/.depend
+++ b/helm/ocaml/cic_disambiguation/.depend
@@ -23,5 +23,3 @@ logic_notation.cmo: cicTextualParser2.cmi disambiguateChoices.cmi
 logic_notation.cmx: cicTextualParser2.cmx disambiguateChoices.cmx 
 arit_notation.cmo: cicTextualParser2.cmi disambiguateChoices.cmi 
 arit_notation.cmx: cicTextualParser2.cmx disambiguateChoices.cmx 
-tex_notation.cmo: cicTextualParser2.cmi 
-tex_notation.cmx: cicTextualParser2.cmx 

diff --git a/helm/ocaml/cic_disambiguation/Makefile b/helm/ocaml/cic_disambiguation/Makefile
index ea516c526930d5c4144ab0ccdac8477861f1e2af..34ade20718136b8cfe8e878f76cab4261801e6d9 100644 (file)
--- a/helm/ocaml/cic_disambiguation/Makefile
+++ b/helm/ocaml/cic_disambiguation/Makefile
@@ -69,6 +69,7 @@ extra_clean:
        rm -f test_lexer test_parser make_table
 
 include ../Makefile.common
+OCAMLARCHIVEOPTIONS += -linkall
 
 .PHONY: depend
 depend: cicTextualParser2Macro.cmi cicTextualParser2Macro.cmo pa_unicode_macro.cmi pa_unicode_macro.cmo

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 793d95e025fe89cdf8fcae17c8b65e30596576ec..349825bf99b53a33c0bd399a83fb88a890a51489 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -43,11 +43,13 @@ let grammar = Grammar.gcreate CicTextualLexer2.cic_lexer
 
 let term = Grammar.Entry.create grammar "term"
 let term0 = Grammar.Entry.create grammar "term0"
-(* let tactic = Grammar.Entry.create grammar "tactic" *)
-(* let tactical = Grammar.Entry.create grammar "tactical" *)
+let tactic = Grammar.Entry.create grammar "tactic"
+let tactical = Grammar.Entry.create grammar "tactical"
+let tactical0 = Grammar.Entry.create grammar "tactical0"
 
 let return_term loc term = CicAst.AttributedTerm (`Loc loc, term)
-(* let return_term loc term = term *)
+let return_tactic loc tactic = TacticAst.LocatedTactic (loc, tactic)
+let return_tactical loc tactical = TacticAst.LocatedTactical (loc, tactical)
 
 let fail (x, y) msg =
   failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
@@ -57,7 +59,17 @@ let name_of_string = function
   | s -> Cic.Name s
 
 EXTEND
-  GLOBAL: term term0;
+  GLOBAL: term term0 tactic tactical tactical0;
+  int: [
+    [ num = NUM ->
+        try
+          int_of_string num
+        with Failure _ ->
+          let (x, y) = loc in
+          raise (Parse_error (sprintf
+            "integer literal expected at characters %d-%d" x y))
+    ]
+  ];
   meta_subst: [
     [ s = SYMBOL "_" -> None
     | t = term -> Some t ]
@@ -191,6 +203,92 @@ EXTEND
       | PAREN "("; t = term; PAREN ")" -> return_term loc t
       ]
     ];
+  tactic_where: [
+    [ where = OPT [ "in"; ident = IDENT -> ident ] -> where ]
+  ];
+  tactic_term: [
+    [ t = term -> t ]
+  ];
+  ident_list0: [
+    [ PAREN "["; idents = LIST0 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]
+  ];
+  ident_list1: [
+    [ PAREN "["; idents = LIST1 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]
+  ];
+  reduction_kind: [
+    [ "reduce" -> `Reduce
+    | "simpl" -> `Simpl
+    | "whd" -> `Whd ]
+  ];
+  tactic: [
+    [ IDENT "absurd" -> return_tactic loc TacticAst.Absurd
+    | IDENT "apply"; t = tactic_term -> return_tactic loc (TacticAst.Apply t)
+    | IDENT "assumption" -> return_tactic loc TacticAst.Assumption
+    | IDENT "change"; t1 = tactic_term; "with"; t2 = tactic_term;
+      where = tactic_where ->
+        return_tactic loc (TacticAst.Change (t1, t2, where))
+    (* TODO Change_pattern *)
+    | IDENT "contradiction" -> return_tactic loc TacticAst.Contradiction
+    | IDENT "cut"; t = tactic_term -> return_tactic loc (TacticAst.Cut t)
+    | IDENT "decompose"; principles = ident_list1; where = IDENT ->
+        return_tactic loc (TacticAst.Decompose (where, principles))
+    | IDENT "discriminate"; hyp = IDENT ->
+        return_tactic loc (TacticAst.Discriminate hyp)
+    | IDENT "elim"; IDENT "type"; t = tactic_term ->
+        return_tactic loc (TacticAst.ElimType t)
+    | IDENT "elim"; t1 = tactic_term;
+      using = OPT [ IDENT "using"; using = tactic_term -> using ] ->
+        return_tactic loc (TacticAst.Elim (t1, using))
+    | IDENT "exact"; t = tactic_term -> return_tactic loc (TacticAst.Exact t)
+    | IDENT "exists" -> return_tactic loc TacticAst.Exists
+    | IDENT "fold"; kind = reduction_kind; t = tactic_term ->
+        return_tactic loc (TacticAst.Fold (kind, t))
+    | IDENT "fourier" -> return_tactic loc TacticAst.Fourier
+    | IDENT "injection"; ident = IDENT ->
+        return_tactic loc (TacticAst.Injection ident)
+    | IDENT "intros";
+      num = OPT [ num = int -> num ];
+      idents = OPT ident_list0 ->
+        let idents = match idents with None -> [] | Some idents -> idents in
+        return_tactic loc (TacticAst.Intros (num, idents))
+    | IDENT "left" -> return_tactic loc TacticAst.Left
+    | "let"; t = tactic_term; IDENT "in"; where = IDENT ->
+        return_tactic loc (TacticAst.LetIn (t, where))
+    (* TODO Reduce *)
+    | IDENT "reflexivity" -> return_tactic loc TacticAst.Reflexivity
+    | IDENT "replace"; t1 = tactic_term; "with"; t2 = tactic_term ->
+        return_tactic loc (TacticAst.Replace (t1, t2))
+    (* TODO Rewrite *)
+    (* TODO Replace_pattern *)
+    | IDENT "right" -> return_tactic loc TacticAst.Right
+    | IDENT "ring" -> return_tactic loc TacticAst.Ring
+    | IDENT "split" -> return_tactic loc TacticAst.Split
+    | IDENT "symmetry" -> return_tactic loc TacticAst.Symmetry
+    | IDENT "transitivity"; t = tactic_term ->
+        return_tactic loc (TacticAst.Transitivity t)
+    ]
+  ];
+  tactical0 : [ [ t = tactical; SYMBOL "." -> t ] ];
+  tactical: [
+    [ IDENT "fail" -> return_tactical loc TacticAst.Fail
+    | IDENT "do"; count = int; tac = tactical ->
+        return_tactical loc (TacticAst.Do (count, tac))
+    | IDENT "id" -> return_tactical loc TacticAst.IdTac
+    | IDENT "repeat"; tac = tactical ->
+        return_tactical loc (TacticAst.Repeat tac)
+    | tactics = LIST0 tactical SEP SYMBOL ";" ->
+        return_tactical loc (TacticAst.Seq tactics)
+    | tac = tactical;
+      PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
+        return_tactical loc (TacticAst.Then (tac, tacs))
+    | IDENT "tries";
+      PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
+        return_tactical loc (TacticAst.Tries tacs)
+    | IDENT "try"; tac = tactical -> return_tactical loc (TacticAst.Try tac)
+    | tac = tactic -> return_tactical loc (TacticAst.Tactic tac)
+    | PAREN "("; tac = tactical; PAREN ")" -> return_tactical loc tac
+    ]
+  ];
 END
 
 let parse_term stream =
@@ -200,6 +298,20 @@ let parse_term stream =
     raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
         (Printexc.to_string exn)))
 
+let parse_tactic stream =
+  try
+    Grammar.Entry.parse tactic stream
+  with Stdpp.Exc_located ((x, y), exn) ->
+    raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
+        (Printexc.to_string exn)))
+
+let parse_tactical stream =
+  try
+    Grammar.Entry.parse tactical0 stream
+  with Stdpp.Exc_located ((x, y), exn) ->
+    raise (Parse_error (sprintf "parse error at characters %d-%d: %s" x y
+        (Printexc.to_string exn)))
+
 (**/**)
 
 (** {2 Interface for gTopLevel} *)

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli
index 7e0625cc361567c3c7bf7f9d0226b749bc776702..a6f8dcce310bd8c30f2f96609d7254a1d4674342 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli
@@ -28,6 +28,10 @@ exception Parse_error of string
 (** {2 Parsing functions} *)
 
 val parse_term: char Stream.t -> CicAst.term
+val parse_tactic: char Stream.t -> (CicAst.term, string) TacticAst.tactic
+val parse_tactical:
+  char Stream.t ->
+    (CicAst.term, string) TacticAst.tactic TacticAst.tactical
 
 (** {2 Grammar extensions} *)
 

diff --git a/helm/ocaml/cic_disambiguation/test_parser.ml b/helm/ocaml/cic_disambiguation/test_parser.ml
index 911e278ecb43c49e728e25465a62994089e7dfc9..ff4ae9726e41bac09d7dad80d831d92d54e1d6bd 100644 (file)
--- a/helm/ocaml/cic_disambiguation/test_parser.ml
+++ b/helm/ocaml/cic_disambiguation/test_parser.ml
@@ -23,34 +23,48 @@
  * http://helm.cs.unibo.it/
  *)
 
-let mode = ref `Term
+let default_mode = `Term
+
+let mode = ref default_mode
 
 let _ =
   try
     match Sys.argv.(1) with
     | "alias" -> mode := `Alias
     | "term" -> mode := `Term
-    | _ -> ()
+    | "tactic" -> mode := `Tactic
+    | "tactical" -> mode := `Tactical
+    | _ ->
+        prerr_endline "What???????";
+        exit 1
   with Invalid_argument _ -> ()
 
 let _ =
+  let ic = stdin in
   try
-    let ic = stdin in
-    (match !mode with
-    | `Term ->
-        let term = CicTextualParser2.parse_term (Stream.of_channel ic) in
-        close_in ic;
-(*         print_endline (CicAstPp.pp_term term) *)
-        print_endline (BoxPp.pp_term term)
-    | `Alias ->
-        while true do
-          let line = input_line ic in
-          let env = CicTextualParser2.EnvironmentP3.of_string line in
-          print_endline (CicTextualParser2.EnvironmentP3.to_string env)
-        done)
-  with
-  | End_of_file -> ()
-  | Stdpp.Exc_located ((p_start, p_end), exn) ->
-    prerr_endline (Printf.sprintf "Exception at character %d-%d: %s"
-      p_start p_end (Printexc.to_string exn))
+    while true do
+      try
+        let line = input_line ic in
+        let istream = Stream.of_string line in
+        (match !mode with
+        | `Term ->
+            let term = CicTextualParser2.parse_term istream in
+            print_endline (BoxPp.pp_term term)
+        | `Tactic ->
+            let term = CicTextualParser2.parse_tactic istream in
+            print_endline (TacticAstPp.pp_tactic term)
+        | `Tactical ->
+            let term = CicTextualParser2.parse_tactical istream in
+            print_endline (TacticAstPp.pp_tactical term)
+        | `Alias ->
+            let env = CicTextualParser2.EnvironmentP3.of_string line in
+            print_endline (CicTextualParser2.EnvironmentP3.to_string env));
+        flush stdout
+      with
+      | Stdpp.Exc_located ((p_start, p_end), exn) ->
+        prerr_endline (Printf.sprintf "Exception at character %d-%d: %s"
+          p_start p_end (Printexc.to_string exn))
+    done
+  with End_of_file ->
+    close_in ic