diff --git a/src/ecCommands.ml b/src/ecCommands.ml index c3b06c5e85..be936bf078 100644 --- a/src/ecCommands.ml +++ b/src/ecCommands.ml @@ -319,7 +319,7 @@ and process_tycinst (scope : EcScope.scope) (tci : ptycinstance located) = (* -------------------------------------------------------------------- *) 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 ?(src : string option) (scope : EcScope.scope) intf = @@ -329,7 +329,7 @@ and process_interface ?(src : string option) (scope : EcScope.scope) intf = (* -------------------------------------------------------------------- *) 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 ?src 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 } -> @@ -385,9 +385,9 @@ and process_axiom ?(src : string option) (scope : EcScope.scope) (ax : paxiom lo 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) = @@ -652,7 +652,7 @@ and process ?(src : string option) (ld : Loader.loader) (scope : EcScope.scope) | 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 ?src scope (mk_loc loc a)) - | GthOpen name -> `Fct (fun scope -> process_th_open scope name) + | 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) diff --git a/src/ecScope.ml b/src/ecScope.ml index 435dcf37d2..f36f501a68 100644 --- a/src/ecScope.ml +++ b/src/ecScope.ml @@ -340,8 +340,9 @@ type scope = { } and docstate = { - docentities : docentity list; - docstringbacklog : string list; + docentities : docentity list; + docstringbl : string list; + srcstringbl : string list; } and docentity = @@ -349,7 +350,7 @@ and docentity = | SubDoc of docentity list and docitem = - string (* raw definition *) + string list (* raw definition *) (* -------------------------------------------------------------------- *) (* let extend_globdoc (sc : scope) (doc : string) : scope = @@ -357,18 +358,24 @@ and docitem = module DocState = struct let empty : docstate = - { docentities = []; docstringbacklog = []; } + { docentities = []; + docstringbl = []; + srcstringbl = []; } (* let push_global (state : docstate) (doc : string) : docstate = { state with docentities = GlobalDoc doc :: state.docentities } *) - let push_backlog (state : docstate) (doc : string) : docstate = - { state with docstringbacklog = state.docstringbacklog @ [doc] } + let push_docbl (state : docstate) (docc : string) : docstate = + { state with docstringbl = state.docstringbl @ [docc] } - let add_item (state : docstate) (item : string) : docstate = + let push_srcbl (state : docstate) (srcs : string) : docstate = + { state with srcstringbl = state.srcstringbl @ [srcs] } + + let add_item (state : docstate) : docstate = { state with - docentities = state.docentities @ [ItemDoc (state.docstringbacklog, item)]; - docstringbacklog = [] } + docentities = state.docentities @ [ItemDoc (state.docstringbl, state.srcstringbl)]; + docstringbl = []; + srcstringbl = []; } let add_sub (state : docstate) (substate : docstate) : docstate = { state with @@ -525,7 +532,8 @@ let subscope (scope : scope) (mode : EcTheory.thmode) (name : symbol) lc = sc_pr_uc = None; sc_options = GenOptions.for_subscope scope.sc_options; sc_globdoc = []; - sc_locdoc = DocState.empty; } + sc_locdoc = DocState.empty; + } (* -------------------------------------------------------------------- *) module Prover = struct @@ -867,13 +875,13 @@ module Ax = struct let item = EcTheory.mkitem import (EcTheory.Th_schema (x, sc)) in { scope with sc_env = EcSection.add_item item scope.sc_env } - let bind ?(src : string option) ?(import = EcTheory.import0) (scope : scope) ((x, ax) : _ * axiom) = + let bind ?(import = EcTheory.import0) (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; - sc_locdoc = DocState.add_item scope.sc_locdoc (odfl "axiom" src)} - + sc_locdoc = DocState.add_item scope.sc_locdoc } + (* ------------------------------------------------------------------ *) let start_lemma scope (cont, axflags) check ?name (axd, ctxt) = let puc = @@ -897,7 +905,7 @@ module Ax = struct { scope with sc_pr_uc = Some puc } (* ------------------------------------------------------------------ *) - let rec add_r ?(src : string option) (scope : scope) (mode : mode) (ax : paxiom located) = + let rec add_r (scope : scope) (mode : mode) (ax : paxiom located) = assert (scope.sc_pr_uc = None); let env = env scope in @@ -977,7 +985,7 @@ module Ax = struct | PLemma tc -> begin let local = match ax.pa_locality with - | `Declare -> hierror ~loc "cannot mark with `declare` a lemma" + | `Declare -> hierror ~loc "cannot mark a lemma with `declare`" | `Local -> true | `Global -> false in @@ -1000,7 +1008,7 @@ module Ax = struct end | PAxiom _ -> - (Some (unloc ax.pa_name), bind ?src scope (unloc ax.pa_name, axd)) + (Some (unloc ax.pa_name), bind scope (unloc ax.pa_name, axd)) | PSchema -> assert false @@ -1122,7 +1130,11 @@ module Ax = struct (* ------------------------------------------------------------------ *) let add ?(src : string option) (scope : scope) (mode : mode) (ax : paxiom located) = - add_r ?src scope mode ax + let scope = + { scope with + sc_locdoc = DocState.push_srcbl scope.sc_locdoc (odfl "axiom/lemma" src)} + in + add_r scope mode ax (* ------------------------------------------------------------------ *) let realize (scope : scope) (mode : mode) (rl : prealize located) = @@ -1175,17 +1187,23 @@ module Op = struct module EHI = EcHiInductive let bind - ?(src : string option) ?(import = EcTheory.import0) + ?(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; - sc_locdoc = DocState.add_item scope.sc_locdoc (odfl "operator" src); } + sc_locdoc = DocState.add_item scope.sc_locdoc; } let add ?(src : string option) (scope : scope) (op : poperator located) = assert (scope.sc_pr_uc = None); + + let scope = { + scope with + sc_locdoc = DocState.push_srcbl scope.sc_locdoc (odfl "operator" src) } + 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 @@ -1278,7 +1296,7 @@ module Op = struct let scope = match op.po_ax with - | None -> bind ?src scope (unloc op.po_name, tyop) + | None -> bind scope (unloc op.po_name, tyop) | Some ax -> begin match tyop.op_kind with | OB_oper (Some (OP_Plain (bd, _))) -> @@ -1288,7 +1306,7 @@ module Op = struct let nargs = List.sum (List.map (List.length |- fst) op.po_args) in EcDecl.axiomatized_op ~nargs ~nosmt path (tyop.op_tparams, bd) lc in let tyop = { tyop with op_opaque = true; } in - let scope = bind ?src scope (unloc op.po_name, tyop) in + let scope = bind scope (unloc op.po_name, tyop) in Ax.bind scope (unloc ax, axop) | _ -> hierror ~loc "cannot axiomatize non-plain operators" @@ -1456,7 +1474,7 @@ module Op = struct op_clinline = false; } in - bind ?src scope (unloc op.ppo_name, opdecl) + bind scope (unloc op.ppo_name, opdecl) end (* -------------------------------------------------------------------- *) @@ -1465,9 +1483,12 @@ module Pred = struct let add ?(src : string option) (scope : scope) (pr : ppredicate located) = assert (scope.sc_pr_uc = None); - + let scope = { + scope with + sc_locdoc = DocState.push_srcbl scope.sc_locdoc (odfl "predicate" src) } + in let typr = EcHiPredicates.trans_preddecl (env scope) pr in - let scope = Op.bind ?src scope (unloc (unloc pr).pp_name, typr) in + let scope = Op.bind scope (unloc (unloc pr).pp_name, typr) in typr, scope end @@ -1508,14 +1529,14 @@ module Mod = struct (ur_empty Sm.empty) env - let bind ?(src : string option) ?(import = EcTheory.import0) (scope : scope) (m : top_module_expr) = + let bind ?(import = EcTheory.import0) (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; - sc_locdoc = DocState.add_item scope.sc_locdoc (odfl "module" src) } + sc_locdoc = DocState.add_item scope.sc_locdoc } - let add_concrete ?(src : string option) (scope : scope) lc (ptm : pmodule_def) = + let add_concrete (scope : scope) lc (ptm : pmodule_def) = assert (scope.sc_pr_uc = None); if lc = `Declare then @@ -1538,7 +1559,7 @@ module Mod = struct (EcPrinting.pp_list "@," pp) ur end; - bind ?src scope {tme_expr = m; tme_loca = lc} + bind scope {tme_expr = m; tme_loca = lc} let declare (scope : scope) (m : pmodule_decl) = let modty = m.ptm_modty in @@ -1551,9 +1572,14 @@ module Mod = struct sc_env = EcSection.add_decl_mod name tysig scope.sc_env } let add ?(src : string option) (scope : scope) (m : pmodule_def_or_decl) = + let scope = { + scope with + sc_locdoc = DocState.push_srcbl scope.sc_locdoc (odfl "module" src) } + in + match m with | { ptm_locality = lc; ptm_def = `Concrete def } -> - add_concrete ?src scope lc def + add_concrete scope lc def | { ptm_locality = lc; ptm_def = `Abstract decl } -> if lc <> `Declare then @@ -1569,19 +1595,23 @@ end (* -------------------------------------------------------------------- *) module ModType = struct let bind - ?(src : string option) ?(import = EcTheory.import0) (scope : scope) + ?(import = EcTheory.import0) (scope : scope) ((x, tysig) : _ * top_module_sig) = 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; - sc_locdoc = DocState.add_item scope.sc_locdoc (odfl "moduletype" src)} + sc_locdoc = DocState.add_item scope.sc_locdoc } let add ?(src : string option) (scope : scope) (intf : pinterface) = assert (scope.sc_pr_uc = None); + let scope = { + scope with + sc_locdoc = DocState.push_srcbl scope.sc_locdoc (odfl "moduletype" src) } + in let tysig = EcTyping.transmodsig (env scope) intf in - bind ?src scope (unloc intf.pi_name, tysig) + bind scope (unloc intf.pi_name, tysig) end (* -------------------------------------------------------------------- *) @@ -1602,15 +1632,20 @@ module Ty = struct hierror ~loc:x.pl_loc "duplicated type/type-class name `%s'" x.pl_desc (* ------------------------------------------------------------------ *) - let bind ?(src : string option) ?(import = EcTheory.import0) (scope : scope) ((x, tydecl) : (_ * tydecl)) = + let bind ?(import = EcTheory.import0) (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; - sc_locdoc = DocState.add_item scope.sc_locdoc (odfl "type" src)} + sc_locdoc = DocState.add_item scope.sc_locdoc } (* ------------------------------------------------------------------ *) let add ?(src : string option) scope (tyd : ptydecl located) = + let scope = { + scope with + sc_locdoc = DocState.push_srcbl scope.sc_locdoc (odfl "type" src) } + in + let loc = loc tyd in let { pty_name = name; pty_tyvars = args; @@ -1647,7 +1682,7 @@ module Ty = struct record.ELI.rc_tparams, `Record (scheme, record.ELI.rc_fields) in - bind ?src scope (unloc name, { tyd_params; tyd_type; tyd_loca; tyd_resolve = true; }) + bind scope (unloc name, { tyd_params; tyd_type; tyd_loca; tyd_resolve = true; }) (* ------------------------------------------------------------------ *) let bindclass ?(import = EcTheory.import0) (scope : scope) (x, tc) = @@ -2013,11 +2048,11 @@ module Theory = struct exception TopScope (* ------------------------------------------------------------------ *) - let bind ?(src : string option) (scope : scope) (x, cth) = + let bind (scope : scope) (x, cth) = assert (scope.sc_pr_uc = None); { scope with sc_env = EcSection.add_th ~import:EcTheory.import0 x cth scope.sc_env; - sc_locdoc = DocState.add_item scope.sc_locdoc (odfl "theory" src)} + sc_locdoc = DocState.add_item scope.sc_locdoc} (* ------------------------------------------------------------------ *) let required (scope : scope) (name : required_info) = @@ -2039,8 +2074,12 @@ 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 scope = { + scope with + sc_locdoc = DocState.push_srcbl scope.sc_locdoc (odfl "theory" src) } + in subscope scope mode name (* ------------------------------------------------------------------ *) @@ -2087,13 +2126,13 @@ module Theory = struct ((cth, required), scope.sc_name, sup) (* ------------------------------------------------------------------ *) - let exit ?(src : string option) ?(pempty = `ClearOnly) ?(clears =[]) (scope : scope) = + let exit ?(pempty = `ClearOnly) ?(clears =[]) (scope : scope) = assert (scope.sc_pr_uc = None); let cth = exit_r ~pempty (add_clears clears scope) in let ((cth, required), (name, _), scope) = cth in let scope = List.fold_right require_loaded required scope in - let scope = ofold (fun cth scope -> bind ?src scope (name, cth)) scope cth in + let scope = ofold (fun cth scope -> bind scope (name, cth)) scope cth in (name, scope) (* ------------------------------------------------------------------ *) @@ -2471,11 +2510,11 @@ end (* -------------------------------------------------------------------- *) module DocComment = struct - let add (scope : scope) ((kind, doc) : [`Global | `Item] * string) : scope = + let add (scope : scope) ((kind, docc) : [`Global | `Item] * string) : scope = match kind with | `Global -> - { scope with sc_globdoc = scope.sc_globdoc @ [doc] } + { scope with sc_globdoc = scope.sc_globdoc @ [docc] } | `Item -> - { scope with sc_locdoc = DocState.push_backlog scope.sc_locdoc doc } + { scope with sc_locdoc = DocState.push_docbl scope.sc_locdoc docc } end diff --git a/src/ecScope.mli b/src/ecScope.mli index e171a030e5..0b1a1d0809 100644 --- a/src/ecScope.mli +++ b/src/ecScope.mli @@ -137,13 +137,12 @@ 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. *) val exit : - ?src:string - -> ?pempty:[`ClearOnly | `Full | `No] + ?pempty:[`ClearOnly | `Full | `No] -> ?clears:(pqsymbol option) list -> scope -> symbol * scope