let indexing_retrieval_time = ref 0.;;
-let apply_subst = Equality.apply_subst
+let apply_subst = Subst.apply_subst
let index = Index.index
let remove_index = Index.remove_index
let check_disjoint_invariant subst metasenv msg =
if (List.exists
- (fun (i,_,_) -> (Equality.is_in_subst i subst)) metasenv)
+ (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv)
then
begin
prerr_endline ("not disjoint: " ^ msg);
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"
+ (CicPp.ppterm(Equality.build_proof_term proof))^"\n"
in
check_for_duplicates metas "gia nella metas";
check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^p)
match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
raise e
in
- (match Equality.merge_subst_if_possible subst subst' with
+ (match Subst.merge_subst_if_possible subst subst' with
| None -> ok what tl
| Some s -> Some (s, equation))
with Inference.MatchingFailure ->
let module HL = HelmLibraryObjects in
let module U = Utils in
let metasenv, context, ugraph = env in
- let w, ((proof_new, proof_old) as proof),
- (eq_ty, left, right, order), metas, id =
- Equality.open_equality target in
+ let w, 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 = Equality.mk_equality (w, proof, stat, metas) in
+(* 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 = 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 = Equality.ppsubst subst in
+ let substs = Subst.ppsubst subst in
ignore(check_target context (snd eq_found) ("input3" ^ substs))
end;
let pos, equality = eq_found in
- let (_, (proof'_new,proof'_old),
+ let (_, proof',
(ty, what, other, _), menv',id') = Equality.open_equality equality in
let ty =
try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
S.lift 1 eq_ty; l; r]
in
if sign = Utils.Positive then
- (bo,
- (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)))
+ (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
+ (Cic.Lambda (name, ty, bo'))))))
else
assert false
(*
if Utils.debug_metas then
try ignore(CicTypeChecker.type_of_aux'
newmenv context
- (Equality.build_proof_term_old (snd newproof)) ugraph);
+ (Equality.build_proof_term newproof) ugraph);
()
with exc ->
prerr_endline "sempre lui";
- prerr_endline (Equality.ppsubst subst);
+ prerr_endline (Subst.ppsubst subst);
prerr_endline (CicPp.ppterm
- (Equality.build_proof_term_old (snd newproof)));
+ (Equality.build_proof_term newproof));
prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
- prerr_endline ("+++++++++++++subst: " ^ (Equality.ppsubst subst));
+ prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst));
prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
newmenv));
raise exc;
match res with
| Some t ->
let newmeta, newtarget = build_newtarget true t in
+ assert (not (Equality.meta_convertibility_eq target newtarget));
if (Equality.is_weak_identity newtarget) ||
(Equality.meta_convertibility_eq target newtarget) then
newmeta, newtarget
else
- demodulation_equality newmeta env table sign newtarget
+ demodulation_equality ?from newmeta env table sign newtarget
| None ->
let res = demodulation_aux metasenv' context ugraph table 0 right in
if Utils.debug_res then check_res res "demod result 1";
(Equality.meta_convertibility_eq target newtarget) then
newmeta, newtarget
else
- demodulation_equality newmeta env table sign newtarget
+ demodulation_equality ?from newmeta env table sign newtarget
| None ->
newmeta, target
in
let module HL = HelmLibraryObjects in
let module CR = CicReduction in
let module U = Utils in
- let w, (eqproof1,eqproof2), (eq_ty, left, right, ordering), newmetas,id =
+ let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
Equality.open_equality target
in
if Utils.debug_metas then
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 bo' =
+ Utils.guarded_simpl context (apply_subst s (S.subst other bo))
+ in
let name = C.Name "x" in
incr sup_r_counter;
let bo'' =
S.lift 1 eq_ty; l; r]
in
bo',
- ( 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))
-
+ Equality.Step
+ (s,(Equality.SuperpositionRight,
+ id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
in
let newmeta, newequality =
let left, right =
let module HL = HelmLibraryObjects in
let metasenv, context, ugraph = env in
let maxmeta = ref newmeta in
- let (cicproof,proof), metas, term = goal in
+ let goalproof, metas, term = goal in
let term = Utils.guarded_simpl (~debug:true) context term in
- let goal = (cicproof,proof), metas, term in
+ let goal = goalproof, metas, term in
let metasenv' = metas in
let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
let pos, equality = eq_found in
- let (_, (proofnew',proof'), (ty, what, other, _), menv',id) =
+ 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 ty =
try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
with CicUtil.Meta_not_found _ -> ty
in
- let newterm, newproof, newcicproof =
+ let newterm, newgoalproof =
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 bo' = (*apply_subst subst*) t in
let name = C.Name "x" in
incr demod_counter;
- let metaproof =
- incr maxmeta;
- 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 eq_found_proof =
- let termlist =
- if pos = Utils.Left then [ty; what; other]
- else [ty; other; what]
- in
- Equality.ProofSymBlock (termlist, proof')
- in
- let what, other =
- if pos = Utils.Left then what, other else other, what
- in
- pos,
- Equality.mk_equality
- (0,(proofnew',eq_found_proof), (ty, other, what, Utils.Incomparable), menv')
- in
- let goal_proof =
- let pb =
- Equality.ProofBlock
- (subst, eq_URI, (name, ty), bo',
- eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
- in
- let rec repl = function
- | Equality.NoProof ->
-(* debug_print (lazy "replacing a NoProof"); *)
- pb
- | Equality.BasicProof _ ->
-(* debug_print (lazy "replacing a BasicProof"); *)
- pb
- | Equality.ProofGoalBlock (_, parent_proof) ->
-(* debug_print (lazy "replacing another ProofGoalBlock"); *)
- Equality.ProofGoalBlock (pb, parent_proof)
- | Equality.SubProof (term, meta_index, p) ->
- prerr_endline "subproof!";
- Equality.SubProof (term, meta_index, repl p)
- | _ -> assert false
- in repl proof
- in
- let newcicproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
- bo, Equality.ProofGoalBlock (Equality.NoProof, goal_proof),
- (newcicproofstep::cicproof)
+ let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
+ bo, (newgoalproofstep::goalproof)
in
let newmetasenv = (* Inference.filter subst *) menv in
- !maxmeta, ((newcicproof,newproof), newmetasenv, newterm)
+ !maxmeta, (newgoalproof, newmetasenv, newterm)
in
let res =
demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
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
+(* let bo' = apply_subst subst t in *)
+(* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
incr demod_counter;
+(*
let newproofold =
Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
Equality.BasicProof (Equality.empty_subst,term))
in
(Equality.build_proof_term_old newproofold, bo)
+*)
+ (* TODO, not ported to the new proofs *)
+ if true then assert false; term, bo
in
!maxmeta, (newterm, newty, menv)
in
projects / helm.git / blobdiff