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