helm/ocaml/paramodulation/inference.ml

   1 open Utils;;
   2
   3
   4 exception NotMetaConvertible;;
   5
   6 let meta_convertibility_aux table t1 t2 =
   7   let module C = Cic in
   8   let rec aux table t1 t2 =
   9     match t1, t2 with
  10     | t1, t2 when t1 = t2 -> table
  11     | C.Meta (m1, tl1), C.Meta (m2, tl2) ->
  12         let m1_binding, table =
  13           try List.assoc m1 table, table
  14           with Not_found -> m2, (m1, m2)::table
  15         in
  16         if m1_binding <> m2 then
  17           raise NotMetaConvertible
  18         else (
  19           try
  20             List.fold_left2
  21               (fun res t1 t2 ->
  22                  match t1, t2 with
  23                  | None, Some _ | Some _, None -> raise NotMetaConvertible
  24                  | None, None -> res
  25                  | Some t1, Some t2 -> (aux res t1 t2))
  26               table tl1 tl2
  27           with Invalid_argument _ ->
  28             raise NotMetaConvertible
  29         )
  30     | C.Var (u1, ens1), C.Var (u2, ens2)
  31     | C.Const (u1, ens1), C.Const (u2, ens2) when (UriManager.eq u1 u2) ->
  32         aux_ens table ens1 ens2
  33     | C.Cast (s1, t1), C.Cast (s2, t2)
  34     | C.Prod (_, s1, t1), C.Prod (_, s2, t2)
  35     | C.Lambda (_, s1, t1), C.Lambda (_, s2, t2)
  36     | C.LetIn (_, s1, t1), C.LetIn (_, s2, t2) ->
  37         let table = aux table s1 s2 in
  38         aux table t1 t2
  39     | C.Appl l1, C.Appl l2 -> (
  40         try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
  41         with Invalid_argument _ -> raise NotMetaConvertible
  42       )
  43     | C.MutInd (u1, i1, ens1), C.MutInd (u2, i2, ens2)
  44         when (UriManager.eq u1 u2) && i1 = i2 -> aux_ens table ens1 ens2
  45     | C.MutConstruct (u1, i1, j1, ens1), C.MutConstruct (u2, i2, j2, ens2)
  46         when (UriManager.eq u1 u2) && i1 = i2 && j1 = j2 ->
  47         aux_ens table ens1 ens2
  48     | C.MutCase (u1, i1, s1, t1, l1), C.MutCase (u2, i2, s2, t2, l2)
  49         when (UriManager.eq u1 u2) && i1 = i2 ->
  50         let table = aux table s1 s2 in
  51         let table = aux table t1 t2 in (
  52           try List.fold_left2 (fun res t1 t2 -> (aux res t1 t2)) table l1 l2
  53           with Invalid_argument _ -> raise NotMetaConvertible
  54         )
  55     | C.Fix (i1, il1), C.Fix (i2, il2) when i1 = i2 -> (
  56         try
  57           List.fold_left2
  58             (fun res (n1, i1, s1, t1) (n2, i2, s2, t2) ->
  59                if i1 <> i2 then raise NotMetaConvertible
  60                else
  61                  let res = (aux res s1 s2) in aux res t1 t2)
  62             table il1 il2
  63         with Invalid_argument _ -> raise NotMetaConvertible
  64       )
  65     | C.CoFix (i1, il1), C.CoFix (i2, il2) when i1 = i2 -> (
  66         try
  67           List.fold_left2
  68             (fun res (n1, s1, t1) (n2, s2, t2) ->
  69                let res = aux res s1 s2 in aux res t1 t2)
  70             table il1 il2
  71         with Invalid_argument _ -> raise NotMetaConvertible
  72       )
  73     | _, _ -> raise NotMetaConvertible
  74
  75   and aux_ens table ens1 ens2 =
  76     let cmp (u1, t1) (u2, t2) =
  77       compare (UriManager.string_of_uri u1) (UriManager.string_of_uri u2)
  78     in
  79     let ens1 = List.sort cmp ens1
  80     and ens2 = List.sort cmp ens2 in
  81     try
  82       List.fold_left2
  83         (fun res (u1, t1) (u2, t2) ->
  84            if not (UriManager.eq u1 u2) then raise NotMetaConvertible
  85            else aux res t1 t2)
  86         table ens1 ens2
  87     with Invalid_argument _ -> raise NotMetaConvertible
  88   in
  89   aux table t1 t2
  90 ;;
  91
  92
  93 let meta_convertibility_eq eq1 eq2 =
  94   let _, (ty, left, right), _, _ = eq1
  95   and _, (ty', left', right'), _, _ = eq2 in
  96   if ty <> ty' then
  97     false
  98   else
  99     let print_table t w =
 100       Printf.printf "table %s is:\n" w;
 101       List.iter
 102         (fun (k, v) -> Printf.printf "?%d: ?%d\n" k v)
 103         t;
 104       print_newline ();
 105     in
 106     try
 107       let table = meta_convertibility_aux [] left left' in
 108 (*       print_table table "before"; *)
 109       let table = meta_convertibility_aux table right right' in
 110 (*       print_table table "after"; *)
 111       true
 112     with NotMetaConvertible ->
 113 (*       Printf.printf "NotMetaConvertible:\n%s = %s\n%s = %s\n\n" *)
 114 (*         (CicPp.ppterm left) (CicPp.ppterm right) *)
 115 (*         (CicPp.ppterm left') (CicPp.ppterm right'); *)
 116       false
 117 ;;
 118
 119
 120 let meta_convertibility t1 t2 =
 121   try
 122     let _ = meta_convertibility_aux [] t1 t2 in
 123     true
 124   with NotMetaConvertible ->
 125     false
 126 ;;
 127
 128
 129 let beta_expand ?(metas_ok=true) ?(match_only=false)
 130     what type_of_what where context metasenv ugraph =
 131   let module S = CicSubstitution in
 132   let module C = Cic in
 133   (*
 134     return value:
 135     ((list of all possible beta expansions, subst, metasenv, ugraph),
 136      lifted term)
 137   *)
 138   let rec aux lift_amount term context metasenv subst ugraph =
 139 (*     Printf.printf "enter aux %s\n" (CicPp.ppterm term); *)
 140     let res, lifted_term =
 141       match term with
 142       | C.Rel m  ->
 143           [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
 144
 145       | C.Var (uri, exp_named_subst) ->
 146           let ens', lifted_ens =
 147             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
 148           in
 149           let expansions =
 150             List.map
 151               (fun (e, s, m, ug) ->
 152                  (C.Var (uri, e), s, m, ug)) ens'
 153           in
 154           expansions, C.Var (uri, lifted_ens)
 155
 156       | C.Meta (i, l) ->
 157           let l', lifted_l =
 158             List.fold_right
 159               (fun arg (res, lifted_tl) ->
 160                  match arg with
 161                  | Some arg ->
 162                      let arg_res, lifted_arg =
 163                        aux lift_amount arg context metasenv subst ugraph in
 164                      let l1 =
 165                        List.map
 166                          (fun (a, s, m, ug) -> (Some a)::lifted_tl, s, m, ug)
 167                          arg_res
 168                      in
 169                      (l1 @
 170                         (List.map
 171                            (fun (r, s, m, ug) -> (Some lifted_arg)::r, s, m, ug)
 172                            res),
 173                       (Some lifted_arg)::lifted_tl)
 174                  | None ->
 175                      (List.map
 176                         (fun (r, s, m, ug) -> None::r, s, m, ug)
 177                         res,
 178                       None::lifted_tl)
 179               ) l ([], [])
 180           in
 181           let e =
 182             List.map
 183               (fun (l, s, m, ug) ->
 184                  (C.Meta (i, l), s, m, ug)) l'
 185           in
 186           e, C.Meta (i, lifted_l)
 187
 188       | C.Sort _
 189       | C.Implicit _ as t -> [], t
 190
 191       | C.Cast (s, t) ->
 192           let l1, lifted_s =
 193             aux lift_amount s context metasenv subst ugraph in
 194           let l2, lifted_t =
 195             aux lift_amount t context metasenv subst ugraph
 196           in
 197           let l1' =
 198             List.map
 199               (fun (t, s, m, ug) ->
 200                  C.Cast (t, lifted_t), s, m, ug) l1 in
 201           let l2' =
 202             List.map
 203               (fun (t, s, m, ug) ->
 204                  C.Cast (lifted_s, t), s, m, ug) l2 in
 205           l1'@l2', C.Cast (lifted_s, lifted_t)
 206
 207       | C.Prod (nn, s, t) ->
 208           let l1, lifted_s =
 209             aux lift_amount s context metasenv subst ugraph in
 210           let l2, lifted_t =
 211             aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
 212               metasenv subst ugraph
 213           in
 214           let l1' =
 215             List.map
 216               (fun (t, s, m, ug) ->
 217                  C.Prod (nn, t, lifted_t), s, m, ug) l1 in
 218           let l2' =
 219             List.map
 220               (fun (t, s, m, ug) ->
 221                  C.Prod (nn, lifted_s, t), s, m, ug) l2 in
 222           l1'@l2', C.Prod (nn, lifted_s, lifted_t)
 223
 224       | C.Lambda (nn, s, t) ->
 225           let l1, lifted_s =
 226             aux lift_amount s context metasenv subst ugraph in
 227           let l2, lifted_t =
 228             aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
 229               metasenv subst ugraph
 230           in
 231           let l1' =
 232             List.map
 233               (fun (t, s, m, ug) ->
 234                  C.Lambda (nn, t, lifted_t), s, m, ug) l1 in
 235           let l2' =
 236             List.map
 237               (fun (t, s, m, ug) ->
 238                  C.Lambda (nn, lifted_s, t), s, m, ug) l2 in
 239           l1'@l2', C.Lambda (nn, lifted_s, lifted_t)
 240
 241       | C.LetIn (nn, s, t) ->
 242           let l1, lifted_s =
 243             aux lift_amount s context metasenv subst ugraph in
 244           let l2, lifted_t =
 245             aux (lift_amount+1) t ((Some (nn, C.Def (s, None)))::context)
 246               metasenv subst ugraph
 247           in
 248           let l1' =
 249             List.map
 250               (fun (t, s, m, ug) ->
 251                  C.LetIn (nn, t, lifted_t), s, m, ug) l1 in
 252           let l2' =
 253             List.map
 254               (fun (t, s, m, ug) ->
 255                  C.LetIn (nn, lifted_s, t), s, m, ug) l2 in
 256           l1'@l2', C.LetIn (nn, lifted_s, lifted_t)
 257
 258       | C.Appl l ->
 259           let l', lifted_l =
 260             aux_list lift_amount l context metasenv subst ugraph
 261           in
 262           (List.map (fun (l, s, m, ug) -> (C.Appl l, s, m, ug)) l',
 263            C.Appl lifted_l)
 264
 265       | C.Const (uri, exp_named_subst) ->
 266           let ens', lifted_ens =
 267             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
 268           in
 269           let expansions =
 270             List.map
 271               (fun (e, s, m, ug) ->
 272                  (C.Const (uri, e), s, m, ug)) ens'
 273           in
 274           (expansions, C.Const (uri, lifted_ens))
 275
 276       | C.MutInd (uri, i ,exp_named_subst) ->
 277           let ens', lifted_ens =
 278             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
 279           in
 280           let expansions =
 281             List.map
 282               (fun (e, s, m, ug) ->
 283                  (C.MutInd (uri, i, e), s, m, ug)) ens'
 284           in
 285           (expansions, C.MutInd (uri, i, lifted_ens))
 286
 287       | C.MutConstruct (uri, i, j, exp_named_subst) ->
 288           let ens', lifted_ens =
 289             aux_ens lift_amount exp_named_subst context metasenv subst ugraph
 290           in
 291           let expansions =
 292             List.map
 293               (fun (e, s, m, ug) ->
 294                  (C.MutConstruct (uri, i, j, e), s, m, ug)) ens'
 295           in
 296           (expansions, C.MutConstruct (uri, i, j, lifted_ens))
 297
 298       | C.MutCase (sp, i, outt, t, pl) ->
 299           let pl_res, lifted_pl =
 300             aux_list lift_amount pl context metasenv subst ugraph
 301           in
 302           let l1, lifted_outt =
 303             aux lift_amount outt context metasenv subst ugraph in
 304           let l2, lifted_t =
 305             aux lift_amount t context metasenv subst ugraph in
 306
 307           let l1' =
 308             List.map
 309               (fun (outt, s, m, ug) ->
 310                  C.MutCase (sp, i, outt, lifted_t, lifted_pl), s, m, ug) l1 in
 311           let l2' =
 312             List.map
 313               (fun (t, s, m, ug) ->
 314                  C.MutCase (sp, i, lifted_outt, t, lifted_pl), s, m, ug) l2 in
 315           let l3' =
 316             List.map
 317               (fun (pl, s, m, ug) ->
 318                  C.MutCase (sp, i, lifted_outt, lifted_t, pl), s, m, ug) pl_res
 319           in
 320           (l1'@l2'@l3', C.MutCase (sp, i, lifted_outt, lifted_t, lifted_pl))
 321
 322       | C.Fix (i, fl) ->
 323           let len = List.length fl in
 324           let fl', lifted_fl =
 325             List.fold_right
 326               (fun (nm, idx, ty, bo) (res, lifted_tl) ->
 327                  let lifted_ty = S.lift lift_amount ty in
 328                  let bo_res, lifted_bo =
 329                    aux (lift_amount+len) bo context metasenv subst ugraph in
 330                  let l1 =
 331                    List.map
 332                      (fun (a, s, m, ug) ->
 333                         (nm, idx, lifted_ty, a)::lifted_tl, s, m, ug)
 334                      bo_res
 335                  in
 336                  (l1 @
 337                     (List.map
 338                        (fun (r, s, m, ug) ->
 339                           (nm, idx, lifted_ty, lifted_bo)::r, s, m, ug) res),
 340                   (nm, idx, lifted_ty, lifted_bo)::lifted_tl)
 341               ) fl ([], [])
 342           in
 343           (List.map
 344              (fun (fl, s, m, ug) -> C.Fix (i, fl), s, m, ug) fl',
 345            C.Fix (i, lifted_fl))
 346
 347       | C.CoFix (i, fl) ->
 348           let len = List.length fl in
 349           let fl', lifted_fl =
 350             List.fold_right
 351               (fun (nm, ty, bo) (res, lifted_tl) ->
 352                  let lifted_ty = S.lift lift_amount ty in
 353                  let bo_res, lifted_bo =
 354                    aux (lift_amount+len) bo context metasenv subst ugraph in
 355                  let l1 =
 356                    List.map
 357                      (fun (a, s, m, ug) ->
 358                         (nm, lifted_ty, a)::lifted_tl, s, m, ug)
 359                      bo_res
 360                  in
 361                  (l1 @
 362                     (List.map
 363                        (fun (r, s, m, ug) ->
 364                           (nm, lifted_ty, lifted_bo)::r, s, m, ug) res),
 365                   (nm, lifted_ty, lifted_bo)::lifted_tl)
 366               ) fl ([], [])
 367           in
 368           (List.map
 369              (fun (fl, s, m, ug) -> C.CoFix (i, fl), s, m, ug) fl',
 370            C.CoFix (i, lifted_fl))
 371     in
 372     let retval =
 373       match term with
 374       | C.Meta _ when (not metas_ok) ->
 375           res, lifted_term
 376       | _ ->
 377           try
 378             let subst', metasenv', ugraph' =
 379               CicUnification.fo_unif metasenv context
 380                 (S.lift lift_amount what) term ugraph
 381             in
 382             (*           Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
 383             (*             (CicPp.ppterm (S.lift lift_amount what)); *)
 384             (*           Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
 385             (*           Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
 386             (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
 387             let term' = CicMetaSubst.apply_subst subst' term in (
 388               if match_only && not (meta_convertibility term term') then (
 389 (*                 Printf.printf "term e term' sono diversi!:\n%s\n%s\n\n" *)
 390 (*                   (CicPp.ppterm term) (CicPp.ppterm term'); *)
 391                 res, lifted_term
 392               )
 393               else
 394 (*                 let _ = *)
 395 (*                   if match_only then *)
 396 (*                     Printf.printf "OK, trovato match con %s\n" *)
 397 (*                       (CicPp.ppterm term) *)
 398 (*                 in *)
 399                 ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
 400                  lifted_term)
 401             )
 402           with _ ->
 403             res, lifted_term
 404     in
 405 (*     Printf.printf "exit aux\n"; *)
 406     retval
 407
 408   and aux_list lift_amount l context metasenv subst ugraph =
 409     List.fold_right
 410       (fun arg (res, lifted_tl) ->
 411          let arg_res, lifted_arg =
 412            aux lift_amount arg context metasenv subst ugraph in
 413          let l1 = List.map
 414            (fun (a, s, m, ug) -> a::lifted_tl, s, m, ug) arg_res
 415          in
 416          (l1 @ (List.map
 417                   (fun (r, s, m, ug) -> lifted_arg::r, s, m, ug) res),
 418           lifted_arg::lifted_tl)
 419       ) l ([], [])
 420
 421   and aux_ens lift_amount exp_named_subst context metasenv subst ugraph =
 422     List.fold_right
 423       (fun (u, arg) (res, lifted_tl) ->
 424          let arg_res, lifted_arg =
 425            aux lift_amount arg context metasenv subst ugraph in
 426          let l1 =
 427            List.map
 428              (fun (a, s, m, ug) -> (u, a)::lifted_tl, s, m, ug) arg_res
 429          in
 430          (l1 @ (List.map (fun (r, s, m, ug) ->
 431                             (u, lifted_arg)::r, s, m, ug) res),
 432           (u, lifted_arg)::lifted_tl)
 433       ) exp_named_subst ([], [])
 434
 435   in
 436   let expansions, _ = aux 0 where context metasenv [] ugraph in
 437   List.map
 438     (fun (term, subst, metasenv, ugraph) ->
 439        let term' = C.Lambda (C.Anonymous, type_of_what, term) in
 440 (*        Printf.printf "term is: %s\nsubst is:\n%s\n\n" *)
 441 (*          (CicPp.ppterm term') (print_subst subst); *)
 442        (term', subst, metasenv, ugraph))
 443     expansions
 444 ;;
 445
 446
 447 type equality =
 448     Cic.term  *    (* proof *)
 449     (Cic.term *    (* type *)
 450      Cic.term *    (* left side *)
 451      Cic.term) *   (* right side *)
 452     Cic.metasenv * (* environment for metas *)
 453     Cic.term list  (* arguments *)
 454 ;;
 455
 456
 457 let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
 458   let module C = Cic in
 459   let module S = CicSubstitution in
 460   let module T = CicTypeChecker in
 461   let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
 462   let rec aux index newmeta = function
 463     | [] -> [], newmeta
 464     | (Some (_, C.Decl (term)))::tl ->
 465         let do_find context term =
 466           match term with
 467           | C.Prod (name, s, t) ->
 468 (*               let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
 469               let (head, newmetas, args, _) =
 470                 PrimitiveTactics.new_metasenv_for_apply newmeta proof
 471                   context (S.lift index term)
 472               in
 473               let newmeta =
 474                 List.fold_left
 475                   (fun maxm arg ->
 476                      match arg with
 477                      | C.Meta (i, _) -> (max maxm i)
 478                      | _ -> assert false)
 479                   newmeta args
 480               in
 481               let p =
 482                 if List.length args = 0 then
 483                   C.Rel index
 484                 else
 485                   C.Appl ((C.Rel index)::args)
 486               in (
 487                 match head with
 488                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
 489                     Printf.printf "OK: %s\n" (CicPp.ppterm term);
 490                     Some (p, (ty, t1, t2), newmetas, args), (newmeta+1)
 491                 | _ -> None, newmeta
 492               )
 493           | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
 494               Some (C.Rel index,
 495                     (ty, S.lift index t1, S.lift index t2), [], []), (newmeta+1)
 496           | _ -> None, newmeta
 497         in (
 498           match do_find context term with
 499           | Some p, newmeta ->
 500               let tl, newmeta' = (aux (index+1) newmeta tl) in
 501               p::tl, max newmeta newmeta'
 502           | None, _ ->
 503               aux (index+1) newmeta tl
 504         )
 505     | _::tl ->
 506         aux (index+1) newmeta tl
 507   in
 508   aux 1 newmeta context
 509 ;;
 510
 511
 512 let fix_metas newmeta ((proof, (ty, left, right), menv, args) as equality) =
 513   let newargs, _ =
 514     List.fold_right
 515       (fun t (newargs, index) ->
 516          match t with
 517          | Cic.Meta (i, l) -> ((Cic.Meta (index, l))::newargs, index+1)
 518          | _ -> assert false)
 519       args ([], newmeta)
 520   in
 521   let repl where =
 522     ProofEngineReduction.replace ~equality:(=) ~what:args ~with_what:newargs
 523       ~where
 524   in
 525   let menv', _ =
 526     List.fold_right
 527       (fun (i, context, term) (menv, index) ->
 528          ((index, context, term)::menv, index+1))
 529       menv ([], newmeta)
 530   in
 531   (newmeta + (List.length newargs) + 1,
 532    (repl proof, (repl ty, repl left, repl right), menv', newargs))
 533 ;;
 534
 535
 536 exception TermIsNotAnEquality;;
 537
 538 let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
 539   | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
 540       (proof, (ty, t1, t2), [], [])
 541   | _ ->
 542       raise TermIsNotAnEquality
 543 ;;
 544
 545
 546 type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;;
 547
 548
 549 let superposition_left (metasenv, context, ugraph) target source =
 550   let module C = Cic in
 551   let module S = CicSubstitution in
 552   let module M = CicMetaSubst in
 553   let module HL = HelmLibraryObjects in
 554   let module CR = CicReduction in
 555   (* we assume that target is ground (does not contain metavariables): this
 556    * should always be the case (I hope, at least) *)
 557   let proof, (eq_ty, left, right), _, _ = target in
 558   let eqproof, (ty, t1, t2), newmetas, args = source in
 559
 560   (* ALB: TODO check that ty and eq_ty are indeed equal... *)
 561   assert (eq_ty = ty);
 562
 563   let where, is_left =
 564     match nonrec_kbo left right with
 565     | Lt -> right, false
 566     | Gt -> left, true
 567     | _ -> (
 568         Printf.printf "????????? %s = %s" (CicPp.ppterm left)
 569           (CicPp.ppterm right);
 570         print_newline ();
 571         assert false (* again, for ground terms this shouldn't happen... *)
 572       )
 573   in
 574   let metasenv' = newmetas @ metasenv in
 575   let res1 =
 576     List.filter
 577       (fun (t, s, m, ug) ->
 578          nonrec_kbo (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
 579       (beta_expand t1 ty where context metasenv' ugraph)
 580   and res2 =
 581     List.filter
 582       (fun (t, s, m, ug) ->
 583          nonrec_kbo (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
 584       (beta_expand t2 ty where context metasenv' ugraph)
 585   in
 586 (*   let what, other = *)
 587 (*     if is_left then left, right *)
 588 (*     else right, left *)
 589 (*   in *)
 590   let build_new what other eq_URI (t, s, m, ug) =
 591     let newgoal, newgoalproof =
 592       match t with
 593       | C.Lambda (nn, ty, bo) ->
 594           let bo' = S.subst (M.apply_subst s other) bo in
 595           let bo'' =
 596             C.Appl (
 597               [C.MutInd (HL.Logic.eq_URI, 0, []);
 598                S.lift 1 eq_ty] @
 599                 if is_left then [bo'; S.lift 1 right] else [S.lift 1 left; bo'])
 600           in
 601           let t' = C.Lambda (nn, ty, bo'') in
 602           S.subst (M.apply_subst s other) bo,
 603           M.apply_subst s
 604             (C.Appl [C.Const (eq_URI, []); ty; what; t';
 605                      proof; other; eqproof])
 606       | _ -> assert false
 607     in
 608     let equation =
 609       if is_left then (eq_ty, newgoal, right)
 610       else (eq_ty, left, newgoal)
 611     in
 612     (eqproof, equation, [], [])
 613   in
 614   let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1
 615   and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in
 616   new1 @ new2
 617 ;;
 618
 619
 620 let superposition_right newmeta (metasenv, context, ugraph) target source =
 621   let module C = Cic in
 622   let module S = CicSubstitution in
 623   let module M = CicMetaSubst in
 624   let module HL = HelmLibraryObjects in
 625   let module CR = CicReduction in
 626   let eqproof, (eq_ty, left, right), newmetas, args = target in
 627   let eqp', (ty', t1, t2), newm', args' = source in
 628   let maxmeta = ref newmeta in
 629
 630   (* TODO check if ty and ty' are equal... *)
 631   assert (eq_ty = ty');
 632
 633 (*   let ok term subst other other_eq_side ugraph = *)
 634 (*     match term with *)
 635 (*     | C.Lambda (nn, ty, bo) -> *)
 636 (*         let bo' = S.subst (M.apply_subst subst other) bo in *)
 637 (*         let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *)
 638 (*         not res *)
 639 (*     |  _ -> assert false *)
 640 (*   in *)
 641   let condition left right what other (t, s, m, ug) =
 642     let subst = M.apply_subst s in
 643     let cmp1 = nonrec_kbo (subst what) (subst other) in
 644     let cmp2 = nonrec_kbo (subst left) (subst right) in
 645 (*     cmp1 = Gt && cmp2 = Gt *)
 646     cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
 647 (*     && (ok t s other right ug) *)
 648   in
 649   let metasenv' = metasenv @ newmetas @ newm' in
 650   let beta_expand = beta_expand ~metas_ok:false in
 651   let res1 =
 652     List.filter
 653       (condition left right t1 t2)
 654       (beta_expand t1 eq_ty left context metasenv' ugraph)
 655   and res2 =
 656     List.filter
 657       (condition left right t2 t1)
 658       (beta_expand t2 eq_ty left context metasenv' ugraph)
 659   and res3 =
 660     List.filter
 661       (condition right left t1 t2)
 662       (beta_expand t1 eq_ty right context metasenv' ugraph)
 663   and res4 =
 664     List.filter
 665       (condition right left t2 t1)
 666       (beta_expand t2 eq_ty right context metasenv' ugraph)
 667   in
 668   let newmetas = newmetas @ newm' in
 669   let newargs = args @ args' in
 670   let build_new what other is_left eq_URI (t, s, m, ug) =
 671 (*     let what, other = *)
 672 (*       if is_left then left, right *)
 673 (*       else right, left *)
 674 (*     in *)
 675     let newterm, neweqproof =
 676       match t with
 677       | C.Lambda (nn, ty, bo) ->
 678           let bo' = M.apply_subst s (S.subst other bo) in
 679           let bo'' =
 680             C.Appl (
 681               [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @
 682                 if is_left then [bo'; S.lift 1 right] else [S.lift 1 left; bo'])
 683           in
 684           let t' = C.Lambda (nn, ty, bo'') in
 685           bo',
 686           M.apply_subst s
 687             (C.Appl [C.Const (eq_URI, []); ty; what; t'; eqproof; other; eqp'])
 688       | _ -> assert false
 689     in
 690     let newmeta, newequality =
 691       let left, right =
 692         if is_left then (newterm, M.apply_subst s right)
 693         else (M.apply_subst s left, newterm) in
 694       fix_metas !maxmeta
 695         (neweqproof, (eq_ty, left, right), newmetas, newargs)
 696     in
 697     maxmeta := newmeta;
 698     newequality
 699   in
 700   let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
 701   and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
 702   and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
 703   and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
 704   let ok = function
 705     | _, (_, left, right), _, _ ->
 706         not (fst (CR.are_convertible context left right ugraph))
 707   in
 708   !maxmeta, (List.filter ok (new1 @ new2 @ new3 @ new4))
 709 ;;
 710
 711
 712 let demodulation newmeta (metasenv, context, ugraph) target source =
 713   let module C = Cic in
 714   let module S = CicSubstitution in
 715   let module M = CicMetaSubst in
 716   let module HL = HelmLibraryObjects in
 717   let module CR = CicReduction in
 718
 719   let proof, (eq_ty, left, right), metas, args = target
 720   and proof', (ty, t1, t2), metas', args' = source in
 721   if eq_ty <> ty then
 722     newmeta, target
 723   else
 724     let get_params step =
 725       match step with
 726       | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
 727       | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
 728       | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
 729       | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
 730       | _ -> assert false
 731     in
 732     let rec demodulate newmeta step metasenv target =
 733       let proof, (eq_ty, left, right), metas, args = target in
 734       let is_left, what, other, eq_URI = get_params step in
 735 (*       Printf.printf *)
 736 (*         "demodulate\ntarget: %s = %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
 737 (*         (CicPp.ppterm left) (CicPp.ppterm right) (CicPp.ppterm what) *)
 738 (*         (CicPp.ppterm other) (string_of_bool is_left); *)
 739 (*       Printf.printf "step: %d\n" step; *)
 740 (*       print_newline (); *)
 741       let ok (t, s, m, ug) =
 742         nonrec_kbo (M.apply_subst s what) (M.apply_subst s other) = Gt
 743       in
 744       let res =
 745         List.filter ok
 746           (beta_expand ~metas_ok:false ~match_only:true
 747              what ty left context (metasenv @ metas) ugraph)
 748       in
 749       match res with
 750       | [] ->
 751           if step = 0 then newmeta, target
 752           else demodulate newmeta (step-1) metasenv target
 753       | (t, s, m, ug)::_ ->
 754           let newterm, newproof =
 755             match t with
 756             | C.Lambda (nn, ty, bo) ->
 757                 let bo' = M.apply_subst s (S.subst other bo) in
 758                 let bo'' =
 759                   C.Appl (
 760                     [C.MutInd (HL.Logic.eq_URI, 0, []);
 761                      S.lift 1 eq_ty] @
 762                       if is_left then [bo'; S.lift 1 right]
 763                       else [S.lift 1 left; bo'])
 764                 in
 765                 let t' = C.Lambda (nn, ty, bo'') in
 766                 M.apply_subst s (S.subst other bo),
 767                 M.apply_subst s
 768                   (C.Appl [C.Const (eq_URI, []); ty; what; t';
 769                            proof; other; proof'])
 770             | _ -> assert false
 771           in
 772           let newmeta, newtarget =
 773             let left, right =
 774               if is_left then (newterm, M.apply_subst s right)
 775               else (M.apply_subst s left, newterm) in
 776             let newmetasenv = metasenv @ metas in
 777             let newargs = args @ args' in
 778             fix_metas newmeta
 779               (newproof, (eq_ty, left, right), newmetasenv, newargs)
 780           in
 781           let _, (_, left, right), _, _ = newtarget
 782           and _, (_, oldleft, oldright), _, _ = target in
 783 (*           Printf.printf *)
 784 (*             "demodulate, newtarget: %s = %s\ntarget was: %s = %s\n" *)
 785 (*             (CicPp.ppterm left) (CicPp.ppterm right) *)
 786 (*             (CicPp.ppterm oldleft) (CicPp.ppterm oldright); *)
 787 (*           print_newline (); *)
 788           demodulate newmeta step metasenv newtarget
 789     in
 790     demodulate newmeta 3 (metasenv @ metas') target
 791 ;;
 792
 793
 794 (*
 795 let demodulation newmeta env target source =
 796   newmeta, target
 797 ;;
 798 *)
 799
 800