Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits: 83f93ecc by Jonathan Graveline at 2018-05-14T22:13:28Z First draft - - - - -
1 changed file:
- + samples/list.typer
Changes:
===================================== samples/list.typer ===================================== --- /dev/null +++ b/samples/list.typer @@ -0,0 +1,144 @@ +% +% 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 + | nil => nil + | cons x xs => ( case (f x) + | true => List_remove f xs + | false => cons x (List_remove f xs) + ); + +List_nth : Int -> List ?a -> ?a -> ?a; +List_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; + +%% take a function for ordering + +List_sort : (a : Type) ≡> (a -> a -> Bool) -> List a -> List a; +List_sort o l = let + + sortp : Option a -> List a -> List a -> List a -> List 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) + ) + | cons x xs => ( case (o x pp) + | true => sortp p lt (cons x gt) xs + | false => sortp p (cons x lt) gt xs + ) + ); + +in sortp (List_head1 l) nil nil (List_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 + | nil => none + | cons x xs => ( case (f x) + | true => some x + | false => ( case (o x a) + | false => sList_find o f a xs + | true => none + ) + ); + +sList_all : (a : Type) ≡> (a -> Bool) -> List a -> List a; +sList_all f l = case l + | nil => nil + | cons x xs => ( case (f x) + | true => cons x (sList_all f xs) + | false => sList_all 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) + | none => false + | some _ => true; + +sList_insert : (a : Type) ≡> (a -> a -> Bool) -> a -> List a -> List a; +sList_insert 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) + ); + +sList_up : (a : Type) ≡> (a -> a -> Bool) -> a -> List a -> List a; +sList_up o a l = case l + | nil => nil + | cons x xs => ( case (o x a) + | true => l + | false => sList_up o a xs + ); + +sList_low : (a : Type) ≡> (a -> a -> Bool) -> a -> List a -> List a; +sList_low o a l = case l + | nil => nil + | cons x xs => ( case (o x a) + | true => nil + | false => cons x (sList_low 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/83f93ecc58be52d7d1c449326f033fb35581...