Mercurial > emacs
changeset 109213:78b7e0e27a89
Merge from mainline.
| author | Katsumi Yamaoka <katsumi@flagship2> |
|---|---|
| date | Thu, 03 Jun 2010 12:01:23 +0000 |
| parents | 791f929d0313 (current diff) faf45a0d7ab2 (diff) |
| children | e38bba2d1deb |
| files | |
| diffstat | 26 files changed, 543 insertions(+), 314 deletions(-) [+] |
line wrap: on
line diff
--- a/ChangeLog Wed Jun 02 11:55:37 2010 +0000 +++ b/ChangeLog Thu Jun 03 12:01:23 2010 +0000 @@ -1,3 +1,7 @@ +2010-06-03 Glenn Morris <rgm@gnu.org> + + * configure.in (AH_BOTTOM): Remove NOT_C_CODE test, it is always true. + 2010-06-02 Dan Nicolaescu <dann@ics.uci.edu> Fix alloca definition when using gcc on non-gnu systems.
--- a/admin/CPP-DEFINES Wed Jun 02 11:55:37 2010 +0000 +++ b/admin/CPP-DEFINES Thu Jun 03 12:01:23 2010 +0000 @@ -131,7 +131,6 @@ GNU_LINUX GNU_MALLOC HAVE_AIX_SMT_EXP -HAVE_ALLOCA HAVE_BCMP HAVE_BCOPY HAVE_CBRT @@ -227,7 +226,6 @@ MODE_LINE_BINARY_TEXT MUST_UNDEF__STDC__ NLIST_STRUCT -NOT_C_CODE NO_ABORT NO_EDITRES NO_MATHERR
--- a/admin/notes/font-backend Wed Jun 02 11:55:37 2010 +0000 +++ b/admin/notes/font-backend Thu Jun 03 12:01:23 2010 +0000 @@ -6,11 +6,6 @@ New font handling mechanism with font backend method ---------------------------------------------------- -The configure script, if invoked with "--enable-font-backend", checks -if libraries freetype and fontconfig exist. If they are both -available, macro "USE_FONT_BACKEND" is defined in src/config.h. In -that case, the existence of Xft library is checked too. - The new files are: font.h -- header providing font-backend related structures (most important ones are "struct font" and "struct @@ -44,10 +39,6 @@ ftw32font.c -- font-driver on w32 directly using FreeType fonts utilizing methods provided by ftfont.c. -And, for those to work, macterm.c and macfns.c must be changed by the -similar way as xterm.c and xfns.c (the parts "#ifdef USE_FONT_BACKEND" -... "#endif" should be checked). - It may be interesting if Emacs supports a frame buffer directly and has these font driver. ftfbfont.c -- font-driver on FB for FreeType fonts.
--- a/configure.in Wed Jun 02 11:55:37 2010 +0000 +++ b/configure.in Thu Jun 03 12:01:23 2010 +0000 @@ -3546,13 +3546,8 @@ /* Some of the files of Emacs which are intended for use with other programs assume that if you have a config.h file, you must declare - the type of getenv. - - This declaration shouldn't appear when alloca.s or Makefile.in - includes config.h. */ -#ifndef NOT_C_CODE + the type of getenv. */ extern char *getenv (); -#endif /* These default definitions are good for almost all machines. The exceptions override them in m/MACHINE.h. */ @@ -3593,17 +3588,18 @@ # endif /* GCC. */ #endif /* __P */ -/* Don't include "string.h" or <stdlib.h> in non-C code. */ -#ifndef NOT_C_CODE #ifdef HAVE_STRING_H #include "string.h" #endif + #ifdef HAVE_STRINGS_H #include "strings.h" /* May be needed for bcopy & al. */ #endif + #ifdef HAVE_STDLIB_H #include <stdlib.h> #endif + #ifdef HAVE_ALLOCA_H # include <alloca.h> #elif defined __GNUC__ @@ -3617,10 +3613,10 @@ # endif void *alloca (size_t); #endif + #ifndef HAVE_SIZE_T typedef unsigned size_t; #endif -#endif /* NOT_C_CODE */ /* Define HAVE_X_I18N if we have usable i18n support. */
--- a/lisp/ChangeLog Wed Jun 02 11:55:37 2010 +0000 +++ b/lisp/ChangeLog Thu Jun 03 12:01:23 2010 +0000 @@ -1,13 +1,28 @@ +2010-06-03 Stefan Monnier <monnier@iro.umontreal.ca> + + Split smie-indent-calculate into more manageable chunks. + * emacs-lisp/smie.el (smie-indent-virtual, smie-indent-fixindent) + (smie-indent-comment, smie-indent-after-keyword, smie-indent-keyword) + (smie-indent-close, smie-indent-comment-continue, smie-indent-bob) + (smie-indent-exps): Extract from smie-indent-calculate. + (smie-indent-functions): New var. + (smie-indent-functions): Use them. + +2010-06-02 Stefan Monnier <monnier@iro.umontreal.ca> + + * emacs-lisp/smie.el (smie-indent-hanging-p): Use smie-bolp. + (smie-indent-calculate): Simplify and cleanup. + 2010-06-02 Michael Albinus <michael.albinus@gmx.de> * net/tramp-gvfs.el (top): Require url-util. - (tramp-gvfs-mount-point): Removed. - (tramp-gvfs-stringify-dbus-message, tramp-gvfs-send-command): New - defuns. + (tramp-gvfs-mount-point): Remove. + (tramp-gvfs-stringify-dbus-message, tramp-gvfs-send-command): + New defuns. (with-tramp-dbus-call-method): Format trace message. (tramp-gvfs-handle-copy-file, tramp-gvfs-handle-rename-file): - Implement backup call, when operation on local files fails. Use - progress reporter. Flush properties of changed files. + Implement backup call, when operation on local files fails. + Use progress reporter. Flush properties of changed files. (tramp-gvfs-handle-make-directory): Make more traces. (tramp-gvfs-url-file-name): Hexify file name in url. (tramp-gvfs-fuse-file-name): Take also prefix (like dav shares)
--- a/lisp/emacs-lisp/smie.el Wed Jun 02 11:55:37 2010 +0000 +++ b/lisp/emacs-lisp/smie.el Thu Jun 03 12:01:23 2010 +0000 @@ -484,6 +484,14 @@ :type 'integer) (defvar smie-indent-rules 'unset + ;; TODO: For SML, we need more rule formats, so as to handle + ;; structure Foo = + ;; Bar (toto) + ;; and + ;; structure Foo = + ;; struct ... end + ;; I.e. the indentation after "=" depends on the parent ("structure") + ;; as well as on the following token ("struct"). "Rules of the following form. \(TOK OFFSET) how to indent right after TOK. \(TOK O1 O2) how to indent right after TOK: @@ -506,7 +514,7 @@ (forward-char 1)) (skip-chars-forward " \t") (eolp)) - (save-excursion (skip-chars-backward " \t") (not (bolp))))) + (not (smie-bolp)))) (defun smie-bolp () (save-excursion (skip-chars-backward " \t") (bolp))) @@ -516,197 +524,210 @@ (cdr (assq t smie-indent-rules)) smie-indent-basic)) -(defun smie-indent-calculate (&optional virtual) - "Compute the indentation to use for point. -If VIRTUAL is non-nil, it means we're not trying to indent point but just +(defun smie-indent-virtual (virtual) + "Compute the virtual indentation to use for point. +This is used when we're not trying to indent point but just need to compute the column at which point should be indented in order to figure out the indentation of some other (further down) point. -VIRTUAL can take two different non-nil values: +VIRTUAL can take two different values: - :bolp: means that the current indentation of point can be trusted to be good only if it follows a line break. -- :hanging: means that the current indentation of point can be +- :not-hanging: means that the current indentation of point can be trusted to be good except if the following token is hanging." - ;; FIXME: This has accumulated a lot of rules, some of which aren't - ;; clearly orthogonal any more, so we should probably try and - ;; restructure it somewhat. - (or - ;; Trust pre-existing indentation on other lines. - (and virtual - (if (eq virtual :hanging) (not (smie-indent-hanging-p)) (smie-bolp)) + ;; Trust pre-existing indentation on other lines. + (assert virtual) + (if (if (eq virtual :not-hanging) (not (smie-indent-hanging-p)) (smie-bolp)) + (current-column) + (smie-indent-calculate))) + +(defun smie-indent-fixindent () + ;; Obey the `fixindent' special comment. + (when (save-excursion + (comment-normalize-vars) + (re-search-forward (concat comment-start-skip + "fixindent" + comment-end-skip) + ;; 1+ to account for the \n comment termination. + (1+ (line-end-position)) t)) + (current-column))) + +(defun smie-indent-bob () + ;; Start the file at column 0. + (save-excursion + (forward-comment (- (point))) + (if (bobp) 0))) + +(defun smie-indent-close () + ;; Align close paren with opening paren. + (save-excursion + ;; (forward-comment (point-max)) + (when (looking-at "\\s)") + (while (not (zerop (skip-syntax-forward ")"))) + (skip-chars-forward " \t")) + (condition-case nil + (progn + (backward-sexp 1) + (smie-indent-virtual :not-hanging)) + (scan-error nil))))) + +(defun smie-indent-keyword () + ;; Align closing token with the corresponding opening one. + ;; (e.g. "of" with "case", or "in" with "let"). + (save-excursion + (let* ((pos (point)) + (token (funcall smie-forward-token-function)) + (toklevels (cdr (assoc token smie-op-levels)))) + (when (car toklevels) + (let ((res (smie-backward-sexp 'halfsexp)) tmp) + ;; If we didn't move at all, that means we didn't really skip + ;; what we wanted. + (when (< (point) pos) + (cond + ((eq (car res) (car toklevels)) + ;; We bumped into a same-level operator. align with it. + (goto-char (cadr res)) + ;; Don't use (smie-indent-virtual :not-hanging) here, because we + ;; want to jump back over a sequence of same-level ops such as + ;; a -> b -> c + ;; -> d + ;; So as to align with the earliest appropriate place. + (smie-indent-virtual :bolp)) + ((equal token (save-excursion + (funcall smie-backward-token-function))) + ;; in cases such as "fn x => fn y => fn z =>", + ;; jump back to the very first fn. + ;; FIXME: should we only do that for special tokens like "=>"? + (smie-indent-virtual :bolp)) + ((setq tmp (assoc (cons (caddr res) token) + smie-indent-rules)) + (goto-char (cadr res)) + (+ (cdr tmp) (smie-indent-virtual :not-hanging))) + (t + (+ (or (cdr (assoc (cons t token) smie-indent-rules)) 0) + (current-column)))))))))) + +(defun smie-indent-comment () + ;; Indentation of a comment. + (and (looking-at comment-start-skip) + (save-excursion + (forward-comment (point-max)) + (skip-chars-forward " \t\r\n") + (smie-indent-calculate)))) + +(defun smie-indent-comment-continue () + ;; indentation of comment-continue lines. + (and (< 0 (length comment-continue)) + (looking-at (regexp-quote comment-continue)) (nth 4 (syntax-ppss)) + (let ((ppss (syntax-ppss))) + (save-excursion + (forward-line -1) + (if (<= (point) (nth 8 ppss)) + (progn (goto-char (1+ (nth 8 ppss))) (current-column)) + (skip-chars-forward " \t") + (if (looking-at (regexp-quote comment-continue)) + (current-column))))))) + +(defun smie-indent-after-keyword () + ;; Indentation right after a special keyword. + (save-excursion + (let* ((tok (funcall smie-backward-token-function)) + (tokinfo (assoc tok smie-indent-rules)) + (toklevel (if (and (zerop (length tok)) + ;; 4 == Open paren syntax. + (eq (syntax-class (syntax-after (1- (point)))) + 4)) + (progn (forward-char -1) + (setq tok (buffer-substring + (point) (1+ (point)))) + (setq tokinfo (assoc tok smie-indent-rules)) + (list tok nil 0)) + (assoc tok smie-op-levels)))) + (if (and toklevel (null (cadr toklevel)) (null tokinfo)) + (setq tokinfo (list (car toklevel) nil nil))) + (if (and tokinfo (null toklevel)) + (error "Token %S has indent rule but has no parsing info" tok)) + (when toklevel + (let ((default-offset + ;; The default indentation after a keyword/operator + ;; is 0 for infix and t for prefix. + ;; Using the BNF syntax, we could come up with + ;; better defaults, but we only have the + ;; precedence levels here. + (if (or tokinfo (null (cadr toklevel))) + (smie-indent-offset t) 0))) + ;; For indentation after "(let", we end up accumulating the + ;; offset of "(" and the offset of "let", so we use `min' + ;; to try and get it right either way. + (min + (+ (smie-indent-virtual :bolp) + (or (caddr tokinfo) (cadr tokinfo) default-offset)) + (+ (current-column) + (or (cadr tokinfo) default-offset)))))))) + +(defun smie-indent-exps () + ;; Indentation of sequences of simple expressions without + ;; intervening keywords or operators. E.g. "a b c" or "g (balbla) f". + ;; Can be a list of expressions or a function call. + ;; If it's a function call, the first element is special (it's the + ;; function). We distinguish function calls from mere lists of + ;; expressions based on whether the preceding token is listed in + ;; the `list-intro' entry of smie-indent-rules. + ;; + ;; TODO: to indent Lisp code, we should add a way to specify + ;; particular indentation for particular args depending on the + ;; function (which would require always skipping back until the + ;; function). + ;; TODO: to indent C code, such as "if (...) {...}" we might need + ;; to add similar indentation hooks for particular positions, but + ;; based on the preceding token rather than based on the first exp. + (save-excursion + (let ((positions nil) + arg) + (while (and (null (car (smie-backward-sexp))) + (push (point) positions) + (not (smie-bolp)))) + (save-excursion + ;; Figure out if the atom we just skipped is an argument rather + ;; than a function. + (setq arg (or (null (car (smie-backward-sexp))) + (member (funcall smie-backward-token-function) + (cdr (assoc 'list-intro smie-indent-rules)))))) + (cond + ((null positions) + ;; We're the first expression of the list. In that case, the + ;; indentation should be (have been) determined by its context. + nil) + (arg + ;; There's a previous element, and it's not special (it's not + ;; the function), so let's just align with that one. + (goto-char (car positions)) (current-column)) - ;; Obey the `fixindent' special comment. - (when (save-excursion - (comment-normalize-vars) - (re-search-forward (concat comment-start-skip - "fixindent" - comment-end-skip) - ;; 1+ to account for the \n comment termination. - (1+ (line-end-position)) t)) - (current-column)) - ;; Start the file at column 0. - (save-excursion - (forward-comment (- (point))) - (if (bobp) 0)) - ;; Align close paren with opening paren. - (save-excursion - ;; (forward-comment (point-max)) - (when (looking-at "\\s)") - (while (not (zerop (skip-syntax-forward ")"))) - (skip-chars-forward " \t")) - (condition-case nil - (progn - (backward-sexp 1) - (smie-indent-calculate :hanging)) - (scan-error nil)))) - ;; Align closing token with the corresponding opening one. - ;; (e.g. "of" with "case", or "in" with "let"). - (save-excursion - (let* ((pos (point)) - (token (funcall smie-forward-token-function)) - (toklevels (cdr (assoc token smie-op-levels)))) - (when (car toklevels) - (let ((res (smie-backward-sexp 'halfsexp)) tmp) - ;; If we didn't move at all, that means we didn't really skip - ;; what we wanted. - (when (< (point) pos) - (cond - ((eq (car res) (car toklevels)) - ;; We bumped into a same-level operator. align with it. - (goto-char (cadr res)) - ;; Don't use (smie-indent-calculate :hanging) here, because we - ;; want to jump back over a sequence of same-level ops such as - ;; a -> b -> c - ;; -> d - ;; So as to align with the earliest appropriate place. - (smie-indent-calculate :bolp)) - ((equal token (save-excursion - (funcall smie-backward-token-function))) - ;; in cases such as "fn x => fn y => fn z =>", - ;; jump back to the very first fn. - ;; FIXME: should we only do that for special tokens like "=>"? - (smie-indent-calculate :bolp)) - ((setq tmp (assoc (cons (caddr res) token) - smie-indent-rules)) - (goto-char (cadr res)) - (+ (cdr tmp) (smie-indent-calculate :hanging))) - (t - (+ (or (cdr (assoc (cons t token) smie-indent-rules)) 0) - (current-column))))))))) - ;; Indentation of a comment. - (and (looking-at comment-start-skip) - (save-excursion - (forward-comment (point-max)) - (skip-chars-forward " \t\r\n") - (smie-indent-calculate nil))) - ;; indentation inside a comment. - ;; FIXME: Hey, this is not generic!! - (and (looking-at "\\*") (nth 4 (syntax-ppss)) - (let ((ppss (syntax-ppss))) - (save-excursion - (forward-line -1) - (if (<= (point) (nth 8 ppss)) - (progn (goto-char (1+ (nth 8 ppss))) (current-column)) - (skip-chars-forward " \t") - (if (looking-at "\\*") - (current-column)))))) - ;; Indentation right after a special keyword. - (save-excursion - (let* ((tok (funcall smie-backward-token-function)) - (tokinfo (assoc tok smie-indent-rules)) - (toklevel (assoc tok smie-op-levels))) - (when (or tokinfo (and toklevel (null (cadr toklevel)))) - (if (or (smie-indent-hanging-p) - ;; If calculating the virtual indentation point, prefer - ;; looking up the virtual indentation of the alignment - ;; point as well. This is used for indentation after - ;; "fn x => fn y =>". - virtual) - (+ (smie-indent-calculate :bolp) - (or (caddr tokinfo) (cadr tokinfo) (smie-indent-offset t))) - (+ (current-column) - (or (cadr tokinfo) (smie-indent-offset t))))))) - ;; Main loop (FIXME: whatever that means!?). - (save-excursion - (let ((positions nil) - (begline nil) - arg) - (while (and (null (car (smie-backward-sexp))) - (push (point) positions) - (not (setq begline (smie-bolp))))) - (save-excursion - ;; Figure out if the atom we just skipped is an argument rather - ;; than a function. - (setq arg (or (null (car (smie-backward-sexp))) - (member (funcall smie-backward-token-function) - (cdr (assoc 'list-intro smie-indent-rules)))))) - (cond - ((and arg positions) - (goto-char (car positions)) - (current-column)) - ((and (null begline) (cdr positions)) - ;; We skipped some args plus the function and bumped into something. - ;; Align with the first arg. - (goto-char (cadr positions)) - (current-column)) - ((and (null begline) positions) - ;; We're the first arg. - ;; FIXME: it might not be a funcall, in which case we might be the - ;; second element. - (goto-char (car positions)) - (+ (smie-indent-offset 'args) - ;; We used to use (smie-indent-calculate :bolp), but that - ;; doesn't seem right since it might then indent args less than - ;; the function itself. - (current-column))) - ((and (null arg) (null positions)) - ;; We're the function itself. Not sure what to do here yet. - ;; FIXME: This should not be possible, because it should mean - ;; we're right after some special token. - (if virtual (current-column) - (save-excursion - (let* ((pos (point)) - (tok (funcall smie-backward-token-function)) - (toklevels (cdr (assoc tok smie-op-levels)))) - (cond - ((numberp (car toklevels)) - ;; We're right after an infix token. Let's skip over the - ;; lefthand side. - (goto-char pos) - (let (res) - (while (progn (setq res (smie-backward-sexp 'halfsexp)) - (and (not (smie-bolp)) - (equal (car res) (car toklevels))))) - ;; We should be right after a token of equal or - ;; higher precedence. - (cond - ((and (consp res) (memq (car res) '(t nil))) - ;; The token of higher-precedence is like an open-paren. - ;; Sample case for t: foo { bar, \n[TAB] baz }. - ;; Sample case for nil: match ... with \n[TAB] | toto ... - ;; (goto-char (cadr res)) - (smie-indent-calculate :hanging)) - ((and (consp res) (<= (car res) (car toklevels))) - ;; We stopped at a token of equal or higher precedence - ;; because we found a place with which to align. - (current-column)) - ))) - ;; For other cases.... hmm... we'll see when we get there. - ))))) - ((null positions) - (funcall smie-backward-token-function) - (+ (smie-indent-offset 'args) (smie-indent-calculate :bolp))) - ((car (smie-backward-sexp)) - ;; No arg stands on its own line, but the function does: - (if (cdr positions) - (progn - (goto-char (cadr positions)) - (current-column)) - (goto-char (car positions)) - (+ (current-column) (smie-indent-offset 'args)))) - (t - ;; We've skipped to a previous arg on its own line: align. - (goto-char (car positions)) - (current-column))))))) + ((cdr positions) + ;; We skipped some args plus the function and bumped into something. + ;; Align with the first arg. + (goto-char (cadr positions)) + (current-column)) + (positions + ;; We're the first arg. + (goto-char (car positions)) + (+ (smie-indent-offset 'args) + ;; We used to use (smie-indent-virtual :bolp), but that + ;; doesn't seem right since it might then indent args less than + ;; the function itself. + (current-column))))))) + +(defvar smie-indent-functions + '(smie-indent-fixindent smie-indent-bob smie-indent-close smie-indent-keyword + smie-indent-comment smie-indent-comment-continue smie-indent-after-keyword + smie-indent-exps) + "Functions to compute the indentation. +Each function is called with no argument, shouldn't move point, and should +return either nil if it has no opinion, or an integer representing the column +to which that point should be aligned, if we were to reindent it.") + +(defun smie-indent-calculate () + "Compute the indentation to use for point." + (run-hook-with-args-until-success 'smie-indent-functions)) (defun smie-indent-line () "Indent current line using the SMIE indentation engine."
--- a/msdos/ChangeLog Wed Jun 02 11:55:37 2010 +0000 +++ b/msdos/ChangeLog Thu Jun 03 12:01:23 2010 +0000 @@ -1,3 +1,7 @@ +2010-06-03 Glenn Morris <rgm@gnu.org> + + * sed2v2.inp: Do not edit HAVE_ALLOCA. + 2010-05-26 Glenn Morris <rgm@gnu.org> * sed1v2.inp (@PRE_EDIT_LDFLAGS@, @POST_EDIT_LDFLAGS@): Edit to nothing.
--- a/msdos/sed2v2.inp Wed Jun 02 11:55:37 2010 +0000 +++ b/msdos/sed2v2.inp Thu Jun 03 12:01:23 2010 +0000 @@ -27,7 +27,6 @@ #define NSIG 320\ #endif -/^#undef HAVE_ALLOCA *$/s/^.*$/#define HAVE_ALLOCA 1/ /^#undef HAVE_SETITIMER *$/s/^.*$/#define HAVE_SETITIMER 1/ /^#undef HAVE_STRUCT_UTIMBUF *$/s/^.*$/#define HAVE_STRUCT_UTIMBUF 1/ /^#undef LOCALTIME_CACHE *$/s/^.*$/#define LOCALTIME_CACHE 1/
--- a/nextstep/DEV-NOTES Wed Jun 02 11:55:37 2010 +0000 +++ b/nextstep/DEV-NOTES Thu Jun 03 12:01:23 2010 +0000 @@ -64,13 +64,8 @@ Currently ctrl-g is not detected in as many circumstances as other emacsen. It is not certain whether this is due to the means of event loop integration, -or errors of omission in the NS code. One area for exploration is the -NO_SOCK_SIGIO define. When it is defined, ctrl-g seems to be picked up more -often, but there are some annoying side effects. Currently it is left off by -default, unless the --enable-cocoa-experimental-ctrl-g option is passed to -configure [option removed Feb 2009]. (Has no effect under GNUstep.) -This is an area for improvement. Also, see the article here and its -containing thread: +or errors of omission in the NS code. This is an area for improvement. +Also, see the article here and its containing thread: http://article.gmane.org/gmane.emacs.devel/92021/match=handling%5fsignal
--- a/nt/ChangeLog Wed Jun 02 11:55:37 2010 +0000 +++ b/nt/ChangeLog Thu Jun 03 12:01:23 2010 +0000 @@ -1,3 +1,7 @@ +2010-06-03 Glenn Morris <rgm@gnu.org> + + * config.nt: Remove NOT_C_CODE tests, it is always true now. + 2010-05-13 Glenn Morris <rgm@gnu.org> * config.nt (LD_SWITCH_X_SITE, C_SWITCH_X_SITE): Remove undefs.
--- a/nt/config.nt Wed Jun 02 11:55:37 2010 +0000 +++ b/nt/config.nt Thu Jun 03 12:01:23 2010 +0000 @@ -365,14 +365,9 @@ #ifndef WINDOWSNT /* Some of the files of Emacs which are intended for use with other programs assume that if you have a config.h file, you must declare - the type of getenv. - - This declaration shouldn't appear when alloca.s or Makefile.in - includes config.h. */ -#ifndef NOT_C_CODE + the type of getenv. */ extern char *getenv (); #endif -#endif #endif /* EMACS_CONFIG_H */ @@ -414,8 +409,6 @@ #endif #endif -/* Don't include <string.h> during configure. */ -#ifndef NOT_C_CODE #ifdef HAVE_STRING_H #include "string.h" #endif @@ -425,7 +418,6 @@ #ifdef HAVE_STDLIB_H #include <stdlib.h> #endif -#endif #ifndef NO_RETURN #if defined __GNUC__ && (__GNUC__ > 2 || (__GNUC__ == 2 && __GNUC_MINOR >= 5)) @@ -436,12 +428,10 @@ #endif /* Redefine abort. */ -#ifndef NOT_C_CODE #ifdef HAVE_NTGUI #define abort w32_abort void w32_abort (void) NO_RETURN; #endif -#endif /* Prevent accidental use of features unavailable in older Windows versions we still support. */
--- a/src/ChangeLog Wed Jun 02 11:55:37 2010 +0000 +++ b/src/ChangeLog Thu Jun 03 12:01:23 2010 +0000 @@ -1,3 +1,16 @@ +2010-06-03 Glenn Morris <rgm@gnu.org> + + * m/template.h (NO_SOCK_SIGIO): Remove, no longer used. + + * m/hp800.h (alloca) [__NetBSD__ && __GNUC__]: No need to define it, + now that AH_BOTTOM does it. + + * m/hp800.h (HAVE_ALLOCA): + * m/ibms390x.h (HAVE_ALLOCA): Do not define, no longer needed. + + * m/ia64.h, s/gnu-linux.h, s/gnu.h, s/netbsd.h, s/usg5-4.h: + Remove NOT_C_CODE tests, it is always true now. + 2010-06-02 Dan Nicolaescu <dann@ics.uci.edu> Fix config.h includes.
--- a/src/config.in Wed Jun 02 11:55:37 2010 +0000 +++ b/src/config.in Thu Jun 03 12:01:23 2010 +0000 @@ -312,10 +312,10 @@ /* Define to 1 if you have the <kerberos/krb.h> header file. */ #undef HAVE_KERBEROS_KRB_H -/* Define to 1 if `e_text' is a member of `krb5_error'. */ +/* Define to 1 if `e_text' is member of `krb5_error'. */ #undef HAVE_KRB5_ERROR_E_TEXT -/* Define to 1 if `text' is a member of `krb5_error'. */ +/* Define to 1 if `text' is member of `krb5_error'. */ #undef HAVE_KRB5_ERROR_TEXT /* Define to 1 if you have the <krb5.h> header file. */ @@ -606,25 +606,25 @@ /* Define to 1 if you have the `strsignal' function. */ #undef HAVE_STRSIGNAL -/* Define to 1 if `ifr_addr' is a member of `struct ifreq'. */ +/* Define to 1 if `ifr_addr' is member of `struct ifreq'. */ #undef HAVE_STRUCT_IFREQ_IFR_ADDR -/* Define to 1 if `ifr_broadaddr' is a member of `struct ifreq'. */ +/* Define to 1 if `ifr_broadaddr' is member of `struct ifreq'. */ #undef HAVE_STRUCT_IFREQ_IFR_BROADADDR -/* Define to 1 if `ifr_flags' is a member of `struct ifreq'. */ +/* Define to 1 if `ifr_flags' is member of `struct ifreq'. */ #undef HAVE_STRUCT_IFREQ_IFR_FLAGS -/* Define to 1 if `ifr_hwaddr' is a member of `struct ifreq'. */ +/* Define to 1 if `ifr_hwaddr' is member of `struct ifreq'. */ #undef HAVE_STRUCT_IFREQ_IFR_HWADDR -/* Define to 1 if `ifr_netmask' is a member of `struct ifreq'. */ +/* Define to 1 if `ifr_netmask' is member of `struct ifreq'. */ #undef HAVE_STRUCT_IFREQ_IFR_NETMASK -/* Define to 1 if `n_un.n_name' is a member of `struct nlist'. */ +/* Define to 1 if `n_un.n_name' is member of `struct nlist'. */ #undef HAVE_STRUCT_NLIST_N_UN_N_NAME -/* Define to 1 if `tm_zone' is a member of `struct tm'. */ +/* Define to 1 if `tm_zone' is member of `struct tm'. */ #undef HAVE_STRUCT_TM_TM_ZONE /* Define to 1 if `struct utimbuf' is declared by <utime.h>. */ @@ -853,9 +853,6 @@ /* Define to the one symbol short name of this package. */ #undef PACKAGE_TARNAME -/* Define to the home page for this package. */ -#undef PACKAGE_URL - /* Define to the version of this package. */ #undef PACKAGE_VERSION @@ -915,28 +912,6 @@ /* Define to 1 if using the Motif X toolkit. */ #undef USE_MOTIF -/* Enable extensions on AIX 3, Interix. */ -#ifndef _ALL_SOURCE -# undef _ALL_SOURCE -#endif -/* Enable GNU extensions on systems that have them. */ -#ifndef _GNU_SOURCE -# undef _GNU_SOURCE -#endif -/* Enable threading extensions on Solaris. */ -#ifndef _POSIX_PTHREAD_SEMANTICS -# undef _POSIX_PTHREAD_SEMANTICS -#endif -/* Enable extensions on HP NonStop. */ -#ifndef _TANDEM_SOURCE -# undef _TANDEM_SOURCE -#endif -/* Enable general extensions on Solaris. */ -#ifndef __EXTENSIONS__ -# undef __EXTENSIONS__ -#endif - - /* Define to 1 if we should use toolkit scroll bars. */ #undef USE_TOOLKIT_SCROLL_BARS @@ -972,6 +947,28 @@ /* Define to 1 if you need to in order for `stat' and other things to work. */ #undef _POSIX_SOURCE +/* Enable extensions on AIX 3, Interix. */ +#ifndef _ALL_SOURCE +# undef _ALL_SOURCE +#endif +/* Enable GNU extensions on systems that have them. */ +#ifndef _GNU_SOURCE +# undef _GNU_SOURCE +#endif +/* Enable threading extensions on Solaris. */ +#ifndef _POSIX_PTHREAD_SEMANTICS +# undef _POSIX_PTHREAD_SEMANTICS +#endif +/* Enable extensions on HP NonStop. */ +#ifndef _TANDEM_SOURCE +# undef _TANDEM_SOURCE +#endif +/* Enable general extensions on Solaris. */ +#ifndef __EXTENSIONS__ +# undef __EXTENSIONS__ +#endif + + /* Define to rpl_ if the getopt replacement functions and variables should be used. */ #undef __GETOPT_PREFIX @@ -1106,13 +1103,8 @@ /* Some of the files of Emacs which are intended for use with other programs assume that if you have a config.h file, you must declare - the type of getenv. - - This declaration shouldn't appear when alloca.s or Makefile.in - includes config.h. */ -#ifndef NOT_C_CODE + the type of getenv. */ extern char *getenv (); -#endif /* These default definitions are good for almost all machines. The exceptions override them in m/MACHINE.h. */ @@ -1153,17 +1145,18 @@ # endif /* GCC. */ #endif /* __P */ -/* Don't include "string.h" or <stdlib.h> in non-C code. */ -#ifndef NOT_C_CODE #ifdef HAVE_STRING_H #include "string.h" #endif + #ifdef HAVE_STRINGS_H #include "strings.h" /* May be needed for bcopy & al. */ #endif + #ifdef HAVE_STDLIB_H #include <stdlib.h> #endif + #ifdef HAVE_ALLOCA_H # include <alloca.h> #elif defined __GNUC__ @@ -1177,10 +1170,10 @@ # endif void *alloca (size_t); #endif + #ifndef HAVE_SIZE_T typedef unsigned size_t; #endif -#endif /* NOT_C_CODE */ /* Define HAVE_X_I18N if we have usable i18n support. */
--- a/src/m/hp800.h Wed Jun 02 11:55:37 2010 +0000 +++ b/src/m/hp800.h Thu Jun 03 12:01:23 2010 +0000 @@ -29,13 +29,5 @@ This flag only matters if you use USE_LISP_UNION_TYPE. */ #define EXPLICIT_SIGN_EXTEND -/* Systems with GCC don't need to lose. */ -#ifdef __NetBSD__ -# ifdef __GNUC__ -# define alloca __builtin_alloca -# define HAVE_ALLOCA -# endif /* __GNUC__ */ -#endif /* __NetBSD__ */ - /* arch-tag: 809436e6-1645-4b92-b40d-2de5d6e7227c (do not change this comment) */
--- a/src/m/ia64.h Wed Jun 02 11:55:37 2010 +0000 +++ b/src/m/ia64.h Thu Jun 03 12:01:23 2010 +0000 @@ -48,8 +48,6 @@ /* Convert that into an integer that is 100 for a load average of 1.0 */ #define LOAD_AVE_CVT(x) (int) (((double) (x)) * 100.0 / FSCALE) -#ifndef NOT_C_CODE - #ifdef REL_ALLOC #ifndef _MALLOC_INTERNAL /* "char *" because ralloc.c defines it that way. gmalloc.c thinks it @@ -60,8 +58,6 @@ #endif /* not _MALLOC_INTERNAL */ #endif /* REL_ALLOC */ -#endif /* not NOT_C_CODE */ - #define HAVE_TEXT_START /* arch-tag: 9b8e9fb2-2e49-4c22-b68f-11a488e77c66
--- a/src/m/ibms390.h Wed Jun 02 11:55:37 2010 +0000 +++ b/src/m/ibms390.h Thu Jun 03 12:01:23 2010 +0000 @@ -1,4 +1,4 @@ -/* machine description file template. +/* Machine description file for IBM S390 in 32-bit mode Copyright (C) 1985, 1986, 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008, 2009, 2010 Free Software Foundation, Inc.
--- a/src/m/ibms390x.h Wed Jun 02 11:55:37 2010 +0000 +++ b/src/m/ibms390x.h Thu Jun 03 12:01:23 2010 +0000 @@ -54,11 +54,6 @@ numerically. */ #define VIRT_ADDR_VARIES -/* Define HAVE_ALLOCA to say that the system provides a properly - working alloca function and it should be used. Undefine it if an - assembler-language alloca in the file alloca.s should be used. */ -#define HAVE_ALLOCA - /* On the 64 bit architecture, we can use 60 bits for addresses */ #define VALBITS 60
--- a/src/m/template.h Wed Jun 02 11:55:37 2010 +0000 +++ b/src/m/template.h Thu Jun 03 12:01:23 2010 +0000 @@ -58,17 +58,6 @@ code will not be sharable; but that's better than failing completely. */ #define NO_REMAP -/* Some really obscure 4.2-based systems (like Sequent DYNIX) - do not support asynchronous I/O (using SIGIO) on sockets, - even though it works fine on tty's. If you have one of - these systems, define the following, and then use it in - config.h (or elsewhere) to decide when (not) to use SIGIO. - - You'd think this would go in an operating-system description file, - but since it only occurs on some, but not all, BSD systems, the - reasonable place to select for it is in the machine description file. */ -#define NO_SOCK_SIGIO - /* After adding support for a new machine, modify the large case statement in configure.in to recognize reasonable configuration names, and add a description of the system to
--- a/src/s/gnu-linux.h Wed Jun 02 11:55:37 2010 +0000 +++ b/src/s/gnu-linux.h Thu Jun 03 12:01:23 2010 +0000 @@ -29,7 +29,6 @@ It sets the Lisp variable system-type. */ #define SYSTEM_TYPE "gnu/linux" /* All the best software is free. */ -#ifndef NOT_C_CODE #ifdef emacs #ifdef HAVE_LINUX_VERSION_H #include <linux/version.h> @@ -40,7 +39,6 @@ #endif /* LINUX_VERSION_CODE >= 0x20400 */ #endif /* HAVE_LINUX_VERSION_H */ #endif /* emacs */ -#endif /* NOT_C_CODE */ #if defined HAVE_GRANTPT #define UNIX98_PTYS
--- a/src/s/gnu.h Wed Jun 02 11:55:37 2010 +0000 +++ b/src/s/gnu.h Thu Jun 03 12:01:23 2010 +0000 @@ -34,9 +34,7 @@ /* Some losing code fails to include this and then assumes that because it is braindead that O_RDONLY==0. */ -#ifndef NOT_C_CODE #include <fcntl.h> -#endif #ifdef emacs #include <stdio.h> /* Get the definition of _IO_STDIO_H. */
--- a/src/s/netbsd.h Wed Jun 02 11:55:37 2010 +0000 +++ b/src/s/netbsd.h Thu Jun 03 12:01:23 2010 +0000 @@ -31,9 +31,7 @@ /* Greg A. Woods <woods@weird.com> says we must include signal.h before syssignal.h is included, to work around interface conflicts that are handled with CPP __RENAME() macro in signal.h. */ -#ifndef NOT_C_CODE #include <signal.h> -#endif /* Don't close pty in process.c to make it as controlling terminal. It is already a controlling terminal of subprocess, because we did
--- a/src/s/sol2-10.h Wed Jun 02 11:55:37 2010 +0000 +++ b/src/s/sol2-10.h Thu Jun 03 12:01:23 2010 +0000 @@ -7,15 +7,14 @@ /* Use the Solaris dldump() function, called from unexsol.c, to dump emacs, instead of the generic ELF dump code found in unexelf.c. The resulting binary has a complete symbol table, and is better - for debugging and other observabilty tools (debuggers, pstack, etc). + for debugging and other observability tools (debuggers, pstack, etc). If you encounter a problem using dldump(), please consider sending a message to the OpenSolaris tools-linking mailing list: http://mail.opensolaris.org/mailman/listinfo/tools-linking - It is likely that dldump() works with older Solaris too, - but this has not been tested, and so, this change is for - Solaris 10 and newer only at this time. */ + It is likely that dldump() works with older Solaris too, but this has + not been tested, so for now this change is for Solaris 10 or newer. */ #undef UNEXEC #define UNEXEC unexsol.o
--- a/src/s/usg5-4.h Wed Jun 02 11:55:37 2010 +0000 +++ b/src/s/usg5-4.h Thu Jun 03 12:01:23 2010 +0000 @@ -77,9 +77,7 @@ /* Get FIONREAD from <sys/filio.h>. Get <sys/ttold.h> to get struct tchars. But get <termio.h> first to make sure ttold.h doesn't interfere. And don't try to use SIGIO yet. */ -#ifndef NOT_C_CODE #include <sys/wait.h> -#endif #ifdef emacs #include <sys/filio.h>
--- a/test/ChangeLog Wed Jun 02 11:55:37 2010 +0000 +++ b/test/ChangeLog Thu Jun 03 12:01:23 2010 +0000 @@ -1,3 +1,7 @@ +2010-06-02 Stefan Monnier <monnier@iro.umontreal.ca> + + * indent: New dir. + 2010-05-07 Chong Yidong <cyd@stupidchicken.com> * Version 23.2 released.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/indent/Makefile Thu Jun 03 12:01:23 2010 +0000 @@ -0,0 +1,15 @@ +RM=rm +EMACS=emacs + +clean: + -$(RM) *.test + +# TODO: +# - mark the places where the indentation is known to be incorrect, +# and allow either ignoring those errors or not. +%.test: % + -$(RM) $<.test + $(EMACS) --batch $< \ + --eval '(indent-region (point-min) (point-max) nil)' \ + --eval '(write-region (point-min) (point-max) "$<.test")' + diff -u -B $< $<.test
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/test/indent/prolog.prolog Thu Jun 03 12:01:23 2010 +0000 @@ -0,0 +1,224 @@ +%% -*- mode: prolog; coding: utf-8 -*- + +%% wf(+E) +%% Vérifie que E est une expression syntaxiquement correcte. +wf(X) :- atom(X); integer(X); var(X). %Une variable ou un entier. +wf(lambda(X, T, B)) :- atom(X), wf(T), wf(B). %Une fonction. +wf(app(E1, E2)) :- wf(E1), wf(E2). %Un appel de fonction. +wf(pi(X, T, B)) :- atom(X), wf(T), wf(B). %Le type d'une fonction. + +%% Éléments additionnels utilisés dans le langage source. +wf(lambda(X, B)) :- atom(X), wf(B). +wf(let(X, E1, E2)) :- atom(X), wf(E1), wf(E2). +wf(let(X, T, E1, E2)) :- atom(X), wf(T), wf(E1), wf(E2). +wf((T1 -> T2)) :- wf(T1), wf(T2). +wf(forall(X, T, B)) :- atom(X), wf(T), wf(B). +wf(fix(X,T,E1,E2)) :- atom(X), wf(T), wf(E1), wf(E2). +wf(fix(X,E1,E2)) :- atom(X), wf(E1), wf(E2). +wf(app(E1,E2,E3)) :- wf(E1), wf(E2), wf(E3). +wf(app(E1,E2,E3,E4)) :- wf(E1), wf(E2), wf(E3), wf(E4). + +%% subst(+X, +V, +FV, +Ei, -Eo) +%% Remplace X par V dans Ei. Les variables qui apparaissent libres dans +%% V et peuvent aussi apparaître dans Ei doivent toutes être inclues +%% dans l'environnement FV. +subst(X, V, _, X, E) :- !, E = V. +subst(_, _, _, Y, Y) :- atom(Y); integer(Y). +%% Residualize the substitution when applied to an uninstantiated variable. +%% subst(X, V, _, Y, app(lambda(X,_,Y),V)) :- var(Y). +%% Rather than residualize and leave us with unifications that fail, let's +%% rather assume that Y will not refer to X. +subst(X, V, _, Y, Y) :- var(Y). +subst(X, V, FV, lambda(Y, Ti, Bi), lambda(Y1, To, Bo)) :- + subst(X, V, FV, Ti, To), + (X = Y -> + %% If X is equal to Y, X is shadowed, so no subst can take place. + Y1 = Y, Bo = Bi; + (member((Y, _), FV) -> + %% If Y appears in FV, it can appear in V, so we need to + %% rename it to avoid name capture. + new_atom(Y, Y1), + subst(Y, Y1, [], Bi, Bi1); + Y1 = Y, Bi1 = Bi), + %% Perform substitution on the body. + subst(X, V, FV, Bi1, Bo)). +subst(X, V, FV, pi(Y, Ti, Bi), pi(Y1, To, Bo)) :- + subst(X, V, FV, lambda(Y, Ti, Bi), lambda(Y1, To, Bo)). +subst(X, V, FV, forall(Y, Ti, Bi), forall(Y1, To, Bo)) :- + subst(X, V, FV, lambda(Y, Ti, Bi), lambda(Y1, To, Bo)). +subst(X, V, FV, app(E1i, E2i), app(E1o, E2o)) :- + subst(X, V, FV, E1i, E1o), subst(X, V, FV, E2i, E2o). + +%% apply(+F, +Arg, +Env, -E) +apply(lambda(X, _, B), Arg, Env, E) :- \+ var(B), subst(X, Arg, Env, B, E). +apply(app(plus, N1), N2, _, N) :- integer(N1), integer(N2), N is N1 + N2. +apply(app(minus, N1), N2, _, N) :- integer(N1), integer(N2), N is N1 - N2. + + +%% normalize(+E1, +Env, -E2) +%% Applique toutes les réductions possibles sur E1. +normalize(X, _, X) :- integer(X); var(X); atom(X). +%% normalize(X, Env, E) :- atom(X), member((X, E), Env). +normalize(lambda(X, T, B), Env, lambda(X, Tn, Bn)) :- + normalize(T, [(X,T)|Env], Tn), normalize(B, [(X,T)|Env], Bn). +normalize(pi(X, T, B), Env, pi(X, Tn, Bn)) :- + normalize(T, [(X,T)|Env], Tn), normalize(B, [(X,T)|Env], Bn). +normalize(forall(X, T, B), Env, forall(X, Tn, Bn)) :- + normalize(T, [(X,T)|Env], Tn), normalize(B, [(X,T)|Env], Bn). +normalize(app(E1, E2), Env, En) :- + normalize(E1, Env, E1n), + normalize(E2, Env, E2n), + (apply(E1n, E2n, Env, E) -> + normalize(E, Env, En); + En = app(E1n, E2n)). + +%% infer(+E, +Env, -T) +%% Infère le type de E dans Env. On essaie d'être permissif, dans le sens +%% que l'on présume que l'expression est typée correctement. +infer(X, _, int) :- integer(X). +infer(X, _, _) :- var(X). %Une expression encore inconnue. +infer(X, Env, T) :- + atom(X), + (member((X, T1), Env) -> + %% X est déjà dans Env: vérifie que le type est correct. + T = T1; + %% X est une variable libre. + true). +infer(lambda(X,T,B), Env, pi(Y,T,TB)) :- + infer(B, [(X,T)|Env], TBx), + (var(Y) -> + Y = X, TB = TBx; + subst(X, Y, Env, TBx, TB)). +infer(app(E1, E2), Env, Tn) :- + infer(E1, Env, T1), + (T1 = pi(X,T2,B); T1 = forall(X,T2,B)), + infer(E2, Env, T2), + subst(X, E2, Env, B, T), + normalize(T, Env, Tn). +infer(pi(X,T1,T2), Env, type) :- + infer(T1, Env, type), + infer(T2, [(X,T1)|Env], type). +infer(forall(X,T1,T2), Env, type) :- + infer(T1, Env, type), + infer(T2, [(X,T1)|Env], type). + +%% freevars(+E, +Env, -Vs) +%% Renvoie les variables libres de E. Vs est une liste associative +%% où chaque élément est de la forme (X,T) où X est une variable et T est +%% son type. +freevars(X, _, []) :- integer(X). +freevars(X, Env, Vs) :- + atom(X), + (member((X,_), Env) -> + %% Variable liée. + Vs = []; + %% Variable libre. Type inconnu :-( + Vs = [(X,_)]). +%% Les variables non-instanciées peuvent être remplacées par des paramètres +%% qui seront liés par `closetype' selon le principe de Hindley-Milner. +freevars(X, _, [(X, _)]) :- var(X), new_atom(X). +freevars(app(E1, E2), Env, Vs) :- + freevars(E1, Env, Vs1), + append(Vs1, Env, Env1), + freevars(E2, Env1, Vs2), + append(Vs1, Vs2, Vs). +freevars(lambda(X, T, B), Env, Vs) :- + freevars(T, Env, TVs), + append(TVs, Env, Env1), + freevars(B, [(X,T)|Env1], BVs), + append(TVs, BVs, Vs). +freevars(pi(X, T, B), Env, Vs) :- freevars(lambda(X, T, B), Env, Vs). +freevars(forall(X, T, B), Env, Vs) :- freevars(lambda(X, T, B), Env, Vs). + +%% close(+Eo, +To, +Vs, -Ec, -Tc) +%% Ferme un type ouvert To en liant chaque variable libre (listées dans Vs) +%% avec `forall'. +closetype(E, T, [], E, T). +closetype(Eo, To, [(X,T)|Vs], lambda(X, T, Ec), forall(X, T, Tc)) :- + closetype(Eo, To, Vs, Ec, Tc). + +%% elab_type(+Ee, +Te, +Env, -Eg, -Tg) +%% Ajoute les arguments implicites de E:T. +generalize(Ee, Te, Env, Eg, Tg) :- + freevars(Te, Env, Vs), + append(Vs, Env, EnvX), + %% Essaie d'instancier les types des paramètres que `generalize' vient + %% d'ajouter. + infer(Te, EnvX, type), + closetype(Ee, Te, Vs, Eg, Tg). + +%% instantiate(+X, +T, -E) +%% Utilise la variable X de type T. Le résultat E est X auquel on ajoute +%% tous les arguments implicites (de valeur inconnue). +instantiate(X, T, X) :- var(T), ! . +instantiate(X, forall(_, _, T), app(E, _)) :- !, instantiate(X, T, E). +instantiate(X, _, X). + +%% elaborate(+E1, +Env, -E2) +%% Transforme E1 en une expression E2 où le sucre syntaxique a été éliminé +%% et où les arguments implicites ont été rendus explicites. +elaborate(X, _, X) :- integer(X); var(X). +elaborate(X, Env, E) :- + atom(X), + (member((X, T), Env) -> + instantiate(X, T, E); + %% Si X n'est pas dans l'environnement, c'est une variable libre que + %% l'on voudra probablement généraliser. + X = E). +elaborate(lambda(X, T, B), Env, lambda(X, Te, Be)) :- + elaborate(T, Env, Te), + elaborate(B, [(X,Te)|Env], Be). +elaborate(pi(X, T, B), Env, pi(X, Te, Be)) :- + elaborate(T, Env, Te), + elaborate(B, [(X,Te)|Env], Be). +elaborate(app(E1, E2), Env, app(E1e, E2e)) :- + elaborate(E1, Env, E1e), + elaborate(E2, Env, E2e). +elaborate(let(X, T, E1, E2), Env, app(lambda(X, Tg, E2e), E1g)) :- + elaborate(E1, Env, E1e), + elaborate(T, Env, Te), + infer(E1e, Env, Te), + generalize(E1e, Te, Env, E1g, Tg), + elaborate(E2, [(X,Te)|Env], E2e). +%% Expansion du sucre syntaxique. +elaborate((T1 -> T2), Env, Ee) :- + new_atom(X), elaborate(pi(X, T1, T2), Env, Ee). +elaborate(app(E1, E2, E3, E4), Env, Ee) :- + elaborate(app(app(E1,E2,E3),E4), Env, Ee). +elaborate(app(E1, E2, E3), Env, Ee) :- elaborate(app(app(E1,E2),E3), Env, Ee). +elaborate(lambda(X, B), Env, Ee) :- elaborate(lambda(X, _, B), Env, Ee). +elaborate(let(X, E1, E2), Env, Ee) :- elaborate(let(X, _, E1, E2), Env, Ee). +elaborate(fix(F,B,E), Env, Ee) :- elaborate(fix(F,_,B,E), Env, Ee). +elaborate(fix(F,T,B,E), Env, Ee) :- + elaborate(let(F,T,app(fix,lambda(F,T,B)),E), Env, Ee). + +%% elab_bindings(+TS, +Env, -TS). +%% Applique `elaborate' sur l'environnment de type TS. +elab_tenv([], _, []). +elab_tenv([(X,T)|TS], Env, [(X, Tg)|TSe]) :- + elaborate(T, Env, Te), + infer(Te, Env, type), + generalize(_, Te, Env, _, Tg), + elab_tenv(TS, [(X, Tg)|Env], TSe). + + +%% elaborate(+E1, -E2) +%% Comme le `elaborate' ci-dessus, mais avec un environnement par défaut. +elaborate(SRC, E) :- + elab_tenv([(int, type), + (fix, ((t -> t) -> t)), + %% list: type → int → type + (list, (type -> int -> type)), + %% plus: int → int → int + (plus, (int -> int -> int)), + %% minus: int → int → int + (minus, (int -> int -> int)), + %% nil: list t 0 + (nil, app(app(list,t),0)), + %% cons: t -> list t n → list t (n + 1) + (cons, (t -> app(app(list,t),n) -> + app(app(list,t), app(app(plus,n),1)))) %fixindent + ], + [(type,type)], + Env), + elaborate(SRC, Env, E).