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