components/ng_refiner/nCicMetaSubst.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 MetaSubstFailure of string Lazy.t
  15 exception Uncertain of string Lazy.t
  16
  17 (*
  18 (*** Functions to apply a substitution ***)
  19
  20 let apply_subst_gen ~appl_fun subst term =
  21  let rec um_aux =
  22   let module C = Cic in
  23   let module S = CicSubstitution in
  24    function
  25       C.Rel _ as t -> t
  26     | C.Var (uri,exp_named_subst) ->
  27        let exp_named_subst' =
  28          List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
  29        in
  30        C.Var (uri, exp_named_subst')
  31     | C.Meta (i, l) ->
  32         (try
  33           let (_, t,_) = lookup_subst i subst in
  34           um_aux (S.subst_meta l t)
  35         with CicUtil.Subst_not_found _ ->
  36           (* unconstrained variable, i.e. free in subst*)
  37           let l' =
  38             List.map (function None -> None | Some t -> Some (um_aux t)) l
  39           in
  40            C.Meta (i,l'))
  41     | C.Sort _
  42     | C.Implicit _ as t -> t
  43     | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
  44     | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
  45     | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
  46     | C.LetIn (n,s,ty,t) -> C.LetIn (n, um_aux s, um_aux ty, um_aux t)
  47     | C.Appl (hd :: tl) -> appl_fun um_aux hd tl
  48     | C.Appl _ -> assert false
  49     | C.Const (uri,exp_named_subst) ->
  50        let exp_named_subst' =
  51          List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
  52        in
  53        C.Const (uri, exp_named_subst')
  54     | C.MutInd (uri,typeno,exp_named_subst) ->
  55        let exp_named_subst' =
  56          List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
  57        in
  58        C.MutInd (uri,typeno,exp_named_subst')
  59     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
  60        let exp_named_subst' =
  61          List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
  62        in
  63        C.MutConstruct (uri,typeno,consno,exp_named_subst')
  64     | C.MutCase (sp,i,outty,t,pl) ->
  65        let pl' = List.map um_aux pl in
  66        C.MutCase (sp, i, um_aux outty, um_aux t, pl')
  67     | C.Fix (i, fl) ->
  68        let fl' =
  69          List.map (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo)) fl
  70        in
  71        C.Fix (i, fl')
  72     | C.CoFix (i, fl) ->
  73        let fl' =
  74          List.map (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo)) fl
  75        in
  76        C.CoFix (i, fl')
  77  in
  78   um_aux term
  79 ;;
  80
  81 let apply_subst =
  82   let appl_fun um_aux he tl =
  83     let tl' = List.map um_aux tl in
  84     let t' =
  85      match um_aux he with
  86         Cic.Appl l -> Cic.Appl (l@tl')
  87       | he' -> Cic.Appl (he'::tl')
  88     in
  89      begin
  90       match he with
  91          Cic.Meta (m,_) -> CicReduction.head_beta_reduce t'
  92        | _ -> t'
  93      end
  94   in
  95   fun subst t ->
  96 (*     incr apply_subst_counter; *)
  97 match subst with
  98    [] -> t
  99  | _ -> apply_subst_gen ~appl_fun subst t
 100 ;;
 101
 102 let profiler = HExtlib.profile "U/CicMetaSubst.apply_subst"
 103 let apply_subst s t =
 104   profiler.HExtlib.profile (apply_subst s) t
 105
 106
 107 let apply_subst_context subst context =
 108  match subst with
 109     [] -> context
 110   | _ ->
 111 (*
 112   incr apply_subst_context_counter;
 113   context_length := !context_length + List.length context;
 114 *)
 115   List.fold_right
 116     (fun item context ->
 117       match item with
 118       | Some (n, Cic.Decl t) ->
 119           let t' = apply_subst subst t in
 120           Some (n, Cic.Decl t') :: context
 121       | Some (n, Cic.Def (t, ty)) ->
 122           let ty' = apply_subst subst ty in
 123           let t' = apply_subst subst t in
 124           Some (n, Cic.Def (t', ty')) :: context
 125       | None -> None :: context)
 126     context []
 127
 128 let apply_subst_metasenv subst metasenv =
 129 (*
 130   incr apply_subst_metasenv_counter;
 131   metasenv_length := !metasenv_length + List.length metasenv;
 132 *)
 133 match subst with
 134    [] -> metasenv
 135  | _ ->
 136   List.map
 137     (fun (n, context, ty) ->
 138       (n, apply_subst_context subst context, apply_subst subst ty))
 139     (List.filter
 140       (fun (i, _, _) -> not (List.mem_assoc i subst))
 141       metasenv)
 142
 143 let tempi_type_of_aux_subst = ref 0.0;;
 144 let tempi_subst = ref 0.0;;
 145 let tempi_type_of_aux = ref 0.0;;
 146 *)
 147
 148
 149 exception NotInTheList;;
 150
 151 let position n (shift, lc) =
 152   match lc with
 153   | NCic.Irl len when n <= shift || n > shift + len -> raise NotInTheList
 154   | NCic.Itl len -> n - shift
 155   | NCic.Ctx tl ->
 156       let rec aux k = function
 157          | [] -> raise NotInTheList
 158          | (Cic.Rel m)::_ when m + shift = n -> k
 159          | _::tl -> aux (k+1) tl
 160       in
 161        aux 1 tl
 162 ;;
 163 (*
 164 exception Occur;;
 165
 166 let rec force_does_not_occur subst to_be_restricted t =
 167  let module C = Cic in
 168  let more_to_be_restricted = ref [] in
 169  let rec aux k = function
 170       C.Rel r when List.mem (r - k) to_be_restricted -> raise Occur
 171     | C.Rel _
 172     | C.Sort _ as t -> t
 173     | C.Implicit _ -> assert false
 174     | C.Meta (n, l) ->
 175        (* we do not retrieve the term associated to ?n in subst since *)
 176        (* in this way we can restrict if something goes wrong         *)
 177        let l' =
 178          let i = ref 0 in
 179          List.map
 180            (function t ->
 181              incr i ;
 182              match t with
 183                 None -> None
 184               | Some t ->
 185                  try
 186                    Some (aux k t)
 187                  with Occur ->
 188                    more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
 189                    None)
 190            l
 191        in
 192         C.Meta (n, l')
 193     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
 194     | C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest)
 195     | C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest)
 196     | C.LetIn (name,so,ty,dest) ->
 197        C.LetIn (name, aux k so, aux k ty, aux (k+1) dest)
 198     | C.Appl l -> C.Appl (List.map (aux k) l)
 199     | C.Var (uri,exp_named_subst) ->
 200         let exp_named_subst' =
 201           List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
 202         in
 203         C.Var (uri, exp_named_subst')
 204     | C.Const (uri, exp_named_subst) ->
 205         let exp_named_subst' =
 206           List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
 207         in
 208         C.Const (uri, exp_named_subst')
 209     | C.MutInd (uri,tyno,exp_named_subst) ->
 210         let exp_named_subst' =
 211           List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
 212         in
 213         C.MutInd (uri, tyno, exp_named_subst')
 214     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 215         let exp_named_subst' =
 216           List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
 217         in
 218         C.MutConstruct (uri, tyno, consno, exp_named_subst')
 219     | C.MutCase (uri,tyno,out,te,pl) ->
 220         C.MutCase (uri, tyno, aux k out, aux k te, List.map (aux k) pl)
 221     | C.Fix (i,fl) ->
 222        let len = List.length fl in
 223        let k_plus_len = k + len in
 224        let fl' =
 225          List.map
 226           (fun (name,j,ty,bo) -> (name, j, aux k ty, aux k_plus_len bo)) fl
 227        in
 228        C.Fix (i, fl')
 229     | C.CoFix (i,fl) ->
 230        let len = List.length fl in
 231        let k_plus_len = k + len in
 232        let fl' =
 233          List.map
 234           (fun (name,ty,bo) -> (name, aux k ty, aux k_plus_len bo)) fl
 235        in
 236        C.CoFix (i, fl')
 237  in
 238  let res = aux 0 t in
 239  (!more_to_be_restricted, res)
 240
 241 let rec restrict subst to_be_restricted metasenv =
 242  match to_be_restricted with
 243  | [] -> metasenv, subst
 244  | _ ->
 245   let names_of_context_indexes context indexes =
 246     String.concat ", "
 247       (List.map
 248         (fun i ->
 249           try
 250            match List.nth context (i-1) with
 251            | None -> assert false
 252            | Some (n, _) -> CicPp.ppname n
 253           with
 254            Failure _ -> assert false
 255         ) indexes)
 256   in
 257   let force_does_not_occur_in_context to_be_restricted = function
 258     | None -> [], None
 259     | Some (name, Cic.Decl t) ->
 260         let (more_to_be_restricted, t') =
 261           force_does_not_occur subst to_be_restricted t
 262         in
 263         more_to_be_restricted, Some (name, Cic.Decl t')
 264     | Some (name, Cic.Def (bo, ty)) ->
 265         let (more_to_be_restricted, bo') =
 266           force_does_not_occur subst to_be_restricted bo
 267         in
 268         let more_to_be_restricted, ty' =
 269          let more_to_be_restricted', ty' =
 270            force_does_not_occur subst to_be_restricted ty
 271          in
 272          more_to_be_restricted @ more_to_be_restricted',
 273          ty'
 274         in
 275         more_to_be_restricted, Some (name, Cic.Def (bo', ty'))
 276   in
 277   let rec erase i to_be_restricted n = function
 278     | [] -> [], to_be_restricted, []
 279     | hd::tl ->
 280         let more_to_be_restricted,restricted,tl' =
 281           erase (i+1) to_be_restricted n tl
 282         in
 283         let restrict_me = List.mem i restricted in
 284         if restrict_me then
 285           more_to_be_restricted, restricted, None:: tl'
 286         else
 287           (try
 288             let more_to_be_restricted', hd' =
 289               let delifted_restricted =
 290                let rec aux =
 291                 function
 292                    [] -> []
 293                  | j::tl when j > i -> (j - i)::aux tl
 294                  | _::tl -> aux tl
 295                in
 296                 aux restricted
 297               in
 298                force_does_not_occur_in_context delifted_restricted hd
 299             in
 300              more_to_be_restricted @ more_to_be_restricted',
 301              restricted, hd' :: tl'
 302           with Occur ->
 303             more_to_be_restricted, (i :: restricted), None :: tl')
 304   in
 305   let (more_to_be_restricted, metasenv) =  (* restrict metasenv *)
 306     List.fold_right
 307       (fun (n, context, t) (more, metasenv) ->
 308         let to_be_restricted =
 309           List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
 310         in
 311         let (more_to_be_restricted, restricted, context') =
 312          (* just an optimization *)
 313          if to_be_restricted = [] then
 314           [],[],context
 315          else
 316           erase 1 to_be_restricted n context
 317         in
 318         try
 319           let more_to_be_restricted', t' =
 320             force_does_not_occur subst restricted t
 321           in
 322           let metasenv' = (n, context', t') :: metasenv in
 323           (more @ more_to_be_restricted @ more_to_be_restricted',
 324           metasenv')
 325         with Occur ->
 326           raise (MetaSubstFailure (lazy (sprintf
 327             "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them"
 328             n (names_of_context_indexes context to_be_restricted)))))
 329       metasenv ([], [])
 330   in
 331   let (more_to_be_restricted', subst) = (* restrict subst *)
 332     List.fold_right
 333       (* TODO: cambiare dopo l'aggiunta del ty *)
 334       (fun (n, (context, term,ty)) (more, subst') ->
 335         let to_be_restricted =
 336           List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
 337         in
 338         (try
 339           let (more_to_be_restricted, restricted, context') =
 340            (* just an optimization *)
 341             if to_be_restricted = [] then
 342               [], [], context
 343             else
 344               erase 1 to_be_restricted n context
 345           in
 346           let more_to_be_restricted', term' =
 347             force_does_not_occur subst restricted term
 348           in
 349           let more_to_be_restricted'', ty' =
 350             force_does_not_occur subst restricted ty in
 351           let subst' = (n, (context', term',ty')) :: subst' in
 352           let more =
 353             more @ more_to_be_restricted
 354             @ more_to_be_restricted'@more_to_be_restricted'' in
 355           (more, subst')
 356         with Occur ->
 357           let error_msg = lazy (sprintf
 358             "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term"
 359             n (names_of_context_indexes context to_be_restricted) n
 360             (ppterm ~metasenv subst term))
 361           in
 362           (* DEBUG
 363           debug_print (lazy error_msg);
 364           debug_print (lazy ("metasenv = \n" ^ (ppmetasenv metasenv subst)));
 365           debug_print (lazy ("subst = \n" ^ (ppsubst subst)));
 366           debug_print (lazy ("context = \n" ^ (ppcontext subst context))); *)
 367           raise (MetaSubstFailure error_msg)))
 368       subst ([], [])
 369   in
 370    restrict subst (more_to_be_restricted @ more_to_be_restricted') metasenv
 371 ;;
 372 *)
 373
 374 let newmeta =
 375   let maxmeta = ref 0 in
 376   fun () -> incr maxmeta; !maxmeta
 377 ;;
 378
 379 let restrict metasenv subst i to_be_restricted =
 380   let force_does_not_occur_in_context to_be_restricted = function
 381     | None -> [], None
 382     | Some (name, Cic.Decl t) ->
 383         let (more_to_be_restricted, t') =
 384           force_does_not_occur subst to_be_restricted t
 385         in
 386         more_to_be_restricted, Some (name, Cic.Decl t')
 387     | Some (name, Cic.Def (bo, ty)) ->
 388         let (more_to_be_restricted, bo') =
 389           force_does_not_occur subst to_be_restricted bo
 390         in
 391         let more_to_be_restricted, ty' =
 392          let more_to_be_restricted', ty' =
 393            force_does_not_occur subst to_be_restricted ty
 394          in
 395          more_to_be_restricted @ more_to_be_restricted',
 396          ty'
 397         in
 398         more_to_be_restricted, Some (name, Cic.Def (bo', ty'))
 399   in
 400   let rec erase i to_be_restricted n = function
 401     | [] -> [], to_be_restricted, []
 402     | hd::tl ->
 403         let more_to_be_restricted,restricted,tl' =
 404           erase (i+1) to_be_restricted n tl
 405         in
 406         let restrict_me = List.mem i restricted in
 407         if restrict_me then
 408           more_to_be_restricted, restricted, None:: tl'
 409         else
 410           (try
 411             let more_to_be_restricted', hd' =
 412               let delifted_restricted =
 413                let rec aux =
 414                 function
 415                    [] -> []
 416                  | j::tl when j > i -> (j - i)::aux tl
 417                  | _::tl -> aux tl
 418                in
 419                 aux restricted
 420               in
 421                force_does_not_occur_in_context delifted_restricted hd
 422             in
 423              more_to_be_restricted @ more_to_be_restricted',
 424              restricted, hd' :: tl'
 425           with Occur ->
 426             more_to_be_restricted, (i :: restricted), None :: tl')
 427   in
 428   let (more_to_be_restricted, metasenv) =  (* restrict metasenv *)
 429     List.fold_right
 430       (fun (n, context, t) (more, metasenv) ->
 431         let to_be_restricted =
 432           List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
 433         in
 434         let (more_to_be_restricted, restricted, context') =
 435          (* just an optimization *)
 436          if to_be_restricted = [] then
 437           [],[],context
 438          else
 439           erase 1 to_be_restricted n context
 440         in
 441         try
 442           let more_to_be_restricted', t' =
 443             force_does_not_occur subst restricted t
 444           in
 445           let metasenv' = (n, context', t') :: metasenv in
 446           (more @ more_to_be_restricted @ more_to_be_restricted',
 447           metasenv')
 448         with Occur ->
 449           raise (MetaSubstFailure (lazy (sprintf
 450             "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them"
 451             n (names_of_context_indexes context to_be_restricted)))))
 452       metasenv ([], [])
 453   in
 454   let (more_to_be_restricted', subst) = (* restrict subst *)
 455     List.fold_right
 456       (* TODO: cambiare dopo l'aggiunta del ty *)
 457       (fun (n, (context, term,ty)) (more, subst') ->
 458         let to_be_restricted =
 459           List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
 460         in
 461         (try
 462           let (more_to_be_restricted, restricted, context') =
 463            (* just an optimization *)
 464             if to_be_restricted = [] then
 465               [], [], context
 466             else
 467               erase 1 to_be_restricted n context
 468           in
 469           let more_to_be_restricted', term' =
 470             force_does_not_occur subst restricted term
 471           in
 472           let more_to_be_restricted'', ty' =
 473             force_does_not_occur subst restricted ty in
 474           let subst' = (n, (context', term',ty')) :: subst' in
 475           let more =
 476             more @ more_to_be_restricted
 477             @ more_to_be_restricted'@more_to_be_restricted'' in
 478           (more, subst')
 479         with Occur ->
 480           let error_msg = lazy (sprintf
 481             "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term"
 482             n (names_of_context_indexes context to_be_restricted) n
 483             (ppterm ~metasenv subst term))
 484           in
 485           (* DEBUG
 486           debug_print (lazy error_msg);
 487           debug_print (lazy ("metasenv = \n" ^ (ppmetasenv metasenv subst)));
 488           debug_print (lazy ("subst = \n" ^ (ppsubst subst)));
 489           debug_print (lazy ("context = \n" ^ (ppcontext subst context))); *)
 490           raise (MetaSubstFailure error_msg)))
 491       subst ([], [])
 492   in
 493    restrict subst (more_to_be_restricted @ more_to_be_restricted') metasenv
 494 ;;
 495 *)
 496 ;;
 497
 498 (* INVARIANT: we suppose that t is not another occurrence of Meta(n,_),
 499    otherwise the occur check does not make sense in case of unification
 500    of ?n with ?n *)
 501 let delift metasenv subst context n l t =
 502   let to_be_restricted = ref [] in
 503   let rec aux k = function
 504     | NCic.Rel n as t when n <= k -> t
 505     | NCic.Rel n ->
 506         (try
 507           match List.nth context (n-k-1) with
 508           | _,NCic.Def (bo,_) ->
 509                 (try C.Rel ((position (n-k) l) + k)
 510                  with NotInTheList ->
 511                 (* CSC: This bit of reduction hurts performances since it is
 512                  * possible to  have an exponential explosion of the size of the
 513                  * proof. required for nat/nth_prime.ma *)
 514                   aux k (NCicSubstitution.lift n bo))
 515           | _,NCic.Decl _ -> NCic.Rel ((position (n-k) l) + k)
 516         with Failure _ -> assert false) (*Unbound variable found in delift*)
 517     | NCic.Meta (i,l1) as orig ->
 518         (try
 519            let _,_,t,_ = NCicUtil.lookup_subst i subst in
 520            aux k (NCicSubstitution.subst_meta l1 t)
 521          with NCicUtil.Subst_not_found _ ->
 522            (* see the top level invariant *)
 523            if (i = n) then
 524             raise (MetaSubstFailure (lazy (Printf.sprintf (
 525               "Cannot unify the metavariable ?%d with a term that has "^^
 526               "as subterm %s in which the same metavariable "^^
 527               "occurs (occur check)") i
 528                (NCicPp.ppterm ~context ~metasenv ~subst t))))
 529            else
 530               let shift1,lc1 = l1 in
 531               let shift,lc = l in
 532               match lc, lc1 with
 533               | NCic.Irl len, NCic.Irl len1
 534                 when shift1 < shift || len1 + shift1 > len + shift ->
 535                   (* new meta with shortened l1
 536                     (1 -> shift - shift1 /\ shift + len + 1 -> shift1+len1)
 537                   subst += (i,new meta)
 538                   restrict checks (deleted entry cannot occur in the type...)
 539                   return that meta *)
 540                   assert false
 541               | NCic.Irl len, NCic.Irl len1 when shift = 0 -> orig
 542               | NCic.Irl len, NCic.Irl len1 ->
 543                    NCic.Meta (i, (shift1 - shift, lc1))
 544               | _ ->
 545                   let lc1 = NCicUtils.expand_local_context lc1 in
 546                   let rec deliftl j = function
 547                     | [] -> []
 548                     | t::tl ->
 549                         let tl = deliftl (j+1) tl in
 550                         try (aux (k+shift1) t)::tl
 551                         with
 552                         | NotInTheList | MetaSubstFailure _ ->
 553                             to_be_restricted := (i,j)::!to_be_restricted;
 554                             tl
 555                   in
 556                   let l1 = deliftl 1 l1 in
 557                   C.Meta(i,l1)) (* or another ?k and possibly compress l1 *)
 558     | t -> NCicUtils.map (fun _ k -> k+1) k aux t
 559   in
 560   let t = aux 0 t in
 561   let metasenv, subst = restrict subst !to_be_restricted metasenv in
 562   metasenv, subst, t
 563 ;;
 564
 565
 566   let to_be_restricted = ref [] in
 567   let rec deliftaux k =
 568    let module C = Cic in
 569     function
 570      | C.Rel m as t->
 571          if m <=k then
 572           t
 573          else
 574            (try
 575             match List.nth context (m-k-1) with
 576                Some (_,C.Def (t,_)) ->
 577                 (try
 578                   C.Rel ((position (m-k) l) + k)
 579                  with
 580                   NotInTheList ->
 581                 (*CSC: Hmmm. This bit of reduction is not in the spirit of    *)
 582                 (*CSC: first order unification. Does it help or does it harm? *)
 583                 (*CSC: ANSWER: it hurts performances since it is possible to  *)
 584                 (*CSC: have an exponential explosion of the size of the proof.*)
 585                 (*CSC: However, without this bit of reduction some "apply" in *)
 586                 (*CSC: the library fail (e.g. nat/nth_prime.ma).              *)
 587                   deliftaux k (S.lift m t))
 588              | Some (_,C.Decl t) ->
 589                 C.Rel ((position (m-k) l) + k)
 590              | None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis"))
 591            with
 592             Failure _ ->
 593              raise (MetaSubstFailure (lazy "Unbound variable found in deliftaux"))
 594           )
 595      | C.Var (uri,exp_named_subst) ->
 596         let exp_named_subst' =
 597          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
 598         in
 599          C.Var (uri,exp_named_subst')
 600      | C.Meta (i, l1) as t ->
 601          (try
 602            let (_,t,_) = CicUtil.lookup_subst i subst in
 603              deliftaux k (CicSubstitution.subst_meta l1 t)
 604          with CicUtil.Subst_not_found _ ->
 605            (* see the top level invariant *)
 606            if (i = n) then
 607             raise (MetaSubstFailure (lazy (sprintf
 608               "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
 609               i (ppterm ~metasenv subst t))))
 610           else
 611             begin
 612               let rec deliftl j =
 613                 function
 614                     [] -> []
 615                   | None::tl -> None::(deliftl (j+1) tl)
 616                   | (Some t)::tl ->
 617                       let l1' = (deliftl (j+1) tl) in
 618                         try
 619                           Some (deliftaux k t)::l1'
 620                         with
 621                             NotInTheList
 622                           | MetaSubstFailure _ ->
 623                               to_be_restricted :=
 624                               (i,j)::!to_be_restricted ; None::l1'
 625               in
 626               let l' = deliftl 1 l1 in
 627                 C.Meta(i,l')
 628             end)
 629      | C.Sort _ as t -> t
 630      | C.Implicit _ as t -> t
 631      | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
 632      | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
 633      | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
 634      | C.LetIn (n,s,ty,t) ->
 635         C.LetIn (n, deliftaux k s, deliftaux k ty, deliftaux (k+1) t)
 636      | C.Appl l -> C.Appl (List.map (deliftaux k) l)
 637      | C.Const (uri,exp_named_subst) ->
 638         let exp_named_subst' =
 639          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
 640         in
 641          C.Const (uri,exp_named_subst')
 642      | C.MutInd (uri,typeno,exp_named_subst) ->
 643         let exp_named_subst' =
 644          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
 645         in
 646          C.MutInd (uri,typeno,exp_named_subst')
 647      | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
 648         let exp_named_subst' =
 649          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
 650         in
 651          C.MutConstruct (uri,typeno,consno,exp_named_subst')
 652      | C.MutCase (sp,i,outty,t,pl) ->
 653         C.MutCase (sp, i, deliftaux k outty, deliftaux k t,
 654          List.map (deliftaux k) pl)
 655      | C.Fix (i, fl) ->
 656         let len = List.length fl in
 657         let liftedfl =
 658          List.map
 659           (fun (name, i, ty, bo) ->
 660            (name, i, deliftaux k ty, deliftaux (k+len) bo))
 661            fl
 662         in
 663          C.Fix (i, liftedfl)
 664      | C.CoFix (i, fl) ->
 665         let len = List.length fl in
 666         let liftedfl =
 667          List.map
 668           (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo))
 669            fl
 670         in
 671          C.CoFix (i, liftedfl)
 672   in
 673    let res =
 674     try
 675      deliftaux 0 t
 676     with
 677      NotInTheList ->
 678       (* This is the case where we fail even first order unification. *)
 679       (* The reason is that our delift function is weaker than first  *)
 680       (* order (in the sense of alpha-conversion). See comment above  *)
 681       (* related to the delift function.                              *)
 682 (* debug_print (lazy "First Order UnificationFailure during delift") ;
 683 debug_print(lazy (sprintf
 684         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
 685         (ppterm subst t)
 686         (String.concat "; "
 687           (List.map
 688             (function Some t -> ppterm subst t | None -> "_") l
 689           )))); *)
 690       let msg = (lazy (sprintf
 691         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
 692         (ppterm ~metasenv subst t)
 693         (String.concat "; "
 694           (List.map
 695             (function Some t -> ppterm ~metasenv subst t | None -> "_")
 696             l))))
 697       in
 698        if
 699          List.exists
 700           (function
 701               Some t -> CicUtil.is_meta_closed (apply_subst subst t)
 702             | None -> true) l
 703        then
 704         raise (Uncertain msg)
 705        else
 706         raise (MetaSubstFailure msg)
 707    in
 708    let (metasenv, subst) = restrict subst !to_be_restricted metasenv in
 709     res, metasenv, subst
 710 ;;
 711
 712 (* delifts a term t of n levels strating from k, that is changes (Rel m)
 713  * to (Rel (m - n)) when m > (k + n). if k <= m < k + n delift fails
 714  *)
 715 let delift_rels_from subst metasenv k n =
 716  let rec liftaux subst metasenv k =
 717   let module C = Cic in
 718    function
 719       C.Rel m as t ->
 720        if m < k then
 721         t, subst, metasenv
 722        else if m < k + n then
 723          raise DeliftingARelWouldCaptureAFreeVariable
 724        else
 725         C.Rel (m - n), subst, metasenv
 726     | C.Var (uri,exp_named_subst) ->
 727        let exp_named_subst',subst,metasenv =
 728         List.fold_right
 729          (fun (uri,t) (l,subst,metasenv) ->
 730            let t',subst,metasenv = liftaux subst metasenv k t in
 731             (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
 732        in
 733         C.Var (uri,exp_named_subst'),subst,metasenv
 734     | C.Meta (i,l) ->
 735         (try
 736           let (_, t,_) = lookup_subst i subst in
 737            liftaux subst metasenv k (CicSubstitution.subst_meta l t)
 738          with CicUtil.Subst_not_found _ ->
 739           let l',to_be_restricted,subst,metasenv =
 740            let rec aux con l subst metasenv =
 741             match l with
 742                [] -> [],[],subst,metasenv
 743              | he::tl ->
 744                 let tl',to_be_restricted,subst,metasenv =
 745                  aux (con + 1) tl subst metasenv in
 746                 let he',more_to_be_restricted,subst,metasenv =
 747                  match he with
 748                     None -> None,[],subst,metasenv
 749                   | Some t ->
 750                      try
 751                       let t',subst,metasenv = liftaux subst metasenv k t in
 752                        Some t',[],subst,metasenv
 753                      with
 754                       DeliftingARelWouldCaptureAFreeVariable ->
 755                        None,[i,con],subst,metasenv
 756                 in
 757                  he'::tl',more_to_be_restricted@to_be_restricted,subst,metasenv
 758            in
 759             aux 1 l subst metasenv in
 760           let metasenv,subst = restrict subst to_be_restricted metasenv in
 761            C.Meta(i,l'),subst,metasenv)
 762     | C.Sort _ as t -> t,subst,metasenv
 763     | C.Implicit _ as t -> t,subst,metasenv
 764     | C.Cast (te,ty) ->
 765        let te',subst,metasenv = liftaux subst metasenv k te in
 766        let ty',subst,metasenv = liftaux subst metasenv k ty in
 767         C.Cast (te',ty'),subst,metasenv
 768     | C.Prod (n,s,t) ->
 769        let s',subst,metasenv = liftaux subst metasenv k s in
 770        let t',subst,metasenv = liftaux subst metasenv (k+1) t in
 771         C.Prod (n,s',t'),subst,metasenv
 772     | C.Lambda (n,s,t) ->
 773        let s',subst,metasenv = liftaux subst metasenv k s in
 774        let t',subst,metasenv = liftaux subst metasenv (k+1) t in
 775         C.Lambda (n,s',t'),subst,metasenv
 776     | C.LetIn (n,s,ty,t) ->
 777        let s',subst,metasenv = liftaux subst metasenv k s in
 778        let ty',subst,metasenv = liftaux subst metasenv k ty in
 779        let t',subst,metasenv = liftaux subst metasenv (k+1) t in
 780         C.LetIn (n,s',ty',t'),subst,metasenv
 781     | C.Appl l ->
 782        let l',subst,metasenv =
 783         List.fold_right
 784          (fun t (l,subst,metasenv) ->
 785            let t',subst,metasenv = liftaux subst metasenv k t in
 786             t'::l,subst,metasenv) l ([],subst,metasenv) in
 787        C.Appl l',subst,metasenv
 788     | C.Const (uri,exp_named_subst) ->
 789        let exp_named_subst',subst,metasenv =
 790         List.fold_right
 791          (fun (uri,t) (l,subst,metasenv) ->
 792            let t',subst,metasenv = liftaux subst metasenv k t in
 793             (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
 794        in
 795         C.Const (uri,exp_named_subst'),subst,metasenv
 796     | C.MutInd (uri,tyno,exp_named_subst) ->
 797        let exp_named_subst',subst,metasenv =
 798         List.fold_right
 799          (fun (uri,t) (l,subst,metasenv) ->
 800            let t',subst,metasenv = liftaux subst metasenv k t in
 801             (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
 802        in
 803         C.MutInd (uri,tyno,exp_named_subst'),subst,metasenv
 804     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 805        let exp_named_subst',subst,metasenv =
 806         List.fold_right
 807          (fun (uri,t) (l,subst,metasenv) ->
 808            let t',subst,metasenv = liftaux subst metasenv k t in
 809             (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
 810        in
 811         C.MutConstruct (uri,tyno,consno,exp_named_subst'),subst,metasenv
 812     | C.MutCase (sp,i,outty,t,pl) ->
 813        let outty',subst,metasenv = liftaux subst metasenv k outty in
 814        let t',subst,metasenv = liftaux subst metasenv k t in
 815        let pl',subst,metasenv =
 816         List.fold_right
 817          (fun t (l,subst,metasenv) ->
 818            let t',subst,metasenv = liftaux subst metasenv k t in
 819             t'::l,subst,metasenv) pl ([],subst,metasenv)
 820        in
 821         C.MutCase (sp,i,outty',t',pl'),subst,metasenv
 822     | C.Fix (i, fl) ->
 823        let len = List.length fl in
 824        let liftedfl,subst,metasenv =
 825         List.fold_right
 826          (fun (name, i, ty, bo) (l,subst,metasenv) ->
 827            let ty',subst,metasenv = liftaux subst metasenv k ty in
 828            let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in
 829             (name,i,ty',bo')::l,subst,metasenv
 830          ) fl ([],subst,metasenv)
 831        in
 832         C.Fix (i, liftedfl),subst,metasenv
 833     | C.CoFix (i, fl) ->
 834        let len = List.length fl in
 835        let liftedfl,subst,metasenv =
 836         List.fold_right
 837          (fun (name, ty, bo) (l,subst,metasenv) ->
 838            let ty',subst,metasenv = liftaux subst metasenv k ty in
 839            let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in
 840             (name,ty',bo')::l,subst,metasenv
 841          ) fl ([],subst,metasenv)
 842        in
 843         C.CoFix (i, liftedfl),subst,metasenv
 844  in
 845   liftaux subst metasenv k
 846
 847 let delift_rels subst metasenv n t =
 848   delift_rels_from subst metasenv 1 n t
 849
 850