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