From: Alberto Griggio Date: Thu, 9 Jun 2005 17:17:30 +0000 (+0000) Subject: cambiato il tipo equality, aggiunto l'ordinamento tra left e right X-Git-Tag: PRE_INDEX_1~2 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=423f3f23abfe6d5906818c26ab92d3703714057d;p=helm.git cambiato il tipo equality, aggiunto l'ordinamento tra left e right --- diff --git a/helm/ocaml/paramodulation/Makefile b/helm/ocaml/paramodulation/Makefile index 85668aaf9..c50c1b41f 100644 --- a/helm/ocaml/paramodulation/Makefile +++ b/helm/ocaml/paramodulation/Makefile @@ -5,9 +5,9 @@ TEST_REQUIRES = \ helm-tactics \ helm-cic_transformations \ helm-cic_textual_parser2 \ - helm-mathql_interpreter \ - helm-mathql_generator \ - helm-xmldiff +# helm-mathql_interpreter \ +# helm-mathql_generator \ +# helm-xmldiff # lablgtk2 \ # mathml-editor \ # lablgtkmathview \ @@ -16,12 +16,12 @@ TEST_REQUIRES = \ REQUIRES = $(TEST_REQUIRES) #gdome2-xslt helm-hbugs lablgtk2.init lablgtk2.glade OCAMLOPTIONS = \ - -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o -thread + -package "$(REQUIRES)" -predicates "$(PREDICATES)" #-pp camlp4o -thread OCAMLFIND = ocamlfind OCAMLDEBUGOPTIONS = -g OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS) OCAMLOPT = $(OCAMLFIND) ocamlopt $(OCAMLOPTIONS) -OCAMLDEP = $(OCAMLFIND) ocamldep -pp camlp4o +OCAMLDEP = $(OCAMLFIND) ocamldep #-pp camlp4o OCAMLDEBUG = wowcamldebug LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES)) diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index 4d56d30e9..00e543c2e 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -5,16 +5,17 @@ let string_of_equality ?env = match env with | None -> ( function - | _, (ty, left, right), _, _ -> - Printf.sprintf "{%s}: %s = %s" (CicPp.ppterm ty) - (CicPp.ppterm left) (CicPp.ppterm right) + | _, (ty, left, right, o), _, _ -> + Printf.sprintf "{%s}: %s =(%s) %s" (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), _, _ -> - Printf.sprintf "{%s}: %s = %s" (CicPp.pp ty names) - (CicPp.pp left names) (CicPp.pp right names) + | _, (ty, left, right, o), _, _ -> + Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.pp ty names) + (CicPp.pp left names) (string_of_comparison o) + (CicPp.pp right names) ) ;; @@ -160,8 +161,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 @@ -584,7 +585,7 @@ let beta_expand ?(metas_ok=true) ?(match_only=false) (* Printf.printf "provo a unificare %s e %s\n" *) (* (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *) if match_only then - matching metasenv context term (S.lift lift_amount what)ugraph + matching metasenv context term (S.lift lift_amount what) ugraph else CicUnification.fo_unif metasenv context (S.lift lift_amount what) term ugraph @@ -677,12 +678,13 @@ 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 *) - Cic.metasenv * (* environment for metas *) - Cic.term list (* arguments *) + 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 *) ;; @@ -719,12 +721,15 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = match head with | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri -> Printf.printf "OK: %s\n" (CicPp.ppterm term); - Some (p, (ty, t1, t2), newmetas, args), (newmeta+1) + let o = !Utils.compare_terms t1 t2 in + Some (p, (ty, t1, t2, o), newmetas, args), (newmeta+1) | _ -> None, newmeta ) | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri -> - Some (C.Rel index, - (ty, S.lift index t1, S.lift index t2), [], []), (newmeta+1) + 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) | _ -> None, newmeta in ( match do_find context term with @@ -741,7 +746,7 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof = ;; -let fix_metas newmeta ((proof, (ty, left, right), menv, args) as equality) = +let fix_metas newmeta ((proof, (ty, left, right, o), menv, args) as equality) = let table = Hashtbl.create (List.length args) in let newargs, _ = List.fold_right @@ -777,7 +782,7 @@ let fix_metas newmeta ((proof, (ty, left, right), 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), menv', newargs)) + (repl proof, (ty, left, right, o), menv', newargs)) ;; @@ -785,7 +790,8 @@ 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 -> - (proof, (ty, t1, t2), [], []) + let o = !Utils.compare_terms t1 t2 in + (proof, (ty, t1, t2, o), [], []) | _ -> raise TermIsNotAnEquality ;; @@ -802,8 +808,8 @@ let superposition_left (metasenv, context, ugraph) target source = let module CR = CicReduction in (* we assume that target is ground (does not contain metavariables): this * should always be the case (I hope, at least) *) - let proof, (eq_ty, left, right), _, _ = target in - let eqproof, (ty, t1, t2), newmetas, args = source in + let proof, (eq_ty, left, right, t_order), _, _ = target in + let eqproof, (ty, t1, t2, s_order), newmetas, args = source in let compare_terms = !Utils.compare_terms in @@ -811,7 +817,7 @@ let superposition_left (metasenv, context, ugraph) target source = [] else let where, is_left = - match compare_terms left right with + match t_order (* compare_terms left right *) with | Lt -> right, false | Gt -> left, true | _ -> ( @@ -822,7 +828,7 @@ let superposition_left (metasenv, context, ugraph) target source = ) in let metasenv' = newmetas @ metasenv in - let result = compare_terms t1 t2 in + let result = s_order (* compare_terms t1 t2 *) in let res1, res2 = match result with | Gt -> (beta_expand t1 ty where context metasenv' ugraph), [] @@ -865,10 +871,10 @@ let superposition_left (metasenv, context, ugraph) target source = | _ -> assert false in let equation = - if is_left then (eq_ty, newgoal, right) - else (eq_ty, left, newgoal) + if is_left then (eq_ty, newgoal, right, compare_terms newgoal right) + else (eq_ty, left, newgoal, compare_terms left newgoal) in - (eqproof, equation, [], []) + (newgoalproof (* eqproof *), equation, [], []) in let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1 and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in @@ -882,8 +888,8 @@ let superposition_right newmeta (metasenv, context, ugraph) target source = let module M = CicMetaSubst in let module HL = HelmLibraryObjects in let module CR = CicReduction in - let eqproof, (eq_ty, left, right), newmetas, args = target in - let eqp', (ty', t1, t2), newm', args' = source in + let eqproof, (eq_ty, left, right, t_order), newmetas, args = target in + let eqp', (ty', t1, t2, s_order), newm', args' = source in let maxmeta = ref newmeta in let compare_terms = !Utils.compare_terms in @@ -909,8 +915,8 @@ let superposition_right newmeta (metasenv, context, ugraph) target source = in let metasenv' = metasenv @ newmetas @ newm' in let beta_expand = beta_expand ~metas_ok:false in - let cmp1 = compare_terms left right - and cmp2 = compare_terms t1 t2 in + let cmp1 = t_order (* compare_terms left right *) + and cmp2 = s_order (* compare_terms t1 t2 *) in let res1, res2, res3, res4 = let res l r s t = List.filter @@ -977,8 +983,9 @@ let superposition_right newmeta (metasenv, context, ugraph) target source = let left, right = if is_left then (newterm, M.apply_subst s right) else (M.apply_subst s left, newterm) in + let neworder = compare_terms left right in fix_metas !maxmeta - (neweqproof, (eq_ty, left, right), newmetas, newargs) + (neweqproof, (eq_ty, left, right, neworder), newmetas, newargs) in maxmeta := newmeta; newequality @@ -988,15 +995,16 @@ let superposition_right newmeta (metasenv, context, ugraph) target source = and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3 and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in let ok = function - | _, (_, left, right), _, _ -> + | _, (_, left, right, _), _, _ -> not (fst (CR.are_convertible context left right ugraph)) in - !maxmeta, (List.filter ok (new1 @ new2 @ new3 @ new4)) + (!maxmeta, + (List.filter ok (new1 @ new2 @ new3 @ new4))) ;; let is_identity ((_, context, ugraph) as env) = function - | ((_, (ty, left, right), _, _) as equality) -> + | ((_, (ty, left, right, _), _, _) as equality) -> let res = (left = right || (fst (CicReduction.are_convertible context left right ugraph))) @@ -1016,8 +1024,8 @@ let demodulation newmeta (metasenv, context, ugraph) target source = let module HL = HelmLibraryObjects in let module CR = CicReduction in - let proof, (eq_ty, left, right), metas, args = target - and proof', (ty, t1, t2), metas', args' = source in + let proof, (eq_ty, left, right, t_order), metas, args = target + and proof', (ty, t1, t2, s_order), metas', args' = source in let compare_terms = !Utils.compare_terms in @@ -1025,7 +1033,7 @@ let demodulation newmeta (metasenv, context, ugraph) target source = newmeta, target else let first_step, get_params = - match compare_terms t1 t2 with + match s_order (* compare_terms t1 t2 *) with | Gt -> 1, (function | 1 -> true, t1, t2, HL.Logic.eq_ind_URI | 0 -> false, t1, t2, HL.Logic.eq_ind_URI @@ -1047,7 +1055,7 @@ let demodulation newmeta (metasenv, context, ugraph) target source = first_step, get_params in let rec demodulate newmeta step metasenv target = - let proof, (eq_ty, left, right), metas, args = target in + let proof, (eq_ty, left, right, t_order), metas, args = target in let is_left, what, other, eq_URI = get_params step in let env = metasenv, context, ugraph in @@ -1116,6 +1124,7 @@ let demodulation newmeta (metasenv, context, ugraph) target source = if is_left then newterm, right else left, newterm in + let neworder = compare_terms left right in (* let newmetasenv = metasenv @ metas in *) (* let newargs = args @ args' in *) (* fix_metas newmeta *) @@ -1127,7 +1136,8 @@ let demodulation newmeta (metasenv, context, ugraph) target source = (function C.Meta (i, _) -> List.mem i m | _ -> assert false) args in - newmeta, (newproof, (eq_ty, left, right), newmetasenv, newargs) + newmeta, + (newproof, (eq_ty, left, right, neworder), newmetasenv, newargs) in (* Printf.printf *) (* "demodulate, newtarget: %s\ntarget was: %s\n" *) @@ -1155,8 +1165,8 @@ let demodulation newmeta env target source = let subsumption env target source = - let _, (ty, tl, tr), tmetas, _ = target - and _, (ty', sl, sr), smetas, _ = source in + let _, (ty, tl, tr, _), tmetas, _ = target + and _, (ty', sl, sr, _), smetas, _ = source in if ty <> ty' then false else diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli index fab2026ad..0cc0fcb70 100644 --- a/helm/ocaml/paramodulation/inference.mli +++ b/helm/ocaml/paramodulation/inference.mli @@ -1,15 +1,24 @@ type equality = - Cic.term * (* proof *) - (Cic.term * (* type *) - Cic.term * (* left side *) - Cic.term) * (* right side *) - Cic.metasenv * (* environment for metas *) - Cic.term list (* arguments *) + 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 *) ;; type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;; +exception MatchingFailure + +val matching: + Cic.metasenv -> Cic.context -> Cic.term -> Cic.term -> + CicUniv.universe_graph -> + Cic.substitution * Cic.metasenv * CicUniv.universe_graph + + (** Performs the beta expansion of the term "where" w.r.t. "what", i.e. returns the list of all the terms t s.t. "(t what) = where". @@ -66,3 +75,7 @@ val is_identity: environment -> equality -> bool val string_of_equality: ?env:environment -> equality -> string val subsumption: environment -> equality -> equality -> bool + +val metas_of_term: Cic.term -> int list + +val fix_metas: int -> equality -> int * equality diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 4c1480d10..5f9ffe335 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -7,21 +7,13 @@ type result = ;; -type equality_sign = Negative | Positive;; - -let string_of_sign = function - | Negative -> "Negative" - | Positive -> "Positive" -;; - - (* let symbols_of_equality (_, (_, left, right), _, _) = TermSet.union (symbols_of_term left) (symbols_of_term right) ;; *) -let symbols_of_equality ((_, (_, left, right), _, _) as equality) = +let symbols_of_equality ((_, (_, left, right, _), _, _) as equality) = let m1 = symbols_of_term left in let m = TermMap.fold @@ -49,8 +41,8 @@ struct match meta_convertibility_eq eq1 eq2 with | true -> 0 | false -> - let _, (ty, left, right), _, _ = eq1 - and _, (ty', left', right'), _, _ = eq2 in + let _, (ty, left, right, _), _, _ = eq1 + and _, (ty', left', right', _), _, _ = eq2 in let weight_of t = fst (weight_of_term ~consider_metas:false t) in let w1 = (weight_of ty) + (weight_of left) + (weight_of right) and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in @@ -234,7 +226,7 @@ let contains_empty env (negative, positive) = try let (proof, _, _, _) = List.find - (fun (proof, (ty, left, right), m, a) -> + (fun (proof, (ty, left, right, ordering), m, a) -> fst (CicReduction.are_convertible context left right ugraph)) negative in @@ -663,24 +655,18 @@ let main () = let env = (metasenv, context, ugraph) in try let term_equality = equality_of_term meta_proof goal in - let meta_proof, (eq_ty, left, right), _, _ = term_equality in + let meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in let active = [] in let passive = make_passive [term_equality] equalities in - Printf.printf "\ncurrent goal: %s ={%s} %s\n" - (PP.ppterm left) (PP.ppterm eq_ty) (PP.ppterm right); + Printf.printf "\ncurrent goal: %s\n" + (string_of_equality ~env term_equality); Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context); Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv); - Printf.printf "\nequalities:\n"; - List.iter - (function (_, (ty, t1, t2), _, _) -> - let w1 = weight_of_term t1 in - let w2 = weight_of_term t2 in - let res = !compare_terms t1 t2 in - Printf.printf "{%s}: %s<%s> %s %s<%s>\n" (PP.ppterm ty) - (PP.ppterm t1) (string_of_weight w1) - (string_of_comparison res) - (PP.ppterm t2) (string_of_weight w2)) - equalities; + Printf.printf "\nequalities:\n%s\n" + (String.concat "\n" + (List.map + (string_of_equality ~env) + equalities)); print_endline "--------------------------------------------------"; let start = Unix.gettimeofday () in print_endline "GO!"; diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml index b0aa00e89..4a20f5c3d 100644 --- a/helm/ocaml/paramodulation/utils.ml +++ b/helm/ocaml/paramodulation/utils.ml @@ -397,3 +397,12 @@ let rec lpo t1 t2 = (* settable by the user... *) let compare_terms = ref nonrec_kbo;; + + +type equality_sign = Negative | Positive;; + +let string_of_sign = function + | Negative -> "Negative" + | Positive -> "Positive" +;; + diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli index 1adf90e50..295d1aa4d 100644 --- a/helm/ocaml/paramodulation/utils.mli +++ b/helm/ocaml/paramodulation/utils.mli @@ -31,3 +31,8 @@ val lpo: Cic.term -> Cic.term -> comparison (** term-ordering function settable by the user *) val compare_terms: (Cic.term -> Cic.term -> comparison) ref + +type equality_sign = Negative | Positive + +val string_of_sign: equality_sign -> string +