-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 eq_indexes, equalities, maxm = Inference.find_equalities context proof in
- let lib_eq_uris, library_equalities, maxm =
- Inference.find_library_equalities false dbd context (proof, goal') (maxm+2)
- 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 eq_uri env (equalities@library_equalities)
- in
- let active = make_active () in
- let passive = make_passive equalities in
- Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
- Printf.printf "\nmetasenv:\n%s\n" (Utils.print_metasenv metasenv);
- Printf.printf "\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 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