Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

6 files changed, 466 insertions, 0 deletions

diff --git a/dev/tools/Makefile.common b/dev/tools/Makefile.common
new file mode 100644
index 00000000..1ff5cf79
--- /dev/null
+++ b/dev/tools/Makefile.common
@@ -0,0 +1,52 @@
+# this Makefile contains goals common for directory and main devel makefiles
+
+ifndef TOPDIR
+TOPDIR=..
+endif
+
+ifndef BASEDIR
+BASEDIR=
+endif
+
+# the following entries are used to make synchronize two source trees
+# (on big computer and on a laptop for example)
+
+OTHER_FILE=$(TOPDIR)/dev/other
+OTHER=$(shell cat $(OTHER_FILE))
+
+# this is a directory of useful temporary things
+WORKDIR=tmp
+
+ifneq (,$(findstring n,$(MAKEFLAGS)))
+NFLAG=-n
+else
+NFLAG=
+endif
+
+check_other:
+	+@(if [ "$(OTHER)" = "" ] ; then \
+	  echo You must put the ssh path to the other Coq source in $(OTHER_FILE) ; \
+	  echo For example: chrzaszc@ruta:coq/V7 ; \
+	  exit 1; \
+	fi)
+
+get:	check_other
+	+rsync -Cauvz $(NFLAG) $(OTHER)/ $(TOPDIR)/
+	+@(if [ -d $(TOPDIR)/$(WORKDIR) ]; then \
+	  rsync -auvz $(NFLAG) $(OTHER)/tmp/ $(TOPDIR)/tmp/ ; \
+	fi)
+
+put:	check_other
+	+rsync -Cauvz $(NFLAG) $(TOPDIR)/ $(OTHER)/
+	+@(if [ -d $(TOPDIR)/$(WORKDIR) ]; then \
+	  rsync -auvz $(NFLAG) $(TOPDIR)/tmp/ $(OTHER)/tmp/ ; \
+	fi)
+
+sync:	get put
+
+
+conflicts:
+	cvs status | grep File | grep conflicts | less
+
+confl:	conflicts
+
diff --git a/dev/tools/Makefile.devel b/dev/tools/Makefile.devel
new file mode 100644
index 00000000..f3abb62d
--- /dev/null
+++ b/dev/tools/Makefile.devel
@@ -0,0 +1,74 @@
+# to be linked to makefile (lowercase - takes precedence over Makefile)
+# in main directory
+# make devel in main directory should do this for you.
+
+TOPDIR=.
+BASEDIR=
+
+SOURCEDIRS=lib kernel library pretyping parsing proofs tactics toplevel
+
+default:	usage noargument
+
+usage::
+	@echo Usage: make \<target\>
+	@echo Targets are:
+
+usage::
+	@echo "  setup-devel	-- set the devel makefile"
+setup-devel:
+	@ln -sfv dev/Makefile.devel makefile
+	@(for i in $(SOURCEDIRS); do \
+	    (cd $(TOPDIR)/$$i; ln -sfv ../dev/Makefile.dir Makefile) \
+	done)
+
+
+usage::
+	@echo "  clean-devel	-- clear all devel files"
+clean-devel:
+	echo rm -f makefile .depend.devel
+	echo rm -f $(foreach dir,$(SOURCEDIRS), $(TOPDIR)/$(dir)/Makefile)
+
+
+usage::
+	@echo "  coqtop	-- make until the bytecode executable, make the link"
+coqtop:	bin/coqtop.byte
+	ln -sf bin/coqtop.byte coqtop
+
+
+usage::
+	@echo "  quick		-- make bytecode executable and states"
+quick: 
+	$(MAKE) states BEST=byte
+
+include Makefile
+
+include $(TOPDIR)/dev/Makefile.common
+
+# this file is better described in dev/Makefile.dir
+include .depend.devel
+
+#if dev/Makefile.local exists, it is included
+ifneq ($(wildcard $(TOPDIR)/dev/Makefile.local),)
+include $(TOPDIR)/dev/Makefile.local
+endif
+
+
+usage::
+	@echo "  total		-- runs coqtop with all theories required"
+total:
+	ledit ./bin/coqtop.byte $(foreach th,$(THEORIESVO),-require $(notdir $(basename $(th))))
+
+
+usage::
+	@echo "  run		-- makes and runs bytecode coqtop using ledit and the history file"
+	@echo "		   if you want to pass arguments to coqtop, use make run ARG=<args>"
+run:	$(TOPDIR)/coqtop
+	ledit -h $(TOPDIR)/dev/debug_history -x $(TOPDIR)/coqtop $(ARG) $(ARGS)
+
+
+usage::
+	@echo "  vars		-- echos commands to set COQTOP and COQBIN variables"
+vars:
+	@(cd $(TOPDIR); \
+	echo export COQTOP=`pwd`/ ; \
+	echo export COQBIN=`pwd`/bin/ )
\ No newline at end of file
diff --git a/dev/tools/Makefile.dir b/dev/tools/Makefile.dir
new file mode 100644
index 00000000..68c917ac
--- /dev/null
+++ b/dev/tools/Makefile.dir
@@ -0,0 +1,131 @@
+# make a link to this file if you are working hard in one directory of Coq
+#   ln -s ../dev/Makefile.dir Makefile
+# if you are working in a sub/dir/ make a link to dev/Makefile.subdir instead
+# this Makefile provides many useful facilities to develop Coq
+# it is not completely compatible with .ml4 files unfortunately
+
+ifndef TOPDIR
+TOPDIR=..
+endif
+
+# this complicated thing should work for subsubdirs as well
+BASEDIR=$(shell (dir=`pwd`; cd $(TOPDIR); top=`pwd`; echo $$dir | sed -e "s|$$top/||"))
+
+noargs:	dir
+
+test-dir:
+	@echo TOPDIR=$(TOPDIR)
+	@echo BASEDIR=$(BASEDIR)
+
+include $(TOPDIR)/dev/tools/Makefile.common
+
+# make this directory
+dir:
+	$(MAKE) -C $(TOPDIR) $(notdir $(BASEDIR))
+
+# make all cmo's in this directory. Useful in case the main Makefile is not
+# up-to-date
+all:	
+	@( ( for i in *.ml; do \
+	       echo -n $(BASEDIR)/`basename $$i .ml`.cmo "" ; \
+	     done; \
+	     for i in *.ml4; do \
+	       echo -n $(BASEDIR)/`basename $$i .ml4`.cmo "" ; \
+	     done ) \
+	  | xargs $(MAKE) -C $(TOPDIR) )
+
+# lists all files that should be compiled in this directory
+list:
+	@(for i in *.mli; do \
+	   ls -l `basename $$i .mli`.cmi; \
+	done)
+	@(for i in *.ml; do \
+	   ls -l `basename $$i .ml`.cmo; \
+	done)
+	@(for i in *.ml4; do \
+	   ls -l `basename $$i .ml4`.cmo; \
+	done)
+
+
+clean::  
+	rm -f *.cmi *.cmo *.cmx *.o
+
+
+# if grammar.cmo files cannot be compiled and main .depend cannot be
+# rebuilt, this is quite useful
+depend:
+	(cd $(TOPDIR); ocamldep -I $(BASEDIR) $(BASEDIR)/*.ml $(BASEDIR)/*.mli > .depend.devel)
+
+
+# displays the dependency graph of the current directory (vertically,
+# unlike in doc/)
+graph:
+	(ocamldep *.ml *.mli | ocamldot | dot -Tps | gv -) &
+
+
+# the pretty entry draws a dependency graph marking red those nodes
+# which do not have their .cmo files 
+
+.INTERMEDIATE: depend.dot depend.2.dot
+.PHONY: depend.ps
+
+depend.dot:
+	ocamldep *.ml *.mli | ocamldot > $@
+
+depend.2.dot:	depend.dot
+	(i=`cat $< | wc -l`; i=`expr $$i - 1`; head -n $$i $<) > $@
+	(for ml in *.ml; do \
+	   base=`basename $$ml .ml`; \
+	   fst=`echo $$base | cut -c1 | tr [:lower:] [:upper:]`; \
+	   rest=`echo $$base | cut -c2-`; \
+	   name=`echo $$fst $$rest | tr -d " "`; \
+	   cmo=$$base.cmo; \
+	   if [ ! -e $$cmo ]; then \
+	     echo \"$$name\" [color=red]\; >> $@;\
+	   fi;\
+         done;\
+	 echo } >> $@)
+
+depend.ps:	depend.2.dot
+	dot -Tps $< > $@
+
+clean::
+	rm -f depend.ps
+
+pretty:	depend.ps
+	(gv -spartan $<; rm $<) &
+#	gv -spartan $< &
+
+
+
+# generating file.ml.mli by tricking make to pass -i to ocamlc 
+
+%.ml.mli:	FORCE
+	@(cmo=`basename $@ .ml.mli`.cmo ; \
+	mv -f $$cmo $$cmo.tmp ; \
+	$(MAKE) -s -C $(TOPDIR) $(BASEDIR)/$$cmo CAMLDEBUG=-i > $@ ; \
+	echo Generated interface file $@ ; \
+	mv -f $$cmo.tmp $$cmo)
+
+%.annot:	FORCE
+	@(cmo=`basename $@ .annot`.cmo ; \
+	mv -f $$cmo $$cmo.tmp ; \
+	$(MAKE) -s -C $(TOPDIR) $(BASEDIR)/$$cmo CAMLDEBUG=-dtypes ; \
+	echo Generated annotation file $@ ; \
+	mv -f $$cmo.tmp $$cmo)
+
+FORCE:
+
+clean::
+	rm -f *.ml.mli
+
+# this is not perfect but mostly WORKS! It just calls the main makefile
+
+%.cmi:	FORCE
+	$(MAKE) -C $(TOPDIR) $(BASEDIR)/$@
+
+%.cmo:	FORCE
+	$(MAKE) -C $(TOPDIR) $(BASEDIR)/$@
+
+coqtop:	
+	$(MAKE) -C $(TOPDIR) bin/coqtop.byte
diff --git a/dev/tools/Makefile.subdir b/dev/tools/Makefile.subdir
new file mode 100644
index 00000000..ff1f3077
--- /dev/null
+++ b/dev/tools/Makefile.subdir
@@ -0,0 +1,7 @@
+# if you work in a sub/sub-rectory of Coq
+# you should make a link to that makefile 
+#    ln -s ../../dev/Makefile.subdir Makefile
+# in order to have all the facilities of dev/Makefile.dir
+
+TOPDIR=../..
+include $(TOPDIR)/dev/tools/Makefile.dir
diff --git a/dev/tools/objects.el b/dev/tools/objects.el
new file mode 100644
index 00000000..b3a2694d
--- /dev/null
+++ b/dev/tools/objects.el
@@ -0,0 +1,153 @@
+(defun add-survive-module nil
+  (interactive)
+  (query-replace-regexp 
+   "
+\\([ 	]*\\)\\(Summary\.\\)?survive_section"
+   "
+\\1\\2survive_module = false;
+\\1\\2survive_section")
+  )
+
+(global-set-key [f2] 'add-survive-module)
+
+; functions to change old style object declaration to new style
+
+(defun repl-open nil
+  (interactive)
+  (query-replace-regexp 
+   "open_function\\([ 	]*\\)=\\([ 	]*\\)cache_\\([a-zA-Z0-9'_]*\\)\\( *\\);" 
+   "open_function\\1=\\2(fun i o -> if i=1 then cache_\\3 o)\\4;") 
+  )
+
+(global-set-key [f6] 'repl-open)
+
+(defun repl-load nil
+  (interactive)
+  (query-replace-regexp 
+   "load_function\\([ 	]*\\)=\\([ 	]*\\)cache_\\([a-zA-Z0-9'_]*\\)\\( *\\);" 
+   "load_function\\1=\\2(fun _ -> cache_\\3)\\4;") 
+  )
+
+(global-set-key [f7] 'repl-load)
+
+(defun repl-decl nil
+  (interactive)
+  (query-replace-regexp
+   "\\(Libobject\.\\)?declare_object[ 
+	]*([ 	]*\\(.*\\)[ 
+	]*,[ 	]*
+\\([ 	]*\\){\\([ 	]*\\)\\([^ ][^}]*\\)}[ 	]*)"
+
+   "\\1declare_object {(\\1default_object \\2) with
+\\3 \\4\\5}")
+;   "|$1=\\1|$2=\\2|$3=\\3|$4=\\4|")
+)
+
+(global-set-key [f9] 'repl-decl)
+
+; eval the above and try f9 f6 f7 on the following:
+
+let (inThing,outThing) =
+  declare_object
+    ("THING", 
+     { load_function = cache_thing;
+       cache_function = cache_thing;
+       open_function = cache_thing;
+       export_function = (function x -> Some x)
+     })
+
+
+;%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+;%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+; functions helping writing non-copying substitutions
+
+(defun make-subst (name)
+  (interactive "s")
+  (defun f (l)
+    (save-excursion
+      (query-replace-regexp
+       (concat "\\([a-zA-z_0-9]*\\)[ 	]*:[ 	]*" 
+	       (car l) 
+	       "\\([ 	]*;\\|[ 	
+]*\}\\)")
+       (concat "let \\1\' = " (cdr l) " " name "\\1 in"))
+      )
+    )
+  (mapcar 'f '(("constr"."subst_mps subst") 
+	       ("Coqast.t"."subst_ast subst") 
+	       ("Coqast.t list"."list_smartmap (subst_ast subst)") 
+	       ("'pat"."subst_pat subst") 
+	       ("'pat unparsing_hunk"."subst_hunk subst_pat subst")
+	       ("'pat unparsing_hunk list"."list_smartmap (subst_hunk subst_pat subst)") 
+	       ("'pat syntax_entry"."subst_syntax_entry subst_pat subst")
+	       ("'pat syntax_entry list"."list_smartmap (subst_syntax_entry subst_pat subst)") 
+	       ("constr option"."option_smartmap (subst_mps subst)")
+	       ("constr list"."list_smartmap (subst_mps subst)")
+	       ("constr array"."array_smartmap (subst_mps subst)")
+	       ("constr_pattern"."subst_pattern subst")
+	       ("constr_pattern option"."option_smartmap (subst_pattern subst)")
+	       ("constr_pattern array"."array_smartmap (subst_pattern subst)")
+	       ("constr_pattern list"."list_smartmap (subst_pattern subst)")
+	       ("global_reference"."subst_global subst")
+	       ("extended_global_reference"."subst_ext subst")
+	       ("obj_typ"."subst_obj subst")
+	       )
+	  )
+  )
+
+
+(global-set-key [f2] 'make-subst)
+
+(defun make-if (name)
+  (interactive "s")
+  (save-excursion
+    (query-replace-regexp
+     "\\([a-zA-z_0-9]*\\)[ 	]*:[ 	]*['a-zA-z_. ]*\\(;\\|[ 	
+]*\}\\)"
+     (concat "&& \\1\' == " name "\\1")
+     )
+    )
+  )
+
+(global-set-key [f4] 'make-if)
+
+(defun make-record nil
+  (interactive)
+  (save-excursion 
+    (query-replace-regexp
+     "\\([a-zA-z_0-9]*\\)[ 	]*:[ 	]*['a-zA-z_. ]*\\(;\\|[ 	
+]*\}\\)"
+     (concat "\\1 = \\1\' ;")
+     )
+    )
+  )
+
+(global-set-key [f5] 'make-record)
+
+(defun make-prim nil
+  (interactive)
+  (save-excursion (query-replace-regexp "\\<[a-zA-Z'_0-9]*\\>" "\\&'"))
+  )
+
+(global-set-key [f6] 'make-prim)
+
+
+; eval the above, yank the text below and do 
+; paste f2 morph.
+; paste f4 morph.
+; paste f5
+
+      lem : constr;
+      profil : bool list;
+      arg_types : constr list;
+      lem2 : constr option                                                      }
+
+
+; and you almost get   Setoid_replace.subst_morph  :)
+
+; and now f5 on this:
+
+   (ref,(c1,c2))
+
+
+
diff --git a/dev/tools/univdot b/dev/tools/univdot
new file mode 100755
index 00000000..bb0dd2c8
--- /dev/null
+++ b/dev/tools/univdot
@@ -0,0 +1,49 @@
+#!/bin/sh
+
+usage() {
+    echo ""
+    echo "usage: univdot [INPUT] [OUTPUT]"
+    echo ""
+    echo "takes the output of Dump Universes \"file\" command"
+    echo "and transforms it to the dot format"
+    echo ""
+    echo "Coq> Dump Universes \"univ.raw\"."
+    echo ""
+    echo "user@host> univdot univ.raw | dot -Tps > univ.ps" 
+    echo ""
+}
+    
+
+# these are dot edge attributes to draw arrows corresponding 
+# to > >= and = edges of the universe graph
+
+GT="[color=red]"
+GE="[color=blue]"
+EQ="[color=black]"
+
+
+# input/output redirection
+case $# in
+  0) ;;
+  1) case $1 in
+       -h|-help|--help) usage
+               exit 0 ;;
+       *) exec < $1 ;;
+     esac ;;
+  2) exec < $1 > $2 ;;
+  *) usage
+     exit 0;;
+esac
+
+
+# dot header
+echo 'digraph G {\
+  size="7.5,10" ;\
+  rankdir = TB ;'
+
+sed -e "s/^\([^ =>]\+\) > \([^ =>]\+\)/\1 -> \2 $GT/" \
+      -e "s/^\([^ =>]\+\) >= \([^ =>]\+\)/\1 -> \2 $GE/" \
+      -e "s/^\([^ =>]\+\) = \([^ =>]\+\)/\1 -> \2 $EQ/" \
+| sed -e "s/\./_/g" 
+
+echo "}"
\ No newline at end of file