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