From 8e66761c81648add03ed21b157a3bace716b8e08 Mon Sep 17 00:00:00 2001 From: pboutill Date: Thu, 29 Apr 2010 16:33:36 +0000 Subject: "make source-doc" builds documentation of mli in html and pdf at dev/ocamldoc/ old "make source-doc" that documents ml files and didn't work is now "make ml-doc" but still don't work :-) "make clean" cleans dev/ocamldoc/ properly wierd? calls of dependency graph generation leave unchanged git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12978 85f007b7-540e-0410-9357-904b9bb8a0f7 --- .gitignore | 6 ++ Makefile | 3 + Makefile.build | 65 +++++++------ Makefile.common | 15 ++- config/Makefile.template | 5 - dev/Makefile | 53 ----------- dev/docintro | 50 ---------- dev/html/style.css | 220 -------------------------------------------- dev/ocamldoc/docintro | 49 ++++++++++ dev/ocamldoc/html/style.css | 220 ++++++++++++++++++++++++++++++++++++++++++++ ide/coq.png | Bin 6269 -> 2335 bytes kernel/term.mli | 94 ++++++++++--------- library/nameops.mli | 2 +- library/nametab.mli | 10 +- 14 files changed, 388 insertions(+), 404 deletions(-) delete mode 100644 dev/Makefile delete mode 100644 dev/docintro delete mode 100644 dev/html/style.css create mode 100644 dev/ocamldoc/docintro create mode 100644 dev/ocamldoc/html/style.css diff --git a/.gitignore b/.gitignore index 4a16b7722..f0dd91db9 100644 --- a/.gitignore +++ b/.gitignore @@ -169,3 +169,9 @@ kernel/copcodes.ml scripts/tolink.ml theories/Numbers/Natural/BigN/NMake_gen.v ide/index_urls.txt + +# mlis documentation + +dev/ocamldoc/html/ +dev/ocamldoc/coq.* +dev/ocamldoc/ocamldoc.sty diff --git a/Makefile b/Makefile index f1f04e77d..ea318c111 100644 --- a/Makefile +++ b/Makefile @@ -227,6 +227,9 @@ voclean: devdocclean: find . -name '*.dep.ps' -o -name '*.dot' | xargs rm -f + rm -f $(OCAMLDOCDIR)/*.log $(OCAMLDOCDIR)/*.aux $(OCAMLDOCDIR)/*.toc + rm -f $(OCAMLDOCDIR)/ocamldoc.sty $(OCAMLDOCDIR)/coq.tex + rm -f $(OCAMLDOCDIR)/html/*.html ########################################################################### # Emacs tags diff --git a/Makefile.build b/Makefile.build index fe2bba29e..2dd8ec01b 100644 --- a/Makefile.build +++ b/Makefile.build @@ -584,12 +584,47 @@ install-latex: # Documentation of the source code (using ocamldoc) ########################################################################### -.PHONY: source-doc +.PHONY: source-doc mli-doc ml-doc -source-doc: - if !(test -d $(SOURCEDOCDIR)); then mkdir $(SOURCEDOCDIR); fi +source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf + +$(OCAMLDOCDIR)/coq.tex:: $(DOCMLIS:.mli=.cmi) + $(OCAMLDOC) -latex -rectypes -I /usr/lib/ocaml/camlp5 $(MLINCLUDES)\ + $(DOCMLIS) -t "Coq mlis documentation" \ + -intro $(OCAMLDOCDIR)/docintro -o $@ + +mli-doc:: $(DOCMLIS:.mli=.cmi) + $(OCAMLDOC) -html -rectypes -I /usr/lib/ocaml/camlp5 $(MLINCLUDES)\ + $(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \ + -t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \ + -css-style style.css + +%.png: %.dot + $(DOT) -Tpng $< -o $@ + +%.types.dot: %.mli + $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $< + +OCAMLDOC_MLLIBD = $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \ + `cat $| | tr ' ' '\n' | sed -n -e "/\.cmo/s/\.cmo/\.ml/p"` + +%.dot: | %.mllib.d + $(OCAMLDOC_MLLIBD) + +ml-doc: $(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) $(MLSTATICFILES) +parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d + $(OCAMLDOC_MLLIBD) + +tactics/tactics.dot: | tactics/tactics.mllib.d tactics/hightactics.mllib.d + $(OCAMLDOC_MLLIBD) + +%.dot: %.mli + $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< + +$(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex + (cd $(OCAMLDOCDIR) ; pdflatex $*.tex && pdflatex $*.tex) ########################################################################### ### Special rules @@ -657,7 +692,7 @@ ifeq ($(CHECKEDOUT),git) if test -x "`which git`"; then \ LANG=C; export LANG; \ GIT_BRANCH=$$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/\1/p'); \ - GIT_HOST=$$(hostname -f); \ + GIT_HOST=$$(hostname); \ GIT_PATH=$$(pwd); \ (echo "$${GIT_HOST}:$${GIT_PATH},$${GIT_BRANCH}") > revision.new; \ (echo "$$(git log -1 --pretty='format:%H')") >> revision.new; \ @@ -822,28 +857,6 @@ devel: $(DEBUGPRINTERS) ########################################################################### -%.types.dot: %.mli - $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $< - -%.dep.ps: %.dot - $(DOT) $(DOTOPTS) -o $@ $< - -OCAMLDOC_MLLIBD = $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \ - `cat $| | tr ' ' '\n' | sed -n -e "/\.cmo/s/\.cmo/\.ml/p"` - -%.dot: | %.mllib.d - $(OCAMLDOC_MLLIBD) - -parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d - $(OCAMLDOC_MLLIBD) - -tactics/tactics.dot: | tactics/tactics.mllib.d tactics/hightactics.mllib.d - $(OCAMLDOC_MLLIBD) - -%.dot: %.mli - $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< - - # For emacs: # Local Variables: # mode: makefile diff --git a/Makefile.common b/Makefile.common index 4d5e00d25..9f44b3b6f 100644 --- a/Makefile.common +++ b/Makefile.common @@ -339,7 +339,20 @@ MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ DATE=$(shell LANG=C date +"%B %Y") -SOURCEDOCDIR=dev/source-doc +########################################################################### +# Source documentation +########################################################################### + +OCAMLDOCDIR=dev/ocamldoc + +DOCMLIS=$(wildcard ./lib/*.mli ./kernel/*.mli ./library/*.mli \ + ./pretyping/*.mli ./interp/*.mli \ + ./parsing/*.mli ./proofs/*.mli \ + ./tactics/*.mli ./toplevel/*.mli) + +# Defining options to generate dependencies graphs +DOT=dot +ODOCDOTOPTS=-dot -dot-reduce # For emacs: # Local Variables: diff --git a/config/Makefile.template b/config/Makefile.template index 74ec95807..e29a4befe 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -144,11 +144,6 @@ UIMSCRIPTDIR=UIMSCRIPTPATH # Defining REVISION CHECKEDOUT=CHECKEDOUTSOURCETREE -# Defining options to generate dependencies graphs -DOT=dot -DOTOPTS=-Tps -ODOCDOTOPTS=-dot -dot-reduce - # Option to control compilation and installation of the documentation WITHDOC=WITHDOCOPT diff --git a/dev/Makefile b/dev/Makefile deleted file mode 100644 index 4693bd136..000000000 --- a/dev/Makefile +++ /dev/null @@ -1,53 +0,0 @@ -include ../config/Makefile - -LOCALINCLUDES=-I ../config -I ../tools -I ../tools/coqdoc \ - -I ../scripts -I ../lib -I ../kernel -I ../kernel/byterun -I ../library \ - -I ../proofs -I ../tactics -I ../pretyping \ - -I ../interp -I ../toplevel -I ../parsing -I ../ide/utils -I ../ide \ - -I ../plugins/omega -I ../plugins/romega \ - -I ../plugins/ring -I ../plugins/dp -I ../plugins/setoid_ring \ - -I ../plugins/xml -I ../plugins/extraction \ - -I ../plugins/fourier -I ../plugins/cc \ - -I ../plugins/funind -I ../plugins/firstorder \ - -I ../plugins/field -I ../plugins/subtac -I ../plugins/rtauto \ - -I ../plugins/recdef - -MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) - -MLIS=$(wildcard ../lib/*.mli ../kernel/*.mli ../library/*.mli \ - ../pretyping/*.mli ../interp/*.mli \ - ../parsing/*.mli ../proofs/*.mli \ - ../tactics/*.mli ../toplevel/*.mli) - -all:: html coq.pdf - -newsyntax.dvi: newsyntax.tex - latex $< - latex $< - -coq.dvi: coq.tex - latex coq - latex coq - -coq.tex:: - ocamldoc -latex -rectypes -I /usr/lib/ocaml/camlp5 $(MLINCLUDES)\ - $(MLIS) -t "Coq mlis documentation" -intro docintro -o coq.tex - -html:: - ocamldoc -html -rectypes -I /usr/lib/ocaml/camlp5 $(MLINCLUDES)\ - $(MLIS) -d html -colorize-code \ - -t "Coq mlis documentation" -intro docintro -css-style style.css - -%.dot: ../% - ocamldoc -rectypes $(MLINCLUDES) -t $* -dot -dot-reduce ../$*/*.ml ../$*/*.mli -o $@ - -%.png: %.dot - dot -Tpng $< -o $@ - -clean:: - rm -f *~ *.log *.aux - -.SUFFIXES: .tex .png - -%.pdf: %.tex - pdflatex $< && pdflatex $< \ No newline at end of file diff --git a/dev/docintro b/dev/docintro deleted file mode 100644 index 3d37d5374..000000000 --- a/dev/docintro +++ /dev/null @@ -1,50 +0,0 @@ -{!indexlist} - -This is Coq, a proof assistant for the Calculus of Inductive Construction. -This document describes the implementation of Coq. -It has been automatically generated from the source of -Coq using ocamldoc, a literate programming tool for -Objective Caml freely available at http://caml.inria.fr/. -The source files are organized in several directories ordered like that: - -{ol {- Utility libraries : lib - -describes the various utility libraries used in the code -of Coq.} -{- Kernel : kernel - -describes the \Coq\ kernel, which is a type checker for the Calculus -of Inductive Construction.} -{- Library : library - -describes the Coq library, which is made of two parts: -- a general mechanism to keep a trace of all operations and of - the state of the system, with backtrack capabilities; -- a global environment for the CCI, with functions to export and - import compiled modules. - -} -{- Pretyping : pretyping - -} -{- Front abstract syntax of terms : interp - -describes the translation from Coq context-dependent -front abstract syntax of terms {v front v} to and from the -context-free, untyped, raw form of constructions {v rawconstr v}.} -{- Parsers and printers : parsing - -describes the implementation of the \Coq\ parsers and printers.} -{- Proof engine : proofs - -describes the Coq proof engine, which is also called -the ``refiner'', since it provides a way to build terms by successive -refining steps. Those steps are either primitive rules or higher-level -tactics.} -{- Tacticts : tactics - -describes the Coq main tactics.} -{- Toplevel : toplevel - -describes the highest modules of the Coq system.} -} diff --git a/dev/html/style.css b/dev/html/style.css deleted file mode 100644 index b8f02a15f..000000000 --- a/dev/html/style.css +++ /dev/null @@ -1,220 +0,0 @@ -a:visited { - color: #416DFF; text-decoration: none; -} - -a:link { - color: #416DFF; text-decoration: none; -} - -a:hover { - color: Red; text-decoration: none; background-color: #5FFF88 -} - -a:active { - color: Red; text-decoration: underline; -} - -.keyword { - font-weight: bold; color: Red -} - -.keywordsign { - color: #C04600 -} - -.superscript { - font-size: 4 -} - -.subscript { - font-size: 4 -} - -.comment { - color: Green -} - -.constructor { - color: Blue -} - -.type { - color: #5C6585 -} - -.string { - color: Maroon -} - -.warning { - color: Red; font-weight: bold -} - -.info { - margin-left: 3em; margin-right: 3em -} - -.param_info { - margin-top: 4px; margin-left: 3em; margin-right: 3em -} - -.code { - color: #465F91; -} - -h1 { - font-size: 20pt; text-align: center; -} - -h5, h6, div.h7, div.h8, div.h9 { - font-size: 20pt; - border: 1px solid #000000; - margin-top: 5px; - margin-bottom: 2px; - text-align: center; - padding: 2px; -} - -h5 { - background-color: #90FDFF; -} - -h6 { - background-color: #016699; - color: white; -} - -div.h7 { - background-color: #E0FFFF; -} - -div.h8 { - background-color: #F0FFFF; -} - -div.h9 { - background-color: #FFFFFF; -} - -.typetable, .indextable, .paramstable { - border-style: hidden; -} - -.paramstable { - padding: 5pt 5pt; -} - -body { - background-color: white; -} - -tr { - background-color: white; -} - -td.typefieldcomment { - background-color: #FFFFFF; - font-size: smaller; -} - -pre { - margin-bottom: 4px; -} - -div.sig_block { - margin-left: 2em; -} - - -h2 { - font-family: Arial, Helvetica, sans-serif; - font-size: 16pt; - font-weight: normal; - border-bottom: 1px solid #dadada; - border-top: 1px solid #dadada; - color: #101010; - background: #eeeeff; - margin: 25px 0px 10px 0px; - padding: 1px 1px 1px 1px; -} - -h3 { - font-family: Arial, Helvetica, sans-serif; - font-size: 12pt; - color: #016699; - font-weight: bold; - padding: 15px 0 0 0ex; - margin: 5px 0 0 0; -} - -h4 { - font-family: Arial, Helvetica, sans-serif; - font-size: 10pt; - color: #016699; - padding: 15px 0 0 0ex; - margin: 5px 0 0 0; -} - -/* Here starts the overwrite of default rules to give a better look */ - -body { - font-family: Calibri, Georgia, Garamond, Baskerville, serif; - font-size: 12pt; - background-color: white; -} - -a:link, a { - color: #6895c3 !important; -} - -a:hover { - color: #2F4459 !important; - background-color: white; -} - -hr { - height: 1px; - color: #016699; - background-color: #016699; - border-width: 0; -} - -h1, h1 a:link, h1 a:visited, h1 a { - font-family: Cambria, Georgia, Garamond, Baskerville, serif; - color: #016699; -} - -.navbar { - float: left; -} - -.navbar a, .navbar a:link, .navbar a:visited { - color: #016699; - font-family: Arial, Helvetica, sans-serif; - font-weight: bold; - font-size: 80%; -} - -.keyword { - color: #c13939; -} - -.constructor { - color: #3c8f7e; -} - -pre, code { - font-family: "DejaVu Sans Mono", "Bitstream Vera Mono", "Courrier New", monospace; - white-space: normal; - font-size: 9pt; - font-weight: bold; -} - -.type br { - display: none; -} - -.info { - margin-left: 1em; - font-size: 12pt; -} diff --git a/dev/ocamldoc/docintro b/dev/ocamldoc/docintro new file mode 100644 index 000000000..3c0e262d4 --- /dev/null +++ b/dev/ocamldoc/docintro @@ -0,0 +1,49 @@ +{!indexlist} + +This is Coq, a proof assistant for the Calculus of Inductive Constructions. +This document describes the implementation of Coq. +It has been automatically generated from the source of +Coq using {{:http://caml.inria.fr/}ocamldoc}. +The source files are organized in several directories ordered like that: + +{ol {- Utility libraries : lib + +describes the various utility libraries used in the code +of Coq.} +{- Kernel : kernel + +describes the Coq kernel, which is a type checker for the Calculus +of Inductive Constructions.} +{- Library : library + +describes the Coq library, which is made of two parts: +- a general mechanism to keep a trace of all operations and of + the state of the system, with backtrack capabilities; +- a global environment for the CCI, with functions to export and + import compiled modules. + +} +{- Pretyping : pretyping + +} +{- Front abstract syntax of terms : interp + +describes the translation from Coq context-dependent +front abstract syntax of terms {v constr_expr v} to and from the +context-free, untyped, raw form of constructions {v rawconstr v}.} +{- Parsers and printers : parsing + +describes the implementation of the Coq parsers and printers.} +{- Proof engine : proofs + +describes the Coq proof engine, which is also called +the ``refiner'', since it provides a way to build terms by successive +refining steps. Those steps are either primitive rules or higher-level +tactics.} +{- Tacticts : tactics + +describes the Coq main tactics.} +{- Toplevel : toplevel + +describes the highest modules of the Coq system.} +} diff --git a/dev/ocamldoc/html/style.css b/dev/ocamldoc/html/style.css new file mode 100644 index 000000000..c2c45b629 --- /dev/null +++ b/dev/ocamldoc/html/style.css @@ -0,0 +1,220 @@ +a:visited { + color: #416DFF; text-decoration: none; +} + +a:link { + color: #416DFF; text-decoration: none; +} + +a:hover { + color: Red; text-decoration: none; background-color: #5FFF88 +} + +a:active { + color: Red; text-decoration: underline; +} + +.keyword { + font-weight: bold; color: Red +} + +.keywordsign { + color: #C04600 +} + +.superscript { + font-size: 8 +} + +.subscript { + font-size: 8 +} + +.comment { + color: Green +} + +.constructor { + color: Blue +} + +.type { + color: #5C6585 +} + +.string { + color: Maroon +} + +.warning { + color: Red; font-weight: bold +} + +.info { + margin-left: 3em; margin-right: 3em +} + +.param_info { + margin-top: 4px; margin-left: 3em; margin-right: 3em +} + +.code { + color: #465F91; +} + +h1 { + font-size: 20pt; text-align: center; +} + +h5, h6, div.h7, div.h8, div.h9 { + font-size: 20pt; + border: 1px solid #000000; + margin-top: 5px; + margin-bottom: 2px; + text-align: center; + padding: 2px; +} + +h5 { + background-color: #90FDFF; +} + +h6 { + background-color: #016699; + color: white; +} + +div.h7 { + background-color: #E0FFFF; +} + +div.h8 { + background-color: #F0FFFF; +} + +div.h9 { + background-color: #FFFFFF; +} + +.typetable, .indextable, .paramstable { + border-style: hidden; +} + +.paramstable { + padding: 5pt 5pt; +} + +body { + background-color: white; +} + +tr { + background-color: white; +} + +td.typefieldcomment { + background-color: #FFFFFF; + font-size: smaller; +} + +pre { + margin-bottom: 4px; +} + +div.sig_block { + margin-left: 2em; +} + + +h2 { + font-family: Arial, Helvetica, sans-serif; + font-size: 16pt; + font-weight: normal; + border-bottom: 1px solid #dadada; + border-top: 1px solid #dadada; + color: #101010; + background: #eeeeff; + margin: 25px 0px 10px 0px; + padding: 1px 1px 1px 1px; +} + +h3 { + font-family: Arial, Helvetica, sans-serif; + font-size: 12pt; + color: #016699; + font-weight: bold; + padding: 15px 0 0 0ex; + margin: 5px 0 0 0; +} + +h4 { + font-family: Arial, Helvetica, sans-serif; + font-size: 10pt; + color: #016699; + padding: 15px 0 0 0ex; + margin: 5px 0 0 0; +} + +/* Here starts the overwrite of default rules to give a better look */ + +body { + font-family: Calibri, Georgia, Garamond, Baskerville, serif; + font-size: 12pt; + background-color: white; +} + +a:link, a { + color: #6895c3 !important; +} + +a:hover { + color: #2F4459 !important; + background-color: white; +} + +hr { + height: 1px; + color: #016699; + background-color: #016699; + border-width: 0; +} + +h1, h1 a:link, h1 a:visited, h1 a { + font-family: Cambria, Georgia, Garamond, Baskerville, serif; + color: #016699; +} + +.navbar { + float: left; +} + +.navbar a, .navbar a:link, .navbar a:visited { + color: #016699; + font-family: Arial, Helvetica, sans-serif; + font-weight: bold; + font-size: 80%; +} + +.keyword { + color: #c13939; +} + +.constructor { + color: #3c8f7e; +} + +pre, code { + font-family: "DejaVu Sans Mono", "Bitstream Vera Mono", "Courrier New", monospace; + white-space: normal; + font-size: 9pt; + font-weight: bold; +} + +.type br { + display: none; +} + +.info { + margin-left: 1em; + font-size: 12pt; +} diff --git a/ide/coq.png b/ide/coq.png index 06aac4597..992f2d63f 100644 Binary files a/ide/coq.png and b/ide/coq.png differ diff --git a/kernel/term.mli b/kernel/term.mli index f7819d6e6..5efd95696 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -36,7 +36,8 @@ type existential_key = int type metavariable = int (** {6 Case annotation } *) -type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle (** infer printing form from number of constructor *) +type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle + | RegularStyle (** infer printing form from number of constructor *) type case_printing = { ind_nargs : int; (** length of the arity of the inductive type *) style : case_style } @@ -64,8 +65,7 @@ val eq_constr : constr -> constr -> bool type types = constr -(** {6 ... } *) -(** Functions for dealing with constr terms. +(** {5 Functions for dealing with constr terms. } The following functions are intended to simplify and to uniform the manipulation of terms. Some of these functions may be overlapped with previous ones. *) @@ -95,20 +95,21 @@ val mkType : Univ.universe -> types (** This defines the strategy to use for verifiying a Cast *) type cast_kind = VMcast | DEFAULTcast -(** Constructs the term [t1::t2], i.e. the term {% $ %}t_1{% $ %} casted with the - type {% $ %}t_2{% $ %} (that means t2 is declared as the type of t1). *) +(** Constructs the term [t1::t2], i.e. the term t{_ 1} casted with the + type t{_ 2} (that means t2 is declared as the type of t1). *) val mkCast : constr * cast_kind * constr -> constr (** Constructs the product [(x:t1)t2] *) val mkProd : name * types * types -> types val mkNamedProd : identifier -> types -> types -> types -(** non-dependant product {% $ %}t_1 \rightarrow t_2{% $ %}, an alias for - [(_:t1)t2]. Beware {% $ %}t_2{% $ %} is NOT lifted. - Eg: A |- A->A is built by [(mkArrow (mkRel 0) (mkRel 1))] *) +(** non-dependent product [t1 -> t2], an alias for + [forall (_:t1), t2]. Beware [t_2] is NOT lifted. + Eg: in context [A:Prop], [A->A] is built by [(mkArrow (mkRel 0) (mkRel 1))] +*) val mkArrow : types -> types -> constr -(** Constructs the abstraction {% $ %}[x:t_1]t_2{% $ %} *) +(** Constructs the abstraction \[x:t{_ 1}\]t{_ 2} *) val mkLambda : name * types * constr -> constr val mkNamedLambda : identifier -> types -> constr -> constr @@ -117,7 +118,7 @@ val mkLetIn : name * constr * types * constr -> constr val mkNamedLetIn : identifier -> constr -> types -> constr -> constr (** [mkApp (f,[| t_1; ...; t_n |]] constructs the application - {% $ %}(f~t_1~\dots~t_n){% $ %}. *) + {% $(f~t_1~\dots~t_n)$ %}. *) val mkApp : constr * constr array -> constr (** Constructs a constant @@ -135,12 +136,12 @@ val mkInd : inductive -> constr introduced in the section *) val mkConstruct : constructor -> constr -(** Construct the term

Case c of c1 | c2 .. | cn end +(** Constructs a destructor of inductive type. - [mkCase ci p c ac] stand for match [c] return [p] with [ac] presented as - describe in [ci]. + [mkCase ci p c ac] stand for match [c] as [x] in [I args] return [p] with [ac] + presented as describe in [ci]. - [p] stucture is lambda inductive_args, I inductive_args -> "return" + [p] stucture is [fun args x -> "return clause"] [ac]{^ ith} element is ith constructor case presented as {e lambda construct_args (without params). case_term } *) @@ -158,7 +159,7 @@ val mkCase : case_info * constr * constr * constr array -> constr ... with fn [ctxn] = bn.] - \noindent where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. + where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. *) type rec_declaration = name array * types array * constr array type fixpoint = (int array * int) * rec_declaration @@ -166,7 +167,7 @@ val mkFix : fixpoint -> constr (** If [funnames = [|f1,.....fn|]] [typarray = [|t1,...tn|]] - [bodies = [b1,.....bn]] \par\noindent + [bodies = [b1,.....bn]] then [mkCoFix (i, (funnames, typarray, bodies))] constructs the ith function of the block @@ -253,10 +254,10 @@ val is_Type : constr -> bool val iskind : constr -> bool val is_small : sorts -> bool -(** {6 ... } *) -(** Term destructors. - Destructor operations are partial functions and - raise [invalid_arg "dest*"] if the term has not the expected form. *) + +(** {6 Term destructors } *) +(** Destructor operations are partial functions and + @raise Invalid_argument "dest*" if the term has not the expected form. *) (** Destructs a DeBrujin index *) val destRel : constr -> int @@ -304,28 +305,32 @@ val destInd : constr -> inductive (** Destructs a constructor *) val destConstruct : constr -> constructor -(** Destructs a term

Case c of lc1 | lc2 .. | lcn end *) +(** Destructs a [match c as x in I args return P with ... | +Ci(...yij...) => ti | ... end] (or [let (..y1i..) := c as x in I args +return P in t1], or [if c then t1 else t2]) +@return [(info,c,fun args x => P,[|...|fun yij => ti| ...|])] +where [info] is pretty-printing information *) val destCase : constr -> case_info * constr * constr * constr array (** Destructs the {% $ %}i{% $ %}th function of the block - {% $ %}{% \mathit{%}Fixpoint{% }%} ~ f_1 ~ [ctx_1] = b_1 - {% \mathit{%}with{% }%} ~ f_2 ~ [ctx_2] = b_2 - \dots - {% \mathit{%}with{% }%} ~ f_n ~ [ctx_n] = b_n{% $ %}, - where the lenght of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. + [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1} + with f{_ 2} ctx{_ 2} = b{_ 2} + ... + with f{_ n} ctx{_ n} = b{_ n}], + where the length of the {% $ %}j{% $ %}th context is {% $ %}ij{% $ %}. *) val destFix : constr -> fixpoint val destCoFix : constr -> cofixpoint -(** {6 ... } *) -(** A {e declaration} has the form (name,body,type). It is either an +(** {6 Local } *) +(** A {e declaration} has the form [(name,body,type)]. It is either an {e assumption} if [body=None] or a {e definition} if [body=Some actualbody]. It is referred by {e name} if [na] is an identifier or by {e relative index} if [na] is not an identifier (in the latter case, [na] is of type [name] but just for printing - purpose *) + purpose) *) type named_declaration = identifier * constr option * types type rel_declaration = name * constr option * types @@ -367,44 +372,47 @@ val abs_implicit : constr -> constr val lambda_implicit : constr -> constr val lambda_implicit_lift : int -> constr -> constr -(** [applist (f,args)] and co work as [mkApp] *) +(** [applist (f,args)] and its variants work as [mkApp] *) val applist : constr * constr list -> constr val applistc : constr -> constr list -> constr val appvect : constr * constr array -> constr val appvectc : constr -> constr array -> constr -(** [prodn n l b] = {% $ %}(x_1:T_1)..(x_n:T_n)b{% $ %} - where {% $ %}l = [(x_n,T_n);\dots;(x_1,T_1);Gamma]{% $ %} *) +(** [prodn n l b] = [forall (x_1:T_1)...(x_n:T_n), b] + where [l] is [(x_n,T_n)...(x_1,T_1)...]. *) val prodn : int -> (name * constr) list -> constr -> constr -(** [compose_prod l b] = {% $ %}(x_1:T_1)..(x_n:T_n)b{% $ %} - where {% $ %}l = [(x_n,T_n);\dots;(x_1,T_1)]{% $ %}. +(** [compose_prod l b] + @return [forall (x_1:T_1)...(x_n:T_n), b] + where [l] is [(x_n,T_n)...(x_1,T_1)]. Inverse of [decompose_prod]. *) val compose_prod : (name * constr) list -> constr -> constr -(** [lamn n l b] = {% $ %}[x_1:T_1]..[x_n:T_n]b{% $ %} - where {% $ %}l = [(x_n,T_n);\dots;(x_1,T_1);Gamma]{% $ %} *) +(** [lamn n l b] + @return [fun (x_1:T_1)...(x_n:T_n) => b] + where [l] is [(x_n,T_n)...(x_1,T_1)...]. *) val lamn : int -> (name * constr) list -> constr -> constr -(** [compose_lam l b] = {% $ %}[x_1:T_1]..[x_n:T_n]b{% $ %} - where {% $ %}l = [(x_n,T_n);\dots;(x_1,T_1)]{% $ %}. +(** [compose_lam l b] + @return [fun (x_1:T_1)...(x_n:T_n) => b] + where [l] is [(x_n,T_n)...(x_1,T_1)]. Inverse of [it_destLam] *) val compose_lam : (name * constr) list -> constr -> constr (** [to_lambda n l] - = {% $ %}[x_1:T_1]...[x_n:T_n]T{% $ %} - where {% $ %}l = (x_1:T_1)...(x_n:T_n)T{% $ %} *) + @return [fun (x_1:T_1)...(x_n:T_n) => T] + where [l] is [forall (x_1:T_1)...(x_n:T_n), T] *) val to_lambda : int -> constr -> constr (** [to_prod n l] - = {% $ %}(x_1:T_1)...(x_n:T_n)T{% $ %} - where {% $ %}l = [x_1:T_1]...[x_n:T_n]T{% $ %} *) + @return [forall (x_1:T_1)...(x_n:T_n), T] + where [l] is [fun (x_1:T_1)...(x_n:T_n) => T] *) val to_prod : int -> constr -> constr (** pseudo-reduction rule *) -(** [prod_appvect] {% $ %}(x1:B1;...;xn:Bn)B a1...an \rightarrow B[a1...an]{% $ %} *) +(** [prod_appvect] [forall (x1:B1;...;xn:Bn), B] [a1...an] @return [B[a1...an]] *) val prod_appvect : constr -> constr array -> constr val prod_applist : constr -> constr list -> constr diff --git a/library/nameops.mli b/library/nameops.mli index 0f1d52420..121f0ce77 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -16,7 +16,7 @@ val make_ident : string -> int option -> identifier val repr_ident : identifier -> string * int option val atompart_of_id : identifier -> string (** remove trailing digits *) -val root_of_id : identifier -> identifier (** remove trailing digits, {% $ %}'{% $ %} and {% $ %}\_{% $ %} *) +val root_of_id : identifier -> identifier (** remove trailing digits, ' and _ *) val add_suffix : identifier -> string -> identifier val add_prefix : string -> identifier -> identifier diff --git a/library/nametab.mli b/library/nametab.mli index 4303d86a3..aaef53e4a 100755 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -53,6 +53,7 @@ open Libnames The [user_name] can be for example the shortest non ambiguous [qualid] or the [full_user_name] or [identifier]. Such a function can also have a local context argument.}} + *) @@ -67,12 +68,11 @@ val error_global_constant_not_found_loc : loc -> qualid -> 'a (** {6 Register visibility of things } *) (** The visibility can be registered either - - for all suffixes not shorter then a given int -- when the - object is loaded inside a module -- or - + object is loaded inside a module -- or - for a precise suffix, when the module containing (the module containing ...) the object is opened (imported) + *) type visibility = Until of int | Exactly of int @@ -133,8 +133,8 @@ val full_name_cci : qualid -> full_path val full_name_modtype : qualid -> full_path val full_name_module : qualid -> dir_path -(** {6 ... } *) -(** Reverse lookup -- finding user names corresponding to the given +(** {6 Reverse lookup } + Finding user names corresponding to the given internal name *) (** Returns the full path bound to a global reference or syntactic -- cgit v1.2.3