.gitignore

-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

@@ -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

@@ -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/do.typer

+%%% 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

+%%% 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

@@ -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.
@@ -295,18 +356,12 @@ type-impl = lambda (x : List Sexp) ->
               in for-each ctor (Sexp_node (Sexp_symbol "_;_") nil)
 
                             %% return decls
-  in IO_return (chain-decl decl    % inductive type declaration
+  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

+%%% 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

+%%% 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

+%%% 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

+%%%%
+%%%% 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

+%%%%
+%%%% 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_test.typer

+%%%%
+%%%% 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

+%%% 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

+%%%%
+%%%% 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

+%%% 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

+%%%%
+%%%% 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

+%%%%
+%%%% 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)))));
+};