[Emacs-diffs] /srv/bzr/emacs/trunk r100506: * lisp/emacs-lisp/smie.el (smie-indent-calculate): Simplify and cleanup.

[Stefan Monnier]

------------------------------------------------------------
revno: 100506
committer: Stefan Monnier <address@hidden>
branch nick: trunk
timestamp: Wed 2010-06-02 16:13:11 -0400
message:
  * lisp/emacs-lisp/smie.el (smie-indent-calculate): Simplify and cleanup.
  (smie-indent-hanging-p): Use smie-bolp.
  * test/indent: New dir.
added:
  test/indent/
  test/indent/Makefile
  test/indent/prolog.prolog
modified:
  lisp/ChangeLog
  lisp/emacs-lisp/smie.el
  test/ChangeLog

=== modified file 'lisp/ChangeLog'
--- a/lisp/ChangeLog    2010-06-02 09:53:00 +0000
+++ b/lisp/ChangeLog    2010-06-02 20:13:11 +0000
@@ -1,13 +1,18 @@
+2010-06-02  Stefan Monnier  <address@hidden>
+
+       * emacs-lisp/smie.el (smie-indent-hanging-p): Use smie-bolp.
+       (smie-indent-calculate): Simplify and cleanup.
+
 2010-06-02  Michael Albinus  <address@hidden>
 
        * 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)

=== modified file 'lisp/emacs-lisp/smie.el'
--- a/lisp/emacs-lisp/smie.el   2010-05-27 04:41:36 +0000
+++ b/lisp/emacs-lisp/smie.el   2010-06-02 20:13:11 +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)))
@@ -526,9 +534,6 @@
   to be good only if it follows a line break.
 - :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
@@ -598,41 +603,73 @@
           (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))
+   ;; 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 "\\*")
+              (if (looking-at (regexp-quote comment-continue))
                   (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)
+            (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-calculate :bolp)
-                (or (caddr tokinfo) (cadr tokinfo) (smie-indent-offset t)))
+               (or (caddr tokinfo) (cadr tokinfo) default-offset))
            (+ (current-column)
-              (or (cadr tokinfo) (smie-indent-offset t)))))))
-   ;; Main loop (FIXME: whatever that means!?).
+               (or (cadr tokinfo) default-offset)))))))
+   ;; 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)
-           (begline nil)
            arg)
        (while (and (null (car (smie-backward-sexp)))
                    (push (point) positions)
-                   (not (setq begline (smie-bolp)))))
+                   (not (smie-bolp))))
        (save-excursion
          ;; Figure out if the atom we just skipped is an argument rather
          ;; than a function.
@@ -640,73 +677,28 @@
                        (member (funcall smie-backward-token-function)
                                (cdr (assoc 'list-intro smie-indent-rules))))))
        (cond
-        ((and arg positions)
+        ((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))
-        ((and (null begline) (cdr positions))
+        ((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)
+        (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)))))))
+            (current-column))))))))
 
 (defun smie-indent-line ()
   "Indent current line using the SMIE indentation engine."

=== modified file 'test/ChangeLog'
--- a/test/ChangeLog    2010-05-08 18:47:07 +0000
+++ b/test/ChangeLog    2010-06-02 20:13:11 +0000
@@ -1,3 +1,7 @@
+2010-06-02  Stefan Monnier  <address@hidden>
+
+       * indent: New dir.
+
 2010-05-07  Chong Yidong  <address@hidden>
 
        * Version 23.2 released.

=== added directory 'test/indent'
=== added file 'test/indent/Makefile'
--- a/test/indent/Makefile      1970-01-01 00:00:00 +0000
+++ b/test/indent/Makefile      2010-06-02 20:13:11 +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

=== added file 'test/indent/prolog.prolog'
--- a/test/indent/prolog.prolog 1970-01-01 00:00:00 +0000
+++ b/test/indent/prolog.prolog 2010-06-02 20:13:11 +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).