helm/ocaml/tactics/newConstraints.ml

   1 (* Copyright (C) 2000-2002, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (*********************************************************************)
  27 (*                                                                   *)
  28 (*                           PROJECT HELM                            *)
  29 (*                                                                   *)
  30 (*               Andrea Asperti <asperti@cs.unibo.it>                *)
  31 (*                            18/03/2004                             *)
  32 (*                                                                   *)
  33 (*                                                                   *)
  34 (*********************************************************************)
  35
  36 (* the file contains functions for computing prefixes and related
  37    stuff, required by the new management of matching *)
  38
  39 module SortedString =
  40   struct
  41     type t = string
  42     let compare = Pervasives.compare
  43   end
  44 ;;
  45
  46 module StringSet = Set.Make (SortedString)
  47 ;;
  48
  49 module SetSet = Set.Make (StringSet)
  50 ;;
  51
  52
  53 (*
  54   module SetSet :
  55   sig
  56     type elt = StringSet.t
  57     and t = Set.Make(StringSet).t
  58     val empty : t
  59     val is_empty : t -> bool
  60     val mem : elt -> t -> bool
  61     val add : elt -> t -> t
  62     val singleton : elt -> t
  63     val remove : elt -> t -> t
  64     val union : t -> t -> t
  65     val inter : t -> t -> t
  66     val diff : t -> t -> t
  67     val compare : t -> t -> int
  68     val equal : t -> t -> bool
  69     val subset : t -> t -> bool
  70     val iter : (elt -> unit) -> t -> unit
  71     val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
  72     val for_all : (elt -> bool) -> t -> bool
  73     val exists : (elt -> bool) -> t -> bool
  74     val filter : (elt -> bool) -> t -> t
  75     val partition : (elt -> bool) -> t -> t * t
  76     val cardinal : t -> int
  77     val elements : t -> elt list
  78     val min_elt : t -> elt
  79     val max_elt : t -> elt
  80     val choose : t -> elt
  81   end
  82 *)
  83
  84 let pp_StringSet set =
  85   if (StringSet.is_empty set) then "EMPTY"
  86   else
  87     "{" ^ (String.concat "," (StringSet.elements set)) ^ "}"
  88 ;;
  89
  90 let pp_SetSet set =
  91   let el = List.map pp_StringSet (SetSet.elements set) in
  92   "{" ^ (String.concat ",\n" el) ^ "}"
  93 ;;
  94
  95 let pp_prefix (n,l) =
  96   (string_of_int n) ^
  97   ": {" ^ (String.concat "," l) ^ "}"
  98
  99 let pp_prefixes l =
 100   let el = List.map pp_prefix l in
 101   "{" ^ (String.concat ",\n" el) ^ "}"
 102
 103
 104
 105 let filter_by_card n =
 106   SetSet.filter (fun t -> (StringSet.cardinal t) <= n)
 107 ;;
 108
 109 let merge n a b =
 110   let init = SetSet.union a b in
 111   let merge_single_set s1 b =
 112     SetSet.fold
 113       (fun s2 res -> SetSet.add (StringSet.union s1 s2) res)
 114       b SetSet.empty in
 115   let res =
 116     SetSet.fold (fun s1 res -> SetSet.union (merge_single_set s1 b) res) a init
 117   in
 118   filter_by_card n res
 119 ;;
 120
 121 let mutinduri u t =
 122   (UriManager.string_of_uri u) ^ "#xpointer(1/" ^ (string_of_int (t+1)) ^ ")"
 123 ;;
 124
 125 let mutconstructuri u t c =
 126   (UriManager.string_of_uri u)
 127   ^ "#xpointer(1/" ^ (string_of_int (t+1)) ^ "/" ^ (string_of_int c) ^ ")"
 128 ;;
 129
 130 let rec inspect_children n childs =
 131   List.fold_left
 132     (fun res term -> merge n (inspect_conclusion n term) res)
 133     SetSet.empty childs
 134
 135 and add_root n root childs =
 136   let childunion = inspect_children n childs in
 137   let addroot = StringSet.add root in
 138     SetSet.fold
 139       (fun child newsets -> SetSet.add (addroot child) newsets)
 140       childunion
 141       (SetSet.singleton (StringSet.singleton root))
 142
 143 and inspect_conclusion n t =
 144 if n = 0 then SetSet.empty
 145 else match t with
 146       Cic.Rel _
 147     | Cic.Meta _
 148     | Cic.Sort _
 149     | Cic.Implicit _ -> SetSet.empty
 150     | Cic.Var (u,exp_named_subst) -> SetSet.empty
 151     | Cic.Const (u,exp_named_subst) ->
 152         SetSet.singleton (StringSet.singleton (UriManager.string_of_uri u))
 153     | Cic.MutInd (u, t, exp_named_subst) ->
 154         SetSet.singleton (StringSet.singleton (mutinduri u t))
 155     | Cic.MutConstruct (u, t, c, exp_named_subst) ->
 156         SetSet.singleton (StringSet.singleton (mutconstructuri u t c))
 157     | Cic.Cast (t, _) -> inspect_conclusion n t
 158     | Cic.Prod (_, s, t) ->
 159         merge n (inspect_conclusion n s) (inspect_conclusion n t)
 160     | Cic.Lambda (_, s, t) ->
 161         merge n (inspect_conclusion n s) (inspect_conclusion n t)
 162     | Cic.LetIn (_, s, t) ->
 163         merge n (inspect_conclusion n s) (inspect_conclusion n t)
 164     | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
 165         let suri = UriManager.string_of_uri u in
 166         add_root (n-1) suri l
 167     | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
 168         let suri = mutinduri u t in
 169         add_root (n-1) suri l
 170     | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
 171         let suri = mutconstructuri u t c in
 172         add_root (n-1) suri l
 173     | Cic.Appl l ->
 174         SetSet.empty
 175     | Cic.MutCase (u, t, tt, uu, m) ->
 176         SetSet.empty
 177     | Cic.Fix (_, m) ->
 178         SetSet.empty
 179     | Cic.CoFix (_, m) ->
 180         SetSet.empty
 181 ;;
 182
 183 let rec inspect_term n t =
 184 if n = 0 then assert false
 185 else match t with
 186       Cic.Rel _
 187     | Cic.Meta _
 188     | Cic.Sort _
 189     | Cic.Implicit _ -> None, SetSet.empty
 190     | Cic.Var (u,exp_named_subst) -> None, SetSet.empty
 191     | Cic.Const (u,exp_named_subst) ->
 192         Some (UriManager.string_of_uri u), SetSet.empty
 193     | Cic.MutInd (u, t, exp_named_subst) ->
 194         Some (mutinduri u t), SetSet.empty
 195     | Cic.MutConstruct (u, t, c, exp_named_subst) ->
 196         Some (mutconstructuri u t c), SetSet.empty
 197     | Cic.Cast (t, _) -> inspect_term n t
 198     | Cic.Prod (_, _, t) -> inspect_term n t
 199     | Cic.LetIn (_, _, t) -> inspect_term n t
 200     | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
 201         let suri = UriManager.string_of_uri u in
 202         let childunion = inspect_children (n-1) l in
 203         Some suri, childunion
 204     | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
 205         let suri = mutinduri u t in
 206         if u = HelmLibraryObjects.Logic.eq_URI && n>1 then
 207           (* equality is handled in a special way: in particular,
 208              the type, if defined, is always added to the prefix,
 209              and n is not decremented - it should have been n-2 *)
 210           match l with
 211               Cic.Const (u1,exp_named_subst1)::l1 ->
 212                 let suri1 = UriManager.string_of_uri u1 in
 213                 let inconcl = add_root (n-1) suri1 l1 in
 214                 Some suri, inconcl
 215             | Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
 216                 let suri1 = mutinduri u1 t1 in
 217                 let inconcl = add_root (n-1) suri1 l1 in
 218                 Some suri, inconcl
 219             | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
 220                 let suri1 = mutconstructuri u1 t1 c1 in
 221                 let inconcl = add_root (n-1) suri1 l1 in
 222                 Some suri, inconcl
 223             | _ :: _ -> Some suri, SetSet.empty
 224             | _ -> assert false (* args number must be > 0 *)
 225         else
 226           let childunion = inspect_children (n-1) l in
 227           Some suri, childunion
 228     | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
 229         let suri = mutconstructuri u t c in
 230         let childunion = inspect_children (n-1) l in
 231         Some suri, childunion
 232     | _ -> None, SetSet.empty
 233
 234 let rec add uri children =
 235   List.fold_left
 236     (fun acc t ->
 237        StringSet.union (constants_concl t) acc)
 238     (StringSet.singleton uri) children
 239
 240 (* this function creates the set of all different constants appearing in
 241    the conclusion of the term *)
 242 and constants_concl =
 243   function
 244       Cic.Rel _
 245     | Cic.Meta _
 246     | Cic.Sort _
 247     | Cic.Implicit _ -> StringSet.empty
 248     | Cic.Var (u,exp_named_subst) -> StringSet.empty
 249     | Cic.Const (u,exp_named_subst) ->
 250         StringSet.singleton (UriManager.string_of_uri u)
 251     | Cic.MutInd (u, t, exp_named_subst) ->
 252         StringSet.singleton (mutinduri u t)
 253     | Cic.MutConstruct (u, t, c, exp_named_subst) ->
 254         StringSet.singleton (mutconstructuri u t c)
 255     | Cic.Cast (t, _) -> constants_concl t
 256     | Cic.Prod (_, s, t) ->
 257         StringSet.union (constants_concl s) (constants_concl t)
 258     | Cic.Lambda (_, s, t) ->
 259         StringSet.union (constants_concl s) (constants_concl t)
 260     | Cic.LetIn (_, s, t) ->
 261         StringSet.union (constants_concl s) (constants_concl t)
 262     | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
 263         let suri = UriManager.string_of_uri u in
 264           add suri l
 265     | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
 266         let suri = mutinduri u t in
 267         add suri l
 268     | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
 269         let suri = mutconstructuri u t c in
 270         add suri l
 271     | Cic.Appl l ->
 272         StringSet.empty
 273     | Cic.MutCase (u, t, tt, uu, m) ->
 274         StringSet.empty
 275     | Cic.Fix (_, m) ->
 276         StringSet.empty
 277     | Cic.CoFix (_, m) ->
 278         StringSet.empty
 279 ;;
 280
 281 (* (constants_of t) returns a pair (b,n) where n is the number of
 282    constants in the conclusion of t, and b is true if in MainConclusion
 283    we have an equality *)
 284
 285 let rec constants_of = function
 286   | Cic.Cast (t, _)      -> constants_of t
 287   | Cic.Prod (_, _, t)   -> constants_of t
 288   | Cic.LetIn (_, _, t) -> constants_of t
 289   | (Cic.Appl ((Cic.MutInd (u, _, _))::l)) as t when
 290      u = HelmLibraryObjects.Logic.eq_URI ->
 291       (true, constants_concl t)
 292   | t -> (false, constants_concl t)
 293 ;;
 294
 295
 296 let add_cardinality s =
 297   let l = SetSet.elements s in
 298   let res =
 299     List.map
 300       (fun set ->
 301          let el = StringSet.elements set in
 302          (List.length el, el)) l in
 303     (* ordered by descending cardinality *)
 304     List.sort (fun (n,_) (m,_) -> m - n) ((0,[])::res)
 305 ;;
 306
 307 let prefixes n t =
 308   match inspect_term n t with
 309       Some a, set -> Some a, add_cardinality set
 310     | None, set when (SetSet.is_empty set) -> None, []
 311     | _, _ -> assert false
 312 ;;