diff options
Diffstat (limited to 'src/pretty_print_ocaml.ml')
| -rw-r--r-- | src/pretty_print_ocaml.ml | 705 |
1 files changed, 0 insertions, 705 deletions
diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml deleted file mode 100644 index 74461aab..00000000 --- a/src/pretty_print_ocaml.ml +++ /dev/null @@ -1,705 +0,0 @@ -(**************************************************************************) -(* Sail *) -(* *) -(* Copyright (c) 2013-2017 *) -(* Kathyrn Gray *) -(* Shaked Flur *) -(* Stephen Kell *) -(* Gabriel Kerneis *) -(* Robert Norton-Wright *) -(* Christopher Pulte *) -(* Peter Sewell *) -(* *) -(* All rights reserved. *) -(* *) -(* This software was developed by the University of Cambridge Computer *) -(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) -(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) -(* *) -(* Redistribution and use in source and binary forms, with or without *) -(* modification, are permitted provided that the following conditions *) -(* are met: *) -(* 1. Redistributions of source code must retain the above copyright *) -(* notice, this list of conditions and the following disclaimer. *) -(* 2. Redistributions in binary form must reproduce the above copyright *) -(* notice, this list of conditions and the following disclaimer in *) -(* the documentation and/or other materials provided with the *) -(* distribution. *) -(* *) -(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) -(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) -(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) -(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) -(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) -(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) -(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) -(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) -(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) -(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) -(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) -(* SUCH DAMAGE. *) -(**************************************************************************) - -open Big_int -open Ast -open Ast_util -open Type_check -open PPrint -open Pretty_print_common - -(**************************************************************************** - * PPrint-based sail-to-ocaml pretty printer -****************************************************************************) - -let star_sp = star ^^ space - -let sanitize_name s = - "_" ^ s - -let doc_id_ocaml (Id_aux(i,_)) = - match i with - | Id("bit") -> string "vbit" - | Id i -> string (sanitize_name i) - | DeIid x -> - (* add an extra space through empty to avoid a closing-comment - * token in case of x ending with star. *) - parens (separate space [colon; string x; empty]) - -let doc_id_ocaml_type (Id_aux(i,_)) = - match i with - | Id("bit") -> string "vbit" - | Id i -> string (sanitize_name i) - | DeIid x -> - (* add an extra space through empty to avoid a closing-comment - * token in case of x ending with star. *) - parens (separate space [colon; string (String.uncapitalize x); empty]) - -let doc_id_ocaml_ctor (Id_aux(i,_)) = - match i with - | Id("bit") -> string "vbit" - | Id i -> string ((* TODO if n > 246 then "`" else "") ^ *) (String.capitalize i)) - | DeIid x -> - (* add an extra space through empty to avoid a closing-comment - * token in case of x ending with star. *) - parens (separate space [colon; string (String.capitalize x); empty]) - -let doc_typ_ocaml, doc_atomic_typ_ocaml = - (* following the structure of parser for precedence *) - let rec typ ty = fn_typ ty - and fn_typ ((Typ_aux (t, _)) as ty) = match t with - | Typ_fn(arg,ret,efct) -> - separate space [tup_typ arg; arrow; fn_typ ret] - | _ -> tup_typ ty - and tup_typ ((Typ_aux (t, _)) as ty) = match t with - | Typ_tup typs -> parens (separate_map star app_typ typs) - | _ -> app_typ ty - and app_typ ((Typ_aux (t, _)) as ty) = match t with - | Typ_app(Id_aux (Id "vector", _), [ - Typ_arg_aux(Typ_arg_nexp n, _); - Typ_arg_aux(Typ_arg_nexp m, _); - Typ_arg_aux (Typ_arg_order ord, _); - Typ_arg_aux (Typ_arg_typ typ, _)]) -> - string "value" - | Typ_app(Id_aux (Id "range", _), [ - Typ_arg_aux(Typ_arg_nexp n, _); - Typ_arg_aux(Typ_arg_nexp m, _);]) -> - (string "number") - | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) -> - (string "number") - | Typ_app(id,args) -> - (separate_map space doc_typ_arg_ocaml args) ^^ space ^^ (doc_id_ocaml_type id) - | _ -> atomic_typ ty - and atomic_typ ((Typ_aux (t, _)) as ty) = match t with - | Typ_id id -> doc_id_ocaml_type id - | Typ_var v -> doc_var v - | Typ_app _ | Typ_tup _ | Typ_fn _ -> - (* exhaustiveness matters here to avoid infinite loops - * if we add a new Typ constructor *) - group (parens (typ ty)) - and doc_typ_arg_ocaml (Typ_arg_aux(t,_)) = match t with - | Typ_arg_typ t -> app_typ t - | Typ_arg_nexp n -> empty - | Typ_arg_order o -> empty - in typ, atomic_typ - -let doc_lit_ocaml in_pat (L_aux(l,_)) = - utf8string (match l with - | L_unit -> "()" - | L_zero -> "Vzero" - | L_one -> "Vone" - | L_true -> "Vone" - | L_false -> "Vzero" - | L_num i -> - let s = string_of_int i in - if (i >= 0) && (i <= 257) then - "bi" ^ s - else - "(big_int_of_int (" ^ s ^ "))" - | L_hex n -> "(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*) - | L_bin n -> "(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*) - | L_undef -> "(failwith \"undef literal not supported\")" (* XXX Undef vectors get handled with to_vec_undef. We could support undef bit but would need to check type. For the moment treat as runtime error. *) - | L_string s -> "\"" ^ s ^ "\"" - | L_real s -> s) - -(* typ_doc is the doc for the type being quantified *) -let doc_typquant_ocaml (TypQ_aux(tq,_)) typ_doc = typ_doc - -let doc_typscm_ocaml (TypSchm_aux(TypSchm_ts(tq,t),_)) = - (doc_typquant_ocaml tq (doc_typ_ocaml t)) - -(*Note: vector concatenation, literal vectors, indexed vectors, and record should - be removed prior to pp. The latter two have never yet been seen -*) -let doc_pat_ocaml = - let rec pat pa = app_pat pa - and app_pat ((P_aux(p,(l,annot))) as pa) = match p with - | P_app(id, ((_ :: _) as pats)) -> - (* TODO This check fails for some reason in the MIPS execute function; - lookup_id returns Unbound, maybe because the environment is not - propagated correctly during rewriting. - I comment out the check for now. *) - (* (match annot with - | Some (env, typ, eff) -> - (match Env.lookup_id id env with - | Union _ -> *) - doc_unop (doc_id_ocaml_ctor id) (parens (separate_map comma_sp pat pats)) - (* | _ -> empty) - | _ -> empty) *) - | P_lit lit -> doc_lit_ocaml true lit - | P_wild -> underscore - | P_id id -> doc_id_ocaml id - | P_as(p,id) -> parens (separate space [pat p; string "as"; doc_id_ocaml id]) - | P_typ(typ,p) -> parens (doc_op colon (pat p) (doc_typ_ocaml typ)) - | P_app(id,[]) -> - (match annot with - | Some (env, typ, eff) -> - (match Env.lookup_id id env with - | Union _ | Enum _ -> doc_id_ocaml_ctor id - | _ -> failwith "encountered unexpected P_app pattern") - | _ -> failwith "encountered unexpected P_app pattern") - | P_vector pats -> - let non_bit_print () = - parens - (separate space [string "VvectorR"; - parens (separate comma_sp [squarebars (separate_map semi pat pats); - underscore; - underscore])]) in - (match annot with - | Some (env, typ, _) -> - if is_bitvector_typ (Env.base_typ_of env typ) - then parens (separate space [string "Vvector"; - parens (separate comma_sp [squarebars (separate_map semi pat pats); - underscore; - underscore])]) - else non_bit_print() - | None -> non_bit_print()) - | P_tup pats -> parens (separate_map comma_sp pat pats) - | P_list pats -> brackets (separate_map semi pat pats) (*Never seen but easy in ocaml*) - | P_cons (p,p') -> doc_op (string "::") (pat p) (pat p') - | P_record _ -> raise (Reporting_basic.err_unreachable l "unhandled record pattern") - | P_vector_concat _ -> raise (Reporting_basic.err_unreachable l "unhandled vector_concat pattern") - in pat - -let id_is_local_var id env = match Env.lookup_id id env with - | Local _ | Unbound -> true - | _ -> false - -let rec lexp_is_local (LEXP_aux (lexp, _)) env = match lexp with - | LEXP_memory _ -> false - | LEXP_id id - | LEXP_cast (_, id) -> id_is_local_var id env - | LEXP_tup lexps -> List.for_all (fun lexp -> lexp_is_local lexp env) lexps - | LEXP_vector (lexp,_) - | LEXP_vector_range (lexp,_,_) - | LEXP_field (lexp,_) -> lexp_is_local lexp env - -let is_regtyp (Typ_aux (typ,_)) env = match typ with - | Typ_app (register, _) -> string_of_id register = "register" - | Typ_id id -> Env.is_regtyp id env - | _ -> false - -let doc_exp_ocaml, doc_let_ocaml = - let rec top_exp read_registers (E_aux (e, (l,annot)) as full_exp) = - let exp = top_exp read_registers in - let (env, typ, eff) = match annot with - | Some (env, typ, eff) -> (env, typ, eff) - | None -> raise (Reporting_basic.err_unreachable l "no type annotation") in - match e with - | E_assign((LEXP_aux(le_act,tannot) as le),e) -> - if lexp_is_local le env - then - (match le_act with - | LEXP_id _ | LEXP_cast _ -> - (*Setting local variable fully *) - doc_op coloneq (doc_lexp_ocaml true le) (exp e) - | LEXP_vector _ -> - doc_op (string "<-") (doc_lexp_array_ocaml le) (exp e) - | LEXP_vector_range _ | LEXP_field _ -> - doc_lexp_rwrite le e) - else - (match le_act with - | LEXP_vector _ | LEXP_vector_range _ | LEXP_cast _ | LEXP_field _ | LEXP_id _ -> - (doc_lexp_rwrite le e) - | LEXP_memory _ -> (doc_lexp_fcall le e)) - | E_vector_append(l,r) -> - parens ((string "vector_concat ") ^^ (exp l) ^^ space ^^ (exp r)) - | E_cons(l,r) -> doc_op (group (colon^^colon)) (exp l) (exp r) - | E_if(c,t,E_aux(E_block [], _)) -> - parens (string "if" ^^ space ^^ string "to_bool" ^^ parens (exp c) ^/^ - string "then" ^^ space ^^ (exp t)) - | E_if(c,t,e) -> - parens ( - string "if" ^^ space ^^ string "to_bool" ^^ parens (exp c) ^/^ - string "then" ^^ space ^^ group (exp t) ^/^ - string "else" ^^ space ^^ group (exp e)) - | E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) -> - let var= doc_id_ocaml id in - let (compare,next) = if order = Ord_inc then string "le_big_int",string "add_big_int" else string "ge_big_int",string "sub_big_int" in - let by = exp exp3 in - let stop = exp exp2 in - (*takes over two names but doesn't require building a closure*) - parens - (separate space [(string "let (__stop,__by) = ") ^^ (parens (doc_op comma stop by)); - string "in" ^/^ empty; - string "let rec foreach"; - var; - equals; - string "if"; - parens (compare ^^ space ^^ var ^^ space ^^ (string "__stop") ); - string "then"; - parens (exp exp4 ^^ space ^^ semi ^^ (string "foreach") ^^ - parens (next ^^ space ^^ var ^^ space ^^ (string "__by"))); - string "in"; - string "foreach"; - exp exp1]) - (*Requires fewer introduced names but introduces a closure*) - (*let forL = if order = Ord_inc then string "foreach_inc" else string "foreach_dec" in - forL ^^ space ^^ (group (exp exp1)) ^^ (group (exp exp2)) ^^ (group (exp full_exp3)) ^/^ - group ((string "fun") ^^ space ^^ (doc_id id) ^^ space ^^ arrow ^/^ (exp exp4)) - - (* this way requires the following OCaml declarations first - - let rec foreach_inc i stop by body = - if i <= stop then (body i; foreach_inc (i + by) stop by body) else () - - let rec foreach_dec i stop by body = - if i >= stop then (body i; foreach_dec (i - by) stop by body) else () - - *)*) - | E_let(leb,e) -> doc_op (string "in") (let_exp leb) (exp e) - | E_app(f,args) -> - let call,ctor = match Env.lookup_id f env with - | Union _ -> doc_id_ocaml_ctor f,true - | _ -> doc_id_ocaml f,false in - let base_print () = parens (doc_unop call (parens (separate_map comma exp args))) in - if not(ctor) - then base_print () - else (match args with - | [] -> call - | [arg] -> (match arg with - | E_aux(E_lit (L_aux(L_unit,_)),_) -> call - | _ -> base_print()) - | args -> base_print()) - | E_vector_access(v,e) -> - let call = - if is_bit_typ (Env.base_typ_of env typ) - then (string "bit_vector_access") - else (string "vector_access") in - parens (call ^^ space ^^ exp v ^^ space ^^ exp e) - | E_vector_subrange(v,e1,e2) -> - parens ((string "vector_subrange") ^^ space ^^ (exp v) ^^ space ^^ (exp e1) ^^ space ^^ (exp e2)) - | E_field((E_aux(_,(fl,fannot)) as fexp),id) -> - let ftyp = typ_of_annot (fl,fannot) in - if (is_regtyp ftyp env) then - let field_f = - if (is_bit_typ (Env.base_typ_of env ftyp)) - then string "get_register_field_bit" - else string "get_register_field_vec" in - parens (field_f ^^ space ^^ (exp fexp) ^^ space ^^ string_lit (doc_id id)) - else exp fexp ^^ dot ^^ doc_id_ocaml id - | E_block [] -> string "()" - | E_block exps | E_nondet exps -> - let exps_doc = separate_map (semi ^^ hardline) exp exps in - surround 2 1 (string "begin") exps_doc (string "end") - | E_id id -> - (match Env.lookup_id id env with - | Local (Mutable, _) -> - string "!" ^^ doc_id_ocaml id - | Union _ | Enum _ -> doc_id_ocaml_ctor id - | _ -> - if (is_regtyp typ env) then - if read_registers - then string "(read_register " ^^ doc_id_ocaml id ^^ string ")" - else doc_id_ocaml id - else doc_id_ocaml id) - (*match annot with - | Base((_,t),Alias alias_info,_,_,_,_) -> - (match alias_info with - | Alias_field(reg,field) -> - let field_f = match t.t with - | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> string "get_register_field_bit" - | _ -> string "get_register_field_vec" in - parens (separate space [field_f; string (sanitize_name reg); string_lit (string field)]) - | Alias_extract(reg,start,stop) -> - if start = stop - then parens (separate space [string "bit_vector_access";string (sanitize_name reg);doc_int start]) - else parens - (separate space [string "vector_subrange"; string (sanitize_name reg); doc_int start; doc_int stop]) - | Alias_pair(reg1,reg2) -> - parens (separate space [string "vector_concat"; - string (sanitize_name reg1); - string (sanitize_name reg2)])) *) - | E_lit lit -> doc_lit_ocaml false lit - | E_cast(typ,e) -> - (* (match annot with - | Base(_,External _,_,_,_,_) -> - if read_registers - then parens (string "read_register" ^^ space ^^ exp e) - else exp e - | _ -> *) - let (Typ_aux (t,_)) = typ in - (match t with - | Typ_app (Id_aux (Id "vector",_), [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i,_)),_);_;_;_]) -> - parens ((concat [string "set_start";space;string (string_of_int i)]) ^//^ - exp e) - | Typ_var (Kid_aux (Var "length",_)) -> - parens ((string "set_start_to_length") ^//^ exp 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,_),_)) -> - braces (separate_map semi_sp doc_fexp fexps) - | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) -> - braces (doc_op (string "with") (exp e) (separate_map semi_sp doc_fexp fexps)) - | E_vector exps -> - let (start, _, order, _) = vector_typ_args_of (Env.base_typ_of env typ) in - (*match annot with - | Base((_,t),_,_,_,_,_) -> - match t.t with - | Tapp("vector", [TA_nexp start; _; TA_ord order; _]) - | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; _; TA_ord order; _])}) ->*) - let call = if is_bitvector_typ typ then (string "Vvector") else (string "VvectorR") in - let dir,dir_out = if is_order_inc order then (true,"true") else (false, "false") in - let start = match start with - | Nexp_aux (Nexp_constant i, _) -> string_of_int i - | Nexp_aux (Nexp_exp (Nexp_aux (Nexp_constant i, _)), _) -> - string_of_int (Util.power 2 i) - | _ -> if dir then "0" else string_of_int (List.length exps) in - parens (separate space [call; parens (separate comma_sp [squarebars (separate_map semi exp exps); - string start; - string dir_out])]) - | E_vector_update(v,e1,e2) -> - (*Has never happened to date*) - brackets (doc_op (string "with") (exp v) (doc_op equals (exp e1) (exp e2))) - | E_vector_update_subrange(v,e1,e2,e3) -> - (*Has never happened to date*) - brackets ( - doc_op (string "with") (exp v) - (doc_op equals (exp e1 ^^ colon ^^ exp e2) (exp e3))) - | E_list exps -> - brackets (separate_map semi exp exps) - | E_case(e,pexps) -> - let opening = separate space [string "("; string "match"; top_exp false e; string "with"] in - let cases = separate_map (break 1) doc_case pexps in - surround 2 1 opening cases rparen - | E_exit e -> - separate space [string "exit"; exp e;] - | E_return e -> - separate space [string "begin ret := Some" ; exp e ; string "; raise Sail_return; end"] - | E_app_infix (e1,id,e2) -> - let call = - (* match annot with - | Base((_,t),External(Some name),_,_,_,_) -> string name - | _ -> *) doc_id_ocaml id in - parens (separate space [call; parens (separate_map comma exp [e1;e2])]) - | E_internal_let(lexp, eq_exp, in_exp) -> - separate space [string "let"; - doc_lexp_ocaml true lexp; (*Rewriter/typecheck should ensure this is only cast or id*) - equals; - string "ref"; - exp eq_exp; - string "in"; - exp in_exp] - - | E_internal_plet (pat,e1,e2) -> - (separate space [(exp e1); string ">>= fun"; doc_pat_ocaml pat;arrow]) ^/^ - exp e2 - - | E_internal_return (e1) -> - separate space [string "return"; exp e1;] - | E_assert (e1, e2) -> - (string "assert") ^^ parens ((string "to_bool") ^^ space ^^ exp e1) (* XXX drops e2 *) - | E_sizeof _ -> raise (Reporting_basic.err_unreachable l - "E_sizeof should have been rewritten before pretty-printing") - | E_constraint _ -> empty - | E_sizeof_internal _ | E_internal_exp_user (_, _) | E_internal_cast (_, _) - | E_internal_exp _ -> raise (Reporting_basic.err_unreachable l - "internal expression should have been rewritten before pretty-printing") - | E_comment _ | E_comment_struc _ -> empty (* TODO Should we output comments? *) - and let_exp (LB_aux(lb,_)) = match lb with - | LB_val(pat,e) -> - prefix 2 1 - (separate space [string "let"; doc_pat_ocaml pat; equals]) - (top_exp false e) - - and doc_fexp (FE_aux(FE_Fexp(id,e),_)) = doc_op equals (doc_id_ocaml id) (top_exp false e) - - and doc_case = function - | (Pat_aux(Pat_exp(pat,e),_)) -> - doc_op arrow (separate space [pipe; doc_pat_ocaml pat]) (group (top_exp false e)) - | (Pat_aux(Pat_when(pat,guard,e),_)) -> - doc_op arrow - (separate space [pipe; - doc_op (string "when") (doc_pat_ocaml pat) (top_exp false guard)]) - (group (top_exp false e)) - - and doc_lexp_ocaml top_call ((LEXP_aux(lexp,(l,annot))) as le) = - let exp = top_exp false in - match lexp with - | LEXP_vector(v,e) -> doc_lexp_array_ocaml le - | LEXP_vector_range(v,e1,e2) -> - parens ((string "vector_subrange") ^^ space ^^ (doc_lexp_ocaml false v) ^^ space ^^ (exp e1) ^^ space ^^ (exp e2)) - | LEXP_field(v,id) -> (doc_lexp_ocaml false v) ^^ dot ^^ doc_id_ocaml id - | LEXP_id id | LEXP_cast(_,id) -> - let name = doc_id_ocaml id in - match annot,top_call with - | Some (env, _, _), false -> - (match Env.lookup_id id env with - | Local (Mutable, _) -> string "!" ^^ name - | _ -> name) - | _ -> name - - and doc_lexp_array_ocaml ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with - | LEXP_vector(v,e) -> - (match annot with - | Some (env, t, _) -> - if (is_bit_typ (Env.base_typ_of env t)) - then parens ((string "get_barray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (top_exp false e)) - else parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (top_exp false e)) - | _ -> - parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (top_exp false e))) - | _ -> empty - - and doc_lexp_rwrite ((LEXP_aux(lexp,(l,annot))) as le) e_new_v = - let exp = top_exp false in - let (is_bit,is_bitv) = match annot with - | Some (env, typ, _) -> - let typ = Env.base_typ_of env typ in - (is_bit_typ typ, is_bitvector_typ typ) - | _ -> (false, false) in - match lexp with - | LEXP_vector(v,e) -> - if is_bit then (* XXX check whether register or not?? *) - parens ((string "set_register_bit" ^^ space ^^ doc_lexp_ocaml false v ^^ space ^^ exp e ^^ space ^^ exp e_new_v)) - else (* XXX Check whether vector of reg? XXX Does not work for decreasing vector. *) - parens ((string "set_register") ^^ space ^^ - ((group (parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml false v)) ^^ - dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (exp e))) ^^ space ^^ (exp e_new_v))) - | LEXP_vector_range(v,e1,e2) -> - parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_vec")) ^^ space ^^ - doc_lexp_ocaml false v ^^ space ^^ exp e1 ^^ space ^^ exp e2 ^^ space ^^ exp e_new_v) - | LEXP_field(v,id) -> - parens ((string (if is_bit then "set_register_field_bit" else "set_register_field_v")) ^^ space ^^ - doc_lexp_ocaml false v ^^ space ^^string_lit (doc_id id) ^^ space ^^ exp e_new_v) - | LEXP_id id | LEXP_cast (_,id) -> - (* (match annot with - | Base(_,Alias alias_info,_,_,_,_) -> - (match alias_info with - | Alias_field(reg,field) -> - parens ((if is_bit then string "set_register_field_bit" else string "set_register_field_v") ^^ space ^^ - string (sanitize_name reg) ^^ space ^^string_lit (string field) ^^ space ^^ exp e_new_v) - | Alias_extract(reg,start,stop) -> - if start = stop - then - doc_op (string "<-") - (group (parens ((string (if is_bit then "get_barray" else "get_varray")) ^^ space ^^ string reg)) ^^ - dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (doc_int start))) - (exp e_new_v) - else - parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_vec")) ^^ space ^^ - 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 (separate space [string "set_register"; 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 (top_exp false) (args@[e_new_v])) - - (* expose doc_exp and doc_let *) - in top_exp false, let_exp - -(*TODO Upcase and downcase type and constructors as needed*) -let doc_type_union_ocaml n (Tu_aux(typ_u,_)) = match typ_u with - | Tu_ty_id(typ,id) -> separate space [pipe; doc_id_ocaml_ctor id; string "of"; doc_typ_ocaml typ;] - | Tu_id id -> separate space [pipe; doc_id_ocaml_ctor id] - -let rec doc_range_ocaml (BF_aux(r,_)) = match r with - | BF_single i -> parens (doc_op comma (doc_int i) (doc_int i)) - | BF_range(i1,i2) -> parens (doc_op comma (doc_int i1) (doc_int i2)) - | BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2) - -let doc_typdef_ocaml (TD_aux(td,_)) = match td with - | TD_abbrev(id,nm,typschm) -> - doc_op equals (concat [string "type"; space; doc_id_ocaml_type id;]) (doc_typscm_ocaml typschm) - | TD_record(id,nm,typq,fs,_) -> - let f_pp (typ,id) = concat [doc_id_ocaml_type id; space; colon; doc_typ_ocaml typ; semi] in - let fs_doc = group (separate_map (break 1) f_pp fs) in - doc_op equals - (concat [string "type"; space; doc_id_ocaml_type id;]) (doc_typquant_ocaml typq (braces fs_doc)) - | TD_variant(id,nm,typq,ar,_) -> - let n = List.length ar in - let ar_doc = group (separate_map (break 1) (doc_type_union_ocaml n) ar) in - doc_op equals - (concat [string "type"; space; doc_id_ocaml_type id;]) - (if n > 246 - then brackets (space ^^(doc_typquant_ocaml typq ar_doc)) - else (doc_typquant_ocaml typq ar_doc)) - | TD_enum(id,nm,enums,_) -> - let n = List.length enums in - let enums_doc = group (separate_map (break 1 ^^ pipe) (doc_id_ocaml_ctor) enums) in - doc_op equals - (concat [string "type"; space; doc_id_ocaml_type id;]) - (enums_doc) - | TD_register(id,n1,n2,rs) -> - let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id id); doc_range_ocaml r;]) in - let doc_rids = group (separate_map (semi ^^ (break 1)) doc_rid rs) in - 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 - [parens (separate space - [string "match init_val with"; - pipe; - string "None"; - arrow; - string "ref"; - string "(Array.make"; - doc_int size; - string "Vzero)"; - pipe; - string "Some init_val"; - arrow; - string "ref init_val";]); - doc_nexp n1; - string (if dir then "true" else "false"); - string_lit (doc_id id); - brackets doc_rids]))]) - -let doc_kdef_ocaml (KD_aux(kd,_)) = match kd with - | KD_nabbrev (k, id, name_scm, nexp) -> - separate space [string "let" ; - doc_id_ocaml id; - equals; - doc_nexp nexp] - -let doc_rec_ocaml (Rec_aux(r,_)) = match r with - | Rec_nonrec -> empty - | Rec_rec -> string "rec" ^^ space - -let doc_tannot_opt_ocaml (Typ_annot_opt_aux(t,_)) = match t with - | Typ_annot_opt_some(tq,typ) -> doc_typquant_ocaml tq (doc_typ_ocaml typ) - -let doc_funcl_exp_ocaml (E_aux (e, (l, annot)) as ea) = match annot with - | Some (_, t, efctsum) -> - (* | Base((_,t),tag,nes,efct,efctsum,_) -> *) - if has_effect efctsum BE_lret then - separate hardline [string "let ret = ref None in"; - string "try"; - (doc_exp_ocaml ea); - string "with Sail_return -> match(!ret) with"; - string "| Some(x) -> x"; - string "| None -> failwith \"ret unset\"" - ] - else - doc_exp_ocaml ea - | _ -> doc_exp_ocaml ea - -let doc_funcl_ocaml (FCL_aux(FCL_Funcl(id,pat,exp),_)) = - group (doc_op arrow (doc_pat_ocaml pat) (doc_funcl_exp_ocaml exp)) - -let get_id = function - | [] -> failwith "FD_function with empty list" - | (FCL_aux (FCL_Funcl (id,_,_),_))::_ -> id - -let doc_fundef_ocaml (FD_aux(FD_function(r, typa, efa, fcls),_)) = - match fcls with - | [] -> failwith "FD_function with empty function list" - | [FCL_aux (FCL_Funcl(id,pat,exp),_)] -> - (separate space [(string "let"); (doc_rec_ocaml r); (doc_id_ocaml id); (doc_pat_ocaml pat); equals]) ^^ hardline ^^ (doc_funcl_exp_ocaml exp) - | _ -> - let id = get_id fcls in - let sep = hardline ^^ pipe ^^ space in - let clauses = separate_map sep doc_funcl_ocaml fcls in - separate space [string "let"; - doc_rec_ocaml r; - doc_id_ocaml id; - equals; - (string "function"); - (hardline^^pipe); - clauses] - -let doc_dec_ocaml (DEC_aux (reg,(l,annot))) = - match reg with - | DEC_reg(typ,id) -> - if is_vector_typ typ then - let (start, size, order, itemt) = vector_typ_args_of typ in - if is_bit_typ itemt && is_nexp_constant start && is_nexp_constant size then - let o = if is_order_inc order then string "true" else string "false" in - separate space [string "let"; - doc_id_ocaml id; - equals; - string "Vregister"; - parens (separate comma [separate space [string "ref"; - parens (separate space - [string "Array.make"; - doc_nexp size; - string "Vzero";])]; - doc_nexp start; - o; - string_lit (doc_id id); - brackets empty])] - else raise (Reporting_basic.err_unreachable l - ("can't deal with register type " ^ string_of_typ typ)) - else - (match typ with - | Typ_aux (Typ_id idt, _) -> - (* | Tapp("register", [TA_typ {t=Tid idt}]) | - Tabbrev( {t= Tid idt}, _) -> *) - separate space [string "let"; - doc_id_ocaml id; - equals; - doc_id_ocaml idt; - string "None"] - |_-> raise (Reporting_basic.err_unreachable l - ("can't deal with register type " ^ string_of_typ typ))) - (* | _ -> failwith "annot was not Base") *) - | DEC_alias(id,alspec) -> empty (* - doc_op equals (string "register alias" ^^ space ^^ doc_id id) (doc_alias alspec) *) - | DEC_typ_alias(typ,id,alspec) -> empty (* - 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 - | DEF_spec v_spec -> empty (*unless we want to have a separate pass to create mli files*) - | 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 -> doc_dec_ocaml dec - | DEF_scattered sdef -> empty (*shoulnd't still be here*) - | DEF_kind k_def -> doc_kdef_ocaml k_def - | DEF_overload _ -> empty - | DEF_comm _ -> failwith "unhandled DEF_comm" - ) ^^ hardline - -let doc_defs_ocaml (Defs(defs)) = - separate_map hardline doc_def_ocaml defs -let pp_defs_ocaml f d top_line opens = - print f (string "(*" ^^ (string top_line) ^^ string "*)" ^/^ - (separate_map hardline (fun lib -> (string "open") ^^ space ^^ (string lib)) opens) ^/^ - (doc_defs_ocaml d)) |