* http://cs.unibo.it/helm/.
*)
+let _profiler = <:profiler<_profiler>>;;
+
(* $Id$ *)
+type goal = Equality.goal_proof * Cic.metasenv * Cic.term
+
module Index = Equality_indexing.DT (* discrimination tree based indexing *)
(*
module Index = Equality_indexing.DT (* path tree based indexing *)
*)
-let beta_expand_time = ref 0.;;
-
let debug_print = Utils.debug_print;;
(*
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)
+ (Equality.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)
+ (Equality.string_of_equality ?env e))
+ res));
;;
-let indexing_retrieval_time = ref 0.;;
-
-
-let apply_subst = CicMetaSubst.apply_subst
+let apply_subst = Subst.apply_subst
let index = Index.index
let remove_index = Index.remove_index
let check_disjoint_invariant subst metasenv msg =
if (List.exists
- (fun (i,_,_) -> (List.exists (fun (j,_) -> i=j) subst)) metasenv)
+ (fun (i,_,_) -> (Subst.is_in_subst i 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 = 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 = target in
+ let w, proof, (eq_ty, left, right, order), metas,_ =
+ Equality.open_equality target in
(* check that metas does not contains duplicates *)
- let eqs = Inference.string_of_equality target in
+ let eqs = Equality.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 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 ("right: " ^ (CicPp.ppterm right));
prerr_endline ("ty: " ^ (CicPp.ppterm eq_ty));
assert false
- end
- else () in
+ end
+ else () in ()
+(*
try
- CicTypeChecker.type_of_aux'
- metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph
+ ignore(CicTypeChecker.type_of_aux'
+ metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph)
with e ->
prerr_endline msg;
prerr_endline (Inference.string_of_proof proof);
prerr_endline (CicPp.ppterm (Inference.build_proof_term proof));
prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right));
- raise e
-;;
+ raise e
+*)
(* returns a list of all the equalities in the tree that are in relation
the position will always be Left, and if the ordering is left < right,
position will be Right.
*)
-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 =
- match mode with
- | Matching -> Index.retrieve_generalizations tree term
- | Unification -> Index.retrieve_unifiables tree term
- in
- Index.PosEqSet.elements s
+ let s =
+ match mode with
+ | Matching ->
+ let _ = <:start<retrieve_generalizations>> in
+ <:stop<retrieve_generalizations
+ Index.retrieve_generalizations tree term
+ >>
+ | Unification ->
+ let _ = <:start<retrieve_unifiables>> in
+ <:stop<retrieve_unifiables
+ Index.retrieve_unifiables tree term
+ >>
+
in
-(* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
-(* print_newline (); *)
- let t2 = Unix.gettimeofday () in
- indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
- (* make fresh instances *)
- res
+ Index.PosEqSet.elements s
;;
-
-let match_unif_time_ok = ref 0.;;
-let match_unif_time_no = ref 0.;;
-
-
(*
finds the first equality in the index that matches "term", of type "termty"
termty can be Implicit if it is not needed. The result (one of the sides of
function
| [] -> None
| candidate::tl ->
- let pos, (_, proof, (ty, left, right, o), metas) = 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");
+ 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;
+ 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 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
) else
let do_match c eq_URI =
let subst', metasenv', ugraph' =
- let t1 = Unix.gettimeofday () in
- try
- let r =
- ( 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 ->
- 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
+ Inference.matching
+ metasenv metas context term (S.lift lift_amount c) ugraph
in
- Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
+ Some (Cic.Rel (1 + lift_amount), subst', metasenv', ugraph',
(candidate, eq_URI))
in
let c, other, 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
;;
+let find_matches metasenv context ugraph lift_amount term termty =
+ find_matches metasenv context ugraph lift_amount term termty
+;;
(*
as above, but finds all the matching equalities, and the matching condition
function
| [] -> []
| candidate::tl ->
- let pos, (_, _, (ty, left, right, o), metas) = 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
- 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
- | CicUnification.UnificationFailure _
- | CicUnification.Uncertain _ as e ->
- let t2 = Unix.gettimeofday () in
- match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
- raise e
+ unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
in
- (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
- (candidate, eq_URI))
+ (C.Rel (1+lift_amount),subst',metasenv',ugraph',(candidate, eq_URI))
in
let c, other, eq_URI =
if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
lift_amount term termty tl
;;
-
+let find_all_matches
+ ?unif_fun metasenv context ugraph lift_amount term termty l
+=
+ find_all_matches
+ ?unif_fun metasenv context ugraph lift_amount term termty l
+ (*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));*)
+;;
(*
returns true if target is subsumed by some equality in table
*)
-let subsumption env table target =
- let _, _, (ty, left, right, _), tmetas = target in
+let print_res l =
+ prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
+ ((pos,equation),_)) -> Equality.string_of_equality equation)l))
+;;
+
+let subsumption_aux use_unification env table target =
+ let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality 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 metasenv = tmetas in
+ let predicate, unif_fun =
+ if use_unification then
+ Unification, Inference.unification
+ else
+ Matching, Inference.matching
in
let leftr =
match left with
- | Cic.Meta _ -> []
+ | Cic.Meta _ when not use_unification -> []
| _ ->
- let leftc = get_candidates Matching table left in
- find_all_matches ~unif_fun:Inference.matching
+ let leftc = get_candidates predicate table left in
+ find_all_matches ~unif_fun
metasenv context ugraph 0 left ty leftc
in
- let rec ok what = function
- | [] -> false, []
- | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), m)), _))::tl ->
+ let rec ok what leftorright = function
+ | [] -> 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 what' = Subst.apply_subst subst what in
+ let other' = Subst.apply_subst subst other in
let subst', menv', ug' =
- let t1 = Unix.gettimeofday () in
- try
- let r =
- 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
- with Inference.MatchingFailure as e ->
- let t2 = Unix.gettimeofday () in
- match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
- raise e
+ unif_fun metasenv m context what' other' ugraph
in
- if samesubst subst subst' then
- true, subst
- else
- ok what tl
- with Inference.MatchingFailure ->
- ok what tl
+ (match Subst.merge_subst_if_possible subst subst' with
+ | None -> ok what leftorright tl
+ | Some s -> Some (s, equation, leftorright <> pos ))
+ with
+ | Inference.MatchingFailure
+ | CicUnification.UnificationFailure _ -> ok what leftorright tl
in
- let r, subst = ok right leftr in
- let r, s =
- if r then
- true, subst
- else
+ match ok right Utils.Left leftr with
+ | Some _ as res -> res
+ | None ->
let rightr =
- 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
+ match right with
+ | Cic.Meta _ when not use_unification -> []
+ | _ ->
+ let rightc = get_candidates predicate table right in
+ find_all_matches ~unif_fun
+ metasenv context ugraph 0 right ty rightc
in
- 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)))); *)
- r, s
+ ok left Utils.Right rightr
+;;
+
+let subsumption x y z =
+ subsumption_aux false x y z
+;;
+
+let unification x y z =
+ subsumption_aux true x y z
;;
let rec demodulation_aux ?from ?(typecheck=false)
metasenv context ugraph table lift_amount term =
- (* Printf.eprintf "term = %s\n" (CicPp.ppterm 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 ~env:(metasenv,context,ugraph) Matching table term in
-(* let candidates = List.map make_variant candidates in *)
+ get_candidates
+ ~env:(metasenv,context,ugraph) (* Unification *) Matching table term
+ in
let res =
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
;;
-
-let build_newtarget_time = ref 0.;;
-
-
-let demod_counter = ref 1;;
-
exception Foo
(** demodulation, when target is an equality *)
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 = target in
+ let w, 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 order = !Utils.compare_terms left right in
- let stat = (eq_ty, left, right, order) in
- let w = Utils.compute_equality_weight stat in
- let target = w, proof, stat, metas in
+(* let right = U.guarded_simpl context right in *)
+(* let left = U.guarded_simpl context left in *)
+(* let order = !Utils.compare_terms left right 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
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))
+ ignore(check_disjoint_invariant subst menv "input2");
+ let substs = Subst.ppsubst subst in
+ ignore(check_target context (snd eq_found) ("input3" ^ substs))
end;
- let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
+ let pos, equality = eq_found in
+ let (_, proof',
+ (ty, what, other, _), menv',id') = Equality.open_equality equality 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
- incr demod_counter;
+ 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
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, []);
+ C.Appl [C.MutInd (Utils.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'),
+ (Cic.Lambda (name, ty, bo'))))))
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')
+ 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 _ ->
+ assert false, (* not implemented *)
+ (match snd proof with
+ | Equality.BasicProof _ ->
(* print_endline "replacing a BasicProof"; *)
pb
- | Inference.ProofGoalBlock (_, parent_proof) ->
-
+ | Equality.ProofGoalBlock (_, parent_proof) ->
(* print_endline "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 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 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 ->
+ try ignore(CicTypeChecker.type_of_aux'
+ newmenv context
+ (Equality.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 (Subst.ppsubst subst);
+ prerr_endline (CicPp.ppterm
+ (Equality.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;
+ prerr_endline ("+++++++++++++subst: " ^ (Subst.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 stat in
- (w, newproof, stat,newmenv) in
+ (Equality.mk_equality (w, newproof, stat,newmenv))
+ in
if Utils.debug_metas then
ignore(check_target context res "buildnew_target output");
!maxmeta, res
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
- demodulation_equality newmeta env table sign newtarget
+ 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 ?from 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 (Equality.is_weak_identity newtarget) ||
+ (Equality.meta_convertibility_eq target newtarget) then
+ newmeta, newtarget
+ else
+ demodulation_equality ?from 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
in table.
*)
-let rec betaexpand_term metasenv context ugraph table lift_amount term =
+let rec betaexpand_term
+ ?(subterms_only=false) metasenv context ugraph table lift_amount 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 Unification table term in
let res, lifted_term =
match term with
C.Implicit None, ugraph
(* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
in
+ let candidates = get_candidates Unification table term in
let r =
- find_all_matches
- metasenv context ugraph lift_amount term termty candidates
+ if subterms_only then
+ []
+ else
+ find_all_matches
+ metasenv context ugraph lift_amount term termty candidates
in
r @ res, lifted_term
;;
-
-let sup_l_counter = ref 1;;
-
-(**
- superposition_left
- 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 =
- let module C = Cic in
- let module S = CicSubstitution in
- let module M = CicMetaSubst 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
- if Utils.debug_metas then
- ignore(check_target context target "superpositionleft");
- 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
- 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') = 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 name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
- incr sup_l_counter;
- let bo'' =
- let l, r =
- if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
- C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
- S.lift 1 eq_ty; l; r]
- in
- incr maxmeta;
- let metaproof =
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context in
- C.Meta (!maxmeta, irl)
- in
- let eq_found =
- let proof' =
- let termlist =
- if pos = Utils.Left then [ty; what; other]
- else [ty; other; what]
- in
- Inference.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')
- in
- let target_proof =
- let pb =
- Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found,
- Inference.BasicProof metaproof)
- in
- match proof with
- | Inference.BasicProof _ ->
-(* debug_print (lazy "replacing a BasicProof"); *)
- pb
- | Inference.ProofGoalBlock (_, parent_proof) ->
-(* debug_print (lazy "replacing another ProofGoalBlock"); *)
- Inference.ProofGoalBlock (pb, parent_proof)
- | _ -> assert false
- in
- let refl =
- C.Appl [C.MutConstruct (* reflexivity *)
- (LibraryObjects.eq_URI (), 0, 1, []);
- eq_ty; if ordering = U.Gt then right else left]
- in
- (bo',
- 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 w = Utils.compute_equality_weight stat in
- (w, newproof, stat, newmenv)
-
- in
- !maxmeta, List.map build_new expansions
-;;
-
-
-let sup_r_counter = ref 1;;
-
(**
superposition_right
returns a list of new clauses inferred with a right superposition step
the first free meta index, i.e. the first number above the highest meta
index: its updated value is also returned
*)
-let superposition_right newmeta (metasenv, context, ugraph) table target =
+let superposition_right
+ ?(subterms_only=false) newmeta (metasenv, context, ugraph) table target
+=
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
let module CR = CicReduction in
let module U = Utils in
- let w, eqproof, (eq_ty, left, right, ordering), newmetas = target in
+ let w, eqproof, (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)
+ | U.Gt ->
+ fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
+ | U.Lt ->
+ [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
| _ ->
let res l r =
List.filter
let subst = apply_subst subst in
let o = !Utils.compare_terms (subst l) (subst r) in
o <> U.Lt && o <> U.Le)
- (fst (betaexpand_term metasenv' context ugraph table 0 l))
+ (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
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 pos, (_, proof', (ty, what, other, _), menv') = 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
- incr sup_r_counter;
+ let bo' =
+ Utils.guarded_simpl context (apply_subst s (S.subst other bo))
+ in
+ let name = C.Name "x" in
let bo'' =
let l, r =
if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
- C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
+ C.Appl [C.MutInd (Utils.eq_URI (), 0, []);
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'),(Cic.Lambda(name,ty,bo''))))
in
let newmeta, newequality =
let left, right =
let stat = (eq_ty, left, right, neworder) in
let eq' =
let w = Utils.compute_equality_weight stat in
- (w, newproof, stat, newmenv) in
+ Equality.mk_equality (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
+ 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");
+ 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 (Equality.is_identity (metasenv', context, ugraph) e) in
(!maxmeta,
(List.filter ok (new1 @ new2)))
;;
-
-(** demodulation, when the target is a goal *)
-let rec demodulation_goal newmeta env table goal =
- let module C = Cic in
- let module S = CicSubstitution in
- let module M = CicMetaSubst in
- let module HL = HelmLibraryObjects in
- let metasenv, context, ugraph = env in
- let maxmeta = ref newmeta in
- let proof, metas, term = goal in
- let term = Utils.guarded_simpl (~debug:true) context term in
- let goal = proof, metas, term in
- let metasenv' = metas in
-
- let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
- let pos, (_, proof', (ty, what, other, _), menv') = eq_found in
- let what, other = if pos = Utils.Left then what, other else other, what in
- let ty =
- try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
- with CicUtil.Meta_not_found _ -> ty
- in
- let newterm, newproof =
- 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
- incr demod_counter;
- let metaproof =
- incr maxmeta;
- 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 termlist =
- if pos = Utils.Left then [ty; what; other]
- else [ty; other; what]
- in
- Inference.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')
- in
- let goal_proof =
- let pb =
- Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
- eq_found, Inference.BasicProof metaproof)
- in
- let rec repl = function
- | Inference.NoProof ->
-(* debug_print (lazy "replacing a NoProof"); *)
- pb
- | Inference.BasicProof _ ->
-(* debug_print (lazy "replacing a BasicProof"); *)
- pb
- | Inference.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)
- | _ -> assert false
- in repl proof
- in
- bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
- 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
- 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
- else
- demodulation_goal newmeta env table newgoal
- | None ->
- newmeta, goal
-;;
-
-
(** demodulation, when the target is a theorem *)
let rec demodulation_theorem newmeta env table theorem =
let module C = Cic in
let metasenv' = metas in
let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
- let pos, (_, proof', (ty, what, other, _), menv') = 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 =
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 bo' = apply_subst subst t in *)
+(* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
+(*
+ 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)
+*)
+ (* TODO, not ported to the new proofs *)
+ if true then assert false; term, bo
in
-
- let m = Inference.metas_of_term newterm in
!maxmeta, (newterm, newty, menv)
in
let res =
| 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
newmeta, theorem
;;
+(*****************************************************************************)
+(** OPERATIONS ON GOALS **)
+(** **)
+(** DEMODULATION_GOAL & SUPERPOSITION_LEFT **)
+(*****************************************************************************)
+
+let open_goal g =
+ match g with
+ | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
+ assert (LibraryObjects.is_eq_URI uri);
+ proof,menv,eq,ty,l,r
+ | _ -> assert false
+;;
+
+let ty_of_goal (_,_,ty) = ty ;;
+
+(* checks if two goals are metaconvertible *)
+let goal_metaconvertibility_eq g1 g2 =
+ Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
+;;
+
+(* when the betaexpand_term function is called on the left/right side of the
+ * goal, the predicate has to be fixed
+ * C[x] ---> (eq ty unchanged C[x])
+ * [posu] is the side of the [unchanged] term in the original goal
+ *)
+let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
+ let _,_,eq,ty,l,r = open_goal goal in
+ let unchanged = if posu = Utils.Left then l else r in
+ let unchanged = CicSubstitution.lift 1 unchanged in
+ let ty = CicSubstitution.lift 1 ty in
+ let pred =
+ match posu with
+ | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
+ | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
+ in
+ (pred, subst, menv, ug, eq_f)
+;;
+
+(* ginve the old [goal], the side that has not changed [posu] and the
+ * expansion builds a new goal *)
+let build_newgoal context goal posu rule expansion =
+ let goalproof,_,_,_,_,_ = open_goal goal in
+ let (t,subst,menv,ug,(eq_found,eq_URI)) = fix_expansion goal posu expansion 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, newgoalproof =
+ let bo =
+ Utils.guarded_simpl context
+ (apply_subst subst (CicSubstitution.subst other t))
+ in
+ let bo' = (*apply_subst subst*) t in
+ let name = Cic.Name "x" in
+ let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
+ bo, (newgoalproofstep::goalproof)
+ in
+ let newmetasenv = (* Inference.filter subst *) menv in
+ (newgoalproof, newmetasenv, newterm)
+;;
+
+(**
+ superposition_left
+ 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 (metasenv, context, ugraph) table goal =
+ let proof,menv,eq,ty,l,r = open_goal goal in
+ let c =
+ Utils.compare_weights ~normalize:true
+ (Utils.weight_of_term l) (Utils.weight_of_term r)
+ in
+ let big,small,possmall =
+ match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left
+ in
+ let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+ List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions
+;;
+
+(** demodulation, when the target is a goal *)
+let rec demodulation_goal env table goal =
+ let goalproof,menv,_,_,left,right = open_goal goal in
+ let _, context, ugraph = env in
+(* let term = Utils.guarded_simpl (~debug:true) context term in*)
+ let do_right () =
+ let resright = demodulation_aux menv context ugraph table 0 right in
+ match resright with
+ | Some t ->
+ let newg =
+ build_newgoal context goal Utils.Left Equality.Demodulation t
+ in
+ if goal_metaconvertibility_eq goal newg then
+ false, goal
+ else
+ true, snd (demodulation_goal env table newg)
+ | None -> false, goal
+ in
+ let resleft = demodulation_aux menv context ugraph table 0 left in
+ match resleft with
+ | Some t ->
+ let newg = build_newgoal context goal Utils.Right Equality.Demodulation t in
+ if goal_metaconvertibility_eq goal newg then
+ do_right ()
+ else
+ true, snd (demodulation_goal env table newg)
+ | None -> do_right ()
+;;
+
+let get_stats () = <:show<Indexing.>> ;;
projects / helm.git / blobdiff