Add LaTeX to the layout engine

coq-layout-engine/README.md

@@ -0,0 +1,14 @@
+## Features
+
+- For identifiers:
+  + Global name
+  + Type of identifiers
+- For notations:
+
+## TODO
+
+- tests
+- coverage
+- split coq_utils to its own library
+- versioning of format
+- add a cache for meta-data resolution

coq-layout-engine/boxModel.ml

@@ -0,0 +1,171 @@
+(************************************************************************)
+(* coq-layout-engine                                                    *)
+(* Copyright 2021 Inria                                                 *)
+(* Written by Emilio J. Gallego Arias                                   *)
+(************************************************************************)
+(* Status: Very Experimental                                            *)
+(************************************************************************)
+
+type abs_kind =
+  | Prod
+  | Lam
+
+module Id = struct
+  type 'a t =
+    { relative : string
+    ; absolute : string option
+    ; typ : 'a option
+    }
+end
+
+module Variable = struct
+  type 'a t =
+    { name : string
+    ; typ : 'a
+    }
+end
+
+module Binder = struct
+  type 'a t =
+    { namel : string list
+    ; typ : 'a
+    }
+
+  let map ~f b = { b with typ = f b.typ }
+end
+
+(** Output Layout Box model, designed to be embedded in DOM almost directly, and
+    to replace Pp.t *)
+type t =
+  | Variable of t Variable.t  (** Variable *)
+  | Constant of string  (** Constant (lexical) *)
+  | Identifier of t Id.t  (** Identifier *)
+  | Sort of string list  (** Sort *)
+  | App of
+      { fn : t
+      ; impl : t list
+      ; argl : t list
+      }  (** Application box *)
+  | Cast of t option * t  (** Cast box *)
+  | Abs of
+      { kind : abs_kind
+      ; binderl : t Binder.t list
+      ; v : t
+      }  (** Abstraction *)
+  (* XXX Use binder.t *)
+  | Let of
+      { lhs : t
+      ; rhs : t
+      ; typ : t option
+      ; v : t
+      }  (** Let *)
+  | Notation of
+      { key : string
+      ; args : t list
+      ; pretty : t list
+      ; raw : t
+      }  (** Notation *)
+  | Fixpoint of t * t
+
+(** Renderer *)
+module H = Tyxml.Html
+
+module LaTeX = struct
+
+  type t =
+    | Token of string
+    | Macro of string * t list
+    | List of t list
+
+  let macro s = Macro(s, [])
+end
+
+module Render = struct
+  let xxx kind = H.txt ("uninplemented: " ^ kind)
+  let _class c = [ H.a_class [ c ] ]
+
+  let span ?(extra = []) c e =
+    let a = _class c in
+    H.span ~a (extra @ e)
+
+  let id_to_html id = span "identifier" [ H.txt id ]
+
+  let binder_to_html ({ Binder.namel; typ } : _ Binder.t) : _ H.elt =
+    let namel = List.map H.txt namel in
+    span "binder" [ span "namel" namel; span "btype" [ typ ] ]
+
+  let rec to_html (b : t) : _ H.elt =
+    match b with
+    | Variable { name; typ } ->
+      let name = span "name" [ id_to_html name ] in
+      let typ = span "type" [ to_html typ ] in
+      span "variable" [ name; typ ]
+    | Constant c -> span "constant" [ H.txt c ]
+    | Identifier { relative; absolute; typ } ->
+      span "reference"
+      @@ [ span "relative" [ H.txt relative ] ]
+      @ Option.cata (fun a -> [ span "absolute" [ H.txt a ] ]) [] absolute
+      @ Option.cata (fun typ -> [ span "type" [ to_html typ ] ]) [] typ
+    | Cast (_c, t) -> span "cast" @@ [ to_html t ]
+    | Sort e -> span "sort" @@ List.map H.txt e
+    | App { fn; impl = _; argl } ->
+      let fn = to_html fn in
+      let argl = List.map to_html argl in
+      span "app" [ H.txt "("; fn; span "args" argl; H.txt ")" ]
+    | Abs { kind; binderl; v } ->
+      let head, delim =
+        match kind with
+        | Prod -> ("forall", ",")
+        | Lam -> ("fun", "=>")
+      in
+      let binderl = List.map (Binder.map ~f:to_html) binderl in
+      let binderl = List.map binder_to_html binderl in
+      let v = to_html v in
+      span "abs" [ H.txt head; span "binderl" binderl; H.txt delim; v ]
+    | Let _ -> xxx "let"
+    | Notation { key; args; pretty; raw } ->
+      let t_h = span "arguments" (List.map to_html args) in
+      let pretty_h = List.map to_html pretty in
+      span "notation"
+        [ span "key" [ H.txt key ]
+        ; t_h
+        ; span "pretty" pretty_h
+        ; span "raw" [ to_html raw ]
+        ]
+    | Fixpoint (_, _) -> xxx "fixpoint"
+
+  module LaTeX = struct
+
+    let binder_to_latex : _ Binder.t -> LaTeX.t =
+      function { Binder.namel; _ } ->
+        LaTeX.List([Token "("; LaTeX.List(List.map (fun x -> LaTeX.Token x) namel); Token")"])
+
+    let rec to_latex : t -> LaTeX.t =
+      let open LaTeX in 
+      function
+       | Variable {name; _ } -> Token name
+       | Constant c -> Token c
+       | Identifier {relative ; absolute = _ ; _ } -> Token relative
+       | Sort e -> List (List.map (fun e -> Token e) e)
+       | App {fn; impl= _; argl} -> List(to_latex fn :: (List.map to_latex argl))
+       | Cast (_c, t) -> to_latex t
+       | Abs {kind; binderl; v} ->
+         (* let head, delim = *)
+         let binderl = List.map (Binder.map ~f:to_latex) binderl in
+         let binderl = List.map binder_to_latex binderl in         
+         (match kind with
+         | Prod -> List( (macro "prod") :: to_latex v :: binderl)
+         | Lam ->  List( (macro "lambda") :: to_latex v :: binderl))
+       | Let {lhs; rhs; typ =_; v} ->
+         List([Token "let";
+               to_latex lhs;
+               Token ":=";
+               to_latex rhs;
+               Token "in";
+               to_latex v])
+       | Notation _ -> Token ""
+       | Fixpoint (f1, f2) ->
+         List([Token "fix"; to_latex f1; to_latex f2 ])
+  end
+  let to_latex = LaTeX.to_latex
+end

coq-layout-engine/boxModel.mli

@@ -0,0 +1,81 @@
+(************************************************************************)
+(* coq-layout-engine                                                    *)
+(* Copyright 2021 Inria                                                 *)
+(* Written by Emilio J. Gallego Arias                                   *)
+(************************************************************************)
+(* Status: Very Experimental                                            *)
+(************************************************************************)
+
+(* Note: This file is independent of Coq        *)
+(* XXX: TODO enforce the above in the dune file *)
+type abs_kind =
+  | Prod
+  | Lam
+
+module Id : sig
+  type 'a t =
+    { relative : string
+    ; absolute : string option
+    ; typ : 'a option
+    }
+end
+
+module Variable : sig
+  type 'a t =
+    { name : string
+    ; typ : 'a
+    }
+end
+
+module Binder : sig
+  type 'a t =
+    { namel : string list
+    ; typ : 'a
+    }
+end
+
+(** Output Layout Box model, designed to be embedded in DOM almost directly, and
+    to replace Pp.t *)
+type t =
+  | Variable of t Variable.t  (** Variable *)
+  | Constant of string  (** Constant *)
+  | Identifier of t Id.t  (** Identifier *)
+  | Sort of string list  (** Sort *)
+  | App of
+      { fn : t
+      ; impl : t list
+      ; argl : t list
+      }  (** Application box *)
+  | Cast of t option * t  (** Cast box *)
+  | Abs of
+      { kind : abs_kind
+      ; binderl : t Binder.t list
+      ; v : t
+      }  (** Abstraction *)
+  | Let of
+      { lhs : t
+      ; rhs : t
+      ; typ : t option
+      ; v : t
+      }  (** Let *)
+  | Notation of
+      { key : string
+      ; args : t list
+      ; pretty : t list
+      ; raw : t
+      }  (** Notation *)
+  | Fixpoint of t * t
+
+module LaTeX : sig
+  type t =
+    | Token of string
+    | Macro of string * t list
+    | List of t list
+end
+
+(** Simple wrapping in <div> *)
+module Render : sig
+  val to_html :
+    t -> [< Html_types.span_content_fun > `PCDATA `Span ] Tyxml.Html.elt
+  val to_latex : t -> LaTeX.t
+end

coq-layout-engine/coq_util.ml

@@ -0,0 +1,116 @@
+open Constrexpr
+
+let debug = ref false
+
+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 intern_reference qid =
+  if !debug then
+    Feedback.msg_warning Pp.(str "ir [<-] " ++ Libnames.pr_qualid qid);
+  let r =
+    try Some (Nametab.locate_extended qid) with
+    | Not_found -> None
+    (* XXX behavior here is dubious unfortunately, as we see a var as a ref,
+       GlobalizationError is raised *)
+    | Nametab.GlobalizationError _ -> None
+    | _ ->
+      Feedback.msg_warning Pp.(str "uuuuuuhgggh");
+      None
+  in
+  let r = Option.bind r Smartlocate.global_of_extended_global in
+  if !debug then
+    Feedback.msg_warning Pp.(str "ir [->] " ++ Pp.pr_opt Printer.pr_global r);
+  r
+
+(* From a term to its representation with notations *)
+let recover_notation env sigma t =
+  let gt = Constrintern.intern_constr env sigma t in
+  set_flag (* Notations = yes *) Constrextern.print_no_symbol false (fun () ->
+      let eenv = Constrextern.extern_env env sigma in
+      Constrextern.extern_glob_type eenv gt)
+  |> fun t ->
+  match t.CAst.v with
+  | CNotation _ -> Some t
+  | _ -> None
+
+let _recover_notation env sigma t =
+  try recover_notation env sigma t (* Due to wrong env passed *)
+  with exn ->
+    Feedback.msg_warning
+      (let iexn = Exninfo.capture exn in
+       Pp.(str "error in recover_notation: " ++ CErrors.iprint iexn));
+    None
+
+(* From a notation to a notation-free term *)
+let notation_raw env sigma t =
+  if !debug then
+    Feedback.msg_warning
+      Pp.(str "nr [<-] " ++ Ppconstr.pr_constr_expr env sigma t);
+  (* Wish: In place of full internalization + notation-free extern, we could have an operation
+   *
+   * [expand_notation : constr_expr -> constr_expr]
+   * [expand_implicits : constr_expr -> constr_expr]
+   *
+   *)
+  let gt = Constrintern.intern_constr env sigma t in
+  let r =
+    set_flag (* Notations = no *) Constrextern.print_no_symbol true (fun () ->
+        let eenv = Constrextern.extern_env env sigma in
+        Constrextern.extern_glob_type eenv gt)
+  in
+  if !debug then
+    Feedback.msg_warning
+      Pp.(str "nr [->] " ++ Ppconstr.pr_constr_expr env sigma r);
+  r
+
+let notation_raw env sigma t =
+  try
+    Some (notation_raw env sigma t)
+    (* Due to wrong env passed, usually when traversing terms *)
+  with exn ->
+    Feedback.msg_warning
+      (let iexn = Exninfo.capture exn in
+       Pp.(str "error in notation_raw: " ++ CErrors.iprint iexn));
+    None
+
+module Id = struct
+  type 'a t =
+    { relative : Libnames.qualid
+    ; absolute : Libnames.full_path option
+    ; typ : 'a option
+    }
+
+  (* Uh, this requires to use the global env... *)
+  let type_of_global gref =
+    let env = Global.env () in
+    let typ, _univs = Typeops.type_of_global_in_context env gref in
+    let typ = Arguments_renaming.rename_type typ gref in
+    let bl =
+      Printer.universe_binders_with_opt_names
+        (Environ.universes_of_global env gref)
+        None
+    in
+    let sigma = Evd.from_ctx (UState.of_names bl) in
+    Constrextern.extern_type env sigma (EConstr.of_constr typ)
+
+  let type_of_global gref = try Some (type_of_global gref) with _ -> None
+
+  let path_of_global gref =
+    try Some (Nametab.path_of_global gref) with _ -> None
+
+  let make qid =
+    let gref = intern_reference qid in
+    let typ = Option.bind gref type_of_global in
+    { relative = qid; absolute = Option.bind gref path_of_global; typ }
+
+  let map_typ ~f info = { info with typ = Option.map f info.typ }
+end