| None -> raise BaseUriNotSetYet)
| CicNotationPt.Inductive _ -> assert false
| CicNotationPt.Theorem _ -> None in
- 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);
+ let try_new cic =
(NCicLibrary.clear_cache ();
NCicEnvironment.invalidate ();
OCic2NCic.clear ();
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) ->
graph (CoercDb.to_list ())
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
(* | 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: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);
+ try_new cic;
+*)
+
+
+
let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
lexicon_status, metasenv, cic
+
+
+(*
+ with
+ | Sys.Break as exn -> raise exn
+ | exn ->
+ try_new (Cic.InductiveDefinition ([],[],0,[]));
+ raise exn
+*)
+
+
+;;
let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
match cmd with
disambiguate_term None text prefix_len lexicon_status_ref [] in
let metasenv,t = disambiguate_term metasenv t in
!lexicon_status_ref, metasenv, GrafiteAst.Coercion (loc,t,b,a,s)
+ | GrafiteAst.UnificationHint (loc, t) ->
+ let lexicon_status_ref = ref lexicon_status in
+ let disambiguate_term =
+ disambiguate_term None text prefix_len lexicon_status_ref [] in
+ let metasenv,t = disambiguate_term metasenv t in
+ !lexicon_status_ref, metasenv, GrafiteAst.UnificationHint (loc,t)
| GrafiteAst.Default _
| GrafiteAst.Drop _
| GrafiteAst.Include _