source: Deliverables/D2.2/8051/src/utilities/bList.mli @ 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.3 KB
Line 
1(** This module gives lists with internal binders. *)
2
3type ('a, 'b, 'c) t =
4  | Nil
5  | Cons of 'a * ('a, 'b, 'c) t
6  | New of 'c * ('b -> ('a, 'b, 'c) t)
7
8type ('a, 'b) t2 = ('a, 'b, unit) t
9
10val rev : ('a, 'b, 'c) t -> ('a, 'b, 'c) t
11
12val append : ('a, 'b, 'c) t -> ('a, 'b, 'c) t -> ('a, 'b, 'c) t
13
14val of_list : 'a list -> ('a, 'b, 'c) t
15
16val compile : ('u -> 'c -> 'u * 'b) -> 'u -> ('a, 'b, 'c) t -> 'u * 'a list
17val compile2 : ('u -> 'u * 'b) -> 'u -> ('a, 'b) t2 -> 'u * 'a list
18
19val fold_left : ('a -> 'b -> 'a) -> ('d -> ('c -> 'a) -> 'a) -> 'a ->
20  ('b, 'c, 'd) t -> 'a
21
22val fold_right :
23  ('a -> 'b -> 'b) -> ('d -> ('c -> 'b) -> 'b) -> ('a, 'c, 'd) t -> 'b -> 'b
24
25val concat : ('a, 'b, 'c) t list -> ('a, 'b, 'c) t
26
27val fresh_n : int -> ('b list -> ('a, 'b) t2) -> ('a, 'b) t2
28
29val fresh_ts : 'c list -> ('b list -> ('a, 'b, 'c) t) -> ('a, 'b, 'c) t
30
31module Notation : sig
32  val (^::) : 'a -> ('a, 'b, 'c) t -> ('a, 'b, 'c) t
33  val (^@) : ('a, 'b, 'c) t -> ('a, 'b, 'c) t -> ('a, 'b, 'c) t
34  val bnil : ('a, 'b, 'c) t
35  val fresh : ('b -> ('a, 'b) t2) -> ('a, 'b) t2
36  val fresh_n : int -> ('b list -> ('a, 'b) t2) -> ('a, 'b) t2
37  val fresh_t : 'c -> ('b -> ('a, 'b, 'c) t) -> ('a, 'b, 'c) t
38  val fresh_ts : 'c list -> ('b list -> ('a, 'b, 'c) t) -> ('a, 'b, 'c) t
39end
Note: See TracBrowser for help on using the repository browser.