- match obj with
- | CicNotationPt.Inductive (_,(name,_,_,_)::_)
- | CicNotationPt.Record (_,name,_,_) ->
- (match baseuri with
- | Some baseuri ->
- Some (UriManager.uri_of_string (baseuri ^ "/" ^ name ^ ".ind"))
- | None -> raise BaseUriNotSetYet)
- | CicNotationPt.Inductive _ -> assert false
- | CicNotationPt.Theorem _ -> None in
- let (diff, metasenv, cic, _) =
- singleton
- (GrafiteDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ())
- ~aliases:lexicon_status.LexiconEngine.aliases
- ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri
- (text,prefix_len,obj)) in
- let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
- lexicon_status, metasenv, cic
+ let baseuri =
+ match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
+ in
+ let name =
+ match obj with
+ | CicNotationPt.Inductive (_,(name,_,_,_)::_)
+ | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind"
+ | CicNotationPt.Theorem (_,name,_,_) -> name ^ ".con"
+ | CicNotationPt.Inductive _ -> assert false
+ in
+ UriManager.uri_of_string (baseuri ^ "/" ^ name)
+ in
+(*
+ let _try_new cic =
+ (NCicLibrary.clear_cache ();
+ NCicEnvironment.invalidate ();
+ OCic2NCic.clear ();
+ let graph =
+ match cic with
+ | Some (Cic.CurrentProof (_,metasenv, _, ty,_,_)) ->
+ let _, ugraph =
+ CicTypeChecker.type_of_aux' metasenv [] ty CicUniv.empty_ugraph
+ in
+ ugraph
+ | Some (Cic.Constant (_,_, ty,_,_)) ->
+ let _, ugraph =
+ CicTypeChecker.type_of_aux' [] [] ty CicUniv.empty_ugraph
+ in
+ ugraph
+ | _ -> CicUniv.empty_ugraph
+ in
+
+(*
+ prerr_endline "PRIMA COERCIONS";
+ let _,l = CicUniv.do_rank graph in
+ List.iter (fun k ->
+ prerr_endline (CicUniv.string_of_universe k ^ " = " ^ string_of_int
+ (CicUniv.get_rank k))) l;
+*)
+
+ let graph =
+ List.fold_left
+ (fun graph (_,_,l) ->
+ List.fold_left
+ (fun graph (uri,_,_) ->
+ let _,g = CicTypeChecker.typecheck uri in
+ CicUniv.merge_ugraphs ~base_ugraph:graph ~increment:(g,uri))
+ graph l)
+ graph (CoercDb.to_list (CoercDb.dump ()))
+ in
+ ignore(CicUniv.do_rank graph);
+
+
+(*
+ prerr_endline "DOPO COERCIONS";
+ let _,l = CicUniv.do_rank graph in
+ List.iter (fun k ->
+ prerr_endline (CicUniv.string_of_universe k ^ " = " ^ string_of_int
+ (CicUniv.get_rank k))) l;
+*)
+
+
+ prerr_endline "INIZIO NUOVA DISAMBIGUAZIONE";
+ let time = Unix.gettimeofday () in
+ (try
+ (match
+ NCicDisambiguate.disambiguate_obj
+ ~rdb:estatus
+ ~lookup_in_library:nlookup_in_library
+ ~description_of_alias:LexiconAst.description_of_alias
+ ~mk_choice:ncic_mk_choice
+ ~mk_implicit
+ ~uri:(OCic2NCic.nuri_of_ouri uri)
+ ~aliases:estatus#lstatus.LexiconEngine.aliases
+ ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases)
+ (text,prefix_len,obj)
+ with
+ | [_,_,_,obj],_ ->
+ let time = Unix.gettimeofday () -. time in
+(* NCicTypeChecker.typecheck_obj obj; *)
+ prerr_endline ("NUOVA DISAMBIGUAZIONE OK: "^ string_of_float time);
+(*
+ let obj =
+ let u,i,m,_,o = obj in
+ u,i,m,[],o
+ in
+*)
+ prerr_endline (NCicPp.ppobj obj)
+ | _ ->
+ prerr_endline ("NUOVA DISAMBIGUAZIONE AMBIGUO!!!!!!!!! "))
+ with
+ | MultiPassDisambiguator.DisambiguationError (_,s) ->
+ prerr_endline ("ERRORE NUOVA DISAMBIGUAZIONE ("
+ ^UriManager.string_of_uri uri^
+ "):\n" ^
+ String.concat "\n"
+ (List.map (fun _,_,x,_ -> snd (Lazy.force x)) (List.flatten s)))
+(* | exn -> prerr_endline (Printexc.to_string exn) *)
+ )
+ )
+ in
+*)
+
+
+ try
+(* let time = Unix.gettimeofday () in *)
+
+
+ let (diff, metasenv, _, cic, _) =
+ singleton "third"
+ (CicDisambiguate.disambiguate_obj
+ ~lookup_in_library
+ ~mk_choice:cic_mk_choice
+ ~mk_implicit
+ ~description_of_alias:LexiconAst.description_of_alias
+ ~aliases:estatus#lstatus.LexiconEngine.aliases
+ ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases)
+ ~uri:(Some uri)
+ (text,prefix_len,obj))
+ in
+
+
+(*
+ let time = Unix.gettimeofday () -. time in
+ prerr_endline ("VECCHIA DISAMBIGUAZIONE ("^
+ UriManager.string_of_uri uri ^"): " ^ string_of_float time);
+*)
+(* try_new (Some cic); *)
+
+
+ let estatus = LexiconEngine.set_proof_aliases estatus diff in
+ estatus, metasenv, cic
+
+ with
+ | Sys.Break as exn -> raise exn
+ | exn ->
+(* try_new None; *)
+ raise exn
+;;
+
+let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) =
+ let uri =
+ let baseuri =
+ match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
+ in
+ let name =
+ match obj with
+ | CicNotationPt.Inductive (_,(name,_,_,_)::_)
+ | CicNotationPt.Record (_,name,_,_) -> name ^ ".ind"
+ | CicNotationPt.Theorem (_,name,_,_) -> name ^ ".con"
+ | CicNotationPt.Inductive _ -> assert false
+ in
+ UriManager.uri_of_string (baseuri ^ "/" ^ name)
+ in
+ let diff, _, _, cic =
+ singleton "third"
+ (NCicDisambiguate.disambiguate_obj
+ ~lookup_in_library:nlookup_in_library
+ ~description_of_alias:LexiconAst.description_of_alias
+ ~mk_choice:ncic_mk_choice
+ ~mk_implicit
+ ~uri:(OCic2NCic.nuri_of_ouri uri)
+ ~rdb:estatus
+ ~aliases:estatus#lstatus.LexiconEngine.aliases
+ ~universe:(Some estatus#lstatus.LexiconEngine.multi_aliases)
+ (text,prefix_len,obj)) in
+ let estatus = LexiconEngine.set_proof_aliases estatus diff in
+ estatus, cic
+;;