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