Commit 648d56be authored by Aliaume Lopez's avatar Aliaume Lopez

Now correct behaviour for link

parent d47599e6
......@@ -316,12 +316,16 @@ let rules = [ Rewriting.remove_identity ;
let looping_reduction_step x =
let x = Rewriting.garbage_collect_dual x in
report "GARBAGE COLLECT" x;
let x = rewrite_local rules x in
report "LOCAL REWRITE" x;
let x = Rewriting.unfold_trace x in
report "TRACE UNFOLDING" x;
let x = Rewriting.garbage_collect_dual x in
report "GARBAGE COLLECT" x;
x;;
......
......@@ -221,40 +221,55 @@ let link ~vars ~dag:g =
let c = vi |> List.mapi (fun i v -> (v,i + m + 1)) in
let ci = List.length c in
(* d : vi -> node_id *)
let d = vo |> List.mapi (fun i v -> (v,i + m + ci + 1)) in
let d = vo |> List.mapi (fun i v -> (v,i + m + ci + 1)) in
let di = List.length d in
(* FIXME
* if fiberV x == [] then
* the binding node is just a dangling node ...
*
* Need to be seen !
(** adding the bottoms *)
let disc = c |> List.mapi (fun k (_,v) -> (k + m + ci + di + 1, v)) in
let bots = d |> List.mapi (fun k (_,v) -> (k + m + ci + ci + di + 1, v)) in
(* The edges for each instance of a variable to
* the corresponding binding node
*)
let ei = vi >>= (fun x ->
fiberV (VarI x) g.labels >>= (fun v ->
[anonym_link (of_option (imageV x c)) v]))
in
(* The edges for each instance of a variable to
* the corresponding binding node
*)
let eo = vo >>= (fun x ->
fiberV (VarO x) g.labels >>= (fun v ->
[anonym_link v (of_option (imageV x d))]))
in
(* The edges between the binding nodes *)
let eb = vars |> List.map (fun (x,y) -> anonym_link (of_option (imageV x d)) (of_option (imageV y c)))
|> remove_duplicates
in
let ebots = bots |> List.map (fun (x,y) -> anonym_link x y) in
let edisc = disc |> List.map (fun (x,y) -> anonym_link y x) in
let check_label = function
| VarI x -> not (List.mem x vi)
| VarO x -> not (List.mem x vo)
| _ -> true
in
let new_labels = g.labels |> List.filter (fun x -> check_label (snd x)) in
let new_labels = g.labels |> List.filter (fun x -> check_label (snd x)) in
{
iports = g.iports ;
oports = g.oports ;
nodes = (List.map (fun x -> (snd x, 0, 0)) d) @
nodes = (List.map (fun x -> (fst x, 0, 0)) disc) @
(List.map (fun x -> (fst x, 0, 0)) bots) @
(List.map (fun x -> (snd x, 0, 0)) d) @
(List.map (fun x -> (snd x, 0, 0)) c) @ g.nodes ;
edges = ei @ eo @ eb @ g.edges ;
labels = new_labels ;
edges = ebots @ edisc @ ei @ eo @ eb @ g.edges ;
labels = (List.map (fun x -> (fst x, Const "DISC")) disc) @
(List.map (fun x -> (fst x, Const "BOT")) bots) @
new_labels ;
ibinders = List.map snd c @ g.ibinders ;
obinders = List.map snd d @ g.obinders ;
};;
......
(HIGH | (HIGH . WAIT) | (HIGH . WAIT)) . (JOIN | 1) . JOIN
link a:b for HIGH
......@@ -85,6 +85,11 @@ let propagate_fork ~node:n t =
* forks
*
* NOTE useless because of join reducing gate ...
*
*
* FIXME There should be a global garbage collecting stuff
* so that local reductions are not needed to replace
* whole subcircuits with _|_ ...
*)
let bottom_join ~node:n t =
try (* pattern matching failure means no modification *)
......@@ -550,11 +555,14 @@ let garbage_collect_dual t =
let remove_node_safely ~node:n t =
print_string ("\tREMOVE NODE : " ^ string_of_int n ^ "\n");
(* The edges comming from a reachable node *)
let pre = t
|> edges_towards ~node:n
|> List.filter (is_reachable fst)
in
(* The edges going to a reachable node *)
let post = t
|> edges_from ~node:n
|> List.filter (is_reachable snd)
......
......@@ -119,8 +119,8 @@ let var_type nom a b =
in
(ivar,ovar,c,
{ itype = Var ivar;
otype = Var ovar;
vtypes = VarType.singleton nom [(ivar,ovar)]
otype = Var ovar;
vtypes = VarType.singleton nom [(ivar,ovar)]
});;
let union_vtypes a b =
......@@ -185,6 +185,12 @@ let calcul_type circuit =
|> make_equations
|> (fun e -> constraints := e @ !constraints)
in
(* accumulating the type
*
* accum_type : (type, annotated circuit)
*
*)
let accum_type = function
| Id x -> (base_type x x, TCirc (Id x, (Const x, Const x)))
| IdPoly ->
......@@ -202,9 +208,11 @@ let calcul_type circuit =
| VarI y -> let (_,o,c,v) = var_type y 0 1 in
add_constraints c;
(v, TCirc (VarI y, (Const 0, Var o)))
(*(base_type 0 1, TCirc (VarI y, (Const 0, Const 1)))*)
| VarO y -> let (i,_,c,v) = var_type y 1 0 in
add_constraints c;
(v, TCirc (VarO y, (Var i, Const 0)))
(*(base_type 1 0, TCirc (VarO y, (Const 1, Const 0)))*)
| Par ((a,annotA),(b,annotB)) ->
let i = Var (newvarid ()) in
let o = Var (newvarid ()) in
......@@ -248,7 +256,7 @@ let calcul_type circuit =
| Solution v -> (annotated,v)
| NoSol -> failwith "Not typeable"
| Negative _ -> failwith "Negative solution"
| ManySol liste -> failwith ("Many solution ... fix variable : " ^ (liste |> List.map string_of_int |> String.concat " or "))
| ManySol liste -> failwith ("Many solutions ... fix variable : " ^ (liste |> List.map string_of_int |> String.concat " or "))
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment