Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 194 insertions, 0 deletions

diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll
new file mode 100644
index 00000000..03ce950f
--- /dev/null
+++ b/ide/coq_lex.mll
@@ -0,0 +1,194 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+{
+  open Lexing
+
+  type token =
+    | Comment
+    | Keyword
+    | Declaration
+    | ProofDeclaration
+    | Qed
+    | String
+
+  (* Without this table, the automaton would be too big and
+     ocamllex would fail *)
+  let is_one_word_command =
+    let h = Hashtbl.create 97 in
+    List.iter (fun s -> Hashtbl.add h s ())
+      [  "Add" ; "Check"; "Eval"; "Extraction" ;
+	 "Load" ; "Undo"; "Goal";
+	 "Proof" ; "Print";"Save" ;
+	 "End" ; "Section"; "Chapter"; "Transparent"; "Opaque"; "Comments"
+      ];
+    Hashtbl.mem h
+
+  let is_constr_kw =
+    let h = Hashtbl.create 97 in
+      List.iter (fun s -> Hashtbl.add h s ())
+	[ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "for";
+	  "end"; "as"; "let"; "in"; "if"; "then"; "else"; "return";
+	  "Prop"; "Set"; "Type" ];
+      Hashtbl.mem h
+
+  (* Without this table, the automaton would be too big and
+     ocamllex would fail *)
+  let is_one_word_declaration =
+    let h = Hashtbl.create 97 in
+      List.iter (fun s -> Hashtbl.add h s ())
+	[ (* Definitions *)
+	  "Definition" ; "Let" ; "Example" ; "SubClass" ;
+          "Fixpoint" ; "CoFixpoint" ; "Scheme" ; "Function" ;
+          (* Assumptions *)
+	  "Hypothesis" ; "Variable" ; "Axiom" ; "Parameter" ; "Conjecture" ;
+	  "Hypotheses" ; "Variables" ; "Axioms" ; "Parameters";
+          (* Inductive *)
+          "Inductive" ; "CoInductive" ; "Record" ; "Structure" ;
+          (* Other *)
+	  "Ltac" ; "Typeclasses"; "Instance"; "Include"; "Context"; "Class"
+	];
+      Hashtbl.mem h
+
+  let is_proof_declaration =
+    let h = Hashtbl.create 97 in
+    List.iter (fun s -> Hashtbl.add h s ())
+      [ "Theorem" ; "Lemma" ; " Fact" ; "Remark" ; "Corollary" ;
+        "Proposition" ; "Property" ];
+    Hashtbl.mem h
+
+  let is_proof_end =
+    let h = Hashtbl.create 97 in
+    List.iter (fun s -> Hashtbl.add h s ())
+      [ "Qed" ; "Defined" ; "Admitted" ];
+    Hashtbl.mem h
+
+  let start = ref true
+}
+
+let space =
+  [' ' '\010' '\013' '\009' '\012']
+
+let firstchar =
+  ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255']
+let identchar =
+  ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
+let ident = firstchar identchar*
+
+let sentence_sep = '.' [ ' ' '\n' '\t' ]
+
+let multiword_declaration =
+  "Module" (space+ "Type")?
+| "Program" space+ ident
+| "Existing" space+ "Instance"
+| "Canonical" space+ "Structure"
+
+let locality = ("Local" space+)?
+
+let multiword_command =
+  "Set" (space+ ident)*
+| "Unset" (space+ ident)*
+| "Open" space+ locality "Scope"
+| "Close" space+ locality "Scope"
+| "Bind" space+ "Scope"
+| "Arguments" space+ "Scope"
+| "Reserved" space+ "Notation" space+ locality
+| "Delimit" space+ "Scope"
+| "Next" space+ "Obligation"
+| "Solve" space+ "Obligations"
+| "Require" space+ ("Import"|"Export")?
+| "Infix" space+ locality
+| "Notation" space+ locality
+| "Hint" space+ locality ident
+| "Reset" (space+ "Initial")?
+| "Tactic" space+ "Notation"
+| "Implicit" space+ "Arguments"
+| "Implicit" space+ ("Type"|"Types")
+| "Combined" space+ "Scheme"
+| "Extraction" space+ (("Language" space+ ("Ocaml"|"Haskell"|"Scheme"|"Toplevel"))|
+    ("Library"|"Inline"|"NoInline"|"Blacklist"))
+| "Recursive" space+ "Extraction" (space+ "Library")?
+| ("Print"|"Reset") space+ "Extraction" space+ ("Inline"|"Blacklist")
+| "Extract" space+ (("Inlined" space+) "Constant"| "Inductive")
+
+(* At least still missing: "Inline" + decl, variants of "Identity
+  Coercion", variants of Print, Add, ... *)
+
+rule coq_string = parse
+  | "\"\"" { coq_string lexbuf }
+  | "\"" { Lexing.lexeme_end lexbuf }
+  | eof { Lexing.lexeme_end lexbuf }
+  | _ { coq_string lexbuf }
+
+and comment = parse
+  | "(*" { ignore (comment lexbuf); comment lexbuf }
+  | "\"" { ignore (coq_string lexbuf); comment lexbuf }
+  | "*)" { Lexing.lexeme_end lexbuf }
+  | eof { Lexing.lexeme_end lexbuf }
+  | _ { comment lexbuf }
+
+and sentence stamp = parse
+  | space+ { sentence stamp lexbuf }
+  | "(*" {
+      let comm_start = Lexing.lexeme_start lexbuf in
+      let comm_end = comment lexbuf in
+      stamp comm_start comm_end Comment;
+      sentence stamp lexbuf
+    }
+  | "\"" {
+      let str_start = Lexing.lexeme_start lexbuf in
+      let str_end = coq_string lexbuf in
+      stamp str_start str_end String;
+      start := false;
+      sentence stamp lexbuf
+    }
+  | multiword_declaration {
+      if !start then begin
+        start := false;
+        stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Declaration
+      end;
+      sentence stamp lexbuf
+    }
+  | multiword_command {
+      if !start then begin
+        start := false;
+        stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Keyword
+      end;
+      sentence stamp lexbuf }
+  | ident as id {
+      if !start then begin
+        start := false;
+        if id <> "Time" then begin
+            if is_proof_end id then
+              stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Qed
+            else if is_one_word_command id then
+              stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Keyword
+            else if is_one_word_declaration id then
+              stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Declaration
+            else if is_proof_declaration id then
+              stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) ProofDeclaration
+        end
+      end else begin
+        if is_constr_kw id then
+	  stamp (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf) Keyword
+      end;
+      sentence stamp lexbuf }
+  | ".."
+  | _    { sentence stamp lexbuf}
+  | sentence_sep { }
+  | eof { raise Not_found }
+
+{
+  let find_end_offset stamp slice =
+    let lb = Lexing.from_string slice in
+    start := true;
+    sentence stamp lb;
+    Lexing.lexeme_end lb
+}