summaryrefslogtreecommitdiff
path: root/minijazz/src/global
diff options
context:
space:
mode:
Diffstat (limited to 'minijazz/src/global')
-rw-r--r--minijazz/src/global/_tags0
-rw-r--r--minijazz/src/global/ast.ml107
-rw-r--r--minijazz/src/global/errors.ml22
-rw-r--r--minijazz/src/global/ident.ml39
-rw-r--r--minijazz/src/global/location.ml130
-rw-r--r--minijazz/src/global/mapfold.ml164
-rw-r--r--minijazz/src/global/misc.ml115
-rw-r--r--minijazz/src/global/printer.ml156
-rw-r--r--minijazz/src/global/static.ml31
-rw-r--r--minijazz/src/global/static_utils.ml76
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-21 21:11:42 +0000