From 278f3697e16d5e7d79326cb3d859f87e5efdb2b3 Mon Sep 17 00:00:00 2001 From: Aliaume Lopez Date: Mon, 18 Jul 2016 10:17:43 +0100 Subject: [PATCH] Rewriting huge progress --- circuits.ml | 728 ++++++++++++++++++++++++++++++++++++++++----------- ptg.ml | 624 +++++++++++++++++++++++++++++++++++++++++++ rewriting.ml | 475 +++++++++++++++++++++++++++++++++ utils.ml | 16 +- 4 files changed, 1683 insertions(+), 160 deletions(-) create mode 100644 ptg.ml create mode 100644 rewriting.ml diff --git a/circuits.ml b/circuits.ml index b127a0d..6634920 100644 --- a/circuits.ml +++ b/circuits.ml @@ -2,24 +2,40 @@ * * circuits.ml * - * Dan Ghica + * Aliaume Lopez * - * Entry point of the program - * generates dot output, - * handles graph reduction, - * embedded DSL, and all. + * TODO * - * « aliaume hook » is the - * hook from all the rest of - * the librairies into this - * file to interface the new - * language and definition to - * the new model + * 1) rules + * a) Dangle : propagating disconnect nodes + * b) Garbage collect nodes + * c) fork constant + * d) gate reduce (end the work) + * + * 3) compiling from dags + * + * 4) waveforms ? * *) open Dot;; +let rec zip_with_3 f a b c = match (a,b,c) with + | [],[],[] -> [] + | a1::a2,b1::b2,c1::c2 -> + (f a1 b1 c1) :: zip_with_3 f a2 b2 c2;; + +let rec zip_with_4 f a b c d = match (a,b,c,d) with + | [],[],[],[] -> [] + | a1::a2,b1::b2,c1::c2,d1::d2 -> + (f a1 b1 c1 d1) :: zip_with_4 f a2 b2 c2 d2;; + +let rec zip_with f a b = match (a,b) with + | [],[] -> [] + | a1::a2,b1::b2 -> + (f a1 b1) :: zip_with f a2 b2;; + + module ComparableInts = struct type t = int @@ -104,8 +120,6 @@ type label = * *) type ptg = { - maxid : int; (* the maximum id inside the graph *) - (* naturally have a notion of order *) iports : nid list; oports : nid list; @@ -134,26 +148,6 @@ type ptg = { } -(*** PRETTY PRINTING ***) -let string_of_gate = function - | Fork -> "F" - | Join -> "J" - | Nmos -> "N" - | Pmos -> "P" - | Box s -> "B " ^ s - | Wait -> "W" - | Mux -> "M" - | Disconnect -> "D";; - -let string_of_value = function - | High -> "H" - | Low -> "L" - | Top -> "T" - | Bottom -> "Z";; - -let string_of_label = function - | Value v -> string_of_value v - | Gate g -> string_of_gate g;; (** @@ -195,31 +189,6 @@ let pp_ptg ptg = ptg |> string_of_ptg |> print_string;; (**** DOT CONVERSION ****) -let example_ptg = - { - maxid = 6; - - iports = [1;2]; - oports = [3]; - - traced = []; - delays = []; - - nodes = [(0,4,0); - (0,5,9); - (2,6,1)]; - - labels = id_empty |> id_add 4 (Gate Fork) - |> id_add 5 (Gate Join) - |> id_add 6 (Gate (Box "Test")); - - edges = [ (1,None,4,None); - (2,None,5,None); - (4,None,6,Some 1); - (5,None,6,Some 2); - (6,Some 1, 3, None) ] - };; - let dot_of_ptg ptg = let init_rank = rank_group "min" ptg.iports in @@ -284,21 +253,48 @@ let newid () = let newids n = Utils.range n |> List.map (fun _ -> newid ());; -(** Duplique un ptg **) +(** TEMPORARY FUNCTIONS **) +let make_arrow x y = + (x,None,y,None);; + +(** Working on edges **) +let is_from ~node:n ~edge:e = + match e with + | (a,_,_,_) -> a = n;; + +let is_to ~node:n ~edge:e = + match e with + | (_,_,a,_) -> a = n;; + +let is_from_l ~nodes:l ~edge:e = + List.exists (fun x -> is_from x e) l;; + +let is_to_l ~nodes:l ~edge:e = + List.exists (fun x -> is_to x e) l;; + +let set_from ~node:n ~edge:(x,y,z,t) = (n,y,z,t);; +let set_to ~node:n ~edge:(x,y,z,t) = (x,y,n,t);; + + +(** + * Create a copy of the ptg with + * a disjoint set of nodes + * along with the translation function + *) let replicate ptg = - let translate x = x + ptg.maxid in + let m = !counter in + let translate x = x + m + 1 in let update_label m (oldid,lbl) = id_add (translate oldid) lbl m in - counter := translate !counter; + counter := translate m; (translate, { - maxid = translate ptg.maxid; - + iports = List.map translate ptg.iports; - oports = List.map translate ptg.iports; + oports = List.map translate ptg.oports; traced = List.map translate ptg.traced; delays = List.map translate ptg.delays; @@ -315,70 +311,90 @@ let replicate ptg = });; -(** Working on edges **) -let is_from ~node:n ~edge:e = - match e with - | (a,_,_,_) -> a = n;; +let pre_nodes ~node:n t = + t.edges |> List.filter (fun e -> is_to ~node:n ~edge:e);; -let is_to ~node:n ~edge:e = - match e with - | (_,_,a,_) -> a = n;; +let post_nodes ~node:n t = + t.edges |> List.filter (fun e -> is_from ~node:n ~edge:e);; -let is_from_l ~nodes:l ~edge:e = - List.exists (fun x -> is_from x e) l;; -let is_to_l ~nodes:l ~edge:e = - List.exists (fun x -> is_to x e) l;; +let remove_node ~node:n t = + let node_rem (_,x,_) = not (x = n) in + let simple_rem x = not (x = n) in + let edge_rem e = + (is_from ~node:n ~edge:e) || (is_to ~node:n ~edge:e) + in -let set_from ~node:n ~edge:(x,y,z,t) = (n,y,z,t);; -let set_to ~node:n ~edge:(x,y,z,t) = (x,y,n,t);; + { + edges = List.filter edge_rem t.edges ; + nodes = List.filter node_rem t.nodes ; + iports = List.filter simple_rem t.iports ; + oports = List.filter simple_rem t.oports ; + traced = List.filter simple_rem t.traced ; + delays = List.filter simple_rem t.delays ; -(** Split the trace of a pTG + labels = id_remove n t.labels + };; + +(** * - **) -let split_trace ptg = - let trids = newids (List.length ptg.traced) in - let corres = List.combine ptg.traced trids in - let edge_mod (oldt,newt) e = - if is_from ~node:oldt ~edge:e then - set_from ~node:newt ~edge:e - else - e + * Remove a _main_ node + * + * Create new Disconnect for the pre + * Create new Bottoms for the post + * + * --> this way the circuit is always + * correct : no strange modifications + * + * *) +let remove_node_safe ~node:n t = + let bottoms = ref [] in + let discard = ref [] in + let new_bottom () = + let x = newid () in + bottoms := x :: !bottoms; + x in - let update_edges l p = - l |> List.map (edge_mod p) + let new_discard () = + let x = newid () in + discard := x :: !discard; + x in - let traced_to_main x = (1,x,1) in - (corres, { - ptg with - maxid = !counter; - traced = []; - nodes = List.map traced_to_main (ptg.traced @ trids) @ ptg.nodes; - edges = List.fold_left update_edges ptg.edges corres; - });; -(** Remove a _main_ node *) -let remove_node ~node:n t = - let edge_rem e = - not (is_from ~node:n ~edge:e || is_to ~node:n ~edge:e) + let edge_mod e = + if is_from ~node:n ~edge:e then + let (_,_,x,i) = e in + (new_bottom (), None, x, i) + else if is_to ~node:n ~edge:e then + let (x,i,_,_) = e in + (x, i, new_discard (), None) + else + e in + let node_rem (_,x,_) = not (x = n) in let simple_rem x = not (x = n) in + + let add_bottoms l = + List.fold_left (fun a b -> id_add b (Value Bottom) a) l !bottoms + in + + let add_discard l = + List.fold_left (fun a b -> id_add b (Gate Disconnect) a) l !discard + in + { t with - edges = List.filter edge_rem t.edges ; - nodes = List.filter node_rem t.nodes ; + edges = List.map edge_mod t.edges ; + nodes = List.map (fun x -> (0,x,0)) !bottoms + @ List.map (fun x -> (0,x,0)) !discard + @ List.filter node_rem t.nodes ; traced = List.filter simple_rem t.traced ; delays = List.filter simple_rem t.delays ; oports = List.filter simple_rem t.oports ; iports = List.filter simple_rem t.iports ; - labels = t.labels |> id_remove n; + labels = t.labels |> id_remove n |> add_bottoms |> add_discard };; -let pre_nodes ~node:n t = - t.edges |> List.filter (fun e -> is_to ~node:n ~edge:e);; - -let post_nodes ~node:n t = - t.edges |> List.filter (fun e -> is_from ~node:n ~edge:e);; let relabel_node ~node:n ~label:l t = { @@ -388,6 +404,9 @@ let relabel_node ~node:n ~label:l t = |> id_add n l };; +let relabel_l ~nodes:ns ~label:l t = + List.fold_left (fun b a -> relabel_node ~node:a ~label:l b) t ns;; + (** adding an edge * * Does not include sanity checks @@ -399,6 +418,17 @@ let add_edge ~edge:e t = edges = e :: t.edges };; +let add_node ~node:e t = + { t with + nodes = (0,e,0) :: t.nodes + };; + +let add_nodes ~nodes:l t = + List.fold_left + (fun a b -> add_node ~node:b a) + t + l;; + (** * Try moving a node to main, * does nothing if main already exists @@ -408,7 +438,7 @@ let move_to_main ~node:n t = let simple_rem x = not (x = n) in if try_find = [] then { t with - nodes = (1,n,1) :: t.nodes; + nodes = (0,n,0) :: t.nodes; traced = List.filter simple_rem t.traced ; delays = List.filter simple_rem t.delays ; oports = List.filter simple_rem t.oports ; @@ -417,6 +447,75 @@ let move_to_main ~node:n t = else t;; +let flatten_ptg g = + let others = g.iports @ g.oports @ g.traced @ g.delays in + List.fold_left (fun a b -> move_to_main ~node:b a) + g others;; + +let merger_v k x y = + match x with + | Some v -> Some v + | None -> y;; + +(** + * The two graphs have + * distinct node names + *) +let ptg_merge g1 g2 = + { + nodes = (flatten_ptg g1).nodes @ (flatten_ptg g2).nodes ; + delays = []; + traced = []; + iports = []; + oports = []; + + labels = id_merge merger_v g1.labels g2.labels; + + edges = g1.edges @ g2.edges; + };; + + +(** Dispatch nodes *) +let dispatch_with ~f ~from1 ~from2 ~fst ~snd g = + let make_edge a b c d = + if f c d g then + [ + (a,None,c,None); + (b,None,d,None) + ] + else + [ + (b,None,c,None); + (a,None,d,None) + ] + in + { g with + edges = List.concat (zip_with_4 make_edge from1 from2 fst snd) @ g.edges + };; + +let set_inputs ~nodes:l ptg = + { + ptg with + iports = l + };; + +let set_outputs ~nodes:l ptg = + { + ptg with + oports = l + };; + +let set_delays ~nodes:l ptg = + { + ptg with + delays = l + };; + +let set_trace ~nodes:l ptg = + { + ptg with + traced = l + };; (** * Checks if a node is in the main * graph (not special set) @@ -431,6 +530,97 @@ let delete_label ~node:n t = labels = t.labels |> id_remove n };; +let delete_label_l ~nodes:n t = + List.fold_left + (fun a b -> delete_label ~node:b a) + t + n;; + +let connect ~from:i ~towards:j ptg = + { ptg with + edges = zip_with make_arrow i j @ ptg.edges + };; + +let mk_join ~towards ~fst ~snd ptg = + let new_joins = newids (List.length towards) in + ptg |> add_nodes ~nodes:new_joins + |> connect ~from:fst ~towards:new_joins + |> connect ~from:snd ~towards:new_joins + |> connect ~from:new_joins ~towards:towards + |> relabel_l ~nodes:new_joins ~label:(Gate Join);; + +let mk_fork ~from ~fst ~snd ptg = + let new_forks = newids (List.length from) in + ptg |> add_nodes ~nodes:new_forks + |> connect ~from:new_forks ~towards:fst + |> connect ~from:new_forks ~towards:snd + |> connect ~from:from ~towards:new_forks + |> relabel_l ~nodes:new_forks ~label:(Gate Fork);; + + +let rec fork_into ~node:n ~nodes:l ptg = + match l with + | [] -> ptg + | [t] -> + ptg |> add_edge ~edge:(n,None,t,None) + | t :: q -> + let fork_node = newid () in + ptg |> fork_into ~node:fork_node ~nodes:q + |> add_node ~node:fork_node + |> relabel_node ~node:fork_node ~label:(Gate Fork) + |> add_edge ~edge:(fork_node,None,t,None) + |> add_edge ~edge:(n,None,fork_node,None);; + +let rec join_into ~node:n ~nodes:l ptg = + match l with + | [] -> ptg + | [t] -> + ptg |> add_edge ~edge:(t,None,n,None) + | t :: q -> + let join_node = newid () in + ptg |> join_into ~node:join_node ~nodes:q + |> add_node ~node:join_node + |> relabel_node ~node:join_node ~label:(Gate Join) + |> add_edge ~edge:(t,None,join_node,None) + |> add_edge ~edge:(join_node,None,n,None);; + + +(** Split the trace of a pTG + * + **) +let split_trace ptg = + let trids = newids (List.length ptg.traced) in + let corres = List.combine ptg.traced trids in + let edge_mod (oldt,newt) e = + if is_from ~node:oldt ~edge:e then + set_from ~node:newt ~edge:e + else + e + in + let update_edges l p = + l |> List.map (edge_mod p) + in + let traced_to_main_left x = (0,x,0) in + let traced_to_main_right x = (0,x,0) in + (trids, ptg.traced, { + ptg with + traced = []; + nodes = List.map traced_to_main_left ptg.traced + @ List.map traced_to_main_right trids + @ ptg.nodes; + edges = List.fold_left update_edges ptg.edges corres; + });; + + +(*** + * The original PTG does not have any trace + *) +let connect_trace ~from:i ~towards:j ptg = + let new_trace = newids (List.length i) in + ptg |> connect ~from:i ~towards:new_trace + |> connect ~from:new_trace ~towards:j + |> set_trace ~nodes:new_trace;; + (** * Change a node's signature * and the edges according to @@ -470,6 +660,7 @@ let signature_node ~node:n ~ins:i ~outs:j t = (** * pass a constant node through * a simple node + * the node can be a traced one *) let propagate_constant ~node:n t = match id_find n t.labels with @@ -483,7 +674,7 @@ let propagate_constant ~node:n t = | None -> false | Some _ -> true in - (* + (* * replace the node if and only if there is * only us on the node, and it is a non-labeled * node @@ -507,14 +698,17 @@ let propagate_constant ~node:n t = let simplify_identity ~node:n t = match id_find n t.labels with | None -> - begin (* an unlabeled node is ALWAYS an identity *) - let [x,i,_,_] = pre_nodes ~node:n t in - let [_,_,y,j] = post_nodes ~node:n t in - if is_main_node ~node:x t && is_main_node ~node:y t then - t |> remove_node ~node:n - |> add_edge ~edge:(x,i,y,j) - else - t + begin + try + let [x,i,_,_] = pre_nodes ~node:n t in + let [_,_,y,j] = post_nodes ~node:n t in + if is_main_node ~node:x t && is_main_node ~node:y t then + t |> remove_node ~node:n + |> add_edge ~edge:(x,i,y,j) + else + t + with + Match_failure _ -> t end | Some _ -> t;; @@ -553,14 +747,14 @@ let reduce_mux ~node:mux t = in match v1 with | Top -> - first |> relabel_node ~node:p2 ~label:(Gate Disconnect) - |> relabel_node ~node:p3 ~label:(Gate Disconnect) - |> relabel_node ~node:mux ~label:(Value Top) + first |> relabel_node ~node:p2 ~label:(Gate Disconnect) + |> relabel_node ~node:p3 ~label:(Gate Disconnect) + |> relabel_node ~node:mux ~label:(Value Top) |> signature_node ~node:mux ~ins:0 ~outs:0 | Bottom -> - first |> relabel_node ~node:p2 ~label:(Gate Disconnect) - |> relabel_node ~node:p3 ~label:(Gate Disconnect) - |> relabel_node ~node:mux ~label:(Value Bottom) + first |> relabel_node ~node:p2 ~label:(Gate Disconnect) + |> relabel_node ~node:p3 ~label:(Gate Disconnect) + |> relabel_node ~node:mux ~label:(Value Bottom) |> signature_node ~node:mux ~ins:0 ~outs:0 | Low -> first @@ -575,55 +769,283 @@ let reduce_mux ~node:mux t = | _ -> t;; +let join_values a b = match a,b with + | Bottom,_ -> b + | _,Bottom -> a + | High,Low -> Top + | Low,High -> Top + | Top,_ -> Top + | _,Top -> Top + | _ -> a;; (* otherwise a = b = join a b *) + +(* TODO nmos & pmos table *) +let nmos_values a b = a;; +let pmos_values a b = a;; + +let function_of_gate = function + | Join -> join_values + | Nmos -> nmos_values + | Pmos -> pmos_values ;; + +let reduce_gate ~node:n ptg = + match id_find n ptg.labels with + | Some (Gate Mux) -> reduce_mux ~node:n ptg + | Some (Gate g) when List.mem g [Join;Nmos;Pmos] -> + begin + let inputs = pre_nodes ~node:n ptg in + let trait_inpt (x,j,_,i) = (j,x,i, id_find x ptg.labels) in + let compare_input (_,_,i,_) (_,_,j,_) = compare i j in + let real_inputs = inputs + |> List.map trait_inpt + |> List.sort compare_input + |> List.map (fun (j,x,_,y) -> (j,x,y)) + in + match real_inputs with + | [(_ ,p1,Some (Value v1)); + (k2,p2,Some (Value v2)) ] -> + begin + ptg |> remove_node ~node:p1 + |> remove_node ~node:p2 + |> signature_node ~node:n ~ins:0 ~outs:0 (** set regular node **) + |> relabel_node ~node:n ~label:(Value (function_of_gate g v1 v2)) + end + (* TODO pmos AND nmos short circuit *) + (* TODO join short circuit too *) + | _ -> ptg -let reduce_times ptg1 = - let ptg2 = replicate ptg1 in - let new_inputs = ... in - - dispatch f new_inputs ptg1.inputs ptg2.inputs + end + | _ -> ptg;; - mk_join new_outputs ptg1.outputs ptg2.outputs - relabel ptg1.outputs DELAY +let yank_constant ~node:n ptg = + match id_find n ptg.labels with + | Some (Value v) -> + begin + match post_nodes ~node:n ptg with + | [(_,_,t,_)] -> + if List.mem t ptg.traced then + ptg |> remove_node ~node:n + |> move_to_main ~node:t + |> relabel_node ~node:t ~label:(Value v) + else + ptg + | _ -> ptg + end + | _ -> ptg;; + - (a,b) = split_trace +let propagate_fork ~node:n ptg = + match id_find n ptg.labels with + | Some (Gate Fork) -> + begin + match (pre_nodes ~node:n ptg, post_nodes ~node:n ptg) with + | [(x,_,_,_)], [(_,_,a,_);(_,_,b,_)] -> + begin + match id_find x ptg.labels with + | Some (Value v) -> + let y = newid () in + + ptg |> remove_node ~node:n + |> add_node ~node:y + |> relabel_node ~node:y ~label:(Value v) + |> connect ~from:[x;y] ~towards:[a;b] + | _ -> ptg + end + | _ -> ptg + end + | _ -> ptg;; - new_trace - dispatch new_trace a1 a2 +let dangling_fork ~node:n ptg = ();; +let dangling_trace ~node:n ptg = ();; - relink new_trace b1 - ignore b2 +let dangling_node ~node:n ptg = + ptg |> dangling_fork ~node:n + |> dangling_trace ~node:n;; - - +(** + * Mark nodes + *) +let rec mark_nodes ~seen ~nexts ptg = + match nexts with + | [] -> seen + | t :: q -> + if List.mem t seen then + mark_nodes ~seen:seen ~nexts:q ptg + else + let pre_nodes = pre_nodes ~node:t ptg + |> List.map (fun (x,_,_,_) -> x) + in + mark_nodes ~seen:(t :: seen) + ~nexts:(pre_nodes @ q) + ptg;; (** * - * unfolding ptg + * The mark and sweep + * phase + * + * + * FIXME : wrong wrong and wrong * *) -let unfold_ptg t1 = - let t2 = t1 |> replicate |> reduce_times in +let mark_and_sweep t = + let reachable = mark_nodes ~seen:[] ~nexts:t.oports t in + let filter_func (_,x,_) = List.mem x reachable in + let nodes_to_delete = List.filter filter_func t.nodes in + List.fold_left (fun a b -> remove_node_safe ~node:b a) + t + (List.map (fun (_,x,_) -> x) nodes_to_delete);; + +(* + * TODO + * convince that it does the right thing + *) +let rewrite_delays g1 = + let (_, g2) = replicate g1 in + + let (pre1,post1,g1) = split_trace g1 in + let (pre2,post2,g2) = split_trace g2 in + + (* Creating new special nodes *) + let new_trace = newids (List.length post1) in + let new_inputs = newids (List.length g1.iports) in + let new_delays = newids (List.length g1.oports) in + let new_outputs = newids (List.length g1.oports) in + + let bottoms_pre = newids (List.length post1) in + let bottoms_ipts = newids (List.length g1.iports) in + + + let is_delayed a _ g = + match post_nodes ~node:a g with + | [_,_,x,_] -> + begin + match id_find x g.labels with + | Some (Gate Wait) -> true + | _ -> false + end + | _ -> false + in + - let (a,b,c) = split_trace t1 in - let (e,f,g) = split_trace t2 in + ptg_merge g1 g2 + |> relabel_l ~nodes:post2 + ~label:(Gate Disconnect) - connect b,e - connect b,a + |> dispatch_with ~f:is_delayed + ~from1:new_trace + ~from2:bottoms_pre + ~fst:pre1 + ~snd:pre2 - set_trace a - set_forks b + |> dispatch_with ~f:is_delayed + ~from1:new_inputs + ~from2:bottoms_ipts + ~fst:g1.iports + ~snd:g2.iports - ignore c - ignore t1.inputs + |> connect_trace ~from:new_trace + ~towards:post1 + |> add_nodes ~nodes:(bottoms_pre @ bottoms_ipts) - - retime ;; + |> add_nodes ~nodes:new_delays + + |> relabel_l ~nodes:(bottoms_pre @ bottoms_ipts) + ~label:(Value Bottom) + + |> delete_label_l ~nodes:g1.delays + |> delete_label_l ~nodes:g2.delays + + |> connect ~from:g1.oports + ~towards:new_delays + |> mk_join ~fst:new_delays + ~snd:g2.oports + ~towards:new_outputs + + |> set_inputs ~nodes:new_inputs + |> set_delays ~nodes:[] + |> set_outputs ~nodes:new_outputs;; + +(** + * + * TODO faire plus haut nivea encore !!! + * + * parce que là on change le label, mais il faut + * aussi changer le type ?! + * + *) +let unfold_trace g1 = + let (_,g2) = replicate g1 in + + let new_inputs = newids (List.length g1.iports) in + + let (pre1,post1,g1) = split_trace g1 in + let (pre2,post2,g2) = split_trace g2 in + + + ptg_merge g1 g2 + |> relabel_l ~nodes:post2 ~label:(Gate Disconnect) + |> relabel_l ~nodes:g1.oports ~label:(Gate Disconnect) + |> relabel_l ~nodes:post1 ~label:(Gate Fork) + |> mk_fork ~from:post1 ~fst:pre2 ~snd:pre1 + |> set_trace ~nodes:pre1 + |> mk_fork ~from:new_inputs ~fst:g1.iports ~snd:g2.iports + |> set_inputs ~nodes:new_inputs + |> set_outputs ~nodes:g2.oports;; -(* TODO understand dangling nodes *) +let example_ptg = + { + iports = [1;2]; + oports = [3]; + + traced = []; + delays = []; + + nodes = [(0,4,0); + (0,5,9); + (2,6,1)]; + + labels = id_empty |> id_add 4 (Gate Fork) + |> id_add 5 (Gate Join) + |> id_add 6 (Gate (Box "Test")); + + edges = [ (1,None,4,None); + (2,None,5,None); + (4,None,6,Some 1); + (5,None,6,Some 2); + (6,Some 1, 3, None) ] + };; + +let empty_ptg = + { iports = []; oports = []; traced = []; delays = []; nodes = []; labels = id_empty; edges = [] };; + +let example_ptg_2 = + counter := 9; + empty_ptg |> add_nodes ~nodes:[2;3;4;5;6] + |> set_inputs ~nodes:[1] + |> set_trace ~nodes:[7] + |> add_edge ~edge:(1,None,2,None) + |> add_edge ~edge:(2,None,3,None) + |> add_edge ~edge:(3,None,4,None) + |> add_edge ~edge:(4,None,5,None) + |> add_edge ~edge:(5,None,6,None) + |> add_edge ~edge:(6,None,7,None) + |> add_edge ~edge:(7,None,2,None) + |> relabel_node ~node:2 ~label:(Gate Join);; + +let () = + example_ptg_2 + |> (fun ptg -> + List.fold_left (fun a b -> simplify_identity ~node:b a) + ptg + (List.map (fun (_,x,_) -> x) ptg.nodes)) + |> unfold_trace + |> dot_of_ptg |> print_string;; + + diff --git a/ptg.ml b/ptg.ml new file mode 100644 index 0000000..ead0f67 --- /dev/null +++ b/ptg.ml @@ -0,0 +1,624 @@ +(*** + * + * + * The file containing all + * the internal definition + * of pTG and operations + * on them. + * + * This is different from dags.ml + * because dags is the graph structure + * to compile (handles variables, etc ...) + * but not optimised to do rewriting + * (one way arrows, lists instead of maps ...) + * + *) + + +let rec zip f a b = match (a,b) with + | [],[] -> [] + | a :: b, c :: d -> f a c :: zip f b d ;; + +let rec remove_once p l = match l with + | [] -> [] + | t :: q when p = t -> q + | t :: q -> t :: remove_once p q;; + +let rec replace_once a b l = match l with + | [] -> [] + | t :: q when t = a -> b :: q + | t ::q -> t :: replace_once a b q;; + + + +(*** THE MAP UTILITIES ***) + + +module ComparableInts = +struct + type t = int + let compare = compare +end;; + + +module IntegerDictionary = Map.Make (ComparableInts);; + +type 'a mapping = 'a IntegerDictionary.t;; + +type nid = int;; + +let id_empty = IntegerDictionary.empty +let id_add = IntegerDictionary.add +let id_map = IntegerDictionary.map +let id_mapi = IntegerDictionary.mapi +let id_filter = IntegerDictionary.filter +let id_fold = IntegerDictionary.fold +let id_merge = IntegerDictionary.merge +let id_bindings = IntegerDictionary.bindings +let id_remove = IntegerDictionary.remove +let id_mem = IntegerDictionary.mem +let id_singleton = IntegerDictionary.singleton +let id_find x y = + try + Some (IntegerDictionary.find x y) + with + Not_found -> None;; + +let id_update k f y = + match f (id_find k y) with + | None -> id_remove k y + | Some x -> id_add k x y;; + +let merger_v k a b = match a, b with + | None , None -> None + | Some a, None -> Some a + | None , Some b -> Some b + | Some a, Some b when a = b -> Some a + | Some a, Some b -> Some a ;; (** default value ... Careful !!!*) + + +type gate = + | Fork + | Join + | Nmos + | Pmos + | Box of string + | Wait + | Mux;; + +type value = + | High + | Low + | Top + | Bottom;; + + +type label = + | Disconnect (* dangling node *) + | Value of value + | Gate of gate;; + + +(**** + * + * The pTG + * + * iports : a connection giving the input nodes in order + * oports : a connection giving the output nodes in order + * + * traced : a connection giving the traced nodes with an (arbitrary) order + * delays : a connection giving the delayed nodes with an (arbitrary) order + * + * labels : a mapping from nodes to their labels + * if a node is not found in the map, + * the label is the empty label + * + * edges : a mapping from a node to a list + * representing it's « sons » IN ORDER + * + * co-edeges : a mapping from nodes to a connection + * representing it's « parents » + * IN ORDER + * + *) +type ptg = { + (* naturally have a notion of order *) + iports : nid list; + oports : nid list; + + (* + * impose a notion of order to simplify + * ulterior modification + *) + traced : nid list; (* 1 input 1 output *) + delays : nid list; (* 1 input 1 output *) + + (* nodes that are not iport or oport or traced or delays *) + nodes : nid list; + + (* only need to store the labels to have the nodes + * this time the labelling function is total and + * we have an CONNECTOR label for connecting nodes + *) + labels : label mapping; + + (* edges in right order *) + edges : (nid list) mapping; + (* edges for the dual graph *) + co_edges : (nid list) mapping; +};; + + + +(**** PRETTY PRINTING ****) + +let string_of_gate = function + | Fork -> "F" + | Join -> "J" + | Nmos -> "N" + | Pmos -> "P" + | Box s -> "B " ^ s + | Wait -> "W" + | Mux -> "M";; + +let string_of_value = function + | High -> "H" + | Low -> "L" + | Top -> "T" + | Bottom -> "Z";; + +let string_of_label = function + | Disconnect -> "D" + | Value v -> string_of_value v + | Gate g -> string_of_gate g;; + +let string_of_ptg ptg = + (* TODO add the pretty printing of labels *) + let structure = [ + "BEGIN"; + "\tINPUTS : "; + ptg.iports |> List.map (fun x -> string_of_int x) |> String.concat ", "; + "\tOUTPUTS : "; + ptg.oports |> List.map (fun x -> string_of_int x) |> String.concat ", "; + "\tTRACED : "; + ptg.traced |> List.map (fun x -> string_of_int x) |> String.concat ", "; + "\tDELAYS : "; + ptg.delays |> List.map (fun x -> string_of_int x) |> String.concat ", "; + "\tEDGES"; + ptg.edges |> id_bindings + |> List.map (fun (x,l) -> List.map (fun k -> (x,k)) l) + |> List.concat + |> List.map (fun (x,y) -> + "\t\t " ^ string_of_int x ^ " -> " + ^ string_of_int y) + |> String.concat "\n"; + ] in + structure |> String.concat "\n";; + + +(* UNIQUE NODE ID PROVIDER *) +let counter = ref 0;; +let newid () = + incr counter; !counter;; + +let newids n = Utils.range n |> List.map (fun _ -> newid ());; + +(**** BASE OPERATIONS ****) + +(* Node insertion *) +let trace_add ~node:n t = + { t with + traced = n :: t.traced + };; + +let delay_add ~node:n t = + { t with + delays = n :: t.delays + };; + +let iport_add ~node:n t = + { t with + iports = n :: t.iports + };; + +let oport_add ~node:n t = + { t with + oports = n :: t.oports + };; + +let main_add ~node:n t = + { t with + nodes = n :: t.nodes + };; + + + +(* Node neighbourhood exploration *) + +let pre_nodes ~node:n t = + match id_find n t.co_edges with + | Some l -> l + | None -> [];; + +let post_nodes ~node:n t = + match id_find n t.edges with + | Some l -> l + | None -> [];; + + +(* Edge construction and destruction + * adding an EDGE at the TOP of the list + * for both nodes ... + * + * It will use the first available output + * and the first available input + * + * *) +let edge_add ~from:n ~towards:m t = + let insert_node node = function + | None -> Some [node] + | Some l -> Some (node :: l) + in + + { t with + edges = id_update n (insert_node m) t.edges; + co_edges = id_update m (insert_node n) t.co_edges; + };; + +(* + * Removes a node from the list of neighbours + * WARNING: KEEPS THE ORDER FROM THE LIST, BUT DOES NOT + * KEEP THE ASSOCIATED PORT !!! + * + * WARNING 2: removes only _one_ edge between two nodes + * (it could be that they share several connection + * on different ports) + *) +let edge_rem ~from:n ~towards:m t = + let update_func node = function + | Some l when List.mem node l -> Some (remove_once node l) + | _ -> failwith "edge already removed !!! (edge_rem)" + in + { t with + edges = id_update n (update_func m) t.edges; + co_edges = id_update m (update_func n) t.co_edges; + };; + +(* Label updating *) +let label_set ~node:n ~label:l t = + { t with + labels = id_add n l t.labels ; + };; + +let label_rem ~node:n t = + { t with + labels = id_remove n t.labels ; + };; + +let label_update ~node:n ~f t = + { t with + labels = id_update n f t.labels ; + };; + +(* Node deletion + * + * NO SAFETY CHECK !!!! + * + * TODO should also delete + * the edges going in and + * out of the node !!! + * + * *) + + + +let trace_rem ~node:n t = + { t with + traced = List.filter ((<>) n) t.traced; + };; + +let delay_rem ~node:n t = + { t with + delays = List.filter ((<>) n) t.delays; + labels = id_remove n t.labels; + };; + +let iport_rem ~node:n t = + { t with + iports = List.filter ((<>) n) t.iports ; + };; + +let oport_rem ~node:n t = + { t with + oports = List.filter ((<>) n) t.iports ; + };; + +let main_rem ~node:n t = + { t with + nodes = List.filter ((<>) n) t.nodes ; + labels = id_remove n t.labels; + };; + +(** some helpful function *) +let batch ~nodes:nds ~f t = + List.fold_left (fun a b -> f ~node:b a) t nds;; + +let apply ~f ~elems:nds t = (* generic function batch *) + List.fold_left (fun a b -> f b a) t nds;; + +(** removes all the edges going in and out of a node *) +let node_edges_rem ~node:n t = + let pre = pre_nodes ~node:n t in + let post = post_nodes ~node:n t in + t |> apply ~f:(fun x -> edge_rem ~from:n ~towards:x) ~elems:post + |> apply ~f:(fun x -> edge_rem ~from:x ~towards:n) ~elems:pre;; + +(** global pre/post disconnection *) +let pre_disconnect ~node:n t = + let p = pre_nodes ~node:n t in + apply ~f:(fun x -> edge_rem ~from:x ~towards:n) ~elems:p t;; + +let post_disconnect ~node:n t = + let p = post_nodes ~node:n t in + apply ~f:(fun x -> edge_rem ~from:n ~towards:x) ~elems:p t;; + + +(**** HIGHER LEVEL OPERATIONS ON GRAPHS *****) + +let connect ~from:l1 ~towards:l2 t = + List.fold_left (fun b (x,y) -> edge_add ~from:x ~towards:y b) + t + (zip (fun x y -> (x,y)) l1 l2);; + +(** + * Replace all connections to / from this + * node by bottoms / disconnect nodes + * so that removing the node + * afterwards does not affect the meaning + * of the circuit (no connections to + * non-existing nodes) + *) +let inactive ~node:n t = + let pre = pre_nodes ~node:n t in + let post = post_nodes ~node:n t in + + let dis = newids (List.length pre) in + let bot = newids (List.length post) in + + t |> batch ~f:(label_set ~label:Disconnect) ~nodes:dis + |> batch ~f:(label_set ~label:(Value Bottom)) ~nodes:bot + |> pre_disconnect ~node:n + |> post_disconnect ~node:n + |> connect ~from:pre ~towards:dis + |> connect ~from:bot ~towards:post + |> batch ~f:main_add ~nodes:(dis @ bot) ;; + +(** + * Safe remove for a main node + *) +let safe_remove ~node:n t = + t |> inactive ~node:n + |> main_rem ~node:n;; + + +(** + * Deletes all the specific structure for + * a pTG + *) +let flatten t = + { t with + nodes = t.iports @ t.oports @ t.traced @ t.delays @ t.nodes ; + iports = []; + oports = []; + delays = []; + traced = []; + };; + +(*** BATCH FORK AND JOIN ***) + + +let mk_join ~towards ~fst ~snd ptg = + let new_joins = newids (List.length towards) in + ptg |> batch ~f:main_add ~nodes:new_joins + |> connect ~from:fst ~towards:new_joins + |> connect ~from:snd ~towards:new_joins + |> connect ~from:new_joins ~towards:towards + |> batch ~f:(label_set ~label:(Gate Join)) ~nodes:new_joins;; + +let mk_fork ~from ~fst ~snd ptg = + let new_forks = newids (List.length from) in + ptg |> batch ~f:main_add ~nodes:new_forks + |> connect ~from:new_forks ~towards:fst + |> connect ~from:new_forks ~towards:snd + |> connect ~from:from ~towards:new_forks + |> batch ~f:(label_set ~label:(Gate Fork)) ~nodes:new_forks;; + + +(*** DIAGONAL FORK and JOIN ***) +let rec fork_into ~node:n ~nodes:l ptg = + match l with + | [] -> ptg + | [t] -> + ptg |> edge_add ~from:n ~towards:t + | t :: q -> + let fork_node = newid () in + ptg |> fork_into ~node:fork_node ~nodes:q + |> main_add ~node:fork_node + |> label_set ~node:fork_node ~label:(Gate Fork) + |> edge_add ~from:fork_node ~towards:t + |> edge_add ~from:n ~towards:fork_node;; + +let rec join_into ~node:n ~nodes:l ptg = + match l with + | [] -> ptg + | [t] -> + ptg |> edge_add ~from:t ~towards:n + | t :: q -> + let join_node = newid () in + ptg |> join_into ~node:join_node ~nodes:q + |> main_add ~node:join_node + |> label_set ~node:join_node ~label:(Gate Join) + |> edge_add ~from:t ~towards:join_node + |> edge_add ~from:join_node ~towards:n;; + + +(**** SPLITTING THE TRACE *****) +let trace_split ptg = + let trids = newids (List.length ptg.traced) in + let corres = List.combine ptg.traced trids in + + (* this function seems complex, but in fact + * traced nodes have only one input and + * one output, so this function runs in + * constant time !! + *) + let copy_pre_conn (x,y) t = + let pre = pre_nodes ~node:x t in + let action ~node:n t = + t |> edge_rem ~from:n ~towards:x + |> edge_add ~from:n ~towards:y + in + batch ~f:action ~nodes:pre t + in + + let new_graph = { + ptg with + traced = []; + nodes = ptg.traced + @ trids + @ ptg.nodes; + } + in + let new_graph_2 = + new_graph |> apply ~f:copy_pre_conn ~elems:corres + in + (trids, ptg.traced, new_graph_2);; + +(**** + * edge merging, preserving the ordering of lists + * + * a -> b -> c + * + * removes b and connects a to c preserving + * the output number for a and the input + * number for c + * + * b is supposed to be a simple connecting + * node of type 1->1 + * + *) +let edge_remove_node ~from:a ~using:b ~towards:c t = + let a_out = post_nodes ~node:a t in + let c_in = pre_nodes ~node:a t in + let convert n x = + if x = b then + n + else + x + in + + { t with + edges = t.edges |> id_add a (replace_once b c a_out) |> id_remove b ; + co_edges = t.co_edges |> id_add c (replace_once b a c_in) |> id_remove b ; + };; + +(*** + * Does exactly the opposite construction + *) +let edge_insert_node ~from:a ~towards:c ~using:b t = + let a_out = post_nodes ~node:a t in + let c_in = pre_nodes ~node:c t in + let convert n x = + if x = b then + n + else + x + in + { t with + edges = t.edges |> id_add a (replace_once c b a_out) + |> id_add b [a] ; + co_edges = t.co_edges |> id_add c (replace_once a b c_in) + |> id_add b [c]; + };; + + + +(**** dispatching *****) + +(** Dispatch nodes *) +let rec dispatch_with ~f ~from1 ~from2 ~fst ~snd g = + match from1,from2,fst,snd with + | [],[],[],[] -> g + | a1::a2,b1::b2,c1::c2,d1::d2 -> + if f c1 d1 g then + g |> edge_add ~from:a1 ~towards:c1 + |> edge_add ~from:b1 ~towards:d1 + |> dispatch_with ~f ~from1:a2 ~from2:b2 ~fst:c2 ~snd:d2 + else + g |> edge_add ~from:a1 ~towards:d1 + |> edge_add ~from:b1 ~towards:c1 + |> dispatch_with ~f ~from1:a2 ~from2:b2 ~fst:c2 ~snd:d2;; + +(** + * Create a copy of the ptg with + * a disjoint set of nodes + * along with the translation function + *) +let replicate ptg = + let m = !counter in + let translate x = x + m + 1 in + + let update_label m (oldid,lbl) = + id_add (translate oldid) lbl m + in + + + + counter := translate m; + + (translate, { + + iports = List.map translate ptg.iports; + oports = List.map translate ptg.oports; + + traced = List.map translate ptg.traced; + delays = List.map translate ptg.delays; + + nodes = List.map translate ptg.nodes ; + + edges = ptg.edges + |> id_bindings + |> List.fold_left update_label id_empty; + + co_edges = ptg.co_edges + |> id_bindings + |> List.fold_left update_label id_empty; + + labels = ptg.labels + |> id_bindings + |> List.fold_left update_label id_empty ; + + });; + + +(*** + * + * Merging two graphs + * with disjoint node names + * + * The result is flattened + *) +let ptg_merge g1 g2 = + { + nodes = (flatten g1).nodes @ (flatten g2).nodes ; + delays = []; + traced = []; + iports = []; + oports = []; + + labels = id_merge merger_v g1.labels g2.labels; + + edges = id_merge merger_v g1.edges g2.edges; + + co_edges = id_merge merger_v g1.co_edges g2.co_edges; + };; diff --git a/rewriting.ml b/rewriting.ml new file mode 100644 index 0000000..99cdb99 --- /dev/null +++ b/rewriting.ml @@ -0,0 +1,475 @@ + +open Utils;; +open Ptg;; + +(**** + * + * FIXME utiliser des SET de nodes + * quand l'appartenance est souvent + * de mise. + * + * Par exemple quand on fait le garbage + * collection + *) + +(** + * pass a constant node through + * a traced node + *) +let propagate_constant ~node:n t = + try (* pattern matching failure means no modification *) + let Some (Value v) = id_find n t.labels in + let [traced_node] = post_nodes ~node:n t in + if not (List.mem traced_node t.traced) then + t + else + t |> trace_rem ~node:traced_node + |> main_rem ~node:n + |> label_set ~node:traced_node ~label:(Value v) + |> main_add ~node:traced_node + with + Match_failure _ -> t;; + + +(** + * remove a main identity node + *) +let remove_identity ~node:n t = + try (* pattern matching failure means no modification *) + let [pre] = pre_nodes ~node:n t in + let [pos] = post_nodes ~node:n t in + let None = id_find n t.labels in + if List.mem n t.nodes then + t |> edge_remove_node ~from:pre ~using:n ~towards:pos + |> main_rem ~node:n + else + t + with + Match_failure _ -> t;; + +(** + * propagate a fork node + *) +let propagate_fork ~node:n t = + try (* pattern matching failure means no modification *) + let Some (Gate Fork) = id_find n t.labels in + let [z] = pre_nodes ~node:n t in + let Some (Value v) = id_find z t.labels in + let [x;y] = post_nodes ~node:n t in + + (* now do the update *) + let new_node = newid () in + + t |> edge_insert_node ~from:n ~towards:x ~using:new_node + |> edge_rem ~from:n ~towards:new_node + |> main_rem ~node:z + |> label_set ~node:n ~label:(Value v) + |> label_set ~node:new_node ~label:(Value v) + with + Match_failure _ -> t;; + + +(** + * Propagating bottoms + * through joins and disconnect trough + * forks + *) +let bottom_join ~node:n t = + try (* pattern matching failure means no modification *) + let Some (Value Bottom) = id_find n t.labels in + let [j] = post_nodes ~node:n t in + let Some (Gate Join) = id_find j t.labels in + t |> main_rem ~node:n + |> label_rem ~node:j + |> edge_rem ~from:j ~towards:n + with + Match_failure _ -> t;; + + +let disconnect_fork ~node:n t = + try (* pattern matching failure means no modification *) + let Some Disconnect = id_find n t.labels in + let [f] = pre_nodes ~node:n t in + let Some (Gate Fork) = id_find f t.labels in + t |> main_rem ~node:n + |> label_rem ~node:f + |> edge_rem ~from:f ~towards:n + with + Match_failure _ -> t;; + + +let gate_of_node ~node:n t = + match id_find n t.labels with + | Some (Gate g) -> g + | _ -> failwith "(gate_of_node) try to get a gate from a non-gate node";; + +let is_gate ~node:n t = + match id_find n t.labels with + | Some (Gate g) -> true + | _ -> false;; + +type gate_func_outpt = + | Result of value + | Wire of int + | NoOP;; + +let reduce_mux inputs = + try + let [a;b;c] = inputs in + match Lazy.force a with + | Some (Value Bottom) -> Result Bottom + | Some (Value Top) -> Result Top + | Some (Value High) -> Wire 1 + | Some (Value Low) -> Wire 2 + | None -> NoOP + with + Match_failure _ -> NoOP;; + +(** + * + * TODO: + * join + * nmos + * pmos + *) + + +let fun_of_gate = function + | Mux -> reduce_mux + | _ -> (fun _ -> NoOP);; + +(** + * Gate reduction + * + * Things that are important + * + * 1) Short circuit / lazyness + * -> use Lazy values as input + * 2) Simple code : no boilerplate for gate reductin + * -> gate reduction is a first class function + * + * A] pattern match + * B] Use f : (label option lazy) list -> label | nothing | int (* gate output *) + * C] replace the pattern + * -> NEVER delete the nodes, just put disconnect in front + * of every node that is not used, the garbage collection + * and the dangling nodes rewriting will do their job + * better than we evel will + * + * LIMITATIONS: + * + * Gates have only one output + * + *) +let reduce_gate ~node:n t = + if is_gate ~node:n t then + try + let pre = pre_nodes ~node:n t in + let [o] = post_nodes ~node:n t in + let ipt = List.map (fun x -> lazy (id_find x t.labels)) pre in + + match fun_of_gate (gate_of_node ~node:n t) ipt with + | Wire i -> + (* connect wire i with the output + * through the gate (edge_remove_node) + * (bypassing the gate) + *) + t |> edge_remove_node ~from:(List.nth pre i) ~towards:o ~using:n + (* completely delete the gate + * with safe deletion + * *) + |> safe_remove ~node:n + | Result l -> + (* + * insert node between the gate and the output, + * putting label l + *) + let m = newid () in + t |> main_add ~node:n + |> label_set ~node:n ~label:(Value l) + |> edge_insert_node ~from:n ~towards:o ~using:m + (* remove the edge between the inserted node + * and the gate + *) + |> edge_rem ~from:n ~towards:m + (* + * remove the gate using safe remove + *) + |> safe_remove ~node:n + | NoOP -> t + with + Match_failure _ -> t + else + t;; + +(* + * TODO + * convince that it does the right thing + * + * ---> explain every step of + * the process + * + *) +let rewrite_delays g1 = + let (_, g2) = replicate g1 in + + let (pre1,post1,g1) = trace_split g1 in + let (pre2,post2,g2) = trace_split g2 in + + (* Creating new special nodes *) + let new_trace = newids (List.length post1) in + let new_inputs = newids (List.length g1.iports) in + let new_delays = newids (List.length g1.oports) in + let new_outputs = newids (List.length g1.oports) in + + let bottoms_pre = newids (List.length post1) in + let bottoms_ipts = newids (List.length g1.iports) in + + + let is_delayed a _ g = + match post_nodes ~node:a g with + | [x] -> + begin + match id_find x g.labels with + | Some (Gate Wait) -> true + | _ -> false + end + | _ -> false + in + + + ptg_merge g1 g2 + |> batch ~f:(label_set ~label:Disconnect) ~nodes:post2 + + (** adding trace nodes in reverse order to keep the same order + * in the end ... + *) + |> batch ~f:trace_add ~nodes:(List.rev new_trace) + |> batch ~f:main_add ~nodes:(bottoms_pre @ bottoms_ipts @ new_delays) + + |> dispatch_with ~f:is_delayed + ~from1:new_trace + ~from2:bottoms_pre + ~fst:pre1 + ~snd:pre2 + + |> dispatch_with ~f:is_delayed + ~from1:new_inputs + ~from2:bottoms_ipts + ~fst:g1.iports + ~snd:g2.iports + + |> connect ~from:new_trace ~towards:post1 + + + |> batch ~f:(label_set ~label:(Value Bottom)) + ~nodes:(bottoms_pre @ bottoms_ipts) + + |> batch ~f:label_rem ~nodes:(g1.delays @ g2.delays) + + |> connect ~from:g1.oports + ~towards:new_delays + + |> mk_join ~fst:new_delays + ~snd:g2.oports + ~towards:new_outputs + + (** adding nodes in reverse order to keep the same order + * in the end ... + *) + |> batch ~f:iport_add ~nodes:(List.rev new_inputs) + |> batch ~f:oport_add ~nodes:(List.rev new_outputs);; + +(** + * + * trace unfolding ! + * for now without delays + * + *) +let unfold_trace g1 = + let g2 = rewrite_delays g1 in + + let new_inputs = newids (List.length g1.iports) in + + let (pre1,post1,g1) = trace_split g1 in + let (pre2,post2,g2) = trace_split g2 in + + + ptg_merge g1 g2 + |> batch ~f:(label_set ~label:Disconnect) ~nodes:post2 + |> batch ~f:(label_set ~label:Disconnect) ~nodes:g1.oports + |> batch ~f:(label_set ~label:(Gate Fork)) ~nodes:post1 + + |> mk_fork ~from:post1 ~fst:pre2 ~snd:pre1 + |> mk_fork ~from:new_inputs ~fst:g1.iports ~snd:g2.iports + + |> batch ~f:trace_add ~nodes:(List.rev pre1) + |> batch ~f:iport_add ~nodes:(List.rev new_inputs) + |> batch ~f:oport_add ~nodes:(List.rev g2.oports);; + +(** + * Mark nodes + *) +let rec mark_nodes ~seen ~nexts ptg = + match nexts with + | [] -> seen + | t :: q -> + if List.mem t seen then + mark_nodes ~seen:seen ~nexts:q ptg + else + let pre_nodes = pre_nodes ~node:t ptg in + mark_nodes ~seen:(t :: seen) + ~nexts:(pre_nodes @ q) + ptg;; + +(** + * + * The mark and sweep + * phase + * + * TODO: be better than that ... because gates other than fork and join + * can be targeted !!!!! This only works when the gates only have one + * output + * + * CORRECT BEHAVIOR + * + * for each reachable node, + * for each edge going to a non-reachable node + * replace it with Disconnect + * + * for each edge coming from a non-reachable node + * replace it with Bottom + * + * This function should replace « update_forks_and_joins » + * + * NOTE the second part is not necessary because of the + * way mark and sweeps works ... (but right now correct + * code is better than optimized one) + * + *) +let mark_and_sweep t = + let reachable = mark_nodes ~seen:[] ~nexts:t.oports t in + print_string "\n REACHABLE : "; + reachable |> List.map string_of_int |> String.concat " ; " |> print_string; + let filter_func x = not (List.mem x reachable) in + let is_reachable x = List.mem x reachable in + let nodes_to_delete = List.filter filter_func t.nodes in + + let remove_node_safely ~node:n t = + let pre = t + |> pre_nodes ~node:n + |> List.filter is_reachable + in + + let post = t + |> post_nodes ~node:n + |> List.filter is_reachable + in + + let bottoms = newids (List.length post) in + let discons = newids (List.length pre ) in + + + t |> apply ~f:(fun (x,y) -> edge_insert_node ~from:n ~using:y ~towards:x) ~elems:(List.combine post bottoms) + |> apply ~f:(fun (x,y) -> edge_insert_node ~from:x ~using:y ~towards:n) ~elems:(List.combine pre discons) + |> batch ~f:(label_set ~label:Disconnect) ~nodes:discons + |> batch ~f:(label_set ~label:(Value Bottom)) ~nodes:bottoms + |> main_rem ~node:n + |> node_edges_rem ~node:n + in + + print_string "\n TO DELETE : "; + nodes_to_delete |> List.map string_of_int |> String.concat " ; " |> print_string; + print_string "\n"; + t |> batch ~f:remove_node_safely ~nodes:nodes_to_delete + + +(* TODO + * + * 1) test on examples + * 2) Gate rewriting : finish implementing + * 3) Dot output : very clever + * + *) + + +let empty_ptg = + { iports = []; oports = []; traced = []; delays = []; nodes = []; labels = id_empty; edges = id_empty ; co_edges = id_empty };; + + +let example_ptg_2 = + let [a;b;c;d] = newids 4 in + empty_ptg |> batch ~f:main_add ~nodes:[a;b] + |> iport_add ~node:c + |> oport_add ~node:d + |> label_set ~node:a ~label:(Gate Fork) + |> label_set ~node:b ~label:Disconnect + |> connect ~from:[a;a;c] ~towards:[b;d;a];; + + +let () = + example_ptg_2 |> string_of_ptg |> print_string; + example_ptg_2 |> mark_and_sweep |> string_of_ptg |> print_string;; + + + +(******* DOT OUTPUT ... *******) + +open Dot;; +let dot_of_ptg ptg = + let init_rank = rank_group "min" (ptg.iports @ ptg.traced @ ptg.delays) in + let fin_rank = rank_group "max" ptg.oports in + + let main_node nid = + let n = List.length (pre_nodes ~node:nid ptg) in + let m = List.length (post_nodes ~node:nid ptg) in + match id_find nid ptg.labels with + | None -> mkNode nid (emptyMod |> mod_shape "point") + | Some (Gate Join) -> + mkNode nid (emptyMod |> mod_shape "point") + | Some (Gate Fork) -> + mkNode nid (emptyMod |> mod_shape "point") + | Some l -> + mkNode nid (baseMod |> inputsOutputs (string_of_label l) n m) + in + + (* + * DO SOMETHING CLEVER HERE + * + *) + let edges_from n t = () in + + + let main_nodes = + ptg.nodes |> List.map main_node + |> String.concat "\n" + in + + let inputs = + ptg.iports + |> List.map (fun x -> mkNode x (emptyMod |> mod_shape "diamond")) + |> String.concat "\n" + in + + let outputs = + ptg.oports + |> List.map (fun x -> mkNode x (emptyMod |> mod_shape "diamond")) + |> String.concat "\n" + in + + let traced = + ptg.traced + |> List.map (fun x -> mkNode x (emptyMod |> mod_shape "point" |> mod_width 0.1 |> mod_color "red")) + |> String.concat "\n" + in + + let delays = + ptg.delays + |> List.map (fun x -> mkNode x (emptyMod |> mod_shape "point" |> mod_width 0.1 |> mod_color "grey")) + |> String.concat "\n" + in + + [ init_rank; fin_rank; main_nodes; inputs; outputs; delays; traced ] + |> String.concat "\n" + |> addPrelude;; + diff --git a/utils.ml b/utils.ml index b2390ed..5576eef 100644 --- a/utils.ml +++ b/utils.ml @@ -60,20 +60,21 @@ let rec zipWith f l1 l2 = match (l1,l2) with | (a::c, b::d) -> (f a b) :: (zipWith f c d);; (* - * Place un morceau de texte des deux côtés - * d'un texte * - * Utile pour composer avec des fonctions + * Put surroundings to a string + * Usefull in long function composition + * chain + * + * WARNING: intended behaviour, + * if the string is empty, does NOT + * put any surroundings * - * ATTENTION: ne met entre p et q - * que si la chaine est non vide ! - * (pratique) *) let surround p q s = if s = "" then "" else p ^ s ^ q;; (** - * permute les lignes d'un vecteur + * Swap lines of a vector *) let permute_lignes i j v = let tmp = v.(i) in @@ -91,6 +92,7 @@ let array_find f a = done; !c;; +(* option trying combinator *) let (<|>) a b = match a with | Some x -> a | None -> b;; -- GitLab