First commit ; includes first TP and minijazz compiler

10 files changed, 840 insertions, 0 deletions

diff --git a/minijazz/src/global/_tags b/minijazz/src/global/_tags
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/minijazz/src/global/_tags
diff --git a/minijazz/src/global/ast.ml b/minijazz/src/global/ast.ml
new file mode 100644
index 0000000..cc29486
--- /dev/null
+++ b/minijazz/src/global/ast.ml
@@ -0,0 +1,107 @@
+open Location
+open Static
+
+type ident = Ident.t
+type name = string
+
+module IdentEnv = Map.Make (struct type t = ident let compare = compare end)
+module IdentSet = Set.Make (struct type t = ident let compare = compare end)
+
+module NameEnv = Map.Make (struct type t = name let compare = compare end)
+module NameSet = Set.Make (struct type t = name let compare = compare end)
+
+type ty =
+  | TUnit | TBit | TBitArray of static_exp | TProd of ty list
+  | TVar of link ref
+and link =
+  | TIndex of int
+  | TLink of ty
+let invalid_type = TUnit
+
+type mem_kind = MRom | MRam
+
+type value =
+  | VBit of bool
+  | VBitArray of bool array
+
+type edesc =
+  | Econst of value
+  | Evar of ident
+  | Ereg of exp
+  | Ecall of name * static_exp list * exp list
+      (* function * params * args *)
+  | Emem of mem_kind * static_exp * static_exp * string option * exp list
+      (* ro * address size * word size * input file * args *)
+
+and exp = {
+  e_desc : edesc;
+  e_ty : ty;
+  e_loc: location;
+}
+
+type pat =
+  | Evarpat of ident
+  | Etuplepat of ident list
+
+type equation = pat * exp
+
+type var_dec = {
+  v_ident : ident;
+  v_ty : ty;
+}
+
+type param = {
+  p_name : name;
+}
+
+type block =
+    | BEqs of equation list * var_dec list
+    | BIf of static_exp * block * block
+
+type inlined_status = Inlined | NotInlined
+
+type node_dec = {
+  n_name : name;
+  n_loc: location;
+  n_inlined : inlined_status;
+  n_inputs : var_dec list;
+  n_outputs : var_dec list;
+  n_params : param list;
+  n_constraints : static_exp list;
+  n_body : block;
+  n_probes : ident list;
+}
+
+type const_dec = {
+  c_name : name;
+  c_loc : location;
+  c_value : static_exp;
+}
+
+type program = {
+  p_consts : const_dec list;
+  p_nodes : node_dec list;
+}
+
+
+let mk_exp ?(loc = no_location) ?(ty = invalid_type) desc =
+  { e_desc = desc; e_loc = loc; e_ty = ty }
+
+let mk_const_dec ?(loc = no_location) n se =
+  { c_name = n; c_loc = loc; c_value = se }
+
+let mk_equation pat e = (pat, e)
+
+let mk_var_dec n ty =
+  { v_ident = n; v_ty = ty }
+
+let mk_param n =
+  { p_name = n }
+
+let mk_node n loc inlined inputs outputs params b probes =
+  { n_name = n; n_inputs = inputs; n_outputs = outputs;
+    n_body = b; n_params = params; n_constraints = [];
+    n_loc = loc; n_inlined = inlined; n_probes = probes }
+
+let mk_program cds nds =
+  { p_consts = cds; p_nodes = nds }
diff --git a/minijazz/src/global/errors.ml b/minijazz/src/global/errors.ml
new file mode 100644
index 0000000..9f64d36
--- /dev/null
+++ b/minijazz/src/global/errors.ml
@@ -0,0 +1,22 @@
+open Location
+
+exception Error
+
+type lexical_error =
+  | Illegal_character
+  | Unterminated_comment
+  | Bad_char_constant
+  | Unterminated_string
+
+let lexical_error err loc =
+  Format.eprintf (match err with
+    | Illegal_character -> Pervasives.format_of_string "%aIllegal character.@."
+    | Unterminated_comment -> "%aUnterminated comment.@."
+    | Bad_char_constant -> "%aBad char constant.@."
+    | Unterminated_string -> "%aUnterminated string.@."
+     ) print_location loc;
+  raise Error
+
+let syntax_error loc =
+  Format.eprintf "%aSyntax error.@." print_location loc;
+  raise Error
diff --git a/minijazz/src/global/ident.ml b/minijazz/src/global/ident.ml
new file mode 100644
index 0000000..9e36549
--- /dev/null
+++ b/minijazz/src/global/ident.ml
@@ -0,0 +1,39 @@
+
+type t = {
+  i_id : int;
+  i_name : string;
+  i_from_source : bool
+}
+
+let string_of_ident id =
+  if id.i_from_source then
+    id.i_name
+  else
+    id.i_name^"_"^(string_of_int id.i_id)
+
+let print_ident ff id =
+  Format.fprintf ff "%s" (string_of_ident id)
+
+module StringEnv = Map.Make (struct type t = string let compare = compare end)
+
+let ident_counter = ref 0
+let fresh_ident from_source s =
+  incr ident_counter;
+  { i_id = !ident_counter; i_name = s; i_from_source = from_source }
+
+let copy id =
+  fresh_ident false (string_of_ident id)
+
+let symbol_table = ref StringEnv.empty
+let reset_symbol_table () =
+  symbol_table := StringEnv.empty
+let ident_of_string s =
+  if StringEnv.mem s !symbol_table then
+    StringEnv.find s !symbol_table
+  else (
+    let id = fresh_ident true s in
+    symbol_table := StringEnv.add s id !symbol_table;
+    id
+  )
+
+let fresh_ident = fresh_ident false
diff --git a/minijazz/src/global/location.ml b/minijazz/src/global/location.ml
new file mode 100644
index 0000000..1837584
--- /dev/null
+++ b/minijazz/src/global/location.ml
@@ -0,0 +1,130 @@
+(* Printing a location in the source program *)
+(* inspired from the source of the Caml Light 0.73 compiler *)
+
+open Lexing
+open Parsing
+open Format
+
+(* two important global variables: [input_name] and [input_chan] *)
+type location =
+    Loc of position  (* Position of the first character *)
+         * position  (* Position of the next character following the last one *)
+
+
+let input_name = ref ""                 (* Input file name. *)
+
+let input_chan = ref stdin              (* The channel opened on the input. *)
+
+let initialize iname ic =
+  input_name := iname;
+  input_chan := ic
+
+
+let no_location =  Loc (dummy_pos, dummy_pos)
+
+let error_prompt = ">"
+
+
+(** Prints [n] times char [c] on [oc]. *)
+let prints_n_chars ff n c = for i = 1 to n do pp_print_char ff c done
+
+(** Prints out to [oc] a line designed to be printed under [line] from file [ic]
+  underlining from char [first] to char [last] with char [ch].
+  [line] is the index of the first char of line. *)
+let underline_line ic ff ch line first last =
+  let c = ref ' '
+  and f = ref first
+  and l = ref (last-first) in
+  ( try
+    seek_in ic line;
+    pp_print_string ff error_prompt;
+    while c := input_char ic; !c != '\n' do
+      if !f > 0 then begin
+        f := !f - 1;
+        pp_print_char ff (if !c == '\t' then !c else ' ')
+      end
+      else if !l > 0 then begin
+        l := !l - 1;
+        pp_print_char ff (if !c == '\t' then !c else ch)
+      end
+      else ()
+    done
+  with End_of_file ->
+    if !f = 0 && !l > 0 then prints_n_chars ff 5 ch )
+
+
+let copy_lines nl ic ff prompt =
+  for i = 1 to nl do
+    pp_print_string ff prompt;
+    (try pp_print_string ff (input_line ic)
+     with End_of_file -> pp_print_string ff "<EOF>");
+    fprintf ff "@\n"
+  done
+
+let copy_chunk p1 p2 ic ff =
+  try for i = p1 to p2 - 1 do pp_print_char ff (input_char ic) done
+  with End_of_file -> pp_print_string ff "<EOF>"
+
+
+
+let skip_lines n ic =
+  try for i = 1 to n do
+    let _ = input_line ic in ()
+    done
+  with End_of_file -> ()
+
+
+
+let print_location ff (Loc(p1,p2)) =
+  let n1 = p1.pos_cnum - p1.pos_bol in (* character number *)
+  let n2 = p2.pos_cnum - p2.pos_bol in
+  let np1 = p1.pos_cnum in (* character position *)
+  let np2 = p2.pos_cnum in
+  let l1 = p1.pos_lnum in (* line number *)
+  let l2 = p2.pos_lnum in
+  let lp1 = p1.pos_bol in (* line position *)
+  let lp2 = p2.pos_bol in
+  let f1 = p1.pos_fname in (* file name *)
+  let f2 = p2.pos_fname in
+
+  if f1 != f2 then (* Strange case *)
+    fprintf ff
+    "File \"%s\" line %d, character %d, to file \"%s\" line %d, character %d@."
+      f1 l1 n1 f2 l2 n2
+
+  else begin (* Same file *)
+    if l2 > l1 then
+      fprintf ff
+        "File \"%s\", line %d-%d, characters %d-%d:@\n" f1 l1 l2 n1 n2
+    else
+      fprintf ff "File \"%s\", line %d, characters %d-%d:@\n" f1 l1 n1 n2;
+    (* Output source code *)
+    try
+      let ic = open_in f1 in
+
+      if l1 == l2 then (
+        (* Only one line : copy full line and underline *)
+        seek_in ic lp1;
+        copy_lines 1 ic ff ">";
+        underline_line ic ff '^' lp1 n1 n2 )
+      else (
+        underline_line ic ff '.' lp1 0 n1; (* dots until n1 *)
+        seek_in ic np1;
+        (* copy the end of the line l1 after the dots *)
+        copy_lines 1 ic ff "";
+        if l2 - l1 <= 8 then
+          (* copy the 6 or less middle lines *)
+          copy_lines (l2-l1-1) ic ff ">"
+        else (
+          (* sum up the middle lines to 6 *)
+          copy_lines 3 ic ff ">";
+          fprintf ff "..........@\n";
+          skip_lines (l2-l1-7) ic; (* skip middle lines *)
+          copy_lines 3 ic ff ">"
+        );
+        fprintf ff ">";
+        copy_chunk lp2 np2 ic ff; (* copy interesting begining of l2 *)
+      )
+    with Sys_error _ -> ();
+  end;
+  fprintf ff "@."
diff --git a/minijazz/src/global/mapfold.ml b/minijazz/src/global/mapfold.ml
new file mode 100644
index 0000000..50ffbaf
--- /dev/null
+++ b/minijazz/src/global/mapfold.ml
@@ -0,0 +1,164 @@
+open Ast
+open Static
+open Misc
+
+exception Fallback
+
+type 'a it_funs = {
+  static_exp : 'a it_funs -> 'a -> static_exp -> static_exp * 'a;
+  static_exp_desc : 'a it_funs -> 'a -> static_exp_desc -> static_exp_desc * 'a;
+  ty : 'a it_funs -> 'a -> ty -> ty * 'a;
+  link : 'a it_funs -> 'a -> link -> link * 'a;
+  edesc : 'a it_funs -> 'a -> edesc -> edesc * 'a;
+  exp : 'a it_funs -> 'a -> exp -> exp * 'a;
+  pat : 'a it_funs -> 'a -> pat -> pat * 'a;
+  equation : 'a it_funs -> 'a -> equation -> equation * 'a;
+  var_dec : 'a it_funs -> 'a -> var_dec -> var_dec * 'a;
+  block : 'a it_funs -> 'a -> block -> block * 'a;
+  node_dec : 'a it_funs -> 'a -> node_dec -> node_dec * 'a;
+  const_dec : 'a it_funs -> 'a -> const_dec -> const_dec * 'a;
+  program : 'a it_funs -> 'a -> program -> program * 'a;
+}
+
+let rec exp_it funs acc e = funs.exp funs acc e
+and exp funs acc e =
+  let e_desc, acc = edesc_it funs acc e.e_desc in
+  let e_ty, acc = ty_it funs acc e.e_ty in
+  { e with e_desc = e_desc; e_ty = e_ty }, acc
+
+and edesc_it funs acc ed =
+  try funs.edesc funs acc ed
+  with Fallback -> edesc funs acc ed
+and edesc funs acc ed = match ed with
+  | Econst v -> Econst v, acc
+  | Evar id -> Evar id, acc
+  | Ereg e ->
+      let e, acc = exp_it funs acc e in
+      Ereg e, acc
+  | Emem(k, addr_size, word_size, s, args) ->
+      let addr_size, acc = static_exp_it funs acc addr_size in
+      let word_size, acc = static_exp_it funs acc word_size in
+      let args, acc = mapfold (exp_it funs) acc args in
+      Emem(k, addr_size, word_size, s, args), acc
+  | Ecall(id, params, args) ->
+      let params, acc = mapfold (static_exp_it funs) acc params in
+      let args, acc = mapfold (exp_it funs) acc args in
+      Ecall(id, params, args), acc
+
+and static_exp_it funs acc sd =
+  try funs.static_exp funs acc sd
+  with Fallback -> static_exp funs acc sd
+and static_exp funs acc se =
+  let se_desc, acc = static_exp_desc_it funs acc se.se_desc in
+  { se with se_desc = se_desc }, acc
+
+and static_exp_desc_it funs acc sed =
+  try funs.static_exp_desc funs acc sed
+  with Fallback -> static_exp_desc funs acc sed
+and static_exp_desc funs acc sed = match sed with
+  | SInt _ | SBool _ | SVar _ -> sed, acc
+  | SBinOp (sop, se1, se2) ->
+      let se1, acc = static_exp_it funs acc se1 in
+      let se2, acc = static_exp_it funs acc se2 in
+      SBinOp(sop, se1, se2), acc
+  | SIf(c, se1, se2) ->
+      let c, acc = static_exp_it funs acc c in
+      let se1, acc = static_exp_it funs acc se1 in
+      let se2, acc = static_exp_it funs acc se2 in
+      SIf(c, se1, se2), acc
+
+and ty_it funs acc t = try funs.ty funs acc t with Fallback -> ty funs acc t
+and ty funs acc t = match t with
+  | TUnit | TBit -> t, acc
+  | TBitArray se ->
+      let se, acc = static_exp_it funs acc se in
+      TBitArray se, acc
+  | TProd t_l ->
+      let t_l, acc = mapfold (ty_it funs) acc t_l in
+      TProd t_l, acc
+  | TVar link ->
+      let link_v, acc = link_it funs acc !link in
+      link := link_v;
+      TVar link, acc
+
+and link_it funs acc c =
+  try funs.link funs acc c
+  with Fallback -> link funs acc c
+and link funs acc l = match l with
+  | TIndex _ -> l, acc
+  | TLink ty ->
+      let ty, acc = ty_it funs acc ty in
+      TLink ty, acc
+
+and pat_it funs acc p =
+  try funs.pat funs acc p
+  with Fallback -> pat funs acc p
+and pat funs acc p = p, acc
+
+and equation_it funs acc eq = funs.equation funs acc eq
+and equation funs acc (pat, e) =
+  let pat, acc = pat_it funs acc pat in
+  let e, acc = exp_it funs acc e in
+  (pat, e), acc
+
+and block_it funs acc b =
+  try funs.block funs acc b
+  with Fallback -> block funs acc b
+and block funs acc b = match b with
+  | BEqs(eqs, vds) ->
+      let vds, acc = mapfold (var_dec_it funs) acc vds in
+      let eqs, acc = mapfold (equation_it funs) acc eqs in
+      BEqs (eqs, vds), acc
+  | BIf(se, b1, b2) ->
+      let se, acc = static_exp_it funs acc se in
+      let b1, acc = block_it funs acc b1 in
+      let b2, acc = block_it funs acc b2 in
+      BIf(se, b1, b2), acc
+
+and var_dec_it funs acc vd = funs.var_dec funs acc vd
+and var_dec funs acc vd =
+  let v_ty, acc = ty_it funs acc vd.v_ty in
+  { vd with v_ty = v_ty }, acc
+
+
+and node_dec_it funs acc nd = funs.node_dec funs acc nd
+and node_dec funs acc nd =
+  let n_inputs, acc = mapfold (var_dec_it funs) acc nd.n_inputs in
+  let n_outputs, acc = mapfold (var_dec_it funs) acc nd.n_outputs in
+  let n_constraints, acc = mapfold (static_exp_it funs) acc nd.n_constraints in
+  let n_body, acc = block_it funs acc nd.n_body in
+  { nd with
+      n_inputs = n_inputs;
+      n_outputs = n_outputs;
+      n_body = n_body;
+      n_constraints = n_constraints }
+  , acc
+
+
+and const_dec_it funs acc c = funs.const_dec funs acc c
+and const_dec funs acc c =
+  let c_value, acc = static_exp_it funs acc c.c_value in
+  { c with c_value = c_value }, acc
+
+and program_it funs acc p = funs.program funs acc p
+and program funs acc p =
+  let p_consts, acc = mapfold (const_dec_it funs) acc p.p_consts in
+  let p_nodes, acc = mapfold (node_dec_it funs) acc p.p_nodes in
+  { p_nodes = p_nodes; p_consts = p_consts }, acc
+
+
+let defaults = {
+  static_exp = static_exp;
+  static_exp_desc = static_exp_desc;
+  ty = ty;
+  link = link;
+  edesc = edesc;
+  exp = exp;
+  pat = pat;
+  equation = equation;
+  var_dec = var_dec;
+  block = block;
+  node_dec = node_dec;
+  const_dec = const_dec;
+  program = program;
+}
diff --git a/minijazz/src/global/misc.ml b/minijazz/src/global/misc.ml
new file mode 100644
index 0000000..3a45456
--- /dev/null
+++ b/minijazz/src/global/misc.ml
@@ -0,0 +1,115 @@
+
+(* Functions to decompose a list into a tuple *)
+exception Arity_error of int * int (*expected, found*)
+exception Arity_min_error of int * int (*expected, found*)
+
+let try_1 = function
+  | [v] -> v
+  | l -> raise (Arity_error(1, List.length l))
+
+let try_2 = function
+  | [v1; v2] -> v1, v2
+  | l -> raise (Arity_error(2, List.length l))
+
+let try_3 = function
+  | [v1; v2; v3] -> v1, v2, v3
+  | l -> raise (Arity_error(3, List.length l))
+
+let try_4 = function
+  | [v1; v2; v3; v4] -> v1, v2, v3, v4
+  | l -> raise (Arity_error(4, List.length l))
+
+let try_1min = function
+  | v::l -> v, l
+  | l -> raise (Arity_min_error(1, List.length l))
+
+let assert_fun f l =
+  try
+    f l
+  with
+      Arity_error(expected, found) ->
+        Format.eprintf "Internal compiler error: \
+     wrong list size (found %d, expected %d).@." found expected;
+        assert false
+
+let assert_min_fun f l =
+  try
+    f l
+  with
+      Arity_min_error(expected, found) ->
+        Format.eprintf "Internal compiler error: \
+     wrong list size (found %d, expected %d at least).@." found expected;
+        assert false
+
+let assert_1 l = assert_fun try_1 l
+let assert_2 l = assert_fun try_2 l
+let assert_3 l = assert_fun try_3 l
+let assert_4 l = assert_fun try_4 l
+
+let assert_1min l = assert_min_fun try_1min l
+
+let mapfold f acc l =
+  let l,acc = List.fold_left
+                (fun (l,acc) e -> let e,acc = f acc e in e::l, acc)
+                ([],acc) l in
+  List.rev l, acc
+
+let mapi f l =
+  let rec aux i = function
+    | [] -> []
+    | v::l -> (f i v)::(aux (i+1) l)
+  in
+    aux 1 l
+
+let unique l =
+  let tbl = Hashtbl.create (List.length l) in
+  List.iter (fun i -> Hashtbl.replace tbl i ()) l;
+  Hashtbl.fold (fun key _ accu -> key :: accu) tbl []
+
+let is_empty = function | [] -> true | _ -> false
+
+let gen_symbol =
+  let counter = ref 0 in
+  let _gen_symbol () =
+    counter := !counter + 1;
+    "_"^(string_of_int !counter)
+  in
+    _gen_symbol
+
+let bool_of_string s = match s with
+  | "t" | "1" -> true
+  | "f" | "0" -> false
+  | _ -> raise (Invalid_argument ("bool_of_string"))
+
+let bool_array_of_string s =
+  let a = Array.make (String.length s) false in
+  for i = 0 to String.length s - 1 do
+    a.(i) <- bool_of_string (String.sub s i 1)
+  done;
+  a
+
+exception Int_too_big
+let convert_size s n =
+  let m = String.length s in
+  if m > n then
+    raise Int_too_big
+  else
+    if m = n then s else (String.make (n - m) '0')^s
+
+let binary_not s =
+  for i=0 to String.length s - 1 do
+    s.[i] <- if s.[i] = '0' then '1' else '0'
+  done;
+  s
+
+let rec binary_string_of_int i n =
+  let rec s_of_i i = match i with
+    | 0 -> "0"
+    | 1 -> "1"
+    | i when i < 0 -> binary_not (binary_string_of_int (-i-1) n)
+    | _ ->
+      let q, r = i / 2, i mod 2 in
+      (s_of_i q) ^ (s_of_i r)
+  in
+  convert_size (s_of_i i) n
+
diff --git a/minijazz/src/global/printer.ml b/minijazz/src/global/printer.ml
new file mode 100644
index 0000000..747541d
--- /dev/null
+++ b/minijazz/src/global/printer.ml
@@ -0,0 +1,156 @@
+open Ident
+open Ast
+open Static
+open Format
+open Misc
+
+let print_name ff n = fprintf ff "%s" n
+
+let rec print_list_r print lp sep rp ff = function
+  | [] -> ()
+  | x :: l ->
+      fprintf ff "%s%a" lp print x;
+      List.iter (fprintf ff "%s %a" sep print) l;
+      fprintf ff "%s" rp
+
+let rec print_list_nlr print lp sep rp ff = function
+  | [] -> ()
+  | x :: l ->
+      fprintf ff "%s%a" lp print x;
+      List.iter (fprintf ff "%s@ %a" sep print) l;
+      fprintf ff "%s" rp
+
+let print_bool ff b =
+  if b then
+    fprintf ff "1"
+  else
+    fprintf ff "0"
+
+let rec print_const ff v = match v with
+  | VBit b -> print_bool ff b
+  | VBitArray a when Array.length a = 0 -> fprintf ff "[]"
+  | VBitArray l -> Array.iter (print_bool ff) l
+
+let rec print_static_exp ff se = match se.se_desc with
+  | SInt i -> fprintf ff "%d" i
+  | SBool b -> print_bool ff b
+  | SVar n -> print_name ff n
+  | SBinOp(op, se1, se2) ->
+    let op_str = match op with
+      | SAdd -> "+" | SMinus -> "-"
+      | SMult -> "*" | SDiv -> "/"
+      | SPower -> "^" | SEqual -> "="
+      | SLess -> "<" | SLeq -> "<="
+      | SGreater -> ">" | SGeq -> ">=" in
+      fprintf ff "(%a %s %a)" print_static_exp se1  op_str  print_static_exp se2
+  | SIf (c, se1, se2) ->
+      fprintf ff "(%a ? %a : %a)"
+        print_static_exp c  print_static_exp se1  print_static_exp se2
+
+let rec print_static_type ff sty = match sty with
+  | STInt -> fprintf ff "int"
+  | STBool -> fprintf ff "bool"
+
+let rec print_type ff ty = match ty with
+  | TUnit -> fprintf ff "()"
+  | TBit -> fprintf ff "bit"
+  | TBitArray se -> fprintf ff "bit[%a]" print_static_exp se
+  | TProd l ->  print_list_r print_type "" "*" "" ff l
+  | TVar _ -> fprintf ff "<var>"
+
+let print_call_params ff params = match params with
+  | [] -> ()
+  | _ -> print_list_r print_static_exp "<<"","">>" ff params
+
+let rec print_exp ff e =
+  if !Cli_options.print_types then
+    fprintf ff "(%a : %a)" print_edesc e.e_desc print_type e.e_ty
+  else
+    fprintf ff "%a" print_edesc e.e_desc
+
+and print_edesc ff ed = match ed with
+  | Econst v -> print_const ff v
+  | Evar n -> print_ident ff n
+  | Ereg e -> fprintf ff "reg %a" print_exp e
+  | Ecall("select", idx::_, args) ->
+      let e1 = assert_1 args in
+        fprintf ff "%a[%a]" print_exp e1  print_static_exp idx
+  | Ecall("slice", low::high::_, args) ->
+      let e1 = assert_1 args in
+        fprintf ff "%a[%a..%a]"
+          print_exp e1  print_static_exp low  print_static_exp high
+  | Ecall("concat", _, args) ->
+      let e1, e2 = assert_2 args in
+        fprintf ff "%a . %a" print_exp e1  print_exp e2
+  | Ecall(fn, params, args) ->
+      fprintf ff "%a%a%a" print_name fn  print_call_params params  print_args args
+  | Emem(MRom, addr_size, word_size, _, args) ->
+      fprintf ff "rom<%a,%a>%a"
+        print_static_exp addr_size  print_static_exp word_size  print_args args
+  | Emem(MRam, addr_size, word_size, _, args) ->
+      fprintf ff "ram<%a,%a>%a"
+        print_static_exp addr_size  print_static_exp word_size  print_args args
+
+and print_args ff args =
+  print_list_r print_exp "(" "," ")" ff args
+
+let rec print_pat ff pat = match pat with
+  | Evarpat id -> print_ident ff id
+  | Etuplepat l -> print_list_r print_ident "(" "," ")" ff l
+
+let print_eq ff (pat, e) =
+  fprintf ff "%a = %a" print_pat pat  print_exp e
+
+let print_eqs ff eqs =
+  print_list_nlr print_eq """;""" ff eqs
+
+let print_var_dec ff vd = match vd.v_ty with
+  | TUnit -> fprintf ff "@[%a : .@]" print_ident vd.v_ident
+  | TBit -> fprintf ff "@[%a@]" print_ident vd.v_ident
+  | TBitArray se ->
+    fprintf ff "@[%a : [%a]@]" print_ident vd.v_ident  print_static_exp se
+  | TProd _ -> assert false
+  | TVar _ -> fprintf ff "%a : <var>" print_ident vd.v_ident
+
+let print_var_decs ff vds =
+  print_list_r print_var_dec "("","")" ff vds
+
+let rec print_block ff b = match b with
+  | BEqs (eqs, []) -> print_eqs ff eqs
+  | BEqs (eqs, vds) ->
+    fprintf ff "@[<v 2>var %a@] in@,%a" print_var_decs vds print_eqs eqs
+  | BIf(se, thenb, elseb) ->
+      fprintf ff "@[<v 2>if %a then@,%a@]@,@[<v 2>else@,%a@]"
+        print_static_exp se
+        print_block thenb
+        print_block elseb
+
+let print_param ff p =
+  print_name ff p.p_name
+
+let print_params ff params = match params with
+  | [] -> ()
+  | _ -> print_list_r print_param "<<"","">>" ff params
+
+let print_constraints ff cl =
+  if !Cli_options.print_types then
+    fprintf ff " with %a" (print_list_r print_static_exp "" " and " "") cl
+
+let print_node ff n =
+  fprintf ff "@[<v2>@[%a%a%a = %a@] where@ %a@.end where%a;@]@\n@."
+    print_name n.n_name
+    print_params n.n_params
+    print_var_decs n.n_inputs
+    print_var_decs n.n_outputs
+    print_block n.n_body
+    print_constraints n.n_constraints
+
+let print_const_dec ff cd =
+  fprintf ff "const %a = %a@\n@."
+    print_name cd.c_name  print_static_exp cd.c_value
+
+let print_program oc p =
+  let ff = formatter_of_out_channel oc in
+    List.iter (print_const_dec ff) p.p_consts;
+    List.iter (print_node ff) p.p_nodes
+
diff --git a/minijazz/src/global/static.ml b/minijazz/src/global/static.ml
new file mode 100644
index 0000000..352e62e
--- /dev/null
+++ b/minijazz/src/global/static.ml
@@ -0,0 +1,31 @@
+open Errors
+open Location
+
+type name = string
+module NameEnv = Map.Make (struct type t = name let compare = compare end)
+
+type sop =
+  | SAdd | SMinus | SMult | SDiv | SPower (*int*)
+  | SEqual | SLess | SLeq | SGreater | SGeq (*bool*)
+
+type static_exp_desc =
+  | SInt of int
+  | SBool of bool
+  | SVar of name
+  | SBinOp of sop * static_exp * static_exp
+  | SIf of static_exp * static_exp * static_exp (* se1 ? se2 : se3 *)
+
+and static_exp =
+    { se_desc : static_exp_desc;
+      se_loc : location }
+
+type static_ty = STInt | STBool
+
+let mk_static_exp ?(loc = no_location) desc =
+  { se_desc = desc; se_loc = loc }
+let mk_static_var s =
+  mk_static_exp (SVar s)
+let mk_static_int i =
+  mk_static_exp (SInt i)
+let mk_static_bool b =
+  mk_static_exp (SBool b)
diff --git a/minijazz/src/global/static_utils.ml b/minijazz/src/global/static_utils.ml
new file mode 100644
index 0000000..f95ce30
--- /dev/null
+++ b/minijazz/src/global/static_utils.ml
@@ -0,0 +1,76 @@
+open Static
+
+let pow a n =
+  let rec g p x = function
+  | 0 -> x
+  | i ->
+      g (p * p) (if i mod 2 = 1 then p * x else x) (i/2)
+  in
+  g a 1 n
+;;
+
+
+let fun_of_op op = match op with
+  | SAdd -> (+) | SMinus -> (-)
+  | SMult -> (fun i1 i2 -> i1 * i2)
+  | SDiv -> (/)
+  | SPower -> pow
+  | _ -> assert false
+
+let fun_of_comp_op op = match op with
+  | SEqual -> (=) | SLeq -> (<=)  | SLess -> (<)
+  | _ -> assert false
+
+let rec simplify env se = match se.se_desc with
+  | SInt _ | SBool _ -> se
+  | SVar n ->
+      (try
+         let se = NameEnv.find n env in
+         simplify env se
+        with
+          | Not_found -> se)
+  | SBinOp(op, se1, se2) ->
+      let se1 = simplify env se1 in
+      let se2 = simplify env se2 in
+      let desc =
+        match op, se1.se_desc, se2.se_desc with
+          | (SAdd | SMinus | SDiv  | SMult | SPower), SInt i1, SInt i2 ->
+              let f = fun_of_op op in
+              SInt (f i1 i2)
+        | (SEqual | SLess | SLeq | SGreater | SGeq), SInt i1, SInt i2 ->
+            let f = fun_of_comp_op op in
+            SBool (f i1 i2)
+        | _, _, _ -> SBinOp(op, se1, se2)
+      in
+      { se with se_desc = desc }
+  | SIf(c, se1, se2) ->
+      let c = simplify env c in
+      let se1 = simplify env se1 in
+      let se2 = simplify env se2 in
+      (match c.se_desc, se1.se_desc, se2.se_desc with
+        | SBool true, _, _ -> se1
+        | SBool false, _, _ -> se2
+        | _, sed1, sed2 when sed1 = sed2 -> { se with se_desc = sed1 }
+        | _, _, _ -> { se with se_desc = SIf(c, se1, se2) })
+
+let rec subst env se = match se.se_desc with
+  | SInt _ | SBool _ -> se
+  | SVar n ->
+      (try
+          NameEnv.find n env
+        with
+          | Not_found -> se)
+  | SBinOp(op, se1, se2) ->
+      { se with se_desc = SBinOp(op, subst env se1, subst env se2) }
+  | SIf(c, se1, se2) ->
+      { se with se_desc = SIf(subst env c, subst env se1, subst env se2) }
+
+exception Unsatisfiable of static_exp
+let check_true env cl =
+  let check_one c =
+    let res = simplify env c in
+    match res.se_desc with
+      | SBool true -> ()
+      | _ -> raise (Unsatisfiable c)
+  in
+  List.iter check_one cl