+ 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
+ debug_print (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty));
+ 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 active = make_active () in
+ let passive =
+ make_passive [term_equality] (equalities @ library_equalities)
+ in
+ let res = given_clause_fullred env passive active in
+ match res with
+ | ParamodulationSuccess (Some goal, env) ->
+ debug_print "OK, found a proof!";
+ let proof = Inference.build_proof_term goal in
+ let names = names_of_context context in
+ 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 *)
+(* | t -> *)
+(* Printf.printf "\nHMMM!!! meta_proof: %s\ngoal': %s" *)
+(* (CicPp.pp meta_proof names) (string_of_int goal'); *)
+(* print_newline (); *)
+(* assert false *)
+(* in *)
+ List.filter (fun (i, _, _) -> i <> i1 && i <> goal') metasenv
+ in
+ let newstatus =
+ try
+ let ty, ug =
+ CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
+ in
+ debug_print (CicPp.pp proof [](* names *));
+ debug_print
+ (Printf.sprintf
+ "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n"
+ (CicPp.pp type_of_goal names) (CicPp.pp ty names)
+ (string_of_bool
+ (fst (CicReduction.are_convertible
+ context type_of_goal ty ug))));
+ let equality_for_replace i t1 =
+ match t1 with
+ | C.Meta (n, _) -> n = i
+ | _ -> false
+ in
+ let real_proof =
+ ProofEngineReduction.replace
+ ~equality:equality_for_replace
+ ~what:[goal'] ~with_what:[proof]
+ ~where:meta_proof
+ in
+ debug_print (
+ Printf.sprintf "status:\n%s\n%s\n%s\n%s\n"
+ (match uri with Some uri -> UriManager.string_of_uri uri
+ | None -> "")
+ (print_metasenv newmetasenv)
+ (CicPp.pp real_proof [](* names *))
+ (CicPp.pp term_to_prove names));
+ ((uri, newmetasenv, real_proof, term_to_prove), [])
+ with CicTypeChecker.TypeCheckerFailure _ ->
+ debug_print "THE PROOF DOESN'T TYPECHECK!!!";
+ debug_print (CicPp.pp proof names);
+ raise
+ (ProofEngineTypes.Fail "Found a proof, but it doesn't typecheck")
+ in
+ newstatus
+ | _ ->
+ raise (ProofEngineTypes.Fail "NO proof found")
+(* with e -> *)
+(* raise (Failure "saturation failed") *)
+;;