diff options
| author | Pierre-Marie Pédrot | 2019-03-03 21:03:37 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-04 14:00:20 +0100 |
| commit | d72e5c154faeea1d55387bc8c039d97f63ebd1c4 (patch) | |
| tree | d7f3c292606e98d2c2891354398e8d406d4dc15c /dev | |
| parent | 6632739f853e42e5828fbf603f7a3089a00f33f7 (diff) | |
Change the representation of kernel case.
We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
Diffstat (limited to 'dev')
| -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"; |