diff --git a/INSTALL.md b/INSTALL.md index a9808fe4f..99a9a91de 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -522,6 +522,9 @@ proceed to [install EasyCrypt from Source](#installing-easycrypt-from-source). - [OCaml ini-files](https://opam.ocaml.org/packages/ocaml-inifiles/) (version >= 1.2) Additional resources: - http://archive.ubuntu.com/ubuntu/pool/universe/o/ocaml-inifiles +- [OCaml Markdown](https://github.com/gildor478/ocaml-markdown) + Additional resources: + - https://opam.ocaml.org/packages/markdown - [Python3](https://www.python.org/downloads) You also need to install the following libraries: - [Python3 YAML](https://pyyaml.org/wiki/PyYAMLDocumentation) diff --git a/assets/.gitignore b/assets/.gitignore new file mode 100644 index 000000000..e69de29bb diff --git a/assets/styles/styles.css b/assets/styles/styles.css new file mode 100644 index 000000000..e3bdc9944 --- /dev/null +++ b/assets/styles/styles.css @@ -0,0 +1,228 @@ +/* General Styling */ +/* Body */ +body { + font-family: "-apple-system", "BlinkMacSystemFont", "Roboto", "Arial", sans-serif; + line-height: 1.2; + font-size: 16px; + margin: 0; + padding: 0; + color: #333; + background-color: #f9f9f9; +} + +/* Code blocks */ +pre { + font-family: "Fira Code", "Consolas", monospace; + font-size: 1rem; + padding: 5px; + border-radius: 1px; + color: #2d2d2d; + background-color: #ecf0f1; +} + +/* Inline code */ +code { + font-family: "Fira Code", "Consolas", monospace; + font-size: 1rem; + color: #d6336c; +} + +/* Headings */ +h1, h2, h3, h4, h5, h6 { + font-family: "Roboto", "Arial", sans-serif; + font-weight: 600; + color: #1a1a1a; + margin-bottom: 0.5em; +} + +h1 { + font-size: 2.25rem; +} +h2 { + font-size: 2rem; +} +h3 { + font-size: 1.75rem; +} +h4 { + font-size: 1.5rem; +} +h5 { + font-size: 1.25rem; +} +h6 { + font-size: 1rem; +} + +/* Links */ +a { + font-family: "Roboto", "Arial", sans-serif; + color: #007bff; + text-decoration: none; +} + +a:hover { + color: #0056b3; + text-decoration: underline; +} + +.serif-text { + font-family: "Times New Roman", "Times", serif; + font-size: 1rem; + color: #333; +} + +/* Specific styling */ + +/* Sidebar */ +.sidebar { + width: 200px; + background-color: #2c3e50; + color: #ecf0f1; + position: fixed; + height: 100%; + overflow: auto; +} + +.sidebar-title { + padding: 20px; + color: #ecf0f1; + background-color: #34495e; + margin-bottom: 20px; +} + +.sidebar-title h2 { + font-size: 1.5em; + margin-bottom: 5px; + color: #ecf0f1; +} + +.sidebar-title .sidebar-title-theory { + font-size: 1.2em; + color: #3498db; +} + +.sidebar-title-theory { + word-wrap: break-word; + overflow-wrap: break-word; + white-space: normal; +} + +.sidebar-elems { + padding: 20px; +} + +.sidebar-section-list { + list-style: none; + padding: 0; +} + +.sidebar-section-list li { + margin: 15px 0; +} + +.sidebar-section-list li a { + color: #ecf0f1; + font-weight: bold; +} + +/* Main content */ +main { + margin-left: 220px; + padding: 20px; + max-width: 960px; +} + +.page-heading-container { + border-bottom: 2px solid #ddd; + padding-bottom: 5px; + margin-bottom: 20px; +} + +.page-heading-container .page-heading { + margin-block-end: 5px; +} + +.page-heading-container .page-subheading { + margin-block-start: 0px; + margin-block-end: 5px; + font-size: 1.2em; +} + +/* Sections */ +.item-section { + margin-bottom: 40px; +} + +.section-heading { + color: #34495e; + border-bottom: 2px solid #ddd; + padding-bottom: 10px; + margin-bottom: 20px; +} + +/* Item lists */ +.item-list { + list-style: none; + padding: 0; +} + +.item-entry { + display: flex; + flex-direction: column; + margin-bottom: 20px; +} + +.item-name-desc-container { + display: flex; + align-items: flex-start; +} + +.item-name { + width: 200px; + font-weight: bold; + color: #2980b9; + white-space: normal; + overflow-wrap: break-word; +} + +.item-basic-desc { + flex: 1; + margin-left: 10px; +} + +.item-basic-desc p { + margin-top: 0px; +} + +.item-details { + margin-left: 210px; +} + +.item-details summary { + cursor: pointer; + color: #3498db; + font-weight: bold; +} + +.item-details summary:hover { + text-decoration: underline; +} + +.item-details-par { + margin-top: 10px; +} + +/* Source code */ +pre.source { + border: 2px solid #bdc3c7; + padding: 10px; + border-radius: 5px; + overflow-x: auto; + white-space: pre-wrap; +} + +/* Introduction section */ +.intro-section { + margin-bottom: 40px; +} diff --git a/dune b/dune index e19b69c5a..7c8edf709 100644 --- a/dune +++ b/dune @@ -1,9 +1,13 @@ -(dirs 3rdparty src etc theories examples scripts) +(dirs 3rdparty src etc theories examples assets scripts) (install (section (site (easycrypt commands))) (files (scripts/testing/runtest as runtest))) +(install + (section (site (easycrypt doc))) + (files (assets/styles/styles.css as styles.css))) + (install (section (bin)) (files (scripts/testing/bin-ec-runtest as ec-runtest))) diff --git a/dune-project b/dune-project index b285ee175..85f142616 100644 --- a/dune-project +++ b/dune-project @@ -10,7 +10,7 @@ (package (name easycrypt) - (sites (lib theories) (libexec commands) (lib config)) + (sites (lib theories) (libexec commands) (lib doc) (lib config)) (depends (ocaml (>= 4.08.0)) (batteries (>= 3)) @@ -19,6 +19,7 @@ dune dune-build-info dune-site + markdown (pcre2 (>= 8)) (why3 (and (>= 1.8.0) (< 1.9))) yojson diff --git a/easycrypt.opam b/easycrypt.opam index 47ea3eb08..08bdb40ea 100644 --- a/easycrypt.opam +++ b/easycrypt.opam @@ -7,6 +7,7 @@ depends: [ "dune" {>= "3.13"} "dune-build-info" "dune-site" + "markdown" "pcre2" {>= "8"} "why3" {>= "1.8.0" & < "1.9"} "yojson" diff --git a/examples/docgen/docgenbasic.ec b/examples/docgen/docgenbasic.ec new file mode 100644 index 000000000..691efa23e --- /dev/null +++ b/examples/docgen/docgenbasic.ec @@ -0,0 +1,320 @@ +(*^ + EasyCrypt_DocGen_Tutorial.ec + + To generate documentation for a source file, run the following command: + {{ + docgen [-outdir ] + }} + Here, `` is the path to the EasyCrypt executable on your + system, `` is the directory where the generated + documentation files will be stored, and `` is the path to the + source file you want to generate documentation for. You may omit the output + directory, in which case the tool defaults to the directory of the source file. + + This is a file documentation comment. In the generated documentation file, this + comment appears at the top. File documentation comments are typically used for + summaries, overviews, and meta-information about the file. +^*) + +(*^ + This is an additional file-documentation comment. In the generated + documentation, it is added as a paragraph below the (last paragraph of the) + previous file documentation comment. +^*) + +(* + Regular, non-documentation comments like this one are excluded from the + generated documentation file. +*) +require import FinType. + +(*& + This is a regular documentation comment, which is linked to the next + "documentable" item. In the generated documentation file, it appears as + documentation for the linked item. + + At the time of writing, the "documentable" items are: + - types, + - operators, + - axioms, + - lemmas, + - module types, + - modules, and + - theories. + + Note that "scoped" items (those specified with, e.g., `local` or `declare`) + are not "documentable", even if their "non-scoped" versions would be. + + This documentation comment is linked to `type t` below. +&*) +type t. + +(*& + It is not necessary to close a documentation comment with a matching closing + delimiter. Only the opening delimiter determines the type of comment. However, + it is good practice to use a matching closing delimiter. +*) +type u. + +(*& + Multiple documentation comments can be placed consecutively without any + "documentable" items in between. All of these comments are linked to the next + "documentable" item. However, starting with the second comment, each will be + hidden under an un-foldable "details" section, indicated by a clickable arrow. + Even if fewer than two documentation comments are linked to an item, this + "details" section always contains the source code for the item, except in the + case of (sub)theories. +&*) + +(*& + As an example, both the previous and this documentation comment are linked to + `type v` below. The first comment is shown by default, while this second one + is initially hidden, but can be revealed by unfolding the corresponding + "details" section. +&*) +type v. + +(*& + Documentation comments can be interleaved with non-documentation comments, + even before the item to which the documentation comments are linked. +&*) + +(* + This is a non-documentation comment between two documentation comments linked + to the same item. +*) + +(*& + Both the previous and this __documentation__ comment are correctly linked to + `type w` below, even though they are separated by a __non-documentation__ + comment. +&*) +type w. + +(*^ + File documentation comments can be placed anywhere in the file. Each comment + is added as a new paragraph below the previous one. However, it is + considered good practice to place file documentation comments at the + beginning of the file whenever possible. +^*) + +(*& + __Any__ comments nested inside documentation comments + are excluded from the generated documentation file. + (* This comment is excluded from the generated documentation file *) + (*& This comment is excluded from the generated documentation file &*) + (*^ This comment is excluded from the generated documentation file ^*) + However, anything outside these nested comments (but within + the documentation comment, of course) is included. +&*) +type x. + +(* + All "documentable" items are included in the generated documentation file, whether + or not they have a corresponding documentation comment. The source code + of each item is always included, though it is initially hidden under an + un-foldable "details" section. If there is no corresponding documentation + comment, a default message is shown, referring to the details section for the + source code. +*) +type y. + +(*& + All documentation comments can be + formatted using (a non-standard dialect of) Markdown. + The following is supported. + + As first non-blank character on a line (followed by a space): + - \! indicates a heading (one for largest heading, two for second-largest + heading, etc.); + - \*, \+, or \- indicate an item of an unordered list; + - \# indicates an item of an ordered list; and + - \> indicates (a line of) a blockquote. + + As delimiters: + - \{\{ and \}\} delimit a code block (both the delimiters and content should be + on separate lines); + - \` delimits inline code (e.g., `inline code`); + - \* delimits bold text (e.g., *bold text* ); and + - \__ delimits emphasized text (e.g., __emph text__). + + Any special characters can be escaped with a backslash (e.g., \`). + + Hyperlinks are formatted as `[]()` + (e.g., [EasyCrypt GitHub repository](https://github.com/EasyCrypt/easycrypt)). +&*) +type z. + +(*& + It is possible to link to other documented items *within + the theory's scope* (i.e., items defined in the file itself or + imported from other theories). The syntax is similar to + that for hyperlinks: `[](>|)`, + Here, `` is one of the following: + - `Ty` (or `Type`), + - `Op` (or `Operator`), + - `Ax` (or `Axiom`), + - `Lem` (or `Lemma`), + - `ModTy` (or `ModuleType`), + - `Mod` (or `Module`), and + - `Th` (or `Theory`). + + `` is the name of the item as you would print it in the theory + itself. Particularly, this means that the name may need to be qualified, + depending on the imports in the theory. For example, `[go to type t above](>Ty|t)` + becomes [go to type t above](>Ty|t). However, `[go to operator t below](>Op|t)` + becomes [go to operator t below](>Op|t). (Note that, even though the linked + type and operator are both referred to with the same name, the correct item is + linked due to the specification of the item kind.) + + If you omit ``, the documentation tool checks each item kind in the + order listed above for the given `` and links to the first match. + E.g., instead of `[go to type t above](>Ty|t)`, you can use `[go to type t + above](>|t)` (proof: [go to type t above](>|t)). However, you still need + to explicitly specify the `Op` kind for operator `t` below, because the + documentation tool checks the `Type` kind before the `Operator` kind, which + already results in a match. +&*) +op f : u -> v. + +(*& This is a documented operator &*) +op t : v -> w. + +(*& + The generated documentation file contains a section for each item kind. Within each + section, items are displayed in the order they appear in the source. +&*) +axiom ax : true. + +(*& + If there are no items of a certain kind, + the generated documentation file does not contain a section for that kind. + For example, the generated documentation file for this theory does not + contain a section for module types. + + The navigation bar on the left-hand side of the generated documentation file + shows only the sections that are present and provides links to them + for convenience. +&*) +lemma lem : true. +proof. by trivial. qed. + +(*& + Currently, individual procedures inside of modules (and module types) cannot + be documented using documentation comments. For the time being, a + (unsatisfactory) workaround is to use regular comments within the module (or + module type), which appear in the source code for the module (or module type) + in the generated documentation file. +&*) +module M = { + (* + This regular comment appears in the source code + for this module in the generated documentation file. + *) + proc p() : int = { + return 1; + } +}. + +(*& + Theories are special as "documentable" items. They appear as documented items + in the generated documentation file for their parent theory __and__ + receive their own documentation file, in turn documenting all their + "documentable" items. This file has a subheading indicating the subtheory and + links to entry of the (sub)theory in the parent theory's documentation file. + + The file name for a (sub)theory follows this pattern: `Y!Z`, where `Y`, and + `Z` represent the parent theory and (sub)theory, respectively. (This works + recursively: `Y` may itself be a (sub)theory of another theory `X`, in which + case the file name becomes `X!Y!Z`.) + + The "introductory text" for the (sub)theory, which you would usually put in + file documentation comments, is drawn from the regular documentation comments + in the parent theory. In the parent theory's documentation file, the + (sub)theory's name links to the corresponding (sub)theory documentation file. + + No source code is shown for subtheories in the parent theory's documentation + file. +&*) +theory T. + +(*& + This item is documented in the documentation file corresponding to + (sub)theory `T'. +&*) +type s. + +(*& + Linking to items is done from the perspective of the outermost theory (`Top`), + so names for items within (sub)theories that are not imported must be qualified. + In other words, if a (sub)theory is not imported by the outermost theory, + linking requires the item name to be qualified properly, even within the + (sub)theory itself. For example, to link to `type s` above, something along + the lines of `[go to s in T](>|s)` __does not__ work, but + `[go to s in T](>|T.s)` __does__ (proof: [go to s in T](>|T.s)). + However, if the (sub)theory would be imported at some point in the + outermost theory, `[go to s in T](>|s)` __would work__, provided + there are no naming collisions. +&*) +op a : s -> s. + +(*& + Linking to items in a parent theory works as expected. For example `[go to w + in parent](>|w)` would create a link to the entry for `w` in the parent + theory's documentation file (proof: [go to w in parent](>|w)). +&*) +op b : w -> w. + +(*& + The documentation mechanism for theories works recursively. + For example, theory `U` below is treated in the documentation file for `T` in the + same way that `T` is treated in the documentation file for the outermost theory. + In addition to appearing in `T`'s documentation file, `U` also receives its own + documentation file, similar to `T`, but now linking back to `T` rather than the + outermost theory. +&*) +abstract theory U. + +end U. + +end T. + + +section. + +(* + As mentioned before, "scoped" items are never documented, even + if their "non-scoped" version are. +*) +declare op lf : t -> t. + +(*& + If a documentation comment precedes (and would normally be linked to) an item + that is "undocumentable" (e.g., due to its scope), the comment is discarded, + effectively making it a regular, non-documentation comment. +&*) +local module M' = { + +}. + +(*& + This operator is documented, but the previous documentation comment is + not visible (indicating it has been dropped). +&*) +op foo = T.a. + +end section. + +(*& + At present, similar to the previously discussed "scoped" items, clones are + "undocumentable" items. As such, any preceding (would-be-linked) documentation + comments are discarded, effectively making them regular, non-documentation + comments. +&*) +clone FinType as FT with + type t <- t. + +(*& + A documentation comment without any subsequent item is + discarded, effectively making it a regular, non-documentation comment. +&*) diff --git a/src/dune b/src/dune index d3e809314..75cb7e8ab 100644 --- a/src/dune +++ b/src/dune @@ -15,7 +15,7 @@ (public_name easycrypt.ecLib) (foreign_stubs (language c) (names eunix)) (modules :standard \ ec) - (libraries batteries camlp-streams dune-build-info dune-site inifiles pcre2 why3 yojson zarith) + (libraries batteries camlp-streams dune-build-info dune-site inifiles markdown markdown.html pcre2 tyxml why3 yojson zarith) ) (executable diff --git a/src/ec.ml b/src/ec.ml index d61bd4329..48da43b80 100644 --- a/src/ec.ml +++ b/src/ec.ml @@ -413,6 +413,8 @@ let main () = interactive : bool; eco : bool; gccompact : int option; + docgen : bool; + outdirp : string option; } end in @@ -467,7 +469,9 @@ let main () = ; terminal = terminal ; interactive = true ; eco = false - ; gccompact = None } + ; gccompact = None + ; docgen = false + ; outdirp = None } end @@ -494,13 +498,54 @@ let main () = ; terminal = terminal ; interactive = false ; eco = cmpopts.cmpo_noeco - ; gccompact = cmpopts.cmpo_compact } + ; gccompact = cmpopts.cmpo_compact + ; docgen = false + ; outdirp = None } end | `Runtest _ -> (* Eagerly executed *) assert false + + | `DocGen docopts -> begin + let name = docopts.doco_input in + + begin try + let ext = Filename.extension name in + ignore (EcLoader.getkind ext : EcLoader.kind) + with EcLoader.BadExtension ext -> + Format.eprintf "do not know what to do with %s@." ext; + exit 1 + end; + + let prvoff = { + prvo_maxjobs = None; + prvo_timeout = None; + prvo_cpufactor = None; + prvo_provers = None; + prvo_pragmas = []; + prvo_ppwidth = None; + prvo_checkall = false; + prvo_profile = false; + prvo_iterate = false; + prvo_why3server = None; } + in + + let terminal = + lazy (T.from_channel ~name (open_in name)) + in + + { prvopts = prvoff + ; input = Some name + ; terminal = terminal + ; interactive = false + ; eco = true + ; gccompact = None + ; docgen = true + ; outdirp = docopts.doco_outdirp } + end + in (match state.input with @@ -511,9 +556,10 @@ let main () = | Some pwd -> EcCommands.addidir pwd); (* Check if the .eco is up-to-date and exit if so *) - oiter - (fun input -> if EcCommands.check_eco input then exit 0) - state.input; + (if not state.docgen then + oiter + (fun input -> if EcCommands.check_eco input then exit 0) + state.input); let finalize_input input scope = match input with @@ -606,8 +652,13 @@ let main () = EcCommands.cm_iterate = state.prvopts.prvo_iterate; } in + let checkproof = not state.docgen in + EcCommands.initialize ~restart - ~undo:state.interactive ~boot:ldropts.ldro_boot ~checkmode; + ~undo:state.interactive + ~boot:ldropts.ldro_boot + ~checkmode + ~checkproof; (try List.iter EcCommands.apply_pragma state.prvopts.prvo_pragmas with EcCommands.InvalidPragma x -> @@ -633,8 +684,9 @@ let main () = | Some (`Int i) -> Some i | _ -> None); begin - match EcLocation.unloc (T.next terminal) with - | EP.P_Prog (commands, locterm) -> + match snd_map EcLocation.unloc (T.next terminal) with + | (src, EP.P_Prog (commands, locterm)) -> + let src = String.strip src in terminate := locterm; List.iter (fun p -> @@ -643,7 +695,7 @@ let main () = let break = p.EP.gl_debug = Some `Break in let ignore_fail = ref false in try - let tdelta = EcCommands.process ~timed ~break p.EP.gl_action in + let tdelta = EcCommands.process ~src ~timed ~break p.EP.gl_action in if p.EP.gl_fail then begin ignore_fail := true; raise (EcScope.HiScopeError (None, "this command is expected to fail")) @@ -670,11 +722,15 @@ let main () = end) commands - | EP.P_Undo i -> + | _, EP.P_DocComment doc -> + EcCommands.doc_comment doc + + | _, EP.P_Undo i -> EcCommands.undo i - | EP.P_Exit -> + | _, EP.P_Exit -> terminate := true end; + T.finish `ST_Ok terminal; state.gccompact |> Option.iter (fun i -> @@ -689,6 +745,8 @@ let main () = T.finalize terminal; if not state.eco then finalize_input state.input (EcCommands.current ()); + if state.docgen then + EcDoc.generate_html ?outdirp:state.outdirp state.input (EcCommands.current ()); exit 0 end; with diff --git a/src/ecCommands.ml b/src/ecCommands.ml index f2da6001d..9f647c52b 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -401,15 +401,15 @@ let process_print scope p = exception Pragma of [`Reset | `Restart] (* -------------------------------------------------------------------- *) -let rec process_type (scope : EcScope.scope) (tyd : ptydecl located) = +let rec process_type ?(src : string option) (scope : EcScope.scope) (tyd : ptydecl located) = EcScope.check_state `InTop "type" scope; - let scope = EcScope.Ty.add scope tyd in + let scope = EcScope.Ty.add ?src scope tyd in EcScope.notify scope `Info "added type: `%s'" (unloc tyd.pl_desc.pty_name); scope (* -------------------------------------------------------------------- *) -and process_types (scope : EcScope.scope) tyds = - List.fold_left process_type scope tyds +and process_types ?(src : string option) (scope : EcScope.scope) tyds = + List.fold_left (process_type ?src) scope tyds (* -------------------------------------------------------------------- *) and process_subtype (scope : EcScope.scope) (subtype : psubtype located) = @@ -431,19 +431,19 @@ and process_tycinst (scope : EcScope.scope) (tci : ptycinstance located) = EcScope.Ty.add_instance scope (Pragma.get ()).pm_check tci (* -------------------------------------------------------------------- *) -and process_module (scope : EcScope.scope) m = +and process_module ?(src : string option) (scope : EcScope.scope) m = EcScope.check_state `InTop "module" scope; - EcScope.Mod.add scope m + EcScope.Mod.add ?src scope m (* -------------------------------------------------------------------- *) -and process_interface (scope : EcScope.scope) intf = +and process_interface ?(src : string option) (scope : EcScope.scope) intf = EcScope.check_state `InTop "interface" scope; - EcScope.ModType.add scope intf + EcScope.ModType.add ?src scope intf (* -------------------------------------------------------------------- *) -and process_operator (scope : EcScope.scope) (pop : poperator located) = +and process_operator ?(src : string option) (scope : EcScope.scope) (pop : poperator located) = EcScope.check_state `InTop "operator" scope; - let op, axs, scope = EcScope.Op.add scope pop in + let op, axs, scope = EcScope.Op.add ?src scope pop in let ppe = EcPrinting.PPEnv.ofenv (EcScope.env scope) in List.iter (fun { pl_desc = name } -> @@ -455,14 +455,14 @@ and process_operator (scope : EcScope.scope) (pop : poperator located) = scope (* -------------------------------------------------------------------- *) -and process_procop (scope : EcScope.scope) (pop : pprocop located) = +and process_procop ?(src : string option) (scope : EcScope.scope) (pop : pprocop located) = EcScope.check_state `InTop "operator" scope; - EcScope.Op.add_opsem scope pop + EcScope.Op.add_opsem ?src scope pop (* -------------------------------------------------------------------- *) -and process_predicate (scope : EcScope.scope) (p : ppredicate located) = +and process_predicate ?(src : string option) (scope : EcScope.scope) (p : ppredicate located) = EcScope.check_state `InTop "predicate" scope; - let op, scope = EcScope.Pred.add scope p in + let op, scope = EcScope.Pred.add ?src scope p in let ppe = EcPrinting.PPEnv.ofenv (EcScope.env scope) in EcScope.notify scope `Info "added predicate %s %a" (unloc p.pl_desc.pp_name) (EcPrinting.pp_added_op ppe) op; @@ -486,9 +486,9 @@ and process_abbrev (scope : EcScope.scope) (a : pabbrev located) = scope (* -------------------------------------------------------------------- *) -and process_axiom (scope : EcScope.scope) (ax : paxiom located) = +and process_axiom ?(src : string option) (scope : EcScope.scope) (ax : paxiom located) = EcScope.check_state `InTop "axiom" scope; - let (name, scope) = EcScope.Ax.add scope (Pragma.get ()).pm_check ax in + let (name, scope) = EcScope.Ax.add ?src scope (Pragma.get ()).pm_check ax in name |> EcUtils.oiter (fun x -> match (unloc ax).pa_kind with @@ -497,9 +497,9 @@ and process_axiom (scope : EcScope.scope) (ax : paxiom located) = scope (* -------------------------------------------------------------------- *) -and process_th_open (scope : EcScope.scope) (loca, abs, name) = +and process_th_open ?(src : string option) (scope : EcScope.scope) (loca, abs, name) = EcScope.check_state `InTop "theory" scope; - EcScope.Theory.enter scope (if abs then `Abstract else `Concrete) (unloc name) loca + EcScope.Theory.enter ?src scope (if abs then `Abstract else `Concrete) (unloc name) loca (* -------------------------------------------------------------------- *) and process_th_close (scope : EcScope.scope) (clears, name) = @@ -557,7 +557,7 @@ and process_th_require1 ld scope (nm, (sysname, thname), io) = try_finally (fun () -> let commands = EcIo.parseall (EcIo.from_file filename) in let commands = - List.fold_left + List.fold_left (fun scope g -> process_internal subld scope g.gl_action) iscope commands in commands) @@ -614,19 +614,21 @@ and process_sct_close (scope : EcScope.scope) name = EcScope.Section.exit scope name (* -------------------------------------------------------------------- *) -and process_tactics (scope : EcScope.scope) t = +(* Add and store src for proofs *) +and process_tactics ?(src : string option) (scope : EcScope.scope) t = let mode = (Pragma.get ()).pm_check in match t with - | `Actual t -> snd (EcScope.Tactics.process scope mode t) - | `Proof -> EcScope.Tactics.proof scope + | `Actual t -> snd (EcScope.Tactics.process ?src scope mode t) + | `Proof -> EcScope.Tactics.proof ?src scope (* -------------------------------------------------------------------- *) -and process_save (scope : EcScope.scope) ed = +(* Add and store src for proofs *) +and process_save ?(src : string option) (scope : EcScope.scope) ed = let (oname, scope) = match unloc ed with - | `Qed -> EcScope.Ax.save scope - | `Admit -> EcScope.Ax.admit scope - | `Abort -> (None, EcScope.Ax.abort scope) + | `Qed -> EcScope.Ax.save ?src scope + | `Admit -> EcScope.Ax.admit ?src scope + | `Abort -> (None, EcScope.Ax.abort ?src scope) in oname |> EcUtils.oiter (fun x -> EcScope.notify scope `Info "added lemma: `%s'" x); @@ -748,25 +750,25 @@ and process_dump scope (source, tc) = scope (* -------------------------------------------------------------------- *) -and process (ld : Loader.loader) (scope : EcScope.scope) g = +and process ?(src : string option) (ld : Loader.loader) (scope : EcScope.scope) g = let loc = g.pl_loc in let scope = match match g.pl_desc with - | Gtype t -> `Fct (fun scope -> process_types scope (List.map (mk_loc loc) t)) + | Gtype t -> `Fct (fun scope -> process_types ?src scope (List.map (mk_loc loc) t)) | Gsubtype t -> `Fct (fun scope -> process_subtype scope (mk_loc loc t)) | Gtypeclass t -> `Fct (fun scope -> process_typeclass scope (mk_loc loc t)) | Gtycinstance t -> `Fct (fun scope -> process_tycinst scope (mk_loc loc t)) - | Gmodule m -> `Fct (fun scope -> process_module scope m) - | Ginterface i -> `Fct (fun scope -> process_interface scope i) - | Goperator o -> `Fct (fun scope -> process_operator scope (mk_loc loc o)) - | Gprocop o -> `Fct (fun scope -> process_procop scope (mk_loc loc o)) - | Gpredicate p -> `Fct (fun scope -> process_predicate scope (mk_loc loc p)) + | Gmodule m -> `Fct (fun scope -> process_module ?src scope m) + | Ginterface i -> `Fct (fun scope -> process_interface ?src scope i) + | Goperator o -> `Fct (fun scope -> process_operator ?src scope (mk_loc loc o)) + | Gprocop o -> `Fct (fun scope -> process_procop ?src scope (mk_loc loc o)) + | Gpredicate p -> `Fct (fun scope -> process_predicate ?src scope (mk_loc loc p)) | Gnotation n -> `Fct (fun scope -> process_notation scope (mk_loc loc n)) | Gabbrev n -> `Fct (fun scope -> process_abbrev scope (mk_loc loc n)) - | Gaxiom a -> `Fct (fun scope -> process_axiom scope (mk_loc loc a)) - | GthOpen name -> `Fct (fun scope -> process_th_open scope name) + | Gaxiom a -> `Fct (fun scope -> process_axiom ?src scope (mk_loc loc a)) + | GthOpen name -> `Fct (fun scope -> process_th_open ?src scope name) | GthClose info -> `Fct (fun scope -> process_th_close scope info) | GthClear info -> `Fct (fun scope -> process_th_clear scope info) | GthRequire name -> `Fct (fun scope -> process_th_require ld scope name) @@ -780,11 +782,11 @@ and process (ld : Loader.loader) (scope : EcScope.scope) g = | Gprint p -> `Fct (fun scope -> process_print scope p; scope) | Gsearch qs -> `Fct (fun scope -> process_search scope qs; scope) | Glocate x -> `Fct (fun scope -> process_locate scope x; scope) - | Gtactics t -> `Fct (fun scope -> process_tactics scope t) + | Gtactics t -> `Fct (fun scope -> process_tactics ?src scope t) | Gtcdump info -> `Fct (fun scope -> process_dump scope info) | Grealize p -> `Fct (fun scope -> process_realize scope p) | Gprover_info pi -> `Fct (fun scope -> process_proverinfo scope pi) - | Gsave ed -> `Fct (fun scope -> process_save scope ed) + | Gsave ed -> `Fct (fun scope -> process_save ?src scope ed) | Gpragma opt -> `State (fun scope -> process_pragma scope opt) | Goption opt -> `Fct (fun scope -> process_option scope opt) | Gaddrw hint -> `Fct (fun scope -> process_addrw scope hint) @@ -827,7 +829,7 @@ type checkmode = { cm_iterate : bool; } -let initial ~checkmode ~boot = +let initial ~checkmode ~boot ~checkproof = let checkall = checkmode.cm_checkall in let profile = checkmode.cm_profile in let poptions = { EcScope.Prover.empty_options with @@ -850,7 +852,14 @@ let initial ~checkmode ~boot = scope [tactics; prelude] in let scope = EcScope.Prover.set_default scope poptions in - let scope = if checkall then EcScope.Prover.full_check scope else scope in + let scope = if checkproof then + begin + if checkall then + EcScope.Prover.full_check scope + else scope + end + else EcScope.Prover.check_proof scope false + in EcScope.freeze scope @@ -890,10 +899,10 @@ let push_context scope context = |> omap (fun st -> context.ct_current :: st); } (* -------------------------------------------------------------------- *) -let initialize ~restart ~undo ~boot ~checkmode = +let initialize ~restart ~undo ~boot ~checkmode ~checkproof = assert (restart || EcUtils.is_none !context); if restart then Pragma.set dpragma; - context := Some (rootctxt ~undo (initial ~checkmode ~boot)) + context := Some (rootctxt ~undo (initial ~checkmode ~boot ~checkproof)) (* -------------------------------------------------------------------- *) type notifier = EcGState.loglevel -> string Lazy.t -> unit @@ -925,19 +934,30 @@ let undo (olduuid : int) = context := Some (pop_context (oget !context)) done +(* -------------------------------------------------------------------- *) +let doc_comment (doc : [`Global | `Item] * string) : unit = + let current = oget !context in + let scope = current.ct_current in + let scope = EcScope.DocComment.add scope doc in + + context := Some (push_context scope current) + (* -------------------------------------------------------------------- *) let reset () = context := Some (rootctxt (oget !context).ct_root) (* -------------------------------------------------------------------- *) -let process ?(timed = false) ?(break = false) (g : global_action located) : float option = +let process + ?(src : string option) ?(timed = false) ?(break = false) + (g : global_action located) : float option += ignore break; let current = oget !context in let scope = current.ct_current in try - let (tdelta, oscope) = EcUtils.timed (process loader scope) g in + let (tdelta, oscope) = EcUtils.timed (process ?src loader scope) g in oscope |> oiter (fun scope -> context := Some (push_context scope current)); if timed then EcScope.notify scope `Info "time: %f" tdelta; diff --git a/src/ecCommands.mli b/src/ecCommands.mli index 69e6c47fd..f61a313f3 100644 --- a/src/ecCommands.mli +++ b/src/ecCommands.mli @@ -24,13 +24,14 @@ type checkmode = { cm_iterate : bool; } -val initial : checkmode:checkmode -> boot:bool -> EcScope.scope +val initial : checkmode:checkmode -> boot:bool -> checkproof:bool -> EcScope.scope val initialize : restart:bool -> undo:bool -> boot:bool -> checkmode:checkmode + -> checkproof:bool -> unit val current : unit -> EcScope.scope @@ -44,7 +45,7 @@ val process_internal : -> EcScope.scope (* -------------------------------------------------------------------- *) -val process : ?timed:bool -> ?break:bool -> +val process : ?src:string -> ?timed:bool -> ?break:bool -> EcParsetree.global_action located -> float option val undo : int -> unit @@ -54,6 +55,8 @@ val mode : unit -> string val check_eco : string -> bool +val doc_comment : [`Global | `Item] * string -> unit + (* -------------------------------------------------------------------- *) val pp_current_goal : ?all:bool -> Format.formatter -> unit val pp_maybe_current_goal : Format.formatter -> unit diff --git a/src/ecDoc.ml b/src/ecDoc.ml new file mode 100644 index 000000000..01b343770 --- /dev/null +++ b/src/ecDoc.ml @@ -0,0 +1,338 @@ +(* -------------------------------------------------------------------- *) +open Tyxml.Html + +open EcScope + +(* -------------------------------------------------------------------- *) +let styles_file : string = + let (module Sites) = EcRelocate.sites in + Filename.concat Sites.doc "styles.css" + +let stdlib_doc_dp (th : string) : string = + match th with + | _ -> "" + +(* -------------------------------------------------------------------- *) +let from_stdlib (th : string) : bool = + match th with + | _ -> false + +(* -------------------------------------------------------------------- *) +let c_filename ?(ext : string option) (nms : string list) = + match ext with + | None -> String.concat "!" nms + | Some ext -> String.concat "!" nms ^ ext + +(* -------------------------------------------------------------------- *) +let thkind_str (kind : EcLoader.kind) : string = + match kind with + | `Ec -> "Theory" + | `EcA -> "Abstract Theory" + +(* -------------------------------------------------------------------- *) +let itemkind_str_pl (ik : itemkind) : string = + match ik with + | `Type -> "Types" + | `Operator -> "Operators" + | `Axiom -> "Axioms" + | `Lemma -> "Lemmas" + | `ModuleType -> "Module Types" + | `Module -> "Modules" + | `Theory -> "Theories" + +let itemkind_lookup_path (ik : itemkind) (q : EcSymbols.qsymbol) (env : EcEnv.env) = + match ik with + | `Type -> EcEnv.Ty.lookup_path q env + | `Operator -> EcEnv.Op.lookup_path q env + | `Axiom -> EcEnv.Ax.lookup_path q env + | `Lemma -> EcEnv.Ax.lookup_path q env + | `ModuleType -> EcEnv.ModTy.lookup_path q env + | `Module -> + begin + match (EcEnv.Mod.lookup_path q env).m_top with + | `Concrete (p, None) -> p + | `Concrete (_, Some _) -> failwith "Linking to sub-modules not supported." + | `Local _ -> failwith "Linking to local/declared modules not supported." + end + | `Theory -> EcEnv.Theory.lookup_path ~mode:`All q env + +(* -------------------------------------------------------------------- *) +let rec bot_env_of_qsymbol (q : EcSymbols.qsymbol) (env : EcEnv.env)= + match fst q with + | [] | ["Top"] -> env + | x :: xs -> + let p = EcEnv.Theory.lookup_path ~mode:`All ([], x) env in + let env = EcEnv.Theory.env_of_theory p env in + bot_env_of_qsymbol (xs, snd q) env + +let filename_of_path ?(ext : string option) (rth : string) (p : EcPath.path) = + let qs = EcPath.toqsymbol p in + match fst qs with + | [] -> assert false + | ["Top"] -> c_filename ?ext [rth] + | "Top" :: ts -> + let reqrt = (List.hd ts) in + if from_stdlib reqrt then + Filename.concat (stdlib_doc_dp reqrt) (c_filename ?ext ts) + else + (c_filename ?ext (rth :: ts)) + | _ -> assert false + +(* -------------------------------------------------------------------- *) +let md_pre_format ~kind (s : string) = + match kind with | _ -> pre [txt s] + +let md_href_format (rth : string) (env : EcEnv.env) (hr : Markdown.href) : Html_types.phrasing elt = + let il_format = Str.regexp "^>\\([^|]*\\)|\\([^|]+\\)$" in + if Str.string_match il_format hr.href_target 0 then + let tkind = Str.matched_group 1 hr.href_target in + let tname = Str.matched_group 2 hr.href_target in + let tqs = EcSymbols.qsymbol_of_string tname in + let env = bot_env_of_qsymbol tqs env in + let ikstr, path = + match tkind with + | "Ty" | "Type" -> itemkind_str_pl `Type, itemkind_lookup_path `Type tqs env + | "Op" | "Operator" -> itemkind_str_pl `Operator, itemkind_lookup_path `Operator tqs env + | "Ax" | "Axiom" -> itemkind_str_pl `Axiom, itemkind_lookup_path `Axiom tqs env + | "Lem" | "Lemma" -> itemkind_str_pl `Lemma, itemkind_lookup_path `Lemma tqs env + | "ModTy" | "ModuleType" -> itemkind_str_pl `ModuleType, itemkind_lookup_path `ModuleType tqs env + | "Mod" | "Module" -> itemkind_str_pl `Module, itemkind_lookup_path `Module tqs env + | "Th" | "Theory" -> itemkind_str_pl `Theory, itemkind_lookup_path `Theory tqs env + | "" -> + let rec try_lookup = function + | [] -> failwith (Printf.sprintf "No item/entity found with name `%s'." tname) + | ik :: iks -> + try itemkind_str_pl ik, itemkind_lookup_path ik tqs env + with EcEnv.LookupFailure _ -> try_lookup iks + in + let iks = [`Type; `Operator; `Axiom; `Lemma; `ModuleType; `Module; `Theory] in + try_lookup iks + | _ -> failwith (Printf.sprintf "Invalid item/entity kind `%s'." tkind) + in + let fn = filename_of_path ~ext:".html" rth path in + let il = fn ^ "#" ^ ikstr ^ snd tqs in + a ~a:[a_href (uri_of_string il)] [txt hr.href_desc] + else + a ~a:[a_href (uri_of_string hr.href_target)] [txt hr.href_desc] + +let md_img_format (_ : Markdown.img_ref) = + failwith "Image embedding not supported." + +let c_markdown (input : string) (rth : string) (env : EcEnv.env) = + let input = Markdown.parse_text input in + + MarkdownHTML.to_html + ~render_pre:md_pre_format + ~render_link:(md_href_format rth env) + ~render_img:md_img_format + input + + +(* -------------------------------------------------------------------- *) +let c_head (tstr : string) : [> Html_types.head] elt = + head (title (txt tstr)) [link ~rel:[`Stylesheet] ~href:styles_file ()] + +(* -------------------------------------------------------------------- *) +let c_sidebar (th : string) (lents : EcScope.docentity list) = + let iks = [`Type; `Operator; `Axiom; `Lemma; `ModuleType; `Module; `Theory] in + let iksin = + List.filter (fun ik -> + List.exists (fun ldoc -> + match ldoc with + | ItemDoc (_, (_, ikp, _, _)) -> ikp = ik + | SubDoc ((_, (_, ikp, _, _)), _) -> ikp = ik) lents) iks + in + nav ~a:[a_class ["sidebar"]] + [ + div ~a:[a_class["sidebar-title"]] + [ + h2 [txt "EasyCrypt Documentation"]; + span ~a:[a_class ["sidebar-title-theory"]] [txt th] + ]; + div ~a:[a_class ["sidebar-elems"]] + [ + ul ~a:[a_class ["sidebar-section-list"]] + (List.map (fun ik -> + let ikstr = itemkind_str_pl ik in + li [a ~a:[a_href (Xml.uri_of_string ("#" ^ ikstr))] [txt ikstr]]) iksin) + ] + ] + +(* -------------------------------------------------------------------- *) +let c_section_intro (rth : string) (gdoc : string list) (env : EcEnv.env) = + match gdoc with + | [] -> [] + | _ -> [ + let ids = "Introduction" in + section ~a:[a_id ids; a_title ids; a_class ["intro-section"]] [ + div ~a:[a_class ["intro-text-container"]] + (List.map (fun s -> div ~a:[a_class ["intro-par-container"]] (c_markdown s rth env)) gdoc) + ] + ] + +(* -------------------------------------------------------------------- *) +let c_section_main_itemkind_li ?(supthf : string option) (rth : string) (th : string) (lent_ik : EcScope.docentity) (env : EcEnv.env) = + match lent_ik with + | SubDoc ((doc, (_, ik, subth, _)), _) -> + begin + match ik with + | `Theory -> + let (hdoc, tdoc) = + if doc = [] then "No description available.", [] + else if List.length doc = 1 then List.hd doc, [] + else List.hd doc, List.tl doc + in + let hn = + match supthf with + | None -> c_filename ~ext:(".html") [th; subth] + | Some supf -> c_filename ~ext:(".html") [supf; th; subth] + in + li ~a:[a_id (itemkind_str_pl ik ^ subth); a_class ["item-entry"]] ([ + div ~a:[a_class ["item-name-desc-container"]] [ + div ~a:[a_class ["item-name"]] [a ~a:[a_href (Xml.uri_of_string hn)] [txt subth]]; + div ~a:[a_class ["item-basic-desc"]] (c_markdown hdoc rth env) + ] + ] @ (if tdoc <> [] + then [details ~a:[a_class ["item-details"]] (summary []) + (List.map (fun d -> div ~a:[a_class ["item-details-par"]] (c_markdown d rth env)) tdoc)] + else [])) + | _ -> assert false + end + | ItemDoc (doc, (_, ik, nm, src)) -> + let psrc = String.trim (String.concat "\n" src) in + match ik with + | `Theory -> assert false + | _ -> + let (hdoc, tdoc) = + if doc = [] then "No description available. (However, see source below.)", [] + else if List.length doc = 1 then List.hd doc, [] + else List.hd doc, List.tl doc + in + li ~a:[a_id (itemkind_str_pl ik ^ nm) ; a_class ["item-entry"]] [ + div ~a:[a_class ["item-name-desc-container"]] [ + div ~a:[a_class ["item-name"]] [txt nm]; + div ~a:[a_class ["item-basic-desc"]] (c_markdown hdoc rth env) + ]; + details ~a:[a_class ["item-details"]] (summary []) + (List.map (fun d -> div ~a:[a_class ["item-details-par"]] (c_markdown d rth env)) tdoc + @ [div ~a:[a_class ["source-container"]] + [txt "Source:"; pre ~a:[a_class ["source"]] [txt psrc]]]) + ] + +(* -------------------------------------------------------------------- *) +let c_section_main_itemkind ?(supthf : string option) (rth : string) (th : string) (lents_ik : EcScope.docentity list) (env : EcEnv.env) = + [ + ul ~a:[a_class ["item-list"]] + (List.map (fun lent_ik -> c_section_main_itemkind_li ?supthf rth th lent_ik env) lents_ik) + ] + +(* -------------------------------------------------------------------- *) +let c_section_main ?(supthf : string option) (rth : string) (th : string) (lents : EcScope.docentity list) (env : EcEnv.env) = + let iks = [`Type; `Operator; `Axiom; `Lemma; `ModuleType; `Module; `Theory] in + List.concat + (List.map (fun ik -> + let lents_ik = List.filter (fun ent -> + match ent with + | ItemDoc (_, (md, ikp, _, _)) -> md = `Specific && ikp = ik + | SubDoc ((_, (_, ikp, _, _)), _) -> ikp = ik) lents + in + match lents_ik with + | [] -> [] + | _ -> [ + let iks = itemkind_str_pl ik in + section ~a:[a_id iks; a_title iks; a_class ["item-section"]] [ + h2 ~a:[a_class ["section-heading"]] [txt iks]; + div ~a:[a_class ["item-list-container"]] (c_section_main_itemkind ?supthf rth th lents_ik env) + ] + ] + ) + iks) + +let c_body ?(supths : string option) ?(supthf : string option) (rth : string) (th : string) (tstr : string) (gdoc : string list) (ldocents : EcScope.docentity list) (env : EcEnv.env) : [> Html_types.body] elt = + let sidebar = c_sidebar th ldocents in + let page_heading = + div ~a:[a_class ["page-heading-container"]] + (h1 ~a:[a_class ["page-heading"]] [txt tstr] + :: + match supths with + | None -> [] + | Some sup -> + match supthf with + | None -> assert false + | Some supf -> + [ + h2 ~a:[a_class ["page-subheading"]] [ + txt ("Subtheory of "); + a ~a:[a_href (Xml.uri_of_string (supf ^ ".html" ^ "#" ^ itemkind_str_pl `Theory ^ th))] [txt sup] + ] + ]) + in + let sec_intro = c_section_intro rth gdoc env in + let sec_main = c_section_main ?supthf rth th ldocents env in + body (sidebar :: [main (page_heading :: sec_intro @ sec_main)]) + +(* -------------------------------------------------------------------- *) +let c_page ?(supths : string option) ?(supthf : string option) (rth : string) (th : string) (tstr : string) (gdoc : string list) (ldocents : EcScope.docentity list) (env : EcEnv.env) : [> Html_types.html] elt = + html (c_head tstr) (c_body ?supths ?supthf rth th tstr gdoc ldocents env) + +(* -------------------------------------------------------------------- *) +let emit_page (dp : string) (fn : string) (page : [> Html_types.html ] elt) = + let wp = Filename.concat dp fn ^ ".html" in + let file = open_out wp in + let fmt = Format.formatter_of_out_channel file in + pp () fmt page; + Format.fprintf fmt "@."; + close_out file + +(* -------------------------------------------------------------------- *) +let emit_pages (dp : string) (th : string) (tstr : string) (gdoc : string list) (ldocents : EcScope.docentity list) (env : EcEnv.env) = + let rec c_subpages ?supths ?supthf th docents = + match docents with + | [] -> [] + | de :: docents' -> + match de with + | ItemDoc _ -> c_subpages ?supths ?supthf th docents' + | SubDoc ((sgdoc, (smd, _, sth, _)), sldocents) -> + let ststr = (if smd = `Abstract then "Abstract " else "") ^ "Theory " ^ sth in + let stsupf = + match supthf with + | None -> th + | Some supf -> c_filename [supf; th] + in + let stf = c_filename [stsupf; sth] in + (stf, c_page ~supths:th ~supthf:stsupf th sth ststr sgdoc sldocents env) + :: c_subpages ~supths:th ~supthf:stsupf sth sldocents + @ c_subpages ?supths ?supthf th docents' + in + let spgs = c_subpages th ldocents in + List.iter (fun fnpg -> emit_page dp (fst fnpg) (snd fnpg)) spgs; + emit_page dp th (c_page th th tstr gdoc ldocents env) + +(* -------------------------------------------------------------------- *) +(* input = input name, scope contains all documentation items *) +let generate_html ?(outdirp : string option) (fname : string option) (scope : EcScope.scope) : unit = + match fname with + | Some fn -> + let kind = + try EcLoader.getkind (Filename.extension fn) + with EcLoader.BadExtension _ -> assert false + in + let dp = + match outdirp with + | None -> Filename.dirname fn + | Some outdirp -> + try + if Sys.is_directory outdirp + then outdirp + else raise (Invalid_argument (Format.sprintf "%s is not an existing directory." outdirp)) + with + | _ as ex -> Printf.eprintf "Exception: %s\n." (Printexc.to_string ex); raise ex + in + let fn = Filename.basename fn in + let th = Filename.remove_extension fn in + let tstr = thkind_str kind ^ " " ^ th in + begin + try emit_pages dp th tstr (get_gdocstrings scope) (get_ldocentities scope) (env scope) with + | _ as ex -> Printf.eprintf "Exception: %s\n." (Printexc.to_string ex); raise ex + end + | None -> () diff --git a/src/ecDoc.mli b/src/ecDoc.mli new file mode 100644 index 000000000..1e8fd31d2 --- /dev/null +++ b/src/ecDoc.mli @@ -0,0 +1,2 @@ +(* -------------------------------------------------------------------- *) +val generate_html : ?outdirp:string -> string option -> EcScope.scope -> unit \ No newline at end of file diff --git a/src/ecIo.ml b/src/ecIo.ml index e630d4b49..016545d85 100644 --- a/src/ecIo.ml +++ b/src/ecIo.ml @@ -34,16 +34,20 @@ let isuniop_fun () : unit parser_t = (* -------------------------------------------------------------------- *) type ecreader_r = { (*---*) ecr_lexbuf : Lexing.lexbuf; + (*---*) ecr_source : Buffer.t; mutable ecr_atstart : bool; + mutable ecr_trim : int; mutable ecr_tokens : EcParser.token list; } type ecreader = ecreader_r Disposable.t (* -------------------------------------------------------------------- *) -let ecreader_of_lexbuf (lexbuf : L.lexbuf) : ecreader_r = +let ecreader_of_lexbuf (buffer : Buffer.t) (lexbuf : L.lexbuf) : ecreader_r = { ecr_lexbuf = lexbuf; + ecr_source = buffer; ecr_atstart = true; + ecr_trim = 0; ecr_tokens = []; } (* -------------------------------------------------------------------- *) @@ -51,28 +55,42 @@ let lexbuf (reader : ecreader) = (Disposable.get reader).ecr_lexbuf (* -------------------------------------------------------------------- *) -let from_channel ~(name : string) (channel : in_channel) = - let lexbuf = lexbuf_from_channel name channel in +let from_channel ?(close = false) ~name channel = + let buffer = Buffer.create 0 in + + let refill (bytes : bytes) (len : int) = + let aout = input channel bytes 0 len in + Buffer.add_bytes buffer (Bytes.sub bytes 0 aout); + aout + in + + let lexbuf = Lexing.from_function refill in + + Lexing.set_filename lexbuf name; + Disposable.create - (ecreader_of_lexbuf lexbuf) + ~cb:(fun _ -> if close then close_in channel) + (ecreader_of_lexbuf buffer lexbuf) (* -------------------------------------------------------------------- *) let from_file (filename : string) = let channel = open_in filename in + try - let lexbuf = lexbuf_from_channel filename channel in - Disposable.create - ~cb:(fun _ -> close_in channel) - (ecreader_of_lexbuf lexbuf) + from_channel ~close:true ~name:filename channel with e -> (try close_in channel with _ -> ()); raise e (* -------------------------------------------------------------------- *) -let from_string (data : string) = - Disposable.create - (ecreader_of_lexbuf (Lexing.from_string data)) +let from_string data = + let lexbuf = Lexing.from_string data in + let buffer = Buffer.create (String.length data) in + + Buffer.add_string buffer data; + + Disposable.create (ecreader_of_lexbuf buffer lexbuf) (* -------------------------------------------------------------------- *) let finalize (ecreader : ecreader) = @@ -86,8 +104,20 @@ let lexer ?(checkpoint : _ I.checkpoint option) (ecreader : ecreader_r) = | EcParser.FINAL _ -> true | _ -> false in - if List.is_empty (ecreader.ecr_tokens) then - ecreader.ecr_tokens <- EcLexer.main lexbuf; + if ecreader.ecr_atstart then + ecreader.ecr_trim <- ecreader.ecr_lexbuf.Lexing.lex_curr_p.pos_cnum; + + while List.is_empty (ecreader.ecr_tokens) do + match EcLexer.main lexbuf with + | [COMMENT] -> + if ecreader.ecr_atstart then + ecreader.ecr_trim <- (Lexing.lexeme_end_p ecreader.ecr_lexbuf).pos_cnum + | [DOCCOMMENT _] as tokens -> + if ecreader.ecr_atstart then + ecreader.ecr_tokens <- tokens + | tokens -> + ecreader.ecr_tokens <- tokens + done; let token, queue = List.destruct ecreader.ecr_tokens in @@ -103,7 +133,16 @@ let lexer ?(checkpoint : _ I.checkpoint option) (ecreader : ecreader_r) = in ecreader.ecr_tokens <- prequeue @ queue; - ecreader.ecr_atstart <- (isfinal token); + + if isfinal token then + ecreader.ecr_atstart <- true + else + ecreader.ecr_atstart <- ecreader.ecr_atstart && ( + match token with + | P.DOCCOMMENT _ | P.COMMENT -> true + | _ -> false + ); + (token, Lexing.lexeme_start_p lexbuf, Lexing.lexeme_end_p lexbuf) (* -------------------------------------------------------------------- *) @@ -119,7 +158,7 @@ let drain (ecreader : ecreader) = drain () (* -------------------------------------------------------------------- *) -let parse (ecreader : ecreader) = +let parse (ecreader : ecreader) : EcParsetree.prog = let ecreader = Disposable.get ecreader in let rec parse (checkpoint : EcParsetree.prog I.checkpoint) : EcParsetree.prog = @@ -138,6 +177,17 @@ let parse (ecreader : ecreader) = in parse (EcParser.Incremental.prog ecreader.ecr_lexbuf.lex_curr_p) +(* -------------------------------------------------------------------- *) +let xparse (ecreader : ecreader) : string * EcParsetree.prog = + let ecr = Disposable.get ecreader in + + let p1 = ecr.ecr_lexbuf.Lexing.lex_curr_p.pos_cnum in + let cd = parse ecreader in + let p2 = ecr.ecr_lexbuf.Lexing.lex_curr_p.pos_cnum in + let p1 = max p1 ecr.ecr_trim in + + (Buffer.sub ecr.ecr_source p1 (p2 - p1), cd) + (* -------------------------------------------------------------------- *) let parseall (ecreader : ecreader) = let rec aux acc = @@ -145,6 +195,8 @@ let parseall (ecreader : ecreader) = | EcParsetree.P_Prog (commands, terminate) -> let acc = List.rev_append commands acc in if terminate then List.rev acc else aux acc + | EcParsetree.P_DocComment _ -> + aux acc | EcParsetree.P_Undo _ | EcParsetree.P_Exit -> assert false (* FIXME *) in diff --git a/src/ecIo.mli b/src/ecIo.mli index ce52869b4..42d28ba74 100644 --- a/src/ecIo.mli +++ b/src/ecIo.mli @@ -2,12 +2,13 @@ type ecreader (* -------------------------------------------------------------------- *) -val from_channel : name:string -> in_channel -> ecreader +val from_channel : ?close:bool -> name:string -> in_channel -> ecreader val from_file : string -> ecreader val from_string : string -> ecreader (* -------------------------------------------------------------------- *) val finalize : ecreader -> unit +val xparse : ecreader -> string * EcParsetree.prog val parse : ecreader -> EcParsetree.prog val parseall : ecreader -> EcParsetree.global list val drain : ecreader -> unit diff --git a/src/ecLexer.mll b/src/ecLexer.mll index 0e6f9a02e..c359c3754 100644 --- a/src/ecLexer.mll +++ b/src/ecLexer.mll @@ -381,7 +381,14 @@ rule main = parse with Not_found -> [PUNIOP name] } - | "(*" { comment lexbuf; main lexbuf } + | "(*" (['&' '^'] as c) { + let buffer = doccomment c (Buffer.create 0) lexbuf in + let kind = match c with '&' -> `Item | '^' -> `Global | _ -> assert false in + [DOCCOMMENT (kind, Buffer.contents buffer)] + } + + | "(*" { comment lexbuf; [COMMENT] } + | "\"" { [STRING (Buffer.contents (string (Buffer.create 0) lexbuf))] } (* string symbols *) @@ -458,6 +465,20 @@ and comment = parse | eof { unterminated_comment () } | _ { comment lexbuf } +and doccomment kind buf = parse + | ['&' '^']? "*)" { buf } + | "(*" { comment lexbuf; doccomment kind buf lexbuf } + | eof { unterminated_comment () } + | newline { + Lexing.new_line lexbuf; + Buffer.add_char buf '\n'; + doccomment kind buf lexbuf + } + | _ as c { + Buffer.add_char buf c; + doccomment kind buf lexbuf + } + and string buf = parse | "\"" { buf } | "\\n" { Buffer.add_char buf '\n'; string buf lexbuf } diff --git a/src/ecOptions.ml b/src/ecOptions.ml index b3704e1a1..499773796 100644 --- a/src/ecOptions.ml +++ b/src/ecOptions.ml @@ -9,6 +9,7 @@ type command = [ | `Config | `Runtest of run_option | `Why3Config + | `DocGen of doc_option ] and options = { @@ -40,6 +41,11 @@ and run_option = { runo_rawargs : string list; } +and doc_option = { + doco_input : string; + doco_outdirp : string option; +} + and prv_options = { prvo_maxjobs : int option; prvo_timeout : int option; @@ -359,6 +365,10 @@ let specs = { ]); ("why3config", "Configure why3", []); + + ("docgen", "Generate documentation", [ + `Spec ("outdir", `String, "Output documentation files in ") + ]); ]; xp_groups = [ @@ -516,6 +526,10 @@ let runtest_options_of_values ini values (input, scenarios) = runo_jobs = get_int "jobs" values; runo_rawargs = get_strings "raw-args" values; } +let doc_options_of_values values input = + { doco_input = input; + doco_outdirp = get_string "outdir" values; } + (* -------------------------------------------------------------------- *) let parse getini argv = let (command, values, anons) = parse specs argv in @@ -575,6 +589,18 @@ let parse getini argv = (cmd, ini, true) + | "docgen" -> + begin + match anons with + | [input] -> + let ini = getini None in + let cmd = `DocGen (doc_options_of_values values input) in + (cmd, ini, true) + + | _ -> + raise (Arg.Bad "this command takes a single input file as argument") + end + | _ -> assert false in { diff --git a/src/ecOptions.mli b/src/ecOptions.mli index b779aa44e..5ba1d0f63 100644 --- a/src/ecOptions.mli +++ b/src/ecOptions.mli @@ -5,6 +5,7 @@ type command = [ | `Config | `Runtest of run_option | `Why3Config + | `DocGen of doc_option ] and options = { @@ -36,6 +37,11 @@ and run_option = { runo_rawargs : string list; } +and doc_option = { + doco_input : string; + doco_outdirp : string option; +} + and prv_options = { prvo_maxjobs : int option; prvo_timeout : int option; diff --git a/src/ecParser.mly b/src/ecParser.mly index 90ff33bf6..34bc48748 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -412,6 +412,7 @@ %token COLON %token COLONTILD %token COMMA +%token COMMENT %token CONGR %token CONSEQ %token CONST @@ -605,7 +606,8 @@ %token ZETA %token NOP LOP1 ROP1 LOP2 ROP2 LOP3 ROP3 LOP4 ROP4 NUMOP %token LTCOLON DASHLT GT LT GE LE LTSTARGT LTLTSTARGT LTSTARGTGT -%token < Lexing.position> FINAL +%token FINAL +%token DOCCOMMENT %nonassoc prec_below_comma %nonassoc COMMA ELSE @@ -3900,6 +3902,9 @@ prog_r: | EXIT FINAL { P_Exit } +| d=DOCCOMMENT + { P_DocComment d } + | error { parse_error (EcLocation.make $startpos $endpos) None } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 81b4ad18f..8068950fa 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -382,6 +382,12 @@ let rec pf_ident ?(raw = false) f = | PFtuple [f] when not raw -> pf_ident ~raw f | _ -> None + let rec pcmhd_ident (pcmhd : pmodule_header) : psymbol = + match pcmhd with + | Pmh_ident nm -> nm + | Pmh_params x -> pcmhd_ident (fst (unloc x)) + | Pmh_cast (pmh, _) -> pcmhd_ident pmh + (* -------------------------------------------------------------------- *) type psubtype = { pst_name : psymbol; @@ -1312,5 +1318,8 @@ type prog_r = | P_Prog of global list * bool | P_Exit | P_Undo of int + | P_DocComment of (dockind * string) + +and dockind = [`Global | `Item] type prog = prog_r located diff --git a/src/ecRelocate.ml b/src/ecRelocate.ml index f07cb429a..0505a9b36 100644 --- a/src/ecRelocate.ml +++ b/src/ecRelocate.ml @@ -23,6 +23,7 @@ let local (name : string list) : string = module type Sites = sig val commands : string val theories : string list + val doc : string val config : string end @@ -30,6 +31,7 @@ end module LocalSites() : Sites = struct let commands = local ["scripts"; "testing"] let theories = [local ["theories"]] + let doc = local ["assets"; "styles"] let config = local ["etc"] end @@ -42,7 +44,11 @@ module DuneSites() : Sites = struct let theories = EcDuneSites.Sites.theories - let config = + let doc = + Option.value ~default:"." + (EcUtils.List.Exceptionless.hd EcDuneSites.Sites.doc) + + let config = Option.value ~default:"etc" (EcUtils.List.Exceptionless.hd EcDuneSites.Sites.config) end diff --git a/src/ecRelocate.mli b/src/ecRelocate.mli index 8600315c0..59e80d735 100644 --- a/src/ecRelocate.mli +++ b/src/ecRelocate.mli @@ -5,6 +5,7 @@ val sourceroot : string option module type Sites = sig val commands : string val theories : string list + val doc : string val config : string end diff --git a/src/ecScope.ml b/src/ecScope.ml index 21e1403d5..ac8b01178 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -337,8 +337,105 @@ type scope = { sc_clears : path list; sc_pr_uc : proof_uc option; sc_options : GenOptions.options; + sc_globdoc : string list; + sc_locdoc : docstate; } +and docstate = { + docentities : docentity list; + subdocentbl : docentity list; + docstringbl : string list; + srcstringbl : string list; + currentname : string option; + currentkind : itemkind option; + currentmode : mode option; + currentproc : bool; +} + +and docentity = + | ItemDoc of string list * docitem + | SubDoc of (string list * docitem) * docentity list + +and docitem = + mode * itemkind * string * string list (* dec/reg, kind, name, src *) + +and itemkind = [`Type | `Operator | `Axiom | `Lemma | `ModuleType | `Module | `Theory] + +and mode = [`Abstract | `Specific] + +(* -------------------------------------------------------------------- *) +let get_gdocstrings (sc : scope) : string list = + sc.sc_globdoc + +let get_ldocentities (sc : scope) : docentity list = + sc.sc_locdoc.docentities + +module DocState = struct + let empty : docstate = + { docentities = []; + subdocentbl = []; + docstringbl = []; + srcstringbl = []; + currentname = None; + currentkind = None; + currentmode = None; + currentproc = false; } + + let start_process (state : docstate) (name : string) (kind : itemkind) (md : mode): docstate = + { state with + currentname = Some name; + currentkind = Some kind; + currentmode = Some md; + currentproc = true } + + let prevent_process (state : docstate) : docstate = + { state with + currentname = None; + currentkind = None; + currentmode = None; + currentproc = false } + + let reinitialize_process (state : docstate) : docstate = + { state with + docstringbl = []; + srcstringbl = []; + currentname = None; + currentkind = None; + currentmode = None; + currentproc = false } + + let push_docbl (state : docstate) (docc : string) : docstate = + { state with docstringbl = state.docstringbl @ [docc] } + + let push_srcbl (state : docstate) (srcs : string) : docstate = + { state with srcstringbl = state.srcstringbl @ [srcs] } + + let add_entity (state : docstate) (docent : docentity) : docstate = + { state with docentities = state.docentities @ [docent] } + + let add_item (state : docstate) : docstate = + let state = + if state.currentproc + then + add_entity state (ItemDoc (state.docstringbl, (oget state.currentmode, oget state.currentkind, oget state.currentname, state.srcstringbl))) + else + state + in + reinitialize_process state + + let add_sub (state : docstate) (substate : docstate) : docstate = + let state = + if state.currentproc + then + add_entity state (SubDoc ((state.docstringbl, (oget state.currentmode, oget state.currentkind, oget state.currentname, state.srcstringbl)), + (substate.docentities))) + else + state + in + reinitialize_process state + + end + (* -------------------------------------------------------------------- *) let empty (gstate : EcGState.gstate) = let env = EcEnv.initial gstate in @@ -350,7 +447,9 @@ let empty (gstate : EcGState.gstate) = sc_required = []; sc_clears = []; sc_pr_uc = None; - sc_options = GenOptions.freeze (); } + sc_options = GenOptions.freeze (); + sc_globdoc = []; + sc_locdoc = DocState.empty; } (* -------------------------------------------------------------------- *) let env (scope : scope) = @@ -470,7 +569,8 @@ let for_loading (scope : scope) = sc_clears = []; sc_pr_uc = None; sc_options = GenOptions.for_loading scope.sc_options; - } + sc_globdoc = []; + sc_locdoc = DocState.empty; } (* -------------------------------------------------------------------- *) let subscope (scope : scope) (mode : EcTheory.thmode) (name : symbol) lc = @@ -484,7 +584,10 @@ let subscope (scope : scope) (mode : EcTheory.thmode) (name : symbol) lc = sc_required = scope.sc_required; sc_clears = []; sc_pr_uc = None; - sc_options = GenOptions.for_subscope scope.sc_options; } + sc_options = GenOptions.for_subscope scope.sc_options; + sc_globdoc = []; + sc_locdoc = DocState.empty; + } (* -------------------------------------------------------------------- *) module Prover = struct @@ -694,7 +797,7 @@ module Tactics = struct let pi scope pi = Prover.do_prover_info scope pi - let proof (scope : scope) = + let proof ?(src : string option) (scope : scope) = check_state `InActiveProof "proof script" scope; match (oget scope.sc_pr_uc).puc_active with @@ -705,10 +808,14 @@ module Tactics = struct hierror "[proof] can only be used at beginning of a proof script"; { pac with puc_started = true } in - { scope with sc_pr_uc = - Some { (oget scope.sc_pr_uc) with puc_active = Some (pac, pct); } } + { scope with + sc_pr_uc = Some { (oget scope.sc_pr_uc) with puc_active = Some (pac, pct) }; + sc_locdoc = + match src with + | Some src -> DocState.push_srcbl scope.sc_locdoc src + | None -> scope.sc_locdoc; } - let process_r ?reloc mark (mode : proofmode) (scope : scope) (tac : ptactic list) = + let process_r ?(src : string option) ?reloc mark (mode : proofmode) (scope : scope) (tac : ptactic list) = check_state `InProof "proof script" scope; let scope = @@ -720,6 +827,13 @@ module Tactics = struct else scope in + let scope = { scope with + sc_locdoc = + match src with + | Some src -> DocState.push_srcbl scope.sc_locdoc src + | None -> scope.sc_locdoc; } + in + let puc = oget (scope.sc_pr_uc) in let pac, pct = oget (puc).puc_active in @@ -760,7 +874,7 @@ module Tactics = struct let pac = { pac with puc_jdg = PSCheck juc } in let puc = { puc with puc_active = Some (pac, pct); } in - let scope = { scope with sc_pr_uc = Some puc } in + let scope = { scope with sc_pr_uc = Some puc; } in Some (penv, hds), scope let process1_r mark mode scope t = @@ -770,8 +884,8 @@ module Tactics = struct let ts = List.map (fun t -> { pt_core = t; pt_intros = []; }) ts in snd (process_r mark mode scope ts) - let process scope mode tac = - process_r true mode scope tac + let process ?(src : string option) scope mode tac = + process_r ?src true mode scope tac end (* -------------------------------------------------------------------- *) @@ -825,7 +939,9 @@ module Ax = struct let bind ?(import = true) (scope : scope) ((x, ax) : _ * axiom) = assert (scope.sc_pr_uc = None); let item = EcTheory.mkitem ~import (EcTheory.Th_axiom (x, ax)) in - { scope with sc_env = EcSection.add_item item scope.sc_env } + { scope with sc_env = + EcSection.add_item item scope.sc_env; + sc_locdoc = DocState.add_item scope.sc_locdoc; } (* ------------------------------------------------------------------ *) let start_lemma scope (cont, axflags) check ?name (axd, ctxt) = @@ -1017,22 +1133,69 @@ module Ax = struct save_r scope (* ------------------------------------------------------------------ *) - let save scope = + let save ?(src : string option) scope = check_state `InProof "save" scope; + + let scope = + { scope with + sc_locdoc = + match src with + | Some src -> DocState.push_srcbl scope.sc_locdoc src + | None -> scope.sc_locdoc; } + in save_r ~mode:`Save scope (* ------------------------------------------------------------------ *) - let admit scope = + let admit ?(src : string option) scope = check_state `InProof "admitted" scope; + + let scope = + { scope with + sc_locdoc = + match src with + | Some src -> DocState.push_srcbl scope.sc_locdoc src + | None -> scope.sc_locdoc; } + in + save_r ~mode:`Admit scope (* ------------------------------------------------------------------ *) - let abort scope = + let abort ?(src : string option) scope = check_state `InProof "abort" scope; + + let scope = + { scope with + sc_locdoc = + match src with + | Some src -> DocState.push_srcbl scope.sc_locdoc src + | None -> scope.sc_locdoc; } + in + snd (save_r ~mode:`Abort scope) (* ------------------------------------------------------------------ *) - let add (scope : scope) (mode : proofmode) (ax : paxiom located) = + let add ?(src : string option) (scope : scope) (mode : proofmode) (ax : paxiom located) = + let uax = unloc ax in + let kind = + match uax.pa_kind with + | PLemma _ -> `Lemma + | _ -> `Axiom + in + let scope = + { scope with + sc_locdoc = + match uax.pa_locality with + | `Local -> DocState.prevent_process scope.sc_locdoc + | `Global -> DocState.start_process scope.sc_locdoc (unloc uax.pa_name) kind `Specific + | `Declare -> DocState.start_process scope.sc_locdoc (unloc uax.pa_name) kind `Abstract} + in + let scope = + { scope with + sc_locdoc = + match src with + | Some src -> DocState.push_srcbl scope.sc_locdoc src + | None -> scope.sc_locdoc; } + in add_r scope mode ax (* ------------------------------------------------------------------ *) @@ -1088,10 +1251,30 @@ module Op = struct let bind ?(import = true) (scope : scope) ((x, op) : _ * operator) = assert (scope.sc_pr_uc = None); let item = EcTheory.mkitem ~import (EcTheory.Th_operator (x, op)) in - { scope with sc_env = EcSection.add_item item scope.sc_env; } + { scope with sc_env = + EcSection.add_item item scope.sc_env; + sc_locdoc = DocState.add_item scope.sc_locdoc; } - let add (scope : scope) (op : poperator located) = + let add ?(src : string option) (scope : scope) (op : poperator located) = assert (scope.sc_pr_uc = None); + + let uop = unloc op in + let scope = + { scope with + sc_locdoc = + match uop.po_locality with + | `Local -> DocState.prevent_process scope.sc_locdoc + | `Global -> DocState.start_process scope.sc_locdoc (unloc uop.po_name) `Operator `Specific + | `Declare -> DocState.start_process scope.sc_locdoc (unloc uop.po_name) `Operator `Abstract } + in + let scope = + { scope with + sc_locdoc = + match src with + | Some src -> DocState.push_srcbl scope.sc_locdoc src + | None -> scope.sc_locdoc; } + in + let op = op.pl_desc and loc = op.pl_loc in let eenv = env scope in let ue = TT.transtyvars eenv (loc, op.po_tyvars) in @@ -1317,9 +1500,26 @@ module Op = struct tyop, List.rev !axs, scope - let add_opsem (scope : scope) (op : pprocop located) = + let add_opsem ?(src : string option) (scope : scope) (op : pprocop located) = let module Sem = EcProcSem in + let uop = unloc op in + let scope = + { scope with + sc_locdoc = + match uop.ppo_locality with + | `Local -> DocState.prevent_process scope.sc_locdoc + | `Global -> DocState.start_process scope.sc_locdoc (unloc uop.ppo_name) `Operator `Specific + | `Declare -> DocState.start_process scope.sc_locdoc (unloc uop.ppo_name) `Operator `Abstract } + in + let scope = + { scope with + sc_locdoc = + match src with + | Some src -> DocState.push_srcbl scope.sc_locdoc src + | None -> scope.sc_locdoc; } + in + let op = unloc op in let f = EcTyping.trans_gamepath (env scope) op.ppo_target in let sig_, body = @@ -1452,9 +1652,26 @@ end module Pred = struct module TT = EcTyping - let add (scope : scope) (pr : ppredicate located) = + let add ?(src : string option) (scope : scope) (pr : ppredicate located) = assert (scope.sc_pr_uc = None); + let upr = unloc pr in + let scope = + { scope with + sc_locdoc = + match upr.pp_locality with + | `Local -> DocState.prevent_process scope.sc_locdoc + | `Global -> DocState.start_process scope.sc_locdoc (unloc upr.pp_name) `Operator `Specific + | `Declare -> DocState.start_process scope.sc_locdoc (unloc upr.pp_name) `Operator `Abstract } + in + let scope = + { scope with + sc_locdoc = + match src with + | Some src -> DocState.push_srcbl scope.sc_locdoc src + | None -> scope.sc_locdoc; } + in + let typr = EcHiPredicates.trans_preddecl (env scope) pr in let scope = Op.bind scope (unloc (unloc pr).pp_name, typr) in typr, scope @@ -1479,14 +1696,34 @@ module Mod = struct let bind ?(import = true) (scope : scope) (m : top_module_expr) = assert (scope.sc_pr_uc = None); let item = EcTheory.mkitem ~import (EcTheory.Th_module m) in - { scope with sc_env = EcSection.add_item item scope.sc_env } + { scope with + sc_env = EcSection.add_item item scope.sc_env; + sc_locdoc = DocState.add_item scope.sc_locdoc; } - let add_concrete (scope : scope) lc (ptm : pmodule_def) = + let add_concrete ?(src : string option) (scope : scope) lc (ptm : pmodule_def) = assert (scope.sc_pr_uc = None); if lc = `Declare then hierror "cannot use [declare] for concrete modules"; + let nm = unloc (EcParsetree.pcmhd_ident ptm.ptm_header) in + + let scope = + { scope with + sc_locdoc = + match lc with + | `Local -> DocState.prevent_process scope.sc_locdoc + | `Global -> DocState.start_process scope.sc_locdoc nm `Module `Specific + | `Declare -> DocState.start_process scope.sc_locdoc nm `Module `Abstract } + in + let scope = + { scope with + sc_locdoc = + match src with + | Some src -> DocState.push_srcbl scope.sc_locdoc src + | None -> scope.sc_locdoc; } + in + let m = TT.transmod (env scope) ~attop:true ptm in let ur = EcModules.get_uninit_read_of_module (path scope) m in @@ -1516,10 +1753,10 @@ module Mod = struct { scope with sc_env = EcSection.add_decl_mod name tysig scope.sc_env } - let add (scope : scope) (m : pmodule_def_or_decl) = + let add ?(src : string option) (scope : scope) (m : pmodule_def_or_decl) = match m with | { ptm_locality = lc; ptm_def = `Concrete def } -> - add_concrete scope lc def + add_concrete ?src scope lc def | { ptm_locality = lc; ptm_def = `Abstract decl } -> if lc <> `Declare then @@ -1540,10 +1777,27 @@ module ModType = struct = assert (scope.sc_pr_uc = None); let item = EcTheory.mkitem ~import (EcTheory.Th_modtype (x, tysig)) in - { scope with sc_env = EcSection.add_item item scope.sc_env } + { scope with + sc_env = EcSection.add_item item scope.sc_env; + sc_locdoc = DocState.add_item scope.sc_locdoc; } - let add (scope : scope) (intf : pinterface) = + let add ?(src : string option) (scope : scope) (intf : pinterface) = assert (scope.sc_pr_uc = None); + + let scope = + { scope with + sc_locdoc = + match intf.pi_locality with + | `Local -> DocState.prevent_process scope.sc_locdoc + | `Global -> DocState.start_process scope.sc_locdoc (unloc intf.pi_name) `ModuleType `Specific } + in + let scope = + { scope with + sc_locdoc = + match src with + | Some src -> DocState.push_srcbl scope.sc_locdoc src + | None -> scope.sc_locdoc; } + in let tysig = EcTyping.transmodsig (env scope) intf in bind scope (unloc intf.pi_name, tysig) end @@ -1580,8 +1834,23 @@ module Theory = struct in { scope with sc_required = List.map for1 scope.sc_required } (* ------------------------------------------------------------------ *) - let enter (scope : scope) (mode : thmode) (name : symbol) = + let enter ?(src : string option) (scope : scope) (mode : thmode) (name : symbol) = assert (scope.sc_pr_uc = None); + let sc_locdoc = scope.sc_locdoc in + let sc_locdoc = + match src with + | None -> DocState.prevent_process scope.sc_locdoc + | Some src -> + let sc_locdoc = + DocState.start_process sc_locdoc name `Theory + (match mode with `Concrete -> `Specific | `Abstract -> `Abstract) + in + DocState.push_srcbl sc_locdoc src + in + let + scope = { scope with sc_locdoc } + in + subscope scope mode name (* ------------------------------------------------------------------ *) @@ -1632,7 +1901,10 @@ module Theory = struct let _, cth, _ = EcSection.exit_theory ?pempty ~clears scope.sc_env in let loaded = scope.sc_loaded in let required = scope.sc_required in - let sup = { sup with sc_loaded = loaded; } in + let sup = { + sup with + sc_loaded = loaded; + sc_locdoc = DocState.add_sub sup.sc_locdoc scope.sc_locdoc} in ((cth, required), scope.sc_name, sup) (* ------------------------------------------------------------------ *) @@ -1896,7 +2168,7 @@ module Cloning = struct | `Include -> scope) scope in - + if is_none thcl.pthc_local && oth.cth_loca = `Local then notify scope `Info "Theory `%s` has inherited `local` visibility. \ @@ -1928,10 +2200,29 @@ module Ty = struct let bind ?(import = true) (scope : scope) ((x, tydecl) : (_ * tydecl)) = assert (scope.sc_pr_uc = None); let item = EcTheory.mkitem ~import (EcTheory.Th_type (x, tydecl)) in - { scope with sc_env = EcSection.add_item item scope.sc_env } + { scope with + sc_env = EcSection.add_item item scope.sc_env; + sc_locdoc = DocState.add_item scope.sc_locdoc; } (* ------------------------------------------------------------------ *) - let add scope (tyd : ptydecl located) = + let add ?(src : string option) scope (tyd : ptydecl located) = + let utyd = unloc tyd in + let scope = + { scope with + sc_locdoc = + match utyd.pty_locality with + | `Local -> DocState.prevent_process scope.sc_locdoc + | `Global -> DocState.start_process scope.sc_locdoc (unloc utyd.pty_name) `Type `Specific + | `Declare -> DocState.start_process scope.sc_locdoc (unloc utyd.pty_name) `Type `Abstract } + in + let scope = + { scope with + sc_locdoc = + match src with + | Some src -> DocState.push_srcbl scope.sc_locdoc src + | None -> scope.sc_locdoc; } + in + let loc = loc tyd in let { pty_name = name; pty_tyvars = args; @@ -1985,14 +2276,14 @@ module Ty = struct let carrier = let ue = EcUnify.UniEnv.create None in transty tp_tydecl env ue subtype.pst_carrier in - + let pred = let x = EcIdent.create (fst subtype.pst_pred).pl_desc in let env = EcEnv.Var.bind_local x carrier env in let ue = EcUnify.UniEnv.create None in let pred = EcTyping.trans_prop env ue (snd subtype.pst_pred) in if not (EcUnify.UniEnv.closed ue) then - hierror ~loc:(snd subtype.pst_pred).pl_loc + hierror ~loc:(snd subtype.pst_pred).pl_loc "the predicate contains free type variables"; let uidmap = EcUnify.UniEnv.close ue in let fs = Tuni.subst uidmap in @@ -2014,12 +2305,12 @@ module Ty = struct ev_bynames = Msym.empty; ev_global = [ (None, Some [`Include, "prove"]) ] } } in - + let cname = Option.map unloc subtype.pst_cname in let npath = ofold ((^~) EcPath.pqname) (EcEnv.root env) cname in let cpath = EcPath.fromqsymbol ([EcCoreLib.i_top], "Subtype") in let theory = EcEnv.Theory.by_path ~mode:`Abstract cpath env in - + let renames = match subtype.pst_rename with | None -> [] @@ -2042,7 +2333,7 @@ module Ty = struct ) in let proofs = Cloning.replay_proofs scope `Check proofs in - + Ax.add_defer scope proofs (* ------------------------------------------------------------------ *) @@ -2507,3 +2798,14 @@ end notify scope `Info "%s" (Buffer.contents buffer) end + +(* -------------------------------------------------------------------- *) +module DocComment = struct + let add (scope : scope) ((kind, docc) : [`Global | `Item] * string) : scope = + match kind with + | `Global -> + { scope with sc_globdoc = scope.sc_globdoc @ [docc] } + + | `Item -> + { scope with sc_locdoc = DocState.push_docbl scope.sc_locdoc docc } +end diff --git a/src/ecScope.mli b/src/ecScope.mli index bc3c2812d..d64007674 100644 --- a/src/ecScope.mli +++ b/src/ecScope.mli @@ -54,9 +54,25 @@ and pucflags = { puc_local : bool; } +type docentity = + | ItemDoc of string list * docitem + | SubDoc of (string list * docitem) * docentity list + +and docitem = + mode * itemkind * string * string list (* dec/reg, kind, name, src *) + +and itemkind = [`Type | `Operator | `Axiom | `Lemma | `ModuleType | `Module | `Theory] + +and mode = [`Abstract | `Specific] + (* -------------------------------------------------------------------- *) val notify : scope -> EcGState.loglevel -> ('a, Format.formatter, unit, unit) format4 -> 'a +(* -------------------------------------------------------------------- *) +val get_gdocstrings : scope -> string list +val get_ldocentities : scope -> docentity list + + (* -------------------------------------------------------------------- *) val empty : EcGState.gstate -> scope val gstate : scope -> EcGState.gstate @@ -93,30 +109,30 @@ end (* -------------------------------------------------------------------- *) module Op : sig - val add : scope -> poperator located -> EcDecl.operator * string list * scope + val add : ?src:string -> scope -> poperator located -> EcDecl.operator * string list * scope - val add_opsem : scope -> pprocop located -> scope + val add_opsem : ?src:string -> scope -> pprocop located -> scope end (* -------------------------------------------------------------------- *) module Pred : sig - val add : scope -> ppredicate located -> EcDecl.operator * scope + val add : ?src:string -> scope -> ppredicate located -> EcDecl.operator * scope end (* -------------------------------------------------------------------- *) module Ax : sig type proofmode = [`WeakCheck | `Check | `Report] - val add : scope -> proofmode -> paxiom located -> symbol option * scope - val save : scope -> string option * scope - val admit : scope -> string option * scope - val abort : scope -> scope + val add : ?src:string -> scope -> proofmode -> paxiom located -> symbol option * scope + val save : ?src:string -> scope -> string option * scope + val admit : ?src:string -> scope -> string option * scope + val abort : ?src:string -> scope -> scope val realize : scope -> proofmode -> prealize located -> symbol option * scope end (* -------------------------------------------------------------------- *) module Ty : sig - val add : scope -> ptydecl located -> scope + val add : ?src:string -> scope -> ptydecl located -> scope val add_subtype : scope -> psubtype located -> scope val add_class : scope -> ptypeclass located -> scope @@ -125,14 +141,14 @@ end (* -------------------------------------------------------------------- *) module Mod : sig - val add : scope -> pmodule_def_or_decl -> scope + val add : ?src:string ->scope -> pmodule_def_or_decl -> scope val declare : scope -> pmodule_decl -> scope val import : scope -> pmsymbol located -> scope end (* -------------------------------------------------------------------- *) module ModType : sig - val add : scope -> pinterface -> scope + val add : ?src:string -> scope -> pinterface -> scope end (* -------------------------------------------------------------------- *) @@ -147,7 +163,7 @@ module Theory : sig (* [enter scope mode name] start a theory in scope [scope] with * name [name] and mode (abstract/concrete) [mode]. *) - val enter : scope -> thmode -> symbol -> EcTypes.is_local -> scope + val enter : ?src:string -> scope -> thmode -> symbol -> EcTypes.is_local -> scope (* [exit scope] close and finalize the top-most theory and returns * its name. Raises [TopScope] if [scope] has not super scope. *) @@ -195,8 +211,8 @@ module Tactics : sig type prinfos = proofenv * (handle * handle list) type proofmode = Ax.proofmode - val process : scope -> proofmode -> ptactic list -> prinfos option * scope - val proof : scope -> scope + val process : ?src:string -> scope -> proofmode -> ptactic list -> prinfos option * scope + val proof : ?src:string -> scope -> scope end (* -------------------------------------------------------------------- *) @@ -260,3 +276,8 @@ module Search : sig val search : scope -> pformula list -> unit val locate : scope -> pqsymbol -> unit end + +(* -------------------------------------------------------------------- *) +module DocComment : sig + val add : scope -> [`Global | `Item] * string -> scope +end diff --git a/src/ecSection.ml b/src/ecSection.ml index d04386066..f11ad35e3 100644 --- a/src/ecSection.ml +++ b/src/ecSection.ml @@ -1442,7 +1442,7 @@ let genenv_of_scenv (scenv : scenv) : to_gen = ; tg_params = [] ; tg_binds = [] ; tg_subst = EcSubst.empty - ; tg_clear = empty_locals } + ; tg_clear = empty_locals } let generalize_lc_items scenv = let togen = @@ -1451,7 +1451,7 @@ let generalize_lc_items scenv = (EcEnv.root scenv.sc_env) (List.rev scenv.sc_items) in togen.tg_env - + (* -----------------------------------------------------------*) let import p scenv = { scenv with sc_env = EcEnv.Theory.import p scenv.sc_env } diff --git a/src/ecSymbols.ml b/src/ecSymbols.ml index e1e37313f..9b2ee1cc6 100644 --- a/src/ecSymbols.ml +++ b/src/ecSymbols.ml @@ -87,3 +87,11 @@ let rec string_of_msymbol (mx : msymbol) = let pp_msymbol fmt x = Format.fprintf fmt "%s" (string_of_msymbol x) + +(* -------------------------------------------------------------------- *) +let qsymbol_of_string (s : string) : qsymbol = + let sspl = String.split_on_char '.' s in + match List.rev sspl with + | [] -> raise (invalid_arg "EcSymbols.qsymbol_of_string") + | [x] -> ([], x) + | x :: xs -> (List.rev xs, x) diff --git a/src/ecSymbols.mli b/src/ecSymbols.mli index a761df52f..b42cb35e9 100644 --- a/src/ecSymbols.mli +++ b/src/ecSymbols.mli @@ -32,3 +32,5 @@ val pp_qsymbol : Format.formatter -> qsymbol -> unit val pp_msymbol : Format.formatter -> msymbol -> unit val string_of_qsymbol : qsymbol -> string + +val qsymbol_of_string : string -> qsymbol \ No newline at end of file diff --git a/src/ecTerminal.ml b/src/ecTerminal.ml index 7ed63fd89..94f7c048e 100644 --- a/src/ecTerminal.ml +++ b/src/ecTerminal.ml @@ -15,7 +15,7 @@ type loglevel = EcGState.loglevel class type terminal = object method interactive : bool - method next : EcParsetree.prog + method next : string * EcParsetree.prog method notice : immediate:bool -> loglevel -> string -> unit method finish : status -> unit method finalize : unit @@ -70,7 +70,7 @@ object(self) end; Format.printf "[%d|%s]>\n%!" (EcCommands.uuid ()) (EcCommands.mode ()); - EcIo.parse iparser + EcIo.xparse iparser method notice ~(immediate:bool) (lvl : loglevel) (msg : string) = match immediate with @@ -116,7 +116,7 @@ object method next = Format.printf "[%d|%s]>\n%!" (EcCommands.uuid ()) (EcCommands.mode ()); EcIo.drain iparser; - EcIo.parse iparser + EcIo.xparse iparser method notice ~(immediate:bool) (_ : loglevel) (msg : string) = ignore immediate; @@ -271,8 +271,8 @@ class from_channel method interactive = false method next = - let aout = EcIo.parse iparser in - loc <- aout.LC.pl_loc; + let aout = EcIo.xparse iparser in + loc <- (snd aout).LC.pl_loc; self#_update_progress; aout method notice ~immediate lvl msg = diff --git a/src/ecTerminal.mli b/src/ecTerminal.mli index f18cee1ac..0a96a56d2 100644 --- a/src/ecTerminal.mli +++ b/src/ecTerminal.mli @@ -10,7 +10,7 @@ type loglevel = EcGState.loglevel (* -------------------------------------------------------------------- *) val interactive : terminal -> bool -val next : terminal -> EcParsetree.prog +val next : terminal -> string * EcParsetree.prog val notice : immediate:bool -> loglevel -> string -> terminal -> unit val finish : status -> terminal -> unit val finalize : terminal -> unit