let indexing_retrieval_time = ref 0.;;
-let apply_subst = CicMetaSubst.apply_subst
+let apply_subst = Inference.apply_subst
let index = Index.index
let remove_index = Index.remove_index
let eqs = Inference.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
+ @(Inference.metas_of_term eq_ty)@(Inference.metas_of_proof proof) in
let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
let _ = if menv <> metas then
begin
prerr_endline ("right: " ^ (CicPp.ppterm right));
prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
assert false
- end
- else () in
+ end
+ else () in ()
+(*
try
- CicTypeChecker.type_of_aux'
- metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph
+ ignore(CicTypeChecker.type_of_aux'
+ metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph)
with e ->
prerr_endline msg;
prerr_endline (Inference.string_of_proof proof);
prerr_endline (CicPp.ppterm (Inference.build_proof_term proof));
prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right));
- raise e
-;;
+ raise e
+*)
(* returns a list of all the equalities in the tree that are in relation
let subsumption env table target =
let _, _, (ty, left, right, _), tmetas = target in
let metasenv, context, ugraph = env in
- let metasenv = metasenv @ tmetas in
+ let metasenv = tmetas in
let samesubst subst subst' =
let tbl = Hashtbl.create (List.length subst) in
- List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
+ List.iter (fun (m, x) -> Hashtbl.add tbl m x) subst;
List.for_all
- (fun (m, (c, t1, t2)) ->
+ (fun (m, x) ->
try
- let c', t1', t2' = Hashtbl.find tbl m in
- if (c = c') && (t1 = t1') && (t2 = t2') then true
- else false
+ let x' = Hashtbl.find tbl m in
+ x = x'
with Not_found ->
true)
subst'
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
let candidates =
- get_candidates ~env:(metasenv,context,ugraph) Matching table term in
+ get_candidates ~env:(metasenv,context,ugraph) (* Unification *) Matching table term in
+ 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))
+ candidates;
+ prerr_endline ("-------");
+ prerr_endline ("+++++++"));
(* let candidates = List.map make_variant candidates in *)
let res =
match term with
begin
ignore(check_for_duplicates menv "input1");
ignore(check_disjoint_invariant subst menv "input2");
- let substs = CicMetaSubst.ppsubst subst in
+ let substs = Inference.ppsubst subst in
ignore(check_target context (snd eq_found) ("input3" ^ substs))
end;
let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
Inference.ProofBlock (
subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
else
+ begin
+ prerr_endline "***************************************negative";
let metaproof =
incr maxmeta;
let irl =
in
let target_proof =
let pb =
- Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
- eq_found, Inference.BasicProof metaproof)
+ Inference.ProofBlock
+ (subst, eq_URI, (name, ty), bo',
+ eq_found, Inference.BasicProof ([],metaproof))
in
match proof with
| Inference.BasicProof _ ->
(* print_endline "replacing a BasicProof"; *)
pb
| Inference.ProofGoalBlock (_, parent_proof) ->
-
(* print_endline "replacing another ProofGoalBlock"; *)
Inference.ProofGoalBlock (pb, parent_proof)
| _ -> assert false
eq_ty; if is_left then right else left]
in
(bo,
- Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
+ Inference.ProofGoalBlock (Inference.BasicProof ([],refl), target_proof))
+ end
in
let newmenv = (* Inference.filter subst *) menv in
let _ =
()
with exc ->
prerr_endline "sempre lui";
- prerr_endline (CicMetaSubst.ppsubst subst);
+ prerr_endline (Inference.ppsubst subst);
prerr_endline (CicPp.ppterm (Inference.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: " ^ (CicMetaSubst.ppsubst subst));
+ prerr_endline ("+++++++++++++subst: " ^ (Inference.ppsubst subst));
raise exc;
else ()
in
let target_proof =
let pb =
Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
- Inference.BasicProof metaproof)
+ Inference.BasicProof ([],metaproof))
in
match proof with
| Inference.BasicProof _ ->
eq_ty; if ordering = U.Gt then right else left]
in
(bo',
- Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
+ Inference.ProofGoalBlock (Inference.BasicProof ([],refl), target_proof))
in
let left, right =
if ordering = U.Gt then newgoal, right else left, newgoal in
let term = Utils.guarded_simpl (~debug:true) context term in
let goal = 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 what, other = if pos = Utils.Left then what, other else other, what in
let goal_proof =
let pb =
Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
- eq_found, Inference.BasicProof metaproof)
+ eq_found, Inference.BasicProof ([],metaproof))
in
let rec repl = function
| Inference.NoProof ->
(* debug_print (lazy "replacing another ProofGoalBlock"); *)
Inference.ProofGoalBlock (pb, parent_proof)
| Inference.SubProof (term, meta_index, p) ->
+ prerr_endline "subproof!";
Inference.SubProof (term, meta_index, repl p)
| _ -> assert false
in repl proof
incr demod_counter;
let newproof =
Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
- Inference.BasicProof term)
+ Inference.BasicProof ([],term))
in
(Inference.build_proof_term newproof, bo)
in
-
- (* let m = Inference.metas_of_term newterm in *)
!maxmeta, (newterm, newty, menv)
in
let res =
projects / helm.git / blobdiff