doc-src/IsarAdvanced/Codegen/Thy/examples/Example.hs
changeset 29735 6df726203e39
parent 29297 62e0f892e525
equal deleted inserted replaced
29734:08ef36ed2f8a 29735:6df726203e39
    12 
    12 
    13 list_case :: forall t a. t -> (a -> [a] -> t) -> [a] -> t;
    13 list_case :: forall t a. t -> (a -> [a] -> t) -> [a] -> t;
    14 list_case f1 f2 (a : list) = f2 a list;
    14 list_case f1 f2 (a : list) = f2 a list;
    15 list_case f1 f2 [] = f1;
    15 list_case f1 f2 [] = f1;
    16 
    16 
    17 data Queue a = Queue [a] [a];
    17 data Queue a = AQueue [a] [a];
    18 
    18 
    19 empty :: forall a. Queue a;
    19 empty :: forall a. Queue a;
    20 empty = Queue [] [];
    20 empty = AQueue [] [];
    21 
    21 
    22 dequeue :: forall a. Queue a -> (Maybe a, Queue a);
    22 dequeue :: forall a. Queue a -> (Maybe a, Queue a);
    23 dequeue (Queue [] []) = (Nothing, Queue [] []);
    23 dequeue (AQueue [] []) = (Nothing, AQueue [] []);
    24 dequeue (Queue xs (y : ys)) = (Just y, Queue xs ys);
    24 dequeue (AQueue xs (y : ys)) = (Just y, AQueue xs ys);
    25 dequeue (Queue (v : va) []) =
    25 dequeue (AQueue (v : va) []) =
    26   let {
    26   let {
    27     (y : ys) = rev (v : va);
    27     (y : ys) = rev (v : va);
    28   } in (Just y, Queue [] ys);
    28   } in (Just y, AQueue [] ys);
    29 
    29 
    30 enqueue :: forall a. a -> Queue a -> Queue a;
    30 enqueue :: forall a. a -> Queue a -> Queue a;
    31 enqueue x (Queue xs ys) = Queue (x : xs) ys;
    31 enqueue x (AQueue xs ys) = AQueue (x : xs) ys;
    32 
    32 
    33 }
    33 }