helm/ocaml/cic_unification/cicMetaSubst.ml

   1 (* Copyright (C) 2004, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 open Printf
  27
  28 (*  (* PROFILING *)
  29 let apply_subst_counter = ref 0
  30 let apply_subst_context_counter = ref 0
  31 let apply_subst_metasenv_counter = ref 0
  32 let lift_counter = ref 0
  33 let subst_counter = ref 0
  34 let whd_counter = ref 0
  35 let are_convertible_counter = ref 0
  36 let metasenv_length = ref 0
  37 let context_length = ref 0
  38 let reset_counters () =
  39  apply_subst_counter := 0;
  40  apply_subst_context_counter := 0;
  41  apply_subst_metasenv_counter := 0;
  42  lift_counter := 0;
  43  subst_counter := 0;
  44  whd_counter := 0;
  45  are_convertible_counter := 0;
  46  metasenv_length := 0;
  47  context_length := 0
  48 let print_counters () =
  49   prerr_endline (Printf.sprintf
  50 "apply_subst: %d
  51 apply_subst_context: %d
  52 apply_subst_metasenv: %d
  53 lift: %d
  54 subst: %d
  55 whd: %d
  56 are_convertible: %d
  57 metasenv length: %d (avg = %.2f)
  58 context length: %d (avg = %.2f)
  59 "
  60   !apply_subst_counter !apply_subst_context_counter
  61   !apply_subst_metasenv_counter !lift_counter !subst_counter !whd_counter
  62   !are_convertible_counter !metasenv_length
  63   ((float !metasenv_length) /. (float !apply_subst_metasenv_counter))
  64   !context_length
  65   ((float !context_length) /. (float !apply_subst_context_counter))
  66   )
  67 *)
  68
  69 exception MetaSubstFailure of string
  70 exception Uncertain of string
  71 exception AssertFailure of string
  72 exception SubstNotFound of int
  73
  74 let debug_print = prerr_endline
  75
  76 type substitution = (int * (Cic.context * Cic.term)) list
  77
  78 let lookup_subst n subst =
  79   try
  80     List.assoc n subst
  81   with Not_found -> raise (SubstNotFound n)
  82
  83 (*** Functions to apply a substitution ***)
  84
  85 let apply_subst_gen ~appl_fun subst term =
  86  let rec um_aux =
  87   let module C = Cic in
  88   let module S = CicSubstitution in
  89    function
  90       C.Rel _ as t -> t
  91     | C.Var (uri,exp_named_subst) ->
  92        let exp_named_subst' =
  93          List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
  94        in
  95        C.Var (uri, exp_named_subst')
  96     | C.Meta (i, l) ->
  97         (try
  98           let (context, t) = lookup_subst i subst in
  99           um_aux (S.lift_meta l t)
 100         with SubstNotFound _ -> (* unconstrained variable, i.e. free in subst*)
 101           let l' =
 102             List.map (function None -> None | Some t -> Some (um_aux t)) l
 103           in
 104            C.Meta (i,l'))
 105     | C.Sort _ as t -> t
 106     | C.Implicit _ -> assert false
 107     | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
 108     | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
 109     | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
 110     | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t)
 111     | C.Appl (hd :: tl) -> appl_fun um_aux hd tl
 112     | C.Appl _ -> assert false
 113     | C.Const (uri,exp_named_subst) ->
 114        let exp_named_subst' =
 115          List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
 116        in
 117        C.Const (uri, exp_named_subst')
 118     | C.MutInd (uri,typeno,exp_named_subst) ->
 119        let exp_named_subst' =
 120          List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
 121        in
 122        C.MutInd (uri,typeno,exp_named_subst')
 123     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
 124        let exp_named_subst' =
 125          List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
 126        in
 127        C.MutConstruct (uri,typeno,consno,exp_named_subst')
 128     | C.MutCase (sp,i,outty,t,pl) ->
 129        let pl' = List.map um_aux pl in
 130        C.MutCase (sp, i, um_aux outty, um_aux t, pl')
 131     | C.Fix (i, fl) ->
 132        let fl' =
 133          List.map (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo)) fl
 134        in
 135        C.Fix (i, fl')
 136     | C.CoFix (i, fl) ->
 137        let fl' =
 138          List.map (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo)) fl
 139        in
 140        C.CoFix (i, fl')
 141  in
 142  um_aux term
 143 ;;
 144
 145 let apply_subst =
 146 (* CSC: old code that never performs beta reduction
 147   let appl_fun um_aux he tl =
 148     let tl' = List.map um_aux tl in
 149       begin
 150        match um_aux he with
 151           Cic.Appl l -> Cic.Appl (l@tl')
 152         | he' -> Cic.Appl (he'::tl')
 153       end
 154   in
 155   apply_subst_gen ~appl_fun
 156 *)
 157   let appl_fun um_aux he tl =
 158     let tl' = List.map um_aux tl in
 159     let t' =
 160      match um_aux he with
 161         Cic.Appl l -> Cic.Appl (l@tl')
 162       | he' -> Cic.Appl (he'::tl')
 163     in
 164      begin
 165       match he with
 166          Cic.Meta (m,_) ->
 167           let rec beta_reduce =
 168            function
 169               (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
 170                 let he'' = CicSubstitution.subst he' t in
 171                  if tl' = [] then
 172                   he''
 173                  else
 174                   beta_reduce (Cic.Appl(he''::tl'))
 175             | t -> t
 176           in
 177            beta_reduce t'
 178        | _ -> t'
 179      end
 180   in
 181   fun s t ->
 182 (*     incr apply_subst_counter; *)
 183     apply_subst_gen ~appl_fun s t
 184 ;;
 185
 186 let rec apply_subst_context subst context =
 187 (*
 188   incr apply_subst_context_counter;
 189   context_length := !context_length + List.length context;
 190 *)
 191   List.fold_right
 192     (fun item context ->
 193       match item with
 194       | Some (n, Cic.Decl t) ->
 195           let t' = apply_subst subst t in
 196           Some (n, Cic.Decl t') :: context
 197       | Some (n, Cic.Def (t, ty)) ->
 198           let ty' =
 199             match ty with
 200             | None -> None
 201             | Some ty -> Some (apply_subst subst ty)
 202           in
 203           let t' = apply_subst subst t in
 204           Some (n, Cic.Def (t', ty')) :: context
 205       | None -> None :: context)
 206     context []
 207
 208 let apply_subst_metasenv subst metasenv =
 209 (*
 210   incr apply_subst_metasenv_counter;
 211   metasenv_length := !metasenv_length + List.length metasenv;
 212 *)
 213   List.map
 214     (fun (n, context, ty) ->
 215       (n, apply_subst_context subst context, apply_subst subst ty))
 216     (List.filter
 217       (fun (i, _, _) -> not (List.mem_assoc i subst))
 218       metasenv)
 219
 220 (***** Pretty printing functions ******)
 221
 222 let ppsubst subst =
 223   String.concat "\n"
 224     (List.map
 225       (fun (idx, (_, term)) ->
 226         Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
 227       subst)
 228 ;;
 229
 230 let ppterm subst term = CicPp.ppterm (apply_subst subst term)
 231
 232 let ppterm_in_context subst term name_context =
 233  CicPp.pp (apply_subst subst term) name_context
 234
 235 let ppcontext' ?(sep = "\n") subst context =
 236  let separate s = if s = "" then "" else s ^ sep in
 237   List.fold_right
 238    (fun context_entry (i,name_context) ->
 239      match context_entry with
 240         Some (n,Cic.Decl t) ->
 241          sprintf "%s%s : %s" (separate i) (CicPp.ppname n)
 242           (ppterm_in_context subst t name_context), (Some n)::name_context
 243       | Some (n,Cic.Def (bo,ty)) ->
 244          sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n)
 245           (match ty with
 246               None -> "_"
 247             | Some ty -> ppterm_in_context subst ty name_context)
 248           (ppterm_in_context subst bo name_context), (Some n)::name_context
 249        | None ->
 250           sprintf "%s_ :? _" (separate i), None::name_context
 251     ) context ("",[])
 252
 253 let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context)
 254
 255 let ppmetasenv ?(sep = "\n") metasenv subst =
 256   String.concat sep
 257     (List.map
 258       (fun (i, c, t) ->
 259         let context,name_context = ppcontext' ~sep:"; " subst c in
 260          sprintf "%s |- ?%d: %s" context i
 261           (ppterm_in_context subst t name_context))
 262       (List.filter
 263         (fun (i, _, _) -> not (List.mem_assoc i subst))
 264         metasenv))
 265
 266 (* From now on we recreate a kernel abstraction where substitutions are part of
 267  * the calculus *)
 268
 269 let lift subst n term =
 270 (*   incr subst_counter; *)
 271   let term = apply_subst subst term in
 272   try
 273     CicSubstitution.lift n term
 274   with e ->
 275     raise (MetaSubstFailure ("Lift failure: " ^ Printexc.to_string e))
 276
 277 let subst subst t1 t2 =
 278 (*   incr subst_counter; *)
 279   let t1 = apply_subst subst t1 in
 280   let t2 = apply_subst subst t2 in
 281   try
 282     CicSubstitution.subst t1 t2
 283   with e ->
 284     raise (MetaSubstFailure ("Subst failure: " ^ Printexc.to_string e))
 285
 286 let whd subst context term =
 287 (*   incr whd_counter; *)
 288   let term = apply_subst subst term in
 289   let context = apply_subst_context subst context in
 290   try
 291     CicReduction.whd context term
 292   with e ->
 293     raise (MetaSubstFailure ("Weak head reduction failure: " ^
 294       Printexc.to_string e))
 295
 296 let are_convertible subst context t1 t2 =
 297 (*   incr are_convertible_counter; *)
 298   let context = apply_subst_context subst context in
 299   let t1 = apply_subst subst t1 in
 300   let t2 = apply_subst subst t2 in
 301   CicReduction.are_convertible context t1 t2
 302
 303 let tempi_type_of_aux_subst = ref 0.0;;
 304 let tempi_subst = ref 0.0;;
 305 let tempi_type_of_aux = ref 0.0;;
 306
 307   (* assumption: metasenv is already instantiated wrt subst *)
 308 let type_of_aux' metasenv subst context term =
 309   let time1 = Unix.gettimeofday () in
 310   let term = apply_subst subst term in
 311   let context = apply_subst_context subst context in
 312 (*   let metasenv = apply_subst_metasenv subst metasenv in *)
 313   let time2 = Unix.gettimeofday () in
 314   let res =
 315     try
 316       CicTypeChecker.type_of_aux' metasenv context term
 317     with CicTypeChecker.TypeCheckerFailure msg ->
 318       raise (MetaSubstFailure ("Type checker failure: " ^ msg))
 319   in
 320   let time3 = Unix.gettimeofday () in
 321    tempi_type_of_aux_subst := !tempi_type_of_aux_subst +. time3 -. time1 ;
 322    tempi_subst := !tempi_subst +. time2 -. time1 ;
 323    tempi_type_of_aux := !tempi_type_of_aux +. time3 -. time2 ;
 324    res
 325
 326 (**** DELIFT ****)
 327 (* the delift function takes in input a metavariable index, an ordered list of
 328  * optional terms [t1,...,tn] and a term t, and substitutes every tk = Some
 329  * (rel(nk)) with rel(k).  Typically, the list of optional terms is the explicit
 330  * substitution that is applied to a metavariable occurrence and the result of
 331  * the delift function is a term the implicit variable can be substituted with
 332  * to make the term [t] unifiable with the metavariable occurrence.  In general,
 333  * the problem is undecidable if we consider equivalence in place of alpha
 334  * convertibility. Our implementation, though, is even weaker than alpha
 335  * convertibility, since it replace the term [tk] if and only if [tk] is a Rel
 336  * (missing all the other cases). Does this matter in practice?
 337  * The metavariable index is the index of the metavariable that must not occur
 338  * in the term (for occur check).
 339  *)
 340
 341 exception NotInTheList;;
 342
 343 let position n =
 344   let rec aux k =
 345    function
 346        [] -> raise NotInTheList
 347      | (Some (Cic.Rel m))::_ when m=n -> k
 348      | _::tl -> aux (k+1) tl in
 349   aux 1
 350 ;;
 351
 352 exception Occur;;
 353
 354 let rec force_does_not_occur subst to_be_restricted t =
 355  let module C = Cic in
 356  let more_to_be_restricted = ref [] in
 357  let rec aux k = function
 358       C.Rel r when List.mem (r - k) to_be_restricted -> raise Occur
 359     | C.Rel _
 360     | C.Sort _ as t -> t
 361     | C.Implicit _ -> assert false
 362     | C.Meta (n, l) ->
 363        (* we do not retrieve the term associated to ?n in subst since *)
 364        (* in this way we can restrict if something goes wrong         *)
 365        let l' =
 366          let i = ref 0 in
 367          List.map
 368            (function t ->
 369              incr i ;
 370              match t with
 371                 None -> None
 372               | Some t ->
 373                  try
 374                    Some (aux k t)
 375                  with Occur ->
 376                    more_to_be_restricted := (n,!i) :: !more_to_be_restricted;
 377                    None)
 378            l
 379        in
 380         C.Meta (n, l')
 381     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
 382     | C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest)
 383     | C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest)
 384     | C.LetIn (name,so,dest) -> C.LetIn (name, aux k so, aux (k+1) dest)
 385     | C.Appl l -> C.Appl (List.map (aux k) l)
 386     | C.Var (uri,exp_named_subst) ->
 387         let exp_named_subst' =
 388           List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
 389         in
 390         C.Var (uri, exp_named_subst')
 391     | C.Const (uri, exp_named_subst) ->
 392         let exp_named_subst' =
 393           List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
 394         in
 395         C.Const (uri, exp_named_subst')
 396     | C.MutInd (uri,tyno,exp_named_subst) ->
 397         let exp_named_subst' =
 398           List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
 399         in
 400         C.MutInd (uri, tyno, exp_named_subst')
 401     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 402         let exp_named_subst' =
 403           List.map (fun (uri,t) -> (uri, aux k t)) exp_named_subst
 404         in
 405         C.MutConstruct (uri, tyno, consno, exp_named_subst')
 406     | C.MutCase (uri,tyno,out,te,pl) ->
 407         C.MutCase (uri, tyno, aux k out, aux k te, List.map (aux k) pl)
 408     | C.Fix (i,fl) ->
 409        let len = List.length fl in
 410        let k_plus_len = k + len in
 411        let fl' =
 412          List.map
 413           (fun (name,j,ty,bo) -> (name, j, aux k ty, aux k_plus_len bo)) fl
 414        in
 415        C.Fix (i, fl')
 416     | C.CoFix (i,fl) ->
 417        let len = List.length fl in
 418        let k_plus_len = k + len in
 419        let fl' =
 420          List.map
 421           (fun (name,ty,bo) -> (name, aux k ty, aux k_plus_len bo)) fl
 422        in
 423        C.CoFix (i, fl')
 424  in
 425  let res = aux 0 t in
 426  (!more_to_be_restricted, res)
 427
 428 let rec restrict subst to_be_restricted metasenv =
 429   let names_of_context_indexes context indexes =
 430     String.concat ", "
 431       (List.map
 432         (fun i ->
 433           try
 434            match List.nth context i with
 435            | None -> assert false
 436            | Some (n, _) -> CicPp.ppname n
 437           with
 438            Failure _ -> assert false
 439         ) indexes)
 440   in
 441   let force_does_not_occur_in_context to_be_restricted = function
 442     | None -> [], None
 443     | Some (name, Cic.Decl t) ->
 444         let (more_to_be_restricted, t') =
 445           force_does_not_occur subst to_be_restricted t
 446         in
 447         more_to_be_restricted, Some (name, Cic.Decl t')
 448     | Some (name, Cic.Def (bo, ty)) ->
 449         let (more_to_be_restricted, bo') =
 450           force_does_not_occur subst to_be_restricted bo
 451         in
 452         let more_to_be_restricted, ty' =
 453           match ty with
 454           | None ->  more_to_be_restricted, None
 455           | Some ty ->
 456               let more_to_be_restricted', ty' =
 457                 force_does_not_occur subst to_be_restricted ty
 458               in
 459               more_to_be_restricted @ more_to_be_restricted',
 460               Some ty'
 461         in
 462         more_to_be_restricted, Some (name, Cic.Def (bo', ty'))
 463   in
 464   let rec erase i to_be_restricted n = function
 465     | [] -> [], to_be_restricted, []
 466     | hd::tl ->
 467         let more_to_be_restricted,restricted,tl' =
 468          erase (i+1) to_be_restricted n tl
 469         in
 470         let restrict_me = List.mem i restricted in
 471         if restrict_me then
 472          more_to_be_restricted, restricted, None:: tl'
 473         else
 474           (try
 475             let more_to_be_restricted', hd' =
 476               let delifted_restricted =
 477                let rec aux =
 478                 function
 479                    [] -> []
 480                  | j::tl when j > i -> (j - i)::aux tl
 481                  | _::tl -> aux tl
 482                in
 483                 aux restricted
 484               in
 485                force_does_not_occur_in_context delifted_restricted hd
 486             in
 487              more_to_be_restricted @ more_to_be_restricted',
 488              restricted, hd' :: tl'
 489           with Occur ->
 490             more_to_be_restricted, (i :: restricted), None :: tl')
 491   in
 492   let (more_to_be_restricted, metasenv) =  (* restrict metasenv *)
 493     List.fold_right
 494       (fun (n, context, t) (more, metasenv) ->
 495         let to_be_restricted =
 496           List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
 497         in
 498         let (more_to_be_restricted, restricted, context') =
 499          (* just an optimization *)
 500          if to_be_restricted = [] then
 501           [],[],context
 502          else
 503           erase 1 to_be_restricted n context
 504         in
 505         try
 506           let more_to_be_restricted', t' =
 507             force_does_not_occur subst restricted t
 508           in
 509           let metasenv' = (n, context', t') :: metasenv in
 510           (more @ more_to_be_restricted @ more_to_be_restricted',
 511           metasenv')
 512         with Occur ->
 513           raise (MetaSubstFailure (sprintf
 514             "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them"
 515             n (names_of_context_indexes context to_be_restricted))))
 516       metasenv ([], [])
 517   in
 518   let (more_to_be_restricted', subst) = (* restrict subst *)
 519     List.fold_right
 520       (fun (n, (context, term)) (more, subst) ->
 521         let to_be_restricted =
 522           List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
 523         in
 524         (try
 525           let (more_to_be_restricted, restricted, context') =
 526            (* just an optimization *)
 527             if to_be_restricted = [] then
 528               [], [], context
 529             else
 530               erase 1 to_be_restricted n context
 531           in
 532           let more_to_be_restricted', term' =
 533             force_does_not_occur subst restricted term
 534           in
 535           let subst' = (n, (context', term')) :: subst in
 536           let more = more @ more_to_be_restricted @ more_to_be_restricted' in
 537           (more, subst')
 538         with Occur ->
 539           raise (MetaSubstFailure (sprintf
 540             "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"
 541             n (names_of_context_indexes context to_be_restricted) n
 542             (ppterm subst term)))))
 543       subst ([], [])
 544   in
 545   match more_to_be_restricted @ more_to_be_restricted' with
 546   | [] -> (metasenv, subst)
 547   | l -> restrict subst l metasenv
 548 ;;
 549
 550 (*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)
 551 let delift n subst context metasenv l t =
 552  let module S = CicSubstitution in
 553   let l =
 554    let (_, canonical_context, _) = CicUtil.lookup_meta n metasenv in
 555    List.map2 (fun ct lt ->
 556      match (ct, lt) with
 557      | None, _ -> None
 558      | Some _, _ -> lt)
 559      canonical_context l
 560   in
 561   let to_be_restricted = ref [] in
 562   let rec deliftaux k =
 563    let module C = Cic in
 564     function
 565        C.Rel m ->
 566          if m <=k then
 567           C.Rel m   (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *)
 568                     (*CSC: deliftato la regola per il LetIn                 *)
 569                     (*CSC: FALSO! La regola per il LetIn non lo fa          *)
 570          else
 571           (try
 572             match List.nth context (m-k-1) with
 573                Some (_,C.Def (t,_)) ->
 574                 (*CSC: Hmmm. This bit of reduction is not in the spirit of    *)
 575                 (*CSC: first order unification. Does it help or does it harm? *)
 576                 deliftaux k (S.lift m t)
 577              | Some (_,C.Decl t) ->
 578                 C.Rel ((position (m-k) l) + k)
 579              | None -> raise (MetaSubstFailure "RelToHiddenHypothesis")
 580            with
 581             Failure _ ->
 582              raise (MetaSubstFailure "Unbound variable found in deliftaux")
 583           )
 584      | C.Var (uri,exp_named_subst) ->
 585         let exp_named_subst' =
 586          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
 587         in
 588          C.Var (uri,exp_named_subst')
 589      | C.Meta (i, l1) as t ->
 590         if i = n then
 591           raise (MetaSubstFailure (sprintf
 592             "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
 593             i (ppterm subst t)))
 594         else
 595          (* I do not consider the term associated to ?i in subst since *)
 596          (* in this way I can restrict if something goes wrong.        *)
 597           let rec deliftl j =
 598            function
 599               [] -> []
 600             | None::tl -> None::(deliftl (j+1) tl)
 601             | (Some t)::tl ->
 602                let l1' = (deliftl (j+1) tl) in
 603                 try
 604                  Some (deliftaux k t)::l1'
 605                 with
 606                    NotInTheList
 607                  | MetaSubstFailure _ ->
 608                     to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
 609           in
 610            let l' = deliftl 1 l1 in
 611             C.Meta(i,l')
 612      | C.Sort _ as t -> t
 613      | C.Implicit _ as t -> t
 614      | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
 615      | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t)
 616      | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t)
 617      | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t)
 618      | C.Appl l -> C.Appl (List.map (deliftaux k) l)
 619      | C.Const (uri,exp_named_subst) ->
 620         let exp_named_subst' =
 621          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
 622         in
 623          C.Const (uri,exp_named_subst')
 624      | C.MutInd (uri,typeno,exp_named_subst) ->
 625         let exp_named_subst' =
 626          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
 627         in
 628          C.MutInd (uri,typeno,exp_named_subst')
 629      | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
 630         let exp_named_subst' =
 631          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
 632         in
 633          C.MutConstruct (uri,typeno,consno,exp_named_subst')
 634      | C.MutCase (sp,i,outty,t,pl) ->
 635         C.MutCase (sp, i, deliftaux k outty, deliftaux k t,
 636          List.map (deliftaux k) pl)
 637      | C.Fix (i, fl) ->
 638         let len = List.length fl in
 639         let liftedfl =
 640          List.map
 641           (fun (name, i, ty, bo) ->
 642            (name, i, deliftaux k ty, deliftaux (k+len) bo))
 643            fl
 644         in
 645          C.Fix (i, liftedfl)
 646      | C.CoFix (i, fl) ->
 647         let len = List.length fl in
 648         let liftedfl =
 649          List.map
 650           (fun (name, ty, bo) -> (name, deliftaux k ty, deliftaux (k+len) bo))
 651            fl
 652         in
 653          C.CoFix (i, liftedfl)
 654   in
 655    let res =
 656     try
 657      deliftaux 0 t
 658     with
 659      NotInTheList ->
 660       (* This is the case where we fail even first order unification. *)
 661       (* The reason is that our delift function is weaker than first  *)
 662       (* order (in the sense of alpha-conversion). See comment above  *)
 663       (* related to the delift function.                              *)
 664 debug_print "\n!!!!!!!!!!! First Order UnificationFailure, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ;
 665       raise (Uncertain (sprintf
 666         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
 667         (ppterm subst t)
 668         (String.concat "; "
 669           (List.map
 670             (function Some t -> ppterm subst t | None -> "_")
 671             l))))
 672    in
 673    let (metasenv, subst) = restrict subst !to_be_restricted metasenv in
 674     res, metasenv, subst
 675 ;;
 676
 677 (**** END OF DELIFT ****)
 678
 679
 680 (** {2 Format-like pretty printers} *)
 681
 682 let fpp_gen ppf s =
 683   Format.pp_print_string ppf s;
 684   Format.pp_print_newline ppf ();
 685   Format.pp_print_flush ppf ()
 686
 687 let fppsubst ppf subst = fpp_gen ppf (ppsubst subst)
 688 let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term)
 689 let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv metasenv [])
 690