module Index = Equality_indexing.DT (* path tree based indexing *)
*)
+let beta_expand_time = ref 0.;;
+
let debug_print = Utils.debug_print;;
(*
for debugging
let check_equation env equation msg =
let w, proof, (eq_ty, left, right, order), metas, args = equation in
- let metasenv, context, ugraph = env in
+ let metasenv, context, ugraph = env
let metasenv' = metasenv @ metas in
try
CicTypeChecker.type_of_aux' metasenv' context left ugraph;
type retrieval_mode = Matching | Unification;;
-let print_candidates mode term res =
+let string_of_res ?env =
+ function
+ None -> "None"
+ | 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)
+ (CicPp.ppterm t)
+;;
+
+let print_res ?env res =
+ prerr_endline
+ (String.concat "\n"
+ (List.map (string_of_res ?env) res))
+;;
+
+let print_candidates ?env mode term res =
let _ =
match mode with
| Matching ->
- Printf.printf "| candidates Matching %s\n" (CicPp.ppterm term)
+ prerr_endline ("| candidates Matching " ^ (CicPp.ppterm term))
| Unification ->
- Printf.printf "| candidates Unification %s\n" (CicPp.ppterm term)
+ prerr_endline ("| candidates Unification " ^ (CicPp.ppterm term))
in
- print_endline
+ prerr_endline
(String.concat "\n"
(List.map
- (fun (p, e) ->
- Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
- (Inference.string_of_equality e))
- res));
- print_endline "|";
+ (fun (p, e) ->
+ Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
+ (Inference.string_of_equality ?env e))
+ res));
;;
let empty = Index.empty
let init_index = Index.init_index
+let check_disjoint_invariant subst metasenv msg =
+ if (List.exists
+ (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv)
+ then
+ begin
+ prerr_endline ("not disjoint: " ^ msg);
+ assert false
+ end
+;;
+
+let check_for_duplicates metas msg =
+let _ =
+ try
+ ignore(CicUtil.lookup_meta 190 metas);
+ prerr_endline ("eccoci in " ^ msg);
+ with
+ CicUtil.Meta_not_found _ -> () in
+if List.length metas <>
+ List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then
+ begin
+ prerr_endline ("DUPLICATI " ^ msg);
+ prerr_endline (CicMetaSubst.ppmetasenv [] metas);
+ assert false
+ end
+;;
+
+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
+ 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, args = target in
+ (* check that metas does not contains duplicates *)
+ 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
+ let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
+ let _ = if menv <> metas then
+ begin
+ prerr_endline ("extra metas " ^ msg);
+ prerr_endline (CicMetaSubst.ppmetasenv [] metas);
+ prerr_endline "**********************";
+ prerr_endline (CicMetaSubst.ppmetasenv [] menv);
+ prerr_endline ("left: " ^ (CicPp.ppterm left));
+ prerr_endline ("right: " ^ (CicPp.ppterm right));
+ prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
+ assert false
+ end
+ else () in
+ try
+ 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
+;;
+
+
(* returns a list of all the equalities in the tree that are in relation
"mode" with the given term, where mode can be either Matching or
Unification.
the position will always be Left, and if the ordering is left < right,
position will be Right.
*)
-let get_candidates mode tree term =
+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
let res =
let s =
in
Index.PosEqSet.elements s
in
- (* print_candidates mode term res; *)
(* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
(* print_newline (); *)
let t2 = Unix.gettimeofday () in
- indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
- res
+ indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
+ (* make fresh instances *)
+ res
;;
| [] -> None
| candidate::tl ->
let pos, (_, proof, (ty, left, right, o), metas, args) = candidate 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
+ check_for_duplicates metas "gia nella metas";
+ 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 (
find_matches metasenv context ugraph lift_amount term termty tl
let t1 = Unix.gettimeofday () in
try
let r =
- Inference.matching (metasenv @ metas) context
- term (S.lift lift_amount c) ugraph
+ ( Inference.matching metasenv metas context
+ term (S.lift lift_amount c)) ugraph
in
let t2 = Unix.gettimeofday () in
match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
let t2 = Unix.gettimeofday () in
match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
raise e
- | CicUtil.Meta_not_found _ as exn ->
- prerr_endline "zurg";
- raise exn
+ | CicUtil.Meta_not_found _ as exn -> raise exn
in
Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
(candidate, eq_URI))
else right, left, Utils.eq_ind_r_URI ()
in
if o <> U.Incomparable then
- try
- do_match c eq_URI
- with Inference.MatchingFailure ->
- find_matches metasenv context ugraph lift_amount term termty tl
+ let res =
+ try
+ do_match c eq_URI
+ with Inference.MatchingFailure ->
+ find_matches metasenv context ugraph lift_amount term termty tl
+ in
+ if Utils.debug_res then ignore (check_res res "find1");
+ res
else
let res =
try do_match c eq_URI
with Inference.MatchingFailure -> None
in
+ if Utils.debug_res then ignore (check_res res "find2");
match res with
| Some (_, s, _, _, _) ->
let c' = apply_subst s c in
let t1 = Unix.gettimeofday () in
try
let r =
- unif_fun (metasenv @ metas) context
+ unif_fun metasenv metas context
term (S.lift lift_amount c) ugraph in
let t2 = Unix.gettimeofday () in
match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
let t1 = Unix.gettimeofday () in
try
let r =
- Inference.matching (metasenv @ menv @ m) context what other ugraph
+ Inference.matching menv m context what other ugraph
in
let t2 = Unix.gettimeofday () in
match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
r, s
;;
-
-let rec demodulation_aux ?(typecheck=false)
- metasenv context ugraph table lift_amount term =
+let rec demodulation_aux ?from ?(typecheck=false)
+ metasenv context ugraph table lift_amount term =
(* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *)
-
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
- let candidates = get_candidates Matching table term in
- match term with
- | C.Meta _ -> None
- | term ->
- let termty, ugraph =
- if typecheck then
- CicTypeChecker.type_of_aux' metasenv context term ugraph
- else
- C.Implicit None, ugraph
- in
- let res =
- find_matches metasenv context ugraph lift_amount term termty candidates
- in
- if res <> None then
- res
- else
- match term with
- | C.Appl l ->
- let res, ll =
- List.fold_left
- (fun (res, tl) t ->
- if res <> None then
- (res, tl @ [S.lift 1 t])
- else
- let r =
- demodulation_aux metasenv context ugraph table
- lift_amount t
- in
- match r with
- | None -> (None, tl @ [S.lift 1 t])
- | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
- (None, []) l
- in (
- match res with
- | None -> None
- | Some (_, subst, menv, ug, eq_found) ->
- Some (C.Appl ll, subst, menv, ug, eq_found)
- )
- | C.Prod (nn, s, t) ->
- let r1 =
- demodulation_aux metasenv context ugraph table lift_amount s in (
- match r1 with
- | None ->
- let r2 =
- demodulation_aux metasenv
- ((Some (nn, C.Decl s))::context) ugraph
- table (lift_amount+1) t
- in (
- match r2 with
- | None -> None
- | Some (t', subst, menv, ug, eq_found) ->
- Some (C.Prod (nn, (S.lift 1 s), t'),
- subst, menv, ug, eq_found)
- )
- | Some (s', subst, menv, ug, eq_found) ->
- Some (C.Prod (nn, s', (S.lift 1 t)),
- subst, menv, ug, eq_found)
- )
- | C.Lambda (nn, s, t) ->
- let r1 =
- demodulation_aux metasenv context ugraph table lift_amount s in (
- match r1 with
- | None ->
- let r2 =
- demodulation_aux metasenv
- ((Some (nn, C.Decl s))::context) ugraph
- table (lift_amount+1) t
- in (
- match r2 with
- | None -> None
- | Some (t', subst, menv, ug, eq_found) ->
- Some (C.Lambda (nn, (S.lift 1 s), t'),
- subst, menv, ug, eq_found)
- )
- | Some (s', subst, menv, ug, eq_found) ->
- Some (C.Lambda (nn, s', (S.lift 1 t)),
- subst, menv, ug, eq_found)
- )
- | t ->
- None
+ let candidates =
+ get_candidates ~env:(metasenv,context,ugraph) Matching table term in
+(* let candidates = List.map make_variant candidates in *)
+ let res =
+ match term with
+ | C.Meta _ -> None
+ | term ->
+ let termty, ugraph =
+ if typecheck then
+ CicTypeChecker.type_of_aux' metasenv context term ugraph
+ else
+ C.Implicit None, ugraph
+ in
+ let res =
+ find_matches metasenv context ugraph lift_amount term termty candidates
+ in
+ if Utils.debug_res then ignore(check_res res "demod1");
+ if res <> None then
+ res
+ else
+ match term with
+ | C.Appl l ->
+ let res, ll =
+ List.fold_left
+ (fun (res, tl) t ->
+ if res <> None then
+ (res, tl @ [S.lift 1 t])
+ else
+ let r =
+ demodulation_aux ~from:"1" metasenv context ugraph table
+ lift_amount t
+ in
+ match r with
+ | None -> (None, tl @ [S.lift 1 t])
+ | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
+ (None, []) l
+ in (
+ match res with
+ | None -> None
+ | Some (_, subst, menv, ug, eq_found) ->
+ Some (C.Appl ll, subst, menv, ug, eq_found)
+ )
+ | C.Prod (nn, s, t) ->
+ let r1 =
+ demodulation_aux ~from:"2"
+ metasenv context ugraph table lift_amount s in (
+ match r1 with
+ | None ->
+ let r2 =
+ demodulation_aux metasenv
+ ((Some (nn, C.Decl s))::context) ugraph
+ table (lift_amount+1) t
+ in (
+ match r2 with
+ | None -> None
+ | Some (t', subst, menv, ug, eq_found) ->
+ Some (C.Prod (nn, (S.lift 1 s), t'),
+ subst, menv, ug, eq_found)
+ )
+ | Some (s', subst, menv, ug, eq_found) ->
+ Some (C.Prod (nn, s', (S.lift 1 t)),
+ subst, menv, ug, eq_found)
+ )
+ | C.Lambda (nn, s, t) ->
+ let r1 =
+ demodulation_aux
+ metasenv context ugraph table lift_amount s in (
+ match r1 with
+ | None ->
+ let r2 =
+ demodulation_aux metasenv
+ ((Some (nn, C.Decl s))::context) ugraph
+ table (lift_amount+1) t
+ in (
+ match r2 with
+ | None -> None
+ | Some (t', subst, menv, ug, eq_found) ->
+ Some (C.Lambda (nn, (S.lift 1 s), t'),
+ subst, menv, ug, eq_found)
+ )
+ | Some (s', subst, menv, ug, eq_found) ->
+ Some (C.Lambda (nn, s', (S.lift 1 t)),
+ subst, menv, ug, eq_found)
+ )
+ | t ->
+ None
+ in
+ if Utils.debug_res then ignore(check_res res "demod_aux output");
+ res
;;
let demod_counter = ref 1;;
+exception Foo
+
(** demodulation, when target is an equality *)
-let rec demodulation_equality newmeta env table sign target =
+let rec demodulation_equality ?from newmeta env table sign target =
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
let w = Utils.compute_equality_weight eq_ty left right in
let order = !Utils.compare_terms left right in
let target = w, proof, (eq_ty, left, right, order), metas, args in
-
- let metasenv' = metasenv @ metas in
-
+ if Utils.debug_metas then
+ ignore(check_target context target "demod equalities input");
+ let metasenv' = (* metasenv @ *) metas in
let maxmeta = ref newmeta in
let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
let time1 = Unix.gettimeofday () in
+ if Utils.debug_metas then
+ begin
+ ignore(check_for_duplicates menv "input1");
+ ignore(check_disjoint_invariant subst menv "input2");
+ let substs = CicMetaSubst.ppsubst subst in
+ ignore(check_target context (snd eq_found) ("input3" ^ substs))
+ end;
let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found 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 name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) 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
- C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
- S.lift 1 eq_ty; l; r]
+ C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
+ S.lift 1 eq_ty; l; r]
in
if sign = Utils.Positive then
- (bo,
- Inference.ProofBlock (
- subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
+ (bo,
+ Inference.ProofBlock (
+ subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof))
else
let metaproof =
incr maxmeta;
in
match proof with
| Inference.BasicProof _ ->
- print_endline "replacing a BasicProof";
+ (* print_endline "replacing a BasicProof"; *)
pb
| Inference.ProofGoalBlock (_, parent_proof) ->
- print_endline "replacing another ProofGoalBlock";
+
+ (* print_endline "replacing another ProofGoalBlock"; *)
Inference.ProofGoalBlock (pb, parent_proof)
| _ -> assert false
in
(bo,
Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
in
- let left, right = if is_left then newterm, right else left, newterm in
- let m =
- (Inference.metas_of_term left)
- @ (Inference.metas_of_term right)
- @ (Inference.metas_of_term eq_ty) in
- (* let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') *)
- let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metasenv' @ menv')
- and newargs = args
+ 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);
+ ()
+ with exc ->
+ prerr_endline "sempre lui";
+ prerr_endline (CicMetaSubst.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));
+ raise exc;
+ else ()
in
+ let left, right = if is_left then newterm, right else left, newterm in
let ordering = !Utils.compare_terms left right in
-
let time2 = Unix.gettimeofday () in
build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
-
let res =
let w = Utils.compute_equality_weight eq_ty left right in
- (w, newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
- in
- !maxmeta, res
- in
- let _ =
- try
- CicTypeChecker.type_of_aux' metasenv' context left ugraph;
- CicTypeChecker.type_of_aux' metasenv' context right ugraph;
- with
- CicUtil.Meta_not_found _ as exn ->
- begin
- prerr_endline "siamo in demodulation_equality 1";
- prerr_endline (CicPp.ppterm left);
- prerr_endline (CicPp.ppterm right);
- raise exn
- end
+ (w, newproof, (eq_ty, left, right, ordering),newmenv,args) in
+ if Utils.debug_metas then
+ ignore(check_target context res "buildnew_target output");
+ !maxmeta, res
in
- let res = demodulation_aux metasenv' context ugraph table 0 left in
+
+ let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
+ if Utils.debug_res then check_res res "demod result";
let newmeta, newtarget =
match res with
| Some t ->
if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
(Inference.meta_convertibility_eq target newtarget) then
newmeta, newtarget
- else
+ else
demodulation_equality 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";
match res with
| Some t ->
let newmeta, newtarget = build_newtarget false t in
(Inference.meta_convertibility_eq target newtarget) then
newmeta, newtarget
else
- demodulation_equality newmeta env table sign newtarget
+ demodulation_equality newmeta env table sign newtarget
| None ->
newmeta, target
in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
let candidates = get_candidates Unification table term in
+
let res, lifted_term =
match term with
| C.Meta (i, l) ->
let module CR = CicReduction in
let module U = Utils in
let weight, proof, (eq_ty, left, right, ordering), menv, _ = 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
- betaexpand_term metasenv context ugraph table 0 term
+ 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
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', args') = eq_found in
let left, right =
if ordering = U.Gt then newgoal, right else left, newgoal in
let neworder = !Utils.compare_terms left right in
-
+ let newmenv = (* Inference.filter s *) menv in
let time2 = Unix.gettimeofday () in
build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
- let res =
- let w = Utils.compute_equality_weight eq_ty left right in
- (w, newproof, (eq_ty, left, right, neworder), menv @ menv', [])
- in
- res
+ let w = Utils.compute_equality_weight eq_ty left right in
+ (w, newproof, (eq_ty, left, right, neworder), newmenv, [])
+
in
!maxmeta, List.map build_new expansions
;;
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
let module CR = CicReduction in
- let module U = Utils in
- let _, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
- let metasenv' = metasenv @ newmetas in
+ let module U = Utils in
+ let w, eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
+ if Utils.debug_metas then
+ ignore (check_target context target "superpositionright");
+ let metasenv' = newmetas in
let maxmeta = ref newmeta in
let res1, res2 =
+ let betaexpand_term metasenv context ugraph table d term =
+ let t1 = Unix.gettimeofday () in
+ let res = betaexpand_term metasenv context ugraph table d term in
+ let t2 = Unix.gettimeofday () in
+ beta_expand_time := !beta_expand_time +. (t2 -. t1);
+ res
+ in
match ordering with
| U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
| U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
in
(res left right), (res right left)
in
- let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
-
+ let build_new ordering ((bo, s, m, ug, (eq_found, eq_URI)) as input) =
+ if Utils.debug_metas then
+ ignore (check_target context (snd eq_found) "buildnew1" );
let time1 = Unix.gettimeofday () in
let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
let left, right =
if ordering = U.Gt then newgoal, apply_subst s right
else apply_subst s left, newgoal in
- let neworder = !Utils.compare_terms left right
- and newmenv = newmetas @ menv'
- and newargs = args @ args' in
+ let neworder = !Utils.compare_terms left right in
+ let newmenv = (* Inference.filter s *) m in
+ let newargs = args @ args' in
let eq' =
let w = Utils.compute_equality_weight eq_ty left right in
(w, newproof, (eq_ty, left, right, neworder), newmenv, newargs) in
+ if Utils.debug_metas then
+ ignore (check_target context eq' "buildnew3");
let newm, eq' = Inference.fix_metas !maxmeta eq' in
+ if Utils.debug_metas then
+ ignore (check_target context eq' "buildnew4");
newm, eq'
in
maxmeta := newmeta;
-
let time2 = Unix.gettimeofday () in
build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
-
+ if Utils.debug_metas then
+ ignore(check_target context newequality "buildnew2");
newequality
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 (Inference.is_identity (metasenv', context, ugraph) e) in
(!maxmeta,
(List.filter ok (new1 @ new2)))
let proof, metas, term = goal in
let term = Utils.guarded_simpl (~debug:true) context term in
let goal = proof, metas, term in
- let metasenv' = metasenv @ metas in
+ let metasenv' = metas in
let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
with CicUtil.Meta_not_found _ -> ty
in
let newterm, newproof =
- (* qua *)
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
in
bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
in
- let m = Inference.metas_of_term newterm in
- (* QUA *)
- let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (menv @ menv')in
+ let newmetasenv = (* Inference.filter subst *) menv in
!maxmeta, (newproof, newmetasenv, newterm)
in
let res =
- demodulation_aux ~typecheck:true metasenv' context ugraph table 0 term
+ demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
in
match res with
| Some t ->
let metasenv, context, ugraph = env in
let maxmeta = ref newmeta in
let term, termty, metas = theorem in
- let metasenv' = metasenv @ metas in
+ let metasenv' = metas in
let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
let what, other = if pos = Utils.Left then what, other else other, what in
let newterm, newty =
- (* qua *)
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
in
let m = Inference.metas_of_term newterm in
- let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (metas @ menv') in
- !maxmeta, (newterm, newty, newmetasenv)
+ !maxmeta, (newterm, newty, menv)
in
let res =
- demodulation_aux ~typecheck:true metasenv' context ugraph table 0 termty
+ demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
in
match res with
| Some t ->
projects / helm.git / blobdiff