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;
CicTypeChecker.type_of_aux' metasenv' context right ugraph;
()
with
- CicUtil.Meta_not_found _ as exn ->
- begin
- prerr_endline msg;
- prerr_endline (CicPp.ppterm left);
- prerr_endline (CicPp.ppterm right);
- raise exn
- end
+ CicUtil.Meta_not_found _ as exn ->
+ begin
+ prerr_endline msg;
+ prerr_endline (CicPp.ppterm left);
+ prerr_endline (CicPp.ppterm right);
+ raise exn
+ end
*)
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))
+ (Inference.string_of_equality ?env e))
res));
- print_endline "|";
;;
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 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 =
+ 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 = 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
+ 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
+*)
+
+
(* 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
;;
+let profiler = HExtlib.profile "P/Indexing.get_candidates"
+
+let get_candidates ?env mode tree term =
+ profiler.HExtlib.profile (get_candidates ?env mode tree) term
let match_unif_time_ok = ref 0.;;
let match_unif_time_no = ref 0.;;
function
| [] -> None
| candidate::tl ->
- let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
+ let pos, (_, proof, (ty, left, right, o), metas) = 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);
r
with
- | Inference.MatchingFailure as e ->
+ | Inference.MatchingFailure as e ->
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
find_matches metasenv context ugraph lift_amount term termty tl
;;
-
(*
as above, but finds all the matching equalities, and the matching condition
can be either Inference.matching or Inference.unification
function
| [] -> []
| candidate::tl ->
- let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
+ let pos, (_, _, (ty, left, right, o), metas) = candidate in
let do_match c eq_URI =
let subst', metasenv', ugraph' =
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);
lift_amount term termty tl
;;
+let find_all_matches
+ ?unif_fun metasenv context ugraph lift_amount term termty l
+=
+ let rc =
+ find_all_matches
+ ?unif_fun metasenv context ugraph lift_amount term termty l
+ in
+ (*prerr_endline "CANDIDATES:";
+ List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
+ prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
+ (List.length rc));*)
+ rc
(*
returns true if target is subsumed by some equality in table
*)
let subsumption env table target =
- let _, _, (ty, left, right, _), tmetas, _ = target in
+ 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'
in
let rec ok what = function
| [] -> false, []
- | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m, _)), _))::tl ->
+ | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m)), _))::tl ->
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 @ m) context what other ugraph
- in
+ 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
true, subst
else
let rightr =
- match right with
- | Cic.Meta _ -> []
- | _ ->
+ match right with
+ | Cic.Meta _ -> []
+ | _ ->
let rightc = get_candidates Matching table right in
- find_all_matches ~unif_fun:Inference.matching
- metasenv context ugraph 0 right ty rightc
+ find_all_matches ~unif_fun:Inference.matching
+ metasenv context ugraph 0 right ty rightc
in
- ok left 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)))); *)
+(* (lazy *)
+(* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
+(* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
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) (* 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
+ | 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
+
+let profiler = HExtlib.profile "P/Indexing.demod_eq[build_new_target]"
+
(** 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 module HL = HelmLibraryObjects in
let module U = Utils in
let metasenv, context, ugraph = env in
- let w, proof, (eq_ty, left, right, order), metas, args = target in
+ let w, proof, (eq_ty, left, right, order), metas = target in
(* first, we simplify *)
let right = U.guarded_simpl context right in
let left = U.guarded_simpl context left 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
-
+ let stat = (eq_ty, left, right, order) in
+ let w = Utils.compute_equality_weight stat in
+ let target = w, proof, stat, 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
- let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
+ if Utils.debug_metas then
+ begin
+ ignore(check_for_duplicates menv "input1");
+ ignore(check_disjoint_invariant subst menv "input2");
+ 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
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
+ begin
+ prerr_endline "***************************************negative";
let metaproof =
incr maxmeta;
let irl =
let what, other =
if pos = Utils.Left then what, other else other, what
in
- pos, (0, proof', (ty, other, what, Utils.Incomparable),
- menv', args')
+ pos, (0, proof', (ty, other, what, Utils.Incomparable),menv')
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";
+ (* 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
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 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 (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: " ^ (Inference.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 stat = (eq_ty, left, right, ordering) 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
+ let w = Utils.compute_equality_weight stat in
+ (w, newproof, stat,newmenv) in
+ if Utils.debug_metas then
+ ignore(check_target context res "buildnew_target output");
+ !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
+ let build_newtarget is_left x =
+ profiler.HExtlib.profile (build_newtarget is_left) x
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 ->
- let newmeta, newtarget = build_newtarget true t in
- if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
+ let newmeta, newtarget = build_newtarget true t in
+ if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
(Inference.meta_convertibility_eq target newtarget) then
- newmeta, newtarget
- else
+ newmeta, newtarget
+ else
demodulation_equality newmeta env table sign newtarget
| None ->
- let res = demodulation_aux metasenv' context ugraph table 0 right in
- 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
- newmeta, newtarget
- else
- demodulation_equality newmeta env table sign newtarget
- | None ->
- newmeta, target
+ 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
+ if (Inference.is_weak_identity (metasenv', context, ugraph) newtarget) ||
+ (Inference.meta_convertibility_eq target newtarget) then
+ newmeta, newtarget
+ else
+ demodulation_equality newmeta env table sign newtarget
+ | None ->
+ newmeta, target
in
(* newmeta, newtarget *)
newmeta,newtarget
;;
-
(**
Performs the beta expansion of the term "term" w.r.t. "table",
i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
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) ->
r @ res, lifted_term
;;
+let profiler = HExtlib.profile "P/Indexing.betaexpand_term"
+
+let betaexpand_term metasenv context ugraph table lift_amount term =
+ profiler.HExtlib.profile
+ (betaexpand_term metasenv context ugraph table lift_amount) term
+
let sup_l_counter = ref 1;;
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 = 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 pos, (_, proof', (ty, what, other, _), menv') = eq_found 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
let what, other =
if pos = Utils.Left then what, other else other, what
in
- pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
+ pos, (0, proof', (ty, other, what, Utils.Incomparable), menv')
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 neworder = !Utils.compare_terms left right in
-
+ let stat = (eq_ty, left, right, neworder) 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 stat in
+ (w, newproof, stat, 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 = 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)
(res left right), (res right left)
in
let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
-
+ 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 pos, (_, proof', (ty, what, other, _), menv') = eq_found in
let what, other = if pos = Utils.Left then what, other else other, what in
let newgoal, newproof =
(* qua *)
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 stat = (eq_ty, left, right, neworder) in
let eq' =
- let w = Utils.compute_equality_weight eq_ty left right in
- (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs) in
+ let w = Utils.compute_equality_weight stat in
+ (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
+ 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
+ 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 ty =
try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
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
let what, other =
if pos = Utils.Left then what, other else other, what
in
- pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
+ pos, (0, 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)
+ 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
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 ->
newmeta, goal
;;
-
(** demodulation, when the target is a theorem *)
let rec demodulation_theorem newmeta env table theorem =
let module C = Cic in
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 pos, (_, proof', (ty, what, other, _), menv') = 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
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
- 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 ->