[Git][monnier/typer][graveline] Better name, more function - Typer

24 Mai 2018

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...
-- 
View it on GitLab: https://gitlab.com/monnier/typer/commit/ae09719f13815afdebff77b4f73ae5ed362f...
You're receiving this email because of your account on gitlab.com.



    