Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits: a89aa4f4 by Jonathan Graveline at 2018-07-11T19:39:36Z Compile samples/* only once in some unit tests; New balanced bst (bbst.typer)
- - - - -
4 changed files:
- + samples/bbst.typer - + tests/bbst_test.ml - tests/case_test.ml - tests/table_test.ml
Changes:
===================================== samples/bbst.typer ===================================== @@ -0,0 +1,705 @@ +%%% +%%% Balanced Binary Search Tree (bbst) +%%% +%%% (this first implementation is a 2-3-4-tree) +%%% (which is another representation for a Red Black Tree) +%%% + +%% +%% The 2-3-4 tree +%% + +type BbsTree (a : Type) + | node2 (d : a) (l0 : BbsTree a) (l1 : BbsTree a) + | node3 (d0 : a) (d1 : a) (l0 : BbsTree a) (l1 : BbsTree a) (l2 : BbsTree a) + | node4 (d0 : a) (d1 : a) (d2 : a) + (l0 : BbsTree a) (l1 : BbsTree a) (l2 : BbsTree a) (l3 : BbsTree a) + | node-leaf; + +%% +%% The tree with necessary data +%% +%% c is a compare function which should be similar to <= (or >=) +%% + +type Bbst (a : Type) + | bbst (c : a -> a -> Bool) (t : BbsTree a); + +%% +%% Fold the tree in an unspecified order +%% + +fold : (b : Type) ≡> (a : Type) ≡> (b -> a -> b) -> b -> Bbst a -> b; +fold f o t = let + + helper : (b : Type) ≡> (b -> a -> b) -> b -> BbsTree a -> b; + helper f o t = case t + | node2 d l0 l1 => let + o1 = helper f o l0; + o2 = helper f o1 l1; + in f o2 d + | node3 d0 d1 l0 l1 l2 => let + o1 = helper f o l0; + o2 = helper f o1 l1; + o3 = helper f o2 l2; + o4 = f o3 d0; + in f o4 d1 + | node4 d0 d1 d2 l0 l1 l2 l3 => let + o1 = helper f o l0; + o2 = helper f o1 l1; + o3 = helper f o2 l2; + o4 = helper f o3 l3; + o5 = f o4 d0; + o6 = f o5 d1; + in f o6 d2 + | node-leaf => o; + +in case t + | bbst c t => helper f o t; + +%% +%% Fold the tree leftmost element first +%% +%% (If comparator is "<=" then it fold the smallest first) +%% + +foldl : (b : Type) ≡> (a : Type) ≡> (b -> a -> b) -> b -> Bbst a -> b; +foldl f o t = let + + helper : (b : Type) ≡> (b -> a -> b) -> b -> BbsTree a -> b; + helper f o t = case t + | node2 d l0 l1 => let + o1 = helper f o l0; + o2 = f o1 d; + in helper f o2 l1 + | node3 d0 d1 l0 l1 l2 => let + o1 = helper f o l0; + o2 = f o1 d0; + o3 = helper f o2 l1; + o4 = f o3 d1; + in helper f o4 l2 + | node4 d0 d1 d2 l0 l1 l2 l3 => let + o1 = helper f o l0; + o2 = f o1 d0; + o3 = helper f o2 l1; + o4 = f o3 d1; + o5 = helper f o4 l2; + o6 = f o5 d2; + in helper f o6 l3 + | node-leaf => o; + +in case t + | bbst c t => helper f o t; + +%% +%% Fold the tree rightmost element first +%% +%% (If comparator is ">=" then it fold the biggest first) +%% + +foldr : (b : Type) ≡> (a : Type) ≡> (b -> a -> b) -> b -> Bbst a -> b; +foldr f o t = let + + helper : (b : Type) ≡> (b -> a -> b) -> b -> BbsTree a -> b; + helper f o t = case t + | node2 d l0 l1 => let + o1 = helper f o l1; + o2 = f o1 d; + in helper f o2 l0 + | node3 d0 d1 l0 l1 l2 => let + o1 = helper f o l2; + o2 = f o1 d1; + o3 = helper f o2 l1; + o4 = f o3 d0; + in helper f o4 l0 + | node4 d0 d1 d2 l0 l1 l2 l3 => let + o1 = helper f o l3; + o2 = f o1 d2; + o3 = helper f o2 l2; + o4 = f o3 d1; + o5 = helper f o4 l1; + o6 = f o5 d0; + in helper f o6 l0 + | node-leaf => o; + +in case t + | bbst c t => helper f o t; + +%% +%% Get the number of element in the tree +%% + +length = fold (lambda len _ -> len + 1) 0; + +%% +%% Is the tree empty? +%% + +is-empty tree = (Int_eq (length tree) 0); + +%% +%% Check if two value are equal with comparison function only +%% + +comp-equal : (a : Type) ≡> (a -> a -> Bool) -> a -> a -> Bool; +comp-equal comp x y = if_then_else_ (comp x y) + (comp y x) + (false); + +%% +%% Insert an element in the tree +%% + +insert : (a : Type) ≡> a -> Bbst a -> Bbst a; +insert elem tree = let + + helper : (a -> a -> Bool) -> a -> BbsTree a -> BbsTree a; + helper comp e p = case p + + | node2 d0 k0 k1 => + if_then_else_ (comp e d0) + (if_then_else_ (comp d0 e) + (node2 e k0 k1) + (case k0 + | node4 e0 e1 e2 l0 l1 l2 l3 => + if_then_else_ (comp e e0) + (if_then_else_ (comp e0 e) + (node2 d0 (node4 e e1 e2 l0 l1 l2 l3) k1) + (node3 e1 d0 (helper comp e (node2 e0 l0 l1)) (node2 e2 l2 l3) k1)) + (if_then_else_ (comp e e1) + (if_then_else_ (comp e1 e) + (node2 d0 (node4 e0 e e2 l0 l1 l2 l3) k1) + (node3 e1 d0 (helper comp e (node2 e0 l0 l1)) (node2 e2 l2 l3) k1)) + (if_then_else_ (comp e e2) + (if_then_else_ (comp e2 e) + (node2 d0 (node4 e0 e1 e l0 l1 l2 l3) k1) + (node3 e1 d0 (node2 e0 l0 l1) (helper comp e (node2 e2 l2 l3)) k1)) + (node3 e1 d0 (node2 e0 l0 l1) (helper comp e (node2 e2 l2 l3)) k1))) + | node-leaf => node3 e d0 node-leaf node-leaf k1 + | _ => node2 d0 (helper comp e k0) k1)) + (case k1 + | node4 e0 e1 e2 l0 l1 l2 l3 => + if_then_else_ (comp e e0) + (if_then_else_ (comp e0 e) + (node2 d0 k0 (node4 e e1 e2 l0 l1 l2 l3)) + (node3 d0 e1 k0 (helper comp e (node2 e0 l0 l1)) (node2 e2 l2 l3))) + (if_then_else_ (comp e e1) + (if_then_else_ (comp e1 e) + (node2 d0 k0 (node4 e0 e e2 l0 l1 l2 l3)) + (node3 d0 e1 k0 (helper comp e (node2 e0 l0 l1)) (node2 e2 l2 l3))) + (if_then_else_ (comp e e2) + (if_then_else_ (comp e2 e) + (node2 d0 k0 (node4 e0 e1 e l0 l1 l2 l3)) + (node3 d0 e1 k0 (node2 e0 l0 l1) (helper comp e (node2 e2 l2 l3)))) + (node3 d0 e1 k0 (node2 e0 l0 l1) (helper comp e (node2 e2 l2 l3))))) + | node-leaf => node3 d0 e k0 node-leaf node-leaf + | _ => node2 d0 k0 (helper comp e k1)) + + %% When doing a recursion I try not to call helper on a node4 + %% Because we then would need the parent of this node4 + + | node3 d0 d1 k0 k1 k2 => + if_then_else_ (comp e d0) + (if_then_else_ (comp d0 e) + (node3 e d1 k0 k1 k2) + (case k0 + | node4 e0 e1 e2 l0 l1 l2 l3 => + if_then_else_ (comp e e0) + (if_then_else_ (comp e0 e) + (node3 d0 d1 (node4 e e1 e2 l0 l1 l2 l3) k1 k2) + (node4 e1 d0 d1 (helper comp e (node2 e0 l0 l1)) (node2 e2 l2 l3) k1 k2)) + (if_then_else_ (comp e e1) + (if_then_else_ (comp e1 e) + (node3 d0 d1 (node4 e0 e e2 l0 l1 l2 l3) k1 k2) + (node4 e1 d0 d1 (helper comp e (node2 e0 l0 l1)) (node2 e2 l2 l3) k1 k2)) + (if_then_else_ (comp e e2) + (if_then_else_ (comp e2 e) + (node3 d0 d1 (node4 e0 e1 e l0 l1 l2 l3) k1 k2) + (node4 e1 d0 d1 (node2 e0 l0 l1) (helper comp e (node2 e2 l2 l3)) k1 k2)) + (node4 e1 d0 d1 (node2 e0 l0 l1) (helper comp e (node2 e2 l2 l3)) k1 k2))) + | node-leaf => node4 e d0 d1 node-leaf node-leaf k1 k2 + | _ => node3 d0 d1 (helper comp e k0) k1 k2)) + (if_then_else_ (comp e d1) + (if_then_else_ (comp d1 e) + (node3 d0 e k0 k1 k2) + (case k1 + | node4 e0 e1 e2 l0 l1 l2 l3 => + if_then_else_ (comp e e0) + (if_then_else_ (comp e0 e) + (node3 d0 d1 k0 (node4 e e1 e2 l0 l1 l2 l3) k2) + (node4 d0 e1 d1 k0 (helper comp e (node2 e0 l0 l1)) (node2 e2 l2 l3) k2)) + (if_then_else_ (comp e e1) + (if_then_else_ (comp e1 e) + (node3 d0 d1 k0 (node4 e0 e e2 l0 l1 l2 l3) k2) + (node4 d0 e1 d1 k0 (helper comp e (node2 e0 l0 l1)) (node2 e2 l2 l3) k2)) + (if_then_else_ (comp e e2) + (if_then_else_ (comp e2 e) + (node3 d0 d1 k0 (node4 e0 e1 e l0 l1 l2 l3) k2) + (node4 d0 e1 d1 k0 (node2 e0 l0 l1) (helper comp e (node2 e2 l2 l3)) k2)) + (node4 d0 e1 d1 k0 (node2 e0 l0 l1) (helper comp e (node2 e2 l2 l3)) k2))) + | node-leaf => node4 d0 e d1 k0 node-leaf node-leaf k2 + | _ => node3 d0 d1 k0 (helper comp e k1) k2)) + (case k2 + | node4 e0 e1 e2 l0 l1 l2 l3 => + if_then_else_ (comp e e0) + (if_then_else_ (comp e0 e) + (node3 d0 d1 k0 k1 (node4 e e1 e2 l0 l1 l2 l3)) + (node4 d0 d1 e1 k0 k1 (helper comp e (node2 e0 l0 l1)) (node2 e2 l2 l3))) + (if_then_else_ (comp e e1) + (if_then_else_ (comp e1 e) + (node3 d0 d1 k0 k1 (node4 e0 e e2 l0 l1 l2 l3)) + (node4 d0 d1 e1 k0 k1 (helper comp e (node2 e0 l0 l1)) (node2 e2 l2 l3))) + (if_then_else_ (comp e e2) + (if_then_else_ (comp e2 e) + (node3 d0 d1 k0 k1 (node4 e0 e1 e l0 l1 l2 l3)) + (node4 d0 d1 e1 k0 k1 (node2 e0 l0 l1) (helper comp e (node2 e2 l2 l3)))) + (node4 d0 d1 e1 k0 k1 (node2 e0 l0 l1) (helper comp e (node2 e2 l2 l3))))) + | node-leaf => node4 d0 d1 e k0 k1 node-leaf node-leaf + | _ => node3 d0 d1 k0 k1 (helper comp e k2))) + + | node4 d0 d1 d2 k0 k1 k2 k3 => + %% I need the parent of "p" + %% But it seems to work with other branch (see above) + helper comp e (node2 d1 (node2 d0 k0 k1) (node2 d2 k2 k3)) + + | node-leaf => node2 e node-leaf node-leaf; + +in case tree + | bbst c t => bbst c (helper c elem t); + +%% +%% Remove the smallest element. Used in remove. +%% + +pop-leftmost : (a : Type) ≡> (a -> a -> Bool) -> BbsTree a -> BbsTree a; +pop-leftmost comp tree = let + + four2three : a -> a -> a -> + BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a; + + three2two : a -> a -> + BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a; + + two2leaf : a -> BbsTree a -> BbsTree a -> BbsTree a; + + helper : BbsTree a -> BbsTree a; + + helper tree = case tree + | node2 d l0 l1 => + two2leaf d l0 l1 + | node3 d0 d1 l0 l1 l2 => + three2two d0 d1 l0 l1 l2 + | node4 d0 d1 d2 l0 l1 l2 l3 => + four2three d0 d1 d2 l0 l1 l2 l3 + | node-leaf => node-leaf; + + two2leaf d0 l0 l1 = case l0 + | node-leaf => l1 + | _ => node2 d0 (helper l0) l1; + + three2two d0 d1 l0 l1 l2 = case l0 + | node-leaf => node2 d1 l1 l2 + | _ => node3 d0 d1 (helper l0) l1 l2; + + four2three d0 d1 d2 l0 l1 l2 l3 = case l0 + | node-leaf => node3 d1 d2 l1 l2 l3 + | _ => node4 d0 d1 d2 (helper l0) l1 l2 l3; + +in (helper tree); + +%% +%% Remove the biggest element. Used in remove. +%% + +pop-rightmost : (a : Type) ≡> (a -> a -> Bool) -> BbsTree a -> BbsTree a; +pop-rightmost comp tree = let + + four2three : a -> a -> a -> + BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a; + + three2two : a -> a -> + BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a; + + two2leaf : a -> BbsTree a -> BbsTree a -> BbsTree a; + + helper : BbsTree a -> BbsTree a; + + helper tree = case tree + | node2 d l0 l1 => + two2leaf d l0 l1 + | node3 d0 d1 l0 l1 l2 => + three2two d0 d1 l0 l1 l2 + | node4 d0 d1 d2 l0 l1 l2 l3 => + four2three d0 d1 d2 l0 l1 l2 l3 + | node-leaf => node-leaf; + + two2leaf d0 l0 l1 = case l1 + | node-leaf => l0 + | _ => node2 d0 l0 (helper l1); + + three2two d0 d1 l0 l1 l2 = case l2 + | node-leaf => node2 d0 l0 l1 + | _ => node3 d0 d1 l0 l1 (helper l2); + + four2three d0 d1 d2 l0 l1 l2 l3 = case l3 + | node-leaf => node3 d0 d1 l0 l1 l2 + | _ => node4 d0 d1 d2 l0 l1 l2 (helper l3); + +in (helper tree); + +%% +%% Get the smallest element. Used in remove. +%% + +get-leftmost : (a : Type) ≡> (a -> a -> Bool) -> BbsTree a -> Option a; +get-leftmost comp tree = let + + four2three : a -> a -> a -> + BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a -> Option a; + + three2two : a -> a -> BbsTree a -> BbsTree a -> BbsTree a -> Option a; + + two2leaf : a -> BbsTree a -> BbsTree a -> Option a; + + helper : BbsTree a -> Option a; + + helper tree = case tree + | node2 d l0 l1 => + two2leaf d l0 l1 + | node3 d0 d1 l0 l1 l2 => + three2two d0 d1 l0 l1 l2 + | node4 d0 d1 d2 l0 l1 l2 l3 => + four2three d0 d1 d2 l0 l1 l2 l3 + | node-leaf => none; + + two2leaf d0 l0 l1 = case l0 + | node-leaf => some d0 + | _ => (helper l0); + + three2two d0 d1 l0 l1 l2 = case l0 + | node-leaf => some d0 + | _ => (helper l0); + + four2three d0 d1 d2 l0 l1 l2 l3 = case l0 + | node-leaf => some d0 + | _ => (helper l0); + +in (helper tree); + +%% +%% Get the biggest element. Used in remove. +%% + +get-rightmost : (a : Type) ≡> (a -> a -> Bool) -> BbsTree a -> Option a; +get-rightmost comp tree = let + + four2three : a -> a -> a -> + BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a -> Option a; + + three2two : a -> a -> BbsTree a -> BbsTree a -> BbsTree a -> Option a; + + two2leaf : a -> BbsTree a -> BbsTree a -> Option a; + + helper : BbsTree a -> Option a; + + helper tree = case tree + | node2 d l0 l1 => + two2leaf d l0 l1 + | node3 d0 d1 l0 l1 l2 => + three2two d0 d1 l0 l1 l2 + | node4 d0 d1 d2 l0 l1 l2 l3 => + four2three d0 d1 d2 l0 l1 l2 l3 + | node-leaf => none; + + two2leaf d0 l0 l1 = case l1 + | node-leaf => some d0 + | _ => (helper l1); + + three2two d0 d1 l0 l1 l2 = case l2 + | node-leaf => some d1 + | _ => (helper l2); + + four2three d0 d1 d2 l0 l1 l2 l3 = case l3 + | node-leaf => some d2 + | _ => (helper l3); + +in (helper tree); + +%% +%% Remove an element from the tree +%% +%% This implementation isn't always balanced +%% I may remove a node2 when it has a leaf child but I should +%% do some tricks with sibling to always be balanced +%% + +remove : (a : Type) ≡> a -> Bbst a -> Bbst a; +remove elem tree = let + + rebuild-two : (a -> a -> Bool) -> + BbsTree a -> BbsTree a -> BbsTree a; + + rebuild-two comp l0 l1 = case l0 + | node-leaf => ( case l1 + | node-leaf => node-leaf + | _ => let + oe = get-leftmost comp l1; + in case oe + | some e => node2 e l0 (pop-leftmost comp l1) + | none => node-leaf ) % I think this case may not happen + | _ => let + oe = get-rightmost comp l0; + in case oe + | some e => node2 e (pop-rightmost comp l0) l1 + | none => node-leaf; % May not happen too + + rebuild-left-three : (a -> a -> Bool) -> a -> + BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a; + + rebuild-left-three comp d1 l0 l1 l2 = case l0 + | node-leaf => ( case l1 + | node-leaf => node2 d1 node-leaf l2 + | _ => let + oe = get-leftmost comp l1; + in case oe + | some e => node3 e d1 l0 (pop-leftmost comp l1) l2 + | none => node-leaf ) % I think this case may not happen + | _ => let + oe = get-rightmost comp l0; + in case oe + | some e => node3 e d1 (pop-rightmost comp l0) l1 l2 + | none => node-leaf; % May not happen too + + rebuild-right-three : (a -> a -> Bool) -> a -> + BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a; + + rebuild-right-three comp d0 l0 l1 l2 = case l1 + | node-leaf => ( case l2 + | node-leaf => node2 d0 l0 node-leaf + | _ => let + oe = get-leftmost comp l2; + in case oe + | some e => node3 d0 e l0 l1 (pop-leftmost comp l2) + | none => node-leaf ) % I think this case may not happen + | _ => let + oe = get-rightmost comp l1; + in case oe + | some e => node3 d0 e l0 (pop-rightmost comp l1) l2 + | none => node-leaf; % May not happen too + + rebuild-left-four : (a -> a -> Bool) -> a -> a -> + BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a; + + rebuild-left-four comp d1 d2 l0 l1 l2 l3 = case l0 + | node-leaf => ( case l1 + | node-leaf => node3 d1 d2 node-leaf l2 l3 + | _ => let + oe = get-leftmost comp l1; + in case oe + | some e => node4 e d1 d2 l0 (pop-leftmost comp l1) l2 l3 + | none => node-leaf ) % I think this case may not happen + | _ => let + oe = get-rightmost comp l0; + in case oe + | some e => node4 e d1 d2 (pop-rightmost comp l0) l1 l2 l3 + | none => node-leaf; % May not happen too + + rebuild-middle-four : (a -> a -> Bool) -> a -> a -> + BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a; + + rebuild-middle-four comp d0 d2 l0 l1 l2 l3 = case l1 + | node-leaf => ( case l2 + | node-leaf => node3 d0 d2 l0 node-leaf l3 + | _ => let + oe = get-leftmost comp l2; + in case oe + | some e => node4 d0 e d2 l0 l1 (pop-leftmost comp l2) l3 + | none => node-leaf ) % I think this case may not happen + | _ => let + oe = get-rightmost comp l1; + in case oe + | some e => node4 d0 e d2 l0 (pop-rightmost comp l1) l2 l3 + | none => node-leaf; % May not happen too + + rebuild-right-four : (a -> a -> Bool) -> a -> a -> + BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a -> BbsTree a; + + rebuild-right-four comp d0 d1 l0 l1 l2 l3 = case l2 + | node-leaf => ( case l3 + | node-leaf => node3 d0 d1 l0 l1 node-leaf + | _ => let + oe = get-leftmost comp l3; + in case oe + | some e => node4 d0 d1 e l0 l1 l2 (pop-leftmost comp l3) + | none => node-leaf ) % I think this case may not happen + | _ => let + oe = get-rightmost comp l2; + in case oe + | some e => node4 d0 d1 e l0 l1 (pop-rightmost comp l2) l3 + | none => node-leaf; % May not happen too + + helper : (a -> a -> Bool) -> a -> BbsTree a -> BbsTree a; + helper comp elem tree = case tree + | node2 d l0 l1 => + + if_then_else_ (comp elem d) + (if_then_else_ (comp d elem) + (rebuild-two comp l0 l1) + (node2 d (helper comp elem l0) l1)) + (node2 d l0 (helper comp elem l1)) + + | node3 d0 d1 l0 l1 l2 => + + if_then_else_ (comp elem d0) + (if_then_else_ (comp d0 elem) + (rebuild-left-three comp d1 l0 l1 l2) % replace d0 + (node3 d0 d1 (helper comp elem l0) l1 l2)) + (if_then_else_ (comp elem d1) + (if_then_else_ (comp d1 elem) + (rebuild-right-three comp d0 l0 l1 l2) % replace d1 + (node3 d0 d1 l0 (helper comp elem l1) l2)) + (node3 d0 d1 l0 l1 (helper comp elem l2))) + + | node4 d0 d1 d2 l0 l1 l2 l3 => + + if_then_else_ (comp elem d0) + (if_then_else_ (comp d0 elem) + (rebuild-left-four comp d1 d2 l0 l1 l2 l3) + (node4 d0 d1 d2 (helper comp elem l0) l1 l2 l3)) + (if_then_else_ (comp elem d1) + (if_then_else_ (comp d1 elem) + (rebuild-middle-four comp d0 d2 l0 l1 l2 l3) + (node4 d0 d1 d2 l0 (helper comp elem l1) l2 l3)) + (if_then_else_ (comp elem d2) + (if_then_else_ (comp d2 elem) + (rebuild-right-four comp d0 d1 l0 l1 l2 l3) + (node4 d0 d1 d2 l0 l1 (helper comp elem l2) l3)) + (node4 d0 d1 d2 l0 l1 l2 (helper comp elem l3)))) + + | node-leaf => node-leaf; + +in case tree + | bbst c t => bbst c (helper c elem t); + +%% +%% Find an element in the tree and return it +%% + +find : (a : Type) ≡> a -> Bbst a -> Option a; +find elem tree = let + + helper : (a -> a -> Bool) -> a -> BbsTree a -> Option a; + helper comp elem tree = case tree + | node2 d0 l0 l1 => + if_then_else_ (comp elem d0) + (if_then_else_ (comp d0 elem) + (some d0) + (helper comp elem l0)) + (helper comp elem l1) + | node3 d0 d1 l0 l1 l2 => + if_then_else_ (comp elem d0) + (if_then_else_ (comp d0 elem) + (some d0) + (helper comp elem l0)) + (if_then_else_ (comp elem d1) + (if_then_else_ (comp d1 elem) + (some d1) + (helper comp elem l1)) + (helper comp elem l2)) + | node4 d0 d1 d2 l0 l1 l2 l3 => + if_then_else_ (comp elem d0) + (if_then_else_ (comp d0 elem) + (some d0) + (helper comp elem l0)) + (if_then_else_ (comp elem d1) + (if_then_else_ (comp d1 elem) + (some d1) + (helper comp elem l1)) + (if_then_else_ (comp elem d2) + (if_then_else_ (comp d2 elem) + (some d2) + (helper comp elem l2)) + (helper comp elem l3))) + | node-leaf => none; + +in case tree + | bbst c t => helper c elem t; + +%% +%% Is elem in the tree? +%% + +member : (a : Type) ≡> a -> Bbst a -> Bool; +member elem tree = let + + oe = find elem tree; + +in case oe + | some _ => true + | none => false; + +%% +%% An empty tree with a key compare function as argument +%% + +empty : (a : Type) ≡> (a -> a -> Bool) -> Bbst a; +empty comp-fun = bbst comp-fun node-leaf; + +%%% +%%% Test helper +%%% + +%% +%% Compare function for Int +%% + +int-comp : Int -> Int -> Bool; +int-comp x y = Int_<= x y; + +%% +%% Construct a set with Int in interval [min,max[ +%% +%% (This is the worst case for a binary tree) +%% + +int-range1 : Int -> Int -> Bbst Int; +int-range1 min max = let + + helper : Int -> Bbst Int -> Bbst Int; + helper min tree = if_then_else_ (Int_eq min max) + (tree) (helper (min + 1) (insert min tree)); + +in helper min (empty int-comp); + +%% +%% Construct a set with Int in interval [min,max[ +%% +%% (This one is not the worst case) +%% + +int-range2 : Int -> Int -> Bbst Int; +int-range2 min max = let + + helper : Int -> Int -> Bbst Int -> Bbst Int; + helper min max tree = let + + a = insert (max - 1) tree; + + in if_then_else_ (Int_eq min max) + (a) + (helper (min + 1) (max - 1) (insert min a)); + +in helper min max (empty int-comp); + +%% +%% Remove Int inside interval [min,max[ from the Tree +%% + +remove-range : Int -> Int -> Bbst Int -> Bbst Int; +remove-range min max tree = let + + helper : Int -> Bbst Int -> Bbst Int; + helper min tree = if_then_else_ (Int_eq min max) + (tree) (helper (min + 1) (remove min tree)); + +in helper min tree;
===================================== tests/bbst_test.ml ===================================== @@ -0,0 +1,207 @@ + +open Util +open Utest_lib + +open Sexp +open Lexp + +open Eval (* reset_eval_trace *) + +open Builtin +open Env + +(* default environment *) +let ectx = Elab.default_ectx +let rctx = Elab.default_rctx + +(* TODO : use special form "load" *) +let bbst_decl = let read_file filename = + let lines = ref [] in + let chan = open_in filename in + try + while true; do + lines := input_line chan :: !lines + done; !lines + with End_of_file -> + close_in chan; + List.rev !lines + +in String.concat "\n" (read_file "samples/bbst.typer") + +(* eval bbst.typer only once! *) +let rctx, ectx = Elab.eval_decl_str bbst_decl ectx rctx + +(* really basic tests *) + +(* first part of this file is mostly identical to table_test.ml *) + +let _ = (add_test "BBST" "length" (fun () -> + + (* it's hard to test int-range1 alone *) + let dcode = " + a = length (int-range1 0 0); + b = length (int-range1 0 1); + c = length (int-range1 0 2); + d = length (int-range1 0 100); + e = length (int-range1 1111 2222); + " in + + let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in + + let ecode = "a; b; c; d; e;" in + + let ret = Elab.eval_expr_str ecode ectx rctx in + + match ret with + | [Vint 0; Vint 1; Vint 2; Vint 100; Vint 1111] -> success () + | _ -> failure ()) +) + +let _ = (add_test "BBST" "find" (fun () -> + let dcode = " + a = find 5 (int-range1 0 100); + a = case a | some a => a | none => 777; + + b = find 101 (int-range1 0 100); + b = case b | some b => b | none => 777; + " in + + let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in + + let ecode = "a; b;" in + + let ret = Elab.eval_expr_str ecode ectx rctx in + + match ret with + | [Vint 5; Vint 777] -> success () + | _ -> failure ()) +) + +let _ = (add_test "BBST" "insert" (fun () -> + let dcode = " + a = find 777 (insert 777 (int-range1 0 0)); + a = case a | some a => a | none => 11111; + + b = find 101 (insert 101 (int-range1 0 100)); + b = case b | some b => b | none => 11111; + " in + + let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in + + let ecode = "a; b;" in + + let ret = Elab.eval_expr_str ecode ectx rctx in + + match ret with + | [Vint 777; Vint 101] -> success () + | _ -> failure ()) +) + +let _ = (add_test "BBST" "member" (fun () -> + let dcode = " + a = member 0 (int-range1 0 0); + a = case a | true => 1 | false => 0; + + b = member 15 (int-range1 15 75); + b = case b | true => 1 | false => 0; + + c = member 50 (int-range1 0 100); + c = case c | true => 1 | false => 0; + " in + + let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in + + let ecode = "a; b; c;" in + + let ret = Elab.eval_expr_str ecode ectx rctx in + + match ret with + | [Vint 0; Vint 1; Vint 1] -> success () + | _ -> failure ()) +) + +let _ = (add_test "BBST" "remove" (fun () -> + let dcode = " + t = int-range1 15 75; + + a = (length t) - (length (remove 50 t)); + + b = member 50 t; + b = case b | true => 1 | false => 0; + + c = member 50 (remove 50 t); + c = case c | true => 1 | false => 0; + " in + + let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in + + let ecode = "a; b; c;" in + + let ret = Elab.eval_expr_str ecode ectx rctx in + + match ret with + | [Vint 1; Vint 1; Vint 0] -> success () + | _ -> failure ()) +) + +(* next part isn't in table_test.ml *) + +(* foldr and foldl should work only if the tree is correctly ordered *) + +let _ = (add_test "BBST" "order and fold" (fun () -> + let dcode = " + t1 = int-range1 15 75; % max is 74, min is 15 + + t2 = int-range2 11 91; % max is 90, min is 11 + + a = foldl + (lambda o e -> if_then_else_ (Int_> o e) (75) (e)) + (14) t1; + + b = foldr + (lambda o e -> if_then_else_ (Int_< o e) (14) (e)) + (75) t1; + + c = foldl + (lambda o e -> if_then_else_ (Int_> o e) (91) (e)) + (10) t2; + + d = foldr + (lambda o e -> if_then_else_ (Int_< o e) (10) (e)) + (91) t2; + + t3 = remove-range 20 70 t1; % max is still 74, min is still 15 + + t4 = remove-range 20 80 t2; % max is still 90, min is still 11 + + e = foldl + (lambda o e -> if_then_else_ (Int_> o e) (75) (e)) + (14) t3; + + f = foldr + (lambda o e -> if_then_else_ (Int_< o e) (14) (e)) + (75) t3; + + g = foldl + (lambda o e -> if_then_else_ (Int_> o e) (91) (e)) + (10) t4; + + h = foldr + (lambda o e -> if_then_else_ (Int_< o e) (10) (e)) + (91) t4; + " in + + let rctx, ectx = Elab.eval_decl_str dcode ectx rctx in + + let ecode = "a; b; c; d; e; f; g; h;" in + + let ret = Elab.eval_expr_str ecode ectx rctx in + + match ret with + | [Vint 74; Vint 15; Vint 90; Vint 11; Vint 74; Vint 15; Vint 90; Vint 11] -> success () + | _ -> failure ()) +) + + +(* run all tests *) +let _ = run_all ()
===================================== tests/case_test.ml ===================================== @@ -33,8 +33,11 @@ let case_decl = let read_file filename =
in String.concat "\n" (read_file "samples/case.typer")
+(* eval case.typer only once! *) +let rctx, ectx = Elab.eval_decl_str case_decl ectx rctx + let _ = (add_test "CASE MACROS" "case on single variable" (fun () -> - let dcode = (case_decl^" + let dcode = (" f : Bool -> Int; f a = case a | true => 1 @@ -67,7 +70,7 @@ let _ = (add_test "CASE MACROS" "case on single variable" (fun () -> )
let _ = (add_test "CASE MACROS" "case on Bool" (fun () -> - let dcode = (case_decl^" + let dcode = (" f : Bool -> Bool -> Bool -> Int; f a b c = case (a,b,c) | (true,false,_) => 1 @@ -102,7 +105,7 @@ let _ = (add_test "CASE MACROS" "case on Bool" (fun () -> )
let _ = (add_test "CASE MACROS" "case on list" (fun () -> - let dcode = (case_decl^" + let dcode = (" f : List Int -> List Int -> Int; f xs ys = case (xs,ys) | (cons x xs,cons y ys) => (x + y) + (f xs ys) @@ -135,7 +138,7 @@ let _ = (add_test "CASE MACROS" "case on list" (fun () -> )
let _ = (add_test "CASE MACROS" "3 constant" (fun () -> - let dcode = (case_decl^" + let dcode = (" type ColorComponent | red | green @@ -175,7 +178,7 @@ let _ = (add_test "CASE MACROS" "3 constant" (fun () -> )
let _ = (add_test "CASE MACROS" "sub pattern" (fun () -> - let dcode = (case_decl^" + let dcode = (" f : List (Option Bool) -> List (Option Bool) -> Int; f xs ys = case (xs,ys) | (cons (some true) xs, cons (some true) ys) => f xs ys @@ -208,7 +211,7 @@ let _ = (add_test "CASE MACROS" "sub pattern" (fun () -> )
let _ = (add_test "CASE MACROS" "no default" (fun () -> - let dcode = (case_decl^" + let dcode = (" f : Bool -> Bool -> Int; f b1 b2 = case (b1,b2) | (false,false) => 0
===================================== tests/table_test.ml ===================================== @@ -28,12 +28,15 @@ let table_decl = let read_file filename =
in String.concat "\n" (read_file "samples/table.typer")
+(* eval table.typer only once! *) +let rctx, ectx = Elab.eval_decl_str table_decl ectx rctx + (* really basic tests *)
let _ = (add_test "TABLE" "length" (fun () ->
(* it's hard to test int-range alone *) - let dcode = table_decl^" + let dcode = " a = length (int-range 0 0); b = length (int-range 0 1); c = length (int-range 0 2); @@ -53,7 +56,7 @@ let _ = (add_test "TABLE" "length" (fun () -> )
let _ = (add_test "TABLE" "find" (fun () -> - let dcode = table_decl^" + let dcode = " a = find 5 (int-range 0 100); a = case a | some a => a | none => 777;
@@ -73,7 +76,7 @@ let _ = (add_test "TABLE" "find" (fun () -> )
let _ = (add_test "TABLE" "insert" (fun () -> - let dcode = table_decl^" + let dcode = " a = find 777 (insert 777 (int-range 0 0)); a = case a | some a => a | none => 11111;
@@ -93,7 +96,7 @@ let _ = (add_test "TABLE" "insert" (fun () -> )
let _ = (add_test "TABLE" "member" (fun () -> - let dcode = table_decl^" + let dcode = " a = member 0 (int-range 0 0); a = case a | true => 1 | false => 0;
@@ -116,7 +119,7 @@ let _ = (add_test "TABLE" "member" (fun () -> )
let _ = (add_test "TABLE" "remove" (fun () -> - let dcode = table_decl^" + let dcode = " t = int-range 15 75;
a = (length t) - (length (remove 50 t));
View it on GitLab: https://gitlab.com/monnier/typer/commit/a89aa4f4123e02fc8539347743a47bbc60e5...
Afficher les réponses par date