let apply_subst = CicMetaSubst.apply_subst
-(* Profiling code
-let apply_subst =
- let profile = CicUtil.profile "apply_subst" in
- (fun s a -> profile.profile (apply_subst s) a)
-;;
-*)
+(* let apply_subst = *)
+(* let profile = CicUtil.profile "apply_subst" in *)
+(* (fun s a -> profile (apply_subst s) a) *)
+(* ;; *)
(*
(* DISCRIMINATION TREES *)
+let init_index () =
+ Hashtbl.clear Discrimination_tree.arities;
+;;
+
let empty_table () =
Discrimination_tree.DiscriminationTree.empty
;;
(candidate, eq_URI))
in
let c, other, eq_URI =
- if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
- else right, left, HL.Logic.eq_ind_r_URI
+ if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
+ else right, left, Utils.eq_ind_r_URI ()
in
if o <> U.Incomparable then
try
and other' = (* M. *)apply_subst s other in
let order = cmp c' other' in
let names = U.names_of_context context in
+(* let _ = *)
+(* debug_print *)
+(* (Printf.sprintf "OK matching: %s and %s, order: %s" *)
+(* (CicPp.ppterm c') *)
+(* (CicPp.ppterm other') *)
+(* (Utils.string_of_comparison order)); *)
+(* debug_print *)
+(* (Printf.sprintf "subst:\n%s\n" (Utils.print_subst s)) *)
+(* in *)
if order = U.Gt then
res
else
(candidate, eq_URI))
in
let c, other, eq_URI =
- if pos = Utils.Left then left, right, HL.Logic.eq_ind_URI
- else right, left, HL.Logic.eq_ind_r_URI
+ if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
+ else right, left, Utils.eq_ind_r_URI ()
in
if o <> U.Incomparable then
try
find_all_matches ~unif_fun:Inference.matching
metasenv context ugraph 0 left ty leftc
in
- let ok what (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), _, _)), _)) =
- try
- let other = if pos = Utils.Left then r else l in
- let subst', menv', ug' =
- let t1 = Unix.gettimeofday () in
+ let rec ok what = function
+ | [] -> false, []
+ | (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), _, _)), _))::tl ->
try
- let r =
- Inference.matching metasenv 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
- in
- samesubst subst subst'
- with Inference.MatchingFailure ->
- false
+ 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 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
+ in
+ if samesubst subst subst' then
+ true, subst
+ else
+ ok what tl
+ with Inference.MatchingFailure ->
+ ok what tl
in
- let r = List.exists (ok right) leftr in
+ let r, subst = ok right leftr in
if r then
- true
+ true, subst
else
let rightr =
match right with
find_all_matches ~unif_fun:Inference.matching
metasenv context ugraph 0 right ty rightc
in
- List.exists (ok left) rightr
+ ok left rightr
;;
-let rec demodulate_term metasenv context ugraph table lift_amount term =
+let rec demodulation_aux metasenv context ugraph table lift_amount term =
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
(res, tl @ [S.lift 1 t])
else
let r =
- demodulate_term metasenv context ugraph table
+ demodulation_aux metasenv context ugraph table
lift_amount t
in
match r with
)
| C.Prod (nn, s, t) ->
let r1 =
- demodulate_term metasenv context ugraph table lift_amount s in (
+ demodulation_aux metasenv context ugraph table lift_amount s in (
match r1 with
| None ->
let r2 =
- demodulate_term metasenv
+ demodulation_aux metasenv
((Some (nn, C.Decl s))::context) ugraph
table (lift_amount+1) t
in (
)
| C.Lambda (nn, s, t) ->
let r1 =
- demodulate_term metasenv context ugraph table lift_amount s in (
+ demodulation_aux metasenv context ugraph table lift_amount s in (
match r1 with
| None ->
let r2 =
- demodulate_term metasenv
+ demodulation_aux metasenv
((Some (nn, C.Decl s))::context) ugraph
table (lift_amount+1) t
in (
;;
-let build_ens_for_sym_eq ty x y =
- [(UriManager.uri_of_string
- "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var", ty);
- (UriManager.uri_of_string
- "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var", x);
- (UriManager.uri_of_string
- "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var", y)]
-;;
-
-
let build_newtarget_time = ref 0.;;
let demod_counter = ref 1;;
-let rec demodulation newmeta env table sign target =
+let rec demodulation_equality newmeta env table sign target =
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst 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 (HelmLibraryObjects.Logic.eq_URI, 0, []);
+ C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
S.lift 1 eq_ty; l; r]
in
if sign = Utils.Positive then
(* let target' = *)
let eq_found =
let proof' =
- let ens =
- if pos = Utils.Left then
- build_ens_for_sym_eq ty what other
- else
- build_ens_for_sym_eq ty other what
+(* let ens = *)
+(* if pos = Utils.Left then *)
+(* build_ens_for_sym_eq ty what other *)
+(* else *)
+(* build_ens_for_sym_eq ty other what *)
+ let termlist =
+ if pos = Utils.Left then [ty; what; other]
+ else [ty; other; what]
in
- Inference.ProofSymBlock (ens, proof')
+ Inference.ProofSymBlock (termlist, proof')
in
let what, other =
if pos = Utils.Left then what, other else other, what
(* in *)
let refl =
C.Appl [C.MutConstruct (* reflexivity *)
- (HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
+ (LibraryObjects.eq_URI (), 0, 1, []);
eq_ty; if is_left then right else left]
in
(bo,
in
!maxmeta, res
in
- let res = demodulate_term metasenv' context ugraph table 0 left in
+ let res = demodulation_aux metasenv' context ugraph table 0 left in
match res with
| Some t ->
let newmeta, newtarget = build_newtarget true t in
(* if subsumption env table newtarget then *)
(* newmeta, build_identity newtarget *)
(* else *)
- demodulation newmeta env table sign newtarget
+ demodulation_equality newmeta env table sign newtarget
| None ->
- let res = demodulate_term metasenv' context ugraph table 0 right in
+ 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 subsumption env table newtarget then *)
(* newmeta, build_identity newtarget *)
(* else *)
- demodulation newmeta env table sign newtarget
+ demodulation_equality newmeta env table sign newtarget
| None ->
newmeta, target
;;
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 (HL.Logic.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
incr maxmeta;
let metaproof =
(* let target' = *)
let eq_found =
let proof' =
- let ens =
- if pos = Utils.Left then
- build_ens_for_sym_eq ty what other
- else
- build_ens_for_sym_eq ty other what
+(* let ens = *)
+(* if pos = Utils.Left then *)
+(* build_ens_for_sym_eq ty what other *)
+(* else *)
+(* build_ens_for_sym_eq ty other what *)
+(* in *)
+ let termlist =
+ if pos = Utils.Left then [ty; what; other]
+ else [ty; other; what]
in
- Inference.ProofSymBlock (ens, proof')
+ Inference.ProofSymBlock (termlist, proof')
in
let what, other =
if pos = Utils.Left then what, other else other, what
(* in *)
let refl =
C.Appl [C.MutConstruct (* reflexivity *)
- (HelmLibraryObjects.Logic.eq_URI, 0, 1, []);
+ (LibraryObjects.eq_URI (), 0, 1, []);
eq_ty; if ordering = U.Gt then right else left]
in
(bo',
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 (HL.Logic.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
bo',
Inference.ProofBlock (
(* | _, _, (_, left, right, _), _, _ -> *)
(* not (fst (CR.are_convertible context left right ugraph)) *)
(* in *)
+ let _ =
+ let env = metasenv, context, ugraph in
+ debug_print
+ (lazy
+ (Printf.sprintf "end of superposition_right:\n%s\n"
+ (String.concat "\n"
+ ((List.map
+ (fun e -> "Positive " ^
+ (Inference.string_of_equality ~env e)) (new1 @ new2))))))
+ in
let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in
(!maxmeta,
(List.filter ok (new1 @ new2)))
let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
let what, other = if pos = Utils.Left then what, other else other, what in
+ let ty =
+ try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
+ with CicUtil.Meta_not_found _ -> ty
+ in
let newterm, newproof =
let bo = (* M. *)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 =
in
let eq_found =
let proof' =
- let ens =
- if pos = Utils.Left then build_ens_for_sym_eq ty what other
- else build_ens_for_sym_eq ty other what
+(* let ens = *)
+(* if pos = Utils.Left then build_ens_for_sym_eq ty what other *)
+(* else build_ens_for_sym_eq ty other what *)
+(* in *)
+ let termlist =
+ if pos = Utils.Left then [ty; what; other]
+ else [ty; other; what]
in
- Inference.ProofSymBlock (ens, proof')
+ Inference.ProofSymBlock (termlist, proof')
in
let what, other =
if pos = Utils.Left then what, other else other, what
in
let goal_proof =
let pb =
- Inference.ProofBlock (subst, eq_URI, (name, ty), bo,
+ Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
eq_found, Inference.BasicProof metaproof)
in
- match proof with
- | 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)
- | _ -> assert false
+ 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) as subproof) ->
+ debug_print
+ (lazy
+ (Printf.sprintf "replacing %s"
+ (Inference.string_of_proof subproof)));
+ Inference.SubProof (term, meta_index, repl p)
+ | _ -> assert false
+ in repl proof
in
bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
in
let m = Inference.metas_of_term newterm in
let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
!maxmeta, (newproof, newmetasenv, newterm)
- in
-
- let res = demodulate_term metasenv' context ugraph table 0 term in
+ in
+ let res = demodulation_aux metasenv' context ugraph table 0 term in
match res with
| Some t ->
let newmeta, newgoal = build_newgoal t in
| None ->
newmeta, goal
;;
+
+
+let rec demodulation_theorem newmeta env table theorem =
+ 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 = theorem in
+ let term, termty, metas = theorem in
+ let metasenv' = metasenv @ metas in
+
+ let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
+ let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
+ let what, other = if pos = Utils.Left then what, other else other, what in
+ let newterm, newty =
+ let bo = 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)
+ in
+ (Inference.build_proof_term newproof, bo)
+ in
+ let m = Inference.metas_of_term newterm in
+ let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
+ !maxmeta, (newterm, newty, newmetasenv)
+ in
+ let res = demodulation_aux 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
+ newmeta, newthm
+ else
+ demodulation_theorem newmeta env table newthm
+ | None ->
+ newmeta, theorem
+;;
projects / helm.git / blobdiff