Jonathan Graveline pushed to branch graveline at Stefan / Typer

Commits: a8b733a6 by Jonathan Graveline at 2018-08-13T17:05:25Z Macro `Test_file` now return a command: `exec-test` from loaded file

File samples/batch_test.typer now working

Most unit test in Typer adapted for `Test_file` and batch_test.typer

- - - - - c11bb8a4 by Jonathan Graveline at 2018-08-13T20:52:32Z New complementary primitive: `Elab_arg-pos`

Improved macro `case` on explicit field pattern

- - - - -

12 changed files:

- btl/builtins.typer - btl/case.typer - btl/pervasive.typer - samples/array_test.typer - samples/batch_test.typer - samples/case_test.typer - samples/do_test.typer - samples/elabctx_test.typer - samples/polyfun_test.typer - samples/tuple_test.typer - src/elab.ml - src/eval.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -272,7 +272,9 @@ Elab_is-nth-erasable = Built-in "Elab.is-nth-erasable" : String -> Int -> Elab_C

Elab_is-arg-erasable = Built-in "Elab.is-arg-erasable" : String -> String -> Elab_Context -> Bool;

-Elab_nth-arg = Built-in "Elab.nth-arg" : String -> Int -> Elab_Context -> String; +Elab_nth-arg' = Built-in "Elab.nth-arg" : String -> Int -> Elab_Context -> String; + +Elab_arg-pos' = Built-in "Elab.arg-pos" : String -> String -> Elab_Context -> Int;

%%%% Unit test helper IO

===================================== btl/case.typer ===================================== @@ -185,6 +185,31 @@ kinds pat = let (lambda _ -> (nil : List Sexp)) xserr xserr xserr xserr;

+ str_of_sym : Sexp -> String; + str_of_sym arg = Sexp_dispatch arg + (lambda _ _ -> "< error >") + (lambda s -> s) + (lambda _ -> "< error >") + (lambda _ -> "< error >") + (lambda _ -> "< error >") + (lambda _ -> "< error >"); + + mf : Elab_Context -> Sexp -> Int -> Bool; + mf env arg i = Sexp_dispatch arg + (lambda s ss -> if (Sexp_eq s (Sexp_symbol "_:=_")) then + ( if (Sexp_eq (List_nth 0 ss Sexp_error) dflt-var) then + (Elab_is-nth-erasable ctor i env) + else + (Elab_is-arg-erasable ctor (str_of_sym (List_nth 0 ss Sexp_error)) env) ) + else + (false)) + (lambda _ -> false) + (lambda _ -> false) + (lambda _ -> false) + (lambda _ -> false) + (lambda _ -> false); + + %% %% What to do if argument are named (`(arg-name := x)`)? %% And if some are named and other not (`(_ := x)`) in a random order? @@ -192,7 +217,7 @@ kinds pat = let ks : IO (List Bool); ks = do { env <- Elab_getenv (); - IO_return (List_mapi (lambda _ i -> Elab_is-nth-erasable ctor i env) args); + IO_return (List_mapi (mf env) args); };

in ks;

===================================== btl/pervasive.typer ===================================== @@ -522,6 +522,20 @@ test4 : Option Int; test4 = test1 : Option ?; test3 = test4;

+%%%% Rewrite of some builtins to use `Option` + +Elab_nth-arg a b c = let + r = Elab_nth-arg' a b c; +in case (String_eq r "_") + | true => (none) + | false => (some r); + +Elab_arg-pos a b c = let + r = Elab_arg-pos' a b c; +in case (Int_eq r (-1)) + | true => (none) + | false => (some r); + %%%% `<-` operator used in macro `do` and for tuple assignment

define-operator "<-" 80 96; @@ -577,7 +591,7 @@ Test_file = macro (lambda args -> let in IO_return (Sexp_dispatch (List_nth 0 args Sexp_error) (lambda _ _ -> ret) (lambda _ -> ret) - (lambda s -> quote (let _ = load_ (uquote (Sexp_string s)); in (uquote ret))) + (lambda s -> quote (let lib = load_ (uquote (Sexp_string s)); in lib.exec-test)) (lambda _ -> ret) (lambda _ -> ret) (lambda _ -> ret))

===================================== samples/array_test.typer ===================================== @@ -42,10 +42,14 @@ test-length = do { r4 <- Test_eq "a3" (len a3) 7; r5 <- Test_eq "a4" (len a4) 7;

- if (and r0 (and r1 (and r2 (and r3 (and r4 r5))))) then + 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 { @@ -57,10 +61,14 @@ test-get = do { r3 <- Test_eq "a4" (get 3 a4) 3; r4 <- Test_eq "out of bounds" (get 10 a4) (-1);

- if (and r0 (and r1 (and r2 (and r3 r4)))) then + 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 { @@ -73,12 +81,20 @@ test-from-list = do { r4 <- Test_eq "from-list 2" (get 2 from-list) 2; r5 <- Test_eq "out of bounds" (get 3 from-list) (-1);

- if (and r0 (and r1 (and r2 (and r3 (and r4 r5))))) then + 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; };

-u = (IO_run test-length) (); -u = (IO_run test-get) (); -u = (IO_run test-from-list) (); +exec-test = do { + b1 <- test-length; + b2 <- test-get; + b3 <- test-from-list; + + IO_return (and b1 (and b2 b3)); +};

===================================== samples/batch_test.typer ===================================== @@ -2,15 +2,58 @@ %%%% File for testing mutiple unit tests file written in Typer %%%%

-%% Not currently working, lots of error -%% but individual test pass if executed alone +%% +%% 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";

-u3 = Test_file "./samples/do_test.typer"; +u2 = Test_file "./samples/elabctx_test.typer"; + +u3 = Test_file "./samples/case_test.typer"; + +u4 = Test_file "./samples/polyfun_test.typer";

-u5 = Test_file "./samples/elabctx_test.typer"; +u5 = Test_file "./samples/tuple_test.typer";

-u7 = Test_file "./samples/polyfun_test.typer"; +u6 = Test_file "./samples/do_test.typer";

-u9 = Test_file "./samples/tuple_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\tlast file\n"; + b6 <- u6; + Test_info "BATCH TESTS" "\n\n\tdone\n"; + + success <- IO_return (and b1 (and b2 (and b3 (and b4 (and b5 b6))))); + + if success then + (Test_info "BATCH TESTS" "all tests succeeded") + else + (Test_warning "BATCH TESTS" "some tests failed"); +};

===================================== samples/case_test.typer ===================================== @@ -23,10 +23,14 @@ test-one-var = do { r3 <- Test_eq "last" (last (cons 1 nil)) (some 1); r4 <- Test_eq "last" (last (cons 1 (cons 2 nil))) (some 2);

- if (and r0 (and r1 (and r2 (and r3 r4)))) then + 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; @@ -84,10 +88,14 @@ test-dflt = do {

part3 <- IO_return (and r16 (and r17 (and r18 r19)));

- if (and part1 (and part2 part3)) then + success <- IO_return (and part1 (and part2 part3)); + + 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; @@ -112,10 +120,14 @@ test-list = do { 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);

- if (and r0 (and r1 (and r2 (and r3 (and r4 r5))))) then + 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 @@ -205,10 +217,14 @@ test-color = do { part2 <- IO_return (and r9 (and r10 (and r11 (and r12 (and r13 (and r14 (and r15 (and r16 r17))))))));

- if (and part1 part2) then + 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; @@ -259,10 +275,14 @@ test-sub-pattern = do { part2 <- IO_return (and r8 (and r9 (and r10 (and r11 (and r12 (and r13 (and r14 (and r15 r16))))))));

- if (and part1 part2) then + 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` @@ -294,20 +314,53 @@ test-var-name = do { r5 <- Test_eq "f5" (f5 nil nil) 0; r6 <- Test_eq "f5" (f5 (cons true (cons false nil)) (cons true (cons true nil))) 3;

- if (and r0 (and r1 (and r2 (and r3 (and r4 (and r5 r6)))))) then + 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; };

-u = (IO_run test-one-var) (); - -u = (IO_run test-dflt) (); +type AllImplicit + | ctor2 (a :: Int) (b :: Bool) (c :: Option Bool);

-u = (IO_run test-list) (); +f6 : AllImplicit -> Bool; +f6 c = case c + | ctor2 (_ := va) (_ := vb) (_ := vc) => vb;

-u = (IO_run test-color) (); +f7 : AllImplicit -> Bool; +f7 c = case c + | ctor2 (c := vc) (a := va) (b := vb) => vb;

-u = (IO_run test-sub-pattern) (); +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; +};

-u = (IO_run test-var-name) (); +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/do_test.typer ===================================== @@ -2,52 +2,37 @@ %%%% Unit tests on macro `do` %%%%

-%% -%% This one is particular since we can't use -%% the macro we test for doing tests -%% - -return = IO_return; - -nop = (lambda _ -> return ()); - %% test for warning

test-hw = do { - str <- return "Hello, world!"; + str <- IO_return "Hello, world!";

- nop str; + IO_return unit; };

-%% check return value from do macro +%% check IO_return value from do macro

test-return = do { - nop "Doing random stuff before returning..."; - - n <- return 123456789; + n <- IO_return 123456789;

- return n; + IO_return n; };

%% check if any problem when using do as command inside another do

test-inside = do { - x <- do { return (Float_+ 16.0 0.125); }; + x <- do { IO_return (Float_+ 16.0 0.125); };

- nop "Doing random stuff..."; + str <- IO_return (Float->String x);

- str <- return (Float->String x); + do { IO_return unit; };

- val123 <- test-return; + do { do { IO_return unit; }; };

- do { nop str; }; - - do { do { nop str; }; }; - - return str; + IO_return str; };

%% declaring the type before assignement @@ -55,27 +40,33 @@ test-inside = do

test-type = do { - (t : Bool) <- return true; + (t : Bool) <- IO_return true;

- (f : Bool) <- return false; + (f : Bool) <- IO_return false;

- return (if f then 333 else + IO_return (if f then 333 else (if t then 777 else 333)); };

-test : String -> String -> IO Bool -> IO Unit; -test msg-success msg-fail x = IO_bind x (lambda (x : Bool) -> (if x then - (Test_info "DO MACRO" msg-success) - else - (Test_warning "DO MACRO" msg-fail))); +exec-test = do { + Test_info "MACRO DO" "everything work or everything fail!";

-u = (IO_run test-hw) (); -u = (IO_run (test "test on return succeeded" "test on return failed" - (IO_bind (IO_bind test-return (lambda x -> return x)) - (lambda x -> (Test_eq "return" x (123456789)))))) (); -u = (IO_run (test "test on do inside do succeeded" "test on do inside do failed" - (IO_bind (IO_bind test-inside (lambda x -> return x)) - (lambda x -> (Test_eq "inside" x ("16.125")))))) (); -u = (IO_run (test "test on type succeeded" "test on type failed" - (IO_bind (IO_bind test-type (lambda x -> return x)) - (lambda x -> (Test_eq "type" x (777)))))) (); + 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 ===================================== @@ -19,11 +19,15 @@ test-isbound = do { r9 <- Test_false "randomunusednameabc123" (Elab_isbound "randomunusednameabc123" env); r10 <- Test_false " " (Elab_isbound " " env);

- if (and r0 (and r1 (and r2 (and r3 (and r4 (and r5 - (and r6 (and r7 (and r8 (and r9 r10)))))))))) then + 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 { @@ -43,25 +47,17 @@ test-isconstructor = do { r9 <- Test_false "randomunusednameabc123" (Elab_isconstructor "randomunusednameabc123" env); r10 <- Test_false " " (Elab_isconstructor " " env);

- if (and r0 (and r1 (and r2 (and r3 (and r4 (and r5 - (and r6 (and r7 (and r8 (and r9 r10)))))))))) then + 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; };

-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); - test-is-nth-erasable = do { Test_info "ELABCTX" "is-nth-erasable";

@@ -83,11 +79,15 @@ test-is-nth-erasable = do { r10 <- Test_false "ctor4 1" (Elab_is-nth-erasable "ctor4" 1 env); r11 <- Test_false "ctor4 2" (Elab_is-nth-erasable "ctor4" 2 env);

- if (and r0 (and r1 (and r2 (and r3 (and r4 (and r5 - (and r6 (and r7 (and r8 (and r9 (and r10 r11))))))))))) then + 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 { @@ -111,11 +111,15 @@ test-is-arg-erasable = do { r10 <- Test_false "ctor4 1" (Elab_is-arg-erasable "ctor4" "b" env); r11 <- Test_false "ctor4 2" (Elab_is-arg-erasable "ctor4" "c" env);

- if (and r0 (and r1 (and r2 (and r3 (and r4 (and r5 - (and r6 (and r7 (and r8 (and r9 (and r10 r11))))))))))) then + 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 { @@ -123,29 +127,68 @@ test-nth-arg = do {

env <- Elab_getenv ();

- r0 <- Test_eq "ctor4 0" (Elab_nth-arg "ctor4" 0 env) "a"; - r1 <- Test_eq "ctor4 1" (Elab_nth-arg "ctor4" 1 env) "b"; - r2 <- Test_eq "ctor4 2" (Elab_nth-arg "ctor4" 2 env) "c"; + 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) "a"; - r1 <- Test_eq "ctor1 1" (Elab_nth-arg "ctor1" 1 env) "b"; - r2 <- Test_eq "ctor1 2" (Elab_nth-arg "ctor1" 2 env) "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) "_"; - r4 <- Test_eq "cons 1" (Elab_nth-arg "cons" 1 env) "_"; + 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) "_"; + r5 <- Test_eq "nil 0" (Elab_nth-arg "nil" 0 env) none;

- if (and r0 (and r1 (and r2 (and r3 (and r4 r5))))) then + 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; };

-u = (IO_run test-isbound) (); -u = (IO_run test-isconstructor) (); -u = (IO_run test-is-nth-erasable) (); -u = (IO_run test-is-arg-erasable) (); -u = (IO_run test-nth-arg) (); +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))))); +};

===================================== samples/polyfun_test.typer ===================================== @@ -28,10 +28,14 @@ test-and = do { r2 <- Test_false "my-and true false" (my-and true false); r3 <- Test_false "my-and false true" (my-and false true);

- if (and r0 (and r1 (and r2 r3))) then + success <- IO_return (and r0 (and r1 (and r2 r3))); + + if success then (Test_info "POLYFUN" "test on my-and succeeded") else (Test_warning "POLYFUN" "test on my-and failed"); + + IO_return success; };

test-or = do { @@ -42,10 +46,14 @@ test-or = do { r2 <- Test_true "my-or true false" (my-or true false); r3 <- Test_true "my-or false true" (my-or false true);

- if (and r0 (and r1 (and r2 r3))) then + success <- IO_return (and r0 (and r1 (and r2 r3))); + + if success then (Test_info "POLYFUN" "test on my-or succeeded") else (Test_warning "POLYFUN" "test on my-or failed"); + + IO_return success; };

test-not = do { @@ -55,10 +63,14 @@ test-not = do { r1 <- Test_eq "my-not (some false)" (my-not (some false)) (some true); r2 <- Test_eq "my-not none" (my-not none) (some false);

- if (and r0 (and r1 r2)) then + success <- IO_return (and r0 (and r1 r2)); + + if success then (Test_info "POLYFUN" "test on my-not succeeded") else (Test_info "POLYFUN" "test on my-not failed"); + + IO_return success; };

test-rec = do { @@ -72,13 +84,21 @@ test-rec = do { (my-merge (cons 0 (cons 1 nil)) (cons 1 (cons 0 nil))) (cons (pair 0 1) (cons (pair 1 0) nil));

- if (and r0 (and r1 (and r2 r3))) then + success <- IO_return (and r0 (and r1 (and r2 r3))); + + if success then (Test_info "POLYFUN" "test on my-merge succeeded") else (Test_info "POLYFUN" "test on my-merge failed"); + + IO_return success; };

-u = (IO_run test-and) (); -u = (IO_run test-or) (); -u = (IO_run test-not) (); -u = (IO_run test-rec) (); +exec-test = do { + b1 <- test-and; + b2 <- test-or; + b3 <- test-not; + b4 <- test-rec; + + IO_return (and b1 (and b2 (and b3 b4))); +};

===================================== samples/tuple_test.typer ===================================== @@ -24,10 +24,14 @@ test-int = do { r3 <- Test_eq "d = 3" d 3; r4 <- Test_eq "e = 4" e 4;

- if (and r0 (and r1 (and r2 (and r3 r4)))) then + success <- IO_return (and r0 (and r1 (and r2 (and r3 r4)))); + + if success then (Test_info "TUPLE" "test on Int succeeded") else (Test_warning "TUPLE" "test on Int failed"); + + IO_return success; };

test-datatype = do { @@ -38,10 +42,14 @@ test-datatype = do { r2 <- Test_eq "h = (some true)" h (some true); r3 <- Test_eq "i = (some false)" i (some false);

- if (and r0 (and r1 (and r2 r3))) then + success <- IO_return (and r0 (and r1 (and r2 r3))); + + if success then (Test_info "TUPLE" "test on datatype succeeded") else (Test_warning "TUPLE" "test on datatype failed"); + + IO_return success; };

test-tuple = do { @@ -62,12 +70,20 @@ test-tuple = do { %% But those value are tested within `r0` to `r3` %%

- if (and r0 (and r1 (and r2 r3))) then + success <- IO_return (and r0 (and r1 (and r2 r3))); + + if success then (Test_info "TUPLE" "test on tuple succeeded") else (Test_warning "TUPLE" "test on tuple failed"); + + IO_return success; };

-u = (IO_run test-int) (); -u = (IO_run test-datatype) (); -u = (IO_run test-tuple) (); +exec-test = do { + b1 <- test-int; + b2 <- test-datatype; + b3 <- test-tuple; + + IO_return (and b1 (and b2 b3)); +};

===================================== src/elab.ml ===================================== @@ -1645,7 +1645,7 @@ let dynamic_bind r v body =

(* Make lxp context with built-in types *) let default_ectx - = let _ = register_special_forms () in + = try let _ = register_special_forms () in

(* Read BTL files *) let read_file file_name elctx = @@ -1691,6 +1691,7 @@ let default_ectx let _ = _in_pervasive := false in let _ = _set_default_ectx lctx in lctx + with (Stop_Compilation _) -> fatal dloc "compilation stopped in default context"

let default_rctx = let rctx = EV.from_ectx default_ectx in

===================================== src/eval.ml ===================================== @@ -768,8 +768,7 @@ let erasable_p name nth ectx = | (Some args) -> if (nth < (List.length args) && nth >= 0) then ( match (List.nth args nth) with - | (k, _, _) -> k = Aerasable - | _ -> false ) + | (k, _, _) -> k = Aerasable ) else false | _ -> false in try let idx = senv_lookup name ectx in @@ -803,7 +802,7 @@ let erasable_p2 t name ectx = with Senv_Lookup_Fail _ -> false

let nth_ctor_arg name nth ectx = - let is_erasable ctors = match (SMap.find_opt name ctors) with + let find_nth ctors = match (SMap.find_opt name ctors) with | (Some args) -> ( match (List.nth_opt args nth) with | Some (_, (_, Some n), _) -> n @@ -814,11 +813,32 @@ let nth_ctor_arg name nth ectx = (ectx_to_lctx ectx) with | Cons (Var v, _) -> ( match (env_lookup_expr ectx v) with | Some (Inductive (_, _, _, ctors)) -> - is_erasable ctors + find_nth ctors | _ -> "_" ) | _ -> "_" with Senv_Lookup_Fail _ -> "_"

+let ctor_arg_pos name arg ectx = + let rec find_opt xs n = match xs with + | [] -> None + | (_, (_, Some x), _)::xs -> if x = arg then Some n else find_opt xs (n + 1) + | _::xs -> find_opt xs (n + 1) in + let find_arg ctors = match (SMap.find_opt name ctors) with + | (Some args) -> + ( match (find_opt args 0) with + | None -> (-1) + | Some n -> n ) + | _ -> (-1) in + try let idx = senv_lookup name ectx in + match OL.lexp_whnf (mkVar ((dummy_location, Some name), idx)) + (ectx_to_lctx ectx) with + | Cons (Var v, _) -> ( match (env_lookup_expr ectx v) with + | Some (Inductive (_, _, _, ctors)) -> + find_arg ctors + | _ -> (-1) ) + | _ -> (-1) + with Senv_Lookup_Fail _ -> (-1) + let is_constructor loc depth args_val = match args_val with | [Vstring name; Velabctx ectx] -> o2v_bool (constructor_p name ectx) | _ -> error loc "Elab.isconstructor takes a String and an Elab_Context as arguments" @@ -833,7 +853,11 @@ let is_arg_erasable loc depth args_val = match args_val with

let nth_arg loc depth args_val = match args_val with | [Vstring t; Vint nth; Velabctx ectx] -> Vstring (nth_ctor_arg t nth ectx) - | _ -> error loc "Elab.nth-arg takes an Int and an Elab_Context as arguments" + | _ -> error loc "Elab.nth-arg takes a String, an Int and an Elab_Context as arguments" + +let arg_pos loc depth args_val = match args_val with + | [Vstring t; Vstring a; Velabctx ectx] -> Vint (ctor_arg_pos t a ectx) + | _ -> error loc "Elab.arg-pos takes two String and an Elab_Context as arguments"

let array_append loc depth args_val = match args_val with | [v; Varray a] -> @@ -975,6 +999,7 @@ let register_builtin_functions () = ("Elab.is-nth-erasable", is_nth_erasable, 3); ("Elab.is-arg-erasable", is_arg_erasable, 3); ("Elab.nth-arg" , nth_arg, 3); + ("Elab.arg-pos" , arg_pos, 3); ("Array.append" , array_append,2); ("Array.create" , array_create,2); ("Array.length" , array_length,1);

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