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.ml

    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)
    73
    8 let (^::) x l = BCons (x, l)
     4type ('a, 'b, 'c) t =
     5  | Nil
     6  | Cons of 'a * ('a, 'b, 'c) t
     7  | New of 'c * ('b -> ('a, 'b, 'c) t)
    98
    10 let rec (^@) l1 l2 = match l1 with
    11   | BNil -> l2
    12   | BCons (x, l1') -> BCons (x, l1' ^@ l2)
    13   | BNew f -> BNew (fun x -> f x ^@ l2)
     9type ('a, 'b) t2 = ('a, 'b, unit) t
    1410
    15 let (?^) f = BNew f
     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)
    1615
    17 let b_rev l =
     16let rev l =
    1817  let rec rev_acc acc = function
    19     | BNil -> acc
    20     | BCons (x, l) -> rev_acc (BCons (x, acc)) l
    21     | BNew f -> BNew (fun x -> rev_acc acc (f x)) in
    22   rev_acc BNil l
     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 TracChangeset for help on using the changeset viewer.