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)
+ (Equality.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))
+ (Equality.string_of_equality ?env e))
res));
- print_endline "|";
;;
let indexing_retrieval_time = ref 0.;;
-let apply_subst = CicMetaSubst.apply_subst
+let apply_subst = Equality.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,_,_) -> (Equality.is_in_subst i 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 = Equality.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,_ =
+ Equality.open_equality target in
+ (* check that metas does not contains duplicates *)
+ let eqs = Equality.string_of_equality target in
+ let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
+ let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right)
+ @(Utils.metas_of_term eq_ty)@(Equality.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 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, equality = candidate in
+ let (_, proof, (ty, left, right, o), metas,_) =
+ Equality.open_equality equality in
+ if Utils.debug_metas then
+ ignore(check_target context (snd candidate) "find_matches");
+ if Utils.debug_res then
+ begin
+ let c="eq = "^(Equality.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(Equality.build_proof_term_old (snd 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, equality = candidate in
+ let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality 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 metasenv, context, ugraph = env in
- let metasenv = 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.for_all
- (fun (m, (c, t1, t2)) ->
- try
- let c', t1', t2' = Hashtbl.find tbl m in
- if (c = c') && (t1 = t1') && (t2 = t2') then true
- else false
- with Not_found ->
- true)
- subst'
+let subsumption env table target =
+ (*
+ let print_res l =
+ prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
+ ((pos,equation),_)) -> Inference.string_of_equality equation)l))
in
+ *)
+ let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
+ let metasenv, context, ugraph = env in
+ let metasenv = tmetas in
let leftr =
match left with
- | Cic.Meta _ -> []
+ | Cic.Meta _ -> []
| _ ->
let leftc = get_candidates Matching table left in
find_all_matches ~unif_fun:Inference.matching
metasenv context ugraph 0 left ty leftc
in
+(* print_res leftr;*)
let rec ok what = function
- | [] -> false, []
- | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m, _)), _))::tl ->
+ | [] -> None
+ | (_, subst, menv, ug, ((pos,equation),_))::tl ->
+ let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
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 metasenv m context what other ugraph
+ in
let t2 = Unix.gettimeofday () in
match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
r
match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
raise e
in
- if samesubst subst subst' then
- true, subst
- else
- ok what tl
+ (match Equality.merge_subst_if_possible subst subst' with
+ | None -> ok what tl
+ | Some s -> Some (s, equation))
with Inference.MatchingFailure ->
ok what tl
in
- let r, subst = ok right leftr in
- let r, s =
- if r then
- true, subst
- else
+ match ok right leftr with
+ | Some _ as res -> res
+ | None ->
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
- in
+(* print_res rightr;*)
+ ok left rightr
(* (if r then *)
(* debug_print *)
-(* (lazy *)
-(* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
-(* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
- r, s
+(* (lazy *)
+(* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
+(* (Inference.string_of_equality target) (Utils.print_subst 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 (Equality.string_of_equality x))
+ candidates;
+ prerr_endline ("-------");
+ prerr_endline ("+++++++"));
+ 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_new, proof_old) as 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 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 = 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
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 = Equality.ppsubst subst in
+ ignore(check_target context (snd eq_found) ("input3" ^ substs))
+ end;
+ let pos, equality = eq_found in
+ let (_, (proof'_new,proof'_old),
+ (ty, what, other, _), menv',id') = Equality.open_equality equality in
let ty =
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 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" 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,
+ (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)))
else
+ assert false
+(*
+ begin
+ prerr_endline "***************************************negative";
let metaproof =
incr maxmeta;
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context in
-(* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
-(* print_newline (); *)
+(* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
+(* print_newline (); *)
C.Meta (!maxmeta, irl)
in
let eq_found =
- let proof' =
+ let proof'_old' =
let termlist =
if pos = Utils.Left then [ty; what; other]
else [ty; other; what]
in
- Inference.ProofSymBlock (termlist, proof')
+ Equality.ProofSymBlock (termlist, proof'_old)
in
+ let proof'_new' = assert false (* not implemented *) 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,
+ Equality.mk_equality
+ (0, (proof'_new',proof'_old'),
+ (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)
+ Equality.ProofBlock
+ (subst, eq_URI, (name, ty), bo',
+ eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
in
- match proof with
- | Inference.BasicProof _ ->
- print_endline "replacing a BasicProof";
+ assert false, (* not implemented *)
+ (match snd proof with
+ | Equality.BasicProof _ ->
+ (* print_endline "replacing a BasicProof"; *)
pb
- | Inference.ProofGoalBlock (_, parent_proof) ->
- print_endline "replacing another ProofGoalBlock";
- Inference.ProofGoalBlock (pb, parent_proof)
- | _ -> assert false
+ | Equality.ProofGoalBlock (_, parent_proof) ->
+ (* print_endline "replacing another ProofGoalBlock"; *)
+ Equality.ProofGoalBlock (pb, parent_proof)
+ | _ -> assert false)
in
let refl =
C.Appl [C.MutConstruct (* reflexivity *)
eq_ty; if is_left then right else left]
in
(bo,
- Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
+ (assert false, (* not implemented *)
+ Equality.ProofGoalBlock
+ (Equality.BasicProof (Equality.empty_subst,refl), snd 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
+ (Equality.build_proof_term_old (snd newproof)) ugraph);
+ ()
+ with exc ->
+ prerr_endline "sempre lui";
+ prerr_endline (Equality.ppsubst subst);
+ prerr_endline (CicPp.ppterm
+ (Equality.build_proof_term_old (snd 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 ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
+ newmenv));
+ 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)
+ let w = Utils.compute_equality_weight stat in
+ Equality.mk_equality (w, newproof, stat,newmenv)
in
- !maxmeta, res
+ 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) ||
- (Inference.meta_convertibility_eq target newtarget) then
- newmeta, newtarget
- else
+ 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
| 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 (Equality.is_weak_identity newtarget) ||
+ (Equality.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;;
returns a list of new clauses inferred with a left superposition step
the negative equation "target" and one of the positive equations in "table"
*)
+let superposition_left newmeta (metasenv, context, ugraph) table target =
+ assert false
+(*
let superposition_left newmeta (metasenv, context, ugraph) table target =
let module C = Cic in
let module S = CicSubstitution in
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, id =
+ Equality.open_equality 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
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, equality = eq_found in
+ let _,proof',(ty,what,other,_),menv',id'=Equality.open_equality equality in
+ let proof'_new, proof'_old = proof' 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
if pos = Utils.Left then [ty; what; other]
else [ty; other; what]
in
- Inference.ProofSymBlock (termlist, proof')
+ proof'_new, (* MAH????? *)
+ Equality.ProofSymBlock (termlist, proof'_old)
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,
+ Equality.mk_equality
+ (0, proof', (ty, other, what, Utils.Incomparable), menv')
in
- let target_proof =
+ let target_proof = assert false (*
let pb =
- Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
- Inference.BasicProof metaproof)
+ Equality.ProofBlock
+ (s, eq_URI, (name, ty), bo'', eq_found,
+ Equality.BasicProof (Equality.empty_subst,metaproof))
in
match proof with
- | Inference.BasicProof _ ->
+ | Equality.BasicProof _ ->
(* debug_print (lazy "replacing a BasicProof"); *)
pb
- | Inference.ProofGoalBlock (_, parent_proof) ->
+ | Equality.ProofGoalBlock (_, parent_proof) ->
(* debug_print (lazy "replacing another ProofGoalBlock"); *)
- Inference.ProofGoalBlock (pb, parent_proof)
- | _ -> assert false
+ Equality.ProofGoalBlock (pb, parent_proof)
+ | _ -> assert false*)
in
let refl =
C.Appl [C.MutConstruct (* reflexivity *)
eq_ty; if ordering = U.Gt then right else left]
in
(bo',
- Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof))
+ (Equality.Step (Equality.SuperpositionLeft,id,(pos,id'),
+ assert false), (* il predicato della beta expand non viene tenuto? *)
+ Equality.ProofGoalBlock
+ (Equality.BasicProof (Equality.empty_subst,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
+ Equality.mk_equality (w, newproof, stat, newmenv)
+
in
!maxmeta, List.map build_new expansions
;;
-
+*)
let sup_r_counter = ref 1;;
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, (eqproof1,eqproof2), (eq_ty, left, right, ordering), newmetas,id =
+ Equality.open_equality 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, equality = eq_found in
+ 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 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 name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in*)
+ let name = C.Name "x" in
incr sup_r_counter;
let bo'' =
let l, r =
S.lift 1 eq_ty; l; r]
in
bo',
- Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof)
+ ( 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))
+
in
let newmeta, newequality =
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 newm, eq' = Inference.fix_metas !maxmeta eq' in
+ let w = Utils.compute_equality_weight stat in
+ Equality.mk_equality (w, newproof, stat, newmenv) in
+ if Utils.debug_metas then
+ ignore (check_target context eq' "buildnew3");
+ let newm, eq' = Equality.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
+ let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
(!maxmeta,
(List.filter ok (new1 @ new2)))
;;
let module HL = HelmLibraryObjects in
let metasenv, context, ugraph = env in
let maxmeta = ref newmeta in
- let proof, metas, term = goal in
+ let (cicproof,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 goal = (cicproof,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', args') = eq_found in
+ let pos, equality = eq_found in
+ let (_, (proofnew',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 =
- (* qua *)
- let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
+ let newterm, newproof, newcicproof =
+ 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 name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in*)
+ let name = C.Name "x" in
incr demod_counter;
let metaproof =
incr maxmeta;
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context in
+ 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 proof' =
+ let eq_found_proof =
let termlist =
if pos = Utils.Left then [ty; what; other]
else [ty; other; what]
in
- Inference.ProofSymBlock (termlist, proof')
+ Equality.ProofSymBlock (termlist, proof')
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,
+ Equality.mk_equality
+ (0,(proofnew',eq_found_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)
+ Equality.ProofBlock
+ (subst, eq_URI, (name, ty), bo',
+ eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
in
let rec repl = function
- | Inference.NoProof ->
+ | Equality.NoProof ->
(* debug_print (lazy "replacing a NoProof"); *)
pb
- | Inference.BasicProof _ ->
+ | Equality.BasicProof _ ->
(* debug_print (lazy "replacing a BasicProof"); *)
pb
- | Inference.ProofGoalBlock (_, parent_proof) ->
+ | Equality.ProofGoalBlock (_, parent_proof) ->
(* debug_print (lazy "replacing another ProofGoalBlock"); *)
- Inference.ProofGoalBlock (pb, parent_proof)
- | Inference.SubProof (term, meta_index, p) ->
- Inference.SubProof (term, meta_index, repl p)
+ 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
- bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
+ let newcicproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
+ bo, Equality.ProofGoalBlock (Equality.NoProof, goal_proof),
+ (newcicproofstep::cicproof)
in
- let m = Inference.metas_of_term newterm in
- (* QUA *)
- let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) (menv @ menv')in
- !maxmeta, (newproof, newmetasenv, newterm)
+ let newmetasenv = (* Inference.filter subst *) menv in
+ !maxmeta, ((newcicproof,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 newmeta, newgoal = build_newgoal t in
let _, _, newg = newgoal in
- if Inference.meta_convertibility term newg then
- newmeta, newgoal
+ if Equality.meta_convertibility term newg then
+ false, newmeta, newgoal
else
- demodulation_goal newmeta env table newgoal
+ let changed, newmeta, newgoal =
+ demodulation_goal newmeta env table newgoal
+ in
+ true, newmeta, newgoal
| None ->
- newmeta, goal
+ false, 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, equality = eq_found in
+ 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 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)
+ let newproofold =
+ Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
+ Equality.BasicProof (Equality.empty_subst,term))
in
- (Inference.build_proof_term newproof, bo)
+ (Equality.build_proof_term_old newproofold, 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 ->
let newmeta, newthm = build_newtheorem t in
let newt, newty, _ = newthm in
- if Inference.meta_convertibility termty newty then
+ if Equality.meta_convertibility termty newty then
newmeta, newthm
else
demodulation_theorem newmeta env table newthm
projects / helm.git / blobdiff