Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits: f0d1072f by Jonathan Graveline at 2018-05-14T22:15:06Z First draft - - - - -
1 changed file:
- + samples/myers.typer
Changes:
===================================== samples/myers.typer ===================================== --- /dev/null +++ b/samples/myers.typer @@ -0,0 +1,183 @@ +% +% Adaptation of Myers list from ocaml file `myers.ml` +% +% since 2018-05-14 +% + +Myers : Type -> Type; +type Myers (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; + +% 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 + | mcons _ _ s1 l1 => ( case l1 + | mcons _ _ s2 l2 => ( case (Int_>= s1 s2) + | true => mcons x l (s1 + s2 + 1) l2 + | false => mcons x l 1 l + ) + | _ => mcons x l 1 l + ) + | _ => mcons x l 1 l; + +Myers_car : (a : Type) ≡> Myers a -> Option a; +Myers_car l = case l + | mnil => none + | mcons x _ _ _ => some x; + +Myers_cdr : (a : Type) ≡> Myers a -> Myers a; +Myers_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 + | mnil => n + | mcons x l _ _ => c x l; + +Myers_empty : (a : Type) ≡> Myers a -> Bool; +Myers_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 + ( case l + | mnil => mnil + | mcons _ l1 s l2 => ( case (Int_>= n s) + | true => Myers_nthcdr (n - s) l2 + | false => Myers_nthcdr (n - 1) l1 + ) + ); + +Myers_nth : (a : Type) ≡> Int -> Myers a -> Option a; +Myers_nth n l = Myers_car (Myers_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) + + | _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) ) + + % 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) + ( 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 + + lengthp : Myers a -> Int -> Int; + lengthp l n = case l + | mnil => n + | mcons _ _ s l => lengthp l (s + n); + +in lengthp l 0; + +% Find the first element for which the predicate `p' is true. +% "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 + + find1 : Myers a -> Option a; + find2 : Myers a -> Myers a -> Option a; + + find2 l1 l2 = case l2 + | mcons x l1 _ l2 => ( case (p x) + | false => find2 l1 l2 + | true => find1 l + ) + | _ => find1 l; + + find1 l = case l + | mnil => none + | mcons x l1 _ l2 => ( case (p x) + | true => some x + | false => find2 l1 l2 + ); + +in find1 l; + +% Find the last node for which the predicate `p' is false. +% "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 + + maybev : Option (Myers a) -> Myers 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; + + findcdr2 last l1 l2 = case l2 + | mcons x l1p _ l2p => ( case (p x) + | false => findcdr2 (some l2) l1p l2p + | true => findcdr1 last l1 + ) + | _ => findcdr1 last l1; + + findcdr1 last l = case l + | mnil => maybev last + | mcons x l1 _ l2 => ( case (p x) + | true => maybev last + | false => findcdr2 (some l) l1 l2 + ); + +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 + | mnil => i + | mcons x l _ _ => Myers_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 + | mnil => i + | mcons x l _ _ => f x (Myers_fold_right f l i); + +Myers_map : (a : Type) ≡> (b : Type) ≡> (a -> b) -> Myers a -> Myers b; +Myers_map f l = let + + fp : a -> Myers b -> Myers b; + fp x lp = Myers_cons (f x) lp; + +in Myers_fold_right fp l mnil; + +Myers_iteri : (a : Type) ≡> (Int -> a -> Unit) -> Myers a -> Int; +Myers_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;
View it on GitLab: https://gitlab.com/monnier/typer/commit/f0d1072fcad40af573207eb09c999ace99b2...
Afficher les réponses par date