and w2, _, (ty', left', right', _), m2 = eq2 in
match Pervasives.compare w1 w2 with
| 0 ->
- let res = (List.length m1) - (List.length m2) in
+ let res = (List.length m1) - (List.length m2) in
if res <> 0 then res else Pervasives.compare eq1 eq2
| res -> res
end
let minor eq =
let w, _, (ty, left, right, o), _ = eq in
match o with
- | Lt -> Some left
- | Le -> assert false
- | Gt -> Some right
- | Ge -> assert false
- | Eq
- | Incomparable -> None
-
+ | Lt -> Some left
+ | Le -> assert false
+ | Gt -> Some right
+ | Ge -> assert false
+ | Eq
+ | Incomparable -> None
+
let compare eq1 eq2 =
let w1, _, (ty, left, right, o1), m1 = eq1
and w2, _, (ty', left', right', o2), m2 = eq2 in
match Pervasives.compare w1 w2 with
| 0 ->
- (match minor eq1, minor eq2 with
- | Some t1, Some t2 ->
- fst (Utils.weight_of_term t1) - fst (Utils.weight_of_term t2)
- | Some _, None -> -1
- | None, Some _ -> 1
- | _,_ ->
- (List.length m2) - (List.length m1) )
- | res -> res
+ (match minor eq1, minor eq2 with
+ | Some t1, Some t2 ->
+ fst (Utils.weight_of_term t1) - fst (Utils.weight_of_term t2)
+ | Some _, None -> -1
+ | None, Some _ -> 1
+ | _,_ ->
+ (List.length m2) - (List.length m1) )
+ | res -> res
let compare eq1 eq2 =
match compare eq1 eq2 with
- 0 -> Pervasives.compare eq1 eq2
+ 0 -> Pervasives.compare eq1 eq2
| res -> res
end
*)
(match l with
[] -> raise Empty_list
| a::tl ->
- let wa = float_of_int (weight a) in
- let x = ref 0. in
- List.fold_left
- (fun (current,w) arg ->
- x:=!x +. 1.;
+ let wa = float_of_int (weight a) in
+ let x = ref 0. in
+ List.fold_left
+ (fun (current,w) arg ->
+ x:=!x +. 1.;
let w1 = weight arg in
let wa = (float_of_int w1) +. !x *. age_factor in
- if wa < w then (arg,wa) else (current,w))
- (a,wa) tl)
+ if wa < w then (arg,wa) else (current,w))
+ (a,wa) tl)
;;
(*
((tl, EqualitySet.remove hd neg_set), (pos, pos_set), passive_table)
| [], (hd:EqualitySet.elt)::tl ->
let passive_table =
- Indexing.remove_index passive_table hd
+ Indexing.remove_index passive_table hd
in (Positive, hd),
(([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table)
| _, _ -> assert false
let maxm, res =
Indexing.superposition_left !maxmeta env active_table current in
if Utils.debug_metas then
- ignore(List.map
- (function current ->
- Indexing.check_target c current "sup-1") res);
+ ignore(List.map
+ (function current ->
+ Indexing.check_target c current "sup-1") res);
maxmeta := maxm;
res, []
| Positive ->
let maxm, res =
Indexing.superposition_right !maxmeta env active_table current in
if Utils.debug_metas then
- ignore(List.map
- (function current ->
- Indexing.check_target c current "sup0") res);
+ ignore(List.map
+ (function current ->
+ Indexing.check_target c current "sup0") res);
maxmeta := maxm;
let rec infer_positive table = function
| [] -> [], []
let maxm, res =
Indexing.superposition_left !maxmeta env table equality in
maxmeta := maxm;
- if Utils.debug_metas then
- ignore(List.map
- (function current ->
- Indexing.check_target c current "supl") res);
+ if Utils.debug_metas then
+ ignore(List.map
+ (function current ->
+ Indexing.check_target c current "supl") res);
let neg, pos = infer_positive table tl in
res @ neg, pos
| (Positive, equality)::tl ->
let maxm, res =
Indexing.superposition_right !maxmeta env table equality in
maxmeta := maxm;
- if Utils.debug_metas then
- ignore
- (List.map
- (function current ->
- Indexing.check_target c current "sup2") res);
+ if Utils.debug_metas then
+ ignore
+ (List.map
+ (function current ->
+ Indexing.check_target c current "sup2") res);
let neg, pos = infer_positive table tl in
neg, res @ pos
in
maxmeta := maxm;
let curr_table = Indexing.index Indexing.empty current in
let neg, pos =
- infer_positive curr_table ((sign,copy_of_current)::active_list)
- in
- if Utils.debug_metas then
- ignore(List.map
- (function current ->
- Indexing.check_target c current "sup3") pos);
+ infer_positive curr_table ((sign,copy_of_current)::active_list)
+ in
+ if Utils.debug_metas then
+ ignore(List.map
+ (function current ->
+ Indexing.check_target c current "sup3") pos);
neg, res @ pos
in
derived_clauses := !derived_clauses + (List.length new_neg) +
match !maximal_retained_equality with
| None ->
if Utils.debug_metas then
- (ignore(List.map
- (function current ->
- Indexing.check_target c current "sup4") new_pos);
- ignore(List.map
- (function current ->
- Indexing.check_target c current "sup5") new_neg));
+ (ignore(List.map
+ (function current ->
+ Indexing.check_target c current "sup4") new_pos);
+ ignore(List.map
+ (function current ->
+ Indexing.check_target c current "sup5") new_neg));
new_neg, new_pos
| Some eq ->
ignore(assert false);
in
List.filter filterfun new_pos
in
- new_neg, new_pos
+ new_neg, new_pos
;;
if is_identity env newcurrent then
if sign = Negative then Some (sign, newcurrent)
else (
-(* debug_print *)
-(* (lazy *)
-(* (Printf.sprintf "\ncurrent was: %s\nnewcurrent is: %s\n" *)
-(* (string_of_equality current) *)
-(* (string_of_equality newcurrent))); *)
-(* debug_print *)
-(* (lazy *)
-(* (Printf.sprintf "active is: %s" *)
-(* (String.concat "\n" *)
-(* (List.map (fun (_, e) -> (string_of_equality e)) active_list)))); *)
- None
+(* debug_print *)
+(* (lazy *)
+(* (Printf.sprintf "\ncurrent was: %s\nnewcurrent is: %s\n" *)
+(* (string_of_equality current) *)
+(* (string_of_equality newcurrent))); *)
+(* debug_print *)
+(* (lazy *)
+(* (Printf.sprintf "active is: %s" *)
+(* (String.concat "\n" *)
+(* (List.map (fun (_, e) -> (string_of_equality e)) active_list)))); *)
+ None
)
else
Some (sign, newcurrent)
ignore (Indexing.check_target context current "demod0");
let res = demodulate active_table current in
if Utils.debug_metas then
- ignore ((function None -> () | Some (_,x) ->
- ignore (Indexing.check_target context x "demod1");()) res);
+ ignore ((function None -> () | Some (_,x) ->
+ ignore (Indexing.check_target context x "demod1");()) res);
match res with
| None -> None
| Some (sign, newcurrent) ->
match passive_table with
| None -> res
| Some passive_table ->
- match demodulate passive_table newcurrent with
- | None -> None
+ match demodulate passive_table newcurrent with
+ | None -> None
| Some (sign,newnewcurrent) ->
- if newcurrent <> newnewcurrent then
- demod newnewcurrent
- else Some (sign,newnewcurrent)
+ if newcurrent <> newnewcurrent then
+ demod newnewcurrent
+ else Some (sign,newnewcurrent)
in
let res = demod current in
match res with
else
match passive_table with
| None ->
- if fst (Indexing.subsumption env active_table c) then
- None
- else
- res
+ if fst (Indexing.subsumption env active_table c) then
+ None
+ else
+ res
| Some passive_table ->
if Indexing.in_index passive_table c then None
else
- let r1, _ = Indexing.subsumption env active_table c in
- if r1 then None else
- let r2, _ = Indexing.subsumption env passive_table c in
- if r2 then None else res
+ let r1, _ = Indexing.subsumption env active_table c in
+ if r1 then None else
+ let r2, _ = Indexing.subsumption env passive_table c in
+ if r2 then None else res
;;
type fs_time_info_t = {
if Utils.debug_metas then
begin
let m,c,u = env in
- ignore(List.map
- (fun current ->
- Indexing.check_target c current "forward new neg") new_neg);
- ignore(List.map
- (fun current -> Indexing.check_target c current "forward new pos")
+ ignore(List.map
+ (fun current ->
+ Indexing.check_target c current "forward new neg") new_neg);
+ ignore(List.map
+ (fun current -> Indexing.check_target c current "forward new pos")
new_pos;)
end;
let t1 = Unix.gettimeofday () in
List.fold_left
(fun (n,p) (s,c) ->
let neg,pos = infer env s c (new_pos,new_table) in
- neg@n,pos@p)
+ neg@n,pos@p)
([],[]) given
;;
let is_commutative_law eq =
let w, proof, (eq_ty, left, right, order), metas = snd eq in
match left,right with
- Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1],
- Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] ->
- f1 = f2 && a1 = b2 && a2 = b1
+ Cic.Appl[f1;Cic.Meta _ as a1;Cic.Meta _ as b1],
+ Cic.Appl[f2;Cic.Meta _ as a2;Cic.Meta _ as b2] ->
+ f1 = f2 && a1 = b2 && a2 = b1
| _ -> false
;;
| I.NoProof -> newproof
| I.BasicProof _ -> newproof
| I.SubProof (t, i, p) ->
- prerr_endline "SUBPROOF!";
- I.SubProof (t, i, repl p)
+ prerr_endline "SUBPROOF!";
+ I.SubProof (t, i, repl p)
| _ -> assert false
in
repl gproof
| ProofSymBlock (s, sp) ->
ProofSymBlock (s, gp sp)
| ProofBlock (s, u, nt, t, pe, sp) ->
- prerr_endline "apply_to_goal!";
+ prerr_endline "apply_to_goal!";
ProofBlock (s, u, nt, t, pe, gp sp)
in gp proof
in
let (sign, current), passive = select env (fst goals) passive active in
let names = List.map (HExtlib.map_option (fun (name,_) -> name)) context in
prerr_endline ("Selected = " ^
- (CicPp.pp (Inference.term_of_equality current) names));
+ (CicPp.pp (Inference.term_of_equality current) names));
let time1 = Unix.gettimeofday () in
let res = forward_simplify env (sign, current) ~passive active in
let time2 = Unix.gettimeofday () in
let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
match (fst goals) with
| (_, [proof, m, Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]])::_
- when left = right && iseq uri ->
- let p =
+ when left = right && iseq uri ->
+ let p =
Cic.Appl [Cic.MutConstruct (* reflexivity *)
- (LibraryObjects.eq_URI (), 0, 1, []);eq_ty; left]
- in
- let newp =
+ (LibraryObjects.eq_URI (), 0, 1, []);eq_ty; left]
+ in
+ let newp =
let rec repl = function
| Inference.ProofGoalBlock (_, gp) ->
Inference.ProofGoalBlock (Inference.BasicProof ([],p), gp)
in
repl proof
in true, Some newp
- | _ -> false, None
+ | (_, [proof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right]])::_->
+ (* here we check if the goal is subsumed by an active *)
+ let ok, subst =
+ (* the first m is unused *)
+ Indexing.subsumption (m,context,CicUniv.empty_ugraph)
+ (snd active)
+ (0,proof,(eq_ty,left,right,Eq),m)
+ in
+ if ok then
+ begin
+ prerr_endline "The goal is subsumed by an active";
+ false, None
+ end
+ else
+ ok, None
+ | _ -> false, None
in
if ok then
- (* let proof =
- match (fst goals) with
- | (_, [proof, m, _])::_ ->
- prerr_endline (CicMetaSubst.ppmetasenv [] m); Some proof
- | _ -> assert false
- in *)
( prerr_endline "esco qui";
let active =
- List.filter test (fst active) in
- let s = Printf.sprintf "actives:\n%s\n"
- (String.concat "\n"
+ List.filter test (fst active) in
+ let s = Printf.sprintf "actives:\n%s\n"
+ (String.concat "\n"
((List.map
- (fun (s, e) -> (string_of_sign s) ^ " " ^
+ (fun (s, e) -> (string_of_sign s) ^ " " ^
(string_of_equality ~env e))
- active)))
- in prerr_endline s;
+ active)))
+ in prerr_endline s;
let passive =
- List.filter
- (fun x -> test (1,x))
- (let x,y,_ = passive in (fst x)@(fst y)) in
- let p = Printf.sprintf "passives:\n%s\n"
- (String.concat "\n"
+ List.filter
+ (fun x -> test (1,x))
+ (let x,y,_ = passive in (fst x)@(fst y)) in
+ let p = Printf.sprintf "passives:\n%s\n"
+ (String.concat "\n"
((List.map
- (fun e ->
+ (fun e ->
(string_of_equality ~env e))
- passive)))
- in prerr_endline p;
+ passive)))
+ in prerr_endline p;
(*
- let s = Printf.sprintf "actives:\n%s\n"
- (String.concat "\n"
+ let s = Printf.sprintf "actives:\n%s\n"
+ (String.concat "\n"
((List.map
- (fun (s, e) -> (string_of_sign s) ^ " " ^
+ (fun (s, e) -> (string_of_sign s) ^ " " ^
(string_of_equality ~env e))
- (fst active)))) in
- let sp = Printf.sprintf "passives:\n%s\n"
- (String.concat "\n"
+ (fst active)))) in
+ let sp = Printf.sprintf "passives:\n%s\n"
+ (String.concat "\n"
(List.map
- (string_of_equality ~env)
- (let x,y,_ = passive in (fst x)@(fst y)))) in
- prerr_endline s;
- prerr_endline sp; *)
+ (string_of_equality ~env)
+ (let x,y,_ = passive in (fst x)@(fst y)))) in
+ prerr_endline s;
+ prerr_endline sp; *)
ParamodulationSuccess (proof, env))
else
given_clause_fullred_aux dbd env goals theorems passive active
and given_clause_fullred_aux dbd env goals theorems passive active =
prerr_endline (string_of_int !counter ^
- " MAXMETA: " ^ string_of_int !maxmeta ^
+ " MAXMETA: " ^ string_of_int !maxmeta ^
" LOCALMAX: " ^ string_of_int !Indexing.local_max ^
- " #ACTIVES: " ^ string_of_int (size_of_active active) ^
+ " #ACTIVES: " ^ string_of_int (size_of_active active) ^
" #PASSIVES: " ^ string_of_int (size_of_passive passive));
incr counter;
(* if !counter mod 10 = 0 then
let sizel = HExtlib.estimate_size (l1,l2) in
let sizes = HExtlib.estimate_size (s1,s2) in
- prerr_endline ("SIZE: " ^ string_of_int size);
- prerr_endline ("SIZE P: " ^ string_of_int sizep);
- prerr_endline ("SIZE A: " ^ string_of_int sizea);
+ prerr_endline ("SIZE: " ^ string_of_int size);
+ prerr_endline ("SIZE P: " ^ string_of_int sizep);
+ prerr_endline ("SIZE A: " ^ string_of_int sizea);
prerr_endline ("SIZE TBL: " ^ string_of_int sizetbl ^
- " SIZE L: " ^ string_of_int sizel ^
- " SIZE S:" ^ string_of_int sizes);
+ " SIZE L: " ^ string_of_int sizel ^
+ " SIZE S:" ^ string_of_int sizes);
end;*)
(*
if (size_of_active active) mod 50 = 0 then
| false ->
let (sign, current), passive = select env (fst goals) passive active in
prerr_endline
- ("Selected = " ^ (string_of_sign sign) ^ " " ^
- string_of_equality ~env current);
+ ("Selected = " ^ (string_of_sign sign) ^ " " ^
+ string_of_equality ~env current);
(* ^
- (let w,p,(t,l,r,o),m = current in
- " size w: " ^ string_of_int (HExtlib.estimate_size w)^
- " size p: " ^ string_of_int (HExtlib.estimate_size p)^
- " size t: " ^ string_of_int (HExtlib.estimate_size t)^
- " size l: " ^ string_of_int (HExtlib.estimate_size l)^
- " size r: " ^ string_of_int (HExtlib.estimate_size r)^
- " size o: " ^ string_of_int (HExtlib.estimate_size o)^
- " size m: " ^ string_of_int (HExtlib.estimate_size m)^
- " size m-c: " ^ string_of_int
- (HExtlib.estimate_size (List.map (fun (x,_,_) -> x) m)))) *)
+ (let w,p,(t,l,r,o),m = current in
+ " size w: " ^ string_of_int (HExtlib.estimate_size w)^
+ " size p: " ^ string_of_int (HExtlib.estimate_size p)^
+ " size t: " ^ string_of_int (HExtlib.estimate_size t)^
+ " size l: " ^ string_of_int (HExtlib.estimate_size l)^
+ " size r: " ^ string_of_int (HExtlib.estimate_size r)^
+ " size o: " ^ string_of_int (HExtlib.estimate_size o)^
+ " size m: " ^ string_of_int (HExtlib.estimate_size m)^
+ " size m-c: " ^ string_of_int
+ (HExtlib.estimate_size (List.map (fun (x,_,_) -> x) m)))) *)
let time1 = Unix.gettimeofday () in
let res = forward_simplify env (sign, current) ~passive active in
let time2 = Unix.gettimeofday () in
given_clause_fullred dbd env goals theorems passive active
| Some (sign, current) ->
if test (sign, current) then
- (prerr_endline
- ("Simplified = " ^ (string_of_sign sign) ^ " " ^
- string_of_equality ~env current);
- let active = fst active in
- let s = Printf.sprintf "actives:\n%s\n"
- (String.concat "\n"
+ (prerr_endline
+ ("Simplified = " ^ (string_of_sign sign) ^ " " ^
+ string_of_equality ~env current);
+ let active = fst active in
+ let s = Printf.sprintf "actives:\n%s\n"
+ (String.concat "\n"
((List.map
- (fun (s, e) -> (string_of_sign s) ^ " " ^
+ (fun (s, e) -> (string_of_sign s) ^ " " ^
(string_of_equality ~env e))
- active)))
- in prerr_endline s;
+ active)))
+ in prerr_endline s;
assert false);
if (sign = Negative) && (is_identity env current) then (
debug_print
let t1 = Unix.gettimeofday () in
let new' = infer env sign current active in
- let _ =
+ let _ =
match new' with
| neg, pos ->
debug_print
| Some (n, p), None
| None, Some (n, p) ->
let nn, np = new' in
- if Utils.debug_metas then
- begin
- List.iter
- (fun x->Indexing.check_target context x "simplify1")
- n;
- List.iter
- (fun x->Indexing.check_target context x "simplify2")
- p
- end;
+ if Utils.debug_metas then
+ begin
+ List.iter
+ (fun x->Indexing.check_target context x "simplify1")
+ n;
+ List.iter
+ (fun x->Indexing.check_target context x "simplify2")
+ p
+ end;
simplify (nn @ n, np @ p) active passive
| Some (n, p), Some (rn, rp) ->
let nn, np = new' in
in
let active, _, new' = simplify new' active passive in
(* pessima prova
- let new1 = prova env new' active in
+ let new1 = prova env new' active in
let new' = (fst new') @ (fst new1), (snd new') @ (snd new1) in
let _ =
match new1 with
| ParamodulationSuccess (None, env) ->
Printf.printf "Success, but no proof?!?\n\n"
in
- if Utils.time then
- begin
- prerr_endline
- ((Printf.sprintf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
+ if Utils.time then
+ begin
+ prerr_endline
+ ((Printf.sprintf ("infer_time: %.9f\nforward_simpl_time: %.9f\n" ^^
"forward_simpl_new_time: %.9f\n" ^^
"backward_simpl_time: %.9f\n")
!infer_time !forward_simpl_time !forward_simpl_new_time
!backward_simpl_time) ^
- (Printf.sprintf "beta_expand_time: %.9f\n"
- !Indexing.beta_expand_time) ^
- (Printf.sprintf "passive_maintainance_time: %.9f\n"
- !passive_maintainance_time) ^
- (Printf.sprintf " successful unification/matching time: %.9f\n"
- !Indexing.match_unif_time_ok) ^
- (Printf.sprintf " failed unification/matching time: %.9f\n"
- !Indexing.match_unif_time_no) ^
- (Printf.sprintf " indexing retrieval time: %.9f\n"
- !Indexing.indexing_retrieval_time) ^
- (Printf.sprintf " demodulate_term.build_newtarget_time: %.9f\n"
- !Indexing.build_newtarget_time) ^
- (Printf.sprintf "derived %d clauses, kept %d clauses.\n"
- !derived_clauses !kept_clauses))
- end
+ (Printf.sprintf "beta_expand_time: %.9f\n"
+ !Indexing.beta_expand_time) ^
+ (Printf.sprintf "passive_maintainance_time: %.9f\n"
+ !passive_maintainance_time) ^
+ (Printf.sprintf " successful unification/matching time: %.9f\n"
+ !Indexing.match_unif_time_ok) ^
+ (Printf.sprintf " failed unification/matching time: %.9f\n"
+ !Indexing.match_unif_time_no) ^
+ (Printf.sprintf " indexing retrieval time: %.9f\n"
+ !Indexing.indexing_retrieval_time) ^
+ (Printf.sprintf " demodulate_term.build_newtarget_time: %.9f\n"
+ !Indexing.build_newtarget_time) ^
+ (Printf.sprintf "derived %d clauses, kept %d clauses.\n"
+ !derived_clauses !kept_clauses))
+ end
(*
with exc ->
print_endline ("EXCEPTION: " ^ (Printexc.to_string exc));
debug_print (lazy "OK, found a proof!");
let proof = Inference.build_proof_term proof in
(* prerr_endline (CicPp.ppterm proof); *)
- let metasenv = (2839,context,Cic.Rel 17)::(214882,context,Cic.Rel 17)::metasenv in
let names = names_of_context context in
let newmetasenv =
let i1 =
let tdemodulate = fs_time_info.demodulate in
let tsubsumption = fs_time_info.subsumption in
if Utils.time then
- begin
- prerr_endline (
- (Printf.sprintf "\nTIME NEEDED: %.9f" time) ^
- (Printf.sprintf "\ntall: %.9f" tall) ^
- (Printf.sprintf "\ntdemod: %.9f" tdemodulate) ^
- (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption) ^
- (Printf.sprintf "\ninfer_time: %.9f" !infer_time) ^
- (Printf.sprintf "\nbeta_expand_time: %.9f\n"
- !Indexing.beta_expand_time) ^
- (Printf.sprintf "\nmetas_of_proof: %.9f\n"
- !Inference.metas_of_proof_time) ^
- (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time) ^
- (Printf.sprintf "\nforward_simpl_new_times: %.9f"
- !forward_simpl_new_time) ^
- (Printf.sprintf "\nbackward_simpl_times: %.9f" !backward_simpl_time) ^
- (Printf.sprintf "\npassive_maintainance_time: %.9f"
- !passive_maintainance_time))
- end;
+ begin
+ prerr_endline (
+ (Printf.sprintf "\nTIME NEEDED: %.9f" time) ^
+ (Printf.sprintf "\ntall: %.9f" tall) ^
+ (Printf.sprintf "\ntdemod: %.9f" tdemodulate) ^
+ (Printf.sprintf "\ntsubsumption: %.9f" tsubsumption) ^
+ (Printf.sprintf "\ninfer_time: %.9f" !infer_time) ^
+ (Printf.sprintf "\nbeta_expand_time: %.9f\n"
+ !Indexing.beta_expand_time) ^
+ (Printf.sprintf "\nmetas_of_proof: %.9f\n"
+ !Inference.metas_of_proof_time) ^
+ (Printf.sprintf "\nforward_simpl_times: %.9f" !forward_simpl_time) ^
+ (Printf.sprintf "\nforward_simpl_new_times: %.9f"
+ !forward_simpl_new_time) ^
+ (Printf.sprintf "\nbackward_simpl_times: %.9f" !backward_simpl_time) ^
+ (Printf.sprintf "\npassive_maintainance_time: %.9f"
+ !passive_maintainance_time))
+ end;
newstatus
| _ ->
raise (ProofEngineTypes.Fail (lazy "NO proof found"))
debug_print
(lazy
(Printf.sprintf "\n\nequalities:\n%s\n"
- (String.concat "\n"
+ (String.concat "\n"
(List.map
- (fun (u, e) ->
-(* Printf.sprintf "%s: %s" *)
- (UriManager.string_of_uri u)
-(* (string_of_equality e) *)
- )
- equalities))));
+ (fun (u, e) ->
+(* Printf.sprintf "%s: %s" *)
+ (UriManager.string_of_uri u)
+(* (string_of_equality e) *)
+ )
+ equalities))));
debug_print (lazy "RETR: SIMPLYFYING EQUALITIES...");
let rec simpl e others others_simpl =
let (u, e) = e in
let res = forward_simplify env (Positive, e) (active, tbl) in
match others with
| hd::tl -> (
- match res with
- | None -> simpl hd tl others_simpl
- | Some e -> simpl hd tl ((u, (snd e))::others_simpl)
- )
+ match res with
+ | None -> simpl hd tl others_simpl
+ | Some e -> simpl hd tl ((u, (snd e))::others_simpl)
+ )
| [] -> (
- match res with
- | None -> others_simpl
- | Some e -> (u, (snd e))::others_simpl
- )
+ match res with
+ | None -> others_simpl
+ | Some e -> (u, (snd e))::others_simpl
+ )
in
let _equalities =
match equalities with
| [] -> []
| hd::tl ->
- let others = tl in (* List.map (fun e -> (Positive, e)) tl in *)
- let res =
- List.rev (simpl (*(Positive,*) hd others [])
- in
- 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)
- (string_of_equality e)
- )
- res))));
- res in
+ let others = tl in (* List.map (fun e -> (Positive, e)) tl in *)
+ let res =
+ List.rev (simpl (*(Positive,*) hd others [])
+ in
+ 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)
+ (string_of_equality e)
+ )
+ res))));
+ res in
debug_print
(lazy
(Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)))
begin
let opengoal = Cic.Meta(maxm,irl) in
let proofterm =
- Inference.build_proof_term ~noproof:opengoal newproof in
+ Inference.build_proof_term ~noproof:opengoal newproof in
let extended_metasenv = (maxm,context,newty)::metasenv in
- let extended_status =
- (curi,extended_metasenv,pbo,pty),goal in
- let (status,newgoals) =
- ProofEngineTypes.apply_tactic
- (PrimitiveTactics.apply_tac ~term:proofterm)
- extended_status in
- (status,maxm::newgoals)
+ let extended_status =
+ (curi,extended_metasenv,pbo,pty),goal in
+ let (status,newgoals) =
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.apply_tac ~term:proofterm)
+ extended_status in
+ (status,maxm::newgoals)
end
else if newty = ty then
raise (ProofEngineTypes.Fail (lazy "no progress"))
projects / helm.git / commitdiff