[layout-engine] Enable client and protocol bits; runnable prototype.

Clients can now set the server option `pp_type` to 2 in setting to see
the coq-layout-engine in action.

This is still very experimental, but YMMV.

CHANGES.md

@@ -14,6 +14,9 @@
    outline (@ejgallego, @Alizter, #825, fixes: #824)
  - [fleche] [coq] support `Restart` meta command (@ejgallego,
    @Alizter, #829, fixes #828)
+ - [coq] incorporate experimental `coq-layout-engine` printer, both in
+   client and server parts (@ejgallego, #668, see also #72 and
+   https://github.com/jscoq/jscoq/pull/282 )
 
 # coq-lsp 0.2.0: From Green to Blue
 -----------------------------------

controller/dune

@@ -1,7 +1,7 @@
 (library
  (name controller)
  (modules :standard \ coq_lsp)
- (libraries coq fleche petanque petanque_json lsp dune-build-info))
+ (libraries coq fleche petanque petanque_json lsp layout dune-build-info))
 
 (executable
  (name coq_lsp)

controller/lsp_core.ml

@@ -350,6 +350,7 @@ let get_pp_format_from_config () =
   match !Fleche.Config.v.pp_type with
   | 0 -> Rq_goals.Str
   | 1 -> Rq_goals.Pp
+  | 2 -> Rq_goals.Box
   | v ->
     L.trace "get_pp_format_from_config" "unknown output parameter: %d" v;
     Rq_goals.Str

controller/rq_goals.ml

@@ -26,11 +26,44 @@ let mk_error node =
 type format =
   | Pp
   | Str
+  | Box
 
-let pp ~pp_format pp =
+(* BoxLayout helpers *)
+let set_flag flag value f =
+  let v = !flag in
+  flag := value;
+  try
+    let res = f () in
+    flag := v;
+    res
+  with exn ->
+    flag := v;
+    raise exn
+
+let layout_term env sigma t =
+  (* Coq stores goals in kernel-format, we need to recover the AST back before
+     calling the layout engine; this is called "externalization" in Coq
+     jargon *)
+  let t = Constrextern.extern_type env sigma t in
+  let html = Layout.(Term.layout env sigma t |> BoxModel.Render.to_html) in
+  Format.asprintf "@[%a@]" (Tyxml.Html.pp_elt ()) html
+
+let layout_term env sigma t =
+  set_flag
+    (* Notations = no *)
+    (* Constrextern.print_no_symbol true *)
+    (* Notations = yes *)
+    Constrextern.print_no_symbol false (fun () -> layout_term env sigma t)
+
+let pp ~pp_format ~token env evd x =
   match pp_format with
-  | Pp -> Lsp.JCoq.Pp.to_yojson pp
-  | Str -> `String (Pp.string_of_ppcmds pp)
+  | Pp -> Fleche.Info.Goals.to_pp ~token env evd x |> Lsp.JCoq.Pp.to_yojson
+  | Str ->
+    let pp = Fleche.Info.Goals.to_pp ~token env evd x in
+    `String (Pp.string_of_ppcmds pp)
+  | Box ->
+    let pp = layout_term env evd x in
+    `List [ `String "box"; `String pp ]
 
 let parse ~token ~loc tac st =
   let str = Gramlib.Stream.of_string tac in
@@ -52,7 +85,7 @@ let run_pretac ~token ~loc ~st pretac =
   | Some tac ->
     Coq.State.in_stateM ~token ~st ~f:(parse_and_execute_in ~token ~loc tac) st
 
-let get_goal_info ~token ~doc ~point ~mode ~pretac () =
+let get_goal_info ~pp_format ~token ~doc ~point ~mode ~pretac () =
   let open Fleche in
   let node = Info.LC.node ~doc ~point mode in
   match node with
@@ -63,7 +96,8 @@ let get_goal_info ~token ~doc ~point ~mode ~pretac () =
     (* XXX: Get the location from node *)
     let loc = None in
     let* st = run_pretac ~token ~loc ~st pretac in
-    let+ goals = Info.Goals.goals ~token ~st in
+    let pr = pp ~pp_format in
+    let+ goals = Info.Goals.goals ~token ~pr ~st in
     let program = Info.Goals.program ~st in
     (goals, Some program)
 
@@ -75,13 +109,17 @@ let goals ~pp_format ~mode ~pretac () ~token ~doc ~point =
     Lang.Point.{ line = fst point; character = snd point; offset = -1 }
   in
   let open Coq.Protect.E.O in
-  let+ goals, program = get_goal_info ~token ~doc ~point ~mode ~pretac () in
+  let+ goals, program =
+    get_goal_info ~pp_format ~token ~doc ~point ~mode ~pretac ()
+  in
   let node = Info.LC.node ~doc ~point Exact in
   let messages = mk_messages node in
   let error = Option.bind node mk_error in
-  let pp = pp ~pp_format in
   Lsp.JFleche.GoalsAnswer.(
-    to_yojson pp { textDocument; position; goals; program; messages; error })
+    to_yojson
+      (fun x -> x)
+      (fun x -> Lsp.JCoq.Pp.to_yojson x)
+      { textDocument; position; goals; program; messages; error })
   |> Result.ok
 
 let goals ~pp_format ~mode ~pretac () ~token ~doc ~point =

controller/rq_goals.mli

@@ -8,6 +8,7 @@
 type format =
   | Pp
   | Str
+  | Box
 
 (** [goals ~pp_format ?pretac] Serve goals at point; users can request
     pre-processing and formatting using the provided parameters. *)

coq-layout-engine/dune

@@ -1,4 +1,4 @@
 (library
- (name layoutPrinter)
+ (name layout)
  (public_name coq-lsp.layout-printer)
  (libraries coq-core.interp coq-core.parsing coq-core.printing tyxml))

coq-layout-engine/term.ml

@@ -56,11 +56,12 @@ let ly_sort_name_expr (s : sort_name_expr) =
 let ly_named_sort ((s, _i) : sort_name_expr * int) = ly_sort_name_expr s
 
 let ly_sort (s : sort_expr) =
+  let _qv_expr, s = s in
   match s with
   | Glob_term.UAnonymous { rigid } ->
     (* XXX: What's going on here *)
     if rigid == UnivRigid then BM.Sort [ "Type" ] else BM.Sort [ "Type" ]
-  | Glob_term.UNamed (_qv_expr, sl) -> BM.Sort (List.map ly_named_sort sl)
+  | Glob_term.UNamed sl -> BM.Sort (List.map ly_named_sort sl)
 
 type _cast_kind =
   | VMcast

editor/code/lib/types.ts

@@ -15,12 +15,12 @@ export interface Goal<Pp> {
   hyps: Hyp<Pp>[];
 }
 
-export interface GoalConfig<Pp> {
-  goals: Goal<Pp>[];
-  stack: [Goal<Pp>[], Goal<Pp>[]][];
+export interface GoalConfig<G, Pp> {
+  goals: Goal<G>[];
+  stack: [Goal<G>[], Goal<G>[]][];
   bullet?: Pp;
-  shelf: Goal<Pp>[];
-  given_up: Goal<Pp>[];
+  shelf: Goal<G>[];
+  given_up: Goal<G>[];
 }
 
 export interface Message<Pp> {
@@ -57,10 +57,10 @@ export interface OblsView {
 
 export type ProgramInfo = [Id, OblsView][];
 
-export interface GoalAnswer<Pp> {
+export interface GoalAnswer<Goals, Pp> {
   textDocument: VersionedTextDocumentIdentifier;
   position: Position;
-  goals?: GoalConfig<Pp>;
+  goals?: GoalConfig<Goals, Pp>;
   program?: ProgramInfo;
   messages: Pp[] | Message<Pp>[];
   error?: Pp;
@@ -69,7 +69,7 @@ export interface GoalAnswer<Pp> {
 export interface GoalRequest {
   textDocument: VersionedTextDocumentIdentifier;
   position: Position;
-  pp_format?: "Pp" | "Str";
+  pp_format?: "Box" | "Pp" | "Str";
   pretac?: string;
   command?: string;
   mode?: "Prev" | "After";
@@ -87,6 +87,10 @@ export type Pp =
 
 export type PpString = Pp | string;
 
+export type Box = ["box", string];
+
+export type BoxString = Box | Pp | string;
+
 export interface FlecheDocumentParams {
   textDocument: VersionedTextDocumentIdentifier;
 }
@@ -139,7 +143,7 @@ export interface DocumentPerfParams<R> {
 // View messaging interfaces; should go on their own file
 export interface RenderGoals {
   method: "renderGoals";
-  params: GoalAnswer<PpString>;
+  params: GoalAnswer<BoxString, PpString>;
 }
 
 export interface WaitingForInfo {

editor/code/src/client.ts

@@ -40,6 +40,7 @@ import {
   PpString,
   DocumentPerfParams,
   ViewRangeParams,
+  BoxString,
 } from "../lib/types";
 
 import {
@@ -110,12 +111,12 @@ export interface CoqLspAPI {
   /**
    * Query goals from Coq
    */
-  goalsRequest(params: GoalRequest): Promise<GoalAnswer<PpString>>;
+  goalsRequest(params: GoalRequest): Promise<GoalAnswer<BoxString, PpString>>;
 
   /**
    * Register callback on user-initiated goals request
    */
-  onUserGoals(fn: (goals: GoalAnswer<String>) => void): Disposable;
+  onUserGoals(fn: (goals: GoalAnswer<String, String>) => void): Disposable;
 }
 
 export function activateCoqLSP(

editor/code/src/goals.ts

@@ -9,6 +9,7 @@ import {
   GoalRequest,
   GoalAnswer,
   PpString,
+  BoxString,
   CoqMessagePayload,
   ErrorData,
 } from "../lib/types";
@@ -19,14 +20,16 @@ import {
   TextDocumentIdentifier,
 } from "vscode-languageserver-types";
 
-export const goalReq = new RequestType<GoalRequest, GoalAnswer<PpString>, void>(
-  "proof/goals"
-);
+export const goalReq = new RequestType<
+  GoalRequest,
+  GoalAnswer<BoxString, PpString>,
+  void
+>("proof/goals");
 
 export class InfoPanel {
   private panel: WebviewPanel | null = null;
   private extensionUri: Uri;
-  private listeners: Array<(goals: GoalAnswer<String>) => void> = [];
+  private listeners: Array<(goals: GoalAnswer<String, String>) => void> = [];
 
   constructor(extensionUri: Uri) {
     this.extensionUri = extensionUri;
@@ -42,11 +45,11 @@ export class InfoPanel {
     this.panel?.dispose();
   }
 
-  registerObserver(fn: (goals: GoalAnswer<String>) => void) {
+  registerObserver(fn: (goals: GoalAnswer<String, String>) => void) {
     this.listeners.push(fn);
   }
 
-  unregisterObserver(fn: (goals: GoalAnswer<String>) => void) {
+  unregisterObserver(fn: (goals: GoalAnswer<String, String>) => void) {
     let index = this.listeners.indexOf(fn);
     if (index >= 0) {
       this.listeners.splice(index, 1);
@@ -115,7 +118,7 @@ export class InfoPanel {
   }
 
   // notify the info panel that we have fresh goals to render
-  requestDisplay(goals: GoalAnswer<PpString>) {
+  requestDisplay(goals: GoalAnswer<BoxString, PpString>) {
     this.postMessage({ method: "renderGoals", params: goals });
   }
 
@@ -152,7 +155,7 @@ export class InfoPanel {
       params.pp_format = "Str";
       client.sendRequest(goalReq, params).then(
         (goals) => {
-          let goals_fn = goals as GoalAnswer<String>;
+          let goals_fn = goals as GoalAnswer<String, String>;
           this.listeners.forEach((fn) => fn(goals_fn));
         },
         // We should actually provide a better setup so we can pass
@@ -173,7 +176,7 @@ export class InfoPanel {
     uri: URI,
     version: number,
     position: Position,
-    pp_format: "Pp" | "Str"
+    pp_format: "Box" | "Pp" | "Str"
   ) {
     let textDocument = VersionedTextDocumentIdentifier.create(uri, version);
 

editor/code/views/info/CoqPp.tsx

@@ -1,13 +1,14 @@
-import { PpString } from "../../lib/types";
+import { PpString, BoxString } from "../../lib/types";
 import { FormatPrettyPrint } from "../../lib/format-pprint/js/main";
 
 import "./media/coqpp.css";
+import "./media/boxmodel.css";
 
 export function CoqPp({
   content,
   inline,
 }: {
-  content: PpString;
+  content: BoxString;
   inline: boolean;
 }) {
   if (typeof content == "string") {
@@ -16,6 +17,26 @@ export function CoqPp({
     } else {
       return <pre className="coqpp">{content}</pre>;
     }
+  } else if (content[0] == "box") {
+    let html = content[1];
+    if (inline) {
+      return (
+        <div
+          style={{ display: "inline" }}
+          dangerouslySetInnerHTML={{
+            __html: html,
+          }}
+        ></div>
+      );
+    } else {
+      return (
+        <div
+          dangerouslySetInnerHTML={{
+            __html: html,
+          }}
+        ></div>
+      );
+    }
   } else {
     // https://reactjs.org/docs/integrating-with-other-libraries.html
     if (inline) {