| ParamodulationFailure ->
Printf.printf "NO proof found! :-(\n\n"
| ParamodulationSuccess (Some goal, env) ->
- let proof = Inference.build_proof_term goal in
+ let proof = Inference.build_proof_term goal in
+(* let proof = *)
+(* (\* let p = CicSubstitution.lift 1 proof in *\) *)
+(* let rec repl i = function *)
+(* | C.Meta _ -> C.Rel i *)
+(* | C.Appl l -> C.Appl (List.map (repl i) l) *)
+(* | C.Prod (n, s, t) -> C.Prod (n, s, repl (i+1) t) *)
+(* | C.Lambda (n, s, t) -> C.Lambda (n, s, repl (i+1) t) *)
+(* | t -> t *)
+(* in *)
+(* let p = repl 1 proof in *)
+(* p *)
+(* (\* C.Lambda (C.Anonymous, C.Rel 9, p) *\) *)
+(* in *)
let newmetasenv =
List.fold_left
(fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities
in
let _ =
+ Printf.printf "OK, found a proof!\n";
+ (* REMEMBER: we have to instantiate meta_proof, we should use
+ apply the "apply" tactic to proof and status
+ *)
+ let names = names_of_context context in
+ print_endline (PP.pp proof names);
try
let ty, ug =
CicTypeChecker.type_of_aux' newmetasenv context proof ugraph
in
- Printf.printf "OK, found a proof!\n";
- (* REMEMBER: we have to instantiate meta_proof, we should use
- apply the "apply" tactic to proof and status
- *)
- let names = names_of_context context in
- print_endline (PP.pp proof names);
+(* Printf.printf "OK, found a proof!\n"; *)
+(* (\* REMEMBER: we have to instantiate meta_proof, we should use *)
+(* apply the "apply" tactic to proof and status *)
+(* *\) *)
+(* let names = names_of_context context in *)
+(* print_endline (PP.pp proof names); *)
(* print_endline (PP.ppterm proof); *)
print_endline (string_of_float (finish -. start));