Stefan pushed to branch master at Stefan / Typer

Commits: dec52d81 by Stefan Monnier at 2017-02-24T09:49:52-05:00 * btl/pervasive.typer: New file, combining type.typer and quote.typer

* btl/quote.typer, btl/type.typer: Remove. * emacs/typer-mode.el (typer-outline-regexp): Change default. * src/lparse.ml (default_ectx): Read btl/pervasive.typer after builtins. (default_ectx.read_file): Don't bind _parsing_internals here any more.

- - - - - 36c64913 by Stefan Monnier at 2017-02-24T10:05:27-05:00 * emacs/typer-mode.el (typer-font-lock-keywords): Highlight section titles (typer--section-face): New function.

- - - - -

5 changed files:

- btl/builtins.typer - btl/type.typer → btl/pervasive.typer - − btl/quote.typer - emacs/typer-mode.el - src/lparse.ml

Changes:

===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -1,39 +1,35 @@ -%* -%* Typer Compiler -%* -%* --------------------------------------------------------------------------- -%* -%* Copyright (C) 2011-2017 Free Software Foundation, Inc. -%* -%* Author: Pierre Delaunay pierre.delaunay@hec.ca -%* Keywords: languages, lisp, dependent types. -%* -%* This file is part of Typer. -%* -%* Typer is free software; you can redistribute it and/or modify it under the -%* terms of the GNU General Public License as published by the Free Software -%* Foundation, either version 3 of the License, or (at your option) any -%* later version. -%* -%* Typer is distributed in the hope that it will be useful, but WITHOUT ANY -%* WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS -%* FOR A PARTICULAR PURPOSE. See the GNU General Public License for -%* more details. -%* -%* You should have received a copy of the GNU General Public License along -%* with this program. If not, see http://www.gnu.org/licenses/. -%* -%* --------------------------------------------------------------------------- -%* -%* Description: -%* Define builtin types and functions -%* This file MUST be correctly typed -%* -%* --------------------------------------------------------------------------- +%%% builtins.typer --- File to initialize the builtin functions

-% ----------------------------------------------------- -% Base Types -% ----------------------------------------------------- +%% Copyright (C) 2011-2017 Free Software Foundation, Inc. +%% +%% Author: Pierre Delaunay pierre.delaunay@hec.ca +%% Keywords: languages, lisp, dependent types. +%% +%% This file is part of Typer. +%% +%% Typer is free software; you can redistribute it and/or modify it under the +%% terms of the GNU General Public License as published by the Free Software +%% Foundation, either version 3 of the License, or (at your option) any +%% later version. +%% +%% Typer is distributed in the hope that it will be useful, but WITHOUT ANY +%% WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS +%% FOR A PARTICULAR PURPOSE. See the GNU General Public License for +%% more details. +%% +%% You should have received a copy of the GNU General Public License along +%% with this program. If not, see http://www.gnu.org/licenses/. + +%%% Commentary: + +%% Define builtin types and functions. +%% This file MUST be correctly typed, in the sense that many of the types in +%% here are "axioms" that the type checker must accept without being +%% able to verify them. + +%%% Code: + +%%%% Base Types used in builtin functions

% The trivial type which carries no information. Unit = typecons Unit unit; @@ -109,14 +105,14 @@ sexp_eq = Built-in "sexp_eq" (Sexp -> Sexp -> Bool); % -----------------------------------------------------

List : Type -> Type; +%% List a = typecons List (nil) (cons a (List a)); +%% nil = lambda a ≡> datacons (List a) nil; +%% cons = lambda a ≡> datacons (List a) cons; List = typecons (List (a : Type)) (nil) (cons a (List a)); - nil = datacons List nil; cons = datacons List cons;

-% ----------------------------------------------------- -% Macro -% ----------------------------------------------------- +%%%% Macro-related definitions

%% block_ = Built-in "block_" (List Pretoken -> Sexp); symbol_ = Built-in "symbol_" (String -> Sexp); @@ -131,7 +127,6 @@ Macro = typecons (Macro)

Macro_ = datacons Macro Macro_ ;

- expand_macro_ : Macro -> List Sexp -> Sexp; expand_macro_ m args = case m | Macro_ f => (f args); @@ -148,10 +143,7 @@ sexp_dispatch_ = Built-in "sexp_dispatch_" ( -> a );

- -% ----------------------------------------------------- -% Monads -% ----------------------------------------------------- +%%%% Monads

% Builtin bind bind = Built-in "bind" ( @@ -176,65 +168,4 @@ open = Built-in "open" (String -> String -> IO FileHandle); write = Built-in "write" (FileHandle -> String -> IO Unit); read = Built-in "read" (FileHandle -> Int -> IO String);

-% ----------------------------------------------------- -% Logic -% ----------------------------------------------------- - -% False should be one of the many empty types. -% Other common choices are False = ∀a.a and True = ∃a.a. -False = Void; -True = Unit; - -Not : Type -> Type; -Not prop = prop -> False; - -% Like Bool, except that it additionally carries the meaning of its value. -Decidable = typecons (Decidable (prop : Type)) - (true (p ::: prop)) (false (p ::: Not prop)); - - -% ----------------------------------------------------- -% To be removed (used it tests) -% ----------------------------------------------------- - -Option = typecons (Option (a : Type)) (none) (some a); -some = datacons Option some; -none = datacons Option none; - -length : (a : Type) ≡> List a -> Int; -length = lambda a ≡> - lambda xs -> - case xs - | nil => 0 - | cons hd tl => (1 + (length tl)); - -reverse : (a : Type) ≡> List a -> List a -> List a; -reverse = lambda a ≡> lambda l -> lambda t -> - case l - | nil => t - | cons hd tl => reverse tl (cons hd t); - -concat : (a : Type) ≡> List a -> List a -> List a; -concat = lambda a ≡> - lambda l -> lambda t -> - let l' = reverse l nil in - reverse l' t; - -% 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) ≡> List a -> a -> a; -% - Disallow problem case : (a : Type) ≡> (l : List a) -> (l != nil) -> a; -% - Return an Option/Error. -head : (a : Type) ≡> List a -> Option a; -head = lambda a ≡> - lambda xs -> - case xs - | nil => none - | cons hd tl => some hd; - -tail : (a : Type) ≡> List a -> List a; -tail = lambda a ≡> - lambda xs -> - case xs - | nil => nil - | cons hd tl => tl; +%%% builtins.typer ends here.

===================================== btl/type.typer → btl/pervasive.typer ===================================== --- a/btl/type.typer +++ b/btl/pervasive.typer @@ -1,3 +1,102 @@ +%%% pervasive.typer --- Always available definitions + +%% Copyright (C) 2011-2017 Free Software Foundation, Inc. +%% +%% Author: Pierre Delaunay pierre.delaunay@hec.ca +%% Keywords: languages, lisp, dependent types. +%% +%% This file is part of Typer. +%% +%% Typer is free software; you can redistribute it and/or modify it under the +%% terms of the GNU General Public License as published by the Free Software +%% Foundation, either version 3 of the License, or (at your option) any +%% later version. +%% +%% Typer is distributed in the hope that it will be useful, but WITHOUT ANY +%% WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS +%% FOR A PARTICULAR PURPOSE. See the GNU General Public License for +%% more details. +%% +%% You should have received a copy of the GNU General Public License along +%% with this program. If not, see http://www.gnu.org/licenses/. + +%%% 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 +%% 2 different files, is that for technical reasons, one cannot use macros +%% in builtins.typer. + +%%% Code: + +%%%% `Option` type + +Option = typecons (Option (a : Type)) (none) (some a); +some = datacons Option some; +none = datacons Option none; + +%%%% List functions + +List_length : (a : Type) ≡> List a -> Int; +List_length = lambda a ≡> lambda xs -> case xs + | nil => 0 + | cons hd tl => (1 + (List_length tl)); + +List_reverse : (a : Type) ≡> List a -> List a -> List a; +List_reverse = lambda a ≡> lambda l -> lambda t -> case l + | nil => t + | cons hd tl => List_reverse tl (cons hd t); + +List_concat : (a : Type) ≡> List a -> List a -> List a; +List_concat = lambda a ≡> + lambda l -> lambda t -> List_reverse (List_reverse l nil) t; + +% 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) ≡> List a -> a -> a; +% - Disallow problem case : (a : Type) ≡> (l : List a) -> (l != nil) -> a; +% - Return an Option/Error. +List_head1 : (a : Type) ≡> List a -> Option a; +List_head1 = lambda a ≡> lambda xs -> case xs + | nil => none + | cons hd tl => some hd; + +List_tail : (a : Type) ≡> List a -> List a; +List_tail = lambda a ≡> lambda xs -> case xs + | nil => nil + | cons hd tl => tl; + +List_map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> List a -> List b; +List_map = lambda a b ≡> lambda f xs -> case xs + | nil => nil + | cons x xs => cons (f x) (List_map f xs); + +List_head : (a : Type) ≡> a -> List a -> a; +List_head = lambda a ≡> lambda x xs -> case xs + | cons x _ => x + | nil => x; + +%%%% Quasi-Quote macro + +%% f = (quote (uquote x) * x) (node _*_ [(node_ unquote "x") "x"]) +%% +%% f = node_ "*" cons (x, cons (symbol_ "x") nil)) +%% +%% => x + +quote1 : Sexp -> Sexp; +quote1 x = let k = lambda (a : Type) ≡> lambda (_ : a) -> x; + node op y = case (sexp_eq op (symbol_ "uquote")) + | true => List_head (symbol_ "<error>") y + | false => node_ (quote1 op) (List_map quote1 y) + in sexp_dispatch_ x node k k k k k; + +% quote definition +quote = Macro_ (lambda x -> quote1 (List_head (symbol_ "<error>") x)); + +%%%% The `type` declaration macro + % build a declaration % var-name = value-expr; make-decl : Sexp -> Sexp -> Sexp; @@ -68,7 +167,7 @@ type-impl = lambda (x : List Sexp) ->

% head is (node_ type-name (arg list)) let name = get-head lst; - ctor = tail lst in + ctor = List_tail lst in

let type-name = get-name name in

@@ -94,3 +193,26 @@ type-impl = lambda (x : List Sexp) ->

type_ = Macro_ type-impl; + +%%%% Backward compatibility + +length = List_length; +head = List_head1; +tail = List_tail; + +%%%% Logic + +% False should be one of the many empty types. +% Other common choices are False = ∀a.a and True = ∃a.a. +False = Void; +True = Unit; + +Not : Type -> Type; +Not prop = prop -> False; + +% Like Bool, except that it additionally carries the meaning of its value. +Decidable = typecons (Decidable (prop : Type)) + (true (p ::: prop)) (false (p ::: Not prop)); + + +%%% pervasive.typer ends here.

===================================== btl/quote.typer deleted ===================================== --- a/btl/quote.typer +++ /dev/null @@ -1,29 +0,0 @@ -% -% f = (quote (uquote x) * x) (node _*_ [(node_ unquote "x") "x"]) -% -% f = node_ "*" cons (x, cons (symbol_ "x") nil)) -% -% -% => x - -%% FIXME: Should be List.map. -List_map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> List a -> List b; -List_map = lambda a b ≡> lambda f xs -> case xs - | nil => nil - | cons x xs => cons (f x) (List_map f xs); - -%% FIXME: Should be List.head. -List_head : (a : Type) ≡> a -> List a -> a; -List_head = lambda a ≡> lambda x xs -> case xs - | cons x _ => x - | nil => x; - -quote1 : Sexp -> Sexp; -quote1 x = let k = lambda (a : Type) ≡> lambda (_ : a) -> x; - node op y = case (sexp_eq op (symbol_ "uquote")) - | true => List_head (symbol_ "<error>") y - | false => node_ (quote1 op) (List_map quote1 y) - in sexp_dispatch_ x node k k k k k; - -% quote definition -quote = Macro_ (lambda x -> quote1 (List_head (symbol_ "<error>") x));

===================================== emacs/typer-mode.el ===================================== --- a/emacs/typer-mode.el +++ b/emacs/typer-mode.el @@ -1,6 +1,6 @@ ;;; typer-mode.el --- Typer major mode

-;; Copyright (C) 2011-2016 Free Software Foundation, Inc. +;; Copyright (C) 2011-2017 Free Software Foundation, Inc.

;; Author: Stefan Monnier monnier@iro.umontreal.ca ;; Keywords: @@ -55,16 +55,25 @@ (defvar typer-font-lock-keywords '(("deftoken[ \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)) ) "Keyword highlighting specification for `typer-mode'.")

+(defun typer--section-face (length) + (pcase length + (1 'info-title-1) + (2 'info-title-2) + (3 'info-title-3) + (_ 'info-title-4))) + (defvar typer-imenu-generic-expression '(("Special tokens" "^deftoken[ \t]+\([^\t\n ]+\)" 1) ;; (nil "^function[ \t]+\(\(\sw\|\s_\)+\)" 1) ) "Regex patterns for the index menu of `typer-mode'.")

-(defvar typer-outline-regexp "(\|;;;+" +(defvar typer-outline-regexp "%%%+\|[^%\s\n\t]......" "Regexp for `outline-minor-mode' in `typer-mode'.")

;; Abbreviations and Skeletons

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -1255,11 +1255,11 @@ let default_ectx let sxps = lex default_stt pres in let nods = sexp_parse_all_to_list default_grammar sxps (Some ";") in let pxps = pexp_decls_all nods in - let _, lctx = dynamic_bind _parsing_internals true - (fun () -> lexp_p_decls pxps elctx) in lctx in + let _, lctx = lexp_p_decls pxps elctx + in lctx in

(* Register predef *) - let register_pred elctx = + let register_predefs elctx = try List.iter (fun name -> let idx = senv_lookup name elctx in let v = Var((dloc, name), idx) in @@ -1275,8 +1275,11 @@ let default_ectx (!BI.lmap) lctx in

(* read base file *) - let lctx = read_file (!btl_folder ^ "builtins.typer") lctx in - let _ = register_pred lctx in + let lctx = dynamic_bind _parsing_internals true + (fun () + -> read_file (!btl_folder ^ "builtins.typer") + lctx) in + let _ = register_predefs lctx in

(* Does not work, not sure why let files = ["list.typer"; "quote.typer"; "type.typer"] in @@ -1284,7 +1287,9 @@ let default_ectx read_file (!btl_folder ^ file_name) lctx) lctx files in *)

- builtin_size := get_size lctx; lctx + builtin_size := get_size lctx; + let lctx = read_file (!btl_folder ^ "pervasive.typer") lctx in + lctx

let default_rctx = let meta_ctx, _ = !global_substitution in

View it on GitLab: https://gitlab.com/monnier/typer/compare/f5cb3ff0ce40d3dfe8f8f6d5996b753f82a...