mirror of
https://git.savannah.gnu.org/git/emacs.git
synced 2025-01-13 16:38:14 +00:00
* lisp/emacs-lisp/smie.el (smie-indent-calculate): Simplify and cleanup.
(smie-indent-hanging-p): Use smie-bolp. * test/indent: New dir.
This commit is contained in:
Stefan Monnier
parent
1efeec868d
commit
927c346bd6
@ -1,13 +1,18 @@
|
||||
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)
|
||||
|
||||
@ -484,6 +484,14 @@ Possible return values:
|
||||
: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 @@ A nil offset defaults to `smie-indent-basic'.")
|
||||
(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 @@ VIRTUAL can take two different non-nil values:
|
||||
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 @@ VIRTUAL can take two different non-nil values:
|
||||
(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 @@ VIRTUAL can take two different non-nil values:
|
||||
(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."
|
||||
|
||||
@ -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.
|
||||
|
||||
15
test/indent/Makefile
Normal file
15
test/indent/Makefile
Normal file
@ -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
|
||||
224
test/indent/prolog.prolog
Normal file
224
test/indent/prolog.prolog
Normal file
@ -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).
|
||||
Loading…
Reference in New Issue
Block a user