X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Finference.ml;h=62308896fd02b6b89bb420bd9c2c501c99273e54;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=d8ff4a7d9d116537f963b222f92da5da379c62d0;hpb=bbe7741f3bbaacb93f2876c018dace82f5e929b8;p=helm.git diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index d8ff4a7d9..62308896f 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -1,25 +1,76 @@ 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 = + | 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 +;; + + 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 rec build_term_proof equality = +(* Printf.printf "build_term_proof %s" (string_of_equality equality); *) +(* print_newline (); *) + 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']) +;; + + let rec metas_of_term = function | Cic.Meta (i, c) -> [i] | Cic.Var (_, ens) @@ -161,8 +212,8 @@ let meta_convertibility_aux table t1 t2 = 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 @@ -933,17 +984,6 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) ;; -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 @@ -956,18 +996,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 @@ -978,14 +1010,19 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = | 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 @@ -1002,7 +1039,7 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = ;; -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) = let table = Hashtbl.create (List.length args) in let newargs, _ = List.fold_right @@ -1038,7 +1075,7 @@ let fix_metas newmeta ((proof, (ty, left, right, o), menv, args) as equality) = (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)) + (w, p, (ty, left, right, o), menv', newargs)) ;; @@ -1047,7 +1084,10 @@ exception TermIsNotAnEquality;; 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 ;; @@ -1056,6 +1096,7 @@ let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function 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 @@ -1257,22 +1298,17 @@ let superposition_right newmeta (metasenv, context, ugraph) target source = (!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 @@ -1470,6 +1506,7 @@ let subsumption env target source = ); res ;; +*) let extract_differing_subterms t1 t2 =