First draft of type & term printer for F.

demos/system-F-type/Main.ml

@@ -4,7 +4,7 @@ open F
 open FTypeChecker
 
 let identity : raw_term =
-  TeTyAbs ("A", TeAbs ("x", TyArrow (TyVar "A", TyVar "A"), TeVar "x"))
+  TeTyAbs ("A", TeAbs ("x", TyVar "A", TeVar "x"))
 
 let identity : nominal_term =
   import_term KitImport.empty identity
@@ -16,4 +16,4 @@ let ty : raw_typ =
   export_typ KitExport.empty ty
 
 let () =
-  printf "Success.\n%!"
+  printf "Success.\nThis term has type %a.\n%!" (PPrintAux.adapt Print.typ) ty

demos/system-F-type/PPrintAux.ml

+open PPrint
+
+(* -------------------------------------------------------------------------- *)
+
+(* A block with indentation. *)
+
+let indentation = 2
+
+let block opening contents closing =
+  group (opening ^^ nest indentation (contents) ^^ closing)
+
+let oblock opening contents =
+  block opening contents empty
+
+(* -------------------------------------------------------------------------- *)
+
+(* Parentheses with indentation. *)
+
+(* We allow breaking a parenthesized thing into several lines by leaving the
+   opening and closing parentheses alone on a line and indenting the content. *)
+
+let parens d =
+  block
+    lparen
+    (break 0 ^^ d)
+    (break 0 ^^ rparen)
+
+(* -------------------------------------------------------------------------- *)
+
+(* Lambda-calculus application. *)
+
+let app d1 d2 =
+  (* The following definition would reject a large argument on a line of
+     its own, indented: *)
+  (* group (d1 ^^ nest indentation (break 1 ^^ d2)) *)
+  (* However, that would be redundant with the fact that large arguments
+     are usually parenthesized, and we already break lines and indent
+     within the parentheses. So, the following suffices: *)
+  group (d1 ^^ space ^^ d2)
+
+(* -------------------------------------------------------------------------- *)
+
+(* Running a buffer printer in a fresh buffer, and sending the result to an
+   output channel. *)
+
+let run (oc : out_channel) (print : Buffer.t -> 'a -> unit) (x : 'a) =
+  let b = Buffer.create 1024 in
+  print b x;
+  Buffer.output_buffer oc b
+
+(* -------------------------------------------------------------------------- *)
+
+(* Printing a document into an output channel, with fixed parameters. *)
+
+let output (oc : out_channel) (d : document) =
+  run oc (PPrintEngine.ToBuffer.pretty 0.9 80) d
+
+let adapt (f : 'a -> document) : out_channel -> 'a -> unit =
+  fun oc x ->
+    output oc (f x)

demos/system-F-type/Print.ml

+open PPrint
+open PPrintAux
+open F
+
+let arrow =
+  string "->"
+
+let forall =
+  string "forall"
+
+let rec typ0 ty =
+  match ty with
+  | TyVar x ->
+      string x
+  | TyArrow _
+  | TyProduct _
+  | TyForall _ ->
+     parens (typ ty)
+
+and typ1 ty =
+  match ty with
+  | TyProduct (ty1, ty2) ->
+      typ0 ty1 ^/^ star ^/^ typ1 ty2
+  | _ ->
+      typ0 ty
+
+and typ2 ty =
+  match ty with
+  | TyArrow (ty1, ty2) ->
+      typ1 ty1 ^/^ arrow ^/^ typ2 ty2
+  | _ ->
+      typ1 ty
+
+and typ3 ty =
+  match ty with
+  | TyForall (x, ty) ->
+      forall ^/^ string x ^^ dot ^/^ typ3 ty
+  | _ ->
+      typ2 ty
+
+and typ ty =
+  typ3 ty
+
+let rec term0 t =
+  match t with
+  | TeVar x ->
+      string x
+  | TeAbs _
+  | TeApp _
+  | TeLet _
+  | TeTyAbs _
+  | TeTyApp _
+  | TePair _
+  | TeProj _ ->
+      parens (term t)
+
+and term1 t =
+  match t with
+  | TeApp (t1, t2) ->
+      app (term1 t1) (term0 t2)
+  | TeTyApp (t1, ty2) ->
+      app (term1 t1) (brackets (typ ty2))
+  | TeProj (i, t) ->
+      app (string (Printf.sprintf "proj%d" i)) (term0 t)
+  | _ ->
+      term0 t
+
+and term2 t =
+  match t with
+  | TePair (t1, t2) ->
+      term1 t1 ^^ comma ^/^ term2 t2
+  | _ ->
+      term1 t
+
+and term3 t =
+  match t with
+  | TeAbs (x, ty, t) ->
+      oblock
+        (backslash ^^ string x ^^ colon ^^ typ ty ^^ dot)
+        (term3 t)
+  | TeLet (x, t1, t2) ->
+      block
+        (string "let" ^/^ string x ^/^ equals)
+        (term t1)
+        (string "in")
+      ^/^
+      term t2
+  | TeTyAbs (a, t) ->
+      oblock
+        (backslash ^^ backslash ^^ string a ^^ dot)
+        (term3 t)
+  | _ ->
+      term2 t
+
+and term t =
+  term3 t
+
+let term (oc : out_channel) (t : (string, string) term) : unit =
+  output oc (term t)