helm/ocaml/paramodulation/inference.ml

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