Stefan pushed to branch master at Stefan / Typer Commits: 756bdbdf by Stefan Monnier at 2017-09-19T17:26:13Z * emacs/typer-mode.el: Render comments as markdown (typer--markdown-verbatim-block-re, typer--markdown-verbatim-face): New consts. (typer--markdown-p): New function. (typer-markdown-blockquote): New face. (typer-markdown-keywords): New var. (typer-font-lock-keywords): Use it. (typer-mode): Setup use of `invisible' property. * btl/pervasive.typer: Make use of new comment style. * src/subst.ml: Rework top-level comment. - - - - - 5 changed files: - btl/pervasive.typer - doc/manual.texi - emacs/typer-mode.el - src/subst.ml - tests/elab_test.ml Changes: ===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -1,4 +1,4 @@ -%%% pervasive.typer --- Always available definitions +%%% pervasive --- Always available definitions %% Copyright (C) 2011-2017 Free Software Foundation, Inc. %% @@ -23,10 +23,10 @@ %%% Commentary: %% This file includes all kinds of predefined types and functions that are -%% generally useful. It plays a similar role to builtins.typer and is read -%% right after that one. The main reason for the separation into +%% generally useful. It plays a similar role to `builtins.typer` and is +%% read right after that one. The main reason for the separation into %% 2 different files, is that for technical reasons, one cannot use macros -%% in builtins.typer. +%% in `builtins.typer`. %%% Code: @@ -46,9 +46,9 @@ List_length xs = case xs %% ML's typical `head` function is not total, so can't be defined %% as-is in Typer. There are several workarounds: -%% - Provide a default value : (a : Type) ≡> a -> List a -> a; -%% - Disallow problem case : (a : Type) ≡> (l : List a) -> (l != nil) -> a; -%% - Return an Option/Error. +%% - Provide a default value : `a -> List a -> a`; +%% - Disallow problem case : `(l : List a) -> (l != nil) -> a`; +%% - Return an Option/Error List_head1 : (a : Type) ≡> List a -> Option a; List_head1 xs = case xs | nil => none @@ -89,7 +89,7 @@ List_nth = lambda n -> lambda xs -> lambda d -> case xs %%%% A more flexible `lambda` -%% An Sexp which we use to represents an error. +%% An `Sexp` which we use to represents an *error*. Sexp_error = Sexp_symbol "<error>"; Sexp_to_list : Sexp -> List Sexp -> List Sexp; @@ -108,10 +108,12 @@ Sexp_to_list s = lambda exceptions -> singleton singleton singleton singleton; multiarg_lambda = - %% This macro lets `lambda_->_` (and siblings) accept multiplke arguments. + %% This macro lets `lambda_->_` (and siblings) accept multiple arguments. %% TODO: We could additionally turn - %% `lambda (x :: t) y -> e` into `lambda (x : t) => lambda y -> e` - %% thus providing an alternate syntax for lambdas which doesn't use + %% lambda (x :: t) y -> e + %% into + %% lambda (x : t) => lambda y -> e` + %% thus providing an alternate syntax for lambdas which don't use %% => and ≡>. let exceptions = List_map Sexp_symbol (cons "_:_" (cons "_::_" (cons "_:::_" nil))) in @@ -168,7 +170,7 @@ K x y = x; %% Takes an Sexp `x` as argument and return an Sexp which represents code %% which will construct an Sexp equivalent to `x` at run-time. -%% This is basically "cross stage persistence" for Sexp. +%% This is basically *cross stage persistence* for Sexp. quote1 : Sexp -> Sexp; quote1 x = let k = K x; qlist : List Sexp -> Sexp; @@ -191,8 +193,8 @@ quote = macro (lambda x -> quote1 (List_head Sexp_error x)); %%%% The `type` declaration macro -%% build a declaration -%% var-name = value-expr; +%% Build a declaration: +%% var-name = value-expr; make-decl : Sexp -> Sexp -> Sexp; make-decl var-name value-expr = Sexp_node (Sexp_symbol "_=_") @@ -203,8 +205,8 @@ chain-decl : Sexp -> Sexp -> Sexp; chain-decl a b = Sexp_node (Sexp_symbol "_;_") (cons a (cons b nil)); -%% build datacons -%% ctor-name = datacons type-name ctor-name; +%% Build datacons: +%% ctor-name = datacons type-name ctor-name; make-cons : Sexp -> Sexp -> Sexp; make-cons ctor-name type-name = make-decl ctor-name @@ -212,8 +214,8 @@ make-cons ctor-name type-name = (cons type-name (cons ctor-name nil))); -%% buil type annotation -%% var-name : type-expr; +%% Build type annotation: +%% var-name : type-expr; make-ann : Sexp -> Sexp -> Sexp; make-ann var-name type-expr = Sexp_node (Sexp_symbol "_:_") @@ -221,10 +223,11 @@ make-ann var-name type-expr = (cons type-expr nil)); type-impl = lambda (x : List Sexp) -> - %% x follow the mask -> (_|_ Nat zero (succ Nat)) - %% Type name --^ ^------^ constructors + %% `x` follow the mask -> + %% (_|_ Nat zero (succ Nat)) + %% Type name --^ ^------^ constructors - %% Return a list contained inside a node sexp + %% Return a list contained inside a node sexp. let knil = K nil; kerr = K Sexp_error; @@ -252,7 +255,7 @@ type-impl = lambda (x : List Sexp) -> get-head = List_head Sexp_error; - %% Get expression + %% Get expression. expr = get-head x; %% Expression is Sexp_node (Sexp_symbol "|") (list) @@ -265,13 +268,13 @@ type-impl = lambda (x : List Sexp) -> type-name = get-name name; - %% Create the inductive type definition + %% Create the inductive type definition. inductive = Sexp_node (Sexp_symbol "typecons") (cons name ctor); decl = make-decl type-name inductive; - %% Add constructors + %% Add constructors. ctors = let for-each : List Sexp -> Sexp -> Sexp; for-each ctr acc = case ctr | cons hd tl => @@ -331,8 +334,8 @@ __\.__ = %%%% Logic -%% False should be one of the many empty types. -%% Other common choices are False = ∀a.a and True = ∃a.a. +%% `False` should be one of the many empty types. +%% Other popular choices are False = ∀a.a and True = ∃a.a. False = Void; True = Unit; @@ -360,15 +363,18 @@ if_then_else_ | false => uquote e3)); %%%% Test -test1 : Option Int; +test1 : ?; test2 : Option Int; test3 : Option Int; test1 = test2; -test4 : Option ?; +%% In earlier versions of Typer, we could use `?` in declarations +%% to mean "fill this for me by unifying with later type information", +%% but this is incompatible with the use of generalization to introduce +%% implicit arguments. +%% test4 : Option ?; test2 = none; test4 : Option Int; -test4 = test1; +test4 = test1 : Option ?; test3 = test4; - %%% pervasive.typer ends here. ===================================== doc/manual.texi ===================================== --- a/doc/manual.texi +++ b/doc/manual.texi @@ -206,7 +206,7 @@ A = { TypeLevel : SortL, TypeLevel.z : TypeLevel TypeLevel.s : TypeLevel → TypeLevel, TypeLevel.∪ : TypeLevel → TypeLevel → TypeLevel. - Type l : Type (TypeLevel.s l), ∀ l : TypeLevel + Type : (l : TypeLevel) → Type (TypeLevel.s l) } R = { (SortL, Type l, Sortω), ∀ l : TypeLevel (SortL, Sortω, Sortω), ===================================== emacs/typer-mode.el ===================================== --- a/emacs/typer-mode.el +++ b/emacs/typer-mode.el @@ -55,15 +55,82 @@ st) "Syntax table for `typer-mode'.") +;;;; Support for markdown-style rendering in comments + +(defconst typer--markdown-verbatim-block-re "^[ \t]*%+\\(?: *\t\\| \\)") + +(defconst typer--markdown-verbatim-face + (if (facep 'fixed-pitch-serif) 'fixed-pitch-serif 'fixed-pitch)) + +(defun typer--markdown-p () + (and (save-excursion (nth 4 (syntax-ppss))) + (let ((prop (get-text-property (1- (point)) 'face))) + (not (and (consp prop) + (memq typer--markdown-verbatim-face prop)))))) + +(defface typer-markdown-blockquote + '((t :background "grey95")) + "Face used for blocks quoted with `>' in comments.") + +(defvar typer-markdown-keywords + `((,(concat "\\(?:\\`%%\\(%+\\)[ \t]+\\(.*?\\)[ \t]+---" ;First line + "\\|^%%\\(?1:%+\\)" ;Other header lines + "\\)[ \t]+\\(.*\\)") + (2 typer--markdown-verbatim-face prepend t) + (3 (typer--section-face (- (match-end 1) (match-beginning 1))) prepend)) + (,(concat typer--markdown-verbatim-block-re "[ \t]*\\(.*\\)") + (1 (when (save-excursion + (forward-line -1) + (looking-at (concat typer--markdown-verbatim-block-re + "[ \t]*\\(.*\\)" + "\\|[ \t]*%+\\(?:[ \t]*$\\| ?[^ \t]\\)"))) + typer--markdown-verbatim-face) + append)) + ("^[ \t]*%+[ \t]+>\\([ \t]+.*\\)" + (1 'typer-markdown-blockquote append)) + (,(concat typer--markdown-verbatim-block-re "[ \t]*\\(.*\\)") + (1 (when (save-excursion + (forward-line -1) + (looking-at (concat typer--markdown-verbatim-block-re + "[ \t]*\\(.*\\)" + "\\|[ \t]*%+[ \t]*$"))) + typer--markdown-verbatim-face) + append)) + ("`\\([^`\n]+\\)`" + (1 (if (typer--markdown-p) typer--markdown-verbatim-face) + prepend)) + ("\\*\\*\\(.+?\\)\\*\\*" + (1 (let ((p0 (match-beginning 0)) + (p1 (match-beginning 1)) + (p2 (match-end 1)) + (p3 (match-end 0))) + (when (typer--markdown-p) + ;; FIXME: Completely hiding the ** is evil! + (put-text-property p0 p1 'invisible 'typer-markdown) + (put-text-property p2 p3 'invisible 'typer-markdown) + 'bold)) + prepend)) + ("\\*\\([^*\n]+\\)\\*" + (1 (unless (or (eq ?* (char-before (match-beginning 0))) + (eq ?* (char-after (match-end 0)))) + (let ((p0 (match-beginning 0)) + (p1 (match-beginning 1)) + (p2 (match-end 1)) + (p3 (match-end 0))) + (when (typer--markdown-p) + ;; FIXME: Completely hiding the ** is evil! + (put-text-property p0 p1 'invisible 'typer-markdown) + (put-text-property p2 p3 'invisible 'typer-markdown) + 'italic))) + prepend)))) + (defvar typer-font-lock-keywords `(("deftoken[ \t]+\\([^ \t\n]+\\)" (1 font-lock-function-name-face)) (,(concat "\\_<" (regexp-opt '("type" "case" "lambda" "let" "in")) "\\_>") (0 font-lock-keyword-face)) ("\\_<type[ \t]+\\([^ \t\n]+\\)" (1 font-lock-function-name-face)) ("^\\([^() \t]+\\)[ \t]" (1 font-lock-function-name-face)) - ("^%%\\(%+\\)\\(?:.* ---\\)?\\(.*\\)" - (2 (typer--section-face (- (match-end 1) (match-beginning 1))) prepend)) - ) + ,@typer-markdown-keywords) "Keyword highlighting specification for `typer-mode'.") (defun typer--section-face (length) @@ -202,6 +269,8 @@ (concat "./typer " (shell-quote-argument (file-relative-name buffer-file-name))))) (smie-setup typer-smie-grammar #'typer-smie-rules) + (add-to-invisibility-spec '(typer-markdown . nil)) + (push 'invisible font-lock-extra-managed-props) ;; (set (make-local-variable 'compilation-first-column) 0) (set (make-local-variable 'compilation-error-screen-columns) nil) (set (make-local-variable 'imenu-generic-expression) ===================================== src/subst.ml ===================================== --- a/src/subst.ml +++ b/src/subst.ml @@ -1,6 +1,6 @@ (* subst.ml --- Substitutions for Lexp -Copyright (C) 2016 Free Software Foundation, Inc. +Copyright (C) 2016-2017 Free Software Foundation, Inc. Author: Stefan Monnier <monnier@iro.umontreal.ca> @@ -37,174 +37,70 @@ module U = Util * - S.identity_p * - S.lookup * - * This implementation is generic (i.e. can be with various datatypes + * This implementation is generic (i.e. can be used with various datatypes * implementing the associated lambda-calculus), which is the reason for * the added complexity of arguments like `mkVar` and `mkShift` to `S.lookup`. * So in general, you'll want to use Lexp.scompose and Lexp.slookup * for those functions. *) -(* Suspensions definitions. +(* There are many different ways to do an explicit substitution system. + * See for example: + * Implementation of Explicit Substitutions: + * from λσ to the Suspension Calculus. + * Vincent Archambault-Bouffard and Stefan Monnier. HOR'2016. + * http://www.iro.umontreal.ca/~monnier/HOR-2016.pdf * - * ol: old embedding level ('associate' level, length with environement) - * nl: new .... + * We mostly follow the above article, which we summarize here. + * We start from Abadi's calculs which looks like: * - * n: A Natural Number - * i: A positive integer + * e ::= #0 % Reference to dbi_index 0 + * e₁ e₂ + * (λ e) + * e[s] % Application of a substitution * - * t ::= c : - * #i : Debruijn Index variable bound by the ith abstraction - * (t, t) : Applications - * (λ t) : Abstractions - * [t, n, n, e] : Suspensions + * s ::= id % identity substitution + * e . s % replace #0 with `e` and use `s` for the rest + * s₁ ∘ s₂ % Composition (apply s₁ *first* and then s₂!). + * ↑ % dbi_index = dbi_index + 1 * - * length level - * e ::= nil : 0 : 0 - * (t, n)::e : n + len(e) : n - * {e1, nl, ol, e2} : len(e1) + len(e2) - nl : lev(e1) + nl - ol + * But we make it more practical by using instead: * - * level is the dbi index ? + * e ::= #i % Reference to dbi_index `i` + * e₁ e₂ + * (λ e) + * e[s] % Application of a substitution * - * Substitutions Compositions definitions. + * s ::= id % identity substitution + * e . s % replace #0 by `e` and use `s` for the rest + * s ↑n % like Abadi's "s ∘ (↑ⁿ)" * - * a ::= 1 - * a b - * (λ a) : - * a[s] : + * And the composition ∘ is defined as a function rather than a constructor. * - * s ::= id : identity - * a . s : cons replace dbi_idx = 0 by a use s for the rest - * s o t : Composition - * shift : dbi_index + 1 - *) -(* Substitutions. - * - * There are many different ways to implement a calculus with explicit - * substitutions, with tradeoffs between complexity of implementation, - * performance etc... - * - * The "fine-grained notation" version of the suspension calculus uses - * The following special rules: - * - * (λ [t₁, ol+1, nl+1, @nl::e]) t₂ ==> [t₁, ol+1, nl, (t₂,nl)::e] - * [[t, ol, nl, e], 0, nl', nil] ==> [t, ol, nl+nl', e] - * - * Alternate rules: - * - * [(λ t₁), ol, nl, e]) t₂ ==> [t₁, ol+1, nl, (t₂,nl)::e] - * - * The normal beta rule is: - * - * (λ t₁) t₂ ==> [t₁, 1, 0, (t₂,0) :: nil] - * - * which would be instantiated to - * - * (λ [t₁, ol, nl, e]) t₂ ==> [[t₁, ol, nl, e], 1, 0, (t₂,0) :: nil] - * - * So we could do it as follows: - * - * (λ [t₁ σ₁]) t₂ ==> [t₁ ((1, 0, (t₂::nil)) ∘ σ₁)] - * ((1, 0, (t₂::nil)) ∘ (ol+1, nl+1, e) ==> (ol₁, nl, (t₂,nl)::e) - * - * Rules used in the "no merging" version: - * - * (λ t₁) t₂ ==> [t₁, 1, 0, (t₂,0) :: nil] - * (λ [t₁, ol+1, nl+1, @nl::e]) t₂ ==> [t₁, ol+1, nl, (t₂,nl)::e] - * [t, 0, 0, nil] ==> t - * [#i, ol, nl, e] ==> #(i-ol+nl) if i>ol - * [#i, ol, nl, e] ==> #(nl - j) if e.i = @j' - * [#i, ol, nl, e] ==> [t, 0, nl - j, nil] if e.i = (t,j) - * [λt, ol, nl, e] ==> λ[t, ol+1, nl+1, @nl :: e] - * [[t, ol, nl, e], 0, nl', nil] ==> [t, ol, nl+nl', e] - * - * First simplification: get rid of `ol`! - * - * (λ t₁) t₂ ==> [t₁, 0, (t₂,0)::nil] - * [#i, nl, e] ==> [t, nl - j, nil] if e.i = (t,j) - * [λt, nl, e] ==> λ[t, nl+1, @nl::e] + * And we have the propagation rules: * - * (λ [t₁, nl+1, @nl::e]) t₂ ==> [t₁, nl, (t₂,nl)::e] - * [(λ t₁), nl, e]) t₂ ==> [t₁, nl, (t₂,nl)::e] - * [[t, nl, e], nl', nil] ==> [t, nl+nl', e] + * #i[s] ==> lookup i s + * (e₁ e₂)[s] ==> (e₁[s]) (e₂[s]) + * (λ e)[s] ==> λ(e[#0 · (s ↑1)]) + * e[s₁][s₂] ==> e[s₁ ∘ s₂] * - * [t, 0, nil] ==> t - * [#i, nl, e] ==> #(i-len(e)+nl) if i>len(e) - * [#i, nl, e] ==> #(nl - j) if e.i = @j' + * We also have beta rules: * - * Re-introduce subst-merging. So we currently have two merging rules: + * (λ e₁) e₂ ==> e₁[e₂·id] * - * ((0, (t₂::nil)) ∘ (nl+1, e) ==> (nl, (t₂,nl)::e) if e≠nil - * (nl, e) ∘ (nl', nil) ==> (nl+nl', e) + * To which we can add (as an optimisation to avoid using `compose`): * - * What do these substitutions mean? - * - * (N, nil) == shift N - * (0, e) == replace nearest N vars with values from `e` - * (nl+1, @nl::e) == lift e - * (nl, e) == shift (nl - ol) (ol, e) if ol = lvl(e) - * - * Another way to look at it: - * - * (λ t₁) t₂ ==> [t₁, t₂::nil] - * [λt, σ] ==> λ[t, lift σ] - * - * (λ [t₁, lift σ]) t₂ ==> [t₁, t₂::σ] - * [(λ t₁), σ]) t₂ ==> [t₁, t₂::σ] - * [[t, σ], shift n nil] ==> [t, shift n σ] - * - * [t, id] ==> t - * [#0, t::σ] ==> t - * [#i, t::σ] ==> [#i-1, σ] - * [#0, lift σ] ==> #0 - * [#i, lift σ] ==> [[#i-1, σ], shift 1 nil] - * [#i, shift N σ] ==> [[#i, σ], shift N nil] - * - * I guess I'm leaning towards a kind of λσ, but with - * - * σ = id | σ ↑n | a·σ - * - * where σ ↑n == (σ ∘ ↑n) - * and lift σ == #0·(σ ↑) - * and #n == [#0, ↑n] - * - * (λt₁)t₂ ==> [t₁, t₂·nil] - * [λt, σ] ==> λ[t, lift σ] - * [t, id] ==> t - * [#0, t·σ] ==> t - * [#i+1, t·σ] ==> [#i, σ] (because => [[#i, ↑] t·σ] => [#i, ↑ ∘ t·σ]) - * [#i, σ ↑n] ==> [[#i, σ], ↑n] + * (λ e₁)[s] e₂ ==> e₁[e₂·s] * * Merging rules: * - * (σ ↑n₂) ↑n₁ ==> σ ↑(n₁+n₂) {part of m1} - * σ₁ ∘ id ==> σ₁ {m2} - * σ₁ ∘ σ₂ ↑n ==> (σ₁ ∘ σ₂) ↑n {part of m1} - * id ∘ σ ==> σ {m3} - * σ₁ ↑n ∘ a·σ₂ ==> σ₁ ↑(n-1) ∘ σ₂ {m4 & m5} - * a·σ₁ ∘ σ₂ ==> [a, σ₂]·(σ₁ ∘ σ₂) {m6} - * - * The optimisations used in FLINT would translate to: - * - * [λt₁, σ] t₂ ==> (λ[t₁, lift σ]) t₂ - * ==> [t₁, (lift σ) ∘ t₂·nil] - * ==> [t₁, #0·(σ ↑) ∘ t₂·nil] - * ==> [t₁, [#0, t₂·nil]·(σ ↑ ∘ t₂·nil)] - * ==> [t₁, t₂·σ] - * [[t, σ], id ↑n] ==> [t, σ ∘ id ↑n] - * ==> [t, σ ↑n] - * - * Confluence: - * - * a·σ₁ ∘ σ₂ ↑n ==> (a·σ₁ ∘ σ₂) ↑n - * a·σ₁ ∘ σ₂ ↑n ==> [a, σ₂ ↑n]·(σ₁ ∘ σ₂ ↑n) - * - * so we might also need to make sure that - * - * (a·σ₁ ∘ σ₂) ↑n <==> [a, σ₂ ↑n]·(σ₁ ∘ σ₂ ↑n) - * - * for confluence. Which might boild down to adding a rule like + * (s ↑n₂) ↑n₁ ==> s ↑(n₁+n₂) {part of m1} + * s₁ ∘ id ==> s₁ {m2} + * s₁ ∘ s₂ ↑n ==> (s₁ ∘ s₂) ↑n {part of m1} + * id ∘ s ==> s {m3} + * s₁ ↑n ∘ e·s₂ ==> s₁ ↑(n-1) ∘ s₂ {m4 & m5} + * e·s₁ ∘ s₂ ==> (e[s₂])·(s₁ ∘ s₂) {m6} * - * (a·σ₁) ↑n <==> [a, id ↑n]·(σ₁ ↑n) *) (* We define here substitutions which take a variable within a source context @@ -219,7 +115,7 @@ type db_index = int (* DeBruijn index. *) type db_offset = int (* DeBruijn index offset. *) (* Substitution, i.e. a mapping from db_index to 'a - * In practice, 'a is always lexp, but we keep it as a paramter: + * In practice, 'a is always lexp, but we keep it as a parameter: * - for better modularity of the code. * - to break a mutual dependency between the Lexp and the Subst modules. *) type 'a subst = (* lexp subst *) ===================================== tests/elab_test.ml ===================================== --- a/tests/elab_test.ml +++ b/tests/elab_test.ml @@ -1,4 +1,4 @@ -(* lparse_test.ml --- +(* elab_test.ml --- * * Copyright (C) 2016-2017 Free Software Foundation, Inc. * View it on GitLab: https://gitlab.com/monnier/typer/commit/756bdbdfa94cf2d683e2e9b67a73661dece5... --- View it on GitLab: https://gitlab.com/monnier/typer/commit/756bdbdfa94cf2d683e2e9b67a73661dece5... You're receiving this email because of your account on gitlab.com.