From: Enrico Tassi Date: Tue, 9 Jun 2009 15:09:42 +0000 (+0000) Subject: snapshot X-Git-Tag: make_still_working~3894 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=01b628fc79155f545b283c1d095d8a2ffe00e0a1;p=helm.git snapshot --- diff --git a/helm/software/components/ng_paramodulation/foSubst.ml b/helm/software/components/ng_paramodulation/foSubst.ml index bfef2f2b1..9053ec223 100644 --- a/helm/software/components/ng_paramodulation/foSubst.ml +++ b/helm/software/components/ng_paramodulation/foSubst.ml @@ -38,7 +38,10 @@ module Subst (B : Terms.Blob) = struct let rec apply_subst subst = function | (Terms.Leaf _) as t -> t - | Terms.Var i -> lookup_subst i subst + | Terms.Var i -> + (match lookup_subst i subst with + | Terms.Node _ as t -> apply_subst subst t + | t -> t) | (Terms.Node l) -> Terms.Node (List.map (fun t -> apply_subst subst t) l) ;; diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml index d53b19c82..624b6c99c 100644 --- a/helm/software/components/ng_paramodulation/foUtils.ml +++ b/helm/software/components/ng_paramodulation/foUtils.ml @@ -11,6 +11,15 @@ (* $Id: terms.ml 9836 2009-06-05 15:33:35Z denes $ *) +let rec lexicograph f l1 l2 = + match l1, l2 with + | [], [] -> 0 + | x::xs, y::ys -> + let c = f x y in + if c <> 0 then c else lexicograph f xs ys + | [],_ -> ~-1 + | _,[] -> 1 +;; module Utils (B : Terms.Blob) = struct module Subst = FoSubst.Subst(B) ;; @@ -25,15 +34,6 @@ module Utils (B : Terms.Blob) = struct | _ -> false ;; - let rec lexicograph f l1 l2 = - match l1, l2 with - | [], [] -> 0 - | x::xs, y::ys -> - let c = f x y in - if c <> 0 then c else lexicograph f xs ys - | [],_ -> ~-1 - | _,[] -> 1 - ;; let rec compare_foterm x y = match x, y with @@ -127,12 +127,10 @@ module Utils (B : Terms.Blob) = struct fresh_unit_clause maxvar (mk_id (), lit, varlist, proof) ;; - let add_to_bag = - let id = ref 0 in - fun bag (_,lit,vl,proof) -> - incr id; - let clause = (!id, lit, vl, proof) in - let bag = Terms.M.add !id clause bag in + let add_to_bag bag (_,lit,vl,proof) = + let id = mk_id () in + let clause = (id, lit, vl, proof) in + let bag = Terms.M.add id clause bag in bag, clause ;; diff --git a/helm/software/components/ng_paramodulation/foUtils.mli b/helm/software/components/ng_paramodulation/foUtils.mli index 4cddee8c1..d78ce32f2 100644 --- a/helm/software/components/ng_paramodulation/foUtils.mli +++ b/helm/software/components/ng_paramodulation/foUtils.mli @@ -11,6 +11,8 @@ (* $Id: terms.ml 9836 2009-06-05 15:33:35Z denes $ *) +val lexicograph : ('a -> 'b -> int) -> 'a list -> 'b list -> int + module Utils (B : Terms.Blob) : sig val eq_foterm : B.t Terms.foterm -> B.t Terms.foterm -> bool diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml index 7cd4e5762..09399b326 100644 --- a/helm/software/components/ng_paramodulation/nCicBlob.ml +++ b/helm/software/components/ng_paramodulation/nCicBlob.ml @@ -27,10 +27,22 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct let rec compare x y = match x,y with | NCic.Rel i, NCic.Rel j -> i-j + | NCic.Meta (i,_), NCic.Meta (j,_) -> i-j | NCic.Const r1, NCic.Const r2 -> NReference.compare r1 r2 - | NCic.Appl l1, NCic.Appl l2 -> assert false (* TODO *) + | NCic.Appl l1, NCic.Appl l2 -> FoUtils.lexicograph compare l1 l2 + | NCic.Rel _, ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ) -> ~-1 + | ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ), NCic.Rel _ -> 1 + | NCic.Const _, ( NCic.Meta _ | NCic.Appl _ ) -> ~-1 + | ( NCic.Meta _ | NCic.Appl _ ), NCic.Const _ -> 1 + | NCic.Appl _, NCic.Meta _ -> ~-1 + | NCic.Meta _, NCic.Appl _ -> 1 | _ -> assert false ;; + + let compare x y = + if NCicReduction.alpha_eq C.metasenv C.subst C.context x y then 0 + else compare x y + ;; let pp t = NCicPp.ppterm ~context:C.context ~metasenv:C.metasenv ~subst:C.subst t;; diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 1bd9bcf4f..fb93ec7f8 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -1,4 +1,5 @@ let nparamod metasenv subst context t table = + prerr_endline "========================================"; let module C = struct let metasenv = metasenv let subst = subst @@ -45,9 +46,12 @@ let nparamod metasenv subst context t table = let table = List.fold_left IDX.index_unit_clause IDX.DT.empty active_clauses in + prerr_endline "Active table:"; + List.iter (fun uc -> prerr_endline (Pp.pp_unit_clause uc)) active_clauses; let bag, maxvar, newclauses = Sup.superposition_right_with_table bag maxvar clause table in prerr_endline "Output clauses :"; List.iter (fun c -> prerr_endline (Pp.pp_unit_clause c)) newclauses; + prerr_endline "========================================"; ;; diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 64cc35bd4..fe4b578b6 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -18,6 +18,7 @@ module Superposition (B : Terms.Blob) = module Subst = FoSubst.Subst(B) module Order = Orderings.Orderings(B) module Utils = FoUtils.Utils(B) + module Pp = Pp.Pp(B) let all_positions pos ctx t f = let rec aux pos ctx = function @@ -41,7 +42,7 @@ module Superposition (B : Terms.Blob) = let superposition_right table varlist subterm pos context = let cands = IDX.DT.retrieve_unifiables table subterm in HExtlib.filter_map - (fun (dir, (id,lit,vl,_)) -> + (fun (dir, (id,lit,vl,_ (*as uc*))) -> match lit with | Terms.Predicate _ -> assert false | Terms.Equation (l,r,_,o) -> @@ -59,7 +60,10 @@ module Superposition (B : Terms.Blob) = if o <> Terms.Lt && o <> Terms.Eq then Some (context newside, subst, varlist, id, pos, dir) else - None + ((*prerr_endline ("Filtering: " ^ + Pp.pp_foterm side ^ " =(< || =)" ^ + Pp.pp_foterm newside ^ " coming from " ^ + Pp.pp_unit_clause uc );*)None) else Some (context newside, subst, varlist, id, pos, dir) with FoUnif.UnificationFailure _ -> None) @@ -84,7 +88,7 @@ module Superposition (B : Terms.Blob) = in Some (bag, maxvar, uc) else - None + ((*prerr_endline ("Filtering: " ^ Pp.pp_foterm t);*)None) ;; let fold_build_new_clause bag maxvar id filter res = diff --git a/helm/software/matita/tests/paratest.ma b/helm/software/matita/tests/paratest.ma index 4e8747297..de4c42048 100644 --- a/helm/software/matita/tests/paratest.ma +++ b/helm/software/matita/tests/paratest.ma @@ -14,5 +14,9 @@ include "nat/plus.ma". -ntheorem foo: \forall x, y. ((λz. x + x = z + z) ?). -##[ #x; #y; nnormalize; nauto. \ No newline at end of file +ntheorem foo: + ((λx.x + 0 = x) ?) → + ((λx,y.x + S y = S (x + y)) ? ?) → + ((λx,y.y + x = x + y) ? ?) → + ∀x. ((λz. x + x = z + S z) ?). +##[ #H; #H1; #H2; #x; nnormalize in H H1 H2 ⊢ %; nauto by H, H1, H2. \ No newline at end of file