From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 21 Nov 2006 21:38:49 +0000 Subject: Imported Upstream version 8.1~gamma --- dev/doc/perf-analysis | 21 ++++++++++++++++++ dev/include | 1 + dev/ocamldebug-coq.template | 24 +++++---------------- dev/tools/Makefile.common | 52 --------------------------------------------- dev/tools/Makefile.devel | 16 +++++++------- dev/tools/Makefile.dir | 4 ++-- dev/tools/Makefile.subdir | 4 ++-- dev/top_printers.ml | 39 ++++++++++++++++++++++++++++++++-- dev/vm_printers.ml | 4 ---- 9 files changed, 76 insertions(+), 89 deletions(-) (limited to 'dev') diff --git a/dev/doc/perf-analysis b/dev/doc/perf-analysis index 23259156..f4cb3bff 100644 --- a/dev/doc/perf-analysis +++ b/dev/doc/perf-analysis @@ -1,6 +1,27 @@ Performance analysis for V8-0 branch ------------------------------------ +Oct 29, 2006: polymorphism on definitions (+ 4%) + +Oct 17, 2006: improvement in new field [r9248] + (QArith -3%, geometry: -2%) + +Oct 5, 2006: fixing wrong unification of Meta below binders + (e.g. CatsInZFC: +10%, CoRN: -2.5%, Godel: +4%, + DISTRIBUTED_REFERENCE_COUNTING: +10%, CoLoR: +1%) + +Sep 26, 2006: new field [r9178-9181] + (QArith: -16%, geometry: -5%, Float: +6%, BDDS:+5% but no ring in it) + + Sep 12, 2006: Rocq/AREA_METHOD extended (~ 530s) + Aug 12, 2006: Rocq/AREA_METHOD added (~ 480s) + May 30, 2006: Nancy/CoLoR added (~ 319s) + +May 17, 2006: changes in List.v (DISTRIBUTED_REFERENCE_COUNTING: -) + +May 5, 2006: improvement in closure (array instead of lists) + (e.g. CatsInZFC: -10%, CoRN: -3%, + Dec 29, 2005: new test and use of -vm in Stalmarck Dec 27, 2005: contrib Karatsuba added (~ 30s) diff --git a/dev/include b/dev/include index 563edd04..42d2a017 100644 --- a/dev/include +++ b/dev/include @@ -25,6 +25,7 @@ #install_printer (* tactic *) pptac;; #install_printer (* object *) ppobj;; #install_printer (* global_reference *) ppglobal;; +#install_printer (* generic_argument *) pp_generic_argument;; #install_printer (* fconstr *) ppfconstr;; diff --git a/dev/ocamldebug-coq.template b/dev/ocamldebug-coq.template index 5c4c4475..44680d6d 100644 --- a/dev/ocamldebug-coq.template +++ b/dev/ocamldebug-coq.template @@ -9,20 +9,7 @@ CAMLBIN=CAMLBINDIRECTORY OCAMLDEBUG=$CAMLBIN/ocamldebug export CAMLP4LIB=`$CAMLBIN/camlp4 -where` -args="" -coqdebug="no" -for op in $* - do case `basename $op` in - coq-debug-programs.out) - coqdebug="yes" - args="-is programs.coq";; - *coq*) coqdebug="yes";; - esac -done - -case $coqdebug in - yes) - exec $OCAMLDEBUG \ +exec $OCAMLDEBUG \ -I $CAMLP4LIB \ -I $COQTOP/config \ -I $COQTOP/lib -I $COQTOP/kernel \ @@ -30,13 +17,12 @@ case $coqdebug in -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics \ -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config \ -I $COQTOP/translate \ - -I $COQTOP/contrib/correctness \ -I $COQTOP/contrib/extraction -I $COQTOP/contrib/field \ - -I $COQTOP/contrib/fourier -I $COQTOP/contrib/graphs \ + -I $COQTOP/contrib/fourier -I $COQTOP/contrib/first-order \ -I $COQTOP/contrib/interface -I $COQTOP/contrib/jprover \ -I $COQTOP/contrib/omega -I $COQTOP/contrib/romega \ -I $COQTOP/contrib/ring -I $COQTOP/contrib/xml \ -I $COQTOP/contrib/subtac -I $COQTOP/contrib/funind \ - $* $args;; - *) exec $OCAMLDEBUG $*;; -esac + -I $COQTOP/contrib/rtauto -I $COQTOP/contrib/setoid_ring \ + -I $COQTOP/contrib/recdef -I $COQTOP/contrib/dp \ + $* diff --git a/dev/tools/Makefile.common b/dev/tools/Makefile.common index 1ff5cf79..e69de29b 100644 --- a/dev/tools/Makefile.common +++ b/dev/tools/Makefile.common @@ -1,52 +0,0 @@ -# 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 index f3abb62d..8dcc70cf 100644 --- a/dev/tools/Makefile.devel +++ b/dev/tools/Makefile.devel @@ -16,9 +16,9 @@ usage:: usage:: @echo " setup-devel -- set the devel makefile" setup-devel: - @ln -sfv dev/Makefile.devel makefile + @ln -sfv dev/tools/Makefile.devel makefile @(for i in $(SOURCEDIRS); do \ - (cd $(TOPDIR)/$$i; ln -sfv ../dev/Makefile.dir Makefile) \ + (cd $(TOPDIR)/$$i; ln -sfv ../dev/tools/Makefile.dir Makefile) \ done) @@ -42,14 +42,14 @@ quick: include Makefile -include $(TOPDIR)/dev/Makefile.common +include $(TOPDIR)/dev/tools/Makefile.common -# this file is better described in dev/Makefile.dir +# this file is better described in dev/tools/Makefile.dir include .depend.devel -#if dev/Makefile.local exists, it is included -ifneq ($(wildcard $(TOPDIR)/dev/Makefile.local),) -include $(TOPDIR)/dev/Makefile.local +#if dev/tools/Makefile.local exists, it is included +ifneq ($(wildcard $(TOPDIR)/dev/tools/Makefile.local),) +include $(TOPDIR)/dev/tools/Makefile.local endif @@ -71,4 +71,4 @@ usage:: vars: @(cd $(TOPDIR); \ echo export COQTOP=`pwd`/ ; \ - echo export COQBIN=`pwd`/bin/ ) \ No newline at end of file + echo export COQBIN=`pwd`/bin/ ) diff --git a/dev/tools/Makefile.dir b/dev/tools/Makefile.dir index 68c917ac..1a1bb90b 100644 --- a/dev/tools/Makefile.dir +++ b/dev/tools/Makefile.dir @@ -1,6 +1,6 @@ # 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 +# ln -s ../dev/tools/Makefile.dir Makefile +# if you are working in a sub/dir/ make a link to dev/tools/Makefile.subdir instead # this Makefile provides many useful facilities to develop Coq # it is not completely compatible with .ml4 files unfortunately diff --git a/dev/tools/Makefile.subdir b/dev/tools/Makefile.subdir index ff1f3077..cb914bd1 100644 --- a/dev/tools/Makefile.subdir +++ b/dev/tools/Makefile.subdir @@ -1,7 +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 +# ln -s ../../dev/tools/Makefile.subdir Makefile +# in order to have all the facilities of dev/tools/Makefile.dir TOPDIR=../.. include $(TOPDIR)/dev/tools/Makefile.dir diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 273f109c..e1ee29e4 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -27,6 +27,8 @@ open Clenv open Cerrors open Evd open Goptions +open Genarg + let _ = Constrextern.print_evar_arguments := true let _ = set_bool_option_value (SecondaryTable ("Printing","Matching")) false @@ -145,9 +147,9 @@ let constr_display csr = | Fix ((t,i),(lna,tl,bl)) -> "Fix(([|"^(Array.fold_right (fun x i -> (string_of_int x)^(if not(i="") then (";"^i) else "")) t "")^"|],"^(string_of_int i)^")," - ^(array_display tl)^"," + ^(array_display tl)^",[|" ^(Array.fold_right (fun x i -> (name_display x)^(if not(i="") - then (";"^i) else "")) lna "")^"," + then (";"^i) else "")) lna "")^"|]," ^(array_display bl)^")" | CoFix(i,(lna,tl,bl)) -> "CoFix("^(string_of_int i)^")," @@ -309,6 +311,39 @@ let ppfconstr c = ppconstr (Closure.term_of_fconstr c) let pploc x = let (l,r) = unloc x in print_string"(";print_int l;print_string",";print_int r;print_string")" +(* extendable tactic arguments *) +let rec pr_argument_type = function + (* Basic types *) + | BoolArgType -> str"bool" + | IntArgType -> str"int" + | IntOrVarArgType -> str"int-or-var" + | StringArgType -> str"string" + | PreIdentArgType -> str"pre-ident" + | IntroPatternArgType -> str"intro-pattern" + | IdentArgType -> str"ident" + | VarArgType -> str"var" + | RefArgType -> str"ref" + (* Specific types *) + | SortArgType -> str"sort" + | ConstrArgType -> str"constr" + | ConstrMayEvalArgType -> str"constr-may-eval" + | QuantHypArgType -> str"qhyp" + | OpenConstrArgType _ -> str"open-constr" + | ConstrWithBindingsArgType -> str"constr-with-bindings" + | BindingsArgType -> str"bindings" + | RedExprArgType -> str"redexp" + | List0ArgType t -> pr_argument_type t ++ str" list0" + | List1ArgType t -> pr_argument_type t ++ str" list1" + | OptArgType t -> pr_argument_type t ++ str" opt" + | PairArgType (t1,t2) -> + str"("++ pr_argument_type t1 ++ str"*" ++ pr_argument_type t2 ++str")" + | ExtraArgType s -> str"\"" ++ str s ++ str "\"" + +let pp_argument_type t = pp (pr_argument_type t) + +let pp_generic_argument arg = + pp(str"") + (**********************************************************************) (* Vernac-level debugging commands *) diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index c037eca7..1e114489 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -65,8 +65,6 @@ and ppatom a = print_string (string_of_kn sp); print_string ","; print_int i; print_string ")" - | Afix_app _ -> print_vfix_app () - | Aswitch _ -> print_vswith() and ppwhd whd = match whd with @@ -74,9 +72,7 @@ and ppwhd whd = | Vprod _ -> print_string "product" | Vfun _ -> print_string "function" | Vfix _ -> print_vfix() - | Vfix_app _ -> print_vfix_app() | Vcofix _ -> print_string "cofix" - | Vcofix_app _ -> print_string "cofix_app" | Vconstr_const i -> print_string "C(";print_int i;print_string")" | Vconstr_block b -> ppvblock b | Vatom_stk(a,s) -> -- cgit v1.2.3