Skip to content
Commits on Source (3)
Hide whitespace changes
Inline Side-by-side
btl/builtins.typer
View file @ 6ef13572
......@@ -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
View file @ 6ef13572
......@@ -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
View file @ 6ef13572
......@@ -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
View file @ 6ef13572
......@@ -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
View file @ 6ef13572
......@@ -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
View file @ 6ef13572
......@@ -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
View file @ 6ef13572
......@@ -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
View file @ 6ef13572
......@@ -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
View file @ 6ef13572
......@@ -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
View file @ 6ef13572
......@@ -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
View file @ 6ef13572
......@@ -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
View file @ 6ef13572
%%%
%%% 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 → 100644
View file @ 6ef13572
%%%%
%%%% 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 → 100644
View file @ 6ef13572
%%%%
%%%% 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
View file @ 6ef13572
......@@ -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
View file @ 6ef13572
......@@ -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) ();
......