From abb7b4623d6c2eb93f289c44fe46f45faa7e3374 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Wed, 29 Oct 2008 15:10:01 +0000 Subject: [PATCH] New demod function working for arbitary goals. --- .../tactics/paramodulation/indexing.ml | 183 +++++++++++++++--- .../tactics/paramodulation/indexing.mli | 7 + 2 files changed, 164 insertions(+), 26 deletions(-) diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index 9c471d3b3..8f696d6f3 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -109,19 +109,73 @@ let check_disjoint_invariant subst metasenv msg = ;; let check_for_duplicates metas msg = - if List.length metas <> - List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then - begin + let rec aux = function + | [] -> true + | (m,_,_)::tl -> not (List.exists (fun (i, _, _) -> i = m) tl) && aux tl in + let b = aux metas in + if not b then + begin prerr_endline ("DUPLICATI " ^ msg); prerr_endline (CicMetaSubst.ppmetasenv [] metas); assert false - end + end + else () +;; + +let check_metasenv msg menv = + List.iter + (fun (i,ctx,ty) -> + try ignore(CicTypeChecker.type_of_aux' menv ctx ty + CicUniv.empty_ugraph) + with + | CicUtil.Meta_not_found _ -> + prerr_endline (msg ^ CicMetaSubst.ppmetasenv [] menv); + assert false + | _ -> () + ) menv +;; + +(* the metasenv returned by res must included in the original one, +due to matching. If it fails, it is probably because we are not +demodulating with a unit equality *) + +let not_unit_eq ctx eq = + let (_,_,(ty,left,right,o),metas,_) = Equality.open_equality eq in + let b = + List.exists + (fun (_,_,ty) -> + try + let s,_ = CicTypeChecker.type_of_aux' metas ctx ty CicUniv.empty_ugraph + in s = Cic.Sort(Cic.Prop) + with _ -> + prerr_endline ("ERROR typing " ^ CicPp.ppterm ty); assert false) metas + in b +(* +if b then prerr_endline ("not a unit equality: " ^ Equality.string_of_equality eq); b *) +;; + +let check_demod_res res metasenv msg = + match res with + | Some (_, _, menv, _, _) -> + let b = + List.for_all + (fun (i,_,_) -> + (List.exists (fun (j,_,_) -> i=j) metasenv)) menv + in + if (not b) then + begin + prerr_endline ("extended context " ^ msg); + prerr_endline (CicMetaSubst.ppmetasenv [] menv); + end; + b + | None -> false ;; let check_res res msg = match res with - Some (t, subst, menv, ug, eq_found) -> + | Some (t, subst, menv, ug, eq_found) -> let eqs = Equality.string_of_equality (snd eq_found) in + check_metasenv msg menv; check_disjoint_invariant subst menv msg; check_for_duplicates menv (msg ^ "\nchecking " ^ eqs); | None -> () @@ -222,6 +276,11 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty = | [] -> None | candidate::tl -> let pos, equality = candidate in + (* if not_unit_eq context equality then + begin + prerr_endline "not a unit"; + prerr_endline (Equality.string_of_equality equality) + end; *) let (_, proof, (ty, left, right, o), metas,_) = Equality.open_equality equality in @@ -232,13 +291,18 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty = let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in let t="t = " ^ (CicPp.ppterm term) ^ "\n" in let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in -(* + let ms="metasenv =" ^ (CicMetaSubst.ppmetasenv [] metasenv) ^ "\n" in + let eq_uri = + match LibraryObjects.eq_URI () with + | Some (uri) -> uri + | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in let p="proof = "^ - (CicPp.ppterm(Equality.build_proof_term proof))^"\n" + (CicPp.ppterm(Equality.build_proof_term bag eq_uri [] 0 proof))^"\n" in -*) + check_for_duplicates metas "gia nella metas"; - check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m(*^p*)) + check_for_duplicates metasenv "gia nel metasenv"; + check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^ms^p) end; if check && not (fst (CicReduction.are_convertible ~metasenv context termty ty ugraph)) then ( @@ -249,6 +313,7 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty = Founif.matching metasenv metas context term (S.lift lift_amount c) ugraph in + check_metasenv "founif :" metasenv'; Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate) in let c, other = @@ -269,7 +334,7 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty = try do_match c with Founif.MatchingFailure -> None in - if Utils.debug_res then ignore (check_res res "find2"); + if Utils.debug_res then ignore (check_res res "find2"); match res with | Some (_, s, _, _, _) -> let c' = apply_subst s c in @@ -303,17 +368,23 @@ let rec find_all_matches ?(unif_fun=Founif.unification) let module M = CicMetaSubst in let module HL = HelmLibraryObjects in let cmp = !Utils.compare_terms in + let check = match termty with C.Implicit None -> false | _ -> true in function | [] -> [] | candidate::tl -> let pos, equality = candidate in - let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in + let (_,_,(ty,left,right,o),metas,_)= Equality.open_equality equality in + if check && not (fst (CicReduction.are_convertible + ~metasenv context termty ty ugraph)) then ( + find_all_matches metasenv context ugraph lift_amount term termty tl + ) else let do_match c = let subst', metasenv', ugraph' = unif_fun metasenv metas context term (S.lift lift_amount c) ugraph in (C.Rel (1+lift_amount),subst',metasenv',ugraph',candidate) in + let c, other = if pos = Utils.Left then left, right else right, left @@ -429,10 +500,12 @@ let unification x y z = subsumption_aux true x y z ;; +(* the target must be disjoint from the equations in the table *) let subsumption_aux_all use_unification env table target = let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in let _, context, ugraph = env in let metasenv = tmetas in + check_for_duplicates metasenv "subsumption_aux_all"; let predicate, unif_fun = if use_unification then Unification, Founif.unification @@ -484,32 +557,46 @@ let subsumption_all x y z = let unification_all x y z = subsumption_aux_all true x y z ;; + let rec demodulation_aux bag ?from ?(typecheck=false) metasenv context ugraph table lift_amount term = -(* Printf.eprintf "term = %s\n" (CicPp.ppterm term);*) let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in let module HL = HelmLibraryObjects in + (* prerr_endline ("demodulating " ^ CicPp.ppterm term); *) + check_for_duplicates metasenv "in input a demodulation aux"; let candidates = get_candidates ~env:(metasenv,context,ugraph) (* Unification *) Matching table term + in let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates in let res = match term with | C.Meta _ -> None | term -> - let termty, ugraph = - if typecheck then - CicTypeChecker.type_of_aux' metasenv context term ugraph - else - C.Implicit None, ugraph - in - let res = - find_matches bag metasenv context ugraph lift_amount term termty candidates + let res = + try + let termty, ugraph = + if typecheck then + CicTypeChecker.type_of_aux' metasenv context term ugraph + else + C.Implicit None, ugraph + in + find_matches bag metasenv context ugraph + lift_amount term termty candidates + with _ -> + prerr_endline "type checking error"; + prerr_endline ("menv :\n" ^ CicMetaSubst.ppmetasenv [] metasenv); + prerr_endline ("term: " ^ (CicPp.ppterm term)); + assert false; + (* None *) in - if Utils.debug_res then ignore(check_res res "demod1"); - if res <> None then + let res = + (if Utils.debug_res then + ignore(check_res res "demod1"); + if check_demod_res res metasenv "demod" then res else None) in + if res <> None then res else match term with @@ -521,7 +608,7 @@ let rec demodulation_aux bag ?from ?(typecheck=false) (res, tl @ [S.lift 1 t]) else let r = - demodulation_aux bag ~from:"1" metasenv context ugraph table + demodulation_aux bag ~from:"1" metasenv context ugraph table ~typecheck lift_amount t in match r with @@ -534,6 +621,7 @@ let rec demodulation_aux bag ?from ?(typecheck=false) | Some (_, subst, menv, ug, eq_found) -> Some (C.Appl ll, subst, menv, ug, eq_found) ) +(* | C.Prod (nn, s, t) -> let r1 = demodulation_aux bag ~from:"2" @@ -556,6 +644,7 @@ let rec demodulation_aux bag ?from ?(typecheck=false) subst, menv, ug, eq_found) ) | C.Lambda (nn, s, t) -> + prerr_endline "siam qui"; let r1 = demodulation_aux bag metasenv context ugraph table lift_amount s in ( @@ -576,6 +665,7 @@ let rec demodulation_aux bag ?from ?(typecheck=false) Some (C.Lambda (nn, s', (S.lift 1 t)), subst, menv, ug, eq_found) ) +*) | t -> None in @@ -810,8 +900,8 @@ let rec betaexpand_term | C.Meta (i, l) -> res, lifted_term | term -> let termty, ugraph = - C.Implicit None, ugraph -(* CicTypeChecker.type_of_aux' metasenv context term ugraph *) +(* C.Implicit None, ugraph *) + CicTypeChecker.type_of_aux' metasenv context term ugraph in let candidates = get_candidates Unification table term in let r = @@ -971,13 +1061,53 @@ let rec demodulation_theorem bag env table theorem = (** DEMODULATION_GOAL & SUPERPOSITION_LEFT **) (*****************************************************************************) +(* new: demodulation of non_equality terms *) +let build_newg bag context goal rule expansion = + let goalproof,_,_ = goal in + let (t,subst,menv,ug,eq_found) = expansion in + let pos, equality = eq_found in + let (_, proof', (ty, what, other, _), menv',id) = + Equality.open_equality equality in + let what, other = if pos = Utils.Left then what, other else other, what in + let newterm, newgoalproof = + let bo = + Utils.guarded_simpl context + (apply_subst subst (CicSubstitution.subst other t)) + in + let bo' = apply_subst subst t in + let ty = apply_subst subst ty in + let name = Cic.Name "x" in + let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in + bo, (newgoalproofstep::goalproof) + in + let newmetasenv = (* Founif.filter subst *) menv in + (newgoalproof, newmetasenv, newterm) +;; + +let rec demod bag env table goal = + let goalproof,menv,t = goal in + let _, context, ugraph = env in + let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:true)in + match res with + | Some newt -> + let newg = + build_newg bag context goal Equality.Demodulation newt + in + let _,_,newt = newg in + if Equality.meta_convertibility t newt then + false, goal + else + true, snd (demod bag env table newg) + | None -> + false, goal +;; + let open_goal g = match g with | (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) -> (* assert (LibraryObjects.is_eq_URI uri); *) proof,menv,eq,ty,l,r | _ -> assert false -;; let ty_of_goal (_,_,ty) = ty ;; @@ -991,6 +1121,7 @@ let goal_metaconvertibility_eq g1 g2 = * C[x] ---> (eq ty unchanged C[x]) * [posu] is the side of the [unchanged] term in the original goal *) + let fix_expansion goal posu (t, subst, menv, ug, eq_f) = let _,_,eq,ty,l,r = open_goal goal in let unchanged = if posu = Utils.Left then l else r in diff --git a/helm/software/components/tactics/paramodulation/indexing.mli b/helm/software/components/tactics/paramodulation/indexing.mli index 52afad8c2..1caa5ed41 100644 --- a/helm/software/components/tactics/paramodulation/indexing.mli +++ b/helm/software/components/tactics/paramodulation/indexing.mli @@ -34,6 +34,7 @@ module Index : Discrimination_tree.Make(Discrimination_tree.CicIndexable)(PosEqSet).t end +val check_for_duplicates : Cic.metasenv -> string -> unit val index : Index.t -> Equality.equality -> Index.t val remove_index : Index.t -> Equality.equality -> Index.t val in_index : Index.t -> Equality.equality -> bool @@ -75,6 +76,12 @@ val superposition_right : Equality.equality -> int * Equality.equality list +val demod : + Equality.equality_bag -> + Cic.metasenv * Cic.context * CicUniv.universe_graph -> + Index.t -> + Equality.goal -> + bool * Equality.goal val demodulation_equality : Equality.equality_bag -> ?from:string -> -- 2.39.2