| Some (t, s, m, u, ((p,e), eq_URI)) ->
Printf.sprintf "Some: (%s, %s, %s)"
(Utils.string_of_pos p)
- (Inference.string_of_equality ?env e)
+ (Equality.string_of_equality ?env e)
(CicPp.ppterm t)
;;
(List.map
(fun (p, e) ->
Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
- (Inference.string_of_equality ?env e))
+ (Equality.string_of_equality ?env e))
res));
;;
let indexing_retrieval_time = ref 0.;;
-let apply_subst = Inference.apply_subst
+let apply_subst = Equality.apply_subst
let index = Index.index
let remove_index = Index.remove_index
let check_disjoint_invariant subst metasenv msg =
if (List.exists
- (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv)
+ (fun (i,_,_) -> (Equality.is_in_subst i subst)) metasenv)
then
begin
prerr_endline ("not disjoint: " ^ msg);
let check_res res msg =
match res with
Some (t, subst, menv, ug, (eq_found, eq_URI)) ->
- let eqs = Inference.string_of_equality (snd eq_found) in
+ let eqs = Equality.string_of_equality (snd eq_found) in
check_disjoint_invariant subst menv msg;
check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
| None -> ()
;;
let check_target context target msg =
- let w, proof, (eq_ty, left, right, order), metas = target in
+ let w, proof, (eq_ty, left, right, order), metas,_ =
+ Equality.open_equality target in
(* check that metas does not contains duplicates *)
- let eqs = Inference.string_of_equality target in
+ let eqs = Equality.string_of_equality target in
let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
- let actual = (Inference.metas_of_term left)@(Inference.metas_of_term right)
- @(Inference.metas_of_term eq_ty)@(Inference.metas_of_proof proof) in
+ let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right)
+ @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof proof) in
let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
let _ = if menv <> metas then
begin
the position will always be Left, and if the ordering is left < right,
position will be Right.
*)
-let local_max = ref 100;;
-
-let make_variant (p,eq) =
- let maxmeta, eq = Inference.fix_metas !local_max eq in
- local_max := maxmeta;
- p, eq
-;;
let get_candidates ?env mode tree term =
let t1 = Unix.gettimeofday () in
function
| [] -> None
| candidate::tl ->
- let pos, (_, proof, (ty, left, right, o), metas) = candidate in
+ let pos, equality = candidate in
+ let (_, proof, (ty, left, right, o), metas,_) =
+ Equality.open_equality equality in
if Utils.debug_metas then
ignore(check_target context (snd candidate) "find_matches");
if Utils.debug_res then
begin
- let c = "eq = " ^ (Inference.string_of_equality (snd candidate)) ^ "\n"in
- let t = "t = " ^ (CicPp.ppterm term) ^ "\n" in
- let m = "metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
- let p = "proof = " ^ (CicPp.ppterm (Inference.build_proof_term proof)) ^ "\n" in
+ let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
+ let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
+ let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
+ let p="proof = "^
+ (CicPp.ppterm(Equality.build_proof_term_old (snd proof)))^"\n"
+ in
check_for_duplicates metas "gia nella metas";
- check_for_duplicates (metasenv @ metas) ("not disjoint" ^ c ^ t ^ m ^ p)
+ check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^p)
end;
if check && not (fst (CicReduction.are_convertible
~metasenv context termty ty ugraph)) then (
function
| [] -> []
| candidate::tl ->
- let pos, (_, _, (ty, left, right, o), metas) = candidate in
+ let pos, equality = candidate in
+ let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
let do_match c eq_URI =
let subst', metasenv', ugraph' =
let t1 = Unix.gettimeofday () in
(*
returns true if target is subsumed by some equality in table
*)
-let subsumption env table target =
- let _, _, (ty, left, right, _), tmetas = target in
+let subsumption env table target =
+ (*
+ let print_res l =
+ prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
+ ((pos,equation),_)) -> Inference.string_of_equality equation)l))
+ in
+ *)
+ let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
let metasenv, context, ugraph = env in
let metasenv = tmetas in
- let merge_if_possible s1 s2 =
- let already_in = Hashtbl.create 13 in
- let rec aux acc = function
- | ((i,x) as s)::tl ->
- (try
- let x' = Hashtbl.find already_in i in
- if x = x' then aux acc tl else None
- with
- | Not_found ->
- Hashtbl.add already_in i x;
- aux (s::acc) tl)
- | [] -> Some acc
- in
- aux [] (s1@s2)
- in
let leftr =
match left with
| Cic.Meta _ -> []
find_all_matches ~unif_fun:Inference.matching
metasenv context ugraph 0 left ty leftc
in
+(* print_res leftr;*)
let rec ok what = function
- | [] -> false, []
- | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m)), _))::tl ->
+ | [] -> None
+ | (_, subst, menv, ug, ((pos,equation),_))::tl ->
+ let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
try
let other = if pos = Utils.Left then r else l in
let subst', menv', ug' =
let t1 = Unix.gettimeofday () in
try
let r =
- Inference.matching metasenv menv context what other ugraph
+ Inference.matching metasenv m context what other ugraph
in
let t2 = Unix.gettimeofday () in
match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
raise e
in
- (match merge_if_possible subst subst' with
+ (match Equality.merge_subst_if_possible subst subst' with
| None -> ok what tl
- | Some s -> true, s)
+ | Some s -> Some (s, equation))
with Inference.MatchingFailure ->
ok what tl
in
- let r, subst = ok right leftr in
- let r, s =
- if r then
- true, subst
- else
+ match ok right leftr with
+ | Some _ as res -> res
+ | None ->
let rightr =
match right with
| Cic.Meta _ -> []
find_all_matches ~unif_fun:Inference.matching
metasenv context ugraph 0 right ty rightc
in
+(* print_res rightr;*)
ok left rightr
- in
(* (if r then *)
(* debug_print *)
(* (lazy *)
(* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
(* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
- r, s
;;
let rec demodulation_aux ?from ?(typecheck=false)
if List.exists (fun (i,_,_) -> i = 2840) metasenv
then
(prerr_endline ("term: " ^(CicPp.ppterm term));
- List.iter (fun (_,x) -> prerr_endline (Inference.string_of_equality x))
+ List.iter (fun (_,x) -> prerr_endline (Equality.string_of_equality x))
candidates;
prerr_endline ("-------");
prerr_endline ("+++++++"));
-(* let candidates = List.map make_variant candidates in *)
let res =
match term with
| C.Meta _ -> None
let module HL = HelmLibraryObjects in
let module U = Utils in
let metasenv, context, ugraph = env in
- let w, proof, (eq_ty, left, right, order), metas = target in
+ let w, ((proof_new, proof_old) as proof),
+ (eq_ty, left, right, order), metas, id =
+ Equality.open_equality target in
(* first, we simplify *)
let right = U.guarded_simpl context right in
let left = U.guarded_simpl context left in
let order = !Utils.compare_terms left right in
let stat = (eq_ty, left, right, order) in
let w = Utils.compute_equality_weight stat in
- let target = w, proof, stat, metas in
+ let target = Equality.mk_equality (w, proof, stat, metas) in
if Utils.debug_metas then
ignore(check_target context target "demod equalities input");
let metasenv' = (* metasenv @ *) metas in
begin
ignore(check_for_duplicates menv "input1");
ignore(check_disjoint_invariant subst menv "input2");
- let substs = Inference.ppsubst subst in
+ let substs = Equality.ppsubst subst in
ignore(check_target context (snd eq_found) ("input3" ^ substs))
end;
- let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
+ let pos, equality = eq_found in
+ let (_, (proof'_new,proof'_old),
+ (ty, what, other, _), menv',id') = Equality.open_equality equality in
let ty =
- try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
+ try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
with CicUtil.Meta_not_found _ -> ty
in
let what, other = if pos = Utils.Left then what, other else other, what in
let newterm, newproof =
- let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
- let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in
+ let bo =
+ Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
+(* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
+ let name = C.Name "x" in
incr demod_counter;
let bo' =
let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
in
if sign = Utils.Positive then
(bo,
- Inference.ProofBlock (
- subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
+ (Equality.Step (subst,(Equality.Demodulation,id,(pos,id'),
+ (*apply_subst subst*) (Cic.Lambda (name, ty, bo')))),
+ Equality.ProofBlock (
+ subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof_old)))
else
+ assert false
+(*
begin
prerr_endline "***************************************negative";
let metaproof =
incr maxmeta;
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context in
-(* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
-(* print_newline (); *)
+(* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
+(* print_newline (); *)
C.Meta (!maxmeta, irl)
in
let eq_found =
- let proof' =
+ let proof'_old' =
let termlist =
if pos = Utils.Left then [ty; what; other]
else [ty; other; what]
in
- Inference.ProofSymBlock (termlist, proof')
+ Equality.ProofSymBlock (termlist, proof'_old)
in
+ let proof'_new' = assert false (* not implemented *) in
let what, other =
if pos = Utils.Left then what, other else other, what
in
- pos, (0, proof', (ty, other, what, Utils.Incomparable),menv')
+ pos,
+ Equality.mk_equality
+ (0, (proof'_new',proof'_old'),
+ (ty, other, what, Utils.Incomparable),menv')
in
let target_proof =
let pb =
- Inference.ProofBlock
+ Equality.ProofBlock
(subst, eq_URI, (name, ty), bo',
- eq_found, Inference.BasicProof ([],metaproof))
+ eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
in
- match proof with
- | Inference.BasicProof _ ->
+ assert false, (* not implemented *)
+ (match snd proof with
+ | Equality.BasicProof _ ->
(* print_endline "replacing a BasicProof"; *)
pb
- | Inference.ProofGoalBlock (_, parent_proof) ->
+ | Equality.ProofGoalBlock (_, parent_proof) ->
(* print_endline "replacing another ProofGoalBlock"; *)
- Inference.ProofGoalBlock (pb, parent_proof)
- | _ -> assert false
+ Equality.ProofGoalBlock (pb, parent_proof)
+ | _ -> assert false)
in
let refl =
C.Appl [C.MutConstruct (* reflexivity *)
eq_ty; if is_left then right else left]
in
(bo,
- Inference.ProofGoalBlock (Inference.BasicProof ([],refl), target_proof))
- end
+ (assert false, (* not implemented *)
+ Equality.ProofGoalBlock
+ (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof)))
+ end
+*)
in
let newmenv = (* Inference.filter subst *) menv in
let _ =
if Utils.debug_metas then
try ignore(CicTypeChecker.type_of_aux'
- newmenv context (Inference.build_proof_term newproof) ugraph);
+ newmenv context
+ (Equality.build_proof_term_old (snd newproof)) ugraph);
()
with exc ->
prerr_endline "sempre lui";
- prerr_endline (Inference.ppsubst subst);
- prerr_endline (CicPp.ppterm (Inference.build_proof_term newproof));
+ prerr_endline (Equality.ppsubst subst);
+ prerr_endline (CicPp.ppterm
+ (Equality.build_proof_term_old (snd newproof)));
prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
- prerr_endline ("+++++++++++++subst: " ^ (Inference.ppsubst subst));
+ prerr_endline ("+++++++++++++subst: " ^ (Equality.ppsubst subst));
+ prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
+ newmenv));
raise exc;
else ()
in
build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
let res =
let w = Utils.compute_equality_weight stat in
- (w, newproof, stat,newmenv) in
+ Equality.mk_equality (w, newproof, stat,newmenv)
+ in
if Utils.debug_metas then
ignore(check_target context res "buildnew_target output");
!maxmeta, res
match res with
| Some t ->
let newmeta, newtarget = build_newtarget true t in
- if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
- (Inference.meta_convertibility_eq target newtarget) then
+ if (Equality.is_weak_identity newtarget) ||
+ (Equality.meta_convertibility_eq target newtarget) then
newmeta, newtarget
else
demodulation_equality newmeta env table sign newtarget
match res with
| Some t ->
let newmeta, newtarget = build_newtarget false t in
- if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
- (Inference.meta_convertibility_eq target newtarget) then
+ if (Equality.is_weak_identity newtarget) ||
+ (Equality.meta_convertibility_eq target newtarget) then
newmeta, newtarget
else
demodulation_equality newmeta env table sign newtarget
returns a list of new clauses inferred with a left superposition step
the negative equation "target" and one of the positive equations in "table"
*)
+let superposition_left newmeta (metasenv, context, ugraph) table target =
+ assert false
+(*
let superposition_left newmeta (metasenv, context, ugraph) table target =
let module C = Cic in
let module S = CicSubstitution in
let module HL = HelmLibraryObjects in
let module CR = CicReduction in
let module U = Utils in
- let weight, proof, (eq_ty, left, right, ordering), menv = target in
+ let weight, proof, (eq_ty, left, right, ordering), menv, id =
+ Equality.open_equality target
+ in
if Utils.debug_metas then
ignore(check_target context target "superpositionleft");
let expansions, _ =
let term = if ordering = U.Gt then left else right in
- begin
- let t1 = Unix.gettimeofday () in
- let res = betaexpand_term metasenv context ugraph table 0 term in
- let t2 = Unix.gettimeofday () in
- beta_expand_time := !beta_expand_time +. (t2 -. t1);
- res
- end
+ betaexpand_term metasenv context ugraph table 0 term
in
let maxmeta = ref newmeta in
let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
(* debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
let time1 = Unix.gettimeofday () in
- let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
+ let pos, equality = eq_found in
+ let _,proof',(ty,what,other,_),menv',id'=Equality.open_equality equality in
+ let proof'_new, proof'_old = proof' in
let what, other = if pos = Utils.Left then what, other else other, what in
let newgoal, newproof =
let bo' = U.guarded_simpl context (apply_subst s (S.subst other bo)) in
if pos = Utils.Left then [ty; what; other]
else [ty; other; what]
in
- Inference.ProofSymBlock (termlist, proof')
+ proof'_new, (* MAH????? *)
+ Equality.ProofSymBlock (termlist, proof'_old)
in
let what, other =
if pos = Utils.Left then what, other else other, what
in
- pos, (0, proof', (ty, other, what, Utils.Incomparable), menv')
+ pos,
+ Equality.mk_equality
+ (0, proof', (ty, other, what, Utils.Incomparable), menv')
in
- let target_proof =
+ let target_proof = assert false (*
let pb =
- Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
- Inference.BasicProof ([],metaproof))
+ Equality.ProofBlock
+ (s, eq_URI, (name, ty), bo'', eq_found,
+ Equality.BasicProof (Equality.empty_subst,metaproof))
in
match proof with
- | Inference.BasicProof _ ->
+ | Equality.BasicProof _ ->
(* debug_print (lazy "replacing a BasicProof"); *)
pb
- | Inference.ProofGoalBlock (_, parent_proof) ->
+ | Equality.ProofGoalBlock (_, parent_proof) ->
(* debug_print (lazy "replacing another ProofGoalBlock"); *)
- Inference.ProofGoalBlock (pb, parent_proof)
- | _ -> assert false
+ Equality.ProofGoalBlock (pb, parent_proof)
+ | _ -> assert false*)
in
let refl =
C.Appl [C.MutConstruct (* reflexivity *)
eq_ty; if ordering = U.Gt then right else left]
in
(bo',
- Inference.ProofGoalBlock (Inference.BasicProof ([],refl), target_proof))
+ (Equality.Step (Equality.SuperpositionLeft,id,(pos,id'),
+ assert false), (* il predicato della beta expand non viene tenuto? *)
+ Equality.ProofGoalBlock
+ (Equality.BasicProof (Equality.empty_subst,refl), target_proof)))
in
let left, right =
if ordering = U.Gt then newgoal, right else left, newgoal in
build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
let w = Utils.compute_equality_weight stat in
- (w, newproof, stat, newmenv)
+ Equality.mk_equality (w, newproof, stat, newmenv)
in
!maxmeta, List.map build_new expansions
;;
-
+*)
let sup_r_counter = ref 1;;
let module HL = HelmLibraryObjects in
let module CR = CicReduction in
let module U = Utils in
- let w, eqproof, (eq_ty, left, right, ordering), newmetas = target in
+ let w, (eqproof1,eqproof2), (eq_ty, left, right, ordering), newmetas,id =
+ Equality.open_equality target
+ in
if Utils.debug_metas then
ignore (check_target context target "superpositionright");
let metasenv' = newmetas in
ignore (check_target context (snd eq_found) "buildnew1" );
let time1 = Unix.gettimeofday () in
- let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
+ let pos, equality = eq_found in
+ let (_, proof', (ty, what, other, _), menv',id') =
+ Equality.open_equality equality in
let what, other = if pos = Utils.Left then what, other else other, what in
let newgoal, newproof =
(* qua *)
let bo' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in
- let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in
+(* let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in*)
+ let name = C.Name "x" in
incr sup_r_counter;
let bo'' =
let l, r =
S.lift 1 eq_ty; l; r]
in
bo',
- Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
+ ( Equality.Step (s,(Equality.SuperpositionRight,
+ id,(pos,id'),(*apply_subst s*) (Cic.Lambda(name,ty,bo'')))),
+ Equality.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof2))
+
in
let newmeta, newequality =
let left, right =
let stat = (eq_ty, left, right, neworder) in
let eq' =
let w = Utils.compute_equality_weight stat in
- (w, newproof, stat, newmenv) in
+ Equality.mk_equality (w, newproof, stat, newmenv) in
if Utils.debug_metas then
ignore (check_target context eq' "buildnew3");
- let newm, eq' = Inference.fix_metas !maxmeta eq' in
+ let newm, eq' = Equality.fix_metas !maxmeta eq' in
if Utils.debug_metas then
ignore (check_target context eq' "buildnew4");
newm, eq'
in
let new1 = List.map (build_new U.Gt) res1
and new2 = List.map (build_new U.Lt) res2 in
- let ok e = not (Inference.is_identity (metasenv', context, ugraph) e) in
+ let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
(!maxmeta,
(List.filter ok (new1 @ new2)))
;;
let module HL = HelmLibraryObjects in
let metasenv, context, ugraph = env in
let maxmeta = ref newmeta in
- let proof, metas, term = goal in
+ let (cicproof,proof), metas, term = goal in
let term = Utils.guarded_simpl (~debug:true) context term in
- let goal = proof, metas, term in
+ let goal = (cicproof,proof), metas, term in
let metasenv' = metas in
let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
- let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
+ let pos, equality = eq_found in
+ let (_, (proofnew',proof'), (ty, what, other, _), menv',id) =
+ Equality.open_equality equality in
let what, other = if pos = Utils.Left then what, other else other, what in
let ty =
try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
with CicUtil.Meta_not_found _ -> ty
in
- let newterm, newproof =
- let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
+ let newterm, newproof, newcicproof =
+ let bo =
+ Utils.guarded_simpl context (apply_subst subst(S.subst other t))
+ in
let bo' = apply_subst subst t in
- let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
+(* let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in*)
+ let name = C.Name "x" in
incr demod_counter;
let metaproof =
incr maxmeta;
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context in
+ let irl = [] (*
+ CicMkImplicit.identity_relocation_list_for_metavariable context *) in
(* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
C.Meta (!maxmeta, irl)
in
let eq_found =
- let proof' =
+ let eq_found_proof =
let termlist =
if pos = Utils.Left then [ty; what; other]
else [ty; other; what]
in
- Inference.ProofSymBlock (termlist, proof')
+ Equality.ProofSymBlock (termlist, proof')
in
let what, other =
if pos = Utils.Left then what, other else other, what
in
- pos, (0, proof', (ty, other, what, Utils.Incomparable), menv')
+ pos,
+ Equality.mk_equality
+ (0,(proofnew',eq_found_proof), (ty, other, what, Utils.Incomparable), menv')
in
let goal_proof =
let pb =
- Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
- eq_found, Inference.BasicProof ([],metaproof))
+ Equality.ProofBlock
+ (subst, eq_URI, (name, ty), bo',
+ eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
in
let rec repl = function
- | Inference.NoProof ->
+ | Equality.NoProof ->
(* debug_print (lazy "replacing a NoProof"); *)
pb
- | Inference.BasicProof _ ->
+ | Equality.BasicProof _ ->
(* debug_print (lazy "replacing a BasicProof"); *)
pb
- | Inference.ProofGoalBlock (_, parent_proof) ->
+ | Equality.ProofGoalBlock (_, parent_proof) ->
(* debug_print (lazy "replacing another ProofGoalBlock"); *)
- Inference.ProofGoalBlock (pb, parent_proof)
- | Inference.SubProof (term, meta_index, p) ->
+ Equality.ProofGoalBlock (pb, parent_proof)
+ | Equality.SubProof (term, meta_index, p) ->
prerr_endline "subproof!";
- Inference.SubProof (term, meta_index, repl p)
+ Equality.SubProof (term, meta_index, repl p)
| _ -> assert false
in repl proof
in
- bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
+ let newcicproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
+ bo, Equality.ProofGoalBlock (Equality.NoProof, goal_proof),
+ (newcicproofstep::cicproof)
in
let newmetasenv = (* Inference.filter subst *) menv in
- !maxmeta, (newproof, newmetasenv, newterm)
+ !maxmeta, ((newcicproof,newproof), newmetasenv, newterm)
in
let res =
demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
| Some t ->
let newmeta, newgoal = build_newgoal t in
let _, _, newg = newgoal in
- if Inference.meta_convertibility term newg then
- newmeta, newgoal
+ if Equality.meta_convertibility term newg then
+ true, newmeta, newgoal
else
demodulation_goal newmeta env table newgoal
| None ->
- newmeta, goal
+ false, newmeta, goal
;;
(** demodulation, when the target is a theorem *)
let metasenv' = metas in
let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
- let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
+ let pos, equality = eq_found in
+ let (_, proof', (ty, what, other, _), menv',id) =
+ Equality.open_equality equality in
let what, other = if pos = Utils.Left then what, other else other, what in
let newterm, newty =
let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
let bo' = apply_subst subst t in
let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
incr demod_counter;
- let newproof =
- Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
- Inference.BasicProof ([],term))
+ let newproofold =
+ Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
+ Equality.BasicProof (Equality.empty_subst,term))
in
- (Inference.build_proof_term newproof, bo)
+ (Equality.build_proof_term_old newproofold, bo)
in
!maxmeta, (newterm, newty, menv)
in
| Some t ->
let newmeta, newthm = build_newtheorem t in
let newt, newty, _ = newthm in
- if Inference.meta_convertibility termty newty then
+ if Equality.meta_convertibility termty newty then
newmeta, newthm
else
demodulation_theorem newmeta env table newthm
projects / helm.git / blobdiff