Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits:
588c02a6 by Jonathan Graveline at 2018-05-26T15:23:50Z
Sexp_print for debugging
- - - - -
1 changed file:
- btl/builtins.typer
Changes:
=====================================
btl/builtins.typer
=====================================
--- a/btl/builtins.typer
+++ b/btl/builtins.typer
@@ -153,6 +153,8 @@ String_sub = Built-in "String.sub" : String -> Int -> Int -> String;
Sexp_eq = Built-in "Sexp.=" : Sexp -> Sexp -> Bool;
+Sexp_print = Built-in "Sexp.print" : Sexp -> Sexp;
+
%% -----------------------------------------------------
%% List
%% -----------------------------------------------------
View it on GitLab: https://gitlab.com/monnier/typer/commit/588c02a68e47e84f56cb000743a0cbdb3e7…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/588c02a68e47e84f56cb000743a0cbdb3e7…
You're receiving this email because of your account on gitlab.com.
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/26df3634d45c596755335dab2dc7c1cf048…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/26df3634d45c596755335dab2dc7c1cf048…
You're receiving this email because of your account on gitlab.com.
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/ae09719f13815afdebff77b4f73ae5ed362…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/ae09719f13815afdebff77b4f73ae5ed362…
You're receiving this email because of your account on gitlab.com.
Stefan pushed to branch graveline at Stefan / Typer
Commits:
aaa4c5dc by Stefan Monnier at 2018-05-18T21:10:47Z
Add missing parts of last commit
- - - - -
4 changed files:
- samples/bool.typer
- − samples/bugs.typer
- samples/empty.typer
- src/opslexp.ml
Changes:
=====================================
samples/bool.typer
=====================================
--- a/samples/bool.typer
+++ b/samples/bool.typer
@@ -25,20 +25,22 @@ if_then_else_
%% FIXME: Type annotations should not be needed below.
not : t -> t;
-not x = if x then false else true;
+%% FIXME: We use braces here to delay parsing, otherwise the if/then/else
+%% part of the grammar declared above is not yet taken into account.
+not x = { if x then false else true };
or : t -> t -> t;
-or x y = if x then x else y;
+or x y = { if x then x else y };
and : t -> t -> t;
-and x y = if x then y else x;
+and x y = { if x then y else x };
xor : t -> t -> t;
-xor x y = if x then (not y) else y;
+xor x y = { if x then (not y) else y };
%% FIXME: Can't use ?a because that is generalized to be universe-polymorphic,
%% which we don't support in `load` yet.
fold : t -> (a : Type) ≡> a -> a -> a;
-fold x t e = if x then t else e;
+fold x t e = { if x then t else e};
=====================================
samples/bugs.typer deleted
=====================================
--- a/samples/bugs.typer
+++ /dev/null
=====================================
samples/empty.typer
=====================================
--- a/samples/empty.typer
+++ b/samples/empty.typer
@@ -0,0 +1 @@
+%%% empty.typer --- Yay! An empty library!
=====================================
src/opslexp.ml
=====================================
--- a/src/opslexp.ml
+++ b/src/opslexp.ml
@@ -958,8 +958,8 @@ let ctx2tup ctx nctx =
types)
SMap.empty),
cons_label),
- List.map (fun (oname, t)
- -> (P.Aimplicit, Var (maybev oname, offset)))
+ List.mapi (fun i (oname, t)
+ -> (P.Aimplicit, Var (maybev oname, offset - i - 1)))
types)
| (DB.CVlet (oname, LetDef (_, e), t, _) :: blocs)
-> Let (loc, [(maybev oname, mkSusp e (S.shift 1), t)],
View it on GitLab: https://gitlab.com/monnier/typer/commit/aaa4c5dccf508240be9afda1615bff78857…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/aaa4c5dccf508240be9afda1615bff78857…
You're receiving this email because of your account on gitlab.com.