exception IncludedFileNotCompiled of string * string
exception MetadataNotFound of string (* file name *)
-type status = {
+type lexicon_status = {
aliases: L.alias_spec DisambiguateTypes.Environment.t;
multi_aliases: L.alias_spec list DisambiguateTypes.Environment.t;
lexicon_content_rev: LexiconMarshal.lexicon;
notation_ids: CicNotation.notation_id list; (** in-scope notation ids *)
}
-let dump_aliases out msg status =
- out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:");
- DisambiguateTypes.Environment.iter
- (fun _ x -> out (LexiconAstPp.pp_alias x))
- status.aliases
-
let initial_status = {
aliases = DisambiguateTypes.Environment.empty;
multi_aliases = DisambiguateTypes.Environment.empty;
notation_ids = [];
}
+class type g_status =
+ object
+ method lstatus: lexicon_status
+ end
+
+class status =
+ object(self)
+ val lstatus = initial_status
+ method lstatus = lstatus
+ method set_lstatus v = {< lstatus = v >}
+ method set_lexicon_engine_status : 'status. #g_status as 'status -> 'self
+ = fun o -> self#set_lstatus o#lstatus
+ end
+
+let dump_aliases out msg status =
+ out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:");
+ DisambiguateTypes.Environment.iter
+ (fun _ x -> out (LexiconAstPp.pp_alias x))
+ status#lstatus.aliases
+
let add_lexicon_content cmds status =
- let content = status.lexicon_content_rev in
+ let content = status#lstatus.lexicon_content_rev in
let content' =
List.fold_right
(fun cmd acc ->
String.concat "; " (List.map LexiconAstPp.pp_command content')
);
*)
- { status with lexicon_content_rev = content' }
+ status#set_lstatus
+ { status#lstatus with lexicon_content_rev = content' }
let set_proof_aliases mode status new_aliases =
if mode = L.WithoutPreferences then
in
let aliases =
List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
- status.aliases new_aliases in
+ status#lstatus.aliases new_aliases in
let multi_aliases =
List.fold_left (fun acc (d,c) ->
DisambiguateTypes.Environment.cons L.description_of_alias
d c acc)
- status.multi_aliases new_aliases
+ status#lstatus.multi_aliases new_aliases
in
let new_status =
- { status with multi_aliases = multi_aliases ; aliases = aliases}
- in
- if new_aliases = [] then
- new_status
- else
- let status =
- add_lexicon_content (commands_of_aliases new_aliases) new_status
- in
- status
-
+ { status#lstatus with
+ multi_aliases = multi_aliases ; aliases = aliases} in
+ let new_status = status#set_lstatus new_status in
+ if new_aliases = [] then
+ new_status
+ else
+ add_lexicon_content (commands_of_aliases new_aliases) new_status
-let rec eval_command ?(mode=L.WithPreferences) status cmd =
+let rec eval_command ?(mode=L.WithPreferences) sstatus cmd =
(*
let bmode = match mode with L.WithPreferences -> true | _ -> false in
Printf.eprintf "Include preferences: %b\n" bmode;
*)
+ let status = sstatus#lstatus in
let cmd =
match cmd with
| L.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) ->
with Not_found ->
prerr_endline ("LexiconEngine.eval_command: domain item not found: " ^
(DisambiguateTypes.string_of_domain_item item));
- dump_aliases prerr_endline "" status;
- assert false
+ dump_aliases prerr_endline "" sstatus;
+ raise (Failure (
+ (DisambiguateTypes.string_of_domain_item item) ^
+ " not found"));
end
| p -> p
in
let notation_ids' = CicNotation.process_notation cmd in
let status =
{ status with notation_ids = notation_ids' @ status.notation_ids } in
+ let sstatus = sstatus#set_lstatus status in
match cmd with
| L.Include (loc, baseuri, mode, fullpath) ->
let lexiconpath_rw, lexiconpath_r =
raise (IncludedFileNotCompiled (lexiconpath_rw,fullpath))
in
let lexicon = LexiconMarshal.load_lexicon lexiconpath in
- let status = List.fold_left (eval_command ~mode) status lexicon in
- status
+ List.fold_left (eval_command ~mode) sstatus lexicon
| L.Alias (loc, spec) ->
let diff =
(*CSC: Warning: this code should be factorized with the corresponding
| L.Number_alias (instance,desc) ->
[DisambiguateTypes.Num instance,spec]
in
- set_proof_aliases mode status diff
+ set_proof_aliases mode sstatus diff
| L.Interpretation (_, dsc, (symbol, _), _) as stm ->
- let status = add_lexicon_content [stm] status in
+ let sstatus = add_lexicon_content [stm] sstatus in
let diff =
try
[DisambiguateTypes.Symbol (symbol, 0),
prerr_endline (Lazy.force msg);
assert false
in
- let status = set_proof_aliases mode status diff in
- status
+ let sstatus = set_proof_aliases mode sstatus diff in
+ sstatus
| L.Notation _ as stm ->
- add_lexicon_content [stm] status
+ add_lexicon_content [stm] sstatus
let eval_command status cmd =
if !debug then dump_aliases prerr_endline "before eval_command" status;