method disambiguate_db: db
end
-class status =
+class virtual status =
object (self)
inherit Interpretations.status
val disambiguate_db = initial_status
;;
-let disambiguate_nterm estatus expty context metasenv subst thing
+let disambiguate_nterm status expty context metasenv subst thing
=
let diff, metasenv, subst, cic =
singleton "first"
(NCicDisambiguate.disambiguate_term
- ~rdb:estatus
- ~aliases:estatus#disambiguate_db.aliases
+ status
+ ~aliases:status#disambiguate_db.aliases
~expty
- ~universe:(Some estatus#disambiguate_db.multi_aliases)
+ ~universe:(Some status#disambiguate_db.multi_aliases)
~lookup_in_library:nlookup_in_library
- ~mk_choice:(ncic_mk_choice estatus)
+ ~mk_choice:(ncic_mk_choice status)
~mk_implicit ~fix_instance
~description_of_alias:GrafiteAst.description_of_alias
~context ~metasenv ~subst thing)
in
- let estatus =
- set_proof_aliases estatus ~implicit_aliases:true GrafiteAst.WithPreferences
+ let status =
+ set_proof_aliases status ~implicit_aliases:true GrafiteAst.WithPreferences
diff
in
- metasenv, subst, estatus, cic
+ metasenv, subst, status, cic
;;
NotationPt.term Disambiguate.disambiguator_input option *
(string * NCic.term) list * NCic.term option
-let disambiguate_npattern (text, prefix_len, (wanted, hyp_paths, goal_path)) =
- let interp path = NCicDisambiguate.disambiguate_path path in
+let disambiguate_npattern status (text, prefix_len, (wanted, hyp_paths, goal_path)) =
+ let interp path = NCicDisambiguate.disambiguate_path status path in
let goal_path = HExtlib.map_option interp goal_path in
let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
- let wanted =
- match wanted with None -> None | Some x -> Some (text,prefix_len,x)
- in
+ let wanted = HExtlib.map_option (fun x -> text,prefix_len,x) wanted in
(wanted, hyp_paths, goal_path)
;;
-let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function
+let disambiguate_reduction_kind text prefix_len = function
| `Unfold (Some t) -> assert false (* MATITA 1.0 *)
| `Normalize
| `Simpl
metasenv, `Auto params
;;
-let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
+let disambiguate_nobj status ?baseuri (text,prefix_len,obj) =
let uri =
let baseuri =
match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
match obj with
| NotationPt.Inductive (_,(name,_,_,_)::_)
| NotationPt.Record (_,name,_,_) -> name ^ ".ind"
- | NotationPt.Theorem (_,name,_,_,_) -> name ^ ".con"
+ | NotationPt.Theorem (name,_,_,_) -> name ^ ".con"
| NotationPt.Inductive _ -> assert false
in
NUri.uri_of_string (baseuri ^ "/" ^ name)
let diff, _, _, cic =
singleton "third"
(NCicDisambiguate.disambiguate_obj
+ status
~lookup_in_library:nlookup_in_library
~description_of_alias:GrafiteAst.description_of_alias
- ~mk_choice:(ncic_mk_choice estatus)
- ~mk_implicit ~fix_instance
- ~uri
- ~rdb:estatus
- ~aliases:estatus#disambiguate_db.aliases
- ~universe:(Some estatus#disambiguate_db.multi_aliases)
+ ~mk_choice:(ncic_mk_choice status)
+ ~mk_implicit ~fix_instance ~uri
+ ~aliases:status#disambiguate_db.aliases
+ ~universe:(Some status#disambiguate_db.multi_aliases)
(text,prefix_len,obj)) in
- let estatus =
- set_proof_aliases estatus ~implicit_aliases:true GrafiteAst.WithPreferences
+ let status =
+ set_proof_aliases status ~implicit_aliases:true GrafiteAst.WithPreferences
diff
in
- estatus, cic
+ status, cic
;;
let disambiguate_cic_appl_pattern status args =
disambiguate
;;
-let aliases_for_objs refs =
+let aliases_for_objs status refs =
List.concat
(List.map
(fun nref ->
let references = NCicLibrary.aliases_of nref in
List.map
(fun u ->
- let name = NCicPp.r2s true u in
+ let name = NCicPp.r2s status true u in
DisambiguateTypes.Id name,
GrafiteAst.Ident_alias (name,NReference.string_of_reference u)
) references) refs)