Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits: 26df3634 by Jonathan Graveline at 2018-05-25T03:33:03Z Better name - - - - -
1 changed file:
- samples/myers.typer
Changes:
===================================== samples/myers.typer ===================================== --- a/samples/myers.typer +++ b/samples/myers.typer @@ -4,29 +4,20 @@ % since 2018-05-14 %
-Myers : Type -> Type; -type Myers (a : Type) +%% We could replace mnil and mcons by nil and cons +%% when load and list.typer are ready +t : Type -> Type; +type t (a : Type) | mnil - | mcons (data : a) (link1 : (Myers a)) (i : Int) (link2 : (Myers a)); - -% client shouldn't use next two definition - -type _MyersPatternHelper (a : Type) - | _pat1 (idx : Int) (data : a) (link1 : Myers a) (i : Int) (link2 : Myers a) - | _pat2 (idx : Int); - -_pattern_helper : (a : Type) ≡> Int -> Myers a -> _MyersPatternHelper a; -_pattern_helper n l = case l - | mnil => _pat2 n - | mcons a l1 i l2 => _pat1 n a l1 i l2; + | mcons (data : a) (link1 : (t a)) (i : Int) (link2 : (t a));
% Contrary to Myers's presentation, we index from the top of the stack, % and we don't store the total length but the "skip distance" instead. % This makes `cons' slightly faster, and better matches our use for % debruijn environments.
-Myers_cons : (a : Type) ≡> a -> Myers a -> Myers a; -Myers_cons x l = case l +cons : (a : Type) ≡> a -> t a -> t a; +cons x l = case l | mcons _ _ s1 l1 => ( case l1 | mcons _ _ s2 l2 => ( case (Int_>= s1 s2) | true => mcons x l (s1 + s2 + 1) l2 @@ -36,63 +27,74 @@ Myers_cons x l = case l ) | _ => mcons x l 1 l;
-Myers_car : (a : Type) ≡> Myers a -> Option a; -Myers_car l = case l +car : (a : Type) ≡> t a -> Option a; +car l = case l | mnil => none | mcons x _ _ _ => some x;
-Myers_cdr : (a : Type) ≡> Myers a -> Myers a; -Myers_cdr l = case l +cdr : (a : Type) ≡> t a -> t a; +cdr l = case l | mnil => mnil | mcons _ l _ _ => l;
-Myers_case : (a : Type) ≡> (b : Type) ≡> Myers a -> b -> (a -> Myers a -> b) -> b; -Myers_case l n c = case l +match : (a : Type) ≡> (b : Type) ≡> t a -> b -> (a -> t a -> b) -> b; +match l n c = case l | mnil => n | mcons x l _ _ => c x l;
-Myers_empty : (a : Type) ≡> Myers a -> Bool; -Myers_empty l = case l +empty : (a : Type) ≡> t a -> Bool; +empty l = case l | mnil => true | _ => false;
-Myers_nthcdr : (a : Type) ≡> Int -> Myers a -> Myers a; -Myers_nthcdr n l = if_then_else_ (Int_eq n 0) l +nthcdr : (a : Type) ≡> Int -> t a -> t a; +nthcdr n l = if_then_else_ (Int_eq n 0) l ( case l | mnil => mnil | mcons _ l1 s l2 => ( case (Int_>= n s) - | true => Myers_nthcdr (n - s) l2 - | false => Myers_nthcdr (n - 1) l1 + | true => nthcdr (n - s) l2 + | false => nthcdr (n - 1) l1 ) );
-Myers_nth : (a : Type) ≡> Int -> Myers a -> Option a; -Myers_nth n l = Myers_car (Myers_nthcdr n l); +nth : (a : Type) ≡> Int -> t a -> Option a; +nth n l = car (nthcdr n l);
% While `nth` is O(log N), `set_nth` is O(N)! :-(
-Myers_set_nth : (a : Type) ≡> Int -> a -> Myers a -> Myers a; -Myers_set_nth n v l = case (_pattern_helper n l) +set_nth : (a : Type) ≡> Int -> a -> t a -> t a; +set_nth n v l = let + + type Helper (a : Type) + | pat1 (idx : Int) (data : a) (link1 : t a) (i : Int) (link2 : t a) + | pat2 (idx : Int); + + helper : (a : Type) ≡> Int -> t a -> Helper a; + helper n l = case l + | mnil => pat2 n + | mcons a l1 i l2 => pat1 n a l1 i l2; + + in case (helper n l)
- | _pat1 n vp cdr s tail => if_then_else_ (Int_eq n 0) + | pat1 n vp cdr s tail => if_then_else_ (Int_eq n 0) ( mcons v cdr s tail ) - ( Myers_cons vp (Myers_set_nth (n - 1) v cdr) ) + ( cons vp (set_nth (n - 1) v cdr) )
% We can't set_nth past the end in general because we'd need to % magically fill the intermediate entries with something of the right type. % But we *can* set_nth just past the end.
- | _pat2 n => if_then_else_ (Int_eq n 0) + | pat2 n => if_then_else_ (Int_eq n 0) ( mcons v mnil 1 mnil ) ( l ); % should throw an error here!
% This operation would be more efficient using Myers's choice of keeping % the length (instead of the skip-distance) in each node.
-Myers_length : (a : Type) ≡> Myers a -> Int; -Myers_length l = let +length : (a : Type) ≡> t a -> Int; +length l = let
- lengthp : Myers a -> Int -> Int; + lengthp : t a -> Int -> Int; lengthp l n = case l | mnil => n | mcons _ _ s l => lengthp l (s + n); @@ -103,11 +105,11 @@ in lengthp l 0; % "Binary" search, assuming the list is "sorted" (i.e. all elements after % this one also return true).
-Myers_find : (a : Type) ≡> (a -> Bool) -> Myers a -> Option a; -Myers_find p l = let +find : (a : Type) ≡> (a -> Bool) -> t a -> Option a; +find p l = let
- find1 : Myers a -> Option a; - find2 : Myers a -> Myers a -> Option a; + find1 : t a -> Option a; + find2 : t a -> t a -> Option a;
find2 l1 l2 = case l2 | mcons x l1 _ l2 => ( case (p x) @@ -129,16 +131,16 @@ in find1 l; % "Binary" search, assuming the list is "sorted" (i.e. all elements after % this one also return true).
-Myers_findcdr : (a : Type) ≡> (a -> Bool) -> Myers a -> Myers a; -Myers_findcdr p l = let +findcdr : (a : Type) ≡> (a -> Bool) -> t a -> t a; +findcdr p l = let
- maybev : Option (Myers a) -> Myers a; + maybev : Option (t a) -> t a; maybev ov = case ov | none => mnil | some l => l;
- findcdr1 : Option (Myers a) -> Myers a -> Myers a; - findcdr2 : Option (Myers a) -> Myers a -> Myers a -> Myers a; + findcdr1 : Option (t a) -> t a -> t a; + findcdr2 : Option (t a) -> t a -> t a -> t a;
findcdr2 last l1 l2 = case l2 | mcons x l1p _ l2p => ( case (p x) @@ -156,28 +158,28 @@ Myers_findcdr p l = let
in findcdr1 none l;
-Myers_fold_left : (a : Type) ≡> (b : Type) ≡> (b -> a -> b) -> b -> Myers a -> b; -Myers_fold_left f i l = case l +fold_left : (a : Type) ≡> (b : Type) ≡> (b -> a -> b) -> b -> t a -> b; +fold_left f i l = case l | mnil => i - | mcons x l _ _ => Myers_fold_left f (f i x) l; + | mcons x l _ _ => fold_left f (f i x) l;
-Myers_fold_right : (a : Type) ≡> (b : Type) ≡> (a -> b -> b) -> Myers a -> b -> b; -Myers_fold_right f l i = case l +fold_right : (a : Type) ≡> (b : Type) ≡> (a -> b -> b) -> t a -> b -> b; +fold_right f l i = case l | mnil => i - | mcons x l _ _ => f x (Myers_fold_right f l i); + | mcons x l _ _ => f x (fold_right f l i);
-Myers_map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> Myers a -> Myers b; -Myers_map f l = let +map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> t a -> t b; +map f l = let
- fp : a -> Myers b -> Myers b; - fp x lp = Myers_cons (f x) lp; + fp : a -> t b -> t b; + fp x lp = cons (f x) lp;
-in Myers_fold_right fp l mnil; +in fold_right fp l mnil;
-Myers_iteri : (a : Type) ≡> (Int -> a -> Unit) -> Myers a -> Int; -Myers_iteri f l = let +iteri : (a : Type) ≡> (Int -> a -> Unit) -> t a -> Int; +iteri f l = let
fp : (Int -> a -> Int); fp i x = let _ = (f i x); in i + 1;
-in Myers_fold_left fp 0 l; +in fold_left fp 0 l;
View it on GitLab: https://gitlab.com/monnier/typer/commit/26df3634d45c596755335dab2dc7c1cf048b...