Jonathan Graveline pushed to branch graveline at Stefan / Typer

Commits: 246ba428 by Jonathan Graveline at 2018-06-25T21:22:00Z macro "case" now use "do" and "Elab_isconstructor"; added tests/case_test.ml

- - - - -

2 changed files:

- samples/case.typer - + tests/case_test.ml

Changes:

===================================== samples/case.typer ===================================== @@ -3,9 +3,6 @@ %%% %%% (pattern matching) %%% -%%% This file may not be up to date with version -%%% in pervasive.typer -%%%

%% %% Match every variable in each pattern with a list of VarTest. @@ -68,12 +65,21 @@ mapi f i xs = case xs | cons x xs => cons (f x i) (mapi f (i + 1) xs);

io_list : List (IO ?a) -> IO (List ?a); -io_list l = IO_bind (List_foldl - (lambda o v -> IO_bind o - (lambda o -> IO_bind v - (lambda v -> IO_return (cons v o)))) - (IO_return nil) l) - (lambda l -> IO_return (List_reverse l nil)); +io_list l = let + + fold_fun : IO (List ?a) -> IO ?a -> IO (List ?a); + fold_fun o v = do + { + o <- o; + v <- v; + IO_return (cons v o); + }; + +in do +{ + l <- (List_foldl fold_fun (IO_return nil) l); + IO_return (List_reverse l nil); +};

get_num_vars : List Sexp -> IO (List Sexp); get_num_vars vars = io_list (List_map @@ -109,6 +115,21 @@ get_cases sexps = let

in helper sexps;

+%% +%% return true if v is a ctor +%% +is_ctor : Sexp -> IO Bool; +is_ctor v = Sexp_dispatch v + (lambda _ _ -> IO_return true) + (lambda s -> do + { + env <- Elab_getenv (); + b <- Elab_isconstructor s env; + IO_return (Int_eq b 1); + }) + (lambda _ -> IO_return false) (lambda _ -> IO_return false) + (lambda _ -> IO_return false) (lambda _ -> IO_return false); + %% %% Rename nth constructor inside ctor to sym %% @@ -116,27 +137,45 @@ in helper sexps; rename_nth : Int -> Sexp -> Sexp -> IO Sexp; rename_nth n ctor sym = let

- mapiif : (Sexp -> Int -> Sexp) -> (Sexp -> Bool) -> Int -> List Sexp -> List Sexp; - mapiif f b i xs = case xs - | nil => nil - | cons x xs => if_then_else_ (b x) - (cons (f x i) (mapiif f b (i + 1) xs)) - (cons x (mapiif f b i xs)); + mapiif : (Sexp -> Int -> Sexp) -> (Sexp -> IO Bool) + -> Int -> IO (List Sexp) -> IO (List Sexp); + mapiif f b i xs = let

- err = (lambda _ -> Sexp_symbol "<not a ctor (0)>"); + helper : (Sexp -> Int -> Sexp) -> (Sexp -> IO Bool) -> Int + -> List Sexp -> IO (List Sexp); + helper f b i xs = case xs + | nil => IO_return nil + | cons x xs => (let + + apply : (Sexp -> Int -> Sexp) -> (Sexp -> IO Bool) -> Int + -> List Sexp -> IO (List Sexp); + apply f b i xs = do + { + xs <- (helper f b (i + 1) xs); + IO_return (cons (f x i) xs); + }; + + continue : (Sexp -> Int -> Sexp) -> (Sexp -> IO Bool) -> Int + -> List Sexp -> IO (List Sexp); + continue f b i xs = do + { + xs <- (helper f b i xs); + IO_return (cons x xs); + }; + + in do + { + bv <- b x; + (if_then_else_ bv (apply f b i xs) (continue f b i xs)); + });

- %% - %% Is argument a variable or a ctor - %% - %% (use keyword "ctor" if the ctor has no argument to - %% to differentiate with a variable) - %% + in do + { + xs <- xs; + helper f b i xs; + };

- is_ctor : Sexp -> Bool; - is_ctor v = Sexp_dispatch v - (lambda _ _ -> true) (lambda _ -> false) - (lambda _ -> false) (lambda _ -> false) - (lambda _ -> false) (lambda _ -> false); + err = (lambda _ -> Sexp_symbol "<not a ctor (0)>");

%% %% Check for ctor within englobing ctor and rename variable @@ -147,14 +186,21 @@ rename_nth n ctor sym = let (lambda s ss -> if_then_else_ (Int_eq i n) (sym) (Sexp_symbol "_")) - (lambda s -> Sexp_symbol s) + (lambda s -> if_then_else_ (Int_eq i n) + (sym) + (Sexp_symbol "_")) err err err err ; + + io_err = (lambda _ -> IO_return (Sexp_symbol "<not a ctor (1)>"));

-in IO_return (Sexp_dispatch ctor - (lambda s ss -> Sexp_node s - (mapiif sub_ctor is_ctor 0 ss)) - (lambda s -> Sexp_symbol s) - err err err err); +in (Sexp_dispatch ctor + (lambda s ss -> do + { + ss <- (mapiif sub_ctor is_ctor 0 (IO_return ss)); + IO_return (Sexp_node s ss); + }) + (lambda s -> IO_return (Sexp_symbol s)) + io_err io_err io_err io_err);

%% %% Expand sub pattern into sub_test @@ -170,28 +216,29 @@ expand_cases pats = let | nil => o | cons x xs => foldi f (i + 1) (f x i o) xs;

- get_sub_pattern : Sexp -> List Sexp; + get_sub_pattern : Sexp -> IO (List Sexp); get_sub_pattern ctor = let

err = (lambda _ -> Sexp_error); - - check_keyword : Sexp -> Sexp; - check_keyword ctor = Sexp_dispatch ctor - (lambda s ss -> if_then_else_ (Sexp_eq s (Sexp_symbol "ctor")) - (Sexp_node (List_nth 0 ss Sexp_error) (List_tail ss)) - (Sexp_node s ss)) - (lambda s -> Sexp_symbol s) - err err err err;

- no_pattern : List Sexp -> ? -> List Sexp; - no_pattern pats = (lambda _ -> pats); + no_pattern : List Sexp -> ? -> IO (List Sexp); + no_pattern pats = (lambda _ -> IO_return pats);

- helper : List Sexp -> List Sexp; - helper vars = List_foldl (lambda pats var -> + helper : List Sexp -> IO (List Sexp); + helper vars = List_foldl (lambda pats var -> do + { + pats <- pats; Sexp_dispatch var - (lambda s ss -> cons (check_keyword (Sexp_node s ss)) pats) - (no_pattern pats) (no_pattern pats) (no_pattern pats) (no_pattern pats) (no_pattern pats) - ) nil vars; + (lambda s ss -> IO_return (cons (Sexp_node s ss) pats)) + (lambda s -> do + { + b <- is_ctor (Sexp_symbol s); + if_then_else_ b + (IO_return (cons (Sexp_symbol s) pats)) + (no_pattern pats ()); + }) + (no_pattern pats) (no_pattern pats) (no_pattern pats) (no_pattern pats) + }) (IO_return nil) vars;

in Sexp_dispatch ctor (lambda s ss -> helper ss) @@ -227,11 +274,12 @@ expand_cases pats = let (lambda t -> IO_return (sub_test v t)) | _ => IO_return (var_test Sexp_error);

- sub_pattern : List Sexp; - sub_pattern = List_reverse (get_sub_pattern t) nil; - - nb_pattern : Int; - nb_pattern = List_length sub_pattern; + sub_pattern : IO (List Sexp); + sub_pattern = do + { + l <- get_sub_pattern t; + IO_return (List_reverse l nil); + };

sub_case : IO (List VarTest); sub_case = let @@ -240,17 +288,42 @@ expand_cases pats = let helper c r o = IO_return (List_concat o (cons r (cons (sub_test not_unique_sym c) nil)));

- in IO_bind (foldi - (lambda c i o -> IO_bind o (lambda o -> (IO_bind (renamed i) - (lambda r -> (helper c r o))))) - 0 (IO_return nil) sub_pattern) - (lambda l -> IO_return (cons (push_var nb_pattern) l)); + l : IO (List VarTest); + l = do + { + sub_pattern <- sub_pattern; + (foldi + (lambda c i o -> do + { + o <- o; + r <- (renamed i); + helper c r o; + }) 0 (IO_return nil) sub_pattern) + };

- in if_then_else_ (Int_eq nb_pattern 0) - (IO_bind all (lambda all -> - IO_return (List_concat all (cons test nil)))) - (IO_bind sub_case (lambda l -> IO_bind all - (lambda all -> IO_return (List_concat all l)))) + in do + { + l <- l; + sub_pattern <- sub_pattern; + IO_return (cons (push_var (List_length sub_pattern)) l); + }; + + in do + { + sub_pattern <- sub_pattern; + if_then_else_ (Int_eq (List_length sub_pattern) 0) + (do + { + all <- all; + IO_return (List_concat all (cons test nil)); + }) + (do + { + sub_case <- sub_case; + all <- all; + IO_return (List_concat all sub_case); + }) + };

in expand test);

@@ -261,11 +334,18 @@ expand_cases pats = let

ctors : IO (List VarTest); ctors = (List_foldl expand_one (IO_return nil) cs); - - in IO_bind ctors (lambda ctors -> - if_then_else_ (Int_eq (List_length cs) (List_length ctors)) + + stop_on_id : List VarTest -> IO Pattern; + stop_on_id ctors = if_then_else_ + (Int_eq (List_length cs) (List_length ctors)) (IO_return (branch ctors f)) - (expand_all (branch ctors f)))); + (expand_all (branch ctors f)); + + in do + { + ctors <- ctors; + stop_on_id ctors; + });

in io_list (List_map expand_all pats);

@@ -406,30 +486,20 @@ case_ = macro (lambda args -> let

nfun : Sexp; nfun = fun; - - % - % I was using lambda_->_, then ##case_ needed a type so I added decltype, - % then decltype needed variable (rather than composed expression) - % so we end up with a let_in_ (thanks to gensym). - % - % nfun = (Sexp_node (foldi - % (lambda v i fun -> (quote (lambda_->_ - % ((uquote (List_nth i nvars Sexp_error)) : (decltype (uquote v))) - % (uquote fun)))) - % 0 fun fvars) (List_reverse fvars nil)); - %

in IO_return ( (foldi (lambda v i fun -> (quote ( let (uquote (List_nth i nvars Sexp_error)) = (uquote v); in (uquote fun)))) 0 nfun vars)); - % in IO_return nfun;

- in IO_bind (expand_cases pats) (lambda pats -> - (IO_bind num_vars (lambda num_vars -> - IO_bind free_vars (lambda free_vars -> - IO_bind (pattern_to_sexp num_vars pats) (lambda f -> - vars_wrap free_vars num_vars f))))); + in do + { + pats <- expand_cases pats; + num_vars <- num_vars; + free_vars <- free_vars; + f <- pattern_to_sexp num_vars pats; + vars_wrap free_vars num_vars f; + };

% Only the Sexp after "_|_" are interesting

===================================== tests/case_test.ml ===================================== @@ -0,0 +1,212 @@ + +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 + +(* + Macro case break some test so I read definition here. + It's temporary. I will need to modify other test to use ##case_ (which is what + they need to test) or modify the macro to work with everything (there's strange + case in eval_test.ml which I did not expect). +*) +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/case.typer") + +let _ = (add_test "CASE MACROS" "case on single variable" (fun () -> + let dcode = (case_decl^" + 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" "case on Bool" (fun () -> + let dcode = (case_decl^" + 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" "case on list" (fun () -> + let dcode = (case_decl^" + 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" (fun () -> + let dcode = (case_decl^" + 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 ()) +) + +let _ = (add_test "CASE MACROS" "sub pattern" (fun () -> + let dcode = (case_decl^" + 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 + | (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); + ") in + + let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in + + let ecode = "va; vb; vc; vd; ve; vf; vg;" 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] -> ( + match (a,b,c,d,e,f,g) with + | (1,1,1,0,0,0,0) -> success () + | (_,_,_,_,_,_,_) -> failure () ) + | _ -> failure ()) +) + + +(* run all tests *) +let _ = run_all ()

View it on GitLab: https://gitlab.com/monnier/typer/commit/246ba4287daff4c4107d43fd8db4fc9727c1...