helm/ocaml/paramodulation/inference.ml

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