diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-12-24 11:53:29 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-12-24 11:53:29 +0100 |
| commit | 6b691bbd2101fd39395c0d2135fd7c06a8915e14 (patch) | |
| tree | b04b45d1a6f42d19b1428c522d647afbad2f9b83 | |
| parent | 3e96002677226c0cdaa8f355938a76cfb37a722a (diff) | |
Imported Upstream version 8.3pl1upstream/8.3pl1
68 files changed, 2472 insertions, 470 deletions
@@ -102,3 +102,4 @@ _build plugins/*/*_mod.ml myocamlbuild_config.ml .DS_Store +.pc @@ -1,3 +1,54 @@ +Changes from V8.3 to V8.3pl1 +============================ + +Type inference, notations and implicit arguments bug fixes + +- #2448 (alpha-renaming problems with notations internally using binders) +- #2454 (pattern-matching sometimes not supporting type casts) +- fixing combined use of non-implicit and explictly-declared implicit arguments + in inductive arities +- restored support for using some ident with different scopes in notations + +Ltac and tactics bug fixes + +- #2414 (rewrite in not looking for eq_ind in the right module) +- #2433 (new "is_evar"/"has_evar" to restore support for matching evars in Ltac) +- #2453 (dependent destruction) +- loop in dependent destruction +- new "constr_eq" tactic for restoring support for term equality test in Ltac +- setoid rewrite under cases and abstraction fixed + +Coqdoc and documentation bugs + +- #2418 (wrong URLs in documentation) +- #2441 (coqdoc bug in Mergesort.v) +- #2445 (correct support for "'" character in coqdoc links to notations) +- fixed wrong use of "moduleid" instead of "module" in coqdoc html indexes +- fixing parsing of Multiplication and Division signs (unicode 0xD7 and 0xF7) + +Compilation + +- #2432 (support for compilation with camlp5 6.02.0) +- support for compilation with ocaml >= 3.09.3 restored + +Extraction + +- #2413 (prevent type-unsafe optimisations of pattern matching) +- Identifiers of a development aimed to be extracted should + avoid containing "__", since the extraction make various use of + this sub-string, leading to potential name clashes. This was + already so in V8.3, but not announced, as mentionned by #2421. + +Miscellaneous bug fixes + +- #2412 (anomaly Ploc.Exc when using Ltac Debug) +- #2419 (redundant opp_compare removed) +- #2427 (Module Functor claims Signature does not match) +- #2431 (compliance of CoqIDE use of mutexes with FreeBSD) +- #2434 (anomaly DuringSyntaxChecking with Local/Global prefixes) +- a few improvements in efficiency + + Changes from V8.2 to V8.3 ========================= @@ -41,7 +41,7 @@ WHAT DO YOU NEED ? Should you need or prefer to compile Coq V8.3 yourself, you need: - - Objective Caml version 3.10.2 or later + - Objective Caml version 3.09.3 or later (available at http://caml.inria.fr/) For Objective Caml version >= 3.10.0, you also need to install @@ -88,7 +88,7 @@ QUICK INSTALLATION PROCEDURE. INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). ================================================= -1- Check that you have the Objective Caml compiler version 3.10.2 (or later) +1- Check that you have the Objective Caml compiler version 3.09.3 (or later) installed on your computer and that "ocamlmktop" and "ocamlc" (or its native code version "ocamlc.opt") lie in a directory which is present in your $PATH environment variable. diff --git a/INSTALL.ide b/INSTALL.ide index e99002f0..2c2f86f5 100644 --- a/INSTALL.ide +++ b/INSTALL.ide @@ -23,7 +23,7 @@ On Gentoo GNU/Linux, do: Else, read the rest of this document to compile your own CoqIde. REQUIREMENT: - - OCaml >= 3.10.2 with native threads support. + - OCaml >= 3.09.3 with native threads support. - make world must succeed. - The graphical toolkit GTK+ 2.x. See http://www.gtk.org. The official supported version is at least 2.10.x. @@ -6,7 +6,7 @@ # # GNU Lesser General Public License Version 2.1 # ####################################################################### -# $Id: Makefile 13540 2010-10-13 19:53:28Z notin $ +# $Id: Makefile 13566 2010-10-19 13:22:08Z glondu $ # Makefile for Coq @@ -160,9 +160,19 @@ else stage1 $(STAGE1_TARGETS) : always $(call stage-template,1) +ifneq (,$(STAGE1_IMPLICITS)) +$(STAGE1_IMPLICITS) : always + $(call stage-template,1) +endif + stage2 $(STAGE2_TARGETS) : stage1 $(call stage-template,2) +ifneq (,$(STAGE2_IMPLICITS)) +$(STAGE2_IMPLICITS) : stage1 + $(call stage-template,2) +endif + # Nota: # - world is one of the targets in $(STAGE2_TARGETS), hence launching # "make" or "make world" leads to recursion into stage1 then stage2 diff --git a/Makefile.common b/Makefile.common index cc38980c..46bf2175 100644 --- a/Makefile.common +++ b/Makefile.common @@ -365,7 +365,7 @@ DATE=$(shell LANG=C date +"%B %Y") SOURCEDOCDIR=dev/source-doc -CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot +CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.o %.cmi %.cma %.cmxa %.a %.cmxs %.dep.ps %.dot ### Targets forwarded by Makefile to a specific stage: @@ -374,10 +374,12 @@ CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot STAGE1_TARGETS:= $(STAGE1) $(COQDEPBOOT) \ $(GENFILES) \ source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \ - $(STAGE1_ML4:.ml4=.ml4-preprocessed) %.o + $(STAGE1_ML4:.ml4=.ml4-preprocessed) + +STAGE1_IMPLICITS:= ifdef CM_STAGE1 - STAGE1_TARGETS+=$(CAML_OBJECT_PATTERNS) + STAGE1_IMPLICITS+=$(CAML_OBJECT_PATTERNS) endif ## Enumeration of targets that require being done at stage2 @@ -402,12 +404,13 @@ STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \ printers debug initplugins plugins \ world install coqide coqide-files coq coqlib \ coqlight states check init theories theories-light \ - $(DOC_TARGETS) $(VO_TARGETS) validate \ - %.vo %.glob states/% install-% %.ml4-preprocessed \ + $(DOC_TARGETS) $(VO_TARGETS) validate + +STAGE2_IMPLICITS:= %.vo %.glob states/% install-% %.ml4-preprocessed \ $(DOC_TARGET_PATTERNS) ifndef CM_STAGE1 - STAGE2_TARGETS+=$(CAML_OBJECT_PATTERNS) + STAGE2_IMPLICITS+=$(CAML_OBJECT_PATTERNS) endif diff --git a/Makefile.doc b/Makefile.doc index 4c6e209f..5a3a6a0a 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -185,15 +185,15 @@ doc/faq/html/index.html: doc/faq/FAQ.v.html ### Standard library (browsable html format) -ifeq ($(QUICK),1) +ifdef QUICK doc/stdlib/html/genindex.html: else -doc/stdlib/html/genindex.html: | $(COQDOC) $(THEORIESVO) +doc/stdlib/html/genindex.html: | $(COQDOC) $(THEORIESVO) $(PLUGINSVO) endif - rm -rf doc/stdlib/html $(MKDIR) doc/stdlib/html $(COQDOC) -q -d doc/stdlib/html --with-header doc/common/styles/html/$(HTMLSTYLE)/header.html --with-footer doc/common/styles/html/$(HTMLSTYLE)/footer.html --multi-index --html -g \ - -R theories Coq $(THEORIESVO:.vo=.v) + -R theories Coq -R plugins Coq $(THEORIESVO:.vo=.v) $(PLUGINSVO:.vo=.v) mv doc/stdlib/html/index.html doc/stdlib/html/genindex.html doc/stdlib/index-list.html: doc/stdlib/index-list.html.template doc/stdlib/make-library-index @@ -20,7 +20,7 @@ COMPILATION. distribution. If you really need to recompile under Windows, here are some indications: - 1- Install ocaml for Windows (MinGW port), at least version 3.10.2. + 1- Install ocaml for Windows (MinGW port), at least version 3.09.3. See: http://caml.inria.fr 2- Install a shell environment with at least: @@ -6,7 +6,7 @@ # ################################## -VERSION=8.3 +VERSION=8.3pl1 VOMAGIC=08300 STATEMAGIC=58300 DATE=`LANG=C date +"%B %Y"` @@ -411,12 +411,12 @@ esac CAMLVERSION=`"$bytecamlc" -version` case $CAMLVERSION in - 1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.06|3.07*|3.08*|3.09*) + 1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.06|3.07*|3.08*|3.09.[012]) echo "Your version of Objective-Caml is $CAMLVERSION." if [ "$force_caml_version" = "yes" ]; then echo "*Warning* You are compiling Coq with an outdated version of Objective-Caml." else - echo " You need Objective-Caml 3.10.2 or later." + echo " You need Objective-Caml 3.09.3 or later." echo " Configuration script failed!" exit 1 fi;; @@ -1094,4 +1094,4 @@ echo echo "*Warning* To compile the system for a new architecture" echo " don't forget to do a 'make archclean' before './configure'." -# $Id: configure 13552 2010-10-14 14:02:46Z notin $ +# $Id: configure 13740 2010-12-23 12:37:18Z notin $ diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index de1d84be..bd6f7dbf 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -97,6 +97,7 @@ \def\symmetryin{{\tt symmetryin}} \def\instantiate{{\tt instantiate}} \def\inversion{{\tt inversion}} +\def\specialize{{\tt specialize}} \def\Defined{{\tt Defined}} \def\Qed{{\tt Qed}} \def\pattern{{\tt pattern}} @@ -868,6 +869,16 @@ provide names for these variables: {\Coq} will do it anyway, but such automatic naming decreases legibility and robustness. +\Question{My goal contains an universally quantified statement, how can I use it?} + +If the universally quantified assumption matches the goal you can +use the {\apply} tactic. If it is an equation you can use the +{\rewrite} tactic. Otherwise you can use the {\specialize} tactic +to instantiate the quantified variables with terms. The variant +{\tt assert(Ht := H t)} makes a copy of assumption {\tt H} before +instantiating it. + + \Question{My goal is an existential, how can I prove it?} Use some theorem or assumption or exhibit the witness using the {\existstac} tactic. diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index 7bd4f352..f427609f 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -10,7 +10,7 @@ \label{typeclasses} \begin{flushleft} - \em The status of Type Classes is (extremely) experimental. + \em The status of Type Classes is experimental. \end{flushleft} This chapter presents a quick reference of the commands related to type @@ -128,9 +128,7 @@ particular support for type classes: methods. In the example above, \texttt{A} and \texttt{eqa} should be set maximally implicit. \item They support implicit quantification on partialy applied type - classes (\S \ref{implicit-generalization}). - Any argument not given as part of a type class binder will be - automatically generalized. + classes. \item They also support implicit quantification on superclasses (\S \ref{classes:superclasses}) \end{itemize} @@ -143,6 +141,19 @@ Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y). Here \texttt{A} is implicitly generalized, and the resulting function is equivalent to the one above. +The parsing of generalized type-class binders is different from regular +binders: +\begin{itemize} +\item Implicit arguments of the class type are ignored. +\item Superclasses arguments are automatically generalized. +\item Any remaining arguments not given as part of a type class binder + will be automatically generalized. In other words, the rightmost + parameters are automatically generalized if not mentionned. +\end{itemize} + +One can switch off this special treatment using the $!$ mark in front of +the class name (see example below). + \asection{Parameterized Instances} One can declare parameterized instances as in \Haskell simply by giving @@ -231,9 +242,9 @@ Definition le_eqb `{Ord A} (x y : A) := andb (le x y) (le y x). \end{coq_example*} In some cases, to be able to specify sharing of structures, one may want to give -explicitly the superclasses. It is is possible to do it directly in regular -binders, and using the \texttt{!} modifier in class binders. For -example: +explicitly the superclasses. It is possible to do it directly in regular +generalized binders, and using the \texttt{!} modifier in class +binders. For example: \begin{coq_example*} Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) := andb (le x y) (neqb x y). diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 9efa7048..b8a893d5 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1622,7 +1622,7 @@ the generalized variables. Inside implicit generalization delimiters, free variables in the current context are automatically quantified using a product or a lambda abstraction to generate a closed term. In the following statement for example, the variables \texttt{n} -and \texttt{m} are autamatically generalized and become explicit +and \texttt{m} are automatically generalized and become explicit arguments of the lemma as we are using \verb|`( )|: \begin{coq_example} @@ -1638,7 +1638,7 @@ generalizations when mistyping identifiers. There are three variants of the command: \begin{quote} -{\tt Generalizable (All|No) Variable(s)? ({\ident$_1$ \ident$_n$})?.} +{\tt (Global)? Generalizable (All|No) Variable(s)? ({\ident$_1$ \ident$_n$})?.} \end{quote} \begin{Variants} diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex index 04830531..5d9c8c16 100644 --- a/doc/refman/RefMan-ide.tex +++ b/doc/refman/RefMan-ide.tex @@ -261,26 +261,32 @@ CONTROL and the SHIFT keys, and type the hexadecimal code of the symbol required, for example \verb|2200| for the $\forall$ symbol. A list of symbol codes is available at \url{http://www.unicode.org}. -This method obviously doesn't scale, that's why the preferred alternative is to -use an Input Method Editor. On POSIX systems (Linux distros, BSD variants and -MacOS X), you can use \texttt{uim} version 1.6 or later which provides a \LaTeX{}-style -input method. - -To configure \texttt{uim}, execute \texttt{uim-pref-gtk} as your regular user. -In the "Global Settings" group set the default Input Method to "ELatin" (don't -forget to tick the checkbox "Specify default IM"). In the "ELatin" group set the -layout to "TeX", and remember the content of the "[ELatin] on" field (by default -"<Control>\"). You can now execute CoqIDE with the following commands (assuming -you use a Bourne-style shell): +This method obviously doesn't scale, that's why the preferred +alternative is to use an Input Method Editor. On POSIX systems (Linux +distributions, BSD variants and MacOS X), you can use \texttt{uim} to +support \LaTeX{}-style edition and, if using X Windows, you can also use +the XCompose method (XIM). How to use \texttt{uim} is documented below. + +If you have \texttt{uim} 1.5.x, first manually copy the files located +in directory {\tt ide/uim} of the Coq source distribution to the +{\tt uim} directory of input methods which typically is {\tt + /usr/share/uim}. Execute {\tt uim-module-manager -{-}register + coqide}. Then, execute \texttt{uim-pref-gtk} as regular user and set +the default Input Method to "CoqIDE" in the "Global Settings" group +(don't forget to tick the checkbox "Specify default IM"; you may also +have to first edit the set of "Enabled input method" to add CoqIDE to +the set). You can now execute CoqIDE with the following commands +(assuming you use a Bourne-style shell): \begin{verbatim} $ export GTK_IM_MODULE=uim $ coqide \end{verbatim} -Activate the ELatin Input Method with Ctrl-\textbackslash, then type the -sequence "\verb=\Gamma=". You will see the sequence being -replaced by $\Gamma$ as soon as you type the second "a". +If you then type the sequence "\verb=\Gamma=", you will see the sequence being +replaced by $\Gamma$ as soon as you type the second "a". + +If you have \texttt{uim} 1.6.x, the \LaTeX{} input method is built-in. You just have to execute \texttt{uim-pref-gtk} and choose "ELatin" as default Input Method in the "Global Settings". Then, in the "ELatin" group set the layout to "TeX", and remember the content of the "[ELatin] on" field (by default "<Control>$\backslash$"). Proceed then as above. \subsection[Character encoding for saved files]{Character encoding for saved files\label{sec:coqidecharencoding}} @@ -314,7 +320,7 @@ or -% $Id: RefMan-ide.tex 13477 2010-09-30 16:50:00Z vgross $ +% $Id: RefMan-ide.tex 13701 2010-12-10 07:48:30Z herbelin $ %%% Local Variables: %%% mode: latex diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index b82cdc2d..450d3b2d 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -989,6 +989,36 @@ Assumptions} (see Section~\ref{PrintAssumptions}). Admitted subgoals have names of the form {\ident}\texttt{\_admitted} possibly followed by a number. +\subsection{\tt constr\_eq \term$_1$ \term$_2$ +\tacindex{constr\_eq} +\label{constreq}} + +This tactic applies to any goal. It checks whether its arguments are +equal modulo alpha conversion and casts. + +\ErrMsg \errindex{Not equal} + +\subsection{\tt is\_evar \term +\tacindex{is\_evar} +\label{isevar}} + +This tactic applies to any goal. It checks whether its argument is an +existential variable. Existential variables are uninstantiated +variables generated by e.g. {\tt eapply} (see Section~\ref{apply}). + +\ErrMsg \errindex{Not an evar} + +\subsection{\tt has\_evar \term +\tacindex{has\_evar} +\label{hasevar}} + +This tactic applies to any goal. It checks whether its argument has an +existential variable as a subterm. Unlike {\tt context} patterns +combined with {\tt is\_evar}, this tactic scans all subterms, +including those under binders. + +\ErrMsg \errindex{No evars} + \subsection{Bindings list \index{Binding list} \label{Binding-list}} @@ -3917,7 +3947,7 @@ where {\sl hint\_definition} is one of the following expressions: \begin{quotation} \begin{verbatim} -Hint Extern 4 ~(?=?) => discriminate. +Hint Extern 4 (~(_ = _)) => discriminate. \end{verbatim} \end{quotation} @@ -4294,7 +4324,7 @@ Chapter~\ref{TacticLanguage} gives examples of more complex user-defined tactics. -% $Id: RefMan-tac.tex 13344 2010-07-28 15:04:36Z msozeau $ +% $Id: RefMan-tac.tex 13659 2010-11-29 11:09:07Z glondu $ %%% Local Variables: %%% mode: latex diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex index 63c35548..723295bf 100755 --- a/doc/tutorial/Tutorial.tex +++ b/doc/tutorial/Tutorial.tex @@ -1574,4 +1574,4 @@ with \Coq, in order to acquaint yourself with various proof techniques. \end{document} -% $Id: Tutorial.tex 13548 2010-10-14 12:35:43Z notin $ +% $Id: Tutorial.tex 13547 2010-10-14 12:35:00Z notin $ diff --git a/ide/coqide.ml b/ide/coqide.ml index 08452fe2..fdf33c39 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqide.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: coqide.ml 13708 2010-12-13 14:49:29Z gmelquio $ *) open Preferences open Vernacexpr @@ -251,27 +251,31 @@ let break () = end let do_if_not_computing text f x = - if Mutex.try_lock coq_computing then - let threaded_task () = - prerr_endline "Getting lock"; - try - f x; - prerr_endline "Releasing lock"; - Mutex.unlock coq_computing; - with e -> - prerr_endline "Releasing lock (on error)"; - Mutex.unlock coq_computing; - raise e - in - prerr_endline ("Launching thread " ^ text); - ignore (Glib.Timeout.add ~ms:300 ~callback: - (fun () -> if Mutex.try_lock coq_computing - then (Mutex.unlock coq_computing; false) - else (pbar#pulse (); true))); - ignore (Thread.create threaded_task ()) - else - prerr_endline - "Discarded order (computations are ongoing)" + let threaded_task () = + (* Beware: mutexes must be locked and unlocked in the same thread + on at least FreeBSD (see bug #2431) *) + if Mutex.try_lock coq_computing then + begin + prerr_endline "Getting lock"; + try + f x; + prerr_endline "Releasing lock"; + Mutex.unlock coq_computing; + with e -> + prerr_endline "Releasing lock (on error)"; + Mutex.unlock coq_computing; + raise e + end + else + prerr_endline + "Discarded order (computations are ongoing)" + in + prerr_endline ("Launching thread " ^ text); + ignore (Glib.Timeout.add ~ms:300 ~callback: + (fun () -> if Mutex.try_lock coq_computing + then (Mutex.unlock coq_computing; false) + else (pbar#pulse (); true))); + ignore (Thread.create threaded_task ()) (* XXX - 1 appel *) let kill_input_view i = @@ -282,15 +286,59 @@ let kill_input_view i = v.proof_view#destroy (); v.message_view#destroy (); session_notebook#remove_page i + +let warning msg = + GToolbox.message_box ~title:"Warning" + ~icon:(let img = GMisc.image () in + img#set_stock `DIALOG_WARNING; + img#set_icon_size `DIALOG; + img#coerce) + msg + (* (* XXX - beaucoups d'appels, a garder *) let get_current_view = focused_session *) let remove_current_view_page () = - let c = session_notebook#current_page in - kill_input_view c - + let do_remove () = + let c = session_notebook#current_page in + kill_input_view c + in + let current = session_notebook#current_term in + if current.script#buffer#modified then + match GToolbox.question_box ~title:"Close" + ~buttons:["Save Buffer and Close"; + "Close without Saving"; + "Don't Close"] + ~default:0 + ~icon:(let img = GMisc.image () in + img#set_stock `DIALOG_WARNING; + img#set_icon_size `DIALOG; + img#coerce) + "This buffer has unsaved modifications" + with + | 1 -> + begin match current.analyzed_view#filename with + | None -> + begin match select_file_for_save ~title:"Save file" () with + | None -> () + | Some f -> + if current.analyzed_view#save_as f then begin + flash_info ("File " ^ f ^ " saved") ; + do_remove () + end else + warning ("Save Failed (check if " ^ f ^ " is writable)") + end + | Some f -> + if current.analyzed_view#save f then begin + flash_info ("File " ^ f ^ " saved") ; + do_remove () + end else + warning ("Save Failed (check if " ^ f ^ " is writable)") + end + | 2 -> do_remove () + | _ -> () (* Reset this to None on page change ! *) let (last_completion:(string*int*int*bool) option ref) = ref None @@ -383,14 +431,6 @@ let activate_input i = set_active_view i; prerr_endline "exiting activate_input" -let warning msg = - GToolbox.message_box ~title:"Warning" - ~icon:(let img = GMisc.image () in - img#set_stock `DIALOG_WARNING; - img#set_icon_size `DIALOG; - img#coerce) - msg - let apply_tag (buffer:GText.buffer) orig off_conv from upto sort = let conv_and_apply start stop tag = let start = orig#forward_chars (off_conv from) in diff --git a/ide/uim/coqide-custom.scm b/ide/uim/coqide-custom.scm new file mode 100644 index 00000000..622f5063 --- /dev/null +++ b/ide/uim/coqide-custom.scm @@ -0,0 +1,99 @@ +;;; coqide-custom.scm -- customization variables for coqide.scm +;;; +;;; Copyright (c) 2003-2009 uim Project http://code.google.com/p/uim/ +;;; +;;; All rights reserved. +;;; +;;; Redistribution and use in source and binary forms, with or without +;;; modification, are permitted provided that the following conditions +;;; are met: +;;; 1. Redistributions of source code must retain the above copyright +;;; notice, this list of conditions and the following disclaimer. +;;; 2. Redistributions in binary form must reproduce the above copyright +;;; notice, this list of conditions and the following disclaimer in the +;;; documentation and/or other materials provided with the distribution. +;;; 3. Neither the name of authors nor the names of its contributors +;;; may be used to endorse or promote products derived from this software +;;; without specific prior written permission. +;;; +;;; THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS ``AS IS'' AND +;;; ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +;;; IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE +;;; ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS OR CONTRIBUTORS BE LIABLE +;;; FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +;;; DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS +;;; OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) +;;; HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT +;;; LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY +;;; OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF +;;; SUCH DAMAGE. +;;;; + +(require "i18n.scm") + +(define coqide-im-name-label (N_ "CoqIDE")) +(define coqide-im-short-desc (N_ "Emacs-style Latin characters input")) +(define coqide-im-long-desc (N_ "An input method for entering Latin letters used in European languages with the key translations adopted in Emacs.")) + +(define-custom-group 'coqide + coqide-im-name-label + coqide-im-short-desc) + +(define-custom-group 'coqide-properties + (N_ "Properties") + (N_ "long description will be here.")) + +(define-custom 'coqide-rules 'coqide-rules-latin-ltx + '(coqide coqide-properties) + (list 'choice + (list 'coqide-rules-latin-ltx + (N_ "TeX") + (N_ "long description will be here."))) + (N_ "Latin characters keyboard layout") + (N_ "long description will be here.")) + +(custom-add-hook 'coqide-rules + 'custom-set-hooks + (lambda () + (map (lambda (lc) + (let ((new-rkc (rk-context-new + (symbol-value coqide-rules) #f #f))) + (coqide-context-flush lc) + (coqide-update-preedit lc) + (coqide-context-set-rkc! lc new-rkc))) + coqide-context-list))) + +;; For VI users. +(define-custom 'coqide-esc-turns-off? #f + '(coqide coqide-properties) + '(boolean) + (N_ "ESC turns off composition mode (for vi users)") + (N_ "long description will be here.")) + + +(define-custom-group 'coqide-keys + (N_ "CoqIDE key bindings") + (N_ "long description will be here.")) + +(define-custom 'coqide-on-key '("<Control>\\") + '(coqide coqide-keys) + '(key) + (N_ "CoqIDE on") + (N_ "long description will be here")) + +(define-custom 'coqide-off-key '("<Control>\\") + '(coqide coqide-keys) + '(key) + (N_ "CoqIDE off") + (N_ "long description will be here")) + +(define-custom 'coqide-backspace-key '(generic-backspace-key) + '(coqide coqide-keys) + '(key) + (N_ "CoqIDE backspace") + (N_ "long description will be here")) + +;; Local Variables: +;; mode: scheme +;; coding: utf-8 +;; End: diff --git a/ide/uim/coqide-rules.scm b/ide/uim/coqide-rules.scm new file mode 100644 index 00000000..c483c88b --- /dev/null +++ b/ide/uim/coqide-rules.scm @@ -0,0 +1,1142 @@ +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; v ; The Coq Proof Assistant / The Coq Development Team ;; +;; <O___,, ; INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 ;; +;; \VV/ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; // ; This file is distributed under the terms of the ;; +;; ; GNU Lesser General Public License Version 2.1 ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;;; coqide-rules.scm -- key sequence tables for coqide.scm + +;; Copyright (c) 2003-2009 uim Project http://code.google.com/p/uim/ +;; +;; All rights reserved. + +;; The translation tables in this file were derived from +;; the emacs-lisp source files latin-pre.el, latin-post.el, latin-alt.el +;; included in GNU Emacs. The following is the original copyright notice +;; therein, with the name GNU Emacs replaced by "this program". + +;; Copyright (C) 1997, 1998, 1999, 2000, 2001, 2002, 2003, 2004, 2005, +;; 2006, 2007 +;; Free Software Foundation, Inc. +;; Copyright (C) 1997, 1998, 1999, 2000, 2001, 2002, 2003, 2004, 2005, +;; 2006, 2007 +;; National Institute of Advanced Industrial Science and Technology (AIST) +;; Registration Number H14PRO021 + +;; This program is free software; you can redistribute it and/or modify +;; it under the terms of the GNU General Public License as published by +;; the Free Software Foundation; either version 2, or (at your option) +;; any later version. + +;; This program is distributed in the hope that it will be useful, +;; but WITHOUT ANY WARRANTY; without even the implied warranty of +;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +;; GNU General Public License for more details. + +;; You should have received a copy of the GNU General Public License +;; along with this program. If not, write to the +;; Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, +;; Boston, MA 02110-1301, USA. + +;;; Commentary: + +;; Key translation maps were originally copied from iso-acc.el. +;; latin-1-prefix: extra special characters added, adapted from the vim +;; digraphs (from J.H.M.Dassen <jdassen@wi.leidenuniv.nl>) +;; by R.F. Smith <rsmith@xs4all.nl> +;; +;; polish-slash: +;; Author: Włodek Bzyl <matwb@univ.gda.pl> +;; Maintainer: Włodek Bzyl <matwb@univ.gda.pl> +;; +;; latin-[89]-prefix: Dave Love <fx@gnu.org> + +(define coqide-rules-latin-ltx '( +((("!" "`")) ("¡")) +((("\\" "p" "o" "u" "n" "d" "s")) ("£")) +((("\\" "S")) ("§")) +((("\\" "\"" "{" "}")) ("¨")) +((("\\" "c" "o" "p" "y" "r" "i" "g" "h" "t")) ("©")) +((("$" "^" "a" "$")) ("ª")) +((("\\" "=" "{" "}")) ("¯")) +((("$" "\\" "p" "m" "$")) ("±")) +((("\\" "p" "m")) ("±")) +((("$" "^" "2" "$")) ("²")) +((("$" "^" "3" "$")) ("³")) +((("\\" "'" "{" "}")) ("´")) +((("\\" "P")) ("¶")) +((("$" "\\" "c" "d" "o" "t" "$")) ("·")) +((("\\" "c" "d" "o" "t")) ("·")) +((("\\" "c" "{" "}")) ("¸")) +((("$" "^" "1" "$")) ("¹")) +((("$" "^" "o" "$")) ("º")) +((("?" "`")) ("¿")) +((("\\" "`" "{" "A" "}")) ("À")) +((("\\" "`" "A")) ("À")) +((("\\" "'" "{" "A" "}")) ("Á")) +((("\\" "'" "A")) ("Á")) +((("\\" "^" "{" "A" "}")) ("Â")) +((("\\" "^" "A")) ("Â")) +((("\\" "~" "{" "A" "}")) ("Ã")) +((("\\" "~" "A")) ("Ã")) +((("\\" "\"" "{" "A" "}")) ("Ä")) +((("\\" "\"" "A")) ("Ä")) +((("\\" "k" "{" "A" "}")) ("Ą")) +((("\\" "A" "A")) ("Å")) +((("\\" "A" "E")) ("Æ")) +((("\\" "c" "{" "C" "}")) ("Ç")) +((("\\" "c" "C")) ("Ç")) +((("\\" "`" "{" "E" "}")) ("È")) +((("\\" "`" "E")) ("È")) +((("\\" "'" "{" "E" "}")) ("É")) +((("\\" "'" "E")) ("É")) +((("\\" "^" "{" "E" "}")) ("Ê")) +((("\\" "^" "E")) ("Ê")) +((("\\" "\"" "{" "E" "}")) ("Ë")) +((("\\" "\"" "E")) ("Ë")) +((("\\" "k" "{" "E" "}")) ("Ę")) +((("\\" "`" "{" "I" "}")) ("Ì")) +((("\\" "`" "I")) ("Ì")) +((("\\" "'" "{" "I" "}")) ("Í")) +((("\\" "'" "I")) ("Í")) +((("\\" "^" "{" "I" "}")) ("Î")) +((("\\" "^" "I")) ("Î")) +((("\\" "\"" "{" "I" "}")) ("Ï")) +((("\\" "\"" "I")) ("Ï")) +((("\\" "k" "{" "I" "}")) ("Į")) +((("\\" "~" "{" "N" "}")) ("Ñ")) +((("\\" "~" "N")) ("Ñ")) +((("\\" "`" "{" "O" "}")) ("Ò")) +((("\\" "`" "O")) ("Ò")) +((("\\" "'" "{" "O" "}")) ("Ó")) +((("\\" "'" "O")) ("Ó")) +((("\\" "^" "{" "O" "}")) ("Ô")) +((("\\" "^" "O")) ("Ô")) +((("\\" "~" "{" "O" "}")) ("Õ")) +((("\\" "~" "O")) ("Õ")) +((("\\" "\"" "{" "O" "}")) ("Ö")) +((("\\" "\"" "O")) ("Ö")) +((("\\" "k" "{" "O" "}")) ("Ǫ")) +((("$" "\\" "t" "i" "m" "e" "s" "$")) ("×")) +((("\\" "t" "i" "m" "e" "s")) ("×")) +((("\\" "O")) ("Ø")) +((("\\" "`" "{" "U" "}")) ("Ù")) +((("\\" "`" "U")) ("Ù")) +((("\\" "'" "{" "U" "}")) ("Ú")) +((("\\" "'" "U")) ("Ú")) +((("\\" "^" "{" "U" "}")) ("Û")) +((("\\" "^" "U")) ("Û")) +((("\\" "\"" "{" "U" "}")) ("Ü")) +((("\\" "\"" "U")) ("Ü")) +((("\\" "k" "{" "U" "}")) ("Ų")) +((("\\" "'" "{" "Y" "}")) ("Ý")) +((("\\" "'" "Y")) ("Ý")) +((("\\" "s" "s")) ("ß")) +((("\\" "`" "{" "a" "}")) ("à")) +((("\\" "`" "a")) ("à")) +((("\\" "'" "{" "a" "}")) ("á")) +((("\\" "'" "a")) ("á")) +((("\\" "^" "{" "a" "}")) ("â")) +((("\\" "^" "a")) ("â")) +((("\\" "~" "{" "a" "}")) ("ã")) +((("\\" "~" "a")) ("ã")) +((("\\" "\"" "{" "a" "}")) ("ä")) +((("\\" "\"" "a")) ("ä")) +((("\\" "k" "{" "a" "}")) ("ą")) +((("\\" "a" "a")) ("å")) +((("\\" "a" "e")) ("æ")) +((("\\" "c" "{" "c" "}")) ("ç")) +((("\\" "c" "c")) ("ç")) +((("\\" "`" "{" "e" "}")) ("è")) +((("\\" "`" "e")) ("è")) +((("\\" "'" "{" "e" "}")) ("é")) +((("\\" "'" "e")) ("é")) +((("\\" "^" "{" "e" "}")) ("ê")) +((("\\" "^" "e")) ("ê")) +((("\\" "\"" "{" "e" "}")) ("ë")) +((("\\" "\"" "e")) ("ë")) +((("\\" "k" "{" "e" "}")) ("ę")) +((("\\" "`" "{" "\\" "i" "}")) ("ì")) +((("\\" "`" "i")) ("ì")) +((("\\" "'" "{" "\\" "i" "}")) ("í")) +((("\\" "'" "i")) ("í")) +((("\\" "^" "{" "\\" "i" "}")) ("î")) +((("\\" "^" "i")) ("î")) +((("\\" "\"" "{" "\\" "i" "}")) ("ï")) +((("\\" "\"" "i")) ("ï")) +((("\\" "k" "{" "i" "}")) ("į")) +((("\\" "~" "{" "n" "}")) ("ñ")) +((("\\" "~" "n")) ("ñ")) +((("\\" "`" "{" "o" "}")) ("ò")) +((("\\" "`" "o")) ("ò")) +((("\\" "'" "{" "o" "}")) ("ó")) +((("\\" "'" "o")) ("ó")) +((("\\" "^" "{" "o" "}")) ("ô")) +((("\\" "^" "o")) ("ô")) +((("\\" "~" "{" "o" "}")) ("õ")) +((("\\" "~" "o")) ("õ")) +((("\\" "\"" "{" "o" "}")) ("ö")) +((("\\" "\"" "o")) ("ö")) +((("\\" "k" "{" "o" "}")) ("ǫ")) +((("$" "\\" "d" "i" "v" "$")) ("÷")) +((("\\" "d" "i" "v")) ("÷")) +((("\\" "o")) ("ø")) +((("\\" "`" "{" "u" "}")) ("ù")) +((("\\" "`" "u")) ("ù")) +((("\\" "'" "{" "u" "}")) ("ú")) +((("\\" "'" "u")) ("ú")) +((("\\" "^" "{" "u" "}")) ("û")) +((("\\" "^" "u")) ("û")) +((("\\" "\"" "{" "u" "}")) ("ü")) +((("\\" "\"" "u")) ("ü")) +((("\\" "k" "{" "u" "}")) ("ų")) +((("\\" "'" "{" "y" "}")) ("ý")) +((("\\" "'" "y")) ("ý")) +((("\\" "\"" "{" "y" "}")) ("ÿ")) +((("\\" "\"" "y")) ("ÿ")) +((("\\" "=" "{" "A" "}")) ("Ā")) +((("\\" "=" "A")) ("Ā")) +((("\\" "=" "{" "a" "}")) ("ā")) +((("\\" "=" "a")) ("ā")) +((("\\" "u" "{" "A" "}")) ("Ă")) +((("\\" "u" "A")) ("Ă")) +((("\\" "u" "{" "a" "}")) ("ă")) +((("\\" "u" "a")) ("ă")) +((("\\" "'" "{" "C" "}")) ("Ć")) +((("\\" "'" "C")) ("Ć")) +((("\\" "'" "{" "c" "}")) ("ć")) +((("\\" "'" "c")) ("ć")) +((("\\" "^" "{" "C" "}")) ("Ĉ")) +((("\\" "^" "C")) ("Ĉ")) +((("\\" "^" "{" "c" "}")) ("ĉ")) +((("\\" "^" "c")) ("ĉ")) +((("\\" "." "{" "C" "}")) ("Ċ")) +((("\\" "." "C")) ("Ċ")) +((("\\" "." "{" "c" "}")) ("ċ")) +((("\\" "." "c")) ("ċ")) +((("\\" "v" "{" "C" "}")) ("Č")) +((("\\" "v" "C")) ("Č")) +((("\\" "v" "{" "c" "}")) ("č")) +((("\\" "v" "c")) ("č")) +((("\\" "v" "{" "D" "}")) ("Ď")) +((("\\" "v" "D")) ("Ď")) +((("\\" "v" "{" "d" "}")) ("ď")) +((("\\" "v" "d")) ("ď")) +((("\\" "=" "{" "E" "}")) ("Ē")) +((("\\" "=" "E")) ("Ē")) +((("\\" "=" "{" "e" "}")) ("ē")) +((("\\" "=" "e")) ("ē")) +((("\\" "u" "{" "E" "}")) ("Ĕ")) +((("\\" "u" "E")) ("Ĕ")) +((("\\" "u" "{" "e" "}")) ("ĕ")) +((("\\" "u" "e")) ("ĕ")) +((("\\" "." "{" "E" "}")) ("Ė")) +((("\\" "." "E")) ("Ė")) +((("\\" "e" "{" "e" "}")) ("ė")) +((("\\" "e" "e")) ("ė")) +((("\\" "v" "{" "E" "}")) ("Ě")) +((("\\" "v" "E")) ("Ě")) +((("\\" "v" "{" "e" "}")) ("ě")) +((("\\" "v" "e")) ("ě")) +((("\\" "^" "{" "G" "}")) ("Ĝ")) +((("\\" "^" "G")) ("Ĝ")) +((("\\" "^" "{" "g" "}")) ("ĝ")) +((("\\" "^" "g")) ("ĝ")) +((("\\" "u" "{" "G" "}")) ("Ğ")) +((("\\" "u" "G")) ("Ğ")) +((("\\" "u" "{" "g" "}")) ("ğ")) +((("\\" "u" "g")) ("ğ")) +((("\\" "." "{" "G" "}")) ("Ġ")) +((("\\" "." "G")) ("Ġ")) +((("\\" "." "{" "g" "}")) ("ġ")) +((("\\" "." "g")) ("ġ")) +((("\\" "c" "{" "G" "}")) ("Ģ")) +((("\\" "c" "G")) ("Ģ")) +((("\\" "c" "{" "g" "}")) ("ģ")) +((("\\" "c" "g")) ("ģ")) +((("\\" "^" "{" "H" "}")) ("Ĥ")) +((("\\" "^" "H")) ("Ĥ")) +((("\\" "^" "{" "h" "}")) ("ĥ")) +((("\\" "^" "h")) ("ĥ")) +((("\\" "~" "{" "I" "}")) ("Ĩ")) +((("\\" "~" "I")) ("Ĩ")) +((("\\" "~" "{" "\\" "i" "}")) ("ĩ")) +((("\\" "~" "i")) ("ĩ")) +((("\\" "=" "{" "I" "}")) ("Ī")) +((("\\" "=" "I")) ("Ī")) +((("\\" "=" "{" "\\" "i" "}")) ("ī")) +((("\\" "=" "i")) ("ī")) +((("\\" "u" "{" "I" "}")) ("Ĭ")) +((("\\" "u" "I")) ("Ĭ")) +((("\\" "u" "{" "\\" "i" "}")) ("ĭ")) +((("\\" "u" "i")) ("ĭ")) +((("\\" "." "{" "I" "}")) ("İ")) +((("\\" "." "I")) ("İ")) +((("\\" "i")) ("ı")) +((("\\" "^" "{" "J" "}")) ("Ĵ")) +((("\\" "^" "J")) ("Ĵ")) +((("\\" "^" "{" "\\" "j" "}")) ("ĵ")) +((("\\" "^" "j")) ("ĵ")) +((("\\" "c" "{" "K" "}")) ("Ķ")) +((("\\" "c" "K")) ("Ķ")) +((("\\" "c" "{" "k" "}")) ("ķ")) +((("\\" "c" "k")) ("ķ")) +((("\\" "'" "{" "L" "}")) ("Ĺ")) +((("\\" "'" "L")) ("Ĺ")) +((("\\" "'" "{" "l" "}")) ("ĺ")) +((("\\" "'" "l")) ("ĺ")) +((("\\" "c" "{" "L" "}")) ("Ļ")) +((("\\" "c" "L")) ("Ļ")) +((("\\" "c" "{" "l" "}")) ("ļ")) +((("\\" "c" "l")) ("ļ")) +((("\\" "L")) ("Ł")) +((("\\" "l")) ("ł")) +((("\\" "'" "{" "N" "}")) ("Ń")) +((("\\" "'" "N")) ("Ń")) +((("\\" "'" "{" "n" "}")) ("ń")) +((("\\" "'" "n")) ("ń")) +((("\\" "c" "{" "N" "}")) ("Ņ")) +((("\\" "c" "N")) ("Ņ")) +((("\\" "c" "{" "n" "}")) ("ņ")) +((("\\" "c" "n")) ("ņ")) +((("\\" "v" "{" "N" "}")) ("Ň")) +((("\\" "v" "N")) ("Ň")) +((("\\" "v" "{" "n" "}")) ("ň")) +((("\\" "v" "n")) ("ň")) +((("\\" "=" "{" "O" "}")) ("Ō")) +((("\\" "=" "O")) ("Ō")) +((("\\" "=" "{" "o" "}")) ("ō")) +((("\\" "=" "o")) ("ō")) +((("\\" "u" "{" "O" "}")) ("Ŏ")) +((("\\" "u" "O")) ("Ŏ")) +((("\\" "u" "{" "o" "}")) ("ŏ")) +((("\\" "u" "o")) ("ŏ")) +((("\\" "H" "{" "O" "}")) ("Ő")) +((("\\" "H" "O")) ("Ő")) +((("\\" "U" "{" "o" "}")) ("ő")) +((("\\" "U" "o")) ("ő")) +((("\\" "O" "E")) ("Œ")) +((("\\" "o" "e")) ("œ")) +((("\\" "'" "{" "R" "}")) ("Ŕ")) +((("\\" "'" "R")) ("Ŕ")) +((("\\" "'" "{" "r" "}")) ("ŕ")) +((("\\" "'" "r")) ("ŕ")) +((("\\" "c" "{" "R" "}")) ("Ŗ")) +((("\\" "c" "R")) ("Ŗ")) +((("\\" "c" "{" "r" "}")) ("ŗ")) +((("\\" "c" "r")) ("ŗ")) +((("\\" "v" "{" "R" "}")) ("Ř")) +((("\\" "v" "R")) ("Ř")) +((("\\" "v" "{" "r" "}")) ("ř")) +((("\\" "v" "r")) ("ř")) +((("\\" "'" "{" "S" "}")) ("Ś")) +((("\\" "'" "S")) ("Ś")) +((("\\" "'" "{" "s" "}")) ("ś")) +((("\\" "'" "s")) ("ś")) +((("\\" "^" "{" "S" "}")) ("Ŝ")) +((("\\" "^" "S")) ("Ŝ")) +((("\\" "^" "{" "s" "}")) ("ŝ")) +((("\\" "^" "s")) ("ŝ")) +((("\\" "c" "{" "S" "}")) ("Ş")) +((("\\" "c" "S")) ("Ş")) +((("\\" "c" "{" "s" "}")) ("ş")) +((("\\" "c" "s")) ("ş")) +((("\\" "v" "{" "S" "}")) ("Š")) +((("\\" "v" "S")) ("Š")) +((("\\" "v" "{" "s" "}")) ("š")) +((("\\" "v" "s")) ("š")) +((("\\" "c" "{" "T" "}")) ("Ţ")) +((("\\" "c" "T")) ("Ţ")) +((("\\" "c" "{" "t" "}")) ("ţ")) +((("\\" "c" "t")) ("ţ")) +((("\\" "v" "{" "T" "}")) ("Ť")) +((("\\" "v" "T")) ("Ť")) +((("\\" "v" "{" "t" "}")) ("ť")) +((("\\" "v" "t")) ("ť")) +((("\\" "~" "{" "U" "}")) ("Ũ")) +((("\\" "~" "U")) ("Ũ")) +((("\\" "~" "{" "u" "}")) ("ũ")) +((("\\" "~" "u")) ("ũ")) +((("\\" "=" "{" "U" "}")) ("Ū")) +((("\\" "=" "U")) ("Ū")) +((("\\" "=" "{" "u" "}")) ("ū")) +((("\\" "=" "u")) ("ū")) +((("\\" "u" "{" "U" "}")) ("Ŭ")) +((("\\" "u" "U")) ("Ŭ")) +((("\\" "u" "{" "u" "}")) ("ŭ")) +((("\\" "u" "u")) ("ŭ")) +((("\\" "H" "{" "U" "}")) ("Ű")) +((("\\" "H" "U")) ("Ű")) +((("\\" "H" "{" "u" "}")) ("ű")) +((("\\" "H" "u")) ("ű")) +((("\\" "^" "{" "W" "}")) ("Ŵ")) +((("\\" "^" "W")) ("Ŵ")) +((("\\" "^" "{" "w" "}")) ("ŵ")) +((("\\" "^" "w")) ("ŵ")) +((("\\" "^" "{" "Y" "}")) ("Ŷ")) +((("\\" "^" "Y")) ("Ŷ")) +((("\\" "^" "{" "y" "}")) ("ŷ")) +((("\\" "^" "y")) ("ŷ")) +((("\\" "\"" "{" "Y" "}")) ("Ÿ")) +((("\\" "\"" "Y")) ("Ÿ")) +((("\\" "'" "{" "Z" "}")) ("Ź")) +((("\\" "'" "Z")) ("Ź")) +((("\\" "'" "{" "z" "}")) ("ź")) +((("\\" "'" "z")) ("ź")) +((("\\" "." "{" "Z" "}")) ("Ż")) +((("\\" "." "Z")) ("Ż")) +((("\\" "." "{" "z" "}")) ("ż")) +((("\\" "." "z")) ("ż")) +((("\\" "v" "{" "Z" "}")) ("Ž")) +((("\\" "v" "Z")) ("Ž")) +((("\\" "v" "{" "z" "}")) ("ž")) +((("\\" "v" "z")) ("ž")) +((("\\" "v" "{" "A" "}")) ("Ǎ")) +((("\\" "v" "A")) ("Ǎ")) +((("\\" "v" "{" "a" "}")) ("ǎ")) +((("\\" "v" "a")) ("ǎ")) +((("\\" "v" "{" "I" "}")) ("Ǐ")) +((("\\" "v" "I")) ("Ǐ")) +((("\\" "v" "{" "\\" "i" "}")) ("ǐ")) +((("\\" "v" "i")) ("ǐ")) +((("\\" "v" "{" "O" "}")) ("Ǒ")) +((("\\" "v" "O")) ("Ǒ")) +((("\\" "v" "{" "o" "}")) ("ǒ")) +((("\\" "v" "o")) ("ǒ")) +((("\\" "v" "{" "U" "}")) ("Ǔ")) +((("\\" "v" "U")) ("Ǔ")) +((("\\" "v" "{" "u" "}")) ("ǔ")) +((("\\" "v" "u")) ("ǔ")) +((("\\" "=" "{" "\\" "A" "E" "}")) ("Ǣ")) +((("\\" "=" "\\" "A" "E")) ("Ǣ")) +((("\\" "=" "{" "\\" "a" "e" "}")) ("ǣ")) +((("\\" "=" "\\" "a" "e")) ("ǣ")) +((("\\" "v" "{" "G" "}")) ("Ǧ")) +((("\\" "v" "G")) ("Ǧ")) +((("\\" "v" "{" "g" "}")) ("ǧ")) +((("\\" "v" "g")) ("ǧ")) +((("\\" "v" "{" "K" "}")) ("Ǩ")) +((("\\" "v" "K")) ("Ǩ")) +((("\\" "v" "{" "k" "}")) ("ǩ")) +((("\\" "v" "k")) ("ǩ")) +((("\\" "v" "{" "\\" "j" "}")) ("ǰ")) +((("\\" "v" "j")) ("ǰ")) +((("\\" "'" "{" "G" "}")) ("Ǵ")) +((("\\" "'" "G")) ("Ǵ")) +((("\\" "'" "{" "g" "}")) ("ǵ")) +((("\\" "'" "g")) ("ǵ")) +((("\\" "`" "{" "N" "}")) ("Ǹ")) +((("\\" "`" "N")) ("Ǹ")) +((("\\" "`" "{" "n" "}")) ("ǹ")) +((("\\" "`" "n")) ("ǹ")) +((("\\" "'" "{" "\\" "A" "E" "}")) ("Ǽ")) +((("\\" "'" "\\" "A" "E")) ("Ǽ")) +((("\\" "'" "{" "\\" "a" "e" "}")) ("ǽ")) +((("\\" "'" "\\" "a" "e")) ("ǽ")) +((("\\" "'" "{" "\\" "O" "}")) ("Ǿ")) +((("\\" "'" "\\" "O")) ("Ǿ")) +((("\\" "'" "{" "\\" "o" "}")) ("ǿ")) +((("\\" "'" "\\" "o")) ("ǿ")) +((("\\" "v" "{" "H" "}")) ("Ȟ")) +((("\\" "v" "H")) ("Ȟ")) +((("\\" "v" "{" "h" "}")) ("ȟ")) +((("\\" "v" "h")) ("ȟ")) +((("\\" "." "{" "A" "}")) ("Ȧ")) +((("\\" "." "A")) ("Ȧ")) +((("\\" "." "{" "a" "}")) ("ȧ")) +((("\\" "." "a")) ("ȧ")) +((("\\" "c" "{" "E" "}")) ("Ȩ")) +((("\\" "c" "E")) ("Ȩ")) +((("\\" "c" "{" "e" "}")) ("ȩ")) +((("\\" "c" "e")) ("ȩ")) +((("\\" "." "{" "O" "}")) ("Ȯ")) +((("\\" "." "O")) ("Ȯ")) +((("\\" "." "{" "o" "}")) ("ȯ")) +((("\\" "." "o")) ("ȯ")) +((("\\" "=" "{" "Y" "}")) ("Ȳ")) +((("\\" "=" "Y")) ("Ȳ")) +((("\\" "=" "{" "y" "}")) ("ȳ")) +((("\\" "=" "y")) ("ȳ")) +((("\\" "v" "{" "}")) ("ˇ")) +((("\\" "u" "{" "}")) ("˘")) +((("\\" "." "{" "}")) ("˙")) +((("\\" "~" "{" "}")) ("˜")) +((("\\" "H" "{" "}")) ("˝")) +((("\\" "'")) ("́")) +((("\\" "'" "K")) ("Ḱ")) +((("\\" "'" "M")) ("Ḿ")) +((("\\" "'" "P")) ("Ṕ")) +((("\\" "'" "W")) ("Ẃ")) +((("\\" "'" "k")) ("ḱ")) +((("\\" "'" "m")) ("ḿ")) +((("\\" "'" "p")) ("ṕ")) +((("\\" "'" "w")) ("ẃ")) +((("\\" ",")) (" ")) +((("\\" ".")) ("̇")) +((("\\" "." "B")) ("Ḃ")) +((("\\" "." "D")) ("Ḋ")) +((("\\" "." "F")) ("Ḟ")) +((("\\" "." "H")) ("Ḣ")) +((("\\" "." "M")) ("Ṁ")) +((("\\" "." "N")) ("Ṅ")) +((("\\" "." "P")) ("Ṗ")) +((("\\" "." "R")) ("Ṙ")) +((("\\" "." "S")) ("Ṡ")) +((("\\" "." "T")) ("Ṫ")) +((("\\" "." "W")) ("Ẇ")) +((("\\" "." "X")) ("Ẋ")) +((("\\" "." "Y")) ("Ẏ")) +((("\\" "." "b")) ("ḃ")) +((("\\" "." "d")) ("ḋ")) +((("\\" "." "e")) ("ė")) +((("\\" "." "f")) ("ḟ")) +((("\\" "." "h")) ("ḣ")) +((("\\" "." "m")) ("ṁ")) +((("\\" "." "n")) ("ṅ")) +((("\\" "." "p")) ("ṗ")) +((("\\" "." "r")) ("ṙ")) +((("\\" "." "s")) ("ṡ")) +((("\\" "." "t")) ("ṫ")) +((("\\" "." "w")) ("ẇ")) +((("\\" "." "x")) ("ẋ")) +((("\\" "." "y")) ("ẏ")) +((("\\" "/")) ("")) +((("\\" ":")) (" ")) +((("\\" ";")) (" ")) +((("\\" "=")) ("̄")) +((("\\" "=" "G")) ("Ḡ")) +((("\\" "=" "g")) ("ḡ")) +((("^" "(")) ("⁽")) +((("^" ")")) ("⁾")) +((("^" "+")) ("⁺")) +((("^" "-")) ("⁻")) +((("^" "0")) ("⁰")) +((("^" "1")) ("¹")) +((("^" "2")) ("²")) +((("^" "3")) ("³")) +((("^" "4")) ("⁴")) +((("^" "5")) ("⁵")) +((("^" "6")) ("⁶")) +((("^" "7")) ("⁷")) +((("^" "8")) ("⁸")) +((("^" "9")) ("⁹")) +((("^" "=")) ("⁼")) +((("^" "\\" "g" "a" "m" "m" "a")) ("ˠ")) +((("^" "h")) ("ʰ")) +((("^" "j")) ("ʲ")) +((("^" "l")) ("ˡ")) +((("^" "n")) ("ⁿ")) +((("^" "o")) ("º")) +((("^" "r")) ("ʳ")) +((("^" "s")) ("ˢ")) +((("^" "w")) ("ʷ")) +((("^" "x")) ("ˣ")) +((("^" "y")) ("ʸ")) +((("^" "{" "S" "M" "}")) ("℠")) +((("^" "{" "T" "E" "L" "}")) ("℡")) +((("^" "{" "T" "M" "}")) ("™")) +((("_" "(")) ("₍")) +((("_" ")")) ("₎")) +((("_" "+")) ("₊")) +((("_" "-")) ("₋")) +((("_" "0")) ("₀")) +((("_" "1")) ("₁")) +((("_" "2")) ("₂")) +((("_" "3")) ("₃")) +((("_" "4")) ("₄")) +((("_" "5")) ("₅")) +((("_" "6")) ("₆")) +((("_" "7")) ("₇")) +((("_" "8")) ("₈")) +((("_" "9")) ("₉")) +((("_" "=")) ("₌")) +((("\\" "~")) ("̃")) +((("\\" "~" "E")) ("Ẽ")) +((("\\" "~" "V")) ("Ṽ")) +((("\\" "~" "Y")) ("Ỹ")) +((("\\" "~" "e")) ("ẽ")) +((("\\" "~" "v")) ("ṽ")) +((("\\" "~" "y")) ("ỹ")) +((("\\" "\"")) ("̈")) +((("\\" "\"" "H")) ("Ḧ")) +((("\\" "\"" "W")) ("Ẅ")) +((("\\" "\"" "X")) ("Ẍ")) +((("\\" "\"" "h")) ("ḧ")) +((("\\" "\"" "t")) ("ẗ")) +((("\\" "\"" "w")) ("ẅ")) +((("\\" "\"" "x")) ("ẍ")) +((("\\" "^")) ("̂")) +((("\\" "^" "Z")) ("Ẑ")) +((("\\" "^" "z")) ("ẑ")) +((("\\" "`")) ("̀")) +((("\\" "`" "W")) ("Ẁ")) +((("\\" "`" "Y")) ("Ỳ")) +((("\\" "`" "w")) ("ẁ")) +((("\\" "`" "y")) ("ỳ")) +((("\\" "b")) ("̱")) +((("\\" "c")) ("̧")) +((("\\" "c" "{" "D" "}")) ("Ḑ")) +((("\\" "c" "{" "H" "}")) ("Ḩ")) +((("\\" "c" "{" "d" "}")) ("ḑ")) +((("\\" "c" "{" "h" "}")) ("ḩ")) +((("\\" "d")) ("̣")) +((("\\" "d" "{" "A" "}")) ("Ạ")) +((("\\" "d" "{" "B" "}")) ("Ḅ")) +((("\\" "d" "{" "D" "}")) ("Ḍ")) +((("\\" "d" "{" "E" "}")) ("Ẹ")) +((("\\" "d" "{" "H" "}")) ("Ḥ")) +((("\\" "d" "{" "I" "}")) ("Ị")) +((("\\" "d" "{" "K" "}")) ("Ḳ")) +((("\\" "d" "{" "L" "}")) ("Ḷ")) +((("\\" "d" "{" "M" "}")) ("Ṃ")) +((("\\" "d" "{" "N" "}")) ("Ṇ")) +((("\\" "d" "{" "O" "}")) ("Ọ")) +((("\\" "d" "{" "R" "}")) ("Ṛ")) +((("\\" "d" "{" "S" "}")) ("Ṣ")) +((("\\" "d" "{" "T" "}")) ("Ṭ")) +((("\\" "d" "{" "U" "}")) ("Ụ")) +((("\\" "d" "{" "V" "}")) ("Ṿ")) +((("\\" "d" "{" "W" "}")) ("Ẉ")) +((("\\" "d" "{" "Y" "}")) ("Ỵ")) +((("\\" "d" "{" "Z" "}")) ("Ẓ")) +((("\\" "d" "{" "a" "}")) ("ạ")) +((("\\" "d" "{" "b" "}")) ("ḅ")) +((("\\" "d" "{" "d" "}")) ("ḍ")) +((("\\" "d" "{" "e" "}")) ("ẹ")) +((("\\" "d" "{" "h" "}")) ("ḥ")) +((("\\" "d" "{" "i" "}")) ("ị")) +((("\\" "d" "{" "k" "}")) ("ḳ")) +((("\\" "d" "{" "l" "}")) ("ḷ")) +((("\\" "d" "{" "m" "}")) ("ṃ")) +((("\\" "d" "{" "n" "}")) ("ṇ")) +((("\\" "d" "{" "o" "}")) ("ọ")) +((("\\" "d" "{" "r" "}")) ("ṛ")) +((("\\" "d" "{" "s" "}")) ("ṣ")) +((("\\" "d" "{" "t" "}")) ("ṭ")) +((("\\" "d" "{" "u" "}")) ("ụ")) +((("\\" "d" "{" "v" "}")) ("ṿ")) +((("\\" "d" "{" "w" "}")) ("ẉ")) +((("\\" "d" "{" "y" "}")) ("ỵ")) +((("\\" "d" "{" "z" "}")) ("ẓ")) +((("\\" "r" "q")) ("’")) +((("\\" "u")) ("̆")) +((("\\" "v")) ("̌")) +((("\\" "v" "{" "L" "}")) ("Ľ")) +((("\\" "v" "{" "i" "}")) ("ǐ")) +((("\\" "v" "{" "j" "}")) ("ǰ")) +((("\\" "v" "{" "l" "}")) ("ľ")) +((("\\" "y" "e" "n")) ("¥")) +((("\\" "B" "o" "x")) ("□")) +((("\\" "B" "u" "m" "p" "e" "q")) ("≎")) +((("\\" "C" "a" "p")) ("⋒")) +((("\\" "C" "u" "p")) ("⋓")) +((("\\" "D" "e" "l" "t" "a")) ("Δ")) +((("\\" "D" "i" "a" "m" "o" "n" "d")) ("◇")) +((("\\" "D" "o" "w" "n" "a" "r" "r" "o" "w")) ("⇓")) +((("\\" "G" "a" "m" "m" "a")) ("Γ")) +((("\\" "H")) ("̋")) +((("\\" "H" "{" "o" "}")) ("ő")) +((("\\" "I" "m")) ("ℑ")) +((("\\" "J" "o" "i" "n")) ("⋈")) +((("\\" "L" "a" "m" "b" "d" "a")) ("Λ")) +((("\\" "L" "e" "f" "t" "a" "r" "r" "o" "w")) ("⇐")) +((("\\" "L" "e" "f" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("⇔")) +((("\\" "L" "l")) ("⋘")) +((("\\" "L" "l" "e" "f" "t" "a" "r" "r" "o" "w")) ("⇚")) +((("\\" "L" "o" "n" "g" "l" "e" "f" "t" "a" "r" "r" "o" "w")) ("⇐")) +((("\\" "L" "o" "n" "g" "l" "e" "f" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("⇔")) +((("\\" "L" "o" "n" "g" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("⇒")) +((("\\" "L" "s" "h")) ("↰")) +((("\\" "O" "m" "e" "g" "a")) ("Ω")) +((("\\" "P" "h" "i")) ("Φ")) +((("\\" "P" "i")) ("Π")) +((("\\" "P" "s" "i")) ("Ψ")) +((("\\" "R" "e")) ("ℜ")) +((("\\" "R" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("⇒")) +((("\\" "R" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("⇛")) +((("\\" "R" "s" "h")) ("↱")) +((("\\" "S" "i" "g" "m" "a")) ("Σ")) +((("\\" "S" "u" "b" "s" "e" "t")) ("⋐")) +((("\\" "S" "u" "p" "s" "e" "t")) ("⋑")) +((("\\" "T" "h" "e" "t" "a")) ("Θ")) +((("\\" "U" "p" "a" "r" "r" "o" "w")) ("⇑")) +((("\\" "U" "p" "d" "o" "w" "n" "a" "r" "r" "o" "w")) ("⇕")) +((("\\" "U" "p" "s" "i" "l" "o" "n")) ("Υ")) +((("\\" "V" "d" "a" "s" "h")) ("⊩")) +((("\\" "V" "e" "r" "t")) ("‖")) +((("\\" "V" "v" "d" "a" "s" "h")) ("⊪")) +((("\\" "X" "i")) ("Ξ")) +((("\\" "a" "l" "e" "p" "h")) ("א")) +((("\\" "a" "l" "p" "h" "a")) ("α")) +((("\\" "a" "m" "a" "l" "g")) ("∐")) +((("\\" "a" "n" "g" "l" "e")) ("∠")) +((("\\" "a" "p" "p" "r" "o" "x")) ("≈")) +((("\\" "a" "p" "p" "r" "o" "x" "e" "q")) ("≊")) +((("\\" "a" "s" "t")) ("∗")) +((("\\" "a" "s" "y" "m" "p")) ("≍")) +((("\\" "b" "a" "c" "k" "c" "o" "n" "g")) ("≌")) +((("\\" "b" "a" "c" "k" "e" "p" "s" "i" "l" "o" "n")) ("∍")) +((("\\" "b" "a" "c" "k" "p" "r" "i" "m" "e")) ("‵")) +((("\\" "b" "a" "c" "k" "s" "i" "m")) ("∽")) +((("\\" "b" "a" "c" "k" "s" "i" "m" "e" "q")) ("⋍")) +((("\\" "b" "a" "c" "k" "s" "l" "a" "s" "h")) ("\\")) +((("\\" "b" "a" "r" "w" "e" "d" "g" "e")) ("⊼")) +((("\\" "b" "e" "c" "a" "u" "s" "e")) ("∵")) +((("\\" "b" "e" "t" "a")) ("β")) +((("\\" "b" "e" "t" "h")) ("ב")) +((("\\" "b" "e" "t" "w" "e" "e" "n")) ("≬")) +((("\\" "b" "i" "g" "c" "a" "p")) ("⋂")) +((("\\" "b" "i" "g" "c" "i" "r" "c")) ("◯")) +((("\\" "b" "i" "g" "c" "u" "p")) ("⋃")) +((("\\" "b" "i" "g" "s" "t" "a" "r")) ("★")) +((("\\" "b" "i" "g" "t" "r" "i" "a" "n" "g" "l" "e" "d" "o" "w" "n")) ("▽")) +((("\\" "b" "i" "g" "t" "r" "i" "a" "n" "g" "l" "e" "u" "p")) ("△")) +((("\\" "b" "i" "g" "v" "e" "e")) ("⋁")) +((("\\" "b" "i" "g" "w" "e" "d" "g" "e")) ("⋀")) +((("\\" "b" "l" "a" "c" "k" "l" "o" "z" "e" "n" "g" "e")) ("✦")) +((("\\" "b" "l" "a" "c" "k" "s" "q" "u" "a" "r" "e")) ("▪")) +((("\\" "b" "l" "a" "c" "k" "t" "r" "i" "a" "n" "g" "l" "e")) ("▴")) +((("\\" "b" "l" "a" "c" "k" "t" "r" "i" "a" "n" "g" "l" "e" "d" "o" "w" "n")) ("▾")) +((("\\" "b" "l" "a" "c" "k" "t" "r" "i" "a" "n" "g" "l" "e" "l" "e" "f" "t")) ("◂")) +((("\\" "b" "l" "a" "c" "k" "t" "r" "i" "a" "n" "g" "l" "e" "r" "i" "g" "h" "t")) ("▸")) +((("\\" "b" "o" "t")) ("⊥")) +((("\\" "b" "o" "w" "t" "i" "e")) ("⋈")) +((("\\" "b" "o" "x" "m" "i" "n" "u" "s")) ("⊟")) +((("\\" "b" "o" "x" "p" "l" "u" "s")) ("⊞")) +((("\\" "b" "o" "x" "t" "i" "m" "e" "s")) ("⊠")) +((("\\" "b" "u" "l" "l" "e" "t")) ("•")) +((("\\" "b" "u" "m" "p" "e" "q")) ("≏")) +((("\\" "c" "a" "p")) ("∩")) +((("\\" "c" "d" "o" "t" "s")) ("⋯")) +((("\\" "c" "e" "n" "t" "e" "r" "d" "o" "t")) ("·")) +((("\\" "c" "h" "e" "c" "k" "m" "a" "r" "k")) ("✓")) +((("\\" "c" "h" "i")) ("χ")) +((("\\" "c" "i" "r" "c")) ("○")) +((("\\" "c" "i" "r" "c" "e" "q")) ("≗")) +((("\\" "c" "i" "r" "c" "l" "e" "a" "r" "r" "o" "w" "l" "e" "f" "t")) ("↺")) +((("\\" "c" "i" "r" "c" "l" "e" "a" "r" "r" "o" "w" "r" "i" "g" "h" "t")) ("↻")) +((("\\" "c" "i" "r" "c" "l" "e" "d" "R")) ("®")) +((("\\" "c" "i" "r" "c" "l" "e" "d" "S")) ("Ⓢ")) +((("\\" "c" "i" "r" "c" "l" "e" "d" "a" "s" "t")) ("⊛")) +((("\\" "c" "i" "r" "c" "l" "e" "d" "c" "i" "r" "c")) ("⊚")) +((("\\" "c" "i" "r" "c" "l" "e" "d" "d" "a" "s" "h")) ("⊝")) +((("\\" "c" "l" "u" "b" "s" "u" "i" "t")) ("♣")) +((("\\" "c" "o" "l" "o" "n")) (":")) +((("\\" "c" "o" "l" "o" "n" "e" "q")) ("≔")) +((("\\" "c" "o" "m" "p" "l" "e" "m" "e" "n" "t")) ("∁")) +((("\\" "c" "o" "n" "g")) ("≅")) +((("\\" "c" "o" "p" "r" "o" "d")) ("∐")) +((("\\" "c" "u" "p")) ("∪")) +((("\\" "c" "u" "r" "l" "y" "e" "q" "p" "r" "e" "c")) ("⋞")) +((("\\" "c" "u" "r" "l" "y" "e" "q" "s" "u" "c" "c")) ("⋟")) +((("\\" "c" "u" "r" "l" "y" "p" "r" "e" "c" "e" "q")) ("≼")) +((("\\" "c" "u" "r" "l" "y" "v" "e" "e")) ("⋎")) +((("\\" "c" "u" "r" "l" "y" "w" "e" "d" "g" "e")) ("⋏")) +((("\\" "c" "u" "r" "v" "e" "a" "r" "r" "o" "w" "l" "e" "f" "t")) ("↶")) +((("\\" "c" "u" "r" "v" "e" "a" "r" "r" "o" "w" "r" "i" "g" "h" "t")) ("↷")) +((("\\" "d" "a" "g")) ("†")) +((("\\" "d" "a" "g" "g" "e" "r")) ("†")) +((("\\" "d" "a" "l" "e" "t" "h")) ("ד")) +((("\\" "d" "a" "s" "h" "v")) ("⊣")) +((("\\" "d" "d" "a" "g")) ("‡")) +((("\\" "d" "d" "a" "g" "g" "e" "r")) ("‡")) +((("\\" "d" "d" "o" "t" "s")) ("⋱")) +((("\\" "d" "e" "l" "t" "a")) ("δ")) +((("\\" "d" "i" "a" "m" "o" "n" "d")) ("⋄")) +((("\\" "d" "i" "a" "m" "o" "n" "d" "s" "u" "i" "t")) ("♢")) +((("\\" "d" "i" "g" "a" "m" "m" "a")) ("Ϝ")) +((("\\" "d" "i" "v" "i" "d" "e" "o" "n" "t" "i" "m" "e" "s")) ("⋇")) +((("\\" "d" "o" "t" "e" "q")) ("≐")) +((("\\" "d" "o" "t" "e" "q" "d" "o" "t")) ("≑")) +((("\\" "d" "o" "t" "p" "l" "u" "s")) ("∔")) +((("\\" "d" "o" "t" "s" "q" "u" "a" "r" "e")) ("⊡")) +((("\\" "d" "o" "w" "n" "a" "r" "r" "o" "w")) ("↓")) +((("\\" "d" "o" "w" "n" "d" "o" "w" "n" "a" "r" "r" "o" "w" "s")) ("⇊")) +((("\\" "d" "o" "w" "n" "l" "e" "f" "t" "h" "a" "r" "p" "o" "o" "n")) ("⇃")) +((("\\" "d" "o" "w" "n" "r" "i" "g" "h" "t" "h" "a" "r" "p" "o" "o" "n")) ("⇂")) +((("\\" "e" "l" "l")) ("ℓ")) +((("\\" "e" "m" "p" "t" "y" "s" "e" "t")) ("∅")) +((("\\" "e" "p" "s" "i" "l" "o" "n")) ("ε")) +((("\\" "e" "q" "c" "i" "r" "c")) ("≖")) +((("\\" "e" "q" "c" "o" "l" "o" "n")) ("≕")) +((("\\" "e" "q" "s" "l" "a" "n" "t" "g" "t" "r")) ("⋝")) +((("\\" "e" "q" "s" "l" "a" "n" "t" "l" "e" "s" "s")) ("⋜")) +((("\\" "e" "q" "u" "i" "v")) ("≡")) +((("\\" "e" "t" "a")) ("η")) +((("\\" "e" "u" "r" "o")) ("€")) +((("\\" "e" "x" "i" "s" "t" "s")) ("∃")) +((("\\" "f" "a" "l" "l" "i" "n" "g" "d" "o" "t" "s" "e" "q")) ("≒")) +((("\\" "f" "l" "a" "t")) ("♭")) +((("\\" "f" "o" "r" "a" "l" "l")) ("∀")) +((("\\" "f" "r" "a" "c" "1")) ("⅟")) +((("\\" "f" "r" "a" "c" "1" "2")) ("½")) +((("\\" "f" "r" "a" "c" "1" "3")) ("⅓")) +((("\\" "f" "r" "a" "c" "1" "4")) ("¼")) +((("\\" "f" "r" "a" "c" "1" "5")) ("⅕")) +((("\\" "f" "r" "a" "c" "1" "6")) ("⅙")) +((("\\" "f" "r" "a" "c" "1" "8")) ("⅛")) +((("\\" "f" "r" "a" "c" "2" "3")) ("⅔")) +((("\\" "f" "r" "a" "c" "2" "5")) ("⅖")) +((("\\" "f" "r" "a" "c" "3" "4")) ("¾")) +((("\\" "f" "r" "a" "c" "3" "5")) ("⅗")) +((("\\" "f" "r" "a" "c" "3" "8")) ("⅜")) +((("\\" "f" "r" "a" "c" "4" "5")) ("⅘")) +((("\\" "f" "r" "a" "c" "5" "6")) ("⅚")) +((("\\" "f" "r" "a" "c" "5" "8")) ("⅝")) +((("\\" "f" "r" "a" "c" "7" "8")) ("⅞")) +((("\\" "f" "r" "o" "w" "n")) ("⌢")) +((("\\" "g" "a" "m" "m" "a")) ("γ")) +((("\\" "g" "e")) ("≥")) +((("\\" "g" "e" "q")) ("≥")) +((("\\" "g" "e" "q" "q")) ("≧")) +((("\\" "g" "e" "q" "s" "l" "a" "n" "t")) ("≥")) +((("\\" "g" "e" "t" "s")) ("←")) +((("\\" "g" "g")) ("≫")) +((("\\" "g" "g" "g")) ("⋙")) +((("\\" "g" "i" "m" "e" "l")) ("ג")) +((("\\" "g" "n" "a" "p" "p" "r" "o" "x")) ("⋧")) +((("\\" "g" "n" "e" "q")) ("≩")) +((("\\" "g" "n" "e" "q" "q")) ("≩")) +((("\\" "g" "n" "s" "i" "m")) ("⋧")) +((("\\" "g" "t" "r" "a" "p" "p" "r" "o" "x")) ("≳")) +((("\\" "g" "t" "r" "d" "o" "t")) ("⋗")) +((("\\" "g" "t" "r" "e" "q" "l" "e" "s" "s")) ("⋛")) +((("\\" "g" "t" "r" "e" "q" "q" "l" "e" "s" "s")) ("⋛")) +((("\\" "g" "t" "r" "l" "e" "s" "s")) ("≷")) +((("\\" "g" "t" "r" "s" "i" "m")) ("≳")) +((("\\" "g" "v" "e" "r" "t" "n" "e" "q" "q")) ("≩")) +((("\\" "h" "b" "a" "r")) ("ℏ")) +((("\\" "h" "e" "a" "r" "t" "s" "u" "i" "t")) ("♥")) +((("\\" "h" "o" "o" "k" "l" "e" "f" "t" "a" "r" "r" "o" "w")) ("↩")) +((("\\" "h" "o" "o" "k" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("↪")) +((("\\" "i" "f" "f")) ("⇔")) +((("\\" "i" "m" "a" "t" "h")) ("ı")) +((("\\" "i" "n")) ("∈")) +((("\\" "i" "n" "f" "t" "y")) ("∞")) +((("\\" "i" "n" "t")) ("∫")) +((("\\" "i" "n" "t" "e" "r" "c" "a" "l")) ("⊺")) +((("\\" "i" "o" "t" "a")) ("ι")) +((("\\" "k" "a" "p" "p" "a")) ("κ")) +((("\\" "l" "a" "m" "b" "d" "a")) ("λ")) +((("\\" "l" "a" "n" "g" "l" "e")) ("〈")) +((("\\" "l" "b" "r" "a" "c" "e")) ("{")) +((("\\" "l" "b" "r" "a" "c" "k")) ("[")) +((("\\" "l" "c" "e" "i" "l")) ("⌈")) +((("\\" "l" "d" "o" "t" "s")) ("…")) +((("\\" "l" "e")) ("≤")) +((("\\" "l" "e" "a" "d" "s" "t" "o")) ("↝")) +((("\\" "l" "e" "f" "t" "a" "r" "r" "o" "w")) ("←")) +((("\\" "l" "e" "f" "t" "a" "r" "r" "o" "w" "t" "a" "i" "l")) ("↢")) +((("\\" "l" "e" "f" "t" "h" "a" "r" "p" "o" "o" "n" "d" "o" "w" "n")) ("↽")) +((("\\" "l" "e" "f" "t" "h" "a" "r" "p" "o" "o" "n" "u" "p")) ("↼")) +((("\\" "l" "e" "f" "t" "l" "e" "f" "t" "a" "r" "r" "o" "w" "s")) ("⇇")) +((("\\" "l" "e" "f" "t" "p" "a" "r" "e" "n" "g" "t" "r")) ("〈")) +((("\\" "l" "e" "f" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("↔")) +((("\\" "l" "e" "f" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w" "s")) ("⇆")) +((("\\" "l" "e" "f" "t" "r" "i" "g" "h" "t" "h" "a" "r" "p" "o" "o" "n" "s")) ("⇋")) +((("\\" "l" "e" "f" "t" "r" "i" "g" "h" "t" "s" "q" "u" "i" "g" "a" "r" "r" "o" "w")) ("↭")) +((("\\" "l" "e" "f" "t" "t" "h" "r" "e" "e" "t" "i" "m" "e" "s")) ("⋋")) +((("\\" "l" "e" "q")) ("≤")) +((("\\" "l" "e" "q" "q")) ("≦")) +((("\\" "l" "e" "q" "s" "l" "a" "n" "t")) ("≤")) +((("\\" "l" "e" "s" "s" "a" "p" "p" "r" "o" "x")) ("≲")) +((("\\" "l" "e" "s" "s" "d" "o" "t")) ("⋖")) +((("\\" "l" "e" "s" "s" "e" "q" "g" "t" "r")) ("⋚")) +((("\\" "l" "e" "s" "s" "e" "q" "q" "g" "t" "r")) ("⋚")) +((("\\" "l" "e" "s" "s" "g" "t" "r")) ("≶")) +((("\\" "l" "e" "s" "s" "s" "i" "m")) ("≲")) +((("\\" "l" "f" "l" "o" "o" "r")) ("⌊")) +((("\\" "l" "h" "d")) ("◁")) +((("\\" "r" "h" "d")) ("▷")) +((("\\" "l" "l")) ("≪")) +((("\\" "l" "l" "c" "o" "r" "n" "e" "r")) ("⌞")) +((("\\" "l" "n" "a" "p" "p" "r" "o" "x")) ("⋦")) +((("\\" "l" "n" "e" "q")) ("≨")) +((("\\" "l" "n" "e" "q" "q")) ("≨")) +((("\\" "l" "n" "s" "i" "m")) ("⋦")) +((("\\" "l" "o" "n" "g" "l" "e" "f" "t" "a" "r" "r" "o" "w")) ("←")) +((("\\" "l" "o" "n" "g" "l" "e" "f" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("↔")) +((("\\" "l" "o" "n" "g" "m" "a" "p" "s" "t" "o")) ("↦")) +((("\\" "l" "o" "n" "g" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("→")) +((("\\" "l" "o" "o" "p" "a" "r" "r" "o" "w" "l" "e" "f" "t")) ("↫")) +((("\\" "l" "o" "o" "p" "a" "r" "r" "o" "w" "r" "i" "g" "h" "t")) ("↬")) +((("\\" "l" "o" "z" "e" "n" "g" "e")) ("✧")) +((("\\" "l" "q")) ("‘")) +((("\\" "l" "r" "c" "o" "r" "n" "e" "r")) ("⌟")) +((("\\" "l" "t" "i" "m" "e" "s")) ("⋉")) +((("\\" "l" "v" "e" "r" "t" "n" "e" "q" "q")) ("≨")) +((("\\" "m" "a" "l" "t" "e" "s" "e")) ("✠")) +((("\\" "m" "a" "p" "s" "t" "o")) ("↦")) +((("\\" "m" "e" "a" "s" "u" "r" "e" "d" "a" "n" "g" "l" "e")) ("∡")) +((("\\" "m" "h" "o")) ("℧")) +((("\\" "m" "i" "d")) ("∣")) +((("\\" "m" "o" "d" "e" "l" "s")) ("⊧")) +((("\\" "m" "p")) ("∓")) +((("\\" "m" "u" "l" "t" "i" "m" "a" "p")) ("⊸")) +((("\\" "n" "L" "e" "f" "t" "a" "r" "r" "o" "w")) ("⇍")) +((("\\" "n" "L" "e" "f" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("⇎")) +((("\\" "n" "R" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("⇏")) +((("\\" "n" "V" "D" "a" "s" "h")) ("⊯")) +((("\\" "n" "V" "d" "a" "s" "h")) ("⊮")) +((("\\" "n" "a" "b" "l" "a")) ("∇")) +((("\\" "n" "a" "p" "p" "r" "o" "x")) ("≉")) +((("\\" "n" "a" "t" "u" "r" "a" "l")) ("♮")) +((("\\" "n" "c" "o" "n" "g")) ("≇")) +((("\\" "n" "e")) ("≠")) +((("\\" "n" "e" "a" "r" "r" "o" "w")) ("↗")) +((("\\" "n" "e" "g")) ("¬")) +((("\\" "n" "e" "q")) ("≠")) +((("\\" "n" "e" "q" "u" "i" "v")) ("≢")) +((("\\" "n" "e" "w" "l" "i" "n" "e")) ("
")) +((("\\" "n" "e" "x" "i" "s" "t" "s")) ("∄")) +((("\\" "n" "g" "e" "q")) ("≱")) +((("\\" "n" "g" "e" "q" "q")) ("≱")) +((("\\" "n" "g" "e" "q" "s" "l" "a" "n" "t")) ("≱")) +((("\\" "n" "g" "t" "r")) ("≯")) +((("\\" "n" "i")) ("∋")) +((("\\" "n" "l" "e" "f" "t" "a" "r" "r" "o" "w")) ("↚")) +((("\\" "n" "l" "e" "f" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("↮")) +((("\\" "n" "l" "e" "q")) ("≰")) +((("\\" "n" "l" "e" "q" "q")) ("≰")) +((("\\" "n" "l" "e" "q" "s" "l" "a" "n" "t")) ("≰")) +((("\\" "n" "l" "e" "s" "s")) ("≮")) +((("\\" "n" "m" "i" "d")) ("∤")) +((("\\" "n" "o" "t")) ("̸")) +((("\\" "n" "o" "t" "i" "n")) ("∉")) +((("\\" "n" "p" "a" "r" "a" "l" "l" "e" "l")) ("∦")) +((("\\" "n" "p" "r" "e" "c")) ("⊀")) +((("\\" "n" "p" "r" "e" "c" "e" "q")) ("⋠")) +((("\\" "n" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("↛")) +((("\\" "n" "s" "h" "o" "r" "t" "m" "i" "d")) ("∤")) +((("\\" "n" "s" "h" "o" "r" "t" "p" "a" "r" "a" "l" "l" "e" "l")) ("∦")) +((("\\" "n" "s" "i" "m")) ("≁")) +((("\\" "n" "s" "i" "m" "e" "q")) ("≄")) +((("\\" "n" "s" "u" "b" "s" "e" "t")) ("⊄")) +((("\\" "n" "s" "u" "b" "s" "e" "t" "e" "q")) ("⊈")) +((("\\" "n" "s" "u" "b" "s" "e" "t" "e" "q" "q")) ("⊈")) +((("\\" "n" "s" "u" "c" "c")) ("⊁")) +((("\\" "n" "s" "u" "c" "c" "e" "q")) ("⋡")) +((("\\" "n" "s" "u" "p" "s" "e" "t")) ("⊅")) +((("\\" "n" "s" "u" "p" "s" "e" "t" "e" "q")) ("⊉")) +((("\\" "n" "s" "u" "p" "s" "e" "t" "e" "q" "q")) ("⊉")) +((("\\" "n" "t" "r" "i" "a" "n" "g" "l" "e" "l" "e" "f" "t")) ("⋪")) +((("\\" "n" "t" "r" "i" "a" "n" "g" "l" "e" "l" "e" "f" "t" "e" "q")) ("⋬")) +((("\\" "n" "t" "r" "i" "a" "n" "g" "l" "e" "r" "i" "g" "h" "t")) ("⋫")) +((("\\" "n" "t" "r" "i" "a" "n" "g" "l" "e" "r" "i" "g" "h" "t" "e" "q")) ("⋭")) +((("\\" "n" "u")) ("ν")) +((("\\" "n" "v" "D" "a" "s" "h")) ("⊭")) +((("\\" "n" "v" "d" "a" "s" "h")) ("⊬")) +((("\\" "n" "w" "a" "r" "r" "o" "w")) ("↖")) +((("\\" "o" "d" "o" "t")) ("⊙")) +((("\\" "o" "i" "n" "t")) ("∮")) +((("\\" "o" "m" "e" "g" "a")) ("ω")) +((("\\" "o" "m" "i" "n" "u" "s")) ("⊖")) +((("\\" "o" "p" "l" "u" "s")) ("⊕")) +((("\\" "o" "s" "l" "a" "s" "h")) ("⊘")) +((("\\" "o" "t" "i" "m" "e" "s")) ("⊗")) +((("\\" "p" "a" "r")) ("
")) +((("\\" "p" "a" "r" "a" "l" "l" "e" "l")) ("∥")) +((("\\" "p" "a" "r" "t" "i" "a" "l")) ("∂")) +((("\\" "p" "e" "r" "p")) ("⊥")) +((("\\" "p" "h" "i")) ("φ")) +((("\\" "p" "i")) ("π")) +((("\\" "p" "i" "t" "c" "h" "f" "o" "r" "k")) ("⋔")) +((("\\" "p" "r" "e" "c")) ("≺")) +((("\\" "p" "r" "e" "c" "a" "p" "p" "r" "o" "x")) ("≾")) +((("\\" "p" "r" "e" "c" "e" "q")) ("≼")) +((("\\" "p" "r" "e" "c" "n" "a" "p" "p" "r" "o" "x")) ("⋨")) +((("\\" "p" "r" "e" "c" "n" "s" "i" "m")) ("⋨")) +((("\\" "p" "r" "e" "c" "s" "i" "m")) ("≾")) +((("\\" "p" "r" "i" "m" "e")) ("′")) +((("\\" "p" "r" "o" "d")) ("∏")) +((("\\" "p" "r" "o" "p" "t" "o")) ("∝")) +((("\\" "p" "s" "i")) ("ψ")) +((("\\" "q" "e" "d")) ("∎")) +((("\\" "q" "u" "a" "d")) (" ")) +((("\\" "r" "a" "n" "g" "l" "e")) ("〉")) +((("\\" "r" "b" "r" "a" "c" "e")) ("}")) +((("\\" "r" "b" "r" "a" "c" "k")) ("]")) +((("\\" "r" "c" "e" "i" "l")) ("⌉")) +((("\\" "r" "f" "l" "o" "o" "r")) ("⌋")) +((("\\" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("→")) +((("\\" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w" "t" "a" "i" "l")) ("↣")) +((("\\" "r" "i" "g" "h" "t" "h" "a" "r" "p" "o" "o" "n" "d" "o" "w" "n")) ("⇁")) +((("\\" "r" "i" "g" "h" "t" "h" "a" "r" "p" "o" "o" "n" "u" "p")) ("⇀")) +((("\\" "r" "i" "g" "h" "t" "l" "e" "f" "t" "a" "r" "r" "o" "w" "s")) ("⇄")) +((("\\" "r" "i" "g" "h" "t" "l" "e" "f" "t" "h" "a" "r" "p" "o" "o" "n" "s")) ("⇌")) +((("\\" "r" "i" "g" "h" "t" "p" "a" "r" "e" "n" "g" "t" "r")) ("〉")) +((("\\" "r" "i" "g" "h" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w" "s")) ("⇉")) +((("\\" "r" "i" "g" "h" "t" "t" "h" "r" "e" "e" "t" "i" "m" "e" "s")) ("⋌")) +((("\\" "r" "i" "s" "i" "n" "g" "d" "o" "t" "s" "e" "q")) ("≓")) +((("\\" "r" "t" "i" "m" "e" "s")) ("⋊")) +((("\\" "s" "b" "s")) ("﹨")) +((("\\" "s" "e" "a" "r" "r" "o" "w")) ("↘")) +((("\\" "s" "e" "t" "m" "i" "n" "u" "s")) ("∖")) +((("\\" "s" "h" "a" "r" "p")) ("♯")) +((("\\" "s" "h" "o" "r" "t" "m" "i" "d")) ("∣")) +((("\\" "s" "h" "o" "r" "t" "p" "a" "r" "a" "l" "l" "e" "l")) ("∥")) +((("\\" "s" "i" "g" "m" "a")) ("σ")) +((("\\" "s" "i" "m")) ("∼")) +((("\\" "s" "i" "m" "e" "q")) ("≃")) +((("\\" "s" "m" "a" "l" "l" "a" "m" "a" "l" "g")) ("∐")) +((("\\" "s" "m" "a" "l" "l" "s" "e" "t" "m" "i" "n" "u" "s")) ("∖")) +((("\\" "s" "m" "a" "l" "l" "s" "m" "i" "l" "e")) ("⌣")) +((("\\" "s" "m" "i" "l" "e")) ("⌣")) +((("\\" "s" "p" "a" "d" "e" "s" "u" "i" "t")) ("♠")) +((("\\" "s" "p" "h" "e" "r" "i" "c" "a" "l" "a" "n" "g" "l" "e")) ("∢")) +((("\\" "s" "q" "c" "a" "p")) ("⊓")) +((("\\" "s" "q" "c" "u" "p")) ("⊔")) +((("\\" "s" "q" "s" "u" "b" "s" "e" "t")) ("⊏")) +((("\\" "s" "q" "s" "u" "b" "s" "e" "t" "e" "q")) ("⊑")) +((("\\" "s" "q" "s" "u" "p" "s" "e" "t")) ("⊐")) +((("\\" "s" "q" "s" "u" "p" "s" "e" "t" "e" "q")) ("⊒")) +((("\\" "s" "q" "u" "a" "r" "e")) ("□")) +((("\\" "s" "q" "u" "i" "g" "a" "r" "r" "o" "w" "r" "i" "g" "h" "t")) ("⇝")) +((("\\" "s" "t" "a" "r")) ("⋆")) +((("\\" "s" "t" "r" "a" "i" "g" "h" "t" "p" "h" "i")) ("φ")) +((("\\" "s" "u" "b" "s" "e" "t")) ("⊂")) +((("\\" "s" "u" "b" "s" "e" "t" "e" "q")) ("⊆")) +((("\\" "s" "u" "b" "s" "e" "t" "e" "q" "q")) ("⊆")) +((("\\" "s" "u" "b" "s" "e" "t" "n" "e" "q")) ("⊊")) +((("\\" "s" "u" "b" "s" "e" "t" "n" "e" "q" "q")) ("⊊")) +((("\\" "s" "u" "c" "c")) ("≻")) +((("\\" "s" "u" "c" "c" "a" "p" "p" "r" "o" "x")) ("≿")) +((("\\" "s" "u" "c" "c" "c" "u" "r" "l" "y" "e" "q")) ("≽")) +((("\\" "s" "u" "c" "c" "e" "q")) ("≽")) +((("\\" "s" "u" "c" "c" "n" "a" "p" "p" "r" "o" "x")) ("⋩")) +((("\\" "s" "u" "c" "c" "n" "s" "i" "m")) ("⋩")) +((("\\" "s" "u" "c" "c" "s" "i" "m")) ("≿")) +((("\\" "s" "u" "m")) ("∑")) +((("\\" "s" "u" "p" "s" "e" "t")) ("⊃")) +((("\\" "s" "u" "p" "s" "e" "t" "e" "q")) ("⊇")) +((("\\" "s" "u" "p" "s" "e" "t" "e" "q" "q")) ("⊇")) +((("\\" "s" "u" "p" "s" "e" "t" "n" "e" "q")) ("⊋")) +((("\\" "s" "u" "p" "s" "e" "t" "n" "e" "q" "q")) ("⊋")) +((("\\" "s" "u" "r" "d")) ("√")) +((("\\" "s" "w" "a" "r" "r" "o" "w")) ("↙")) +((("\\" "t" "a" "u")) ("τ")) +((("\\" "t" "h" "e" "r" "e" "f" "o" "r" "e")) ("∴")) +((("\\" "t" "h" "e" "t" "a")) ("θ")) +((("\\" "t" "h" "i" "c" "k" "a" "p" "p" "r" "o" "x")) ("≈")) +((("\\" "t" "h" "i" "c" "k" "s" "i" "m")) ("∼")) +((("\\" "t" "o")) ("→")) +((("\\" "t" "o" "p")) ("⊤")) +((("\\" "t" "r" "i" "a" "n" "g" "l" "e")) ("▵")) +((("\\" "t" "r" "i" "a" "n" "g" "l" "e" "d" "o" "w" "n")) ("▿")) +((("\\" "t" "r" "i" "a" "n" "g" "l" "e" "l" "e" "f" "t")) ("◃")) +((("\\" "t" "r" "i" "a" "n" "g" "l" "e" "l" "e" "f" "t" "e" "q")) ("⊴")) +((("\\" "t" "r" "i" "a" "n" "g" "l" "e" "q")) ("≜")) +((("\\" "t" "r" "i" "a" "n" "g" "l" "e" "r" "i" "g" "h" "t")) ("▹")) +((("\\" "t" "r" "i" "a" "n" "g" "l" "e" "r" "i" "g" "h" "t" "e" "q")) ("⊵")) +((("\\" "t" "w" "o" "h" "e" "a" "d" "l" "e" "f" "t" "a" "r" "r" "o" "w")) ("↞")) +((("\\" "t" "w" "o" "h" "e" "a" "d" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("↠")) +((("\\" "u" "l" "c" "o" "r" "n" "e" "r")) ("⌜")) +((("\\" "u" "p" "a" "r" "r" "o" "w")) ("↑")) +((("\\" "u" "p" "d" "o" "w" "n" "a" "r" "r" "o" "w")) ("↕")) +((("\\" "u" "p" "l" "e" "f" "t" "h" "a" "r" "p" "o" "o" "n")) ("↿")) +((("\\" "u" "p" "l" "u" "s")) ("⊎")) +((("\\" "u" "p" "r" "i" "g" "h" "t" "h" "a" "r" "p" "o" "o" "n")) ("↾")) +((("\\" "u" "p" "s" "i" "l" "o" "n")) ("υ")) +((("\\" "u" "p" "u" "p" "a" "r" "r" "o" "w" "s")) ("⇈")) +((("\\" "u" "r" "c" "o" "r" "n" "e" "r")) ("⌝")) +((("\\" "u" "{" "i" "}")) ("ĭ")) +((("\\" "v" "D" "a" "s" "h")) ("⊨")) +((("\\" "v" "a" "r" "k" "a" "p" "p" "a")) ("ϰ")) +((("\\" "v" "a" "r" "p" "h" "i")) ("ϕ")) +((("\\" "v" "a" "r" "p" "i")) ("ϖ")) +((("\\" "v" "a" "r" "p" "r" "i" "m" "e")) ("′")) +((("\\" "v" "a" "r" "p" "r" "o" "p" "t" "o")) ("∝")) +((("\\" "v" "a" "r" "r" "h" "o")) ("ϱ")) +((("\\" "v" "a" "r" "s" "i" "g" "m" "a")) ("ς")) +((("\\" "v" "a" "r" "t" "h" "e" "t" "a")) ("ϑ")) +((("\\" "v" "a" "r" "t" "r" "i" "a" "n" "g" "l" "e" "l" "e" "f" "t")) ("⊲")) +((("\\" "v" "a" "r" "t" "r" "i" "a" "n" "g" "l" "e" "r" "i" "g" "h" "t")) ("⊳")) +((("\\" "v" "d" "a" "s" "h")) ("⊢")) +((("\\" "v" "d" "o" "t" "s")) ("⋮")) +((("\\" "v" "e" "e")) ("∨")) +((("\\" "v" "e" "e" "b" "a" "r")) ("⊻")) +((("\\" "v" "e" "r" "t")) ("|")) +((("\\" "w" "e" "d" "g" "e")) ("∧")) +((("\\" "w" "p")) ("℘")) +((("\\" "w" "r")) ("≀")) +((("\\" "x" "i")) ("ξ")) +((("\\" "z" "e" "t" "a")) ("ζ")) +((("\\" "B" "b" "b" "{" "N" "}")) ("ℕ")) +((("\\" "B" "b" "b" "{" "P" "}")) ("ℙ")) +((("\\" "B" "b" "b" "{" "R" "}")) ("ℝ")) +((("\\" "B" "b" "b" "{" "Z" "}")) ("ℤ")) +((("-" "-")) ("–")) +((("-" "-" "-")) ("—")) +((("\\" " ")) (" ")) +((("\\" "\\")) ("\\")) +((("\\" "m" "u")) ("μ")) +((("\\" "r" "h" "o")) ("ρ")) +((("\\" "m" "a" "t" "h" "s" "c" "r" "{" "I" "}")) ("ℐ")) +((("\\" "S" "m" "i" "l" "e" "y")) ("☺")) +((("\\" "b" "l" "a" "c" "k" "s" "m" "i" "l" "e" "y")) ("☻")) +((("\\" "F" "r" "o" "w" "n" "y")) ("☹")) +((("\\" "L" "e" "t" "t" "e" "r")) ("✉")) +((("\\" "p" "e" "r" "m" "i" "l")) ("‰")) +((("\\" "r" "e" "g" "i" "s" "t" "e" "r" "e" "d")) ("®")) +((("\\" "c" "u" "r" "r" "e" "n" "c" "y")) ("¤")) +((("\\" "d" "h")) ("ð")) +((("\\" "D" "H")) ("Ð")) +((("\\" "t" "h")) ("þ")) +((("\\" "T" "H")) ("Þ")) +((("\\" "m" "i" "c" "r" "o")) ("µ")) +((("\\" "l" "n" "o" "t")) ("¬")) +((("\\" "o" "r" "d" "f" "e" "m" "i" "n" "i" "n" "e")) ("ª")) +((("\\" "o" "r" "d" "m" "a" "s" "c" "u" "l" "i" "n" "e")) ("º")) +((("\\" "l" "a" "m" "b" "d" "a" "b" "a" "r")) ("ƛ")) +((("\\" "c" "e" "l" "s" "i" "u" "s")) ("℃")) +((("\\" "l" "d" "q")) ("“")) +((("\\" "r" "d" "q")) ("”")) +((("\\" "m" "i" "n" "u" "s")) ("−")) +((("\\" "d" "e" "f" "s")) ("≙")) +((("\\" "l" "l" "b" "r" "a" "c" "k" "e" "t")) ("〚")) +((("\\" "r" "r" "b" "r" "a" "c" "k" "e" "t")) ("〛")) +((("\\" "l" "d" "a" "t" "a")) ("《")) +((("\\" "r" "d" "a" "t" "a")) ("》")) +((("\\" "g" "l" "q")) ("‚")) +((("\\" "g" "r" "q")) ("‘")) +((("\\" "g" "l" "q" "q")) ("„")) +((("\\" "\"" "`")) ("„")) +((("\\" "g" "r" "q" "q")) ("“")) +((("\\" "\"" "'")) ("“")) +((("\\" "f" "l" "q")) ("‹")) +((("\\" "f" "r" "q")) ("›")) +((("\\" "f" "l" "q" "q")) ("«")) +((("\\" "\"" "<")) ("«")) +((("\\" "f" "r" "q" "q")) ("»")) +((("\\" "\"" ">")) ("»")) +((("\\" "-")) ("")) +((("\\" "t" "e" "x" "t" "m" "u")) ("µ")) +((("\\" "t" "e" "x" "t" "f" "r" "a" "c" "t" "i" "o" "n" "s" "o" "l" "i" "d" "u" "s")) ("⁄")) +((("\\" "t" "e" "x" "t" "b" "i" "g" "c" "i" "r" "c" "l" "e")) ("⃝")) +((("\\" "t" "e" "x" "t" "m" "u" "s" "i" "c" "a" "l" "n" "o" "t" "e")) ("♪")) +((("\\" "t" "e" "x" "t" "d" "i" "e" "d")) ("✝")) +((("\\" "t" "e" "x" "t" "c" "o" "l" "o" "n" "m" "o" "n" "e" "t" "a" "r" "y")) ("₡")) +((("\\" "t" "e" "x" "t" "w" "o" "n")) ("₩")) +((("\\" "t" "e" "x" "t" "n" "a" "i" "r" "a")) ("₦")) +((("\\" "t" "e" "x" "t" "p" "e" "s" "o")) ("₱")) +((("\\" "t" "e" "x" "t" "l" "i" "r" "a")) ("₤")) +((("\\" "t" "e" "x" "t" "r" "e" "c" "i" "p" "e")) ("℞")) +((("\\" "t" "e" "x" "t" "i" "n" "t" "e" "r" "r" "o" "b" "a" "n" "g")) ("‽")) +((("\\" "t" "e" "x" "t" "p" "e" "r" "t" "e" "n" "t" "h" "o" "u" "s" "a" "n" "d")) ("‱")) +((("\\" "t" "e" "x" "t" "b" "a" "h" "t")) ("฿")) +((("\\" "t" "e" "x" "t" "n" "u" "m" "e" "r" "o")) ("№")) +((("\\" "t" "e" "x" "t" "d" "i" "s" "c" "o" "u" "n" "t")) ("⁒")) +((("\\" "t" "e" "x" "t" "e" "s" "t" "i" "m" "a" "t" "e" "d")) ("℮")) +((("\\" "t" "e" "x" "t" "o" "p" "e" "n" "b" "u" "l" "l" "e" "t")) ("◦")) +((("\\" "t" "e" "x" "t" "l" "q" "u" "i" "l" "l")) ("⁅")) +((("\\" "t" "e" "x" "t" "r" "q" "u" "i" "l" "l")) ("⁆")) +((("\\" "t" "e" "x" "t" "c" "i" "r" "c" "l" "e" "d" "P")) ("℗")) +((("\\" "t" "e" "x" "t" "r" "e" "f" "e" "r" "e" "n" "c" "e" "m" "a" "r" "k")) ("※")) +)) + +;; Local Variables: +;; mode: scheme +;; coding: utf-8 +;; End: diff --git a/ide/uim/coqide.scm b/ide/uim/coqide.scm new file mode 100644 index 00000000..62355ac2 --- /dev/null +++ b/ide/uim/coqide.scm @@ -0,0 +1,277 @@ +;;; coqide.scm -- Emacs-style Latin characters translation +;;; +;;; Copyright (c) 2003-2009 uim Project http://code.google.com/p/uim/ +;;; +;;; All rights reserved. +;;; +;;; Redistribution and use in source and binary forms, with or without +;;; modification, are permitted provided that the following conditions +;;; are met: +;;; 1. Redistributions of source code must retain the above copyright +;;; notice, this list of conditions and the following disclaimer. +;;; 2. Redistributions in binary form must reproduce the above copyright +;;; notice, this list of conditions and the following disclaimer in the +;;; documentation and/or other materials provided with the distribution. +;;; 3. Neither the name of authors nor the names of its contributors +;;; may be used to endorse or promote products derived from this software +;;; without specific prior written permission. +;;; +;;; THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS ``AS IS'' AND +;;; ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE +;;; IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE +;;; ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS OR CONTRIBUTORS BE LIABLE +;;; FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL +;;; DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS +;;; OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) +;;; HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT +;;; LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY +;;; OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF +;;; SUCH DAMAGE. +;;;; + +;; This input method implements character composition rules for the +;; Latin letters used in European languages. The rules, defined in +;; the file coqide-rules.scm, have been adapted from GNU Emacs 22. + +(require "util.scm") +(require "rk.scm") +(require "coqide-rules.scm") +(require-custom "generic-key-custom.scm") +(require-custom "coqide-custom.scm") + +(define coqide-context-rec-spec + (append + context-rec-spec + '((on #f) + (rkc #f) + (show-cands #f)))) +(define-record 'coqide-context coqide-context-rec-spec) +(define coqide-context-new-internal coqide-context-new) + +(define (coqide-context-new id im) + (let ((lc (coqide-context-new-internal id im)) + (rkc (rk-context-new (symbol-value coqide-rules) #f #f))) + (coqide-context-set-widgets! lc coqide-widgets) + (coqide-context-set-rkc! lc rkc) + lc)) + +(define (coqide-current-translation lc) + (let ((rkc (coqide-context-rkc lc))) + (or (rk-peek-terminal-match rkc) + (and (not (null? (rk-context-seq rkc))) + (list (rk-pending rkc)))))) + +(define (coqide-current-string lc) + (let ((trans (coqide-current-translation lc))) + (if trans (car trans) ""))) + +(define (coqide-context-clear lc) + (rk-flush (coqide-context-rkc lc))) + +(define (coqide-context-flush lc) + (let ((str (coqide-current-string lc))) + (if (not (equal? str "")) (im-commit lc str)) + (coqide-context-clear lc))) + +(define (coqide-open-candidates-window lc height) + (if (coqide-context-show-cands lc) + (im-deactivate-candidate-selector lc)) + (im-activate-candidate-selector lc height height) + (im-select-candidate lc 0) + (coqide-context-set-show-cands! lc #t)) + +(define (coqide-close-candidates-window lc) + (if (coqide-context-show-cands lc) + (im-deactivate-candidate-selector lc)) + (coqide-context-set-show-cands! lc #f)) + +(define (coqide-update-preedit lc) + (if (coqide-context-on lc) + (let ((trans (coqide-current-translation lc)) + (ltrans 0)) + (im-clear-preedit lc) + (if trans + (begin (im-pushback-preedit lc + preedit-underline + (car trans)) + (set! ltrans (length trans)))) + (im-pushback-preedit lc + preedit-cursor + "") + (im-update-preedit lc) + (if (> ltrans 1) + (coqide-open-candidates-window lc ltrans) + (coqide-close-candidates-window lc))))) + +(define (coqide-prepare-activation lc) + (coqide-context-flush lc) + (coqide-update-preedit lc)) + +(register-action 'action_coqide_off + (lambda (lc) + (list + 'off + "a" + (N_ "CoqIDE mode off") + (N_ "CoqIDE composition off"))) + (lambda (lc) + (not (coqide-context-on lc))) + (lambda (lc) + (coqide-prepare-activation lc) + (coqide-context-set-on! lc #f))) + +(register-action 'action_coqide_on + (lambda (lc) + (list + 'on + "à" + (N_ "CoqIDE mode on") + (N_ "CoqIDE composition on"))) + (lambda (lc) + (coqide-context-on lc)) + (lambda (lc) + (coqide-prepare-activation lc) + (coqide-context-set-on! lc #t))) + +(define coqide-input-mode-actions + '(action_coqide_off action_coqide_on)) + +(define coqide-widgets '(widget_coqide_input_mode)) + +(define default-widget_coqide_input_mode 'action_coqide_on) + +(register-widget 'widget_coqide_input_mode + (activity-indicator-new coqide-input-mode-actions) + (actions-new coqide-input-mode-actions)) + +(define coqide-context-list '()) + +(define (coqide-init-handler id im arg) + (let ((lc (coqide-context-new id im))) + (set! coqide-context-list (cons lc coqide-context-list)) + lc)) + +(define (coqide-release-handler lc) + (let ((rkc (coqide-context-rkc lc))) + (set! coqide-context-list + ;; (delete lc coqide-context-list eq?) does not work + (remove (lambda (c) (eq? (coqide-context-rkc c) rkc)) + coqide-context-list)))) + +(define coqide-control-key? + (let ((shift-or-no-modifier? (make-key-predicate '("<Shift>" "")))) + (lambda (key key-state) + (not (shift-or-no-modifier? -1 key-state))))) + +(define (coqide-proc-on-state lc key key-state) + (let ((rkc (coqide-context-rkc lc)) + (cur-trans (coqide-current-translation lc))) + (cond + + ((or (coqide-off-key? key key-state) + (and coqide-esc-turns-off? (eq? key 'escape))) + (coqide-context-flush lc) + (if (eq? key 'escape) + (im-commit-raw lc)) + (coqide-context-set-on! lc #f) + (coqide-close-candidates-window lc) + (im-clear-preedit lc) + (im-update-preedit lc)) + + ((coqide-backspace-key? key key-state) + (if (not (rk-backspace rkc)) + (im-commit-raw lc))) + + ((coqide-control-key? key key-state) + (coqide-context-flush lc) + (im-commit-raw lc)) + + ((and (ichar-numeric? key) + (coqide-context-show-cands lc) + (let ((idx (- (numeric-ichar->integer key) 1))) + (if (= idx -1) (set! idx 9)) + (and (>= idx 0) (< idx (length cur-trans)) + (begin + (im-commit lc (nth idx cur-trans)) + (coqide-context-clear lc) + #t))))) + + (else + (let* ((key-str (if (symbol? key) + (symbol->string key) + (charcode->string key))) + (cur-seq (rk-context-seq rkc)) + (res (rk-push-key! rkc key-str)) + (new-seq (rk-context-seq rkc)) + (new-trans (coqide-current-translation lc))) + (if (equal? new-seq (cons key-str cur-seq)) + (if (not (or (rk-partial? rkc) (> (length new-trans) 1))) + (begin (im-commit lc (car (rk-peek-terminal-match rkc))) + (coqide-context-clear lc))) + (begin (if (not (null? cur-seq)) (im-commit lc (car cur-trans))) + (if (null? new-seq) (im-commit-raw lc))))))))) + +(define (coqide-proc-off-state lc key key-state) + (if (coqide-on-key? key key-state) + (coqide-context-set-on! lc #t) + (im-commit-raw lc))) + +(define (coqide-key-press-handler lc key key-state) + (if (coqide-context-on lc) + (coqide-proc-on-state lc key key-state) + (coqide-proc-off-state lc key key-state)) + (coqide-update-preedit lc)) + +(define (coqide-key-release-handler lc key key-state) + (if (or (ichar-control? key) + (not (coqide-context-on lc))) + ;; don't discard key release event for apps + (im-commit-raw lc))) + +(define (coqide-reset-handler lc) + (coqide-context-clear lc)) + +(define (coqide-get-candidate-handler lc idx accel-enum-hint) + (let* ((candidates (coqide-current-translation lc)) + (candidate (nth idx candidates))) + (list candidate (digit->string (+ idx 1)) ""))) + +;; Emacs does nothing on focus-out +;; TODO: this should be configurable +(define (coqide-focus-out-handler lc) + #f) + +(define (coqide-place-handler lc) + (coqide-update-preedit lc)) + +(define (coqide-displace-handler lc) + (coqide-context-flush lc) + (coqide-update-preedit lc)) + +(register-im + 'coqide + "" + "UTF-8" + coqide-im-name-label + coqide-im-short-desc + #f + coqide-init-handler + coqide-release-handler + context-mode-handler + coqide-key-press-handler + coqide-key-release-handler + coqide-reset-handler + coqide-get-candidate-handler + #f + context-prop-activate-handler + #f + #f + coqide-focus-out-handler + coqide-place-handler + coqide-displace-handler +) + +;; Local Variables: +;; mode: scheme +;; coding: utf-8 +;; End: diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d918e94d..524448a6 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: constrintern.ml 13492 2010-10-04 21:20:01Z herbelin $ *) +(* $Id: constrintern.ml 13620 2010-11-04 14:11:49Z herbelin $ *) open Pp open Util @@ -266,6 +266,9 @@ let set_var_scope loc id istermvar (_,_,scopt,scopes) ntnvars = try let idscopes,typ = List.assoc id ntnvars in if !idscopes <> None & + (* scopes have no effect on the interpretation of identifiers, hence + we can tolerate having a variable occurring several times in + different scopes: *) typ <> NtnInternTypeIdent & make_current_scope (Option.get !idscopes) <> make_current_scope (scopt,scopes) then error_inconsistent_scope loc id diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 0a42b78b..020c3622 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: dumpglob.ml 13328 2010-07-26 11:05:30Z herbelin $ *) +(* $Id: dumpglob.ml 13674 2010-12-04 10:34:11Z herbelin $ *) (* Dump of globalization (to be used by coqdoc) *) @@ -181,15 +181,32 @@ let dump_libref loc dp ty = (fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty) let cook_notation df sc = + (* We encode notations so that they are space-free and still human-readable *) + (* - all spaces are replaced by _ *) + (* - all _ denoting a non-terminal symbol are replaced by x *) + (* - all terminal tokens are surrounded by single quotes, including '_' *) + (* which already denotes terminal _ *) + (* - all single quotes in terminal tokens are doubled *) + (* The output is decoded in function Index.prepare_entry of coqdoc *) let ntn = String.make (String.length df * 3) '_' in let j = ref 0 in - let quoted = ref false in - for i = 0 to String.length df - 1 do - if df.[i] = '\'' then quoted := not !quoted; - if df.[i] = ' ' then (ntn.[!j] <- '_'; incr j) else - if df.[i] = '_' && not !quoted then (ntn.[!j] <- 'x'; incr j) else - if df.[i] = 'x' && not !quoted then (String.blit "'x'" 0 ntn !j 3; j := !j + 3) else - (ntn.[!j] <- df.[i]; incr j) + let l = String.length df - 1 in + let i = ref 0 in + while !i <= l do + assert (df.[!i] <> ' '); + if df.[!i] = '_' && (!i = l || df.[!i+1] = ' ') then + (* Next token is a non-terminal *) + (ntn.[!j] <- 'x'; incr j; incr i) + else begin + (* Next token is a terminal *) + ntn.[!j] <- '\''; incr j; + while !i <= l && df.[!i] <> ' ' do + if df.[!i] = '\'' then (ntn.[!j] <- '\''; incr j); + ntn.[!j] <- df.[!i]; incr j; incr i + done; + ntn.[!j] <- '\''; incr j + end; + if !i <= l then (ntn.[!j] <- '_'; incr j; incr i) done; let df = String.sub ntn 0 !j in match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df diff --git a/interp/topconstr.ml b/interp/topconstr.ml index b8a90088..a358249f 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: topconstr.ml 13357 2010-07-29 22:59:55Z herbelin $ *) +(* $Id: topconstr.ml 13680 2010-12-04 15:06:06Z herbelin $ *) (*i*) open Pp @@ -115,11 +115,11 @@ let rawconstr_of_aconstr_with_binders loc g f e = function let outerl = [(ldots_var,inner)] in subst_rawvars outerl it | ALambda (na,ty,c) -> - let e,na = g e na in RLambda (loc,na,Explicit,f e ty,f e c) + let e',na = g e na in RLambda (loc,na,Explicit,f e ty,f e' c) | AProd (na,ty,c) -> - let e,na = g e na in RProd (loc,na,Explicit,f e ty,f e c) + let e',na = g e na in RProd (loc,na,Explicit,f e ty,f e' c) | ALetIn (na,b,c) -> - let e,na = g e na in RLetIn (loc,na,f e b,f e c) + let e',na = g e na in RLetIn (loc,na,f e b,f e' c) | ACases (sty,rtntypopt,tml,eqnl) -> let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') -> let e',t' = match t with @@ -137,18 +137,18 @@ let rawconstr_of_aconstr_with_binders loc g f e = function (loc,idl,patl,f e rhs)) eqnl in RCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl') | ALetTuple (nal,(na,po),b,c) -> - let e,nal = list_fold_map g e nal in - let e,na = g e na in - RLetTuple (loc,nal,(na,Option.map (f e) po),f e b,f e c) + let e',nal = list_fold_map g e nal in + let e'',na = g e na in + RLetTuple (loc,nal,(na,Option.map (f e'') po),f e b,f e' c) | AIf (c,(na,po),b1,b2) -> - let e,na = g e na in - RIf (loc,f e c,(na,Option.map (f e) po),f e b1,f e b2) + let e',na = g e na in + RIf (loc,f e c,(na,Option.map (f e') po),f e b1,f e b2) | ARec (fk,idl,dll,tl,bl) -> - let e,idl = array_fold_map (to_id g) e idl in let e,dll = array_fold_map (list_fold_map (fun e (na,oc,b) -> let e,na = g e na in (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in - RRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e) bl) + let e',idl = array_fold_map (to_id g) e idl in + RRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl) | ACast (c,k) -> RCast (loc,f e c, match k with | CastConv (k,t) -> CastConv (k,f e t) diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index cbff43ad..9216f2f3 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: subtyping.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: subtyping.ml 13616 2010-11-03 12:14:36Z soubiran $ i*) (*i*) open Util @@ -163,7 +163,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 match mind_of_delta reso2 kn2 with | kn2' when kn2=kn2' -> () | kn2' -> - if not (eq_mind (mind_of_delta reso1 kn1) kn2') then + if not (eq_mind (mind_of_delta reso1 kn1) (subst_ind subst2 kn2')) then error () end; (* we check that records and their field names are preserved. *) diff --git a/kernel/term.mli b/kernel/term.mli index f9e11df5..05a750b8 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: term.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: term.mli 13728 2010-12-19 11:35:20Z herbelin $ i*) (*i*) open Names @@ -507,7 +507,7 @@ val noccur_between : int -> int -> constr -> bool (* Checking function for terms containing existential- or meta-variables. The function [noccur_with_meta] does not consider - meta-variables applied to some terms (intented to be its local + meta-variables applied to some terms (intended to be its local context) (for existential variables, it is necessarily the case) *) val noccur_with_meta : int -> int -> constr -> bool diff --git a/kernel/univ.ml b/kernel/univ.ml index 77c14b10..9d93b16f 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: univ.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: univ.ml 13735 2010-12-21 18:21:58Z letouzey $ *) (* Initial Caml version originates from CoC 4.8 [Dec 1988] *) (* Extension with algebraic universes by HH [Sep 2001] *) @@ -115,15 +115,16 @@ let terminal u = {univ=u; lt=[]; le=[]} (* A universe_level is either an alias for another one, or a canonical one, for which we know the universes that are above *) + type univ_entry = Canonical of canonical_arc - | Equiv of universe_level * universe_level + | Equiv of universe_level type universes = univ_entry UniverseLMap.t let enter_equiv_arc u v g = - UniverseLMap.add u (Equiv(u,v)) g + UniverseLMap.add u (Equiv v) g let enter_arc ca g = UniverseLMap.add ca.univ (Canonical ca) g @@ -173,34 +174,13 @@ let repr g u = (str"Universe " ++ pr_uni_level u ++ str" undefined") in match a with - | Equiv(_,v) -> repr_rec v + | Equiv v -> repr_rec v | Canonical arc -> arc in repr_rec u let can g = List.map (repr g) -(* transitive closure : we follow the Less links *) - -(* collect : canonical_arc -> canonical_arc list * canonical_arc list *) -(* collect u = (V,W) iff V={v canonical | u<v} W={w canonical | u<=w}-V *) -(* i.e. collect does the transitive upward closure of what is known about u *) -let collect g arcu = - let rec coll_rec lt le = function - | [],[] -> (lt, list_subtractq le lt) - | arcv::lt', le' -> - if List.memq arcv lt then - coll_rec lt le (lt',le') - else - coll_rec (arcv::lt) le ((can g (arcv.lt@arcv.le))@lt',le') - | [], arcw::le' -> - if (List.memq arcw lt) or (List.memq arcw le) then - coll_rec lt le ([],le') - else - coll_rec lt (arcw::le) (can g arcw.lt, (can g arcw.le)@le') - in - coll_rec [] [] ([],[arcu]) - (* reprleq : canonical_arc -> canonical_arc list *) (* All canonical arcv such that arcu<=arcv with arcv#arcu *) let reprleq g arcu = @@ -252,20 +232,50 @@ let between g u arcv = type order = EQ | LT | LE | NLE -(* compare : universe_level -> universe_level -> order *) +(** [compare_neq] : is [arcv] in the transitive upward closure of [arcu] ? + + We try to avoid visiting unneeded parts of this transitive closure, + by stopping as soon as [arcv] is encountered. During the recursive + traversal, [lt_done] and [le_done] are universes we have already + visited, they do not contain [arcv]. The 3rd arg is + [(lt_todo,le_todo)], two lists of universes not yet considered, + known to be above [arcu], strictly or not. + + We use depth-first search, but the presence of [arcv] in [new_lt] + is checked as soon as possible : this seems to be slightly faster + on a test. +*) + +let compare_neq g arcu arcv = + let rec cmp lt_done le_done = function + | [],[] -> NLE + | arc::lt_todo, le_todo -> + if List.memq arc lt_done then + cmp lt_done le_done (lt_todo,le_todo) + else + let lt_new = can g (arc.lt@arc.le) in + if List.memq arcv lt_new then LT + else cmp (arc::lt_done) le_done (lt_new@lt_todo,le_todo) + | [], arc::le_todo -> + if arc == arcv then LE + (* No need to continue inspecting universes above arc: + if arcv is strictly above arc, then we would have a cycle *) + else + if (List.memq arc lt_done) || (List.memq arc le_done) then + cmp lt_done le_done ([],le_todo) + else + let lt_new = can g arc.lt in + if List.memq arcv lt_new then LT + else + let le_new = can g arc.le in + cmp lt_done (arc::le_done) (lt_new, le_new@le_todo) + in + cmp [] [] ([],[arcu]) + let compare g u v = let arcu = repr g u and arcv = repr g v in - if arcu==arcv then - EQ - else - let (lt,leq) = collect g arcu in - if List.memq arcv lt then - LT - else if List.memq arcv leq then - LE - else - NLE + if arcu == arcv then EQ else compare_neq g arcu arcv (* Invariants : compare(u,v) = EQ <=> compare(v,u) = EQ compare(u,v) = LT or LE => compare(v,u) = NLE @@ -299,9 +309,6 @@ let rec check_eq g u v = compare_list (compare_eq g) ult vlt | _ -> anomaly "check_eq" (* not complete! (Atom(u) = Max([u],[]) *) -let check_eq g u v = - check_eq g u v - let compare_greater g strict u v = let g = declare_univ u g in let g = declare_univ v g in @@ -429,21 +436,6 @@ let enforce_univ_lt u v g = | NLE -> setlt g u v | _ -> error_inconsistency Lt u v) -(* -let enforce_univ_relation g = function - | Equiv (u,v) -> enforce_univ_eq u v g - | Canonical {univ=u; lt=lt; le=le} -> - let g' = List.fold_right (enforce_univ_lt u) lt g in - List.fold_right (enforce_univ_leq u) le g' -*) - -(* Merging 2 universe graphs *) -(* -let merge_universes sp u1 u2 = - UniverseLMap.fold (fun _ a g -> enforce_univ_relation g a) u1 u2 -*) - - (* Constraints and sets of consrtaints. *) type constraint_type = Lt | Leq | Eq @@ -578,21 +570,21 @@ let num_edges g = UniverseLMap.fold (fun _ a n -> n + (reln_len a)) g 0 let pr_arc = function - | Canonical {univ=u; lt=[]; le=[]} -> + | _, Canonical {univ=u; lt=[]; le=[]} -> mt () - | Canonical {univ=u; lt=lt; le=le} -> + | _, Canonical {univ=u; lt=lt; le=le} -> pr_uni_level u ++ str " " ++ v 0 (prlist_with_sep pr_spc (fun v -> str "< " ++ pr_uni_level v) lt ++ (if lt <> [] & le <> [] then spc () else mt()) ++ prlist_with_sep pr_spc (fun v -> str "<= " ++ pr_uni_level v) le) ++ fnl () - | Equiv (u,v) -> + | u, Equiv v -> pr_uni_level u ++ str " = " ++ pr_uni_level v ++ fnl () let pr_universes g = - let graph = UniverseLMap.fold (fun k a l -> (k,a)::l) g [] in - prlist (function (_,a) -> pr_arc a) graph + let graph = UniverseLMap.fold (fun u a l -> (u,a)::l) g [] in + prlist pr_arc graph let pr_constraints c = Constraint.fold (fun (u1,op,u2) pp_std -> @@ -606,7 +598,7 @@ let pr_constraints c = (* Dumping constraints to a file *) let dump_universes output g = - let dump_arc _ = function + let dump_arc u = function | Canonical {univ=u; lt=lt; le=le} -> let u_str = string_of_univ_level u in List.iter @@ -619,7 +611,7 @@ let dump_universes output g = Printf.fprintf output "%s <= %s ;\n" u_str (string_of_univ_level v)) le - | Equiv (u,v) -> + | Equiv v -> Printf.fprintf output "%s = %s ;\n" (string_of_univ_level u) (string_of_univ_level v) in diff --git a/lib/compat.ml4 b/lib/compat.ml4 index 9b6bb19c..a77c2bc6 100644 --- a/lib/compat.ml4 +++ b/lib/compat.ml4 @@ -65,3 +65,15 @@ let unloc = M.unloc let join_loc = M.join_loc type token = M.token type lexer = M.lexer + +IFDEF CAMLP5_6_00 THEN + +let slist0sep x y = Gramext.Slist0sep (x, y, false) +let slist1sep x y = Gramext.Slist1sep (x, y, false) + +ELSE + +let slist0sep x y = Gramext.Slist0sep (x, y) +let slist1sep x y = Gramext.Slist1sep (x, y) + +END diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 304640b2..a00bb689 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -9,7 +9,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) (*i camlp4use: "pa_extend.cmo" i*) -(* $Id: g_vernac.ml4 13492 2010-10-04 21:20:01Z herbelin $ *) +(* $Id: g_vernac.ml4 13699 2010-12-09 19:24:45Z herbelin $ *) open Pp @@ -233,7 +233,7 @@ GEXTEND Gram def_body: [ [ bl = binders; ":="; red = reduce; c = lconstr -> (match c with - CCast(_,c, Rawterm.CastConv (k,t)) -> DefineBody (bl, red, c, Some t) + CCast(_,c, Rawterm.CastConv (Term.DEFAULTcast,t)) -> DefineBody (bl, red, c, Some t) | _ -> DefineBody (bl, red, c, None)) | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> DefineBody (bl, red, c, Some t) diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 90a9220f..14d50e6c 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -8,7 +8,7 @@ (*i camlp4use: "pa_extend.cmo pa_macro.cmo" i*) -(*i $Id: pcoq.ml4 13329 2010-07-26 11:05:39Z herbelin $ i*) +(*i $Id: pcoq.ml4 13690 2010-12-06 16:15:54Z glondu $ i*) open Pp open Util @@ -145,6 +145,11 @@ module Gram = G.delete_rule e pil end +IFDEF CAMLP5_6_02_1 THEN +let entry_print x = Gram.Entry.print !Pp_control.std_ft x +ELSE +let entry_print = Gram.Entry.print +END let camlp4_verbosity silent f x = let a = !Gramext.warning_verbose in @@ -631,16 +636,16 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ = | ETConstrList (typ',[]) -> Gramext.Slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ')) | ETConstrList (typ',tkl) -> - Gramext.Slist1sep - (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'), - make_sep_rules tkl) + Compat.slist1sep + (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ')) + (make_sep_rules tkl) | ETBinderList (false,[]) -> Gramext.Slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false)) | ETBinderList (false,tkl) -> - Gramext.Slist1sep - (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false), - make_sep_rules tkl) + Compat.slist1sep + (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false)) + (make_sep_rules tkl) | _ -> match interp_constr_prod_entry_key assoc from forpat typ with | (eobj,None,_) -> Gramext.Snterm (Gram.Entry.obj eobj) @@ -654,16 +659,16 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ = let rec symbol_of_prod_entry_key = function | Alist1 s -> Gramext.Slist1 (symbol_of_prod_entry_key s) | Alist1sep (s,sep) -> - Gramext.Slist1sep (symbol_of_prod_entry_key s, Gramext.Stoken ("",sep)) + Compat.slist1sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", sep)) | Alist0 s -> Gramext.Slist0 (symbol_of_prod_entry_key s) | Alist0sep (s,sep) -> - Gramext.Slist0sep (symbol_of_prod_entry_key s, Gramext.Stoken ("",sep)) + Compat.slist0sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", sep)) | Aopt s -> Gramext.Sopt (symbol_of_prod_entry_key s) | Amodifiers s -> Gramext.srules [([], Gramext.action(fun _loc -> [])); ([Gramext.Stoken ("", "("); - Gramext.Slist1sep ((symbol_of_prod_entry_key s), Gramext.Stoken ("", ",")); + Compat.slist1sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", ",")); Gramext.Stoken ("", ")")], Gramext.action (fun _ l _ _loc -> l))] | Aself -> Gramext.Sself diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index e4566e77..4eb06088 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pcoq.mli 13329 2010-07-26 11:05:39Z herbelin $ i*) +(*i $Id: pcoq.mli 13690 2010-12-06 16:15:54Z glondu $ i*) open Util open Names @@ -23,6 +23,8 @@ open Libnames module Gram : Grammar.S with type te = Compat.token +val entry_print : 'a Gram.Entry.e -> unit + (**********************************************************************) (* The parser of Coq is built from three kinds of rule declarations: - dynamic rules declared at the evaluation of Coq files (using diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml index 34b32c0a..ceadd26e 100644 --- a/plugins/dp/dp.ml +++ b/plugins/dp/dp.ml @@ -719,7 +719,7 @@ and tr_formula tv bv env f = | _, [a;b] when c = Lazy.force coq_iff -> Iff (tr_formula tv bv env a, tr_formula tv bv env b) | Prod (n, a, b), _ -> - if is_imp_term f then + if is_Prop (Typing.type_of env Evd.empty a) then Imp (tr_formula tv bv env a, tr_formula tv bv env b) else let id, t, bv, env, b = quantifiers n a b tv bv env in diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index b615955f..5329c675 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extraction.ml 13427 2010-09-17 17:37:52Z letouzey $ i*) +(*i $Id: extraction.ml 13733 2010-12-21 13:08:53Z letouzey $ i*) (*i*) open Util @@ -29,7 +29,7 @@ open Table open Mlutil (*i*) -exception I of inductive_info +exception I of inductive_kind (* A set of all fixpoint functions currently being extracted *) let current_fixpoints = ref ([] : constant list) @@ -368,7 +368,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) in add_ind kn mib - {ind_info = Standard; + {ind_kind = Standard; ind_nparams = npar; ind_packets = packets; ind_equiv = equiv @@ -453,7 +453,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) Record field_glob with (I info) -> info in - let i = {ind_info = ind_info; + let i = {ind_kind = ind_info; ind_nparams = npar; ind_packets = packets; ind_equiv = equiv } @@ -711,9 +711,15 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = let magic1 = needs_magic (type_cons, type_recomp (metas, a)) in let magic2 = needs_magic (a, mlt) in let head mla = - if mi.ind_info = Singleton then + if mi.ind_kind = Singleton then put_magic_if magic1 (List.hd mla) (* assert (List.length mla = 1) *) - else put_magic_if magic1 (MLcons (mi.ind_info, ConstructRef cp, mla)) + else + let typeargs = match snd (type_decomp type_cons) with + | Tglob (_,l) -> List.map type_simpl l + | _ -> assert false + in + let info = {c_kind = mi.ind_kind; c_typs = typeargs} in + put_magic_if magic1 (MLcons (info, ConstructRef cp, mla)) in (* Different situations depending of the number of arguments: *) if la < params_nb then @@ -779,7 +785,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = let e' = handle_exn r (List.length s) (fun _ -> Anonymous) e in (r, List.rev ids, e') in - if mi.ind_info = Singleton then + if mi.ind_kind = Singleton then begin (* Informative singleton case: *) (* [match c with C i -> t] becomes [let i = c' in t'] *) @@ -790,7 +796,9 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = end else (* Standard case: we apply [extract_branch]. *) - MLcase ((mi.ind_info,BranchNone), a, Array.init br_size extract_branch) + let typs = List.map type_simpl (Array.to_list metas) in + let info = { m_kind = mi.ind_kind; m_typs = typs; m_same = BranchNone } + in MLcase (info, a, Array.init br_size extract_branch) (*s Extraction of a (co)-fixpoint. *) diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 29d3da4d..1c47ad81 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: haskell.ml 13414 2010-09-14 13:28:15Z glondu $ i*) +(*i $Id: haskell.ml 13733 2010-12-21 13:08:53Z letouzey $ i*) (*s Production of Haskell syntax. *) @@ -156,10 +156,10 @@ let rec pp_expr par env args = hov 2 (str (find_custom_match pv) ++ fnl () ++ prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv ++ pp_expr true env [] t) - | MLcase ((_,factors),t, pv) -> + | MLcase (info,t, pv) -> apply (pp_par par' (v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++ - fnl () ++ str " " ++ pp_pat env factors pv))) + fnl () ++ str " " ++ pp_pat env info pv))) | MLfix (i,ids,defs) -> let ids',env' = push_vars (List.rev (Array.to_list ids)) env in pp_fix par env' i (Array.of_list (List.rev ids'),defs) args @@ -172,7 +172,7 @@ let rec pp_expr par env args = pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args) | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"") -and pp_pat env factors pv = +and pp_pat env info pv = let pp_one_pat (name,ids,t) = let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in let par = expr_needs_par t in @@ -184,27 +184,32 @@ and pp_pat env factors pv = (fun () -> (spc ())) pr_id (List.rev ids))) ++ str " ->" ++ spc () ++ pp_expr par env' [] t) in - let factor_br, factor_l = try match factors with - | BranchFun (i::_ as l) -> check_function_branch pv.(i), l - | BranchCst (i::_ as l) -> ast_pop (check_constant_branch pv.(i)), l - | _ -> MLdummy, [] - with Impossible -> MLdummy, [] + let factor_br, factor_set = try match info.m_same with + | BranchFun ints -> + let i = Intset.choose ints in + branch_as_fun info.m_typs pv.(i), ints + | BranchCst ints -> + let i = Intset.choose ints in + ast_pop (branch_as_cst pv.(i)), ints + | BranchNone -> MLdummy, Intset.empty + with _ -> MLdummy, Intset.empty in - let par = expr_needs_par factor_br in let last = Array.length pv - 1 in prvecti - (fun i x -> if List.mem i factor_l then mt () else + (fun i x -> if Intset.mem i factor_set then mt () else (pp_one_pat pv.(i) ++ - if i = last && factor_l = [] then mt () else + if i = last && Intset.is_empty factor_set then mt () else fnl () ++ str " ")) pv ++ - if factor_l = [] then mt () else match factors with + if Intset.is_empty factor_set then mt () else + let par = expr_needs_par factor_br in + match info.m_same with | BranchFun _ -> - let ids, env' = push_vars [anonymous_name] env in - pr_id (List.hd ids) ++ str " ->" ++ spc () ++ - pp_expr par env' [] factor_br + let ids, env' = push_vars [anonymous_name] env in + pr_id (List.hd ids) ++ str " ->" ++ spc () ++ + pp_expr par env' [] factor_br | BranchCst _ -> - str "_ ->" ++ spc () ++ pp_expr par env [] factor_br + str "_ ->" ++ spc () ++ pp_expr par env [] factor_br | BranchNone -> mt () (*s names of the functions ([ids]) are already pushed in [env], @@ -286,7 +291,7 @@ let rec pp_ind first kn i ind = let pp_string_parameters ids = prlist (fun id -> str id ++ str " ") let pp_decl = function - | Dind (kn,i) when i.ind_info = Singleton -> + | Dind (kn,i) when i.ind_kind = Singleton -> pp_singleton (mind_of_kn kn) i.ind_packets.(0) ++ fnl () | Dind (kn,i) -> hov 0 (pp_ind true (mind_of_kn kn) 0 i) | Dtype (r, l, t) -> diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index 7ff11b90..20092815 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: miniml.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: miniml.mli 13733 2010-12-21 13:08:53Z letouzey $ i*) (*s Target language for extraction: a core ML called MiniML. *) @@ -53,7 +53,7 @@ type ml_schema = int * ml_type (*s ML inductive types. *) -type inductive_info = +type inductive_kind = | Singleton | Coinductive | Standard @@ -85,7 +85,7 @@ type equiv = | RenEquiv of string type ml_ind = { - ind_info : inductive_info; + ind_kind : inductive_kind; ind_nparams : int; ind_packets : ml_ind_packet array; ind_equiv : equiv @@ -98,12 +98,27 @@ type ml_ident = | Id of identifier | Tmp of identifier -(* list of branches to merge in a common pattern *) +(** We now store some typing information on constructors + and cases to avoid type-unsafe optimisations. + For cases, we also store the set of branches to merge + in a common pattern, either "_ -> c" or "x -> f x" +*) + +type constructor_info = { + c_kind : inductive_kind; + c_typs : ml_type list; +} -type case_info = +type branch_same = | BranchNone - | BranchFun of int list - | BranchCst of int list + | BranchFun of Intset.t + | BranchCst of Intset.t + +type match_info = { + m_kind : inductive_kind; + m_typs : ml_type list; + m_same : branch_same +} type ml_branch = global_reference * ml_ident list * ml_ast @@ -113,8 +128,8 @@ and ml_ast = | MLlam of ml_ident * ml_ast | MLletin of ml_ident * ml_ast * ml_ast | MLglob of global_reference - | MLcons of inductive_info * global_reference * ml_ast list - | MLcase of (inductive_info*case_info) * ml_ast * ml_branch array + | MLcons of constructor_info * global_reference * ml_ast list + | MLcase of match_info * ml_ast * ml_branch array | MLfix of int * identifier array * ml_ast array | MLexn of string | MLdummy diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index a079aacc..d467f508 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mlutil.ml 13420 2010-09-16 15:47:08Z letouzey $ i*) +(*i $Id: mlutil.ml 13733 2010-12-21 13:08:53Z letouzey $ i*) (*i*) open Pp @@ -291,6 +291,8 @@ let type_expand env t = | a -> a in if Table.type_expand () then expand t else t +let type_simpl = type_expand (fun _ -> None) + (*s Generating a signature from a ML type. *) let type_to_sign env t = match type_expand env t with @@ -665,12 +667,23 @@ let rec ast_glob_subst s t = match t with (*S Auxiliary functions used in simplification of ML cases. *) -(*s [check_function_branch (r,l,c)] checks if branch [c] can be seen +(* Factorisation of some match branches into a common "x -> f x" + branch may break types sometimes. Example: [type 'x a = A]. + Then [let id = function A -> A] has type ['x a -> 'y a], + which is incompatible with the type of [let id x = x]. + We now check that the type arguments of the inductive are + preserved by our transformation. + + TODO: this verification should be done someday modulo + expansion of type definitions. +*) + +(*s [branch_as_function b typs (r,l,c)] tries to see branch [c] as a function [f] applied to [MLcons(r,l)]. For that it transforms - any [MLcons(r,l)] in [MLrel 1] and raises [Impossible] if any - variable in [l] occurs outside such a [MLcons] *) + any [MLcons(r,l)] in [MLrel 1] and raises [Impossible] + if any variable in [l] occurs outside such a [MLcons] *) -let check_function_branch (r,l,c) = +let branch_as_fun typs (r,l,c) = let nargs = List.length l in let rec genrec n = function | MLrel i as c -> @@ -678,22 +691,32 @@ let check_function_branch (r,l,c) = if i'<1 then c else if i'>nargs then MLrel (i-nargs+1) else raise Impossible - | MLcons(_,r',args) when r=r' && (test_eta_args_lift n nargs args) -> + | MLcons(i,r',args) when + r=r' && (test_eta_args_lift n nargs args) && typs = i.c_typs -> MLrel (n+1) | a -> ast_map_lift genrec n a in genrec 0 c -(*s [check_constant_branch (r,l,c)] checks if branch [c] is independent - from the pattern [MLcons(r,l)]. For that is raises [Impossible] if any - variable in [l] occurs in [c], and otherwise returns [c] lifted to - appear like a function with one arg (for uniformity with the - branch-as-function optimization) *) +(*s [branch_as_cst (r,l,c)] tries to see branch [c] as a constant + independent from the pattern [MLcons(r,l)]. For that is raises [Impossible] + if any variable in [l] occurs in [c], and otherwise returns [c] lifted to + appear like a function with one arg (for uniformity with [branch_as_fun]). + NB: [MLcons(r,l)] might occur nonetheless in [c], but only when [l] is + empty, i.e. when [r] is a constant constructor +*) -let check_constant_branch (_,l,c) = +let branch_as_cst (_,l,c) = let n = List.length l in if ast_occurs_itvl 1 n c then raise Impossible; ast_lift (1-n) c +(* A branch [MLcons(r,l)->c] can be seen at the same time as a function + branch and a constant branch, either because: + - [MLcons(r,l)] doesn't occur in [c]. For example : "A -> B" + - this constructor is constant (i.e. [l] is empty). For example "A -> A" + When searching for the best factorisation below, we'll try both. +*) + (* The following structure allows to record which element occurred at what position, and then finally return the most frequent element and its positions. *) @@ -702,61 +725,39 @@ let census_add, census_max, census_clean = let h = Hashtbl.create 13 in let clear () = Hashtbl.clear h in let add e i = - let l = try Hashtbl.find h e with Not_found -> [] in - Hashtbl.replace h e (i::l) + let s = try Hashtbl.find h e with Not_found -> Intset.empty in + Hashtbl.replace h e (Intset.add i s) in let max e0 = - let len = ref 0 and lst = ref [] and elm = ref e0 in + let len = ref 0 and lst = ref Intset.empty and elm = ref e0 in Hashtbl.iter - (fun e l -> - let n = List.length l in - if n > !len then begin len := n; lst := l; elm := e end) + (fun e s -> + let n = Intset.cardinal s in + if n > !len then begin len := n; lst := s; elm := e end) h; (!elm,!lst) in (add,max,clear) -(* Given an abstraction function [abstr] (one of [check_*_branch]), - return the longest possible list of branches that have the - same abstraction, along with this abstraction. *) +(* [factor_branches] return the longest possible list of branches + that have the same factorization, either as a function or as a + constant. +*) -let factor_branches abstr br = +let factor_branches o typs br = census_clean (); for i = 0 to Array.length br - 1 do - try census_add (abstr br.(i)) i with Impossible -> () + if o.opt_case_idr then + (try census_add (branch_as_fun typs br.(i)) i with Impossible -> ()); + if o.opt_case_cst then + (try census_add (branch_as_cst br.(i)) i with Impossible -> ()); done; - let br_factor, br_list = census_max MLdummy in - if br_list = [] then None - else if Array.length br >= 2 && List.length br_list < 2 then None - else Some (br_factor, br_list) - -(*s [check_generalizable_case] checks if all branches can be seen as the - same function [f] applied to the term matched. It is a generalized version - of both the identity case optimization and the constant case optimisation - ([f] can be a constant function) *) - -(* The optimisation [factor_branches check_function_branch] breaks types - in some special case. Example: [type 'x a = A]. - Then [let f = function A -> A] has type ['x a -> 'y a], - which is incompatible with the type of [let f x = x]. - We check first that there isn't such phantom variable in the inductive type - we're considering. *) - -let check_optim_id br = - let (kn,i) = - match br.(0) with (ConstructRef (c,_),_,_) -> c | _ -> assert false - in - let ip = (snd (lookup_ind kn)).ind_packets.(i) in - match ip.ip_optim_id_ok with - | Some ok -> ok - | None -> - let tvars = - intset_union_map_array (intset_union_map_list type_listvar) - ip.ip_types - in - let ok = (Intset.cardinal tvars = List.length ip.ip_vars) in - ip.ip_optim_id_ok <- Some ok; - ok + let br_factor, br_set = census_max MLdummy in + census_clean (); + let n = Intset.cardinal br_set in + if n = 0 then None + else if Array.length br >= 2 && n < 2 then None + else Some (br_factor, br_set) (*s If all branches are functions, try to permut the case and the functions. *) @@ -897,26 +898,14 @@ and simpl_case o i br e = if n <> 0 then simpl o (named_lams ids (MLcase (i,ast_lift n e, br))) else - (* Does a term [f] exist such that many branches are [(f e)] ? *) - let opt1 = - if o.opt_case_idr && (o.opt_case_idg || check_optim_id br) then - factor_branches check_function_branch br - else None - in - (* Detect common constant branches. Often a particular case of - branch-as-function optim, but not always (e.g. A->A|B->A) *) - let opt2 = - if opt1 = None && o.opt_case_cst then - factor_branches check_constant_branch br - else opt1 - in - match opt2 with - | Some (f,ints) when List.length ints = Array.length br -> - (* if all branches have been factorized, we remove the match *) + (* Can we merge several branches as the same constant or function ? *) + match factor_branches o i.m_typs br with + | Some (f,ints) when Intset.cardinal ints = Array.length br -> + (* If all branches have been factorized, we remove the match *) simpl o (MLletin (Tmp anonymous_name, e, f)) | Some (f,ints) -> - let ci = if ast_occurs 1 f then BranchFun ints else BranchCst ints - in MLcase ((fst i,ci), e, br) + let same = if ast_occurs 1 f then BranchFun ints else BranchCst ints + in MLcase ({i with m_same=same}, e, br) | None -> MLcase (i, e, br) (*S Local prop elimination. *) diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index d2ac48ea..6b0cd4f9 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mlutil.mli 13420 2010-09-16 15:47:08Z letouzey $ i*) +(*i $Id: mlutil.mli 13733 2010-12-21 13:08:53Z letouzey $ i*) open Util open Names @@ -63,6 +63,7 @@ val var2var' : ml_type -> ml_type type abbrev_map = global_reference -> ml_type option val type_expand : abbrev_map -> ml_type -> ml_type +val type_simpl : ml_type -> ml_type val type_to_sign : abbrev_map -> ml_type -> sign val type_to_signature : abbrev_map -> ml_type -> signature val type_expunge : abbrev_map -> ml_type -> ml_type @@ -116,8 +117,8 @@ val optimize_fix : ml_ast -> ml_ast val inline : global_reference -> ml_ast -> bool exception Impossible -val check_function_branch : ml_branch -> ml_ast -val check_constant_branch : ml_branch -> ml_ast +val branch_as_fun : ml_type list -> ml_branch -> ml_ast +val branch_as_cst : ml_branch -> ml_ast (* Classification of signatures *) diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index b4334750..313fc58d 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modutil.ml 13420 2010-09-16 15:47:08Z letouzey $ i*) +(*i $Id: modutil.ml 13733 2010-12-21 13:08:53Z letouzey $ i*) open Names open Declarations @@ -82,10 +82,10 @@ let ast_iter_references do_term do_cons do_type a = match a with | MLglob r -> do_term r | MLcons (i,r,_) -> - if lang () = Ocaml then record_iter_references do_term i; + if lang () = Ocaml then record_iter_references do_term i.c_kind; do_cons r | MLcase (i,_,v) -> - if lang () = Ocaml then record_iter_references do_term (fst i); + if lang () = Ocaml then record_iter_references do_term i.m_kind; Array.iter (fun (r,_,_) -> do_cons r) v | _ -> () in iter a @@ -101,7 +101,7 @@ let ind_iter_references do_term do_cons do_type kn ind = | _ -> ()); Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types in - if lang () = Ocaml then record_iter_references do_term ind.ind_info; + if lang () = Ocaml then record_iter_references do_term ind.ind_kind; Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets let decl_iter_references do_term do_cons do_type = diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 36ca3713..f136fab5 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ocaml.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: ocaml.ml 13733 2010-12-21 13:08:53Z letouzey $ i*) (*s Production of Ocaml syntax. *) @@ -218,17 +218,17 @@ let rec pp_expr par env args = when kn = ind_ascii && check_extract_ascii () & is_list_cons l -> assert (args=[]); pp_char l - | MLcons (Coinductive,r,[]) -> + | MLcons ({c_kind = Coinductive},r,[]) -> assert (args=[]); pp_par par (str "lazy " ++ pp_global Cons r) - | MLcons (Coinductive,r,args') -> + | MLcons ({c_kind = Coinductive},r,args') -> assert (args=[]); let tuple = pp_tuple (pp_expr true env []) args' in pp_par par (str "lazy (" ++ pp_global Cons r ++ spc() ++ tuple ++str ")") | MLcons (_,r,[]) -> assert (args=[]); pp_global Cons r - | MLcons (Record projs, r, args') -> + | MLcons ({c_kind = Record projs}, r, args') -> assert (args=[]); pp_record_pat (projs, List.map (pp_expr true env []) args') | MLcons (_,r,[arg1;arg2]) when is_infix r -> @@ -250,14 +250,14 @@ let rec pp_expr par env args = hov 2 (str (find_custom_match pv) ++ fnl () ++ prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv ++ pp_expr true env [] t) - | MLcase ((i,factors), t, pv) -> - let expr = if i = Coinductive then + | MLcase (info, t, pv) -> + let expr = if info.m_kind = Coinductive then (str "Lazy.force" ++ spc () ++ pp_expr true env [] t) else (pp_expr false env [] t) in (try - let projs = find_projections i in + let projs = find_projections info.m_kind in let (_, ids, c) = pv.(0) in let n = List.length ids in match c with @@ -277,7 +277,7 @@ let rec pp_expr par env args = | _ -> raise NoRecord with NoRecord -> if Array.length pv = 1 then - let s1,s2 = pp_one_pat env i pv.(0) in + let s1,s2 = pp_one_pat env info pv.(0) in apply (hv 0 (pp_par par' @@ -291,7 +291,7 @@ let rec pp_expr par env args = (try pp_ifthenelse par' env expr pv with Not_found -> v 0 (str "match " ++ expr ++ str " with" ++ fnl () ++ - str " | " ++ pp_pat env (i,factors) pv)))) + str " | " ++ pp_pat env info pv)))) | MLfix (i,ids,defs) -> let ids',env' = push_vars (List.rev (Array.to_list ids)) env in pp_fix par env' i (Array.of_list (List.rev ids'),defs) args @@ -324,11 +324,11 @@ and pp_ifthenelse par env expr pv = match pv with hov 2 (pp_expr (expr_needs_par els) env [] els))) | _ -> raise Not_found -and pp_one_pat env i (r,ids,t) = +and pp_one_pat env info (r,ids,t) = let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in let expr = pp_expr (expr_needs_par t) env' [] t in try - let projs = find_projections i in + let projs = find_projections info.m_kind in pp_record_pat (projs, List.rev_map pr_id ids), expr with NoRecord -> (match List.rev ids with @@ -340,36 +340,42 @@ and pp_one_pat env i (r,ids,t) = ++ pp_boxed_tuple pr_id ids), expr -and pp_pat env (info,factors) pv = - let factor_br, factor_l = try match factors with - | BranchFun (i::_ as l) -> check_function_branch pv.(i), l - | BranchCst (i::_ as l) -> ast_pop (check_constant_branch pv.(i)), l - | _ -> MLdummy, [] - with Impossible -> MLdummy, [] +and pp_pat env info pv = + let factor_br, factor_set = try match info.m_same with + | BranchFun ints -> + let i = Intset.choose ints in + branch_as_fun info.m_typs pv.(i), ints + | BranchCst ints -> + let i = Intset.choose ints in + ast_pop (branch_as_cst pv.(i)), ints + | BranchNone -> MLdummy, Intset.empty + with _ -> MLdummy, Intset.empty in - let par = expr_needs_par factor_br in let last = Array.length pv - 1 in prvecti - (fun i x -> if List.mem i factor_l then mt () else + (fun i x -> if Intset.mem i factor_set then mt () else let s1,s2 = pp_one_pat env info x in hov 2 (s1 ++ str " ->" ++ spc () ++ s2) ++ - if i = last && factor_l = [] then mt () else + if i = last && Intset.is_empty factor_set then mt () else fnl () ++ str " | ") pv ++ - if factor_l = [] then mt () else match factors with + if Intset.is_empty factor_set then mt () else + let par = expr_needs_par factor_br in + match info.m_same with | BranchFun _ -> - let ids, env' = push_vars [anonymous_name] env in - hov 2 (pr_id (List.hd ids) ++ str " ->" ++ spc () ++ - pp_expr par env' [] factor_br) + let ids, env' = push_vars [anonymous_name] env in + hov 2 (pr_id (List.hd ids) ++ str " ->" ++ spc () ++ + pp_expr par env' [] factor_br) | BranchCst _ -> - hov 2 (str "_ ->" ++ spc () ++ pp_expr par env [] factor_br) + hov 2 (str "_ ->" ++ spc () ++ pp_expr par env [] factor_br) | BranchNone -> mt () and pp_function env t = let bl,t' = collect_lams t in let bl,env' = push_vars (List.map id_of_mlid bl) env in match t' with - | MLcase(i,MLrel 1,pv) when fst i=Standard && not (is_custom_match pv) -> + | MLcase(i,MLrel 1,pv) when + i.m_kind = Standard && not (is_custom_match pv) -> if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then pr_binding (List.rev (List.tl bl)) ++ str " = function" ++ fnl () ++ @@ -519,7 +525,7 @@ let pp_ind co kn ind = (*s Pretty-printing of a declaration. *) let pp_mind kn i = - match i.ind_info with + match i.ind_kind with | Singleton -> pp_singleton kn i.ind_packets.(0) | Coinductive -> pp_ind true kn i | Record projs -> diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index fa293ba1..06098591 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: scheme.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: scheme.ml 13733 2010-12-21 13:08:53Z letouzey $ i*) (*s Production of Scheme syntax. *) @@ -87,7 +87,7 @@ let rec pp_expr env args = ++ spc () ++ hov 0 (pp_expr env' [] a2))))) | MLglob r -> apply (pp_global Term r) - | MLcons (i,r,args') -> + | MLcons (info,r,args') -> assert (args=[]); let st = str "`" ++ @@ -95,7 +95,7 @@ let rec pp_expr env args = (if args' = [] then mt () else spc ()) ++ prlist_with_sep spc (pp_cons_args env) args') in - if i = Coinductive then paren (str "delay " ++ st) else st + if info.c_kind = Coinductive then paren (str "delay " ++ st) else st | MLcase (_,t,pv) when is_custom_match pv -> let mkfun (_,ids,e) = if ids <> [] then named_lams (List.rev ids) e @@ -104,9 +104,9 @@ let rec pp_expr env args = hov 2 (str (find_custom_match pv) ++ fnl () ++ prvect (fun tr -> pp_expr env [] (mkfun tr) ++ fnl ()) pv ++ pp_expr env [] t) - | MLcase ((i,_),t, pv) -> + | MLcase (info,t, pv) -> let e = - if i <> Coinductive then pp_expr env [] t + if info.m_kind <> Coinductive then pp_expr env [] t else paren (str "force" ++ spc () ++ pp_expr env [] t) in apply (v 3 (paren (str "match " ++ e ++ fnl () ++ pp_pat env pv))) @@ -123,7 +123,7 @@ let rec pp_expr env args = | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"") and pp_cons_args env = function - | MLcons (i,r,args) when i<>Coinductive -> + | MLcons (info,r,args) when info.c_kind<>Coinductive -> paren (pp_global Cons r ++ (if args = [] then mt () else spc ()) ++ prlist_with_sep spc (pp_cons_args env) args) diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index a7e636ff..085c0a44 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: table.ml 13420 2010-09-16 15:47:08Z letouzey $ i*) +(*i $Id: table.ml 13733 2010-12-21 13:08:53Z letouzey $ i*) open Names open Term @@ -421,7 +421,8 @@ let flag_of_int n = opt_lin_beta = kth_digit n 10 } (* For the moment, we allow by default everything except : - - the type-unsafe optimization [opt_case_idg] + - the type-unsafe optimization [opt_case_idg], which anyway + cannot be activated currently (cf [Mlutil.branch_as_fun]) - the linear let and beta reduction [opt_lin_let] and [opt_lin_beta] (may lead to complexity blow-up, subsumed by finer reductions when inlining recursors). diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml index f1bdd640..3fb6824b 100644 --- a/plugins/subtac/eterm.ml +++ b/plugins/subtac/eterm.ml @@ -28,7 +28,7 @@ type oblinfo = ev_hyps: named_context; ev_status: obligation_definition_status; ev_chop: int option; - ev_loc: Util.loc; + ev_source: hole_kind located; ev_typ: types; ev_tac: tactic option; ev_deps: Intset.t } @@ -218,9 +218,9 @@ let eterm_obligations env name isevars evm fs ?status t ty = else None | None -> None in - let info = { ev_name = (n, nstr); - ev_hyps = hyps; ev_status = status; ev_chop = chop; - ev_loc = loc; ev_typ = evtyp ; ev_deps = deps; ev_tac = tac } + let info = { ev_name = (n, nstr); ev_hyps = hyps; + ev_status = status; ev_chop = chop; + ev_source = (loc, k); ev_typ = evtyp ; ev_deps = deps; ev_tac = tac } in (id, info) :: l) evn [] in @@ -231,12 +231,12 @@ let eterm_obligations env name isevars evm fs ?status t ty = let evars = List.map (fun (ev, info) -> let { ev_name = (_, name); ev_status = status; - ev_loc = loc; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info + ev_source = source; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info in let status = match status with | Define true when Idset.mem name transparent -> Define false | _ -> status - in name, typ, loc, status, deps, tac) evts + in name, typ, source, status, deps, tac) evts in let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in let evmap f c = pi1 (subst_evar_constr evts 0 f c) in diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli index 262889c8..2abc25a3 100644 --- a/plugins/subtac/eterm.mli +++ b/plugins/subtac/eterm.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: eterm.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: eterm.mli 13693 2010-12-08 15:32:25Z msozeau $ i*) open Environ open Tacmach open Term @@ -24,7 +24,7 @@ val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info * evars contexts, object and type *) val eterm_obligations : env -> identifier -> evar_map -> evar_map -> int -> ?status:obligation_definition_status -> constr -> types -> - (identifier * types * loc * obligation_definition_status * Intset.t * + (identifier * types * hole_kind located * obligation_definition_status * Intset.t * tactic option) array (* Existential key, obl. name, type as product, location of the original evar, associated tactic, status and dependencies as indexes into the array *) diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index b76d0cb0..d3a63410 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -30,13 +30,13 @@ let explain_no_obligations = function Some ident -> str "No obligations for program " ++ str (string_of_id ident) | None -> str "No obligations remaining" -type obligation_info = (Names.identifier * Term.types * loc * obligation_definition_status * Intset.t - * tactic option) array +type obligation_info = (Names.identifier * Term.types * hole_kind located * + obligation_definition_status * Intset.t * tactic option) array type obligation = { obl_name : identifier; obl_type : types; - obl_location : loc; + obl_source : hole_kind located; obl_body : constr option; obl_status : obligation_definition_status; obl_deps : Intset.t; @@ -307,14 +307,14 @@ let init_prog_info n b t deps fixkind notations obls impls kind reduce hook = assert(obls = [||]); let n = Nameops.add_suffix n "_obligation" in [| { obl_name = n; obl_body = None; - obl_location = dummy_loc; obl_type = t; + obl_source = (dummy_loc, QuestionMark Expand); obl_type = t; obl_status = Expand; obl_deps = Intset.empty; obl_tac = None } |], mkVar n | Some b -> Array.mapi (fun i (n, t, l, o, d, tac) -> { obl_name = n ; obl_body = None; - obl_location = l; obl_type = reduce t; obl_status = o; + obl_source = l; obl_type = reduce t; obl_status = o; obl_deps = d; obl_tac = tac }) obls, b in @@ -488,7 +488,7 @@ and solve_obligation_by_tac prg obls i tac = | Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s))) | Stdpp.Exc_located(_, Refiner.FailError (_, s)) | Refiner.FailError (_, s) -> - user_err_loc (obl.obl_location, "solve_obligation", Lazy.force s) + user_err_loc (fst obl.obl_source, "solve_obligation", Lazy.force s) | e -> false and solve_prg_obligations prg tac = diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli index bc5fc3e1..5f6d1a2e 100644 --- a/plugins/subtac/subtac_obligations.mli +++ b/plugins/subtac/subtac_obligations.mli @@ -6,9 +6,9 @@ open Proof_type open Vernacexpr type obligation_info = - (identifier * Term.types * loc * + (identifier * Term.types * hole_kind located * obligation_definition_status * Intset.t * tactic option) array - (* ident, type, location, (opaque or transparent, expand or define), + (* ident, type, source, (opaque or transparent, expand or define), dependencies, tactic to solve it *) type progress = (* Resolution status of a program *) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 09603d8b..bae89329 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml 13511 2010-10-06 20:48:16Z herbelin $ *) +(* $Id: cases.ml 13728 2010-12-19 11:35:20Z herbelin $ *) open Util open Names @@ -1648,9 +1648,11 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon pred = let sigma2,pred2 = build_inversion_problem loc env !evdref tomatchs t in [!evdref, KnownDep, pred1; sigma2, DepUnknown, pred2] | None, Some (None, t) -> - (* Only one strategy: we build an "inversion" predicate *) - let sigma,pred = build_inversion_problem loc env !evdref tomatchs t in - [sigma, DepUnknown, pred] + (* First strategy: we build an "inversion" predicate *) + let sigma1,pred = build_inversion_problem loc env !evdref tomatchs t in + (* Second strategy: we abstract the tycon wrt to the dependencies *) + let pred2 = lift (List.length names) t in + [sigma1, DepUnknown, pred; !evdref, KnownNotDep, pred2] | None, _ -> (* No type constaints: we use two strategies *) let t = mkExistential env ~src:(loc, CasesType) evdref in diff --git a/tactics/equality.ml b/tactics/equality.ml index 6b16adb4..7a774cc9 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: equality.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: equality.ml 13586 2010-10-27 17:42:13Z jforest $ *) open Pp open Util @@ -185,12 +185,30 @@ let find_elim hdcncl lft2rgt dep cls args gl = pf_conv_x gl (List.nth args 0) (List.nth args 2)) && not dep || Flags.version_less_or_equal Flags.V8_2 then - (* use eq_rect, eq_rect_r, JMeq_rect, etc for compatibility *) - let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in - let hdcncls = string_of_inductive hdcncl ^ suffix in - let rwr_thm = if lft2rgt = Some (cls=None) then hdcncls^"_r" else hdcncls in - try pf_global gl (id_of_string rwr_thm) - with Not_found -> error ("Cannot find rewrite principle "^rwr_thm^".") + match kind_of_term hdcncl with + | Ind ind_sp -> + let pr1 = + lookup_eliminator ind_sp (elimination_sort_of_clause cls gl) + in + if lft2rgt = Some (cls=None) + then + let c1 = destConst pr1 in + let mp,dp,l = repr_con (constant_of_kn (canonical_con c1)) in + let l' = label_of_id (add_suffix (id_of_label l) "_r") in + let c1' = Global.constant_of_delta (make_con mp dp l') in + begin + try + let _ = Global.lookup_constant c1' in + mkConst c1' + with Not_found -> + let rwr_thm = string_of_label l' in + error ("Cannot find rewrite principle "^rwr_thm^".") + end + else pr1 + | _ -> + (* cannot occur since we checked that we are in presence of + Logic.eq or Jmeq just before *) + assert false else let scheme_name = match dep, lft2rgt, inccl with (* Non dependent case with symmetric equality *) diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 3f069ab2..dfc8b6bf 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: extratactics.ml4 13434 2010-09-18 20:11:37Z msozeau $ *) +(* $Id: extratactics.ml4 13658 2010-11-29 11:09:05Z glondu $ *) open Pp open Pcoq @@ -545,7 +545,7 @@ let subst_var_with_hole occ tid t = | RVar (_,id) as x -> if id = tid then (decr occref; if !occref = 0 then x - else (incr locref; RHole (Ploc.make !locref 0 (0,0),Evd.QuestionMark(Evd.Define true)))) + else (incr locref; RHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true)))) else x | c -> map_rawconstr_left_to_right substrec c in let t' = substrec t @@ -558,7 +558,7 @@ let subst_hole_with_term occ tc t = let rec substrec = function | RHole (_,Evd.QuestionMark(Evd.Define true)) -> decr occref; if !occref = 0 then tc - else (incr locref; RHole (Ploc.make !locref 0 (0,0),Evd.QuestionMark(Evd.Define true))) + else (incr locref; RHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true))) | c -> map_rawconstr_left_to_right substrec c in substrec t @@ -580,8 +580,8 @@ let hResolve id c occ t gl = try Pretyping.Default.understand sigma env t_hole with - | Ploc.Exc (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) -> - resolve_hole (subst_hole_with_term (Ploc.line_nb loc) c_raw t_hole) + | Stdpp.Exc_located (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) -> + resolve_hole (subst_hole_with_term (fst (unloc loc)) c_raw t_hole) in let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in let t_constr_type = Retyping.get_type_of env sigma t_constr in @@ -629,3 +629,36 @@ TACTIC EXTEND constr_eq | [ "constr_eq" constr(x) constr(y) ] -> [ if eq_constr x y then tclIDTAC else tclFAIL 0 (str "Not equal") ] END + +TACTIC EXTEND is_evar +| [ "is_evar" constr(x) ] -> + [ match kind_of_term x with + | Evar _ -> tclIDTAC + | _ -> tclFAIL 0 (str "Not an evar") + ] +END + +let rec has_evar x = + match kind_of_term x with + | Evar _ -> true + | Rel _ | Var _ | Meta _ | Sort _ | Const _ | Ind _ | Construct _ -> + false + | Cast (t1, _, t2) | Prod (_, t1, t2) | Lambda (_, t1, t2) -> + has_evar t1 || has_evar t2 + | LetIn (_, t1, t2, t3) -> + has_evar t1 || has_evar t2 || has_evar t3 + | App (t1, ts) -> + has_evar t1 || has_evar_array ts + | Case (_, t1, t2, ts) -> + has_evar t1 || has_evar t2 || has_evar_array ts + | Fix ((_, tr)) | CoFix ((_, tr)) -> + has_evar_prec tr +and has_evar_array x = + array_exists has_evar x +and has_evar_prec (_, ts1, ts2) = + array_exists has_evar ts1 || array_exists has_evar ts2 + +TACTIC EXTEND has_evar +| [ "has_evar" constr(x) ] -> + [ if has_evar x then tclIDTAC else tclFAIL 0 (str "No evars") ] +END diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index d8497a7d..360be9ef 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -596,13 +596,13 @@ let make_leibniz_proof c ty r = let prf = mkApp (Lazy.force coq_f_equal, [| r.rew_car; ty; - mkLambda (Anonymous, r.rew_car, c (mkRel 1)); + mkLambda (Anonymous, r.rew_car, c); r.rew_from; r.rew_to; prf |]) in RewPrf (rel, prf) | RewCast k -> r.rew_prf in { r with rew_car = ty; - rew_from = c r.rew_from; rew_to = c r.rew_to; rew_prf = prf } + rew_from = subst1 r.rew_from c; rew_to = subst1 r.rew_to c; rew_prf = prf } open Elimschemes @@ -772,21 +772,21 @@ let subterm all flags (s : strategy) : strategy = let c' = s env sigma c cty cstr' evars in (match c' with | Some (Some r) -> - Some (Some (make_leibniz_proof (fun x -> mkCase (ci, p, x, brs)) ty r)) + Some (Some (make_leibniz_proof (mkCase (ci, lift 1 p, mkRel 1, Array.map (lift 1) brs)) ty r)) | x -> if array_for_all ((=) 0) ci.ci_cstr_nargs then let cstr = Some (mkApp (Lazy.force coq_eq, [| ty |])) in let found, brs' = Array.fold_left (fun (found, acc) br -> - if found <> None then (found, fun x -> br :: acc x) + if found <> None then (found, fun x -> lift 1 br :: acc x) else match s env sigma br ty cstr evars with - | Some (Some r) -> (Some r, fun x -> x :: acc x) - | _ -> (None, fun x -> br :: acc x)) + | Some (Some r) -> (Some r, fun x -> mkRel 1 :: acc x) + | _ -> (None, fun x -> lift 1 br :: acc x)) (None, fun x -> []) brs in match found with | Some r -> - let ctxc x = mkCase (ci, p, c, Array.of_list (List.rev (brs' x))) in + let ctxc = mkCase (ci, lift 1 p, lift 1 c, Array.of_list (List.rev (brs' x))) in Some (Some (make_leibniz_proof ctxc ty r)) | None -> x else diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 4ecc4739..569cf356 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: tactics.ml 13464 2010-09-24 22:23:02Z herbelin $ *) +(* $Id: tactics.ml 13693 2010-12-08 15:32:25Z msozeau $ *) open Pp open Util @@ -2365,8 +2365,8 @@ let abstract_args gl generalize_vars dep id defined f args = in let f', args' = decompose_indapp f args in let parvars = ids_of_constr ~all:true Idset.empty f' in + let seen = ref parvars in let dogen, f', args' = - let seen = ref parvars in let find i x = not (isVar x) || let v = destVar x in if is_defined_variable env v || Idset.mem v !seen then true @@ -2379,8 +2379,8 @@ let abstract_args gl generalize_vars dep id defined f args = true, mkApp (f', before), after in if dogen then - let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = - Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],parvars,Idset.empty,env) args' + let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = + Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],!seen,Idset.empty,env) args' in let args, refls = List.rev args, List.rev refls in let vars = diff --git a/test-suite/Makefile b/test-suite/Makefile index 62d443d0..98bab43b 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -40,7 +40,7 @@ endif command := $(coqtop) -top Top -load-vernac-source coqc := $(coqtop) -compile -coqdep := $(BIN)coqdep +coqdep := $(BIN)coqdep -coqlib $(LIB) SHOW := $(if $(VERBOSE),@true,@echo) HIDE := $(if $(VERBOSE),,@) diff --git a/test-suite/bugs/closed/shouldsucceed/2388.v b/test-suite/bugs/closed/shouldsucceed/2388.v index c7926711..8cc43ee6 100644 --- a/test-suite/bugs/closed/shouldsucceed/2388.v +++ b/test-suite/bugs/closed/shouldsucceed/2388.v @@ -2,9 +2,3 @@ Fail Parameters (A:Prop) (a:A A). -(* This is a variant (reported as part of bug #2347) *) - -Require Import EquivDec. -Fail Program Instance bool_eq_eqdec : EqDec bool eq := - {equiv_dec x y := (fix aux (x y : bool) {struct x}:= aux _ y) x y}. - diff --git a/test-suite/output/Extraction_matchs_2413.out b/test-suite/output/Extraction_matchs_2413.out new file mode 100644 index 00000000..7bce6671 --- /dev/null +++ b/test-suite/output/Extraction_matchs_2413.out @@ -0,0 +1,52 @@ +(** val test1 : bool -> bool **) + +let test1 b = + b +(** val test2 : bool -> bool **) + +let test2 b = + False +(** val wrong_id : 'a1 hole -> 'a2 hole **) + +let wrong_id = function + | Hole -> Hole + | Hole2 -> Hole2 +(** val test3 : 'a1 option -> 'a1 option **) + +let test3 o = + o +(** val test4 : indu -> indu **) + +let test4 = function + | A m -> A (S m) + | x -> x +(** val test5 : indu -> indu **) + +let test5 = function + | A m -> A (S m) + | _ -> B +(** val test6 : indu' -> indu' **) + +let test6 = function + | A' m -> A' (S m) + | E' -> B' + | F' -> B' + | _ -> C' +(** val test7 : indu -> nat option **) + +let test7 = function + | A m -> Some m + | _ -> None +(** val decode_cond_mode : + (word -> opcode option) -> (word -> 'a1 decoder_result) -> word -> ('a1 + -> opcode -> 'a2) -> 'a2 decoder_result **) + +let decode_cond_mode condition f w g = + match condition w with + | Some oc -> + (match f w with + | DecUndefined -> DecUndefined + | DecUnpredictable -> DecUnpredictable + | DecInst i -> DecInst (g i oc) + | DecError m -> DecError m) + | None -> DecUndefined diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v new file mode 100644 index 00000000..f5610efc --- /dev/null +++ b/test-suite/output/Extraction_matchs_2413.v @@ -0,0 +1,128 @@ +(** Extraction : tests of optimizations of pattern matching *) + +(** First, a few basic tests *) + +Definition test1 b := + match b with + | true => true + | false => false + end. + +Extraction test1. (** should be seen as the identity *) + +Definition test2 b := + match b with + | true => false + | false => false + end. + +Extraction test2. (** should be seen a the always-false constant function *) + +Inductive hole (A:Set) : Set := Hole | Hole2. + +Definition wrong_id (A B : Set) (x:hole A) : hole B := + match x with + | Hole => @Hole _ + | Hole2 => @Hole2 _ + end. + +Extraction wrong_id. (** should _not_ be optimized as an identity *) + +Definition test3 (A:Type)(o : option A) := + match o with + | Some x => Some x + | None => None + end. + +Extraction test3. (** Even with type parameters, should be seen as identity *) + +Inductive indu : Type := A : nat -> indu | B | C. + +Definition test4 n := + match n with + | A m => A (S m) + | B => B + | C => C + end. + +Extraction test4. (** should merge branchs B C into a x->x *) + +Definition test5 n := + match n with + | A m => A (S m) + | B => B + | C => B + end. + +Extraction test5. (** should merge branches B C into _->B *) + +Inductive indu' : Type := A' : nat -> indu' | B' | C' | D' | E' | F'. + +Definition test6 n := + match n with + | A' m => A' (S m) + | B' => C' + | C' => C' + | D' => C' + | E' => B' + | F' => B' + end. + +Extraction test6. (** should merge some branches into a _->C' *) + +(** NB : In Coq, "| a => a" corresponds to n, hence some "| _ -> n" are + extracted *) + +Definition test7 n := + match n with + | A m => Some m + | B => None + | C => None + end. + +Extraction test7. (** should merge branches B,C into a _->None *) + +(** Script from bug #2413 *) + +Set Implicit Arguments. + +Section S. + +Definition message := nat. +Definition word := nat. +Definition mode := nat. +Definition opcode := nat. + +Variable condition : word -> option opcode. + +Section decoder_result. + + Variable inst : Type. + + Inductive decoder_result : Type := + | DecUndefined : decoder_result + | DecUnpredictable : decoder_result + | DecInst : inst -> decoder_result + | DecError : message -> decoder_result. + +End decoder_result. + +Definition decode_cond_mode (mode : Type) (f : word -> decoder_result mode) + (w : word) (inst : Type) (g : mode -> opcode -> inst) : + decoder_result inst := + match condition w with + | Some oc => + match f w with + | DecInst i => DecInst (g i oc) + | DecError m => @DecError inst m + | DecUndefined => @DecUndefined inst + | DecUnpredictable => @DecUnpredictable inst + end + | None => @DecUndefined inst + end. + +End S. + +Extraction decode_cond_mode. +(** inner match should not be factorized with a partial x->x (different type) *) + diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 8f6c59fd..052d9c92 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: NMake_gen.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: NMake_gen.ml 13734 2010-12-21 18:21:56Z letouzey $ i*) (*S NMake_gen.ml : this file generates NMake.v *) @@ -1299,7 +1299,7 @@ let _ = pr " (iter _"; for i = 0 to size do pr " compare_%i" i; - pr " (fun n x y => opp_compare (comparen_%i (S n) y x))" i; + pr " (fun n x y => CompOpp (comparen_%i (S n) y x))" i; pr " (fun n => comparen_%i (S n))" i; done; pr " comparenm)."; @@ -1339,9 +1339,9 @@ let _ = pp " Let spec_opp_compare: forall c (u v: Z),"; pp " match c with Eq => u = v | Lt => u < v | Gt => u > v end ->"; - pp " match opp_compare c with Eq => v = u | Lt => v < u | Gt => v > u end."; + pp " match CompOpp c with Eq => v = u | Lt => v < u | Gt => v > u end."; pp " Proof."; - pp " intros c u v; case c; unfold opp_compare; auto with zarith."; + pp " intros c u v; case c; unfold CompOpp; auto with zarith."; pp " Qed."; pp ""; @@ -1362,7 +1362,7 @@ let _ = pp " end)"; for i = 0 to size do pp " compare_%i" i; - pp " (fun n x y => opp_compare (comparen_%i (S n) y x))" i; + pp " (fun n x y => CompOpp (comparen_%i (S n) y x))" i; pp " (fun n => comparen_%i (S n)) _ _ _" i; done; pp " comparenm _)."; diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v index a531b92e..3741c95d 100644 --- a/theories/Numbers/Natural/BigN/Nbasic.v +++ b/theories/Numbers/Natural/BigN/Nbasic.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -(*i $Id: Nbasic.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: Nbasic.v 13734 2010-12-21 18:21:56Z letouzey $ i*) Require Import ZArith. Require Import BigNumPrelude. @@ -260,13 +260,6 @@ Section ReduceRec. End ReduceRec. -Definition opp_compare cmp := - match cmp with - | Lt => Gt - | Eq => Eq - | Gt => Lt - end. - Section CompareRec. Variable wm w : Type. @@ -447,7 +440,7 @@ End AddS. | Lt => y < x | Gt => y > x end -> - match opp_compare u with + match CompOpp u with | Eq => x = y | Lt => x < y | Gt => x > y diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 53e12723..b9eb8f80 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Equality.v 13492 2010-10-04 21:20:01Z herbelin $ i*) +(*i $Id: Equality.v 13730 2010-12-19 13:32:01Z msozeau $ i*) (** Tactics related to (dependent) equality and proof irrelevance. *) @@ -320,19 +320,35 @@ Hint Unfold solution_left solution_right deletion simplification_heq constructor forms). Compare with the lemma 16 of the paper. We don't have a [noCycle] procedure yet. *) +Ltac block_equality id := + match type of id with + | @eq ?A ?t ?u => change (block (@eq A t u)) in id + | _ => idtac + end. + +Ltac revert_blocking_until id := + Tactics.on_last_hyp ltac:(fun id' => + match id' with + | id => idtac + | _ => block_equality id' ; revert id' ; revert_blocking_until id + end). + Ltac simplify_one_dep_elim_term c := match c with | @JMeq _ _ _ _ -> _ => refine (simplification_heq _ _ _ _ _) | ?t = ?t -> _ => intros _ || refine (simplification_K _ t _ _) - | eq (existT _ _ _) (existT _ _ _) -> _ => + | eq (existT _ ?p _) (existT _ ?q _) -> _ => refine (simplification_existT2 _ _ _ _ _ _ _) || - refine (simplification_existT1 _ _ _ _ _ _ _ _) + match goal with + | H : p = q |- _ => intro + | _ => refine (simplification_existT1 _ _ _ _ _ _ _ _) + end | ?x = ?y -> _ => (* variables case *) (let hyp := fresh in intros hyp ; - move hyp before x ; revert_until hyp ; generalize dependent x ; + move hyp before x ; revert_blocking_until hyp ; generalize dependent x ; refine (solution_left _ _ _ _)(* ; intros until 0 *)) || (let hyp := fresh in intros hyp ; - move hyp before y ; revert_until hyp ; generalize dependent y ; + move hyp before y ; revert_blocking_until hyp ; generalize dependent y ; refine (solution_right _ _ _ _)(* ; intros until 0 *)) | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; injection H ; clear H) | ?t = ?u -> _ => let hyp := fresh in diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index 333dd7a6..4a41d9c9 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Tactics.v 13332 2010-07-26 22:12:43Z msozeau $ i*) +(*i $Id: Tactics.v 13693 2010-12-08 15:32:25Z msozeau $ i*) (** This module implements various tactics used to simplify the goals produced by Program, which are also generally useful. *) @@ -308,11 +308,14 @@ Ltac program_simplify := subst*; autoinjections ; try discriminates ; try (solve [ red ; intros ; destruct_conjs ; autoinjections ; discriminates ]). -Ltac program_solve_wf := +(** We only try to solve proposition goals automatically. *) + +Ltac program_solve := match goal with - |- well_founded _ => auto with * + | |- well_founded _ => auto with * + | |- ?T => match type of T with Prop => auto end end. -Ltac program_simpl := program_simplify ; auto; try program_solve_wf. +Ltac program_simpl := program_simplify ; try program_solve. Obligation Tactic := program_simpl. diff --git a/theories/Sorting/Mergesort.v b/theories/Sorting/Mergesort.v index e576db2b..04de1bfc 100644 --- a/theories/Sorting/Mergesort.v +++ b/theories/Sorting/Mergesort.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Mergesort.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: Mergesort.v 13678 2010-12-04 10:34:28Z herbelin $ i*) (** A modular implementation of mergesort (the complexity is O(n.log n) in the length of the list) *) @@ -61,6 +61,7 @@ Fixpoint merge l1 l2 := For instance, here is how [6;2;3;1;5] is sorted: +<< operation stack list iter_merge [] [6;2;3;1;5] = append_list_to_stack [ + [6]] [2;3;1;5] @@ -77,7 +78,7 @@ Fixpoint merge l1 l2 := = append_list_to_stack [[1;2;3;6];; + [5]] [] -> merge_stack [[1;2;3;6];;[5]] = [1;2;3;5;6] - +>> The complexity of the algorithm is n*log n, since there are 2^(p-1) mergings to do of length 2, 2^(p-2) of length 4, ..., 2^0 of length 2^p for a list of length 2^p. The algorithm does not need diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 2a615311..357d0b7e 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: BinInt.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: BinInt.v 13697 2010-12-09 18:48:04Z herbelin $ i*) (***********************************************************) (** Binary Integers (Pierre Crégut, CNET, Lannion, France) *) @@ -223,7 +223,6 @@ Qed. (**********************************************************************) - (** ** Properties of opposite on binary integer numbers *) Theorem Zopp_0 : Zopp Z0 = Z0. @@ -270,21 +269,21 @@ Qed. (**********************************************************************) (** * Properties of the addition on integers *) -(** ** zero is left neutral for addition *) +(** ** Zero is left neutral for addition *) Theorem Zplus_0_l : forall n:Z, Z0 + n = n. Proof. intro x; destruct x; reflexivity. Qed. -(** *** zero is right neutral for addition *) +(** ** Zero is right neutral for addition *) Theorem Zplus_0_r : forall n:Z, n + Z0 = n. Proof. intro x; destruct x; reflexivity. Qed. -(** ** addition is commutative *) +(** ** Addition is commutative *) Theorem Zplus_comm : forall n m:Z, n + m = m + n. Proof. @@ -296,7 +295,7 @@ Proof. rewrite Pplus_comm; reflexivity. Qed. -(** ** opposite distributes over addition *) +(** ** Opposite distributes over addition *) Theorem Zopp_plus_distr : forall n m:Z, - (n + m) = - n + - m. Proof. @@ -310,7 +309,7 @@ Proof. intro; unfold Zsucc; now rewrite Zopp_plus_distr. Qed. -(** ** opposite is inverse for addition *) +(** ** Opposite is inverse for addition *) Theorem Zplus_opp_r : forall n:Z, n + - n = Z0. Proof. @@ -327,7 +326,7 @@ Qed. Hint Local Resolve Zplus_0_l Zplus_0_r. -(** ** addition is associative *) +(** ** Addition is associative *) Lemma weak_assoc : forall (p q:positive) (n:Z), Zpos p + (Zpos q + n) = Zpos p + Zpos q + n. @@ -495,7 +494,7 @@ Proof. rewrite (Zplus_comm p n); trivial with arith. Qed. -(** ** addition simplifies *) +(** ** Addition simplifies *) Theorem Zplus_reg_l : forall n m p:Z, n + m = n + p -> m = p. intros n m p H; cut (- n + (n + m) = - n + (n + p)); @@ -504,7 +503,7 @@ Theorem Zplus_reg_l : forall n m p:Z, n + m = n + p -> m = p. | rewrite H; trivial with arith ]. Qed. -(** ** addition and successor permutes *) +(** ** Addition and successor permutes *) Lemma Zplus_succ_l : forall n m:Z, Zsucc n + m = Zsucc (n + m). Proof. @@ -575,7 +574,7 @@ Proof. trivial with arith. Qed. -(** successor and predecessor are inverse functions *) +(** ** Successor and predecessor are inverse functions *) Theorem Zsucc_pred : forall n:Z, n = Zsucc (Zpred n). Proof. @@ -600,7 +599,7 @@ Proof. Qed. (*************************************************************************) -(** ** Properties of the direct definition of successor and predecessor *) +(** ** Properties of the direct definition of successor and predecessor *) Theorem Zsucc_succ' : forall n:Z, Zsucc n = Zsucc' n. Proof. diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty index 4314d07d..9de9a38f 100644 --- a/tools/coqdoc/coqdoc.sty +++ b/tools/coqdoc/coqdoc.sty @@ -83,7 +83,7 @@ \newcommand{\coqdocnotation}[1]{\coqdockw{#1}} \newcommand{\coqdocsection}[1]{\coqdoccst{#1}} \newcommand{\coqdocaxiom}[1]{\coqdocax{#1}} -\newcommand{\coqdocmoduleid}[1]{\coqdocmod{#1}} +\newcommand{\coqdocmodule}[1]{\coqdocmod{#1}} % Environment encompassing code fragments % !!! CAUTION: This environment may have empty contents @@ -107,9 +107,6 @@ % Empty lines (in code only) \newcommand{\coqdocemptyline}{\vskip 0.4em plus 0.1em minus 0.1em} -% macro for typesetting the title of a module implementation -\newcommand{\coqdocmodule}[1]{\chapter{Module #1}\markboth{Module #1}{} -} \usepackage{ifpdf} \ifpdf \RequirePackage{hyperref} diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index a23a4f74..177058b3 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: cpretty.mll 13440 2010-09-19 20:21:12Z herbelin $ i*) +(*i $Id: cpretty.mll 13692 2010-12-06 23:55:10Z herbelin $ i*) (*s Utility functions for the scanners *) @@ -272,7 +272,9 @@ let firstchar = (* superscript 1 *) '\194' '\185' | (* utf-8 latin 1 supplement *) - '\195' ['\128'-'\191'] | + '\195' ['\128'-'\150'] | + '\195' ['\152'-'\182'] | + '\195' ['\184'-'\191'] | (* utf-8 letterlike symbols *) (* '\206' ([ '\145' - '\183'] | '\187') | *) (* '\xCF' [ '\x00' - '\xCE' ] | *) @@ -315,7 +317,6 @@ let def_token = | "Class" | "SubClass" | "Example" - | "Local" | "Fixpoint" | "Boxed" | "CoFixpoint" @@ -450,6 +451,12 @@ rule coq_bol = parse { begin_show (); coq_bol lexbuf } | space* end_show { end_show (); coq_bol lexbuf } + | space* ("Local"|"Global") + { + in_proof := None; + let s = lexeme lexbuf in + output_indented_keyword s lexbuf; + coq_bol lexbuf } | space* gallina_kw_to_hide { let s = lexeme lexbuf in if !Cdglobals.light && section_or_end s then diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index e8f30853..a28e1197 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: index.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: index.ml 13676 2010-12-04 10:34:21Z herbelin $ i*) open Filename open Lexing @@ -216,7 +216,7 @@ let type_name = function | Library -> let ln = !lib_name in if ln <> "" then String.lowercase ln else "library" - | Module -> "moduleid" + | Module -> "module" | Definition -> "definition" | Inductive -> "inductive" | Constructor -> "constructor" @@ -235,23 +235,45 @@ let type_name = function let prepare_entry s = function | Notation -> - (* Notations have conventially the form section.:sc:x_++_'x'_x *) + (* We decode the encoding done in Dumpglob.cook_notation of coqtop *) + (* Encoded notations have the form section:sc:x_'++'_x where: *) + (* - the section, if any, ends with a "." *) + (* - the scope can be empty *) + (* - tokens are separated with "_" *) + (* - non-terminal symbols are conventionally represented by "x" *) + (* - terminals are enclosed within simple quotes *) + (* - existing simple quotes (that necessarily are parts of terminals) *) + (* are doubled *) + (* (as a consequence, when a terminal contains "_" or "x", these *) + (* necessarily appear enclosed within non-doubled simple quotes) *) + (* Example: "x ' %x _% y %'x %'_' z" is encoded as *) + (* "x_''''_'%x'_'_%'_x_'%''x'_'%''_'''_x" *) let err () = eprintf "Invalid notation in globalization file\n"; exit 1 in let h = try String.index_from s 0 ':' with _ -> err () in let i = try String.index_from s (h+1) ':' with _ -> err () in let sc = String.sub s (h+1) (i-h-1) in - let ntn = String.make (String.length s) ' ' in + let ntn = String.make (String.length s - i) ' ' in let k = ref 0 in let j = ref (i+1) in let quoted = ref false in - while !j <> String.length s do - if s.[!j] = '_' && not !quoted then ntn.[!k] <- ' ' else - if s.[!j] = 'x' && not !quoted then ntn.[!k] <- '_' else - if s.[!j] = '\'' then - if s.[!j+1] = 'x' && s.[!j+1] = '\'' then (ntn.[!k] <- 'x'; j:=!j+2) - else (quoted := not !quoted; ntn.[!k] <- '\'') - else ntn.[!k] <- s.[!j]; - incr j; incr k + let l = String.length s - 1 in + while !j <= l do + if not !quoted then begin + (match s.[!j] with + | '_' -> ntn.[!k] <- ' '; incr k + | 'x' -> ntn.[!k] <- '_'; incr k + | '\'' -> quoted := true + | _ -> assert false) + end + else + if s.[!j] = '\'' then begin + if (!j = l || s.[!j+1] <> '\'') then quoted := false + else (ntn.[!k] <- s.[!j]; incr k; incr j) + end else begin + ntn.[!k] <- s.[!j]; + incr k + end; + incr j done; let ntn = String.sub ntn 0 !k in if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")" diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index cbebbd79..4f9dd169 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: output.ml 13541 2010-10-13 19:53:29Z notin $ i*) +(*i $Id: output.ml 13676 2010-12-04 10:34:21Z herbelin $ i*) open Cdglobals open Index @@ -287,7 +287,7 @@ module Latex = struct printf "\\coqdocindent{%2.2fem}\n" space let module_ref m s = - printf "\\moduleid{%s}{%s}" m (escaped s) + printf "\\coqdocmodule{%s}{%s}" m (escaped s) let ident_ref m fid typ s = let id = if fid <> "" then (m ^ "." ^ fid) else m in diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index db2f9ae9..3bba0605 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cerrors.ml 13431 2010-09-18 08:15:29Z herbelin $ *) +(* $Id: cerrors.ml 13639 2010-11-16 15:36:01Z glondu $ *) open Pp open Util @@ -81,6 +81,10 @@ let rec explain_exn_default_aux anomaly_string report_fn = function hov 0 (str "Syntax error: Undefined token.") | Lexer.Error (Bad_token s) -> hov 0 (str "Syntax error: Bad token" ++ spc () ++ str s ++ str ".") + | Stdpp.Exc_located (loc,exc) -> + hov 0 ((if loc = dummy_loc then (mt ()) + else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) + ++ explain_exn_default_aux anomaly_string report_fn exc) | Assert_failure (s,b,e) -> hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++ (if s <> "" then @@ -167,10 +171,13 @@ let explain_exn_default = let raise_if_debug e = if !Flags.debug then raise e -let _ = Tactic_debug.explain_logic_error := explain_exn_default +let _ = Tactic_debug.explain_logic_error := + (fun e -> explain_exn_default (process_vernac_interp_error e)) let _ = Tactic_debug.explain_logic_error_no_anomaly := - explain_exn_default_aux (fun () -> mt()) (fun () -> str ".") + (fun e -> + explain_exn_default_aux (fun () -> mt()) (fun () -> str ".") + (process_vernac_interp_error e)) let explain_exn_function = ref explain_exn_default diff --git a/toplevel/command.ml b/toplevel/command.ml index 9b18ef27..2d0cdea6 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: command.ml 13344 2010-07-28 15:04:36Z msozeau $ *) +(* $Id: command.ml 13672 2010-12-03 20:05:46Z herbelin $ *) open Pp open Util @@ -241,7 +241,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite = let env_ar_params = push_rel_context ctx_params env_ar in (* Compute interpretation metadatas *) - let indimpls = List.map (fun (_, impls) -> userimpls @ lift_implicits (List.length userimpls) impls) arities in + let indimpls = List.map (fun (_, impls) -> userimpls @ lift_implicits (rel_context_nhyps ctx_params) impls) arities in let arities = List.map fst arities in let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in @@ -275,7 +275,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite = mind_entry_lc = ctypes }) indl arities constructors in let impls = - let len = List.length ctx_params in + let len = rel_context_nhyps ctx_params in List.map2 (fun indimpls (_,_,cimpls) -> indimpls, List.map (fun impls -> userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 6ee00f48..c1663685 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: metasyntax.ml 13329 2010-07-26 11:05:39Z herbelin $ *) +(* $Id: metasyntax.ml 13690 2010-12-06 16:15:54Z glondu $ *) open Pp open Flags @@ -106,33 +106,33 @@ let add_tactic_notation (n,prods,e) = let print_grammar = function | "constr" | "operconstr" | "binder_constr" -> msgnl (str "Entry constr is"); - Gram.Entry.print Pcoq.Constr.constr; + entry_print Pcoq.Constr.constr; msgnl (str "and lconstr is"); - Gram.Entry.print Pcoq.Constr.lconstr; + entry_print Pcoq.Constr.lconstr; msgnl (str "where binder_constr is"); - Gram.Entry.print Pcoq.Constr.binder_constr; + entry_print Pcoq.Constr.binder_constr; msgnl (str "and operconstr is"); - Gram.Entry.print Pcoq.Constr.operconstr; + entry_print Pcoq.Constr.operconstr; | "pattern" -> - Gram.Entry.print Pcoq.Constr.pattern + entry_print Pcoq.Constr.pattern | "tactic" -> msgnl (str "Entry tactic_expr is"); - Gram.Entry.print Pcoq.Tactic.tactic_expr; + entry_print Pcoq.Tactic.tactic_expr; msgnl (str "Entry binder_tactic is"); - Gram.Entry.print Pcoq.Tactic.binder_tactic; + entry_print Pcoq.Tactic.binder_tactic; msgnl (str "Entry simple_tactic is"); - Gram.Entry.print Pcoq.Tactic.simple_tactic; + entry_print Pcoq.Tactic.simple_tactic; | "vernac" -> msgnl (str "Entry vernac is"); - Gram.Entry.print Pcoq.Vernac_.vernac; + entry_print Pcoq.Vernac_.vernac; msgnl (str "Entry command is"); - Gram.Entry.print Pcoq.Vernac_.command; + entry_print Pcoq.Vernac_.command; msgnl (str "Entry syntax is"); - Gram.Entry.print Pcoq.Vernac_.syntax; + entry_print Pcoq.Vernac_.syntax; msgnl (str "Entry gallina is"); - Gram.Entry.print Pcoq.Vernac_.gallina; + entry_print Pcoq.Vernac_.gallina; msgnl (str "Entry gallina_ext is"); - Gram.Entry.print Pcoq.Vernac_.gallina_ext; + entry_print Pcoq.Vernac_.gallina_ext; | _ -> error "Unknown or unprintable grammar entry." (**********************************************************************) diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index 9594c988..299214f0 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: toplevel.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: toplevel.ml 13668 2010-12-02 17:43:59Z herbelin $ *) open Pp open Util @@ -276,7 +276,6 @@ let rec is_pervasive_exn = function | Error_in_file (_,_,e) -> is_pervasive_exn e | Stdpp.Exc_located (_,e) -> is_pervasive_exn e | DuringCommandInterp (_,e) -> is_pervasive_exn e - | DuringSyntaxChecking (_,e) -> is_pervasive_exn e | _ -> false (* Toplevel error explanation, dealing with locations, Drop, Ctrl-D @@ -285,8 +284,7 @@ let rec is_pervasive_exn = function let print_toplevel_error exc = let (dloc,exc) = match exc with - | DuringCommandInterp (loc,ie) - | DuringSyntaxChecking (loc,ie) -> + | DuringCommandInterp (loc,ie) -> if loc = dummy_loc then (None,ie) else (Some loc, ie) | _ -> (None, exc) in @@ -335,8 +333,7 @@ let rec discard_to_dot () = * in encountered. *) let process_error = function - | DuringCommandInterp _ - | DuringSyntaxChecking _ as e -> e + | DuringCommandInterp _ as e -> e | e -> if is_pervasive_exn e then e diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index a00efc5c..9464d763 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vernac.ml 13488 2010-10-03 22:27:05Z herbelin $ *) +(* $Id: vernac.ml 13668 2010-12-02 17:43:59Z herbelin $ *) (* Parsing of vernacular. *) @@ -34,8 +34,7 @@ exception HasNotFailed let raise_with_file file exc = let (cmdloc,re) = match exc with - | DuringCommandInterp(loc,e) - | DuringSyntaxChecking(loc,e) -> (loc,e) + | DuringCommandInterp(loc,e) -> (loc,e) | e -> (dummy_loc,e) in let (inner,inex) = @@ -171,7 +170,7 @@ let rec vernac_com interpfun (loc,com) = | e -> (* if [e] is an anomaly, the next function will re-raise it *) let msg = Cerrors.explain_exn_no_anomaly e in - msgnl (str "The command has indeed failed with message:" ++ + if_verbose msgnl (str "The command has indeed failed with message:" ++ fnl () ++ str "=> " ++ hov 0 msg) end diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index b5af665c..0d247189 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacexpr.ml 13492 2010-10-04 21:20:01Z herbelin $ i*) +(*i $Id: vernacexpr.ml 13668 2010-12-02 17:43:59Z herbelin $ i*) open Util open Names @@ -360,10 +360,7 @@ and located_vernac_expr = loc * vernac_expr (* Locating errors raised just after the dot is parsed but before the interpretation phase *) -exception DuringSyntaxChecking of exn located - -let syntax_checking_error loc s = - raise (DuringSyntaxChecking (loc,UserError ("",Pp.str s))) +let syntax_checking_error loc s = user_err_loc (loc,"",Pp.str s) (**********************************************************************) (* Managing locality *) |