Jonathan Graveline pushed to branch graveline at Stefan / Typer

Commits: 3d4035ac by Jonathan Graveline at 2018-08-07T18:25:12Z Correction of bounds check in `array_get`

samples/array_test.typer: Unit test for `Array` rewritten in Typer

- - - - - f9d7cefc by Jonathan Graveline at 2018-08-09T17:30:04Z New primitive for inductive type info

Temporary fix of macro `case` to pass unit tests

Commented incorrect `Metavar` case in `conv_p`

- - - - - ab2c6d9b by Jonathan Graveline at 2018-08-10T16:59:38Z New macro `Test_file` not working on multiple call

Unit test rewritten in Typer for `case`, `do`, `Elab_Context`

Correction of primitive `Elab.is-arg-erasable`

- - - - -

15 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/list_n.typer - src/eval.ml - src/opslexp.ml - − tests/array_test.ml - − tests/case_test.ml - − tests/elabctx_test.ml - − tests/macro_do_test.ml

Changes:

===================================== btl/builtins.typer ===================================== @@ -268,6 +268,12 @@ Elab_isbound = Built-in "Elab.isbound" : String -> Elab_Context -> Bool; Elab_isconstructor = Built-in "Elab.isconstructor" : String -> Elab_Context -> Bool;

+Elab_is-nth-erasable = Built-in "Elab.is-nth-erasable" : String -> Int -> Elab_Context -> Bool; + +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; + %%%% Unit test helper IO

%% Print message and/or fail (terminate)

===================================== btl/case.typer ===================================== @@ -161,6 +161,42 @@ get-branches vars sexps = let

in helper sexps;

+kinds : Sexp -> IO (List Bool); +kinds pat = let + + serr = lambda _ -> Sexp_error; + + strerr = lambda _ -> "< error >"; + + xserr = lambda _ -> (nil : List Sexp); + + ctor : String; + ctor = let + ctor-name : Sexp -> String; + ctor-name pat = Sexp_dispatch pat + (lambda s ss -> ctor-name s) + (lambda s -> s) + strerr strerr strerr strerr; + in ctor-name pat; + + args : List Sexp; + args = Sexp_dispatch pat + (lambda s ss -> ss) + (lambda _ -> (nil : List Sexp)) + xserr xserr xserr xserr; + + %% + %% What to do if argument are named (`(arg-name := x)`)? + %% And if some are named and other not (`(_ := x)`) in a random order? + %% + ks : IO (List Bool); + ks = do { + env <- Elab_getenv (); + IO_return (List_mapi (lambda _ i -> Elab_is-nth-erasable ctor i env) args); + }; + +in ks; + %% %% Get constructor without any sub constructor and with variable renamed %% @@ -173,18 +209,26 @@ renamed-pat pat names = let

serr = lambda _ -> Sexp_error;

+ strerr = lambda _ -> "< error >"; + + xserr = lambda _ -> (nil : List Sexp); + tup : Bool; tup = is-tuple pat;

tuple-nth : Int -> Sexp; tuple-nth n = Sexp_symbol (String_concat "%" (Int->String n)); - - mf : Sexp -> Int -> Sexp; - mf v i = Sexp_dispatch v + + mf : List Bool -> Sexp -> Int -> Sexp; + mf kinds v i = Sexp_dispatch v (lambda sym ss -> if (Sexp_eq sym (Sexp_symbol "_:=_")) - then - (Sexp_node sym (cons (List_nth 0 ss Sexp_error) (cons (List_nth i names Sexp_error) nil))) + then if (List_nth i kinds false) then + %% if client use multiple name for the same erasable args, + %% I expect it to not compile... + (Sexp_node sym ss) + else + (Sexp_node sym (cons (List_nth 0 ss Sexp_error) (cons (List_nth i names Sexp_error) nil))) else if tup then %% tuples argument are all implicit so we must take special care of those (Sexp_node (Sexp_symbol "_:=_") @@ -197,11 +241,18 @@ renamed-pat pat names = let else (List_nth i names Sexp_error)) serr serr serr serr; + + ctor : Sexp -> String; + ctor pat = Sexp_dispatch pat + (lambda s _ -> ctor s) + (lambda s -> s) + strerr strerr strerr strerr;

in do { pat <- IO_return pat; + kinds <- kinds pat; IO_return (Sexp_dispatch pat - (lambda s ss -> Sexp_node s (List_mapi mf ss)) + (lambda s ss -> Sexp_node s (List_mapi (mf kinds) ss)) (lambda s -> Sexp_symbol s) serr serr serr serr); }; @@ -265,30 +316,54 @@ in Sexp_eq (ctor-of p0) (ctor-of p1); introduced-vars : Pat -> IO (List Var); introduced-vars pat = let

- serr = lambda _ -> IO_return nil; + serr = lambda _ -> IO_return (pair 0 nil); + + ks : IO (List Bool); + ks = kinds pat;

- ff : IO (List Sexp) -> Sexp -> IO (List Sexp); - ff o v = Sexp_dispatch v + ff : IO (Pair Int (List Sexp)) -> Sexp -> IO (Pair Int (List Sexp)); + ff p v = let + + o = do { + p <- p; + IO_return (case p | pair _ x => x); + }; + i = do { + p <- p; + IO_return (case p | pair x _ => x); + }; + + in Sexp_dispatch v (lambda s ss -> do { o <- o; % bind + i <- i; + ks <- ks; if (Sexp_eq s (Sexp_symbol "_:=_")) then - (IO_return (List_concat o (cons (List_nth 1 ss Var_error) nil))) + if (List_nth i ks false) then + (IO_return (pair (i + 1) (List_concat o (cons dflt-var nil)))) + else + (IO_return (pair (i + 1) (List_concat o (cons (List_nth 1 ss Var_error) nil)))) else - (IO_return (List_concat o (cons dflt-var nil))); + (IO_return (pair (i + 1) (List_concat o (cons dflt-var nil)))); }) (lambda s -> do { o <- o; % bind + i <- i; sym <- IO_return (Sexp_symbol s); b <- is-pat sym; if (b) then - (IO_return (List_concat o (cons dflt-var nil))) + (IO_return (pair (i + 1) (List_concat o (cons dflt-var nil)))) else - (IO_return (List_concat o (cons sym nil))); + (IO_return (pair (i + 1) (List_concat o (cons sym nil)))); }) serr serr serr serr;

in Sexp_dispatch pat - (lambda _ ss -> List_foldl ff (IO_return nil) ss) + (lambda _ ss -> do { + p <- (List_foldl ff (IO_return (pair 0 nil)) ss); + IO_return (case p + | pair _ xs => xs); + }) (lambda _ -> IO_return nil) % constructor as a unique symbol (as `true`) (lambda _ -> IO_return nil) (lambda _ -> IO_return nil) % error (lambda _ -> IO_return nil) (lambda _ -> IO_return nil); % error

===================================== btl/pervasive.typer ===================================== @@ -560,4 +560,27 @@ define-operator "plain-let" () 3;

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

+%%%% `case` at function level +_|_ = 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... + +Test_file = macro (lambda args -> let + + ret = Sexp_node + (Sexp_symbol "IO_return") + (cons (Sexp_symbol "unit") nil); + +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 _ -> ret) + (lambda _ -> ret) + (lambda _ -> ret)) +); + %%% pervasive.typer ends here.

===================================== samples/array_test.typer ===================================== @@ -0,0 +1,84 @@ +%%%% +%%%% 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; + + if (and r0 (and r1 (and r2 (and r3 (and r4 r5))))) then + (Test_info "ARRAY" "test on length succeeded") + else + (Test_warning "ARRAY" "test on length failed"); +}; + +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); + + if (and r0 (and r1 (and r2 (and r3 r4)))) then + (Test_info "ARRAY" "test on get succeeded") + else + (Test_warning "ARRAY" "test on get failed"); +}; + +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); + + if (and r0 (and r1 (and r2 (and r3 (and r4 r5))))) then + (Test_info "ARRAY" "test on List->Array succeeded") + else + (Test_warning "ARRAY" "test on List->Array failed"); +}; + +u = (IO_run test-length) (); +u = (IO_run test-get) (); +u = (IO_run test-from-list) ();

===================================== samples/batch_test.typer ===================================== @@ -0,0 +1,16 @@ +%%%% +%%%% File for testing mutiple unit tests file written in Typer +%%%% + +%% Not currently working, lots of error +%% but individual test pass if executed alone + +u1 = Test_file "./samples/array_test.typer"; + +u3 = Test_file "./samples/do_test.typer"; + +u5 = Test_file "./samples/elabctx_test.typer"; + +u7 = Test_file "./samples/polyfun_test.typer"; + +u9 = Test_file "./samples/tuple_test.typer";

===================================== samples/case_test.typer ===================================== @@ -0,0 +1,313 @@ +%%%% +%%%% 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); + + if (and r0 (and r1 (and r2 (and r3 r4)))) then + (Test_info "MACRO CASE" "test on one variable succeeded") + else + (Test_warning "MACRO CASE" "test on one variable failed"); +}; + +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; + +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); + + 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))); + + if (and part1 (and part2 part3)) then + (Test_info "MACRO CASE" "test on default succeeded") + else + (Test_warning "MACRO CASE" "test on default failed"); +}; + +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); + + if (and r0 (and r1 (and r2 (and r3 (and r4 r5))))) then + (Test_info "MACRO CASE" "test on list succeeded") + else + (Test_warning "MACRO CASE" "test on list failed"); +}; + +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)))))))); + + if (and part1 part2) then + (Test_info "MACRO CASE" "test on color succeeded") + else + (Test_warning "MACRO CASE" "test on color failed"); +}; + +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)))))))); + + if (and part1 part2) then + (Test_info "MACRO CASE" "test on sub pattern succeeded") + else + (Test_warning "MACRO CASE" "test on sub pattern failed"); +}; + +%% `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; + + if (and r0 (and r1 (and r2 (and r3 (and r4 (and r5 r6)))))) then + (Test_info "MACRO CASE" "test on variable names succeeded") + else + (Test_warning "MACRO CASE" "test on variable names failed"); +}; + +u = (IO_run test-one-var) (); + +u = (IO_run test-dflt) (); + +u = (IO_run test-list) (); + +u = (IO_run test-color) (); + +u = (IO_run test-sub-pattern) (); + +u = (IO_run test-var-name) ();

===================================== samples/do_test.typer ===================================== @@ -0,0 +1,81 @@ +%%%% +%%%% 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!"; + + nop str; +}; + +%% check return value from do macro + +test-return = do +{ + nop "Doing random stuff before returning..."; + + n <- return 123456789; + + 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); }; + + nop "Doing random stuff..."; + + str <- return (Float->String x); + + val123 <- test-return; + + do { nop str; }; + + do { do { nop str; }; }; + + return str; +}; + +%% declaring the type before assignement +%% this is an unexpected functionality that may be usefull + +test-type = do +{ + (t : Bool) <- return true; + + (f : Bool) <- return false; + + 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))); + +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)))))) ();

===================================== samples/elabctx_test.typer ===================================== @@ -0,0 +1,151 @@ +%%%% +%%%% 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); + + if (and r0 (and r1 (and r2 (and r3 (and r4 (and r5 + (and r6 (and r7 (and r8 (and r9 r10)))))))))) then + (Test_info "ELABCTX" "test on isbound succeeded") + else + (Test_warning "ELABCTX" "test on isbound failed"); +}; + +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); + + if (and r0 (and r1 (and r2 (and r3 (and r4 (and r5 + (and r6 (and r7 (and r8 (and r9 r10)))))))))) then + (Test_info "ELABCTX" "test on isconstructor succeeded") + else + (Test_warning "ELABCTX" "test on isconstructor failed"); +}; + +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"; + + 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); + + 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 + (Test_info "ELABCTX" "test on is-nth-erasable succeeded") + else + (Test_warning "ELABCTX" "test on is-nth-erasable failed"); +}; + +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); + + 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 + (Test_info "ELABCTX" "test on is-arg-erasable succeeded") + else + (Test_warning "ELABCTX" "test on is-arg-erasable failed"); +}; + +test-nth-arg = do { + Test_info "ELABCTX" "nth-arg"; + + 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 "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"; + + %% 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) "_"; + + %% no argument + r5 <- Test_eq "nil 0" (Elab_nth-arg "nil" 0 env) "_"; + + if (and r0 (and r1 (and r2 (and r3 (and r4 r5))))) then + (Test_info "ELABCTX" "test on nth-arg succeeded") + else + (Test_info "ELABCTX" "test on nth-arg failed"); +}; + +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) ();

===================================== samples/list_n.typer ===================================== @@ -11,27 +11,21 @@ type Nat Nat_add : Nat -> Nat -> Nat;

Nat_add n k = case n - | (succ n) => Nat_add n (succ k) + | (succ n) => succ (Nat_add n k) | zero => k;

-Nat_eq : Nat -> Nat -> Type; -Nat_eq n k = case (n,k) - | (succ n,succ k) => Nat_eq n k - | (zero,zero) => True - | False; - one = succ zero;

-List_n : Nat -> Type -> Type; +Listn : Nat -> Type -> Type;

-type List_n (n : Nat) (a : Type) - | cons a (List_n sn a) (p ::: (Nat_eq n (succ sn))) - | nil (p ::: (Nat_eq n zero)); +type Listn (n : Nat) (a : Type) + | cons (sn ::: Nat) a (Listn sn a) (p ::: (Eq_refl n (succ sn))) + | nil (p ::: (Eq_refl n zero));

-len : (n : Nat) ≡> (a : Type) ≡> List_n n a -> Nat; +len : (n : Nat) ≡> (a : Type) ≡> Listn n a -> Nat; len xs = case (xs) | cons x xs => succ (len xs) | nil => zero;

-%prep : (n : Nat) ≡> a -> List_n n a -> List_n (succ n) a; -%prep x xs = cons (n := (succ n)) x xs (Nat_eq (succ n) (succ n)); +preppend : (n : Nat) ≡> a -> Listn n a -> Listn (succ n) a; +preppend x xs = cons (sn := (succ n)) x xs (Eq_refl sn (succ n));

===================================== src/eval.ml ===================================== @@ -763,9 +763,77 @@ let constructor_p name ectx = | _ -> false with Senv_Lookup_Fail _ -> false

+let erasable_p name nth ectx = + let is_erasable ctors = match (SMap.find_opt name ctors) with + | (Some args) -> + if (nth < (List.length args) && nth >= 0) then + ( match (List.nth args nth) with + | (k, _, _) -> k = Aerasable + | _ -> false ) + else false + | _ -> false 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)) -> + is_erasable ctors + | _ -> false ) + | _ -> false + with Senv_Lookup_Fail _ -> false + +let erasable_p2 t name ectx = + let is_erasable ctors = match (SMap.find_opt t ctors) with + | (Some args) -> + ( match (List.find_opt (fun (k, oname, _) -> + match oname with + | (_, Some n) -> (n = name && k = Aerasable) + | _ -> false) args) with + | Some _ -> true + | _ -> false ) + | _ -> false in + try let idx = senv_lookup t ectx in + match OL.lexp_whnf (mkVar ((dummy_location, Some t), idx)) + (ectx_to_lctx ectx) with + | Cons (Var v, _) -> ( match (env_lookup_expr ectx v) with + | Some (Inductive (_, _, _, ctors)) -> + is_erasable ctors + | _ -> false ) + | _ -> false + with Senv_Lookup_Fail _ -> false + +let nth_ctor_arg name nth ectx = + let is_erasable ctors = match (SMap.find_opt name ctors) with + | (Some args) -> + ( match (List.nth_opt args nth) with + | Some (_, (_, Some n), _) -> n + | _ -> "_" ) + | _ -> "_" 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)) -> + is_erasable ctors + | _ -> "_" ) + | _ -> "_" + with Senv_Lookup_Fail _ -> "_" + 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 an Elab_Context and a String as arguments" + | _ -> error loc "Elab.isconstructor takes a String and an Elab_Context as arguments" + +let is_nth_erasable loc depth args_val = match args_val with + | [Vstring name; Vint nth_arg; Velabctx ectx] -> o2v_bool (erasable_p name nth_arg ectx) + | _ -> error loc "Elab.is-nth-erasable takes a String, an Int and an Elab_Context as arguments" + +let is_arg_erasable loc depth args_val = match args_val with + | [Vstring t; Vstring arg; Velabctx ectx] -> o2v_bool (erasable_p2 t arg ectx) + | _ -> error loc "Elab.is-arg-erasable takes two String and an Elab_Context as arguments" + +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"

let array_append loc depth args_val = match args_val with | [v; Varray a] -> @@ -791,7 +859,7 @@ let array_set loc depth args_val = match args_val with | _ -> error loc "Array.set takes an Int, a value and an Array as arguments"

let array_get loc depth args_val = match args_val with - | [dflt; Vint idx; Varray a] -> if (idx > (Array.length a)) || (idx < 0) + | [dflt; Vint idx; Varray a] -> if (idx >= (Array.length a)) || (idx < 0) then dflt else @@ -808,8 +876,7 @@ let array_empty loc depth args_val = match args_val with

let test_fatal loc depth args_val = match args_val with | [Vstring section; Vstring msg] -> - Vcommand (fun () -> Util.msg_user_fatal section loc msg; - tunit) + Vcommand (fun () -> Util.msg_user_fatal section loc msg) | _ -> error loc "Test.fatal takes two String as argument"

let test_warning loc depth args_val = match args_val with @@ -905,6 +972,9 @@ let register_builtin_functions () = ("Elab.getenv" , getenv, 1); ("Elab.isbound" , is_bound, 2); ("Elab.isconstructor", is_constructor, 2); + ("Elab.is-nth-erasable", is_nth_erasable, 3); + ("Elab.is-arg-erasable", is_arg_erasable, 3); + ("Elab.nth-arg" , nth_arg, 3); ("Array.append" , array_append,2); ("Array.create" , array_create,2); ("Array.length" , array_length,1);

===================================== src/opslexp.ml ===================================== @@ -281,7 +281,7 @@ let rec conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = | (Cons (t1, (_, l1)), Cons (t2, (_, l2))) -> l1 = l2 && conv_p t1 t2 (* I'm not sure to understand how to compare two Metavar * * Should I do a `lookup`? Or is it that simple: *) - | (Metavar (id1,_,_), Metavar (id2,_,_)) -> id1 = id2 + (*| (Metavar (id1,_,_), Metavar (id2,_,_)) -> id1 = id2*) (* FIXME: Various missing cases, such as Case. *) | (_, _) -> false

===================================== tests/array_test.ml deleted ===================================== @@ -1,187 +0,0 @@ - -open Util -open Utest_lib - -open Sexp -open Lexp - -open Eval (* reset_eval_trace *) - -open Builtin -open Env - -(* default environment *) -let ectx = Elab.default_ectx -let rctx = Elab.default_rctx - - -let _ = (add_test "ARRAY" "Array.create" (fun () -> - let dcode = " - % value_string should also be tested (it is used in interpreter) - - empty = Array_create 0 0; - - a = Array_create 1 1; - - b = Array_create 10 1; - " in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "empty; a; b;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - (* should I use value_equal here? *) - match ret with - | [Varray empty; Varray a; Varray b] -> - if (empty = (Array.make 0 (Vint 0))) - && (a = (Array.make 1 (Vint 1))) - && (b = (Array.make 10 (Vint 1))) - then success () - else failure () - | _ -> failure ()) -) - -let _ = (add_test "ARRAY" "Array.append" (fun () -> - let dcode = " - empty = Array_create 0 0; - - a = Array_append 1 empty; - - b = Array_create 1 1; - - c = Array_append 2 b; - " in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "a; c;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Varray a; Varray c] -> - if (a = (Array.make 1 (Vint 1))) - && (c = - (Array.append (Array.make 1 (Vint 1)) (Array.make 1 (Vint 2)))) - then success () - else failure () - | _ -> failure ()) -) - -let _ = (add_test "ARRAY" "Array.length" (fun () -> - let dcode = " - empty = Array_create 0 0; - - a = Array_create 101 0; - - lempty = Array_length empty; - - la = Array_length a; - " in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "lempty; la;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint empty; Vint a] -> - if (empty = 0) && (a = 101) - then success () - else failure () - | _ -> failure ()) -) - -let _ = (add_test "ARRAY" "Array.set" (fun () -> - let dcode = " - a = Array_create 101 0; - - b = Array_set 57 1 a; - - % should throw a warning (out of bounds) - c = Array_set 102 1 a; - " in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "a; b; c;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Varray a; Varray b; Varray c] -> let - aa = Array.make 101 (Vint 0) - in if (a = aa) && (Array.set aa 57 (Vint 1); b = aa) && (a = c) - then success () - else failure () - | _ -> failure ()) -) - -let _ = (add_test "ARRAY" "Array.get" (fun () -> - let dcode = " - a = Array_create 101 0; - - aa = Array_set 57 1 a; - - b = Array_get (-1) 57 aa; - - c = Array_get (-1) 102 aa; - - d = Array_get (-1) 0 aa; - " in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "b; c; d;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint b; Vint c; Vint d] -> - if (b = 1 && c = (-1) && d = 0) - then success () - else failure () - | _ -> failure ()) -) - -let _ = (add_test "ARRAY" "Array.empty, List->Array" (fun () -> - let dcode = " - List->Array = list.List->Array; - - empty1 = Array_empty (); - - empty2 = List->Array nil; - - a = List->Array (cons "a" (cons "b" (cons "c" nil))); - - b = List->Array (cons 1 (cons 2 (cons 3 nil))); - " in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "empty1; empty2; a; b;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Varray empty1; Varray empty2; Varray a; Varray b] -> - if empty1 = empty2 - && (Array.length empty1) = 0 - && (Array.length empty2) = 0 - && (Array.get a 0) = (Vstring "a") - && (Array.get a 1) = (Vstring "b") - && (Array.get a 2) = (Vstring "c") - && (Array.get b 0) = (Vint 1) - && (Array.get b 1) = (Vint 2) - && (Array.get b 2) = (Vint 3) - then success () - else failure () - | _ -> failure ()) -) - - -(* run all tests *) -let _ = run_all ()

===================================== tests/case_test.ml deleted ===================================== @@ -1,440 +0,0 @@ - -open Util -open Utest_lib - -open Sexp -open Lexp - -open Eval (* reset_eval_trace *) - -open Builtin -open Env - -(* default environment *) -let ectx = Elab.default_ectx -let rctx = Elab.default_rctx - -let case_decl = "" -(* -let case_decl = let read_file filename = - let lines = ref [] in - let chan = open_in filename in - try - while true; do - lines := input_line chan :: !lines - done; !lines - with End_of_file -> - close_in chan; - List.rev !lines - -in String.concat "\n" (read_file "samples/case2.typer") -*) - -(* eval case.typer only once! *) -let rctx, ectx = Elab.eval_decl_str case_decl ectx rctx - -let _ = (add_test "CASE MACROS" "case on single variable" (fun () -> - let dcode = (" - f : Bool -> Int; - f a = case a - | true => 1 - | _ => 0; - - g : List Int -> Int; - g xs = case xs - | cons x nil => x - | cons x xs => g xs - | _ => 0; - - va = f true; - vb = f false; - vc = g nil; - vd = g (cons 1 nil); - ve = g (cons 1 (cons 2 nil));") in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "va; vb; vc; vd; ve;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint a; Vint b; Vint c; Vint d; Vint e;] -> ( - match (a,b,c,d,e) with - | (1,0,0,1,2) -> success () - | (_,_,_,_,_) -> failure () ) - | _ -> failure ()) -) - -let _ = (add_test "CASE MACROS" "complex default 1" (fun () -> - let dcode = (" - f : Bool -> Bool -> Bool -> Int; - f a b c = case (a,b,c) - | (true,false,_) => 1 - | (false,_,true) => 2 - | (_,true,false) => 3 - | (true,true,true) => 4 - | (_,_,_) => 0; - - va = f true true true; - vb = f false true true; - vc = f true false true; - vd = f false false true; - ve = f true true false; - vf = f false true false; - vg = f true false false; - vh = f false false false; - ") in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "va; vb; vc; vd; ve; vf; vg; vh;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint a; Vint b; Vint c; Vint d; - Vint e; Vint f; Vint g; Vint h] -> ( - match (a,b,c,d,e,f,g,h) with - | (4,2,1,2,3,3,1,0) -> success () - | (_,_,_,_,_,_,_,_) -> failure () ) - | _ -> failure ()) -) - -let _ = (add_test "CASE MACROS" "complex default 2" (fun () -> - let dcode = (" - - %% I just reordered branches from `complex default 1` - - f : Bool -> Bool -> Bool -> Int; - f a b c = case (a,b,c) - | (true,true,true) => 4 - | (_,true,false) => 3 - | (false,_,true) => 2 - | (true,false,_) => 1 - | (_,_,_) => 0; - - va = f true true true; - vb = f false true true; - vc = f true false true; - vd = f false false true; - ve = f true true false; - vf = f false true false; - vg = f true false false; - vh = f false false false; - ") in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "va; vb; vc; vd; ve; vf; vg; vh;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint a; Vint b; Vint c; Vint d; - Vint e; Vint f; Vint g; Vint h] -> ( - match (a,b,c,d,e,f,g,h) with - | (4,2,1,2,3,3,1,0) -> success () - | (_,_,_,_,_,_,_,_) -> failure () ) - | _ -> failure ()) -) - -let _ = (add_test "CASE MACROS" "simple case on list" (fun () -> - let dcode = (" - f : List Int -> List Int -> Int; - f xs ys = case (xs,ys) - | (cons x xs,cons y ys) => (x + y) + (f xs ys) - | (_,_) => 0; - - g : List Int -> List Int; - g xs = case xs - | cons x ( nil) => (nil : List Int) - | cons x xs => cons x (g xs) - | _ => (nil : List Int); - - va = f (g (cons 100 (cons 101 (cons 102 nil)))) - (g (cons 1000 (cons 1001 nil))); - - vb = f (g nil) (g (cons 100 (cons 101 nil))); - ") in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "va; vb;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint a; Vint b] -> ( - match (a,b) with - | (1100,0) -> success () - | (_,_) -> failure () ) - | _ -> failure ()) -) - -let _ = (add_test "CASE MACROS" "3 constant constructor" (fun () -> - let dcode = (" - type ColorComponent - | red - | green - | blue; - - f : ColorComponent -> ColorComponent -> Int; - f c1 c2 = case (c1,c2) - | (red,red) => 1 - | (green,green) => 3 - | (blue,blue) => 2 - | (red,green) => 1 - | (red,blue) => 1 - | (green,red) => 3 - | (green,blue) => 3 - | (blue,red) => 2 - | (_,_) => 2; % (blue,green) - - va = f red red; vb = f red green; vc = f red blue; - vd = f blue blue; ve = f blue red; vf = f blue green; - vg = f green green; vh = f green red; vi = f green blue; - ") in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "va; vb; vc; vd; ve; vf; vg; vh; vi;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint a; Vint b; Vint c; - Vint d; Vint e; Vint f; - Vint g; Vint h; Vint i] -> ( - match (a,b,c,d,e,f,g,h,i) with - | (1,1,1,2,2,2,3,3,3) -> success () - | (_,_,_,_,_,_,_,_,_) -> failure () ) - | _ -> failure ()) -) - -(* I expected some particular bug which did not happen *) -(* so `sub pattern [x]` are uselessly complicated *) - -let _ = (add_test "CASE MACROS" "sub pattern 1" (fun () -> - let dcode = (" - f : List (Option Bool) -> List (Option Bool) -> Int; - f xs ys = case (xs,ys) - | (cons (some true) xs, cons (some true) ys) => f xs ys - | (cons none nil, cons none nil) => 2 - | (nil,nil) => 1 - | (_,_) => 0; - - va = f (cons (some true) nil) (cons (some true) nil); - vb = f (cons (some true) (cons (some true) nil)) - (cons (some true) (cons (some true) nil)); - vc = f nil nil; - vd = f (cons (some true) (cons none nil)) (cons (some true) (cons none nil)); - ve = f (cons (some false) nil) (cons (some false) nil); - vf = f (cons none nil) (cons (some true) nil); - vg = f (cons (some true) nil) (cons none nil); - vh = f (cons (none : Option Bool) nil) (cons (none : Option Bool) nil); - ") in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "va; vb; vc; vd; ve; vf; vg; vh;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint a; Vint b; Vint c; Vint d; - Vint e; Vint f; Vint g; Vint h] -> ( - match (a,b,c,d,e,f,g,h) with - | (1,1,1,2,0,0,0,2) -> success () - | (_,_,_,_,_,_,_,_) -> failure () ) - | _ -> failure ()) -) - -let _ = (add_test "CASE MACROS" "sub pattern 2" (fun () -> - let dcode = (" - f : List (Option Bool) -> List (Option Bool) -> Int; - f xs ys = case (xs,ys) - | (cons (some true) xs, cons (some true) ys) => f xs ys - | (cons none nil, cons none nil) => 2 - | (cons none xs, cons none ys) => f xs ys - | (nil,nil) => 1 - | (cons (some false) (cons (some false) nil), - cons (some false) (cons (some false) nil)) => 7 - | (_,_) => 0; - - va = f (cons (some true) nil) (cons (some true) nil); - vb = f (cons (some true) (cons (some true) nil)) - (cons (some true) (cons (some true) nil)); - vc = f nil nil; - vd = f (cons (some true) (cons none nil)) (cons (some true) (cons none nil)); - ve = f (cons (some false) nil) (cons (some false) nil); - vf = f (cons none nil) (cons (some true) nil); - vg = f (cons (some true) nil) (cons none nil); - vh = f (cons (none : Option Bool) nil) (cons (none : Option Bool) nil); - vi = f (cons none (cons (some true) nil)) (cons none (cons (some true) nil)); - vj = f (cons (some false) (cons (some false) nil)) - (cons (some false) (cons (some false) nil)); - ") in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "va; vb; vc; vd; ve; vf; vg; vh; vi; vj;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint a; Vint b; Vint c; Vint d; Vint e; - Vint f; Vint g; Vint h; Vint i; Vint j] -> ( - match (a,b,c,d,e,f,g,h,i,j) with - | (1,1,1,2,0,0,0,2,1,7) -> success () - | (_,_,_,_,_,_,_,_,_,_) -> failure () ) - | _ -> failure ()) -) - -let _ = (add_test "CASE MACROS" "sub pattern 3" (fun () -> - let dcode = (" - f : Option Bool -> Option Bool -> Int; - f 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; - - va = f (some true) (some true); - vb = f (some false) (some true); - vc = f (some true) (some false); - vd = f (some false) (some false); - ve = f (some true) none; - vf = f (some false) none; - vg = f none (some true); - vh = f none (some false); - vi = f none none; - ") in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "va; vb; vc; vd; ve; vf; vg; vh; vi;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint a; Vint b; Vint c; Vint d; Vint e; - Vint f; Vint g; Vint h; Vint i] -> ( - match (a,b,c,d,e,f,g,h,i) with - | (0,1,2,3,4,5,6,7,8) -> success () - | (_,_,_,_,_,_,_,_,_) -> failure () ) - | _ -> failure ()) -) - -let _ = (add_test "CASE MACROS" "sub pattern 4" (fun () -> - let dcode = (" - g : Bool -> Bool -> Int; - g b0 b1 = case (b0,b1) - | (true,true) => 0 - | (_,_) => 1; - - f : Option (Option Bool) -> Option (Option Bool) -> Int; - f oob0 oob1 = case (oob0,oob1) - | (some (some b0), some (some b1)) => g b0 b1 - | (some none, some none) => 2 - | (none, none) => 3 - | (_,_) => 4; - - va = f (some none) none; - vb = f none none; - vc = f (some none) (some none); - vd = f (some (some false)) (some (some false)); - ve = f (some (some true)) (some (some true)); - ") in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "va; vb; vc; vd; ve;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint a; Vint b; Vint c; Vint d; Vint e] -> ( - match (a,b,c,d,e) with - | (4,3,2,1,0) -> success () - | (_,_,_,_,_) -> failure () ) - | _ -> failure ()) -) - -let _ = (add_test "CASE MACROS" "no default" (fun () -> - let dcode = (" - f : Bool -> Bool -> Int; - f b1 b2 = case (b1,b2) - | (false,false) => 0 - | (true,false) => 1 - | (false,true) => 2 - | (true,true) => 3; - - va = f false false; - vb = f true false; - vc = f false true; - vd = f true true; - ") in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "va; vb; vc; vd;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint a; Vint b; Vint c; Vint d] -> ( - match (a,b,c,d) with - | (0,1,2,3) -> success () - | (_,_,_,_) -> failure () ) - | _ -> failure ()) -) - -let _ = (add_test "CASE MACROS" "introduced variable name" (fun () -> - let dcode = (" - and : Bool -> Bool -> Int; - and b0 b1 = case (b0, b1) - | (true, true) => 2 - | (true, false) => 1 - | (false, true) => 1 - | (false, false) => 0; - - %% `cons x xs` vs `cons a as` and `cons y ys` vs `cons b bs` - - f : List Bool -> List Bool -> Int; - f xs ys = case (xs, ys) - | (cons x xs, nil) => (and x false) + (f xs nil) - | (nil, cons y ys) => (and false y) + (f nil ys) - | (cons a as, cons b bs) => (and a b) + (f as bs) - | (nil, nil) => 0; - - va = f (cons true nil) nil; - vb = f nil (cons false nil); - vc = f (cons true nil) (cons true nil); - vd = f (cons false nil) (cons false nil); - ve = f (cons true nil) (cons false nil); - vf = f nil nil; - ") in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "va; vb; vc; vd; ve; vf;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vint a; Vint b; Vint c; Vint d; Vint e; Vint f] -> ( - match (a,b,c,d,e,f) with - | (1,0,2,0,1,0) -> success () - | (_,_,_,_,_,_) -> failure () ) - | _ -> failure ()) -) - - -(* run all tests *) -let _ = run_all ()

===================================== tests/elabctx_test.ml deleted ===================================== @@ -1,196 +0,0 @@ - -open Util -open Utest_lib - -open Sexp -open Lexp - -open Eval (* reset_eval_trace *) - -open Builtin -open Env - -(* default environment *) -let ectx = Elab.default_ectx -let rctx = Elab.default_rctx - - -let _ = (add_test "ELABCTX" "Elab_getenv" (fun () -> - let dcode = " - return = IO_return; - - nop = (lambda _ -> return ()); - - action = do - { - env <- (Elab_getenv ()); - - return env; - };" in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "action;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vcommand cmd] -> ( match (cmd ()) with - | (Velabctx _) -> success () - | _ -> failure () ) - | _ -> failure ()) -) - -let v2o_bool v = match v with - | Vcons ((_, "false"), []) -> false - | Vcons ((_, "true"), []) -> true - | _ -> raise Not_found - -let _ = (add_test "ELABCTX" "Elab_isbound" (fun () -> - let dcode = " - return = IO_return; - - nop = (lambda _ -> return ()); - - a = do - { - env <- (Elab_getenv ()); - - return (Elab_isbound "Int" env); - }; - - b = do - { - env <- (Elab_getenv ()); - - return (Elab_isbound "List" env); - }; - - c = do - { - env <- (Elab_getenv ()); - - return (Elab_isbound "Elab_isbound" env); - }; - - d = do - { - env <- (Elab_getenv ()); - - return (Elab_isbound "do" env); - }; - - e = do - { - env <- (Elab_getenv ()); - - return (Elab_isbound "randomunusednameabc123" env); - };" in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "a; b; c; d; e;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - try match List.map (function (Vcommand cmd) -> v2o_bool (cmd ()) - | _ -> raise Not_found) ret with - | [true; true; true; true; false] -> success () - | _ -> failure () - with _ -> failure ()) -) - -let _ = (add_test "ELABCTX" "Elab_isconstructor" (fun () -> - let dcode = " - return = IO_return; - - nop = (lambda _ -> return ()); - othercons = cons; - - af = do - { - env <- (Elab_getenv ()); - - return (Elab_isconstructor "Int" env); - }; - - bf = do - { - env <- (Elab_getenv ()); - - return (Elab_isconstructor "List" env); - }; - - cf = do - { - env <- (Elab_getenv ()); - - return (Elab_isconstructor "Elab_isbound" env); - }; - - df = do - { - env <- (Elab_getenv ()); - - return (Elab_isconstructor "do" env); - }; - - ef = do - { - env <- (Elab_getenv ()); - - return (Elab_isconstructor "randomunusednameabc123" env); - }; - - at = do - { - env <- (Elab_getenv ()); - - return (Elab_isconstructor "cons" env); - }; - - bt = do - { - env <- (Elab_getenv ()); - - return (Elab_isconstructor "nil" env); - }; - - ct = do - { - env <- (Elab_getenv ()); - - return (Elab_isconstructor "true" env); - }; - - dt = do - { - env <- (Elab_getenv ()); - - return (Elab_isconstructor "false" env); - }; - - et = do - { - env <- (Elab_getenv ()); - - return (Elab_isconstructor "othercons" env); - };" in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "af; bf; cf; df; ef; at; bt; ct; dt; et;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - try match List.map (function (Vcommand cmd) -> v2o_bool (cmd ()) - | _ -> raise Not_found) ret with - | [false; false; false; false; false; - true; true; true; true; true] -> success () - | _ -> failure () - with _ -> failure ()) -) - - -(* run all tests *) -let _ = run_all ()

===================================== tests/macro_do_test.ml deleted ===================================== @@ -1,149 +0,0 @@ - -open Util -open Utest_lib - -open Sexp -open Lexp - -open Eval (* reset_eval_trace *) - -open Builtin -open Env - -(* default environment *) -let ectx = Elab.default_ectx -let rctx = Elab.default_rctx - -(* all tests use binded variable *) -(* I'm saying it in case everythings break *) - -(* there's a problem with string inside string when I use new line ("\n") *) - -(* mostly to check if no exception are thrown *) -let _ = (add_test "DO MACROS" "Hello, world!" (fun () -> - let dcode = " - return = IO_return; - - nop = (lambda _ -> return ()); - - action = do - { - str <- return "Hello, world!"; - - nop str; - };" in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "action;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vcommand _] -> success () - | _ -> failure ()) -) - -(* check return value from do macro *) -let _ = (add_test "DO MACROS" "return value" (fun () -> - let dcode = " - return = IO_return; - - nop = (lambda _ -> return ()); - - action = do - { - nop "Doing random stuff before returning..."; - - n <- return 123456789; - - return n; - };" in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "action;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vcommand cmd] -> ( match (cmd ()) with - | Vint v -> - if (123456789 = v) then success () else failure () - | _ -> failure() ) - - | _ -> failure ()) -) - -(* check if any problem when using do as command inside another do *) -let _ = (add_test "DO MACROS" "do inside do" (fun () -> - let dcode = " - return = IO_return; - - nop = (lambda _ -> return ()); - - action0 = do { return 123; }; - - action1 = do - { - x <- do { return (Float_+ 16.0 0.125); }; - - nop "Doing random stuff..."; - - str <- return (Float->String x); - - val123 <- action0; - - do { nop str; }; - - do { do { nop str; }; }; - - return str; - };" in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "action1;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vcommand cmd] -> ( match (cmd ()) with - | Vstring str -> if ("16.125" = str) then success () else failure () - | _ -> failure () ) - | _ -> failure ()) -) - -(* declaring the type before assignement *) -(* this is an unexpected functionality that may be usefull *) -let _ = (add_test "DO MACROS" "assignement with type declaration" (fun () -> - let dcode = " - return = IO_return; - - nop = (lambda _ -> return ()); - - action = do - { - (t : Bool) <- return true; - - (f : Bool) <- return false; - - return (if f then 333 else - (if t then 777 else 333)); - };" in - - let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in - - let ecode = "action;" in - - let ret = Elab.eval_expr_str ecode ectx rctx in - - match ret with - | [Vcommand cmd] -> ( match (cmd ()) with - | Vint 777 -> success () - | _ -> failure () ) - | _ -> failure ()) -) - -(* run all tests *) -let _ = run_all ()

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