Changeset 1584 for Deliverables/D2.2/8051/src/utilities

Timestamp:

Dec 2, 2011, 3:13:04 PM (9 years ago)

Author:

tranquil

Message:

• new form of translation written in graphUtilites (mainly as a test before implementation in Matita)
• rewritten multiplication in RTLasbToRTL

Location:

Deliverables/D2.2/8051/src/utilities

Files:

• bList.ml (modified) (1 diff)
• bList.mli (modified) (1 diff)
• graphUtilities.ml (modified) (2 diffs)
• graphUtilities.mli (modified) (3 diffs)
• miscPottier.ml (modified) (3 diffs)
• miscPottier.mli (modified) (3 diffs)

Deliverables/D2.2/8051/src/utilities/bList.ml

@@ -1 +1 @@
 (** This module gives lists with internal binders. *)
 
-type ('a, 'b) t =
-  | BNil
-  | BCons of 'a * ('a, 'b) t
-  | BNew of ('b -> ('a, 'b) t)
 
-let (^::) x l = BCons (x, l)
+type ('a, 'b, 'c) t =
+  | Nil
+  | Cons of 'a * ('a, 'b, 'c) t
+  | New of 'c * ('b -> ('a, 'b, 'c) t)
 
-let rec (^@) l1 l2 = match l1 with
-  | BNil -> l2
-  | BCons (x, l1') -> BCons (x, l1' ^@ l2)
-  | BNew f -> BNew (fun x -> f x ^@ l2)
+type ('a, 'b) t2 = ('a, 'b, unit) t
 
-let (?^) f = BNew f
+let rec append l1 l2 = match l1 with
+  | Nil -> l2
+  | Cons (x, l1') -> Cons (x, append l1' l2)
+  | New (t, f) -> New (t, fun x -> append (f x) l2)
 
-let b_rev l =
+let rev l =
   let rec rev_acc acc = function
-    | BNil -> acc
-    | BCons (x, l) -> rev_acc (BCons (x, acc)) l
-    | BNew f -> BNew (fun x -> rev_acc acc (f x)) in
-  rev_acc BNil l
+    | Nil -> acc
+    | Cons (x, l) -> rev_acc (Cons (x, acc)) l
+    | New (t, f) -> New (t, fun x -> rev_acc acc (f x)) in
+  rev_acc Nil l
+
+let of_list l = List.fold_right (fun x l -> Cons (x, l)) l Nil
+
+let rec compile fresh u l = match l with
+  | Nil -> (u, [])
+  | Cons (a, l) ->
+    let (u', l') = compile fresh u l in
+    (u', a :: l')
+  | New (t, f) ->
+    let (u', r) = fresh u t in
+    compile fresh u' (f r)
+
+let compile2 fresh =
+  let fresh' u () = fresh u in
+  compile fresh'
+
+let rec fold_left f f_new init = function
+  | Nil -> init
+  | Cons (a, l) -> fold_left f f_new (f init a) l
+  | New (t, f_l) -> f_new t (fun x -> fold_left f f_new init (f_l x))
+
+let rec fold_right f f_new l init = match l with
+  | Nil -> init
+  | Cons (a, l) -> f a (fold_right f f_new l init)
+  | New (t, f_l) -> f_new t (fun x -> fold_right f f_new (f_l x) init)
+
+let rec concat = function
+  | [] -> Nil
+  | l :: ls -> append l (concat ls)
+
+let rec fresh_ts ts f = match ts with
+  | [] -> f []
+  | t :: ts -> New (t, fun x -> (fresh_ts ts (fun l -> f (x :: l))))
+
+let rec fresh_n n f =
+  if n <= 0 then f [] else
+    New ((), fun x -> (fresh_n (n - 1) (fun l -> f (x :: l))))
+
+module Notation = struct
+
+  let (^::) x l = Cons (x, l)
+  let (^@) = append
+  let bnil = Nil
+  let fresh f = New ((), f)
+  let fresh_n = fresh_n
+  let fresh_t t f = New (t, f)
+  let fresh_ts = fresh_ts
+
+end

Deliverables/D2.2/8051/src/utilities/bList.mli

@@ -1 +1 @@
 (** This module gives lists with internal binders. *)
 
-type ('a, 'b) t =
-  | BNil
-  | BCons of 'a * ('a, 'b) t
-  | BNew of ('b -> ('a, 'b) t)
+type ('a, 'b, 'c) t =
+  | Nil
+  | Cons of 'a * ('a, 'b, 'c) t
+  | New of 'c * ('b -> ('a, 'b, 'c) t)
 
-val (^::) : 'a -> ('a, 'b) t -> ('a, 'b) t
+type ('a, 'b) t2 = ('a, 'b, unit) t
 
-val (^@) : ('a, 'b) t -> ('a, 'b) t -> ('a, 'b) t
+val rev : ('a, 'b, 'c) t -> ('a, 'b, 'c) t
 
-val (?^) : ('b -> ('a, 'b) t) -> ('a, 'b) t
+val append : ('a, 'b, 'c) t -> ('a, 'b, 'c) t -> ('a, 'b, 'c) t
 
-val b_rev : ('a, 'b) t -> ('a, 'b) t
+val of_list : 'a list -> ('a, 'b, 'c) t
+
+val compile : ('u -> 'c -> 'u * 'b) -> 'u -> ('a, 'b, 'c) t -> 'u * 'a list
+val compile2 : ('u -> 'u * 'b) -> 'u -> ('a, 'b) t2 -> 'u * 'a list
+
+val fold_left : ('a -> 'b -> 'a) -> ('d -> ('c -> 'a) -> 'a) -> 'a ->
+  ('b, 'c, 'd) t -> 'a
+
+val fold_right :
+  ('a -> 'b -> 'b) -> ('d -> ('c -> 'b) -> 'b) -> ('a, 'c, 'd) t -> 'b -> 'b
+
+val concat : ('a, 'b, 'c) t list -> ('a, 'b, 'c) t
+
+val fresh_n : int -> ('b list -> ('a, 'b) t2) -> ('a, 'b) t2
+
+val fresh_ts : 'c list -> ('b list -> ('a, 'b, 'c) t) -> ('a, 'b, 'c) t
+
+module Notation : sig
+  val (^::) : 'a -> ('a, 'b, 'c) t -> ('a, 'b, 'c) t
+  val (^@) : ('a, 'b, 'c) t -> ('a, 'b, 'c) t -> ('a, 'b, 'c) t
+  val bnil : ('a, 'b, 'c) t
+  val fresh : ('b -> ('a, 'b) t2) -> ('a, 'b) t2
+  val fresh_n : int -> ('b list -> ('a, 'b) t2) -> ('a, 'b) t2
+  val fresh_t : 'c -> ('b -> ('a, 'b, 'c) t) -> ('a, 'b, 'c) t
+  val fresh_ts : 'c list -> ('b list -> ('a, 'b, 'c) t) -> ('a, 'b, 'c) t
+end

Deliverables/D2.2/8051/src/utilities/graphUtilities.ml

@@ -82 +82 @@
     NodeMap.filter is_reachable g
 
+  let rec put_rev freshl stmts src dests graph =
+    match stmts, dests with
+      | [], [next] -> (src, NodeMap.add src (skip next) graph)
+      | [last], _ ->
+        (src, NodeMap.add src (fill_succs last dests) graph)
+      | last :: stmts, _ ->
+        let new_l = freshl () in
+        let graph = NodeMap.add new_l (fill_succs last dests) graph in
+        (new_l, snd (put_rev freshl stmts src [new_l] graph))
+      | _ ->
+        invalid_arg "successors of statement and translation do not match"
+
+  let replace freshl lbl stmts succs g =
+    let succs = match succs with
+      | Some x -> x
+      | None -> successors (NodeMap.find lbl g) in
+
+    snd (put_rev freshl (List.rev stmts) lbl succs g)
+
+  let replace'
+      (freshl : unit -> node)
+      (freshr : 'u -> 't -> 'u * 'r)
+      (lbl : node)
+      (stmts : (statement, 'r, 't) BList.t)
+      (succs : node list option)
+      (def : 'u)
+      (g : t)
+      : 'u * t =
+    let succs = match succs with
+      | Some x -> x
+      | None -> successors (NodeMap.find lbl g) in
+    let (def, l) = BList.compile freshr def stmts in
+    (def, snd (put_rev freshl l lbl succs g))
+
+  let insert freshl lbl stmts g =
+    let stmt = NodeMap.find lbl g in
+    let succs = successors (NodeMap.find lbl g) in
+    put_rev freshl (stmt :: List.rev stmts) lbl succs g
+
+  let insert' freshl freshr lbl stmts def g =
+    let stmt = NodeMap.find lbl g in
+    let succs = successors (NodeMap.find lbl g) in
+    let (def, l) = BList.compile freshr def stmts in
+    let (lbl, g) = put_rev freshl (stmt :: l) lbl succs g in
+    (def, lbl, g)
+
 end
 
@@ -155 +201 @@
 
   let translate_with_redirects' freshl freshr f def g =
-
-    let rec put_rev stmts src dests def graph =
-      match stmts, dests with
-        | BNil, [next] -> (def, Trg.NodeMap.add src (Trg.skip next) graph)
-        | BCons (last, BNil), _ ->
-          (def, Trg.NodeMap.add src (Trg.fill_succs last dests) graph)
-        | BCons (last, stmts), _ ->
-          let new_l = freshl () in
-          let graph = Trg.NodeMap.add new_l (Trg.fill_succs last dests) graph in
-          put_rev stmts src [new_l] def graph
-        | BNew f_stmts, _ ->
-          let (def, new_r) = freshr def in
-          let stmts = f_stmts new_r in
-          put_rev stmts src dests def graph
-        | _ ->
-          invalid_arg "successors of statement and translation do not match" in
-
-    let trans lbl stmt (def, graph) =
+    let f' def lbl stmt =
       let (stmts, redirects) = f lbl stmt in
-      let succs = match redirects with
-        | Some x -> x
-        | None -> Src.successors stmt in
-      put_rev (b_rev stmts) lbl succs def graph in
-
-    Src.NodeMap.fold trans g (def, Trg.NodeMap.empty)
+      let (def, stmts) = BList.compile freshr def stmts in
+      (def, stmts, redirects) in
+    translate_with_redirects freshl f' def g
 
   let translate' freshl freshr f =
     let f' lbl stmt = (f lbl stmt, None) in
     translate_with_redirects' freshl freshr f'
+
 
 

Deliverables/D2.2/8051/src/utilities/graphUtilities.mli

@@ -64 +64 @@
   val dead_code_elim : G.t -> G.node -> G.t
 
+  val replace : (unit -> G.node) ->
+    G.node -> G.statement list -> G.node list option -> G.t -> G.t
+
+  val replace' : (unit -> G.node) -> ('u -> 't -> 'u * 'r) ->
+    G.node -> (G.statement, 'r, 't) BList.t -> G.node list option ->
+    'u -> G.t -> 'u * G.t
+
+  val insert : (unit -> G.node) ->
+    G.node -> G.statement list -> G.t -> G.node * G.t
+
+  val insert' : (unit -> G.node) -> ('u -> 't -> 'u * 'r) ->
+    G.node -> (G.statement, 'r, 't) BList.t ->
+    'u -> G.t -> 'u * G.node * G.t
+
+
 end
 
@@ -123 +138 @@
       translation.
       @see translate *)
-  val translate' : (unit -> node) -> ('u -> 'u * 'reg) ->
-    (node -> Src.statement -> (Trg.statement, 'reg) BList.t) ->
+  val translate' : (unit -> node) -> ('u -> 't -> 'u * 'reg) ->
+    (node -> Src.statement -> (Trg.statement, 'reg, 't) BList.t) ->
     'u -> Src.t -> 'u * Trg.t
 
@@ -131 +146 @@
       @see translate'
       @see translate_with_redirect *)
-  val translate_with_redirects' : (unit -> node) -> ('u -> 'u * 'reg) ->
+  val translate_with_redirects' : (unit -> node) -> ('u -> 't -> 'u * 'reg) ->
     (node -> Src.statement ->
-     (Trg.statement, 'reg) BList.t * node list option) ->
+     (Trg.statement, 'reg, 't) BList.t * node list option) ->
     'u -> Src.t -> 'u * Trg.t
 

Deliverables/D2.2/8051/src/utilities/miscPottier.ml

@@ -1 +1 @@
 
-let rec map3 f al bl cl =
+let map3 f al bl cl =
   let f' ((a, b), c) = f a b c in
   List.map f' (List.combine (List.combine al bl) cl)
+
+let fold3_right f al bl cl =
+  let f' ((a, b), c) d = f a b c d in
+  List.fold_right f' (List.combine (List.combine al bl) cl)
 
 let rec max_list = function
@@ -25 +29 @@
 
 let rec make a n =
-  if n = 0 then []
+  if n <= 0 then []
   else a :: (make a (n-1))
+
+let makei f n =
+  let rec app f k =
+  if k >= n then []
+  else f k :: (app f (k + 1)) in
+  app f 0
 
 let index_of x =
@@ -159 +169 @@
   in
   aux
+
+
+let rec sublist l k h =
+  if h < k || h < 0 || k < 0 then
+    invalid_arg "sublist: invalid interval"
+  else
+  match k, h, l with
+  | 0, 0, _ -> []
+  | 0, _, x :: l -> x :: sublist l 0 (h-1)
+  | _, _, x :: l -> sublist l (k-1) (h-1)
+  | _ -> invalid_arg "sublist: invalid interval"
+
+let rec fill l n =
+  let k = List.length l in
+  if k = 0 then invalid_arg "fill: list empty" else
+  if n < 0 then invalid_arg "fill: negative argument" else
+  if n <= k then sublist l 0 n else
+    l @ fill l (n - k)

Deliverables/D2.2/8051/src/utilities/miscPottier.mli

@@ -10 +10 @@
    size. *)
 val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
+val fold3_right : ('a -> 'b -> 'c -> 'd -> 'd) ->
+  'a list -> 'b list -> 'c list -> 'd -> 'd
 
 val max_list : 'a list -> 'a
@@ -16 +18 @@
 
 val make: 'a -> int -> 'a list
+
+val makei : (int -> 'a) -> int -> 'a list
 
 val index_of : 'a -> 'a list -> int
@@ -84 +88 @@
 
 val string_of_list: string -> ('a -> string) -> 'a list -> string
+
+(* [sublist h k l] gives the sublist of [l] starting from index [h] to
+   [k] excluded. Can raise [Invalid_argument "sublist: invalid interval"]. *)
+val sublist : 'a list -> int -> int -> 'a list
+
+(* [fill l n] makes a list of length [n] using elements from [l], possibly
+   repeating it. Raises Invalid_argument if [n < 0] or [l = []]. *)
+val fill : 'a list -> int -> 'a list
+