open Utils;;
+type equality =
+ int * (* weight *)
+ proof *
+ (Cic.term * (* type *)
+ Cic.term * (* left side *)
+ Cic.term * (* right side *)
+ Utils.comparison) * (* ordering *)
+ Cic.metasenv * (* environment for metas *)
+ Cic.term list (* arguments *)
+
+and proof =
+ | NoProof
+ | BasicProof of Cic.term
+ | ProofBlock of
+ Cic.substitution * UriManager.uri *
+ (* name, ty, eq_ty, left, right *)
+ (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) *
+ (Utils.pos * equality) * proof
+ | ProofGoalBlock of proof * equality
+ | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof
+;;
+
+
let string_of_equality ?env =
match env with
| None -> (
function
- | _, (ty, left, right, o), _, _ ->
- Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.ppterm ty)
+ | w, _, (ty, left, right, o), _, _ ->
+ Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.ppterm ty)
(CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right)
)
| Some (_, context, _) -> (
let names = names_of_context context in
function
- | _, (ty, left, right, o), _, _ ->
- Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.pp ty names)
+ | w, _, (ty, left, right, o), _, _ ->
+ Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.pp ty names)
(CicPp.pp left names) (string_of_comparison o)
(CicPp.pp right names)
)
;;
+let build_proof_term equality =
+(* Printf.printf "build_term_proof %s" (string_of_equality equality); *)
+(* print_newline (); *)
+
+ let indent = ref 0 in
+
+ let rec do_build_proof proof =
+ match proof with
+ | NoProof ->
+ Printf.fprintf stderr "WARNING: no proof!\n";
+(* (string_of_equality equality); *)
+ Cic.Implicit None
+ | BasicProof term -> term
+ | ProofGoalBlock (proofbit, equality) ->
+ print_endline "found ProofGoalBlock, going up...";
+ let _, proof, _, _, _ = equality in
+ do_build_goal_proof proofbit proof
+ | ProofSymBlock (ens, proof) ->
+ let proof = do_build_proof proof in
+ Cic.Appl [
+ Cic.Const (HelmLibraryObjects.Logic.sym_eq_URI, ens); (* symmetry *)
+ proof
+ ]
+ | ProofBlock (subst, eq_URI, t', (pos, eq), eqproof) ->
+(* Printf.printf "\nsubst:\n%s\n" (print_subst subst); *)
+(* print_newline (); *)
+
+ let name, ty, eq_ty, left, right = t' in
+ let bo =
+ Cic.Appl [Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
+ eq_ty; left; right]
+ in
+ let t' = Cic.Lambda (name, ty, (* CicSubstitution.lift 1 *) bo) in
+ (* Printf.printf " ProofBlock: eq = %s, eq' = %s" *)
+ (* (string_of_equality eq) (string_of_equality eq'); *)
+ (* print_newline (); *)
+
+(* let s = String.make !indent ' ' in *)
+(* incr indent; *)
+
+(* print_endline (s ^ "build proof'------------"); *)
+
+ let proof' =
+ let _, proof', _, _, _ = eq in
+ do_build_proof proof'
+ in
+(* print_endline (s ^ "END proof'"); *)
+
+(* print_endline (s ^ "build eqproof-----------"); *)
+
+ let eqproof = do_build_proof eqproof in
+
+(* print_endline (s ^ "END eqproof"); *)
+(* decr indent; *)
+
+
+ let _, _, (ty, what, other, _), menv', args' = eq in
+ let what, other =
+ if pos = Utils.Left then what, other else other, what
+ in
+ CicMetaSubst.apply_subst subst
+ (Cic.Appl [Cic.Const (eq_URI, []); ty;
+ what; t'; eqproof; other; proof'])
+
+ and do_build_goal_proof proofbit proof =
+(* match proofbit with *)
+(* | BasicProof _ -> do_build_proof proof *)
+(* | proofbit -> *)
+ match proof with
+ | ProofGoalBlock (pb, eq) ->
+ do_build_proof (ProofGoalBlock (replace_proof proofbit pb, eq))
+(* let _, proof, _, _, _ = eq in *)
+(* let newproof = replace_proof proofbit proof in *)
+(* do_build_proof newproof *)
+
+(* | ProofBlock (subst, eq_URI, t', poseq, eqproof) -> *)
+(* let eqproof' = replace_proof proofbit eqproof in *)
+(* do_build_proof (ProofBlock (subst, eq_URI, t', poseq, eqproof')) *)
+ | _ -> do_build_proof (replace_proof proofbit proof) (* assert false *)
+
+ and replace_proof newproof = function
+ | ProofBlock (subst, eq_URI, t', poseq, eqproof) ->
+ let uri = eq_URI in
+(* if eq_URI = HelmLibraryObjects.Logic.eq_ind_URI then *)
+(* HelmLibraryObjects.Logic.eq_ind_r_URI *)
+(* else *)
+(* HelmLibraryObjects.Logic.eq_ind_URI *)
+(* in *)
+ let eqproof' = replace_proof newproof eqproof in
+ ProofBlock (subst, uri(* eq_URI *), t', poseq, eqproof')
+(* ProofBlock (subst, eq_URI, t', poseq, newproof) *)
+ | ProofGoalBlock (pb, equality) ->
+ let pb' = replace_proof newproof pb in
+ ProofGoalBlock (pb', equality)
+(* let w, proof, t, menv, args = equality in *)
+(* let proof' = replace_proof newproof proof in *)
+(* ProofGoalBlock (pb, (w, proof', t, menv, args)) *)
+ | BasicProof _ -> newproof
+ | p -> p
+ in
+ let _, proof, _, _, _ = equality in
+ do_build_proof proof
+;;
+
+
let rec metas_of_term = function
| Cic.Meta (i, c) -> [i]
| Cic.Var (_, ens)
let meta_convertibility_eq eq1 eq2 =
- let _, (ty, left, right, _), _, _ = eq1
- and _, (ty', left', right', _), _, _ = eq2 in
+ let _, _, (ty, left, right, _), _, _ = eq1
+ and _, _, (ty', left', right', _), _, _ = eq2 in
if ty <> ty' then
false
else if (left = left') && (right = right') then
in
(* Printf.printf "| subst: %s\n" (print_subst ~prefix:" ; " subst); *)
(* print_endline "|"; *)
- (* fix_subst *) subst, menv, ug
+ fix_subst subst, menv, ug
;;
+
(* let unification = CicUnification.fo_unif;; *)
exception MatchingFailure;;
;;
-type equality =
- Cic.term * (* proof *)
- (Cic.term * (* type *)
- Cic.term * (* left side *)
- Cic.term * (* right side *)
- Utils.comparison) * (* ordering *)
- Cic.metasenv * (* environment for metas *)
- Cic.term list (* arguments *)
-;;
-
-
let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
let module C = Cic in
let module S = CicSubstitution in
match term with
| C.Prod (name, s, t) ->
(* let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
- let (head, newmetas, args, _) =
- PrimitiveTactics.new_metasenv_for_apply newmeta proof
+ let (head, newmetas, args, newmeta) =
+ ProofEngineHelpers.saturate_term newmeta []
context (S.lift index term)
in
- let newmeta =
- List.fold_left
- (fun maxm arg ->
- match arg with
- | C.Meta (i, _) -> (max maxm i)
- | _ -> assert false)
- newmeta args
- in
let p =
if List.length args = 0 then
C.Rel index
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
Printf.printf "OK: %s\n" (CicPp.ppterm term);
let o = !Utils.compare_terms t1 t2 in
- Some (p, (ty, t1, t2, o), newmetas, args), (newmeta+1)
+ let w = compute_equality_weight ty t1 t2 in
+ let proof = BasicProof p in
+ let e = (w, proof, (ty, t1, t2, o), newmetas, args) in
+ Some e, (newmeta+1)
| _ -> None, newmeta
)
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
let t1 = S.lift index t1
and t2 = S.lift index t2 in
let o = !Utils.compare_terms t1 t2 in
- Some (C.Rel index, (ty, t1, t2, o), [], []), (newmeta+1)
+ let w = compute_equality_weight ty t1 t2 in
+ let e = (w, BasicProof (C.Rel index), (ty, t1, t2, o), [], []) in
+ Some e, (newmeta+1)
| _ -> None, newmeta
in (
match do_find context term with
;;
-let fix_metas newmeta ((proof, (ty, left, right, o), menv, args) as equality) =
+let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
+(* print_endline ("fix_metas " ^ (string_of_int newmeta)); *)
let table = Hashtbl.create (List.length args) in
- let newargs, _ =
+ let is_this_case = ref false in
+ let newargs, newmeta =
List.fold_right
(fun t (newargs, index) ->
match t with
| Cic.Meta (i, l) ->
Hashtbl.add table i index;
+(* if index = 5469 then ( *)
+(* Printf.printf "?5469 COMES FROM (%d): %s\n" *)
+(* i (string_of_equality equality); *)
+(* print_newline (); *)
+(* is_this_case := true *)
+(* ); *)
((Cic.Meta (index, l))::newargs, index+1)
| _ -> assert false)
- args ([], newmeta)
+ args ([], newmeta+1)
in
let repl where =
ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
List.filter
(function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
in
- (newmeta + (List.length newargs) + 1,
- (repl proof, (ty, left, right, o), menv', newargs))
+ let rec fix_proof = function
+ | NoProof -> NoProof
+ | BasicProof term -> BasicProof (repl term)
+ | ProofBlock (subst, eq_URI, t', (pos, eq), p) ->
+
+(* Printf.printf "fix_proof of equality %s, subst is:\n%s\n" *)
+(* (string_of_equality equality) (print_subst subst); *)
+
+ let subst' =
+ List.fold_left
+ (fun s arg ->
+ match arg with
+ | Cic.Meta (i, l) -> (
+ try
+ let j = Hashtbl.find table i in
+ if List.mem_assoc i subst then
+ s
+ else
+(* let _, context, ty = CicUtil.lookup_meta j menv' in *)
+(* (i, (context, Cic.Meta (j, l), ty))::s *)
+ let _, context, ty = CicUtil.lookup_meta i menv in
+ (i, (context, Cic.Meta (j, l), ty))::s
+ with _ -> s
+ )
+ | _ -> assert false)
+ [] args
+ in
+(* let subst'' = *)
+(* List.map *)
+(* (fun (i, e) -> *)
+(* try let j = Hashtbl.find table i in (j, e) *)
+(* with _ -> (i, e)) subst *)
+(* in *)
+
+(* Printf.printf "subst' is:\n%s\n" (print_subst subst'); *)
+(* print_newline (); *)
+
+ ProofBlock (subst' @ subst, eq_URI, t', (pos, eq), p)
+(* | ProofSymBlock (ens, p) -> *)
+(* let ens' = List.map (fun (u, t) -> (u, repl t)) ens in *)
+(* ProofSymBlock (ens', fix_proof p) *)
+ | p -> assert false
+ in
+(* (newmeta + (List.length newargs) + 2, *)
+ let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in
+(* if !is_this_case then ( *)
+(* print_endline "\nTHIS IS THE TROUBLE!!!"; *)
+(* let pt = build_proof_term neweq in *)
+(* Printf.printf "equality: %s\nproof: %s\n" *)
+(* (string_of_equality neweq) (CicPp.ppterm pt); *)
+(* print_endline (String.make 79 '-'); *)
+(* ); *)
+ (newmeta + 1, neweq)
+(* (w, fix_proof p, (ty, left, right, o), menv', newargs)) *)
;;
let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
| Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
let o = !Utils.compare_terms t1 t2 in
- (proof, (ty, t1, t2, o), [], [])
+ let w = compute_equality_weight ty t1 t2 in
+ let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in
+ e
+(* (proof, (ty, t1, t2, o), [], []) *)
| _ ->
raise TermIsNotAnEquality
;;
type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
+(*
let superposition_left (metasenv, context, ugraph) target source =
let module C = Cic in
let module S = CicSubstitution in
(!maxmeta,
(List.filter ok (new1 @ new2 @ new3 @ new4)))
;;
+*)
let is_identity ((_, context, ugraph) as env) = function
- | ((_, (ty, left, right, _), _, _) as equality) ->
- let res =
- (left = right ||
- (fst (CicReduction.are_convertible context left right ugraph)))
- in
-(* if res then ( *)
-(* Printf.printf "is_identity: %s" (string_of_equality ~env equality); *)
-(* print_newline (); *)
-(* ); *)
- res
+ | ((_, _, (ty, left, right, _), _, _) as equality) ->
+ (left = right ||
+ (fst (CicReduction.are_convertible context left right ugraph)))
;;
+(*
let demodulation newmeta (metasenv, context, ugraph) target source =
let module C = Cic in
let module S = CicSubstitution in
);
res
;;
+*)
let extract_differing_subterms t1 t2 =
projects / helm.git / blobdiff