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