Ignore:
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:
6 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
  • 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
  • Deliverables/D2.2/8051/src/utilities/graphUtilities.ml

    r1580 r1584  
    8282    NodeMap.filter is_reachable g
    8383
     84  let rec put_rev freshl stmts src dests graph =
     85    match stmts, dests with
     86      | [], [next] -> (src, NodeMap.add src (skip next) graph)
     87      | [last], _ ->
     88        (src, NodeMap.add src (fill_succs last dests) graph)
     89      | last :: stmts, _ ->
     90        let new_l = freshl () in
     91        let graph = NodeMap.add new_l (fill_succs last dests) graph in
     92        (new_l, snd (put_rev freshl stmts src [new_l] graph))
     93      | _ ->
     94        invalid_arg "successors of statement and translation do not match"
     95
     96  let replace freshl lbl stmts succs g =
     97    let succs = match succs with
     98      | Some x -> x
     99      | None -> successors (NodeMap.find lbl g) in
     100
     101    snd (put_rev freshl (List.rev stmts) lbl succs g)
     102
     103  let replace'
     104      (freshl : unit -> node)
     105      (freshr : 'u -> 't -> 'u * 'r)
     106      (lbl : node)
     107      (stmts : (statement, 'r, 't) BList.t)
     108      (succs : node list option)
     109      (def : 'u)
     110      (g : t)
     111      : 'u * t =
     112    let succs = match succs with
     113      | Some x -> x
     114      | None -> successors (NodeMap.find lbl g) in
     115    let (def, l) = BList.compile freshr def stmts in
     116    (def, snd (put_rev freshl l lbl succs g))
     117
     118  let insert freshl lbl stmts g =
     119    let stmt = NodeMap.find lbl g in
     120    let succs = successors (NodeMap.find lbl g) in
     121    put_rev freshl (stmt :: List.rev stmts) lbl succs g
     122
     123  let insert' freshl freshr lbl stmts def g =
     124    let stmt = NodeMap.find lbl g in
     125    let succs = successors (NodeMap.find lbl g) in
     126    let (def, l) = BList.compile freshr def stmts in
     127    let (lbl, g) = put_rev freshl (stmt :: l) lbl succs g in
     128    (def, lbl, g)
     129
    84130end
    85131
     
    155201
    156202  let translate_with_redirects' freshl freshr f def g =
    157 
    158     let rec put_rev stmts src dests def graph =
    159       match stmts, dests with
    160         | BNil, [next] -> (def, Trg.NodeMap.add src (Trg.skip next) graph)
    161         | BCons (last, BNil), _ ->
    162           (def, Trg.NodeMap.add src (Trg.fill_succs last dests) graph)
    163         | BCons (last, stmts), _ ->
    164           let new_l = freshl () in
    165           let graph = Trg.NodeMap.add new_l (Trg.fill_succs last dests) graph in
    166           put_rev stmts src [new_l] def graph
    167         | BNew f_stmts, _ ->
    168           let (def, new_r) = freshr def in
    169           let stmts = f_stmts new_r in
    170           put_rev stmts src dests def graph
    171         | _ ->
    172           invalid_arg "successors of statement and translation do not match" in
    173 
    174     let trans lbl stmt (def, graph) =
     203    let f' def lbl stmt =
    175204      let (stmts, redirects) = f lbl stmt in
    176       let succs = match redirects with
    177         | Some x -> x
    178         | None -> Src.successors stmt in
    179       put_rev (b_rev stmts) lbl succs def graph in
    180 
    181     Src.NodeMap.fold trans g (def, Trg.NodeMap.empty)
     205      let (def, stmts) = BList.compile freshr def stmts in
     206      (def, stmts, redirects) in
     207    translate_with_redirects freshl f' def g
    182208
    183209  let translate' freshl freshr f =
    184210    let f' lbl stmt = (f lbl stmt, None) in
    185211    translate_with_redirects' freshl freshr f'
     212
    186213
    187214
  • Deliverables/D2.2/8051/src/utilities/graphUtilities.mli

    r1580 r1584  
    6464  val dead_code_elim : G.t -> G.node -> G.t
    6565
     66  val replace : (unit -> G.node) ->
     67    G.node -> G.statement list -> G.node list option -> G.t -> G.t
     68
     69  val replace' : (unit -> G.node) -> ('u -> 't -> 'u * 'r) ->
     70    G.node -> (G.statement, 'r, 't) BList.t -> G.node list option ->
     71    'u -> G.t -> 'u * G.t
     72
     73  val insert : (unit -> G.node) ->
     74    G.node -> G.statement list -> G.t -> G.node * G.t
     75
     76  val insert' : (unit -> G.node) -> ('u -> 't -> 'u * 'r) ->
     77    G.node -> (G.statement, 'r, 't) BList.t ->
     78    'u -> G.t -> 'u * G.node * G.t
     79
     80
    6681end
    6782
     
    123138      translation.
    124139      @see translate *)
    125   val translate' : (unit -> node) -> ('u -> 'u * 'reg) ->
    126     (node -> Src.statement -> (Trg.statement, 'reg) BList.t) ->
     140  val translate' : (unit -> node) -> ('u -> 't -> 'u * 'reg) ->
     141    (node -> Src.statement -> (Trg.statement, 'reg, 't) BList.t) ->
    127142    'u -> Src.t -> 'u * Trg.t
    128143
     
    131146      @see translate'
    132147      @see translate_with_redirect *)
    133   val translate_with_redirects' : (unit -> node) -> ('u -> 'u * 'reg) ->
     148  val translate_with_redirects' : (unit -> node) -> ('u -> 't -> 'u * 'reg) ->
    134149    (node -> Src.statement ->
    135      (Trg.statement, 'reg) BList.t * node list option) ->
     150     (Trg.statement, 'reg, 't) BList.t * node list option) ->
    136151    'u -> Src.t -> 'u * Trg.t
    137152
  • Deliverables/D2.2/8051/src/utilities/miscPottier.ml

    r818 r1584  
    11
    2 let rec map3 f al bl cl =
     2let map3 f al bl cl =
    33  let f' ((a, b), c) = f a b c in
    44  List.map f' (List.combine (List.combine al bl) cl)
     5
     6let fold3_right f al bl cl =
     7  let f' ((a, b), c) d = f a b c d in
     8  List.fold_right f' (List.combine (List.combine al bl) cl)
    59
    610let rec max_list = function
     
    2529
    2630let rec make a n =
    27   if n = 0 then []
     31  if n <= 0 then []
    2832  else a :: (make a (n-1))
     33
     34let makei f n =
     35  let rec app f k =
     36  if k >= n then []
     37  else f k :: (app f (k + 1)) in
     38  app f 0
    2939
    3040let index_of x =
     
    159169  in
    160170  aux
     171
     172
     173let rec sublist l k h =
     174  if h < k || h < 0 || k < 0 then
     175    invalid_arg "sublist: invalid interval"
     176  else
     177  match k, h, l with
     178  | 0, 0, _ -> []
     179  | 0, _, x :: l -> x :: sublist l 0 (h-1)
     180  | _, _, x :: l -> sublist l (k-1) (h-1)
     181  | _ -> invalid_arg "sublist: invalid interval"
     182
     183let rec fill l n =
     184  let k = List.length l in
     185  if k = 0 then invalid_arg "fill: list empty" else
     186  if n < 0 then invalid_arg "fill: negative argument" else
     187  if n <= k then sublist l 0 n else
     188    l @ fill l (n - k)
  • Deliverables/D2.2/8051/src/utilities/miscPottier.mli

    r818 r1584  
    1010   size. *)
    1111val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
     12val fold3_right : ('a -> 'b -> 'c -> 'd -> 'd) ->
     13  'a list -> 'b list -> 'c list -> 'd -> 'd
    1214
    1315val max_list : 'a list -> 'a
     
    1618
    1719val make: 'a -> int -> 'a list
     20
     21val makei : (int -> 'a) -> int -> 'a list
    1822
    1923val index_of : 'a -> 'a list -> int
     
    8488
    8589val string_of_list: string -> ('a -> string) -> 'a list -> string
     90
     91(* [sublist h k l] gives the sublist of [l] starting from index [h] to
     92   [k] excluded. Can raise [Invalid_argument "sublist: invalid interval"]. *)
     93val sublist : 'a list -> int -> int -> 'a list
     94
     95(* [fill l n] makes a list of length [n] using elements from [l], possibly
     96   repeating it. Raises Invalid_argument if [n < 0] or [l = []]. *)
     97val fill : 'a list -> int -> 'a list
     98
Note: See TracChangeset for help on using the changeset viewer.