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