[] subst in
[ Node ([loc], Id name, terms) ]))
| Ast.Uri _ -> []
- | Ast.Implicit -> []
+ | Ast.NRef _ -> []
+ | Ast.NCic _ -> []
+ | Ast.Implicit _ -> []
| Ast.Num (num, i) -> [ Node ([loc], Num i, []) ]
| Ast.Meta (index, local_context) ->
List.fold_left
let domain_of_obj ~context ast =
assert (context = []);
match ast with
- | Ast.Theorem (_,_,ty,bo) ->
+ | Ast.Theorem (_,_,ty,bo,_) ->
domain_of_term [] ty
@ (match bo with
None -> []
in
aux dom1
-module type Disambiguator =
-sig
- val disambiguate_thing:
- context:'context ->
- metasenv:'metasenv ->
- subst:'subst ->
- use_coercions:bool ->
- string_context_of_context:('context -> string option list) ->
- initial_ugraph:'ugraph ->
- hint:
- ('metasenv -> 'raw_thing -> 'raw_thing) *
- (('refined_thing,'metasenv,'subst,'ugraph) test_result ->
- ('refined_thing,'metasenv,'subst,'ugraph) test_result) ->
- mk_implicit:(bool -> 'alias) ->
- description_of_alias:('alias -> string) ->
- aliases:'alias DisambiguateTypes.Environment.t ->
- universe:'alias list DisambiguateTypes.Environment.t option ->
- lookup_in_library:(
- DisambiguateTypes.interactive_user_uri_choice_type ->
- DisambiguateTypes.input_or_locate_uri_type ->
- DisambiguateTypes.Environment.key ->
- 'alias list) ->
- uri:'uri ->
- pp_thing:('ast_thing -> string) ->
- domain_of_thing:(context: string option list -> 'ast_thing -> domain) ->
- interpretate_thing:(
- context:'context ->
- env:'alias DisambiguateTypes.Environment.t ->
- uri:'uri ->
- is_path:bool ->
- 'ast_thing ->
- localization_tbl:'cichash ->
- 'raw_thing) ->
- refine_thing:(
- 'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
- 'raw_thing -> 'ugraph -> localization_tbl:'cichash ->
- ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
- mk_localization_tbl:(int -> 'cichash) ->
- string * int * 'ast_thing ->
- ((DisambiguateTypes.Environment.key * 'alias) list *
- 'metasenv * 'subst * 'refined_thing * 'ugraph)
- list * bool
-end
-
let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
+type alias_spec =
+ | Ident_alias of string * string (* identifier, uri *)
+ | Symbol_alias of string * int * string (* name, instance no, description *)
+ | Number_alias of int * string (* instance no, description *)
+
let disambiguate_thing
~context ~metasenv ~subst ~use_coercions
~string_context_of_context
- ~initial_ugraph:base_univ ~hint
- ~mk_implicit ~description_of_alias
+ ~initial_ugraph:base_univ ~expty
+ ~mk_implicit ~description_of_alias ~fix_instance
~aliases ~universe ~lookup_in_library
~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing
~mk_localization_tbl
input_or_locate_uri item
| Some e ->
(try
- let item =
- match item with
- | Symbol (symb, _) -> Symbol (symb, 0)
- | item -> item
- in
- Environment.find item e
- with Not_found ->
- lookup_in_library
- interactive_user_uri_choice
- input_or_locate_uri item)
+ fix_instance item (Environment.find item e)
+ with Not_found -> [])
in
+
+ (* items with 1 choice are interpreted ASAP *)
+ let aliases, todo_dom =
+ let rec aux (aliases,acc) = function
+ | [] -> aliases, acc
+ | (Node (_, item,extra) as node) :: tl ->
+ let choices = lookup_choices item in
+ if List.length choices <> 1 then aux (aliases, acc@[node]) tl
+ else
+ let tl = tl @ extra in
+ if Environment.mem item aliases then aux (aliases, acc) tl
+ else aux (Environment.add item (List.hd choices) aliases, acc) tl
+ in
+ aux (aliases,[]) todo_dom
+ in
+
(*
(* <benchmark> *)
let _ =
interpretate_thing ~context ~env:filled_env
~uri ~is_path:false thing ~localization_tbl
in
- let cic_thing = (fst hint) metasenv cic_thing in
let foo () =
- let k =
refine_thing metasenv subst context uri
- ~use_coercions cic_thing ugraph ~localization_tbl
- in
- let k = (snd hint) k in
- k
+ ~use_coercions cic_thing expty ugraph ~localization_tbl
in refine_profiler.HExtlib.profile foo ()
with
| Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))