diff options
| author | Gabriel Kerneis | 2014-05-20 15:10:25 +0100 |
|---|---|---|
| committer | Gabriel Kerneis | 2014-05-20 15:10:25 +0100 |
| commit | 0fc4488f471f701cf0f5b20899da89dcd79b618f (patch) | |
| tree | b8714591cdcb1306ad868b3a4222eab761caad7d /src/pretty_print.ml | |
| parent | 5ad43e6a9ffd677c3ba1b381de00027f8c272e2c (diff) | |
Remove legacy pretty printer
Diffstat (limited to 'src/pretty_print.ml')
| -rw-r--r-- | src/pretty_print.ml | 351 |
1 files changed, 6 insertions, 345 deletions
diff --git a/src/pretty_print.ml b/src/pretty_print.ml index e728e8a9..d37aeab9 100644 --- a/src/pretty_print.ml +++ b/src/pretty_print.ml @@ -2,21 +2,9 @@ open Type_internal open Ast open Format -let is_atomic_typ (Typ_aux(t,_)) = - match t with - | Typ_id _ | Typ_var _ | Typ_tup _ -> true - | _ -> false -let is_atomic_nexp (Nexp_aux(n,_)) = - match n with - | Nexp_var _ | Nexp_constant _ | Nexp_exp _ -> true - | _ -> false - -let is_atomic_pat (P_aux(p,l)) = - match p with - | P_lit(_) | P_wild | P_id(_) | P_as _ | P_typ _ -> true - | P_app(_,pats) -> if (pats = []) then true else false - | P_record(_,_) | P_vector(_) | P_vector_indexed(_) | P_tup(_) | P_list(_) -> true - | _ -> false +(**************************************************************************** + * annotated source to Lem ast pretty printer +****************************************************************************) let rec list_format (sep : string) (fmt : 'a -> string) (ls : 'a list) : string = match ls with @@ -34,342 +22,13 @@ let rec list_pp i_format l_format = let kwd ppf s = fprintf ppf "%s" s let base ppf s = fprintf ppf "%s" s -let parens is_atomic to_base v = - if (is_atomic v) then to_base v - else "(" ^ to_base v ^ ")" - -let pp_parens is_atomic format = - fun ppf v -> - if (is_atomic v) - then format ppf v - else fprintf ppf "%a %a %a" kwd "(" format v kwd ")" - -(**************************************************************************** - * source to source pretty printer -****************************************************************************) - let pp_format_id (Id_aux(i,_)) = match i with | Id(i) -> i | DeIid(x) -> "(deinfix " ^ x ^ ")" -let pp_id ppf id = base ppf (pp_format_id id) - let pp_format_var (Kid_aux(Var v,_)) = v -let pp_var ppf var = base ppf (pp_format_var var) - -let pp_format_bkind (BK_aux(k,_)) = - match k with - | BK_type -> "Type" - | BK_nat -> "Nat" - | BK_order -> "Order" - | BK_effect -> "Effect" - -let pp_bkind ppf bk = base ppf (pp_format_bkind bk) - -let pp_format_kind (K_aux(K_kind(klst),_)) = - list_format " -> " pp_format_bkind klst - -let pp_kind ppf k = base ppf (pp_format_kind k) - -let rec pp_format_typ (Typ_aux(t,_)) = - match t with - | Typ_id(id) -> pp_format_id id - | Typ_var(var) -> pp_format_var var - | Typ_wild -> "_" - | Typ_fn(arg,ret,efct) -> "(" ^ (parens is_atomic_typ pp_format_typ arg) ^ " -> " ^ - (parens is_atomic_typ pp_format_typ ret) ^ " effect " ^ - (pp_format_effects efct) ^ ")" - | Typ_tup(typs) -> "(" ^ (list_format " * " pp_format_typ typs) ^ ")" - | Typ_app(id,args) -> (pp_format_id id) ^ "<" ^ (list_format ", " pp_format_typ_arg args) ^ ">" -and pp_format_nexp (Nexp_aux(n,_)) = - match n with - | Nexp_var(var) -> pp_format_var var - | Nexp_constant(i) -> string_of_int i - | Nexp_sum(n1,n2) -> "(" ^ (pp_format_nexp n1) ^ " + " ^ (pp_format_nexp n2) ^ ")" - | Nexp_times(n1,n2) -> "(" ^ (pp_format_nexp n1) ^ " * " ^ (pp_format_nexp n2) ^ ")" - | Nexp_exp(n1) -> "2** (" ^ (pp_format_nexp n1) ^ ")" - | Nexp_neg(n1) -> "(* - *)" ^ (pp_format_nexp n1) -and pp_format_ord (Ord_aux(o,_)) = - match o with - | Ord_var(var) -> pp_format_var var - | Ord_inc -> "inc" - | Ord_dec -> "dec" -and pp_format_effects (Effect_aux(e,_)) = - match e with - | Effect_var(var) -> pp_format_var var - | Effect_set(efcts) -> - if (efcts = []) - then "pure" - else "{" ^ - (list_format "," - (fun (BE_aux(e,l)) -> - match e with - | BE_rreg -> "rreg" - | BE_wreg -> "wreg" - | BE_rmem -> "rmem" - | BE_wmem -> "wmem" - | BE_undef -> "undef" - | BE_unspec -> "unspec" - | BE_nondet -> "nondet") - efcts) ^ " }" -and pp_format_typ_arg (Typ_arg_aux(t,_)) = - match t with - | Typ_arg_typ(t) -> pp_format_typ t - | Typ_arg_nexp(n) -> pp_format_nexp n - | Typ_arg_order(o) -> pp_format_ord o - | Typ_arg_effect(e) -> pp_format_effects e - -let pp_typ ppf t = base ppf (pp_format_typ t) -let pp_nexp ppf n = base ppf (pp_format_nexp n) -let pp_ord ppf o = base ppf (pp_format_ord o) -let pp_effects ppf e = base ppf (pp_format_effects e) - -let pp_format_nexp_constraint (NC_aux(nc,_)) = - match nc with - | NC_fixed(n1,n2) -> pp_format_nexp n1 ^ " = " ^ pp_format_nexp n2 - | NC_bounded_ge(n1,n2) -> pp_format_nexp n1 ^ " >= " ^ pp_format_nexp n2 - | NC_bounded_le(n1,n2) -> pp_format_nexp n1 ^ " <= " ^ pp_format_nexp n2 - | NC_nat_set_bounded(var,bounds) -> - pp_format_var var ^ - " IN {" ^ - list_format ", " string_of_int bounds ^ - "}" - -let pp_nexp_constraint ppf nc = base ppf (pp_format_nexp_constraint nc) - -let pp_format_qi (QI_aux(qi,_)) = - match qi with - | QI_const(n_const) -> pp_format_nexp_constraint n_const - | QI_id(KOpt_aux(ki,_)) -> - (match ki with - | KOpt_none(var) -> pp_format_var var - | KOpt_kind(k,var) -> pp_format_kind k ^ " " ^ pp_format_var var) - -let pp_qi ppf qi = base ppf (pp_format_qi qi) - -let pp_format_typquant (TypQ_aux(tq,_)) = - match tq with - | TypQ_no_forall -> "" - | TypQ_tq(qlist) -> - "forall " ^ - (list_format ", " pp_format_qi qlist) ^ - ". " - -let pp_typquant ppf tq = base ppf (pp_format_typquant tq) - -let pp_format_typscm (TypSchm_aux(TypSchm_ts(tq,t),_)) = - (pp_format_typquant tq) ^ pp_format_typ t - -let pp_typscm ppf ts = base ppf (pp_format_typscm ts) - -let pp_format_lit (L_aux(l,_)) = - 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 pp_lit ppf l = base ppf (pp_format_lit l) - -let rec pp_format_pat (P_aux(p,l)) = - match p with - | P_lit(lit) -> pp_format_lit lit - | P_wild -> "_" - | P_id(id) -> pp_format_id id - | P_as(pat,id) -> "(" ^ pp_format_pat pat ^ " as " ^ pp_format_id id ^ ")" - | P_typ(typ,pat) -> "(" ^ pp_format_typ typ ^ ") " ^ pp_format_pat pat - | P_app(id,pats) -> if (pats = []) - then pp_format_id id - else pp_format_id id ^ "(" ^ - list_format ", " (parens is_atomic_pat pp_format_pat) pats ^ ")" - | P_record(fpats,_) -> "{" ^ - list_format "; " (fun (FP_aux(FP_Fpat(id,fpat),_)) -> - pp_format_id id ^ " = " ^ pp_format_pat fpat) fpats - ^ "}" - | P_vector(pats) -> "[" ^ list_format "; " (parens is_atomic_pat pp_format_pat) pats ^ "]" - | P_vector_indexed(ipats) -> - "[" ^ list_format "; " (fun (i,p) -> string_of_int i ^ " = " ^ pp_format_pat p) ipats ^ "]" - | P_vector_concat(pats) -> list_format " ^ " pp_format_pat pats - | P_tup(pats) -> "(" ^ (list_format ", " (parens is_atomic_pat pp_format_pat) pats) ^ ")" - | P_list(pats) -> "[||" ^ (list_format "; " (parens is_atomic_pat pp_format_pat) pats) ^ "||]" - -let pp_pat ppf p = base ppf (pp_format_pat p) -let pp_pat_atomic ppf p = base ppf (parens is_atomic_pat pp_format_pat p) - -let rec pp_let ppf (LB_aux(lb,_)) = - match lb with - | LB_val_explicit(ts,pat,exp) -> fprintf ppf "@[<0>%a %a %a %a@ %a@]" kwd "let" pp_typscm ts pp_pat_atomic pat kwd " =" pp_exp exp - | LB_val_implicit(pat,exp) -> fprintf ppf "@[<0>%a %a %a@ %a@]" kwd "let" pp_pat_atomic pat kwd " =" pp_exp exp - -(* Need an is_atomic? check and insert parens otherwise *) -and pp_exp ppf (E_aux(e,(_,annot))) = - match e with - | E_block(exps) -> fprintf ppf "@[<0>%a%a@ %a@]" - kwd "{" - (list_pp pp_semi_exp pp_exp) exps - kwd "}" - | E_id(id) -> pp_id ppf id - | E_lit(lit) -> pp_lit ppf lit - | E_cast(typ,exp) -> fprintf ppf "@[<0>%a%a%a %a@]" kwd "(" pp_typ typ kwd ")" pp_exp exp - | E_internal_cast((_,NoTyp),e) -> pp_exp ppf e - | E_internal_cast((_,Base((_,t),_,_,_)), (E_aux(_,(_,eannot)) as exp)) -> - (match t.t,eannot with - | Tapp("vector",[TA_nexp n1;_;_;_]),Base((_,{t=Tapp("vector",[TA_nexp n2;_;_;_])}),_,_,_) -> - if nexp_eq n1 n2 - then pp_exp ppf exp - else - fprintf ppf "@[<0>%a%a%a %a@]" kwd "(" pp_typ (t_to_typ t) kwd ")" pp_exp exp - | _ -> fprintf ppf "@[<0>%a%a%a %a@]" kwd "(" pp_typ (t_to_typ t) kwd ")" pp_exp exp) - | E_app(f,args) -> fprintf ppf "@[<0>%a(%a)@]" pp_id f (list_pp pp_comma_exp pp_exp) args - | E_app_infix(l,op,r) -> fprintf ppf "@[<0>%a %a %a@]" pp_exp l pp_id op pp_exp r - | E_tuple(exps) -> fprintf ppf "@[<0>%a %a %a@]" kwd "(" (list_pp pp_comma_exp pp_exp) exps kwd ")" - | E_if(c,t,e) -> fprintf ppf "@[<0>%a %a @[<1>%a %a@] @[<1>%a@ %a@]@]" kwd "if " pp_exp c kwd "then" pp_exp t kwd "else" pp_exp e - | E_for(id,exp1,exp2,exp3,order,exp4) -> - fprintf ppf "@[<0> %a %a (%a %a %a %a %a %a %a %a)@ @[<1>%a@]@]" - kwd "foreach " pp_id id kwd "from " pp_exp exp1 kwd " to " pp_exp exp2 kwd "by " pp_exp exp3 kwd "in" pp_ord order pp_exp exp4 - | E_vector(exps) -> fprintf ppf "@[<0>%a%a%a@]" kwd "[" (list_pp pp_comma_exp pp_exp) exps kwd "]" - | E_vector_indexed(iexps,default) -> - let iformat ppf (i,e) = fprintf ppf "@[<1>%i%a %a%a@]" i kwd " = " pp_exp e kwd "," in - let lformat ppf (i,e) = fprintf ppf "@[<1>%i%a %a@]" i kwd " = " pp_exp e in - fprintf ppf "@[<0> %a%a%a@]" kwd "[" (list_pp iformat lformat) iexps kwd "]" - | E_vector_access(v,e) -> fprintf ppf "@[<0>%a%a%a%a@]" pp_exp v kwd "[" pp_exp e kwd "]" - | E_vector_subrange(v,e1,e2) -> fprintf ppf "@[<0>%a%a%a%a%a%a@]" pp_exp v kwd "[" pp_exp e1 kwd " : " pp_exp e1 kwd "]" - | E_vector_update(v,e1,e2) -> - fprintf ppf "@[<0>%a%a %a %a%a%a%a@]" kwd "[" pp_exp v kwd "with" pp_exp e1 kwd " = " pp_exp e2 kwd "]" - | E_vector_update_subrange(v,e1,e2,e3) -> - fprintf ppf "@[<0>%a%a %a %a %a %a %a %a %a@]" kwd "[" pp_exp v kwd "with" pp_exp e1 kwd ":" pp_exp e2 kwd " = " pp_exp e3 kwd "]" - | E_list(exps) -> fprintf ppf "@[<0>%a%a%a@]" kwd "[||" (list_pp pp_comma_exp pp_exp) exps kwd "||]" - | E_cons(e1,e2) -> fprintf ppf "@[<0>%a%a%a@]" pp_exp e1 kwd ":" pp_exp e2 - | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> fprintf ppf "@[<0>%a%a%a@]" kwd "{" (list_pp pp_semi_fexp pp_fexp) fexps kwd "}" - | E_record_update(exp,(FES_aux(FES_Fexps(fexps,_),_))) -> - fprintf ppf "@[<0>%a%a %a %a%a@]" kwd "{" pp_exp exp kwd " with " (list_pp pp_semi_fexp pp_fexp) fexps kwd "}" - | E_field(fexp,id) -> fprintf ppf "@[<0>%a%a%a@]" pp_exp fexp kwd "." pp_id id - | E_case(exp,pexps) -> fprintf ppf "@[<0>%a %a %a %a %a@]" kwd "switch " pp_exp exp kwd "{" (list_pp pp_case pp_case) pexps kwd "}" - | E_let(leb,exp) -> fprintf ppf "@[<0>%a@ %a@ %a@]" pp_let leb kwd "in" pp_exp exp - | E_assign(lexp,exp) -> fprintf ppf "@[<0>%a%a%a@]" pp_lexp lexp kwd " := " pp_exp exp - (* XXX missing cases *) - | E_internal_cast ((_, Overload (_, _)), _) | E_internal_exp _ -> assert false - - -and pp_semi_exp ppf e = fprintf ppf "@[<1>%a%a@]" pp_exp e kwd ";" - -and pp_comma_exp ppf e = fprintf ppf "@[<1>%a%a@]" pp_exp e kwd "," - -and pp_fexp ppf (FE_aux(FE_Fexp(id,exp),_)) = fprintf ppf "@[<1>%a %a %a@]" pp_id id kwd " = " pp_exp exp -and pp_semi_fexp ppf fexp = fprintf ppf "@[<1>%a%a@]" pp_fexp fexp kwd ";" - -and pp_case ppf (Pat_aux(Pat_exp(pat,exp),_)) = - fprintf ppf "@[<1>%a %a@@[<1>%a@]@]" pp_pat_atomic pat kwd "-> " pp_exp exp - -and pp_lexp ppf (LEXP_aux(lexp,_)) = - match lexp with - | LEXP_id(id) -> pp_id ppf id - | LEXP_memory(id,args) -> fprintf ppf "@[%a(%a)@]" pp_id id (list_pp pp_exp pp_exp) args - | LEXP_cast(typ,id) -> fprintf ppf "@[(%a) %a@]" pp_typ typ pp_id id - | LEXP_vector(v,exp) -> fprintf ppf "@[%a%a%a%a@]" pp_lexp v kwd "[" pp_exp exp kwd "]" - | LEXP_vector_range(v,e1,e2) -> fprintf ppf "@[%a%a%a%a%a%a@]" pp_lexp v kwd "[" pp_exp e1 kwd ":" pp_exp e2 kwd "]" - | LEXP_field(v,id) -> fprintf ppf "@[%a%a%a@]" pp_lexp v kwd "." pp_id id - -let pp_default ppf (DT_aux(df,_)) = - match df with - | DT_kind(bk,var) -> fprintf ppf "@[<0>%a %a %a@]@\n" kwd "default" pp_bkind bk pp_var var - | DT_typ(ts,id) -> fprintf ppf "@[<0>%a %a %a@]@\n" kwd "default" pp_typscm ts pp_id id - -let pp_spec ppf (VS_aux(v,_)) = - match v with - | VS_val_spec(ts,id) -> fprintf ppf "@[<0>%a %a %a@]@\n" kwd "val" pp_typscm ts pp_id id - | VS_extern_spec(ts,id,s) -> fprintf ppf "@[<0>%a %a %a %a %a \"%s\"@]@\n" kwd "val" kwd "extern" pp_typscm ts pp_id id kwd "=" s - | VS_extern_no_rename(ts,id) -> fprintf ppf "@[<0>%a %a %a %a@]@\n" kwd "val" kwd "extern" pp_typscm ts pp_id id - -let pp_namescm ppf (Name_sect_aux(ns,_)) = - match ns with - | Name_sect_none -> fprintf ppf "" - | Name_sect_some(s) -> fprintf ppf "[%a \"%s\"]" kwd "name =" s - -let rec pp_range ppf (BF_aux(r,_)) = - match r with - | BF_single(i) -> fprintf ppf "%i" i - | BF_range(i1,i2) -> fprintf ppf "%i..%i" i1 i2 - | BF_concat(ir1,ir2) -> fprintf ppf "%a%a %a" pp_range ir1 kwd ", " pp_range ir2 - -let pp_typdef ppf (TD_aux(td,_)) = - match td with - | TD_abbrev(id,namescm,typschm) -> - fprintf ppf "@[<0>%a %a %a %a %a@]@\n" kwd "typedef" pp_id id pp_namescm namescm kwd "=" pp_typscm typschm - | TD_record(id,nm,typq,fs,_) -> - let f_pp ppf (typ,id) = - fprintf ppf "@[<1>%a %a%a@]" pp_typ typ pp_id id kwd ";" in - fprintf ppf "@[<0>%a %a %a%a %a %a %a%a@[<1>%a@]%a@]@\n" - kwd "typedef" pp_id id pp_namescm nm kwd "=" kwd "const" kwd "struct" pp_typquant typq kwd "{" (list_pp f_pp f_pp) fs kwd "}" - | TD_variant(id,nm,typq,ar,_) -> - let a_pp ppf (Tu_aux(typ_u,_)) = - match typ_u with - | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>%a %a%a@]" pp_typ typ pp_id id kwd ";" - | Tu_id(id) -> fprintf ppf "@[<1>%a%a@]" pp_id id kwd ";" - in - fprintf ppf "@[<0>%a %a %a %a %a %a %a %a@[<1>%a@] %a@]@\n" - kwd "typedef" pp_id id pp_namescm nm kwd "=" kwd "const" kwd "union" pp_typquant typq kwd "{" (list_pp a_pp a_pp) ar kwd "}" - | TD_enum(id,ns,enums,_) -> - let pp_id_semi ppf id = fprintf ppf "%a%a " pp_id id kwd ";" in - fprintf ppf "@[<0>%a %a %a %a %a %a%a %a@]@\n" - kwd "typedef" pp_id id pp_namescm ns kwd "=" kwd "enumerate" kwd "{" (list_pp pp_id_semi pp_id) enums kwd "}" - | TD_register(id,n1,n2,rs) -> - let pp_rid ppf (r,id) = fprintf ppf "%a%a%a%a " pp_range r kwd ":" pp_id id kwd ";" in - let pp_rids = (list_pp pp_rid pp_rid) in - fprintf ppf "@[<0>%a %a %a %a %a %a%a%a%a%a %a%a%a@]@\n" - kwd "typedef" pp_id id kwd "=" kwd "register" kwd "bits" kwd "[" pp_nexp n1 kwd ":" pp_nexp n2 kwd "]" kwd "{" pp_rids rs kwd "}" - -let pp_rec ppf (Rec_aux(r,_)) = - match r with - | Rec_nonrec -> fprintf ppf "" - | Rec_rec -> fprintf ppf "rec " - -let pp_tannot_opt ppf (Typ_annot_opt_aux(t,_)) = - match t with - | Typ_annot_opt_some(tq,typ) -> fprintf ppf "%a%a " pp_typquant tq pp_typ typ - -let pp_effects_opt ppf (Effect_opt_aux(e,_)) = - match e with - | Effect_opt_pure -> fprintf ppf "effect pure" - | Effect_opt_effect e -> fprintf ppf "effect %a" pp_effects e - -let pp_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),_)) = - fprintf ppf "%a %a %a @[<1>%a@]@\n" pp_id id pp_pat_atomic pat kwd "=" pp_exp exp - -let pp_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),_)) = - let pp_funcls ppf funcl = fprintf ppf "%a %a" kwd "and" pp_funcl funcl in - fprintf ppf "@[<0>%a %a%a%a @[<1>%a@] @[<1>%a@] @]@\n" - kwd "function" pp_rec r pp_tannot_opt typa pp_effects_opt efa pp_funcl (List.hd fcls) (list_pp pp_funcls pp_funcls) (List.tl fcls) - -let pp_dec ppf (DEC_aux(DEC_reg(typ,id),_)) = - fprintf ppf "@[<0>register %a %a@]@\n" pp_typ typ pp_id id - -let pp_def ppf d = - match d with - | DEF_default(df) -> pp_default ppf df - | DEF_spec(v_spec) -> pp_spec ppf v_spec - | DEF_type(t_def) -> pp_typdef ppf t_def - | DEF_fundef(f_def) -> pp_fundef ppf f_def - | DEF_val(lbind) -> fprintf ppf "@[<0>%a@]@\n" pp_let lbind - | DEF_reg_dec(dec) -> pp_dec ppf dec - | _ -> raise (Reporting_basic.err_unreachable Parse_ast.Unknown "initial_check didn't remove all scattered Defs") - -let pp_defs ppf (Defs(defs)) = - fprintf ppf "@[%a@]@\n" (list_pp pp_def pp_def) defs - - -(**************************************************************************** - * annotated source to Lem ast pretty printer -****************************************************************************) - let rec pp_format_l_lem = function | Parse_ast.Unknown -> "Unknown" | Parse_ast.Int(s,None) -> "(Int \"" ^ s ^ "\" Nothing)" @@ -823,7 +482,9 @@ let pp_lem_defs ppf (Defs(defs)) = fprintf ppf "Defs [@[%a@]]@\n" (list_pp pp_lem_def pp_lem_def) defs -(** PPrint based source-to-source pretty-printer *) +(**************************************************************************** + * PPrint-based source-to-source pretty printer +****************************************************************************) open PPrint |
