summaryrefslogtreecommitdiff
path: root/src/pretty_print.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/pretty_print.ml')
-rw-r--r--src/pretty_print.ml104
1 files changed, 49 insertions, 55 deletions
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 083bd087..a32db3b1 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -3,11 +3,11 @@ open Format
let is_atomic_typ (Typ_aux(t,_)) =
match t with
- | Typ_var _ | Typ_tup _ -> true
+ | Typ_id _ | Typ_var _ | Typ_tup _ -> true
| _ -> false
let is_atomic_nexp (Nexp_aux(n,_)) =
match n with
- | Nexp_id _ | Nexp_constant _ | Nexp_exp _ -> true
+ | Nexp_var _ | Nexp_constant _ | Nexp_exp _ -> true
| _ -> false
let is_atomic_pat (P_aux(p,l)) =
@@ -54,7 +54,7 @@ let pp_format_id (Id_aux(i,_)) =
let pp_id ppf id = base ppf (pp_format_id id)
-let pp_format_var (Var_aux(Var v,_)) = "'" ^ v
+let pp_format_var (Kid_aux(Var v,_)) = "'" ^ v
let pp_var ppf var = base ppf (pp_format_var var)
@@ -63,7 +63,7 @@ let pp_format_bkind (BK_aux(k,_)) =
| BK_type -> "Type"
| BK_nat -> "Nat"
| BK_order -> "Order"
- | BK_effects -> "Effects"
+ | BK_effect -> "Effect"
let pp_bkind ppf bk = base ppf (pp_format_bkind bk)
@@ -78,13 +78,12 @@ let rec pp_format_typ (Typ_aux(t,_)) =
| 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) ^ " " ^
+ (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) ^ ")"
+ | 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_id(id) -> pp_format_id id
| 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) ^ ")"
@@ -92,35 +91,33 @@ and pp_format_nexp (Nexp_aux(n,_)) =
| Nexp_exp(n1) -> "2** (" ^ (pp_format_nexp n1) ^ ")"
and pp_format_ord (Ord_aux(o,_)) =
match o with
- | Ord_id(id) -> pp_format_id id
| Ord_var(var) -> pp_format_var var
| Ord_inc -> "inc"
| Ord_dec -> "dec"
-and pp_format_effects (Effects_aux(e,_)) =
+and pp_format_effects (Effect_aux(e,_)) =
match e with
- | Effects_id(id) -> "effect " ^ pp_format_id id
- | Effects_var(var) -> "effect " ^ pp_format_var var
- | Effects_set(efcts) ->
+ | Effect_var(var) -> pp_format_var var
+ | Effect_set(efcts) ->
if (efcts = [])
then "pure"
- else "effect {" ^
+ else "{" ^
(list_format ","
- (fun (Effect_aux(e,l)) ->
+ (fun (BE_aux(e,l)) ->
match e with
- | Effect_rreg -> "rreg"
- | Effect_wreg -> "wreg"
- | Effect_rmem -> "rmem"
- | Effect_wmem -> "wmem"
- | Effect_undef -> "undef"
- | Effect_unspec -> "unspec"
- | Effect_nondet -> "nondet")
+ | 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_effects(e) -> pp_format_effects e
+ | 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)
@@ -132,8 +129,8 @@ let pp_format_nexp_constraint (NC_aux(nc,_)) =
| 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(id,bounds) ->
- pp_format_id id ^
+ | NC_nat_set_bounded(var,bounds) ->
+ pp_format_var var ^
" In {" ^
list_format ", " string_of_int bounds ^
"}"
@@ -185,7 +182,7 @@ let rec pp_format_pat (P_aux(p,l)) =
| 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_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 ^ "(" ^
@@ -199,7 +196,7 @@ let rec pp_format_pat (P_aux(p,l)) =
"[" ^ 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) ^ "|]"
+ | 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)
@@ -218,8 +215,8 @@ and pp_exp ppf (E_aux(e,_)) =
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_app(f,args) -> fprintf ppf "@[<0>%a %a@]" pp_id f (list_pp pp_exp pp_exp) args
+ | E_cast(typ,exp) -> fprintf ppf "@[<0>%a%a%a %a@]" kwd "(" pp_typ typ kwd ")" pp_exp exp
+ | E_app(f,args) -> fprintf ppf "@[<0>%a(%a)@]" pp_id f (list_pp pp_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
@@ -260,7 +257,7 @@ and pp_case ppf (Pat_aux(Pat_exp(pat,exp),_)) =
and pp_lexp ppf (LEXP_aux(lexp,_)) =
match lexp with
| LEXP_id(id) -> pp_id ppf id
- | LEXP_memory(id,exp) -> fprintf ppf "@[%a %a@]" pp_id id pp_exp exp
+ | LEXP_memory(id,args) -> fprintf ppf "@[%a(%a)@]" pp_id id (list_pp pp_exp pp_exp) args
| 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
@@ -323,10 +320,10 @@ 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 (Effects_opt_aux(e,_)) =
+let pp_effects_opt ppf (Effect_opt_aux(e,_)) =
match e with
- | Effects_opt_pure -> fprintf ppf ""
- | Effects_opt_effects e -> pp_effects ppf e
+ | 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 "@[<0>%a %a %a @[<1>%a@] @]@\n" pp_id id pp_pat_atomic pat kwd "=" pp_exp exp
@@ -361,7 +358,7 @@ let pp_format_id_lem (Id_aux(i,_)) =
let pp_lem_id ppf id = base ppf (pp_format_id_lem id)
-let pp_format_var_lem (Var_aux(Var v,_)) = "(Var \"" ^ v ^ "\")"
+let pp_format_var_lem (Kid_aux(Var v,_)) = "(Var \"" ^ v ^ "\")"
let pp_lem_var ppf var = base ppf (pp_format_var_lem var)
@@ -370,7 +367,7 @@ let pp_format_bkind_lem (BK_aux(k,_)) =
| BK_type -> "BK_type"
| BK_nat -> "BK_nat"
| BK_order -> "BK_order"
- | BK_effects -> "BK_effects"
+ | BK_effect -> "BK_effect"
let pp_lem_bkind ppf bk = base ppf (pp_format_bkind_lem bk)
@@ -391,7 +388,6 @@ let rec pp_format_typ_lem (Typ_aux(t,_)) =
| Typ_wild -> "Typ_wild"
and pp_format_nexp_lem (Nexp_aux(n,_)) =
match n with
- | Nexp_id(id) -> "(Nexp_id " ^ pp_format_id_lem id ^ ")"
| Nexp_var(v) -> "(Nexp_var " ^ pp_format_var_lem v ^ ")"
| Nexp_constant(i) -> "(Nexp_constant " ^ string_of_int i ^ ")"
| Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
@@ -399,33 +395,31 @@ and pp_format_nexp_lem (Nexp_aux(n,_)) =
| Nexp_exp(n1) -> "(Nexp_exp " ^ (pp_format_nexp_lem n1) ^ ")"
and pp_format_ord_lem (Ord_aux(o,_)) =
match o with
- | Ord_id(id) -> "(Ord_id " ^ pp_format_id_lem id ^ ")"
| Ord_var(v) -> "(Ord_var " ^ pp_format_var_lem v ^ ")"
| Ord_inc -> "Ord_inc"
| Ord_dec -> "Ord_dec"
-and pp_format_effects_lem (Effects_aux(e,_)) =
+and pp_format_effects_lem (Effect_aux(e,_)) =
match e with
- | Effects_id(id) -> "(Effects_id " ^ pp_format_id id ^ ")"
- | Effects_var(v) -> "(Effects_var " ^ pp_format_var v ^ ")"
- | Effects_set(efcts) ->
- "(Effects_set [" ^
+ | Effect_var(v) -> "(Effect_var " ^ pp_format_var v ^ ")"
+ | Effect_set(efcts) ->
+ "(Effect_set [" ^
(list_format "; "
- (fun (Effect_aux(e,l)) ->
+ (fun (BE_aux(e,l)) ->
match e with
- | Effect_rreg -> "Effect_rreg"
- | Effect_wreg -> "Effect_wreg"
- | Effect_rmem -> "Effect_rmem"
- | Effect_wmem -> "Effect_wmem"
- | Effect_undef -> "Effect_undef"
- | Effect_unspec -> "Effect_unspec"
- | Effect_nondet -> "Effect_nondet")
+ | BE_rreg -> "BE_rreg"
+ | BE_wreg -> "BE_wreg"
+ | BE_rmem -> "BE_rmem"
+ | BE_wmem -> "BE_wmem"
+ | BE_undef -> "BE_undef"
+ | BE_unspec -> "BE_unspec"
+ | BE_nondet -> "BE_nondet")
efcts) ^ " ])"
and pp_format_typ_arg_lem (Typ_arg_aux(t,_)) =
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_effects(e) -> "(Typ_arg_effects " ^ pp_format_effects_lem e ^ ")"
+ | Typ_arg_effect(e) -> "(Typ_arg_effect " ^ pp_format_effects_lem e ^ ")"
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)
@@ -438,7 +432,7 @@ let pp_format_nexp_constraint_lem (NC_aux(nc,_)) =
| 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_id id ^
+ pp_format_var_lem id ^
" [" ^
list_format "; " string_of_int bounds ^
"])"
@@ -567,7 +561,7 @@ and pp_lem_case ppf (Pat_aux(Pat_exp(pat,exp),_)) =
and pp_lem_lexp ppf (LEXP_aux(lexp,_)) =
match lexp with
| LEXP_id(id) -> fprintf ppf "(%a %a)" kwd "LEXP_id" pp_lem_id id
- | LEXP_memory(id,exp) -> fprintf ppf "(%a %a %a)" kwd "LEXP_memory" pp_lem_id id pp_lem_exp exp
+ | LEXP_memory(id,args) -> fprintf ppf "(%a %a [%a])" kwd "LEXP_memory" pp_lem_id id (list_pp pp_semi_lem_exp pp_lem_exp) args
| 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
@@ -631,10 +625,10 @@ let pp_lem_tannot_opt ppf (Typ_annot_opt_aux(t,_)) =
match t with
| Typ_annot_opt_some(tq,typ) -> fprintf ppf "(Typ_annot_opt_some %a %a)" pp_lem_typquant tq pp_lem_typ typ
-let pp_lem_effects_opt ppf (Effects_opt_aux(e,_)) =
+let pp_lem_effects_opt ppf (Effect_opt_aux(e,_)) =
match e with
- | Effects_opt_pure -> fprintf ppf "Effects_opt_pure"
- | Effects_opt_effects e -> fprintf ppf "(Effects_opt_effects %a)" pp_effects e
+ | Effect_opt_pure -> fprintf ppf "Effect_opt_pure"
+ | Effect_opt_effect e -> fprintf ppf "(Effect_opt_effects %a)" pp_lem_effects e
let pp_lem_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
fprintf ppf "@[<0>(%a %a %a %a)@]@\n" kwd "FCL_Funcl" pp_lem_id id pp_lem_pat pat pp_lem_exp exp
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 13:31:51 +0000