Jonathan Graveline pushed to branch graveline at Stefan / Typer

Commits: caa73195 by Jonathan Graveline at 2018-08-24T18:33:07Z Revised comments, trying to be more clear

- - - - - cd2381bc by Jonathan Graveline at 2018-08-24T19:46:34Z New unit test for `plain-let`

Revision of bbst.typer and table.typer

- - - - - 6ef13572 by Jonathan Graveline at 2018-08-27T19:01:33Z More comments in samples/myers.typer

Basic unit tests on Myers list in samples/myers_test.typer

- - - - -

16 changed files:

- btl/builtins.typer - btl/case.typer - btl/do.typer - btl/list.typer - btl/pervasive.typer - btl/plain-let.typer - btl/polyfun.typer - btl/tuple.typer - samples/batch_test.typer - samples/bbst.typer - samples/bbst_test.typer - samples/myers.typer - + samples/myers_test.typer - + samples/plain_let_test.typer - samples/table.typer - samples/table_test.typer

Changes:

===================================== btl/builtins.typer ===================================== @@ -208,13 +208,25 @@ Parser_newest = Built-in "Parser.newest" : Sexp -> List Sexp;

%%%% Array (without IO, but they could be added easily)

+%% +%% Array_set is in O(N) where N is the length +%% +Array_set = Built-in "Array.set" : (a : Type) ≡> Int -> a -> Array a -> Array a; + +%% +%% Array_append is in O(N) where N is the length +%% Array_append = Built-in "Array.append" : (a : Type) ≡> a -> Array a -> Array a; + Array_create = Built-in "Array.create" : (a : Type) ≡> Int -> a -> Array a; Array_length = Built-in "Array.length" : (a : Type) ≡> Array a -> Int; -Array_set = Built-in "Array.set" : (a : Type) ≡> Int -> a -> Array a -> Array a; Array_get = Built-in "Array.get" : (a : Type) ≡> a -> Int -> Array a -> a;

-% let Typer deduce the value of (a : Type) +%% +%% It returns an empty array +%% +%% let Typer deduce the value of (a : Type) +%% Array_empty = Built-in "Array.empty" : (a : Type) ≡> Unit -> Array a;

%%%% Monads @@ -246,10 +258,13 @@ File_read = Built-in "File.read" : FileHandle -> Int -> IO String; Sys_cpu_time = Built-in "Sys.cpu_time" : Unit -> IO Float; Sys_exit = Built-in "Sys.exit" : Int -> IO Unit;

+%% %% Ref (modifiable value) - -% Ref : Type -> Type; -% Ref = typecons (Ref (a : Type)) (Ref a); +%% +%% Conceptualy: +%% Ref : Type -> Type; +%% Ref = typecons (Ref (a : Type)) (Ref a); +%%

Ref_make = Built-in "Ref.make" : (a : Type) ≡> a -> IO (Ref a); Ref_read = Built-in "Ref.read" : (a : Type) ≡> Ref a -> IO a; @@ -259,7 +274,7 @@ Ref_write = Built-in "Ref.write" : (a : Type) ≡> a -> Ref a -> IO Unit; %% gensym for macro %% Generate pseudo-unique symbol %% At least they cannot be obtained outside macro -%% In macro you should NOT use symbol of the form ` %gensym% ...` +%% In macro you should NOT use symbol of the form " %gensym% ..." %% gensym = Built-in "gensym" : Unit -> IO Sexp;

@@ -302,7 +317,7 @@ Elab_nth-arg' = Built-in "Elab.nth-arg" : String -> Int -> Elab_Context -> Strin

%% %% Get the position of a field in a constructor -%% It return -1 in case something isn't defined +%% It return -1 in case the field isn't defined %% see pervasive.typer for a more convenient function %% Elab_arg-pos' = Built-in "Elab.arg-pos" : String -> String -> Elab_Context -> Int; @@ -316,12 +331,13 @@ Elab_debug-doc = Built-in "Elab.debug-doc" : String -> Elab_Context -> String;

%% %% Print message and/or fail (terminate) -%% These message are registered like any other error +%% These messages are registered like any other error %% And location is printed before the error +%%

%% %% Voluntarily fail -%% for exemple if next unit tests are not worth testing +%% use case: next unit tests are not worth testing %% %% Takes a "section" and a "message" as argument %% @@ -347,12 +363,33 @@ Test_info = Built-in "Test.info" : String -> String -> IO Unit; %% Test_location = Built-in "Test.location" : Unit -> String;

+%%% +%%% Do some test which print a message: "[ OK]" or "[FAIL]" +%%% followed by a message passed as argument +%%% + %% -%% Do some test which print a message: "[ OK]" or "[FAIL]" +%% Takes a message and a boolean which should be true +%% Returns true if the boolean was true %% Test_true = Built-in "Test.true" : String -> Bool -> IO Bool; + +%% +%% Takes a message and a boolean which should be false +%% Returns true if the boolean was false +%% Test_false = Built-in "Test.false" : String -> Bool -> IO Bool; + +%% +%% Takes a message and two arbitrary value of the same type +%% Returns true when the two value are equal +%% Test_eq = Built-in "Test.eq" : (a : Type) ≡> String -> a -> a -> IO Bool; + +%% +%% Takes a message and two arbitrary value of the same type +%% Returns true when the two value are not equal +%% Test_neq = Built-in "Test.neq" : (a : Type) ≡> String -> a -> a -> IO Bool;

%%% builtins.typer ends here.

===================================== btl/case.typer ===================================== @@ -14,9 +14,11 @@ %%%% Another problem is that this macro is dependent of tuple implementation %%%%

+%% %% Move IO outside List (from element to List) %% (Was helpful for me when translating code that used to not be IO code) %% (The function's type explain everything) +%% io-list : List (IO ?a) -> IO (List ?a); io-list l = let ff : IO (List ?a) -> IO ?a -> IO (List ?a); @@ -90,12 +92,12 @@ in Sexp_dispatch sexp sfalse sfalse sfalse sfalse sfalse;

%% -%% Get matched expression (e.g. case var1 var2 ... | ...) +%% Get matched expression (e.g. case (var1,var2,...) | ...) %% -%% Expression are separated by " " (space) so it is useful for -%% case expr1 expr2 ... | ... +%% Expression are separated by "," so it is useful for +%% case (expr1,expr2,...) | ... %% but also for -%% case ... | expr3 expr4 ... => ... +%% case ... | (expr3,expr4,...) => ... %% %% (This function is now doing nothing since there's only one %% variable at any time: one expression or a tuple of expressions) @@ -308,24 +310,20 @@ renamed-pat pat names = let (lambda sym ss -> if (Sexp_eq sym (Sexp_symbol "_:=_")) then if (List_nth i kinds false) then - %% %% if client use multiple name for the same erasable args, %% I expect it to not compile... - %% (Sexp_node sym ss) else (Sexp_node sym (cons (List_nth 0 ss Sexp_error) (cons (List_nth i names Sexp_error) nil))) else if tup then - %% %% tuples argument are all implicit so we must take special care of those - %% (Sexp_node (Sexp_symbol "_:=_") - (cons (tuple-nth i) (cons (List_nth i names Sexp_error) nil))) + (cons (tuple-nth i) (cons (List_nth i names Sexp_error) nil))) else (List_nth i names Sexp_error)) (lambda _ -> if tup then (Sexp_node (Sexp_symbol "_:=_") - (cons (tuple-nth i) (cons (List_nth i names Sexp_error) nil))) + (cons (tuple-nth i) (cons (List_nth i names Sexp_error) nil))) else (List_nth i names Sexp_error)) serr serr serr serr; @@ -340,7 +338,7 @@ in do { };

%% -%% Takes an Sexp as argument and IO_return `IO true` if it is a pattern +%% Takes an Sexp as argument and return `IO true` if it is a pattern %% (i.e. a constructor with or without argument) %% is-pat : Pat -> IO Bool; @@ -401,7 +399,7 @@ in Sexp_eq (ctor-of p0) (ctor-of p1); %% %% Get variable introduced by a constructor %% -%% Takes a pattern as argument and return each arguments +%% Takes a pattern as argument and returns each arguments %% of the constructor which is a variable (as opposed to a sub pattern) %% introduced-vars : Pat -> IO (List Var); @@ -422,7 +420,7 @@ introduced-vars pat = let %% Function to fold each argument of the pattern %% The Int is used internaly to keep track of argument index %% It is useful to know where is the variable in `ks` to get its kind - %% (kind is actualy only erasable or not here) + %% (kind is actualy only erasable or not) %% ff : IO (Pair Int (List Sexp)) -> Sexp -> IO (Pair Int (List Sexp)); ff p v = let @@ -473,16 +471,15 @@ in Sexp_dispatch pat

%% %% Wrap the third argument (`fun`) with a `let` definition for each variables -%% Names are taken from `rvars` and definition are taken from `ivars` %% wrap-vars : List Var -> List Var -> Code -> Code; -wrap-vars ivars rvars fun = List_fold2 (lambda fun v0 v1 -> +wrap-vars rhs lhs fun = List_fold2 (lambda fun v0 v1 -> %% %% I prefer `let` definition because a lambda function would need a type %% (quote ((lambda (uquote v0) -> (uquote fun)) (uquote v1)))) %% (quote (let (uquote v1) = (uquote v0) in (uquote fun)))) - fun ivars rvars; + fun rhs lhs;

%% %% Take a List of branches and return a List of the first pattern in each branches @@ -603,7 +600,7 @@ in do { };

%% -%% Type of one partition of branches (one branch with some possible child branches) +%% Type of one partition of branches (one branch with child branches) %% %% Pair of %% Triplet of renamed pat, @@ -729,8 +726,8 @@ in do { %% %% There's a need to merge branch because default branch may be anywhere %% -%% (I tried to consider default branches similar to everything but it failed in some way -%% So here we are...) +%% (I tried to consider default branches similar to every patterns +%% but it failed in some way. So here we are...) %% merge-dflt : List part-type -> Option part-type -> List part-type; merge-dflt parts odflt = let

===================================== btl/do.typer ===================================== @@ -131,7 +131,9 @@ do = macro (lambda args -> (IO_return (set-fun (get-decl args))) );

+%% %% Next are example command +%%

print str = (File_write (File_stdout ()) str);

===================================== btl/list.typer ===================================== @@ -45,11 +45,13 @@ length xs = case xs | 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 -> List a -> a`; %% - Disallow problem case : `(l : List a) -> (l != nil) -> a`; %% - Return an Option/Error +%% head1 : (a : Type) ≡> List a -> Option a; head1 xs = case xs | nil => none @@ -102,9 +104,9 @@ in helper f 0 xs; %% map2 : (a : Type) ≡> (b : Type) ≡> (c : Type) ≡> (a -> b -> c) -> List a -> List b -> List c; map2 = lambda f -> lambda xs -> lambda ys -> case xs - | nil => nil + | nil => nil % may be an error | cons x xs => case ys - | nil => nil % error + | nil => nil % may be an error | cons y ys => cons (f x y) (map2 f xs ys);

%% @@ -129,7 +131,7 @@ fold2 = lambda f -> lambda o -> lambda xs -> lambda ys -> case xs | nil => o; % may or may not be an error

%% -%% (Should be as any `fold right` of functional language) +%% (Should be as any `fold right` function of functional language) %% foldr : (a : Type) ≡> (b : Type) ≡> (b -> a -> a) -> List b -> a -> a; foldr = lambda f -> lambda xs -> lambda i -> case xs @@ -147,7 +149,7 @@ find = lambda f -> lambda xs -> case xs | cons x xs => case f x | true => some x | false => find f xs;

%% -%% Get the n'th element of a list or a default if the list is smaller +%% Get the n'th element of a list or a default if the list is smaller than n %% nth : (a : Type) ≡> Int -> List a -> a -> a; nth = lambda n -> lambda xs -> lambda d -> case xs @@ -183,7 +185,8 @@ foldl = lambda f -> lambda i -> lambda xs -> case xs

%% %% Takes a function and a list -%% Returns the list with element removed if the function return true on those element +%% Returns the list with element removed +%% when the user function return true on those element %% remove : (a : Type) ≡> (a -> Bool) -> List a -> List a; remove = lambda f -> lambda l -> case l @@ -243,7 +246,7 @@ empty? = lambda xs -> case xs %% Takes a comparison function and a list %% Returns the same list but sorted %% -%% If comparison is `>` then the list start with the smallest element +%% If comparison is `>` then the result start with the smallest element %% sort : (a : Type) ≡> (a -> a -> Bool) -> List a -> List a; sort = lambda o -> lambda l -> let @@ -278,7 +281,7 @@ in sortp (head1 l) nil nil (tail l); %% Find an element with a shortcut because the list is sorted %% Takes a comparison function, a function to match, an element and a list %% -%% (...maybe to parametric for what it does, this function is useless) +%% (...maybe too parametric for what it does, this function is useless) %% sfind : (a : Type) ≡> (a -> a -> Bool) -> (a -> Bool) -> a -> List a -> Option a; sfind = lambda o -> lambda f -> lambda a -> lambda l -> case l

===================================== btl/pervasive.typer ===================================== @@ -518,59 +518,117 @@ test3 = test4;

%%%% Rewrite of some builtins to use `Option`

+%% +%% If `Elab_nth-arg'` returns "_" it means: +%% A- The constructor isn't defined, or +%% B- The constructor has no n'th argument +%% +%% So in those case this function returns `none` +%% Elab_nth-arg a b c = let r = Elab_nth-arg' a b c; in case (String_eq r "_") | true => (none) | false => (some r);

+%% +%% If `Elab_arg-pos'` returns (-1) it means: +%% A- The constructor isn't defined, or +%% B- The constructor has no argument named like this +%% +%% So in those case this function returns `none` +%% Elab_arg-pos a b c = let r = Elab_arg-pos' a b c; in case (Int_eq r (-1)) | true => (none) | false => (some r);

-%%%% `<-` operator used in macro `do` and for tuple assignment - -define-operator "<-" 80 96; - %%%% %%%% Common library %%%%

-%% `List` is the type and `list` is the module (tuple) +%% +%% `<-` operator used in macro `do` and for tuple assignment +%% + +define-operator "<-" 80 96; + +%% +%% `List` is the type and `list` is the module +%% list = load "btl/list.typer";

-%% macro `do` for easier series of IO operation +%% +%% Macro `do` for easier series of IO operation +%% +%% e.g.: +%% do { IO_return true; }; +%% do = let lib = load "btl/do.typer" in lib.do;

-%% various macro for tuple -%% used by `case_` +%% +%% Module containing various macro for tuple +%% Used by `case_` +%% tuple-lib = load "btl/tuple.typer";

-%% get nth element +%% +%% Get the nth element of a tuple +%% +%% e.g.: +%% tuple-nth tup 0; +%% tuple-nth = tuple-lib.tuple-nth;

-%% affectation (e.g. `(x,y,z) <- tup`) +%% +%% Affectation of tuple +%% +%% e.g.: +%% (x,y,z) <- tup; +%% _<-_ = tuple-lib.assign-tuple;

-%% creation (e.g. `tup = (x,y,z)`) +%% +%% Instantiate a tuple from expressions +%% +%% e.g.: +%% tup = (x,y,z); +%% _,_ = tuple-lib.make-tuple;

Tuple = tuple-lib.tuple-type;

-%% macro `case` for a little more complex pattern matching +%% +%% Macro `case` for a some more complex pattern matching +%% case_ = let lib = load "btl/case.typer" in lib.case-macro;

-%%%% plain-let -%%%% Not recursive and not sequential +%% +%% plain-let +%% Not recursive and not sequential +%% +%% e.g.: +%% plain-let x = 1; in x; +%%

define-operator "plain-let" () 3; + +%% +%% Already defined: %% define-operator "in" 3 67; +%%

plain-let_in_ = let lib = load "btl/plain-let.typer" in lib.plain-let-macro;

-%%%% `case` at function level +%% +%% `case` at function level +%% +%% e.g.: +%% my-fun (x : Bool) +%% | true => false +%% | false => true; +%% _|_ = let lib = load "btl/polyfun.typer" in lib._|_;

%%%% Unit tests function for doing file @@ -582,7 +640,7 @@ _|_ = let lib = load "btl/polyfun.typer" in lib._|_; %% A macro using `load` for unit testing purpose %% %% Takes a file name (String) as argument -%% Return variable named `exec-test` from the loaded file +%% Returns variable named `exec-test` from the loaded file %% %% `exec-test` should be a command doing unit tests %% for other purpose than that just use `load` directly!

===================================== btl/plain-let.typer ===================================== @@ -13,18 +13,18 @@

%% %% The idea is to use unique identifier in a first let -%% and then assign those first identifier to the original symbol +%% and then assign those unique identifier to the original symbol %% %% Useful for auto-generated code (macro, ...) %%

%% -%% Takes the plain input of macro `plain-let` +%% Takes the plain argument of macro `plain-let` %% impl : List Sexp -> IO Sexp; impl args = let

- %% error use in Sexp_dispatch + %% Error use in Sexp_dispatch serr = lambda _ -> Sexp_error;

%% Takes an assignment statement and return a new @@ -37,7 +37,7 @@ impl args = let io-serr = lambda _ -> IO_return Sexp_error;

%% Get a `gensym` symbol - %% I can rename a function name (not the argument) + %% It can rename a function name (not the argument) %% or just a symbol rename : Sexp -> IO Sexp; rename sexp = Sexp_dispatch sexp @@ -101,7 +101,7 @@ impl args = let };

%% Takes a list of assignment and a body (likely using those assignment) - %% Returns a `let ... in ...` construction + %% Returns a `let [assignment] in [body]` construction let-in : Sexp -> Sexp -> Sexp; let-in decls body = Sexp_node (Sexp_symbol "let_in_") (cons decls (cons body nil));

@@ -112,7 +112,7 @@ impl args = let %% Takes lists of pairs (`gensym`,definition) and (`gensym`,original symbol) %% and the body (likely using original symbol) %% Returns - %% let [gensym] = [definition] ... in let [original symbol] = [gensym] in [body] + %% let [gensym] = [definition] in let [original symbol] = [gensym] in [body] gen-code : List (Pair Sexp Sexp) -> List (Pair Sexp Sexp) -> Sexp -> Sexp; gen-code sym-def var-sym body = let

===================================== btl/polyfun.typer ===================================== @@ -5,11 +5,12 @@ %%%% (Just a `case` at function definition level) %%%%

-%% error use in Sexp_dispatch +%% +%% Error use in Sexp_dispatch +%% serr : (a : Type) ≡> a -> Sexp; serr = lambda _ -> Sexp_error;

-%% other error for Sexp_dispatch xserr : (a : Type) ≡> a -> List Sexp; xserr = lambda _ -> (nil : List Sexp);

@@ -55,7 +56,7 @@ fun-args decl = Sexp_dispatch decl

%% %% Takes a list of "_=>_"-node -%% Returns a list of pair of (pattern, body) +%% Returns a list of (pattern, body) pair %% fun-cases : List Sexp -> List (Pair Sexp Sexp); fun-cases args = let @@ -76,7 +77,7 @@ fun-cases args = let in List_map mf args;

%% -%% Takes argument list and list of pair of (pattern, body) +%% Takes argument list and list of (pattern, body) pair %% Returns a function with a `case` on argument for each pattern %% cases-to-sexp : List Sexp -> List (Pair Sexp Sexp) -> Sexp;

===================================== btl/tuple.typer ===================================== @@ -33,9 +33,11 @@ %% List_map2 = list.map2; %% List_concat = list.concat;

+%% %% Move IO outside List (from element to List) %% (Was helpful for me when translating code that used to not be IO code) %% (The function's type explain everything) +%% io-list : List (IO ?a) -> IO (List ?a); io-list l = let ff : IO (List ?a) -> IO ?a -> IO (List ?a); @@ -166,7 +168,7 @@ wrap-vars ivars rvars fun = List_fold2 (lambda fun v0 v1 -> fun ivars rvars;

%% -%% Takes a list of values as Sexp (like 1, 1.0, "str", etc) +%% Takes a list of values (expressions) as Sexp (like a variable, 1, 1.0, "str", etc) %% Returns a tuple containing those values %% make-tuple-impl : List Sexp -> IO Sexp; @@ -216,6 +218,7 @@ make-tuple = macro (lambda args -> do { %% %% Takes element's type as argument %% +%% tuple-type = macro (lambda args -> let

mf : Sexp -> Sexp -> Sexp;

===================================== samples/batch_test.typer ===================================== @@ -35,6 +35,8 @@ u5 = Test_file "./samples/tuple_test.typer";

u6 = Test_file "./samples/do_test.typer";

+u7 = Test_file "./samples/plain_let_test.typer"; + exec-all = do { Test_info "BATCH TESTS" "\n\n\tfirst file\n"; b1 <- u1; @@ -46,11 +48,13 @@ exec-all = do { b4 <- u4; Test_info "BATCH TESTS" "\n\n\tnext file\n"; b5 <- u5; - Test_info "BATCH TESTS" "\n\n\tlast file\n"; + Test_info "BATCH TESTS" "\n\n\tnext file\n"; b6 <- u6; + Test_info "BATCH TESTS" "\n\n\tlast file\n"; + b7 <- u7; Test_info "BATCH TESTS" "\n\n\tdone\n";

- success <- IO_return (and b1 (and b2 (and b3 (and b4 (and b5 b6))))); + success <- IO_return (and b1 (and b2 (and b3 (and b4 (and b5 (and b6 b7))))));

if success then (Test_info "BATCH TESTS" "all tests succeeded")

===================================== samples/bbst.typer ===================================== @@ -8,6 +8,8 @@ %% %% The 2-3-4 tree %% +%% (Internal representation) +%%

type BbsTree (a : Type) | node2 (d : a) (l0 : BbsTree a) (l1 : BbsTree a) @@ -17,7 +19,7 @@ type BbsTree (a : Type) | node-leaf;

%% -%% The tree with necessary data +%% The data structure with necessary data %% %% c is a compare function which should be similar to <= (or >=) %% @@ -139,7 +141,7 @@ length tree = case tree %% Is the tree empty? %%

-is-empty tree = (Int_eq (length tree) 0); +empty? tree = (Int_eq (length tree) 0);

%% %% Check if two value are equal with comparison function only @@ -212,8 +214,8 @@ in case tree %% Is elem in the tree? %%

-member : (a : Type) ≡> a -> Bbst a -> Bool; -member elem tree = let +member? : (a : Type) ≡> a -> Bbst a -> Bool; +member? elem tree = let

oe = find elem tree;

@@ -375,7 +377,7 @@ insert elem tree = let

| node-leaf => node2 e node-leaf node-leaf;

-in if (member elem tree) then +in if (member? elem tree) then (case tree % we may want to replace an element (partial comparison function) | bbst s c t => bbst s c (helper c elem t)) else @@ -383,11 +385,11 @@ in if (member elem tree) then | bbst s c t => bbst (s + 1) c (helper c elem t));

%% -%% Remove the smallest element. Used in remove. +%% Internal function used in `remove` and `pop-leftmost` %%

-pop-leftmost : (a : Type) ≡> (a -> a -> Bool) -> BbsTree a -> BbsTree a; -pop-leftmost comp tree = let +pop-leftmost' : (a : Type) ≡> (a -> a -> Bool) -> BbsTree a -> BbsTree a; +pop-leftmost' comp tree = let

four2three : a -> a -> a -> BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a; @@ -423,11 +425,22 @@ pop-leftmost comp tree = let in (helper tree);

%% -%% Remove the biggest element. Used in remove. +%% Remove the smallest element +%% + +pop-leftmost : (a : Type) ≡> Bbst a -> Bbst a; +pop-leftmost t = case t + | bbst s c t => if (Int_eq 0 s) then + (bbst s c t) + else + (bbst (s - 1) c (pop-leftmost' c t)); + +%% +%% Internal used in `remove` and `pop-rightmost` %%

-pop-rightmost : (a : Type) ≡> (a -> a -> Bool) -> BbsTree a -> BbsTree a; -pop-rightmost comp tree = let +pop-rightmost' : (a : Type) ≡> (a -> a -> Bool) -> BbsTree a -> BbsTree a; +pop-rightmost' comp tree = let

four2three : a -> a -> a -> BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a; @@ -463,11 +476,22 @@ pop-rightmost comp tree = let in (helper tree);

%% -%% Get the smallest element. Used in remove. +%% Remove the greatest element +%% + +pop-rightmost : (a : Type) ≡> Bbst a -> Bbst a; +pop-rightmost t = case t + | bbst s c t => if (Int_eq 0 s) then + (bbst s c t) + else + (bbst (s - 1) c (pop-rightmost' c t)); + +%% +%% Internal used in `remove` and `get-leftmost` %%

-get-leftmost : (a : Type) ≡> (a -> a -> Bool) -> BbsTree a -> Option a; -get-leftmost comp tree = let +get-leftmost' : (a : Type) ≡> (a -> a -> Bool) -> BbsTree a -> Option a; +get-leftmost' comp tree = let

four2three : a -> a -> a -> BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a -> Option a; @@ -502,11 +526,19 @@ get-leftmost comp tree = let in (helper tree);

%% -%% Get the biggest element. Used in remove. +%% Get smallest element %%

-get-rightmost : (a : Type) ≡> (a -> a -> Bool) -> BbsTree a -> Option a; -get-rightmost comp tree = let +get-leftmost : (a : Type) ≡> Bbst a -> Option a; +get-leftmost t = case t + | bbst _ c t => get-leftmost' c t; + +%% +%% Internal used in `remove` and `get-rightmost` +%% + +get-rightmost' : (a : Type) ≡> (a -> a -> Bool) -> BbsTree a -> Option a; +get-rightmost' comp tree = let

four2three : a -> a -> a -> BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a -> Option a; @@ -540,6 +572,14 @@ get-rightmost comp tree = let

in (helper tree);

+%% +%% Get greatest element +%% + +get-rightmost : (a : Type) ≡> Bbst a -> Option a; +get-rightmost t = case t + | bbst _ c t => get-rightmost' c t; + %% %% Remove an element from the tree %% @@ -558,14 +598,14 @@ remove elem tree = let | node-leaf => ( case l1 | node-leaf => node-leaf | _ => let - oe = get-leftmost comp l1; + oe = get-leftmost' comp l1; in case oe - | some e => node2 e l0 (pop-leftmost comp l1) + | some e => node2 e l0 (pop-leftmost' comp l1) | none => node-leaf ) % I think this case may not happen | _ => let - oe = get-rightmost comp l0; + oe = get-rightmost' comp l0; in case oe - | some e => node2 e (pop-rightmost comp l0) l1 + | some e => node2 e (pop-rightmost' comp l0) l1 | none => node-leaf; % May not happen too

rebuild-left-three : (a -> a -> Bool) -> a -> @@ -575,14 +615,14 @@ remove elem tree = let | node-leaf => ( case l1 | node-leaf => node2 d1 node-leaf l2 | _ => let - oe = get-leftmost comp l1; + oe = get-leftmost' comp l1; in case oe - | some e => node3 e d1 l0 (pop-leftmost comp l1) l2 + | some e => node3 e d1 l0 (pop-leftmost' comp l1) l2 | none => node-leaf ) % I think this case may not happen | _ => let - oe = get-rightmost comp l0; + oe = get-rightmost' comp l0; in case oe - | some e => node3 e d1 (pop-rightmost comp l0) l1 l2 + | some e => node3 e d1 (pop-rightmost' comp l0) l1 l2 | none => node-leaf; % May not happen too

rebuild-right-three : (a -> a -> Bool) -> a -> @@ -592,14 +632,14 @@ remove elem tree = let | node-leaf => ( case l2 | node-leaf => node2 d0 l0 node-leaf | _ => let - oe = get-leftmost comp l2; + oe = get-leftmost' comp l2; in case oe - | some e => node3 d0 e l0 l1 (pop-leftmost comp l2) + | some e => node3 d0 e l0 l1 (pop-leftmost' comp l2) | none => node-leaf ) % I think this case may not happen | _ => let - oe = get-rightmost comp l1; + oe = get-rightmost' comp l1; in case oe - | some e => node3 d0 e l0 (pop-rightmost comp l1) l2 + | some e => node3 d0 e l0 (pop-rightmost' comp l1) l2 | none => node-leaf; % May not happen too

rebuild-left-four : (a -> a -> Bool) -> a -> a -> @@ -609,14 +649,14 @@ remove elem tree = let | node-leaf => ( case l1 | node-leaf => node3 d1 d2 node-leaf l2 l3 | _ => let - oe = get-leftmost comp l1; + oe = get-leftmost' comp l1; in case oe - | some e => node4 e d1 d2 l0 (pop-leftmost comp l1) l2 l3 + | some e => node4 e d1 d2 l0 (pop-leftmost' comp l1) l2 l3 | none => node-leaf ) % I think this case may not happen | _ => let - oe = get-rightmost comp l0; + oe = get-rightmost' comp l0; in case oe - | some e => node4 e d1 d2 (pop-rightmost comp l0) l1 l2 l3 + | some e => node4 e d1 d2 (pop-rightmost' comp l0) l1 l2 l3 | none => node-leaf; % May not happen too

rebuild-middle-four : (a -> a -> Bool) -> a -> a -> @@ -626,14 +666,14 @@ remove elem tree = let | node-leaf => ( case l2 | node-leaf => node3 d0 d2 l0 node-leaf l3 | _ => let - oe = get-leftmost comp l2; + oe = get-leftmost' comp l2; in case oe - | some e => node4 d0 e d2 l0 l1 (pop-leftmost comp l2) l3 + | some e => node4 d0 e d2 l0 l1 (pop-leftmost' comp l2) l3 | none => node-leaf ) % I think this case may not happen | _ => let - oe = get-rightmost comp l1; + oe = get-rightmost' comp l1; in case oe - | some e => node4 d0 e d2 l0 (pop-rightmost comp l1) l2 l3 + | some e => node4 d0 e d2 l0 (pop-rightmost' comp l1) l2 l3 | none => node-leaf; % May not happen too

rebuild-right-four : (a -> a -> Bool) -> a -> a -> @@ -643,14 +683,14 @@ remove elem tree = let | node-leaf => ( case l3 | node-leaf => node3 d0 d1 l0 l1 node-leaf | _ => let - oe = get-leftmost comp l3; + oe = get-leftmost' comp l3; in case oe - | some e => node4 d0 d1 e l0 l1 l2 (pop-leftmost comp l3) + | some e => node4 d0 d1 e l0 l1 l2 (pop-leftmost' comp l3) | none => node-leaf ) % I think this case may not happen | _ => let - oe = get-rightmost comp l2; + oe = get-rightmost' comp l2; in case oe - | some e => node4 d0 d1 e l0 l1 (pop-rightmost comp l2) l3 + | some e => node4 d0 d1 e l0 l1 (pop-rightmost' comp l2) l3 | none => node-leaf; % May not happen too

helper : (a -> a -> Bool) -> a -> BbsTree a -> BbsTree a; @@ -705,7 +745,7 @@ remove elem tree = let

| node-leaf => node-leaf;

-in if (member elem tree) then +in if (member? elem tree) then (case tree | bbst s c t => bbst (s - 1) c (helper c elem t)) else @@ -745,9 +785,9 @@ odict-insert : (Key : Type) ≡> (Data : Type) ≡> Key -> Data -> Bbst (Pair Key (Option Data)) -> Bbst (Pair Key (Option Data)); odict-insert k d t = insert (pair k (some d)) t;

-odict-member : (Key : Type) ≡> (Data : Type) ≡> Key -> +odict-member? : (Key : Type) ≡> (Data : Type) ≡> Key -> Bbst (Pair Key (Option Data)) -> Bool; -odict-member k t = member (pair k none) t; +odict-member? k t = member? (pair k none) t;

odict-remove : (Key : Type) ≡> (Data : Type) ≡> Key -> Bbst (Pair Key (Option Data)) -> Bbst (Pair Key (Option Data)); @@ -757,8 +797,8 @@ odict-update : (Key : Type) ≡> (Data : Type) ≡> Key -> Data -> Bbst (Pair Key (Option Data)) -> Bbst (Pair Key (Option Data)); odict-update k d t = insert (pair k (some d)) t;

-odict-is-empty : (Key : Type) ≡> (Data : Type) ≡> Bbst (Pair Key (Option Data)) -> Bool; -odict-is-empty t = is-empty t; +odict-empty? : (Key : Type) ≡> (Data : Type) ≡> Bbst (Pair Key (Option Data)) -> Bool; +odict-empty? t = empty? t;

%%% %%% Test helper

===================================== samples/bbst_test.typer ===================================== @@ -41,7 +41,7 @@ test-length = do { r3 <- Test_eq "t3" (length t3) 53; r4 <- Test_eq "t4" (length t4) 50; r5 <- Test_eq "t5" (length t5) 50; - r6 <- Test_true "e0" (is-empty e0); + r6 <- Test_true "e0" (empty? e0); r7 <- Test_eq "e1" (length e1) 1; r8 <- Test_eq "e2" (length e2) 0;

@@ -70,7 +70,7 @@ test-find = do { (Test_warning "BBST" "find test failed"); };

-%% member is just a wrapped version of find so not need to test it +%% member? is just a wrapped version of find so not need to test it %% in the actual implementation

test-fold = do {

===================================== samples/myers.typer ===================================== @@ -1,52 +1,77 @@ %%% %%% Adaptation of Myers list from ocaml file `myers.ml` %%% -%%% since 2018-05-14 -%%%

+%% %% We could replace mnil and mcons by nil and cons %% when load and list.typer are ready +%% t : Type -> Type; type t (a : Type) | mnil | mcons (data : a) (link1 : (t a)) (i : Int) (link2 : (t a));

-% Contrary to Myers's presentation, we index from the top of the stack, -% and we don't store the total length but the "skip distance" instead. -% This makes `cons' slightly faster, and better matches our use for -% debruijn environments. +%% +%% Contrary to Myers's presentation, we index from the top of the stack, +%% and we don't store the total length but the "skip distance" instead. +%% This makes `cons' slightly faster, and better matches our use for +%% debruijn environments. +%%

+%% +%% Prepend an element `x` to a Myers list `l` +%% cons : (a : Type) ≡> a -> t a -> t a; cons x l = case l | mcons _ _ s1 l1 => ( case l1 | mcons _ _ s2 l2 => ( case (Int_>= s1 s2) | true => mcons x l (s1 + s2 + 1) l2 - | false => mcons x l 1 l - ) - | _ => mcons x l 1 l - ) + | false => mcons x l 1 l ) + | _ => mcons x l 1 l ) | _ => mcons x l 1 l;

+%% +%% Get the head of a Myers list `l` +%% (Get the first element) +%% Returns `some x` if the list is non-empty or `none` if it is empty +%% car : (a : Type) ≡> t a -> Option a; car l = case l | mnil => none | mcons x _ _ _ => some x;

+%% +%% Get the tail of a Myers list `l` +%% (Get the same list without its first element) +%% Always returns `mnil` if the list is empty +%% cdr : (a : Type) ≡> t a -> t a; cdr l = case l | mnil => mnil | mcons _ l _ _ => l;

+%% +%% Pass the first element to a user function and return the result +%% or return a default value passed as argument +%% match : (a : Type) ≡> (b : Type) ≡> t a -> b -> (a -> t a -> b) -> b; match l n c = case l | mnil => n | mcons x l _ _ => c x l;

-empty : (a : Type) ≡> t a -> Bool; -empty l = case l +%% +%% Is the Myers list empty? +%% +empty? : (a : Type) ≡> t a -> Bool; +empty? l = case l | mnil => true | _ => false;

+%% +%% Remove the n'th first element from the Myers list +%% (It is the same as `(cdr (cdr ...))` with `cdr` called `n` times +%% but may be faster for greater `n`) +%% nthcdr : (a : Type) ≡> Int -> t a -> t a; nthcdr n l = if_then_else_ (Int_eq n 0) l ( case l @@ -57,13 +82,21 @@ nthcdr n l = if_then_else_ (Int_eq n 0) l ) );

+%% +%% Get the n'th element of a Myers list +%% nth : (a : Type) ≡> Int -> t a -> Option a; nth n l = car (nthcdr n l);

-% While `nth` is O(log N), `set_nth` is O(N)! :-( - -set_nth : (a : Type) ≡> Int -> a -> t a -> t a; -set_nth n v l = let +%% +%% Update the n'th element of a Myers list +%% Takes the index, the new value and the list +%% Returns the updated list +%% +%% (While `nth` is O(log N), `set-nth` is O(N)! :-( ) +%% +set-nth : (a : Type) ≡> Int -> a -> t a -> t a; +set-nth n v l = let

% I should use the new case_ macro here!

@@ -80,19 +113,24 @@ set_nth n v l = let

| pat1 n vp cdr s tail => if_then_else_ (Int_eq n 0) ( mcons v cdr s tail ) - ( cons vp (set_nth (n - 1) v cdr) ) + ( cons vp (set-nth (n - 1) v cdr) )

- % We can't set_nth past the end in general because we'd need to - % magically fill the intermediate entries with something of the right type. - % But we *can* set_nth just past the end. + %% + %% We can't set-nth past the end in general because we'd need to + %% magically fill the intermediate entries with something of the right type. + %% But we *can* set-nth just past the end. + %%

| pat2 n => if_then_else_ (Int_eq n 0) ( mcons v mnil 1 mnil ) ( l ); % should throw an error here!

-% This operation would be more efficient using Myers's choice of keeping -% the length (instead of the skip-distance) in each node. - +%% +%% Get the element count of a Myers list +%% +%% (This operation would be more efficient using Myers's choice of keeping +%% the length (instead of the skip-distance) in each node.) +%% length : (a : Type) ≡> t a -> Int; length l = let

@@ -103,10 +141,11 @@ length l = let

in lengthp l 0;

-% Find the first element for which the predicate `p' is true. -% "Binary" search, assuming the list is "sorted" (i.e. all elements after -% this one also return true). - +%% +%% Find the first element for which the predicate `p' is true. +%% "Binary" search, assuming the list is "sorted" (i.e. all elements after +%% this one also return true). +%% find : (a : Type) ≡> (a -> Bool) -> t a -> Option a; find p l = let

@@ -129,10 +168,11 @@ find p l = let

in find1 l;

-% Find the last node for which the predicate `p' is false. -% "Binary" search, assuming the list is "sorted" (i.e. all elements after -% this one also return true). - +%% +%% Find the last node for which the predicate `p' is false. +%% "Binary" search, assuming the list is "sorted" (i.e. all elements after +%% this one also return true). +%% findcdr : (a : Type) ≡> (a -> Bool) -> t a -> t a; findcdr p l = let

@@ -160,28 +200,43 @@ findcdr p l = let

in findcdr1 none l;

-fold_left : (a : Type) ≡> (b : Type) ≡> (b -> a -> b) -> b -> t a -> b; -fold_left f i l = case l +%% +%% As `fold_left` of any functional language but on Myers list +%% +foldl : (a : Type) ≡> (b : Type) ≡> (b -> a -> b) -> b -> t a -> b; +foldl f i l = case l | mnil => i - | mcons x l _ _ => fold_left f (f i x) l; + | mcons x l _ _ => foldl f (f i x) l;

-fold_right : (a : Type) ≡> (b : Type) ≡> (a -> b -> b) -> t a -> b -> b; -fold_right f l i = case l +%% +%% As 'fold_right` of any functional language but on Myers list +%% +foldr : (a : Type) ≡> (b : Type) ≡> (a -> b -> b) -> t a -> b -> b; +foldr f l i = case l | mnil => i - | mcons x l _ _ => f x (fold_right f l i); + | mcons x l _ _ => f x (foldr f l i);

+%% +%% As `map` of any functional language but on Myers list +%% (Apply a function to all element of the list) +%% map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> t a -> t b; map f l = let

fp : a -> t b -> t b; fp x lp = cons (f x) lp;

-in fold_right fp l mnil; +in foldr fp l mnil;

+%% +%% Apply all element of a Myers list to a user function +%% Takes a function and a list +%% Returns the length of the list +%% iteri : (a : Type) ≡> (Int -> a -> Unit) -> t a -> Int; iteri f l = let

fp : (Int -> a -> Int); fp i x = let _ = (f i x); in i + 1;

-in fold_left fp 0 l; +in foldl fp 0 l;

===================================== samples/myers_test.typer ===================================== @@ -0,0 +1,42 @@ +%%%% +%%%% Unit tests for Myers list +%%%% + +xs = cons 1 (cons 2 (cons 3 (cons 4 mnil))); + +ys = cons 2 (cons 3 (cons 4 mnil)); + +zs = cons 4 mnil; + +ws = set-nth 1 7 ys; + +test = do { + Test_info "MYERS LIST" ""; + + r0 <- Test_eq "cdr" zs (cdr (cdr ys)); + r1 <- Test_eq "nthcdr" zs (nthcdr 2 ys); + + r2 <- Test_true "empty?" (empty? mnil); + r3 <- Test_false "empty?" (empty? zs); + + r4 <- Test_eq "car" (car xs) (some 1); + r5 <- Test_eq "car" (car zs) (some 4); + r6 <- Test_eq "car" (car mnil) none; + + r7 <- Test_eq "nth" (nth 0 zs) (some 4); + r8 <- Test_eq "nth" (nth 1 ys) (some 3); + + r9 <- Test_neq "set-nth" (nth 1 ys) (nth 1 ws); + r10 <- Test_eq "set-nth" (nth 1 ws) (some 7); + + success <- IO_return (and r0 (and r1 (and r2 (and r3 (and r4 + (and r5 (and r6 (and r7 (and r8 (and r9 r10)))))))))); + + if success then + (Test_info "MYERS LIST" "test on Myers list succeeded") + else + (Test_warning "MYERS LIST" "test on Myers list failed"); + + %% IO_return success; +}; +

===================================== samples/plain_let_test.typer ===================================== @@ -0,0 +1,37 @@ +%%%% +%%%% Unit tests for `plain-let` +%%%% + +f : Int; +f = 3; + +g : Int; +g = 5; + +fun = plain-let + f x = f + x; + g = g; + a = 10; +in lambda x -> (f x) + g; + +test = do { + Test_info "PLAIN-LET" ""; + + r0 <- Test_eq "fun 0" (fun 0) 8; + r1 <- Test_eq "fun 7" (fun 7) 15; + + success <- IO_return (and r0 r1); + + if success then + (Test_info "PLAIN-LET" "test on plain-let succeeded") + else + (Test_warning "PLAIN-LET" "test on plain-let failed"); + + IO_return success; +}; + +exec-test = do { + b1 <- test; + + IO_return b1; +};

===================================== samples/table.typer ===================================== @@ -59,7 +59,7 @@ length t = case t %% Is the tree empty? %%

-is-empty t = Int_eq (length t) 0; +empty? t = Int_eq (length t) 0;

%% %% Find an element in the tree and return it @@ -94,8 +94,8 @@ in case tree %% Is this element in the tree? %%

-member : (a : Type) ≡> a -> Table a -> Bool; -member elem tree = case (find elem tree) +member? : (a : Type) ≡> a -> Table a -> Bool; +member? elem tree = case (find elem tree) | some _ => true | none => false;

@@ -128,7 +128,7 @@ insert elem tree = let (table-node table-nil (table-leaf (Int_lsr h1 1) es)))) | table-nil => table-leaf h (cons e nil);

-in if (member elem tree) then +in if (member? elem tree) then (case tree % we may want to replace a variable (partial comparison function) | table s c h t => table s c h (helper elem c (h elem) t)) else @@ -142,16 +142,16 @@ in if (member elem tree) then remove : (a : Type) ≡> a -> Table a -> Table a; remove elem tree = let

- is-empty : TableTree a -> Bool; - is-empty t = case t - | table-node l r => if (is-empty l) then - (is-empty r) else + empty? : TableTree a -> Bool; + empty? t = case t + | table-node l r => if (empty? l) then + (empty? r) else (false) | table-leaf _ es => Int_eq 0 (List_length es) | table-nil => true;

pop-empty : TableTree a -> TableTree a; - pop-empty t = if (is-empty t) then + pop-empty t = if (empty? t) then (table-nil) else (t);

@@ -174,7 +174,7 @@ remove elem tree = let (table-leaf h1 es) % element not found | table-nil => table-nil; % element not found

-in if (member elem tree) then +in if (member? elem tree) then (case tree | table s c h t => table (s - 1) c h (helper elem c (h elem) t)) else @@ -230,9 +230,9 @@ udict-insert : (Key : Type) ≡> (Data : Type) ≡> Key -> Data -> Table (Pair Key (Option Data)) -> Table (Pair Key (Option Data)); udict-insert k d t = insert (pair k (some d)) t;

-udict-member : (Key : Type) ≡> (Data : Type) ≡> Key -> +udict-member? : (Key : Type) ≡> (Data : Type) ≡> Key -> Table (Pair Key (Option Data)) -> Bool; -udict-member k t = member (pair k none) t; +udict-member? k t = member? (pair k none) t;

udict-remove : (Key : Type) ≡> (Data : Type) ≡> Key -> Table (Pair Key (Option Data)) -> Table (Pair Key (Option Data)); @@ -242,8 +242,8 @@ udict-update : (Key : Type) ≡> (Data : Type) ≡> Key -> Data -> Table (Pair Key (Option Data)) -> Table (Pair Key (Option Data)); udict-update k d t = update (pair k (some d)) t;

-udict-is-empty : (Key : Type) ≡> (Data : Type) ≡> Table (Pair Key (Option Data)) -> Bool; -udict-is-empty t = is-empty t; +udict-empty? : (Key : Type) ≡> (Data : Type) ≡> Table (Pair Key (Option Data)) -> Bool; +udict-empty? t = empty? t;

%%% %%% Test helper

===================================== samples/table_test.typer ===================================== @@ -41,8 +41,8 @@ test-length = do { r3 <- Test_eq "t3" (length t3) 53; r4 <- Test_eq "t4" (length t4) 50; r5 <- Test_eq "t5" (length t5) 50; - %% r6 <- Test_eq "e0" (is-empty e0) true; - r6 <- Test_true "e0" (is-empty e0); + %% r6 <- Test_eq "e0" (empty? e0) true; + r6 <- Test_true "e0" (empty? e0); r7 <- Test_eq "e1" (length e1) 1; r8 <- Test_eq "e2" (length e2) 0;

@@ -71,7 +71,7 @@ test-find = do { (Test_warning "TABLE" "find test failed"); };

-%% member is just a wrapped version of find so not need to test it +%% member? is just a wrapped version of find so not need to test it %% in the actual implementation

u = (IO_run test-length) ();

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