From 90a88a05bb66c0e14a95d54929a4b545c8f2a36c Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 10 May 2004 09:43:55 +0000 Subject: [PATCH] Adding file newConstraint The file contains functions for computing prefixes and related stuff, required by the new management of matching. --- helm/ocaml/tactics/newConstraints.ml | 312 ++++++++++++++++++++++++++ helm/ocaml/tactics/newConstraints.mli | 54 +++++ 2 files changed, 366 insertions(+) create mode 100644 helm/ocaml/tactics/newConstraints.ml create mode 100644 helm/ocaml/tactics/newConstraints.mli diff --git a/helm/ocaml/tactics/newConstraints.ml b/helm/ocaml/tactics/newConstraints.ml new file mode 100644 index 000000000..00cf27956 --- /dev/null +++ b/helm/ocaml/tactics/newConstraints.ml @@ -0,0 +1,312 @@ +(* Copyright (C) 2000-2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(*********************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Andrea Asperti *) +(* 18/03/2004 *) +(* *) +(* *) +(*********************************************************************) + +(* the file contains functions for computing prefixes and related + stuff, required by the new management of matching *) + +module SortedString = + struct + type t = string + let compare = Pervasives.compare + end +;; + +module StringSet = Set.Make (SortedString) +;; + +module SetSet = Set.Make (StringSet) +;; + + +(* + module SetSet : + sig + type elt = StringSet.t + and t = Set.Make(StringSet).t + val empty : t + val is_empty : t -> bool + val mem : elt -> t -> bool + val add : elt -> t -> t + val singleton : elt -> t + val remove : elt -> t -> t + val union : t -> t -> t + val inter : t -> t -> t + val diff : t -> t -> t + val compare : t -> t -> int + val equal : t -> t -> bool + val subset : t -> t -> bool + val iter : (elt -> unit) -> t -> unit + val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a + val for_all : (elt -> bool) -> t -> bool + val exists : (elt -> bool) -> t -> bool + val filter : (elt -> bool) -> t -> t + val partition : (elt -> bool) -> t -> t * t + val cardinal : t -> int + val elements : t -> elt list + val min_elt : t -> elt + val max_elt : t -> elt + val choose : t -> elt + end +*) + +let pp_StringSet set = + if (StringSet.is_empty set) then "EMPTY" + else + "{" ^ (String.concat "," (StringSet.elements set)) ^ "}" +;; + +let pp_SetSet set = + let el = List.map pp_StringSet (SetSet.elements set) in + "{" ^ (String.concat ",\n" el) ^ "}" +;; + +let pp_prefix (n,l) = + (string_of_int n) ^ + ": {" ^ (String.concat "," l) ^ "}" + +let pp_prefixes l = + let el = List.map pp_prefix l in + "{" ^ (String.concat ",\n" el) ^ "}" + + + +let filter_by_card n = + SetSet.filter (fun t -> (StringSet.cardinal t) <= n) +;; + +let merge n a b = + let init = SetSet.union a b in + let merge_single_set s1 b = + SetSet.fold + (fun s2 res -> SetSet.add (StringSet.union s1 s2) res) + b SetSet.empty in + let res = + SetSet.fold (fun s1 res -> SetSet.union (merge_single_set s1 b) res) a init + in + filter_by_card n res +;; + +let mutinduri u t = + (UriManager.string_of_uri u) ^ "#xpointer(1/" ^ (string_of_int (t+1)) ^ ")" +;; + +let mutconstructuri u t c = + (UriManager.string_of_uri u) + ^ "#xpointer(1/" ^ (string_of_int (t+1)) ^ "/" ^ (string_of_int c) ^ ")" +;; + +let rec inspect_children n childs = + List.fold_left + (fun res term -> merge n (inspect_conclusion n term) res) + SetSet.empty childs + +and add_root n root childs = + let childunion = inspect_children n childs in + let addroot = StringSet.add root in + SetSet.fold + (fun child newsets -> SetSet.add (addroot child) newsets) + childunion + (SetSet.singleton (StringSet.singleton root)) + +and inspect_conclusion n t = +if n = 0 then SetSet.empty +else match t with + Cic.Rel _ + | Cic.Meta _ + | Cic.Sort _ + | Cic.Implicit _ -> SetSet.empty + | Cic.Var (u,exp_named_subst) -> SetSet.empty + | Cic.Const (u,exp_named_subst) -> + SetSet.singleton (StringSet.singleton (UriManager.string_of_uri u)) + | Cic.MutInd (u, t, exp_named_subst) -> + SetSet.singleton (StringSet.singleton (mutinduri u t)) + | Cic.MutConstruct (u, t, c, exp_named_subst) -> + SetSet.singleton (StringSet.singleton (mutconstructuri u t c)) + | Cic.Cast (t, _) -> inspect_conclusion n t + | Cic.Prod (_, s, t) -> + merge n (inspect_conclusion n s) (inspect_conclusion n t) + | Cic.Lambda (_, s, t) -> + merge n (inspect_conclusion n s) (inspect_conclusion n t) + | Cic.LetIn (_, s, t) -> + merge n (inspect_conclusion n s) (inspect_conclusion n t) + | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) -> + let suri = UriManager.string_of_uri u in + add_root (n-1) suri l + | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) -> + let suri = mutinduri u t in + add_root (n-1) suri l + | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) -> + let suri = mutconstructuri u t c in + add_root (n-1) suri l + | Cic.Appl l -> + SetSet.empty + | Cic.MutCase (u, t, tt, uu, m) -> + SetSet.empty + | Cic.Fix (_, m) -> + SetSet.empty + | Cic.CoFix (_, m) -> + SetSet.empty +;; + +let rec inspect_term n t = +if n = 0 then assert false +else match t with + Cic.Rel _ + | Cic.Meta _ + | Cic.Sort _ + | Cic.Implicit _ -> None, SetSet.empty + | Cic.Var (u,exp_named_subst) -> None, SetSet.empty + | Cic.Const (u,exp_named_subst) -> + Some (UriManager.string_of_uri u), SetSet.empty + | Cic.MutInd (u, t, exp_named_subst) -> + Some (mutinduri u t), SetSet.empty + | Cic.MutConstruct (u, t, c, exp_named_subst) -> + Some (mutconstructuri u t c), SetSet.empty + | Cic.Cast (t, _) -> inspect_term n t + | Cic.Prod (_, _, t) -> inspect_term n t + | Cic.LetIn (_, _, t) -> inspect_term n t + | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) -> + let suri = UriManager.string_of_uri u in + let childunion = inspect_children (n-1) l in + Some suri, childunion + | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) -> + let suri = mutinduri u t in + if u = HelmLibraryObjects.Logic.eq_URI && n>1 then + (* equality is handled in a special way: in particular, + the type, if defined, is always added to the prefix, + and n is not decremented - it should have been n-2 *) + match l with + Cic.Const (u1,exp_named_subst1)::l1 -> + let suri1 = UriManager.string_of_uri u1 in + let inconcl = add_root (n-1) suri1 l1 in + Some suri, inconcl + | Cic.MutInd (u1, t1, exp_named_subst1)::l1 -> + let suri1 = mutinduri u1 t1 in + let inconcl = add_root (n-1) suri1 l1 in + Some suri, inconcl + | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 -> + let suri1 = mutconstructuri u1 t1 c1 in + let inconcl = add_root (n-1) suri1 l1 in + Some suri, inconcl + | _ :: _ -> Some suri, SetSet.empty + | _ -> assert false (* args number must be > 0 *) + else + let childunion = inspect_children (n-1) l in + Some suri, childunion + | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) -> + let suri = mutconstructuri u t c in + let childunion = inspect_children (n-1) l in + Some suri, childunion + | _ -> None, SetSet.empty + +let rec add uri children = + List.fold_left + (fun acc t -> + StringSet.union (constants_concl t) acc) + (StringSet.singleton uri) children + +(* this function creates the set of all different constants appearing in + the conclusion of the term *) +and constants_concl = + function + Cic.Rel _ + | Cic.Meta _ + | Cic.Sort _ + | Cic.Implicit _ -> StringSet.empty + | Cic.Var (u,exp_named_subst) -> StringSet.empty + | Cic.Const (u,exp_named_subst) -> + StringSet.singleton (UriManager.string_of_uri u) + | Cic.MutInd (u, t, exp_named_subst) -> + StringSet.singleton (mutinduri u t) + | Cic.MutConstruct (u, t, c, exp_named_subst) -> + StringSet.singleton (mutconstructuri u t c) + | Cic.Cast (t, _) -> constants_concl t + | Cic.Prod (_, s, t) -> + StringSet.union (constants_concl s) (constants_concl t) + | Cic.Lambda (_, s, t) -> + StringSet.union (constants_concl s) (constants_concl t) + | Cic.LetIn (_, s, t) -> + StringSet.union (constants_concl s) (constants_concl t) + | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) -> + let suri = UriManager.string_of_uri u in + add suri l + | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) -> + let suri = mutinduri u t in + add suri l + | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l) -> + let suri = mutconstructuri u t c in + add suri l + | Cic.Appl l -> + StringSet.empty + | Cic.MutCase (u, t, tt, uu, m) -> + StringSet.empty + | Cic.Fix (_, m) -> + StringSet.empty + | Cic.CoFix (_, m) -> + StringSet.empty +;; + +(* (constants_of t) returns a pair (b,n) where n is the number of + constants in the conclusion of t, and b is true if in MainConclusion + we have an equality *) + +let rec constants_of = function + | Cic.Cast (t, _) -> constants_of t + | Cic.Prod (_, _, t) -> constants_of t + | Cic.LetIn (_, _, t) -> constants_of t + | (Cic.Appl ((Cic.MutInd (u, _, _))::l)) as t when + u = HelmLibraryObjects.Logic.eq_URI -> + (true, constants_concl t) + | t -> (false, constants_concl t) +;; + + +let add_cardinality s = + let l = SetSet.elements s in + let res = + List.map + (fun set -> + let el = StringSet.elements set in + (List.length el, el)) l in + (* ordered by descending cardinality *) + List.sort (fun (n,_) (m,_) -> m - n) ((0,[])::res) +;; + +let prefixes n t = + match inspect_term n t with + Some a, set -> Some a, add_cardinality set + | None, set when (SetSet.is_empty set) -> None, [] + | _, _ -> assert false +;; diff --git a/helm/ocaml/tactics/newConstraints.mli b/helm/ocaml/tactics/newConstraints.mli new file mode 100644 index 000000000..e57d6b1e0 --- /dev/null +++ b/helm/ocaml/tactics/newConstraints.mli @@ -0,0 +1,54 @@ +(* Copyright (C) 2000-2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(*********************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Andrea Asperti *) +(* 18/03/2004 *) +(* *) +(* *) +(*********************************************************************) + + +module StringSet : Set.S with type elt = string + +module SetSet : Set.S with type elt = StringSet.t + +val pp_SetSet : SetSet.t -> string + +val inspect_term : int -> Cic.term -> string option * SetSet.t + +val prefixes : int -> Cic.term -> string option * ((int * (StringSet.elt list)) list) + +(* (constants_of t) returns a pair (b,n) where n is the number of + constants in the conclusion of t, and b is true if in MainConclusion + we have an equality *) + +val constants_of : Cic.term -> bool * StringSet.t + +val pp_prefixes : ((int * (StringSet.elt list)) list) -> string + -- 2.39.2