helm/software/components/ng_refiner/nCicUnification.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id$ *)
  13
  14 exception UnificationFailure of string Lazy.t;;
  15 exception Uncertain of string Lazy.t;;
  16 exception AssertFailure of string Lazy.t;;
  17
  18 let (===) x y = Pervasives.compare x y = 0 ;;
  19
  20 let fail_exc metasenv subst context t1 t2 =
  21   UnificationFailure (lazy (
  22   "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^
  23   " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2))
  24 ;;
  25
  26 let unify metasenv subst context t1 t2 =
  27  (* are_convertible?? *)
  28  let rec aux test_eq_only metasenv subst context t1 t2 =
  29    let fo_unif test_eq_only t1 t2 =
  30      if t1 === t2 then
  31        metasenv, subst
  32      else
  33        match (t1,t2) with
  34        | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
  35            if NCicEnvironment.universe_leq a b then metasenv, subst
  36            else raise (fail_exc metasenv subst context t1 t2)
  37        | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
  38            if NCicEnvironment.universe_eq a b then metasenv, subst
  39            else raise (fail_exc metasenv subst context t1 t2)
  40        | (C.Sort C.Prop,C.Sort (C.Type _)) ->
  41            if (not test_eq_only) then metasenv, subst
  42            else raise (fail_exc metasenv subst context t1 t2)
  43
  44        | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
  45        | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
  46            let metasenv, subst = aux true metasenv subst context s1 s2 in
  47            aux test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
  48        | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
  49            let metasenv,subst=aux test_eq_only metasenv subst context ty1 ty2 in
  50            let metasenv,subst=aux test_eq_only metasenv subst context s1 s2 in
  51            let context = (name1, C.Def (s1,ty1))::context in
  52            aux test_eq_only metasenv subst context t1 t2
  53
  54        | (C.Meta (n1,(s1, C.Irl _)), C.Meta (n2,(s2, C.Irl _)))
  55           when n1 = n2 && s1 = s2 -> true
  56        | (C.Meta (n1,(s1, l1)), C.Meta (n2,(s2, l2))) when n1 = n2 &&
  57           let l1 = NCicUtils.expand_local_context l1 in
  58           let l2 = NCicUtils.expand_local_context l2 in
  59           (try List.for_all2
  60             (fun t1 t2 -> aux test_eq_only context
  61               (NCicSubstitution.lift s1 t1)
  62               (NCicSubstitution.lift s2 t2))
  63             l1 l2
  64           with Invalid_argument _ -> assert false) -> true
  65
  66        | C.Meta (n1,l1), _ ->
  67           (try
  68              let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
  69              let term = NCicSubstitution.subst_meta l1 term in
  70               aux test_eq_only context term t2
  71            with NCicUtils.Subst_not_found _ -> false)
  72        | _, C.Meta (n2,l2) ->
  73           (try
  74              let _,_,term,_ = NCicUtils.lookup_subst n2 subst in
  75              let term = NCicSubstitution.subst_meta l2 term in
  76               aux test_eq_only context t1 term
  77            with NCicUtils.Subst_not_found _ -> false)
  78
  79        | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
  80            when (Ref.eq r1 r2 &&
  81              List.length (E.get_relevance r1) >= List.length tl1) ->
  82          let relevance = E.get_relevance r1 in
  83          let relevance = match r1 with
  84              | Ref.Ref (_,Ref.Con (_,_,lno)) ->
  85                  let _,relevance = HExtlib.split_nth lno relevance in
  86                    HExtlib.mk_list false lno @ relevance
  87              | _ -> relevance
  88          in
  89          let fail = ref ~-1 in
  90          let res = (try
  91              HExtlib.list_forall_default3
  92               (fun t1 t2 b -> fail := !fail+1; not b || aux test_eq_only context t1 t2)
  93               tl1 tl2 true relevance
  94             with Invalid_argument _ -> false)
  95          in res
  96          (* if res then true
  97          else
  98            let relevance = get_relevance_p ~subst context _hd1 tl1 in
  99            let _,relevance = HExtlib.split_nth !fail relevance in
 100            let b,relevance = (match relevance with
 101              | [] -> assert false
 102              | b::tl -> b,tl) in
 103            let _,tl1 = HExtlib.split_nth (!fail+1) tl1 in
 104            let _,tl2 = HExtlib.split_nth (!fail+1) tl2 in
 105            if (not b) then
 106              (dance ();
 107               try
 108                HExtlib.list_forall_default3
 109                 (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)
 110                 tl1 tl2 true relevance
 111              with Invalid_argument _ -> false)
 112            else false *)
 113        | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) ->
 114            aux test_eq_only context hd1 hd2 &&
 115            let relevance = get_relevance ~subst context hd1 tl1 in
 116            (try
 117              HExtlib.list_forall_default3
 118               (fun t1 t2 b -> not b || aux test_eq_only context t1 t2)
 119               tl1 tl2 true relevance
 120             with Invalid_argument _ -> false)
 121
 122        | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
 123           C.Match (ref2,outtype2,term2,pl2)) ->
 124            let _,_,itl,_,_ = E.get_checked_indtys ref1 in
 125            let _,_,ty,_ = List.nth itl tyno in
 126            let rec remove_prods ~subst context ty =
 127              let ty = whd ~subst context ty in
 128              match ty with
 129              | C.Sort _ -> ty
 130              | C.Prod (name,so,ta) ->
 131                    remove_prods ~subst ((name,(C.Decl so))::context) ta
 132              | _ -> assert false
 133            in
 134            let is_prop =
 135              match remove_prods ~subst [] ty with
 136              | C.Sort C.Prop -> true
 137            let rec remove_prods ~subst context ty =
 138              let ty = whd ~subst context ty in
 139              match ty with
 140              | C.Sort _ -> ty
 141              | C.Prod (name,so,ta) ->
 142                    remove_prods ~subst ((name,(C.Decl so))::context) ta
 143              | _ -> assert false
 144            in
 145            if not (Ref.eq ref1 ref2) then
 146              raise (uncert_exc metasenv subst context t1 t2)
 147            else
 148              let metasenv, subst =
 149                aux test_eq_only metasenv subst context outtype1 outtype2 in
 150              let metasenv, subst =
 151                try aux test_eq_only metasenv subst context term1 term2
 152                with UnificationFailure _ | Uncertain _ when is_prop ->
 153                  metasenv, subst
 154              in
 155              try
 156               List.fold_left2
 157                (fun (metasenv,subst) -> aux test_eq_only metasenv subst context)
 158                (metasenv, subst) pl1 pl2
 159              with Invalid_argument _ ->
 160                raise (uncert_exc metasenv subst context t1 t2)
 161        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
 162        | _ -> raise (uncert_exc metasenv subst context t1 t2)
 163     in
 164     let unif_machines ...
 165
 166     in
 167      try fo_unif
 168      with Uncertain msg as exn ->
 169        try unif_machines
 170        with
 171        | UnificationFailure _ -> raise (UnificationFailure msg)
 172        | Uncertain _ -> raise exn
 173  in
 174   aux false metasenv subst context t1 t2
 175
 176 let are_convertible ?(subst=[]) get_relevance =
 177  let rec aux test_eq_only metasenv subst context t1 t2 =
 178   in
 179    if alpha_eq test_eq_only t1 t2 then
 180      true
 181    else
 182      let height_of = function
 183       | C.Const (Ref.Ref (_,Ref.Def h))
 184       | C.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
 185       | C.Appl(C.Const(Ref.Ref(_,Ref.Def h))::_)
 186       | C.Appl(C.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
 187       | _ -> 0
 188      in
 189      let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
 190        let h1 = height_of t1 in
 191        let h2 = height_of t2 in
 192        let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
 193        R.reduce ~delta ~subst context m1,
 194        R.reduce ~delta ~subst context m2,
 195        delta
 196      in
 197      let rec convert_machines ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) =
 198        (alpha_eq test_eq_only
 199          (R.unwind (k1,e1,t1,[])) (R.unwind (k2,e2,t2,[])) &&
 200         let relevance =
 201           match t1 with
 202               C.Const r -> NCicEnvironment.get_relevance r
 203             | _ -> [] in
 204         try
 205          HExtlib.list_forall_default3
 206            (fun t1 t2 b  ->
 207              not b ||
 208              let t1 = RS.from_stack t1 in
 209              let t2 = RS.from_stack t2 in
 210              convert_machines (small_delta_step t1 t2)) s1 s2 true relevance
 211         with Invalid_argument _ -> false) ||
 212        (delta > 0 &&
 213           let delta = delta - 1 in
 214           let red = R.reduce ~delta ~subst context in
 215           convert_machines (red m1,red m2,delta))
 216      in
 217      convert_machines (small_delta_step (0,[],t1,[]) (0,[],t2,[]))
 218  in
 219   aux false
 220 ;;
 221
 222
 223
 224 (*
 225
 226 open Printf
 227
 228 exception UnificationFailure of string Lazy.t;;
 229 exception Uncertain of string Lazy.t;;
 230 exception AssertFailure of string Lazy.t;;
 231
 232 let verbose = false;;
 233 let debug_print = fun _ -> ()
 234
 235 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
 236 let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
 237 let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
 238 let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
 239
 240 let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
 241
 242 let type_of_aux' metasenv subst context term ugraph =
 243 let foo () =
 244   try
 245     profile.HExtlib.profile
 246       (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
 247   with
 248       CicTypeChecker.TypeCheckerFailure msg ->
 249         let msg =
 250          lazy
 251           (sprintf
 252            "Kernel Type checking error:
 253 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
 254              (CicMetaSubst.ppterm ~metasenv subst term)
 255              (CicMetaSubst.ppterm ~metasenv [] term)
 256              (CicMetaSubst.ppcontext ~metasenv subst context)
 257              (CicMetaSubst.ppmetasenv subst metasenv)
 258              (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
 259         raise (AssertFailure msg)
 260     | CicTypeChecker.AssertFailure msg ->
 261         let msg = lazy
 262          (sprintf
 263            "Kernel Type checking assertion failure:
 264 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
 265              (CicMetaSubst.ppterm ~metasenv subst term)
 266              (CicMetaSubst.ppterm ~metasenv [] term)
 267              (CicMetaSubst.ppcontext ~metasenv subst context)
 268              (CicMetaSubst.ppmetasenv subst metasenv)
 269              (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
 270         raise (AssertFailure msg)
 271 in profiler_toa.HExtlib.profile foo ()
 272 ;;
 273
 274 let exists_a_meta l =
 275   List.exists
 276     (function
 277        | Cic.Meta _
 278        | Cic.Appl (Cic.Meta _::_) -> true
 279        | _ -> false) l
 280
 281 let rec deref subst t =
 282   let snd (_,a,_) = a in
 283   match t with
 284       Cic.Meta(n,l) ->
 285         (try
 286            deref subst
 287              (CicSubstitution.subst_meta
 288                 l (snd (CicUtil.lookup_subst n subst)))
 289          with
 290              CicUtil.Subst_not_found _ -> t)
 291     | Cic.Appl(Cic.Meta(n,l)::args) ->
 292         (match deref subst (Cic.Meta(n,l)) with
 293            | Cic.Lambda _ as t ->
 294                deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
 295            | r -> Cic.Appl(r::args))
 296     | Cic.Appl(((Cic.Lambda _) as t)::args) ->
 297            deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
 298     | t -> t
 299 ;;
 300
 301 let deref subst t =
 302  let foo () = deref subst t
 303  in profiler_deref.HExtlib.profile foo ()
 304
 305 exception WrongShape;;
 306 let eta_reduce after_beta_expansion after_beta_expansion_body
 307      before_beta_expansion
 308  =
 309  try
 310   match before_beta_expansion,after_beta_expansion_body with
 311      Cic.Appl l, Cic.Appl l' ->
 312       let rec all_but_last check_last =
 313        function
 314           [] -> assert false
 315         | [Cic.Rel 1] -> []
 316         | [_] -> if check_last then raise WrongShape else []
 317         | he::tl -> he::(all_but_last check_last tl)
 318       in
 319        let all_but_last check_last l =
 320         match all_but_last check_last l with
 321            [] -> assert false
 322          | [he] -> he
 323          | l -> Cic.Appl l
 324        in
 325        let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
 326        let all_but_last = all_but_last false l in
 327         (* here we should test alpha-equivalence; however we know by
 328            construction that here alpha_equivalence is equivalent to = *)
 329         if t = all_but_last then
 330          all_but_last
 331         else
 332          after_beta_expansion
 333    | _,_ -> after_beta_expansion
 334  with
 335   WrongShape -> after_beta_expansion
 336
 337 let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
 338  let module S = CicSubstitution in
 339  let module C = Cic in
 340 let foo () =
 341   let rec aux metasenv subst n context t' ugraph =
 342    try
 343
 344     let subst,metasenv,ugraph1 =
 345      fo_unif_subst test_equality_only subst context metasenv
 346       (CicSubstitution.lift n arg) t' ugraph
 347
 348     in
 349      subst,metasenv,C.Rel (1 + n),ugraph1
 350    with
 351       Uncertain _
 352     | UnificationFailure _ ->
 353        match t' with
 354         | C.Rel m  -> subst,metasenv,
 355            (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
 356         | C.Var (uri,exp_named_subst) ->
 357            let subst,metasenv,exp_named_subst',ugraph1 =
 358             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
 359            in
 360             subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
 361         | C.Meta (i,l) ->
 362             (* andrea: in general, beta_expand can create badly typed
 363              terms. This happens quite seldom in practice, UNLESS we
 364              iterate on the local context. For this reason, we renounce
 365              to iterate and just lift *)
 366             let l =
 367               List.map
 368                 (function
 369                      Some t -> Some (CicSubstitution.lift 1 t)
 370                    | None -> None) l in
 371             subst, metasenv, C.Meta (i,l), ugraph
 372         | C.Sort _
 373         | C.Implicit _ as t -> subst,metasenv,t,ugraph
 374         | C.Cast (te,ty) ->
 375             let subst,metasenv,te',ugraph1 =
 376               aux metasenv subst n context te ugraph in
 377             let subst,metasenv,ty',ugraph2 =
 378               aux metasenv subst n context ty ugraph1 in
 379             (* TASSI: sure this is in serial? *)
 380             subst,metasenv,(C.Cast (te', ty')),ugraph2
 381         | C.Prod (nn,s,t) ->
 382            let subst,metasenv,s',ugraph1 =
 383              aux metasenv subst n context s ugraph in
 384            let subst,metasenv,t',ugraph2 =
 385              aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
 386                ugraph1
 387            in
 388            (* TASSI: sure this is in serial? *)
 389            subst,metasenv,(C.Prod (nn, s', t')),ugraph2
 390         | C.Lambda (nn,s,t) ->
 391            let subst,metasenv,s',ugraph1 =
 392              aux metasenv subst n context s ugraph in
 393            let subst,metasenv,t',ugraph2 =
 394             aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
 395            in
 396            (* TASSI: sure this is in serial? *)
 397             subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
 398         | C.LetIn (nn,s,ty,t) ->
 399            let subst,metasenv,s',ugraph1 =
 400              aux metasenv subst n context s ugraph in
 401            let subst,metasenv,ty',ugraph1 =
 402              aux metasenv subst n context ty ugraph in
 403            let subst,metasenv,t',ugraph2 =
 404             aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
 405               ugraph1
 406            in
 407            (* TASSI: sure this is in serial? *)
 408             subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
 409         | C.Appl l ->
 410            let subst,metasenv,revl',ugraph1 =
 411             List.fold_left
 412              (fun (subst,metasenv,appl,ugraph) t ->
 413                let subst,metasenv,t',ugraph1 =
 414                  aux metasenv subst n context t ugraph in
 415                 subst,metasenv,(t'::appl),ugraph1
 416              ) (subst,metasenv,[],ugraph) l
 417            in
 418             subst,metasenv,(C.Appl (List.rev revl')),ugraph1
 419         | C.Const (uri,exp_named_subst) ->
 420            let subst,metasenv,exp_named_subst',ugraph1 =
 421             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
 422            in
 423             subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
 424         | C.MutInd (uri,i,exp_named_subst) ->
 425            let subst,metasenv,exp_named_subst',ugraph1 =
 426             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
 427            in
 428             subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
 429         | C.MutConstruct (uri,i,j,exp_named_subst) ->
 430            let subst,metasenv,exp_named_subst',ugraph1 =
 431             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
 432            in
 433             subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
 434         | C.MutCase (sp,i,outt,t,pl) ->
 435            let subst,metasenv,outt',ugraph1 =
 436              aux metasenv subst n context outt ugraph in
 437            let subst,metasenv,t',ugraph2 =
 438              aux metasenv subst n context t ugraph1 in
 439            let subst,metasenv,revpl',ugraph3 =
 440             List.fold_left
 441              (fun (subst,metasenv,pl,ugraph) t ->
 442                let subst,metasenv,t',ugraph1 =
 443                  aux metasenv subst n context t ugraph in
 444                subst,metasenv,(t'::pl),ugraph1
 445              ) (subst,metasenv,[],ugraph2) pl
 446            in
 447            subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
 448            (* TASSI: not sure this is serial *)
 449         | C.Fix (i,fl) ->
 450 (*CSC: not implemented
 451            let tylen = List.length fl in
 452             let substitutedfl =
 453              List.map
 454               (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
 455                fl
 456             in
 457              C.Fix (i, substitutedfl)
 458 *)
 459             subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
 460         | C.CoFix (i,fl) ->
 461 (*CSC: not implemented
 462            let tylen = List.length fl in
 463             let substitutedfl =
 464              List.map
 465               (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
 466                fl
 467             in
 468              C.CoFix (i, substitutedfl)
 469
 470 *)
 471             subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
 472
 473   and aux_exp_named_subst metasenv subst n context ens ugraph =
 474    List.fold_right
 475     (fun (uri,t) (subst,metasenv,l,ugraph) ->
 476       let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
 477        subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
 478   in
 479   let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
 480   let fresh_name =
 481    FreshNamesGenerator.mk_fresh_name ~subst
 482     metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
 483   in
 484    let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
 485    let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
 486    subst, metasenv, t'', ugraph2
 487 in profiler_beta_expand.HExtlib.profile foo ()
 488
 489
 490 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
 491   let _,subst,metasenv,hd,ugraph =
 492     List.fold_right
 493       (fun arg (num,subst,metasenv,t,ugraph) ->
 494          let subst,metasenv,t,ugraph1 =
 495            beta_expand num test_equality_only
 496              metasenv subst context t arg ugraph
 497          in
 498            num+1,subst,metasenv,t,ugraph1
 499       ) args (1,subst,metasenv,t,ugraph)
 500   in
 501     subst,metasenv,hd,ugraph
 502
 503 and warn_if_not_unique xxx to1 to2 carr car1 car2 =
 504   match xxx with
 505   | [] -> ()
 506   | (m2,_,c2,c2')::_ ->
 507      let m1,c1,c1' = carr,to1,to2 in
 508      let unopt =
 509        function Some (_,t) -> CicPp.ppterm t
 510        | None -> "id"
 511      in
 512      HLog.warn
 513        ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^
 514        CoercDb.string_of_carr car2^": " ^
 515        CoercDb.string_of_carr m1^" via "^unopt c1^" + "^
 516        unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^
 517        unopt c2^" + "^unopt c2')
 518
 519 (* NUOVA UNIFICAZIONE *)
 520 (* A substitution is a (int * Cic.term) list that associates a
 521    metavariable i with its body.
 522    A metaenv is a (int * Cic.term) list that associate a metavariable
 523    i with is type.
 524    fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
 525    a new substitution which is _NOT_ unwinded. It must be unwinded before
 526    applying it. *)
 527
 528 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
 529  let module C = Cic in
 530  let module R = CicReduction in
 531  let module S = CicSubstitution in
 532  let t1 = deref subst t1 in
 533  let t2 = deref subst t2 in
 534  let (&&&) a b = (a && b) || ((not a) && (not b)) in
 535 (* let bef = Sys.time () in *)
 536  let b,ugraph =
 537   if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
 538    false,ugraph
 539   else
 540 let foo () =
 541    R.are_convertible ~subst ~metasenv context t1 t2 ugraph
 542 in profiler_are_convertible.HExtlib.profile foo ()
 543  in
 544 (* let aft = Sys.time () in
 545 if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^
 546 CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^
 547 CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
 548    if b then
 549      subst, metasenv, ugraph
 550    else
 551    match (t1, t2) with
 552      | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
 553          let _,subst,metasenv,ugraph1 =
 554            (try
 555               List.fold_left2
 556                 (fun (j,subst,metasenv,ugraph) t1 t2 ->
 557                    match t1,t2 with
 558                        None,_
 559                      | _,None -> j+1,subst,metasenv,ugraph
 560                      | Some t1', Some t2' ->
 561                          (* First possibility:  restriction    *)
 562                          (* Second possibility: unification    *)
 563                          (* Third possibility:  convertibility *)
 564                          let b, ugraph1 =
 565                          R.are_convertible
 566                            ~subst ~metasenv context t1' t2' ugraph
 567                          in
 568                          if b then
 569                            j+1,subst,metasenv, ugraph1
 570                          else
 571                            (try
 572                               let subst,metasenv,ugraph2 =
 573                                 fo_unif_subst
 574                                   test_equality_only
 575                                   subst context metasenv t1' t2' ugraph
 576                               in
 577                                 j+1,subst,metasenv,ugraph2
 578                             with
 579                                 Uncertain _
 580                               | UnificationFailure _ ->
 581 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
 582                                   let metasenv, subst =
 583                                     CicMetaSubst.restrict
 584                                       subst [(n,j)] metasenv in
 585                                     j+1,subst,metasenv,ugraph1)
 586                 ) (1,subst,metasenv,ugraph) ln lm
 587             with
 588                 Exit ->
 589                   raise
 590                     (UnificationFailure (lazy "1"))
 591                     (*
 592                     (sprintf
 593                       "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
 594                       (CicMetaSubst.ppterm ~metasenv subst t1)
 595                       (CicMetaSubst.ppterm ~metasenv subst t2))) *)
 596               | Invalid_argument _ ->
 597                   raise
 598                     (UnificationFailure (lazy "2")))
 599                     (*
 600                     (sprintf
 601                       "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
 602                       (CicMetaSubst.ppterm ~metasenv subst t1)
 603                       (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
 604          in subst,metasenv,ugraph1
 605      | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
 606          fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
 607      | (C.Meta (n,l), t)
 608      | (t, C.Meta (n,l)) ->
 609          let swap =
 610            match t1,t2 with
 611                C.Meta (n,_), C.Meta (m,_) when n < m -> false
 612              | _, C.Meta _ -> false
 613              | _,_ -> true
 614          in
 615          let lower = fun x y -> if swap then y else x in
 616          let upper = fun x y -> if swap then x else y in
 617          let fo_unif_subst_ordered
 618              test_equality_only subst context metasenv m1 m2 ugraph =
 619            fo_unif_subst test_equality_only subst context metasenv
 620              (lower m1 m2) (upper m1 m2) ugraph
 621          in
 622          begin
 623          let subst,metasenv,ugraph1 =
 624            let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv in
 625            (try
 626               let tyt,ugraph1 =
 627                 type_of_aux' metasenv subst context t ugraph
 628               in
 629                 fo_unif_subst
 630                   test_equality_only
 631                   subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
 632             with
 633                 UnificationFailure _ as e -> raise e
 634               | Uncertain msg -> raise (UnificationFailure msg)
 635               | AssertFailure _ ->
 636                   debug_print (lazy "siamo allo huge hack");
 637                   (* TODO huge hack!!!!
 638                    * we keep on unifying/refining in the hope that
 639                    * the problem will be eventually solved.
 640                    * In the meantime we're breaking a big invariant:
 641                    * the terms that we are unifying are no longer well
 642                    * typed in the current context (in the worst case
 643                    * we could even diverge) *)
 644                   (subst, metasenv,ugraph)) in
 645          let t',metasenv,subst =
 646            try
 647              CicMetaSubst.delift n subst context metasenv l t
 648            with
 649                (CicMetaSubst.MetaSubstFailure msg)->
 650                  raise (UnificationFailure msg)
 651              | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
 652          in
 653          let t'',ugraph2 =
 654            match t' with
 655                C.Sort (C.Type u) when not test_equality_only ->
 656                  let u' = CicUniv.fresh () in
 657                  let s = C.Sort (C.Type u') in
 658                   (try
 659                     let ugraph2 =
 660                      CicUniv.add_ge (upper u u') (lower u u') ugraph1
 661                     in
 662                      s,ugraph2
 663                    with
 664                     CicUniv.UniverseInconsistency msg ->
 665                      raise (UnificationFailure msg))
 666              | _ -> t',ugraph1
 667          in
 668          (* Unifying the types may have already instantiated n. Let's check *)
 669          try
 670            let (_, oldt,_) = CicUtil.lookup_subst n subst in
 671            let lifted_oldt = S.subst_meta l oldt in
 672              fo_unif_subst_ordered
 673                test_equality_only subst context metasenv t lifted_oldt ugraph2
 674          with
 675              CicUtil.Subst_not_found _ ->
 676                let (_, context, ty) = CicUtil.lookup_meta n metasenv in
 677                let subst = (n, (context, t'',ty)) :: subst in
 678                let metasenv =
 679                  List.filter (fun (m,_,_) -> not (n = m)) metasenv in
 680                subst, metasenv, ugraph2
 681          end
 682    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
 683    | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
 684       if UriManager.eq uri1 uri2 then
 685        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 686         exp_named_subst1 exp_named_subst2 ugraph
 687       else
 688        raise (UnificationFailure (lazy
 689           (sprintf
 690             "Can't unify %s with %s due to different constants"
 691             (CicMetaSubst.ppterm ~metasenv subst t1)
 692             (CicMetaSubst.ppterm ~metasenv subst t2))))
 693    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
 694        if UriManager.eq uri1 uri2 && i1 = i2 then
 695          fo_unif_subst_exp_named_subst
 696            test_equality_only
 697            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
 698        else
 699          raise (UnificationFailure
 700            (lazy
 701             (sprintf
 702              "Can't unify %s with %s due to different inductive principles"
 703              (CicMetaSubst.ppterm ~metasenv subst t1)
 704              (CicMetaSubst.ppterm ~metasenv subst t2))))
 705    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
 706        C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
 707        if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
 708          fo_unif_subst_exp_named_subst
 709            test_equality_only
 710            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
 711        else
 712          raise (UnificationFailure
 713           (lazy
 714             (sprintf
 715               "Can't unify %s with %s due to different inductive constructors"
 716               (CicMetaSubst.ppterm ~metasenv subst t1)
 717               (CicMetaSubst.ppterm ~metasenv subst t2))))
 718    | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
 719    | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
 720                               subst context metasenv te t2 ugraph
 721    | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
 722                               subst context metasenv t1 te ugraph
 723    | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
 724        let subst',metasenv',ugraph1 =
 725          fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
 726        in
 727          fo_unif_subst test_equality_only
 728            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
 729    | (C.LetIn (_,s1,ty1,t1), t2)
 730    | (t2, C.LetIn (_,s1,ty1,t1)) ->
 731        fo_unif_subst
 732         test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
 733    | (C.Appl l1, C.Appl l2) ->
 734        (* andrea: this case should be probably rewritten in the
 735           spirit of deref *)
 736        (match l1,l2 with
 737           | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
 738               (try
 739                  List.fold_left2
 740                    (fun (subst,metasenv,ugraph) t1 t2 ->
 741                       fo_unif_subst
 742                         test_equality_only subst context metasenv t1 t2 ugraph)
 743                    (subst,metasenv,ugraph) l1 l2
 744                with (Invalid_argument msg) ->
 745                  raise (UnificationFailure (lazy msg)))
 746           | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
 747               (* we verify that none of the args is a Meta,
 748                 since beta expanding with respoect to a metavariable
 749                 makes no sense  *)
 750  (*
 751               (try
 752                  let (_,t,_) = CicUtil.lookup_subst i subst in
 753                  let lifted = S.subst_meta l t in
 754                  let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
 755                    fo_unif_subst
 756                     test_equality_only
 757                      subst context metasenv reduced t2 ugraph
 758                with CicUtil.Subst_not_found _ -> *)
 759               let subst,metasenv,beta_expanded,ugraph1 =
 760                 beta_expand_many
 761                   test_equality_only metasenv subst context t2 args ugraph
 762               in
 763                 fo_unif_subst test_equality_only subst context metasenv
 764                   (C.Meta (i,l)) beta_expanded ugraph1
 765           | _, C.Meta (i,l)::args when not(exists_a_meta args)  ->
 766               (* (try
 767                  let (_,t,_) = CicUtil.lookup_subst i subst in
 768                  let lifted = S.subst_meta l t in
 769                  let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
 770                    fo_unif_subst
 771                      test_equality_only
 772                      subst context metasenv t1 reduced ugraph
 773                with CicUtil.Subst_not_found _ -> *)
 774                  let subst,metasenv,beta_expanded,ugraph1 =
 775                    beta_expand_many
 776                      test_equality_only
 777                      metasenv subst context t1 args ugraph
 778                  in
 779                    fo_unif_subst test_equality_only subst context metasenv
 780                      (C.Meta (i,l)) beta_expanded ugraph1
 781           | _,_ ->
 782               let lr1 = List.rev l1 in
 783               let lr2 = List.rev l2 in
 784               let rec
 785                   fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
 786                 match (l1,l2) with
 787                     [],_
 788                   | _,[] -> assert false
 789                   | ([h1],[h2]) ->
 790                       fo_unif_subst
 791                         test_equality_only subst context metasenv h1 h2 ugraph
 792                   | ([h],l)
 793                   | (l,[h]) ->
 794                       fo_unif_subst test_equality_only subst context metasenv
 795                         h (C.Appl (List.rev l)) ugraph
 796                   | ((h1::l1),(h2::l2)) ->
 797                       let subst', metasenv',ugraph1 =
 798                         fo_unif_subst
 799                           test_equality_only
 800                           subst context metasenv h1 h2 ugraph
 801                       in
 802                         fo_unif_l
 803                           test_equality_only subst' metasenv' (l1,l2) ugraph1
 804               in
 805               (try
 806                 fo_unif_l
 807                   test_equality_only subst metasenv (lr1, lr2)  ugraph
 808               with
 809               | UnificationFailure s
 810               | Uncertain s as exn ->
 811                   (match l1, l2 with
 812                             (* {{{ pullback *)
 813                   | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
 814                      (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
 815                     CoercDb.is_a_coercion cc1 <> None &&
 816                     CoercDb.is_a_coercion cc2 <> None &&
 817                     not (UriManager.eq uri1 uri2) ->
 818 (*DEBUGGING ONLY:
 819 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
 820 *)
 821                      let inner_coerced t =
 822                       let t = CicMetaSubst.apply_subst subst t in
 823                       let rec aux c x t =
 824                         match t with
 825                         | Cic.Appl l ->
 826                             (match CoercGraph.coerced_arg l with
 827                             | None -> c, x
 828                             | Some (t,_) -> aux (List.hd l) t t)
 829                         | _ ->  c, x
 830                       in
 831                       aux (Cic.Implicit None) (Cic.Implicit None) t
 832                      in
 833                       let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
 834                       let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
 835                       let car1, car2 =
 836                         match
 837                           CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
 838                         with
 839                         | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
 840                         | _ -> assert false
 841                       in
 842                       let head1_c, head2_c =
 843                         match
 844                           CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
 845                         with
 846                         | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
 847                         | _ -> assert false
 848                       in
 849                       let unfold uri ens args =
 850                         let o, _ =
 851                           CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
 852                         in
 853                         assert (ens = []);
 854                         match o with
 855                         | Cic.Constant (_,Some bo,_,_,_) ->
 856                             CicReduction.head_beta_reduce ~delta:false
 857                               (Cic.Appl (bo::args))
 858                         | _ -> assert false
 859                       in
 860                       let conclude subst metasenv ugraph last_tl1' last_tl2' =
 861                        let subst',metasenv,ugraph =
 862 (*DEBUGGING ONLY:
 863 prerr_endline
 864   ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
 865    " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
 866 *)
 867                         fo_unif_subst test_equality_only subst context
 868                          metasenv last_tl1' last_tl2' ugraph
 869                        in
 870                        if subst = subst' then raise exn
 871                        else
 872 (*DEBUGGING ONLY:
 873 let subst,metasenv,ugrph as res =
 874 *)
 875                         fo_unif_subst test_equality_only subst' context
 876                          metasenv (C.Appl l1) (C.Appl l2) ugraph
 877 (*DEBUGGING ONLY:
 878 in
 879 (prerr_endline
 880   (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
 881    " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
 882 res)
 883 *)
 884                       in
 885                       if CoercDb.eq_carr car1 car2 then
 886                          match last_tl1,last_tl2 with
 887                          | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
 888                          | _, C.Meta _
 889                          | C.Meta _, _ ->
 890                            let subst,metasenv,ugraph =
 891                             fo_unif_subst test_equality_only subst context
 892                              metasenv last_tl1 last_tl2 ugraph
 893                            in
 894                             fo_unif_subst test_equality_only subst context
 895                              metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
 896                          | _ when CoercDb.eq_carr head1_c head2_c ->
 897                              (* composite VS composition + metas avoiding
 898                               * coercions not only in coerced position    *)
 899                              if c1 <> cc1 && c2 <> cc2 then
 900                                conclude subst metasenv ugraph
 901                                 last_tl1 last_tl2
 902                              else
 903                               let l1, l2 =
 904                                if c1 = cc1 then
 905                                  unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
 906                                else
 907                                  Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
 908                               in
 909                                fo_unif_subst test_equality_only subst context
 910                                 metasenv l1 l2 ugraph
 911                          | _ -> raise exn
 912                       else
 913                        let grow1 =
 914                          match last_tl1 with Cic.Meta _ -> true | _ -> false in
 915                        let grow2 =
 916                          match last_tl2 with Cic.Meta _ -> true | _ -> false in
 917                        if not (grow1 || grow2) then
 918                           (* no flexible terminals -> no pullback, but
 919                            * we still unify them, in some cases it helps *)
 920                           conclude subst metasenv ugraph last_tl1 last_tl2
 921                        else
 922                         let meets =
 923                           CoercGraph.meets
 924                             metasenv subst context (grow1,car1) (grow2,car2)
 925                         in
 926                         (match meets with
 927                         | [] -> raise exn
 928                         | (carr,metasenv,to1,to2)::xxx ->
 929                            warn_if_not_unique xxx to1 to2 carr car1 car2;
 930                            let last_tl1',(subst,metasenv,ugraph) =
 931                             match grow1,to1 with
 932                              | true,Some (last,coerced) ->
 933                                  last,
 934                                   fo_unif_subst test_equality_only subst context
 935                                   metasenv coerced last_tl1 ugraph
 936                              | _ -> last_tl1,(subst,metasenv,ugraph)
 937                            in
 938                            let last_tl2',(subst,metasenv,ugraph) =
 939                             match grow2,to2 with
 940                              | true,Some (last,coerced) ->
 941                                  last,
 942                                   fo_unif_subst test_equality_only subst context
 943                                   metasenv coerced last_tl2 ugraph
 944                              | _ -> last_tl2,(subst,metasenv,ugraph)
 945                            in
 946                            conclude subst metasenv ugraph last_tl1' last_tl2')
 947                         (* }}} pullback *)
 948                   (* {{{ CSC: This is necessary because of the "elim H" tactic
 949                          where the type of H is only reducible to an
 950                          inductive type. This could be extended from inductive
 951                          types to any rigid term. However, the code is
 952                          duplicated in two places: inside applications and
 953                          outside them. Probably it would be better to
 954                          work with lambda-bar terms instead. *)
 955                   | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
 956                   | (_, Cic.MutInd _::_) ->
 957                      let t1' = R.whd ~subst context t1 in
 958                      (match t1' with
 959                           C.Appl (C.MutInd _::_) ->
 960                             fo_unif_subst test_equality_only
 961                               subst context metasenv t1' t2 ugraph
 962                         | _ -> raise (UnificationFailure (lazy "88")))
 963                   | (Cic.MutInd _::_,_) ->
 964                      let t2' = R.whd ~subst context t2 in
 965                      (match t2' with
 966                           C.Appl (C.MutInd _::_) ->
 967                             fo_unif_subst test_equality_only
 968                               subst context metasenv t1 t2' ugraph
 969                         | _ -> raise
 970                             (UnificationFailure
 971                                (lazy ("not a mutind :"^
 972                                 CicMetaSubst.ppterm ~metasenv subst t2 ))))
 973                      (* }}} elim H *)
 974                   | _ -> raise exn)))
 975    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
 976        let subst', metasenv',ugraph1 =
 977         fo_unif_subst test_equality_only subst context metasenv outt1 outt2
 978           ugraph in
 979        let subst'',metasenv'',ugraph2 =
 980         fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
 981           ugraph1 in
 982        (try
 983          List.fold_left2
 984           (fun (subst,metasenv,ugraph) t1 t2 ->
 985             fo_unif_subst
 986              test_equality_only subst context metasenv t1 t2 ugraph
 987           ) (subst'',metasenv'',ugraph2) pl1 pl2
 988         with
 989          Invalid_argument _ ->
 990           raise (UnificationFailure (lazy "6.1")))
 991            (* (sprintf
 992               "Error trying to unify %s with %s: the number of branches is not the same."
 993               (CicMetaSubst.ppterm ~metasenv subst t1)
 994               (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
 995    | (C.Rel _, _) | (_,  C.Rel _) ->
 996        if t1 = t2 then
 997          subst, metasenv,ugraph
 998        else
 999         raise (UnificationFailure (lazy
1000            (sprintf
1001              "Can't unify %s with %s because they are not convertible"
1002              (CicMetaSubst.ppterm ~metasenv subst t1)
1003              (CicMetaSubst.ppterm ~metasenv subst t2))))
1004    | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
1005        let subst,metasenv,beta_expanded,ugraph1 =
1006          beta_expand_many
1007            test_equality_only metasenv subst context t2 args ugraph
1008        in
1009          fo_unif_subst test_equality_only subst context metasenv
1010            (C.Meta (i,l)) beta_expanded ugraph1
1011    | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
1012        let subst,metasenv,beta_expanded,ugraph1 =
1013          beta_expand_many
1014            test_equality_only metasenv subst context t1 args ugraph
1015        in
1016          fo_unif_subst test_equality_only subst context metasenv
1017            beta_expanded (C.Meta (i,l)) ugraph1
1018 (* Works iff there are no arguments applied to it; similar to the
1019    case below
1020    | (_, C.MutInd _) ->
1021        let t1' = R.whd ~subst context t1 in
1022        (match t1' with
1023             C.MutInd _ ->
1024               fo_unif_subst test_equality_only
1025                 subst context metasenv t1' t2 ugraph
1026           | _ -> raise (UnificationFailure (lazy "8")))
1027 *)
1028    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
1029        let subst',metasenv',ugraph1 =
1030          fo_unif_subst true subst context metasenv s1 s2 ugraph
1031        in
1032          fo_unif_subst test_equality_only
1033            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
1034    | (C.Prod _, _) ->
1035        (match CicReduction.whd ~subst context t2 with
1036         | C.Prod _ as t2 ->
1037             fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1038         | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
1039    | (_, C.Prod _) ->
1040        (match CicReduction.whd ~subst context t1 with
1041         | C.Prod _ as t1 ->
1042             fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1043         | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
1044    | (_,_) ->
1045      (* delta-beta reduction should almost never be a problem for
1046         unification since:
1047          1. long computations require iota reduction
1048          2. it is extremely rare that a close term t1 (that could be unified
1049             to t2) beta-delta reduces to t1' while t2 does not beta-delta
1050             reduces in the same way. This happens only if one meta of t2
1051             occurs in head position during beta reduction. In this unluky
1052             case too much reduction will be performed on t1 and unification
1053             will surely fail. *)
1054      let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
1055      let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
1056       if t1 = t1' && t2 = t2' then
1057        raise (UnificationFailure
1058         (lazy
1059           (sprintf
1060             "Can't unify %s with %s because they are not convertible"
1061             (CicMetaSubst.ppterm ~metasenv subst t1)
1062             (CicMetaSubst.ppterm ~metasenv subst t2))))
1063       else
1064        try
1065         fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
1066        with
1067           UnificationFailure _
1068         | Uncertain _ ->
1069            raise (UnificationFailure
1070             (lazy
1071               (sprintf
1072                 "Can't unify %s with %s because they are not convertible"
1073                 (CicMetaSubst.ppterm ~metasenv subst t1)
1074                 (CicMetaSubst.ppterm ~metasenv subst t2))))
1075
1076 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
1077  exp_named_subst1 exp_named_subst2 ugraph
1078 =
1079  try
1080   List.fold_left2
1081    (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
1082      assert (uri1=uri2) ;
1083      fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1084    ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
1085  with
1086   Invalid_argument _ ->
1087    let print_ens ens =
1088     String.concat " ; "
1089      (List.map
1090        (fun (uri,t) ->
1091          UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
1092        ) ens)
1093    in
1094     raise (UnificationFailure (lazy (sprintf
1095      "Error trying to unify the two explicit named substitutions (local contexts) %s and %s: their lengths is different." (print_ens exp_named_subst1) (print_ens exp_named_subst2))))
1096
1097 (* A substitution is a (int * Cic.term) list that associates a               *)
1098 (* metavariable i with its body.                                             *)
1099 (* metasenv is of type Cic.metasenv                                          *)
1100 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back   *)
1101 (* a new substitution which is already unwinded and ready to be applied and  *)
1102 (* a new metasenv in which some hypothesis in the contexts of the            *)
1103 (* metavariables may have been restricted.                                   *)
1104 let fo_unif metasenv context t1 t2 ugraph =
1105  fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
1106
1107 let enrich_msg msg subst context metasenv t1 t2 ugraph =
1108  lazy (
1109   if verbose then
1110    sprintf "[Verbose] Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s"
1111     (CicMetaSubst.ppterm ~metasenv subst t1)
1112     (try
1113       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1114       CicPp.ppterm ty_t1
1115     with
1116     | UnificationFailure s
1117     | Uncertain s
1118     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1119     (CicMetaSubst.ppterm ~metasenv subst t2)
1120     (try
1121       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1122       CicPp.ppterm ty_t2
1123     with
1124     | UnificationFailure s
1125     | Uncertain s
1126     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1127     (CicMetaSubst.ppcontext ~metasenv subst context)
1128     (CicMetaSubst.ppmetasenv subst metasenv)
1129     (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
1130  else
1131    sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
1132     (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
1133     (try
1134       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1135       CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
1136     with
1137     | UnificationFailure s
1138     | Uncertain s
1139     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1140     (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
1141     (try
1142       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1143       CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
1144     with
1145     | UnificationFailure s
1146     | Uncertain s
1147     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1148     (CicMetaSubst.ppcontext ~metasenv subst context)
1149     (CicMetaSubst.ppmetasenv subst metasenv)
1150     (Lazy.force msg)
1151  )
1152
1153 let fo_unif_subst subst context metasenv t1 t2 ugraph =
1154   try
1155     fo_unif_subst false subst context metasenv t1 t2 ugraph
1156   with
1157   | AssertFailure msg ->
1158      raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
1159   | UnificationFailure msg ->
1160      raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
1161 ;;
1162 *)