X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Finference.ml;h=38bc6abe54ca24196cfdfcf40bee65db1ce9eefd;hb=904ecbd458b20b47d250889459f9aa9ebd26d04d;hp=fad86a854aeec9f7db327e70ba0dfec5cee78de8;hpb=e61d023695578ebf09d487480e6e7cac3a2dd2ee;p=helm.git diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index fad86a854..38bc6abe5 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -12,13 +12,15 @@ type equality = 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) * equality - | NoProof + (Utils.pos * equality) * proof + | ProofGoalBlock of proof * equality + | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof ;; @@ -41,33 +43,108 @@ let string_of_equality ?env = ;; -let rec build_term_proof equality = +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 - match proof with - | NoProof -> - Printf.fprintf stderr "WARNING: no proof for %s\n" - (string_of_equality equality); - Cic.Implicit None - | BasicProof term -> term - | ProofBlock (subst, eq_URI, t', (pos, eq), eq') -> - 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 proof' = build_term_proof eq in - let eqproof = build_term_proof eq' in - 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']) + do_build_proof proof ;; @@ -493,9 +570,10 @@ let unification metasenv context t1 t2 ugraph = 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;; @@ -996,18 +1074,10 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = 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 @@ -1048,16 +1118,24 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = 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 @@ -1082,8 +1160,60 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) = List.filter (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs in - (newmeta + (List.length newargs) + 1, - (w, p, (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)) *) ;;