Skip to content

Commit 2db1417

Browse files
MM45MM45
committed
Address feedback and fix bug that generated docs for cloned theories
1 parent 1413188 commit 2db1417

2 files changed

Lines changed: 75 additions & 44 deletions

File tree

resources/tests/EasyCrypt_GenDoc_Tutorial.ec renamed to examples/docgen/docgenbasic.ec

Lines changed: 21 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,9 @@
11
(*^
2-
EasyCrypt_GenDoc_Tutorial.ec
2+
EasyCrypt_DocGen_Tutorial.ec
33

44
To generate documentation for a source file, run the following command:
55
{{
6-
<easycrypt-executable> gendoc [-outdir <output-directory>] <source-file>
6+
<easycrypt-executable> docgen [-outdir <output-directory>] <source-file>
77
}}
88
Here, `<easycrypt-executable>` is the path to the EasyCrypt executable on your
99
system, `<output-directory>` is the directory where the generated
@@ -26,7 +26,7 @@
2626
Regular, non-documentation comments like this one are excluded from the
2727
generated documentation file.
2828
*)
29-
require import AllCore.
29+
require import FinType.
3030

3131
(*&
3232
This is a regular documentation comment, which is linked to the next
@@ -43,9 +43,9 @@ require import AllCore.
4343
- theories.
4444

4545
Note that "scoped" items (those specified with, e.g., `local` or `declare`)
46-
are not "documentable", even if their "non-scoped" versions are.
46+
are not "documentable", even if their "non-scoped" versions would be.
4747

48-
In this case, this documentation comment is linked to `type t` below.
48+
This documentation comment is linked to `type t` below.
4949
&*)
5050
type t.
5151

@@ -247,12 +247,12 @@ type s.
247247
(*&
248248
Linking to items is done from the perspective of the outermost theory (`Top`),
249249
so names for items within (sub)theories that are not imported must be qualified.
250-
In other words, if a (sub)theory is not imported by the outside-most theory,
250+
In other words, if a (sub)theory is not imported by the outermost theory,
251251
linking requires the item name to be qualified properly, even within the
252252
(sub)theory itself. For example, to link to `type s` above, something along
253253
the lines of `[go to s in T](>|s)` __does not__ work, but
254254
`[go to s in T](>|T.s)` __does__ (proof: [go to s in T](>|T.s)).
255-
However, if the (sub)theory would be mported at some point in the
255+
However, if the (sub)theory would be imported at some point in the
256256
outermost theory, `[go to s in T](>|s)` __would work__, provided
257257
there are no naming collisions.
258258
&*)
@@ -289,23 +289,32 @@ section.
289289
declare op lf : t -> t.
290290
291291
(*&
292-
If a documentation comment precedes an item that is "undocumentable" due to
293-
its scope, the comment will be dropped, effectively becoming a regular,
294-
non-documentation comment.
292+
If a documentation comment precedes (and would normally be linked to) an item
293+
that is "undocumentable" (e.g., due to its scope), the comment is discarded,
294+
effectively making it a regular, non-documentation comment.
295295
&*)
296296
local module M' = {
297297

298298
}.
299299

300300
(*&
301-
This operator will be documented, but the previous documentation comment is
301+
This operator is documented, but the previous documentation comment is
302302
not visible (indicating it has been dropped).
303303
&*)
304304
op foo = T.a.
305305

306306
end section.
307307

308308
(*&
309-
A documentation comment without any subsequent "documentable" item is
309+
At present, similar to the previously discussed "scoped" items, clones are
310+
"undocumentable" items. As such, any preceding (would-be-linked) documentation
311+
comments are discarded, effectively making them regular, non-documentation
312+
comments.
313+
&*)
314+
clone FinType as FT with
315+
type t <- t.
316+
317+
(*&
318+
A documentation comment without any subsequent item is
310319
discarded, effectively making it a regular, non-documentation comment.
311320
&*)

‎src/ecScope.ml‎

Lines changed: 54 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -370,9 +370,6 @@ let get_gdocstrings (sc : scope) : string list =
370370
let get_ldocentities (sc : scope) : docentity list =
371371
sc.sc_locdoc.docentities
372372

373-
(* let extend_globdoc (sc : scope) (doc : string) : scope =
374-
{ sc with sc_globdoc = sc.sc_globdoc @ [doc] } *)
375-
376373
module DocState = struct
377374
let empty : docstate =
378375
{ docentities = [];
@@ -384,9 +381,6 @@ module DocState = struct
384381
currentmode = None;
385382
currentproc = false; }
386383

387-
(* let push_global (state : docstate) (doc : string) : docstate =
388-
{ state with docentities = GlobalDoc doc :: state.docentities } *)
389-
390384
let start_process (state : docstate) (name : string) (kind : itemkind) (md : mode): docstate =
391385
{ state with
392386
currentname = Some name;
@@ -1274,10 +1268,10 @@ module Op = struct
12741268
match uop.po_locality with
12751269
| `Local -> DocState.prevent_process scope.sc_locdoc
12761270
| `Global -> DocState.start_process scope.sc_locdoc (unloc uop.po_name) `Operator `Specific
1277-
| `Declare -> DocState.start_process scope.sc_locdoc (unloc uop.po_name) `Operator `Abstract}
1271+
| `Declare -> DocState.start_process scope.sc_locdoc (unloc uop.po_name) `Operator `Abstract }
12781272
in
1279-
let scope = {
1280-
scope with
1273+
let scope =
1274+
{ scope with
12811275
sc_locdoc =
12821276
match src with
12831277
| Some src -> DocState.push_srcbl scope.sc_locdoc src
@@ -1519,10 +1513,10 @@ module Op = struct
15191513
match uop.ppo_locality with
15201514
| `Local -> DocState.prevent_process scope.sc_locdoc
15211515
| `Global -> DocState.start_process scope.sc_locdoc (unloc uop.ppo_name) `Operator `Specific
1522-
| `Declare -> DocState.start_process scope.sc_locdoc (unloc uop.ppo_name) `Operator `Abstract}
1516+
| `Declare -> DocState.start_process scope.sc_locdoc (unloc uop.ppo_name) `Operator `Abstract }
15231517
in
1524-
let scope = {
1525-
scope with
1518+
let scope =
1519+
{ scope with
15261520
sc_locdoc =
15271521
match src with
15281522
| Some src -> DocState.push_srcbl scope.sc_locdoc src
@@ -1670,10 +1664,10 @@ module Pred = struct
16701664
match upr.pp_locality with
16711665
| `Local -> DocState.prevent_process scope.sc_locdoc
16721666
| `Global -> DocState.start_process scope.sc_locdoc (unloc upr.pp_name) `Operator `Specific
1673-
| `Declare -> DocState.start_process scope.sc_locdoc (unloc upr.pp_name) `Operator `Abstract}
1667+
| `Declare -> DocState.start_process scope.sc_locdoc (unloc upr.pp_name) `Operator `Abstract }
16741668
in
1675-
let scope = {
1676-
scope with
1669+
let scope =
1670+
{ scope with
16771671
sc_locdoc =
16781672
match src with
16791673
| Some src -> DocState.push_srcbl scope.sc_locdoc src
@@ -1722,10 +1716,10 @@ module Mod = struct
17221716
match lc with
17231717
| `Local -> DocState.prevent_process scope.sc_locdoc
17241718
| `Global -> DocState.start_process scope.sc_locdoc nm `Module `Specific
1725-
| `Declare -> DocState.start_process scope.sc_locdoc nm `Module `Abstract}
1719+
| `Declare -> DocState.start_process scope.sc_locdoc nm `Module `Abstract }
17261720
in
1727-
let scope = {
1728-
scope with
1721+
let scope =
1722+
{ scope with
17291723
sc_locdoc =
17301724
match src with
17311725
| Some src -> DocState.push_srcbl scope.sc_locdoc src
@@ -1799,8 +1793,8 @@ module ModType = struct
17991793
| `Local -> DocState.prevent_process scope.sc_locdoc
18001794
| `Global -> DocState.start_process scope.sc_locdoc (unloc intf.pi_name) `ModuleType `Specific }
18011795
in
1802-
let scope = {
1803-
scope with
1796+
let scope =
1797+
{ scope with
18041798
sc_locdoc =
18051799
match src with
18061800
| Some src -> DocState.push_srcbl scope.sc_locdoc src
@@ -1844,15 +1838,43 @@ module Theory = struct
18441838
(* ------------------------------------------------------------------ *)
18451839
let enter ?(src : string option) (scope : scope) (mode : thmode) (name : symbol) =
18461840
assert (scope.sc_pr_uc = None);
1847-
1848-
let scope =
1849-
let sc_locdoc = scope.sc_locdoc in
1850-
let sc_locdoc =
1851-
let mode = match mode with `Concrete -> `Specific | `Abstract -> `Abstract in
1852-
DocState.start_process sc_locdoc name `Theory mode in
1853-
let sc_locdoc =
1854-
ofold ((^~) DocState.push_srcbl) sc_locdoc src in
1855-
{ scope with sc_locdoc } in
1841+
let sc_locdoc = scope.sc_locdoc in
1842+
let sc_locdoc =
1843+
match src with
1844+
| None -> DocState.prevent_process scope.sc_locdoc
1845+
| Some src ->
1846+
let sc_locdoc =
1847+
DocState.start_process sc_locdoc name `Theory
1848+
(match mode with `Concrete -> `Specific | `Abstract -> `Abstract)
1849+
in
1850+
DocState.push_srcbl sc_locdoc src
1851+
in
1852+
let
1853+
scope = { scope with sc_locdoc }
1854+
in
1855+
(* let scope = *)
1856+
(* let scope = *)
1857+
(* { scope with *)
1858+
(* sc_locdoc = *)
1859+
(* match uax.pa_locality with *)
1860+
(* | `Local -> DocState.prevent_process scope.sc_locdoc *)
1861+
(* | `Global -> DocState.start_process scope.sc_locdoc (unloc uax.pa_name) kind `Specific *)
1862+
(* | `Declare -> DocState.start_process scope.sc_locdoc (unloc uax.pa_name) kind `Abstract} *)
1863+
(* in *)
1864+
(* let scope = *)
1865+
(* { scope with *)
1866+
(* sc_locdoc = *)
1867+
(* match src with *)
1868+
(* | Some src -> DocState.push_srcbl scope.sc_locdoc src *)
1869+
(* | None -> scope.sc_locdoc; } *)
1870+
1871+
(* let sc_locdoc = scope.sc_locdoc in *)
1872+
(* let sc_locdoc = *)
1873+
(* let mode = match mode with `Concrete -> `Specific | `Abstract -> `Abstract in *)
1874+
(* DocState.start_process sc_locdoc name `Theory mode in *)
1875+
(* let sc_locdoc = *)
1876+
(* ofold ((^~) DocState.push_srcbl) sc_locdoc src in *)
1877+
(* { scope with sc_locdoc } in *)
18561878

18571879
subscope scope mode name
18581880

@@ -2217,10 +2239,10 @@ module Ty = struct
22172239
match utyd.pty_locality with
22182240
| `Local -> DocState.prevent_process scope.sc_locdoc
22192241
| `Global -> DocState.start_process scope.sc_locdoc (unloc utyd.pty_name) `Type `Specific
2220-
| `Declare -> DocState.start_process scope.sc_locdoc (unloc utyd.pty_name) `Type `Abstract}
2242+
| `Declare -> DocState.start_process scope.sc_locdoc (unloc utyd.pty_name) `Type `Abstract }
22212243
in
2222-
let scope = {
2223-
scope with
2244+
let scope =
2245+
{ scope with
22242246
sc_locdoc =
22252247
match src with
22262248
| Some src -> DocState.push_srcbl scope.sc_locdoc src

0 commit comments

Comments
 (0)