| None -> raise BaseUriNotSetYet)
| CicNotationPt.Inductive _ -> assert false
| CicNotationPt.Theorem _ -> None in
- (*
- (match obj with
+ 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:lexicon_status.LexiconEngine.aliases
+ ~universe:(Some lexicon_status.LexiconEngine.multi_aliases) ~uri
+ (text,prefix_len,obj)) in
+
+ let time = Unix.gettimeofday () -. time in
+ prerr_endline ("VECCHIA DISAMBIGUAZIONE: " ^ string_of_float time);
+ (NCicLibrary.clear_cache ();
+ NCicEnvironment.invalidate ();
+ OCic2NCic.clear ();
+ prerr_endline "INIZIO NUOVA DISAMBIGUAZIONE";
+ (match obj with
CicNotationPt.Theorem (_,_,ty,_) ->
+ let graph =
+ match cic with
+ | Cic.CurrentProof (_,metasenv, _, ty,_,_) ->
+ let _, ugraph =
+ CicTypeChecker.type_of_aux' metasenv [] ty CicUniv.empty_ugraph
+ in
+ ugraph
+ | Cic.Constant (_,_, ty,_,_) ->
+ let _, ugraph =
+ CicTypeChecker.type_of_aux' [] [] ty CicUniv.empty_ugraph
+ in
+ ugraph
+ | _ -> CicUniv.empty_ugraph
+ in
+(*
+ 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 ())
+ in
+ ignore(CicUniv.do_rank graph);
+ let time = Unix.gettimeofday () in
(try
(match
NCicDisambiguate.disambiguate_term
~description_of_alias:LexiconAst.description_of_alias
~mk_choice:ncic_mk_choice
~mk_implicit
+ ~coercion_db:(NCicCoercion.db ())
~context:[] ~metasenv:[] ~subst:[]
- ~aliases:lexicon_status.LexiconEngine.aliases
- ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
+ ~aliases:lexicon_status.LexiconEngine.aliases
+ ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
(text,prefix_len,ty)
with
| [_,metasenv,subst,ty],_ ->
- prerr_endline ("NUOVA DISAMBIGUAZIONE OK!!!!!!!!! " ^
- NCicPp.ppterm ~metasenv ~subst ~context:[] ty)
+ let time = Unix.gettimeofday () -. time in
+ prerr_endline ("NUOVA DISAMBIGUAZIONE OK: "^ string_of_float time);
+ prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context:[] ty)
| _ ->
prerr_endline ("NUOVA DISAMBIGUAZIONE AMBIGUO!!!!!!!!! "))
with
(List.map (fun _,_,x,_ -> snd (Lazy.force x)) (List.flatten s)))
(* | exn -> prerr_endline (Printexc.to_string exn) *)
)
- | _ -> ()
+ | _ -> ())
);
- *)
- 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: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