Stefan pushed to branch master at Stefan / Typer

Commits: 0bb921c9 by Stefan Monnier at 2017-02-24T15:04:21-05:00 Wholesale renaming

Try and follow the convention: - types and "modules" are capitalized. - functions and constructors are lower case. - in the absence of actual modules, use <module>_<name>.

- - - - -

15 changed files:

- btl/builtins.typer - btl/list.typer - btl/pervasive.typer - emacs/typer-mode.el - samples/error.typer - − samples/inductive.typer - samples/io.typer - − samples/macro.typer - − samples/qquote_temp.typer - − samples/quote.typer - src/builtin.ml - src/eval.ml - src/lparse.ml - tests/eval_test.ml - tests/macro_test.ml

Changes:

===================================== btl/builtins.typer ===================================== --- a/btl/builtins.typer +++ b/btl/builtins.typer @@ -1,4 +1,4 @@ -%%% builtins.typer --- File to initialize the builtin functions +%%% builtins.typer --- Initialize the builtin functions

%% Copyright (C) 2011-2017 Free Software Foundation, Inc. %% @@ -31,15 +31,15 @@

%%%% Base Types used in builtin functions

-% The trivial type which carries no information. +%% The trivial type which carries no information. Unit = typecons Unit unit; unit = datacons Unit unit;

-% The empty type, with no constructors: nothing can have this type. +%% The empty type, with no constructors: nothing can have this type. Void = typecons Void;

-% Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l -% Eq' : (l : TypeLevel) ≡> Type_ l -> Type_ l -> Type_ l +%% Eq : (l : TypeLevel) ≡> (t : Type_ l) ≡> t -> t -> Type_ l +%% Eq' : (l : TypeLevel) ≡> Type_ l -> Type_ l -> Type_ l Eq_refl = Built-in "Eq.refl" ((l : TypeLevel) ≡> (t : Type_ l) ≡> (x : t) ≡> Eq (t := t) x x); @@ -54,9 +54,9 @@ Eq_cast = Built-in "Eq.cast" Eq_comm : (l : TypeLevel) ≡> (t : Type_ l) ≡> (x : t) ≡> (y : t) ≡> (p : Eq (t := t) x y) -> Eq (t := t) y x; Eq_comm = lambda l t x y ≡> lambda p -> - Eq_cast (f := lambda xy -> Eq (t := t) xy x) - (p := p) - Eq_refl; + Eq_cast (f := lambda xy -> Eq (t := t) xy x) + (p := p) + Eq_refl;

%% General recursion!! %% Whether this breaks onsistency or not is a good question. @@ -86,7 +86,7 @@ Eq_comm = lambda l t x y ≡> lambda p -> Y = Built-in "Y" ((a : Type) ≡> (b : Type) ≡> (witness : a -> b) ≡> ((a -> b) -> (a -> b)) -> (a -> b));

-% Basic operators +%% Basic operators _+_ = Built-in "Int.+" (Int -> Int -> Int); _-_ = Built-in "Int.-" (Int -> Int -> Int); _*_ = Built-in "Int.*" (Int -> Int -> Int); @@ -96,13 +96,13 @@ Bool = typecons (Boolean) (true) (false); true = datacons Bool true; false = datacons Bool false;

-string_eq = Built-in "string_eq" (String -> String -> Bool); -int_eq = Built-in "int_eq" (Int -> Int -> Bool); -sexp_eq = Built-in "sexp_eq" (Sexp -> Sexp -> Bool); +String_eq = Built-in "String.=" (String -> String -> Bool); +Int_eq = Built-in "Int.=" (Int -> Int -> Bool); +Sexp_eq = Built-in "Sexp.=" (Sexp -> Sexp -> Bool);

-% ----------------------------------------------------- -% List -% ----------------------------------------------------- +%% ----------------------------------------------------- +%% List +%% -----------------------------------------------------

List : Type -> Type; %% List a = typecons List (nil) (cons a (List a)); @@ -115,45 +115,43 @@ cons = datacons List cons; %%%% Macro-related definitions

%% block_ = Built-in "block_" (List Pretoken -> Sexp); -symbol_ = Built-in "symbol_" (String -> Sexp); -string_ = Built-in "string_" (String -> Sexp); -node_ = Built-in "node_" (Sexp -> List Sexp -> Sexp); -integer_ = Built-in "integer_" (Int -> Sexp); -float_ = Built-in "float_" (Float -> Sexp); +Sexp_symbol = Built-in "Sexp.symbol" (String -> Sexp); +Sexp_string = Built-in "Sexp.string" (String -> Sexp); +Sexp_node = Built-in "Sexp.node" (Sexp -> List Sexp -> Sexp); +Sexp_integer = Built-in "Sexp.integer" (Int -> Sexp); +Sexp_float = Built-in "Sexp.float" (Float -> Sexp);

Macro = typecons (Macro) - (Macro_ (List Sexp -> Sexp)); -% (macro ((ctx : Context) ≡> (a : Type) ≡> (arg : List Sexp) -> Sexp)); - -Macro_ = datacons Macro Macro_ ; - -expand_macro_ : Macro -> List Sexp -> Sexp; -expand_macro_ m args = case m - | Macro_ f => (f args); - -sexp_dispatch_ = Built-in "sexp_dispatch_" ( - (a : Type) ≡> - Sexp - -> (node : Sexp -> List Sexp -> a) - -> (symbol : String -> a) - -> (string : String -> a) - -> (int : Int -> a) - -> (float : Float -> a) - -> (block : List Sexp -> a) - -> a - ); + (macro (List Sexp -> Sexp)); +macro = datacons Macro macro; + +Macro_expand : Macro -> List Sexp -> Sexp; +Macro_expand m args = case m + | macro f => (f args); + +Sexp_dispatch = Built-in "Sexp.dispatch" ( + (a : Type) ≡> + Sexp + -> (node : Sexp -> List Sexp -> a) + -> (symbol : String -> a) + -> (string : String -> a) + -> (int : Int -> a) + -> (float : Float -> a) + -> (block : List Sexp -> a) + -> a + );

%%%% Monads

-% Builtin bind -bind = Built-in "bind" ( - (a : Type) ≡> - (b : Type) ≡> - IO a -> (a -> IO b) -> (IO b)); +%% Builtin bind +IO_bind = Built-in "IO.bind" ( + (a : Type) ≡> + (b : Type) ≡> + IO a -> (a -> IO b) -> (IO b));

-% return = Built-in "return" ((a : Type) ≡> a -> IO a); +%% return = Built-in "return" ((a : Type) ≡> a -> IO a);

-% File monad +%% File monad

%% `runIO` should have type IO Unit -> b -> b %% or IO a -> b -> b, which means "run the IO, throw away the result, @@ -161,11 +159,11 @@ bind = Built-in "bind" ( %% is actually crucial to make sure the result of runIO is used, otherwise %% the whole call would look like a dead function call and could be %% optimized away! -run-io = Built-in "run-io" ((a : Type) ≡> IO Unit -> a -> a); +IO_run = Built-in "IO.run" ((a : Type) ≡> IO Unit -> a -> a);

-% Define operations on file handle. -open = Built-in "open" (String -> String -> IO FileHandle); -write = Built-in "write" (FileHandle -> String -> IO Unit); -read = Built-in "read" (FileHandle -> Int -> IO String); +%% Define operations on file handle. +File_open = Built-in "File.open" (String -> String -> IO FileHandle); +File_write = Built-in "File.write" (FileHandle -> String -> IO Unit); +File_read = Built-in "File.read" (FileHandle -> Int -> IO String);

%%% builtins.typer ends here.

===================================== btl/list.typer ===================================== --- a/btl/list.typer +++ b/btl/list.typer @@ -1,33 +1,3 @@ -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)); - -% 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; - accumulate : (t : Type) ≡> (acc-op : (t -> t -> t)) -> (init : t) -> (list : List t) -> t; accumulate = lambda (t : Type) ≡> lambda (acc-op : (t -> t -> t)) -> @@ -37,11 +7,3 @@ accumulate = lambda (t : Type) ≡> | cons hd tl => accumulate acc-op (acc-op init hd) tl | nil => init;

-map : (a : Type) ≡> (b : Type) ≡> (list : List a) -> (f : a -> b) -> List b; -map = lambda (a : Type) ≡> - lambda (b : Type) ≡> - lambda (list : List a) -> - lambda (f : a -> b) -> - case list - | cons hd tl => (cons (f hd) (map tl f)) - | nil => nil;

===================================== btl/pervasive.typer ===================================== --- a/btl/pervasive.typer +++ b/btl/pervasive.typer @@ -36,163 +36,176 @@ Option = typecons (Option (a : Type)) (none) (some a); some = datacons Option some; none = datacons Option none;

+%%% Good 'ol combinators + +I : (a : Type) ≡> a -> a; +I = lambda a ≡> lambda x -> x; + +K : (a : Type) ≡> a -> (b : Type) ≡> b -> a; +K = lambda a ≡> lambda x -> lambda b ≡> lambda y -> x; + %%%% 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)); + | 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); + | 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_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) ≡> a -> List 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; + | nil => none + | cons hd tl => some hd; + +List_head : (a : Type) ≡> a -> List a -> a; +List_head = lambda a ≡> lambda x xs -> case xs + | cons x _ => x + | nil => x;

List_tail : (a : Type) ≡> List a -> List a; List_tail = lambda a ≡> lambda xs -> case xs - | nil => nil - | cons hd tl => tl; + | 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; + | nil => nil + | cons x xs => cons (f x) (List_map f xs);

%%%% Quasi-Quote macro

-%% f = (quote (uquote x) * x) (node _*_ [(node_ unquote "x") "x"]) +%% f = (quote (uquote x) * x) (node _*_ [(Sexp_node unquote "x") "x"]) %% -%% f = node_ "*" cons (x, cons (symbol_ "x") nil)) +%% f = Sexp_node "*" cons (x, cons (Sexp_symbol "x") nil)) %% %% => x

+%% An Sexp which we use to represents an error. +Sexp_error = Sexp_symbol "<error>"; + 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; +quote1 x = let k = K x; + node op y = case (Sexp_eq op (Sexp_symbol "uquote")) + | true => List_head Sexp_error y + | false => Sexp_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)); +%% quote definition +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 = - node_ (symbol_ "_=_") - (cons var-name - (cons value-expr nil)); + Sexp_node (Sexp_symbol "_=_") + (cons var-name + (cons value-expr nil));

chain-decl : Sexp -> Sexp -> Sexp; chain-decl a b = - node_ (symbol_ "_;_") (cons a (cons b nil)); + 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 - (node_ (symbol_ "datacons") - (cons type-name - (cons ctor-name nil))); + (Sexp_node (Sexp_symbol "datacons") + (cons type-name + (cons ctor-name nil)));

-% buil type annotation -% var-name : type-expr; +%% buil type annotation +%% var-name : type-expr; make-ann : Sexp -> Sexp -> Sexp; make-ann var-name type-expr = - node_ (symbol_ "_:_") - (cons var-name - (cons type-expr nil)); + Sexp_node (Sexp_symbol "_:_") + (cons var-name + (cons type-expr nil));

type-impl = lambda (x : List Sexp) -> - % x follow the mask -> (_|_ Nat zero (succ Nat)) - % Type name --^ ^------^ constructors - - % Return a list contained inside a node sexp - let get-list : Sexp -> List Sexp; - get-list node = sexp_dispatch_ (a := List Sexp) node - (lambda op lst -> lst) % Nodes - (lambda _ -> nil) % Symbol - (lambda _ -> nil) % String - (lambda _ -> nil) % Integer - (lambda _ -> nil) % Float - (lambda _ -> nil) in % List of Sexp - - % Get a name from a sexp - % - (name t) -> name - % - name -> name - let get-name : Sexp -> Sexp; + %% x follow the mask -> (_|_ Nat zero (succ Nat)) + %% Type name --^ ^------^ constructors + + %% Return a list contained inside a node sexp + let knil = K nil; + kerr = K Sexp_error; + + get-list : Sexp -> List Sexp; + get-list node = Sexp_dispatch node + (lambda op lst -> lst) % Nodes + knil % Symbol + knil % String + knil % Integer + knil % Float + knil; % List of Sexp + + %% Get a name (symbol) from a sexp + %% - (name t) -> name + %% - name -> name + get-name : Sexp -> Sexp; get-name sxp = - sexp_dispatch_ (a := Sexp) sxp - (lambda op lst -> get-name op) % Nodes - (lambda str -> symbol_ str) % Symbol - (lambda _ -> symbol_ "error") % String - (lambda _ -> symbol_ "error") % Integer - (lambda _ -> symbol_ "error") % Float - (lambda _ -> symbol_ "error") in % List of Sexp + Sexp_dispatch sxp + (lambda op _ -> get-name op) % Nodes + (lambda _ -> sxp) % Symbol + kerr % String + kerr % Integer + kerr % Float + kerr; % List of Sexp

- let get-head : List Sexp -> Sexp; - get-head x = case x - | cons hd _ => hd - | nil => symbol_ "error" in + get-head = List_head Sexp_error;

- % Get expression - let expr = get-head x in + %% Get expression + expr = get-head x;

- % Expression is node_ (symbol_ "|") (list) - % we only care about the list bit - let lst = get-list expr in + %% Expression is Sexp_node (Sexp_symbol "|") (list) + %% we only care about the list bit + lst = get-list expr;

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

- let type-name = get-name name in + type-name = get-name name;

- % Create the inductive type definition - let inductive = node_ (symbol_ "typecons") - (cons name ctor) in + %% Create the inductive type definition + inductive = Sexp_node (Sexp_symbol "typecons") + (cons name ctor);

- let decl = make-decl type-name inductive in + decl = make-decl type-name inductive;

- % Add constructors - let ctors = - let for-each : List Sexp -> Sexp -> Sexp; - for-each ctr acc = case ctr - | cons hd tl => ( - let acc2 = chain-decl (make-cons (get-name hd) type-name) acc in - for-each tl acc2) - | nil => acc - in for-each ctor (node_ (symbol_ "_;_") nil) in + %% Add constructors + ctors = let for-each : List Sexp -> Sexp -> Sexp; + for-each ctr acc = case ctr + | cons hd tl => + let acc2 = chain-decl (make-cons (get-name hd) + type-name) + acc + in for-each tl acc2 + | nil => acc + in for-each ctor (Sexp_node (Sexp_symbol "_;_") nil)

- % return decls - (chain-decl decl % inductive type declaration - ctors); % constructor declarations + %% return decls + in chain-decl decl % inductive type declaration + ctors; % constructor declarations

-type_ = Macro_ type-impl; +type_ = macro type-impl;

%%%% Backward compatibility

@@ -202,15 +215,15 @@ 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 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. +%% Like Bool, except that it additionally carries the meaning of its value. Decidable = typecons (Decidable (prop : Type)) (true (p ::: prop)) (false (p ::: Not prop));

===================================== emacs/typer-mode.el ===================================== --- a/emacs/typer-mode.el +++ b/emacs/typer-mode.el @@ -46,6 +46,9 @@ (modify-syntax-entry ?% "<" st) (modify-syntax-entry ?\n ">" st) (modify-syntax-entry ?" """ st) + (modify-syntax-entry ?; "." st) + (modify-syntax-entry ?, "." st) + (modify-syntax-entry ?\≡ "_" st) (modify-syntax-entry ?\ "\" st) (modify-syntax-entry ?{ "(}" st) (modify-syntax-entry ?} "){" st) @@ -166,7 +169,14 @@ ;; along the lines of what's done in Tuareg. (pcase (cons kind token) (`(:before . "|") (smie-rule-parent)) + (`(:before . "(") (if (smie-rule-hanging-p) (smie-rule-parent))) + (`(:before . ,(or "case" "lambda")) + (and (not (smie-rule-bolp)) + (smie-rule-prev-p "=" "->" "=>" "≡>") + (smie-rule-parent (if (smie-rule-prev-p "=") 2)))) (`(:after . "=") 2) + (`(:after . ,(or "->" "=>" "≡>")) + (if (smie-rule-parent-p "|") 2 0)) ))

;;;###autoload

===================================== samples/error.typer ===================================== --- a/samples/error.typer +++ b/samples/error.typer @@ -3,7 +3,7 @@ % * % * --------------------------------------------------------------------------- % * -% * Copyright (C) 2011-2016 Free Software Foundation, Inc. +% * Copyright (C) 2011-2017 Free Software Foundation, Inc. % * % * Author: Pierre Delaunay pierre.delaunay@hec.ca % * Keywords: languages, lisp, dependent types. @@ -73,11 +73,11 @@ fun2 n = case n

% h = fun2 1 2;

-% [X] Fatal [Ln 6, cl 6] LPARSE Macro_ expects `(List Sexp) -> Sexp` +% [X] Fatal [Ln 6, cl 6] LPARSE macro expects `(List Sexp) -> Sexp` % > Vcons: (cons 2 (nil)) % > Root: n

-% m = Macro_ (lambda (n : Int) -> n); +% m = macro (lambda (n : Int) -> n); % v = (m 2);

% [X] Fatal [Ln 43, cl 5] LPARSE Expected Type Arrow ( _ -> _ )

===================================== samples/inductive.typer deleted ===================================== --- a/samples/inductive.typer +++ /dev/null @@ -1,128 +0,0 @@ -% build a declaration -% var-name = value-expr; -make-decl : Sexp -> Sexp -> Sexp; -make-decl var-name value-expr = - node_ (symbol_ "_=_") - (cons var-name - (cons value-expr nil)); - -chain-decl : Sexp -> Sexp -> Sexp; -chain-decl a b = - node_ (symbol_ "_;_") (cons a (cons b nil)); - -% build datacons -% ctor-name = datacons type-name ctor-name; -make-cons : Sexp -> Sexp -> Sexp; -make-cons ctor-name type-name = - make-decl ctor-name - (node_ (symbol_ "datacons") - (cons type-name - (cons ctor-name nil))); - -% buil type annotation -% var-name : type-expr; -make-ann : Sexp -> Sexp -> Sexp; -make-ann var-name type-expr = - node_ (symbol_ "_:_") - (cons var-name - (cons type-expr nil)); - -type-impl = lambda (x : List Sexp) -> - % x follow the mask -> (_|_ Nat zero (succ Nat)) - % Type name --^ ^------^ constructors - - % Return a list contained inside a node sexp - let get-list : Sexp -> List Sexp; - get-list node = sexp_dispatch_ (a := List Sexp) node - (lambda op lst -> lst) % Nodes - (lambda _ -> nil) % Symbol - (lambda _ -> nil) % String - (lambda _ -> nil) % Integer - (lambda _ -> nil) % Float - (lambda _ -> nil) in % List of Sexp - - % Get a name from a sexp - % - (name t) -> name - % - name -> name - let get-name : Sexp -> Sexp; - get-name sxp = - sexp_dispatch_ (a := Sexp) sxp - (lambda op lst -> get-name op) % Nodes - (lambda str -> symbol_ str) % Symbol - (lambda _ -> symbol_ "error") % String - (lambda _ -> symbol_ "error") % Integer - (lambda _ -> symbol_ "error") % Float - (lambda _ -> symbol_ "error") in % List of Sexp - - let get-head : List Sexp -> Sexp; - get-head x = case x - | cons hd _ => hd - | nil => symbol_ "error" in - - % Get expression - let expr = get-head x in - - % Expression is node_ (symbol_ "|") (list) - % we only care about the list bit - let lst = get-list expr in - - % head is (node_ type-name (arg list)) - let name = get-head lst; - ctor = tail lst in - - let type-name = get-name name in - - % Create the inductive type definition - let inductive = node_ (symbol_ "typecons") - (cons name ctor) in - - let decl = make-decl type-name inductive in - - % Add constructors - let ctors = - let for-each : List Sexp -> Sexp -> Sexp; - for-each ctr acc = case ctr - | cons hd tl => ( - let acc2 = chain-decl (make-cons (get-name hd) type-name) acc in - for-each tl acc2) - | nil => acc - in for-each ctor (node_ (symbol_ "_;_") nil) in - - % return decls - (chain-decl decl % inductive type declaration - ctors); % constructor declarations - - -type_ = Macro_ type-impl; - -% (type_ (_|_ (Either t1 t2) (either-first t1) (either-second t2))) -%type Either t1 t2 -% | either-first t1 -% | either-second t2; - -type A - | a Int; - -type Pair (t1 : Type) (t2 : Type) - | pair t1 t2; - -type Point (t : Type) - | point (x : t) (y : t); - -%get-first : (a : Type) => (b : Type) => Pair a b -> a; -%get-second : (a : Type) => (b : Type) => Pair a b -> b; - -%get-first p = case p | pair a b => a; -%get-second p = case p | pair a b => b; - -%get-x : (a : Type) => Point a -> a; -%get-y : (a : Type) => Point a -> a; -%get-x p = case p | point x y => x; -%get-y p = case p | point x y => y; - - -% transformed to: -% Nat : Type; -% Nat = typecons (Nat) (succ Nat) (zero); -% zero = datacons Nat zero; -% succ = datacons Nat succ;

===================================== samples/io.typer ===================================== --- a/samples/io.typer +++ b/samples/io.typer @@ -1,3 +1,5 @@ +%%% BEWARE: This file is not valid Typer! + type Location | location (line : col) (col : Int) (file : String);

@@ -48,7 +50,7 @@ sexp_string s = (lambda str val -> str ++ " " ++ sexp_string val) "" args in "(" ++ (sexp_string op) ++ args ++ ")";

-% is there a simplier way ? +% is there a simpler way ? sexp_equal : Sexp -> Sexp -> Bool; sexp_equal a b = case a

===================================== samples/macro.typer deleted ===================================== --- a/samples/macro.typer +++ /dev/null @@ -1,79 +0,0 @@ -% -% The Hardcore way of building a Macro -% - -sqr_fun = node_ (symbol_ "lambda_->_") (symbol_ "x") - (node_ (symbol_ "_*_") (symbol_ "x") (symbol_ "x")); - -sqr_type = node_ (symbol_ "_->_") (symbol_ "Int") (symbol_ "Int"); - -give_type : Sexp -> Sexp -> Sexp; -give_type = lambda expr -> - lambda tp -> - node_ (symbol_ "_:_") expr tp; - -sqr = Macro_ (give_type sqr_fun sqr_type); - -m1 = (sqr 2); - -% -% The easy way -% - -%Type List a = -% | Nil -% | Cons a (list a); - - -sqr = Macro_ (qquote (lambda (x : Int) -> x * x)); - -m2 = (sqr 2); - -% -% Use unquote to replace a variable by its value -% - -my_fun = let a = 2 in - Macro_ lambda (x : Sexp) -> qquote ((uquote x) * (uquote (integer_ a)))); - -my_fun = - Macro_ lambda (x : Sexp) -> qquote (lambda (y : Int) -> (uquote x) * (uquote y))); - - -quote = Maocr_ quote -quote e = case early - | Node () - -main = (my_fun 3); 3 * 2 - - -% -% Hygiene -% - -fun1 = lambda (x : Int) -> x * 2; -fun2 = Macro_ (lambda (x : Int) -> (qquote x * (fun1 x))); -fun1 = lambda (x : Int) -> x * 3; - -m3 = (fun2 2); % if Hygienic == 8 - % else == 12 - -% -% Depends when the macro is lexp and evaluated... -% lexp_parsing the macro early would fix its index -% and prevent the presented issue -% - -% We can force function inlining - -%sqr_inline = lambda (x : Int) -> -% let a = x in -% Macro_ (qquote ((uquote x) * ((uquote x)))); - - -% Macro_ (qquote (lambda (x : Int) -> x * x)); -% sqr2 = (inline (lambda (x : Int) -> x * x)); - - - -

===================================== samples/qquote_temp.typer deleted ===================================== --- a/samples/qquote_temp.typer +++ /dev/null @@ -1,14 +0,0 @@ - - -sqr = Macro_ (lambda (x : List Sexp) -> - let hd = head Sexp x in - (node_ (symbol_ "_*_") (cons hd (cons hd nil)))); - - - - -%nd = node_ (symbol_ "_+_") (cons (symbol_ "x") (cons (symbol_ "x") nil)); -%tst = cons nd nil; -%tst = (cons (symbol_ "x") (cons (symbol_ "x") nil)); -%main = qquote tst; -%main = Macro_ lamda \ No newline at end of file

===================================== samples/quote.typer deleted ===================================== --- a/samples/quote.typer +++ /dev/null @@ -1,89 +0,0 @@ -% -% f = (qquote (uquote x) * x) (node _*_ [(node_ unquote "x") "x"]) -% -% f = node_ "*" cons (x, cons (symbol_ "x") nil)) -% -% -% => x - -get-head : List Sexp -> Sexp; -get-head x = case x - | cons hd _ => hd - | nil => symbol_ "error"; - -symbol = lambda (y : String) -> (symbol_ y); -string = lambda (y : String) -> (string_ y); -integer = lambda (y : Int) -> (integer_ y); -float = lambda (y : Float) -> (float_ y); -block = lambda (y : List Sexp) -> (block_ y); - -quote' : List Sexp -> List Sexp; - -has-uquote : List Sexp -> Sexp; -has-uquote = lambda y -> - let expr = case y - | cons hd tl => hd - | nil => symbol_ "uquote expects one argument" in - expr; - -% traverse nodes -node : Sexp -> List Sexp -> Sexp; -node = lambda (op : Sexp) -> - lambda (y : List Sexp) -> - case (sexp_eq op (symbol_ "uquote")) - | true => has-uquote y - | false => node_ op (quote' y); - -% tree traversal -quote' = lambda (x : List Sexp) -> - case x - | cons hd tl => ( - let nhd = sexp_dispatch_ (a := Sexp) hd node symbol string integer float block in - let ntl = quote' tl in - cons nhd ntl) - - | nil => nil; - -% quote definition -qq = lambda (x : List Sexp) -> get-head (quote' x); -quote = Macro_ qq; - -% Raw -my_sqr = lambda (x : List Sexp) -> - let hd = (case x - | cons hd tl => hd - | nil => symbol_ "x") : Sexp in - (node_ (symbol_ "_*_") (cons hd (cons hd nil))); - -% Quote -qq_sqr' = lambda (args : List Sexp) -> - let hd : Sexp; - hd = case args - | cons hd tl => hd - | nil => symbol_ "sqr expects a single argument" in - - quote ((uquote hd) * (uquote hd)); - -sqr = Macro_ my_sqr; -qqsqr = Macro_ qq_sqr'; - -% fun = Macro_ my_fun; -% main = fun 2; - -my_fun = lambda (arg : List Sexp) -> - let x = sqr 2 in - integer_ 2; - -fun = Macro_ my_fun; -main = qqsqr 2; - -% x = 2; -% sqr = Macro_ my_fun; - -% main = sqr 2; -% a = Macro_ (lambda x -> quote (2 + 2)); - -% main = a Unit; -% main = let x = 2 in quote (x * x); -% main = let x = 2 in quote ((uquote x) * (uquote x)); -% add = Macro_ my_add;

===================================== src/builtin.ml ===================================== --- a/src/builtin.ml +++ b/src/builtin.ml @@ -1,6 +1,6 @@ (* builtin.ml --- Infrastructure to define built-in primitives * - * Copyright (C) 2016 Free Software Foundation, Inc. + * Copyright (C) 2016-2017 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -73,7 +73,7 @@ let predef_name = [ "true"; "false"; "Macro"; - "expand_macro_"; + "Macro_expand"; ]

(* FIXME: Actually, we should map the predefs to *values* since that's

===================================== src/eval.ml ===================================== --- a/src/eval.ml +++ b/src/eval.ml @@ -140,46 +140,43 @@ let _ = add_binary_iop "+" (+);

let make_symbol loc depth args_val = match args_val with | [Vstring str] -> Vsexp (Symbol (loc, str)) - | _ -> error loc "symbol_ expects one string as argument" + | _ -> error loc "Sexp.symbol expects one string as argument"

-let make_node loc depth args_val = +let make_node loc depth args_val = match args_val with + | [Vsexp (op); lst] -> + let args = v2o_list lst in

- let op, tlist = match args_val with - | [Vsexp(op); lst] -> op, lst - | op::_ -> value_error loc op "node_ expects one 'Sexp' got: " - | _ -> typer_unreachable "-" in + let s = List.map (fun g -> match g with + | Vsexp(sxp) -> sxp + (* eval transform sexp into those... *) + (* FIXME: Really? Why? *) + | Vint (i) -> Integer(dloc, i) + | Vstring (s) -> String(dloc, s) + | _ -> + (* print_rte_ctx ctx; *) + value_error loc g "Sexp.node expects `List Sexp` second as arguments") args in

- (* value_print tlist; print_string "\n"; *) + Vsexp (Node (op, s))

- let args = v2o_list tlist in + | _ -> error loc "Sexp.node expects a `Sexp` and a `List Sexp`"

- let s = List.map (fun g -> match g with - | Vsexp(sxp) -> sxp - (* eval transform sexp into those... *) - | Vint (i) -> Integer(dloc, i) - | Vstring (s) -> String(dloc, s) - | _ -> - (* print_rte_ctx ctx; *) - value_error loc g "node_ expects 'List Sexp' second as arguments") args in - - Vsexp(Node(op, s))

let make_string loc depth args_val = match args_val with | [Vstring str] -> Vsexp (String (loc, str)) - | _ -> error loc "string_ expects one string as argument" + | _ -> error loc "Sexp.string expects one string as argument"

let make_integer loc depth args_val = match args_val with | [Vint (str)] -> Vsexp (Integer (loc, str)) - | _ -> error loc "integer_ expects one integer as argument" + | _ -> error loc "Sexp.integer expects one integer as argument"

let make_float loc depth args_val = match args_val with | [Vfloat x] -> Vsexp (Float (loc, x)) - | _ -> error loc "float_ expects one float as argument" + | _ -> error loc "Sexp.float expects one float as argument"

(* let make_block loc depth args_val = match args_val with * | [Vblock b] -> Vsexp (Block (loc, b)) - * | _ -> error loc "float_ expects one block as argument" *) + * | _ -> error loc "Sexp.block expects one block as argument" *)

(* FIXME: We're not using predef here. This will break if we change * the definition of `Bool` in builtins.typer. *) @@ -193,31 +190,29 @@ let string_eq loc depth args_val = match args_val with

let int_eq loc depth args_val = match args_val with | [Vint i1; Vint i2] -> o2v_bool (i1 = i2) - | _ -> error loc "int_eq expects 2 integers" + | _ -> error loc "Int.= expects 2 integers"

let sexp_eq loc depth args_val = match args_val with | [Vsexp (s1); Vsexp (s2)] -> o2v_bool (sexp_equal s1 s2) - | _ -> error loc "sexp_eq expects 2 sexps" - -let open_impl loc depth args_val = + | _ -> error loc "Sexp.= expects 2 sexps"

- let file, mode = match args_val with - | [Vstring(file_name); Vstring(mode)] -> file_name, mode - | _ -> error loc "open expects 2 strings" in +let open_impl loc depth args_val = match args_val with + | [Vstring (file); Vstring (mode)] -> + (* open file *) (* return a file handle *) + Vcommand(fun () -> + match mode with + | "r" -> Vin (open_in file) + | "w" -> Vout (open_out file) + | _ -> error loc "wrong open mode")

- (* open file *) (* return a file handle *) - Vcommand(fun () -> - match mode with - | "r" -> Vin(open_in file) - | "w" -> Vout(open_out file) - | _ -> error loc "wrong open mode") + | _ -> error loc "File.open expects 2 strings"

let read_impl loc depth args_val = match args_val with (* FIXME: Either rename it to "readline" and drop the second arg, * or actually pay attention to the second arg. *) | [Vin channel; Vint n] -> Vstring (input_line channel) | _ -> List.iter (fun v -> value_print v; print_string "\n") args_val; - error loc "read expects an in_channel" + error loc "File.read expects an in_channel"

let write_impl loc depth args_val = match args_val with @@ -225,7 +220,7 @@ let write_impl loc depth args_val = match args_val with (* FIXME: This should be the unit value! *) Vundefined | _ -> List.iter (fun v -> value_print v) args_val; - error loc "write expects an out_channel and a string" + error loc "File.write expects an out_channel and a string"

let rec _eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) = @@ -421,17 +416,17 @@ and bind_impl loc depth args_val = | [Vcommand (cmd); callback] -> (* bind returns another Vcommand *) Vcommand (fun () -> eval_call loc trace_dum depth callback [cmd ()]) - | _ -> error loc "Wrong number of args or wrong first arg value in `bind`" + | _ -> error loc "Wrong number of args or wrong first arg value in `IO.bind`"

and run_io loc depth args_val =

let io, ltp = match args_val with | [io; ltp] -> io, ltp - | _ -> error loc "run-io expects 2 arguments" in + | _ -> error loc "IO.run expects 2 arguments" in

let cmd = match io with | Vcommand (cmd) -> cmd - | _ -> error loc "run-io expects a monad as first argument" in + | _ -> error loc "IO.run expects a monad as first argument" in

(* run given command *) let _ = cmd () in @@ -572,21 +567,21 @@ let nop_fun loc _ vs = match vs with let register_built_functions () = List.iter (fun (name, f, arity) -> add_builtin_function name f arity) [ - (* ("block_" , make_block, 1); *) - ("symbol_" , make_symbol, 1); - ("string_" , make_string, 1); - ("integer_" , make_integer, 1); - ("float_" , make_float, 1); - ("node_" , make_node, 2); - ("sexp_dispatch_", sexp_dispatch, 7); - ("string_eq" , string_eq, 2); - ("int_eq" , int_eq, 2); - ("sexp_eq" , sexp_eq, 2); - ("open" , open_impl, 2); - ("bind" , bind_impl, 2); - ("run-io" , run_io, 2); - ("read" , read_impl, 2); - ("write" , write_impl, 2); + (* ("Sexp.block" , make_block, 1); *) + ("Sexp.symbol" , make_symbol, 1); + ("Sexp.string" , make_string, 1); + ("Sexp.integer" , make_integer, 1); + ("Sexp.float" , make_float, 1); + ("Sexp.node" , make_node, 2); + ("Sexp.dispatch" , sexp_dispatch, 7); + ("String.=" , string_eq, 2); + ("Int.=" , int_eq, 2); + ("Sexp.=" , sexp_eq, 2); + ("File.open" , open_impl, 2); + ("IO.bind" , bind_impl, 2); + ("IO.run" , run_io, 2); + ("File.read" , read_impl, 2); + ("File.write" , write_impl, 2); ("Eq.refl" , arity0_fun, 0); ("Eq.cast" , nop_fun, 1); ("Y" , y_operator, 1);

===================================== src/lparse.ml ===================================== --- a/src/lparse.ml +++ b/src/lparse.ml @@ -375,7 +375,7 @@ and get_implicit_arg ctx loc name t = * to distinguish two cases. * Better yet: let's not do any table lookup here. Instead, * call a `default-arg-filler` function, implemented in Typer, - * just like `expand_macro_` function. That one can then look + * just like `Macro_expand` function. That one can then look * things up in a table and/or do anything else it wants. *) let v = lexp_expand_macro loc attr [] ctx (Some t) in

@@ -868,7 +868,7 @@ and lexp_expand_macro loc macro_funct sargs ctx (ot : ltype option)

(* Build the function to be called *) let meta_ctx, _ = !global_substitution in - let macro_expand = BI.get_predef "expand_macro_" ctx in + let macro_expand = BI.get_predef "Macro_expand" ctx in (* FIXME: Rather than remember the lexp of "expand_macro" in predef, * we should remember its value so we don't have to re-eval it everytime. *) let macro_expand = lexp_eval meta_ctx ctx macro_expand in

===================================== tests/eval_test.ml ===================================== --- a/tests/eval_test.ml +++ b/tests/eval_test.ml @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * Copyright (C) 2011-2017 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -284,13 +284,13 @@ let _ = test_eval_eqv_named let _ = (add_test "EVAL" "Monads" (fun () ->

let dcode = " - c = bind (open "./_build/w_file.txt" "w") - (lambda f -> write f "Hello2"); + c = IO_bind (File_open "./_build/w_file.txt" "w") + (lambda f -> File_write f "Hello2"); " in

let rctx, ectx = eval_decl_str dcode ectx rctx in

- let rcode = "run-io c 2" in + let rcode = "IO_run c 2" in

(* Eval defined lambda *) let ret = eval_expr_str rcode ectx rctx in @@ -344,7 +344,7 @@ let _ = test_eval_eqv_named "Implicit Arguments"

"default = new-attribute Macro; - default = add-attribute default Int (Macro_ (lambda (lst : List Sexp) -> integer_ 1)); + default = add-attribute default Int (macro (lambda (lst : List Sexp) -> Sexp_integer 1));

fun = lambda (x : Int) => lambda (y : Int) ->

===================================== tests/macro_test.ml ===================================== --- a/tests/macro_test.ml +++ b/tests/macro_test.ml @@ -3,7 +3,7 @@ * * --------------------------------------------------------------------------- * - * Copyright (C) 2011-2016 Free Software Foundation, Inc. + * Copyright (C) 2011-2017 Free Software Foundation, Inc. * * Author: Pierre Delaunay pierre.delaunay@hec.ca * Keywords: languages, lisp, dependent types. @@ -49,11 +49,11 @@ let _ = (add_test "MACROS" "macros base" (fun () -> my_fun = lambda (x : List Sexp) -> let hd = (case x | cons hd tl => hd - | nil => symbol_ "x") : Sexp in - (node_ (symbol_ "_*_") + | nil => Sexp_symbol "x") : Sexp in + (Sexp_node (Sexp_symbol "_*_") (cons hd (cons hd nil)));

- sqr = Macro_ my_fun; + sqr = macro my_fun; " in

let rctx, ectx = eval_decl_str dcode ectx rctx in @@ -72,17 +72,17 @@ let _ = (add_test "MACROS" "macros decls" (fun () -> let dcode = " decls-impl = lambda (x : List Sexp) -> let chain-decl : Sexp -> Sexp -> Sexp; - chain-decl a b = node_ (symbol_ "_;_") (cons a (cons b nil)) in + chain-decl a b = Sexp_node (Sexp_symbol "_;_") (cons a (cons b nil)) in

let make-decl : String -> Int -> Sexp; make-decl name val = - (node_ (symbol_ "_=_") (cons (symbol_ name) (cons (integer_ val) nil))) in + (Sexp_node (Sexp_symbol "_=_") (cons (Sexp_symbol name) (cons (Sexp_integer val) nil))) in

let d1 = make-decl "a" 1 in let d2 = make-decl "b" 2 in chain-decl d1 d2;

- my-decls = Macro_ decls-impl; + my-decls = macro decls-impl;

my-decls Nat;" in

View it on GitLab: https://gitlab.com/monnier/typer/commit/0bb921c96b13c0a9a257df255c3a380a6887...