helm/ocaml/cic_unification/cicMetaSubst.ml

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