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