pretty.ml (6447B)
1 module F = Format 2 open Node 3 module B = Builtin 4 open Internal 5 6 let rec pp_print_with_parens 7 : 'a. int -> int -> F.formatter -> ('a, F.formatter, unit) format -> 'a 8 = fun m c ppf -> 9 if c < m then begin 10 F.fprintf ppf "("; 11 F.kfprintf (fun ppf -> F.fprintf ppf ")") ppf 12 end else 13 F.fprintf ppf 14 15 (* TODO: Fix precedences given recent parser changes *) 16 let rec pp_print_term 17 : int -> F.formatter -> term -> unit 18 = fun m ppf -> function 19 | Let (definers, body) -> 20 pp_print_with_parens m 0 ppf "@[<v>@[%a@];@,%a@]" 21 (F.pp_print_array ~pp_sep:pp_print_comma pp_print_definer) definers 22 (pp_print_term 0) body 23 24 | Match {scrutinee; cases; switch} -> 25 pp_print_with_parens m 1 ppf "@[<v 4>%a match {%a} %a@]" 26 (pp_print_term 2) scrutinee 27 pp_print_cases cases 28 pp_print_switch switch 29 30 | App (fn, args) -> 31 pp_print_with_parens m 5 ppf "@[<4>%a@ %a@]" 32 (pp_print_term 6) fn 33 pp_print_args args 34 35 | Fn {multibinder = {binders; _}; term = body} -> 36 pp_print_with_parens m 1 ppf "@[@[<hv 4>fn@ %a%t@]=>@;<1 4>%a@]" 37 pp_print_binders binders 38 (F.pp_print_custom_break ~fits:(" ", 0, "") ~breaks:(",", -4, "")) 39 (pp_print_term 1) body 40 41 | FnType {multibinder = {binders; _}; term = codomain} -> 42 pp_print_with_parens m 3 ppf "@[@[<hv 4>[@,%a%t@]] ->@;<1 4>%a@]" 43 pp_print_binders binders 44 (F.pp_print_custom_break ~fits:("", 0, "") ~breaks:(",", -4, "")) 45 (pp_print_term 3) codomain 46 47 | Data {tag; args; datatype; _} -> 48 begin match args with 49 | [||] -> 50 pp_print_with_parens m 6 ppf "@[%a@]" 51 Name.Tag.pp_print tag 52 | args -> 53 (*pp_print_with_parens m 2 ppf "@[<hv 4>@[<4>%a%a@]:@ %a@;<0 -4>@]"*) 54 pp_print_with_parens m 2 ppf "@[<4>%a@ %a@]" 55 Name.Tag.pp_print tag 56 pp_print_args args 57 (*(pp_print_term 2) (DataType datatype)*) 58 end 59 60 | DataType {ctors; names} -> 61 pp_print_with_parens m 6 ppf "@[@[<hv 4>#{@,%a%t@]}@]" 62 pp_print_ctors (ctors, names) 63 (F.pp_print_custom_break ~fits:("", 0, "") ~breaks:(";", -4, "")) 64 65 | Nat n -> 66 pp_print_with_parens m 6 ppf "%a" 67 Z.pp_print n 68 69 (* TODO: Print surface names here, possibly in addition to indices. This 70 * requires passing around a context during pretty printing *sigh*. *) 71 | Var ij -> 72 pp_print_with_parens m 6 ppf "%a" 73 Index.pp_print ij 74 75 | Builtin b -> 76 pp_print_with_parens m 6 ppf "%a" 77 pp_print_builtin b 78 79 and pp_print_definer 80 : F.formatter -> definer -> unit 81 = fun ppf {names; rhs; typ} -> 82 F.fprintf ppf "@[@[<hv 4>%a:@ %a@;<1 -4>@]:=@;<1 4>%a@]" 83 (pp_print_names 3) names 84 (pp_print_term 2) typ 85 (pp_print_term 1) rhs 86 87 and pp_print_cases 88 : F.formatter -> case array -> unit 89 = fun ppf -> function 90 | [||] -> () 91 | cases -> 92 for i = 0 to Array.length cases - 1 do 93 F.fprintf ppf "@,@[%a =>@;<1 4>%a@]," 94 (pp_print_patt 2) cases.(i).patt 95 (pp_print_term 1) cases.(i).body 96 done; 97 F.fprintf ppf "@;<0 -4>" 98 99 and pp_print_patt 100 : int -> F.formatter -> patt -> unit 101 = fun m ppf -> function 102 | {names = [||]; disc} -> 103 pp_print_disc m ppf disc 104 | {names; disc = DWild _} -> 105 pp_print_names m ppf names 106 | {names; disc = DData _ as disc} -> 107 (* XXX: The grammar uses precdence 4 for all binops. *) 108 pp_print_with_parens m 4 ppf "%a & %a" 109 (pp_print_names 4) names 110 (pp_print_disc 4) disc 111 112 and pp_print_disc 113 : int -> F.formatter -> discriminant -> unit 114 = fun m ppf -> function 115 | DWild _ -> 116 pp_print_with_parens m 6 ppf "_" 117 | DData {tag; subpatts = [||]; _} -> 118 pp_print_with_parens m 6 ppf "%a" 119 Name.Tag.pp_print tag 120 | DData {tag; subpatts; _} -> 121 pp_print_with_parens m 5 ppf "%a %a" 122 Name.Tag.pp_print tag 123 (F.pp_print_array ~pp_sep:F.pp_print_space (pp_print_patt 6)) subpatts 124 125 and pp_print_switch 126 : F.formatter -> switch -> unit 127 = fun ppf -> function 128 | Switch {index; subswitches; names} -> 129 F.fprintf ppf "%a switch {%a}" 130 Index.pp_print index 131 pp_print_subswitches (subswitches, names) 132 | Goto casei -> 133 F.fprintf ppf "goto %d" 134 casei 135 136 and pp_print_subswitches 137 : F.formatter -> switch array * int Name.Tag.Map.t -> unit 138 = fun ppf -> function 139 | ([||], _) -> () 140 | (subswitches, names) -> 141 (* TODO: Doing this conversion sucks. *) 142 let names = Array.of_list (Name.Tag.Map.to_list names) in 143 for i = 0 to Array.length subswitches - 1 do 144 let (tag, _) = names.(i) in 145 F.fprintf ppf "@,@[<v 4>@[%a@] => %a@]," 146 Name.Tag.pp_print tag 147 pp_print_switch subswitches.(i) 148 done; 149 F.fprintf ppf "@;<0 -4>" 150 151 and pp_print_args 152 : F.formatter -> term array -> unit 153 = fun ppf args -> 154 F.pp_print_array ~pp_sep:F.pp_print_space (pp_print_term 6) ppf args 155 156 and pp_print_binders 157 : F.formatter -> binder array -> unit 158 = fun ppf binders -> 159 F.pp_print_array ~pp_sep:pp_print_comma pp_print_binder ppf binders 160 161 and pp_print_binder 162 : F.formatter -> binder -> unit 163 = fun ppf {plicity; patt = {names; disc}} -> 164 F.fprintf ppf "@[%a%a:@;<1 4>%a@]" 165 pp_print_plicity plicity 166 (pp_print_names 3) names 167 (pp_print_term 2) (disc_type disc) 168 169 and pp_print_plicity 170 : F.formatter -> Plicity.t -> unit 171 = fun ppf -> function 172 | Plicity.Im -> F.fprintf ppf "?" 173 | Plicity.Ex -> () 174 175 and pp_print_ctors 176 : F.formatter -> multibinder array * int Name.Tag.Map.t -> unit 177 = fun ppf (ctors, names) -> 178 let first = ref true in 179 Name.Tag.Map.iter (fun tag tagi -> 180 begin if not !first then 181 F.fprintf ppf ";@ "; 182 first := false 183 end; 184 match ctors.(tagi).binders with 185 | [||] -> Name.Tag.pp_print ppf tag 186 | binders -> 187 F.fprintf ppf "@[<4>%a@ %a@]" 188 Name.Tag.pp_print tag 189 pp_print_binders binders 190 ) names 191 192 and pp_print_builtin 193 : F.formatter -> B.builtin -> unit 194 = fun ppf -> function 195 | B.Type -> F.fprintf ppf "~Type" 196 | B.NatType -> F.fprintf ppf "~Nat" 197 | B.NatOpAdd -> F.fprintf ppf "~+" 198 | B.NatOpSub -> F.fprintf ppf "~-" 199 | B.NatOpMul -> F.fprintf ppf "~*" 200 | B.NatOpDiv -> F.fprintf ppf "~/" 201 | B.NatOpMod -> F.fprintf ppf "~%%" 202 | B.NatOpLt -> F.fprintf ppf "~<" 203 | B.NatOpLe -> F.fprintf ppf "~<=" 204 | B.NatOpEq -> F.fprintf ppf "~=" 205 | B.NatOpGe -> F.fprintf ppf "~>=" 206 | B.NatOpGt -> F.fprintf ppf "~>" 207 | B.NatOpNe -> F.fprintf ppf "~<>" 208 209 and pp_print_names 210 : int -> F.formatter -> Name.Var.t array -> unit 211 = fun m ppf -> function 212 | [||] -> 213 pp_print_with_parens m 6 ppf "_" 214 | [|name|] -> 215 pp_print_with_parens m 6 ppf "%a" 216 Name.Var.pp_print name 217 | names -> 218 (* XXX: The grammar uses precdence 4 for all binops. *) 219 pp_print_with_parens m 4 ppf "%a" 220 (F.pp_print_array ~pp_sep:pp_print_and Name.Var.pp_print) names 221 222 and pp_print_comma 223 : F.formatter -> unit -> unit 224 = fun ppf () -> F.fprintf ppf ",@ " 225 226 and pp_print_and 227 : F.formatter -> unit -> unit 228 = fun ppf () -> F.fprintf ppf " & "