helm/ocaml/paramodulation/inference.ml

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