+let retrieve_and_print dbd term metasenv ugraph =
+ let module C = Cic in
+ let module T = CicTypeChecker in
+ let module PET = ProofEngineTypes in
+ let module PP = CicPp in
+ let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
+ let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
+ let proof, goals = status in
+ let goal' = List.nth goals 0 in
+ let uri, metasenv, meta_proof, term_to_prove = proof in
+ let _, context, type_of_goal = CicUtil.lookup_meta goal' metasenv in
+ let eq_uri = eq_of_goal type_of_goal in
+ let bag = Equality.mk_equality_bag () in
+ let eq_indexes, equalities, maxm,cache =
+ Equality_retrieval.find_context_equalities 0 bag None context proof AutoCache.cache_empty in
+ let ugraph = CicUniv.empty_ugraph in
+ let env = (metasenv, context, ugraph) in
+ let t1 = Unix.gettimeofday () in
+ let lib_eq_uris, library_equalities, maxm, cache =
+ Equality_retrieval.find_library_equalities bag None
+ false dbd context (proof, goal') (maxm+2) cache
+ in
+ let t2 = Unix.gettimeofday () in
+ maxmeta := maxm+2;
+ let equalities = (* equalities @ *) library_equalities in
+ Utils.debug_print
+ (lazy
+ (Printf.sprintf "\n\nequalities:\n%s\n"
+ (String.concat "\n"
+ (List.map
+ (fun (u, e) ->
+(* Printf.sprintf "%s: %s" *)
+ (UriManager.string_of_uri u)
+(* (string_of_equality e) *)
+ )
+ equalities))));
+ Utils.debug_print (lazy "RETR: SIMPLYFYING EQUALITIES...");
+ let rec simpl e others others_simpl =
+ let (u, e) = e in
+ let active = (others @ others_simpl) in
+ let tbl =
+ List.fold_left
+ (fun t (_, e) -> Indexing.index t e)
+ Indexing.empty active
+ in
+ let res = forward_simplify bag eq_uri env e (active, tbl) in
+ match others with
+ | hd::tl -> (
+ match res with
+ | None -> simpl hd tl others_simpl
+ | Some e -> simpl hd tl ((u, e)::others_simpl)
+ )
+ | [] -> (
+ match res with
+ | None -> others_simpl
+ | Some e -> (u, e)::others_simpl
+ )
+ in
+ let _equalities =
+ match equalities with
+ | [] -> []
+ | hd::tl ->
+ let others = tl in (* List.map (fun e -> (Utils.Positive, e)) tl in *)
+ let res =
+ List.rev (simpl (*(Positive,*) hd others [])
+ in
+ Utils.debug_print
+ (lazy
+ (Printf.sprintf "\nequalities AFTER:\n%s\n"
+ (String.concat "\n"
+ (List.map
+ (fun (u, e) ->
+ Printf.sprintf "%s: %s"
+ (UriManager.string_of_uri u)
+ (Equality.string_of_equality e)
+ )
+ res))));
+ res in
+ Utils.debug_print
+ (lazy
+ (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)))
+;;
+
+
+let main_demod_equalities dbd term metasenv ugraph =
+ let module C = Cic in
+ let module T = CicTypeChecker in
+ let module PET = ProofEngineTypes in
+ let module PP = CicPp in
+ let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
+ let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
+ let proof, goals = status in
+ let goal' = List.nth goals 0 in
+ let _, metasenv, meta_proof, _ = proof in
+ let _, context, goal = CicUtil.lookup_meta goal' metasenv in
+ let eq_uri = eq_of_goal goal in
+ let bag = Equality.mk_equality_bag () in
+ let eq_indexes, equalities, maxm, cache =
+ Equality_retrieval.find_context_equalities 0 bag None context proof AutoCache.cache_empty in
+ let lib_eq_uris, library_equalities, maxm,cache =
+ Equality_retrieval.find_library_equalities bag None
+ false dbd context (proof, goal') (maxm+2) cache
+ in
+ let library_equalities = List.map snd library_equalities in
+ maxmeta := maxm+2; (* TODO ugly!! *)
+ let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
+ let new_meta_goal, metasenv, type_of_goal =
+ let _, context, ty = CicUtil.lookup_meta goal' metasenv in
+ Utils.debug_print
+ (lazy
+ (Printf.sprintf "\n\nTRYING TO INFER EQUALITIES MATCHING: %s\n\n"
+ (CicPp.ppterm ty)));
+ Cic.Meta (maxm+1, irl),
+ (maxm+1, context, ty)::metasenv,
+ ty
+ in
+ let env = (metasenv, context, ugraph) in
+ (*try*)
+ let goal = [], [], goal
+ in
+ let equalities =
+ simplify_equalities bag eq_uri env (equalities@library_equalities)
+ in
+ let active = make_empty_active () in
+ let passive = make_passive equalities in
+ Printf.eprintf "\ncontext:\n%s\n" (PP.ppcontext context);
+ Printf.eprintf "\nmetasenv:\n%s\n" (Utils.print_metasenv metasenv);
+ Printf.eprintf "\nequalities:\n%s\n"
+ (String.concat "\n"
+ (List.map
+ (Equality.string_of_equality ~env) equalities));
+ prerr_endline "--------------------------------------------------";
+ prerr_endline "GO!";
+ start_time := Unix.gettimeofday ();
+ if !time_limit < 1. then time_limit := 60.;
+ let ra, rp =
+ saturate_equations bag eq_uri env goal (fun e -> true) passive active
+ in
+
+ let initial =
+ List.fold_left (fun s e -> EqualitySet.add e s)
+ EqualitySet.empty equalities
+ in
+ let addfun s e =
+ if not (EqualitySet.mem e initial) then EqualitySet.add e s else s
+ in
+
+ let passive =
+ match rp with
+ | p, _ ->
+ EqualitySet.elements (List.fold_left addfun EqualitySet.empty p)
+ in
+ let active =
+ let l = fst ra in
+ EqualitySet.elements (List.fold_left addfun EqualitySet.empty l)
+ in
+ Printf.eprintf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n"
+ (String.concat "\n" (List.map (Equality.string_of_equality ~env) active))
+ (* (String.concat "\n"
+ (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active)) *)
+(* (String.concat "\n" (List.map (string_of_equality ~env) passive)); *)
+ (String.concat "\n"
+ (List.map
+ (fun e -> CicPp.ppterm (Equality.term_of_equality eq_uri e))
+ passive));
+ print_newline ();
+(*
+ with e ->
+ Utils.debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e)))
+*)
+;;
+let saturate_equations eq_uri env goal accept_fun passive active =
+ let bag = Equality.mk_equality_bag () in
+ saturate_equations bag eq_uri env goal accept_fun passive active
+;;
+
+let add_to_passive eql passives =
+ add_to_passive passives eql eql
+;;