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