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;;
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)
+ 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
- (fun (p, e) ->
- Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
- (Inference.string_of_equality ?env e))
- res));
+ (fun (p, e) ->
+ Printf.sprintf "| (%s, %s)" (Utils.string_of_pos p)
+ (Inference.string_of_equality ?env e))
+ res));
;;
let check_disjoint_invariant subst metasenv msg =
if (List.exists
- (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv)
+ (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) 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
- check_disjoint_invariant subst menv msg;
- check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
+ let eqs = Inference.string_of_equality (snd eq_found) in
+ check_disjoint_invariant subst menv msg;
+ check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
| None -> ()
;;
else () in
try
CicTypeChecker.type_of_aux'
- metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph
+ metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph
with e ->
prerr_endline msg;
prerr_endline (Inference.string_of_proof proof);
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.;;
| candidate::tl ->
let pos, (_, proof, (ty, left, right, o), metas) = candidate in
if Utils.debug_metas then
- ignore(check_target context (snd candidate) "find_matches");
+ 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
+ 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;
+ 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
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 -> raise exn
+ | CicUtil.Meta_not_found _ as exn -> raise exn
in
Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
(candidate, eq_URI))
in
if o <> U.Incomparable then
let res =
- try
- do_match c eq_URI
+ 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
+ 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
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
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
try
let r =
Inference.matching menv m context what other ugraph
- in
+ 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
;;
match term with
| C.Meta _ -> None
| term ->
- let termty, ugraph =
+ let termty, ugraph =
if typecheck then
CicTypeChecker.type_of_aux' metasenv context term ugraph
else
C.Implicit None, ugraph
- in
- let res =
+ in
+ let res =
find_matches metasenv context ugraph lift_amount term termty candidates
- in
+ in
if Utils.debug_res then ignore(check_res res "demod1");
- if res <> None then
+ if res <> None then
res
- else
+ 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
+ | 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
exception Foo
+let profiler = HExtlib.profile "P/Indexing.demod_eq[build_new_target]"
+
(** demodulation, when target is an equality *)
let rec demodulation_equality ?from newmeta env table sign target =
let module C = Cic in
if Utils.debug_metas then
begin
ignore(check_for_duplicates menv "input1");
- ignore(check_disjoint_invariant subst menv "input2");
+ ignore(check_disjoint_invariant subst menv "input2");
let substs = CicMetaSubst.ppsubst subst in
- ignore(check_target context (snd eq_found) ("input3" ^ substs))
+ ignore(check_target context (snd eq_found) ("input3" ^ substs))
end;
let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
let ty =
let newmenv = (* Inference.filter subst *) menv in
let _ =
if Utils.debug_metas then
- try ignore(CicTypeChecker.type_of_aux'
+ try ignore(CicTypeChecker.type_of_aux'
newmenv context (Inference.build_proof_term newproof) ugraph);
- ()
- with exc ->
+ ()
+ with exc ->
prerr_endline "sempre lui";
prerr_endline (CicMetaSubst.ppsubst subst);
- prerr_endline (CicPp.ppterm (Inference.build_proof_term newproof));
+ 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;
+ raise exc;
else ()
in
let left, right = if is_left then newterm, right else left, newterm in
ignore(check_target context res "buildnew_target output");
!maxmeta, res
in
+ let build_newtarget is_left x =
+ profiler.HExtlib.profile (build_newtarget is_left) x
+ 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
- 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
+ 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
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 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
+ 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
in
(res left right), (res right left)
in
- let build_new ordering ((bo, s, m, ug, (eq_found, eq_URI)) as input) =
+ 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 w = Utils.compute_equality_weight stat in
(w, newproof, stat, newmenv) in
if Utils.debug_metas then
- ignore (check_target context eq' "buildnew3");
+ 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");
+ ignore (check_target context eq' "buildnew4");
newm, eq'
in
maxmeta := newmeta;
newmeta, goal
;;
-
(** demodulation, when the target is a theorem *)
let rec demodulation_theorem newmeta env table theorem =
let module C = Cic in
(Inference.build_proof_term newproof, bo)
in
- let m = Inference.metas_of_term newterm in
+ (* let m = Inference.metas_of_term newterm in *)
!maxmeta, (newterm, newty, menv)
in
let res =
projects / helm.git / blobdiff