Skip to content

GitLab

S
stage-L3-2016
Commit 9c91186e authored by Aliaume Lopez's avatar Aliaume Lopez
Browse files
Options

Maintenant ça marche bien !

parent a3e89de9
Hide whitespace changes
Inline Side-by-side
Showing with 320 additions and 1137 deletions
Makefile
View file @ 9c91186e
OCAMLCC=ocamlc
OSRC=utils.ml lexer.ml ast.ml parser.ml dot.ml solver.ml typesystem.ml dags.ml compiler.ml
OSRC=utils.ml lexer.ml ast.ml parser.ml dot.ml solver.ml typesystem.ml dags.ml compiler.ml ptg.ml rewriting.ml
OSRCL=utils.mli ast.mli dot.mli typesystem.mli dags.mli
.PHONY: test clean doc
......@@ -21,18 +21,6 @@ circuits: $(OSRC) $(OSRCL) circuits.ml
$(OCAMLCC) -g -o circuits $(OSRC) circuits.ml
./circuits
examples: $(OSRC) $(OSRCL) examples.ml
$(OCAMLCC) $(OSRCL)
$(OCAMLCC) -g -o examples $(OSRC) examples.ml
./examples
dot -Tpdf example1.dot > example1.pdf && open example1.pdf
dot -Tpdf example2.dot > example2.pdf && open example2.pdf
dot -Tpdf example3.dot > example3.pdf && open example3.pdf
dot -Tpdf example4.dot > example4.pdf && open example4.pdf
dot -Tpdf example5.dot > example5.pdf && open example5.pdf
dot -Tpdf example6.dot > example6.pdf && open example6.pdf
dot -Tpdf example7.dot > example7.pdf && open example7.pdf
clean:
rm *.cmi
rm *.cmo
circuits.ml
View file @ 9c91186e
......@@ -4,214 +4,67 @@
*
* Aliaume Lopez
*
* TODO
*
* 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
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;;
type connection = {
nbr : int; (* the number of ports *)
con : nid mapping; (* a map from port number to node *)
}
(** FOR NOW WE WILL NOT USE THE CONNECTION TYPE **)
type gate =
| Fork
| Join
| Nmos
| Pmos
| Box of string
| Wait
| Mux
| Disconnect;;
type value =
| High
| Low
| Top
| Bottom;;
type label =
| 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 order
* delays : a connection giving the delayed nodes with an order
*
* labels : a mapping from nodes to their labels
* ALL nodes are represented
*
* edges : a mapping from a node to a connection
* representing it's « sons »
* with convention that a negative ID
* represents an output
*
* co-edeges : a mapping from nodes to a connection
* representing it's « parents »
* with convention that a negative ID
* represents an input
*
*)
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 : (int * nid * int) 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 * int option * nid * int option) list;
(* edges in reverse order *)
(* co_edges : connection mapping; *)
}
(**
* @t : potential tabulation in front of each line
*)
let string_of_connection t c =
let nbr = string_of_int c.nbr in
let arr = Array.make c.nbr "EMPTY" in
c.con
|> id_bindings
|> List.iter (fun (i,y) -> arr.(i) <- string_of_int y);
arr |> Array.mapi (fun i x -> t ^ string_of_int i ^ " :: " ^ x)
|> Array.to_list
|> String.concat "\n";;
open Dags;;
open Ptg ;;
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 |> List.map (fun (x,i,y,j) ->
"\t\t " ^ string_of_int x ^ " -> "
^ string_of_int y)
|> String.concat "\n";
] in
structure |> String.concat "\n";;
let pp_ptg ptg = ptg |> string_of_ptg |> print_string;;
(**** DOT CONVERSION ****)
(******* DOT OUTPUT ... *******)
let rec list_index x = function
| [] -> failwith "oups"
| t :: q when t = x -> 0
| t :: q -> 1 + list_index x q;;
open Dot;;
let dot_of_ptg ptg =
let init_rank = rank_group "min" ptg.iports in
let init_rank = rank_group "min" (ptg.iports @ ptg.traced @ ptg.delays) in
let fin_rank = rank_group "max" ptg.oports in
let edges = ptg.edges
|> List.map (fun (x,y,z,t) -> mkLink x y z t)
|> String.concat "\n"
in
let main_node nid n m =
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) ->
| None
| Some (Gate Join)
| Some (Gate Fork)
->
mkNode nid (emptyMod |> mod_shape "point")
| Some Disconnect ->
mkNode nid (baseMod |> mod_label (string_of_label Disconnect))
| Some (Value v) ->
mkNode nid (baseMod |> mod_label (string_of_label (Value v)))
| Some l ->
mkNode nid (baseMod |> inputsOutputs (string_of_label l) n m)
in
let node_port_from_edge nid l eid =
match id_find nid ptg.labels with
| None
| Some (Gate Join)
| Some (Gate Fork)
| Some Disconnect
| Some (Value _) -> None
| _ -> Some (1 + list_index eid l)
in
let draw_edge eid (a,b) =
let l1 = edges_from ~node:a ptg in
let l2 = edges_towards ~node:b ptg in
let i1 = node_port_from_edge a l1 eid in
let i2 = node_port_from_edge b l2 eid in
mkLink a i1 b i2
in
let edges =
ptg.arrows |> id_bindings
|> List.map (fun (x,y) -> draw_edge x y)
|> String.concat "\n"
in
let main_nodes =
ptg.nodes |> List.map (fun (x,y,z) -> main_node y x z)
ptg.nodes |> List.map main_node
|> String.concat "\n"
in
......@@ -239,813 +92,207 @@ let dot_of_ptg ptg =
|> String.concat "\n"
in
[ init_rank; fin_rank; edges; main_nodes; inputs; outputs; delays; traced ]
[ init_rank; fin_rank; main_nodes; inputs; outputs; delays; traced;edges ]
|> String.concat "\n"
|> addPrelude;;
(*** DOT CONVERSION FINISHED ***)
let counter = ref 0;;
let newid () =
incr counter; !counter;;
let newids n = Utils.range n |> List.map (fun _ -> newid ());;
(** 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;;
(**** DAG CONVERSION *****)
(* turn an implict n-ary fork into an explicit one *)
let real_fork ~node:n ptg =
let images = post_nodes ~node:n ptg in
ptg |> post_disconnect ~node:n
|> fork_into ~node:n ~nodes:images;;
(* turn an implict n-ary join into an explicit one *)
let real_join ~node:n ptg =
let images = pre_nodes ~node:n ptg in
ptg |> pre_disconnect ~node:n
|> join_into ~node:n ~nodes:images;;
(* Converting the labels
* for constants into PTG labels
* *)
let convert_label = function
| VarI x -> Gate (Box x)
| VarO x -> Gate (Box x)
| Const g ->
begin
match g with
| "BOT" -> Value Bottom
| "HIGH" -> Value High
| "LOW" -> Value Low
| "TOP" -> Value Top
| "MUX" -> Gate Mux
| "NMOS" -> Gate Nmos
| "PMOS" -> Gate Pmos
| "WAIT" -> Gate Wait
| "DISC" -> Disconnect
| x -> Gate (Box x)
end;;
let ptg_of_dag dag =
(* FIRST OF ALL TRANSLATE ALL THE NAMES SO THAT
* THEY DO NOT CONFLICT WITH OTHER PTG NAMES
*)
let dag = mapids (fun x -> x + !counter) dag in
counter := 10 + maxid dag;
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);;
(*
* then extract the informations
*)
let nodes = dag.nodes |> List.map (fun (x,y,z) -> x) in
let iport = dag.iports |> List.map (fun (x,y) -> x) in
let oport = dag.oports |> List.map (fun (x,y) -> x) in
let ibind = dag.ibinders in
let obind = dag.obinders in
(**
* 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
(*
* the « inside nodes » of the DAG !!! Theses are NOT
* the inside nodes of the whole ptg
*)
let inside = Utils.remove_list nodes (ibind @ obind) in
let update_label m (oldid,lbl) =
id_add (translate oldid) lbl m
in
(* Creating the input nodes and outputs nodes *)
let ins = newids (List.length iport) in
let outs = newids (List.length oport) in
counter := translate m;
(*** HANDLING THE EDGES ***)
(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 = ptg.nodes
|> List.map (fun (x,y,z) -> (x, translate y, z));
edges = ptg.edges |> List.map (fun (x,y,z,t) ->
(translate x, y, translate z, t));
labels = ptg.labels
|> id_bindings
|> List.fold_left update_label id_empty ;
});;
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 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
{
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 ;
labels = id_remove n t.labels
};;
(**
*
* 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 new_discard () =
let x = newid () in
discard := x :: !discard;
x
in
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.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 |> add_bottoms |> add_discard
};;
let relabel_node ~node:n ~label:l t =
{
t with
labels = t.labels
|> id_remove n
|> 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
*
*)
let add_edge ~edge:e t =
{
t with
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
*)
let move_to_main ~node:n t =
let try_find = List.filter (fun (_,x,_) -> x = n) t.nodes in
let simple_rem x = not (x = n) in
if try_find = [] then
{ t with
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 ;
iports = List.filter simple_rem t.iports ;
}
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)
]
let add_edge_to_list a b = function
| None -> Some [(a,b)]
| Some k -> Some ((a,b) :: k)
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)
*)
let is_main_node ~node:n t =
t.nodes |> List.map (fun (_,x,_) -> x)
|> List.mem n;;
let delete_label ~node:n t =
{ t with
labels = t.labels |> id_remove n
};;
let delete_label_l ~nodes:n t =