(* $Id$ *)
-let out = ref ignore
+module L = LexiconAst
-let set_callback f = out := f
+let debug = ref true
(* lexicon file name * ma file name *)
exception IncludedFileNotCompiled of string * string
exception MetadataNotFound of string (* file name *)
type status = {
- aliases: LexiconAst.alias_spec DisambiguateTypes.Environment.t;
- multi_aliases: LexiconAst.alias_spec list DisambiguateTypes.Environment.t;
+ 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;
List.fold_right
(fun cmd acc ->
match cmd with
- | LexiconAst.Alias _
- | LexiconAst.Include _
- | LexiconAst.Notation _ -> cmd :: (List.filter ((<>) cmd) acc)
- | LexiconAst.Interpretation _ -> if List.exists ((=) cmd) acc then acc else cmd::acc)
+ | L.Alias _
+ | L.Include _
+ | L.Notation _ -> cmd :: (List.filter ((<>) cmd) acc)
+ | L.Interpretation _ -> if List.exists ((=) cmd) acc then acc else cmd::acc)
cmds content
in
-(* prerr_endline ("new lexicon content: " ^ String.concat " " (List.map
- LexiconAstPp.pp_command content')); *)
+(*
+ prerr_endline ("new lexicon content: " ^
+ String.concat "; " (List.map LexiconAstPp.pp_command content')
+ );
+*)
{ status with lexicon_content_rev = content' }
let set_proof_aliases mode status new_aliases =
- if mode = LexiconAst.WithoutPreferences then
+ if mode = L.WithoutPreferences then
status
else
let commands_of_aliases =
List.map
- (fun _,alias -> LexiconAst.Alias (HExtlib.dummy_floc, alias))
+ (fun _,alias -> L.Alias (HExtlib.dummy_floc, alias))
in
let aliases =
List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc)
status.aliases new_aliases in
let multi_aliases =
List.fold_left (fun acc (d,c) ->
- DisambiguateTypes.Environment.cons LexiconAst.description_of_alias
+ DisambiguateTypes.Environment.cons L.description_of_alias
d c acc)
status.multi_aliases new_aliases
in
status
-let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd =
+let rec eval_command ?(mode=L.WithPreferences) status cmd =
+(*
+ let bmode = match mode with L.WithPreferences -> true | _ -> false in
+ Printf.eprintf "Include preferences: %b\n" bmode;
+*)
let cmd =
match cmd with
- | LexiconAst.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) ->
+ | L.Interpretation (loc, dsc, (symbol, args), cic_appl_pattern) ->
let rec disambiguate =
function
CicNotationPt.ApplPattern l ->
(function (CicNotationPt.IdentArg (_,id')) -> id'=id) args)
->
let item = DisambiguateTypes.Id id in
- (try
+ begin try
let uri =
match DisambiguateTypes.Environment.find item status.aliases with
- LexiconAst.Ident_alias (_, uri)-> UriManager.uri_of_string uri
+ L.Ident_alias (_, uri)-> UriManager.uri_of_string uri
| _ -> assert false
in
CicNotationPt.UriPattern uri
with Not_found ->
- prerr_endline ("Domain item not found: " ^
+ prerr_endline ("LexiconEngine.eval_command: domain item not found: " ^
(DisambiguateTypes.string_of_domain_item item));
- assert false)
+ dump_aliases prerr_endline "" status;
+ assert false
+ end
| p -> p
in
- LexiconAst.Interpretation
+ L.Interpretation
(loc, dsc, (symbol, args), disambiguate cic_appl_pattern)
| _-> cmd
in
- !out cmd;
let notation_ids' = CicNotation.process_notation cmd in
let status =
{ status with notation_ids = notation_ids' @ status.notation_ids } in
match cmd with
- | LexiconAst.Include (loc, baseuri, mode, fullpath) ->
+ | L.Include (loc, baseuri, mode, fullpath) ->
let lexiconpath_rw, lexiconpath_r =
LibraryMisc.lexicon_file_of_baseuri
~must_exist:false ~writable:true ~baseuri,
let lexicon = LexiconMarshal.load_lexicon lexiconpath in
let status = List.fold_left (eval_command ~mode) status lexicon in
status
- | LexiconAst.Alias (loc, spec) ->
+ | L.Alias (loc, spec) ->
let diff =
(*CSC: Warning: this code should be factorized with the corresponding
code in DisambiguatePp *)
match spec with
- | LexiconAst.Ident_alias (id,uri) ->
+ | L.Ident_alias (id,uri) ->
[DisambiguateTypes.Id id,spec]
- | LexiconAst.Symbol_alias (symb, instance, desc) ->
+ | L.Symbol_alias (symb, instance, desc) ->
[DisambiguateTypes.Symbol (symb,instance),spec]
- | LexiconAst.Number_alias (instance,desc) ->
+ | L.Number_alias (instance,desc) ->
[DisambiguateTypes.Num instance,spec]
in
set_proof_aliases mode status diff
- | LexiconAst.Interpretation (_, dsc, (symbol, _), _) as stm ->
+ | L.Interpretation (_, dsc, (symbol, _), _) as stm ->
let status = add_lexicon_content [stm] status in
let diff =
try
[DisambiguateTypes.Symbol (symbol, 0),
- LexiconAst.Symbol_alias (symbol,0,dsc)]
+ L.Symbol_alias (symbol,0,dsc)]
with
DisambiguateChoices.Choice_not_found msg ->
prerr_endline (Lazy.force msg);
in
let status = set_proof_aliases mode status diff in
status
- | LexiconAst.Notation _ as stm ->
+ | L.Notation _ as stm ->
add_lexicon_content [stm] status
-let eval_command = eval_command ?mode:None
+let eval_command status cmd =
+ if !debug then dump_aliases prerr_endline "before eval_command" status;
+ let status = eval_command ?mode:None status cmd in
+ if !debug then dump_aliases prerr_endline "after eval_command" status;
+ status
-let set_proof_aliases = set_proof_aliases LexiconAst.WithPreferences
-
+let set_proof_aliases status aliases =
+ if !debug then dump_aliases prerr_endline "before set_proof_aliases" status;
+ let status = set_proof_aliases L.WithPreferences status aliases in
+ if !debug then dump_aliases prerr_endline "after set_proof_aliases" status;
+ status
projects / helm.git / blobdiff