Previous Up Next

Module Basic

The basic module contains general functions not already present in the general libraries. Lists will heavily be used later, hence a number of list-manipulation function are collected here. All are straightforward. Therefore, the list-manipulating functions are not documented here.

let list_product (l1: α list) (ll2: α list list): α list list =
                   (fun e → ( (fun e2 → e::e2ll2)))

let list_product_2 (ll : β list list) : β list list =
   List.fold_right list_product ll [[ ]]

The next function takes two lists and applies f to all combinations of elements. As an example: list_map_cross_product f [a1,...,an][b1,...,bm] = [f(a1,b1),...,f(an,bm)].
let list_map_cross_product (f: α → β → γ) (l1: α list) (l2: β list
     : γ list = 
       (fun (cl: γ list) → fun(a: α) → (cl @( (f al2)))
       [ ]

let rec list_to_n (l: α listn : α list list =
(∗ gives back a list containing list of all combination of l, concatenated

tested: ok

   if n = 0 
   then [[ ]]
   else if (n = 1)
   then (fun x → [x]) l
       (fun a → fun b → (a::b))
       (list_to_n l (n−1))

The following one similarly takes a list and applies f to all combinations of itselements. The function f is assumed symmetric, i.e., that f(a,b) equals f(b,a); therefore only one of the two is entered. As example list_symproduct_3 f [a1,...,an] =[f(a1,a1),...,f(an,an)].

let rec list_symproduct_3 (f: α → α → γ) (l: α list) : γ list =
       match l with [ ] → [ ] ∣ a::l → (f a a) :: (( (f al) @
       list_symproduct_3 f l)

let list_flatten_2 (l : (((α list) × (β list)) list)) 
     : ((α list) × (β list)) =
   let (allbll) = List.split l
   in (List.flatten allList.flatten bll)

let list_flatten_map f l = (∗ more efficient than separate flatten and map

tested, ok

     (fun l → fun a → l @ (f a))
     [ ]

The next function does, what the name implies: given 2 list of the same type: it gives back the longest common prefix of the lists as first return value together with the remaining parts of the list.

tested: ok

let list_longest_common_prefix (l1l2) =
   let rec collect_revprefix (l_prel1l2) =
     match (l1,l2with
       ([ ],[ ]) → (l_prel1l2)
     ∣ ([ ],l2) → (l_prel1l2)
     ∣ (l1,[ ]) → (l_prel1l2)
     ∣ (e1::l1′e2:: l2′) → 
         (if (e1 = e2
         then collect_revprefix (e1::l_prel1′l2′)
         else (l_prel1l2))
   in let (l_pre_revl1_restl2_rest) = collect_revprefix ([ ], l1l2)
   in (List.rev l_pre_revl1_restl2_rest)

The following function checks, whether its first argument is a postfix of its second |both are generic lists| and if so, it additionally gives back the prefix.

tested: ok

let rec list_is_prefix_and_post l1 l2 =
   match (l1,l2with
     ([ ],l2) → (truel2)
   ∣ (l1,[ ]) → (false,[ ]) (∗ second return value doesn’t matter ∗)
   ∣ (e1::l1′,e2::l2′) →
       if (e1=e2)
       then list_is_prefix_and_post l1′ l2′
       else (false,[ ])

     second return value doesn’t matter
let list_is_postfix_and_pre l1 l2 = (∗ l2 = lpre l1? ∗)
   let (pl_pre_rev) = 
     list_is_prefix_and_post (List.rev l1) (List.rev l2)
   in (pList.rev l_pre_rev)

let rec list_remove_all (a: α) (l: α list) : α list =
   match l with
     [ ] → [ ]
   ∣ e::l → 
       if (a = e
       then (list_remove_all a l
       else e:: (list_remove_all a l)

   The function list_merge calulates l2\ l1 (the 2nd returned value), while at the same time removes duplicates from l1,

let list_merge l1 l2 =
   let rec merge l1 lnew l2 =
     match l2 with
       [ ] → (l1,lnew)
     ∣ x::l2′ → 
         let (l1′lnew) = merge l1 lnew l2′
         in if (List.mem x l1′)
         then (l1′lnew)
         else (x::l1′x::lnew)
   merge l1 [ ] l2

let list_remove_doublettes (l: α list) : α list =
   let rec purge l l_purged =
     match l with
       [ ] → l_purged
     ∣ a::l → 
         if (List.mem a l_purged)
         then purge l l_purged
         else purge l (a::l_purged)
   in List.rev (purge l [ ])

tested on ints, ok

let rec list_has_unique_entries l = 
   match l with 
       [ ] → true
   ∣ e::l → 
       if List.mem e l 
       then false
       else list_has_unique_entries l

The cross-product of 2 lists.
let list_cross_product l1 l2 = 
     list_map_cross_product (fun x → fun y → (x,y)) l1 l2

The following function takes a reservoir of elements, and builds all combinations i.e., lists of length n, i.e., it builds Ln if L is seen as the set (not list) of its members.


let rec list_combinations (l:α list) (n:int) : α list list =
   assert (n ≥0);
   match n with
     0 → [[ ]]
   ∣ _ → 
         (fun xfun y → x::y)
         l (list_combinations l (n−1))

The function list_insert_after_nth inserts an element into a list after the nth position. The positions in a list range from 1 to the length of the list, i.e., allowed argument values range from 0 (before the first element) up to the length of the list, i.e., after the last element. For values out of range, a general exception is raised. The function list_insert_after_allpos inserts an element after all legal positions

both tested ok

let list_insert_after_nth (n:int) (x: α) (l: α list) : α list =
   let rec h_insert m l_1 y l_2 = 
     match m with
       0 → List.rev_append l_1 (x:: l_2)
     ∣ _ → (∗ n > 0 ∗)
         match l_2 with
           [ ] → raise (Failure "list_insert_after_nth: illegal position")
         ∣ z::l_2′→ h_insert (m−1) (z::l_1y l_2′
   h_insert n [ ] x l

let list_insert_after_allpos (x: α) (l: α list) : (α listlist =
   let rec h_insert m y l = 
     match m with 
       0 → [list_insert_after_nth m y l]
     ∣ _ → (list_insert_after_nth m y l) :: (h_insert (m−1) y l)
   h_insert (List.length lx l

The function for symmetrifying takes a relation R (as list) and calculates its symmetric core, i.e., RId.
let symmetrify (ql: (α × α) list): (α × α) list =
   List.find_all (fun (x,y) → List.mem (y,xqlql

Graphs and searching

The next functions deal with graphs. Again the representation is rather standard: α → α list is the one-step successor function of the directed graph. The graphs will later be used to represent the reachability relation of the transducer. This will be done by depth-first-search, a plain search, and a “collecting” version, finding all nodes matching a given predicate.

type α dgraph = Graph of (α → α list)

exception Not_Found

let dfs (g: α dgraph) (p: α → bool) (start: α) : α = 
   match g with Graph succ →
     let rec search (visited: α list) (l: α list ) : α =
       match l with
         [ ] → raise Not_Found
       ∣ a::rl → 
           if (List.mem a visited)
           then (search visited rl)
             if (p a
             then a 
             else search (a::visited) ((succ a) @ rl)
     search [ ] [start]

let dfs_collect (g: α dgraph) (p: α → bool) (start: α) : α list = 
   match g with Graph succ →
     let rec search (visited: α list) (l:α list) (hits: α list): α list =
       match l with
         [ ] → hits
       ∣ a::rl → 
           if (List.mem a visited)
           then (search visited rl hits)
             if (p a
             then search (a::visited) ((succ a) @ rl) (a::hits)
             else search (a::visited) ((succ a) @ rlhits
     in search [ ] [start] [ ]


Finally some functions concerning orders. For sake of efficiency, we introduce some dedicated three-valued inductive type. With this type, we give a function for lexicographic order on lists, i.e., sequences, of the ordered elements: first compare the length of the list, if they are equal, recurse from left to right for a first possible difference which decides on the ordering.

type order = LESS ∣ EQ ∣ NLESS

let lex_order (ord: α → β → order) (la: α list) (lb: β list) : order =
   let rec lex_order_n (ord: α → β → order) (la: α list) (lb: β list
       : order =
     match (lalbwith
       ([ ],[ ]) → EQ
     ∣ (a::lab::lb) → 
         (match ord a b with
           LESS → LESS
         ∣ EQ → lex_order_n ord la lb
         ∣ NLESS → NLESS)
     ∣ _ → raise (Failure "lex_order: must not happen (lex_order)")
   let (length_lalength_lb) = ((List.length la), (List.length lb))
   in if length_la < length_lb
   then LESS
     (if (length_la = length_lb
     then (lex_order_n ord la lb)
     else NLESS)

Previous Up Next