commit 9a8eb672e0e4035f7764ad9c71baaad617dad523
parent c5310a3a45f9e009878f3244b461931fdd547542
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Wed, 17 Jan 2024 01:43:13 -0800
Save pretty print stuff in case I want to revert in a minute
Diffstat:
| M | Makefile | | | 2 | +- |
| M | error.ml | | | 2 | +- |
| M | internal.ml | | | 211 | ------------------------------------------------------------------------------- |
| M | main.ml | | | 11 | +++++++++-- |
| M | pretty.ml | | | 186 | ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++--------------- |
5 files changed, 162 insertions(+), 250 deletions(-)
diff --git a/Makefile b/Makefile
@@ -8,13 +8,13 @@ SRC = \
plicity.ml \
loc.ml \
node.ml \
- pretty.ml \
env.ml \
ctx.ml \
concrete.ml \
abstract.ml \
internal.ml \
value.ml \
+ pretty.ml \
error.ml \
parser.ml \
lexer.ml \
diff --git a/error.ml b/error.ml
@@ -70,7 +70,7 @@ and pp_print_error' ppf = function
| EElabApplyNonFunction typ ->
F.fprintf ppf "@[<4>%s@ %a@]"
"attempt to apply non-function of inferred type"
- (I.pp_print_term 0) typ
+ (Pretty.pp_print_term 0) typ
| EElabNonInferablePatt ->
F.pp_print_string ppf "non-inferable pattern"
diff --git a/internal.ml b/internal.ml
@@ -1,5 +1,4 @@
open Node
-module F = Format
(* Ideas for implicit args/metavariables/unification: Unlike in Andras's
* elaboration-zoo, we use globally fresh names in the semantic domain, so
@@ -124,213 +123,3 @@ and data_discriminant = {
subpatts: patt array;
datatype: datatype;
}
-
-let rec pp_print_with_parens
-: 'a. int -> int -> F.formatter -> ('a, F.formatter, unit) format -> 'a
-= fun m c ppf ->
- if c < m then begin
- F.pp_print_string ppf "(";
- F.kfprintf (fun ppf -> F.pp_print_string ppf ")") ppf
- end else
- F.fprintf ppf
-
-and pp_print_term
-: int -> F.formatter -> term -> unit
-= fun m ppf -> function
-| Let (definers, body) ->
- pp_print_with_parens m 0 ppf "@[<v 0>%a;@,%a@]"
- (F.pp_print_array ~pp_sep:pp_print_comma pp_print_definer) definers
- (pp_print_term 0) body
-
-(* TODO: Match *)
-
-| App (fn, args) ->
- pp_print_with_parens m 5 ppf "@[<4>%a%a@]"
- (pp_print_term 6) fn
- pp_print_args args
-
-| Fn {multibinder = {binders; _}; body; codomain} ->
- pp_print_with_parens m 1 ppf "@[fn@[<hv 4>@ %a@]%a=>@[<4>@ %a: %a@]@]"
- pp_print_binders binders
- pp_print_trailing_delim (1, ",")
- (pp_print_term 3) body
- (pp_print_term 2) codomain
-
-| FnType {multibinder = {binders; _}; codomain} ->
- pp_print_with_parens m 3 ppf "@[[@[<hv 4>@,%a@]%a] -> %a@]"
- pp_print_binders binders
- pp_print_trailing_delim (0, ",")
- (pp_print_term 3) codomain
-
-| Data {tag; args; datatype; _} ->
- pp_print_with_parens m 5 ppf "@[<4>%a%a: %a@]"
- Name.Ctor.pp_print tag
- pp_print_args args
- (pp_print_term 2) (DataType datatype)
-
-| DataType {ctors; names} ->
- pp_print_with_parens m 6 ppf "@[#{@[<hv 4>@,%a@]%a}@]"
- pp_print_ctors (ctors, names)
- pp_print_trailing_delim (0, ";")
-
-| Nat n ->
- pp_print_with_parens m 6 ppf "%a"
- Z.pp_print n
-
-(* TODO: Print surface names here, possibly in addition to indices. This
- * requires passing around a context during pretty printing *sigh*. *)
-| Var ij ->
- pp_print_with_parens m 6 ppf "%a"
- Index.pp_print ij
-
-| Type ->
- pp_print_with_parens m 6 ppf "%s"
- "~Type"
-
-| Builtin b ->
- pp_print_with_parens m 6 ppf "%a"
- pp_print_builtin b
-
-and pp_print_definer ppf {names; rhs; typ} =
- F.fprintf ppf "@[<4>%a: %a :=@ %a@]"
- pp_print_names names
- (pp_print_term 2) typ
- (pp_print_term 1) rhs
-
-and pp_print_args ppf = function
-| [||] -> () (* This only happens for Data, not Fn. *)
-| args ->
- F.fprintf ppf "@ %a"
- (F.pp_print_array ~pp_sep:F.pp_print_space (pp_print_term 6)) args
-
-and pp_print_binders ppf binders =
- F.pp_print_array ~pp_sep:pp_print_comma pp_print_binder ppf binders
-
-and pp_print_binder ppf {plicity; names; typ} =
- F.fprintf ppf "@[%a%a: %a@]"
- pp_print_plicity plicity
- pp_print_names names
- (pp_print_term 2) typ
-
-and pp_print_ctors ppf (ctors, names) =
- let first = ref true in
- Name.Ctor.Map.iter (fun tag tagi ->
- begin if not !first then
- F.fprintf ppf ";@ ";
- first := false
- end;
- match ctors.(tagi).binders with
- | [||] -> Name.Ctor.pp_print ppf tag
- | binders ->
- F.fprintf ppf "@[<4>%a%a@]"
- Name.Ctor.pp_print tag
- pp_print_binders binders
- ) names
-
-and pp_print_plicity ppf = function
-| Plicity.Im -> F.pp_print_string ppf "?"
-| Plicity.Ex -> ()
-
-and pp_print_names ppf = function
-| [||] -> F.fprintf ppf "_"
-| names -> F.pp_print_array ~pp_sep:pp_print_and pp_print_name ppf names
-
-and pp_print_name ppf {data = name; _} = Name.Var.pp_print ppf name
-
-and pp_print_trailing_delim ppf (n, d) =
- F.pp_print_custom_break ppf ~fits:("", n, "") ~breaks:(d, 0, "")
-
-and pp_print_comma ppf () = F.fprintf ppf ",@ "
-
-and pp_print_and ppf () = F.pp_print_string ppf " & "
-
-and pp_print_builtin ppf = function
-| NatType -> F.pp_print_string ppf "~Nat"
-| NatOpAdd -> F.pp_print_string ppf "~+"
-| NatOpMul -> F.pp_print_string ppf "~*"
-
-(*
-let rec write_term buf = function
-| Let (definers, body) ->
- P.parens buf 0 @@ fun () ->
- P.at 1 P.iter buf ", " write_definer definers;
- P.string buf "; ";
- P.at 0 write_term buf body
-| App (fn, args) ->
- P.parens buf 6 @@ fun () ->
- P.at 7 write_term buf fn;
- P.string buf " ";
- P.at 7 P.iter buf " " write_term args
-| Fn {multibinder = {binders; _}; body; codomain} ->
- P.parens buf 1 @@ fun () ->
- P.string buf "fn ";
- P.at 2 P.iter buf ", " write_binder binders;
- P.string buf " : ";
- P.at 2 write_term buf codomain;
- P.string buf " => ";
- P.at 1 write_term buf body
-| FnType {multibinder = {binders; _}; codomain} ->
- P.parens buf 3 @@ fun () ->
- P.string buf "[";
- P.at 3 P.iter buf ", " write_binder binders;
- P.string buf "] -> ";
- P.at 3 write_term buf codomain
-| Data {tag; args; datatype} ->
- P.parens buf 6 @@ fun () ->
- P.at 7 P.string buf (Tag.Index.to_string tag);
- begin if Array.length args > 0 then
- P.string buf " ";
- P.at 7 P.iter buf " " write_term args
- end;
- P.string buf " : ";
- P.at 2 write_term buf (DataType datatype)
-| DataType {ctors; names} ->
- P.parens buf 7 @@ fun () ->
- P.string buf "#{";
- P.at 3 P.iter2 buf "; " write_ctor
- (Array.of_list (Tag.Name.Map.to_list names)) ctors;
- P.string buf "}"
-| Nat n ->
- P.parens buf 7 @@ fun () ->
- P.string buf (Z.to_string n)
-| Var ij ->
- P.parens buf 7 @@ fun () ->
- P.string buf "`";
- P.string buf (Index.to_string ij) (* TODO: writer for indices *)
-| Type ->
- P.parens buf 7 @@ fun () ->
- P.string buf "`Type"
-| Builtin NatType ->
- P.parens buf 7 @@ fun () ->
- P.string buf "`Nat"
-| Builtin NatOpAdd ->
- P.parens buf 7 @@ fun () ->
- P.string buf "`+"
-| Builtin NatOpMul ->
- P.parens buf 7 @@ fun () ->
- P.string buf "`*"
-
-and write_definer buf {rhs; typ} =
- P.at 3 write_term buf rhs;
- P.string buf " : ";
- P.at 2 write_term buf typ
-
-and write_binder buf = function
-| {plicity = Plicity.Im; typ} ->
- P.string buf "?";
- write_term buf typ
-| {plicity = Plicity.Ex; typ} ->
- write_term buf typ
-
-and write_ctor buf (tag, _) {binders; _} =
- P.string buf (Tag.Name.to_string tag);
- begin if Array.length binders > 0 then
- P.string buf " ";
- P.at 3 P.iter buf ", " write_binder binders
- end
-
-let to_string t =
- let buf = P.make 1024 in (* Arbitrary initial size *)
- write_term buf t;
- P.to_string buf
-*)
diff --git a/main.ml b/main.ml
@@ -2,6 +2,7 @@ open Node
module I = Internal
module V = Value
+(*
let buf = Lexing.from_string "\
N := [A: Type, A, A -> A] -> A;\n\
add: [N, N] -> N := fn m, n => fn A, z, s => m A (n A z s) s;\n\
@@ -10,6 +11,12 @@ let buf = Lexing.from_string "\
five := add two three;\n\
five Nat 0 (fn n => n + 1)\n\
"
+*)
+
+let buf = Lexing.from_string "\
+ f := fn a: Nat, b: Nat, c: Nat, d: Nat, e: Nat, f: Nat, g: Nat, h: Nat =>\
+ fn a: Nat, b: Nat, c: Nat, d: Nat, e: Nat, f: Nat, g: Nat, h: Nat => 3; 3\
+"
(*
let buf = Lexing.from_string "\
@@ -87,5 +94,5 @@ with Error.Exn e ->
let internal' = Quote.quote ctx.env (Eval.eval ctx.env internal)
let () =
- print (I.pp_print_term 0) internal;
- print (I.pp_print_term 0) internal'
+ print (Pretty.pp_print_term 0) internal;
+ print (Pretty.pp_print_term 0) internal'
diff --git a/pretty.ml b/pretty.ml
@@ -1,35 +1,151 @@
-(* "Pretty" printing. All this module does is handle insertion of
- * parentheses. *)
-
-let make n = (Buffer.create n, 0)
-
-let to_string (b, _) = Buffer.contents b
-
-let at c f (b, _) = f (b, c)
-
-let parens (b, m) c k =
- begin if c < m then Buffer.add_char b '(' end;
- k ();
- begin if c < m then Buffer.add_char b ')' end
-
-let string (b, _) s =
- Buffer.add_string b s
-
-let iter (b, m) sep f = function
-| [||] -> ()
-| xs ->
- f (b, m) xs.(0);
- for i = 1 to Array.length xs - 1 do
- Buffer.add_string b sep;
- f (b, m) xs.(i)
- done
-
-let iter2 (b, m) sep f xs ys =
- if Array.length xs <> Array.length ys then
- invalid_arg "Pretty.iter2"
- else if Array.length xs > 0 then
- f (b, m) xs.(0) ys.(0);
- for i = 1 to Array.length xs - 1 do
- Buffer.add_string b sep;
- f (b, m) xs.(i) ys.(i)
- done
+module F = Format
+open Node
+open Internal
+
+let rec pp_print_with_parens
+: 'a. int -> int -> F.formatter -> ('a, F.formatter, unit) format -> 'a
+= fun m c ppf ->
+ if c < m then begin
+ F.fprintf ppf "(@[<h>";
+ F.kfprintf (fun ppf -> F.fprintf ppf "@])") ppf
+ end else
+ F.fprintf ppf
+
+and pp_print_term
+: int -> F.formatter -> term -> unit
+= fun m ppf -> function
+| Let (definers, body) ->
+ pp_print_with_parens m 0 ppf "@[<v 0>%a;@,@[%a@]@]"
+ (F.pp_print_array ~pp_sep:pp_print_comma pp_print_definer) definers
+ (pp_print_term 0) body
+
+(* TODO: Match *)
+
+| App (fn, args) ->
+ pp_print_with_parens m 5 ppf "%a%a"
+ (pp_print_term 6) fn
+ pp_print_args args
+
+| Fn {multibinder = {binders; _}; body; codomain} ->
+ pp_print_with_parens m 1 ppf "@[<hv>fn@;<1 4>@[<hv 0>%a@]%a:: %a =>@;<1 4>@[<h>%a@]@]"
+ pp_print_binders binders
+ pp_print_trailing_delim (1, ",")
+ (pp_print_term 2) codomain
+ (pp_print_term 1) body
+
+| FnType {multibinder = {binders; _}; codomain} ->
+ pp_print_with_parens m 3 ppf "[@;<0 4>@[<hv 0>%a@]%a] -> %a"
+ pp_print_binders binders
+ pp_print_trailing_delim (0, ",")
+ (pp_print_term 3) codomain
+
+| Data {tag; args; datatype; _} ->
+ pp_print_with_parens m 5 ppf "@[<4>%a%a: %a@]"
+ Name.Ctor.pp_print tag
+ pp_print_args args
+ (pp_print_term 2) (DataType datatype)
+
+| DataType {ctors; names} ->
+ pp_print_with_parens m 6 ppf "@[#{@[<hv 4>@,%a@]%a}@]"
+ pp_print_ctors (ctors, names)
+ pp_print_trailing_delim (0, ";")
+
+| Nat n ->
+ pp_print_with_parens m 6 ppf "%a"
+ Z.pp_print n
+
+(* TODO: Print surface names here, possibly in addition to indices. This
+ * requires passing around a context during pretty printing *sigh*. *)
+| Var ij ->
+ pp_print_with_parens m 6 ppf "%a"
+ Index.pp_print ij
+
+| Type ->
+ pp_print_with_parens m 6 ppf "%s"
+ "~Type"
+
+| Builtin b ->
+ pp_print_with_parens m 6 ppf "%a"
+ pp_print_builtin b
+
+and pp_print_definer
+: F.formatter -> definer -> unit
+= fun ppf {names; rhs; typ} ->
+ F.fprintf ppf "@[@[<hv>%a: %a@] :=@;<1 4>@[%a@]@]"
+ pp_print_names names
+ (pp_print_term 2) typ
+ (pp_print_term 1) rhs
+
+and pp_print_args
+: F.formatter -> term array -> unit
+= fun ppf -> function
+| [||] -> () (* This only happens for Data, not Fn. *)
+| args ->
+ F.fprintf ppf "@ %a"
+ (F.pp_print_array ~pp_sep:F.pp_print_space (pp_print_term 6)) args
+
+and pp_print_binders
+: F.formatter -> binder array -> unit
+= fun ppf binders ->
+ F.pp_print_array ~pp_sep:pp_print_comma pp_print_binder ppf binders
+
+and pp_print_binder
+: F.formatter -> binder -> unit
+= fun ppf {plicity; names; typ} ->
+ F.fprintf ppf "@[%a%a: %a@]"
+ pp_print_plicity plicity
+ pp_print_names names
+ (pp_print_term 2) typ
+
+and pp_print_ctors
+: F.formatter -> multibinder array * int Name.Ctor.Map.t -> unit
+= fun ppf (ctors, names) ->
+ let first = ref true in
+ Name.Ctor.Map.iter (fun tag tagi ->
+ begin if not !first then
+ F.fprintf ppf ";@ ";
+ first := false
+ end;
+ match ctors.(tagi).binders with
+ | [||] -> Name.Ctor.pp_print ppf tag
+ | binders ->
+ F.fprintf ppf "@[<4>%a%a@]"
+ Name.Ctor.pp_print tag
+ pp_print_binders binders
+ ) names
+
+and pp_print_plicity
+: F.formatter -> Plicity.t -> unit
+= fun ppf -> function
+| Plicity.Im -> F.pp_print_string ppf "?"
+| Plicity.Ex -> ()
+
+and pp_print_names
+: F.formatter -> Name.Var.t node array -> unit
+= fun ppf -> function
+| [||] -> F.fprintf ppf "_"
+| names -> F.pp_print_array ~pp_sep:pp_print_and pp_print_name ppf names
+
+and pp_print_name
+: F.formatter -> Name.Var.t node -> unit
+= fun ppf {data = name; _} -> Name.Var.pp_print ppf name
+
+and pp_print_trailing_delim
+: F.formatter -> int * string -> unit
+= fun ppf (n, d) ->
+ F.pp_print_custom_break ppf ~fits:("", n, "") ~breaks:(d, 0, "")
+
+and pp_print_comma
+: F.formatter -> unit -> unit
+= fun ppf () -> F.fprintf ppf ",@ "
+
+and pp_print_and
+: F.formatter -> unit -> unit
+= fun ppf () -> F.pp_print_string ppf " & "
+
+and pp_print_builtin
+: F.formatter -> builtin -> unit
+= fun ppf -> function
+| NatType -> F.pp_print_string ppf "~Nat"
+| NatOpAdd -> F.pp_print_string ppf "~+"
+| NatOpMul -> F.pp_print_string ppf "~*"
