From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- dev/Makefile.common | 52 +++++ dev/Makefile.devel | 74 +++++++ dev/Makefile.dir | 131 ++++++++++++ dev/Makefile.subdir | 7 + dev/README | 21 ++ dev/TODO | 22 ++ dev/base_db | 6 + dev/base_include | 76 +++++++ dev/changements.txt | 455 +++++++++++++++++++++++++++++++++++++++++ dev/db | 35 ++++ dev/db_printers.ml | 16 ++ dev/deboguage.txt | 30 +++ dev/debugging.txt | 50 +++++ dev/header | 7 + dev/include | 35 ++++ dev/objects.el | 153 ++++++++++++++ dev/ocamldebug-v7.template | 41 ++++ dev/style.txt | 49 +++++ dev/top_printers.ml | 303 +++++++++++++++++++++++++++ dev/translate.txt | 495 +++++++++++++++++++++++++++++++++++++++++++++ dev/univdot | 49 +++++ dev/universes.txt | 32 +++ 22 files changed, 2139 insertions(+) create mode 100644 dev/Makefile.common create mode 100644 dev/Makefile.devel create mode 100644 dev/Makefile.dir create mode 100644 dev/Makefile.subdir create mode 100644 dev/README create mode 100644 dev/TODO create mode 100644 dev/base_db create mode 100644 dev/base_include create mode 100644 dev/changements.txt create mode 100644 dev/db create mode 100644 dev/db_printers.ml create mode 100644 dev/deboguage.txt create mode 100644 dev/debugging.txt create mode 100644 dev/header create mode 100644 dev/include create mode 100644 dev/objects.el create mode 100644 dev/ocamldebug-v7.template create mode 100644 dev/style.txt create mode 100644 dev/top_printers.ml create mode 100644 dev/translate.txt create mode 100755 dev/univdot create mode 100644 dev/universes.txt (limited to 'dev') diff --git a/dev/Makefile.common b/dev/Makefile.common new file mode 100644 index 00000000..1ff5cf79 --- /dev/null +++ b/dev/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/Makefile.devel b/dev/Makefile.devel new file mode 100644 index 00000000..f3abb62d --- /dev/null +++ b/dev/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 \ + @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=" +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/Makefile.dir b/dev/Makefile.dir new file mode 100644 index 00000000..54f7bfe9 --- /dev/null +++ b/dev/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/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/Makefile.subdir b/dev/Makefile.subdir new file mode 100644 index 00000000..45358c42 --- /dev/null +++ b/dev/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/Makefile.dir diff --git a/dev/README b/dev/README new file mode 100644 index 00000000..a8811bea --- /dev/null +++ b/dev/README @@ -0,0 +1,21 @@ +This directory contains informations and tools to help developping the +Coq system + + +TODO +changements.txt +header +lisezmoi.txt +style.txt + +Debugging and profiling +======================= + +debugging.txt: help for debugging or profiling +db: to install pretty-printers from ocaml debugger +base_db: to install raw pretty-printers from ocaml debugger +ocamldebug-v7: to launch ocaml debugger +include: to install pretty-printers from ocaml toplevel +base_include: to install raw pretty-printers from ocaml toplevel +universes.txt: help to debug universes +univdot: produces a graph of CIC universes diff --git a/dev/TODO b/dev/TODO new file mode 100644 index 00000000..926861c9 --- /dev/null +++ b/dev/TODO @@ -0,0 +1,22 @@ + + o options de la ligne de commande + - reporter les options de l'ancien script coqtop sur le nouveau coqtop.ml + + o arguments implicites + - les calculer une fois pour toutes à la déclaration (dans Declare) + et stocker cette information dans le in_variable, in_constant, etc. + + o Environnements compilés (type Environ.compiled_env) + - pas de timestamp mais plutôt un checksum avec Digest (mais comment ?) + + o Efficacité + - utiliser DOPL plutôt que DOPN (sauf pour Case) + - batch mode => pas de undo, ni de reset + - conversion : déplier la constante la plus récente + - un cache pour type_of_const, type_of_inductive, type_of_constructor, + lookup_mind_specif + + o Toplevel + - parsing de la ligne de commande : utiliser Arg ??? + + diff --git a/dev/base_db b/dev/base_db new file mode 100644 index 00000000..b540aed6 --- /dev/null +++ b/dev/base_db @@ -0,0 +1,6 @@ +load_printer "gramlib.cma" +load_printer "top_printers.cmo" +install_printer Top_printers.prid +install_printer Top_printers.prsp +install_printer Top_printers.print_pure_constr + diff --git a/dev/base_include b/dev/base_include new file mode 100644 index 00000000..17293776 --- /dev/null +++ b/dev/base_include @@ -0,0 +1,76 @@ + +(* File to include to get some Coq facilities under the ocaml toplevel. + This file is loaded by include *) + +#cd".";; +#directory "parsing";; +#directory "interp";; +#directory "toplevel";; +#directory "library";; +#directory "kernel";; +#directory "pretyping";; +#directory "lib";; +#directory "proofs";; +#directory "tactics";; +#directory "translate";; +#use "top_printers.ml";; + +#install_printer (* identifier *) prid;; +#install_printer (* label *) prlab;; +#install_printer prmsid;; +#install_printer prmbid;; +#install_printer prdir;; +#install_printer prmp;; +#install_printer (* section_path *) prsp;; +#install_printer (* qualid *) prqualid;; +#install_printer (* kernel_name *) prkn;; +#install_printer (* constr *) print_pure_constr;; + +(* parsing of names *) + +let qid = Libnames.qualid_of_string;; + +(* parsing of terms *) + +let parse_com = Pcoq.parse_string Pcoq.Constr.constr;; +let parse_tac = Pcoq.parse_string Pcoq.Tactic.tactic;; +let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;; + +(* For compatibility reasons *) +let parse_ast = parse_com;; + +(* build a term of type rawconstr without type-checking or resolution of + implicit syntax *) + +let e s = Constrintern.interp_rawconstr Evd.empty (Global.env()) (parse_ast s);; + +(* For compatibility *) +let raw_constr_of_string = e;; + +(* build a term of type constr with type-checking and resolution of + implicit syntax *) + +let constr_of_string s = + Constrintern.interp_constr Evd.empty (Global.env()) (parse_ast s);; + +(* get the body of a constant *) + +open Declarations;; + +let constbody_of_string s = + let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_sp (path_of_string s))) in + Util.out_some b.const_body;; + +(* Get the current goal *) + +let getgoal x = top_goal_of_pftreestate (Pfedit.get_pftreestate x);; + +let get_nth_goal n = nth_goal_of_pftreestate n (Pfedit.get_pftreestate ());; +let current_goal () = get_nth_goal 1;; + +let pf_e gl s = + Constrintern.interp_constr (project gl) (pf_env gl) (parse_ast s);; + +open Toplevel +let go = loop + diff --git a/dev/changements.txt b/dev/changements.txt new file mode 100644 index 00000000..d1df2a81 --- /dev/null +++ b/dev/changements.txt @@ -0,0 +1,455 @@ +CHANGES DUE TO INTRODUCTION OF MODULES +====================================== + +1.Kernel +-------- + + The module level has no effect on constr except for the structure of +section_path. The type of unique names for constructions (what +section_path served) is now called a kernel name and is defined by + +type uniq_ident = int * string * dir_path (* int may be enough *) +type module_path = + | MPfile of dir_path (* reference to physical module, e.g. file *) + | MPbound of uniq_ident (* reference to a module parameter in a functor *) + | MPself of uniq_ident (* reference to one of the containing module *) + | MPdot of module_path * label +type label = identifier +type kernel_name = module_path * dir_path * label + ^^^^^^^^^^^ ^^^^^^^^ ^^^^^ + | | \ + | | the base name + | \ + / the (true) section path + example: (non empty only inside open sections) + L = (* i.e. some file of logical name L *) + struct + module A = struct Def a = ... end + end + M = (* i.e. some file of logical name M *) + struct + Def t = ... + N = functor (X : sig module T = struct Def b = ... end end) -> struct + module O = struct + Def u = ... + end + Def x := ... .t ... .O.u ... X.T.b ... L.A.a + + and are self-references, X is a bound reference and L is a +reference to a physical module. + + Notice that functor application is not part of a path: it must be +named by a "module M = F(A)" declaration to be used in a kernel +name. + + Notice that Jacek chose a practical approach, making directories not +modules. Another approach could have been to replace the constructor +MPfile by a constant constructor MProot representing the root of the +world. + + Other relevant informations are in kernel/entries.ml (type +module_expr) and kernel/declarations.ml (type module_body and +module_type_body). + +2. Library +---------- + +i) tables +[Summaries] - the only change is the special treatment of the +global environmet. + +ii) objects +[Libobject] declares persistent objects, given with methods: + + * cache_function specifying how to add the object in the current + scope; + * load_function, specifying what to do when the module + containing the object is loaded; + * open_function, specifying what to do when the module + containing the object is opened (imported); + * classify_function, specyfying what to do with the object, + when the current module (containing the object) is ended. + * subst_function + * export_function, to signal end_section survival + +(Almost) Each of these methods is called with a parameter of type +object_name = section_path * kernel_name +where section_path is the full user name of the object (such as +Coq.Init.Datatypes.Fst) and kernel_name is its substitutive internal +version such as (MPself,[],"Fst") (see above) + + +What happens at the end of an interactive module ? +================================================== +(or when a file is stored and reloaded from disk) + +All summaries (except Global environment) are reverted to the state +from before the beginning of the module, and: + +a) the objects (again, since last Declaremods.start_module or + Library.start_library) are classified using the classify_function. + To simplify consider only those who returned Substitute _ or Keep _. + +b) If the module is not a functor, the subst_function for each object of + the first group is called with the substitution + [MPself "" |-> MPfile "Coq.Init.Datatypes"]. + Then the load_function is called for substituted objects and the + "keep" object. + (If the module is a library the substitution is done at reloading). + +c) The objects which returned substitute are stored in the modtab + together with the self ident of the module, and functor argument + names if the module was a functor. + + They will be used (substituted and loaded) when a command like + Module M := F(N) or + Module Z := N + is evaluated + + +The difference between "substitute" and "keep" objects +======================================================== +i) The "keep" objects can _only_ reference other objects by section_paths +and qualids. They do not need the substitution function. + +They will work after end_module (or reloading a compiled library), +because these operations do not change section_path's + +They will obviously not work after Module Z:=N. + +These would typically be grammar rules, pretty printing rules etc. + + + +ii) The "substitute" objects can _only_ reference objects by +kernel_names. They must have a valid subst_function. + +They will work after end_module _and_ after Module Z:=N or +Module Z:=F(M). + + + +Other kinds of objects: +iii) "Dispose" - objects which do not survive end_module + As a consequence, objects which reference other objects sometimes + by kernel_names and sometimes by section_path must be of this kind... + +iv) "Anticipate" - objects which must be treated individually by + end_module (typically "REQUIRE" objects) + + + +Writing subst_thing functions +============================= +The subst_thing shoud not copy the thing if it hasn't actually +changed. There are some cool emacs macros in dev/objects.el +to help writing subst functions this way quickly and without errors. +Also there are *_smartmap functions in Util. + +The subst_thing functions are already written for many types, +including constr (Term.subst_mps), +global_reference (Libnames.subst_global), +rawconstr (Rawterm.subst_raw) etc + +They are all (apart from constr, for now) written in the non-copying +way. + + +Nametab +======= + +Nametab has been made more uniform. For every kind of thing there is +only one "push" function and one "locate" function. + + +Lib +=== + +library_segment is now a list of object_name * library_item, where +object_name = section_path * kernel_name (see above) + +New items have been added for open modules and module types + + +Declaremods +========== +Functions to declare interactive and noninteractive modules and module +types. + + +Library +======= +Uses Declaremods to actually communicate with Global and to register +objects. + + +MAIN CHANGES FROM COQ V7.3 +========================== + +Internal representation of tactics bindings has changed (see type +Rawterm.substitution). + +New parsing model for tactics and vernacular commands + + - Introduction of a dedicated type for tactic expressions + (Tacexpr.raw_tactic_expr) + - Introduction of a dedicated type for vernac expressions + (Vernacexpr.vernac_expr) + - Declaration of new vernacular parsing rules by a new camlp4 macro + GRAMMAR COMMAND EXTEND ... END to be used in ML files + - Declaration of new tactics parsing/printing rules by a new camlp4 macro + TACTIC EXTEND ... END to be used in ML files + +New organisation of THENS: +tclTHENS tac tacs : tacs is now an array +tclTHENSFIRSTn tac1 tacs tac2 : + apply tac1 then, apply the array tacs on the first n subgoals and + tac2 on the remaining subgoals (previously tclTHENST) +tclTHENSLASTn tac1 tac2 tacs : + apply tac1 then, apply tac2 on the first subgoals and apply the array + tacs on the last n subgoals +tclTHENFIRSTn tac1 tacs = tclTHENSFIRSTn tac1 tacs tclIDTAC (prev. tclTHENSI) +tclTHENLASTn tac1 tacs = tclTHENSLASTn tac1 tclIDTAC tacs +tclTHENFIRST tac1 tac2 = tclTHENFIRSTn tac1 [|tac2|] +tclTHENLAST tac1 tac2 = tclTHENLASTn tac1 [|tac2|] (previously tclTHENL) +tclTHENS tac1 tacs = tclTHENSFIRSTn tac1 tacs (fun _ -> error "wrong number") +tclTHENSV same as tclTHENS but with an array +tclTHENSi : no longer available + +Proof_type: subproof field in type proof_tree glued with the ref field + +Tacmach: no more echo from functions of module Refiner + +Files contrib/*/g_*.ml4 take the place of files contrib/*/*.v. +Files parsing/{vernac,tac}extend.ml{4,i} implements TACTIC EXTEND andd + VERNAC COMMAND EXTEND macros +File syntax/PPTactic.v moved to parsing/pptactic.ml +Tactics about False and not now in tactics/contradiction.ml +Tactics depending on Init now tactics/*.ml4 (no longer in tactics/*.v) +File tacinterp.ml moved from proofs to directory tactics + +MAIN CHANGES FROM COQ V7.1 TO COQ V7.2 +====================================== + +The core of Coq (kernel) has meen minimized with the following effects: + +kernel/term.ml split into kernel/term.ml, pretyping/termops.ml +kernel/reduction.ml split into kernel/reduction.ml, pretyping/reductionops.ml +kernel/names.ml split into kernel/names.ml, library/nameops.ml +kernel/inductive.ml split into kernel/inductive.ml, pretyping/inductiveops.ml + +the prefixes "Is" ans "IsMut" have been dropped from kind_of_term constructors, +e.g. IsRel is now Rel, IsMutCase is now Case, etc. + + +PRINCIPAUX CHANGEMENTS ENTRE COQ V6.3.1 ET COQ V7.0 +=================================================== + +Changements d'organisation / modules : +-------------------------------------- + + Std, More_util -> lib/util.ml + + Names -> kernel/names.ml et kernel/sign.ml + (les parties noms et signatures ont été séparées) + + Avm,Mavm,Fmavm,Mhm -> utiliser plutôt Map (et freeze alors gratuit) + Mhb -> Bij + + Generic est intégré à Term (et un petit peu à Closure) + +Changements dans les types de données : +--------------------------------------- + dans Generic: free_rels : constr -> int Listset.t + devient : constr -> Intset.t + + type_judgement -> typed_type + environment -> context + context -> typed_type signature + + +ATTENTION: +---------- + + Il y a maintenant d'autres exceptions que UserError (TypeError, + RefinerError, etc.) + + Il ne faut donc plus se contenter (pour rattraper) de faire + + try . .. with UserError _ -> ... + + mais écrire à la place + + try ... with e when Logic.catchable_exception e -> ... + + +Changements dans les fonctions : +-------------------------------- + + Vectops. + it_vect -> Array.fold_left + vect_it -> Array.fold_right + exists_vect -> Util.array_exists + for_all2eq_vect -> Util.array_for_all2 + tabulate_vect -> Array.init + hd_vect -> Util.array_hd + tl_vect -> Util.array_tl + last_vect -> Util.array_last + it_vect_from -> array_fold_left_from + vect_it_from -> array_fold_right_from + app_tl_vect -> array_app_tl + cons_vect -> array_cons + map_i_vect -> Array.mapi + map2_vect -> array_map2 + list_of_tl_vect -> array_list_of_tl + + Names + sign_it -> fold_var_context (se fait sur env maintenant) + it_sign -> fold_var_context_reverse (sur env maintenant) + + Generic + noccur_bet -> noccur_between + substn_many -> substnl + + Std + comp -> Util.compose + rev_append -> List.rev_append + + Termenv + mind_specif_of_mind -> Global.lookup_mind_specif + ou Environ.lookup_mind_specif si on a un env sous la main + mis_arity -> instantiate_arity + mis_lc -> instantiate_lc + + Ex-Environ + mind_of_path -> Global.lookup_mind + + Printer + gentermpr -> gen_pr_term + term0 -> prterm_env + pr_sign -> pr_var_context + pr_context_opt -> pr_context_of + pr_ne_env -> pr_ne_context_of + + Typing, Machops + type_of_type -> judge_of_type + fcn_proposition -> judge_of_prop_contents + safe_fmachine -> safe_infer + + Reduction, Clenv + whd_betadeltat -> whd_betaevar + whd_betadeltatiota -> whd_betaiotaevar + find_mrectype -> Inductive.find_mrectype + find_minductype -> Inductive.find_inductive + find_mcoinductype -> Inductive.find_coinductive + + Astterm + constr_of_com_casted -> interp_casted_constr + constr_of_com_sort -> interp_type + constr_of_com -> interp_constr + rawconstr_of_com -> interp_rawconstr + type_of_com -> type_judgement_of_rawconstr + judgement_of_com -> judgement_of_rawconstr + + Termast + bdize -> ast_of_constr + + Tacmach + pf_constr_of_com_sort -> pf_interp_type + pf_constr_of_com -> pf_interp_constr + pf_get_hyp -> pf_get_hyp_typ + pf_hyps, pf_untyped_hyps -> pf_env (tout se fait sur env maintenant) + + Pattern + raw_sopattern_of_compattern -> Astterm.interp_constrpattern + somatch -> is_matching + dest_somatch -> matches + + Tacticals + matches -> gl_is_matching + dest_match -> gl_matches + suff -> utiliser sort_of_goal + lookup_eliminator -> utiliser sort_of_goal pour le dernier arg + + Divers + initial_sign -> var_context + + Sign + ids_of_sign -> ids_of_var_context (or Environ.ids_of_context) + empty_sign -> empty_var_context + + Pfedit + list_proofs -> get_all_proof_names + get_proof -> get_current_proof_name + abort_goal -> abort_proof + abort_goals -> abort_all_proofs + abort_cur_goal -> abort_current_proof + get_evmap_sign -> get_goal_context/get_current_goal_context + unset_undo -> reset_undo + + Proof_trees + mkGOAL -> mk_goal + + Declare + machine_constant -> declare_constant (+ modifs) + + ex-Trad, maintenant Pretyping + inh_cast_rel -> Coercion.inh_conv_coerce_to + inh_conv_coerce_to -> Coercion.inh_conv_coerce_to_fail + ise_resolve1 -> understand, understand_type + ise_resolve -> understand_judgment, understand_type_judgment + + ex-Tradevar, maintenant Evarutil + mt_tycon -> empty_tycon + + Recordops + struc_info -> find_structure + +Changements dans les inductifs +------------------------------ +Nouveaux types "constructor" et "inductive" dans Term +La plupart des fonctions de typage des inductives prennent maintenant +un inductive au lieu d'un oonstr comme argument. Les seules fonctions +à traduire un constr en inductive sont les find_rectype and co. + +Changements dans les grammaires +------------------------------- + + . le lexer (parsing/lexer.mll) est maintenant un lexer ocamllex + + . attention : LIDENT -> IDENT (les identificateurs n'ont pas de + casse particulière dans Coq) + + . Le mot "command" est remplacé par "constr" dans les noms de + fichiers, noms de modules et non-terminaux relatifs au parsing des + termes; aussi les changements suivants "COMMAND"/"CONSTR" dans + g_vernac.ml4, VARG_COMMAND/VARG_CONSTR dans vernac*.ml* + + . Les constructeurs d'arguments de tactiques IDENTIFIER, CONSTR, ...n + passent en minuscule Identifier, Constr, ... + + . Plusieurs parsers ont changé de format (ex: sortarg) + +Changements dans le pretty-printing +----------------------------------- + + . Découplage de la traduction de constr -> rawconstr (dans detyping) + et de rawconstr -> ast (dans termast) + . Déplacement des options d'affichage de printer vers termast + . Déplacement des réaiguillage d'univers du pp de printer vers esyntax + + +Changements divers +------------------ + + . il n'y a plus de script coqtop => coqtop et coqtop.byte sont + directement le résultat du link du code + => debuggage et profiling directs + + . il n'y a plus d'installation locale dans bin/$ARCH + + . #use "include.ml" => #use "include" + go() => loop() + + . il y a "make depend" et "make dependcamlp4" car ce dernier prend beaucoup + de temps diff --git a/dev/db b/dev/db new file mode 100644 index 00000000..44effd77 --- /dev/null +++ b/dev/db @@ -0,0 +1,35 @@ +load_printer "gramlib.cma" +load_printer "top_printers.cmo" +install_printer Top_printers.prid +install_printer Top_printers.prlab +install_printer Top_printers.prmsid +install_printer Top_printers.prmbid +install_printer Top_printers.prdir +install_printer Top_printers.prmp +install_printer Top_printers.prkn +install_printer Top_printers.prsp +install_printer Top_printers.prqualid +install_printer Top_printers.prast +install_printer Top_printers.prastpat +install_printer Top_printers.prastpatl + +install_printer Top_printers.pppattern +install_printer Top_printers.pprawterm + +install_printer Top_printers.ppterm +install_printer Top_printers.print_uni +install_printer Top_printers.pp_universes +install_printer Top_printers.pptype +install_printer Top_printers.prj + +install_printer Top_printers.prgoal +install_printer Top_printers.prsigmagoal +install_printer Top_printers.pproof +install_printer Top_printers.prevd +install_printer Top_printers.prevc +install_printer Top_printers.prwc +install_printer Top_printers.prclenv + +install_printer Top_printers.pptac +install_printer Top_printers.pr_obj + diff --git a/dev/db_printers.ml b/dev/db_printers.ml new file mode 100644 index 00000000..cee94d47 --- /dev/null +++ b/dev/db_printers.ml @@ -0,0 +1,16 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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/ocamldebug-v7.template b/dev/ocamldebug-v7.template new file mode 100644 index 00000000..96c53192 --- /dev/null +++ b/dev/ocamldebug-v7.template @@ -0,0 +1,41 @@ +#!/bin/sh + +# wrap around ocamldebug for Coq + +export COQTOP=COQTOPDIRECTORY +export COQLIB=COQLIBDIRECTORY +export COQTH=$COQLIB/theories +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 \ + -I $CAMLP4LIB \ + -I $COQTOP/config \ + -I $COQTOP/lib -I $COQTOP/kernel \ + -I $COQTOP/library -I $COQTOP/pretyping -I $COQTOP/parsing \ + -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/interface -I $COQTOP/contrib/jprover \ + -I $COQTOP/contrib/omega -I $COQTOP/contrib/romega \ + -I $COQTOP/contrib/ring -I $COQTOP/contrib/xml \ + $* $args;; + *) exec $OCAMLDEBUG $*;; +esac diff --git a/dev/style.txt b/dev/style.txt new file mode 100644 index 00000000..2e597dc4 --- /dev/null +++ b/dev/style.txt @@ -0,0 +1,49 @@ + +<< L'uniformité du style est plus importante que le style lui-même. >> +(Kernigan & Pike, The Practice of Programming) + +Mode Emacs +========== + Tuareg, que l'on trouve ici : http://www.prism.uvsq.fr/~acohen/tuareg/ + + avec le réglage suivant : (setq tuareg-in-indent 2) + +Types récursifs et filtrages +============================ + Une barre de séparation y compris sur le premier constructeur + +type t = + | A + | B of machin + +match expr with + | A -> ... + | B x -> ... + + +Conditionnelles +=============== + if condition then + premier-cas + else + deuxieme-cas + + Si effets de bord dans les branches, utilisez begin ... end et non des + parenthèses i.e. + + if condition then begin + instr1; + instr2 + end else begin + instr3; + instr4 + end + + Si la première branche lève une exception, évitez le else i.e. + + if condition then if condition then error "machin"; + error "machin" -----> suite + else + suite + + diff --git a/dev/top_printers.ml b/dev/top_printers.ml new file mode 100644 index 00000000..7f92d64c --- /dev/null +++ b/dev/top_printers.ml @@ -0,0 +1,303 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* pp(pr_rawterm x)) +let pppattern = (fun x -> pp(pr_pattern x)) +let pptype = (fun x -> pp(prtype x)) + +let safe_prglobal = function + | ConstRef kn -> pp (str "CONSTREF(" ++ pr_kn kn ++ str ")") + | IndRef (kn,i) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++ + int i ++ str ")") + | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ pr_kn kn ++ str "," ++ + int i ++ str "," ++ int j ++ str ")") + | VarRef id -> pp (str "VARREF(" ++ pr_id id ++ str ")") + +let prglobal x = try pp(pr_global x) with _ -> safe_prglobal x + +let prid id = pp (pr_id id) +let prlab l = pp (pr_lab l) + +let prmsid msid = pp (str (debug_string_of_msid msid)) +let prmbid mbid = pp (str (debug_string_of_mbid mbid)) + +let prdir dir = pp (pr_dirpath dir) + +let prmp mp = pp(str (string_of_mp mp)) +let prkn kn = pp(pr_kn kn) + +let prsp sp = pp(pr_sp sp) + +let prqualid qid = pp(pr_qualid qid) + +let prconst (sp,j) = + pp (str"#" ++ pr_kn sp ++ str"=" ++ prterm j.uj_val) + +let prvar ((id,a)) = + pp (str"#" ++ pr_id id ++ str":" ++ prterm a) + +let genprj f j = let (c,t) = f j in (c ++ str " : " ++ t) + +let prj j = pp (genprj prjudge j) + +let prgoal g = pp(prgl g) + +let prsigmagoal g = pp(prgl (sig_it g)) + +let prgls gls = pp(pr_gls gls) + +let prglls glls = pp(pr_glls glls) + +let pproof p = pp(print_proof Evd.empty empty_named_context p) + +let prevd evd = pp(pr_decls evd) + +let prevc evc = pp(pr_evc evc) + +let prwc wc = pp(pr_evc wc) + +let prclenv clenv = pp(pr_clenv clenv) + +let print_uni u = (pp (pr_uni u)) + +let pp_universes u = pp (str"[" ++ pr_universes u ++ str"]") + +let ppenv e = pp + (str "[" ++ pr_named_context_of e ++ str "]" ++ spc() ++ + str "[" ++ pr_rel_context e (rel_context e) ++ str "]") + +let pptac = (fun x -> pp(Pptactic.pr_glob_tactic x)) + +let pr_obj obj = Format.print_string (Libobject.object_tag obj) + +let cnt = ref 0 + +let constr_display csr = + let rec term_display c = match kind_of_term c with + | Rel n -> "Rel("^(string_of_int n)^")" + | Meta n -> "Meta("^(string_of_int n)^")" + | Var id -> "Var("^(string_of_id id)^")" + | Sort s -> "Sort("^(sort_display s)^")" + | Cast (c,t) -> "Cast("^(term_display c)^","^(term_display t)^")" + | Prod (na,t,c) -> + "Prod("^(name_display na)^","^(term_display t)^","^(term_display c)^")\n" + | Lambda (na,t,c) -> + "Lambda("^(name_display na)^","^(term_display t)^","^(term_display c)^")\n" + | LetIn (na,b,t,c) -> + "LetIn("^(name_display na)^","^(term_display b)^"," + ^(term_display t)^","^(term_display c)^")" + | App (c,l) -> "App("^(term_display c)^","^(array_display l)^")\n" + | Evar (e,l) -> "Evar("^(string_of_int e)^","^(array_display l)^")" + | Const c -> "Const("^(string_of_kn c)^")" + | Ind (sp,i) -> + "MutInd("^(string_of_kn sp)^","^(string_of_int i)^")" + | Construct ((sp,i),j) -> + "MutConstruct(("^(string_of_kn sp)^","^(string_of_int i)^")," + ^(string_of_int j)^")" + | Case (ci,p,c,bl) -> + "MutCase(,"^(term_display p)^","^(term_display c)^"," + ^(array_display bl)^")" + | 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.fold_right (fun x i -> (name_display x)^(if not(i="") + then (";"^i) else "")) lna "")^"," + ^(array_display bl)^")" + | CoFix(i,(lna,tl,bl)) -> + "CoFix("^(string_of_int i)^")," + ^(array_display tl)^"," + ^(Array.fold_right (fun x i -> (name_display x)^(if not(i="") + then (";"^i) else "")) lna "")^"," + ^(array_display bl)^")" + + and array_display v = + "[|"^ + (Array.fold_right + (fun x i -> (term_display x)^(if not(i="") then (";"^i) else "")) + v "")^"|]" + + and sort_display = function + | Prop(Pos) -> "Prop(Pos)" + | Prop(Null) -> "Prop(Null)" + | Type u -> + incr cnt; pp (str "with " ++ int !cnt ++ pr_uni u ++ fnl ()); + "Type("^(string_of_int !cnt)^")" + + and name_display = function + | Name id -> "Name("^(string_of_id id)^")" + | Anonymous -> "Anonymous" + + in + msg (str (term_display csr) ++fnl ()) + +open Format;; + +let print_pure_constr csr = + let rec term_display c = match kind_of_term c with + | Rel n -> print_string "#"; print_int n + | Meta n -> print_string "Meta("; print_int n; print_string ")" + | Var id -> print_string (string_of_id id) + | Sort s -> sort_display s + | Cast (c,t) -> open_hovbox 1; + print_string "("; (term_display c); print_cut(); + print_string "::"; (term_display t); print_string ")"; close_box() + | Prod (Name(id),t,c) -> + open_hovbox 1; + print_string"("; print_string (string_of_id id); + print_string ":"; box_display t; + print_string ")"; print_cut(); + box_display c; close_box() + | Prod (Anonymous,t,c) -> + print_string"("; box_display t; print_cut(); print_string "->"; + box_display c; print_string ")"; + | Lambda (na,t,c) -> + print_string "["; name_display na; + print_string ":"; box_display t; print_string "]"; + print_cut(); box_display c; + | LetIn (na,b,t,c) -> + print_string "["; name_display na; print_string "="; + box_display b; print_cut(); + print_string ":"; box_display t; print_string "]"; + print_cut(); box_display c; + | App (c,l) -> + print_string "("; + box_display c; + Array.iter (fun x -> print_space (); box_display x) l; + print_string ")" + | Evar (e,l) -> print_string "Evar#"; print_int e; print_string "{"; + Array.iter (fun x -> print_space (); box_display x) l; + print_string"}" + | Const c -> print_string "Cons("; + sp_display c; + print_string ")" + | Ind (sp,i) -> + print_string "Ind("; + sp_display sp; + print_string ","; print_int i; + print_string ")" + | Construct ((sp,i),j) -> + print_string "Constr("; + sp_display sp; + print_string ","; + print_int i; print_string ","; print_int j; print_string ")" + | Case (ci,p,c,bl) -> + open_vbox 0; + print_string "<"; box_display p; print_string ">"; + print_cut(); print_string "Case"; + print_space(); box_display c; print_space (); print_string "of"; + open_vbox 0; + Array.iter (fun x -> print_cut(); box_display x) bl; + close_box(); + print_cut(); + print_string "end"; + close_box() + | Fix ((t,i),(lna,tl,bl)) -> + print_string "Fix("; print_int i; print_string ")"; + print_cut(); + open_vbox 0; + let rec print_fix () = + for k = 0 to Array.length tl do + open_vbox 0; + name_display lna.(k); print_string "/"; + print_int t.(k); print_cut(); print_string ":"; + box_display tl.(k) ; print_cut(); print_string ":="; + box_display bl.(k); close_box (); + print_cut() + done + in print_string"{"; print_fix(); print_string"}" + | CoFix(i,(lna,tl,bl)) -> + print_string "CoFix("; print_int i; print_string ")"; + print_cut(); + open_vbox 0; + let rec print_fix () = + for k = 0 to Array.length tl do + open_vbox 1; + name_display lna.(k); print_cut(); print_string ":"; + box_display tl.(k) ; print_cut(); print_string ":="; + box_display bl.(k); close_box (); + print_cut(); + done + in print_string"{"; print_fix (); print_string"}" + + and box_display c = open_hovbox 1; term_display c; close_box() + + and sort_display = function + | Prop(Pos) -> print_string "Set" + | Prop(Null) -> print_string "Prop" + | Type u -> open_hbox(); + print_string "Type("; pp (pr_uni u); print_string ")"; close_box() + + and name_display = function + | Name id -> print_string (string_of_id id) + | Anonymous -> print_string "_" +(* Remove the top names for library and Scratch to avoid long names *) + and sp_display sp = +(* let dir,l = decode_kn sp in + let ls = + match List.rev (List.map string_of_id (repr_dirpath dir)) with + ("Top"::l)-> l + | ("Coq"::_::l) -> l + | l -> l + in List.iter (fun x -> print_string x; print_string ".") ls;*) + print_string (string_of_kn sp) + + in + box_display csr; print_flush() +(* +let _ = + Vernacentries.add "PrintConstr" + (function + | [VARG_CONSTR c] -> + (fun () -> + let (evmap,sign) = Command.get_current_context () in + constr_display (Constrintern.interp_constr evmap sign c)) + | _ -> bad_vernac_args "PrintConstr") + +let _ = + Vernacentries.add "PrintPureConstr" + (function + | [VARG_CONSTR c] -> + (fun () -> + let (evmap,sign) = Command.get_current_context () in + print_pure_constr (Constrintern.interp_constr evmap sign c)) + | _ -> bad_vernac_args "PrintPureConstr") +*) + +let ppfconstr c = ppterm (Closure.term_of_fconstr c) diff --git a/dev/translate.txt b/dev/translate.txt new file mode 100644 index 00000000..5b372c96 --- /dev/null +++ b/dev/translate.txt @@ -0,0 +1,495 @@ + + How to use the translator + ========================= + + (temporary version to be included in the official + TeX document describing the translator) + +The translator is a smart, robust and powerful tool to improve the +readibility of your script. The current document describes the +possibilities of the translator. + +In case of problem recompiling the translated files, don't waste time +to modify the translated file by hand, read first the following +document telling on how to modify the original files to get a smooth +uniform safe translation. All 60000 lines of Coq lines on our +user-contributions server have been translated without any change +afterwards, and 0,5 % of the lines of the original files (mainly +notations) had to be modified beforehand to get this result. + +Table of contents +----------------- + +I) Implicit Arguments + 1) Strict Implicit Arguments + 2) Implicit Arguments in standard library + +II) Notations + 1) Translating a V7 notation as it was + 2) Translating a V7 notation which conflicts with the new syntax + a) Associativity conflicts + b) Conflicts with other notations + b1) A notation hides another notation + b2) A notation conflicts with the V8 grammar + b3) My notation is already defined at another level + c) How to use V8only with Distfix ? + d) Can I overload a notation in V8, e.g. use "*" and "+" ? + 3) Using the translator to have simplest notations + 4) Setting the translator to automatically use new notations that + wasn't used in old syntax + 5) Defining a construction and its notation simultaneously + +III) Various pitfalls + 1) New keywords + 2) Old "Case" and "Match" + 3) Change of definition or theorem names + 4) Change of tactic names + +--------------------------------------------------------------------- + +I) Implicit Arguments + ------------------ + +1) Strict Implicit Arguments + + "Set Implicit Arguments" changes its meaning in V8: the default is +to turn implicit only the arguments that are _strictly_ implicit (or +rigid), i.e. that remains inferable whatever the other arguments +are. E.g "x" inferable from "P x" is not strictly inferable since it +can disappears if "P" is instanciated by a term which erase "x". + + To respect the old semantics, the default behaviour of the +translator is to replace each occurrence "Set Implicit Arguments" by + + Set Implicit Arguments. + Unset Strict Implicits. + + However, you may wish to adopt the new semantics of "Set Implicit +Arguments" (for instance because you think that the choice of +arguments it setsimplicit is more "natural" for you). In this case, +add the option -strict-implicit to the translator. + + Warning: Changing the number of implicit arguments can break the +notations. Then use the V8only modifier of Notations. + +2) Implicit Arguments in standard library + + Main definitions of standard library have now implicit +arguments. These arguments are dropped in the translated files. This +can exceptionally be a source of incompatibilities which has to be +solved by hand (it typically happens for polymorphic functions applied +to "nil" or "None"). + +II) Notations + --------- + + Grammar (on constr) and Syntax are no longer supported. Replace them by +Notation before translation. + + Precedence levels are now from 0 to 200. In V8, the precedence and +associativity of an operator cannot be redefined. Typical level are +(refer to the chapter on notations in the Reference Manual for the +full list): + + <-> : 95 (no associativity) + -> : 90 (right associativity) + \/ : 85 (right associativity) + /\ : 80 (right associativity) + ~ : 75 (right associativity) + =, <, >, <=, >=, <> : 70 (no associativity) + +, - : 50 (left associativity) + *, / : 40 (left associativity) + ^ : 30 (right associativity) + +1) Translating a V7 notation as it was + + By default, the translator keeps the associativity given in V7 while +the levels are mapped according to the following table: + + the V7 levels [ 0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10] + are resp. mapped in V8 to [ 0; 20; 30; 40; 50; 70; 80; 85; 90; 95; 100] + with predefined assoc [ No; L; R; L; L; No; R; R; R; No; L] + + If this is OK for you, just simply apply the translator. + +2) Translating a V7 notation which conflicts with the new syntax + +a) Associativity conflict + + Since the associativity of the levels obtained by translating a V7 +level (as shown on table above) cannot be changed, you have to choose +another level with a compatible associativity. + + You can choose any level between 0 and 200, knowing that the +standard operators are already set at the levels shown on the list +above. + +Example 1: Assume you have a notation + +Infix NONA 2 "=_S" my_setoid_eq. + +By default, the translator moves it to level 30 which is right +associative, hence a conflict with the expected no associativity. + +To solve the problem, just add the "V8only" modifier to reset the +level and enforce the associativity as follows: + +Infix NONA 2 "=_S" my_setoid_eq V8only (at level 70, no associativity). + +The translator now knows that it has to translate "=_S" at level 70 +with no associativity. + +Rem: 70 is the "natural" level for relations, hence the choice of 70 +here, but any other level accepting a no-associativity would have been +OK. + +Example 2: Assume you have a notation + +Infix RIGHTA 1 "o" my_comp. + +By default, the translator moves it to level 20 which is left +associative, hence a conflict with the expected right associativity. + +To solve the problem, just add the "V8only" modifier to reset the +level and enforce the associativity as follows: + +Infix RIGHTA 1 "o" my_comp V8only (at level 20, right associativity). + +The translator now knows that it has to translate "o" at level 20 +which has the correct "right associativity". + +Rem: We assumed here that the user wants a strong precedence for +composition, in such a way, say, that "f o g + h" is parsed as +"(f o g) + h". To get "o" binding less than the arithmetical operators, +an appropriated level would have been close of 70, and below, e.g. 65. + +b) Conflicts with other notations + +Since the new syntax comes with new keywords and new predefined +symbols, new conflicts can occur. Again, you can use the option V8only +to inform the translator of the new syntax to use. + +b1) A notation hides another notation + +Rem: use Print Grammar constr in V8 to diagnose the overlap and see the +section on factorization in the chapter on notations of the Reference +Manual for hints on how to factorize. + +Example: + +Notation "{ x }" := (my_embedding x) (at level 1). + +overlaps in V8 with notation "{ x : A & P }" at level 0 and with x at +level 99. The conflicts can be solved by left-factorizing the notation +as follows: + +Notation "{ x }" := (my_embedding x) (at level 1) + V8only (at level 0, x at level 99). + +b2) A notation conflicts with the V8 grammar. + +Again, use the V8only modifier to tell the translator to automatically +take in charge the new syntax. + +Example: + +Infix 3 "@" app. + +Since "@" is used in the new syntax for deactivating the implicit +arguments, another symbol has to be used, e.g. "@@". This is done via +the V8only option as follows: + +Infix 3 "@" app V8only "@@" (at level 40, left associativity). + +or, alternatively by + +Notation "x @ y" := (app x y) (at level 3, left associativity) + V8only "x @@ y" (at level 40, left associativity). + +b3) My notation is already defined at another level (or with another +associativity) + +In V8, the level and associativity of a given notation can no longer +be changed. Then, either you adopt the standard reserved levels and +associativity for this notation (as given on the list above) or you +change your notation. + +- To change the notation, follow the directions in section b2. + +- To adopt the standard level, just use V8only without any argument. + +Example. + +Infix 6 "*" my_mult. + +is not accepted as such in V8. Write + +Infix 6 "*" my_mult V8only. + +to tell the translator to use "*" at the reserved level (i.e. 40 with +left associativity). Even better, use interpretation scopes (look at +the Reference Manual). + +c) How to use V8only with Distfix ? + +You can't, use Notation instead of Distfix. + +d) Can I overload a notation in V8, e.g. use "*" and "+" for my own +algebraic operations ? + +Yes, using interpretation scopes (see the corresponding chapter in the +Reference Manual). + +3) Using the translator to have simplest notations + +Thanks to the new syntax, * has now the expected left associativity, +and the symbols <, >, <= and >= are now available. + +Thanks to the interpretation scopes, you can overload the +interpretation of these operators with the default interpretation +provided in Coq. + +This may be a motivation to use the translator to automatically change +the notations while switching to the new syntax. + +See sections b) and d) above for examples. + +4) Setting the translator to automatically use new notations that +wasn't used in old syntax + +Thanks to the "Notation" mechanism, defining symbolic notations is +simpler than in the previous versions of Coq. + +Thanks to the new syntax and interpretation scopes, new symbols and +overloading is available. + +This may be a motivation for using the translator to automatically change +the notations while switching to the new syntax. + +Use for that the commands V8Notation and V8Infix. + +Examples: + +V8Infix "==>" my_relation (at level 65, right associativity). + +tells the translator to write an infix "==>" instead of my_relation in +the translated files. + +V8Infix ">=" my_ge. + +tells the translator to write an infix ">=" instead of my_ge in the +translated files and that the level and associativity are the standard +one (as defined in the chart above). + +V8Infix ">=" my_ge : my_scope. + +tells the translator to write an infix ">=" instead of my_ge in the +translated files, that the level and associativity are the standard +one (as defined in the chart above), but only if scope my_scope is +open or if a delimiting key is available for "my_scope" (see the +Reference Manual). + +5) Defining a construction and its notation simultaneously + +This is permitted by the new syntax. Look at the Reference Manual for +explanation. The translator is not fully able to take this in charge... + +III) Various pitfalls + ---------------- + +1) New keywords + + The following identifiers are new keywords + + "forall"; "fun"; "match"; "fix"; "cofix"; "for"; "if"; "then"; + "else"; "return"; "mod"; "at"; "let"; "_"; ".(" + + The translator automatically add a "_" to names clashing with a +keyword, except for files. Hence users may need to rename the files +whose name clashes with a keyword. + + Remark: "in"; "with"; "end"; "as"; "Prop"; "Set"; "Type" + were already keywords + +2) Old "Case" and "Match" + + "Case" and "Match" are normally automatically translated into + "match" or "match" and "fix", but sometimes it fails to do so. It + typically fails when the Case or Match is argument of a tactic whose + typing context is unknown because of a preceding Intro/Intros, as e.g. in + + Intros; Exists [m:nat](Case m of t [p:nat](f m) end) + + The solution is then to replace the invocation of the sequence of + tactics into several invocation of the elementary tactics as follows + + Intros. Exists [m:nat](Case m of t [p:nat](f m) end) + ^^^ + +3) Change of definition or theorem names + + Type "entier" from fast_integer.v is renamed into "N" by the +translator. As a consequence, user-defined objects of same name "N" +are systematically qualified even tough it may not be necessary. The +same apply for names "GREATER", "EQUAL", "LESS", etc... [COMPLETE LIST +TO GIVE]. + +4) Change of tactics names + + Since tactics names are now lowercase, this can clash with +user-defined tactic definitions. To pally this, clashing names are +renamed by adding an extra "_" to their name. + +====================================================================== +Main examples for new syntax +---------------------------- + +1) Constructions + + Applicative terms don't any longer require to be surrounded by parentheses as +e.g in + + "x = f y -> S x = S (f y)" + + + Product is written + + "forall x y : T, U" + "forall x y, U" + "forall (x y : T) z (v w : V), U" + etc. + + Abstraction is written + + "fun x y : T, U" + "fun x y, U" + "fun (x y : T) z (v w : V), U" + etc. + + Pattern-matching is written + + "match x with c1 x1 x2 => t | c2 y as z => u end" + "match v1, v2 with c1 x1 x2, _ => t | c2 y, d z => u end" + "match v1 as y in le _ n, v2 as z in I p q return P n y p q z with + c1 x1 x2, _ => t | c2 y, d z => u end" + + The last example is the new form of what was written + + "<[n;y:(le ? n);p;q;z:(I p q)](P n y p q z)>Cases v1 v2 of + (c1 x1 x2) _ => t | (c2 y) (d z) => u end" + + Pattern-matching of type with one constructors and no dependencies +of the arguments in the resulting type can be written + + "let (x,y,z) as u return P u := t in v" + + Local fixpoints are written + + "fix f (n m:nat) z (x : X) {struct m} : nat := ... + with ..." + + and "struct" tells which argument is structurally decreasing. + + Explicitation of implicit arguments is written + + "f @1:=u v @3:=w t" + "@f u v w t" + +2) Tactics + + The main change is that tactics names are now lowercase. Besides +this, the following renaming are applied: + + "NewDestruct" -> "destruct" + "NewInduction" -> "induction" + "Induction" -> "simple induction" + "Destruct" -> "simple destruct" + + For tactics with occurrences, the occurrences now comes after and + repeated use is separated by comma as in + + "Pattern 1 3 c d 4 e" -> "pattern c at 3 1, d, e at 4" + "Unfold 1 3 f 4 g" -> "unfold f at 1 3, g at 4" + "Simpl 1 3 e" -> "simpl e at 1 3" + +3) Tactic language + + Definitions are now introduced with keyword "Ltac" (instead of +"Tactic"/"Meta" "Definition") and are implicitly recursive +("Recursive" is no longer used). + + The new rule for distinguishing terms from ltac expressions is: + + Write "ltac:" in front of any tactic in argument position and + "constr:" in front of any construction in head position + +4) Vernacular language + +a) Assumptions + + The syntax for commands is mainly unchanged. Declaration of +assumptions is now done as follows + + Variable m : t. + Variables m n p : t. + Variables (m n : t) (u v : s) (w : r). + +b) Definitions + + Definitions are done as follows + + Definition f m n : t := ... . + Definition f m n := ... . + Definition f m n := ... : t. + Definition f (m n : u) : t := ... . + Definition f (m n : u) := ... : t. + Definition f (m n : u) := ... . + Definition f a b (p q : v) r s (m n : t) : t := ... . + Definition f a b (p q : v) r s (m n : t) := ... . + Definition f a b (p q : v) r s (m n : t) := ... : t. + +c) Fixpoints + + Fixpoints are done this way + + Fixpoint f x (y : t) z a (b c : u) {struct z} : v := ... with ... . + Fixpoint f x : v := ... . + Fixpoint f (x : t) : v := ... . + + It is possible to give a concrete notation to a fixpoint as follows + + Fixpoint plus (n m:nat) {struct n} : nat as "n + m" := + match n with + | O => m + | S p => S (p + m) + end. + +d) Inductive types + + The syntax for inductive types is as follows + + Inductive t (a b : u) (d : e) : v := + c1 : w1 | c2 : w2 | ... . + + Inductive t (a b : u) (d : e) : v := + c1 : w1 | c2 : w2 | ... . + + Inductive t (a b : u) (d : e) : v := + c1 (x y : t) : w1 | c2 (z : r) : w2 | ... . + + As seen in the last example, arguments of the constructors can be +given before the colon. If the type itself is omitted (allowed only in +case the inductive type has no real arguments), this yields an +ML-style notation as follows + + Inductive nat : Set := O | S (n:nat). + Inductive bool : Set := true | false. + + It is even possible to define a syntax at the same time, as follows: + + Inductive or (A B:Prop) : Prop as "A \/ B":= + | or_introl (a:A) : A \/ B + | or_intror (b:B) : A \/ B. + + Inductive and (A B:Prop) : Prop as "A /\ B" := conj (a:A) (b:B). + diff --git a/dev/univdot b/dev/univdot new file mode 100755 index 00000000..bb0dd2c8 --- /dev/null +++ b/dev/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 diff --git a/dev/universes.txt b/dev/universes.txt new file mode 100644 index 00000000..65c1e522 --- /dev/null +++ b/dev/universes.txt @@ -0,0 +1,32 @@ +How to debug universes? + +1. There is a command Dump Universes in Coq toplevel + + Dump Universes. + prints the graph of universes in the form of constraints + + Dump Universes "file". + produces the "file" containing universe constraints in the form + univ1 # univ2 ; + where # can be either > >= or = + + The file produced by the latter command can be transformed using + the script univdot to dot format. + For example + + univdot file | dot -Tps > file.ps + + produces a graph of universes in ps format. + > arrows are red, >= blue, and = black. + + + *) for dot see http://www.research.att.com/sw/tools/graphviz/ + + +2. There is a printing option + + Termast.print_universes : bool ref + + which, when set (in ocaml after Drop), makes all pretty-printed + Type's annotated with the name of the universe. + -- cgit v1.2.3