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 uncert_exc metasenv subst context t1 t2 =
  21   Uncertain (lazy (
  22   "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^
  23   " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2))
  24 ;;
  25
  26 let fail_exc metasenv subst context t1 t2 =
  27   UnificationFailure (lazy (
  28   "Can't unify " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^
  29   " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2))
  30 ;;
  31
  32 let mk_appl hd tl =
  33   match hd with
  34   | NCic.Appl l -> NCic.Appl (l@tl)
  35   | _ -> NCic.Appl (hd :: tl)
  36 ;;
  37
  38 let flexible l =
  39   List.exists
  40     (function
  41        | NCic.Meta _
  42        | NCic.Appl (NCic.Meta _::_) -> true
  43        | _ -> false) l
  44 ;;
  45
  46 exception WrongShape;;
  47
  48 let eta_reduce =
  49   let delift_if_not_occur body orig =
  50     try
  51         NCicSubstitution.psubst ~avoid_beta_redexes:true
  52           (fun () -> raise WrongShape) [()] body
  53     with WrongShape -> orig
  54   in
  55   function
  56   | NCic.Lambda(_, _, NCic.Appl [hd; NCic.Rel 1]) as orig ->
  57       delift_if_not_occur hd orig
  58   | NCic.Lambda(_, _, NCic.Appl (hd :: l)) as orig
  59     when HExtlib.list_last l = NCic.Rel 1 ->
  60        let body =
  61          let args, _ = HExtlib.split_nth (List.length l - 1) l in
  62          NCic.Appl (hd::args)
  63        in
  64        delift_if_not_occur body orig
  65   | t -> t
  66 ;;
  67
  68 module C = NCic;;
  69 module Ref = NReference;;
  70
  71 let indent = ref "";;
  72 let inside c = indent := !indent ^ String.make 1 c;;
  73 let outside () = indent := String.sub !indent 0 (String.length !indent -1);;
  74
  75 (*
  76 let pp s =
  77   prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s)
  78 ;;
  79 *)
  80
  81 let pp _ = ();;
  82
  83 let fix_sorts swap metasenv subst context meta t =
  84   let rec aux () = function
  85     | NCic.Sort (NCic.Type u) as orig ->
  86         if swap then
  87          match NCicEnvironment.sup u with
  88          | None -> prerr_endline "no sup for" ;
  89             raise (fail_exc metasenv subst context meta t)
  90          | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)
  91         else
  92          NCic.Sort (NCic.Type (
  93            match NCicEnvironment.sup NCicEnvironment.type0 with
  94            | Some x -> x
  95            | _ -> assert false))
  96     | NCic.Meta _ as orig -> orig
  97     | t -> NCicUtils.map (fun _ _ -> ()) () aux t
  98   in
  99     aux () t
 100 ;;
 101
 102 let rec beta_expand num test_eq_only swap metasenv subst context t arg =
 103   let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' =
 104    try
 105     let metasenv, subst =
 106      if swap then
 107       unify test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg)
 108      else
 109       unify test_eq_only metasenv subst context (NCicSubstitution.lift n arg) t'
 110     in
 111      (metasenv, subst), NCic.Rel (1 + n)
 112    with Uncertain _ | UnificationFailure _ ->
 113        match t' with
 114        | NCic.Rel m as orig ->
 115            (metasenv, subst), if m <= n then orig else NCic.Rel (m+1)
 116        (* andrea: in general, beta_expand can create badly typed
 117         terms. This happens quite seldom in practice, UNLESS we
 118         iterate on the local context. For this reason, we renounce
 119         to iterate and just lift *)
 120        | NCic.Meta (i,(shift,lc)) ->
 121            (metasenv,subst), NCic.Meta (i,(shift+1,lc))
 122        | NCic.Prod (name, src, tgt) as orig ->
 123            let (metasenv, subst), src1 = aux (n,context,true) acc src in
 124            let k = n+1, (name, NCic.Decl src) :: context, test_eq_only in
 125            let ms, tgt1 = aux k (metasenv, subst) tgt in
 126            if src == src1 && tgt == tgt1 then ms, orig else
 127            ms, NCic.Prod (name, src1, tgt1)
 128        | t ->
 129            NCicUntrusted.map_term_fold_a
 130              (fun e (n,ctx,teq) -> n+1,e::ctx,teq) k aux acc t
 131
 132   in
 133   let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in
 134   let fresh_name = "Hbeta" ^ string_of_int num in
 135   let (metasenv,subst), t1 =
 136     aux (0, context, test_eq_only) (metasenv, subst) t in
 137   let t2 = eta_reduce (NCic.Lambda (fresh_name,argty,t1)) in
 138   try
 139     ignore(NCicTypeChecker.typeof ~metasenv ~subst context t2);
 140     metasenv, subst, t2
 141   with NCicTypeChecker.TypeCheckerFailure _ ->
 142     metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg)
 143
 144 and beta_expand_many test_equality_only swap metasenv subst context t args =
 145 (* (*D*)  inside 'B'; try let rc = *)
 146   pp (lazy (String.concat ", "
 147      (List.map (NCicPp.ppterm ~metasenv ~subst ~context)
 148      args) ^ " ∈ " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
 149   let _, subst, metasenv, hd =
 150     List.fold_right
 151       (fun arg (num,subst,metasenv,t) ->
 152          let metasenv, subst, t =
 153            beta_expand num test_equality_only swap metasenv subst context t arg
 154          in
 155            num+1,subst,metasenv,t)
 156       args (1,subst,metasenv,t)
 157   in
 158   pp (lazy ("Head syntesized by b-exp: " ^
 159     NCicPp.ppterm ~metasenv ~subst ~context hd));
 160     metasenv, subst, hd
 161 (* (*D*)  in outside (); rc with exn -> outside (); raise exn *)
 162
 163 and instantiate test_eq_only metasenv subst context n lc t swap =
 164  (*D*)  inside 'I'; try let rc =
 165          pp (lazy(string_of_int n ^ " :=?= "^
 166            NCicPp.ppterm ~metasenv ~subst ~context t));
 167   let unify test_eq_only m s c t1 t2 =
 168     if swap then unify test_eq_only m s c t2 t1
 169     else unify test_eq_only m s c t1 t2
 170   in
 171   let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
 172   let metasenv, subst, t =
 173     match ty with
 174     | NCic.Implicit (`Typeof _) ->
 175        metasenv,subst, t
 176          (* fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t *)
 177     | _ ->
 178        pp (lazy (
 179          "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\nctx:\n"^
 180           NCicPp.ppcontext ~metasenv ~subst context ^ "\nmenv:\n"^
 181           NCicPp.ppmetasenv ~subst metasenv));
 182        let t, ty_t =
 183          try t, NCicTypeChecker.typeof ~subst ~metasenv context t
 184          with
 185          | NCicTypeChecker.AssertFailure msg ->
 186            (pp (lazy "fine typeof (fallimento)");
 187            let ft =
 188             fix_sorts swap metasenv subst context (NCic.Meta (n,lc)) t
 189            in
 190            if ft == t then
 191              (prerr_endline ( ("ILLTYPED: " ^
 192                 NCicPp.ppterm ~metasenv ~subst ~context t
 193             ^ "\nBECAUSE:" ^ Lazy.force msg ^ "\nCONTEXT:\n" ^
 194             NCicPp.ppcontext ~metasenv ~subst context ^ "\nMENV:\n" ^
 195             NCicPp.ppmetasenv ~subst metasenv
 196             ));
 197                      assert false)
 198            else
 199             try
 200               pp (lazy ("typeof: " ^
 201                 NCicPp.ppterm ~metasenv ~subst ~context ft));
 202               ft, NCicTypeChecker.typeof ~subst ~metasenv context ft
 203             with NCicTypeChecker.AssertFailure _ ->
 204               assert false)
 205          | NCicTypeChecker.TypeCheckerFailure msg ->
 206               pp msg; assert false
 207        in
 208        let lty = NCicSubstitution.subst_meta lc ty in
 209        pp (lazy("On the types: " ^
 210         NCicPp.ppterm ~metasenv ~subst ~context:ctx ty ^ " ~~~ " ^
 211         NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
 212          ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t));
 213        let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in
 214        metasenv, subst, t
 215   in
 216          pp (lazy(string_of_int n ^ " := 111 = "^
 217            NCicPp.ppterm ~metasenv ~subst ~context t));
 218   let (metasenv, subst), t =
 219     try NCicMetaSubst.delift metasenv subst context n lc t
 220     with NCicMetaSubst.Uncertain msg ->
 221          pp (lazy ("delift fails: " ^ Lazy.force msg));
 222          raise (Uncertain msg)
 223     | NCicMetaSubst.MetaSubstFailure msg ->
 224          pp (lazy ("delift fails: " ^ Lazy.force msg));
 225          raise (UnificationFailure msg)
 226   in
 227          pp (lazy(string_of_int n ^ " := 222 = "^
 228            NCicPp.ppterm ~metasenv ~subst ~context:ctx t
 229          ^ "\n" ^ NCicPp.ppmetasenv ~subst metasenv));
 230   (* Unifying the types may have already instantiated n. *)
 231   try
 232     let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
 233     let oldt = NCicSubstitution.subst_meta lc oldt in
 234     let t = NCicSubstitution.subst_meta lc t in
 235     (* conjecture: always fail --> occur check *)
 236     unify test_eq_only metasenv subst context oldt t
 237   with NCicUtils.Subst_not_found _ ->
 238     (* by cumulativity when unify(?,Type_i)
 239      * we could ? := Type_j with j <= i... *)
 240     let subst = (n, (name, ctx, t, ty)) :: subst in
 241     pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm
 242       ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t)));
 243     let metasenv =
 244       List.filter (fun (m,_) -> not (n = m)) metasenv
 245     in
 246     metasenv, subst
 247  (*D*)  in outside(); rc with exn -> outside (); raise exn
 248
 249 and unify test_eq_only metasenv subst context t1 t2 =
 250  (*D*) inside 'U'; try let rc =
 251    let fo_unif test_eq_only metasenv subst t1 t2 =
 252     (*D*) inside 'F'; try let rc =
 253      pp (lazy("  " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^
 254          NCicPp.ppterm ~metasenv ~subst ~context t2));
 255      if t1 === t2 then
 256        metasenv, subst
 257      else
 258        match (t1,t2) with
 259        | (C.Sort (C.Type a), C.Sort (C.Type b)) when not test_eq_only ->
 260            if NCicEnvironment.universe_leq a b then metasenv, subst
 261            else raise (fail_exc metasenv subst context t1 t2)
 262        | (C.Sort (C.Type a), C.Sort (C.Type b)) ->
 263            if NCicEnvironment.universe_eq a b then metasenv, subst
 264            else raise (fail_exc metasenv subst context t1 t2)
 265        | (C.Sort C.Prop,C.Sort (C.Type _)) ->
 266            if (not test_eq_only) then metasenv, subst
 267            else raise (fail_exc metasenv subst context t1 t2)
 268
 269        | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2))
 270        | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
 271            let metasenv, subst = unify true metasenv subst context s1 s2 in
 272            unify test_eq_only metasenv subst ((name1, C.Decl s1)::context) t1 t2
 273        | (C.LetIn (name1,ty1,s1,t1), C.LetIn(_,ty2,s2,t2)) ->
 274            let metasenv,subst=unify test_eq_only metasenv subst context ty1 ty2 in
 275            let metasenv,subst=unify test_eq_only metasenv subst context s1 s2 in
 276            let context = (name1, C.Def (s1,ty1))::context in
 277            unify test_eq_only metasenv subst context t1 t2
 278
 279        | (C.Meta (n1,(s1,l1 as lc1)),C.Meta (n2,(s2,l2 as lc2))) when n1 = n2 ->
 280           (try
 281            let l1 = NCicUtils.expand_local_context l1 in
 282            let l2 = NCicUtils.expand_local_context l2 in
 283            let metasenv, subst, to_restrict, _ =
 284             List.fold_right2
 285              (fun t1 t2 (metasenv, subst, to_restrict, i) ->
 286                 try
 287                   let metasenv, subst =
 288                    unify test_eq_only metasenv subst context
 289                     (NCicSubstitution.lift s1 t1) (NCicSubstitution.lift s2 t2)
 290                   in
 291                   metasenv, subst, to_restrict, i-1
 292                 with UnificationFailure _ | Uncertain _ ->
 293                   metasenv, subst, i::to_restrict, i-1)
 294              l1 l2 (metasenv, subst, [], List.length l1)
 295            in
 296            if to_restrict <> [] then
 297              let metasenv, subst, _ =
 298                NCicMetaSubst.restrict metasenv subst n1 to_restrict
 299              in
 300                metasenv, subst
 301            else metasenv, subst
 302           with
 303            | Invalid_argument _ -> assert false
 304            | NCicMetaSubst.MetaSubstFailure msg ->
 305               try
 306                 let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
 307                 let term1 = NCicSubstitution.subst_meta lc1 term in
 308                 let term2 = NCicSubstitution.subst_meta lc2 term in
 309                   unify test_eq_only metasenv subst context term1 term2
 310               with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
 311
 312        | C.Meta (n,lc), t ->
 313            (try
 314              let _,_,term,_ = NCicUtils.lookup_subst n subst in
 315              let term = NCicSubstitution.subst_meta lc term in
 316                unify test_eq_only metasenv subst context term t
 317            with NCicUtils.Subst_not_found _->
 318              instantiate test_eq_only metasenv subst context n lc t false)
 319
 320        | t, C.Meta (n,lc) ->
 321            (try
 322              let _,_,term,_ = NCicUtils.lookup_subst n subst in
 323              let term = NCicSubstitution.subst_meta lc term in
 324                unify test_eq_only metasenv subst context t term
 325            with NCicUtils.Subst_not_found _->
 326              instantiate test_eq_only metasenv subst context n lc t true)
 327
 328        | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
 329             let _,_,term,_ = NCicUtils.lookup_subst i subst in
 330             let term = NCicSubstitution.subst_meta l term in
 331               unify test_eq_only metasenv subst context (mk_appl term args) t2
 332
 333        | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
 334             let _,_,term,_ = NCicUtils.lookup_subst i subst in
 335             let term = NCicSubstitution.subst_meta l term in
 336               unify test_eq_only metasenv subst context t1 (mk_appl term args)
 337
 338        |  NCic.Appl (NCic.Meta (i,_)::_ as l1),
 339           NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
 340             (try
 341               List.fold_left2
 342                 (fun (metasenv, subst) t1 t2 ->
 343                   unify test_eq_only metasenv subst context t1 t2)
 344                 (metasenv,subst) l1 l2
 345             with Invalid_argument _ ->
 346               raise (fail_exc metasenv subst context t1 t2))
 347
 348        | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
 349            (* we verify that none of the args is a Meta,
 350               since beta expanding w.r.t a metavariable makes no sense  *)
 351               let metasenv, subst, beta_expanded =
 352                 beta_expand_many
 353                   test_eq_only false
 354                   metasenv subst context t2 args
 355               in
 356                 unify test_eq_only metasenv subst context
 357                   (C.Meta (i,l)) beta_expanded
 358
 359        | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
 360               let metasenv, subst, beta_expanded =
 361                 beta_expand_many
 362                   test_eq_only true
 363                   metasenv subst context t1 args
 364               in
 365                 unify test_eq_only metasenv subst context
 366                   beta_expanded (C.Meta (i,l))
 367
 368        (* processing this case here we avoid a useless small delta step *)
 369        | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
 370          when Ref.eq r1 r2 ->
 371            let relevance = NCicEnvironment.get_relevance r1 in
 372            let relevance = match r1 with
 373              | Ref.Ref (_,Ref.Con (_,_,lno)) ->
 374                  let _,relevance = HExtlib.split_nth lno relevance in
 375                    HExtlib.mk_list false lno @ relevance
 376              | _ -> relevance
 377            in
 378            let metasenv, subst, _ =
 379              try
 380                List.fold_left2
 381                  (fun (metasenv, subst, relevance) t1 t2 ->
 382                     let b, relevance =
 383                       match relevance with b::tl -> b,tl | _ -> true, [] in
 384                     let metasenv, subst =
 385                       try unify test_eq_only metasenv subst context t1 t2
 386                       with UnificationFailure _ | Uncertain _ when not b ->
 387                         metasenv, subst
 388                     in
 389                       metasenv, subst, relevance)
 390                  (metasenv, subst, relevance) tl1 tl2
 391              with Invalid_argument _ ->
 392                raise (uncert_exc metasenv subst context t1 t2)
 393            in
 394              metasenv, subst
 395
 396        | (C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as ref1,outtype1,term1,pl1),
 397           C.Match (ref2,outtype2,term2,pl2)) ->
 398            let _,_,itl,_,_ = NCicEnvironment.get_checked_indtys ref1 in
 399            let _,_,ty,_ = List.nth itl tyno in
 400            let rec remove_prods ~subst context ty =
 401              let ty = NCicReduction.whd ~subst context ty in
 402              match ty with
 403              | C.Sort _ -> ty
 404              | C.Prod (name,so,ta) ->
 405                    remove_prods ~subst ((name,(C.Decl so))::context) ta
 406              | _ -> assert false
 407            in
 408            let is_prop =
 409              match remove_prods ~subst [] ty with
 410              | C.Sort C.Prop -> true
 411              | _ -> false
 412            in
 413            let rec remove_prods ~subst context ty =
 414              let ty = NCicReduction.whd ~subst context ty in
 415              match ty with
 416              | C.Sort _ -> ty
 417              | C.Prod (name,so,ta) ->
 418                    remove_prods ~subst ((name,(C.Decl so))::context) ta
 419              | _ -> assert false
 420            in
 421            if not (Ref.eq ref1 ref2) then
 422              raise (uncert_exc metasenv subst context t1 t2)
 423            else
 424              let metasenv, subst =
 425                unify test_eq_only metasenv subst context outtype1 outtype2 in
 426              let metasenv, subst =
 427                try unify test_eq_only metasenv subst context term1 term2
 428                with UnificationFailure _ | Uncertain _ when is_prop ->
 429                  metasenv, subst
 430              in
 431              (try
 432               List.fold_left2
 433                (fun (metasenv,subst) ->
 434                   unify test_eq_only metasenv subst context)
 435                (metasenv, subst) pl1 pl2
 436              with Invalid_argument _ ->
 437                raise (uncert_exc metasenv subst context t1 t2))
 438        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
 439        | _ -> raise (uncert_exc metasenv subst context t1 t2)
 440      (*D*)  in outside(); rc with exn -> outside (); raise exn
 441     in
 442     let height_of = function
 443      | NCic.Const (Ref.Ref (_,Ref.Def h))
 444      | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h)))
 445      | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_)
 446      | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h
 447      | _ -> 0
 448     in
 449     let put_in_whd m1 m2 =
 450       NCicReduction.reduce_machine ~delta:max_int ~subst context m1,
 451       NCicReduction.reduce_machine ~delta:max_int ~subst context m2
 452     in
 453     let small_delta_step
 454       ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2)
 455     =
 456      assert (not (norm1 && norm2));
 457      if norm1 then
 458       x1,NCicReduction.reduce_machine ~delta:(height_of t2 -1) ~subst context m2
 459      else if norm2 then
 460       NCicReduction.reduce_machine ~delta:(height_of t1 -1) ~subst context m1,x2
 461      else
 462       let h1 = height_of t1 in
 463       let h2 = height_of t2 in
 464       let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in
 465       NCicReduction.reduce_machine ~delta ~subst context m1,
 466       NCicReduction.reduce_machine ~delta ~subst context m2
 467     in
 468     let rec unif_machines metasenv subst =
 469       function
 470       | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) ->
 471      (*D*) inside 'M'; try let rc =
 472 (*
 473          pp (lazy((if are_normal then "*" else " ") ^ " " ^
 474            NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^
 475            " === " ^
 476            NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2)));
 477 *)
 478           let relevance = [] (* TO BE UNDERSTOOD
 479             match t1 with
 480             | C.Const r -> NCicEnvironment.get_relevance r
 481             | _ -> [] *) in
 482           let unif_from_stack t1 t2 b metasenv subst =
 483               try
 484                 let t1 = NCicReduction.from_stack t1 in
 485                 let t2 = NCicReduction.from_stack t2 in
 486                 unif_machines metasenv subst (put_in_whd t1 t2)
 487               with UnificationFailure _ | Uncertain _ when not b ->
 488                 metasenv, subst
 489           in
 490           let rec check_stack l1 l2 r (metasenv, subst) =
 491             match l1,l2,r with
 492             | x1::tl1, x2::tl2, r::tr ->
 493                 check_stack tl1 tl2 tr
 494                   (unif_from_stack x1 x2 r metasenv subst)
 495             | x1::tl1, x2::tl2, [] ->
 496                 check_stack tl1 tl2 []
 497                   (unif_from_stack x1 x2 true metasenv subst)
 498             | l1, l2, _ ->
 499                 fo_unif test_eq_only metasenv subst
 500                    (NCicReduction.unwind (k1,e1,t1,List.rev l1))
 501                    (NCicReduction.unwind (k2,e2,t2,List.rev l2))
 502           in
 503         try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
 504         with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) ->
 505             unif_machines metasenv subst (small_delta_step m1 m2)
 506       (*D*)  in outside(); rc with exn -> outside (); raise exn
 507      in
 508      try fo_unif test_eq_only metasenv subst t1 t2
 509      with UnificationFailure msg | Uncertain msg as exn ->
 510        try
 511          unif_machines metasenv subst
 512           (put_in_whd (0,[],t1,[]) (0,[],t2,[]))
 513        with
 514        | UnificationFailure _ -> raise (UnificationFailure msg)
 515        | Uncertain _ -> raise exn
 516  (*D*)  in outside(); rc with exn -> outside (); raise exn
 517 ;;
 518
 519 let unify =
 520   indent := "";
 521   unify false;;
 522
 523
 524
 525 (*
 526
 527 open Printf
 528
 529 exception UnificationFailure of string Lazy.t;;
 530 exception Uncertain of string Lazy.t;;
 531 exception AssertFailure of string Lazy.t;;
 532
 533 let verbose = false;;
 534 let debug_print = fun _ -> ()
 535
 536 let profiler_toa = HExtlib.profile "fo_unif_subst.type_of_aux'"
 537 let profiler_beta_expand = HExtlib.profile "fo_unif_subst.beta_expand"
 538 let profiler_deref = HExtlib.profile "fo_unif_subst.deref'"
 539 let profiler_are_convertible = HExtlib.profile "fo_unif_subst.are_convertible"
 540
 541 let profile = HExtlib.profile "U/CicTypeChecker.type_of_aux'"
 542
 543 let type_of_aux' metasenv subst context term ugraph =
 544 let foo () =
 545   try
 546     profile.HExtlib.profile
 547       (CicTypeChecker.type_of_aux' ~subst metasenv context term) ugraph
 548   with
 549       CicTypeChecker.TypeCheckerFailure msg ->
 550         let msg =
 551          lazy
 552           (sprintf
 553            "Kernel Type checking error:
 554 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
 555              (CicMetaSubst.ppterm ~metasenv subst term)
 556              (CicMetaSubst.ppterm ~metasenv [] term)
 557              (CicMetaSubst.ppcontext ~metasenv subst context)
 558              (CicMetaSubst.ppmetasenv subst metasenv)
 559              (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
 560         raise (AssertFailure msg)
 561     | CicTypeChecker.AssertFailure msg ->
 562         let msg = lazy
 563          (sprintf
 564            "Kernel Type checking assertion failure:
 565 %s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
 566              (CicMetaSubst.ppterm ~metasenv subst term)
 567              (CicMetaSubst.ppterm ~metasenv [] term)
 568              (CicMetaSubst.ppcontext ~metasenv subst context)
 569              (CicMetaSubst.ppmetasenv subst metasenv)
 570              (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)) in
 571         raise (AssertFailure msg)
 572 in profiler_toa.HExtlib.profile foo ()
 573 ;;
 574
 575 let exists_a_meta l =
 576   List.exists
 577     (function
 578        | Cic.Meta _
 579        | Cic.Appl (Cic.Meta _::_) -> true
 580        | _ -> false) l
 581
 582 let rec deref subst t =
 583   let snd (_,a,_) = a in
 584   match t with
 585       Cic.Meta(n,l) ->
 586         (try
 587            deref subst
 588              (CicSubstitution.subst_meta
 589                 l (snd (CicUtil.lookup_subst n subst)))
 590          with
 591              CicUtil.Subst_not_found _ -> t)
 592     | Cic.Appl(Cic.Meta(n,l)::args) ->
 593         (match deref subst (Cic.Meta(n,l)) with
 594            | Cic.Lambda _ as t ->
 595                deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
 596            | r -> Cic.Appl(r::args))
 597     | Cic.Appl(((Cic.Lambda _) as t)::args) ->
 598            deref subst (CicReduction.head_beta_reduce (Cic.Appl(t::args)))
 599     | t -> t
 600 ;;
 601
 602 let deref subst t =
 603  let foo () = deref subst t
 604  in profiler_deref.HExtlib.profile foo ()
 605
 606 exception WrongShape;;
 607 let eta_reduce after_beta_expansion after_beta_expansion_body
 608      before_beta_expansion
 609  =
 610  try
 611   match before_beta_expansion,after_beta_expansion_body with
 612      Cic.Appl l, Cic.Appl l' ->
 613       let rec all_but_last check_last =
 614        function
 615           [] -> assert false
 616         | [Cic.Rel 1] -> []
 617         | [_] -> if check_last then raise WrongShape else []
 618         | he::tl -> he::(all_but_last check_last tl)
 619       in
 620        let all_but_last check_last l =
 621         match all_but_last check_last l with
 622            [] -> assert false
 623          | [he] -> he
 624          | l -> Cic.Appl l
 625        in
 626        let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
 627        let all_but_last = all_but_last false l in
 628         (* here we should test alpha-equivalence; however we know by
 629            construction that here alpha_equivalence is equivalent to = *)
 630         if t = all_but_last then
 631          all_but_last
 632         else
 633          after_beta_expansion
 634    | _,_ -> after_beta_expansion
 635  with
 636   WrongShape -> after_beta_expansion
 637
 638 let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
 639  let module S = CicSubstitution in
 640  let module C = Cic in
 641 let foo () =
 642   let rec aux metasenv subst n context t' ugraph =
 643    try
 644
 645     let subst,metasenv,ugraph1 =
 646      fo_unif_subst test_equality_only subst context metasenv
 647       (CicSubstitution.lift n arg) t' ugraph
 648
 649     in
 650      subst,metasenv,C.Rel (1 + n),ugraph1
 651    with
 652       Uncertain _
 653     | UnificationFailure _ ->
 654        match t' with
 655         | C.Rel m  -> subst,metasenv,
 656            (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
 657         | C.Var (uri,exp_named_subst) ->
 658            let subst,metasenv,exp_named_subst',ugraph1 =
 659             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
 660            in
 661             subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
 662         | C.Meta (i,l) ->
 663             (* andrea: in general, beta_expand can create badly typed
 664              terms. This happens quite seldom in practice, UNLESS we
 665              iterate on the local context. For this reason, we renounce
 666              to iterate and just lift *)
 667             let l =
 668               List.map
 669                 (function
 670                      Some t -> Some (CicSubstitution.lift 1 t)
 671                    | None -> None) l in
 672             subst, metasenv, C.Meta (i,l), ugraph
 673         | C.Sort _
 674         | C.Implicit _ as t -> subst,metasenv,t,ugraph
 675         | C.Cast (te,ty) ->
 676             let subst,metasenv,te',ugraph1 =
 677               aux metasenv subst n context te ugraph in
 678             let subst,metasenv,ty',ugraph2 =
 679               aux metasenv subst n context ty ugraph1 in
 680             (* TASSI: sure this is in serial? *)
 681             subst,metasenv,(C.Cast (te', ty')),ugraph2
 682         | C.Prod (nn,s,t) ->
 683            let subst,metasenv,s',ugraph1 =
 684              aux metasenv subst n context s ugraph in
 685            let subst,metasenv,t',ugraph2 =
 686              aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
 687                ugraph1
 688            in
 689            (* TASSI: sure this is in serial? *)
 690            subst,metasenv,(C.Prod (nn, s', t')),ugraph2
 691         | C.Lambda (nn,s,t) ->
 692            let subst,metasenv,s',ugraph1 =
 693              aux metasenv subst n context s ugraph in
 694            let subst,metasenv,t',ugraph2 =
 695             aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
 696            in
 697            (* TASSI: sure this is in serial? *)
 698             subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
 699         | C.LetIn (nn,s,ty,t) ->
 700            let subst,metasenv,s',ugraph1 =
 701              aux metasenv subst n context s ugraph in
 702            let subst,metasenv,ty',ugraph1 =
 703              aux metasenv subst n context ty ugraph in
 704            let subst,metasenv,t',ugraph2 =
 705             aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
 706               ugraph1
 707            in
 708            (* TASSI: sure this is in serial? *)
 709             subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
 710         | C.Appl l ->
 711            let subst,metasenv,revl',ugraph1 =
 712             List.fold_left
 713              (fun (subst,metasenv,appl,ugraph) t ->
 714                let subst,metasenv,t',ugraph1 =
 715                  aux metasenv subst n context t ugraph in
 716                 subst,metasenv,(t'::appl),ugraph1
 717              ) (subst,metasenv,[],ugraph) l
 718            in
 719             subst,metasenv,(C.Appl (List.rev revl')),ugraph1
 720         | C.Const (uri,exp_named_subst) ->
 721            let subst,metasenv,exp_named_subst',ugraph1 =
 722             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
 723            in
 724             subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
 725         | C.MutInd (uri,i,exp_named_subst) ->
 726            let subst,metasenv,exp_named_subst',ugraph1 =
 727             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
 728            in
 729             subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
 730         | C.MutConstruct (uri,i,j,exp_named_subst) ->
 731            let subst,metasenv,exp_named_subst',ugraph1 =
 732             aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
 733            in
 734             subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
 735         | C.MutCase (sp,i,outt,t,pl) ->
 736            let subst,metasenv,outt',ugraph1 =
 737              aux metasenv subst n context outt ugraph in
 738            let subst,metasenv,t',ugraph2 =
 739              aux metasenv subst n context t ugraph1 in
 740            let subst,metasenv,revpl',ugraph3 =
 741             List.fold_left
 742              (fun (subst,metasenv,pl,ugraph) t ->
 743                let subst,metasenv,t',ugraph1 =
 744                  aux metasenv subst n context t ugraph in
 745                subst,metasenv,(t'::pl),ugraph1
 746              ) (subst,metasenv,[],ugraph2) pl
 747            in
 748            subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
 749            (* TASSI: not sure this is serial *)
 750         | C.Fix (i,fl) ->
 751 (*CSC: not implemented
 752            let tylen = List.length fl in
 753             let substitutedfl =
 754              List.map
 755               (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
 756                fl
 757             in
 758              C.Fix (i, substitutedfl)
 759 *)
 760             subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
 761         | C.CoFix (i,fl) ->
 762 (*CSC: not implemented
 763            let tylen = List.length fl in
 764             let substitutedfl =
 765              List.map
 766               (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
 767                fl
 768             in
 769              C.CoFix (i, substitutedfl)
 770
 771 *)
 772             subst,metasenv,(CicSubstitution.lift 1 t'), ugraph
 773
 774   and aux_exp_named_subst metasenv subst n context ens ugraph =
 775    List.fold_right
 776     (fun (uri,t) (subst,metasenv,l,ugraph) ->
 777       let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
 778        subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
 779   in
 780   let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
 781   let fresh_name =
 782    FreshNamesGenerator.mk_fresh_name ~subst
 783     metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
 784   in
 785    let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
 786    let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
 787    subst, metasenv, t'', ugraph2
 788 in profiler_beta_expand.HExtlib.profile foo ()
 789
 790
 791 and beta_expand_many test_equality_only metasenv subst context t args ugraph =
 792   let _,subst,metasenv,hd,ugraph =
 793     List.fold_right
 794       (fun arg (num,subst,metasenv,t,ugraph) ->
 795          let subst,metasenv,t,ugraph1 =
 796            beta_expand num test_equality_only
 797              metasenv subst context t arg ugraph
 798          in
 799            num+1,subst,metasenv,t,ugraph1
 800       ) args (1,subst,metasenv,t,ugraph)
 801   in
 802     subst,metasenv,hd,ugraph
 803
 804 and warn_if_not_unique xxx to1 to2 carr car1 car2 =
 805   match xxx with
 806   | [] -> ()
 807   | (m2,_,c2,c2')::_ ->
 808      let m1,c1,c1' = carr,to1,to2 in
 809      let unopt =
 810        function Some (_,t) -> CicPp.ppterm t
 811        | None -> "id"
 812      in
 813      HLog.warn
 814        ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^
 815        CoercDb.string_of_carr car2^": " ^
 816        CoercDb.string_of_carr m1^" via "^unopt c1^" + "^
 817        unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^
 818        unopt c2^" + "^unopt c2')
 819
 820 (* NUOVA UNIFICAZIONE *)
 821 (* A substitution is a (int * Cic.term) list that associates a
 822    metavariable i with its body.
 823    A metaenv is a (int * Cic.term) list that associate a metavariable
 824    i with is type.
 825    fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
 826    a new substitution which is _NOT_ unwinded. It must be unwinded before
 827    applying it. *)
 828
 829 and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
 830  let module C = Cic in
 831  let module R = CicReduction in
 832  let module S = CicSubstitution in
 833  let t1 = deref subst t1 in
 834  let t2 = deref subst t2 in
 835  let (&&&) a b = (a && b) || ((not a) && (not b)) in
 836 (* let bef = Sys.time () in *)
 837  let b,ugraph =
 838   if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
 839    false,ugraph
 840   else
 841 let foo () =
 842    R.are_convertible ~subst ~metasenv context t1 t2 ugraph
 843 in profiler_are_convertible.HExtlib.profile foo ()
 844  in
 845 (* let aft = Sys.time () in
 846 if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^
 847 CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^
 848 CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
 849    if b then
 850      subst, metasenv, ugraph
 851    else
 852    match (t1, t2) with
 853      | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
 854          let _,subst,metasenv,ugraph1 =
 855            (try
 856               List.fold_left2
 857                 (fun (j,subst,metasenv,ugraph) t1 t2 ->
 858                    match t1,t2 with
 859                        None,_
 860                      | _,None -> j+1,subst,metasenv,ugraph
 861                      | Some t1', Some t2' ->
 862                          (* First possibility:  restriction    *)
 863                          (* Second possibility: unification    *)
 864                          (* Third possibility:  convertibility *)
 865                          let b, ugraph1 =
 866                          R.are_convertible
 867                            ~subst ~metasenv context t1' t2' ugraph
 868                          in
 869                          if b then
 870                            j+1,subst,metasenv, ugraph1
 871                          else
 872                            (try
 873                               let subst,metasenv,ugraph2 =
 874                                 fo_unif_subst
 875                                   test_equality_only
 876                                   subst context metasenv t1' t2' ugraph
 877                               in
 878                                 j+1,subst,metasenv,ugraph2
 879                             with
 880                                 Uncertain _
 881                               | UnificationFailure _ ->
 882 debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
 883                                   let metasenv, subst =
 884                                     CicMetaSubst.restrict
 885                                       subst [(n,j)] metasenv in
 886                                     j+1,subst,metasenv,ugraph1)
 887                 ) (1,subst,metasenv,ugraph) ln lm
 888             with
 889                 Exit ->
 890                   raise
 891                     (UnificationFailure (lazy "1"))
 892                     (*
 893                     (sprintf
 894                       "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."
 895                       (CicMetaSubst.ppterm ~metasenv subst t1)
 896                       (CicMetaSubst.ppterm ~metasenv subst t2))) *)
 897               | Invalid_argument _ ->
 898                   raise
 899                     (UnificationFailure (lazy "2")))
 900                     (*
 901                     (sprintf
 902                       "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
 903                       (CicMetaSubst.ppterm ~metasenv subst t1)
 904                       (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
 905          in subst,metasenv,ugraph1
 906      | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
 907          fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
 908      | (C.Meta (n,l), t)
 909      | (t, C.Meta (n,l)) ->
 910          let swap =
 911            match t1,t2 with
 912                C.Meta (n,_), C.Meta (m,_) when n < m -> false
 913              | _, C.Meta _ -> false
 914              | _,_ -> true
 915          in
 916          let lower = fun x y -> if swap then y else x in
 917          let upper = fun x y -> if swap then x else y in
 918          let fo_unif_subst_ordered
 919              test_equality_only subst context metasenv m1 m2 ugraph =
 920            fo_unif_subst test_equality_only subst context metasenv
 921              (lower m1 m2) (upper m1 m2) ugraph
 922          in
 923          begin
 924          let subst,metasenv,ugraph1 =
 925            let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv in
 926            (try
 927               let tyt,ugraph1 =
 928                 type_of_aux' metasenv subst context t ugraph
 929               in
 930                 fo_unif_subst
 931                   test_equality_only
 932                   subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
 933             with
 934                 UnificationFailure _ as e -> raise e
 935               | Uncertain msg -> raise (UnificationFailure msg)
 936               | AssertFailure _ ->
 937                   debug_print (lazy "siamo allo huge hack");
 938                   (* TODO huge hack!!!!
 939                    * we keep on unifying/refining in the hope that
 940                    * the problem will be eventually solved.
 941                    * In the meantime we're breaking a big invariant:
 942                    * the terms that we are unifying are no longer well
 943                    * typed in the current context (in the worst case
 944                    * we could even diverge) *)
 945                   (subst, metasenv,ugraph)) in
 946          let t',metasenv,subst =
 947            try
 948              CicMetaSubst.delift n subst context metasenv l t
 949            with
 950                (CicMetaSubst.MetaSubstFailure msg)->
 951                  raise (UnificationFailure msg)
 952              | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
 953          in
 954          let t'',ugraph2 =
 955            match t' with
 956                C.Sort (C.Type u) when not test_equality_only ->
 957                  let u' = CicUniv.fresh () in
 958                  let s = C.Sort (C.Type u') in
 959                   (try
 960                     let ugraph2 =
 961                      CicUniv.add_ge (upper u u') (lower u u') ugraph1
 962                     in
 963                      s,ugraph2
 964                    with
 965                     CicUniv.UniverseInconsistency msg ->
 966                      raise (UnificationFailure msg))
 967              | _ -> t',ugraph1
 968          in
 969          (* Unifying the types may have already instantiated n. Let's check *)
 970          try
 971            let (_, oldt,_) = CicUtil.lookup_subst n subst in
 972            let lifted_oldt = S.subst_meta l oldt in
 973              fo_unif_subst_ordered
 974                test_equality_only subst context metasenv t lifted_oldt ugraph2
 975          with
 976              CicUtil.Subst_not_found _ ->
 977                let (_, context, ty) = CicUtil.lookup_meta n metasenv in
 978                let subst = (n, (context, t'',ty)) :: subst in
 979                let metasenv =
 980                  List.filter (fun (m,_,_) -> not (n = m)) metasenv in
 981                subst, metasenv, ugraph2
 982          end
 983    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
 984    | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
 985       if UriManager.eq uri1 uri2 then
 986        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
 987         exp_named_subst1 exp_named_subst2 ugraph
 988       else
 989        raise (UnificationFailure (lazy
 990           (sprintf
 991             "Can't unify %s with %s due to different constants"
 992             (CicMetaSubst.ppterm ~metasenv subst t1)
 993             (CicMetaSubst.ppterm ~metasenv subst t2))))
 994    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
 995        if UriManager.eq uri1 uri2 && i1 = i2 then
 996          fo_unif_subst_exp_named_subst
 997            test_equality_only
 998            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
 999        else
1000          raise (UnificationFailure
1001            (lazy
1002             (sprintf
1003              "Can't unify %s with %s due to different inductive principles"
1004              (CicMetaSubst.ppterm ~metasenv subst t1)
1005              (CicMetaSubst.ppterm ~metasenv subst t2))))
1006    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
1007        C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
1008        if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
1009          fo_unif_subst_exp_named_subst
1010            test_equality_only
1011            subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
1012        else
1013          raise (UnificationFailure
1014           (lazy
1015             (sprintf
1016               "Can't unify %s with %s due to different inductive constructors"
1017               (CicMetaSubst.ppterm ~metasenv subst t1)
1018               (CicMetaSubst.ppterm ~metasenv subst t2))))
1019    | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
1020    | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
1021                               subst context metasenv te t2 ugraph
1022    | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
1023                               subst context metasenv t1 te ugraph
1024    | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
1025        let subst',metasenv',ugraph1 =
1026          fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
1027        in
1028          fo_unif_subst test_equality_only
1029            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
1030    | (C.LetIn (_,s1,ty1,t1), t2)
1031    | (t2, C.LetIn (_,s1,ty1,t1)) ->
1032        fo_unif_subst
1033         test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph
1034    | (C.Appl l1, C.Appl l2) ->
1035        (* andrea: this case should be probably rewritten in the
1036           spirit of deref *)
1037        (match l1,l2 with
1038           | C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
1039               (try
1040                  List.fold_left2
1041                    (fun (subst,metasenv,ugraph) t1 t2 ->
1042                       fo_unif_subst
1043                         test_equality_only subst context metasenv t1 t2 ugraph)
1044                    (subst,metasenv,ugraph) l1 l2
1045                with (Invalid_argument msg) ->
1046                  raise (UnificationFailure (lazy msg)))
1047           | C.Meta (i,l)::args, _ when not(exists_a_meta args) ->
1048               (* we verify that none of the args is a Meta,
1049                 since beta expanding with respoect to a metavariable
1050                 makes no sense  *)
1051  (*
1052               (try
1053                  let (_,t,_) = CicUtil.lookup_subst i subst in
1054                  let lifted = S.subst_meta l t in
1055                  let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
1056                    fo_unif_subst
1057                     test_equality_only
1058                      subst context metasenv reduced t2 ugraph
1059                with CicUtil.Subst_not_found _ -> *)
1060               let subst,metasenv,beta_expanded,ugraph1 =
1061                 beta_expand_many
1062                   test_equality_only metasenv subst context t2 args ugraph
1063               in
1064                 fo_unif_subst test_equality_only subst context metasenv
1065                   (C.Meta (i,l)) beta_expanded ugraph1
1066           | _, C.Meta (i,l)::args when not(exists_a_meta args)  ->
1067               (* (try
1068                  let (_,t,_) = CicUtil.lookup_subst i subst in
1069                  let lifted = S.subst_meta l t in
1070                  let reduced = CicReduction.head_beta_reduce (Cic.Appl (lifted::args)) in
1071                    fo_unif_subst
1072                      test_equality_only
1073                      subst context metasenv t1 reduced ugraph
1074                with CicUtil.Subst_not_found _ -> *)
1075                  let subst,metasenv,beta_expanded,ugraph1 =
1076                    beta_expand_many
1077                      test_equality_only
1078                      metasenv subst context t1 args ugraph
1079                  in
1080                    fo_unif_subst test_equality_only subst context metasenv
1081                      (C.Meta (i,l)) beta_expanded ugraph1
1082           | _,_ ->
1083               let lr1 = List.rev l1 in
1084               let lr2 = List.rev l2 in
1085               let rec
1086                   fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph =
1087                 match (l1,l2) with
1088                     [],_
1089                   | _,[] -> assert false
1090                   | ([h1],[h2]) ->
1091                       fo_unif_subst
1092                         test_equality_only subst context metasenv h1 h2 ugraph
1093                   | ([h],l)
1094                   | (l,[h]) ->
1095                       fo_unif_subst test_equality_only subst context metasenv
1096                         h (C.Appl (List.rev l)) ugraph
1097                   | ((h1::l1),(h2::l2)) ->
1098                       let subst', metasenv',ugraph1 =
1099                         fo_unif_subst
1100                           test_equality_only
1101                           subst context metasenv h1 h2 ugraph
1102                       in
1103                         fo_unif_l
1104                           test_equality_only subst' metasenv' (l1,l2) ugraph1
1105               in
1106               (try
1107                 fo_unif_l
1108                   test_equality_only subst metasenv (lr1, lr2)  ugraph
1109               with
1110               | UnificationFailure s
1111               | Uncertain s as exn ->
1112                   (match l1, l2 with
1113                             (* {{{ pullback *)
1114                   | (((Cic.Const (uri1, ens1)) as cc1) :: tl1),
1115                      (((Cic.Const (uri2, ens2)) as cc2) :: tl2) when
1116                     CoercDb.is_a_coercion cc1 <> None &&
1117                     CoercDb.is_a_coercion cc2 <> None &&
1118                     not (UriManager.eq uri1 uri2) ->
1119 (*DEBUGGING ONLY:
1120 prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1121 *)
1122                      let inner_coerced t =
1123                       let t = CicMetaSubst.apply_subst subst t in
1124                       let rec aux c x t =
1125                         match t with
1126                         | Cic.Appl l ->
1127                             (match CoercGraph.coerced_arg l with
1128                             | None -> c, x
1129                             | Some (t,_) -> aux (List.hd l) t t)
1130                         | _ ->  c, x
1131                       in
1132                       aux (Cic.Implicit None) (Cic.Implicit None) t
1133                      in
1134                       let c1,last_tl1 = inner_coerced (Cic.Appl l1) in
1135                       let c2,last_tl2 = inner_coerced (Cic.Appl l2) in
1136                       let car1, car2 =
1137                         match
1138                           CoercDb.is_a_coercion c1, CoercDb.is_a_coercion c2
1139                         with
1140                         | Some (s1,_,_,_,_), Some (s2,_,_,_,_) -> s1, s2
1141                         | _ -> assert false
1142                       in
1143                       let head1_c, head2_c =
1144                         match
1145                           CoercDb.is_a_coercion cc1, CoercDb.is_a_coercion cc2
1146                         with
1147                         | Some (_,t1,_,_,_), Some (_,t2,_,_,_) -> t1, t2
1148                         | _ -> assert false
1149                       in
1150                       let unfold uri ens args =
1151                         let o, _ =
1152                           CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
1153                         in
1154                         assert (ens = []);
1155                         match o with
1156                         | Cic.Constant (_,Some bo,_,_,_) ->
1157                             CicReduction.head_beta_reduce ~delta:false
1158                               (Cic.Appl (bo::args))
1159                         | _ -> assert false
1160                       in
1161                       let conclude subst metasenv ugraph last_tl1' last_tl2' =
1162                        let subst',metasenv,ugraph =
1163 (*DEBUGGING ONLY:
1164 prerr_endline
1165   ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^
1166    " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context);
1167 *)
1168                         fo_unif_subst test_equality_only subst context
1169                          metasenv last_tl1' last_tl2' ugraph
1170                        in
1171                        if subst = subst' then raise exn
1172                        else
1173 (*DEBUGGING ONLY:
1174 let subst,metasenv,ugrph as res =
1175 *)
1176                         fo_unif_subst test_equality_only subst' context
1177                          metasenv (C.Appl l1) (C.Appl l2) ugraph
1178 (*DEBUGGING ONLY:
1179 in
1180 (prerr_endline
1181   (">>>> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^
1182    " <==> "^CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context);
1183 res)
1184 *)
1185                       in
1186                       if CoercDb.eq_carr car1 car2 then
1187                          match last_tl1,last_tl2 with
1188                          | C.Meta (i1,_),C.Meta(i2,_) when i1 = i2 -> raise exn
1189                          | _, C.Meta _
1190                          | C.Meta _, _ ->
1191                            let subst,metasenv,ugraph =
1192                             fo_unif_subst test_equality_only subst context
1193                              metasenv last_tl1 last_tl2 ugraph
1194                            in
1195                             fo_unif_subst test_equality_only subst context
1196                              metasenv (Cic.Appl l1) (Cic.Appl l2) ugraph
1197                          | _ when CoercDb.eq_carr head1_c head2_c ->
1198                              (* composite VS composition + metas avoiding
1199                               * coercions not only in coerced position    *)
1200                              if c1 <> cc1 && c2 <> cc2 then
1201                                conclude subst metasenv ugraph
1202                                 last_tl1 last_tl2
1203                              else
1204                               let l1, l2 =
1205                                if c1 = cc1 then
1206                                  unfold uri1 ens1 tl1, Cic.Appl (cc2::tl2)
1207                                else
1208                                  Cic.Appl (cc1::tl1), unfold uri2 ens2 tl2
1209                               in
1210                                fo_unif_subst test_equality_only subst context
1211                                 metasenv l1 l2 ugraph
1212                          | _ -> raise exn
1213                       else
1214                        let grow1 =
1215                          match last_tl1 with Cic.Meta _ -> true | _ -> false in
1216                        let grow2 =
1217                          match last_tl2 with Cic.Meta _ -> true | _ -> false in
1218                        if not (grow1 || grow2) then
1219                           (* no flexible terminals -> no pullback, but
1220                            * we still unify them, in some cases it helps *)
1221                           conclude subst metasenv ugraph last_tl1 last_tl2
1222                        else
1223                         let meets =
1224                           CoercGraph.meets
1225                             metasenv subst context (grow1,car1) (grow2,car2)
1226                         in
1227                         (match meets with
1228                         | [] -> raise exn
1229                         | (carr,metasenv,to1,to2)::xxx ->
1230                            warn_if_not_unique xxx to1 to2 carr car1 car2;
1231                            let last_tl1',(subst,metasenv,ugraph) =
1232                             match grow1,to1 with
1233                              | true,Some (last,coerced) ->
1234                                  last,
1235                                   fo_unif_subst test_equality_only subst context
1236                                   metasenv coerced last_tl1 ugraph
1237                              | _ -> last_tl1,(subst,metasenv,ugraph)
1238                            in
1239                            let last_tl2',(subst,metasenv,ugraph) =
1240                             match grow2,to2 with
1241                              | true,Some (last,coerced) ->
1242                                  last,
1243                                   fo_unif_subst test_equality_only subst context
1244                                   metasenv coerced last_tl2 ugraph
1245                              | _ -> last_tl2,(subst,metasenv,ugraph)
1246                            in
1247                            conclude subst metasenv ugraph last_tl1' last_tl2')
1248                         (* }}} pullback *)
1249                   (* {{{ CSC: This is necessary because of the "elim H" tactic
1250                          where the type of H is only reducible to an
1251                          inductive type. This could be extended from inductive
1252                          types to any rigid term. However, the code is
1253                          duplicated in two places: inside applications and
1254                          outside them. Probably it would be better to
1255                          work with lambda-bar terms instead. *)
1256                   | (Cic.MutInd _::_, Cic.MutInd _::_) -> raise exn
1257                   | (_, Cic.MutInd _::_) ->
1258                      let t1' = R.whd ~subst context t1 in
1259                      (match t1' with
1260                           C.Appl (C.MutInd _::_) ->
1261                             fo_unif_subst test_equality_only
1262                               subst context metasenv t1' t2 ugraph
1263                         | _ -> raise (UnificationFailure (lazy "88")))
1264                   | (Cic.MutInd _::_,_) ->
1265                      let t2' = R.whd ~subst context t2 in
1266                      (match t2' with
1267                           C.Appl (C.MutInd _::_) ->
1268                             fo_unif_subst test_equality_only
1269                               subst context metasenv t1 t2' ugraph
1270                         | _ -> raise
1271                             (UnificationFailure
1272                                (lazy ("not a mutind :"^
1273                                 CicMetaSubst.ppterm ~metasenv subst t2 ))))
1274                      (* }}} elim H *)
1275                   | _ -> raise exn)))
1276    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
1277        let subst', metasenv',ugraph1 =
1278         fo_unif_subst test_equality_only subst context metasenv outt1 outt2
1279           ugraph in
1280        let subst'',metasenv'',ugraph2 =
1281         fo_unif_subst test_equality_only subst' context metasenv' t1' t2'
1282           ugraph1 in
1283        (try
1284          List.fold_left2
1285           (fun (subst,metasenv,ugraph) t1 t2 ->
1286             fo_unif_subst
1287              test_equality_only subst context metasenv t1 t2 ugraph
1288           ) (subst'',metasenv'',ugraph2) pl1 pl2
1289         with
1290          Invalid_argument _ ->
1291           raise (UnificationFailure (lazy "6.1")))
1292            (* (sprintf
1293               "Error trying to unify %s with %s: the number of branches is not the same."
1294               (CicMetaSubst.ppterm ~metasenv subst t1)
1295               (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
1296    | (C.Rel _, _) | (_,  C.Rel _) ->
1297        if t1 = t2 then
1298          subst, metasenv,ugraph
1299        else
1300         raise (UnificationFailure (lazy
1301            (sprintf
1302              "Can't unify %s with %s because they are not convertible"
1303              (CicMetaSubst.ppterm ~metasenv subst t1)
1304              (CicMetaSubst.ppterm ~metasenv subst t2))))
1305    | (C.Appl (C.Meta(i,l)::args),t2) when not(exists_a_meta args) ->
1306        let subst,metasenv,beta_expanded,ugraph1 =
1307          beta_expand_many
1308            test_equality_only metasenv subst context t2 args ugraph
1309        in
1310          fo_unif_subst test_equality_only subst context metasenv
1311            (C.Meta (i,l)) beta_expanded ugraph1
1312    | (t1,C.Appl (C.Meta(i,l)::args)) when not(exists_a_meta args) ->
1313        let subst,metasenv,beta_expanded,ugraph1 =
1314          beta_expand_many
1315            test_equality_only metasenv subst context t1 args ugraph
1316        in
1317          fo_unif_subst test_equality_only subst context metasenv
1318            beta_expanded (C.Meta (i,l)) ugraph1
1319 (* Works iff there are no arguments applied to it; similar to the
1320    case below
1321    | (_, C.MutInd _) ->
1322        let t1' = R.whd ~subst context t1 in
1323        (match t1' with
1324             C.MutInd _ ->
1325               fo_unif_subst test_equality_only
1326                 subst context metasenv t1' t2 ugraph
1327           | _ -> raise (UnificationFailure (lazy "8")))
1328 *)
1329    | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) ->
1330        let subst',metasenv',ugraph1 =
1331          fo_unif_subst true subst context metasenv s1 s2 ugraph
1332        in
1333          fo_unif_subst test_equality_only
1334            subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1
1335    | (C.Prod _, _) ->
1336        (match CicReduction.whd ~subst context t2 with
1337         | C.Prod _ as t2 ->
1338             fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1339         | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t2^"Not a product"))))
1340    | (_, C.Prod _) ->
1341        (match CicReduction.whd ~subst context t1 with
1342         | C.Prod _ as t1 ->
1343             fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1344         | _ -> raise (UnificationFailure (lazy (CicMetaSubst.ppterm ~metasenv subst t1^"Not a product"))))
1345    | (_,_) ->
1346      (* delta-beta reduction should almost never be a problem for
1347         unification since:
1348          1. long computations require iota reduction
1349          2. it is extremely rare that a close term t1 (that could be unified
1350             to t2) beta-delta reduces to t1' while t2 does not beta-delta
1351             reduces in the same way. This happens only if one meta of t2
1352             occurs in head position during beta reduction. In this unluky
1353             case too much reduction will be performed on t1 and unification
1354             will surely fail. *)
1355      let t1' = CicReduction.head_beta_reduce ~delta:true t1 in
1356      let t2' = CicReduction.head_beta_reduce ~delta:true t2 in
1357       if t1 = t1' && t2 = t2' then
1358        raise (UnificationFailure
1359         (lazy
1360           (sprintf
1361             "Can't unify %s with %s because they are not convertible"
1362             (CicMetaSubst.ppterm ~metasenv subst t1)
1363             (CicMetaSubst.ppterm ~metasenv subst t2))))
1364       else
1365        try
1366         fo_unif_subst test_equality_only subst context metasenv t1' t2' ugraph
1367        with
1368           UnificationFailure _
1369         | Uncertain _ ->
1370            raise (UnificationFailure
1371             (lazy
1372               (sprintf
1373                 "Can't unify %s with %s because they are not convertible"
1374                 (CicMetaSubst.ppterm ~metasenv subst t1)
1375                 (CicMetaSubst.ppterm ~metasenv subst t2))))
1376
1377 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
1378  exp_named_subst1 exp_named_subst2 ugraph
1379 =
1380  try
1381   List.fold_left2
1382    (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) ->
1383      assert (uri1=uri2) ;
1384      fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph
1385    ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2
1386  with
1387   Invalid_argument _ ->
1388    let print_ens ens =
1389     String.concat " ; "
1390      (List.map
1391        (fun (uri,t) ->
1392          UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm ~metasenv subst t)
1393        ) ens)
1394    in
1395     raise (UnificationFailure (lazy (sprintf
1396      "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))))
1397
1398 (* A substitution is a (int * Cic.term) list that associates a               *)
1399 (* metavariable i with its body.                                             *)
1400 (* metasenv is of type Cic.metasenv                                          *)
1401 (* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back   *)
1402 (* a new substitution which is already unwinded and ready to be applied and  *)
1403 (* a new metasenv in which some hypothesis in the contexts of the            *)
1404 (* metavariables may have been restricted.                                   *)
1405 let fo_unif metasenv context t1 t2 ugraph =
1406  fo_unif_subst false [] context metasenv t1 t2 ugraph ;;
1407
1408 let enrich_msg msg subst context metasenv t1 t2 ugraph =
1409  lazy (
1410   if verbose then
1411    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"
1412     (CicMetaSubst.ppterm ~metasenv subst t1)
1413     (try
1414       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1415       CicPp.ppterm ty_t1
1416     with
1417     | UnificationFailure s
1418     | Uncertain s
1419     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1420     (CicMetaSubst.ppterm ~metasenv subst t2)
1421     (try
1422       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1423       CicPp.ppterm ty_t2
1424     with
1425     | UnificationFailure s
1426     | Uncertain s
1427     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1428     (CicMetaSubst.ppcontext ~metasenv subst context)
1429     (CicMetaSubst.ppmetasenv subst metasenv)
1430     (CicMetaSubst.ppsubst ~metasenv subst) (Lazy.force msg)
1431  else
1432    sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
1433     (CicMetaSubst.ppterm_in_context ~metasenv subst t1 context)
1434     (try
1435       let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in
1436       CicMetaSubst.ppterm_in_context ~metasenv subst ty_t1 context
1437     with
1438     | UnificationFailure s
1439     | Uncertain s
1440     | AssertFailure s -> sprintf "MALFORMED(t1): \n<BEGIN>%s\n<END>" (Lazy.force s))
1441     (CicMetaSubst.ppterm_in_context ~metasenv subst t2 context)
1442     (try
1443       let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in
1444       CicMetaSubst.ppterm_in_context ~metasenv subst ty_t2 context
1445     with
1446     | UnificationFailure s
1447     | Uncertain s
1448     | AssertFailure s -> sprintf "MALFORMED(t2): \n<BEGIN>%s\n<END>" (Lazy.force s))
1449     (CicMetaSubst.ppcontext ~metasenv subst context)
1450     (CicMetaSubst.ppmetasenv subst metasenv)
1451     (Lazy.force msg)
1452  )
1453
1454 let fo_unif_subst subst context metasenv t1 t2 ugraph =
1455   try
1456     fo_unif_subst false subst context metasenv t1 t2 ugraph
1457   with
1458   | AssertFailure msg ->
1459      raise (AssertFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
1460   | UnificationFailure msg ->
1461      raise (UnificationFailure (enrich_msg msg subst context metasenv t1 t2 ugraph))
1462 ;;
1463 *)