aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Vincent Laporte <Vincent.Laporte@gmail.com>2018-06-18 16:53:54 +0000
committerGravatar Vincent Laporte <Vincent.Laporte@gmail.com>2018-06-25 16:15:07 +0000
commit6c4062ca13e6fb9e7d2dc93c70b545ccb22575de (patch)
treeca7fff282c7f567488b322a897a379213963b2ff /tools
parent24279abf43cfbd65e2fc29f171eb8705fdf61a3e (diff)
Archive the `gallina` tool
Diffstat (limited to 'tools')
-rw-r--r--tools/CoqMakefile.in9
-rw-r--r--tools/gallina.ml63
-rw-r--r--tools/gallina_lexer.mll126
3 files changed, 0 insertions, 198 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 8e60d3932..b8ce164a6 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -86,7 +86,6 @@ COQC ?= "$(COQBIN)coqc"
COQTOP ?= "$(COQBIN)coqtop"
COQCHK ?= "$(COQBIN)coqchk"
COQDEP ?= "$(COQBIN)coqdep"
-GALLINA ?= "$(COQBIN)gallina"
COQDOC ?= "$(COQBIN)coqdoc"
COQMKFILE ?= "$(COQBIN)coq_makefile"
@@ -256,7 +255,6 @@ VO = vo
VOFILES = $(VFILES:.v=.$(VO))
GLOBFILES = $(VFILES:.v=.glob)
-GFILES = $(VFILES:.v=.g)
HTMLFILES = $(VFILES:.v=.html)
GHTMLFILES = $(VFILES:.v=.g.html)
BEAUTYFILES = $(addsuffix .beautified,$(VFILES))
@@ -442,8 +440,6 @@ all-mli.tex: $(MLIFILES:.mli=.cmi)
$(HIDE)$(CAMLDOC) -latex \
-o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES)
-gallina: $(GFILES)
-
all.ps: $(VFILES)
$(SHOW)'COQDOC -ps $(GAL)'
$(HIDE)$(COQDOC) \
@@ -564,7 +560,6 @@ clean::
$(HIDE)find . -name .coq-native -type d -empty -delete
$(HIDE)rm -f $(VOFILES)
$(HIDE)rm -f $(VOFILES:.vo=.vio)
- $(HIDE)rm -f $(GFILES)
$(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old)
$(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex
$(HIDE)rm -f $(VFILES:.v=.glob)
@@ -683,10 +678,6 @@ $(BEAUTYFILES): %.v.beautified: %.v
$(SHOW)'BEAUTIFY $<'
$(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -beautify $<
-$(GFILES): %.g: %.v
- $(SHOW)'GALLINA $<'
- $(HIDE)$(GALLINA) $<
-
$(TEXFILES): %.tex: %.v
$(SHOW)'COQDOC -latex $<'
$(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
diff --git a/tools/gallina.ml b/tools/gallina.ml
deleted file mode 100644
index c7ff76bec..000000000
--- a/tools/gallina.ml
+++ /dev/null
@@ -1,63 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open Gallina_lexer
-
-let vfiles = ref ([] : string list)
-
-let option_moins = ref false
-
-let option_stdout = ref false
-
-let traite_fichier f =
- try
- let chan_in = open_in (f^".v") in
- let buf = Lexing.from_channel chan_in in
- if not !option_stdout then chan_out := open_out (f ^ ".g");
- try
- while true do Gallina_lexer.action buf done
- with Fin_fichier -> begin
- flush !chan_out;
- close_in chan_in;
- if not !option_stdout then close_out !chan_out
- end
- with Sys_error _ ->
- ()
-
-let traite_stdin () =
- try
- let buf = Lexing.from_channel stdin in
- try
- while true do Gallina_lexer.action buf done
- with Fin_fichier ->
- flush !chan_out
- with Sys_error _ ->
- ()
-
-let _ =
- let lg_command = Array.length Sys.argv in
- if lg_command < 2 then begin
- output_string stderr "Usage: gallina [-] [-stdout] file1 file2 ...\n";
- flush stderr;
- exit 1
- end;
- let treat = function
- | "-" -> option_moins := true
- | "-stdout" -> option_stdout := true
- | "-nocomments" -> comments := false
- | f ->
- if Filename.check_suffix f ".v" then
- vfiles := (Filename.chop_suffix f ".v") :: !vfiles
- in
- Array.iter treat Sys.argv;
- if !option_moins then
- traite_stdin ()
- else
- List.iter traite_fichier !vfiles
diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll
deleted file mode 100644
index 1a594aebb..000000000
--- a/tools/gallina_lexer.mll
+++ /dev/null
@@ -1,126 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-{
-
- let chan_out = ref stdout
-
- let comment_depth = ref 0
- let cRcpt = ref 0
- let comments = ref true
- let print s = output_string !chan_out s
-
- exception Fin_fichier
-
-}
-
-let space = [' ' '\t' '\n' '\r']
-let enddot = '.' (' ' | '\t' | '\n' | '\r' | eof)
-
-rule action = parse
- | "Theorem" space { print "Theorem "; body lexbuf;
- cRcpt := 1; action lexbuf }
- | "Lemma" space { print "Lemma "; body lexbuf;
- cRcpt := 1; action lexbuf }
- | "Fact" space { print "Fact "; body lexbuf;
- cRcpt := 1; action lexbuf }
- | "Remark" space { print "Remark "; body lexbuf;
- cRcpt := 1; action lexbuf }
- | "Goal" space { print "Goal "; body lexbuf;
- cRcpt := 1; action lexbuf }
- | "Correctness" space { print "Correctness "; body_pgm lexbuf;
- cRcpt := 1; action lexbuf }
- | "Definition" space { print "Definition "; body_def lexbuf;
- cRcpt := 1; action lexbuf }
- | "Hint" space { skip_until_point lexbuf ; action lexbuf }
- | "Hints" space { skip_until_point lexbuf ; action lexbuf }
- | "Transparent" space { skip_until_point lexbuf ; action lexbuf }
- | "Immediate" space { skip_until_point lexbuf ; action lexbuf }
- | "Syntax" space { skip_until_point lexbuf ; action lexbuf }
- | "(*" { (if !comments then print "(*");
- comment_depth := 1;
- comment lexbuf;
- cRcpt := 0; action lexbuf }
- | [' ' '\t']* '\n' { if !cRcpt < 2 then print "\n";
- cRcpt := !cRcpt+1; action lexbuf}
- | eof { (raise Fin_fichier : unit)}
- | _ { print (Lexing.lexeme lexbuf); cRcpt := 0; action lexbuf }
-
-and comment = parse
- | "(*" { (if !comments then print "(*");
- comment_depth := succ !comment_depth; comment lexbuf }
- | "*)" { (if !comments then print "*)");
- comment_depth := pred !comment_depth;
- if !comment_depth > 0 then comment lexbuf }
- | "*)" [' ''\t']*'\n' { (if !comments then print (Lexing.lexeme lexbuf));
- comment_depth := pred !comment_depth;
- if !comment_depth > 0 then comment lexbuf }
- | eof { raise Fin_fichier }
- | _ { (if !comments then print (Lexing.lexeme lexbuf));
- comment lexbuf }
-
-and skip_comment = parse
- | "(*" { comment_depth := succ !comment_depth; skip_comment lexbuf }
- | "*)" { comment_depth := pred !comment_depth;
- if !comment_depth > 0 then skip_comment lexbuf }
- | eof { raise Fin_fichier }
- | _ { skip_comment lexbuf }
-
-and body_def = parse
- | [^'.']* ":=" { print (Lexing.lexeme lexbuf); () }
- | _ { print (Lexing.lexeme lexbuf); body lexbuf }
-
-and body = parse
- | enddot { print ".\n"; skip_proof lexbuf }
- | ":=" { print ".\n"; skip_proof lexbuf }
- | "(*" { print "(*"; comment_depth := 1;
- comment lexbuf; body lexbuf }
- | eof { raise Fin_fichier }
- | _ { print (Lexing.lexeme lexbuf); body lexbuf }
-
-and body_pgm = parse
- | enddot { print ".\n"; skip_proof lexbuf }
- | "(*" { print "(*"; comment_depth := 1;
- comment lexbuf; body_pgm lexbuf }
- | eof { raise Fin_fichier }
- | _ { print (Lexing.lexeme lexbuf); body_pgm lexbuf }
-
-and skip_until_point = parse
- | '.' '\n' { () }
- | enddot { end_of_line lexbuf }
- | "(*" { comment_depth := 1;
- skip_comment lexbuf; skip_until_point lexbuf }
- | eof { raise Fin_fichier }
- | _ { skip_until_point lexbuf }
-
-and end_of_line = parse
- | [' ' '\t' ]* { end_of_line lexbuf }
- | '\n' { () }
- | eof { raise Fin_fichier }
- | _ { print (Lexing.lexeme lexbuf) }
-
-and skip_proof = parse
- | "Save" space
- { skip_until_point lexbuf }
- | "Qed." { end_of_line lexbuf }
- | "Qed" space
- { skip_until_point lexbuf }
- | "Defined." { end_of_line lexbuf }
- | "Defined" space
- { skip_until_point lexbuf }
- | "Abort." { end_of_line lexbuf }
- | "Abort" space
- { skip_until_point lexbuf }
- | "Proof" space { skip_until_point lexbuf }
- | "Proof" [' ' '\t']* '.' { skip_proof lexbuf }
- | "(*" { comment_depth := 1;
- skip_comment lexbuf; skip_proof lexbuf }
- | eof { raise Fin_fichier }
- | _ { skip_proof lexbuf }