added support for commands and scripts

diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
index 71574dbb1ce081e24da3455739cedba56f70ba76..22c911eaf5b543e16bb7b1a35d21b3a758eee43c 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml
@@ -51,7 +51,7 @@ let regexp uri =
 let keywords = Hashtbl.create 17
 let _ =
   List.iter (fun keyword -> Hashtbl.add keywords keyword ("", keyword))
-    [ "Prop"; "Type"; "Set"; "let"; "rec"; "using"; "match"; "with" ]
+    [ "Prop"; "Type"; "Set"; "let"; "Let"; "rec"; "using"; "match"; "with" ]
 
 let error lexbuf msg =
   raise (Error (Ulexing.lexeme_start lexbuf, Ulexing.lexeme_end lexbuf, msg))

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 7c0dfc1c6ab31c04a36d7f6ed8189d3cc09fbfa6..2474191fe4f0c9f866b40e8949f40e504e0fd91f 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -35,6 +35,11 @@ open Printf
 
 exception Parse_error of string
 
+type tactic = (CicAst.term, string) TacticAst.tactic
+type tactical = (CicAst.term, string) TacticAst.tactic TacticAst.tactical
+type command = CicAst.term CommandAst.command
+type script = CicAst.term CommandAst.Script.script
+
 let choice_of_uri (uri: string) =
   let cic = HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri) in
   (uri, (fun _ _ _ -> cic))
@@ -46,10 +51,14 @@ let term0 = Grammar.Entry.create grammar "term0"
 let tactic = Grammar.Entry.create grammar "tactic"
 let tactical = Grammar.Entry.create grammar "tactical"
 let tactical0 = Grammar.Entry.create grammar "tactical0"
+let command = Grammar.Entry.create grammar "command"
+let script = Grammar.Entry.create grammar "script"
 
 let return_term loc term = CicAst.AttributedTerm (`Loc loc, term)
 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 return_script loc script = script
 
 let fail (x, y) msg =
   failwith (Printf.sprintf "Error at characters %d - %d: %s" x y msg)
@@ -59,7 +68,7 @@ let name_of_string = function
   | s -> Cic.Name s
 
 EXTEND
-  GLOBAL: term term0 tactic tactical tactical0;
+  GLOBAL: term term0 tactic tactical tactical0 command script;
   int: [
     [ num = NUM ->
         try
@@ -219,54 +228,72 @@ EXTEND
     | "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;
+    [ [ IDENT "absurd" | IDENT "Absurd" ] -> return_tactic loc TacticAst.Absurd
+    | [ 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" ];
+      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 ->
+    | [ IDENT "contradiction" | IDENT "Contradiction" ] ->
+        return_tactic loc TacticAst.Contradiction
+    | [ IDENT "cut" | IDENT "Cut" ];
+      t = tactic_term -> return_tactic loc (TacticAst.Cut t)
+    | [ IDENT "decompose" | IDENT "Decompose" ];
+      principles = ident_list1; where = IDENT ->
         return_tactic loc (TacticAst.Decompose (where, principles))
-    | IDENT "discriminate"; hyp = IDENT ->
+    | [ IDENT "discriminate" | IDENT "Discriminate" ];
+      hyp = IDENT ->
         return_tactic loc (TacticAst.Discriminate hyp)
-    | IDENT "elim"; IDENT "type"; t = tactic_term ->
+    | [ IDENT "elim" | IDENT "Elim" ]; IDENT "type";
+      t = tactic_term ->
         return_tactic loc (TacticAst.ElimType t)
-    | IDENT "elim"; t1 = tactic_term;
+    | [ IDENT "elim" | IDENT "Elim" ];
+      t1 = tactic_term;
       using = OPT [ "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 ->
+    | [ IDENT "exact" | IDENT "Exact" ]; t = tactic_term ->
+        return_tactic loc (TacticAst.Exact t)
+    | [ IDENT "exists" | IDENT "Exists" ] ->
+        return_tactic loc TacticAst.Exists
+    | [ IDENT "fold" | 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 ->
+    | [ IDENT "fourier" | IDENT "Fourier" ] ->
+        return_tactic loc TacticAst.Fourier
+    | [ IDENT "injection" | IDENT "Injection" ]; ident = IDENT ->
         return_tactic loc (TacticAst.Injection ident)
-    | IDENT "intros";
+    | [ IDENT "intros" | 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 ->
+    | [ IDENT "left" | IDENT "Left" ] -> return_tactic loc TacticAst.Left
+    | [ "let" | "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 ->
+    | [ IDENT "reflexivity" | IDENT "Reflexivity" ] ->
+        return_tactic loc TacticAst.Reflexivity
+    | [ IDENT "replace" | 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 ->
+    | [ IDENT "right" | IDENT "Right" ] -> return_tactic loc TacticAst.Right
+    | [ IDENT "ring" | IDENT "Ring" ] -> return_tactic loc TacticAst.Ring
+    | [ IDENT "split" | IDENT "Split" ] -> return_tactic loc TacticAst.Split
+    | [ IDENT "symmetry" | IDENT "Symmetry" ] ->
+        return_tactic loc TacticAst.Symmetry
+    | [ IDENT "transitivity" | IDENT "Transitivity" ];
+      t = tactic_term ->
         return_tactic loc (TacticAst.Transitivity t)
     ]
   ];
-  tactical0 : [ [ t = tactical; SYMBOL "." -> t ] ];
+  tactical0: [ [ t = tactical; SYMBOL "." -> t ] ];
   tactical:
     [ "sequence" LEFTA
       [ tactics = LIST1 NEXT SEP SYMBOL ";" ->
@@ -278,44 +305,115 @@ EXTEND
           return_tactical loc (TacticAst.Then (tac, tacs))
       ]
     | "loops" RIGHTA
-      [ IDENT "do"; count = int; tac = tactical ->
+      [ [ IDENT "do" | IDENT "Do" ]; count = int; tac = tactical ->
           return_tactical loc (TacticAst.Do (count, tac))
-      | IDENT "repeat"; tac = tactical ->
+      | [ IDENT "repeat" | IDENT "Repeat" ]; tac = tactical ->
           return_tactical loc (TacticAst.Repeat tac)
       ]
     | "simple" NONA
-      [ IDENT "tries";
+      [ [ IDENT "tries" | IDENT "Tries" ];
         PAREN "["; tacs = LIST0 tactical SEP SYMBOL ";"; PAREN "]" ->
           return_tactical loc (TacticAst.Tries tacs)
-      | IDENT "try"; tac = NEXT -> return_tactical loc (TacticAst.Try tac)
-      | IDENT "fail" -> return_tactical loc TacticAst.Fail
-      | IDENT "id" -> return_tactical loc TacticAst.IdTac
+      | [ IDENT "try" | IDENT "Try" ]; tac = NEXT ->
+          return_tactical loc (TacticAst.Try tac)
+      | [ IDENT "fail" | IDENT "Fail" ] -> return_tactical loc TacticAst.Fail
+      | [ 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)
       ]
     ];
+  theorem_flavour: [  (* all flavours but Goal *)
+    [ [ IDENT "definition"  | IDENT "Definition"  ] -> `Definition
+    | [ IDENT "fact"        | IDENT "Fact"        ] -> `Fact
+    | [ IDENT "lemma"       | IDENT "Lemma"       ] -> `Lemma
+    | [ IDENT "remark"      | IDENT "Remark"      ] -> `Remark
+    | [ IDENT "theorem"     | IDENT "Theorem"     ] -> `Theorem
+(*     | [ IDENT "goal"        | IDENT "Goal"        ] -> `Goal *)
+    ]
+  ];
+  theorem_cmd: [
+    [ flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term;
+      body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ];
+      SYMBOL "." ->
+        (loc, flavour, name, typ, body)
+    | [ IDENT "goal" | IDENT "Goal" ]; typ = term;
+      body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ];
+      SYMBOL "." ->
+        (loc, `Goal, None, typ, body)
+    ]
+  ];
+  proof_cmd: [ [ [ IDENT "proof" | IDENT "Proof" ]; SYMBOL "." -> loc ] ];
+  qed_cmd: [
+    [ [ IDENT "qed" | IDENT "Qed" ]; SYMBOL "." -> (loc, None)
+    | [ IDENT "save" | IDENT "Save" ]; name = IDENT; SYMBOL "." ->
+        (loc, Some name)
+    ]
+  ];
+  command: [
+    [ (loc', flavour, name, typ, body) = theorem_cmd ->
+        return_command loc (CommandAst.Theorem (loc', flavour, name, typ, body))
+    | (loc') = proof_cmd -> return_command loc (CommandAst.Proof loc')
+    | (loc, name) = qed_cmd -> return_command loc (CommandAst.Qed (loc, name))
+    ]
+  ];
+  script_entry: [
+    [ theorem = theorem_cmd;
+      proof = OPT [
+        proof_cmd; tacticals = LIST1 tactical0; qed = qed_cmd ->
+          (tacticals, qed)
+      ] ->
+        let (loc', flavour, name', typ, body_verbatim) = theorem in
+        let name'' =
+          match proof with
+          | None | Some (_, (_, None)) -> None
+          | Some (_, (_, Some name)) -> Some name
+        in
+        let name =
+          match (name', name'') with
+          | Some name, None -> name
+          | None, Some name -> name
+          | None, None ->
+              Stdpp.raise_with_loc loc (Failure "theorem's name is missing")
+          | Some name', Some name'' when name' <> name'' ->
+              Stdpp.raise_with_loc loc (Failure (sprintf
+                "theorem's name mismatch: %s <> %s" name' name''))
+          | Some name, _ -> name
+        in
+        let body =
+          match (body_verbatim, proof) with
+          | Some term, None -> CommandAst.Script.Verbatim (loc', term)
+          | None, Some (tacticals, (loc'', _)) ->
+              CommandAst.Script.Tactics (loc'', tacticals)
+          | Some _, Some _ ->
+              Stdpp.raise_with_loc loc (Failure (sprintf
+                "theorem %s has too many proofs" name))
+          | None, None ->
+              Stdpp.raise_with_loc loc (Failure (sprintf
+                "theorem %s has no proof" name))
+        in
+        return_script loc (CommandAst.Script.Theorem (flavour, name, typ, body))
+    ]
+  ];
+  script: [ [ entries = LIST0 script_entry; EOI -> entries ] ];
 END
 
-let parse_term stream =
+let exc_located_wrapper f =
   try
-    Grammar.Entry.parse term0 stream
+    Lazy.force f
   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_term stream =
+  exc_located_wrapper (lazy (Grammar.Entry.parse term0 stream))
 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)))
-
+  exc_located_wrapper (lazy (Grammar.Entry.parse tactic stream))
 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)))
+  exc_located_wrapper (lazy (Grammar.Entry.parse tactical0 stream))
+let parse_command stream =
+  exc_located_wrapper (lazy (Grammar.Entry.parse command stream))
+let parse_script stream =
+  exc_located_wrapper (lazy (Grammar.Entry.parse script stream))
 
 (**/**)
 
@@ -390,3 +488,4 @@ module EnvironmentP3 =
           (Printexc.to_string exn)))
   end
 
+(* vim:set encoding=utf8: *)

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli
index a6f8dcce310bd8c30f2f96609d7254a1d4674342..e867d3435c500cfc620bda538c88f0bc8a44b016 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.mli
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.mli
@@ -25,13 +25,20 @@
 
 exception Parse_error of string
 
+(** {3 type shortands} *)
+
+type tactic = (CicAst.term, string) TacticAst.tactic
+type tactical = (CicAst.term, string) TacticAst.tactic TacticAst.tactical
+type command = CicAst.term CommandAst.command
+type script = CicAst.term CommandAst.Script.script
+
 (** {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
+val parse_term:     char Stream.t -> CicAst.term
+val parse_tactic:   char Stream.t -> tactic
+val parse_tactical: char Stream.t -> tactical
+val parse_command:  char Stream.t -> command
+val parse_script:   char Stream.t -> script
 
 (** {2 Grammar extensions} *)
 

diff --git a/helm/ocaml/cic_disambiguation/test_parser.ml b/helm/ocaml/cic_disambiguation/test_parser.ml
index d6afddc670607b1099de6e7384f3bb9f28744458..dde96955506853815b0f4bebe7f0a29a8f428233 100644 (file)
--- a/helm/ocaml/cic_disambiguation/test_parser.ml
+++ b/helm/ocaml/cic_disambiguation/test_parser.ml
@@ -30,7 +30,8 @@ let mode = ref default_mode
 (* let pp_tactical = TacticAstPp.pp_tactical *)
 
 let pp_tactical = TacticAst2Box.tacticalPp
-
+let pp_command = CommandAst.pp_command
+let pp_script = CommandAst.pp_script
 
 let _ =
   try
@@ -39,6 +40,8 @@ let _ =
     | "term" -> mode := `Term
     | "tactic" -> mode := `Tactic
     | "tactical" -> mode := `Tactical
+    | "command" -> mode := `Command
+    | "script" -> mode := `Script
     | _ ->
         prerr_endline "What???????";
         exit 1
@@ -47,32 +50,40 @@ let _ =
 let _ =
   let ic = stdin in
   try
-    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 (pp_tactical term)
-        | `Alias ->
-            let env = CicTextualParser2.EnvironmentP3.of_string line in
-            print_endline (CicTextualParser2.EnvironmentP3.to_string env));
-        flush stdout
-      with
-      | CicTextualParser2.Parse_error msg -> prerr_endline msg
-(*
-      | 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
+    if !mode =  `Script then begin
+      let script = CicTextualParser2.parse_script (Stream.of_channel ic) in
+      print_endline (pp_script script)
+    end else
+      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 tac = CicTextualParser2.parse_tactic istream in
+              print_endline (TacticAstPp.pp_tactic tac)
+          | `Tactical ->
+              let tac = CicTextualParser2.parse_tactical istream in
+              print_endline (pp_tactical tac)
+          | `Command ->
+              let cmd = CicTextualParser2.parse_command istream in
+              print_endline (pp_command cmd)
+          | `Script -> assert false (* catched above *)
+          | `Alias ->
+              let env = CicTextualParser2.EnvironmentP3.of_string line in
+              print_endline (CicTextualParser2.EnvironmentP3.to_string env));
+          flush stdout
+        with
+        | CicTextualParser2.Parse_error msg -> prerr_endline msg
+  (*
+        | 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