helm/ocaml/paramodulation/utils.ml

   1 let debug = true;;
   2
   3 let debug_print = if debug then prerr_endline else ignore;;
   4
   5
   6 let print_metasenv metasenv =
   7   String.concat "\n--------------------------\n"
   8     (List.map (fun (i, context, term) ->
   9                  (string_of_int i) ^ " [\n" ^ (CicPp.ppcontext context) ^
  10                    "\n] " ^  (CicPp.ppterm term))
  11        metasenv)
  12 ;;
  13
  14
  15 let print_subst ?(prefix="\n") subst =
  16   String.concat prefix
  17     (List.map
  18        (fun (i, (c, t, ty)) ->
  19           Printf.sprintf "?%d -> %s : %s" i
  20             (CicPp.ppterm t) (CicPp.ppterm ty))
  21        subst)
  22 ;;
  23
  24 (* (weight of constants, [(meta, weight_of_meta)]) *)
  25 type weight = int * (int * int) list;;
  26
  27 let string_of_weight (cw, mw) =
  28   let s =
  29     String.concat ", "
  30       (List.map (function (m, w) -> Printf.sprintf "(%d,%d)" m w) mw)
  31   in
  32   Printf.sprintf "[%d; %s]" cw s
  33
  34
  35 let weight_of_term ?(consider_metas=true) term =
  36   (* ALB: what to consider as a variable? I think "variables" in our case are
  37      Metas and maybe Rels... *)
  38   let module C = Cic in
  39   let vars_dict = Hashtbl.create 5 in
  40   let rec aux = function
  41     | C.Meta (metano, _) when consider_metas ->
  42         (try
  43            let oldw = Hashtbl.find vars_dict metano in
  44            Hashtbl.replace vars_dict metano (oldw+1)
  45          with Not_found ->
  46            Hashtbl.add vars_dict metano 1);
  47         0
  48     | C.Meta _ -> 0 (* "variables" are lighter than constants and functions...*)
  49
  50     | C.Var (_, ens)
  51     | C.Const (_, ens)
  52     | C.MutInd (_, _, ens)
  53     | C.MutConstruct (_, _, _, ens) ->
  54         List.fold_left (fun w (u, t) -> (aux t) + w) 1 ens
  55
  56     | C.Cast (t1, t2)
  57     | C.Lambda (_, t1, t2)
  58     | C.Prod (_, t1, t2)
  59     | C.LetIn (_, t1, t2) ->
  60         let w1 = aux t1 in
  61         let w2 = aux t2 in
  62         w1 + w2 + 1
  63
  64     | C.Appl l -> List.fold_left (+) 0 (List.map aux l)
  65
  66     | C.MutCase (_, _, outt, t, pl) ->
  67         let w1 = aux outt in
  68         let w2 = aux t in
  69         let w3 = List.fold_left (+) 0 (List.map aux pl) in
  70         w1 + w2 + w3 + 1
  71
  72     | C.Fix (_, fl) ->
  73         List.fold_left (fun w (n, i, t1, t2) -> (aux t1) + (aux t2) + w) 1 fl
  74
  75     | C.CoFix (_, fl) ->
  76         List.fold_left (fun w (n, t1, t2) -> (aux t1) + (aux t2) + w) 1 fl
  77
  78     | _ -> 1
  79   in
  80   let w = aux term in
  81   let l =
  82     Hashtbl.fold (fun meta metaw resw -> (meta, metaw)::resw) vars_dict [] in
  83   let compare w1 w2 =
  84     match w1, w2 with
  85     | (m1, _), (m2, _) -> m2 - m1
  86   in
  87   (w, List.sort compare l) (* from the biggest meta to the smallest (0) *)
  88 ;;
  89
  90
  91 let compute_equality_weight ty left right =
  92   let metasw = ref 0 in
  93   let weight_of t =
  94     let w, m = (weight_of_term ~consider_metas:true(* false *) t) in
  95 (*     let mw = List.fold_left (fun mw (_, c) -> mw + 2 * c) 0 m in *)
  96 (*     metasw := !metasw + mw; *)
  97     metasw := !metasw + (2 * (List.length m));
  98     w
  99   in
 100   (weight_of ty) + (weight_of left) + (weight_of right) + !metasw
 101 ;;
 102
 103
 104 (* returns a "normalized" version of the polynomial weight wl (with type
 105  * weight list), i.e. a list sorted ascending by meta number,
 106  * from 0 to maxmeta. wl must be sorted descending by meta number. Example:
 107  * normalize_weight 5 (3, [(3, 2); (1, 1)]) ->
 108  *      (3, [(1, 1); (2, 0); (3, 2); (4, 0); (5, 0)]) *)
 109 let normalize_weight maxmeta (cw, wl) =
 110 (*   Printf.printf "normalize_weight: %d, %s\n" maxmeta *)
 111 (*     (string_of_weight (cw, wl)); *)
 112   let rec aux = function
 113     | 0 -> []
 114     | m -> (m, 0)::(aux (m-1))
 115   in
 116   let tmpl = aux maxmeta in
 117   let wl =
 118     List.sort
 119       (fun (m, _) (n, _) -> Pervasives.compare m n)
 120       (List.fold_left
 121          (fun res (m, w) -> (m, w)::(List.remove_assoc m res)) tmpl wl)
 122   in
 123   (cw, wl)
 124 ;;
 125
 126
 127 let normalize_weights (cw1, wl1) (cw2, wl2) =
 128   let rec aux wl1 wl2 =
 129     match wl1, wl2 with
 130     | [], [] -> [], []
 131     | (m, w)::tl1, (n, w')::tl2 when m = n ->
 132         let res1, res2 = aux tl1 tl2 in
 133         (m, w)::res1, (n, w')::res2
 134     | (m, w)::tl1, ((n, w')::_ as wl2) when m < n ->
 135         let res1, res2 = aux tl1 wl2 in
 136         (m, w)::res1, (m, 0)::res2
 137     | ((m, w)::_ as wl1), (n, w')::tl2 when m > n ->
 138         let res1, res2 = aux wl1 tl2 in
 139         (n, 0)::res1, (n, w')::res2
 140     | [], (n, w)::tl2 ->
 141         let res1, res2 = aux [] tl2 in
 142         (n, 0)::res1, (n, w)::res2
 143     | (m, w)::tl1, [] ->
 144         let res1, res2 = aux tl1 [] in
 145         (m, w)::res1, (m, 0)::res2
 146   in
 147   let cmp (m, _) (n, _) = compare m n in
 148   let wl1, wl2 = aux (List.sort cmp wl1) (List.sort cmp wl2) in
 149   (cw1, wl1), (cw2, wl2)
 150 ;;
 151
 152
 153 type comparison = Lt | Le | Eq | Ge | Gt | Incomparable;;
 154
 155 let string_of_comparison = function
 156   | Lt -> "<"
 157   | Le -> "<="
 158   | Gt -> ">"
 159   | Ge -> ">="
 160   | Eq -> "="
 161   | Incomparable -> "I"
 162
 163
 164 let compare_weights ?(normalize=false)
 165     ((h1, w1) as weight1) ((h2, w2) as weight2)=
 166   let (h1, w1), (h2, w2) =
 167     if normalize then
 168 (*       let maxmeta =  *)
 169 (*         let maxmeta l = *)
 170 (*           try *)
 171 (*             match List.hd l with *)
 172 (*             | (m, _) -> m *)
 173 (*           with Failure _ -> 0 *)
 174 (*         in *)
 175 (*         max (maxmeta w1) (maxmeta w2) *)
 176 (*       in *)
 177 (*       (normalize_weight maxmeta (h1, w1)), (normalize_weight maxmeta (h2, w2)) *)
 178       normalize_weights weight1 weight2
 179     else
 180       (h1, w1), (h2, w2)
 181   in
 182   let res, diffs =
 183     try
 184       List.fold_left2
 185         (fun ((lt, eq, gt), diffs) w1 w2 ->
 186            match w1, w2 with
 187            | (meta1, w1), (meta2, w2) when meta1 = meta2 ->
 188                let diffs = (w1 - w2) + diffs in
 189                let r = compare w1 w2 in
 190                if r < 0 then (lt+1, eq, gt), diffs
 191                else if r = 0 then (lt, eq+1, gt), diffs
 192                else (lt, eq, gt+1), diffs
 193            | (meta1, w1), (meta2, w2) ->
 194                Printf.printf "HMMM!!!! %s, %s\n"
 195                  (string_of_weight weight1) (string_of_weight weight2);
 196                assert false)
 197         ((0, 0, 0), 0) w1 w2
 198     with Invalid_argument _ ->
 199       Printf.printf "Invalid_argument: %s{%s}, %s{%s}, normalize = %s\n"
 200         (string_of_weight (h1, w1)) (string_of_weight weight1)
 201         (string_of_weight (h2, w2)) (string_of_weight weight2)
 202         (string_of_bool normalize);
 203       assert false
 204   in
 205   let hdiff = h1 - h2 in
 206   match res with
 207   | (0, _, 0) ->
 208       if hdiff < 0 then Lt
 209       else if hdiff > 0 then Gt
 210       else Eq (* Incomparable *)
 211   | (m, _, 0) ->
 212       if hdiff <= 0 then
 213         if m > 0 || hdiff < 0 then Lt
 214         else if diffs >= (- hdiff) then Le else Incomparable
 215       else
 216         if diffs >= (- hdiff) then Le else Incomparable
 217   | (0, _, m) ->
 218       if hdiff >= 0 then
 219         if m > 0 || hdiff > 0 then Gt
 220         else if (- diffs) >= hdiff then Ge else Incomparable
 221       else
 222         if (- diffs) >= hdiff then Ge else Incomparable
 223   | (m, _, n) when m > 0 && n > 0 ->
 224       Incomparable
 225 ;;
 226
 227
 228 let rec aux_ordering t1 t2 =
 229   let module C = Cic in
 230   let compare_uris u1 u2 =
 231     let res =
 232       compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2) in
 233     if res < 0 then Lt
 234     else if res = 0 then Eq
 235     else Gt
 236   in
 237   match t1, t2 with
 238   | C.Meta _, _
 239   | _, C.Meta _ -> Incomparable
 240
 241   | t1, t2 when t1 = t2 -> Eq
 242
 243   | C.Rel n, C.Rel m -> if n > m then Lt else Gt
 244   | C.Rel _, _ -> Lt
 245   | _, C.Rel _ -> Gt
 246
 247   | C.Const (u1, _), C.Const (u2, _) -> compare_uris u1 u2
 248   | C.Const _, _ -> Lt
 249   | _, C.Const _ -> Gt
 250
 251   | C.MutInd (u1, _, _), C.MutInd (u2, _, _) -> compare_uris u1 u2
 252   | C.MutInd _, _ -> Lt
 253   | _, C.MutInd _ -> Gt
 254
 255   | C.MutConstruct (u1, _, _, _), C.MutConstruct (u2, _, _, _) ->
 256       compare_uris u1 u2
 257   | C.MutConstruct _, _ -> Lt
 258   | _, C.MutConstruct _ -> Gt
 259
 260   | C.Appl l1, C.Appl l2 ->
 261       let rec cmp t1 t2 =
 262         match t1, t2 with
 263         | [], [] -> Eq
 264         | _, [] -> Gt
 265         | [], _ -> Lt
 266         | hd1::tl1, hd2::tl2 ->
 267             let o = aux_ordering hd1 hd2 in
 268             if o = Eq then cmp tl1 tl2
 269             else o
 270       in
 271       cmp l1 l2
 272
 273   | t1, t2 ->
 274       Printf.printf "These two terms are not comparable:\n%s\n%s\n\n"
 275         (CicPp.ppterm t1) (CicPp.ppterm t2);
 276       Incomparable
 277 ;;
 278
 279
 280 (* w1, w2 are the weights, they should already be normalized... *)
 281 let nonrec_kbo_w (t1, w1) (t2, w2) =
 282   match compare_weights w1 w2 with
 283   | Le -> if aux_ordering t1 t2 = Lt then Lt else Incomparable
 284   | Ge -> if aux_ordering t1 t2 = Gt then Gt else Incomparable
 285   | Eq -> aux_ordering t1 t2
 286   | res -> res
 287 ;;
 288
 289
 290 let nonrec_kbo t1 t2 =
 291   let w1 = weight_of_term t1 in
 292   let w2 = weight_of_term t2 in
 293   match compare_weights ~normalize:true w1 w2 with
 294   | Le -> if aux_ordering t1 t2 = Lt then Lt else Incomparable
 295   | Ge -> if aux_ordering t1 t2 = Gt then Gt else Incomparable
 296   | Eq -> aux_ordering t1 t2
 297   | res -> res
 298 ;;
 299
 300
 301 let names_of_context context =
 302   List.map
 303     (function
 304        | None -> None
 305        | Some (n, e) -> Some n)
 306     context
 307 ;;
 308
 309
 310 module OrderedTerm =
 311 struct
 312   type t = Cic.term
 313
 314   let compare = Pervasives.compare
 315 end
 316
 317 module TermSet = Set.Make(OrderedTerm);;
 318 module TermMap = Map.Make(OrderedTerm);;
 319
 320 let symbols_of_term term =
 321   let module C = Cic in
 322   let rec aux map = function
 323     | C.Meta _ -> map
 324     | C.Appl l ->
 325         List.fold_left (fun res t -> (aux res t)) map l
 326     | t ->
 327         let map =
 328           try
 329             let c = TermMap.find t map in
 330             TermMap.add t (c+1) map
 331           with Not_found ->
 332             TermMap.add t 1 map
 333         in
 334         map
 335   in
 336   aux TermMap.empty term
 337 ;;
 338
 339
 340 let metas_of_term term =
 341   let module C = Cic in
 342   let rec aux = function
 343     | C.Meta _ as t -> TermSet.singleton t
 344     | C.Appl l ->
 345         List.fold_left (fun res t -> TermSet.union res (aux t)) TermSet.empty l
 346     | t -> TermSet.empty (* TODO: maybe add other cases? *)
 347   in
 348   aux term
 349 ;;
 350
 351
 352 let rec lpo t1 t2 =
 353   let module C = Cic in
 354   match t1, t2 with
 355   | t1, t2 when t1 = t2 -> Eq
 356   | t1, (C.Meta _ as m) ->
 357       if TermSet.mem m (metas_of_term t1) then Gt else Incomparable
 358   | (C.Meta _ as m), t2 ->
 359       if TermSet.mem m (metas_of_term t2) then Lt else Incomparable
 360   | C.Appl (hd1::tl1), C.Appl (hd2::tl2) -> (
 361       let res =
 362         let f o r t =
 363           if r then true else
 364             match lpo t o with
 365             | Gt | Eq -> true
 366             | _ -> false
 367         in
 368         let res1 = List.fold_left (f t2) false tl1 in
 369         if res1 then Gt
 370         else let res2 = List.fold_left (f t1) false tl2 in
 371         if res2 then Lt
 372         else Incomparable
 373       in
 374       if res <> Incomparable then
 375         res
 376       else
 377         let f o r t =
 378           if not r then false else
 379             match lpo o t with
 380             | Gt -> true
 381             | _ -> false
 382         in
 383         match aux_ordering hd1 hd2 with
 384         | Gt ->
 385             let res = List.fold_left (f t1) false tl2 in
 386             if res then Gt
 387             else Incomparable
 388         | Lt ->
 389             let res = List.fold_left (f t2) false tl1 in
 390             if res then Lt
 391             else Incomparable
 392         | Eq -> (
 393             let lex_res =
 394               try
 395                 List.fold_left2
 396                   (fun r t1 t2 -> if r <> Eq then r else lpo t1 t2)
 397                   Eq tl1 tl2
 398               with Invalid_argument _ ->
 399                 Incomparable
 400             in
 401             match lex_res with
 402             | Gt ->
 403                 if List.fold_left (f t1) false tl2 then Gt
 404                 else Incomparable
 405             | Lt ->
 406                 if List.fold_left (f t2) false tl1 then Lt
 407                 else Incomparable
 408             | _ -> Incomparable
 409           )
 410         | _ -> Incomparable
 411     )
 412   | t1, t2 -> aux_ordering t1 t2
 413 ;;
 414
 415
 416 (* settable by the user... *)
 417 let compare_terms = ref nonrec_kbo;;
 418
 419
 420 type equality_sign = Negative | Positive;;
 421
 422 let string_of_sign = function
 423   | Negative -> "Negative"
 424   | Positive -> "Positive"
 425 ;;
 426
 427
 428 type pos = Left | Right
 429
 430 let string_of_pos = function
 431   | Left -> "Left"
 432   | Right -> "Right"
 433 ;;