Ignore:
Timestamp:
Dec 2, 2011, 3:13:04 PM (8 years ago)
Author:
tranquil
Message:
  • new form of translation written in graphUtilites (mainly as a test before implementation in Matita)
  • rewritten multiplication in RTLasbToRTL
File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D2.2/8051/src/utilities/bList.mli

    r1580 r1584  
    11(** This module gives lists with internal binders. *)
    22
    3 type ('a, 'b) t =
    4   | BNil
    5   | BCons of 'a * ('a, 'b) t
    6   | BNew of ('b -> ('a, 'b) t)
     3type ('a, 'b, 'c) t =
     4  | Nil
     5  | Cons of 'a * ('a, 'b, 'c) t
     6  | New of 'c * ('b -> ('a, 'b, 'c) t)
    77
    8 val (^::) : 'a -> ('a, 'b) t -> ('a, 'b) t
     8type ('a, 'b) t2 = ('a, 'b, unit) t
    99
    10 val (^@) : ('a, 'b) t -> ('a, 'b) t -> ('a, 'b) t
     10val rev : ('a, 'b, 'c) t -> ('a, 'b, 'c) t
    1111
    12 val (?^) : ('b -> ('a, 'b) t) -> ('a, 'b) t
     12val append : ('a, 'b, 'c) t -> ('a, 'b, 'c) t -> ('a, 'b, 'c) t
    1313
    14 val b_rev : ('a, 'b) t -> ('a, 'b) t
     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 TracChangeset for help on using the changeset viewer.