Commit 9e80fb3c authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Print less useless parentheses

parent 677a582e
......@@ -8,12 +8,12 @@ let print_label out_fmter (Label l) = Format.fprintf out_fmter "lab_%s" l
let compile_string out_fmter s =
let n = String.length s in
String.iter (Format.fprintf out_fmter "dk_string.cons@ dk_char.%c@ (") s;
String.iter (Format.fprintf out_fmter "@[<hov>dk_string.cons@ dk_char.%c@ (") s;
Format.fprintf out_fmter "dk_string.nil";
Format.fprintf out_fmter "%s" (String.make n ')')
Format.fprintf out_fmter "%s@]" (String.make n ')')
let declare_label out_fmter (Label l) =
Format.fprintf out_fmter "lab_%s :@ dk_string.String :=@ @[%a@]."
Format.fprintf out_fmter "@[<h>lab_%s : dk_string.String@ := %a.@]@."
l
compile_string l
......@@ -22,93 +22,104 @@ let declare_labels out_fmter = List.iter (declare_label out_fmter)
let rec print_ty out_fmter = function
| Stcid (c, _) -> print_cid out_fmter c
| Stlist [] ->
Format.fprintf out_fmter "@[dk_type.nil@]"
Format.fprintf out_fmter "dk_type.nil"
| Stlist ((l, ty) :: ll) ->
Format.fprintf out_fmter "@[dk_type.cons@ (%a)@ (%a)@ (%a)@]"
Format.fprintf out_fmter "@[<hov>dk_type.cons@ %a@ %a@ %a@]"
print_label l
print_ty ty
print_ty (Stlist ll)
print_par_ty ty
print_par_ty (Stlist ll)
| Starr (ty1, ty2) ->
Format.fprintf out_fmter "@[dk_obj_examples.arrow@ (%a)@ (%a)@]"
print_ty ty1
print_ty ty2
Format.fprintf out_fmter "@[<hov>dk_obj_examples.arrow@ %a@ %a@]"
print_par_ty ty1
print_par_ty ty2
and print_par_ty out_fmter = function
| Stcid _ | Stlist [] as ty -> print_ty out_fmter ty
| ty ->
Format.fprintf out_fmter "(%a)"
print_ty ty
let rec print_term out_fmter : tterm -> unit = function
| Tvar (id, _) -> print_id out_fmter id
| Tvar (id, _)
| Tconst (id, _, _) -> print_id out_fmter id
| Tpar t ->
Format.fprintf out_fmter "(%a)"
print_term t
| Tapp (t1, t2, ty2, ty) ->
Format.fprintf out_fmter "@[dk_obj_examples.App@ (%a)@ (%a)@ (%a)@ (%a)@]"
print_ty ty
print_ty ty2
print_term t1
print_term t2
Format.fprintf out_fmter "@[<hov>dk_obj_examples.App@ %a@ %a@ %a@ %a@]"
print_par_ty ty2
print_par_ty ty
print_par_term t1
print_par_term t2
| Tabst (x, ty, body, rty) ->
Format.fprintf out_fmter "@[dk_obj_examples.Lambda@ (%a)@ (%a)@ (%a :@ dk_obj.Expr (%a) =>@ %a)@]"
print_ty ty
print_ty rty
Format.fprintf out_fmter "@[<hov>dk_obj_examples.Lambda@ %a@ %a@ (%a :@ dk_obj.Expr %a =>@ %a)@]"
print_par_ty ty
print_par_ty rty
print_id x
print_ty ty
print_par_ty ty
print_term body
| Tobj (ll, ty) ->
print_object ty out_fmter ll
| Tsel (t, l, ty) ->
Format.fprintf out_fmter "@[dk_obj.select@ (%a)@ (%a)@ (%a)@]"
print_ty (infer t)
print_term t
Format.fprintf out_fmter "@[<hov>dk_obj.select@ %a@ %a@ %a@]"
print_par_ty (infer t)
print_par_term t
print_label l
| Tupd (t, l, m, ty) ->
Format.fprintf out_fmter "@[dk_obj.update@ (%a)@ (%a)@ (%a)@ (%a)@]"
print_ty ty
print_term t
Format.fprintf out_fmter "@[<hov>dk_obj.update@ %a@ %a@ %a@ %a@]"
print_par_ty ty
print_par_term t
print_label l
print_meth m
print_par_meth m
| Tcast (t, ty1, ty2) ->
Format.fprintf out_fmter "@[dk_obj.coerce@ (%a)@ (%a)@ dk_logic.I@ (%a)@]"
print_ty ty1
print_ty ty2
Format.fprintf out_fmter "@[<hov>dk_obj.coerce@ %a@ %a@ dk_logic.I@ %a@]"
print_par_ty ty1
print_par_ty ty2
print_par_term t
and print_par_term out_fmter = function
| Tvar _ | Tconst _ | Tpar _ as t -> print_term out_fmter t
| t ->
Format.fprintf out_fmter "(%a)"
print_term t
and print_object ty out_fmter = function
| [] ->
Format.fprintf out_fmter "@[dk_obj.Po_nil@ (%a)@ (dk_type.assoc@ (%a))@]"
print_ty ty
print_ty ty
Format.fprintf out_fmter "@[<hov>dk_obj.Po_nil@ %a@ (dk_type.assoc@ %a)@]"
print_par_ty ty
print_par_ty ty
| (l, m) :: ll ->
Format.fprintf out_fmter "@[dk_obj.Po_cons@ (%a)@ (dk_type.assoc@ (%a))@ (%a)@ (%a)@ (%a)@ (%a)@]"
print_ty ty
print_ty ty
print_domain ll
Format.fprintf out_fmter "@[<hov>dk_obj.Po_cons@ %a@ (dk_type.assoc@ %a)@ %a@ %a@ %a@ %a@]"
print_par_ty ty
print_par_ty ty
print_par_domain ll
print_label l
print_meth m
(print_object ty) ll
and print_domain out_fmter = function
print_par_meth m
(print_par_object ty) ll
and print_par_object ty out_fmter t = Format.fprintf out_fmter "(%a)" (print_object ty) t
and print_par_domain out_fmter = function
| [] -> Format.fprintf out_fmter "dk_domain.nil"
| (l, _) :: ll ->
Format.fprintf out_fmter "@[dk_domain.cons@ (%a)@ (%a)"
Format.fprintf out_fmter "(@[<hov>dk_domain.cons@ %a@ %a@])"
print_label l
print_domain ll
and print_meth out_fmter (Tmeth (x, ty, body, rty)) =
Format.fprintf out_fmter "@[(%a :@ dk_obj.Expr (%a) => %a)@]"
print_par_domain ll
and print_par_meth out_fmter (Tmeth (x, ty, body, rty)) =
Format.fprintf out_fmter "(@[<h>%a :@ dk_obj.Expr %a =>@ %a@])"
print_id x
print_ty ty
print_par_ty ty
print_term body
let print_line out_fmter = function
| Ttypedef (cid, ty) ->
Format.fprintf out_fmter "@[%a :@ dk_type.type :=@ %a.@]@\n"
Format.fprintf out_fmter "@[<h>%a :@ dk_type.type@ := %a.@]@\n"
print_cid cid
print_ty ty
| Tvardef (id, ty, def) ->
Format.fprintf out_fmter "@[%a :@ dk_obj.Expr (%a) :=@ %a.@]@\n"
Format.fprintf out_fmter "@[<h>%a :@ dk_obj.Expr %a@ := %a.@]@\n"
print_id id
print_ty ty
print_par_ty ty
print_term def
| Tcheck (t, ty) ->
Format.fprintf out_fmter "@[#CHECK %a,@ dk_obj.Expr@ (%a).@]@\n"
Format.fprintf out_fmter "@[<h>#CHECK %a,@ dk_obj.Expr@ %a.@]@\n"
print_term t
print_ty ty
print_par_ty ty
| Tconv (t1, t2, ty) ->
Format.fprintf out_fmter "@[<h>#CHECK %a,@ dk_obj.Expr@ %a.@]@\n"
print_term t1
......@@ -120,7 +131,7 @@ let print_line out_fmter = function
print_term t1
print_term t2
| Tnorm t ->
Format.fprintf out_fmter "@[#SNF %a.@]@\n"
Format.fprintf out_fmter "@[<h>#SNF %a.@]@\n"
print_term t
let print out_fmter = List.iter (print_line out_fmter)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment