Source file show_embellish_examples.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
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
open Cairo
open Diagram
open UtilsLib
open Logic.Lambda.Lambda
open Show_exts
module Make (T : Show_text_sig) : Show_embellish_sig = struct
open T
module L = Show.Lambda_show (T)
open L
let rec unfold_cats (cat_id : int) (t : term) : term list =
match t with
| App (App ((Const id | DConst id), t1), t2) when id = cat_id ->
unfold_cats cat_id t1 @ unfold_cats cat_id t2
| _ -> [ t ]
let simplify_cats default_fn recur_fn t l_level level (l_env, env) id_to_sym =
let recurse t l_level level (l_env, env) =
recur_fn t l_level level (l_env, env) id_to_sym
in
match t with
| App (App (((Const id | DConst id) as op), t1), t2)
when is_infix id id_to_sym && "+" = snd @@ id_to_sym id ->
let args = unfold_cats id t1 @ unfold_cats id t2 in
let sep =
hcat
[
n " ";
parenthesize_d @@ recurse op l_level level (l_env, env);
n " ";
]
in
( args
|> List.map (fun arg ->
parenthesize_d @@ recurse arg l_level level (l_env, env))
|> Utils.intersperse sep |> hcat,
false )
| _ -> default_fn recur_fn t l_level level (l_env, env) id_to_sym
let render_constants_with render_fn default_fn recur_fn t l_level level
(l_env, env) id_to_sym =
match t with
| Const id | DConst id -> (render_fn @@ snd @@ id_to_sym id, true)
| _ -> default_fn recur_fn t l_level level (l_env, env) id_to_sym
let logic_const name =
let name =
match name with
| "Ex" -> "∃"
| "ExUni" -> "∃!"
| "Ex_l" -> "∃ₗ"
| "Ex_t" -> "∃ₜ"
| "All" -> "∀"
| "All_t" -> "∀ₜ"
| "TOP" -> "⊤"
| "The" -> "ι"
| "&" -> "∧"
| ">" -> "⇒"
| "~" -> "¬"
| _ -> name
in
match name with
| "∃!" | "∃ₗ" | "∃ₜ" | "∃" | "∀" | "∀ₜ" | "ι" ->
n name
|> reframe (fun exts -> { exts with w = exts.w -. (extents (n " ")).w })
| "∧" | "⇒" -> n name
| _ -> b name
let symbol_with_arity s =
let regexp = Str.regexp "^\\([A-Za-z]+\\)[0-9]+$" in
if Str.string_match regexp s 0 then
let s' = Str.matched_string s in
Str.matched_group 1 s'
else s
let tag_derived_tree_cst s = symbol_with_arity s
let string_const = function "e" -> n "ε" | name -> i name
let render_with_color c default_fn recur_fn t l_level level (l_env, env)
id_to_sym =
let d, b = default_fn recur_fn t l_level level (l_env, env) id_to_sym in
(color c d, b)
[@@warning "-32"]
let big_parens (d : diagram) : diagram =
let paren_height = (extents @@ tighten_text @@ n "(").h in
let d_height = (extents d).h in
let y_scale = d_height /. paren_height in
let x_scale = y_scale ** 0.125 in
let scale_paren p =
n p |> tighten_text |> centerY
|> scale (x_scale, y_scale)
|> pad_abs ~left:2.
in
hcat [ scale_paren "("; d; scale_paren ")" ]
let tag_style default_fn recur_fn t l_level level (l_env, env) id_to_sym =
let recurse t l_level level (l_env, env) =
recur_fn t l_level level (l_env, env) id_to_sym
in
match t with
| App (t1, t2) -> (
let args, fn = unfold_app [ t2 ] t1 in
let arg_diagrams =
List.map (fun x -> fst @@ recurse x l_level level (l_env, env)) args
in
match fn with
| Const _ | DConst _ ->
( Tree.T
( parenthesize_d @@ recurse fn l_level level (l_env, env),
List.map Tree.singleton arg_diagrams )
|> Tree.to_diagram ~vgap:10. |> centerY
|> setup (fun cr -> set_line_width cr 1.),
true )
| Var _ | LVar _ ->
( hcat
[
parenthesize_d @@ recurse fn l_level level (l_env, env);
big_parens @@ hcat @@ Utils.intersperse (n ", ") arg_diagrams;
]
|> centerX,
false )
| _ -> default_fn recur_fn t l_level level (l_env, env) id_to_sym)
| _ -> default_fn recur_fn t l_level level (l_env, env) id_to_sym
let embellishments = function
| "Strings" | "strings" | "anglais" | "francais" ->
simplify_cats >> render_constants_with string_const
| "labelled_logic" | "logic" | "logique" | "HybridLogic" | "semantics" ->
render_constants_with logic_const
| "Trees" | "Derived_trees" | "trees" | "derived_trees" ->
fun x y z t u v w ->
tag_style x y z t u v (fun x ->
let b, s = w x in
(b, tag_derived_tree_cst s))
| "discourse_grammar" | "Derivations" | "derivations" | "Derivation_trees"
| "derivation_trees" | "TAG" | "DSTAG" ->
fun x y z t u v w ->
tag_style x y z t u v (fun x ->
let b, s = w x in
(b, s))
| _ -> fun x -> x
let embellishments_engines = function
| Rendering_config.STRINGS ->
simplify_cats >> render_constants_with string_const
| Rendering_config.LOGIC -> render_constants_with logic_const
| Rendering_config.DERIVED_TREES ->
fun x y z t u v w ->
tag_style x y z t u v (fun x ->
let b, s = w x in
(b, tag_derived_tree_cst s))
| Rendering_config.TREES ->
fun x y z t u v w ->
tag_style x y z t u v (fun x ->
let b, s = w x in
(b, s))
| Rendering_config.DEFAULT -> fun x -> x
let embellishments_functions sig_name config =
try
embellishments_engines
(Utils.StringMap.find sig_name (Rendering_config.engines config))
with Not_found -> fun x -> x
end