helm/software/components/ng_refiner/nCicUnification.ml

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