Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits: ff69f5cf by Jonathan Graveline at 2018-07-24T01:55:12Z more List functions
- - - - - 61fc705d by Jonathan Graveline at 2018-07-24T02:18:36Z progression on the `case` macro
- - - - - e3e9599b by Jonathan Graveline at 2018-07-24T02:22:13Z Merge branch 'graveline' of https://gitlab.com/monnier/typer into graveline
- - - - -
4 changed files:
- btl/pervasive.typer - + samples/case2.typer - samples/list.typer - tests/case_test.ml
Changes:
===================================== btl/pervasive.typer ===================================== @@ -154,6 +154,33 @@ List_foldl f i xs = case xs | nil => i | cons x xs => List_foldl f (f i x) xs;
+List_mapi : (a : Type) ≡> (b : Type) ≡> (a -> Int -> b) -> List a -> List b; +List_mapi f xs = let + helper : (a -> Int -> b) -> Int -> List a -> List b; + helper f i xs = case xs + | nil => nil + | cons x xs => cons (f x i) (helper f (i + 1) xs); +in helper f 0 xs; + +List_map2 : (?a -> ?b -> ?c) -> List ?a -> List ?b -> List ?c; +List_map2 f xs ys = case xs + | nil => nil + | cons x xs => case ys + | nil => nil % error + | cons y ys => cons (f x y) (List_map2 f xs ys); + +%% Fold 2 List as long as both List are non-empty +List_fold2 : (?a -> ?b -> ?c -> ?a) -> ?a -> List ?b -> List ?c -> ?a; +List_fold2 f o xs ys = case xs + | cons x xs => ( case ys + | cons y ys => List_fold2 f (f o x y) xs ys + | nil => o ) % may be an error + | nil => o; % may or may not be an error + +%% Is argument List empty? +List_empty : List ?a -> Bool; +List_empty xs = Int_eq (List_length xs) 0; + %%% Good 'ol combinators
I : ?a -> ?a; @@ -391,6 +418,35 @@ __.__ = | nil => Sexp_error) | nil => Sexp_error);
+%% Triplet (tuple with 3 values) +type Triplet (a : Type) (b : Type) (c : Type) + | triplet (x : a) (y : b) (z : c); + +%%%% List with tuple + +%% Merge two List to a List of Pair +%% Both List must be of same length +List_merge : List ?a -> List ?b -> List (Pair ?a ?b); +List_merge xs ys = case xs + | cons x xs => ( case ys + | cons y ys => cons (pair x y) (List_merge xs ys) + | nil => nil ) % error + | nil => nil; + +%% `Unmerge` a List of Pair +%% The two functions name said it all +List_map-fst : List (Pair ?a ?b) -> List ?a; +List_map-fst xs = let + mf : Pair ?a ?b -> ?a; + mf p = case p | pair x _ => x; +in List_map mf xs; + +List_map-snd : List (Pair ?a ?b) -> List ?b; +List_map-snd xs = let + mf : Pair ?a ?b -> ?b; + mf p = case p | pair _ y => y; +in List_map mf xs; + %%%% Logic
%% `False` should be one of the many empty types. @@ -563,4 +619,20 @@ List->Array xs = let
in (helper xs (Array_empty ()));
+%% Move IO outside List (from element to List) +%% (Was helpful for me when translating code that used to not be IO code) +%% (The function's type explain everything) +io-list : List (IO ?a) -> IO (List ?a); +io-list l = let + ff : IO (List ?a) -> IO ?a -> IO (List ?a); + ff o v = do { + o <- o; + v <- v; + IO_return (cons v o); + }; +in do { + l <- (List_foldl ff (IO_return nil) l); + IO_return (List_reverse l nil); +}; + %%% pervasive.typer ends here.
===================================== samples/case2.typer ===================================== @@ -0,0 +1,660 @@ +%%%% +%%%% macro "case" (pattern matching) +%%%% +%%%% case ... | (...) => ... +%%%% +%%%% (Just to be clear: What I call a pattern is +%%%% a constructor with or without argument and +%%%% argument may be sub pattern or variable) +%%%% + +%% +%% Generate a List of pseudo-unique symbol +%% +%% Takes a List of Sexp and generate a List of new name of the same length +%% whatever are the element of the List +%% + +gen-vars : List Sexp -> IO (List Sexp); +gen-vars vars = io-list (List_map + (lambda _ -> gensym ()) + vars); + +%% +%% Get matched expression (e.g. case (var1,var2,...) | ...) +%% +%% Expression are separated by "," so it is useful for +%% case (expr1,expr2,...) ... +%% but also for +%% case ... | (expr3,expr4,...) => ... +%% + +get-tup-exprs : Sexp -> List Sexp; +get-tup-exprs sexp = let + + err = (lambda _ -> cons Sexp_error nil); + + get-tup-exprs-helper : Sexp -> List Sexp -> List Sexp; + get-tup-exprs-helper s ss = case (Sexp_eq (Sexp_symbol "_,_") s) + | true => (ss) % tuple + %% constructor or function called (only 1 pattern) + | false => (cons (Sexp_node s ss) nil); + +in Sexp_dispatch sexp + get-tup-exprs-helper + (lambda s -> (cons (Sexp_symbol s) nil)) + err err err + (lambda ss -> cons ss nil); % do nothing to Block + +%% +return = IO_return; + +%% +%% Some alias to clarify type of functions +%% + +Var = Sexp; +Pat = Sexp; +Pats = List Pat; +Code = Sexp; + +Pat_error = Sexp_symbol "<pattern error>"; +Var_error = Sexp_symbol "<variable error>"; +Code_error = Sexp_symbol "<code error>"; + +dflt-var : Var; +dflt-var = Sexp_symbol "_"; + +is-dflt : Var -> Bool; +is-dflt v = Sexp_eq dflt-var v; + +%% +%% Get pattern to match +%% + +get-branches : List Sexp -> List (Pair Pats Code); +get-branches sexps = let + + perr = (lambda _ -> pair (cons Pat_error nil) Code_error); + + to-case : Sexp -> Pair Pats Code; + to-case sexp = Sexp_dispatch sexp + + (lambda s ss -> case (Sexp_eq (Sexp_symbol "_=>_") s) + % expecting a Sexp_node as second argument to _=>_ + | true => pair (get-tup-exprs (List_nth 0 ss Pat_error)) (List_nth 1 ss Code_error) + | false => pair (cons Pat_error nil) Code_error) + + perr perr perr perr perr; + + helper : List Sexp -> List (Pair Pats Code); + helper sexps = List_map (lambda s -> (to-case s)) sexps; + +in helper sexps; + +%% +%% Get constructor without any sub constructor and with variable renamed +%% +%% Takes a pattern and a list of new name for each argument +%% It even rename sub pattern +%% + +renamed-pat : Sexp -> List Sexp -> IO Sexp; +renamed-pat pat names = let + + serr = lambda _ -> Sexp_error; + + mf : Sexp -> Int -> Sexp; + mf v i = Sexp_dispatch v + (lambda _ _ -> List_nth i names Sexp_error) + (lambda _ -> List_nth i names Sexp_error) + serr serr serr serr; + +in return (Sexp_dispatch pat + (lambda s ss -> Sexp_node s (List_mapi mf ss)) + (lambda s -> Sexp_symbol s) + serr serr serr serr); + +%%% +%%% +%%% +%%% +%%% + +%% +%% Takes an Sexp as argument and return `IO true` if it is a pattern +%% (i.e. a constructor with or without argument) +%% + +is-pat : Pat -> IO Bool; +is-pat pat = let + + err = lambda _ -> return false; + +in Sexp_dispatch pat + (lambda _ _ -> return true) + (lambda sym -> do { + env <- Elab_getenv (); + return (Elab_isconstructor sym env); + }) + err err err err; + +%% +%% Takes two pattern and return `IO true` if the two pattern +%% has the same constructor +%% + +is-same-ctor : Pat -> Pat -> Bool; +is-same-ctor p0 p1 = let + + err = lambda _ -> Pat_error; + + ctor-of : Pat -> Sexp; + ctor-of p = Sexp_dispatch p + (lambda s _ -> s) + (lambda s -> Sexp_symbol s) + err err err err; + +in Sexp_eq (ctor-of p0) (ctor-of p1); + +%% +%% Get variable introduced by a constructor +%% +%% Takes a pattern as argument and return each arguments +%% of the constructor which is a variable (as opposed to a sub pattern) +%% + +introduced-vars : Pat -> IO (List Var); +introduced-vars pat = let + + serr = lambda _ -> return nil; + + ff : IO (List Sexp) -> Sexp -> IO (List Sexp); + ff o v = Sexp_dispatch v + (lambda _ _ -> do { + o <- o; % bind + %% there's no introduced variable here + %% `case` on sub pattern will introduce new variable + %% but not here + return (List_concat o (cons dflt-var nil)); + }) + (lambda s -> do { + o <- o; % bind + sym <- return (Sexp_symbol s); + b <- is-pat sym; + if_then_else_ (b) + (return (List_concat o (cons dflt-var nil))) + (return (List_concat o (cons sym nil))); + }) + serr serr serr serr; + +in Sexp_dispatch pat + (lambda _ ss -> List_foldl ff (return nil) ss) + (lambda _ -> return nil) % constructor as a unique symbol (as `true`) + (lambda _ -> return nil) (lambda _ -> return nil) % error + (lambda _ -> return nil) (lambda _ -> return nil); % error + +%% +%% Wrap the third argument (`fun`) with a `let` definition for each variables +%% Names are taken from `rvars` and definition are taken from `ivars` +%% + +wrap-vars : List Var -> List Var -> Code -> Code; +wrap-vars ivars rvars fun = List_fold2 (lambda fun v0 v1 -> + (quote (let (uquote v1) = (uquote v0) in (uquote fun)))) + %%(quote ((lambda (uquote v0) -> (uquote fun)) (uquote v1)))) + fun ivars rvars; + +%% +%% Take a List of branches and return a List of the first pattern in each branches +%% (I must keep the order from input to ouput) +%% + +head-pats : List (Pair Pats Code) -> List Pat; +head-pats ps = let + + mf : Pair Pats Code -> Pat; + mf p = case p + | pair pats _ => (List_nth 0 pats Pat_error); + +in List_map mf ps; + +%% +%% Takes a pattern as argument and +%% return a List of sub pattern for that branch +%% the List contain dflt-var if it has a variable which is not a pattern +%% + +pattern-sub-pats : Pat -> IO (List Pat); +pattern-sub-pats pat = let + + err = lambda _ -> return nil; + + %% + %% dflt-var mean there's no sub pattern + %% + %% I keep it because it could be a default + %% if another branch has a sub pattern + %% at this position + %% + + map-arg : Var -> IO Var; + map-arg arg = do { + b <- is-pat arg; + if_then_else_ (b) + (return arg) + (return dflt-var); + }; + +in Sexp_dispatch pat + (lambda ctor args -> do { + r <- io-list (List_map map-arg args); + return r; + }) + (lambda sym -> do { + %% + %% constructor has no argument + %% so there can't be any sub pattern + %% + return nil; + }) + err err err err; + +%% +%% Takes a List of similar pattern (i.e. a pattern of same constructor) +%% return a List of gensym variable if there's is a sub pattern +%% and a default variable when there's no sub pattern +%% + +pattern-sub-pats-vars : List Var -> List (Pair Pat (List (Pair Var Var))) -> IO (List Var); +pattern-sub-pats-vars rvars branches = let + + pats : List Pat; + pats = let + + mf : Pair Pat (List (Pair Var Var)) -> Pat; + mf p = case p | pair pat _ => pat; + + in List_map mf branches; + + ff : IO (List Var) -> Pat -> IO (List Var); + ff psubs pat = let + + subs : IO (List Pat); + subs = do { + r <- pattern-sub-pats pat; + return r; + }; + + in do { + psubs <- psubs; + subs <- subs; + + if_then_else_ (List_empty subs) + (return psubs) + (return (List_mapi (lambda c n -> let + new-sym = List_nth n rvars Var_error; + prev-sym = List_nth n psubs dflt-var; + in if_then_else_ (is-dflt c) + (prev-sym) + (new-sym) + ) subs)); + }; + +in List_foldl ff (return nil) pats; + +%% +%% return a List of old/new variables names +%% +%% new variable should be identical for each branches +%% but old variable (from user code) are arbitrary +%% + +pattern-term : Pat -> List Var -> IO (List (Pair Var Var)); +pattern-term pat rvars = let + + ff : List (Pair Var Var) -> Var -> Var -> List (Pair Var Var); + ff o v0 v1 = if_then_else_ (is-dflt v0) + (o) + (List_concat o (cons (pair v0 v1) nil)) + +in do { + ivars <- introduced-vars pat; + rvv <- return (List_fold2 ff nil ivars rvars); + return rvv; +}; + +%% +%% Type of one partition of branches (one branch with some possible child branches) +%% +%% pair of renamed pat, variables old/new in each branch and List of next branch +%% a branch with a pattern with old/new variables for each next branches +%% and each next branches from this branch +%% + +part-type = Pair (Triplet Pat (List Var) (List (Pair Pat (List (Pair Var Var))))) (List (Pair Pats Code)); + +%% +%% return a pair of renamed and patitioned pattern +%% (i.e. a Pair of renamed pattern, introduced variables, old pattern and tail of branches) +%% (Yeah, I need old pattern to get sub pattern at some point) +%% + +partition-branches : List (Pair Pats Code) -> IO (List part-type); +partition-branches branches = let + + tl-branches : List (Pair Pats Code); + tl-branches = let + + mf : Pair Pats Code -> Pair Pats Code; + mf p = case p + | pair pats code => pair (List_tail pats) code; + + in List_map mf branches; + + hd-pair : List (Pair Pat (Pair Pats Code)); + hd-pair = let + + ff : List (Pair Pat (Pair Pats Code)) -> Pat -> Pair Pats Code -> + List (Pair Pat (Pair Pats Code)); + ff o pat tails = List_concat o (cons (pair pat tails) nil); + + in List_fold2 ff nil (head-pats branches) tl-branches; + + %% + %% Type for first step partition + %% + %% Pair of List sorted with similar hd (hd as in `fst`) + %% + + pre-part-type = Pair (List Pat) (List (Pair Pats Code)); + + pre-parts : List pre-part-type; + pre-parts = let + + is-similar : Pat -> Pat -> Bool; + is-similar p0 p1 = is-same-ctor p0 p1; + + ff : List pre-part-type -> Pair Pat (Pair Pats Code) -> List pre-part-type; + ff o p = case p | pair pat tail => (case o + | nil => cons (pair (cons pat nil) (cons tail nil)) nil + | cons part parts => (case part | pair ps _ => + if_then_else_ (is-dflt pat) + %% default is both equivalent and different from every pattern? + %% the are merged with `merge-dflt` + (case part | pair pp tt => cons + (pair (List_concat pp (cons pat nil)) + (List_concat tt (cons tail nil))) + (ff parts p)) %% This line sometimes produce too many patterns + (if_then_else_ (is-similar pat (List_nth 0 ps Pat_error)) + (case part | pair pp tt => cons + (pair (List_concat pp (cons pat nil)) + (List_concat tt (cons tail nil))) + parts) + (cons part (ff parts p))))); + + in List_foldl ff nil hd-pair; + + parts : IO (List part-type); + parts = let + + ff : List Var -> IO (List (List (Pair Var Var))) -> Pat -> + IO (List (List (Pair Var Var))); + ff rvars o p = do { + o <- o; + p <- pattern-term p rvars; + return (List_concat o (cons p nil)); + }; + + mf : pre-part-type -> IO part-type; + mf p = case p + | pair pp tt => do { + pat <- return (List_nth 0 pp Pat_error); + ivars <- introduced-vars pat; + rvars <- gen-vars ivars; + rpat <- renamed-pat pat rvars; + vars <- List_foldl (ff rvars) (return nil) pp; + return (pair (triplet rpat rvars (List_merge pp vars)) tt); + }; + + in io-list (List_map mf pre-parts); + +in do { + parts <- parts; + return parts; +}; + +%% +%% reminder +%% part-type = Pair (Triplet Pat (List Var) (List (Pair Pat (List (Pair Var Var))))) (List (Pair Pats Code)); +%% + +merge-dflt : List part-type -> Option part-type -> List part-type; +merge-dflt parts odflt = let + + %% It must be bugged in one way or another... + + %% preppend child branches in case we see a default branch before a normal branch + + preppend : Pat -> List (Pair Pat (List (Pair Var Var))) -> List (Pair Pats Code) -> + part-type -> part-type; + preppend pat vars branches part = case part + | pair p b => (case p | triplet _ lv v => + pair (triplet pat lv (List_concat vars v)) (List_concat branches b)); + + %% append child branches in case we see more than one default branches + + append : Pat -> List (Pair Pat (List (Pair Var Var))) -> List (Pair Pats Code) -> + part-type -> part-type; + append pat vars branches part = case part + | pair p b => (case p | triplet _ lv v => + pair (triplet pat lv (List_concat v vars)) (List_concat b branches)); + +in case parts + | cons part parts => (case part | pair p pp => + (case p | triplet pat _ vars => if_then_else_ (is-dflt pat) + (case odflt + | some dflt => merge-dflt parts (some (append pat vars pp dflt)) + | none => merge-dflt parts (some part)) + (case odflt + %% merge previous default to all branches + | some dflt => cons (preppend pat vars pp dflt) (merge-dflt parts odflt) + | none => cons part (merge-dflt parts odflt)))) + | nil => (case odflt + | some dflt => (cons dflt nil) + | none => nil); + +%% takes some branches and preppend default variable to smaller branches + +adjust-len : List (Pair Pats Code) -> List (Pair Pats Code); +adjust-len branches = let + + max-len : Int; + max-len = let + + ff : Int -> Pair Pats Code -> Int; + ff n branch = case branch + | pair pats _ => if_then_else_ (Int_< n (List_length pats)) + (List_length pats) + (n); + + in List_foldl ff 0 branches; + + preppend-dflt : Int -> Pair Pats Code -> Pair Pats Code; + preppend-dflt n branch = let + + sup : Int -> Pats; + sup n = if_then_else_ (Int_eq n 0) + (nil) + (cons dflt-var (sup (n - 1))); + + in case branch | pair pats code => + pair (List_concat (sup (n - (List_length pats))) pats) code; + +in List_map (preppend-dflt max-len) branches; + +%% +%% reminder +%% part-type = Pair +%% (Triplet +%% Pat (List Var) (List (Pair Pat (List (Pair Var Var))))) +%% (List (Pair Pats Code)); +%% + +compile-case : List Var -> List (Pair Pats Code) -> IO Code; +compile-case subjects branches = let + + subject = (List_nth 0 subjects Var_error); + + parts : IO (List part-type); + parts = do { + ps <- partition-branches branches; + return (merge-dflt ps none); + }; + + translate-sub-pats : List Var -> List (Pair Pat (List (Pair Var Var))) -> List (Pair Pats Code) + -> IO Code; + translate-sub-pats rvars pats-vars branches = let + + recursion : List (Pair Pat (List (Pair Var Var))) -> List (Pair Pats Code) + -> IO Code; + recursion pats-vars branches = let + + sub-pats-vars : IO (List Var); + sub-pats-vars = pattern-sub-pats-vars rvars pats-vars; + + mf : Pair Pat (List (Pair Var Var)) -> Pair Pats Code -> IO (Pair Pats Code); + mf pat-vars branch = case pat-vars + | pair pat vars => let + + sub-pats : IO (List Pat); + sub-pats = pattern-sub-pats pat; + + in do { + sub-pats <- sub-pats; + sub-pats-vars <- sub-pats-vars; + + sub-pats <- return (List_fold2 (lambda o pat var -> + if_then_else_ (is-dflt var) + (o) + (List_concat o (cons pat nil)) + ) nil sub-pats sub-pats-vars); + + return (case branch | pair pats code => + pair (List_concat sub-pats pats) + (wrap-vars (List_map-snd vars) (List_map-fst vars) code)); + }; + + new-branches : IO (List (Pair Pats Code)); + new-branches = do { + nbranches <- io-list (List_map2 mf pats-vars branches); + return (adjust-len nbranches); + }; + + new-subjects : IO (List Var); + new-subjects = do { + sub-pats-vars <- sub-pats-vars; + r <- return (List_concat sub-pats-vars (List_tail subjects)); + + %% As for constructor we remove variable if it is always a default + %% variable without any corresponding sub pattern + + r <- return (List_foldl (lambda o v -> + if_then_else_ (is-dflt v) + (o) + (List_concat o (cons v nil)) + ) nil r); + return r; + }; + + code-or-recurse : List Var -> List (Pair Pats Code) -> IO Code; + code-or-recurse subjects branches = case subjects + | cons _ _ => compile-case subjects branches + | nil => (case branches + | cons branch _ => (case branch + | pair _ code => return code) + | nil => return Code_error); + + in do { + new-subjects <- new-subjects; + new-branches <- new-branches; + code <- code-or-recurse new-subjects new-branches; + return code; + }; + + in recursion pats-vars branches; + + translate-part : part-type -> IO Code; + translate-part branch = case branch + | pair patterns branches => (case patterns + | triplet pat rvars pats-vars => do { + sub-cases <- translate-sub-pats rvars pats-vars branches; + return (quote (_=>_ (uquote pat) (uquote sub-cases))); + }); + + translate : List part-type -> IO Code; + translate parts = do { + branches <- io-list (List_map translate-part parts); + return (Sexp_node (Sexp_symbol "##case_") (cons ( + Sexp_node (Sexp_symbol "_|_") (cons subject branches) + ) nil)); + }; + +in do { + parts <- parts; + r <- translate parts; + return r; +}; + +%%% +%%% The macro we want. +%%% + +rec-case : List Sexp -> IO Sexp; +rec-case args = let + + case0 : List Sexp -> IO Sexp; + case0 args = let + + vars : List Sexp; + vars = case args + | (cons s ss) => get-tup-exprs s + | nil => nil; + + ctors : List (Pair Pats Code); + ctors = case args + | (cons s ss) => get-branches ss + | nil => nil; + + num-vars : IO (List Sexp); + num-vars = let + + vars = gen-vars vars; + + in do { + vars <- vars; + return vars; + }; + + in do { + num-vars <- num-vars; + f <- compile-case num-vars ctors; + r <- return (wrap-vars vars num-vars f); + return r; + }; + + %% Only the Sexp after "_|_" are interesting + + case1 : Sexp -> List Sexp -> IO Sexp; + case1 s ss = if_then_else_ (Sexp_eq (Sexp_symbol "_|_") s) + (case0 ss) + (IO_return Sexp_error); + + err = (lambda _ -> IO_return Sexp_error); + +%% Expecting only one Sexp_node containing a case with arguments + +in (Sexp_dispatch (List_nth 0 args Sexp_error) + case1 err err err err err); + +case_ = macro rec-case;
===================================== samples/list.typer ===================================== @@ -1,6 +1,6 @@ -%% -%% List -%% +%%%%% +%%%%% List +%%%%%
%%%% List type
@@ -52,6 +52,13 @@ mapi f xs = let | cons x xs => cons (f x i) (helper f (i + 1) xs); in helper f 0 xs;
+map2 : (?a -> ?b -> ?c) -> t ?a -> t ?b -> t ?c; +map2 f xs ys = case xs + | nil => nil + | cons x xs => case ys + | nil => nil % error + | cons y ys => cons (f x y) (map2 f xs ys); + foldli : (a : Type) ≡> (b : Type) ≡> (a -> b -> Int -> a) -> a -> t b -> a; foldli f o xs = let helper : (a -> b -> Int -> a) -> Int -> a -> t b -> a; @@ -60,6 +67,14 @@ foldli f o xs = let | cons x xs => helper f (i + 1) (f o x i) xs; in helper f 0 o xs;
+%% Fold 2 List as long as both List are non-empty +fold2 : (?a -> ?b -> ?c -> ?a) -> ?a -> t ?b -> t ?c -> ?a; +fold2 f o xs ys = case xs + | cons x xs => ( case ys + | cons y ys => fold2 f (f o x y) xs ys + | nil => o ) % may be an error + | nil => o; % may or may not be an error + foldr : (a : Type) ≡> (b : Type) ≡> (b -> a -> a) -> t b -> a -> a; foldr f = lambda xs -> lambda i -> case xs | nil => i @@ -99,7 +114,50 @@ remove f l = case l | false => cons x (remove f xs) );
-%% Sorting List +%% Merge two List to a List of Pair +%% Both List must be of same length +merge : t ?a -> t ?b -> t (Pair ?a ?b); +merge xs ys = case xs + | cons x xs => ( case ys + | cons y ys => cons (pair x y) (merge xs ys) + | nil => nil ) % error + | nil => nil; + +%% `Unmerge` a List of Pair +%% The two functions name said it all +map-fst : t (Pair ?a ?b) -> t ?a; +map-fst xs = let + mf : Pair ?a ?b -> ?a; + mf p = case p | pair x _ => x; +in map mf xs; + +map-snd : t (Pair ?a ?b) -> t ?b; +map-snd xs = let + mf : Pair ?a ?b -> ?b; + mf p = case p | pair _ y => y; +in map mf xs; + +%% Is argument List empty? +empty : t ?a -> Bool; +empty xs = Int_eq (length xs) 0; + +%% Move IO outside List (from element to List) +%% (Was helpful for me when translating code that used to not be IO code) +%% (The function's type explain everything) +io-list : t (IO ?a) -> IO (t ?a); +io-list l = let + ff : IO (t ?a) -> IO ?a -> IO (t ?a); + ff o v = do { + o <- o; + v <- v; + IO_return (cons v o); + }; +in do { + l <- (foldl ff (IO_return nil) l); + IO_return (reverse l nil); +}; + +%%%% Sorting List
sort : (a : Type) ≡> (a -> a -> Bool) -> t a -> t a; sort o l = let @@ -121,7 +179,7 @@ sort o l = let
in sortp (head1 l) nil nil (tail l);
-%% Some algo on sorted list +%%%% Some algo on sorted list
sfind : (a : Type) ≡> (a -> a -> Bool) -> (a -> Bool) -> a -> t a -> Option a; sfind o f a l = case l
===================================== tests/case_test.ml ===================================== @@ -31,7 +31,7 @@ let case_decl = let read_file filename = close_in chan; List.rev !lines
-in String.concat "\n" (read_file "samples/case.typer") +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 @@ -41,13 +41,13 @@ let _ = (add_test "CASE MACROS" "case on single variable" (fun () -> f : Bool -> Int; f a = case a | true => 1 - | 0; + | _ => 0;
g : List Int -> Int; g xs = case xs | cons x nil => x | cons x xs => g xs - | 0; + | _ => 0;
va = f true; vb = f false; @@ -69,7 +69,7 @@ let _ = (add_test "CASE MACROS" "case on single variable" (fun () -> | _ -> failure ()) )
-let _ = (add_test "CASE MACROS" "case on Bool" (fun () -> +let _ = (add_test "CASE MACROS" "complex default 1" (fun () -> let dcode = (" f : Bool -> Bool -> Bool -> Int; f a b c = case (a,b,c) @@ -104,7 +104,45 @@ let _ = (add_test "CASE MACROS" "case on Bool" (fun () -> | _ -> failure ()) )
-let _ = (add_test "CASE MACROS" "case on list" (fun () -> +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) @@ -137,7 +175,7 @@ let _ = (add_test "CASE MACROS" "case on list" (fun () -> | _ -> failure ()) )
-let _ = (add_test "CASE MACROS" "3 constant" (fun () -> +let _ = (add_test "CASE MACROS" "3 constant constructor" (fun () -> let dcode = (" type ColorComponent | red @@ -154,7 +192,7 @@ let _ = (add_test "CASE MACROS" "3 constant" (fun () -> | (green,red) => 3 | (green,blue) => 3 | (blue,red) => 2 - | 2; % (blue,green) + | (_,_) => 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; @@ -177,13 +215,17 @@ let _ = (add_test "CASE MACROS" "3 constant" (fun () -> | _ -> failure ()) )
-let _ = (add_test "CASE MACROS" "sub pattern" (fun () -> +(* 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; + | (_,_) => 0;
va = f (cons (some true) nil) (cons (some true) nil); vb = f (cons (some true) (cons (some true) nil)) @@ -193,20 +235,101 @@ let _ = (add_test "CASE MACROS" "sub pattern" (fun () -> 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;" in + let ecode = "va; vb; vc; vd; ve; vf; vg; vh;" in + + let print x = print_string ("\n"^(string_of_int x)) 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 () ) + | [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 () + | (_,_,_,_,_,_,_,_) -> + (print a; print b; print c; print d; + print e; print f; print g; print h; + failure ()) ) + | _ -> failure ()) +) + +let _ = (add_test "CASE MACROS" "sub pattern 2" (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 3" (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 ()) )
View it on GitLab: https://gitlab.com/monnier/typer/compare/9f8cd1898e5d63a86dacef3614f8ad4143c...
Afficher les réponses par date