--- /dev/null
+(* 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 <asperti@cs.unibo.it> *)
+(* 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
+;;
projects / helm.git / commitdiff