Commit 6b691bbd2101fd39395c0d2135fd7c06a8915e14 - coq

Imported Upstream version 8.3pl1 Stephane Glondu 13 years ago

68 changed file(s) with 2482 addition(s) and 480 deletion(s). Raw diff Collapse all Expand all

-0

.gitignore less more

101	101	plugins//_mod.ml
102	102	myocamlbuild_config.ml
103	103	.DS_Store
	104	.pc

+51

-0

CHANGES less more

	0	Changes from V8.3 to V8.3pl1
	1	============================
	2
	3	Type inference, notations and implicit arguments bug fixes
	4
	5	- #2448 (alpha-renaming problems with notations internally using binders)
	6	- #2454 (pattern-matching sometimes not supporting type casts)
	7	- fixing combined use of non-implicit and explictly-declared implicit arguments
	8	in inductive arities
	9	- restored support for using some ident with different scopes in notations
	10
	11	Ltac and tactics bug fixes
	12
	13	- #2414 (rewrite in not looking for eq_ind in the right module)
	14	- #2433 (new "is_evar"/"has_evar" to restore support for matching evars in Ltac)
	15	- #2453 (dependent destruction)
	16	- loop in dependent destruction
	17	- new "constr_eq" tactic for restoring support for term equality test in Ltac
	18	- setoid rewrite under cases and abstraction fixed
	19
	20	Coqdoc and documentation bugs
	21
	22	- #2418 (wrong URLs in documentation)
	23	- #2441 (coqdoc bug in Mergesort.v)
	24	- #2445 (correct support for "'" character in coqdoc links to notations)
	25	- fixed wrong use of "moduleid" instead of "module" in coqdoc html indexes
	26	- fixing parsing of Multiplication and Division signs (unicode 0xD7 and 0xF7)
	27
	28	Compilation
	29
	30	- #2432 (support for compilation with camlp5 6.02.0)
	31	- support for compilation with ocaml >= 3.09.3 restored
	32
	33	Extraction
	34
	35	- #2413 (prevent type-unsafe optimisations of pattern matching)
	36	- Identifiers of a development aimed to be extracted should
	37	avoid containing "__", since the extraction make various use of
	38	this sub-string, leading to potential name clashes. This was
	39	already so in V8.3, but not announced, as mentionned by #2421.
	40
	41	Miscellaneous bug fixes
	42
	43	- #2412 (anomaly Ploc.Exc when using Ltac Debug)
	44	- #2419 (redundant opp_compare removed)
	45	- #2427 (Module Functor claims Signature does not match)
	46	- #2431 (compliance of CoqIDE use of mutexes with FreeBSD)
	47	- #2434 (anomaly DuringSyntaxChecking with Local/Global prefixes)
	48	- a few improvements in efficiency
	49
	50
0	51	Changes from V8.2 to V8.3
1	52	=========================
2	53

-2

INSTALL less more

40	40
41	41	Should you need or prefer to compile Coq V8.3 yourself, you need:
42	42
43		- Objective Caml version 3.10.2 or later
	43	- Objective Caml version 3.09.3 or later
44	44	(available at http://caml.inria.fr/)
45	45
46	46	For Objective Caml version >= 3.10.0, you also need to install

87	87	INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
88	88	=================================================
89	89
90		1- Check that you have the Objective Caml compiler version 3.10.2 (or later)
	90	1- Check that you have the Objective Caml compiler version 3.09.3 (or later)
91	91	installed on your computer and that "ocamlmktop" and "ocamlc" (or
92	92	its native code version "ocamlc.opt") lie in a directory which is present
93	93	in your $PATH environment variable.

-1

INSTALL.ide less more

22	22	Else, read the rest of this document to compile your own CoqIde.
23	23
24	24	REQUIREMENT:
25		- OCaml >= 3.10.2 with native threads support.
	25	- OCaml >= 3.09.3 with native threads support.
26	26	- make world must succeed.
27	27	- The graphical toolkit GTK+ 2.x. See http://www.gtk.org.
28	28	The official supported version is at least 2.10.x.

+11

-1

Makefile less more

5	5	# # GNU Lesser General Public License Version 2.1 #
6	6	#######################################################################
7	7
8		# $Id: Makefile 13540 2010-10-13 19:53:28Z notin $
	8	# $Id: Makefile 13566 2010-10-19 13:22:08Z glondu $
9	9
10	10
11	11	# Makefile for Coq

159	159	stage1 $(STAGE1_TARGETS) : always
160	160	$(call stage-template,1)
161	161
	162	ifneq (,$(STAGE1_IMPLICITS))
	163	$(STAGE1_IMPLICITS) : always
	164	$(call stage-template,1)
	165	endif
	166
162	167	stage2 $(STAGE2_TARGETS) : stage1
163	168	$(call stage-template,2)
	169
	170	ifneq (,$(STAGE2_IMPLICITS))
	171	$(STAGE2_IMPLICITS) : stage1
	172	$(call stage-template,2)
	173	endif
164	174
165	175	# Nota:
166	176	# - world is one of the targets in $(STAGE2_TARGETS), hence launching

-6

Makefile.common less more

364	364
365	365	SOURCEDOCDIR=dev/source-doc
366	366
367		CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot
	367	CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.o %.cmi %.cma %.cmxa %.a %.cmxs %.dep.ps %.dot
368	368
369	369	### Targets forwarded by Makefile to a specific stage:
370	370

373	373	STAGE1_TARGETS:= $(STAGE1) $(COQDEPBOOT) \
374	374	$(GENFILES) \
375	375	source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \
376		$(STAGE1_ML4:.ml4=.ml4-preprocessed) %.o
	376	$(STAGE1_ML4:.ml4=.ml4-preprocessed)
	377
	378	STAGE1_IMPLICITS:=
377	379
378	380	ifdef CM_STAGE1
379		STAGE1_TARGETS+=$(CAML_OBJECT_PATTERNS)
	381	STAGE1_IMPLICITS+=$(CAML_OBJECT_PATTERNS)
380	382	endif
381	383
382	384	## Enumeration of targets that require being done at stage2

401	403	printers debug initplugins plugins \
402	404	world install coqide coqide-files coq coqlib \
403	405	coqlight states check init theories theories-light \
404		$(DOC_TARGETS) $(VO_TARGETS) validate \
405		%.vo %.glob states/% install-% %.ml4-preprocessed \
	406	$(DOC_TARGETS) $(VO_TARGETS) validate
	407
	408	STAGE2_IMPLICITS:= %.vo %.glob states/% install-% %.ml4-preprocessed \
406	409	$(DOC_TARGET_PATTERNS)
407	410
408	411	ifndef CM_STAGE1
409		STAGE2_TARGETS+=$(CAML_OBJECT_PATTERNS)
	412	STAGE2_IMPLICITS+=$(CAML_OBJECT_PATTERNS)
410	413	endif
411	414
412	415

-3

Makefile.doc less more

184	184
185	185	### Standard library (browsable html format)
186	186
187		ifeq ($(QUICK),1)
	187	ifdef QUICK
188	188	doc/stdlib/html/genindex.html:
189	189	else
190		doc/stdlib/html/genindex.html: \| $(COQDOC) $(THEORIESVO)
	190	doc/stdlib/html/genindex.html: \| $(COQDOC) $(THEORIESVO) $(PLUGINSVO)
191	191	endif
192	192	- rm -rf doc/stdlib/html
193	193	$(MKDIR) doc/stdlib/html
194	194	$(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 \
195		-R theories Coq $(THEORIESVO:.vo=.v)
	195	-R theories Coq -R plugins Coq $(THEORIESVO:.vo=.v) $(PLUGINSVO:.vo=.v)
196	196	mv doc/stdlib/html/index.html doc/stdlib/html/genindex.html
197	197
198	198	doc/stdlib/index-list.html: doc/stdlib/index-list.html.template doc/stdlib/make-library-index

-1

README.win less more

19	19	distribution. If you really need to recompile under Windows, here
20	20	are some indications:
21	21
22		1- Install ocaml for Windows (MinGW port), at least version 3.10.2.
	22	1- Install ocaml for Windows (MinGW port), at least version 3.09.3.
23	23	See: http://caml.inria.fr
24	24
25	25	2- Install a shell environment with at least:

-4

configure less more

5	5	#
6	6	##################################
7	7
8		VERSION=8.3
	8	VERSION=8.3pl1
9	9	VOMAGIC=08300
10	10	STATEMAGIC=58300
11	11	DATE=`LANG=C date +"%B %Y"`

410	410	CAMLVERSION=`"$bytecamlc" -version`
411	411
412	412	case $CAMLVERSION in
413		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*)
	413	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])
414	414	echo "Your version of Objective-Caml is $CAMLVERSION."
415	415	if [ "$force_caml_version" = "yes" ]; then
416	416	echo "Warning You are compiling Coq with an outdated version of Objective-Caml."
417	417	else
418		echo " You need Objective-Caml 3.10.2 or later."
	418	echo " You need Objective-Caml 3.09.3 or later."
419	419	echo " Configuration script failed!"
420	420	exit 1
421	421	fi;;

1093	1093	echo "Warning To compile the system for a new architecture"
1094	1094	echo " don't forget to do a 'make archclean' before './configure'."
1095	1095
1096		# $Id: configure 13552 2010-10-14 14:02:46Z notin $
	1096	# $Id: configure 13740 2010-12-23 12:37:18Z notin $

+11

-0

doc/faq/FAQ.tex less more

96	96	\def\symmetryin{{\tt symmetryin}}
97	97	\def\instantiate{{\tt instantiate}}
98	98	\def\inversion{{\tt inversion}}
	99	\def\specialize{{\tt specialize}}
99	100	\def\Defined{{\tt Defined}}
100	101	\def\Qed{{\tt Qed}}
101	102	\def\pattern{{\tt pattern}}

865	866	variables you can use the {\intros} tactic. A good habit is to
866	867	provide names for these variables: {\Coq} will do it anyway, but such
867	868	automatic naming decreases legibility and robustness.
	869
	870
	871	\Question{My goal contains an universally quantified statement, how can I use it?}
	872
	873	If the universally quantified assumption matches the goal you can
	874	use the {\apply} tactic. If it is an equation you can use the
	875	{\rewrite} tactic. Otherwise you can use the {\specialize} tactic
	876	to instantiate the quantified variables with terms. The variant
	877	{\tt assert(Ht := H t)} makes a copy of assumption {\tt H} before
	878	instantiating it.
868	879
869	880
870	881	\Question{My goal is an existential, how can I prove it?}

+18

-7

doc/refman/Classes.tex less more

9	9	\label{typeclasses}
10	10
11	11	\begin{flushleft}
12		\em The status of Type Classes is (extremely) experimental.
	12	\em The status of Type Classes is experimental.
13	13	\end{flushleft}
14	14
15	15	This chapter presents a quick reference of the commands related to type

127	127	methods. In the example above, \texttt{A} and \texttt{eqa} should be
128	128	set maximally implicit.
129	129	\item They support implicit quantification on partialy applied type
130		classes (\S \ref{implicit-generalization}).
131		Any argument not given as part of a type class binder will be
132		automatically generalized.
	130	classes.
133	131	\item They also support implicit quantification on superclasses
134	132	(\S \ref{classes:superclasses})
135	133	\end{itemize}

141	139
142	140	Here \texttt{A} is implicitly generalized, and the resulting function
143	141	is equivalent to the one above.
	142
	143	The parsing of generalized type-class binders is different from regular
	144	binders:
	145	\begin{itemize}
	146	\item Implicit arguments of the class type are ignored.
	147	\item Superclasses arguments are automatically generalized.
	148	\item Any remaining arguments not given as part of a type class binder
	149	will be automatically generalized. In other words, the rightmost
	150	parameters are automatically generalized if not mentionned.
	151	\end{itemize}
	152
	153	One can switch off this special treatment using the $!$ mark in front of
	154	the class name (see example below).
144	155
145	156	\asection{Parameterized Instances}
146	157

230	241	\end{coq_example*}
231	242
232	243	In some cases, to be able to specify sharing of structures, one may want to give
233		explicitly the superclasses. It is is possible to do it directly in regular
234		binders, and using the \texttt{!} modifier in class binders. For
235		example:
	244	explicitly the superclasses. It is possible to do it directly in regular
	245	generalized binders, and using the \texttt{!} modifier in class
	246	binders. For example:
236	247	\begin{coq_example*}
237	248	Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) :=
238	249	andb (le x y) (neqb x y).

-2

doc/refman/RefMan-ext.tex less more

1621	1621	delimiters, free variables in the current context are automatically
1622	1622	quantified using a product or a lambda abstraction to generate a closed
1623	1623	term. In the following statement for example, the variables \texttt{n}
1624		and \texttt{m} are autamatically generalized and become explicit
	1624	and \texttt{m} are automatically generalized and become explicit
1625	1625	arguments of the lemma as we are using \verb\|`( )\|:
1626	1626
1627	1627	\begin{coq_example}

1637	1637	the command:
1638	1638
1639	1639	\begin{quote}
1640		{\tt Generalizable (All\|No) Variable(s)? ({\ident$_1$ \ident$_n$})?.}
	1640	{\tt (Global)? Generalizable (All\|No) Variable(s)? ({\ident$_1$ \ident$_n$})?.}
1641	1641	\end{quote}
1642	1642
1643	1643	\begin{Variants}

+21

-15

doc/refman/RefMan-ide.tex less more

260	260	symbol required, for example \verb\|2200\| for the $\forall$ symbol.
261	261	A list of symbol codes is available at \url{http://www.unicode.org}.
262	262
263		This method obviously doesn't scale, that's why the preferred alternative is to
264		use an Input Method Editor. On POSIX systems (Linux distros, BSD variants and
265		MacOS X), you can use \texttt{uim} version 1.6 or later which provides a \LaTeX{}-style
266		input method.
267
268		To configure \texttt{uim}, execute \texttt{uim-pref-gtk} as your regular user.
269		In the "Global Settings" group set the default Input Method to "ELatin" (don't
270		forget to tick the checkbox "Specify default IM"). In the "ELatin" group set the
271		layout to "TeX", and remember the content of the "[ELatin] on" field (by default
272		"<Control>\"). You can now execute CoqIDE with the following commands (assuming
273		you use a Bourne-style shell):
	263	This method obviously doesn't scale, that's why the preferred
	264	alternative is to use an Input Method Editor. On POSIX systems (Linux
	265	distributions, BSD variants and MacOS X), you can use \texttt{uim} to
	266	support \LaTeX{}-style edition and, if using X Windows, you can also use
	267	the XCompose method (XIM). How to use \texttt{uim} is documented below.
	268
	269	If you have \texttt{uim} 1.5.x, first manually copy the files located
	270	in directory {\tt ide/uim} of the Coq source distribution to the
	271	{\tt uim} directory of input methods which typically is {\tt
	272	/usr/share/uim}. Execute {\tt uim-module-manager -{-}register
	273	coqide}. Then, execute \texttt{uim-pref-gtk} as regular user and set
	274	the default Input Method to "CoqIDE" in the "Global Settings" group
	275	(don't forget to tick the checkbox "Specify default IM"; you may also
	276	have to first edit the set of "Enabled input method" to add CoqIDE to
	277	the set). You can now execute CoqIDE with the following commands
	278	(assuming you use a Bourne-style shell):
274	279
275	280	\begin{verbatim}
276	281	$ export GTK_IM_MODULE=uim
277	282	$ coqide
278	283	\end{verbatim}
279	284
280		Activate the ELatin Input Method with Ctrl-\textbackslash, then type the
281		sequence "\verb=\Gamma=". You will see the sequence being
282		replaced by $\Gamma$ as soon as you type the second "a".
	285	If you then type the sequence "\verb=\Gamma=", you will see the sequence being
	286	replaced by $\Gamma$ as soon as you type the second "a".
	287
	288	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.
283	289
284	290	\subsection[Character encoding for saved files]{Character encoding for saved files\label{sec:coqidecharencoding}}
285	291

313	319
314	320
315	321
316		% $Id: RefMan-ide.tex 13477 2010-09-30 16:50:00Z vgross $
	322	% $Id: RefMan-ide.tex 13701 2010-12-10 07:48:30Z herbelin $
317	323
318	324	%%% Local Variables:
319	325	%%% mode: latex

+32

-2

doc/refman/RefMan-tac.tex less more

987	987	Assumptions} (see Section~\ref{PrintAssumptions}). Admitted subgoals
988	988	have names of the form {\ident}\texttt{\_admitted} possibly followed
989	989	by a number.
	990
	991	\subsection{\tt constr\_eq \term$_1$ \term$_2$
	992	\tacindex{constr\_eq}
	993	\label{constreq}}
	994
	995	This tactic applies to any goal. It checks whether its arguments are
	996	equal modulo alpha conversion and casts.
	997
	998	\ErrMsg \errindex{Not equal}
	999
	1000	\subsection{\tt is\_evar \term
	1001	\tacindex{is\_evar}
	1002	\label{isevar}}
	1003
	1004	This tactic applies to any goal. It checks whether its argument is an
	1005	existential variable. Existential variables are uninstantiated
	1006	variables generated by e.g. {\tt eapply} (see Section~\ref{apply}).
	1007
	1008	\ErrMsg \errindex{Not an evar}
	1009
	1010	\subsection{\tt has\_evar \term
	1011	\tacindex{has\_evar}
	1012	\label{hasevar}}
	1013
	1014	This tactic applies to any goal. It checks whether its argument has an
	1015	existential variable as a subterm. Unlike {\tt context} patterns
	1016	combined with {\tt is\_evar}, this tactic scans all subterms,
	1017	including those under binders.
	1018
	1019	\ErrMsg \errindex{No evars}
990	1020
991	1021	\subsection{Bindings list
992	1022	\index{Binding list}

3916	3946
3917	3947	\begin{quotation}
3918	3948	\begin{verbatim}
3919		Hint Extern 4 ~(?=?) => discriminate.
	3949	Hint Extern 4 (~(_ = _)) => discriminate.
3920	3950	\end{verbatim}
3921	3951	\end{quotation}
3922	3952

4293	4323	user-defined tactics.
4294	4324
4295	4325
4296		% $Id: RefMan-tac.tex 13344 2010-07-28 15:04:36Z msozeau $
	4326	% $Id: RefMan-tac.tex 13659 2010-11-29 11:09:07Z glondu $
4297	4327
4298	4328	%%% Local Variables:
4299	4329	%%% mode: latex

-1

doc/tutorial/Tutorial.tex less more

1573	1573
1574	1574	\end{document}
1575	1575
1576		% $Id: Tutorial.tex 13548 2010-10-14 12:35:43Z notin $
	1576	% $Id: Tutorial.tex 13547 2010-10-14 12:35:00Z notin $

+73

-33

ide/coqide.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: coqide.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
	8	(* $Id: coqide.ml 13708 2010-12-13 14:49:29Z gmelquio $ *)
9	9
10	10	open Preferences
11	11	open Vernacexpr

250	250	end
251	251
252	252	let do_if_not_computing text f x =
253		if Mutex.try_lock coq_computing then
254		let threaded_task () =
255		prerr_endline "Getting lock";
256		try
257		f x;
258		prerr_endline "Releasing lock";
259		Mutex.unlock coq_computing;
260		with e ->
261		prerr_endline "Releasing lock (on error)";
262		Mutex.unlock coq_computing;
263		raise e
264		in
265		prerr_endline ("Launching thread " ^ text);
266		ignore (Glib.Timeout.add ~ms:300 ~callback:
267		(fun () -> if Mutex.try_lock coq_computing
268		then (Mutex.unlock coq_computing; false)
269		else (pbar#pulse (); true)));
270		ignore (Thread.create threaded_task ())
271		else
272		prerr_endline
273		"Discarded order (computations are ongoing)"
	253	let threaded_task () =
	254	(* Beware: mutexes must be locked and unlocked in the same thread
	255	on at least FreeBSD (see bug #2431) *)
	256	if Mutex.try_lock coq_computing then
	257	begin
	258	prerr_endline "Getting lock";
	259	try
	260	f x;
	261	prerr_endline "Releasing lock";
	262	Mutex.unlock coq_computing;
	263	with e ->
	264	prerr_endline "Releasing lock (on error)";
	265	Mutex.unlock coq_computing;
	266	raise e
	267	end
	268	else
	269	prerr_endline
	270	"Discarded order (computations are ongoing)"
	271	in
	272	prerr_endline ("Launching thread " ^ text);
	273	ignore (Glib.Timeout.add ~ms:300 ~callback:
	274	(fun () -> if Mutex.try_lock coq_computing
	275	then (Mutex.unlock coq_computing; false)
	276	else (pbar#pulse (); true)));
	277	ignore (Thread.create threaded_task ())
274	278
275	279	(* XXX - 1 appel *)
276	280	let kill_input_view i =

281	285	v.proof_view#destroy ();
282	286	v.message_view#destroy ();
283	287	session_notebook#remove_page i
	288
	289	let warning msg =
	290	GToolbox.message_box ~title:"Warning"
	291	~icon:(let img = GMisc.image () in
	292	img#set_stock `DIALOG_WARNING;
	293	img#set_icon_size `DIALOG;
	294	img#coerce)
	295	msg
	296
284	297	(*
285	298	(* XXX - beaucoups d'appels, a garder *)
286	299	let get_current_view =
287	300	focused_session
288	301	*)
289	302	let remove_current_view_page () =
290		let c = session_notebook#current_page in
291		kill_input_view c
292
	303	let do_remove () =
	304	let c = session_notebook#current_page in
	305	kill_input_view c
	306	in
	307	let current = session_notebook#current_term in
	308	if current.script#buffer#modified then
	309	match GToolbox.question_box ~title:"Close"
	310	~buttons:["Save Buffer and Close";
	311	"Close without Saving";
	312	"Don't Close"]
	313	~default:0
	314	~icon:(let img = GMisc.image () in
	315	img#set_stock `DIALOG_WARNING;
	316	img#set_icon_size `DIALOG;
	317	img#coerce)
	318	"This buffer has unsaved modifications"
	319	with
	320	\| 1 ->
	321	begin match current.analyzed_view#filename with
	322	\| None ->
	323	begin match select_file_for_save ~title:"Save file" () with
	324	\| None -> ()
	325	\| Some f ->
	326	if current.analyzed_view#save_as f then begin
	327	flash_info ("File " ^ f ^ " saved") ;
	328	do_remove ()
	329	end else
	330	warning ("Save Failed (check if " ^ f ^ " is writable)")
	331	end
	332	\| Some f ->
	333	if current.analyzed_view#save f then begin
	334	flash_info ("File " ^ f ^ " saved") ;
	335	do_remove ()
	336	end else
	337	warning ("Save Failed (check if " ^ f ^ " is writable)")
	338	end
	339	\| 2 -> do_remove ()
	340	\| _ -> ()
293	341
294	342	(* Reset this to None on page change ! *)
295	343	let (last_completion:(stringintint*bool) option ref) = ref None

381	429	(session_notebook#get_nth_term i).analyzed_view#activate ();
382	430	set_active_view i;
383	431	prerr_endline "exiting activate_input"
384
385		let warning msg =
386		GToolbox.message_box ~title:"Warning"
387		~icon:(let img = GMisc.image () in
388		img#set_stock `DIALOG_WARNING;
389		img#set_icon_size `DIALOG;
390		img#coerce)
391		msg
392	432
393	433	let apply_tag (buffer:GText.buffer) orig off_conv from upto sort =
394	434	let conv_and_apply start stop tag =

+99

-0

ide/uim/coqide-custom.scm less more

	0	;;; coqide-custom.scm -- customization variables for coqide.scm
	1	;;;
	2	;;; Copyright (c) 2003-2009 uim Project http://code.google.com/p/uim/
	3	;;;
	4	;;; All rights reserved.
	5	;;;
	6	;;; Redistribution and use in source and binary forms, with or without
	7	;;; modification, are permitted provided that the following conditions
	8	;;; are met:
	9	;;; 1. Redistributions of source code must retain the above copyright
	10	;;; notice, this list of conditions and the following disclaimer.
	11	;;; 2. Redistributions in binary form must reproduce the above copyright
	12	;;; notice, this list of conditions and the following disclaimer in the
	13	;;; documentation and/or other materials provided with the distribution.
	14	;;; 3. Neither the name of authors nor the names of its contributors
	15	;;; may be used to endorse or promote products derived from this software
	16	;;; without specific prior written permission.
	17	;;;
	18	;;; THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS ``AS IS'' AND
	19	;;; ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
	20	;;; IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
	21	;;; ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS OR CONTRIBUTORS BE LIABLE
	22	;;; FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
	23	;;; DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
	24	;;; OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
	25	;;; HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
	26	;;; LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
	27	;;; OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
	28	;;; SUCH DAMAGE.
	29	;;;;
	30
	31	(require "i18n.scm")
	32
	33	(define coqide-im-name-label (N_ "CoqIDE"))
	34	(define coqide-im-short-desc (N_ "Emacs-style Latin characters input"))
	35	(define coqide-im-long-desc (N_ "An input method for entering Latin letters used in European languages with the key translations adopted in Emacs."))
	36
	37	(define-custom-group 'coqide
	38	coqide-im-name-label
	39	coqide-im-short-desc)
	40
	41	(define-custom-group 'coqide-properties
	42	(N_ "Properties")
	43	(N_ "long description will be here."))
	44
	45	(define-custom 'coqide-rules 'coqide-rules-latin-ltx
	46	'(coqide coqide-properties)
	47	(list 'choice
	48	(list 'coqide-rules-latin-ltx
	49	(N_ "TeX")
	50	(N_ "long description will be here.")))
	51	(N_ "Latin characters keyboard layout")
	52	(N_ "long description will be here."))
	53
	54	(custom-add-hook 'coqide-rules
	55	'custom-set-hooks
	56	(lambda ()
	57	(map (lambda (lc)
	58	(let ((new-rkc (rk-context-new
	59	(symbol-value coqide-rules) #f #f)))
	60	(coqide-context-flush lc)
	61	(coqide-update-preedit lc)
	62	(coqide-context-set-rkc! lc new-rkc)))
	63	coqide-context-list)))
	64
	65	;; For VI users.
	66	(define-custom 'coqide-esc-turns-off? #f
	67	'(coqide coqide-properties)
	68	'(boolean)
	69	(N_ "ESC turns off composition mode (for vi users)")
	70	(N_ "long description will be here."))
	71
	72
	73	(define-custom-group 'coqide-keys
	74	(N_ "CoqIDE key bindings")
	75	(N_ "long description will be here."))
	76
	77	(define-custom 'coqide-on-key '("<Control>\\")
	78	'(coqide coqide-keys)
	79	'(key)
	80	(N_ "CoqIDE on")
	81	(N_ "long description will be here"))
	82
	83	(define-custom 'coqide-off-key '("<Control>\\")
	84	'(coqide coqide-keys)
	85	'(key)
	86	(N_ "CoqIDE off")
	87	(N_ "long description will be here"))
	88
	89	(define-custom 'coqide-backspace-key '(generic-backspace-key)
	90	'(coqide coqide-keys)
	91	'(key)
	92	(N_ "CoqIDE backspace")
	93	(N_ "long description will be here"))
	94
	95	;; Local Variables:
	96	;; mode: scheme
	97	;; coding: utf-8
	98	;; End:

+1142

-0

ide/uim/coqide-rules.scm less more

	0	;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
	1	;; v ; The Coq Proof Assistant / The Coq Development Team ;;
	2	;; <O___,, ; INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 ;;
	3	;; \VV/ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
	4	;; // ; This file is distributed under the terms of the ;;
	5	;; ; GNU Lesser General Public License Version 2.1 ;;
	6	;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
	7
	8	;;; coqide-rules.scm -- key sequence tables for coqide.scm
	9
	10	;; Copyright (c) 2003-2009 uim Project http://code.google.com/p/uim/
	11	;;
	12	;; All rights reserved.
	13
	14	;; The translation tables in this file were derived from
	15	;; the emacs-lisp source files latin-pre.el, latin-post.el, latin-alt.el
	16	;; included in GNU Emacs. The following is the original copyright notice
	17	;; therein, with the name GNU Emacs replaced by "this program".
	18
	19	;; Copyright (C) 1997, 1998, 1999, 2000, 2001, 2002, 2003, 2004, 2005,
	20	;; 2006, 2007
	21	;; Free Software Foundation, Inc.
	22	;; Copyright (C) 1997, 1998, 1999, 2000, 2001, 2002, 2003, 2004, 2005,
	23	;; 2006, 2007
	24	;; National Institute of Advanced Industrial Science and Technology (AIST)
	25	;; Registration Number H14PRO021
	26
	27	;; This program is free software; you can redistribute it and/or modify
	28	;; it under the terms of the GNU General Public License as published by
	29	;; the Free Software Foundation; either version 2, or (at your option)
	30	;; any later version.
	31
	32	;; This program is distributed in the hope that it will be useful,
	33	;; but WITHOUT ANY WARRANTY; without even the implied warranty of
	34	;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
	35	;; GNU General Public License for more details.
	36
	37	;; You should have received a copy of the GNU General Public License
	38	;; along with this program. If not, write to the
	39	;; Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
	40	;; Boston, MA 02110-1301, USA.
	41
	42	;;; Commentary:
	43
	44	;; Key translation maps were originally copied from iso-acc.el.
	45	;; latin-1-prefix: extra special characters added, adapted from the vim
	46	;; digraphs (from J.H.M.Dassen <jdassen@wi.leidenuniv.nl>)
	47	;; by R.F. Smith <rsmith@xs4all.nl>
	48	;;
	49	;; polish-slash:
	50	;; Author: Włodek Bzyl <matwb@univ.gda.pl>
	51	;; Maintainer: Włodek Bzyl <matwb@univ.gda.pl>
	52	;;
	53	;; latin-[89]-prefix: Dave Love <fx@gnu.org>
	54
	55	(define coqide-rules-latin-ltx '(
	56	((("!" "`")) ("¡"))
	57	((("\\" "p" "o" "u" "n" "d" "s")) ("£"))
	58	((("\\" "S")) ("§"))
	59	((("\\" "\"" "{" "}")) ("¨"))
	60	((("\\" "c" "o" "p" "y" "r" "i" "g" "h" "t")) ("©"))
	61	((("$" "^" "a" "$")) ("ª"))
	62	((("\\" "=" "{" "}")) ("¯"))
	63	((("$" "\\" "p" "m" "$")) ("±"))
	64	((("\\" "p" "m")) ("±"))
	65	((("$" "^" "2" "$")) ("²"))
	66	((("$" "^" "3" "$")) ("³"))
	67	((("\\" "'" "{" "}")) ("´"))
	68	((("\\" "P")) ("¶"))
	69	((("$" "\\" "c" "d" "o" "t" "$")) ("·"))
	70	((("\\" "c" "d" "o" "t")) ("·"))
	71	((("\\" "c" "{" "}")) ("¸"))
	72	((("$" "^" "1" "$")) ("¹"))
	73	((("$" "^" "o" "$")) ("º"))
	74	((("?" "`")) ("¿"))
	75	((("\\" "`" "{" "A" "}")) ("À"))
	76	((("\\" "`" "A")) ("À"))
	77	((("\\" "'" "{" "A" "}")) ("Á"))
	78	((("\\" "'" "A")) ("Á"))
	79	((("\\" "^" "{" "A" "}")) ("Â"))
	80	((("\\" "^" "A")) ("Â"))
	81	((("\\" "~" "{" "A" "}")) ("Ã"))
	82	((("\\" "~" "A")) ("Ã"))
	83	((("\\" "\"" "{" "A" "}")) ("Ä"))
	84	((("\\" "\"" "A")) ("Ä"))
	85	((("\\" "k" "{" "A" "}")) ("Ą"))
	86	((("\\" "A" "A")) ("Å"))
	87	((("\\" "A" "E")) ("Æ"))
	88	((("\\" "c" "{" "C" "}")) ("Ç"))
	89	((("\\" "c" "C")) ("Ç"))
	90	((("\\" "`" "{" "E" "}")) ("È"))
	91	((("\\" "`" "E")) ("È"))
	92	((("\\" "'" "{" "E" "}")) ("É"))
	93	((("\\" "'" "E")) ("É"))
	94	((("\\" "^" "{" "E" "}")) ("Ê"))
	95	((("\\" "^" "E")) ("Ê"))
	96	((("\\" "\"" "{" "E" "}")) ("Ë"))
	97	((("\\" "\"" "E")) ("Ë"))
	98	((("\\" "k" "{" "E" "}")) ("Ę"))
	99	((("\\" "`" "{" "I" "}")) ("Ì"))
	100	((("\\" "`" "I")) ("Ì"))
	101	((("\\" "'" "{" "I" "}")) ("Í"))
	102	((("\\" "'" "I")) ("Í"))
	103	((("\\" "^" "{" "I" "}")) ("Î"))
	104	((("\\" "^" "I")) ("Î"))
	105	((("\\" "\"" "{" "I" "}")) ("Ï"))
	106	((("\\" "\"" "I")) ("Ï"))
	107	((("\\" "k" "{" "I" "}")) ("Į"))
	108	((("\\" "~" "{" "N" "}")) ("Ñ"))
	109	((("\\" "~" "N")) ("Ñ"))
	110	((("\\" "`" "{" "O" "}")) ("Ò"))
	111	((("\\" "`" "O")) ("Ò"))
	112	((("\\" "'" "{" "O" "}")) ("Ó"))
	113	((("\\" "'" "O")) ("Ó"))
	114	((("\\" "^" "{" "O" "}")) ("Ô"))
	115	((("\\" "^" "O")) ("Ô"))
	116	((("\\" "~" "{" "O" "}")) ("Õ"))
	117	((("\\" "~" "O")) ("Õ"))
	118	((("\\" "\"" "{" "O" "}")) ("Ö"))
	119	((("\\" "\"" "O")) ("Ö"))
	120	((("\\" "k" "{" "O" "}")) ("Ǫ"))
	121	((("$" "\\" "t" "i" "m" "e" "s" "$")) ("×"))
	122	((("\\" "t" "i" "m" "e" "s")) ("×"))
	123	((("\\" "O")) ("Ø"))
	124	((("\\" "`" "{" "U" "}")) ("Ù"))
	125	((("\\" "`" "U")) ("Ù"))
	126	((("\\" "'" "{" "U" "}")) ("Ú"))
	127	((("\\" "'" "U")) ("Ú"))
	128	((("\\" "^" "{" "U" "}")) ("Û"))
	129	((("\\" "^" "U")) ("Û"))
	130	((("\\" "\"" "{" "U" "}")) ("Ü"))
	131	((("\\" "\"" "U")) ("Ü"))
	132	((("\\" "k" "{" "U" "}")) ("Ų"))
	133	((("\\" "'" "{" "Y" "}")) ("Ý"))
	134	((("\\" "'" "Y")) ("Ý"))
	135	((("\\" "s" "s")) ("ß"))
	136	((("\\" "`" "{" "a" "}")) ("à"))
	137	((("\\" "`" "a")) ("à"))
	138	((("\\" "'" "{" "a" "}")) ("á"))
	139	((("\\" "'" "a")) ("á"))
	140	((("\\" "^" "{" "a" "}")) ("â"))
	141	((("\\" "^" "a")) ("â"))
	142	((("\\" "~" "{" "a" "}")) ("ã"))
	143	((("\\" "~" "a")) ("ã"))
	144	((("\\" "\"" "{" "a" "}")) ("ä"))
	145	((("\\" "\"" "a")) ("ä"))
	146	((("\\" "k" "{" "a" "}")) ("ą"))
	147	((("\\" "a" "a")) ("å"))
	148	((("\\" "a" "e")) ("æ"))
	149	((("\\" "c" "{" "c" "}")) ("ç"))
	150	((("\\" "c" "c")) ("ç"))
	151	((("\\" "`" "{" "e" "}")) ("è"))
	152	((("\\" "`" "e")) ("è"))
	153	((("\\" "'" "{" "e" "}")) ("é"))
	154	((("\\" "'" "e")) ("é"))
	155	((("\\" "^" "{" "e" "}")) ("ê"))
	156	((("\\" "^" "e")) ("ê"))
	157	((("\\" "\"" "{" "e" "}")) ("ë"))
	158	((("\\" "\"" "e")) ("ë"))
	159	((("\\" "k" "{" "e" "}")) ("ę"))
	160	((("\\" "`" "{" "\\" "i" "}")) ("ì"))
	161	((("\\" "`" "i")) ("ì"))
	162	((("\\" "'" "{" "\\" "i" "}")) ("í"))
	163	((("\\" "'" "i")) ("í"))
	164	((("\\" "^" "{" "\\" "i" "}")) ("î"))
	165	((("\\" "^" "i")) ("î"))
	166	((("\\" "\"" "{" "\\" "i" "}")) ("ï"))
	167	((("\\" "\"" "i")) ("ï"))
	168	((("\\" "k" "{" "i" "}")) ("į"))
	169	((("\\" "~" "{" "n" "}")) ("ñ"))
	170	((("\\" "~" "n")) ("ñ"))
	171	((("\\" "`" "{" "o" "}")) ("ò"))
	172	((("\\" "`" "o")) ("ò"))
	173	((("\\" "'" "{" "o" "}")) ("ó"))
	174	((("\\" "'" "o")) ("ó"))
	175	((("\\" "^" "{" "o" "}")) ("ô"))
	176	((("\\" "^" "o")) ("ô"))
	177	((("\\" "~" "{" "o" "}")) ("õ"))
	178	((("\\" "~" "o")) ("õ"))
	179	((("\\" "\"" "{" "o" "}")) ("ö"))
	180	((("\\" "\"" "o")) ("ö"))
	181	((("\\" "k" "{" "o" "}")) ("ǫ"))
	182	((("$" "\\" "d" "i" "v" "$")) ("÷"))
	183	((("\\" "d" "i" "v")) ("÷"))
	184	((("\\" "o")) ("ø"))
	185	((("\\" "`" "{" "u" "}")) ("ù"))
	186	((("\\" "`" "u")) ("ù"))
	187	((("\\" "'" "{" "u" "}")) ("ú"))
	188	((("\\" "'" "u")) ("ú"))
	189	((("\\" "^" "{" "u" "}")) ("û"))
	190	((("\\" "^" "u")) ("û"))
	191	((("\\" "\"" "{" "u" "}")) ("ü"))
	192	((("\\" "\"" "u")) ("ü"))
	193	((("\\" "k" "{" "u" "}")) ("ų"))
	194	((("\\" "'" "{" "y" "}")) ("ý"))
	195	((("\\" "'" "y")) ("ý"))
	196	((("\\" "\"" "{" "y" "}")) ("ÿ"))
	197	((("\\" "\"" "y")) ("ÿ"))
	198	((("\\" "=" "{" "A" "}")) ("Ā"))
	199	((("\\" "=" "A")) ("Ā"))
	200	((("\\" "=" "{" "a" "}")) ("ā"))
	201	((("\\" "=" "a")) ("ā"))
	202	((("\\" "u" "{" "A" "}")) ("Ă"))
	203	((("\\" "u" "A")) ("Ă"))
	204	((("\\" "u" "{" "a" "}")) ("ă"))
	205	((("\\" "u" "a")) ("ă"))
	206	((("\\" "'" "{" "C" "}")) ("Ć"))
	207	((("\\" "'" "C")) ("Ć"))
	208	((("\\" "'" "{" "c" "}")) ("ć"))
	209	((("\\" "'" "c")) ("ć"))
	210	((("\\" "^" "{" "C" "}")) ("Ĉ"))
	211	((("\\" "^" "C")) ("Ĉ"))
	212	((("\\" "^" "{" "c" "}")) ("ĉ"))
	213	((("\\" "^" "c")) ("ĉ"))
	214	((("\\" "." "{" "C" "}")) ("Ċ"))
	215	((("\\" "." "C")) ("Ċ"))
	216	((("\\" "." "{" "c" "}")) ("ċ"))
	217	((("\\" "." "c")) ("ċ"))
	218	((("\\" "v" "{" "C" "}")) ("Č"))
	219	((("\\" "v" "C")) ("Č"))
	220	((("\\" "v" "{" "c" "}")) ("č"))
	221	((("\\" "v" "c")) ("č"))
	222	((("\\" "v" "{" "D" "}")) ("Ď"))
	223	((("\\" "v" "D")) ("Ď"))
	224	((("\\" "v" "{" "d" "}")) ("ď"))
	225	((("\\" "v" "d")) ("ď"))
	226	((("\\" "=" "{" "E" "}")) ("Ē"))
	227	((("\\" "=" "E")) ("Ē"))
	228	((("\\" "=" "{" "e" "}")) ("ē"))
	229	((("\\" "=" "e")) ("ē"))
	230	((("\\" "u" "{" "E" "}")) ("Ĕ"))
	231	((("\\" "u" "E")) ("Ĕ"))
	232	((("\\" "u" "{" "e" "}")) ("ĕ"))
	233	((("\\" "u" "e")) ("ĕ"))
	234	((("\\" "." "{" "E" "}")) ("Ė"))
	235	((("\\" "." "E")) ("Ė"))
	236	((("\\" "e" "{" "e" "}")) ("ė"))
	237	((("\\" "e" "e")) ("ė"))
	238	((("\\" "v" "{" "E" "}")) ("Ě"))
	239	((("\\" "v" "E")) ("Ě"))
	240	((("\\" "v" "{" "e" "}")) ("ě"))
	241	((("\\" "v" "e")) ("ě"))
	242	((("\\" "^" "{" "G" "}")) ("Ĝ"))
	243	((("\\" "^" "G")) ("Ĝ"))
	244	((("\\" "^" "{" "g" "}")) ("ĝ"))
	245	((("\\" "^" "g")) ("ĝ"))
	246	((("\\" "u" "{" "G" "}")) ("Ğ"))
	247	((("\\" "u" "G")) ("Ğ"))
	248	((("\\" "u" "{" "g" "}")) ("ğ"))
	249	((("\\" "u" "g")) ("ğ"))
	250	((("\\" "." "{" "G" "}")) ("Ġ"))
	251	((("\\" "." "G")) ("Ġ"))
	252	((("\\" "." "{" "g" "}")) ("ġ"))
	253	((("\\" "." "g")) ("ġ"))
	254	((("\\" "c" "{" "G" "}")) ("Ģ"))
	255	((("\\" "c" "G")) ("Ģ"))
	256	((("\\" "c" "{" "g" "}")) ("ģ"))
	257	((("\\" "c" "g")) ("ģ"))
	258	((("\\" "^" "{" "H" "}")) ("Ĥ"))
	259	((("\\" "^" "H")) ("Ĥ"))
	260	((("\\" "^" "{" "h" "}")) ("ĥ"))
	261	((("\\" "^" "h")) ("ĥ"))
	262	((("\\" "~" "{" "I" "}")) ("Ĩ"))
	263	((("\\" "~" "I")) ("Ĩ"))
	264	((("\\" "~" "{" "\\" "i" "}")) ("ĩ"))
	265	((("\\" "~" "i")) ("ĩ"))
	266	((("\\" "=" "{" "I" "}")) ("Ī"))
	267	((("\\" "=" "I")) ("Ī"))
	268	((("\\" "=" "{" "\\" "i" "}")) ("ī"))
	269	((("\\" "=" "i")) ("ī"))
	270	((("\\" "u" "{" "I" "}")) ("Ĭ"))
	271	((("\\" "u" "I")) ("Ĭ"))
	272	((("\\" "u" "{" "\\" "i" "}")) ("ĭ"))
	273	((("\\" "u" "i")) ("ĭ"))
	274	((("\\" "." "{" "I" "}")) ("İ"))
	275	((("\\" "." "I")) ("İ"))
	276	((("\\" "i")) ("ı"))
	277	((("\\" "^" "{" "J" "}")) ("Ĵ"))
	278	((("\\" "^" "J")) ("Ĵ"))
	279	((("\\" "^" "{" "\\" "j" "}")) ("ĵ"))
	280	((("\\" "^" "j")) ("ĵ"))
	281	((("\\" "c" "{" "K" "}")) ("Ķ"))
	282	((("\\" "c" "K")) ("Ķ"))
	283	((("\\" "c" "{" "k" "}")) ("ķ"))
	284	((("\\" "c" "k")) ("ķ"))
	285	((("\\" "'" "{" "L" "}")) ("Ĺ"))
	286	((("\\" "'" "L")) ("Ĺ"))
	287	((("\\" "'" "{" "l" "}")) ("ĺ"))
	288	((("\\" "'" "l")) ("ĺ"))
	289	((("\\" "c" "{" "L" "}")) ("Ļ"))
	290	((("\\" "c" "L")) ("Ļ"))
	291	((("\\" "c" "{" "l" "}")) ("ļ"))
	292	((("\\" "c" "l")) ("ļ"))
	293	((("\\" "L")) ("Ł"))
	294	((("\\" "l")) ("ł"))
	295	((("\\" "'" "{" "N" "}")) ("Ń"))
	296	((("\\" "'" "N")) ("Ń"))
	297	((("\\" "'" "{" "n" "}")) ("ń"))
	298	((("\\" "'" "n")) ("ń"))
	299	((("\\" "c" "{" "N" "}")) ("Ņ"))
	300	((("\\" "c" "N")) ("Ņ"))
	301	((("\\" "c" "{" "n" "}")) ("ņ"))
	302	((("\\" "c" "n")) ("ņ"))
	303	((("\\" "v" "{" "N" "}")) ("Ň"))
	304	((("\\" "v" "N")) ("Ň"))
	305	((("\\" "v" "{" "n" "}")) ("ň"))
	306	((("\\" "v" "n")) ("ň"))
	307	((("\\" "=" "{" "O" "}")) ("Ō"))
	308	((("\\" "=" "O")) ("Ō"))
	309	((("\\" "=" "{" "o" "}")) ("ō"))
	310	((("\\" "=" "o")) ("ō"))
	311	((("\\" "u" "{" "O" "}")) ("Ŏ"))
	312	((("\\" "u" "O")) ("Ŏ"))
	313	((("\\" "u" "{" "o" "}")) ("ŏ"))
	314	((("\\" "u" "o")) ("ŏ"))
	315	((("\\" "H" "{" "O" "}")) ("Ő"))
	316	((("\\" "H" "O")) ("Ő"))
	317	((("\\" "U" "{" "o" "}")) ("ő"))
	318	((("\\" "U" "o")) ("ő"))
	319	((("\\" "O" "E")) ("Œ"))
	320	((("\\" "o" "e")) ("œ"))
	321	((("\\" "'" "{" "R" "}")) ("Ŕ"))
	322	((("\\" "'" "R")) ("Ŕ"))
	323	((("\\" "'" "{" "r" "}")) ("ŕ"))
	324	((("\\" "'" "r")) ("ŕ"))
	325	((("\\" "c" "{" "R" "}")) ("Ŗ"))
	326	((("\\" "c" "R")) ("Ŗ"))
	327	((("\\" "c" "{" "r" "}")) ("ŗ"))
	328	((("\\" "c" "r")) ("ŗ"))
	329	((("\\" "v" "{" "R" "}")) ("Ř"))
	330	((("\\" "v" "R")) ("Ř"))
	331	((("\\" "v" "{" "r" "}")) ("ř"))
	332	((("\\" "v" "r")) ("ř"))
	333	((("\\" "'" "{" "S" "}")) ("Ś"))
	334	((("\\" "'" "S")) ("Ś"))
	335	((("\\" "'" "{" "s" "}")) ("ś"))
	336	((("\\" "'" "s")) ("ś"))
	337	((("\\" "^" "{" "S" "}")) ("Ŝ"))
	338	((("\\" "^" "S")) ("Ŝ"))
	339	((("\\" "^" "{" "s" "}")) ("ŝ"))
	340	((("\\" "^" "s")) ("ŝ"))
	341	((("\\" "c" "{" "S" "}")) ("Ş"))
	342	((("\\" "c" "S")) ("Ş"))
	343	((("\\" "c" "{" "s" "}")) ("ş"))
	344	((("\\" "c" "s")) ("ş"))
	345	((("\\" "v" "{" "S" "}")) ("Š"))
	346	((("\\" "v" "S")) ("Š"))
	347	((("\\" "v" "{" "s" "}")) ("š"))
	348	((("\\" "v" "s")) ("š"))
	349	((("\\" "c" "{" "T" "}")) ("Ţ"))
	350	((("\\" "c" "T")) ("Ţ"))
	351	((("\\" "c" "{" "t" "}")) ("ţ"))
	352	((("\\" "c" "t")) ("ţ"))
	353	((("\\" "v" "{" "T" "}")) ("Ť"))
	354	((("\\" "v" "T")) ("Ť"))
	355	((("\\" "v" "{" "t" "}")) ("ť"))
	356	((("\\" "v" "t")) ("ť"))
	357	((("\\" "~" "{" "U" "}")) ("Ũ"))
	358	((("\\" "~" "U")) ("Ũ"))
	359	((("\\" "~" "{" "u" "}")) ("ũ"))
	360	((("\\" "~" "u")) ("ũ"))
	361	((("\\" "=" "{" "U" "}")) ("Ū"))
	362	((("\\" "=" "U")) ("Ū"))
	363	((("\\" "=" "{" "u" "}")) ("ū"))
	364	((("\\" "=" "u")) ("ū"))
	365	((("\\" "u" "{" "U" "}")) ("Ŭ"))
	366	((("\\" "u" "U")) ("Ŭ"))
	367	((("\\" "u" "{" "u" "}")) ("ŭ"))
	368	((("\\" "u" "u")) ("ŭ"))
	369	((("\\" "H" "{" "U" "}")) ("Ű"))
	370	((("\\" "H" "U")) ("Ű"))
	371	((("\\" "H" "{" "u" "}")) ("ű"))
	372	((("\\" "H" "u")) ("ű"))
	373	((("\\" "^" "{" "W" "}")) ("Ŵ"))
	374	((("\\" "^" "W")) ("Ŵ"))
	375	((("\\" "^" "{" "w" "}")) ("ŵ"))
	376	((("\\" "^" "w")) ("ŵ"))
	377	((("\\" "^" "{" "Y" "}")) ("Ŷ"))
	378	((("\\" "^" "Y")) ("Ŷ"))
	379	((("\\" "^" "{" "y" "}")) ("ŷ"))
	380	((("\\" "^" "y")) ("ŷ"))
	381	((("\\" "\"" "{" "Y" "}")) ("Ÿ"))
	382	((("\\" "\"" "Y")) ("Ÿ"))
	383	((("\\" "'" "{" "Z" "}")) ("Ź"))
	384	((("\\" "'" "Z")) ("Ź"))
	385	((("\\" "'" "{" "z" "}")) ("ź"))
	386	((("\\" "'" "z")) ("ź"))
	387	((("\\" "." "{" "Z" "}")) ("Ż"))
	388	((("\\" "." "Z")) ("Ż"))
	389	((("\\" "." "{" "z" "}")) ("ż"))
	390	((("\\" "." "z")) ("ż"))
	391	((("\\" "v" "{" "Z" "}")) ("Ž"))
	392	((("\\" "v" "Z")) ("Ž"))
	393	((("\\" "v" "{" "z" "}")) ("ž"))
	394	((("\\" "v" "z")) ("ž"))
	395	((("\\" "v" "{" "A" "}")) ("Ǎ"))
	396	((("\\" "v" "A")) ("Ǎ"))
	397	((("\\" "v" "{" "a" "}")) ("ǎ"))
	398	((("\\" "v" "a")) ("ǎ"))
	399	((("\\" "v" "{" "I" "}")) ("Ǐ"))
	400	((("\\" "v" "I")) ("Ǐ"))
	401	((("\\" "v" "{" "\\" "i" "}")) ("ǐ"))
	402	((("\\" "v" "i")) ("ǐ"))
	403	((("\\" "v" "{" "O" "}")) ("Ǒ"))
	404	((("\\" "v" "O")) ("Ǒ"))
	405	((("\\" "v" "{" "o" "}")) ("ǒ"))
	406	((("\\" "v" "o")) ("ǒ"))
	407	((("\\" "v" "{" "U" "}")) ("Ǔ"))
	408	((("\\" "v" "U")) ("Ǔ"))
	409	((("\\" "v" "{" "u" "}")) ("ǔ"))
	410	((("\\" "v" "u")) ("ǔ"))
	411	((("\\" "=" "{" "\\" "A" "E" "}")) ("Ǣ"))
	412	((("\\" "=" "\\" "A" "E")) ("Ǣ"))
	413	((("\\" "=" "{" "\\" "a" "e" "}")) ("ǣ"))
	414	((("\\" "=" "\\" "a" "e")) ("ǣ"))
	415	((("\\" "v" "{" "G" "}")) ("Ǧ"))
	416	((("\\" "v" "G")) ("Ǧ"))
	417	((("\\" "v" "{" "g" "}")) ("ǧ"))
	418	((("\\" "v" "g")) ("ǧ"))
	419	((("\\" "v" "{" "K" "}")) ("Ǩ"))
	420	((("\\" "v" "K")) ("Ǩ"))
	421	((("\\" "v" "{" "k" "}")) ("ǩ"))
	422	((("\\" "v" "k")) ("ǩ"))
	423	((("\\" "v" "{" "\\" "j" "}")) ("ǰ"))
	424	((("\\" "v" "j")) ("ǰ"))
	425	((("\\" "'" "{" "G" "}")) ("Ǵ"))
	426	((("\\" "'" "G")) ("Ǵ"))
	427	((("\\" "'" "{" "g" "}")) ("ǵ"))
	428	((("\\" "'" "g")) ("ǵ"))
	429	((("\\" "`" "{" "N" "}")) ("Ǹ"))
	430	((("\\" "`" "N")) ("Ǹ"))
	431	((("\\" "`" "{" "n" "}")) ("ǹ"))
	432	((("\\" "`" "n")) ("ǹ"))
	433	((("\\" "'" "{" "\\" "A" "E" "}")) ("Ǽ"))
	434	((("\\" "'" "\\" "A" "E")) ("Ǽ"))
	435	((("\\" "'" "{" "\\" "a" "e" "}")) ("ǽ"))
	436	((("\\" "'" "\\" "a" "e")) ("ǽ"))
	437	((("\\" "'" "{" "\\" "O" "}")) ("Ǿ"))
	438	((("\\" "'" "\\" "O")) ("Ǿ"))
	439	((("\\" "'" "{" "\\" "o" "}")) ("ǿ"))
	440	((("\\" "'" "\\" "o")) ("ǿ"))
	441	((("\\" "v" "{" "H" "}")) ("Ȟ"))
	442	((("\\" "v" "H")) ("Ȟ"))
	443	((("\\" "v" "{" "h" "}")) ("ȟ"))
	444	((("\\" "v" "h")) ("ȟ"))
	445	((("\\" "." "{" "A" "}")) ("Ȧ"))
	446	((("\\" "." "A")) ("Ȧ"))
	447	((("\\" "." "{" "a" "}")) ("ȧ"))
	448	((("\\" "." "a")) ("ȧ"))
	449	((("\\" "c" "{" "E" "}")) ("Ȩ"))
	450	((("\\" "c" "E")) ("Ȩ"))
	451	((("\\" "c" "{" "e" "}")) ("ȩ"))
	452	((("\\" "c" "e")) ("ȩ"))
	453	((("\\" "." "{" "O" "}")) ("Ȯ"))
	454	((("\\" "." "O")) ("Ȯ"))
	455	((("\\" "." "{" "o" "}")) ("ȯ"))
	456	((("\\" "." "o")) ("ȯ"))
	457	((("\\" "=" "{" "Y" "}")) ("Ȳ"))
	458	((("\\" "=" "Y")) ("Ȳ"))
	459	((("\\" "=" "{" "y" "}")) ("ȳ"))
	460	((("\\" "=" "y")) ("ȳ"))
	461	((("\\" "v" "{" "}")) ("ˇ"))
	462	((("\\" "u" "{" "}")) ("˘"))
	463	((("\\" "." "{" "}")) ("˙"))
	464	((("\\" "~" "{" "}")) ("˜"))
	465	((("\\" "H" "{" "}")) ("˝"))
	466	((("\\" "'")) ("́"))
	467	((("\\" "'" "K")) ("Ḱ"))
	468	((("\\" "'" "M")) ("Ḿ"))
	469	((("\\" "'" "P")) ("Ṕ"))
	470	((("\\" "'" "W")) ("Ẃ"))
	471	((("\\" "'" "k")) ("ḱ"))
	472	((("\\" "'" "m")) ("ḿ"))
	473	((("\\" "'" "p")) ("ṕ"))
	474	((("\\" "'" "w")) ("ẃ"))
	475	((("\\" ",")) (" "))
	476	((("\\" ".")) ("̇"))
	477	((("\\" "." "B")) ("Ḃ"))
	478	((("\\" "." "D")) ("Ḋ"))
	479	((("\\" "." "F")) ("Ḟ"))
	480	((("\\" "." "H")) ("Ḣ"))
	481	((("\\" "." "M")) ("Ṁ"))
	482	((("\\" "." "N")) ("Ṅ"))
	483	((("\\" "." "P")) ("Ṗ"))
	484	((("\\" "." "R")) ("Ṙ"))
	485	((("\\" "." "S")) ("Ṡ"))
	486	((("\\" "." "T")) ("Ṫ"))
	487	((("\\" "." "W")) ("Ẇ"))
	488	((("\\" "." "X")) ("Ẋ"))
	489	((("\\" "." "Y")) ("Ẏ"))
	490	((("\\" "." "b")) ("ḃ"))
	491	((("\\" "." "d")) ("ḋ"))
	492	((("\\" "." "e")) ("ė"))
	493	((("\\" "." "f")) ("ḟ"))
	494	((("\\" "." "h")) ("ḣ"))
	495	((("\\" "." "m")) ("ṁ"))
	496	((("\\" "." "n")) ("ṅ"))
	497	((("\\" "." "p")) ("ṗ"))
	498	((("\\" "." "r")) ("ṙ"))
	499	((("\\" "." "s")) ("ṡ"))
	500	((("\\" "." "t")) ("ṫ"))
	501	((("\\" "." "w")) ("ẇ"))
	502	((("\\" "." "x")) ("ẋ"))
	503	((("\\" "." "y")) ("ẏ"))
	504	((("\\" "/")) ("‌"))
	505	((("\\" ":")) (" "))
	506	((("\\" ";")) (" "))
	507	((("\\" "=")) ("̄"))
	508	((("\\" "=" "G")) ("Ḡ"))
	509	((("\\" "=" "g")) ("ḡ"))
	510	((("^" "(")) ("⁽"))
	511	((("^" ")")) ("⁾"))
	512	((("^" "+")) ("⁺"))
	513	((("^" "-")) ("⁻"))
	514	((("^" "0")) ("⁰"))
	515	((("^" "1")) ("¹"))
	516	((("^" "2")) ("²"))
	517	((("^" "3")) ("³"))
	518	((("^" "4")) ("⁴"))
	519	((("^" "5")) ("⁵"))
	520	((("^" "6")) ("⁶"))
	521	((("^" "7")) ("⁷"))
	522	((("^" "8")) ("⁸"))
	523	((("^" "9")) ("⁹"))
	524	((("^" "=")) ("⁼"))
	525	((("^" "\\" "g" "a" "m" "m" "a")) ("ˠ"))
	526	((("^" "h")) ("ʰ"))
	527	((("^" "j")) ("ʲ"))
	528	((("^" "l")) ("ˡ"))
	529	((("^" "n")) ("ⁿ"))
	530	((("^" "o")) ("º"))
	531	((("^" "r")) ("ʳ"))
	532	((("^" "s")) ("ˢ"))
	533	((("^" "w")) ("ʷ"))
	534	((("^" "x")) ("ˣ"))
	535	((("^" "y")) ("ʸ"))
	536	((("^" "{" "S" "M" "}")) ("℠"))
	537	((("^" "{" "T" "E" "L" "}")) ("℡"))
	538	((("^" "{" "T" "M" "}")) ("™"))
	539	((("_" "(")) ("₍"))
	540	((("_" ")")) ("₎"))
	541	((("_" "+")) ("₊"))
	542	((("_" "-")) ("₋"))
	543	((("_" "0")) ("₀"))
	544	((("_" "1")) ("₁"))
	545	((("_" "2")) ("₂"))
	546	((("_" "3")) ("₃"))
	547	((("_" "4")) ("₄"))
	548	((("_" "5")) ("₅"))
	549	((("_" "6")) ("₆"))
	550	((("_" "7")) ("₇"))
	551	((("_" "8")) ("₈"))
	552	((("_" "9")) ("₉"))
	553	((("_" "=")) ("₌"))
	554	((("\\" "~")) ("̃"))
	555	((("\\" "~" "E")) ("Ẽ"))
	556	((("\\" "~" "V")) ("Ṽ"))
	557	((("\\" "~" "Y")) ("Ỹ"))
	558	((("\\" "~" "e")) ("ẽ"))
	559	((("\\" "~" "v")) ("ṽ"))
	560	((("\\" "~" "y")) ("ỹ"))
	561	((("\\" "\"")) ("̈"))
	562	((("\\" "\"" "H")) ("Ḧ"))
	563	((("\\" "\"" "W")) ("Ẅ"))
	564	((("\\" "\"" "X")) ("Ẍ"))
	565	((("\\" "\"" "h")) ("ḧ"))
	566	((("\\" "\"" "t")) ("ẗ"))
	567	((("\\" "\"" "w")) ("ẅ"))
	568	((("\\" "\"" "x")) ("ẍ"))
	569	((("\\" "^")) ("̂"))
	570	((("\\" "^" "Z")) ("Ẑ"))
	571	((("\\" "^" "z")) ("ẑ"))
	572	((("\\" "`")) ("̀"))
	573	((("\\" "`" "W")) ("Ẁ"))
	574	((("\\" "`" "Y")) ("Ỳ"))
	575	((("\\" "`" "w")) ("ẁ"))
	576	((("\\" "`" "y")) ("ỳ"))
	577	((("\\" "b")) ("̱"))
	578	((("\\" "c")) ("̧"))
	579	((("\\" "c" "{" "D" "}")) ("Ḑ"))
	580	((("\\" "c" "{" "H" "}")) ("Ḩ"))
	581	((("\\" "c" "{" "d" "}")) ("ḑ"))
	582	((("\\" "c" "{" "h" "}")) ("ḩ"))
	583	((("\\" "d")) ("̣"))
	584	((("\\" "d" "{" "A" "}")) ("Ạ"))
	585	((("\\" "d" "{" "B" "}")) ("Ḅ"))
	586	((("\\" "d" "{" "D" "}")) ("Ḍ"))
	587	((("\\" "d" "{" "E" "}")) ("Ẹ"))
	588	((("\\" "d" "{" "H" "}")) ("Ḥ"))
	589	((("\\" "d" "{" "I" "}")) ("Ị"))
	590	((("\\" "d" "{" "K" "}")) ("Ḳ"))
	591	((("\\" "d" "{" "L" "}")) ("Ḷ"))
	592	((("\\" "d" "{" "M" "}")) ("Ṃ"))
	593	((("\\" "d" "{" "N" "}")) ("Ṇ"))
	594	((("\\" "d" "{" "O" "}")) ("Ọ"))
	595	((("\\" "d" "{" "R" "}")) ("Ṛ"))
	596	((("\\" "d" "{" "S" "}")) ("Ṣ"))
	597	((("\\" "d" "{" "T" "}")) ("Ṭ"))
	598	((("\\" "d" "{" "U" "}")) ("Ụ"))
	599	((("\\" "d" "{" "V" "}")) ("Ṿ"))
	600	((("\\" "d" "{" "W" "}")) ("Ẉ"))
	601	((("\\" "d" "{" "Y" "}")) ("Ỵ"))
	602	((("\\" "d" "{" "Z" "}")) ("Ẓ"))
	603	((("\\" "d" "{" "a" "}")) ("ạ"))
	604	((("\\" "d" "{" "b" "}")) ("ḅ"))
	605	((("\\" "d" "{" "d" "}")) ("ḍ"))
	606	((("\\" "d" "{" "e" "}")) ("ẹ"))
	607	((("\\" "d" "{" "h" "}")) ("ḥ"))
	608	((("\\" "d" "{" "i" "}")) ("ị"))
	609	((("\\" "d" "{" "k" "}")) ("ḳ"))
	610	((("\\" "d" "{" "l" "}")) ("ḷ"))
	611	((("\\" "d" "{" "m" "}")) ("ṃ"))
	612	((("\\" "d" "{" "n" "}")) ("ṇ"))
	613	((("\\" "d" "{" "o" "}")) ("ọ"))
	614	((("\\" "d" "{" "r" "}")) ("ṛ"))
	615	((("\\" "d" "{" "s" "}")) ("ṣ"))
	616	((("\\" "d" "{" "t" "}")) ("ṭ"))
	617	((("\\" "d" "{" "u" "}")) ("ụ"))
	618	((("\\" "d" "{" "v" "}")) ("ṿ"))
	619	((("\\" "d" "{" "w" "}")) ("ẉ"))
	620	((("\\" "d" "{" "y" "}")) ("ỵ"))
	621	((("\\" "d" "{" "z" "}")) ("ẓ"))
	622	((("\\" "r" "q")) ("’"))
	623	((("\\" "u")) ("̆"))
	624	((("\\" "v")) ("̌"))
	625	((("\\" "v" "{" "L" "}")) ("Ľ"))
	626	((("\\" "v" "{" "i" "}")) ("ǐ"))
	627	((("\\" "v" "{" "j" "}")) ("ǰ"))
	628	((("\\" "v" "{" "l" "}")) ("ľ"))
	629	((("\\" "y" "e" "n")) ("¥"))
	630	((("\\" "B" "o" "x")) ("□"))
	631	((("\\" "B" "u" "m" "p" "e" "q")) ("≎"))
	632	((("\\" "C" "a" "p")) ("⋒"))
	633	((("\\" "C" "u" "p")) ("⋓"))
	634	((("\\" "D" "e" "l" "t" "a")) ("Δ"))
	635	((("\\" "D" "i" "a" "m" "o" "n" "d")) ("◇"))
	636	((("\\" "D" "o" "w" "n" "a" "r" "r" "o" "w")) ("⇓"))
	637	((("\\" "G" "a" "m" "m" "a")) ("Γ"))
	638	((("\\" "H")) ("̋"))
	639	((("\\" "H" "{" "o" "}")) ("ő"))
	640	((("\\" "I" "m")) ("ℑ"))
	641	((("\\" "J" "o" "i" "n")) ("⋈"))
	642	((("\\" "L" "a" "m" "b" "d" "a")) ("Λ"))
	643	((("\\" "L" "e" "f" "t" "a" "r" "r" "o" "w")) ("⇐"))
	644	((("\\" "L" "e" "f" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("⇔"))
	645	((("\\" "L" "l")) ("⋘"))
	646	((("\\" "L" "l" "e" "f" "t" "a" "r" "r" "o" "w")) ("⇚"))
	647	((("\\" "L" "o" "n" "g" "l" "e" "f" "t" "a" "r" "r" "o" "w")) ("⇐"))
	648	((("\\" "L" "o" "n" "g" "l" "e" "f" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("⇔"))
	649	((("\\" "L" "o" "n" "g" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("⇒"))
	650	((("\\" "L" "s" "h")) ("↰"))
	651	((("\\" "O" "m" "e" "g" "a")) ("Ω"))
	652	((("\\" "P" "h" "i")) ("Φ"))
	653	((("\\" "P" "i")) ("Π"))
	654	((("\\" "P" "s" "i")) ("Ψ"))
	655	((("\\" "R" "e")) ("ℜ"))
	656	((("\\" "R" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("⇒"))
	657	((("\\" "R" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("⇛"))
	658	((("\\" "R" "s" "h")) ("↱"))
	659	((("\\" "S" "i" "g" "m" "a")) ("Σ"))
	660	((("\\" "S" "u" "b" "s" "e" "t")) ("⋐"))
	661	((("\\" "S" "u" "p" "s" "e" "t")) ("⋑"))
	662	((("\\" "T" "h" "e" "t" "a")) ("Θ"))
	663	((("\\" "U" "p" "a" "r" "r" "o" "w")) ("⇑"))
	664	((("\\" "U" "p" "d" "o" "w" "n" "a" "r" "r" "o" "w")) ("⇕"))
	665	((("\\" "U" "p" "s" "i" "l" "o" "n")) ("Υ"))
	666	((("\\" "V" "d" "a" "s" "h")) ("⊩"))
	667	((("\\" "V" "e" "r" "t")) ("‖"))
	668	((("\\" "V" "v" "d" "a" "s" "h")) ("⊪"))
	669	((("\\" "X" "i")) ("Ξ"))
	670	((("\\" "a" "l" "e" "p" "h")) ("א"))
	671	((("\\" "a" "l" "p" "h" "a")) ("α"))
	672	((("\\" "a" "m" "a" "l" "g")) ("∐"))
	673	((("\\" "a" "n" "g" "l" "e")) ("∠"))
	674	((("\\" "a" "p" "p" "r" "o" "x")) ("≈"))
	675	((("\\" "a" "p" "p" "r" "o" "x" "e" "q")) ("≊"))
	676	((("\\" "a" "s" "t")) ("∗"))
	677	((("\\" "a" "s" "y" "m" "p")) ("≍"))
	678	((("\\" "b" "a" "c" "k" "c" "o" "n" "g")) ("≌"))
	679	((("\\" "b" "a" "c" "k" "e" "p" "s" "i" "l" "o" "n")) ("∍"))
	680	((("\\" "b" "a" "c" "k" "p" "r" "i" "m" "e")) ("‵"))
	681	((("\\" "b" "a" "c" "k" "s" "i" "m")) ("∽"))
	682	((("\\" "b" "a" "c" "k" "s" "i" "m" "e" "q")) ("⋍"))
	683	((("\\" "b" "a" "c" "k" "s" "l" "a" "s" "h")) ("\\"))
	684	((("\\" "b" "a" "r" "w" "e" "d" "g" "e")) ("⊼"))
	685	((("\\" "b" "e" "c" "a" "u" "s" "e")) ("∵"))
	686	((("\\" "b" "e" "t" "a")) ("β"))
	687	((("\\" "b" "e" "t" "h")) ("ב"))
	688	((("\\" "b" "e" "t" "w" "e" "e" "n")) ("≬"))
	689	((("\\" "b" "i" "g" "c" "a" "p")) ("⋂"))
	690	((("\\" "b" "i" "g" "c" "i" "r" "c")) ("◯"))
	691	((("\\" "b" "i" "g" "c" "u" "p")) ("⋃"))
	692	((("\\" "b" "i" "g" "s" "t" "a" "r")) ("★"))
	693	((("\\" "b" "i" "g" "t" "r" "i" "a" "n" "g" "l" "e" "d" "o" "w" "n")) ("▽"))
	694	((("\\" "b" "i" "g" "t" "r" "i" "a" "n" "g" "l" "e" "u" "p")) ("△"))
	695	((("\\" "b" "i" "g" "v" "e" "e")) ("⋁"))
	696	((("\\" "b" "i" "g" "w" "e" "d" "g" "e")) ("⋀"))
	697	((("\\" "b" "l" "a" "c" "k" "l" "o" "z" "e" "n" "g" "e")) ("✦"))
	698	((("\\" "b" "l" "a" "c" "k" "s" "q" "u" "a" "r" "e")) ("▪"))
	699	((("\\" "b" "l" "a" "c" "k" "t" "r" "i" "a" "n" "g" "l" "e")) ("▴"))
	700	((("\\" "b" "l" "a" "c" "k" "t" "r" "i" "a" "n" "g" "l" "e" "d" "o" "w" "n")) ("▾"))
	701	((("\\" "b" "l" "a" "c" "k" "t" "r" "i" "a" "n" "g" "l" "e" "l" "e" "f" "t")) ("◂"))
	702	((("\\" "b" "l" "a" "c" "k" "t" "r" "i" "a" "n" "g" "l" "e" "r" "i" "g" "h" "t")) ("▸"))
	703	((("\\" "b" "o" "t")) ("⊥"))
	704	((("\\" "b" "o" "w" "t" "i" "e")) ("⋈"))
	705	((("\\" "b" "o" "x" "m" "i" "n" "u" "s")) ("⊟"))
	706	((("\\" "b" "o" "x" "p" "l" "u" "s")) ("⊞"))
	707	((("\\" "b" "o" "x" "t" "i" "m" "e" "s")) ("⊠"))
	708	((("\\" "b" "u" "l" "l" "e" "t")) ("•"))
	709	((("\\" "b" "u" "m" "p" "e" "q")) ("≏"))
	710	((("\\" "c" "a" "p")) ("∩"))
	711	((("\\" "c" "d" "o" "t" "s")) ("⋯"))
	712	((("\\" "c" "e" "n" "t" "e" "r" "d" "o" "t")) ("·"))
	713	((("\\" "c" "h" "e" "c" "k" "m" "a" "r" "k")) ("✓"))
	714	((("\\" "c" "h" "i")) ("χ"))
	715	((("\\" "c" "i" "r" "c")) ("○"))
	716	((("\\" "c" "i" "r" "c" "e" "q")) ("≗"))
	717	((("\\" "c" "i" "r" "c" "l" "e" "a" "r" "r" "o" "w" "l" "e" "f" "t")) ("↺"))
	718	((("\\" "c" "i" "r" "c" "l" "e" "a" "r" "r" "o" "w" "r" "i" "g" "h" "t")) ("↻"))
	719	((("\\" "c" "i" "r" "c" "l" "e" "d" "R")) ("®"))
	720	((("\\" "c" "i" "r" "c" "l" "e" "d" "S")) ("Ⓢ"))
	721	((("\\" "c" "i" "r" "c" "l" "e" "d" "a" "s" "t")) ("⊛"))
	722	((("\\" "c" "i" "r" "c" "l" "e" "d" "c" "i" "r" "c")) ("⊚"))
	723	((("\\" "c" "i" "r" "c" "l" "e" "d" "d" "a" "s" "h")) ("⊝"))
	724	((("\\" "c" "l" "u" "b" "s" "u" "i" "t")) ("♣"))
	725	((("\\" "c" "o" "l" "o" "n")) (":"))
	726	((("\\" "c" "o" "l" "o" "n" "e" "q")) ("≔"))
	727	((("\\" "c" "o" "m" "p" "l" "e" "m" "e" "n" "t")) ("∁"))
	728	((("\\" "c" "o" "n" "g")) ("≅"))
	729	((("\\" "c" "o" "p" "r" "o" "d")) ("∐"))
	730	((("\\" "c" "u" "p")) ("∪"))
	731	((("\\" "c" "u" "r" "l" "y" "e" "q" "p" "r" "e" "c")) ("⋞"))
	732	((("\\" "c" "u" "r" "l" "y" "e" "q" "s" "u" "c" "c")) ("⋟"))
	733	((("\\" "c" "u" "r" "l" "y" "p" "r" "e" "c" "e" "q")) ("≼"))
	734	((("\\" "c" "u" "r" "l" "y" "v" "e" "e")) ("⋎"))
	735	((("\\" "c" "u" "r" "l" "y" "w" "e" "d" "g" "e")) ("⋏"))
	736	((("\\" "c" "u" "r" "v" "e" "a" "r" "r" "o" "w" "l" "e" "f" "t")) ("↶"))
	737	((("\\" "c" "u" "r" "v" "e" "a" "r" "r" "o" "w" "r" "i" "g" "h" "t")) ("↷"))
	738	((("\\" "d" "a" "g")) ("†"))
	739	((("\\" "d" "a" "g" "g" "e" "r")) ("†"))
	740	((("\\" "d" "a" "l" "e" "t" "h")) ("ד"))
	741	((("\\" "d" "a" "s" "h" "v")) ("⊣"))
	742	((("\\" "d" "d" "a" "g")) ("‡"))
	743	((("\\" "d" "d" "a" "g" "g" "e" "r")) ("‡"))
	744	((("\\" "d" "d" "o" "t" "s")) ("⋱"))
	745	((("\\" "d" "e" "l" "t" "a")) ("δ"))
	746	((("\\" "d" "i" "a" "m" "o" "n" "d")) ("⋄"))
	747	((("\\" "d" "i" "a" "m" "o" "n" "d" "s" "u" "i" "t")) ("♢"))
	748	((("\\" "d" "i" "g" "a" "m" "m" "a")) ("Ϝ"))
	749	((("\\" "d" "i" "v" "i" "d" "e" "o" "n" "t" "i" "m" "e" "s")) ("⋇"))
	750	((("\\" "d" "o" "t" "e" "q")) ("≐"))
	751	((("\\" "d" "o" "t" "e" "q" "d" "o" "t")) ("≑"))
	752	((("\\" "d" "o" "t" "p" "l" "u" "s")) ("∔"))
	753	((("\\" "d" "o" "t" "s" "q" "u" "a" "r" "e")) ("⊡"))
	754	((("\\" "d" "o" "w" "n" "a" "r" "r" "o" "w")) ("↓"))
	755	((("\\" "d" "o" "w" "n" "d" "o" "w" "n" "a" "r" "r" "o" "w" "s")) ("⇊"))
	756	((("\\" "d" "o" "w" "n" "l" "e" "f" "t" "h" "a" "r" "p" "o" "o" "n")) ("⇃"))
	757	((("\\" "d" "o" "w" "n" "r" "i" "g" "h" "t" "h" "a" "r" "p" "o" "o" "n")) ("⇂"))
	758	((("\\" "e" "l" "l")) ("ℓ"))
	759	((("\\" "e" "m" "p" "t" "y" "s" "e" "t")) ("∅"))
	760	((("\\" "e" "p" "s" "i" "l" "o" "n")) ("ε"))
	761	((("\\" "e" "q" "c" "i" "r" "c")) ("≖"))
	762	((("\\" "e" "q" "c" "o" "l" "o" "n")) ("≕"))
	763	((("\\" "e" "q" "s" "l" "a" "n" "t" "g" "t" "r")) ("⋝"))
	764	((("\\" "e" "q" "s" "l" "a" "n" "t" "l" "e" "s" "s")) ("⋜"))
	765	((("\\" "e" "q" "u" "i" "v")) ("≡"))
	766	((("\\" "e" "t" "a")) ("η"))
	767	((("\\" "e" "u" "r" "o")) ("€"))
	768	((("\\" "e" "x" "i" "s" "t" "s")) ("∃"))
	769	((("\\" "f" "a" "l" "l" "i" "n" "g" "d" "o" "t" "s" "e" "q")) ("≒"))
	770	((("\\" "f" "l" "a" "t")) ("♭"))
	771	((("\\" "f" "o" "r" "a" "l" "l")) ("∀"))
	772	((("\\" "f" "r" "a" "c" "1")) ("⅟"))
	773	((("\\" "f" "r" "a" "c" "1" "2")) ("½"))
	774	((("\\" "f" "r" "a" "c" "1" "3")) ("⅓"))
	775	((("\\" "f" "r" "a" "c" "1" "4")) ("¼"))
	776	((("\\" "f" "r" "a" "c" "1" "5")) ("⅕"))
	777	((("\\" "f" "r" "a" "c" "1" "6")) ("⅙"))
	778	((("\\" "f" "r" "a" "c" "1" "8")) ("⅛"))
	779	((("\\" "f" "r" "a" "c" "2" "3")) ("⅔"))
	780	((("\\" "f" "r" "a" "c" "2" "5")) ("⅖"))
	781	((("\\" "f" "r" "a" "c" "3" "4")) ("¾"))
	782	((("\\" "f" "r" "a" "c" "3" "5")) ("⅗"))
	783	((("\\" "f" "r" "a" "c" "3" "8")) ("⅜"))
	784	((("\\" "f" "r" "a" "c" "4" "5")) ("⅘"))
	785	((("\\" "f" "r" "a" "c" "5" "6")) ("⅚"))
	786	((("\\" "f" "r" "a" "c" "5" "8")) ("⅝"))
	787	((("\\" "f" "r" "a" "c" "7" "8")) ("⅞"))
	788	((("\\" "f" "r" "o" "w" "n")) ("⌢"))
	789	((("\\" "g" "a" "m" "m" "a")) ("γ"))
	790	((("\\" "g" "e")) ("≥"))
	791	((("\\" "g" "e" "q")) ("≥"))
	792	((("\\" "g" "e" "q" "q")) ("≧"))
	793	((("\\" "g" "e" "q" "s" "l" "a" "n" "t")) ("≥"))
	794	((("\\" "g" "e" "t" "s")) ("←"))
	795	((("\\" "g" "g")) ("≫"))
	796	((("\\" "g" "g" "g")) ("⋙"))
	797	((("\\" "g" "i" "m" "e" "l")) ("ג"))
	798	((("\\" "g" "n" "a" "p" "p" "r" "o" "x")) ("⋧"))
	799	((("\\" "g" "n" "e" "q")) ("≩"))
	800	((("\\" "g" "n" "e" "q" "q")) ("≩"))
	801	((("\\" "g" "n" "s" "i" "m")) ("⋧"))
	802	((("\\" "g" "t" "r" "a" "p" "p" "r" "o" "x")) ("≳"))
	803	((("\\" "g" "t" "r" "d" "o" "t")) ("⋗"))
	804	((("\\" "g" "t" "r" "e" "q" "l" "e" "s" "s")) ("⋛"))
	805	((("\\" "g" "t" "r" "e" "q" "q" "l" "e" "s" "s")) ("⋛"))
	806	((("\\" "g" "t" "r" "l" "e" "s" "s")) ("≷"))
	807	((("\\" "g" "t" "r" "s" "i" "m")) ("≳"))
	808	((("\\" "g" "v" "e" "r" "t" "n" "e" "q" "q")) ("≩"))
	809	((("\\" "h" "b" "a" "r")) ("ℏ"))
	810	((("\\" "h" "e" "a" "r" "t" "s" "u" "i" "t")) ("♥"))
	811	((("\\" "h" "o" "o" "k" "l" "e" "f" "t" "a" "r" "r" "o" "w")) ("↩"))
	812	((("\\" "h" "o" "o" "k" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("↪"))
	813	((("\\" "i" "f" "f")) ("⇔"))
	814	((("\\" "i" "m" "a" "t" "h")) ("ı"))
	815	((("\\" "i" "n")) ("∈"))
	816	((("\\" "i" "n" "f" "t" "y")) ("∞"))
	817	((("\\" "i" "n" "t")) ("∫"))
	818	((("\\" "i" "n" "t" "e" "r" "c" "a" "l")) ("⊺"))
	819	((("\\" "i" "o" "t" "a")) ("ι"))
	820	((("\\" "k" "a" "p" "p" "a")) ("κ"))
	821	((("\\" "l" "a" "m" "b" "d" "a")) ("λ"))
	822	((("\\" "l" "a" "n" "g" "l" "e")) ("〈"))
	823	((("\\" "l" "b" "r" "a" "c" "e")) ("{"))
	824	((("\\" "l" "b" "r" "a" "c" "k")) ("["))
	825	((("\\" "l" "c" "e" "i" "l")) ("⌈"))
	826	((("\\" "l" "d" "o" "t" "s")) ("…"))
	827	((("\\" "l" "e")) ("≤"))
	828	((("\\" "l" "e" "a" "d" "s" "t" "o")) ("↝"))
	829	((("\\" "l" "e" "f" "t" "a" "r" "r" "o" "w")) ("←"))
	830	((("\\" "l" "e" "f" "t" "a" "r" "r" "o" "w" "t" "a" "i" "l")) ("↢"))
	831	((("\\" "l" "e" "f" "t" "h" "a" "r" "p" "o" "o" "n" "d" "o" "w" "n")) ("↽"))
	832	((("\\" "l" "e" "f" "t" "h" "a" "r" "p" "o" "o" "n" "u" "p")) ("↼"))
	833	((("\\" "l" "e" "f" "t" "l" "e" "f" "t" "a" "r" "r" "o" "w" "s")) ("⇇"))
	834	((("\\" "l" "e" "f" "t" "p" "a" "r" "e" "n" "g" "t" "r")) ("〈"))
	835	((("\\" "l" "e" "f" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("↔"))
	836	((("\\" "l" "e" "f" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w" "s")) ("⇆"))
	837	((("\\" "l" "e" "f" "t" "r" "i" "g" "h" "t" "h" "a" "r" "p" "o" "o" "n" "s")) ("⇋"))
	838	((("\\" "l" "e" "f" "t" "r" "i" "g" "h" "t" "s" "q" "u" "i" "g" "a" "r" "r" "o" "w")) ("↭"))
	839	((("\\" "l" "e" "f" "t" "t" "h" "r" "e" "e" "t" "i" "m" "e" "s")) ("⋋"))
	840	((("\\" "l" "e" "q")) ("≤"))
	841	((("\\" "l" "e" "q" "q")) ("≦"))
	842	((("\\" "l" "e" "q" "s" "l" "a" "n" "t")) ("≤"))
	843	((("\\" "l" "e" "s" "s" "a" "p" "p" "r" "o" "x")) ("≲"))
	844	((("\\" "l" "e" "s" "s" "d" "o" "t")) ("⋖"))
	845	((("\\" "l" "e" "s" "s" "e" "q" "g" "t" "r")) ("⋚"))
	846	((("\\" "l" "e" "s" "s" "e" "q" "q" "g" "t" "r")) ("⋚"))
	847	((("\\" "l" "e" "s" "s" "g" "t" "r")) ("≶"))
	848	((("\\" "l" "e" "s" "s" "s" "i" "m")) ("≲"))
	849	((("\\" "l" "f" "l" "o" "o" "r")) ("⌊"))
	850	((("\\" "l" "h" "d")) ("◁"))
	851	((("\\" "r" "h" "d")) ("▷"))
	852	((("\\" "l" "l")) ("≪"))
	853	((("\\" "l" "l" "c" "o" "r" "n" "e" "r")) ("⌞"))
	854	((("\\" "l" "n" "a" "p" "p" "r" "o" "x")) ("⋦"))
	855	((("\\" "l" "n" "e" "q")) ("≨"))
	856	((("\\" "l" "n" "e" "q" "q")) ("≨"))
	857	((("\\" "l" "n" "s" "i" "m")) ("⋦"))
	858	((("\\" "l" "o" "n" "g" "l" "e" "f" "t" "a" "r" "r" "o" "w")) ("←"))
	859	((("\\" "l" "o" "n" "g" "l" "e" "f" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("↔"))
	860	((("\\" "l" "o" "n" "g" "m" "a" "p" "s" "t" "o")) ("↦"))
	861	((("\\" "l" "o" "n" "g" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("→"))
	862	((("\\" "l" "o" "o" "p" "a" "r" "r" "o" "w" "l" "e" "f" "t")) ("↫"))
	863	((("\\" "l" "o" "o" "p" "a" "r" "r" "o" "w" "r" "i" "g" "h" "t")) ("↬"))
	864	((("\\" "l" "o" "z" "e" "n" "g" "e")) ("✧"))
	865	((("\\" "l" "q")) ("‘"))
	866	((("\\" "l" "r" "c" "o" "r" "n" "e" "r")) ("⌟"))
	867	((("\\" "l" "t" "i" "m" "e" "s")) ("⋉"))
	868	((("\\" "l" "v" "e" "r" "t" "n" "e" "q" "q")) ("≨"))
	869	((("\\" "m" "a" "l" "t" "e" "s" "e")) ("✠"))
	870	((("\\" "m" "a" "p" "s" "t" "o")) ("↦"))
	871	((("\\" "m" "e" "a" "s" "u" "r" "e" "d" "a" "n" "g" "l" "e")) ("∡"))
	872	((("\\" "m" "h" "o")) ("℧"))
	873	((("\\" "m" "i" "d")) ("∣"))
	874	((("\\" "m" "o" "d" "e" "l" "s")) ("⊧"))
	875	((("\\" "m" "p")) ("∓"))
	876	((("\\" "m" "u" "l" "t" "i" "m" "a" "p")) ("⊸"))
	877	((("\\" "n" "L" "e" "f" "t" "a" "r" "r" "o" "w")) ("⇍"))
	878	((("\\" "n" "L" "e" "f" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("⇎"))
	879	((("\\" "n" "R" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("⇏"))
	880	((("\\" "n" "V" "D" "a" "s" "h")) ("⊯"))
	881	((("\\" "n" "V" "d" "a" "s" "h")) ("⊮"))
	882	((("\\" "n" "a" "b" "l" "a")) ("∇"))
	883	((("\\" "n" "a" "p" "p" "r" "o" "x")) ("≉"))
	884	((("\\" "n" "a" "t" "u" "r" "a" "l")) ("♮"))
	885	((("\\" "n" "c" "o" "n" "g")) ("≇"))
	886	((("\\" "n" "e")) ("≠"))
	887	((("\\" "n" "e" "a" "r" "r" "o" "w")) ("↗"))
	888	((("\\" "n" "e" "g")) ("¬"))
	889	((("\\" "n" "e" "q")) ("≠"))
	890	((("\\" "n" "e" "q" "u" "i" "v")) ("≢"))
	891	((("\\" "n" "e" "w" "l" "i" "n" "e")) (" "))
	892	((("\\" "n" "e" "x" "i" "s" "t" "s")) ("∄"))
	893	((("\\" "n" "g" "e" "q")) ("≱"))
	894	((("\\" "n" "g" "e" "q" "q")) ("≱"))
	895	((("\\" "n" "g" "e" "q" "s" "l" "a" "n" "t")) ("≱"))
	896	((("\\" "n" "g" "t" "r")) ("≯"))
	897	((("\\" "n" "i")) ("∋"))
	898	((("\\" "n" "l" "e" "f" "t" "a" "r" "r" "o" "w")) ("↚"))
	899	((("\\" "n" "l" "e" "f" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("↮"))
	900	((("\\" "n" "l" "e" "q")) ("≰"))
	901	((("\\" "n" "l" "e" "q" "q")) ("≰"))
	902	((("\\" "n" "l" "e" "q" "s" "l" "a" "n" "t")) ("≰"))
	903	((("\\" "n" "l" "e" "s" "s")) ("≮"))
	904	((("\\" "n" "m" "i" "d")) ("∤"))
	905	((("\\" "n" "o" "t")) ("̸"))
	906	((("\\" "n" "o" "t" "i" "n")) ("∉"))
	907	((("\\" "n" "p" "a" "r" "a" "l" "l" "e" "l")) ("∦"))
	908	((("\\" "n" "p" "r" "e" "c")) ("⊀"))
	909	((("\\" "n" "p" "r" "e" "c" "e" "q")) ("⋠"))
	910	((("\\" "n" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("↛"))
	911	((("\\" "n" "s" "h" "o" "r" "t" "m" "i" "d")) ("∤"))
	912	((("\\" "n" "s" "h" "o" "r" "t" "p" "a" "r" "a" "l" "l" "e" "l")) ("∦"))
	913	((("\\" "n" "s" "i" "m")) ("≁"))
	914	((("\\" "n" "s" "i" "m" "e" "q")) ("≄"))
	915	((("\\" "n" "s" "u" "b" "s" "e" "t")) ("⊄"))
	916	((("\\" "n" "s" "u" "b" "s" "e" "t" "e" "q")) ("⊈"))
	917	((("\\" "n" "s" "u" "b" "s" "e" "t" "e" "q" "q")) ("⊈"))
	918	((("\\" "n" "s" "u" "c" "c")) ("⊁"))
	919	((("\\" "n" "s" "u" "c" "c" "e" "q")) ("⋡"))
	920	((("\\" "n" "s" "u" "p" "s" "e" "t")) ("⊅"))
	921	((("\\" "n" "s" "u" "p" "s" "e" "t" "e" "q")) ("⊉"))
	922	((("\\" "n" "s" "u" "p" "s" "e" "t" "e" "q" "q")) ("⊉"))
	923	((("\\" "n" "t" "r" "i" "a" "n" "g" "l" "e" "l" "e" "f" "t")) ("⋪"))
	924	((("\\" "n" "t" "r" "i" "a" "n" "g" "l" "e" "l" "e" "f" "t" "e" "q")) ("⋬"))
	925	((("\\" "n" "t" "r" "i" "a" "n" "g" "l" "e" "r" "i" "g" "h" "t")) ("⋫"))
	926	((("\\" "n" "t" "r" "i" "a" "n" "g" "l" "e" "r" "i" "g" "h" "t" "e" "q")) ("⋭"))
	927	((("\\" "n" "u")) ("ν"))
	928	((("\\" "n" "v" "D" "a" "s" "h")) ("⊭"))
	929	((("\\" "n" "v" "d" "a" "s" "h")) ("⊬"))
	930	((("\\" "n" "w" "a" "r" "r" "o" "w")) ("↖"))
	931	((("\\" "o" "d" "o" "t")) ("⊙"))
	932	((("\\" "o" "i" "n" "t")) ("∮"))
	933	((("\\" "o" "m" "e" "g" "a")) ("ω"))
	934	((("\\" "o" "m" "i" "n" "u" "s")) ("⊖"))
	935	((("\\" "o" "p" "l" "u" "s")) ("⊕"))
	936	((("\\" "o" "s" "l" "a" "s" "h")) ("⊘"))
	937	((("\\" "o" "t" "i" "m" "e" "s")) ("⊗"))
	938	((("\\" "p" "a" "r")) (" "))
	939	((("\\" "p" "a" "r" "a" "l" "l" "e" "l")) ("∥"))
	940	((("\\" "p" "a" "r" "t" "i" "a" "l")) ("∂"))
	941	((("\\" "p" "e" "r" "p")) ("⊥"))
	942	((("\\" "p" "h" "i")) ("φ"))
	943	((("\\" "p" "i")) ("π"))
	944	((("\\" "p" "i" "t" "c" "h" "f" "o" "r" "k")) ("⋔"))
	945	((("\\" "p" "r" "e" "c")) ("≺"))
	946	((("\\" "p" "r" "e" "c" "a" "p" "p" "r" "o" "x")) ("≾"))
	947	((("\\" "p" "r" "e" "c" "e" "q")) ("≼"))
	948	((("\\" "p" "r" "e" "c" "n" "a" "p" "p" "r" "o" "x")) ("⋨"))
	949	((("\\" "p" "r" "e" "c" "n" "s" "i" "m")) ("⋨"))
	950	((("\\" "p" "r" "e" "c" "s" "i" "m")) ("≾"))
	951	((("\\" "p" "r" "i" "m" "e")) ("′"))
	952	((("\\" "p" "r" "o" "d")) ("∏"))
	953	((("\\" "p" "r" "o" "p" "t" "o")) ("∝"))
	954	((("\\" "p" "s" "i")) ("ψ"))
	955	((("\\" "q" "e" "d")) ("∎"))
	956	((("\\" "q" "u" "a" "d")) (" "))
	957	((("\\" "r" "a" "n" "g" "l" "e")) ("〉"))
	958	((("\\" "r" "b" "r" "a" "c" "e")) ("}"))
	959	((("\\" "r" "b" "r" "a" "c" "k")) ("]"))
	960	((("\\" "r" "c" "e" "i" "l")) ("⌉"))
	961	((("\\" "r" "f" "l" "o" "o" "r")) ("⌋"))
	962	((("\\" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("→"))
	963	((("\\" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w" "t" "a" "i" "l")) ("↣"))
	964	((("\\" "r" "i" "g" "h" "t" "h" "a" "r" "p" "o" "o" "n" "d" "o" "w" "n")) ("⇁"))
	965	((("\\" "r" "i" "g" "h" "t" "h" "a" "r" "p" "o" "o" "n" "u" "p")) ("⇀"))
	966	((("\\" "r" "i" "g" "h" "t" "l" "e" "f" "t" "a" "r" "r" "o" "w" "s")) ("⇄"))
	967	((("\\" "r" "i" "g" "h" "t" "l" "e" "f" "t" "h" "a" "r" "p" "o" "o" "n" "s")) ("⇌"))
	968	((("\\" "r" "i" "g" "h" "t" "p" "a" "r" "e" "n" "g" "t" "r")) ("〉"))
	969	((("\\" "r" "i" "g" "h" "t" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w" "s")) ("⇉"))
	970	((("\\" "r" "i" "g" "h" "t" "t" "h" "r" "e" "e" "t" "i" "m" "e" "s")) ("⋌"))
	971	((("\\" "r" "i" "s" "i" "n" "g" "d" "o" "t" "s" "e" "q")) ("≓"))
	972	((("\\" "r" "t" "i" "m" "e" "s")) ("⋊"))
	973	((("\\" "s" "b" "s")) ("﹨"))
	974	((("\\" "s" "e" "a" "r" "r" "o" "w")) ("↘"))
	975	((("\\" "s" "e" "t" "m" "i" "n" "u" "s")) ("∖"))
	976	((("\\" "s" "h" "a" "r" "p")) ("♯"))
	977	((("\\" "s" "h" "o" "r" "t" "m" "i" "d")) ("∣"))
	978	((("\\" "s" "h" "o" "r" "t" "p" "a" "r" "a" "l" "l" "e" "l")) ("∥"))
	979	((("\\" "s" "i" "g" "m" "a")) ("σ"))
	980	((("\\" "s" "i" "m")) ("∼"))
	981	((("\\" "s" "i" "m" "e" "q")) ("≃"))
	982	((("\\" "s" "m" "a" "l" "l" "a" "m" "a" "l" "g")) ("∐"))
	983	((("\\" "s" "m" "a" "l" "l" "s" "e" "t" "m" "i" "n" "u" "s")) ("∖"))
	984	((("\\" "s" "m" "a" "l" "l" "s" "m" "i" "l" "e")) ("⌣"))
	985	((("\\" "s" "m" "i" "l" "e")) ("⌣"))
	986	((("\\" "s" "p" "a" "d" "e" "s" "u" "i" "t")) ("♠"))
	987	((("\\" "s" "p" "h" "e" "r" "i" "c" "a" "l" "a" "n" "g" "l" "e")) ("∢"))
	988	((("\\" "s" "q" "c" "a" "p")) ("⊓"))
	989	((("\\" "s" "q" "c" "u" "p")) ("⊔"))
	990	((("\\" "s" "q" "s" "u" "b" "s" "e" "t")) ("⊏"))
	991	((("\\" "s" "q" "s" "u" "b" "s" "e" "t" "e" "q")) ("⊑"))
	992	((("\\" "s" "q" "s" "u" "p" "s" "e" "t")) ("⊐"))
	993	((("\\" "s" "q" "s" "u" "p" "s" "e" "t" "e" "q")) ("⊒"))
	994	((("\\" "s" "q" "u" "a" "r" "e")) ("□"))
	995	((("\\" "s" "q" "u" "i" "g" "a" "r" "r" "o" "w" "r" "i" "g" "h" "t")) ("⇝"))
	996	((("\\" "s" "t" "a" "r")) ("⋆"))
	997	((("\\" "s" "t" "r" "a" "i" "g" "h" "t" "p" "h" "i")) ("φ"))
	998	((("\\" "s" "u" "b" "s" "e" "t")) ("⊂"))
	999	((("\\" "s" "u" "b" "s" "e" "t" "e" "q")) ("⊆"))
	1000	((("\\" "s" "u" "b" "s" "e" "t" "e" "q" "q")) ("⊆"))
	1001	((("\\" "s" "u" "b" "s" "e" "t" "n" "e" "q")) ("⊊"))
	1002	((("\\" "s" "u" "b" "s" "e" "t" "n" "e" "q" "q")) ("⊊"))
	1003	((("\\" "s" "u" "c" "c")) ("≻"))
	1004	((("\\" "s" "u" "c" "c" "a" "p" "p" "r" "o" "x")) ("≿"))
	1005	((("\\" "s" "u" "c" "c" "c" "u" "r" "l" "y" "e" "q")) ("≽"))
	1006	((("\\" "s" "u" "c" "c" "e" "q")) ("≽"))
	1007	((("\\" "s" "u" "c" "c" "n" "a" "p" "p" "r" "o" "x")) ("⋩"))
	1008	((("\\" "s" "u" "c" "c" "n" "s" "i" "m")) ("⋩"))
	1009	((("\\" "s" "u" "c" "c" "s" "i" "m")) ("≿"))
	1010	((("\\" "s" "u" "m")) ("∑"))
	1011	((("\\" "s" "u" "p" "s" "e" "t")) ("⊃"))
	1012	((("\\" "s" "u" "p" "s" "e" "t" "e" "q")) ("⊇"))
	1013	((("\\" "s" "u" "p" "s" "e" "t" "e" "q" "q")) ("⊇"))
	1014	((("\\" "s" "u" "p" "s" "e" "t" "n" "e" "q")) ("⊋"))
	1015	((("\\" "s" "u" "p" "s" "e" "t" "n" "e" "q" "q")) ("⊋"))
	1016	((("\\" "s" "u" "r" "d")) ("√"))
	1017	((("\\" "s" "w" "a" "r" "r" "o" "w")) ("↙"))
	1018	((("\\" "t" "a" "u")) ("τ"))
	1019	((("\\" "t" "h" "e" "r" "e" "f" "o" "r" "e")) ("∴"))
	1020	((("\\" "t" "h" "e" "t" "a")) ("θ"))
	1021	((("\\" "t" "h" "i" "c" "k" "a" "p" "p" "r" "o" "x")) ("≈"))
	1022	((("\\" "t" "h" "i" "c" "k" "s" "i" "m")) ("∼"))
	1023	((("\\" "t" "o")) ("→"))
	1024	((("\\" "t" "o" "p")) ("⊤"))
	1025	((("\\" "t" "r" "i" "a" "n" "g" "l" "e")) ("▵"))
	1026	((("\\" "t" "r" "i" "a" "n" "g" "l" "e" "d" "o" "w" "n")) ("▿"))
	1027	((("\\" "t" "r" "i" "a" "n" "g" "l" "e" "l" "e" "f" "t")) ("◃"))
	1028	((("\\" "t" "r" "i" "a" "n" "g" "l" "e" "l" "e" "f" "t" "e" "q")) ("⊴"))
	1029	((("\\" "t" "r" "i" "a" "n" "g" "l" "e" "q")) ("≜"))
	1030	((("\\" "t" "r" "i" "a" "n" "g" "l" "e" "r" "i" "g" "h" "t")) ("▹"))
	1031	((("\\" "t" "r" "i" "a" "n" "g" "l" "e" "r" "i" "g" "h" "t" "e" "q")) ("⊵"))
	1032	((("\\" "t" "w" "o" "h" "e" "a" "d" "l" "e" "f" "t" "a" "r" "r" "o" "w")) ("↞"))
	1033	((("\\" "t" "w" "o" "h" "e" "a" "d" "r" "i" "g" "h" "t" "a" "r" "r" "o" "w")) ("↠"))
	1034	((("\\" "u" "l" "c" "o" "r" "n" "e" "r")) ("⌜"))
	1035	((("\\" "u" "p" "a" "r" "r" "o" "w")) ("↑"))
	1036	((("\\" "u" "p" "d" "o" "w" "n" "a" "r" "r" "o" "w")) ("↕"))
	1037	((("\\" "u" "p" "l" "e" "f" "t" "h" "a" "r" "p" "o" "o" "n")) ("↿"))
	1038	((("\\" "u" "p" "l" "u" "s")) ("⊎"))
	1039	((("\\" "u" "p" "r" "i" "g" "h" "t" "h" "a" "r" "p" "o" "o" "n")) ("↾"))
	1040	((("\\" "u" "p" "s" "i" "l" "o" "n")) ("υ"))
	1041	((("\\" "u" "p" "u" "p" "a" "r" "r" "o" "w" "s")) ("⇈"))
	1042	((("\\" "u" "r" "c" "o" "r" "n" "e" "r")) ("⌝"))
	1043	((("\\" "u" "{" "i" "}")) ("ĭ"))
	1044	((("\\" "v" "D" "a" "s" "h")) ("⊨"))
	1045	((("\\" "v" "a" "r" "k" "a" "p" "p" "a")) ("ϰ"))
	1046	((("\\" "v" "a" "r" "p" "h" "i")) ("ϕ"))
	1047	((("\\" "v" "a" "r" "p" "i")) ("ϖ"))
	1048	((("\\" "v" "a" "r" "p" "r" "i" "m" "e")) ("′"))
	1049	((("\\" "v" "a" "r" "p" "r" "o" "p" "t" "o")) ("∝"))
	1050	((("\\" "v" "a" "r" "r" "h" "o")) ("ϱ"))
	1051	((("\\" "v" "a" "r" "s" "i" "g" "m" "a")) ("ς"))
	1052	((("\\" "v" "a" "r" "t" "h" "e" "t" "a")) ("ϑ"))
	1053	((("\\" "v" "a" "r" "t" "r" "i" "a" "n" "g" "l" "e" "l" "e" "f" "t")) ("⊲"))
	1054	((("\\" "v" "a" "r" "t" "r" "i" "a" "n" "g" "l" "e" "r" "i" "g" "h" "t")) ("⊳"))
	1055	((("\\" "v" "d" "a" "s" "h")) ("⊢"))
	1056	((("\\" "v" "d" "o" "t" "s")) ("⋮"))
	1057	((("\\" "v" "e" "e")) ("∨"))
	1058	((("\\" "v" "e" "e" "b" "a" "r")) ("⊻"))
	1059	((("\\" "v" "e" "r" "t")) ("\|"))
	1060	((("\\" "w" "e" "d" "g" "e")) ("∧"))
	1061	((("\\" "w" "p")) ("℘"))
	1062	((("\\" "w" "r")) ("≀"))
	1063	((("\\" "x" "i")) ("ξ"))
	1064	((("\\" "z" "e" "t" "a")) ("ζ"))
	1065	((("\\" "B" "b" "b" "{" "N" "}")) ("ℕ"))
	1066	((("\\" "B" "b" "b" "{" "P" "}")) ("ℙ"))
	1067	((("\\" "B" "b" "b" "{" "R" "}")) ("ℝ"))
	1068	((("\\" "B" "b" "b" "{" "Z" "}")) ("ℤ"))
	1069	((("-" "-")) ("–"))
	1070	((("-" "-" "-")) ("—"))
	1071	((("\\" " ")) (" "))
	1072	((("\\" "\\")) ("\\"))
	1073	((("\\" "m" "u")) ("μ"))
	1074	((("\\" "r" "h" "o")) ("ρ"))
	1075	((("\\" "m" "a" "t" "h" "s" "c" "r" "{" "I" "}")) ("ℐ"))
	1076	((("\\" "S" "m" "i" "l" "e" "y")) ("☺"))
	1077	((("\\" "b" "l" "a" "c" "k" "s" "m" "i" "l" "e" "y")) ("☻"))
	1078	((("\\" "F" "r" "o" "w" "n" "y")) ("☹"))
	1079	((("\\" "L" "e" "t" "t" "e" "r")) ("✉"))
	1080	((("\\" "p" "e" "r" "m" "i" "l")) ("‰"))
	1081	((("\\" "r" "e" "g" "i" "s" "t" "e" "r" "e" "d")) ("®"))
	1082	((("\\" "c" "u" "r" "r" "e" "n" "c" "y")) ("¤"))
	1083	((("\\" "d" "h")) ("ð"))
	1084	((("\\" "D" "H")) ("Ð"))
	1085	((("\\" "t" "h")) ("þ"))
	1086	((("\\" "T" "H")) ("Þ"))
	1087	((("\\" "m" "i" "c" "r" "o")) ("µ"))
	1088	((("\\" "l" "n" "o" "t")) ("¬"))
	1089	((("\\" "o" "r" "d" "f" "e" "m" "i" "n" "i" "n" "e")) ("ª"))
	1090	((("\\" "o" "r" "d" "m" "a" "s" "c" "u" "l" "i" "n" "e")) ("º"))
	1091	((("\\" "l" "a" "m" "b" "d" "a" "b" "a" "r")) ("ƛ"))
	1092	((("\\" "c" "e" "l" "s" "i" "u" "s")) ("℃"))
	1093	((("\\" "l" "d" "q")) ("“"))
	1094	((("\\" "r" "d" "q")) ("”"))
	1095	((("\\" "m" "i" "n" "u" "s")) ("−"))
	1096	((("\\" "d" "e" "f" "s")) ("≙"))
	1097	((("\\" "l" "l" "b" "r" "a" "c" "k" "e" "t")) ("〚"))
	1098	((("\\" "r" "r" "b" "r" "a" "c" "k" "e" "t")) ("〛"))
	1099	((("\\" "l" "d" "a" "t" "a")) ("《"))
	1100	((("\\" "r" "d" "a" "t" "a")) ("》"))
	1101	((("\\" "g" "l" "q")) ("‚"))
	1102	((("\\" "g" "r" "q")) ("‘"))
	1103	((("\\" "g" "l" "q" "q")) ("„"))
	1104	((("\\" "\"" "`")) ("„"))
	1105	((("\\" "g" "r" "q" "q")) ("“"))
	1106	((("\\" "\"" "'")) ("“"))
	1107	((("\\" "f" "l" "q")) ("‹"))
	1108	((("\\" "f" "r" "q")) ("›"))
	1109	((("\\" "f" "l" "q" "q")) ("«"))
	1110	((("\\" "\"" "<")) ("«"))
	1111	((("\\" "f" "r" "q" "q")) ("»"))
	1112	((("\\" "\"" ">")) ("»"))
	1113	((("\\" "-")) (""))
	1114	((("\\" "t" "e" "x" "t" "m" "u")) ("µ"))
	1115	((("\\" "t" "e" "x" "t" "f" "r" "a" "c" "t" "i" "o" "n" "s" "o" "l" "i" "d" "u" "s")) ("⁄"))
	1116	((("\\" "t" "e" "x" "t" "b" "i" "g" "c" "i" "r" "c" "l" "e")) ("⃝"))
	1117	((("\\" "t" "e" "x" "t" "m" "u" "s" "i" "c" "a" "l" "n" "o" "t" "e")) ("♪"))
	1118	((("\\" "t" "e" "x" "t" "d" "i" "e" "d")) ("✝"))
	1119	((("\\" "t" "e" "x" "t" "c" "o" "l" "o" "n" "m" "o" "n" "e" "t" "a" "r" "y")) ("₡"))
	1120	((("\\" "t" "e" "x" "t" "w" "o" "n")) ("₩"))
	1121	((("\\" "t" "e" "x" "t" "n" "a" "i" "r" "a")) ("₦"))
	1122	((("\\" "t" "e" "x" "t" "p" "e" "s" "o")) ("₱"))
	1123	((("\\" "t" "e" "x" "t" "l" "i" "r" "a")) ("₤"))
	1124	((("\\" "t" "e" "x" "t" "r" "e" "c" "i" "p" "e")) ("℞"))
	1125	((("\\" "t" "e" "x" "t" "i" "n" "t" "e" "r" "r" "o" "b" "a" "n" "g")) ("‽"))
	1126	((("\\" "t" "e" "x" "t" "p" "e" "r" "t" "e" "n" "t" "h" "o" "u" "s" "a" "n" "d")) ("‱"))
	1127	((("\\" "t" "e" "x" "t" "b" "a" "h" "t")) ("฿"))
	1128	((("\\" "t" "e" "x" "t" "n" "u" "m" "e" "r" "o")) ("№"))
	1129	((("\\" "t" "e" "x" "t" "d" "i" "s" "c" "o" "u" "n" "t")) ("⁒"))
	1130	((("\\" "t" "e" "x" "t" "e" "s" "t" "i" "m" "a" "t" "e" "d")) ("℮"))
	1131	((("\\" "t" "e" "x" "t" "o" "p" "e" "n" "b" "u" "l" "l" "e" "t")) ("◦"))
	1132	((("\\" "t" "e" "x" "t" "l" "q" "u" "i" "l" "l")) ("⁅"))
	1133	((("\\" "t" "e" "x" "t" "r" "q" "u" "i" "l" "l")) ("⁆"))
	1134	((("\\" "t" "e" "x" "t" "c" "i" "r" "c" "l" "e" "d" "P")) ("℗"))
	1135	((("\\" "t" "e" "x" "t" "r" "e" "f" "e" "r" "e" "n" "c" "e" "m" "a" "r" "k")) ("※"))
	1136	))
	1137
	1138	;; Local Variables:
	1139	;; mode: scheme
	1140	;; coding: utf-8
	1141	;; End:

+277

-0

ide/uim/coqide.scm less more

	0	;;; coqide.scm -- Emacs-style Latin characters translation
	1	;;;
	2	;;; Copyright (c) 2003-2009 uim Project http://code.google.com/p/uim/
	3	;;;
	4	;;; All rights reserved.
	5	;;;
	6	;;; Redistribution and use in source and binary forms, with or without
	7	;;; modification, are permitted provided that the following conditions
	8	;;; are met:
	9	;;; 1. Redistributions of source code must retain the above copyright
	10	;;; notice, this list of conditions and the following disclaimer.
	11	;;; 2. Redistributions in binary form must reproduce the above copyright
	12	;;; notice, this list of conditions and the following disclaimer in the
	13	;;; documentation and/or other materials provided with the distribution.
	14	;;; 3. Neither the name of authors nor the names of its contributors
	15	;;; may be used to endorse or promote products derived from this software
	16	;;; without specific prior written permission.
	17	;;;
	18	;;; THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS ``AS IS'' AND
	19	;;; ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
	20	;;; IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
	21	;;; ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS OR CONTRIBUTORS BE LIABLE
	22	;;; FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
	23	;;; DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
	24	;;; OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
	25	;;; HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
	26	;;; LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
	27	;;; OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
	28	;;; SUCH DAMAGE.
	29	;;;;
	30
	31	;; This input method implements character composition rules for the
	32	;; Latin letters used in European languages. The rules, defined in
	33	;; the file coqide-rules.scm, have been adapted from GNU Emacs 22.
	34
	35	(require "util.scm")
	36	(require "rk.scm")
	37	(require "coqide-rules.scm")
	38	(require-custom "generic-key-custom.scm")
	39	(require-custom "coqide-custom.scm")
	40
	41	(define coqide-context-rec-spec
	42	(append
	43	context-rec-spec
	44	'((on #f)
	45	(rkc #f)
	46	(show-cands #f))))
	47	(define-record 'coqide-context coqide-context-rec-spec)
	48	(define coqide-context-new-internal coqide-context-new)
	49
	50	(define (coqide-context-new id im)
	51	(let ((lc (coqide-context-new-internal id im))
	52	(rkc (rk-context-new (symbol-value coqide-rules) #f #f)))
	53	(coqide-context-set-widgets! lc coqide-widgets)
	54	(coqide-context-set-rkc! lc rkc)
	55	lc))
	56
	57	(define (coqide-current-translation lc)
	58	(let ((rkc (coqide-context-rkc lc)))
	59	(or (rk-peek-terminal-match rkc)
	60	(and (not (null? (rk-context-seq rkc)))
	61	(list (rk-pending rkc))))))
	62
	63	(define (coqide-current-string lc)
	64	(let ((trans (coqide-current-translation lc)))
	65	(if trans (car trans) "")))
	66
	67	(define (coqide-context-clear lc)
	68	(rk-flush (coqide-context-rkc lc)))
	69
	70	(define (coqide-context-flush lc)
	71	(let ((str (coqide-current-string lc)))
	72	(if (not (equal? str "")) (im-commit lc str))
	73	(coqide-context-clear lc)))
	74
	75	(define (coqide-open-candidates-window lc height)
	76	(if (coqide-context-show-cands lc)
	77	(im-deactivate-candidate-selector lc))
	78	(im-activate-candidate-selector lc height height)
	79	(im-select-candidate lc 0)
	80	(coqide-context-set-show-cands! lc #t))
	81
	82	(define (coqide-close-candidates-window lc)
	83	(if (coqide-context-show-cands lc)
	84	(im-deactivate-candidate-selector lc))
	85	(coqide-context-set-show-cands! lc #f))
	86
	87	(define (coqide-update-preedit lc)
	88	(if (coqide-context-on lc)
	89	(let ((trans (coqide-current-translation lc))
	90	(ltrans 0))
	91	(im-clear-preedit lc)
	92	(if trans
	93	(begin (im-pushback-preedit lc
	94	preedit-underline
	95	(car trans))
	96	(set! ltrans (length trans))))
	97	(im-pushback-preedit lc
	98	preedit-cursor
	99	"")
	100	(im-update-preedit lc)
	101	(if (> ltrans 1)
	102	(coqide-open-candidates-window lc ltrans)
	103	(coqide-close-candidates-window lc)))))
	104
	105	(define (coqide-prepare-activation lc)
	106	(coqide-context-flush lc)
	107	(coqide-update-preedit lc))
	108
	109	(register-action 'action_coqide_off
	110	(lambda (lc)
	111	(list
	112	'off
	113	"a"
	114	(N_ "CoqIDE mode off")
	115	(N_ "CoqIDE composition off")))
	116	(lambda (lc)
	117	(not (coqide-context-on lc)))
	118	(lambda (lc)
	119	(coqide-prepare-activation lc)
	120	(coqide-context-set-on! lc #f)))
	121
	122	(register-action 'action_coqide_on
	123	(lambda (lc)
	124	(list
	125	'on
	126	"à"
	127	(N_ "CoqIDE mode on")
	128	(N_ "CoqIDE composition on")))
	129	(lambda (lc)
	130	(coqide-context-on lc))
	131	(lambda (lc)
	132	(coqide-prepare-activation lc)
	133	(coqide-context-set-on! lc #t)))
	134
	135	(define coqide-input-mode-actions
	136	'(action_coqide_off action_coqide_on))
	137
	138	(define coqide-widgets '(widget_coqide_input_mode))
	139
	140	(define default-widget_coqide_input_mode 'action_coqide_on)
	141
	142	(register-widget 'widget_coqide_input_mode
	143	(activity-indicator-new coqide-input-mode-actions)
	144	(actions-new coqide-input-mode-actions))
	145
	146	(define coqide-context-list '())
	147
	148	(define (coqide-init-handler id im arg)
	149	(let ((lc (coqide-context-new id im)))
	150	(set! coqide-context-list (cons lc coqide-context-list))
	151	lc))
	152
	153	(define (coqide-release-handler lc)
	154	(let ((rkc (coqide-context-rkc lc)))
	155	(set! coqide-context-list
	156	;; (delete lc coqide-context-list eq?) does not work
	157	(remove (lambda (c) (eq? (coqide-context-rkc c) rkc))
	158	coqide-context-list))))
	159
	160	(define coqide-control-key?
	161	(let ((shift-or-no-modifier? (make-key-predicate '("<Shift>" ""))))
	162	(lambda (key key-state)
	163	(not (shift-or-no-modifier? -1 key-state)))))
	164
	165	(define (coqide-proc-on-state lc key key-state)
	166	(let ((rkc (coqide-context-rkc lc))
	167	(cur-trans (coqide-current-translation lc)))
	168	(cond
	169
	170	((or (coqide-off-key? key key-state)
	171	(and coqide-esc-turns-off? (eq? key 'escape)))
	172	(coqide-context-flush lc)
	173	(if (eq? key 'escape)
	174	(im-commit-raw lc))
	175	(coqide-context-set-on! lc #f)
	176	(coqide-close-candidates-window lc)
	177	(im-clear-preedit lc)
	178	(im-update-preedit lc))
	179
	180	((coqide-backspace-key? key key-state)
	181	(if (not (rk-backspace rkc))
	182	(im-commit-raw lc)))
	183
	184	((coqide-control-key? key key-state)
	185	(coqide-context-flush lc)
	186	(im-commit-raw lc))
	187
	188	((and (ichar-numeric? key)
	189	(coqide-context-show-cands lc)
	190	(let ((idx (- (numeric-ichar->integer key) 1)))
	191	(if (= idx -1) (set! idx 9))
	192	(and (>= idx 0) (< idx (length cur-trans))
	193	(begin
	194	(im-commit lc (nth idx cur-trans))
	195	(coqide-context-clear lc)
	196	#t)))))
	197
	198	(else
	199	(let* ((key-str (if (symbol? key)
	200	(symbol->string key)
	201	(charcode->string key)))
	202	(cur-seq (rk-context-seq rkc))
	203	(res (rk-push-key! rkc key-str))
	204	(new-seq (rk-context-seq rkc))
	205	(new-trans (coqide-current-translation lc)))
	206	(if (equal? new-seq (cons key-str cur-seq))
	207	(if (not (or (rk-partial? rkc) (> (length new-trans) 1)))
	208	(begin (im-commit lc (car (rk-peek-terminal-match rkc)))
	209	(coqide-context-clear lc)))
	210	(begin (if (not (null? cur-seq)) (im-commit lc (car cur-trans)))
	211	(if (null? new-seq) (im-commit-raw lc)))))))))
	212
	213	(define (coqide-proc-off-state lc key key-state)
	214	(if (coqide-on-key? key key-state)
	215	(coqide-context-set-on! lc #t)
	216	(im-commit-raw lc)))
	217
	218	(define (coqide-key-press-handler lc key key-state)
	219	(if (coqide-context-on lc)
	220	(coqide-proc-on-state lc key key-state)
	221	(coqide-proc-off-state lc key key-state))
	222	(coqide-update-preedit lc))
	223
	224	(define (coqide-key-release-handler lc key key-state)
	225	(if (or (ichar-control? key)
	226	(not (coqide-context-on lc)))
	227	;; don't discard key release event for apps
	228	(im-commit-raw lc)))
	229
	230	(define (coqide-reset-handler lc)
	231	(coqide-context-clear lc))
	232
	233	(define (coqide-get-candidate-handler lc idx accel-enum-hint)
	234	(let* ((candidates (coqide-current-translation lc))
	235	(candidate (nth idx candidates)))
	236	(list candidate (digit->string (+ idx 1)) "")))
	237
	238	;; Emacs does nothing on focus-out
	239	;; TODO: this should be configurable
	240	(define (coqide-focus-out-handler lc)
	241	#f)
	242
	243	(define (coqide-place-handler lc)
	244	(coqide-update-preedit lc))
	245
	246	(define (coqide-displace-handler lc)
	247	(coqide-context-flush lc)
	248	(coqide-update-preedit lc))
	249
	250	(register-im
	251	'coqide
	252	""
	253	"UTF-8"
	254	coqide-im-name-label
	255	coqide-im-short-desc
	256	#f
	257	coqide-init-handler
	258	coqide-release-handler
	259	context-mode-handler
	260	coqide-key-press-handler
	261	coqide-key-release-handler
	262	coqide-reset-handler
	263	coqide-get-candidate-handler
	264	#f
	265	context-prop-activate-handler
	266	#f
	267	#f
	268	coqide-focus-out-handler
	269	coqide-place-handler
	270	coqide-displace-handler
	271	)
	272
	273	;; Local Variables:
	274	;; mode: scheme
	275	;; coding: utf-8
	276	;; End:

-1

interp/constrintern.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: constrintern.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
	8	(* $Id: constrintern.ml 13620 2010-11-04 14:11:49Z herbelin $ *)
9	9
10	10	open Pp
11	11	open Util

265	265	try
266	266	let idscopes,typ = List.assoc id ntnvars in
267	267	if !idscopes <> None &
	268	(* scopes have no effect on the interpretation of identifiers, hence
	269	we can tolerate having a variable occurring several times in
	270	different scopes: *) typ <> NtnInternTypeIdent &
268	271	make_current_scope (Option.get !idscopes)
269	272	<> make_current_scope (scopt,scopes) then
270	273	error_inconsistent_scope loc id

+25

-8

interp/dumpglob.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: dumpglob.ml 13328 2010-07-26 11:05:30Z herbelin $ *)
	8	(* $Id: dumpglob.ml 13674 2010-12-04 10:34:11Z herbelin $ *)
9	9
10	10
11	11	(* Dump of globalization (to be used by coqdoc) *)

180	180	(fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty)
181	181
182	182	let cook_notation df sc =
	183	(* We encode notations so that they are space-free and still human-readable *)
	184	(* - all spaces are replaced by _ *)
	185	(* - all _ denoting a non-terminal symbol are replaced by x *)
	186	(* - all terminal tokens are surrounded by single quotes, including '_' *)
	187	(* which already denotes terminal _ *)
	188	(* - all single quotes in terminal tokens are doubled *)
	189	(* The output is decoded in function Index.prepare_entry of coqdoc *)
183	190	let ntn = String.make (String.length df * 3) '_' in
184	191	let j = ref 0 in
185		let quoted = ref false in
186		for i = 0 to String.length df - 1 do
187		if df.[i] = '\'' then quoted := not !quoted;
188		if df.[i] = ' ' then (ntn.[!j] <- '_'; incr j) else
189		if df.[i] = '_' && not !quoted then (ntn.[!j] <- 'x'; incr j) else
190		if df.[i] = 'x' && not !quoted then (String.blit "'x'" 0 ntn !j 3; j := !j + 3) else
191		(ntn.[!j] <- df.[i]; incr j)
	192	let l = String.length df - 1 in
	193	let i = ref 0 in
	194	while !i <= l do
	195	assert (df.[!i] <> ' ');
	196	if df.[!i] = '_' && (!i = l \|\| df.[!i+1] = ' ') then
	197	(* Next token is a non-terminal *)
	198	(ntn.[!j] <- 'x'; incr j; incr i)
	199	else begin
	200	(* Next token is a terminal *)
	201	ntn.[!j] <- '\''; incr j;
	202	while !i <= l && df.[!i] <> ' ' do
	203	if df.[!i] = '\'' then (ntn.[!j] <- '\''; incr j);
	204	ntn.[!j] <- df.[!i]; incr j; incr i
	205	done;
	206	ntn.[!j] <- '\''; incr j
	207	end;
	208	if !i <= l then (ntn.[!j] <- '_'; incr j; incr i)
192	209	done;
193	210	let df = String.sub ntn 0 !j in
194	211	match sc with Some sc -> ":" ^ sc ^ ":" ^ df \| _ -> "::" ^ df

+11

-11

interp/topconstr.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: topconstr.ml 13357 2010-07-29 22:59:55Z herbelin $ *)
	8	(* $Id: topconstr.ml 13680 2010-12-04 15:06:06Z herbelin $ *)
9	9
10	10	(i)
11	11	open Pp

114	114	let outerl = [(ldots_var,inner)] in
115	115	subst_rawvars outerl it
116	116	\| ALambda (na,ty,c) ->
117		let e,na = g e na in RLambda (loc,na,Explicit,f e ty,f e c)
	117	let e',na = g e na in RLambda (loc,na,Explicit,f e ty,f e' c)
118	118	\| AProd (na,ty,c) ->
119		let e,na = g e na in RProd (loc,na,Explicit,f e ty,f e c)
	119	let e',na = g e na in RProd (loc,na,Explicit,f e ty,f e' c)
120	120	\| ALetIn (na,b,c) ->
121		let e,na = g e na in RLetIn (loc,na,f e b,f e c)
	121	let e',na = g e na in RLetIn (loc,na,f e b,f e' c)
122	122	\| ACases (sty,rtntypopt,tml,eqnl) ->
123	123	let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
124	124	let e',t' = match t with

136	136	(loc,idl,patl,f e rhs)) eqnl in
137	137	RCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl')
138	138	\| ALetTuple (nal,(na,po),b,c) ->
139		let e,nal = list_fold_map g e nal in
140		let e,na = g e na in
141		RLetTuple (loc,nal,(na,Option.map (f e) po),f e b,f e c)
	139	let e',nal = list_fold_map g e nal in
	140	let e'',na = g e na in
	141	RLetTuple (loc,nal,(na,Option.map (f e'') po),f e b,f e' c)
142	142	\| AIf (c,(na,po),b1,b2) ->
143		let e,na = g e na in
144		RIf (loc,f e c,(na,Option.map (f e) po),f e b1,f e b2)
	143	let e',na = g e na in
	144	RIf (loc,f e c,(na,Option.map (f e') po),f e b1,f e b2)
145	145	\| ARec (fk,idl,dll,tl,bl) ->
146		let e,idl = array_fold_map (to_id g) e idl in
147	146	let e,dll = array_fold_map (list_fold_map (fun e (na,oc,b) ->
148	147	let e,na = g e na in
149	148	(e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
150		RRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e) bl)
	149	let e',idl = array_fold_map (to_id g) e idl in
	150	RRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
151	151	\| ACast (c,k) -> RCast (loc,f e c,
152	152	match k with
153	153	\| CastConv (k,t) -> CastConv (k,f e t)

-2

kernel/subtyping.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: subtyping.ml 13323 2010-07-24 15:57:30Z herbelin $ i)
	8	(i $Id: subtyping.ml 13616 2010-11-03 12:14:36Z soubiran $ i)
9	9
10	10	(i)
11	11	open Util

162	162	match mind_of_delta reso2 kn2 with
163	163	\| kn2' when kn2=kn2' -> ()
164	164	\| kn2' ->
165		if not (eq_mind (mind_of_delta reso1 kn1) kn2') then
	165	if not (eq_mind (mind_of_delta reso1 kn1) (subst_ind subst2 kn2')) then
166	166	error ()
167	167	end;
168	168	(* we check that records and their field names are preserved. *)

-2

kernel/term.mli less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: term.mli 13323 2010-07-24 15:57:30Z herbelin $ i)
	8	(i $Id: term.mli 13728 2010-12-19 11:35:20Z herbelin $ i)
9	9
10	10	(i)
11	11	open Names

506	506
507	507	(* Checking function for terms containing existential- or
508	508	meta-variables. The function [noccur_with_meta] does not consider
509		meta-variables applied to some terms (intented to be its local
	509	meta-variables applied to some terms (intended to be its local
510	510	context) (for existential variables, it is necessarily the case) *)
511	511	val noccur_with_meta : int -> int -> constr -> bool
512	512

+53

-61

kernel/univ.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: univ.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
	8	(* $Id: univ.ml 13735 2010-12-21 18:21:58Z letouzey $ *)
9	9
10	10	(* Initial Caml version originates from CoC 4.8 [Dec 1988] *)
11	11	(* Extension with algebraic universes by HH [Sep 2001] *)

114	114
115	115	(* A universe_level is either an alias for another one, or a canonical one,
116	116	for which we know the universes that are above *)
	117
117	118	type univ_entry =
118	119	Canonical of canonical_arc
119		\| Equiv of universe_level * universe_level
	120	\| Equiv of universe_level
120	121
121	122
122	123	type universes = univ_entry UniverseLMap.t
123	124
124	125	let enter_equiv_arc u v g =
125		UniverseLMap.add u (Equiv(u,v)) g
	126	UniverseLMap.add u (Equiv v) g
126	127
127	128	let enter_arc ca g =
128	129	UniverseLMap.add ca.univ (Canonical ca) g

172	173	(str"Universe " ++ pr_uni_level u ++ str" undefined")
173	174	in
174	175	match a with
175		\| Equiv(_,v) -> repr_rec v
	176	\| Equiv v -> repr_rec v
176	177	\| Canonical arc -> arc
177	178	in
178	179	repr_rec u
179	180
180	181	let can g = List.map (repr g)
181
182		(* transitive closure : we follow the Less links *)
183
184		(* collect : canonical_arc -> canonical_arc list * canonical_arc list *)
185		(* collect u = (V,W) iff V={v canonical \| u<v} W={w canonical \| u<=w}-V *)
186		(* i.e. collect does the transitive upward closure of what is known about u *)
187		let collect g arcu =
188		let rec coll_rec lt le = function
189		\| [],[] -> (lt, list_subtractq le lt)
190		\| arcv::lt', le' ->
191		if List.memq arcv lt then
192		coll_rec lt le (lt',le')
193		else
194		coll_rec (arcv::lt) le ((can g (arcv.lt@arcv.le))@lt',le')
195		\| [], arcw::le' ->
196		if (List.memq arcw lt) or (List.memq arcw le) then
197		coll_rec lt le ([],le')
198		else
199		coll_rec lt (arcw::le) (can g arcw.lt, (can g arcw.le)@le')
200		in
201		coll_rec [] [] ([],[arcu])
202	182
203	183	(* reprleq : canonical_arc -> canonical_arc list *)
204	184	(* All canonical arcv such that arcu<=arcv with arcv#arcu *)

251	231
252	232	type order = EQ \| LT \| LE \| NLE
253	233
254		(* compare : universe_level -> universe_level -> order *)
	234	(** [compare_neq] : is [arcv] in the transitive upward closure of [arcu] ?
	235
	236	We try to avoid visiting unneeded parts of this transitive closure,
	237	by stopping as soon as [arcv] is encountered. During the recursive
	238	traversal, [lt_done] and [le_done] are universes we have already
	239	visited, they do not contain [arcv]. The 3rd arg is
	240	[(lt_todo,le_todo)], two lists of universes not yet considered,
	241	known to be above [arcu], strictly or not.
	242
	243	We use depth-first search, but the presence of [arcv] in [new_lt]
	244	is checked as soon as possible : this seems to be slightly faster
	245	on a test.
	246	*)
	247
	248	let compare_neq g arcu arcv =
	249	let rec cmp lt_done le_done = function
	250	\| [],[] -> NLE
	251	\| arc::lt_todo, le_todo ->
	252	if List.memq arc lt_done then
	253	cmp lt_done le_done (lt_todo,le_todo)
	254	else
	255	let lt_new = can g (arc.lt@arc.le) in
	256	if List.memq arcv lt_new then LT
	257	else cmp (arc::lt_done) le_done (lt_new@lt_todo,le_todo)
	258	\| [], arc::le_todo ->
	259	if arc == arcv then LE
	260	(* No need to continue inspecting universes above arc:
	261	if arcv is strictly above arc, then we would have a cycle *)
	262	else
	263	if (List.memq arc lt_done) \|\| (List.memq arc le_done) then
	264	cmp lt_done le_done ([],le_todo)
	265	else
	266	let lt_new = can g arc.lt in
	267	if List.memq arcv lt_new then LT
	268	else
	269	let le_new = can g arc.le in
	270	cmp lt_done (arc::le_done) (lt_new, le_new@le_todo)
	271	in
	272	cmp [] [] ([],[arcu])
	273
255	274	let compare g u v =
256	275	let arcu = repr g u
257	276	and arcv = repr g v in
258		if arcu==arcv then
259		EQ
260		else
261		let (lt,leq) = collect g arcu in
262		if List.memq arcv lt then
263		LT
264		else if List.memq arcv leq then
265		LE
266		else
267		NLE
	277	if arcu == arcv then EQ else compare_neq g arcu arcv
268	278
269	279	(* Invariants : compare(u,v) = EQ <=> compare(v,u) = EQ
270	280	compare(u,v) = LT or LE => compare(v,u) = NLE

297	307	compare_list (compare_eq g) ule vle &&
298	308	compare_list (compare_eq g) ult vlt
299	309	\| _ -> anomaly "check_eq" (* not complete! (Atom(u) = Max([u],[]) *)
300
301		let check_eq g u v =
302		check_eq g u v
303	310
304	311	let compare_greater g strict u v =
305	312	let g = declare_univ u g in

428	435	\| NLE -> setlt g u v
429	436	\| _ -> error_inconsistency Lt u v)
430	437
431		(*
432		let enforce_univ_relation g = function
433		\| Equiv (u,v) -> enforce_univ_eq u v g
434		\| Canonical {univ=u; lt=lt; le=le} ->
435		let g' = List.fold_right (enforce_univ_lt u) lt g in
436		List.fold_right (enforce_univ_leq u) le g'
437		*)
438
439		(* Merging 2 universe graphs *)
440		(*
441		let merge_universes sp u1 u2 =
442		UniverseLMap.fold (fun _ a g -> enforce_univ_relation g a) u1 u2
443		*)
444
445
446	438	(* Constraints and sets of consrtaints. *)
447	439
448	440	type constraint_type = Lt \| Leq \| Eq

577	569	UniverseLMap.fold (fun _ a n -> n + (reln_len a)) g 0
578	570
579	571	let pr_arc = function
580		\| Canonical {univ=u; lt=[]; le=[]} ->
	572	\| _, Canonical {univ=u; lt=[]; le=[]} ->
581	573	mt ()
582		\| Canonical {univ=u; lt=lt; le=le} ->
	574	\| _, Canonical {univ=u; lt=lt; le=le} ->
583	575	pr_uni_level u ++ str " " ++
584	576	v 0
585	577	(prlist_with_sep pr_spc (fun v -> str "< " ++ pr_uni_level v) lt ++
586	578	(if lt <> [] & le <> [] then spc () else mt()) ++
587	579	prlist_with_sep pr_spc (fun v -> str "<= " ++ pr_uni_level v) le) ++
588	580	fnl ()
589		\| Equiv (u,v) ->
	581	\| u, Equiv v ->
590	582	pr_uni_level u ++ str " = " ++ pr_uni_level v ++ fnl ()
591	583
592	584	let pr_universes g =
593		let graph = UniverseLMap.fold (fun k a l -> (k,a)::l) g [] in
594		prlist (function (_,a) -> pr_arc a) graph
	585	let graph = UniverseLMap.fold (fun u a l -> (u,a)::l) g [] in
	586	prlist pr_arc graph
595	587
596	588	let pr_constraints c =
597	589	Constraint.fold (fun (u1,op,u2) pp_std ->

605	597	(* Dumping constraints to a file *)
606	598
607	599	let dump_universes output g =
608		let dump_arc _ = function
	600	let dump_arc u = function
609	601	\| Canonical {univ=u; lt=lt; le=le} ->
610	602	let u_str = string_of_univ_level u in
611	603	List.iter

618	610	Printf.fprintf output "%s <= %s ;\n" u_str
619	611	(string_of_univ_level v))
620	612	le
621		\| Equiv (u,v) ->
	613	\| Equiv v ->
622	614	Printf.fprintf output "%s = %s ;\n"
623	615	(string_of_univ_level u) (string_of_univ_level v)
624	616	in

+12

-0

lib/compat.ml4 less more

64	64	let join_loc = M.join_loc
65	65	type token = M.token
66	66	type lexer = M.lexer
	67
	68	IFDEF CAMLP5_6_00 THEN
	69
	70	let slist0sep x y = Gramext.Slist0sep (x, y, false)
	71	let slist1sep x y = Gramext.Slist1sep (x, y, false)
	72
	73	ELSE
	74
	75	let slist0sep x y = Gramext.Slist0sep (x, y)
	76	let slist1sep x y = Gramext.Slist1sep (x, y)
	77
	78	END

-2

parsing/g_vernac.ml4 less more

8	8	(i camlp4deps: "parsing/grammar.cma" i)
9	9	(i camlp4use: "pa_extend.cmo" i)
10	10
11		(* $Id: g_vernac.ml4 13492 2010-10-04 21:20:01Z herbelin $ *)
	11	(* $Id: g_vernac.ml4 13699 2010-12-09 19:24:45Z herbelin $ *)
12	12
13	13
14	14	open Pp

232	232	def_body:
233	233	[ [ bl = binders; ":="; red = reduce; c = lconstr ->
234	234	(match c with
235		CCast(_,c, Rawterm.CastConv (k,t)) -> DefineBody (bl, red, c, Some t)
	235	CCast(_,c, Rawterm.CastConv (Term.DEFAULTcast,t)) -> DefineBody (bl, red, c, Some t)
236	236	\| _ -> DefineBody (bl, red, c, None))
237	237	\| bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
238	238	DefineBody (bl, red, c, Some t)

+15

-10

parsing/pcoq.ml4 less more

7	7
8	8	(i camlp4use: "pa_extend.cmo pa_macro.cmo" i)
9	9
10		(i $Id: pcoq.ml4 13329 2010-07-26 11:05:39Z herbelin $ i)
	10	(i $Id: pcoq.ml4 13690 2010-12-06 16:15:54Z glondu $ i)
11	11
12	12	open Pp
13	13	open Util

144	144	G.delete_rule e pil
145	145	end
146	146
	147	IFDEF CAMLP5_6_02_1 THEN
	148	let entry_print x = Gram.Entry.print !Pp_control.std_ft x
	149	ELSE
	150	let entry_print = Gram.Entry.print
	151	END
147	152
148	153	let camlp4_verbosity silent f x =
149	154	let a = !Gramext.warning_verbose in

630	635	\| ETConstrList (typ',[]) ->
631	636	Gramext.Slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
632	637	\| ETConstrList (typ',tkl) ->
633		Gramext.Slist1sep
634		(symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'),
635		make_sep_rules tkl)
	638	Compat.slist1sep
	639	(symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'))
	640	(make_sep_rules tkl)
636	641	\| ETBinderList (false,[]) ->
637	642	Gramext.Slist1
638	643	(symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false))
639	644	\| ETBinderList (false,tkl) ->
640		Gramext.Slist1sep
641		(symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false),
642		make_sep_rules tkl)
	645	Compat.slist1sep
	646	(symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false))
	647	(make_sep_rules tkl)
643	648	\| _ ->
644	649	match interp_constr_prod_entry_key assoc from forpat typ with
645	650	\| (eobj,None,_) -> Gramext.Snterm (Gram.Entry.obj eobj)

653	658	let rec symbol_of_prod_entry_key = function
654	659	\| Alist1 s -> Gramext.Slist1 (symbol_of_prod_entry_key s)
655	660	\| Alist1sep (s,sep) ->
656		Gramext.Slist1sep (symbol_of_prod_entry_key s, Gramext.Stoken ("",sep))
	661	Compat.slist1sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", sep))
657	662	\| Alist0 s -> Gramext.Slist0 (symbol_of_prod_entry_key s)
658	663	\| Alist0sep (s,sep) ->
659		Gramext.Slist0sep (symbol_of_prod_entry_key s, Gramext.Stoken ("",sep))
	664	Compat.slist0sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", sep))
660	665	\| Aopt s -> Gramext.Sopt (symbol_of_prod_entry_key s)
661	666	\| Amodifiers s ->
662	667	Gramext.srules
663	668	[([], Gramext.action(fun _loc -> []));
664	669	([Gramext.Stoken ("", "(");
665		Gramext.Slist1sep ((symbol_of_prod_entry_key s), Gramext.Stoken ("", ","));
	670	Compat.slist1sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", ","));
666	671	Gramext.Stoken ("", ")")],
667	672	Gramext.action (fun _ l _ _loc -> l))]
668	673	\| Aself -> Gramext.Sself

-1

parsing/pcoq.mli less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: pcoq.mli 13329 2010-07-26 11:05:39Z herbelin $ i)
	8	(i $Id: pcoq.mli 13690 2010-12-06 16:15:54Z glondu $ i)
9	9
10	10	open Util
11	11	open Names

21	21	(* The parser of Coq *)
22	22
23	23	module Gram : Grammar.S with type te = Compat.token
	24
	25	val entry_print : 'a Gram.Entry.e -> unit
24	26
25	27	(**********************************************************************)
26	28	(* The parser of Coq is built from three kinds of rule declarations:

-1

plugins/dp/dp.ml less more

718	718	\| _, [a;b] when c = Lazy.force coq_iff ->
719	719	Iff (tr_formula tv bv env a, tr_formula tv bv env b)
720	720	\| Prod (n, a, b), _ ->
721		if is_imp_term f then
	721	if is_Prop (Typing.type_of env Evd.empty a) then
722	722	Imp (tr_formula tv bv env a, tr_formula tv bv env b)
723	723	else
724	724	let id, t, bv, env, b = quantifiers n a b tv bv env in

+16

-8

plugins/extraction/extraction.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: extraction.ml 13427 2010-09-17 17:37:52Z letouzey $ i)
	8	(i $Id: extraction.ml 13733 2010-12-21 13:08:53Z letouzey $ i)
9	9
10	10	(i)
11	11	open Util

28	28	open Mlutil
29	29	(i)
30	30
31		exception I of inductive_info
	31	exception I of inductive_kind
32	32
33	33	(* A set of all fixpoint functions currently being extracted *)
34	34	let current_fixpoints = ref ([] : constant list)

367	367	in
368	368
369	369	add_ind kn mib
370		{ind_info = Standard;
	370	{ind_kind = Standard;
371	371	ind_nparams = npar;
372	372	ind_packets = packets;
373	373	ind_equiv = equiv

452	452	Record field_glob
453	453	with (I info) -> info
454	454	in
455		let i = {ind_info = ind_info;
	455	let i = {ind_kind = ind_info;
456	456	ind_nparams = npar;
457	457	ind_packets = packets;
458	458	ind_equiv = equiv }

710	710	let magic1 = needs_magic (type_cons, type_recomp (metas, a)) in
711	711	let magic2 = needs_magic (a, mlt) in
712	712	let head mla =
713		if mi.ind_info = Singleton then
	713	if mi.ind_kind = Singleton then
714	714	put_magic_if magic1 (List.hd mla) (* assert (List.length mla = 1) *)
715		else put_magic_if magic1 (MLcons (mi.ind_info, ConstructRef cp, mla))
	715	else
	716	let typeargs = match snd (type_decomp type_cons) with
	717	\| Tglob (_,l) -> List.map type_simpl l
	718	\| _ -> assert false
	719	in
	720	let info = {c_kind = mi.ind_kind; c_typs = typeargs} in
	721	put_magic_if magic1 (MLcons (info, ConstructRef cp, mla))
716	722	in
717	723	(* Different situations depending of the number of arguments: *)
718	724	if la < params_nb then

778	784	let e' = handle_exn r (List.length s) (fun _ -> Anonymous) e in
779	785	(r, List.rev ids, e')
780	786	in
781		if mi.ind_info = Singleton then
	787	if mi.ind_kind = Singleton then
782	788	begin
783	789	(* Informative singleton case: *)
784	790	(* [match c with C i -> t] becomes [let i = c' in t'] *)

789	795	end
790	796	else
791	797	(* Standard case: we apply [extract_branch]. *)
792		MLcase ((mi.ind_info,BranchNone), a, Array.init br_size extract_branch)
	798	let typs = List.map type_simpl (Array.to_list metas) in
	799	let info = { m_kind = mi.ind_kind; m_typs = typs; m_same = BranchNone }
	800	in MLcase (info, a, Array.init br_size extract_branch)
793	801
794	802	(s Extraction of a (co)-fixpoint. )
795	803

+24

-19

plugins/extraction/haskell.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: haskell.ml 13414 2010-09-14 13:28:15Z glondu $ i)
	8	(i $Id: haskell.ml 13733 2010-12-21 13:08:53Z letouzey $ i)
9	9
10	10	(s Production of Haskell syntax. )
11	11

155	155	hov 2 (str (find_custom_match pv) ++ fnl () ++
156	156	prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv
157	157	++ pp_expr true env [] t)
158		\| MLcase ((_,factors),t, pv) ->
	158	\| MLcase (info,t, pv) ->
159	159	apply (pp_par par'
160	160	(v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++
161		fnl () ++ str " " ++ pp_pat env factors pv)))
	161	fnl () ++ str " " ++ pp_pat env info pv)))
162	162	\| MLfix (i,ids,defs) ->
163	163	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
164	164	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args

171	171	pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args)
172	172	\| MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"")
173	173
174		and pp_pat env factors pv =
	174	and pp_pat env info pv =
175	175	let pp_one_pat (name,ids,t) =
176	176	let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
177	177	let par = expr_needs_par t in

183	183	(fun () -> (spc ())) pr_id (List.rev ids))) ++
184	184	str " ->" ++ spc () ++ pp_expr par env' [] t)
185	185	in
186		let factor_br, factor_l = try match factors with
187		\| BranchFun (i::_ as l) -> check_function_branch pv.(i), l
188		\| BranchCst (i::_ as l) -> ast_pop (check_constant_branch pv.(i)), l
189		\| _ -> MLdummy, []
190		with Impossible -> MLdummy, []
191		in
192		let par = expr_needs_par factor_br in
	186	let factor_br, factor_set = try match info.m_same with
	187	\| BranchFun ints ->
	188	let i = Intset.choose ints in
	189	branch_as_fun info.m_typs pv.(i), ints
	190	\| BranchCst ints ->
	191	let i = Intset.choose ints in
	192	ast_pop (branch_as_cst pv.(i)), ints
	193	\| BranchNone -> MLdummy, Intset.empty
	194	with _ -> MLdummy, Intset.empty
	195	in
193	196	let last = Array.length pv - 1 in
194	197	prvecti
195		(fun i x -> if List.mem i factor_l then mt () else
	198	(fun i x -> if Intset.mem i factor_set then mt () else
196	199	(pp_one_pat pv.(i) ++
197		if i = last && factor_l = [] then mt () else
	200	if i = last && Intset.is_empty factor_set then mt () else
198	201	fnl () ++ str " ")) pv
199	202	++
200		if factor_l = [] then mt () else match factors with
	203	if Intset.is_empty factor_set then mt () else
	204	let par = expr_needs_par factor_br in
	205	match info.m_same with
201	206	\| BranchFun _ ->
202		let ids, env' = push_vars [anonymous_name] env in
203		pr_id (List.hd ids) ++ str " ->" ++ spc () ++
204		pp_expr par env' [] factor_br
	207	let ids, env' = push_vars [anonymous_name] env in
	208	pr_id (List.hd ids) ++ str " ->" ++ spc () ++
	209	pp_expr par env' [] factor_br
205	210	\| BranchCst _ ->
206		str "_ ->" ++ spc () ++ pp_expr par env [] factor_br
	211	str "_ ->" ++ spc () ++ pp_expr par env [] factor_br
207	212	\| BranchNone -> mt ()
208	213
209	214	(*s names of the functions ([ids]) are already pushed in [env],

285	290	let pp_string_parameters ids = prlist (fun id -> str id ++ str " ")
286	291
287	292	let pp_decl = function
288		\| Dind (kn,i) when i.ind_info = Singleton ->
	293	\| Dind (kn,i) when i.ind_kind = Singleton ->
289	294	pp_singleton (mind_of_kn kn) i.ind_packets.(0) ++ fnl ()
290	295	\| Dind (kn,i) -> hov 0 (pp_ind true (mind_of_kn kn) 0 i)
291	296	\| Dtype (r, l, t) ->

+25

-10

plugins/extraction/miniml.mli less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: miniml.mli 13323 2010-07-24 15:57:30Z herbelin $ i)
	8	(i $Id: miniml.mli 13733 2010-12-21 13:08:53Z letouzey $ i)
9	9
10	10	(s Target language for extraction: a core ML called MiniML. )
11	11

52	52
53	53	(s ML inductive types. )
54	54
55		type inductive_info =
	55	type inductive_kind =
56	56	\| Singleton
57	57	\| Coinductive
58	58	\| Standard

84	84	\| RenEquiv of string
85	85
86	86	type ml_ind = {
87		ind_info : inductive_info;
	87	ind_kind : inductive_kind;
88	88	ind_nparams : int;
89	89	ind_packets : ml_ind_packet array;
90	90	ind_equiv : equiv

97	97	\| Id of identifier
98	98	\| Tmp of identifier
99	99
100		(* list of branches to merge in a common pattern *)
101
102		type case_info =
	100	(** We now store some typing information on constructors
	101	and cases to avoid type-unsafe optimisations.
	102	For cases, we also store the set of branches to merge
	103	in a common pattern, either "_ -> c" or "x -> f x"
	104	*)
	105
	106	type constructor_info = {
	107	c_kind : inductive_kind;
	108	c_typs : ml_type list;
	109	}
	110
	111	type branch_same =
103	112	\| BranchNone
104		\| BranchFun of int list
105		\| BranchCst of int list
	113	\| BranchFun of Intset.t
	114	\| BranchCst of Intset.t
	115
	116	type match_info = {
	117	m_kind : inductive_kind;
	118	m_typs : ml_type list;
	119	m_same : branch_same
	120	}
106	121
107	122	type ml_branch = global_reference * ml_ident list * ml_ast
108	123

112	127	\| MLlam of ml_ident * ml_ast
113	128	\| MLletin of ml_ident * ml_ast * ml_ast
114	129	\| MLglob of global_reference
115		\| MLcons of inductive_info * global_reference * ml_ast list
116		\| MLcase of (inductive_infocase_info) ml_ast * ml_branch array
	130	\| MLcons of constructor_info * global_reference * ml_ast list
	131	\| MLcase of match_info * ml_ast * ml_branch array
117	132	\| MLfix of int * identifier array * ml_ast array
118	133	\| MLexn of string
119	134	\| MLdummy

+65

-76

plugins/extraction/mlutil.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: mlutil.ml 13420 2010-09-16 15:47:08Z letouzey $ i)
	8	(i $Id: mlutil.ml 13733 2010-12-21 13:08:53Z letouzey $ i)
9	9
10	10	(i)
11	11	open Pp

289	289	\| Tarr (a,b) -> Tarr (expand a, expand b)
290	290	\| a -> a
291	291	in if Table.type_expand () then expand t else t
	292
	293	let type_simpl = type_expand (fun _ -> None)
292	294
293	295	(s Generating a signature from a ML type. )
294	296

664	666
665	667	(S Auxiliary functions used in simplification of ML cases. )
666	668
667		(*s [check_function_branch (r,l,c)] checks if branch [c] can be seen
	669	(* Factorisation of some match branches into a common "x -> f x"
	670	branch may break types sometimes. Example: [type 'x a = A].
	671	Then [let id = function A -> A] has type ['x a -> 'y a],
	672	which is incompatible with the type of [let id x = x].
	673	We now check that the type arguments of the inductive are
	674	preserved by our transformation.
	675
	676	TODO: this verification should be done someday modulo
	677	expansion of type definitions.
	678	*)
	679
	680	(*s [branch_as_function b typs (r,l,c)] tries to see branch [c]
668	681	as a function [f] applied to [MLcons(r,l)]. For that it transforms
669		any [MLcons(r,l)] in [MLrel 1] and raises [Impossible] if any
670		variable in [l] occurs outside such a [MLcons] *)
671
672		let check_function_branch (r,l,c) =
	682	any [MLcons(r,l)] in [MLrel 1] and raises [Impossible]
	683	if any variable in [l] occurs outside such a [MLcons] *)
	684
	685	let branch_as_fun typs (r,l,c) =
673	686	let nargs = List.length l in
674	687	let rec genrec n = function
675	688	\| MLrel i as c ->

677	690	if i'<1 then c
678	691	else if i'>nargs then MLrel (i-nargs+1)
679	692	else raise Impossible
680		\| MLcons(_,r',args) when r=r' && (test_eta_args_lift n nargs args) ->
	693	\| MLcons(i,r',args) when
	694	r=r' && (test_eta_args_lift n nargs args) && typs = i.c_typs ->
681	695	MLrel (n+1)
682	696	\| a -> ast_map_lift genrec n a
683	697	in genrec 0 c
684	698
685		(*s [check_constant_branch (r,l,c)] checks if branch [c] is independent
686		from the pattern [MLcons(r,l)]. For that is raises [Impossible] if any
687		variable in [l] occurs in [c], and otherwise returns [c] lifted to
688		appear like a function with one arg (for uniformity with the
689		branch-as-function optimization) *)
690
691		let check_constant_branch (_,l,c) =
	699	(*s [branch_as_cst (r,l,c)] tries to see branch [c] as a constant
	700	independent from the pattern [MLcons(r,l)]. For that is raises [Impossible]
	701	if any variable in [l] occurs in [c], and otherwise returns [c] lifted to
	702	appear like a function with one arg (for uniformity with [branch_as_fun]).
	703	NB: [MLcons(r,l)] might occur nonetheless in [c], but only when [l] is
	704	empty, i.e. when [r] is a constant constructor
	705	*)
	706
	707	let branch_as_cst (_,l,c) =
692	708	let n = List.length l in
693	709	if ast_occurs_itvl 1 n c then raise Impossible;
694	710	ast_lift (1-n) c
	711
	712	(* A branch [MLcons(r,l)->c] can be seen at the same time as a function
	713	branch and a constant branch, either because:
	714	- [MLcons(r,l)] doesn't occur in [c]. For example : "A -> B"
	715	- this constructor is constant (i.e. [l] is empty). For example "A -> A"
	716	When searching for the best factorisation below, we'll try both.
	717	*)
695	718
696	719	(* The following structure allows to record which element occurred
697	720	at what position, and then finally return the most frequent

701	724	let h = Hashtbl.create 13 in
702	725	let clear () = Hashtbl.clear h in
703	726	let add e i =
704		let l = try Hashtbl.find h e with Not_found -> [] in
705		Hashtbl.replace h e (i::l)
	727	let s = try Hashtbl.find h e with Not_found -> Intset.empty in
	728	Hashtbl.replace h e (Intset.add i s)
706	729	in
707	730	let max e0 =
708		let len = ref 0 and lst = ref [] and elm = ref e0 in
	731	let len = ref 0 and lst = ref Intset.empty and elm = ref e0 in
709	732	Hashtbl.iter
710		(fun e l ->
711		let n = List.length l in
712		if n > !len then begin len := n; lst := l; elm := e end)
	733	(fun e s ->
	734	let n = Intset.cardinal s in
	735	if n > !len then begin len := n; lst := s; elm := e end)
713	736	h;
714	737	(!elm,!lst)
715	738	in
716	739	(add,max,clear)
717	740
718		(* Given an abstraction function [abstr] (one of [check_*_branch]),
719		return the longest possible list of branches that have the
720		same abstraction, along with this abstraction. *)
721
722		let factor_branches abstr br =
	741	(* [factor_branches] return the longest possible list of branches
	742	that have the same factorization, either as a function or as a
	743	constant.
	744	*)
	745
	746	let factor_branches o typs br =
723	747	census_clean ();
724	748	for i = 0 to Array.length br - 1 do
725		try census_add (abstr br.(i)) i with Impossible -> ()
	749	if o.opt_case_idr then
	750	(try census_add (branch_as_fun typs br.(i)) i with Impossible -> ());
	751	if o.opt_case_cst then
	752	(try census_add (branch_as_cst br.(i)) i with Impossible -> ());
726	753	done;
727		let br_factor, br_list = census_max MLdummy in
728		if br_list = [] then None
729		else if Array.length br >= 2 && List.length br_list < 2 then None
730		else Some (br_factor, br_list)
731
732		(*s [check_generalizable_case] checks if all branches can be seen as the
733		same function [f] applied to the term matched. It is a generalized version
734		of both the identity case optimization and the constant case optimisation
735		([f] can be a constant function) *)
736
737		(* The optimisation [factor_branches check_function_branch] breaks types
738		in some special case. Example: [type 'x a = A].
739		Then [let f = function A -> A] has type ['x a -> 'y a],
740		which is incompatible with the type of [let f x = x].
741		We check first that there isn't such phantom variable in the inductive type
742		we're considering. *)
743
744		let check_optim_id br =
745		let (kn,i) =
746		match br.(0) with (ConstructRef (c,_),_,_) -> c \| _ -> assert false
747		in
748		let ip = (snd (lookup_ind kn)).ind_packets.(i) in
749		match ip.ip_optim_id_ok with
750		\| Some ok -> ok
751		\| None ->
752		let tvars =
753		intset_union_map_array (intset_union_map_list type_listvar)
754		ip.ip_types
755		in
756		let ok = (Intset.cardinal tvars = List.length ip.ip_vars) in
757		ip.ip_optim_id_ok <- Some ok;
758		ok
	754	let br_factor, br_set = census_max MLdummy in
	755	census_clean ();
	756	let n = Intset.cardinal br_set in
	757	if n = 0 then None
	758	else if Array.length br >= 2 && n < 2 then None
	759	else Some (br_factor, br_set)
759	760
760	761	(s If all branches are functions, try to permut the case and the functions. )
761	762

896	897	if n <> 0 then
897	898	simpl o (named_lams ids (MLcase (i,ast_lift n e, br)))
898	899	else
899		(* Does a term [f] exist such that many branches are [(f e)] ? *)
900		let opt1 =
901		if o.opt_case_idr && (o.opt_case_idg \|\| check_optim_id br) then
902		factor_branches check_function_branch br
903		else None
904		in
905		(* Detect common constant branches. Often a particular case of
906		branch-as-function optim, but not always (e.g. A->A\|B->A) *)
907		let opt2 =
908		if opt1 = None && o.opt_case_cst then
909		factor_branches check_constant_branch br
910		else opt1
911		in
912		match opt2 with
913		\| Some (f,ints) when List.length ints = Array.length br ->
914		(* if all branches have been factorized, we remove the match *)
	900	(* Can we merge several branches as the same constant or function ? *)
	901	match factor_branches o i.m_typs br with
	902	\| Some (f,ints) when Intset.cardinal ints = Array.length br ->
	903	(* If all branches have been factorized, we remove the match *)
915	904	simpl o (MLletin (Tmp anonymous_name, e, f))
916	905	\| Some (f,ints) ->
917		let ci = if ast_occurs 1 f then BranchFun ints else BranchCst ints
918		in MLcase ((fst i,ci), e, br)
	906	let same = if ast_occurs 1 f then BranchFun ints else BranchCst ints
	907	in MLcase ({i with m_same=same}, e, br)
919	908	\| None -> MLcase (i, e, br)
920	909
921	910	(S Local prop elimination. )

-3

plugins/extraction/mlutil.mli less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: mlutil.mli 13420 2010-09-16 15:47:08Z letouzey $ i)
	8	(i $Id: mlutil.mli 13733 2010-12-21 13:08:53Z letouzey $ i)
9	9
10	10	open Util
11	11	open Names

62	62	type abbrev_map = global_reference -> ml_type option
63	63
64	64	val type_expand : abbrev_map -> ml_type -> ml_type
	65	val type_simpl : ml_type -> ml_type
65	66	val type_to_sign : abbrev_map -> ml_type -> sign
66	67	val type_to_signature : abbrev_map -> ml_type -> signature
67	68	val type_expunge : abbrev_map -> ml_type -> ml_type

115	116	val inline : global_reference -> ml_ast -> bool
116	117
117	118	exception Impossible
118		val check_function_branch : ml_branch -> ml_ast
119		val check_constant_branch : ml_branch -> ml_ast
	119	val branch_as_fun : ml_type list -> ml_branch -> ml_ast
	120	val branch_as_cst : ml_branch -> ml_ast
120	121
121	122	(* Classification of signatures *)
122	123

-4

plugins/extraction/modutil.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: modutil.ml 13420 2010-09-16 15:47:08Z letouzey $ i)
	8	(i $Id: modutil.ml 13733 2010-12-21 13:08:53Z letouzey $ i)
9	9
10	10	open Names
11	11	open Declarations

81	81	match a with
82	82	\| MLglob r -> do_term r
83	83	\| MLcons (i,r,_) ->
84		if lang () = Ocaml then record_iter_references do_term i;
	84	if lang () = Ocaml then record_iter_references do_term i.c_kind;
85	85	do_cons r
86	86	\| MLcase (i,_,v) ->
87		if lang () = Ocaml then record_iter_references do_term (fst i);
	87	if lang () = Ocaml then record_iter_references do_term i.m_kind;
88	88	Array.iter (fun (r,_,_) -> do_cons r) v
89	89	\| _ -> ()
90	90	in iter a

100	100	\| _ -> ());
101	101	Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types
102	102	in
103		if lang () = Ocaml then record_iter_references do_term ind.ind_info;
	103	if lang () = Ocaml then record_iter_references do_term ind.ind_kind;
104	104	Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets
105	105
106	106	let decl_iter_references do_term do_cons do_type =

+34

-28

plugins/extraction/ocaml.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: ocaml.ml 13323 2010-07-24 15:57:30Z herbelin $ i)
	8	(i $Id: ocaml.ml 13733 2010-12-21 13:08:53Z letouzey $ i)
9	9
10	10	(s Production of Ocaml syntax. )
11	11

217	217	when kn = ind_ascii && check_extract_ascii () & is_list_cons l ->
218	218	assert (args=[]);
219	219	pp_char l
220		\| MLcons (Coinductive,r,[]) ->
	220	\| MLcons ({c_kind = Coinductive},r,[]) ->
221	221	assert (args=[]);
222	222	pp_par par (str "lazy " ++ pp_global Cons r)
223		\| MLcons (Coinductive,r,args') ->
	223	\| MLcons ({c_kind = Coinductive},r,args') ->
224	224	assert (args=[]);
225	225	let tuple = pp_tuple (pp_expr true env []) args' in
226	226	pp_par par (str "lazy (" ++ pp_global Cons r ++ spc() ++ tuple ++str ")")
227	227	\| MLcons (_,r,[]) ->
228	228	assert (args=[]);
229	229	pp_global Cons r
230		\| MLcons (Record projs, r, args') ->
	230	\| MLcons ({c_kind = Record projs}, r, args') ->
231	231	assert (args=[]);
232	232	pp_record_pat (projs, List.map (pp_expr true env []) args')
233	233	\| MLcons (_,r,[arg1;arg2]) when is_infix r ->

249	249	hov 2 (str (find_custom_match pv) ++ fnl () ++
250	250	prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv
251	251	++ pp_expr true env [] t)
252		\| MLcase ((i,factors), t, pv) ->
253		let expr = if i = Coinductive then
	252	\| MLcase (info, t, pv) ->
	253	let expr = if info.m_kind = Coinductive then
254	254	(str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
255	255	else
256	256	(pp_expr false env [] t)
257	257	in
258	258	(try
259		let projs = find_projections i in
	259	let projs = find_projections info.m_kind in
260	260	let (_, ids, c) = pv.(0) in
261	261	let n = List.length ids in
262	262	match c with

276	276	\| _ -> raise NoRecord
277	277	with NoRecord ->
278	278	if Array.length pv = 1 then
279		let s1,s2 = pp_one_pat env i pv.(0) in
	279	let s1,s2 = pp_one_pat env info pv.(0) in
280	280	apply
281	281	(hv 0
282	282	(pp_par par'

290	290	(try pp_ifthenelse par' env expr pv
291	291	with Not_found ->
292	292	v 0 (str "match " ++ expr ++ str " with" ++ fnl () ++
293		str " \| " ++ pp_pat env (i,factors) pv))))
	293	str " \| " ++ pp_pat env info pv))))
294	294	\| MLfix (i,ids,defs) ->
295	295	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
296	296	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args

323	323	hov 2 (pp_expr (expr_needs_par els) env [] els)))
324	324	\| _ -> raise Not_found
325	325
326		and pp_one_pat env i (r,ids,t) =
	326	and pp_one_pat env info (r,ids,t) =
327	327	let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
328	328	let expr = pp_expr (expr_needs_par t) env' [] t in
329	329	try
330		let projs = find_projections i in
	330	let projs = find_projections info.m_kind in
331	331	pp_record_pat (projs, List.rev_map pr_id ids), expr
332	332	with NoRecord ->
333	333	(match List.rev ids with

339	339	++ pp_boxed_tuple pr_id ids),
340	340	expr
341	341
342		and pp_pat env (info,factors) pv =
343		let factor_br, factor_l = try match factors with
344		\| BranchFun (i::_ as l) -> check_function_branch pv.(i), l
345		\| BranchCst (i::_ as l) -> ast_pop (check_constant_branch pv.(i)), l
346		\| _ -> MLdummy, []
347		with Impossible -> MLdummy, []
348		in
349		let par = expr_needs_par factor_br in
	342	and pp_pat env info pv =
	343	let factor_br, factor_set = try match info.m_same with
	344	\| BranchFun ints ->
	345	let i = Intset.choose ints in
	346	branch_as_fun info.m_typs pv.(i), ints
	347	\| BranchCst ints ->
	348	let i = Intset.choose ints in
	349	ast_pop (branch_as_cst pv.(i)), ints
	350	\| BranchNone -> MLdummy, Intset.empty
	351	with _ -> MLdummy, Intset.empty
	352	in
350	353	let last = Array.length pv - 1 in
351	354	prvecti
352		(fun i x -> if List.mem i factor_l then mt () else
	355	(fun i x -> if Intset.mem i factor_set then mt () else
353	356	let s1,s2 = pp_one_pat env info x in
354	357	hov 2 (s1 ++ str " ->" ++ spc () ++ s2) ++
355		if i = last && factor_l = [] then mt () else
	358	if i = last && Intset.is_empty factor_set then mt () else
356	359	fnl () ++ str " \| ") pv
357	360	++
358		if factor_l = [] then mt () else match factors with
	361	if Intset.is_empty factor_set then mt () else
	362	let par = expr_needs_par factor_br in
	363	match info.m_same with
359	364	\| BranchFun _ ->
360		let ids, env' = push_vars [anonymous_name] env in
361		hov 2 (pr_id (List.hd ids) ++ str " ->" ++ spc () ++
362		pp_expr par env' [] factor_br)
	365	let ids, env' = push_vars [anonymous_name] env in
	366	hov 2 (pr_id (List.hd ids) ++ str " ->" ++ spc () ++
	367	pp_expr par env' [] factor_br)
363	368	\| BranchCst _ ->
364		hov 2 (str "_ ->" ++ spc () ++ pp_expr par env [] factor_br)
	369	hov 2 (str "_ ->" ++ spc () ++ pp_expr par env [] factor_br)
365	370	\| BranchNone -> mt ()
366	371
367	372	and pp_function env t =
368	373	let bl,t' = collect_lams t in
369	374	let bl,env' = push_vars (List.map id_of_mlid bl) env in
370	375	match t' with
371		\| MLcase(i,MLrel 1,pv) when fst i=Standard && not (is_custom_match pv) ->
	376	\| MLcase(i,MLrel 1,pv) when
	377	i.m_kind = Standard && not (is_custom_match pv) ->
372	378	if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then
373	379	pr_binding (List.rev (List.tl bl)) ++
374	380	str " = function" ++ fnl () ++

518	524	(s Pretty-printing of a declaration. )
519	525
520	526	let pp_mind kn i =
521		match i.ind_info with
	527	match i.ind_kind with
522	528	\| Singleton -> pp_singleton kn i.ind_packets.(0)
523	529	\| Coinductive -> pp_ind true kn i
524	530	\| Record projs ->

-6

plugins/extraction/scheme.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: scheme.ml 13323 2010-07-24 15:57:30Z herbelin $ i)
	8	(i $Id: scheme.ml 13733 2010-12-21 13:08:53Z letouzey $ i)
9	9
10	10	(s Production of Scheme syntax. )
11	11

86	86	++ spc () ++ hov 0 (pp_expr env' [] a2)))))
87	87	\| MLglob r ->
88	88	apply (pp_global Term r)
89		\| MLcons (i,r,args') ->
	89	\| MLcons (info,r,args') ->
90	90	assert (args=[]);
91	91	let st =
92	92	str "`" ++

94	94	(if args' = [] then mt () else spc ()) ++
95	95	prlist_with_sep spc (pp_cons_args env) args')
96	96	in
97		if i = Coinductive then paren (str "delay " ++ st) else st
	97	if info.c_kind = Coinductive then paren (str "delay " ++ st) else st
98	98	\| MLcase (_,t,pv) when is_custom_match pv ->
99	99	let mkfun (_,ids,e) =
100	100	if ids <> [] then named_lams (List.rev ids) e

103	103	hov 2 (str (find_custom_match pv) ++ fnl () ++
104	104	prvect (fun tr -> pp_expr env [] (mkfun tr) ++ fnl ()) pv
105	105	++ pp_expr env [] t)
106		\| MLcase ((i,_),t, pv) ->
	106	\| MLcase (info,t, pv) ->
107	107	let e =
108		if i <> Coinductive then pp_expr env [] t
	108	if info.m_kind <> Coinductive then pp_expr env [] t
109	109	else paren (str "force" ++ spc () ++ pp_expr env [] t)
110	110	in
111	111	apply (v 3 (paren (str "match " ++ e ++ fnl () ++ pp_pat env pv)))

122	122	\| MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"")
123	123
124	124	and pp_cons_args env = function
125		\| MLcons (i,r,args) when i<>Coinductive ->
	125	\| MLcons (info,r,args) when info.c_kind<>Coinductive ->
126	126	paren (pp_global Cons r ++
127	127	(if args = [] then mt () else spc ()) ++
128	128	prlist_with_sep spc (pp_cons_args env) args)

-2

plugins/extraction/table.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: table.ml 13420 2010-09-16 15:47:08Z letouzey $ i)
	8	(i $Id: table.ml 13733 2010-12-21 13:08:53Z letouzey $ i)
9	9
10	10	open Names
11	11	open Term

420	420	opt_lin_beta = kth_digit n 10 }
421	421
422	422	(* For the moment, we allow by default everything except :
423		- the type-unsafe optimization [opt_case_idg]
	423	- the type-unsafe optimization [opt_case_idg], which anyway
	424	cannot be activated currently (cf [Mlutil.branch_as_fun])
424	425	- the linear let and beta reduction [opt_lin_let] and [opt_lin_beta]
425	426	(may lead to complexity blow-up, subsumed by finer reductions
426	427	when inlining recursors).

-6

plugins/subtac/eterm.ml less more

27	27	ev_hyps: named_context;
28	28	ev_status: obligation_definition_status;
29	29	ev_chop: int option;
30		ev_loc: Util.loc;
	30	ev_source: hole_kind located;
31	31	ev_typ: types;
32	32	ev_tac: tactic option;
33	33	ev_deps: Intset.t }

217	217	else None
218	218	\| None -> None
219	219	in
220		let info = { ev_name = (n, nstr);
221		ev_hyps = hyps; ev_status = status; ev_chop = chop;
222		ev_loc = loc; ev_typ = evtyp ; ev_deps = deps; ev_tac = tac }
	220	let info = { ev_name = (n, nstr); ev_hyps = hyps;
	221	ev_status = status; ev_chop = chop;
	222	ev_source = (loc, k); ev_typ = evtyp ; ev_deps = deps; ev_tac = tac }
223	223	in (id, info) :: l)
224	224	evn []
225	225	in

230	230	let evars =
231	231	List.map (fun (ev, info) ->
232	232	let { ev_name = (_, name); ev_status = status;
233		ev_loc = loc; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
	233	ev_source = source; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
234	234	in
235	235	let status = match status with
236	236	\| Define true when Idset.mem name transparent -> Define false
237	237	\| _ -> status
238		in name, typ, loc, status, deps, tac) evts
	238	in name, typ, source, status, deps, tac) evts
239	239	in
240	240	let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in
241	241	let evmap f c = pi1 (subst_evar_constr evts 0 f c) in

-2

plugins/subtac/eterm.mli less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: eterm.mli 13323 2010-07-24 15:57:30Z herbelin $ i)
	8	(i $Id: eterm.mli 13693 2010-12-08 15:32:25Z msozeau $ i)
9	9	open Environ
10	10	open Tacmach
11	11	open Term

23	23	evars contexts, object and type *)
24	24	val eterm_obligations : env -> identifier -> evar_map -> evar_map -> int ->
25	25	?status:obligation_definition_status -> constr -> types ->
26		(identifier * types * loc * obligation_definition_status * Intset.t *
	26	(identifier * types * hole_kind located * obligation_definition_status * Intset.t *
27	27	tactic option) array
28	28	(* Existential key, obl. name, type as product, location of the original evar, associated tactic,
29	29	status and dependencies as indexes into the array *)

-6

plugins/subtac/subtac_obligations.ml less more

29	29	Some ident -> str "No obligations for program " ++ str (string_of_id ident)
30	30	\| None -> str "No obligations remaining"
31	31
32		type obligation_info = (Names.identifier * Term.types * loc * obligation_definition_status * Intset.t
33		* tactic option) array
	32	type obligation_info = (Names.identifier * Term.types * hole_kind located *
	33	obligation_definition_status * Intset.t * tactic option) array
34	34
35	35	type obligation =
36	36	{ obl_name : identifier;
37	37	obl_type : types;
38		obl_location : loc;
	38	obl_source : hole_kind located;
39	39	obl_body : constr option;
40	40	obl_status : obligation_definition_status;
41	41	obl_deps : Intset.t;

306	306	assert(obls = [\|\|]);
307	307	let n = Nameops.add_suffix n "_obligation" in
308	308	[\| { obl_name = n; obl_body = None;
309		obl_location = dummy_loc; obl_type = t;
	309	obl_source = (dummy_loc, QuestionMark Expand); obl_type = t;
310	310	obl_status = Expand; obl_deps = Intset.empty; obl_tac = None } \|],
311	311	mkVar n
312	312	\| Some b ->
313	313	Array.mapi
314	314	(fun i (n, t, l, o, d, tac) ->
315	315	{ obl_name = n ; obl_body = None;
316		obl_location = l; obl_type = reduce t; obl_status = o;
	316	obl_source = l; obl_type = reduce t; obl_status = o;
317	317	obl_deps = d; obl_tac = tac })
318	318	obls, b
319	319	in

487	487	\| Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
488	488	\| Stdpp.Exc_located(_, Refiner.FailError (_, s))
489	489	\| Refiner.FailError (_, s) ->
490		user_err_loc (obl.obl_location, "solve_obligation", Lazy.force s)
	490	user_err_loc (fst obl.obl_source, "solve_obligation", Lazy.force s)
491	491	\| e -> false
492	492
493	493	and solve_prg_obligations prg tac =

-2

plugins/subtac/subtac_obligations.mli less more

5	5	open Vernacexpr
6	6
7	7	type obligation_info =
8		(identifier * Term.types * loc *
	8	(identifier * Term.types * hole_kind located *
9	9	obligation_definition_status * Intset.t * tactic option) array
10		(* ident, type, location, (opaque or transparent, expand or define),
	10	(* ident, type, source, (opaque or transparent, expand or define),
11	11	dependencies, tactic to solve it *)
12	12
13	13	type progress = (* Resolution status of a program *)

-4

pretyping/cases.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: cases.ml 13511 2010-10-06 20:48:16Z herbelin $ *)
	8	(* $Id: cases.ml 13728 2010-12-19 11:35:20Z herbelin $ *)
9	9
10	10	open Util
11	11	open Names

1647	1647	let sigma2,pred2 = build_inversion_problem loc env !evdref tomatchs t in
1648	1648	[!evdref, KnownDep, pred1; sigma2, DepUnknown, pred2]
1649	1649	\| None, Some (None, t) ->
1650		(* Only one strategy: we build an "inversion" predicate *)
1651		let sigma,pred = build_inversion_problem loc env !evdref tomatchs t in
1652		[sigma, DepUnknown, pred]
	1650	(* First strategy: we build an "inversion" predicate *)
	1651	let sigma1,pred = build_inversion_problem loc env !evdref tomatchs t in
	1652	(* Second strategy: we abstract the tycon wrt to the dependencies *)
	1653	let pred2 = lift (List.length names) t in
	1654	[sigma1, DepUnknown, pred; !evdref, KnownNotDep, pred2]
1653	1655	\| None, _ ->
1654	1656	(* No type constaints: we use two strategies *)
1655	1657	let t = mkExistential env ~src:(loc, CasesType) evdref in

+25

-7

tactics/equality.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: equality.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
	8	(* $Id: equality.ml 13586 2010-10-27 17:42:13Z jforest $ *)
9	9
10	10	open Pp
11	11	open Util

184	184	pf_conv_x gl (List.nth args 0) (List.nth args 2)) && not dep
185	185	\|\| Flags.version_less_or_equal Flags.V8_2
186	186	then
187		(* use eq_rect, eq_rect_r, JMeq_rect, etc for compatibility *)
188		let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
189		let hdcncls = string_of_inductive hdcncl ^ suffix in
190		let rwr_thm = if lft2rgt = Some (cls=None) then hdcncls^"_r" else hdcncls in
191		try pf_global gl (id_of_string rwr_thm)
192		with Not_found -> error ("Cannot find rewrite principle "^rwr_thm^".")
	187	match kind_of_term hdcncl with
	188	\| Ind ind_sp ->
	189	let pr1 =
	190	lookup_eliminator ind_sp (elimination_sort_of_clause cls gl)
	191	in
	192	if lft2rgt = Some (cls=None)
	193	then
	194	let c1 = destConst pr1 in
	195	let mp,dp,l = repr_con (constant_of_kn (canonical_con c1)) in
	196	let l' = label_of_id (add_suffix (id_of_label l) "_r") in
	197	let c1' = Global.constant_of_delta (make_con mp dp l') in
	198	begin
	199	try
	200	let _ = Global.lookup_constant c1' in
	201	mkConst c1'
	202	with Not_found ->
	203	let rwr_thm = string_of_label l' in
	204	error ("Cannot find rewrite principle "^rwr_thm^".")
	205	end
	206	else pr1
	207	\| _ ->
	208	(* cannot occur since we checked that we are in presence of
	209	Logic.eq or Jmeq just before *)
	210	assert false
193	211	else
194	212	let scheme_name = match dep, lft2rgt, inccl with
195	213	(* Non dependent case with symmetric equality *)

+38

-5

tactics/extratactics.ml4 less more

7	7
8	8	(i camlp4deps: "parsing/grammar.cma" i)
9	9
10		(* $Id: extratactics.ml4 13434 2010-09-18 20:11:37Z msozeau $ *)
	10	(* $Id: extratactics.ml4 13658 2010-11-29 11:09:05Z glondu $ *)
11	11
12	12	open Pp
13	13	open Pcoq

544	544	\| RVar (_,id) as x ->
545	545	if id = tid
546	546	then (decr occref; if !occref = 0 then x
547		else (incr locref; RHole (Ploc.make !locref 0 (0,0),Evd.QuestionMark(Evd.Define true))))
	547	else (incr locref; RHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true))))
548	548	else x
549	549	\| c -> map_rawconstr_left_to_right substrec c in
550	550	let t' = substrec t

557	557	let rec substrec = function
558	558	\| RHole (_,Evd.QuestionMark(Evd.Define true)) ->
559	559	decr occref; if !occref = 0 then tc
560		else (incr locref; RHole (Ploc.make !locref 0 (0,0),Evd.QuestionMark(Evd.Define true)))
	560	else (incr locref; RHole (make_loc (!locref,0),Evd.QuestionMark(Evd.Define true)))
561	561	\| c -> map_rawconstr_left_to_right substrec c
562	562	in
563	563	substrec t

579	579	try
580	580	Pretyping.Default.understand sigma env t_hole
581	581	with
582		\| Ploc.Exc (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) ->
583		resolve_hole (subst_hole_with_term (Ploc.line_nb loc) c_raw t_hole)
	582	\| Stdpp.Exc_located (loc,Pretype_errors.PretypeError (_, Pretype_errors.UnsolvableImplicit _)) ->
	583	resolve_hole (subst_hole_with_term (fst (unloc loc)) c_raw t_hole)
584	584	in
585	585	let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in
586	586	let t_constr_type = Retyping.get_type_of env sigma t_constr in

628	628	\| [ "constr_eq" constr(x) constr(y) ] -> [
629	629	if eq_constr x y then tclIDTAC else tclFAIL 0 (str "Not equal") ]
630	630	END
	631
	632	TACTIC EXTEND is_evar
	633	\| [ "is_evar" constr(x) ] ->
	634	[ match kind_of_term x with
	635	\| Evar _ -> tclIDTAC
	636	\| _ -> tclFAIL 0 (str "Not an evar")
	637	]
	638	END
	639
	640	let rec has_evar x =
	641	match kind_of_term x with
	642	\| Evar _ -> true
	643	\| Rel _ \| Var _ \| Meta _ \| Sort _ \| Const _ \| Ind _ \| Construct _ ->
	644	false
	645	\| Cast (t1, _, t2) \| Prod (_, t1, t2) \| Lambda (_, t1, t2) ->
	646	has_evar t1 \|\| has_evar t2
	647	\| LetIn (_, t1, t2, t3) ->
	648	has_evar t1 \|\| has_evar t2 \|\| has_evar t3
	649	\| App (t1, ts) ->
	650	has_evar t1 \|\| has_evar_array ts
	651	\| Case (_, t1, t2, ts) ->
	652	has_evar t1 \|\| has_evar t2 \|\| has_evar_array ts
	653	\| Fix ((_, tr)) \| CoFix ((_, tr)) ->
	654	has_evar_prec tr
	655	and has_evar_array x =
	656	array_exists has_evar x
	657	and has_evar_prec (_, ts1, ts2) =
	658	array_exists has_evar ts1 \|\| array_exists has_evar ts2
	659
	660	TACTIC EXTEND has_evar
	661	\| [ "has_evar" constr(x) ] ->
	662	[ if has_evar x then tclIDTAC else tclFAIL 0 (str "No evars") ]
	663	END

-7

tactics/rewrite.ml4 less more

595	595	let prf =
596	596	mkApp (Lazy.force coq_f_equal,
597	597	[\| r.rew_car; ty;
598		mkLambda (Anonymous, r.rew_car, c (mkRel 1));
	598	mkLambda (Anonymous, r.rew_car, c);
599	599	r.rew_from; r.rew_to; prf \|])
600	600	in RewPrf (rel, prf)
601	601	\| RewCast k -> r.rew_prf
602	602	in
603	603	{ r with rew_car = ty;
604		rew_from = c r.rew_from; rew_to = c r.rew_to; rew_prf = prf }
	604	rew_from = subst1 r.rew_from c; rew_to = subst1 r.rew_to c; rew_prf = prf }
605	605
606	606	open Elimschemes
607	607

771	771	let c' = s env sigma c cty cstr' evars in
772	772	(match c' with
773	773	\| Some (Some r) ->
774		Some (Some (make_leibniz_proof (fun x -> mkCase (ci, p, x, brs)) ty r))
	774	Some (Some (make_leibniz_proof (mkCase (ci, lift 1 p, mkRel 1, Array.map (lift 1) brs)) ty r))
775	775	\| x ->
776	776	if array_for_all ((=) 0) ci.ci_cstr_nargs then
777	777	let cstr = Some (mkApp (Lazy.force coq_eq, [\| ty \|])) in
778	778	let found, brs' = Array.fold_left (fun (found, acc) br ->
779		if found <> None then (found, fun x -> br :: acc x)
	779	if found <> None then (found, fun x -> lift 1 br :: acc x)
780	780	else
781	781	match s env sigma br ty cstr evars with
782		\| Some (Some r) -> (Some r, fun x -> x :: acc x)
783		\| _ -> (None, fun x -> br :: acc x))
	782	\| Some (Some r) -> (Some r, fun x -> mkRel 1 :: acc x)
	783	\| _ -> (None, fun x -> lift 1 br :: acc x))
784	784	(None, fun x -> []) brs
785	785	in
786	786	match found with
787	787	\| Some r ->
788		let ctxc x = mkCase (ci, p, c, Array.of_list (List.rev (brs' x))) in
	788	let ctxc = mkCase (ci, lift 1 p, lift 1 c, Array.of_list (List.rev (brs' x))) in
789	789	Some (Some (make_leibniz_proof ctxc ty r))
790	790	\| None -> x
791	791	else

-4

tactics/tactics.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: tactics.ml 13464 2010-09-24 22:23:02Z herbelin $ *)
	8	(* $Id: tactics.ml 13693 2010-12-08 15:32:25Z msozeau $ *)
9	9
10	10	open Pp
11	11	open Util

2364	2364	in
2365	2365	let f', args' = decompose_indapp f args in
2366	2366	let parvars = ids_of_constr ~all:true Idset.empty f' in
	2367	let seen = ref parvars in
2367	2368	let dogen, f', args' =
2368		let seen = ref parvars in
2369	2369	let find i x = not (isVar x) \|\|
2370	2370	let v = destVar x in
2371	2371	if is_defined_variable env v \|\| Idset.mem v !seen then true

2378	2378	true, mkApp (f', before), after
2379	2379	in
2380	2380	if dogen then
2381		let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env =
2382		Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],parvars,Idset.empty,env) args'
	2381	let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env =
	2382	Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],!seen,Idset.empty,env) args'
2383	2383	in
2384	2384	let args, refls = List.rev args, List.rev refls in
2385	2385	let vars =

-1

test-suite/Makefile less more

39	39
40	40	command := $(coqtop) -top Top -load-vernac-source
41	41	coqc := $(coqtop) -compile
42		coqdep := $(BIN)coqdep
	42	coqdep := $(BIN)coqdep -coqlib $(LIB)
43	43
44	44	SHOW := $(if $(VERBOSE),@true,@echo)
45	45	HIDE := $(if $(VERBOSE),,@)

-6

test-suite/bugs/closed/shouldsucceed/2388.v less more

1	1
2	2	Fail Parameters (A:Prop) (a:A A).
3	3
4		(* This is a variant (reported as part of bug #2347) *)
5
6		Require Import EquivDec.
7		Fail Program Instance bool_eq_eqdec : EqDec bool eq :=
8		{equiv_dec x y := (fix aux (x y : bool) {struct x}:= aux _ y) x y}.
9

+52

-0

test-suite/output/Extraction_matchs_2413.out less more

	0	( val test1 : bool -> bool )
	1
	2	let test1 b =
	3	b
	4	( val test2 : bool -> bool )
	5
	6	let test2 b =
	7	False
	8	( val wrong_id : 'a1 hole -> 'a2 hole )
	9
	10	let wrong_id = function
	11	\| Hole -> Hole
	12	\| Hole2 -> Hole2
	13	( val test3 : 'a1 option -> 'a1 option )
	14
	15	let test3 o =
	16	o
	17	( val test4 : indu -> indu )
	18
	19	let test4 = function
	20	\| A m -> A (S m)
	21	\| x -> x
	22	( val test5 : indu -> indu )
	23
	24	let test5 = function
	25	\| A m -> A (S m)
	26	\| _ -> B
	27	( val test6 : indu' -> indu' )
	28
	29	let test6 = function
	30	\| A' m -> A' (S m)
	31	\| E' -> B'
	32	\| F' -> B'
	33	\| _ -> C'
	34	( val test7 : indu -> nat option )
	35
	36	let test7 = function
	37	\| A m -> Some m
	38	\| _ -> None
	39	(** val decode_cond_mode :
	40	(word -> opcode option) -> (word -> 'a1 decoder_result) -> word -> ('a1
	41	-> opcode -> 'a2) -> 'a2 decoder_result **)
	42
	43	let decode_cond_mode condition f w g =
	44	match condition w with
	45	\| Some oc ->
	46	(match f w with
	47	\| DecUndefined -> DecUndefined
	48	\| DecUnpredictable -> DecUnpredictable
	49	\| DecInst i -> DecInst (g i oc)
	50	\| DecError m -> DecError m)
	51	\| None -> DecUndefined

+128

-0

test-suite/output/Extraction_matchs_2413.v less more

	0	(** Extraction : tests of optimizations of pattern matching *)
	1
	2	(** First, a few basic tests *)
	3
	4	Definition test1 b :=
	5	match b with
	6	\| true => true
	7	\| false => false
	8	end.
	9
	10	Extraction test1. (** should be seen as the identity *)
	11
	12	Definition test2 b :=
	13	match b with
	14	\| true => false
	15	\| false => false
	16	end.
	17
	18	Extraction test2. (** should be seen a the always-false constant function *)
	19
	20	Inductive hole (A:Set) : Set := Hole \| Hole2.
	21
	22	Definition wrong_id (A B : Set) (x:hole A) : hole B :=
	23	match x with
	24	\| Hole => @Hole _
	25	\| Hole2 => @Hole2 _
	26	end.
	27
	28	Extraction wrong_id. (** should _not_ be optimized as an identity *)
	29
	30	Definition test3 (A:Type)(o : option A) :=
	31	match o with
	32	\| Some x => Some x
	33	\| None => None
	34	end.
	35
	36	Extraction test3. (** Even with type parameters, should be seen as identity *)
	37
	38	Inductive indu : Type := A : nat -> indu \| B \| C.
	39
	40	Definition test4 n :=
	41	match n with
	42	\| A m => A (S m)
	43	\| B => B
	44	\| C => C
	45	end.
	46
	47	Extraction test4. (** should merge branchs B C into a x->x *)
	48
	49	Definition test5 n :=
	50	match n with
	51	\| A m => A (S m)
	52	\| B => B
	53	\| C => B
	54	end.
	55
	56	Extraction test5. (** should merge branches B C into _->B *)
	57
	58	Inductive indu' : Type := A' : nat -> indu' \| B' \| C' \| D' \| E' \| F'.
	59
	60	Definition test6 n :=
	61	match n with
	62	\| A' m => A' (S m)
	63	\| B' => C'
	64	\| C' => C'
	65	\| D' => C'
	66	\| E' => B'
	67	\| F' => B'
	68	end.
	69
	70	Extraction test6. (** should merge some branches into a _->C' *)
	71
	72	(** NB : In Coq, "\| a => a" corresponds to n, hence some "\| _ -> n" are
	73	extracted *)
	74
	75	Definition test7 n :=
	76	match n with
	77	\| A m => Some m
	78	\| B => None
	79	\| C => None
	80	end.
	81
	82	Extraction test7. (** should merge branches B,C into a _->None *)
	83
	84	(** Script from bug #2413 *)
	85
	86	Set Implicit Arguments.
	87
	88	Section S.
	89
	90	Definition message := nat.
	91	Definition word := nat.
	92	Definition mode := nat.
	93	Definition opcode := nat.
	94
	95	Variable condition : word -> option opcode.
	96
	97	Section decoder_result.
	98
	99	Variable inst : Type.
	100
	101	Inductive decoder_result : Type :=
	102	\| DecUndefined : decoder_result
	103	\| DecUnpredictable : decoder_result
	104	\| DecInst : inst -> decoder_result
	105	\| DecError : message -> decoder_result.
	106
	107	End decoder_result.
	108
	109	Definition decode_cond_mode (mode : Type) (f : word -> decoder_result mode)
	110	(w : word) (inst : Type) (g : mode -> opcode -> inst) :
	111	decoder_result inst :=
	112	match condition w with
	113	\| Some oc =>
	114	match f w with
	115	\| DecInst i => DecInst (g i oc)
	116	\| DecError m => @DecError inst m
	117	\| DecUndefined => @DecUndefined inst
	118	\| DecUnpredictable => @DecUnpredictable inst
	119	end
	120	\| None => @DecUndefined inst
	121	end.
	122
	123	End S.
	124
	125	Extraction decode_cond_mode.
	126	(** inner match should not be factorized with a partial x->x (different type) *)
	127

-6

theories/Numbers/Natural/BigN/NMake_gen.ml less more

7	7	(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
8	8	(************************************************************************)
9	9
10		(i $Id: NMake_gen.ml 13323 2010-07-24 15:57:30Z herbelin $ i)
	10	(i $Id: NMake_gen.ml 13734 2010-12-21 18:21:56Z letouzey $ i)
11	11
12	12	(S NMake_gen.ml : this file generates NMake.v )
13	13

1298	1298	pr " (iter _";
1299	1299	for i = 0 to size do
1300	1300	pr " compare_%i" i;
1301		pr " (fun n x y => opp_compare (comparen_%i (S n) y x))" i;
	1301	pr " (fun n x y => CompOpp (comparen_%i (S n) y x))" i;
1302	1302	pr " (fun n => comparen_%i (S n))" i;
1303	1303	done;
1304	1304	pr " comparenm).";

1338	1338
1339	1339	pp " Let spec_opp_compare: forall c (u v: Z),";
1340	1340	pp " match c with Eq => u = v \| Lt => u < v \| Gt => u > v end ->";
1341		pp " match opp_compare c with Eq => v = u \| Lt => v < u \| Gt => v > u end.";
1342		pp " Proof.";
1343		pp " intros c u v; case c; unfold opp_compare; auto with zarith.";
	1341	pp " match CompOpp c with Eq => v = u \| Lt => v < u \| Gt => v > u end.";
	1342	pp " Proof.";
	1343	pp " intros c u v; case c; unfold CompOpp; auto with zarith.";
1344	1344	pp " Qed.";
1345	1345	pp "";
1346	1346

1361	1361	pp " end)";
1362	1362	for i = 0 to size do
1363	1363	pp " compare_%i" i;
1364		pp " (fun n x y => opp_compare (comparen_%i (S n) y x))" i;
	1364	pp " (fun n x y => CompOpp (comparen_%i (S n) y x))" i;
1365	1365	pp " (fun n => comparen_%i (S n)) _ _ _" i;
1366	1366	done;
1367	1367	pp " comparenm _).";

-9

theories/Numbers/Natural/BigN/Nbasic.v less more

7	7	(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
8	8	(************************************************************************)
9	9
10		(i $Id: Nbasic.v 13323 2010-07-24 15:57:30Z herbelin $ i)
	10	(i $Id: Nbasic.v 13734 2010-12-21 18:21:56Z letouzey $ i)
11	11
12	12	Require Import ZArith.
13	13	Require Import BigNumPrelude.

258	258	end.
259	259
260	260	End ReduceRec.
261
262		Definition opp_compare cmp :=
263		match cmp with
264		\| Lt => Gt
265		\| Eq => Eq
266		\| Gt => Lt
267		end.
268	261
269	262	Section CompareRec.
270	263

446	439	\| Lt => y < x
447	440	\| Gt => y > x
448	441	end ->
449		match opp_compare u with
	442	match CompOpp u with
450	443	\| Eq => x = y
451	444	\| Lt => x < y
452	445	\| Gt => x > y

+21

-5

theories/Program/Equality.v less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: Equality.v 13492 2010-10-04 21:20:01Z herbelin $ i)
	8	(i $Id: Equality.v 13730 2010-12-19 13:32:01Z msozeau $ i)
9	9
10	10	(** Tactics related to (dependent) equality and proof irrelevance. *)
11	11

319	319	constructor forms). Compare with the lemma 16 of the paper.
320	320	We don't have a [noCycle] procedure yet. *)
321	321
	322	Ltac block_equality id :=
	323	match type of id with
	324	\| @eq ?A ?t ?u => change (block (@eq A t u)) in id
	325	\| _ => idtac
	326	end.
	327
	328	Ltac revert_blocking_until id :=
	329	Tactics.on_last_hyp ltac:(fun id' =>
	330	match id' with
	331	\| id => idtac
	332	\| _ => block_equality id' ; revert id' ; revert_blocking_until id
	333	end).
	334
322	335	Ltac simplify_one_dep_elim_term c :=
323	336	match c with
324	337	\| @JMeq _ _ _ _ -> _ => refine (simplification_heq _ _ _ _ _)
325	338	\| ?t = ?t -> _ => intros _ \|\| refine (simplification_K _ t _ _)
326		\| eq (existT _ _ _) (existT _ _ _) -> _ =>
	339	\| eq (existT _ ?p _) (existT _ ?q _) -> _ =>
327	340	refine (simplification_existT2 _ _ _ _ _ _ _) \|\|
328		refine (simplification_existT1 _ _ _ _ _ _ _ _)
	341	match goal with
	342	\| H : p = q \|- _ => intro
	343	\| _ => refine (simplification_existT1 _ _ _ _ _ _ _ _)
	344	end
329	345	\| ?x = ?y -> _ => (* variables case *)
330	346	(let hyp := fresh in intros hyp ;
331		move hyp before x ; revert_until hyp ; generalize dependent x ;
	347	move hyp before x ; revert_blocking_until hyp ; generalize dependent x ;
332	348	refine (solution_left _ _ _ _)(* ; intros until 0 *)) \|\|
333	349	(let hyp := fresh in intros hyp ;
334		move hyp before y ; revert_until hyp ; generalize dependent y ;
	350	move hyp before y ; revert_blocking_until hyp ; generalize dependent y ;
335	351	refine (solution_right _ _ _ _)(* ; intros until 0 *))
336	352	\| ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; injection H ; clear H)
337	353	\| ?t = ?u -> _ => let hyp := fresh in

+10

-7

theories/Program/Tactics.v less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: Tactics.v 13332 2010-07-26 22:12:43Z msozeau $ i)
	8	(i $Id: Tactics.v 13693 2010-12-08 15:32:25Z msozeau $ i)
9	9
10	10	(** This module implements various tactics used to simplify the goals produced by Program,
11	11	which are also generally useful. *)

307	307	subst*; autoinjections ; try discriminates ;
308	308	try (solve [ red ; intros ; destruct_conjs ; autoinjections ; discriminates ]).
309	309
310		Ltac program_solve_wf :=
311		match goal with
312		\|- well_founded _ => auto with *
313		end.
314
315		Ltac program_simpl := program_simplify ; auto; try program_solve_wf.
	310	(** We only try to solve proposition goals automatically. *)
	311
	312	Ltac program_solve :=
	313	match goal with
	314	\| \|- well_founded _ => auto with *
	315	\| \|- ?T => match type of T with Prop => auto end
	316	end.
	317
	318	Ltac program_simpl := program_simplify ; try program_solve.
316	319
317	320	Obligation Tactic := program_simpl.

-2

theories/Sorting/Mergesort.v less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: Mergesort.v 13323 2010-07-24 15:57:30Z herbelin $ i)
	8	(i $Id: Mergesort.v 13678 2010-12-04 10:34:28Z herbelin $ i)
9	9
10	10	(** A modular implementation of mergesort (the complexity is O(n.log n) in
11	11	the length of the list) *)

60	60
61	61	For instance, here is how [6;2;3;1;5] is sorted:
62	62
	63	<<
63	64	operation stack list
64	65	iter_merge [] [6;2;3;1;5]
65	66	= append_list_to_stack [ + [6]] [2;3;1;5]

76	77	= append_list_to_stack [[1;2;3;6];; + [5]] []
77	78	-> merge_stack [[1;2;3;6];;[5]]
78	79	= [1;2;3;5;6]
79
	80	>>
80	81	The complexity of the algorithm is n*log n, since there are
81	82	2^(p-1) mergings to do of length 2, 2^(p-2) of length 4, ..., 2^0
82	83	of length 2^p for a list of length 2^p. The algorithm does not need

+11

-12

theories/ZArith/BinInt.v less more

6	6	(* * GNU Lesser General Public License Version 2.1 *)
7	7	(************************************************************************)
8	8
9		(i $Id: BinInt.v 13323 2010-07-24 15:57:30Z herbelin $ i)
	9	(i $Id: BinInt.v 13697 2010-12-09 18:48:04Z herbelin $ i)
10	10
11	11	(***********************************************************)
12	12	(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)

222	222
223	223
224	224	(**********************************************************************)
225
226	225	( Properties of opposite on binary integer numbers *)
227	226
228	227	Theorem Zopp_0 : Zopp Z0 = Z0.

269	268	(**********************************************************************)
270	269	(** * Properties of the addition on integers *)
271	270
272		( zero is left neutral for addition *)
	271	( Zero is left neutral for addition *)
273	272
274	273	Theorem Zplus_0_l : forall n:Z, Z0 + n = n.
275	274	Proof.
276	275	intro x; destruct x; reflexivity.
277	276	Qed.
278	277
279		( * zero is right neutral for addition *)
	278	( Zero is right neutral for addition *)
280	279
281	280	Theorem Zplus_0_r : forall n:Z, n + Z0 = n.
282	281	Proof.
283	282	intro x; destruct x; reflexivity.
284	283	Qed.
285	284
286		( addition is commutative *)
	285	( Addition is commutative *)
287	286
288	287	Theorem Zplus_comm : forall n m:Z, n + m = m + n.
289	288	Proof.

295	294	rewrite Pplus_comm; reflexivity.
296	295	Qed.
297	296
298		( opposite distributes over addition *)
	297	( Opposite distributes over addition *)
299	298
300	299	Theorem Zopp_plus_distr : forall n m:Z, - (n + m) = - n + - m.
301	300	Proof.

309	308	intro; unfold Zsucc; now rewrite Zopp_plus_distr.
310	309	Qed.
311	310
312		( opposite is inverse for addition *)
	311	( Opposite is inverse for addition *)
313	312
314	313	Theorem Zplus_opp_r : forall n:Z, n + - n = Z0.
315	314	Proof.

326	325
327	326	Hint Local Resolve Zplus_0_l Zplus_0_r.
328	327
329		( addition is associative *)
	328	( Addition is associative *)
330	329
331	330	Lemma weak_assoc :
332	331	forall (p q:positive) (n:Z), Zpos p + (Zpos q + n) = Zpos p + Zpos q + n.

494	493	rewrite (Zplus_comm p n); trivial with arith.
495	494	Qed.
496	495
497		( addition simplifies *)
	496	( Addition simplifies *)
498	497
499	498	Theorem Zplus_reg_l : forall n m p:Z, n + m = n + p -> m = p.
500	499	intros n m p H; cut (- n + (n + m) = - n + (n + p));

503	502	\| rewrite H; trivial with arith ].
504	503	Qed.
505	504
506		( addition and successor permutes *)
	505	( Addition and successor permutes *)
507	506
508	507	Lemma Zplus_succ_l : forall n m:Z, Zsucc n + m = Zsucc (n + m).
509	508	Proof.

574	573	trivial with arith.
575	574	Qed.
576	575
577		(** successor and predecessor are inverse functions *)
	576	( Successor and predecessor are inverse functions *)
578	577
579	578	Theorem Zsucc_pred : forall n:Z, n = Zsucc (Zpred n).
580	579	Proof.

599	598	Qed.
600	599
601	600	(*************************************************************************)
602		( Properties of the direct definition of successor and predecessor *)
	601	( Properties of the direct definition of successor and predecessor *)
603	602
604	603	Theorem Zsucc_succ' : forall n:Z, Zsucc n = Zsucc' n.
605	604	Proof.

-4

tools/coqdoc/coqdoc.sty less more

82	82	\newcommand{\coqdocnotation}[1]{\coqdockw{#1}}
83	83	\newcommand{\coqdocsection}[1]{\coqdoccst{#1}}
84	84	\newcommand{\coqdocaxiom}[1]{\coqdocax{#1}}
85		\newcommand{\coqdocmoduleid}[1]{\coqdocmod{#1}}
	85	\newcommand{\coqdocmodule}[1]{\coqdocmod{#1}}
86	86
87	87	% Environment encompassing code fragments
88	88	% !!! CAUTION: This environment may have empty contents

106	106	% Empty lines (in code only)
107	107	\newcommand{\coqdocemptyline}{\vskip 0.4em plus 0.1em minus 0.1em}
108	108
109		% macro for typesetting the title of a module implementation
110		\newcommand{\coqdocmodule}[1]{\chapter{Module #1}\markboth{Module #1}{}
111		}
112	109	\usepackage{ifpdf}
113	110	\ifpdf
114	111	\RequirePackage{hyperref}

+10

-3

tools/coqdoc/cpretty.mll less more

6	6	(* * GNU Lesser General Public License Version 2.1 *)
7	7	(************************************************************************)
8	8
9		(i $Id: cpretty.mll 13440 2010-09-19 20:21:12Z herbelin $ i)
	9	(i $Id: cpretty.mll 13692 2010-12-06 23:55:10Z herbelin $ i)
10	10
11	11	(s Utility functions for the scanners )
12	12

271	271	(* superscript 1 *)
272	272	'\194' '\185' \|
273	273	(* utf-8 latin 1 supplement *)
274		'\195' ['\128'-'\191'] \|
	274	'\195' ['\128'-'\150'] \|
	275	'\195' ['\152'-'\182'] \|
	276	'\195' ['\184'-'\191'] \|
275	277	(* utf-8 letterlike symbols *)
276	278	(* '\206' ([ '\145' - '\183'] \| '\187') \| *)
277	279	(* '\xCF' [ '\x00' - '\xCE' ] \| *)

314	316	\| "Class"
315	317	\| "SubClass"
316	318	\| "Example"
317		\| "Local"
318	319	\| "Fixpoint"
319	320	\| "Boxed"
320	321	\| "CoFixpoint"

449	450	{ begin_show (); coq_bol lexbuf }
450	451	\| space* end_show
451	452	{ end_show (); coq_bol lexbuf }
	453	\| space* ("Local"\|"Global")
	454	{
	455	in_proof := None;
	456	let s = lexeme lexbuf in
	457	output_indented_keyword s lexbuf;
	458	coq_bol lexbuf }
452	459	\| space* gallina_kw_to_hide
453	460	{ let s = lexeme lexbuf in
454	461	if !Cdglobals.light && section_or_end s then

+34

-12

tools/coqdoc/index.ml less more

6	6	(* * GNU Lesser General Public License Version 2.1 *)
7	7	(************************************************************************)
8	8
9		(i $Id: index.ml 13323 2010-07-24 15:57:30Z herbelin $ i)
	9	(i $Id: index.ml 13676 2010-12-04 10:34:21Z herbelin $ i)
10	10
11	11	open Filename
12	12	open Lexing

215	215	\| Library ->
216	216	let ln = !lib_name in
217	217	if ln <> "" then String.lowercase ln else "library"
218		\| Module -> "moduleid"
	218	\| Module -> "module"
219	219	\| Definition -> "definition"
220	220	\| Inductive -> "inductive"
221	221	\| Constructor -> "constructor"

234	234
235	235	let prepare_entry s = function
236	236	\| Notation ->
237		(* Notations have conventially the form section.:sc:x_++_'x'_x *)
	237	(* We decode the encoding done in Dumpglob.cook_notation of coqtop *)
	238	(* Encoded notations have the form section:sc:x_'++'_x where: *)
	239	(* - the section, if any, ends with a "." *)
	240	(* - the scope can be empty *)
	241	(* - tokens are separated with "_" *)
	242	(* - non-terminal symbols are conventionally represented by "x" *)
	243	(* - terminals are enclosed within simple quotes *)
	244	(* - existing simple quotes (that necessarily are parts of terminals) *)
	245	(* are doubled *)
	246	(* (as a consequence, when a terminal contains "_" or "x", these *)
	247	(* necessarily appear enclosed within non-doubled simple quotes) *)
	248	(* Example: "x ' %x _% y %'x %'_' z" is encoded as *)
	249	(* "x_''''_'%x'_'_%'_x_'%''x'_'%''_'''_x" *)
238	250	let err () = eprintf "Invalid notation in globalization file\n"; exit 1 in
239	251	let h = try String.index_from s 0 ':' with _ -> err () in
240	252	let i = try String.index_from s (h+1) ':' with _ -> err () in
241	253	let sc = String.sub s (h+1) (i-h-1) in
242		let ntn = String.make (String.length s) ' ' in
	254	let ntn = String.make (String.length s - i) ' ' in
243	255	let k = ref 0 in
244	256	let j = ref (i+1) in
245	257	let quoted = ref false in
246		while !j <> String.length s do
247		if s.[!j] = '_' && not !quoted then ntn.[!k] <- ' ' else
248		if s.[!j] = 'x' && not !quoted then ntn.[!k] <- '_' else
249		if s.[!j] = '\'' then
250		if s.[!j+1] = 'x' && s.[!j+1] = '\'' then (ntn.[!k] <- 'x'; j:=!j+2)
251		else (quoted := not !quoted; ntn.[!k] <- '\'')
252		else ntn.[!k] <- s.[!j];
253		incr j; incr k
	258	let l = String.length s - 1 in
	259	while !j <= l do
	260	if not !quoted then begin
	261	(match s.[!j] with
	262	\| '_' -> ntn.[!k] <- ' '; incr k
	263	\| 'x' -> ntn.[!k] <- '_'; incr k
	264	\| '\'' -> quoted := true
	265	\| _ -> assert false)
	266	end
	267	else
	268	if s.[!j] = '\'' then begin
	269	if (!j = l \|\| s.[!j+1] <> '\'') then quoted := false
	270	else (ntn.[!k] <- s.[!j]; incr k; incr j)
	271	end else begin
	272	ntn.[!k] <- s.[!j];
	273	incr k
	274	end;
	275	incr j
254	276	done;
255	277	let ntn = String.sub ntn 0 !k in
256	278	if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")"

-2

tools/coqdoc/output.ml less more

6	6	(* * GNU Lesser General Public License Version 2.1 *)
7	7	(************************************************************************)
8	8
9		(i $Id: output.ml 13541 2010-10-13 19:53:29Z notin $ i)
	9	(i $Id: output.ml 13676 2010-12-04 10:34:21Z herbelin $ i)
10	10
11	11	open Cdglobals
12	12	open Index

286	286	printf "\\coqdocindent{%2.2fem}\n" space
287	287
288	288	let module_ref m s =
289		printf "\\moduleid{%s}{%s}" m (escaped s)
	289	printf "\\coqdocmodule{%s}{%s}" m (escaped s)
290	290
291	291	let ident_ref m fid typ s =
292	292	let id = if fid <> "" then (m ^ "." ^ fid) else m in

+10

-3

toplevel/cerrors.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: cerrors.ml 13431 2010-09-18 08:15:29Z herbelin $ *)
	8	(* $Id: cerrors.ml 13639 2010-11-16 15:36:01Z glondu $ *)
9	9
10	10	open Pp
11	11	open Util

80	80	hov 0 (str "Syntax error: Undefined token.")
81	81	\| Lexer.Error (Bad_token s) ->
82	82	hov 0 (str "Syntax error: Bad token" ++ spc () ++ str s ++ str ".")
	83	\| Stdpp.Exc_located (loc,exc) ->
	84	hov 0 ((if loc = dummy_loc then (mt ())
	85	else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
	86	++ explain_exn_default_aux anomaly_string report_fn exc)
83	87	\| Assert_failure (s,b,e) ->
84	88	hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
85	89	(if s <> "" then

166	170	let raise_if_debug e =
167	171	if !Flags.debug then raise e
168	172
169		let _ = Tactic_debug.explain_logic_error := explain_exn_default
	173	let _ = Tactic_debug.explain_logic_error :=
	174	(fun e -> explain_exn_default (process_vernac_interp_error e))
170	175
171	176	let _ = Tactic_debug.explain_logic_error_no_anomaly :=
172		explain_exn_default_aux (fun () -> mt()) (fun () -> str ".")
	177	(fun e ->
	178	explain_exn_default_aux (fun () -> mt()) (fun () -> str ".")
	179	(process_vernac_interp_error e))
173	180
174	181	let explain_exn_function = ref explain_exn_default
175	182

-3

toplevel/command.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: command.ml 13344 2010-07-28 15:04:36Z msozeau $ *)
	8	(* $Id: command.ml 13672 2010-12-03 20:05:46Z herbelin $ *)
9	9
10	10	open Pp
11	11	open Util

240	240	let env_ar_params = push_rel_context ctx_params env_ar in
241	241
242	242	(* Compute interpretation metadatas *)
243		let indimpls = List.map (fun (_, impls) -> userimpls @ lift_implicits (List.length userimpls) impls) arities in
	243	let indimpls = List.map (fun (_, impls) -> userimpls @ lift_implicits (rel_context_nhyps ctx_params) impls) arities in
244	244	let arities = List.map fst arities in
245	245	let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in
246	246	let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in

274	274	mind_entry_lc = ctypes
275	275	}) indl arities constructors in
276	276	let impls =
277		let len = List.length ctx_params in
	277	let len = rel_context_nhyps ctx_params in
278	278	List.map2 (fun indimpls (_,_,cimpls) ->
279	279	indimpls, List.map (fun impls ->
280	280	userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors

+14

-14

toplevel/metasyntax.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: metasyntax.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
	8	(* $Id: metasyntax.ml 13690 2010-12-06 16:15:54Z glondu $ *)
9	9
10	10	open Pp
11	11	open Flags

105	105	let print_grammar = function
106	106	\| "constr" \| "operconstr" \| "binder_constr" ->
107	107	msgnl (str "Entry constr is");
108		Gram.Entry.print Pcoq.Constr.constr;
	108	entry_print Pcoq.Constr.constr;
109	109	msgnl (str "and lconstr is");
110		Gram.Entry.print Pcoq.Constr.lconstr;
	110	entry_print Pcoq.Constr.lconstr;
111	111	msgnl (str "where binder_constr is");
112		Gram.Entry.print Pcoq.Constr.binder_constr;
	112	entry_print Pcoq.Constr.binder_constr;
113	113	msgnl (str "and operconstr is");
114		Gram.Entry.print Pcoq.Constr.operconstr;
	114	entry_print Pcoq.Constr.operconstr;
115	115	\| "pattern" ->
116		Gram.Entry.print Pcoq.Constr.pattern
	116	entry_print Pcoq.Constr.pattern
117	117	\| "tactic" ->
118	118	msgnl (str "Entry tactic_expr is");
119		Gram.Entry.print Pcoq.Tactic.tactic_expr;
	119	entry_print Pcoq.Tactic.tactic_expr;
120	120	msgnl (str "Entry binder_tactic is");
121		Gram.Entry.print Pcoq.Tactic.binder_tactic;
	121	entry_print Pcoq.Tactic.binder_tactic;
122	122	msgnl (str "Entry simple_tactic is");
123		Gram.Entry.print Pcoq.Tactic.simple_tactic;
	123	entry_print Pcoq.Tactic.simple_tactic;
124	124	\| "vernac" ->
125	125	msgnl (str "Entry vernac is");
126		Gram.Entry.print Pcoq.Vernac_.vernac;
	126	entry_print Pcoq.Vernac_.vernac;
127	127	msgnl (str "Entry command is");
128		Gram.Entry.print Pcoq.Vernac_.command;
	128	entry_print Pcoq.Vernac_.command;
129	129	msgnl (str "Entry syntax is");
130		Gram.Entry.print Pcoq.Vernac_.syntax;
	130	entry_print Pcoq.Vernac_.syntax;
131	131	msgnl (str "Entry gallina is");
132		Gram.Entry.print Pcoq.Vernac_.gallina;
	132	entry_print Pcoq.Vernac_.gallina;
133	133	msgnl (str "Entry gallina_ext is");
134		Gram.Entry.print Pcoq.Vernac_.gallina_ext;
	134	entry_print Pcoq.Vernac_.gallina_ext;
135	135	\| _ -> error "Unknown or unprintable grammar entry."
136	136
137	137	(**********************************************************************)

-6

toplevel/toplevel.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: toplevel.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
	8	(* $Id: toplevel.ml 13668 2010-12-02 17:43:59Z herbelin $ *)
9	9
10	10	open Pp
11	11	open Util

275	275	\| Error_in_file (_,_,e) -> is_pervasive_exn e
276	276	\| Stdpp.Exc_located (_,e) -> is_pervasive_exn e
277	277	\| DuringCommandInterp (_,e) -> is_pervasive_exn e
278		\| DuringSyntaxChecking (_,e) -> is_pervasive_exn e
279	278	\| _ -> false
280	279
281	280	(* Toplevel error explanation, dealing with locations, Drop, Ctrl-D

284	283	let print_toplevel_error exc =
285	284	let (dloc,exc) =
286	285	match exc with
287		\| DuringCommandInterp (loc,ie)
288		\| DuringSyntaxChecking (loc,ie) ->
	286	\| DuringCommandInterp (loc,ie) ->
289	287	if loc = dummy_loc then (None,ie) else (Some loc, ie)
290	288	\| _ -> (None, exc)
291	289	in

334	332	* in encountered. *)
335	333
336	334	let process_error = function
337		\| DuringCommandInterp _
338		\| DuringSyntaxChecking _ as e -> e
	335	\| DuringCommandInterp _ as e -> e
339	336	\| e ->
340	337	if is_pervasive_exn e then
341	338	e

-4

toplevel/vernac.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(* $Id: vernac.ml 13488 2010-10-03 22:27:05Z herbelin $ *)
	8	(* $Id: vernac.ml 13668 2010-12-02 17:43:59Z herbelin $ *)
9	9
10	10	(* Parsing of vernacular. *)
11	11

33	33	let raise_with_file file exc =
34	34	let (cmdloc,re) =
35	35	match exc with
36		\| DuringCommandInterp(loc,e)
37		\| DuringSyntaxChecking(loc,e) -> (loc,e)
	36	\| DuringCommandInterp(loc,e) -> (loc,e)
38	37	\| e -> (dummy_loc,e)
39	38	in
40	39	let (inner,inex) =

170	169	\| e ->
171	170	(* if [e] is an anomaly, the next function will re-raise it *)
172	171	let msg = Cerrors.explain_exn_no_anomaly e in
173		msgnl (str "The command has indeed failed with message:" ++
	172	if_verbose msgnl (str "The command has indeed failed with message:" ++
174	173	fnl () ++ str "=> " ++ hov 0 msg)
175	174	end
176	175

-5

toplevel/vernacexpr.ml less more

5	5	(* * GNU Lesser General Public License Version 2.1 *)
6	6	(************************************************************************)
7	7
8		(i $Id: vernacexpr.ml 13492 2010-10-04 21:20:01Z herbelin $ i)
	8	(i $Id: vernacexpr.ml 13668 2010-12-02 17:43:59Z herbelin $ i)
9	9
10	10	open Util
11	11	open Names

359	359	(* Locating errors raised just after the dot is parsed but before the
360	360	interpretation phase *)
361	361
362		exception DuringSyntaxChecking of exn located
363
364		let syntax_checking_error loc s =
365		raise (DuringSyntaxChecking (loc,UserError ("",Pp.str s)))
	362	let syntax_checking_error loc s = user_err_loc (loc,"",Pp.str s)
366	363
367	364	(**********************************************************************)
368	365	(* Managing locality *)