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