+let saturation_tactic status =
+ let module C = Cic in
+ let saturation_tac (proof, goal) =
+ maxmeta := 0;
+(* if List.length goals <> 1 then *)
+(* raise (ProofEngineTypes.Fail "There should be only one open goal"); *)
+
+(* let goal' = List.hd goals in *)
+ let goal' = goal in
+ let uri, metasenv, meta_proof, term_to_prove = proof in
+ let _, context, goal = CicUtil.lookup_meta goal' metasenv in
+ let equalities, maxm = find_equalities context proof in
+ maxmeta := maxm+2;
+ let new_meta_goal, metasenv, type_of_goal =
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context in
+ let _, context, ty = CicUtil.lookup_meta goal' metasenv in
+ Printf.printf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty);
+ print_newline ();
+ Cic.Meta (maxm+1, irl),
+ (maxm+1, context, ty)::metasenv,
+ ty
+ in
+ let ugraph = CicUniv.empty_ugraph in
+ let env = (metasenv, context, ugraph) in
+ try
+ let term_equality = equality_of_term new_meta_goal goal in
+(* let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in *)
+ let active = make_active () in
+ let passive = make_passive [term_equality] equalities in
+ let res = given_clause_fullred env passive active in
+ match res with
+ | Success (Some goal, env) ->
+ Printf.printf "OK, found a proof!\n";
+ let proof = Inference.build_proof_term goal in
+ let names = names_of_context context in
+ print_endline (CicPp.pp proof names);
+ let newmetasenv =
+ let i1 =
+ match new_meta_goal with
+ | C.Meta (i, _) -> i | _ -> assert false
+ in
+ let i2 =
+ match meta_proof with
+ | C.Meta (i, _) -> i | _ -> assert false
+ in
+ List.filter (fun (i, _, _) -> i <> i1 && i <> i2) metasenv
+ in
+ let newstatus =
+ try
+ let ty, ug =
+ CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
+ in
+ Printf.printf
+ "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n"
+ (CicPp.pp type_of_goal names) (CicPp.pp ty names)
+ (string_of_bool
+ (fst (CicReduction.are_convertible
+ context type_of_goal ty ug)));
+ ((uri, newmetasenv, proof, term_to_prove), [])
+ with e ->
+ raise (ProofEngineTypes.Fail
+ "Found a proof, but it doesn't typecheck")
+ in
+ newstatus
+ | _ ->
+ raise (ProofEngineTypes.Fail "NO proof found")
+ with e ->
+ raise (ProofEngineTypes.Fail "saturation failed")
+ in
+ ProofEngineTypes.mk_tactic saturation_tac
+;;
+
+
+
+let configuration_file = ref "../../matita/matita.conf.xml";;