Skip to content
Commits on Source (115)
15 additional commits have been omitted to prevent performance issues.
Expand all Hide whitespace changes
Inline Side-by-side
.gitignore
View file @ 2269559a
ChangeLog
typer
# Files generated by OCaml's compiler
*.byte
*.elc
*.annot
*.cmi
*.cmo
.depend
# Files generated by LaTeX and Texinfo
*.toc
*.pdf
*.log
*.aux
manual.??
*.info
*_build/
# Random backup/autosave files
*~
\#*\#
test.ml
_temp_hack
test__.typer
# Files generated by merges and such. Don't include `*.rej` here since
# we want them to be "in your face" so you don't forget to merge them.
*.orig
_tags
# Aux files used by Merlin
.merlin
# FIXME: What is this `_tags` for?
_tags
# FIXME: What is this `.directory` for?
.directory
# Files generated by profilers
gmon.out
ocamlprof.dump
# Files auto-generated for ELPA packaging and other Emacs stuff
emacs/*-autoloads.el
emacs/*-pkg.el
emacs/*.elc
GNUmakefile
View file @ 2269559a
......@@ -8,7 +8,7 @@ SRC_FILES := $(wildcard ./src/*.ml)
CPL_FILES := $(wildcard ./$(BUILDDIR)/src/*.cmo)
TEST_FILES := $(wildcard ./tests/*_test.ml)
OBFLAGS = -tag debug -tag profile -lib nums -build-dir $(BUILDDIR)
OBFLAGS = -tag debug -tag profile -lib str -build-dir $(BUILDDIR) -pkg num
# OBFLAGS := -I $(SRCDIR) -build-dir $(BUILDDIR) -pkg str
# OBFLAGS_DEBUG := -tag debug -tag profile -tag "warn(+20)"
# OBFLAGS_RELEASE := -tag unsafe -tag inline
......
btl/builtins.typer
View file @ 2269559a
......@@ -99,13 +99,30 @@ _-_ = Built-in "Int.-" : Int -> Int -> Int;
_*_ = Built-in "Int.*" : Int -> Int -> Int;
_/_ = Built-in "Int./" : Int -> Int -> Int;
%% modulo
Int_mod = Built-in "Int.mod" : Int -> Int -> Int;
%% Operators on bits
Int_and = Built-in "Int.and" : Int -> Int -> Int;
Int_or = Built-in "Int.or" : Int -> Int -> Int;
Int_xor = Built-in "Int.xor" : Int -> Int -> Int;
Int_lsl = Built-in "Int.lsl" : Int -> Int -> Int;
Int_lsr = Built-in "Int.lsr" : Int -> Int -> Int;
Int_asr = Built-in "Int.asr" : Int -> Int -> Int;
Int_< = Built-in "Int.<" : Int -> Int -> Bool;
Int_> = Built-in "Int.>" : Int -> Int -> Bool;
Int_eq = Built-in "Int.=" : Int -> Int -> Bool;
Int_<= = Built-in "Int.<=" : Int -> Int -> Bool;
Int_>= = Built-in "Int.>=" : Int -> Int -> Bool;
%% bitwise negation
Int_not = Built-in "Int.not" : Int -> Int;
Int->Integer = Built-in "Int->Integer" : Int -> Integer;
Int->String = Built-in "Int->String" : Int -> String;
Integer_+ = Built-in "Integer.+" : Integer -> Integer -> Integer;
Integer_- = Built-in "Integer.-" : Integer -> Integer -> Integer;
Integer_* = Built-in "Integer.*" : Integer -> Integer -> Integer;
......@@ -117,15 +134,36 @@ Integer_eq = Built-in "Integer.=" : Integer -> Integer -> Bool;
Integer_<= = Built-in "Integer.<=" : Integer -> Integer -> Bool;
Integer_>= = Built-in "Integer.>=" : Integer -> Integer -> Bool;
Integer->String = Built-in "Integer->String" : Integer -> String;
Float_+ = Built-in "Float.+" : Float -> Float -> Float;
Float_- = Built-in "Float.-" : Float -> Float -> Float;
Float_* = Built-in "Float.*" : Float -> Float -> Float;
Float_/ = Built-in "Float./" : Float -> Float -> Float;
Float->String = Built-in "Float->String" : Float -> String;
Float_< = Built-in "Float.<" : Float -> Float -> Bool;
Float_> = Built-in "Float.>" : Float -> Float -> Bool;
Float_eq = Built-in "Float.=" : Float -> Float -> Bool;
Float_<= = Built-in "Float.<=" : Float -> Float -> Bool;
Float_>= = Built-in "Float.>=" : Float -> Float -> Bool;
Float_trunc = Built-in "Float.trunc" : Float -> Float;
String_eq = Built-in "String.=" : String -> String -> Bool;
String_concat = Built-in "String.concat" : String -> String -> String;
String_sub = Built-in "String.sub" : String -> Int -> Int -> String;
Sexp_eq = Built-in "Sexp.=" : Sexp -> Sexp -> Bool;
%%
%% Takes an Sexp
%% Returns the same Sexp in the IO monad
%% but also print the Sexp to standard output
%%
Sexp_debug_print = Built-in "Sexp.debug_print" : Sexp -> IO Sexp;
%% -----------------------------------------------------
%% List
%% -----------------------------------------------------
......@@ -141,7 +179,7 @@ cons = datacons List cons;
%%%% Macro-related definitions
%% Sexp_block= Built-in "Sexp.block" : List Pretoken -> Sexp;
Sexp_block = Built-in "Sexp.block" : String -> 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;
......@@ -164,9 +202,75 @@ Sexp_dispatch = Built-in "Sexp.dispatch"
-> (string : String -> a)
-> (int : Integer -> a)
-> (float : Float -> a)
-> (block : List Sexp -> a)
-> (block : Sexp -> a)
-> a ;
%%
%% Parse an Sexp with the default context
%% default context include builtins.typer and pervasive.typer
%% but nothing else
%%
%% It was implemented to parse Sexp block in a macro
%%
Parser_default = Built-in "Parser.default" : Sexp -> List Sexp;
%%
%% Same as `Parser_default` but with a custom context
%%
Parser_custom = Built-in "Parser.custom" : Elab_Context -> Sexp -> List Sexp;
%%
%% Parse an Sexp with the latest context
%%
%% (Previous top level definition should be in the context)
%%
Parser_newest = Built-in "Parser.newest" : Sexp -> List Sexp;
%%%% Array (without IO, but they could be added easily)
%%
%% Takes an index, a new value and an array
%% Returns a copy of the array with the element
%% at the specified index set to the new value
%%
%% 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;
%%
%% Takes an element and an array
%% Returns a copy of the array with the new element at the end
%%
%% Array_append is in O(N) where N is the length
%%
Array_append = Built-in "Array.append" : (a : Type) ≡> a -> Array a -> Array a;
%%
%% Takes an Int (n) and a value
%% Returns an array containing n times the value
%%
Array_create = Built-in "Array.create" : (a : Type) ≡> Int -> a -> Array a;
%%
%% Takes an array
%% Returns the number of element in the array
%%
Array_length = Built-in "Array.length" : (a : Type) ≡> Array a -> Int;
%%
%% Takes a default value, an index and an array
%% Returns the value in the array at the specified index or
%% the default value if the index is out of bounds
%%
Array_get = Built-in "Array.get" : (a : Type) ≡> a -> Int -> Array a -> a;
%%
%% 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
%% Builtin bind
......@@ -196,4 +300,156 @@ 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)
%%
%% Conceptualy:
%% Ref : Type -> Type;
%% Ref = typecons (Ref (a : Type)) (Ref a);
%%
%%
%% Takes a value
%% Returns a value modifiable in the IO monad
%% and which already contain the specified value
%%
Ref_make = Built-in "Ref.make" : (a : Type) ≡> a -> IO (Ref a);
%%
%% Takes a Ref
%% Returns in the IO monad the value in the Ref
%%
Ref_read = Built-in "Ref.read" : (a : Type) ≡> Ref a -> IO a;
%%
%% Takes a value and a Ref
%% Returns the an empty command
%% and set the Ref to contain specified value
%%
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% ...".
%% Assume the three dots to be anything.
%%
gensym = Built-in "gensym" : Unit -> IO Sexp;
%%%% Function on Elab_Context
%%
%% Get the current context of elaboration
%%
Elab_getenv = Built-in "Elab.getenv" : Unit -> IO Elab_Context;
%%
%% Check if a symbol is defined in a particular context
%%
Elab_isbound = Built-in "Elab.isbound" : String -> Elab_Context -> Bool;
%%
%% Check if a symbol is a constructor in a particular context
%%
Elab_isconstructor = Built-in "Elab.isconstructor"
: String -> Elab_Context -> Bool;
%%
%% Check if the n'th field of a constructor is erasable
%% If the constructor isn't defined it will always return false
%%
Elab_is-nth-erasable = Built-in "Elab.is-nth-erasable" : String -> Int -> Elab_Context -> Bool;
%%
%% Check if a field of a constructor is erasable
%% If the constructor or the field aren't defined it will always return false
%%
Elab_is-arg-erasable = Built-in "Elab.is-arg-erasable" : String -> String -> Elab_Context -> Bool;
%%
%% Get n'th field of a constructor
%% It return "_" in case the field isn't defined
%% see pervasive.typer for a more convenient function
%%
Elab_nth-arg' = Built-in "Elab.nth-arg" : String -> Int -> Elab_Context -> String;
%%
%% Get the position of a field in a constructor
%% 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;
%%
%% Get the docstring associated with a symbol
%%
Elab_debug-doc = Built-in "Elab.debug-doc" : String -> Elab_Context -> String;
%%%% Unit test helper IO
%%
%% Print message and/or fail (terminate)
%% And location is printed before the error
%%
%%
%% Voluntarily fail
%% use case: next unit tests are not worth testing
%%
%% Takes a "section" and a "message" as argument
%%
Test_fatal = Built-in "Test.fatal" : String -> String -> IO Unit;
%%
%% Throw a warning, very similar to `Test_info`
%% but it's possible to implement a parameter for user who want it to sometimes be fatal
%%
%% Takes a "section" and a "message" as argument
%%
Test_warning = Built-in "Test.warning" : String -> String -> IO Unit;
%%
%% Just print a message with location of the call
%%
%% Takes a "section" and a "message" as argument
%%
Test_info = Built-in "Test.info" : String -> String -> IO Unit;
%%
%% Get a string representing location of call ("file:line:column")
%%
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
%%%
%%
%% 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 0 → 100644
View file @ 2269559a
This diff is collapsed.
btl/do.typer 0 → 100644
View file @ 2269559a
%%% do.typer --- Monadic do notation
%% Here's an example :
%%
%% fun = do {
%% str <- return "\n\tHello world!\n\n";
%% print str;
%% };
%%
%% `str` is bind by macro,
%%
%% `fun` is a command,
%%
%% `do` may contain `do` because it returns a command.
%%
%% Operator of assignment in `do` block
%%
%% FIXME: "assign" is a poor choice, because it doesn't perform any
%% assignment, it only "binds" a new variable.
assign = Sexp_symbol "_<-_";
%%
%% Takes one of `;`-separated command in `do` block
%% Returns the left-hand side symbol or a default symbol
%%
%% lhs <- rhs;
%%
get-sym : Sexp -> Sexp;
get-sym sexp = let
dflt-sym = (lambda _ -> (Sexp_symbol " %not used% "));
in Sexp_dispatch sexp
(lambda s ss -> if (Sexp_eq s assign) then
(List_nth 0 ss Sexp_error)
else
(dflt-sym ()))
dflt-sym dflt-sym dflt-sym
dflt-sym dflt-sym; % there must be a command
%%
%% Takes one of `;`-separated command in `do` block
%% Returns the right-hand side command
%%
%% lhs <- rhs;
%%
%% or
%%
%% rhs;
%%
get-op : Sexp -> Sexp;
get-op sexp = let
as-is = lambda _ -> sexp;
helper = (lambda sexp -> Sexp_dispatch sexp
( lambda s ss -> if (Sexp_eq s assign) then
(Sexp_node (List_nth 1 ss Sexp_error) (List_tail (List_tail ss)))
else
(Sexp_node s ss)
)
as-is as-is as-is as-is as-is
);
op = (helper sexp);
in if (Sexp_eq op (Sexp_symbol "")) then Sexp_error else op;
%%
%% Takes a block (`{...}`)
%% Parse the block and returns the list of command inside the block
%%
get-decl : List Sexp -> List Sexp;
get-decl args = let
err = lambda _ -> cons Sexp_error nil;
%% Expecting a Block of command separated by ";"
node = Sexp_dispatch (List_nth 0 args Sexp_error)
(lambda _ _ -> cons Sexp_error nil) err err err err
%% `Parser_newest` use the most recent environment
(lambda l -> Parser_newest l);
in node;
%%
%% The idea of the macro is :
%%
%% IO_bind a-op (lambda a-sym -> [next command or return a-sym])
%% IO_bind a-op (lambda a-sym -> (IO_bind b-op (lambda b-sym -> [next command or return b-sym])))
%%
%% this way a-sym is defined within b-op and so on
%% a-sym is now just `a` and not `IO a`
%%
%% (It could be possible to use `IO Ref` rather than a new variable
%% for each command with same lhs symbol, but will it be useful?)
%%
%%
%% Takes the list of command inside `do` block
%% This is the `main` of macro `do`
%%
set-fun : List Sexp -> Sexp;
set-fun args = let
helper : Sexp -> List Sexp -> Sexp;
helper lsym args = case args
| cons s ss => (let
sym = get-sym s;
op = get-op s;
in Sexp_node (Sexp_symbol "IO_bind") (cons (op)
(cons (Sexp_node (Sexp_symbol "lambda_->_") (cons sym (cons (helper sym ss) nil))) nil))
)
| nil => Sexp_node (Sexp_symbol "IO_return") (cons lsym nil);
in helper (Sexp_symbol "") args; % return Unit if no command given
%%
%% Macro `do`
%% Serie of command
%%
do = macro (lambda args ->
(IO_return (set-fun (get-decl args)))
);
%%
%% Next are example command
%%
print str = (File_write (File_stdout ()) str);
return v = IO_return v;
newline = print "\n";
tab = print "\t";
float2string v = IO_return (Float->String v);
%%
%% example0 = do {
%% str <- return "\n\tHello world!";
%% print str;
%% return 0.0;
%% };
%%
%% example1 = do {
%% flt <- example0;
%% str <- float2string flt;
%% newline;
%% tab;
%% print str;
%% newline;
%% newline;
%% };
%%
btl/list.typer 0 → 100644
View file @ 2269559a
%%% list.typer --- Singly linked lists manipulation
%% I kept it simple:
%% not using macro `lambda`
%% not usgin macro `case`
%% in case we want to change order of definition in pervasive.typer
%%%% List type
%% List's type is currently in pervasive.typer
%%
%% FIXME: "List : ?" should be sufficient but triggers
%% macro `type` isn't actually defined where this file is included
%% in pervasive.typer
%%
%% List : Type -> Type;
%% type List (a : Type)
%% | nil
%% | cons (hd : a) (tl : List a);
%%%% List functions
%% Get the length of a list in O(N) times where N is the length
%%
%% Alternative (tail recursive):
%%
%% length xs = let
%% helper : (a : Type) ≡> Int -> List a -> Int;
%% helper len xs = case xs
%% | nil => len
%% | cons hd tl => helper (len + 1) tl;
%% in helper 0 xs;
%%
%%
length : (a : Type) ≡> List a -> Int;
length 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 -> 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
| cons hd tl => some hd;
%%
%% Takes a list
%% Returns `some x` where x is the first element of the list
%% or none if the list is empty
%%
head : (a : Type) ≡> List a -> Option a;
head xs = case xs
| cons x _ => some x
| nil => none;
%%
%% Takes a list
%% Returns the same list without it's first element
%% The tail of `nil` is still `nil`
%%
tail : (a : Type) ≡> List a -> List a;
tail xs = case xs
| nil => nil
| cons hd tl => tl;
%%
%% Apply a function to all element of a list
%%
%% (Should be as `map` of every functional language)
%%
map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> List a -> List b;
map f = lambda xs -> case xs
| nil => nil
| cons x xs => cons (f x) (map f xs);
%%
%% As `map` but user's function also takes element index as last argument
%%
mapi : (a : Type) ≡> (b : Type) ≡> (a -> Int -> b) -> List a -> List b;
mapi = lambda f -> lambda xs -> let
helper : (a -> Int -> b) -> Int -> List a -> List b;
helper = lambda f -> lambda i -> lambda xs -> case xs
| nil => nil
| cons x xs => cons (f x i) (helper f (i + 1) xs);
in helper f 0 xs;
%%
%% As `map` but with 2 list at the same time
%% If they are not of the same length the result is just as long as the smallest
%%
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 % may be an error
| cons x xs => case ys
| nil => nil % may be an error
| cons y ys => cons (f x y) (map2 f xs ys);
%%
%% As `foldl` but user's function also takes element index as last argument
%%
foldli : (a : Type) ≡> (b : Type) ≡> (a -> b -> Int -> a) -> a -> List b -> a;
foldli = lambda f -> lambda o -> lambda xs -> let
helper : (a -> b -> Int -> a) -> Int -> a -> List b -> a;
helper = lambda f -> lambda i -> lambda o -> lambda xs -> case xs
| nil => o
| cons x xs => helper f (i + 1) (f o x i) xs;
in helper f 0 o xs;
%%
%% Fold 2 List as long as both List are non-empty
%%
fold2 : (a : Type) ≡> (b : Type) ≡> (c : Type) ≡> (a -> b -> c -> a) -> a -> List b -> List c -> a;
fold2 = lambda f -> lambda o -> lambda xs -> lambda ys -> case xs
| cons x xs => ( case ys
| cons y ys => fold2 f (f o x y) xs ys
| nil => o ) % may be an error
| nil => o; % may or may not be an error
%%
%% (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
| nil => i
| cons x xs => f x (foldr f xs i);
%%
%% Takes a function and a list
%% Returns `some x` if x is the first element on the list to return true
%% when applied to the function or `none` if there was no such element
%%
find : (a : Type) ≡> (a -> Bool) -> List a -> Option a;
find = lambda f -> lambda xs -> case xs
| nil => none
| 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 than n
%%
nth : (a : Type) ≡> Int -> List a -> a -> a;
nth = lambda n -> lambda xs -> lambda d -> case xs
| nil => d
| cons x xs
=> case Int_<= n 0
| true => x
| false => nth (n - 1) xs d;
%%
%% Reverse the element of a list
%% Common usage is `reverse ll nil` which reverse the list ll
%%
reverse : (a : Type) ≡> List a -> List a -> List a;
reverse = lambda l -> lambda t -> case l
| nil => t
| cons hd tl => reverse tl (cons hd t);
%%
%% Concat two list with first argument first
%%
concat : (a : Type) ≡> List a -> List a -> List a;
concat = lambda l -> lambda t -> reverse (reverse l nil) t;
%%
%% Apply all element of the list to an object through a function
%% (Should be as `fold-left` of any functional language)
%%
foldl : (a : Type) ≡> (b : Type) ≡> (a -> b -> a) -> a -> List b -> a;
foldl = lambda f -> lambda i -> lambda xs -> case xs
| nil => i
| cons x xs => foldl f (f i x) xs;
%%
%% Takes a function and a list
%% 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
| nil => nil
| cons x xs => ( case (f x)
| true => remove f xs
| false => cons x (remove f xs)
);
%%
%% Merge two List to a List of Pair
%% Both List must be of same length
%%
merge : (a : Type) ≡> (b : Type) ≡> List a -> List b -> List (Pair a b);
merge = lambda xs -> lambda ys -> case xs
| cons x xs => ( case ys
| cons y ys => cons (pair x y) (merge xs ys)
| nil => nil ) % error
| nil => nil;
%%
%% `Unmerge` a List of Pair
%% The two functions' name say it all
%%
map-fst : (a : Type) ≡> (b : Type) ≡> List (Pair a b) -> List a;
map-fst = lambda xs -> let
mf : Pair a b -> a;
mf p = case p | pair x _ => x;
in map mf xs;
map-snd : (a : Type) ≡> (b : Type) ≡> List (Pair a b) -> List b;
map-snd = lambda xs -> let
mf : Pair a b -> b;
mf p = case p | pair _ y => y;
in map mf xs;
%%
%% Is argument List empty
%%
empty? : (a : Type) ≡> List a -> Bool;
%%
%% O(N):
%% empty? = lambda xs -> Int_eq (length xs) 0;
%%
%% O(1):
empty? = lambda xs -> case xs
| nil => true
| _ => false;
%%%%
%%%% Sorting List
%%%%
%%
%% Using Quicksort but not in-place
%% Takes a comparison function and a list
%% Returns the same list but sorted
%%
%% 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
sortp : Option a -> List a -> List a -> List a -> List a;
sortp = lambda p -> lambda lt -> lambda gt -> lambda l -> case p
| none => nil
| some (pp) => ( case l
| nil => ( let
%% Sort the two sub-list
%% With the head as pivot
ltp : List a; ltp = sortp (head1 lt) nil nil (tail lt);
gtp : List a; gtp = sortp (head1 gt) nil nil (tail gt);
%% concatenate because we can't do it in-place
in concat ltp (cons pp gtp)
)
| cons x xs => ( case (o x pp)
%% partition with `p` as pivot
| true => sortp p lt (cons x gt) xs
| false => sortp p (cons x lt) gt xs
)
);
in sortp (head1 l) nil nil (tail l);
%%%% Some algo on sorted list
%%
%% 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 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
| nil => none
| cons x xs => ( case (f x)
| true => some x
| false => ( case (o x a)
| false => sfind o f a xs
| true => none
)
);
%%
%% Takes a function and a list
%% Returns all element which return true when applied to the function
%%
sall : (a : Type) ≡> (a -> Bool) -> List a -> List a;
sall = lambda f -> lambda l -> case l
| nil => nil
| cons x xs => ( case (f x)
| true => cons x (sall f xs)
| false => sall f xs
);
%%
%% Is some element member of the list?
%%
sexist? : (a : Type) ≡> (a -> a -> Bool) -> (a -> Bool) -> a -> List a -> Bool;
sexist? = lambda o -> lambda f -> lambda a -> lambda l -> case (sfind o f a l)
| none => false
| some _ => true;
%%
%% Insert an element into an already sorted list
%% Takes a comparison function, an element to insert and a list
%%
sinsert : (a : Type) ≡> (a -> a -> Bool) -> a -> List a -> List a;
sinsert = lambda o -> lambda a -> lambda l -> case l
| nil => cons a l
| cons x xs => ( case (o x a)
| true => cons a l
| false => cons x (sinsert o a xs)
);
%%
%% Takes a comparison function, a pivot and a list
%% Returns the sub-list with all element "greater" than pivot
%% (For exemple if the comparison function is `>` then it returns
%% all element greater or equal to pivot)
%%
ssup : (a : Type) ≡> (a -> a -> Bool) -> a -> List a -> List a;
ssup = lambda o -> lambda a -> lambda l -> case l
| nil => nil
| cons x xs => ( case (o x a)
| true => l
| false => ssup o a xs
);
%%
%% Takes a comparison function, a pivot and a list
%% Returns the sub-list with all element "smaller" than pivot
%% (For exemple if the comparison function is `>` then it returns
%% all element smaller than pivot)
%%
sinf : (a : Type) ≡> (a -> a -> Bool) -> a -> List a -> List a;
sinf = lambda o -> lambda a -> lambda l -> case l
| nil => nil
| cons x xs => ( case (o x a)
| true => nil
| false => cons x (sinf o a xs)
);
%%%%
%%%% Array from List
%%%%
%%
%% Takes a list and returns an array with the same element in the same order
%%
List->Array : (a : Type) ≡> List a -> Array a;
List->Array xs = let
helper : List a -> Array a -> Array a;
helper xs a = case xs
| cons x xs => helper xs (Array_append x a)
| nil => a;
in (helper xs (Array_empty ()));
btl/pervasive.typer
View file @ 2269559a
......@@ -154,6 +154,33 @@ List_foldl f i xs = case xs
| nil => i
| cons x xs => List_foldl f (f i x) xs;
List_mapi : (a : Type) ≡> (b : Type) ≡> (a -> Int -> b) -> List a -> List b;
List_mapi f xs = let
helper : (a -> Int -> b) -> Int -> List a -> List b;
helper f i xs = case xs
| nil => nil
| cons x xs => cons (f x i) (helper f (i + 1) xs);
in helper f 0 xs;
List_map2 : (?a -> ?b -> ?c) -> List ?a -> List ?b -> List ?c;
List_map2 f xs ys = case xs
| nil => nil
| cons x xs => case ys
| nil => nil % error
| cons y ys => cons (f x y) (List_map2 f xs ys);
%% Fold 2 List as long as both List are non-empty
List_fold2 : (?a -> ?b -> ?c -> ?a) -> ?a -> List ?b -> List ?c -> ?a;
List_fold2 f o xs ys = case xs
| cons x xs => ( case ys
| cons y ys => List_fold2 f (f o x y) xs ys
| nil => o ) % may be an error
| nil => o; % may or may not be an error
%% Is argument List empty?
List_empty : List ?a -> Bool;
List_empty xs = Int_eq (List_length xs) 0;
%%% Good 'ol combinators
I : ?a -> ?a;
......@@ -214,6 +241,10 @@ chain-decl : Sexp -> Sexp -> Sexp;
chain-decl a b =
Sexp_node (Sexp_symbol "_;_") (cons a (cons b nil));
chain-decl3 : Sexp -> Sexp -> Sexp -> Sexp;
chain-decl3 a b c =
Sexp_node (Sexp_symbol "_;_") (cons a (cons b (cons c nil)));
%% Build datacons:
%% ctor-name = datacons type-name ctor-name;
make-cons : Sexp -> Sexp -> Sexp;
......@@ -262,6 +293,28 @@ type-impl = lambda (x : List Sexp) ->
kerr % Float
kerr; % List of Sexp
get-args : Sexp -> List Sexp;
get-args sxp =
Sexp_dispatch sxp
(lambda _ args -> args) % Nodes
(lambda _ -> (nil : List Sexp)) % Symbol
(lambda _ -> (nil : List Sexp)) % String
(lambda _ -> (nil : List Sexp)) % Integer
(lambda _ -> (nil : List Sexp)) % Float
(lambda _ -> (nil : List Sexp)); % List of Sexp
get-type : Sexp -> Sexp;
get-type sxp =
Sexp_dispatch sxp
(lambda s ss -> case (Sexp_eq s (Sexp_symbol "_:_"))
| true => List_nth 1 ss Sexp_error
| false => sxp)
(lambda _ -> sxp)
(lambda _ -> Sexp_error)
(lambda _ -> Sexp_error)
(lambda _ -> Sexp_error)
(lambda _ -> Sexp_error);
get-head = List_head Sexp_error;
%% Get expression.
......@@ -281,6 +334,14 @@ type-impl = lambda (x : List Sexp) ->
inductive = Sexp_node (Sexp_symbol "typecons")
(cons name ctor);
%% Declare the inductive type as a function
%% Useful for recursive type
type-decl = quote ((uquote (get-name name)) : (uquote (
(List_foldl (lambda args arg ->
Sexp_node (Sexp_symbol "_->_") (cons (get-type arg) (cons args nil)))
(Sexp_symbol "Type") (List_reverse (get-args name) nil))
)));
decl = make-decl type-name inductive;
%% Add constructors.
......@@ -294,19 +355,13 @@ type-impl = lambda (x : List Sexp) ->
| nil => acc
in for-each ctor (Sexp_node (Sexp_symbol "_;_") nil)
%% return decls
in IO_return (chain-decl decl % inductive type declaration
ctors); % constructor declarations
%% return decls
in IO_return (chain-decl3 type-decl % type as a function declaration
decl % inductive type declaration
ctors); % constructor declarations
type_ = macro type-impl;
%%%% Backward compatibility
length = List_length;
head = List_head1;
tail = List_tail;
%%%% Tuples
%% Sample tuple: a module holding Bool and its constructors.
......@@ -317,7 +372,7 @@ BoolMod = (##datacons
%%
%% typecons _ (cons (τ₁ : Type) (t : τ₁)
%% (τ₂ : Type) (true : τ₂)
%% (τ₃ : Type) (false : τ₃)
%% (τ₃ : Type) (false : τ₃))
%%
%% And it's actually even worse because it tries to generalize
%% over the level of those `Type`s, so we end up with an invalid
......@@ -328,7 +383,8 @@ BoolMod = (##datacons
cons)
(_ := Bool) (_ := true) (_ := false);
Pair = typecons (Pair (a : Type) (b : Type)) (cons (x :: a) (y :: b));
Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b));
pair = datacons Pair pair;
__\.__ =
let mksel o f =
......@@ -356,6 +412,35 @@ __\.__ =
| nil => Sexp_error)
| nil => Sexp_error);
%% Triplet (tuple with 3 values)
type Triplet (a : Type) (b : Type) (c : Type)
| triplet (x : a) (y : b) (z : c);
%%%% List with tuple
%% Merge two List to a List of Pair
%% Both List must be of same length
List_merge : List ?a -> List ?b -> List (Pair ?a ?b);
List_merge xs ys = case xs
| cons x xs => ( case ys
| cons y ys => cons (pair x y) (List_merge xs ys)
| nil => nil ) % error
| nil => nil;
%% `Unmerge` a List of Pair
%% The two functions name said it all
List_map-fst : List (Pair ?a ?b) -> List ?a;
List_map-fst xs = let
mf : Pair ?a ?b -> ?a;
mf p = case p | pair x _ => x;
in List_map mf xs;
List_map-snd : List (Pair ?a ?b) -> List ?b;
List_map-snd xs = let
mf : Pair ?a ?b -> ?b;
mf p = case p | pair _ y => y;
in List_map mf xs;
%%%% Logic
%% `False` should be one of the many empty types.
......@@ -375,7 +460,7 @@ Decidable = typecons (Decidable (prop : Type))
%% Testing generalization in inductive type constructors.
LList : (a : Type) -> Int -> Type; %FIXME: `LList : ?` should be sufficient!
type LList (a : Type) n
type LList (a : Type) (n : Int)
| vnil (p ::: Eq n 0)
| vcons a (LList a ?n1) (p ::: Eq n (?n1 + 1)); %FIXME: Unsound wraparound!
......@@ -394,6 +479,28 @@ if_then_else_
| true => uquote e2
| false => uquote e3)));
%%%% More boolean
%% FIXME: Type annotations should not be needed below.
not : Bool -> Bool;
%% FIXME: We use braces here to delay parsing, otherwise the if/then/else
%% part of the grammar declared above is not yet taken into account.
not x = { if x then false else true };
or : Bool -> Bool -> Bool;
or x y = { if x then x else y };
and : Bool -> Bool -> Bool;
and x y = { if x then y else x };
xor : Bool -> Bool -> Bool;
xor x y = { if x then (not y) else y };
%% FIXME: Can't use ?a because that is generalized to be universe-polymorphic,
%% which we don't support in `load` yet.
fold : Bool -> (a : Type) ≡> a -> a -> a;
fold x t e = { if x then t else e};
%%%% Test
test1 : ?;
test2 : Option Int;
......@@ -409,4 +516,151 @@ test4 : Option Int;
test4 = test1 : Option ?;
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);
%%%%
%%%% Common library
%%%%
%%
%% `<-` 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
%%
%% e.g.:
%% do { IO_return true; };
%%
do = let lib = load "btl/do.typer" in lib.do;
%%
%% Module containing various macros for tuple
%% Used by `case_`
%%
tuple-lib = load "btl/tuple.typer";
%%
%% Get the nth element of a tuple
%%
%% e.g.:
%% tuple-nth tup 0;
%%
tuple-nth = tuple-lib.tuple-nth;
%%
%% Affectation of tuple
%%
%% e.g.:
%% (x,y,z) <- tup;
%%
_<-_ = tuple-lib.assign-tuple;
%%
%% Instantiate a tuple from expressions
%%
%% e.g.:
%% tup = (x,y,z);
%%
_\,_ = tuple-lib.make-tuple;
Tuple = tuple-lib.tuple-type;
%%
%% 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
%%
%% 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
%%
%% e.g.:
%% my-fun (x : Bool)
%% | true => false
%% | false => true;
%%
_|_ = let lib = load "btl/polyfun.typer" in lib._|_;
%%%% Unit tests function for doing file
%% It's hard to do a primitive which execute test file
%% because of circular dependency...
%%
%% A macro using `load` for unit testing purpose
%%
%% Takes a file name (String) as argument
%% 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!
%%
Test_file = macro (lambda args -> let
%% return an empty command on error
ret = Sexp_node
(Sexp_symbol "IO_return")
(cons (Sexp_symbol "unit") nil);
%% Expecting a String and nothing else
in IO_return (Sexp_dispatch (List_nth 0 args Sexp_error)
(lambda _ _ -> ret)
(lambda _ -> ret)
%% `load` is a special form and takes a Sexp rather than a real `String`
(lambda s -> quote (let lib = load (uquote (Sexp_string s)); in lib.exec-test))
(lambda _ -> ret)
(lambda _ -> ret)
(lambda _ -> ret))
);
%%% pervasive.typer ends here.
btl/plain-let.typer 0 → 100644
View file @ 2269559a
%%% plain-let.typer --- Basic "parallel" `let`
%% List_nth = list.nth;
%% List_fold2 = list.fold2;
%% List_map = list.map;
%% List_foldl = list.foldl;
%% List_reverse = list.reverse;
%% List_tail = list.tail;
%%
%% The idea is to use unique identifier in a first let
%% and then assign those unique identifier to the original symbol
%%
%% Useful for auto-generated code (macro, ...)
%%
%%
%% Takes the plain argument of macro `plain-let`
%% Returns the `plain-let` code
%%
impl : List Sexp -> IO Sexp;
impl args = let
%% Error use in Sexp_dispatch
serr = lambda _ -> Sexp_error;
%% Takes an assignment statement and return a new
%% symbol for the resulting variable
%% For function it only rename the function name and not the argument
gen-sym : Sexp -> IO Sexp;
gen-sym arg = let
%% error use in Sexp_dispatch
io-serr = lambda _ -> IO_return Sexp_error;
%% Get a `gensym` symbol
%% It can rename a function name (not the argument)
%% or just a symbol
rename : Sexp -> IO Sexp;
rename sexp = Sexp_dispatch sexp
(lambda _ ss -> do {
name <- gensym ();
IO_return (Sexp_node name ss);
})
(lambda _ -> gensym ())
io-serr io-serr io-serr io-serr;
in Sexp_dispatch arg
(lambda s ss -> if (Sexp_eq s (Sexp_symbol "_=_")) then
(rename (List_nth 0 ss Sexp_error)) else
(IO_return Sexp_error))
io-serr io-serr io-serr io-serr io-serr;
%% Takes an assignment statement and return the right-hand side
get-def : Sexp -> Sexp;
get-def arg = Sexp_dispatch arg
(lambda s ss -> if (Sexp_eq s (Sexp_symbol "_=_")) then
(List_nth 1 ss Sexp_error) else
(Sexp_error))
serr serr serr serr serr;
%% Takes an assignment statement and return the left-hand side
get-var : Sexp -> Sexp;
get-var arg = Sexp_dispatch arg
(lambda s ss -> if (Sexp_eq s (Sexp_symbol "_=_")) then
(List_nth 0 ss Sexp_error) else
(Sexp_error))
serr serr serr serr serr;
%% Takes a list of assignment and return a list of pair of `gensym` and definition (rhs)
get-sym-def : List Sexp -> IO (List (Pair Sexp Sexp));
get-sym-def args = do {
r <- List_foldl (lambda o arg -> do {
o <- o;
sym <- gen-sym arg;
def <- IO_return (get-def arg);
IO_return (cons (pair sym def) o); % order doesn't matter
}) (IO_return nil) args;
IO_return r;
};
%% Takes a list of assignment and the output of `get-sym-def`
%% Returns a list of pair of `gensym` and original symbol
get-var-sym : List Sexp -> List (Pair Sexp Sexp) -> IO (List (Pair Sexp Sexp));
get-var-sym args syms = let
ff : IO (List (Pair Sexp Sexp)) -> Pair Sexp Sexp -> Sexp -> IO (List (Pair Sexp Sexp));
ff o p arg = do {
o <- o;
sym <- IO_return (case p | pair s _ => s);
var <- IO_return (get-var arg);
IO_return (cons (pair var sym) o);
};
in do {
r <- List_fold2 ff (IO_return nil) syms args;
IO_return r;
};
%% Takes a list of assignment and a body (likely using those assignment)
%% 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));
%% Takes a list of assignment and separate them with `;`
let-decls : List Sexp -> Sexp;
let-decls decls = Sexp_node (Sexp_symbol "_;_") decls;
%% 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]
gen-code : List (Pair Sexp Sexp) -> List (Pair Sexp Sexp) -> Sexp -> Sexp;
gen-code sym-def var-sym body = let
mf : Pair Sexp Sexp -> Sexp;
mf p = case p | pair s0 s1 =>
Sexp_node (Sexp_symbol "_=_") (cons s0 (cons s1 nil));
decls0 = List_map mf sym-def;
decls1 = List_map mf var-sym;
in let-in (let-decls decls0) (let-in (let-decls decls1) body);
%% Returns a list of assignment from a "_;_"-node
get-decls : Sexp -> List Sexp;
get-decls sexp = let
xserr = lambda _ -> (nil : List Sexp);
in Sexp_dispatch sexp
(lambda s ss -> if (Sexp_eq s (Sexp_symbol "_;_")) then
(ss) else
(nil))
xserr xserr xserr xserr xserr;
in do {
%% get list of pair and use it to generate `plain-let`
defs <- IO_return (get-decls (List_nth 0 args Sexp_error));
body <- IO_return (List_nth 1 args Sexp_error);
sym-def <- get-sym-def defs;
sym-def <- IO_return (List_reverse (List_tail sym-def) nil);
var-sym <- get-var-sym defs sym-def;
IO_return (gen-code sym-def var-sym body);
};
%% just calling the `impl` function in a macro
plain-let-macro = macro (lambda args -> do {
r <- impl args;
%% Sexp_debug_print r;
IO_return r;
});
btl/polyfun.typer 0 → 100644
View file @ 2269559a
%%% polyfun.typer --- Function definition by cases
%%
%% Error use in Sexp_dispatch
%%
serr : (a : Type) ≡> a -> Sexp;
serr = lambda _ -> Sexp_error;
xserr : (a : Type) ≡> a -> List Sexp;
xserr = lambda _ -> (nil : List Sexp);
%% List_nth = list.nth;
%% List_map = list.map;
%% List_tail = list.tail;
%%
%% Takes a function node with its argument and the body as a second argument
%% Returns a definition with a `;`
%%
fun-decl : Sexp -> Sexp -> Sexp;
fun-decl decl body = Sexp_node (Sexp_symbol "_;_") (cons (quote (
(uquote decl) = (uquote body)
)) nil);
%%
%% Sexp_node (Sexp_symbol "_;_") (cons
%% (Sexp_node (Sexp_symbol "_=_") (cons decl (cons body nil)))
%% nil);
%%
%%
%% Takes a function node with it's argument (`f x y`)
%% Returns a list of the symbol of every argument
%% (for `f (x : Int) y` it returns a list containing symbol "x" and "y")
%%
fun-args : Sexp -> List Sexp;
fun-args decl = Sexp_dispatch decl
(lambda s ss -> let
mf : Sexp -> Sexp;
mf arg = Sexp_dispatch arg
(lambda s ss ->
if (Sexp_eq s (Sexp_symbol "_:_")) then
(List_nth 0 ss Sexp_error)
else
(Sexp_node s ss))
(lambda s -> Sexp_symbol s)
serr serr serr serr;
in List_map mf ss)
xserr xserr xserr xserr xserr;
%%
%% Takes a list of "_=>_"-node
%% Returns a list of (pattern, body) pair
%%
fun-cases : List Sexp -> List (Pair Sexp Sexp);
fun-cases args = let
mf : Sexp -> Pair Sexp Sexp;
mf arg = let
err = lambda _ -> pair Sexp_error Sexp_error;
in Sexp_dispatch arg
(lambda s ss ->
if (Sexp_eq s (Sexp_symbol "_=>_")) then
(pair (List_nth 0 ss Sexp_error) (List_nth 1 ss Sexp_error))
else
(err ()))
err err err err err;
in List_map mf args;
%%
%% 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;
cases-to-sexp vars cases = let
mf : Pair Sexp Sexp -> Sexp;
mf p = case p | pair pat body =>
Sexp_node (Sexp_symbol "_=>_")
(cons pat (cons body nil));
tup : Bool;
tup = Int_< 1 (List_length vars);
in Sexp_node (Sexp_symbol "case_") (cons
(Sexp_node (Sexp_symbol "_|_") (cons
(if tup then
(Sexp_node (Sexp_symbol "_,_") vars)
else
(List_nth 0 vars Sexp_error))
(List_map mf cases))) nil);
%%
%% The macro we want
%%
%% I expect a function node and then "_=>_"-nodes
%%
_|_ = macro (lambda args -> let
%% function with argument (e.g. `f x y`)
decl : Sexp;
decl = List_nth 0 args Sexp_error;
%% symbol to match
fargs : List Sexp;
fargs = fun-args decl;
%% pattern for argument match
cases : List (Pair Sexp Sexp);
cases = fun-cases (List_tail args);
in do {
IO_return (fun-decl decl (cases-to-sexp fargs cases));
});
btl/tuple.typer 0 → 100644
View file @ 2269559a
%%% tuple.typer --- Notation `_,_` for tuples
%% Here's an example similar to tuple from `load`
%%
%% Sample tuple: a module holding Bool and its constructors.
%%
%% We need the `?` metavars to be lexically outside of the
%% `typecons` expression, otherwise they end up generalized, so
%% we end up with a type constructor like
%%
%% typecons _ (cons (τ₁ : Type) (t : τ₁)
%% (τ₂ : Type) (true : τ₂)
%% (τ₃ : Type) (false : τ₃))
%%
%% And it's actually even worse because it tries to generalize
%% over the level of those `Type`s, so we end up with an invalid
%% inductive type.
%%
%% BoolMod = (##datacons
%% ((lambda t1 t2 t3
%% -> typecons _ (cons (t :: t1) (true :: t2) (false :: t3)))
%% ? ? ?)
%% cons)
%% (_ := Bool) (_ := true) (_ := false);
%%
%% List_nth = list.nth;
%% List_map = list.map;
%% List_mapi = list.mapi;
%% List_map2 = list.map2;
%% List_concat = list.concat;
%%
%% Move IO outside List (from element to List)
%% (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);
ff o v = do {
o <- o;
v <- v;
IO_return (cons v o);
};
in do {
l <- (List_foldl ff (IO_return nil) l);
IO_return (List_reverse l nil);
};
%%
%% Generate a List of pseudo-unique symbol
%%
%% Takes a List of Sexp and generate a List of new name of the same length
%% whatever are the element of the List
%%
gen-vars : List Sexp -> IO (List Sexp);
gen-vars vars = io-list (List_map
(lambda _ -> gensym ())
vars);
%%
%% Reference for tuple's implicit field name
%%
%% Takes a list of vars (it could actually only takes a length)
%% Returns symbol `%n` with n in [0,length) (integer only, obviously)
%%
gen-tuple-names : List Sexp -> List Sexp;
gen-tuple-names vars = List_mapi
(lambda _ i -> Sexp_symbol (String_concat "%" (Int->String i)))
vars;
%%
%% Takes a list
%% Returns a list of the same length with every element set to "?" symbol
%%
gen-deduce : List Sexp -> List Sexp;
gen-deduce vars = List_map
(lambda _ -> Sexp_symbol "?")
vars;
%%%
%%% Access one tuple's element
%%%
%%
%% This is a macro with conceptualy this signature:
%% tuple-nth : (tup-type : Type) ≡> (elem-type : Type) ≡> tup-type -> Int -> elem-type;
%%
%% Returns the n'th element of the tuple
%%
tuple-nth = macro (lambda args -> let
nerr = lambda _ -> (Int->Integer (-1));
%% argument `n` of this macro
n : Integer;
n = Sexp_dispatch (List_nth 1 args Sexp_error)
(lambda _ _ -> nerr ())
nerr nerr
(lambda n -> n)
nerr nerr;
%% implicit tuple field name
elem-sym : Sexp;
elem-sym = Sexp_symbol (String_concat "%" (Integer->String n));
%% tuple, argument of this macro
tup : Sexp;
tup = List_nth 0 args Sexp_error;
in IO_return (Sexp_node (Sexp_symbol "__.__") (cons tup (cons elem-sym nil)))
);
%%%
%%% Affectation, unwraping tuple
%%%
%%
%% syntax:
%% (x, y, z) <- p;
%%
%% and then `x`, `y`, `z` are defined as tuple's element 0, 1, 2
%%
assign-tuple = macro (lambda args -> let
xserr = lambda _ -> (nil : List Sexp);
%% Expect a ","-node
%% Returns variables
get-tup-elem : Sexp -> List Sexp;
get-tup-elem sexp = Sexp_dispatch sexp
(lambda s ss ->
if (Sexp_eq s (Sexp_symbol "_,_")) then
(ss)
else
(nil))
xserr xserr xserr xserr xserr;
%% map every tuple's variable
%% using `tuple-nth` to assign element to variable
mf : Sexp -> Sexp -> Int -> Sexp;
mf t arg i = Sexp_node (Sexp_symbol "_=_")
(cons arg (cons (Sexp_node (Sexp_symbol "tuple-nth")
(cons t (cons (Sexp_integer (Int->Integer i)) nil))) nil));
in do {
IO_return (Sexp_node (Sexp_symbol "_;_") (List_mapi
(mf (List_nth 1 args Sexp_error))
(get-tup-elem (List_nth 0 args Sexp_error))));
});
%%
%% 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 Sexp -> List Sexp -> Sexp -> Sexp;
wrap-vars ivars rvars 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;
%%
%% 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;
make-tuple-impl values = let
%% map tuple element declaration
mf1 : Sexp -> Sexp -> Sexp;
mf1 name value = Sexp_node (Sexp_symbol "_::_") (cons name (cons value nil));
%% map tuple element value
mf2 : Sexp -> Sexp -> Sexp;
mf2 value nth = Sexp_node (Sexp_symbol "_:=_") (cons nth (cons value nil));
ff1 : Sexp -> Sexp -> Sexp -> Sexp;
ff1 body arg arg-t = Sexp_node (Sexp_symbol "lambda_->_")
(cons (Sexp_node (Sexp_symbol "_:_") (cons arg (cons arg-t nil)))
(cons body nil));
ff2 : Sexp -> Sexp -> Sexp;
ff2 body arg = Sexp_node (Sexp_symbol "lambda_≡>_")
(cons (Sexp_node (Sexp_symbol "_:_") (cons arg (cons (Sexp_symbol "Type") nil)))
(cons body nil));
in do {
args-t <- gen-vars values;
args <- gen-vars values;
names <- IO_return (gen-tuple-names values);
tuple-t <- IO_return (Sexp_node (Sexp_symbol "typecons")
(cons (Sexp_symbol "Tuple")
(cons (Sexp_node (Sexp_symbol "cons") (List_map2 mf1 names args-t)) nil)));
tuple <- IO_return (Sexp_node (Sexp_node (Sexp_symbol "datacons")
(cons tuple-t (cons (Sexp_symbol "cons") nil)))
(List_map2 mf2 args names));
fun <- IO_return (List_foldl ff2
(List_fold2 ff1 tuple (List_reverse args nil)
(List_reverse args-t nil))
(List_reverse args-t nil));
values <- IO_return (List_reverse values nil);
affect <- IO_return (Sexp_node fun (List_reverse values nil));
IO_return affect;
};
%%
%% Macro to instantiate a tuple
%%
make-tuple = macro (lambda args -> do {
r <- make-tuple-impl args;
r <- IO_return r;
IO_return r;
});
%%
%% Macro returning the type of a tuple
%%
%% Takes element's type as argument
%%
tuple-type = macro (lambda args -> let
mf : Sexp -> Sexp -> Sexp;
mf n t = Sexp_node (Sexp_symbol "_::_")
(cons n (cons t nil));
in do {
names <- IO_return (gen-tuple-names args);
r <- IO_return (Sexp_node (Sexp_symbol "typecons") (cons
(Sexp_symbol "Tuple") (cons (Sexp_node (Sexp_symbol "cons")
(List_map2 mf names args)) nil)));
IO_return r;
});
samples/array_test.typer 0 → 100644
View file @ 2269559a
%%%%
%%%% Unit test for builtin primitive `Array`
%%%%
List->Array = list.List->Array;
len = Array_length;
get = Array_get (-1);
a0 : Array Int;
a0 = Array_create 0 0;
a1 : Array Int;
a1 = Array_create 5 0;
a2 : Array Int;
a2 = Array_append 2 (Array_append 1 a0);
a3 : Array Int;
a3 = Array_append 6 (Array_append 5 a1);
a4 : Array Int;
a4 = Array_set 1 1 (Array_set 2 2 (Array_set 3 3 (Array_set 4 4 a3)));
empty : Array Int;
empty = Array_empty ();
empty2 : Array Int;
empty2 = List->Array nil;
from-list : Array Int;
from-list = List->Array (cons 0 (cons 1 (cons 2 nil)));
test-length = do {
Test_info "ARRAY" "length";
r0 <- Test_eq "a0" (len a0) 0;
r1 <- Test_eq "empty" (len empty) (len a0);
r2 <- Test_eq "a1" (len a1) 5;
r3 <- Test_eq "a2" (len a2) 2;
r4 <- Test_eq "a3" (len a3) 7;
r5 <- Test_eq "a4" (len a4) 7;
success <- IO_return (and r0 (and r1 (and r2 (and r3 (and r4 r5)))));
if success then
(Test_info "ARRAY" "test on length succeeded")
else
(Test_warning "ARRAY" "test on length failed");
IO_return success;
};
test-get = do {
Test_info "ARRAY" "get";
r0 <- Test_eq "a1" (get 3 a1) 0;
r1 <- Test_eq "a2" (get 0 a2) 1;
r2 <- Test_eq "a3" (get 6 a3) 6;
r3 <- Test_eq "a4" (get 3 a4) 3;
r4 <- Test_eq "out of bounds" (get 10 a4) (-1);
success <- IO_return (and r0 (and r1 (and r2 (and r3 r4))));
if success then
(Test_info "ARRAY" "test on get succeeded")
else
(Test_warning "ARRAY" "test on get failed");
IO_return success;
};
test-from-list = do {
Test_info "ARRAY" "List->Array";
r0 <- Test_eq "empty2" (len empty2) 0;
r1 <- Test_eq "len" (len from-list) 3;
r2 <- Test_eq "from-list 0" (get 0 from-list) 0;
r3 <- Test_eq "from-list 1" (get 1 from-list) 1;
r4 <- Test_eq "from-list 2" (get 2 from-list) 2;
r5 <- Test_eq "out of bounds" (get 3 from-list) (-1);
success <- IO_return (and r0 (and r1 (and r2 (and r3 (and r4 r5)))));
if success then
(Test_info "ARRAY" "test on List->Array succeeded")
else
(Test_warning "ARRAY" "test on List->Array failed");
IO_return success;
};
exec-test = do {
b1 <- test-length;
b2 <- test-get;
b3 <- test-from-list;
IO_return (and b1 (and b2 b3));
};
samples/batch_test.typer 0 → 100644
View file @ 2269559a
%%%%
%%%% File for testing mutiple unit tests file written in Typer
%%%%
%%
%% Some tests use `Elab_getenv ()` which may fail if
%% The tests use internal declaration
%%
%% declaration from elabctx_test.typer
type AllErasable
| ctor1 (a ::: Int) (b ::: Bool) (c ::: Option Bool);
type AllImplicit
| ctor2 (a :: Int) (b :: Bool) (c :: Option Bool);
type AllExplicit
| ctor3 (a : Int) (b : Bool) (c : Option Bool);
type AllAny
| ctor4 (a ::: Int) (b :: Bool) (c : Option Bool);
%% End of elabctx_test.typer declaration
u1 = Test_file "./samples/array_test.typer";
u2 = Test_file "./samples/elabctx_test.typer";
u3 = Test_file "./samples/case_test.typer";
u4 = Test_file "./samples/polyfun_test.typer";
%%
%% This test is currently failling due to type error in ELAB and TC
%% 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;
Test_info "BATCH TESTS" "\n\n\tnext file\n";
b2 <- u2;
Test_info "BATCH TESTS" "\n\n\tnext file\n";
b3 <- u3;
Test_info "BATCH TESTS" "\n\n\tnext file\n";
b4 <- u4;
%% Test_info "BATCH TESTS" "\n\n\tnext file\n";
%% b5 <- u5;
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 (and b6 b7))))));
success <- IO_return (and b1 (and b2 (and b3 (and b4 (and b6 b7)))));
if success then
(Test_info "BATCH TESTS" "all tests succeeded")
else
(Test_warning "BATCH TESTS" "some tests failed");
};
samples/bbst.typer 0 → 100644
View file @ 2269559a
This diff is collapsed.
samples/bbst_test.typer 0 → 100644
View file @ 2269559a
%%%%
%%%% Tests on Bbst
%%%%
t0 : Bbst Int;
t0 = int-range1 0 100;
t1 : Bbst Int;
t1 = remove-range 25 75 t0;
t2 : Bbst Int;
t2 = insert (-1) (insert 50 (insert 100 t1));
t3 : Bbst Int;
t3 = insert 100 (insert (-1) (insert 50 t2));
t4 : Bbst Int;
t4 = remove (-1) (remove 10 (remove 100 t3));
t5 : Bbst Int;
t5 = remove (-2) (remove 101 (remove 10 t4));
e0 : Bbst Int;
e0 = int-empty;
e1 : Bbst Int;
e1 = insert 777 e0;
e2 : Bbst Int;
e2 = remove 777 e1;
%% insert and remove doesn't need to be tested:
%% every test will fail if those are broken
test-length = do {
Test_info "BBST" "length";
r0 <- Test_eq "t0" (length t0) 100;
r1 <- Test_eq "t1" (length t1) 50;
r2 <- Test_eq "t2" (length t2) 53;
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" (empty? e0);
r7 <- Test_eq "e1" (length e1) 1;
r8 <- Test_eq "e2" (length e2) 0;
if (and r0 (and r1 (and r2 (and r3 (and r4 (and r5 (and r6 (and r7 r8)))))))) then
(Test_info "BBST" "length test succeeded")
else
(Test_warning "BBST" "length test failed");
};
test-find = do {
Test_info "BBST" "find";
r0 <- Test_eq "10 in t0" (find 10 t0) (some 10);
r1 <- Test_eq "25 not in t1" (find 25 t1) none;
r2 <- Test_eq "-1 in t2" (find (-1) t2) (some (-1));
r3 <- Test_eq "50 in t3" (find 50 t3) (some 50);
r4 <- Test_eq "10 not in t4" (find 10 t4) none;
r5 <- Test_eq "-2 not in t5" (find (-2) t5) none;
r6 <- Test_eq "10 not in e0" (find 10 e0) none;
r7 <- Test_eq "777 in e1" (find 777 e1) (some 777);
r8 <- Test_eq "777 not in e2" (find 777 e2) none;
if (and r0 (and r1 (and r2 (and r3 (and r4 (and r5 (and r6 (and r7 r8)))))))) then
(Test_info "BBST" "find test succeeded")
else
(Test_warning "BBST" "find test failed");
};
%% member? is just a wrapped version of find so not need to test it
%% in the actual implementation
test-fold = do {
Test_info "BBST" "order";
v0 <- IO_return (foldl
(lambda o e -> if (Int_> o e) then 1000 else e)
(-1000) t5);
v1 <- IO_return (foldr
(lambda o e -> if (Int_< o e) then (-1000) else e)
(1000) t5);
r0 <- Test_false "v0" (Int_eq v0 1000);
r1 <- Test_false "v1" (Int_eq v1 (-1000));
if (and r0 r1) then
(Test_info "BBST" "order test succeeded")
else
(Test_warning" BBST" "order test failed");
};
u = (IO_run test-length) ();
u = (IO_run test-find) ();
u = (IO_run test-fold) ();
samples/bool.typer 0 → 100644
View file @ 2269559a
%%% bool.typer --- Library of plain old booleans
%% Call it `t` so when we do `Bool = load "bool.typer"`, we
%% can use `Bool.t` to refer to the type.
%% FIXME: In a type context, `Bool` should then automatically be "coerced"
%% to `Bool.t`.
type t
| false
| true;
%% FIXME: These grammar settings currently only apply to this file,
%% whereas they should be import(ed|able) via something like `load`.
define-operator "if" () 2;
define-operator "then" 2 1;
define-operator "else" 1 66;
if_then_else_
= macro (lambda args ->
let e1 = List_nth 0 args Sexp_error;
e2 = List_nth 1 args Sexp_error;
e3 = List_nth 2 args Sexp_error;
in IO_return (quote (case uquote e1
| true => uquote e2
| false => uquote e3)));
%% FIXME: Type annotations should not be needed below.
not : t -> t;
%% FIXME: We use braces here to delay parsing, otherwise the if/then/else
%% part of the grammar declared above is not yet taken into account.
not x = { if x then false else true };
or : t -> t -> t;
or x y = { if x then x else y };
and : t -> t -> t;
and x y = { if x then y else x };
xor : t -> t -> t;
xor x y = { if x then (not y) else y };
%% FIXME: Can't use ?a because that is generalized to be universe-polymorphic,
%% which we don't support in `load` yet.
fold : t -> (a : Type) ≡> a -> a -> a;
fold x t e = { if x then t else e};
samples/case_test.typer 0 → 100644
View file @ 2269559a
%%%%
%%%% Unit tests for macro `case`
%%%%
b2i : Bool -> Int;
b2i a = case a
| true => 1
| _ => 0;
last : List Int -> Option Int;
last xs = case xs
| cons x nil => some x
| cons x xs => last xs
| _ => none;
test-one-var = do {
Test_info "MACRO CASE" "one variable";
r0 <- Test_eq "b2i" (b2i true) 1;
r1 <- Test_eq "b2i" (b2i false) 0;
r2 <- Test_eq "last" (last nil) none;
r3 <- Test_eq "last" (last (cons 1 nil)) (some 1);
r4 <- Test_eq "last" (last (cons 1 (cons 2 nil))) (some 2);
success <- IO_return (and r0 (and r1 (and r2 (and r3 r4))));
if success then
(Test_info "MACRO CASE" "test on one variable succeeded")
else
(Test_warning "MACRO CASE" "test on one variable failed");
IO_return success;
};
dflt1 : Bool -> Bool -> Bool -> Int;
dflt1 a b c = case (a,b,c)
| (true,false,_) => 1
| (false,_,true) => 2
| (_,true,false) => 3
| (true,true,true) => 4
| (_,_,_) => 0;
dflt2 : Bool -> Bool -> Bool -> Int;
dflt2 a b c = case (a,b,c)
| (true,true,true) => 4
| (_,true,false) => 3
| (false,_,true) => 2
| (true,false,_) => 1
| (_,_,_) => 0;
dflt3 : Bool -> Bool -> Bool -> Int;
dflt3 a b c = case (a,b,c)
| (_,_,true) => 777
| (_,false,false) => 888
| (_,_,_) => 999;
nand : Bool -> Bool -> Bool;
nand b0 b1 = case (b0,b1)
| (true,true) => false
| _ => true;
test-dflt = do {
Test_info "MACRO CASE" "default";
r0 <- Test_eq "dflt1" (dflt1 true true true) 4;
r1 <- Test_eq "dflt1" (dflt1 true true false) 3;
r2 <- Test_eq "dflt1" (dflt1 true false true) 1;
r3 <- Test_eq "dflt1" (dflt1 true false false) 1;
r4 <- Test_eq "dflt1" (dflt1 false true true) 2;
r5 <- Test_eq "dflt1" (dflt1 false true false) 3;
r6 <- Test_eq "dflt1" (dflt1 false false true) 2;
r7 <- Test_eq "dflt1" (dflt1 false false false) 0;
r8 <- Test_eq "dflt2" (dflt1 true true true) 4;
r9 <- Test_eq "dflt2" (dflt1 true true false) 3;
r10 <- Test_eq "dflt2" (dflt1 true false true) 1;
r11 <- Test_eq "dflt2" (dflt1 true false false) 1;
r12 <- Test_eq "dflt2" (dflt1 false true true) 2;
r13 <- Test_eq "dflt2" (dflt1 false true false) 3;
r14 <- Test_eq "dflt2" (dflt1 false false true) 2;
r15 <- Test_eq "dflt2" (dflt1 false false false) 0;
r16 <- Test_false "nand" (nand true true);
r17 <- Test_true "nand" (nand true false);
r18 <- Test_true "nand" (nand false true);
r19 <- Test_true "nand" (nand false false);
r20 <- Test_eq "dflt3" (dflt3 true false false) 888;
r21 <- Test_eq "dflt3" (dflt3 true true false) 999;
r22 <- Test_eq "dflt3" (dflt3 true false true) 777;
part1 <- IO_return (and r0 (and r1 (and r2 (and r3
(and r4 (and r5 (and r6 r7)))))));
part2 <- IO_return (and r8 (and r9 (and r10 (and r11
(and r12 (and r13 (and r14 r15)))))));
part3 <- IO_return (and r16 (and r17 (and r18 r19)));
part4 <- IO_return (and r20 (and r21 r22));
success <- IO_return (and part1 (and part2 (and part3 part4)));
if success then
(Test_info "MACRO CASE" "test on default succeeded")
else
(Test_warning "MACRO CASE" "test on default failed");
IO_return success;
};
sum : List Int -> List Int -> Int;
sum xs ys = case (xs,ys)
| (cons x xs,cons y ys) => (x + y) + (sum xs ys)
| (_,_) => 0;
rm-last : List Int -> List Int;
rm-last xs = case xs
| cons x nil => (nil : List Int)
| cons x xs => cons x (rm-last xs)
| _ => (nil : List Int);
test-list = do {
Test_info "MACRO CASE" "list";
r0 <- Test_eq "sum" (sum nil nil) 0;
r1 <- Test_eq "sum" (sum (cons 1 nil) (cons 1 nil)) 2;
r2 <- Test_eq "sum" (sum (cons 1 (cons 100 nil)) (cons 1 nil)) 2;
r3 <- Test_eq "rm-last" (rm-last nil) nil;
r4 <- Test_eq "rm-last" (rm-last (cons 1 nil)) nil;
r5 <- Test_eq "rm-last" (rm-last (cons 1 (cons 2 nil))) (cons 1 nil);
success <- IO_return (and r0 (and r1 (and r2 (and r3 (and r4 r5)))));
if success then
(Test_info "MACRO CASE" "test on list succeeded")
else
(Test_warning "MACRO CASE" "test on list failed");
IO_return success;
};
type APColor
| ap-red
| ap-green
| ap-blue;
type SPColor
| sp-magenta
| sp-cyan
| sp-yellow;
type Color
| red
| magenta
| blue
| cyan
| green
| yellow
| white
| black;
mix-add : APColor -> APColor -> Color;
mix-add a b = case (a, b)
| (ap-red, ap-red) => red
| (ap-blue, ap-blue) => blue
| (ap-green, ap-green) => green
| (ap-red, ap-blue) => magenta
| (ap-blue, ap-red) => magenta
| (ap-blue, ap-green) => cyan
| (ap-green, ap-blue) => cyan
| (ap-green, ap-red) => yellow
| (ap-red, ap-green) => yellow;
mix-sub : SPColor -> SPColor -> Color;
mix-sub a b = case (a, b)
| (sp-magenta, sp-magenta) => magenta
| (sp-cyan, sp-cyan) => cyan
| (sp-yellow, sp-yellow) => yellow
| (sp-magenta, sp-cyan) => blue
| (sp-cyan, sp-magenta) => blue
| (sp-cyan, sp-yellow) => green
| (sp-yellow, sp-cyan) => green
| (sp-yellow, sp-magenta) => red
| (sp-magenta, sp-yellow) => red;
to-ap : Color -> Option APColor;
to-ap c = case c
| red => some ap-red
| green => some ap-green
| blue => some ap-blue
| _ => none;
to-sp : Color -> Option SPColor;
to-sp c = case c
| magenta => some sp-magenta
| cyan => some sp-cyan
| yellow => some sp-yellow
| _ => none;
test-color = do {
Test_info "MACRO CASE" "color";
r0 <- Test_eq "mix-add" (mix-add ap-red ap-red) red;
r1 <- Test_eq "mix-add" (mix-add ap-blue ap-blue) blue;
r2 <- Test_eq "mix-add" (mix-add ap-green ap-green) green;
r3 <- Test_eq "mix-add" (mix-add ap-red ap-blue) magenta;
r4 <- Test_eq "mix-add" (mix-add ap-blue ap-red) magenta;
r5 <- Test_eq "mix-add" (mix-add ap-blue ap-green) cyan;
r6 <- Test_eq "mix-add" (mix-add ap-green ap-blue) cyan;
r7 <- Test_eq "mix-add" (mix-add ap-green ap-red) yellow;
r8 <- Test_eq "mix-add" (mix-add ap-red ap-green) yellow;
r9 <- Test_eq "mix-sub" (mix-sub sp-magenta sp-magenta) magenta;
r10 <- Test_eq "mix-sub" (mix-sub sp-cyan sp-cyan) cyan;
r11 <- Test_eq "mix-sub" (mix-sub sp-yellow sp-yellow) yellow;
r12 <- Test_eq "mix-sub" (mix-sub sp-magenta sp-cyan) blue;
r13 <- Test_eq "mix-sub" (mix-sub sp-cyan sp-magenta) blue;
r14 <- Test_eq "mix-sub" (mix-sub sp-cyan sp-yellow) green;
r15 <- Test_eq "mix-sub" (mix-sub sp-yellow sp-cyan) green;
r16 <- Test_eq "mix-sub" (mix-sub sp-yellow sp-magenta) red;
r17 <- Test_eq "mix-sub" (mix-sub sp-magenta sp-yellow) red;
part1 <- IO_return (and r0 (and r1 (and r2 (and r3 (and r4
(and r5 (and r6 (and r7 r8))))))));
part2 <- IO_return (and r9 (and r10 (and r11 (and r12 (and r13
(and r14 (and r15 (and r16 r17))))))));
success <- IO_return (and part1 part2);
if success then
(Test_info "MACRO CASE" "test on color succeeded")
else
(Test_warning "MACRO CASE" "test on color failed");
IO_return success;
};
f1 : List (Option Bool) -> List (Option Bool) -> Int;
f1 xs ys = case (xs,ys)
| (cons (some true) xs, cons (some true) ys) => f1 xs ys
| (cons none nil, cons none nil) => 2
| (nil,nil) => 1
| (_,_) => 0;
f3 : Option Bool -> Option Bool -> Int;
f3 ob0 ob1 = case (ob0,ob1)
| (some true, some true) => 0
| (some false, some true) => 1
| (some true, some false) => 2
| (some false, some false) => 3
| (some true, none) => 4
| (some false, none) => 5
| (none, some true) => 6
| (none, some false) => 7
| (none, none) => 8;
test-sub-pattern = do {
Test_info "MACRO CASE" "sub pattern";
r0 <- Test_eq "f1" (f1 (cons (some true) nil) (cons (some true) nil)) 1;
r1 <- Test_eq "f1" (f1 (cons (some true) (cons (some true) nil))
(cons (some true) (cons (some true) nil))) 1;
r2 <- Test_eq "f1" (f1 nil nil) 1;
r3 <- Test_eq "f1" (f1 (cons (some true) (cons none nil)) (cons (some true) (cons none nil))) 2;
r4 <- Test_eq "f1" (f1 (cons (some false) nil) (cons (some false) nil)) 0;
r5 <- Test_eq "f1" (f1 (cons none nil) (cons (some true) nil)) 0;
r6 <- Test_eq "f1" (f1 (cons (some true) nil) (cons none nil)) 0;
r7 <- Test_eq "f1" (f1 (cons (none : Option Bool) nil) (cons (none : Option Bool) nil)) 2;
r8 <- Test_eq "f3" (f3 (some true) (some true)) 0;
r9 <- Test_eq "f3" (f3 (some false) (some true)) 1;
r10 <- Test_eq "f3" (f3 (some true) (some false)) 2;
r11 <- Test_eq "f3" (f3 (some false) (some false)) 3;
r12 <- Test_eq "f3" (f3 (some true) none) 4;
r13 <- Test_eq "f3" (f3 (some false) none) 5;
r14 <- Test_eq "f3" (f3 none (some true)) 6;
r15 <- Test_eq "f3" (f3 none (some false)) 7;
r16 <- Test_eq "f3" (f3 none none) 8;
part1 <- IO_return (and r0 (and r1 (and r2 (and r3 (and r4
(and r5 (and r6 r7)))))));
part2 <- IO_return (and r8 (and r9 (and r10 (and r11 (and r12
(and r13 (and r14 (and r15 r16))))))));
success <- IO_return (and part1 part2);
if success then
(Test_info "MACRO CASE" "test on sub pattern succeeded")
else
(Test_warning "MACRO CASE" "test on sub pattern failed");
IO_return success;
};
%% `cons x xs` vs `cons a as` and `cons y ys` vs `cons b bs`
f5 : List Bool -> List Bool -> Int;
f5 xs ys = let
count : Bool -> Bool -> Int;
count a b = case (a, b)
| (true,true) => 2
| (true,false) => 1
| (false,true) => 1
| (false,false) => 0;
in case (xs, ys)
| (cons x xs, nil) => (count x false) + (f5 xs nil)
| (nil, cons y ys) => (count false y) + (f5 nil ys)
| (cons a as, cons b bs) => (count a b) + (f5 as bs)
| (nil, nil) => 0;
test-var-name = do {
Test_info "MACRO CASE" "variable names";
r0 <- Test_eq "f5" (f5 (cons true nil) nil) 1;
r1 <- Test_eq "f5" (f5 nil (cons false nil)) 0;
r2 <- Test_eq "f5" (f5 (cons true nil) (cons true nil)) 2;
r3 <- Test_eq "f5" (f5 (cons false nil) (cons false nil)) 0;
r4 <- Test_eq "f5" (f5 (cons true nil) (cons false nil)) 1;
r5 <- Test_eq "f5" (f5 nil nil) 0;
r6 <- Test_eq "f5" (f5 (cons true (cons false nil)) (cons true (cons true nil))) 3;
success <- IO_return (and r0 (and r1 (and r2 (and r3 (and r4 (and r5 r6))))));
if success then
(Test_info "MACRO CASE" "test on variable names succeeded")
else
(Test_warning "MACRO CASE" "test on variable names failed");
IO_return success;
};
type AllImplicit
| ctor2 (a :: Int) (b :: Bool) (c :: Option Bool);
f6 : AllImplicit -> Bool;
f6 c = case c
| ctor2 (_ := va) (_ := vb) (_ := vc) => vb;
f7 : AllImplicit -> Bool;
f7 c = case c
| ctor2 (c := vc) (a := va) (b := vb) => vb;
test-named = do {
Test_info "MACRO CASE" "named argument";
r0 <- Test_false "default" (f6 (ctor2 (a := 0) (b := false) (c := none)));
r1 <- Test_true "default" (f6 (ctor2 (a := 0) (b := true) (c := none)));
r2 <- Test_false "order" (f7 (ctor2 (a := 0) (b := false) (c := none)));
r3 <- Test_true "order" (f7 (ctor2 (a := 0) (b := true) (c := none)));
success <- IO_return (and r0 (and r1 (and r2 r3)));
if success then
(Test_info "MACRO CASE" "test on named argument succeeded")
else
(Test_warning "MACRO CASE" "test on named argument failed");
IO_return success;
};
exec-test = do {
b1 <- test-one-var;
b2 <- test-dflt;
b3 <- test-list;
b4 <- test-color;
b5 <- test-sub-pattern;
b6 <- test-var-name;
b7 <- test-named;
IO_return (and b1 (and b2 (and b3 (and b4 (and b5 (and b6 b7))))));
};
samples/decltype.typer 0 → 100644
View file @ 2269559a
%%% decltype.typer --- Extract type of expression
%% Get type of expression:
%%
%% decl-type E
%%
%% returns the type of `E`.
decl-type = lambda (t : Type) => lambda (_ : t) -> t;
%%
%% It mostly work as exemples below work fine
%% but I can't do somethings like:
%% y = decl-type x;
%%
%%
%% Some tests and exemples
%%
int-var : Int;
int-var = 100;
%%
%% Error "Metavar in erase_type":
%% int = decl-type int-var;
%%
flt-var : Float;
flt-var = 0.1;
str-var : String;
str-var = "abc";
bool-var : Bool;
bool-var = true;
take-int : (decl-type int-var) -> (decl-type 1);
take-int n = n + n;
take-flt : (decl-type flt-var) -> (decl-type 1.0);
take-flt x = Float_+ x x;
take-str : (decl-type str-var) -> (decl-type "123");
take-str s = String_concat s s;
%%
%% Next are exemple where we really need
%% type annotation
%%
take-bool : (decl-type bool-var) -> (decl-type true);
take-bool b = case b
| true => false
| false => true;
rec-int : (decl-type int-var) -> (decl-type int-var);
rec-int n = if (Int_> n 0) then
(n + rec-int (n - 1))
else
(0);
samples/do_test.typer 0 → 100644
View file @ 2269559a
%%%%
%%%% Unit tests on macro `do`
%%%%
%% test for warning
test-hw = do
{
str <- IO_return "Hello, world!";
IO_return unit;
};
%% check IO_return value from do macro
test-return = do
{
n <- IO_return 123456789;
IO_return n;
};
%% check if any problem when using do as command inside another do
test-inside = do
{
x <- do { IO_return (Float_+ 16.0 0.125); };
str <- IO_return (Float->String x);
do { IO_return unit; };
do { do { IO_return unit; }; };
IO_return str;
};
%% declaring the type before assignement
%% this is an unexpected functionality that may be usefull
test-type = do
{
(t : Bool) <- IO_return true;
(f : Bool) <- IO_return false;
IO_return (if f then 333 else
(if t then 777 else 333));
};
exec-test = do {
Test_info "MACRO DO" "everything work or everything fail!";
test-hw;
v1 <- test-return;
v2 <- test-inside;
v3 <- test-type;
b1 <- Test_eq "return" v1 123456789;
b2 <- Test_eq "inside" v2 "16.125";
b3 <- Test_eq "type" v3 777;
success <- IO_return (and b1 (and b2 b3));
if success then
(Test_info "MACRO DO" "test on macro do succeeded")
else
(Test_warning "MACRO DO" "test on macro do failed");
IO_return success;
};
samples/elabctx_test.typer 0 → 100644
View file @ 2269559a
%%%%
%%%% Test of primitive related with Elab_Context
%%%%
test-isbound = do {
Test_info "ELABCTX" "isbound";
env <- Elab_getenv ();
r0 <- Test_true "Int" (Elab_isbound "Int" env);
r1 <- Test_true "List" (Elab_isbound "List" env);
r2 <- Test_true "Elab_isbound" (Elab_isbound "Elab_isbound" env);
r3 <- Test_true "do" (Elab_isbound "do" env);
r4 <- Test_true "cons" (Elab_isbound "cons" env);
r5 <- Test_true "nil" (Elab_isbound "nil" env);
r6 <- Test_true "true" (Elab_isbound "true" env);
r7 <- Test_true "false" (Elab_isbound "false" env);
r8 <- Test_true "none" (Elab_isbound "none" env);
r9 <- Test_false "randomunusednameabc123" (Elab_isbound "randomunusednameabc123" env);
r10 <- Test_false " " (Elab_isbound " " env);
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 "ELABCTX" "test on isbound succeeded")
else
(Test_warning "ELABCTX" "test on isbound failed");
IO_return success;
};
test-isconstructor = do {
Test_info "ELABCTX" "isconstructor";
env <- Elab_getenv ();
r0 <- Test_false "Int" (Elab_isconstructor "Int" env);
r1 <- Test_false "List" (Elab_isconstructor "List" env);
r2 <- Test_false "Elab_isconstructor" (Elab_isconstructor "Elab_isconstructor" env);
r3 <- Test_false "do" (Elab_isconstructor "do" env);
r4 <- Test_true "cons" (Elab_isconstructor "cons" env);
r5 <- Test_true "nil" (Elab_isconstructor "nil" env);
r6 <- Test_true "true" (Elab_isconstructor "true" env);
r7 <- Test_true "false" (Elab_isconstructor "false" env);
r8 <- Test_true "none" (Elab_isconstructor "none" env);
r9 <- Test_false "randomunusednameabc123" (Elab_isconstructor "randomunusednameabc123" env);
r10 <- Test_false " " (Elab_isconstructor " " env);
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 "ELABCTX" "test on isconstructor succeeded")
else
(Test_warning "ELABCTX" "test on isconstructor failed");
IO_return success;
};
test-is-nth-erasable = do {
Test_info "ELABCTX" "is-nth-erasable";
env <- Elab_getenv ();
r0 <- Test_true "ctor1 0" (Elab_is-nth-erasable "ctor1" 0 env);
r1 <- Test_true "ctor1 1" (Elab_is-nth-erasable "ctor1" 1 env);
r2 <- Test_true "ctor1 2" (Elab_is-nth-erasable "ctor1" 2 env);
r3 <- Test_false "ctor2 0" (Elab_is-nth-erasable "ctor2" 0 env);
r4 <- Test_false "ctor2 1" (Elab_is-nth-erasable "ctor2" 1 env);
r5 <- Test_false "ctor2 2" (Elab_is-nth-erasable "ctor2" 2 env);
r6 <- Test_false "ctor3 0" (Elab_is-nth-erasable "ctor3" 0 env);
r7 <- Test_false "ctor3 1" (Elab_is-nth-erasable "ctor3" 1 env);
r8 <- Test_false "ctor3 2" (Elab_is-nth-erasable "ctor3" 2 env);
r9 <- Test_true "ctor4 0" (Elab_is-nth-erasable "ctor4" 0 env);
r10 <- Test_false "ctor4 1" (Elab_is-nth-erasable "ctor4" 1 env);
r11 <- Test_false "ctor4 2" (Elab_is-nth-erasable "ctor4" 2 env);
success <- IO_return (and r0 (and r1 (and r2 (and r3 (and r4 (and r5
(and r6 (and r7 (and r8 (and r9 (and r10 r11)))))))))));
if success then
(Test_info "ELABCTX" "test on is-nth-erasable succeeded")
else
(Test_warning "ELABCTX" "test on is-nth-erasable failed");
IO_return success;
};
test-is-arg-erasable = do {
Test_info "ELABCTX" "is-arg-erasable";
env <- Elab_getenv ();
r0 <- Test_true "ctor1 0" (Elab_is-arg-erasable "ctor1" "a" env);
r1 <- Test_true "ctor1 1" (Elab_is-arg-erasable "ctor1" "b" env);
r2 <- Test_true "ctor1 2" (Elab_is-arg-erasable "ctor1" "c" env);
r3 <- Test_false "ctor2 0" (Elab_is-arg-erasable "ctor2" "a" env);
r4 <- Test_false "ctor2 1" (Elab_is-arg-erasable "ctor2" "b" env);
r5 <- Test_false "ctor2 2" (Elab_is-arg-erasable "ctor2" "c" env);
r6 <- Test_false "ctor3 0" (Elab_is-arg-erasable "ctor3" "a" env);
r7 <- Test_false "ctor3 1" (Elab_is-arg-erasable "ctor3" "b" env);
r8 <- Test_false "ctor3 2" (Elab_is-arg-erasable "ctor3" "c" env);
r9 <- Test_true "ctor4 0" (Elab_is-arg-erasable "ctor4" "a" env);
r10 <- Test_false "ctor4 1" (Elab_is-arg-erasable "ctor4" "b" env);
r11 <- Test_false "ctor4 2" (Elab_is-arg-erasable "ctor4" "c" env);
success <- IO_return (and r0 (and r1 (and r2 (and r3 (and r4 (and r5
(and r6 (and r7 (and r8 (and r9 (and r10 r11)))))))))));
if success then
(Test_info "ELABCTX" "test on is-arg-erasable succeeded")
else
(Test_warning "ELABCTX" "test on is-arg-erasable failed");
IO_return success;
};
test-nth-arg = do {
Test_info "ELABCTX" "nth-arg";
env <- Elab_getenv ();
r0 <- Test_eq "ctor4 0" (Elab_nth-arg "ctor4" 0 env) (some "a");
r1 <- Test_eq "ctor4 1" (Elab_nth-arg "ctor4" 1 env) (some "b");
r2 <- Test_eq "ctor4 2" (Elab_nth-arg "ctor4" 2 env) (some "c");
r0 <- Test_eq "ctor1 0" (Elab_nth-arg "ctor1" 0 env) (some "a");
r1 <- Test_eq "ctor1 1" (Elab_nth-arg "ctor1" 1 env) (some "b");
r2 <- Test_eq "ctor1 2" (Elab_nth-arg "ctor1" 2 env) (some "c");
%% argument without name
r3 <- Test_eq "cons 0" (Elab_nth-arg "cons" 0 env) none;
r4 <- Test_eq "cons 1" (Elab_nth-arg "cons" 1 env) none;
%% no argument
r5 <- Test_eq "nil 0" (Elab_nth-arg "nil" 0 env) none;
success <- IO_return (and r0 (and r1 (and r2 (and r3 (and r4 r5)))));
if success then
(Test_info "ELABCTX" "test on nth-arg succeeded")
else
(Test_info "ELABCTX" "test on nth-arg failed");
IO_return success;
};
test-arg-pos = do {
Test_info "ELABCTX" "arg-pos";
env <- Elab_getenv ();
r0 <- Test_eq "ctor4 a" (Elab_arg-pos "ctor4" "a" env) (some 0);
r1 <- Test_eq "ctor4 b" (Elab_arg-pos "ctor4" "b" env) (some 1);
r2 <- Test_eq "ctor4 c" (Elab_arg-pos "ctor4" "c" env) (some 2);
r0 <- Test_eq "ctor1 a" (Elab_arg-pos "ctor1" "a" env) (some 0);
r1 <- Test_eq "ctor1 b" (Elab_arg-pos "ctor1" "b" env) (some 1);
r2 <- Test_eq "ctor1 c" (Elab_arg-pos "ctor1" "c" env) (some 2);
%% argument without name
r3 <- Test_eq "cons foo" (Elab_arg-pos "cons" "foo" env) none;
r4 <- Test_eq "cons bar" (Elab_arg-pos "cons" "bar" env) none;
%% no argument
r5 <- Test_eq "nil bidon" (Elab_arg-pos "nil" "bidon" env) none;
success <- IO_return (and r0 (and r1 (and r2 (and r3 (and r4 r5)))));
if success then
(Test_info "ELABCTX" "test on arg-pos succeeded")
else
(Test_info "ELABCTX" "test on arg-pos failed");
IO_return success;
};
exec-test = do {
b1 <- test-isbound;
b2 <- test-isconstructor;
b3 <- test-is-nth-erasable;
b4 <- test-is-arg-erasable;
b5 <- test-nth-arg;
b6 <- test-arg-pos;
IO_return (and b1 (and b2 (and b3 (and b4 (and b5 b6)))));
};