X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fparamodulation%2Findexing.ml;h=a4bdef1a2a48b0121246ead95c73f21edb56183a;hb=ff074375003b7b0e3d38e2742ff1d6098a0dab57;hp=e7166324de60d735480374a21595b3c9b1af8318;hpb=8ab96f137cdd78abea388ca7f58a24ba1bce61e2;p=helm.git diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml index e7166324d..a4bdef1a2 100644 --- a/components/tactics/paramodulation/indexing.ml +++ b/components/tactics/paramodulation/indexing.ml @@ -27,8 +27,6 @@ let _profiler = <:profiler<_profiler>>;; (* $Id$ *) -type goal = Equality.goal_proof * Cic.metasenv * Cic.term - module Index = Equality_indexing.DT (* discrimination tree based indexing *) (* module Index = Equality_indexing.DT (* path tree based indexing *) @@ -536,7 +534,7 @@ let rec demodulation_aux ?from ?(typecheck=false) exception Foo (** demodulation, when target is an equality *) -let rec demodulation_equality ?from eq_uri newmeta env table sign target = +let rec demodulation_equality ?from eq_uri newmeta env table target = let module C = Cic in let module S = CicSubstitution in let module M = CicMetaSubst in @@ -584,90 +582,10 @@ let rec demodulation_equality ?from eq_uri newmeta env table sign target = let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r] in - if sign = Utils.Positive then (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'), (Cic.Lambda (name, ty, bo')))))) - else - assert false -(* - begin - prerr_endline "***************************************negative"; - let metaproof = - incr maxmeta; - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context in -(* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *) -(* print_newline (); *) - C.Meta (!maxmeta, irl) - in - let eq_found = - let proof'_old' = - let termlist = - if pos = Utils.Left then [ty; what; other] - else [ty; other; what] - in - Equality.ProofSymBlock (termlist, proof'_old) - in - let proof'_new' = assert false (* not implemented *) in - let what, other = - if pos = Utils.Left then what, other else other, what - in - pos, - Equality.mk_equality - (0, (proof'_new',proof'_old'), - (ty, other, what, Utils.Incomparable),menv') - in - let target_proof = - let pb = - Equality.ProofBlock - (subst, eq_URI, (name, ty), bo', - eq_found, Equality.BasicProof (Equality.empty_subst,metaproof)) - in - assert false, (* not implemented *) - (match snd proof with - | Equality.BasicProof _ -> - (* print_endline "replacing a BasicProof"; *) - pb - | Equality.ProofGoalBlock (_, parent_proof) -> - (* print_endline "replacing another ProofGoalBlock"; *) - Equality.ProofGoalBlock (pb, parent_proof) - | _ -> assert false) - in - let refl = - C.Appl [C.MutConstruct (* reflexivity *) - (LibraryObjects.eq_URI (), 0, 1, []); - eq_ty; if is_left then right else left] - in - (bo, - (assert false, (* not implemented *) - Equality.ProofGoalBlock - (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof))) - end -*) - in - let newmenv = (* Inference.filter subst *) menv in -(* - let _ = - if Utils.debug_metas then - try ignore(CicTypeChecker.type_of_aux' - newmenv context - (Equality.build_proof_term newproof) ugraph); - () - with exc -> - prerr_endline "sempre lui"; - prerr_endline (Subst.ppsubst subst); - prerr_endline (CicPp.ppterm - (Equality.build_proof_term newproof)); - prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t)); - prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what)); - prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other)); - prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst)); - prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv [] - newmenv)); - raise exc; - else () in -*) + let newmenv = menv in let left, right = if is_left then newterm, right else left, newterm in let ordering = !Utils.compare_terms left right in let stat = (eq_ty, left, right, ordering) in @@ -691,7 +609,7 @@ let rec demodulation_equality ?from eq_uri newmeta env table sign target = (Equality.meta_convertibility_eq target newtarget) then newmeta, newtarget else - demodulation_equality ?from eq_uri newmeta env table sign newtarget + demodulation_equality ?from eq_uri newmeta env table newtarget | None -> let res = demodulation_aux metasenv' context ugraph table 0 right in if Utils.debug_res then check_res res "demod result 1"; @@ -702,7 +620,7 @@ let rec demodulation_equality ?from eq_uri newmeta env table sign target = (Equality.meta_convertibility_eq target newtarget) then newmeta, newtarget else - demodulation_equality ?from eq_uri newmeta env table sign newtarget + demodulation_equality ?from eq_uri newmeta env table newtarget | None -> newmeta, target in @@ -1048,30 +966,48 @@ let build_newgoal context goal posu rule expansion = returns a list of new clauses inferred with a left superposition step the negative equation "target" and one of the positive equations in "table" *) -let superposition_left (metasenv, context, ugraph) table goal = +let superposition_left (metasenv, context, ugraph) table goal maxmeta = + let names = Utils.names_of_context context in let proof,menv,eq,ty,l,r = open_goal goal in let c = !Utils.compare_terms l r in - if c = Utils.Incomparable then - begin - let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in - let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in - (* prerr_endline "incomparable"; - prerr_endline (string_of_int (List.length expansionsl)); - prerr_endline (string_of_int (List.length expansionsr)); - *) - List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl - @ - List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr - end - else - let big,small,possmall = - match c with - Utils.Gt -> (* prerr_endline "GT"; *) l,r,Utils.Right - | Utils.Lt -> (* prerr_endline "LT"; *) r,l,Utils.Left - | _ -> assert false - in - let expansions, _ = betaexpand_term menv context ugraph table 0 big in - List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions + let newgoals = + if c = Utils.Incomparable then + begin + let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in + let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in + (* prerr_endline "incomparable"; + prerr_endline (string_of_int (List.length expansionsl)); + prerr_endline (string_of_int (List.length expansionsr)); + *) + List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl + @ + List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr + end + else + match c with + | Utils.Gt -> (* prerr_endline "GT"; *) + let big,small,possmall = l,r,Utils.Right in + let expansions, _ = betaexpand_term menv context ugraph table 0 big in + List.map + (build_newgoal context goal possmall Equality.SuperpositionLeft) + expansions + | Utils.Lt -> (* prerr_endline "LT"; *) + let big,small,possmall = r,l,Utils.Left in + let expansions, _ = betaexpand_term menv context ugraph table 0 big in + List.map + (build_newgoal context goal possmall Equality.SuperpositionLeft) + expansions + | Utils.Eq -> [] + | _ -> + prerr_endline + ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names); + assert false + in + (* rinfresco le meta *) + List.fold_right + (fun g (max,acc) -> + let max,g = Equality.fix_metas_goal max g in max,g::acc) + newgoals (maxmeta,[]) ;; (** demodulation, when the target is a goal *)