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) *)
+(* ;; *)
(*
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
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 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
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 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 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