[layout engine] Move Coq Layout engine tree to coq-lsp repos.

For now we just host the code here, and compile it. We will add the
selection method later on.

CC: #72

Replaces: jscoq/jscoq#282

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,126 @@
+(************************************************************************)
+(* 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 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"
+end

coq-layout-engine/boxModel.mli

@@ -0,0 +1,73 @@
+(************************************************************************)
+(* 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
+
+(** Simple wrapping in <div> *)
+module Render : sig
+  val to_html :
+    t -> [< Html_types.span_content_fun > `PCDATA `Span ] Tyxml.Html.elt
+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

coq-layout-engine/coq_util.mli

@@ -0,0 +1,32 @@
+(************************************************************************)
+(* coq-layout-engine                                                    *)
+(* Copyright 2021 Inria                                                 *)
+(* Written by Emilio J. Gallego Arias                                   *)
+(************************************************************************)
+(* Status: Very Experimental                                            *)
+(************************************************************************)
+
+val intern_reference : Libnames.qualid -> Names.GlobRef.t option
+
+(* val recover_notation : Environ.env -> Evd.evar_map -> Constrexpr.constr_expr
+   -> Constrexpr.constr_expr option *)
+
+(** [notation_raw env sigma expr] will return [Some raw_expr] if [raw_expr] is
+    the unfolding of a notation [expr] *)
+val notation_raw :
+     Environ.env
+  -> Evd.evar_map
+  -> Constrexpr.constr_expr
+  -> Constrexpr.constr_expr option
+
+(* XXX: Really a reference *)
+module Id : sig
+  type 'a t =
+    { relative : Libnames.qualid
+    ; absolute : Libnames.full_path option
+    ; typ : 'a option
+    }
+
+  val make : Libnames.qualid -> Constrexpr.constr_expr t
+  val map_typ : f:('a -> 'b) -> 'a t -> 'b t
+end

coq-layout-engine/dune

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