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