source: Deliverables/D2.2/8051/src/utilities/bList.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: 1.7 KB
Line 
1(** This module gives lists with internal binders. *)
2
3
4type ('a, 'b, 'c) t =
5  | Nil
6  | Cons of 'a * ('a, 'b, 'c) t
7  | New of 'c * ('b -> ('a, 'b, 'c) t)
8
9type ('a, 'b) t2 = ('a, 'b, unit) t
10
11let rec append l1 l2 = match l1 with
12  | Nil -> l2
13  | Cons (x, l1') -> Cons (x, append l1' l2)
14  | New (t, f) -> New (t, fun x -> append (f x) l2)
15
16let rev l =
17  let rec rev_acc acc = function
18    | Nil -> acc
19    | Cons (x, l) -> rev_acc (Cons (x, acc)) l
20    | New (t, f) -> New (t, fun x -> rev_acc acc (f x)) in
21  rev_acc Nil l
22
23let of_list l = List.fold_right (fun x l -> Cons (x, l)) l Nil
24
25let rec compile fresh u l = match l with
26  | Nil -> (u, [])
27  | Cons (a, l) ->
28    let (u', l') = compile fresh u l in
29    (u', a :: l')
30  | New (t, f) ->
31    let (u', r) = fresh u t in
32    compile fresh u' (f r)
33
34let compile2 fresh =
35  let fresh' u () = fresh u in
36  compile fresh'
37
38let rec fold_left f f_new init = function
39  | Nil -> init
40  | Cons (a, l) -> fold_left f f_new (f init a) l
41  | New (t, f_l) -> f_new t (fun x -> fold_left f f_new init (f_l x))
42
43let rec fold_right f f_new l init = match l with
44  | Nil -> init
45  | Cons (a, l) -> f a (fold_right f f_new l init)
46  | New (t, f_l) -> f_new t (fun x -> fold_right f f_new (f_l x) init)
47
48let rec concat = function
49  | [] -> Nil
50  | l :: ls -> append l (concat ls)
51
52let rec fresh_ts ts f = match ts with
53  | [] -> f []
54  | t :: ts -> New (t, fun x -> (fresh_ts ts (fun l -> f (x :: l))))
55
56let rec fresh_n n f =
57  if n <= 0 then f [] else
58    New ((), fun x -> (fresh_n (n - 1) (fun l -> f (x :: l))))
59
60module Notation = struct
61
62  let (^::) x l = Cons (x, l)
63  let (^@) = append
64  let bnil = Nil
65  let fresh f = New ((), f)
66  let fresh_n = fresh_n
67  let fresh_t t f = New (t, f)
68  let fresh_ts = fresh_ts
69
70end
Note: See TracBrowser for help on using the repository browser.