diff options
Diffstat (limited to 'src/pretty_print.ml')
| -rw-r--r-- | src/pretty_print.ml | 87 |
1 files changed, 66 insertions, 21 deletions
diff --git a/src/pretty_print.ml b/src/pretty_print.ml index 87a7b94c..6e3605e7 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -1272,14 +1272,14 @@ let doc_typ_ocaml, doc_atomic_typ_ocaml = let doc_lit_ocaml (L_aux(l,_)) = utf8string (match l with | L_unit -> "()" - | L_zero -> "0" - | L_one -> "1" - | L_true -> "1" - | L_false -> "0" + | L_zero -> "Vzero" + | L_one -> "Vone" + | L_true -> "Vone" + | L_false -> "Vzero" | L_num i -> string_of_int i - | L_hex n -> "(num_to_vec" ^ ("0x" ^ n) ^ ")" - | L_bin n -> "(num_to_vec" ^ ("0b" ^ n) ^ ")" - | L_undef -> "2" + | L_hex n -> "(num_to_vec" ^ ("0x" ^ n) ^ ")" (*shouldn't happen*) + | L_bin n -> "(num_to_vec" ^ ("0b" ^ n) ^ ")" (*shouldn't happen*) + | L_undef -> "Vundef" | L_string s -> "\"" ^ s ^ "\"") (* typ_doc is the doc for the type being quantified *) @@ -1408,9 +1408,12 @@ let doc_exp_ocaml, doc_let_ocaml = (match annot with | Base((_, ({t = Tapp("reg",_)} | {t=Tabbrev(_,{t=Tapp("reg",_)})})),_,_,_,_,_) -> string "!" ^^ doc_id_ocaml id + | Base((_,({t=Tapp("register",_)} | {t=Tabbrev(_,{t=Tapp("register",_)})})), External _,_,_,_,_) -> + string "!" ^^ doc_id_ocaml id | Base(_,Alias alias_info,_,_,_,_) -> (match alias_info with - | Alias_field(reg,field) -> parens (string "get_register_field" ^^ space ^^ string reg ^^ string_lit (string field)) + | Alias_field(reg,field) -> + parens (string "get_register_field" ^^ space ^^ string reg ^^ string_lit (string field)) | Alias_extract(reg,start,stop) -> if start = stop then parens (string "bit_vector_access" ^^ space ^^ string reg ^^ space ^^ doc_int start) @@ -1419,7 +1422,7 @@ let doc_exp_ocaml, doc_let_ocaml = parens (string "vector_append" ^^ space ^^ string reg1 ^^ space ^^ string reg2)) | _ -> doc_id_ocaml id) | E_lit lit -> doc_lit lit - | E_cast(typ,e) -> (parens (doc_op colon (group (exp e)) (doc_typ typ))) + | E_cast(typ,e) -> (parens (doc_op colon (group (exp e)) (doc_typ_ocaml typ))) | E_tuple exps -> parens (separate_map comma exp exps) | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> @@ -1547,8 +1550,8 @@ let doc_exp_ocaml, doc_let_ocaml = string reg ^^ space ^^ doc_int start ^^ space ^^ doc_int stop ^^ space ^^ exp e_new_v) | Alias_pair(reg1,reg2) -> parens ((string "set_two_regs") ^^ space ^^ string reg1 ^^ space ^^ string reg2 ^^ space ^^ exp e_new_v)) - | _ -> - parens (string "set_named_register" ^^ space ^^ string_lit (doc_id_ocaml id) ^^ space ^^ (exp e_new_v))) + | _ -> + doc_op (string ":=") (doc_id_ocaml id) (exp e_new_v)) and doc_lexp_fcall ((LEXP_aux(lexp,(l,annot))) as le) e_new_v = match lexp with | LEXP_memory(id,args) -> doc_id_ocaml id ^^ parens (separate_map comma exp (args@[e_new_v])) @@ -1590,13 +1593,27 @@ let doc_typdef_ocaml (TD_aux(td,_)) = match td with match n1,n2 with | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) -> let dir = i1 < i2 in + let size = if dir then i2-i1 -1 else i1-i2 -1 in doc_op equals ((string "let") ^^ space ^^ doc_id_ocaml id ^^ space ^^ (string "init_val")) - (separate space [string "Vregister"; - (parens (separate comma_sp [string "init_val"; - doc_nexp n1; - string (if dir then "true" else "false"); - brackets doc_rids]))]) + (separate space [string "ref"; + string "Vregister"; + (parens (separate comma_sp + [parens (separate space + [string "match init_val with"; + pipe; + string "None"; + arrow; + string "Array.make"; + doc_int size; + string "Vzero"; + pipe; + string "Some init_val"; + arrow; + string "init_val";]); + doc_nexp n1; + string (if dir then "true" else "false"); + brackets doc_rids]))]) let doc_rec_ocaml (Rec_aux(r,_)) = match r with | Rec_nonrec -> empty @@ -1628,14 +1645,42 @@ let doc_fundef_ocaml (FD_aux(FD_function(r, typa, efa, fcls),_)) = (string "function"); clauses] -(*Aliases should be removed by here; registers not sure about*) -(*let doc_dec (DEC_aux (reg,_)) = +let doc_dec_ocaml (DEC_aux (reg,(l,annot))) = match reg with - | DEC_reg(typ,id) -> separate space [string "register"; doc_atomic_typ typ; doc_id id] + | DEC_reg(typ,id) -> + (match annot with + | Base((_,t),_,_,_,_,_) -> + (match t.t with + | Tapp("register", [TA_typ {t= Tapp("vector", [TA_nexp start; TA_nexp size; TA_ord order; TA_typ itemt])}]) -> + (match itemt.t,start.nexp,size.nexp with + | Tid "bit", Nconst start, Nconst size -> + let o = if order.order = Oinc then string "true" else string "false" in + separate space [string "let"; + doc_id_ocaml id; + equals; + string "ref"; + parens (separate space + [string "Vregister"; + parens (separate comma [doc_int (int_of_big_int start); + o; + parens (separate space + [string "Array.make"; + doc_int (int_of_big_int size); + string "Vzero"; + string "[]"])])])] + | _ -> empty) + | Tapp("register", [TA_typ {t=Tid idt}]) -> + separate space [string "let"; + doc_id_ocaml id; + equals; + string idt; + string "None"] + |_-> empty) + | _ -> empty) | DEC_alias(id,alspec) -> doc_op equals (string "register alias" ^^ space ^^ doc_id id) (doc_alias alspec) | DEC_typ_alias(typ,id,alspec) -> - doc_op equals (string "register alias" ^^ space ^^ doc_atomic_typ typ) (doc_alias alspec)*) + doc_op equals (string "register alias" ^^ space ^^ doc_atomic_typ typ) (doc_alias alspec) let doc_def_ocaml def = group (match def with | DEF_default df -> empty @@ -1643,7 +1688,7 @@ let doc_def_ocaml def = group (match def with | DEF_type t_def -> doc_typdef_ocaml t_def | DEF_fundef f_def -> doc_fundef_ocaml f_def | DEF_val lbind -> doc_let_ocaml lbind - | DEF_reg_dec dec -> empty (*unless we want to have something for the declaration of a register and guess a default init value*) + | DEF_reg_dec dec -> doc_dec_ocaml dec | DEF_scattered sdef -> empty (*shoulnd't still be here*) ) ^^ hardline |