X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.ml;h=f3af1b482e8afb2eece8d1ce79d3e10af7812ec7;hb=4ab3123d6a8e5080009d7b471b0cefd05f4817ed;hp=7aafcbcd627927c66ced9577151dd61f2ef985ab;hpb=50844b0116c863862434c7c673c5caaf6ff78cdf;p=helm.git diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index 7aafcbcd6..f3af1b482 100644 --- a/helm/software/components/tactics/paramodulation/indexing.ml +++ b/helm/software/components/tactics/paramodulation/indexing.ml @@ -23,12 +23,10 @@ * http://cs.unibo.it/helm/. *) -let _profiler = <:profiler<_profiler>>;; +(* 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 *) @@ -182,15 +180,9 @@ let get_candidates ?env mode tree term = let s = match mode with | Matching -> - let _ = <:start> in - <:stop> | Unification -> - let _ = <:start> in - <:stop> in Index.PosEqSet.elements s @@ -536,7 +528,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 +576,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 +603,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 +614,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 @@ -798,8 +710,8 @@ let rec betaexpand_term | C.Appl l -> let l', lifted_l = - List.fold_right - (fun arg (res, lifted_tl) -> + List.fold_left + (fun (res, lifted_tl) arg -> let arg_res, lifted_arg = betaexpand_term metasenv context ugraph table lift_amount arg in @@ -815,7 +727,7 @@ let rec betaexpand_term lifted_arg::r, s, m, ug, eq_found) res), lifted_arg::lifted_tl) - ) l ([], []) + ) ([], []) (List.rev l) in (List.map (fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l', @@ -1048,26 +960,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_weights ~normalize:true - (Utils.weight_of_term l) (Utils.weight_of_term r) + let c = !Utils.compare_terms l r in + 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 - - if c = Utils.Incomparable then - let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in - let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in - List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl - @ - List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr - - else - let big,small,possmall = - match c with Utils.Gt -> l,r,Utils.Right | _ -> 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 + (* 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 *) @@ -1099,4 +1033,4 @@ let rec demodulation_goal env table goal = | None -> do_right () ;; -let get_stats () = <:show> ;; +let get_stats () = "" ;;