diff options
| author | coqbot-app[bot] | 2021-01-06 13:04:20 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-06 13:04:20 +0000 |
| commit | 30f497eaf34f2cf641c3fe854fc9066ae19eea67 (patch) | |
| tree | 473734cdc4ea6769de9a5563a0e9e6eeb56dce20 /dev/top_printers.ml | |
| parent | 960178db193c8a78b9414abad13536693ee5b9b8 (diff) | |
| parent | a95654a21c350f19ad0da67713359cbf6c49e95a (diff) | |
Merge PR #13563: Revival of #9710 (Compact kernel representation of pattern-matching)
Reviewed-by: mattam82
Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: jfehrle
Diffstat (limited to 'dev/top_printers.ml')
| -rw-r--r-- | dev/top_printers.ml | 24 |
1 files changed, 18 insertions, 6 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 6ce347ad59..c4eed5756f 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -307,9 +307,9 @@ let constr_display csr = "MutConstruct(("^(MutInd.to_string sp)^","^(string_of_int i)^")," ^","^(universes_display u)^(string_of_int j)^")" | Proj (p, c) -> "Proj("^(Constant.to_string (Projection.constant p))^","^term_display c ^")" - | Case (ci,p,iv,c,bl) -> + | Case (ci,u,pms,(_,p),iv,c,bl) -> "MutCase(<abs>,"^(term_display p)^","^(term_display c)^"," - ^(array_display bl)^")" + ^(array_display (Array.map snd bl))^")" | Fix ((t,i),(lna,tl,bl)) -> "Fix(([|"^(Array.fold_right (fun x i -> (string_of_int x)^(if not(i="") then (";"^i) else "")) t "")^"|],"^(string_of_int i)^")," @@ -420,13 +420,25 @@ let print_pure_constr csr = print_int i; print_string ","; print_int j; print_string ","; universes_display u; print_string ")" - | Case (ci,p,iv,c,bl) -> + | Case (ci,u,pms,p,iv,c,bl) -> + let pr_ctx (nas, c) = + Array.iter (fun na -> print_cut (); name_display na) nas; + print_string " |- "; + box_display c + in open_vbox 0; - print_string "<"; box_display p; print_string ">"; print_cut(); print_string "Case"; - print_space(); box_display c; print_space (); print_string "of"; + print_space(); box_display c; print_space (); + print_cut(); print_string "in"; + print_cut(); print_string "Ind("; + sp_display (fst ci.ci_ind); + print_string ","; print_int (snd ci.ci_ind); print_string ")"; + print_string "@{"; universes_display u; print_string "}"; + Array.iter (fun x -> print_space (); box_display x) pms; + print_cut(); print_string "return <"; pr_ctx p; print_string ">"; + print_cut(); print_string "with"; open_vbox 0; - Array.iter (fun x -> print_cut(); box_display x) bl; + Array.iter (fun x -> print_cut(); pr_ctx x) bl; close_box(); print_cut(); print_string "end"; |