helm/software/components/ng_refiner/nCicUnification.ml

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