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 let rec check_irl start = function
 298   | [] -> true
 299   | None::tl -> check_irl (start+1) tl
 300   | (Some (Cic.Rel x))::tl ->
 301       if x = start then check_irl (start+1) tl else false
 302   | _ -> false
 303 ;;
 304
 305 let rec is_simple_term = function
 306   | Cic.Appl ((Cic.Meta _)::_) -> false
 307   | Cic.Appl l -> List.for_all is_simple_term l
 308   | Cic.Meta (i, l) -> check_irl 1 l
 309   | Cic.Rel _ -> true
 310   | _ -> false
 311 ;;
 312
 313
 314 let lookup_subst meta subst =
 315   match meta with
 316   | Cic.Meta (i, _) -> (
 317       try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
 318       with Not_found -> meta
 319     )
 320   | _ -> assert false
 321 ;;
 322
 323
 324 let unification_simple metasenv context t1 t2 ugraph =
 325   let module C = Cic in
 326   let module M = CicMetaSubst in
 327   let module U = CicUnification in
 328   let lookup = lookup_subst in
 329   let rec occurs_check subst what where =
 330     (*       Printf.printf "occurs_check %s %s" *)
 331     (*         (CicPp.ppterm what) (CicPp.ppterm where); *)
 332     (*       print_newline (); *)
 333     match where with
 334     | t when what = t -> true
 335     | C.Appl l -> List.exists (occurs_check subst what) l
 336     | C.Meta _ ->
 337         let t = lookup where subst in
 338         if t <> where then occurs_check subst what t else false
 339     | _ -> false
 340   in
 341   let rec unif subst menv s t =
 342 (*     Printf.printf "unif %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
 343 (*       (print_subst subst); *)
 344 (*     print_newline (); *)
 345     let s = match s with C.Meta _ -> lookup s subst | _ -> s
 346     and t = match t with C.Meta _ -> lookup t subst | _ -> t
 347     in
 348     (*       Printf.printf "after apply_subst: %s %s\n%s" *)
 349     (*         (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
 350     (*       print_newline (); *)
 351     match s, t with
 352     | s, t when s = t -> subst, menv
 353     | C.Meta (i, _), C.Meta (j, _) when i > j ->
 354         unif subst menv t s
 355     | C.Meta _, t when occurs_check subst s t ->
 356         raise (U.UnificationFailure "Inference.unification.unif")
 357 (*     | C.Meta (i, l), C.Meta (j, l') -> *)
 358 (*         let _, _, ty = CicUtil.lookup_meta i menv in *)
 359 (*         let _, _, ty' = CicUtil.lookup_meta j menv in *)
 360 (*         let binding1 = lookup s subst in *)
 361 (*         let binding2 = lookup t subst in *)
 362 (*         let subst, menv =  *)
 363 (*           if binding1 != s then *)
 364 (*             if binding2 != t then *)
 365 (*               unif subst menv binding1 binding2 *)
 366 (*             else *)
 367 (*               if binding1 = t then *)
 368 (*                 subst, menv *)
 369 (*               else *)
 370 (*                 ((j, (context, binding1, ty'))::subst, *)
 371 (*                  List.filter (fun (m, _, _) -> j <> m) menv) *)
 372 (*           else *)
 373 (*             if binding2 != t then *)
 374 (*               if s = binding2 then *)
 375 (*                 subst, menv *)
 376 (*               else *)
 377 (*                 ((i, (context, binding2, ty))::subst, *)
 378 (*                  List.filter (fun (m, _, _) -> i <> m) menv) *)
 379 (*             else *)
 380 (*               ((i, (context, t, ty))::subst, *)
 381 (*                List.filter (fun (m, _, _) -> i <> m) menv) *)
 382 (*         in *)
 383 (*         subst, menv *)
 384
 385     | C.Meta (i, l), t ->
 386         let _, _, ty = CicUtil.lookup_meta i menv in
 387         let subst =
 388           if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst
 389           else subst
 390         in
 391         let menv = List.filter (fun (m, _, _) -> i <> m) menv in
 392         subst, menv
 393     | _, C.Meta _ -> unif subst menv t s
 394     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
 395         raise (U.UnificationFailure "Inference.unification.unif")
 396     | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
 397         try
 398           List.fold_left2
 399             (fun (subst', menv) s t -> unif subst' menv s t)
 400             (subst, menv) tls tlt
 401         with e ->
 402           raise (U.UnificationFailure "Inference.unification.unif")
 403       )
 404     | _, _ -> raise (U.UnificationFailure "Inference.unification.unif")
 405   in
 406   let subst, menv = unif [] metasenv t1 t2 in
 407   (*     Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
 408   (*     print_newline (); *)
 409 (*   let rec fix_term = function *)
 410 (*     | (C.Meta (i, l) as t) -> *)
 411 (*         lookup t subst *)
 412 (*     | C.Appl l -> C.Appl (List.map fix_term l) *)
 413 (*     | t -> t *)
 414 (*   in *)
 415 (*   let rec fix_subst = function *)
 416 (*     | [] -> [] *)
 417 (*     | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl) *)
 418 (*   in *)
 419 (*   List.rev (fix_subst subst), menv, ugraph *)
 420   List.rev subst, menv, ugraph
 421 ;;
 422
 423
 424 let unification metasenv context t1 t2 ugraph =
 425 (*   Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
 426   let subst, menv, ug =
 427     if not (is_simple_term t1) || not (is_simple_term t2) then
 428       CicUnification.fo_unif metasenv context t1 t2 ugraph
 429     else
 430       unification_simple metasenv context t1 t2 ugraph
 431   in
 432   let rec fix_term = function
 433     | (Cic.Meta (i, l) as t) ->
 434         let t' = lookup_subst t subst in
 435         if t <> t' then fix_term t' else t
 436     | Cic.Appl l -> Cic.Appl (List.map fix_term l)
 437     | t -> t
 438   in
 439   let rec fix_subst = function
 440     | [] -> []
 441     | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl)
 442   in
 443 (*   Printf.printf "| subst: %s\n" (print_subst ~prefix:" ; " subst); *)
 444 (*   print_endline "|"; *)
 445   (* fix_subst *) subst, menv, ug
 446 ;;
 447
 448 (* let unification = CicUnification.fo_unif;; *)
 449
 450 exception MatchingFailure;;
 451
 452
 453 let matching_simple metasenv context t1 t2 ugraph =
 454   let module C = Cic in
 455   let module M = CicMetaSubst in
 456   let module U = CicUnification in
 457   let lookup meta subst =
 458     match meta with
 459     | C.Meta (i, _) -> (
 460         try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in t
 461         with Not_found -> meta
 462       )
 463     | _ -> assert false
 464   in
 465   let rec do_match subst menv s t =
 466 (*     Printf.printf "do_match %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
 467 (*       (print_subst subst); *)
 468 (*     print_newline (); *)
 469 (*     let s = match s with C.Meta _ -> lookup s subst | _ -> s *)
 470 (*     let t = match t with C.Meta _ -> lookup t subst | _ -> t in  *)
 471     (*       Printf.printf "after apply_subst: %s %s\n%s" *)
 472     (*         (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
 473     (*       print_newline (); *)
 474     match s, t with
 475     | s, t when s = t -> subst, menv
 476 (*     | C.Meta (i, _), C.Meta (j, _) when i > j -> *)
 477 (*         do_match subst menv t s *)
 478 (*     | C.Meta _, t when occurs_check subst s t -> *)
 479 (*         raise MatchingFailure *)
 480 (*     | s, C.Meta _ when occurs_check subst t s -> *)
 481 (*         raise MatchingFailure *)
 482     | s, C.Meta (i, l) ->
 483         let filter_menv i menv =
 484           List.filter (fun (m, _, _) -> i <> m) menv
 485         in
 486         let subst, menv =
 487           let value = lookup t subst in
 488           match value with
 489 (*           | C.Meta (i', l') when Hashtbl.mem table i' -> *)
 490 (*               (i', (context, s, ty))::subst, menv (\* filter_menv i' menv *\) *)
 491           | value when value = t ->
 492               let _, _, ty = CicUtil.lookup_meta i menv in
 493               (i, (context, s, ty))::subst, filter_menv i menv
 494           | value when value <> s ->
 495               raise MatchingFailure
 496           | value -> do_match subst menv s value
 497         in
 498         subst, menv
 499 (*           else if value <> s then *)
 500 (*             raise MatchingFailure *)
 501 (*           else subst *)
 502 (*           if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst *)
 503 (*           else subst *)
 504 (*         in *)
 505 (*         let menv = List.filter (fun (m, _, _) -> i <> m) menv in *)
 506 (*         subst, menv *)
 507 (*     | _, C.Meta _ -> do_match subst menv t s *)
 508 (*     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt -> *)
 509 (*         raise MatchingFailure *)
 510     | C.Appl ls, C.Appl lt -> (
 511         try
 512           List.fold_left2
 513             (fun (subst, menv) s t -> do_match subst menv s t)
 514             (subst, menv) ls lt
 515         with e ->
 516 (*           print_endline (Printexc.to_string e); *)
 517 (*           Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
 518 (*           print_newline ();           *)
 519           raise MatchingFailure
 520       )
 521     | _, _ ->
 522 (*         Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
 523 (*         print_newline (); *)
 524         raise MatchingFailure
 525   in
 526   let subst, menv = do_match [] metasenv t1 t2 in
 527   (*     Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
 528   (*     print_newline (); *)
 529   subst, menv, ugraph
 530 ;;
 531
 532
 533 let matching metasenv context t1 t2 ugraph =
 534 (*   if (is_simple_term t1) && (is_simple_term t2) then *)
 535 (*     let subst, menv, ug = *)
 536 (*       matching_simple metasenv context t1 t2 ugraph in *)
 537 (* (\*     Printf.printf "matching %s %s:\n%s\n" *\) *)
 538 (* (\*       (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *\) *)
 539 (* (\*     print_newline (); *\) *)
 540 (*     subst, menv, ug *)
 541 (*   else *)
 542     try
 543       let subst, metasenv, ugraph =
 544         (*       CicUnification.fo_unif metasenv context t1 t2 ugraph *)
 545         unification metasenv context t1 t2 ugraph
 546       in
 547       let t' = CicMetaSubst.apply_subst subst t1 in
 548       if not (meta_convertibility t1 t') then
 549         raise MatchingFailure
 550       else
 551         let metas = metas_of_term t1 in
 552         let fix_subst = function
 553           | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
 554               (j, (c, Cic.Meta (i, lc), ty))
 555           | s -> s
 556         in
 557         let subst = List.map fix_subst subst in
 558
 559 (*         Printf.printf "matching %s %s:\n%s\n" *)
 560 (*           (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *)
 561 (*         print_newline (); *)
 562
 563         subst, metasenv, ugraph
 564     with e ->
 565 (*       Printf.printf "failed to match %s %s\n" *)
 566 (*         (CicPp.ppterm t1) (CicPp.ppterm t2); *)
 567       raise MatchingFailure
 568 ;;
 569
 570 (* let matching = *)
 571 (*   let profile = CicUtil.profile "Inference.matching" in *)
 572 (*   (fun metasenv context t1 t2 ugraph -> *)
 573 (*      profile (matching metasenv context t1 t2) ugraph) *)
 574 (* ;; *)
 575
 576
 577 let beta_expand ?(metas_ok=true) ?(match_only=false)
 578     what type_of_what where context metasenv ugraph =
 579   let module S = CicSubstitution in
 580   let module C = Cic in
 581
 582   let print_info = false in
 583
 584 (*   let _ = *)
 585 (*     let names = names_of_context context in *)
 586 (*     Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *)
 587 (*       (CicPp.pp what names) (CicPp.ppterm what) *)
 588 (*       (CicPp.pp where names) (CicPp.ppterm where); *)
 589 (*     print_newline (); *)
 590 (*   in *)
 591   (*
 592     return value:
 593     ((list of all possible beta expansions, subst, metasenv, ugraph),
 594      lifted term)
 595   *)
 596   let rec aux lift_amount term context metasenv subst ugraph =
 597 (*     Printf.printf "enter aux %s\n" (CicPp.ppterm term); *)
 598     let res, lifted_term =
 599       match term with
 600       | C.Rel m  ->
 601           [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 602
 603       | C.Var (uri, exp_named_subst) ->
 604           let ens', lifted_ens =
 605             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
 606           in
 607           let expansions =
 608             List.map
 609               (fun (e, s, m, ug) ->
 610                  (C.Var (uri, e), s, m, ug)) ens'
 611           in
 612           expansions, C.Var (uri, lifted_ens)
 613
 614       | C.Meta (i, l) ->
 615           let l', lifted_l =
 616             List.fold_right
 617               (fun arg (res, lifted_tl) ->
 618                  match arg with
 619                  | Some arg ->
 620                      let arg_res, lifted_arg =
 621                        aux lift_amount arg context metasenv subst ugraph in
 622                      let l1 =
 623                        List.map
 624                          (fun (a, s, m, ug) -> (Some a)::lifted_tl, s, m, ug)
 625                          arg_res
 626                      in
 627                      (l1 @
 628                         (List.map
 629                            (fun (r, s, m, ug) -> (Some lifted_arg)::r, s, m, ug)
 630                            res),
 631                       (Some lifted_arg)::lifted_tl)
 632                  | None ->
 633                      (List.map
 634                         (fun (r, s, m, ug) -> None::r, s, m, ug)
 635                         res,
 636                       None::lifted_tl)
 637               ) l ([], [])
 638           in
 639           let e =
 640             List.map
 641               (fun (l, s, m, ug) ->
 642                  (C.Meta (i, l), s, m, ug)) l'
 643           in
 644           e, C.Meta (i, lifted_l)
 645
 646       | C.Sort _
 647       | C.Implicit _ as t -> [], t
 648
 649       | C.Cast (s, t) ->
 650           let l1, lifted_s =
 651             aux lift_amount s context metasenv subst ugraph in
 652           let l2, lifted_t =
 653             aux lift_amount t context metasenv subst ugraph
 654           in
 655           let l1' =
 656             List.map
 657               (fun (t, s, m, ug) ->
 658                  C.Cast (t, lifted_t), s, m, ug) l1 in
 659           let l2' =
 660             List.map
 661               (fun (t, s, m, ug) ->
 662                  C.Cast (lifted_s, t), s, m, ug) l2 in
 663           l1'@l2', C.Cast (lifted_s, lifted_t)
 664
 665       | C.Prod (nn, s, t) ->
 666           let l1, lifted_s =
 667             aux lift_amount s context metasenv subst ugraph in
 668           let l2, lifted_t =
 669             aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
 670               metasenv subst ugraph
 671           in
 672           let l1' =
 673             List.map
 674               (fun (t, s, m, ug) ->
 675                  C.Prod (nn, t, lifted_t), s, m, ug) l1 in
 676           let l2' =
 677             List.map
 678               (fun (t, s, m, ug) ->
 679                  C.Prod (nn, lifted_s, t), s, m, ug) l2 in
 680           l1'@l2', C.Prod (nn, lifted_s, lifted_t)
 681
 682       | C.Lambda (nn, s, t) ->
 683           let l1, lifted_s =
 684             aux lift_amount s context metasenv subst ugraph in
 685           let l2, lifted_t =
 686             aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
 687               metasenv subst ugraph
 688           in
 689           let l1' =
 690             List.map
 691               (fun (t, s, m, ug) ->
 692                  C.Lambda (nn, t, lifted_t), s, m, ug) l1 in
 693           let l2' =
 694             List.map
 695               (fun (t, s, m, ug) ->
 696                  C.Lambda (nn, lifted_s, t), s, m, ug) l2 in
 697           l1'@l2', C.Lambda (nn, lifted_s, lifted_t)
 698
 699       | C.LetIn (nn, s, t) ->
 700           let l1, lifted_s =
 701             aux lift_amount s context metasenv subst ugraph in
 702           let l2, lifted_t =
 703             aux (lift_amount+1) t ((Some (nn, C.Def (s, None)))::context)
 704               metasenv subst ugraph
 705           in
 706           let l1' =
 707             List.map
 708               (fun (t, s, m, ug) ->
 709                  C.LetIn (nn, t, lifted_t), s, m, ug) l1 in
 710           let l2' =
 711             List.map
 712               (fun (t, s, m, ug) ->
 713                  C.LetIn (nn, lifted_s, t), s, m, ug) l2 in
 714           l1'@l2', C.LetIn (nn, lifted_s, lifted_t)
 715
 716       | C.Appl l ->
 717           let l', lifted_l =
 718             aux_list lift_amount l context metasenv subst ugraph
 719           in
 720           (List.map (fun (l, s, m, ug) -> (C.Appl l, s, m, ug)) l',
 721            C.Appl lifted_l)
 722
 723       | C.Const (uri, exp_named_subst) ->
 724           let ens', lifted_ens =
 725             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
 726           in
 727           let expansions =
 728             List.map
 729               (fun (e, s, m, ug) ->
 730                  (C.Const (uri, e), s, m, ug)) ens'
 731           in
 732           (expansions, C.Const (uri, lifted_ens))
 733
 734       | C.MutInd (uri, i ,exp_named_subst) ->
 735           let ens', lifted_ens =
 736             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
 737           in
 738           let expansions =
 739             List.map
 740               (fun (e, s, m, ug) ->
 741                  (C.MutInd (uri, i, e), s, m, ug)) ens'
 742           in
 743           (expansions, C.MutInd (uri, i, lifted_ens))
 744
 745       | C.MutConstruct (uri, i, j, exp_named_subst) ->
 746           let ens', lifted_ens =
 747             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
 748           in
 749           let expansions =
 750             List.map
 751               (fun (e, s, m, ug) ->
 752                  (C.MutConstruct (uri, i, j, e), s, m, ug)) ens'
 753           in
 754           (expansions, C.MutConstruct (uri, i, j, lifted_ens))
 755
 756       | C.MutCase (sp, i, outt, t, pl) ->
 757           let pl_res, lifted_pl =
 758             aux_list lift_amount pl context metasenv subst ugraph
 759           in
 760           let l1, lifted_outt =
 761             aux lift_amount outt context metasenv subst ugraph in
 762           let l2, lifted_t =
 763             aux lift_amount t context metasenv subst ugraph in
 764
 765           let l1' =
 766             List.map
 767               (fun (outt, s, m, ug) ->
 768                  C.MutCase (sp, i, outt, lifted_t, lifted_pl), s, m, ug) l1 in
 769           let l2' =
 770             List.map
 771               (fun (t, s, m, ug) ->
 772                  C.MutCase (sp, i, lifted_outt, t, lifted_pl), s, m, ug) l2 in
 773           let l3' =
 774             List.map
 775               (fun (pl, s, m, ug) ->
 776                  C.MutCase (sp, i, lifted_outt, lifted_t, pl), s, m, ug) pl_res
 777           in
 778           (l1'@l2'@l3', C.MutCase (sp, i, lifted_outt, lifted_t, lifted_pl))
 779
 780       | C.Fix (i, fl) ->
 781           let len = List.length fl in
 782           let fl', lifted_fl =
 783             List.fold_right
 784               (fun (nm, idx, ty, bo) (res, lifted_tl) ->
 785                  let lifted_ty = S.lift lift_amount ty in
 786                  let bo_res, lifted_bo =
 787                    aux (lift_amount+len) bo context metasenv subst ugraph in
 788                  let l1 =
 789                    List.map
 790                      (fun (a, s, m, ug) ->
 791                         (nm, idx, lifted_ty, a)::lifted_tl, s, m, ug)
 792                      bo_res
 793                  in
 794                  (l1 @
 795                     (List.map
 796                        (fun (r, s, m, ug) ->
 797                           (nm, idx, lifted_ty, lifted_bo)::r, s, m, ug) res),
 798                   (nm, idx, lifted_ty, lifted_bo)::lifted_tl)
 799               ) fl ([], [])
 800           in
 801           (List.map
 802              (fun (fl, s, m, ug) -> C.Fix (i, fl), s, m, ug) fl',
 803            C.Fix (i, lifted_fl))
 804
 805       | C.CoFix (i, fl) ->
 806           let len = List.length fl in
 807           let fl', lifted_fl =
 808             List.fold_right
 809               (fun (nm, ty, bo) (res, lifted_tl) ->
 810                  let lifted_ty = S.lift lift_amount ty in
 811                  let bo_res, lifted_bo =
 812                    aux (lift_amount+len) bo context metasenv subst ugraph in
 813                  let l1 =
 814                    List.map
 815                      (fun (a, s, m, ug) ->
 816                         (nm, lifted_ty, a)::lifted_tl, s, m, ug)
 817                      bo_res
 818                  in
 819                  (l1 @
 820                     (List.map
 821                        (fun (r, s, m, ug) ->
 822                           (nm, lifted_ty, lifted_bo)::r, s, m, ug) res),
 823                   (nm, lifted_ty, lifted_bo)::lifted_tl)
 824               ) fl ([], [])
 825           in
 826           (List.map
 827              (fun (fl, s, m, ug) -> C.CoFix (i, fl), s, m, ug) fl',
 828            C.CoFix (i, lifted_fl))
 829     in
 830     let retval =
 831       match term with
 832       | C.Meta _ when (not metas_ok) ->
 833           res, lifted_term
 834       | _ ->
 835 (*           let term' = *)
 836 (*             if match_only then replace_metas context term *)
 837 (*             else term *)
 838 (*           in *)
 839           try
 840             let subst', metasenv', ugraph' =
 841 (*               Printf.printf "provo a unificare %s e %s\n" *)
 842 (*                 (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *)
 843               if match_only then
 844                 matching metasenv context term (S.lift lift_amount what) ugraph
 845               else
 846                 CicUnification.fo_unif metasenv context
 847                   (S.lift lift_amount what) term ugraph
 848             in
 849 (*           Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
 850 (*             (CicPp.ppterm (S.lift lift_amount what)); *)
 851 (*           Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
 852 (*           Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
 853             (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
 854 (*             if match_only then *)
 855 (*               let t' = CicMetaSubst.apply_subst subst' term in *)
 856 (*               if not (meta_convertibility term t') then ( *)
 857 (*                 res, lifted_term *)
 858 (*               ) else ( *)
 859 (*                 let metas = metas_of_term term in *)
 860 (*                 let fix_subst = function *)
 861 (*                   | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas -> *)
 862 (*                       (j, (c, C.Meta (i, lc), ty)) *)
 863 (*                   | s -> s *)
 864 (*                 in *)
 865 (*                 let subst' = List.map fix_subst subst' in *)
 866 (*                 ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, *)
 867 (*                  lifted_term) *)
 868 (*               ) *)
 869 (*             else *)
 870               ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
 871                lifted_term)
 872           with e ->
 873             if print_info then (
 874               print_endline ("beta_expand ERROR!: " ^ (Printexc.to_string e));
 875             );
 876             res, lifted_term
 877     in
 878 (*     Printf.printf "exit aux\n"; *)
 879     retval
 880
 881   and aux_list lift_amount l context metasenv subst ugraph =
 882     List.fold_right
 883       (fun arg (res, lifted_tl) ->
 884          let arg_res, lifted_arg =
 885            aux lift_amount arg context metasenv subst ugraph in
 886          let l1 = List.map
 887            (fun (a, s, m, ug) -> a::lifted_tl, s, m, ug) arg_res
 888          in
 889          (l1 @ (List.map
 890                   (fun (r, s, m, ug) -> lifted_arg::r, s, m, ug) res),
 891           lifted_arg::lifted_tl)
 892       ) l ([], [])
 893
 894   and aux_ens lift_amount exp_named_subst context metasenv subst ugraph =
 895     List.fold_right
 896       (fun (u, arg) (res, lifted_tl) ->
 897          let arg_res, lifted_arg =
 898            aux lift_amount arg context metasenv subst ugraph in
 899          let l1 =
 900            List.map
 901              (fun (a, s, m, ug) -> (u, a)::lifted_tl, s, m, ug) arg_res
 902          in
 903          (l1 @ (List.map (fun (r, s, m, ug) ->
 904                             (u, lifted_arg)::r, s, m, ug) res),
 905           (u, lifted_arg)::lifted_tl)
 906       ) exp_named_subst ([], [])
 907
 908   in
 909   let expansions, _ =
 910 (*     let where = *)
 911 (*       if match_only then replace_metas (\* context *\) where *)
 912 (*       else where *)
 913 (*     in *)
 914     if print_info then (
 915       Printf.printf "searching %s inside %s\n"
 916         (CicPp.ppterm what) (CicPp.ppterm where);
 917     );
 918     aux 0 where context metasenv [] ugraph
 919   in
 920   let mapfun =
 921 (*     if match_only then *)
 922 (*       (fun (term, subst, metasenv, ugraph) -> *)
 923 (*          let term' = *)
 924 (*            C.Lambda (C.Anonymous, type_of_what, restore_metas term) *)
 925 (*          and subst = restore_subst subst in *)
 926 (*          (term', subst, metasenv, ugraph)) *)
 927 (*     else *)
 928       (fun (term, subst, metasenv, ugraph) ->
 929          let term' = C.Lambda (C.Anonymous, type_of_what, term) in
 930          (term', subst, metasenv, ugraph))
 931   in
 932   List.map mapfun expansions
 933 ;;
 934
 935
 936 type equality =
 937     Cic.term  *          (* proof *)
 938     (Cic.term *          (* type *)
 939      Cic.term *          (* left side *)
 940      Cic.term *          (* right side *)
 941      Utils.comparison) * (* ordering *)
 942     Cic.metasenv *       (* environment for metas *)
 943     Cic.term list        (* arguments *)
 944 ;;
 945
 946
 947 let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
 948   let module C = Cic in
 949   let module S = CicSubstitution in
 950   let module T = CicTypeChecker in
 951   let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
 952   let rec aux index newmeta = function
 953     | [] -> [], newmeta
 954     | (Some (_, C.Decl (term)))::tl ->
 955         let do_find context term =
 956           match term with
 957           | C.Prod (name, s, t) ->
 958 (*               let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
 959               let (head, newmetas, args, _) =
 960                 PrimitiveTactics.new_metasenv_for_apply newmeta proof
 961                   context (S.lift index term)
 962               in
 963               let newmeta =
 964                 List.fold_left
 965                   (fun maxm arg ->
 966                      match arg with
 967                      | C.Meta (i, _) -> (max maxm i)
 968                      | _ -> assert false)
 969                   newmeta args
 970               in
 971               let p =
 972                 if List.length args = 0 then
 973                   C.Rel index
 974                 else
 975                   C.Appl ((C.Rel index)::args)
 976               in (
 977                 match head with
 978                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
 979                     Printf.printf "OK: %s\n" (CicPp.ppterm term);
 980                     let o = !Utils.compare_terms t1 t2 in
 981                     Some (p, (ty, t1, t2, o), newmetas, args), (newmeta+1)
 982                 | _ -> None, newmeta
 983               )
 984           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
 985               let t1 = S.lift index t1
 986               and t2 = S.lift index t2 in
 987               let o = !Utils.compare_terms t1 t2 in
 988               Some (C.Rel index, (ty, t1, t2, o), [], []), (newmeta+1)
 989           | _ -> None, newmeta
 990         in (
 991           match do_find context term with
 992           | Some p, newmeta ->
 993               let tl, newmeta' = (aux (index+1) newmeta tl) in
 994               p::tl, max newmeta newmeta'
 995           | None, _ ->
 996               aux (index+1) newmeta tl
 997         )
 998     | _::tl ->
 999         aux (index+1) newmeta tl
1000   in
1001   aux 1 newmeta context
1002 ;;
1003
1004
1005 let fix_metas newmeta ((proof, (ty, left, right, o), menv, args) as equality) =
1006   let table = Hashtbl.create (List.length args) in
1007   let newargs, _ =
1008     List.fold_right
1009       (fun t (newargs, index) ->
1010          match t with
1011          | Cic.Meta (i, l) ->
1012              Hashtbl.add table i index;
1013              ((Cic.Meta (index, l))::newargs, index+1)
1014          | _ -> assert false)
1015       args ([], newmeta)
1016   in
1017   let repl where =
1018     ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
1019       ~where
1020   in
1021   let menv' =
1022     List.fold_right
1023       (fun (i, context, term) menv ->
1024          try
1025            let index = Hashtbl.find table i in
1026            (index, context, term)::menv
1027          with Not_found ->
1028            (i, context, term)::menv)
1029       menv []
1030   in
1031   let ty = repl ty
1032   and left = repl left
1033   and right = repl right in
1034   let metas = (metas_of_term left) @ (metas_of_term right) in
1035   let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv'
1036   and newargs =
1037     List.filter
1038       (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
1039   in
1040   (newmeta + (List.length newargs) + 1,
1041    (repl proof, (ty, left, right, o), menv', newargs))
1042 ;;
1043
1044
1045 exception TermIsNotAnEquality;;
1046
1047 let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
1048   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
1049       let o = !Utils.compare_terms t1 t2 in
1050       (proof, (ty, t1, t2, o), [], [])
1051   | _ ->
1052       raise TermIsNotAnEquality
1053 ;;
1054
1055
1056 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
1057
1058
1059 let superposition_left (metasenv, context, ugraph) target source =
1060   let module C = Cic in
1061   let module S = CicSubstitution in
1062   let module M = CicMetaSubst in
1063   let module HL = HelmLibraryObjects in
1064   let module CR = CicReduction in
1065   (* we assume that target is ground (does not contain metavariables): this
1066    * should always be the case (I hope, at least) *)
1067   let proof, (eq_ty, left, right, t_order), _, _ = target in
1068   let eqproof, (ty, t1, t2, s_order), newmetas, args = source in
1069
1070   let compare_terms = !Utils.compare_terms in
1071
1072   if eq_ty <> ty then
1073     []
1074   else
1075     let where, is_left =
1076       match t_order (* compare_terms left right *) with
1077       | Lt -> right, false
1078       | Gt -> left, true
1079       | _ -> (
1080           Printf.printf "????????? %s = %s" (CicPp.ppterm left)
1081             (CicPp.ppterm right);
1082           print_newline ();
1083           assert false (* again, for ground terms this shouldn't happen... *)
1084         )
1085     in
1086     let metasenv' = newmetas @ metasenv in
1087     let result = s_order (* compare_terms t1 t2 *) in
1088     let res1, res2 =
1089       match result with
1090       | Gt -> (beta_expand t1 ty where context metasenv' ugraph), []
1091       | Lt -> [], (beta_expand t2 ty where context metasenv' ugraph)
1092       | _ ->
1093           let res1 =
1094             List.filter
1095               (fun (t, s, m, ug) ->
1096                  compare_terms (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
1097               (beta_expand t1 ty where context metasenv' ugraph)
1098           and res2 =
1099             List.filter
1100               (fun (t, s, m, ug) ->
1101                  compare_terms (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
1102               (beta_expand t2 ty where context metasenv' ugraph)
1103           in
1104           res1, res2
1105     in
1106     (*   let what, other = *)
1107     (*     if is_left then left, right *)
1108     (*     else right, left *)
1109     (*   in *)
1110     let build_new what other eq_URI (t, s, m, ug) =
1111       let newgoal, newgoalproof =
1112         match t with
1113         | C.Lambda (nn, ty, bo) ->
1114             let bo' = S.subst (M.apply_subst s other) bo in
1115             let bo'' =
1116               C.Appl (
1117                 [C.MutInd (HL.Logic.eq_URI, 0, []);
1118                  S.lift 1 eq_ty] @
1119                   if is_left then [bo'; S.lift 1 right]
1120                   else [S.lift 1 left; bo'])
1121             in
1122             let t' = C.Lambda (nn, ty, bo'') in
1123             S.subst (M.apply_subst s other) bo,
1124             M.apply_subst s
1125               (C.Appl [C.Const (eq_URI, []); ty; what; t';
1126                        proof; other; eqproof])
1127         | _ -> assert false
1128       in
1129       let equation =
1130         if is_left then (eq_ty, newgoal, right, compare_terms newgoal right)
1131         else (eq_ty, left, newgoal, compare_terms left newgoal)
1132       in
1133       (newgoalproof (* eqproof *), equation, [], [])
1134     in
1135     let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1
1136     and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in
1137     new1 @ new2
1138 ;;
1139
1140
1141 let superposition_right newmeta (metasenv, context, ugraph) target source =
1142   let module C = Cic in
1143   let module S = CicSubstitution in
1144   let module M = CicMetaSubst in
1145   let module HL = HelmLibraryObjects in
1146   let module CR = CicReduction in
1147   let eqproof, (eq_ty, left, right, t_order), newmetas, args = target in
1148   let eqp', (ty', t1, t2, s_order), newm', args' = source in
1149   let maxmeta = ref newmeta in
1150
1151   let compare_terms = !Utils.compare_terms in
1152
1153   if eq_ty <> ty' then
1154     newmeta, []
1155   else
1156     (*   let ok term subst other other_eq_side ugraph = *)
1157     (*     match term with *)
1158     (*     | C.Lambda (nn, ty, bo) -> *)
1159     (*         let bo' = S.subst (M.apply_subst subst other) bo in *)
1160     (*         let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *)
1161     (*         not res *)
1162     (*     |  _ -> assert false *)
1163     (*   in *)
1164     let condition left right what other (t, s, m, ug) =
1165       let subst = M.apply_subst s in
1166       let cmp1 = compare_terms (subst what) (subst other) in
1167       let cmp2 = compare_terms (subst left) (subst right) in
1168       (*     cmp1 = Gt && cmp2 = Gt *)
1169       cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
1170         (*     && (ok t s other right ug) *)
1171     in
1172     let metasenv' = metasenv @ newmetas @ newm' in
1173     let beta_expand = beta_expand ~metas_ok:false in
1174     let cmp1 = t_order (* compare_terms left right *)
1175     and cmp2 = s_order (* compare_terms t1 t2 *) in
1176     let res1, res2, res3, res4 =
1177       let res l r s t =
1178         List.filter
1179           (condition l r s t)
1180           (beta_expand s eq_ty l context metasenv' ugraph)
1181       in
1182       match cmp1, cmp2 with
1183       | Gt, Gt ->
1184           (beta_expand t1 eq_ty left context metasenv' ugraph), [], [], []
1185       | Gt, Lt ->
1186           [], (beta_expand t2 eq_ty left context metasenv' ugraph), [], []
1187       | Lt, Gt ->
1188           [], [], (beta_expand t1 eq_ty right context metasenv' ugraph), []
1189       | Lt, Lt ->
1190           [], [], [], (beta_expand t2 eq_ty right context metasenv' ugraph)
1191       | Gt, _ ->
1192           let res1 = res left right t1 t2
1193           and res2 = res left right t2 t1 in
1194           res1, res2, [], []
1195       | Lt, _ ->
1196           let res3 = res right left t1 t2
1197           and res4 = res right left t2 t1 in
1198           [], [], res3, res4
1199       | _, Gt ->
1200           let res1 = res left right t1 t2
1201           and res3 = res right left t1 t2 in
1202           res1, [], res3, []
1203       | _, Lt ->
1204           let res2 = res left right t2 t1
1205           and res4 = res right left t2 t1 in
1206           [], res2, [], res4
1207       | _, _ ->
1208           let res1 = res left right t1 t2
1209           and res2 = res left right t2 t1
1210           and res3 = res right left t1 t2
1211           and res4 = res right left t2 t1 in
1212           res1, res2, res3, res4
1213     in
1214     let newmetas = newmetas @ newm' in
1215     let newargs = args @ args' in
1216     let build_new what other is_left eq_URI (t, s, m, ug) =
1217       (*     let what, other = *)
1218       (*       if is_left then left, right *)
1219       (*       else right, left *)
1220       (*     in *)
1221       let newterm, neweqproof =
1222         match t with
1223         | C.Lambda (nn, ty, bo) ->
1224             let bo' = M.apply_subst s (S.subst other bo) in
1225             let bo'' =
1226               C.Appl (
1227                 [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
1228                   if is_left then [bo'; S.lift 1 right]
1229                   else [S.lift 1 left; bo'])
1230             in
1231             let t' = C.Lambda (nn, ty, bo'') in
1232             bo',
1233             M.apply_subst s
1234               (C.Appl [C.Const (eq_URI, []); ty; what; t';
1235                        eqproof; other; eqp'])
1236         | _ -> assert false
1237       in
1238       let newmeta, newequality =
1239         let left, right =
1240           if is_left then (newterm, M.apply_subst s right)
1241           else (M.apply_subst s left, newterm) in
1242         let neworder = compare_terms left right in
1243         fix_metas !maxmeta
1244           (neweqproof, (eq_ty, left, right, neworder), newmetas, newargs)
1245       in
1246       maxmeta := newmeta;
1247       newequality
1248     in
1249     let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
1250     and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
1251     and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
1252     and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
1253     let ok = function
1254       | _, (_, left, right, _), _, _ ->
1255           not (fst (CR.are_convertible context left right ugraph))
1256     in
1257     (!maxmeta,
1258      (List.filter ok (new1 @ new2 @ new3 @ new4)))
1259 ;;
1260
1261
1262 let is_identity ((_, context, ugraph) as env) = function
1263   | ((_, (ty, left, right, _), _, _) as equality) ->
1264       let res =
1265         (left = right ||
1266             (fst (CicReduction.are_convertible context left right ugraph)))
1267       in
1268 (*       if res then ( *)
1269 (*         Printf.printf "is_identity: %s" (string_of_equality ~env equality); *)
1270 (*         print_newline (); *)
1271 (*       ); *)
1272       res
1273 ;;
1274
1275
1276 let demodulation newmeta (metasenv, context, ugraph) target source =
1277   let module C = Cic in
1278   let module S = CicSubstitution in
1279   let module M = CicMetaSubst in
1280   let module HL = HelmLibraryObjects in
1281   let module CR = CicReduction in
1282
1283   let proof, (eq_ty, left, right, t_order), metas, args = target
1284   and proof', (ty, t1, t2, s_order), metas', args' = source in
1285
1286   let compare_terms = !Utils.compare_terms in
1287
1288   if eq_ty <> ty then
1289     newmeta, target
1290   else
1291     let first_step, get_params =
1292       match s_order (* compare_terms t1 t2 *) with
1293       | Gt -> 1, (function
1294                     | 1 -> true, t1, t2, HL.Logic.eq_ind_URI
1295                     | 0 -> false, t1, t2, HL.Logic.eq_ind_URI
1296                     | _ -> assert false)
1297       | Lt -> 1, (function
1298                     | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
1299                     | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
1300                     | _ -> assert false)
1301       | _ ->
1302           let first_step = 3 in
1303           let get_params step =
1304             match step with
1305             | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
1306             | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
1307             | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
1308             | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
1309             | _ -> assert false
1310           in
1311           first_step, get_params
1312     in
1313     let rec demodulate newmeta step metasenv target =
1314       let proof, (eq_ty, left, right, t_order), metas, args = target in
1315       let is_left, what, other, eq_URI = get_params step in
1316
1317       let env = metasenv, context, ugraph in
1318       let names = names_of_context context in
1319 (*       Printf.printf *)
1320 (*         "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
1321 (*         (string_of_equality ~env target) (CicPp.pp what names) *)
1322 (*         (CicPp.pp other names) (string_of_bool is_left); *)
1323 (*       Printf.printf "step: %d" step; *)
1324 (*       print_newline (); *)
1325
1326       let ok (t, s, m, ug) =
1327         compare_terms (M.apply_subst s what) (M.apply_subst s other) = Gt
1328       in
1329       let res =
1330         let r = (beta_expand ~metas_ok:false ~match_only:true
1331                    what ty (if is_left then left else right)
1332                    context (metasenv @ metas) ugraph)
1333         in
1334 (*         let m' = metas_of_term what *)
1335 (*         and m'' = metas_of_term (if is_left then left else right) in *)
1336 (*         if (List.mem 527 m'') && (List.mem 6 m') then ( *)
1337 (*           Printf.printf *)
1338 (*             "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
1339 (*             (string_of_equality ~env target) (CicPp.pp what names) *)
1340 (*             (CicPp.pp other names) (string_of_bool is_left); *)
1341 (*           Printf.printf "step: %d" step; *)
1342 (*           print_newline (); *)
1343 (*           print_endline "res:"; *)
1344 (*           List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *)
1345 (*           print_newline (); *)
1346 (*           Printf.printf "metasenv:\n%s\n" (print_metasenv (metasenv @ metas)); *)
1347 (*           print_newline (); *)
1348 (*         ); *)
1349         List.filter ok r
1350       in
1351       match res with
1352       | [] ->
1353           if step = 0 then newmeta, target
1354           else demodulate newmeta (step-1) metasenv target
1355       | (t, s, m, ug)::_ ->
1356           let newterm, newproof =
1357             match t with
1358             | C.Lambda (nn, ty, bo) ->
1359 (*                 let bo' = M.apply_subst s (S.subst other bo) in *)
1360                 let bo' = S.subst (M.apply_subst s other) bo in
1361                 let bo'' =
1362                   C.Appl (
1363                     [C.MutInd (HL.Logic.eq_URI, 0, []);
1364                      S.lift 1 eq_ty] @
1365                       if is_left then [bo'; S.lift 1 right]
1366                       else [S.lift 1 left; bo'])
1367                 in
1368                 let t' = C.Lambda (nn, ty, bo'') in
1369 (*                 M.apply_subst s (S.subst other bo), *)
1370                 bo',
1371                 M.apply_subst s
1372                   (C.Appl [C.Const (eq_URI, []); ty; what; t';
1373                            proof; other; proof'])
1374             | _ -> assert false
1375           in
1376           let newmeta, newtarget =
1377             let left, right =
1378 (*               if is_left then (newterm, M.apply_subst s right) *)
1379 (*               else (M.apply_subst s left, newterm) in *)
1380               if is_left then newterm, right
1381               else left, newterm
1382             in
1383             let neworder = compare_terms left right in
1384 (*             let newmetasenv = metasenv @ metas in *)
1385 (*             let newargs = args @ args' in *)
1386 (*             fix_metas newmeta *)
1387 (*               (newproof, (eq_ty, left, right), newmetasenv, newargs) *)
1388             let m = (metas_of_term left) @ (metas_of_term right) in
1389             let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
1390             and newargs =
1391               List.filter
1392                 (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
1393                 args
1394             in
1395             newmeta,
1396             (newproof, (eq_ty, left, right, neworder), newmetasenv, newargs)
1397           in
1398 (*           Printf.printf *)
1399 (*             "demodulate, newtarget: %s\ntarget was: %s\n" *)
1400 (*             (string_of_equality ~env newtarget) *)
1401 (*             (string_of_equality ~env target); *)
1402 (* (\*           let _, _, newm, newa = newtarget in *\) *)
1403 (* (\*           Printf.printf "newmetasenv:\n%s\nnewargs:\n%s\n" *\) *)
1404 (* (\*             (print_metasenv newm) *\) *)
1405 (* (\*             (String.concat "\n" (List.map CicPp.ppterm newa)); *\) *)
1406 (*           print_newline (); *)
1407           if is_identity env newtarget then
1408             newmeta, newtarget
1409           else
1410             demodulate newmeta first_step metasenv newtarget
1411     in
1412     demodulate newmeta first_step (metasenv @ metas') target
1413 ;;
1414
1415
1416 (*
1417 let demodulation newmeta env target source =
1418   newmeta, target
1419 ;;
1420 *)
1421
1422
1423 let subsumption env target source =
1424   let _, (ty, tl, tr, _), tmetas, _ = target
1425   and _, (ty', sl, sr, _), smetas, _ = source in
1426   if ty <> ty' then
1427     false
1428   else
1429     let metasenv, context, ugraph = env in
1430     let metasenv = metasenv @ tmetas @ smetas in
1431     let names = names_of_context context in
1432     let samesubst subst subst' =
1433 (*       Printf.printf "samesubst:\nsubst: %s\nsubst': %s\n" *)
1434 (*         (print_subst subst) (print_subst subst'); *)
1435 (*       print_newline (); *)
1436       let tbl = Hashtbl.create (List.length subst) in
1437       List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
1438       List.for_all
1439         (fun (m, (c, t1, t2)) ->
1440            try
1441              let c', t1', t2' = Hashtbl.find tbl m in
1442              if (c = c') && (t1 = t1') && (t2 = t2') then true
1443              else false
1444            with Not_found ->
1445              true)
1446         subst'
1447     in
1448     let subsaux left right left' right' =
1449       try
1450         let subst, menv, ug = matching metasenv context left left' ugraph
1451         and subst', menv', ug' = matching metasenv context right right' ugraph
1452         in
1453 (*         Printf.printf "left = right: %s = %s\n" *)
1454 (*           (CicPp.pp left names) (CicPp.pp right names); *)
1455 (*         Printf.printf "left' = right': %s = %s\n" *)
1456 (*           (CicPp.pp left' names) (CicPp.pp right' names);         *)
1457         samesubst subst subst'
1458       with e ->
1459 (*         print_endline (Printexc.to_string e); *)
1460         false
1461     in
1462     let res =
1463       if subsaux tl tr sl sr then true
1464       else subsaux tl tr sr sl
1465     in
1466     if res then (
1467       Printf.printf "subsumption!:\ntarget: %s\nsource: %s\n"
1468         (string_of_equality ~env target) (string_of_equality ~env source);
1469       print_newline ();
1470     );
1471     res
1472 ;;
1473
1474
1475 let extract_differing_subterms t1 t2 =
1476   let module C = Cic in
1477   let rec aux t1 t2 =
1478     match t1, t2 with
1479     | C.Appl l1, C.Appl l2 when (List.length l1) <> (List.length l2) ->
1480         [(t1, t2)]
1481     | C.Appl (h1::tl1), C.Appl (h2::tl2) ->
1482         let res = List.concat (List.map2 aux tl1 tl2) in
1483         if h1 <> h2 then
1484           if res = [] then [(h1, h2)] else [(t1, t2)]
1485         else
1486           if List.length res > 1 then [(t1, t2)] else res
1487     | t1, t2 ->
1488         if t1 <> t2 then [(t1, t2)] else []
1489   in
1490   let res = aux t1 t2 in
1491   match res with
1492   | hd::[] -> Some hd
1493   | _ -> None
1494 ;;