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