helm/ocaml/paramodulation/inference.ml

   1 open Utils;;
   2
   3
   4 type equality =
   5     Cic.term  *          (* proof *)
   6     (Cic.term *          (* type *)
   7      Cic.term *          (* left side *)
   8      Cic.term *          (* right side *)
   9      Utils.comparison) * (* ordering *)
  10     Cic.metasenv *       (* environment for metas *)
  11     Cic.term list        (* arguments *)
  12 ;;
  13
  14
  15 type proof =
  16   | BasicProof of Cic.term
  17   | ProofBlock of
  18       Cic.substitution * UriManager.uri * Cic.term * (Utils.pos * equality) *
  19         equality
  20   | NoProof
  21 ;;
  22
  23
  24 let string_of_equality ?env =
  25   match env with
  26   | None -> (
  27       function
  28         | _, (ty, left, right, o), _, _ ->
  29             Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.ppterm ty)
  30               (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right)
  31     )
  32   | Some (_, context, _) -> (
  33       let names = names_of_context context in
  34       function
  35         | _, (ty, left, right, o), _, _ ->
  36             Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.pp ty names)
  37               (CicPp.pp left names) (string_of_comparison o)
  38               (CicPp.pp right names)
  39     )
  40 ;;
  41
  42
  43 let prooftable = Hashtbl.create 2001;;
  44
  45 let store_proof equality proof =
  46   if not (Hashtbl.mem prooftable equality) then
  47     Hashtbl.add prooftable equality proof
  48 ;;
  49
  50
  51 let delete_proof equality =
  52 (*   Printf.printf "| Removing proof of %s" (string_of_equality equality); *)
  53 (*   print_newline (); *)
  54   Hashtbl.remove prooftable equality
  55 ;;
  56
  57
  58 let rec build_term_proof equality =
  59 (*   Printf.printf "build_term_proof %s" (string_of_equality equality); *)
  60 (*   print_newline (); *)
  61   let proof = try Hashtbl.find prooftable equality with Not_found -> NoProof in
  62   match proof with
  63   | NoProof ->
  64       Printf.fprintf stderr "WARNING: no proof for %s\n"
  65         (string_of_equality equality);
  66       Cic.Implicit None
  67   | BasicProof term -> term
  68   | ProofBlock (subst, eq_URI, t', (pos, eq), eq') ->
  69 (*       Printf.printf "   ProofBlock: eq = %s, eq' = %s" *)
  70 (*         (string_of_equality eq) (string_of_equality eq'); *)
  71 (*       print_newline (); *)
  72       let proof' = build_term_proof eq in
  73       let eqproof = build_term_proof eq' in
  74       let _, (ty, what, other, _), menv', args' = eq in
  75       let what, other = if pos = Utils.Left then what, other else other, what in
  76       CicMetaSubst.apply_subst subst
  77         (Cic.Appl [Cic.Const (eq_URI, []); ty;
  78                    what; t'; eqproof; other; proof'])
  79 ;;
  80
  81
  82 let rec metas_of_term = function
  83   | Cic.Meta (i, c) -> [i]
  84   | Cic.Var (_, ens)
  85   | Cic.Const (_, ens)
  86   | Cic.MutInd (_, _, ens)
  87   | Cic.MutConstruct (_, _, _, ens) ->
  88       List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
  89   | Cic.Cast (s, t)
  90   | Cic.Prod (_, s, t)
  91   | Cic.Lambda (_, s, t)
  92   | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
  93   | Cic.Appl l -> List.flatten (List.map metas_of_term l)
  94   | Cic.MutCase (uri, i, s, t, l) ->
  95       (metas_of_term s) @ (metas_of_term t) @
  96         (List.flatten (List.map metas_of_term l))
  97   | Cic.Fix (i, il) ->
  98       List.flatten
  99         (List.map (fun (s, i, t1, t2) ->
 100                      (metas_of_term t1) @ (metas_of_term t2)) il)
 101   | Cic.CoFix (i, il) ->
 102       List.flatten
 103         (List.map (fun (s, t1, t2) ->
 104                      (metas_of_term t1) @ (metas_of_term t2)) il)
 105   | _ -> []
 106 ;;
 107
 108
 109 exception NotMetaConvertible;;
 110
 111 let meta_convertibility_aux table t1 t2 =
 112   let module C = Cic in
 113   let print_table t =
 114     String.concat ", "
 115       (List.map
 116          (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
 117   in
 118   let rec aux ((table_l, table_r) as table) t1 t2 =
 119 (*     Printf.printf "aux %s, %s\ntable_l: %s, table_r: %s\n" *)
 120 (*       (CicPp.ppterm t1) (CicPp.ppterm t2) *)
 121 (*       (print_table table_l) (print_table table_r); *)
 122     match t1, t2 with
 123     | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
 124         let m1_binding, table_l =
 125           try List.assoc m1 table_l, table_l
 126           with Not_found -> m2, (m1, m2)::table_l
 127         and m2_binding, table_r =
 128           try List.assoc m2 table_r, table_r
 129           with Not_found -> m1, (m2, m1)::table_r
 130         in
 131 (*         let m1_binding, m2_binding, table = *)
 132 (*           let m1b, table =  *)
 133 (*             try List.assoc m1 table, table *)
 134 (*             with Not_found -> m2, (m1, m2)::table *)
 135 (*           in *)
 136 (*           let m2b, table =  *)
 137 (*             try List.assoc m2 table, table *)
 138 (*             with Not_found -> m1, (m2, m1)::table *)
 139 (*           in *)
 140 (*           m1b, m2b, table *)
 141 (*         in *)
 142 (*         Printf.printf "table_l: %s\ntable_r: %s\n\n" *)
 143 (*           (print_table table_l) (print_table table_r); *)
 144         if (m1_binding <> m2) || (m2_binding <> m1) then
 145           raise NotMetaConvertible
 146         else (
 147           try
 148             List.fold_left2
 149               (fun res t1 t2 ->
 150                  match t1, t2 with
 151                  | None, Some _ | Some _, None -> raise NotMetaConvertible
 152                  | None, None -> res
 153                  | Some t1, Some t2 -> (aux res t1 t2))
 154               (table_l, table_r) tl1 tl2
 155           with Invalid_argument _ ->
 156             raise NotMetaConvertible
 157         )
 158     | C.Var (u1, ens1), C.Var (u2, ens2)
 159     | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
 160         aux_ens table ens1 ens2
 161     | C.Cast (s1, t1), C.Cast (s2, t2)
 162     | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
 163     | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
 164     | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
 165         let table = aux table s1 s2 in
 166         aux table t1 t2
 167     | C.Appl l1, C.Appl l2 -> (
 168         try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
 169         with Invalid_argument _ -> raise NotMetaConvertible
 170       )
 171     | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
 172         when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
 173     | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
 174         when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
 175         aux_ens table ens1 ens2
 176     | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
 177         when (UriManager.eq u1 u2) && i1 = i2 ->
 178         let table = aux table s1 s2 in
 179         let table = aux table t1 t2 in (
 180           try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
 181           with Invalid_argument _ -> raise NotMetaConvertible
 182         )
 183     | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
 184         try
 185           List.fold_left2
 186             (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
 187                if i1 <> i2 then raise NotMetaConvertible
 188                else
 189                  let res = (aux res s1 s2) in aux res t1 t2)
 190             table il1 il2
 191         with Invalid_argument _ -> raise NotMetaConvertible
 192       )
 193     | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
 194         try
 195           List.fold_left2
 196             (fun res (n1, s1, t1) (n2, s2, t2) ->
 197                let res = aux res s1 s2 in aux res t1 t2)
 198             table il1 il2
 199         with Invalid_argument _ -> raise NotMetaConvertible
 200       )
 201     | t1, t2 when t1 = t2 -> table
 202     | _, _ -> raise NotMetaConvertible
 203
 204   and aux_ens table ens1 ens2 =
 205     let cmp (u1, t1) (u2, t2) =
 206       compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
 207     in
 208     let ens1 = List.sort cmp ens1
 209     and ens2 = List.sort cmp ens2 in
 210     try
 211       List.fold_left2
 212         (fun res (u1, t1) (u2, t2) ->
 213            if not (UriManager.eq u1 u2) then raise NotMetaConvertible
 214            else aux res t1 t2)
 215         table ens1 ens2
 216     with Invalid_argument _ -> raise NotMetaConvertible
 217   in
 218   aux table t1 t2
 219 ;;
 220
 221
 222 let meta_convertibility_eq eq1 eq2 =
 223   let _, (ty, left, right, _), _, _ = eq1
 224   and _, (ty', left', right', _), _, _ = eq2 in
 225   if ty <> ty' then
 226     false
 227   else if (left = left') && (right = right') then
 228     true
 229   else if (left = right') && (right = left') then
 230     true
 231   else
 232     try
 233       let table = meta_convertibility_aux ([], []) left left' in
 234       let _ = meta_convertibility_aux table right right' in
 235       true
 236     with NotMetaConvertible ->
 237       try
 238         let table = meta_convertibility_aux ([], []) left right' in
 239         let _ = meta_convertibility_aux table right left' in
 240         true
 241       with NotMetaConvertible ->
 242         false
 243 ;;
 244
 245
 246 let meta_convertibility t1 t2 =
 247   let f t =
 248     String.concat ", "
 249       (List.map
 250          (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t)
 251   in
 252   if t1 = t2 then
 253     true
 254   else
 255     try
 256       let l, r = meta_convertibility_aux ([], []) t1 t2 in
 257       (*     Printf.printf "meta_convertibility:\n%s\n%s\n\n" (f l) (f r); *)
 258       true
 259     with NotMetaConvertible ->
 260       false
 261 ;;
 262
 263
 264 let replace_metas (* context *) term =
 265   let module C = Cic in
 266   let rec aux = function
 267     | C.Meta (i, c) ->
 268 (*         let irl = *)
 269 (*           CicMkImplicit.identity_relocation_list_for_metavariable context *)
 270 (*         in *)
 271 (*         if c = irl then *)
 272 (*           C.Implicit (Some (`MetaIndex i)) *)
 273 (*         else ( *)
 274 (*           Printf.printf "WARNING: c non e` un identity_relocation_list!\n%s\n" *)
 275 (*             (String.concat "\n" *)
 276 (*                (List.map *)
 277 (*                   (function None -> "" | Some t -> CicPp.ppterm t) c)); *)
 278 (*           C.Meta (i, c) *)
 279 (*         ) *)
 280         C.Implicit (Some (`MetaInfo (i, c)))
 281     | C.Var (u, ens) -> C.Var (u, aux_ens ens)
 282     | C.Const (u, ens) -> C.Const (u, aux_ens ens)
 283     | C.Cast (s, t) -> C.Cast (aux s, aux t)
 284     | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
 285     | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
 286     | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
 287     | C.Appl l -> C.Appl (List.map aux l)
 288     | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
 289     | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
 290     | C.MutCase (uri, i, s, t, l) ->
 291         C.MutCase (uri, i, aux s, aux t, List.map aux l)
 292     | C.Fix (i, il) ->
 293         let il' =
 294           List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
 295         C.Fix (i, il')
 296     | C.CoFix (i, il) ->
 297         let il' =
 298           List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
 299         C.CoFix (i, il')
 300     | t -> t
 301   and aux_ens ens =
 302     List.map (fun (u, t) -> (u, aux t)) ens
 303   in
 304   aux term
 305 ;;
 306
 307
 308 let restore_metas (* context *) term =
 309   let module C = Cic in
 310   let rec aux = function
 311     | C.Implicit (Some (`MetaInfo (i, c))) ->
 312 (*         let c = *)
 313 (*           CicMkImplicit.identity_relocation_list_for_metavariable context *)
 314 (*         in *)
 315 (*         C.Meta (i, c) *)
 316 (*         let local_context:(C.term option) list = *)
 317 (*           Marshal.from_string mc 0 *)
 318 (*         in *)
 319 (*         C.Meta (i, local_context) *)
 320         C.Meta (i, c)
 321     | C.Var (u, ens) -> C.Var (u, aux_ens ens)
 322     | C.Const (u, ens) -> C.Const (u, aux_ens ens)
 323     | C.Cast (s, t) -> C.Cast (aux s, aux t)
 324     | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t)
 325     | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t)
 326     | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t)
 327     | C.Appl l -> C.Appl (List.map aux l)
 328     | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens)
 329     | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens)
 330     | C.MutCase (uri, i, s, t, l) ->
 331         C.MutCase (uri, i, aux s, aux t, List.map aux l)
 332     | C.Fix (i, il) ->
 333         let il' =
 334           List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in
 335         C.Fix (i, il')
 336     | C.CoFix (i, il) ->
 337         let il' =
 338           List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in
 339         C.CoFix (i, il')
 340     | t -> t
 341   and aux_ens ens =
 342     List.map (fun (u, t) -> (u, aux t)) ens
 343   in
 344   aux term
 345 ;;
 346
 347
 348 let rec restore_subst (* context *) subst =
 349   List.map
 350     (fun (i, (c, t, ty)) ->
 351        i, (c, restore_metas (* context *) t, ty))
 352     subst
 353 ;;
 354
 355
 356 let rec check_irl start = function
 357   | [] -> true
 358   | None::tl -> check_irl (start+1) tl
 359   | (Some (Cic.Rel x))::tl ->
 360       if x = start then check_irl (start+1) tl else false
 361   | _ -> false
 362 ;;
 363
 364 let rec is_simple_term = function
 365   | Cic.Appl ((Cic.Meta _)::_) -> false
 366   | Cic.Appl l -> List.for_all is_simple_term l
 367   | Cic.Meta (i, l) -> check_irl 1 l
 368   | Cic.Rel _ -> true
 369   | _ -> false
 370 ;;
 371
 372
 373 let lookup_subst meta subst =
 374   match meta with
 375   | Cic.Meta (i, _) -> (
 376       try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
 377       with Not_found -> meta
 378     )
 379   | _ -> assert false
 380 ;;
 381
 382
 383 let unification_simple metasenv context t1 t2 ugraph =
 384   let module C = Cic in
 385   let module M = CicMetaSubst in
 386   let module U = CicUnification in
 387   let lookup = lookup_subst in
 388   let rec occurs_check subst what where =
 389     (*       Printf.printf "occurs_check %s %s" *)
 390     (*         (CicPp.ppterm what) (CicPp.ppterm where); *)
 391     (*       print_newline (); *)
 392     match where with
 393     | t when what = t -> true
 394     | C.Appl l -> List.exists (occurs_check subst what) l
 395     | C.Meta _ ->
 396         let t = lookup where subst in
 397         if t <> where then occurs_check subst what t else false
 398     | _ -> false
 399   in
 400   let rec unif subst menv s t =
 401 (*     Printf.printf "unif %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
 402 (*       (print_subst subst); *)
 403 (*     print_newline (); *)
 404     let s = match s with C.Meta _ -> lookup s subst | _ -> s
 405     and t = match t with C.Meta _ -> lookup t subst | _ -> t
 406     in
 407     (*       Printf.printf "after apply_subst: %s %s\n%s" *)
 408     (*         (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
 409     (*       print_newline (); *)
 410     match s, t with
 411     | s, t when s = t -> subst, menv
 412     | C.Meta (i, _), C.Meta (j, _) when i > j ->
 413         unif subst menv t s
 414     | C.Meta _, t when occurs_check subst s t ->
 415         raise (U.UnificationFailure "Inference.unification.unif")
 416 (*     | C.Meta (i, l), C.Meta (j, l') -> *)
 417 (*         let _, _, ty = CicUtil.lookup_meta i menv in *)
 418 (*         let _, _, ty' = CicUtil.lookup_meta j menv in *)
 419 (*         let binding1 = lookup s subst in *)
 420 (*         let binding2 = lookup t subst in *)
 421 (*         let subst, menv =  *)
 422 (*           if binding1 != s then *)
 423 (*             if binding2 != t then *)
 424 (*               unif subst menv binding1 binding2 *)
 425 (*             else *)
 426 (*               if binding1 = t then *)
 427 (*                 subst, menv *)
 428 (*               else *)
 429 (*                 ((j, (context, binding1, ty'))::subst, *)
 430 (*                  List.filter (fun (m, _, _) -> j <> m) menv) *)
 431 (*           else *)
 432 (*             if binding2 != t then *)
 433 (*               if s = binding2 then *)
 434 (*                 subst, menv *)
 435 (*               else *)
 436 (*                 ((i, (context, binding2, ty))::subst, *)
 437 (*                  List.filter (fun (m, _, _) -> i <> m) menv) *)
 438 (*             else *)
 439 (*               ((i, (context, t, ty))::subst, *)
 440 (*                List.filter (fun (m, _, _) -> i <> m) menv) *)
 441 (*         in *)
 442 (*         subst, menv *)
 443
 444     | C.Meta (i, l), t ->
 445         let _, _, ty = CicUtil.lookup_meta i menv in
 446         let subst =
 447           if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst
 448           else subst
 449         in
 450         let menv = List.filter (fun (m, _, _) -> i <> m) menv in
 451         subst, menv
 452     | _, C.Meta _ -> unif subst menv t s
 453     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
 454         raise (U.UnificationFailure "Inference.unification.unif")
 455     | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
 456         try
 457           List.fold_left2
 458             (fun (subst', menv) s t -> unif subst' menv s t)
 459             (subst, menv) tls tlt
 460         with e ->
 461           raise (U.UnificationFailure "Inference.unification.unif")
 462       )
 463     | _, _ -> raise (U.UnificationFailure "Inference.unification.unif")
 464   in
 465   let subst, menv = unif [] metasenv t1 t2 in
 466   (*     Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
 467   (*     print_newline (); *)
 468 (*   let rec fix_term = function *)
 469 (*     | (C.Meta (i, l) as t) -> *)
 470 (*         lookup t subst *)
 471 (*     | C.Appl l -> C.Appl (List.map fix_term l) *)
 472 (*     | t -> t *)
 473 (*   in *)
 474 (*   let rec fix_subst = function *)
 475 (*     | [] -> [] *)
 476 (*     | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl) *)
 477 (*   in *)
 478 (*   List.rev (fix_subst subst), menv, ugraph *)
 479   List.rev subst, menv, ugraph
 480 ;;
 481
 482
 483 let unification metasenv context t1 t2 ugraph =
 484 (*   Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
 485   let subst, menv, ug =
 486     if not (is_simple_term t1) || not (is_simple_term t2) then
 487       CicUnification.fo_unif metasenv context t1 t2 ugraph
 488     else
 489       unification_simple metasenv context t1 t2 ugraph
 490   in
 491   let rec fix_term = function
 492     | (Cic.Meta (i, l) as t) ->
 493         let t' = lookup_subst t subst in
 494         if t <> t' then fix_term t' else t
 495     | Cic.Appl l -> Cic.Appl (List.map fix_term l)
 496     | t -> t
 497   in
 498   let rec fix_subst = function
 499     | [] -> []
 500     | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl)
 501   in
 502 (*   Printf.printf "| subst: %s\n" (print_subst ~prefix:" ; " subst); *)
 503 (*   print_endline "|"; *)
 504   (* fix_subst *) subst, menv, ug
 505 ;;
 506
 507 (* let unification = CicUnification.fo_unif;; *)
 508
 509 exception MatchingFailure;;
 510
 511
 512 let matching_simple metasenv context t1 t2 ugraph =
 513   let module C = Cic in
 514   let module M = CicMetaSubst in
 515   let module U = CicUnification in
 516   let lookup meta subst =
 517     match meta with
 518     | C.Meta (i, _) -> (
 519         try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
 520         with Not_found -> meta
 521       )
 522     | _ -> assert false
 523   in
 524   let rec do_match subst menv s t =
 525 (*     Printf.printf "do_match %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
 526 (*       (print_subst subst); *)
 527 (*     print_newline (); *)
 528 (*     let s = match s with C.Meta _ -> lookup s subst | _ -> s *)
 529 (*     let t = match t with C.Meta _ -> lookup t subst | _ -> t in  *)
 530     (*       Printf.printf "after apply_subst: %s %s\n%s" *)
 531     (*         (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
 532     (*       print_newline (); *)
 533     match s, t with
 534     | s, t when s = t -> subst, menv
 535 (*     | C.Meta (i, _), C.Meta (j, _) when i > j -> *)
 536 (*         do_match subst menv t s *)
 537 (*     | C.Meta _, t when occurs_check subst s t -> *)
 538 (*         raise MatchingFailure *)
 539 (*     | s, C.Meta _ when occurs_check subst t s -> *)
 540 (*         raise MatchingFailure *)
 541     | s, C.Meta (i, l) ->
 542         let filter_menv i menv =
 543           List.filter (fun (m, _, _) -> i <> m) menv
 544         in
 545         let subst, menv =
 546           let value = lookup t subst in
 547           match value with
 548 (*           | C.Meta (i', l') when Hashtbl.mem table i' -> *)
 549 (*               (i', (context, s, ty))::subst, menv (\* filter_menv i' menv *\) *)
 550           | value when value = t ->
 551               let _, _, ty = CicUtil.lookup_meta i menv in
 552               (i, (context, s, ty))::subst, filter_menv i menv
 553           | value when value <> s ->
 554               raise MatchingFailure
 555           | value -> do_match subst menv s value
 556         in
 557         subst, menv
 558 (*           else if value <> s then *)
 559 (*             raise MatchingFailure *)
 560 (*           else subst *)
 561 (*           if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst *)
 562 (*           else subst *)
 563 (*         in *)
 564 (*         let menv = List.filter (fun (m, _, _) -> i <> m) menv in *)
 565 (*         subst, menv *)
 566 (*     | _, C.Meta _ -> do_match subst menv t s *)
 567 (*     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt -> *)
 568 (*         raise MatchingFailure *)
 569     | C.Appl ls, C.Appl lt -> (
 570         try
 571           List.fold_left2
 572             (fun (subst, menv) s t -> do_match subst menv s t)
 573             (subst, menv) ls lt
 574         with e ->
 575 (*           print_endline (Printexc.to_string e); *)
 576 (*           Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
 577 (*           print_newline ();           *)
 578           raise MatchingFailure
 579       )
 580     | _, _ ->
 581 (*         Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
 582 (*         print_newline (); *)
 583         raise MatchingFailure
 584   in
 585   let subst, menv = do_match [] metasenv t1 t2 in
 586   (*     Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
 587   (*     print_newline (); *)
 588   subst, menv, ugraph
 589 ;;
 590
 591
 592 let matching metasenv context t1 t2 ugraph =
 593 (*   if (is_simple_term t1) && (is_simple_term t2) then *)
 594 (*     let subst, menv, ug = *)
 595 (*       matching_simple metasenv context t1 t2 ugraph in *)
 596 (* (\*     Printf.printf "matching %s %s:\n%s\n" *\) *)
 597 (* (\*       (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *\) *)
 598 (* (\*     print_newline (); *\) *)
 599 (*     subst, menv, ug *)
 600 (*   else *)
 601     try
 602       let subst, metasenv, ugraph =
 603         (*       CicUnification.fo_unif metasenv context t1 t2 ugraph *)
 604         unification metasenv context t1 t2 ugraph
 605       in
 606       let t' = CicMetaSubst.apply_subst subst t1 in
 607       if not (meta_convertibility t1 t') then
 608         raise MatchingFailure
 609       else
 610         let metas = metas_of_term t1 in
 611         let fix_subst = function
 612           | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
 613               (j, (c, Cic.Meta (i, lc), ty))
 614           | s -> s
 615         in
 616         let subst = List.map fix_subst subst in
 617
 618 (*         Printf.printf "matching %s %s:\n%s\n" *)
 619 (*           (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *)
 620 (*         print_newline (); *)
 621
 622         subst, metasenv, ugraph
 623     with e ->
 624 (*       Printf.printf "failed to match %s %s\n" *)
 625 (*         (CicPp.ppterm t1) (CicPp.ppterm t2); *)
 626       raise MatchingFailure
 627 ;;
 628
 629 (* let matching = *)
 630 (*   let profile = CicUtil.profile "Inference.matching" in *)
 631 (*   (fun metasenv context t1 t2 ugraph -> *)
 632 (*      profile (matching metasenv context t1 t2) ugraph) *)
 633 (* ;; *)
 634
 635
 636 let beta_expand ?(metas_ok=true) ?(match_only=false)
 637     what type_of_what where context metasenv ugraph =
 638   let module S = CicSubstitution in
 639   let module C = Cic in
 640
 641   let print_info = false in
 642
 643 (*   let _ = *)
 644 (*     let names = names_of_context context in *)
 645 (*     Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *)
 646 (*       (CicPp.pp what names) (CicPp.ppterm what) *)
 647 (*       (CicPp.pp where names) (CicPp.ppterm where); *)
 648 (*     print_newline (); *)
 649 (*   in *)
 650   (*
 651     return value:
 652     ((list of all possible beta expansions, subst, metasenv, ugraph),
 653      lifted term)
 654   *)
 655   let rec aux lift_amount term context metasenv subst ugraph =
 656 (*     Printf.printf "enter aux %s\n" (CicPp.ppterm term); *)
 657     let res, lifted_term =
 658       match term with
 659       | C.Rel m  ->
 660           [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 661
 662       | C.Var (uri, exp_named_subst) ->
 663           let ens', lifted_ens =
 664             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
 665           in
 666           let expansions =
 667             List.map
 668               (fun (e, s, m, ug) ->
 669                  (C.Var (uri, e), s, m, ug)) ens'
 670           in
 671           expansions, C.Var (uri, lifted_ens)
 672
 673       | C.Meta (i, l) ->
 674           let l', lifted_l =
 675             List.fold_right
 676               (fun arg (res, lifted_tl) ->
 677                  match arg with
 678                  | Some arg ->
 679                      let arg_res, lifted_arg =
 680                        aux lift_amount arg context metasenv subst ugraph in
 681                      let l1 =
 682                        List.map
 683                          (fun (a, s, m, ug) -> (Some a)::lifted_tl, s, m, ug)
 684                          arg_res
 685                      in
 686                      (l1 @
 687                         (List.map
 688                            (fun (r, s, m, ug) -> (Some lifted_arg)::r, s, m, ug)
 689                            res),
 690                       (Some lifted_arg)::lifted_tl)
 691                  | None ->
 692                      (List.map
 693                         (fun (r, s, m, ug) -> None::r, s, m, ug)
 694                         res,
 695                       None::lifted_tl)
 696               ) l ([], [])
 697           in
 698           let e =
 699             List.map
 700               (fun (l, s, m, ug) ->
 701                  (C.Meta (i, l), s, m, ug)) l'
 702           in
 703           e, C.Meta (i, lifted_l)
 704
 705       | C.Sort _
 706       | C.Implicit _ as t -> [], t
 707
 708       | C.Cast (s, t) ->
 709           let l1, lifted_s =
 710             aux lift_amount s context metasenv subst ugraph in
 711           let l2, lifted_t =
 712             aux lift_amount t context metasenv subst ugraph
 713           in
 714           let l1' =
 715             List.map
 716               (fun (t, s, m, ug) ->
 717                  C.Cast (t, lifted_t), s, m, ug) l1 in
 718           let l2' =
 719             List.map
 720               (fun (t, s, m, ug) ->
 721                  C.Cast (lifted_s, t), s, m, ug) l2 in
 722           l1'@l2', C.Cast (lifted_s, lifted_t)
 723
 724       | C.Prod (nn, s, t) ->
 725           let l1, lifted_s =
 726             aux lift_amount s context metasenv subst ugraph in
 727           let l2, lifted_t =
 728             aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
 729               metasenv subst ugraph
 730           in
 731           let l1' =
 732             List.map
 733               (fun (t, s, m, ug) ->
 734                  C.Prod (nn, t, lifted_t), s, m, ug) l1 in
 735           let l2' =
 736             List.map
 737               (fun (t, s, m, ug) ->
 738                  C.Prod (nn, lifted_s, t), s, m, ug) l2 in
 739           l1'@l2', C.Prod (nn, lifted_s, lifted_t)
 740
 741       | C.Lambda (nn, s, t) ->
 742           let l1, lifted_s =
 743             aux lift_amount s context metasenv subst ugraph in
 744           let l2, lifted_t =
 745             aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
 746               metasenv subst ugraph
 747           in
 748           let l1' =
 749             List.map
 750               (fun (t, s, m, ug) ->
 751                  C.Lambda (nn, t, lifted_t), s, m, ug) l1 in
 752           let l2' =
 753             List.map
 754               (fun (t, s, m, ug) ->
 755                  C.Lambda (nn, lifted_s, t), s, m, ug) l2 in
 756           l1'@l2', C.Lambda (nn, lifted_s, lifted_t)
 757
 758       | C.LetIn (nn, s, t) ->
 759           let l1, lifted_s =
 760             aux lift_amount s context metasenv subst ugraph in
 761           let l2, lifted_t =
 762             aux (lift_amount+1) t ((Some (nn, C.Def (s, None)))::context)
 763               metasenv subst ugraph
 764           in
 765           let l1' =
 766             List.map
 767               (fun (t, s, m, ug) ->
 768                  C.LetIn (nn, t, lifted_t), s, m, ug) l1 in
 769           let l2' =
 770             List.map
 771               (fun (t, s, m, ug) ->
 772                  C.LetIn (nn, lifted_s, t), s, m, ug) l2 in
 773           l1'@l2', C.LetIn (nn, lifted_s, lifted_t)
 774
 775       | C.Appl l ->
 776           let l', lifted_l =
 777             aux_list lift_amount l context metasenv subst ugraph
 778           in
 779           (List.map (fun (l, s, m, ug) -> (C.Appl l, s, m, ug)) l',
 780            C.Appl lifted_l)
 781
 782       | C.Const (uri, exp_named_subst) ->
 783           let ens', lifted_ens =
 784             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
 785           in
 786           let expansions =
 787             List.map
 788               (fun (e, s, m, ug) ->
 789                  (C.Const (uri, e), s, m, ug)) ens'
 790           in
 791           (expansions, C.Const (uri, lifted_ens))
 792
 793       | C.MutInd (uri, i ,exp_named_subst) ->
 794           let ens', lifted_ens =
 795             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
 796           in
 797           let expansions =
 798             List.map
 799               (fun (e, s, m, ug) ->
 800                  (C.MutInd (uri, i, e), s, m, ug)) ens'
 801           in
 802           (expansions, C.MutInd (uri, i, lifted_ens))
 803
 804       | C.MutConstruct (uri, i, j, exp_named_subst) ->
 805           let ens', lifted_ens =
 806             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
 807           in
 808           let expansions =
 809             List.map
 810               (fun (e, s, m, ug) ->
 811                  (C.MutConstruct (uri, i, j, e), s, m, ug)) ens'
 812           in
 813           (expansions, C.MutConstruct (uri, i, j, lifted_ens))
 814
 815       | C.MutCase (sp, i, outt, t, pl) ->
 816           let pl_res, lifted_pl =
 817             aux_list lift_amount pl context metasenv subst ugraph
 818           in
 819           let l1, lifted_outt =
 820             aux lift_amount outt context metasenv subst ugraph in
 821           let l2, lifted_t =
 822             aux lift_amount t context metasenv subst ugraph in
 823
 824           let l1' =
 825             List.map
 826               (fun (outt, s, m, ug) ->
 827                  C.MutCase (sp, i, outt, lifted_t, lifted_pl), s, m, ug) l1 in
 828           let l2' =
 829             List.map
 830               (fun (t, s, m, ug) ->
 831                  C.MutCase (sp, i, lifted_outt, t, lifted_pl), s, m, ug) l2 in
 832           let l3' =
 833             List.map
 834               (fun (pl, s, m, ug) ->
 835                  C.MutCase (sp, i, lifted_outt, lifted_t, pl), s, m, ug) pl_res
 836           in
 837           (l1'@l2'@l3', C.MutCase (sp, i, lifted_outt, lifted_t, lifted_pl))
 838
 839       | C.Fix (i, fl) ->
 840           let len = List.length fl in
 841           let fl', lifted_fl =
 842             List.fold_right
 843               (fun (nm, idx, ty, bo) (res, lifted_tl) ->
 844                  let lifted_ty = S.lift lift_amount ty in
 845                  let bo_res, lifted_bo =
 846                    aux (lift_amount+len) bo context metasenv subst ugraph in
 847                  let l1 =
 848                    List.map
 849                      (fun (a, s, m, ug) ->
 850                         (nm, idx, lifted_ty, a)::lifted_tl, s, m, ug)
 851                      bo_res
 852                  in
 853                  (l1 @
 854                     (List.map
 855                        (fun (r, s, m, ug) ->
 856                           (nm, idx, lifted_ty, lifted_bo)::r, s, m, ug) res),
 857                   (nm, idx, lifted_ty, lifted_bo)::lifted_tl)
 858               ) fl ([], [])
 859           in
 860           (List.map
 861              (fun (fl, s, m, ug) -> C.Fix (i, fl), s, m, ug) fl',
 862            C.Fix (i, lifted_fl))
 863
 864       | C.CoFix (i, fl) ->
 865           let len = List.length fl in
 866           let fl', lifted_fl =
 867             List.fold_right
 868               (fun (nm, ty, bo) (res, lifted_tl) ->
 869                  let lifted_ty = S.lift lift_amount ty in
 870                  let bo_res, lifted_bo =
 871                    aux (lift_amount+len) bo context metasenv subst ugraph in
 872                  let l1 =
 873                    List.map
 874                      (fun (a, s, m, ug) ->
 875                         (nm, lifted_ty, a)::lifted_tl, s, m, ug)
 876                      bo_res
 877                  in
 878                  (l1 @
 879                     (List.map
 880                        (fun (r, s, m, ug) ->
 881                           (nm, lifted_ty, lifted_bo)::r, s, m, ug) res),
 882                   (nm, lifted_ty, lifted_bo)::lifted_tl)
 883               ) fl ([], [])
 884           in
 885           (List.map
 886              (fun (fl, s, m, ug) -> C.CoFix (i, fl), s, m, ug) fl',
 887            C.CoFix (i, lifted_fl))
 888     in
 889     let retval =
 890       match term with
 891       | C.Meta _ when (not metas_ok) ->
 892           res, lifted_term
 893       | _ ->
 894 (*           let term' = *)
 895 (*             if match_only then replace_metas context term *)
 896 (*             else term *)
 897 (*           in *)
 898           try
 899             let subst', metasenv', ugraph' =
 900 (*               Printf.printf "provo a unificare %s e %s\n" *)
 901 (*                 (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *)
 902               if match_only then
 903                 matching metasenv context term (S.lift lift_amount what) ugraph
 904               else
 905                 CicUnification.fo_unif metasenv context
 906                   (S.lift lift_amount what) term ugraph
 907             in
 908 (*           Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
 909 (*             (CicPp.ppterm (S.lift lift_amount what)); *)
 910 (*           Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
 911 (*           Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
 912             (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
 913 (*             if match_only then *)
 914 (*               let t' = CicMetaSubst.apply_subst subst' term in *)
 915 (*               if not (meta_convertibility term t') then ( *)
 916 (*                 res, lifted_term *)
 917 (*               ) else ( *)
 918 (*                 let metas = metas_of_term term in *)
 919 (*                 let fix_subst = function *)
 920 (*                   | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas -> *)
 921 (*                       (j, (c, C.Meta (i, lc), ty)) *)
 922 (*                   | s -> s *)
 923 (*                 in *)
 924 (*                 let subst' = List.map fix_subst subst' in *)
 925 (*                 ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, *)
 926 (*                  lifted_term) *)
 927 (*               ) *)
 928 (*             else *)
 929               ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
 930                lifted_term)
 931           with e ->
 932             if print_info then (
 933               print_endline ("beta_expand ERROR!: " ^ (Printexc.to_string e));
 934             );
 935             res, lifted_term
 936     in
 937 (*     Printf.printf "exit aux\n"; *)
 938     retval
 939
 940   and aux_list lift_amount l context metasenv subst ugraph =
 941     List.fold_right
 942       (fun arg (res, lifted_tl) ->
 943          let arg_res, lifted_arg =
 944            aux lift_amount arg context metasenv subst ugraph in
 945          let l1 = List.map
 946            (fun (a, s, m, ug) -> a::lifted_tl, s, m, ug) arg_res
 947          in
 948          (l1 @ (List.map
 949                   (fun (r, s, m, ug) -> lifted_arg::r, s, m, ug) res),
 950           lifted_arg::lifted_tl)
 951       ) l ([], [])
 952
 953   and aux_ens lift_amount exp_named_subst context metasenv subst ugraph =
 954     List.fold_right
 955       (fun (u, arg) (res, lifted_tl) ->
 956          let arg_res, lifted_arg =
 957            aux lift_amount arg context metasenv subst ugraph in
 958          let l1 =
 959            List.map
 960              (fun (a, s, m, ug) -> (u, a)::lifted_tl, s, m, ug) arg_res
 961          in
 962          (l1 @ (List.map (fun (r, s, m, ug) ->
 963                             (u, lifted_arg)::r, s, m, ug) res),
 964           (u, lifted_arg)::lifted_tl)
 965       ) exp_named_subst ([], [])
 966
 967   in
 968   let expansions, _ =
 969 (*     let where = *)
 970 (*       if match_only then replace_metas (\* context *\) where *)
 971 (*       else where *)
 972 (*     in *)
 973     if print_info then (
 974       Printf.printf "searching %s inside %s\n"
 975         (CicPp.ppterm what) (CicPp.ppterm where);
 976     );
 977     aux 0 where context metasenv [] ugraph
 978   in
 979   let mapfun =
 980 (*     if match_only then *)
 981 (*       (fun (term, subst, metasenv, ugraph) -> *)
 982 (*          let term' = *)
 983 (*            C.Lambda (C.Anonymous, type_of_what, restore_metas term) *)
 984 (*          and subst = restore_subst subst in *)
 985 (*          (term', subst, metasenv, ugraph)) *)
 986 (*     else *)
 987       (fun (term, subst, metasenv, ugraph) ->
 988          let term' = C.Lambda (C.Anonymous, type_of_what, term) in
 989          (term', subst, metasenv, ugraph))
 990   in
 991   List.map mapfun expansions
 992 ;;
 993
 994
 995 let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
 996   let module C = Cic in
 997   let module S = CicSubstitution in
 998   let module T = CicTypeChecker in
 999   let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
1000   let rec aux index newmeta = function
1001     | [] -> [], newmeta
1002     | (Some (_, C.Decl (term)))::tl ->
1003         let do_find context term =
1004           match term with
1005           | C.Prod (name, s, t) ->
1006 (*               let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
1007               let (head, newmetas, args, _) =
1008                 PrimitiveTactics.new_metasenv_for_apply newmeta proof
1009                   context (S.lift index term)
1010               in
1011               let newmeta =
1012                 List.fold_left
1013                   (fun maxm arg ->
1014                      match arg with
1015                      | C.Meta (i, _) -> (max maxm i)
1016                      | _ -> assert false)
1017                   newmeta args
1018               in
1019               let p =
1020                 if List.length args = 0 then
1021                   C.Rel index
1022                 else
1023                   C.Appl ((C.Rel index)::args)
1024               in (
1025                 match head with
1026                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
1027                     Printf.printf "OK: %s\n" (CicPp.ppterm term);
1028                     let o = !Utils.compare_terms t1 t2 in
1029                     let e = (p, (ty, t1, t2, o), newmetas, args) in
1030                     store_proof e (BasicProof p);
1031                     Some e, (newmeta+1)
1032                 | _ -> None, newmeta
1033               )
1034           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
1035               let t1 = S.lift index t1
1036               and t2 = S.lift index t2 in
1037               let o = !Utils.compare_terms t1 t2 in
1038               let e = (C.Rel index, (ty, t1, t2, o), [], []) in
1039               store_proof e (BasicProof (C.Rel index));
1040               Some e, (newmeta+1)
1041           | _ -> None, newmeta
1042         in (
1043           match do_find context term with
1044           | Some p, newmeta ->
1045               let tl, newmeta' = (aux (index+1) newmeta tl) in
1046               p::tl, max newmeta newmeta'
1047           | None, _ ->
1048               aux (index+1) newmeta tl
1049         )
1050     | _::tl ->
1051         aux (index+1) newmeta tl
1052   in
1053   aux 1 newmeta context
1054 ;;
1055
1056
1057 let fix_metas newmeta ((proof, (ty, left, right, o), menv, args) as equality) =
1058   let table = Hashtbl.create (List.length args) in
1059   let newargs, _ =
1060     List.fold_right
1061       (fun t (newargs, index) ->
1062          match t with
1063          | Cic.Meta (i, l) ->
1064              Hashtbl.add table i index;
1065              ((Cic.Meta (index, l))::newargs, index+1)
1066          | _ -> assert false)
1067       args ([], newmeta)
1068   in
1069   let repl where =
1070     ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
1071       ~where
1072   in
1073   let menv' =
1074     List.fold_right
1075       (fun (i, context, term) menv ->
1076          try
1077            let index = Hashtbl.find table i in
1078            (index, context, term)::menv
1079          with Not_found ->
1080            (i, context, term)::menv)
1081       menv []
1082   in
1083   let ty = repl ty
1084   and left = repl left
1085   and right = repl right in
1086   let metas = (metas_of_term left) @ (metas_of_term right) in
1087   let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv'
1088   and newargs =
1089     List.filter
1090       (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
1091   in
1092   (newmeta + (List.length newargs) + 1,
1093    (repl proof, (ty, left, right, o), menv', newargs))
1094 ;;
1095
1096
1097 exception TermIsNotAnEquality;;
1098
1099 let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
1100   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
1101       let o = !Utils.compare_terms t1 t2 in
1102       let e = (proof, (ty, t1, t2, o), [], []) in
1103       store_proof e (BasicProof proof);
1104       e
1105 (*       (proof, (ty, t1, t2, o), [], []) *)
1106   | _ ->
1107       raise TermIsNotAnEquality
1108 ;;
1109
1110
1111 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
1112
1113
1114 let superposition_left (metasenv, context, ugraph) target source =
1115   let module C = Cic in
1116   let module S = CicSubstitution in
1117   let module M = CicMetaSubst in
1118   let module HL = HelmLibraryObjects in
1119   let module CR = CicReduction in
1120   (* we assume that target is ground (does not contain metavariables): this
1121    * should always be the case (I hope, at least) *)
1122   let proof, (eq_ty, left, right, t_order), _, _ = target in
1123   let eqproof, (ty, t1, t2, s_order), newmetas, args = source in
1124
1125   let compare_terms = !Utils.compare_terms in
1126
1127   if eq_ty <> ty then
1128     []
1129   else
1130     let where, is_left =
1131       match t_order (* compare_terms left right *) with
1132       | Lt -> right, false
1133       | Gt -> left, true
1134       | _ -> (
1135           Printf.printf "????????? %s = %s" (CicPp.ppterm left)
1136             (CicPp.ppterm right);
1137           print_newline ();
1138           assert false (* again, for ground terms this shouldn't happen... *)
1139         )
1140     in
1141     let metasenv' = newmetas @ metasenv in
1142     let result = s_order (* compare_terms t1 t2 *) in
1143     let res1, res2 =
1144       match result with
1145       | Gt -> (beta_expand t1 ty where context metasenv' ugraph), []
1146       | Lt -> [], (beta_expand t2 ty where context metasenv' ugraph)
1147       | _ ->
1148           let res1 =
1149             List.filter
1150               (fun (t, s, m, ug) ->
1151                  compare_terms (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
1152               (beta_expand t1 ty where context metasenv' ugraph)
1153           and res2 =
1154             List.filter
1155               (fun (t, s, m, ug) ->
1156                  compare_terms (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
1157               (beta_expand t2 ty where context metasenv' ugraph)
1158           in
1159           res1, res2
1160     in
1161     (*   let what, other = *)
1162     (*     if is_left then left, right *)
1163     (*     else right, left *)
1164     (*   in *)
1165     let build_new what other eq_URI (t, s, m, ug) =
1166       let newgoal, newgoalproof =
1167         match t with
1168         | C.Lambda (nn, ty, bo) ->
1169             let bo' = S.subst (M.apply_subst s other) bo in
1170             let bo'' =
1171               C.Appl (
1172                 [C.MutInd (HL.Logic.eq_URI, 0, []);
1173                  S.lift 1 eq_ty] @
1174                   if is_left then [bo'; S.lift 1 right]
1175                   else [S.lift 1 left; bo'])
1176             in
1177             let t' = C.Lambda (nn, ty, bo'') in
1178             S.subst (M.apply_subst s other) bo,
1179             M.apply_subst s
1180               (C.Appl [C.Const (eq_URI, []); ty; what; t';
1181                        proof; other; eqproof])
1182         | _ -> assert false
1183       in
1184       let equation =
1185         if is_left then (eq_ty, newgoal, right, compare_terms newgoal right)
1186         else (eq_ty, left, newgoal, compare_terms left newgoal)
1187       in
1188       (newgoalproof (* eqproof *), equation, [], [])
1189     in
1190     let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1
1191     and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in
1192     new1 @ new2
1193 ;;
1194
1195
1196 let superposition_right newmeta (metasenv, context, ugraph) target source =
1197   let module C = Cic in
1198   let module S = CicSubstitution in
1199   let module M = CicMetaSubst in
1200   let module HL = HelmLibraryObjects in
1201   let module CR = CicReduction in
1202   let eqproof, (eq_ty, left, right, t_order), newmetas, args = target in
1203   let eqp', (ty', t1, t2, s_order), newm', args' = source in
1204   let maxmeta = ref newmeta in
1205
1206   let compare_terms = !Utils.compare_terms in
1207
1208   if eq_ty <> ty' then
1209     newmeta, []
1210   else
1211     (*   let ok term subst other other_eq_side ugraph = *)
1212     (*     match term with *)
1213     (*     | C.Lambda (nn, ty, bo) -> *)
1214     (*         let bo' = S.subst (M.apply_subst subst other) bo in *)
1215     (*         let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *)
1216     (*         not res *)
1217     (*     |  _ -> assert false *)
1218     (*   in *)
1219     let condition left right what other (t, s, m, ug) =
1220       let subst = M.apply_subst s in
1221       let cmp1 = compare_terms (subst what) (subst other) in
1222       let cmp2 = compare_terms (subst left) (subst right) in
1223       (*     cmp1 = Gt && cmp2 = Gt *)
1224       cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
1225         (*     && (ok t s other right ug) *)
1226     in
1227     let metasenv' = metasenv @ newmetas @ newm' in
1228     let beta_expand = beta_expand ~metas_ok:false in
1229     let cmp1 = t_order (* compare_terms left right *)
1230     and cmp2 = s_order (* compare_terms t1 t2 *) in
1231     let res1, res2, res3, res4 =
1232       let res l r s t =
1233         List.filter
1234           (condition l r s t)
1235           (beta_expand s eq_ty l context metasenv' ugraph)
1236       in
1237       match cmp1, cmp2 with
1238       | Gt, Gt ->
1239           (beta_expand t1 eq_ty left context metasenv' ugraph), [], [], []
1240       | Gt, Lt ->
1241           [], (beta_expand t2 eq_ty left context metasenv' ugraph), [], []
1242       | Lt, Gt ->
1243           [], [], (beta_expand t1 eq_ty right context metasenv' ugraph), []
1244       | Lt, Lt ->
1245           [], [], [], (beta_expand t2 eq_ty right context metasenv' ugraph)
1246       | Gt, _ ->
1247           let res1 = res left right t1 t2
1248           and res2 = res left right t2 t1 in
1249           res1, res2, [], []
1250       | Lt, _ ->
1251           let res3 = res right left t1 t2
1252           and res4 = res right left t2 t1 in
1253           [], [], res3, res4
1254       | _, Gt ->
1255           let res1 = res left right t1 t2
1256           and res3 = res right left t1 t2 in
1257           res1, [], res3, []
1258       | _, Lt ->
1259           let res2 = res left right t2 t1
1260           and res4 = res right left t2 t1 in
1261           [], res2, [], res4
1262       | _, _ ->
1263           let res1 = res left right t1 t2
1264           and res2 = res left right t2 t1
1265           and res3 = res right left t1 t2
1266           and res4 = res right left t2 t1 in
1267           res1, res2, res3, res4
1268     in
1269     let newmetas = newmetas @ newm' in
1270     let newargs = args @ args' in
1271     let build_new what other is_left eq_URI (t, s, m, ug) =
1272       (*     let what, other = *)
1273       (*       if is_left then left, right *)
1274       (*       else right, left *)
1275       (*     in *)
1276       let newterm, neweqproof =
1277         match t with
1278         | C.Lambda (nn, ty, bo) ->
1279             let bo' = M.apply_subst s (S.subst other bo) in
1280             let bo'' =
1281               C.Appl (
1282                 [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
1283                   if is_left then [bo'; S.lift 1 right]
1284                   else [S.lift 1 left; bo'])
1285             in
1286             let t' = C.Lambda (nn, ty, bo'') in
1287             bo',
1288             M.apply_subst s
1289               (C.Appl [C.Const (eq_URI, []); ty; what; t';
1290                        eqproof; other; eqp'])
1291         | _ -> assert false
1292       in
1293       let newmeta, newequality =
1294         let left, right =
1295           if is_left then (newterm, M.apply_subst s right)
1296           else (M.apply_subst s left, newterm) in
1297         let neworder = compare_terms left right in
1298         fix_metas !maxmeta
1299           (neweqproof, (eq_ty, left, right, neworder), newmetas, newargs)
1300       in
1301       maxmeta := newmeta;
1302       newequality
1303     in
1304     let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
1305     and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
1306     and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
1307     and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
1308     let ok = function
1309       | _, (_, left, right, _), _, _ ->
1310           not (fst (CR.are_convertible context left right ugraph))
1311     in
1312     (!maxmeta,
1313      (List.filter ok (new1 @ new2 @ new3 @ new4)))
1314 ;;
1315
1316
1317 let is_identity ((_, context, ugraph) as env) = function
1318   | ((_, (ty, left, right, _), _, _) as equality) ->
1319       let res =
1320         (left = right ||
1321             (fst (CicReduction.are_convertible context left right ugraph)))
1322       in
1323 (*       if res then ( *)
1324 (*         Printf.printf "is_identity: %s" (string_of_equality ~env equality); *)
1325 (*         print_newline (); *)
1326 (*       ); *)
1327       res
1328 ;;
1329
1330
1331 let demodulation newmeta (metasenv, context, ugraph) target source =
1332   let module C = Cic in
1333   let module S = CicSubstitution in
1334   let module M = CicMetaSubst in
1335   let module HL = HelmLibraryObjects in
1336   let module CR = CicReduction in
1337
1338   let proof, (eq_ty, left, right, t_order), metas, args = target
1339   and proof', (ty, t1, t2, s_order), metas', args' = source in
1340
1341   let compare_terms = !Utils.compare_terms in
1342
1343   if eq_ty <> ty then
1344     newmeta, target
1345   else
1346     let first_step, get_params =
1347       match s_order (* compare_terms t1 t2 *) with
1348       | Gt -> 1, (function
1349                     | 1 -> true, t1, t2, HL.Logic.eq_ind_URI
1350                     | 0 -> false, t1, t2, HL.Logic.eq_ind_URI
1351                     | _ -> assert false)
1352       | Lt -> 1, (function
1353                     | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
1354                     | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
1355                     | _ -> assert false)
1356       | _ ->
1357           let first_step = 3 in
1358           let get_params step =
1359             match step with
1360             | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
1361             | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
1362             | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
1363             | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
1364             | _ -> assert false
1365           in
1366           first_step, get_params
1367     in
1368     let rec demodulate newmeta step metasenv target =
1369       let proof, (eq_ty, left, right, t_order), metas, args = target in
1370       let is_left, what, other, eq_URI = get_params step in
1371
1372       let env = metasenv, context, ugraph in
1373       let names = names_of_context context in
1374 (*       Printf.printf *)
1375 (*         "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
1376 (*         (string_of_equality ~env target) (CicPp.pp what names) *)
1377 (*         (CicPp.pp other names) (string_of_bool is_left); *)
1378 (*       Printf.printf "step: %d" step; *)
1379 (*       print_newline (); *)
1380
1381       let ok (t, s, m, ug) =
1382         compare_terms (M.apply_subst s what) (M.apply_subst s other) = Gt
1383       in
1384       let res =
1385         let r = (beta_expand ~metas_ok:false ~match_only:true
1386                    what ty (if is_left then left else right)
1387                    context (metasenv @ metas) ugraph)
1388         in
1389 (*         let m' = metas_of_term what *)
1390 (*         and m'' = metas_of_term (if is_left then left else right) in *)
1391 (*         if (List.mem 527 m'') && (List.mem 6 m') then ( *)
1392 (*           Printf.printf *)
1393 (*             "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
1394 (*             (string_of_equality ~env target) (CicPp.pp what names) *)
1395 (*             (CicPp.pp other names) (string_of_bool is_left); *)
1396 (*           Printf.printf "step: %d" step; *)
1397 (*           print_newline (); *)
1398 (*           print_endline "res:"; *)
1399 (*           List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *)
1400 (*           print_newline (); *)
1401 (*           Printf.printf "metasenv:\n%s\n" (print_metasenv (metasenv @ metas)); *)
1402 (*           print_newline (); *)
1403 (*         ); *)
1404         List.filter ok r
1405       in
1406       match res with
1407       | [] ->
1408           if step = 0 then newmeta, target
1409           else demodulate newmeta (step-1) metasenv target
1410       | (t, s, m, ug)::_ ->
1411           let newterm, newproof =
1412             match t with
1413             | C.Lambda (nn, ty, bo) ->
1414 (*                 let bo' = M.apply_subst s (S.subst other bo) in *)
1415                 let bo' = S.subst (M.apply_subst s other) bo in
1416                 let bo'' =
1417                   C.Appl (
1418                     [C.MutInd (HL.Logic.eq_URI, 0, []);
1419                      S.lift 1 eq_ty] @
1420                       if is_left then [bo'; S.lift 1 right]
1421                       else [S.lift 1 left; bo'])
1422                 in
1423                 let t' = C.Lambda (nn, ty, bo'') in
1424 (*                 M.apply_subst s (S.subst other bo), *)
1425                 bo',
1426                 M.apply_subst s
1427                   (C.Appl [C.Const (eq_URI, []); ty; what; t';
1428                            proof; other; proof'])
1429             | _ -> assert false
1430           in
1431           let newmeta, newtarget =
1432             let left, right =
1433 (*               if is_left then (newterm, M.apply_subst s right) *)
1434 (*               else (M.apply_subst s left, newterm) in *)
1435               if is_left then newterm, right
1436               else left, newterm
1437             in
1438             let neworder = compare_terms left right in
1439 (*             let newmetasenv = metasenv @ metas in *)
1440 (*             let newargs = args @ args' in *)
1441 (*             fix_metas newmeta *)
1442 (*               (newproof, (eq_ty, left, right), newmetasenv, newargs) *)
1443             let m = (metas_of_term left) @ (metas_of_term right) in
1444             let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
1445             and newargs =
1446               List.filter
1447                 (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
1448                 args
1449             in
1450             newmeta,
1451             (newproof, (eq_ty, left, right, neworder), newmetasenv, newargs)
1452           in
1453 (*           Printf.printf *)
1454 (*             "demodulate, newtarget: %s\ntarget was: %s\n" *)
1455 (*             (string_of_equality ~env newtarget) *)
1456 (*             (string_of_equality ~env target); *)
1457 (* (\*           let _, _, newm, newa = newtarget in *\) *)
1458 (* (\*           Printf.printf "newmetasenv:\n%s\nnewargs:\n%s\n" *\) *)
1459 (* (\*             (print_metasenv newm) *\) *)
1460 (* (\*             (String.concat "\n" (List.map CicPp.ppterm newa)); *\) *)
1461 (*           print_newline (); *)
1462           if is_identity env newtarget then
1463             newmeta, newtarget
1464           else
1465             demodulate newmeta first_step metasenv newtarget
1466     in
1467     demodulate newmeta first_step (metasenv @ metas') target
1468 ;;
1469
1470
1471 (*
1472 let demodulation newmeta env target source =
1473   newmeta, target
1474 ;;
1475 *)
1476
1477
1478 let subsumption env target source =
1479   let _, (ty, tl, tr, _), tmetas, _ = target
1480   and _, (ty', sl, sr, _), smetas, _ = source in
1481   if ty <> ty' then
1482     false
1483   else
1484     let metasenv, context, ugraph = env in
1485     let metasenv = metasenv @ tmetas @ smetas in
1486     let names = names_of_context context in
1487     let samesubst subst subst' =
1488 (*       Printf.printf "samesubst:\nsubst: %s\nsubst': %s\n" *)
1489 (*         (print_subst subst) (print_subst subst'); *)
1490 (*       print_newline (); *)
1491       let tbl = Hashtbl.create (List.length subst) in
1492       List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
1493       List.for_all
1494         (fun (m, (c, t1, t2)) ->
1495            try
1496              let c', t1', t2' = Hashtbl.find tbl m in
1497              if (c = c') && (t1 = t1') && (t2 = t2') then true
1498              else false
1499            with Not_found ->
1500              true)
1501         subst'
1502     in
1503     let subsaux left right left' right' =
1504       try
1505         let subst, menv, ug = matching metasenv context left left' ugraph
1506         and subst', menv', ug' = matching metasenv context right right' ugraph
1507         in
1508 (*         Printf.printf "left = right: %s = %s\n" *)
1509 (*           (CicPp.pp left names) (CicPp.pp right names); *)
1510 (*         Printf.printf "left' = right': %s = %s\n" *)
1511 (*           (CicPp.pp left' names) (CicPp.pp right' names);         *)
1512         samesubst subst subst'
1513       with e ->
1514 (*         print_endline (Printexc.to_string e); *)
1515         false
1516     in
1517     let res =
1518       if subsaux tl tr sl sr then true
1519       else subsaux tl tr sr sl
1520     in
1521     if res then (
1522       Printf.printf "subsumption!:\ntarget: %s\nsource: %s\n"
1523         (string_of_equality ~env target) (string_of_equality ~env source);
1524       print_newline ();
1525     );
1526     res
1527 ;;
1528
1529
1530 let extract_differing_subterms t1 t2 =
1531   let module C = Cic in
1532   let rec aux t1 t2 =
1533     match t1, t2 with
1534     | C.Appl l1, C.Appl l2 when (List.length l1) <> (List.length l2) ->
1535         [(t1, t2)]
1536     | C.Appl (h1::tl1), C.Appl (h2::tl2) ->
1537         let res = List.concat (List.map2 aux tl1 tl2) in
1538         if h1 <> h2 then
1539           if res = [] then [(h1, h2)] else [(t1, t2)]
1540         else
1541           if List.length res > 1 then [(t1, t2)] else res
1542     | t1, t2 ->
1543         if t1 <> t2 then [(t1, t2)] else []
1544   in
1545   let res = aux t1 t2 in
1546   match res with
1547   | hd::[] -> Some hd
1548   | _ -> None
1549 ;;