Skip to content

Commit

Permalink
Incorporate source string in documentation of standard objects. Still…
Browse files Browse the repository at this point in the history 
… unsure about processing types, axioms, and theories.
  • Loading branch information
@MM45
MM45 committed Oct 4, 2023
1 parent cf57b93 commit 50b6bc4
Show file tree
Hide file tree
Showing 3 changed files with 60 additions and 59 deletions.
44 changes: 22 additions & 22 deletions src/ecCommands.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -294,15 +294,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_typeclass (scope : EcScope.scope) (tcd : ptypeclass located) =
Expand All @@ -317,17 +317,17 @@ 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

(* -------------------------------------------------------------------- *)
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) ?(src : string option) (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 ?src pop in
let ppe = EcPrinting.PPEnv.ofenv (EcScope.env scope) in
Expand All @@ -341,14 +341,14 @@ and process_operator (scope : EcScope.scope) ?(src : string option) (pop : poper
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;
Expand All @@ -372,10 +372,10 @@ 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;
(* TODO: A: aybe rename, as this now also adds schemata. *)
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
Expand Down Expand Up @@ -635,23 +635,23 @@ and process_dump scope (source, tc) =
scope

(* -------------------------------------------------------------------- *)
and process ?src (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))
| 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 ?src (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))
| Gaxiom a -> `Fct (fun scope -> process_axiom ?src scope (mk_loc loc a))
| GthOpen name -> `Fct (fun scope -> process_th_open scope name)
| GthClose info -> `Fct (fun scope -> process_th_close scope info)
| GthClear info -> `Fct (fun scope -> process_th_clear scope info)
Expand Down
58 changes: 29 additions & 29 deletions src/ecScope.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -867,12 +867,12 @@ 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 ?(import = EcTheory.import0) (scope : scope) ((x, ax) : _ * axiom) =
let bind ?(src : string option) ?(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 "axiom" }
sc_locdoc = DocState.add_item scope.sc_locdoc (odfl "axiom" src)}

(* ------------------------------------------------------------------ *)
let start_lemma scope (cont, axflags) check ?name (axd, ctxt) =
Expand All @@ -897,7 +897,7 @@ module Ax = struct
{ scope with sc_pr_uc = Some puc }

(* ------------------------------------------------------------------ *)
let rec add_r (scope : scope) (mode : mode) (ax : paxiom located) =
let rec add_r ?(src : string option) (scope : scope) (mode : mode) (ax : paxiom located) =
assert (scope.sc_pr_uc = None);

let env = env scope in
Expand Down Expand Up @@ -1000,7 +1000,7 @@ module Ax = struct
end

| PAxiom _ ->
(Some (unloc ax.pa_name), bind scope (unloc ax.pa_name, axd))
(Some (unloc ax.pa_name), bind ?src scope (unloc ax.pa_name, axd))

| PSchema ->
assert false
Expand Down Expand Up @@ -1121,8 +1121,8 @@ module Ax = struct
snd (save_r ~mode:`Abort scope)

(* ------------------------------------------------------------------ *)
let add (scope : scope) (mode : mode) (ax : paxiom located) =
add_r scope mode ax
let add ?(src : string option) (scope : scope) (mode : mode) (ax : paxiom located) =
add_r ?src scope mode ax

(* ------------------------------------------------------------------ *)
let realize (scope : scope) (mode : mode) (rl : prealize located) =
Expand Down Expand Up @@ -1184,7 +1184,7 @@ module Op = struct
sc_env = EcSection.add_item item scope.sc_env;
sc_locdoc = DocState.add_item scope.sc_locdoc (odfl "operator" src); }

let add (scope : scope) ?(src : string option) (op : poperator located) =
let add ?(src : string option) (scope : scope) (op : poperator located) =
assert (scope.sc_pr_uc = None);
let op = op.pl_desc and loc = op.pl_loc in
let eenv = env scope in
Expand Down Expand Up @@ -1416,7 +1416,7 @@ 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 op = unloc op in
Expand Down Expand Up @@ -1456,18 +1456,18 @@ module Op = struct
op_clinline = false;
} in

bind scope (unloc op.ppo_name, opdecl)
bind ?src scope (unloc op.ppo_name, opdecl)
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 typr = EcHiPredicates.trans_preddecl (env scope) pr in
let scope = Op.bind scope (unloc (unloc pr).pp_name, typr) in
let scope = Op.bind ?src scope (unloc (unloc pr).pp_name, typr) in
typr, scope
end

Expand Down Expand Up @@ -1508,14 +1508,14 @@ module Mod = struct
(ur_empty Sm.empty)
env

let bind ?(import = EcTheory.import0) (scope : scope) (m : top_module_expr) =
let bind ?(src : string option) ?(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 "module" }
sc_locdoc = DocState.add_item scope.sc_locdoc (odfl "module" src) }

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
Expand All @@ -1538,7 +1538,7 @@ module Mod = struct
(EcPrinting.pp_list "@," pp) ur
end;

bind scope {tme_expr = m; tme_loca = lc}
bind ?src scope {tme_expr = m; tme_loca = lc}

let declare (scope : scope) (m : pmodule_decl) =
let modty = m.ptm_modty in
Expand All @@ -1550,10 +1550,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
Expand All @@ -1569,19 +1569,19 @@ end
(* -------------------------------------------------------------------- *)
module ModType = struct
let bind
?(import = EcTheory.import0) (scope : scope)
?(src : string option) ?(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 "moduletype" }
sc_locdoc = DocState.add_item scope.sc_locdoc (odfl "moduletype" src)}

let add (scope : scope) (intf : pinterface) =
let add ?(src : string option) (scope : scope) (intf : pinterface) =
assert (scope.sc_pr_uc = None);
let tysig = EcTyping.transmodsig (env scope) intf in
bind scope (unloc intf.pi_name, tysig)
bind ?src scope (unloc intf.pi_name, tysig)
end

(* -------------------------------------------------------------------- *)
Expand All @@ -1602,15 +1602,15 @@ module Ty = struct
hierror ~loc:x.pl_loc "duplicated type/type-class name `%s'" x.pl_desc

(* ------------------------------------------------------------------ *)
let bind ?(import = EcTheory.import0) (scope : scope) ((x, tydecl) : (_ * tydecl)) =
let bind ?(src : string option) ?(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 "type" }
sc_locdoc = DocState.add_item scope.sc_locdoc (odfl "type" src)}

(* ------------------------------------------------------------------ *)
let add scope (tyd : ptydecl located) =
let add ?(src : string option) scope (tyd : ptydecl located) =
let loc = loc tyd in

let { pty_name = name; pty_tyvars = args;
Expand Down Expand Up @@ -1647,7 +1647,7 @@ module Ty = struct
record.ELI.rc_tparams, `Record (scheme, record.ELI.rc_fields)
in

bind scope (unloc name, { tyd_params; tyd_type; tyd_loca; tyd_resolve = true; })
bind ?src scope (unloc name, { tyd_params; tyd_type; tyd_loca; tyd_resolve = true; })

(* ------------------------------------------------------------------ *)
let bindclass ?(import = EcTheory.import0) (scope : scope) (x, tc) =
Expand Down Expand Up @@ -2013,11 +2013,11 @@ module Theory = struct
exception TopScope

(* ------------------------------------------------------------------ *)
let bind (scope : scope) (x, cth) =
let bind ?(src : string option) (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 "theory" }
sc_locdoc = DocState.add_item scope.sc_locdoc (odfl "theory" src)}

(* ------------------------------------------------------------------ *)
let required (scope : scope) (name : required_info) =
Expand Down Expand Up @@ -2087,13 +2087,13 @@ module Theory = struct
((cth, required), scope.sc_name, sup)

(* ------------------------------------------------------------------ *)
let exit ?(pempty = `ClearOnly) ?(clears =[]) (scope : scope) =
let exit ?(src : string option) ?(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 scope (name, cth)) scope cth in
let scope = ofold (fun cth scope -> bind ?src scope (name, cth)) scope cth in
(name, scope)

(* ------------------------------------------------------------------ *)
Expand Down
17 changes: 9 additions & 8 deletions src/ecScope.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -88,21 +88,21 @@ end

(* -------------------------------------------------------------------- *)
module Op : sig
val add : scope -> ?src:string -> 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 mode = [`WeakCheck | `Check | `Report]

val add : scope -> mode -> paxiom located -> symbol option * scope
val add : ?src:string -> scope -> mode -> paxiom located -> symbol option * scope
val save : scope -> string option * scope
val admit : scope -> string option * scope
val abort : scope -> scope
Expand All @@ -111,22 +111,22 @@ end

(* -------------------------------------------------------------------- *)
module Ty : sig
val add : scope -> ptydecl located -> scope
val add : ?src:string -> scope -> ptydecl located -> scope

val add_class : scope -> ptypeclass located -> scope
val add_instance : ?import:EcTheory.import -> scope -> Ax.mode -> ptycinstance located -> scope
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

(* -------------------------------------------------------------------- *)
Expand All @@ -142,7 +142,8 @@ module Theory : sig
(* [exit scope] close and finalize the top-most theory and returns
* its name. Raises [TopScope] if [scope] has not super scope. *)
val exit :
?pempty:[`ClearOnly | `Full | `No]
?src:string
-> ?pempty:[`ClearOnly | `Full | `No]
-> ?clears:(pqsymbol option) list
-> scope -> symbol * scope

Expand Down

0 comments on commit 50b6bc4

Please sign in to comment.