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