From e22808c929a9cebf5e4e2b7428ff0cbf89e1f92a Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 8 Feb 2010 07:24:34 +0000 Subject: [PATCH] Some changes towards integration of setoid-rewriting. --- .../components/ng_paramodulation/cicBlob.ml | 2 + .../components/ng_paramodulation/foUtils.ml | 6 +-- .../components/ng_paramodulation/nCicBlob.ml | 40 +++++++++++++++-- .../ng_paramodulation/nCicParamod.ml | 4 +- .../components/ng_paramodulation/nCicProof.ml | 45 ++++++++++++++++--- .../components/ng_paramodulation/paramod.ml | 37 +++++++++------ .../ng_paramodulation/superposition.ml | 3 ++ .../components/ng_paramodulation/terms.ml | 1 + .../components/ng_paramodulation/terms.mli | 1 + 9 files changed, 112 insertions(+), 27 deletions(-) diff --git a/helm/software/components/ng_paramodulation/cicBlob.ml b/helm/software/components/ng_paramodulation/cicBlob.ml index fd6947e9c..716960142 100644 --- a/helm/software/components/ng_paramodulation/cicBlob.ml +++ b/helm/software/components/ng_paramodulation/cicBlob.ml @@ -38,6 +38,8 @@ module CicBlob(C : CicContext) : Terms.Blob with type t = Cic.term = struct let eqP = assert false;; + let is_eq = assert false;; + let saturate = assert false;; end diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml index e42f1b5b9..826687afc 100644 --- a/helm/software/components/ng_paramodulation/foUtils.ml +++ b/helm/software/components/ng_paramodulation/foUtils.ml @@ -114,11 +114,11 @@ module Utils (B : Orderings.Blob) = struct aux (aux [] ty) proofterm in let lit = - match ty with - | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq -> + match B.is_eq ty with + | Some(ty,l,r) -> let o = Order.compare_terms l r in Terms.Equation (l, r, ty, o) - | t -> Terms.Predicate t + | None -> Terms.Predicate ty in let proof = Terms.Exact proofterm in fresh_unit_clause maxvar (0, lit, varlist, proof) diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml index bc7289176..6c6e07101 100644 --- a/helm/software/components/ng_paramodulation/nCicBlob.ml +++ b/helm/software/components/ng_paramodulation/nCicBlob.ml @@ -20,6 +20,17 @@ let default_eqP() = NCic.Const ref ;; +let equivalence_relation = + let uri = NUri.uri_of_string "cic:/matita/ng/properties/relations/eq_rel.con" + in + let ref = NReference.reference_of_spec uri (NReference.Fix(0,1,2)) + in NCic.Const ref + +let setoid_eq = + let uri = NUri.uri_of_string "cic:/matita/ng/sets/setoids/eq.con" in + let ref = NReference.reference_of_spec uri (NReference.Fix(0,0,2)) + in NCic.Const ref + let set_default_eqP() = eqPref := default_eqP let set_reference_of_oxuri f = @@ -49,11 +60,24 @@ with type t = NCic.term and type input = NCic.term = struct let eq x y = x = y;; (* NCicReduction.alpha_eq C.metasenv C.subst C.context x y;; *) + let height_of_ref = function + | NReference.Def h -> h + | NReference.Fix(_,_,h) -> h + | _ -> 0 + + let compare_refs (NReference.Ref (u1,r1)) (NReference.Ref (u2,r2)) = + let x = height_of_ref r2 - height_of_ref r1 in + if x = 0 then + Hashtbl.hash (NUri.string_of_uri u1,r1) - + Hashtbl.hash (NUri.string_of_uri u2,r2) + else x + let rec compare x y = match x,y with | NCic.Rel i, NCic.Rel j -> j-i | NCic.Meta (i,_), NCic.Meta (j,_) -> i-j - | NCic.Const r1, NCic.Const r2 -> NReference.compare r1 r2 + | NCic.Const r1, NCic.Const r2 -> compare_refs r1 r2 + (*NReference.compare r1 r2*) | 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 @@ -72,6 +96,17 @@ with type t = NCic.term and type input = NCic.term = struct else compare x y ;; + let eqP = (!eqPref)() + ;; + + let is_eq = function + | Terms.Node [ Terms.Leaf eqt ; ty; l; r ] when eq eqP eqt -> + Some (ty,l,r) + | Terms.Node [ Terms.Leaf eqt ; _; Terms.Node [Terms.Leaf eqt2 ; ty]; l; r] + when eq equivalence_relation eqt && eq setoid_eq eqt2 -> + Some (ty,l,r) + | _ -> None + let pp t = NCicPp.ppterm ~context:C.context ~metasenv:C.metasenv ~subst:C.subst t;; @@ -105,7 +140,4 @@ with type t = NCic.term and type input = NCic.term = struct proof, sty ;; - let eqP = (!eqPref)() - ;; - end diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml index b3ab4d504..5b3e6148b 100644 --- a/helm/software/components/ng_paramodulation/nCicParamod.ml +++ b/helm/software/components/ng_paramodulation/nCicParamod.ml @@ -107,11 +107,13 @@ let forward_infer_step s t ty = let bag,clause = P.mk_passive bag (t,ty) in if Terms.is_eq_clause clause then P.forward_infer_step (P.replace_bag s bag) clause 0 - else (prerr_endline "not eq"; s) + else (debug (lazy "not eq"); s) ;; let index_obj s uri = let obj = NCicEnvironment.get_checked_obj uri in + debug (lazy ("indexing : " ^ (NUri.string_of_uri uri))); + debug (lazy ("no : " ^ (string_of_int (fst (Obj.magic uri))))); match obj with | (_,d,[],[],NCic.Constant(_,_,Some(_),ty,_)) -> let nref = NReference.reference_of_spec uri (NReference.Def d) in diff --git a/helm/software/components/ng_paramodulation/nCicProof.ml b/helm/software/components/ng_paramodulation/nCicProof.ml index d1f38487c..0bc4dc2c2 100644 --- a/helm/software/components/ng_paramodulation/nCicProof.ml +++ b/helm/software/components/ng_paramodulation/nCicProof.ml @@ -122,6 +122,30 @@ let debug c _ = c;; NCic.Lambda("x", hole_type, aux ft (List.rev p1)) ;; +(* + let mk_morphism eq amount ft p1 vl = + let rec aux t p = + match p with + | [] -> eq + | n::tl -> + match t with + | Terms.Leaf _ + | Terms.Var _ -> assert false + | Terms.Node l -> + let dag,arity = ____ in + let l = + HExtlib.list_rev_mapi_filter + (fun t i -> + if i < arity then None + else if i = n then Some (aux t tl) + else Some (NCic.Appl [refl ...])) + l + in + NCic.Appl (dag::l) + in aux ft (List.rev pl) + ;; +*) + let mk_proof (bag : NCic.term Terms.bag) mp subst steps = let module Subst = FoSubst in let position i l = @@ -245,13 +269,22 @@ let debug c _ = c;; else l,r,eq_ind () in - NCic.LetIn ("clause_" ^ string_of_int id, - close_with_forall vl (extract amount vl lit), + let body = aux ongoal + ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl + in + if NCicUntrusted.count_occurrences [] 0 body <= 1 then + NCicSubstitution.subst + ~avoid_beta_redexes:true ~no_implicit:false + (close_with_lambdas vl (NCic.Appl + [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ])) + body + else + NCic.LetIn ("clause_" ^ string_of_int id, + close_with_forall vl (extract amount vl lit), (* NCic.Implicit `Type, *) - close_with_lambdas vl - (NCic.Appl [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]), - aux ongoal - ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl) + close_with_lambdas vl (NCic.Appl + [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]), + body) in aux false [] steps, proof_type ;; diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml index 7c934df1e..f7bc2eac9 100644 --- a/helm/software/components/ng_paramodulation/paramod.ml +++ b/helm/software/components/ng_paramodulation/paramod.ml @@ -11,8 +11,9 @@ (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *) -(* let debug s = prerr_endline (Lazy.force s) ;; *) -let debug _ = ();; +let print s = prerr_endline (Lazy.force s) ;; +(* let debug = print *) +let debug s = ();; let monster = 100;; @@ -257,6 +258,18 @@ module Paramod (B : Orderings.Blob) = struct (add_passive_goals g_passives new_goals) ;; + let pp_clauses actives passives = + let actives_l, _ = actives in + let passive_t,_,_ = passives in + let wset = IDX.elems passive_t in + ("Actives :" ^ (String.concat ";\n" + (List.map Pp.pp_unit_clause actives_l))) + ^ + ("Passives:" ^(String.concat ";\n" + (List.map (fun _,cl -> Pp.pp_unit_clause cl) + (IDX.ClauseSet.elements wset)))) + ;; + let forward_infer_step ((bag,maxvar,actives,passives,g_actives,g_passives) as s) current iterno = @@ -272,14 +285,12 @@ module Paramod (B : Orderings.Blob) = struct * P' = P + new' *) debug (lazy "Forward infer step..."); debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives))))); - let id,_,_,_ = current in - let _ = Terms.get_from_bag id bag in - + debug (lazy (pp_clauses actives passives)); match Sup.keep_simplified current actives bag maxvar with | _,None -> s | bag,Some (current,actives) -> - debug (lazy "simplified..."); + debug (lazy ("simplified to " ^ (Pp.pp_unit_clause current))); let bag, maxvar, actives, new_clauses = Sup.infer_right bag maxvar current actives in @@ -326,7 +337,7 @@ module Paramod (B : Orderings.Blob) = struct (passive_set_cardinal passives))) ;; - + (* we just check if any of the active goals is subsumed by a passive clause, or if any of the passive goal is subsumed by an active or passive clause *) @@ -344,14 +355,14 @@ module Paramod (B : Orderings.Blob) = struct (lazy ("Passives:" ^(String.concat ";\n" (List.map (fun _,cl -> Pp.pp_unit_clause cl) - (IDX.ClauseSet.elements wset))))) in + (IDX.ClauseSet.elements wset))))) in let g_passives = WeightPassiveSet.fold (fun (_,x) acc -> if List.exists (Sup.are_alpha_eq x) g_actives then acc else x::acc) (fst g_passives) [] - in + in ignore (List.iter (fun x -> @@ -437,7 +448,7 @@ module Paramod (B : Orderings.Blob) = struct let bag,maxvar,actives,passives,g_actives,g_passives = status in match Sup.simplify_goal - ~no_demod:false maxvar (snd actives) bag g_actives current + ~no_demod maxvar (snd actives) bag g_actives current with | None -> status | Some (bag,g_current) -> @@ -469,9 +480,9 @@ module Paramod (B : Orderings.Blob) = struct let _ = debug (lazy("Selected goal : " ^ Pp.pp_unit_clause current)) in - (* awe work both on the original goal and the demodulated one*) - let acc = check_and_infer ~no_demod:true iterno acc current - in check_and_infer ~no_demod:false iterno acc current) + (* we work both on the original goal and the demodulated one*) + let acc = check_and_infer ~no_demod:false iterno acc current + in check_and_infer ~no_demod:true iterno acc current) status passive_goals in goal_narrowing iterno max_steps timeout newstatus diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml index 6ec6048de..37b39fa28 100644 --- a/helm/software/components/ng_paramodulation/superposition.ml +++ b/helm/software/components/ng_paramodulation/superposition.ml @@ -619,6 +619,9 @@ module Superposition (B : Orderings.Blob) = let bag, clause = if no_demod then bag, clause else demodulate bag clause table in + let _ = debug ("demodulated goal : " + ^ Pp.pp_unit_clause clause) + in if List.exists (are_alpha_eq clause) g_actives then None else match (is_identity_goal clause) with | Some subst -> raise (Success (bag,maxvar,clause,subst)) diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml index 61b027d72..87b4f383b 100644 --- a/helm/software/components/ng_paramodulation/terms.ml +++ b/helm/software/components/ng_paramodulation/terms.ml @@ -96,6 +96,7 @@ module type Blob = val eq : t -> t -> bool val compare : t -> t -> int val eqP : t + val is_eq: t foterm -> (t foterm* t foterm *t foterm) option val pp : t -> string type input val embed : input -> t foterm diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli index 03bdddb89..93f106a4f 100644 --- a/helm/software/components/ng_paramodulation/terms.mli +++ b/helm/software/components/ng_paramodulation/terms.mli @@ -87,6 +87,7 @@ module type Blob = (* TODO: consider taking in input an imperative buffer for Format * val pp : Format.formatter -> t -> unit * *) + val is_eq : t foterm -> (t foterm * t foterm * t foterm) option val pp : t -> string type input -- 2.39.2