Source file `boxModel.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
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 option 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; "box" ] ]

  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
      span "variable" @@ [ name ]
      @ Option.cata (fun typ -> [ span "type" [ to_html typ ] ]) [] 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