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