source: Deliverables/D2.2/8051/src/utilities/miscPottier.ml @ 1584

Last change on this file since 1584 was 1584, checked in by tranquil, 8 years ago
  • new form of translation written in graphUtilites (mainly as a test before implementation in Matita)
  • rewritten multiplication in RTLasbToRTL
File size: 4.2 KB
Line 
1
2let map3 f al bl cl =
3  let f' ((a, b), c) = f a b c in
4  List.map f' (List.combine (List.combine al bl) cl)
5
6let fold3_right f al bl cl =
7  let f' ((a, b), c) d = f a b c d in
8  List.fold_right f' (List.combine (List.combine al bl) cl)
9
10let rec max_list = function
11  | [] -> raise (Invalid_argument "MiscPottier.max_list")
12  | [a] -> a
13  | a :: l -> max a (max_list l)
14
15let rec reduce l1 l2 = match l1, l2 with
16  | [], _ -> (([], []), ([], l2))
17  | _, [] -> (([], l1), ([], []))
18  | a :: l1, b :: l2 ->
19    let ((common1, rest1), (common2, rest2)) = reduce l1 l2 in
20    ((a :: common1, rest1), (b :: common2, rest2))
21
22let pow a b =
23  if b < 0 then raise (Invalid_argument "MiscPottier.pow2")
24  else
25    let rec aux = function
26      | 0 -> 1
27      | i -> a * aux (i-1) in
28    aux b
29
30let rec make a n =
31  if n <= 0 then []
32  else a :: (make a (n-1))
33
34let makei f n =
35  let rec app f k =
36  if k >= n then []
37  else f k :: (app f (k + 1)) in
38  app f 0
39
40let index_of x =
41  let rec aux i = function
42    | [] -> raise Not_found
43    | y :: l -> if y = x then i else aux (i+1) l
44  in
45  aux 0
46
47let rec remove_n_first n =
48  let rec aux i = function
49  | [] -> []
50  | l when i = n -> l
51  | _ :: l -> aux (i+1) l in
52  aux 0
53
54let foldi_from_until n m f a l =
55  let rec aux i res = function
56    | [] -> res
57    | _ when i >= m -> res
58    | e :: l -> aux (i+1) (f i res e) l in
59  aux 0 a (remove_n_first n l)
60
61let foldi_from n f a l = foldi_from_until n (List.length l) f a l
62
63let foldi_until m f a l = foldi_from_until 0 m f a l
64
65let foldi f a l = foldi_from_until 0 (List.length l) f a l
66
67let pos e l =
68  let f i res e' = if e' = e then Some i else res in
69  match foldi f None l with
70    | None -> raise Not_found
71    | Some i -> i
72
73let iteri f l =
74  let rec aux i = function
75    | [] -> ()
76    | e :: l -> f i e ; aux (i+1) l
77  in
78  aux 0 l
79
80let mapi f l =
81  let rec aux i = function
82    | [] -> []
83    | e :: l -> (f i e) :: (aux (i+1) l)
84  in
85  aux 0 l
86
87let rec last = function
88  | [] -> raise Not_found
89  | [a] -> a
90  | _ :: l -> last l
91
92(* [split a i] splits the list a in two lists: one with the elements
93   up until the [i]th (exclusive) and one with the rest. *)
94
95let rec split l i =
96  if i = 0 then ([], l)
97  else
98    let (l1, l2) = split (List.tl l) (i-1) in
99    ((List.hd l) :: l1, l2)
100
101(* [split_last l] returns the list [l] without its last element and its last
102   element. Raises Invalid_argument "MiscPottier.split_last" if the list is
103   empty. *)
104
105let split_last l = match split l ((List.length l) - 1) with
106  | l', last :: _ -> (l', last)
107  | _ -> raise (Invalid_argument "MiscPottier.split_last")
108
109let rec update_list_assoc a b = function
110  | [] -> []
111  | (a', b') :: l ->
112      if a' = a then (a, b) :: l else (a', b') :: (update_list_assoc a b l)
113
114(* Pasted from Pottier's PP compiler *)
115
116let rec combine xs1 xs2 =
117  match xs1, xs2 with
118  | [], _
119  | _, [] ->
120      []
121  | x1 :: xs1, x2 :: xs2 ->
122      (x1, x2) :: combine xs1 xs2
123
124let rec subtract xs1 xs2 =
125  match xs1, xs2 with
126  | [], _ ->
127      []
128  | _, [] ->
129      xs1
130  | _ :: xs1, _ :: xs2 ->
131      subtract xs1 xs2
132
133let mirror l =
134  List.map (fun (x, y) -> (y, x)) l
135
136let length l =
137  Int32.of_int (List.length l)
138
139let rec prefix k l =
140  match k, l with
141  | 0, _
142  | _, [] ->
143      []
144  | _, x :: xs ->
145      x :: prefix (k - 1) xs
146
147let memoize f =
148  let table = Hashtbl.create 131 in
149  fun key ->
150    try
151      Hashtbl.find table key
152    with Not_found ->
153      let data = f key in
154      Hashtbl.add table key data;
155      data
156
157let filter_map filter map =
158  let rec aux = function
159    | [] -> []
160    | e :: l -> (if filter e then [map e] else []) @ (aux l)
161  in
162  aux
163
164let string_of_list sep f =
165  let rec aux = function
166    | [] -> ""
167    | [e] -> f e
168    | e :: l -> (f e) ^ sep ^ (aux l)
169  in
170  aux
171
172
173let rec sublist l k h =
174  if h < k || h < 0 || k < 0 then
175    invalid_arg "sublist: invalid interval"
176  else
177  match k, h, l with
178  | 0, 0, _ -> []
179  | 0, _, x :: l -> x :: sublist l 0 (h-1)
180  | _, _, x :: l -> sublist l (k-1) (h-1)
181  | _ -> invalid_arg "sublist: invalid interval"
182
183let rec fill l n =
184  let k = List.length l in
185  if k = 0 then invalid_arg "fill: list empty" else
186  if n < 0 then invalid_arg "fill: negative argument" else
187  if n <= k then sublist l 0 n else
188    l @ fill l (n - k)
Note: See TracBrowser for help on using the repository browser.