From ecd70e5517095820fad8e4fde6f6424617ac5d44 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 22 Apr 2005 08:35:21 +0000 Subject: [PATCH] uses new at_least with criteria on constants number difference --- helm/ocaml/tactics/metadataQuery.ml | 39 ++++++++++++++++++++++++----- 1 file changed, 33 insertions(+), 6 deletions(-) diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml index 8dcbcd08a..b6b360a81 100644 --- a/helm/ocaml/tactics/metadataQuery.ml +++ b/helm/ocaml/tactics/metadataQuery.ml @@ -60,20 +60,47 @@ let locate ~(dbd:Mysql.dbd) ?(vars = false) pat = (fun cols -> match cols.(0) with Some s -> s | _ -> assert false)) let match_term ~(dbd:Mysql.dbd) ty = + prerr_endline (CicPp.ppterm ty); let metadata = MetadataExtractor.compute ~body:None ~ty in let constants_no = MetadataConstraints.StringSet.cardinal (MetadataConstraints.constants_of ty) in - let full_card = + let full_card, diff = if CicUtil.is_meta_closed ty then - Some (MetadataConstraints.Eq constants_no) + Some (MetadataConstraints.Eq constants_no), None else - None (* we already require a set of constants to appear, this additional - constraints is useless *) -(* MetadataConstraints.Gt (constants_no - 1) *) + let diff_no = + let (hyp_constants, concl_constants) = + (* collect different constants in hypotheses and conclusions *) + List.fold_left + (fun ((hyp, concl) as acc) metadata -> + match (metadata: MetadataTypes.metadata) with + | `Sort _ | `Rel _ -> acc + | `Obj (uri, `InConclusion) | `Obj (uri, `MainConclusion _) + when not (List.mem uri concl) -> (hyp, uri :: concl) + | `Obj (uri, `InHypothesis) | `Obj (uri, `MainHypothesis _) + when not (List.mem uri hyp) -> (uri :: hyp, concl) + | `Obj _ -> acc) + ([], []) + metadata + in + List.length hyp_constants - List.length concl_constants + in + let (concl_metas, hyp_metas) = MetadataExtractor.compute_metas ty in + let diff = + if MetadataExtractor.IntSet.equal concl_metas hyp_metas then + Some (MetadataConstraints.Eq diff_no) + else if MetadataExtractor.IntSet.subset concl_metas hyp_metas then + Some (MetadataConstraints.Gt (diff_no - 1)) + else if MetadataExtractor.IntSet.subset hyp_metas concl_metas then + Some (MetadataConstraints.Lt (diff_no + 1)) + else + None + in + None, diff in let constraints = List.map MetadataTypes.constr_of_metadata metadata in - Constr.at_least ~dbd ?full_card constraints + Constr.at_least ~dbd ?full_card ?diff constraints let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y)) -- 2.39.2