Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits: ae09719f by Jonathan Graveline at 2018-05-25T03:32:17Z Better name, more function - - - - -
1 changed file:
- samples/list.typer
Changes:
===================================== samples/list.typer ===================================== --- a/samples/list.typer +++ b/samples/list.typer @@ -1,42 +1,101 @@ -% -% Sorted List as a data structure -% -% since 2018-05-14 -% -% (*function prefixed with `s` take sorted list as argument) -% - -% Some more generic first (not only for sorted list) - -List_remove : (a : Type) ≡> (a -> Bool) -> List a -> List a; -List_remove f l = case l +%% +%% List +%% + +%%%% List type + +%% FIXME: "t : ?" should be sufficient but triggers + +t : Type -> Type; +type t (a : Type) + | nil + | cons (hd : a) (tl : t a); + +%%%% List functions + +length : (a : Type) ≡> t a -> Int; +length xs = case xs + | nil => 0 + | cons hd tl => + (1 + (length tl)); + +%% ML's typical `head` function is not total, so can't be defined +%% as-is in Typer. There are several workarounds: +%% - Provide a default value : `a -> t a -> a`; +%% - Disallow problem case : `(l : t a) -> (l != nil) -> a`; +%% - Return an Option/Error +head1 : (a : Type) ≡> t a -> Option a; +head1 xs = case xs + | nil => none + | cons hd tl => some hd; + +head : (a : Type) ≡> t a -> Option a; +head xs = case xs + | cons x _ => some x + | nil => none; + +tail : (a : Type) ≡> t a -> t a; +tail xs = case xs | nil => nil - | cons x xs => ( case (f x) - | true => List_remove f xs - | false => cons x (List_remove f xs) - ); + | cons hd tl => tl; + +map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> t a -> t b; +map f = lambda xs -> case xs + | nil => nil + | cons x xs => cons (f x) (map f xs); + +foldr : (a : Type) ≡> (b : Type) ≡> (b -> a -> a) -> t b -> a -> a; +foldr f = lambda xs -> lambda i -> case xs + | nil => i + | cons x xs => f x (foldr f xs i); + +find : (a : Type) ≡> (a -> Bool) -> t a -> Option a; +find f = lambda xs -> case xs + | nil => none + | cons x xs => case f x | true => some x | false => find f xs;
-List_nth : Int -> List ?a -> ?a -> ?a; -List_nth = lambda n -> lambda xs -> lambda d -> case xs +nth : (a : Type) ≡> Int -> t a -> a -> a; +nth = lambda n -> lambda xs -> lambda d -> case xs | nil => d | cons x xs => case Int_<= n 0 | true => x - | false => List_nth (n - 1) xs d; + | false => nth (n - 1) xs d;
-%% take a function for ordering +reverse : (a : Type) ≡> t a -> t a -> t a; +reverse l t = case l + | nil => t + | cons hd tl => reverse tl (cons hd t);
-List_sort : (a : Type) ≡> (a -> a -> Bool) -> List a -> List a; -List_sort o l = let +concat : (a : Type) ≡> t a -> t a -> t a; +concat l t = reverse (reverse l nil) t;
- sortp : Option a -> List a -> List a -> List a -> List a; +foldl : (a : Type) ≡> (b : Type) ≡> (a -> b -> a) -> a -> t b -> a; +foldl f i xs = case xs + | nil => i + | cons x xs => foldl f (f i x) xs; + +remove : (a : Type) ≡> (a -> Bool) -> t a -> t a; +remove f l = case l + | nil => nil + | cons x xs => ( case (f x) + | true => remove f xs + | false => cons x (remove f xs) + ); + +%% Sorting List + +sort : (a : Type) ≡> (a -> a -> Bool) -> t a -> t a; +sort o l = let + + sortp : Option a -> t a -> t a -> t a -> t a; sortp p lt gt l = case p | none => nil | some (pp) => ( case l | nil => ( let - ltp : List a; ltp = sortp (List_head1 lt) nil nil (List_tail lt); - gtp : List a; gtp = sortp (List_head1 gt) nil nil (List_tail gt); - in List_concat ltp (cons pp gtp) + ltp : t a; ltp = sortp (head1 lt) nil nil (tail lt); + gtp : t a; gtp = sortp (head1 gt) nil nil (tail gt); + in concat ltp (cons pp gtp) ) | cons x xs => ( case (o x pp) | true => sortp p lt (cons x gt) xs @@ -44,101 +103,54 @@ List_sort o l = let ) );
-in sortp (List_head1 l) nil nil (List_tail l); +in sortp (head1 l) nil nil (tail l);
%% Some algo on sorted list
-sList_find : (a : Type) ≡> (a -> a -> Bool) -> (a -> Bool) -> a -> List a -> Option a; -sList_find o f a l = case l +sfind : (a : Type) ≡> (a -> a -> Bool) -> (a -> Bool) -> a -> t a -> Option a; +sfind o f a l = case l | nil => none | cons x xs => ( case (f x) | true => some x | false => ( case (o x a) - | false => sList_find o f a xs + | false => sfind o f a xs | true => none ) );
-sList_all : (a : Type) ≡> (a -> Bool) -> List a -> List a; -sList_all f l = case l +sall : (a : Type) ≡> (a -> Bool) -> t a -> t a; +sall f l = case l | nil => nil | cons x xs => ( case (f x) - | true => cons x (sList_all f xs) - | false => sList_all f xs + | true => cons x (sall f xs) + | false => sall f xs );
-sList_exist : (a : Type) ≡> (a -> a -> Bool) -> (a -> Bool) -> a -> List a -> Bool; -sList_exist o f a l = case (sList_find o f a l) +sexist : (a : Type) ≡> (a -> a -> Bool) -> (a -> Bool) -> a -> t a -> Bool; +sexist o f a l = case (sfind o f a l) | none => false | some _ => true;
-sList_insert : (a : Type) ≡> (a -> a -> Bool) -> a -> List a -> List a; -sList_insert o a l = case l +sinsert : (a : Type) ≡> (a -> a -> Bool) -> a -> t a -> t a; +sinsert o a l = case l | nil => cons a l | cons x xs => ( case (o x a) | true => cons a l - | false => cons x (sList_insert o a xs) + | false => cons x (sinsert o a xs) );
-sList_up : (a : Type) ≡> (a -> a -> Bool) -> a -> List a -> List a; -sList_up o a l = case l +ssup : (a : Type) ≡> (a -> a -> Bool) -> a -> t a -> t a; +ssup o a l = case l | nil => nil | cons x xs => ( case (o x a) | true => l - | false => sList_up o a xs + | false => ssup o a xs );
-sList_low : (a : Type) ≡> (a -> a -> Bool) -> a -> List a -> List a; -sList_low o a l = case l +sinf : (a : Type) ≡> (a -> a -> Bool) -> a -> t a -> t a; +sinf o a l = case l | nil => nil | cons x xs => ( case (o x a) | true => nil - | false => cons x (sList_low o a xs) + | false => cons x (sinf o a xs) ); - -% -% Some predef for built-in type -% - -% sorted list for Int - -sInt_order : Int -> Int -> Bool; -sInt_order m n = Int_> m n; - -sInt_eq : Int -> Int -> Bool; -sInt_eq m n = Int_eq m n; - -Int_sort = List_sort sInt_order; - -sInt_find n = sList_find sInt_order (sInt_eq n); - -sInt_exist n = sList_exist sInt_order (sInt_eq n); - -sInt_insert n = sList_insert sInt_order n; - -sInt_up n = sList_up sInt_order n; - -sInt_low n = sList_low sInt_order n; - -% sorted list for Float - -sFloat_order : Float -> Float -> Bool; -sFloat_order m n = Float_> m n; - -sFloat_eq : Float -> Float -> Bool; -sFloat_eq m n = Float_eq m n; - -Float_sort = List_sort sFloat_order; - -sFloat_find n = sList_find sFloat_order (sFloat_eq n); - -sFloat_exist n = sList_exist sFloat_order (sFloat_eq n); - -sFloat_insert n = sList_insert sFloat_order n; - -sFloat_up n = sList_up sFloat_order n; - -sFloat_low n = sList_low sFloat_order n; - -% test_list : List Float; -% test_list = cons 9.0 (cons 1.0 (cons 8.0 (cons 2.0 (cons 7.0 (cons 3.0 (cons 6.0 (cons 4.0 (cons 5.0 nil))))))));
View it on GitLab: https://gitlab.com/monnier/typer/commit/ae09719f13815afdebff77b4f73ae5ed362f...