simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat(term): printer

Browse source
This commit is contained in:
Simon Cruanes 2022-08-16 23:21:07 -04:00
parent b7eb6749a1
commit 6a4947a25c
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 2 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/core-logic/term.ml
View file

@ -53,7 +53,7 @@ let unfold_app (e : term) : term * term list =
(* debug printer *) (* debug printer *)
let expr_pp_with_ ~pp_ids ~max_depth out (e : term) : unit = let expr_pp_with_ ~pp_ids ~max_depth out (e : term) : unit =
let rec loop k ~depth names out e = let rec loop k ~depth names out e =
let pp' = loop' k ~depth:(depth + 1) names in let pp' = loop k ~depth:(depth + 1) names in
(match e.view with (match e.view with
| E_type 0 -> Fmt.string out "Type" | E_type 0 -> Fmt.string out "Type"
| E_type i -> Fmt.fprintf out "Type(%d)" i | E_type i -> Fmt.fprintf out "Type(%d)" i
@ -69,7 +69,7 @@ let expr_pp_with_ ~pp_ids ~max_depth out (e : term) : unit =
Fmt.fprintf out "@<1>…/%d" e.id Fmt.fprintf out "@<1>…/%d" e.id
| E_app _ -> | E_app _ ->
let f, args = unfold_app e in let f, args = unfold_app e in
Fmt.fprintf out "%a@ %a" pp' f (Util.pp_list pp') args Fmt.fprintf out "(%a@ %a)" pp' f (Util.pp_list pp') args
| E_lam ("", _ty, bod) -> | E_lam ("", _ty, bod) ->
Fmt.fprintf out "(@[\\_:@[%a@].@ %a@])" pp' _ty Fmt.fprintf out "(@[\\_:@[%a@].@ %a@])" pp' _ty
(loop (k + 1) ~depth:(depth + 1) ("" :: names)) (loop (k + 1) ~depth:(depth + 1) ("" :: names))
@ -94,12 +94,6 @@ let expr_pp_with_ ~pp_ids ~max_depth out (e : term) : unit =
(loop (k + 1) ~depth:(depth + 1) (n :: names)) (loop (k + 1) ~depth:(depth + 1) (n :: names))
bod); bod);
if pp_ids then Fmt.fprintf out "/%d" e.id if pp_ids then Fmt.fprintf out "/%d" e.id
and loop' k ~depth names out e =
match e.view with
| E_type _ | E_var _ | E_bound_var _ | E_const _ ->
loop k ~depth names out e (* atomic expr *)
| E_app _ | E_lam _ | E_pi _ ->
Fmt.fprintf out "(%a)" (loop k ~depth names) e
in in
Fmt.fprintf out "@[%a@]" (loop 0 ~depth:0 []) e Fmt.fprintf out "@[%a@]" (loop 0 ~depth:0 []) e