(**************************************************************************) (* 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 Type_internal open Ast open Format open Big_int (**************************************************************************** * annotated source to Lem ast pretty printer ****************************************************************************) let print_to_from_interp_value = ref false let rec list_format (sep : string) (fmt : 'a -> string) (ls : 'a list) : string = match ls with | [] -> "" | [a] -> fmt a | a::ls -> (fmt a) ^ sep ^ (list_format sep fmt ls) let rec list_pp i_format l_format = fun ppf l -> match l with | [] -> fprintf ppf "" | [i] -> fprintf ppf "%a" l_format i | i::is -> fprintf ppf "%a%a" i_format i (list_pp i_format l_format) is let kwd ppf s = fprintf ppf "%s" s let base ppf s = fprintf ppf "%s" s let lemnum default n = match n with | 0 -> "zero" | 1 -> "one" | 2 -> "two" | 3 -> "three" | 4 -> "four" | 5 -> "five" | 6 -> "six" | 7 -> "seven" | 8 -> "eight" | 15 -> "fifteen" | 16 -> "sixteen" | 20 -> "twenty" | 23 -> "twentythree" | 24 -> "twentyfour" | 30 -> "thirty" | 31 -> "thirtyone" | 32 -> "thirtytwo" | 35 -> "thirtyfive" | 39 -> "thirtynine" | 40 -> "forty" | 47 -> "fortyseven" | 48 -> "fortyeight" | 55 -> "fiftyfive" | 56 -> "fiftysix" | 57 -> "fiftyseven" | 61 -> "sixtyone" | 63 -> "sixtythree" | 64 -> "sixtyfour" | 127 -> "onetwentyseven" | 128 -> "onetwentyeight" | _ -> if n >= 0 then default n else ("(zero - " ^ (default (abs n)) ^ ")") let pp_format_id (Id_aux(i,_)) = match i with | Id(i) -> i | DeIid(x) -> "(deinfix " ^ x ^ ")" let pp_format_var (Kid_aux(Var v,_)) = v let rec pp_format_l_lem = function | Parse_ast.Unknown -> "Unknown" | _ -> "Unknown"(* | Parse_ast.Int(s,None) -> "(Int \"" ^ s ^ "\" Nothing)" | Parse_ast.Int(s,(Some l)) -> "(Int \"" ^ s ^ "\" (Just " ^ (pp_format_l_lem l) ^ "))" | Parse_ast.Range(p1,p2) -> "(Range \"" ^ p1.Lexing.pos_fname ^ "\" " ^ (string_of_int p1.Lexing.pos_lnum) ^ " " ^ (string_of_int (p1.Lexing.pos_cnum - p1.Lexing.pos_bol)) ^ " " ^ (string_of_int p2.Lexing.pos_lnum) ^ " " ^ (string_of_int (p2.Lexing.pos_cnum - p2.Lexing.pos_bol)) ^ ")" | Parse_ast.Generated l -> "(Generated " ^ (pp_format_l_lem l) ^ ")" | _ -> "Unknown"*) let pp_lem_l ppf l = base ppf (pp_format_l_lem l) let pp_format_id_lem (Id_aux(i,l)) = "(Id_aux " ^ (match i with | Id(i) -> "(Id \"" ^ i ^ "\")" | DeIid(x) -> "(DeIid \"" ^ x ^ "\")") ^ " " ^ (pp_format_l_lem l) ^ ")" let pp_lem_id ppf id = base ppf (pp_format_id_lem id) let pp_format_var_lem (Kid_aux(Var v,l)) = "(Kid_aux (Var \"" ^ v ^ "\") " ^ (pp_format_l_lem l) ^ ")" let pp_lem_var ppf var = base ppf (pp_format_var_lem var) let pp_format_bkind_lem (BK_aux(k,l)) = "(BK_aux " ^ (match k with | BK_type -> "BK_type" | BK_nat -> "BK_nat" | BK_order -> "BK_order" | BK_effect -> "BK_effect") ^ " " ^ (pp_format_l_lem l) ^ ")" let pp_lem_bkind ppf bk = base ppf (pp_format_bkind_lem bk) let pp_format_kind_lem (K_aux(K_kind(klst),l)) = "(K_aux (K_kind [" ^ list_format "; " pp_format_bkind_lem klst ^ "]) " ^ (pp_format_l_lem l) ^ ")" let pp_lem_kind ppf k = base ppf (pp_format_kind_lem k) let rec pp_format_typ_lem (Typ_aux(t,l)) = "(Typ_aux " ^ (match t with | Typ_id(id) -> "(Typ_id " ^ pp_format_id_lem id ^ ")" | Typ_var(var) -> "(Typ_var " ^ pp_format_var_lem var ^ ")" | Typ_fn(arg,ret,efct) -> "(Typ_fn " ^ pp_format_typ_lem arg ^ " " ^ pp_format_typ_lem ret ^ " " ^ (pp_format_effects_lem efct) ^ ")" | Typ_tup(typs) -> "(Typ_tup [" ^ (list_format "; " pp_format_typ_lem typs) ^ "])" | Typ_app(id,args) -> "(Typ_app " ^ (pp_format_id_lem id) ^ " [" ^ (list_format "; " pp_format_typ_arg_lem args) ^ "])" | Typ_wild -> "Typ_wild") ^ " " ^ (pp_format_l_lem l) ^ ")" and pp_format_nexp_lem (Nexp_aux(n,l)) = "(Nexp_aux " ^ (match n with | Nexp_id(i) -> "(Nexp_id " ^ pp_format_id_lem i ^ ")" | Nexp_var(v) -> "(Nexp_var " ^ pp_format_var_lem v ^ ")" | Nexp_constant(i) -> "(Nexp_constant " ^ (lemnum string_of_int i) ^ ")" | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")" | Nexp_minus(n1,n2) -> "(Nexp_minus " ^ (pp_format_nexp_lem n1)^ " " ^ (pp_format_nexp_lem n2) ^ ")" | Nexp_times(n1,n2) -> "(Nexp_times " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")" | Nexp_exp(n1) -> "(Nexp_exp " ^ (pp_format_nexp_lem n1) ^ ")" | Nexp_neg(n1) -> "(Nexp_neg " ^ (pp_format_nexp_lem n1) ^ ")") ^ " " ^ (pp_format_l_lem l) ^ ")" and pp_format_ord_lem (Ord_aux(o,l)) = "(Ord_aux " ^ (match o with | Ord_var(v) -> "(Ord_var " ^ pp_format_var_lem v ^ ")" | Ord_inc -> "Ord_inc" | Ord_dec -> "Ord_dec") ^ " " ^ (pp_format_l_lem l) ^ ")" and pp_format_base_effect_lem (BE_aux(e,l)) = "(BE_aux " ^ (match e with | BE_rreg -> "BE_rreg" | BE_wreg -> "BE_wreg" | BE_rmem -> "BE_rmem" | BE_wmem -> "BE_wmem" | BE_wmv -> "BE_wmv" | BE_eamem -> "BE_eamem" | BE_barr -> "BE_barr" | BE_depend -> "BE_depend" | BE_undef -> "BE_undef" | BE_unspec -> "BE_unspec" | BE_nondet -> "BE_nondet" | BE_lset -> "BE_lset" | BE_lret -> "BE_lret" | BE_escape -> "BE_escape") ^ " " ^ (pp_format_l_lem l) ^ ")" and pp_format_effects_lem (Effect_aux(e,l)) = "(Effect_aux " ^ (match e with | Effect_var(v) -> "(Effect_var " ^ pp_format_var v ^ ")" | Effect_set(efcts) -> "(Effect_set [" ^ (list_format "; " pp_format_base_effect_lem efcts) ^ " ])") ^ " " ^ (pp_format_l_lem l) ^ ")" and pp_format_typ_arg_lem (Typ_arg_aux(t,l)) = "(Typ_arg_aux " ^ (match t with | Typ_arg_typ(t) -> "(Typ_arg_typ " ^ pp_format_typ_lem t ^ ")" | Typ_arg_nexp(n) -> "(Typ_arg_nexp " ^ pp_format_nexp_lem n ^ ")" | Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")" | Typ_arg_effect(e) -> "(Typ_arg_effect " ^ pp_format_effects_lem e ^ ")") ^ " " ^ (pp_format_l_lem l) ^ ")" let pp_lem_typ ppf t = base ppf (pp_format_typ_lem t) let pp_lem_nexp ppf n = base ppf (pp_format_nexp_lem n) let pp_lem_ord ppf o = base ppf (pp_format_ord_lem o) let pp_lem_effects ppf e = base ppf (pp_format_effects_lem e) let pp_lem_beffect ppf be = base ppf (pp_format_base_effect_lem be) let pp_format_nexp_constraint_lem (NC_aux(nc,l)) = "(NC_aux " ^ (match nc with | NC_fixed(n1,n2) -> "(NC_fixed " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")" | NC_bounded_ge(n1,n2) -> "(NC_bounded_ge " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")" | NC_bounded_le(n1,n2) -> "(NC_bounded_le " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")" | NC_nat_set_bounded(id,bounds) -> "(NC_nat_set_bounded " ^ pp_format_var_lem id ^ " [" ^ list_format "; " string_of_int bounds ^ "])") ^ " " ^ (pp_format_l_lem l) ^ ")" let pp_lem_nexp_constraint ppf nc = base ppf (pp_format_nexp_constraint_lem nc) let pp_format_qi_lem (QI_aux(qi,lq)) = "(QI_aux " ^ (match qi with | QI_const(n_const) -> "(QI_const " ^ pp_format_nexp_constraint_lem n_const ^ ")" | QI_id(KOpt_aux(ki,lk)) -> "(QI_id (KOpt_aux " ^ (match ki with | KOpt_none(var) -> "(KOpt_none " ^ pp_format_var_lem var ^ ")" | KOpt_kind(k,var) -> "(KOpt_kind " ^ pp_format_kind_lem k ^ " " ^ pp_format_var_lem var ^ ")") ^ " " ^ (pp_format_l_lem lk) ^ "))") ^ " " ^ (pp_format_l_lem lq) ^ ")" let pp_lem_qi ppf qi = base ppf (pp_format_qi_lem qi) let pp_format_typquant_lem (TypQ_aux(tq,l)) = "(TypQ_aux " ^ (match tq with | TypQ_no_forall -> "TypQ_no_forall" | TypQ_tq(qlist) -> "(TypQ_tq [" ^ (list_format "; " pp_format_qi_lem qlist) ^ "])") ^ " " ^ (pp_format_l_lem l) ^ ")" let pp_lem_typquant ppf tq = base ppf (pp_format_typquant_lem tq) let pp_format_typscm_lem (TypSchm_aux(TypSchm_ts(tq,t),l)) = "(TypSchm_aux (TypSchm_ts " ^ (pp_format_typquant_lem tq) ^ " " ^ pp_format_typ_lem t ^ ") " ^ (pp_format_l_lem l) ^ ")" let pp_lem_typscm ppf ts = base ppf (pp_format_typscm_lem ts) let pp_format_lit_lem (L_aux(lit,l)) = "(L_aux " ^ (match lit with | L_unit -> "L_unit" | L_zero -> "L_zero" | L_one -> "L_one" | L_true -> "L_true" | L_false -> "L_false" | L_num(i) -> "(L_num " ^ (lemnum string_of_int i) ^ ")" | L_hex(n) -> "(L_hex \"" ^ n ^ "\")" | L_bin(n) -> "(L_bin \"" ^ n ^ "\")" | L_undef -> "L_undef" | L_string(s) -> "(L_string \"" ^ s ^ "\")") ^ " " ^ (pp_format_l_lem l) ^ ")" let pp_lem_lit ppf l = base ppf (pp_format_lit_lem l) let rec pp_format_t_lem t = match t.t with | Tid i -> "(T_id \"" ^ i ^ "\")" | Tvar i -> "(T_var \"" ^ i ^ "\")" | Tfn(t1,t2,_,e) -> "(T_fn " ^ (pp_format_t_lem t1) ^ " " ^ (pp_format_t_lem t2) ^ " " ^ pp_format_e_lem e ^ ")" | Ttup(tups) -> "(T_tup [" ^ (list_format "; " pp_format_t_lem tups) ^ "])" | Tapp(i,args) -> "(T_app \"" ^ i ^ "\" (T_args [" ^ list_format "; " pp_format_targ_lem args ^ "]))" | Tabbrev(ti,ta) -> "(T_abbrev " ^ (pp_format_t_lem ti) ^ " " ^ (pp_format_t_lem ta) ^ ")" | Tuvar(_) -> "(T_var \"fresh_v\")" | Toptions _ -> "(T_var \"fresh_v\")" and pp_format_targ_lem = function | TA_typ t -> "(T_arg_typ " ^ pp_format_t_lem t ^ ")" | TA_nexp n -> "(T_arg_nexp " ^ pp_format_n_lem n ^ ")" | TA_eft e -> "(T_arg_effect " ^ pp_format_e_lem e ^ ")" | TA_ord o -> "(T_arg_order " ^ pp_format_o_lem o ^ ")" and pp_format_n_lem n = match n.nexp with | Nid (i, n) -> "(Ne_id \"" ^ i ^ " " ^ "\")" | Nvar i -> "(Ne_var \"" ^ i ^ "\")" | Nconst i -> "(Ne_const " ^ (lemnum string_of_int (int_of_big_int i)) ^ ")" | Npos_inf -> "Ne_inf" | Nadd(n1,n2) -> "(Ne_add [" ^ (pp_format_n_lem n1) ^ "; " ^ (pp_format_n_lem n2) ^ "])" | Nsub(n1,n2) -> "(Ne_minus "^ (pp_format_n_lem n1) ^ " " ^ (pp_format_n_lem n2) ^ ")" | Nmult(n1,n2) -> "(Ne_mult " ^ (pp_format_n_lem n1) ^ " " ^ (pp_format_n_lem n2) ^ ")" | N2n(n,Some i) -> "(Ne_exp " ^ (pp_format_n_lem n) ^ "(*" ^ string_of_big_int i ^ "*)" ^ ")" | N2n(n,None) -> "(Ne_exp " ^ (pp_format_n_lem n) ^ ")" | Nneg n -> "(Ne_unary " ^ (pp_format_n_lem n) ^ ")" | Nuvar _ -> "(Ne_var \"fresh_v_" ^ string_of_int (get_index n) ^ "\")" | Nneg_inf -> "(Ne_unary Ne_inf)" | Npow _ -> "power_not_implemented" | Ninexact -> "(Ne_add Ne_inf (Ne_unary Ne_inf)" and pp_format_e_lem e = "(Effect_aux " ^ (match e.effect with | Evar i -> "(Effect_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))" | Eset es -> "(Effect_set [" ^ (list_format "; " pp_format_base_effect_lem es) ^ " ])" | Euvar(_) -> "(Effect_var (Kid_aux (Var \"fresh_v\") Unknown))") ^ " Unknown)" and pp_format_o_lem o = "(Ord_aux " ^ (match o.order with | Ovar i -> "(Ord_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))" | Oinc -> "Ord_inc" | Odec -> "Ord_dec" | Ouvar(_) -> "(Ord_var (Kid_aux (Var \"fresh_v\") Unknown))") ^ " Unknown)" let rec pp_format_tag = function | Emp_local -> "Tag_empty" | Emp_intro -> "Tag_intro" | Emp_set -> "Tag_set" | Emp_global -> "Tag_global" | Tuple_assign tags -> (*"(Tag_tuple_assign [" ^ list_format " ;" pp_format_tag tags ^ "])"*) "Tag_tuple_assign" | External (Some s) -> "(Tag_extern (Just \""^s^"\"))" | External None -> "(Tag_extern Nothing)" | Default -> "Tag_default" | Constructor _ -> "Tag_ctor" | Enum i -> "(Tag_enum " ^ (lemnum string_of_int i) ^ ")" | Alias alias_inf -> "Tag_alias" | Spec -> "Tag_spec" let rec pp_format_nes nes = "[" ^ (* (list_format "; " (fun ne -> match ne with | LtEq(_,n1,n2) -> "(Nec_lteq " ^ pp_format_n_lem n1 ^ " " ^ pp_format_n_lem n2 ^ ")" | Eq(_,n1,n2) -> "(Nec_eq " ^ pp_format_n_lem n1 ^ " " ^ pp_format_n_lem n2 ^ ")" | GtEq(_,n1,n2) -> "(Nec_gteq " ^ pp_format_n_lem n1 ^ " " ^ pp_format_n_lem n2 ^ ")" | In(_,i,ns) | InS(_,{nexp=Nvar i},ns) -> "(Nec_in \"" ^ i ^ "\" [" ^ (list_format "; " string_of_int ns)^ "])" | InS(_,_,ns) -> "(Nec_in \"fresh\" [" ^ (list_format "; " string_of_int ns)^ "])" | CondCons(_,nes_c,nes_t) -> "(Nec_cond " ^ (pp_format_nes nes_c) ^ " " ^ (pp_format_nes nes_t) ^ ")" | BranchCons(_,nes_b) -> "(Nec_branch " ^ (pp_format_nes nes_b) ^ ")" ) nes) ^*) "]" let pp_format_annot = function | NoTyp -> "Nothing" | Base((_,t),tag,nes,efct,efctsum,_) -> (*TODO print out bindings for use in pattern match in interpreter*) "(Just (" ^ pp_format_t_lem t ^ ", " ^ pp_format_tag tag ^ ", " ^ pp_format_nes nes ^ ", " ^ pp_format_e_lem efct ^ ", " ^ pp_format_e_lem efctsum ^ "))" | Overload _ -> "Nothing" let pp_annot ppf ant = base ppf (pp_format_annot ant) let rec pp_format_pat_lem (P_aux(p,(l,annot))) = "(P_aux " ^ (match p with | P_lit(lit) -> "(P_lit " ^ pp_format_lit_lem lit ^ ")" | P_wild -> "P_wild" | P_id(id) -> "(P_id " ^ pp_format_id_lem id ^ ")" | P_as(pat,id) -> "(P_as " ^ pp_format_pat_lem pat ^ " " ^ pp_format_id_lem id ^ ")" | P_typ(typ,pat) -> "(P_typ " ^ pp_format_typ_lem typ ^ " " ^ pp_format_pat_lem pat ^ ")" | P_app(id,pats) -> "(P_app " ^ pp_format_id_lem id ^ " [" ^ list_format "; " pp_format_pat_lem pats ^ "])" | P_record(fpats,_) -> "(P_record [" ^ list_format "; " (fun (FP_aux(FP_Fpat(id,fpat),_)) -> "(FP_Fpat " ^ pp_format_id_lem id ^ " " ^ pp_format_pat_lem fpat ^ ")") fpats ^ "])" | P_vector(pats) -> "(P_vector [" ^ list_format "; " pp_format_pat_lem pats ^ "])" | P_vector_indexed(ipats) -> "(P_vector_indexed [" ^ list_format "; " (fun (i,p) -> Printf.sprintf "(%d, %s)" i (pp_format_pat_lem p)) ipats ^ "])" | P_vector_concat(pats) -> "(P_vector_concat [" ^ list_format "; " pp_format_pat_lem pats ^ "])" | P_tup(pats) -> "(P_tup [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])" | P_list(pats) -> "(P_list [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])") ^ " (" ^ pp_format_l_lem l ^ ", " ^ pp_format_annot annot ^ "))" let pp_lem_pat ppf p = base ppf (pp_format_pat_lem p) let rec pp_lem_let ppf (LB_aux(lb,(l,annot))) = let print_lb ppf lb = match lb with | LB_val_explicit(ts,pat,exp) -> fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "LB_val_explicit" pp_lem_typscm ts pp_lem_pat pat pp_lem_exp exp | LB_val_implicit(pat,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "LB_val_implicit" pp_lem_pat pat pp_lem_exp exp in fprintf ppf "@[<0>(LB_aux %a (%a, %a))@]" print_lb lb pp_lem_l l pp_annot annot and pp_lem_exp ppf (E_aux(e,(l,annot))) = let print_e ppf e = match e with | E_block(exps) -> fprintf ppf "@[<0>(E_aux %a [%a] %a (%a, %a))@]" kwd "(E_block" (list_pp pp_semi_lem_exp pp_lem_exp) exps kwd ")" pp_lem_l l pp_annot annot | E_nondet(exps) -> fprintf ppf "@[<0>(E_aux %a [%a] %a (%a, %a))@]" kwd "(E_nondet" (list_pp pp_semi_lem_exp pp_lem_exp) exps kwd ")" pp_lem_l l pp_annot annot | E_id(id) -> fprintf ppf "(E_aux (%a %a) (%a, %a))" kwd "E_id" pp_lem_id id pp_lem_l l pp_annot annot | E_lit(lit) -> fprintf ppf "(E_aux (%a %a) (%a, %a))" kwd "E_lit" pp_lem_lit lit pp_lem_l l pp_annot annot | E_cast(typ,exp) -> fprintf ppf "@[<0>(E_aux (E_cast %a %a) (%a, %a))@]" pp_lem_typ typ pp_lem_exp exp pp_lem_l l pp_annot annot | E_internal_cast((_,NoTyp),e) -> pp_lem_exp ppf e | E_app(f,args) -> fprintf ppf "@[<0>(E_aux (E_app %a [%a]) (%a, %a))@]" pp_lem_id f (list_pp pp_semi_lem_exp pp_lem_exp) args pp_lem_l l pp_annot annot | E_app_infix(l',op,r) -> fprintf ppf "@[<0>(E_aux (E_app_infix %a %a %a) (%a, %a))@]" pp_lem_exp l' pp_lem_id op pp_lem_exp r pp_lem_l l pp_annot annot | E_tuple(exps) -> fprintf ppf "@[<0>(E_aux (E_tuple [%a]) (%a, %a))@]" (list_pp pp_semi_lem_exp pp_lem_exp) exps pp_lem_l l pp_annot annot | E_if(c,t,e) -> fprintf ppf "@[<0>(E_aux (E_if %a @[<1>%a@] @[<1> %a@]) (%a, %a))@]" pp_lem_exp c pp_lem_exp t pp_lem_exp e pp_lem_l l pp_annot annot | E_for(id,exp1,exp2,exp3,order,exp4) -> fprintf ppf "@[<0>(E_aux (E_for %a %a %a %a %a @ @[<1> %a @]) (%a, %a))@]" pp_lem_id id pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_exp exp3 pp_lem_ord order pp_lem_exp exp4 pp_lem_l l pp_annot annot | E_vector(exps) -> fprintf ppf "@[<0>(E_aux (%a [%a]) (%a, %a))@]" kwd "E_vector" (list_pp pp_semi_lem_exp pp_lem_exp) exps pp_lem_l l pp_annot annot | E_vector_indexed(iexps,(Def_val_aux (default, (dl,dannot)))) -> let iformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) %a@]" i kwd ", " pp_lem_exp e kwd ";" in let lformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) @]" i kwd ", " pp_lem_exp e in let default_string ppf _ = (match default with | Def_val_empty -> fprintf ppf "(Def_val_aux Def_val_empty (%a,%a))" pp_lem_l dl pp_annot dannot | Def_val_dec e -> fprintf ppf "(Def_val_aux (Def_val_dec %a) (%a,%a))" pp_lem_exp e pp_lem_l dl pp_annot dannot) in fprintf ppf "@[<0>(E_aux (%a [%a] %a) (%a, %a))@]" kwd "E_vector_indexed" (list_pp iformat lformat) iexps default_string () pp_lem_l l pp_annot annot | E_vector_access(v,e) -> fprintf ppf "@[<0>(E_aux (%a %a %a) (%a, %a))@]" kwd "E_vector_access" pp_lem_exp v pp_lem_exp e pp_lem_l l pp_annot annot | E_vector_subrange(v,e1,e2) -> fprintf ppf "@[<0>(E_aux (E_vector_subrange %a %a %a) (%a, %a))@]" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_l l pp_annot annot | E_vector_update(v,e1,e2) -> fprintf ppf "@[<0>(E_aux (E_vector_update %a %a %a) (%a, %a))@]" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_l l pp_annot annot | E_vector_update_subrange(v,e1,e2,e3) -> fprintf ppf "@[<0>(E_aux (E_vector_update_subrange %a %a %a %a) (%a, %a))@]" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_exp e3 pp_lem_l l pp_annot annot | E_vector_append(v1,v2) -> fprintf ppf "@[<0>(E_aux (E_vector_append %a %a) (%a, %a))@]" pp_lem_exp v1 pp_lem_exp v2 pp_lem_l l pp_annot annot | E_list(exps) -> fprintf ppf "@[<0>(E_aux (E_list [%a]) (%a, %a))@]" (list_pp pp_semi_lem_exp pp_lem_exp) exps pp_lem_l l pp_annot annot | E_cons(e1,e2) -> fprintf ppf "@[<0>(E_aux (E_cons %a %a) (%a, %a))@]" pp_lem_exp e1 pp_lem_exp e2 pp_lem_l l pp_annot annot | E_record(FES_aux(FES_Fexps(fexps,_),(fl,fannot))) -> fprintf ppf "@[<0>(E_aux (E_record (FES_aux (FES_Fexps [%a] false) (%a,%a))) (%a, %a))@]" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps pp_lem_l fl pp_annot fannot pp_lem_l l pp_annot annot | E_record_update(exp,(FES_aux(FES_Fexps(fexps,_),(fl,fannot)))) -> fprintf ppf "@[<0>(E_aux (E_record_update %a (FES_aux (FES_Fexps [%a] false) (%a,%a))) (%a,%a))@]" pp_lem_exp exp (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps pp_lem_l fl pp_annot fannot pp_lem_l l pp_annot annot | E_field(fexp,id) -> fprintf ppf "@[<0>(E_aux (E_field %a %a) (%a, %a))@]" pp_lem_exp fexp pp_lem_id id pp_lem_l l pp_annot annot | E_case(exp,pexps) -> fprintf ppf "@[<0>(E_aux (E_case %a [%a]) (%a, %a))@]" pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps pp_lem_l l pp_annot annot | E_let(leb,exp) -> fprintf ppf "@[<0>(E_aux (E_let %a %a) (%a, %a))@]" pp_lem_let leb pp_lem_exp exp pp_lem_l l pp_annot annot | E_assign(lexp,exp) -> fprintf ppf "@[<0>(E_aux (E_assign %a %a) (%a, %a))@]" pp_lem_lexp lexp pp_lem_exp exp pp_lem_l l pp_annot annot | E_sizeof nexp -> fprintf ppf "@[<0>(E_aux (E_sizeof %a) (%a, %a))@]" pp_lem_nexp nexp pp_lem_l l pp_annot annot | E_exit exp -> fprintf ppf "@[<0>(E_aux (E_exit %a) (%a, %a))@]" pp_lem_exp exp pp_lem_l l pp_annot annot | E_return exp -> fprintf ppf "@[<0>(E_aux (E_return %a) (%a, %a))@]" pp_lem_exp exp pp_lem_l l pp_annot annot | E_assert(c,msg) -> fprintf ppf "@[<0>(E_aux (E_assert %a %a) (%a, %a))@]" pp_lem_exp c pp_lem_exp msg pp_lem_l l pp_annot annot | E_internal_exp ((l, Base((_,t),_,_,_,_,bindings))) -> (*TODO use bindings where appropriate*) (match t.t with | Tapp("register",[TA_typ {t=Tapp("vector",[TA_nexp _;TA_nexp r;_;_])}]) | Tapp("vector",[TA_nexp _;TA_nexp r;_;_]) -> (match r.nexp with | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]" kwd (lemnum string_of_int (int_of_big_int bi)) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob)) | Nvar v -> fprintf ppf "@[<0>(E_aux (E_id (Id_aux (Id \"%a\") %a)) (%a,%a))@]" kwd v pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob)) | _ -> raise (Reporting_basic.err_unreachable l "Internal exp given vector without known length")) | Tapp("implicit",[TA_nexp r]) -> (match r.nexp with | Nconst bi -> fprintf ppf "@[<0>(E_aux (E_lit (L_aux (L_num %a) %a)) (%a, %a))@]" kwd (lemnum string_of_int (int_of_big_int bi)) pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob)) | Nvar v -> fprintf ppf "@[<0>(E_aux (E_id (Id_aux (Id \"%a\") %a)) (%a,%a))@]" kwd v pp_lem_l l pp_lem_l l pp_annot (Base(([],nat_t),Emp_local,[],pure_e,pure_e,nob)) | _ -> raise (Reporting_basic.err_unreachable l "Internal_exp given implicit without variable or const")) | _ -> raise (Reporting_basic.err_unreachable l "Internal exp given non-vector or implicit")) | E_comment _ | E_comment_struc _ -> fprintf ppf "@[(E_aux (E_lit (L_aux L_unit %a)) (%a,%a))@]" pp_lem_l l pp_lem_l l pp_annot annot | E_internal_cast _ | E_internal_exp _ -> raise (Reporting_basic.err_unreachable l "Found internal cast or exp") | E_internal_exp_user _ -> (raise (Reporting_basic.err_unreachable l "Found non-rewritten internal_exp_user")) | E_sizeof_internal _ -> (raise (Reporting_basic.err_unreachable l "Internal sizeof not removed")) | E_internal_let _ -> (raise (Reporting_basic.err_unreachable l "Found non-rewritten internal_let")) | E_internal_return _ -> (raise (Reporting_basic.err_unreachable l "Found non-rewritten internal_return")) | E_internal_plet _ -> raise (Reporting_basic.err_unreachable l "Found non-rewritten internal_plet") in print_e ppf e and pp_semi_lem_exp ppf e = fprintf ppf "@[<1>%a%a@]" pp_lem_exp e kwd ";" and pp_lem_fexp ppf (FE_aux(FE_Fexp(id,exp),(l,annot))) = fprintf ppf "@[<1>(FE_aux (FE_Fexp %a %a) (%a, %a))@]" pp_lem_id id pp_lem_exp exp pp_lem_l l pp_annot annot and pp_semi_lem_fexp ppf fexp = fprintf ppf "@[<1>%a %a@]" pp_lem_fexp fexp kwd ";" and pp_lem_case ppf (Pat_aux(Pat_exp(pat,exp),(l,annot))) = fprintf ppf "@[<1>(Pat_aux (Pat_exp %a@ %a) (%a, %a))@]" pp_lem_pat pat pp_lem_exp exp pp_lem_l l pp_annot annot and pp_semi_lem_case ppf case = fprintf ppf "@[<1>%a %a@]" pp_lem_case case kwd ";" and pp_lem_lexp ppf (LEXP_aux(lexp,(l,annot))) = let print_le ppf lexp = match lexp with | LEXP_id(id) -> fprintf ppf "(%a %a)" kwd "LEXP_id" pp_lem_id id | LEXP_memory(id,args) -> fprintf ppf "(LEXP_memory %a [%a])" pp_lem_id id (list_pp pp_semi_lem_exp pp_lem_exp) args | LEXP_cast(typ,id) -> fprintf ppf "(LEXP_cast %a %a)" pp_lem_typ typ pp_lem_id id | LEXP_tup tups -> fprintf ppf "(LEXP_tup [%a])" (list_pp pp_semi_lem_lexp pp_lem_lexp) tups | LEXP_vector(v,exp) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_vector" pp_lem_lexp v pp_lem_exp exp | LEXP_vector_range(v,e1,e2) -> fprintf ppf "@[(%a %a %a %a)@]" kwd "LEXP_vector_range" pp_lem_lexp v pp_lem_exp e1 pp_lem_exp e2 | LEXP_field(v,id) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_field" pp_lem_lexp v pp_lem_id id in fprintf ppf "@[(LEXP_aux %a (%a, %a))@]" print_le lexp pp_lem_l l pp_annot annot and pp_semi_lem_lexp ppf le = fprintf ppf "@[<1>%a%a@]" pp_lem_lexp le kwd ";" let pp_lem_default ppf (DT_aux(df,l)) = let print_de ppf df = match df with | DT_kind(bk,var) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_kind" pp_lem_bkind bk pp_lem_var var | DT_typ(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_typ" pp_lem_typscm ts pp_lem_id id | DT_order(ord) -> fprintf ppf "@[<0>(DT_order %a)@]" pp_lem_ord ord in fprintf ppf "@[<0>(DT_aux %a %a)@]" print_de df pp_lem_l l let pp_lem_spec ppf (VS_aux(v,(l,annot))) = let print_spec ppf v = match v with | VS_val_spec(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id | VS_extern_spec(ts,id,s) -> fprintf ppf "@[<0>(%a %a %a \"%s\")@]@\n" kwd "VS_extern_spec" pp_lem_typscm ts pp_lem_id id s | VS_extern_no_rename(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_extern_no_rename" pp_lem_typscm ts pp_lem_id id in fprintf ppf "@[<0>(VS_aux %a (%a, %a))@]" print_spec v pp_lem_l l pp_annot annot let pp_lem_namescm ppf (Name_sect_aux(ns,l)) = match ns with | Name_sect_none -> fprintf ppf "(Name_sect_aux Name_sect_none %a)" pp_lem_l l | Name_sect_some(s) -> fprintf ppf "(Name_sect_aux (Name_sect_some \"%s\") %a)" s pp_lem_l l let rec pp_lem_range ppf (BF_aux(r,l)) = match r with | BF_single(i) -> fprintf ppf "(BF_aux (BF_single %i) %a)" i pp_lem_l l | BF_range(i1,i2) -> fprintf ppf "(BF_aux (BF_range %i %i) %a)" i1 i2 pp_lem_l l | BF_concat(ir1,ir2) -> fprintf ppf "(BF_aux (BF_concat %a %a) %a)" pp_lem_range ir1 pp_lem_range ir2 pp_lem_l l let pp_lem_typdef ppf (TD_aux(td,(l,annot))) = let print_td ppf td = match td with | TD_abbrev(id,namescm,typschm) -> fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "TD_abbrev" pp_lem_id id pp_lem_namescm namescm pp_lem_typscm typschm | TD_record(id,nm,typq,fs,_) -> let f_pp ppf (typ,id) = fprintf ppf "@[<1>(%a, %a)%a@]" pp_lem_typ typ pp_lem_id id kwd ";" in fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]" kwd "TD_record" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp f_pp f_pp) fs | TD_variant(id,nm,typq,ar,_) -> let a_pp ppf (Tu_aux(typ_u,l)) = match typ_u with | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_aux (Tu_ty_id %a %a) %a);@]" pp_lem_typ typ pp_lem_id id pp_lem_l l | Tu_id(id) -> fprintf ppf "@[<1>(Tu_aux (Tu_id %a) %a);@]" pp_lem_id id pp_lem_l l in fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]" kwd "TD_variant" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar | TD_enum(id,ns,enums,_) -> let pp_id_semi ppf id = fprintf ppf "%a%a " pp_lem_id id kwd ";" in fprintf ppf "@[<0>(%a %a %a [%a] false)@]" kwd "TD_enum" pp_lem_id id pp_lem_namescm ns (list_pp pp_id_semi pp_lem_id) enums | TD_register(id,n1,n2,rs) -> let pp_rid ppf (r,id) = fprintf ppf "(%a, %a)%a " pp_lem_range r pp_lem_id id kwd ";" in let pp_rids = (list_pp pp_rid pp_rid) in fprintf ppf "@[<0>(%a %a %a %a [%a])@]" kwd "TD_register" pp_lem_id id pp_lem_nexp n1 pp_lem_nexp n2 pp_rids rs in fprintf ppf "@[<0>(TD_aux %a (%a, %a))@]" print_td td pp_lem_l l pp_annot annot let pp_lem_kindef ppf (KD_aux(kd,(l,annot))) = let print_kd ppf kd = match kd with | KD_abbrev(kind,id,namescm,typschm) -> fprintf ppf "@[<0>(KD_abbrev %a %a %a %a)@]" pp_lem_kind kind pp_lem_id id pp_lem_namescm namescm pp_lem_typscm typschm | KD_nabbrev(kind,id,namescm,n) -> fprintf ppf "@[<0>(KD_nabbrev %a %a %a %a)@]" pp_lem_kind kind pp_lem_id id pp_lem_namescm namescm pp_lem_nexp n | KD_record(kind,id,nm,typq,fs,_) -> let f_pp ppf (typ,id) = fprintf ppf "@[<1>(%a, %a)%a@]" pp_lem_typ typ pp_lem_id id kwd ";" in fprintf ppf "@[<0>(%a %a %a %a %a [%a] false)@]" kwd "KD_record" pp_lem_kind kind pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp f_pp f_pp) fs | KD_variant(kind,id,nm,typq,ar,_) -> let a_pp ppf (Tu_aux(typ_u,l)) = match typ_u with | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_aux (Tu_ty_id %a %a) %a);@]" pp_lem_typ typ pp_lem_id id pp_lem_l l | Tu_id(id) -> fprintf ppf "@[<1>(Tu_aux (Tu_id %a) %a);@]" pp_lem_id id pp_lem_l l in fprintf ppf "@[<0>(%a %a %a %a %a [%a] false)@]" kwd "KD_variant" pp_lem_kind kind pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar | KD_enum(kind,id,ns,enums,_) -> let pp_id_semi ppf id = fprintf ppf "%a%a " pp_lem_id id kwd ";" in fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]" kwd "KD_enum" pp_lem_kind kind pp_lem_id id pp_lem_namescm ns (list_pp pp_id_semi pp_lem_id) enums | KD_register(kind,id,n1,n2,rs) -> let pp_rid ppf (r,id) = fprintf ppf "(%a, %a)%a " pp_lem_range r pp_lem_id id kwd ";" in let pp_rids = (list_pp pp_rid pp_rid) in fprintf ppf "@[<0>(%a %a %a %a %a [%a])@]" kwd "KD_register" pp_lem_kind kind pp_lem_id id pp_lem_nexp n1 pp_lem_nexp n2 pp_rids rs in fprintf ppf "@[<0>(KD_aux %a (%a, %a))@]" print_kd kd pp_lem_l l pp_annot annot let pp_lem_rec ppf (Rec_aux(r,l)) = match r with | Rec_nonrec -> fprintf ppf "(Rec_aux Rec_nonrec %a)" pp_lem_l l | Rec_rec -> fprintf ppf "(Rec_aux Rec_rec %a)" pp_lem_l l let pp_lem_tannot_opt ppf (Typ_annot_opt_aux(t,l)) = match t with | Typ_annot_opt_some(tq,typ) -> fprintf ppf "(Typ_annot_opt_aux (Typ_annot_opt_some %a %a) %a)" pp_lem_typquant tq pp_lem_typ typ pp_lem_l l let pp_lem_effects_opt ppf (Effect_opt_aux(e,l)) = match e with | Effect_opt_pure -> fprintf ppf "(Effect_opt_aux Effect_opt_pure %a)" pp_lem_l l | Effect_opt_effect e -> fprintf ppf "(Effect_opt_aux (Effect_opt_effect %a) %a)" pp_lem_effects e pp_lem_l l let pp_lem_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),(l,annot))) = fprintf ppf "@[<0>(FCL_aux (%a %a %a %a) (%a,%a))@]@\n" kwd "FCL_Funcl" pp_lem_id id pp_lem_pat pat pp_lem_exp exp pp_lem_l l pp_annot annot let pp_lem_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),(l,annot))) = let pp_funcls ppf funcl = fprintf ppf "%a %a" pp_lem_funcl funcl kwd ";" in fprintf ppf "@[<0>(FD_aux (%a %a %a %a [%a]) (%a, %a))@]" kwd "FD_function" pp_lem_rec r pp_lem_tannot_opt typa pp_lem_effects_opt efa (list_pp pp_funcls pp_funcls) fcls pp_lem_l l pp_annot annot let pp_lem_aspec ppf (AL_aux(aspec,(l,annot))) = let pp_reg_id ppf (RI_aux((RI_id ri),(l,annot))) = fprintf ppf "@[<0>(RI_aux (RI_id %a) (%a,%a))@]" pp_lem_id ri pp_lem_l l pp_annot annot in match aspec with | AL_subreg(reg,subreg) -> fprintf ppf "@[<0>(AL_aux (AL_subreg %a %a) (%a,%a))@]" pp_reg_id reg pp_lem_id subreg pp_lem_l l pp_annot annot | AL_bit(reg,ac) -> fprintf ppf "@[<0>(AL_aux (AL_bit %a %a) (%a,%a))@]" pp_reg_id reg pp_lem_exp ac pp_lem_l l pp_annot annot | AL_slice(reg,b,e) -> fprintf ppf "@[<0>(AL_aux (AL_slice %a %a %a) (%a,%a))@]" pp_reg_id reg pp_lem_exp b pp_lem_exp e pp_lem_l l pp_annot annot | AL_concat(f,s) -> fprintf ppf "@[<0>(AL_aux (AL_concat %a %a) (%a,%a))@]" pp_reg_id f pp_reg_id s pp_lem_l l pp_annot annot let pp_lem_dec ppf (DEC_aux(reg,(l,annot))) = match reg with | DEC_reg(typ,id) -> fprintf ppf "@[<0>(DEC_aux (DEC_reg %a %a) (%a,%a))@]" pp_lem_typ typ pp_lem_id id pp_lem_l l pp_annot annot | DEC_alias(id,alias_spec) -> fprintf ppf "@[<0>(DEC_aux (DEC_alias %a %a) (%a, %a))@]" pp_lem_id id pp_lem_aspec alias_spec pp_lem_l l pp_annot annot | DEC_typ_alias(typ,id,alias_spec) -> fprintf ppf "@[<0>(DEC_aux (DEC_typ_alias %a %a %a) (%a, %a))@]" pp_lem_typ typ pp_lem_id id pp_lem_aspec alias_spec pp_lem_l l pp_annot annot let pp_lem_def ppf d = match d with | DEF_default(df) -> fprintf ppf "(DEF_default %a);@\n" pp_lem_default df | DEF_spec(v_spec) -> fprintf ppf "(DEF_spec %a);@\n" pp_lem_spec v_spec | DEF_type(t_def) -> fprintf ppf "(DEF_type %a);@\n" pp_lem_typdef t_def | DEF_kind(k_def) -> fprintf ppf "(DEF_kind %a);@\n" pp_lem_kindef k_def | DEF_fundef(f_def) -> fprintf ppf "(DEF_fundef %a);@\n" pp_lem_fundef f_def | DEF_val(lbind) -> fprintf ppf "(DEF_val %a);@\n" pp_lem_let lbind | DEF_reg_dec(dec) -> fprintf ppf "(DEF_reg_dec %a);@\n" pp_lem_dec dec | DEF_comm d -> fprintf ppf "" | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "initial_check didn't remove all scattered Defs") let pp_lem_defs ppf (Defs(defs)) = fprintf ppf "Defs [@[%a@]]@\n" (list_pp pp_lem_def pp_lem_def) defs (* ************************************************************************** * pp from tannot to ASCII source, for pp of built-in type environment *) let rec pp_format_t_ascii t = match t.t with | Tid i -> i | Tvar i -> "'" ^ i | Tfn(t1,t2,_,e) -> (pp_format_t_ascii t1) ^ " -> " ^ (pp_format_t_ascii t2) ^ " effect " ^ pp_format_e_ascii e | Ttup(tups) -> "(" ^ (list_format ", " pp_format_t_ascii tups) ^ ")" | Tapp(i,args) -> i ^ "<" ^ list_format ", " pp_format_targ_ascii args ^ ">" | Tabbrev(ti,ta) -> (pp_format_t_ascii ti) (* (pp_format_t_ascii ta) *) | Tuvar(_) -> failwith "Tuvar in pp_format_t_ascii" | Toptions _ -> failwith "Toptions in pp_format_t_ascii" and pp_format_targ_ascii = function | TA_typ t -> pp_format_t_ascii t | TA_nexp n -> pp_format_n_ascii n | TA_eft e -> pp_format_e_ascii e | TA_ord o -> pp_format_o_ascii o and pp_format_n_ascii n = match n.nexp with | Nid (i, n) -> i (* from an abbreviation *) | Nvar i -> "'" ^ i | Nconst i -> (string_of_int (int_of_big_int i)) | Npos_inf -> "infinity" | Nadd(n1,n2) -> (pp_format_n_ascii n1) ^ "+" ^ (pp_format_n_ascii n2) | Nsub(n1,n2) -> (pp_format_n_ascii n1) ^ "-" ^ (pp_format_n_ascii n2) | Nmult(n1,n2) -> (pp_format_n_ascii n1) ^ "*" ^ (pp_format_n_ascii n2) | N2n(n,_) -> "2**"^(pp_format_n_ascii n) (* string_of_big_int i ^ *) | Nneg n -> "-" ^ (pp_format_n_ascii n) | Nuvar _ -> failwith "Nuvar in pp_format_n_ascii" | Nneg_inf -> "-infinity" | Npow _ -> failwith "Npow in pp_format_n_ascii" | Ninexact -> failwith "Ninexact in pp_format_n_ascii" and pp_format_e_ascii e = match e.effect with | Evar i -> "'" ^ i | Eset es -> "{" ^ (list_format ", " pp_format_base_effect_ascii es) ^ "}" | Euvar(_) -> failwith "Euvar in pp_format_e_ascii" and pp_format_o_ascii o = match o.order with | Ovar i -> "'" ^ i | Oinc -> "inc" | Odec -> "dec" | Ouvar(_) -> failwith "Ouvar in pp_format_o_ascii" and pp_format_base_effect_ascii (BE_aux(e,l)) = match e with | BE_rreg -> "rreg" | BE_wreg -> "wreg" | BE_rmem -> "rmem" | BE_wmem -> "wmem" | BE_wmv -> "wmv" | BE_eamem -> "eamem" | BE_barr -> "barr" | BE_depend -> "depend" | BE_undef -> "undef" | BE_unspec -> "unspec" | BE_nondet -> "nondet" | BE_lset -> "lset" | BE_lret -> "lret" | BE_escape -> "escape" and pp_format_nes_ascii nes = list_format ", " pp_format_ne_ascii nes and pp_format_ne_ascii ne = match ne with | Lt(_,_,n1,n2) -> pp_format_n_ascii n1 ^ " < " ^ pp_format_n_ascii n2 | LtEq(_,_,n1,n2) -> pp_format_n_ascii n1 ^ " <= " ^ pp_format_n_ascii n2 | NtEq(_,n1,n2) -> pp_format_n_ascii n1 ^ " != " ^ pp_format_n_ascii n2 | Eq(_,n1,n2) -> pp_format_n_ascii n1 ^ " = " ^ pp_format_n_ascii n2 | GtEq(_,_,n1,n2) -> pp_format_n_ascii n1 ^ " >= " ^ pp_format_n_ascii n2 | Gt(_,_,n1,n2) -> pp_format_n_ascii n1 ^ " > " ^ pp_format_n_ascii n2 | In(_,i,ns) | InS(_,{nexp=Nvar i},ns) -> i ^ " IN {" ^ (list_format ", " string_of_int ns)^ "}" | InS(_,_,ns) -> (* when the variable has been replaced by a unification variable, we use this *) failwith "InS in pp_format_nes_ascii" (*"(Nec_in \"fresh\" [" ^ (list_format "; " string_of_int ns)^ "])"*) | Predicate(_,n1,n2) -> "flow_constraints(" ^ pp_format_ne_ascii n1 ^", "^ pp_format_ne_ascii n2 ^")" | CondCons(_,_,_,nes_c,nes_t) -> failwith "CondCons in pp_format_nes_ascii" (*"(Nec_cond " ^ (pp_format_nes nes_c) ^ " " ^ (pp_format_nes nes_t) ^ ")"*) | BranchCons(_,_,nes_b) -> failwith "BranchCons in pp_format_nes_ascii" (*"(Nec_branch " ^ (pp_format_nes nes_b) ^ ")"*) let rec pp_format_annot_ascii = function | NoTyp -> "Nothing" | Base((targs,t),tag,nes,efct,efctsum,_) -> (*TODO print out bindings for use in pattern match in interpreter*) "forall " ^ list_format ", " (function (i,k) -> kind_to_string k ^" '"^ i) targs ^ (match nes with [] -> "" | _ -> ", " ^ pp_format_nes_ascii nes) ^ ". " ^ pp_format_t_ascii t ^ "\n" (* ^ " ********** " ^ pp_format_tag tag ^ ", " ^ pp_format_nes nes ^ ", " ^ pp_format_e_lem efct ^ ", " ^ pp_format_e_lem efctsum ^ "))" *) | Overload (tannot, return_type_overloading_allowed, tannots) -> pp_format_annot_ascii tannot ^ String.concat "" (List.map (function tannot' -> " " ^ pp_format_annot_ascii tannot' ) tannots) (**************************************************************************** * PPrint-based source-to-source pretty printer ****************************************************************************) open PPrint let doc_id (Id_aux(i,_)) = match i with | Id i -> string 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 [string "deinfix"; string x; empty]) let doc_var (Kid_aux(Var v,_)) = string v let doc_int i = string (string_of_int i) let doc_bkind (BK_aux(k,_)) = string (match k with | BK_type -> "Type" | BK_nat -> "Nat" | BK_order -> "Order" | BK_effect -> "Effect") let doc_op symb a b = infix 2 1 symb a b let doc_unop symb a = prefix 2 1 symb a let pipe = string "|" let arrow = string "->" let dotdot = string ".." let coloneq = string ":=" let lsquarebar = string "[|" let rsquarebar = string "|]" let squarebars = enclose lsquarebar rsquarebar let lsquarebarbar = string "[||" let rsquarebarbar = string "||]" let squarebarbars = enclose lsquarebarbar rsquarebarbar let lsquarecolon = string "[:" let rsquarecolon = string ":]" let squarecolons = enclose lsquarecolon rsquarecolon let lcomment = string "(*" let rcomment = string "*)" let comment = enclose lcomment rcomment let string_lit = enclose dquote dquote let spaces op = enclose space space op let semi_sp = semi ^^ space let comma_sp = comma ^^ space let colon_sp = spaces colon let doc_kind (K_aux(K_kind(klst),_)) = separate_map (spaces arrow) doc_bkind klst let doc_effect (BE_aux (e,_)) = string (match e with | BE_rreg -> "rreg" | BE_wreg -> "wreg" | BE_rmem -> "rmem" | BE_wmem -> "wmem" | BE_wmv -> "wmv" | BE_eamem -> "eamem" | BE_barr -> "barr" | BE_depend -> "depend" | BE_escape -> "escape" | BE_undef -> "undef" | BE_unspec -> "unspec" | BE_nondet -> "nondet") let doc_effects (Effect_aux(e,_)) = match e with | Effect_var v -> doc_var v | Effect_set [] -> string "pure" | Effect_set s -> braces (separate_map comma_sp doc_effect s) let doc_ord (Ord_aux(o,_)) = match o with | Ord_var v -> doc_var v | Ord_inc -> string "inc" | Ord_dec -> string "dec" let doc_typ, doc_atomic_typ, doc_nexp = (* 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; string "effect"; doc_effects efct] | _ -> tup_typ ty and tup_typ ((Typ_aux (t, _)) as ty) = match t with | Typ_tup typs -> parens (separate_map comma_sp app_typ typs) | _ -> app_typ ty and app_typ ((Typ_aux (t, _)) as ty) = match t with (*TODO Need to un bid-endian-ify this here, since both can transform to the shorthand, especially with <: and :> *) (* Special case simple vectors to improve legibility * XXX we assume big-endian here, as usual *) | Typ_app(Id_aux (Id "vector", _), [ Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant n, _)), _); Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant m, _)), _); Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_inc, _)), _); Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) -> (doc_id id) ^^ (brackets (if n = 0 then doc_int m else doc_op colon (doc_int n) (doc_int (n+m-1)))) | Typ_app(Id_aux (Id "vector", _), [ Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant n, _)), _); Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant m, _)), _); Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_dec, _)), _); Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) -> (doc_id id) ^^ (brackets (if n = m-1 then doc_int m else doc_op colon (doc_int n) (doc_int (m+1 -n)))) | Typ_app(Id_aux (Id "vector", _), [ Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_minus (Nexp_aux(Nexp_constant n, _), Nexp_aux(Nexp_constant 1, _)),_)),_); Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant m, _)), _); Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_dec, _)), _); Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) -> (doc_id id) ^^ (brackets (if n = m then doc_int m else doc_op colon (doc_int m) (doc_int (n-1)))) | Typ_app(Id_aux (Id "vector", _), [ Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_minus (n', Nexp_aux((Nexp_constant 1), _)),_) as n_n),_); Typ_arg_aux(Typ_arg_nexp m_nexp, _); Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_dec, _)), _); Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) -> (doc_id id) ^^ (brackets (if n' = m_nexp then nexp m_nexp else doc_op colon (nexp m_nexp) (nexp n_n))) | Typ_app(Id_aux (Id "vector", _), [ Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_sum (n', Nexp_aux((Nexp_constant -1), _)),_) as n_n),_); Typ_arg_aux(Typ_arg_nexp m_nexp, _); Typ_arg_aux (Typ_arg_order (Ord_aux (Ord_dec, _)), _); Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id id, _)), _)]) -> (doc_id id) ^^ (brackets (if n' = m_nexp then nexp m_nexp else doc_op colon (nexp m_nexp) (nexp n_n))) | Typ_app(Id_aux (Id "range", _), [ Typ_arg_aux(Typ_arg_nexp (Nexp_aux(Nexp_constant n, _)), _); Typ_arg_aux(Typ_arg_nexp m, _);]) -> (squarebars (if n = 0 then nexp m else doc_op colon (doc_int n) (nexp m))) | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) -> (squarecolons (nexp n)) | Typ_app(id,args) -> (* trailing space to avoid >> token in case of nested app types *) (doc_id id) ^^ (angles (separate_map comma_sp doc_typ_arg args)) ^^ space | _ -> atomic_typ ty (* for simplicity, skip vec_typ - which is only sugar *) and atomic_typ ((Typ_aux (t, _)) as ty) = match t with | Typ_id id -> doc_id id | Typ_var v -> doc_var v | Typ_wild -> underscore | 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 (Typ_arg_aux(t,_)) = match t with (* Be careful here because typ_arg is implemented as nexp in the * parser - in practice falling through app_typ after all the proper nexp * cases; so Typ_arg_typ has the same precedence as a Typ_app *) | Typ_arg_typ t -> app_typ t | Typ_arg_nexp n -> nexp n | Typ_arg_order o -> doc_ord o | Typ_arg_effect e -> doc_effects e (* same trick to handle precedence of nexp *) and nexp ne = sum_typ ne and sum_typ ((Nexp_aux(n,_)) as ne) = match n with | Nexp_sum(n1,n2) -> doc_op plus (sum_typ n1) (star_typ n2) | Nexp_minus(n1,n2) -> doc_op minus (sum_typ n1) (star_typ n2) | _ -> star_typ ne and star_typ ((Nexp_aux(n,_)) as ne) = match n with | Nexp_times(n1,n2) -> doc_op star (star_typ n1) (exp_typ n2) | _ -> exp_typ ne and exp_typ ((Nexp_aux(n,_)) as ne) = match n with | Nexp_exp n1 -> doc_unop (string "2**") (atomic_nexp_typ n1) | _ -> neg_typ ne and neg_typ ((Nexp_aux(n,_)) as ne) = match n with | Nexp_neg n1 -> (* XXX this is not valid Sail, only an internal representation - * work around by commenting it *) let minus = concat [string "(*"; minus; string "*)"] in minus ^^ (atomic_nexp_typ n1) | _ -> atomic_nexp_typ ne and atomic_nexp_typ ((Nexp_aux(n,_)) as ne) = match n with | Nexp_var v -> doc_var v | Nexp_id i -> doc_id i | Nexp_constant i -> doc_int i | Nexp_neg _ | Nexp_exp _ | Nexp_times _ | Nexp_sum _ | Nexp_minus _-> group (parens (nexp ne)) (* expose doc_typ, doc_atomic_typ and doc_nexp *) in typ, atomic_typ, nexp let doc_nexp_constraint (NC_aux(nc,_)) = match nc with | NC_fixed(n1,n2) -> doc_op equals (doc_nexp n1) (doc_nexp n2) | NC_bounded_ge(n1,n2) -> doc_op (string ">=") (doc_nexp n1) (doc_nexp n2) | NC_bounded_le(n1,n2) -> doc_op (string "<=") (doc_nexp n1) (doc_nexp n2) | NC_nat_set_bounded(v,bounds) -> doc_op (string "IN") (doc_var v) (braces (separate_map comma_sp doc_int bounds)) let doc_qi (QI_aux(qi,_)) = match qi with | QI_const n_const -> doc_nexp_constraint n_const | QI_id(KOpt_aux(ki,_)) -> match ki with | KOpt_none v -> doc_var v | KOpt_kind(k,v) -> separate space [doc_kind k; doc_var v] (* typ_doc is the doc for the type being quantified *) let doc_typquant (TypQ_aux(tq,_)) typ_doc = match tq with | TypQ_no_forall -> typ_doc | TypQ_tq [] -> failwith "TypQ_tq with empty list" | TypQ_tq qlist -> (* include trailing break because the caller doesn't know if tq is empty *) doc_op dot (separate space [string "forall"; separate_map comma_sp doc_qi qlist]) typ_doc let doc_typscm (TypSchm_aux(TypSchm_ts(tq,t),_)) = (doc_typquant tq (doc_typ t)) let doc_typscm_atomic (TypSchm_aux(TypSchm_ts(tq,t),_)) = (doc_typquant tq (doc_atomic_typ t)) let doc_lit (L_aux(l,_)) = utf8string (match l with | L_unit -> "()" | L_zero -> "bitzero" | L_one -> "bitone" | L_true -> "true" | L_false -> "false" | L_num i -> string_of_int i | L_hex n -> "0x" ^ n | L_bin n -> "0b" ^ n | L_undef -> "undefined" | L_string s -> "\"" ^ s ^ "\"") let doc_pat, doc_atomic_pat = let rec pat pa = pat_colons pa and pat_colons ((P_aux(p,l)) as pa) = match p with (* XXX add leading indentation if not flat - we need to define our own * combinator for that *) | P_vector_concat pats -> separate_map (space ^^ colon ^^ break 1) atomic_pat pats | _ -> app_pat pa and app_pat ((P_aux(p,l)) as pa) = match p with | P_app(id, ((_ :: _) as pats)) -> doc_unop (doc_id id) (parens (separate_map comma_sp atomic_pat pats)) | _ -> atomic_pat pa and atomic_pat ((P_aux(p,(l,annot))) as pa) = match p with | P_lit lit -> doc_lit lit | P_wild -> underscore | P_id id -> doc_id id | P_as(p,id) -> parens (separate space [pat p; string "as"; doc_id id]) | P_typ(typ,p) -> separate space [parens (doc_typ typ); atomic_pat p] | P_app(id,[]) -> doc_id id | P_record(fpats,_) -> braces (separate_map semi_sp fpat fpats) | P_vector pats -> brackets (separate_map comma_sp atomic_pat pats) | P_vector_indexed ipats -> brackets (separate_map comma_sp npat ipats) | P_tup pats -> parens (separate_map comma_sp atomic_pat pats) | P_list pats -> squarebarbars (separate_map semi_sp atomic_pat pats) | P_app(_, _ :: _) | P_vector_concat _ -> group (parens (pat pa)) and fpat (FP_aux(FP_Fpat(id,fpat),_)) = doc_op equals (doc_id id) (pat fpat) and npat (i,p) = doc_op equals (doc_int i) (pat p) (* expose doc_pat and doc_atomic_pat *) in pat, atomic_pat let doc_exp, doc_let = let rec exp e = group (or_exp e) and or_exp ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id ("|" | "||"),_) as op),r) -> doc_op (doc_id op) (and_exp l) (or_exp r) | _ -> and_exp expr and and_exp ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id ("&" | "&&"),_) as op),r) -> doc_op (doc_id op) (eq_exp l) (and_exp r) | _ -> eq_exp expr and eq_exp ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id ( (* XXX this is not very consistent - is the parser bogus here? *) "=" | "==" | "!=" | ">=" | ">=_s" | ">=_u" | ">" | ">_s" | ">_u" | "<=" | "<=_s" | "<" | "<_s" | "<_si" | "<_u" ),_) as op),r) -> doc_op (doc_id op) (eq_exp l) (at_exp r) (* XXX assignment should not have the same precedence as equal etc. *) | E_assign(le,exp) -> doc_op coloneq (doc_lexp le) (at_exp exp) | _ -> at_exp expr and at_exp ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id ("@" | "^^" | "^" | "~^"),_) as op),r) -> doc_op (doc_id op) (cons_exp l) (at_exp r) | _ -> cons_exp expr and cons_exp ((E_aux(e,_)) as expr) = match e with | E_vector_append(l,r) -> doc_op colon (shift_exp l) (cons_exp r) | E_cons(l,r) -> doc_op colon (shift_exp l) (cons_exp r) | _ -> shift_exp expr and shift_exp ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id (">>" | ">>>" | "<<" | "<<<"),_) as op),r) -> doc_op (doc_id op) (shift_exp l) (plus_exp r) | _ -> plus_exp expr and plus_exp ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id ("+" | "-" | "+_s" | "-_s"),_) as op),r) -> doc_op (doc_id op) (plus_exp l) (star_exp r) | _ -> star_exp expr and star_exp ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id ( "*" | "/" | "div" | "quot" | "quot_s" | "rem" | "mod" | "*_s" | "*_si" | "*_u" | "*_ui"),_) as op),r) -> doc_op (doc_id op) (star_exp l) (starstar_exp r) | _ -> starstar_exp expr and starstar_exp ((E_aux(e,_)) as expr) = match e with | E_app_infix(l,(Id_aux(Id "**",_) as op),r) -> doc_op (doc_id op) (starstar_exp l) (app_exp r) | E_if _ | E_for _ | E_let _ -> right_atomic_exp expr | _ -> app_exp expr and right_atomic_exp ((E_aux(e,_)) as expr) = match e with (* Special case: omit "else ()" when the else branch is empty. *) | E_if(c,t,E_aux(E_block [], _)) -> string "if" ^^ space ^^ group (exp c) ^/^ string "then" ^^ space ^^ group (exp t) | E_if(c,t,e) -> string "if" ^^ space ^^ group (exp c) ^/^ string "then" ^^ space ^^ group (exp t) ^/^ string "else" ^^ space ^^ group (exp e) | E_for(id,exp1,exp2,exp3,order,exp4) -> string "foreach" ^^ space ^^ group (parens ( separate (break 1) [ doc_id id; string "from " ^^ atomic_exp exp1; string "to " ^^ atomic_exp exp2; string "by " ^^ atomic_exp exp3; string "in " ^^ doc_ord order ] )) ^/^ exp exp4 | E_let(leb,e) -> doc_op (string "in") (let_exp leb) (exp e) | _ -> group (parens (exp expr)) and app_exp ((E_aux(e,_)) as expr) = match e with | E_app(f,args) -> (doc_id f) ^^ (parens (separate_map comma exp args)) | _ -> vaccess_exp expr and vaccess_exp ((E_aux(e,_)) as expr) = match e with | E_vector_access(v,e) -> atomic_exp v ^^ brackets (exp e) | E_vector_subrange(v,e1,e2) -> atomic_exp v ^^ brackets (doc_op dotdot (exp e1) (exp e2)) | _ -> field_exp expr and field_exp ((E_aux(e,_)) as expr) = match e with | E_field(fexp,id) -> atomic_exp fexp ^^ dot ^^ doc_id id | _ -> atomic_exp expr and atomic_exp ((E_aux(e,_)) as expr) = match e with (* Special case: an empty block is equivalent to unit, but { } would * be parsed as a struct. *) | E_block [] -> string "()" | E_block exps -> let exps_doc = separate_map (semi ^^ hardline) exp exps in surround 2 1 lbrace exps_doc rbrace | E_nondet exps -> let exps_doc = separate_map (semi ^^ hardline) exp exps in string "nondet" ^^ space ^^ (surround 2 1 lbrace exps_doc rbrace) | E_comment s -> string ("(*" ^ s ^ "*) ()") | E_comment_struc e -> string "(*" ^^ exp e ^^ string "*) ()" | E_id id -> doc_id id | E_lit lit -> doc_lit lit | E_cast(typ,e) -> prefix 2 1 (parens (doc_typ typ)) (group (atomic_exp e)) | E_internal_cast((_,NoTyp),e) -> atomic_exp e | E_internal_cast((_,Base((_,t),_,_,_,_,bindings)), (E_aux(_,(_,eannot)) as e)) -> (match t.t,eannot with (* XXX I don't understand why we can hide the internal cast here AAA Because an internal cast between vectors is only generated to reset the base access; the type checker generates far more than are needed and they're pruned off here, after constraint resolution *) | Tapp("vector",[TA_nexp n1;_;_;_]),Base((_,{t=Tapp("vector",[TA_nexp n2;_;_;_])}),_,_,_,_,_) when nexp_eq n1 n2 -> atomic_exp e | _ -> prefix 2 1 (parens (doc_typ (t_to_typ t))) (group (atomic_exp e))) | E_tuple exps -> parens (separate_map comma exp exps) | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> (* XXX E_record is not handled by parser currently AAA The parser can't handle E_record due to ambiguity with blocks; initial_check looks for blocks that are all field assignments and converts *) 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 default_print _ = brackets (separate_map comma exp exps) in (match exps with | [] -> default_print () | E_aux(e,_)::es -> (match e with | E_lit (L_aux(L_one, _)) | E_lit (L_aux(L_zero, _)) -> utf8string ("0b" ^ (List.fold_right (fun (E_aux( e,_)) rst -> (match e with | E_lit(L_aux(l, _)) -> ((match l with | L_one -> "1" | L_zero -> "0" | L_undef -> "u" | _ -> assert false) ^ rst) | _ -> assert false)) exps "")) | _ -> default_print ())) | E_vector_indexed (iexps, (Def_val_aux (default,_))) -> let default_string = (match default with | Def_val_empty -> string "" | Def_val_dec e -> concat [semi; space; string "default"; equals; (exp e)]) in let iexp (i,e) = doc_op equals (doc_int i) (exp e) in brackets (concat [(separate_map comma iexp iexps); default_string]) | E_vector_update(v,e1,e2) -> brackets (doc_op (string "with") (exp v) (doc_op equals (atomic_exp e1) (exp e2))) | E_vector_update_subrange(v,e1,e2,e3) -> brackets ( doc_op (string "with") (exp v) (doc_op equals (atomic_exp e1 ^^ colon ^^ atomic_exp e2) (exp e3))) | E_list exps -> squarebarbars (separate_map comma exp exps) | E_case(e,pexps) -> let opening = separate space [string "switch"; exp e; lbrace] in let cases = separate_map (break 1) doc_case pexps in surround 2 1 opening cases rbrace | E_sizeof n -> separate space [string "sizeof"; doc_nexp n] | E_exit e -> separate space [string "exit"; atomic_exp e;] | E_return e -> separate space [string "return"; atomic_exp e;] | E_assert(c,m) -> separate space [string "assert"; parens (separate comma [exp c; exp m])] (* adding parens and loop for lower precedence *) | E_app (_, _)|E_vector_access (_, _)|E_vector_subrange (_, _, _) | E_cons (_, _)|E_field (_, _)|E_assign (_, _) | E_if _ | E_for _ | E_let _ | E_vector_append _ | E_app_infix (_, (* for every app_infix operator caught at a higher precedence, * we need to wrap around with parens *) (Id_aux(Id("|" | "||" | "&" | "&&" | "=" | "==" | "!=" | ">=" | ">=_s" | ">=_u" | ">" | ">_s" | ">_u" | "<=" | "<=_s" | "<" | "<_s" | "<_si" | "<_u" | "@" | "^^" | "^" | "~^" | ">>" | ">>>" | "<<" | "<<<" | "+" | "-" | "+_s" | "-_s" | "*" | "/" | "div" | "quot" | "quot_s" | "rem" | "mod" | "*_s" | "*_si" | "*_u" | "*_ui" | "**"), _)) , _) -> group (parens (exp expr)) (* XXX default precedence for app_infix? *) | E_app_infix(l,op,r) -> failwith ("unexpected app_infix operator " ^ (pp_format_id op)) (* doc_op (doc_id op) (exp l) (exp r) *) | E_comment s -> comment (string s) | E_comment_struc e -> comment (exp e) | E_internal_exp((l, Base((_,t),_,_,_,_,bindings))) -> (*TODO use bindings, and other params*) (match t.t with | Tapp("register",[TA_typ {t=Tapp("vector",[TA_nexp _;TA_nexp r;_;_])}]) | Tapp("vector",[TA_nexp _;TA_nexp r;_;_]) -> (match r.nexp with | Nvar v -> utf8string v | Nconst bi -> utf8string (Big_int.string_of_big_int bi) | _ -> raise (Reporting_basic.err_unreachable l ("Internal exp given vector without known length, instead given " ^ n_to_string r))) | Tapp("implicit",[TA_nexp r]) -> (match r.nexp with | Nconst bi -> utf8string (Big_int.string_of_big_int bi) | Nvar v -> utf8string v | _ -> raise (Reporting_basic.err_unreachable l "Internal exp given implicit without var or const")) | _ -> raise (Reporting_basic.err_unreachable l ("Internal exp given non-vector, non-implicit " ^ t_to_string t))) | E_internal_exp_user _ -> raise (Reporting_basic.err_unreachable Unknown ("internal_exp_user not rewritten away")) | E_internal_cast ((_, Overload (_, _,_ )), _) | E_internal_exp _ -> assert false and let_exp (LB_aux(lb,_)) = match lb with | LB_val_explicit(ts,pat,e) -> (match ts with | TypSchm_aux (TypSchm_ts (TypQ_aux (TypQ_no_forall,_),_),_) -> prefix 2 1 (separate space [string "let"; parens (doc_typscm_atomic ts); doc_atomic_pat pat; equals]) (atomic_exp e) | _ -> prefix 2 1 (separate space [string "let"; doc_typscm_atomic ts; doc_atomic_pat pat; equals]) (atomic_exp e)) | LB_val_implicit(pat,e) -> prefix 2 1 (separate space [string "let"; doc_atomic_pat pat; equals]) (atomic_exp e) and doc_fexp (FE_aux(FE_Fexp(id,e),_)) = doc_op equals (doc_id id) (exp e) and doc_case (Pat_aux(Pat_exp(pat,e),_)) = doc_op arrow (separate space [string "case"; doc_atomic_pat pat]) (group (exp e)) (* lexps are parsed as eq_exp - we need to duplicate the precedence * structure for them *) and doc_lexp le = app_lexp le and app_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with | LEXP_memory(id,args) -> doc_id id ^^ parens (separate_map comma exp args) | _ -> vaccess_lexp le and vaccess_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with | LEXP_vector(v,e) -> atomic_lexp v ^^ brackets (exp e) | LEXP_vector_range(v,e1,e2) -> atomic_lexp v ^^ brackets (exp e1 ^^ dotdot ^^ exp e2) | _ -> field_lexp le and field_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with | LEXP_field(v,id) -> atomic_lexp v ^^ dot ^^ doc_id id | _ -> atomic_lexp le and atomic_lexp ((LEXP_aux(lexp,_)) as le) = match lexp with | LEXP_id id -> doc_id id | LEXP_cast(typ,id) -> prefix 2 1 (parens (doc_typ typ)) (doc_id id) | LEXP_memory _ | LEXP_vector _ | LEXP_vector_range _ | LEXP_field _ -> group (parens (doc_lexp le)) | LEXP_tup tups -> parens (separate_map comma doc_lexp tups) (* expose doc_exp and doc_let *) in exp, let_exp let doc_default (DT_aux(df,_)) = match df with | DT_kind(bk,v) -> separate space [string "default"; doc_bkind bk; doc_var v] | DT_typ(ts,id) -> separate space [string "default"; doc_typscm ts; doc_id id] | DT_order(ord) -> separate space [string "default"; string "order"; doc_ord ord] let doc_spec (VS_aux(v,_)) = match v with | VS_val_spec(ts,id) -> separate space [string "val"; doc_typscm ts; doc_id id] | VS_extern_no_rename(ts,id) -> separate space [string "val"; string "extern"; doc_typscm ts; doc_id id] | VS_extern_spec(ts,id,s) -> separate space [string "val"; string "extern"; doc_typscm ts; doc_op equals (doc_id id) (dquotes (string s))] let doc_namescm (Name_sect_aux(ns,_)) = match ns with | Name_sect_none -> empty (* include leading space because the caller doesn't know if ns is * empty, and trailing break already added by the following equals *) | Name_sect_some s -> space ^^ brackets (doc_op equals (string "name") (dquotes (string s))) let rec doc_range (BF_aux(r,_)) = match r with | BF_single i -> doc_int i | BF_range(i1,i2) -> doc_op dotdot (doc_int i1) (doc_int i2) | BF_concat(ir1,ir2) -> (doc_range ir1) ^^ comma ^^ (doc_range ir2) let doc_type_union (Tu_aux(typ_u,_)) = match typ_u with | Tu_ty_id(typ,id) -> separate space [doc_typ typ; doc_id id] | Tu_id id -> doc_id id let doc_typdef (TD_aux(td,_)) = match td with | TD_abbrev(id,nm,typschm) -> doc_op equals (concat [string "typedef"; space; doc_id id; doc_namescm nm]) (doc_typscm typschm) | TD_record(id,nm,typq,fs,_) -> let f_pp (typ,id) = concat [doc_typ typ; space; doc_id id; semi] in let fs_doc = group (separate_map (break 1) f_pp fs) in doc_op equals (concat [string "typedef"; space; doc_id id; doc_namescm nm]) (string "const struct" ^^ space ^^ doc_typquant typq (braces fs_doc)) | TD_variant(id,nm,typq,ar,_) -> let ar_doc = group (separate_map (semi ^^ break 1) doc_type_union ar) in doc_op equals (concat [string "typedef"; space; doc_id id; doc_namescm nm]) (string "const union" ^^ space ^^ doc_typquant typq (braces ar_doc)) | TD_enum(id,nm,enums,_) -> let enums_doc = group (separate_map (semi ^^ break 1) doc_id enums) in doc_op equals (concat [string "typedef"; space; doc_id id; doc_namescm nm]) (string "enumerate" ^^ space ^^ braces enums_doc) | TD_register(id,n1,n2,rs) -> let doc_rid (r,id) = separate space [doc_range r; colon; doc_id id] ^^ semi in let doc_rids = group (separate_map (break 1) doc_rid rs) in doc_op equals (string "typedef" ^^ space ^^ doc_id id) (separate space [ string "register bits"; brackets (doc_nexp n1 ^^ colon ^^ doc_nexp n2); braces doc_rids; ]) let doc_kindef (KD_aux(kd,_)) = match kd with | KD_abbrev(kind,id,nm,typschm) -> doc_op equals (concat [string "def"; space; doc_kind kind; space; doc_id id; doc_namescm nm]) (doc_typscm typschm) | KD_nabbrev(kind,id,nm,n) -> doc_op equals (concat [string "def"; space; doc_kind kind; space; doc_id id; doc_namescm nm]) (doc_nexp n) | KD_record(kind,id,nm,typq,fs,_) -> let f_pp (typ,id) = concat [doc_typ typ; space; doc_id id; semi] in let fs_doc = group (separate_map (break 1) f_pp fs) in doc_op equals (concat [string "def"; space;doc_kind kind; space; doc_id id; doc_namescm nm]) (string "const struct" ^^ space ^^ doc_typquant typq (braces fs_doc)) | KD_variant(kind,id,nm,typq,ar,_) -> let ar_doc = group (separate_map (semi ^^ break 1) doc_type_union ar) in doc_op equals (concat [string "def"; space; doc_kind kind; space; doc_id id; doc_namescm nm]) (string "const union" ^^ space ^^ doc_typquant typq (braces ar_doc)) | KD_enum(kind,id,nm,enums,_) -> let enums_doc = group (separate_map (semi ^^ break 1) doc_id enums) in doc_op equals (concat [string "def"; space; doc_kind kind; space; doc_id id; doc_namescm nm]) (string "enumerate" ^^ space ^^ braces enums_doc) | KD_register(kind,id,n1,n2,rs) -> let doc_rid (r,id) = separate space [doc_range r; colon; doc_id id] ^^ semi in let doc_rids = group (separate_map (break 1) doc_rid rs) in doc_op equals (string "def" ^^ space ^^ doc_kind kind ^^ space ^^ doc_id id) (separate space [ string "register bits"; brackets (doc_nexp n1 ^^ colon ^^ doc_nexp n2); braces doc_rids; ]) let doc_rec (Rec_aux(r,_)) = match r with | Rec_nonrec -> empty (* include trailing space because caller doesn't know if we return * empty *) | Rec_rec -> string "rec" ^^ space let doc_tannot_opt (Typ_annot_opt_aux(t,_)) = match t with | Typ_annot_opt_some(tq,typ) -> doc_typquant tq (doc_typ typ) let doc_effects_opt (Effect_opt_aux(e,_)) = match e with | Effect_opt_pure -> string "pure" | Effect_opt_effect e -> doc_effects e let doc_funcl (FCL_aux(FCL_Funcl(id,pat,exp),_)) = group (doc_op equals (separate space [doc_id id; doc_atomic_pat pat]) (doc_exp exp)) let doc_fundef (FD_aux(FD_function(r, typa, efa, fcls),_)) = match fcls with | [] -> failwith "FD_function with empty function list" | _ -> let sep = hardline ^^ string "and" ^^ space in let clauses = separate_map sep doc_funcl fcls in separate space ([string "function"; doc_rec r ^^ doc_tannot_opt typa;]@ (match efa with | Effect_opt_aux (Effect_opt_pure,_) -> [] | _ -> [string "effect"; doc_effects_opt efa;]) @[clauses]) let doc_alias (AL_aux (alspec,_)) = match alspec with | AL_subreg((RI_aux (RI_id id,_)),subid) -> doc_id id ^^ dot ^^ doc_id subid | AL_bit((RI_aux (RI_id id,_)),ac) -> doc_id id ^^ brackets (doc_exp ac) | AL_slice((RI_aux (RI_id id,_)),b,e) -> doc_id id ^^ brackets (doc_op dotdot (doc_exp b) (doc_exp e)) | AL_concat((RI_aux (RI_id f,_)),(RI_aux (RI_id s,_))) -> doc_op colon (doc_id f) (doc_id s) let doc_dec (DEC_aux (reg,_)) = match reg with | DEC_reg(typ,id) -> separate space [string "register"; doc_typ typ; doc_id id] | 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_typ typ) (doc_alias alspec) let doc_scattered (SD_aux (sdef, _)) = match sdef with | SD_scattered_function (r, typa, efa, id) -> separate space ([ string "scattered function"; doc_rec r ^^ doc_tannot_opt typa;]@ (match efa with | Effect_opt_aux (Effect_opt_pure,_) -> [] | _ -> [string "effect"; doc_effects_opt efa;]) @[doc_id id]) | SD_scattered_variant (id, ns, tq) -> doc_op equals (string "scattered typedef" ^^ space ^^ doc_id id ^^ doc_namescm ns) (string "const union" ^^ space ^^ (doc_typquant tq empty)) | SD_scattered_funcl funcl -> string "function clause" ^^ space ^^ doc_funcl funcl | SD_scattered_unioncl (id, tu) -> separate space [string "union"; doc_id id; string "member"; doc_type_union tu] | SD_scattered_end id -> string "end" ^^ space ^^ doc_id id let rec doc_def def = group (match def with | DEF_default df -> doc_default df | DEF_spec v_spec -> doc_spec v_spec | DEF_type t_def -> doc_typdef t_def | DEF_kind k_def -> doc_kindef k_def | DEF_fundef f_def -> doc_fundef f_def | DEF_val lbind -> doc_let lbind | DEF_reg_dec dec -> doc_dec dec | DEF_scattered sdef -> doc_scattered sdef | DEF_comm (DC_comm s) -> comment (string s) | DEF_comm (DC_comm_struct d) -> comment (doc_def d) ) ^^ hardline let doc_defs (Defs(defs)) = separate_map hardline doc_def defs let print ?(len=100) channel doc = ToChannel.pretty 1. len channel doc let to_buf ?(len=100) buf doc = ToBuffer.pretty 1. len buf doc let pp_defs f d = print f (doc_defs d) let pp_exp b e = to_buf b (doc_exp e) let pat_to_string p = let b = Buffer.create 20 in to_buf b (doc_pat p); Buffer.contents b (**************************************************************************** * PPrint-based sail-to-ocaml pretty printer ****************************************************************************) let star_sp = star ^^ space let is_number char = char = '0' || char = '1' || char = '2' || char = '3' || char = '4' || char = '5' || char = '6' || char = '7' || char = '8' || char = '9' let doc_id_ocaml (Id_aux(i,_)) = match i with | Id("bit") -> string "vbit" | Id i -> string (if i.[0] = '\'' || is_number(i.[0]) then "_" ^ i else String.uncapitalize 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 (String.uncapitalize 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 n (Id_aux(i,_)) = match i with | Id("bit") -> string "vbit" | Id i -> string ((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_wild -> underscore | 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 | Typ_arg_effect e -> 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 -> string_of_int i | 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 *) let doc_typquant_ocaml (TypQ_aux(tq,_)) typ_doc = typ_doc let doc_typscm_ocaml (TypSchm_aux(TypSchm_ts(tq,t),_)) = (doc_typquant 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)) -> (match annot with | Base(_,Constructor n,_,_,_,_) -> doc_unop (doc_id_ocaml_ctor n id) (parens (separate_map comma_sp pat pats)) | _ -> 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) -> doc_op colon (pat p) (doc_typ_ocaml typ) | P_app(id,[]) -> (match annot with | Base(_,Constructor n,_,_,_,_) -> doc_id_ocaml_ctor n id | _ -> empty) | 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 | Base(([],t),_,_,_,_,_) -> if is_bit_vector t then parens (separate space [string "Vvector"; parens (separate comma_sp [squarebars (separate_map semi pat pats); underscore; underscore])]) else non_bit_print() | _ -> 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*) in pat let doc_exp_ocaml, doc_let_ocaml = let rec top_exp read_registers (E_aux (e, (_,annot))) = let exp = top_exp read_registers in match e with | E_assign((LEXP_aux(le_act,tannot) as le),e) -> (match annot with | Base(_,(Emp_local | Emp_set),_,_,_,_) -> (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 _ -> doc_lexp_rwrite le e) | _ -> (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 "<=",string "+" else string ">=",string "-" 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 (doc_op compare var (string "__stop") ); string "then"; parens (exp exp4 ^^ space ^^ semi ^^ (string "foreach") ^^ parens (doc_op next var (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 annot with | Base(_,External (Some n),_,_,_,_) -> string n,false | Base(_,Constructor i,_,_,_,_) -> doc_id_ocaml_ctor i 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 = (match annot with | Base((_,t),_,_,_,_,_) -> (match t.t with | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> (string "bit_vector_access") | _ -> (string "vector_access")) | _ -> (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(_,(_,fannot)) as fexp),id) -> (match fannot with | Base((_,{t= Tapp("register",_)}),_,_,_,_,_) | Base((_,{t= Tabbrev(_,{t=Tapp("register",_)})}),_,_,_,_,_)-> let field_f = match annot with | Base((_,{t = Tid "bit"}),_,_,_,_,_) | Base((_,{t = Tabbrev(_,{t=Tid "bit"})}),_,_,_,_,_) -> string "get_register_field_bit" | _ -> string "get_register_field_vec" in parens (field_f ^^ space ^^ (exp fexp) ^^ space ^^ string_lit (doc_id id)) | _ -> exp fexp ^^ dot ^^ doc_id 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 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",_)})})),_,_,_,_,_) -> if read_registers then string "(read_register " ^^ doc_id_ocaml id ^^ string ")" else doc_id_ocaml id | Base(_,(Constructor i |Enum i),_,_,_,_) -> doc_id_ocaml_ctor i id | 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 (String.uncapitalize reg); string_lit (string field)]) | Alias_extract(reg,start,stop) -> if start = stop then parens (separate space [string "bit_vector_access";string (String.uncapitalize reg);doc_int start]) else parens (separate space [string "vector_subrange"; string (String.uncapitalize reg); doc_int start; doc_int stop]) | Alias_pair(reg1,reg2) -> parens (separate space [string "vector_concat"; string (String.uncapitalize reg1); string (String.uncapitalize reg2)])) | _ -> doc_id_ocaml id) | 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 | _ -> (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 -> (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_bit_vector t then (string "Vvector") else (string "VvectorR") in let dir,dir_out = match order.order with | Oinc -> true,"true" | _ -> false, "false" in let start = match start.nexp with | Nconst i -> string_of_big_int i | N2n(_,Some i) -> string_of_big_int 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_indexed (iexps, (Def_val_aux (default,_))) -> (match annot with | Base((_,t),_,_,_,_,_) -> match t.t with | Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _]) | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _])}) | Tapp("reg", [TA_typ {t =Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _])}]) -> let call = if is_bit_vector t then (string "make_indexed_bitv") else (string "make_indexed_v") in let dir,dir_out = match order.order with | Oinc -> true,"true" | _ -> false, "false" in let start = match start.nexp with | Nconst i | N2n(_,Some i)-> string_of_big_int i | N2n({nexp=Nconst i},_) -> string_of_int (Util.power 2 (int_of_big_int i)) | _ -> if dir then "0" else string_of_int (List.length iexps) in let size = match len.nexp with | Nconst i | N2n(_,Some i)-> string_of_big_int i | N2n({nexp=Nconst i},_) -> string_of_int (Util.power 2 (int_of_big_int i)) in let default_string = (match default with | Def_val_empty -> string "None" | Def_val_dec e -> parens (string "Some " ^^ (exp e))) in let iexp (i,e) = parens (separate_map comma_sp (fun x -> x) [(doc_int i); (exp e)]) in parens (separate space [call; (brackets (separate_map semi iexp iexps)); default_string; string start; string size; 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 true 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_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;] and let_exp (LB_aux(lb,_)) = match lb with | LB_val_explicit(ts,pat,e) -> prefix 2 1 (separate space [string "let"; doc_pat_ocaml pat; equals]) (top_exp false e) | LB_val_implicit(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 (Pat_aux(Pat_exp(pat,e),_)) = doc_op arrow (separate space [pipe; doc_pat_ocaml pat]) (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 | Base((_,{t=Tapp("reg",_)}),Emp_set,_,_,_,_),false | Base((_,{t=Tabbrev(_,{t=Tapp("reg",_)})}),Emp_set,_,_,_,_),false -> string "!" ^^ name | _ -> name and doc_lexp_array_ocaml ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with | LEXP_vector(v,e) -> (match annot with | Base((_,t),_,_,_,_,_) -> let t_act = match t.t with | Tapp("reg",[TA_typ t]) | Tabbrev(_,{t=Tapp("reg",[TA_typ t])}) -> t | _ -> t in (match t_act.t with | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> parens ((string "get_barray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens (top_exp false e) | _ -> parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens (top_exp false e)) | _ -> parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens (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 e_new_v with | E_aux(_,(_,Base((_,t),_,_,_,_,_))) -> (match t.t with | Tapp("vector", [_;_;_;(TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})}))]) | Tabbrev(_,{t=Tapp("vector",[_;_;_;TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})})])}) | Tapp("reg", [TA_typ {t= Tapp("vector", [_;_;_;(TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})}))])}]) -> (false,true) | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) | Tapp("reg",[TA_typ ({t=Tid "bit"} | {t=Tabbrev(_,{t=Tid "bit"})})]) -> (true,false) | _ -> (false,false)) | _ -> (false,false) in match lexp with | LEXP_vector(v,e) -> doc_op (string "<-") (group (parens ((string (if is_bit then "get_barray" else "get_varray")) ^^ space ^^ doc_lexp_ocaml false v)) ^^ dot ^^ parens (exp e)) (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 (String.uncapitalize 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 (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 n id; string "of"; doc_typ_ocaml typ;] | Tu_id id -> separate space [pipe; doc_id_ocaml_ctor n 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 n) 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 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"); brackets doc_rids]))]) let doc_kdef_ocaml (KD_aux(kd,_)) = match kd with | KD_abbrev(_,id,nm,typschm) -> doc_op equals (concat [string "type"; space; doc_id_ocaml_type id;]) (doc_typscm_ocaml typschm) | KD_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)) | KD_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)) | KD_enum(_,id,nm,enums,_) -> let n = List.length enums in let enums_doc = group (separate_map (break 1 ^^ pipe) (doc_id_ocaml_ctor n) enums) in doc_op equals (concat [string "type"; space; doc_id_ocaml_type id;]) (enums_doc) | KD_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 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"); brackets doc_rids]))]) 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_ocaml (FCL_aux(FCL_Funcl(id,pat,exp),_)) = group (doc_op arrow (doc_pat_ocaml pat) (doc_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_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) -> (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 "Vregister"; parens (separate comma [separate space [string "ref"; parens (separate space [string "Array.make"; doc_int (int_of_big_int size); string "Vzero";])]; doc_int (int_of_big_int start); o; brackets empty])] | _ -> empty) | Tapp("register", [TA_typ {t=Tid idt}]) | Tabbrev( {t= Tid idt}, _) -> separate space [string "let"; doc_id_ocaml id; equals; string idt; string "None"] |_-> empty) | _ -> empty) | 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*) ) ^^ 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)) (**************************************************************************** * PPrint-based sail-to-lem pprinter ****************************************************************************) let langlebar = string "<|" let ranglebar = string "|>" let anglebars = enclose langlebar ranglebar let fix_id name = match name with | "assert" | "lsl" | "lsr" | "asr" | "type" | "fun" | "function" | "raise" | "try" | "match" | "with" | "field" | "LT" | "GT" | "EQ" | "integer" -> name ^ "'" | _ -> name let doc_id_lem (Id_aux(i,_)) = match i with | Id i -> (* this not the right place to do this, just a workaround *) if i.[0] = '\'' then string ((String.sub i 1 (String.length i - 1)) ^ "'") else if is_number(i.[0]) then string ("v" ^ i ^ "'") else string (fix_id 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_lem_type (Id_aux(i,_)) = match i with | Id("int") -> string "ii" | Id("nat") -> string "ii" | Id("option") -> string "maybe" | Id i -> string (fix_id 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_lem_ctor (Id_aux(i,_)) = match i with | Id("bit") -> string "bitU" | Id("int") -> string "integer" | Id("nat") -> string "integer" | Id("Some") -> string "Just" | Id("None") -> string "Nothing" | Id i -> string (fix_id (String.capitalize i)) | DeIid x -> (* add an extra space through empty to avoid a closing-comment * token in case of x ending with star. *) separate space [colon; string (String.capitalize x); empty] let effectful (Effect_aux (eff,_)) = match eff with | Effect_var _ -> failwith "effectful: Effect_var not supported" | Effect_set effs -> List.exists (fun (BE_aux (eff,_)) -> match eff with | BE_rreg | BE_wreg | BE_rmem | BE_wmem | BE_eamem | BE_wmv | BE_barr | BE_depend | BE_nondet | BE_escape -> true | _ -> false) effs let rec is_number {t=t} = match t with | Tabbrev (t1,t2) -> is_number t1 || is_number t2 | Tapp ("range",_) | Tapp ("implicit",_) | Tapp ("atom",_) -> true | _ -> false let doc_typ_lem, doc_atomic_typ_lem = (* following the structure of parser for precedence *) let rec typ regtypes ty = fn_typ regtypes true ty and typ' regtypes ty = fn_typ regtypes false ty and fn_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with | Typ_fn(arg,ret,efct) -> (*let exc_typ = string "string" in*) let ret_typ = if effectful efct then separate space [string "M";(*parens exc_typ;*) fn_typ regtypes true ret] else separate space [fn_typ regtypes false ret] in let tpp = separate space [tup_typ regtypes true arg; arrow;ret_typ] in (* once we have proper excetions we need to know what the exceptions type is *) if atyp_needed then parens tpp else tpp | _ -> tup_typ regtypes atyp_needed ty and tup_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with | Typ_tup typs -> let tpp = separate_map (space ^^ star ^^ space) (app_typ regtypes false) typs in if atyp_needed then parens tpp else tpp | _ -> app_typ regtypes atyp_needed ty and app_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with | Typ_app(Id_aux (Id "vector", _),[_;_;_;Typ_arg_aux (Typ_arg_typ typa, _)]) -> let tpp = string "vector" ^^ space ^^ typ regtypes typa in if atyp_needed then parens tpp else tpp | Typ_app(Id_aux (Id "range", _),_) -> (string "integer") | Typ_app(Id_aux (Id "implicit", _),_) -> (string "integer") | Typ_app(Id_aux (Id "atom", _), [Typ_arg_aux(Typ_arg_nexp n,_)]) -> (string "integer") | Typ_app(id,args) -> let tpp = (doc_id_lem_type id) ^^ space ^^ (separate_map space (doc_typ_arg_lem regtypes) args) in if atyp_needed then parens tpp else tpp | _ -> atomic_typ regtypes atyp_needed ty and atomic_typ regtypes atyp_needed ((Typ_aux (t, _)) as ty) = match t with | Typ_id (Id_aux (Id "bool",_)) -> string "bitU" | Typ_id (Id_aux (Id "boolean",_)) -> string "bitU" | Typ_id (Id_aux (Id "bit",_)) -> string "bitU" | Typ_id ((Id_aux (Id name,_)) as id) -> if List.exists ((=) name) regtypes then string "register" else doc_id_lem_type id | Typ_var v -> doc_var v | Typ_wild -> underscore | Typ_app _ | Typ_tup _ | Typ_fn _ -> (* exhaustiveness matters here to avoid infinite loops * if we add a new Typ constructor *) let tpp = typ regtypes ty in if atyp_needed then parens tpp else tpp and doc_typ_arg_lem regtypes (Typ_arg_aux(t,_)) = match t with | Typ_arg_typ t -> app_typ regtypes false t | Typ_arg_nexp n -> empty | Typ_arg_order o -> empty | Typ_arg_effect e -> empty in typ', atomic_typ (* doc_lit_lem gets as an additional parameter the type information from the * expression around it: that's a hack, but how else can we distinguish between * undefined values of different types ? *) let doc_lit_lem in_pat (L_aux(lit,l)) a = utf8string (match lit with | L_unit -> "()" | L_zero -> "B0" | L_one -> "B1" | L_false -> "B0" | L_true -> "B1" | L_num i -> let ipp = string_of_int i in if in_pat then "("^ipp^":nn)" else if i < 0 then "((0"^ipp^"):ii)" else "("^ipp^":ii)" | L_hex n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)*) | L_bin n -> failwith "Shouldn't happen" (*"(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)*) | L_undef -> let (Base ((_,{t = t}),_,_,_,_,_)) = a in (match t with | Tid "bit" | Tabbrev ({t = Tid "bit"},_) -> "BU" | Tapp ("register",_) | Tabbrev ({t = Tapp ("register",_)},_) -> "UndefinedRegister 0" | Tid "string" | Tabbrev ({t = Tapp ("string",_)},_) -> "\"\"" | _ -> "(failwith \"undefined value of unsupported type\")") | L_string s -> "\"" ^ s ^ "\"") (* typ_doc is the doc for the type being quantified *) let doc_typquant_lem (TypQ_aux(tq,_)) typ_doc = typ_doc let doc_typschm_lem regtypes (TypSchm_aux(TypSchm_ts(tq,t),_)) = (doc_typquant_lem tq (doc_typ_lem regtypes 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 rec doc_pat_lem regtypes apat_needed (P_aux (p,(l,annot)) as pa) = match p with | P_app(id, ((_ :: _) as pats)) -> (match annot with | Base(_,(Constructor _ | Enum _),_,_,_,_) -> let ppp = doc_unop (doc_id_lem_ctor id) (parens (separate_map comma (doc_pat_lem regtypes true) pats)) in if apat_needed then parens ppp else ppp | _ -> empty) | P_app(id,[]) -> (match annot with | Base(_,(Constructor _| Enum _),_,_,_,_) -> doc_id_lem_ctor id | _ -> empty) | P_lit lit -> doc_lit_lem true lit annot | P_wild -> underscore | P_id id -> begin match id with | Id_aux (Id "None",_) -> string "Nothing" (* workaround temporary issue *) | _ -> doc_id_lem id end | P_as(p,id) -> parens (separate space [doc_pat_lem regtypes true p; string "as"; doc_id_lem id]) | P_typ(typ,p) -> doc_op colon (doc_pat_lem regtypes true p) (doc_typ_lem regtypes typ) | P_vector pats -> let ppp = (separate space) [string "Vector";brackets (separate_map semi (doc_pat_lem regtypes true) pats);underscore;underscore] in if apat_needed then parens ppp else ppp | P_vector_concat pats -> let ppp = (separate space) [string "Vector";parens (separate_map (string "::") (doc_pat_lem regtypes true) pats);underscore;underscore] in if apat_needed then parens ppp else ppp | P_tup pats -> (match pats with | [p] -> doc_pat_lem regtypes apat_needed p | _ -> parens (separate_map comma_sp (doc_pat_lem regtypes false) pats)) | P_list pats -> brackets (separate_map semi (doc_pat_lem regtypes false) pats) (*Never seen but easy in lem*) let prefix_recordtype = true let report = Reporting_basic.err_unreachable let doc_exp_lem, doc_let_lem = let rec top_exp regtypes (aexp_needed : bool) (E_aux (e, (l,annot))) = let expY = top_exp regtypes true in let expN = top_exp regtypes false in let expV = top_exp regtypes in match e with | E_assign((LEXP_aux(le_act,tannot) as le),e) -> (* can only be register writes *) let (_,(Base ((_,{t = t}),tag,_,_,_,_))) = tannot in (match le_act, t, tag with | LEXP_vector_range (le,e2,e3),_,_ -> (match le with | LEXP_aux (LEXP_field (le,id), (_,((Base ((_,{t = t}),_,_,_,_,_))))) -> if t = Tid "bit" then raise (report l "indexing a register's (single bit) bitfield not supported") else (prefix 2 1) (string "write_reg_field_range") (align (doc_lexp_deref_lem regtypes le ^^ space^^ string_lit (doc_id_lem id) ^/^ expY e2 ^/^ expY e3 ^/^ expY e)) | _ -> (prefix 2 1) (string "write_reg_range") (align (doc_lexp_deref_lem regtypes le ^^ space ^^ expY e2 ^/^ expY e3 ^/^ expY e)) ) | LEXP_vector (le,e2), (Tid "bit" | Tabbrev (_,{t=Tid "bit"})),_ -> (match le with | LEXP_aux (LEXP_field (le,id), (_,((Base ((_,{t = t}),_,_,_,_,_))))) -> if t = Tid "bit" then raise (report l "indexing a register's (single bit) bitfield not supported") else (prefix 2 1) (string "write_reg_field_bit") (align (doc_lexp_deref_lem regtypes le ^^ space ^^ doc_id_lem id ^/^ expY e2 ^/^ expY e)) | _ -> (prefix 2 1) (string "write_reg_bit") (doc_lexp_deref_lem regtypes le ^^ space ^^ expY e2 ^/^ expY e) ) | LEXP_field (le,id), (Tid "bit"| Tabbrev (_,{t=Tid "bit"})), _ -> (prefix 2 1) (string "write_reg_bitfield") (doc_lexp_deref_lem regtypes le ^^ space ^^ string_lit(doc_id_lem id) ^/^ expY e) | LEXP_field (le,id), _, _ -> (prefix 2 1) (string "write_reg_field") (doc_lexp_deref_lem regtypes le ^^ space ^^ string_lit(doc_id_lem id) ^/^ expY e) | (LEXP_id id | LEXP_cast (_,id)), t, Alias alias_info -> (match alias_info with | Alias_field(reg,field) -> let f = match t with | (Tid "bit" | Tabbrev (_,{t=Tid "bit"})) -> string "write_reg_bitfield" | _ -> string "write_reg_field" in (prefix 2 1) f (separate space [string reg;string_lit(string field);expY e]) | Alias_pair(reg1,reg2) -> string "write_two_regs" ^^ space ^^ string reg1 ^^ space ^^ string reg2 ^^ space ^^ expY e) | _ -> (prefix 2 1) (string "write_reg") (doc_lexp_deref_lem regtypes le ^/^ expY e)) | E_vector_append(l,r) -> let epp = align (group (separate space [expY l;string "^^"] ^/^ expY r)) in if aexp_needed then parens epp else epp | E_cons(l,r) -> doc_op (group (colon^^colon)) (expY l) (expY r) | E_if(c,t,e) -> let (E_aux (_,(_,cannot))) = c in let epp = separate space [string "if";group (align (string "bitU_to_bool" ^//^ group (expY c)))] ^^ break 1 ^^ (prefix 2 1 (string "then") (expN t)) ^^ (break 1) ^^ (prefix 2 1 (string "else") (expN e)) in if aexp_needed then parens (align epp) else epp | E_for(id,exp1,exp2,exp3,(Ord_aux(order,_)),exp4) -> raise (report l "E_for should have been removed till now") | E_let(leb,e) -> let epp = let_exp regtypes leb ^^ space ^^ string "in" ^^ hardline ^^ expN e in if aexp_needed then parens epp else epp | E_app(f,args) -> begin match f with (* temporary hack to make the loop body a function of the temporary variables *) | Id_aux ((Id (("foreach_inc" | "foreach_dec" | "foreachM_inc" | "foreachM_dec" ) as loopf),_)) -> let [id;indices;body;e5] = args in let varspp = match e5 with | E_aux (E_tuple vars,_) -> let vars = List.map (fun (E_aux (E_id (Id_aux (Id name,_)),_)) -> string name) vars in begin match vars with | [v] -> v | _ -> parens (separate comma vars) end | E_aux (E_id (Id_aux (Id name,_)),_) -> string name | E_aux (E_lit (L_aux (L_unit,_)),_) -> string "_" in parens ( (prefix 2 1) ((separate space) [string loopf;group (expY indices);expY e5]) (parens (prefix 1 1 (separate space [string "fun";expY id;varspp;arrow]) (expN body)) ) ) | Id_aux (Id "append",_) -> let [e1;e2] = args in let epp = align (expY e1 ^^ space ^^ string "++" ^//^ expY e2) in if aexp_needed then parens (align epp) else epp | Id_aux (Id "slice_raw",_) -> let [e1;e2;e3] = args in let epp = separate space [string "slice_raw";expY e1;expY e2;expY e3] in if aexp_needed then parens (align epp) else epp | _ -> begin match annot with | Base (_,External (Some "bitwise_not_bit"),_,_,_,_) -> let [a] = args in let epp = align (string "~" ^^ expY a) in if aexp_needed then parens (align epp) else epp | Base (_,Constructor _,_,_,_,_) -> let argpp a_needed arg = let (E_aux (_,(_,Base((_,{t=t}),_,_,_,_,_)))) = arg in match t with | Tapp("vector",_) -> let epp = concat [string "reset_vector_start";space;expY arg] in if a_needed then parens epp else epp | _ -> expV a_needed arg in let epp = match args with | [] -> doc_id_lem_ctor f | [arg] -> doc_id_lem_ctor f ^^ space ^^ argpp true arg | _ -> doc_id_lem_ctor f ^^ space ^^ parens (separate_map comma (argpp false) args) in if aexp_needed then parens (align epp) else epp | _ -> let call = match annot with | Base(_,External (Some n),_,_,_,_) -> string n | _ -> doc_id_lem f in let argpp a_needed arg = let (E_aux (_,(_,Base((_,{t=t}),_,_,_,_,_)))) = arg in match t with | Tapp("vector",_) -> let epp = concat [string "reset_vector_start";space;expY arg] in if a_needed then parens epp else epp | _ -> expV a_needed arg in let argspp = match args with | [arg] -> argpp true arg | args -> parens (align (separate_map (comma ^^ break 0) (argpp false) args)) in let epp = align (call ^//^ argspp) in if aexp_needed then parens (align epp) else epp end end | E_vector_access (v,e) -> let (Base (_,_,_,_,eff,_)) = annot in let epp = if has_rreg_effect eff then separate space [string "read_reg_bit";expY v;expY e] else separate space [string "access";expY v;expY e] in if aexp_needed then parens (align epp) else epp | E_vector_subrange (v,e1,e2) -> let (Base (_,_,_,_,eff,_)) = annot in let epp = if has_rreg_effect eff then align (string "read_reg_range" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2) else align (string "slice" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2) in if aexp_needed then parens (align epp) else epp | E_field((E_aux(_,(l,fannot)) as fexp),id) -> let (Base ((_,{t = t}),_,_,_,_,_)) = fannot in (match t with | Tabbrev({t = Tid regtyp},{t=Tapp("register",_)}) -> let field_f = match annot with | Base((_,{t = Tid "bit"}),_,_,_,_,_) | Base((_,{t = Tabbrev(_,{t=Tid "bit"})}),_,_,_,_,_) -> string "read_reg_bitfield" | _ -> string "read_reg_field" in let epp = field_f ^^ space ^^ (expY fexp) ^^ space ^^ string_lit (doc_id_lem id) in if aexp_needed then parens (align epp) else epp | Tid recordtyp | Tabbrev ({t = Tid recordtyp},_) -> let fname = if prefix_recordtype then (string (recordtyp ^ "_")) ^^ doc_id_lem id else doc_id_lem id in expY fexp ^^ dot ^^ fname | _ -> raise (report l "E_field expression with no register or record type")) | E_block [] -> string "()" | E_block exps -> raise (report l "Blocks should have been removed till now.") | E_nondet exps -> raise (report l "Nondet blocks not supported.") | E_id id -> (match annot with | Base((_, ({t = Tapp("register",_)} | {t=Tabbrev(_,{t=Tapp("register",_)})})), External _,_,eff,_,_) -> if has_rreg_effect eff then separate space [string "read_reg";doc_id_lem id] else doc_id_lem id | Base(_,(Constructor i |Enum i),_,_,_,_) -> doc_id_lem_ctor id | Base((_,t),Alias alias_info,_,eff,_,_) -> (match alias_info with | Alias_field(reg,field) -> let epp = match t.t with | Tid "bit" | Tabbrev (_,{t=Tid "bit"}) -> (separate space) [string "read_reg_bitfield"; string reg;string_lit(string field)] | _ -> (separate space) [string "read_reg_field"; string reg; string_lit(string field)] in if aexp_needed then parens (align epp) else epp | Alias_pair(reg1,reg2) -> let epp = if has_rreg_effect eff then separate space [string "read_two_regs";string reg1;string reg2] else separate space [string "RegisterPair";string reg1;string reg2] in if aexp_needed then parens (align epp) else epp | Alias_extract(reg,start,stop) -> let epp = if start = stop then (separate space) [string "access";doc_int start; parens (string "read_reg" ^^ space ^^ string reg)] else (separate space) [string "slice"; doc_int start; doc_int stop; parens (string "read_reg" ^^ space ^^ string reg)] in if aexp_needed then parens (align epp) else epp ) | _ -> doc_id_lem id) | E_lit lit -> doc_lit_lem false lit annot | E_cast(Typ_aux (typ,_),e) -> (match annot with | Base(_,External _,_,_,_,_) -> string "read_reg" ^^ space ^^ expY e | _ -> (match typ with | Typ_app (Id_aux (Id "vector",_), [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i,_)),_);_;_;_]) -> let epp = (concat [string "set_vector_start";space;string (string_of_int i)]) ^//^ expY e in if aexp_needed then parens epp else epp | Typ_var (Kid_aux (Var "length",_)) -> let epp = (string "set_vector_start_to_length") ^//^ expY e in if aexp_needed then parens epp else epp | _ -> expV aexp_needed e)) (*(parens (doc_op colon (group (expY e)) (doc_typ_lem typ)))) *) | E_tuple exps -> (match exps with (* | [e] -> expV aexp_needed e *) | _ -> parens (separate_map comma expN exps)) | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> let (Base ((_,{t = t}),_,_,_,_,_)) = annot in let recordtyp = match t with | Tid recordtyp | Tabbrev ({t = Tid recordtyp},_) -> recordtyp | _ -> raise (report l "cannot get record type") in let epp = anglebars (space ^^ (align (separate_map (semi_sp ^^ break 1) (doc_fexp regtypes recordtyp) fexps)) ^^ space) in if aexp_needed then parens epp else epp | E_record_update(e,(FES_aux(FES_Fexps(fexps,_),_))) -> let (Base ((_,{t = t}),_,_,_,_,_)) = annot in let recordtyp = match t with | Tid recordtyp | Tabbrev ({t = Tid recordtyp},_) -> recordtyp | _ -> raise (report l "cannot get record type") in anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp regtypes recordtyp) fexps)) | E_vector exps -> (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 dir,dir_out = match order.order with | Oinc -> true,"true" | _ -> false, "false" in let start = match start.nexp with | Nconst i -> string_of_big_int i | N2n(_,Some i) -> string_of_big_int i | _ -> if dir then "0" else string_of_int (List.length exps) in let expspp = match exps with | [] -> empty | e :: es -> let (expspp,_) = List.fold_left (fun (pp,count) e -> (pp ^^ semi ^^ (if count = 20 then break 0 else empty) ^^ expN e), if count = 20 then 0 else count + 1) (expN e,0) es in align (group expspp) in let epp = group (separate space [string "Vector"; brackets expspp;string start;string dir_out]) in if aexp_needed then parens (align epp) else epp ) | E_vector_indexed (iexps, (Def_val_aux (default,(dl,dannot)))) -> let (Base((_,t),_,_,_,_,_)) = annot in let call = string "make_indexed_vector" in let (start,len,order) = match t.t with | Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _]) | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _])}) | Tapp("reg", [TA_typ {t =Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; _])}]) -> (start,len,order.order) in let dir,dir_out = match order with | Oinc -> true,"true" | _ -> false, "false" in let start = match start.nexp with | Nconst i | N2n(_,Some i)-> string_of_big_int i | N2n({nexp=Nconst i},_) -> string_of_int (Util.power 2 (int_of_big_int i)) | _ -> if dir then "0" else string_of_int (List.length iexps) in let size = match len.nexp with | Nconst i | N2n(_,Some i)-> string_of_big_int i | N2n({nexp=Nconst i},_) -> string_of_int (Util.power 2 (int_of_big_int i)) in let default_string = match default with | Def_val_empty -> if is_bit_vector t then string "BU" else failwith "E_vector_indexed of non-bitvector type without default argument" | Def_val_dec e -> let (Base ((_,{t = t}),_,_,_,_,_)) = dannot in match t with | Tapp ("register", [TA_typ ({t = rt})]) -> let n = match rt with | Tapp ("vector",TA_nexp {nexp = Nconst i} :: TA_nexp {nexp = Nconst j} ::_) -> abs_big_int (sub_big_int i j) | _ -> raise ((Reporting_basic.err_unreachable dl) ("not the right type information available to construct "^ "undefined register")) in parens (string ("UndefinedRegister " ^ string_of_big_int n)) | _ -> expY e in let iexp (i,e) = parens (doc_int i ^^ comma ^^ expN e) in let expspp = match iexps with | [] -> empty | e :: es -> let (expspp,_) = List.fold_left (fun (pp,count) e -> (pp ^^ semi ^^ (if count = 5 then break 1 else empty) ^^ iexp e), if count = 5 then 0 else count + 1) (iexp e,0) es in align (expspp) in let epp = align (group (call ^//^ brackets expspp ^/^ separate space [default_string;string start;string size;string dir_out])) in if aexp_needed then parens (align epp) else epp | E_vector_update(v,e1,e2) -> let epp = separate space [string "update_pos";expY v;expY e1;expY e2] in if aexp_needed then parens (align epp) else epp | E_vector_update_subrange(v,e1,e2,e3) -> let epp = align (string "update" ^//^ group (group (expY v) ^/^ group (expY e1) ^/^ group (expY e2)) ^/^ group (expY e3)) in if aexp_needed then parens (align epp) else epp | E_list exps -> brackets (separate_map semi (expN) exps) | E_case(e,pexps) -> let only_integers (E_aux(_,(_,annot)) as e) = match annot with | Base((_,t),_,_,_,_,_) -> if is_number t then let e_pp = expY e in align (string "toNatural" ^//^ e_pp) else (match t with | {t = Ttup ([t1;t2;t3;t4;t5] as ts)} when List.for_all is_number ts -> let e_pp = expY e in align (string "toNaturalFiveTup" ^//^ e_pp) | _ -> expY e) | _ -> expY e in (* This is a hack, incomplete. It's because lem does not allow pattern-matching on integers *) let epp = group ((separate space [string "match"; only_integers e; string "with"]) ^/^ (separate_map (break 1) (doc_case regtypes) pexps) ^/^ (string "end")) in if aexp_needed then parens (align epp) else align epp | E_exit e -> separate space [string "exit"; expY e;] | E_assert (e1,e2) -> let epp = separate space [string "assert'"; expY e1; expY e2] in if aexp_needed then parens (align epp) else align epp | E_app_infix (e1,id,e2) -> (match annot with | Base((_,t),External(Some name),_,_,_,_) -> let argpp arg = let (E_aux (_,(_,Base((_,{t=t}),_,_,_,_,_)))) = arg in match t with | Tapp("vector",_) -> parens (concat [string "reset_vector_start";space;expY arg]) | _ -> expY arg in let epp = let aux name = align (argpp e1 ^^ space ^^ string name ^//^ argpp e2) in let aux2 name = align (string name ^//^ argpp e1 ^/^ argpp e2) in align (match name with | "power" -> aux2 "pow" | "bitwise_and_bit" -> aux "&." | "bitwise_or_bit" -> aux "|." | "bitwise_xor_bit" -> aux "+." | "add" -> aux "+" | "minus" -> aux "-" | "multiply" -> aux "*" | "quot" -> aux2 "quot" | "quot_signed" -> aux2 "quot" | "modulo" -> aux2 "modulo" | "add_vec" -> aux2 "add_VVV" | "add_vec_signed" -> aux2 "addS_VVV" | "add_overflow_vec" -> aux2 "addO_VVV" | "add_overflow_vec_signed" -> aux2 "addSO_VVV" | "minus_vec" -> aux2 "minus_VVV" | "minus_overflow_vec" -> aux2 "minusO_VVV" | "minus_overflow_vec_signed" -> aux2 "minusSO_VVV" | "multiply_vec" -> aux2 "mult_VVV" | "multiply_vec_signed" -> aux2 "multS_VVV" | "mult_overflow_vec" -> aux2 "multO_VVV" | "mult_overflow_vec_signed" -> aux2 "multSO_VVV" | "quot_vec" -> aux2 "quot_VVV" | "quot_vec_signed" -> aux2 "quotS_VVV" | "quot_overflow_vec" -> aux2 "quotO_VVV" | "quot_overflow_vec_signed" -> aux2 "quotSO_VVV" | "mod_vec" -> aux2 "mod_VVV" | "add_vec_range" -> aux2 "add_VIV" | "add_vec_range_signed" -> aux2 "addS_VIV" | "minus_vec_range" -> aux2 "minus_VIV" | "mult_vec_range" -> aux2 "mult_VIV" | "mult_vec_range_signed" -> aux2 "multS_VIV" | "mod_vec_range" -> aux2 "minus_VIV" | "add_range_vec" -> aux2 "add_IVV" | "add_range_vec_signed" -> aux2 "addS_IVV" | "minus_range_vec" -> aux2 "minus_IVV" | "mult_range_vec" -> aux2 "mult_IVV" | "mult_range_vec_signed" -> aux2 "multS_IVV" | "add_range_vec_range" -> aux2 "add_IVI" | "add_range_vec_range_signed" -> aux2 "addS_IVI" | "minus_range_vec_range" -> aux2 "minus_IVI" | "add_vec_range_range" -> aux2 "add_VII" | "add_vec_range_range_signed" -> aux2 "addS_VII" | "minus_vec_range_range" -> aux2 "minus_VII" | "add_vec_vec_range" -> aux2 "add_VVI" | "add_vec_vec_range_signed" -> aux2 "addS_VVI" | "add_vec_bit" -> aux2 "add_VBV" | "add_vec_bit_signed" -> aux2 "addS_VBV" | "add_overflow_vec_bit_signed" -> aux2 "addSO_VBV" | "minus_vec_bit_signed" -> aux2 "minus_VBV" | "minus_overflow_vec_bit" -> aux2 "minusO_VBV" | "minus_overflow_vec_bit_signed" -> aux2 "minusSO_VBV" | _ -> string name ^//^ parens (expN e1 ^^ comma ^/^ expN e2)) in if aexp_needed then parens (align epp) else epp | _ -> let epp = align (doc_id_lem id ^//^ parens (expN e1 ^^ comma ^/^ expN e2)) in if aexp_needed then parens (align epp) else epp) | E_internal_let(lexp, eq_exp, in_exp) -> raise (report l "E_internal_lets should have been removed till now") (* (separate space [string "let internal"; (match lexp with (LEXP_aux ((LEXP_id id | LEXP_cast (_,id)),_)) -> doc_id_lem id); coloneq; exp eq_exp; string "in"]) ^/^ exp in_exp *) | E_internal_plet (pat,e1,e2) -> let epp = let b = match e1 with E_aux (E_if _,_) -> true | _ -> false in match pat with | P_aux (P_wild,_) -> (separate space [expV b e1; string ">>"]) ^^ hardline ^^ expN e2 | _ -> (separate space [expV b e1; string ">>= fun"; doc_pat_lem regtypes true pat;arrow]) ^^ hardline ^^ expN e2 in if aexp_needed then parens (align epp) else epp | E_internal_return (e1) -> separate space [string "return"; expY e1;] and let_exp regtypes (LB_aux(lb,_)) = match lb with | LB_val_explicit(_,pat,e) | LB_val_implicit(pat,e) -> prefix 2 1 (separate space [string "let"; doc_pat_lem regtypes true pat; equals]) (top_exp regtypes false e) and doc_fexp regtypes recordtyp (FE_aux(FE_Fexp(id,e),_)) = let fname = if prefix_recordtype then (string (recordtyp ^ "_")) ^^ doc_id_lem id else doc_id_lem id in group (doc_op equals fname (top_exp regtypes true e)) and doc_case regtypes (Pat_aux(Pat_exp(pat,e),_)) = group (prefix 3 1 (separate space [pipe; doc_pat_lem regtypes false pat;arrow]) (group (top_exp regtypes false e))) and doc_lexp_deref_lem regtypes ((LEXP_aux(lexp,(l,annot))) as le) = match lexp with | LEXP_field (le,id) -> parens (separate empty [doc_lexp_deref_lem regtypes le;dot;doc_id_lem id]) | LEXP_vector(le,e) -> parens ((separate space) [string "access";doc_lexp_deref_lem regtypes le; top_exp regtypes true e]) | LEXP_id id -> doc_id_lem id | LEXP_cast (typ,id) -> doc_id_lem id | _ -> raise (Reporting_basic.err_unreachable l ("doc_lexp_deref_lem: Shouldn't happen")) (* expose doc_exp_lem and doc_let *) in top_exp, let_exp (*TODO Upcase and downcase type and constructors as needed*) let doc_type_union_lem regtypes (Tu_aux(typ_u,_)) = match typ_u with | Tu_ty_id(typ,id) -> separate space [pipe; doc_id_lem_ctor id; string "of"; parens (doc_typ_lem regtypes typ)] | Tu_id id -> separate space [pipe; doc_id_lem_ctor id] let rec doc_range_lem (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_lem regtypes (TD_aux(td,_)) = match td with | TD_abbrev(id,nm,typschm) -> doc_op equals (concat [string "type"; space; doc_id_lem_type id]) (doc_typschm_lem regtypes typschm) | TD_record(id,nm,typq,fs,_) -> let f_pp (typ,fid) = let fname = if prefix_recordtype then concat [doc_id_lem id;string "_";doc_id_lem_type fid;] else doc_id_lem_type fid in concat [fname;space;colon;space;doc_typ_lem regtypes typ; semi] in let fs_doc = group (separate_map (break 1) f_pp fs) in doc_op equals (concat [string "type"; space; doc_id_lem_type id;]) (doc_typquant_lem typq (anglebars (space ^^ align fs_doc ^^ space))) | TD_variant(id,nm,typq,ar,_) -> (match id with | Id_aux ((Id "read_kind"),_) -> empty | Id_aux ((Id "write_kind"),_) -> empty | Id_aux ((Id "barrier_kind"),_) -> empty | Id_aux ((Id "instruction_kind"),_) -> empty | Id_aux ((Id "regfp"),_) -> empty | Id_aux ((Id "niafp"),_) -> empty | Id_aux ((Id "diafp"),_) -> empty | _ -> let ar_doc = group (separate_map (break 1) (doc_type_union_lem regtypes) ar) in let typ_pp = (doc_op equals) (concat [string "type"; space; doc_id_lem_type id;]) (doc_typquant_lem typq ar_doc) in let make_id pat id = separate space [string "SIA.Id_aux"; parens (string "SIA.Id " ^^ string_lit (doc_id id)); if pat then underscore else string "SIA.Unknown"] in let fromInterpValueF = concat [doc_id_lem_type id;string "FromInterpValue"] in let toInterpValueF = concat [doc_id_lem_type id;string "ToInterpValue"] in let fromInterpValuePP = (prefix 2 1) (separate space [string "let rec";fromInterpValueF;string "v";equals;string "match v with"]) ( ((separate_map (break 1)) (fun (Tu_aux (tu,_)) -> match tu with | Tu_ty_id (ty,cid) -> (separate space) [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v"; arrow; doc_id_lem_ctor cid; parens (string "fromInterpValue v")] | Tu_id cid -> (separate space) [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v"; arrow; doc_id_lem_ctor cid]) ar) ^/^ ((separate space) [pipe;string "SI.V_tuple [v]";arrow;fromInterpValueF;string "v"]) ^/^ let failmessage = (string_lit (concat [string "fromInterpValue";space;doc_id_lem_type id;colon;space;string "unexpected value. ";])) ^^ (string " ^ Interp.debug_print_value v") in ((separate space) [pipe;string "v";arrow;string "failwith";parens failmessage]) ^/^ string "end") in let toInterpValuePP = (prefix 2 1) (separate space [string "let";toInterpValueF;equals;string "function"]) ( ((separate_map (break 1)) (fun (Tu_aux (tu,_)) -> match tu with | Tu_ty_id (ty,cid) -> (separate space) [pipe;doc_id_lem_ctor cid;string "v";arrow; string "SI.V_ctor"; parens (make_id false cid); parens (string "SIA.T_id " ^^ string_lit (doc_id id)); string "SI.C_Union"; parens (string "toInterpValue v")] | Tu_id cid -> (separate space) [pipe;doc_id_lem_ctor cid;arrow; string "SI.V_ctor"; parens (make_id false cid); parens (string "SIA.T_id " ^^ string_lit (doc_id id)); string "SI.C_Union"; parens (string "toInterpValue ()")]) ar) ^/^ string "end") in let fromToInterpValuePP = ((prefix 2 1) (concat [string "instance ";parens (string "ToFromInterpValue " ^^ doc_id_lem_type id)]) (concat [string "let toInterpValue = ";toInterpValueF;hardline; string "let fromInterpValue = ";fromInterpValueF])) ^/^ string "end" in typ_pp ^^ hardline ^^ hardline ^^ if !print_to_from_interp_value then toInterpValuePP ^^ hardline ^^ hardline ^^ fromInterpValuePP ^^ hardline ^^ hardline ^^ fromToInterpValuePP ^^ hardline else empty) | TD_enum(id,nm,enums,_) -> (match id with | Id_aux ((Id "read_kind"),_) -> empty | Id_aux ((Id "write_kind"),_) -> empty | Id_aux ((Id "barrier_kind"),_) -> empty | Id_aux ((Id "instruction_kind"),_) -> empty | _ -> let rec range i j = if i > j then [] else i :: (range (i+1) j) in let nats = range 0 in let enums_doc = group (separate_map (break 1 ^^ pipe ^^ space) doc_id_lem_ctor enums) in let typ_pp = (doc_op equals) (concat [string "type"; space; doc_id_lem_type id;]) (enums_doc) in let fromInterpValueF = concat [doc_id_lem_type id;string "FromInterpValue"] in let toInterpValueF = concat [doc_id_lem_type id;string "ToInterpValue"] in let make_id pat id = separate space [string "SIA.Id_aux"; parens (string "SIA.Id " ^^ string_lit (doc_id id)); if pat then underscore else string "SIA.Unknown"] in let fromInterpValuePP = (prefix 2 1) (separate space [string "let rec";fromInterpValueF;string "v";equals;string "match v with"]) ( ((separate_map (break 1)) (fun (cid) -> (separate space) [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v"; arrow;doc_id_lem_ctor cid] ) enums ) ^/^ ( (align ((prefix 3 1) (separate space [pipe;string ("SI.V_lit (SIA.L_aux (SIA.L_num n) _)");arrow]) (separate space [string "match";parens(string "natFromInteger n");string "with"] ^/^ ( ((separate_map (break 1)) (fun (cid,number) -> (separate space) [pipe;string (string_of_int number);arrow;doc_id_lem_ctor cid] ) (List.combine enums (nats ((List.length enums) - 1))) ) ^/^ string "end" ) ) ) ) ) ^/^ ((separate space) [pipe;string "SI.V_tuple [v]";arrow;fromInterpValueF;string "v"]) ^/^ let failmessage = (string_lit (concat [string "fromInterpValue";space;doc_id_lem_type id;colon;space;string "unexpected value. ";])) ^^ (string " ^ Interp.debug_print_value v") in ((separate space) [pipe;string "v";arrow;string "failwith";parens failmessage]) ^/^ string "end") in let toInterpValuePP = (prefix 2 1) (separate space [string "let";toInterpValueF;equals;string "function"]) ( ((separate_map (break 1)) (fun (cid,number) -> (separate space) [pipe;doc_id_lem_ctor cid;arrow; string "SI.V_ctor"; parens (make_id false cid); parens (string "SIA.T_id " ^^ string_lit (doc_id id)); parens (string ("SI.C_Enum " ^ string_of_int number)); parens (string "toInterpValue ()")]) (List.combine enums (nats ((List.length enums) - 1)))) ^/^ string "end") in let fromToInterpValuePP = ((prefix 2 1) (concat [string "instance ";parens (string "ToFromInterpValue " ^^ doc_id_lem_type id)]) (concat [string "let toInterpValue = ";toInterpValueF;hardline; string "let fromInterpValue = ";fromInterpValueF])) ^/^ string "end" in typ_pp ^^ hardline ^^ hardline ^^ if !print_to_from_interp_value then toInterpValuePP ^^ hardline ^^ hardline ^^ fromInterpValuePP ^^ hardline ^^ hardline ^^ fromToInterpValuePP ^^ hardline else empty) | TD_register(id,n1,n2,rs) -> match n1,n2 with | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) -> let doc_rid (r,id) = parens (separate comma_sp [string_lit (doc_id_lem id); doc_range_lem r;]) in let doc_rids = group (separate_map (semi ^^ (break 1)) doc_rid rs) in (*let doc_rfield (_,id) = (doc_op equals) (string "let" ^^ space ^^ doc_id_lem id) (string "Register_field" ^^ space ^^ string_lit(doc_id_lem id)) in*) let dir_b = i1 < i2 in let dir = string (if dir_b then "true" else "false") in let size = if dir_b then i2-i1 +1 else i1-i2 + 1 in (doc_op equals) (concat [string "let";space;string "build_";doc_id_lem id;space;string "regname"]) (string "Register" ^^ space ^^ align (separate space [string "regname"; doc_int size; doc_int i1; dir; break 0 ^^ brackets (align doc_rids)])) (*^^ hardline ^^ separate_map hardline doc_rfield rs *) let doc_rec_lem (Rec_aux(r,_)) = match r with | Rec_nonrec -> space | Rec_rec -> space ^^ string "rec" ^^ space let doc_tannot_opt_lem regtypes (Typ_annot_opt_aux(t,_)) = match t with | Typ_annot_opt_some(tq,typ) -> doc_typquant_lem tq (doc_typ_lem regtypes typ) let doc_funcl_lem regtypes (FCL_aux(FCL_Funcl(id,pat,exp),_)) = group (prefix 3 1 ((doc_pat_lem regtypes false pat) ^^ space ^^ arrow) (doc_exp_lem regtypes false exp)) let get_id = function | [] -> failwith "FD_function with empty list" | (FCL_aux (FCL_Funcl (id,_,_),_))::_ -> id module StringSet = Set.Make(String) let rec doc_fundef_lem regtypes (FD_aux(FD_function(r, typa, efa, fcls),fannot)) = match fcls with | [] -> failwith "FD_function with empty function list" | [FCL_aux (FCL_Funcl(id,pat,exp),_)] -> (prefix 2 1) ((separate space) [(string "let") ^^ (doc_rec_lem r) ^^ (doc_id_lem id); (doc_pat_lem regtypes true pat); equals]) (doc_exp_lem regtypes false exp) | _ -> let id = get_id fcls in (* let sep = hardline ^^ pipe ^^ space in *) match id with | Id_aux (Id fname,idl) when fname = "execute" || fname = "initial_analysis" -> let (_,auxiliary_functions,clauses) = List.fold_left (fun (already_used_fnames,auxiliary_functions,clauses) funcl -> match funcl with | FCL_aux (FCL_Funcl (Id_aux (Id _,l),pat,exp),annot) -> let (P_aux (P_app (Id_aux (Id ctor,l),argspat),pannot)) = pat in let rec pick_name_not_clashing_with already_used candidate = if StringSet.mem candidate already_used then pick_name_not_clashing_with already_used (candidate ^ "'") else candidate in let aux_fname = pick_name_not_clashing_with already_used_fnames (fname ^ "_" ^ ctor) in let already_used_fnames = StringSet.add aux_fname already_used_fnames in let fcl = FCL_aux (FCL_Funcl (Id_aux (Id aux_fname,l), P_aux (P_tup argspat,pannot),exp),annot) in let auxiliary_functions = auxiliary_functions ^^ hardline ^^ hardline ^^ doc_fundef_lem regtypes (FD_aux (FD_function(r,typa,efa,[fcl]),fannot)) in let clauses = clauses ^^ (break 1) ^^ (separate space [pipe;doc_pat_lem regtypes false pat;arrow; string aux_fname; doc_pat_lem regtypes true (P_aux (P_tup argspat, pannot))]) in (already_used_fnames,auxiliary_functions,clauses) ) (StringSet.empty,empty,empty) fcls in auxiliary_functions ^^ hardline ^^ hardline ^^ (prefix 2 1) ((separate space) [string "let" ^^ doc_rec_lem r ^^ doc_id_lem id;equals;string "function"]) (clauses ^/^ string "end") | _ -> let clauses = (separate_map (break 1)) (fun fcl -> separate space [pipe;doc_funcl_lem regtypes fcl]) fcls in (prefix 2 1) ((separate space) [string "let" ^^ doc_rec_lem r ^^ doc_id_lem id;equals;string "function"]) (clauses ^/^ string "end") let doc_dec_lem (DEC_aux (reg,(l,annot))) = match reg with | 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])}]) | Tapp("register", [TA_typ {t= Tabbrev(_,{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 "true" else "false" in (doc_op equals) (string "let" ^^ space ^^ doc_id_lem id) (string "Register" ^^ space ^^ align (separate space [string_lit(doc_id_lem id); doc_int (int_of_big_int size); doc_int (int_of_big_int start); string o; string "[]"])) ^/^ hardline | _ -> let (Id_aux (Id name,_)) = id in failwith ("can't deal with register " ^ name)) | Tapp("register", [TA_typ {t=Tid idt}]) | Tid idt | Tabbrev( {t= Tid idt}, _) -> separate space [string "let";doc_id_lem id;equals; string "build_" ^^ string idt;string_lit (doc_id_lem id)] ^/^ hardline |_-> empty) | _ -> empty) | DEC_alias(id,alspec) -> empty | DEC_typ_alias(typ,id,alspec) -> empty let doc_spec_lem regtypes (VS_aux (valspec,annot)) = match valspec with | VS_extern_no_rename _ | VS_extern_spec _ -> empty (* ignore these at the moment *) | VS_val_spec (typschm,id) -> empty (* separate space [string "val"; doc_id_lem id; string ":";doc_typschm_lem regtypes typschm] ^/^ hardline *) let rec doc_def_lem regtypes def = match def with | DEF_spec v_spec -> (doc_spec_lem regtypes v_spec,empty) | DEF_type t_def -> (group (doc_typdef_lem regtypes t_def) ^/^ hardline,empty) | DEF_reg_dec dec -> (group (doc_dec_lem dec),empty) | DEF_default df -> (empty,empty) | DEF_fundef f_def -> (empty,group (doc_fundef_lem regtypes f_def) ^/^ hardline) | DEF_val lbind -> (empty,group (doc_let_lem regtypes lbind) ^/^ hardline) | DEF_scattered sdef -> failwith "doc_def_lem: shoulnd't have DEF_scattered at this point" | DEF_kind _ -> (empty,empty) | DEF_comm (DC_comm s) -> (empty,comment (string s)) | DEF_comm (DC_comm_struct d) -> let (typdefs,vdefs) = doc_def_lem regtypes d in (empty,comment (typdefs ^^ hardline ^^ vdefs)) let doc_defs_lem regtypes (Defs defs) = let (typdefs,valdefs) = List.split (List.map (doc_def_lem regtypes) defs) in (separate empty typdefs,separate empty valdefs) let find_regtypes (Defs defs) = List.fold_left (fun acc def -> match def with | DEF_type (TD_aux(TD_register (Id_aux (Id tname, _),_,_,_),_)) -> tname :: acc | _ -> acc ) [] defs let typ_to_t env = Type_check.typ_to_t env false false let pp_defs_lem (types_file,types_modules) (prompt_file,prompt_modules) (state_file,state_modules) d top_line = let regtypes = find_regtypes d in let (typdefs,valdefs) = doc_defs_lem regtypes d in (print types_file) (concat [string "(*" ^^ (string top_line) ^^ string "*)";hardline; (separate_map hardline) (fun lib -> separate space [string "open import";string lib]) types_modules;hardline; if !print_to_from_interp_value then concat [(separate_map hardline) (fun lib -> separate space [string " import";string lib]) ["Interp";"Interp_ast"]; string "open import Deep_shallow_convert"; hardline; hardline; string "module SI = Interp"; hardline; string "module SIA = Interp_ast"; hardline; hardline] else empty; typdefs]); (print prompt_file) (concat [string "(*" ^^ (string top_line) ^^ string "*)";hardline; (separate_map hardline) (fun lib -> separate space [string "open import";string lib]) prompt_modules;hardline; hardline; valdefs]); (print state_file) (concat [string "(*" ^^ (string top_line) ^^ string "*)";hardline; (separate_map hardline) (fun lib -> separate space [string "open import";string lib]) state_modules;hardline; hardline; valdefs]);