WIP

src/ec.ml

@@ -445,6 +445,9 @@ let main () =
                    end)
                 commands
 
+          | EP.P_DocComment doc ->
+             EcCommands.doc_comment doc
+
           | EP.P_Undo i ->
               EcCommands.undo i
           | EP.P_Exit ->

src/ecCommands.ml

@@ -805,6 +805,14 @@ 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)

src/ecCommands.mli

@@ -42,6 +42,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

src/ecIo.ml

@@ -131,6 +131,8 @@ let parseall (ecreader : 'a ecreader_g) =
     | 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

src/ecLexer.mll

@@ -375,7 +375,14 @@ rule main = parse
       with Not_found -> [PUNIOP name]
   }
 
+  | "(*" (['*' '^'] 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; main lexbuf }
+
   | "\"" { [STRING (Buffer.contents (string (Buffer.create 0) lexbuf))] }
 
   (* string symbols *)
@@ -453,6 +460,30 @@ and comment = parse
   | eof         { unterminated_comment () }
   | _           { comment lexbuf }
 
+and doccomment kind buf = parse
+  | (['*' '^'] as c) "*)" {
+      if kind <> c then begin
+        lex_error
+          lexbuf
+          (Printf.sprintf "(*%c comment closed with %c*)" kind c);
+      end; buf
+  }
+
+  | 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 }

src/ecParser.mly

@@ -606,7 +606,8 @@
 %token ZETA
 %token <string> 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 <Lexing.position> FINAL
+%token <EcParsetree.dockind * string> DOCCOMMENT
 
 %nonassoc prec_below_comma
 %nonassoc COMMA ELSE
@@ -4012,6 +4013,9 @@ prog_r:
 | EXIT FINAL
    { P_Exit }
 
+| d=DOCCOMMENT
+   { P_DocComment d }
+
 | error
    { parse_error (EcLocation.make $startpos $endpos) None }
 

src/ecParsetree.ml

@@ -1289,5 +1289,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

src/ecScope.ml

@@ -335,8 +335,38 @@ type scope = {
   sc_clears   : path list;
   sc_pr_uc    : proof_uc option;
   sc_options  : GenOptions.options;
+  sc_doc      : docstate;
 }
 
+and docstate = {
+  docitems : docstate1 list;
+  docfw    : string list;
+}
+
+and docstate1 =
+  | GlobalDoc of string
+  | ItemDoc   of string list * docitem
+
+and docitem =
+  string                        (* raw definition *)
+
+(* -------------------------------------------------------------------- *)
+module DocState = struct
+  let empty : docstate =
+    { docitems = []; docfw = []; }
+
+  let push_global (state : docstate) (doc : string) : docstate =
+    { state with docitems = GlobalDoc doc :: state.docitems }
+
+  let push_temporary (state : docstate) (doc : string) : docstate =
+    { state with docfw = doc :: state.docfw }
+
+  let promote_temporary (state : docstate) (item : string) : docstate =
+    { state with
+        docitems = ItemDoc (state.docfw, item) :: state.docitems;
+        docfw    = []; }
+end
+
 (* -------------------------------------------------------------------- *)
 let empty (gstate : EcGState.gstate) =
   let env = EcEnv.initial gstate in
@@ -348,7 +378,8 @@ let empty (gstate : EcGState.gstate) =
     sc_required   = [];
     sc_clears     = [];
     sc_pr_uc      = None;
-    sc_options    = GenOptions.freeze (); }
+    sc_options    = GenOptions.freeze ();
+    sc_doc        = DocState.empty; }
 
 (* -------------------------------------------------------------------- *)
 let env (scope : scope) =
@@ -468,7 +499,7 @@ let for_loading (scope : scope) =
     sc_clears     = [];
     sc_pr_uc      = None;
     sc_options    = GenOptions.for_loading scope.sc_options;
-  }
+    sc_doc        = DocState.empty; }
 
 (* -------------------------------------------------------------------- *)
 let subscope (scope : scope) (mode : EcTheory.thmode) (name : symbol) lc =
@@ -482,7 +513,8 @@ 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_doc        = DocState.empty; }
 
 (* -------------------------------------------------------------------- *)
 module Prover = struct
@@ -1132,7 +1164,9 @@ module Op = struct
   let bind ?(import = EcTheory.import0) (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_doc = DocState.promote_temporary scope.sc_doc "operator"; }
 
   let add (scope : scope) (op : poperator located) =
     assert (scope.sc_pr_uc = None);
@@ -2409,3 +2443,14 @@ module Search = struct
 
     notify scope `Info "%s" (Buffer.contents buffer)
 end
+
+(* -------------------------------------------------------------------- *)
+module DocComment = struct
+  let add (scope : scope) ((kind, doc) : [`Global | `Item] * string) : scope =
+    match kind with
+    | `Global ->
+       { scope with sc_doc = DocState.push_global scope.sc_doc doc }
+
+    | `Item ->
+       { scope with sc_doc = DocState.push_temporary scope.sc_doc doc }
+end

src/ecScope.mli

@@ -238,3 +238,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