From 2383b30bb6efd01f68547113ac5019fb53b44479 Mon Sep 17 00:00:00 2001 From: vgross Date: Fri, 19 Feb 2010 10:28:45 +0000 Subject: Fixing compilation issues git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12798 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/coqLex.mll | 194 -------------------------------------------------------- ide/coq_lex.mll | 194 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 194 insertions(+), 194 deletions(-) delete mode 100644 ide/coqLex.mll create mode 100644 ide/coq_lex.mll diff --git a/ide/coqLex.mll b/ide/coqLex.mll deleted file mode 100644 index 03ce950fdd..0000000000 --- a/ide/coqLex.mll +++ /dev/null @@ -1,194 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* 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 -} diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll new file mode 100644 index 0000000000..03ce950fdd --- /dev/null +++ b/ide/coq_lex.mll @@ -0,0 +1,194 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 +} -- cgit v1.2.3