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