diff options
| author | Maxime Dénès | 2020-02-03 18:19:42 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2020-07-06 11:22:43 +0200 |
| commit | 0ea2d0ff4ed84e1cc544c958b8f6e98f6ba2e9b6 (patch) | |
| tree | fbad060c3c2e29e81751dea414c898b5cb0fa22d /dev/top_printers.ml | |
| parent | cf388fdb679adb88a7e8b3122f65377552d2fb94 (diff) | |
Primitive persistent arrays
Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Diffstat (limited to 'dev/top_printers.ml')
| -rw-r--r-- | dev/top_printers.ml | 20 |
1 files changed, 13 insertions, 7 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 3df6f986ce..ea90e83a83 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -50,13 +50,8 @@ let ppqualid qid = pp(pr_qualid qid) let ppclindex cl = pp(Coercionops.pr_cl_index cl) let ppscheme k = pp (Ind_tables.pr_scheme_kind k) -let prrecarg = function - | Declarations.Norec -> str "Norec" - | Declarations.Mrec (mind,i) -> - str "Mrec[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]" - | Declarations.Imbr (mind,i) -> - str "Imbr[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]" -let ppwf_paths x = pp (Rtree.pp_tree prrecarg x) +let prrecarg = Declareops.pp_recarg +let ppwf_paths x = pp (Declareops.pp_wf_paths x) let get_current_context () = try Vernacstate.Declare.get_current_context () @@ -316,6 +311,7 @@ let constr_display csr = "Int("^(Uint63.to_string i)^")" | Float f -> "Float("^(Float64.to_string f)^")" + | Array (u,t,def,ty) -> "Array("^(array_display t)^","^(term_display def)^","^(term_display ty)^")@{" ^universes_display u^"\n" and array_display v = "[|"^ @@ -450,6 +446,16 @@ let print_pure_constr csr = print_string ("Int("^(Uint63.to_string i)^")") | Float f -> print_string ("Float("^(Float64.to_string f)^")") + | Array (u,t,def,ty) -> + print_string "Array("; + Array.iter (fun x -> box_display x; print_space()) t; + print_string "|"; + box_display def; + print_string ":"; + box_display ty; + print_string ")@{"; + universes_display u; + print_string "}" and box_display c = open_hovbox 1; term_display c; close_box() |