[Git][monnier/typer][graveline] New data structure "Table" (some kind of tree) (work in progress)
Jonathan Graveline pushed to branch graveline at Stefan / Typer Commits: 9156b075 by Jonathan Graveline at 2018-07-02T21:08:22Z New data structure "Table" (some kind of tree) (work in progress) - - - - - 3 changed files: - samples/case.typer - + samples/table.typer - tests/case_test.ml Changes: ===================================== samples/case.typer ===================================== --- a/samples/case.typer +++ b/samples/case.typer @@ -3,6 +3,11 @@ %%% %%% (pattern matching) %%% +%%% TODO : +%%% - Handle named constructor variable +%%% - Find a way to get no error when there's no default case +%%% and user pattern is exhaustive +%%% %% %% Match every variable in each pattern with a list of VarTest. @@ -362,8 +367,13 @@ pattern_to_sexp vars pats = let | some fail => (quote (##case_ (_|_ (uquote var) (_=>_ (uquote ctor) (uquote succ)) (_=>_ _ (uquote fail))))) - | none => (quote (##case_ (_|_ (uquote var) - (_=>_ (uquote ctor) (uquote succ))))); + | none => % if_then_else_ (Sexp_eq ctor (Sexp_symbol "_")) + (quote (##case_ (_|_ (uquote var) + (_=>_ (uquote ctor) (uquote succ))))); + % "?" doesn't seem to help + % (quote (##case_ (_|_ (uquote var) + % (_=>_ (uquote ctor) (uquote succ))) + % (_=>_ _ ?))); push : Int -> List Sexp -> List Sexp; push n vars = if_then_else_ (Int_<= n 1) ===================================== samples/table.typer ===================================== --- /dev/null +++ b/samples/table.typer @@ -0,0 +1,325 @@ +%%% +%%% Table as a B tree +%%% + +%% +%% Just a Pair type returned by some function and use in the tree. +%% Prefer use of "data" and "key" for access in case the internal change. +%% + +type Vec2 (a : Type) (b : Type) + | vec2 a b; + +%% +%% Access function +%% + +data : (a : Type) ≡> (k : Type) ≡> Vec2 a k -> a; + +data e = case e + | vec2 d _ => d; + +key : (a : Type) ≡> (k : Type) ≡> Vec2 a k -> k; + +key e = case e + | vec2 _ k => k; + +%% +%% a : element type +%% k : key type +%% s : size as a base of 2 (e.g. s = 5 <=> size = 32) +%% c : compare function (for key) +%% h : hash function (for key) +%% +%% Many things are specified but there will be +%% some predefined table at the end of this file. +%% + +TableData : Type -> Type -> Type; + +type TableData (a : Type) (k : Type) + | table-node (left : TableData a k) (right : TableData a k) + | table-leaf (elems : List (Vec2 a k)) + | table-nil; + +type Table (a : Type) (k : Type) + | table (s : Int) (c : k -> k -> Bool) (h : k -> Int) (t : TableData a k); + +%% +%% fold left in an unspecified order +%% + +foldl : (b : Type) ≡> (a : Type) ≡> (k : Type) ≡> + (b -> (Vec2 a k) -> b) -> b -> Table a k -> b; + +foldl f o t = let + + helper : (b : Type) ≡> (a : Type) ≡> (k : Type) ≡> + (b -> (Vec2 a k) -> b) -> b -> TableData a k -> b; + + helper f o t = case t + | table-node l r => ( let + o1 = helper f o l; + o2 = helper f o1 r; + in o2 ) + | table-leaf xs => List_foldl f o xs + | table-nil => o; + +in case t + | table _ _ _ t => helper f o t; + +%% +%% This function is for internal use only (used in shrink) +%% + +tabledata-length : (a : Type) ≡> (k : Type) ≡> Int -> TableData a k -> Int; +tabledata-length o tree = case tree + | table-node l r => ( let + o1 = tabledata-length o l; + o2 = tabledata-length o1 r; + in o2 ) + | table-leaf xs => o + (List_length xs) + | table-nil => o; + +%% +%% After many "insert" and "remove" there may be useless node which +%% are still in the tree. Use "shrink" to remove useless node. +%% +%% (there may be a way to do it efficiently within "remove") +%% + +shrink : (a : Type) ≡> (k : Type) ≡> Table a k -> Table a k; +shrink tree = let + + helper : (a : Type) ≡> (k : Type) ≡> TableData a k -> TableData a k; + helper tree = case tree + | table-node l r => ( let + l1 = helper l; + r1 = helper r; + l2 = if_then_else_ (Int_eq (tabledata-length 0 l1) 0) + (table-nil) (l); + r2 = if_then_else_ (Int_eq (tabledata-length 0 r1) 0) + (table-nil) (r); + in table-node l2 r2 ) + | table-leaf xs => if_then_else_ (Int_eq (List_length xs) 0) + (table-nil) (table-leaf xs) + | table-nil => table-nil; + +in case tree + | table s c h t => table s c h (helper t); + +%% +%% Get the number of element in the tree +%% + +length t = let + fold-fun len _ = len + 1; +in foldl fold-fun 0 t; + +%% +%% Is the tree empty? +%% + +is-empty t = Int_eq (length t) 0; + +%% +%% Insert a data/key pair (vec2) in the tree +%% + +insert : (a : Type) ≡> (k : Type) ≡> a -> k -> Table a k -> Table a k; +insert elem key tree = let + + choose-fun : (k -> k -> Bool) -> (Vec2 a k) -> (Vec2 a k) -> (Vec2 a k); + choose-fun comp p0 p1 = case p0 + | vec2 e0 k0 => ( case p1 + | vec2 e1 k1 => if_then_else_ (comp k1 k0) (p1) (p0) + ); + + is-key-in : (k -> k -> Bool) -> k -> List (Vec2 a k) -> Bool; + is-key-in comp k0 xs = let + + fold-fun : Bool -> (Vec2 a k) -> Bool; + fold-fun b x = ( case b + | true => true + | false => ( case x + | vec2 _ k1 => comp k0 k1 + ) + ); + + in List_foldl fold-fun false xs; + + helper : Int -> Int -> (k -> k -> Bool) -> TableData a k -> TableData a k; + + helper count hash comp tree = case tree + | table-node l r => if_then_else_ (Int_eq (Int_and hash 1) 0) + (table-node (helper (count - 1) (Int_lsr hash 1) comp l) r) + (table-node l (helper (count - 1) (Int_lsr hash 1) comp r)) + | table-leaf elems => if_then_else_ (is-key-in comp key elems) + (table-leaf (List_foldl (lambda es e -> + (cons (choose-fun comp e (vec2 elem key)) es)) nil elems)) + (table-leaf (cons (vec2 elem key) elems)) + | table-nil => if_then_else_ (Int_eq count 0) + (table-leaf (cons (vec2 elem key) nil)) + (helper count hash comp + (table-node table-nil table-nil)); + +in case tree + | table s c h t => table s c h (helper s (Int_mod (h key) (Int_lsl 1 s)) c t); + +%% +%% Remove a data/key pair associated with a given key from the tree. +%% + +remove : (a : Type) ≡> (k : Type) ≡> k -> Table a k -> Table a k; + +remove key tree = let + + to-remove : (k -> k -> Bool) -> (Vec2 a k) -> Bool; + to-remove comp elem = case elem + | vec2 _ key0 => comp key key0; + + helper : Int -> Int -> (k -> k -> Bool) -> TableData a k -> TableData a k; + + helper count hash comp tree = case tree + | table-node l r => if_then_else_ (Int_eq (Int_and hash 1) 0) + (table-node (helper (count - 1) (Int_lsr hash 1) comp l) r) + (table-node l (helper (count - 1) (Int_lsr hash 1) comp r)) + | table-leaf elems => (table-leaf (List_foldl (lambda es e -> + (if_then_else_ (to-remove comp e) (es) (cons e es)) + ) nil elems)) + | table-nil => table-nil; + +in case tree + | table s c h t => table s c h (helper s (Int_mod (h key) (Int_lsl 1 s)) c t); + +%% +%% Change a data associated with a given key +%% +%% Should be faster to use this than "remove" and then "insert" +%% + +update : (a : Type) ≡> (k : Type) ≡> a -> k -> Table a k -> Table a k; + +update elem key tree = let + + to-update : (k -> k -> Bool) -> (Vec2 a k) -> Bool; + to-update comp elem = case elem + | vec2 _ key0 => comp key key0; + + helper : Int -> Int -> (k -> k -> Bool) -> TableData a k -> TableData a k; + + helper count hash comp tree = case tree + | table-node l r => if_then_else_ (Int_eq (Int_and hash 1) 0) + (table-node (helper (count - 1) (Int_lsr hash 1) comp l) r) + (table-node l (helper (count - 1) (Int_lsr hash 1) comp r)) + | table-leaf elems => (table-leaf (List_foldl (lambda es e -> + (if_then_else_ (to-update comp e) (cons (vec2 elem key) es) (cons e es)) + ) nil elems)) + | table-nil => table-nil; + +in case tree + | table s c h t => table s c h (helper s (Int_mod (h key) (Int_lsl 1 s)) c t); + +%% +%% Is there a data associated with key in the tree? +%% + +member : (a : Type) ≡> (k : Type) ≡> k -> Table a k -> Bool; +member key tree = let + + searched : (k -> k -> Bool) -> (Vec2 a k) -> Bool; + searched comp elem = case elem + | vec2 _ key0 => comp key key0; + + search-fun : (k -> k -> Bool) -> Bool -> Vec2 a k -> Bool; + search-fun comp b e = if_then_else_ b true (searched comp e); + + helper : Int -> Int -> (k -> k -> Bool) -> TableData a k -> Bool; + + helper count hash comp tree = case tree + | table-node l r => if_then_else_ (Int_eq (Int_and hash 1) 0) + (helper (count - 1) (Int_lsr hash 1) comp l) + (helper (count - 1) (Int_lsr hash 1) comp r) + | table-leaf elems => (List_foldl (search-fun comp) false elems) + | table-nil => false; + +in case tree + | table s c h t => helper s (Int_mod (h key) (Int_lsl 1 s)) c t; + +%% +%% Find a data/key pair in the tree and return it +%% +%% You should then use "data" or "key" to access value in the pair +%% + +find : (a : Type) ≡> (k : Type) ≡> k -> Table a k -> Option (Vec2 a k); + +find key tree = let + + searched : (k -> k -> Bool) -> (Vec2 a k) -> Bool; + searched comp elem = case elem + | vec2 _ key0 => comp key key0; + + search : (k -> k -> Bool) -> List (Vec2 a k) -> Option (Vec2 a k); + search comp xs = case xs + | cons x xs => if_then_else_ (searched comp x) (some x) (search comp xs) + | nil => none; + + helper : Int -> Int -> (k -> k -> Bool) -> TableData a k -> Option (Vec2 a k); + + helper count hash comp tree = case tree + | table-node l r => if_then_else_ (Int_eq (Int_and hash 1) 0) + (helper (count - 1) (Int_lsr hash 1) comp l) + (helper (count - 1) (Int_lsr hash 1) comp r) + | table-leaf elems => search comp elems + | table-nil => none; + +in case tree + | table s c h t => helper s (Int_mod (h key) (Int_lsl 1 s)) c t; + +%% +%% Find a data/key pair in the tree and return the data only +%% + +at : (a : Type) ≡> (k : Type) ≡> k -> Table a k -> Option a; + +at key tree = case (find key tree) + | some x => some (data x) + | none => none; + +%% +%% An empty tree with a key compare function and a key hash function as argument +%% + +empty : (a : Type) ≡> (k : Type) ≡> (k -> k -> Bool) -> (k -> Int) -> Table a k; +empty comp-fun hash-fun = table 8 comp-fun hash-fun table-nil; + +%%% +%%% Test helper and default definition will follow +%%% + +int-comp : Int -> Int -> Bool; +int-comp x y = Int_eq x y; + +int-hash : Int -> Int; +int-hash x = x; + +int-range : Int -> Int -> Table Int Int; + +int-range min max = let + + helper : Int -> Int -> Table Int Int -> Table Int Int; + helper min max tree = if_then_else_ (Int_eq min max) + (tree) (helper (min + 1) max (insert min min tree)); + +in helper min max (empty int-comp int-hash); + +remove-range : Int -> Int -> Table Int Int -> Table Int Int; + +remove-range min max tree = let + + helper : Int -> Int -> Table Int Int -> Table Int Int; + helper min max tree = if_then_else_ (Int_eq min max) + (tree) (helper (min + 1) max (remove min tree)); + +in helper min max tree; ===================================== tests/case_test.ml ===================================== --- a/tests/case_test.ml +++ b/tests/case_test.ml @@ -207,6 +207,35 @@ let _ = (add_test "CASE MACROS" "sub pattern" (fun () -> | _ -> failure ()) ) +let _ = (add_test "CASE MACROS" "no default" (fun () -> + let dcode = (case_decl^" + f : Bool -> Bool -> Int; + f b1 b2 = case (b1,b2) + | (false,false) => 0 + | (true,false) => 1 + | (false,true) => 2 + | (true,true) => 3; + + va = f false false; + vb = f true false; + vc = f false true; + vd = f true true; + ") in + + let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in + + let ecode = "va; vb; vc; vd;" in + + let ret = Elab.eval_expr_str ecode ectx rctx in + + match ret with + | [Vint a; Vint b; Vint c; Vint d] -> ( + match (a,b,c,d) with + | (0,1,2,3) -> success () + | (_,_,_,_) -> failure () ) + | _ -> failure ()) +) + (* run all tests *) let _ = run_all () View it on GitLab: https://gitlab.com/monnier/typer/commit/9156b0759d9823237cb4391c962cfb3240a2... -- View it on GitLab: https://gitlab.com/monnier/typer/commit/9156b0759d9823237cb4391c962cfb3240a2... You're receiving this email because of your account on gitlab.com.
Afficher les réponses par date
+ | none => % if_then_else_ (Sexp_eq ctor (Sexp_symbol "_")) + (quote (##case_ (_|_ (uquote var) + (_=>_ (uquote ctor) (uquote succ))))); + % "?" doesn't seem to help + % (quote (##case_ (_|_ (uquote var) + % (_=>_ (uquote ctor) (uquote succ))) + % (_=>_ _ ?)));
A "%" tout seul c'est pour les commentaires en fin de ligne, pour des commentaires comme ceux-ci, il faudrait utiliser "%%". [ Si tu édites avec Emacs (en utilisant le mode disponible dans typer/emacs/typer-mode.el), l'indentation automatique (e.g. en pressant TAB) rend ces conventions plus évidentes. ] Plus sérieusement, il semble qu'il faudra effectivement implémenter un "case" plus optimisé pour éliminer ces problèmes. Je crois qu'on peut le faire sans trop se soucier du := si on suit le principe suivant: quand on compare X contre en ensemble de motifs, on commence par partitionner ces motifs selon le constructeur principal qu'ils utilisent. Ensuite, pour chaque constructeur qui n'a qu'on seul motif on peut accepter les := sans avoir besoin de savoir à quelle position ils correspondent. Pour les constructeurs pour lesquels il y a plusieurs motifs, on peut simplement imposer que tous ces motifs utilisent les mêmes := Donc on peut accepter case x | cons (x := foo) bar => ... | cons (x := toto) titi => ... | ... mais refuser case x | cons (x := foo) bar => ... | cons toto titi => ... | ... C'est pas parfait, mais en attendant de faire mieux ça fera l'affaire.
+type Vec2 (a : Type) (b : Type) + | vec2 a b;
Il vaudrait mieux l'appeler `Pair` comme dans Haskell (et ça pourrait aller dans pervasive.typer remplacer le Pair actuel): type Pair a b | pair (fst : a) (snd : b); Tu peux (ou en tout cas, tu devrais pouvoir) ensuite faire: p = pair 1 2; s = p.fst + p.snd;
+TableData : Type -> Type -> Type; + +type TableData (a : Type) (k : Type) + | table-node (left : TableData a k) (right : TableData a k) + | table-leaf (elems : List (Vec2 a k)) + | table-nil;
Au fait, la macro `type` devrait ajouter le "TableData : Type -> Type -> Type;" automatiquement. En fait, il suffit probablement de changer la macro pour qu'elle émette un "TableData : ? -> ? -> Type;".
+%% a : element type +%% k : key type +%% s : size as a base of 2 (e.g. s = 5 <=> size = 32) +%% c : compare function (for key) +%% h : hash function (for key)
Je crois que t'as pas besoin de `s`: tu prends le hash, et sur cette base, tu fais gauche/droite/... bit par bit jusqu'à ce que l'arbre soit vide ou qu'il n'y a plus qu'un seule valeur de hash dans le sous arbre. Donc pour un arbre contenant 2 valeurs dont les hash respectifs sont 345394 et 119450, tu auras un arbre de la forme: table-node (left := table-node (table-leaf X) (table-leaf Y)) table-nil parce que le dernier bit des deux est 0 (donc on va à gauche dans le noeud racine pour les deux) et le bit suivant et 0 d'un côté et 1 de l'autre, donc au niveau suivant l'arbre se termine, vu que chaque sous-arbre ne contient plus qu'une seule entrée. Je changerais `table-leaf` pour qu'il garde le hash des éléments qu'il porte (devrait être le même pour tous), de manière à éviter de recalculer ce hash autant que possible. Un autre changement possible serait de n'avoir que `a` (ou que `k`): ça peut être utilisé pour les cas où il n'y pas vraiment de "clé" séparément des données (e.g. quant tu fais tu hash-consing). Avec une telle Table' tu peux ensuite définir: Table a k = Table' (Vec2 a k); pour retrouver la structure que tu as actuellement.
+ | table-node l r => ( let + o1 = helper f o l; + o2 = helper f o1 r; + in o2 )
Hmm.... il faudrait peut-être changer la précédence du `in` par rapport à `|` pour ne pas avoir besoin de ces parenthèses?
+ l2 = if_then_else_ (Int_eq (tabledata-length 0 l1) 0) + (table-nil) (l);
Pourquo n'utilises-tu pas l2 = if Int_eq (tabledata-length 0 l1) 0 then table-nil else l; ?
+ r2 = if_then_else_ (Int_eq (tabledata-length 0 r1) 0) + (table-nil) (r); + in table-node l2 r2 ) + | table-leaf xs => if_then_else_ (Int_eq (List_length xs) 0) + (table-nil) (table-leaf xs)
Je trouve cette indentation assez horrible, à vrai dire. Stefan
participants (2)
-
Jonathan Graveline -
Stefan Monnier