helm/software/components/ng_refiner/nCicUnification.ml

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