+++ /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 / blobdiff