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